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 : ι
ω : Ω
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}
pos : ∀ (hi' : i ≤ m₁), sInf (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s}) ≤ i
⊢ sInf (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s}) ≤ i
have neg : ∀ (hi' : ¬i ≤ m₁), sInf (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s}) ≤ i
Tactic: by_cases hi' : i ≤ m₁
-- 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₁ 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}
hi' : ¬i ≤ m₁
⊢ sInf (Set.Icc n m₁ ∩ {i : ι | u i ω ∈ s}) ≤ i
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 (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
E F : Set β
hEF : E ≤ F
ω : Ω
⊢ LE.le.{u_3} (α := (fun (a : Ω) ↦ ι) ω) ((fun (x : Set β) ↦ hittingBtwn u x n m) F ω)
    ((fun (x : Set β) ↦ hittingBtwn u x n m) E ω)
have simp : (if ∃ j ∈ Set.Icc n m, u j ω ∈ F then sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ F}) else m) ≤
  if ∃ j ∈ Set.Icc n m, u j ω ∈ E then sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ E}) else m
Tactic: simp only [hittingBtwn_def]
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
E F : Set β
hEF : E ≤ F
ω : Ω
⊢ (if ∃ j ∈ Set.Icc n m, u j ω ∈ F then sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ F}) else m) ≤
    if ∃ j ∈ Set.Icc n m, u j ω ∈ E then sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ E}) else m
have pos : ∀ (hF : ∃ j ∈ Set.Icc n m, u j ω ∈ F) (hE : ∃ j ∈ Set.Icc n m, u j ω ∈ E),
  sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ F}) ≤ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ E})
Tactic: split_ifs with hF hE hE
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
E F : Set β
hEF : E ≤ F
ω : Ω
pos :
  ∀ (hF : ∃ j ∈ Set.Icc n m, u j ω ∈ F) (hE : ∃ j ∈ Set.Icc n m, u j ω ∈ E),
    sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ F}) ≤ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ E})
⊢ (if ∃ j ∈ Set.Icc n m, u j ω ∈ F then sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ F}) else m) ≤
    if ∃ j ∈ Set.Icc n m, u j ω ∈ E then sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ E}) else m
have neg : ∀ (hF : ∃ j ∈ Set.Icc n m, u j ω ∈ F) (hE : ¬∃ j ∈ Set.Icc n m, u j ω ∈ E), sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ F}) ≤ m
Tactic: split_ifs with hF hE hE
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
E F : Set β
hEF : E ≤ F
ω : Ω
pos :
  ∀ (hF : ∃ j ∈ Set.Icc n m, u j ω ∈ F) (hE : ∃ j ∈ Set.Icc n m, u j ω ∈ E),
    sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ F}) ≤ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ E})
neg :
  ∀ (hF : ∃ j ∈ Set.Icc n m, u j ω ∈ F) (hE : ¬∃ j ∈ Set.Icc n m, u j ω ∈ E),
    sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ F}) ≤ m
⊢ (if ∃ j ∈ Set.Icc n m, u j ω ∈ F then sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ F}) else m) ≤
    if ∃ j ∈ Set.Icc n m, u j ω ∈ E then sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ E}) else m
have pos₁ : ∀ (hF : ¬∃ j ∈ Set.Icc n m, u j ω ∈ F) (hE : ∃ j ∈ Set.Icc n m, u j ω ∈ E), m ≤ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ E})
Tactic: split_ifs with hF hE hE
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
E F : Set β
hEF : E ≤ F
ω : Ω
pos :
  ∀ (hF : ∃ j ∈ Set.Icc n m, u j ω ∈ F) (hE : ∃ j ∈ Set.Icc n m, u j ω ∈ E),
    sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ F}) ≤ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ E})
neg :
  ∀ (hF : ∃ j ∈ Set.Icc n m, u j ω ∈ F) (hE : ¬∃ j ∈ Set.Icc n m, u j ω ∈ E),
    sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ F}) ≤ m
pos₁ :
  ∀ (hF : ¬∃ j ∈ Set.Icc n m, u j ω ∈ F) (hE : ∃ j ∈ Set.Icc n m, u j ω ∈ E),
    m ≤ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ E})
