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

Tactic:
fun hX ↦ he.dep.not_indep (hX.subset (singleton_subset_iff.mpr h))

Premises used: Iff.mpr, Matroid.Dep.not_indep, Set.singleton_subset_iff, Matroid.Indep.subset, Matroid.IsLoop.dep, Not
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
I : Set α
he : M.IsLoop e
hI : M.Indep I
⊢ e ∉ I

Tactic:
fun h ↦ he.not_indep_of_mem h hI

Premises used: Not, Matroid.IsLoop.not_indep_of_mem
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
C : Set α
he : M.IsLoop e
hC : M.IsCircuit C
h : e ∈ C
rw rw₁ : C = C
⊢ C = {e}

Tactic:
rw [he.isCircuit.eq_of_subset_isCircuit hC (singleton_subset_iff.mpr h)]

Premises used: Iff.mpr, Set.singleton_subset_iff, Matroid.IsCircuit.eq_of_subset_isCircuit, Matroid.IsLoop.isCircuit
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
⊢ Disjoint I M.loops

Tactic:
by_contra fun h ↦
    let ⟨_, ⟨heI, he⟩⟩ := not_disjoint_iff.mp h
    IsLoop.notMem_of_indep he hI heI

Premises used: False, _private.0.Matroid.Indep.disjoint_loops.match_1, Set.not_disjoint_iff, Matroid.IsLoop.notMem_of_indep, Iff.mp, by_contra
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
h : I ⊆ M.loops
⊢ I = ∅

Tactic:
eq_empty_iff_forall_notMem.mpr fun _ he ↦ IsLoop.notMem_of_indep (h he) hI he

Premises used: Iff.mpr, Matroid.IsLoop.notMem_of_indep, Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
I : Set α
⊢ I = ∅ → M.IsBasis I M.loops

Tactic:
simp +contextual [closure_empty]

Premises used: Matroid.closure_empty
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
X : Set α
h : X ⊆ M.loops
⊢ M.closure X = M.loops

Tactic:
(closure_subset_closure_of_subset_closure h).antisymm (M.closure_mono (empty_subset _))

Premises used: Matroid.closure_mono, Matroid.closure_subset_closure_of_subset_closure, HasSubset.Subset.antisymm, Set.empty_subset, Matroid.loops
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.loops
⊢ M.IsBasis ∅ X

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
X I : Set α
hX : X ⊆ M.loops
refine : ∀ (h : M.IsBasis I X), I = ∅
⊢ M.IsBasis I X ↔ I = ∅

Tactic:
refine ⟨fun h ↦ ?_, by rintro rfl; simpa⟩
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
X I : Set α
hX : X ⊆ M.loops
h : M.IsBasis I X
⊢ M.IsBasis I M.loops

Tactic:
have := (closure_eq_loops_of_subset hX) ▸ h.isBasis_closure_right
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
X I : Set α
hX : X ⊆ M.loops
h : M.IsBasis I X
this : M.IsBasis I M.loops
⊢ I = ∅

Tactic:
simpa using this
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
he : M.IsLoop e
⊢ M.closure {e} = M.loops

Tactic:
closure_eq_loops_of_subset (singleton_subset_iff.mpr he)

Premises used: Iff.mpr, Set.singleton_subset_iff, Matroid.closure_eq_loops_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
h : M.closure {e} = M.loops ∧ e ∈ M.E
rw : e ∈ M.loops
rw₁ : e ∈ M.closure ∅
rw₂ : {e} ⊆ M.closure ∅
rw₃ : M.closure {e} ⊆ M.closure ∅
rw₄ : M.loops ⊆ M.closure ∅
rw₅ rw₆ : M.closure ∅ ⊆ M.closure ∅
⊢ M.IsLoop e

Tactic:
rw [isLoop_iff, ← closure_empty, ← singleton_subset_iff,
      ← closure_subset_closure_iff_subset_closure, h.1, loops]

Premises used: Set.singleton_subset_iff, Matroid.closure_subset_closure_iff_subset_closure, Matroid.closure_empty, And.left, Matroid.isLoop_iff, Matroid.loops
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
rw : M.closure {e} = M.loops ∧ e ∈ M.E ↔ M.closure {e} = M.loops
rw₁ rw₂ : M.closure {e} = M.loops ↔ M.closure {e} = M.loops
⊢ M.IsLoop e ↔ M.closure {e} = M.loops

