awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
ι : Type u_1
α : Type u_2
M : Matroid α
Xs Ys : ι → Set α
A : Set ι
h : ∀ i ∈ A, M.closure (Xs i) = M.closure (Ys i)
⊢ M.closure (⋃ i ∈ A, Xs i) = M.closure (⋃ i ∈ A, Ys i)
have rw : M.closure (⋃ i ∈ A, M.closure (Xs i)) = M.closure (⋃ i ∈ A, Ys i)
Tactic: rw [← closure_biUnion_closure_eq_closure_biUnion, iUnion₂_congr h,
    closure_biUnion_closure_eq_closure_biUnion]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
ι : Type u_1
α : Type u_2
M : Matroid α
Xs Ys : ι → Set α
A : Set ι
h : ∀ i ∈ A, M.closure (Xs i) = M.closure (Ys i)
rw : M.closure (⋃ i ∈ A, M.closure (Xs i)) = M.closure (⋃ i ∈ A, Ys i)
⊢ M.closure (⋃ i ∈ A, Xs i) = M.closure (⋃ i ∈ A, Ys i)
have rw₁ : M.closure (⋃ i ∈ A, M.closure (Ys i)) = M.closure (⋃ i ∈ A, Ys i)
Tactic: rw [← closure_biUnion_closure_eq_closure_biUnion, iUnion₂_congr h,
    closure_biUnion_closure_eq_closure_biUnion]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
ι : Type u_1
α : Type u_2
M : Matroid α
Xs Ys : ι → Set α
A : Set ι
h : ∀ i ∈ A, M.closure (Xs i) = M.closure (Ys i)
rw : M.closure (⋃ i ∈ A, M.closure (Xs i)) = M.closure (⋃ i ∈ A, Ys i)
rw₁ : M.closure (⋃ i ∈ A, M.closure (Ys i)) = M.closure (⋃ i ∈ A, Ys i)
⊢ M.closure (⋃ i ∈ A, Xs i) = M.closure (⋃ i ∈ A, Ys i)
have rw₂ : M.closure (⋃ i ∈ A, Ys i) = M.closure (⋃ i ∈ A, Ys i)
Tactic: rw [← closure_biUnion_closure_eq_closure_biUnion, iUnion₂_congr h,
    closure_biUnion_closure_eq_closure_biUnion]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X Y : Set α
⊢ M.closure (M.closure X ∪ M.closure Y) = M.closure (X ∪ Y)
have rw : M.closure (⋃ (i : Bool), M.closure (bif i then X else Y)) =
  M.closure (⋃ (b : Bool), bif b then M.closure X else M.closure Y)
Tactic: rw [eq_comm, union_eq_iUnion, ← closure_iUnion_closure_eq_closure_iUnion, union_eq_iUnion]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X Y : Set α
⊢ M.closure (⋃ (i : Bool), M.closure (bif i then X else Y)) =
    M.closure (⋃ (b : Bool), bif b then M.closure X else M.closure Y)
have simp_rw : M.closure (⋃ (i : Bool), M.closure (if i = true then X else Y)) =
  M.closure (⋃ (b : Bool), if b = true then M.closure X else M.closure Y)
Tactic: simp_rw [Bool.cond_eq_ite, apply_ite]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X Y : Set α
⊢ M.closure (X ∪ M.closure Y) = M.closure (X ∪ Y)
have rw : M.closure (M.closure X ∪ M.closure (M.closure Y)) = M.closure (X ∪ Y)
Tactic: rw [← closure_closure_union_closure_eq_closure_union, closure_closure,
    closure_closure_union_closure_eq_closure_union]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X Y : Set α
rw : M.closure (M.closure X ∪ M.closure (M.closure Y)) = M.closure (X ∪ Y)
⊢ M.closure (X ∪ M.closure Y) = M.closure (X ∪ Y)
have rw₁ : M.closure (M.closure X ∪ M.closure Y) = M.closure (X ∪ Y)
Tactic: rw [← closure_closure_union_closure_eq_closure_union, closure_closure,
    closure_closure_union_closure_eq_closure_union]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X Y : Set α
