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}
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.IsColoop e ↔ ¬M.Spanning (M.E \ {e})

Tactic:
exact iff_of_false (fun h ↦ he h.mem_ground) <| by simp [he, M.ground_spanning]

Premises used: iff_of_false
-- Module: Mathlib.Combinatorics.Matroid.Loop
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
⊢ {e} ⊆ M.E

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Loop
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
⊢ {e} ⊆ M✶.E

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Loop
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}
rw₄ rw₅ : ¬M✶.Indep {e} ↔ ¬M.Coindep {e}
⊢ M.IsColoop e ↔ ¬M.Spanning (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)]

Premises used: Set.diff_subset, Matroid.spanning_iff_compl_coindep, Matroid.dual_isLoop_iff_isColoop, Set.diff_diff_cancel_left, Matroid.singleton_dep, Matroid.not_indep_iff
-- 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:
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)]
-- 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
tfae_1_iff_7 : M.IsColoop e ↔ ¬M.Spanning (M.E \ {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

Tactic:
tfae_finish
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
⊢ M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B

Tactic:
(M.isColoop_tfae e).out 0 3

Premises used: List.TFAE.out, Matroid.isColoop_tfae, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : M.IsColoop e
⊢ e ∈ B

Tactic:
isColoop_iff_forall_mem_isBase.mp he hB

Premises used: Matroid.isColoop_iff_forall_mem_isBase, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
he : M.IsColoop e
hB : M.IsBase B
⊢ e ∈ B

Tactic:
isColoop_iff_forall_mem_isBase.mp he hB

Premises used: Matroid.isColoop_iff_forall_mem_isBase, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
⊢ M.coloops ⊆ B

Tactic:
fun _ he ↦ IsColoop.mem_of_isBase he hB

Premises used: Set.Subset, Matroid.IsColoop.mem_of_isBase
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
h : M.IsColoop e
⊢ M.IsNonloop e

Tactic:
let ⟨_, hB⟩ := M.exists_isBase
  hB.indep.isNonloop_of_mem ((isColoop_iff_forall_mem_isBase.mp h) hB)

Premises used: Matroid.IsNonloop, Matroid.isColoop_iff_forall_mem_isBase, Matroid.exists_isBase, Iff.mp, Matroid.Indep.isNonloop_of_mem, Matroid.IsBase.indep, _private.0.Matroid.exists_isNonloop.match_1
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
h : M.IsLoop e
⊢ M✶.IsColoop e

Tactic:
rw [← dual_dual M, dual_isLoop_iff_isColoop] at h

Premises used: Matroid.dual_isLoop_iff_isColoop, Matroid.dual_dual
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
h : M✶.IsColoop e
⊢ ¬M✶.IsLoop e

Tactic:
h.isNonloop.not_isLoop

Premises used: Matroid.IsColoop.isNonloop, Matroid.IsNonloop.not_isLoop
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
h : M✶.IsColoop e
⊢ ¬M✶.IsLoop e

Tactic:
exact h.isNonloop.not_isLoop

Premises used: Matroid.IsColoop.isNonloop, Matroid.IsNonloop.not_isLoop
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
C : Set α
he : M.IsColoop e
hC : M.IsCircuit C
⊢ e ∉ C

Tactic:
fun h ↦ (hC.isCocircuit.isNonloop_of_mem h).not_isLoop he

Premises used: Matroid.IsCircuit.isCocircuit, Matroid.IsNonloop.not_isLoop, Matroid.IsCocircuit.isNonloop_of_mem, Not
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
⊢ Disjoint C M.coloops

Tactic:
disjoint_right.2 <| fun _ he ↦ IsColoop.notMem_isCircuit he hC

Premises used: Iff.mpr, Matroid.IsColoop.notMem_isCircuit, Set.disjoint_right
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
simp_rw : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E ↔ ∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C
⊢ M.IsColoop e ↔ ∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C

Tactic:
simp_rw [(M.isColoop_tfae e).out 0 4, and_iff_left he]

Premises used: and_iff_left, List.TFAE.out, Matroid.isColoop_tfae, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Matroid.Loop
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
neg : ∀ (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

Tactic:
by_cases he : e ∈ M.E

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

Tactic:
simp [isColoop_iff_forall_notMem_isCircuit, he]

Premises used: Matroid.isColoop_iff_forall_notMem_isCircuit
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
inst : M✶.RankPos
he : e ∉ M.E
neg : ∀ (C : Set α) (hC : M.IsCircuit C), M.IsColoop e ↔ ∀ (C : Set α), M.IsCircuit C → e ∈ M.E \ C
⊢ M.IsColoop e ↔ ∀ (C : Set α), M.IsCircuit C → e ∈ M.E \ C

Tactic:
obtain ⟨C, hC⟩ := M.exists_isCircuit

Premises used: Matroid.exists_isCircuit
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
inst : M✶.RankPos
he : e ∉ M.E
C : Set α
hC : M.IsCircuit C
⊢ M.IsColoop e ↔ ∀ (C : Set α), M.IsCircuit C → e ∈ M.E \ C

Tactic:
iff_of_false (fun h ↦ he h.mem_ground) fun h ↦ he (h C hC).1

Premises used: Matroid.IsColoop.mem_ground, iff_of_false, And.left
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
inst : M✶.RankPos
he : e ∉ M.E
C : Set α
hC : M.IsCircuit C
⊢ M.IsColoop e ↔ ∀ (C : Set α), M.IsCircuit C → e ∈ M.E \ C

Tactic:
exact iff_of_false (fun h ↦ he h.mem_ground) fun h ↦ he (h C hC).1

Premises used: iff_of_false
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
C : Set α
hC : M.IsCircuit C
heC : e ∈ C
⊢ ¬M.IsColoop e

Tactic:
fun h ↦ h.notMem_isCircuit hC heC

Premises used: Matroid.IsColoop.notMem_isCircuit, Not
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
⊢ M.IsColoop e ↔ ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X

Tactic:
(M.isColoop_tfae e).out 0 5

Premises used: List.TFAE.out, Matroid.isColoop_tfae, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
⊢ M.IsColoop e ↔ (∀ X ⊆ M.E, e ∈ M.closure X ↔ e ∈ X) ∧ e ∈ M.E

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

Premises used: Iff.mpr, Matroid.isColoop_iff_forall_mem_closure_iff_mem, Matroid.IsColoop.mem_ground, Matroid.IsColoop, And.intro, Iff.intro, Iff.mp, _private.0.Matroid.isColoop_iff_forall_mem_closure_iff_mem'.match_1
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
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
⊢ M.IsColoop e ↔ (∀ X ⊆ M.E, e ∈ M.closure X ↔ e ∈ X) ∧ e ∈ M.E

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 ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Loop
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
rw₃ rw₄ : e ∈ X ↔ e ∈ X
⊢ e ∈ M.closure X ↔ e ∈ X

Tactic:
rw [← closure_inter_ground, h _ inter_subset_right, mem_inter_iff, and_iff_left he]

Premises used: Set.mem_inter_iff, and_iff_left, Matroid.closure_inter_ground, Set.inter_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
X : Set α
he : M.IsColoop e
⊢ e ∈ M.closure X ↔ e ∈ X

Tactic:
(isColoop_iff_forall_mem_closure_iff_mem.1 he) X

Premises used: Matroid.isColoop_iff_forall_mem_closure_iff_mem, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
X : Set α
he : M.IsColoop e
heX : e ∈ M.closure X
⊢ e ∈ X

Tactic:
he.mem_closure_iff_mem.1 heX

Premises used: Iff.mp, Matroid.IsColoop.mem_closure_iff_mem
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
⊢ M.IsColoop e ↔ ¬M.Spanning (M.E \ {e})

Tactic:
(M.isColoop_tfae e).out 0 6

Premises used: List.TFAE.out, Matroid.isColoop_tfae, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
rw : ¬M.Spanning (M.E \ {e}) ↔ M.closure (M.E \ {e}) ≠ M.E
rw₁ rw₂ : ¬M.closure (M.E \ {e}) = M.E ↔ M.closure (M.E \ {e}) ≠ M.E
⊢ M.IsColoop e ↔ M.closure (M.E \ {e}) ≠ M.E

Tactic:
rw [isColoop_iff_diff_not_spanning, spanning_iff_closure_eq]

Premises used: Matroid.isColoop_iff_diff_not_spanning, Matroid.spanning_iff_closure_eq
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
rw : M.closure (M.E \ {e}) = M.E ↔ e ∈ M.closure (M.E \ {e})
⊢ M.IsColoop e ↔ e ∉ M.closure (M.E \ {e})

Tactic:
rw [isColoop_iff_diff_closure, not_iff_not]

Premises used: not_iff_not, Matroid.isColoop_iff_diff_closure
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
h : M.closure (M.E \ {e}) = M.E
rwa rwa₁ rwa₂ rwa₃ : e ∈ M.E
⊢ e ∈ M.closure (M.E \ {e})

Tactic:
rwa [h]
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
refine : ∀ (h : e ∈ M.closure (M.E \ {e})) (x : α) (hx : x ∈ M.E), x ∈ M.closure (M.E \ {e})
⊢ M.closure (M.E \ {e}) = M.E ↔ e ∈ M.closure (M.E \ {e})

Tactic:
refine ⟨fun h ↦ by rwa [h], fun h ↦ (M.closure_subset_ground _).antisymm fun x hx ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Loop
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})
inr : ∀ (hne : x ≠ e), x ∈ M.closure (M.E \ {e})
⊢ x ∈ M.closure (M.E \ {e})

Tactic:
obtain (rfl | hne) := eq_or_ne x e

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
x : α
hx he : x ∈ M.E
h : x ∈ M.closure (M.E \ {x})
⊢ x ∈ M.closure (M.E \ {x})

Tactic:
assumption
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
h : e ∈ M.closure (M.E \ {e})
x : α
hx : x ∈ M.E
hne : x ≠ e
⊢ x ∈ M.closure (M.E \ {e})

Tactic:
M.subset_closure (M.E \ {e}) diff_subset (show x ∈ M.E \ {e} from ⟨hx, hne⟩)

Premises used: Set.diff_subset, Matroid.E, Matroid.subset_closure, SDiff.sdiff, And.intro, Singleton.singleton
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
h : e ∈ M.closure (M.E \ {e})
x : α
hx : x ∈ M.E
hne : x ≠ e
⊢ x ∈ M.closure (M.E \ {e})

Tactic:
exact M.subset_closure (M.E \ {e}) diff_subset (show x ∈ M.E \ {e} from ⟨hx, hne⟩)

Premises used: Set.diff_subset, Matroid.E, Matroid.subset_closure, SDiff.sdiff, And.intro, Singleton.singleton
-- Module: Mathlib.Combinatorics.Matroid.Loop
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

Tactic:
⟨fun h x hx heC ↦ (h.notMem_isCircuit <| hB.fundCircuit_isCircuit hx.1 hx.2) heC,
    fun h ↦ ?_⟩

Premises used: Matroid.IsColoop.notMem_isCircuit, And.right, And.left, Matroid.IsBase.fundCircuit_isCircuit, Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
refine : ∀ (h : ∀ x ∈ M.E \ B, e ∉ M.fundCircuit x B), M.IsColoop e
⊢ M.IsColoop e ↔ ∀ x ∈ M.E \ B, e ∉ M.fundCircuit x B

Tactic:
refine ⟨fun h x hx heC ↦ (h.notMem_isCircuit <| hB.fundCircuit_isCircuit hx.1 hx.2) heC,
    fun h ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Loop
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})
inr : ∀ (hx : x ∉ B), x ∈ M.closure (B \ {e})
⊢ x ∈ M.closure (B \ {e})

Tactic:
obtain (hx | hx) := em (x ∈ B)

Premises used: Membership.mem, em
-- Module: Mathlib.Combinatorics.Matroid.Loop
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})

Tactic:
M.subset_closure (B \ {e}) (diff_subset.trans hB.subset_ground) ⟨hx, hne⟩

Premises used: Set.diff_subset, HasSubset.Subset.trans, Matroid.subset_closure, Matroid.IsBase.subset_ground, SDiff.sdiff, And.intro, Singleton.singleton
-- Module: Mathlib.Combinatorics.Matroid.Loop
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})

Tactic:
exact M.subset_closure (B \ {e}) (diff_subset.trans hB.subset_ground) ⟨hx, hne⟩

Premises used: Set.diff_subset, HasSubset.Subset.trans, Matroid.subset_closure, Matroid.IsBase.subset_ground, SDiff.sdiff, And.intro, Singleton.singleton
-- Module: Mathlib.Combinatorics.Matroid.Loop
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 (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)
-- Module: Mathlib.Combinatorics.Matroid.Loop
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})

Tactic:
(M.closure_subset_closure (subset_diff_singleton ?_ ?_)) h_cct

Premises used: Matroid.closure_subset_closure, Set.subset_diff_singleton
-- Module: Mathlib.Combinatorics.Matroid.Loop
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
inr₁ : e ∉ M.fundCircuit x B \ {x}
⊢ x ∈ M.closure (B \ {e})

