awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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
r₁ : R
m₁ : M
r₂ : R
m₂ : M
calc : ‖r₁ * r₂‖ + ‖r₁ • m₂ + MulOpposite.op r₂ • m₁‖ ≤ ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖)
⊢ ‖((r₁, m₁) * (r₂, m₂)).fst‖ + ‖((r₁, m₁) * (r₂, m₂)).snd‖ ≤
    (‖fst (r₁, m₁)‖ + ‖snd (r₁, m₁)‖) * (‖fst (r₂, m₂)‖ + ‖snd (r₂, m₂)‖)
have calc₁ : ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖) ≤ ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖) + ‖m₁‖ * ‖m₂‖
Tactic: calc ‖r₁ * r₂‖ + ‖r₁ • m₂ + MulOpposite.op r₂ • m₁‖
    _ ≤ ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖) := by
      gcongr
      · apply norm_mul_le
      · refine norm_add_le_of_le ?_ ?_ <;>
        apply norm_smul_le
    _ ≤ ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖) + (‖m₁‖ * ‖m₂‖) := by
      apply le_add_of_nonneg_right
      positivity
    _ = (‖r₁‖ + ‖m₁‖) * (‖r₂‖ + ‖m₂‖) := by ring
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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
r₁ : R
m₁ : M
r₂ : R
m₂ : M
calc : ‖r₁ * r₂‖ + ‖r₁ • m₂ + MulOpposite.op r₂ • m₁‖ ≤ ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖)
calc₁ : ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖) ≤ ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖) + ‖m₁‖ * ‖m₂‖
⊢ ‖((r₁, m₁) * (r₂, m₂)).fst‖ + ‖((r₁, m₁) * (r₂, m₂)).snd‖ ≤
    (‖fst (r₁, m₁)‖ + ‖snd (r₁, m₁)‖) * (‖fst (r₂, m₂)‖ + ‖snd (r₂, m₂)‖)
