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

Goal state before:
pp: p : ℕ
hp : Prime p
this✝ : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
hm✝ : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
m : ℕ
hmin : ∀ m_1 < m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
hm₁ : 1 < m
this : NeZero m
hm : ¬2 ∣ m
⊢ ∃ f, (∀ (x : ℕ), 2 * (f x).natAbs < m) ∧ ∀ (x : ℕ), ↑(f x) = ↑x

Tactic:
refine ⟨fun x ↦ (x : ZMod m).valMinAbs, fun x ↦ ?_, fun x ↦ (x : ZMod m).coe_valMinAbs⟩
      exact (mul_le_mul' le_rfl (x : ZMod m).natAbs_valMinAbs_le).trans_lt
        (Nat.mul_div_lt_iff_not_dvd.2 hm)

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: case h.left
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
prime_p : Nat.Prime p
gp' : ℤ[X]
h' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
h : ↑p ∣ eval 0 f ^ p
⊢ p ≤ (eval 0 f).natAbs

Tactic:
exact Nat.le_of_dvd (Int.natAbs_pos.mpr hf) (Int.natCast_dvd.mp (Int.Prime.dvd_pow' prime_p h))

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

Goal state before:
pp: x : ℝ
⊢ LiouvilleWith 1 x

Tactic:
use 2

Goal state after:
case h
x : ℝ
⊢ ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < 2 / ↑n ^ 1
Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure

Goal state before:
pp: x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
this :
  ∀ (y : ℝ),
    LiouvilleWith p y →
      y ∈ Ico 0 1 → ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |y - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(n + 1))
⊢ x ∈
    ⋃ m,
      (fun x ↦ x + ↑m) ⁻¹'
        ⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}

Tactic:
simp only [mem_iUnion, mem_preimage]
    have hx : x + ↑(-⌊x⌋) ∈ Ico (0 : ℝ) 1 := by
      simp only [Int.floor_le, Int.lt_floor_add_one, add_neg_lt_iff_le_add', zero_add, and_self_iff,
        mem_Ico, Int.cast_neg, le_add_neg_iff_add_le]
    exact ⟨-⌊x⌋, n + 1, n.succ_pos, this _ (hxp.add_int _) hx⟩

Goal state after:
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ↑(p - 1)! = ∏ x ∈ Ico 1 (p - 1).succ, ↑x

Tactic:
rw [← Finset.prod_Ico_id_eq_factorial, prod_natCast]

Goal state after:
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: case refine_3.refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
h : (↑b).val = val 0
⊢ b = 0

Tactic:
simpa only [val_cast_of_lt hb.right, val_zero] using h

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

Goal state before:
pp: x : ℝ
hx : Liouville x
p : ℝ
⊢ LiouvilleWith p x

Tactic:
by
  suffices LiouvilleWith ⌈p⌉₊ x from this.mono (Nat.le_ceil p)
  refine ⟨1, ((eventually_gt_atTop 1).and_frequently (hx.frequently_exists_num ⌈p⌉₊)).mono ?_⟩
  rintro b ⟨_hb, a, hne, hlt⟩
  refine ⟨a, hne, ?_⟩
  rwa [rpow_natCast]

Goal state after:
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
a b : ↥L
⊢ Disjoint ↑a ↑b ∧ Codisjoint a b ↔ Disjoint ↑a ↑b ∧ Codisjoint ↑a ↑b

Tactic:
CompleteSublattice.codisjoint_iff

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
a b : ↥L
⊢ Disjoint ↑a ↑b ∧ Codisjoint ↑a ↑b ↔ Disjoint ↑a ↑b ∧ Codisjoint ↑a ↑b
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
x✝ : ComplementedLattice ↥L
a : α
ha : a ∈ L
h : ∀ (a : ↥L), ∃ b, IsCompl a b
b : ↥L
hb : IsCompl ⟨a, ha⟩ b
⊢ ∃ b ∈ L, IsCompl a b

Tactic:
exact ⟨b, b.property, CompleteSublattice.isCompl_iff.mp hb⟩

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
p : ℕ
hp : Nat.Prime p
x : 𝕊 := u ⟨p, hp⟩
f : 𝕊 → 𝕊 := fun y ↦ p • y + x
n : ℕ
hn : 0 < n
h_ndiv : ¬p * p ∣ n
h_cop : (addOrderOf x).Coprime (n / p)
h_div : n / p * p = n
hf : f = (fun y ↦ x + y) ∘ fun y ↦ p • y
this : Monotone (image fun y ↦ x + y)
⊢ (fun y ↦ x + y) '' (fun y ↦ p • y) '' X n ⊆ approxAddOrderOf 𝕊 n (↑p * δ n)

Tactic:
specialize this (approxAddOrderOf.image_nsmul_subset (δ n) (n / p) hp.pos)

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
p : ℕ
hp : Nat.Prime p
x : 𝕊 := u ⟨p, hp⟩
f : 𝕊 → 𝕊 := fun y ↦ p • y + x
n : ℕ
hn : 0 < n
h_ndiv : ¬p * p ∣ n
h_cop : (addOrderOf x).Coprime (n / p)
h_div : n / p * p = n
hf : f = (fun y ↦ x + y) ∘ fun y ↦ p • y
this :
  (fun y ↦ x + y) '' (fun y ↦ p • y) '' approxAddOrderOf 𝕊 (n / p * p) (δ n) ⊆
    (fun y ↦ x + y) '' approxAddOrderOf 𝕊 (n / p) (↑p * δ n)
⊢ (fun y ↦ x + y) '' (fun y ↦ p • y) '' X n ⊆ approxAddOrderOf 𝕊 n (↑p * δ n)
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: case refine_1
ι α β : Type u
c : Cardinal.{u}
l✝ : Filter α
inst✝ : CardinalInterFilter l✝ c
l : Set (Set α)
hc : 2 < c
hUnion : ∀ (S : Set (Set α)), #↑S < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
S : Set (Set α)
hSc : #↑S < c
hSp : S ⊆ {s | sᶜ ∈ l}
s : Set α
hs : ∃ x ∈ S, xᶜ = s
⊢ s ∈ l

Tactic:
rcases hs with ⟨t, ht, rfl⟩

Goal state after:
case refine_1
ι α β : Type u
c : Cardinal.{u}
l✝ : Filter α
inst✝ : CardinalInterFilter l✝ c
l : Set (Set α)
hc : 2 < c
hUnion : ∀ (S : Set (Set α)), #↑S < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
S : Set (Set α)
hSc : #↑S < c
hSp : S ⊆ {s | sᶜ ∈ l}
t : Set α
ht : t ∈ S
⊢ tᶜ ∈ l
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: case refine_2
α : ℕ → 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 : ℕ
b : α (i + 1)
h : i ≤ i + 1
⊢ ¬⟨i, π h b⟩ = ⟨i + 1, b⟩ ∧
    ∀ (a : ℕ) (b_1 : α a),
      ⟨i, π h b⟩ ≤ ⟨a, b_1⟩ → ⟨a, b_1⟩ ≤ ⟨i + 1, b⟩ → ¬⟨a, b_1⟩ = ⟨i, π h b⟩ → ⟨a, b_1⟩ = ⟨i + 1, b⟩

Tactic:
refine ⟨fun h ↦ by simp at h, ?_⟩

Goal state after:
case refine_2
α : ℕ → 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 : ℕ
b : α (i + 1)
h : i ≤ i + 1
⊢ ∀ (a : ℕ) (b_1 : α a), ⟨i, π h b⟩ ≤ ⟨a, b_1⟩ → ⟨a, b_1⟩ ≤ ⟨i + 1, b⟩ → ¬⟨a, b_1⟩ = ⟨i, π h b⟩ → ⟨a, b_1⟩ = ⟨i + 1, b⟩
Module: Mathlib.Order.Std

Goal state before:
pp: α : Type u_1
args : OfStdArgs α
this✝⁵ : LE α := args.le
this✝⁴ : LT α := args.lt
this✝³ :
  let this := args.le;
  let this_1 := args.lt;
  Std.LawfulOrderLT α
this✝² :
  let this := args.le;
  Std.IsLinearOrder α
this✝¹ : DecidableLE α := args.decidableLE
this✝ : Std.LawfulOrderLeftLeaningMin α
this : Std.LawfulOrderLeftLeaningMax α
a b : α
h : ¬b ≤ a
⊢ b = if a ≤ b then b else a

Tactic:
case =>

Goal state after:
Module: Mathlib.Order.Std

Goal state before:
pp: α : Type u_1
args : OfStdArgs α
this✝⁷ : LE α := args.le
this✝⁶ : LT α := args.lt
this✝⁵ :
  let this := args.le;
  let this_1 := args.lt;
  Std.LawfulOrderLT α
this✝⁴ :
  let this := args.le;
  Std.IsLinearOrder α
this✝³ : DecidableLE α := args.decidableLE
this✝² : Std.LawfulOrderLeftLeaningMin α
this✝¹ : Std.LawfulOrderLeftLeaningMax α
a b : α
this✝ : Ord α := args.ord
this :
  let this := args.le;
  let this_1 := args.lt;
  let this_2 := ⋯;
  let this_3 := ⋯;
  let this_4 := args.decidableEq;
  let this_5 := args.decidableLT;
  Std.LawfulOrderOrd α
h✝ : a < b
⊢ compare a b = Ordering.lt

Tactic:
case =>

Goal state after:
Module: Mathlib.Order.Std

Goal state before:
pp: α : Type u_1
args : OfStdArgs α
this✝⁷ : LE α := args.le
this✝⁶ : LT α := args.lt
this✝⁵ :
  let this := args.le;
  let this_1 := args.lt;
  Std.LawfulOrderLT α
this✝⁴ :
  let this := args.le;
  Std.IsLinearOrder α
this✝³ : DecidableLE α := args.decidableLE
this✝² : Std.LawfulOrderLeftLeaningMin α
this✝¹ : Std.LawfulOrderLeftLeaningMax α
a b : α
this✝ : Ord α := args.ord
this :
  let this := args.le;
  let this_1 := args.lt;
  let this_2 := ⋯;
  let this_3 := ⋯;
  let this_4 := args.decidableEq;
  let this_5 := args.decidableLT;
  Std.LawfulOrderOrd α
h✝¹ : ¬a < b
h✝ : a = b
⊢ compare a b = Ordering.eq

Tactic:
case =>

Goal state after:
Module: Mathlib.Order.Std

Goal state before:
pp: α : Type u_1
args : OfStdArgs α
this✝⁷ : LE α := args.le
this✝⁶ : LT α := args.lt
this✝⁵ :
  let this := args.le;
  let this_1 := args.lt;
  Std.LawfulOrderLT α
this✝⁴ :
  let this := args.le;
  Std.IsLinearOrder α
this✝³ : DecidableLE α := args.decidableLE
this✝² : Std.LawfulOrderLeftLeaningMin α
this✝¹ : Std.LawfulOrderLeftLeaningMax α
a b : α
this✝ : Ord α := args.ord
this :
  let this := args.le;
  let this_1 := args.lt;
  let this_2 := ⋯;
  let this_3 := ⋯;
  let this_4 := args.decidableEq;
  let this_5 := args.decidableLT;
  Std.LawfulOrderOrd α
h : ¬a < b
h' : ¬a = b
⊢ compare a b = Ordering.gt

Tactic:
case =>

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s : Set X
f : ι → X
a✝ b✝ : X
S : Sublocale X
a : X
b : ↥S
⊢ S.restrictAux a ≤ b ↔ a ≤ ↑b

Tactic:
constructor <;> intro h
    · exact le_trans (by simp +contextual [restrictAux]) h
    · exact sInf_le (by simp [h])

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 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 | ↑ℱ i] ω = μ[g j | ↑ℱ i] ω
h_eq : f i ω = g i ω
⊢ μ[f j | ↑ℱ i] ω ≤ g i ω

