awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
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 : 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

Tactic:
exact (Finset.measurable_restrict _).comp_aemeasurable hX

Premises used: Finset.measurable_restrict, Measurable.comp_aemeasurable
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
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 : 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

Tactic:
(Finset.measurable_restrict _).comp_aemeasurable hY

Premises used: Finset.measurable_restrict, Finset.restrict, Measurable.comp_aemeasurable
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
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 : 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

Tactic:
exact (Finset.measurable_restrict _).comp_aemeasurable hY

Premises used: Finset.measurable_restrict, Measurable.comp_aemeasurable
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
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 : 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)

Tactic:
(map_eq_iff_forall_finset_map_restrict_eq hX hY).mp h.map_eq I

Premises used: ProbabilityTheory.map_eq_iff_forall_finset_map_restrict_eq, Iff.mp, ProbabilityTheory.IdentDistrib.map_eq
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
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 : 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)

Tactic:
exact (map_eq_iff_forall_finset_map_restrict_eq hX hY).mp h.map_eq I

Premises used: ProbabilityTheory.map_eq_iff_forall_finset_map_restrict_eq, Iff.mp, ProbabilityTheory.IdentDistrib.map_eq
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
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 :
  ∀ (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:
(map_eq_iff_forall_finset_map_restrict_eq hX hY).mpr (fun I ↦ (h I).map_eq)

Premises used: Iff.mpr, ProbabilityTheory.map_eq_iff_forall_finset_map_restrict_eq, ProbabilityTheory.IdentDistrib.map_eq
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
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 :
  ∀ (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:
exact (map_eq_iff_forall_finset_map_restrict_eq hX hY).mpr (fun I ↦ (h I).map_eq)

Premises used: Iff.mpr, ProbabilityTheory.map_eq_iff_forall_finset_map_restrict_eq, ProbabilityTheory.IdentDistrib.map_eq
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
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
rw : ∀ (i : ↥I), ∀ᵐ (a : Ω) ∂P, Eq (α := 𝓧 (↑i : T)) (X (↑i : T) a) (Y (↑i : T) a)
⊢ ∀ᵐ (ω : Ω) ∂P, ∀ (i : ↥I), Eq (α := 𝓧 (↑i : T)) (X (↑i : T) ω) (Y (↑i : T) ω)

Tactic:
rw [MeasureTheory.ae_all_iff]

Premises used: MeasureTheory.ae_all_iff
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
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
⊢ ∀ (i : ↥I), ∀ᵐ (a : Ω) ∂P, Eq (α := 𝓧 (↑i : T)) (X (↑i : T) a) (Y (↑i : T) a)

Tactic:
fun i ↦ h i

Premises used: Filter.EventuallyEq, Subtype.val
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
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
⊢ ∀ (i : ↥I), ∀ᵐ (a : Ω) ∂P, Eq (α := 𝓧 (↑i : T)) (X (↑i : T) a) (Y (↑i : T) a)

Tactic:
exact fun i ↦ h i
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
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) ω)

Tactic:
have h' : ∀ᵐ ω ∂P, ∀ (i : I), X i ω = Y i ω := by
    rw [MeasureTheory.ae_all_iff]
    exact fun i ↦ h i
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
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)

Tactic:
Measure.map_congr ?_

Premises used: MeasureTheory.Measure.map_congr
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
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) ω)
refine :
  (ae P).EventuallyEq (β := (i : ↥I) → 𝓧 (↑i : T)) (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) fun (ω : Ω) ↦
    I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω
⊢ 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:
refine Measure.map_congr ?_

