awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
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
⊢ Nontrivial A

Tactic:
nontriviality A
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
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 :
  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)‖
⊢ 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:
rw [two_mul]

Premises used: two_mul
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
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
⊢ ‖x.toProd.2‖ = norm (E := A →L[𝕜] A) ((mul 𝕜 A : (a : A) → A →L[𝕜] A) x.toProd.2 : A →L[𝕜] A)

Tactic:
.symm <| (isometry_mul 𝕜 A).norm_map_of_map_zero (map_zero _) _

Premises used: map_zero, ContinuousLinearMap.isometry_mul, Isometry.norm_map_of_map_zero, Eq.symm
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
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 (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:
simpa only [add_comm _ (mul 𝕜 A x.snd), norm_algebraMap'] using
          norm_le_add_norm_add (mul 𝕜 A x.snd) (algebraMap 𝕜 _ x.fst)

Premises used: Algebra.algebraMap, norm_le_add_norm_add, add_comm, Prod.fst, ContinuousLinearMap.mul, Unitization.toProd, norm_algebraMap', Prod.snd, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
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)‖ +
      ‖x.toProd.1‖ ≤
    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:
add_le_add le_sup_right le_sup_left

Premises used: le_sup_left, add_le_add, le_sup_right
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
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 (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‖
⊢ 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:
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

Premises used: Algebra.algebraMap, le_sup_left, add_le_add, map_zero, le_sup_right, Prod.fst, ContinuousLinearMap.isometry_mul, Isometry.norm_map_of_map_zero, ContinuousLinearMap.mul, Unitization.toProd, Prod.snd, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
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)

Tactic:
AddMonoidHomClass.antilipschitz_of_bound (addEquiv 𝕜 A) fun x => ?_

Premises used: Unitization.addEquiv, AddMonoidHomClass.antilipschitz_of_bound
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
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
refine :
  ∀ (x : Unitization 𝕜 A), ‖x‖ ≤ (↑2 : ℝ) * norm (E := 𝕜 × A) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x : 𝕜 × A)
⊢ AntilipschitzWith (α := Unitization 𝕜 A) (β := 𝕜 × A) 2 (⇑(addEquiv 𝕜 A) : (a : Unitization 𝕜 A) → 𝕜 × A)

Tactic:
refine AddMonoidHomClass.antilipschitz_of_bound (addEquiv 𝕜 A) fun x => ?_

Premises used: Unitization.addEquiv, AddMonoidHomClass.antilipschitz_of_bound
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
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
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)
⊢ ‖x‖ ≤ (↑2 : ℝ) * norm (E := 𝕜 × A) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x : 𝕜 × A)

Tactic:
rw [norm_eq_sup, Prod.norm_def, NNReal.coe_two]

Premises used: Unitization.norm_eq_sup, NNReal.coe_two, Prod.norm_def
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
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)

Tactic:
max_le ?_ ?_

Premises used: max_le
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
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)
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)
⊢ 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:
refine max_le ?_ ?_

Premises used: max_le
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
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‖ ≤
    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)
⊢ ‖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:
rw [mul_max_of_nonneg _ _ (zero_le_two : (0 : ℝ) ≤ 2)]

Premises used: mul_max_of_nonneg, zero_le_two
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
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‖ ≤
    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:
le_max_of_le_left ((le_add_of_nonneg_left (norm_nonneg _)).trans_eq (two_mul _).symm)

Premises used: LE.le.trans_eq, two_mul, le_max_of_le_left, Eq.symm, norm_nonneg, le_add_of_nonneg_left
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
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‖ ≤
    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:
exact le_max_of_le_left ((le_add_of_nonneg_left (norm_nonneg _)).trans_eq (two_mul _).symm)

Premises used: LE.le.trans_eq, two_mul, le_max_of_le_left, Eq.symm, norm_nonneg, le_add_of_nonneg_left
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
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)‖ ≤
    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)

Tactic:
norm_add_le _ _

Premises used: norm_add_le
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
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‖
rw₁ rw₂ : ‖x.toProd.1‖ + ‖x.toProd.2‖ = ‖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‖