Tactic:
← h_eq

Goal state after:
Ω : 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 | ↑ℱ i] ω = μ[g j | ↑ℱ i] ω
h_eq : f i ω = g i ω
⊢ μ[f j | ↑ℱ i] ω ≤ f 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 ω ∂μ
i j : ι
hij : i ≤ j
this : 0 ≤ᵐ[μ.trim ⋯] μ[f j | ↑ℱ i] - f i
x : Ω
hx : 0 x ≤ (μ[f j | ↑ℱ i] - f i) x
⊢ f i x ≤ μ[f j | ↑ℱ i] x

Tactic:
rwa [← sub_nonneg]

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 : ι
ω : Ω
m₁ m₂ : ι
h : m₁ ≤ m₂
j : ι
hj₁ : j ∈ Set.Icc n m₁
hj₂ : u j ω ∈ s
⊢ sInf (Set.Icc n m₁ ∩ {i | u i ω ∈ s}) = sInf (Set.Icc n m₂ ∩ {i | u i ω ∈ s})

Tactic:
refine le_antisymm ?_ (by gcongr; exacts [bddBelow_Icc.inter_of_left, ⟨j, hj₁, hj₂⟩])
    refine le_csInf ⟨j, Set.Icc_subset_Icc_right h hj₁, hj₂⟩ fun i hi => ?_
    by_cases hi' : i ≤ m₁
    · exact csInf_le bddBelow_Icc.inter_of_left ⟨⟨hi.1.1, hi'⟩, hi.2⟩
    · change j ∈ {i | u i ω ∈ s} at hj₂
      exact ((csInf_le bddBelow_Icc.inter_of_left ⟨hj₁, hj₂⟩).trans hj₁.2).trans (le_of_not_ge hi')

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

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : upperCrossingTime a b f N n ω < N
⊢ upperCrossingTime a b f M n ω = upperCrossingTime a b f N n ω

Tactic:
by
  cases n
  · simp
  · exact (crossing_eq_crossing_of_upperCrossingTime_lt hNM h).1

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

Goal state before:
pp: case refine_1
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : ConditionallyCompleteLinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet {ω | τ ω < ↑i}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet {ω | τ ω = ↑i}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι), t < u → ∃ i, s i < u
h_exists_lt' : ∀ (u : WithTop ι), ↑t < u → ∃ i, ↑(s i) < u
h_eq_iInter : {ω | τ ω ≤ ↑t} = ⋂ m, {ω | τ ω < ↑(s m)}
⊢ ⨅ j, ⨅ (_ : j > t), ↑f j ≤ ⨅ m_1, ↑f (s m_1)

pp: case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : ConditionallyCompleteLinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet {ω | τ ω < ↑i}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet {ω | τ ω = ↑i}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι), t < u → ∃ i, s i < u
h_exists_lt' : ∀ (u : WithTop ι), ↑t < u → ∃ i, ↑(s i) < u
h_eq_iInter : {ω | τ ω ≤ ↑t} = ⋂ m, {ω | τ ω < ↑(s m)}
⊢ ⨅ m_1, ↑f (s m_1) ≤ ⨅ j, ⨅ (_ : j > t), ↑f j

Tactic:
· simp only [gt_iff_lt, le_iInf_iff]
      exact fun i ↦ iInf₂_le (s i) (hs_gt i)

Goal state after:
case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : ConditionallyCompleteLinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet {ω | τ ω < ↑i}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet {ω | τ ω = ↑i}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι), t < u → ∃ i, s i < u
h_exists_lt' : ∀ (u : WithTop ι), ↑t < u → ∃ i, ↑(s i) < u
h_eq_iInter : {ω | τ ω ≤ ↑t} = ⋂ m, {ω | τ ω < ↑(s m)}
⊢ ⨅ m_1, ↑f (s m_1) ≤ ⨅ j, ⨅ (_ : j > t), ↑f j
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : ConditionallyCompleteLinearOrder ι
inst✝¹ : WellFoundedLT ι
inst✝ : Countable ι
x✝ : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n n' : ι
hu : Adapted f u
hs : MeasurableSet s
⊢ IsStoppingTime f fun ω ↦ ↑(hittingBtwn u s n n' ω)

Tactic:
by
  intro i
  rcases le_or_gt n' i with hi | hi
  · have h_le : ∀ ω, hittingBtwn u s n n' ω ≤ i := fun x => (hittingBtwn_le x).trans hi
    simp [h_le]
  · have h_set_eq_Union : {ω | hittingBtwn u s n n' ω ≤ i} = ⋃ j ∈ Set.Icc n i, u j ⁻¹' s := by
      ext; simp [hittingBtwn_le_iff_of_lt _ hi]
    simpa [h_set_eq_Union] using MeasurableSet.iUnion fun j =>
      MeasurableSet.iUnion fun hj => f.mono hj.2 _ ((hu j) hs)

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

Goal state before:
pp: case pos
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun m ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (k + 1) ω)) ω -
        stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N k ω)) ω
