awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hle : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
⊢ eLpNorm.{u_1, u_4} (ε := E) (∑ i ∈ Finset.range n, s.indicator (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i))) p μ ≤
    ENNReal.ofReal ε
have refine_2 : ∑ i ∈ Finset.range n, eLpNorm (s.indicator (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i))) p μ ≤ ENNReal.ofReal ε
Tactic: refine le_trans (eLpNorm_sum_le (fun i _ => ((hf₁ i).const_smul _).indicator hs) hp) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hle : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
⊢ ∑ i ∈ Finset.range n, eLpNorm (s.indicator (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i))) p μ ≤ ENNReal.ofReal ε
have this : ∀ (i : ℕ), s.indicator (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i)) = HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.indicator (f i))
Tactic: have this i : s.indicator ((n : ℝ)⁻¹ • f i) = (↑n : ℝ)⁻¹ • s.indicator (f i) :=
      indicator_const_smul _ _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hle : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
this :
  ∀ (i : ℕ), s.indicator (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i)) = HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.indicator (f i))
⊢ ∑ i ∈ Finset.range n, eLpNorm (s.indicator (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i))) p μ ≤ ENNReal.ofReal ε
have refine_2 : ∀
  (this :
    ∀ (i : ℕ),
      s.indicator (HSMul.hSMul (α := ℝ) (↑0 : ℝ)⁻¹ (f i)) = HSMul.hSMul (α := ℝ) (↑0 : ℝ)⁻¹ (s.indicator (f i))),
  ∑ i ∈ Finset.range 0, eLpNorm (s.indicator (HSMul.hSMul (α := ℝ) (↑0 : ℝ)⁻¹ (f i))) p μ ≤ ENNReal.ofReal ε
Tactic: obtain rfl | hn := eq_or_ne n 0
Cleared hypotheses: n, this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hle : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
this :
  ∀ (i : ℕ), s.indicator (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i)) = HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.indicator (f i))
refine_2 :
  ∀
    (this :
      ∀ (i : ℕ),
        s.indicator (HSMul.hSMul (α := ℝ) (↑0 : ℝ)⁻¹ (f i)) = HSMul.hSMul (α := ℝ) (↑0 : ℝ)⁻¹ (s.indicator (f i))),
    ∑ i ∈ Finset.range 0, eLpNorm (s.indicator (HSMul.hSMul (α := ℝ) (↑0 : ℝ)⁻¹ (f i))) p μ ≤ ENNReal.ofReal ε
⊢ ∑ i ∈ Finset.range n, eLpNorm (s.indicator (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i))) p μ ≤ ENNReal.ofReal ε
have refine_2₁ : ∀ (hn : n ≠ 0),
  ∑ i ∈ Finset.range n, eLpNorm (s.indicator (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i))) p μ ≤ ENNReal.ofReal ε
Tactic: obtain rfl | hn := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hle : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
this :
  ∀ (i : ℕ), s.indicator (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i)) = HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.indicator (f i))
hn : n ≠ 0
⊢ ∑ i ∈ Finset.range n, eLpNorm (s.indicator (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i))) p μ ≤ ENNReal.ofReal ε
have refine_2 : enorm (E := ℝ) (↑n : ℝ)⁻¹ * ∑ i ∈ Finset.range n, eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
Tactic: simp_rw [this, eLpNorm_const_smul, ← Finset.mul_sum]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hle : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
this :
  ∀ (i : ℕ), s.indicator (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i)) = HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.indicator (f i))
hn : n ≠ 0
⊢ enorm (E := ℝ) (↑n : ℝ)⁻¹ * ∑ i ∈ Finset.range n, eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
have refine_2 : HDiv.hDiv (α := ℝ≥0∞) (∑ i ∈ Finset.range n, eLpNorm (s.indicator (f i)) p μ) (↑n : ℝ≥0∞) ≤ ENNReal.ofReal ε
Tactic: rw [enorm_inv (by positivity), Real.enorm_natCast, ← ENNReal.div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hle : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
this :
  ∀ (i : ℕ), s.indicator (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i)) = HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.indicator (f i))
hn : n ≠ 0
⊢ HDiv.hDiv (α := ℝ≥0∞) (∑ i ∈ Finset.range n, eLpNorm (s.indicator (f i)) p μ) (↑n : ℝ≥0∞) ≤ ENNReal.ofReal ε
have refine_2 : ∑ i ∈ Finset.range n, eLpNorm (s.indicator (f i)) p μ ≤ (↑n : ℝ≥0∞) * ENNReal.ofReal ε
Tactic: refine ENNReal.div_le_of_le_mul' ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
⊢ ∃ (C : ℝ≥0),
    ∀ (i : ℕ),
      eLpNorm.{u_1, u_4} (ε := E)
          ((fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) i) p μ ≤
        (↑C : ℝ≥0∞)
have refine_3 : ∀ (C : ℝ≥0) (hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)),
  ∃ (C : ℝ≥0),
    ∀ (i : ℕ),
      eLpNorm.{u_1, u_4} (ε := E)
          ((fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) i) p μ ≤
        (↑C : ℝ≥0∞)
Tactic: obtain ⟨C, hC⟩ := hf₃
Cleared hypotheses: hf₃
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
⊢ ∃ (C : ℝ≥0),
    ∀ (i : ℕ),
      eLpNorm.{u_1, u_4} (ε := E)
          ((fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) i) p μ ≤
        (↑C : ℝ≥0∞)
have refine_3 : ∃ (C : ℝ≥0),
  ∀ (i : ℕ), eLpNorm.{u_1, u_4} (ε := E) (∑ x ∈ Finset.range i, HSMul.hSMul (α := ℝ) (↑i : ℝ)⁻¹ (f x)) p μ ≤ (↑C : ℝ≥0∞)
Tactic: simp_rw [Finset.smul_sum]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
⊢ ∃ (C : ℝ≥0),
    ∀ (i : ℕ),
      eLpNorm.{u_1, u_4} (ε := E) (∑ x ∈ Finset.range i, HSMul.hSMul (α := ℝ) (↑i : ℝ)⁻¹ (f x)) p μ ≤ (↑C : ℝ≥0∞)
have refine_3 : ∀ (n : ℕ), ∑ i ∈ Finset.range n, eLpNorm (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i)) p μ ≤ (↑C : ℝ≥0∞)
Tactic: refine ⟨C, fun n => (eLpNorm_sum_le (fun i _ => (hf₁ i).const_smul _) hp).trans ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
n : ℕ
⊢ ∑ i ∈ Finset.range n, eLpNorm (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i)) p μ ≤ (↑C : ℝ≥0∞)
have refine_3 : ∑ i ∈ Finset.range 0, eLpNorm (HSMul.hSMul (α := ℝ) (↑0 : ℝ)⁻¹ (f i)) p μ ≤ (↑C : ℝ≥0∞)
Tactic: obtain rfl | hn := eq_or_ne n 0
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
n : ℕ
refine_3 : ∑ i ∈ Finset.range 0, eLpNorm (HSMul.hSMul (α := ℝ) (↑0 : ℝ)⁻¹ (f i)) p μ ≤ (↑C : ℝ≥0∞)
⊢ ∑ i ∈ Finset.range n, eLpNorm (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i)) p μ ≤ (↑C : ℝ≥0∞)
have refine_3₁ : ∀ (hn : n ≠ 0), ∑ i ∈ Finset.range n, eLpNorm (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i)) p μ ≤ (↑C : ℝ≥0∞)
Tactic: obtain rfl | hn := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
n : ℕ
hn : n ≠ 0
⊢ ∑ i ∈ Finset.range n, eLpNorm (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i)) p μ ≤ (↑C : ℝ≥0∞)
have refine_3 : enorm (E := ℝ) (↑n : ℝ)⁻¹ * ∑ i ∈ Finset.range n, eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
Tactic: simp_rw [eLpNorm_const_smul, ← Finset.mul_sum]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
n : ℕ
hn : n ≠ 0
⊢ enorm (E := ℝ) (↑n : ℝ)⁻¹ * ∑ i ∈ Finset.range n, eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
have refine_3 : HDiv.hDiv (α := ℝ≥0∞) (∑ i ∈ Finset.range n, eLpNorm (f i) p μ) (↑n : ℝ≥0∞) ≤ (↑C : ℝ≥0∞)
Tactic: rw [enorm_inv (by positivity), Real.enorm_natCast, ← ENNReal.div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
n : ℕ
hn : n ≠ 0
⊢ HDiv.hDiv (α := ℝ≥0∞) (∑ i ∈ Finset.range n, eLpNorm (f i) p μ) (↑n : ℝ≥0∞) ≤ (↑C : ℝ≥0∞)
have refine_3 : ∑ i ∈ Finset.range n, eLpNorm (f i) p μ ≤ (↑n : ℝ≥0∞) * (↑C : ℝ≥0∞)
Tactic: refine ENNReal.div_le_of_le_mul' ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
f : ℕ → α → ℝ
hf : UniformIntegrable f p μ
⊢ UniformIntegrable (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := α → ℝ) (∑ i ∈ Finset.range n, f i) (↑n : α → ℝ)) p μ
have h : ∀ (n : ℕ),
  HDiv.hDiv (α := α → ℝ) (∑ i ∈ Finset.range n, f i) (↑n : α → ℝ) =
    HSMul.hSMul (α := ℝ) (β := α → ℝ) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)