Tactic:
rw [norm_algebraMap', (AddMonoidHomClass.isometry_iff_norm (mul 𝕜 A)).mp (isometry_mul 𝕜 A)]

Premises used: ContinuousLinearMap.isometry_mul, ContinuousLinearMap.mul, AddMonoidHomClass.isometry_iff_norm, Iff.mp, norm_algebraMap'
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
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
⊢ ‖x.toProd.1‖ + ‖x.toProd.2‖ ≤ 2 * max ‖x.toProd.1‖ ‖x.toProd.2‖

Tactic:
(add_le_add (le_max_left _ _) (le_max_right _ _)).trans_eq (two_mul _).symm

Premises used: le_max_right, LE.le.trans_eq, add_le_add, two_mul, Eq.symm, le_max_left
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
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‖
⊢ ‖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:
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

Premises used: le_max_right, LE.le.trans_eq, Algebra.algebraMap, add_le_add, two_mul, norm_add_le, Prod.fst, ContinuousLinearMap.mul, Unitization.toProd, Eq.symm, le_max_left, Prod.snd, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
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
⊢ IsUniformInducing (α := Unitization 𝕜 A) (β := 𝕜 × A) (⇑(addEquiv 𝕜 A) : (a : Unitization 𝕜 A) → 𝕜 × A)

Tactic:
have key : IsUniformInducing (addEquiv 𝕜 A) :=
    antilipschitzWith_addEquiv.isUniformInducing lipschitzWith_addEquiv.uniformContinuous
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
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)
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)))
⊢ Eq (α := Filter (Unitization 𝕜 A × Unitization 𝕜 A)) (𝓤 (Unitization 𝕜 A)) (𝓤 (Unitization 𝕜 A))

Tactic:
rw [← key.comap_uniformity]

Premises used: IsUniformInducing.comap_uniformity
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
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))
    (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:
rfl
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
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)) (cobounded (Unitization 𝕜 A)) (cobounded (Unitization 𝕜 A))

Tactic:
le_antisymm lipschitzWith_addEquiv.comap_cobounded_le
    antilipschitzWith_addEquiv.tendsto_cobounded.le_comap

Premises used: Filter.Tendsto.le_comap, AntilipschitzWith.tendsto_cobounded, LipschitzWith.comap_cobounded_le, le_antisymm
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
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
inst_6 : CompleteSpace 𝕜
inst_7 : CompleteSpace A
⊢ CompleteSpace (Unitization 𝕜 A)

Tactic:
uniformEquivProd.completeSpace_iff.2 .prod

Premises used: Iff.mpr, CompleteSpace.prod, UniformEquiv.completeSpace_iff, Unitization.uniformEquivProd
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
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
⊢ T2Space (Unitization 𝕜 A)

Tactic:
Unitization.uniformEquivProd.symm.toHomeomorph.t2Space

Premises used: UniformEquiv.toHomeomorph, UniformEquiv.symm, Homeomorph.t2Space, Unitization.uniformEquivProd
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
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‖
rw₃ rw₄ : ‖k‖ * ‖x‖ ≤ ‖k‖ * ‖x‖
⊢ ‖k • x‖ ≤ ‖k‖ * ‖x‖

Tactic:
rw [norm_def, map_smul, norm_smul, ← norm_def]

Premises used: norm_smul, Unitization.norm_def, map_smul
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
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 : A
⊢ norm (E := A) ((1 : (a : A) → A) x : A) ≤ 1 * ‖x‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
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
⊢ norm (E := Unitization 𝕜 A) 1 = 1

Tactic:
simpa only [norm_eq_sup, fst_one, norm_one, snd_one, map_one, map_zero,
      add_zero, sup_eq_left] using opNorm_le_bound _ zero_le_one fun x => by simp

Premises used: NormOneClass.norm_one, map_zero, sup_eq_left, ContinuousLinearMap.opNorm_le_bound, Unitization.norm_eq_sup, zero_le_one, Unitization.fst_one, map_one, Unitization.snd_one, add_zero
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
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
a : A
⊢ norm (E := Unitization 𝕜 A) (↑a : Unitization 𝕜 A) = ‖a‖

Tactic:
simp [norm_eq_sup]

Premises used: Unitization.norm_eq_sup
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
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
a : A
⊢ nnnorm (E := Unitization 𝕜 A) (↑a : Unitization 𝕜 A) = ‖a‖₊

Tactic:
NNReal.eq <| norm_inr a

Premises used: NNReal.eq, Unitization.norm_inr
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
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
⊢ Isometry (α := A) (β := Unitization 𝕜 A) inr

Tactic:
AddMonoidHomClass.isometry_of_norm (inrNonUnitalAlgHom 𝕜 A) norm_inr

Premises used: AddMonoidHomClass.isometry_of_norm, Unitization.inr, Unitization.inrNonUnitalAlgHom, Unitization.norm_inr
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
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
⊢ Continuous (X := A) (Y := Unitization 𝕜 A) inr

Tactic:
isometry_inr.continuous

Premises used: Unitization.isometry_inr, Isometry.continuous
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
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
a b : A
⊢ dist (α := Unitization 𝕜 A) (↑a : Unitization 𝕜 A) (↑b : Unitization 𝕜 A) = dist a b

Tactic:
isometry_inr.dist_eq a b

Premises used: Unitization.isometry_inr, Isometry.dist_eq
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
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
a b : A
⊢ nndist (α := Unitization 𝕜 A) (↑a : Unitization 𝕜 A) (↑b : Unitization 𝕜 A) = nndist a b

Tactic:
isometry_inr.nndist_eq a b

Premises used: Unitization.isometry_inr, Isometry.nndist_eq