awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜₂ : Type u_2
𝕜₃ : Type u_3
F : Type u_5
G : Type u_7
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NontriviallyNormedField 𝕜₃
inst_4 : NormedSpace 𝕜₂ F
inst_5 : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
𝕜₂' : Type u_8
inst_6 : NontriviallyNormedField 𝕜₂'
F' : Type u_9
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜₂' F'
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂'' : 𝕜₂ →+* 𝕜₂'
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst_9 : RingHomInvPair σ₂' σ₂''
inst_10 : RingHomInvPair σ₂'' σ₂'
inst_11 : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst_12 : RingHomCompTriple σ₂'' σ₂₃' σ₂₃
inst_13 : RingHomIsometric σ₂₃
inst_14 : RingHomIsometric σ₂'
inst_15 : RingHomIsometric σ₂''
inst_16 : RingHomIsometric σ₂₃'
f : F →SL[σ₂₃] G
g : F' ≃ₛₗᵢ[σ₂'] F
h : Subsingleton F'
⊢ Subsingleton F

Tactic:
haveI := g.symm.toLinearEquiv.toEquiv.subsingleton
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜₂ : Type u_2
𝕜₃ : Type u_3
F : Type u_5
G : Type u_7
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NontriviallyNormedField 𝕜₃
inst_4 : NormedSpace 𝕜₂ F
inst_5 : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
𝕜₂' : Type u_8
inst_6 : NontriviallyNormedField 𝕜₂'
F' : Type u_9
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜₂' F'
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂'' : 𝕜₂ →+* 𝕜₂'
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst_9 : RingHomInvPair σ₂' σ₂''
inst_10 : RingHomInvPair σ₂'' σ₂'
inst_11 : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst_12 : RingHomCompTriple σ₂'' σ₂₃' σ₂₃
inst_13 : RingHomIsometric σ₂₃
inst_14 : RingHomIsometric σ₂'
inst_15 : RingHomIsometric σ₂''
inst_16 : RingHomIsometric σ₂₃'
f : F →SL[σ₂₃] G
g : F' ≃ₛₗᵢ[σ₂'] F
h : Subsingleton F'
this : Subsingleton F
⊢ ‖f ∘SL g.toLinearIsometry.toContinuousLinearMap‖ = ‖f‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜₂ : Type u_2
𝕜₃ : Type u_3
F : Type u_5
G : Type u_7
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NontriviallyNormedField 𝕜₃
inst_4 : NormedSpace 𝕜₂ F
inst_5 : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
𝕜₂' : Type u_8
inst_6 : NontriviallyNormedField 𝕜₂'
F' : Type u_9
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜₂' F'
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂'' : 𝕜₂ →+* 𝕜₂'
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst_9 : RingHomInvPair σ₂' σ₂''
inst_10 : RingHomInvPair σ₂'' σ₂'
inst_11 : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst_12 : RingHomCompTriple σ₂'' σ₂₃' σ₂₃
inst_13 : RingHomIsometric σ₂₃
inst_14 : RingHomIsometric σ₂'
inst_15 : RingHomIsometric σ₂''
inst_16 : RingHomIsometric σ₂₃'
f : F →SL[σ₂₃] G
g : F' ≃ₛₗᵢ[σ₂'] F
h : Nontrivial F'
⊢ ‖f ∘SL g.toLinearIsometry.toContinuousLinearMap‖ = ‖f‖

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜₂ : Type u_2
𝕜₃ : Type u_3
F : Type u_5
G : Type u_7
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NontriviallyNormedField 𝕜₃
inst_4 : NormedSpace 𝕜₂ F
inst_5 : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
𝕜₂' : Type u_8
inst_6 : NontriviallyNormedField 𝕜₂'
F' : Type u_9
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜₂' F'
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂'' : 𝕜₂ →+* 𝕜₂'
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst_9 : RingHomInvPair σ₂' σ₂''
inst_10 : RingHomInvPair σ₂'' σ₂'
inst_11 : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst_12 : RingHomCompTriple σ₂'' σ₂₃' σ₂₃
inst_13 : RingHomIsometric σ₂₃
inst_14 : RingHomIsometric σ₂'
inst_15 : RingHomIsometric σ₂''
inst_16 : RingHomIsometric σ₂₃'
f : F →SL[σ₂₃] G
g : F' ≃ₛₗᵢ[σ₂'] F
h : Nontrivial F'
inr : ‖f ∘SL g.toLinearIsometry.toContinuousLinearMap‖ ≤ ‖f‖
inr₁ : ‖f‖ ≤ ‖f ∘SL g.toLinearIsometry.toContinuousLinearMap‖
⊢ ‖f ∘SL g.toLinearIsometry.toContinuousLinearMap‖ = ‖f‖

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜₂ : Type u_2
𝕜₃ : Type u_3
F : Type u_5
G : Type u_7
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NontriviallyNormedField 𝕜₃
inst_4 : NormedSpace 𝕜₂ F
inst_5 : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
𝕜₂' : Type u_8
inst_6 : NontriviallyNormedField 𝕜₂'
F' : Type u_9
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜₂' F'
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂'' : 𝕜₂ →+* 𝕜₂'
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst_9 : RingHomInvPair σ₂' σ₂''
inst_10 : RingHomInvPair σ₂'' σ₂'
inst_11 : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst_12 : RingHomCompTriple σ₂'' σ₂₃' σ₂₃
inst_13 : RingHomIsometric σ₂₃
inst_14 : RingHomIsometric σ₂'
inst_15 : RingHomIsometric σ₂''
inst_16 : RingHomIsometric σ₂₃'
f : F →SL[σ₂₃] G
g : F' ≃ₛₗᵢ[σ₂'] F
h : Nontrivial F'
⊢ ‖f ∘SL g.toLinearIsometry.toContinuousLinearMap‖ ≤ ‖f‖ * ‖g.toLinearIsometry.toContinuousLinearMap‖

