Theorem: Matroid.IsSimplification.eq_self_iff (Matroid/Simple.lean)

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
h : N.IsSimplification M
⊢ N = M ↔ M.Simple
Tactic:
refine ⟨fun h' ↦ h' ▸ h.simple, fun h' ↦ ?_⟩
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
h : N.IsSimplification M
h' : M.Simple
⊢ N = M

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
h : N.IsSimplification M
h' : M.Simple
⊢ N = M
Tactic:
obtain ⟨f, rfl⟩ := h
State after:
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
h' : M.Simple
f : M.parallelClasses.RepFun
⊢ M ↾ ⇑f '' {e | M.Nonloop e} = M

State before:
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
h' : M.Simple
f : M.parallelClasses.RepFun
⊢ M ↾ ⇑f '' {e | M.Nonloop e} = M
Tactic:
rw [restrict_eq_self_iff, f.coeFun_eq_id_of_eq_discrete M.parallelClasses_eq_discrete, image_id,
  Loopless.ground_eq]
State after:
no goals