case a.h
n✝ n : ℕ
α α' β β' : TypeVec n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
i : Fin2 (n + 1)
a : ((α ⊗ β) ::: (φ × ψ)) i
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) i a = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁)) i a
n✝ n : ℕ
α α' β β' : TypeVec n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁))
ext (i a)
case a.h.fz
n✝ n : ℕ
α α' β β' : TypeVec n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
a : ((α ⊗ β) ::: (φ × ψ)) Fin2.fz
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) Fin2.fz a = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁)) Fin2.fz a

case a.h.fs
n✝ n : ℕ
α α' β β' : TypeVec n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
a✝ : Fin2 (Nat.add n 0)
a : ((α ⊗ β) ::: (φ × ψ)) (Fin2.fs a✝)
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) (Fin2.fs a✝) a = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁)) (Fin2.fs a✝) a
case a.h
n✝ n : ℕ
α α' β β' : TypeVec n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
i : Fin2 (n + 1)
a : ((α ⊗ β) ::: (φ × ψ)) i
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) i a = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁)) i a
cases i
case a.h.fs
n✝ n : ℕ
α α' β β' : TypeVec n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
a✝ : Fin2 (Nat.add n 0)
a : ((α ⊗ β) ::: (φ × ψ)) (Fin2.fs a✝)
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) (Fin2.fs a✝) a = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁)) (Fin2.fs a✝) a
case a.h.fz
n✝ n : ℕ
α α' β β' : TypeVec n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
a : ((α ⊗ β) ::: (φ × ψ)) Fin2.fz
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) Fin2.fz a = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁)) Fin2.fz a

case a.h.fs
n✝ n : ℕ
α α' β β' : TypeVec n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
a✝ : Fin2 (Nat.add n 0)
a : ((α ⊗ β) ::: (φ × ψ)) (Fin2.fs a✝)
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) (Fin2.fs a✝) a = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁)) (Fin2.fs a✝) a
. cases a
  rfl
no goals
case a.h.fs
n✝ n : ℕ
α α' β β' : TypeVec n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
a✝ : Fin2 (Nat.add n 0)
a : ((α ⊗ β) ::: (φ × ψ)) (Fin2.fs a✝)
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) (Fin2.fs a✝) a = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁)) (Fin2.fs a✝) a
. rfl
case a.h.fz.mk
n✝ n : ℕ
α α' β β' : TypeVec n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
fst✝ : φ
snd✝ : ψ
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) Fin2.fz (fst✝, snd✝) = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁)) Fin2.fz (fst✝, snd✝)
case a.h.fz
n✝ n : ℕ
α α' β β' : TypeVec n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
a : ((α ⊗ β) ::: (φ × ψ)) Fin2.fz
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) Fin2.fz a = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁)) Fin2.fz a
cases a
no goals
case a.h.fz.mk
n✝ n : ℕ
α α' β β' : TypeVec n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
fst✝ : φ
snd✝ : ψ
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) Fin2.fz (fst✝, snd✝) = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁)) Fin2.fz (fst✝, snd✝)
rfl
no goals
case a.h.fs
n✝ n : ℕ
α α' β β' : TypeVec n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
a✝ : Fin2 (Nat.add n 0)
a : ((α ⊗ β) ::: (φ × ψ)) (Fin2.fs a✝)
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) (Fin2.fs a✝) a = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁)) (Fin2.fs a✝) a
rfl