awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
⊢ f ∈ M.fundCircuit e B
have inl : ∀ (he : e ∈ M.fundCocircuit e B), e ∈ M.fundCircuit e B
Tactic: obtain rfl | hne := eq_or_ne e f
Cleared hypotheses: f, he
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
inl : ∀ (he : e ∈ M.fundCocircuit e B), e ∈ M.fundCircuit e B
⊢ f ∈ M.fundCircuit e B
have inr : ∀ (hne : e ≠ f), f ∈ M.fundCircuit e B
Tactic: obtain rfl | hne := eq_or_ne e f
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (hypothesis)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
⊢ f ∈ M.fundCircuit e B
have hB' : M✶.IsBase (M✶.E \ B)
Tactic: have hB' : M✶.IsBase (M✶.E \ B) := hB.compl_isBase_dual
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
⊢ f ∈ M.fundCircuit e B
have inr : ∀ (hfE : f ∉ M.E), f ∈ M.fundCircuit e B
Tactic: obtain hfE | hfE := em' <| f ∈ M.E
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
inr : ∀ (hfE : f ∉ M.E), f ∈ M.fundCircuit e B
⊢ f ∈ M.fundCircuit e B
have inr₁ : ∀ (hfE : f ∈ M.E), f ∈ M.fundCircuit e B
Tactic: obtain hfE | hfE := em' <| f ∈ M.E
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (hypothesis)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∉ M.E
⊢ f ∈ M.fundCircuit e B
have he₁ : Membership.mem (γ := Set α) {f} e
Tactic: rw [fundCocircuit, fundCircuit_eq_of_notMem_ground (by simpa)] at he
Cleared hypotheses: he, hne, hB', hfE
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
⊢ f ∈ M.fundCircuit e B
have inr : ∀ (hfB : f ∉ B), f ∈ M.fundCircuit e B
Tactic: obtain hfB | hfB := em' <| f ∈ B
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
inr : ∀ (hfB : f ∉ B), f ∈ M.fundCircuit e B
⊢ f ∈ M.fundCircuit e B
have inr₁ : ∀ (hfB : f ∈ B), f ∈ M.fundCircuit e B
Tactic: obtain hfB | hfB := em' <| f ∈ B
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (hypothesis)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∉ B
⊢ f ∈ M.fundCircuit e B
have he₁ : Membership.mem (γ := Set α) {f} e
Tactic: rw [fundCocircuit, fundCircuit_eq_of_mem (by simp [hfE, hfB])] at he
Cleared hypotheses: he, hne, hB', hfE, hfB
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (hypothesis)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
⊢ f ∈ M.fundCircuit e B
have heE : e ∈ M.E
Tactic: obtain ⟨heE, heB⟩ : e ∈ M.E \ B := by
    simpa [hne] using (M.fundCocircuit_subset_insert_compl f B) he
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (hypothesis)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
⊢ f ∈ M.fundCircuit e B
have heB : e ∉ B
Tactic: obtain ⟨heE, heB⟩ : e ∈ M.E \ B := by
    simpa [hne] using (M.fundCocircuit_subset_insert_compl f B) he
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M✶.fundCircuit f (M✶.E \ B)
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
⊢ f ∈ M✶.closure (M✶.E \ B)
have rwa : f ∈ M✶.E
Tactic: rwa [hB'.closure_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (hypothesis)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
⊢ f ∈ M.fundCircuit e B
have he₁ : M✶.Indep (insert f (M✶.E \ B) \ {e})
Tactic: rw [fundCocircuit, hB'.indep.mem_fundCircuit_iff (by rwa [hB'.closure_eq]) (by simp [hfB])] at he
Cleared hypotheses: he, hne, hB', hfE, hfB, heE, heB
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
⊢ f ∈ M.fundCircuit e B
have inr : M.Indep (insert e B \ {f})
Tactic: rw [hB.indep.mem_fundCircuit_iff (by rwa [hB.closure_eq]) heB]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (hypothesis)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
⊢ M.Indep (insert e B \ {f})
have hB'₁ : M.IsBase (M.E \ (insert f (M✶.E \ B) \ {e}))
Tactic: have hB' : M.IsBase (M.E \ (insert f (M✶.E \ B) \ {e})) :=
    (hB'.exchange_isBase_of_indep' ⟨heE, heB⟩ (by simp [hfE, hfB]) he).compl_isBase_of_dual
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB'_1 : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
hB' : M.IsBase (M.E \ (insert f (M✶.E \ B) \ {e}))
⊢ M.Indep (insert e B \ {f})
have inr : insert e B \ {f} ⊆ M.E \ (insert f (M✶.E \ B) \ {e})
Tactic: refine hB'.indep.subset ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB'_1 : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
hB' : M.IsBase (M.E \ (insert f (M✶.E \ B) \ {e}))
⊢ insert e B \ {f} ⊆ M.E \ (insert f (M✶.E \ B) \ {e})
have inr : insert e B ⊆ insert f (M.E \ (insert f (M.E \ B) \ {e}))
Tactic: simp only [dual_ground, diff_singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Circuit (goal)
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB'_1 : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
hB' : M.IsBase (M.E \ (insert f (M✶.E \ B) \ {e}))
⊢ insert e B ⊆ insert f (M.E \ (insert f (M.E \ B) \ {e}))
have inr : insert e B ⊆ insert e (insert f (B \ {f}))
Tactic: rw [diff_diff_right, inter_eq_self_of_subset_right (by simpa), union_singleton, insert_comm,
    ← union_singleton (s := M.E \ B), ← diff_diff, diff_diff_cancel_left hB.subset_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
ι : Type u_3
inst : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.IsFlat (Fs i)
⊢ M.IsFlat (⋂ (i : ι), Fs i)
have refine : ∀ (I X : Set α) (hI : M.IsBasis I (⋂ (i : ι), Fs i)) (hIX : M.IsBasis I X) (i : ι), X ⊆ Fs i
Tactic: refine ⟨fun I X hI hIX ↦ subset_iInter fun i ↦ ?_,
    (iInter_subset _ (Classical.arbitrary _)).trans (hFs _).subset_ground⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
ι : Type u_3
inst : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.IsFlat (Fs i)
I X : Set α
hI : M.IsBasis I (⋂ (i : ι), Fs i)
hIX : M.IsBasis I X
i : ι
⊢ X ⊆ Fs i
have obtain : ∀ (J : Set α) (hIJ : M.IsBasis J (Fs i)) (hJ : I ⊆ J), X ⊆ Fs i
Tactic: obtain ⟨J, hIJ, hJ⟩ := hI.indep.subset_isBasis_of_subset (hI.subset.trans (iInter_subset _ i))
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
ι : Type u_3
inst : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.IsFlat (Fs i)
I X : Set α
hI : M.IsBasis I (⋂ (i : ι), Fs i)
hIX : M.IsBasis I X
i : ι
J : Set α
hIJ : M.IsBasis J (Fs i)
hJ : I ⊆ J
⊢ X ⊆ Fs i
have refine : M.IsBasis J (Fs i ∪ X)
Tactic: refine subset_union_right.trans ((hFs i).1 (X := Fs i ∪ X) hIJ ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
ι : Type u_3
inst : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.IsFlat (Fs i)
I X : Set α
hI : M.IsBasis I (⋂ (i : ι), Fs i)
hIX : M.IsBasis I X
i : ι
J : Set α
hIJ : M.IsBasis J (Fs i)
hJ : I ⊆ J
⊢ M.IsBasis J (Fs i ∪ X)
have h : Fs i ∪ X = Fs i ∪ (J ∪ X)
Tactic: convert! hIJ.isBasis_union (hIX.isBasis_union_of_subset hIJ.indep hJ) using 1
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
ι : Type u_3
inst : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.IsFlat (Fs i)
I X : Set α
hI : M.IsBasis I (⋂ (i : ι), Fs i)
hIX : M.IsBasis I X
i : ι
J : Set α
hIJ : M.IsBasis J (Fs i)
hJ : I ⊆ J
⊢ Fs i ∪ X = Fs i ∪ (J ∪ X)
have h : Fs i ∪ X = Fs i ∪ J ∪ X
Tactic: rw [← union_assoc, union_eq_self_of_subset_right hIJ.subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
ι : Type u_3
inst : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.IsFlat (Fs i)
I X : Set α
hI : M.IsBasis I (⋂ (i : ι), Fs i)
hIX : M.IsBasis I X
i : ι
J : Set α
hIJ : M.IsBasis J (Fs i)
hJ : I ⊆ J
h : Fs i ∪ X = Fs i ∪ J ∪ X
⊢ Fs i ∪ X = Fs i ∪ (J ∪ X)
have h₁ : Fs i ∪ X = Fs i ∪ X
Tactic: rw [← union_assoc, union_eq_self_of_subset_right hIJ.subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
ι : Type u_1
α : Type u_2
M_1 : Matroid α
F X Y : Set α
e f : α
M : Matroid α
s : Set (↑(Iic M.E) : Type u_2)
hs : ∀ a ∈ s, (fun (F : (↑(Iic M.E) : Type u_2)) ↦ M.IsFlat (↑F : Set α)) a
⊢ (fun (F : (↑(Iic M.E) : Type u_2)) ↦ M.IsFlat (↑F : Set α)) (sInf s)
have inl : ∀
  (hs :
    ∀ (a : (↑(Iic M.E) : Type u_2)),
      Membership.mem (γ := Set (↑(Iic M.E) : Type u_2)) ∅ a →
        (fun (F : (↑(Iic M.E) : Type u_2)) ↦ M.IsFlat (↑F : Set α)) a),
  M.IsFlat (↑(sInf ∅) : Set α)
Tactic: obtain (rfl | hne) := s.eq_empty_or_nonempty
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
ι : Type u_1
α : Type u_2
M_1 : Matroid α
F X Y : Set α
e f : α
M : Matroid α
s : Set (↑(Iic M.E) : Type u_2)
hs : ∀ a ∈ s, (fun (F : (↑(Iic M.E) : Type u_2)) ↦ M.IsFlat (↑F : Set α)) a
inl :
  ∀
    (hs :
      ∀ (a : (↑(Iic M.E) : Type u_2)),
        Membership.mem (γ := Set (↑(Iic M.E) : Type u_2)) ∅ a →
          (fun (F : (↑(Iic M.E) : Type u_2)) ↦ M.IsFlat (↑F : Set α)) a),
    M.IsFlat (↑(sInf ∅) : Set α)
⊢ M.IsFlat (↑(sInf s) : Set α)
have inr : ∀ (hne : s.Nonempty), M.IsFlat (↑(sInf s) : Set α)
Tactic: obtain (rfl | hne) := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
M_1 : Matroid α
F X Y : Set α
e f : α
M : Matroid α
s : Set (↑(Iic M.E) : Type u_2)
hs : ∀ a ∈ s, (fun (F : (↑(Iic M.E) : Type u_2)) ↦ M.IsFlat (↑F : Set α)) a
hne : s.Nonempty
⊢ M.IsFlat (↑(sInf s) : Set α)
have x : Nonempty.{u_2 + 1} (↑s : Type u_2)
Tactic: have _ := hne.coe_sort
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
ι : Type u_1
α : Type u_2
M_1 : Matroid α
F X Y : Set α
e f : α
M : Matroid α
s : Set (↑(Iic M.E) : Type u_2)
hs : ∀ a ∈ s, (fun (F : (↑(Iic M.E) : Type u_2)) ↦ M.IsFlat (↑F : Set α)) a
hne : s.Nonempty
h : Nonempty.{u_2 + 1} (↑s : Type u_2)
⊢ M.IsFlat (↑(sInf s) : Set α)
have h : (↑(sInf s) : Set α) = ⋂ (i : (↑s : Type u_2)), (↑(↑i : (↑(Iic M.E) : Type u_2)) : Set α)
Tactic: convert! IsFlat.iInter (M := M) (Fs := fun (F : s) ↦ F.1.1) (fun F ↦ hs F.1 F.2)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
ι : Type u_1
α : Type u_2
M_1 : Matroid α
F X Y : Set α
e f : α
M : Matroid α
s : Set (↑(Iic M.E) : Type u_2)
hs : ∀ a ∈ s, (fun (F : (↑(Iic M.E) : Type u_2)) ↦ M.IsFlat (↑F : Set α)) a
hne : s.Nonempty
h : Nonempty.{u_2 + 1} (↑s : Type u_2)
⊢ (↑(sInf s) : Set α) = ⋂ (i : (↑s : Type u_2)), (↑(↑i : (↑(Iic M.E) : Type u_2)) : Set α)
have h : ∀ (x : α),
  x ∈ (↑(sInf s) : Set α) ↔
    Membership.mem (γ := Set α) (⋂ (i : (↑s : Type u_2)), (↑(↑i : (↑(Iic M.E) : Type u_2)) : Set α)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ M.closure X = ⋂₀ {F : Set α | M.IsFlat F ∧ X ⊆ F}
have rw : Eq.{u_2 + 1} (α := Set α) (⋂₀ {F : Set α | M.IsFlat F ∧ X ∩ M.E ⊆ F}) (⋂₀ {F : Set α | M.IsFlat F ∧ X ⊆ F})
Tactic: rw [closure, inter_eq_self_of_subset_left hX]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
hX : X ⊆ M.E
rw : Eq.{u_2 + 1} (α := Set α) (⋂₀ {F : Set α | M.IsFlat F ∧ X ∩ M.E ⊆ F}) (⋂₀ {F : Set α | M.IsFlat F ∧ X ⊆ F})
⊢ M.closure X = ⋂₀ {F : Set α | M.IsFlat F ∧ X ⊆ F}
have rw₁ : Eq.{u_2 + 1} (α := Set α) (⋂₀ {F : Set α | M.IsFlat F ∧ X ⊆ F}) (⋂₀ {F : Set α | M.IsFlat F ∧ X ⊆ F})
Tactic: rw [closure, inter_eq_self_of_subset_left hX]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
⊢ M.closure X =
    (↑((M.subtypeClosure : (a : (↑(Iic M.E) : Type u_2)) → (↑(Iic M.E) : Type u_2))
          (Subtype.mk (p := fun (x : Set α) ↦ x ∈ Iic M.E) (X ∩ M.E) ⋯)) :
      Set α)
have suffices : ∀ (x : α), (∀ (t : Set α), M.IsFlat t → X ∩ M.E ⊆ t → x ∈ t) ↔ x ∈ M.E ∧ ∀ a ⊆ M.E, X ∩ M.E ⊆ a → M.IsFlat a → x ∈ a
Tactic: suffices ∀ (x : α), (∀ (t : Set α), M.IsFlat t → X ∩ M.E ⊆ t → x ∈ t) ↔
    (x ∈ M.E ∧ ∀ a ⊆ M.E, X ∩ M.E ⊆ a → M.IsFlat a → x ∈ a) by
    simpa [closure, subtypeClosure, Set.ext_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
⊢ M.closure (X ∩ M.E) = M.closure X
have simp_rw : Eq.{u_2 + 1} (α := Set α) (⋂₀ {F : Set α | M.IsFlat F ∧ X ∩ M.E ∩ M.E ⊆ F}) (⋂₀ {F : Set α | M.IsFlat F ∧ X ∩ M.E ⊆ F})
Tactic: simp_rw [closure_def, inter_assoc, inter_self]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
simp_rw :
  Eq.{u_2 + 1} (α := Set α) (⋂₀ {F : Set α | M.IsFlat F ∧ X ∩ M.E ∩ M.E ⊆ F})
    (⋂₀ {F : Set α | M.IsFlat F ∧ X ∩ M.E ⊆ F})
⊢ M.closure (X ∩ M.E) = M.closure X
have simp_rw₁ : Eq.{u_2 + 1} (α := Set α) (⋂₀ {F : Set α | M.IsFlat F ∧ X ∩ (M.E ∩ M.E) ⊆ F})
  (⋂₀ {F : Set α | M.IsFlat F ∧ X ∩ M.E ⊆ F})
Tactic: simp_rw [closure_def, inter_assoc, inter_self]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
⊢ X ∩ M.E ⊆ M.closure X
have simp_rw : ∀ (t' : Set α), Membership.mem (γ := Set (Set α)) {F : Set α | M.IsFlat F ∧ X ∩ M.E ⊆ F} t' → X ∩ M.E ⊆ t'
Tactic: simp_rw [closure_def, subset_sInter_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e : α
X : Set α
hX : X ⊆ M.E
⊢ e ∈ M.closure X ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → e ∈ F
have simp_rw : Membership.mem (γ := Set α) (⋂₀ {F : Set α | M.IsFlat F ∧ X ⊆ F}) e ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → e ∈ F
Tactic: simp_rw [M.closure_def' X, mem_sInter, mem_setOf, and_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e : α
X : Set α
hX : X ⊆ M.E
simp_rw :
  Membership.mem (γ := Set α) (⋂₀ {F : Set α | M.IsFlat F ∧ X ⊆ F}) e ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → e ∈ F
⊢ e ∈ M.closure X ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → e ∈ F
have simp_rw₁ : (∀ (t : Set α), Membership.mem (γ := Set (Set α)) {F : Set α | M.IsFlat F ∧ X ⊆ F} t → e ∈ t) ↔
  ∀ (F : Set α), M.IsFlat F → X ⊆ F → e ∈ F
Tactic: simp_rw [M.closure_def' X, mem_sInter, mem_setOf, and_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e : α
X : Set α
hX : X ⊆ M.E
simp_rw :
  Membership.mem (γ := Set α) (⋂₀ {F : Set α | M.IsFlat F ∧ X ⊆ F}) e ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → e ∈ F
simp_rw₁ :
  (∀ (t : Set α), Membership.mem (γ := Set (Set α)) {F : Set α | M.IsFlat F ∧ X ⊆ F} t → e ∈ t) ↔
    ∀ (F : Set α), M.IsFlat F → X ⊆ F → e ∈ F
⊢ e ∈ M.closure X ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → e ∈ F
have simp_rw₂ : (∀ (t : Set α), M.IsFlat t ∧ X ⊆ t → e ∈ t) ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → e ∈ F
Tactic: simp_rw [M.closure_def' X, mem_sInter, mem_setOf, and_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
Y X : Set α
hX : X ⊆ M.E
⊢ Y ⊆ M.closure X ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → Y ⊆ F
have simp_rw : Y ⊆ ⋂₀ {F : Set α | M.IsFlat F ∧ X ⊆ F} ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → Y ⊆ F
Tactic: simp_rw [M.closure_def' X, subset_sInter_iff, mem_setOf, and_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
Y X : Set α
hX : X ⊆ M.E
simp_rw : Y ⊆ ⋂₀ {F : Set α | M.IsFlat F ∧ X ⊆ F} ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → Y ⊆ F
⊢ Y ⊆ M.closure X ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → Y ⊆ F
have simp_rw₁ : (∀ (t' : Set α), Membership.mem (γ := Set (Set α)) {F : Set α | M.IsFlat F ∧ X ⊆ F} t' → Y ⊆ t') ↔
  ∀ (F : Set α), M.IsFlat F → X ⊆ F → Y ⊆ F
Tactic: simp_rw [M.closure_def' X, subset_sInter_iff, mem_setOf, and_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
Y X : Set α
hX : X ⊆ M.E
simp_rw : Y ⊆ ⋂₀ {F : Set α | M.IsFlat F ∧ X ⊆ F} ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → Y ⊆ F
simp_rw₁ :
  (∀ (t' : Set α), Membership.mem (γ := Set (Set α)) {F : Set α | M.IsFlat F ∧ X ⊆ F} t' → Y ⊆ t') ↔
    ∀ (F : Set α), M.IsFlat F → X ⊆ F → Y ⊆ F
⊢ Y ⊆ M.closure X ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → Y ⊆ F
have simp_rw₂ : (∀ (t' : Set α), M.IsFlat t' ∧ X ⊆ t' → Y ⊆ t') ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → Y ⊆ F
Tactic: simp_rw [M.closure_def' X, subset_sInter_iff, mem_setOf, and_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
⊢ M.IsFlat (M.closure X)
have rw : M.IsFlat (⋂ (i : (↑{F : Set α | M.IsFlat F ∧ X ∩ M.E ⊆ F} : Type u_2)), (↑i : Set α))
Tactic: rw [closure, sInter_eq_iInter]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
⊢ M.closure univ = M.E
have rw : M.closure (univ ∩ M.E) = M.E
Tactic: rw [← closure_inter_ground, univ_inter, closure_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
rw : M.closure (univ ∩ M.E) = M.E
⊢ M.closure univ = M.E
have rw₁ : M.closure M.E = M.E
Tactic: rw [← closure_inter_ground, univ_inter, closure_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
rw : M.closure (univ ∩ M.E) = M.E
rw₁ : M.closure M.E = M.E
⊢ M.closure univ = M.E
have rw₂ : M.E = M.E
Tactic: rw [← closure_inter_ground, univ_inter, closure_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
X Y : Set α
M : Matroid α
hXY : X ⊆ Y
hX : X ⊆ M.E
⊢ X ⊆ M.closure Y
have rw : X ⊆ M.closure (Y ∩ M.E)
Tactic: rw [← closure_inter_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X Y : Set α
hXY : M.closure X ⊂ M.closure Y
⊢ ∃ e ∈ Y, e ∉ M.closure X
have by_contra! : ∀ (hcon : ∀ (e : α) (_ : e ∈ Y), e ∈ M.closure X), False
Tactic: by_contra! hcon
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
X : Set α
e : α
M : Matroid α
heX : e ∈ X
h : e ∈ M.E
⊢ e ∈ M.closure X
have rw : e ∈ M.closure (X ∩ M.E)
Tactic: rw [← closure_inter_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
ι : Type u_1
α : Type u_2
M : Matroid α
Xs : ι → Set α
⊢ M.closure (⋃ (i : ι), M.closure (Xs i)) = M.closure (⋃ (i : ι), Xs i)
have simp_rw : Eq (α := { x : Set α // x ∈ Iic M.E })
  ((M.subtypeClosure : (a : (↑(Iic M.E) : Type u_2)) → (↑(Iic M.E) : Type u_2))
      (Subtype.mk (p := fun (x : Set α) ↦ x ∈ Iic M.E)
        (⋃ (i : ι),
          (↑((M.subtypeClosure : (a : (↑(Iic M.E) : Type u_2)) → (↑(Iic M.E) : Type u_2))
                  (Subtype.mk (p := fun (x : Set α) ↦ x ∈ Iic M.E) (Xs i ∩ M.E) sorry)) :
              Set α) ∩
            M.E)
        sorry) :
    (↑(Iic M.E) : Type u_2))
  ((M.subtypeClosure : (a : (↑(Iic M.E) : Type u_2)) → (↑(Iic M.E) : Type u_2))
      (Subtype.mk (p := fun (x : Set α) ↦ x ∈ Iic M.E) (⋃ (i : ι), Xs i ∩ M.E) sorry) :
    (↑(Iic M.E) : Type u_2))
Tactic: simp_rw [closure_eq_subtypeClosure, iUnion_inter, Subtype.coe_inj]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
Xs : Set (Set α)
⊢ M.closure (⋃ X ∈ Xs, M.closure X) = M.closure (⋃₀ Xs)
have rw : M.closure (⋃ X ∈ Xs, M.closure X) = M.closure (⋃ (i : (↑Xs : Type u_2)), (↑i : Set α))
Tactic: rw [sUnion_eq_iUnion, biUnion_eq_iUnion, closure_iUnion_closure_eq_closure_iUnion]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
Xs : Set (Set α)
rw : M.closure (⋃ X ∈ Xs, M.closure X) = M.closure (⋃ (i : (↑Xs : Type u_2)), (↑i : Set α))
⊢ M.closure (⋃ X ∈ Xs, M.closure X) = M.closure (⋃₀ Xs)
have rw₁ : M.closure (⋃ (x : (↑Xs : Type u_2)), M.closure (↑x : Set α)) = M.closure (⋃ (i : (↑Xs : Type u_2)), (↑i : Set α))
Tactic: rw [sUnion_eq_iUnion, biUnion_eq_iUnion, closure_iUnion_closure_eq_closure_iUnion]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
Xs : Set (Set α)
rw : M.closure (⋃ X ∈ Xs, M.closure X) = M.closure (⋃ (i : (↑Xs : Type u_2)), (↑i : Set α))
rw₁ : M.closure (⋃ (x : (↑Xs : Type u_2)), M.closure (↑x : Set α)) = M.closure (⋃ (i : (↑Xs : Type u_2)), (↑i : Set α))
⊢ M.closure (⋃ X ∈ Xs, M.closure X) = M.closure (⋃₀ Xs)
have rw₂ : M.closure (⋃ (i : (↑Xs : Type u_2)), (↑i : Set α)) = M.closure (⋃ (i : (↑Xs : Type u_2)), (↑i : Set α))
Tactic: rw [sUnion_eq_iUnion, biUnion_eq_iUnion, closure_iUnion_closure_eq_closure_iUnion]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
ι : Type u_1
α : Type u_2
M : Matroid α
Xs : ι → Set α
A : Set ι
⊢ M.closure (⋃ i ∈ A, M.closure (Xs i)) = M.closure (⋃ i ∈ A, Xs i)
have rw : M.closure (⋃ (x : (↑A : Type u_1)), M.closure (Xs (↑x : ι))) = M.closure (⋃ i ∈ A, Xs i)
Tactic: rw [biUnion_eq_iUnion, M.closure_iUnion_closure_eq_closure_iUnion, biUnion_eq_iUnion]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
ι : Type u_1
α : Type u_2
M : Matroid α
Xs : ι → Set α
A : Set ι
rw : M.closure (⋃ (x : (↑A : Type u_1)), M.closure (Xs (↑x : ι))) = M.closure (⋃ i ∈ A, Xs i)
⊢ M.closure (⋃ i ∈ A, M.closure (Xs i)) = M.closure (⋃ i ∈ A, Xs i)
have rw₁ : M.closure (⋃ (i : (↑A : Type u_1)), Xs (↑i : ι)) = M.closure (⋃ i ∈ A, Xs i)
Tactic: rw [biUnion_eq_iUnion, M.closure_iUnion_closure_eq_closure_iUnion, biUnion_eq_iUnion]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
ι : Type u_1
α : Type u_2
M : Matroid α
Xs : ι → Set α
A : Set ι
rw : M.closure (⋃ (x : (↑A : Type u_1)), M.closure (Xs (↑x : ι))) = M.closure (⋃ i ∈ A, Xs i)
rw₁ : M.closure (⋃ (i : (↑A : Type u_1)), Xs (↑i : ι)) = M.closure (⋃ i ∈ A, Xs i)
⊢ M.closure (⋃ i ∈ A, M.closure (Xs i)) = M.closure (⋃ i ∈ A, Xs i)
have rw₂ : M.closure (⋃ (i : (↑A : Type u_1)), Xs (↑i : ι)) = M.closure (⋃ (x : (↑A : Type u_1)), Xs (↑x : ι))
Tactic: rw [biUnion_eq_iUnion, M.closure_iUnion_closure_eq_closure_iUnion, biUnion_eq_iUnion]