Tactic:
refine (M.closure_subset_closure (subset_diff_singleton ?_ ?_)) h_cct

Premises used: Matroid.closure_subset_closure, Set.subset_diff_singleton
-- Module: Mathlib.Combinatorics.Matroid.Loop
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})
⊢ M.fundCircuit x B \ {x} ⊆ B

Tactic:
simpa using fundCircuit_subset_insert ..

Premises used: Matroid.fundCircuit_subset_insert
-- Module: Mathlib.Combinatorics.Matroid.Loop
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})
⊢ e ∉ M.fundCircuit x B \ {x}

Tactic:
simp [hne.symm, h x ⟨hxE, hx⟩]

Premises used: Ne.symm, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Loop
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.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⟩]
-- Module: Mathlib.Combinatorics.Matroid.Loop
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})
rw : e ∉ M.closure (M.E \ {e})
⊢ M.IsColoop e

Tactic:
rw [isColoop_iff_notMem_closure_compl (hB.subset_ground he)]

Premises used: Matroid.IsBase.subset_ground, Matroid.isColoop_iff_notMem_closure_compl
-- Module: Mathlib.Combinatorics.Matroid.Loop
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})
⊢ e ∉ M.closure (M.E \ {e})

Tactic:
notMem_subset (M.closure_subset_closure_of_subset_closure h') <|
    hB.indep.notMem_closure_diff_of_mem he

Premises used: Matroid.closure_subset_closure_of_subset_closure, Matroid.Indep.notMem_closure_diff_of_mem, Matroid.IsBase.indep, Set.notMem_subset
-- Module: Mathlib.Combinatorics.Matroid.Loop
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})
⊢ e ∉ M.closure (M.E \ {e})

Tactic:
exact notMem_subset (M.closure_subset_closure_of_subset_closure h') <|
    hB.indep.notMem_closure_diff_of_mem he

Premises used: Matroid.closure_subset_closure_of_subset_closure, Matroid.Indep.notMem_closure_diff_of_mem, Matroid.IsBase.indep, Set.notMem_subset
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
X I : Set α
hIX : M.IsBasis' I X
e : α
this : ∀ (heX : e ∈ X) (heI : M.IsColoop e), e ∈ I
⊢ e ∈ X ∩ M.coloops → e ∈ I

Tactic:
⟨heX, (heI : M.IsColoop e)⟩
-- Module: Mathlib.Combinatorics.Matroid.Loop
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
rwa₁ : e ∈ M.closure X
rwa₂ rwa₃ rwa₄ rwa₅ : e ∈ X
⊢ e ∈ I

Tactic:
rwa [← heI.mem_closure_iff_mem, hIX.isBasis_closure_right.closure_eq_right,
    heI.mem_closure_iff_mem]

Premises used: Matroid.IsBasis.closure_eq_right, Matroid.IsColoop.mem_closure_iff_mem, Matroid.IsBasis'.isBasis_closure_right
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
X I : Set α
hIX : M.IsBasis I X
⊢ X ∩ M.coloops ⊆ I

Tactic:
hIX.isBasis'.inter_coloops_subset

Premises used: Matroid.IsBasis.isBasis', Matroid.IsBasis'.inter_coloops_subset
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
heE : e ∈ M.E
he : ¬M.IsColoop e
⊢ ∃ (x : Set α), M.IsBase x ∧ e ∉ x

Tactic:
simp only [isColoop_iff_forall_mem_isBase, not_forall, exists_prop] at he

Premises used: exists_prop, Matroid.isColoop_iff_forall_mem_isBase, Classical.not_forall
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
heE : e ∈ M.E
he : ∃ (x : Set α), M.IsBase x ∧ e ∉ x
obtain : ∀ (B : Set α) (hB : M.IsBase B) (heB : e ∉ B), ∃ (C : Set α), M.IsCircuit C ∧ e ∈ C
⊢ ∃ (C : Set α), M.IsCircuit C ∧ e ∈ C

Tactic:
obtain ⟨B, hB, heB⟩ := he
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
heE : e ∈ M.E
B : Set α
hB : M.IsBase B
heB : e ∉ B
⊢ ∃ (C : Set α), M.IsCircuit C ∧ e ∈ C

Tactic:
⟨M.fundCircuit e B, hB.fundCircuit_isCircuit heE heB, .inl rfl⟩

Premises used: Matroid.IsBase.fundCircuit_isCircuit, And.intro, Exists.intro, Matroid.fundCircuit, Or.inl, rfl
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
heE : e ∈ M.E
B : Set α
hB : M.IsBase B
heB : e ∉ B
⊢ ∃ (C : Set α), M.IsCircuit C ∧ e ∈ C

Tactic:
exact ⟨M.fundCircuit e B, hB.fundCircuit_isCircuit heE heB, .inl rfl⟩
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
X : Set α
simp_rw : ∀ (x : α), M.IsColoop x → (x ∈ M.closure X ↔ x ∈ X)
⊢ M.closure X ∩ M.coloops = X ∩ M.coloops

Tactic:
simp_rw [Set.ext_iff, mem_inter_iff, ← isColoop_iff_mem_coloops, and_congr_left_iff]

Premises used: Set.mem_inter_iff, and_congr_left_iff, Set.ext_iff, Matroid.isColoop_iff_mem_coloops