awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
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
⊢ ‖f ∘SL g.toLinearIsometry.toContinuousLinearMap‖ = ‖f‖
have inl : Subsingleton F' → ‖f ∘SL g.toLinearIsometry.toContinuousLinearMap‖ = ‖f‖
Tactic: cases subsingleton_or_nontrivial F'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
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
inl : Subsingleton F' → ‖f ∘SL g.toLinearIsometry.toContinuousLinearMap‖ = ‖f‖
⊢ ‖f ∘SL g.toLinearIsometry.toContinuousLinearMap‖ = ‖f‖
have inr : Nontrivial F' → ‖f ∘SL g.toLinearIsometry.toContinuousLinearMap‖ = ‖f‖
Tactic: cases subsingleton_or_nontrivial F'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (hypothesis)
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'
⊢ ‖f ∘SL g.toLinearIsometry.toContinuousLinearMap‖ = ‖f‖
have this : Subsingleton F
Tactic: haveI := g.symm.toLinearEquiv.toEquiv.subsingleton
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
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‖
have inr : ‖f ∘SL g.toLinearIsometry.toContinuousLinearMap‖ ≤ ‖f‖
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
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‖
⊢ ‖f ∘SL g.toLinearIsometry.toContinuousLinearMap‖ = ‖f‖
have inr₁ : ‖f‖ ≤ ‖f ∘SL g.toLinearIsometry.toContinuousLinearMap‖
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
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‖
have h : ‖f‖ = ‖f‖ * ‖g.toLinearIsometry.toContinuousLinearMap‖
Tactic: convert! f.opNorm_comp_le g.toLinearIsometry.toContinuousLinearMap
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
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 ∘SL g.toLinearIsometry.toContinuousLinearMap‖
have h : f = (f ∘SL g.toLinearIsometry.toContinuousLinearMap) ∘SL g.symm.toLinearIsometry.toContinuousLinearMap
Tactic: convert!
    (f.comp g.toLinearIsometry.toContinuousLinearMap).opNorm_comp_le
      g.symm.toLinearIsometry.toContinuousLinearMap
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
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
⊢ ‖f‖ ≤ ‖f ∘SL g.toLinearIsometry.toContinuousLinearMap‖
have h₁ : ‖f ∘SL g.toLinearIsometry.toContinuousLinearMap‖ =
  ‖f ∘SL g.toLinearIsometry.toContinuousLinearMap‖ * ‖g.symm.toLinearIsometry.toContinuousLinearMap‖
Tactic: convert!
    (f.comp g.toLinearIsometry.toContinuousLinearMap).opNorm_comp_le
      g.symm.toLinearIsometry.toContinuousLinearMap
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
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 ∘SL g.toLinearIsometry.toContinuousLinearMap) ∘SL g.symm.toLinearIsometry.toContinuousLinearMap
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (hypothesis)
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 ∘SL g.toLinearIsometry.toContinuousLinearMap‖ * ‖g.symm.toLinearIsometry.toContinuousLinearMap‖
have this : Nontrivial F
Tactic: haveI := g.symm.surjective.nontrivial
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
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
⊢ 1 ≤ ‖(↑e : E →SL[σ₁₂] F)‖ * ‖(↑e.symm : F →SL[σ₂₁] E)‖
have rw : 1 ≤ ‖(↑e.symm : F →SL[σ₂₁] E)‖ * ‖(↑e : E →SL[σ₁₂] F)‖
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
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
⊢ 1 ≤ ‖(↑e.symm : F →SL[σ₂₁] E)‖ * ‖(↑e : E →SL[σ₁₂] F)‖
have h : 1 = ‖(↑e.symm : F →SL[σ₂₁] E) ∘SL (↑e : E →SL[σ₁₂] F)‖
Tactic: convert! (e.symm : F →SL[σ₂₁] E).opNorm_comp_le (e : E →SL[σ₁₂] F)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
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
⊢ 1 = ‖(↑e.symm : F →SL[σ₂₁] E) ∘SL (↑e : E →SL[σ₁₂] F)‖
have h : 1 = norm (E := E →L[𝕜] E) (ContinuousLinearMap.id 𝕜 E)
Tactic: rw [e.coe_symm_comp_coe, ContinuousLinearMap.norm_id]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
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)
⊢ 1 = ‖(↑e.symm : F →SL[σ₂₁] E) ∘SL (↑e : E →SL[σ₁₂] F)‖
have h₁ : Eq (α := ℝ) 1 1
Tactic: rw [e.coe_symm_comp_coe, ContinuousLinearMap.norm_id]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
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
⊢ Subsingleton E ∨ 0 < ‖(↑e.symm : F →SL[σ₂₁] E)‖
have inl : ∀ (_i : Subsingleton E), Subsingleton E ∨ 0 < ‖(↑e.symm : F →SL[σ₂₁] E)‖
Tactic: rcases subsingleton_or_nontrivial E with (_i | _i)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
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)‖
⊢ Subsingleton E ∨ 0 < ‖(↑e.symm : F →SL[σ₂₁] E)‖
have inr : ∀ (_i : Nontrivial E), Subsingleton E ∨ 0 < ‖(↑e.symm : F →SL[σ₂₁] E)‖
Tactic: rcases subsingleton_or_nontrivial E with (_i | _i)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
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
⊢ Subsingleton E ∨ 0 < ‖(↑e.symm : F →SL[σ₂₁] E)‖
have inr : 0 < ‖(↑e.symm : F →SL[σ₂₁] E)‖
Tactic: right
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
x : E
h : x ≠ 0
⊢ norm (E := StrongDual.{u_1, u_4} 𝕜 ↥(𝕜 ∙ x)) (coord 𝕜 x h) = ‖x‖⁻¹
have hx : 0 < ‖x‖
Tactic: have hx : 0 < ‖x‖ := norm_pos_iff.mpr h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
x : E
h : x ≠ 0
hx : 0 < ‖x‖
⊢ norm (E := StrongDual.{u_1, u_4} 𝕜 ↥(𝕜 ∙ x)) (coord 𝕜 x h) = ‖x‖⁻¹
have this : Nontrivial.{u_4} ↥(𝕜 ∙ x)
Tactic: haveI : Nontrivial (𝕜 ∙ x) := Submodule.nontrivial_span_singleton h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (hypothesis)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
ι : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : SeminormedAddCommGroup E
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜₂ F
f : ι → E →SL[σ₁₂] F
⊢ [EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0,
      Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f),
      UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f),
      ∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖,
      ∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖,
      ∃ (C : ℝ), ∀ (i : ι), ‖f i‖ ≤ C, ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C, BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖),
      LT.lt (α := ENNReal) (⨆ (i : ι), (↑‖f i‖₊ : ENNReal)) ⊤].TFAE
