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

Goal state before:
pp: s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), (if n = 1 then 1 else 0) ≤ ∑ d ∈ n.divisors, muPlus d
⊢ (∑ y ∈ s.prodPrimes.divisors, ∑ x ∈ s.support, if y ∣ x then s.weights x * muPlus y else 0) =
    ∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum d

Tactic:
[

Goal state after:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), (if n = 1 then 1 else 0) ≤ ∑ d ∈ n.divisors, muPlus d
⊢ (∑ y ∈ s.prodPrimes.divisors, ∑ x ∈ s.support, if y ∣ x then s.weights x * muPlus y else 0) =
    ∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum d
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
this : ∀ (d1 d2 : ℕ), (d1 ∣ d ∧ d2 ∣ d ∧ d = d1.lcm d2) = (d = d1.lcm d2)
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then f d1 d2 d else 0) =
    ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then f d1 d2 d else 0

Tactic:
[

Goal state after:
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
this : ∀ (d1 d2 : ℕ), (d1 ∣ d ∧ d2 ∣ d ∧ d = d1.lcm d2) = (d = d1.lcm d2)
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then f d1 d2 d else 0) =
    ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then f d1 d2 d else 0
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case h
K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
hv : v.IsRankOneDiscrete
h0 : v ↑πᵥ ≠ 0
γ : Γˣ
x✝ : ∃ k, ⋯.unit ^ k = γ
k : ℤ
hk : ⋯.unit ^ k = γ
⊢ (MonoidWithZeroHom.ofClass v) 1 * ↑γ = (MonoidWithZeroHom.ofClass v) (↑πᵥ ^ k)

Tactic:
simp only [← Units.val_inj, Units.val_zpow_eq_zpow_val] at hk

Goal state after:
case h
K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
hv : v.IsRankOneDiscrete
h0 : v ↑πᵥ ≠ 0
γ : Γˣ
x✝ : ∃ k, ⋯.unit ^ k = γ
k : ℤ
hk : ↑⋯.unit ^ k = ↑γ
⊢ (MonoidWithZeroHom.ofClass v) 1 * ↑γ = (MonoidWithZeroHom.ofClass v) (↑πᵥ ^ k)
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
this : ∀ (d1 d2 : ℕ), (d1 ∣ d ∧ d2 ∣ d ∧ d = d1.lcm d2) = (d = d1.lcm d2)
⊢ (∑ x ∈ n.divisors, ∑ x_1 ∈ n.divisors, if x ∣ d ∧ x_1 ∣ d ∧ d = x.lcm x_1 then f x x_1 d else 0) =
    ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then f d1 d2 d else 0

Tactic:
this

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case neg
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h✝ : ¬n = 1
⊢ (∑ d ∈ n.divisors, weights d) ^ 2 =
    ∑ y ∈ n.divisors, ∑ x ∈ n.divisors, ∑ d2 ∈ n.divisors, if x = y.lcm d2 then weights y * weights d2 else 0

Tactic:
[

Goal state after:
case neg
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h✝ : ¬n = 1
⊢ (∑ d ∈ n.divisors, weights d) ^ 2 =
    ∑ y ∈ n.divisors, ∑ x ∈ n.divisors, ∑ d2 ∈ n.divisors, if x = y.lcm d2 then weights y * weights d2 else 0
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case neg
s : BoundingSieve
d : ℕ
h : ¬d = 0
⊢ (s.nu.pmul (prodPrimeFactors fun p ↦ (1 - s.nu p)⁻¹)) d = s.nu d * ∏ p ∈ d.primeFactors, (1 - s.nu p)⁻¹

Tactic:
ArithmeticFunction.pmul_apply,

Goal state after:
case neg
s : BoundingSieve
d : ℕ
h : ¬d = 0
⊢ s.nu d * (prodPrimeFactors fun p ↦ (1 - s.nu p)⁻¹) d = s.nu d * ∏ p ∈ d.primeFactors, (1 - s.nu p)⁻¹
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ (∑ l ∈ s.prodPrimes.divisors, if l ∣ d then selbergTerms l else 0) =
    ∑ l ∈ s.prodPrimes.divisors, if l ∣ d then selbergTerms (d / l) else 0

Tactic:
[

Goal state after:
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ (∑ l ∈ s.prodPrimes.divisors, if l ∣ d then selbergTerms l else 0) =
    ∑ l ∈ s.prodPrimes.divisors, if l ∣ d then selbergTerms (d / l) else 0
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ (∑ l ∈ s.prodPrimes.divisors, if l ∣ d then selbergTerms (d / l) else 0) =
    selbergTerms d * ∑ l ∈ s.prodPrimes.divisors, if l ∣ d then (selbergTerms l)⁻¹ else 0

Tactic:
[

Goal state after:
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ (∑ l ∈ s.prodPrimes.divisors, if l ∣ d then selbergTerms (d / l) else 0) =
    selbergTerms d * ∑ l ∈ s.prodPrimes.divisors, if l ∣ d then (selbergTerms l)⁻¹ else 0
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case a.a
s : BoundingSieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ s.prodPrimes.divisors
d2 : ℕ
hd2 : d2 ∈ s.prodPrimes.divisors
hgcd_dvd : d1.gcd d2 ∣ s.prodPrimes
⊢ s.nu d1 * w d1 * s.nu d2 * w d2 * (s.nu (d1.gcd d2))⁻¹ =
    ∑ l ∈ s.prodPrimes.divisors, if l ∣ d1.gcd d2 then (selbergTerms l)⁻¹ * (s.nu d1 * w d1) * (s.nu d2 * w d2) else 0

Tactic:
[

Goal state after:
case a.a
s : BoundingSieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ s.prodPrimes.divisors
d2 : ℕ
hd2 : d2 ∈ s.prodPrimes.divisors
hgcd_dvd : d1.gcd d2 ∣ s.prodPrimes
⊢ s.nu d1 * w d1 * s.nu d2 * w d2 * (s.nu (d1.gcd d2))⁻¹ =
    ∑ l ∈ s.prodPrimes.divisors, if l ∣ d1.gcd d2 then (selbergTerms l)⁻¹ * (s.nu d1 * w d1) * (s.nu d2 * w d2) else 0
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
w : ℕ → ℝ
⊢ (∑ l ∈ s.prodPrimes.divisors,
      ∑ d1 ∈ s.prodPrimes.divisors,
        ∑ d2 ∈ s.prodPrimes.divisors,
          if l ∣ d1.gcd d2 then (selbergTerms l)⁻¹ * (s.nu d1 * w d1) * (s.nu d2 * w d2) else 0) =
    ∑ l ∈ s.prodPrimes.divisors,
      (selbergTerms l)⁻¹ * (∑ d ∈ s.prodPrimes.divisors, if l ∣ d then s.nu d * w d else 0) ^ 2

Tactic:
[

Goal state after:
s : BoundingSieve
w : ℕ → ℝ
⊢ (∑ l ∈ s.prodPrimes.divisors,
      ∑ d1 ∈ s.prodPrimes.divisors,
        ∑ d2 ∈ s.prodPrimes.divisors,
          if l ∣ d1.gcd d2 then (selbergTerms l)⁻¹ * (s.nu d1 * w d1) * (s.nu d2 * w d2) else 0) =
    ∑ l ∈ s.prodPrimes.divisors,
      (selbergTerms l)⁻¹ * (∑ d ∈ s.prodPrimes.divisors, if l ∣ d then s.nu d * w d else 0) ^ 2
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
w : ℕ → ℝ
⊢ ∑ x ∈ s.prodPrimes.divisors,
      ∑ x_1 ∈ s.prodPrimes.divisors,
        ∑ a ∈ s.prodPrimes.divisors with x ∣ x_1.gcd a, (selbergTerms x)⁻¹ * (s.nu x_1 * w x_1) * (s.nu a * w a) =
    ∑ x ∈ s.prodPrimes.divisors,
      (selbergTerms x)⁻¹ *
        ((∑ a ∈ s.prodPrimes.divisors with x ∣ a, s.nu a * w a) * ∑ a ∈ s.prodPrimes.divisors with x ∣ a, s.nu a * w a)

Tactic:
sum_mul,

Goal state after:
s : BoundingSieve
w : ℕ → ℝ
⊢ ∑ x ∈ s.prodPrimes.divisors,
      ∑ x_1 ∈ s.prodPrimes.divisors,
        ∑ a ∈ s.prodPrimes.divisors with x ∣ x_1.gcd a, (selbergTerms x)⁻¹ * (s.nu x_1 * w x_1) * (s.nu a * w a) =
    ∑ x ∈ s.prodPrimes.divisors,
      (selbergTerms x)⁻¹ *
        ∑ i ∈ s.prodPrimes.divisors with x ∣ i, s.nu i * w i * ∑ a ∈ s.prodPrimes.divisors with x ∣ a, s.nu a * w a
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: case right
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := max (Real.exp s.re) 1
c₂ : ℝ := max (Real.exp ‖s‖) 1
c₃ : ℝ := max ‖s‖ 1
p : ℕ
hp : p ≠ 0
⊢ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖) ≤ (c₁ * (c₂ * c' * c₃)) ^ p

Tactic:
[

Goal state after:
case right
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := max (Real.exp s.re) 1
c₂ : ℝ := max (Real.exp ‖s‖) 1
c₃ : ℝ := max ‖s‖ 1
p : ℕ
hp : p ≠ 0
⊢ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖) ≤ (c₁ * (c₂ * c' * c₃)) ^ p
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 ^ 2 * (r * p))

Tactic:
sq m,

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)
| ↑(m * m * (r * p))
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 : ℝ
h : ∀ x ∈ (fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1, ‖x‖ ≤ c
⊢ ∃ c ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c ^ p

Tactic:
[

Goal state after:
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
h : ∀ x ∈ (fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1, ‖x‖ ≤ c
⊢ ∃ c ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c ^ p
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))‖ ≤ |max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖| ^ p

Tactic:
[

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.Lindemann.AnalyticalPart

Goal state before:
pp: f : ℤ[X]
hf : eval 0 f ≠ 0
⊢ ∃ c,
    ∀ p > (eval 0 f).natAbs,
      Nat.Prime p →
        ∃ n,
          ¬↑p ∣ n ∧
            ∃ gp,
              gp.natDegree ≤ p * f.natDegree - 1 ∧
                ∀ {r : ℂ}, r ∈ f.aroots ℂ → ‖n • cexp r - p • (aeval r) gp‖ ≤ c ^ p / ↑(p - 1)!

Tactic:
[

Goal state after:
f : ℤ[X]
hf : eval 0 f ≠ 0
⊢ ∃ c,
    ∀ p > (eval 0 f).natAbs,
      Nat.Prime p →
        ∃ n,
          ¬↑p ∣ n ∧
            ∃ gp,
              gp.natDegree ≤ p * f.natDegree - 1 ∧
                ∀ {r : ℂ}, r ∈ f.aroots ℂ → ‖n • cexp r - p • (aeval r) gp‖ ≤ c ^ p / ↑(p - 1)!
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: case hbc
Z : Type u_1
N : Type u_2
R : Type u_3
inst✝ : PseudoMetricSpace R
d : N → ℝ
j : Z → N → R
f : R → R
α : R
ε M : ℝ
d0 : ∀ (a : N), 1 ≤ d a
e0 : 0 < ε
B : ∀ ⦃y : R⦄, y ∈ closedBall α ε → dist (f α) (f y) ≤ dist α y * M
L : ∀ ⦃z : Z⦄ ⦃a : N⦄, j z a ∈ closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))
me0 : 0 < max (1 / ε) M
z : Z
a : N
dm1 : ¬1 ≤ dist α (j z a) * max (1 / ε) M
this : j z a ∈ closedBall α ε
⊢ dist (f α) (f (j z a)) ≤ dist α (j z a) * max (1 / ε) M

Tactic:
refine (B this).trans ?_
      gcongr
      apply le_max_right

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

Goal state before:
pp: case refine_2
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ f.natDegree * |x - ↑a / ↑b|) < 1
b0 : 0 < ↑b
⊢ 1 / A ≤ ↑b ^ f.natDegree * |x - ↑a / ↑b|

Tactic:
lift b to ℕ using zero_le_one.trans b1.le

Goal state after:
case refine_2
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a : ℤ
b : ℕ
b1 : 1 < ↑b
a1 : ↑↑b ^ r * (↑↑b ^ f.natDegree * |x - ↑a / ↑↑b|) < 1
b0 : 0 < ↑↑b
⊢ 1 / A ≤ ↑↑b ^ f.natDegree * |x - ↑a / ↑↑b|
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber

Goal state before:
pp: m : ℕ
hm : 2 ≤ m
⊢ Liouville (liouvilleNumber ↑m)

Tactic:
by
  -- two useful inequalities
  have mZ1 : 1 < (m : ℤ) := by norm_cast
  have m1 : 1 < (m : ℝ) := by norm_cast
  intro n
  -- the first `n` terms sum to `p / m ^ k!`
  rcases partialSum_eq_rat (zero_lt_two.trans_le hm) n with ⟨p, hp⟩
  refine ⟨p, m ^ n !, one_lt_pow₀ mZ1 n.factorial_ne_zero, ?_⟩
  push_cast
  rw [Nat.cast_pow] at hp
  -- separate out the sum of the first `n` terms and the rest
  rw [← partialSum_add_remainder m1 n, ← hp]
  have hpos := remainder_pos m1 n
  simpa [abs_of_pos hpos, hpos.ne'] using @remainder_lt n m (by assumption_mod_cast)

Goal state after:
Module: Mathlib.Topology.Instances.Irrational

Goal state before:
pp: n : ℕ
A : IsClosed (range fun m ↦ (↑n)⁻¹ * ↑m)
m : ℤ
hx : Irrational ((fun m ↦ (↑n)⁻¹ * ↑m) m)
⊢ False

Tactic:
simp at hx

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

Goal state before:
pp: ⊢ IsGδ {x | Liouville x}

Tactic:
rw [setOfPred_liouville_eq_iInter_iUnion]

Goal state after:
⊢ IsGδ (⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b})
Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual

Goal state before:
pp: case refine_1
⊢ {x | Liouville x} ⊆ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)

Tactic:
rw [setOfPred_liouville_eq_iInter_iUnion]

Goal state after:
case refine_1
⊢ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b} ⊆
    ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: R : Type u
inst✝¹⁷ : CommRing R
S : Type v
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Algebra R S
inst✝¹⁴ : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : IsFractionRing S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : Module.Finite R S
inst✝¹ : IsLocalRing S
p : Ideal R
inst✝ : p.IsMaximal
hp0 : p ≠ ⊥
this : FaithfulSMul R S
⊢ p.ramificationIdx' (IsLocalRing.maximalIdeal S) * p.inertiaDeg' (IsLocalRing.maximalIdeal S) = finrank K L

Tactic:
[

Goal state after:
R : Type u
inst✝¹⁷ : CommRing R
S : Type v
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Algebra R S
inst✝¹⁴ : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : IsFractionRing S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : Module.Finite R S
inst✝¹ : IsLocalRing S
p : Ideal R
inst✝ : p.IsMaximal
hp0 : p ≠ ⊥
this : FaithfulSMul R S
⊢ p.ramificationIdx' (IsLocalRing.maximalIdeal S) * p.inertiaDeg' (IsLocalRing.maximalIdeal S) = finrank K L
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: 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
⊢ LiouvilleWith p (x * ↑r)

Tactic:
refine ⟨r.den ^ p * (|r| * C), (tendsto_id.nsmul_atTop r.pos).frequently (hC.mono ?_)⟩

Goal state after:
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
⊢ ∀ (x_1 : ℕ),
    (1 ≤ x_1 ∧ ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < C / ↑x_1 ^ p) →
      ∃ m,
        x * ↑r ≠ ↑m / ↑(r.den • id x_1) ∧
          |x * ↑r - ↑m / ↑(r.den • id x_1)| < ↑r.den ^ p * (↑|r| * C) / ↑(r.den • id x_1) ^ p
Module: Mathlib.NumberTheory.Wilson

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

Tactic:
[

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∏ x, ↑x = -1
Module: Mathlib.Order.Bounded

Goal state before:
pp: α : Type u_1
s : Set α
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
⊢ Unbounded (fun x1 x2 ↦ x1 < x2) s ↔ Unbounded (fun x1 x2 ↦ x1 ≤ x2) s

Tactic:
[

Goal state after:
α : Type u_1
s : Set α
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
⊢ Unbounded (fun x1 x2 ↦ x1 < x2) s ↔ Unbounded (fun x1 x2 ↦ x1 ≤ x2) s
Module: Mathlib.Order.Bounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
H : ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m
a : α
⊢ Unbounded r (s ∩ {b | ¬r b a}) ↔ Unbounded r s

Tactic:
[

Goal state after:
α : Type u_1
r : α → α → Prop
s : Set α
H : ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m
a : α
⊢ Unbounded r (s ∩ {b | ¬r b a}) ↔ Unbounded r s
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:
[

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
Module: Mathlib.Order.Bounds.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
ι : Sort u_2
s : ι → Set α
u : ι → α
hs : ∀ (i : ι), IsLUB (s i) (u i)
c : α
⊢ upperBounds (range u) = upperBounds (⋃ i, s i)

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : Preorder α
ι : Sort u_2
s : ι → Set α
u : ι → α
hs : ∀ (i : ι), IsLUB (s i) (u i)
c : α
⊢ upperBounds (range u) = upperBounds (⋃ i, s i)
Module: Mathlib.Order.Bounds.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
ι : Sort u_2
s : ι → Set α
u : ι → α
hs : ∀ (i : ι), IsGLB (s i) (u i)
c : α
⊢ lowerBounds (range u) = lowerBounds (⋃ i, s i)

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : Preorder α
ι : Sort u_2
s : ι → Set α
u : ι → α
hs : ∀ (i : ι), IsGLB (s i) (u i)
c : α
⊢ lowerBounds (range u) = lowerBounds (⋃ i, s i)
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p x : ℝ
r : ℚ
⊢ LiouvilleWith p (x + ↑r) ↔ LiouvilleWith p x

Tactic:
add_rat_iff

Goal state after:
p x : ℝ
r : ℚ
⊢ LiouvilleWith p x ↔ LiouvilleWith p x
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p x : ℝ
m : ℤ
⊢ LiouvilleWith p (x + ↑↑m) ↔ LiouvilleWith p x

Tactic:
add_rat_iff

Goal state after:
p x : ℝ
m : ℤ
⊢ LiouvilleWith p x ↔ LiouvilleWith p x
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p x : ℝ
n : ℕ
⊢ LiouvilleWith p (x + ↑↑n) ↔ LiouvilleWith p x

Tactic:
add_rat_iff

Goal state after:
p x : ℝ
n : ℕ
⊢ LiouvilleWith p x ↔ LiouvilleWith p x
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p x : ℝ
r : ℚ
⊢ LiouvilleWith p (x + ↑(-r)) ↔ LiouvilleWith p x

Tactic:
add_rat_iff

Goal state after:
p x : ℝ
r : ℚ
⊢ LiouvilleWith p x ↔ LiouvilleWith p x
Module: Mathlib.NumberTheory.WellApproximable

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

Tactic:
[

Goal state after:
A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
han : (orderOf a).Coprime n
⊢ a • approxOrderOf A n δ ⊆ approxOrderOf A (orderOf a * n) δ
Module: Mathlib.NumberTheory.WellApproximable

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

Tactic:
[

Goal state after:
A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : orderOf a ^ 2 ∣ n
⊢ a • approxOrderOf A n δ = approxOrderOf A n δ
Module: Mathlib.Order.Comparable

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ a < b ∨ AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) a b ∨ b < a ∨ IncompRel (fun x1 x2 ↦ x1 ≤ x2) a b

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ a < b ∨ AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) a b ∨ b < a ∨ IncompRel (fun x1 x2 ↦ x1 ≤ x2) 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
a : ι
ha : (∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j a → e j = sSup s j) ∧ (fun {i} x1 x2 ↦ x1 < x2) (e a) (sSup s a)
⊢ False

Tactic:
refine ha.2.not_ge <| sSup_apply_le fun f hf hf' ↦ apply_le_of_toLex (h hf) ?_

Goal state after:
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
a : ι
ha : (∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j a → e j = sSup s j) ∧ (fun {i} x1 x2 ↦ x1 < x2) (e a) (sSup s a)
f : Lex ((i : ι) → (fun i ↦ α i) i)
hf : f ∈ s
hf' : ∀ j < a, f j = sSup s j
⊢ ∀ j < a, f j = e j
Module: Mathlib.Order.Concept

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

Tactic:
[

Goal state after:
α : Type u_2
β : Type u_3
r : α → β → Prop
a : α
b : β
⊢ b ∈ upperPolar r {a} ↔ r a b
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:
[

Goal state after:
α : Type u_2
β : Type u_3
r : α → β → Prop
a : α
b : β
⊢ a ∈ lowerPolar r {b} ↔ r a b
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
s s' : Set α
⊢ IsExtent r s → IsExtent r s' → IsExtent r (s ∩ s')

Tactic:
[

Goal state after:
α : Type u_2
β : Type u_3
r : α → β → Prop
s s' : Set α
⊢ IsExtent r s → IsExtent r s' → IsExtent r (s ∩ s')
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
c : DedekindCut α
⊢ c ≤ principal a ↔ a ∈ c.right

Tactic:
simp only [← intent_subset_intent_iff, right_principal]

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : α
c : DedekindCut α
⊢ Ici a ⊆ c.intent ↔ a ∈ c.right
Module: Mathlib.Order.Concept

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
h : d ≤ c
⊢ upperPolar r c.extent ⊆ upperPolar r d.extent

Tactic:
exact upperPolar_anti _ h

Goal state after:
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : PartialOrder β
f : β ↪o α
A B : DedekindCut β
h : sSup (⇑f '' A.left) ≤ sSup (⇑f '' B.left)
x : β
hx : x ∈ A.extent
⊢ x ∈ B.extent

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : PartialOrder β
f : β ↪o α
A B : DedekindCut β
h : sSup (⇑f '' A.left) ≤ sSup (⇑f '' B.left)
x : β
hx : x ∈ A.extent
⊢ x ∈ B.extent
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : PartialOrder β
f : β ↪o α
A B : DedekindCut β
h : sSup (⇑f '' A.left) ≤ sSup (⇑f '' B.left)
x : β
hx : x ∈ A.extent
⊢ x ∈ lowerBounds B.right

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : PartialOrder β
f : β ↪o α
A B : DedekindCut β
h : sSup (⇑f '' A.left) ≤ sSup (⇑f '' B.left)
x : β
hx : x ∈ A.extent
⊢ x ∈ lowerBounds B.right