awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
𝕜 : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst : SeminormedCommRing S
inst_1 : SeminormedRing R
inst_2 : SeminormedAddCommGroup M
inst_3 : Algebra S R
inst_4 : Module S M
inst_5 : IsBoundedSMul S R
inst_6 : IsBoundedSMul S M
inst_7 : Module R M
inst_8 : IsBoundedSMul R M
inst_9 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_10 : IsBoundedSMul.{u_3, u_4} Rᵐᵒᵖ M
inst_11 : SMulCommClass R Rᵐᵒᵖ M
inst_12 : NormOneClass R
rw : norm.{u_3} (E := R) (fst.{u_3, u_4} (M := M) 1) + norm.{u_4} (E := M) (snd.{u_3, u_4} (R := R) 1) = 1
rw₁ : norm.{u_3} (E := R) 1 + norm.{u_4} (E := M) (snd.{u_3, u_4} (R := R) 1) = 1
rw₂ : norm.{u_3} (E := R) 1 + norm.{u_4} (E := M) 0 = 1
rw₃ : norm.{u_3} (E := R) 1 + 0 = 1
rw₄ : HAdd.hAdd (α := ℝ) 1 0 = 1
rw₅ rw₆ : Eq (α := ℝ) 1 1
⊢ norm (E := tsze R M) 1 = 1

Tactic:
rw [norm_def, fst_one, snd_one, norm_zero, norm_one, add_zero]

Premises used: norm_zero, TrivSqZeroExt.norm_def, NormOneClass.norm_one, TrivSqZeroExt.fst_one, TrivSqZeroExt.snd_one, add_zero
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
𝕜 : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst : NormedRing R
inst_1 : NormedAddCommGroup M
inst_2 : NormedAlgebra ℚ R
inst_3 : NormedSpace ℚ M
inst_4 : Module R M
inst_5 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_6 : IsBoundedSMul R M
inst_7 : IsBoundedSMul.{u_3, u_4} Rᵐᵒᵖ M
inst_8 : SMulCommClass R Rᵐᵒᵖ M
inst_9 : CompleteSpace R
inst_10 : CompleteSpace M
a b : tsze R M
h : Commute a b
⊢ exp (a + b) = exp a * exp b

Tactic:
exp_add_of_commute h

Premises used: NormedSpace.exp_add_of_commute
-- Module: Mathlib.Analysis.Normed.Algebra.Ultra
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : SeminormedRing L
inst_2 : NormOneClass L
inst_3 : NormedAlgebra K L
h : IsUltrametricDist L
x y z : K
⊢ dist x z ≤ max (dist x y) (dist y z)

Tactic:
simpa using h.dist_triangle_max (algebraMap K L x) (algebraMap K L y) (algebraMap K L z)

Premises used: Algebra.algebraMap, IsUltrametricDist.dist_triangle_max, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Algebra.Ultra
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : NormedDivisionRing L
inst_2 : NormedAlgebra K L
h : IsUltrametricDist K
rw : ∀ (h : ∀ (n : ℕ), norm.{u_1} (E := K) (↑n : K) ≤ 1) (n : ℕ), norm.{u_2} (E := L) (↑n : L) ≤ 1
⊢ IsUltrametricDist L

Tactic:
rw [isUltrametricDist_iff_forall_norm_natCast_le_one] at h ⊢

Premises used: isUltrametricDist_iff_forall_norm_natCast_le_one
-- Module: Mathlib.Analysis.Normed.Algebra.Ultra
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : NormedDivisionRing L
inst_2 : NormedAlgebra K L
h : ∀ (n : ℕ), norm.{u_1} (E := K) (↑n : K) ≤ 1
⊢ ∀ (n : ℕ), norm.{u_2} (E := L) (↑n : L) ≤ 1

Tactic:
fun n => (algebraMap.coe_natCast (R := K) (A := L) n) ▸ norm_algebraMap' L (n : K) ▸ h n

Premises used: Eq.rec, Nat.cast, norm_algebraMap', algebraMap.coe_natCast, Eq.symm
-- Module: Mathlib.Analysis.Normed.Algebra.Ultra
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : NormedDivisionRing L
inst_2 : NormedAlgebra K L
h : ∀ (n : ℕ), norm.{u_1} (E := K) (↑n : K) ≤ 1
⊢ ∀ (n : ℕ), norm.{u_2} (E := L) (↑n : L) ≤ 1

Tactic:
exact fun n => (algebraMap.coe_natCast (R := K) (A := L) n) ▸ norm_algebraMap' L (n : K) ▸ h n
-- Module: Mathlib.Analysis.Normed.Algebra.Ultra
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : NormedDivisionRing L
inst_2 : NormedAlgebra K L
⊢ IsUltrametricDist L ↔ IsUltrametricDist K

Tactic:
⟨fun _ => IsUltrametricDist.of_normedAlgebra' L, fun _ => IsUltrametricDist.of_normedAlgebra K⟩

Premises used: IsUltrametricDist.of_normedAlgebra', IsUltrametricDist.of_normedAlgebra, Iff.intro
-- 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
x : Unitization 𝕜 A
rw :
  (x.toProd.1,
      (AlgHom.toRingHom (R := 𝕜)
            ((lift : (a : A →ₙₐ[𝕜] A →L[𝕜] A) → Unitization 𝕜 A →ₐ[𝕜] A →L[𝕜] A) (NonUnitalAlgHom.Lmul 𝕜 A)) :
          (a : Unitization 𝕜 A) → A →L[𝕜] A)
        x) =
    (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))
⊢ (x.toProd.1 + 0,
      (AlgHom.toRingHom (R := 𝕜)
            ((lift : (a : A →ₙₐ[𝕜] A →L[𝕜] A) → Unitization 𝕜 A →ₐ[𝕜] A →L[𝕜] A) (NonUnitalAlgHom.Lmul 𝕜 A)) :
          (a : Unitization 𝕜 A) → A →L[𝕜] A)
        x) =
    (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 [add_zero]

Premises used: 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
x : Unitization 𝕜 A
⊢ (x.toProd.1,
      (AlgHom.toRingHom (R := 𝕜)
            ((lift : (a : A →ₙₐ[𝕜] A →L[𝕜] A) → Unitization 𝕜 A →ₐ[𝕜] A →L[𝕜] A) (NonUnitalAlgHom.Lmul 𝕜 A)) :
          (a : Unitization 𝕜 A) → A →L[𝕜] A)
        x) =
    (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:
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
h : Function.Injective (α := A) (β := A →L[𝕜] A) (⇑(mul 𝕜 A) : (a : A) → A →L[𝕜] A)
rw :
  ∀ (a : Unitization 𝕜 A),
    Eq (α := Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A))
        ((splitMul 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × (A →L[𝕜] A)) a : Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A))
        (0 : Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A)) →
      a = 0
⊢ Function.Injective (α := Unitization 𝕜 A) (β := Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A))
    (⇑(splitMul 𝕜 A) : (a : Unitization 𝕜 A) → 𝕜 × (A →L[𝕜] A))

Tactic:
rw [injective_iff_map_eq_zero]

Premises used: injective_iff_map_eq_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
h : Function.Injective (α := A) (β := A →L[𝕜] A) (⇑(mul 𝕜 A) : (a : A) → A →L[𝕜] A)
x : Unitization 𝕜 A
hx :
  Eq (α := 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))
    (0 : Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A))
inl_add_inr :
  ∀ (r : 𝕜) (a : A)
    (hx :
      Eq (α := Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A))
        ((splitMul 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × (A →L[𝕜] A)) (inl r + (↑a : Unitization 𝕜 A)) :
          Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A))
        (0 : Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A))),
    inl r + (↑a : Unitization 𝕜 A) = 0
⊢ x = 0

Tactic:
induction x
-- 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
h : Function.Injective (α := A) (β := A →L[𝕜] A) (⇑(mul 𝕜 A) : (a : A) → A →L[𝕜] A)
r : 𝕜
a : A
hx :
  Eq (α := Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A))
    ((splitMul 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × (A →L[𝕜] A)) (inl r + (↑a : Unitization 𝕜 A)) :
      Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A))
    (0 : Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A))
⊢ HAdd.hAdd (α := Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A)) (β := Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A))
      ((splitMul 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × (A →L[𝕜] A)) (inl r) : Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A))
      ((splitMul 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × (A →L[𝕜] A)) (↑a : Unitization 𝕜 A) :
        Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A)) =
    0

Tactic:
rw [map_add] at hx

Premises used: map_add
-- 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
h : Function.Injective (α := A) (β := A →L[𝕜] A) (⇑(mul 𝕜 A) : (a : A) → A →L[𝕜] A)
r : 𝕜
a : A
hx :
  HAdd.hAdd (α := Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A)) (β := Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A))
      ((splitMul 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × (A →L[𝕜] A)) (inl r) : Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A))
      ((splitMul 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × (A →L[𝕜] A)) (↑a : Unitization 𝕜 A) :
        Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A)) =
    0
⊢ r = 0 ∧
    HAdd.hAdd (α := A →L[𝕜] A) (β := A →L[𝕜] A) ((algebraMap 𝕜 (A →L[𝕜] A) : (a : 𝕜) → A →L[𝕜] A) r : A →L[𝕜] A)
        ((mul 𝕜 A : (a : A) → A →L[𝕜] A) a : A →L[𝕜] A) =
      0

Tactic:
simp only [splitMul_apply, fst_inl, snd_inl, map_zero, add_zero, fst_inr, snd_inr,
    zero_add, Prod.mk_add_mk, Prod.mk_eq_zero] at hx

Premises used: Prod.mk_add_mk, Unitization.fst_inr, Unitization.splitMul_apply, Unitization.fst_inl, Unitization.snd_inr, map_zero, zero_add, Prod.mk_eq_zero, add_zero, Unitization.snd_inl
-- 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
h : Function.Injective (α := A) (β := A →L[𝕜] A) (⇑(mul 𝕜 A) : (a : A) → A →L[𝕜] A)
r : 𝕜
a : A
hx :
  r = 0 ∧
    HAdd.hAdd (α := A →L[𝕜] A) (β := A →L[𝕜] A) ((algebraMap 𝕜 (A →L[𝕜] A) : (a : 𝕜) → A →L[𝕜] A) r : A →L[𝕜] A)
        ((mul 𝕜 A : (a : A) → A →L[𝕜] A) a : A →L[𝕜] A) =
      0
inl_add_inr :
  ∀
    (hx :
      HAdd.hAdd (α := A →L[𝕜] A) (β := A →L[𝕜] A) ((algebraMap 𝕜 (A →L[𝕜] A) : (a : 𝕜) → A →L[𝕜] A) 0 : A →L[𝕜] A)
          ((mul 𝕜 A : (a : A) → A →L[𝕜] A) a : A →L[𝕜] A) =
        0),
    HAdd.hAdd (α := Unitization 𝕜 A) (inl 0) (↑a : Unitization 𝕜 A) = 0
⊢ inl r + (↑a : Unitization 𝕜 A) = 0

Tactic:
obtain ⟨rfl, hx⟩ := hx

Premises used: 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
h : Function.Injective (α := A) (β := A →L[𝕜] A) (⇑(mul 𝕜 A) : (a : A) → A →L[𝕜] A)
a : A
hx :
  HAdd.hAdd (α := A →L[𝕜] A) (β := A →L[𝕜] A) ((algebraMap 𝕜 (A →L[𝕜] A) : (a : 𝕜) → A →L[𝕜] A) 0 : A →L[𝕜] A)
      ((mul 𝕜 A : (a : A) → A →L[𝕜] A) a : A →L[𝕜] A) =
    0
inl_add_inr :
  ∀ (hx : Eq (α := A →L[𝕜] A) ((mul 𝕜 A : (a : A) → A →L[𝕜] A) a : A →L[𝕜] A) (0 : A →L[𝕜] A)),
    Eq (α := Unitization 𝕜 A) (↑a : Unitization 𝕜 A) 0
⊢ HAdd.hAdd (α := Unitization 𝕜 A) (inl 0) (↑a : Unitization 𝕜 A) = 0

Tactic:
simp only [map_zero, zero_add, inl_zero] at hx ⊢

Premises used: Unitization.inl_zero, map_zero, zero_add
-- 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
h : Function.Injective (α := A) (β := A →L[𝕜] A) (⇑(mul 𝕜 A) : (a : A) → A →L[𝕜] A)
a : A
hx : Eq (α := A →L[𝕜] A) ((mul 𝕜 A : (a : A) → A →L[𝕜] A) a : A →L[𝕜] A) (0 : A →L[𝕜] A)
⊢ Eq (α := A →L[𝕜] A) ((mul 𝕜 A : (a : A) → A →L[𝕜] A) a : A →L[𝕜] A) ((mul 𝕜 A : (a : A) → A →L[𝕜] A) 0 : A →L[𝕜] A)

