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

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
⊢ M.Simple ↔ ∀ ⦃e f : α⦄, e ∈ M.E → f ∈ M.E → M.Indep {e, f}
Tactic:
refine ⟨fun h _ _ he hf ↦ pair_indep he hf, fun h ↦ ?_⟩
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : ∀ ⦃e f : α⦄, e ∈ M.E → f ∈ M.E → M.Indep {e, f}
⊢ M.Simple

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

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : ∀ ⦃e f : α⦄, e ∈ M.E → f ∈ M.E → M.Indep {e, f}
⊢ (∀ e ∈ M.E, ¬M.Loop e) ∧ ∀ (e f : α), M.Parallel e f → e = f
Tactic:
exact ⟨fun e he hl ↦ hl.dep.not_indep <| by simpa using h he he,
  fun e f hef ↦ hef.eq_of_indep (h hef.mem_ground_left hef.mem_ground_right) ⟩
State after:
no goals

State before:
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
h : ∀ ⦃e f : α⦄, e ∈ M.E → f ∈ M.E → M.Indep {e, f}
e : α
he : e ∈ M.E
hl : M.Loop e
⊢ M.Indep {e}
Tactic:
simpa using h he he
State after:
no goals