awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
⊢ ContDiffOn ℝ ∞ (uncurry y) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)
have hs : IsOpen (X := ℝ) (Ioo 0 1)
Tactic: have hs : IsOpen (Ioo (0 : ℝ) (1 : ℝ)) := isOpen_Ioo
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
hs : IsOpen (X := ℝ) (Ioo 0 1)
⊢ ContDiffOn ℝ ∞ (uncurry y) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)
have hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
Tactic: have hk : IsCompact (closedBall (0 : E) 1) := ProperSpace.isCompact_closedBall _ _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
⊢ ContDiffOn ℝ ∞ (uncurry y) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)
have refine_1 : ∀ (p : ℝ) (x : E), Membership.mem (γ := Set ℝ) (Ioo 0 1) p → x ∉ closedBall 0 1 → w p x = 0
Tactic: refine contDiffOn_convolution_left_with_param (lsmul ℝ ℝ) hs hk ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
refine_1 : ∀ (p : ℝ) (x : E), Membership.mem (γ := Set ℝ) (Ioo 0 1) p → x ∉ closedBall 0 1 → w p x = 0
⊢ ContDiffOn ℝ ∞ (uncurry y) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)
have refine_2 : LocallyIntegrable.{u_1, 0} (X := E) φ μ
Tactic: refine contDiffOn_convolution_left_with_param (lsmul ℝ ℝ) hs hk ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
refine_1 : ∀ (p : ℝ) (x : E), Membership.mem (γ := Set ℝ) (Ioo 0 1) p → x ∉ closedBall 0 1 → w p x = 0
refine_2 : LocallyIntegrable.{u_1, 0} (X := E) φ μ
⊢ ContDiffOn ℝ ∞ (uncurry y) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)
have refine_3 : ContDiffOn ℝ ∞ (HasUncurry.uncurry (α := ℝ → E → ℝ) w) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)
Tactic: refine contDiffOn_convolution_left_with_param (lsmul ℝ ℝ) hs hk ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
p : ℝ
x : E
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : x ∉ closedBall 0 1
⊢ w p x = 0
have refine_1 : (|p| ^ finrank ℝ E = 0 ∨ Eq (α := ℝ) (@integral _ _ _ _ inst_3 μ fun (x : E) ↦ u x) 0) ∨ u (p⁻¹ • x) = 0
Tactic: simp only [w, mul_inv_rev, smul_eq_mul, mul_eq_zero, inv_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
p : ℝ
x : E
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : x ∉ closedBall 0 1
⊢ (|p| ^ finrank ℝ E = 0 ∨ Eq (α := ℝ) (@integral _ _ _ _ inst_3 μ fun (x : E) ↦ u x) 0) ∨ u (p⁻¹ • x) = 0
have refine_1 : u (p⁻¹ • x) = 0
Tactic: right
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
p : ℝ
x : E
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : x ∉ closedBall 0 1
⊢ u (p⁻¹ • x) = 0
have refine_1 : ∀ (hx : u (p⁻¹ • x) ≠ 0), Membership.mem (γ := Set E) (closedBall 0 1) x
Tactic: contrapose! hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
p : ℝ
x : E
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : u (p⁻¹ • x) ≠ 0
⊢ Membership.mem (γ := Set E) (closedBall 0 1) x
have this : Membership.mem (γ := Set E) (support u) (p⁻¹ • x)
Tactic: have : p⁻¹ • x ∈ support u := mem_support.2 hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
p : ℝ
x : E
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : u (p⁻¹ • x) ≠ 0
this : Membership.mem (γ := Set E) (support u) (p⁻¹ • x)
⊢ Membership.mem (γ := Set E) (closedBall 0 1) x
have this₁ : ‖x‖ < p
Tactic: simp only [u_support, norm_smul, mem_ball_zero_iff, Real.norm_eq_abs, abs_inv,
      abs_of_nonneg hp.1.le, ← div_eq_inv_mul, div_lt_one hp.1] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
p : ℝ
x : E
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : u (p⁻¹ • x) ≠ 0
this : ‖x‖ < p
⊢ Membership.mem (γ := Set E) (closedBall 0 1) x
have refine_1 : ‖x‖ ≤ 1
Tactic: rw [mem_closedBall_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
⊢ ContDiffOn ℝ ∞ (HasUncurry.uncurry (α := ℝ → E → ℝ) w) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)
have refine_3 : ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ × E) ↦ ((@integral _ _ _ _ inst_3 μ fun (x : E) ↦ u x) * |x.1| ^ finrank ℝ E)⁻¹)
  (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)
Tactic: apply ContDiffOn.mul
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
refine_3 :
  ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ × E) ↦ ((@integral _ _ _ _ inst_3 μ fun (x : E) ↦ u x) * |x.1| ^ finrank ℝ E)⁻¹)
    (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)
⊢ ContDiffOn ℝ ∞ (HasUncurry.uncurry (α := ℝ → E → ℝ) w) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)
have refine_3₁ : ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ × E) ↦ u (x.1⁻¹ • x.2)) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)
Tactic: apply ContDiffOn.mul
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
⊢ ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ × E) ↦ ((@integral _ _ _ _ inst_3 μ fun (x : E) ↦ u x) * |x.1| ^ finrank ℝ E)⁻¹)
    (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)
have refine_3 : ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ × E) ↦ |x.1| ^ finrank ℝ E) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)
Tactic: refine
        (contDiffOn_const.mul ?_).inv fun x hx =>
          ne_of_gt (mul_pos (u_int_pos E) (pow_pos (abs_pos_of_pos hx.1.1) (finrank ℝ E)))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
⊢ ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ × E) ↦ |x.1| ^ finrank ℝ E) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)
have refine_3 : ContDiffOn ℝ (F := ℝ) ∞ (fun (y : ℝ × E) ↦ |y.1|) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)
Tactic: apply ContDiffOn.pow
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
⊢ ContDiffOn ℝ (F := ℝ) ∞ (fun (y : ℝ × E) ↦ ‖y.1‖) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)
have refine_3 : ContDiffOn ℝ ∞ Prod.fst (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)
Tactic: apply ContDiffOn.norm ℝ
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
refine_3 : ContDiffOn ℝ ∞ Prod.fst (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)
⊢ ContDiffOn ℝ (F := ℝ) ∞ (fun (y : ℝ × E) ↦ ‖y.1‖) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)
have refine_3₁ : ∀ x ∈ SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ, x.1 ≠ 0
Tactic: apply ContDiffOn.norm ℝ
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
⊢ ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ × E) ↦ u (x.1⁻¹ • x.2)) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)
have refine_3 : ContDiffOn ℝ (F := E) ∞ (fun (x : ℝ × E) ↦ x.1⁻¹ • x.2) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)
Tactic: apply (u_smooth E).comp_contDiffOn
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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
⊢ HasContDiffBump E
have refine : ContDiffBumpBase E
Tactic: refine ⟨⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (hypothesis)
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
⊢ ContDiffBumpBase E
have this : let this := borel E;
BorelSpace E
Tactic: borelize E
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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
R : ℝ
hR : 1 < R
⊢ 0 < (R - 1) / (R + 1)
have ha : 0 < R - 1
Tactic: apply div_pos
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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
R : ℝ
hR : 1 < R
ha : 0 < R - 1
⊢ 0 < (R - 1) / (R + 1)
have hb : 0 < R + 1
Tactic: apply div_pos
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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
R : ℝ
hR : 1 < R
⊢ 0 < R - 1
have linarith : R - 1 ≤ 0 → 1 - R + (R - 1 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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
R : ℝ
hR : 1 < R
⊢ 0 < R + 1
have linarith : R + 1 ≤ 0 → HMul.hMul (α := ℝ) 2 (-1) + (1 - R) + (R + 1 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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
R : ℝ
hR : 1 < R
linarith : R + 1 ≤ 0 → HMul.hMul (α := ℝ) 2 (-1) + (1 - R) + (R + 1 - 0) = 0
⊢ 0 < R + 1
have linarith₁ : R + 1 ≤ 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (hypothesis)
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
⊢ ContDiffBumpBase E
have IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
Tactic: have IR : ∀ R : ℝ, 1 < R → 0 < (R - 1) / (R + 1) := by intro R hR; apply div_pos <;> linarith
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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
⊢ (0 ≤ if 1 < R then y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) else 0) ∧
    (if 1 < R then y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) else 0) ≤ 1
have pos : ∀ (h : 1 < R), 0 ≤ y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) ∧ y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) ≤ 1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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
pos : ∀ (h : 1 < R), 0 ≤ y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) ∧ y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) ≤ 1
⊢ (0 ≤ if 1 < R then y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) else 0) ∧
    (if 1 < R then y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) else 0) ≤ 1
have neg : ∀ (h : ¬1 < R), LE.le (α := ℝ) 0 0 ∧ LE.le (α := ℝ) 0 1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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
⊢ (if 1 < R then y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • -x) else 0) =
    if 1 < R then y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) else 0
have pos : 1 < R → y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • -x) = y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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
pos : 1 < R → y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • -x) = y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x)
⊢ (if 1 < R then y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • -x) else 0) =
    if 1 < R then y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) else 0
have neg : ¬1 < R → Eq (α := ℝ) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
this :
  ContDiffOn ℝ ∞
    (Function.comp (β := ℝ × E) (uncurry y) fun (p : ℝ × E) ↦ ((p.1 - 1) / (p.1 + 1), ((p.1 + 1) / 2)⁻¹ • p.2))
    (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ)
⊢ ContDiffOn ℝ (F := ℝ) ∞
    (uncurry fun (R : ℝ) (x : E) ↦ if 1 < R then y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) else 0)
    (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ)
have apply : ∀ x ∈ SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ,
  uncurry (fun (R : ℝ) (x : E) ↦ if 1 < R then y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) else 0) x =
    Function.comp (β := ℝ × E) (uncurry y) (fun (p : ℝ × E) ↦ ((p.1 - 1) / (p.1 + 1), ((p.1 + 1) / 2)⁻¹ • p.2)) x
Tactic: apply this.congr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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)
⊢ ContDiffOn ℝ (F := ℝ) ∞
    (uncurry fun (R : ℝ) (x : E) ↦ if 1 < R then y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) else 0)
    (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ)
have ContDiffOn : ContDiffOn ℝ ∞
  (Function.comp (β := ℝ × E) (uncurry y) fun (p : ℝ × E) ↦ ((p.1 - 1) / (p.1 + 1), ((p.1 + 1) / 2)⁻¹ • p.2))
  (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ)
Tactic: 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]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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)
⊢ ContDiffOn ℝ ∞
    (Function.comp (β := ℝ × E) (uncurry y) fun (p : ℝ × E) ↦ ((p.1 - 1) / (p.1 + 1), ((p.1 + 1) / 2)⁻¹ • p.2))
    (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ)
have hf : ContDiffOn ℝ (F := ℝ × E) ∞ (fun (p : ℝ × E) ↦ ((p.1 - 1) / (p.1 + 1), ((p.1 + 1) / 2)⁻¹ • p.2))
  (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ)
Tactic: apply (y_smooth E).comp
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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)
hf :
  ContDiffOn ℝ (F := ℝ × E) ∞ (fun (p : ℝ × E) ↦ ((p.1 - 1) / (p.1 + 1), ((p.1 + 1) / 2)⁻¹ • p.2))
    (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ)
⊢ ContDiffOn ℝ ∞
    (Function.comp (β := ℝ × E) (uncurry y) fun (p : ℝ × E) ↦ ((p.1 - 1) / (p.1 + 1), ((p.1 + 1) / 2)⁻¹ • p.2))
    (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ)
have st : MapsTo (fun (p : ℝ × E) ↦ ((p.1 - 1) / (p.1 + 1), ((p.1 + 1) / 2)⁻¹ • p.2))
  (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)
Tactic: apply (y_smooth E).comp
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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)
⊢ ContDiffOn ℝ (F := ℝ × E) ∞ (fun (p : ℝ × E) ↦ ((p.1 - 1) / (p.1 + 1), ((p.1 + 1) / 2)⁻¹ • p.2))
    (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ)
have hf : ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ × E) ↦ (x.1 - 1) / (x.1 + 1)) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ)
Tactic: apply ContDiffOn.prodMk
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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)
hf :
  ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ × E) ↦ (x.1 - 1) / (x.1 + 1)) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ)
⊢ ContDiffOn ℝ (F := ℝ × E) ∞ (fun (p : ℝ × E) ↦ ((p.1 - 1) / (p.1 + 1), ((p.1 + 1) / 2)⁻¹ • p.2))
    (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ)
have hf₁ : ContDiffOn ℝ (F := E) ∞ (fun (x : ℝ × E) ↦ ((x.1 + 1) / 2)⁻¹ • x.2) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ)
Tactic: apply ContDiffOn.prodMk
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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)
⊢ ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ × E) ↦ (x.1 - 1) / (x.1 + 1)) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ)
have hf : ∀ x ∈ SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ, x.1 + 1 ≠ 0
Tactic: refine
              (contDiffOn_fst.sub contDiffOn_const).div (contDiffOn_fst.add contDiffOn_const) ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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
⊢ (R, x).1 + 1 ≠ 0
have hf : 0 < (R, x).1 + 1
Tactic: apply ne_of_gt