awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.Unitization
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
inst_7 : StarRing 𝕜
inst_8 : StarModule 𝕜 E
inst_9 : CStarRing 𝕜
x : Unitization 𝕜 E
h₁ :
  ∀ (x : Unitization 𝕜 E),
    norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2 ≤
      norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x⋆).2
refine :
  norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) (x⋆ * x)).2 ≤
    HPow.hPow (β := ℕ) (norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2) 2
⊢ norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) (x⋆ * x)).2 =
    HPow.hPow (β := ℕ) (norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2) 2

Tactic:
refine le_antisymm ?_ (norm_splitMul_snd_sq 𝕜 x)

Premises used: le_antisymm, Unitization.norm_splitMul_snd_sq
-- Module: Mathlib.Analysis.CStarAlgebra.Unitization
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
inst_7 : StarRing 𝕜
inst_8 : StarModule 𝕜 E
inst_9 : CStarRing 𝕜
x : Unitization 𝕜 E
h₁ :
  ∀ (x : Unitization 𝕜 E),
    norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2 ≤
      norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x⋆).2
rw :
  ‖HMul.hMul (α := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x⋆).2
        ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2‖ ≤
    HPow.hPow (β := ℕ) (norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2) 2
⊢ norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) (x⋆ * x)).2 ≤
    HPow.hPow (β := ℕ) (norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2) 2

Tactic:
rw [map_mul, Prod.snd_mul]

Premises used: Prod.snd_mul, map_mul
-- Module: Mathlib.Analysis.CStarAlgebra.Unitization
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
inst_7 : StarRing 𝕜
inst_8 : StarModule 𝕜 E
inst_9 : CStarRing 𝕜
x : Unitization 𝕜 E
h₁ :
  ∀ (x : Unitization 𝕜 E),
    norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2 ≤
      norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x⋆).2
rw :
  norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x⋆).2 *
      norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2 ≤
    norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2 *
      norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2
⊢ norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x⋆).2 *
      norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2 ≤
    HPow.hPow (β := ℕ) (norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2) 2

Tactic:
rw [sq]

Premises used: sq
-- Module: Mathlib.Analysis.CStarAlgebra.Unitization
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
inst_7 : StarRing 𝕜
inst_8 : StarModule 𝕜 E
inst_9 : CStarRing 𝕜
x : Unitization 𝕜 E
h₁ :
  ∀ (x : Unitization 𝕜 E),
    norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2 ≤
      norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x⋆).2
hbc :
  norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x⋆).2 ≤
    norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2
⊢ norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x⋆).2 *
      norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2 ≤
    norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2 *
      norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2

Tactic:
gcongr
-- Module: Mathlib.Analysis.CStarAlgebra.Unitization
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
inst_7 : StarRing 𝕜
inst_8 : StarModule 𝕜 E
inst_9 : CStarRing 𝕜
x : Unitization 𝕜 E
h₁ :
  ∀ (x : Unitization 𝕜 E),
    norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2 ≤
      norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x⋆).2
⊢ norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x⋆).2 ≤
    norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2

Tactic:
simpa only [star_star] using h₁ (star x)

Premises used: star_star, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.Unitization
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
inst_7 : StarRing 𝕜
inst_8 : StarModule 𝕜 E
inst_9 : CStarRing 𝕜
x : Unitization 𝕜 E
h₁ :
  ∀ (x : Unitization 𝕜 E),
    norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2 ≤
      norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x⋆).2
⊢ ‖HMul.hMul (α := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x⋆).2
        ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2‖ ≤
    HPow.hPow (β := ℕ) (norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2) 2

Tactic:
exact (norm_mul_le _ _).trans <| by
        rw [sq]
        gcongr
        simpa only [star_star] using h₁ (star x)

