awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
⊢ ∀ᶠ (i : ℝ) in atTop, ∀ (x : F), 0 ≤ i ^ finrank ℝ F * φ (i • x)
have h₁ : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      Membership.mem (γ := Set ℝ) (Ici 0) x →
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (i : ℝ) ↦ ∀ (x : F), 0 ≤ i ^ finrank ℝ F * φ (i • x)) x} x}
    a
Tactic: filter_upwards [Ici_mem_atTop 0] with c (hc : 0 ≤ c) x using mul_nonneg (by positivity) (hφ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
h₁ :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) (Ici 0) x →
          Membership.mem (γ := Set ℝ) {x : ℝ | (fun (i : ℝ) ↦ ∀ (x : F), 0 ≤ i ^ finrank ℝ F * φ (i • x)) x} x}
      a
⊢ ∀ᶠ (i : ℝ) in atTop, ∀ (x : F), 0 ≤ i ^ finrank ℝ F * φ (i • x)
have h₂ : ∀ (a : ℝ), Membership.mem (γ := Set ℝ) (Ici 0) a → ∀ (x : F), 0 ≤ a ^ finrank ℝ F * φ (a • x)
Tactic: filter_upwards [Ici_mem_atTop 0] with c (hc : 0 ≤ c) x using mul_nonneg (by positivity) (hφ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
h₁ :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) (Ici 0) x →
          Membership.mem (γ := Set ℝ) {x : ℝ | (fun (i : ℝ) ↦ ∀ (x : F), 0 ≤ i ^ finrank ℝ F * φ (i • x)) x} x}
      a
