awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
h : X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun (I : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk (β := α) i ⁻¹' X) ∧ Sigma.mk (β := α) i ⁻¹' I ⊆ Js i
S : Set ((i : ι) × α i)
hS : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' S)
hSX : S ⊆ X
hJS : Set.sigma (α := α) univ Js ⊆ S
⊢ (Set.sigma (α := fun (i : ι) ↦ α i) univ fun (i : ι) ↦ Sigma.mk (β := fun (i : ι) ↦ α i) i ⁻¹' S) ⊆
    Set.sigma (α := α) univ Js

Tactic:
sigma_mono rfl.subset fun i ↦ ?_

Premises used: Eq.subset, Set.sigma_mono, rfl
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
h_1 : X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun (I : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk (β := α) i ⁻¹' X) ∧ Sigma.mk (β := α) i ⁻¹' I ⊆ Js i
S : Set ((i : ι) × α i)
hS : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' S)
hSX : S ⊆ X
hJS : Set.sigma (α := α) univ Js ⊆ S
h : ∀ (i : ι), Sigma.mk (β := fun (i : ι) ↦ α i) i ⁻¹' S ⊆ Js i
⊢ (Set.sigma (α := fun (i : ι) ↦ α i) univ fun (i : ι) ↦ Sigma.mk (β := fun (i : ι) ↦ α i) i ⁻¹' S) ⊆
    Set.sigma (α := α) univ Js

Tactic:
refine sigma_mono rfl.subset fun i ↦ ?_

Premises used: Eq.subset, Set.sigma_mono, rfl
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
h_1 : X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun (I : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk (β := α) i ⁻¹' X) ∧ Sigma.mk (β := α) i ⁻¹' I ⊆ Js i
S : Set ((i : ι) × α i)
hS : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' S)
hSX : S ⊆ X
hJS : Set.sigma (α := α) univ Js ⊆ S
i : ι
h :
  ∀
    (hJS :
      ∀ ⦃i : ι⦄, Membership.mem (γ := Set ι) univ i → ∀ ⦃a : α i⦄, a ∈ Js i → Sigma.mk (β := fun (i : ι) ↦ α i) i a ∈ S)
    (i : ι), Sigma.mk (β := fun (i : ι) ↦ α i) i ⁻¹' S ⊆ Js i
⊢ Sigma.mk (β := fun (i : ι) ↦ α i) i ⁻¹' S ⊆ Js i

Tactic:
rw [sigma_subset_iff] at hJS

Premises used: Set.sigma_subset_iff
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
h_1 : X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun (I : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk (β := α) i ⁻¹' X) ∧ Sigma.mk (β := α) i ⁻¹' I ⊆ Js i
S : Set ((i : ι) × α i)
hS : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' S)
hSX : S ⊆ X
hJS : ∀ ⦃i : ι⦄, Membership.mem (γ := Set ι) univ i → ∀ ⦃a : α i⦄, a ∈ Js i → Sigma.mk (β := fun (i : ι) ↦ α i) i a ∈ S
i : ι
h : Sigma.mk (β := α) i ⁻¹' S ⊆ Sigma.mk (β := α) i ⁻¹' X
⊢ Sigma.mk (β := fun (i : ι) ↦ α i) i ⁻¹' S ⊆ Js i

Tactic:
rw [(hJs i).1.eq_of_subset_indep (hS i) (hJS <| mem_univ i)]

Premises used: Matroid.IsBasis'.eq_of_subset_indep, And.left, Set.mem_univ
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
h : X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun (I : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk (β := α) i ⁻¹' X) ∧ Sigma.mk (β := α) i ⁻¹' I ⊆ Js i
S : Set ((i : ι) × α i)
hS : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' S)
hSX : S ⊆ X
hJS : ∀ ⦃i : ι⦄, Membership.mem (γ := Set ι) univ i → ∀ ⦃a : α i⦄, a ∈ Js i → Sigma.mk (β := fun (i : ι) ↦ α i) i a ∈ S
i : ι
⊢ Sigma.mk (β := α) i ⁻¹' S ⊆ Sigma.mk (β := α) i ⁻¹' X

Tactic:
preimage_mono hSX

Premises used: Set.preimage_mono
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
h : X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun (I : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk (β := α) i ⁻¹' X) ∧ Sigma.mk (β := α) i ⁻¹' I ⊆ Js i
S : Set ((i : ι) × α i)
hS : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' S)
hSX : S ⊆ X
hJS : ∀ ⦃i : ι⦄, Membership.mem (γ := Set ι) univ i → ∀ ⦃a : α i⦄, a ∈ Js i → Sigma.mk (β := fun (i : ι) ↦ α i) i a ∈ S
i : ι
⊢ Sigma.mk (β := α) i ⁻¹' S ⊆ Sigma.mk (β := α) i ⁻¹' X

Tactic:
exact preimage_mono hSX

Premises used: Set.preimage_mono
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
B : Set ((i : ι) × α i)
hB : ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)
rw :
  Subset (α := Set ((i : ι) × α i))
    (Set.sigma (α := fun (i : ι) ↦ α i) univ fun (i : ι) ↦ Sigma.mk (β := fun (i : ι) ↦ α i) i ⁻¹' B)
    (Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E)
⊢ B ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E

Tactic:
rw [← univ_sigma_preimage_mk B]

Premises used: Set.univ_sigma_preimage_mk
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
B : Set ((i : ι) × α i)
hB : ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)
⊢ Subset (α := Set ((i : ι) × α i))
    (Set.sigma (α := fun (i : ι) ↦ α i) univ fun (i : ι) ↦ Sigma.mk (β := fun (i : ι) ↦ α i) i ⁻¹' B)
    (Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E)

Tactic:
apply sigma_mono Subset.rfl fun i ↦ (hB i).subset_ground

Premises used: Matroid.IsBase.subset_ground, Set.Subset.rfl, Set.sigma_mono
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I : Set ((i : ι) × α i)
⊢ (Matroid.sigma (α := α) M).Indep I ↔ ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
B : Set ((i : ι) × α i)
⊢ (Matroid.sigma (α := α) M).IsBase B ↔ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
⊢ (Matroid.sigma (α := α) M).E = Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E

Tactic:
rfl

Premises used: setOf, Set.sigma, rfl
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
simp :
  (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)) →
    ((I ⊆ X ∧
        (∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t) ∧
          X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E) ↔
      (∀ (x : ι), Sigma.mk (β := α) x ⁻¹' I ⊆ Sigma.mk (β := α) x ⁻¹' X) ∧
        (∀ (x : ι) ⦃t : Set (α x)⦄,
            (M x).Indep t →
              t ⊆ Sigma.mk (β := α) x ⁻¹' X → Sigma.mk (β := α) x ⁻¹' I ⊆ t → Sigma.mk (β := α) x ⁻¹' I = t) ∧
          ∀ (x : ι), Sigma.mk (β := α) x ⁻¹' X ⊆ (M x).E)
⊢ (Matroid.sigma (α := α) M).IsBasis I X ↔
    ∀ (i : ι), (M i).IsBasis (Sigma.mk (β := α) i ⁻¹' I) (Sigma.mk (β := α) i ⁻¹' X)

Tactic:
simp only [IsBasis, sigma_indep_iff, maximal_subset_iff, and_imp, and_assoc, sigma_ground_eq,
    forall_and, and_congr_right_iff]

Premises used: and_imp, Matroid.sigma_ground_eq, and_congr_right_iff, maximal_subset_iff, and_assoc, Matroid.sigma_indep_iff, Matroid.IsBasis, forall_and
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
⊢ (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)) →
    ((I ⊆ X ∧
        (∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t) ∧
          X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E) ↔
      (∀ (x : ι), Sigma.mk (β := α) x ⁻¹' I ⊆ Sigma.mk (β := α) x ⁻¹' X) ∧
        (∀ (x : ι) ⦃t : Set (α x)⦄,
            (M x).Indep t →
              t ⊆ Sigma.mk (β := α) x ⁻¹' X → Sigma.mk (β := α) x ⁻¹' I ⊆ t → Sigma.mk (β := α) x ⁻¹' I = t) ∧
          ∀ (x : ι), Sigma.mk (β := α) x ⁻¹' X ⊆ (M x).E)

Tactic:
fun hI ↦ ⟨fun ⟨hIX, h, h'⟩ ↦ ⟨fun i ↦ preimage_mono hIX, fun i I₀ hI₀ hI₀X hII₀ ↦ ?_, ?_⟩,
    fun ⟨hIX, h', h''⟩ ↦ ⟨?_, ?_, ?_⟩⟩

Premises used: Matroid.E, Set.univ, _private.0.Matroid.sigma_isBasis_iff.match_5, _private.0.Matroid.sigma_isBasis_iff.match_4, HasSubset.Subset, And, Set.preimage_mono, Set.sigma, And.intro, Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)
h_1 :
  I ⊆ X ∧
    (∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t) ∧
      X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
hIX : I ⊆ X
h : ∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t
h' : X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
i : ι
I₀ : Set (α i)
hI₀ : (M i).Indep I₀
hI₀X : I₀ ⊆ Sigma.mk (β := α) i ⁻¹' X
hII₀ : Sigma.mk (β := α) i ⁻¹' I ⊆ I₀
⊢ Sigma.mk (β := α) i ⁻¹' I = I₀

Tactic:
hII₀.antisymm ?_

Premises used: HasSubset.Subset.antisymm
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)
h_1 :
  I ⊆ X ∧
    (∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t) ∧
      X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
hIX : I ⊆ X
h : ∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t
h' : X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
i : ι
I₀ : Set (α i)
hI₀ : (M i).Indep I₀
hI₀X : I₀ ⊆ Sigma.mk (β := α) i ⁻¹' X
hII₀ : Sigma.mk (β := α) i ⁻¹' I ⊆ I₀
refine_1 : I₀ ⊆ Sigma.mk (β := α) i ⁻¹' I
⊢ Sigma.mk (β := α) i ⁻¹' I = I₀

Tactic:
refine hII₀.antisymm ?_

Premises used: HasSubset.Subset.antisymm
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)
h_1 :
  I ⊆ X ∧
    (∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t) ∧
      X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
hIX : I ⊆ X
h : ∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t
h' : X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
i : ι
I₀ : Set (α i)
hI₀ : (M i).Indep I₀
hI₀X : I₀ ⊆ Sigma.mk (β := α) i ⁻¹' X
hII₀ : Sigma.mk (β := α) i ⁻¹' I ⊆ I₀
⊢ (∀ (i_1 : ι), (M i_1).Indep (Sigma.mk (β := α) i_1 ⁻¹' (I ∪ Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀))) →
    I ∪ Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀ ⊆ X →
      I ⊆ I ∪ Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀ → I = I ∪ Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀

Tactic:
specialize h (t := I ∪ Sigma.mk i '' I₀)
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)
h_1 :
  I ⊆ X ∧
    (∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t) ∧
      X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
hIX : I ⊆ X
h' : X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
i : ι
I₀ : Set (α i)
hI₀ : (M i).Indep I₀
hI₀X : I₀ ⊆ Sigma.mk (β := α) i ⁻¹' X
hII₀ : Sigma.mk (β := α) i ⁻¹' I ⊆ I₀
h :
  (∀ (i_1 : ι), (M i_1).Indep (Sigma.mk (β := α) i_1 ⁻¹' (I ∪ Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀))) →
    I ∪ Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀ ⊆ X →
      I ⊆ I ∪ Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀ → I = I ∪ Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀
⊢ (∀ (i_1 : ι),
      (M i_1).Indep
        (Sigma.mk (β := α) i_1 ⁻¹' I ∪ Sigma.mk (β := α) i_1 ⁻¹' Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀)) →
    I = I ∪ Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀

Tactic:
simp only [preimage_union, union_subset_iff, hIX, image_subset_iff, hI₀X, and_self,
      subset_union_left, true_implies] at h

Premises used: and_self, Set.union_subset_iff, Set.preimage_union, Set.subset_union_left, true_implies, Set.image_subset_iff
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)
h_1 :
  I ⊆ X ∧
    (∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t) ∧
      X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
hIX : I ⊆ X
h' : X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
i : ι
I₀ : Set (α i)
hI₀ : (M i).Indep I₀
hI₀X : I₀ ⊆ Sigma.mk (β := α) i ⁻¹' X
hII₀ : Sigma.mk (β := α) i ⁻¹' I ⊆ I₀
h :
  (∀ (i_1 : ι),
      (M i_1).Indep
        (Sigma.mk (β := α) i_1 ⁻¹' I ∪ Sigma.mk (β := α) i_1 ⁻¹' Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀)) →
    I = I ∪ Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀
refine_1 : I₀ ⊆ Sigma.mk (β := α) i ⁻¹' I ∪ I₀
refine_1₁ :
  ∀ (i_1 : ι),
    (M i_1).Indep (Sigma.mk (β := α) i_1 ⁻¹' I ∪ Sigma.mk (β := α) i_1 ⁻¹' Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀)
⊢ I₀ ⊆ Sigma.mk (β := α) i ⁻¹' I

Tactic:
rw [h, preimage_union, sigma_mk_preimage_image_eq_self]

Premises used: Set.preimage_union, sigma_mk_preimage_image_eq_self
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)
h_1 :
  I ⊆ X ∧
    (∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t) ∧
      X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
hIX : I ⊆ X
h' : X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
i : ι
I₀ : Set (α i)
hI₀ : (M i).Indep I₀
hI₀X : I₀ ⊆ Sigma.mk (β := α) i ⁻¹' X
hII₀ : Sigma.mk (β := α) i ⁻¹' I ⊆ I₀
h :
  (∀ (i_1 : ι),
      (M i_1).Indep
        (Sigma.mk (β := α) i_1 ⁻¹' I ∪ Sigma.mk (β := α) i_1 ⁻¹' Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀)) →
    I = I ∪ Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀
⊢ I₀ ⊆ Sigma.mk (β := α) i ⁻¹' I ∪ I₀

Tactic:
subset_union_right

Premises used: Set.subset_union_right
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)
h_1 :
  I ⊆ X ∧
    (∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t) ∧
      X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
hIX : I ⊆ X
h' : X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
i : ι
I₀ : Set (α i)
hI₀ : (M i).Indep I₀
hI₀X : I₀ ⊆ Sigma.mk (β := α) i ⁻¹' X
hII₀ : Sigma.mk (β := α) i ⁻¹' I ⊆ I₀
h :
  (∀ (i_1 : ι),
      (M i_1).Indep
        (Sigma.mk (β := α) i_1 ⁻¹' I ∪ Sigma.mk (β := α) i_1 ⁻¹' Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀)) →
    I = I ∪ Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀
⊢ I₀ ⊆ Sigma.mk (β := α) i ⁻¹' I ∪ I₀

Tactic:
exact subset_union_right

Premises used: Set.subset_union_right
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)
h_1 :
  I ⊆ X ∧
    (∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t) ∧
      X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
hIX : I ⊆ X
h' : X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
i : ι
I₀ : Set (α i)
hI₀ : (M i).Indep I₀
hI₀X : I₀ ⊆ Sigma.mk (β := α) i ⁻¹' X
hII₀ : Sigma.mk (β := α) i ⁻¹' I ⊆ I₀
h :
  (∀ (i_1 : ι),
      (M i_1).Indep
        (Sigma.mk (β := α) i_1 ⁻¹' I ∪ Sigma.mk (β := α) i_1 ⁻¹' Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀)) →
    I = I ∪ Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀
j : ι
refine_1 : (M i).Indep (Sigma.mk (β := α) i ⁻¹' I ∪ Sigma.mk (β := α) i ⁻¹' Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀)
refine_1₁ :
  ∀ (hij : i ≠ j),
    (M j).Indep (Sigma.mk (β := α) j ⁻¹' I ∪ Sigma.mk (β := α) j ⁻¹' Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀)
⊢ (M j).Indep (Sigma.mk (β := α) j ⁻¹' I ∪ Sigma.mk (β := α) j ⁻¹' Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀)

Tactic:
obtain (rfl | hij) := eq_or_ne i j

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)
h_1 :
  I ⊆ X ∧
    (∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t) ∧
      X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
hIX : I ⊆ X
h' : X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
i : ι
I₀ : Set (α i)
hI₀ : (M i).Indep I₀
hI₀X : I₀ ⊆ Sigma.mk (β := α) i ⁻¹' X
hII₀ : Sigma.mk (β := α) i ⁻¹' I ⊆ I₀
h :
  (∀ (i_1 : ι),
      (M i_1).Indep
        (Sigma.mk (β := α) i_1 ⁻¹' I ∪ Sigma.mk (β := α) i_1 ⁻¹' Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀)) →
    I = I ∪ Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀
refine_1 : (M i).Indep (Sigma.mk (β := α) i ⁻¹' I ∪ I₀)
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : (M i).Indep I₀
⊢ (M i).Indep (Sigma.mk (β := α) i ⁻¹' I ∪ Sigma.mk (β := α) i ⁻¹' Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀)

Tactic:
rwa [sigma_mk_preimage_image_eq_self, union_eq_self_of_subset_left hII₀]

Premises used: Set.union_eq_self_of_subset_left, sigma_mk_preimage_image_eq_self
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)
h_1 :
  I ⊆ X ∧
    (∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t) ∧
      X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
hIX : I ⊆ X
h' : X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
i : ι
I₀ : Set (α i)
hI₀ : (M i).Indep I₀
hI₀X : I₀ ⊆ Sigma.mk (β := α) i ⁻¹' X
hII₀ : Sigma.mk (β := α) i ⁻¹' I ⊆ I₀
h :
  (∀ (i_1 : ι),
      (M i_1).Indep
        (Sigma.mk (β := α) i_1 ⁻¹' I ∪ Sigma.mk (β := α) i_1 ⁻¹' Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀)) →
    I = I ∪ Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀
j : ι
hij : i ≠ j
refine_1 : (M j).Indep (Sigma.mk (β := α) j ⁻¹' I)
⊢ (M j).Indep (Sigma.mk (β := α) j ⁻¹' I ∪ Sigma.mk (β := α) j ⁻¹' Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀)

Tactic:
rw [sigma_mk_preimage_image' hij, union_empty]

Premises used: Set.union_empty, sigma_mk_preimage_image'
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)
h_1 :
  I ⊆ X ∧
    (∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t) ∧
      X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
hIX : I ⊆ X
h' : X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
i : ι
I₀ : Set (α i)
hI₀ : (M i).Indep I₀
hI₀X : I₀ ⊆ Sigma.mk (β := α) i ⁻¹' X
hII₀ : Sigma.mk (β := α) i ⁻¹' I ⊆ I₀
h :
  (∀ (i_1 : ι),
      (M i_1).Indep
        (Sigma.mk (β := α) i_1 ⁻¹' I ∪ Sigma.mk (β := α) i_1 ⁻¹' Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀)) →
    I = I ∪ Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀
j : ι
hij : i ≠ j
⊢ (M j).Indep (Sigma.mk (β := α) j ⁻¹' I)

Tactic:
apply hI
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)
h_1 :
  I ⊆ X ∧
    (∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t) ∧
      X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
hIX : I ⊆ X
h : ∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t
h' : X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
i : ι
⊢ Sigma.mk (β := α) i ⁻¹' X ⊆ (M i).E

Tactic:
simpa using preimage_mono (f := Sigma.mk i) h'

Premises used: Set.preimage_mono
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)
h_1 :
  I ⊆ X ∧
    (∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t) ∧
      X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
hIX : I ⊆ X
h : ∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t
h' : X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
⊢ ∀ (x : ι), Sigma.mk (β := α) x ⁻¹' X ⊆ (M x).E

Tactic:
exact fun i ↦ by simpa using preimage_mono (f := Sigma.mk i) h'
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)
h :
  (∀ (x : ι), Sigma.mk (β := α) x ⁻¹' I ⊆ Sigma.mk (β := α) x ⁻¹' X) ∧
    (∀ (x : ι) ⦃t : Set (α x)⦄,
        (M x).Indep t → t ⊆ Sigma.mk (β := α) x ⁻¹' X → Sigma.mk (β := α) x ⁻¹' I ⊆ t → Sigma.mk (β := α) x ⁻¹' I = t) ∧
      ∀ (x : ι), Sigma.mk (β := α) x ⁻¹' X ⊆ (M x).E
hIX : ∀ (x : ι), Sigma.mk (β := α) x ⁻¹' I ⊆ Sigma.mk (β := α) x ⁻¹' X
h' :
  ∀ (x : ι) ⦃t : Set (α x)⦄,
    (M x).Indep t → t ⊆ Sigma.mk (β := α) x ⁻¹' X → Sigma.mk (β := α) x ⁻¹' I ⊆ t → Sigma.mk (β := α) x ⁻¹' I = t
h'' : ∀ (x : ι), Sigma.mk (β := α) x ⁻¹' X ⊆ (M x).E
x_1 : (i : ι) × α i
i : ι
x : α i
hx : Sigma.mk (β := fun (i : ι) ↦ α i) i x ∈ I
⊢ Sigma.mk (β := fun (i : ι) ↦ α i) i x ∈ X

Tactic:
simpa using hIX i hx
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)
h :
  (∀ (x : ι), Sigma.mk (β := α) x ⁻¹' I ⊆ Sigma.mk (β := α) x ⁻¹' X) ∧
    (∀ (x : ι) ⦃t : Set (α x)⦄,
        (M x).Indep t → t ⊆ Sigma.mk (β := α) x ⁻¹' X → Sigma.mk (β := α) x ⁻¹' I ⊆ t → Sigma.mk (β := α) x ⁻¹' I = t) ∧
      ∀ (x : ι), Sigma.mk (β := α) x ⁻¹' X ⊆ (M x).E
hIX : ∀ (x : ι), Sigma.mk (β := α) x ⁻¹' I ⊆ Sigma.mk (β := α) x ⁻¹' X
h' :
  ∀ (x : ι) ⦃t : Set (α x)⦄,
    (M x).Indep t → t ⊆ Sigma.mk (β := α) x ⁻¹' X → Sigma.mk (β := α) x ⁻¹' I ⊆ t → Sigma.mk (β := α) x ⁻¹' I = t
h'' : ∀ (x : ι), Sigma.mk (β := α) x ⁻¹' X ⊆ (M x).E
⊢ I ⊆ X

Tactic:
exact fun ⟨i, x⟩ hx ↦ by simpa using hIX i hx
-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)
h :
  (∀ (x : ι), Sigma.mk (β := α) x ⁻¹' I ⊆ Sigma.mk (β := α) x ⁻¹' X) ∧
    (∀ (x : ι) ⦃t : Set (α x)⦄,
        (M x).Indep t → t ⊆ Sigma.mk (β := α) x ⁻¹' X → Sigma.mk (β := α) x ⁻¹' I ⊆ t → Sigma.mk (β := α) x ⁻¹' I = t) ∧
      ∀ (x : ι), Sigma.mk (β := α) x ⁻¹' X ⊆ (M x).E
hIX : ∀ (x : ι), Sigma.mk (β := α) x ⁻¹' I ⊆ Sigma.mk (β := α) x ⁻¹' X
h' :
  ∀ (x : ι) ⦃t : Set (α x)⦄,
    (M x).Indep t → t ⊆ Sigma.mk (β := α) x ⁻¹' X → Sigma.mk (β := α) x ⁻¹' I ⊆ t → Sigma.mk (β := α) x ⁻¹' I = t
h'' : ∀ (x : ι), Sigma.mk (β := α) x ⁻¹' X ⊆ (M x).E
⊢ ∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t

Tactic:
fun J hJ hJX hIJ ↦ hIJ.antisymm fun ⟨i,x⟩ hx ↦ ?_

Premises used: _private.0.Matroid.sigma_isBasis_iff.match_7, Membership.mem, HasSubset.Subset.antisymm