awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
hR : 1 < R
right : Membership.mem (γ := Set E) univ (R, x).2
A : 0 < (R - 1) / (R + 1)
linarith : R + 1 ≤ 0 → HMul.hMul (α := ℝ) 2 (-1) + (1 - R) + (R + 1 - 0) = 0
linarith₁ : R + 1 ≤ 0 → GT.gt (α := ℝ) 2 0
⊢ 0 < R + 1

Tactic:
linarith
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
hR : 1 < R
right : Membership.mem (γ := Set E) univ (R, x).2
A : 0 < (R - 1) / (R + 1)
⊢ (R - 1) / (R + 1) < 1

Tactic:
have B : (R - 1) / (R + 1) < 1 := by apply (div_lt_one _).2 <;> linarith
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
hR : 1 < R
right : Membership.mem (γ := Set E) univ (R, x).2
A : 0 < (R - 1) / (R + 1)
B : (R - 1) / (R + 1) < 1
⊢ (fun (p : ℝ × E) ↦ ((p.1 - 1) / (p.1 + 1), ((p.1 + 1) / 2)⁻¹ • p.2)) (R, x) ∈
    SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ

Tactic:
simp only [prodMk_mem_set_prod_eq, mem_Ioo, mem_univ, and_true, A, B]

Premises used: Set.mem_Ioo, and_true, Set.prodMk_mem_set_prod_eq, Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
hR : 1 < R
x : E
hx : ‖x‖ ≤ 1
linarith : R + 1 ≤ 0 → HMul.hMul (α := ℝ) 2 (-1) + (1 - R) + (R + 1 - 0) = 0
linarith₁ : R + 1 ≤ 0 → GT.gt (α := ℝ) 2 0
⊢ 0 < R + 1

Tactic:
linarith
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
hR : 1 < R
x : E
hx : ‖x‖ ≤ 1
⊢ 0 < R + 1

Tactic:
have A : 0 < R + 1 := by linarith
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
hR : 1 < R
x : E
hx : ‖x‖ ≤ 1
A : 0 < R + 1
simp : y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) = 1
⊢ (if 1 < R then y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) else 0) = 1

Tactic:
simp only [hR, if_true]

Premises used: if_true
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
hR : 1 < R
x : E
hx : ‖x‖ ≤ 1
A : 0 < R + 1
apply : Membership.mem (γ := Set E) (closedBall 0 (1 - (R - 1) / (R + 1))) (((R + 1) / 2)⁻¹ • x)
⊢ y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) = 1

Tactic:
apply y_eq_one_of_mem_closedBall (IR R hR)

Premises used: ExistsContDiffBumpBase.y_eq_one_of_mem_closedBall
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
hR : 1 < R
x : E
hx : ‖x‖ ≤ 1
A : 0 < R + 1
simp : 2 / (R + 1) * ‖x‖ ≤ 1 - (R - 1) / (R + 1)
⊢ Membership.mem (γ := Set E) (closedBall 0 (1 - (R - 1) / (R + 1))) (((R + 1) / 2)⁻¹ • x)

Tactic:
simp only [norm_smul, inv_div, mem_closedBall_zero_iff, Real.norm_eq_abs, abs_div, abs_two,
          abs_of_nonneg A.le]

Premises used: norm_smul, abs_div, LT.lt.le, abs_of_nonneg, inv_div, mem_closedBall_zero_iff, Real.norm_eq_abs, abs_two
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
hR : 1 < R
x : E
hx : ‖x‖ ≤ 1
A : 0 < R + 1
⊢ 0 ≤ 2 / (R + 1)

Tactic:
positivity
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
hR : 1 < R
x : E
hx : ‖x‖ ≤ 1
A : 0 < R + 1
⊢ 2 / (R + 1) = 1 - (R - 1) / (R + 1)

Tactic:
field
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
hR : 1 < R
x : E
hx : ‖x‖ ≤ 1
A : 0 < R + 1
mul_le_of_le_one_right : 2 / (R + 1) = 1 - (R - 1) / (R + 1)
⊢ 2 / (R + 1) * ‖x‖ ≤ 1 - (R - 1) / (R + 1)

Tactic:
calc
          2 / (R + 1) * ‖x‖ ≤ 2 / (R + 1) := mul_le_of_le_one_right (by positivity) hx
          _ = 1 - (R - 1) / (R + 1) := by field

