awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℝ)
n : ℕ
x : ℝ
hx : x ∈ s
⊢ 0 ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((p x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)
      ((q x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)

Tactic:
add_nonneg (hp_nn n hx) (hq_nn n hx)

Premises used: add_nonneg
-- 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 : ℝ)
n : ℕ
x : ℝ
hx : x ∈ s
⊢ 0 ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((p x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)
      ((q x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)

Tactic:
exact add_nonneg (hp_nn n hx) (hq_nn n hx)

Premises used: add_nonneg
-- Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone
Goal:
f : ℝ → ℝ
s : Set ℝ
c : ℝ
hf : AbsolutelyMonotoneOn f s
hc : 0 ≤ c
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
⊢ AbsolutelyMonotoneOn (c • f) s

Tactic:
obtain ⟨p, hp, hp_nn⟩ := hf
-- Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone
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 : ℝ)
⊢ let T := HSMul.hSMul (β := ℝ →L[ℝ] ℝ) c (ContinuousLinearMap.id ℝ ℝ);
  T = HSMul.hSMul (β := ℝ →L[ℝ] ℝ) c (ContinuousLinearMap.id ℝ ℝ)

Tactic:
set T : ℝ →L[ℝ] ℝ := c • ContinuousLinearMap.id ℝ ℝ with hT

Premises used: Real, ContinuousLinearMap.id
-- Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone
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 ℝ ℝ)
h : ∀ (x : ℝ), ((⇑T : (a : ℝ) → ℝ) ∘ f) x = (c • f) x
⊢ (⇑T : (a : ℝ) → ℝ) ∘ f = c • f

Tactic:
ext x
-- Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone
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 ℝ ℝ)
x : ℝ
⊢ ((⇑T : (a : ℝ) → ℝ) ∘ f) x = (c • f) x

Tactic:
simp [hT, smul_eq_mul]

Premises used: smul_eq_mul
-- Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone
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

Tactic:
have hcomp : (T ∘ f) = c • f := by ext x; simp [hT, smul_eq_mul]
-- Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone
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

Tactic:
⟨_, hcomp ▸ hp.continuousLinearMap_comp T, fun n x hx => ?_⟩

Premises used: AbsolutelyMonotoneOn, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone
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
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 :
        ℝ)
⊢ AbsolutelyMonotoneOn (c • f) s

Tactic:
refine ⟨_, hcomp ▸ hp.continuousLinearMap_comp T, fun n x hx => ?_⟩
-- Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone
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
simp : 0 ≤ HMul.hMul (β := ℝ) c ((p x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)
⊢ LE.le (α := ℝ) (0 : ℝ)
    ((T.compContinuousMultilinearMap (M₁ := fun (i : Fin n) ↦ ℝ) (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]

Premises used: ContinuousLinearMap.smul_apply, ContinuousLinearMap.id_apply, ContinuousLinearMap.compContinuousMultilinearMap_coe, Function.comp_apply, smul_eq_mul
-- Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone
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
⊢ 0 ≤ HMul.hMul (β := ℝ) c ((p x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)

Tactic:
mul_nonneg hc (hp_nn n hx)

Premises used: mul_nonneg
-- Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone
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
⊢ 0 ≤ HMul.hMul (β := ℝ) c ((p x n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)

Tactic:
exact mul_nonneg hc (hp_nn n hx)

Premises used: mul_nonneg
-- Module: Mathlib.Analysis.Calculus.AddTorsor.AffineMap
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
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))
⊢ ContDiff.{u_1, u_2, u_3} 𝕜 (E := V) (F := W) n (⇑f : (a : V) → W)

Tactic:
rw [f.decomp]

Premises used: ContinuousAffineMap.decomp
-- Module: Mathlib.Analysis.Calculus.AddTorsor.AffineMap
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
apply : ContDiff.{u_1, u_2, u_3} 𝕜 (F := W) n (Function.const V ((f : (a : V) → W) 0) : 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))

Tactic:
apply f.contLinear.contDiff.add

Premises used: ContinuousAffineMap.contLinear, ContDiff.add, ContinuousLinearMap.contDiff
-- Module: Mathlib.Analysis.Calculus.AddTorsor.AffineMap
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} 𝕜 (F := W) n (Function.const V ((f : (a : V) → W) 0) : V → W)

Tactic:
contDiff_const

Premises used: contDiff_const
-- Module: Mathlib.Analysis.Calculus.AddTorsor.AffineMap
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} 𝕜 (F := W) n (Function.const V ((f : (a : V) → W) 0) : V → W)

Tactic:
exact contDiff_const

Premises used: contDiff_const
-- Module: Mathlib.Analysis.Calculus.AddTorsor.Coord
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : FiniteDimensional 𝕜 E
b : AffineBasis ι 𝕜 E
i : ι
⊢ ContDiff.{u_2, u_3, u_2} 𝕜 (E := E) (F := 𝕜) ⊤ (⇑(b.coord i) : (a : E) → 𝕜)

Tactic:
(⟨b.coord i, continuous_barycentric_coord b i⟩ : E →ᴬ[𝕜] 𝕜).contDiff

Premises used: ContinuousAffineMap.mk, AffineBasis.coord, ContinuousAffineMap.contDiff, continuous_barycentric_coord
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
Goal:
E : Type u_1
c : E
f : ContDiffBump c
⊢ 0 < f.rOut

Tactic:
f.rIn_pos.trans f.rIn_lt_rOut

Premises used: ContDiffBump.rIn_lt_rOut, LT.lt.trans, ContDiffBump.rIn_pos
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
Goal:
E : Type u_1
c : E
f : ContDiffBump c
rw : f.rIn < f.rOut
⊢ 1 < f.rOut / f.rIn

Tactic:
rw [one_lt_div f.rIn_pos]

Premises used: one_lt_div, ContDiffBump.rIn_pos
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
Goal:
E : Type u_1
c : E
f : ContDiffBump c
⊢ f.rIn < f.rOut

Tactic:
f.rIn_lt_rOut

Premises used: ContDiffBump.rIn_lt_rOut
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
Goal:
E : Type u_1
c : E
f : ContDiffBump c
⊢ f.rIn < f.rOut

Tactic:
exact f.rIn_lt_rOut

Premises used: ContDiffBump.rIn_lt_rOut
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
⊢ (↑f : E → ℝ) x = ContDiffBumpBase.toFun (someContDiffBumpBase E) (f.rOut / f.rIn) (f.rIn⁻¹ • (x - c))

Tactic:
rfl

Premises used: ContDiffBump.toFun, rfl
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
⊢ (↑f : E → ℝ) (c - x) = (↑f : E → ℝ) (c + x)

Tactic:
simp [f.apply, ContDiffBumpBase.symmetric]

Premises used: ContDiffBump.apply, ContDiffBumpBase.symmetric
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
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
simp_rw₁ : (↑f : E → ℝ) (0 + x) = (↑f : E → ℝ) x
⊢ (↑f : E → ℝ) (-x) = (↑f : E → ℝ) x

Tactic:
simp_rw [← zero_sub, f.sub, zero_add]

Premises used: zero_add, zero_sub, ContDiffBump.sub
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
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
a : norm.{u_1} (E := E) ((fun (x : E) ↦ f.rIn⁻¹ • (x - c)) x) ≤ 1
⊢ (↑f : E → ℝ) x = 1

Tactic:
apply ContDiffBumpBase.eq_one _ _ f.one_lt_rOut_div_rIn

Premises used: ContDiffBump.one_lt_rOut_div_rIn, ContDiffBumpBase.eq_one
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
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
⊢ norm.{u_1} (E := E) ((fun (x : E) ↦ f.rIn⁻¹ • (x - c)) x) ≤ 1

Tactic:
simpa only [norm_smul, Real.norm_eq_abs, abs_inv, abs_of_nonneg f.rIn_pos.le, ← div_eq_inv_mul,
    div_le_one f.rIn_pos] using mem_closedBall_iff_norm.1 hx

Premises used: norm_smul, abs_inv, mem_closedBall_iff_norm, LT.lt.le, div_le_one, Iff.mp, abs_of_nonneg, div_eq_inv_mul, ContDiffBump.rIn_pos, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
⊢ 0 ≤ (↑f : E → ℝ) x

Tactic:
(ContDiffBumpBase.mem_Icc (someContDiffBumpBase E) _ _).1

Premises used: someContDiffBumpBase, ContDiffBumpBase.mem_Icc, And.left, ContDiffBump.toFun
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
⊢ 0 ≤ (↑f : E → ℝ) x

Tactic:
f.nonneg

Premises used: ContDiffBump.nonneg
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
⊢ (↑f : E → ℝ) x ≤ 1

Tactic:
(ContDiffBumpBase.mem_Icc (someContDiffBumpBase E) _ _).2

Premises used: someContDiffBumpBase, ContDiffBumpBase.mem_Icc, And.right, ContDiffBump.toFun
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
c : E
f : ContDiffBump c
simp : preimage (β := E) (fun (x : E) ↦ f.rIn⁻¹ • (x - c)) (ball 0 (f.rOut / f.rIn)) = ball c f.rOut
⊢ support (↑f : E → ℝ) = ball c f.rOut

Tactic:
simp only [toFun, support_comp_eq_preimage, ContDiffBumpBase.support _ _ f.one_lt_rOut_div_rIn]

Premises used: ContDiffBump.one_lt_rOut_div_rIn, ContDiffBumpBase.support, Function.support_comp_eq_preimage, ContDiffBump.toFun
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
c : E
f : ContDiffBump c
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
⊢ preimage (β := E) (fun (x : E) ↦ f.rIn⁻¹ • (x - c)) (ball 0 (f.rOut / f.rIn)) = ball c f.rOut

Tactic:
ext x
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
c : E
f : ContDiffBump c
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:
simp only [mem_ball_iff_norm, sub_zero, norm_smul, mem_preimage, Real.norm_eq_abs, abs_inv,
    abs_of_pos f.rIn_pos, ← div_eq_inv_mul, div_lt_div_iff_of_pos_right f.rIn_pos]

Premises used: norm_smul, sub_zero, div_lt_div_iff_of_pos_right, abs_inv, mem_ball_iff_norm, abs_of_pos, div_eq_inv_mul, ContDiffBump.rIn_pos, Real.norm_eq_abs, Set.mem_preimage
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
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
simp_rw₁ : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball c f.rOut) = closedBall c f.rOut
⊢ tsupport (↑f : E → ℝ) = closedBall c f.rOut

Tactic:
simp_rw [tsupport, f.support_eq, closure_ball _ f.rOut_pos.ne']

Premises used: tsupport, ContDiffBump.support_eq, LT.lt.ne', closure_ball, ContDiffBump.rOut_pos
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
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
rwa : ∀ (hx : x ∈ support (↑f : E → ℝ)), (↑f : E → ℝ) x ≠ 0
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (hx : (↑f : E → ℝ) x ≠ 0), (↑f : E → ℝ) x ≠ 0
⊢ (↑f : E → ℝ) x ≠ 0

Tactic:
rwa [← support_eq, mem_support] at hx

Premises used: ContDiffBump.support_eq, Function.mem_support
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
hx : f.rOut ≤ dist x c
rwa : x ∉ support (↑f : E → ℝ)
rwa₁ : x ∉ ball c f.rOut
rwa₂ : ¬dist x c < f.rOut
rwa₃ rwa₄ rwa₅ rwa₆ : f.rOut ≤ dist x c
⊢ (↑f : E → ℝ) x = 0

Tactic:
rwa [← notMem_support, support_eq, mem_ball, not_lt]

Premises used: ContDiffBump.support_eq, Metric.mem_ball, Function.notMem_support, not_lt
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
c : E
f : ContDiffBump c
inst_3 : FiniteDimensional ℝ E
simp_rw : IsCompact (tsupport (↑f : E → ℝ))
simp_rw₁ : IsCompact (closedBall c f.rOut)
⊢ HasCompactSupport (↑f : E → ℝ)

Tactic:
simp_rw [HasCompactSupport, f.tsupport_eq, isCompact_closedBall]

Premises used: ContDiffBump.tsupport_eq, ProperSpace.isCompact_closedBall, HasCompactSupport
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
h : x ∈ ball c f.rIn
⊢ (↑f : E → ℝ) =ᶠ[𝓝 x] 1

Tactic:
mem_of_superset (closedBall_mem_nhds_of_mem h) fun _ ↦ f.one_of_mem_closedBall

Premises used: Filter.Eventually, Metric.closedBall_mem_nhds_of_mem, Filter.EventuallyEq, ContDiffBump.one_of_mem_closedBall, Filter.mem_of_superset
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
c : E
f : ContDiffBump c
⊢ (↑f : E → ℝ) =ᶠ[𝓝 c] 1

Tactic:
f.eventuallyEq_one_of_mem_ball (mem_ball_self f.rIn_pos)

Premises used: Metric.mem_ball_self, ContDiffBump.eventuallyEq_one_of_mem_ball, ContDiffBump.rIn_pos
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup X
inst_3 : NormedSpace ℝ X
inst_4 : HasContDiffBump E
n : ℕ∞
c g : X → E
s : Set X
f : (x : X) → ContDiffBump (c x)
x : X
hc : ContDiffWithinAt ℝ (↑n : ℕ∞ω) c s x
hr : ContDiffWithinAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : X) ↦ (f x).rIn) s x
hR : ContDiffWithinAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : X) ↦ (f x).rOut) s x
hg : ContDiffWithinAt ℝ (↑n : ℕ∞ω) g s x
change :
  ContDiffWithinAt ℝ (↑n : ℕ∞ω)
    (uncurry (ContDiffBumpBase.toFun (someContDiffBumpBase E)) ∘ fun (x : X) ↦
      ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x)))
    s x
⊢ ContDiffWithinAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : X) ↦ (↑(f x) : E → ℝ) (g x)) s x

Tactic:
change ContDiffWithinAt ℝ n (uncurry (someContDiffBumpBase E).toFun ∘ fun x : X =>
    ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))) s x

Premises used: Real, someContDiffBumpBase, HSub.hSub, Function.comp, ContDiffBumpBase.toFun, HDiv.hDiv, Prod.mk, WithTop.some, Inv.inv, ContDiffBump.rOut, HSMul.hSMul, ContDiffBump.rIn, ContDiffWithinAt, Function.uncurry
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup X
inst_3 : NormedSpace ℝ X
inst_4 : HasContDiffBump E
n : ℕ∞
c g : X → E
s : Set X
f : (x : X) → ContDiffBump (c x)
x : X
hc : ContDiffWithinAt ℝ (↑n : ℕ∞ω) c s x
hr : ContDiffWithinAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : X) ↦ (f x).rIn) s x
hR : ContDiffWithinAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : X) ↦ (f x).rOut) s x
hg : ContDiffWithinAt ℝ (↑n : ℕ∞ω) g s x
⊢ ContDiffWithinAt ℝ (↑n : ℕ∞ω)
    (uncurry (ContDiffBumpBase.toFun (someContDiffBumpBase E)) ∘ fun (x : X) ↦
      ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x)))
    s x

Tactic:
(((someContDiffBumpBase E).smooth.contDiffAt ?_).of_le
    (mod_cast le_top)).comp_contDiffWithinAt x ?_

Premises used: ContDiffBumpBase.smooth, someContDiffBumpBase, ContDiffAt.comp_contDiffWithinAt, ContDiffOn.contDiffAt, ContDiffAt.of_le
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup X
inst_3 : NormedSpace ℝ X
inst_4 : HasContDiffBump E
n : ℕ∞
c g : X → E
s : Set X
f : (x : X) → ContDiffBump (c x)
x : X
hc : ContDiffWithinAt ℝ (↑n : ℕ∞ω) c s x
hr : ContDiffWithinAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : X) ↦ (f x).rIn) s x
hR : ContDiffWithinAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : X) ↦ (f x).rOut) s x
hg : ContDiffWithinAt ℝ (↑n : ℕ∞ω) g s x
refine_1 : SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ ∈ 𝓝 ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))
refine_2 :
  ContDiffWithinAt.{0, u_2, u_1} ℝ (F := ℝ × E) (↑n : ℕ∞ω)
    (fun (x : X) ↦ ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))) s x
⊢ ContDiffWithinAt ℝ (↑n : ℕ∞ω)
    (uncurry (ContDiffBumpBase.toFun (someContDiffBumpBase E)) ∘ fun (x : X) ↦
      ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x)))
    s x

Tactic:
refine (((someContDiffBumpBase E).smooth.contDiffAt ?_).of_le
    (mod_cast le_top)).comp_contDiffWithinAt x ?_

Premises used: ContDiffBumpBase.smooth, someContDiffBumpBase, ContDiffAt.comp_contDiffWithinAt, ContDiffOn.contDiffAt, ContDiffAt.of_le
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup X
inst_3 : NormedSpace ℝ X
inst_4 : HasContDiffBump E
n : ℕ∞
c g : X → E
s : Set X
f : (x : X) → ContDiffBump (c x)
x : X
hc : ContDiffWithinAt ℝ (↑n : ℕ∞ω) c s x
hr : ContDiffWithinAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : X) ↦ (f x).rIn) s x
hR : ContDiffWithinAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : X) ↦ (f x).rOut) s x
hg : ContDiffWithinAt ℝ (↑n : ℕ∞ω) g s x
⊢ SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ ∈ 𝓝 ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))

Tactic:
prod_mem_nhds (Ioi_mem_nhds (f x).one_lt_rOut_div_rIn) univ_mem

Premises used: prod_mem_nhds, Ioi_mem_nhds, Set.Mem, ContDiffBump.one_lt_rOut_div_rIn, setOf, Filter.univ_mem
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Basic
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup X
inst_3 : NormedSpace ℝ X
inst_4 : HasContDiffBump E
n : ℕ∞
c g : X → E
s : Set X
f : (x : X) → ContDiffBump (c x)
x : X
hc : ContDiffWithinAt ℝ (↑n : ℕ∞ω) c s x
hr : ContDiffWithinAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : X) ↦ (f x).rIn) s x
hR : ContDiffWithinAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : X) ↦ (f x).rOut) s x
hg : ContDiffWithinAt ℝ (↑n : ℕ∞ω) g s x
⊢ SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ ∈ 𝓝 ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))

Tactic:
exact prod_mem_nhds (Ioi_mem_nhds (f x).one_lt_rOut_div_rIn) univ_mem

Premises used: prod_mem_nhds, Ioi_mem_nhds, ContDiffBump.one_lt_rOut_div_rIn, Filter.univ_mem