Tactic:
rw [isLoop_iff_closure_eq_loops_and_mem_ground, and_iff_left he]

Premises used: and_iff_left, Matroid.isLoop_iff_closure_eq_loops_and_mem_ground
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
⊢ M.closure M.loops = M.loops

Tactic:
M.closure_closure ∅

Premises used: Matroid.closure_closure, EmptyCollection.emptyCollection, Matroid.loops
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
X : Set α
rw : M.closure (X ∪ M.closure ∅) = M.closure X
rw₁ : M.closure (X ∪ ∅) = M.closure X
rw₂ rw₃ : M.closure X = M.closure X
⊢ M.closure (X ∪ M.loops) = M.closure X

Tactic:
rw [← closure_empty, closure_union_closure_right_eq, union_empty]

Premises used: Set.union_empty, Matroid.closure_empty, Matroid.closure_union_closure_right_eq
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.closure (M.loops ∪ X) = M.closure X

Tactic:
simp [union_comm]

Premises used: Set.union_comm
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
X : Set α
rw : M.closure (X \ M.loops ∪ M.loops) = M.closure X
rw₁ : M.closure (X ∪ M.loops) = M.closure X
rw₂ : M.closure (X ∪ M.closure ∅) = M.closure X
rw₃ : M.closure (X ∪ ∅) = M.closure X
rw₄ rw₅ : M.closure X = M.closure X
⊢ M.closure (X \ M.loops) = M.closure X

Tactic:
rw [← M.closure_union_loops_eq (X \ M.loops), diff_union_self, ← closure_empty,
    closure_union_closure_right_eq, union_empty]

Premises used: Set.union_empty, Matroid.closure_empty, Set.diff_union_self, Matroid.closure_union_closure_right_eq, Matroid.closure_union_loops_eq, SDiff.sdiff, Matroid.loops
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
R : Set α
rw : (M ↾ R).closure ∅ = M.loops ∩ R ∪ R \ M.E
rw₁ : (M ↾ R).closure ∅ = M.closure ∅ ∩ R ∪ R \ M.E
rw₂ : M.closure (∅ ∩ R) ∩ R ∪ R \ M.E = M.closure ∅ ∩ R ∪ R \ M.E
rw₃ rw₄ : M.closure ∅ ∩ R ∪ R \ M.E = M.closure ∅ ∩ R ∪ R \ M.E
⊢ (M ↾ R).loops = M.loops ∩ R ∪ R \ M.E

