mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: case refine_1
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
x✝ : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
⊢ ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b

pp: case refine_2
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b
⊢ ⨆ y ∈ Y, f a y = f a b

pp: case refine_3
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b
⊢ ⨅ x ∈ X, f x b = f a b

Tactic:
· exact le_trans (le_of_eq h) (le_of_eq h'.symm)

Goal state after:
case refine_2
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b
⊢ ⨆ y ∈ Y, f a y = f a b

case refine_3
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b
⊢ ⨅ x ∈ X, f x b = f a b
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : IsSaddlePointOn X Y f a b
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y = f a b ∧ ⨆ y ∈ Y, ⨅ x ∈ X, f x y = f a b

Tactic:
isSaddlePointOn_iff ha hb

Goal state after:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y = f a b ∧ ⨆ y ∈ Y, ⨅ x ∈ X, f x y = f a b
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: case a
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ∀ i ∈ X, f i b ≤ ⨆ y ∈ Y, f i y

Tactic:
intro x

Goal state after:
case a
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
x : E
⊢ x ∈ X → f x b ≤ ⨆ y ∈ Y, f x y
Module: Mathlib.Order.PrimeSeparator

Goal state before:
pp: case h
α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ⊆ J ∧ Disjoint (↑F) J}
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ⊆ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := Jidl.toIdeal
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : ↑J₁ ≠ Jset
J₂J : ↑J₂ ≠ Jset
J₁S : ↑J₁ ∉ S
J₂S : ↑J₂ ∉ S
J₁F : ¬Disjoint ↑F ↑J₁
J₂F : ¬Disjoint ↑F ↑J₂
c₁ : α
c₁F : c₁ ∈ ↑F
c₁J₁ : c₁ ∈ ↑J₁
c₂ : α
c₂F : c₂ ∈ ↑F
c₂J₂ : c₂ ∈ ↑J₂
b₁ : α
b₁J : b₁ ∈ J
cba₁ : c₁ ≤ b₁ ⊔ a₁
b₂ : α
b₂J : b₂ ∈ J
cba₂ : c₂ ≤ b₂ ⊔ a₂
b : α := b₁ ⊔ b₂
bJ : b ∈ J
⊢ a₁ ⊓ a₂ ∉ J

Tactic:
have ineq : c₁ ⊓ c₂ ≤ b ⊔ (a₁ ⊓ a₂) :=
  calc
    c₁ ⊓ c₂ ≤ (b₁ ⊔ a₁) ⊓ (b₂ ⊔ a₂) := inf_le_inf cba₁ cba₂
    _       ≤ (b ⊔ a₁) ⊓ (b ⊔ a₂) := by gcongr; exacts [le_sup_left, le_sup_right]
    _       = b ⊔ (a₁ ⊓ a₂) := (sup_inf_left b a₁ a₂).symm

Goal state after:
case h
α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ⊆ J ∧ Disjoint (↑F) J}
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ⊆ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := Jidl.toIdeal
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : ↑J₁ ≠ Jset
J₂J : ↑J₂ ≠ Jset
J₁S : ↑J₁ ∉ S
J₂S : ↑J₂ ∉ S
J₁F : ¬Disjoint ↑F ↑J₁
J₂F : ¬Disjoint ↑F ↑J₂
c₁ : α
c₁F : c₁ ∈ ↑F
c₁J₁ : c₁ ∈ ↑J₁
c₂ : α
c₂F : c₂ ∈ ↑F
c₂J₂ : c₂ ∈ ↑J₂
b₁ : α
b₁J : b₁ ∈ J
cba₁ : c₁ ≤ b₁ ⊔ a₁
b₂ : α
b₂J : b₂ ∈ J
cba₂ : c₂ ≤ b₂ ⊔ a₂
b : α := b₁ ⊔ b₂
bJ : b ∈ J
ineq : c₁ ⊓ c₂ ≤ b ⊔ a₁ ⊓ a₂
⊢ a₁ ⊓ a₂ ∉ J
Module: Mathlib.Order.ScottContinuity.Prod

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
α' : Type u_4
β' : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder α'
inst✝ : Preorder β'
f : α → α'
g : β → β'
hf : ScottContinuous f
hg : ScottContinuous g
b : β
d : Set α
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
c : α
hdc : IsLUB d c
e2 : (fun a ↦ (f a, g b)) '' d = (f '' d) ×ˢ {g b}
⊢ IsLUB ((fun a ↦ (f a, g b)) '' d) (f c, g b)

Tactic:
e2

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
α' : Type u_4
β' : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder α'
inst✝ : Preorder β'
f : α → α'
g : β → β'
hf : ScottContinuous f
hg : ScottContinuous g
b : β
d : Set α
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
c : α
hdc : IsLUB d c
e2 : (fun a ↦ (f a, g b)) '' d = (f '' d) ×ˢ {g b}
⊢ IsLUB ((f '' d) ×ˢ {g b}) (f c, g b)
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
a : ↑t
h : Disjoint a a
ha : a ∈ ↑t₁
hb : a ∈ ↑t₂
⊢ False

Tactic:
disjoint_self

Goal state after:
t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
a : ↑t
h : a = ⊥
ha : a ∈ ↑t₁
hb : a ∈ ↑t₂
⊢ False
Module: Mathlib.Probability.Martingale.Centering

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
⊢ (fun n ↦ f n - ∑ i ∈ Finset.range n, μ[f (i + 1) - f i | ↑ℱ i]) = fun n ↦
    f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i - μ[f (i + 1) - f i | ↑ℱ i])

Tactic:
ext1 n

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
n : ℕ
⊢ f n - ∑ i ∈ Finset.range n, μ[f (i + 1) - f i | ↑ℱ i] =
    f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i - μ[f (i + 1) - f i | ↑ℱ i])
Module: Mathlib.Probability.Martingale.Basic

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
inst✝¹ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
inst✝ : SigmaFiniteFiltration μ ℱ
f : ι → Ω → ℝ
hadp : StronglyAdapted ℱ f
hint : ∀ (i : ι), Integrable (f i) μ
hf : ∀ (i j : ι), i ≤ j → ∀ (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ
⊢ Submartingale f ℱ μ

Tactic:
refine ⟨hadp, fun i j hij => ?_, hint⟩
  suffices f i ≤ᵐ[μ.trim (ℱ.le i)] μ[f j | ℱ i] by exact ae_le_of_ae_le_trim this
  suffices 0 ≤ᵐ[μ.trim (ℱ.le i)] μ[f j | ℱ i] - f i by
    filter_upwards [this] with x hx
    rwa [← sub_nonneg]
  refine ae_nonneg_of_forall_setIntegral_nonneg
    ((integrable_condExp.sub (hint i)).trim _ (stronglyMeasurable_condExp.sub <| hadp i))
      fun s hs _ => ?_
  specialize hf i j hij s hs
  rwa [← setIntegral_trim _ (stronglyMeasurable_condExp.sub <| hadp i) hs,
    integral_sub' integrable_condExp.integrableOn (hint i).integrableOn, sub_nonneg,
    setIntegral_condExp (ℱ.le i) (hint j) hs]

Goal state after:
Module: Mathlib.Probability.Martingale.Centering

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
hf : StronglyAdapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
h_eq_sum :
  μ[martingalePart f ℱ μ j | ↑ℱ i] =ᵐ[μ]
    f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i])
h_ge : ∀ (k : ℕ), i ≤ k → μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] =ᵐ[μ] 0
h_lt :
  ∀ k < i,
    μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] =ᵐ[μ] f (k + 1) - f k - μ[f (k + 1) - f k | ↑ℱ k]
⊢ ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i]) =ᵐ[μ]
    ∑ i ∈ Finset.range i, (f (i + 1) - f i - μ[f (i + 1) - f i | ↑ℱ i])

Tactic:
← Finset.sum_range_add_sum_Ico _ hij,

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
hf : StronglyAdapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
h_eq_sum :
  μ[martingalePart f ℱ μ j | ↑ℱ i] =ᵐ[μ]
    f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i])
h_ge : ∀ (k : ℕ), i ≤ k → μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] =ᵐ[μ] 0
h_lt :
  ∀ k < i,
    μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] =ᵐ[μ] f (k + 1) - f k - μ[f (k + 1) - f k | ↑ℱ k]
⊢ ∑ k ∈ Finset.range i, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i]) +
      ∑ k ∈ Finset.Ico i j, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i]) =ᵐ[μ]
    ∑ i ∈ Finset.range i, (f (i + 1) - f i - μ[f (i + 1) - f i | ↑ℱ i])
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : 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

Tactic:
simp_rw [hittingBtwn, if_neg h] at hl
    exact False.elim (hl.ne rfl)