have calc₂ : ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖) + ‖m₁‖ * ‖m₂‖ = (‖r₁‖ + ‖m₁‖) * (‖r₂‖ + ‖m₂‖)
Tactic: calc ‖r₁ * r₂‖ + ‖r₁ • m₂ + MulOpposite.op r₂ • m₁‖
    _ ≤ ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖) := by
      gcongr
      · apply norm_mul_le
      · refine norm_add_le_of_le ?_ ?_ <;>
        apply norm_smul_le
    _ ≤ ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖) + (‖m₁‖ * ‖m₂‖) := by
      apply le_add_of_nonneg_right
      positivity
    _ = (‖r₁‖ + ‖m₁‖) * (‖r₂‖ + ‖m₂‖) := by ring
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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
⊢ norm (E := tsze R M) 1 = 1
have 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
Tactic: rw [norm_def, fst_one, snd_one, norm_zero, norm_one, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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
⊢ norm (E := tsze R M) 1 = 1
have rw₁ : norm.{u_3} (E := R) 1 + norm.{u_4} (E := M) (snd.{u_3, u_4} (R := R) 1) = 1
Tactic: rw [norm_def, fst_one, snd_one, norm_zero, norm_one, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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
⊢ norm (E := tsze R M) 1 = 1
have rw₂ : norm.{u_3} (E := R) 1 + norm.{u_4} (E := M) 0 = 1
Tactic: rw [norm_def, fst_one, snd_one, norm_zero, norm_one, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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
⊢ norm (E := tsze R M) 1 = 1
have rw₃ : norm.{u_3} (E := R) 1 + 0 = 1
Tactic: rw [norm_def, fst_one, snd_one, norm_zero, norm_one, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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
⊢ norm (E := tsze R M) 1 = 1
have rw₄ : HAdd.hAdd (α := ℝ) 1 0 = 1
Tactic: rw [norm_def, fst_one, snd_one, norm_zero, norm_one, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
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
⊢ norm (E := tsze R M) 1 = 1
have rw₅ : Eq (α := ℝ) 1 1
Tactic: rw [norm_def, fst_one, snd_one, norm_zero, norm_one, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Ultra (goal)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : NormedDivisionRing L
inst_2 : NormedAlgebra K L
h : IsUltrametricDist K
⊢ IsUltrametricDist L
have rw : ∀ (h : ∀ (n : ℕ), norm.{u_1} (E := K) (↑n : K) ≤ 1) (n : ℕ), norm.{u_2} (E := L) (↑n : L) ≤ 1
Tactic: rw [isUltrametricDist_iff_forall_norm_natCast_le_one] at h ⊢
Cleared hypotheses: h
-- 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
x : Unitization 𝕜 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))
have 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))
Tactic: rw [add_zero]
-- 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
h : Function.Injective (α := A) (β := A →L[𝕜] A) (⇑(mul 𝕜 A) : (a : A) → A →L[𝕜] A)
⊢ Function.Injective (α := Unitization 𝕜 A) (β := Prod.{u_1, u_2} 𝕜 (A →L[𝕜] A))
    (⇑(splitMul 𝕜 A) : (a : Unitization 𝕜 A) → 𝕜 × (A →L[𝕜] A))
have 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
Tactic: rw [injective_iff_map_eq_zero]
-- 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
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))
⊢ x = 0
have 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
Tactic: induction x
Cleared hypotheses: x, hx
-- 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
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))
⊢ inl r + (↑a : Unitization 𝕜 A) = 0
have 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
Tactic: rw [map_add] at hx
Cleared hypotheses: hx
-- 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
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
⊢ inl r + (↑a : Unitization 𝕜 A) = 0
have 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
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
Cleared hypotheses: hx
-- 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
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 r + (↑a : Unitization 𝕜 A) = 0
have 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
Tactic: obtain ⟨rfl, hx⟩ := hx
Cleared hypotheses: r, hx
-- 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
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
⊢ HAdd.hAdd (α := Unitization 𝕜 A) (inl 0) (↑a : Unitization 𝕜 A) = 0
have 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
Tactic: simp only [map_zero, zero_add, inl_zero] at hx ⊢
Cleared hypotheses: hx
-- 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
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 (α := Unitization 𝕜 A) (↑a : Unitization 𝕜 A) 0
have 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)
Tactic: rw [← map_zero (mul 𝕜 A)] at hx
Cleared hypotheses: hx
-- 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
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)
⊢ Eq (α := Unitization 𝕜 A) (↑a : Unitization 𝕜 A) 0
have inl_add_inr : Eq (α := Unitization 𝕜 A) (↑0 : Unitization 𝕜 A) 0
Tactic: rw [h hx, inr_zero]
-- 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
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
⊢ Eq (α := Unitization 𝕜 A) (↑a : Unitization 𝕜 A) 0
have inl_add_inr₁ : Eq (α := Unitization 𝕜 A) 0 0
Tactic: rw [h hx, inr_zero]
-- 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‖ =
    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 (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)‖
Tactic: rw [norm_def, splitMul_apply, Prod.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
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)‖
⊢ ‖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)‖
have 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)‖
Tactic: rw [norm_def, splitMul_apply, Prod.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
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)‖
⊢ ‖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)‖
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)).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)‖
Tactic: rw [norm_def, splitMul_apply, Prod.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
⊢ LipschitzWith (α := Unitization 𝕜 A) (β := 𝕜 × A) 2 (⇑(addEquiv 𝕜 A) : (a : Unitization 𝕜 A) → 𝕜 × A)
have rw : LipschitzWith (α := Unitization 𝕜 A) (β := 𝕜 × A) (Real.toNNReal 2) (⇑(addEquiv 𝕜 A) : (a : Unitization 𝕜 A) → 𝕜 × A)
Tactic: rw [← Real.toNNReal_ofNat]
-- 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
⊢ LipschitzWith (α := Unitization 𝕜 A) (β := 𝕜 × A) (Real.toNNReal 2) (⇑(addEquiv 𝕜 A) : (a : Unitization 𝕜 A) → 𝕜 × A)
have refine : ∀ (x : Unitization 𝕜 A), norm (E := 𝕜 × A) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x : 𝕜 × A) ≤ 2 * ‖x‖
Tactic: refine AddMonoidHomClass.lipschitz_of_bound (Unitization.addEquiv 𝕜 A) 2 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
⊢ norm (E := 𝕜 × A) ((addEquiv 𝕜 A : (a : Unitization 𝕜 A) → 𝕜 × A) x : 𝕜 × A) ≤ 2 * ‖x‖
have 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)‖
Tactic: rw [norm_eq_sup, Prod.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
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)‖
have 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)‖
Tactic: refine max_le ?_ ?_