Tactic:
rw [← map_zero (mul 𝕜 A)] at hx

Premises used: map_zero, ContinuousLinearMap.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
h : Function.Injective (α := A) (β := A →L[𝕜] A) (⇑(mul 𝕜 A) : (a : A) → A →L[𝕜] A)
a : A
hx : Eq (α := A →L[𝕜] A) ((mul 𝕜 A : (a : A) → A →L[𝕜] A) a : A →L[𝕜] A) ((mul 𝕜 A : (a : A) → A →L[𝕜] A) 0 : A →L[𝕜] A)
inl_add_inr : Eq (α := Unitization 𝕜 A) (↑0 : Unitization 𝕜 A) 0
inl_add_inr₁ inl_add_inr₂ : Eq (α := Unitization 𝕜 A) 0 0
⊢ Eq (α := Unitization 𝕜 A) (↑a : Unitization 𝕜 A) 0

Tactic:
rw [h hx, inr_zero]

Premises used: Unitization.inr_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
⊢ Function.Injective (α := Unitization 𝕜 A) (β := Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A))
    (⇑(splitMul 𝕜 A) : (a : Unitization 𝕜 A) → 𝕜 × (A →L[𝕜] A))

Tactic:
splitMul_injective_of_clm_mul_injective (isometry_mul 𝕜 A).injective

Premises used: Unitization.splitMul_injective_of_clm_mul_injective, Isometry.injective, ContinuousLinearMap.isometry_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
⊢ ‖x‖ =
    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))

Tactic:
rfl

Premises used: 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
x : Unitization 𝕜 A
⊢ ‖x‖₊ =
    nnnorm (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))

Tactic:
rfl

Premises used: 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
x : Unitization 𝕜 A
rw :
  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)) =
    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)‖
rw₁ :
  ‖(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)‖
rw₂ 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)).1‖
      ‖(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 ‖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)‖
⊢ ‖x‖ =
    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 [norm_def, splitMul_apply, Prod.norm_def]

Premises used: Unitization.splitMul_apply, Prod.norm_def, Unitization.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
⊢ ‖x‖₊ =
    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:
NNReal.eq <| norm_eq_sup x

Premises used: NNReal.eq, 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
rw :
  LipschitzWith (α := Unitization 𝕜 A) (β := 𝕜 × A) (Real.toNNReal 2) (⇑(addEquiv 𝕜 A) : (a : Unitization 𝕜 A) → 𝕜 × A)
⊢ LipschitzWith (α := Unitization 𝕜 A) (β := 𝕜 × A) 2 (⇑(addEquiv 𝕜 A) : (a : Unitization 𝕜 A) → 𝕜 × A)

Tactic:
rw [← Real.toNNReal_ofNat]

Premises used: Real.toNNReal_ofNat
-- 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
⊢ LipschitzWith (α := Unitization 𝕜 A) (β := 𝕜 × A) (Real.toNNReal 2) (⇑(addEquiv 𝕜 A) : (a : Unitization 𝕜 A) → 𝕜 × A)

Tactic:
AddMonoidHomClass.lipschitz_of_bound (Unitization.addEquiv 𝕜 A) 2 fun x => ?_

Premises used: Unitization.addEquiv, AddMonoidHomClass.lipschitz_of_bound, OfNat.ofNat
-- 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), norm (E := 𝕜 × A) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x : 𝕜 × A) ≤ 2 * ‖x‖
⊢ LipschitzWith (α := Unitization 𝕜 A) (β := 𝕜 × A) (Real.toNNReal 2) (⇑(addEquiv 𝕜 A) : (a : Unitization 𝕜 A) → 𝕜 × A)

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

Premises used: Unitization.addEquiv, AddMonoidHomClass.lipschitz_of_bound, OfNat.ofNat
-- 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 (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)‖
⊢ norm (E := 𝕜 × A) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x : 𝕜 × A) ≤ 2 * ‖x‖

Tactic:
rw [norm_eq_sup, Prod.norm_def]

Premises used: Unitization.norm_eq_sup, 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 (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)‖

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 :
  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)‖
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)‖
⊢ 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)‖

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 :
  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)‖)
⊢ 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)‖

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
⊢ 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:
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
⊢ 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:
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