awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst : IsFiniteMeasure P
hX : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ X x ω) P
hY : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ Y x ω) P
refine_1 :
  ∀ (h : IdentDistrib (γ := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ X x ω) (fun (ω : Ω) (x : T) ↦ Y x ω) P P)
    (I : Finset T), AEMeasurable (β := (i : ↥I) → 𝓧 (↑i : T)) (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P
refine_2 :
  ∀ (h : IdentDistrib (γ := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ X x ω) (fun (ω : Ω) (x : T) ↦ Y x ω) P P)
    (I : Finset T), AEMeasurable (β := (i : ↥I) → 𝓧 (↑i : T)) (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω) P
refine_3 :
  ∀ (h : IdentDistrib (γ := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ X x ω) (fun (ω : Ω) (x : T) ↦ Y x ω) P P)
    (I : Finset T),
    Eq (α := Measure ((i : ↥I) → 𝓧 (↑i : T))) (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P)
      (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω) P)
⊢ IdentDistrib (γ := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ X x ω) (fun (ω : Ω) (x : T) ↦ Y x ω) P P ↔
    ∀ (I : Finset T),
      IdentDistrib (γ := (i : ↥I) → 𝓧 (↑i : T)) (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω)
        (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω) P P
have refine_4 : ∀
  (h :
    ∀ (I : Finset T),
      IdentDistrib (γ := (i : ↥I) → 𝓧 (↑i : T)) (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω)
        (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω) P P),
  Eq (α := Measure ((x : T) → 𝓧 x)) (Measure.map (fun (ω : Ω) (x : T) ↦ X x ω) P)
    (Measure.map (fun (ω : Ω) (x : T) ↦ Y x ω) P)
Tactic: refine ⟨fun h I ↦ ⟨?_, ?_, ?_⟩, fun h ↦ ⟨hX, hY, ?_⟩⟩
-- 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 Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
h : ∀ (t : T), X t =ᶠ[ae P] Y t
I : Finset T
⊢ ∀ᵐ (ω : Ω) ∂P, ∀ (i : ↥I), Eq (α := 𝓧 (↑i : T)) (X (↑i : T) ω) (Y (↑i : T) ω)
have rw : ∀ (i : ↥I), ∀ᵐ (a : Ω) ∂P, Eq (α := 𝓧 (↑i : T)) (X (↑i : T) a) (Y (↑i : T) a)
Tactic: rw [MeasureTheory.ae_all_iff]
-- Lean 4 proof step from Mathlib.Probability.Process.FiniteDimensionalLaws (hypothesis)
Goal:
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
h : ∀ (t : T), X t =ᶠ[ae P] Y t
I : Finset T
⊢ Eq (α := Measure ((i : ↥I) → 𝓧 (↑i : T))) (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P)
    (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω) P)
have h' : ∀ᵐ (ω : Ω) ∂P, ∀ (i : ↥I), Eq (α := 𝓧 (↑i : T)) (X (↑i : T) ω) (Y (↑i : T) ω)
Tactic: have h' : ∀ᵐ ω ∂P, ∀ (i : I), X i ω = Y i ω := by
    rw [MeasureTheory.ae_all_iff]
    exact fun i ↦ h i
-- 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 Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
h : ∀ (t : T), X t =ᶠ[ae P] Y t
I : Finset T
h' : ∀ᵐ (ω : Ω) ∂P, ∀ (i : ↥I), Eq (α := 𝓧 (↑i : T)) (X (↑i : T) ω) (Y (↑i : T) ω)
⊢ Eq (α := Measure ((i : ↥I) → 𝓧 (↑i : T))) (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P)
    (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω) P)
have refine : (ae P).EventuallyEq (β := (i : ↥I) → 𝓧 (↑i : T)) (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) fun (ω : Ω) ↦
  I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω
Tactic: refine Measure.map_congr ?_
-- 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 Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
h : ∀ (t : T), X t =ᶠ[ae P] Y t
I : Finset T
h' : ∀ᵐ (ω : Ω) ∂P, ∀ (i : ↥I), Eq (α := 𝓧 (↑i : T)) (X (↑i : T) ω) (Y (↑i : T) ω)
⊢ (ae P).EventuallyEq (β := (i : ↥I) → 𝓧 (↑i : T)) (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) fun (ω : Ω) ↦
    I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω
have h₁ : ∀ (a : Ω),
  Membership.mem (γ := Set Ω)
    {x : Ω |
      Membership.mem (γ := Set Ω)
          {x : Ω | (fun (ω : Ω) ↦ ∀ (i : ↥I), Eq (α := 𝓧 (↑i : T)) (X (↑i : T) ω) (Y (↑i : T) ω)) x} x →
        Membership.mem (γ := Set Ω)
          {x : Ω |
            (fun (x : Ω) ↦
                Eq (α := (i : ↥I) → 𝓧 (↑i : T))
                  ((fun (ω : Ω) ↦ (I.restrict (π := 𝓧) fun (x : T) ↦ X x ω : (i : ↥I) → 𝓧 (↑i : T))) x)
                  ((fun (ω : Ω) ↦ (I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω : (i : ↥I) → 𝓧 (↑i : T))) x))
              x}
          x}
    a
Tactic: filter_upwards [h'] with ω h using funext h
-- 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 Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
h : ∀ (t : T), X t =ᶠ[ae P] Y t
I : Finset T
h' : ∀ᵐ (ω : Ω) ∂P, ∀ (i : ↥I), Eq (α := 𝓧 (↑i : T)) (X (↑i : T) ω) (Y (↑i : T) ω)
h₁ :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω)
            {x : Ω | (fun (ω : Ω) ↦ ∀ (i : ↥I), Eq (α := 𝓧 (↑i : T)) (X (↑i : T) ω) (Y (↑i : T) ω)) x} x →
          Membership.mem (γ := Set Ω)
            {x : Ω |
              (fun (x : Ω) ↦
                  Eq (α := (i : ↥I) → 𝓧 (↑i : T))
                    ((fun (ω : Ω) ↦ (I.restrict (π := 𝓧) fun (x : T) ↦ X x ω : (i : ↥I) → 𝓧 (↑i : T))) x)
                    ((fun (ω : Ω) ↦ (I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω : (i : ↥I) → 𝓧 (↑i : T))) x))
                x}
            x}
      a
⊢ (ae P).EventuallyEq (β := (i : ↥I) → 𝓧 (↑i : T)) (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) fun (ω : Ω) ↦
    I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω
have h₂ : ∀ (a : Ω),
  (∀ (i : ↥I), Eq (α := 𝓧 (↑i : T)) (X (↑i : T) a) (Y (↑i : T) a)) →
    Eq (α := (i : ↥I) → 𝓧 (↑i : T)) (I.restrict (π := 𝓧) fun (x : T) ↦ X x a) (I.restrict (π := 𝓧) fun (x : T) ↦ Y x a)
Tactic: filter_upwards [h'] with ω h using funext h
-- 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 Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst : IsFiniteMeasure P
hX : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ X x ω) P
hY : AEMeasurable (β := (x : T) → 𝓧 x) (fun (ω : Ω) (x : T) ↦ Y x ω) P
h : ∀ (t : T), X t =ᶠ[ae P] Y t
⊢ Eq (α := Measure ((x : T) → 𝓧 x)) (Measure.map (fun (ω : Ω) (x : T) ↦ X x ω) P)
    (Measure.map (fun (ω : Ω) (x : T) ↦ Y x ω) P)
have rw : ∀ (I : Finset T),
  Eq (α := Measure ((i : ↥I) → 𝓧 (↑i : T))) (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) P)
    (Measure.map (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω) P)
Tactic: rw [map_eq_iff_forall_finset_map_restrict_eq hX hY]
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Preorder ι
inst_1 : InfSet ι
u : ι → Ω → β
n m : ι
⊢ hittingBtwn u ∅ n m = fun (x : Ω) ↦ m
have h : ∀ (x : Ω), hittingBtwn u ∅ n m x = m
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Preorder ι
inst_1 : InfSet ι
u : ι → Ω → β
n : ι
⊢ hittingAfter u ∅ n = fun (x : Ω) ↦ ⊤
have h : ∀ (x : Ω), hittingAfter u ∅ n x = ⊤
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
⊢ hittingBtwn u Set.univ n m = fun (x : Ω) ↦ min n m
have h : ∀ (ω : Ω), hittingBtwn u Set.univ n m ω = min n m
Tactic: ext ω
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
ω : Ω
⊢ hittingBtwn u Set.univ n m ω = min n m
have h : (if ∃ (j : ι), n ≤ j ∧ j ≤ m then sInf (Set.Icc n m) else m) = min n m
Tactic: simp only [hittingBtwn_def, Set.mem_Icc, Set.mem_univ, and_true, Set.setOf_true, Set.inter_univ]
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
ω : Ω
⊢ (if ∃ (j : ι), n ≤ j ∧ j ≤ m then sInf (Set.Icc n m) else m) = min n m
have pos : ∀ (hnm : n ≤ m), (if ∃ (j : ι), n ≤ j ∧ j ≤ m then sInf (Set.Icc n m) else m) = min n m
Tactic: by_cases hnm : n ≤ m
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
ω : Ω
pos : ∀ (hnm : n ≤ m), (if ∃ (j : ι), n ≤ j ∧ j ≤ m then sInf (Set.Icc n m) else m) = min n m
⊢ (if ∃ (j : ι), n ≤ j ∧ j ≤ m then sInf (Set.Icc n m) else m) = min n m
have neg : ∀ (hnm : ¬n ≤ m), (if ∃ (j : ι), n ≤ j ∧ j ≤ m then sInf (Set.Icc n m) else m) = min n m
Tactic: by_cases hnm : n ≤ m
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
ω : Ω
hnm : n ≤ m
⊢ (if ∃ (j : ι), n ≤ j ∧ j ≤ m then sInf (Set.Icc n m) else m) = min n m
have pos : (∀ (x : ι), n ≤ x → m < x) → m = n
Tactic: simp [hnm]
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
ω : Ω
hnm : ¬n ≤ m
⊢ (if ∃ (j : ι), n ≤ j ∧ j ≤ m then sInf (Set.Icc n m) else m) = min n m
have neg : (if ∃ (j : ι), n ≤ j ∧ j ≤ m then sInf ∅ else m) = min n m
Tactic: simp [hnm]
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
ω : Ω
⊢ hittingBtwn u Set.univ n m ω = min n m
have h : (if ∃ (j : ι), n ≤ j ∧ j ≤ m then sInf (Set.Icc n m) else m) = min n m
Tactic: classical
  simp only [hittingBtwn_def, Set.mem_Icc, Set.mem_univ, and_true, Set.setOf_true, Set.inter_univ]
  by_cases hnm : n ≤ m <;> simp [hnm] <;> grind
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLattice ι
u : ι → Ω → β
n : ι
⊢ hittingAfter u Set.univ n = fun (x : Ω) ↦ (↑n : WithTop ι)
have h : ∀ (ω : Ω), hittingAfter u Set.univ n ω = (↑n : WithTop ι)
Tactic: ext ω
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLattice ι
u : ι → Ω → β
n : ι
ω : Ω
⊢ hittingAfter u Set.univ n ω = (↑n : WithTop ι)
have h : (if ∃ (j : ι), n ≤ j then (↑(sInf {j : ι | n ≤ j}) : WithTop ι) else ⊤) = (↑n : WithTop ι)
Tactic: simp only [hittingAfter_def, Set.mem_univ, and_true]
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLattice ι
u : ι → Ω → β
n : ι
ω : Ω
⊢ (if ∃ (j : ι), n ≤ j then (↑(sInf {j : ι | n ≤ j}) : WithTop ι) else ⊤) = (↑n : WithTop ι)
have h : (↑(sInf {j : ι | n ≤ j}) : WithTop ι) = (↑n : WithTop ι)
Tactic: rw [if_pos ⟨n, le_rfl⟩]
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLattice ι
u : ι → Ω → β
n : ι
ω : Ω
⊢ hittingAfter u Set.univ n ω = (↑n : WithTop ι)
have h : (if ∃ (j : ι), n ≤ j then (↑(sInf {j : ι | n ≤ j}) : WithTop ι) else ⊤) = (↑n : WithTop ι)
Tactic: classical
  simp only [hittingAfter_def, Set.mem_univ, and_true]
  rw [if_pos ⟨n, le_rfl⟩]
  exact_mod_cast csInf_Ici
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLattice ι
u : ι → Ω → β
n : ι
ω : Ω
h : (if ∃ (j : ι), n ≤ j then (↑(sInf {j : ι | n ≤ j}) : WithTop ι) else ⊤) = (↑n : WithTop ι)
⊢ hittingAfter u Set.univ n ω = (↑n : WithTop ι)
have h₁ : (↑(sInf {j : ι | n ≤ j}) : WithTop ι) = (↑n : WithTop ι)
Tactic: classical
  simp only [hittingAfter_def, Set.mem_univ, and_true]
  rw [if_pos ⟨n, le_rfl⟩]
  exact_mod_cast csInf_Ici
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
⊢ hittingBtwn u s n m ω ≤ m
have simp : (if ∃ j ∈ Set.Icc n m, u j ω ∈ s then sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) else m) ≤ m
Tactic: simp only [hittingBtwn]
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
⊢ (if ∃ j ∈ Set.Icc n m, u j ω ∈ s then sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) else m) ≤ m
have pos : ∀ (h : ∃ j ∈ Set.Icc n m, u j ω ∈ s), sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ≤ m
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
pos : ∀ (h : ∃ j ∈ Set.Icc n m, u j ω ∈ s), sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ≤ m
⊢ (if ∃ j ∈ Set.Icc n m, u j ω ∈ s then sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) else m) ≤ m
have neg : ∀ (h : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s), m ≤ m
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ≤ m
have pos : ∀ (j : ι) (hj₁ : j ∈ Set.Icc n m) (hj₂ : u j ω ∈ s), sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ≤ m
Tactic: obtain ⟨j, hj₁, hj₂⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (hypothesis)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
j : ι
hj₁ : j ∈ Set.Icc n m
hj₂ : u j ω ∈ s
⊢ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ≤ m
have hj₃ : Membership.mem (γ := Set ι) {i : ι | u i ω ∈ s} j
Tactic: change j ∈ {i | u i ω ∈ s} at hj₂
Cleared hypotheses: hj₂
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (hypothesis)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m k : ι
hk₁ : k < hittingBtwn u s n m ω
hk₂ : n ≤ k
h : u k ω ∈ s
⊢ False
have hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
Tactic: have hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s := ⟨k, ⟨hk₂, le_trans hk₁.le <| hittingBtwn_le _⟩, h⟩
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m k : ι
hk₁ : k < hittingBtwn u s n m ω
hk₂ : n ≤ k
h : u k ω ∈ s
hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ False
have refine : hittingBtwn u s n m ω ≤ k
Tactic: refine not_le.2 hk₁ ?_
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m k : ι
hk₁ : k < hittingBtwn u s n m ω
hk₂ : n ≤ k
h : u k ω ∈ s
hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ hittingBtwn u s n m ω ≤ k
have simp_rw : sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ≤ k
Tactic: simp_rw [hittingBtwn, if_pos hexists]
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m k : ι
hk₁ : k < hittingBtwn u s n m ω
hk₂ : n ≤ k
intro : ∀ (h : u k ω ∈ s), False
⊢ u k ω ∉ s
have intro₁ : ∀ (h : u k ω ∈ s) (hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s), False
Tactic: classical
  intro h
  have hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s := ⟨k, ⟨hk₂, le_trans hk₁.le <| hittingBtwn_le _⟩, h⟩
  refine not_le.2 hk₁ ?_
  simp_rw [hittingBtwn, if_pos hexists]
  exact csInf_le bddBelow_Icc.inter_of_left ⟨⟨hk₂, le_trans hk₁.le <| hittingBtwn_le _⟩, h⟩
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m k : ι
hk₁ : k < hittingBtwn u s n m ω
hk₂ : n ≤ k
intro : ∀ (h : u k ω ∈ s), False
intro₁ : ∀ (h : u k ω ∈ s) (hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s), False
⊢ u k ω ∉ s
have intro₂ : ∀ (h : u k ω ∈ s) (hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s), hittingBtwn u s n m ω ≤ k
Tactic: classical
  intro h
  have hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s := ⟨k, ⟨hk₂, le_trans hk₁.le <| hittingBtwn_le _⟩, h⟩
  refine not_le.2 hk₁ ?_
  simp_rw [hittingBtwn, if_pos hexists]
  exact csInf_le bddBelow_Icc.inter_of_left ⟨⟨hk₂, le_trans hk₁.le <| hittingBtwn_le _⟩, h⟩
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m k : ι
hk₁ : k < hittingBtwn u s n m ω
hk₂ : n ≤ k
intro : ∀ (h : u k ω ∈ s), False
intro₁ : ∀ (h : u k ω ∈ s) (hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s), False
intro₂ : ∀ (h : u k ω ∈ s) (hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s), hittingBtwn u s n m ω ≤ k
⊢ u k ω ∉ s
have intro₃ : ∀ (h : u k ω ∈ s) (hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s), sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ≤ k
Tactic: classical
  intro h
  have hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s := ⟨k, ⟨hk₂, le_trans hk₁.le <| hittingBtwn_le _⟩, h⟩
  refine not_le.2 hk₁ ?_
  simp_rw [hittingBtwn, if_pos hexists]
  exact csInf_le bddBelow_Icc.inter_of_left ⟨⟨hk₂, le_trans hk₁.le <| hittingBtwn_le _⟩, h⟩
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
k : ι
hk₁ : (↑k : WithTop ι) < hittingAfter u s n ω
hk₂ : n ≤ k
⊢ u k ω ∉ s
have refine : ∀ (h : u k ω ∈ s), hittingAfter u s n ω ≤ (↑k : WithTop ι)
Tactic: refine fun h ↦ not_le.2 hk₁ ?_
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
k : ι
hk₁ : (↑k : WithTop ι) < hittingAfter u s n ω
hk₂ : n ≤ k
h : u k ω ∈ s
⊢ hittingAfter u s n ω ≤ (↑k : WithTop ι)
have rw : (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ s}) : WithTop ι) ≤ (↑k : WithTop ι)
Tactic: rw [hittingAfter, if_pos ⟨k, hk₂, h⟩]
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m : ι
⊢ hittingBtwn u s n m ω = m ↔ (∃ j ∈ Set.Icc n m, u j ω ∈ s) → sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) = m
have rw : (if ∃ j ∈ Set.Icc n m, u j ω ∈ s then sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) else m) = m ↔
  (∃ j ∈ Set.Icc n m, u j ω ∈ s) → sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) = m
Tactic: rw [hittingBtwn, ite_eq_right_iff]
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m : ι
rw :
  (if ∃ j ∈ Set.Icc n m, u j ω ∈ s then sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) else m) = m ↔
    (∃ j ∈ Set.Icc n m, u j ω ∈ s) → sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) = m
⊢ hittingBtwn u s n m ω = m ↔ (∃ j ∈ Set.Icc n m, u j ω ∈ s) → sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) = m
have rw₁ : (∃ j ∈ Set.Icc n m, u j ω ∈ s) → sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) = m ↔
  (∃ j ∈ Set.Icc n m, u j ω ∈ s) → sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) = m
Tactic: rw [hittingBtwn, ite_eq_right_iff]
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m : ι
⊢ hittingBtwn u s n m ω = m ↔ (∃ j ∈ Set.Icc n m, u j ω ∈ s) → sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) = m
have rw : (if ∃ j ∈ Set.Icc n m, u j ω ∈ s then sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) else m) = m ↔
  (∃ j ∈ Set.Icc n m, u j ω ∈ s) → sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) = m
Tactic: classical
  rw [hittingBtwn, ite_eq_right_iff]
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m : ι
rw :
  (if ∃ j ∈ Set.Icc n m, u j ω ∈ s then sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) else m) = m ↔
    (∃ j ∈ Set.Icc n m, u j ω ∈ s) → sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) = m
⊢ hittingBtwn u s n m ω = m ↔ (∃ j ∈ Set.Icc n m, u j ω ∈ s) → sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) = m
have rw₁ : (∃ j ∈ Set.Icc n m, u j ω ∈ s) → sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) = m ↔
  (∃ j ∈ Set.Icc n m, u j ω ∈ s) → sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) = m
Tactic: classical
  rw [hittingBtwn, ite_eq_right_iff]
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m : ι
hmn : m ≤ n
⊢ hittingBtwn u s n m ω = m
have inl : ∀ (hmn : m ≤ m), hittingBtwn u s m m ω = m
Tactic: obtain rfl | h := le_iff_eq_or_lt.1 hmn
Cleared hypotheses: n, hmn
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m : ι
hmn : m ≤ n
inl : ∀ (hmn : m ≤ m), hittingBtwn u s m m ω = m
⊢ hittingBtwn u s n m ω = m
have inr : ∀ (h : m < n), hittingBtwn u s n m ω = m
Tactic: obtain rfl | h := le_iff_eq_or_lt.1 hmn
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
ω : Ω
m : ι
hmn : m ≤ m
⊢ hittingBtwn u s m m ω = m
have inl : ∀ (x : ι) (h : x ∈ Set.Icc m m ∧ u x ω ∈ s), sInf (Set.Icc m m ∩ {i : ι | u i ω ∈ s}) = m
Tactic: rw [hittingBtwn, ite_eq_right_iff, forall_exists_index]
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
ω : Ω
m : ι
hmn : m ≤ m
x : ι
| ∀ (h : x ∈ Set.Icc m m ∧ u x ω ∈ s), sInf (Set.Icc m m ∩ {i : ι | u i ω ∈ s}) = m
have rw : m ≤ x → x ≤ m → u x ω ∈ s → sInf ({m} ∩ {i : ι | u i ω ∈ s}) = m
Tactic: rw [Set.mem_Icc, Set.Icc_self, and_imp, and_imp]
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
ω : Ω
m : ι
hmn : m ≤ m
⊢ ∀ (x : ι) (h : x ∈ Set.Icc m m ∧ u x ω ∈ s), sInf (Set.Icc m m ∩ {i : ι | u i ω ∈ s}) = m
have inl : ∀ (x : ι), m ≤ x → x ≤ m → u x ω ∈ s → sInf ({m} ∩ {i : ι | u i ω ∈ s}) = m
Tactic: conv => intro; rw [Set.mem_Icc, Set.Icc_self, and_imp, and_imp]
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
ω : Ω
m : ι
hmn : m ≤ m
i : ι
hi₁ : m ≤ i
hi₂ : i ≤ m
hi : u i ω ∈ s
⊢ sInf ({m} ∩ {i : ι | u i ω ∈ s}) = m
have inl : Subset (α := Set ι) {m} {i : ι | u i ω ∈ s}
Tactic: rw [Set.inter_eq_left.2, csInf_singleton]