h₂ : ∀ (a : ℝ), Membership.mem (γ := Set ℝ) (Ici 0) a → ∀ (x : F), 0 ≤ a ^ finrank ℝ F * φ (a • x)
⊢ ∀ᶠ (i : ℝ) in atTop, ∀ (x : F), 0 ≤ i ^ finrank ℝ F * φ (i • x)
have h₃ : ∀ (c : ℝ) (hc : 0 ≤ c) (x : F), 0 ≤ c ^ finrank ℝ F * φ (c • x)
Tactic: filter_upwards [Ici_mem_atTop 0] with c (hc : 0 ≤ c) x using mul_nonneg (by positivity) (hφ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
⊢ TendstoUniformlyOn (β := ℝ) (fun (i : ℝ) (x : F) ↦ i ^ finrank ℝ F * φ (i • x)) 0 atTop uᶜ
have apply : ∀ (ε : ℝ) (εpos : ε > 0), ∀ᶠ (n : ℝ) in atTop, ∀ x ∈ uᶜ, dist (0 x) (n ^ finrank ℝ F * φ (n • x)) < ε
Tactic: apply tendstoUniformlyOn_iff.2 (fun ε εpos ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
⊢ ∀ᶠ (n : ℝ) in atTop, ∀ x ∈ uᶜ, dist (0 x) (n ^ finrank ℝ F * φ (n • x)) < ε
have obtain : ∀ (δ : ℝ) (δpos : δ > 0) (h'u : ball 0 δ ⊆ u),
  ∀ᶠ (n : ℝ) in atTop, ∀ x ∈ uᶜ, dist (0 x) (n ^ finrank ℝ F * φ (n • x)) < ε
Tactic: obtain ⟨δ, δpos, h'u⟩ : ∃ δ > 0, ball 0 δ ⊆ u := Metric.isOpen_iff.1 u_open _ hu
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
⊢ ∃ M > 0, ∀ ⦃x : F⦄, Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
have rcases : ∀ (M : ℝ)
  (hM : ∀ ⦃x : F⦄, Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε),
  ∃ M > 0, ∀ ⦃x : F⦄, Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
Tactic: rcases (hasBasis_cobounded_compl_closedBall (0 : F)).eventually_iff.1
        ((tendsto_order.1 h).2 (δ ^ finrank ℝ F * ε) (by positivity)) with ⟨M, -, hM⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
hM : ∀ ⦃x : F⦄, Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
⊢ ∃ M > 0, ∀ ⦃x : F⦄, Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
have refine : ∀ (x : F) (hx : Membership.mem (γ := Set F) (closedBall 0 (max M 1))ᶜ x),
  Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x
Tactic: refine ⟨max M 1, zero_lt_one.trans_le (le_max_right _ _), fun x hx ↦ hM ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (hypothesis)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
hM : ∀ ⦃x : F⦄, Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
x : F
hx : Membership.mem (γ := Set F) (closedBall 0 (max M 1))ᶜ x
⊢ Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x
have hx₁ : M < ‖x‖ ∧ 1 < ‖x‖
Tactic: simp only [mem_compl_iff, mem_closedBall, dist_zero_right, le_max_iff, not_or, not_le] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
⊢ ∀ᶠ (n : ℝ) in atTop, ∀ x ∈ uᶜ, dist (0 x) (n ^ finrank ℝ F * φ (n • x)) < ε
have obtain : ∀ (M : ℝ) (Mpos : M > 0)
  (hM : ∀ ⦃x : F⦄, Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε),
  ∀ᶠ (n : ℝ) in atTop, ∀ x ∈ uᶜ, dist (0 x) (n ^ finrank ℝ F * φ (n • x)) < ε
Tactic: obtain ⟨M, Mpos, hM⟩ : ∃ M > 0, ∀ ⦃x : F⦄, x ∈ (closedBall 0 M)ᶜ →
        ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε := by
      rcases (hasBasis_cobounded_compl_closedBall (0 : F)).eventually_iff.1
        ((tendsto_order.1 h).2 (δ ^ finrank ℝ F * ε) (by positivity)) with ⟨M, -, hM⟩
      refine ⟨max M 1, zero_lt_one.trans_le (le_max_right _ _), fun x hx ↦ hM ?_⟩
      simp only [mem_compl_iff, mem_closedBall, dist_zero_right, le_max_iff, not_or, not_le] at hx
      simpa using hx.1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
⊢ c ∈ Ioi (M / δ) → ∀ x ∈ uᶜ, dist (0 x) (c ^ finrank ℝ F * φ (c • x)) < ε
have h₁ : ∀ (hc : M / δ < c), ∀ x ∈ uᶜ, dist (0 x) (c ^ finrank ℝ F * φ (c • x)) < ε
Tactic: (hc : M / δ < c)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
⊢ ∀ᶠ (n : ℝ) in atTop, ∀ x ∈ uᶜ, dist (0 x) (n ^ finrank ℝ F * φ (n • x)) < ε
have h₁ : ∀ (c : ℝ) (hc : M / δ < c) (x : F) (hx : x ∈ uᶜ), dist (0 x) (c ^ finrank ℝ F * φ (c • x)) < ε
Tactic: filter_upwards [Ioi_mem_atTop (M / δ)] with c (hc : M / δ < c) x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (hypothesis)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
hc : M / δ < c
x : F
hx : x ∈ uᶜ
⊢ dist (0 x) (c ^ finrank ℝ F * φ (c • x)) < ε
have cpos : 0 < c
Tactic: have cpos : 0 < c := lt_trans (by positivity) hc
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
hc : M / δ < c
x : F
hx : x ∈ uᶜ
cpos : 0 < c
⊢ dist (0 x) (c ^ finrank ℝ F * φ (c • x)) < ε
have h₁ : c ^ finrank ℝ F * φ (c • x) < ε
Tactic: suffices c ^ finrank ℝ F * φ (c • x) < ε by simpa [abs_of_nonneg (hφ _), abs_of_nonneg cpos.le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (hypothesis)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
hc : M / δ < c
x : F
hx : x ∈ uᶜ
cpos : 0 < c
⊢ δ ≤ ‖x‖
have this : Membership.mem (γ := Set F) (ball 0 δ)ᶜ x
Tactic: have : x ∈ (ball 0 δ)ᶜ := fun h ↦ hx (h'u h)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (hypothesis)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
hc : M / δ < c
x : F
hx : x ∈ uᶜ
cpos : 0 < c
⊢ c ^ finrank ℝ F * φ (c • x) < ε
have hδx : δ ≤ ‖x‖
Tactic: have hδx : δ ≤ ‖x‖ := by
      have : x ∈ (ball 0 δ)ᶜ := fun h ↦ hx (h'u h)
      simpa only [mem_compl_iff, mem_ball, dist_zero_right, not_lt]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
hc : M / δ < c
x : F
hx : x ∈ uᶜ
cpos : 0 < c
hδx : δ ≤ ‖x‖
this : δ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x)) < δ ^ finrank ℝ F * ε
⊢ c ^ finrank ℝ F * φ (c • x) < ε
have rwa : ∀ (this : c ^ finrank ℝ F * φ (c • x) < ε), c ^ finrank ℝ F * φ (c • x) < ε
Tactic: rwa [mul_lt_mul_iff_of_pos_left (by positivity)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
hc : M / δ < c
x : F
hx : x ∈ uᶜ
cpos : 0 < c
hδx : δ ≤ ‖x‖
⊢ c ^ finrank ℝ F * φ (c • x) < ε
have h₁ : δ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x)) < δ ^ finrank ℝ F * ε
Tactic: suffices δ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x)) < δ ^ finrank ℝ F * ε by
      rwa [mul_lt_mul_iff_of_pos_left (by positivity)] at this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
hc : M / δ < c
x : F
hx : x ∈ uᶜ
cpos : 0 < c
hδx : δ ≤ ‖x‖
⊢ δ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x)) ≤ ‖x‖ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x))
have ha : 0 ≤ c ^ finrank ℝ F * φ (c • x)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
hc : M / δ < c
x : F
hx : x ∈ uᶜ
cpos : 0 < c
hδx : δ ≤ ‖x‖
⊢ ‖x‖ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x)) = ‖c • x‖ ^ finrank ℝ F * φ (c • x)
have simp : ‖x‖ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x)) = c ^ finrank ℝ F * ‖x‖ ^ finrank ℝ F * φ (c • x)
Tactic: simp [norm_smul, abs_of_pos cpos, mul_pow]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
hc : M / δ < c
x : F
hx : x ∈ uᶜ
cpos : 0 < c
hδx : δ ≤ ‖x‖
⊢ ‖c • x‖ ^ finrank ℝ F * φ (c • x) < δ ^ finrank ℝ F * ε
have a : Membership.mem (γ := Set F) (closedBall 0 M)ᶜ (c • x)
Tactic: apply hM
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
hc : M / δ < c
x : F
hx : x ∈ uᶜ
cpos : 0 < c
hδx : δ ≤ ‖x‖
⊢ Membership.mem (γ := Set F) (closedBall 0 M)ᶜ (c • x)
have a : ∀ (hc : M < c * δ) (x : F) (hx : x ∈ uᶜ) (cpos : 0 < c) (hδx : δ ≤ ‖x‖),
  Membership.mem (γ := Set F) (closedBall 0 M)ᶜ (c • x)
Tactic: rw [div_lt_iff₀ δpos] at hc
Cleared hypotheses: hc, x, hx, cpos, hδx