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 : ℝ
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
⊢ 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 : ℝ
hR : 1 < R
A : 0 < (R + 1) / 2
⊢ 0 < R + 1
have linarith : R + 1 ≤ 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
A : 0 < (R + 1) / 2
linarith : R + 1 ≤ 0 → 2 / 2 = 1
⊢ 0 < R + 1
have linarith₁ : R + 1 ≤ 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
A : 0 < (R + 1) / 2
linarith : R + 1 ≤ 0 → 2 / 2 = 1
linarith₁ : R + 1 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 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)
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
⊢ 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 (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
A : 0 < (R + 1) / 2
⊢ 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 C : (R - 1) / (R + 1) < 1
Tactic: have C : (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
A : 0 < (R + 1) / 2
C : (R - 1) / (R + 1) < 1
⊢ 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 simp : Eq.{u_2 + 1} (α := Set E) (ball 0 ((R + 1) / 2 * (1 + (R - 1) / (R + 1)))) (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]
-- 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
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)
have refine : (R + 1) / 2 * (1 + (R - 1) / (R + 1)) = R
Tactic: refine congr (congr_arg ball (Eq.refl 0)) ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.InnerProduct (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
R : ℝ
x : E
hR : 1 < R
⊢ 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)
have h : ContDiffAt ℝ (F := ℝ) (↑⊤ : WithTop ℕ∞) (uncurry fun (R : ℝ) (x : E) ↦ ((R - ‖x‖) / (R - 1)).smoothTransition) (R, x)
Tactic: apply ContDiffAt.contDiffWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.InnerProduct (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
R : ℝ
x : E
hR : 1 < R
⊢ ContDiffAt ℝ (F := ℝ) (↑⊤ : WithTop ℕ∞) (uncurry fun (R : ℝ) (x : E) ↦ ((R - ‖x‖) / (R - 1)).smoothTransition) (R, x)
have hR₁ : 0 < R - 1
Tactic: rw [← sub_pos] at hR
Cleared hypotheses: hR
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.InnerProduct (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
R : ℝ
x : E
hR : 0 < R - 1
⊢ ContDiffAt ℝ (F := ℝ) (↑⊤ : WithTop ℕ∞) (uncurry fun (R : ℝ) (x : E) ↦ ((R - ‖x‖) / (R - 1)).smoothTransition) (R, x)
have h : ContDiffAt.{0, u_1, 0} ℝ (E := ℝ × E) (F := ℝ) (↑⊤ : WithTop ℕ∞)
  (uncurry fun (R : ℝ) (x : E) ↦ ((R - ‖x‖) / (R - 1)).smoothTransition) (R, 0)
Tactic: rcases eq_or_ne x 0 with rfl | hx
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.InnerProduct (goal)
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)
⊢ ContDiffAt ℝ (F := ℝ) (↑⊤ : WithTop ℕ∞) (uncurry fun (R : ℝ) (x : E) ↦ ((R - ‖x‖) / (R - 1)).smoothTransition) (R, x)
have h₁ : ∀ (hx : x ≠ 0),
  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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.InnerProduct (goal)
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)
have funProp : (R, 0).1 - 1 ≠ 0
Tactic: fun_prop (disch := positivity)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.InnerProduct (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
R : ℝ
hR : 0 < R - 1
⊢ ContDiffAt.{0, u_1, 0} ℝ (E := ℝ × E) (F := ℝ) (↑⊤ : WithTop ℕ∞)
    (uncurry fun (R : ℝ) (x : E) ↦ ((R - ‖x‖) / (R - 1)).smoothTransition) (R, 0)
have A : 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)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.InnerProduct (hypothesis)
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)
⊢ ContDiffAt.{0, u_1, 0} ℝ (E := ℝ × E) (F := ℝ) (↑⊤ : WithTop ℕ∞)
    (uncurry fun (R : ℝ) (x : E) ↦ ((R - ‖x‖) / (R - 1)).smoothTransition) (R, 0)
have B : ∀ᶠ (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) _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.InnerProduct (goal)
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 ℕ∞) (uncurry fun (R : ℝ) (x : E) ↦ ((R - ‖x‖) / (R - 1)).smoothTransition) (R, x)
have h : ContDiffAt ℝ (F := ℝ) (↑⊤ : WithTop ℕ∞) (fun (a : ℝ × E) ↦ a.1 - ‖a.2‖) (R, x)
Tactic: refine smoothTransition.contDiffAt.comp _ (ContDiffAt.div ?_ (by fun_prop) hR.ne')
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.InnerProduct (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
R : ℝ
hR : 1 < R
⊢ Eq.{u_1 + 1} (α := Set E) (Function.support (M := ℝ) fun (x : E) ↦ ((R - ‖x‖) / (R - 1)).smoothTransition)
    (Metric.ball 0 R)
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.InnerProduct (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
R : ℝ
hR : 1 < R
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
have h : 0 < (R - ‖x‖) / (R - 1) ↔ ‖x‖ < R
Tactic: rw [mem_support, Ne, smoothTransition.zero_iff_nonpos, not_le, mem_ball_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
⊢ LT.lt (α := ℝ) 0 (∫ (x : E), (↑f : E → ℝ) x ∂μ)
have refine : LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set E) → ENNReal) (support (↑f : E → ℝ)) : ENNReal)
Tactic: refine (integral_pos_iff_support_of_nonneg f.nonneg' f.integrable).mpr ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
⊢ LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set E) → ENNReal) (support (↑f : E → ℝ)) : ENNReal)
have rw : LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set E) → ENNReal) (ball c f.rOut) : ENNReal)
Tactic: rw [f.support_eq]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
⊢ Eq (α := ℝ) (∫ (x : E), f.normed μ x ∂μ) 1
have simp_rw : HSMul.hSMul (α := ℝ) (β := ℝ) (∫ (x : E), (↑f : E → ℝ) x ∂μ)⁻¹ (∫ (x : E), (↑f : E → ℝ) x ∂μ) = 1
Tactic: simp_rw [ContDiffBump.normed, div_eq_mul_inv, mul_comm (f _), ← smul_eq_mul, integral_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
⊢ (support (M := ℝ) fun (x : E) ↦ (↑f : E → ℝ) x / ∫ (x : E), (↑f : E → ℝ) x ∂μ) = ball c f.rOut
have rw : (support (↑f : E → ℝ) ∩ support (M := ℝ) fun (x : E) ↦ ∫ (x : E), (↑f : E → ℝ) x ∂μ) = ball c f.rOut
Tactic: rw [support_div, f.support_eq, support_const f.integral_pos.ne', inter_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
rw : (support (↑f : E → ℝ) ∩ support (M := ℝ) fun (x : E) ↦ ∫ (x : E), (↑f : E → ℝ) x ∂μ) = ball c f.rOut
⊢ (support (M := ℝ) fun (x : E) ↦ (↑f : E → ℝ) x / ∫ (x : E), (↑f : E → ℝ) x ∂μ) = ball c f.rOut
have rw₁ : (ball c f.rOut ∩ support (M := ℝ) fun (x : E) ↦ ∫ (x : E), (↑f : E → ℝ) x ∂μ) = ball c f.rOut
Tactic: rw [support_div, f.support_eq, support_const f.integral_pos.ne', inter_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
rw : (support (↑f : E → ℝ) ∩ support (M := ℝ) fun (x : E) ↦ ∫ (x : E), (↑f : E → ℝ) x ∂μ) = ball c f.rOut
rw₁ : (ball c f.rOut ∩ support (M := ℝ) fun (x : E) ↦ ∫ (x : E), (↑f : E → ℝ) x ∂μ) = ball c f.rOut
⊢ (support (M := ℝ) fun (x : E) ↦ (↑f : E → ℝ) x / ∫ (x : E), (↑f : E → ℝ) x ∂μ) = ball c f.rOut
have rw₂ : ball c f.rOut ∩ univ = ball c f.rOut
Tactic: rw [support_div, f.support_eq, support_const f.integral_pos.ne', inter_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
rw : (support (↑f : E → ℝ) ∩ support (M := ℝ) fun (x : E) ↦ ∫ (x : E), (↑f : E → ℝ) x ∂μ) = ball c f.rOut
rw₁ : (ball c f.rOut ∩ support (M := ℝ) fun (x : E) ↦ ∫ (x : E), (↑f : E → ℝ) x ∂μ) = ball c f.rOut
rw₂ : ball c f.rOut ∩ univ = ball c f.rOut
⊢ (support (M := ℝ) fun (x : E) ↦ (↑f : E → ℝ) x / ∫ (x : E), (↑f : E → ℝ) x ∂μ) = ball c f.rOut
have rw₃ : ball c f.rOut = ball c f.rOut
Tactic: rw [support_div, f.support_eq, support_const f.integral_pos.ne', inter_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
⊢ tsupport (f.normed μ) = closedBall c f.rOut
have rw : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (support (f.normed μ)) = closedBall c f.rOut
Tactic: rw [tsupport, f.support_normed_eq, closure_ball _ f.rOut_pos.ne']
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
rw : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (support (f.normed μ)) = closedBall c f.rOut
⊢ tsupport (f.normed μ) = closedBall c f.rOut
have rw₁ : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball c f.rOut) = closedBall c f.rOut
Tactic: rw [tsupport, f.support_normed_eq, closure_ball _ f.rOut_pos.ne']
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
rw : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (support (f.normed μ)) = closedBall c f.rOut
rw₁ : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball c f.rOut) = closedBall c f.rOut
⊢ tsupport (f.normed μ) = closedBall c f.rOut
have rw₂ : closedBall c f.rOut = closedBall c f.rOut
Tactic: rw [tsupport, f.support_normed_eq, closure_ball _ f.rOut_pos.ne']
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
ι : Type u_2
φ : ι → ContDiffBump c
l : Filter ι
hφ : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝 0)
⊢ Tendsto (fun (i : ι) ↦ support (M := ℝ) fun (x : E) ↦ (φ i).normed μ x) l (𝓝 c).smallSets
have hφ₁ : ∀ ε > 0, ∀ᶠ (x : ι) in l, (φ x).rOut < ε
Tactic: simp_rw [NormedAddGroup.tendsto_nhds_zero, Real.norm_eq_abs,
    abs_eq_self.mpr (φ _).rOut_pos.le] at hφ
Cleared hypotheses: hφ
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
ι : Type u_2
φ : ι → ContDiffBump c
l : Filter ι
hφ : ∀ ε > 0, ∀ᶠ (x : ι) in l, (φ x).rOut < ε
⊢ Tendsto (fun (i : ι) ↦ support (M := ℝ) fun (x : E) ↦ (φ i).normed μ x) l (𝓝 c).smallSets
have rw : ∀ (i : ℝ), 0 < i → ∀ᶠ (x : ι) in l, (support (M := ℝ) fun (x_1 : E) ↦ (φ x).normed μ x_1) ∈ 𝒫 ball c i
Tactic: rw [nhds_basis_ball.smallSets.tendsto_right_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
ι : Type u_2
φ : ι → ContDiffBump c
l : Filter ι
hφ : ∀ ε > 0, ∀ᶠ (x : ι) in l, (φ x).rOut < ε
⊢ ∀ (i : ℝ), 0 < i → ∀ᶠ (x : ι) in l, (support (M := ℝ) fun (x_1 : E) ↦ (φ x).normed μ x_1) ∈ 𝒫 ball c i
have refine : ∀ (ε : ℝ) (hε : 0 < ε) (i : ι) (hi : (φ i).rOut < ε), (support (M := ℝ) fun (x : E) ↦ (φ i).normed μ x) ∈ 𝒫 ball c ε
Tactic: refine fun ε hε ↦ (hφ ε hε).mono fun i hi ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
ι : Type u_2
φ : ι → ContDiffBump c
l : Filter ι
hφ : ∀ ε > 0, ∀ᶠ (x : ι) in l, (φ x).rOut < ε
ε : ℝ
hε : 0 < ε
i : ι
hi : (φ i).rOut < ε
⊢ (support (M := ℝ) fun (x : E) ↦ (φ i).normed μ x) ∈ 𝒫 ball c ε
have rw : ball c (φ i).rOut ∈ 𝒫 ball c ε
Tactic: rw [(φ i).support_normed_eq]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
X : Type u_2
inst_8 : NormedAddCommGroup X
inst_9 : NormedSpace ℝ X
inst_10 : CompleteSpace X
z : X
⊢ ∫ (x : E), f.normed μ x • z ∂μ = z
have simp_rw : HSMul.hSMul (α := ℝ) (∫ (x : E), f.normed μ x ∂μ) z = z
Tactic: simp_rw [integral_smul_const, f.integral_normed (μ := μ), one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
X : Type u_2
inst_8 : NormedAddCommGroup X
inst_9 : NormedSpace ℝ X
inst_10 : CompleteSpace X
z : X
simp_rw : HSMul.hSMul (α := ℝ) (∫ (x : E), f.normed μ x ∂μ) z = z
⊢ ∫ (x : E), f.normed μ x • z ∂μ = z
have simp_rw₁ : HSMul.hSMul (α := ℝ) 1 z = z
Tactic: simp_rw [integral_smul_const, f.integral_normed (μ := μ), one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
⊢ μ.real (closedBall c f.rIn) ≤ ∫ (x : E), (↑f : E → ℝ) x ∂μ
have c₁ : μ.real (closedBall c f.rIn) = ∫ (x : E) in closedBall c f.rIn, 1 ∂μ
Tactic: calc
  μ.real (closedBall c f.rIn) = ∫ x in closedBall c f.rIn, 1 ∂μ := by simp
  _ = ∫ x in closedBall c f.rIn, f x ∂μ := setIntegral_congr_fun measurableSet_closedBall
        (fun x hx ↦ (one_of_mem_closedBall f hx).symm)
  _ ≤ ∫ x, f x ∂μ := setIntegral_le_integral f.integrable (Eventually.of_forall (fun x ↦ f.nonneg))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
x : E
⊢ (↑f : E → ℝ) x / ∫ (x : E), (↑f : E → ℝ) x ∂μ ≤ 1 / μ.real (closedBall c f.rIn)
have hd : 0 < μ.real (closedBall c f.rIn)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
x : E
hd : 0 < μ.real (closedBall c f.rIn)
⊢ (↑f : E → ℝ) x / ∫ (x : E), (↑f : E → ℝ) x ∂μ ≤ 1 / μ.real (closedBall c f.rIn)
have hac : (↑f : E → ℝ) x ≤ 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
x : E
hd : 0 < μ.real (closedBall c f.rIn)
hac : (↑f : E → ℝ) x ≤ 1
⊢ (↑f : E → ℝ) x / ∫ (x : E), (↑f : E → ℝ) x ∂μ ≤ 1 / μ.real (closedBall c f.rIn)
have hdb : μ.real (closedBall c f.rIn) ≤ ∫ (x : E), (↑f : E → ℝ) x ∂μ
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
⊢ Eq (α := ℝ) (∫ (x : E), (↑f : E → ℝ) x ∂μ) (∫ (x : E) in closedBall c f.rOut, (↑f : E → ℝ) x ∂μ)
have apply : ∀ (x : E) (hx : x ∉ closedBall c f.rOut), (↑f : E → ℝ) x = 0
Tactic: apply (setIntegral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)).symm