-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_iInf' {f : ℕ → α → ℝ≥0∞} (h_meas : ∀ n, AEMeasurable (f n) μ)
    (h_anti : ∀ᵐ a ∂μ, Antitone (fun i ↦ f i a)) (h_fin : ∫⁻ a, f 0 a ∂μ ≠ ∞) :
    ∫⁻ a, ⨅ n, f n a ∂μ = ⨅ n, ∫⁻ a, f n a ∂μ

Proof state:
case neg
α : Type u_1
m✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
n m : ℕ
hnm : n ≤ m
x : α
hx : x ∉ aeSeqSet h_meas p
⊢ ⋯.some ≤ ⋯.some

Tactic:
exact le_rfl

Result:
no goals

Proof state:
case neg
α : Type u_1
m✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
n m : ℕ
hnm : n ≤ m
x : α
hx : x ∉ aeSeqSet h_meas p
⊢ aeSeq h_meas p m x ≤ aeSeq h_meas p n x

Tactic:
simp only [aeSeq, hx, if_false]

Result:
case neg
α : Type u_1
m✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
n m : ℕ
hnm : n ≤ m
x : α
hx : x ∉ aeSeqSet h_meas p
⊢ ⋯.some ≤ ⋯.some

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
⊢ Antitone (aeSeq h_meas p)

Tactic:
intro n m hnm x

Result:
α : Type u_1
m✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
n m : ℕ
hnm : n ≤ m
x : α
⊢ aeSeq h_meas p m x ≤ aeSeq h_meas p n x

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_mono : Antitone (aeSeq h_meas p)
⊢ ∫⁻ (a : α), (⨅ n, aeSeq h_meas p n) a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ

Tactic:
simp_rw [iInf_apply]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_mono : Antitone (aeSeq h_meas p)
⊢ ∫⁻ (a : α), ⨅ i, aeSeq h_meas p i a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
⊢ ∫⁻ (a : α), ⨅ n, f n a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ

Tactic:
simp_rw [← iInf_apply]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
⊢ ∫⁻ (a : α), (⨅ i, f i) a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_mono : Antitone (aeSeq h_meas p)
⊢ ∫⁻ (a : α), aeSeq h_meas p 0 a ∂μ ≠ ⊤

Tactic:
rwa [lintegral_congr_ae (aeSeq.aeSeq_n_eq_fun_n_ae h_meas hp 0)]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_mono : Antitone (aeSeq h_meas p)
⊢ ⨅ n, ∫⁻ (a : α), aeSeq h_meas p n a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ

Tactic:
congr

Result:
case e_s
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_mono : Antitone (aeSeq h_meas p)
⊢ (fun n => ∫⁻ (a : α), aeSeq h_meas p n a ∂μ) = fun n => ∫⁻ (a : α), f n a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_mono : Antitone (aeSeq h_meas p)
⊢ ∫⁻ (a : α), (⨅ i, f i) a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ

Tactic:
rw [lintegral_congr_ae (aeSeq.iInf h_meas hp).symm]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_mono : Antitone (aeSeq h_meas p)
⊢ ∫⁻ (a : α), (⨅ n, aeSeq h_meas p n) a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ

Proof state:
case e_s
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_mono : Antitone (aeSeq h_meas p)
⊢ (fun n => ∫⁻ (a : α), aeSeq h_meas p n a ∂μ) = fun n => ∫⁻ (a : α), f n a ∂μ

Tactic:
exact funext fun n ↦ lintegral_congr_ae (aeSeq.aeSeq_n_eq_fun_n_ae h_meas hp n)

Result:
no goals

Proof state:
case pos
α : Type u_1
m✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
n m : ℕ
hnm : n ≤ m
x : α
hx : x ∈ aeSeqSet h_meas p
⊢ aeSeq h_meas p m x ≤ aeSeq h_meas p n x

Tactic:
exact aeSeq.prop_of_mem_aeSeqSet h_meas hx hnm

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_mono : Antitone (aeSeq h_meas p)
⊢ ∫⁻ (a : α), ⨅ i, aeSeq h_meas p i a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ

Tactic:
rw [lintegral_iInf (aeSeq.measurable h_meas p) h_ae_seq_mono]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_mono : Antitone (aeSeq h_meas p)
⊢ ⨅ n, ∫⁻ (a : α), aeSeq h_meas p n a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ

α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_mono : Antitone (aeSeq h_meas p)
⊢ ∫⁻ (a : α), aeSeq h_meas p 0 a ∂μ ≠ ⊤