awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
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
⊢ 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)
have pos : ∀
  (h :
    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).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)
Tactic: by_cases! h : ‖(Unitization.splitMul 𝕜 E x).fst‖ ≤ ‖(Unitization.splitMul 𝕜 E x).snd‖
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
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_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).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)
have pos : 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).1 *
      norm.{u_1} (E := 𝕜) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).1)
    (HPow.hPow (β := ℕ) (norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2) 2)
Tactic: rw [sq, sq, sup_eq_right.mpr h, sup_eq_right.mpr (mul_self_le_mul_self (norm_nonneg _) h)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (hypothesis)
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
⊢ 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)
have 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
Tactic: replace h := h.le
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
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
⊢ 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)
have neg : 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).1 *
      norm.{u_1} (E := 𝕜) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).1)
    (HPow.hPow (β := ℕ) (norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2) 2)
Tactic: rw [sq, sq, sup_eq_left.mpr h, sup_eq_left.mpr (mul_self_le_mul_self (norm_nonneg _) h)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.AbsolutelyMonotone (goal)
Goal:
f : ℝ → ℝ
s : Set ℝ
hf : AbsolutelyMonotoneOn f s
⊢ ContDiffOn ℝ ∞ f s
have 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
Tactic: obtain ⟨_, hp, _⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.AbsolutelyMonotone (goal)
Goal:
f : ℝ → ℝ
s : Set ℝ
hf : ContDiff ℝ ∞ f
h : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ iteratedDeriv n f x
⊢ AbsolutelyMonotoneOn f s
have refine : ∀ (n : ℕ) (x : ℝ) (hx : x ∈ s),
  LE.le (α := ℝ) (0 : ℝ) ((ftaylorSeries ℝ f x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)
Tactic: refine ⟨ftaylorSeries ℝ f, (hf.ftaylorSeries).hasFTaylorSeriesUpToOn s, fun n x hx => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.AbsolutelyMonotone (goal)
Goal:
f : ℝ → ℝ
s : Set ℝ
hf : AbsolutelyMonotoneOn f s
hs : UniqueDiffOn ℝ s
n : ℕ
x : ℝ
hx : x ∈ s
⊢ 0 ≤ iteratedDerivWithin n f s x
have 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
Tactic: obtain ⟨p, hp, hp_nn⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.AbsolutelyMonotone (hypothesis)
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 : ℝ)
⊢ 0 ≤ iteratedDerivWithin n f s x
have heq : 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.AbsolutelyMonotone (goal)
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
⊢ 0 ≤ iteratedDerivWithin n f s x
have rw : LE.le (α := ℝ) (0 : ℝ) ((p x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)
Tactic: rw [iteratedDerivWithin_eq_iteratedFDerivWithin, ← heq]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.AbsolutelyMonotone (goal)
Goal:
f : ℝ → ℝ
s : Set ℝ
hs : UniqueDiffOn ℝ s
⊢ AbsolutelyMonotoneOn f s ↔ ContDiffOn ℝ ∞ f s ∧ ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ iteratedDerivWithin n f s x
have refine : (ContDiffOn ℝ ∞ f s ∧ ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ iteratedDerivWithin n f s x) → AbsolutelyMonotoneOn f s
Tactic: refine ⟨fun hf => ⟨hf.contDiffOn, fun n x hx => hf.iteratedDerivWithin_nonneg hs n hx⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.AbsolutelyMonotone (goal)
Goal:
f : ℝ → ℝ
s : Set ℝ
hs : UniqueDiffOn ℝ s
hcont : ContDiffOn ℝ ∞ f s
hnn : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ iteratedDerivWithin n f s x
⊢ AbsolutelyMonotoneOn f s
have refine : ∀ (n : ℕ) (x : ℝ) (hx : x ∈ s),
  LE.le (α := ℝ) (0 : ℝ) ((ftaylorSeriesWithin ℝ f s x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)
Tactic: refine ⟨ftaylorSeriesWithin ℝ f s, hcont.ftaylorSeriesWithin hs, fun n x hx => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.AbsolutelyMonotone (goal)
Goal:
f g : ℝ → ℝ
s : Set ℝ
hf : AbsolutelyMonotoneOn f s
hg : AbsolutelyMonotoneOn g s
⊢ AbsolutelyMonotoneOn (f + g) s
have 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
Tactic: obtain ⟨p, hp, hp_nn⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.AbsolutelyMonotone (goal)
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 : ℝ)
⊢ AbsolutelyMonotoneOn (f + g) s
have 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
Tactic: obtain ⟨q, hq, hq_nn⟩ := hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.Calculus.AbsolutelyMonotone (goal)
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
have refine : ∀ (n : ℕ) (x : ℝ) (hx : x ∈ s),
  LE.le (α := ℝ) (0 : ℝ) (((p + q) x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)
Tactic: refine ⟨p + q, hp.add hq, fun n x hx => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.AbsolutelyMonotone (goal)
Goal:
f : ℝ → ℝ
s : Set ℝ
c : ℝ
hf : AbsolutelyMonotoneOn f s
hc : 0 ≤ c
⊢ AbsolutelyMonotoneOn (c • f) s
have 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 (c • f) s
Tactic: obtain ⟨p, hp, hp_nn⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.AbsolutelyMonotone (hypothesis)
Goal:
f : ℝ → ℝ
s : Set ℝ
c : ℝ
hc : 0 ≤ c
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 (c • f) s
have hT : let T := HSMul.hSMul (β := ℝ →L[ℝ] ℝ) c (ContinuousLinearMap.id ℝ ℝ);
T = HSMul.hSMul (β := ℝ →L[ℝ] ℝ) c (ContinuousLinearMap.id ℝ ℝ)
Tactic: set T : ℝ →L[ℝ] ℝ := c • ContinuousLinearMap.id ℝ ℝ with hT
-- Lean 4 proof step from Mathlib.Analysis.Calculus.AbsolutelyMonotone (goal)
Goal:
f : ℝ → ℝ
s : Set ℝ
c : ℝ
hc : 0 ≤ c
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 : ℝ)
T : ℝ →L[ℝ] ℝ := HSMul.hSMul (β := ℝ →L[ℝ] ℝ) c (ContinuousLinearMap.id ℝ ℝ)
hT : T = HSMul.hSMul (β := ℝ →L[ℝ] ℝ) c (ContinuousLinearMap.id ℝ ℝ)
⊢ (⇑T : (a : ℝ) → ℝ) ∘ f = c • f
have h : ∀ (x : ℝ), ((⇑T : (a : ℝ) → ℝ) ∘ f) x = (c • f) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.AbsolutelyMonotone (hypothesis)
Goal:
f : ℝ → ℝ
s : Set ℝ
c : ℝ
hc : 0 ≤ c
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 : ℝ)
T : ℝ →L[ℝ] ℝ := HSMul.hSMul (β := ℝ →L[ℝ] ℝ) c (ContinuousLinearMap.id ℝ ℝ)
hT : T = HSMul.hSMul (β := ℝ →L[ℝ] ℝ) c (ContinuousLinearMap.id ℝ ℝ)
⊢ AbsolutelyMonotoneOn (c • f) s
have hcomp : (⇑T : (a : ℝ) → ℝ) ∘ f = c • f
Tactic: have hcomp : (T ∘ f) = c • f := by ext x; simp [hT, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.AbsolutelyMonotone (goal)
Goal:
f : ℝ → ℝ
s : Set ℝ
c : ℝ
hc : 0 ≤ c
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 : ℝ)
T : ℝ →L[ℝ] ℝ := HSMul.hSMul (β := ℝ →L[ℝ] ℝ) c (ContinuousLinearMap.id ℝ ℝ)
hT : T = HSMul.hSMul (β := ℝ →L[ℝ] ℝ) c (ContinuousLinearMap.id ℝ ℝ)
hcomp : (⇑T : (a : ℝ) → ℝ) ∘ f = c • f
⊢ AbsolutelyMonotoneOn (c • f) s
have refine : ∀ (n : ℕ) (x : ℝ) (hx : x ∈ s),
  LE.le (α := ℝ) (0 : ℝ)
    ((T.compContinuousMultilinearMap (M₁ := fun (i : Fin n) ↦ ℝ) (p x n) : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦
        1 :
      ℝ)
Tactic: refine ⟨_, hcomp ▸ hp.continuousLinearMap_comp T, fun n x hx => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.AbsolutelyMonotone (goal)
Goal:
f : ℝ → ℝ
s : Set ℝ
c : ℝ
hc : 0 ≤ c
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 : ℝ)
T : ℝ →L[ℝ] ℝ := HSMul.hSMul (β := ℝ →L[ℝ] ℝ) c (ContinuousLinearMap.id ℝ ℝ)
hT : T = HSMul.hSMul (β := ℝ →L[ℝ] ℝ) c (ContinuousLinearMap.id ℝ ℝ)
hcomp : (⇑T : (a : ℝ) → ℝ) ∘ f = c • f
n : ℕ
x : ℝ
hx : x ∈ s
⊢ LE.le (α := ℝ) (0 : ℝ)
    ((T.compContinuousMultilinearMap (M₁ := fun (i : Fin n) ↦ ℝ) (p x n) : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦
        1 :
      ℝ)
have simp : 0 ≤ HMul.hMul (β := ℝ) c ((p x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)
Tactic: simp only [ContinuousLinearMap.compContinuousMultilinearMap_coe, Function.comp_apply, hT,
    ContinuousLinearMap.smul_apply, ContinuousLinearMap.id_apply, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.AddTorsor.AffineMap (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : NormedAddCommGroup W
inst_4 : NormedSpace 𝕜 W
n : WithTop ℕ∞
f : V →ᴬ[𝕜] W
⊢ ContDiff.{u_1, u_2, u_3} 𝕜 (E := V) (F := W) n (⇑f : (a : V) → W)
have rw : ContDiff 𝕜 n
  (HAdd.hAdd (α := (a : V) → W) (β := V → W) ((⇑f.contLinear : (a : V) → W) : (a : V) → W)
    (Function.const V ((f : (a : V) → W) 0) : V → W))
Tactic: rw [f.decomp]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.AddTorsor.AffineMap (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : NormedAddCommGroup W
inst_4 : NormedSpace 𝕜 W
n : WithTop ℕ∞
f : V →ᴬ[𝕜] W
⊢ ContDiff 𝕜 n
    (HAdd.hAdd (α := (a : V) → W) (β := V → W) ((⇑f.contLinear : (a : V) → W) : (a : V) → W)
      (Function.const V ((f : (a : V) → W) 0) : V → W))
have apply : ContDiff.{u_1, u_2, u_3} 𝕜 (F := W) n (Function.const V ((f : (a : V) → W) 0) : V → W)
Tactic: apply f.contLinear.contDiff.add
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Basic (goal)
Goal:
E : Type u_1
c : E
f : ContDiffBump c
⊢ 1 < f.rOut / f.rIn
have rw : f.rIn < f.rOut
Tactic: rw [one_lt_div f.rIn_pos]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
f : ContDiffBump.{u_1} (E := E) 0
x : E
⊢ (↑f : E → ℝ) (-x) = (↑f : E → ℝ) x
have simp_rw : (↑f : E → ℝ) (0 - x) = (↑f : E → ℝ) x
Tactic: simp_rw [← zero_sub, f.sub, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
f : ContDiffBump.{u_1} (E := E) 0
x : E
simp_rw : (↑f : E → ℝ) (0 - x) = (↑f : E → ℝ) x
⊢ (↑f : E → ℝ) (-x) = (↑f : E → ℝ) x
have simp_rw₁ : (↑f : E → ℝ) (0 + x) = (↑f : E → ℝ) x
Tactic: simp_rw [← zero_sub, f.sub, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
hx : x ∈ closedBall c f.rIn
⊢ (↑f : E → ℝ) x = 1
have a : norm.{u_1} (E := E) ((fun (x : E) ↦ f.rIn⁻¹ • (x - c)) x) ≤ 1
Tactic: apply ContDiffBumpBase.eq_one _ _ f.one_lt_rOut_div_rIn
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
c : E
f : ContDiffBump c
⊢ support (↑f : E → ℝ) = ball c f.rOut
have simp : preimage (β := E) (fun (x : E) ↦ f.rIn⁻¹ • (x - c)) (ball 0 (f.rOut / f.rIn)) = ball c f.rOut
Tactic: simp only [toFun, support_comp_eq_preimage, ContDiffBumpBase.support _ _ f.one_lt_rOut_div_rIn]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
c : E
f : ContDiffBump c
⊢ preimage (β := E) (fun (x : E) ↦ f.rIn⁻¹ • (x - c)) (ball 0 (f.rOut / f.rIn)) = ball c f.rOut
have h : ∀ (x : E),
  Membership.mem (γ := Set E) (preimage (β := E) (fun (x : E) ↦ f.rIn⁻¹ • (x - c)) (ball 0 (f.rOut / f.rIn))) x ↔
    x ∈ ball c f.rOut
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
c : E
f : ContDiffBump c
⊢ tsupport (↑f : E → ℝ) = closedBall c f.rOut
have simp_rw : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (support (↑f : E → ℝ)) = closedBall c f.rOut
Tactic: simp_rw [tsupport, f.support_eq, closure_ball _ f.rOut_pos.ne']
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
c : E
f : ContDiffBump c
simp_rw : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (support (↑f : E → ℝ)) = closedBall c f.rOut
⊢ tsupport (↑f : E → ℝ) = closedBall c f.rOut
have simp_rw₁ : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball c f.rOut) = closedBall c f.rOut
Tactic: simp_rw [tsupport, f.support_eq, closure_ball _ f.rOut_pos.ne']
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
hx : x ∈ ball c f.rOut
⊢ (↑f : E → ℝ) x ≠ 0
have rwa : ∀ (hx : x ∈ support (↑f : E → ℝ)), (↑f : E → ℝ) x ≠ 0
Tactic: rwa [← support_eq, mem_support] at hx
Cleared hypotheses: hx