Tactic:
f.opNorm_comp_le g.toLinearIsometry.toContinuousLinearMap

Premises used: LinearIsometryEquiv.toLinearIsometry, ContinuousLinearMap.opNorm_comp_le, LinearIsometry.toContinuousLinearMap
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜₂ : Type u_2
𝕜₃ : Type u_3
F : Type u_5
G : Type u_7
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NontriviallyNormedField 𝕜₃
inst_4 : NormedSpace 𝕜₂ F
inst_5 : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
𝕜₂' : Type u_8
inst_6 : NontriviallyNormedField 𝕜₂'
F' : Type u_9
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜₂' F'
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂'' : 𝕜₂ →+* 𝕜₂'
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst_9 : RingHomInvPair σ₂' σ₂''
inst_10 : RingHomInvPair σ₂'' σ₂'
inst_11 : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst_12 : RingHomCompTriple σ₂'' σ₂₃' σ₂₃
inst_13 : RingHomIsometric σ₂₃
inst_14 : RingHomIsometric σ₂'
inst_15 : RingHomIsometric σ₂''
inst_16 : RingHomIsometric σ₂₃'
f : F →SL[σ₂₃] G
g : F' ≃ₛₗᵢ[σ₂'] F
h_1 : Nontrivial F'
h : ‖f‖ = ‖f‖ * ‖g.toLinearIsometry.toContinuousLinearMap‖
⊢ ‖f ∘SL g.toLinearIsometry.toContinuousLinearMap‖ ≤ ‖f‖

Tactic:
convert! f.opNorm_comp_le g.toLinearIsometry.toContinuousLinearMap

Premises used: LinearIsometryEquiv.toLinearIsometry, ContinuousLinearMap.opNorm_comp_le, LinearIsometry.toContinuousLinearMap
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜₂ : Type u_2
𝕜₃ : Type u_3
F : Type u_5
G : Type u_7
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NontriviallyNormedField 𝕜₃
inst_4 : NormedSpace 𝕜₂ F
inst_5 : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
𝕜₂' : Type u_8
inst_6 : NontriviallyNormedField 𝕜₂'
F' : Type u_9
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜₂' F'
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂'' : 𝕜₂ →+* 𝕜₂'
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst_9 : RingHomInvPair σ₂' σ₂''
inst_10 : RingHomInvPair σ₂'' σ₂'
inst_11 : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst_12 : RingHomCompTriple σ₂'' σ₂₃' σ₂₃
inst_13 : RingHomIsometric σ₂₃
inst_14 : RingHomIsometric σ₂'
inst_15 : RingHomIsometric σ₂''
inst_16 : RingHomIsometric σ₂₃'
f : F →SL[σ₂₃] G
g : F' ≃ₛₗᵢ[σ₂'] F
h : Nontrivial F'
⊢ ‖f‖ = ‖f‖ * ‖g.toLinearIsometry.toContinuousLinearMap‖

Tactic:
simp [g.toLinearIsometry.norm_toContinuousLinearMap]

Premises used: LinearIsometryEquiv.toLinearIsometry, LinearIsometry.norm_toContinuousLinearMap
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜₂ : Type u_2
𝕜₃ : Type u_3
F : Type u_5
G : Type u_7
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NontriviallyNormedField 𝕜₃
inst_4 : NormedSpace 𝕜₂ F
inst_5 : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
𝕜₂' : Type u_8
inst_6 : NontriviallyNormedField 𝕜₂'
F' : Type u_9
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜₂' F'
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂'' : 𝕜₂ →+* 𝕜₂'
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst_9 : RingHomInvPair σ₂' σ₂''
inst_10 : RingHomInvPair σ₂'' σ₂'
inst_11 : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst_12 : RingHomCompTriple σ₂'' σ₂₃' σ₂₃
inst_13 : RingHomIsometric σ₂₃
inst_14 : RingHomIsometric σ₂'
inst_15 : RingHomIsometric σ₂''
inst_16 : RingHomIsometric σ₂₃'
f : F →SL[σ₂₃] G
g : F' ≃ₛₗᵢ[σ₂'] F
h : Nontrivial F'
⊢ ‖(f ∘SL g.toLinearIsometry.toContinuousLinearMap) ∘SL g.symm.toLinearIsometry.toContinuousLinearMap‖ ≤
    ‖f ∘SL g.toLinearIsometry.toContinuousLinearMap‖ * ‖g.symm.toLinearIsometry.toContinuousLinearMap‖

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

Premises used: ContinuousLinearMap.comp, LinearIsometryEquiv.toLinearIsometry, LinearIsometryEquiv.symm, ContinuousLinearMap.opNorm_comp_le, LinearIsometry.toContinuousLinearMap
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜₂ : Type u_2
𝕜₃ : Type u_3
F : Type u_5
G : Type u_7
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NontriviallyNormedField 𝕜₃
inst_4 : NormedSpace 𝕜₂ F
inst_5 : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
𝕜₂' : Type u_8
inst_6 : NontriviallyNormedField 𝕜₂'
F' : Type u_9
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜₂' F'
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂'' : 𝕜₂ →+* 𝕜₂'
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst_9 : RingHomInvPair σ₂' σ₂''
inst_10 : RingHomInvPair σ₂'' σ₂'
inst_11 : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst_12 : RingHomCompTriple σ₂'' σ₂₃' σ₂₃
inst_13 : RingHomIsometric σ₂₃
inst_14 : RingHomIsometric σ₂'
inst_15 : RingHomIsometric σ₂''
inst_16 : RingHomIsometric σ₂₃'
f : F →SL[σ₂₃] G
g : F' ≃ₛₗᵢ[σ₂'] F
h_1 : Nontrivial F'
h : f = (f ∘SL g.toLinearIsometry.toContinuousLinearMap) ∘SL g.symm.toLinearIsometry.toContinuousLinearMap
h₁ :
  ‖f ∘SL g.toLinearIsometry.toContinuousLinearMap‖ =
    ‖f ∘SL g.toLinearIsometry.toContinuousLinearMap‖ * ‖g.symm.toLinearIsometry.toContinuousLinearMap‖
⊢ ‖f‖ ≤ ‖f ∘SL g.toLinearIsometry.toContinuousLinearMap‖

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

Premises used: ContinuousLinearMap.comp, LinearIsometryEquiv.toLinearIsometry, LinearIsometryEquiv.symm, ContinuousLinearMap.opNorm_comp_le, LinearIsometry.toContinuousLinearMap
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜₂ : Type u_2
𝕜₃ : Type u_3
F : Type u_5
G : Type u_7
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NontriviallyNormedField 𝕜₃
inst_4 : NormedSpace 𝕜₂ F
inst_5 : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
𝕜₂' : Type u_8
inst_6 : NontriviallyNormedField 𝕜₂'
F' : Type u_9
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜₂' F'
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂'' : 𝕜₂ →+* 𝕜₂'
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst_9 : RingHomInvPair σ₂' σ₂''
inst_10 : RingHomInvPair σ₂'' σ₂'
inst_11 : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst_12 : RingHomCompTriple σ₂'' σ₂₃' σ₂₃
inst_13 : RingHomIsometric σ₂₃
inst_14 : RingHomIsometric σ₂'
inst_15 : RingHomIsometric σ₂''
inst_16 : RingHomIsometric σ₂₃'
f : F →SL[σ₂₃] G
g : F' ≃ₛₗᵢ[σ₂'] F
h_1 : Nontrivial F'
h :
  ∀ (x : F),
    Eq.{u_7 + 1} (α := G) ((f : (a : F) → G) x : G)
      (((f ∘SL g.toLinearIsometry.toContinuousLinearMap) ∘SL g.symm.toLinearIsometry.toContinuousLinearMap :
            (a : F) → G)
          x :
        G)