Premises used: LE.le.trans, norm_mul_le
-- Module: Mathlib.Analysis.CStarAlgebra.Unitization
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
inst_7 : StarRing 𝕜
inst_8 : StarModule 𝕜 E
inst_9 : CStarRing 𝕜
x : Unitization 𝕜 E
h₁ :
  ∀ (x : Unitization 𝕜 E),
    norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2 ≤
      norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x⋆).2
⊢ norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) (x⋆ * x)).2 =
    HPow.hPow (β := ℕ) (norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2) 2

Tactic:
have h₂ : ‖(Unitization.splitMul 𝕜 E (star x * x)).snd‖
        = ‖(Unitization.splitMul 𝕜 E x).snd‖ ^ 2 := by
      refine le_antisymm ?_ (norm_splitMul_snd_sq 𝕜 x)
      rw [map_mul, Prod.snd_mul]
      exact (norm_mul_le _ _).trans <| by
        rw [sq]
        gcongr
        simpa only [star_star] using h₁ (star x)
-- Module: Mathlib.Analysis.CStarAlgebra.Unitization
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
inst_7 : StarRing 𝕜
inst_8 : StarModule 𝕜 E
inst_9 : CStarRing 𝕜
x : Unitization 𝕜 E
h₁ :
  ∀ (x : Unitization 𝕜 E),
    norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2 ≤
      norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x⋆).2
h₂ :
  norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) (x⋆ * x)).2 =
    HPow.hPow (β := ℕ) (norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2) 2
⊢ norm.{u_1} (E := 𝕜) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) (x⋆ * x)).1 =
    HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).1) 2

Tactic:
simp only [Unitization.splitMul_apply, Unitization.fst_mul, Unitization.fst_star,
        norm_mul, norm_star, sq]

Premises used: norm_star, Unitization.splitMul_apply, Unitization.fst_mul, norm_mul, sq, Unitization.fst_star
-- Module: Mathlib.Analysis.CStarAlgebra.Unitization
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
inst_7 : StarRing 𝕜
inst_8 : StarModule 𝕜 E
inst_9 : CStarRing 𝕜
x : Unitization 𝕜 E
h₁ :
  ∀ (x : Unitization 𝕜 E),
    norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2 ≤
      norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x⋆).2
h₂ :
  norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) (x⋆ * x)).2 =
    HPow.hPow (β := ℕ) (norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2) 2
⊢ norm.{u_1} (E := 𝕜) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) (x⋆ * x)).1 =
    HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).1) 2

Tactic:
have h₃ : ‖(Unitization.splitMul 𝕜 E (star x * x)).fst‖
        = ‖(Unitization.splitMul 𝕜 E x).fst‖ ^ 2 := by
      simp only [Unitization.splitMul_apply, Unitization.fst_mul, Unitization.fst_star,
        norm_mul, norm_star, sq]
-- Module: Mathlib.Analysis.CStarAlgebra.Unitization
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
inst_7 : StarRing 𝕜
inst_8 : StarModule 𝕜 E
inst_9 : CStarRing 𝕜
x : Unitization 𝕜 E
h₁ :
  ∀ (x : Unitization 𝕜 E),
    norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2 ≤
      norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x⋆).2
h₂ :
  norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) (x⋆ * x)).2 =
    HPow.hPow (β := ℕ) (norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2) 2
h₃ :
  norm.{u_1} (E := 𝕜) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) (x⋆ * x)).1 =
    HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).1) 2
rw :
  max (norm.{u_1} (E := 𝕜) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).1)
        (norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2) *
      max (norm.{u_1} (E := 𝕜) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).1)
        (norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2) ≤
    max (HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).1) 2)
      (HPow.hPow (β := ℕ) (norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2)
        2)
⊢ max (norm.{u_1} (E := 𝕜) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).1)
        (norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2) *
      max (norm.{u_1} (E := 𝕜) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).1)
        (norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2) ≤
    max (norm.{u_1} (E := 𝕜) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) (x⋆ * x)).1)
      (norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) (x⋆ * x)).2)

Tactic:
rw [h₂, h₃]
-- Module: Mathlib.Analysis.CStarAlgebra.Unitization
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
inst_7 : StarRing 𝕜
inst_8 : StarModule 𝕜 E
inst_9 : CStarRing 𝕜
x : Unitization 𝕜 E
h₁ :
  ∀ (x : Unitization 𝕜 E),
    norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2 ≤
      norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x⋆).2
h₂ :
  norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) (x⋆ * x)).2 =
    HPow.hPow (β := ℕ) (norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2) 2
h₃ :
  norm.{u_1} (E := 𝕜) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) (x⋆ * x)).1 =
    HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).1) 2
h :
  norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2 <
    norm.{u_1} (E := 𝕜) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).1
⊢ norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2 ≤
    norm.{u_1} (E := 𝕜) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).1

Tactic:
replace h := h.le
-- Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone
Goal:
f : ℝ → ℝ
s : Set ℝ
hf : AbsolutelyMonotoneOn f s
obtain :
  ∀ (w : ℝ → FormalMultilinearSeries ℝ ℝ ℝ) (hp : HasFTaylorSeriesUpToOn ∞ f w s),
    (∀ (n : ℕ) ⦃x : ℝ⦄, x ∈ s → LE.le (α := ℝ) (0 : ℝ) ((w x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)) →
      ContDiffOn ℝ ∞ f s
⊢ ContDiffOn ℝ ∞ f s

Tactic:
obtain ⟨_, hp, _⟩ := hf
-- Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone
Goal:
f : ℝ → ℝ
s : Set ℝ
w : ℝ → FormalMultilinearSeries ℝ ℝ ℝ
hp : HasFTaylorSeriesUpToOn ∞ f w s
right : ∀ (n : ℕ) ⦃x : ℝ⦄, x ∈ s → LE.le (α := ℝ) (0 : ℝ) ((w x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)
⊢ ContDiffOn ℝ ∞ f s

Tactic:
hp.contDiffOn

Premises used: HasFTaylorSeriesUpToOn.contDiffOn
-- Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone
Goal:
f : ℝ → ℝ
s : Set ℝ
w : ℝ → FormalMultilinearSeries ℝ ℝ ℝ
hp : HasFTaylorSeriesUpToOn ∞ f w s
right : ∀ (n : ℕ) ⦃x : ℝ⦄, x ∈ s → LE.le (α := ℝ) (0 : ℝ) ((w x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)
⊢ ContDiffOn ℝ ∞ f s

Tactic:
exact hp.contDiffOn

Premises used: HasFTaylorSeriesUpToOn.contDiffOn
-- Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone
Goal:
f : ℝ → ℝ
s : Set ℝ
hf : ContDiff ℝ ∞ f
h : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ iteratedDeriv n f x
⊢ AbsolutelyMonotoneOn f s

Tactic:
⟨ftaylorSeries ℝ f, (hf.ftaylorSeries).hasFTaylorSeriesUpToOn s, fun n x hx => ?_⟩

Premises used: Real, AbsolutelyMonotoneOn, ftaylorSeries, HasFTaylorSeriesUpTo.hasFTaylorSeriesUpToOn, ContDiff.ftaylorSeries, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone
Goal:
f : ℝ → ℝ
s : Set ℝ
hf : ContDiff ℝ ∞ f
h : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ iteratedDeriv n f x
refine :
  ∀ (n : ℕ) (x : ℝ) (hx : x ∈ s),
    LE.le (α := ℝ) (0 : ℝ) ((ftaylorSeries ℝ f x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)
⊢ AbsolutelyMonotoneOn f s

Tactic:
refine ⟨ftaylorSeries ℝ f, (hf.ftaylorSeries).hasFTaylorSeriesUpToOn s, fun n x hx => ?_⟩
-- Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone
Goal:
f : ℝ → ℝ
s : Set ℝ
hf : ContDiff ℝ ∞ f
h : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ iteratedDeriv n f x
n : ℕ
x : ℝ
hx : x ∈ s
⊢ LE.le (α := ℝ) (0 : ℝ) ((ftaylorSeries ℝ f x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)

Tactic:
iteratedDeriv_eq_iteratedFDeriv (𝕜 := ℝ) (f := f) ▸ h n x hx

Premises used: Eq.rec, iteratedDeriv_eq_iteratedFDeriv
-- Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone
Goal:
f : ℝ → ℝ
s : Set ℝ
hf : ContDiff ℝ ∞ f
h : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ iteratedDeriv n f x
n : ℕ
x : ℝ
hx : x ∈ s
⊢ LE.le (α := ℝ) (0 : ℝ) ((ftaylorSeries ℝ f x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)

Tactic:
exact iteratedDeriv_eq_iteratedFDeriv (𝕜 := ℝ) (f := f) ▸ h n x hx
-- Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone
Goal:
f : ℝ → ℝ
s : Set ℝ
hf : AbsolutelyMonotoneOn f s
hs : UniqueDiffOn ℝ s
n : ℕ
x : ℝ
hx : x ∈ s
obtain :
  ∀ (p : ℝ → FormalMultilinearSeries ℝ ℝ ℝ) (hp : HasFTaylorSeriesUpToOn ∞ f p s)
    (hp_nn :
      ∀ (n : ℕ) ⦃x : ℝ⦄, x ∈ s → LE.le (α := ℝ) (0 : ℝ) ((p x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)),
    0 ≤ iteratedDerivWithin n f s x
⊢ 0 ≤ iteratedDerivWithin n f s x

Tactic:
obtain ⟨p, hp, hp_nn⟩ := hf
-- Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone
Goal:
f : ℝ → ℝ
s : Set ℝ
hs : UniqueDiffOn ℝ s
n : ℕ
x : ℝ
hx : x ∈ s
p : ℝ → FormalMultilinearSeries ℝ ℝ ℝ
hp : HasFTaylorSeriesUpToOn ∞ f p s
hp_nn : ∀ (n : ℕ) ⦃x : ℝ⦄, x ∈ s → LE.le (α := ℝ) (0 : ℝ) ((p x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)
⊢ p x n = iteratedFDerivWithin ℝ n f s x

Tactic:
have heq : p x n = iteratedFDerivWithin ℝ n f s x :=
    hp.eq_iteratedFDerivWithin_of_uniqueDiffOn (mod_cast le_top) hs hx
-- Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone
Goal:
f : ℝ → ℝ
s : Set ℝ
hs : UniqueDiffOn ℝ s
n : ℕ
x : ℝ
hx : x ∈ s
p : ℝ → FormalMultilinearSeries ℝ ℝ ℝ
hp : HasFTaylorSeriesUpToOn ∞ f p s
hp_nn : ∀ (n : ℕ) ⦃x : ℝ⦄, x ∈ s → LE.le (α := ℝ) (0 : ℝ) ((p x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)
heq : p x n = iteratedFDerivWithin ℝ n f s x
rw : LE.le (α := ℝ) (0 : ℝ) ((p x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)
⊢ 0 ≤ iteratedDerivWithin n f s x

Tactic:
rw [iteratedDerivWithin_eq_iteratedFDerivWithin, ← heq]

Premises used: iteratedDerivWithin_eq_iteratedFDerivWithin
-- Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone
Goal:
f : ℝ → ℝ
s : Set ℝ
hs : UniqueDiffOn ℝ s
n : ℕ
x : ℝ
hx : x ∈ s
p : ℝ → FormalMultilinearSeries ℝ ℝ ℝ
hp : HasFTaylorSeriesUpToOn ∞ f p s
hp_nn : ∀ (n : ℕ) ⦃x : ℝ⦄, x ∈ s → LE.le (α := ℝ) (0 : ℝ) ((p x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)
heq : p x n = iteratedFDerivWithin ℝ n f s x
⊢ LE.le (α := ℝ) (0 : ℝ) ((p x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)

Tactic:
hp_nn n hx
-- Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone
Goal:
f : ℝ → ℝ
s : Set ℝ
hs : UniqueDiffOn ℝ s
n : ℕ
x : ℝ
hx : x ∈ s
p : ℝ → FormalMultilinearSeries ℝ ℝ ℝ
hp : HasFTaylorSeriesUpToOn ∞ f p s
hp_nn : ∀ (n : ℕ) ⦃x : ℝ⦄, x ∈ s → LE.le (α := ℝ) (0 : ℝ) ((p x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)
heq : p x n = iteratedFDerivWithin ℝ n f s x
⊢ LE.le (α := ℝ) (0 : ℝ) ((p x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)

Tactic:
exact hp_nn n hx
-- Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone
Goal:
f : ℝ → ℝ
s : Set ℝ
hs : UniqueDiffOn ℝ s
⊢ AbsolutelyMonotoneOn f s ↔ ContDiffOn ℝ ∞ f s ∧ ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ iteratedDerivWithin n f s x

Tactic:
⟨fun hf => ⟨hf.contDiffOn, fun n x hx => hf.iteratedDerivWithin_nonneg hs n hx⟩, ?_⟩

Premises used: AbsolutelyMonotoneOn.contDiffOn, And.intro, Iff.intro, AbsolutelyMonotoneOn.iteratedDerivWithin_nonneg
-- Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone
Goal:
f : ℝ → ℝ
s : Set ℝ
hs : UniqueDiffOn ℝ s
refine : (ContDiffOn ℝ ∞ f s ∧ ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ iteratedDerivWithin n f s x) → AbsolutelyMonotoneOn f s
⊢ AbsolutelyMonotoneOn f s ↔ ContDiffOn ℝ ∞ f s ∧ ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ iteratedDerivWithin n f s x

Tactic:
refine ⟨fun hf => ⟨hf.contDiffOn, fun n x hx => hf.iteratedDerivWithin_nonneg hs n hx⟩, ?_⟩
-- Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone
Goal:
f : ℝ → ℝ
s : Set ℝ
hs : UniqueDiffOn ℝ s
hcont : ContDiffOn ℝ ∞ f s
hnn : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ iteratedDerivWithin n f s x
⊢ AbsolutelyMonotoneOn f s

Tactic:
⟨ftaylorSeriesWithin ℝ f s, hcont.ftaylorSeriesWithin hs, fun n x hx => ?_⟩

Premises used: Real, AbsolutelyMonotoneOn, ftaylorSeriesWithin, And.intro, Exists.intro, ContDiffOn.ftaylorSeriesWithin
-- Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone
Goal:
f : ℝ → ℝ
s : Set ℝ
hs : UniqueDiffOn ℝ s
hcont : ContDiffOn ℝ ∞ f s
hnn : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ iteratedDerivWithin n f s x
refine :
  ∀ (n : ℕ) (x : ℝ) (hx : x ∈ s),
    LE.le (α := ℝ) (0 : ℝ) ((ftaylorSeriesWithin ℝ f s x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)
⊢ AbsolutelyMonotoneOn f s

Tactic:
refine ⟨ftaylorSeriesWithin ℝ f s, hcont.ftaylorSeriesWithin hs, fun n x hx => ?_⟩
-- Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone
Goal:
f : ℝ → ℝ
s : Set ℝ
hs : UniqueDiffOn ℝ s
hcont : ContDiffOn ℝ ∞ f s
hnn : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ iteratedDerivWithin n f s x
n : ℕ
x : ℝ
hx : x ∈ s
⊢ LE.le (α := ℝ) (0 : ℝ) ((ftaylorSeriesWithin ℝ f s x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)

Tactic:
iteratedDerivWithin_eq_iteratedFDerivWithin (𝕜 := ℝ) (f := f) (s := s) ▸ hnn n x hx

Premises used: iteratedDerivWithin_eq_iteratedFDerivWithin, Eq.rec
-- Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone
Goal:
f : ℝ → ℝ
s : Set ℝ
hs : UniqueDiffOn ℝ s
hcont : ContDiffOn ℝ ∞ f s
hnn : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ iteratedDerivWithin n f s x
n : ℕ
x : ℝ
hx : x ∈ s
⊢ LE.le (α := ℝ) (0 : ℝ) ((ftaylorSeriesWithin ℝ f s x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)

Tactic:
exact iteratedDerivWithin_eq_iteratedFDerivWithin (𝕜 := ℝ) (f := f) (s := s) ▸ hnn n x hx
-- Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone
Goal:
f g : ℝ → ℝ
s : Set ℝ
hf : AbsolutelyMonotoneOn f s
hg : AbsolutelyMonotoneOn g s
obtain :
  ∀ (p : ℝ → FormalMultilinearSeries ℝ ℝ ℝ) (hp : HasFTaylorSeriesUpToOn ∞ f p s)
    (hp_nn :
      ∀ (n : ℕ) ⦃x : ℝ⦄, x ∈ s → LE.le (α := ℝ) (0 : ℝ) ((p x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)),
    AbsolutelyMonotoneOn (f + g) s
⊢ AbsolutelyMonotoneOn (f + g) s

Tactic:
obtain ⟨p, hp, hp_nn⟩ := hf
-- Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone
Goal:
f g : ℝ → ℝ
s : Set ℝ
hg : AbsolutelyMonotoneOn g s
p : ℝ → FormalMultilinearSeries ℝ ℝ ℝ
hp : HasFTaylorSeriesUpToOn ∞ f p s
hp_nn : ∀ (n : ℕ) ⦃x : ℝ⦄, x ∈ s → LE.le (α := ℝ) (0 : ℝ) ((p x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)
obtain :
  ∀ (q : ℝ → FormalMultilinearSeries ℝ ℝ ℝ) (hq : HasFTaylorSeriesUpToOn ∞ g q s)
    (hq_nn :
      ∀ (n : ℕ) ⦃x : ℝ⦄, x ∈ s → LE.le (α := ℝ) (0 : ℝ) ((q x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)),
    AbsolutelyMonotoneOn (f + g) s
⊢ AbsolutelyMonotoneOn (f + g) s

Tactic:
obtain ⟨q, hq, hq_nn⟩ := hg
-- Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone
Goal:
f g : ℝ → ℝ
s : Set ℝ
p : ℝ → FormalMultilinearSeries ℝ ℝ ℝ
hp : HasFTaylorSeriesUpToOn ∞ f p s
hp_nn : ∀ (n : ℕ) ⦃x : ℝ⦄, x ∈ s → LE.le (α := ℝ) (0 : ℝ) ((p x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)
q : ℝ → FormalMultilinearSeries ℝ ℝ ℝ
hq : HasFTaylorSeriesUpToOn ∞ g q s
hq_nn : ∀ (n : ℕ) ⦃x : ℝ⦄, x ∈ s → LE.le (α := ℝ) (0 : ℝ) ((q x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)
⊢ AbsolutelyMonotoneOn (f + g) s

Tactic:
⟨p + q, hp.add hq, fun n x hx => ?_⟩

Premises used: AbsolutelyMonotoneOn, HasFTaylorSeriesUpToOn.add, HAdd.hAdd, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone
Goal:
f g : ℝ → ℝ
s : Set ℝ
p : ℝ → FormalMultilinearSeries ℝ ℝ ℝ
hp : HasFTaylorSeriesUpToOn ∞ f p s
hp_nn : ∀ (n : ℕ) ⦃x : ℝ⦄, x ∈ s → LE.le (α := ℝ) (0 : ℝ) ((p x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)
q : ℝ → FormalMultilinearSeries ℝ ℝ ℝ
hq : HasFTaylorSeriesUpToOn ∞ g q s
hq_nn : ∀ (n : ℕ) ⦃x : ℝ⦄, x ∈ s → LE.le (α := ℝ) (0 : ℝ) ((q x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)
refine :
  ∀ (n : ℕ) (x : ℝ) (hx : x ∈ s),
    LE.le (α := ℝ) (0 : ℝ) (((p + q) x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)
⊢ AbsolutelyMonotoneOn (f + g) s

Tactic:
refine ⟨p + q, hp.add hq, fun n x hx => ?_⟩