awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Loop
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 ∈ B

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Combinatorics.Matroid.Loop
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

Tactic:
1 ↔ 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Combinatorics.Matroid.Loop
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}
simp_rw : (∀ (B : Set α), M✶.IsBase B → e ∈ M✶.E \ B) ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
⊢ M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B

Tactic:
simp_rw [← dual_isLoop_iff_isColoop, isLoop_iff_forall_mem_compl_isBase]

Premises used: Matroid.dual_isLoop_iff_isColoop, Matroid.isLoop_iff_forall_mem_compl_isBase
-- Module: Mathlib.Combinatorics.Matroid.Loop
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

Tactic:
⟨fun h B hB ↦ ?_, fun h B hB ↦ h hB.compl_isBase_of_dual⟩

Premises used: Matroid.IsBase.compl_isBase_of_dual, Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.Loop
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}
refine : ∀ (h : ∀ (B : Set α), M✶.IsBase B → e ∈ M✶.E \ B) (B : Set α) (hB : M.IsBase B), e ∈ B
⊢ (∀ (B : Set α), M✶.IsBase B → e ∈ M✶.E \ B) ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B

Tactic:
refine ⟨fun h B hB ↦ ?_, fun h B hB ↦ h hB.compl_isBase_of_dual⟩
-- Module: Mathlib.Combinatorics.Matroid.Loop
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}
h : ∀ (B : Set α), M✶.IsBase B → e ∈ M✶.E \ B
B : Set α
hB : M.IsBase B
⊢ e ∈ M.E ∧ e ∈ B

Tactic:
simpa using h (M.E \ B) hB.compl_isBase_dual

Premises used: Matroid.E, Matroid.IsBase.compl_isBase_dual, SDiff.sdiff
-- Module: Mathlib.Combinatorics.Matroid.Loop
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}
h : ∀ (B : Set α), M✶.IsBase B → e ∈ M✶.E \ B
B : Set α
hB : M.IsBase B
⊢ e ∈ B

