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
⊢ Eq (α := MetricSpace (Unitization 𝕜 A)) NormedRing.toMetricSpace instMetricSpace

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
⊢ Eq (α := Bornology (Unitization 𝕜 A)) PseudoMetricSpace.toBornology instBornology

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
⊢ Eq (α := UniformSpace (Unitization 𝕜 A)) PseudoMetricSpace.toUniformSpace instUniformSpace

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
Goal:
𝕜 : Type u_3
A : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
⊢ UniformContinuous (β := 𝕜) fun (x : Unitization 𝕜 A) ↦ x.toProd.1

Tactic:
uniformContinuous_fst.comp Unitization.uniformEquivProd.uniformContinuous

Premises used: UniformContinuous.comp, uniformContinuous_fst, UniformEquiv.uniformContinuous, Unitization.uniformEquivProd
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
Goal:
𝕜 : Type u_3
A : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
⊢ UniformContinuous (β := A) fun (x : Unitization 𝕜 A) ↦ x.toProd.2

Tactic:
uniformContinuous_snd.comp Unitization.uniformEquivProd.uniformContinuous

Premises used: uniformContinuous_snd, UniformContinuous.comp, UniformEquiv.uniformContinuous, Unitization.uniformEquivProd
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
Goal:
𝕜 : Type u_3
A : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
⊢ Continuous (Y := 𝕜) fun (x : Unitization 𝕜 A) ↦ x.toProd.1

Tactic:
Unitization.uniformContinuous_fst.continuous

Premises used: Unitization.uniformContinuous_fst, UniformContinuous.continuous
-- Module: Mathlib.Analysis.Normed.Algebra.Unitization
Goal:
𝕜 : Type u_3
A : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing A
⊢ Continuous (Y := A) fun (x : Unitization 𝕜 A) ↦ x.toProd.2

Tactic:
Unitization.uniformContinuous_snd.continuous

Premises used: UniformContinuous.continuous, Unitization.uniformContinuous_snd
-- Module: Mathlib.Analysis.Normed.Algebra.UnitizationL1
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : CompleteSpace 𝕜
inst_4 : CompleteSpace A
⊢ CompleteSpace (WithLp 1 (Unitization 𝕜 A))

Tactic:
completeSpace_congr (uniformEquiv_unitization_addEquiv_prod 𝕜 A).isUniformEmbedding |>.mpr
    inferInstance

Premises used: Iff.mpr, WithLp.uniformEquiv_unitization_addEquiv_prod, completeSpace_congr, inferInstance, UniformEquiv.isUniformEmbedding
-- Module: Mathlib.Analysis.Normed.Algebra.UnitizationL1
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
x : WithLp 1 (Unitization 𝕜 A)
⊢ 0 < ENNReal.toReal 1

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Algebra.UnitizationL1
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
x : WithLp 1 (Unitization 𝕜 A)
⊢ (‖x.ofLp.toProd.1‖ ^ ENNReal.toReal 1 + ‖x.ofLp.toProd.2‖ ^ ENNReal.toReal 1) ^ (1 / ENNReal.toReal 1) =
    ‖x.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Algebra.UnitizationL1
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
x : WithLp 1 (Unitization 𝕜 A)
⊢ ‖x‖₊ = ‖x.ofLp.toProd.1‖₊ + ‖x.ofLp.toProd.2‖₊

Tactic:
Subtype.ext <| unitization_norm_def x

Premises used: NNReal, WithLp.unitization_norm_def, Subtype.ext
-- Module: Mathlib.Analysis.Normed.Algebra.UnitizationL1
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
x : A
⊢ norm (E := WithLp 1 (Unitization 𝕜 A)) (toLp 1 (↑x : Unitization 𝕜 A)) = ‖x‖

Tactic:
simp [unitization_norm_def]

Premises used: WithLp.unitization_norm_def
-- Module: Mathlib.Analysis.Normed.Algebra.UnitizationL1
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
x : A
⊢ nnnorm (E := WithLp 1 (Unitization 𝕜 A)) (toLp 1 (↑x : Unitization 𝕜 A)) = ‖x‖₊

Tactic:
simp [unitization_nnnorm_def]