Tactic:
rw [← closure_empty, ← closure_empty, restrict_closure_eq', empty_inter]

Premises used: Matroid.closure_empty, Set.empty_inter, Matroid.restrict_closure_eq'
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
rw : M.loops ∩ R ∪ R \ M.E = M.loops ∩ R
rw₁ : M.loops ∩ R ∪ ∅ = M.loops ∩ R
rw₂ rw₃ : M.loops ∩ R = M.loops ∩ R
⊢ (M ↾ R).loops = M.loops ∩ R

Tactic:
rw [restrict_loops_eq', diff_eq_empty.2 hR, union_empty]

Premises used: Iff.mpr, Set.union_empty, Matroid.restrict_loops_eq', Set.diff_eq_empty
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
simp : e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E ↔ e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
⊢ (M ↾ R).IsLoop e ↔ e ∈ R ∧ (M.IsLoop e ∨ e ∉ M.E)

Tactic:
simp only [isLoop_iff, restrict_closure_eq', empty_inter, mem_union, mem_inter_iff, mem_diff,
    ← closure_empty]

Premises used: Set.mem_union, Matroid.closure_empty, Set.mem_inter_iff, Set.empty_inter, Set.mem_diff, Matroid.isLoop_iff, Matroid.restrict_closure_eq'
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
mp : e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mpr : e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E) → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mp₁ : e ∈ M.closure ∅ → e ∈ R → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₂ : e ∈ R → e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₃ : e ∈ M.closure ∅ → e ∈ R → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₄ : e ∈ R → e ∉ M.E → e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)
mp₅ : e ∈ M.closure ∅ → e ∈ R → e ∈ R
mp₆ : e ∈ M.closure ∅ → e ∈ R → e ∈ M.closure ∅ ∨ e ∉ M.E
mp₇ : e ∈ R → e ∉ M.E → e ∈ R
mp₈ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∨ e ∉ M.E
mpr₁ : e ∈ R → e ∈ M.closure ∅ → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₂ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₃ : e ∈ R → e ∈ M.closure ∅ → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₄ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
mpr₅ : e ∈ R → e ∈ M.closure ∅ → ¬(e ∈ M.closure ∅ ∧ e ∈ R) → e ∈ R
mpr₆ : e ∈ R → e ∈ M.closure ∅ → ¬(e ∈ M.closure ∅ ∧ e ∈ R) → e ∉ M.E
mpr₇ : e ∈ R → e ∉ M.E → ¬(e ∈ M.closure ∅ ∧ e ∈ R) → e ∈ R
mpr₈ : e ∈ R → e ∉ M.E → ¬(e ∈ M.closure ∅ ∧ e ∈ R) → e ∉ M.E
mp₉ mp₁₀ : e ∈ M.closure ∅ → e ∈ R → e ∈ M.closure ∅ ∨ e ∉ M.E
mp₁₁ : e ∈ M.closure ∅ → e ∈ R → e ∉ M.closure ∅ → e ∉ M.E
mp₁₂ mp₁₃ : e ∈ R → e ∉ M.E → e ∈ M.closure ∅ ∨ e ∉ M.E
mp₁₄ : e ∈ R → e ∉ M.E → e ∉ M.closure ∅ → e ∉ M.E
mpr₉ : e ∈ R → e ∈ M.closure ∅ → e ∈ M.E → e ∉ M.closure ∅ → False
mpr₁₀ : e ∈ R → e ∈ M.closure ∅ → e ∈ M.E → e ∉ R → False
mp₁₅ : e ∈ M.closure ∅ → e ∈ R → e ∉ M.closure ∅ → e ∈ M.E → False
⊢ e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E ↔ e ∈ R ∧ (e ∈ M.closure ∅ ∨ e ∉ M.E)

Tactic:
tauto
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M N : Matroid α
e : α
hNM : N ≤r M
obtain : ∀ (R : Set α) (hR : R ⊆ M.E), (M ↾ R).IsLoop e ↔ e ∈ (M ↾ R).E ∧ M.IsLoop e
⊢ N.IsLoop e ↔ e ∈ N.E ∧ M.IsLoop e

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

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
hR : R ⊆ M.E
simp : e ∈ R → e ∉ M.E → M.IsLoop e
⊢ (M ↾ R).IsLoop e ↔ e ∈ (M ↾ R).E ∧ M.IsLoop e

Tactic:
simp only [restrict_isLoop_iff, restrict_ground_eq, and_congr_right_iff, or_iff_left_iff_imp]

Premises used: or_iff_left_iff_imp, Matroid.restrict_ground_eq, and_congr_right_iff, Matroid.restrict_isLoop_iff
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
hR : R ⊆ M.E
⊢ e ∈ R → e ∉ M.E → M.IsLoop e

Tactic:
fun heR heE ↦ (heE (hR heR)).elim

Premises used: False.elim
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
hR : R ⊆ M.E
⊢ e ∈ R → e ∉ M.E → M.IsLoop e

Tactic:
exact fun heR heE ↦ (heE (hR heR)).elim
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M N : Matroid α
e : α
he : N.IsLoop e
hNM : N ≤r M
⊢ M.IsLoop e

Tactic:
((hNM.isLoop_iff).1 he).2

Premises used: And.right, Iff.mp, Matroid.IsRestriction.isLoop_iff
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M N : Matroid α
e : α
he : M.IsLoop e
hNM : N ≤r M
heN : e ∈ N.E
⊢ N.IsLoop e

Tactic:
(hNM.isLoop_iff).2 ⟨heN, he⟩

Premises used: Iff.mpr, And.intro, Matroid.IsRestriction.isLoop_iff
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
⊢ (M.map f hf).loops = f '' M.loops

