-- Mathlib/Control/Functor/Multivariate.lean
theorem LiftP_PredLast_iff {β} (P : β → Prop) (x : F (α ::: β)) :
    LiftP' (PredLast' _ P) x ↔ LiftP (PredLast _ P) x

Proof state:
case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (α.PredLast' P i p_1) }
⊢ (fun i => Subtype.val) <$$> u✝ = x ↔ (fun i => Subtype.val) <$$> MvFunctor.f P n α <$$> u✝ = x

Tactic:
rw [MvFunctor.map_map]

Result:
case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (α.PredLast' P i p_1) }
⊢ (fun i => Subtype.val) <$$> u✝ = x ↔ ((fun i => Subtype.val) ⊚ MvFunctor.f P n α) <$$> u✝ = x

Proof state:
case h₀.a.h.mk.a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x✝ : F (α ::: β)
i : Fin2 (n + 1)
x : (α ::: β) i
property✝ : α.PredLast P x
⊢ ↑((MvFunctor.f P n α ⊚ MvFunctor.g P n α) i ⟨x, property✝⟩) = ↑(TypeVec.id i ⟨x, property✝⟩)

Tactic:
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
P : β → Prop
x : F (α ::: β)
⊢ MvFunctor.f P n α ⊚ MvFunctor.g P n α = TypeVec.id

Tactic:
ext i ⟨x, _⟩

Result:
case h₀.a.h.mk.a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x✝ : F (α ::: β)
i : Fin2 (n + 1)
x : (α ::: β) i
property✝ : α.PredLast P x
⊢ ↑((MvFunctor.f P n α ⊚ MvFunctor.g P 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
P : β → Prop
x : F (α ::: β)
⊢ ∀ (u : F fun i => { p_1 // ofRepeat (α.PredLast' P i p_1) }),
    (fun i => Subtype.val) <$$> u = x ↔ (fun i => Subtype.val) <$$> MvFunctor.f P n α <$$> u = x

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
P : β → Prop
x : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (α.PredLast' P i p_1) }
⊢ (fun i => Subtype.val) <$$> u✝ = x ↔ (fun i => Subtype.val) <$$> MvFunctor.f P n α <$$> u✝ = x

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
⊢ LiftP' (α.PredLast' P) x ↔ LiftP (α.PredLast P) x

Tactic:
dsimp only [LiftP, LiftP']

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
⊢ (∃ u, (fun i => Subtype.val) <$$> u = x) ↔ ∃ u, (fun i => Subtype.val) <$$> u = x

Proof state:
case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (α.PredLast' P i p_1) }
⊢ (fun i => Subtype.val) <$$> u✝ = x ↔ (fun i x => ↑(MvFunctor.f P n α i x)) <$$> u✝ = x

Tactic:
suffices (fun i => Subtype.val) = (fun i x => (MvFunctor.f P n α i x).val) by rw [this]

Result:
case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (α.PredLast' P i p_1) }
⊢ (fun i => Subtype.val) = fun i x => ↑(MvFunctor.f P n α i x)

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
⊢ (∃ u, (fun i => Subtype.val) <$$> u = x) ↔ ∃ u, (fun i => Subtype.val) <$$> u = x

Tactic:
apply exists_iff_exists_of_mono F (f _ n α) (g _ n α)

Result:
case h₀
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
⊢ MvFunctor.f P n α ⊚ MvFunctor.g P 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
P : β → Prop
x : F (α ::: β)
⊢ ∀ (u : F fun i => { p_1 // ofRepeat (α.PredLast' P i p_1) }),
    (fun i => Subtype.val) <$$> u = x ↔ (fun i => Subtype.val) <$$> MvFunctor.f P n α <$$> u = x

Proof state:
case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (α.PredLast' P i p_1) }
⊢ (fun i => Subtype.val) = fun i x => ↑(MvFunctor.f P n α i x)

Tactic:
ext i ⟨x, _⟩

Result:
case h₁.h.h.mk
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x✝ : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (α.PredLast' P i p_1) }
i : Fin2 (n + 1)
x : (α ::: β) i
property✝ : ofRepeat (α.PredLast' P i x)
⊢ ↑⟨x, property✝⟩ = ↑(MvFunctor.f P n α i ⟨x, property✝⟩)

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (α.PredLast' P i p_1) }
this : (fun i => Subtype.val) = fun i x => ↑(MvFunctor.f P n α i x)
⊢ (fun i => Subtype.val) <$$> u✝ = x ↔ (fun i x => ↑(MvFunctor.f P n α i x)) <$$> u✝ = x

Tactic:
rw [this]

Result:
no goals

Proof state:
case h₁.h.h.mk
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x✝ : F (α ::: β)
u✝ : F fun i => { p_1 // ofRepeat (α.PredLast' P i p_1) }
i : Fin2 (n + 1)
x : (α ::: β) i
property✝ : ofRepeat (α.PredLast' P i x)
⊢ ↑⟨x, property✝⟩ = ↑(MvFunctor.f P n α i ⟨x, property✝⟩)

Tactic:
cases i <;> rfl

Result:
no goals