awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p : ℝ
hp : 1 ≤ p
h :
  Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ rexp (-‖x‖ ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ HPow.hPow (β := ℝ) ‖x‖ 0 * rexp (-‖x‖ ^ p))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ rexp (-‖x‖ ^ p)) = π * Real.Gamma (2 / p + 1)
have h₁ : π * Real.Gamma (2 / p + 1) = 2 * π / p * Real.Gamma (HAdd.hAdd (α := ℝ) 0 2 / p)
Tactic: convert! (integral_rpow_mul_exp_neg_rpow hp (by linarith : (-2 : ℝ) < 0)) using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p : ℝ
hp : 1 ≤ p
⊢ Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ rexp (-‖x‖ ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ HPow.hPow (β := ℝ) ‖x‖ 0 * rexp (-‖x‖ ^ p))
have h : Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ rexp (-‖x‖ ^ p))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ 1 * rexp (-‖x‖ ^ p))
Tactic: simp_rw [rpow_zero, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p : ℝ
hp : 1 ≤ p
⊢ p ≠ 0
have linarith : p = 0 → -1 + (1 - p) + (p - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p : ℝ
hp : 1 ≤ p
⊢ π * Real.Gamma (2 / p + 1) = 2 * π / p * Real.Gamma (HAdd.hAdd (α := ℝ) 0 2 / p)
have h : π * (2 / p * Real.Gamma (2 / p)) = 2 * π / p * Real.Gamma (2 / p)
Tactic: rw [zero_add, Real.Gamma_add_one (div_ne_zero two_ne_zero (by linarith))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p b : ℝ
hp : 1 ≤ p
hb : 0 < b
⊢ LT.lt (α := ℝ) (-2) 0
have linarith : LE.le (α := ℝ) 0 (-2) → HMul.hMul (α := ℝ) 2 (-1) + HSub.hSub (α := ℝ) 0 (-2) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p b : ℝ
hp : 1 ≤ p
hb : 0 < b
linarith : LE.le (α := ℝ) 0 (-2) → HMul.hMul (α := ℝ) 2 (-1) + HSub.hSub (α := ℝ) 0 (-2) = 0
⊢ LT.lt (α := ℝ) (-2) 0
have linarith₁ : LE.le (α := ℝ) 0 (-2) → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p b : ℝ
hp : 1 ≤ p
hb : 0 < b
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ rexp (-b * ‖x‖ ^ p)) =
    π * b ^ (-2 / p) * Real.Gamma (2 / p + 1)
have h : Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ rexp (-b * ‖x‖ ^ p))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ HPow.hPow (β := ℝ) ‖x‖ 0 * rexp (-b * ‖x‖ ^ p))
Tactic: convert! (integral_rpow_mul_exp_neg_mul_rpow hp (by linarith : (-2 : ℝ) < 0)) hb using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p b : ℝ
hp : 1 ≤ p
hb : 0 < b
h :
  Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ rexp (-b * ‖x‖ ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦
      HPow.hPow (β := ℝ) ‖x‖ 0 * rexp (-b * ‖x‖ ^ p))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ rexp (-b * ‖x‖ ^ p)) =
    π * b ^ (-2 / p) * Real.Gamma (2 / p + 1)
have h₁ : π * b ^ (-2 / p) * Real.Gamma (2 / p + 1) =
  2 * π / p * b ^ (-HAdd.hAdd (α := ℝ) 0 2 / p) * Real.Gamma (HAdd.hAdd (α := ℝ) 0 2 / p)
Tactic: convert! (integral_rpow_mul_exp_neg_mul_rpow hp (by linarith : (-2 : ℝ) < 0)) hb using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p b : ℝ
hp : 1 ≤ p
hb : 0 < b
⊢ Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ rexp (-b * ‖x‖ ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦
      HPow.hPow (β := ℝ) ‖x‖ 0 * rexp (-b * ‖x‖ ^ p))
have h : Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ rexp (-b * ‖x‖ ^ p))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ 1 * rexp (-b * ‖x‖ ^ p))
Tactic: simp_rw [rpow_zero, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p b : ℝ
hp : 1 ≤ p
hb : 0 < b
⊢ p ≠ 0
have linarith : p = 0 → -1 + (1 - p) + (p - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p b : ℝ
hp : 1 ≤ p
hb : 0 < b
⊢ π * b ^ (-2 / p) * Real.Gamma (2 / p + 1) =
    2 * π / p * b ^ (-HAdd.hAdd (α := ℝ) 0 2 / p) * Real.Gamma (HAdd.hAdd (α := ℝ) 0 2 / p)
have h : π * b ^ (-2 / p) * (2 / p * Real.Gamma (2 / p)) = 2 * π / p * b ^ (-2 / p) * Real.Gamma (2 / p)
Tactic: rw [zero_add, Real.Gamma_add_one (div_ne_zero two_ne_zero (by linarith))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Indicator (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) B : ℝ≥0∞) (∞ : ℝ≥0∞)
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)) L
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) A) : Filter ℝ≥0∞)
have simp_rw : Tendsto (fun (i : ι) ↦ ∫⁻ (a : α), (As i).indicator 1 a ∂μ) L (𝓝 (∫⁻ (a : α), A.indicator 1 a ∂μ))
Tactic: simp_rw [← MeasureTheory.lintegral_indicator_one A_mble,
           ← MeasureTheory.lintegral_indicator_one (As_mble _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Indicator (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) B : ℝ≥0∞) (∞ : ℝ≥0∞)
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ Tendsto (fun (i : ι) ↦ ∫⁻ (a : α), (As i).indicator 1 a ∂μ) L (𝓝 (∫⁻ (a : α), A.indicator 1 a ∂μ))
have refine_1 : ∀ (x : ι), Measurable (β := ℝ≥0∞) ((As x).indicator 1)
Tactic: refine tendsto_lintegral_filter_of_dominated_convergence (B.indicator (1 : α → ℝ≥0∞))
          (Eventually.of_forall ?_) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Indicator (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) B : ℝ≥0∞) (∞ : ℝ≥0∞)
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
refine_1 : ∀ (x : ι), Measurable (β := ℝ≥0∞) ((As x).indicator 1)
⊢ Tendsto (fun (i : ι) ↦ ∫⁻ (a : α), (As i).indicator 1 a ∂μ) L (𝓝 (∫⁻ (a : α), A.indicator 1 a ∂μ))
have refine_2 : ∀ᶠ (n : ι) in L, ∀ᵐ (a : α) ∂μ, LE.le (α := ℝ≥0∞) ((As n).indicator 1 a) (B.indicator 1 a)
Tactic: refine tendsto_lintegral_filter_of_dominated_convergence (B.indicator (1 : α → ℝ≥0∞))
          (Eventually.of_forall ?_) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Indicator (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) B : ℝ≥0∞) (∞ : ℝ≥0∞)
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
refine_1 : ∀ (x : ι), Measurable (β := ℝ≥0∞) ((As x).indicator 1)
refine_2 : ∀ᶠ (n : ι) in L, ∀ᵐ (a : α) ∂μ, LE.le (α := ℝ≥0∞) ((As n).indicator 1 a) (B.indicator 1 a)
⊢ Tendsto (fun (i : ι) ↦ ∫⁻ (a : α), (As i).indicator 1 a ∂μ) L (𝓝 (∫⁻ (a : α), A.indicator 1 a ∂μ))
have refine_3 : ∫⁻ (a : α), B.indicator 1 a ∂μ ≠ ∞
Tactic: refine tendsto_lintegral_filter_of_dominated_convergence (B.indicator (1 : α → ℝ≥0∞))
          (Eventually.of_forall ?_) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Indicator (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) B : ℝ≥0∞) (∞ : ℝ≥0∞)
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
refine_1 : ∀ (x : ι), Measurable (β := ℝ≥0∞) ((As x).indicator 1)
refine_2 : ∀ᶠ (n : ι) in L, ∀ᵐ (a : α) ∂μ, LE.le (α := ℝ≥0∞) ((As n).indicator 1 a) (B.indicator 1 a)
refine_3 : ∫⁻ (a : α), B.indicator 1 a ∂μ ≠ ∞
⊢ Tendsto (fun (i : ι) ↦ ∫⁻ (a : α), (As i).indicator 1 a ∂μ) L (𝓝 (∫⁻ (a : α), A.indicator 1 a ∂μ))
have refine_4 : ∀ᵐ (a : α) ∂μ, Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ (As n).indicator 1 a) L (𝓝 (A.indicator 1 a))
Tactic: refine tendsto_lintegral_filter_of_dominated_convergence (B.indicator (1 : α → ℝ≥0∞))
          (Eventually.of_forall ?_) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Indicator (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) B : ℝ≥0∞) (∞ : ℝ≥0∞)
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ ∀ᶠ (n : ι) in L, ∀ᵐ (a : α) ∂μ, LE.le (α := ℝ≥0∞) ((As n).indicator 1 a) (B.indicator 1 a)
have h : ∀ (i : ι) (hi : As i ⊆ B), ∀ᵐ (a : α) ∂μ, LE.le (α := ℝ≥0∞) ((As i).indicator 1 a) (B.indicator 1 a)
Tactic: filter_upwards [As_le_B] with i hi
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Indicator (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) B : ℝ≥0∞) (∞ : ℝ≥0∞)
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
i : ι
hi : As i ⊆ B
x : α
⊢ LE.le (α := ℝ≥0∞) ((As i).indicator 1 x) (B.indicator 1 x)
have h₁ : LE.le (α := ℝ≥0∞) 0 (1 x)
Tactic: grw [hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Indicator (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) B : ℝ≥0∞) (∞ : ℝ≥0∞)
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
i : ι
hi : As i ⊆ B
x : α
h₁ : LE.le (α := ℝ≥0∞) 0 (1 x)
⊢ LE.le (α := ℝ≥0∞) ((As i).indicator 1 x) (B.indicator 1 x)
have grw : LE.le (α := ℝ≥0∞) (B.indicator 1 x) (B.indicator 1 x)
Tactic: grw [hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Indicator (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) B : ℝ≥0∞) (∞ : ℝ≥0∞)
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ ∫⁻ (a : α), B.indicator 1 a ∂μ ≠ ∞
have refine_3 : ∀ (B_finmeas : ∫⁻ (a : α), B.indicator 1 a ∂μ ≠ ∞) (As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B)
  (h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A), ∫⁻ (a : α), B.indicator 1 a ∂μ ≠ ∞
Tactic: rwa [← lintegral_indicator_one B_mble] at B_finmeas
Cleared hypotheses: B_finmeas, As_le_B, h_lim
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Indicator (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) B : ℝ≥0∞) (∞ : ℝ≥0∞)
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)) L
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) A) : Filter ℝ≥0∞)
have inl : ∀ [IsCountablyGenerated.{u_2} (α := ι) ⊥] (As_le_B : ∀ᶠ (i : ι) in ⊥, As i ⊆ B)
  (h_lim : ∀ (x : α), ∀ᶠ (i : ι) in ⊥, x ∈ As i ↔ x ∈ A),
  Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)) ⊥
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) A) : Filter ℝ≥0∞)
Tactic: rcases L.eq_or_neBot with rfl | _
Cleared hypotheses: L, inst_1, As_le_B, h_lim
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Indicator (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) B : ℝ≥0∞) (∞ : ℝ≥0∞)
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
inl :
  ∀ [IsCountablyGenerated.{u_2} (α := ι) ⊥] (As_le_B : ∀ᶠ (i : ι) in ⊥, As i ⊆ B)
    (h_lim : ∀ (x : α), ∀ᶠ (i : ι) in ⊥, x ∈ As i ↔ x ∈ A),
    Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)) ⊥
      (𝓝 ((μ : (a : Set α) → ℝ≥0∞) A) : Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)) L
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) A) : Filter ℝ≥0∞)
have inr : L.NeBot →
  Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)) L
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) A) : Filter ℝ≥0∞)
Tactic: rcases L.eq_or_neBot with rfl | _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Indicator (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) B : ℝ≥0∞) (∞ : ℝ≥0∞)
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
h : L.NeBot
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)) L
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) A) : Filter ℝ≥0∞)
have apply : MeasurableSet A
Tactic: apply tendsto_measure_of_ae_tendsto_indicator L ?_ As_mble B_mble B_finmeas As_le_B
        (ae_of_all μ h_lim)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Indicator (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
inst_2 : IsFiniteMeasure μ
As_mble : ∀ (i : ι), MeasurableSet (As i)
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)) L
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) A) : Filter ℝ≥0∞)
have inl : ∀ [IsCountablyGenerated.{u_2} (α := ι) ⊥] (h_lim : ∀ (x : α), ∀ᶠ (i : ι) in ⊥, x ∈ As i ↔ x ∈ A),
  Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)) ⊥
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) A) : Filter ℝ≥0∞)
Tactic: rcases L.eq_or_neBot with rfl | _
Cleared hypotheses: L, inst_1, h_lim
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Indicator (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
inst_2 : IsFiniteMeasure μ
As_mble : ∀ (i : ι), MeasurableSet (As i)
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
inl :
  ∀ [IsCountablyGenerated.{u_2} (α := ι) ⊥] (h_lim : ∀ (x : α), ∀ᶠ (i : ι) in ⊥, x ∈ As i ↔ x ∈ A),
    Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)) ⊥
      (𝓝 ((μ : (a : Set α) → ℝ≥0∞) A) : Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)) L
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) A) : Filter ℝ≥0∞)
have inr : L.NeBot →
  Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)) L
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) A) : Filter ℝ≥0∞)
Tactic: rcases L.eq_or_neBot with rfl | _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Indicator (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
inst_2 : IsFiniteMeasure μ
As_mble : ∀ (i : ι), MeasurableSet (As i)
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
h : L.NeBot
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)) L
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) A) : Filter ℝ≥0∞)
have apply : MeasurableSet A
Tactic: apply tendsto_measure_of_ae_tendsto_indicator_of_isFiniteMeasure L ?_ As_mble (ae_of_all μ h_lim)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s : Set α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
C : ℝ≥0∞
hC : ‖C‖ₑ ≠ ∞
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ₑ ≤ C
⊢ LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [Measure.restrict_apply_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
⊢ IntegrableOn f univ μ ↔ Integrable f μ
have rw : Integrable f (μ.restrict univ) ↔ Integrable f μ
Tactic: rw [IntegrableOn, Measure.restrict_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
rw : Integrable f (μ.restrict univ) ↔ Integrable f μ
⊢ IntegrableOn f univ μ ↔ Integrable f μ
have rw₁ : Integrable f μ ↔ Integrable f μ
Tactic: rw [IntegrableOn, Measure.restrict_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
C : ε'
hC : ‖C‖ₑ ≠ ∞
⊢ IntegrableOn.{u_1, u_4} (ε := ε') (fun (x : α) ↦ C) s μ ↔
    ‖C‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : Integrable.{u_4, u_1} (ε := ε') (fun (x : α) ↦ C) (μ.restrict s) ↔
  ‖C‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [IntegrableOn, integrable_const_iff_enorm hC, isFiniteMeasure_restrict, lt_top_iff_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
C : ε'
hC : ‖C‖ₑ ≠ ∞
rw :
  Integrable.{u_4, u_1} (ε := ε') (fun (x : α) ↦ C) (μ.restrict s) ↔
    ‖C‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IntegrableOn.{u_1, u_4} (ε := ε') (fun (x : α) ↦ C) s μ ↔
    ‖C‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw₁ : ‖C‖ₑ = 0 ∨ IsFiniteMeasure (μ.restrict s) ↔ ‖C‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [IntegrableOn, integrable_const_iff_enorm hC, isFiniteMeasure_restrict, lt_top_iff_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
C : ε'
hC : ‖C‖ₑ ≠ ∞
rw :
  Integrable.{u_4, u_1} (ε := ε') (fun (x : α) ↦ C) (μ.restrict s) ↔
    ‖C‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw₁ :
  ‖C‖ₑ = 0 ∨ IsFiniteMeasure (μ.restrict s) ↔
    ‖C‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IntegrableOn.{u_1, u_4} (ε := ε') (fun (x : α) ↦ C) s μ ↔
    ‖C‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw₂ : ‖C‖ₑ = 0 ∨ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔
  ‖C‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [IntegrableOn, integrable_const_iff_enorm hC, isFiniteMeasure_restrict, lt_top_iff_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
C : ε'
hC : ‖C‖ₑ ≠ ∞
rw :
  Integrable.{u_4, u_1} (ε := ε') (fun (x : α) ↦ C) (μ.restrict s) ↔
    ‖C‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw₁ :
  ‖C‖ₑ = 0 ∨ IsFiniteMeasure (μ.restrict s) ↔
    ‖C‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw₂ :
  ‖C‖ₑ = 0 ∨ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔
    ‖C‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IntegrableOn.{u_1, u_4} (ε := ε') (fun (x : α) ↦ C) s μ ↔
    ‖C‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw₃ : ‖C‖ₑ = 0 ∨ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔
  ‖C‖ₑ = 0 ∨ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [IntegrableOn, integrable_const_iff_enorm hC, isFiniteMeasure_restrict, lt_top_iff_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (hypothesis)
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s t : Set α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
h : IntegrableOn f s (μ.restrict t)
⊢ IntegrableOn f (s ∩ t) μ
have this : IntegrableOn f (s ∩ t) (μ.restrict t)
Tactic: have := h.mono_set (inter_subset_left (t := t))
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s t : Set α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
h : IntegrableOn f s (μ.restrict t)
this : IntegrableOn f (s ∩ t) (μ.restrict t)
⊢ IntegrableOn f (s ∩ t) μ
have rwa : ∀ (this : Integrable f ((μ.restrict t).restrict (s ∩ t))), IntegrableOn f (s ∩ t) μ
Tactic: rwa [IntegrableOn, μ.restrict_restrict_of_subset inter_subset_right] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
Goal:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s t : Set α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
h : IntegrableOn f s (μ.restrict t)
this : IntegrableOn f (s ∩ t) (μ.restrict t)
rwa : ∀ (this : Integrable f ((μ.restrict t).restrict (s ∩ t))), IntegrableOn f (s ∩ t) μ
⊢ IntegrableOn f (s ∩ t) μ
have rwa₁ : ∀ (this : Integrable f (μ.restrict (s ∩ t))), IntegrableOn f (s ∩ t) μ
Tactic: rwa [IntegrableOn, μ.restrict_restrict_of_subset inter_subset_right] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (hypothesis)
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
f g : α → ε'
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
hf : IntegrableOn f s μ
hg : IntegrableOn g sᶜ μ
⊢ Integrable (s.piecewise (β := fun (a : α) ↦ ε') f g) μ
have hf₁ : Integrable f (μ.restrict s)
Tactic: rw [IntegrableOn] at hf hg
Cleared hypotheses: hf, hg