-- Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean
theorem liftR_map_last [lawful : LawfulMvFunctor F]
    {α : TypeVec n} {ι ι'} (R : ι' → ι' → Prop)
    (x : F (α ::: ι)) (f g : ι → ι') (hh : ∀ x : ι, R (f x) (g x)) :
    LiftR' (RelLast' _ R) ((id ::: f) <$$> x) ((id ::: g) <$$> x) :=
  let h : ι → { x : ι' × ι' // uncurry R x } := fun x => ⟨(f x, g x), hh x⟩
  let b : (α ::: ι) ⟹ _ := @diagSub n α ::: h
  let c :
    (Subtype_ α.repeatEq ::: { x // uncurry R x }) ⟹
      ((fun i : Fin2 n => { x // ofRepeat (α.RelLast' R i.fs x) }) ::: Subtype (uncurry R)) :=
    ofSubtype _ ::: id
  have hh :
    subtypeVal _ ⊚ toSubtype _ ⊚ fromAppend1DropLast ⊚ c ⊚ b =
      ((id ::: f) ⊗' (id ::: g)) ⊚ prod.diag

Proof state:
case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
lawful : LawfulMvFunctor F
α : TypeVec.{u} n
ι ι' : Type u
R : ι' → ι' → Prop
x : F (α ::: ι)
f g : ι → ι'
hh : ∀ (x : ι), R (f x) (g x)
h : ι → { x // uncurry R x } := fun x => ⟨(f x, g x), ⋯⟩
b : α ::: ι ⟹ Subtype_ α.repeatEq ::: { x // uncurry R x } := diagSub ::: h
c : Subtype_ α.repeatEq ::: { x // uncurry R x } ⟹
  (fun i => { x // ofRepeat (α.RelLast' R i.fs x) }) ::: Subtype (uncurry R) :=
  ofSubtype α.repeatEq ::: _root_.id
⊢ Subtype.val ∘ lastFun c ∘ h = Prod.map f g ∘ lastFun prod.diag

Tactic:
ext1

Result:
case h₁.h
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
lawful : LawfulMvFunctor F
α : TypeVec.{u} n
ι ι' : Type u
R : ι' → ι' → Prop
x : F (α ::: ι)
f g : ι → ι'
hh : ∀ (x : ι), R (f x) (g x)
h : ι → { x // uncurry R x } := fun x => ⟨(f x, g x), ⋯⟩
b : α ::: ι ⟹ Subtype_ α.repeatEq ::: { x // uncurry R x } := diagSub ::: h
c : Subtype_ α.repeatEq ::: { x // uncurry R x } ⟹
  (fun i => { x // ofRepeat (α.RelLast' R i.fs x) }) ::: Subtype (uncurry R) :=
  ofSubtype α.repeatEq ::: _root_.id
x✝ : (α ::: ι).last
⊢ (Subtype.val ∘ lastFun c ∘ h) x✝ = (Prod.map f g ∘ lastFun prod.diag) x✝

Proof state:
case h₀.a.h.fs
n : ℕ
ι ι' : Type u
n✝ : ℕ
a✝ : Fin2 n✝
ih : ∀ {α : TypeVec.{u} n✝} (x : (α ::: ι).drop a✝), subtypeVal α.repeatEq a✝ (diagSub a✝ x) = prod.diag a✝ x
α : TypeVec.{u} (n✝ + 1)
x : (α ::: ι).drop a✝.fs
⊢ subtypeVal α.repeatEq a✝.fs (diagSub a✝.fs x) = prod.diag a✝.fs x

Tactic:
apply ih

Result:
no goals

Proof state:
case h₀
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
lawful : LawfulMvFunctor F
α : TypeVec.{u} n
ι ι' : Type u
R : ι' → ι' → Prop
x : F (α ::: ι)
f g : ι → ι'
hh : ∀ (x : ι), R (f x) (g x)
h : ι → { x // uncurry R x } := fun x => ⟨(f x, g x), ⋯⟩
b : α ::: ι ⟹ Subtype_ α.repeatEq ::: { x // uncurry R x } := diagSub ::: h
c : Subtype_ α.repeatEq ::: { x // uncurry R x } ⟹
  (fun i => { x // ofRepeat (α.RelLast' R i.fs x) }) ::: Subtype (uncurry R) :=
  ofSubtype α.repeatEq ::: _root_.id
⊢ dropFun (subtypeVal (α.RelLast' R) ⊚ toSubtype (α.RelLast' R) ⊚ fromAppend1DropLast ⊚ c ⊚ (diagSub ::: h)) =
    dropFun (((TypeVec.id ::: f) ⊗' (TypeVec.id ::: g)) ⊚ prod.diag)

Tactic:
dsimp

Result:
case h₀
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
lawful : LawfulMvFunctor F
α : TypeVec.{u} n
ι ι' : Type u
R : ι' → ι' → Prop
x : F (α ::: ι)
f g : ι → ι'
hh : ∀ (x : ι), R (f x) (g x)
h : ι → { x // uncurry R x } := fun x => ⟨(f x, g x), ⋯⟩
b : α ::: ι ⟹ Subtype_ α.repeatEq ::: { x // uncurry R x } := diagSub ::: h
c : Subtype_ α.repeatEq ::: { x // uncurry R x } ⟹
  (fun i => { x // ofRepeat (α.RelLast' R i.fs x) }) ::: Subtype (uncurry R) :=
  ofSubtype α.repeatEq ::: _root_.id
⊢ subtypeVal α.repeatEq ⊚ dropFun (toSubtype (α.RelLast' R)) ⊚ dropFun c ⊚ diagSub =
    dropFun ((TypeVec.id ::: f) ⊗' (TypeVec.id ::: g)) ⊚ dropFun prod.diag

Proof state:
case h₀
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
lawful : LawfulMvFunctor F
α : TypeVec.{u} n
ι ι' : Type u
R : ι' → ι' → Prop
x : F (α ::: ι)
f g : ι → ι'
hh : ∀ (x : ι), R (f x) (g x)
h : ι → { x // uncurry R x } := fun x => ⟨(f x, g x), ⋯⟩
b : α ::: ι ⟹ Subtype_ α.repeatEq ::: { x // uncurry R x } := diagSub ::: h
c : Subtype_ α.repeatEq ::: { x // uncurry R x } ⟹
  (fun i => { x // ofRepeat (α.RelLast' R i.fs x) }) ::: Subtype (uncurry R) :=
  ofSubtype α.repeatEq ::: _root_.id
⊢ subtypeVal α.repeatEq ⊚ dropFun (toSubtype (α.RelLast' R)) ⊚ dropFun c ⊚ diagSub =
    dropFun ((TypeVec.id ::: f) ⊗' (TypeVec.id ::: g)) ⊚ dropFun prod.diag

Tactic:
simp only [prod_map_id, dropFun_prod, dropFun_appendFun, dropFun_diag, TypeVec.id_comp,
  dropFun_toSubtype]

Result:
case h₀
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
lawful : LawfulMvFunctor F
α : TypeVec.{u} n
ι ι' : Type u
R : ι' → ι' → Prop
x : F (α ::: ι)
f g : ι → ι'
hh : ∀ (x : ι), R (f x) (g x)
h : ι → { x // uncurry R x } := fun x => ⟨(f x, g x), ⋯⟩
b : α ::: ι ⟹ Subtype_ α.repeatEq ::: { x // uncurry R x } := diagSub ::: h
c : Subtype_ α.repeatEq ::: { x // uncurry R x } ⟹
  (fun i => { x // ofRepeat (α.RelLast' R i.fs x) }) ::: Subtype (uncurry R) :=
  ofSubtype α.repeatEq ::: _root_.id
⊢ subtypeVal α.repeatEq ⊚ (toSubtype fun i => α.RelLast' R i.fs) ⊚ dropFun c ⊚ diagSub = prod.diag

Proof state:
case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
lawful : LawfulMvFunctor F
α : TypeVec.{u} n
ι ι' : Type u
R : ι' → ι' → Prop
x : F (α ::: ι)
f g : ι → ι'
hh : ∀ (x : ι), R (f x) (g x)
h : ι → { x // uncurry R x } := fun x => ⟨(f x, g x), ⋯⟩
b : α ::: ι ⟹ Subtype_ α.repeatEq ::: { x // uncurry R x } := diagSub ::: h
c : Subtype_ α.repeatEq ::: { x // uncurry R x } ⟹
  (fun i => { x // ofRepeat (α.RelLast' R i.fs x) }) ::: Subtype (uncurry R) :=
  ofSubtype α.repeatEq ::: _root_.id
⊢ lastFun (subtypeVal (α.RelLast' R) ⊚ toSubtype (α.RelLast' R) ⊚ fromAppend1DropLast ⊚ c ⊚ (diagSub ::: h)) =
    lastFun (((TypeVec.id ::: f) ⊗' (TypeVec.id ::: g)) ⊚ prod.diag)

Tactic:
simp only [lastFun_from_append1_drop_last, lastFun_toSubtype, lastFun_appendFun,
  lastFun_subtypeVal, Function.id_comp, lastFun_comp, lastFun_prod]

Result:
case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
lawful : LawfulMvFunctor F
α : TypeVec.{u} n
ι ι' : Type u
R : ι' → ι' → Prop
x : F (α ::: ι)
f g : ι → ι'
hh : ∀ (x : ι), R (f x) (g x)
h : ι → { x // uncurry R x } := fun x => ⟨(f x, g x), ⋯⟩
b : α ::: ι ⟹ Subtype_ α.repeatEq ::: { x // uncurry R x } := diagSub ::: h
c : Subtype_ α.repeatEq ::: { x // uncurry R x } ⟹
  (fun i => { x // ofRepeat (α.RelLast' R i.fs x) }) ::: Subtype (uncurry R) :=
  ofSubtype α.repeatEq ::: _root_.id
⊢ Subtype.val ∘ lastFun c ∘ h = Prod.map f g ∘ lastFun prod.diag

Proof state:
case h₀.a.h.fz
n : ℕ
ι ι' : Type u
n✝ : ℕ
α : TypeVec.{u} (n✝ + 1)
x : (α ::: ι).drop Fin2.fz
⊢ subtypeVal α.repeatEq Fin2.fz (diagSub Fin2.fz x) = prod.diag Fin2.fz x

Tactic:
rfl

Result:
no goals

Proof state:
case h₀
n : ℕ
α : TypeVec.{u} n
ι ι' : Type u
⊢ (fun i x => subtypeVal α.repeatEq i (diagSub i x)) = prod.diag

Tactic:
ext (i x) : 2

Result:
case h₀.a.h
n : ℕ
α : TypeVec.{u} n
ι ι' : Type u
i : Fin2 n
x : (α ::: ι).drop i
⊢ subtypeVal α.repeatEq i (diagSub i x) = prod.diag i x