x✝ : upcrossingsBefore a b f N ω ∈ Finset.range N
hi : upcrossingsBefore a b f N ω ∉ Finset.range (upcrossingsBefore a b f N ω)
heq : lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω = N
⊢ 0 ≤ f (↑N).untopA ω - f (↑(lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω)).untopA ω

Tactic:
heq,

Goal state after:
case pos
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun m ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (k + 1) ω)) ω -
        stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N k ω)) ω
x✝ : upcrossingsBefore a b f N ω ∈ Finset.range N
hi : upcrossingsBefore a b f N ω ∉ Finset.range (upcrossingsBefore a b f N ω)
heq : lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω = N
⊢ 0 ≤ f (↑N).untopA ω - f (↑N).untopA ω
Module: Mathlib.Probability.Martingale.Convergence

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
this : ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ f n ω) atTop (𝓝 (g ω))
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ f n ω) atTop (𝓝 (limitProcess f ℱ μ ω))

Tactic:
rw [limitProcess, dif_pos this]
    exact (Classical.choose_spec this).2

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

Goal state before:
pp: case neg
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : b - a ≤ 0
⊢ ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ ⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ

Tactic:
ENNReal.ofReal_of_nonpos hab,

Goal state after:
case neg
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : b - a ≤ 0
⊢ 0 * ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ ⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
Module: Mathlib.Probability.Martingale.Convergence

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
ht : Tendsto (fun n ↦ eLpNorm (μ[μ[g | ⨆ n, ↑ℱ n] | ↑ℱ n] - μ[g | ⨆ n, ↑ℱ n]) 1 μ) atTop (𝓝 0)
heq : ∀ (n : ℕ), ∀ᵐ (x : Ω) ∂μ, μ[μ[g | ⨆ n, ↑ℱ n] | ↑ℱ n] x = μ[g | ↑ℱ n] x
n : ℕ
⊢ μ[μ[g | ⨆ n, ↑ℱ n] | ↑ℱ n] - μ[g | ⨆ n, ↑ℱ n] =ᵐ[μ] μ[g | ↑ℱ n] - μ[g | ⨆ n, ↑ℱ n]

