mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
han : (orderOf a).Coprime n
⊢ a • approxOrderOf A n δ ⊆ approxOrderOf A (orderOf a * n) δ

Tactic:
simp_rw [approxOrderOf, thickening_eq_biUnion_ball, ← image_smul, image_iUnion₂, image_smul,
    smul_ball'', smul_eq_mul, mem_ofPred_eq]

Goal state after:
A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
han : (orderOf a).Coprime n
⊢ ⋃ i, ⋃ (_ : orderOf i = n), ball (a * i) δ ⊆ ⋃ x, ⋃ (_ : orderOf x = orderOf a * n), ball x δ
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : orderOf a ^ 2 ∣ n
⊢ a • approxOrderOf A n δ = approxOrderOf A n δ

Tactic:
simp_rw [approxOrderOf, thickening_eq_biUnion_ball, ← image_smul, image_iUnion₂, image_smul,
    smul_ball'', smul_eq_mul, mem_ofPred_eq]

Goal state after:
A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : orderOf a ^ 2 ∣ n
⊢ ⋃ i, ⋃ (_ : orderOf i = n), ball (a * i) δ = ⋃ x, ⋃ (_ : orderOf x = n), ball x δ
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this✝ : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun n ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ^ 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅ → E =ᵐ[μ] C ↑p
p : ℕ
hp : Nat.Prime p
f : 𝕊 → 𝕊 := fun y ↦ p • y
this : f '' A p ⊆ blimsup (fun n ↦ approxAddOrderOf 𝕊 n (↑p * δ n)) atTop fun n ↦ 0 < n ∧ ¬p ∣ n
⊢ A ↑⟨p, hp⟩ =ᵐ[μ] ∅ ∨ A ↑⟨p, hp⟩ =ᵐ[μ] univ

Tactic:
apply (ergodic_nsmul hp.one_lt).ae_empty_or_univ_of_image_ae_le (hA₀ p).nullMeasurableSet
      apply (LE.le.eventuallyLE this).congr EventuallyEq.rfl
      exact blimsup_thickening_mul_ae_eq μ (fun n => 0 < n ∧ p∤n) (fun n => {y | addOrderOf y = n})
        (Nat.cast_pos.mpr hp.pos) _ hδ

Goal state after:
Module: Mathlib.Order.CompleteLattice.PiLex

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → CompleteLinearOrder (α i)
inst✝ : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun i ↦ α i) i))
e : Lex ((i : ι) → (fun i ↦ α i) i)
he : e ∈ s
a : ι
ha : (∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j a → sSup s j = e j) ∧ (fun {i} x1 x2 ↦ x1 < x2) (sSup s a) (e a)
⊢ False

Tactic:
exact ha.2.not_ge (le_sSup_apply he fun j hj ↦ (ha.1 j hj).symm)

Goal state after:
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : DedekindCut α
h : a.extent ⊆ b.extent ∧ ∃ x ∈ b.extent, x ∉ a.extent
⊢ ∃ c, a < principal c ∧ principal c ≤ b

Tactic:
simpa [← not_le, principal_le_iff, and_comm] using h.2

Goal state after:
Module: Mathlib.Order.Extension.Linear

Goal state before:
pp: case refine_1
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
x : α
⊢ ∃ r ∈ c, r x x

Tactic:
exact ⟨s, hs, refl x⟩

Goal state after:
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
p : α → ι → Prop
hic : #ι < c
⊢ (∀ᶠ (x : α) in l, ∀ (i : ι), p x i) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p x i

Tactic:
simp only [Filter.Eventually, ofPred_forall]
  exact cardinal_iInter_mem hic

Goal state after:
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: case mp.superset
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
s✝ t✝ : Set α
a✝¹ : CardinalGenerateSets g s✝
a✝ : s✝ ⊆ t✝
ih : ∃ S ⊆ g, #↑S < c ∧ ⋂₀ S ⊆ s✝
⊢ ∃ S ⊆ g, #↑S < c ∧ ⋂₀ S ⊆ t✝

Tactic:
| superset _ _ ih =>