Tactic:
simp [loops]

Premises used: Matroid.loops
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
e : α
f : α → β
hf : InjOn f M.E
he : e ∈ M.E
rw : f e ∈ (M.map f hf).loops ↔ M.IsLoop e
rw₁ : f e ∈ f '' M.loops ↔ M.IsLoop e
rw₂ : e ∈ M.loops ↔ M.IsLoop e
rw₃ rw₄ : e ∈ M.loops ↔ e ∈ M.loops
⊢ (M.map f hf).IsLoop (f e) ↔ M.IsLoop e

Tactic:
rw [isLoop_iff, map_loops, hf.mem_image_iff M.loops_subset_ground he, isLoop_iff]

Premises used: Set.InjOn.mem_image_iff, Matroid.map_loops, Matroid.isLoop_iff, Matroid.loops_subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
β : Type u_2
M : Matroid α
e : α
f : α ↪ β
⊢ (M.mapEmbedding f).IsLoop ((f : (a : α) → β) e) ↔ M.IsLoop e

Tactic:
simp [mapEmbedding, isLoop_iff, isLoop_iff, map_closure_eq, preimage_empty, ← closure_empty]

Premises used: Matroid.closure_empty, Matroid.mapEmbedding, Set.preimage_empty, Matroid.map_closure_eq, Matroid.isLoop_iff
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
β : Type u_2
M : Matroid β
f : α → β
rw : (M.comap f).closure ∅ = f ⁻¹' M.loops
rw₁ : f ⁻¹' M.closure (f '' ∅) = f ⁻¹' M.loops
rw₂ : f ⁻¹' M.closure ∅ = f ⁻¹' M.loops
rw₃ rw₄ : f ⁻¹' M.closure ∅ = f ⁻¹' M.closure ∅
⊢ (M.comap f).loops = f ⁻¹' M.loops

Tactic:
rw [loops, comap_closure_eq, image_empty, loops]

Premises used: Matroid.comap_closure_eq, Set.image_empty, Matroid.loops
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
β : Type u_2
e : α
M : Matroid β
f : α → β
⊢ (M.comap f).IsLoop e ↔ M.IsLoop (f e)

Tactic:
simp [isLoop_iff]

Premises used: Matroid.isLoop_iff
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
e : α
E : Set α
⊢ (loopyOn E).IsLoop e ↔ e ∈ E

Tactic:
simp [isLoop_iff, loops]

Premises used: Matroid.isLoop_iff, Matroid.loops
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
E : Set α
h : M = loopyOn E
rw : (loopyOn E).closure ∅ = E ∧ (loopyOn E).E = E
⊢ M.loops = E ∧ M.E = E

Tactic:
rw [h, loops]

Premises used: Matroid.loops
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
E : Set α
h : M = loopyOn E
⊢ (loopyOn E).closure ∅ = E ∧ (loopyOn E).E = E

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
E : Set α
h : M.loops = E
h' : M.E = E
rw : M = loopyOn M.E
rw₁ : M.closure ∅ = M.E
rw₂ : M.loops = M.E
rw₃ : E = M.E
rw₄ rw₅ : E = E
⊢ M = loopyOn E

Tactic:
rw [← h', ← closure_empty_eq_ground_iff, ← loops, h, h']

Premises used: Matroid.closure_empty_eq_ground_iff, Matroid.loops
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.loops
rw : (M ↾ X).loops = X ∧ (M ↾ X).E = X
rw₁ : M.loops ∩ X ∪ X \ M.E = X ∧ (M ↾ X).E = X
rw₂ : X ∪ X \ M.E = X ∧ (M ↾ X).E = X
rw₃ : X = X ∧ (M ↾ X).E = X
rw₄ rw₅ : X = X
⊢ M ↾ X = loopyOn X

Tactic:
rw [eq_loopyOn_iff_loops, restrict_loops_eq', inter_eq_self_of_subset_right hX,
    union_eq_self_of_subset_right diff_subset, and_iff_left M.restrict_ground_eq]

Premises used: Set.diff_subset, Matroid.restrict_loops_eq', and_iff_left, Set.union_eq_self_of_subset_right, Matroid.restrict_ground_eq, Set.inter_eq_self_of_subset_right, Matroid.eq_loopyOn_iff_loops
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
E : Set α
e : α
⊢ ¬(freeOn E).IsLoop e

Tactic:
simp [isLoop_iff, loops]

Premises used: Matroid.isLoop_iff, Matroid.loops
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
e : α
I E : Set α
⊢ (uniqueBaseOn I E).IsLoop e ↔ e ∈ E \ I

Tactic:
simp [isLoop_iff, loops]

Premises used: Matroid.isLoop_iff, Matroid.loops
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
E : Set α
h : M = loopyOn E
⊢ M.loops = E ∧ M.E = E

Tactic:
simp [h, loops]

Premises used: Matroid.loops
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
E : Set α
h_1 : M.loops = E ∧ M.E = E
h : M.loops = E
h' : M.E = E
rw : M = loopyOn M.E
rw₁ : M.closure ∅ = M.E
rw₂ : M.loops = M.E
rw₃ : E = M.E
rw₄ rw₅ : E = E
⊢ M = loopyOn E

Tactic:
rw [← h', ← closure_empty_eq_ground_iff, ← loops, h, h']

Premises used: Matroid.closure_empty_eq_ground_iff, Matroid.loops
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
he : M.IsLoop e
⊢ ¬M.IsNonloop e

Tactic:
fun h ↦ h.not_isLoop he

Premises used: Matroid.IsNonloop.not_isLoop, Not
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
⊢ M.E \ M.loops = {e : α | M.IsNonloop e}

Tactic:
simp [Set.ext_iff, isNonloop_iff, and_comm, isLoop_iff]

Premises used: and_comm, Matroid.isLoop_iff, Set.ext_iff, Matroid.isNonloop_iff
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
h : ¬M.IsLoop e
⊢ M.IsNonloop e

Tactic:
⟨h,he⟩

Premises used: Matroid.IsNonloop.mk
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
h : ¬M.IsNonloop e
rwa : ∀ (h : ¬(¬M.IsLoop e ∧ e ∈ M.E)), M.IsLoop e
rwa₁ : ∀ (h : ¬¬M.IsLoop e), M.IsLoop e
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (h : M.IsLoop e), M.IsLoop e
⊢ M.IsLoop e

Tactic:
rwa [isNonloop_iff, and_iff_left he, not_not] at h

Premises used: Classical.not_not, and_iff_left, Matroid.isNonloop_iff
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ ¬M.IsLoop e ↔ M.IsNonloop e

Tactic:
⟨fun h ↦ ⟨h, he⟩, IsNonloop.not_isLoop⟩

Premises used: Matroid.IsNonloop.mk, Matroid.IsNonloop.not_isLoop, Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
rw : ¬¬M.IsLoop e ↔ M.IsLoop e
rw₁ rw₂ : M.IsLoop e ↔ M.IsLoop e
⊢ ¬M.IsNonloop e ↔ M.IsLoop e

Tactic:
rw [← not_isLoop_iff, not_not]

Premises used: Classical.not_not, Matroid.not_isLoop_iff
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
rw : ¬M.IsLoop e ∧ e ∈ M.E ↔ e ∈ M.E \ M.loops
rw₁ : e ∉ M.loops ∧ e ∈ M.E ↔ e ∈ M.E \ M.loops
rw₂ : e ∈ M.E ∧ e ∉ M.loops ↔ e ∈ M.E \ M.loops
rw₃ rw₄ : e ∈ M.E ∧ e ∉ M.loops ↔ e ∈ M.E ∧ e ∉ M.loops
⊢ M.IsNonloop e ↔ e ∈ M.E \ M.loops

Tactic:
rw [isNonloop_iff, IsLoop, and_comm, mem_diff]

Premises used: and_comm, Set.mem_diff, Matroid.isNonloop_iff, Matroid.IsLoop
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
⊢ {e : α | M.IsNonloop e} = M.E \ M.loops

Tactic:
Set.ext (fun _ ↦ isNonloop_iff_mem_compl_loops)

Premises used: Set.ext, Matroid.isNonloop_iff_mem_compl_loops
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
pos : ∀ (he : e ∈ M.E), ¬M.IsNonloop e ↔ M.closure {e} = M.loops
neg : ∀ (he : e ∉ M.E), ¬M.IsNonloop e ↔ M.closure {e} = M.loops
⊢ ¬M.IsNonloop e ↔ M.closure {e} = M.loops

Tactic:
by_cases he : e ∈ M.E

Premises used: Matroid.E
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ ¬M.IsNonloop e ↔ M.closure {e} = M.loops

Tactic:
simp [isLoop_iff_closure_eq_loops_and_mem_ground, he]

Premises used: Matroid.isLoop_iff_closure_eq_loops_and_mem_ground
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∉ M.E
⊢ ¬M.IsNonloop e ↔ M.closure {e} = M.loops

Tactic:
simp [← closure_inter_ground, singleton_inter_eq_empty.2 he, loops,
    (show ¬ M.IsNonloop e from fun h ↦ he h.mem_ground)]

Premises used: Iff.mpr, Matroid.IsNonloop.mem_ground, Set.singleton_inter_eq_empty, Matroid.closure_inter_ground, Matroid.loops
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
rw : M.IsLoop e ∨ ¬M.IsLoop e
⊢ M.IsLoop e ∨ M.IsNonloop e

Tactic:
rw [isNonloop_iff, and_iff_left he]

Premises used: and_iff_left, Matroid.isNonloop_iff
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ M.IsLoop e ∨ ¬M.IsLoop e

Tactic:
apply em

Premises used: em
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
rw : M.Indep {e} ↔ (e ∈ M.E → M.Indep {e}) ∧ e ∈ M.E
⊢ M.Indep {e} ↔ M.IsNonloop e

Tactic:
rw [isNonloop_iff, ← singleton_dep, dep_iff, not_and, not_imp_not, singleton_subset_iff]

Premises used: Set.singleton_subset_iff, Matroid.singleton_dep, Matroid.isNonloop_iff, not_and, Matroid.dep_iff, not_imp_not
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
⊢ M.Indep {e} ↔ (e ∈ M.E → M.Indep {e}) ∧ e ∈ M.E

Tactic:
⟨fun h ↦ ⟨fun _ ↦ h, singleton_subset_iff.mp h.subset_ground⟩, fun h ↦ h.1 h.2⟩

Premises used: Set.singleton_subset_iff, Matroid.Indep.subset_ground, And.right, And.left, And.intro, Iff.intro, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
⊢ M.Indep {e} ↔ (e ∈ M.E → M.Indep {e}) ∧ e ∈ M.E

Tactic:
exact ⟨fun h ↦ ⟨fun _ ↦ h, singleton_subset_iff.mp h.subset_ground⟩, fun h ↦ h.1 h.2⟩
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
I : Set α
hI : M.Indep I
h : e ∈ I
rw : ¬M.IsLoop e
⊢ M.IsNonloop e

Tactic:
rw [← not_isLoop_iff (hI.subset_ground h)]

Premises used: Matroid.Indep.subset_ground, Matroid.not_isLoop_iff
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
I : Set α
hI : M.Indep I
h : e ∈ I
⊢ ¬M.IsLoop e

Tactic:
fun he ↦ (he.notMem_of_indep hI) h

Premises used: Matroid.IsLoop.notMem_of_indep, Not
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
I : Set α
hI : M.Indep I
h : e ∈ I
⊢ ¬M.IsLoop e

Tactic:
exact fun he ↦ (he.notMem_of_indep hI) h
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
he : M.IsNonloop e
⊢ ∃ (B : Set α), M.IsBase B ∧ e ∈ B

Tactic:
simpa using (indep_singleton.2 he).exists_isBase_superset

Premises used: Iff.mpr, Matroid.Indep.exists_isBase_superset, Matroid.indep_singleton
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
K : Set α
hK : M.IsCocircuit K
he : e ∈ K
rw : ¬M.IsCircuit {e}
⊢ M.IsNonloop e

Tactic:
rw [← not_isLoop_iff (hK.subset_ground he), ← singleton_isCircuit]

Premises used: Matroid.singleton_isCircuit, Matroid.IsCocircuit.subset_ground, Matroid.not_isLoop_iff
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
K : Set α
hK : M.IsCocircuit K
he : e ∈ K
he' : M.IsCircuit {e}
⊢ e ∈ {e} ∩ K

Tactic:
simp [he]
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
K : Set α
hK : M.IsCocircuit K
he : e ∈ K
he' : M.IsCircuit {e}
obtain : ∀ (f : α) (he : f ∈ K) (he' : M.IsCircuit {f}) (hfe : f ≠ f), False
⊢ False

Tactic:
obtain ⟨f, ⟨rfl, -⟩, hfe⟩ := (he'.isCocircuit_inter_nontrivial hK ⟨e, by simp [he]⟩).exists_ne e

Premises used: Set.Nontrivial.exists_ne, Matroid.IsCircuit.isCocircuit_inter_nontrivial, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
K : Set α
hK : M.IsCocircuit K
f : α
he : f ∈ K
he' : M.IsCircuit {f}
hfe : f ≠ f
⊢ False

Tactic:
hfe rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
K : Set α
hK : M.IsCocircuit K
f : α
he : f ∈ K
he' : M.IsCircuit {f}
hfe : f ≠ f
⊢ False

Tactic:
exact hfe rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
C : Set α
hC : M.IsCircuit C
hC' : C.Nontrivial
he : e ∈ C
hL : M.IsLoop e
⊢ False

Tactic:
simp [hL.eq_of_isCircuit_mem hC he] at hC'

Premises used: Matroid.IsLoop.eq_of_isCircuit_mem
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
C : Set α
hC : M.IsCircuit C
h : 1 < C.encard
he : e ∈ C
⊢ M.IsNonloop e

Tactic:
isNonloop_of_not_isLoop (hC.subset_ground he) (fun hlp ↦ ?_)

Premises used: Matroid.IsCircuit.subset_ground, Matroid.isNonloop_of_not_isLoop
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
C : Set α
hC : M.IsCircuit C
h : 1 < C.encard
he : e ∈ C
refine : ∀ (hlp : M.IsLoop e), False
⊢ M.IsNonloop e

Tactic:
refine isNonloop_of_not_isLoop (hC.subset_ground he) (fun hlp ↦ ?_)

Premises used: Matroid.IsCircuit.subset_ground, Matroid.isNonloop_of_not_isLoop
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
C : Set α
hC : M.IsCircuit C
h : 1 < C.encard
he : e ∈ C
hlp : M.IsLoop e
⊢ LT.lt (α := ℕ∞) 1 1

Tactic:
rw [hlp.eq_of_isCircuit_mem hC he, encard_singleton] at h

Premises used: Matroid.IsLoop.eq_of_isCircuit_mem, Set.encard_singleton
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
C : Set α
hC : M.IsCircuit C
h : 1 < C.encard
he : e ∈ C
hlp : M.IsLoop e
h₁ : LT.lt (α := ℕ∞) 1 1
⊢ e ∈ C

Tactic:
rw [hlp.eq_of_isCircuit_mem hC he, encard_singleton] at h

Premises used: Matroid.IsLoop.eq_of_isCircuit_mem, Set.encard_singleton
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
C : Set α
hC : M.IsCircuit C
h : 1 < C.encard
he : e ∈ C
hlp : M.IsLoop e
h₁ : LT.lt (α := ℕ∞) 1 1
he₁ : e ∈ C
⊢ M.IsLoop e

Tactic:
rw [hlp.eq_of_isCircuit_mem hC he, encard_singleton] at h

Premises used: Matroid.IsLoop.eq_of_isCircuit_mem, Set.encard_singleton
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
C : Set α
hC : M.IsCircuit C
h : LT.lt (α := ℕ∞) 1 1
he : e ∈ C
hlp : M.IsLoop e
⊢ False

Tactic:
h.ne rfl

Premises used: rfl, LT.lt.ne
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
C : Set α
hC : M.IsCircuit C
h : LT.lt (α := ℕ∞) 1 1
he : e ∈ C
hlp : M.IsLoop e
⊢ False

Tactic:
exact h.ne rfl

Premises used: rfl, LT.lt.ne