awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Filter.Ultrafilter.Defs (goal)
Goal:
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m (↑g : Filter β) ⊓ 𝓟 s
this : f.NeBot
⊢ (↑(map m (ofComapInfPrincipal (s := s) h)) : Filter β) ≤ (↑g : Filter β)
have m₁ : Filter.map m (Filter.comap m (↑g : Filter β)) ⊓ Filter.map m (𝓟 s) =
  Filter.map m (Filter.comap m (↑g : Filter β)) ⊓ 𝓟 (m '' s)
Tactic: calc
    Filter.map m (of f) ≤ Filter.map m f := map_mono (of_le _)
    _ ≤ (Filter.map m <| Filter.comap m g) ⊓ Filter.map m (𝓟 s) := map_inf_le
    _ = (Filter.map m <| Filter.comap m g) ⊓ (𝓟 <| m '' s) := by rw [map_principal]
    _ ≤ ↑g ⊓ (𝓟 <| m '' s) := inf_le_inf_right _ map_comap_le
    _ = ↑g := inf_of_le_left (le_principal_iff.mpr h)
-- Lean 4 proof step from Mathlib.Probability.Independence.Integrable (goal)
Goal:
Ω : Type u_1
E : Type u_2
F : Type u_3
inst : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ∞
hℒp : MemLp f p μ
h'f : ¬∀ᵐ (ω : Ω) ∂μ, f ω = 0
hindep : f ⟂ᵢ[μ] g
⊢ ∃ (c : ℝ≥0), 0 < c ∧ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ ‖f ω‖₊} : ℝ≥0∞)
have contrapose! : ∀ (h'f : ∀ (c : ℝ≥0) (_ : 0 < c), LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ ‖f ω‖₊} : ℝ≥0∞) (0 : ℝ≥0∞)),
  ∀ᵐ (ω : Ω) ∂μ, f ω = 0
Tactic: contrapose! h'f
Cleared hypotheses: h'f
-- Lean 4 proof step from Mathlib.Probability.Independence.Integrable (hypothesis)
Goal:
Ω : Type u_1
E : Type u_2
F : Type u_3
inst : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ∞
hℒp : MemLp f p μ
hindep : f ⟂ᵢ[μ] g
h'f : ∀ (c : ℝ≥0) (_ : 0 < c), LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ ‖f ω‖₊} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∀ᵐ (ω : Ω) ∂μ, f ω = 0
have A : ∀ (c : ℝ≥0) (hc : 0 < c), ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖₊ < c
Tactic: have A (c : ℝ≥0) (hc : 0 < c) : ∀ᵐ ω ∂μ, ‖f ω‖₊ < c := by simpa [ae_iff] using h'f c hc
-- Lean 4 proof step from Mathlib.Probability.Independence.Integrable (goal)
Goal:
Ω : Type u_1
E : Type u_2
F : Type u_3
inst : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ∞
hℒp : MemLp f p μ
hindep : f ⟂ᵢ[μ] g
h'f : ∀ (c : ℝ≥0) (_ : 0 < c), LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ ‖f ω‖₊} : ℝ≥0∞) (0 : ℝ≥0∞)
A : ∀ (c : ℝ≥0) (hc : 0 < c), ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖₊ < c
⊢ ∀ᵐ (ω : Ω) ∂μ, f ω = 0
have obtain : ∀ (u : ℕ → ℝ≥0) (u_pos : ∀ (n : ℕ), 0 < u n) (u_lim : Tendsto u atTop (𝓝 0)), ∀ᵐ (ω : Ω) ∂μ, f ω = 0
Tactic: obtain ⟨u, -, u_pos, u_lim⟩ : ∃ u, StrictAnti u ∧ (∀ (n : ℕ), 0 < u n)
      ∧ Tendsto u atTop (𝓝 0) := exists_seq_strictAnti_tendsto (0 : ℝ≥0)
-- Lean 4 proof step from Mathlib.Probability.Independence.Integrable (goal)
Goal:
Ω : Type u_1
E : Type u_2
F : Type u_3
inst : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ∞
hℒp : MemLp f p μ
hindep : f ⟂ᵢ[μ] g
h'f : ∀ (c : ℝ≥0) (_ : 0 < c), LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ ‖f ω‖₊} : ℝ≥0∞) (0 : ℝ≥0∞)
A : ∀ (c : ℝ≥0) (hc : 0 < c), ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖₊ < c
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
⊢ ∀ᵐ (ω : Ω) ∂μ, f ω = 0
have h : ∀ (ω : Ω) (hω : ∀ (i : ℕ), ‖f ω‖₊ < u i), f ω = 0
Tactic: filter_upwards [ae_all_iff.2 (fun n ↦ A (u n) (u_pos n))] with ω hω
-- Lean 4 proof step from Mathlib.Probability.Independence.Integrable (goal)
Goal:
Ω : Type u_1
E : Type u_2
F : Type u_3
inst : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ∞
hℒp : MemLp f p μ
h'f : ¬∀ᵐ (ω : Ω) ∂μ, f ω = 0
hindep : f ⟂ᵢ[μ] g
⊢ IsProbabilityMeasure μ
have obtain : ∀ (c : ℝ≥0) (c_pos : 0 < c) (hc : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ ‖f ω‖₊} : ℝ≥0∞)),
  IsProbabilityMeasure μ
