mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
h : |max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖| ≤ c
hx : x ∈ Set.Ioc 0 1
⊢ (x * ‖s‖) ^ (p - 1) ≤ (if x * ‖s‖ ≤ 1 then 1 else x * ‖s‖) ^ p

Tactic:
split_ifs with hx1

Goal state after:
case pos
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
h : |max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖| ≤ c
hx : x ∈ Set.Ioc 0 1
hx1 : x * ‖s‖ ≤ 1
⊢ (x * ‖s‖) ^ (p - 1) ≤ 1 ^ p

case neg
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
h : |max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖| ≤ c
hx : x ∈ Set.Ioc 0 1
hx1 : ¬x * ‖s‖ ≤ 1
⊢ (x * ‖s‖) ^ (p - 1) ≤ (x * ‖s‖) ^ p
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case refine_1
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 : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), ↑(f x) = ↑x
r : ℕ
hr₀ : 0 < r
hrm : r < m
hr : f b ^ 2 + f a ^ 2 + f d ^ 2 + (-f c) ^ 2 = ↑(m * r)
this :
  (f b * ↑a - f a * ↑b - f d * ↑c - -f c * ↑d) ^ 2 + (f b * ↑b + f a * ↑a + f d * ↑d - -f c * ↑c) ^ 2 +
        (f b * ↑c - f a * ↑d + f d * ↑a + -f c * ↑b) ^ 2 +
      (f b * ↑d + f a * ↑c - f d * ↑b + -f c * ↑a) ^ 2 =
    ↑(m * r) * ↑(m * p)
⊢ ↑m ∣ f b * ↑a - f a * ↑b - f d * ↑c - -f c * ↑d

Tactic:
simp [← ZMod.intCast_zmod_eq_zero_iff_dvd, hf_mod, mul_comm]

Goal state after:
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case refine_3
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 : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), ↑(f x) = ↑x
r : ℕ
hr₀ : 0 < r
hrm : r < m
hr : f b ^ 2 + f a ^ 2 + f d ^ 2 + (-f c) ^ 2 = ↑(m * r)
this :
  (f b * ↑a - f a * ↑b - f d * ↑c - -f c * ↑d) ^ 2 + (f b * ↑b + f a * ↑a + f d * ↑d - -f c * ↑c) ^ 2 +
        (f b * ↑c - f a * ↑d + f d * ↑a + -f c * ↑b) ^ 2 +
      (f b * ↑d + f a * ↑c - f d * ↑b + -f c * ↑a) ^ 2 =
    ↑(m * r) * ↑(m * p)
⊢ ↑m ∣ f b * ↑c - f a * ↑d + f d * ↑a + -f c * ↑b

Tactic:
simp [← ZMod.intCast_zmod_eq_zero_iff_dvd, hf_mod, mul_comm]

Goal state after:
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case refine_4
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 : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), ↑(f x) = ↑x
r : ℕ
hr₀ : 0 < r
hrm : r < m
hr : f b ^ 2 + f a ^ 2 + f d ^ 2 + (-f c) ^ 2 = ↑(m * r)
this :
  (f b * ↑a - f a * ↑b - f d * ↑c - -f c * ↑d) ^ 2 + (f b * ↑b + f a * ↑a + f d * ↑d - -f c * ↑c) ^ 2 +
        (f b * ↑c - f a * ↑d + f d * ↑a + -f c * ↑b) ^ 2 +
      (f b * ↑d + f a * ↑c - f d * ↑b + -f c * ↑a) ^ 2 =
    ↑(m * r) * ↑(m * p)
⊢ ↑m ∣ f b * ↑d + f a * ↑c - f d * ↑b + -f c * ↑a

Tactic:
simp [← ZMod.intCast_zmod_eq_zero_iff_dvd, hf_mod, mul_comm]

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

Goal state before:
pp: n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!) ≤ 2 * (1 / m ^ (n + 1)!)

Tactic:
gcongr; exact sub_one_div_inv_le_two hm

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

Goal state before:
pp: m : ℕ
hm : 0 < m
k : ℕ
⊢ ∃ p, partialSum (↑m) k = ↑p / ↑(m ^ k !)

Tactic:
induction k with
  | zero => exact ⟨1, by rw [partialSum, range_one, sum_singleton, Nat.cast_one, Nat.factorial,
      pow_one, pow_one]⟩
  | succ k h =>
    rcases h with ⟨p_k, h_k⟩
    use p_k * m ^ ((k + 1)! - k !) + 1
    rw [partialSum_succ, h_k, div_add_div, div_eq_div_iff, add_mul]
    · norm_cast
      rw [add_mul, one_mul, Nat.factorial_succ, add_mul, one_mul, add_tsub_cancel_right, pow_add]
      simp [mul_assoc]
    all_goals positivity

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

Goal state before:
pp: ⊢ {x | Irrational x} ∩ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) ∈ residual ℝ

Tactic:
refine eventually_residual_irrational.and ?_

Goal state after:
⊢ Filter.Eventually (Membership.mem (⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n))) (residual ℝ)
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p x : ℝ
h : LiouvilleWith p x
⊢ ∃ C, ∃ (_ : 0 < C), ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p

Tactic:
rcases h with ⟨C, hC⟩
  refine ⟨max C 1, zero_lt_one.trans_le <| le_max_right _ _, ?_⟩
  refine ((eventually_ge_atTop 1).and_frequently hC).mono ?_
  rintro n ⟨hle, m, hne, hlt⟩
  refine ⟨hle, m, hne, hlt.trans_le ?_⟩
  gcongr
  apply le_max_left

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

Goal state before:
pp: case refine_2.refine_1
r : ℚ
n : ℕ
this : 0 < r.den
⊢ 1 < ↑r.den * 2

Tactic:
lia

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

Goal state before:
pp: p x : ℝ
m : ℤ
hm : m ≠ 0
⊢ LiouvilleWith p (x * ↑m) ↔ LiouvilleWith p x

Tactic:
mul_int_iff hm

Goal state after:
p x : ℝ
m : ℤ
hm : m ≠ 0
⊢ LiouvilleWith p x ↔ LiouvilleWith p x
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)
hB : ∀ (a : ℤ) (b : ℕ), volume (B a b) = ↑(2 / ↑b ^ r)
b : ℕ
⊢ ∑ a ∈ Finset.Icc 0 ↑b, volume (B a b) = ↑((↑b + 1) * (2 / ↑b ^ r))

Tactic:
simp only [hB, Int.card_Icc, Finset.sum_const, nsmul_eq_mul, sub_zero,
          Int.toNat_natCast, ← Nat.cast_succ, ENNReal.coe_mul, ENNReal.coe_natCast]

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: case refine_1
δ : ℕ → ℝ
x : UnitAddCircle
n : ℕ
hn : n ∈ {n | 0 < n ∧ x ∈ approxAddOrderOf UnitAddCircle n (δ n)}
⊢ n ∈ {n | ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ n}

Tactic:
exact (mem_approxAddOrderOf_iff hn.1).mp hn.2

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
q : ℕ
hn : 0 < p * q
h_ndiv : ¬p * p ∣ p * q
⊢ (addOrderOf x).Coprime (p * q / p)

Tactic:
hu₀,

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
q : ℕ
hn : 0 < p * q
h_ndiv : ¬p * p ∣ p * q
⊢ (↑⟨p, hp⟩).Coprime (p * q / p)
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ principal a = principal b ↔ a = b

Tactic:
simp [le_antisymm_iff]

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
S : Set (Set α)
inst✝ : LE α
hS : ∀ s ∈ S, CountableSupClosed s
A : Set α
hAS : A ⊆ ⋂₀ S
hA_ne : A.Nonempty
hAc : A.Countable
x : α
hx : IsLUB A x
⊢ x ∈ ⋂₀ S

Tactic:
simp only [subset_sInter_iff, mem_sInter] at hAS ⊢
    exact fun s hs ↦ (hS s hs).isLUB_mem A (hAS s hs) hA_ne hAc x hx

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: case e'_4
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 (δ n) ⊆
    (fun y ↦ x + y) '' approxAddOrderOf 𝕊 (n / p) (↑p * δ n)
⊢ n = addOrderOf x * (n / p)

Tactic:
hu₀,

Goal state after:
case e'_4
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 (δ n) ⊆
    (fun y ↦ x + y) '' approxAddOrderOf 𝕊 (n / p) (↑p * δ n)
⊢ n = ↑⟨p, hp⟩ * (n / p)
Module: Mathlib.Order.Filter.Partial

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : SetRel α β
l : Filter α
x✝ y✝ : Set β
hs : x✝ ∈ {s | r.core s ∈ l}
ht : y✝ ∈ {s | r.core s ∈ l}
⊢ r.core (x✝ ∩ y✝) = r.core x✝ ∩ r.core y✝

Tactic:
← SetRel.core_inter

Goal state after:
α : Type u
β : Type v
γ : Type w
r : SetRel α β
l : Filter α
x✝ y✝ : Set β
hs : x✝ ∈ {s | r.core s ∈ l}
ht : y✝ ∈ {s | r.core s ∈ l}
⊢ r.core (x✝ ∩ y✝) = r.core (x✝ ∩ y✝)
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : FunLike F α β
inst✝ : LatticeHomClass F α β
f : F
w✝ x✝² y✝ z✝ : α
x✝¹ : (Setoid.ker ⇑f) w✝ x✝²
x✝ : (Setoid.ker ⇑f) y✝ z✝
⊢ (Setoid.ker ⇑f) (w✝ ⊓ y✝) (x✝² ⊓ z✝)

Tactic:
by simp_all +instances only [Setoid.ker, onFun, map_inf]

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n✝ m : Nucleus X
x y : X
n : Nucleus X
⊢ ↑(rangeFactorization ⇑n ⊤) = ↑⊤

Tactic:
exact map_top n

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 α) := ⋯
IinS : ↑I ∈ S
c : Set (Set α)
hcS : c ⊆ S
hcC : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
hcNe : c.Nonempty
⊢ ⋃₀ c ∈ S ∧ ∀ s ∈ c, s ⊆ ⋃₀ c

Tactic:
refine ⟨?_, fun s hs ↦ le_sSup hs⟩

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}
IinS : ↑I ∈ S
c : Set (Set α)
hcS : c ⊆ S
hcC : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
hcNe : c.Nonempty
⊢ ⋃₀ c ∈ S
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : Order.pred^[Nat.find ⋯ - 1] r = ⊥
this : Nat.find ⋯ ≤ Nat.find ⋯ - 1
⊢ Nat.find ⋯ = 0

Tactic:
lia

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝² : Preorder ι
f : Filtration ι m
β : Type u_3
u : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : OpensMeasurableSpace β
hu : IsProgressive f u
i : ι
⊢ Measurable fun p ↦ (fun t ω ↦ ‖u t ω‖) (↑p.1) p.2

Tactic:
by apply @(hu i).norm; infer_instance

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

Goal state before:
pp: Ω : Type u_1
m✝ : MeasurableSpace Ω
𝓕 : Filtration ℕ m✝
n : ℕ
s : Set Ω
hs : MeasurableSet s
m : ℕ
⊢ m = n + 1 ↔ n < m ∧ m ≤ n + 1

Tactic:
lia

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

Goal state before:
pp: case refine_1
Ω : 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
⊢ μ[f 0 | ↑ℱ i] =ᵐ[μ] f 0

Tactic:
condExp_of_stronglyMeasurable (ℱ.le _) _ (hf_int 0)

Goal state after:
case refine_1
Ω : 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
⊢ f 0 =ᵐ[μ] f 0

Ω : 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
⊢ StronglyMeasurable (f 0)
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case zero
Ω : Type u_1
ι : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
ω : Ω
⊢ upperCrossingTime a b f N 0 ω ≤ N

Tactic:
simp only [upperCrossingTime_zero, Pi.bot_apply, bot_le]

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

Goal state before:
pp: case pos
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : N < Nat.find ⋯
hmono : StrictMonoOn (fun n ↦ upperCrossingTime a b f N n ω) (Set.Iic (Nat.find ⋯).pred)
⊢ N ≤ upperCrossingTime a b f N N ω

Tactic:
convert! StrictMonoOn.Iic_id_le hmono N (Nat.le_sub_one_of_lt hN')

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 : ι
ω : Ω
inst✝ : WellFoundedLT ι
m i : ι
hi : i < m
⊢ hittingBtwn u s n m ω ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s

Tactic:
by_cases h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s

Goal state after:
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m i : ι
hi : i < m
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ hittingBtwn u s n m ω ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s

case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m i : ι
hi : i < m
h_exists : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ hittingBtwn u s n m ω ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case refine_2
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
a b : ℝ
N : ℕ
⊢ ∀ (n : ℕ) (ω : Ω), 0 ≤ (1 - upcrossingStrat a b f N n) ω

Tactic:
· intro n ω
    simp [upcrossingStrat_le_one]

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

Goal state before:
pp: Ω : 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, (∀ (n : ℕ), t < s n) ∧ Tendsto s atTop (𝓝 t)

Tactic:
have h_freq : ∃ᶠ x in 𝓝[>] t, t < x :=
      Eventually.frequently <| eventually_nhdsWithin_of_forall fun _ hx ↦ hx

Goal state after:
Ω : 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
h_freq : ∃ᶠ (x : ι) in 𝓝[>] t, t < x
⊢ ∃ s, (∀ (n : ℕ), t < s n) ∧ Tendsto s atTop (𝓝 t)
Module: Mathlib.Probability.Martingale.Convergence

Goal state before:
pp: case pos
Ω : Type u_1
f : ℕ → Ω → ℝ
ω : Ω
hf₁ : liminf (fun n ↦ ↑‖f n ω‖₊) atTop < ∞
hf₂ : ∀ (a b : ℚ), a < b → upcrossings (↑a) (↑b) f ω < ∞
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ |f n ω|
⊢ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)

Tactic:
rw [isBoundedUnder_le_abs] at h
    refine tendsto_of_no_upcrossings Rat.denseRange_cast ?_ h.1 h.2
    rintro _ ⟨a, rfl⟩ _ ⟨b, rfl⟩ hab
    exact not_frequently_of_upcrossings_lt_top hab (hf₂ a b (Rat.cast_lt.1 hab)).ne

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

Goal state before:
pp: case refine_2
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hfN : ∀ (ω : Ω), a ≤ f N ω
hfzero : 0 ≤ f 0
hab : a < b
ω : Ω
⊢ (b - a) * ↑(upcrossingsBefore a b f N ω) ≤ (∑ k ∈ Finset.range N, upcrossingStrat a b f N k * (f (k + 1) - f k)) ω

Tactic:
simpa using mul_upcrossingsBefore_le (hfN ω) hab

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

Goal state before:
pp: case refine_1
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
hab : a < b
this : ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hR' : ∀ (n : ℕ), ∫⁻ (ω : Ω), ↑‖f n ω - a‖₊ ∂μ ≤ ↑R + ↑‖a‖₊ * μ Set.univ
n : ℕ
ω : Ω
⊢ ↑‖f n ω - a‖₊ ≠ ∞

Tactic:
· finiteness

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

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι✝ : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst✝² : SemilatticeSup ι
inst✝¹ : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
⊢ SigmaFinite (μ.trim ⋯)

Tactic:
by
  refine @sigmaFiniteTrim_mono _ _ ?_ _ _ _ ?_ ?_
  · exact f ⊥
  · exact hτ.le_measurableSpace_of_const_le fun _ => bot_le
  · infer_instance

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

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι✝ : Type u_3
m : MeasurableSpace Ω
ι : Type u_4
inst✝² : SemilatticeSup ι
inst✝¹ : OrderBot ι
μ : Measure Ω
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : SigmaFiniteFiltration μ f
hτ : IsStoppingTime f τ
n : ι
hτ_le : ∀ (ω : Ω), τ ω ≤ ↑n
⊢ SigmaFinite (μ.trim ⋯)

Tactic:
by
  refine @sigmaFiniteTrim_mono _ _ ?_ _ _ _ ?_ ?_
  · exact f ⊥
  · exact hτ.le_measurableSpace_of_const_le fun _ => bot_le
  · infer_instance

Goal state after: