awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
⊢ M.Indep I ↔ ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
have rw : (I ⊆ M.E ∧ ∀ e ∈ I, e ∉ M.closure (I \ {e})) ↔ ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
Tactic: rw [indep_iff_forall_notMem_closure_diff']
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
⊢ (I ⊆ M.E ∧ ∀ e ∈ I, e ∉ M.closure (I \ {e})) ↔ ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
have refine_1 : ∀ (h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I) (e : α) (heI : e ∈ I) (heE : e ∉ M.E),
  M.closure (I \ {e}) = M.closure I
Tactic: refine ⟨fun ⟨hIE, h⟩ e heI h_eq ↦ h e heI (h_eq.symm.subset (M.mem_closure_of_mem heI)),
    fun h ↦ ⟨fun e heI ↦ by_contra fun heE ↦ h heI ?_,fun e heI hin ↦ h heI ?_⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
refine_1 :
  ∀ (h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I) (e : α) (heI : e ∈ I) (heE : e ∉ M.E),
    M.closure (I \ {e}) = M.closure I
⊢ (I ⊆ M.E ∧ ∀ e ∈ I, e ∉ M.closure (I \ {e})) ↔ ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
have refine_2 : ∀ (h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I) (e : α) (heI : e ∈ I) (hin : e ∈ M.closure (I \ {e})),
  M.closure (I \ {e}) = M.closure I
Tactic: refine ⟨fun ⟨hIE, h⟩ e heI h_eq ↦ h e heI (h_eq.symm.subset (M.mem_closure_of_mem heI)),
    fun h ↦ ⟨fun e heI ↦ by_contra fun heE ↦ h heI ?_,fun e heI hin ↦ h heI ?_⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
heE : e ∉ M.E
⊢ M.closure (I \ {e}) = M.closure I
have refine_1 : M.closure (I \ {e} ∩ M.E) = M.closure I
Tactic: rw [← closure_inter_ground, inter_comm, inter_diff_distrib_left,
      inter_singleton_eq_empty.mpr heE, diff_empty, inter_comm, closure_inter_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
heE : e ∉ M.E
refine_1 : M.closure (I \ {e} ∩ M.E) = M.closure I
⊢ M.closure (I \ {e}) = M.closure I
have refine_1₁ : M.closure (M.E ∩ (I \ {e})) = M.closure I
Tactic: rw [← closure_inter_ground, inter_comm, inter_diff_distrib_left,
      inter_singleton_eq_empty.mpr heE, diff_empty, inter_comm, closure_inter_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
heE : e ∉ M.E
refine_1 : M.closure (I \ {e} ∩ M.E) = M.closure I
refine_1₁ : M.closure (M.E ∩ (I \ {e})) = M.closure I
⊢ M.closure (I \ {e}) = M.closure I
have refine_1₂ : M.closure ((M.E ∩ I) \ (M.E ∩ {e})) = M.closure I
Tactic: rw [← closure_inter_ground, inter_comm, inter_diff_distrib_left,
      inter_singleton_eq_empty.mpr heE, diff_empty, inter_comm, closure_inter_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
heE : e ∉ M.E
refine_1 : M.closure (I \ {e} ∩ M.E) = M.closure I
refine_1₁ : M.closure (M.E ∩ (I \ {e})) = M.closure I
refine_1₂ : M.closure ((M.E ∩ I) \ (M.E ∩ {e})) = M.closure I
⊢ M.closure (I \ {e}) = M.closure I
have refine_1₃ : M.closure ((M.E ∩ I) \ ∅) = M.closure I
Tactic: rw [← closure_inter_ground, inter_comm, inter_diff_distrib_left,
      inter_singleton_eq_empty.mpr heE, diff_empty, inter_comm, closure_inter_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
heE : e ∉ M.E
refine_1 : M.closure (I \ {e} ∩ M.E) = M.closure I
refine_1₁ : M.closure (M.E ∩ (I \ {e})) = M.closure I
refine_1₂ : M.closure ((M.E ∩ I) \ (M.E ∩ {e})) = M.closure I
refine_1₃ : M.closure ((M.E ∩ I) \ ∅) = M.closure I
⊢ M.closure (I \ {e}) = M.closure I
have refine_1₄ : M.closure (M.E ∩ I) = M.closure I
Tactic: rw [← closure_inter_ground, inter_comm, inter_diff_distrib_left,
      inter_singleton_eq_empty.mpr heE, diff_empty, inter_comm, closure_inter_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
heE : e ∉ M.E
refine_1 : M.closure (I \ {e} ∩ M.E) = M.closure I
refine_1₁ : M.closure (M.E ∩ (I \ {e})) = M.closure I
refine_1₂ : M.closure ((M.E ∩ I) \ (M.E ∩ {e})) = M.closure I
refine_1₃ : M.closure ((M.E ∩ I) \ ∅) = M.closure I
refine_1₄ : M.closure (M.E ∩ I) = M.closure I
⊢ M.closure (I \ {e}) = M.closure I
have refine_1₅ : M.closure (I ∩ M.E) = M.closure I
Tactic: rw [← closure_inter_ground, inter_comm, inter_diff_distrib_left,
      inter_singleton_eq_empty.mpr heE, diff_empty, inter_comm, closure_inter_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
heE : e ∉ M.E
refine_1 : M.closure (I \ {e} ∩ M.E) = M.closure I
refine_1₁ : M.closure (M.E ∩ (I \ {e})) = M.closure I
refine_1₂ : M.closure ((M.E ∩ I) \ (M.E ∩ {e})) = M.closure I
refine_1₃ : M.closure ((M.E ∩ I) \ ∅) = M.closure I
refine_1₄ : M.closure (M.E ∩ I) = M.closure I
refine_1₅ : M.closure (I ∩ M.E) = M.closure I
⊢ M.closure (I \ {e}) = M.closure I
have refine_1₆ : M.closure I = M.closure I
Tactic: rw [← closure_inter_ground, inter_comm, inter_diff_distrib_left,
      inter_singleton_eq_empty.mpr heE, diff_empty, inter_comm, closure_inter_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
hin : e ∈ M.closure (I \ {e})
⊢ M.closure (I \ {e}) = M.closure I
have refine_2 : M.closure (I \ {e}) = M.closure (insert e (I \ {e}))
Tactic: nth_rw 2 [show I = insert e (I \ {e}) by simp [heI]]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
hin : e ∈ M.closure (I \ {e})
⊢ M.closure (I \ {e}) = M.closure (insert e (I \ {e}))
have refine_2 : M.closure (I \ {e}) = M.closure (insert e (M.closure (I \ {e})))
Tactic: rw [← closure_insert_closure_eq_closure_insert, insert_eq_of_mem hin, closure_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
hin : e ∈ M.closure (I \ {e})
refine_2 : M.closure (I \ {e}) = M.closure (insert e (M.closure (I \ {e})))
⊢ M.closure (I \ {e}) = M.closure (insert e (I \ {e}))
have refine_2₁ : M.closure (I \ {e}) = M.closure (M.closure (I \ {e}))
Tactic: rw [← closure_insert_closure_eq_closure_insert, insert_eq_of_mem hin, closure_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
hin : e ∈ M.closure (I \ {e})
refine_2 : M.closure (I \ {e}) = M.closure (insert e (M.closure (I \ {e})))
refine_2₁ : M.closure (I \ {e}) = M.closure (M.closure (I \ {e}))
⊢ M.closure (I \ {e}) = M.closure (insert e (I \ {e}))
have refine_2₂ : M.closure (I \ {e}) = M.closure (I \ {e})
Tactic: rw [← closure_insert_closure_eq_closure_insert, insert_eq_of_mem hin, closure_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
⊢ M.Indep (I ∪ J) ↔ ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
have refine_1 : ∀ (h : M.Indep (I ∪ J)) (e : α) (heJ : e ∈ J \ I) (hecl : e ∈ M.closure (I ∪ J \ {e})), e ∈ M.closure ((I ∪ J) \ {e})
Tactic: refine ⟨fun h e heJ hecl ↦ h.notMem_closure_diff_of_mem (.inr heJ.1) ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
refine_1 :
  ∀ (h : M.Indep (I ∪ J)) (e : α) (heJ : e ∈ J \ I) (hecl : e ∈ M.closure (I ∪ J \ {e})), e ∈ M.closure ((I ∪ J) \ {e})
⊢ M.Indep (I ∪ J) ↔ ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
have refine_2 : ∀ (h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})), M.Indep (I ∪ J)
Tactic: refine ⟨fun h e heJ hecl ↦ h.notMem_closure_diff_of_mem (.inr heJ.1) ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : M.Indep (I ∪ J)
e : α
heJ : e ∈ J \ I
hecl : e ∈ M.closure (I ∪ J \ {e})
⊢ e ∈ M.closure ((I ∪ J) \ {e})
have refine_1 : e ∈ M.closure (I \ {e} ∪ J \ {e})
Tactic: rwa [union_diff_distrib, diff_singleton_eq_self heJ.2]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
⊢ M.Indep (I ∪ J)
have refine_2 : ∀ (K : Set α) (hKIJ : M.IsBasis K (I ∪ J)) (hK : I ⊆ K), M.Indep (I ∪ J)
Tactic: obtain ⟨K, hKIJ, hK⟩ := hI.subset_isBasis_of_subset (show I ⊆ I ∪ J from subset_union_left)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
K : Set α
hKIJ : M.IsBasis K (I ∪ J)
hK : I ⊆ K
⊢ M.Indep (I ∪ J)
have refine_2 : ∀ (hKIJ : M.IsBasis (I ∪ J) (I ∪ J)) (hK : I ⊆ I ∪ J), M.Indep (I ∪ J)
Tactic: obtain rfl | hssu := hKIJ.subset.eq_or_ssubset
Cleared hypotheses: K, hKIJ, hK
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
K : Set α
hKIJ : M.IsBasis K (I ∪ J)
hK : I ⊆ K
refine_2 : ∀ (hKIJ : M.IsBasis (I ∪ J) (I ∪ J)) (hK : I ⊆ I ∪ J), M.Indep (I ∪ J)
⊢ M.Indep (I ∪ J)
have refine_2₁ : ∀ (hssu : K ⊂ I ∪ J), M.Indep (I ∪ J)
Tactic: obtain rfl | hssu := hKIJ.subset.eq_or_ssubset
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
K : Set α
hKIJ : M.IsBasis K (I ∪ J)
hK : I ⊆ K
hssu : K ⊂ I ∪ J
⊢ M.Indep (I ∪ J)
have refine_2 : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
K : Set α
hKIJ : M.IsBasis K (I ∪ J)
hK : I ⊆ K
hssu : K ⊂ I ∪ J
⊢ False
have refine_2 : ∀ (e : α) (heI : e ∈ I ∪ J) (heK : e ∉ K), False
Tactic: obtain ⟨e, heI, heK⟩ := exists_of_ssubset hssu
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
K : Set α
hKIJ : M.IsBasis K (I ∪ J)
hK : I ⊆ K
hssu : K ⊂ I ∪ J
e : α
heI : e ∈ I ∪ J
heK : e ∉ K
⊢ e ∈ J \ I
have rw : e ∈ (I ∪ J) \ I
Tactic: rw [← union_diff_right, union_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
K : Set α
hKIJ : M.IsBasis K (I ∪ J)
hK : I ⊆ K
hssu : K ⊂ I ∪ J
e : α
heI : e ∈ I ∪ J
heK : e ∉ K
⊢ False
have heJI : e ∈ J \ I
Tactic: have heJI : e ∈ J \ I := by
    rw [← union_diff_right, union_comm]
    exact ⟨heI, notMem_subset hK heK⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
K : Set α
hKIJ : M.IsBasis K (I ∪ J)
hK : I ⊆ K
hssu : K ⊂ I ∪ J
e : α
heI : e ∈ I ∪ J
heK : e ∉ K
heJI : e ∈ J \ I
⊢ False
have refine_2 : e ∈ M.closure (I ∪ J \ {e})
Tactic: refine h _ heJI ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
K : Set α
hKIJ : M.IsBasis K (I ∪ J)
hK : I ⊆ K
hssu : K ⊂ I ∪ J
e : α
heI : e ∈ I ∪ J
heK : e ∉ K
heJI : e ∈ J \ I
⊢ e ∈ M.closure (I ∪ J \ {e})
have refine_2 : e ∈ M.closure ((I ∪ J) \ {e})
Tactic: rw [← diff_singleton_eq_self heJI.2, ← union_diff_distrib]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
⊢ M.Indep (I ∪ J) ↔ ∀ e ∈ I \ J, e ∉ M.closure (I \ {e} ∪ J)
have simp_rw : M.Indep (J ∪ I) ↔ ∀ e ∈ I \ J, e ∉ M.closure (I \ {e} ∪ J)
Tactic: simp_rw [union_comm I J, hJ.union_indep_iff_forall_notMem_closure_right hI, union_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
simp_rw : M.Indep (J ∪ I) ↔ ∀ e ∈ I \ J, e ∉ M.closure (I \ {e} ∪ J)
⊢ M.Indep (I ∪ J) ↔ ∀ e ∈ I \ J, e ∉ M.closure (I \ {e} ∪ J)
have simp_rw₁ : (∀ e ∈ I \ J, e ∉ M.closure (J ∪ I \ {e})) ↔ ∀ e ∈ I \ J, e ∉ M.closure (I \ {e} ∪ J)
Tactic: simp_rw [union_comm I J, hJ.union_indep_iff_forall_notMem_closure_right hI, union_comm]
-- 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
⊢ M.closure J ⊂ M.closure I
have obtain : ∀ (e : α) (heI : e ∈ I) (heJ : e ∉ J), M.closure J ⊂ M.closure I
Tactic: obtain ⟨e, heI, heJ⟩ := exists_of_ssubset hJI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
⊢ M.Indep I ↔ ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I
have refine : ∀ (h : ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I) (e : α) (heI : e ∈ I) (hecl : e ∈ M.closure (I \ {e})), False
Tactic: refine ⟨fun h _ ↦ h.closure_ssubset_closure,
    fun h ↦ (indep_iff_forall_notMem_closure_diff hI).2 fun e heI hecl ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
h : ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I
e : α
heI : e ∈ I
hecl : e ∈ M.closure (I \ {e})
⊢ False
have refine : M.closure (I \ {e}) = M.closure I
Tactic: refine (h (diff_singleton_ssubset.2 heI)).ne ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
h : ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I
e : α
heI : e ∈ I
hecl : e ∈ M.closure (I \ {e})
⊢ M.closure (I \ {e}) = M.closure I
have rw : M.closure (insert e (I \ {e}) \ {e}) = M.closure (M.closure (I \ {e}))
Tactic: rw [show I = insert e (I \ {e}) by simp [heI], ← closure_insert_closure_eq_closure_insert,
    insert_eq_of_mem hecl]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X I : Set α
hI : M.Indep I
hX : (I ∩ X).Nonempty
⊢ M.closure (I \ X) ⊂ M.closure I
have refine : ∀ (h : I \ X = I), False
Tactic: refine hI.closure_ssubset_closure <| diff_subset.ssubset_of_ne fun h ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
X I : Set α
hI : M.Indep I
hX : (I ∩ X).Nonempty
h : I \ X = I
⊢ False
have h₁ : I ∩ X = ∅
Tactic: rw [sdiff_eq_left, disjoint_iff_inter_eq_empty] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure X
hef : e ∈ M.closure (insert f X)
⊢ f ∈ M.closure (insert e X)
have rw : ∀ (he : e ∉ M.closure (X ∩ M.E)) (hef : e ∈ M.closure (insert f X ∩ M.E)), f ∈ M.closure (insert e X ∩ M.E)
Tactic: rw [← closure_inter_ground] at *
Cleared hypotheses: he, hef
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure (X ∩ M.E)
hef : e ∈ M.closure (insert f X ∩ M.E)
⊢ f ∈ M.E
have by_contra! : ∀ (hfE : f ∉ M.E), False
Tactic: by_contra! hfE
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure (X ∩ M.E)
hef : e ∈ M.closure (insert f X ∩ M.E)
hfE : f ∉ M.E
⊢ False
have hef₁ : e ∈ M.closure (X ∩ M.E)
Tactic: rw [insert_inter_of_notMem hfE] at hef
Cleared hypotheses: hef, hfE
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure (X ∩ M.E)
hef : e ∈ M.closure (insert f X ∩ M.E)
⊢ f ∈ M.closure (insert e X ∩ M.E)
have hfE : f ∈ M.E
Tactic: have hfE : f ∈ M.E := by
    by_contra! hfE; rw [insert_inter_of_notMem hfE] at hef; exact he hef
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure (X ∩ M.E)
hef : e ∈ M.closure (insert f X ∩ M.E)
hfE : f ∈ M.E
⊢ f ∈ M.closure (insert e X ∩ M.E)
have heE : e ∈ M.E
Tactic: have heE : e ∈ M.E := (M.closure_subset_ground _) hef
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure (X ∩ M.E)
hef : e ∈ M.closure (insert f X ∩ M.E)
hfE : f ∈ M.E
heE : e ∈ M.E
⊢ f ∈ M.closure (insert e X ∩ M.E)
have hef₁ : e ∈ M.closure (insert f (X ∩ M.E))
Tactic: rw [insert_inter_of_mem hfE] at hef
Cleared hypotheses: hef, hfE, heE
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure (X ∩ M.E)
hef : e ∈ M.closure (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
⊢ f ∈ M.closure (insert e X ∩ M.E)
have rw : f ∈ M.closure (insert e (X ∩ M.E))
Tactic: rw [insert_inter_of_mem heE]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure (X ∩ M.E)
hef : e ∈ M.closure (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
⊢ f ∈ M.closure (insert e (X ∩ M.E))
have obtain : ∀ (I : Set α) (hI : M.IsBasis I (X ∩ M.E)), f ∈ M.closure (insert e (X ∩ M.E))
Tactic: obtain ⟨I, hI⟩ := M.exists_isBasis (X ∩ M.E)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure (X ∩ M.E)
hef : e ∈ M.closure (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hI : M.IsBasis I (X ∩ M.E)
⊢ f ∈ M.closure (insert e (X ∩ M.E))
have he₁ : M.Indep (insert e I) ∧ e ∉ I
Tactic: rw [← hI.closure_eq_closure, hI.indep.notMem_closure_iff] at he
Cleared hypotheses: he, hI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
hef : e ∈ M.closure (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.IsBasis I (X ∩ M.E)
⊢ f ∈ M.closure (insert e (X ∩ M.E))
have rw : ∀ (hfE : f ∈ M.E) (heE : e ∈ M.E) (I : Set α) (hef : e ∈ M.closure (insert f I)) (he : M.Indep (insert e I) ∧ e ∉ I)
  (hI : M.IsBasis I (X ∩ M.E)), M.Dep (insert f (insert e I)) ∨ f ∈ insert e I
Tactic: rw [← closure_insert_closure_eq_closure_insert, ← hI.closure_eq_closure,
    closure_insert_closure_eq_closure_insert, he.1.mem_closure_iff] at *
Cleared hypotheses: hef, hfE, heE, I, he, hI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hef : e ∈ M.closure (insert f I)
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.IsBasis I (X ∩ M.E)
⊢ M.Dep (insert f (insert e I)) ∨ f ∈ insert e I
have rw : M.Indep (insert e (insert f I)) → f ∈ insert e I
Tactic: rw [or_iff_not_imp_left, dep_iff, insert_comm,
    and_iff_left (insert_subset heE (insert_subset hfE hI.indep.subset_ground)), not_not]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hef : e ∈ M.closure (insert f I)
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.IsBasis I (X ∩ M.E)
h : M.Indep (insert e (insert f I))
⊢ f ∈ insert e I
have hef₁ : e = f
Tactic: rw [(h.subset (subset_insert _ _)).mem_closure_iff, or_iff_right (h.not_dep), mem_insert_iff,
    or_iff_left he.2] at hef
Cleared hypotheses: hef, he, hI, h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hef : e = f
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.IsBasis I (X ∩ M.E)
h : M.Indep (insert e (insert f I))
⊢ f ∈ insert e I
have subst : ∀ (hfE : e ∈ M.E) (h : M.Indep (insert e (insert e I))), e ∈ insert e I
Tactic: subst hef
Cleared hypotheses: f, hfE, hef, h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∈ M.closure (insert f X) \ M.closure X
hf : f ∈ M.closure X
⊢ False
have rwa : ∀ (he : e ∈ M.closure X \ M.closure X) (hf : f ∈ M.closure X), False
Tactic: rwa [closure_insert_eq_of_mem_closure hf, diff_self, iff_false_intro (notMem_empty _)] at he
Cleared hypotheses: he, hf
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∈ M.closure (insert f X) \ M.closure X
hf : f ∈ M.closure X
rwa : ∀ (he : e ∈ M.closure X \ M.closure X) (hf : f ∈ M.closure X), False
⊢ False
have rwa₁ : ∀ (he : Membership.mem (γ := Set α) ∅ e) (hf : f ∈ M.closure X), False
Tactic: rwa [closure_insert_eq_of_mem_closure hf, diff_self, iff_false_intro (notMem_empty _)] at he
Cleared hypotheses: he, hf
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∈ M.closure (insert f X) \ M.closure X
hf : f ∈ M.closure X
rwa : ∀ (he : e ∈ M.closure X \ M.closure X) (hf : f ∈ M.closure X), False
rwa₁ : ∀ (he : Membership.mem (γ := Set α) ∅ e) (hf : f ∈ M.closure X), False
⊢ False
have rwa₂ : ∀ (he : False) (hf : f ∈ M.closure X), False
Tactic: rwa [closure_insert_eq_of_mem_closure hf, diff_self, iff_false_intro (notMem_empty _)] at he
Cleared hypotheses: he, hf
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∈ M.closure (insert f X) \ M.closure X
⊢ M.closure (insert e X) = M.closure (insert f X)
have hf : f ∈ M.closure (insert e X) \ M.closure X
Tactic: have hf := closure_exchange he
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∈ M.closure (insert f X) \ M.closure X
hf : f ∈ M.closure (insert e X) \ M.closure X
⊢ M.closure (insert e X) = M.closure (insert f X)
have rw : M.closure (insert f X) = M.closure (insert e X)
Tactic: rw [eq_comm, ← closure_closure, ← insert_eq_of_mem he.1, closure_insert_closure_eq_closure_insert,
    insert_comm, ← closure_closure, ← closure_insert_closure_eq_closure_insert,
    insert_eq_of_mem hf.1, closure_closure, closure_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∈ M.closure (insert f X) \ M.closure X
hf : f ∈ M.closure (insert e X) \ M.closure X
rw : M.closure (insert f X) = M.closure (insert e X)
⊢ M.closure (insert e X) = M.closure (insert f X)
have rw₁ : M.closure (M.closure (insert f X)) = M.closure (insert e X)
Tactic: rw [eq_comm, ← closure_closure, ← insert_eq_of_mem he.1, closure_insert_closure_eq_closure_insert,
    insert_comm, ← closure_closure, ← closure_insert_closure_eq_closure_insert,
    insert_eq_of_mem hf.1, closure_closure, closure_closure]