awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
X : Set α
h : e ∉ M.closure X
he : e ∈ M.E
⊢ M.IsNonloop e

Tactic:
isNonloop_of_not_isLoop he (fun hel ↦ h (hel.mem_closure X))

Premises used: Matroid.IsLoop.mem_closure, Matroid.isNonloop_of_not_isLoop
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
rw : ¬M.IsLoop e ∧ e ∈ M.E ↔ e ∉ M.loops
rw₁ : e ∉ M.loops ∧ e ∈ M.E ↔ e ∉ M.loops
rw₂ rw₃ : e ∉ M.loops ↔ e ∉ M.loops
⊢ M.IsNonloop e ↔ e ∉ M.loops

Tactic:
rw [isNonloop_iff, isLoop_iff, and_iff_left he]

Premises used: and_iff_left, Matroid.isLoop_iff, Matroid.isNonloop_iff
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
rw : ∀ (hef : e ∈ M.closure (insert f ∅)), f ∈ M.closure (insert e ∅)
⊢ f ∈ M.closure {e}

Tactic:
rw [← union_empty {_}, singleton_union] at *

Premises used: Set.union_empty, Set.singleton_union, Singleton.singleton
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure (insert f ∅)
⊢ f ∈ M.closure (insert e ∅)

Tactic:
(M.closure_exchange (X := ∅)
    ⟨hef, (isNonloop_iff_notMem_loops he.mem_ground).1 he⟩).1

Premises used: Matroid.IsNonloop.mem_ground, Matroid.closure_exchange, Matroid.isNonloop_iff_notMem_loops, And.left, And.intro, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure (insert f ∅)
⊢ f ∈ M.closure (insert e ∅)

Tactic:
exact (M.closure_exchange (X := ∅)
    ⟨hef, (isNonloop_iff_notMem_loops he.mem_ground).1 he⟩).1

Premises used: Matroid.IsNonloop.mem_ground, Matroid.closure_exchange, Matroid.isNonloop_iff_notMem_loops, And.left, And.intro, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hf : M.IsNonloop f
⊢ f ∈ M.closure {e} ↔ e ∈ M.closure {f}

Tactic:
⟨hf.mem_closure_singleton, he.mem_closure_singleton⟩

Premises used: Matroid.IsNonloop.mem_closure_singleton, Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
rw : f ∈ M.E ∧ ¬M.IsLoop f
⊢ M.IsNonloop f

Tactic:
rw [isNonloop_iff, and_comm]

Premises used: and_comm, Matroid.isNonloop_iff
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
by_contra! : ∀ (h : ∀ (_ : f ∈ M.E), M.IsLoop f), False
⊢ f ∈ M.E ∧ ¬M.IsLoop f

Tactic:
by_contra! h
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
h : ∀ (_ : f ∈ M.E), M.IsLoop f
apply : M.IsLoop e
⊢ False

Tactic:
apply he.not_isLoop

Premises used: Matroid.IsNonloop.not_isLoop
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
h : ∀ (_ : f ∈ M.E), M.IsLoop f
⊢ ∀ (_ : f ∈ M.E), f ∈ M.loops

Tactic:
rw [isLoop_iff] at *

Premises used: Matroid.isLoop_iff
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
h : ∀ (_ : f ∈ M.E), f ∈ M.loops
⊢ e ∈ M.closure {f}

Tactic:
hef
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
h : ∀ (_ : f ∈ M.E), f ∈ M.loops
h₁ : M.loops = M.closure {f}
⊢ e ∈ M.loops

Tactic:
convert! hef using 1
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
h : ∀ (_ : f ∈ M.E), f ∈ M.loops
h₁ : ∀ (hf : f ∈ M.E), M.loops = M.closure {f}
h₂ : ∀ (hf : f ∉ M.E), M.loops = M.closure {f}
⊢ M.loops = M.closure {f}

Tactic:
obtain (hf | hf) := em (f ∈ M.E)

Premises used: Matroid.E, Membership.mem, em
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
h : ∀ (_ : f ∈ M.E), f ∈ M.loops
hf : f ∈ M.E
h₁ : M.closure M.loops = M.closure {f}
h₂ : M.closure (insert f M.loops) = M.closure {f}
h₃ : M.closure (insert f ∅) = M.closure {f}
h₄ h₅ : M.closure {f} = M.closure {f}
⊢ M.loops = M.closure {f}

