p : ℝ≥0∞
𝕜 : Type u_4
𝕜' : Type ?u.384596
ι : Type u_1
α : ι → Type ?u.384604
β : ι → Type ?u.384609
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
e : ι ≃ ι'
z : PiLp p fun x => E
⊢ ↑(LinearEquiv.symm (LinearEquiv.piCongrLeft' 𝕜 (fun x => E) e)) z =
    ↑(LinearEquiv.piCongrLeft' 𝕜 (fun x => E) e.symm) z
p : ℝ≥0∞
𝕜 : Type u_4
𝕜' : Type ?u.384596
ι : Type u_1
α : ι → Type ?u.384604
β : ι → Type ?u.384609
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
e : ι ≃ ι'
z : PiLp p fun x => E
⊢ ↑(LinearIsometryEquiv.symm (LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e)) z =
    ↑(LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e.symm) z
simp only [LinearIsometryEquiv.piLpCongrLeft, LinearIsometryEquiv.symm,
  LinearIsometryEquiv.coe_mk]
p : ℝ≥0∞
𝕜 : Type u_4
𝕜' : Type ?u.384596
ι : Type u_1
α : ι → Type ?u.384604
β : ι → Type ?u.384609
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
e : ι ≃ ι'
z : PiLp p fun x => E
⊢ ↑(LinearEquiv.symm (LinearEquiv.piCongrLeft' 𝕜 (fun x => E) e)) z =
    ↑(LinearEquiv.piCongrLeft' 𝕜 (fun x => E) e.symm) z
p : ℝ≥0∞
𝕜 : Type u_4
𝕜' : Type ?u.384596
ι : Type u_1
α : ι → Type ?u.384604
β : ι → Type ?u.384609
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
e : ι ≃ ι'
z : PiLp p fun x => E
⊢ ↑(LinearEquiv.symm (LinearEquiv.piCongrLeft' 𝕜 (fun x => E) e)) z =
    ↑(LinearEquiv.piCongrLeft' 𝕜 (fun x => E) e.symm) z
unfold PiLp
case h
p : ℝ≥0∞
𝕜 : Type u_4
𝕜' : Type ?u.384596
ι : Type u_1
α : ι → Type ?u.384604
β : ι → Type ?u.384609
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
e : ι ≃ ι'
z : PiLp p fun x => E
x✝ : ι
⊢ ↑(LinearEquiv.symm (LinearEquiv.piCongrLeft' 𝕜 (fun x => E) e)) z x✝ =
    ↑(LinearEquiv.piCongrLeft' 𝕜 (fun x => E) e.symm) z x✝
p : ℝ≥0∞
𝕜 : Type u_4
𝕜' : Type ?u.384596
ι : Type u_1
α : ι → Type ?u.384604
β : ι → Type ?u.384609
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
e : ι ≃ ι'
z : PiLp p fun x => E
⊢ ↑(LinearEquiv.symm (LinearEquiv.piCongrLeft' 𝕜 (fun x => E) e)) z =
    ↑(LinearEquiv.piCongrLeft' 𝕜 (fun x => E) e.symm) z
ext
no goals
case h
p : ℝ≥0∞
𝕜 : Type u_4
𝕜' : Type ?u.384596
ι : Type u_1
α : ι → Type ?u.384604
β : ι → Type ?u.384609
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
e : ι ≃ ι'
z : PiLp p fun x => E
x✝ : ι
⊢ ↑(LinearEquiv.symm (LinearEquiv.piCongrLeft' 𝕜 (fun x => E) e)) z x✝ =
    ↑(LinearEquiv.piCongrLeft' 𝕜 (fun x => E) e.symm) z x✝
simp only [LinearEquiv.piCongrLeft'_symm_apply, eq_rec_constant,
  LinearEquiv.piCongrLeft'_apply, Equiv.symm_symm_apply]