Goal state after:
Module: Mathlib.Probability.Martingale.OptionalStopping

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
⊢ ∀ (ω : Ω),
    (↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω) → ↑ε ≤ stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) ω

Tactic:
intro x

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
x : Ω
⊢ (↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k x) → ↑ε ≤ stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) x
Module: Mathlib.Probability.Martingale.OptionalStopping

Goal state before:
pp: case e'_3
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
ω : Ω
⊢ ω ∈ Set.univ ↔ ω ∈ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω} ∪ {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε}

Tactic:
change _ ↔ (ε : ℝ) ≤ _ ∨ _ < (ε : ℝ)

Goal state after:
case e'_3
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
ω : Ω
⊢ ω ∈ Set.univ ↔ (↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω) ∨ ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : Nonempty ι
τ : Ω → WithTop ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
⊢ IsStronglyProgressive f fun i ω ↦ (min (↑i) (τ ω)).untopA

Tactic:
by
  refine fun i ↦ (Measurable.untopA ?_).stronglyMeasurable
  let m_prod : MeasurableSpace (Set.Iic i × Ω) := Subtype.instMeasurableSpace.prod (f i)
  let m_set : ∀ t : Set (Set.Iic i × Ω), MeasurableSpace t := fun _ =>
    @Subtype.instMeasurableSpace (Set.Iic i × Ω) _ m_prod
  let s := {p : Set.Iic i × Ω | τ p.2 ≤ i}
  have hs : MeasurableSet[m_prod] s := @measurable_snd (Set.Iic i) Ω _ (f i) _ (hτ i)
  have h_meas_fst : ∀ t : Set (Set.Iic i × Ω),
      Measurable[m_set t] fun x : t => ((x : Set.Iic i × Ω).fst : ι) :=
    fun t => (@measurable_subtype_coe (Set.Iic i × Ω) m_prod _).fst.subtype_val
  refine measurable_of_restrict_of_restrict_compl hs ?_ ?_
  · refine Measurable.min (h_meas_fst s).withTop_coe ?_
    refine measurable_of_Iic fun j ↦ ?_
    cases j with
    | top => simp
    | coe j =>
      have h_set_eq : (fun x : s => τ (x : Set.Iic i × Ω).snd) ⁻¹' Set.Iic j =
          (fun x : s => (x : Set.Iic i × Ω).snd) ⁻¹' {ω | τ ω ≤ min i j} := by
        ext1 ω
        simp only [Set.mem_preimage, Set.mem_Iic, coe_min, le_inf_iff,
          Set.preimage_ofPred_eq, Set.mem_ofPred_eq, iff_and_self]
        exact fun _ => ω.prop
      rw [h_set_eq]
      suffices h_meas : @Measurable _ _ (m_set s) (f i) fun x : s ↦ (x : Set.Iic i × Ω).snd from
        h_meas (f.mono (min_le_left _ _) _ (hτ.measurableSet_le (min i j)))
      exact measurable_snd.comp (@measurable_subtype_coe _ m_prod _)
  · let sc := sᶜ
    suffices h_min_eq_left :
      (fun x : sc => min (↑(x : Set.Iic i × Ω).fst) (τ (x : Set.Iic i × Ω).snd)) = fun x : sc =>
        ↑(x : Set.Iic i × Ω).fst by
      simp +unfoldPartialApp only [sc, Set.domRestrict, h_min_eq_left]
      exact (h_meas_fst _).withTop_coe
    ext1 ω
    rw [min_eq_left]
    have hx_fst_le : ↑(ω : Set.Iic i × Ω).fst ≤ i := (ω : Set.Iic i × Ω).fst.prop
    by_cases h : τ (ω : Set.Iic i × Ω).2 = ⊤
    · simp [h]
    · lift τ (ω : Set.Iic i × Ω).2 to ι using h with t ht
      norm_cast
      refine hx_fst_le.trans (le_of_lt ?_)
      convert! ω.prop
      simp only [sc, s, not_le, Set.mem_compl_iff, Set.mem_ofPred_eq, ← ht]
      norm_cast

Goal state after:
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
inst✝¹ : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝ : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' ↑s
y : Ω
this : {i ∈ s | y ∈ {ω | τ ω = ↑i}} = {(τ y).untopA}
⊢ u (τ y).untopA y = ∑ i ∈ s with y ∈ {ω | τ ω = ↑i}, u i y

