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 : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), ↑(f x) = ↑x
r : ℕ
hr : (f a).natAbs ^ 2 + (f b).natAbs ^ 2 + (f c).natAbs ^ 2 + (f d).natAbs ^ 2 = m * r
hr₀ : 0 < r
hrm : r < m
w x y z : ℤ
hw : ↑m ∣ w
hx : ↑m ∣ x
hy : ↑m ∣ y
hz : ↑m ∣ z
h : w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = ↑(m * r) * ↑(m * p)
| ↑(m * r) * ↑(m * p)

Tactic:
← h

Goal state after:
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 : (f a).natAbs ^ 2 + (f b).natAbs ^ 2 + (f c).natAbs ^ 2 + (f d).natAbs ^ 2 = m * r
hr₀ : 0 < r
hrm : r < m
w x y z : ℤ
hw : ↑m ∣ w
hx : ↑m ∣ x
hy : ↑m ∣ y
hz : ↑m ∣ z
h : w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = ↑(m * r) * ↑(m * p)
| w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2
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
⊢ ‖eval (x • s) (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p))‖ ≤ c ^ p

Tactic:
← h

Goal state after:
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
⊢ ‖eval (x • s) (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p))‖ ≤ |max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖| ^ p
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
⊢ x * ↑n < ↑(⌊x * ↑n⌋ + 1)

Tactic:
Int.cast_add,

Goal state after:
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
⊢ x * ↑n < ↑⌊x * ↑n⌋ + ↑1
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: case h
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
this : x < ↑(⌊x * ↑n⌋ + 1) / ↑n
⊢ ↑(⌊x * ↑n⌋ + 1) / ↑n - x < 2 / ↑n

Tactic:
sub_lt_iff_lt_add',

Goal state after:
case h
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
this : x < ↑(⌊x * ↑n⌋ + 1) / ↑n
⊢ ↑(⌊x * ↑n⌋ + 1) / ↑n < x + 2 / ↑n
Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual

Goal state before:
pp: case refine_2
r : ℚ
⊢ ↑r ∈ {x | x ∈ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)}

Tactic:
simp only [mem_iInter, mem_iUnion]

Goal state after:
case refine_2
r : ℚ
⊢ ↑r ∈ {x | ∀ (i : ℕ), ∃ i_1 i_2, ∃ (_ : 1 < i_2), x ∈ ball (↑i_1 / ↑i_2) (1 / ↑i_2 ^ i)}
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: case h.right.refine_2
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 : ℕ
p_gt : p > (eval 0 f).natAbs
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'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (X ^ (p - 1) * f ^ p).natDegree - p
r : ℂ
h : (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = ↑p ! * (aeval r) gp
hr : r ∈ f.aroots ℂ
this :
  (↑(eval 0 f ^ p + ↑p * eval 0 gp') * cexp r - ↑p * (aeval r) gp) * ↑(p - 1)! =
    ↑(eval 0 f) ^ p * cexp r * ↑(p - 1)! + ↑(p * (p - 1)!) * (↑(eval 0 gp') * cexp r - (aeval r) gp)
⊢ ‖↑(eval 0 f) ^ p * cexp r * ↑(p - 1)! + (↑p ! * (↑(eval 0 gp') * cexp r) - ↑p ! * (aeval r) gp)‖ ≤
    (if h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty then (Multiset.map c' (f.aroots ℂ)).toFinset.max' h
      else 0) ^
      p

Tactic:
← h

Goal state after:
case h.right.refine_2
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 : ℕ
p_gt : p > (eval 0 f).natAbs
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'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (X ^ (p - 1) * f ^ p).natDegree - p
r : ℂ
h : (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = ↑p ! * (aeval r) gp
hr : r ∈ f.aroots ℂ
this :
  (↑(eval 0 f ^ p + ↑p * eval 0 gp') * cexp r - ↑p * (aeval r) gp) * ↑(p - 1)! =
    ↑(eval 0 f) ^ p * cexp r * ↑(p - 1)! + ↑(p * (p - 1)!) * (↑(eval 0 gp') * cexp r - (aeval r) gp)
⊢ ‖↑(eval 0 f) ^ p * cexp r * ↑(p - 1)! +
        (↑p ! * (↑(eval 0 gp') * cexp r) - (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)))‖ ≤
    (if h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty then (Multiset.map c' (f.aroots ℂ)).toFinset.max' h
      else 0) ^
      p
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: case refine_2
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ C / ↑n ^ p * |↑r| = ↑r.den ^ p * (↑|r| * C) / (↑r.den * ↑n) ^ p

Tactic:
rw [mul_rpow, mul_div_mul_left, mul_comm, mul_div_assoc]

Goal state after:
case refine_2
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ |↑r| * (C / ↑n ^ p) = ↑|r| * (C / ↑n ^ p)

case refine_2.hc
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ ↑r.den ^ p ≠ 0

case refine_2.hx
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ 0 ≤ ↑r.den

case refine_2.hy
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ 0 ≤ ↑n
Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure

Goal state before:
pp: p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n.succ)
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
⊢ |x - ↑a / ↑b| < 1 / ↑b

Tactic:
refine hlt.trans_le (one_div_le_one_div_of_le hb0 ?_)

Goal state after:
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n.succ)
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
⊢ ↑b ≤ ↑b ^ (2 + 1 / ↑n.succ)
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: case a.s
p : ℕ
inst✝ : Fact (Nat.Prime p)
| Ico 1 p

pp: case a.f
p : ℕ
inst✝ : Fact (Nat.Prime p)
| fun x ↦ ↑x

pp: case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
| -1

Tactic:
← Nat.add_one_sub_one p,

Goal state after:
case a.s
p : ℕ
inst✝ : Fact (Nat.Prime p)
| Ico 1 (p + 1 - 1)

case a.f
p : ℕ
inst✝ : Fact (Nat.Prime p)
| fun x ↦ ↑x

case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
| -1
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:
← @bounded_le_inter_lt _ s _ a

Goal state after:
α : 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 ∩ {b | a < b})
Module: Mathlib.Order.CompleteLattice.PiLex

Goal state before:
pp: case refine_2
ι : 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)
h : e ∈ upperBounds s
⊢ sSup s ≤ e

Tactic:
· by_contra! hs
    obtain ⟨a, ha⟩ := hs
    refine ha.2.not_ge <| sSup_apply_le fun f hf hf' ↦ apply_le_of_toLex (h hf) ?_
    simp_all

Goal state after:
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : CompleteLatticeHom α β
L✝ L M : CompleteSublattice α
h : (fun L ↦ L.carrier) L = (fun L ↦ L.carrier) M
⊢ L = M

Tactic:
by cases L; cases M; congr; exact SetLike.coe_injective h

Goal state after:
Module: Mathlib.Order.CompleteSublattice

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

Tactic:
obtain ⟨b, hb, hb'⟩ := h a ha
    exact ⟨⟨b, hb⟩, CompleteSublattice.isCompl_iff.mpr hb'⟩

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 ⊢

Goal state after:
α : Type u_2
S : Set (Set α)
inst✝ : LE α
hS : ∀ s ∈ S, CountableSupClosed s
A : Set α
hA_ne : A.Nonempty
hAc : A.Countable
x : α
hx : IsLUB A x
hAS : ∀ t' ∈ S, A ⊆ t'
⊢ ∀ t ∈ S, x ∈ t
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: case refine_2
ι : Sort u_1
α : Type u_2
β : Type u_3
S : Set (Set α)
s✝ t : Set α
a b : α
inst✝ : Preorder α
s A : Set α
hA_ne : A.Nonempty
hAc : A.Countable
x : α
hx : IsLUB A x
B : ⦃a : α⦄ → a ∈ A → Set α
hB : ∀ ⦃a : α⦄ (a_1 : a ∈ A), B a_1 ⊆ s
hB_ne : ∀ ⦃a : α⦄ (a_1 : a ∈ A), (B a_1).Nonempty
hBc : ∀ ⦃a : α⦄ (a_1 : a ∈ A), (B a_1).Countable
hB_lub : ∀ ⦃a : α⦄ (a_1 : a ∈ A), IsLUB (B a_1) a
⊢ (⋃ a, B ⋯).Countable

Tactic:
have : Countable A := Set.countable_coe_iff.mpr hAc
      exact Set.countable_iUnion fun a ↦ hBc a.2

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: case refine_1
α : Type u_2
s : Set α
a : α
inst✝ : CompleteLattice α
h_csc : CountableSupClosed {a | ∃ t, (∀ (n : ℕ), t n ∈ s) ∧ ⨆ n, t n = a}
⊢ s ⊆ {a | ∃ t, (∀ (n : ℕ), t n ∈ s) ∧ ⨆ n, t n = a}

pp: case refine_2
α : Type u_2
s : Set α
a : α
inst✝ : CompleteLattice α
h_csc : CountableSupClosed {a | ∃ t, (∀ (n : ℕ), t n ∈ s) ∧ ⨆ n, t n = a}
⊢ {a | ∃ t, (∀ (n : ℕ), t n ∈ s) ∧ ⨆ n, t n = a} ⊆ countableSupClosure s

Tactic:
· exact fun a ha ↦ ⟨fun _ ↦ a, by simp [ha]⟩

Goal state after:
case refine_2
α : Type u_2
s : Set α
a : α
inst✝ : CompleteLattice α
h_csc : CountableSupClosed {a | ∃ t, (∀ (n : ℕ), t n ∈ s) ∧ ⨆ n, t n = a}
⊢ {a | ∃ t, (∀ (n : ℕ), t n ∈ s) ∧ ⨆ n, t n = a} ⊆ countableSupClosure s
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
hA : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∨ A ↑p =ᵐ[μ] univ
hB : ∀ (p : Nat.Primes), B ↑p =ᵐ[μ] ∅ ∨ B ↑p =ᵐ[μ] univ
hC : ∀ (p : Nat.Primes), u p +ᵥ C ↑p = C ↑p
h : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅
p : Nat.Primes
hE₂ : E =ᵐ[μ] C ↑p
h_qmp : Measure.QuasiMeasurePreserving (fun x ↦ -u p +ᵥ x) μ μ
⊢ u p +ᵥ C ↑p =ᵐ[μ] C ↑p

Tactic:
hC

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
hA : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∨ A ↑p =ᵐ[μ] univ
hB : ∀ (p : Nat.Primes), B ↑p =ᵐ[μ] ∅ ∨ B ↑p =ᵐ[μ] univ
hC : ∀ (p : Nat.Primes), u p +ᵥ C ↑p = C ↑p
h : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅
p : Nat.Primes
hE₂ : E =ᵐ[μ] C ↑p
h_qmp : Measure.QuasiMeasurePreserving (fun x ↦ -u p +ᵥ x) μ μ
⊢ C ↑p =ᵐ[μ] C ↑p
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: case refine_2
A : Type u_1
inst✝⁵ : NormedAddCommGroup A
inst✝⁴ : CompactSpace A
inst✝³ : PreconnectedSpace A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure A
inst✝ : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ : μ univ ≤ (n + 1) • μ (closedBall 0 (δ / 2))
B : ↑(Icc 0 n) → Set A := fun j ↦ closedBall (↑j • ξ) (δ / 2)
hB : ∀ (j : ↑(Icc 0 n)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
this : ¬Pairwise (Disjoint on B)
i j : ↑(Icc 0 n)
hij : i < j
x : A
hx : x ∈ B i ∩ B j
⊢ dist (↑j • ξ) (↑i • ξ) ≤ δ

Tactic:
exact (dist_triangle ((j : ℕ) • ξ) x ((i : ℕ) • ξ)).trans (by
        linarith [mem_closedBall.mp hx.1, mem_closedBall'.mp hx.2])

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝⁵ : NormedAddCommGroup A
inst✝⁴ : CompactSpace A
inst✝³ : PreconnectedSpace A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure A
inst✝ : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ : μ univ ≤ (n + 1) • μ (closedBall 0 (δ / 2))
B : ↑(Icc 0 n) → Set A := fun j ↦ closedBall (↑j • ξ) (δ / 2)
hB : ∀ (j : ↑(Icc 0 n)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
h : Pairwise (Disjoint on B)
h' : ⋃ j, B j = univ
contra : ¬0 ≤ δ / 2
⊢ μ (closedBall 0 (δ / 2)) = 0

Tactic:
rw [not_le, ← closedBall_eq_empty (x := (0 : A))] at contra

Goal state after:
A : Type u_1
inst✝⁵ : NormedAddCommGroup A
inst✝⁴ : CompactSpace A
inst✝³ : PreconnectedSpace A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure A
inst✝ : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ : μ univ ≤ (n + 1) • μ (closedBall 0 (δ / 2))
B : ↑(Icc 0 n) → Set A := fun j ↦ closedBall (↑j • ξ) (δ / 2)
hB : ∀ (j : ↑(Icc 0 n)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
h : Pairwise (Disjoint on B)
h' : ⋃ j, B j = univ
contra : closedBall 0 (δ / 2) = ∅
⊢ μ (closedBall 0 (δ / 2)) = 0
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n m : Nucleus X
h : ⇑n ∘ ⇑m = ⇑m
⊢ ⇑n ≤ ⇑m

Tactic:
← h

Goal state after:
X : Type u_1
inst✝ : Frame X
n m : Nucleus X
h : ⇑n ∘ ⇑m = ⇑m
⊢ ⇑n ≤ ⇑n ∘ ⇑m
Module: Mathlib.Order.Rel.GaloisConnection

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
J J' : Set α
h : J' ∈ R.leftFixedPoints
h₁ : J ⊆ J'
⊢ R.rightDual (R.leftDual J) ⊆ J'

Tactic:
← h

Goal state after:
α : Type u_1
β : Type u_2
R : SetRel α β
J J' : Set α
h : J' ∈ R.leftFixedPoints
h₁ : J ⊆ J'
⊢ R.rightDual (R.leftDual J) ⊆ R.rightDual (R.leftDual J')
Module: Mathlib.Order.Rel.GaloisConnection

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
I I' : Set β
h : I' ∈ R.rightFixedPoints
h₁ : I ⊆ I'
⊢ R.leftDual (R.rightDual I) ⊆ I'

Tactic:
← h

Goal state after:
α : Type u_1
β : Type u_2
R : SetRel α β
I I' : Set β
h : I' ∈ R.rightFixedPoints
h₁ : I ⊆ I'
⊢ R.leftDual (R.rightDual I) ⊆ R.leftDual (R.rightDual 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
a₁ : α
⊢ ∀ {y : α}, a₁ ⊓ y ∈ J → a₁ ∈ J ∨ y ∈ J

Tactic:
a₂

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₂ : α
⊢ a₁ ⊓ a₂ ∈ J → a₁ ∈ J ∨ a₂ ∈ J
Module: Mathlib.Order.SaddlePoint

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

Tactic:
← h

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

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

Tactic:
← h

Goal state after:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : Nat.find ⋯ = 0
⊢ Order.pred^[Nat.find ⋯] r = ⊥
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: case succ
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
n✝ : ℕ
h : Nat.find ⋯ = n✝ + 1
⊢ Order.pred^[n✝ + 1] r = ⊥

Tactic:
← h

Goal state after:
case succ
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
n✝ : ℕ
h : Nat.find ⋯ = n✝ + 1
⊢ Order.pred^[Nat.find ⋯] r = ⊥
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : ↑t
h₁ : t₁.root ≤ v₁
h₂ : t₂.root ≤ v₂
h : v₁ ⊓ v₂ ≠ ⊥
⊢ t₁ = t₂

Tactic:
← bot_lt_iff_ne_bot

Goal state after:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : ↑t
h₁ : t₁.root ≤ v₁
h₂ : t₂.root ≤ v₂
h : ⊥ < v₁ ⊓ v₂
⊢ t₁ = t₂
Module: Mathlib.Probability.Process.Adapted

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝³ : Preorder ι
β : ι → Type u_3
inst✝² : (i : ι) → TopologicalSpace (β i)
u : (i : ι) → Ω → β i
inst✝¹ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝ : ∀ (i : ι), BorelSpace (β i)
hum : ∀ (i : ι), StronglyMeasurable (u i)
i : ι
⊢ StronglyMeasurable (u i)

Tactic:
rw [stronglyMeasurable_iff_measurable_separable]

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝³ : Preorder ι
β : ι → Type u_3
inst✝² : (i : ι) → TopologicalSpace (β i)
u : (i : ι) → Ω → β i
inst✝¹ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝ : ∀ (i : ι), BorelSpace (β i)
hum : ∀ (i : ι), StronglyMeasurable (u i)
i : ι
⊢ Measurable (u i) ∧ IsSeparable (Set.range (u i))
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))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : ℕ → ℕ × Ω → E :=
  fun m_1 x ↦
    match x.1 with
    | 0 => (h₀.approx m_1) x.2
    | n.succ => (⋯.approx m_1) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
⊢ IsStronglyPredictable 𝓕 u

Tactic:
refine ⟨fun m ↦ SimpleFunc.mk (Y m) ?_ ?_, ?_⟩

Goal state after:
case refine_1
Ω : 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
X : ℕ → ℕ × Ω → E :=
  fun m x ↦
    match x.1 with
    | 0 => (h₀.approx m) x.2
    | n.succ => (⋯.approx m) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
⊢ ∀ (x : E), MeasurableSet (Y m ⁻¹' {x})

case refine_2
Ω : 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
X : ℕ → ℕ × Ω → E :=
  fun m x ↦
    match x.1 with
    | 0 => (h₀.approx m) x.2
    | n.succ => (⋯.approx m) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
⊢ (Set.range (Y m)).Finite

case refine_3
Ω : 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
X : ℕ → ℕ × Ω → E :=
  fun m_1 x ↦
    match x.1 with
    | 0 => (h₀.approx m_1) x.2
    | n.succ => (⋯.approx m_1) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
⊢ ∀ (x : ℕ × Ω),
    Tendsto (fun n ↦ ((fun m_1 ↦ { toFun := Y m_1, measurableSet_fiber' := ⋯, finite_range' := ⋯ }) n) x) atTop
      (𝓝 (Function.uncurry u x))
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Preorder ι
inst✝ : InfSet ι
u : ι → Ω → β
n m : ι
⊢ hittingBtwn u ∅ n m = fun x ↦ m

Tactic:
ext; simp [hittingBtwn]

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

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
inst✝ : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted ℱ fun n ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ
hhdef : h = f - martingalePart (f + g) ℱ μ
⊢ h = predictablePart (f + g) ℱ μ - g

Tactic:
rw [hhdef, sub_eq_sub_iff_add_eq_add, add_comm (predictablePart (f + g) ℱ μ),
      martingalePart_add_predictablePart]

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 : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ u (hittingBtwn u s n m ω) ω ∈ s

Tactic:
simp_rw [hittingBtwn, if_pos h_exists]
  have h_nonempty : (Set.Icc n m ∩ {i : ι | u i ω ∈ s}).Nonempty := by
    obtain ⟨k, hk₁, hk₂⟩ := h_exists
    exact ⟨k, Set.mem_inter hk₁ hk₂⟩
  have h_mem := csInf_mem h_nonempty
  rw [Set.mem_inter_iff] at h_mem
  exact h_mem.2

Goal state after: