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 β
n i : ι
ω : Ω
inst_1 : WellFoundedLT ι
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
have mp : ∀ (h' : i' ≤ i) (h_le : n ≤ i'), (↑i' : WithTop ι).untopA ∈ Set.Icc n i
Tactic: norm_cast at h' h_le
Cleared hypotheses: h', h_le
-- 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' : ∃ j ∈ Set.Icc n i, u j ω ∈ s
⊢ hittingAfter u s n ω ≤ (↑i : WithTop ι)
have mpr : ∀ (j : ι) (hj₁ : j ∈ Set.Icc n i) (hj₂ : u j ω ∈ s), hittingAfter u s n ω ≤ (↑i : WithTop ι)
Tactic: obtain ⟨j, hj₁, hj₂⟩ := 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 ι
j : ι
hj₁ : j ∈ Set.Icc n i
hj₂ : u j ω ∈ s
⊢ hittingAfter u s n ω ≤ (↑i : WithTop ι)
have mpr : hittingAfter u s n ω ≤ (↑j : WithTop ι)
Tactic: refine le_trans ?_ (mod_cast hj₁.2 : (j : WithTop ι) ≤ i)
-- 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 i : ι
hi : i < m
⊢ hittingBtwn u s n m ω ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s
have pos : ∀ (h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s), hittingBtwn u s n m ω ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s
Tactic: by_cases h_exists : ∃ 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 i : ι
hi : i < m
pos : ∀ (h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s), 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 neg : ∀ (h_exists : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s), hittingBtwn u s n m ω ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s
Tactic: by_cases h_exists : ∃ 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 i : ι
hi : i < 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 pos : (∃ j ∈ Set.Icc n i, u j ω ∈ s) ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s
Tactic: rw [hittingBtwn_le_iff_of_exists 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 i : ι
hi : i < 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 neg : m ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s
Tactic: simp_rw [hittingBtwn, if_neg 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 i : ι
hi : i < m
h_exists : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ m ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s
have h_exists₁ : ∀ (j : ι) (_ : j ∈ Set.Icc n m), u j ω ∉ s
Tactic: push Not at 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 : ι
ω : Ω
inst_1 : WellFoundedLT ι
m i : ι
hi : i < m
h_exists : ∀ (j : ι) (_ : j ∈ Set.Icc n m), u j ω ∉ s
⊢ m ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s
have neg : ∀ (x : ι), n ≤ x → x ≤ i → u x ω ∉ s
Tactic: simp only [not_le.mpr hi, Set.mem_Icc, false_iff, not_exists, not_and, 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 β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
⊢ hittingBtwn u s n m ω < i ↔ ∃ j ∈ Set.Ico n i, u j ω ∈ s
have mp : hittingBtwn u s n m ω < i → ∃ j ∈ Set.Ico 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 : ι
ω : Ω
m i : ι
hi : i ≤ m
mp : hittingBtwn u s n m ω < i → ∃ j ∈ Set.Ico n i, u j ω ∈ s
⊢ hittingBtwn u s n m ω < i ↔ ∃ j ∈ Set.Ico n i, u j ω ∈ s
have mpr : (∃ j ∈ Set.Ico 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 : ι
ω : Ω
m i : ι
hi : i ≤ m
h' : hittingBtwn u s n m ω < i
⊢ ∃ j ∈ Set.Icc n m, u j ω ∈ s
have by_contra : ∀ (h : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s), 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 i : ι
hi : i ≤ m
h' : hittingBtwn u s n m ω < i
h : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ False
have h'₁ : ¬i ≤ m
Tactic: simp_rw [hittingBtwn, if_neg h, ← not_le] at 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 i : ι
hi : i ≤ m
h' : hittingBtwn u s n m ω < i
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s
have h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
Tactic: have h : ∃ j ∈ Set.Icc n m, u j ω ∈ s := by
      by_contra h
      simp_rw [hittingBtwn, if_neg h, ← not_le] at h'
      exact h' hi
-- 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 i : ι
hi : i ≤ m
h' : hittingBtwn u s n m ω < i
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s
have hni : n < i
Tactic: have hni : n < i := (le_hittingBtwn_of_exists h).trans_lt 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 i : ι
hi : i ≤ m
h' : hittingBtwn u s n m ω < i
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
hni : n < i
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s
have h_le : n ≤ hittingBtwn u s n m ω
Tactic: have h_le := le_hittingBtwn (u := u) (s := s) (hni.le.trans 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 i : ι
hi : i ≤ m
h' : hittingBtwn u s n m ω < i
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
hni : n < i
h_le : n ≤ hittingBtwn u s n m ω
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s
have mp : ∀ (h' : ∃ b ∈ Set.Icc n m ∩ {i : ι | u i ω ∈ s}, b < i) (h : ∃ j ∈ Set.Icc n m, u j ω ∈ s) (hni : n < i)
  (h_le : n ≤ hittingBtwn u s n m ω), ∃ j ∈ Set.Ico n i, u j ω ∈ s
Tactic: rw [hittingBtwn, if_pos h, csInf_lt_iff] at h'
Cleared hypotheses: h', h, hni, h_le
-- 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 i : ι
hi : i ≤ m
h' : hittingBtwn u s n m ω < i
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
hni : n < i
h_le : n ≤ hittingBtwn u s n m ω
mp :
  ∀ (h' : ∃ b ∈ Set.Icc n m ∩ {i : ι | u i ω ∈ s}, b < i) (h : ∃ j ∈ Set.Icc n m, u j ω ∈ s) (hni : n < i)
    (h_le : n ≤ hittingBtwn u s n m ω), ∃ j ∈ Set.Ico n i, u j ω ∈ s
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s
have mp₁ : ∀ (h' : sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) < i) (h : ∃ j ∈ Set.Icc n m, u j ω ∈ s) (hni : n < i)
  (h_le : n ≤ hittingBtwn u s n m ω), BddBelow (Set.Icc n m ∩ {i : ι | u i ω ∈ s})
Tactic: rw [hittingBtwn, if_pos h, csInf_lt_iff] at h'
Cleared hypotheses: h', h, hni, h_le
-- 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 i : ι
hi : i ≤ m
h' : hittingBtwn u s n m ω < i
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
hni : n < i
h_le : n ≤ hittingBtwn u s n m ω
mp :
  ∀ (h' : ∃ b ∈ Set.Icc n m ∩ {i : ι | u i ω ∈ s}, b < i) (h : ∃ j ∈ Set.Icc n m, u j ω ∈ s) (hni : n < i)
    (h_le : n ≤ hittingBtwn u s n m ω), ∃ j ∈ Set.Ico n i, u j ω ∈ s
mp₁ :
  ∀ (h' : sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) < i) (h : ∃ j ∈ Set.Icc n m, u j ω ∈ s) (hni : n < i)
    (h_le : n ≤ hittingBtwn u s n m ω), BddBelow (Set.Icc n m ∩ {i : ι | u i ω ∈ s})
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s
have mp₂ : ∀ (h' : sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) < i) (h : ∃ j ∈ Set.Icc n m, u j ω ∈ s) (hni : n < i)
  (h_le : n ≤ hittingBtwn u s n m ω), (Set.Icc n m ∩ {i : ι | u i ω ∈ s}).Nonempty
Tactic: rw [hittingBtwn, if_pos h, csInf_lt_iff] at h'
Cleared hypotheses: h', h, hni, h_le
-- 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 i : ι
hi : i ≤ m
h' : sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) < i
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
hni : n < i
h_le : n ≤ hittingBtwn u s n m ω
⊢ n ∈ lowerBounds (Set.Icc n m ∩ {i : ι | u i ω ∈ s})
have simp : ∀ (x : ι), n ≤ x → x ≤ m → u x ω ∈ s → n ≤ x
Tactic: simp [mem_lowerBounds]
-- 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 i : ι
hi : i ≤ m
h' : ∃ b ∈ Set.Icc n m ∩ {i : ι | u i ω ∈ s}, b < i
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
hni : n < i
h_le : n ≤ hittingBtwn u s n m ω
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s
have h'₁ : ∃ (b : ι), ((n ≤ b ∧ b ≤ m) ∧ u b ω ∈ s) ∧ b < i
Tactic: simp only [Set.mem_inter_iff, Set.mem_Icc, Set.mem_setOf_eq] at 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 : ι
ω : Ω
m i : ι
hi : i ≤ m
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
hni : n < i
h_le : n ≤ hittingBtwn u s n m ω
h' : ∃ (b : ι), ((n ≤ b ∧ b ≤ m) ∧ u b ω ∈ s) ∧ b < i
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s
have mp : ∀ (j : ι) (hji : j < i) (hj_mem : u j ω ∈ s) (hnj : n ≤ j) (hjm : j ≤ m), ∃ j ∈ Set.Ico n i, u j ω ∈ s
Tactic: obtain ⟨j, ⟨⟨hnj, hjm⟩, hj_mem⟩, hji⟩ := 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 : ι
ω : Ω
m i : ι
hi : i ≤ m
h' : ∃ j ∈ Set.Ico n i, u j ω ∈ s
⊢ hittingBtwn u s n m ω < i
have mpr : ∀ (k : ι) (hk₁ : k ∈ Set.Ico n 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 : ι
ω : Ω
m i : ι
hi : i ≤ m
k : ι
hk₁ : k ∈ Set.Ico n i
hk₂ : u k ω ∈ s
⊢ hittingBtwn u s n m ω < i
have mpr : hittingBtwn u s n m ω ≤ k
Tactic: refine lt_of_le_of_lt ?_ hk₁.2
-- 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 : ι
ω : Ω
⊢ hittingAfter u s n ω < (↑i : WithTop ι) ↔ ∃ j ∈ Set.Ico n i, u j ω ∈ s
have mp : hittingAfter u s n ω < (↑i : WithTop ι) → ∃ j ∈ Set.Ico 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 : ι
ω : Ω
mp : hittingAfter u s n ω < (↑i : WithTop ι) → ∃ j ∈ Set.Ico n i, u j ω ∈ s
⊢ hittingAfter u s n ω < (↑i : WithTop ι) ↔ ∃ j ∈ Set.Ico n i, u j ω ∈ s
have mpr : (∃ j ∈ Set.Ico 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 : ι
ω : Ω
h' : hittingAfter u s n ω < (↑i : WithTop ι)
⊢ ∃ j ∈ Set.Ico 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 : ι
ω : Ω
h' : hittingAfter u s n ω < (↑i : WithTop ι)
h_top : hittingAfter u s n ω ≠ ⊤
⊢ ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
have h_top₁ : ¬∀ (j : ι), n ≤ j → u j ω ∉ s
Tactic: rw [ne_eq, hittingAfter_eq_top_iff] at h_top
Cleared hypotheses: h_top
-- 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 : ι
ω : Ω
h' : hittingAfter u s n ω < (↑i : WithTop ι)
h_top : hittingAfter u s n ω ≠ ⊤
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s
have h_exists : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
Tactic: have h_exists : ∃ j, n ≤ j ∧ u j ω ∈ s := by
      rw [ne_eq, hittingAfter_eq_top_iff] at h_top
      push Not at h_top
      exact h_top
-- 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 : ι
ω : Ω
h' : hittingAfter u s n ω < (↑i : WithTop ι)
h_top : hittingAfter u s n ω ≠ ⊤
h_exists : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
⊢ ∃ j ∈ Set.Ico 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 (hypothesis)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
h' : hittingAfter u s n ω < (↑i : WithTop ι)
h_top : hittingAfter u s n ω ≠ ⊤
h_exists : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
h_le : (↑n : WithTop ι) ≤ hittingAfter u s n ω
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s
have h'₁ : (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ s}) : WithTop ι) < (↑i : WithTop ι)
Tactic: rw [hittingAfter, if_pos h_exists] at h'
Cleared hypotheses: h', h_top, h_exists, h_le
-- 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 : ι
ω : Ω
h' : (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ s}) : WithTop ι) < (↑i : WithTop ι)
h_top : hittingAfter u s n ω ≠ ⊤
h_exists : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
h_le : (↑n : WithTop ι) ≤ hittingAfter u s n ω
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s
have h'₁ : sInf {i : ι | n ≤ i ∧ u i ω ∈ s} < i
Tactic: norm_cast at 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 : ι
ω : Ω
h_top : hittingAfter u s n ω ≠ ⊤
h_exists : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
h_le : (↑n : WithTop ι) ≤ hittingAfter u s n ω
h' : sInf {i : ι | n ≤ i ∧ u i ω ∈ s} < i
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s
have mp : ∀ (h' : ∃ (b : ι), Membership.mem (γ := Set ι) {i : ι | n ≤ i ∧ u i ω ∈ s} b ∧ b < i), ∃ j ∈ Set.Ico n i, u j ω ∈ s
Tactic: rw [csInf_lt_iff] at 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 : ι
ω : Ω
h_top : hittingAfter u s n ω ≠ ⊤
h_exists : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
h_le : (↑n : WithTop ι) ≤ hittingAfter u s n ω
h' : sInf {i : ι | n ≤ i ∧ u i ω ∈ s} < i
mp : ∀ (h' : ∃ (b : ι), Membership.mem (γ := Set ι) {i : ι | n ≤ i ∧ u i ω ∈ s} b ∧ b < i), ∃ j ∈ Set.Ico n i, u j ω ∈ s
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s
have mp₁ : BddBelow.{u_3} (α := ι) {i : ι | n ≤ i ∧ u i ω ∈ s}
Tactic: rw [csInf_lt_iff] at 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 : ι
ω : Ω
h_top : hittingAfter u s n ω ≠ ⊤
h_exists : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
h_le : (↑n : WithTop ι) ≤ hittingAfter u s n ω
h' : sInf {i : ι | n ≤ i ∧ u i ω ∈ s} < i
mp : ∀ (h' : ∃ (b : ι), Membership.mem (γ := Set ι) {i : ι | n ≤ i ∧ u i ω ∈ s} b ∧ b < i), ∃ j ∈ Set.Ico n i, u j ω ∈ s
mp₁ : BddBelow.{u_3} (α := ι) {i : ι | n ≤ i ∧ u i ω ∈ s}
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s
have mp₂ : Set.Nonempty.{u_3} (α := ι) {i : ι | n ≤ i ∧ u i ω ∈ s}
Tactic: rw [csInf_lt_iff] at 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 : ι
ω : Ω
h_top : hittingAfter u s n ω ≠ ⊤
h_exists : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
h_le : (↑n : WithTop ι) ≤ hittingAfter u s n ω
h' : sInf {i : ι | n ≤ i ∧ u i ω ∈ s} < i
⊢ Membership.mem (γ := Set ι) (lowerBounds {i : ι | n ≤ i ∧ u i ω ∈ s}) n
have simp : ∀ (x : ι), n ≤ x → u x ω ∈ s → n ≤ x
Tactic: simp [mem_lowerBounds]
-- 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 : ι
ω : Ω
h_top : hittingAfter u s n ω ≠ ⊤
h_exists : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s
h_le : (↑n : WithTop ι) ≤ hittingAfter u s n ω
h' : ∃ (b : ι), (n ≤ b ∧ u b ω ∈ s) ∧ b < i
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s
have mp : ∀ (j : ι) (hj₁ : n ≤ j ∧ u j ω ∈ s) (hj₂ : j < i), ∃ j ∈ Set.Ico n i, u j ω ∈ s
Tactic: obtain ⟨j, hj₁, hj₂⟩ := 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 : ι
ω : Ω
h' : ∃ j ∈ Set.Ico n i, u j ω ∈ s
⊢ hittingAfter u s n ω < (↑i : WithTop ι)
have mpr : ∀ (j : ι) (hj₁ : j ∈ Set.Ico n i) (hj₂ : u j ω ∈ s), hittingAfter u s n ω < (↑i : WithTop ι)
Tactic: obtain ⟨j, hj₁, hj₂⟩ := 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 : ι
ω : Ω
j : ι
hj₁ : j ∈ Set.Ico n i
hj₂ : u j ω ∈ s
⊢ hittingAfter u s n ω < (↑i : WithTop ι)
have mpr : hittingAfter u s n ω ≤ (↑j : WithTop ι)
Tactic: refine lt_of_le_of_lt ?_ (mod_cast hj₁.2 : (j : WithTop ι) < i)
-- 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₁ m₂ : ι
h : m₁ ≤ m₂
h' : ∃ j ∈ Set.Icc n m₁, u j ω ∈ s
⊢ hittingBtwn u s n m₁ ω = hittingBtwn u s n m₂ ω
have simp : sInf (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s}) =
  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, if_pos 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₁ m₂ : ι
h : m₁ ≤ m₂
h' : ∃ j ∈ Set.Icc n m₁, u j ω ∈ s
⊢ sInf (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s}) =
    if ∃ j ∈ Set.Icc n m₂, u j ω ∈ s then sInf (Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s}) else m₂
have obtain : ∀ (j : ι) (hj₁ : j ∈ Set.Icc n m₁) (hj₂ : u j ω ∈ s),
  sInf (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s}) =
    if ∃ j ∈ Set.Icc n m₂, u j ω ∈ s then sInf (Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s}) else m₂
Tactic: obtain ⟨j, hj₁, hj₂⟩ := 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 : ι
ω : Ω
m₁ m₂ : ι
h : m₁ ≤ m₂
j : ι
hj₁ : j ∈ Set.Icc n m₁
hj₂ : u j ω ∈ s
⊢ sInf (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s}) =
    if ∃ j ∈ Set.Icc n m₂, u j ω ∈ s then sInf (Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s}) else m₂
have rw : sInf (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s}) = sInf (Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s})
Tactic: rw [if_pos]
-- 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₁ m₂ : ι
h : m₁ ≤ m₂
j : ι
hj₁ : j ∈ Set.Icc n m₁
hj₂ : u j ω ∈ s
rw : sInf (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s}) = sInf (Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s})
⊢ sInf (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s}) =
    if ∃ j ∈ Set.Icc n m₂, u j ω ∈ s then sInf (Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s}) else m₂
have hc : ∃ j ∈ Set.Icc n m₂, u j ω ∈ s
Tactic: rw [if_pos]
-- 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₁ m₂ : ι
h : m₁ ≤ m₂
j : ι
hj₁ : j ∈ Set.Icc n m₁
hj₂ : u j ω ∈ s
⊢ sInf (Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s}) ≤ sInf (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s})
have ht : BddBelow (Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s})
Tactic: gcongr
-- 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₁ m₂ : ι
h : m₁ ≤ m₂
j : ι
hj₁ : j ∈ Set.Icc n m₁
hj₂ : u j ω ∈ s
ht : BddBelow (Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s})
⊢ sInf (Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s}) ≤ sInf (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s})
have hs : (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s}).Nonempty
Tactic: gcongr
-- 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₁ m₂ : ι
h : m₁ ≤ m₂
j : ι
hj₁ : j ∈ Set.Icc n m₁
hj₂ : u j ω ∈ s
⊢ sInf (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s}) = sInf (Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s})
have refine : sInf (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s}) ≤ sInf (Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s})
Tactic: refine le_antisymm ?_ (by gcongr; exacts [bddBelow_Icc.inter_of_left, ⟨j, hj₁, hj₂⟩])
-- 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₁ m₂ : ι
h : m₁ ≤ m₂
j : ι
hj₁ : j ∈ Set.Icc n m₁
hj₂ : u j ω ∈ s
⊢ sInf (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s}) ≤ sInf (Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s})
have refine : ∀ (i : ι) (hi : i ∈ Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s}), sInf (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s}) ≤ i
Tactic: refine le_csInf ⟨j, Set.Icc_subset_Icc_right h hj₁, hj₂⟩ fun i 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₁ m₂ : ι
h : m₁ ≤ m₂
j : ι
hj₁ : j ∈ Set.Icc n m₁
hj₂ : u j ω ∈ s
i : ι
hi : i ∈ Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s}
⊢ sInf (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s}) ≤ i
have pos : ∀ (hi' : i ≤ m₁), sInf (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s}) ≤ i
Tactic: by_cases hi' : i ≤ m₁