@[simp]

theorem Matroid.preimage_image_sigmaMk {ι : Type u_1} {α : ι → Type u_2} (i : ι) (s : Set (α i)) : Sigma.mk i ⁻¹' Sigma.mk i '' s = s

@[simp]

theorem Matroid.iUnion_preimage_image_sigma_mk_eq_self {ι : Type u_1} {α : ι → Type u_2} {s : (i : ι) → Set (α i)} {i₀ : ι} : ⋃ (i : ι), Sigma.mk i₀ ⁻¹' Sigma.mk i '' s i = s i₀

@[simp]

theorem Matroid.Sum.preimage_image_inl (α : Type u_1) (β : Type u_2) (X : Set α) : Sum.inl ⁻¹' Sum.inl '' X = X

@[simp]

theorem Matroid.Sum.preimage_image_inr (α : Type u_1) (β : Type u_2) (X : Set β) : Sum.inr ⁻¹' Sum.inr '' X = X

@[simp]

theorem Matroid.Sum.preimage_inl_insert_inl (α : Type u_1) (β : Type u_2) (X : Set (α ⊕ β)) (e : α) : Sum.inl ⁻¹' insert (Sum.inl e) X = insert e (Sum.inl ⁻¹' X)

@[simp]

theorem Matroid.Sum.preimage_inr_insert_inr (α : Type u_1) (β : Type u_2) (X : Set (α ⊕ β)) (e : β) : Sum.inr ⁻¹' insert (Sum.inr e) X = insert e (Sum.inr ⁻¹' X)

@[simp]

theorem Matroid.Sum.preimage_inl_insert_inr (α : Type u_1) (β : Type u_2) (X : Set (α ⊕ β)) (e : β) : Sum.inl ⁻¹' insert (Sum.inr e) X = Sum.inl ⁻¹' X

@[simp]

theorem Matroid.Sum.preimage_inr_insert_inl (α : Type u_1) (β : Type u_2) (X : Set (α ⊕ β)) (e : α) : Sum.inr ⁻¹' insert (Sum.inl e) X = Sum.inr ⁻¹' X

theorem Matroid.Indep.sigma {ι : Type u_1} {α : ι → Type u_2} {M : (i : ι) → Matroid (α i)} {I : (i : ι) → Set (α i)} (h : ∀ (i : ι), (M i).Indep (I i)) : (Matroid.sigma M).Indep (⋃ (i : ι), Sigma.mk i '' I i)

theorem Matroid.sigma_dep_iff {ι : Type u_1} {α : ι → Type u_2} {M : (i : ι) → Matroid (α i)} {X : Set ((i : ι) × α i)} : (Matroid.sigma M).Dep X ↔ ∃ (i : ι), (M i).Dep (Sigma.mk i ⁻¹' X) ∧ ∀ (i : ι), Sigma.mk i ⁻¹' X ⊆ (M i).E

theorem Matroid.sigma_image_indep_iff {ι : Type u_1} {α : ι → Type u_2} {M : (i : ι) → Matroid (α i)} {i : ι} {I : Set (α i)} : (Matroid.sigma M).Indep (Sigma.mk i '' I) ↔ (M i).Indep I

theorem Matroid.sigma_image_dep_iff {ι : Type u_1} {α : ι → Type u_2} {M : (i : ι) → Matroid (α i)} {i : ι} {D : Set (α i)} : (Matroid.sigma M).Dep (Sigma.mk i '' D) ↔ (M i).Dep D

theorem Matroid.IsBase.sigma {ι : Type u_1} {α : ι → Type u_2} {M : (i : ι) → Matroid (α i)} {B : (i : ι) → Set (α i)} (h : ∀ (i : ι), (M i).IsBase (B i)) : (Matroid.sigma M).IsBase (⋃ (i : ι), Sigma.mk i '' B i)

theorem Matroid.IsBasis.sigma {ι : Type u_1} {α : ι → Type u_2} {M : (i : ι) → Matroid (α i)} {I X : (i : ι) → Set (α i)} (h : ∀ (i : ι), (M i).IsBasis (I i) (X i)) : (Matroid.sigma M).IsBasis (⋃ (i : ι), Sigma.mk i '' I i) (⋃ (i : ι), Sigma.mk i '' X i)

theorem Matroid.sigma_isBasis_iff' {ι : Type u_1} {α : ι → Type u_2} {M : (i : ι) → Matroid (α i)} {I X : Set ((i : ι) × α i)} : (Matroid.sigma M).IsBasis I X ↔ ∀ (i : ι), (M i).IsBasis (Sigma.mk i ⁻¹' I) (Sigma.mk i ⁻¹' X)

theorem Matroid.sigma_isBasis'_iff' {ι : Type u_1} {α : ι → Type u_2} {M : (i : ι) → Matroid (α i)} {I X : Set ((i : ι) × α i)} : (Matroid.sigma M).IsBasis' I X ↔ ∀ (i : ι), (M i).IsBasis' (Sigma.mk i ⁻¹' I) (Sigma.mk i ⁻¹' X)

theorem Matroid.sigma_closure_eq {ι : Type u_1} {α : ι → Type u_2} {M : (i : ι) → Matroid (α i)} (X : Set ((i : ι) × α i)) : (Matroid.sigma M).closure X = ⋃ (i : ι), Sigma.mk i '' (M i).closure (Sigma.mk i ⁻¹' X)

theorem Matroid.sigma_dual_eq {ι : Type u_1} {α : ι → Type u_2} {M : (i : ι) → Matroid (α i)} : (Matroid.sigma M)✶ = Matroid.sigma fun (i : ι) => (M i)✶

theorem Matroid.Indep.disjointSigma_iUnion {ι : Type u_1} {α : Type u_2} {M : ι → Matroid α} {I : ι → Set α} (h : Pairwise (Function.onFun Disjoint fun (i : ι) => (M i).E)) (hI : ∀ (i : ι), (M i).Indep (I i)) : (Matroid.disjointSigma M h).Indep (⋃ (i : ι), I i)

theorem Matroid.IsBase.disjointSigma_iUnion {ι : Type u_1} {α : Type u_2} {M : ι → Matroid α} {B : ι → Set α} (h : Pairwise (Function.onFun Disjoint fun (i : ι) => (M i).E)) (hB : ∀ (i : ι), (M i).IsBase (B i)) : (Matroid.disjointSigma M h).IsBase (⋃ (i : ι), B i)

theorem Matroid.IsBasis.disjointSigma_iUnion {ι : Type u_1} {α : Type u_2} {M : ι → Matroid α} {I X : ι → Set α} (h : Pairwise (Function.onFun Disjoint fun (i : ι) => (M i).E)) (hI : ∀ (i : ι), (M i).IsBasis (I i) (X i)) : (Matroid.disjointSigma M h).IsBasis (⋃ (i : ι), I i) (⋃ (i : ι), X i)

theorem Matroid.isRestriction_disjointSigma {ι : Type u_1} {α : Type u_2} {M : ι → Matroid α} (h : Pairwise (Function.onFun Disjoint fun (i : ι) => (M i).E)) (i : ι) : (M i).IsRestriction (Matroid.disjointSigma M h)

theorem Matroid.disjointSigma_closure {ι : Type u_1} {α : Type u_2} {M : ι → Matroid α} (h : Pairwise (Function.onFun Disjoint fun (i : ι) => (M i).E)) (X : Set α) : (Matroid.disjointSigma M h).closure X = ⋃ (i : ι), (M i).closure (X ∩ (M i).E)

theorem Matroid.disjointSigma_spanning_iff {ι : Type u_1} {α : Type u_2} {M : ι → Matroid α} (h : Pairwise (Function.onFun Disjoint fun (i : ι) => (M i).E)) (X : Set α) : (Matroid.disjointSigma M h).Spanning X ↔ (∀ (i : ι), (M i).Spanning (X ∩ (M i).E)) ∧ X ⊆ ⋃ (i : ι), (M i).E

theorem Matroid.disjointSigma_restrict {ι : Type u_1} {α : Type u_2} {M : ι → Matroid α} (hdj : Pairwise (Function.onFun Disjoint fun (i : ι) => (M i).E)) (R : Set α) (hR : R ⊆ ⋃ (i : ι), (M i).E) : (Matroid.disjointSigma M hdj).restrict R = Matroid.disjointSigma (fun (i : ι) => (M i).restrict (R ∩ (M i).E)) ⋯

theorem Matroid.disjointSigma_restrict_iUnion {ι : Type u_1} {α : Type u_2} {M : ι → Matroid α} (hdj : Pairwise (Function.onFun Disjoint fun (i : ι) => (M i).E)) (R : ι → Set α) (hR : ∀ (i : ι), R i ⊆ (M i).E) : (Matroid.disjointSigma M hdj).restrict (⋃ (i : ι), R i) = Matroid.disjointSigma (fun (i : ι) => (M i).restrict (R i)) ⋯

@[simp]

theorem Matroid.disjointSigma_dual {ι : Type u_1} {α : Type u_2} (M : ι → Matroid α) (hdj : Pairwise (Function.onFun Disjoint fun (i : ι) => (M i).E)) : (Matroid.disjointSigma M hdj)✶ = Matroid.disjointSigma (fun (i : ι) => (M i)✶) hdj

theorem Matroid.Indep.disjointSum_indep_union {α : Type u_1} {M N : Matroid α} {I J : Set α} {h : Disjoint M.E N.E} (hI : M.Indep I) (hJ : N.Indep J) : (M.disjointSum N h).Indep (I ∪ J)

theorem Matroid.IsBase.disjointSum_isBase_union {α : Type u_1} {M N : Matroid α} {B B' : Set α} {h : Disjoint M.E N.E} (hB : M.IsBase B) (hB' : N.IsBase B') : (M.disjointSum N h).IsBase (B ∪ B')

theorem Matroid.IsBasis.disjointSum_isBasis_union {α : Type u_1} {I J X Y : Set α} {M N : Matroid α} (hIX : M.IsBasis I X) (hJY : N.IsBasis J Y) (h : Disjoint M.E N.E) : (M.disjointSum N h).IsBasis (I ∪ J) (X ∪ Y)

theorem Matroid.disjointSum_eq_disjointSigma {α : Type u_1} (M N : Matroid α) (hMN : Disjoint M.E N.E) : M.disjointSum N hMN = Matroid.disjointSigma (fun (b : Bool) => bif b then M else N) ⋯

@[simp]

theorem Matroid.disjointSum_dual {α : Type u_1} (M N : Matroid α) (hMN : Disjoint M.E N.E) : (M.disjointSum N hMN)✶ = M✶.disjointSum N✶ hMN

theorem Matroid.isRestriction_disjointSum_left {α : Type u_1} {M N : Matroid α} (hMN : Disjoint M.E N.E) : M.IsRestriction (M.disjointSum N hMN)

theorem Matroid.isRestriction_disjointSum_right {α : Type u_1} {M N : Matroid α} (hMN : Disjoint M.E N.E) : N.IsRestriction (M.disjointSum N hMN)

@[simp]

theorem Matroid.disjointSum_restrict_left {α : Type u_1} {M N : Matroid α} (hMN : Disjoint M.E N.E) : (M.disjointSum N hMN).restrict M.E = M

@[simp]

theorem Matroid.disjointSum_restrict_right {α : Type u_1} {M N : Matroid α} (hMN : Disjoint M.E N.E) : (M.disjointSum N hMN).restrict N.E = N

@[simp]

theorem Matroid.emptyOn_disjointSum {α : Type u_1} {M : Matroid α} : (emptyOn α).disjointSum M ⋯ = M

@[simp]

theorem Matroid.disjointSum_emptyOn {α : Type u_1} {M : Matroid α} : M.disjointSum (emptyOn α) ⋯ = M

instance Matroid.disjointSum_nonempty_left {α : Type u_1} {M N : Matroid α} [M.Nonempty] (hMN : Disjoint M.E N.E) : (M.disjointSum N hMN).Nonempty

instance Matroid.disjointSum_nonempty_right {α : Type u_1} {M N : Matroid α} [N.Nonempty] (hMN : Disjoint M.E N.E) : (M.disjointSum N hMN).Nonempty

instance Matroid.disjointSum_rankPos_left {α : Type u_1} {M N : Matroid α} [M.RankPos] (hMN : Disjoint M.E N.E) : (M.disjointSum N hMN).RankPos

instance Matroid.disjointSum_rankPos_right {α : Type u_1} {M N : Matroid α} [N.RankPos] (hMN : Disjoint M.E N.E) : (M.disjointSum N hMN).RankPos

instance Matroid.disjointSum_dual_rankPos_left {α : Type u_1} {M N : Matroid α} [M✶.RankPos] (hMN : Disjoint M.E N.E) : (M.disjointSum N hMN)✶.RankPos

instance Matroid.disjointSum_dual_rankPos_right {α : Type u_1} {M N : Matroid α} [N✶.RankPos] (hMN : Disjoint M.E N.E) : (M.disjointSum N hMN)✶.RankPos

theorem Matroid.disjointSum_closure_eq {α : Type u_1} {M N : Matroid α} (hMN : Disjoint M.E N.E) (X : Set α) : (M.disjointSum N hMN).closure X = M.closure (X ∩ M.E) ∪ N.closure (X ∩ N.E)

theorem Matroid.disjointSum_spanning_iff {α : Type u_1} {M N : Matroid α} (hMN : Disjoint M.E N.E) {X : Set α} : (M.disjointSum N hMN).Spanning X ↔ M.Spanning (X ∩ M.E) ∧ N.Spanning (X ∩ N.E) ∧ X ⊆ M.E ∪ N.E

theorem Matroid.disjointSum_dep_iff {α : Type u_1} {M N : Matroid α} (hMN : Disjoint M.E N.E) {X : Set α} : (M.disjointSum N hMN).Dep X ↔ (M.Dep (X ∩ M.E) ∨ N.Dep (X ∩ N.E)) ∧ X ⊆ M.E ∪ N.E

theorem Matroid.disjointSum_loopyOn {α : Type u_1} {M : Matroid α} {E : Set α} (hMN : Disjoint M.E E) : M.disjointSum (loopyOn E) hMN = M.restrict (M.E ∪ E)

@[simp]

theorem Matroid.freeOn_disjointSum_freeOn {α : Type u_1} {E E' : Set α} (hdj : Disjoint E E') : (freeOn E).disjointSum (freeOn E') hdj = freeOn (E ∪ E')

@[simp]

theorem Matroid.loopyOn_disjointSum_loopyOn {α : Type u_1} {E E' : Set α} (hdj : Disjoint E E') : (loopyOn E).disjointSum (loopyOn E') hdj = loopyOn (E ∪ E')

theorem Matroid.restrict_superset_ground_eq_disjointSum {α : Type u_1} {M : Matroid α} {X : Set α} (hE : M.E ⊆ X) : M.restrict X = M.disjointSum (loopyOn (X \ M.E)) ⋯

theorem Matroid.disjointSum_assoc {α : Type u_1} {M₁ M₂ M₃ : Matroid α} (h₁₂ : Disjoint M₁.E M₂.E) (h₁₃ : Disjoint (M₁.disjointSum M₂ h₁₂).E M₃.E) : (M₁.disjointSum M₂ h₁₂).disjointSum M₃ h₁₃ = M₁.disjointSum (M₂.disjointSum M₃ ⋯) ⋯

theorem Matroid.disjointSum_restrict_union {α : Type u_1} {M N : Matroid α} {S T : Set α} (hdj : Disjoint M.E N.E) (hS : S ⊆ M.E) (hT : T ⊆ N.E) : (M.disjointSum N hdj).restrict (S ∪ T) = (M.restrict S).disjointSum (N.restrict T) ⋯

theorem Matroid.disjointSum_encard_ground {α : Type u_1} {M N : Matroid α} (hdj : Disjoint M.E N.E) : (M.disjointSum N hdj).E.encard = M.E.encard + N.E.encard

theorem Matroid.sum_eq_disjointSum {α : Type u_1} {β : Type u_2} (M : Matroid α) (N : Matroid β) : M.sum N = (M.map Sum.inl ⋯).disjointSum (N.map Sum.inr ⋯) ⋯

@[simp]

theorem Matroid.sum_dual {α : Type u_1} {β : Type u_2} (M : Matroid α) (N : Matroid β) : (M.sum N)✶ = M✶.sum N✶

theorem Matroid.sum_dep_iff {α : Type u_1} {β : Type u_2} (M : Matroid α) (N : Matroid β) (X : Set (α ⊕ β)) : (M.sum N).Dep X ↔ (M.Dep (Sum.inl ⁻¹' X) ∨ N.Dep (Sum.inr ⁻¹' X)) ∧ Sum.inl ⁻¹' X ⊆ M.E ∧ Sum.inr ⁻¹' X ⊆ N.E

theorem Matroid.sum_closure_eq {α : Type u_1} {β : Type u_2} (M : Matroid α) (N : Matroid β) (X : Set (α ⊕ β)) : (M.sum N).closure X = Sum.inl '' M.closure (Sum.inl ⁻¹' X) ∪ Sum.inr '' N.closure (Sum.inr ⁻¹' X)

@[simp]

theorem Matroid.inl_mem_sum_closure_iff {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} {e : α} {X : Set (α ⊕ β)} : Sum.inl e ∈ (M.sum N).closure X ↔ e ∈ M.closure (Sum.inl ⁻¹' X)

@[simp]

theorem Matroid.inr_mem_sum_closure_iff {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} {e : β} {X : Set (α ⊕ β)} : Sum.inr e ∈ (M.sum N).closure X ↔ e ∈ N.closure (Sum.inr ⁻¹' X)