-- Mathlib/Analysis/InnerProductSpace/ProdL2.lean
theorem prod_apply (v : OrthonormalBasis ι₁ 𝕜 E) (w : OrthonormalBasis ι₂ 𝕜 F) :
    ∀ i : ι₁ ⊕ ι₂, v.prod w i =
      Sum.elim ((LinearMap.inl 𝕜 E F) ∘ v) ((LinearMap.inr 𝕜 E F) ∘ w) i

Proof state:
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : Fintype ι₁
inst✝ : Fintype ι₂
v : OrthonormalBasis ι₁ 𝕜 E
w : OrthonormalBasis ι₂ 𝕜 F
⊢ (∀ (a : ι₁),
      (((v.toBasis.prod w.toBasis).map (WithLp.linearEquiv 2 𝕜 (E × F)).symm).toOrthonormalBasis ⋯) (Sum.inl a) =
        Sum.elim (⇑(LinearMap.inl 𝕜 E F) ∘ ⇑v) (⇑(LinearMap.inr 𝕜 E F) ∘ ⇑w) (Sum.inl a)) ∧
    ∀ (b : ι₂),
      (((v.toBasis.prod w.toBasis).map (WithLp.linearEquiv 2 𝕜 (E × F)).symm).toOrthonormalBasis ⋯) (Sum.inr b) =
        Sum.elim (⇑(LinearMap.inl 𝕜 E F) ∘ ⇑v) (⇑(LinearMap.inr 𝕜 E F) ∘ ⇑w) (Sum.inr b)

Tactic:
aesop

Result:
no goals

Proof state:
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : Fintype ι₁
inst✝ : Fintype ι₂
v : OrthonormalBasis ι₁ 𝕜 E
w : OrthonormalBasis ι₂ 𝕜 F
⊢ (∀ (a : ι₁),
      (v.prod w) (Sum.inl a) = Sum.elim (⇑(LinearMap.inl 𝕜 E F) ∘ ⇑v) (⇑(LinearMap.inr 𝕜 E F) ∘ ⇑w) (Sum.inl a)) ∧
    ∀ (b : ι₂),
      (v.prod w) (Sum.inr b) = Sum.elim (⇑(LinearMap.inl 𝕜 E F) ∘ ⇑v) (⇑(LinearMap.inr 𝕜 E F) ∘ ⇑w) (Sum.inr b)

Tactic:
unfold OrthonormalBasis.prod

Result:
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : Fintype ι₁
inst✝ : Fintype ι₂
v : OrthonormalBasis ι₁ 𝕜 E
w : OrthonormalBasis ι₂ 𝕜 F
⊢ (∀ (a : ι₁),
      (((v.toBasis.prod w.toBasis).map (WithLp.linearEquiv 2 𝕜 (E × F)).symm).toOrthonormalBasis ⋯) (Sum.inl a) =
        Sum.elim (⇑(LinearMap.inl 𝕜 E F) ∘ ⇑v) (⇑(LinearMap.inr 𝕜 E F) ∘ ⇑w) (Sum.inl a)) ∧
    ∀ (b : ι₂),
      (((v.toBasis.prod w.toBasis).map (WithLp.linearEquiv 2 𝕜 (E × F)).symm).toOrthonormalBasis ⋯) (Sum.inr b) =
        Sum.elim (⇑(LinearMap.inl 𝕜 E F) ∘ ⇑v) (⇑(LinearMap.inr 𝕜 E F) ∘ ⇑w) (Sum.inr b)

Proof state:
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : Fintype ι₁
inst✝ : Fintype ι₂
v : OrthonormalBasis ι₁ 𝕜 E
w : OrthonormalBasis ι₂ 𝕜 F
⊢ ∀ (i : ι₁ ⊕ ι₂), (v.prod w) i = Sum.elim (⇑(LinearMap.inl 𝕜 E F) ∘ ⇑v) (⇑(LinearMap.inr 𝕜 E F) ∘ ⇑w) i

Tactic:
rw [Sum.forall]

Result:
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : Fintype ι₁
inst✝ : Fintype ι₂
v : OrthonormalBasis ι₁ 𝕜 E
w : OrthonormalBasis ι₂ 𝕜 F
⊢ (∀ (a : ι₁),
      (v.prod w) (Sum.inl a) = Sum.elim (⇑(LinearMap.inl 𝕜 E F) ∘ ⇑v) (⇑(LinearMap.inr 𝕜 E F) ∘ ⇑w) (Sum.inl a)) ∧
    ∀ (b : ι₂),
      (v.prod w) (Sum.inr b) = Sum.elim (⇑(LinearMap.inl 𝕜 E F) ∘ ⇑v) (⇑(LinearMap.inr 𝕜 E F) ∘ ⇑w) (Sum.inr b)