rw : M.closure (M.closure X ∪ M.closure (M.closure Y)) = M.closure (X ∪ Y)
rw₁ : M.closure (M.closure X ∪ M.closure Y) = M.closure (X ∪ Y)
⊢ M.closure (X ∪ M.closure Y) = M.closure (X ∪ Y)
have rw₂ : M.closure (X ∪ Y) = M.closure (X ∪ Y)
Tactic: rw [← closure_closure_union_closure_eq_closure_union, closure_closure,
    closure_closure_union_closure_eq_closure_union]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X Y : Set α
⊢ M.closure (M.closure X ∪ Y) = M.closure (X ∪ Y)
have rw : M.closure (M.closure (M.closure X) ∪ M.closure Y) = M.closure (X ∪ Y)
Tactic: rw [← closure_closure_union_closure_eq_closure_union, closure_closure,
    closure_closure_union_closure_eq_closure_union]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X Y : Set α
rw : M.closure (M.closure (M.closure X) ∪ M.closure Y) = M.closure (X ∪ Y)
⊢ M.closure (M.closure X ∪ Y) = M.closure (X ∪ Y)
have rw₁ : M.closure (M.closure X ∪ M.closure Y) = M.closure (X ∪ Y)
Tactic: rw [← closure_closure_union_closure_eq_closure_union, closure_closure,
    closure_closure_union_closure_eq_closure_union]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X Y : Set α
rw : M.closure (M.closure (M.closure X) ∪ M.closure Y) = M.closure (X ∪ Y)
rw₁ : M.closure (M.closure X ∪ M.closure Y) = M.closure (X ∪ Y)
⊢ M.closure (M.closure X ∪ Y) = M.closure (X ∪ Y)
have rw₂ : M.closure (X ∪ Y) = M.closure (X ∪ Y)
Tactic: rw [← closure_closure_union_closure_eq_closure_union, closure_closure,
    closure_closure_union_closure_eq_closure_union]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X Y X' : Set α
h : M.closure X = M.closure X'
⊢ M.closure (X ∪ Y) = M.closure (X' ∪ Y)
have rw : M.closure (M.closure X ∪ Y) = M.closure (X' ∪ Y)
Tactic: rw [← M.closure_union_closure_left_eq, h, M.closure_union_closure_left_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X Y X' : Set α
h : M.closure X = M.closure X'
rw : M.closure (M.closure X ∪ Y) = M.closure (X' ∪ Y)
⊢ M.closure (X ∪ Y) = M.closure (X' ∪ Y)
have rw₁ : M.closure (M.closure X' ∪ Y) = M.closure (X' ∪ Y)
Tactic: rw [← M.closure_union_closure_left_eq, h, M.closure_union_closure_left_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X Y X' : Set α
h : M.closure X = M.closure X'
rw : M.closure (M.closure X ∪ Y) = M.closure (X' ∪ Y)
rw₁ : M.closure (M.closure X' ∪ Y) = M.closure (X' ∪ Y)
⊢ M.closure (X ∪ Y) = M.closure (X' ∪ Y)
have rw₂ : M.closure (X' ∪ Y) = M.closure (X' ∪ Y)
Tactic: rw [← M.closure_union_closure_left_eq, h, M.closure_union_closure_left_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X Y Y' : Set α
h : M.closure Y = M.closure Y'
⊢ M.closure (X ∪ Y) = M.closure (X ∪ Y')
have rw : M.closure (X ∪ M.closure Y) = M.closure (X ∪ Y')
Tactic: rw [← M.closure_union_closure_right_eq, h, M.closure_union_closure_right_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X Y Y' : Set α
h : M.closure Y = M.closure Y'
rw : M.closure (X ∪ M.closure Y) = M.closure (X ∪ Y')
⊢ M.closure (X ∪ Y) = M.closure (X ∪ Y')
have rw₁ : M.closure (X ∪ M.closure Y') = M.closure (X ∪ Y')
Tactic: rw [← M.closure_union_closure_right_eq, h, M.closure_union_closure_right_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X Y Y' : Set α
h : M.closure Y = M.closure Y'
rw : M.closure (X ∪ M.closure Y) = M.closure (X ∪ Y')
rw₁ : M.closure (X ∪ M.closure Y') = M.closure (X ∪ Y')
⊢ M.closure (X ∪ Y) = M.closure (X ∪ Y')
have rw₂ : M.closure (X ∪ Y') = M.closure (X ∪ Y')
Tactic: rw [← M.closure_union_closure_right_eq, h, M.closure_union_closure_right_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
e : α
he : e ∈ M.closure X
⊢ M.closure (insert e X) = M.closure X
have rw : M.closure (insert e (M.closure X)) = M.closure X
Tactic: rw [← closure_insert_closure_eq_closure_insert, insert_eq_of_mem he, closure_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
e : α
he : e ∈ M.closure X
rw : M.closure (insert e (M.closure X)) = M.closure X
⊢ M.closure (insert e X) = M.closure X
have rw₁ : M.closure (M.closure X) = M.closure X
Tactic: rw [← closure_insert_closure_eq_closure_insert, insert_eq_of_mem he, closure_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X : Set α
e : α
he : e ∈ M.closure X
rw : M.closure (insert e (M.closure X)) = M.closure X
rw₁ : M.closure (M.closure X) = M.closure X
⊢ M.closure (insert e X) = M.closure X
have rw₂ : M.closure X = M.closure X
Tactic: rw [← closure_insert_closure_eq_closure_insert, insert_eq_of_mem he, closure_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x : α | M.IsBasis I (insert x I)}
⊢ M.closure I = F
have hIF : M.IsBasis I F
Tactic: have hIF : M.IsBasis I F := hI.isBasis_setOf_insert_isBasis
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x : α | M.IsBasis I (insert x I)}
hIF : M.IsBasis I F
⊢ M.IsFlat F
have refine : ∀ (J X : Set α) (hJF : M.IsBasis J F) (hJX : M.IsBasis J X) (e : α) (heX : e ∈ X), M.IsBasis I (insert e I)
Tactic: refine ⟨fun J X hJF hJX e heX ↦ show M.IsBasis _ _ from ?_, hIF.subset_ground⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x : α | M.IsBasis I (insert x I)}
hIF : M.IsBasis I F
⊢ M.closure I = F
have hF : M.IsFlat F
Tactic: have hF : M.IsFlat F := by
    refine ⟨fun J X hJF hJX e heX ↦ show M.IsBasis _ _ from ?_, hIF.subset_ground⟩
    exact (hIF.isBasis_of_isBasis_of_subset_of_subset (hJX.isBasis_union hJF) hJF.subset
      (hIF.subset.trans subset_union_right)).isBasis_subset (subset_insert _ _)
      (insert_subset (Or.inl heX) (hIF.subset.trans subset_union_right))
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x : α | M.IsBasis I (insert x I)}
hIF : M.IsBasis I F
hF : M.IsFlat F
⊢ M.closure I = F
have rw : ∀ (t' : Set α), Membership.mem (γ := Set (Set α)) {F : Set α | M.IsFlat F ∧ I ∩ M.E ⊆ F} t' → F ⊆ t'
Tactic: rw [subset_antisymm_iff, closure_def, subset_sInter_iff, and_iff_right (sInter_subset_of_mem _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x : α | M.IsBasis I (insert x I)}
hIF : M.IsBasis I F
hF : M.IsFlat F
rw : ∀ (t' : Set α), Membership.mem (γ := Set (Set α)) {F : Set α | M.IsFlat F ∧ I ∩ M.E ⊆ F} t' → F ⊆ t'
⊢ M.closure I = F
have rw₁ : Membership.mem (γ := Set (Set α)) {F : Set α | M.IsFlat F ∧ I ∩ M.E ⊆ F} F
Tactic: rw [subset_antisymm_iff, closure_def, subset_sInter_iff, and_iff_right (sInter_subset_of_mem _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x : α | M.IsBasis I (insert x I)}
hIF : M.IsBasis I F
hF : M.IsFlat F
F' : Set α
hF' : M.IsFlat F'
hIF' : I ∩ M.E ⊆ F'
e : α
he : M.IsBasis I (insert e I)
⊢ e ∈ F'
have rw : ∀ (hIF' : I ⊆ F') ⦃e : α⦄ (he : M.IsBasis I (insert e I)), e ∈ F'
Tactic: rw [inter_eq_left.mpr (hIF.subset.trans hIF.subset_ground)] at hIF'
Cleared hypotheses: hIF', e, he
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x : α | M.IsBasis I (insert x I)}
hIF : M.IsBasis I F
hF : M.IsFlat F
F' : Set α
hF' : M.IsFlat F'
hIF' : I ⊆ F'
e : α
he : M.IsBasis I (insert e I)
⊢ e ∈ F'
have obtain : ∀ (J : Set α) (hJ : M.IsBasis J F') (hIJ : I ⊆ J), e ∈ F'
Tactic: obtain ⟨J, hJ, hIJ⟩ := hI.subset_isBasis_of_subset hIF' hF'.2
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
⊢ M.IsBasis I (insert e I) ↔ e ∈ M.closure I
have rw : M.IsBasis I (insert e I) ↔ Membership.mem (γ := Set α) {x : α | M.IsBasis I (insert x I)} e
Tactic: rw [hI.closure_eq_setOf_isBasis_insert, mem_setOf]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
rw : M.IsBasis I (insert e I) ↔ Membership.mem (γ := Set α) {x : α | M.IsBasis I (insert x I)} e
⊢ M.IsBasis I (insert e I) ↔ e ∈ M.closure I
have rw₁ : M.IsBasis I (insert e I) ↔ M.IsBasis I (insert e I)
Tactic: rw [hI.closure_eq_setOf_isBasis_insert, mem_setOf]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
⊢ M.IsBasis I (M.closure I)
have rw : M.IsBasis I {x : α | M.IsBasis I (insert x I)}
Tactic: rw [hI.closure_eq_setOf_isBasis_insert]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis I X
⊢ M.closure I = M.closure X
have refine : M.closure X ⊆ M.closure I
Tactic: refine subset_antisymm (M.closure_subset_closure h.subset) ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis I X
⊢ M.closure X ⊆ M.closure I
have rw : M.closure X ⊆ M.closure {x : α | M.IsBasis I (insert x I)}
Tactic: rw [← M.closure_closure I, h.indep.closure_eq_setOf_isBasis_insert]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis' I X
⊢ M.closure I = M.closure X
have rw : M.closure I = M.closure (X ∩ M.E)
Tactic: rw [← closure_inter_ground _ X, h.isBasis_inter_ground.closure_eq_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis' I X
rw : M.closure I = M.closure (X ∩ M.E)
⊢ M.closure I = M.closure X
have rw₁ : M.closure (X ∩ M.E) = M.closure (X ∩ M.E)
Tactic: rw [← closure_inter_ground _ X, h.isBasis_inter_ground.closure_eq_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis I X
⊢ X ⊆ M.closure I
have rw : M.closure X ⊆ M.closure I
Tactic: rw [← closure_subset_closure_iff_subset_closure, h.closure_eq_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis I X
rw : M.closure X ⊆ M.closure I
⊢ X ⊆ M.closure I
have rw₁ : M.closure X ⊆ M.closure X
Tactic: rw [← closure_subset_closure_iff_subset_closure, h.closure_eq_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis' I X
⊢ M.IsBasis I (M.closure X)
have rw : M.IsBasis I (M.closure I)
Tactic: rw [← h.closure_eq_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
x : α
hI : M.Indep I
⊢ x ∈ M.closure I ↔ M.Dep (insert x I) ∨ x ∈ I
have rwa : Membership.mem (γ := Set α) {x : α | M.IsBasis I (insert x I)} x ↔ M.Dep (insert x I) ∨ x ∈ I
Tactic: rwa [hI.closure_eq_setOf_isBasis_insert, mem_setOf, isBasis_insert_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
x : α
hI : M.Indep I
rwa : Membership.mem (γ := Set α) {x : α | M.IsBasis I (insert x I)} x ↔ M.Dep (insert x I) ∨ x ∈ I
⊢ x ∈ M.closure I ↔ M.Dep (insert x I) ∨ x ∈ I
have rwa₁ : M.IsBasis I (insert x I) ↔ M.Dep (insert x I) ∨ x ∈ I
Tactic: rwa [hI.closure_eq_setOf_isBasis_insert, mem_setOf, isBasis_insert_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
x : α
hI : M.Indep I
rwa : Membership.mem (γ := Set α) {x : α | M.IsBasis I (insert x I)} x ↔ M.Dep (insert x I) ∨ x ∈ I
rwa₁ : M.IsBasis I (insert x I) ↔ M.Dep (insert x I) ∨ x ∈ I
⊢ x ∈ M.closure I ↔ M.Dep (insert x I) ∨ x ∈ I
have rwa₂ : M.Dep (insert x I) ∨ x ∈ I ↔ M.Dep (insert x I) ∨ x ∈ I
Tactic: rwa [hI.closure_eq_setOf_isBasis_insert, mem_setOf, isBasis_insert_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
I : Set α
x : α
hI : M.Indep I
⊢ x ∈ M.closure I ↔ x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)
have rw : ¬M.Indep (insert x I) ∧ x ∈ M.E ∨ x ∈ I ↔ x ∈ M.E ∧ (¬M.Indep (insert x I) ∨ x ∈ I)
Tactic: rw [hI.mem_closure_iff, dep_iff, insert_subset_iff, and_iff_left hI.subset_ground,
    imp_iff_not_or]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (hypothesis)
Goal:
α : Type u_2
M : Matroid α
I : Set α
x : α
hI : M.Indep I
⊢ ¬M.Indep (insert x I) ∧ x ∈ M.E ∨ x ∈ I ↔ x ∈ M.E ∧ (¬M.Indep (insert x I) ∨ x ∈ I)
have this : I ⊆ M.E
Tactic: have := 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.Dep (insert e I) ↔ e ∈ M.closure I \ I
have rw : e ∈ I → ¬M.Dep (insert e I)
Tactic: rw [mem_diff, hI.mem_closure_iff, or_and_right, and_not_self_iff, or_false,
    iff_self_and, imp_not_comm]
-- 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.Dep (insert e I)
have rw : ¬M.Dep I
Tactic: rw [insert_eq_of_mem 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
⊢ e ∈ M.closure I ↔ M.Dep (insert e I)
have rw : e ∈ M.closure I ↔ e ∈ M.closure I \ I
Tactic: rw [hI.insert_dep_iff, mem_diff, 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
rw : e ∈ M.closure I ↔ e ∈ M.closure I \ I
⊢ e ∈ M.closure I ↔ M.Dep (insert e I)
have rw₁ : e ∈ M.closure I ↔ e ∈ M.closure I ∧ e ∉ I
Tactic: rw [hI.insert_dep_iff, mem_diff, 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
rw : e ∈ M.closure I ↔ e ∈ M.closure I \ I
rw₁ : e ∈ M.closure I ↔ e ∈ M.closure I ∧ e ∉ I
⊢ e ∈ M.closure I ↔ M.Dep (insert e I)
have rw₂ : e ∈ M.closure I ↔ e ∈ M.closure I
Tactic: rw [hI.insert_dep_iff, mem_diff, 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
he : e ∈ M.E
⊢ e ∉ M.closure I ↔ M.Indep (insert e I) ∧ e ∉ I
have rw : ¬(¬M.Indep (insert e I) ∨ e ∈ I) ↔ M.Indep (insert e I) ∧ e ∉ I
Tactic: rw [hI.mem_closure_iff, dep_iff, insert_subset_iff, and_iff_right he,
    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
he : e ∈ M.E
⊢ ¬(¬M.Indep (insert e I) ∨ e ∈ I) ↔ M.Indep (insert e I) ∧ e ∉ I
have mp : ¬(¬M.Indep (insert e I) ∨ e ∈ I) → M.Indep (insert e I) ∧ e ∉ I
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
he : e ∈ M.E
mp : ¬(¬M.Indep (insert e I) ∨ e ∈ I) → M.Indep (insert e I) ∧ e ∉ I
⊢ ¬(¬M.Indep (insert e I) ∨ e ∈ I) ↔ M.Indep (insert e I) ∧ e ∉ I
have mpr : M.Indep (insert e I) ∧ e ∉ I → ¬(¬M.Indep (insert e I) ∨ e ∈ I)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
he : e ∈ M.E
mp : ¬(¬M.Indep (insert e I) ∨ e ∈ I) → M.Indep (insert e I) ∧ e ∉ I
mpr : M.Indep (insert e I) ∧ e ∉ I → ¬(¬M.Indep (insert e I) ∨ e ∈ I)
⊢ ¬(¬M.Indep (insert e I) ∨ e ∈ I) ↔ M.Indep (insert e I) ∧ e ∉ I
have mp₁ : ¬¬M.Indep (insert e I) → e ∉ I → M.Indep (insert e I) ∧ e ∉ I
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
he : e ∈ M.E
mp : ¬(¬M.Indep (insert e I) ∨ e ∈ I) → M.Indep (insert e I) ∧ e ∉ I
mpr : M.Indep (insert e I) ∧ e ∉ I → ¬(¬M.Indep (insert e I) ∨ e ∈ I)
mp₁ mp₂ : ¬¬M.Indep (insert e I) → e ∉ I → M.Indep (insert e I) ∧ e ∉ I
⊢ ¬(¬M.Indep (insert e I) ∨ e ∈ I) ↔ M.Indep (insert e I) ∧ e ∉ I
have mp₃ : ¬¬M.Indep (insert e I) → e ∉ I → M.Indep (insert e I)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
he : e ∈ M.E
mp : ¬(¬M.Indep (insert e I) ∨ e ∈ I) → M.Indep (insert e I) ∧ e ∉ I
mpr : M.Indep (insert e I) ∧ e ∉ I → ¬(¬M.Indep (insert e I) ∨ e ∈ I)
mp₁ mp₂ : ¬¬M.Indep (insert e I) → e ∉ I → M.Indep (insert e I) ∧ e ∉ I
mp₃ : ¬¬M.Indep (insert e I) → e ∉ I → M.Indep (insert e I)
⊢ ¬(¬M.Indep (insert e I) ∨ e ∈ I) ↔ M.Indep (insert e I) ∧ e ∉ I
have mp₄ : ¬¬M.Indep (insert e I) → e ∉ I → e ∉ I
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
he : e ∈ M.E
mp : ¬(¬M.Indep (insert e I) ∨ e ∈ I) → M.Indep (insert e I) ∧ e ∉ I
mpr : M.Indep (insert e I) ∧ e ∉ I → ¬(¬M.Indep (insert e I) ∨ e ∈ I)
mp₁ mp₂ : ¬¬M.Indep (insert e I) → e ∉ I → M.Indep (insert e I) ∧ e ∉ I
mp₃ : ¬¬M.Indep (insert e I) → e ∉ I → M.Indep (insert e I)
mp₄ : ¬¬M.Indep (insert e I) → e ∉ I → e ∉ I
⊢ ¬(¬M.Indep (insert e I) ∨ e ∈ I) ↔ M.Indep (insert e I) ∧ e ∉ I
have mpr₁ : M.Indep (insert e I) → e ∉ I → ¬(¬M.Indep (insert e I) ∨ e ∈ I)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
he : e ∈ M.E
mp : ¬(¬M.Indep (insert e I) ∨ e ∈ I) → M.Indep (insert e I) ∧ e ∉ I
mpr : M.Indep (insert e I) ∧ e ∉ I → ¬(¬M.Indep (insert e I) ∨ e ∈ I)
mp₁ mp₂ : ¬¬M.Indep (insert e I) → e ∉ I → M.Indep (insert e I) ∧ e ∉ I
mp₃ : ¬¬M.Indep (insert e I) → e ∉ I → M.Indep (insert e I)
mp₄ : ¬¬M.Indep (insert e I) → e ∉ I → e ∉ I
mpr₁ mpr₂ : M.Indep (insert e I) → e ∉ I → ¬(¬M.Indep (insert e I) ∨ e ∈ I)
mpr₃ : M.Indep (insert e I) → e ∉ I → ¬M.Indep (insert e I) ∨ e ∈ I → False
⊢ ¬(¬M.Indep (insert e I) ∨ e ∈ I) ↔ M.Indep (insert e I) ∧ e ∉ I
have mp₅ : M.Indep (insert e I) → e ∉ I → M.Indep (insert e I)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
he : e ∈ M.E
mp : ¬(¬M.Indep (insert e I) ∨ e ∈ I) → M.Indep (insert e I) ∧ e ∉ I
mpr : M.Indep (insert e I) ∧ e ∉ I → ¬(¬M.Indep (insert e I) ∨ e ∈ I)
mp₁ mp₂ : ¬¬M.Indep (insert e I) → e ∉ I → M.Indep (insert e I) ∧ e ∉ I
mp₃ : ¬¬M.Indep (insert e I) → e ∉ I → M.Indep (insert e I)
mp₄ : ¬¬M.Indep (insert e I) → e ∉ I → e ∉ I
mpr₁ mpr₂ : M.Indep (insert e I) → e ∉ I → ¬(¬M.Indep (insert e I) ∨ e ∈ I)
mpr₃ : M.Indep (insert e I) → e ∉ I → ¬M.Indep (insert e I) ∨ e ∈ I → False
mp₅ mp₆ mp₇ : M.Indep (insert e I) → e ∉ I → M.Indep (insert e I)
⊢ ¬(¬M.Indep (insert e I) ∨ e ∈ I) ↔ M.Indep (insert e I) ∧ e ∉ I
have mpr₄ : M.Indep (insert e I) → e ∉ I → ¬M.Indep (insert e I) → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
he : e ∈ M.E
mp : ¬(¬M.Indep (insert e I) ∨ e ∈ I) → M.Indep (insert e I) ∧ e ∉ I
mpr : M.Indep (insert e I) ∧ e ∉ I → ¬(¬M.Indep (insert e I) ∨ e ∈ I)
mp₁ mp₂ : ¬¬M.Indep (insert e I) → e ∉ I → M.Indep (insert e I) ∧ e ∉ I
mp₃ : ¬¬M.Indep (insert e I) → e ∉ I → M.Indep (insert e I)
mp₄ : ¬¬M.Indep (insert e I) → e ∉ I → e ∉ I
mpr₁ mpr₂ : M.Indep (insert e I) → e ∉ I → ¬(¬M.Indep (insert e I) ∨ e ∈ I)
mpr₃ : M.Indep (insert e I) → e ∉ I → ¬M.Indep (insert e I) ∨ e ∈ I → False
mp₅ mp₆ mp₇ : M.Indep (insert e I) → e ∉ I → M.Indep (insert e I)
mpr₄ : M.Indep (insert e I) → e ∉ I → ¬M.Indep (insert e I) → False
⊢ ¬(¬M.Indep (insert e I) ∨ e ∈ I) ↔ M.Indep (insert e I) ∧ e ∉ I
have mpr₅ : M.Indep (insert e I) → e ∉ I → e ∈ I → False
Tactic: tauto
-- 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
⊢ e ∉ M.closure I ↔ M.Indep (insert e I)
have rw : M.Indep (insert e I) ∧ e ∉ I ↔ M.Indep (insert e I)
Tactic: rw [hI.notMem_closure_iff, and_iff_left heI]