⊢ (if ∃ j ∈ Set.Icc n m, u j ω ∈ F then sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ F}) else m) ≤
    if ∃ j ∈ Set.Icc n m, u j ω ∈ E then sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ E}) else m
have neg₁ : ∀ (hF : ¬∃ j ∈ Set.Icc n m, u j ω ∈ F) (hE : ¬∃ j ∈ Set.Icc n m, u j ω ∈ E), m ≤ m
Tactic: split_ifs with hF hE hE
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
E F : Set β
hEF : E ≤ F
ω : Ω
hF : ∃ j ∈ Set.Icc n m, u j ω ∈ F
hE : ∃ j ∈ Set.Icc n m, u j ω ∈ E
⊢ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ F}) ≤ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ E})
have pos : BddBelow (Set.Icc n m ∩ {i : ι | u i ω ∈ F})
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 : ι → Ω → β
n m : ι
E F : Set β
hEF : E ≤ F
ω : Ω
hF : ∃ j ∈ Set.Icc n m, u j ω ∈ F
hE : ∃ j ∈ Set.Icc n m, u j ω ∈ E
pos : BddBelow (Set.Icc n m ∩ {i : ι | u i ω ∈ F})
⊢ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ F}) ≤ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ E})
have pos₁ : ∀ (a : ι), E ⊆ F
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 : ι → Ω → β
n m : ι
E F : Set β
hEF : E ≤ F
ω : Ω
hF : ∃ j ∈ Set.Icc n m, u j ω ∈ F
hE : ∃ j ∈ Set.Icc n m, u j ω ∈ E
⊢ n ∈ lowerBounds (Set.Icc n m ∩ {i : ι | u i ω ∈ F})
have simp : ∀ (x : ι), n ≤ x → x ≤ m → u x ω ∈ F → 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 : ι → Ω → β
n m : ι
E F : Set β
hEF : E ≤ F
ω : Ω
hF : ∃ j ∈ Set.Icc n m, u j ω ∈ F
hE : ¬∃ j ∈ Set.Icc n m, u j ω ∈ E
⊢ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ F}) ≤ m
have neg : ∀ (t : ι) (ht : t ∈ Set.Icc n m ∧ u t ω ∈ F), sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ F}) ≤ m
Tactic: obtain ⟨t, ht⟩ := hF
Cleared hypotheses: hF
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
E F : Set β
hEF : E ≤ F
ω : Ω
hE : ¬∃ j ∈ Set.Icc n m, u j ω ∈ E
t : ι
ht : t ∈ Set.Icc n m ∧ u t ω ∈ F
⊢ n ∈ lowerBounds (Set.Icc n m ∩ {i : ι | u i ω ∈ F})
have simp : ∀ (x : ι), n ≤ x → x ≤ m → u x ω ∈ F → 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 : ι → Ω → β
n m : ι
E F : Set β
hEF : E ≤ F
ω : Ω
hF : ¬∃ j ∈ Set.Icc n m, u j ω ∈ F
hE : ∃ j ∈ Set.Icc n m, u j ω ∈ E
⊢ m ≤ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ E})
have pos : ∀ (t : ι) (ht : t ∈ Set.Icc n m ∧ u t ω ∈ E), m ≤ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ E})
Tactic: obtain ⟨t, ht⟩ := hE
Cleared hypotheses: hE
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n : ι
E F : Set β
hEF : E ≤ F
ω : Ω
⊢ LE.le.{u_3} (α := WithTop ι)
    (if ∃ (j : ι), n ≤ j ∧ u j ω ∈ F then (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ F}) : WithTop ι) else ⊤)
    (if ∃ (j : ι), n ≤ j ∧ u j ω ∈ E then (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ E}) : WithTop ι) else ⊤)
have pos : ∀ (hF : ∃ (j : ι), n ≤ j ∧ u j ω ∈ F) (hE : ∃ (j : ι), n ≤ j ∧ u j ω ∈ E),
  LE.le.{u_3} (α := WithTop ι) (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ F}) : WithTop ι)
    (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ E}) : WithTop ι)
Tactic: split_ifs with hF hE hE
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n : ι
E F : Set β
hEF : E ≤ F
ω : Ω
pos :
  ∀ (hF : ∃ (j : ι), n ≤ j ∧ u j ω ∈ F) (hE : ∃ (j : ι), n ≤ j ∧ u j ω ∈ E),
    LE.le.{u_3} (α := WithTop ι) (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ F}) : WithTop ι)
      (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ E}) : WithTop ι)
⊢ LE.le.{u_3} (α := WithTop ι)
    (if ∃ (j : ι), n ≤ j ∧ u j ω ∈ F then (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ F}) : WithTop ι) else ⊤)
    (if ∃ (j : ι), n ≤ j ∧ u j ω ∈ E then (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ E}) : WithTop ι) else ⊤)
have neg : ∀ (hF : ∃ (j : ι), n ≤ j ∧ u j ω ∈ F) (hE : ¬∃ (j : ι), n ≤ j ∧ u j ω ∈ E),
  LE.le.{u_3} (α := WithTop ι) (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ F}) : WithTop ι) ⊤
Tactic: split_ifs with hF hE hE
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n : ι
E F : Set β
hEF : E ≤ F
ω : Ω
pos :
  ∀ (hF : ∃ (j : ι), n ≤ j ∧ u j ω ∈ F) (hE : ∃ (j : ι), n ≤ j ∧ u j ω ∈ E),
    LE.le.{u_3} (α := WithTop ι) (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ F}) : WithTop ι)
      (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ E}) : WithTop ι)
neg :
  ∀ (hF : ∃ (j : ι), n ≤ j ∧ u j ω ∈ F) (hE : ¬∃ (j : ι), n ≤ j ∧ u j ω ∈ E),
    LE.le.{u_3} (α := WithTop ι) (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ F}) : WithTop ι) ⊤
⊢ LE.le.{u_3} (α := WithTop ι)
    (if ∃ (j : ι), n ≤ j ∧ u j ω ∈ F then (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ F}) : WithTop ι) else ⊤)
    (if ∃ (j : ι), n ≤ j ∧ u j ω ∈ E then (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ E}) : WithTop ι) else ⊤)
have pos₁ : ∀ (hF : ¬∃ (j : ι), n ≤ j ∧ u j ω ∈ F) (hE : ∃ (j : ι), n ≤ j ∧ u j ω ∈ E),
  LE.le.{u_3} (α := WithTop ι) ⊤ (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ E}) : WithTop ι)
Tactic: split_ifs with hF hE hE
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n : ι
E F : Set β
hEF : E ≤ F
ω : Ω
pos :
  ∀ (hF : ∃ (j : ι), n ≤ j ∧ u j ω ∈ F) (hE : ∃ (j : ι), n ≤ j ∧ u j ω ∈ E),
    LE.le.{u_3} (α := WithTop ι) (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ F}) : WithTop ι)
      (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ E}) : WithTop ι)
neg :
  ∀ (hF : ∃ (j : ι), n ≤ j ∧ u j ω ∈ F) (hE : ¬∃ (j : ι), n ≤ j ∧ u j ω ∈ E),
    LE.le.{u_3} (α := WithTop ι) (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ F}) : WithTop ι) ⊤
pos₁ :
  ∀ (hF : ¬∃ (j : ι), n ≤ j ∧ u j ω ∈ F) (hE : ∃ (j : ι), n ≤ j ∧ u j ω ∈ E),
    LE.le.{u_3} (α := WithTop ι) ⊤ (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ E}) : WithTop ι)
⊢ LE.le.{u_3} (α := WithTop ι)
    (if ∃ (j : ι), n ≤ j ∧ u j ω ∈ F then (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ F}) : WithTop ι) else ⊤)
    (if ∃ (j : ι), n ≤ j ∧ u j ω ∈ E then (↑(sInf {i : ι | n ≤ i ∧ u i ω ∈ E}) : WithTop ι) else ⊤)
have neg₁ : ∀ (hF : ¬∃ (j : ι), n ≤ j ∧ u j ω ∈ F) (hE : ¬∃ (j : ι), n ≤ j ∧ u j ω ∈ E), LE.le.{u_3} (α := WithTop ι) ⊤ ⊤
Tactic: split_ifs with hF hE hE
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n : ι
E F : Set β
hEF : E ≤ F
ω : Ω
hF : ∃ (j : ι), n ≤ j ∧ u j ω ∈ F
hE : ∃ (j : ι), n ≤ j ∧ u j ω ∈ E
⊢ LE.le.{u_3} (α := WithTop ι) (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ F}) : WithTop ι)
    (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ E}) : WithTop ι)
