-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem norm_compContinuous_linearIsometryEquiv (g : ContinuousMultilinearMap 𝕜 E₁ G)
    (f : ∀ i, E i ≃ₗᵢ[𝕜] E₁ i) :
    ‖g.compContinuousLinearMap fun i => (f i : E i →L[𝕜] E₁ i)‖ = ‖g‖

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i ≃ₗᵢ[𝕜] E₁ i
⊢ g =
    (g.compContinuousLinearMap fun i =>
          ↑{ toLinearEquiv := (f i).toLinearEquiv, continuous_toFun := ⋯,
              continuous_invFun := ⋯ }).compContinuousLinearMap
      fun i => ↑{ toLinearEquiv := (f i).symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Tactic:
ext1 m

Result:
case H
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i ≃ₗᵢ[𝕜] E₁ i
m : (i : ι) → E₁ i
⊢ g m =
    ((g.compContinuousLinearMap fun i =>
            ↑{ toLinearEquiv := (f i).toLinearEquiv, continuous_toFun := ⋯,
                continuous_invFun := ⋯ }).compContinuousLinearMap
        fun i => ↑{ toLinearEquiv := (f i).symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })
      m

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i ≃ₗᵢ[𝕜] E₁ i
this :
  g =
    (g.compContinuousLinearMap fun i =>
          ↑{ toLinearEquiv := (f i).toLinearEquiv, continuous_toFun := ⋯,
              continuous_invFun := ⋯ }).compContinuousLinearMap
      fun i => ↑{ toLinearEquiv := (f i).symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ ‖g‖ ≤ ‖g.compContinuousLinearMap fun i => (f i).toLinearIsometry.toContinuousLinearMap‖

Tactic:
conv_lhs => rw [this]

Result:
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i ≃ₗᵢ[𝕜] E₁ i
this :
  g =
    (g.compContinuousLinearMap fun i =>
          ↑{ toLinearEquiv := (f i).toLinearEquiv, continuous_toFun := ⋯,
              continuous_invFun := ⋯ }).compContinuousLinearMap
      fun i => ↑{ toLinearEquiv := (f i).symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ ‖(g.compContinuousLinearMap fun i =>
            ↑{ toLinearEquiv := (f i).toLinearEquiv, continuous_toFun := ⋯,
                continuous_invFun := ⋯ }).compContinuousLinearMap
        fun i => ↑{ toLinearEquiv := (f i).symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }‖ ≤
    ‖g.compContinuousLinearMap fun i => (f i).toLinearIsometry.toContinuousLinearMap‖

Proof state:
case H
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i ≃ₗᵢ[𝕜] E₁ i
m : (i : ι) → E₁ i
⊢ g m =
    ((g.compContinuousLinearMap fun i =>
            ↑{ toLinearEquiv := (f i).toLinearEquiv, continuous_toFun := ⋯,
                continuous_invFun := ⋯ }).compContinuousLinearMap
        fun i => ↑{ toLinearEquiv := (f i).symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })
      m

Tactic:
simp only [compContinuousLinearMap_apply, LinearIsometryEquiv.coe_coe'',
  LinearIsometryEquiv.apply_symm_apply]

Result:
no goals

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i ≃ₗᵢ[𝕜] E₁ i
⊢ ‖g‖ ≤ ‖g.compContinuousLinearMap fun i => (f i).toLinearIsometry.toContinuousLinearMap‖

Tactic:
have : g = (g.compContinuousLinearMap fun i => (f i : E i →L[𝕜] E₁ i)).compContinuousLinearMap
    fun i => ((f i).symm : E₁ i →L[𝕜] E i) := by
  ext1 m
  simp only [compContinuousLinearMap_apply, LinearIsometryEquiv.coe_coe'',
    LinearIsometryEquiv.apply_symm_apply]

Result:
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i ≃ₗᵢ[𝕜] E₁ i
this :
  g =
    (g.compContinuousLinearMap fun i =>
          ↑{ toLinearEquiv := (f i).toLinearEquiv, continuous_toFun := ⋯,
              continuous_invFun := ⋯ }).compContinuousLinearMap
      fun i => ↑{ toLinearEquiv := (f i).symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ ‖g‖ ≤ ‖g.compContinuousLinearMap fun i => (f i).toLinearIsometry.toContinuousLinearMap‖

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i ≃ₗᵢ[𝕜] E₁ i
this :
  g =
    (g.compContinuousLinearMap fun i =>
          ↑{ toLinearEquiv := (f i).toLinearEquiv, continuous_toFun := ⋯,
              continuous_invFun := ⋯ }).compContinuousLinearMap
      fun i => ↑{ toLinearEquiv := (f i).symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ ‖(g.compContinuousLinearMap fun i =>
            ↑{ toLinearEquiv := (f i).toLinearEquiv, continuous_toFun := ⋯,
                continuous_invFun := ⋯ }).compContinuousLinearMap
        fun i => ↑{ toLinearEquiv := (f i).symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }‖ ≤
    ‖g.compContinuousLinearMap fun i => (f i).toLinearIsometry.toContinuousLinearMap‖

Tactic:
apply (g.compContinuousLinearMap fun i =>
  (f i : E i →L[𝕜] E₁ i)).norm_compContinuous_linearIsometry_le
    fun i => (f i).symm.toLinearIsometry

Result:
no goals