Tactic: obtain ⟨c, c_pos, hc⟩ : ∃ (c : ℝ≥0), 0 < c ∧ 0 < μ {ω | c ≤ ‖f ω‖₊} := by
    contrapose! h'f
    have A (c : ℝ≥0) (hc : 0 < c) : ∀ᵐ ω ∂μ, ‖f ω‖₊ < c := by simpa [ae_iff] using h'f c hc
    obtain ⟨u, -, u_pos, u_lim⟩ : ∃ u, StrictAnti u ∧ (∀ (n : ℕ), 0 < u n)
      ∧ Tendsto u atTop (𝓝 0) := exists_seq_strictAnti_tendsto (0 : ℝ≥0)
    filter_upwards [ae_all_iff.2 (fun n ↦ A (u n) (u_pos n))] with ω hω
    simpa using ge_of_tendsto' u_lim (fun i ↦ (hω i).le)
-- Lean 4 proof step from Mathlib.Probability.Independence.Integrable (hypothesis)
Goal:
Ω : Type u_1
E : Type u_2
F : Type u_3
inst : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ∞
hℒp : MemLp f p μ
h'f : ¬∀ᵐ (ω : Ω) ∂μ, f ω = 0
hindep : f ⟂ᵢ[μ] g
c : ℝ≥0
c_pos : 0 < c
hc : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ ‖f ω‖₊} : ℝ≥0∞)
⊢ IsProbabilityMeasure μ
have h'c : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ ‖f ω‖₊} : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have h'c : μ {ω | c ≤ ‖f ω‖₊} < ∞ := hℒp.meas_ge_lt_top hp hp' c_pos.ne'
-- Lean 4 proof step from Mathlib.Probability.Independence.Integrable (hypothesis)
Goal:
Ω : Type u_1
E : Type u_2
F : Type u_3
inst : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ∞
hℒp : MemLp f p μ
h'f : ¬∀ᵐ (ω : Ω) ∂μ, f ω = 0
hindep : f ⟂ᵢ[μ] g
c : ℝ≥0
c_pos : 0 < c
hc : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ ‖f ω‖₊} : ℝ≥0∞)
h'c : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ ‖f ω‖₊} : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IsProbabilityMeasure μ
have this : (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' {x : E | c ≤ ‖x‖₊} ∩ g ⁻¹' Set.univ) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' {x : E | c ≤ ‖x‖₊}) : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' Set.univ) : ℝ≥0∞)
Tactic: have := hindep.measure_inter_preimage_eq_mul {x | c ≤ ‖x‖₊} Set.univ
    (isClosed_le continuous_const continuous_nnnorm).measurableSet MeasurableSet.univ
-- Lean 4 proof step from Mathlib.Probability.Independence.Integrable (hypothesis)
Goal:
Ω : Type u_1
E : Type u_2
F : Type u_3
inst : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ∞
hℒp : MemLp f p μ
h'f : ¬∀ᵐ (ω : Ω) ∂μ, f ω = 0
hindep : f ⟂ᵢ[μ] g
c : ℝ≥0
c_pos : 0 < c
hc : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ ‖f ω‖₊} : ℝ≥0∞)
h'c : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ ‖f ω‖₊} : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' {x : E | c ≤ ‖x‖₊} ∩ g ⁻¹' Set.univ) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' {x : E | c ≤ ‖x‖₊}) : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' Set.univ) : ℝ≥0∞)
⊢ IsProbabilityMeasure μ
have this₁ : (μ : (a : Set Ω) → ℝ≥0∞) {a : Ω | c ≤ ‖f a‖₊} =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {a : Ω | c ≤ ‖f a‖₊} : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
Tactic: simp only [Set.preimage_setOf_eq, Set.preimage_univ, Set.inter_univ] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
κ : Kernel α β
a : α
s : Set γ
hs : MeasurableSet s
⊢ (((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s =
    ∫⁻ (b : β), (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) a
have rw : ((Measure.bind.{u_2, u_3} (α := β) (mα := mβ) ((κ : (a : α) → Measure β) a) (⇑η : (a : β) → Measure γ) : Measure γ) :
      (a : Set γ) → ℝ≥0∞)
    s =
  ∫⁻ (b : β), (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) a
Tactic: rw [comp_apply, Measure.bind_apply hs (Kernel.aemeasurable _)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
κ : Kernel α β
a : α
s : Set γ
hs : MeasurableSet s
rw :
  ((Measure.bind.{u_2, u_3} (α := β) (mα := mβ) ((κ : (a : α) → Measure β) a) (⇑η : (a : β) → Measure γ) : Measure γ) :
        (a : Set γ) → ℝ≥0∞)
      s =
    ∫⁻ (b : β), (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) a
⊢ (((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s =
    ∫⁻ (b : β), (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) a
have rw₁ : ∫⁻ (a : β), (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) a =
  ∫⁻ (b : β), (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) a
Tactic: rw [comp_apply, Measure.bind_apply hs (Kernel.aemeasurable _)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
a : α
⊢ (((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ ≤
    HMul.hMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) η.bound
have rw : ∫⁻ (b : β), (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ ∂(κ : (a : α) → Measure β) a ≤
  HMul.hMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) η.bound
Tactic: rw [comp_apply' _ _ _ .univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
⊢ Eq (α := Kernel α γ) (0 ∘ₖ κ) 0
have h : ∀ (a : α) (s : Set γ),
  MeasurableSet s →
    Eq (α := ℝ≥0∞) ((((0 ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
      (((((0 : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel β γ
⊢ Eq (α := Kernel α γ) (κ ∘ₖ 0) 0
have h : ∀ (a : α) (s : Set γ),
  MeasurableSet s →
    Eq (α := ℝ≥0∞) ((((κ ∘ₖ 0 : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
      (((((0 : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ Kernel.id ∘ₖ κ = κ
have h : ∀ (a : α) (s : Set β) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((((Kernel.id ∘ₖ κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext a s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
Goal:
β : Type u_2
γ : Type u_3
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel β γ
⊢ κ ∘ₖ Kernel.id = κ
have h : ∀ (a : β) (s : Set γ) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((((κ ∘ₖ Kernel.id : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext a s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
s : Set γ
a : α
hs : Ne (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    LT.lt (α := ℝ≥0∞)
      ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (toMeasurable ((η ∘ₖ κ : (a : α) → Measure γ) a) s) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞)
have refine : ∫⁻ (x : β),
    (((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞)
      (toMeasurable ((η ∘ₖ κ : (a : α) → Measure γ) a) s) ∂(κ : (a : α) → Measure β) a ≠
  ∞
Tactic: refine ae_lt_top (Kernel.measurable_coe η (measurableSet_toMeasurable ..)) ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
s : Set γ
a : α
hs : Ne (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : β),
      (((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (toMeasurable ((η ∘ₖ κ : (a : α) → Measure γ) a) s) ∂(κ : (a : α) → Measure β) a ≠
    ∞
have rwa : Ne (α := ℝ≥0∞)
  ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
      (toMeasurable ((η ∘ₖ κ : (a : α) → Measure γ) a) s) :
    ℝ≥0∞)
  (∞ : ℝ≥0∞)
Tactic: rwa [← Kernel.comp_apply' _ _ _ (measurableSet_toMeasurable ..), measure_toMeasurable]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
s : Set γ
a : α
hs : Ne (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    LT.lt (α := ℝ≥0∞) ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have h : ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
  LT.lt (α := ℝ≥0∞)
    ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (toMeasurable ((η ∘ₖ κ : (a : α) → Measure γ) a) s) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)
Tactic: have h : ∀ᵐ b ∂κ a, η b (toMeasurable ((η ∘ₖ κ) a) s) < ∞ := by
    refine ae_lt_top (Kernel.measurable_coe η (measurableSet_toMeasurable ..)) ?_
    rwa [← Kernel.comp_apply' _ _ _ (measurableSet_toMeasurable ..), measure_toMeasurable]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
s : Set γ
a : α
hs : Ne (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    LT.lt (α := ℝ≥0∞)
      ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (toMeasurable ((η ∘ₖ κ : (a : α) → Measure γ) a) s) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞)
⊢ ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    LT.lt (α := ℝ≥0∞) ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have h₁ : ∀ (a_1 : β),
  Membership.mem (γ := Set β)
    {x : β |
      Membership.mem (γ := Set β)
          {x : β |
            (fun (b : β) ↦
                LT.lt (α := ℝ≥0∞)
                  ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞)
                      (toMeasurable ((η ∘ₖ κ : (a : α) → Measure γ) a) s) :
                    ℝ≥0∞)
                  (∞ : ℝ≥0∞))
              x}
          x →
        Membership.mem (γ := Set β)
          {x : β |
            (fun (b : β) ↦
                LT.lt (α := ℝ≥0∞) ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
                  (∞ : ℝ≥0∞))
              x}
          x}
    a_1
Tactic: filter_upwards [h] with b hb using (measure_mono (subset_toMeasurable _ _)).trans_lt hb
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
s : Set γ
a : α
hs : Ne (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    LT.lt (α := ℝ≥0∞)
      ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (toMeasurable ((η ∘ₖ κ : (a : α) → Measure γ) a) s) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞)
h₁ :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β)
            {x : β |
              (fun (b : β) ↦
                  LT.lt (α := ℝ≥0∞)
                    ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞)
                        (toMeasurable ((η ∘ₖ κ : (a : α) → Measure γ) a) s) :
                      ℝ≥0∞)
                    (∞ : ℝ≥0∞))
                x}
            x →
          Membership.mem (γ := Set β)
            {x : β |
              (fun (b : β) ↦
                  LT.lt (α := ℝ≥0∞) ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
                    (∞ : ℝ≥0∞))
                x}
            x}
      a_1
⊢ ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    LT.lt (α := ℝ≥0∞) ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have h₂ : ∀ (a_1 : β),
  LT.lt (α := ℝ≥0∞)
      ((((η : (a : β) → Measure γ) a_1 : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (toMeasurable ((η ∘ₖ κ : (a : α) → Measure γ) a) s) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞) →
    LT.lt (α := ℝ≥0∞) ((((η : (a : β) → Measure γ) a_1 : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: filter_upwards [h] with b hb using (measure_mono (subset_toMeasurable _ _)).trans_lt hb
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
s : Set γ
a : α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
      (fun (y : β) ↦ (((η : (a : β) → Measure γ) y : Measure γ) : (a : Set γ) → ℝ≥0∞) s) 0
have rw : ∫⁻ (b : β), (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) a = 0 ↔
  (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (y : β) ↦ (((η : (a : β) → Measure γ) y : Measure γ) : (a : Set γ) → ℝ≥0∞) s) 0
Tactic: rw [comp_apply' _ _ _ hs, lintegral_eq_zero_iff (η.measurable_coe hs)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
s : Set γ
a : α
hs : MeasurableSet s
rw :
  ∫⁻ (b : β), (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) a = 0 ↔
    (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
      (fun (y : β) ↦ (((η : (a : β) → Measure γ) y : Measure γ) : (a : Set γ) → ℝ≥0∞) s) 0
⊢ Eq (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
      (fun (y : β) ↦ (((η : (a : β) → Measure γ) y : Measure γ) : (a : Set γ) → ℝ≥0∞) s) 0
have rw₁ : (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (a : β) ↦ (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s) 0 ↔
  (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (y : β) ↦ (((η : (a : β) → Measure γ) y : Measure γ) : (a : Set γ) → ℝ≥0∞) s) 0
Tactic: rw [comp_apply' _ _ _ hs, lintegral_eq_zero_iff (η.measurable_coe hs)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
a : α
s : Set γ
h : Eq (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (x : β) ↦ (((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s) 0
have obtain : ∀ (t : Set γ) (hst : s ⊆ t) (mt : MeasurableSet t)
  (ht : Eq (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)),
  (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (x : β) ↦ (((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s) 0
Tactic: obtain ⟨t, hst, mt, ht⟩ := exists_measurable_superset_of_null h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
a : α
s : Set γ
h : Eq (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set γ
hst : s ⊆ t
mt : MeasurableSet t
ht : Eq (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (x : β) ↦ (((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s) 0
have ht₁ : (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
  (fun (y : β) ↦ (((η : (a : β) → Measure γ) y : Measure γ) : (a : Set γ) → ℝ≥0∞) t) 0
Tactic: simp_rw [comp_null a mt] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
a : α
s : Set γ
h : Eq (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set γ
hst : s ⊆ t
mt : MeasurableSet t
ht :
  (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (y : β) ↦ (((η : (a : β) → Measure γ) y : Measure γ) : (a : Set γ) → ℝ≥0∞) t) 0
⊢ (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (x : β) ↦ (((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s) 0
have rw : (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyLE (β := ℝ≥0∞)
    (fun (x : β) ↦ (((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s) 0 ∧
  (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyLE (β := ℝ≥0∞) 0 fun (x : β) ↦
    (((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s
Tactic: rw [Filter.eventuallyLE_antisymm_iff]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
a : α
p : γ → Prop
hp : MeasurableSet.{u_3} (α := γ) {z : γ | p z}
h : ∀ᵐ (y : β) ∂((κ : (a : α) → Measure β) a : Measure β), ∀ᵐ (z : γ) ∂((η : (a : β) → Measure γ) y : Measure γ), p z
⊢ ∀ᵐ (z : γ) ∂((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ), p z
have hs : ∀
  (h :
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞)
          {a : β | ¬∀ᵐ (z : γ) ∂((η : (a : β) → Measure γ) a : Measure γ), p z} :
        ℝ≥0∞)
      (0 : ℝ≥0∞)),
  MeasurableSet.{u_3} (α := γ) {a : γ | ¬p a}
Tactic: rwa [ae_iff, comp_null] at *
Cleared hypotheses: h