-- Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean
theorem opNorm_comp_linearIsometryEquiv (f : F →SL[σ₂₃] G) (g : F' ≃ₛₗᵢ[σ₂'] F) :
    ‖f.comp g.toLinearIsometry.toContinuousLinearMap‖ = ‖f‖

Proof state:
case inr.refine_2
𝕜₂ : Type u_2
𝕜₃ : Type u_3
F : Type u_5
G : Type u_7
inst✝¹⁶ : NormedAddCommGroup F
inst✝¹⁵ : NormedAddCommGroup G
inst✝¹⁴ : NontriviallyNormedField 𝕜₂
inst✝¹³ : NontriviallyNormedField 𝕜₃
inst✝¹² : NormedSpace 𝕜₂ F
inst✝¹¹ : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
𝕜₂' : Type u_8
inst✝¹⁰ : NontriviallyNormedField 𝕜₂'
F' : Type u_9
inst✝⁹ : NormedAddCommGroup F'
inst✝⁸ : NormedSpace 𝕜₂' F'
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂'' : 𝕜₂ →+* 𝕜₂'
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst✝⁷ : RingHomInvPair σ₂' σ₂''
inst✝⁶ : RingHomInvPair σ₂'' σ₂'
inst✝⁵ : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst✝⁴ : RingHomCompTriple σ₂'' σ₂₃' σ₂₃
inst✝³ : RingHomIsometric σ₂₃
inst✝² : RingHomIsometric σ₂'
inst✝¹ : RingHomIsometric σ₂''
inst✝ : RingHomIsometric σ₂₃'
f : F →SL[σ₂₃] G
g : F' ≃ₛₗᵢ[σ₂'] F
h✝ : Nontrivial F'
⊢ ‖f‖ ≤ ‖f.comp g.toLinearIsometry.toContinuousLinearMap‖

Tactic:
convert (f.comp g.toLinearIsometry.toContinuousLinearMap).opNorm_comp_le
    g.symm.toLinearIsometry.toContinuousLinearMap

Result:
case h.e'_3.h.e'_3
𝕜₂ : Type u_2
𝕜₃ : Type u_3
F : Type u_5
G : Type u_7
inst✝¹⁶ : NormedAddCommGroup F
inst✝¹⁵ : NormedAddCommGroup G
inst✝¹⁴ : NontriviallyNormedField 𝕜₂
inst✝¹³ : NontriviallyNormedField 𝕜₃
inst✝¹² : NormedSpace 𝕜₂ F
inst✝¹¹ : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
𝕜₂' : Type u_8
inst✝¹⁰ : NontriviallyNormedField 𝕜₂'
F' : Type u_9
inst✝⁹ : NormedAddCommGroup F'
inst✝⁸ : NormedSpace 𝕜₂' F'
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂'' : 𝕜₂ →+* 𝕜₂'
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst✝⁷ : RingHomInvPair σ₂' σ₂''
inst✝⁶ : RingHomInvPair σ₂'' σ₂'
inst✝⁵ : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst✝⁴ : RingHomCompTriple σ₂'' σ₂₃' σ₂₃
inst✝³ : RingHomIsometric σ₂₃
inst✝² : RingHomIsometric σ₂'
inst✝¹ : RingHomIsometric σ₂''
inst✝ : RingHomIsometric σ₂₃'
f : F →SL[σ₂₃] G
g : F' ≃ₛₗᵢ[σ₂'] F
h✝ : Nontrivial F'
⊢ f = (f.comp g.toLinearIsometry.toContinuousLinearMap).comp g.symm.toLinearIsometry.toContinuousLinearMap

case h.e'_4
𝕜₂ : Type u_2
𝕜₃ : Type u_3
F : Type u_5
G : Type u_7
inst✝¹⁶ : NormedAddCommGroup F
inst✝¹⁵ : NormedAddCommGroup G
inst✝¹⁴ : NontriviallyNormedField 𝕜₂
inst✝¹³ : NontriviallyNormedField 𝕜₃
inst✝¹² : NormedSpace 𝕜₂ F
inst✝¹¹ : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
𝕜₂' : Type u_8
inst✝¹⁰ : NontriviallyNormedField 𝕜₂'
F' : Type u_9
inst✝⁹ : NormedAddCommGroup F'
inst✝⁸ : NormedSpace 𝕜₂' F'
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂'' : 𝕜₂ →+* 𝕜₂'
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst✝⁷ : RingHomInvPair σ₂' σ₂''
inst✝⁶ : RingHomInvPair σ₂'' σ₂'
inst✝⁵ : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst✝⁴ : RingHomCompTriple σ₂'' σ₂₃' σ₂₃
inst✝³ : RingHomIsometric σ₂₃
inst✝² : RingHomIsometric σ₂'
inst✝¹ : RingHomIsometric σ₂''
inst✝ : RingHomIsometric σ₂₃'
f : F →SL[σ₂₃] G
g : F' ≃ₛₗᵢ[σ₂'] F
h✝ : Nontrivial F'
⊢ ‖f.comp g.toLinearIsometry.toContinuousLinearMap‖ =
    ‖f.comp g.toLinearIsometry.toContinuousLinearMap‖ * ‖g.symm.toLinearIsometry.toContinuousLinearMap‖

