Theorem: Matroid.simple_iff_loopless_eq_of_parallel_forall (Matroid/Simple.lean)

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Simple
⊢ M.Loopless
Tactic:
infer_instance
State after:
no goals

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x✝ : M.Loopless ∧ ∀ (e f : α), M.Parallel e f → e = f
left✝ : M.Loopless
h : ∀ (e f : α), M.Parallel e f → e = f
e✝ f✝ : α
heE : e✝ ∈ M.E
⊢ e✝ = f✝ → M.Parallel e✝ f✝
Tactic:
rintro rfl
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x✝ : M.Loopless ∧ ∀ (e f : α), M.Parallel e f → e = f
left✝ : M.Loopless
h : ∀ (e f : α), M.Parallel e f → e = f
e✝ : α
heE : e✝ ∈ M.E
⊢ M.Parallel e✝ e✝

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x✝ : M.Loopless ∧ ∀ (e f : α), M.Parallel e f → e = f
left✝ : M.Loopless
h : ∀ (e f : α), M.Parallel e f → e = f
e✝ : α
heE : e✝ ∈ M.E
⊢ M.Parallel e✝ e✝
Tactic:
exact (toNonloop heE).parallel_self
State after:
no goals