case h
p : ℝ≥0∞
𝕜 : Type u_4
𝕜' : Type ?u.391376
ι : Type u_1
α : ι → Type ?u.391384
β : ι → Type ?u.391389
inst✝¹⁰ : Fintype ι
inst✝⁹ : Fact (1 ≤ p)
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedField 𝕜'
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
x✝ y : PiLp p β
x' y' : (i : ι) → β i
i✝ : ι
ι' : Type u_2
inst✝⁴ : Fintype ι'
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
e : ι ≃ ι'
i : ι
v : E
x : ι'
⊢ ↑(LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e) (↑(PiLp.equiv p fun x => E).symm (Pi.single i v)) x =
    ↑(PiLp.equiv p fun x => E).symm (Pi.single (↑e i) v) x
p : ℝ≥0∞
𝕜 : Type u_4
𝕜' : Type ?u.391376
ι : Type u_1
α : ι → Type ?u.391384
β : ι → Type ?u.391389
inst✝¹⁰ : Fintype ι
inst✝⁹ : Fact (1 ≤ p)
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedField 𝕜'
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
x y : PiLp p β
x' y' : (i : ι) → β i
i✝ : ι
ι' : Type u_2
inst✝⁴ : Fintype ι'
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
e : ι ≃ ι'
i : ι
v : E
⊢ ↑(LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e) (↑(PiLp.equiv p fun x => E).symm (Pi.single i v)) =
    ↑(PiLp.equiv p fun x => E).symm (Pi.single (↑e i) v)
funext x
no goals
case h
p : ℝ≥0∞
𝕜 : Type u_4
𝕜' : Type ?u.391376
ι : Type u_1
α : ι → Type ?u.391384
β : ι → Type ?u.391389
inst✝¹⁰ : Fintype ι
inst✝⁹ : Fact (1 ≤ p)
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedField 𝕜'
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
x✝ y : PiLp p β
x' y' : (i : ι) → β i
i✝ : ι
ι' : Type u_2
inst✝⁴ : Fintype ι'
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
e : ι ≃ ι'
i : ι
v : E
x : ι'
⊢ ↑(LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e) (↑(PiLp.equiv p fun x => E).symm (Pi.single i v)) x =
    ↑(PiLp.equiv p fun x => E).symm (Pi.single (↑e i) v) x
simp [LinearIsometryEquiv.piLpCongrLeft_apply, LinearEquiv.piCongrLeft', Equiv.piCongrLeft',
  Pi.single, Function.update, Equiv.symm_apply_eq]