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

Goal state before:
pp: case neg
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
h₁ : j ∉ {x | ∃ k, beattySeq r k = x}
⊢ j ∈ {x | ∃ k, beattySeq r k = x}ᶜ ↔ j ∈ {x | ∃ k, beattySeq' s k = x}

Tactic:
by_cases h₂ : j ∈ {beattySeq' s k | k}

Goal state after:
case pos
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
h₁ : j ∉ {x | ∃ k, beattySeq r k = x}
h₂ : j ∈ {x | ∃ k, beattySeq' s k = x}
⊢ j ∈ {x | ∃ k, beattySeq r k = x}ᶜ ↔ j ∈ {x | ∃ k, beattySeq' s k = x}

case neg
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
h₁ : j ∉ {x | ∃ k, beattySeq r k = x}
h₂ : j ∉ {x | ∃ k, beattySeq' s k = x}
⊢ j ∈ {x | ∃ k, beattySeq r k = x}ᶜ ↔ j ∈ {x | ∃ k, beattySeq' s k = x}
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d e : ℕ
hl : Squarefree (d * e)
hnu_nonzero : s.nu (d * e) ≠ 0
hd : (d, e) ∈ (d * e).divisorsAntidiagonal
⊢ d.Coprime e ∧ ?m.123

Tactic:
simpa only [squarefree_mul_iff] using hl

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case a.hd
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
l : ℕ
hl : (l ∣ s.prodPrimes ∧ ¬s.prodPrimes = 0) ∧ l ∣ d
⊢ selbergTerms l ≠ 0

Tactic:
exact (selbergTerms_pos hl.1.1).ne'

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case a.hd
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
l : ℕ
hl : (l ∣ s.prodPrimes ∧ ¬s.prodPrimes = 0) ∧ l ∣ d
⊢ selbergTerms l ≠ 0

Tactic:
· exact (selbergTerms_pos hl.1.1).ne'

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
⊢ IsSquare (-1) ↔ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3

Tactic:
rw [ZMod.isSquare_neg_one_iff_forall_mem_primeFactors_mod_four_ne_three hn]

Goal state after:
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
⊢ (∀ q ∈ n.primeFactors, q % 4 ≠ 3) ↔ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: case refine_3
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3
p q : ℕ
hp : Nat.Prime p
hq : q ∣ n → q % 4 ≠ 3
hpq : p * q ∣ n
⊢ p * q % 4 ≠ 3

Tactic:
· replace hp := H _ <|
      Nat.mem_primeFactors.mpr ⟨hp, dvd_of_mul_right_dvd hpq, Squarefree.ne_zero hn⟩
    replace hq := hq (dvd_of_mul_left_dvd hpq)
    rw [show 3 = 3 % 4 by simp, Ne, ← ZMod.natCast_eq_natCast_iff'] at hp hq ⊢
    rw [Nat.cast_mul]
    exact help p q hp hq

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber

Goal state before:
pp: case h
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ p_k * m ^ (k * k ! + k !) * m ^ (k * k ! + k !) + m ^ k ! * 1 * m ^ (k * k ! + k !) =
    p_k * m ^ (k * k !) * (m ^ k ! * m ^ (k * k ! + k !)) + m ^ k ! * m ^ (k * k ! + k !)

Tactic:
pow_add

Goal state after:
case h
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ p_k * (m ^ (k * k !) * m ^ k !) * (m ^ (k * k !) * m ^ k !) + m ^ k ! * 1 * (m ^ (k * k !) * m ^ k !) =
    p_k * m ^ (k * k !) * (m ^ k ! * (m ^ (k * k !) * m ^ k !)) + m ^ k ! * (m ^ (k * k !) * m ^ k !)
Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual

Goal state before:
pp: case refine_2.refine_2.convert_2
r : ℚ
n : ℕ
⊢ 0 < 1 / ↑(↑r.den * 2) ^ n

Tactic:
refine one_div_pos.2 (pow_pos (Int.cast_pos.2 ?_) _)

Goal state after:
case refine_2.refine_2.convert_2
r : ℚ
n : ℕ
⊢ 0 < ↑r.den * 2
Module: Mathlib.Order.Bounded

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : LinearOrder α
a : α
⊢ Bounded (fun x1 x2 ↦ x1 ≤ x2) (s ∩ {b | a < b}) ↔ Bounded (fun x1 x2 ↦ x1 ≤ x2) s

Tactic:
simp_rw [← not_le, bounded_le_inter_not_le]

Goal state after:
Module: Mathlib.Order.Bounds.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ GaloisConnection (⇑OrderDual.toDual ∘ upperBounds) (lowerBounds ∘ ⇑OrderDual.ofDual)

Tactic:
simpa [GaloisConnection, subset_def, mem_upperBounds, mem_lowerBounds]
    using fun S T ↦ forall₂_comm

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure

Goal state before:
pp: r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b ↦ ball (↑a / ↑b) (1 / ↑b ^ r)
a : ℤ
b : ℕ
⊢ ENNReal.ofReal (2 * (1 / ↑b ^ r)) = ↑(2 / ↑b ^ r)

Tactic:
mul_one_div,

Goal state after:
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b ↦ ball (↑a / ↑b) (1 / ↑b ^ r)
a : ℤ
b : ℕ
⊢ ENNReal.ofReal (2 / ↑b ^ r) = ↑(2 / ↑b ^ r)
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
a : α
b : β
⊢ a ∈ lowerPolar r {b} ↔ r a b

Tactic:
simp_rw [mem_lowerPolar_iff, mem_singleton_iff, forall_eq]

Goal state after:
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
s s' : Set α
h : IsExtent r s
hs' : s' ⊆ s
⊢ lowerPolar r (upperPolar r s') ⊆ lowerPolar r (upperPolar r s)

Tactic:
exact lowerPolar_upperPolar_monotone r hs'

Goal state after:
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
hA : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∨ A ↑p =ᵐ[μ] univ
hB : ∀ (p : Nat.Primes), B ↑p =ᵐ[μ] ∅ ∨ B ↑p =ᵐ[μ] univ
⊢ (∀ᵐ (x : 𝕊), x ∉ E) ∨ E ∈ ae volume

Tactic:
rw [← eventuallyEq_empty, ← eventuallyEq_univ]

Goal state after:
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
hA : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∨ A ↑p =ᵐ[μ] univ
hB : ∀ (p : Nat.Primes), B ↑p =ᵐ[μ] ∅ ∨ B ↑p =ᵐ[μ] univ
⊢ E =ᵐ[volume] ∅ ∨ E =ᵐ[volume] univ
Module: Mathlib.Order.Filter.Partial

Goal state before:
pp: α : Type u
β : Type v
f : α →. β
l₁ : Filter α
l₂ : Filter β
h : f.Dom ∈ l₁
h' : ∀ s ∈ l₂, f.core s ∈ l₁
s : Set β
sl₂ : s ∈ l₂
⊢ f.core s ∩ f.Dom ∈ l₁

Tactic:
exact inter_mem (h' s sl₂) h

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : LE α
⊢ (univ.chainHeight fun x1 x2 ↦ x1 ≤ x2) = s.chainHeight fun x1 x2 ↦ x1 ≤ x2

Tactic:
simpa using chainHeight_coe_univ s (· ≤ ·)

Goal state after:
Module: Mathlib.Order.Interval.Set.SurjOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a : α
⊢ SurjOn f (Ioi a) (Ioi (f a))

Tactic:
rw [← compl_Iic, ← compl_compl (Ioi (f a))]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a : α
⊢ SurjOn f (Iic a)ᶜ (Ioi (f a))ᶜᶜ
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n✝ m✝ : Nucleus X
x✝ y✝ : X
m n : Nucleus X
x y : X
this : Nonempty X
k : X
hxyk : k ≥ x ⊓ y
l : X
hlx : ∀ x_1 ≥ x, l ⊓ m x_1 ≤ n x_1
hly : ∀ i ≥ y, l ⊓ m i ≤ n i
hlk : l ≤ m k
⊢ l = l ⊓ m (x ⊔ k) ⊓ (l ⊓ m (y ⊔ k))

Tactic:
rw [← inf_inf_distrib_left, ← map_inf, ← sup_inf_right, sup_eq_right.2 hxyk,
            inf_eq_left.2 hlk]

Goal state after:
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
⊢ a₁ ⊓ a₂ ∉ J

Tactic:
have J₂S : ↑J₂ ∉ S := fun h => J₂J (hmax.eq_of_le h (le_sup_left : J ≤ J₂)).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
⊢ a₁ ⊓ a₂ ∉ J
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α✝ : Type u_1
s✝ t x y z : α✝
S : Set α✝
inst✝¹ : CompleteLattice α✝
P✝ Q✝ : Partition s✝
α : Type u_2
inst✝ : Order.Frame α
s : α
P Q R : Partition s
hQ : P ≤ Q
hR : P ≤ R
a : α
ha : a ∈ P
q : α
hq : q ∈ Q ∧ a ≤ q
⊢ ∃ y ∈ removeBot {a | ∃ p ∈ Q, ∃ q ∈ R, a = p ⊓ q} ⋯ ⋯, a ≤ y

Tactic:
have ⟨r, hr⟩ := hR ha

Goal state after:
α✝ : Type u_1
s✝ t x y z : α✝
S : Set α✝
inst✝¹ : CompleteLattice α✝
P✝ Q✝ : Partition s✝
α : Type u_2
inst✝ : Order.Frame α
s : α
P Q R : Partition s
hQ : P ≤ Q
hR : P ≤ R
a : α
ha : a ∈ P
q : α
hq : q ∈ Q ∧ a ≤ q
r : α
hr : r ∈ R ∧ a ≤ r
⊢ ∃ y ∈ removeBot {a | ∃ p ∈ Q, ∃ q ∈ R, a = p ⊓ q} ⋯ ⋯, a ≤ y
Module: Mathlib.Order.Types.Arithmetic

Goal state before:
pp: a b c : OrderType.{u_1}
⊢ a * (b + c) = a * b + a * c

Tactic:
refine inductionOn₃ a b c (fun _ _ _ _ _ _ ↦ ?_)

Goal state after:
a b c : OrderType.{u_1}
x✝⁵ : Type u_1
x✝⁴ : LinearOrder x✝⁵
x✝³ : Type u_1
x✝² : LinearOrder x✝³
x✝¹ : Type u_1
x✝ : LinearOrder x✝¹
⊢ type x✝⁵ * (type x✝³ + type x✝¹) = type x✝⁵ * type x✝³ + type x✝⁵ * type x✝¹
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m
u : ℕ → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
n : ℕ
⊢ StronglyMeasurable (u (n + 1))

Tactic:
let : MeasurableSpace (ℕ × Ω) := 𝓕.predictable

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m
u : ℕ → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
n : ℕ
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
⊢ StronglyMeasurable (u (n + 1))
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
⊢ IsStronglyPredictable 𝓕 u

Tactic:
let : MeasurableSpace (ℕ × Ω) := 𝓕.predictable

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
⊢ IsStronglyPredictable 𝓕 u
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 g : ι → Ω → E
ℱ : Filtration ι m0
inst✝¹ : CompleteSpace E
inst✝ : LE E
hf : Supermartingale f ℱ μ
hg : StronglyAdapted ℱ g
h_eq✝ : ∀ (t : ι), f t =ᵐ[μ] g t
i j : ι
hij : i ≤ j
ω : Ω
h_le : μ[f j | ↑ℱ i] ω ≤ f i ω
hcond : μ[f j | ?m.84] ω = μ[g j | ?m.84] ω
h_eq : f i ω = g i ω
⊢ μ[g j | ↑ℱ i] ω ≤ g i ω

Tactic:
rwa [← hcond, ← h_eq]

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

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
ω : Ω
m : ι
hmn : m ≤ m
x✝ : ι
| x✝ ∈ Set.Icc m m ∧ u x✝ ω ∈ s → sInf (Set.Icc m m ∩ {i | u i ω ∈ s}) = m

Tactic:
rw [Set.mem_Icc, Set.Icc_self, and_imp, and_imp]

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
ω : Ω
m : ι
hmn : m ≤ m
x✝ : ι
| m ≤ x✝ → x✝ ≤ m → u x✝ ω ∈ s → sInf ({m} ∩ {i | u i ω ∈ s}) = m
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this : {ω | τ ω < ↑i} = {ω | τ ω ≤ ↑i} \ {ω | τ ω = ↑i}
⊢ MeasurableSet ({ω | τ ω ≤ ↑i} \ {ω | τ ω = ↑i})

Tactic:
exact (hτ.measurableSet_le i).diff (hτ.measurableSet_eq_of_countable_range h_countable i)

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

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
h' : hittingAfter u s n ω < ↑i
h_top : hittingAfter u s n ω ≠ ⊤
⊢ ∃ j, n ≤ j ∧ u j ω ∈ s

Tactic:
ne_eq,

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
h' : hittingAfter u s n ω < ↑i
h_top : ¬hittingAfter u s n ω = ⊤
⊢ ∃ j, n ≤ j ∧ u j ω ∈ s
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case mp
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
h_top : hittingAfter u s n ω ≠ ⊤
h_exists : ∃ j, n ≤ j ∧ u j ω ∈ s
h_le : ↑n ≤ hittingAfter u s n ω
h' : ∃ b ∈ {i | n ≤ i ∧ u i ω ∈ s}, b < i
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s

Tactic:
simp only [Set.mem_ofPred_eq] at h'

Goal state after:
case mp
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
h_top : hittingAfter u s n ω ≠ ⊤
h_exists : ∃ j, n ≤ j ∧ u j ω ∈ s
h_le : ↑n ≤ hittingAfter u s n ω
h' : ∃ b, (n ≤ b ∧ u b ω ∈ s) ∧ b < i
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
hN : N ≤ 0
⊢ upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N

Tactic:
Nat.le_zero

Goal state after:
case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
hN : N = 0
⊢ upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrderBot ι
inst✝ : WellFoundedLT ι
u : ι → Ω → β
s : Set β
i n : ι
ω : Ω
hx : ∃ j ≤ n, u j ω ∈ s
⊢ hittingBtwn u s ⊥ n ω ≤ i ↔ ∃ j ≤ i, u j ω ∈ s

Tactic:
by
  rcases lt_or_ge i n with hi | hi
  · rw [hittingBtwn_le_iff_of_lt _ hi]
    simp
  · simp only [(hittingBtwn_le ω).trans hi, true_iff]
    obtain ⟨j, hj₁, hj₂⟩ := hx
    exact ⟨j, hj₁.trans hi, hj₂⟩

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

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : ℕ → Set Ω
i : ι
hs : ∀ (b : ι) (a : ℕ), MeasurableSet (s a ∩ {ω | τ ω ≤ ↑b})
⊢ MeasurableSet (⋃ i_1, s i_1 ∩ {ω | τ ω ≤ ↑i})

Tactic:
exact MeasurableSet.iUnion (hs i)

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

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst✝ : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
⊢ ∀ (τ_1 π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ_1 →
      IsStoppingTime 𝒢 π →
        τ_1 ≤ π →
          (∃ N, ∀ (x : Ω), π x ≤ ↑N) →
            ∫ (x : Ω), stoppedValue (stoppedProcess f τ) τ_1 x ∂μ ≤ ∫ (x : Ω), stoppedValue (stoppedProcess f τ) π x ∂μ

Tactic:
intro σ

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst✝ : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
σ : Ω → ℕ∞
⊢ ∀ (π : Ω → ℕ∞),
    IsStoppingTime 𝒢 σ →
      IsStoppingTime 𝒢 π →
        σ ≤ π →
          (∃ N, ∀ (x : Ω), π x ≤ ↑N) →
            ∫ (x : Ω), stoppedValue (stoppedProcess f τ) σ x ∂μ ≤ ∫ (x : Ω), stoppedValue (stoppedProcess f τ) π x ∂μ
Module: Mathlib.Probability.Martingale.OptionalStopping

Goal state before:
pp: case ha
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
this :
  ∀ (ω : Ω),
    (↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω) → ↑ε ≤ stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) ω
h :
  ↑ε * μ.real {a | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k a} ≤
    ∫ (x : Ω) in {a | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k a},
      stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) x ∂μ
⊢ ε • μ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω} ≠ ∞

Tactic:
exact ENNReal.mul_ne_top (by simp) (measure_ne_top _ _)

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

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝² : Nonempty ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst✝¹ : LinearOrder ι
inst✝ : Zero β
s : Set Ω
⊢ stoppedProcess (fun i ↦ s.indicator (u i)) τ = fun i ↦ s.indicator (stoppedProcess u τ i)

Tactic:
ext i ω

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝² : Nonempty ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst✝¹ : LinearOrder ι
inst✝ : Zero β
s : Set Ω
i : ι
ω : Ω
⊢ stoppedProcess (fun i ↦ s.indicator (u i)) τ i ω = s.indicator (stoppedProcess u τ i) ω
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
⊢ stoppedProcess (stoppedProcess u τ) σ = stoppedProcess u (σ ⊓ τ)

Tactic:
ext i ω

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
i : ι
ω : Ω
⊢ stoppedProcess (stoppedProcess u τ) σ i ω = stoppedProcess u (σ ⊓ τ) i ω
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : Integrable X μ
⊢ centralMoment X 1 μ = 0

Tactic:
rw [centralMoment_one' h_int]
    simp

Goal state after:
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
  by_cases htY : Integrable (fun ω ↦ exp (t * Y ω)) μ
  · refine integral_mono_ae htY htX ?_
    filter_upwards [hXY] with ω hω using exp_monotone <| mul_le_mul_of_nonpos_left hω ht
  · rw [mgf_undef htY]
    exact mgf_nonneg

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
hX : AEStronglyMeasurable (fun ω ↦ rexp (t * X ω)) μ
hY : AEStronglyMeasurable (fun ω ↦ rexp (t * Y ω)) μ
⊢ ∫ (x : Ω), rexp (t * X x) * rexp (t * Y x) ∂μ = (∫ (x : Ω), rexp (t * X x) ∂μ) * ∫ (x : Ω), rexp (t * Y x) ∂μ

Tactic:
exact (h_indep.exp_mul t t).integral_mul_eq_mul_integral hX hY

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
h_int_X : Integrable (fun ω ↦ rexp (t * X ω)) μ
h_int_Y : Integrable (fun ω ↦ rexp (t * Y ω)) μ
⊢ Integrable (fun ω ↦ rexp (t * X ω) * rexp (t * Y ω)) μ

Tactic:
exact (h_indep.exp_mul t t).integrable_mul h_int_X h_int_Y

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

Goal state before:
pp: case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω ↦ rexp (a * X ω)) μ
hb : Integrable (fun ω ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : ¬a = b
ha_zero : ¬a = 0
⊢ AEMeasurable X μ

Tactic:
exact aemeasurable_of_aemeasurable_exp_mul ha_zero ha.1.aemeasurable

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

Goal state before:
pp: case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → WithTop ι
i : ι
s : Set Ω
inst✝ : DecidablePred fun x ↦ x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), ↑i ≤ τ ω
hη : ∀ (ω : Ω), ↑i ≤ η ω
hs : MeasurableSet s
n : ι
this : {ω | s.piecewise τ η ω ≤ ↑n} = s ∩ {ω | τ ω ≤ ↑n} ∪ sᶜ ∩ {ω | η ω ≤ ↑n}
hin : ¬i ≤ n
hτn : ∀ (ω : Ω), ¬τ ω ≤ ↑n
hηn : ∀ (ω : Ω), ¬η ω ≤ ↑n
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ ↑n} ∪ sᶜ ∩ {ω | η ω ≤ ↑n})

Tactic:
simp [hτn, hηn, @MeasurableSet.empty _ _]

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

Goal state before:
pp: Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (fun n ↦ ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 ω) atTop atTop ↔
      Tendsto (fun n ↦ ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | ↑ℱ k] ω) atTop atTop

Tactic:
have := tendsto_sum_indicator_atTop_iff (Eventually.of_forall fun ω n => ?_)
    (stronglyAdapted_process hs) (integrable_process μ hs)
    (Eventually.of_forall <| process_difference_le s)

Goal state after:
case refine_2
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
this :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (fun n ↦ process s n ω) atTop atTop ↔ Tendsto (fun n ↦ predictablePart (process s) ℱ μ n ω) atTop atTop
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (fun n ↦ ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 ω) atTop atTop ↔
      Tendsto (fun n ↦ ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | ↑ℱ k] ω) atTop atTop

case refine_1
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
ω : Ω
n : ℕ
⊢ process s n ω ≤ process s (n + 1) ω
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
f : Ω → E
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : SecondCountableTopology ι
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (μ.trim ⋯)
⊢ μ[f | ⋯.measurableSpace] =ᵐ[μ.restrict {x | τ x ≤ σ x}] μ[f | hτ.measurableSpace]

Tactic:
by
  have : SigmaFinite (μ.trim hτ.measurableSpace_le) :=
    sigmaFiniteTrim_mono _ (hτ.measurableSpace_min hσ ▸ inf_le_left)
  refine (condExp_ae_eq_restrict_of_measurableSpace_eq_on hτ.measurableSpace_le
    (hτ.min hσ).measurableSpace_le (hτ.measurableSet_le_stopping_time hσ) fun t => ?_).symm
  rw [Set.inter_comm _ t, hτ.measurableSet_inter_le_iff hσ]

Goal state after: