Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₁.e_a.e_a.e_a.fz
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x✝ y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
x : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz
property✝ : ofRepeat (α.RelLast' rr Fin2.fz (prod.mk Fin2.fz x.1 x.2))
⊢ (↑⟨x, property✝⟩).1 = (↑(f' rr n α Fin2.fz ⟨x, property✝⟩)).1

pp: case h₁.e_a.e_a.e_a.fs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x✝ y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
a✝ : Fin2 n
x : (α ::: β) a✝.fs × (α ::: β) a✝.fs
property✝ : ofRepeat (α.RelLast' rr a✝.fs (prod.mk a✝.fs x.1 x.2))
⊢ (↑⟨x, property✝⟩).1 = (↑(f' rr n α a✝.fs ⟨x, property✝⟩)).1

pp: case h₁.e_b.e_a.e_a.fz
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x✝ y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
x : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz
property✝ : ofRepeat (α.RelLast' rr Fin2.fz (prod.mk Fin2.fz x.1 x.2))
⊢ (↑⟨x, property✝⟩).2 = (↑(f' rr n α Fin2.fz ⟨x, property✝⟩)).2

pp: case h₁.e_b.e_a.e_a.fs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x✝ y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
a✝ : Fin2 n
x : (α ::: β) a✝.fs × (α ::: β) a✝.fs
property✝ : ofRepeat (α.RelLast' rr a✝.fs (prod.mk a✝.fs x.1 x.2))
⊢ (↑⟨x, property✝⟩).2 = (↑(f' rr n α a✝.fs ⟨x, property✝⟩)).2

Tactic:
<;>

Goal state after:
case h₁.e_a.e_a.e_a.fz
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x✝ y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
x : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz
property✝ : ofRepeat (α.RelLast' rr Fin2.fz (prod.mk Fin2.fz x.1 x.2))
⊢ (↑⟨x, property✝⟩).1 = (↑(f' rr n α Fin2.fz ⟨x, property✝⟩)).1

case h₁.e_a.e_a.e_a.fs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x✝ y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
a✝ : Fin2 n
x : (α ::: β) a✝.fs × (α ::: β) a✝.fs
property✝ : ofRepeat (α.RelLast' rr a✝.fs (prod.mk a✝.fs x.1 x.2))
⊢ (↑⟨x, property✝⟩).1 = (↑(f' rr n α a✝.fs ⟨x, property✝⟩)).1

case h₁.e_b.e_a.e_a.fz
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x✝ y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
x : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz
property✝ : ofRepeat (α.RelLast' rr Fin2.fz (prod.mk Fin2.fz x.1 x.2))
⊢ (↑⟨x, property✝⟩).2 = (↑(f' rr n α Fin2.fz ⟨x, property✝⟩)).2

case h₁.e_b.e_a.e_a.fs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x✝ y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
a✝ : Fin2 n
x : (α ::: β) a✝.fs × (α ::: β) a✝.fs
property✝ : ofRepeat (α.RelLast' rr a✝.fs (prod.mk a✝.fs x.1 x.2))
⊢ (↑⟨x, property✝⟩).2 = (↑(f' rr n α a✝.fs ⟨x, property✝⟩)).2