awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : (if ∃ j ∈ Set.Icc m m, u j ω ∈ s then sInf (Set.Icc m m ∩ {i : ι | u i ω ∈ s}) else m) = m
Tactic: classical
    rw [hittingBtwn, ite_eq_right_iff, forall_exists_index]
    conv => intro; rw [Set.mem_Icc, Set.Icc_self, and_imp, and_imp]
    intro i hi₁ hi₂ hi
    rw [Set.inter_eq_left.2, csInf_singleton]
    exact Set.singleton_subset_iff.2 (le_antisymm hi₂ hi₁ ▸ hi)
-- 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
inl : (if ∃ j ∈ Set.Icc m m, u j ω ∈ s then sInf (Set.Icc m m ∩ {i : ι | u i ω ∈ s}) else m) = m
⊢ hittingBtwn u s m m ω = m
have inl₁ : (∃ j ∈ Set.Icc m m, u j ω ∈ s) → sInf (Set.Icc m m ∩ {i : ι | u i ω ∈ s}) = m
Tactic: classical
    rw [hittingBtwn, ite_eq_right_iff, forall_exists_index]
    conv => intro; rw [Set.mem_Icc, Set.Icc_self, and_imp, and_imp]
    intro i hi₁ hi₂ hi
    rw [Set.inter_eq_left.2, csInf_singleton]
    exact Set.singleton_subset_iff.2 (le_antisymm hi₂ hi₁ ▸ hi)
-- 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
inl : (if ∃ j ∈ Set.Icc m m, u j ω ∈ s then sInf (Set.Icc m m ∩ {i : ι | u i ω ∈ s}) else m) = m
inl₁ : (∃ j ∈ Set.Icc m m, u j ω ∈ s) → sInf (Set.Icc m m ∩ {i : ι | u i ω ∈ s}) = 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: classical
    rw [hittingBtwn, ite_eq_right_iff, forall_exists_index]
    conv => intro; rw [Set.mem_Icc, Set.Icc_self, and_imp, and_imp]
    intro i hi₁ hi₂ hi
    rw [Set.inter_eq_left.2, csInf_singleton]
    exact Set.singleton_subset_iff.2 (le_antisymm hi₂ hi₁ ▸ hi)
-- 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
inl : (if ∃ j ∈ Set.Icc m m, u j ω ∈ s then sInf (Set.Icc m m ∩ {i : ι | u i ω ∈ s}) else m) = m
inl₁ : (∃ j ∈ Set.Icc m m, u j ω ∈ s) → sInf (Set.Icc m m ∩ {i : ι | u i ω ∈ s}) = m
inl₂ inl₃ inl₄ : ∀ (x : ι) (h : x ∈ Set.Icc m m ∧ u x ω ∈ s), sInf (Set.Icc m m ∩ {i : ι | u i ω ∈ s}) = m
⊢ hittingBtwn u s m m ω = m
have inl₅ : ∀ (x : ι), m ≤ x → x ≤ m → u x ω ∈ s → sInf ({m} ∩ {i : ι | u i ω ∈ s}) = m
Tactic: classical
    rw [hittingBtwn, ite_eq_right_iff, forall_exists_index]
    conv => intro; rw [Set.mem_Icc, Set.Icc_self, and_imp, and_imp]
    intro i hi₁ hi₂ hi
    rw [Set.inter_eq_left.2, csInf_singleton]
    exact Set.singleton_subset_iff.2 (le_antisymm hi₂ hi₁ ▸ hi)
-- 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
inl : (if ∃ j ∈ Set.Icc m m, u j ω ∈ s then sInf (Set.Icc m m ∩ {i : ι | u i ω ∈ s}) else m) = m
inl₁ : (∃ j ∈ Set.Icc m m, u j ω ∈ s) → sInf (Set.Icc m m ∩ {i : ι | u i ω ∈ s}) = m
inl₂ inl₃ inl₄ : ∀ (x : ι) (h : x ∈ Set.Icc m m ∧ u x ω ∈ s), sInf (Set.Icc m m ∩ {i : ι | u i ω ∈ s}) = m
inl₅ inl₆ : ∀ (i : ι) (hi₁ : m ≤ i) (hi₂ : i ≤ m) (hi : u i ω ∈ s), sInf ({m} ∩ {i : ι | u i ω ∈ s}) = m
⊢ hittingBtwn u s m m ω = m
have inl₇ : ∀ (i : ι) (hi₁ : m ≤ i) (hi₂ : i ≤ m) (hi : u i ω ∈ s), Subset (α := Set ι) {m} {i : ι | u i ω ∈ s}
Tactic: classical
    rw [hittingBtwn, ite_eq_right_iff, forall_exists_index]
    conv => intro; rw [Set.mem_Icc, Set.Icc_self, and_imp, and_imp]
    intro i hi₁ hi₂ hi
    rw [Set.inter_eq_left.2, csInf_singleton]
    exact Set.singleton_subset_iff.2 (le_antisymm hi₂ hi₁ ▸ hi)
-- 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 : ι
hnm : n ≤ m
ω : Ω
⊢ n ≤ hittingBtwn u s n m ω
have simp : n ≤ if ∃ j ∈ Set.Icc n m, u j ω ∈ s then sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) else 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 : ι
hnm : n ≤ m
ω : Ω
⊢ n ≤ if ∃ j ∈ Set.Icc n m, u j ω ∈ s then sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) else m
have pos : ∀ (h : ∃ j ∈ Set.Icc n m, u j ω ∈ s), n ≤ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s})
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 : ι
hnm : n ≤ m
ω : Ω
pos : ∀ (h : ∃ j ∈ Set.Icc n m, u j ω ∈ s), n ≤ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s})
⊢ n ≤ if ∃ j ∈ Set.Icc n m, u j ω ∈ s then sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) else m
have neg : ∀ (h : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s), n ≤ 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 : ι
hnm : n ≤ m
ω : Ω
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ n ≤ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s})
have pos : (Set.Icc n m ∩ {i : ι | u i ω ∈ s}).Nonempty
Tactic: refine le_csInf ?_ fun b hb => ?_
-- 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 : ι
hnm : n ≤ m
ω : Ω
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
pos : (Set.Icc n m ∩ {i : ι | u i ω ∈ s}).Nonempty
⊢ n ≤ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s})
have pos₁ : ∀ (b : ι) (hb : b ∈ Set.Icc n m ∩ {i : ι | u i ω ∈ s}), n ≤ b
Tactic: refine le_csInf ?_ fun b hb => ?_
-- 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 : ι
hnm : n ≤ m
ω : Ω
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ (Set.Icc n m ∩ {i : ι | u i ω ∈ s}).Nonempty
have pos : ∀ (k : ι) (hk_Icc : k ∈ Set.Icc n m) (hk_s : u k ω ∈ s), (Set.Icc n m ∩ {i : ι | u i ω ∈ s}).Nonempty
Tactic: obtain ⟨k, hk_Icc, hk_s⟩ := 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 : ι
hnm : n ≤ m
ω : Ω
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
b : ι
hb : b ∈ Set.Icc n m ∩ {i : ι | u i ω ∈ s}
⊢ n ≤ b
have hb₁ : b ∈ Set.Icc n m ∧ Membership.mem (γ := Set ι) {i : ι | u i ω ∈ s} b
Tactic: rw [Set.mem_inter_iff] at hb
Cleared hypotheses: hb
-- 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 : ι
ω : Ω
⊢ (↑n : WithTop ι) ≤ if ∃ (j : ι), n ≤ j ∧ u j ω ∈ s then (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ s}) : WithTop ι) else ⊤
have pos : ∀ (h : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s), (↑n : WithTop ι) ≤ (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ s}) : WithTop ι)
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 : ι
ω : Ω
pos : ∀ (h : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s), (↑n : WithTop ι) ≤ (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ s}) : WithTop ι)
⊢ (↑n : WithTop ι) ≤ if ∃ (j : ι), n ≤ j ∧ u j ω ∈ s then (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ s}) : WithTop ι) else ⊤
have neg : ∀ (h : ¬∃ (j : ι), n ≤ j ∧ u j ω ∈ s), (↑n : WithTop ι) ≤ ⊤
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_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ n ≤ hittingBtwn u s n m ω
have refine : n ≤ m
Tactic: refine le_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 : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ n ≤ m
have by_contra : ∀ (h : ¬n ≤ m), False
Tactic: by_contra 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 : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h : ¬n ≤ m
⊢ False
have h_exists₁ : ∃ (j : ι), Membership.mem (γ := Set ι) ∅ j ∧ u j ω ∈ s
Tactic: rw [Set.Icc_eq_empty_of_lt (not_le.mp h)] at h_exists
Cleared hypotheses: h_exists, 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 : ι
ω : Ω
inst_1 : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ u (hittingBtwn u s n m ω) ω ∈ s
have simp_rw : u (sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s})) ω ∈ s
Tactic: simp_rw [hittingBtwn, if_pos h_exists]
-- 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 : ι
ω : Ω
inst_1 : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ (Set.Icc n m ∩ {i : ι | u i ω ∈ s}).Nonempty
have obtain : ∀ (k : ι) (hk₁ : k ∈ Set.Icc n m) (hk₂ : u k ω ∈ s), (Set.Icc n m ∩ {i : ι | u i ω ∈ s}).Nonempty
Tactic: obtain ⟨k, hk₁, hk₂⟩ := h_exists
Cleared hypotheses: h_exists
-- 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 : ι
ω : Ω
inst_1 : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ u (sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s})) ω ∈ s
have h_nonempty : (Set.Icc n m ∩ {i : ι | u i ω ∈ s}).Nonempty
Tactic: have h_nonempty : (Set.Icc n m ∩ {i : ι | u i ω ∈ s}).Nonempty := by
    obtain ⟨k, hk₁, hk₂⟩ := h_exists
    exact ⟨k, Set.mem_inter hk₁ hk₂⟩
-- 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 : ι
ω : Ω
inst_1 : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h_nonempty : (Set.Icc n m ∩ {i : ι | u i ω ∈ s}).Nonempty
⊢ u (sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s})) ω ∈ s
have h_mem : sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ∈ Set.Icc n m ∩ {i : ι | u i ω ∈ s}
Tactic: have h_mem := csInf_mem h_nonempty
-- 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 : ι
ω : Ω
inst_1 : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h_nonempty : (Set.Icc n m ∩ {i : ι | u i ω ∈ s}).Nonempty
h_mem : sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ∈ Set.Icc n m ∩ {i : ι | u i ω ∈ s}
⊢ u (sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s})) ω ∈ s
have h_mem₁ : sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ∈ Set.Icc n m ∧
  Membership.mem (γ := Set ι) {i : ι | u i ω ∈ s} (sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}))
Tactic: rw [Set.mem_inter_iff] at h_mem
Cleared hypotheses: h_mem
-- 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 : ι
ω : Ω
inst_1 : WellFoundedLT ι
h_exists : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
⊢ u (hittingAfter u s n ω).untopA ω ∈ s
have rw : u (WithTop.untopA (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ s}) : WithTop ι)) ω ∈ s
Tactic: rw [hittingAfter, if_pos h_exists]
-- 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 : ι
ω : Ω
inst_1 : WellFoundedLT ι
h_exists : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
⊢ Set.Nonempty.{u_3} (α := ι) {i : ι | n ≤ i ∧ u i ω ∈ s}
have obtain : ∀ (k : ι) (hk₁ : n ≤ k) (hk₂ : u k ω ∈ s), Set.Nonempty.{u_3} (α := ι) {i : ι | n ≤ i ∧ u i ω ∈ s}
Tactic: obtain ⟨k, hk₁, hk₂⟩ := h_exists
Cleared hypotheses: h_exists
-- 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 : ι
ω : Ω
inst_1 : WellFoundedLT ι
h_exists : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
⊢ u (WithTop.untopA (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ s}) : WithTop ι)) ω ∈ s
have h_nonempty : Set.Nonempty.{u_3} (α := ι) {i : ι | n ≤ i ∧ u i ω ∈ s}
Tactic: have h_nonempty : {i : ι | n ≤ i ∧ u i ω ∈ s}.Nonempty := by
    obtain ⟨k, hk₁, hk₂⟩ := h_exists
    exact ⟨k, Set.mem_inter hk₁ 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 : ι
ω : Ω
inst_1 : WellFoundedLT ι
m : ι
hl : hittingBtwn u s n m ω < m
⊢ u (hittingBtwn u s n m ω) ω ∈ s
have pos : ∀ (h : ∃ j ∈ Set.Icc n m, u j ω ∈ s), u (hittingBtwn u s n m ω) ω ∈ s
Tactic: by_cases h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
-- 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 : ι
ω : Ω
inst_1 : WellFoundedLT ι
m : ι
hl : hittingBtwn u s n m ω < m
pos : ∀ (h : ∃ j ∈ Set.Icc n m, u j ω ∈ s), u (hittingBtwn u s n m ω) ω ∈ s
⊢ u (hittingBtwn u s n m ω) ω ∈ s
have neg : ∀ (h : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s), u (hittingBtwn u s n m ω) ω ∈ s
Tactic: by_cases h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
-- 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 : ι
ω : Ω
inst_1 : WellFoundedLT ι
m : ι
hl : hittingBtwn u s n m ω < m
h : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ u (hittingBtwn u s n m ω) ω ∈ s
have hl₁ : m < m
Tactic: simp_rw [hittingBtwn, if_neg h] at hl
Cleared hypotheses: hl
-- 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 : ι
ω : Ω
inst_1 : WellFoundedLT ι
hl : hittingAfter u s n ω ≠ ⊤
⊢ u (hittingAfter u s n ω).untopA ω ∈ s
have hl₁ : ∃ (x : ι) (_ : n ≤ x), u x ω ∈ s
Tactic: simp only [ne_eq, hittingAfter_eq_top_iff, not_forall, not_not] at hl
Cleared hypotheses: hl
-- 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 : ι
ω : Ω
inst_1 : WellFoundedLT ι
hl : ∃ (x : ι) (_ : n ≤ x), u x ω ∈ s
⊢ u (hittingAfter u s n ω).untopA ω ∈ s
have obtain : ∀ (j : ι) (hj₁ : n ≤ j) (hj₂ : u j ω ∈ s), u (hittingAfter u s n ω).untopA ω ∈ s
Tactic: obtain ⟨j, hj₁, hj₂⟩ := hl
Cleared hypotheses: hl
-- 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 i : ι
ω : Ω
m : ι
hin : n ≤ i
him : i ≤ m
his : u i ω ∈ s
⊢ hittingBtwn u s n m ω ≤ i
have h_exists : ∃ k ∈ Set.Icc n m, u k ω ∈ s
Tactic: have h_exists : ∃ k ∈ Set.Icc n m, u k ω ∈ s := ⟨i, ⟨hin, him⟩, his⟩
-- 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 i : ι
ω : Ω
m : ι
hin : n ≤ i
him : i ≤ m
his : u i ω ∈ s
h_exists : ∃ k ∈ Set.Icc n m, u k ω ∈ s
⊢ hittingBtwn u s n m ω ≤ i
have simp_rw : sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ≤ i
Tactic: simp_rw [hittingBtwn, if_pos h_exists]
-- 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 i : ι
ω : Ω
hin : n ≤ i
his : u i ω ∈ s
⊢ hittingAfter u s n ω ≤ (↑i : WithTop ι)
have h_exists : ∃ (k : ι), n ≤ k ∧ u k ω ∈ s
Tactic: have h_exists : ∃ k, n ≤ k ∧ u k ω ∈ s := ⟨i, hin, his⟩
-- 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 i : ι
ω : Ω
hin : n ≤ i
his : u i ω ∈ s
h_exists : ∃ (k : ι), n ≤ k ∧ u k ω ∈ s
⊢ hittingAfter u s n ω ≤ (↑i : WithTop ι)
have rw : (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ s}) : WithTop ι) ≤ (↑i : WithTop ι)
Tactic: rw [hittingAfter, if_pos h_exists]
-- 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 i : ι
ω : Ω
inst_1 : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ hittingBtwn u s n m ω ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s
have mp : hittingBtwn u s n m ω ≤ i → ∃ j ∈ Set.Icc n i, u j ω ∈ s
Tactic: constructor
-- 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 i : ι
ω : Ω
inst_1 : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
mp : hittingBtwn u s n m ω ≤ i → ∃ j ∈ Set.Icc n i, u j ω ∈ s
⊢ hittingBtwn u s n m ω ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s
have mpr : (∃ j ∈ Set.Icc n i, u j ω ∈ s) → hittingBtwn u s n m ω ≤ i
Tactic: constructor
-- 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 i : ι
ω : Ω
inst_1 : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h' : ∃ j ∈ Set.Icc n i, u j ω ∈ s
⊢ ∃ k ∈ Set.Icc n (min m i), u k ω ∈ s
have obtain : ∀ (k₁ : ι) (hk₁_mem : k₁ ∈ Set.Icc n m) (hk₁_s : u k₁ ω ∈ s), ∃ k ∈ Set.Icc n (min m i), u k ω ∈ s
Tactic: obtain ⟨k₁, hk₁_mem, hk₁_s⟩ := h_exists
Cleared hypotheses: h_exists
-- 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 i : ι
ω : Ω
inst_1 : WellFoundedLT ι
m : ι
h' : ∃ j ∈ Set.Icc n i, u j ω ∈ s
k₁ : ι
hk₁_mem : k₁ ∈ Set.Icc n m
hk₁_s : u k₁ ω ∈ s
⊢ ∃ k ∈ Set.Icc n (min m i), u k ω ∈ s
have obtain : ∀ (k₂ : ι) (hk₂_mem : k₂ ∈ Set.Icc n i) (hk₂_s : u k₂ ω ∈ s), ∃ k ∈ Set.Icc n (min m i), u k ω ∈ s
Tactic: obtain ⟨k₂, hk₂_mem, hk₂_s⟩ := h'
Cleared hypotheses: 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 i : ι
ω : Ω
inst_1 : WellFoundedLT ι
m k₁ : ι
hk₁_mem : k₁ ∈ Set.Icc n m
hk₁_s : u k₁ ω ∈ s
k₂ : ι
hk₂_mem : k₂ ∈ Set.Icc n i
hk₂_s : u k₂ ω ∈ s
⊢ ∃ k ∈ Set.Icc n (min m i), u k ω ∈ s
have refine : u (min k₁ k₂) ω ∈ s
Tactic: refine ⟨min k₁ k₂, ⟨le_min hk₁_mem.1 hk₂_mem.1, min_le_min hk₁_mem.2 hk₂_mem.2⟩, ?_⟩
-- 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 i : ι
ω : Ω
inst_1 : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h' : ∃ j ∈ Set.Icc n i, u j ω ∈ s
⊢ hittingBtwn u s n m ω ≤ i
have h'' : ∃ k ∈ Set.Icc n (min m i), u k ω ∈ s
Tactic: have h'' : ∃ k ∈ Set.Icc n (min m i), u k ω ∈ s := by
      obtain ⟨k₁, hk₁_mem, hk₁_s⟩ := h_exists
      obtain ⟨k₂, hk₂_mem, hk₂_s⟩ := h'
      refine ⟨min k₁ k₂, ⟨le_min hk₁_mem.1 hk₂_mem.1, min_le_min hk₁_mem.2 hk₂_mem.2⟩, ?_⟩
      exact min_rec' (fun j => u j ω ∈ s) hk₁_s hk₂_s
-- 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 i : ι
ω : Ω
inst_1 : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h' : ∃ j ∈ Set.Icc n i, u j ω ∈ s
h'' : ∃ k ∈ Set.Icc n (min m i), u k ω ∈ s
⊢ hittingBtwn u s n m ω ≤ i
have mpr : ∀ (k : ι) (hk₁ : k ∈ Set.Icc n (min m i)) (hk₂ : u k ω ∈ s), hittingBtwn u s n m ω ≤ i
Tactic: obtain ⟨k, hk₁, hk₂⟩ := h''
Cleared hypotheses: 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 i : ι
ω : Ω
inst_1 : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h' : ∃ j ∈ Set.Icc n i, u j ω ∈ s
k : ι
hk₁ : k ∈ Set.Icc n (min m i)
hk₂ : u k ω ∈ s
⊢ hittingBtwn u s n m ω ≤ i
have mpr : hittingBtwn u s n m ω ≤ k
Tactic: refine le_trans ?_ (hk₁.2.trans (min_le_right _ _))
-- 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 i : ι
ω : Ω
inst_1 : WellFoundedLT ι
⊢ hittingAfter u s n ω ≤ (↑i : WithTop ι) ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s
have mp : hittingAfter u s n ω ≤ (↑i : WithTop ι) → ∃ j ∈ Set.Icc n i, u j ω ∈ s
Tactic: constructor
-- 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 i : ι
ω : Ω
inst_1 : WellFoundedLT ι
mp : hittingAfter u s n ω ≤ (↑i : WithTop ι) → ∃ j ∈ Set.Icc n i, u j ω ∈ s
⊢ hittingAfter u s n ω ≤ (↑i : WithTop ι) ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s
have mpr : (∃ j ∈ Set.Icc n i, u j ω ∈ s) → hittingAfter u s n ω ≤ (↑i : WithTop ι)
Tactic: constructor
-- 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 i : ι
ω : Ω
inst_1 : WellFoundedLT ι
h' : hittingAfter u s n ω ≤ (↑i : WithTop ι)
⊢ ∃ j ∈ Set.Icc n i, u j ω ∈ s
have h_top : hittingAfter u s n ω ≠ ⊤
Tactic: have h_top : hittingAfter u s n ω ≠ ⊤ := fun h ↦ by simp [h] at 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 i : ι
ω : Ω
inst_1 : WellFoundedLT ι
h' : hittingAfter u s n ω ≤ (↑i : WithTop ι)
h_top : hittingAfter u s n ω ≠ ⊤
⊢ ∃ j ∈ Set.Icc n i, u j ω ∈ s
have h_le : (↑n : WithTop ι) ≤ hittingAfter u s n ω
Tactic: have h_le := le_hittingAfter (u := u) (s := s) (n := n) ω
-- 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 i : ι
ω : Ω
inst_1 : WellFoundedLT ι
h' : hittingAfter u s n ω ≤ (↑i : WithTop ι)
h_top : hittingAfter u s n ω ≠ ⊤
h_le : (↑n : WithTop ι) ≤ hittingAfter u s n ω
⊢ ∃ j ∈ Set.Icc n i, u j ω ∈ s
have mp : (hittingAfter u s n ω).untopA ∈ Set.Icc n i
Tactic: refine ⟨(hittingAfter u s n ω).untopA, ?_, hittingAfter_mem_set_of_ne_top h_top⟩
-- 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 i : ι
ω : Ω
inst_1 : WellFoundedLT ι
h' : hittingAfter u s n ω ≤ (↑i : WithTop ι)
h_top : hittingAfter u s n ω ≠ ⊤
h_le : (↑n : WithTop ι) ≤ hittingAfter u s n ω
⊢ (hittingAfter u s n ω).untopA ∈ Set.Icc n i
have mp : ∀ (i' : ι)
  (hittingAfter_le_iff : ∀ [WellFoundedLT ι], (↑i' : WithTop ι) ≤ (↑i : WithTop ι) ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s)
  (h' : (↑i' : WithTop ι) ≤ (↑i : WithTop ι)) (h_le : (↑n : WithTop ι) ≤ (↑i' : WithTop ι)),
  (↑i' : WithTop ι).untopA ∈ Set.Icc n i
Tactic: lift (hittingAfter u s n ω) to ι using h_top with i'
Cleared hypotheses: h', h_top, h_le