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

State before:
α : Type u_1
M✝ N : Matroid α
e f g : α
I X P D : Set α
M : Matroid α
⊢ M.simplification.IsSimplification M
Tactic:
let f := M.removeLoops.parallelClasses.nonempty_repFun.some
State after:
α : Type u_1
M✝ N : Matroid α
e f✝ g : α
I X P D : Set α
M : Matroid α
f : M.removeLoops.parallelClasses.RepFun := ⋯.some
⊢ M.simplification.IsSimplification M

State before:
α : Type u_1
M✝ N : Matroid α
e f✝ g : α
I X P D : Set α
M : Matroid α
f : M.removeLoops.parallelClasses.RepFun := ⋯.some
⊢ M.simplification.IsSimplification M
Tactic:
refine ⟨Partition.RepFun.mk f (fun a ha ↦ f.apply_of_not_mem (by simpa))
  (fun a ha ↦ by simpa [mem_setOf_eq, parallelClasses_rel_eq] using f.rel_apply (by simpa))
  (fun a b hab ↦ f.apply_eq_apply (by simpa)), ?_⟩
State after:
α : Type u_1
M✝ N : Matroid α
e f✝ g : α
I X P D : Set α
M : Matroid α
f : M.removeLoops.parallelClasses.RepFun := ⋯.some
⊢ M.simplification =
    M ↾
      ⇑{ toFun := ⇑f, apply_eq_self_of_not_mem := ⋯, rel_apply_of_mem := ⋯, apply_eq_of_rel := ⋯ } '' {e | M.Nonloop e}

State before:
α : Type u_1
M✝ N : Matroid α
e f✝ g : α
I X P D : Set α
M : Matroid α
f : M.removeLoops.parallelClasses.RepFun := ⋯.some
⊢ M.simplification =
    M ↾
      ⇑{ toFun := ⇑f, apply_eq_self_of_not_mem := ⋯, rel_apply_of_mem := ⋯, apply_eq_of_rel := ⋯ } '' {e | M.Nonloop e}
Tactic:
simp only [simplification, removeLoops_nonloop_iff, Partition.RepFun.mk_apply]
State after:
α : Type u_1
M✝ N : Matroid α
e f✝ g : α
I X P D : Set α
M : Matroid α
f : M.removeLoops.parallelClasses.RepFun := ⋯.some
⊢ M.removeLoops ↾ ⇑⋯.some '' {e | M.Nonloop e} = M ↾ (fun a => f a) '' {e | M.Nonloop e}

State before:
α : Type u_1
M✝ N : Matroid α
e f✝ g : α
I X P D : Set α
M : Matroid α
f : M.removeLoops.parallelClasses.RepFun := ⋯.some
⊢ M.removeLoops ↾ ⇑⋯.some '' {e | M.Nonloop e} = M ↾ (fun a => f a) '' {e | M.Nonloop e}
Tactic:
rw [removeLoops_restr_eq_restr]
State after:
α : Type u_1
M✝ N : Matroid α
e f✝ g : α
I X P D : Set α
M : Matroid α
f : M.removeLoops.parallelClasses.RepFun := ⋯.some
⊢ ⇑⋯.some '' {e | M.Nonloop e} ⊆ {e | M.Nonloop e}

State before:
α : Type u_1
M✝ N : Matroid α
e f✝ g : α
I X P D : Set α
M : Matroid α
f : M.removeLoops.parallelClasses.RepFun := ⋯.some
⊢ ⇑⋯.some '' {e | M.Nonloop e} ⊆ {e | M.Nonloop e}
Tactic:
simpa only [M.removeLoops_nonloop_iff] using f.image_subset_self
State after:
no goals

State before:
α : Type u_1
M✝ N : Matroid α
e f✝ g : α
I X P D : Set α
M : Matroid α
f : M.removeLoops.parallelClasses.RepFun := ⋯.some
a : α
ha : a ∉ {e | M.Nonloop e}
⊢ a ∉ {e | M.removeLoops.Nonloop e}
Tactic:
simpa
State after:
no goals

State before:
α : Type u_1
M✝ N : Matroid α
e f✝ g : α
I X P D : Set α
M : Matroid α
f : M.removeLoops.parallelClasses.RepFun := ⋯.some
a : α
ha : a ∈ {e | M.Nonloop e}
⊢ M.parallelClasses.Rel a (f a)
Tactic:
simpa [mem_setOf_eq, parallelClasses_rel_eq] using f.rel_apply (by simpa)
State after:
no goals

State before:
α : Type u_1
M✝ N : Matroid α
e f✝ g : α
I X P D : Set α
M : Matroid α
f : M.removeLoops.parallelClasses.RepFun := ⋯.some
a : α
ha : a ∈ {e | M.Nonloop e}
⊢ a ∈ {e | M.removeLoops.Nonloop e}
Tactic:
simpa
State after:
no goals

State before:
α : Type u_1
M✝ N : Matroid α
e f✝ g : α
I X P D : Set α
M : Matroid α
f : M.removeLoops.parallelClasses.RepFun := ⋯.some
a b : α
hab : M.parallelClasses.Rel a b
⊢ M.removeLoops.parallelClasses.Rel a b
Tactic:
simpa
State after:
no goals