awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_3_to_5 : ∀ (a : M.IsCocircuit {e}), (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
tfae_5_to_4 : ∀ (a : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E) ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_5_iff_6 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E ↔ ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X
inr :
  ∀
    (this :
      ∀ {α : Type u_1} (M : Matroid α) (e : α) (tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops)
        (tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e})
        (tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B)
        (tfae_3_to_5 : ∀ (a : M.IsCocircuit {e}), (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E)
        (tfae_5_to_4 : ∀ (a : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E) ⦃B : Set α⦄, M.IsBase B → e ∈ B)
        (tfae_5_iff_6 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E ↔ ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X)
        (he : e ∈ M.E), M.IsColoop e ↔ ¬M.Spanning (M.E \ {e}))
    (he : e ∉ M.E), M.IsColoop e ↔ ¬M.Spanning (M.E \ {e})
⊢ M.IsColoop e ↔ ¬M.Spanning (M.E \ {e})
have wlog : ∀ {α : Type u_1} (M : Matroid α) (e : α) (tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops)
  (tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}) (tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B)
  (tfae_3_to_5 : ∀ (a : M.IsCocircuit {e}), (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E)
  (tfae_5_to_4 : ∀ (a : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E) ⦃B : Set α⦄, M.IsBase B → e ∈ B)
  (tfae_5_iff_6 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E ↔ ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X)
  (he : e ∈ M.E), M.IsColoop e ↔ ¬M.Spanning (M.E \ {e})
Tactic: wlog he : e ∈ M.E
Cleared hypotheses: M, e, tfae_1_iff_2, tfae_1_iff_3, tfae_1_iff_4, tfae_3_to_5, tfae_5_to_4, tfae_5_iff_6
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α_1 α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_3_to_5 : ∀ (a : M.IsCocircuit {e}), (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
tfae_5_to_4 : ∀ (a : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E) ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_5_iff_6 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E ↔ ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X
he : e ∈ M.E
⊢ M.IsColoop e ↔ ¬M.Spanning (M.E \ {e})
have rw : M.IsColoop e ↔ ¬M.Coindep (M.E \ (M.E \ {e}))
Tactic: rw [spanning_iff_compl_coindep diff_subset, ← dual_isLoop_iff_isColoop, ← singleton_dep,
      diff_diff_cancel_left (by simpa), ← not_indep_iff (by simpa)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α_1 α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_3_to_5 : ∀ (a : M.IsCocircuit {e}), (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
tfae_5_to_4 : ∀ (a : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E) ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_5_iff_6 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E ↔ ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X
he : e ∈ M.E
rw : M.IsColoop e ↔ ¬M.Coindep (M.E \ (M.E \ {e}))
⊢ M.IsColoop e ↔ ¬M.Spanning (M.E \ {e})
have rw₁ : M✶.IsLoop e ↔ ¬M.Coindep (M.E \ (M.E \ {e}))
Tactic: rw [spanning_iff_compl_coindep diff_subset, ← dual_isLoop_iff_isColoop, ← singleton_dep,
      diff_diff_cancel_left (by simpa), ← not_indep_iff (by simpa)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α_1 α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_3_to_5 : ∀ (a : M.IsCocircuit {e}), (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
tfae_5_to_4 : ∀ (a : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E) ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_5_iff_6 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E ↔ ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X
he : e ∈ M.E
rw : M.IsColoop e ↔ ¬M.Coindep (M.E \ (M.E \ {e}))
rw₁ : M✶.IsLoop e ↔ ¬M.Coindep (M.E \ (M.E \ {e}))
⊢ M.IsColoop e ↔ ¬M.Spanning (M.E \ {e})
have rw₂ : M✶.Dep {e} ↔ ¬M.Coindep (M.E \ (M.E \ {e}))
Tactic: rw [spanning_iff_compl_coindep diff_subset, ← dual_isLoop_iff_isColoop, ← singleton_dep,
      diff_diff_cancel_left (by simpa), ← not_indep_iff (by simpa)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α_1 α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_3_to_5 : ∀ (a : M.IsCocircuit {e}), (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
tfae_5_to_4 : ∀ (a : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E) ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_5_iff_6 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E ↔ ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X
he : e ∈ M.E
rw : M.IsColoop e ↔ ¬M.Coindep (M.E \ (M.E \ {e}))
rw₁ : M✶.IsLoop e ↔ ¬M.Coindep (M.E \ (M.E \ {e}))
rw₂ : M✶.Dep {e} ↔ ¬M.Coindep (M.E \ (M.E \ {e}))
⊢ M.IsColoop e ↔ ¬M.Spanning (M.E \ {e})
have rw₃ : M✶.Dep {e} ↔ ¬M.Coindep {e}
Tactic: rw [spanning_iff_compl_coindep diff_subset, ← dual_isLoop_iff_isColoop, ← singleton_dep,
      diff_diff_cancel_left (by simpa), ← not_indep_iff (by simpa)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α_1 α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_3_to_5 : ∀ (a : M.IsCocircuit {e}), (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
tfae_5_to_4 : ∀ (a : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E) ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_5_iff_6 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E ↔ ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X
he : e ∈ M.E
rw : M.IsColoop e ↔ ¬M.Coindep (M.E \ (M.E \ {e}))
rw₁ : M✶.IsLoop e ↔ ¬M.Coindep (M.E \ (M.E \ {e}))
rw₂ : M✶.Dep {e} ↔ ¬M.Coindep (M.E \ (M.E \ {e}))
rw₃ : M✶.Dep {e} ↔ ¬M.Coindep {e}
⊢ M.IsColoop e ↔ ¬M.Spanning (M.E \ {e})
have rw₄ : ¬M✶.Indep {e} ↔ ¬M.Coindep {e}
Tactic: rw [spanning_iff_compl_coindep diff_subset, ← dual_isLoop_iff_isColoop, ← singleton_dep,
      diff_diff_cancel_left (by simpa), ← not_indep_iff (by simpa)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (hypothesis)
Goal:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_3_to_5 : ∀ (a : M.IsCocircuit {e}), (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
tfae_5_to_4 : ∀ (a : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E) ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_5_iff_6 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E ↔ ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X
⊢ [M.IsColoop e, e ∈ M.coloops, M.IsCocircuit {e}, ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B,
      (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E, ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X,
      ¬M.Spanning (M.E \ {e})].TFAE
have tfae_1_iff_7 : M.IsColoop e ↔ ¬M.Spanning (M.E \ {e})
Tactic: tfae_have 1 ↔ 7 := by
    wlog he : e ∈ M.E
    · exact iff_of_false (fun h ↦ he h.mem_ground) <| by simp [he, M.ground_spanning]
    rw [spanning_iff_compl_coindep diff_subset, ← dual_isLoop_iff_isColoop, ← singleton_dep,
      diff_diff_cancel_left (by simpa), ← not_indep_iff (by simpa)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (hypothesis)
Goal:
α : Type u_1
M : Matroid α
e : α
h : M.IsLoop e
⊢ ¬M✶.IsLoop e
have h₁ : M✶.IsColoop e
Tactic: rw [← dual_dual M, dual_isLoop_iff_isColoop] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ M.IsColoop e ↔ ∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C
have simp_rw : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E ↔ ∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C
Tactic: simp_rw [(M.isColoop_tfae e).out 0 4, and_iff_left he]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
inst : M✶.RankPos
⊢ M.IsColoop e ↔ ∀ (C : Set α), M.IsCircuit C → e ∈ M.E \ C
have pos : ∀ (he : e ∈ M.E), M.IsColoop e ↔ ∀ (C : Set α), M.IsCircuit C → e ∈ M.E \ C
Tactic: by_cases he : e ∈ M.E
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
inst : M✶.RankPos
pos : ∀ (he : e ∈ M.E), M.IsColoop e ↔ ∀ (C : Set α), M.IsCircuit C → e ∈ M.E \ C
⊢ M.IsColoop e ↔ ∀ (C : Set α), M.IsCircuit C → e ∈ M.E \ C
have neg : ∀ (he : e ∉ M.E), M.IsColoop e ↔ ∀ (C : Set α), M.IsCircuit C → e ∈ M.E \ C
Tactic: by_cases he : e ∈ M.E
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
inst : M✶.RankPos
he : e ∉ M.E
⊢ M.IsColoop e ↔ ∀ (C : Set α), M.IsCircuit C → e ∈ M.E \ C
have neg : ∀ (C : Set α) (hC : M.IsCircuit C), M.IsColoop e ↔ ∀ (C : Set α), M.IsCircuit C → e ∈ M.E \ C
Tactic: obtain ⟨C, hC⟩ := M.exists_isCircuit
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
⊢ M.IsColoop e ↔ (∀ X ⊆ M.E, e ∈ M.closure X ↔ e ∈ X) ∧ e ∈ M.E
have refine : (∀ X ⊆ M.E, e ∈ M.closure X ↔ e ∈ X) ∧ e ∈ M.E →
  ∀ (h : ∀ X ⊆ M.E, e ∈ M.closure X ↔ e ∈ X) (he : e ∈ M.E) (X : Set α), e ∈ M.closure X ↔ e ∈ X
Tactic: refine ⟨fun h ↦ ⟨fun X _ ↦ isColoop_iff_forall_mem_closure_iff_mem.1 h X, h.mem_ground⟩,
    fun ⟨h, he⟩ ↦ isColoop_iff_forall_mem_closure_iff_mem.2 fun X ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
h_1 : (∀ X ⊆ M.E, e ∈ M.closure X ↔ e ∈ X) ∧ e ∈ M.E
h : ∀ X ⊆ M.E, e ∈ M.closure X ↔ e ∈ X
he : e ∈ M.E
X : Set α
⊢ e ∈ M.closure X ↔ e ∈ X
have rw : e ∈ M.closure (X ∩ M.E) ↔ e ∈ X
Tactic: rw [← closure_inter_ground, h _ inter_subset_right, mem_inter_iff, and_iff_left he]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
h_1 : (∀ X ⊆ M.E, e ∈ M.closure X ↔ e ∈ X) ∧ e ∈ M.E
h : ∀ X ⊆ M.E, e ∈ M.closure X ↔ e ∈ X
he : e ∈ M.E
X : Set α
rw : e ∈ M.closure (X ∩ M.E) ↔ e ∈ X
⊢ e ∈ M.closure X ↔ e ∈ X
have rw₁ : e ∈ X ∩ M.E ↔ e ∈ X
Tactic: rw [← closure_inter_ground, h _ inter_subset_right, mem_inter_iff, and_iff_left he]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
h_1 : (∀ X ⊆ M.E, e ∈ M.closure X ↔ e ∈ X) ∧ e ∈ M.E
h : ∀ X ⊆ M.E, e ∈ M.closure X ↔ e ∈ X
he : e ∈ M.E
X : Set α
rw : e ∈ M.closure (X ∩ M.E) ↔ e ∈ X
rw₁ : e ∈ X ∩ M.E ↔ e ∈ X
⊢ e ∈ M.closure X ↔ e ∈ X
have rw₂ : e ∈ X ∧ e ∈ M.E ↔ e ∈ X
Tactic: rw [← closure_inter_ground, h _ inter_subset_right, mem_inter_iff, and_iff_left he]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
h_1 : (∀ X ⊆ M.E, e ∈ M.closure X ↔ e ∈ X) ∧ e ∈ M.E
h : ∀ X ⊆ M.E, e ∈ M.closure X ↔ e ∈ X
he : e ∈ M.E
X : Set α
rw : e ∈ M.closure (X ∩ M.E) ↔ e ∈ X
rw₁ : e ∈ X ∩ M.E ↔ e ∈ X
rw₂ : e ∈ X ∧ e ∈ M.E ↔ e ∈ X
⊢ e ∈ M.closure X ↔ e ∈ X
have rw₃ : e ∈ X ↔ e ∈ X
Tactic: rw [← closure_inter_ground, h _ inter_subset_right, mem_inter_iff, and_iff_left he]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
⊢ M.IsColoop e ↔ M.closure (M.E \ {e}) ≠ M.E
have rw : ¬M.Spanning (M.E \ {e}) ↔ M.closure (M.E \ {e}) ≠ M.E
Tactic: rw [isColoop_iff_diff_not_spanning, spanning_iff_closure_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
rw : ¬M.Spanning (M.E \ {e}) ↔ M.closure (M.E \ {e}) ≠ M.E
⊢ M.IsColoop e ↔ M.closure (M.E \ {e}) ≠ M.E
have rw₁ : ¬M.closure (M.E \ {e}) = M.E ↔ M.closure (M.E \ {e}) ≠ M.E
Tactic: rw [isColoop_iff_diff_not_spanning, spanning_iff_closure_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ M.IsColoop e ↔ e ∉ M.closure (M.E \ {e})
have rw : M.closure (M.E \ {e}) = M.E ↔ e ∈ M.closure (M.E \ {e})
Tactic: rw [isColoop_iff_diff_closure, not_iff_not]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ M.closure (M.E \ {e}) = M.E ↔ e ∈ M.closure (M.E \ {e})
have refine : ∀ (h : e ∈ M.closure (M.E \ {e})) (x : α) (hx : x ∈ M.E), x ∈ M.closure (M.E \ {e})
Tactic: refine ⟨fun h ↦ by rwa [h], fun h ↦ (M.closure_subset_ground _).antisymm fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
h : e ∈ M.closure (M.E \ {e})
x : α
hx : x ∈ M.E
⊢ x ∈ M.closure (M.E \ {e})
have inl : ∀ (he : x ∈ M.E) (h : x ∈ M.closure (M.E \ {x})), x ∈ M.closure (M.E \ {x})
Tactic: obtain (rfl | hne) := eq_or_ne x e
Cleared hypotheses: e, he, h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
h : e ∈ M.closure (M.E \ {e})
x : α
hx : x ∈ M.E
inl : ∀ (he : x ∈ M.E) (h : x ∈ M.closure (M.E \ {x})), x ∈ M.closure (M.E \ {x})
⊢ x ∈ M.closure (M.E \ {e})
have inr : ∀ (hne : x ≠ e), x ∈ M.closure (M.E \ {e})
Tactic: obtain (rfl | hne) := eq_or_ne x e
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
⊢ M.IsColoop e ↔ ∀ x ∈ M.E \ B, e ∉ M.fundCircuit x B
have refine : ∀ (h : ∀ x ∈ M.E \ B, e ∉ M.fundCircuit x B), M.IsColoop e
Tactic: refine ⟨fun h x hx heC ↦ (h.notMem_isCircuit <| hB.fundCircuit_isCircuit hx.1 hx.2) heC,
    fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCircuit x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
⊢ x ∈ M.closure (B \ {e})
have inl : ∀ (hx : x ∈ B), x ∈ M.closure (B \ {e})
Tactic: obtain (hx | hx) := em (x ∈ B)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCircuit x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
inl : ∀ (hx : x ∈ B), x ∈ M.closure (B \ {e})
⊢ x ∈ M.closure (B \ {e})
have inr : ∀ (hx : x ∉ B), x ∈ M.closure (B \ {e})
Tactic: obtain (hx | hx) := em (x ∈ B)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (hypothesis)
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCircuit x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∉ B
⊢ x ∈ M.closure (B \ {e})
have h_cct : x ∈ M.closure (M.fundCircuit x B \ {x})
Tactic: have h_cct := (hB.fundCircuit_isCircuit hxE hx).mem_closure_diff_singleton_of_mem
      (M.mem_fundCircuit x B)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCircuit x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∉ B
h_cct : x ∈ M.closure (M.fundCircuit x B \ {x})
⊢ x ∈ M.closure (B \ {e})
have inr : M.fundCircuit x B \ {x} ⊆ B
Tactic: refine (M.closure_subset_closure (subset_diff_singleton ?_ ?_)) h_cct
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCircuit x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∉ B
h_cct : x ∈ M.closure (M.fundCircuit x B \ {x})
inr : M.fundCircuit x B \ {x} ⊆ B
⊢ x ∈ M.closure (B \ {e})
have inr₁ : e ∉ M.fundCircuit x B \ {x}
Tactic: refine (M.closure_subset_closure (subset_diff_singleton ?_ ?_)) h_cct
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (hypothesis)
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCircuit x B
⊢ M.IsColoop e
have h' : M.E \ {e} ⊆ M.closure (B \ {e})
Tactic: have h' : M.E \ {e} ⊆ M.closure (B \ {e}) := by
    rintro x ⟨hxE, hne : x ≠ e⟩
    obtain (hx | hx) := em (x ∈ B)
    · exact M.subset_closure (B \ {e}) (diff_subset.trans hB.subset_ground) ⟨hx, hne⟩
    have h_cct := (hB.fundCircuit_isCircuit hxE hx).mem_closure_diff_singleton_of_mem
      (M.mem_fundCircuit x B)
    refine (M.closure_subset_closure (subset_diff_singleton ?_ ?_)) h_cct
    · simpa using fundCircuit_subset_insert ..
    simp [hne.symm, h x ⟨hxE, hx⟩]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCircuit x B
h' : M.E \ {e} ⊆ M.closure (B \ {e})
⊢ M.IsColoop e
have rw : e ∉ M.closure (M.E \ {e})
Tactic: rw [isColoop_iff_notMem_closure_compl (hB.subset_ground he)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
X I : Set α
hIX : M.IsBasis' I X
e : α
⊢ e ∈ X ∩ M.coloops → e ∈ I
have this : ∀ (heX : e ∈ X) (heI : M.IsColoop e), e ∈ I
Tactic: ⟨heX, (heI : M.IsColoop e)⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
X I : Set α
hIX : M.IsBasis' I X
e : α
heX : e ∈ X
heI : M.IsColoop e
⊢ e ∈ I
have rwa : e ∈ M.closure I
Tactic: rwa [← heI.mem_closure_iff_mem, hIX.isBasis_closure_right.closure_eq_right,
    heI.mem_closure_iff_mem]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
X I : Set α
hIX : M.IsBasis' I X
e : α
heX : e ∈ X
heI : M.IsColoop e
rwa : e ∈ M.closure I
⊢ e ∈ I
have rwa₁ : e ∈ M.closure X
Tactic: rwa [← heI.mem_closure_iff_mem, hIX.isBasis_closure_right.closure_eq_right,
    heI.mem_closure_iff_mem]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (hypothesis)
Goal:
α : Type u_1
M : Matroid α
e : α
heE : e ∈ M.E
he : ¬M.IsColoop e
⊢ ∃ (C : Set α), M.IsCircuit C ∧ e ∈ C
have he₁ : ∃ (x : Set α), M.IsBase x ∧ e ∉ x
Tactic: simp only [isColoop_iff_forall_mem_isBase, not_forall, exists_prop] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
heE : e ∈ M.E
he : ∃ (x : Set α), M.IsBase x ∧ e ∉ x
⊢ ∃ (C : Set α), M.IsCircuit C ∧ e ∈ C
have obtain : ∀ (B : Set α) (hB : M.IsBase B) (heB : e ∉ B), ∃ (C : Set α), M.IsCircuit C ∧ e ∈ C
Tactic: obtain ⟨B, hB, heB⟩ := he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.closure X ∩ M.coloops = X ∩ M.coloops
have simp_rw : ∀ (x : α), M.IsColoop x → (x ∈ M.closure X ↔ x ∈ X)
Tactic: simp_rw [Set.ext_iff, mem_inter_iff, ← isColoop_iff_mem_coloops, and_congr_left_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
he : M.IsColoop e
⊢ e ∈ M.closure X ↔ e ∈ X
have rw : e ∈ X ↔ e ∈ X
Tactic: rw [he.mem_closure_iff_mem]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
⊢ M.closure X ∩ K = X ∩ K
have nth_rw : M.closure X ∩ (M.coloops ∩ K) = X ∩ K
Tactic: nth_rw 1 [← inter_eq_self_of_subset_right hK]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
⊢ M.closure X ∩ (M.coloops ∩ K) = X ∩ K
have rw : M.closure X ∩ M.coloops ∩ K = X ∩ K
Tactic: rw [← inter_assoc, closure_inter_coloops_eq, inter_assoc, inter_eq_self_of_subset_right hK]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
rw : M.closure X ∩ M.coloops ∩ K = X ∩ K
⊢ M.closure X ∩ (M.coloops ∩ K) = X ∩ K
have rw₁ : X ∩ M.coloops ∩ K = X ∩ K
Tactic: rw [← inter_assoc, closure_inter_coloops_eq, inter_assoc, inter_eq_self_of_subset_right hK]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
rw : M.closure X ∩ M.coloops ∩ K = X ∩ K
rw₁ : X ∩ M.coloops ∩ K = X ∩ K
⊢ M.closure X ∩ (M.coloops ∩ K) = X ∩ K
have rw₂ : X ∩ (M.coloops ∩ K) = X ∩ K
Tactic: rw [← inter_assoc, closure_inter_coloops_eq, inter_assoc, inter_eq_self_of_subset_right hK]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
rw : M.closure X ∩ M.coloops ∩ K = X ∩ K
rw₁ : X ∩ M.coloops ∩ K = X ∩ K
rw₂ : X ∩ (M.coloops ∩ K) = X ∩ K
⊢ M.closure X ∩ (M.coloops ∩ K) = X ∩ K
have rw₃ : X ∩ K = X ∩ K
Tactic: rw [← inter_assoc, closure_inter_coloops_eq, inter_assoc, inter_eq_self_of_subset_right hK]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
⊢ M.closure (X ∪ K) = M.closure X ∪ K
have rw : ∀ (x : α), x ∉ M.closure (M.closure X ∪ K) \ (M.closure X ∪ K)
Tactic: rw [← closure_union_closure_left_eq, subset_antisymm_iff, and_iff_left (M.subset_closure _),
    ← diff_eq_empty, eq_empty_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
⊢ ∀ (x : α), x ∉ M.closure (M.closure X ∪ K) \ (M.closure X ∪ K)
have refine : ∀ e ∈ M.closure (M.closure X ∪ K) \ (M.closure X ∪ K),
  ∀ (hecl : e ∈ M.closure (M.closure X ∪ K)) (he : e ∉ M.closure X ∪ K), e ∈ M.closure X
Tactic: refine fun e ⟨hecl, he⟩ ↦ he (.inl ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
e : α
h : e ∈ M.closure (M.closure X ∪ K) \ (M.closure X ∪ K)
hecl : e ∈ M.closure (M.closure X ∪ K)
he : e ∉ M.closure X ∪ K
⊢ e ∈ M.closure X
have obtain : ∀ (C : Set α) (hCss : C ⊆ insert e (M.closure X ∪ K)) (hC : M.IsCircuit C) (heC : e ∈ C), e ∈ M.closure X
Tactic: obtain ⟨C, hCss, hC, heC⟩ := (mem_closure_iff_exists_isCircuit he).1 hecl
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (hypothesis)
Goal:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
e : α
h : e ∈ M.closure (M.closure X ∪ K) \ (M.closure X ∪ K)
hecl : e ∈ M.closure (M.closure X ∪ K)
he : e ∉ M.closure X ∪ K
C : Set α
hCss : C ⊆ insert e (M.closure X ∪ K)
hC : M.IsCircuit C
heC : e ∈ C
⊢ e ∈ M.closure X
have hCss₁ : C ⊆ insert e (M.closure X)
Tactic: rw [← singleton_union, ← union_assoc, union_comm, ← diff_subset_iff,
    (hC.disjoint_coloops.mono_right hK).sdiff_eq_left, singleton_union] at hCss
Cleared hypotheses: hCss, hC, heC
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
X : Set α
he : M.IsColoop e
⊢ M.closure (insert e X) = insert e (M.closure X)
have rw : M.closure (X ∪ {e}) = insert e (M.closure X)
Tactic: rw [← union_singleton, closure_union_eq_of_subset_coloops _ (by simpa), union_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
X : Set α
he : M.IsColoop e
rw : M.closure (X ∪ {e}) = insert e (M.closure X)
⊢ M.closure (insert e X) = insert e (M.closure X)
have rw₁ : M.closure X ∪ {e} = insert e (M.closure X)
Tactic: rw [← union_singleton, closure_union_eq_of_subset_coloops _ (by simpa), union_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
X : Set α
he : M.IsColoop e
rw : M.closure (X ∪ {e}) = insert e (M.closure X)
rw₁ : M.closure X ∪ {e} = insert e (M.closure X)
⊢ M.closure (insert e X) = insert e (M.closure X)
have rw₂ : insert e (M.closure X) = insert e (M.closure X)
Tactic: rw [← union_singleton, closure_union_eq_of_subset_coloops _ (by simpa), union_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
K : Set α
hK : K ⊆ M.coloops
⊢ M.closure K = K ∪ M.loops
have rw : M.closure (∅ ∪ K) = ∅ ∪ K ∪ M.loops
Tactic: rw [← empty_union K, closure_union_eq_of_subset_coloops _ hK, empty_union, union_comm,
    closure_empty]