Theorem: Matroid.parallel_iff_nonloop_nonloop_indep_imp_eq (Matroid/Parallel.lean)

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
⊢ M.Parallel e f ↔ M.Nonloop e ∧ M.Nonloop f ∧ (M.Indep {e, f} → e = f)
Tactic:
refine ⟨fun h ↦ ⟨h.nonloop_left, h.nonloop_right, fun hi ↦ h.eq_of_indep hi⟩, fun h ↦ ?_⟩
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Nonloop e ∧ M.Nonloop f ∧ (M.Indep {e, f} → e = f)
⊢ M.Parallel e f

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Nonloop e ∧ M.Nonloop f ∧ (M.Indep {e, f} → e = f)
⊢ M.Parallel e f
Tactic:
obtain (rfl | hne) := eq_or_ne e f
State after:
case inl
α : Type u_1
M N : Matroid α
e g : α
I X P D : Set α
h : M.Nonloop e ∧ M.Nonloop e ∧ (M.Indep {e, e} → e = e)
⊢ M.Parallel e e

case inr
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Nonloop e ∧ M.Nonloop f ∧ (M.Indep {e, f} → e = f)
hne : e ≠ f
⊢ M.Parallel e f

State before:
case inr
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Nonloop e ∧ M.Nonloop f ∧ (M.Indep {e, f} → e = f)
hne : e ≠ f
⊢ M.Parallel e f
Tactic:
rw [h.1.parallel_iff_dep h.2.1 hne, Dep, pair_subset_iff, and_iff_left h.2.1.mem_ground,
  and_iff_left h.1.mem_ground]
State after:
case inr
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Nonloop e ∧ M.Nonloop f ∧ (M.Indep {e, f} → e = f)
hne : e ≠ f
⊢ ¬M.Indep {e, f}

State before:
case inr
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Nonloop e ∧ M.Nonloop f ∧ (M.Indep {e, f} → e = f)
hne : e ≠ f
⊢ ¬M.Indep {e, f}
Tactic:
exact fun hi ↦ hne (h.2.2 hi)
State after:
no goals

State before:
case inl
α : Type u_1
M N : Matroid α
e g : α
I X P D : Set α
h : M.Nonloop e ∧ M.Nonloop e ∧ (M.Indep {e, e} → e = e)
⊢ M.Parallel e e
Tactic:
exact h.1.parallel_self
State after:
no goals