Theorem: Matroid.IsSimplification.simple (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.Simple
Tactic:
obtain ⟨f, rfl⟩ := h
State after:
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
f : M.parallelClasses.RepFun
⊢ (M ↾ ⇑f '' {e | M.Nonloop e}).Simple

State before:
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
f : M.parallelClasses.RepFun
⊢ (M ↾ ⇑f '' {e | M.Nonloop e}).Simple
Tactic:
rw [simple_iff_loopless_eq_of_parallel_forall]
State after:
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
f : M.parallelClasses.RepFun
⊢ (M ↾ ⇑f '' {e | M.Nonloop e}).Loopless ∧ ∀ (e f_1 : α), (M ↾ ⇑f '' {e | M.Nonloop e}).Parallel e f_1 → e = f_1

State before:
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
f : M.parallelClasses.RepFun
⊢ (M ↾ ⇑f '' {e | M.Nonloop e}).Loopless ∧ ∀ (e f_1 : α), (M ↾ ⇑f '' {e | M.Nonloop e}).Parallel e f_1 → e = f_1
Tactic:
simp only [restrict_parallel_iff, mem_image, mem_setOf_eq, and_imp, forall_exists_index,
  loopless_iff_forall_nonloop, restrict_ground_eq, mem_image, mem_setOf_eq, restrict_nonloop_iff,
  forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
State after:
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
f : M.parallelClasses.RepFun
⊢ (∀ (a : α), M.Nonloop a → M.Nonloop (f a) ∧ ∃ x, M.Nonloop x ∧ f x = f a) ∧
    ∀ (e f_1 : α), M.Parallel e f_1 → ∀ (x : α), M.Nonloop x → f x = e → ∀ (x : α), M.Nonloop x → f x = f_1 → e = f_1

State before:
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
f : M.parallelClasses.RepFun
⊢ (∀ (a : α), M.Nonloop a → M.Nonloop (f a) ∧ ∃ x, M.Nonloop x ∧ f x = f a) ∧
    ∀ (e f_1 : α), M.Parallel e f_1 → ∀ (x : α), M.Nonloop x → f x = e → ∀ (x : α), M.Nonloop x → f x = f_1 → e = f_1
Tactic:
refine ⟨fun x hx ↦ ⟨f.apply_mem hx, ⟨x, hx, rfl⟩⟩, ?_⟩
State after:
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
f : M.parallelClasses.RepFun
⊢ ∀ (e f_1 : α), M.Parallel e f_1 → ∀ (x : α), M.Nonloop x → f x = e → ∀ (x : α), M.Nonloop x → f x = f_1 → e = f_1

State before:
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
f : M.parallelClasses.RepFun
⊢ ∀ (e f_1 : α), M.Parallel e f_1 → ∀ (x : α), M.Nonloop x → f x = e → ∀ (x : α), M.Nonloop x → f x = f_1 → e = f_1
Tactic:
rintro _ _ hxy x - rfl y - rfl
State after:
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x✝ y✝ : α
f : M.parallelClasses.RepFun
x y : α
hxy : M.Parallel (f x) (f y)
⊢ f x = f y

State before:
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x✝ y✝ : α
f : M.parallelClasses.RepFun
x y : α
hxy : M.Parallel (f x) (f y)
⊢ f x = f y
Tactic:
simpa using f.apply_eq_apply hxy
State after:
no goals