have tfae_1_to_3 : ∀ (a : EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0),
  UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
Tactic: tfae_have 1 → 3 := uniformEquicontinuous_of_equicontinuousAt_zero f
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (hypothesis)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
ι : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : SeminormedAddCommGroup E
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜₂ F
f : ι → E →SL[σ₁₂] F
tfae_1_to_3 :
  ∀ (a : EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0),
    UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
⊢ [EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0,
      Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f),
      UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f),
      ∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖,
      ∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖,
      ∃ (C : ℝ), ∀ (i : ι), ‖f i‖ ≤ C, ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C, BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖),
      LT.lt (α := ENNReal) (⨆ (i : ι), (↑‖f i‖₊ : ENNReal)) ⊤].TFAE
have tfae_3_to_2 : ∀ (a : UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
  Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
Tactic: tfae_have 3 → 2 := UniformEquicontinuous.equicontinuous
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (hypothesis)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
ι : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : SeminormedAddCommGroup E
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜₂ F
f : ι → E →SL[σ₁₂] F
tfae_1_to_3 :
  ∀ (a : EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0),
    UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_3_to_2 :
  ∀ (a : UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
⊢ [EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0,
      Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f),
      UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f),
      ∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖,
      ∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖,
      ∃ (C : ℝ), ∀ (i : ι), ‖f i‖ ≤ C, ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C, BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖),
      LT.lt (α := ENNReal) (⨆ (i : ι), (↑‖f i‖₊ : ENNReal)) ⊤].TFAE
have tfae_2_to_1 : ∀ (a : Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
  EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0
Tactic: tfae_have 2 → 1 := fun H ↦ H 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
ι : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : SeminormedAddCommGroup E
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜₂ F
f : ι → E →SL[σ₁₂] F
tfae_1_to_3 :
  ∀ (a : EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0),
    UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_3_to_2 :
  ∀ (a : UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_2_to_1 :
  ∀ (a : Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0
⊢ (∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) ↔
    ∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖
have rw : Monotone (β := Prop) fun (C : ℝ) ↦ ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖
Tactic: rw [exists_ge_and_iff_exists]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
ι : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : SeminormedAddCommGroup E
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜₂ F
f : ι → E →SL[σ₁₂] F
tfae_1_to_3 :
  ∀ (a : EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0),
    UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_3_to_2 :
  ∀ (a : UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_2_to_1 :
  ∀ (a : Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0
C₁ C₂ : ℝ
hC : C₁ ≤ C₂
i : ι
x : E
⊢ C₁ * ‖x‖ ≤ C₂ * ‖x‖
have ha : 0 ≤ ‖x‖
Tactic: gcongr