Tactic:
rw [this, Finset.sum_singleton]

Goal state after:
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst✝ : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ ↑N
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
⊢ stoppedValue u π - stoppedValue u τ = fun ω ↦
    (∑ i ∈ Finset.range (N + 1), {ω | τ ω ≤ ↑i ∧ ↑i < π ω}.indicator (u (i + 1) - u i)) ω

Tactic:
rw [stoppedValue_sub_eq_sum hle]

Goal state after:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst✝ : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ ↑N
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
⊢ (fun ω ↦ (∑ i ∈ Finset.Ico (untopA (τ ω)) (untopA (π ω)), (u (i + 1) - u i)) ω) = fun ω ↦
    (∑ i ∈ Finset.range (N + 1), {ω | τ ω ≤ ↑i ∧ ↑i < π ω}.indicator (u (i + 1) - u i)) ω

Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst✝ : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ ↑N
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
⊢ ∀ (ω : Ω), ↑(π ω) ≠ ∞
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: μ : Measure ℝ
t : ℝ
⊢ complexMGF id μ (↑t * I) = charFun μ t

Tactic:
simp only [complexMGF, id_eq, charFun, RCLike.inner_apply, conj_trivial, ofReal_mul]

Goal state after:
μ : Measure ℝ
t : ℝ
⊢ ∫ (ω : ℝ), cexp (↑t * I * ↑ω) ∂μ = ∫ (x : ℝ), cexp (↑t * ↑x * I) ∂μ
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: case e'_6
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ interior (integrableExpSet X μ) = Set.univ

Tactic:
interior_eq_univ

Goal state after:
case e'_6
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ integrableExpSet X μ = Set.univ
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: case pos
μ : ℝ
v : ℝ≥0
y : ℝ
hv : v = 0
⊢ Measure.map (fun x ↦ x + y) (gaussianReal μ v) = gaussianReal (μ + y) v

pp: case neg
μ : ℝ
v : ℝ≥0
y : ℝ
hv : ¬v = 0
⊢ Measure.map (fun x ↦ x + y) (gaussianReal μ v) = gaussianReal (μ + y) v

Tactic:
· simp [hv, gaussianReal_zero_var]

Goal state after:
case neg
μ : ℝ
v : ℝ≥0
y : ℝ
hv : ¬v = 0
⊢ Measure.map (fun x ↦ x + y) (gaussianReal μ v) = gaussianReal (μ + y) v
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst✝ : IsProbabilityMeasure μ
hXY : mgf X μ = mgf Y μ'
this : mgf Y μ' 0 ≠ 0
⊢ ¬μ' = 0

Tactic:
by
    intro h_contra
    simp [h_contra] at this

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
⊢ ∫ (x : ℝ), ↑(gaussianPDFReal μ v x) * cexp (z * ↑x) =
    ↑(√(2 * π * ↑v))⁻¹ * ∫ (x : ℝ), cexp (-↑↑(2 * v)⁻¹ * ↑x ^ 2 + (z + ↑μ / ↑↑v) * ↑x + -↑μ ^ 2 / (2 * ↑↑v))

Tactic:
by
      unfold gaussianPDFReal
      push_cast
      simp_rw [mul_assoc, integral_const_mul, ← Complex.exp_add]
      congr with x
      congr 1
      ring