Tactic:
rw [← closure_loops, ← insert_eq_of_mem (h hf), closure_insert_congr_right M.closure_loops,
      insert_empty_eq]

Premises used: Matroid.closure_loops, Set.insert_eq_of_mem, LawfulSingleton.insert_empty_eq, Matroid.closure_insert_congr_right
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
h : ∀ (_ : f ∈ M.E), f ∈ M.loops
hf : f ∉ M.E
h₁ : M.closure {f} = M.loops
h₂ : M.closure ({f} ∩ M.E) = M.loops
h₃ : M.closure (M.E ∩ {f}) = M.loops
h₄ : M.closure ∅ = M.loops
h₅ h₆ : M.closure ∅ = M.closure ∅
⊢ M.loops = M.closure {f}

Tactic:
rw [eq_comm, ← closure_inter_ground, inter_comm, inter_singleton_eq_empty.mpr hf, loops]

Premises used: Iff.mpr, Set.inter_singleton_eq_empty, eq_comm, Set.inter_comm, Matroid.closure_inter_ground, Matroid.loops
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
rw : M.closure {e} = M.closure (M.closure {f})
rw₁ : M.closure {e} = M.closure (insert e (M.closure {f}))
rw₂ : M.closure {e} = M.closure {e, f}
rw₃ : M.closure (M.closure {e}) = M.closure {e, f}
rw₄ : M.closure (insert f (M.closure {e})) = M.closure {e, f}
rw₅ : M.closure {f, e} = M.closure {e, f}
rw₆ rw₇ : M.closure {e, f} = M.closure {e, f}
⊢ M.closure {e} = M.closure {f}

Tactic:
rw [← closure_closure _ {f}, ← insert_eq_of_mem hef, closure_insert_closure_eq_closure_insert,
    ← closure_closure _ {e}, ← insert_eq_of_mem (he.mem_closure_singleton hef),
    closure_insert_closure_eq_closure_insert, pair_comm]

Premises used: Matroid.IsNonloop.mem_closure_singleton, Matroid.closure_insert_closure_eq_closure_insert, Set.insert_eq_of_mem, Matroid.closure_closure, Singleton.singleton, Set.pair_comm
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
⊢ M.closure {e} = M.closure {f} ↔ M.IsCircuit {e, f}

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
refine_1 : ∀ (h : M.closure {e} = M.closure {f}), M.IsCircuit {e, f}
refine_2 : ∀ (h : M.IsCircuit {e, f}), M.closure {e} = M.closure {f}
⊢ M.closure {e} = M.closure {f} ↔ M.IsCircuit {e, f}

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
rw : e ∈ M.closure {e}
⊢ e ∈ M.closure {f}

Tactic:
rw [← h]
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
⊢ e ∈ M.closure {e}

Tactic:
M.mem_closure_self e

Premises used: Matroid.mem_closure_self
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
⊢ e ∈ M.closure {e}

Tactic:
exact M.mem_closure_self e

Premises used: Matroid.mem_closure_self
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
⊢ M.IsNonloop f

Tactic:
have hf := he.isNonloop_of_mem_closure (by rw [← h]; exact M.mem_closure_self e)
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
hf : M.IsNonloop f
refine_1 : ¬M.Indep {e, f} ∧ ∀ (e_1 : α), Membership.mem (γ := Set α) {e, f} e_1 → M.Indep ({e, f} \ {e_1})
⊢ M.IsCircuit {e, f}

Tactic:
rw [isCircuit_iff_dep_forall_diff_singleton_indep, dep_iff, insert_subset_iff,
      and_iff_right he.mem_ground, singleton_subset_iff, and_iff_left hf.mem_ground]

Premises used: Matroid.IsNonloop.mem_ground, Set.singleton_subset_iff, and_iff_left, and_iff_right, Matroid.isCircuit_iff_dep_forall_diff_singleton_indep, Set.insert_subset_iff, Matroid.dep_iff
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
hf : M.IsNonloop f
this : ¬M.Indep {e, f}
⊢ ¬M.Indep {e, f} ∧ ∀ (e_1 : α), Membership.mem (γ := Set α) {e, f} e_1 → M.Indep ({e, f} \ {e_1})

Tactic:
simpa [pair_diff_left hef, hf, pair_diff_right hef, he]

Premises used: Set.pair_diff_left, Set.pair_diff_right
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
hf : M.IsNonloop f
refine_1 : ¬M.Indep {e, f}
⊢ ¬M.Indep {e, f} ∧ ∀ (e_1 : α), Membership.mem (γ := Set α) {e, f} e_1 → M.Indep ({e, f} \ {e_1})

Tactic:
suffices ¬ M.Indep {e, f} by simpa [pair_diff_left hef, hf, pair_diff_right hef, he]
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
hf : M.IsNonloop f
⊢ M.Indep {f}

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
hf : M.IsNonloop f
⊢ e ∉ {f}

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
hf : M.IsNonloop f
refine_1 : e ∉ M.E \ M.closure {f}
⊢ ¬M.Indep {e, f}

Tactic:
rw [Indep.insert_indep_iff_of_notMem (by simpa) (by simpa)]

Premises used: Matroid.Indep.insert_indep_iff_of_notMem
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
hf : M.IsNonloop f
⊢ e ∉ M.E \ M.closure {f}

Tactic:
simp [← h, mem_closure_self _ _ he.mem_ground]

Premises used: Matroid.IsNonloop.mem_ground, Matroid.mem_closure_self
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.IsCircuit {e, f}
⊢ 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
-- Module: Mathlib.Combinatorics.Matroid.Loop
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}
refine_2₂ refine_2₃ refine_2₄ refine_2₅ : ∀ (hclosure : M.closure {e} = M.closure {f}), 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

Premises used: Set.pair_diff_left, eq_comm, Set.pair_diff_right
-- Module: Mathlib.Combinatorics.Matroid.Loop
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}
inr : ∀ (hne : e ≠ f), M.closure {e} = M.closure {f} ↔ e = f ∨ ¬M.Indep {e, f}
⊢ M.closure {e} = M.closure {f} ↔ e = f ∨ ¬M.Indep {e, f}

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

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
he hf : M.IsNonloop e
⊢ M.closure {e} = M.closure {e} ↔ e = e ∨ ¬M.Indep {e, e}

Tactic:
iff_of_true rfl (Or.inl rfl)

Premises used: iff_of_true, Or.inl, rfl
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
he hf : M.IsNonloop e
⊢ M.closure {e} = M.closure {e} ↔ e = e ∨ ¬M.Indep {e, e}

Tactic:
exact iff_of_true rfl (Or.inl rfl)

Premises used: iff_of_true, Or.inl, rfl
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hf : M.IsNonloop f
hne : e ≠ f
inr : ¬M.Indep {e, f} → ∀ (e_1 : α), Membership.mem (γ := Set α) {e, f} e_1 → M.Indep ({e, f} \ {e_1})
⊢ M.closure {e} = M.closure {f} ↔ e = f ∨ ¬M.Indep {e, f}

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]

Premises used: Matroid.IsNonloop.mem_ground, Set.singleton_subset_iff, and_iff_left, Matroid.isCircuit_iff_dep_forall_diff_singleton_indep, Set.insert_subset_iff, or_iff_right, Matroid.IsNonloop.closure_eq_closure_iff_isCircuit_of_ne, and_iff_left_iff_imp, Matroid.dep_iff
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
f : α
hf : M.IsNonloop f
x : α
he : M.IsNonloop x
hne : x ≠ f
hi : ¬M.Indep {x, f}
inr : M.Indep {f}
inr₁ inr₂ inr₃ inr₄ : M.IsNonloop f
⊢ M.Indep ({x, f} \ {x})

Tactic:
rwa [pair_diff_left hne, indep_singleton]

Premises used: Set.pair_diff_left, Matroid.indep_singleton
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
he : M.IsNonloop e
x : α
hf : M.IsNonloop x
hne : e ≠ x
hi : ¬M.Indep {e, x}
inr : M.Indep {e}
inr₁ inr₂ inr₃ inr₄ : M.IsNonloop e
⊢ M.Indep ({e, x} \ {x})

Tactic:
rwa [pair_diff_right hne, indep_singleton]

Premises used: Set.pair_diff_right, Matroid.indep_singleton
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
inst : M.RankPos
⊢ ∃ (e : α), M.IsNonloop e

Tactic:
let ⟨_, hB⟩ := M.exists_isBase
  ⟨_, hB.indep.isNonloop_of_mem hB.nonempty.some_mem⟩

