Theorem: SciLean.inner_proj_dualProj (SciLean/Core/Objects/FinVec.lean)

State before:
ι : Type u_1
K X : Type u_2
x✝ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : RCLike K
inst✝ : FinVec ι K X
x y : X
⊢ ⟪x, y⟫_K = ∑ i, ℼ i x * ℼ' i y
Tactic:
calc
  ⟪x, y⟫[K] = ∑ i, ∑ j, ⟪(ℼ i x) • ⅇ[X] i, (ℼ' j y) • ⅇ' j⟫[K] := by sorry_proof _ = ∑ i, ∑ j, (ℼ i x * ℼ' j y) * ⟪ⅇ[X] i, ⅇ' j⟫[K] := by sorry_proof _ = ∑ i, ∑ j, (ℼ i x * ℼ' j y) * if i=j then 1 else 0 := by simp [FinVec.duality]
       _ = ∑ i, ℼ i x * ℼ' i y := sorry_proof
State after:
no goals

State before:
ι : Type u_1
K X : Type u_2
x✝ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : RCLike K
inst✝ : FinVec ι K X
x y : X
⊢ ⟪x, y⟫_K = ∑ i, ∑ j, ⟪ℼ i x • ⅇ i, ℼ' j y • ⅇ' j⟫_K
Tactic:
sorry_proof
State after:
no goals

State before:
ι : Type u_1
K X : Type u_2
x✝ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : RCLike K
inst✝ : FinVec ι K X
x y : X
⊢  ∑ i, ∑ j, ⟪ℼ i x • ⅇ i, ℼ' j y • ⅇ' j⟫_K = ∑ i, ∑ j, ℼ i x * ℼ' j y * ⟪ⅇ i, ⅇ' j⟫_K
Tactic:
sorry_proof
State after:
no goals

State before:
ι : Type u_1
K X : Type u_2
x✝ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : RCLike K
inst✝ : FinVec ι K X
x y : X
⊢  ∑ i, ∑ j, ℼ i x * ℼ' j y * ⟪ⅇ i, ⅇ' j⟫_K = ∑ i, ∑ j, ℼ i x * ℼ' j y * if i = j then 1 else 0
Tactic:
simp [FinVec.duality]
State after:
no goals