Goal state after:
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : Monotone f
i : Fin n
x : α
hx₁ : f i.castSucc ≤ x
hx₂ : x ≤ f i.succ
j : Fin (n + 1)
⊢ i.castSucc.succ.insertNth x f j.castSucc ≤ i.castSucc.succ.insertNth x f j.succ

Tactic:
obtain hj | rfl | hj := lt_trichotomy j i.castSucc

Goal state after:
case inl
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : Monotone f
i : Fin n
x : α
hx₁ : f i.castSucc ≤ x
hx₂ : x ≤ f i.succ
j : Fin (n + 1)
hj : j < i.castSucc
⊢ i.castSucc.succ.insertNth x f j.castSucc ≤ i.castSucc.succ.insertNth x f j.succ

case inr.inl
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : Monotone f
i : Fin n
x : α
hx₁ : f i.castSucc ≤ x
hx₂ : x ≤ f i.succ
⊢ i.castSucc.succ.insertNth x f i.castSucc.castSucc ≤ i.castSucc.succ.insertNth x f i.castSucc.succ

case inr.inr
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : Monotone f
i : Fin n
x : α
hx₁ : f i.castSucc ≤ x
hx₂ : x ≤ f i.succ
j : Fin (n + 1)
hj : i.castSucc < j
⊢ i.castSucc.succ.insertNth x f j.castSucc ≤ i.castSucc.succ.insertNth x f j.succ
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : ∀ (i : Fin n), f i.castSucc < f i.succ
i : Fin n
x : α
hx₁ : f i.castSucc < x
hx₂ : x < f i.succ
j : Fin (n + 1)
⊢ i.castSucc.succ.insertNth x f j.castSucc < i.castSucc.succ.insertNth x f j.succ

Tactic:
obtain hj | rfl | hj := lt_trichotomy j i.castSucc

Goal state after:
case inl
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : ∀ (i : Fin n), f i.castSucc < f i.succ
i : Fin n
x : α
hx₁ : f i.castSucc < x
hx₂ : x < f i.succ
j : Fin (n + 1)
hj : j < i.castSucc
⊢ i.castSucc.succ.insertNth x f j.castSucc < i.castSucc.succ.insertNth x f j.succ

case inr.inl
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : ∀ (i : Fin n), f i.castSucc < f i.succ
i : Fin n
x : α
hx₁ : f i.castSucc < x
hx₂ : x < f i.succ
⊢ i.castSucc.succ.insertNth x f i.castSucc.castSucc < i.castSucc.succ.insertNth x f i.castSucc.succ

case inr.inr
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : ∀ (i : Fin n), f i.castSucc < f i.succ
i : Fin n
x : α
hx₁ : f i.castSucc < x
hx₂ : x < f i.succ
j : Fin (n + 1)
hj : i.castSucc < j
⊢ i.castSucc.succ.insertNth x f j.castSucc < i.castSucc.succ.insertNth x f j.succ
Module: Mathlib.Order.Monotone.MonovaryOrder

Goal state before:
pp: case e'_2.e'_1
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
a b : ι
⊢ a = b ↔ (f a, g a, a) = (f b, g b, b)

Tactic:
simp only [Prod.ext_iff, ← and_assoc, imp_and, iff_and_self]

Goal state after:
case e'_2.e'_1
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
a b : ι
⊢ (a = b → f a = f b) ∧ (a = b → g a = g b)
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: case refine_1
α : ℕ → Type u_1
inst✝¹ : Finite (α 0)
inst✝ : ∀ (i : ℕ), Nonempty (α i)
π : {i j : ℕ} → i ≤ j → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), {b | π ⋯ b = a}.Finite
αs : Type u_1 := (i : ℕ) × α i
x✝¹ : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
i j : ℕ
b : α j
h : i ≤ j
x✝ :
  ¬⟨i, π h b⟩ = ⟨j, b⟩ ∧
    ∀ (a : ℕ) (b_1 : α a), ⟨i, π h b⟩ ≤ ⟨a, b_1⟩ → ⟨a, b_1⟩ ≤ ⟨j, b⟩ → ¬⟨a, b_1⟩ = ⟨i, π h b⟩ → ⟨a, b_1⟩ = ⟨j, b⟩