Tactic:
filter_upwards [heq n] with x hxeq

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
ht : Tendsto (fun n ↦ eLpNorm (μ[μ[g | ⨆ n, ↑ℱ n] | ↑ℱ n] - μ[g | ⨆ n, ↑ℱ n]) 1 μ) atTop (𝓝 0)
heq : ∀ (n : ℕ), ∀ᵐ (x : Ω) ∂μ, μ[μ[g | ⨆ n, ↑ℱ n] | ↑ℱ n] x = μ[g | ↑ℱ n] x
n : ℕ
x : Ω
hxeq : μ[μ[g | ⨆ n, ↑ℱ n] | ↑ℱ n] x = μ[g | ↑ℱ n] x
⊢ (μ[μ[g | ⨆ n, ↑ℱ n] | ↑ℱ n] - μ[g | ⨆ n, ↑ℱ n]) x = (μ[g | ↑ℱ n] - μ[g | ⨆ n, ↑ℱ n]) x
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hX : ¬Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ mgf X μ t = 0

Tactic:
by
  simp only [mgf, integral_undef hX]

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
⊢ AEStronglyMeasurable (fun ω ↦ rexp (t * X ω)) μ

Tactic:
refine AEMeasurable.aestronglyMeasurable ?_

Goal state after:
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
⊢ AEMeasurable (fun ω ↦ rexp (t * X ω)) μ
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case inr
Ω : 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
this :
  ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : Measure Ω} ⦃t₁ : ℝ⦄,
    t₁ ∈ integrableExpSet X μ →
      ∀ ⦃t₂ : ℝ⦄,
        t₂ ∈ integrableExpSet X μ →
          ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → t₁ ≤ t₂ → a • t₁ + b • t₂ ∈ integrableExpSet X μ
h_le : t₂ < t₁
⊢ a • t₁ + b • t₂ ∈ integrableExpSet X μ

pp: Ω✝ : 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₂ ∈ integrableExpSet X μ

Tactic:
· rw [add_comm] at hab ⊢
    exact this ht₂ ht₁ hb ha hab h_le.le

Goal state after:
Ω✝ : 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₂ ∈ integrableExpSet X μ
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ ∀ᶠ (x : ℂ) in 𝓝 z, AEStronglyMeasurable (fun ω ↦ ↑(X ω) ^ n * cexp (x * ↑(X ω))) μ

Tactic:
exact .of_forall fun z ↦ by fun_prop

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

Goal state before:
pp: μ : ℝ
v : ℝ≥0
hv : v ≠ 0
x : ℝ
⊢ 0 < gaussianPDF μ v x

Tactic:
by
  rw [gaussianPDF, ENNReal.ofReal_pos]
  exact gaussianPDFReal_pos _ _ _ hv

Goal state after: