awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 0 < (R, x).1 + 1
have hf : 0 < R + 1
Tactic: dsimp only
-- 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
⊢ 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
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
hR : 1 < R
right : Membership.mem (γ := Set E) univ (R, x).2
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 (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 (x : ℝ × E) ↦ ((x.1 + 1) / 2)⁻¹ • x.2)
    (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ)
have apply : ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ × E) ↦ ((x.1 + 1) / 2)⁻¹) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ)
Tactic: apply ContDiffOn.smul _ contDiffOn_snd
-- 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) / 2)⁻¹) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ)
have refine : ∀ x ∈ SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ, (x.1 + 1) / 2 ≠ 0
Tactic: refine ((contDiffOn_fst.add contDiffOn_const).div_const _).inv ?_
-- 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) / 2 ≠ 0
have h : 0 < ((R, x).1 + 1) / 2
Tactic: apply ne_of_gt
-- 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
⊢ 0 < ((R, x).1 + 1) / 2
have h : 0 < (R + 1) / 2
Tactic: dsimp only
-- 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
⊢ 0 < (R + 1) / 2
have linarith : (R + 1) / 2 ≤ 0 → 2 / 2 = 1
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
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
hR : 1 < R
right : Membership.mem (γ := Set E) univ (R, x).2
linarith : (R + 1) / 2 ≤ 0 → 2 / 2 = 1
⊢ 0 < (R + 1) / 2
have linarith₁ : (R + 1) / 2 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
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
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
hR : 1 < R
right : Membership.mem (γ := Set E) univ (R, x).2
linarith : (R + 1) / 2 ≤ 0 → 2 / 2 = 1
linarith₁ : (R + 1) / 2 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 0 < (R + 1) / 2
have linarith₂ : (R + 1) / 2 ≤ 0 → GT.gt (α := ℝ) 2 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
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
hR : 1 < R
right : Membership.mem (γ := Set E) univ (R, x).2
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
⊢ 0 < (R + 1) / 2
have linarith₃ : (R + 1) / 2 ≤ 0 → HMul.hMul (α := ℝ) 2 (-1) + (1 - R) + (1 * R + HMul.hMul (α := ℝ) 1 1 - HMul.hMul (α := ℝ) 2 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
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
hR : 1 < R
right : Membership.mem (γ := Set E) univ (R, x).2
⊢ 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
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
hR : 1 < R
right : Membership.mem (γ := Set E) univ (R, x).2
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
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
hR : 1 < R
right : Membership.mem (γ := Set E) univ (R, x).2
⊢ 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 (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
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
hR : 1 < R
right : Membership.mem (γ := Set E) univ (R, x).2
⊢ (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
have A : 0 < (R - 1) / (R + 1)
Tactic: have A : 0 < (R - 1) / (R + 1) := by 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
hR : 1 < R
right : Membership.mem (γ := Set E) univ (R, x).2
A : 0 < (R - 1) / (R + 1)
⊢ (R - 1) / (R + 1) < 1
have apply : R - 1 < R + 1
Tactic: apply (div_lt_one _).2
-- 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
A : 0 < (R - 1) / (R + 1)
apply : R - 1 < R + 1
⊢ (R - 1) / (R + 1) < 1
have apply₁ : 0 < R + 1
Tactic: apply (div_lt_one _).2
-- 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
A : 0 < (R - 1) / (R + 1)
⊢ R - 1 < R + 1
have linarith : R + 1 ≤ R - 1 → HMul.hMul (α := ℝ) 2 (-1) + (R + 1 - (R - 1)) = 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
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 ≤ R - 1 → HMul.hMul (α := ℝ) 2 (-1) + (R + 1 - (R - 1)) = 0
⊢ R - 1 < R + 1
have linarith₁ : R + 1 ≤ R - 1 → GT.gt (α := ℝ) 2 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
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)
⊢ 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
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
⊢ 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
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)
⊢ (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
have B : (R - 1) / (R + 1) < 1
Tactic: have B : (R - 1) / (R + 1) < 1 := by apply (div_lt_one _).2 <;> 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 : ℝ
hR : 1 < R
x : E
hx : ‖x‖ ≤ 1
⊢ 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
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
⊢ 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
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
hR : 1 < R
x : E
hx : ‖x‖ ≤ 1
⊢ (if 1 < R then y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) else 0) = 1
have A : 0 < R + 1
Tactic: have A : 0 < R + 1 := by 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 : ℝ
hR : 1 < R
x : E
hx : ‖x‖ ≤ 1
A : 0 < R + 1
⊢ (if 1 < R then y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) else 0) = 1
have simp : y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) = 1
Tactic: simp only [hR, if_true]
-- 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 : ℝ
hR : 1 < R
x : E
hx : ‖x‖ ≤ 1
A : 0 < R + 1
⊢ y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) = 1
have apply : Membership.mem (γ := Set E) (closedBall 0 (1 - (R - 1) / (R + 1))) (((R + 1) / 2)⁻¹ • x)
Tactic: apply y_eq_one_of_mem_closedBall (IR R hR)
-- 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 : ℝ
hR : 1 < R
x : E
hx : ‖x‖ ≤ 1
A : 0 < R + 1
⊢ Membership.mem (γ := Set E) (closedBall 0 (1 - (R - 1) / (R + 1))) (((R + 1) / 2)⁻¹ • x)
have simp : 2 / (R + 1) * ‖x‖ ≤ 1 - (R - 1) / (R + 1)
Tactic: simp only [norm_smul, inv_div, mem_closedBall_zero_iff, Real.norm_eq_abs, abs_div, abs_two,
          abs_of_nonneg A.le]
-- 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 : ℝ
hR : 1 < R
x : E
hx : ‖x‖ ≤ 1
A : 0 < R + 1
⊢ 2 / (R + 1) * ‖x‖ ≤ 1 - (R - 1) / (R + 1)
have mul_le_of_le_one_right : 2 / (R + 1) = 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
-- 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 : ℝ
hR : 1 < R
⊢ 0 < (R + 1) / 2
have linarith : (R + 1) / 2 ≤ 0 → 2 / 2 = 1
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
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
hR : 1 < R
linarith : (R + 1) / 2 ≤ 0 → 2 / 2 = 1
⊢ 0 < (R + 1) / 2
have linarith₁ : (R + 1) / 2 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
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
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
⊢ 0 < (R + 1) / 2
have linarith₂ : (R + 1) / 2 ≤ 0 → GT.gt (α := ℝ) 2 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
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
⊢ 0 < (R + 1) / 2
have linarith₃ : (R + 1) / 2 ≤ 0 → HMul.hMul (α := ℝ) 2 (-1) + (1 - R) + (1 * R + HMul.hMul (α := ℝ) 1 1 - HMul.hMul (α := ℝ) 2 0) = 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
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
hR : 1 < 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)
have A : 0 < (R + 1) / 2
Tactic: have A : 0 < (R + 1) / 2 := by 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 : ℝ
hR : 1 < R
A : 0 < (R + 1) / 2
⊢ (R - 1) / (R + 1) < 1
have apply : R - 1 < R + 1
Tactic: apply (div_lt_one _).2
-- 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 : ℝ
hR : 1 < R
A : 0 < (R + 1) / 2
apply : R - 1 < R + 1
⊢ (R - 1) / (R + 1) < 1
have apply₁ : 0 < R + 1
Tactic: apply (div_lt_one _).2
-- 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 : ℝ
hR : 1 < R
A : 0 < (R + 1) / 2
⊢ R - 1 < R + 1
have linarith : R + 1 ≤ R - 1 → 2 / 2 = 1
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
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
⊢ R - 1 < R + 1
have linarith₁ : R + 1 ≤ R - 1 → HMul.hMul (α := ℝ) 1 2 = 2
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
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
⊢ R - 1 < R + 1
have linarith₂ : R + 1 ≤ R - 1 → GT.gt (α := ℝ) 2 0
Tactic: linarith