Premises used: WithLp.unitization_nnnorm_def
-- Module: Mathlib.Analysis.Normed.Algebra.UnitizationL1
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
⊢ Isometry (β := WithLp 1 (Unitization 𝕜 A)) fun (x : A) ↦ toLp 1 (↑x : Unitization 𝕜 A)

Tactic:
AddMonoidHomClass.isometry_of_norm
    ((WithLp.linearEquiv 1 𝕜 (Unitization 𝕜 A)).symm.comp <| Unitization.inrHom 𝕜 𝕜 A)
    unitization_norm_inr

Premises used: LinearEquiv.symm, AddMonoidHomClass.isometry_of_norm, Unitization.inr, Unitization.inrHom, LinearMap.comp, LinearEquiv.toLinearMap, Unitization, OfNat.ofNat, WithLp.unitization_norm_inr, WithLp.linearEquiv
-- Module: Mathlib.Analysis.Normed.Algebra.UnitizationL1
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).ofLp = x.ofLp * y.ofLp

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Algebra.UnitizationL1
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
r : 𝕜
⊢ Eq (α := Unitization 𝕜 A)
    (ofLp (p := 1) ((algebraMap 𝕜 (WithLp 1 (Unitization 𝕜 A)) : (a : 𝕜) → WithLp 1 (Unitization 𝕜 A)) r) :
      Unitization 𝕜 A)
    ((algebraMap 𝕜 (Unitization 𝕜 A) : (a : 𝕜) → Unitization 𝕜 A) r : Unitization 𝕜 A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Algebra.UnitizationL1
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)
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‖)
⊢ ‖x * y‖ ≤ ‖x‖ * ‖y‖

Tactic:
simp_rw [unitization_norm_def, add_mul, mul_add, unitization_mul, fst_mul, snd_mul]

Premises used: add_mul, Unitization.snd_mul, Unitization.fst_mul, WithLp.unitization_norm_def, mul_add, WithLp.unitization_mul
-- Module: Mathlib.Analysis.Normed.Algebra.UnitizationL1
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)
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‖))
⊢ ‖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]

Premises used: add_assoc
-- Module: Mathlib.Analysis.Normed.Algebra.UnitizationL1
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‖
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‖)
⊢ ‖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:
gcongr
-- Module: Mathlib.Analysis.Normed.Algebra.UnitizationL1
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.1‖

Tactic:
norm_mul_le _ _

Premises used: norm_mul_le
-- Module: Mathlib.Analysis.Normed.Algebra.UnitizationL1
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.1‖

Tactic:
exact norm_mul_le _ _

Premises used: norm_mul_le
-- Module: Mathlib.Analysis.Normed.Algebra.UnitizationL1
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‖ + ‖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‖)
⊢ ‖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

Premises used: norm_add_le, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Algebra.UnitizationL1
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‖
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‖
⊢ ‖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
-- Module: Mathlib.Analysis.Normed.Algebra.UnitizationL1
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‖ ≤ ‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.2‖

Tactic:
simp [norm_smul]

Premises used: norm_smul
-- Module: Mathlib.Analysis.Normed.Algebra.UnitizationL1
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₂ :
  ‖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‖
⊢ ‖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:
apply (norm_add_le _ _).trans

Premises used: norm_add_le, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Algebra.UnitizationL1
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₂ : ‖y.ofLp.toProd.1 • x.ofLp.toProd.2‖ ≤ ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.1‖
h₃ : ‖x.ofLp.toProd.2 * y.ofLp.toProd.2‖ ≤ ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.2‖
⊢ ‖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
-- Module: Mathlib.Analysis.Normed.Algebra.UnitizationL1
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)
⊢ ‖y.ofLp.toProd.1 • x.ofLp.toProd.2‖ ≤ ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.1‖

Tactic:
simp [norm_smul, mul_comm]

Premises used: norm_smul, mul_comm
-- Module: Mathlib.Analysis.Normed.Algebra.UnitizationL1
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.2 * y.ofLp.toProd.2‖ ≤ ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.2‖

Tactic:
norm_mul_le _ _

Premises used: norm_mul_le
-- Module: Mathlib.Analysis.Normed.Algebra.UnitizationL1
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.2 * y.ofLp.toProd.2‖ ≤ ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.2‖

Tactic:
exact norm_mul_le _ _

Premises used: norm_mul_le
-- Module: Mathlib.Analysis.Normed.Algebra.UnitizationL1
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
r : 𝕜
x : WithLp 1 (Unitization 𝕜 A)
simp_rw : ‖r‖ * ‖x.ofLp.toProd.1‖ + ‖r‖ * ‖x.ofLp.toProd.2‖ ≤ ‖r‖ * ‖x.ofLp.toProd.1‖ + ‖r‖ * ‖x.ofLp.toProd.2‖
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖

Tactic:
simp_rw [unitization_norm_def, ofLp_smul, fst_smul, snd_smul, norm_smul, mul_add]

Premises used: WithLp.ofLp_smul, norm_smul, WithLp.unitization_norm_def, mul_add, Unitization.fst_smul, Unitization.snd_smul
-- Module: Mathlib.Analysis.Normed.Algebra.UnitizationL1
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
r : 𝕜
x : WithLp 1 (Unitization 𝕜 A)
⊢ ‖r‖ * ‖x.ofLp.toProd.1‖ + ‖r‖ * ‖x.ofLp.toProd.2‖ ≤ ‖r‖ * ‖x.ofLp.toProd.1‖ + ‖r‖ * ‖x.ofLp.toProd.2‖

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Analysis.Normed.Algebra.UnitizationL1
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
r : 𝕜
x : WithLp 1 (Unitization 𝕜 A)
⊢ ‖r‖ * ‖x.ofLp.toProd.1‖ + ‖r‖ * ‖x.ofLp.toProd.2‖ ≤ ‖r‖ * ‖x.ofLp.toProd.1‖ + ‖r‖ * ‖x.ofLp.toProd.2‖

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.Analysis.Normed.Field.Approximation
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
this :
  Multiset.prod (Multiset.map (fun (x : K) ↦ ‖a - x‖) g.roots) <
    HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ)
by_contra! :
  ∀
    (h :
      ∀ (b : K) (_ : b ∈ g.roots),
        HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1 ≤ ‖a - b‖),
    False
⊢ ∃ b ∈ g.roots,
    ‖a - b‖ < HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1

Tactic:
by_contra! h
-- Module: Mathlib.Analysis.Normed.Field.Approximation
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
this :
  Multiset.prod (Multiset.map (fun (x : K) ↦ ‖a - x‖) g.roots) <
    HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ)
h :
  ∀ (b : K) (_ : b ∈ g.roots),
    HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1 ≤ ‖a - b‖
i : K
h_1 : i ∈ g.roots
⊢ LE.le (α := ℝ) 0
    ((fun (b : K) ↦ HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1)
      i)

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Field.Approximation
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
this :
  Multiset.prod (Multiset.map (fun (x : K) ↦ ‖a - x‖) g.roots) <
    HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ)
h :
  ∀ (b : K) (_ : b ∈ g.roots),
    HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1 ≤ ‖a - b‖
⊢ LE.le (α := ℝ)
    (Multiset.prod
      (Multiset.map
        (fun (b : K) ↦
          HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1)
        g.roots))
    (Multiset.prod (Multiset.map (fun (b : K) ↦ ‖a - b‖) g.roots))

Tactic:
have := Multiset.prod_map_le_prod_map₀ (fun b ↦ ((f.natDegree + 1) * ε) ^ (f.natDegree : ℝ)⁻¹ *
        (‖a‖ ⊔ 1)) (fun b ↦ ‖a - b‖) (by intros; positivity) h
-- Module: Mathlib.Analysis.Normed.Field.Approximation
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
this_1 :
  Multiset.prod (Multiset.map (fun (x : K) ↦ ‖a - x‖) g.roots) <
    HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ)
h :
  ∀ (b : K) (_ : b ∈ g.roots),
    HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1 ≤ ‖a - b‖
this :
  LE.le (α := ℝ)
    (Multiset.prod
      (Multiset.map
        (fun (b : K) ↦
          HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1)
        g.roots))
    (Multiset.prod (Multiset.map (fun (b : K) ↦ ‖a - b‖) g.roots))
