awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Finite (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hY : M.IsRkFinite Y
I : Set α
hI : M.IsBasis' I X
hIfin : I.Finite
J : Set α
hJ : M.IsBasis' J Y
hJfin : J.Finite
⊢ (X ∪ Y) ∩ M.E ⊆ M.closure (I ∪ J)
have rw : (X ∪ Y) ∩ M.E ⊆ M.closure (X ∪ Y)
Tactic: rw [closure_union_congr_left hI.closure_eq_closure,
    closure_union_congr_right hJ.closure_eq_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Finite (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
⊢ M.IsRkFinite (Y \ X) ↔ M.IsRkFinite Y
have rw : M.IsRkFinite (X ∪ Y \ X) ↔ M.IsRkFinite Y
Tactic: rw [← hX.isRkFinite_union_iff, union_diff_self, hX.isRkFinite_union_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Finite (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
rw : M.IsRkFinite (X ∪ Y \ X) ↔ M.IsRkFinite Y
⊢ M.IsRkFinite (Y \ X) ↔ M.IsRkFinite Y
have rw₁ : M.IsRkFinite (X ∪ Y) ↔ M.IsRkFinite Y
Tactic: rw [← hX.isRkFinite_union_iff, union_diff_self, hX.isRkFinite_union_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Finite (goal)
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
rw : M.IsRkFinite (X ∪ Y \ X) ↔ M.IsRkFinite Y
rw₁ : M.IsRkFinite (X ∪ Y) ↔ M.IsRkFinite Y
⊢ M.IsRkFinite (Y \ X) ↔ M.IsRkFinite Y
have rw₂ : M.IsRkFinite Y ↔ M.IsRkFinite Y
Tactic: rw [← hX.isRkFinite_union_iff, union_diff_self, hX.isRkFinite_union_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Finite (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.IsRkFinite X
e : α
⊢ M.IsRkFinite (Insert.insert e X)
have rw : M.IsRkFinite (X ∪ {e})
Tactic: rw [← union_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Finite (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
⊢ M.IsRkFinite (insert e X) ↔ M.IsRkFinite X
have rw : M.IsRkFinite ({e} ∪ X) ↔ M.IsRkFinite X
Tactic: rw [← singleton_union, isRkFinite_singleton.isRkFinite_union_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Finite (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
rw : M.IsRkFinite ({e} ∪ X) ↔ M.IsRkFinite X
⊢ M.IsRkFinite (insert e X) ↔ M.IsRkFinite X
have rw₁ : M.IsRkFinite X ↔ M.IsRkFinite X
Tactic: rw [← singleton_union, isRkFinite_singleton.isRkFinite_union_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Finite (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
⊢ M.IsRkFinite (X \ {e}) ↔ M.IsRkFinite X
have rw : M.IsRkFinite X ↔ M.IsRkFinite X
Tactic: rw [isRkFinite_singleton.isRkFinite_diff_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Finite (goal)
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
inst : Finite ι
Xs : ι → Set α
h : ∀ (i : ι), M.IsRkFinite (Xs i)
⊢ M.IsRkFinite (⋃ (i : ι), Xs i)
have choose : ∀ (Is : (i : ι) → Set α) (hIs : ∀ (i : ι), M.IsBasis' (Is i) (Xs i)), M.IsRkFinite (⋃ (i : ι), Xs i)
Tactic: choose Is hIs using fun i ↦ M.exists_isBasis' (Xs i)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Finite (hypothesis)
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
inst : Finite ι
Xs : ι → Set α
h : ∀ (i : ι), M.IsRkFinite (Xs i)
Is : (i : ι) → Set α
hIs : ∀ (i : ι), M.IsBasis' (Is i) (Xs i)
⊢ M.IsRkFinite (⋃ (i : ι), Xs i)
have hfin : Set.Finite.{u_1} (α := α) (⋃ (i : ι), Is i)
Tactic: have hfin : (⋃ i, Is i).Finite := finite_iUnion <| fun i ↦ (h i).finite_of_isBasis' (hIs i)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Finite (goal)
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
inst : Finite ι
Xs : ι → Set α
h : ∀ (i : ι), M.IsRkFinite (Xs i)
Is : (i : ι) → Set α
hIs : ∀ (i : ι), M.IsBasis' (Is i) (Xs i)
hfin : Set.Finite.{u_1} (α := α) (⋃ (i : ι), Is i)
⊢ M.IsRkFinite (⋃ (i : ι), Xs i)
have refine : (⋃ (i : ι), Xs i) ∩ M.E ⊆ M.closure (⋃ (i : ι), Is i)
Tactic: refine isRkFinite_inter_ground_iff.1 <| (M.isRkFinite_of_finite hfin).closure.subset ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Finite (goal)
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
inst : Finite ι
Xs : ι → Set α
h : ∀ (i : ι), M.IsRkFinite (Xs i)
Is : (i : ι) → Set α
hIs : ∀ (i : ι), M.IsBasis' (Is i) (Xs i)
hfin : Set.Finite.{u_1} (α := α) (⋃ (i : ι), Is i)
⊢ (⋃ (i : ι), Xs i) ∩ M.E ⊆ M.closure (⋃ (i : ι), Is i)
have rw : ∀ (i : ι), Xs i ∩ M.E ⊆ M.closure (⋃ (i : ι), Is i)
Tactic: rw [iUnion_inter, iUnion_subset_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
I : Set ((i : ι) × α i)
⊢ (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)) ↔
    ∃ (B : Set ((i : ι) × α i)), (∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) ∧ I ⊆ B
have refine : ∀ (h : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)),
  ∃ (B : Set ((i : ι) × α i)), (∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) ∧ I ⊆ B
Tactic: refine ⟨fun h ↦ ?_, fun ⟨B, hB, hIB⟩ i ↦ (hB i).indep.subset (preimage_mono hIB)⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
I : Set ((i : ι) × α i)
h : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)
⊢ ∃ (B : Set ((i : ι) × α i)), (∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) ∧ I ⊆ B
have choose : ∀ (Bs : (i : ι) → Set (α i)) (hBs : ∀ (i : ι), (M i).IsBase (Bs i) ∧ Sigma.mk (β := α) i ⁻¹' I ⊆ Bs i),
  ∃ (B : Set ((i : ι) × α i)), (∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) ∧ I ⊆ B
Tactic: choose Bs hBs using fun i ↦ (h i).exists_isBase_superset
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
I : Set ((i : ι) × α i)
h : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)
Bs : (i : ι) → Set (α i)
hBs : ∀ (i : ι), (M i).IsBase (Bs i) ∧ Sigma.mk (β := α) i ⁻¹' I ⊆ Bs i
⊢ ∃ (B : Set ((i : ι) × α i)), (∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) ∧ I ⊆ B
have refine : I ⊆ Set.sigma (α := α) univ Bs
Tactic: refine ⟨univ.sigma Bs, fun i ↦ by simpa using (hBs i).1, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
I : Set ((i : ι) × α i)
h : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)
Bs : (i : ι) → Set (α i)
hBs : ∀ (i : ι), (M i).IsBase (Bs i) ∧ Sigma.mk (β := α) i ⁻¹' I ⊆ Bs i
⊢ I ⊆ Set.sigma (α := α) univ Bs
have rw : (Set.sigma (α := fun (i : ι) ↦ α i) univ fun (i : ι) ↦ Sigma.mk (β := fun (i : ι) ↦ α i) i ⁻¹' I) ⊆
  Set.sigma (α := α) univ Bs
Tactic: rw [← univ_sigma_preimage_mk 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)), ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)
have choose : ∀ (B : (i : ι) → Set (α i)) (hB : ∀ (i : ι), (M i).IsBase (B i)),
  ∃ (B : Set ((i : ι) × α i)), ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)
Tactic: choose B hB using fun i ↦ (M i).exists_isBase
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₁
h₂ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₂
⊢ ∀ a ∈ B₁ \ B₂,
    ∃ b ∈ B₂ \ B₁,
      (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) (insert b (B₁ \ {a}))
have simp : ∀ (a : ι) (b : α a),
  Sigma.mk (β := fun (a : ι) ↦ α a) a b ∈ B₁ →
    Sigma.mk (β := fun (a : ι) ↦ α a) a b ∉ B₂ →
      ∃ (a_3 : ι) (b_1 : α a_3),
        (Sigma.mk (β := fun (a : ι) ↦ α a) a_3 b_1 ∈ B₂ ∧ Sigma.mk (β := fun (a : ι) ↦ α a) a_3 b_1 ∉ B₁) ∧
          ∀ (i : ι),
            (M i).IsBase
              (Sigma.mk (β := α) i ⁻¹'
                insert (Sigma.mk (β := fun (a : ι) ↦ α a) a_3 b_1) (B₁ \ {Sigma.mk (β := fun (a : ι) ↦ α a) a b}))
Tactic: simp only [mem_diff, Sigma.exists, and_imp, Sigma.forall]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₁
h₂ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∈ B₁
he₂ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∉ B₂
⊢ ∃ (a : ι) (b : α a),
    (Sigma.mk (β := fun (a : ι) ↦ α a) a b ∈ B₂ ∧ Sigma.mk (β := fun (a : ι) ↦ α a) a b ∉ B₁) ∧
      ∀ (i_1 : ι),
        (M i_1).IsBase
          (Sigma.mk (β := α) i_1 ⁻¹'
            insert (Sigma.mk (β := fun (a : ι) ↦ α a) a b) (B₁ \ {Sigma.mk (β := fun (a : ι) ↦ α a) i e}))
have hf_ex : ∃ y ∈ Sigma.mk (β := α) i ⁻¹' B₂ \ Sigma.mk (β := α) i ⁻¹' B₁,
  (M i).IsBase (insert y (Sigma.mk (β := α) i ⁻¹' B₁ \ {e}))
Tactic: have hf_ex := (h₁ i).exchange (h₂ i) ⟨he₁, by simpa⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₁
h₂ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∈ B₁
he₂ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∉ B₂
hf_ex :
  ∃ y ∈ Sigma.mk (β := α) i ⁻¹' B₂ \ Sigma.mk (β := α) i ⁻¹' B₁,
    (M i).IsBase (insert y (Sigma.mk (β := α) i ⁻¹' B₁ \ {e}))
⊢ ∃ (a : ι) (b : α a),
    (Sigma.mk (β := fun (a : ι) ↦ α a) a b ∈ B₂ ∧ Sigma.mk (β := fun (a : ι) ↦ α a) a b ∉ B₁) ∧
      ∀ (i_1 : ι),
        (M i_1).IsBase
          (Sigma.mk (β := α) i_1 ⁻¹'
            insert (Sigma.mk (β := fun (a : ι) ↦ α a) a b) (B₁ \ {Sigma.mk (β := fun (a : ι) ↦ α a) i e}))
have obtain : ∀ (f : α i) (hfB : (M i).IsBase (insert f (Sigma.mk (β := α) i ⁻¹' B₁ \ {e}))) (hf₁ : f ∈ Sigma.mk (β := α) i ⁻¹' B₂)
  (hf₂ : f ∉ Sigma.mk (β := α) i ⁻¹' B₁),
  ∃ (a : ι) (b : α a),
    (Sigma.mk (β := fun (a : ι) ↦ α a) a b ∈ B₂ ∧ Sigma.mk (β := fun (a : ι) ↦ α a) a b ∉ B₁) ∧
      ∀ (i_1 : ι),
        (M i_1).IsBase
          (Sigma.mk (β := α) i_1 ⁻¹'
            insert (Sigma.mk (β := fun (a : ι) ↦ α a) a b) (B₁ \ {Sigma.mk (β := fun (a : ι) ↦ α a) i e}))
Tactic: obtain ⟨f, ⟨hf₁, hf₂⟩, hfB⟩ := hf_ex
Cleared hypotheses: hf_ex
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₁
h₂ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∈ B₁
he₂ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∉ B₂
f : α i
hfB : (M i).IsBase (insert f (Sigma.mk (β := α) i ⁻¹' B₁ \ {e}))
hf₁ : f ∈ Sigma.mk (β := α) i ⁻¹' B₂
hf₂ : f ∉ Sigma.mk (β := α) i ⁻¹' B₁
⊢ ∃ (a : ι) (b : α a),
    (Sigma.mk (β := fun (a : ι) ↦ α a) a b ∈ B₂ ∧ Sigma.mk (β := fun (a : ι) ↦ α a) a b ∉ B₁) ∧
      ∀ (i_1 : ι),
        (M i_1).IsBase
          (Sigma.mk (β := α) i_1 ⁻¹'
            insert (Sigma.mk (β := fun (a : ι) ↦ α a) a b) (B₁ \ {Sigma.mk (β := fun (a : ι) ↦ α a) i e}))
have refine : ∀ (j : ι),
  (M j).IsBase
    (Sigma.mk (β := α) j ⁻¹'
      insert (Sigma.mk (β := fun (a : ι) ↦ α a) i f) (B₁ \ {Sigma.mk (β := fun (a : ι) ↦ α a) i e}))
Tactic: refine ⟨i, f, ⟨hf₁, hf₂⟩, fun j ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₁
h₂ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∈ B₁
he₂ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∉ B₂
f : α i
hfB : (M i).IsBase (insert f (Sigma.mk (β := α) i ⁻¹' B₁ \ {e}))
hf₁ : f ∈ Sigma.mk (β := α) i ⁻¹' B₂
hf₂ : f ∉ Sigma.mk (β := α) i ⁻¹' B₁
j : ι
⊢ (M j).IsBase
    (Sigma.mk (β := α) j ⁻¹'
      insert (Sigma.mk (β := fun (a : ι) ↦ α a) i f) (B₁ \ {Sigma.mk (β := fun (a : ι) ↦ α a) i e}))
have rw : (M j).IsBase
  (Sigma.mk (β := α) j ⁻¹' B₁ \ Sigma.mk (β := α) j ⁻¹' {Sigma.mk (β := fun (a : ι) ↦ α a) i e} ∪
    Sigma.mk (β := α) j ⁻¹' {Sigma.mk (β := fun (a : ι) ↦ α a) i f})
Tactic: rw [← union_singleton, preimage_union, preimage_diff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₁
h₂ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∈ B₁
he₂ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∉ B₂
f : α i
hfB : (M i).IsBase (insert f (Sigma.mk (β := α) i ⁻¹' B₁ \ {e}))
hf₁ : f ∈ Sigma.mk (β := α) i ⁻¹' B₂
hf₂ : f ∉ Sigma.mk (β := α) i ⁻¹' B₁
j : ι
⊢ (M j).IsBase
    (Sigma.mk (β := α) j ⁻¹' B₁ \ Sigma.mk (β := α) j ⁻¹' {Sigma.mk (β := fun (a : ι) ↦ α a) i e} ∪
      Sigma.mk (β := α) j ⁻¹' {Sigma.mk (β := fun (a : ι) ↦ α a) i f})
have inl : (M i).IsBase
  (Sigma.mk (β := α) i ⁻¹' B₁ \ Sigma.mk (β := α) i ⁻¹' {Sigma.mk (β := fun (a : ι) ↦ α a) i e} ∪
    Sigma.mk (β := α) i ⁻¹' {Sigma.mk (β := fun (a : ι) ↦ α a) i f})
Tactic: obtain (rfl | hne) := 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_1 M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₁
h₂ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∈ B₁
he₂ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∉ B₂
f : α i
hfB : (M i).IsBase (insert f (Sigma.mk (β := α) i ⁻¹' B₁ \ {e}))
hf₁ : f ∈ Sigma.mk (β := α) i ⁻¹' B₂
hf₂ : f ∉ Sigma.mk (β := α) i ⁻¹' B₁
j : ι
inl :
  (M i).IsBase
    (Sigma.mk (β := α) i ⁻¹' B₁ \ Sigma.mk (β := α) i ⁻¹' {Sigma.mk (β := fun (a : ι) ↦ α a) i e} ∪
      Sigma.mk (β := α) i ⁻¹' {Sigma.mk (β := fun (a : ι) ↦ α a) i f})
⊢ (M j).IsBase
    (Sigma.mk (β := α) j ⁻¹' B₁ \ Sigma.mk (β := α) j ⁻¹' {Sigma.mk (β := fun (a : ι) ↦ α a) i e} ∪
      Sigma.mk (β := α) j ⁻¹' {Sigma.mk (β := fun (a : ι) ↦ α a) i f})
have inr : ∀ (hne : i ≠ j),
  (M j).IsBase
    (Sigma.mk (β := α) j ⁻¹' B₁ \ Sigma.mk (β := α) j ⁻¹' {Sigma.mk (β := fun (a : ι) ↦ α a) i e} ∪
      Sigma.mk (β := α) j ⁻¹' {Sigma.mk (β := fun (a : ι) ↦ α a) i f})
Tactic: obtain (rfl | hne) := eq_or_ne i j
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
M_1 M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₁
h₂ : (fun (B : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk (β := α) i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∈ B₁
he₂ : Sigma.mk (β := fun (a : ι) ↦ α a) i e ∉ B₂
f : α i
hfB : (M i).IsBase (insert f (Sigma.mk (β := α) i ⁻¹' B₁ \ {e}))
hf₁ : f ∈ Sigma.mk (β := α) i ⁻¹' B₂
hf₂ : f ∉ Sigma.mk (β := α) i ⁻¹' B₁
j : ι
hne : i ≠ j
⊢ (M j).IsBase
    (Sigma.mk (β := α) j ⁻¹' B₁ \ Sigma.mk (β := α) j ⁻¹' {Sigma.mk (β := fun (a : ι) ↦ α a) i e} ∪
      Sigma.mk (β := α) j ⁻¹' {Sigma.mk (β := fun (a : ι) ↦ α a) i f})
have inr : (M j).IsBase (Sigma.mk (β := α) j ⁻¹' B₁)
Tactic: rw [preimage_singleton_eq_empty.2 (by simpa), preimage_singleton_eq_empty.2 (by simpa),
      diff_empty, union_empty]
-- 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
⊢ ∃ (J : Set ((i : ι) × α i)),
    I ⊆ J ∧
      Maximal
        (fun (K : Set ((i : ι) × α i)) ↦
          (fun (I : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)) K ∧ K ⊆ X)
        J
have choose : ∀ (Js : (i : ι) → Set (α i))
  (hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk (β := α) i ⁻¹' X) ∧ Sigma.mk (β := α) i ⁻¹' I ⊆ Js i),
  ∃ (J : Set ((i : ι) × α i)),
    I ⊆ J ∧
      Maximal
        (fun (K : Set ((i : ι) × α i)) ↦
          (fun (I : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)) K ∧ K ⊆ X)
        J
Tactic: choose Js hJs using
      fun i ↦ (hI i).subset_isBasis'_of_subset (preimage_mono (f := Sigma.mk i) hIX)
-- 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
⊢ ∃ (J : Set ((i : ι) × α i)),
    I ⊆ J ∧
      Maximal
        (fun (K : Set ((i : ι) × α i)) ↦
          (fun (I : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)) K ∧ K ⊆ X)
        J
have h : I ⊆ Set.sigma (α := α) univ Js ∧
  Maximal
    (fun (K : Set ((i : ι) × α i)) ↦
      (fun (I : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)) K ∧ K ⊆ X)
    (Set.sigma (α := α) univ Js)
Tactic: use univ.sigma Js
-- 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
⊢ I ⊆ Set.sigma (α := α) univ Js ∧
    Maximal
      (fun (K : Set ((i : ι) × α i)) ↦
        (fun (I : Set ((i : ι) × α i)) ↦ ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)) K ∧ K ⊆ X)
      (Set.sigma (α := α) univ Js)
have h : I ⊆ Set.sigma (α := α) univ Js ∧
  ((∀ (i : ι), (M i).Indep (Js i)) ∧ Set.sigma (α := α) univ Js ⊆ X) ∧
    ∀ ⦃t : Set ((i : ι) × α i)⦄,
      (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) →
        t ⊆ X → Set.sigma (α := α) univ Js ⊆ t → t ⊆ Set.sigma (α := α) univ Js
Tactic: simp only [maximal_subset_iff', mem_univ, mk_preimage_sigma, and_imp]
-- 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
⊢ I ⊆ Set.sigma (α := α) univ Js ∧
    ((∀ (i : ι), (M i).Indep (Js i)) ∧ Set.sigma (α := α) univ Js ⊆ X) ∧
      ∀ ⦃t : Set ((i : ι) × α i)⦄,
        (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) →
          t ⊆ X → Set.sigma (α := α) univ Js ⊆ t → t ⊆ Set.sigma (α := α) univ Js
have h : I ⊆ Set.sigma (α := α) univ Js
Tactic: refine ⟨?_, ⟨fun i ↦ (hJs i).1.indep, ?_⟩, fun S hS hSX hJS ↦ ?_⟩
-- 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_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
h : I ⊆ Set.sigma (α := α) univ Js
⊢ I ⊆ Set.sigma (α := α) univ Js ∧
    ((∀ (i : ι), (M i).Indep (Js i)) ∧ Set.sigma (α := α) univ Js ⊆ X) ∧
      ∀ ⦃t : Set ((i : ι) × α i)⦄,
        (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) →
          t ⊆ X → Set.sigma (α := α) univ Js ⊆ t → t ⊆ Set.sigma (α := α) univ Js
have h₁ : Set.sigma (α := α) univ Js ⊆ X
Tactic: refine ⟨?_, ⟨fun i ↦ (hJs i).1.indep, ?_⟩, fun S hS hSX hJS ↦ ?_⟩
-- 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_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
h : I ⊆ Set.sigma (α := α) univ Js
h₁ : Set.sigma (α := α) univ Js ⊆ X
⊢ I ⊆ Set.sigma (α := α) univ Js ∧
    ((∀ (i : ι), (M i).Indep (Js i)) ∧ Set.sigma (α := α) univ Js ⊆ X) ∧
      ∀ ⦃t : Set ((i : ι) × α i)⦄,
        (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) →
          t ⊆ X → Set.sigma (α := α) univ Js ⊆ t → t ⊆ Set.sigma (α := α) univ Js
have h₂ : ∀ (S : Set ((i : ι) × α i)) (hS : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' S)) (hSX : S ⊆ X)
  (hJS : Set.sigma (α := α) univ Js ⊆ S), S ⊆ Set.sigma (α := α) univ Js
Tactic: refine ⟨?_, ⟨fun i ↦ (hJs i).1.indep, ?_⟩, fun S hS hSX hJS ↦ ?_⟩
-- 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
⊢ I ⊆ Set.sigma (α := α) univ Js
have h : (Set.sigma (α := fun (i : ι) ↦ α i) univ fun (i : ι) ↦ Sigma.mk (β := fun (i : ι) ↦ α i) i ⁻¹' I) ⊆
  Set.sigma (α := α) univ Js
Tactic: rw [← univ_sigma_preimage_mk 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
⊢ Set.sigma (α := α) univ Js ⊆ X
have h : Set.sigma (α := α) univ Js ⊆
  Set.sigma (α := fun (i : ι) ↦ α i) univ fun (i : ι) ↦ Sigma.mk (β := fun (i : ι) ↦ α i) i ⁻¹' X
Tactic: rw [← univ_sigma_preimage_mk X]
-- 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
⊢ S ⊆ Set.sigma (α := α) univ Js
have h : (Set.sigma (α := fun (i : ι) ↦ α i) univ fun (i : ι) ↦ Sigma.mk (β := fun (i : ι) ↦ α i) i ⁻¹' S) ⊆
  Set.sigma (α := α) univ Js
Tactic: rw [← univ_sigma_preimage_mk S]