⊢ f = (f ∘SL g.toLinearIsometry.toContinuousLinearMap) ∘SL g.symm.toLinearIsometry.toContinuousLinearMap

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜₂ : Type u_2
𝕜₃ : Type u_3
F : Type u_5
G : Type u_7
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NontriviallyNormedField 𝕜₃
inst_4 : NormedSpace 𝕜₂ F
inst_5 : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
𝕜₂' : Type u_8
inst_6 : NontriviallyNormedField 𝕜₂'
F' : Type u_9
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜₂' F'
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂'' : 𝕜₂ →+* 𝕜₂'
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst_9 : RingHomInvPair σ₂' σ₂''
inst_10 : RingHomInvPair σ₂'' σ₂'
inst_11 : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst_12 : RingHomCompTriple σ₂'' σ₂₃' σ₂₃
inst_13 : RingHomIsometric σ₂₃
inst_14 : RingHomIsometric σ₂'
inst_15 : RingHomIsometric σ₂''
inst_16 : RingHomIsometric σ₂₃'
f : F →SL[σ₂₃] G
g : F' ≃ₛₗᵢ[σ₂'] F
h : Nontrivial F'
x : F
⊢ Eq.{u_7 + 1} (α := G) ((f : (a : F) → G) x : G)
    (((f ∘SL g.toLinearIsometry.toContinuousLinearMap) ∘SL g.symm.toLinearIsometry.toContinuousLinearMap : (a : F) → G)
        x :
      G)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜₂ : Type u_2
𝕜₃ : Type u_3
F : Type u_5
G : Type u_7
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NontriviallyNormedField 𝕜₃
inst_4 : NormedSpace 𝕜₂ F
inst_5 : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
𝕜₂' : Type u_8
inst_6 : NontriviallyNormedField 𝕜₂'
F' : Type u_9
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜₂' F'
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂'' : 𝕜₂ →+* 𝕜₂'
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst_9 : RingHomInvPair σ₂' σ₂''
inst_10 : RingHomInvPair σ₂'' σ₂'
inst_11 : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst_12 : RingHomCompTriple σ₂'' σ₂₃' σ₂₃
inst_13 : RingHomIsometric σ₂₃
inst_14 : RingHomIsometric σ₂'
inst_15 : RingHomIsometric σ₂''
inst_16 : RingHomIsometric σ₂₃'
f : F →SL[σ₂₃] G
g : F' ≃ₛₗᵢ[σ₂'] F
h : Nontrivial F'
⊢ Nontrivial F

Tactic:
haveI := g.symm.surjective.nontrivial
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜₂ : Type u_2
𝕜₃ : Type u_3
F : Type u_5
G : Type u_7
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NontriviallyNormedField 𝕜₃
inst_4 : NormedSpace 𝕜₂ F
inst_5 : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
𝕜₂' : Type u_8
inst_6 : NontriviallyNormedField 𝕜₂'
F' : Type u_9
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜₂' F'
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂'' : 𝕜₂ →+* 𝕜₂'
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst_9 : RingHomInvPair σ₂' σ₂''
inst_10 : RingHomInvPair σ₂'' σ₂'
inst_11 : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst_12 : RingHomCompTriple σ₂'' σ₂₃' σ₂₃
inst_13 : RingHomIsometric σ₂₃
inst_14 : RingHomIsometric σ₂'
inst_15 : RingHomIsometric σ₂''
inst_16 : RingHomIsometric σ₂₃'
f : F →SL[σ₂₃] G
g : F' ≃ₛₗᵢ[σ₂'] F
h : Nontrivial F'
this : Nontrivial F
⊢ ‖f ∘SL g.toLinearIsometry.toContinuousLinearMap‖ =
    ‖f ∘SL g.toLinearIsometry.toContinuousLinearMap‖ * ‖g.symm.toLinearIsometry.toContinuousLinearMap‖

