-- Mathlib/Control/Functor/Multivariate.lean
theorem LiftR_RelLast_iff (x y : F (α ::: β)) :
    LiftR' (RelLast' _ rr) x y ↔ LiftR (RelLast (i := _) _ rr) x y

Proof state:
case h₀.a.h.mk
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 (α ::: β)
i : Fin2 (n + 1)
x : (α ::: β) i × (α ::: β) i
property✝ : α.RelLast rr x.1 x.2
⊢ (MvFunctor.f' rr n α ⊚ MvFunctor.g' rr n α) i ⟨x, property✝⟩ = TypeVec.id i ⟨x, property✝⟩

Tactic:
cases i <;> rfl

Result:
no goals

Proof state:
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, (fun i t => (↑t).1) <$$> u = x ∧ (fun i t => (↑t).2) <$$> u = y) ↔
    ∃ u, (fun i t => (↑t).1) <$$> u = x ∧ (fun i t => (↑t).2) <$$> u = y

Tactic:
apply exists_iff_exists_of_mono F (f' rr _ _) (g' rr _ _)

Result:
case h₀
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 (α ::: β)
⊢ MvFunctor.f' rr n α ⊚ MvFunctor.g' rr n α = TypeVec.id

case h₁
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)) }),
    (fun i t => (↑t).1) <$$> u = x ∧ (fun i t => (↑t).2) <$$> u = y ↔
      (fun i t => (↑t).1) <$$> MvFunctor.f' rr n α <$$> u = x ∧ (fun i t => (↑t).2) <$$> MvFunctor.f' rr n α <$$> u = y

Proof state:
case h₁
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)) }
⊢ (fun i t => (↑t).1) <$$> u✝ = x ∧ (fun i t => (↑t).2) <$$> u✝ = y ↔
    (fun i x => (↑(MvFunctor.f' rr n α i x)).1) <$$> u✝ = x ∧ (fun i x => (↑(MvFunctor.f' rr n α i x)).2) <$$> u✝ = y

Tactic:
suffices (fun i t => t.val.fst) = ((fun i x => (MvFunctor.f' rr n α i x).val.fst))
        ∧ (fun i t => t.val.snd) = ((fun i x => (MvFunctor.f' rr n α i x).val.snd)) by
  rw [this.1, this.2]

Result:
case h₁
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)) }
⊢ ((fun i t => (↑t).1) = fun i x => (↑(MvFunctor.f' rr n α i x)).1) ∧
    (fun i t => (↑t).2) = fun i x => (↑(MvFunctor.f' rr n α i x)).2

Proof state:
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 (α ::: β)
⊢ LiftR' (α.RelLast' rr) x y ↔ LiftR (fun {i} => α.RelLast rr) x y

Tactic:
dsimp only [LiftR, LiftR']

Result:
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, (fun i t => (↑t).1) <$$> u = x ∧ (fun i t => (↑t).2) <$$> u = y) ↔
    ∃ u, (fun i t => (↑t).1) <$$> u = x ∧ (fun i t => (↑t).2) <$$> u = y

Proof state:
case h₀
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 (α ::: β)
⊢ MvFunctor.f' rr n α ⊚ MvFunctor.g' rr n α = TypeVec.id

Tactic:
ext i ⟨x, _⟩ : 2

Result:
case h₀.a.h.mk
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 (α ::: β)
i : Fin2 (n + 1)
x : (α ::: β) i × (α ::: β) i
property✝ : α.RelLast rr x.1 x.2
⊢ (MvFunctor.f' rr n α ⊚ MvFunctor.g' rr n α) i ⟨x, property✝⟩ = TypeVec.id i ⟨x, property✝⟩

Proof state:
case h₁
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)) }
⊢ ((fun i t => (↑t).1) = fun i x => (↑(MvFunctor.f' rr n α i x)).1) ∧
    (fun i t => (↑t).2) = fun i x => (↑(MvFunctor.f' rr n α i x)).2

Tactic:
constructor <;> ext i ⟨x, _⟩ <;> cases i <;> rfl

Result:
no goals

Proof state:
case h₁
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)) }
⊢ (fun i t => (↑t).1) <$$> u✝ = x ∧ (fun i t => (↑t).2) <$$> u✝ = y ↔
    (fun i t => (↑t).1) <$$> MvFunctor.f' rr n α <$$> u✝ = x ∧ (fun i t => (↑t).2) <$$> MvFunctor.f' rr n α <$$> u✝ = y

Tactic:
simp (config := { unfoldPartialApp := true }) only [map_map, TypeVec.comp]

Result:
case h₁
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)) }
⊢ (fun i t => (↑t).1) <$$> u✝ = x ∧ (fun i t => (↑t).2) <$$> u✝ = y ↔
    (fun i x => (↑(MvFunctor.f' rr n α i x)).1) <$$> u✝ = x ∧ (fun i x => (↑(MvFunctor.f' rr n α i x)).2) <$$> u✝ = y

Proof state:
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)) }
this :
  ((fun i t => (↑t).1) = fun i x => (↑(MvFunctor.f' rr n α i x)).1) ∧
    (fun i t => (↑t).2) = fun i x => (↑(MvFunctor.f' rr n α i x)).2
⊢ (fun i t => (↑t).1) <$$> u✝ = x ∧ (fun i t => (↑t).2) <$$> u✝ = y ↔
    (fun i x => (↑(MvFunctor.f' rr n α i x)).1) <$$> u✝ = x ∧ (fun i x => (↑(MvFunctor.f' rr n α i x)).2) <$$> u✝ = y

Tactic:
rw [this.1, this.2]

Result:
no goals

Proof state:
case h₁
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)) }),
    (fun i t => (↑t).1) <$$> u = x ∧ (fun i t => (↑t).2) <$$> u = y ↔
      (fun i t => (↑t).1) <$$> MvFunctor.f' rr n α <$$> u = x ∧ (fun i t => (↑t).2) <$$> MvFunctor.f' rr n α <$$> u = y

Tactic:
intros

Result:
case h₁
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)) }
⊢ (fun i t => (↑t).1) <$$> u✝ = x ∧ (fun i t => (↑t).2) <$$> u✝ = y ↔
    (fun i t => (↑t).1) <$$> MvFunctor.f' rr n α <$$> u✝ = x ∧ (fun i t => (↑t).2) <$$> MvFunctor.f' rr n α <$$> u✝ = y