have pos : LE.le.{u_3} (α := ι) (sInf {j : ι | n ≤ j ∧ u j ω ∈ F}) (sInf {j : ι | n ≤ j ∧ u j ω ∈ E})
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n : ι
E F : Set β
hEF : E ≤ F
ω : Ω
hF : ∃ (j : ι), n ≤ j ∧ u j ω ∈ F
hE : ∃ (j : ι), n ≤ j ∧ u j ω ∈ E
⊢ LE.le.{u_3} (α := ι) (sInf {j : ι | n ≤ j ∧ u j ω ∈ F}) (sInf {j : ι | n ≤ j ∧ u j ω ∈ E})
have pos : BddBelow.{u_3} (α := ι) {j : ι | n ≤ j ∧ u j ω ∈ F}
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 : ι → Ω → β
n : ι
E F : Set β
hEF : E ≤ F
ω : Ω
hF : ∃ (j : ι), n ≤ j ∧ u j ω ∈ F
hE : ∃ (j : ι), n ≤ j ∧ u j ω ∈ E
pos : BddBelow.{u_3} (α := ι) {j : ι | n ≤ j ∧ u j ω ∈ F}
⊢ LE.le.{u_3} (α := ι) (sInf {j : ι | n ≤ j ∧ u j ω ∈ F}) (sInf {j : ι | n ≤ j ∧ u j ω ∈ E})
have pos₁ : ∀ (a : ι), n ≤ a → E ⊆ F
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 : ι → Ω → β
n : ι
E F : Set β
hEF : E ≤ F
ω : Ω
hF : ∃ (j : ι), n ≤ j ∧ u j ω ∈ F
hE : ∃ (j : ι), n ≤ j ∧ u j ω ∈ E
⊢ Membership.mem (γ := Set ι) (lowerBounds {j : ι | n ≤ j ∧ u j ω ∈ F}) n
have simp : ∀ (x : ι), Membership.mem (γ := Set ι) {j : ι | n ≤ j ∧ u j ω ∈ F} x → n ≤ x
Tactic: simp only [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 : ι → Ω → β
n : ι
E F : Set β
hEF : E ≤ F
ω : Ω
hF : ¬∃ (j : ι), n ≤ j ∧ u j ω ∈ F
hE : ∃ (j : ι), n ≤ j ∧ u j ω ∈ E
⊢ LE.le.{u_3} (α := WithTop ι) ⊤ (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ E}) : WithTop ι)
have pos : ∀ (t : ι) (ht : n ≤ t ∧ u t ω ∈ E), LE.le.{u_3} (α := WithTop ι) ⊤ (↑(sInf {j : ι | n ≤ j ∧ u j ω ∈ E}) : WithTop ι)
Tactic: obtain ⟨t, ht⟩ := hE
Cleared hypotheses: hE
-- 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₂ : ι
hm : m₁ ≤ m₂
⊢ LE.le.{u_3} (α := ι) ((fun (x : ι) ↦ hittingBtwn u s n x ω) m₁) ((fun (x : ι) ↦ hittingBtwn u s n x ω) m₂)
have pos : ∀ (h : ∃ j ∈ Set.Icc n m₁, u j ω ∈ s),
  LE.le.{u_3} (α := ι) ((fun (x : ι) ↦ hittingBtwn u s n x ω) m₁) ((fun (x : ι) ↦ hittingBtwn u s n x ω) m₂)
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 m₁ m₂ : ι
hm : m₁ ≤ m₂
pos :
  ∀ (h : ∃ j ∈ Set.Icc n m₁, u j ω ∈ s),
    LE.le.{u_3} (α := ι) ((fun (x : ι) ↦ hittingBtwn u s n x ω) m₁) ((fun (x : ι) ↦ hittingBtwn u s n x ω) m₂)
⊢ LE.le.{u_3} (α := ι) ((fun (x : ι) ↦ hittingBtwn u s n x ω) m₁) ((fun (x : ι) ↦ hittingBtwn u s n x ω) m₂)
have neg : ∀ (h : ¬∃ j ∈ Set.Icc n m₁, u j ω ∈ s),
  LE.le.{u_3} (α := ι) ((fun (x : ι) ↦ hittingBtwn u s n x ω) m₁) ((fun (x : ι) ↦ hittingBtwn u s n x ω) m₂)
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 m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j ∈ Set.Icc n m₁, u j ω ∈ s
⊢ LE.le.{u_3} (α := ι) ((fun (x : ι) ↦ hittingBtwn u s n x ω) m₁) ((fun (x : ι) ↦ hittingBtwn u s n x ω) m₂)
have neg : m₁ ≤ if ∃ j ∈ Set.Icc n m₂, u j ω ∈ s then sInf (Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s}) else m₂
Tactic: simp_rw [hittingBtwn, if_neg 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₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j ∈ Set.Icc n m₁, u j ω ∈ s
⊢ m₁ ≤ 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), m₁ ≤ 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₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j ∈ Set.Icc n m₁, u j ω ∈ s
pos : ∀ (h' : ∃ j ∈ Set.Icc n m₂, u j ω ∈ s), m₁ ≤ 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₂
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₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j ∈ Set.Icc n m₁, u j ω ∈ s
h' : ∃ j ∈ Set.Icc n m₂, u j ω ∈ s
⊢ m₁ ≤ sInf (Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s})
have pos : ∀ (j : ι) (hj₁ : j ∈ Set.Icc n m₂) (hj₂ : u j ω ∈ s), m₁ ≤ sInf (Set.Icc n m₂ ∩ {i : ι | u i ω ∈ 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 m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j ∈ Set.Icc n m₁, u j ω ∈ s
j : ι
hj₁ : j ∈ Set.Icc n m₂
hj₂ : u j ω ∈ s
⊢ m₁ ≤ sInf (Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s})
have pos : ∀ b ∈ Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s}, m₁ ≤ b
Tactic: refine le_csInf ⟨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₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j ∈ Set.Icc n m₁, u j ω ∈ s
j : ι
hj₁ : j ∈ Set.Icc n m₂
hj₂ : u j ω ∈ s
⊢ ∀ b ∈ Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s}, m₁ ≤ b
have pos : ∀ (i : ι) (hi₁ : i ∈ Set.Icc n m₂ ∩ {i : ι | u i ω ∈ s}) (hi₂ : i < m₁), False
Tactic: by_contra! ⟨i, 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 n n' : ι
hnn' : n ≤ n'
ω : Ω
⊢ LE.le.{u_3} (α := (fun (a : Ω) ↦ ι) ω) ((fun (x : ι) ↦ hittingBtwn u s x m) n ω)
    ((fun (x : ι) ↦ hittingBtwn u s x m) n' ω)
have simp : (if ∃ j ∈ Set.Icc n m, u j ω ∈ s then sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) else m) ≤
  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 β
m n n' : ι
hnn' : n ≤ n'
ω : Ω
⊢ (if ∃ j ∈ Set.Icc n m, u j ω ∈ s then sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) else m) ≤
    if ∃ j ∈ Set.Icc n' m, u j ω ∈ s then sInf (Set.Icc n' m ∩ {i : ι | u i ω ∈ s}) else m
have pos : ∀ (h_n : ∃ j ∈ Set.Icc n m, u j ω ∈ s) (h_n' : ∃ j ∈ Set.Icc n' m, u j ω ∈ s),
  sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ≤ sInf (Set.Icc n' m ∩ {i : ι | u i ω ∈ s})
Tactic: split_ifs with h_n h_n' h_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 β
m n n' : ι
hnn' : n ≤ n'
ω : Ω
pos :
  ∀ (h_n : ∃ j ∈ Set.Icc n m, u j ω ∈ s) (h_n' : ∃ j ∈ Set.Icc n' m, u j ω ∈ 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) ≤
    if ∃ j ∈ Set.Icc n' m, u j ω ∈ s then sInf (Set.Icc n' m ∩ {i : ι | u i ω ∈ s}) else m
have neg : ∀ (h_n : ∃ j ∈ Set.Icc n m, u j ω ∈ s) (h_n' : ¬∃ j ∈ Set.Icc n' m, u j ω ∈ s),
  sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ≤ m
Tactic: split_ifs with h_n h_n' h_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 β
m n n' : ι
hnn' : n ≤ n'
ω : Ω
pos :
  ∀ (h_n : ∃ j ∈ Set.Icc n m, u j ω ∈ s) (h_n' : ∃ j ∈ Set.Icc n' m, u j ω ∈ s),
    sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ≤ sInf (Set.Icc n' m ∩ {i : ι | u i ω ∈ s})
neg :
  ∀ (h_n : ∃ j ∈ Set.Icc n m, u j ω ∈ s) (h_n' : ¬∃ 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) ≤
    if ∃ j ∈ Set.Icc n' m, u j ω ∈ s then sInf (Set.Icc n' m ∩ {i : ι | u i ω ∈ s}) else m
have pos₁ : ∀ (h_n : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s) (h_n' : ∃ j ∈ Set.Icc n' m, u j ω ∈ s),
  m ≤ sInf (Set.Icc n' m ∩ {i : ι | u i ω ∈ s})
Tactic: split_ifs with h_n h_n' h_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 β
m n n' : ι
hnn' : n ≤ n'
ω : Ω
pos :
  ∀ (h_n : ∃ j ∈ Set.Icc n m, u j ω ∈ s) (h_n' : ∃ j ∈ Set.Icc n' m, u j ω ∈ s),
    sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ≤ sInf (Set.Icc n' m ∩ {i : ι | u i ω ∈ s})
neg :
  ∀ (h_n : ∃ j ∈ Set.Icc n m, u j ω ∈ s) (h_n' : ¬∃ j ∈ Set.Icc n' m, u j ω ∈ s),
    sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ≤ m
pos₁ :
  ∀ (h_n : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s) (h_n' : ∃ j ∈ Set.Icc n' m, u j ω ∈ s),
    m ≤ 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) ≤
    if ∃ j ∈ Set.Icc n' m, u j ω ∈ s then sInf (Set.Icc n' m ∩ {i : ι | u i ω ∈ s}) else m
have neg₁ : ∀ (h_n : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s) (h_n' : ¬∃ j ∈ Set.Icc n' m, u j ω ∈ s), m ≤ m
Tactic: split_ifs with h_n h_n' h_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 β
m n n' : ι
hnn' : n ≤ n'
ω : Ω
h_n : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h_n' : ∃ j ∈ Set.Icc n' m, u j ω ∈ s
⊢ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ≤ sInf (Set.Icc n' m ∩ {i : ι | u i ω ∈ s})
have pos : 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 β
m n n' : ι
hnn' : n ≤ n'
ω : Ω
h_n : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h_n' : ∃ j ∈ Set.Icc n' m, u j ω ∈ s
⊢ 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 (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
m n n' : ι
hnn' : n ≤ n'
ω : Ω
h_n : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h_n' : ¬∃ j ∈ Set.Icc n' m, u j ω ∈ s
⊢ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ≤ m
have neg : ∀ (t : ι) (ht : t ∈ Set.Icc n m ∧ u t ω ∈ s), sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ≤ m
Tactic: obtain ⟨t, ht⟩ := h_n
Cleared hypotheses: h_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 β
m n n' : ι
hnn' : n ≤ n'
ω : Ω
h_n' : ¬∃ j ∈ Set.Icc n' m, u j ω ∈ s
t : ι
ht : t ∈ Set.Icc n m ∧ u t ω ∈ s
⊢ 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 (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
m n n' : ι
hnn' : n ≤ n'
ω : Ω
h_n : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
h_n' : ∃ j ∈ Set.Icc n' m, u j ω ∈ s
⊢ m ≤ sInf (Set.Icc n' m ∩ {i : ι | u i ω ∈ s})
have pos : ∀ (t : ι) (ht : t ∈ Set.Icc n' m ∧ u t ω ∈ s), m ≤ sInf (Set.Icc n' m ∩ {i : ι | u i ω ∈ s})
Tactic: have ⟨t, ht⟩ := h_n'