Premises used: Matroid.IsBase.nonempty, Exists, Set.Nonempty.some_mem, Matroid.IsNonloop, Matroid.exists_isBase, Exists.intro, Matroid.Indep.isNonloop_of_mem, Matroid.IsBase.indep, _private.0.Matroid.exists_isNonloop.match_1, Set.Nonempty.some
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
h : M.IsNonloop e
⊢ M.RankPos

Tactic:
h.indep.rankPos_of_nonempty (singleton_nonempty e)

Premises used: Set.singleton_nonempty, Matroid.Indep.rankPos_of_nonempty, Matroid.IsNonloop.indep
-- Module: Mathlib.Combinatorics.Matroid.Loop
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
rw₃ rw₄ : M.IsNonloop e ∧ e ∈ R ↔ M.IsNonloop e ∧ e ∈ R
⊢ (M ↾ R).IsNonloop e ↔ M.IsNonloop e ∧ e ∈ R

Tactic:
rw [← indep_singleton, restrict_indep_iff, singleton_subset_iff, indep_singleton]

Premises used: Set.singleton_subset_iff, Matroid.indep_singleton, Matroid.restrict_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
h : (M ↾ R).IsNonloop e
⊢ M.IsNonloop e

Tactic:
(restrict_isNonloop_iff.1 h).1

Premises used: Matroid.restrict_isNonloop_iff, And.left, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M N : Matroid α
e : α
h : N.IsNonloop e
hNM : N ≤r M
obtain : ∀ (R : Set α) (h : (M ↾ R).IsNonloop e), M.IsNonloop e
⊢ M.IsNonloop e

Tactic:
obtain ⟨R, -, rfl⟩ := hNM

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
h : (M ↾ R).IsNonloop e
⊢ M.IsNonloop e

Tactic:
h.of_restrict

Premises used: Matroid.IsNonloop.of_restrict
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
h : (M ↾ R).IsNonloop e
⊢ M.IsNonloop e

Tactic:
exact h.of_restrict

Premises used: Matroid.IsNonloop.of_restrict
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
he : e ∈ R
⊢ M.IsNonloop e ↔ (M ↾ R).IsNonloop e

Tactic:
⟨fun h ↦ restrict_isNonloop_iff.2 ⟨h, he⟩, fun h ↦ h.of_restrict⟩

Premises used: Iff.mpr, Matroid.restrict_isNonloop_iff, And.intro, Iff.intro, Matroid.IsNonloop.of_restrict
-- Module: Mathlib.Combinatorics.Matroid.Loop
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)
rw₄ rw₅ : M.IsNonloop (f e) ↔ M.IsNonloop (f e)
⊢ (M.comap f).IsNonloop e ↔ M.IsNonloop (f e)

Tactic:
rw [← indep_singleton, comap_indep_iff, image_singleton, indep_singleton,
    and_iff_left (injOn_singleton _ _)]

Premises used: Set.image_singleton, and_iff_left, Matroid.comap_indep_iff, Set.injOn_singleton, Matroid.indep_singleton
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
e : α
E : Set α
rw : (freeOn E).Indep {e} ↔ e ∈ E
rw₁ : {e} ⊆ E ↔ e ∈ E
rw₂ rw₃ : e ∈ E ↔ e ∈ E
⊢ (freeOn E).IsNonloop e ↔ e ∈ E

Tactic:
rw [← indep_singleton, freeOn_indep_iff, singleton_subset_iff]

Premises used: Set.singleton_subset_iff, Matroid.indep_singleton, Matroid.freeOn_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
e : α
I E : Set α
rw : (uniqueBaseOn I E).Indep {e} ↔ e ∈ I ∩ E
rw₁ : {e} ⊆ I ∩ E ↔ e ∈ I ∩ E
rw₂ rw₃ : e ∈ I ∩ E ↔ e ∈ I ∩ E
⊢ (uniqueBaseOn I E).IsNonloop e ↔ e ∈ I ∩ E

Tactic:
rw [← indep_singleton, uniqueBaseOn_indep_iff', singleton_subset_iff]

Premises used: Set.singleton_subset_iff, Matroid.uniqueBaseOn_indep_iff', Matroid.indep_singleton
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
he : M.IsNonloop e
obtain : ∀ (B : Set α) (hB : M.IsBase B) (heB : e ∈ B), ∃ (K : Set α), M.IsCocircuit K ∧ e ∈ K
⊢ ∃ (K : Set α), M.IsCocircuit K ∧ e ∈ K

Tactic:
obtain ⟨B, hB, heB⟩ := he.exists_mem_isBase

Premises used: Matroid.IsNonloop.exists_mem_isBase
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
he : M.IsNonloop e
B : Set α
hB : M.IsBase B
heB : e ∈ B
⊢ ∃ (K : Set α), M.IsCocircuit K ∧ e ∈ K

Tactic:
⟨_, fundCocircuit_isCocircuit heB hB, mem_fundCocircuit M e B⟩

Premises used: Matroid.mem_fundCocircuit, And.intro, Exists.intro, Matroid.fundCocircuit_isCocircuit
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
he : M.IsNonloop e
B : Set α
hB : M.IsBase B
heB : e ∈ B
⊢ ∃ (K : Set α), M.IsCocircuit K ∧ e ∈ K

Tactic:
exact ⟨_, fundCocircuit_isCocircuit heB hB, mem_fundCocircuit M e B⟩
-- Module: Mathlib.Combinatorics.Matroid.Loop
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
rw₃ rw₄ : M.closure X = M.closure X
⊢ M.closure (X ∩ {e : α | M.IsNonloop e}) = M.closure X

Tactic:
rw [setOf_isNonloop_eq, ← inter_diff_assoc, closure_diff_loops_eq, closure_inter_ground]

Premises used: Matroid.setOf_isNonloop_eq, Matroid.closure_diff_loops_eq, Matroid.closure_inter_ground, Set.inter_diff_assoc
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
he : M.IsColoop e
⊢ e ∈ M.E

Tactic:
@IsLoop.mem_ground α (M✶) e he

Premises used: Set.Mem, Matroid.IsLoop.mem_ground
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
⊢ M.coloops ⊆ M.E

Tactic:
fun _ ↦ IsColoop.mem_ground

Premises used: Set.Mem, Matroid.IsColoop.mem_ground, Matroid.coloops, Set.Subset, Matroid.IsColoop, Matroid.IsLoop
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
⊢ M.IsColoop e ↔ e ∈ M.coloops

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, Matroid.coloops, Matroid.IsColoop, Matroid.IsLoop
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
⊢ M✶.loops = M.coloops

Tactic:
rfl

Premises used: Matroid.coloops, rfl
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
rw : M✶✶.loops = M.loops
rw₁ rw₂ : M.loops = M.loops
⊢ M✶.coloops = M.loops

Tactic:
rw [coloops, dual_dual]

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

Tactic:
he

Premises used: Matroid.IsColoop
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
he : M.IsColoop e
⊢ M.IsCocircuit {e}

Tactic:
IsLoop.isCircuit he

Premises used: Matroid.IsLoop.isCircuit
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
he : M.IsLoop e
rwa : M✶✶.IsLoop e
rwa₁ rwa₂ rwa₃ rwa₄ : M.IsLoop e
⊢ M✶.IsColoop e

Tactic:
rwa [IsColoop, dual_dual]

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

Tactic:
rw [← dual_dual M]

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

Tactic:
h.dual_isLoop

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

Tactic:
exact h.dual_isLoop

Premises used: Matroid.IsColoop.dual_isLoop
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
h : M✶.IsLoop e
rw : M✶✶.IsColoop e
⊢ M.IsColoop e

Tactic:
rw [← dual_dual M]

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

Tactic:
h.dual_isColoop

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

Tactic:
exact h.dual_isColoop

Premises used: Matroid.IsLoop.dual_isColoop
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
⊢ M.IsCocircuit {e} ↔ M.IsColoop e

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
⊢ 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 : α
⊢ e ∈ M.coloops

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.IsColoop e ↔ e ∈ M.coloops

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.IsColoop e ↔ e ∈ M.coloops

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.IsColoop e ↔ e ∈ M.coloops
⊢ 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
⊢ 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
⊢ M.IsColoop e ↔ M.IsCocircuit {e}

Tactic:
1 ↔ 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
⊢ M.IsColoop e ↔ M.IsCocircuit {e}

Tactic:
tfae_have 1 ↔ 3 := singleton_isCocircuit.symm

Premises used: Matroid.singleton_isCocircuit, Iff.symm
-- 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

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false