Tactic:
obtain ⟨-, heB : e ∈ B⟩ := by simpa using h (M.E \ B) hB.compl_isBase_dual
-- Module: Mathlib.Combinatorics.Matroid.Loop
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

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
-- Module: Mathlib.Combinatorics.Matroid.Loop
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.IsCocircuit {e}

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Combinatorics.Matroid.Loop
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
⊢ (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Combinatorics.Matroid.Loop
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
⊢ ∀ (a : M.IsCocircuit {e}), (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E

Tactic:
3 → 5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Combinatorics.Matroid.Loop
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
h : M.IsCocircuit {e}
C : Set α
hC : M.IsCircuit C
heC : e ∈ C
⊢ C ∩ {e} = {e}

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Loop
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
⊢ ∀ (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⟩
-- Module: Mathlib.Combinatorics.Matroid.Loop
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
⊢ (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Combinatorics.Matroid.Loop
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
⊢ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Combinatorics.Matroid.Loop
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

Tactic:
5 → 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Combinatorics.Matroid.Loop
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

Tactic:
fun ⟨h, heE⟩ B hB ↦ by_contra fun heB ↦ ?_

Premises used: Membership.mem, _private.0.Matroid.isColoop_tfae.match_1, by_contra
-- Module: Mathlib.Combinatorics.Matroid.Loop
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
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
⊢ ∀ (a : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E) ⦃B : Set α⦄, M.IsBase B → e ∈ B

Tactic:
refine fun ⟨h, heE⟩ B hB ↦ by_contra fun heB ↦ ?_
-- Module: Mathlib.Combinatorics.Matroid.Loop
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
⊢ e ∈ M.closure B

Tactic:
rw [← hB.closure_eq] at heE

Premises used: Matroid.IsBase.closure_eq
-- Module: Mathlib.Combinatorics.Matroid.Loop
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
heE₁ : e ∈ M.closure B
⊢ e ∉ B

Tactic:
rw [← hB.closure_eq] at heE

Premises used: Matroid.IsBase.closure_eq
-- Module: Mathlib.Combinatorics.Matroid.Loop
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.closure B
heB : e ∉ B
obtain : ∀ (C : Set α) (hC : M.IsCircuit C) (heC : e ∈ C), False
⊢ False

Tactic:
obtain ⟨C, -, hC, heC⟩ := (mem_closure_iff_exists_isCircuit heB).1 heE

Premises used: Iff.mp, Matroid.mem_closure_iff_exists_isCircuit
-- Module: Mathlib.Combinatorics.Matroid.Loop
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.closure B
heB : e ∉ B
C : Set α
hC : M.IsCircuit C
heC : e ∈ C
⊢ False

Tactic:
h hC heC
-- Module: Mathlib.Combinatorics.Matroid.Loop
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.closure B
heB : e ∉ B
C : Set α
hC : M.IsCircuit C
heC : e ∈ C
⊢ False

Tactic:
exact h hC heC
-- Module: Mathlib.Combinatorics.Matroid.Loop
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

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
-- Module: Mathlib.Combinatorics.Matroid.Loop
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

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Combinatorics.Matroid.Loop
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
⊢ ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X

Tactic:
6

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Combinatorics.Matroid.Loop
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

Tactic:
5 ↔ 6

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Combinatorics.Matroid.Loop
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

Tactic:
⟨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⟩⟩

Premises used: Iff.mpr, Matroid.closure_subset_ground, Matroid.mem_closure_of_mem', And.right, And.intro, Iff.intro, by_contra, Singleton.singleton, rfl
-- Module: Mathlib.Combinatorics.Matroid.Loop
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
refine_2 : ∀ (h : ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X) (C : Set α) (hC : M.IsCircuit C) (heC : e ∈ C), False
⊢ (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E ↔ ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X

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⟩⟩
-- Module: Mathlib.Combinatorics.Matroid.Loop
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
refine_1 : ∀ (C : Set α) (hC : M.IsCircuit C) (heC : e ∈ C), False
⊢ False

Tactic:
obtain ⟨C, -, hC, heC⟩ := (mem_closure_iff_exists_isCircuit heX').1 heX

Premises used: Iff.mp, Matroid.mem_closure_iff_exists_isCircuit
-- Module: Mathlib.Combinatorics.Matroid.Loop
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
C : Set α
hC : M.IsCircuit C
heC : e ∈ C
⊢ False

Tactic:
h.1 hC heC

Premises used: And.left
-- Module: Mathlib.Combinatorics.Matroid.Loop
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
C : Set α
hC : M.IsCircuit C
heC : e ∈ C
⊢ False

Tactic:
exact h.1 hC heC

Premises used: And.left
-- Module: Mathlib.Combinatorics.Matroid.Loop
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 : ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X
C : Set α
hC : M.IsCircuit C
heC : e ∈ C
⊢ False

Tactic:
simpa [hC.mem_closure_diff_singleton_of_mem heC] using h (C \ {e})

Premises used: Matroid.IsCircuit.mem_closure_diff_singleton_of_mem, SDiff.sdiff, Singleton.singleton
-- Module: Mathlib.Combinatorics.Matroid.Loop
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

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})
-- Module: Mathlib.Combinatorics.Matroid.Loop
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

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Combinatorics.Matroid.Loop
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.Spanning (M.E \ {e})

Tactic:
7

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Combinatorics.Matroid.Loop
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})

Tactic:
1 ↔ 7

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Combinatorics.Matroid.Loop
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})
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})
⊢ M.IsColoop e ↔ ¬M.Spanning (M.E \ {e})

Tactic:
wlog he : e ∈ M.E

Premises used: Matroid.E
-- Module: Mathlib.Combinatorics.Matroid.Loop
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
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.Spanning (M.E \ {e})

Tactic:
simp [he, M.ground_spanning]

Premises used: Matroid.ground_spanning