awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t_1 : Set Ω
n : ι
ht : MeasurableSet t_1
t : Set Ω
hn : n ≤ i
u : Set (β n)
left : MeasurableSet u
hu' : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = t
h : ∀ (heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = Set.univ), MeasurableSet t
h₁ : ∀ (heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = s n), MeasurableSet t
h₂ : ∀ (heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = (s n)ᶜ), MeasurableSet t
⊢ MeasurableSet t
have h₃ : ∀ (heq : Membership.mem (γ := Set (Set Ω)) {∅} (((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u)), MeasurableSet t
Tactic: obtain heq | heq | heq | heq := Set.indicator_const_preimage (s n) u (1 : β n)
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t_1 : Set Ω
n : ι
ht : MeasurableSet t_1
t : Set Ω
hn : n ≤ i
u : Set (β n)
left : MeasurableSet u
hu' : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = t
heq : Membership.mem (γ := Set (Set Ω)) {∅} (((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u)
⊢ MeasurableSet t
have heq₁ : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = ∅
Tactic: rw [Set.mem_singleton_iff] at heq
Cleared hypotheses: heq
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t_1 : Set Ω
n : ι
ht : MeasurableSet t_1
t : Set Ω
hn : n ≤ i
u : Set (β n)
left : MeasurableSet u
hu' : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = t
heq : Membership.mem (γ := Set (Set Ω)) {∅} (((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u)
⊢ MeasurableSet t
have heq₁ : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = ∅
Tactic: on_goal 4 => rw [Set.mem_singleton_iff] at heq
Cleared hypotheses: heq
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t_1 : Set Ω
n : ι
ht : MeasurableSet t_1
t : Set Ω
hn : n ≤ i
u : Set (β n)
left : MeasurableSet u
hu' : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = t
heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = Set.univ
⊢ MeasurableSet t
have hu'₁ : Set.univ = t
Tactic: rw [heq] at hu'
Cleared hypotheses: hu', heq
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t_1 : Set Ω
n : ι
ht : MeasurableSet t_1
t : Set Ω
hn : n ≤ i
u : Set (β n)
left : MeasurableSet u
hu' : Set.univ = t
heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = Set.univ
⊢ MeasurableSet t
have h : MeasurableSet.{u_1} (α := Ω) Set.univ
Tactic: rw [← hu']
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t_1 : Set Ω
n : ι
ht : MeasurableSet t_1
t : Set Ω
hn : n ≤ i
u : Set (β n)
left : MeasurableSet u
hu' : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = t
heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = s n
⊢ MeasurableSet t
have hu'₁ : s n = t
Tactic: rw [heq] at hu'
Cleared hypotheses: hu', heq
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t_1 : Set Ω
n : ι
ht : MeasurableSet t_1
t : Set Ω
hn : n ≤ i
u : Set (β n)
left : MeasurableSet u
hu' : s n = t
heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = s n
⊢ MeasurableSet t
have h : MeasurableSet (s n)
Tactic: rw [← hu']
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t_1 : Set Ω
n : ι
ht : MeasurableSet t_1
t : Set Ω
hn : n ≤ i
u : Set (β n)
left : MeasurableSet u
hu' : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = t
heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = (s n)ᶜ
⊢ MeasurableSet t
have hu'₁ : (s n)ᶜ = t
Tactic: rw [heq] at hu'
Cleared hypotheses: hu', heq
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t_1 : Set Ω
n : ι
ht : MeasurableSet t_1
t : Set Ω
hn : n ≤ i
u : Set (β n)
left : MeasurableSet u
hu' : (s n)ᶜ = t
heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = (s n)ᶜ
⊢ MeasurableSet t
have h : MeasurableSet (s n)ᶜ
Tactic: rw [← hu']
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t_1 : Set Ω
n : ι
ht : MeasurableSet t_1
t : Set Ω
hn : n ≤ i
u : Set (β n)
left : MeasurableSet u
hu' : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = t
heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = ∅
⊢ MeasurableSet t
have hu'₁ : ∅ = t
Tactic: rw [heq] at hu'
Cleared hypotheses: hu', heq
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t_1 : Set Ω
n : ι
ht : MeasurableSet t_1
t : Set Ω
hn : n ≤ i
u : Set (β n)
left : MeasurableSet u
hu' : ∅ = t
heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = ∅
⊢ MeasurableSet t
have h : MeasurableSet.{u_1} (α := Ω) ∅
Tactic: rw [← hu']
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
E : Type u_4
inst_1 : Zero E
inst_2 : TopologicalSpace E
ℱ : Filtration ι m
f : ι → Ω → E
μ : Measure Ω
⊢ StronglyMeasurable.{u_1, u_4} (α := Ω) (β := E)
    (if h : ∃ (g : Ω → E), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ι) ↦ f n ω) atTop (𝓝 (g ω)) then
      Classical.choose (p := fun (x : Ω → E) ↦
        StronglyMeasurable x ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ι) ↦ f n ω) atTop (𝓝 (x ω))) h
    else 0)
have pos : ∀ (h : ∃ (g : Ω → E), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ι) ↦ f n ω) atTop (𝓝 (g ω))),
  StronglyMeasurable
    (Classical.choose (p := fun (x : Ω → E) ↦
      StronglyMeasurable x ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ι) ↦ f n ω) atTop (𝓝 (x ω))) h)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
E : Type u_4
inst_1 : Zero E
inst_2 : TopologicalSpace E
ℱ : Filtration ι m
f : ι → Ω → E
μ : Measure Ω
pos :
  ∀ (h : ∃ (g : Ω → E), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ι) ↦ f n ω) atTop (𝓝 (g ω))),
    StronglyMeasurable
      (Classical.choose (p := fun (x : Ω → E) ↦
        StronglyMeasurable x ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ι) ↦ f n ω) atTop (𝓝 (x ω))) h)
⊢ StronglyMeasurable.{u_1, u_4} (α := Ω) (β := E)
    (if h : ∃ (g : Ω → E), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ι) ↦ f n ω) atTop (𝓝 (g ω)) then
      Classical.choose (p := fun (x : Ω → E) ↦
        StronglyMeasurable x ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ι) ↦ f n ω) atTop (𝓝 (x ω))) h
    else 0)
have neg : ∀ (h : ¬∃ (g : Ω → E), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ι) ↦ f n ω) atTop (𝓝 (g ω))),
  StronglyMeasurable.{u_1, u_4} (α := Ω) (β := E) 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
R : ℝ≥0
p : ℝ≥0∞
F : Type u_5
inst : NormedAddCommGroup F
ℱ : Filtration ℕ m
f : ℕ → Ω → F
hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
⊢ MemLp.{u_1, u_5} (ε := F)
    (if h : ∃ (g : Ω → F), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω)) then
      Classical.choose (p := fun (x : Ω → F) ↦
        StronglyMeasurable x ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (x ω))) h
    else 0)
    p μ
have pos : ∀ (h : ∃ (g : Ω → F), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))),
  MemLp
    (Classical.choose (p := fun (x : Ω → F) ↦
      StronglyMeasurable x ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (x ω))) h)
    p μ
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
R : ℝ≥0
p : ℝ≥0∞
F : Type u_5
inst : NormedAddCommGroup F
ℱ : Filtration ℕ m
f : ℕ → Ω → F
hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
pos :
  ∀ (h : ∃ (g : Ω → F), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))),
    MemLp
      (Classical.choose (p := fun (x : Ω → F) ↦
        StronglyMeasurable x ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (x ω))) h)
      p μ
⊢ MemLp.{u_1, u_5} (ε := F)
    (if h : ∃ (g : Ω → F), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω)) then
      Classical.choose (p := fun (x : Ω → F) ↦
        StronglyMeasurable x ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (x ω))) h
    else 0)
    p μ
have neg : ∀ (h : ¬∃ (g : Ω → F), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))),
  MemLp.{u_1, u_5} (ε := F) 0 p μ
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
R : ℝ≥0
p : ℝ≥0∞
F : Type u_5
inst : NormedAddCommGroup F
ℱ : Filtration ℕ m
f : ℕ → Ω → F
hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
h : ∃ (g : Ω → F), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
⊢ MemLp
    (Classical.choose (p := fun (x : Ω → F) ↦
      StronglyMeasurable x ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (x ω))) h)
    p μ
have pos : liminf (fun (n : ℕ) ↦ eLpNorm (f n) p μ) atTop ≤ (↑R : ℝ≥0∞)
Tactic: refine ⟨StronglyMeasurable.aestronglyMeasurable
      ((Classical.choose_spec h).1.mono (sSup_le fun m ⟨n, hn⟩ => hn ▸ ℱ.le _)),
      lt_of_le_of_lt (Lp.eLpNorm_lim_le_liminf_eLpNorm hfm _ (Classical.choose_spec h).2)
        (lt_of_le_of_lt ?_ (ENNReal.coe_lt_top : ↑R < ∞))⟩
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
R : ℝ≥0
p : ℝ≥0∞
F : Type u_5
inst : NormedAddCommGroup F
ℱ : Filtration ℕ m
f : ℕ → Ω → F
hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
h : ∃ (g : Ω → F), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
⊢ liminf (fun (n : ℕ) ↦ eLpNorm (f n) p μ) atTop ≤ (↑R : ℝ≥0∞)
have pos : sSup {a : ℝ≥0∞ | ∃ (a_1 : ℕ), ∀ b ≥ a_1, a ≤ eLpNorm (f b) p μ} ≤ (↑R : ℝ≥0∞)
Tactic: simp_rw [liminf_eq, eventually_atTop]
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
X : ι → Type u_4
inst_4 : (i : ι) → MeasurableSpace (X i)
i j : ι
hij : i ≤ j
⊢ LE.le (α := MeasurableSpace ((i : ι) → X i))
    (MeasurableSpace.comap (β := (a : (↑(Set.Iic i) : Type u_2)) → X (↑a : ι)) (restrictLe (π := X) i)
      (MeasurableSpace.pi (X := fun (a : (↑(Set.Iic i) : Type u_2)) ↦ X (↑a : ι))))
    (MeasurableSpace.comap (β := (a : (↑(Set.Iic j) : Type u_2)) → X (↑a : ι)) (restrictLe (π := X) j)
      (MeasurableSpace.pi (X := fun (a : (↑(Set.Iic j) : Type u_2)) ↦ X (↑a : ι))))
have rw : LE.le (α := MeasurableSpace ((i : ι) → X i))
  (MeasurableSpace.comap (restrictLe (π := X) j)
    (MeasurableSpace.comap (restrictLe₂ (π := X) hij)
      (MeasurableSpace.pi (X := fun (a : (↑(Set.Iic i) : Type u_2)) ↦ X (↑a : ι)))))
  (MeasurableSpace.comap (β := (a : (↑(Set.Iic j) : Type u_2)) → X (↑a : ι)) (restrictLe (π := X) j)
    (MeasurableSpace.pi (X := fun (a : (↑(Set.Iic j) : Type u_2)) ↦ X (↑a : ι))))
Tactic: rw [← restrictLe₂_comp_restrictLe hij, ← comap_comp]
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
ι : Type u_2
inst : Preorder ι
X : ι → Type u_4
inst_1 : (i : ι) → MeasurableSpace (X i)
inst_2 : LocallyFiniteOrderBot ι
i : ι
⊢ Eq (α := MeasurableSpace ((i : ι) → X i)) ((↑(piLE (X := X)) : ι → MeasurableSpace ((i : ι) → X i)) i)
    (MeasurableSpace.comap (β := (i_1 : ↥(Finset.Iic i)) → X (↑i_1 : ι)) (frestrictLe (π := X) i)
      (MeasurableSpace.pi (X := fun (a : ↥(Finset.Iic i)) ↦ X (↑a : ι))))
have a : LE.le (α := MeasurableSpace ((i : ι) → X i)) ((↑(piLE (X := X)) : ι → MeasurableSpace ((i : ι) → X i)) i)
  (MeasurableSpace.comap (β := (i_1 : ↥(Finset.Iic i)) → X (↑i_1 : ι)) (frestrictLe (π := X) i)
    (MeasurableSpace.pi (X := fun (a : ↥(Finset.Iic i)) ↦ X (↑a : ι))))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
ι : Type u_2
inst : Preorder ι
X : ι → Type u_4
inst_1 : (i : ι) → MeasurableSpace (X i)
inst_2 : LocallyFiniteOrderBot ι
i : ι
a :
  LE.le (α := MeasurableSpace ((i : ι) → X i)) ((↑(piLE (X := X)) : ι → MeasurableSpace ((i : ι) → X i)) i)
    (MeasurableSpace.comap (β := (i_1 : ↥(Finset.Iic i)) → X (↑i_1 : ι)) (frestrictLe (π := X) i)
      (MeasurableSpace.pi (X := fun (a : ↥(Finset.Iic i)) ↦ X (↑a : ι))))
⊢ Eq (α := MeasurableSpace ((i : ι) → X i)) ((↑(piLE (X := X)) : ι → MeasurableSpace ((i : ι) → X i)) i)
    (MeasurableSpace.comap (β := (i_1 : ↥(Finset.Iic i)) → X (↑i_1 : ι)) (frestrictLe (π := X) i)
      (MeasurableSpace.pi (X := fun (a : ↥(Finset.Iic i)) ↦ X (↑a : ι))))
have a₁ : LE.le (α := MeasurableSpace ((i : ι) → X i))
  (MeasurableSpace.comap (β := (i_1 : ↥(Finset.Iic i)) → X (↑i_1 : ι)) (frestrictLe (π := X) i)
    (MeasurableSpace.pi (X := fun (a : ↥(Finset.Iic i)) ↦ X (↑a : ι))))
  ((↑(piLE (X := X)) : ι → MeasurableSpace ((i : ι) → X i)) i)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
ι : Type u_2
inst : Preorder ι
X : ι → Type u_4
inst_1 : (i : ι) → MeasurableSpace (X i)
inst_2 : LocallyFiniteOrderBot ι
i : ι
⊢ LE.le (α := MeasurableSpace ((i : ι) → X i)) ((↑(piLE (X := X)) : ι → MeasurableSpace ((i : ι) → X i)) i)
    (MeasurableSpace.comap (β := (i_1 : ↥(Finset.Iic i)) → X (↑i_1 : ι)) (frestrictLe (π := X) i)
      (MeasurableSpace.pi (X := fun (a : ↥(Finset.Iic i)) ↦ X (↑a : ι))))
have a : LE.le (α := MeasurableSpace ((i : ι) → X i))
  (MeasurableSpace.comap (β :=
    (a : ↥(Finset.Iic i)) → X (↑((Equiv.IicFinsetSet i : (a : ↥(Finset.Iic i)) → (↑(Set.Iic i) : Type u_2)) a) : ι))
    (frestrictLe (π := X) i)
    (MeasurableSpace.comap (β := (a : (↑(Set.Iic i) : Type u_2)) → X (↑a : ι))
      (⇑(MeasurableEquiv.piCongrLeft.{u_2, u_2, u_4} (δ := ↥(Finset.Iic i))
              (fun (i_1 : (↑(Set.Iic i) : Type u_2)) ↦ X (↑i_1 : ι)) (Equiv.IicFinsetSet i) :
            ((b : ↥(Finset.Iic i)) →
                X (↑((Equiv.IicFinsetSet i : (a : ↥(Finset.Iic i)) → (↑(Set.Iic i) : Type u_2)) b) : ι)) ≃ᵐ
              ((a : (↑(Set.Iic i) : Type u_2)) → X (↑a : ι))) :
        (a :
            (b : ↥(Finset.Iic i)) →
              X (↑((Equiv.IicFinsetSet i : (a : ↥(Finset.Iic i)) → (↑(Set.Iic i) : Type u_2)) b) : ι)) →
          (a : (↑(Set.Iic i) : Type u_2)) → X (↑a : ι))
      (MeasurableSpace.pi (X := fun (a : (↑(Set.Iic i) : Type u_2)) ↦ X (↑a : ι)))))
  (MeasurableSpace.comap (β := (i_1 : ↥(Finset.Iic i)) → X (↑i_1 : ι)) (frestrictLe (π := X) i)
    (MeasurableSpace.pi (X := fun (a : ↥(Finset.Iic i)) ↦ X (↑a : ι))))
Tactic: simp_rw [piLE, ← piCongrLeft_comp_frestrictLe, ← MeasurableEquiv.coe_piCongrLeft, ← comap_comp]
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
ι : Type u_2
inst : Preorder ι
X : ι → Type u_4
inst_1 : (i : ι) → MeasurableSpace (X i)
inst_2 : LocallyFiniteOrderBot ι
i : ι
⊢ LE.le (α := MeasurableSpace ((i : ι) → X i))
    (MeasurableSpace.comap (β := (i_1 : ↥(Finset.Iic i)) → X (↑i_1 : ι)) (frestrictLe (π := X) i)
      (MeasurableSpace.pi (X := fun (a : ↥(Finset.Iic i)) ↦ X (↑a : ι))))
    ((↑(piLE (X := X)) : ι → MeasurableSpace ((i : ι) → X i)) i)
have a : LE.le (α := MeasurableSpace ((i : ι) → X i))
  (MeasurableSpace.comap (β :=
    (a : (↑(Set.Iic i) : Type u_2)) →
      X (↑((Equiv.symm (Equiv.IicFinsetSet i) : (a : (↑(Set.Iic i) : Type u_2)) → ↥(Finset.Iic i)) a) : ι))
    (restrictLe (π := X) i)
    (MeasurableSpace.comap (β := (i_1 : ↥(Finset.Iic i)) → X (↑i_1 : ι))
      (⇑(MeasurableEquiv.piCongrLeft.{u_2, u_2, u_4} (fun (i_1 : ↥(Finset.Iic i)) ↦ X (↑i_1 : ι))
              (Equiv.symm (Equiv.IicFinsetSet i)) :
            ((b : (↑(Set.Iic i) : Type u_2)) →
                X (↑((Equiv.symm (Equiv.IicFinsetSet i) : (a : (↑(Set.Iic i) : Type u_2)) → ↥(Finset.Iic i)) b) : ι)) ≃ᵐ
              ((a : ↥(Finset.Iic i)) → X (↑a : ι))) :
        (a :
            (b : (↑(Set.Iic i) : Type u_2)) →
              X (↑(((Equiv.IicFinsetSet i).symm : (a : (↑(Set.Iic i) : Type u_2)) → ↥(Finset.Iic i)) b) : ι)) →
          (a : ↥(Finset.Iic i)) → X (↑a : ι))
      (MeasurableSpace.pi (X := fun (a : ↥(Finset.Iic i)) ↦ X (↑a : ι)))))
  ((↑(piLE (X := X)) : ι → MeasurableSpace ((i : ι) → X i)) i)
Tactic: rw [← piCongrLeft_comp_restrictLe, ← MeasurableEquiv.coe_piCongrLeft, ← comap_comp]
-- Lean 4 proof step from Mathlib.Probability.Process.Filtration (goal)
Goal:
Ω : Type u_1
ι_1 : Type u_2
m : MeasurableSpace Ω
β : ι_1 → Type u_3
inst : (i : ι_1) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι_1), MetrizableSpace.{u_3} (β i)
mβ : (i : ι_1) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι_1), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι_1
ι : Type u_4
X : ι → Type u_5
inst_4 : (i : ι) → MeasurableSpace (X i)
s t : Finset ι
hst : s ≤ t
⊢ LE.le (α := MeasurableSpace ((i : ι) → X i))
    (MeasurableSpace.comap (s.restrict (π := X)) (MeasurableSpace.pi (X := fun (a : ↥s) ↦ X (↑a : ι))))
    (MeasurableSpace.comap (t.restrict (π := X)) (MeasurableSpace.pi (X := fun (a : ↥t) ↦ X (↑a : ι))))
have rw : LE.le (α := MeasurableSpace ((i : ι) → X i))
  (MeasurableSpace.comap (t.restrict (π := X))
    (MeasurableSpace.comap (restrict₂ (π := X) hst) (MeasurableSpace.pi (X := fun (a : ↥s) ↦ X (↑a : ι)))))
  (MeasurableSpace.comap (t.restrict (π := X)) (MeasurableSpace.pi (X := fun (a : ↥t) ↦ X (↑a : ι))))
Tactic: rw [← restrict₂_comp_restrict hst, ← comap_comp]
-- Lean 4 proof step from Mathlib.Probability.Process.FiniteDimensionalLaws (goal)
Goal:
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X : (t : T) → Ω → 𝓧 t
P : Measure Ω
hX : ∀ (t : T), AEMeasurable (X t) P
I J : Finset T
hJI : J ⊆ I
⊢ Eq (α := Measure ((j : ↥J) → 𝓧 (↑j : T)))
    ((fun (I : Finset T) ↦
        (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P : Measure ((j : ↥I) → 𝓧 (↑j : T))))
      J)
    (Measure.map (Finset.restrict₂ (π := 𝓧) hJI)
      ((fun (I : Finset T) ↦
          (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P : Measure ((j : ↥I) → 𝓧 (↑j : T))))
        I))
have rw : Eq (α := Measure ((j : ↥J) → 𝓧 (↑j : T)))
  ((fun (I : Finset T) ↦
      (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P : Measure ((j : ↥I) → 𝓧 (↑j : T))))
    J)
  (Measure.map (Finset.restrict₂ (π := 𝓧) hJI ∘ fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P)
Tactic: rw [AEMeasurable.map_map_of_aemeasurable (Finset.measurable_restrict₂ _).aemeasurable]
-- Lean 4 proof step from Mathlib.Probability.Process.FiniteDimensionalLaws (goal)
Goal:
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X : (t : T) → Ω → 𝓧 t
P : Measure Ω
hX : ∀ (t : T), AEMeasurable (X t) P
I J : Finset T
hJI : J ⊆ I
rw :
  Eq (α := Measure ((j : ↥J) → 𝓧 (↑j : T)))
    ((fun (I : Finset T) ↦
        (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P : Measure ((j : ↥I) → 𝓧 (↑j : T))))
      J)
    (Measure.map (Finset.restrict₂ (π := 𝓧) hJI ∘ fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P)
⊢ Eq (α := Measure ((j : ↥J) → 𝓧 (↑j : T)))
    ((fun (I : Finset T) ↦
        (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P : Measure ((j : ↥I) → 𝓧 (↑j : T))))
      J)
    (Measure.map (Finset.restrict₂ (π := 𝓧) hJI)
      ((fun (I : Finset T) ↦
          (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P : Measure ((j : ↥I) → 𝓧 (↑j : T))))
        I))
have rw₁ : AEMeasurable (β := (i : ↥I) → 𝓧 (↑i : T)) (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P
Tactic: rw [AEMeasurable.map_map_of_aemeasurable (Finset.measurable_restrict₂ _).aemeasurable]