hne : ¬⟨i, π h b⟩ = ⟨j, b⟩
h' : ∀ (a : ℕ) (b_1 : α a), ⟨i, π h b⟩ ≤ ⟨a, b_1⟩ → ⟨a, b_1⟩ ≤ ⟨j, b⟩ → ¬⟨a, b_1⟩ = ⟨i, π h b⟩ → ⟨a, b_1⟩ = ⟨j, b⟩
⊢ i + 1 = j

Tactic:
have hle' : i + 1 ≤ j := h.lt_of_ne <| by rintro rfl; simp [π_refl] at hne
      exact congr_arg Sigma.fst <| h' (i + 1) (π hle' b) ⟨by simp, by rw [π_trans]⟩ ⟨hle', by simp⟩
        (fun h ↦ by simp at h)

Goal state after:
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : I.IsMaximal
⊢ I.IsPrime

Tactic:
rw [isPrime_iff_mem_or_mem]

Goal state after:
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : I.IsMaximal
⊢ ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
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
⊢ J.IsPrime

Tactic:
rw [isPrime_iff_mem_or_mem]

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
⊢ ∀ {x y : α}, x ⊓ y ∈ J → x ∈ J ∨ y ∈ J
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun f
ha : a ∈ u
⊢ f a = f b ↔ P.Rel a b

Tactic:
refine ⟨fun hab ↦ (hf.rel_apply ha).trans ?_, (hf.apply_eq_apply ·)⟩
  rw [hab, P.rel_comm]
  refine hf.rel_apply <| by_contra fun hb ↦ ?_
  rw [hf.apply_of_notMem hb] at hab
  exact hab ▸ hb <| hf.apply_mem ha

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
inst✝ : OrderBot ι
𝓕 : Filtration ι m
m' : MeasurableSpace (ι × Ω)
hm'bot : ∀ (A : Set Ω), MeasurableSet A → MeasurableSet ({⊥} ×ˢ A)
hm' : ∀ (i : ι) (A : Set Ω), MeasurableSet A → MeasurableSet (Set.Ioi i ×ˢ A)
⊢ 𝓕.predictable ≤ m'

Tactic:
refine MeasurableSpace.generateFrom_le ?_
  rintro - (⟨A, hA, rfl⟩ | ⟨i, A, hA, rfl⟩)
  · exact hm'bot A hA
  · exact hm' i A hA

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

Goal state before:
pp: Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst✝² : CompleteSpace E
inst✝¹ : Preorder E
inst✝ : AddLeftMono E
hf : Submartingale f ℱ μ
⊢ Supermartingale (-f) ℱ μ

Tactic:
refine ⟨hf.1.neg, fun i j hij => (condExp_neg ..).le.trans ?_, fun i => (hf.2.2 i).neg⟩
  filter_upwards [hf.2.1 i j hij] with _ _
  simpa

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
inst✝⁶ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : PartialOrder F
inst✝³ : IsOrderedAddMonoid F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : IsOrderedModule ℝ F
f : ι → Ω → F
c : ℝ
hc : 0 ≤ c
hf : Submartingale f ℱ μ
⊢ Submartingale (c • f) ℱ μ

Tactic:
by
  rw [← neg_neg (c • f), ← smul_neg]
  exact Supermartingale.neg (hf.neg.smul_nonneg hc)

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

Goal state before:
pp: case coe
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : ¬IsMin i
ω : Ω
t : ι
⊢ t < i ↔ t ≤ Order.pred i

Tactic:
le_pred_iff_of_not_isMin hi_min

Goal state after:
case coe
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : ¬IsMin i
ω : Ω
t : ι
⊢ t < i ↔ t < i
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
⊢ MeasurableSet {ω | τ ω < ↑i}

Tactic:
by_cases hi_min : IsMin i
  · suffices {ω : Ω | τ ω < i} = ∅ by rw [this]; exact @MeasurableSet.empty _ (f i)
    ext1 ω
    simp only [Set.mem_ofPred_eq, Set.mem_empty_iff_false, iff_false]
    rw [isMin_iff_forall_not_lt] at hi_min
    cases τ ω with
    | top => simp
    | coe t => exact mod_cast hi_min t
  have : {ω : Ω | τ ω < i} = τ ⁻¹' Set.Iic (pred i : ι) := by
    ext ω
    push _ ∈ _
    cases τ ω with
    | top => simp
    | coe t =>
      simp only [coe_lt_coe, coe_le_coe]
      rw [le_pred_iff_of_not_isMin hi_min]
  rw [this]
  exact f.mono (pred_le i) _ (hτ.measurableSet_le <| pred i)

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

