awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (hypothesis)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.IsCircuit {e, f}
⊢ M.closure {e} = M.closure {f}
have hclosure : M.closure ({e, f} \ {e}) = M.closure ({e, f} \ {f})
Tactic: have hclosure := (h.closure_diff_singleton_eq e).trans
    (h.closure_diff_singleton_eq f).symm
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.IsCircuit {e, f}
hclosure : M.closure ({e, f} \ {e}) = M.closure ({e, f} \ {f})
⊢ M.closure {e} = M.closure {f}
have refine_2 : ∀ (hclosure : M.closure {f} = M.closure ({e, f} \ {f})), M.closure {e} = M.closure {f}
Tactic: rwa [pair_diff_left hef, pair_diff_right hef, eq_comm] at hclosure
Cleared hypotheses: hclosure
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.IsCircuit {e, f}
hclosure : M.closure ({e, f} \ {e}) = M.closure ({e, f} \ {f})
refine_2 : ∀ (hclosure : M.closure {f} = M.closure ({e, f} \ {f})), M.closure {e} = M.closure {f}
⊢ M.closure {e} = M.closure {f}
have refine_2₁ : ∀ (hclosure : M.closure {f} = M.closure {e}), M.closure {e} = M.closure {f}
Tactic: rwa [pair_diff_left hef, pair_diff_right hef, eq_comm] at hclosure
Cleared hypotheses: hclosure
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.IsCircuit {e, f}
hclosure : M.closure ({e, f} \ {e}) = M.closure ({e, f} \ {f})
refine_2 : ∀ (hclosure : M.closure {f} = M.closure ({e, f} \ {f})), M.closure {e} = M.closure {f}
refine_2₁ : ∀ (hclosure : M.closure {f} = M.closure {e}), M.closure {e} = M.closure {f}
⊢ M.closure {e} = M.closure {f}
have refine_2₂ : ∀ (hclosure : M.closure {e} = M.closure {f}), M.closure {e} = M.closure {f}
Tactic: rwa [pair_diff_left hef, pair_diff_right hef, eq_comm] at hclosure
Cleared hypotheses: hclosure
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hf : M.IsNonloop f
⊢ M.closure {e} = M.closure {f} ↔ e = f ∨ ¬M.Indep {e, f}
have inl : ∀ (hf : M.IsNonloop e), M.closure {e} = M.closure {e} ↔ e = e ∨ ¬M.Indep {e, e}
Tactic: obtain (rfl | hne) := eq_or_ne e f
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hf : M.IsNonloop f
inl : ∀ (hf : M.IsNonloop e), M.closure {e} = M.closure {e} ↔ e = e ∨ ¬M.Indep {e, e}
⊢ M.closure {e} = M.closure {f} ↔ e = f ∨ ¬M.Indep {e, f}
have inr : ∀ (hne : e ≠ f), M.closure {e} = M.closure {f} ↔ e = f ∨ ¬M.Indep {e, f}
Tactic: obtain (rfl | hne) := eq_or_ne e f
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hf : M.IsNonloop f
hne : e ≠ f
⊢ M.closure {e} = M.closure {f} ↔ e = f ∨ ¬M.Indep {e, f}
have inr : ¬M.Indep {e, f} → ∀ (e_1 : α), Membership.mem (γ := Set α) {e, f} e_1 → M.Indep ({e, f} \ {e_1})
Tactic: simp_rw [he.closure_eq_closure_iff_isCircuit_of_ne hne, or_iff_right hne,
    isCircuit_iff_dep_forall_diff_singleton_indep, dep_iff, insert_subset_iff, singleton_subset_iff,
    and_iff_left hf.mem_ground, and_iff_left he.mem_ground, and_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
f : α
hf : M.IsNonloop f
x : α
he : M.IsNonloop x
hne : x ≠ f
hi : ¬M.Indep {x, f}
⊢ M.Indep ({x, f} \ {x})
have inr : M.Indep {f}
Tactic: rwa [pair_diff_left hne, indep_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
he : M.IsNonloop e
x : α
hf : M.IsNonloop x
hne : e ≠ x
hi : ¬M.Indep {e, x}
⊢ M.Indep ({e, x} \ {x})
have inr : M.Indep {e}
Tactic: rwa [pair_diff_right hne, indep_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
⊢ (M ↾ R).IsNonloop e ↔ M.IsNonloop e ∧ e ∈ R
have rw : (M ↾ R).Indep {e} ↔ M.IsNonloop e ∧ e ∈ R
Tactic: rw [← indep_singleton, restrict_indep_iff, singleton_subset_iff, indep_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
rw : (M ↾ R).Indep {e} ↔ M.IsNonloop e ∧ e ∈ R
⊢ (M ↾ R).IsNonloop e ↔ M.IsNonloop e ∧ e ∈ R
have rw₁ : M.Indep {e} ∧ {e} ⊆ R ↔ M.IsNonloop e ∧ e ∈ R
Tactic: rw [← indep_singleton, restrict_indep_iff, singleton_subset_iff, indep_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
rw : (M ↾ R).Indep {e} ↔ M.IsNonloop e ∧ e ∈ R
rw₁ : M.Indep {e} ∧ {e} ⊆ R ↔ M.IsNonloop e ∧ e ∈ R
⊢ (M ↾ R).IsNonloop e ↔ M.IsNonloop e ∧ e ∈ R
have rw₂ : M.Indep {e} ∧ e ∈ R ↔ M.IsNonloop e ∧ e ∈ R
Tactic: rw [← indep_singleton, restrict_indep_iff, singleton_subset_iff, indep_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
rw : (M ↾ R).Indep {e} ↔ M.IsNonloop e ∧ e ∈ R
rw₁ : M.Indep {e} ∧ {e} ⊆ R ↔ M.IsNonloop e ∧ e ∈ R
rw₂ : M.Indep {e} ∧ e ∈ R ↔ M.IsNonloop e ∧ e ∈ R
⊢ (M ↾ R).IsNonloop e ↔ M.IsNonloop e ∧ e ∈ R
have rw₃ : M.IsNonloop e ∧ e ∈ R ↔ M.IsNonloop e ∧ e ∈ R
Tactic: rw [← indep_singleton, restrict_indep_iff, singleton_subset_iff, indep_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M N : Matroid α
e : α
h : N.IsNonloop e
hNM : N ≤r M
⊢ M.IsNonloop e
have obtain : ∀ (R : Set α) (h : (M ↾ R).IsNonloop e), M.IsNonloop e
Tactic: obtain ⟨R, -, rfl⟩ := hNM
Cleared hypotheses: N, h, hNM
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
β : Type u_2
e : α
M : Matroid β
f : α → β
⊢ (M.comap f).IsNonloop e ↔ M.IsNonloop (f e)
have rw : (M.comap f).Indep {e} ↔ M.IsNonloop (f e)
Tactic: rw [← indep_singleton, comap_indep_iff, image_singleton, indep_singleton,
    and_iff_left (injOn_singleton _ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
β : Type u_2
e : α
M : Matroid β
f : α → β
rw : (M.comap f).Indep {e} ↔ M.IsNonloop (f e)
⊢ (M.comap f).IsNonloop e ↔ M.IsNonloop (f e)
have rw₁ : M.Indep (f '' {e}) ∧ InjOn f {e} ↔ M.IsNonloop (f e)
Tactic: rw [← indep_singleton, comap_indep_iff, image_singleton, indep_singleton,
    and_iff_left (injOn_singleton _ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
β : Type u_2
e : α
M : Matroid β
f : α → β
rw : (M.comap f).Indep {e} ↔ M.IsNonloop (f e)
rw₁ : M.Indep (f '' {e}) ∧ InjOn f {e} ↔ M.IsNonloop (f e)
⊢ (M.comap f).IsNonloop e ↔ M.IsNonloop (f e)
have rw₂ : M.Indep {f e} ∧ InjOn f {e} ↔ M.IsNonloop (f e)
Tactic: rw [← indep_singleton, comap_indep_iff, image_singleton, indep_singleton,
    and_iff_left (injOn_singleton _ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
β : Type u_2
e : α
M : Matroid β
f : α → β
rw : (M.comap f).Indep {e} ↔ M.IsNonloop (f e)
rw₁ : M.Indep (f '' {e}) ∧ InjOn f {e} ↔ M.IsNonloop (f e)
rw₂ : M.Indep {f e} ∧ InjOn f {e} ↔ M.IsNonloop (f e)
⊢ (M.comap f).IsNonloop e ↔ M.IsNonloop (f e)
have rw₃ : M.IsNonloop (f e) ∧ InjOn f {e} ↔ M.IsNonloop (f e)
Tactic: rw [← indep_singleton, comap_indep_iff, image_singleton, indep_singleton,
    and_iff_left (injOn_singleton _ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
β : Type u_2
e : α
M : Matroid β
f : α → β
rw : (M.comap f).Indep {e} ↔ M.IsNonloop (f e)
rw₁ : M.Indep (f '' {e}) ∧ InjOn f {e} ↔ M.IsNonloop (f e)
rw₂ : M.Indep {f e} ∧ InjOn f {e} ↔ M.IsNonloop (f e)
rw₃ : M.IsNonloop (f e) ∧ InjOn f {e} ↔ M.IsNonloop (f e)
⊢ (M.comap f).IsNonloop e ↔ M.IsNonloop (f e)
have rw₄ : M.IsNonloop (f e) ↔ M.IsNonloop (f e)
Tactic: rw [← indep_singleton, comap_indep_iff, image_singleton, indep_singleton,
    and_iff_left (injOn_singleton _ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
e : α
E : Set α
⊢ (freeOn E).IsNonloop e ↔ e ∈ E
have rw : (freeOn E).Indep {e} ↔ e ∈ E
Tactic: rw [← indep_singleton, freeOn_indep_iff, singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
e : α
E : Set α
rw : (freeOn E).Indep {e} ↔ e ∈ E
⊢ (freeOn E).IsNonloop e ↔ e ∈ E
have rw₁ : {e} ⊆ E ↔ e ∈ E
Tactic: rw [← indep_singleton, freeOn_indep_iff, singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
e : α
E : Set α
rw : (freeOn E).Indep {e} ↔ e ∈ E
rw₁ : {e} ⊆ E ↔ e ∈ E
⊢ (freeOn E).IsNonloop e ↔ e ∈ E
have rw₂ : e ∈ E ↔ e ∈ E
Tactic: rw [← indep_singleton, freeOn_indep_iff, singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
e : α
I E : Set α
⊢ (uniqueBaseOn I E).IsNonloop e ↔ e ∈ I ∩ E
have rw : (uniqueBaseOn I E).Indep {e} ↔ e ∈ I ∩ E
Tactic: rw [← indep_singleton, uniqueBaseOn_indep_iff', singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
e : α
I E : Set α
rw : (uniqueBaseOn I E).Indep {e} ↔ e ∈ I ∩ E
⊢ (uniqueBaseOn I E).IsNonloop e ↔ e ∈ I ∩ E
have rw₁ : {e} ⊆ I ∩ E ↔ e ∈ I ∩ E
Tactic: rw [← indep_singleton, uniqueBaseOn_indep_iff', singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
e : α
I E : Set α
rw : (uniqueBaseOn I E).Indep {e} ↔ e ∈ I ∩ E
rw₁ : {e} ⊆ I ∩ E ↔ e ∈ I ∩ E
⊢ (uniqueBaseOn I E).IsNonloop e ↔ e ∈ I ∩ E
have rw₂ : e ∈ I ∩ E ↔ e ∈ I ∩ E
Tactic: rw [← indep_singleton, uniqueBaseOn_indep_iff', singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
he : M.IsNonloop e
⊢ ∃ (K : Set α), M.IsCocircuit K ∧ e ∈ K
have obtain : ∀ (B : Set α) (hB : M.IsBase B) (heB : e ∈ B), ∃ (K : Set α), M.IsCocircuit K ∧ e ∈ K
Tactic: obtain ⟨B, hB, heB⟩ := he.exists_mem_isBase
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.closure (X ∩ {e : α | M.IsNonloop e}) = M.closure X
have rw : M.closure (X ∩ (M.E \ M.loops)) = M.closure X
Tactic: rw [setOf_isNonloop_eq, ← inter_diff_assoc, closure_diff_loops_eq, closure_inter_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
rw : M.closure (X ∩ (M.E \ M.loops)) = M.closure X
⊢ M.closure (X ∩ {e : α | M.IsNonloop e}) = M.closure X
have rw₁ : M.closure ((X ∩ M.E) \ M.loops) = M.closure X
Tactic: rw [setOf_isNonloop_eq, ← inter_diff_assoc, closure_diff_loops_eq, closure_inter_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
rw : M.closure (X ∩ (M.E \ M.loops)) = M.closure X
rw₁ : M.closure ((X ∩ M.E) \ M.loops) = M.closure X
⊢ M.closure (X ∩ {e : α | M.IsNonloop e}) = M.closure X
have rw₂ : M.closure (X ∩ M.E) = M.closure X
Tactic: rw [setOf_isNonloop_eq, ← inter_diff_assoc, closure_diff_loops_eq, closure_inter_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
rw : M.closure (X ∩ (M.E \ M.loops)) = M.closure X
rw₁ : M.closure ((X ∩ M.E) \ M.loops) = M.closure X
rw₂ : M.closure (X ∩ M.E) = M.closure X
⊢ M.closure (X ∩ {e : α | M.IsNonloop e}) = M.closure X
have rw₃ : M.closure X = M.closure X
Tactic: rw [setOf_isNonloop_eq, ← inter_diff_assoc, closure_diff_loops_eq, closure_inter_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ M✶.coloops = M.loops
have rw : M✶✶.loops = M.loops
Tactic: rw [coloops, dual_dual]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
rw : M✶✶.loops = M.loops
⊢ M✶.coloops = M.loops
have rw₁ : M.loops = M.loops
Tactic: rw [coloops, dual_dual]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
he : M.IsLoop e
⊢ M✶.IsColoop e
have rwa : M✶✶.IsLoop e
Tactic: rwa [IsColoop, dual_dual]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
h : M✶.IsColoop e
⊢ M.IsLoop e
have rw : M✶✶.IsLoop e
Tactic: rw [← dual_dual M]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
h : M✶.IsLoop e
⊢ M.IsColoop e
have rw : M✶✶.IsColoop e
Tactic: rw [← dual_dual M]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Loop (hypothesis)
Goal:
α : Type u_1
M : Matroid α
e : α
⊢ [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_2 : M.IsColoop e ↔ e ∈ M.coloops
Tactic: tfae_have 1 ↔ 2 := Iff.rfl
-- 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
⊢ [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_3 : M.IsColoop e ↔ M.IsCocircuit {e}
Tactic: tfae_have 1 ↔ 3 := singleton_isCocircuit.symm
-- 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}
⊢ M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
have simp_rw : (∀ (B : Set α), M✶.IsBase B → e ∈ M✶.E \ B) ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
Tactic: simp_rw [← dual_isLoop_iff_isColoop, isLoop_iff_forall_mem_compl_isBase]
-- 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}
⊢ (∀ (B : Set α), M✶.IsBase B → e ∈ M✶.E \ B) ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
have refine : ∀ (h : ∀ (B : Set α), M✶.IsBase B → e ∈ M✶.E \ B) (B : Set α) (hB : M.IsBase B), e ∈ B
Tactic: refine ⟨fun h B hB ↦ ?_, fun h B hB ↦ h hB.compl_isBase_of_dual⟩
-- 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}
⊢ [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_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
Tactic: tfae_have 1 ↔ 4 := by
    simp_rw [← dual_isLoop_iff_isColoop, isLoop_iff_forall_mem_compl_isBase]
    refine ⟨fun h B hB ↦ ?_, fun h B hB ↦ h hB.compl_isBase_of_dual⟩
    obtain ⟨-, heB : e ∈ B⟩ := by simpa using h (M.E \ B) hB.compl_isBase_dual
    assumption
-- 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
⊢ [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_3_to_5 : ∀ (a : M.IsCocircuit {e}), (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
Tactic: tfae_have 3 → 5 := fun h ↦
    ⟨fun C hC heC ↦ hC.inter_isCocircuit_ne_singleton h (e := e) (by simpa), h.subset_ground rfl⟩
-- 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
⊢ ∀ (a : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E) ⦃B : Set α⦄, M.IsBase B → e ∈ B
have refine : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E →
  ∀ (B : Set α) (hB : M.IsBase B) (h : ∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) (heE : e ∈ M.E) (heB : e ∉ B), False
Tactic: refine fun ⟨h, heE⟩ B hB ↦ by_contra fun heB ↦ ?_
-- 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
h_1 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
B : Set α
hB : M.IsBase B
h : ∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C
heE : e ∈ M.E
heB : e ∉ B
⊢ False
have heE₁ : e ∈ M.closure B
Tactic: rw [← hB.closure_eq] at heE
Cleared hypotheses: heE, heB
-- 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
⊢ [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_5_to_4 : ∀ (a : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E) ⦃B : Set α⦄, M.IsBase B → e ∈ B
Tactic: tfae_have 5 → 4 := by
    refine fun ⟨h, heE⟩ B hB ↦ by_contra fun heB ↦ ?_
    rw [← hB.closure_eq] at heE
    obtain ⟨C, -, hC, heC⟩ := (mem_closure_iff_exists_isCircuit heB).1 heE
    exact h hC heC
-- 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
⊢ (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E ↔ ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X
have refine_1 : ∀ (h : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E) (X : Set α) (heX : e ∈ M.closure X) (heX' : e ∉ X), False
Tactic: refine ⟨fun h X ↦ ⟨fun heX ↦ by_contra fun heX' ↦ ?_, fun heX ↦ M.mem_closure_of_mem' heX h.2⟩,
      fun h ↦ ⟨fun C hC heC ↦ ?_, M.closure_subset_ground _ <| (h {e}).2 rfl⟩⟩
-- 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
refine_1 :
  ∀ (h : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E) (X : Set α) (heX : e ∈ M.closure X) (heX' : e ∉ X), False
⊢ (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E ↔ ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X
have refine_2 : ∀ (h : ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X) (C : Set α) (hC : M.IsCircuit C) (heC : e ∈ C), False
Tactic: refine ⟨fun h X ↦ ⟨fun heX ↦ by_contra fun heX' ↦ ?_, fun heX ↦ M.mem_closure_of_mem' heX h.2⟩,
      fun h ↦ ⟨fun C hC heC ↦ ?_, M.closure_subset_ground _ <| (h {e}).2 rfl⟩⟩
-- 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
h : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
X : Set α
heX : e ∈ M.closure X
heX' : e ∉ X
⊢ False
have refine_1 : ∀ (C : Set α) (hC : M.IsCircuit C) (heC : e ∈ C), False
Tactic: obtain ⟨C, -, hC, heC⟩ := (mem_closure_iff_exists_isCircuit heX').1 heX
-- 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
⊢ [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_5_iff_6 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E ↔ ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X
Tactic: tfae_have 5 ↔ 6 := by
    refine ⟨fun h X ↦ ⟨fun heX ↦ by_contra fun heX' ↦ ?_, fun heX ↦ M.mem_closure_of_mem' heX h.2⟩,
      fun h ↦ ⟨fun C hC heC ↦ ?_, M.closure_subset_ground _ <| (h {e}).2 rfl⟩⟩
    · obtain ⟨C, -, hC, heC⟩ := (mem_closure_iff_exists_isCircuit heX').1 heX
      exact h.1 hC heC
    · simpa [hC.mem_closure_diff_singleton_of_mem heC] using h (C \ {e})
-- 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
⊢ M.IsColoop e ↔ ¬M.Spanning (M.E \ {e})
have 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})
Tactic: wlog he : e ∈ M.E