Premises used: MeasureTheory.Measure.map_congr
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
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_1 : ∀ (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 : ∀ (i : ↥I), Eq (α := 𝓧 (↑i : T)) (X (↑i : T) ω) (Y (↑i : T) ω)
⊢ Eq (α := (i : ↥I) → 𝓧 (↑i : T)) (I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) (I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω)

Tactic:
funext h

Premises used: funext
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
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
h₂ h₃ :
  ∀ (ω : Ω) (h : ∀ (i : ↥I), Eq (α := 𝓧 (↑i : T)) (X (↑i : T) ω) (Y (↑i : T) ω)),
    Eq (α := (i : ↥I) → 𝓧 (↑i : T)) (I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) (I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω)
⊢ (ae P).EventuallyEq (β := (i : ↥I) → 𝓧 (↑i : T)) (fun (ω : Ω) ↦ I.restrict (π := 𝓧) fun (x : T) ↦ X x ω) fun (ω : Ω) ↦
    I.restrict (π := 𝓧) fun (x : T) ↦ Y x ω

Tactic:
filter_upwards [h'] with ω h using funext h

Premises used: funext
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
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
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)
⊢ Eq (α := Measure ((x : T) → 𝓧 x)) (Measure.map (fun (ω : Ω) (x : T) ↦ X x ω) P)
    (Measure.map (fun (ω : Ω) (x : T) ↦ Y x ω) P)

Tactic:
rw [map_eq_iff_forall_finset_map_restrict_eq hX hY]

Premises used: ProbabilityTheory.map_eq_iff_forall_finset_map_restrict_eq
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
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
⊢ ∀ (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:
fun I ↦ map_restrict_eq_of_forall_ae_eq h I

Premises used: ProbabilityTheory.map_restrict_eq_of_forall_ae_eq
-- Module: Mathlib.Probability.Process.FiniteDimensionalLaws
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
⊢ ∀ (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:
exact fun I ↦ map_restrict_eq_of_forall_ae_eq h I

Premises used: ProbabilityTheory.map_restrict_eq_of_forall_ae_eq
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Preorder ι
inst_1 : InfSet ι
u : ι → Ω → β
s : Set β
n m : ι
⊢ hittingBtwn u s n m = fun (x : Ω) ↦
    if ∃ j ∈ Set.Icc n m, u j x ∈ s then sInf (Set.Icc n m ∩ {i : ι | u i x ∈ s}) else m

Tactic:
rfl

Premises used: MeasureTheory.hittingBtwn, rfl
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Preorder ι
inst_1 : InfSet ι
u : ι → Ω → β
s : Set β
n : ι
⊢ hittingAfter u s n = fun (x : Ω) ↦
    if ∃ (j : ι), n ≤ j ∧ u j x ∈ s then (↑(sInf {i : ι | n ≤ i ∧ u i x ∈ s}) : WithTop ι) else ⊤

Tactic:
rfl

Premises used: MeasureTheory.hittingAfter, rfl
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Preorder ι
inst_1 : InfSet ι
u : ι → Ω → β
n m : ι
h : ∀ (x : Ω), hittingBtwn u ∅ n m x = m
⊢ hittingBtwn u ∅ n m = fun (x : Ω) ↦ m

Tactic:
ext
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Preorder ι
inst_1 : InfSet ι
u : ι → Ω → β
n m : ι
x : Ω
⊢ hittingBtwn u ∅ n m x = m

Tactic:
simp [hittingBtwn]

Premises used: MeasureTheory.hittingBtwn
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Preorder ι
inst_1 : InfSet ι
u : ι → Ω → β
n : ι
h : ∀ (x : Ω), hittingAfter u ∅ n x = ⊤
⊢ hittingAfter u ∅ n = fun (x : Ω) ↦ ⊤

Tactic:
ext
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Preorder ι
inst_1 : InfSet ι
u : ι → Ω → β
n : ι
x : Ω
⊢ hittingAfter u ∅ n x = ⊤

Tactic:
simp [hittingAfter]

Premises used: MeasureTheory.hittingAfter
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
h : ∀ (ω : Ω), hittingBtwn u Set.univ n m ω = min n m
⊢ hittingBtwn u Set.univ n m = fun (x : Ω) ↦ min n m

Tactic:
ext ω
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
ω : Ω
h : (if ∃ (j : ι), n ≤ j ∧ j ≤ m then sInf (Set.Icc n m) else m) = min n m
⊢ hittingBtwn u Set.univ n m ω = min n m

Tactic:
simp only [hittingBtwn_def, Set.mem_Icc, Set.mem_univ, and_true, Set.setOf_true, Set.inter_univ]

Premises used: and_true, Set.inter_univ, Set.mem_univ, Set.mem_Icc, Set.setOf_true, MeasureTheory.hittingBtwn_def
-- Module: Mathlib.Probability.Process.HittingTime
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
neg : ∀ (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

Tactic:
by_cases hnm : n ≤ m
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
ω : Ω
hnm : n ≤ m
pos : (∀ (x : ι), n ≤ x → m < x) → m = n
⊢ (if ∃ (j : ι), n ≤ j ∧ j ≤ m then sInf (Set.Icc n m) else m) = min n m

Tactic:
simp [hnm]
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
ω : Ω
hnm : ¬n ≤ m
neg : (if ∃ (j : ι), n ≤ j ∧ j ≤ m then sInf ∅ else m) = min n m
⊢ (if ∃ (j : ι), n ≤ j ∧ j ≤ m then sInf (Set.Icc n m) else m) = min n m

Tactic:
simp [hnm]
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
ω : Ω
hnm : n ≤ m
⊢ (∀ (x : ι), n ≤ x → m < x) → m = n

Tactic:
grind
-- Module: Mathlib.Probability.Process.HittingTime
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 ∅ else m) = min n m

Tactic:
grind
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
ω : Ω
h : (if ∃ (j : ι), n ≤ j ∧ j ≤ m then sInf (Set.Icc n m) else m) = min n m
⊢ hittingBtwn u Set.univ n 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

Premises used: and_true, Set.inter_univ, Set.mem_univ, Set.mem_Icc, Set.setOf_true, MeasureTheory.hittingBtwn_def
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLattice ι
u : ι → Ω → β
n : ι
h : ∀ (ω : Ω), hittingAfter u Set.univ n ω = (↑n : WithTop ι)
⊢ hittingAfter u Set.univ n = fun (x : Ω) ↦ (↑n : WithTop ι)

Tactic:
ext ω
-- Module: Mathlib.Probability.Process.HittingTime
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 ι)

Tactic:
simp only [hittingAfter_def, Set.mem_univ, and_true]

Premises used: and_true, MeasureTheory.hittingAfter_def, Set.mem_univ
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLattice ι
u : ι → Ω → β
n : ι
ω : Ω
h : (↑(sInf {j : ι | n ≤ j}) : WithTop ι) = (↑n : WithTop ι)
⊢ (if ∃ (j : ι), n ≤ j then (↑(sInf {j : ι | n ≤ j}) : WithTop ι) else ⊤) = (↑n : WithTop ι)

Tactic:
rw [if_pos ⟨n, le_rfl⟩]

Premises used: if_pos
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLattice ι
u : ι → Ω → β
n : ι
ω : Ω
⊢ (↑(sInf {j : ι | n ≤ j}) : WithTop ι) = (↑n : WithTop ι)

Tactic:
exact_mod_cast csInf_Ici

Premises used: csInf_Ici
-- Module: Mathlib.Probability.Process.HittingTime
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 ι)
h₁ : (↑(sInf {j : ι | n ≤ j}) : WithTop ι) = (↑n : WithTop ι)
⊢ hittingAfter u Set.univ n ω = (↑n : WithTop ι)

Tactic:
classical
  simp only [hittingAfter_def, Set.mem_univ, and_true]
  rw [if_pos ⟨n, le_rfl⟩]
  exact_mod_cast csInf_Ici

Premises used: and_true, MeasureTheory.hittingAfter_def, if_pos, Set.mem_univ, csInf_Ici
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m : ι
h : m < n
⊢ hittingBtwn u s n m ω = m

Tactic:
grind [hittingBtwn, not_le, Set.Icc_eq_empty]

Premises used: not_le, Set.Icc_eq_empty, MeasureTheory.hittingBtwn
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
simp : (if ∃ j ∈ Set.Icc n m, u j ω ∈ s then sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) else m) ≤ m
⊢ hittingBtwn u s n m ω ≤ m

Tactic:
simp only [hittingBtwn]

Premises used: MeasureTheory.hittingBtwn
-- Module: Mathlib.Probability.Process.HittingTime
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
neg : ∀ (h : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s), m ≤ m
⊢ (if ∃ j ∈ Set.Icc n m, u j ω ∈ s then sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) else m) ≤ m

Tactic:
split_ifs with h
-- Module: Mathlib.Probability.Process.HittingTime
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
pos : ∀ (j : ι) (hj₁ : j ∈ Set.Icc n m) (hj₂ : u j ω ∈ s), sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ≤ m
⊢ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ≤ m

Tactic:
obtain ⟨j, hj₁, hj₂⟩ := h
-- Module: Mathlib.Probability.Process.HittingTime
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
⊢ Membership.mem (γ := Set ι) {i : ι | u i ω ∈ s} j

Tactic:
change j ∈ {i | u i ω ∈ s} at hj₂
-- Module: Mathlib.Probability.Process.HittingTime
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₂ : Membership.mem (γ := Set ι) {i : ι | u i ω ∈ s} j
⊢ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ≤ m

Tactic:
(csInf_le (BddBelow.inter_of_left bddBelow_Icc) (Set.mem_inter hj₁ hj₂)).trans hj₁.2

Premises used: BddBelow.inter_of_left, Set.mem_inter, And.right, bddBelow_Icc, LE.le.trans, csInf_le
-- Module: Mathlib.Probability.Process.HittingTime
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₂ : Membership.mem (γ := Set ι) {i : ι | u i ω ∈ s} j
⊢ sInf (Set.Icc n m ∩ {i : ι | u i ω ∈ s}) ≤ m

Tactic:
exact (csInf_le (BddBelow.inter_of_left bddBelow_Icc) (Set.mem_inter hj₁ hj₂)).trans hj₁.2

Premises used: BddBelow.inter_of_left, Set.mem_inter, And.right, bddBelow_Icc, LE.le.trans, csInf_le
-- Module: Mathlib.Probability.Process.HittingTime
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
⊢ m ≤ m

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Probability.Process.HittingTime
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
⊢ m ≤ m

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.Probability.Process.HittingTime
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
⊢ ∃ 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⟩
-- Module: Mathlib.Probability.Process.HittingTime
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

Tactic:
not_le.2 hk₁ ?_

Premises used: not_le, Iff.mpr
-- Module: Mathlib.Probability.Process.HittingTime
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
refine : hittingBtwn u s n m ω ≤ k
⊢ False

Tactic:
refine not_le.2 hk₁ ?_

Premises used: not_le, Iff.mpr