Goal state before:
pp: case succ
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
k : ℕ
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
h : lowerCrossingTime a b f N (k + 1) ω < N
h' : upperCrossingTime a b f N (k + 1) ω < N
⊢ upperCrossingTime a b f M (k + 1) ω = upperCrossingTime a b f N (k + 1) ω ∧
    lowerCrossingTime a b f M (k + 1) ω = lowerCrossingTime a b f N (k + 1) ω

Tactic:
have : upperCrossingTime a b f M k.succ ω = upperCrossingTime a b f N k.succ ω := by
      rw [upperCrossingTime_succ_eq, hittingBtwn_lt_iff] at h'
      · simp only [upperCrossingTime_succ_eq]
        obtain ⟨j, hj₁, hj₂⟩ := h'
        rw [eq_comm, ih.2]
        exact hittingBtwn_eq_hittingBtwn_of_exists hNM ⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩
      · exact le_rfl

Goal state after:
case succ
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
k : ℕ
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
h : lowerCrossingTime a b f N (k + 1) ω < N
h' : upperCrossingTime a b f N (k + 1) ω < N
this : upperCrossingTime a b f M k.succ ω = upperCrossingTime a b f N k.succ ω
⊢ upperCrossingTime a b f M (k + 1) ω = upperCrossingTime a b f N (k + 1) ω ∧
    lowerCrossingTime a b f M (k + 1) ω = lowerCrossingTime a b f N (k + 1) ω
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
k : ℕ
hk : 1 ≤ k ∧ k < upcrossingsBefore a b f N ω + 1
⊢ {n | upperCrossingTime a b f N n ω < N}.indicator 1 k = 1

Tactic:
Set.indicator_of_mem

Goal state after:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
k : ℕ
hk : 1 ≤ k ∧ k < upcrossingsBefore a b f N ω + 1
⊢ 1 k = 1

case h
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
k : ℕ
hk : 1 ≤ k ∧ k < upcrossingsBefore a b f N ω + 1
⊢ k ∈ {n | upperCrossingTime a b f N n ω < N}
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
⊢ MeasurableSet s ↔ MeasurableSet s ∧ MeasurableSet s

Tactic:
measurableSpace_min hτ hπ

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
⊢ MeasurableSet s ↔ MeasurableSet s ∧ MeasurableSet s
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: case e'_2
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := ⋯
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n ↦ g n ω) ↔ ∃ c, Tendsto (fun n ↦ g n ω) atTop (𝓝 c)
⊢ (∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n ↦ g n ω) atTop (𝓝 c)

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩ <;> obtain ⟨c, hc⟩ := h
    · exact ⟨c - f 0 ω, hc.sub_const _⟩
    · refine ⟨c + f 0 ω, ?_⟩
      have := hc.add_const (f 0 ω)
      simpa only [g, sub_add_cancel]

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

Goal state before:
pp: case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᵐ[μ] Y
ht : 0 ≤ t
htY : Integrable (fun ω ↦ rexp (t * Y ω)) μ
htX : ¬Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ mgf X μ t ≤ mgf Y μ t

Tactic:
mgf_undef htX

Goal state after:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᵐ[μ] Y
ht : 0 ≤ t
htY : Integrable (fun ω ↦ rexp (t * Y ω)) μ
htX : ¬Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ 0 ≤ mgf Y μ t
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᵐ[μ] Y
ht : t ≤ 0
htX : Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ mgf Y μ t ≤ mgf X μ t

Tactic:
by_cases htY : Integrable (fun ω ↦ exp (t * Y ω)) μ

Goal state after:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᵐ[μ] Y
ht : t ≤ 0
htX : Integrable (fun ω ↦ rexp (t * X ω)) μ
htY : Integrable (fun ω ↦ rexp (t * Y ω)) μ
⊢ mgf Y μ t ≤ mgf X μ t

