case h
𝕂 : Type u_3
𝔸✝ : Type ?u.766093
𝔹 : Type ?u.766096
inst✝¹⁰ : IsROrC 𝕂
inst✝⁹ : NormedRing 𝔸✝
inst✝⁸ : NormedAlgebra 𝕂 𝔸✝
inst✝⁷ : NormedRing 𝔹
inst✝⁶ : NormedAlgebra 𝕂 𝔹
inst✝⁵ : CompleteSpace 𝔸✝
ι : Type u_1
𝔸 : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → NormedRing (𝔸 i)
inst✝¹ : (i : ι) → NormedAlgebra 𝕂 (𝔸 i)
inst✝ : ∀ (i : ι), CompleteSpace (𝔸 i)
x : (i : ι) → 𝔸 i
j : ι
xj : 𝔸 j
i : ι
⊢ update (exp 𝕂 x) j (exp 𝕂 xj) i = exp 𝕂 (update x j xj) i
𝕂 : Type u_3
𝔸✝ : Type ?u.766093
𝔹 : Type ?u.766096
inst✝¹⁰ : IsROrC 𝕂
inst✝⁹ : NormedRing 𝔸✝
inst✝⁸ : NormedAlgebra 𝕂 𝔸✝
inst✝⁷ : NormedRing 𝔹
inst✝⁶ : NormedAlgebra 𝕂 𝔹
inst✝⁵ : CompleteSpace 𝔸✝
ι : Type u_1
𝔸 : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → NormedRing (𝔸 i)
inst✝¹ : (i : ι) → NormedAlgebra 𝕂 (𝔸 i)
inst✝ : ∀ (i : ι), CompleteSpace (𝔸 i)
x : (i : ι) → 𝔸 i
j : ι
xj : 𝔸 j
⊢ update (exp 𝕂 x) j (exp 𝕂 xj) = exp 𝕂 (update x j xj)
ext i
case h
𝕂 : Type u_3
𝔸✝ : Type ?u.766093
𝔹 : Type ?u.766096
inst✝¹⁰ : IsROrC 𝕂
inst✝⁹ : NormedRing 𝔸✝
inst✝⁸ : NormedAlgebra 𝕂 𝔸✝
inst✝⁷ : NormedRing 𝔹
inst✝⁶ : NormedAlgebra 𝕂 𝔹
inst✝⁵ : CompleteSpace 𝔸✝
ι : Type u_1
𝔸 : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → NormedRing (𝔸 i)
inst✝¹ : (i : ι) → NormedAlgebra 𝕂 (𝔸 i)
inst✝ : ∀ (i : ι), CompleteSpace (𝔸 i)
x : (i : ι) → 𝔸 i
j : ι
xj : 𝔸 j
i : ι
⊢ update (fun i => exp 𝕂 (x i)) j (exp 𝕂 xj) i = exp 𝕂 (update x j xj i)
case h
𝕂 : Type u_3
𝔸✝ : Type ?u.766093
𝔹 : Type ?u.766096
inst✝¹⁰ : IsROrC 𝕂
inst✝⁹ : NormedRing 𝔸✝
inst✝⁸ : NormedAlgebra 𝕂 𝔸✝
inst✝⁷ : NormedRing 𝔹
inst✝⁶ : NormedAlgebra 𝕂 𝔹
inst✝⁵ : CompleteSpace 𝔸✝
ι : Type u_1
𝔸 : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → NormedRing (𝔸 i)
inst✝¹ : (i : ι) → NormedAlgebra 𝕂 (𝔸 i)
inst✝ : ∀ (i : ι), CompleteSpace (𝔸 i)
x : (i : ι) → 𝔸 i
j : ι
xj : 𝔸 j
i : ι
⊢ update (exp 𝕂 x) j (exp 𝕂 xj) i = exp 𝕂 (update x j xj) i
simp_rw [Pi.exp_def]
no goals
case h
𝕂 : Type u_3
𝔸✝ : Type ?u.766093
𝔹 : Type ?u.766096
inst✝¹⁰ : IsROrC 𝕂
inst✝⁹ : NormedRing 𝔸✝
inst✝⁸ : NormedAlgebra 𝕂 𝔸✝
inst✝⁷ : NormedRing 𝔹
inst✝⁶ : NormedAlgebra 𝕂 𝔹
inst✝⁵ : CompleteSpace 𝔸✝
ι : Type u_1
𝔸 : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → NormedRing (𝔸 i)
inst✝¹ : (i : ι) → NormedAlgebra 𝕂 (𝔸 i)
inst✝ : ∀ (i : ι), CompleteSpace (𝔸 i)
x : (i : ι) → 𝔸 i
j : ι
xj : 𝔸 j
i : ι
⊢ update (fun i => exp 𝕂 (x i)) j (exp 𝕂 xj) i = exp 𝕂 (update x j xj i)
exact (Function.apply_update (fun i => exp 𝕂) x j xj i).symm