Tactic:
simp [g.symm.toLinearIsometry.norm_toContinuousLinearMap]

Premises used: LinearIsometryEquiv.toLinearIsometry, LinearIsometryEquiv.symm, LinearIsometry.norm_toContinuousLinearMap
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup Fₗ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 Fₗ
c : StrongDual 𝕜 E
inst_5 : Nontrivial Fₗ
⊢ norm (E := Fₗ →L[𝕜] E →L[𝕜] Fₗ)
      ((smulRightL 𝕜 E Fₗ : (a : StrongDual 𝕜 E) → Fₗ →L[𝕜] E →L[𝕜] Fₗ) c : Fₗ →L[𝕜] E →L[𝕜] Fₗ) =
    ‖c‖

Tactic:
ContinuousLinearMap.homothety_norm _ c.norm_smulRight_apply

Premises used: ContinuousLinearMap.norm_smulRight_apply, ContinuousLinearMap.homothety_norm
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
⊢ LE.le (α := ℕ) sorry 1

Tactic:
LinearMap.mkContinuous₂_norm_le _ zero_le_one _

Premises used: zero_le_one, LinearMap.mkContinuous₂_norm_le
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : Nontrivial.{u_4} ↥K
⊢ norm (E := ↥K →L[𝕜] E) K.subtypeL = 1

Tactic:
K.subtypeₗᵢ.norm_toContinuousLinearMap

Premises used: Submodule.subtypeL, Set.Mem, LinearIsometry.norm_toContinuousLinearMap, Submodule.subtype, Submodule.subtypeₗᵢ, LinearIsometry.toContinuousLinearMap
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
inst_8 : RingHomIsometric σ₂₁
e : E ≃SL[σ₁₂] F
⊢ AntilipschitzWith.{u_4, u_5} (α := E) (β := F) ‖(↑e.symm : F →SL[σ₂₁] E)‖₊ (⇑e : (a : E) → F)

Tactic:
e.symm.lipschitz.to_rightInverse e.left_inv

Premises used: ContinuousLinearEquiv.symm, ContinuousLinearEquiv.toLinearEquiv, LinearEquiv.left_inv, ContinuousLinearEquiv.lipschitz, LipschitzWith.to_rightInverse
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
inst_8 : RingHomIsometric σ₂₁
inst_9 : RingHomIsometric σ₁₂
inst_10 : Nontrivial E
e : E ≃SL[σ₁₂] F
rw : 1 ≤ ‖(↑e.symm : F →SL[σ₂₁] E)‖ * ‖(↑e : E →SL[σ₁₂] F)‖
⊢ 1 ≤ ‖(↑e : E →SL[σ₁₂] F)‖ * ‖(↑e.symm : F →SL[σ₂₁] E)‖

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
inst_8 : RingHomIsometric σ₂₁
inst_9 : RingHomIsometric σ₁₂
inst_10 : Nontrivial E
e : E ≃SL[σ₁₂] F
⊢ ‖(↑e.symm : F →SL[σ₂₁] E) ∘SL (↑e : E →SL[σ₁₂] F)‖ ≤ ‖(↑e.symm : F →SL[σ₂₁] E)‖ * ‖(↑e : E →SL[σ₁₂] F)‖

Tactic:
(e.symm : F →SL[σ₂₁] E).opNorm_comp_le (e : E →SL[σ₁₂] F)

Premises used: ContinuousLinearEquiv.symm, ContinuousLinearMap.opNorm_comp_le, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
inst_8 : RingHomIsometric σ₂₁
inst_9 : RingHomIsometric σ₁₂
inst_10 : Nontrivial E
e : E ≃SL[σ₁₂] F
h : 1 = ‖(↑e.symm : F →SL[σ₂₁] E) ∘SL (↑e : E →SL[σ₁₂] F)‖
⊢ 1 ≤ ‖(↑e.symm : F →SL[σ₂₁] E)‖ * ‖(↑e : E →SL[σ₁₂] F)‖

Tactic:
convert! (e.symm : F →SL[σ₂₁] E).opNorm_comp_le (e : E →SL[σ₁₂] F)

Premises used: ContinuousLinearEquiv.symm, ContinuousLinearMap.opNorm_comp_le, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
inst_8 : RingHomIsometric σ₂₁
inst_9 : RingHomIsometric σ₁₂
inst_10 : Nontrivial E
e : E ≃SL[σ₁₂] F
h : 1 = norm (E := E →L[𝕜] E) (ContinuousLinearMap.id 𝕜 E)
h₁ h₂ : Eq (α := ℝ) 1 1
⊢ 1 = ‖(↑e.symm : F →SL[σ₂₁] E) ∘SL (↑e : E →SL[σ₁₂] F)‖

Tactic:
rw [e.coe_symm_comp_coe, ContinuousLinearMap.norm_id]

Premises used: ContinuousLinearEquiv.coe_symm_comp_coe, ContinuousLinearMap.norm_id
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
inst_8 : RingHomIsometric σ₂₁
inst_9 : RingHomIsometric σ₁₂
inst_10 : Nontrivial E
e : E ≃SL[σ₁₂] F
⊢ 0 < ‖(↑e : E →SL[σ₁₂] F)‖

Tactic:
pos_of_mul_pos_left (lt_of_lt_of_le zero_lt_one e.one_le_norm_mul_norm_symm) (norm_nonneg _)

Premises used: pos_of_mul_pos_left, ContinuousLinearEquiv.one_le_norm_mul_norm_symm, zero_lt_one, norm_nonneg, lt_of_lt_of_le
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
inst_8 : RingHomIsometric σ₂₁
inst_9 : RingHomIsometric σ₁₂
inst_10 : Nontrivial E
e : E ≃SL[σ₁₂] F
⊢ 0 < ‖(↑e.symm : F →SL[σ₂₁] E)‖

Tactic:
pos_of_mul_pos_right (zero_lt_one.trans_le e.one_le_norm_mul_norm_symm) (norm_nonneg _)

Premises used: ContinuousLinearEquiv.one_le_norm_mul_norm_symm, zero_lt_one, LT.lt.trans_le, norm_nonneg, pos_of_mul_pos_right
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
inst_8 : RingHomIsometric σ₂₁
inst_9 : RingHomIsometric σ₁₂
inst_10 : Nontrivial E
e : E ≃SL[σ₁₂] F
⊢ 0 < ‖(↑e.symm : F →SL[σ₂₁] E)‖₊

Tactic:
e.norm_symm_pos

Premises used: ContinuousLinearEquiv.norm_symm_pos
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
inst_8 : RingHomIsometric σ₂₁
inst_9 : RingHomIsometric σ₁₂
e : E ≃SL[σ₁₂] F
inl : ∀ (_i : Subsingleton E), Subsingleton E ∨ 0 < ‖(↑e.symm : F →SL[σ₂₁] E)‖
inr : ∀ (_i : Nontrivial E), Subsingleton E ∨ 0 < ‖(↑e.symm : F →SL[σ₂₁] E)‖
⊢ Subsingleton E ∨ 0 < ‖(↑e.symm : F →SL[σ₂₁] E)‖

Tactic:
rcases subsingleton_or_nontrivial E with (_i | _i)

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
inst_8 : RingHomIsometric σ₂₁
inst_9 : RingHomIsometric σ₁₂
e : E ≃SL[σ₁₂] F
_i inl : Subsingleton E
⊢ Subsingleton E ∨ 0 < ‖(↑e.symm : F →SL[σ₂₁] E)‖

Tactic:
left
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
inst_8 : RingHomIsometric σ₂₁
inst_9 : RingHomIsometric σ₁₂
e : E ≃SL[σ₁₂] F
_i : Subsingleton E
⊢ Subsingleton E

Tactic:
infer_instance
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
inst_8 : RingHomIsometric σ₂₁
inst_9 : RingHomIsometric σ₁₂
e : E ≃SL[σ₁₂] F
_i : Nontrivial E
inr : 0 < ‖(↑e.symm : F →SL[σ₂₁] E)‖
⊢ Subsingleton E ∨ 0 < ‖(↑e.symm : F →SL[σ₂₁] E)‖

Tactic:
right
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
inst_8 : RingHomIsometric σ₂₁
inst_9 : RingHomIsometric σ₁₂
e : E ≃SL[σ₁₂] F
_i : Nontrivial E
⊢ 0 < ‖(↑e.symm : F →SL[σ₂₁] E)‖

Tactic:
e.norm_symm_pos

Premises used: ContinuousLinearEquiv.norm_symm_pos