awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
M : Matroid α
hM : ∃ (M_1 : Matroid α), E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I
⊢ M.Indep ∅

Tactic:
M.empty_indep

Premises used: Matroid.empty_indep
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
M : Matroid α
hM : ∃ (M_1 : Matroid α), E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I
⊢ M.Indep ∅

Tactic:
exact M.empty_indep

Premises used: Matroid.empty_indep
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
hM : ∃ (M : Matroid α), E = M.E ∧ ∀ (I : Set α), M.Indep I ↔ Indep I
hex : ∃ (M : Matroid α), E = M.E ∧ M.Indep = Indep
obtain :
  ∀ (M : Matroid α) (hM : ∃ (M_1 : Matroid α), E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I) ⦃I J : Set α⦄,
    M.Indep J → I ⊆ J → M.Indep I
⊢ ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I

Tactic:
obtain ⟨M, -, rfl⟩ := hex

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
M : Matroid α
hM : ∃ (M_1 : Matroid α), E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I
⊢ ∀ ⦃I J : Set α⦄, M.Indep J → I ⊆ J → M.Indep I

Tactic:
fun I J hJ hIJ ↦ hJ.subset hIJ

Premises used: Matroid.Indep.subset
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
M : Matroid α
hM : ∃ (M_1 : Matroid α), E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I
⊢ ∀ ⦃I J : Set α⦄, M.Indep J → I ⊆ J → M.Indep I

Tactic:
exact fun I J hJ hIJ ↦ hJ.subset hIJ
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
hM : ∃ (M : Matroid α), E = M.E ∧ ∀ (I : Set α), M.Indep I ↔ Indep I
hex : ∃ (M : Matroid α), E = M.E ∧ M.Indep = Indep
obtain :
  ∀ (M : Matroid α) (hM : ∃ (M_1 : Matroid α), E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I) ⦃I B : Set α⦄,
    M.Indep I → ¬Maximal M.Indep I → Maximal M.Indep B → ∃ x ∈ B \ I, M.Indep (insert x I)
⊢ ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)

Tactic:
obtain ⟨M, -, rfl⟩ := hex

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
M : Matroid α
hM : ∃ (M_1 : Matroid α), E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I
⊢ ∀ ⦃I B : Set α⦄, M.Indep I → ¬Maximal M.Indep I → Maximal M.Indep B → ∃ x ∈ B \ I, M.Indep (insert x I)

Tactic:
Indep.exists_insert_of_not_maximal M

Premises used: Matroid.Indep.exists_insert_of_not_maximal
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
M : Matroid α
hM : ∃ (M_1 : Matroid α), E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I
⊢ ∀ ⦃I B : Set α⦄, M.Indep I → ¬Maximal M.Indep I → Maximal M.Indep B → ∃ x ∈ B \ I, M.Indep (insert x I)

Tactic:
exact Indep.exists_insert_of_not_maximal M

Premises used: Matroid.Indep.exists_insert_of_not_maximal
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
hM : ∃ (M : Matroid α), E = M.E ∧ ∀ (I : Set α), M.Indep I ↔ Indep I
hex : ∃ (M : Matroid α), E = M.E ∧ M.Indep = Indep
obtain :
  ∀ (M : Matroid α) (hM : ∃ (M_1 : Matroid α), M.E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I),
    ∀ X ⊆ M.E, ExistsMaximalSubsetProperty M.Indep X
⊢ ∀ X ⊆ E, ExistsMaximalSubsetProperty Indep X

Tactic:
obtain ⟨M, rfl, rfl⟩ := hex

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : Matroid α
hM : ∃ (M_1 : Matroid α), M.E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I
⊢ ∀ X ⊆ M.E, ExistsMaximalSubsetProperty M.Indep X

Tactic:
M.existsMaximalSubsetProperty_indep

Premises used: Matroid.existsMaximalSubsetProperty_indep
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : Matroid α
hM : ∃ (M_1 : Matroid α), M.E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I
⊢ ∀ X ⊆ M.E, ExistsMaximalSubsetProperty M.Indep X

Tactic:
exact M.existsMaximalSubsetProperty_indep

Premises used: Matroid.existsMaximalSubsetProperty_indep
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
hM : ∃ (M : Matroid α), E = M.E ∧ ∀ (I : Set α), M.Indep I ↔ Indep I
hex : ∃ (M : Matroid α), E = M.E ∧ M.Indep = Indep
obtain :
  ∀ (M : Matroid α) (hM : ∃ (M_1 : Matroid α), M.E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I) (I : Set α),
    M.Indep I → I ⊆ M.E
⊢ ∀ (I : Set α), Indep I → I ⊆ E

Tactic:
obtain ⟨M, rfl, rfl⟩ := hex

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : Matroid α
hM : ∃ (M_1 : Matroid α), M.E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I
⊢ ∀ (I : Set α), M.Indep I → I ⊆ M.E

Tactic:
fun I ↦ Indep.subset_ground

Premises used: Matroid.Indep.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : Matroid α
hM : ∃ (M_1 : Matroid α), M.E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I
⊢ ∀ (I : Set α), M.Indep I → I ⊆ M.E

Tactic:
exact fun I ↦ Indep.subset_ground

Premises used: Matroid.Indep.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
IsBase : Set α → Prop
exists_finite_base : ∃ (B : Set α), IsBase B ∧ B.Finite
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
obtain : ∀ (B : Set α) (h : IsBase B ∧ B.Finite), ∃ (B : Set α), IsBase B
⊢ ∃ (B : Set α), IsBase B

Tactic:
obtain ⟨B, h⟩ := exists_finite_base
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
IsBase : Set α → Prop
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
B : Set α
h : IsBase B ∧ B.Finite
⊢ ∃ (B : Set α), IsBase B

Tactic:
⟨B, h.1⟩

Premises used: And.left, Exists.intro
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
IsBase : Set α → Prop
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
B : Set α
h : IsBase B ∧ B.Finite
⊢ ∃ (B : Set α), IsBase B

Tactic:
exact ⟨B, h.1⟩
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
IsBase : Set α → Prop
exists_finite_base : ∃ (B : Set α), IsBase B ∧ B.Finite
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
obtain :
  ∀ (B : Set α) (hB : IsBase B) (hfin : B.Finite),
    ∀ X ⊆ E, ExistsMaximalSubsetProperty (fun (x : Set α) ↦ ∃ (B : Set α), IsBase B ∧ x ⊆ B) X
⊢ ∀ X ⊆ E, ExistsMaximalSubsetProperty (fun (x : Set α) ↦ ∃ (B : Set α), IsBase B ∧ x ⊆ B) X

Tactic:
obtain ⟨B, hB, hfin⟩ := exists_finite_base
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
IsBase : Set α → Prop
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
B : Set α
hB : IsBase B
hfin : B.Finite
⊢ ∀ X ⊆ E, ExistsMaximalSubsetProperty (fun (x : Set α) ↦ ∃ (B : Set α), IsBase B ∧ x ⊆ B) X

Tactic:
fun X _ ↦ Matroid.existsMaximalSubsetProperty_of_bdd
      ⟨B.ncard, fun Y ⟨B', hB', hYB'⟩ ↦ ?_⟩ X

Premises used: Matroid.existsMaximalSubsetProperty_of_bdd, Exists.intro, Set.ncard
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
IsBase : Set α → Prop
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
B : Set α
hB : IsBase B
hfin : B.Finite
refine :
  ∀ X ⊆ E,
    ∀ (Y : Set α),
      (∃ (B : Set α), IsBase B ∧ Y ⊆ B) → ∀ (B' : Set α) (hB' : IsBase B') (hYB' : Y ⊆ B'), Y.encard ≤ (↑B.ncard : ℕ∞)
⊢ ∀ X ⊆ E, ExistsMaximalSubsetProperty (fun (x : Set α) ↦ ∃ (B : Set α), IsBase B ∧ x ⊆ B) X

Tactic:
refine fun X _ ↦ Matroid.existsMaximalSubsetProperty_of_bdd
      ⟨B.ncard, fun Y ⟨B', hB', hYB'⟩ ↦ ?_⟩ X

Premises used: Matroid.existsMaximalSubsetProperty_of_bdd, Exists.intro, Set.ncard
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
IsBase : Set α → Prop
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
B : Set α
hB : IsBase B
hfin : B.Finite
X : Set α
h : X ⊆ E
Y : Set α
h_1 : ∃ (B : Set α), IsBase B ∧ Y ⊆ B
B' : Set α
hB' : IsBase B'
hYB' : Y ⊆ B'
rw : Y.encard ≤ B'.encard
⊢ Y.encard ≤ (↑B.ncard : ℕ∞)

Tactic:
rw [hfin.cast_ncard_eq, isBase_exchange.encard_isBase_eq hB hB']

Premises used: Matroid.ExchangeProperty.encard_isBase_eq, Set.Finite.cast_ncard_eq
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
IsBase : Set α → Prop
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
B : Set α
hB : IsBase B
hfin : B.Finite
X : Set α
h : X ⊆ E
Y : Set α
h_1 : ∃ (B : Set α), IsBase B ∧ Y ⊆ B
B' : Set α
hB' : IsBase B'
hYB' : Y ⊆ B'
⊢ Y.encard ≤ B'.encard

Tactic:
encard_mono hYB'

Premises used: Set.encard_mono
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
IsBase : Set α → Prop
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
B : Set α
hB : IsBase B
hfin : B.Finite
X : Set α
h : X ⊆ E
Y : Set α
h_1 : ∃ (B : Set α), IsBase B ∧ Y ⊆ B
B' : Set α
hB' : IsBase B'
hYB' : Y ⊆ B'
⊢ Y.encard ≤ B'.encard

Tactic:
exact encard_mono hYB'

Premises used: Set.encard_mono
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
IsBase : Set α → Prop
exists_finite_base : ∃ (B : Set α), IsBase B ∧ B.Finite
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
⊢ (Matroid.ofExistsFiniteIsBase E IsBase exists_finite_base isBase_exchange subset_ground).IsBase = IsBase

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
IsBase : Set α → Prop
exists_finite_base : ∃ (B : Set α), IsBase B ∧ B.Finite
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
obtain :
  ∀ (B : Set α) (hB : IsBase B) (hfin : B.Finite),
    (Matroid.ofExistsFiniteIsBase E IsBase ⋯ isBase_exchange subset_ground).RankFinite
⊢ (Matroid.ofExistsFiniteIsBase E IsBase exists_finite_base isBase_exchange subset_ground).RankFinite

Tactic:
obtain ⟨B, hB, hfin⟩ := exists_finite_base
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
IsBase : Set α → Prop
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
B : Set α
hB : IsBase B
hfin : B.Finite
⊢ (Matroid.ofExistsFiniteIsBase E IsBase ⋯ isBase_exchange subset_ground).IsBase B

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
IsBase : Set α → Prop
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
B : Set α
hB : IsBase B
hfin : B.Finite
⊢ (Matroid.ofExistsFiniteIsBase E IsBase ⋯ isBase_exchange subset_ground).RankFinite

Tactic:
exact Matroid.IsBase.rankFinite_of_finite (by simpa) hfin

Premises used: Matroid.IsBase.rankFinite_of_finite
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
hE : E.Finite
IsBase : Set α → Prop
exists_isBase : ∃ (B : Set α), IsBase B
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
⊢ (Matroid.ofIsBaseOfFinite (E := E) hE IsBase exists_isBase isBase_exchange subset_ground).E = E

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
hE : E.Finite
IsBase : Set α → Prop
exists_isBase : ∃ (B : Set α), IsBase B
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
⊢ (Matroid.ofIsBaseOfFinite (E := E) hE IsBase exists_isBase isBase_exchange subset_ground).IsBase = IsBase

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
hE : E.Finite
IsBase : Set α → Prop
exists_isBase : ∃ (B : Set α), IsBase B
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
⊢ (Matroid.ofIsBaseOfFinite (E := E) hE IsBase exists_isBase isBase_exchange subset_ground).Finite

Tactic:
⟨hE⟩

Premises used: Matroid.Finite.mk
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
⊢ M.loops ⊆ M.E

Tactic:
M.closure_subset_ground ∅

Premises used: Matroid.closure_subset_ground, EmptyCollection.emptyCollection, Matroid.loops
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
⊢ M.IsLoop e ↔ e ∈ M.loops

Tactic:
Iff.rfl

Premises used: Iff.rfl, Matroid.IsLoop
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
⊢ M.closure ∅ = M.loops

Tactic:
rfl

Premises used: rfl, Matroid.loops
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
he : M.IsLoop e
⊢ e ∈ M.E

Tactic:
closure_subset_ground M ∅ he

Premises used: Matroid.closure_subset_ground, EmptyCollection.emptyCollection
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
⊢ M.IsLoop 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 : α
⊢ e ∈ M.closure ∅

Tactic:
2

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 : α
⊢ M.IsLoop e ↔ e ∈ M.closure ∅

Tactic:
1 ↔ 2

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 : α
⊢ M.IsLoop e ↔ e ∈ M.closure ∅

Tactic:
tfae_have 1 ↔ 2 := Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsLoop e ↔ e ∈ M.closure ∅
⊢ e ∈ M.closure ∅

Tactic:
2

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.IsLoop e ↔ e ∈ M.closure ∅
⊢ M.IsCircuit {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.IsLoop e ↔ e ∈ M.closure ∅
⊢ e ∈ M.closure ∅ ↔ M.IsCircuit {e}

Tactic:
2 ↔ 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.IsLoop e ↔ e ∈ M.closure ∅
⊢ e ∈ M.closure ∅ ↔ M.IsCircuit {e}

Tactic:
simp [M.empty_indep.mem_closure_iff_of_notMem (notMem_empty e),
    isCircuit_def, minimal_iff_forall_ssubset, ssubset_singleton_iff]

Premises used: Set.minimal_iff_forall_ssubset, Matroid.empty_indep, Matroid.isCircuit_def, Matroid.Indep.mem_closure_iff_of_notMem, Set.notMem_empty, Set.ssubset_singleton_iff
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsLoop e ↔ e ∈ M.closure ∅
⊢ e ∈ M.closure ∅ ↔ M.IsCircuit {e}

Tactic:
tfae_have 2 ↔ 3 := by simp [M.empty_indep.mem_closure_iff_of_notMem (notMem_empty e),
    isCircuit_def, minimal_iff_forall_ssubset, ssubset_singleton_iff]
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsLoop e ↔ e ∈ M.closure ∅
tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
⊢ e ∈ M.closure ∅

Tactic:
2

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.IsLoop e ↔ e ∈ M.closure ∅
tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
⊢ M.Dep {e}

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.IsLoop e ↔ e ∈ M.closure ∅
tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
⊢ e ∈ M.closure ∅ ↔ M.Dep {e}

Tactic:
2 ↔ 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.IsLoop e ↔ e ∈ M.closure ∅
tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
⊢ e ∈ M.closure ∅ ↔ M.Dep {e}

Tactic:
simp [M.empty_indep.mem_closure_iff_of_notMem (notMem_empty e)]

Premises used: Matroid.empty_indep, Matroid.Indep.mem_closure_iff_of_notMem, Set.notMem_empty
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsLoop e ↔ e ∈ M.closure ∅
tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
⊢ e ∈ M.closure ∅ ↔ M.Dep {e}

Tactic:
tfae_have 2 ↔ 4 := by simp [M.empty_indep.mem_closure_iff_of_notMem (notMem_empty e)]
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsLoop e ↔ e ∈ M.closure ∅
tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
tfae_2_iff_4 : e ∈ M.closure ∅ ↔ M.Dep {e}
⊢ M.Dep {e}

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.IsLoop e ↔ e ∈ M.closure ∅
tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
tfae_2_iff_4 : e ∈ M.closure ∅ ↔ M.Dep {e}
⊢ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ M.E \ B

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.IsLoop e ↔ e ∈ M.closure ∅
tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
tfae_2_iff_4 : e ∈ M.closure ∅ ↔ M.Dep {e}
⊢ M.Dep {e} ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ M.E \ B

Tactic:
4 ↔ 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.IsLoop e ↔ e ∈ M.closure ∅
tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
tfae_2_iff_4 : e ∈ M.closure ∅ ↔ M.Dep {e}
simp : ¬M.Indep {e} ∧ e ∈ M.E ↔ (∀ (x : Set α) (x : M.IsBase x), e ∈ M.E) ∧ ∀ (x : Set α) (x_1 : M.IsBase x), e ∉ x
⊢ M.Dep {e} ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ M.E \ B

Tactic:
simp only [dep_iff, singleton_subset_iff, mem_diff, forall_and]

Premises used: Set.singleton_subset_iff, Set.mem_diff, Matroid.dep_iff, forall_and
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsLoop e ↔ e ∈ M.closure ∅
tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
tfae_2_iff_4 : e ∈ M.closure ∅ ↔ M.Dep {e}
h : ¬M.Indep {e} ∧ e ∈ M.E
B : Set α
hB : M.IsBase B
heB : e ∈ B
⊢ {e} ⊆ B

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsLoop e ↔ e ∈ M.closure ∅
tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
tfae_2_iff_4 : e ∈ M.closure ∅ ↔ M.Dep {e}
refine :
  ∀ (h : (∀ (x : Set α) (x : M.IsBase x), e ∈ M.E) ∧ ∀ (x : Set α) (x_1 : M.IsBase x), e ∉ x) (hi : M.Indep {e}), False
⊢ ¬M.Indep {e} ∧ e ∈ M.E ↔ (∀ (x : Set α) (x : M.IsBase x), e ∈ M.E) ∧ ∀ (x : Set α) (x_1 : M.IsBase x), e ∉ x

Tactic:
refine ⟨fun h ↦ ⟨fun _ _ ↦ h.2, fun B hB heB ↦ h.1 (hB.indep.subset (by simpa))⟩,
      fun h ↦ ⟨fun hi ↦ ?_, h.1 _ M.exists_isBase.choose_spec⟩⟩
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsLoop e ↔ e ∈ M.closure ∅
tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
tfae_2_iff_4 : e ∈ M.closure ∅ ↔ M.Dep {e}
h : (∀ (x : Set α) (x : M.IsBase x), e ∈ M.E) ∧ ∀ (x : Set α) (x_1 : M.IsBase x), e ∉ x
hi : M.Indep {e}
obtain : ∀ (B : Set α) (hB : M.IsBase B) (heB : {e} ⊆ B), False
⊢ False

Tactic:
obtain ⟨B, hB, heB⟩ := hi.exists_isBase_superset

Premises used: Matroid.Indep.exists_isBase_superset
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsLoop e ↔ e ∈ M.closure ∅
tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
tfae_2_iff_4 : e ∈ M.closure ∅ ↔ M.Dep {e}
h : (∀ (x : Set α) (x : M.IsBase x), e ∈ M.E) ∧ ∀ (x : Set α) (x_1 : M.IsBase x), e ∉ x
hi : M.Indep {e}
B : Set α
hB : M.IsBase B
heB : {e} ⊆ B
⊢ e ∈ B

Tactic:
simpa using heB
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsLoop e ↔ e ∈ M.closure ∅
tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
tfae_2_iff_4 : e ∈ M.closure ∅ ↔ M.Dep {e}
h : (∀ (x : Set α) (x : M.IsBase x), e ∈ M.E) ∧ ∀ (x : Set α) (x_1 : M.IsBase x), e ∉ x
hi : M.Indep {e}
B : Set α
hB : M.IsBase B
heB : {e} ⊆ B
⊢ False

Tactic:
exact h.2 _ hB (by simpa using heB)

Premises used: And.right
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsLoop e ↔ e ∈ M.closure ∅
tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
tfae_2_iff_4 : e ∈ M.closure ∅ ↔ M.Dep {e}
⊢ M.Dep {e} ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ M.E \ B

Tactic:
tfae_have 4 ↔ 5 := by
    simp only [dep_iff, singleton_subset_iff, mem_diff, forall_and]
    refine ⟨fun h ↦ ⟨fun _ _ ↦ h.2, fun B hB heB ↦ h.1 (hB.indep.subset (by simpa))⟩,
      fun h ↦ ⟨fun hi ↦ ?_, h.1 _ M.exists_isBase.choose_spec⟩⟩
    obtain ⟨B, hB, heB⟩ := hi.exists_isBase_superset
    exact h.2 _ hB (by simpa using heB)
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsLoop e ↔ e ∈ M.closure ∅
tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
tfae_2_iff_4 : e ∈ M.closure ∅ ↔ M.Dep {e}
tfae_4_iff_5 : M.Dep {e} ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ M.E \ B
⊢ [M.IsLoop e, e ∈ M.closure ∅, M.IsCircuit {e}, M.Dep {e}, ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ M.E \ B].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
⊢ M.Dep {e} ↔ M.IsLoop e

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

Premises used: Matroid.isLoop_tfae, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
rw : ¬M.Indep {e} ↔ M.Dep {e}
rw₁ rw₂ : ¬M.Indep {e} ↔ ¬M.Indep {e}
⊢ ¬M.Indep {e} ↔ M.IsLoop e

Tactic:
rw [← singleton_dep, ← not_indep_iff]

Premises used: Matroid.singleton_dep, Matroid.not_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
⊢ M.IsCircuit {e} ↔ M.IsLoop e

Tactic:
(M.isLoop_tfae e).out 2 0

Premises used: Matroid.isLoop_tfae, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
⊢ M.IsLoop e ↔ ∀ (B : Set α), M.IsBase B → e ∈ M.E \ B

Tactic:
(M.isLoop_tfae e).out 0 4

Premises used: Matroid.isLoop_tfae, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
simp_rw : (∀ (B : Set α), M.IsBase B → e ∈ M.E \ B) ↔ ∀ (B : Set α), M.IsBase B → e ∉ B
simp_rw₁ : (∀ (B : Set α), M.IsBase B → e ∈ M.E ∧ e ∉ B) ↔ ∀ (B : Set α), M.IsBase B → e ∉ B
⊢ M.IsLoop e ↔ ∀ (B : Set α), M.IsBase B → e ∉ B

Tactic:
simp_rw [isLoop_iff_forall_mem_compl_isBase, mem_diff, and_iff_right he]

Premises used: and_iff_right, Matroid.isLoop_iff_forall_mem_compl_isBase, Set.mem_diff
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
he : M.IsLoop e
X : Set α
⊢ e ∈ M.closure X

Tactic:
M.closure_mono (empty_subset _) he

Premises used: Matroid.closure_mono, Set.empty_subset
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
he : M.IsLoop e
F : Set α
hF : M.IsFlat F
⊢ e ∈ F

Tactic:
hF.closure ▸ he.mem_closure F

Premises used: Eq.rec, Matroid.IsLoop.mem_closure, Matroid.IsFlat.closure
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
F : Set α
hF : M.IsFlat F
⊢ M.loops ⊆ F

Tactic:
fun _ he ↦ IsLoop.mem_of_isFlat he hF

Premises used: Matroid.IsLoop.mem_of_isFlat, Set.Subset
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
X : Set α
he : M.IsLoop e
h : e ∈ X
hXE : X ⊆ M.E
⊢ M.Dep X

Tactic:
he.dep.superset (singleton_subset_iff.mpr h) hXE

Premises used: Iff.mpr, Set.singleton_subset_iff, Matroid.Dep.superset, Matroid.IsLoop.dep