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

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
⊢ N.IsSimplification M ↔ N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
Tactic:
refine ⟨fun h ↦ ⟨h.simple.loopless, h.restriction, fun e he ↦ ?_⟩, fun ⟨h, hr, h'⟩ ↦ ?_⟩
State after:
case refine_1
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
x y : α
h : N.IsSimplification M
e : α
he : M.Nonloop e
⊢ ∃! f, f ∈ N.E ∧ M.Parallel e f

case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
h' : ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
⊢ N.IsSimplification M

State before:
case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
h' : ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
⊢ N.IsSimplification M
Tactic:
choose f hf using h'
State after:
case refine_2
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
⊢ N.IsSimplification M

State before:
case refine_2
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
⊢ N.IsSimplification M
Tactic:
refine ⟨Partition.RepFun.mk (fun x ↦ if hx : M.Nonloop x then f hx else x) ?_ ?_ ?_, ?_⟩
State after:
case refine_2.refine_1
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
⊢ ∀ a ∉ {e | M.Nonloop e}, (fun x => if hx : M.Nonloop x then f hx else x) a = a

case refine_2.refine_2
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
⊢ ∀ a ∈ {e | M.Nonloop e}, M.parallelClasses.Rel a ((fun x => if hx : M.Nonloop x then f hx else x) a)

case refine_2.refine_3
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
⊢ ∀ (a b : α),
    M.parallelClasses.Rel a b →
      (fun x => if hx : M.Nonloop x then f hx else x) a = (fun x => if hx : M.Nonloop x then f hx else x) b

case refine_2.refine_4
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
⊢ N =
    M ↾
      ⇑{ toFun := fun x => if hx : M.Nonloop x then f hx else x, apply_eq_self_of_not_mem := ?refine_2.refine_1,
            rel_apply_of_mem := ?refine_2.refine_2, apply_eq_of_rel := ?refine_2.refine_3 } ''
        {e | M.Nonloop e}

State before:
case refine_2.refine_4
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
⊢ N =
    M ↾
      ⇑{ toFun := fun x => if hx : M.Nonloop x then f hx else x, apply_eq_self_of_not_mem := ⋯, rel_apply_of_mem := ⋯,
            apply_eq_of_rel := ⋯ } ''
        {e | M.Nonloop e}
Tactic:
convert hr.eq_restrict.symm
State after:
case h.e'_3.h.e'_3
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
⊢ ⇑{ toFun := fun x => if hx : M.Nonloop x then f hx else x, apply_eq_self_of_not_mem := ⋯, rel_apply_of_mem := ⋯,
          apply_eq_of_rel := ⋯ } ''
      {e | M.Nonloop e} =
    N.E

State before:
case h.e'_3.h.e'_3
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
⊢ ⇑{ toFun := fun x => if hx : M.Nonloop x then f hx else x, apply_eq_self_of_not_mem := ⋯, rel_apply_of_mem := ⋯,
          apply_eq_of_rel := ⋯ } ''
      {e | M.Nonloop e} =
    N.E
Tactic:
refine Set.ext fun x ↦ ⟨?_, fun h ↦ ?_⟩
State after:
case h.e'_3.h.e'_3.refine_1
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x✝¹ y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
x : α
⊢ x ∈
      ⇑{ toFun := fun x => if hx : M.Nonloop x then f hx else x, apply_eq_self_of_not_mem := ⋯, rel_apply_of_mem := ⋯,
            apply_eq_of_rel := ⋯ } ''
        {e | M.Nonloop e} →
    x ∈ N.E

case h.e'_3.h.e'_3.refine_2
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x✝¹ y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h✝ : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
x : α
h : x ∈ N.E
⊢ x ∈
    ⇑{ toFun := fun x => if hx : M.Nonloop x then f hx else x, apply_eq_self_of_not_mem := ⋯, rel_apply_of_mem := ⋯,
          apply_eq_of_rel := ⋯ } ''
      {e | M.Nonloop e}

State before:
case h.e'_3.h.e'_3.refine_2
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x✝¹ y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h✝ : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
x : α
h : x ∈ N.E
⊢ x ∈
    ⇑{ toFun := fun x => if hx : M.Nonloop x then f hx else x, apply_eq_self_of_not_mem := ⋯, rel_apply_of_mem := ⋯,
          apply_eq_of_rel := ⋯ } ''
      {e | M.Nonloop e}
Tactic:
have hx := ((toNonloop h).of_restriction hr)
State after:
case h.e'_3.h.e'_3.refine_2
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x✝¹ y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h✝ : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
x : α
h : x ∈ N.E
hx : M.Nonloop x
⊢ x ∈
    ⇑{ toFun := fun x => if hx : M.Nonloop x then f hx else x, apply_eq_self_of_not_mem := ⋯, rel_apply_of_mem := ⋯,
          apply_eq_of_rel := ⋯ } ''
      {e | M.Nonloop e}

State before:
case h.e'_3.h.e'_3.refine_2
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x✝¹ y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h✝ : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
x : α
h : x ∈ N.E
hx : M.Nonloop x
⊢ x ∈
    ⇑{ toFun := fun x => if hx : M.Nonloop x then f hx else x, apply_eq_self_of_not_mem := ⋯, rel_apply_of_mem := ⋯,
          apply_eq_of_rel := ⋯ } ''
      {e | M.Nonloop e}
Tactic:
simp only [Partition.RepFun.mk_apply, mem_image, mem_setOf_eq]
State after:
case h.e'_3.h.e'_3.refine_2
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x✝¹ y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h✝ : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
x : α
h : x ∈ N.E
hx : M.Nonloop x
⊢ ∃ x_1, M.Nonloop x_1 ∧ (if hx : M.Nonloop x_1 then f hx else x_1) = x

State before:
case h.e'_3.h.e'_3.refine_2
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x✝¹ y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h✝ : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
x : α
h : x ∈ N.E
hx : M.Nonloop x
⊢ ∃ x_1, M.Nonloop x_1 ∧ (if hx : M.Nonloop x_1 then f hx else x_1) = x
Tactic:
exact ⟨x, hx, by rw [dif_pos hx, ← (hf hx).2 _ ⟨h, hx.parallel_self⟩]⟩
State after:
no goals

State before:
case refine_1
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
x y : α
h : N.IsSimplification M
e : α
he : M.Nonloop e
⊢ ∃! f, f ∈ N.E ∧ M.Parallel e f
Tactic:
obtain ⟨f, rfl⟩ := h
State after:
case refine_1.intro
α : Type u_1
M : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y e : α
he : M.Nonloop e
f : M.parallelClasses.RepFun
⊢ ∃! f_1, f_1 ∈ (M ↾ ⇑f '' {e | M.Nonloop e}).E ∧ M.Parallel e f_1

State before:
case refine_1.intro
α : Type u_1
M : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y e : α
he : M.Nonloop e
f : M.parallelClasses.RepFun
⊢ ∃! f_1, f_1 ∈ (M ↾ ⇑f '' {e | M.Nonloop e}).E ∧ M.Parallel e f_1
Tactic:
refine ⟨f e, ⟨⟨e, he, rfl⟩, f.rel_apply he⟩, ?_⟩
State after:
case refine_1.intro
α : Type u_1
M : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y e : α
he : M.Nonloop e
f : M.parallelClasses.RepFun
⊢ ∀ (y : α), (fun f_1 => f_1 ∈ (M ↾ ⇑f '' {e | M.Nonloop e}).E ∧ M.Parallel e f_1) y → y = f e

State before:
case refine_1.intro
α : Type u_1
M : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y e : α
he : M.Nonloop e
f : M.parallelClasses.RepFun
⊢ ∀ (y : α), (fun f_1 => f_1 ∈ (M ↾ ⇑f '' {e | M.Nonloop e}).E ∧ M.Parallel e f_1) y → y = f e
Tactic:
rintro _ ⟨⟨y, -, rfl⟩, hey⟩
State after:
case refine_1.intro.intro.intro.intro
α : Type u_1
M : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y✝ e : α
he : M.Nonloop e
f : M.parallelClasses.RepFun
y : α
hey : M.Parallel e (f y)
⊢ f y = f e

State before:
case refine_1.intro.intro.intro.intro
α : Type u_1
M : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y✝ e : α
he : M.Nonloop e
f : M.parallelClasses.RepFun
y : α
hey : M.Parallel e (f y)
⊢ f y = f e
Tactic:
simp [f.apply_eq_apply hey]
State after:
no goals