case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᵐ[μ] Y
ht : t ≤ 0
htX : Integrable (fun ω ↦ rexp (t * X ω)) μ
htY : ¬Integrable (fun ω ↦ rexp (t * Y ω)) μ
⊢ mgf Y μ t ≤ mgf X μ t
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case inr
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
⊢ u i ω = {ω | τ ω = ↑i}.indicator (u i) ω

pp: case inr.h
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
⊢ ω ∉ {a | ↑n ≤ τ a}

Tactic:
Set.indicator_of_mem

Goal state after:
case inr
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
⊢ u i ω = u i ω

case inr.h
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
⊢ ω ∈ {ω | τ ω = ↑i}

case inr.h
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
⊢ ω ∉ {a | ↑n ≤ τ a}
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_2
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
μ✝ : Measure Ω✝
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ a • t₁ + b • t₂ ≤ t₂

Tactic:
· simp only [smul_eq_mul]
    calc a * t₁ + b * t₂
    _ ≤ a * t₂ + b * t₂ := by gcongr
    _ = t₂ := by rw [← add_mul, hab, one_mul]

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝¹ : PartialOrder ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' ↑s
⊢ MemLp (stoppedValue u τ) p μ

Tactic:
rw [stoppedValue_eq_of_mem_finset hbdd]
  refine memLp_finsetSum' _ fun i _ => MemLp.indicator ?_ (hu i)
  refine ℱ.le i {a : Ω | τ a = i} (hτ.measurableSet_eq_of_countable_range ?_ i)
  have : Set.range τ ⊆ WithTop.some '' s := by
    rintro x ⟨y, rfl⟩
    exact hbdd y
  exact ((Finset.finite_toSet s).image _).subset this |>.countable

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝⁴ : LinearOrder ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s
⊢ MemLp (stoppedProcess u τ n) p μ

Tactic:
stoppedProcess_eq_of_mem_finset n hbdd

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝⁴ : LinearOrder ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s
⊢ MemLp ({a | ↑n ≤ τ a}.indicator (u n) + ∑ i ∈ s with i < n, {ω | τ ω = ↑i}.indicator (u i)) p μ
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
ht_nonneg : 0 ≤ t
⊢ Integrable (fun ω ↦ rexp (|t| * |X ω| + v * X ω)) μ

pp: case inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
ht_nonpos : t ≤ 0
⊢ Integrable (fun ω ↦ rexp (|t| * |X ω| + v * X ω)) μ

Tactic:
· simp_rw [abs_of_nonneg ht_nonneg]
    exact integrable_exp_mul_abs_add ht_int_pos ht_int_neg

Goal state after:
case inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
ht_nonpos : t ≤ 0
⊢ Integrable (fun ω ↦ rexp (|t| * |X ω| + v * X ω)) μ
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ' : Measure Ω'
Y : Ω' → ℝ
h : IdentDistrib X Y μ μ'
⊢ complexMGF X μ = complexMGF Y μ'

Tactic:
← complexMGF_id_map h.aemeasurable_fst,

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ' : Measure Ω'
Y : Ω' → ℝ
h : IdentDistrib X Y μ μ'
⊢ complexMGF id (Measure.map X μ) = complexMGF Y μ'
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ gaussianReal μ v ≪ ℙ

Tactic:
gaussianReal_of_var_ne_zero _ hv

Goal state after:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ ℙ.withDensity (gaussianPDF μ v) ≪ ℙ
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ ℙ ≪ gaussianReal μ v

Tactic:
gaussianReal_of_var_ne_zero _ hv

Goal state after:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ ℙ ≪ ℙ.withDensity (gaussianPDF μ v)
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: case neg
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
⊢ ∂gaussianReal μ v/∂ℙ =ᵐ[ℙ] gaussianPDF μ v

Tactic:
gaussianReal_of_var_ne_zero _ hv

Goal state after:
case neg
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
⊢ ∂ℙ.withDensity (gaussianPDF μ v)/∂ℙ =ᵐ[ℙ] gaussianPDF μ v