Proof state:
𝕜₂ : Type u_2
𝕜₃ : Type u_3
F : Type u_5
G : Type u_7
inst✝¹⁶ : NormedAddCommGroup F
inst✝¹⁵ : NormedAddCommGroup G
inst✝¹⁴ : NontriviallyNormedField 𝕜₂
inst✝¹³ : NontriviallyNormedField 𝕜₃
inst✝¹² : NormedSpace 𝕜₂ F
inst✝¹¹ : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
𝕜₂' : Type u_8
inst✝¹⁰ : NontriviallyNormedField 𝕜₂'
F' : Type u_9
inst✝⁹ : NormedAddCommGroup F'
inst✝⁸ : NormedSpace 𝕜₂' F'
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂'' : 𝕜₂ →+* 𝕜₂'
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst✝⁷ : RingHomInvPair σ₂' σ₂''
inst✝⁶ : RingHomInvPair σ₂'' σ₂'
inst✝⁵ : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst✝⁴ : RingHomCompTriple σ₂'' σ₂₃' σ₂₃
inst✝³ : RingHomIsometric σ₂₃
inst✝² : RingHomIsometric σ₂'
inst✝¹ : RingHomIsometric σ₂''
inst✝ : RingHomIsometric σ₂₃'
f : F →SL[σ₂₃] G
g : F' ≃ₛₗᵢ[σ₂'] F
⊢ ‖f.comp g.toLinearIsometry.toContinuousLinearMap‖ = ‖f‖

Tactic:
cases subsingleton_or_nontrivial F'

Result:
case inl
𝕜₂ : Type u_2
𝕜₃ : Type u_3
F : Type u_5
G : Type u_7
inst✝¹⁶ : NormedAddCommGroup F
inst✝¹⁵ : NormedAddCommGroup G
inst✝¹⁴ : NontriviallyNormedField 𝕜₂
inst✝¹³ : NontriviallyNormedField 𝕜₃
inst✝¹² : NormedSpace 𝕜₂ F
inst✝¹¹ : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
𝕜₂' : Type u_8
inst✝¹⁰ : NontriviallyNormedField 𝕜₂'
F' : Type u_9
inst✝⁹ : NormedAddCommGroup F'
inst✝⁸ : NormedSpace 𝕜₂' F'
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂'' : 𝕜₂ →+* 𝕜₂'
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst✝⁷ : RingHomInvPair σ₂' σ₂''
inst✝⁶ : RingHomInvPair σ₂'' σ₂'
inst✝⁵ : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst✝⁴ : RingHomCompTriple σ₂'' σ₂₃' σ₂₃
inst✝³ : RingHomIsometric σ₂₃
inst✝² : RingHomIsometric σ₂'
inst✝¹ : RingHomIsometric σ₂''
inst✝ : RingHomIsometric σ₂₃'
f : F →SL[σ₂₃] G
g : F' ≃ₛₗᵢ[σ₂'] F
h✝ : Subsingleton F'
⊢ ‖f.comp g.toLinearIsometry.toContinuousLinearMap‖ = ‖f‖

case inr
𝕜₂ : Type u_2
𝕜₃ : Type u_3
F : Type u_5
G : Type u_7
inst✝¹⁶ : NormedAddCommGroup F
inst✝¹⁵ : NormedAddCommGroup G
inst✝¹⁴ : NontriviallyNormedField 𝕜₂
inst✝¹³ : NontriviallyNormedField 𝕜₃
inst✝¹² : NormedSpace 𝕜₂ F
inst✝¹¹ : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
𝕜₂' : Type u_8
inst✝¹⁰ : NontriviallyNormedField 𝕜₂'
F' : Type u_9
inst✝⁹ : NormedAddCommGroup F'
inst✝⁸ : NormedSpace 𝕜₂' F'
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂'' : 𝕜₂ →+* 𝕜₂'
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst✝⁷ : RingHomInvPair σ₂' σ₂''
inst✝⁶ : RingHomInvPair σ₂'' σ₂'
inst✝⁵ : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst✝⁴ : RingHomCompTriple σ₂'' σ₂₃' σ₂₃
inst✝³ : RingHomIsometric σ₂₃
inst✝² : RingHomIsometric σ₂'
inst✝¹ : RingHomIsometric σ₂''
inst✝ : RingHomIsometric σ₂₃'
f : F →SL[σ₂₃] G
g : F' ≃ₛₗᵢ[σ₂'] F
h✝ : Nontrivial F'
⊢ ‖f.comp g.toLinearIsometry.toContinuousLinearMap‖ = ‖f‖

Proof state:
case h.e'_3.h.e'_3.h
𝕜₂ : Type u_2
𝕜₃ : Type u_3
F : Type u_5
G : Type u_7
inst✝¹⁶ : NormedAddCommGroup F
inst✝¹⁵ : NormedAddCommGroup G
inst✝¹⁴ : NontriviallyNormedField 𝕜₂
inst✝¹³ : NontriviallyNormedField 𝕜₃
inst✝¹² : NormedSpace 𝕜₂ F
inst✝¹¹ : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
𝕜₂' : Type u_8
inst✝¹⁰ : NontriviallyNormedField 𝕜₂'
F' : Type u_9
inst✝⁹ : NormedAddCommGroup F'
inst✝⁸ : NormedSpace 𝕜₂' F'
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂'' : 𝕜₂ →+* 𝕜₂'
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst✝⁷ : RingHomInvPair σ₂' σ₂''
inst✝⁶ : RingHomInvPair σ₂'' σ₂'
inst✝⁵ : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst✝⁴ : RingHomCompTriple σ₂'' σ₂₃' σ₂₃
inst✝³ : RingHomIsometric σ₂₃
inst✝² : RingHomIsometric σ₂'
inst✝¹ : RingHomIsometric σ₂''
inst✝ : RingHomIsometric σ₂₃'
f : F →SL[σ₂₃] G
g : F' ≃ₛₗᵢ[σ₂'] F
h✝ : Nontrivial F'
x✝ : F
⊢ f x✝ = ((f.comp g.toLinearIsometry.toContinuousLinearMap).comp g.symm.toLinearIsometry.toContinuousLinearMap) x✝

Tactic:
simp

Result:
no goals