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

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hM : ¬M.Simple
⊢ (∃ e, M.Loop e) ∨ ∃ e f, M.Parallel e f ∧ e ≠ f
Tactic:
by_contra! h
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hM : ¬M.Simple
h : (∀ (e : α), ¬M.Loop e) ∧ ∀ (e f : α), M.Parallel e f → e = f
⊢ False

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hM : ¬M.Simple
h : (∀ (e : α), ¬M.Loop e) ∧ ∀ (e f : α), M.Parallel e f → e = f
⊢ False
Tactic:
rw [simple_iff_loopless_eq_of_parallel_forall, loopless_iff_forall_not_loop] at hM
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hM : ¬((∀ e ∈ M.E, ¬M.Loop e) ∧ ∀ (e f : α), M.Parallel e f → e = f)
h : (∀ (e : α), ¬M.Loop e) ∧ ∀ (e f : α), M.Parallel e f → e = f
⊢ False

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hM : ¬((∀ e ∈ M.E, ¬M.Loop e) ∧ ∀ (e f : α), M.Parallel e f → e = f)
h : (∀ (e : α), ¬M.Loop e) ∧ ∀ (e f : α), M.Parallel e f → e = f
⊢ False
Tactic:
push_neg at hM
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : (∀ (e : α), ¬M.Loop e) ∧ ∀ (e f : α), M.Parallel e f → e = f
hM : (∀ e ∈ M.E, ¬M.Loop e) → ∃ e f, M.Parallel e f ∧ e ≠ f
⊢ False

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : (∀ (e : α), ¬M.Loop e) ∧ ∀ (e f : α), M.Parallel e f → e = f
hM : (∀ e ∈ M.E, ¬M.Loop e) → ∃ e f, M.Parallel e f ∧ e ≠ f
⊢ False
Tactic:
obtain ⟨e, f, hef, hne⟩ := hM (fun e _ ↦ h.1 e)
State after:
case intro.intro.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
h : (∀ (e : α), ¬M.Loop e) ∧ ∀ (e f : α), M.Parallel e f → e = f
hM : (∀ e ∈ M.E, ¬M.Loop e) → ∃ e f, M.Parallel e f ∧ e ≠ f
e f : α
hef : M.Parallel e f
hne : e ≠ f
⊢ False

State before:
case intro.intro.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
h : (∀ (e : α), ¬M.Loop e) ∧ ∀ (e f : α), M.Parallel e f → e = f
hM : (∀ e ∈ M.E, ¬M.Loop e) → ∃ e f, M.Parallel e f ∧ e ≠ f
e f : α
hef : M.Parallel e f
hne : e ≠ f
⊢ False
Tactic:
exact hne <| h.2 e f hef
State after:
no goals