⊢ HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε > 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Field.Approximation
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
this_1 :
  Multiset.prod (Multiset.map (fun (x : K) ↦ ‖a - x‖) g.roots) <
    HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ)
h :
  ∀ (b : K) (_ : b ∈ g.roots),
    HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1 ≤ ‖a - b‖
this :
  LE.le (α := ℝ)
    (Multiset.prod
      (Multiset.map
        (fun (b : K) ↦
          HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1)
        g.roots))
    (Multiset.prod (Multiset.map (fun (b : K) ↦ ‖a - b‖) g.roots))
⊢ (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) ^ HMul.hMul (α := ℝ) (↑f.natDegree : ℝ)⁻¹ (↑f.natDegree : ℝ) *
      HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ) ≤
    Multiset.prod (Multiset.map (fun (b : K) ↦ ‖a - b‖) g.roots)

Tactic:
simp only [Multiset.map_const', hg.natDegree_eq_card_roots.symm ▸ hdeg, Multiset.prod_replicate,
      mul_pow, ← Real.rpow_natCast,
      ← Real.rpow_mul (by positivity : ((f.natDegree + 1) * ε) > 0).le] at this

Premises used: Multiset.prod_replicate, LT.lt.le, Real.rpow_mul, mul_pow, Multiset.map_const', Real.rpow_natCast
-- Module: Mathlib.Analysis.Normed.Field.Approximation
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
this_1 :
  Multiset.prod (Multiset.map (fun (x : K) ↦ ‖a - x‖) g.roots) <
    HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ)
h :
  ∀ (b : K) (_ : b ∈ g.roots),
    HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1 ≤ ‖a - b‖
this :
  (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) ^ HMul.hMul (α := ℝ) (↑f.natDegree : ℝ)⁻¹ (↑f.natDegree : ℝ) *
      HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ) ≤
    Multiset.prod (Multiset.map (fun (b : K) ↦ ‖a - b‖) g.roots)
rw :
  ∀
    (this :
      HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ) ≤
        Multiset.prod (Multiset.map (fun (b : K) ↦ ‖a - b‖) g.roots)),
    False
rw₁ : Ne (α := ℝ) (↑f.natDegree : ℝ) 0
⊢ False

Tactic:
rw [inv_mul_cancel₀, Real.rpow_one] at this

Premises used: Real.rpow_one, inv_mul_cancel₀
-- Module: Mathlib.Analysis.Normed.Field.Approximation
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
this_1 :
  Multiset.prod (Multiset.map (fun (x : K) ↦ ‖a - x‖) g.roots) <
    HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ)
h :
  ∀ (b : K) (_ : b ∈ g.roots),
    HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1 ≤ ‖a - b‖
this :
  HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ) ≤
    Multiset.prod (Multiset.map (fun (b : K) ↦ ‖a - b‖) g.roots)
linarith :
  Multiset.prod (Multiset.map (fun (x : K) ↦ ‖a - x‖) g.roots) -
        HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ) +
      (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ) -
        Multiset.prod (Multiset.map (fun (b : K) ↦ ‖a - b‖) g.roots)) =
    0
⊢ False

Tactic:
linarith
-- Module: Mathlib.Analysis.Normed.Field.Approximation
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
this_1 :
  Multiset.prod (Multiset.map (fun (x : K) ↦ ‖a - x‖) g.roots) <
    HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ)
h :
  ∀ (b : K) (_ : b ∈ g.roots),
    HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1 ≤ ‖a - b‖
this :
  (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) ^ HMul.hMul (α := ℝ) (↑f.natDegree : ℝ)⁻¹ (↑f.natDegree : ℝ) *
      HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ) ≤
    Multiset.prod (Multiset.map (fun (b : K) ↦ ‖a - b‖) g.roots)
simp : ¬f = 1
⊢ Ne (α := ℝ) (↑f.natDegree : ℝ) 0

Tactic:
simp only [ne_eq, Nat.cast_eq_zero, hfm, Monic.natDegree_eq_zero]

Premises used: Polynomial.Monic.natDegree_eq_zero, ne_eq, Nat.cast_eq_zero