awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Unitization (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : IsScalarTower 𝕜 A A
inst_4 : SMulCommClass 𝕜 A A
inst_5 : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
refine_1 :
  norm.{u_1} (E := 𝕜) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x).1 ≤
    2 *
      max ‖x.toProd.1‖
        ‖HAdd.hAdd (α := A →L[𝕜] A) (β := A →L[𝕜] A)
            ((algebraMap 𝕜 (A →L[𝕜] A) : (a : 𝕜) → A →L[𝕜] A) x.toProd.1 : A →L[𝕜] A)
            ((mul 𝕜 A : (a : A) → A →L[𝕜] A) x.toProd.2 : A →L[𝕜] A)‖
⊢ max (norm.{u_1} (E := 𝕜) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x).1)
      (norm.{u_2} (E := A) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x).2) ≤
    2 *
      max ‖x.toProd.1‖
        ‖HAdd.hAdd (α := A →L[𝕜] A) (β := A →L[𝕜] A)
            ((algebraMap 𝕜 (A →L[𝕜] A) : (a : 𝕜) → A →L[𝕜] A) x.toProd.1 : A →L[𝕜] A)
            ((mul 𝕜 A : (a : A) → A →L[𝕜] A) x.toProd.2 : A →L[𝕜] A)‖
have refine_2 : norm.{u_2} (E := A) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x).2 ≤
  2 *
    max ‖x.toProd.1‖
      ‖HAdd.hAdd (α := A →L[𝕜] A) (β := A →L[𝕜] A)
          ((algebraMap 𝕜 (A →L[𝕜] A) : (a : 𝕜) → A →L[𝕜] A) x.toProd.1 : A →L[𝕜] A)
          ((mul 𝕜 A : (a : A) → A →L[𝕜] A) x.toProd.2 : A →L[𝕜] A)‖
Tactic: refine max_le ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Unitization (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : IsScalarTower 𝕜 A A
inst_4 : SMulCommClass 𝕜 A A
inst_5 : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
⊢ norm.{u_1} (E := 𝕜) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x).1 ≤
    2 *
      max ‖x.toProd.1‖
        ‖HAdd.hAdd (α := A →L[𝕜] A) (β := A →L[𝕜] A)
            ((algebraMap 𝕜 (A →L[𝕜] A) : (a : 𝕜) → A →L[𝕜] A) x.toProd.1 : A →L[𝕜] A)
            ((mul 𝕜 A : (a : A) → A →L[𝕜] A) x.toProd.2 : A →L[𝕜] A)‖
have refine_1 : norm.{u_1} (E := 𝕜) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x).1 ≤
  max (2 * ‖x.toProd.1‖)
    (2 *
      ‖HAdd.hAdd (α := A →L[𝕜] A) (β := A →L[𝕜] A)
          ((algebraMap 𝕜 (A →L[𝕜] A) : (a : 𝕜) → A →L[𝕜] A) x.toProd.1 : A →L[𝕜] A)
          ((mul 𝕜 A : (a : A) → A →L[𝕜] A) x.toProd.2 : A →L[𝕜] A)‖)
Tactic: rw [mul_max_of_nonneg _ _ (zero_le_two : (0 : ℝ) ≤ 2)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Unitization (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : IsScalarTower 𝕜 A A
inst_4 : SMulCommClass 𝕜 A A
inst_5 : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
⊢ norm.{u_2} (E := A) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x).2 ≤
    2 *
      max ‖x.toProd.1‖
        ‖HAdd.hAdd (α := A →L[𝕜] A) (β := A →L[𝕜] A)
            ((algebraMap 𝕜 (A →L[𝕜] A) : (a : 𝕜) → A →L[𝕜] A) x.toProd.1 : A →L[𝕜] A)
            ((mul 𝕜 A : (a : A) → A →L[𝕜] A) x.toProd.2 : A →L[𝕜] A)‖
have a : Nontrivial A
Tactic: nontriviality A
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Unitization (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : IsScalarTower 𝕜 A A
inst_4 : SMulCommClass 𝕜 A A
inst_5 : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
h : Nontrivial A
⊢ norm.{u_2} (E := A) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x).2 ≤
    2 *
      max ‖x.toProd.1‖
        ‖HAdd.hAdd (α := A →L[𝕜] A) (β := A →L[𝕜] A)
            ((algebraMap 𝕜 (A →L[𝕜] A) : (a : 𝕜) → A →L[𝕜] A) x.toProd.1 : A →L[𝕜] A)
            ((mul 𝕜 A : (a : A) → A →L[𝕜] A) x.toProd.2 : A →L[𝕜] A)‖
have rw : norm.{u_2} (E := A) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x).2 ≤
  max ‖x.toProd.1‖
      ‖HAdd.hAdd (α := A →L[𝕜] A) (β := A →L[𝕜] A)
          ((algebraMap 𝕜 (A →L[𝕜] A) : (a : 𝕜) → A →L[𝕜] A) x.toProd.1 : A →L[𝕜] A)
          ((mul 𝕜 A : (a : A) → A →L[𝕜] A) x.toProd.2 : A →L[𝕜] A)‖ +
    max ‖x.toProd.1‖
      ‖HAdd.hAdd (α := A →L[𝕜] A) (β := A →L[𝕜] A)
          ((algebraMap 𝕜 (A →L[𝕜] A) : (a : 𝕜) → A →L[𝕜] A) x.toProd.1 : A →L[𝕜] A)
          ((mul 𝕜 A : (a : A) → A →L[𝕜] A) x.toProd.2 : A →L[𝕜] A)‖
Tactic: rw [two_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Unitization (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : IsScalarTower 𝕜 A A
inst_4 : SMulCommClass 𝕜 A A
inst_5 : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
h : Nontrivial A
⊢ norm.{u_2} (E := A) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x).2 ≤
    max ‖x.toProd.1‖
        ‖HAdd.hAdd (α := A →L[𝕜] A) (β := A →L[𝕜] A)
            ((algebraMap 𝕜 (A →L[𝕜] A) : (a : 𝕜) → A →L[𝕜] A) x.toProd.1 : A →L[𝕜] A)
            ((mul 𝕜 A : (a : A) → A →L[𝕜] A) x.toProd.2 : A →L[𝕜] A)‖ +
      max ‖x.toProd.1‖
        ‖HAdd.hAdd (α := A →L[𝕜] A) (β := A →L[𝕜] A)
            ((algebraMap 𝕜 (A →L[𝕜] A) : (a : 𝕜) → A →L[𝕜] A) x.toProd.1 : A →L[𝕜] A)
            ((mul 𝕜 A : (a : A) → A →L[𝕜] A) x.toProd.2 : A →L[𝕜] A)‖
have 𝕜₁ : norm (E := A →L[𝕜] A) ((mul 𝕜 A : (a : A) → A →L[𝕜] A) x.toProd.2 : A →L[𝕜] A) ≤
  ‖HAdd.hAdd (α := A →L[𝕜] A) (β := A →L[𝕜] A) ((algebraMap 𝕜 (A →L[𝕜] A) : (a : 𝕜) → A →L[𝕜] A) x.toProd.1 : A →L[𝕜] A)
        ((mul 𝕜 A : (a : A) → A →L[𝕜] A) x.toProd.2 : A →L[𝕜] A)‖ +
    ‖x.toProd.1‖
Tactic: calc
      ‖x.snd‖ = ‖mul 𝕜 A x.snd‖ :=
        .symm <| (isometry_mul 𝕜 A).norm_map_of_map_zero (map_zero _) _
      _ ≤ ‖algebraMap 𝕜 _ x.fst + mul 𝕜 A x.snd‖ + ‖x.fst‖ := by
        simpa only [add_comm _ (mul 𝕜 A x.snd), norm_algebraMap'] using
          norm_le_add_norm_add (mul 𝕜 A x.snd) (algebraMap 𝕜 _ x.fst)
      _ ≤ _ := add_le_add le_sup_right le_sup_left
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Unitization (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : IsScalarTower 𝕜 A A
inst_4 : SMulCommClass 𝕜 A A
inst_5 : RegularNormedAlgebra 𝕜 A
⊢ AntilipschitzWith (α := Unitization 𝕜 A) (β := 𝕜 × A) 2 (⇑(addEquiv 𝕜 A) : (a : Unitization 𝕜 A) → 𝕜 × A)
have refine : ∀ (x : Unitization 𝕜 A), ‖x‖ ≤ (↑2 : ℝ) * norm (E := 𝕜 × A) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x : 𝕜 × A)
Tactic: refine AddMonoidHomClass.antilipschitz_of_bound (addEquiv 𝕜 A) fun x => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Unitization (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : IsScalarTower 𝕜 A A
inst_4 : SMulCommClass 𝕜 A A
inst_5 : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
⊢ ‖x‖ ≤ (↑2 : ℝ) * norm (E := 𝕜 × A) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x : 𝕜 × A)
have rw : max ‖x.toProd.1‖
    ‖HAdd.hAdd (α := A →L[𝕜] A) (β := A →L[𝕜] A)
        ((algebraMap 𝕜 (A →L[𝕜] A) : (a : 𝕜) → A →L[𝕜] A) x.toProd.1 : A →L[𝕜] A)
        ((mul 𝕜 A : (a : A) → A →L[𝕜] A) x.toProd.2 : A →L[𝕜] A)‖ ≤
  2 *
    max (norm.{u_1} (E := 𝕜) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x).1)
      (norm.{u_2} (E := A) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x).2)
Tactic: rw [norm_eq_sup, Prod.norm_def, NNReal.coe_two]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Unitization (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : IsScalarTower 𝕜 A A
inst_4 : SMulCommClass 𝕜 A A
inst_5 : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
⊢ max ‖x.toProd.1‖
      ‖HAdd.hAdd (α := A →L[𝕜] A) (β := A →L[𝕜] A)
          ((algebraMap 𝕜 (A →L[𝕜] A) : (a : 𝕜) → A →L[𝕜] A) x.toProd.1 : A →L[𝕜] A)
          ((mul 𝕜 A : (a : A) → A →L[𝕜] A) x.toProd.2 : A →L[𝕜] A)‖ ≤
    2 *
      max (norm.{u_1} (E := 𝕜) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x).1)
        (norm.{u_2} (E := A) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x).2)
have refine_1 : ‖x.toProd.1‖ ≤
  2 *
    max (norm.{u_1} (E := 𝕜) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x).1)
      (norm.{u_2} (E := A) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x).2)
Tactic: refine max_le ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Unitization (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : IsScalarTower 𝕜 A A
inst_4 : SMulCommClass 𝕜 A A
inst_5 : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
refine_1 :
  ‖x.toProd.1‖ ≤
    2 *
      max (norm.{u_1} (E := 𝕜) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x).1)
        (norm.{u_2} (E := A) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x).2)
⊢ max ‖x.toProd.1‖
      ‖HAdd.hAdd (α := A →L[𝕜] A) (β := A →L[𝕜] A)
          ((algebraMap 𝕜 (A →L[𝕜] A) : (a : 𝕜) → A →L[𝕜] A) x.toProd.1 : A →L[𝕜] A)
          ((mul 𝕜 A : (a : A) → A →L[𝕜] A) x.toProd.2 : A →L[𝕜] A)‖ ≤
    2 *
      max (norm.{u_1} (E := 𝕜) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x).1)
        (norm.{u_2} (E := A) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x).2)
have refine_2 : ‖HAdd.hAdd (α := A →L[𝕜] A) (β := A →L[𝕜] A) ((algebraMap 𝕜 (A →L[𝕜] A) : (a : 𝕜) → A →L[𝕜] A) x.toProd.1 : A →L[𝕜] A)
      ((mul 𝕜 A : (a : A) → A →L[𝕜] A) x.toProd.2 : A →L[𝕜] A)‖ ≤
  2 *
    max (norm.{u_1} (E := 𝕜) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x).1)
      (norm.{u_2} (E := A) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x).2)
Tactic: refine max_le ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Unitization (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : IsScalarTower 𝕜 A A
inst_4 : SMulCommClass 𝕜 A A
inst_5 : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
⊢ ‖x.toProd.1‖ ≤
    2 *
      max (norm.{u_1} (E := 𝕜) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x).1)
        (norm.{u_2} (E := A) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x).2)
have refine_1 : ‖x.toProd.1‖ ≤
  max (2 * norm.{u_1} (E := 𝕜) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x).1)
    (2 * norm.{u_2} (E := A) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x).2)
Tactic: rw [mul_max_of_nonneg _ _ (zero_le_two : (0 : ℝ) ≤ 2)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Unitization (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : IsScalarTower 𝕜 A A
inst_4 : SMulCommClass 𝕜 A A
inst_5 : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
⊢ ‖HAdd.hAdd (α := A →L[𝕜] A) (β := A →L[𝕜] A) ((algebraMap 𝕜 (A →L[𝕜] A) : (a : 𝕜) → A →L[𝕜] A) x.toProd.1 : A →L[𝕜] A)
        ((mul 𝕜 A : (a : A) → A →L[𝕜] A) x.toProd.2 : A →L[𝕜] A)‖ ≤
    2 *
      max (norm.{u_1} (E := 𝕜) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x).1)
        (norm.{u_2} (E := A) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x).2)
have a : Nontrivial A
Tactic: nontriviality A
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Unitization (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : IsScalarTower 𝕜 A A
inst_4 : SMulCommClass 𝕜 A A
inst_5 : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
h : Nontrivial A
⊢ norm.{u_2} (E := A →L[𝕜] A) ((algebraMap 𝕜 (A →L[𝕜] A) : (a : 𝕜) → A →L[𝕜] A) x.toProd.1 : A →L[𝕜] A) +
      norm (E := A →L[𝕜] A) ((mul 𝕜 A : (a : A) → A →L[𝕜] A) x.toProd.2 : A →L[𝕜] A) =
    ‖x.toProd.1‖ + ‖x.toProd.2‖
have rw : ‖x.toProd.1‖ + norm (E := A →L[𝕜] A) ((mul 𝕜 A : (a : A) → A →L[𝕜] A) x.toProd.2 : A →L[𝕜] A) =
  ‖x.toProd.1‖ + ‖x.toProd.2‖
Tactic: rw [norm_algebraMap', (AddMonoidHomClass.isometry_iff_norm (mul 𝕜 A)).mp (isometry_mul 𝕜 A)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Unitization (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : IsScalarTower 𝕜 A A
inst_4 : SMulCommClass 𝕜 A A
inst_5 : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
h : Nontrivial A
rw :
  ‖x.toProd.1‖ + norm (E := A →L[𝕜] A) ((mul 𝕜 A : (a : A) → A →L[𝕜] A) x.toProd.2 : A →L[𝕜] A) =
    ‖x.toProd.1‖ + ‖x.toProd.2‖
⊢ norm.{u_2} (E := A →L[𝕜] A) ((algebraMap 𝕜 (A →L[𝕜] A) : (a : 𝕜) → A →L[𝕜] A) x.toProd.1 : A →L[𝕜] A) +
      norm (E := A →L[𝕜] A) ((mul 𝕜 A : (a : A) → A →L[𝕜] A) x.toProd.2 : A →L[𝕜] A) =
    ‖x.toProd.1‖ + ‖x.toProd.2‖
have rw₁ : ‖x.toProd.1‖ + ‖x.toProd.2‖ = ‖x.toProd.1‖ + ‖x.toProd.2‖
Tactic: rw [norm_algebraMap', (AddMonoidHomClass.isometry_iff_norm (mul 𝕜 A)).mp (isometry_mul 𝕜 A)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Unitization (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : IsScalarTower 𝕜 A A
inst_4 : SMulCommClass 𝕜 A A
inst_5 : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
h : Nontrivial A
⊢ ‖HAdd.hAdd (α := A →L[𝕜] A) (β := A →L[𝕜] A) ((algebraMap 𝕜 (A →L[𝕜] A) : (a : 𝕜) → A →L[𝕜] A) x.toProd.1 : A →L[𝕜] A)
        ((mul 𝕜 A : (a : A) → A →L[𝕜] A) x.toProd.2 : A →L[𝕜] A)‖ ≤
    2 *
      max (norm.{u_1} (E := 𝕜) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x).1)
        (norm.{u_2} (E := A) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x).2)
have 𝕜₁ : norm.{u_2} (E := A →L[𝕜] A) ((algebraMap 𝕜 (A →L[𝕜] A) : (a : 𝕜) → A →L[𝕜] A) x.toProd.1 : A →L[𝕜] A) +
    norm (E := A →L[𝕜] A) ((mul 𝕜 A : (a : A) → A →L[𝕜] A) x.toProd.2 : A →L[𝕜] A) =
  ‖x.toProd.1‖ + ‖x.toProd.2‖
Tactic: calc
      ‖algebraMap 𝕜 _ x.fst + mul 𝕜 A x.snd‖ ≤ ‖algebraMap 𝕜 _ x.fst‖ + ‖mul 𝕜 A x.snd‖ :=
        norm_add_le _ _
      _ = ‖x.fst‖ + ‖x.snd‖ := by
        rw [norm_algebraMap', (AddMonoidHomClass.isometry_iff_norm (mul 𝕜 A)).mp (isometry_mul 𝕜 A)]
      _ ≤ _ := (add_le_add (le_max_left _ _) (le_max_right _ _)).trans_eq (two_mul _).symm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Unitization (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : IsScalarTower 𝕜 A A
inst_4 : SMulCommClass 𝕜 A A
inst_5 : RegularNormedAlgebra 𝕜 A
⊢ Eq (α := Filter (Unitization 𝕜 A × Unitization 𝕜 A)) (𝓤 (Unitization 𝕜 A)) (𝓤 (Unitization 𝕜 A))
have key : IsUniformInducing (α := Unitization 𝕜 A) (β := 𝕜 × A) (⇑(addEquiv 𝕜 A) : (a : Unitization 𝕜 A) → 𝕜 × A)
Tactic: have key : IsUniformInducing (addEquiv 𝕜 A) :=
    antilipschitzWith_addEquiv.isUniformInducing lipschitzWith_addEquiv.uniformContinuous
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Unitization (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : IsScalarTower 𝕜 A A
inst_4 : SMulCommClass 𝕜 A A
inst_5 : RegularNormedAlgebra 𝕜 A
key : IsUniformInducing (α := Unitization 𝕜 A) (β := 𝕜 × A) (⇑(addEquiv 𝕜 A) : (a : Unitization 𝕜 A) → 𝕜 × A)
⊢ Eq (α := Filter (Unitization 𝕜 A × Unitization 𝕜 A)) (𝓤 (Unitization 𝕜 A)) (𝓤 (Unitization 𝕜 A))
have rw : Eq (α := Filter (Unitization 𝕜 A × Unitization 𝕜 A)) (𝓤 (Unitization 𝕜 A))
  (comap (β := (𝕜 × A) × 𝕜 × A)
    (fun (x : Unitization 𝕜 A × Unitization 𝕜 A) ↦
      ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x.1, (addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x.2))
    (𝓤 (𝕜 × A)))
Tactic: rw [← key.comap_uniformity]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Unitization (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : IsScalarTower 𝕜 A A
inst_4 : SMulCommClass 𝕜 A A
inst_5 : RegularNormedAlgebra 𝕜 A
k : 𝕜
x : Unitization 𝕜 A
⊢ ‖k • x‖ ≤ ‖k‖ * ‖x‖
have rw : norm (E := Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A))
    ((splitMul 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × (A →L[𝕜] A)) (k • x) : Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A)) ≤
  ‖k‖ * ‖x‖
Tactic: rw [norm_def, map_smul, norm_smul, ← norm_def]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Unitization (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : IsScalarTower 𝕜 A A
inst_4 : SMulCommClass 𝕜 A A
inst_5 : RegularNormedAlgebra 𝕜 A
k : 𝕜
x : Unitization 𝕜 A
rw :
  norm (E := Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A))
      ((splitMul 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × (A →L[𝕜] A)) (k • x) : Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A)) ≤
    ‖k‖ * ‖x‖
⊢ ‖k • x‖ ≤ ‖k‖ * ‖x‖
have rw₁ : ‖HSMul.hSMul (β := Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A)) k
      ((splitMul 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × (A →L[𝕜] A)) x : Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A))‖ ≤
  ‖k‖ * ‖x‖
Tactic: rw [norm_def, map_smul, norm_smul, ← norm_def]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Unitization (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : IsScalarTower 𝕜 A A
inst_4 : SMulCommClass 𝕜 A A
inst_5 : RegularNormedAlgebra 𝕜 A
k : 𝕜
x : Unitization 𝕜 A
rw :
  norm (E := Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A))
      ((splitMul 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × (A →L[𝕜] A)) (k • x) : Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A)) ≤
    ‖k‖ * ‖x‖
rw₁ :
  ‖HSMul.hSMul (β := Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A)) k
        ((splitMul 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × (A →L[𝕜] A)) x : Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A))‖ ≤
    ‖k‖ * ‖x‖
⊢ ‖k • x‖ ≤ ‖k‖ * ‖x‖
have rw₂ : ‖k‖ *
    norm (E := Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A))
      ((splitMul 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × (A →L[𝕜] A)) x : Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A)) ≤
  ‖k‖ * ‖x‖
Tactic: rw [norm_def, map_smul, norm_smul, ← norm_def]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Unitization (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : IsScalarTower 𝕜 A A
inst_4 : SMulCommClass 𝕜 A A
inst_5 : RegularNormedAlgebra 𝕜 A
k : 𝕜
x : Unitization 𝕜 A
rw :
  norm (E := Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A))
      ((splitMul 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × (A →L[𝕜] A)) (k • x) : Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A)) ≤
    ‖k‖ * ‖x‖
rw₁ :
  ‖HSMul.hSMul (β := Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A)) k
        ((splitMul 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × (A →L[𝕜] A)) x : Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A))‖ ≤
    ‖k‖ * ‖x‖
rw₂ :
  ‖k‖ *
      norm (E := Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A))
        ((splitMul 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × (A →L[𝕜] A)) x : Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A)) ≤
    ‖k‖ * ‖x‖
⊢ ‖k • x‖ ≤ ‖k‖ * ‖x‖
have rw₃ : ‖k‖ * ‖x‖ ≤ ‖k‖ * ‖x‖
Tactic: rw [norm_def, map_smul, norm_smul, ← norm_def]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.UnitizationL1 (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : IsScalarTower 𝕜 A A
inst_4 : SMulCommClass 𝕜 A A
x y : WithLp 1 (Unitization 𝕜 A)
⊢ ‖x * y‖ ≤ ‖x‖ * ‖y‖
have simp_rw : ‖x.ofLp.toProd.1 * y.ofLp.toProd.1‖ +
    ‖x.ofLp.toProd.1 • y.ofLp.toProd.2 + y.ofLp.toProd.1 • x.ofLp.toProd.2 + x.ofLp.toProd.2 * y.ofLp.toProd.2‖ ≤
  ‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.1‖ + ‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.2‖ +
    (‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.2‖)
Tactic: simp_rw [unitization_norm_def, add_mul, mul_add, unitization_mul, fst_mul, snd_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.UnitizationL1 (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : IsScalarTower 𝕜 A A
inst_4 : SMulCommClass 𝕜 A A
x y : WithLp 1 (Unitization 𝕜 A)
⊢ ‖x.ofLp.toProd.1 * y.ofLp.toProd.1‖ +
      ‖x.ofLp.toProd.1 • y.ofLp.toProd.2 + y.ofLp.toProd.1 • x.ofLp.toProd.2 + x.ofLp.toProd.2 * y.ofLp.toProd.2‖ ≤
    ‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.1‖ + ‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.2‖ +
      (‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.2‖)
have rw : ‖x.ofLp.toProd.1 * y.ofLp.toProd.1‖ +
    ‖x.ofLp.toProd.1 • y.ofLp.toProd.2 + (y.ofLp.toProd.1 • x.ofLp.toProd.2 + x.ofLp.toProd.2 * y.ofLp.toProd.2)‖ ≤
  ‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.1‖ +
    (‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.2‖ +
      (‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.2‖))
Tactic: rw [add_assoc, add_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.UnitizationL1 (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : IsScalarTower 𝕜 A A
inst_4 : SMulCommClass 𝕜 A A
x y : WithLp 1 (Unitization 𝕜 A)
⊢ ‖x.ofLp.toProd.1 * y.ofLp.toProd.1‖ +
      ‖x.ofLp.toProd.1 • y.ofLp.toProd.2 + (y.ofLp.toProd.1 • x.ofLp.toProd.2 + x.ofLp.toProd.2 * y.ofLp.toProd.2)‖ ≤
    ‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.1‖ +
      (‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.2‖ +
        (‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.2‖))
have h₁ : ‖x.ofLp.toProd.1 * y.ofLp.toProd.1‖ ≤ ‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.1‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.UnitizationL1 (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : IsScalarTower 𝕜 A A
inst_4 : SMulCommClass 𝕜 A A
x y : WithLp 1 (Unitization 𝕜 A)
h₁ : ‖x.ofLp.toProd.1 * y.ofLp.toProd.1‖ ≤ ‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.1‖
⊢ ‖x.ofLp.toProd.1 * y.ofLp.toProd.1‖ +
      ‖x.ofLp.toProd.1 • y.ofLp.toProd.2 + (y.ofLp.toProd.1 • x.ofLp.toProd.2 + x.ofLp.toProd.2 * y.ofLp.toProd.2)‖ ≤
    ‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.1‖ +
      (‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.2‖ +
        (‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.2‖))
have h₂ : ‖x.ofLp.toProd.1 • y.ofLp.toProd.2 + (y.ofLp.toProd.1 • x.ofLp.toProd.2 + x.ofLp.toProd.2 * y.ofLp.toProd.2)‖ ≤
  ‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.2‖ +
    (‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.2‖)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.UnitizationL1 (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : IsScalarTower 𝕜 A A
inst_4 : SMulCommClass 𝕜 A A
x y : WithLp 1 (Unitization 𝕜 A)
⊢ ‖x.ofLp.toProd.1 • y.ofLp.toProd.2 + (y.ofLp.toProd.1 • x.ofLp.toProd.2 + x.ofLp.toProd.2 * y.ofLp.toProd.2)‖ ≤
    ‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.2‖ +
      (‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.2‖)
have h₂ : ‖x.ofLp.toProd.1 • y.ofLp.toProd.2‖ + ‖y.ofLp.toProd.1 • x.ofLp.toProd.2 + x.ofLp.toProd.2 * y.ofLp.toProd.2‖ ≤
  ‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.2‖ +
    (‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.2‖)
Tactic: apply (norm_add_le _ _).trans
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.UnitizationL1 (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : IsScalarTower 𝕜 A A
inst_4 : SMulCommClass 𝕜 A A
x y : WithLp 1 (Unitization 𝕜 A)
⊢ ‖x.ofLp.toProd.1 • y.ofLp.toProd.2‖ + ‖y.ofLp.toProd.1 • x.ofLp.toProd.2 + x.ofLp.toProd.2 * y.ofLp.toProd.2‖ ≤
    ‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.2‖ +
      (‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.2‖)
have h₂ : ‖x.ofLp.toProd.1 • y.ofLp.toProd.2‖ ≤ ‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.2‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.UnitizationL1 (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : IsScalarTower 𝕜 A A
inst_4 : SMulCommClass 𝕜 A A
x y : WithLp 1 (Unitization 𝕜 A)
h₂ : ‖x.ofLp.toProd.1 • y.ofLp.toProd.2‖ ≤ ‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.2‖
⊢ ‖x.ofLp.toProd.1 • y.ofLp.toProd.2‖ + ‖y.ofLp.toProd.1 • x.ofLp.toProd.2 + x.ofLp.toProd.2 * y.ofLp.toProd.2‖ ≤
    ‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.2‖ +
      (‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.2‖)
have h₃ : ‖y.ofLp.toProd.1 • x.ofLp.toProd.2 + x.ofLp.toProd.2 * y.ofLp.toProd.2‖ ≤
  ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.2‖
Tactic: gcongr