awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
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
have h : ∀ (i : ι), Sigma.mk (β := fun (i : ι) ↦ α i) i ⁻¹' S ⊆ Js i
Tactic: refine sigma_mono rfl.subset fun i ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
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
i : ι
⊢ Sigma.mk (β := fun (i : ι) ↦ α i) i ⁻¹' S ⊆ Js i
have 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
Tactic: rw [sigma_subset_iff] at hJS
Cleared hypotheses: hJS, i
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
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 (β := fun (i : ι) ↦ α i) i ⁻¹' S ⊆ Js i
have h : Sigma.mk (β := α) i ⁻¹' S ⊆ Sigma.mk (β := α) i ⁻¹' X
Tactic: rw [(hJs i).1.eq_of_subset_indep (hS i) (hJS <| mem_univ i)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
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)
⊢ B ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
have 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)
Tactic: rw [← univ_sigma_preimage_mk B]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
ι : 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)
have 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)
Tactic: simp only [IsBasis, sigma_indep_iff, maximal_subset_iff, and_imp, and_assoc, sigma_ground_eq,
    forall_and, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
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)
have refine_1 : ∀ (hI : ∀ (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) →
    ∀ (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: refine fun hI ↦ ⟨fun ⟨hIX, h, h'⟩ ↦ ⟨fun i ↦ preimage_mono hIX, fun i I₀ hI₀ hI₀X hII₀ ↦ ?_, ?_⟩,
    fun ⟨hIX, h', h''⟩ ↦ ⟨?_, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
refine_1 :
  ∀ (hI : ∀ (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) →
      ∀ (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₀
⊢ (∀ (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)
have refine_2 : ∀ (hI : ∀ (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) →
    ∀ (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: refine fun hI ↦ ⟨fun ⟨hIX, h, h'⟩ ↦ ⟨fun i ↦ preimage_mono hIX, fun i I₀ hI₀ hI₀X hII₀ ↦ ?_, ?_⟩,
    fun ⟨hIX, h', h''⟩ ↦ ⟨?_, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
refine_1 :
  ∀ (hI : ∀ (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) →
      ∀ (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₀
refine_2 :
  ∀ (hI : ∀ (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) →
      ∀ (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
⊢ (∀ (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)
have refine_3 : ∀ (hI : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)),
  ((∀ (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: refine fun hI ↦ ⟨fun ⟨hIX, h, h'⟩ ↦ ⟨fun i ↦ preimage_mono hIX, fun i I₀ hI₀ hI₀X hII₀ ↦ ?_, ?_⟩,
    fun ⟨hIX, h', h''⟩ ↦ ⟨?_, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
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₀
have refine_1 : I₀ ⊆ Sigma.mk (β := α) i ⁻¹' I
Tactic: refine hII₀.antisymm ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (hypothesis)
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₀ ⊆ Sigma.mk (β := α) i ⁻¹' I
have 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₀
Tactic: specialize h (t := I ∪ Sigma.mk i '' I₀)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (hypothesis)
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₀ ⊆ Sigma.mk (β := α) i ⁻¹' I
have 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₀
Tactic: simp only [preimage_union, union_subset_iff, hIX, image_subset_iff, hI₀X, and_self,
      subset_union_left, true_implies] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
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
have refine_1 : I₀ ⊆ Sigma.mk (β := α) i ⁻¹' I ∪ I₀
Tactic: rw [h, preimage_union, sigma_mk_preimage_image_eq_self]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
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₀
⊢ I₀ ⊆ Sigma.mk (β := α) i ⁻¹' I
have refine_1₁ : ∀ (i_1 : ι),
  (M i_1).Indep (Sigma.mk (β := α) i_1 ⁻¹' I ∪ Sigma.mk (β := α) i_1 ⁻¹' Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀)
Tactic: rw [h, preimage_union, sigma_mk_preimage_image_eq_self]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
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 : ι
⊢ (M j).Indep (Sigma.mk (β := α) j ⁻¹' I ∪ Sigma.mk (β := α) j ⁻¹' Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀)
have refine_1 : (M i).Indep (Sigma.mk (β := α) i ⁻¹' I ∪ Sigma.mk (β := α) i ⁻¹' Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀)
Tactic: obtain (rfl | hij) := eq_or_ne i j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
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₀)
⊢ (M j).Indep (Sigma.mk (β := α) j ⁻¹' I ∪ Sigma.mk (β := α) j ⁻¹' Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀)
have refine_1₁ : ∀ (hij : i ≠ j),
  (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
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
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₀
⊢ (M i).Indep (Sigma.mk (β := α) i ⁻¹' I ∪ Sigma.mk (β := α) i ⁻¹' Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀)
have refine_1 : (M i).Indep (Sigma.mk (β := α) i ⁻¹' I ∪ I₀)
Tactic: rwa [sigma_mk_preimage_image_eq_self, union_eq_self_of_subset_left hII₀]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
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 ∪ Sigma.mk (β := α) j ⁻¹' Sigma.mk (β := fun (i : ι) ↦ α i) i '' I₀)
have refine_1 : (M j).Indep (Sigma.mk (β := α) j ⁻¹' I)
Tactic: rw [sigma_mk_preimage_image' hij, union_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
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
have refine_4 : ∀ (J : Set ((i : ι) × α i)) (hJ : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' J)) (hJX : J ⊆ X) (hIJ : I ⊆ J)
  (x : (i : ι) × α i) (i : ι) (x : α i) (hx : Sigma.mk (β := fun (i : ι) ↦ α i) i x ∈ J),
  Sigma.mk (β := fun (i : ι) ↦ α i) i x ∈ I
Tactic: refine fun J hJ hJX hIJ ↦ hIJ.antisymm fun ⟨i,x⟩ hx ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
⊢ (Matroid.sigma (α := α) M).Finitary
have refine : ∀ (I : Set ((i : ι) × α i)) (hI : ∀ J ⊆ I, J.Finite → (Matroid.sigma (α := α) M).Indep J),
  (Matroid.sigma (α := α) M).Indep I
Tactic: refine ⟨fun I hI ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
I : Set ((i : ι) × α i)
hI : ∀ J ⊆ I, J.Finite → (Matroid.sigma (α := α) M).Indep J
⊢ (Matroid.sigma (α := α) M).Indep I
have hI₁ : ∀ J ⊆ I, J.Finite → ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' J)
Tactic: simp only [sigma_indep_iff] at hI ⊢
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
I : Set ((i : ι) × α i)
hI : ∀ J ⊆ I, J.Finite → ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' J)
i : ι
⊢ (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)
have h₁ : ∀ J ⊆ Sigma.mk (β := α) i ⁻¹' I, J.Finite → (M i).Indep J
Tactic: apply indep_of_forall_finite_subset_indep
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
I : Set ((i : ι) × α i)
hI : ∀ J ⊆ I, J.Finite → ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' J)
i : ι
J : Set (α i)
hJI : J ⊆ Sigma.mk (β := α) i ⁻¹' I
hJ : J.Finite
⊢ (M i).Indep J
have h₁ : J = Sigma.mk (β := α) i ⁻¹' Sigma.mk (β := fun (i : ι) ↦ α i) i '' J
Tactic: convert! hI (Sigma.mk i '' J) (by simpa) (hJ.image _) i
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
I : Set ((i : ι) × α i)
hI : ∀ J ⊆ I, J.Finite → ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' J)
i : ι
J : Set (α i)
hJI : J ⊆ Sigma.mk (β := α) i ⁻¹' I
hJ : J.Finite
⊢ J = Sigma.mk (β := α) i ⁻¹' Sigma.mk (β := fun (i : ι) ↦ α i) i '' J
have h₁ : J = J
Tactic: rw [sigma_mk_preimage_image_eq_self]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
I : Set (ι × α)
⊢ (Matroid.sum' M).Indep I ↔ ∀ (i : ι), (M i).Indep (Prod.mk i ⁻¹' I)
have simp : (∀ (i : ι),
    (M i).Indep
      (preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) i)
        ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' I))) ↔
  ∀ (i : ι), (M i).Indep (Prod.mk i ⁻¹' I)
Tactic: simp only [Matroid.sum', mapEquiv_indep_iff, Equiv.sigmaEquivProd_symm_apply, sigma_indep_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
I : Set (ι × α)
⊢ (∀ (i : ι),
      (M i).Indep
        (preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) i)
          ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' I))) ↔
    ∀ (i : ι), (M i).Indep (Prod.mk i ⁻¹' I)
have h : ∀ (a : ι),
  Prod.mk a ⁻¹' I =
    preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) a)
      ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' I)
Tactic: convert! Iff.rfl