Premises used: HSub.hSub, mul_le_of_le_one_right, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
hR : 1 < R
linarith : (R + 1) / 2 ≤ 0 → 2 / 2 = 1
linarith₁ : (R + 1) / 2 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : (R + 1) / 2 ≤ 0 → GT.gt (α := ℝ) 2 0
linarith₃ :
  (R + 1) / 2 ≤ 0 → HMul.hMul (α := ℝ) 2 (-1) + (1 - R) + (1 * R + HMul.hMul (α := ℝ) 1 1 - HMul.hMul (α := ℝ) 2 0) = 0
linarith₄ : (R + 1) / 2 ≤ 0 → GT.gt (α := ℝ) 2 0
⊢ 0 < (R + 1) / 2

Tactic:
linarith
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
hR : 1 < R
⊢ 0 < (R + 1) / 2

Tactic:
have A : 0 < (R + 1) / 2 := by linarith
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
hR : 1 < R
A : 0 < (R + 1) / 2
apply : R - 1 < R + 1
apply₁ : 0 < R + 1
⊢ (R - 1) / (R + 1) < 1

Tactic:
apply (div_lt_one _).2

Premises used: Iff.mpr, div_lt_one
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
hR : 1 < R
A : 0 < (R + 1) / 2
linarith : R + 1 ≤ R - 1 → 2 / 2 = 1
linarith₁ : R + 1 ≤ R - 1 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : R + 1 ≤ R - 1 → GT.gt (α := ℝ) 2 0
linarith₃ : R + 1 ≤ R - 1 → HMul.hMul (α := ℝ) 2 (-1) + (R + 1 - (R - 1)) = 0
linarith₄ : R + 1 ≤ R - 1 → GT.gt (α := ℝ) 2 0
⊢ R - 1 < R + 1

Tactic:
linarith
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
hR : 1 < R
A : 0 < (R + 1) / 2
linarith : R + 1 ≤ 0 → 2 / 2 = 1
linarith₁ : R + 1 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : R + 1 ≤ 0 → GT.gt (α := ℝ) 2 0
linarith₃ : R + 1 ≤ 0 → HMul.hMul (α := ℝ) 2 (-1) + (1 - R) + (R + 1 - 0) = 0
linarith₄ : R + 1 ≤ 0 → GT.gt (α := ℝ) 2 0
⊢ 0 < R + 1

Tactic:
linarith
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
hR : 1 < R
A : 0 < (R + 1) / 2
⊢ (R - 1) / (R + 1) < 1

Tactic:
have C : (R - 1) / (R + 1) < 1 := by apply (div_lt_one _).2 <;> linarith
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
hR : 1 < R
A : 0 < (R + 1) / 2
C : (R - 1) / (R + 1) < 1
simp : Eq.{u_2 + 1} (α := Set E) (ball 0 ((R + 1) / 2 * (1 + (R - 1) / (R + 1)))) (ball 0 R)
⊢ Eq.{u_2 + 1} (α := Set E)
    (support (M := ℝ) fun (x : E) ↦ if 1 < R then y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) else 0) (ball 0 R)

Tactic:
simp only [hR, if_true, support_comp_inv_smul₀ A.ne', y_support _ (IR R hR) C,
          _root_.smul_ball A.ne', Real.norm_of_nonneg A.le, smul_zero]

Premises used: support_comp_inv_smul₀, if_true, smul_zero, LT.lt.le, LT.lt.ne', smul_ball, ExistsContDiffBumpBase.y_support, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
hR : 1 < R
A : 0 < (R + 1) / 2
C : (R - 1) / (R + 1) < 1
⊢ Eq.{u_2 + 1} (α := Set E) (ball 0 ((R + 1) / 2 * (1 + (R - 1) / (R + 1)))) (ball 0 R)

Tactic:
congr (congr_arg ball (Eq.refl 0)) ?_

Premises used: Metric.ball, congr_arg, congr, Eq.refl, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
hR : 1 < R
A : 0 < (R + 1) / 2
C : (R - 1) / (R + 1) < 1
refine : (R + 1) / 2 * (1 + (R - 1) / (R + 1)) = R
⊢ Eq.{u_2 + 1} (α := Set E) (ball 0 ((R + 1) / 2 * (1 + (R - 1) / (R + 1)))) (ball 0 R)

Tactic:
refine congr (congr_arg ball (Eq.refl 0)) ?_

Premises used: Metric.ball, congr_arg, congr, Eq.refl, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
hR : 1 < R
A : 0 < (R + 1) / 2
C : (R - 1) / (R + 1) < 1
⊢ (R + 1) / 2 * (1 + (R - 1) / (R + 1)) = R

Tactic:
field
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
⊢ ContDiffBumpBase E

Tactic:
exact
    { toFun := fun R x => if 1 < R then y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) else 0
      mem_Icc := fun R x => by
        push _ ∈ _
        split_ifs with h
        · refine ⟨y_nonneg _ _, y_le_one _ (IR R h)⟩
        · simp only [le_refl, zero_le_one, and_self]
      symmetric := fun R x => by
        split_ifs
        · simp only [y_neg, smul_neg]
        · rfl
      smooth := by
        suffices
          ContDiffOn ℝ ∞
            (uncurry y ∘ fun p : ℝ × E => ((p.1 - 1) / (p.1 + 1), ((p.1 + 1) / 2)⁻¹ • p.2))
            (Ioi 1 ×ˢ univ) by
          apply this.congr
          rintro ⟨R, x⟩ ⟨hR : 1 < R, _⟩
          simp only [hR, uncurry_apply_pair, if_true, Function.comp_apply]
        apply (y_smooth E).comp
        · apply ContDiffOn.prodMk
          · refine
              (contDiffOn_fst.sub contDiffOn_const).div (contDiffOn_fst.add contDiffOn_const) ?_
            rintro ⟨R, x⟩ ⟨hR : 1 < R, _⟩
            apply ne_of_gt
            dsimp only
            linarith
          · apply ContDiffOn.smul _ contDiffOn_snd
            refine ((contDiffOn_fst.add contDiffOn_const).div_const _).inv ?_
            rintro ⟨R, x⟩ ⟨hR : 1 < R, _⟩
            apply ne_of_gt
            dsimp only
            linarith
        · rintro ⟨R, x⟩ ⟨hR : 1 < R, _⟩
          have A : 0 < (R - 1) / (R + 1) := by apply div_pos <;> linarith
          have B : (R - 1) / (R + 1) < 1 := by apply (div_lt_one _).2 <;> linarith
          simp only [prodMk_mem_set_prod_eq, mem_Ioo, mem_univ, and_true, A, B]
      eq_one := fun R hR x hx => by
        have A : 0 < R + 1 := by linarith
        simp only [hR, if_true]
        apply y_eq_one_of_mem_closedBall (IR R hR)
        simp only [norm_smul, inv_div, mem_closedBall_zero_iff, Real.norm_eq_abs, abs_div, abs_two,
          abs_of_nonneg A.le]
        calc
          2 / (R + 1) * ‖x‖ ≤ 2 / (R + 1) := mul_le_of_le_one_right (by positivity) hx
          _ = 1 - (R - 1) / (R + 1) := by field
      support := fun R hR => by
        have A : 0 < (R + 1) / 2 := by linarith
        have C : (R - 1) / (R + 1) < 1 := by apply (div_lt_one _).2 <;> linarith
        simp only [hR, if_true, support_comp_inv_smul₀ A.ne', y_support _ (IR R hR) C,
          _root_.smul_ball A.ne', Real.norm_of_nonneg A.le, smul_zero]
        refine congr (congr_arg ball (Eq.refl 0)) ?_
        field }
-- Module: Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : ℝ
x_1 : E
⊢ ((x - ‖-x_1‖) / (x - 1)).smoothTransition = ((x - ‖x_1‖) / (x - 1)).smoothTransition

Tactic:
simp only [norm_neg]

Premises used: norm_neg
-- Module: Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
R : ℝ
x : E
hR : 1 < R
h :
  ContDiffAt ℝ (F := ℝ) (↑⊤ : WithTop ℕ∞) (uncurry fun (R : ℝ) (x : E) ↦ ((R - ‖x‖) / (R - 1)).smoothTransition) (R, x)
⊢ ContDiffWithinAt ℝ (F := ℝ) (↑⊤ : WithTop ℕ∞) (uncurry fun (R : ℝ) (x : E) ↦ ((R - ‖x‖) / (R - 1)).smoothTransition)
    (SProd.sprod (α := Set ℝ) (β := Set E) (Set.Ioi 1) Set.univ) (R, x)

Tactic:
apply ContDiffAt.contDiffWithinAt

Premises used: ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
R : ℝ
x : E
hR : 1 < R
⊢ 0 < R - 1

Tactic:
rw [← sub_pos] at hR

Premises used: sub_pos
-- Module: Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
R : ℝ
x : E
hR : 0 < R - 1
h :
  ContDiffAt.{0, u_1, 0} ℝ (E := ℝ × E) (F := ℝ) (↑⊤ : WithTop ℕ∞)
    (uncurry fun (R : ℝ) (x : E) ↦ ((R - ‖x‖) / (R - 1)).smoothTransition) (R, 0)
h₁ :
  ∀ (hx : x ≠ 0),
    ContDiffAt ℝ (F := ℝ) (↑⊤ : WithTop ℕ∞) (uncurry fun (R : ℝ) (x : E) ↦ ((R - ‖x‖) / (R - 1)).smoothTransition)
      (R, x)
⊢ ContDiffAt ℝ (F := ℝ) (↑⊤ : WithTop ℕ∞) (uncurry fun (R : ℝ) (x : E) ↦ ((R - ‖x‖) / (R - 1)).smoothTransition) (R, x)

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
R : ℝ
hR : 0 < R - 1
⊢ (R, 0).1 - 1 ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
R : ℝ
hR : 0 < R - 1
funProp : (R, 0).1 - 1 ≠ 0
⊢ ContinuousAt (Y := ℝ) (fun (p : ℝ × E) ↦ (p.1 - ‖p.2‖) / (p.1 - 1)) (R, 0)

Tactic:
fun_prop (disch := positivity)
-- Module: Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
R : ℝ
hR : 0 < R - 1
⊢ ContinuousAt (Y := ℝ) (fun (p : ℝ × E) ↦ (p.1 - ‖p.2‖) / (p.1 - 1)) (R, 0)

Tactic:
have A : ContinuousAt (fun p : ℝ × E ↦ (p.1 - ‖p.2‖) / (p.1 - 1)) (R, 0) := by
        fun_prop (disch := positivity)
-- Module: Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
R : ℝ
hR : 0 < R - 1
A : ContinuousAt (Y := ℝ) (fun (p : ℝ × E) ↦ (p.1 - ‖p.2‖) / (p.1 - 1)) (R, 0)
⊢ Norm.norm.{u_1} (E := E) (R, 0).2 < 1

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
R : ℝ
hR : 0 < R - 1
A : ContinuousAt (Y := ℝ) (fun (p : ℝ × E) ↦ (p.1 - ‖p.2‖) / (p.1 - 1)) (R, 0)
⊢ ∀ᶠ (p : ℝ × E) in 𝓝 (R, 0), 1 ≤ (p.1 - ‖p.2‖) / (p.1 - 1)

Tactic:
have B : ∀ᶠ p in 𝓝 (R, (0 : E)), 1 ≤ (p.1 - ‖p.2‖) / (p.1 - 1) :=
        A.eventually <| le_mem_nhds <| (one_lt_div hR).2 <| sub_lt_sub_left (by simp) _
-- Module: Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
R : ℝ
hR : 0 < R - 1
A : ContinuousAt (Y := ℝ) (fun (p : ℝ × E) ↦ (p.1 - ‖p.2‖) / (p.1 - 1)) (R, 0)
B : ∀ᶠ (p : ℝ × E) in 𝓝 (R, 0), 1 ≤ (p.1 - ‖p.2‖) / (p.1 - 1)
⊢ ContDiffAt.{0, u_1, 0} ℝ (E := ℝ × E) (F := ℝ) (↑⊤ : WithTop ℕ∞)
    (uncurry fun (R : ℝ) (x : E) ↦ ((R - ‖x‖) / (R - 1)).smoothTransition) (R, 0)

Tactic:
(contDiffAt_const (c := 1)).congr_of_eventuallyEq <| B.mono fun _ ↦
        smoothTransition.one_of_one_le

Premises used: Real.smoothTransition.one_of_one_le, Filter.Eventually.mono, contDiffAt_const, ContDiffAt.congr_of_eventuallyEq
-- Module: Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
R : ℝ
hR : 0 < R - 1
A : ContinuousAt (Y := ℝ) (fun (p : ℝ × E) ↦ (p.1 - ‖p.2‖) / (p.1 - 1)) (R, 0)
B : ∀ᶠ (p : ℝ × E) in 𝓝 (R, 0), 1 ≤ (p.1 - ‖p.2‖) / (p.1 - 1)
⊢ ContDiffAt.{0, u_1, 0} ℝ (E := ℝ × E) (F := ℝ) (↑⊤ : WithTop ℕ∞)
    (uncurry fun (R : ℝ) (x : E) ↦ ((R - ‖x‖) / (R - 1)).smoothTransition) (R, 0)

Tactic:
refine (contDiffAt_const (c := 1)).congr_of_eventuallyEq <| B.mono fun _ ↦
        smoothTransition.one_of_one_le

Premises used: Real.smoothTransition.one_of_one_le, Filter.Eventually.mono, contDiffAt_const, ContDiffAt.congr_of_eventuallyEq
-- Module: Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
R : ℝ
x : E
hR : 0 < R - 1
hx : x ≠ 0
⊢ ContDiffAt ℝ (F := ℝ) (↑⊤ : WithTop ℕ∞) (fun (a : ℝ × E) ↦ a.1 - 1) (R, x)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
R : ℝ
x : E
hR : 0 < R - 1
hx : x ≠ 0
h : ContDiffAt ℝ (F := ℝ) (↑⊤ : WithTop ℕ∞) (fun (a : ℝ × E) ↦ a.1 - ‖a.2‖) (R, x)
⊢ ContDiffAt ℝ (F := ℝ) (↑⊤ : WithTop ℕ∞) (uncurry fun (R : ℝ) (x : E) ↦ ((R - ‖x‖) / (R - 1)).smoothTransition) (R, x)

Tactic:
refine smoothTransition.contDiffAt.comp _ (ContDiffAt.div ?_ (by fun_prop) hR.ne')

Premises used: Real.smoothTransition.contDiffAt, ContDiffAt.div, LT.lt.ne', ContDiffAt.comp
-- Module: Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
R : ℝ
x : E
hR : 0 < R - 1
hx : x ≠ 0
⊢ ContDiffAt ℝ (F := ℝ) (↑⊤ : WithTop ℕ∞) (fun (a : ℝ × E) ↦ a.1 - ‖a.2‖) (R, x)

Tactic:
contDiffAt_fst.sub (contDiffAt_snd.norm ℝ hx)

Premises used: contDiffAt_snd, Real, ContDiffAt.norm, ContDiffAt.sub, contDiffAt_fst
-- Module: Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
R : ℝ
x : E
hR : 0 < R - 1
hx : x ≠ 0
⊢ ContDiffAt ℝ (F := ℝ) (↑⊤ : WithTop ℕ∞) (fun (a : ℝ × E) ↦ a.1 - ‖a.2‖) (R, x)

Tactic:
exact contDiffAt_fst.sub (contDiffAt_snd.norm ℝ hx)

Premises used: contDiffAt_snd, Real, ContDiffAt.norm, ContDiffAt.sub, contDiffAt_fst
-- Module: Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
R : ℝ
hR : 1 < R
h :
  ∀ (x : E),
    Membership.mem (γ := Set E) (Function.support (M := ℝ) fun (x : E) ↦ ((R - ‖x‖) / (R - 1)).smoothTransition) x ↔
      Membership.mem (γ := Set E) (Metric.ball 0 R) x
⊢ Eq.{u_1 + 1} (α := Set E) (Function.support (M := ℝ) fun (x : E) ↦ ((R - ‖x‖) / (R - 1)).smoothTransition)
    (Metric.ball 0 R)

Tactic:
ext x
-- Module: Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
R : ℝ
hR : 1 < R
x : E
h : 0 < (R - ‖x‖) / (R - 1) ↔ ‖x‖ < R
⊢ Membership.mem (γ := Set E) (Function.support (M := ℝ) fun (x : E) ↦ ((R - ‖x‖) / (R - 1)).smoothTransition) x ↔
    Membership.mem (γ := Set E) (Metric.ball 0 R) x

Tactic:
rw [mem_support, Ne, smoothTransition.zero_iff_nonpos, not_le, mem_ball_zero_iff]

Premises used: not_le, Ne, Real.smoothTransition.zero_iff_nonpos, Function.mem_support, mem_ball_zero_iff
-- Module: Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
R : ℝ
hR : 1 < R
x : E
⊢ 0 < (R - ‖x‖) / (R - 1) ↔ ‖x‖ < R

Tactic:
simp [hR]
-- Module: Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
⊢ HasContDiffBump E

Tactic:
⟨⟨.ofInnerProductSpace E⟩⟩

Premises used: HasContDiffBump.mk, Nonempty.intro, ContDiffBumpBase.ofInnerProductSpace