Tactic: convert! uniformIntegrable_average hp hf using 2 with n
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
f : ℕ → α → ℝ
hf : UniformIntegrable f p μ
n : ℕ
⊢ HDiv.hDiv (α := α → ℝ) (∑ i ∈ Finset.range n, f i) (↑n : α → ℝ) =
    HSMul.hSMul (α := ℝ) (β := α → ℝ) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)
have h : ∀ (x : α),
  HDiv.hDiv (α := α → ℝ) (β := α → ℝ) (∑ i ∈ Finset.range n, f i) (↑n : α → ℝ) x =
    HSMul.hSMul (α := ℝ) (β := α → ℝ) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
fn : ι → α → β
hUI : UniformIntegrable fn p μ
⊢ UniformIntegrable (β := β)
    (fun (f : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) ↦ (↑f : α → β)) p
    μ
have refine_1 : ∀ (x : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) (f : α → β) (s : κ → ι)
  (hs : TendstoInMeasure μ (fn ∘ s) u f),
  AEStronglyMeasurable.{u_1, u_2} (β := β)
    ((fun (f : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) ↦ (↑f : α → β))
      (Subtype.mk (p := fun (x : α → β) ↦
        Membership.mem (γ := Set (α → β)) {g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} x) f sorry))
    μ
Tactic: refine ⟨fun ⟨f, s, hs⟩ => ?_, hUI.2.1.unifIntegrable_of_tendstoInMeasure u (fun i => hUI.1 i), ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
fn : ι → α → β
hUI : UniformIntegrable fn p μ
refine_1 :
  ∀ (x : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) (f : α → β) (s : κ → ι)
    (hs : TendstoInMeasure μ (fn ∘ s) u f),
    AEStronglyMeasurable.{u_1, u_2} (β := β)
      ((fun (f : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) ↦ (↑f : α → β))
        (Subtype.mk (p := fun (x : α → β) ↦
          Membership.mem (γ := Set (α → β)) {g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} x) f ⋯))
      μ
⊢ UniformIntegrable (β := β)
    (fun (f : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) ↦ (↑f : α → β)) p
    μ
have refine_2 : ∃ (C : ℝ≥0),
  ∀ (i : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))),
    eLpNorm.{u_1, u_2} (ε := β)
        ((fun (f : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) ↦
            (↑f : α → β))
          i)
        p μ ≤
      (↑C : ℝ≥0∞)
Tactic: refine ⟨fun ⟨f, s, hs⟩ => ?_, hUI.2.1.unifIntegrable_of_tendstoInMeasure u (fun i => hUI.1 i), ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
fn : ι → α → β
hUI : UniformIntegrable fn p μ
⊢ ∃ (C : ℝ≥0),
    ∀ (i : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))),
      eLpNorm.{u_1, u_2} (ε := β)
          ((fun (f : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) ↦
              (↑f : α → β))
            i)
          p μ ≤
        (↑C : ℝ≥0∞)
have refine_2 : ∀ (C : ℝ≥0) (hC : ∀ (i : ι), eLpNorm (fn i) p μ ≤ (↑C : ℝ≥0∞)),
  ∃ (C : ℝ≥0),
    ∀ (i : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))),
      eLpNorm.{u_1, u_2} (ε := β)
          ((fun (f : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) ↦
              (↑f : α → β))
            i)
          p μ ≤
        (↑C : ℝ≥0∞)
Tactic: obtain ⟨C, hC⟩ := hUI.2.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
fn : ι → α → β
hUI : UniformIntegrable fn p μ
⊢ UniformIntegrable (β := β)
    (fun
        (f :
          (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
            Type (max u_1 u_2))) ↦
      (↑f : α → β))
    p μ
have refine_1 : ∀
  (x :
    (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
      Type (max u_1 u_2)))
  (f : α → β) (s : κ → ι) (hs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (s n) x) u (𝓝 (f x))),
  AEStronglyMeasurable.{u_1, u_2} (β := β)
    ((fun
          (f :
            (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
              Type (max u_1 u_2))) ↦
        (↑f : α → β))
      (Subtype.mk (p := fun (x : α → β) ↦
        Membership.mem (γ := Set (α → β))
          {g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} x)
        f sorry))
    μ
Tactic: refine ⟨fun ⟨f, s, hs⟩ => ?_, hUI.2.1.unifIntegrable_of_ae_tendsto u (fun i => hUI.1 i), ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
fn : ι → α → β
hUI : UniformIntegrable fn p μ
refine_1 :
  ∀
    (x :
      (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
        Type (max u_1 u_2)))
    (f : α → β) (s : κ → ι) (hs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (s n) x) u (𝓝 (f x))),
    AEStronglyMeasurable.{u_1, u_2} (β := β)
      ((fun
            (f :
              (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
                Type (max u_1 u_2))) ↦
          (↑f : α → β))
        (Subtype.mk (p := fun (x : α → β) ↦
          Membership.mem (γ := Set (α → β))
            {g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} x)
          f ⋯))
      μ
⊢ UniformIntegrable (β := β)
    (fun
        (f :
          (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
            Type (max u_1 u_2))) ↦
      (↑f : α → β))
    p μ
have refine_2 : ∃ (C : ℝ≥0),
  ∀
    (i :
      (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
        Type (max u_1 u_2))),
    eLpNorm.{u_1, u_2} (ε := β)
        ((fun
              (f :
                (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
                  Type (max u_1 u_2))) ↦
            (↑f : α → β))
          i)
        p μ ≤
      (↑C : ℝ≥0∞)
Tactic: refine ⟨fun ⟨f, s, hs⟩ => ?_, hUI.2.1.unifIntegrable_of_ae_tendsto u (fun i => hUI.1 i), ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
fn : ι → α → β
hUI : UniformIntegrable fn p μ
⊢ ∃ (C : ℝ≥0),
    ∀
      (i :
        (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
          Type (max u_1 u_2))),
      eLpNorm.{u_1, u_2} (ε := β)
          ((fun
                (f :
                  (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
                    Type (max u_1 u_2))) ↦
              (↑f : α → β))
            i)
          p μ ≤
        (↑C : ℝ≥0∞)
have refine_2 : ∀ (C : ℝ≥0) (hC : ∀ (i : ι), eLpNorm (fn i) p μ ≤ (↑C : ℝ≥0∞)),
  ∃ (C : ℝ≥0),
    ∀
      (i :
        (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
          Type (max u_1 u_2))),
      eLpNorm.{u_1, u_2} (ε := β)
          ((fun
                (f :
                  (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
                    Type (max u_1 u_2))) ↦
              (↑f : α → β))
            i)
          p μ ≤
        (↑C : ℝ≥0∞)
Tactic: obtain ⟨C, hC⟩ := hUI.2.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AEStabilizer (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
s t : Set α
h : s =ᶠ[ae μ] t
⊢ Eq (α := Subgroup G) (aestabilizer G μ s) (aestabilizer G μ t)
have h₁ : ∀ (g : G),
  Membership.mem (γ := Subgroup G) (aestabilizer G μ s) g ↔ Membership.mem (γ := Subgroup G) (aestabilizer G μ t) g
Tactic: ext g
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AEStabilizer (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
s t : Set α
h : s =ᶠ[ae μ] t
g : G
⊢ Membership.mem (γ := Subgroup G) (aestabilizer G μ s) g ↔ Membership.mem (γ := Subgroup G) (aestabilizer G μ t) g
have h₁ : g • s =ᶠ[ae μ] s ↔ Membership.mem (γ := Subgroup G) (aestabilizer G μ t) g
Tactic: rw [mem_aestabilizer, mem_aestabilizer, h.congr_right, ((smul_set_ae_eq g).2 h).congr_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AEStabilizer (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
s t : Set α
h : s =ᶠ[ae μ] t
g : G
h₁ : g • s =ᶠ[ae μ] s ↔ Membership.mem (γ := Subgroup G) (aestabilizer G μ t) g
⊢ Membership.mem (γ := Subgroup G) (aestabilizer G μ s) g ↔ Membership.mem (γ := Subgroup G) (aestabilizer G μ t) g
have h₂ : g • s =ᶠ[ae μ] s ↔ g • t =ᶠ[ae μ] t
Tactic: rw [mem_aestabilizer, mem_aestabilizer, h.congr_right, ((smul_set_ae_eq g).2 h).congr_left]