State before:
case refine_2.refine_1
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
⊢ ∀ a ∉ {e | M.Nonloop e}, (fun x => if hx : M.Nonloop x then f hx else x) a = a
Tactic:
exact fun a ha ↦ by simp_rw [dif_neg (show ¬ M.Nonloop a from ha)]
State after:
no goals

State before:
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
a : α
ha : a ∉ {e | M.Nonloop e}
⊢ (fun x => if hx : M.Nonloop x then f hx else x) a = a
Tactic:
simp_rw [dif_neg (show ¬ M.Nonloop a from ha)]
State after:
no goals

State before:
case refine_2.refine_2
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
⊢ ∀ a ∈ {e | M.Nonloop e}, M.parallelClasses.Rel a ((fun x => if hx : M.Nonloop x then f hx else x) a)
Tactic:
intro a (ha : M.Nonloop a)
State after:
case refine_2.refine_2
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
a : α
ha : M.Nonloop a
⊢ M.parallelClasses.Rel a ((fun x => if hx : M.Nonloop x then f hx else x) a)

State before:
case refine_2.refine_2
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
a : α
ha : M.Nonloop a
⊢ M.parallelClasses.Rel a ((fun x => if hx : M.Nonloop x then f hx else x) a)
Tactic:
simp [dif_pos ha, (hf ha).1.2]
State after:
no goals

State before:
case refine_2.refine_3
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
⊢ ∀ (a b : α),
    M.parallelClasses.Rel a b →
      (fun x => if hx : M.Nonloop x then f hx else x) a = (fun x => if hx : M.Nonloop x then f hx else x) b
Tactic:
intro a b (hab : M.Parallel a b)
State after:
case refine_2.refine_3
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
a b : α
hab : M.Parallel a b
⊢ (fun x => if hx : M.Nonloop x then f hx else x) a = (fun x => if hx : M.Nonloop x then f hx else x) b

State before:
case refine_2.refine_3
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
a b : α
hab : M.Parallel a b
⊢ (fun x => if hx : M.Nonloop x then f hx else x) a = (fun x => if hx : M.Nonloop x then f hx else x) b
Tactic:
simp only [hab.nonloop_left, ↓reduceDite, hab.nonloop_right]
State after:
case refine_2.refine_3
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
a b : α
hab : M.Parallel a b
⊢ f ⋯ = f ⋯

State before:
case refine_2.refine_3
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
a b : α
hab : M.Parallel a b
⊢ f ⋯ = f ⋯
Tactic:
exact Eq.symm <| (hf hab.nonloop_left).2 (f hab.nonloop_right)
  ⟨(hf hab.nonloop_right).1.1, hab.trans (hf hab.nonloop_right).1.2⟩
State after:
no goals

State before:
case h.e'_3.h.e'_3.refine_1
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x✝¹ y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
x : α
⊢ x ∈
      ⇑{ toFun := fun x => if hx : M.Nonloop x then f hx else x, apply_eq_self_of_not_mem := ⋯, rel_apply_of_mem := ⋯,
            apply_eq_of_rel := ⋯ } ''
        {e | M.Nonloop e} →
    x ∈ N.E
Tactic:
rintro ⟨x,(hx : M.Nonloop x),rfl⟩
State after:
case h.e'_3.h.e'_3.refine_1.intro.intro
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x✝¹ y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
x : α
hx : M.Nonloop x
⊢ { toFun := fun x => if hx : M.Nonloop x then f hx else x, apply_eq_self_of_not_mem := ⋯, rel_apply_of_mem := ⋯,
        apply_eq_of_rel := ⋯ }
      x ∈
    N.E

State before:
case h.e'_3.h.e'_3.refine_1.intro.intro
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x✝¹ y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
x : α
hx : M.Nonloop x
⊢ { toFun := fun x => if hx : M.Nonloop x then f hx else x, apply_eq_self_of_not_mem := ⋯, rel_apply_of_mem := ⋯,
        apply_eq_of_rel := ⋯ }
      x ∈
    N.E
Tactic:
simp [hx, (hf hx).1.1]
State after:
no goals

State before:
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x✝¹ y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h✝ : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
x : α
h : x ∈ N.E
hx : M.Nonloop x
⊢ (if hx : M.Nonloop x then f hx else x) = x
Tactic:
rw [dif_pos hx, ← (hf hx).2 _ ⟨h, hx.parallel_self⟩]
State after:
no goals