awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.E
rw : M.Indep (insert e I) ∧ e ∉ I ↔ M.Indep (insert e I)
⊢ e ∉ M.closure I ↔ M.Indep (insert e I)
have rw₁ : M.Indep (insert e I) ↔ M.Indep (insert e I)
Tactic: rw [hI.notMem_closure_iff, and_iff_left heI]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
heI : e ∉ I
⊢ M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I
have rw : M.Indep (insert e I) ↔ e ∈ M.E ∧ (e ∈ M.E → M.Indep (insert e I))
Tactic: rw [mem_diff, hI.mem_closure_iff_of_notMem heI, dep_iff, not_and, not_imp_not, insert_subset_iff,
    and_iff_left hI.subset_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
⊢ M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I ∨ e ∈ I
have inl : ∀ (h : e ∈ I), M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I ∨ e ∈ I
Tactic: obtain (h | h) := em (e ∈ I)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
inl : ∀ (h : e ∈ I), M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I ∨ e ∈ I
⊢ M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I ∨ e ∈ I
have inr : ∀ (h : e ∉ I), M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I ∨ e ∈ I
Tactic: obtain (h | h) := em (e ∈ I)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
h : e ∈ I
⊢ M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I ∨ e ∈ I
have inl : M.Indep I ↔ e ∈ M.E \ M.closure I ∨ e ∈ I
Tactic: simp_rw [insert_eq_of_mem h, iff_true_intro hI, true_iff, iff_true_intro h, or_true]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
h : e ∈ I
inl : M.Indep I ↔ e ∈ M.E \ M.closure I ∨ e ∈ I
⊢ M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I ∨ e ∈ I
have inl₁ : True ↔ e ∈ M.E \ M.closure I ∨ e ∈ I
Tactic: simp_rw [insert_eq_of_mem h, iff_true_intro hI, true_iff, iff_true_intro h, or_true]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
h : e ∈ I
inl : M.Indep I ↔ e ∈ M.E \ M.closure I ∨ e ∈ I
inl₁ : True ↔ e ∈ M.E \ M.closure I ∨ e ∈ I
⊢ M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I ∨ e ∈ I
have inl₂ : e ∈ M.E \ M.closure I ∨ e ∈ I
Tactic: simp_rw [insert_eq_of_mem h, iff_true_intro hI, true_iff, iff_true_intro h, or_true]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
h : e ∈ I
inl : M.Indep I ↔ e ∈ M.E \ M.closure I ∨ e ∈ I
inl₁ : True ↔ e ∈ M.E \ M.closure I ∨ e ∈ I
inl₂ : e ∈ M.E \ M.closure I ∨ e ∈ I
⊢ M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I ∨ e ∈ I
have inl₃ : e ∈ M.E \ M.closure I ∨ True
Tactic: simp_rw [insert_eq_of_mem h, iff_true_intro hI, true_iff, iff_true_intro h, or_true]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
h : e ∉ I
⊢ M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I ∨ e ∈ I
have inr : e ∈ M.E \ M.closure I ↔ e ∈ M.E \ M.closure I ∨ e ∈ I
Tactic: rw [hI.insert_indep_iff_of_notMem h, or_iff_left h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
h : e ∉ I
inr : e ∈ M.E \ M.closure I ↔ e ∈ M.E \ M.closure I ∨ e ∈ I
⊢ M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I ∨ e ∈ I
have inr₁ : e ∈ M.E \ M.closure I ↔ e ∈ M.E \ M.closure I
Tactic: rw [hI.insert_indep_iff_of_notMem h, or_iff_left h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
⊢ M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)
have pos : ∀ (hI : M.Indep I), M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)
Tactic: by_cases hI : M.Indep I
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
pos : ∀ (hI : M.Indep I), M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)
⊢ M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)
have neg : ∀ (hI : ¬M.Indep I), M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)
Tactic: by_cases hI : M.Indep I
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
⊢ M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)
have pos : e ∈ M.E \ M.closure I ∨ e ∈ I ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)
Tactic: rw [hI.insert_indep_iff, and_iff_right hI, or_iff_not_imp_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
pos : e ∈ M.E \ M.closure I ∨ e ∈ I ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)
⊢ M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)
have pos₁ : e ∈ M.E \ M.closure I ∨ e ∈ I ↔ e ∉ I → e ∈ M.E \ M.closure I
Tactic: rw [hI.insert_indep_iff, and_iff_right hI, or_iff_not_imp_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
pos : e ∈ M.E \ M.closure I ∨ e ∈ I ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)
pos₁ : e ∈ M.E \ M.closure I ∨ e ∈ I ↔ e ∉ I → e ∈ M.E \ M.closure I
⊢ M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)
have pos₂ : e ∉ I → e ∈ M.E \ M.closure I ↔ e ∉ I → e ∈ M.E \ M.closure I
Tactic: rw [hI.insert_indep_iff, and_iff_right hI, or_iff_not_imp_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep (I \ {e})
heI : e ∈ I
⊢ M.Indep (insert f I \ {e}) ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I
have inl : M.Indep (insert e I \ {e}) ↔ e ∈ M.E \ M.closure (I \ {e}) ∨ e ∈ I
Tactic: obtain rfl | hne := eq_or_ne e f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep (I \ {e})
heI : e ∈ I
inl : M.Indep (insert e I \ {e}) ↔ e ∈ M.E \ M.closure (I \ {e}) ∨ e ∈ I
⊢ M.Indep (insert f I \ {e}) ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I
have inr : ∀ (hne : e ≠ f), M.Indep (insert f I \ {e}) ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I
Tactic: obtain rfl | hne := eq_or_ne e f
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep (I \ {e})
heI : e ∈ I
hne : e ≠ f
⊢ M.Indep (insert f I \ {e}) ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I
have inr : M.Indep (insert f (I \ {e})) ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I
Tactic: rw [← insert_diff_singleton_comm hne.symm, hI.insert_indep_iff, mem_diff_singleton,
    and_iff_left hne.symm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep (I \ {e})
heI : e ∈ I
hne : e ≠ f
inr : M.Indep (insert f (I \ {e})) ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I
⊢ M.Indep (insert f I \ {e}) ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I
have inr₁ : f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I \ {e} ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I
Tactic: rw [← insert_diff_singleton_comm hne.symm, hI.insert_indep_iff, mem_diff_singleton,
    and_iff_left hne.symm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep (I \ {e})
heI : e ∈ I
hne : e ≠ f
inr : M.Indep (insert f (I \ {e})) ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I
inr₁ : f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I \ {e} ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I
⊢ M.Indep (insert f I \ {e}) ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I
have inr₂ : f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I ∧ f ≠ e ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I
Tactic: rw [← insert_diff_singleton_comm hne.symm, hI.insert_indep_iff, mem_diff_singleton,
    and_iff_left hne.symm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep (I \ {e})
heI : e ∈ I
hne : e ≠ f
inr : M.Indep (insert f (I \ {e})) ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I
inr₁ : f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I \ {e} ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I
inr₂ : f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I ∧ f ≠ e ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I
⊢ M.Indep (insert f I \ {e}) ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I
have inr₃ : f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I
Tactic: rw [← insert_diff_singleton_comm hne.symm, hI.insert_indep_iff, mem_diff_singleton,
    and_iff_left hne.symm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
h : M.E ⊆ M.closure I
⊢ M.IsBase I
have rw : M.IsBasis I M.E
Tactic: rw [← isBasis_ground_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
B : Set α
hB : M.IsBase B
⊢ M.closure B = M.E
have hB₁ : M.IsBasis B M.E
Tactic: rw [← isBasis_ground_iff] at hB
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
B : Set α
hB : M.IsBasis B M.E
⊢ M.closure B = M.E
have rw : M.closure M.E = M.E
Tactic: rw [hB.closure_eq_closure, closure_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
B : Set α
hB : M.IsBasis B M.E
rw : M.closure M.E = M.E
⊢ M.closure B = M.E
have rw₁ : M.E = M.E
Tactic: rw [hB.closure_eq_closure, closure_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
B : Set α
⊢ M.IsBase B ↔ M.Indep B ∧ M.closure B = M.E
have rw : M.Indep B → (B ⊆ M.E ∧ M.E ⊆ M.closure B ↔ M.closure B = M.E)
Tactic: rw [← isBasis_ground_iff, isBasis_iff_indep_subset_closure, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ M.closure (B \ {e})
hfE : f ∈ M.E
⊢ M.IsBase (insert f (B \ {e}))
have inl : ∀ (he : f ∈ B) (hf : f ∉ M.closure (B \ {f})), M.IsBase (insert f (B \ {f}))
Tactic: obtain rfl | hne := eq_or_ne f e
Cleared hypotheses: e, he, hf
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ M.closure (B \ {e})
hfE : f ∈ M.E
inl : ∀ (he : f ∈ B) (hf : f ∉ M.closure (B \ {f})), M.IsBase (insert f (B \ {f}))
⊢ M.IsBase (insert f (B \ {e}))
have inr : ∀ (hne : f ≠ e), M.IsBase (insert f (B \ {e}))
Tactic: obtain rfl | hne := eq_or_ne f e
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ M.closure (B \ {e})
hfE : f ∈ M.E
hne : f ≠ e
⊢ M.IsBase (insert f (B \ {e}))
have hi : M.Indep (insert f (B \ {e}))
Tactic: have ⟨hi, hfB⟩ : M.Indep (insert f (B \ {e})) ∧ f ∉ B := by
    simpa [(hB.indep.diff _).notMem_closure_iff, hne] using hf
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ M.closure (B \ {e})
hfE : f ∈ M.E
hne : f ≠ e
hi : M.Indep (insert f (B \ {e}))
⊢ M.IsBase (insert f (B \ {e}))
have hfB : f ∉ B
Tactic: have ⟨hi, hfB⟩ : M.Indep (insert f (B \ {e})) ∧ f ∉ B := by
    simpa [(hB.indep.diff _).notMem_closure_iff, hne] using hf
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJI : J ⊆ I
⊢ M.closure J ∩ I = J
have hJ : M.Indep J
Tactic: have hJ := hI.subset hJI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJI : J ⊆ I
hJ : M.Indep J
⊢ M.closure J ∩ I = J
have rw : M.closure J ∩ I ⊆ J
Tactic: rw [subset_antisymm_iff, and_iff_left (subset_inter (M.subset_closure _) hJI)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
⊢ M.closure (⋂₀ Js) = ⋂ J ∈ Js, M.closure J
have rw : (∀ (i : Set α) (j : i ∈ Js), M.closure (⋂₀ Js) ⊆ M.closure i) ∧ ⋂ J ∈ Js, M.closure J ⊆ M.closure (⋂₀ Js)
Tactic: rw [subset_antisymm_iff, subset_iInter₂_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
⊢ (∀ (i : Set α) (j : i ∈ Js), M.closure (⋂₀ Js) ⊆ M.closure i) ∧ ⋂ J ∈ Js, M.closure J ⊆ M.closure (⋂₀ Js)
have hiX : ⋂₀ Js ⊆ I
Tactic: have hiX : ⋂₀ Js ⊆ I := (sInter_subset_of_mem hne.some_mem).trans (hIs _ hne.some_mem)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
⊢ (∀ (i : Set α) (j : i ∈ Js), M.closure (⋂₀ Js) ⊆ M.closure i) ∧ ⋂ J ∈ Js, M.closure J ⊆ M.closure (⋂₀ Js)
have hiI : M.Indep (⋂₀ Js)
Tactic: have hiI := hI.subset hiX
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
⊢ (∀ (i : Set α) (j : i ∈ Js), M.closure (⋂₀ Js) ⊆ M.closure i) ∧ ⋂ J ∈ Js, M.closure J ⊆ M.closure (⋂₀ Js)
have refine : ∀ (e : α) (he : Membership.mem (γ := Set α) (⋂ J ∈ Js, M.closure J) e) (he' : e ∉ M.closure (⋂₀ Js)), False
Tactic: refine ⟨ fun X hX ↦ M.closure_subset_closure (sInter_subset_of_mem hX),
    fun e he ↦ by_contra fun he' ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : Membership.mem (γ := Set α) (⋂ J ∈ Js, M.closure J) e
he' : e ∉ M.closure (⋂₀ Js)
⊢ False
have he₁ : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
Tactic: rw [mem_iInter₂] at he
Cleared hypotheses: he, he'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : e ∉ M.closure (⋂₀ Js)
⊢ e ∈ M.E \ I
have refine : ∀ (heI : e ∈ I), e ∈ M.closure (⋂₀ Js)
Tactic: refine ⟨M.closure_subset_ground _ (he _ hne.some_mem), fun heI ↦ he' ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : e ∉ M.closure (⋂₀ Js)
heI : e ∈ I
⊢ e ∈ M.closure (⋂₀ Js)
have refine : ∀ (X : Set α) (hX' : X ∈ Js), e ∈ X
Tactic: refine mem_closure_of_mem _ (fun X hX' ↦ ?_) hiI.subset_ground
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : e ∉ M.closure (⋂₀ Js)
heI : e ∈ I
X : Set α
hX' : X ∈ Js
⊢ e ∈ X
have rw : e ∈ M.closure X ∩ I
Tactic: rw [← hI.closure_inter_eq_self_of_subset (hIs X hX')]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : e ∉ M.closure (⋂₀ Js)
⊢ False
have heEI : e ∈ M.E \ I
Tactic: have heEI : e ∈ M.E \ I := by
    refine ⟨M.closure_subset_ground _ (he _ hne.some_mem), fun heI ↦ he' ?_⟩
    refine mem_closure_of_mem _ (fun X hX' ↦ ?_) hiI.subset_ground
    rw [← hI.closure_inter_eq_self_of_subset (hIs X hX')]
    exact ⟨he X hX', heI⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : e ∉ M.closure (⋂₀ Js)
heEI : e ∈ M.E \ I
⊢ False
have he'₁ : M.Indep (insert e (⋂₀ Js))
Tactic: rw [hiI.notMem_closure_iff_of_notMem (notMem_subset hiX heEI.2)] at he'
Cleared hypotheses: he', heEI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
⊢ False
have obtain : ∀ (J : Set α) (hJI : M.IsBasis J (insert e I)) (heJ : insert e (⋂₀ Js) ⊆ J), False
Tactic: obtain ⟨J, hJI, heJ⟩ := he'.subset_isBasis_of_subset (insert_subset_insert hiX)
    (insert_subset heEI.1 hI.subset_ground)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.IsBasis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
⊢ M.IsBasis I (insert e I)
have rw : e ∈ M.closure I
Tactic: rw [hI.insert_isBasis_iff_mem_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.IsBasis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
⊢ False
have hIb : M.IsBasis I (insert e I)
Tactic: have hIb : M.IsBasis I (insert e I) := by
    rw [hI.insert_isBasis_iff_mem_closure]
    exact (M.closure_subset_closure (hIs _ hne.some_mem)) (he _ hne.some_mem)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.IsBasis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
hIb : M.IsBasis I (insert e I)
⊢ False
have obtain : ∀ (f : α) (hfIJ : f ∈ I \ J) (hfb : M.IsBasis (insert f (J \ {e})) (insert e I)), False
Tactic: obtain ⟨f, hfIJ, hfb⟩ := hJI.exchange hIb ⟨heJ (mem_insert e _), heEI.2⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.IsBasis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
hIb : M.IsBasis I (insert e I)
f : α
hfIJ : f ∈ I \ J
hfb : M.IsBasis (insert f (J \ {e})) (insert e I)
⊢ J \ {e} ⊆ I
have rw : J ⊆ insert e I
Tactic: rw [diff_subset_iff, singleton_union]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.IsBasis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
hIb : M.IsBasis I (insert e I)
f : α
hfIJ : f ∈ I \ J
hfb : M.IsBasis (insert f (J \ {e})) (insert e I)
⊢ False
have hI₁ : M.Indep (insert f (J \ {e}))
Tactic: obtain rfl := hI.eq_of_isBasis (hfb.isBasis_subset (insert_subset hfIJ.1
    (by (rw [diff_subset_iff, singleton_union]; exact hJI.subset))) (subset_insert _ _))
Cleared hypotheses: I, hI, hIs, hiX, heEI, hJI, hIb, hfIJ, hfb
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.IsBasis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
hIb : M.IsBasis I (insert e I)
f : α
hfIJ : f ∈ I \ J
hfb : M.IsBasis (insert f (J \ {e})) (insert e I)
hI₁ : M.Indep (insert f (J \ {e}))
⊢ False
have hIs₁ : ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})
Tactic: obtain rfl := hI.eq_of_isBasis (hfb.isBasis_subset (insert_subset hfIJ.1
    (by (rw [diff_subset_iff, singleton_union]; exact hJI.subset))) (subset_insert _ _))
Cleared hypotheses: I, hI, hIs, hiX, heEI, hJI, hIb, hfIJ, hfb
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.IsBasis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
hIb : M.IsBasis I (insert e I)
f : α
hfIJ : f ∈ I \ J
hfb : M.IsBasis (insert f (J \ {e})) (insert e I)
hI₁ : M.Indep (insert f (J \ {e}))
hIs₁ : ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})
⊢ False
have hiX₁ : ⋂₀ Js ⊆ insert f (J \ {e})
Tactic: obtain rfl := hI.eq_of_isBasis (hfb.isBasis_subset (insert_subset hfIJ.1
    (by (rw [diff_subset_iff, singleton_union]; exact hJI.subset))) (subset_insert _ _))
Cleared hypotheses: I, hI, hIs, hiX, heEI, hJI, hIb, hfIJ, hfb
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.IsBasis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
hIb : M.IsBasis I (insert e I)
f : α
hfIJ : f ∈ I \ J
hfb : M.IsBasis (insert f (J \ {e})) (insert e I)
hI₁ : M.Indep (insert f (J \ {e}))
hIs₁ : ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})
hiX₁ : ⋂₀ Js ⊆ insert f (J \ {e})
⊢ False
have heEI₁ : e ∈ M.E \ insert f (J \ {e})
Tactic: obtain rfl := hI.eq_of_isBasis (hfb.isBasis_subset (insert_subset hfIJ.1
    (by (rw [diff_subset_iff, singleton_union]; exact hJI.subset))) (subset_insert _ _))
Cleared hypotheses: I, hI, hIs, hiX, heEI, hJI, hIb, hfIJ, hfb
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.IsBasis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
hIb : M.IsBasis I (insert e I)
f : α
hfIJ : f ∈ I \ J
hfb : M.IsBasis (insert f (J \ {e})) (insert e I)
hI₁ : M.Indep (insert f (J \ {e}))
hIs₁ : ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})
hiX₁ : ⋂₀ Js ⊆ insert f (J \ {e})
heEI₁ : e ∈ M.E \ insert f (J \ {e})
⊢ False
have hJI₁ : M.IsBasis J (insert e (insert f (J \ {e})))
Tactic: obtain rfl := hI.eq_of_isBasis (hfb.isBasis_subset (insert_subset hfIJ.1
    (by (rw [diff_subset_iff, singleton_union]; exact hJI.subset))) (subset_insert _ _))
Cleared hypotheses: I, hI, hIs, hiX, heEI, hJI, hIb, hfIJ, hfb