Goal state after:
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: case e_a.hf
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_int : Integrable (fun ω ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
⊢ Integrable (fun ω ↦ X ω ^ 2 * rexp (v * X ω) - 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ

pp: case e_a.hg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_int : Integrable (fun ω ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
⊢ Integrable (fun ω ↦ deriv (cgf X μ) v ^ 2 * rexp (v * X ω)) μ

pp: case e_a
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_int : Integrable (fun ω ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
⊢ ∫ (ω : Ω), X ω ^ 2 * rexp (v * X ω) ∂μ - (2 * ∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
      deriv (cgf X μ) v ^ 2 * mgf X μ v =
    ∫ (a : Ω), X a ^ 2 * rexp (v * X a) - 2 * X a * deriv (cgf X μ) v * rexp (v * X a) ∂μ +
      ∫ (a : Ω), deriv (cgf X μ) v ^ 2 * rexp (v * X a) ∂μ

Tactic:
· exact (integrable_pow_mul_exp_of_mem_interior_integrableExpSet h 2).sub h_int

Goal state after:
case e_a.hg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_int : Integrable (fun ω ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
⊢ Integrable (fun ω ↦ deriv (cgf X μ) v ^ 2 * rexp (v * X ω)) μ

case e_a
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_int : Integrable (fun ω ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
⊢ ∫ (ω : Ω), X ω ^ 2 * rexp (v * X ω) ∂μ - (2 * ∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
      deriv (cgf X μ) v ^ 2 * mgf X μ v =
    ∫ (a : Ω), X a ^ 2 * rexp (v * X a) - 2 * X a * deriv (cgf X μ) v * rexp (v * X a) ∂μ +
      ∫ (a : Ω), deriv (cgf X μ) v ^ 2 * rexp (v * X a) ∂μ
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: m : ℝ
v : ℝ≥0
L : StrongDual ℝ ℝ
⊢ Measure.map (⇑L) (gaussianReal m v) =
    gaussianReal (∫ (x : ℝ), L x ∂gaussianReal m v) Var[⇑L; gaussianReal m v].toNNReal

Tactic:
gaussianReal_map_continuousLinearMap

Goal state after:
m : ℝ
v : ℝ≥0
L : StrongDual ℝ ℝ
⊢ gaussianReal (L m) ((L 1 ^ 2).toNNReal * v) =
    gaussianReal (∫ (x : ℝ), L x ∂gaussianReal m v) Var[⇑L; gaussianReal m v].toNNReal
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
μ : Measure E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
⊢ ∫ (z : F),
      ⟪u, z - ∫ (x : F), id x ∂Measure.map (⇑L) μ⟫ * ⟪v, z - ∫ (x : F), id x ∂Measure.map (⇑L) μ⟫ ∂Measure.map (⇑L) μ =
    ((covarianceBilin μ) ((ContinuousLinearMap.adjoint L) u)) ((ContinuousLinearMap.adjoint L) v)

pp: case h
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
μ : Measure E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
⊢ MemLp id 2 (Measure.map (⇑L) μ)

Tactic:
covarianceBilin_apply h

Goal state after:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
μ : Measure E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
⊢ ∫ (z : F),
      ⟪u, z - ∫ (x : F), id x ∂Measure.map (⇑L) μ⟫ * ⟪v, z - ∫ (x : F), id x ∂Measure.map (⇑L) μ⟫ ∂Measure.map (⇑L) μ =
    ∫ (z : E),
      ⟪(ContinuousLinearMap.adjoint L) u, z - ∫ (x : E), id x ∂μ⟫ *
        ⟪(ContinuousLinearMap.adjoint L) v, z - ∫ (x : E), id x ∂μ⟫ ∂μ

case h
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
μ : Measure E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
⊢ MemLp id 2 (Measure.map (⇑L) μ)
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ Var[fun x ↦ x; gaussianReal μ v] = ↑v

Tactic:
rw [variance_eq_integral measurable_id'.aemeasurable]
  simp only [integral_id_gaussianReal]
  calc ∫ ω, (ω - μ) ^ 2 ∂gaussianReal μ v
  _ = ∫ ω, ω ^ 2 ∂(gaussianReal μ v).map (fun x ↦ x - μ) := by
    rw [integral_map (by fun_prop) (by fun_prop)]
  _ = ∫ ω, ω ^ 2 ∂(gaussianReal 0 v) := by simp [gaussianReal_map_sub_const]
  _ = iteratedDeriv 2 (mgf (fun x ↦ x) (gaussianReal 0 v)) 0 := by
    rw [iteratedDeriv_mgf_zero] <;> simp
  _ = v := by
    rw [mgf_fun_id_gaussianReal, iteratedDeriv_succ, iteratedDeriv_one]
    simp only [zero_mul, zero_add]
    have : deriv (fun t ↦ rexp (v * t ^ 2 / 2)) = fun t ↦ v * t * rexp (v * t ^ 2 / 2) := by
      ext t
      rw [_root_.deriv_exp (by fun_prop)]
      simp only [deriv_div_const, differentiableAt_const, differentiableAt_fun_id, Nat.cast_ofNat,
        DifferentiableAt.fun_pow, deriv_fun_mul, deriv_const', zero_mul, deriv_fun_pow,
        Nat.add_one_sub_one, pow_one, deriv_id'', mul_one, zero_add]
      ring
    rw [this, deriv_fun_mul (by fun_prop) (by fun_prop), deriv_fun_mul (by fun_prop) (by fun_prop)]
    simp

Goal state after: