mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
r : R
f : MvPowerSeries σ R
⊢ pderivFun i (C r * f) = r • pderivFun i f

Tactic:
smul_eq_C_mul,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
r : R
f : MvPowerSeries σ R
⊢ pderivFun i (C r * f) = C r * pderivFun i f
Module: Mathlib.RingTheory.PowerSeries.Derivative

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n : ℕ
ih : ∀ (k : ℕ), (coeff k) ((⇑(d⁄dX R))^[n] f) = ↑((k + 1).ascFactorial n) * (coeff (k + n)) f
k : ℕ
⊢ (coeff k) ((⇑(d⁄dX R))^[n + 1] f) = ↑((k + 1).ascFactorial (n + 1)) * (coeff (k + (n + 1))) f

Tactic:
rw [Function.iterate_succ_apply', coeff_derivative, ih, Nat.ascFactorial_succ,
      ← Nat.succ_ascFactorial]

Goal state after:
case succ
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n : ℕ
ih : ∀ (k : ℕ), (coeff k) ((⇑(d⁄dX R))^[n] f) = ↑((k + 1).ascFactorial n) * (coeff (k + n)) f
k : ℕ
⊢ ↑((k + 1 + 1).ascFactorial n) * (coeff (k + 1 + n)) f * (↑k + 1) =
    ↑((k + 1) * (k + 1).succ.ascFactorial n) * (coeff (k + (n + 1))) f
Module: Mathlib.RingTheory.PowerSeries.Exp

Goal state before:
pp: A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
k : ℕ
⊢ exp A ^ k = (rescale ↑k) (exp A)

Tactic:
induction k with
  | zero =>
    simp only [rescale_zero, constantCoeff_exp, Function.comp_apply, map_one, cast_zero,
      pow_zero (exp A), coe_comp]
  | succ k h =>
    simpa only [succ_eq_add_one, cast_add, ← exp_mul_exp_eq_exp_add (k : A), ← h, cast_one,
      id_apply, rescale_one] using pow_succ (exp A) k

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case succ
k : ℕ
⊢ derivative (bernoulli (k + 1)) = ↑(k + 1) * bernoulli (k + 1 - 1)

Tactic:
| succ k =>

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
this :
  ↑(n + 1) * ∑ x ∈ range n, Rat.divInt (↑(n.choose x)) (Int.subNatNat n x + 1) * bernoulli' x =
    ∑ x ∈ range n, ↑(n.succ.choose x) * bernoulli' x
⊢ ∑ x ∈ range n, ↑((n + 1).choose x) * bernoulli' x +
      ↑((n + 1).choose n) * (1 - ∑ x ∈ range n, Rat.divInt (↑(n.choose x)) (Int.subNatNat n x + 1) * bernoulli' x) =
    ↑(n + 1)

Tactic:
← this

Goal state after:
n : ℕ
this :
  ↑(n + 1) * ∑ x ∈ range n, Rat.divInt (↑(n.choose x)) (Int.subNatNat n x + 1) * bernoulli' x =
    ∑ x ∈ range n, ↑(n.succ.choose x) * bernoulli' x
⊢ ↑(n + 1) * ∑ x ∈ range n, Rat.divInt (↑(n.choose x)) (Int.subNatNat n x + 1) * bernoulli' x +
      ↑((n + 1).choose n) * (1 - ∑ x ∈ range n, Rat.divInt (↑(n.choose x)) (Int.subNatNat n x + 1) * bernoulli' x) =
    ↑(n + 1)
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 1
hgt : 1 < n
⊢ bernoulli n = bernoulli' n

Tactic:
| inr hgt =>

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
⊢ ∀ x ∈ range (n + 1),
    (algebraMap ℚ A) ↑(n + 1)! *
        ((PowerSeries.coeff x) (PowerSeries.mk fun n ↦ (aeval t) ((1 / ↑n !) • bernoulli n)) *
          ((PowerSeries.coeff (n + 1 - x)) (exp A) - (PowerSeries.coeff (n + 1 - x)) 1)) =
      (aeval t) (↑((n + 1).choose x) • bernoulli x)

Tactic:
intro i hi

Goal state after:
case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
i : ℕ
hi : i ∈ range (n + 1)
⊢ (algebraMap ℚ A) ↑(n + 1)! *
      ((PowerSeries.coeff i) (PowerSeries.mk fun n ↦ (aeval t) ((1 / ↑n !) • bernoulli n)) *
        ((PowerSeries.coeff (n + 1 - i)) (exp A) - (PowerSeries.coeff (n + 1 - i)) 1)) =
    (aeval t) (↑((n + 1).choose i) • bernoulli i)
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n p : ℕ
f : ℕ → ℚ := fun i ↦ bernoulli i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
f' : ℕ → ℚ := fun i ↦ bernoulli' i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
hle : 1 ≤ n + 1
hne : ↑p + 1 + 1 ≠ 0
h1 : ∀ (r : ℚ), r * (↑p + 1 + 1) * ↑n ^ p.succ / (↑p + 1 + 1) = r * ↑n ^ p.succ
h2 : f 1 + ↑n ^ p.succ = 1 / 2 * ↑n ^ p.succ
this :
  ∑ i ∈ range p, bernoulli (i + 2) * ↑((p + 2).choose (i + 2)) * ↑n ^ (p - i) / ↑(p + 2) =
    ∑ i ∈ range p, bernoulli' (i + 2) * ↑((p + 2).choose (i + 2)) * ↑n ^ (p - i) / ↑(p + 2)
⊢ ∑ k ∈ range n, ↑k ^ p.succ + ↑n ^ p.succ = ∑ i ∈ range p.succ.succ, f i + ↑n ^ p.succ

Tactic:
by simp [f, sum_range_pow]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ Monotone ψ

Tactic:
intro x y hxy
  apply sum_le_sum_of_subset_of_nonneg
  · exact Ioc_subset_Ioc (by rfl) (by gcongr)
  · simp

Goal state after:
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : EuclideanDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
T : Type u_6
inst✝² : Ring T
inst✝¹ : LinearOrder T
inst✝ : IsStrictOrderedRing T
a : S
y : T
hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y
i : ι
him : (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).Nonempty
y' : ℤ := (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).max' him
y'_def : y' = (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).max' him
hy' : ∀ (k : ι), abv ((bS.repr a) k) ≤ y'
⊢ ∀ (y_1 : T), (∃ a_1, (∃ a_2 ∈ Finset.univ, abv ((bS.repr a) a_2) = a_1) ∧ ↑a_1 = y_1) → y_1 < y

Tactic:
rintro _ ⟨x, ⟨k, -, rfl⟩, rfl⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : EuclideanDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
T : Type u_6
inst✝² : Ring T
inst✝¹ : LinearOrder T
inst✝ : IsStrictOrderedRing T
a : S
y : T
hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y
i : ι
him : (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).Nonempty
y' : ℤ := (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).max' him
y'_def : y' = (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).max' him
hy' : ∀ (k : ι), abv ((bS.repr a) k) ≤ y'
k : ι
⊢ ↑(abv ((bS.repr a) k)) < y
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : cardPowDegree (x - y) < a
hyz : cardPowDegree (y - z) < a
ha : 0 < a
hxy' : ¬x = y
hyz' : ¬y = z
hxz' : ¬x = z
⊢ cardPowDegree (x - z) < a

Tactic:
← Ne,

Goal state after:
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : cardPowDegree (x - y) < a
hyz : cardPowDegree (y - z) < a
ha : 0 < a
hxy' : x ≠ y
hyz' : y ≠ z
hxz' : x ≠ z
⊢ cardPowDegree (x - z) < a
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ ↑n * log 2 - log (↑n + 1) ≤ ψ ↑n

Tactic:
rw [tsub_le_iff_left, psi_eq_log_lcmUpto, ← log_pow 2,
    ← log_mul (by positivity) (by simp [lcmUpto_ne_zero])]
  exact log_le_log (by positivity) <| mod_cast two_pow_le_mul_lcmUpto n

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
N₁ : ℕ
h1 : ∀ N ≥ N₁, ψ (x ^ (↑1)⁻¹) = ∑ k ∈ Icc 1 N, b x (1 * k)
N₂ : ℕ
h2 : ∀ N ≥ N₂, ψ (x ^ (↑2)⁻¹) = ∑ k ∈ Icc 1 N, b x (2 * k)
N₃ : ℕ
h3 : ∀ N ≥ N₃, ψ (x ^ (↑3)⁻¹) = ∑ k ∈ Icc 1 N, b x (3 * k)
N₅ : ℕ
h5 : ∀ N ≥ N₅, ψ (x ^ (↑5)⁻¹) = ∑ k ∈ Icc 1 N, b x (5 * k)
N₇ : ℕ
h7 : ∀ N ≥ N₇, ψ (x ^ (↑7)⁻¹) = ∑ k ∈ Icc 1 N, b x (7 * k)
N : ℕ := N₁ + N₂ + N₃ + N₅ + N₇
⊢ ψ x - θ x ≤ ψ (x ^ 2⁻¹) + ψ (x ^ 3⁻¹) + ψ (x ^ 5⁻¹) ∧ ψ (x ^ 2⁻¹) + ψ (x ^ 3⁻¹) + ψ (x ^ 7⁻¹) ≤ ψ x - θ x

Tactic:
specialize h1 (1 + 6 * N) (by lia)

Goal state after:
x : ℝ
hx : 0 ≤ x
N₁ N₂ : ℕ
h2 : ∀ N ≥ N₂, ψ (x ^ (↑2)⁻¹) = ∑ k ∈ Icc 1 N, b x (2 * k)
N₃ : ℕ
h3 : ∀ N ≥ N₃, ψ (x ^ (↑3)⁻¹) = ∑ k ∈ Icc 1 N, b x (3 * k)
N₅ : ℕ
h5 : ∀ N ≥ N₅, ψ (x ^ (↑5)⁻¹) = ∑ k ∈ Icc 1 N, b x (5 * k)
N₇ : ℕ
h7 : ∀ N ≥ N₇, ψ (x ^ (↑7)⁻¹) = ∑ k ∈ Icc 1 N, b x (7 * k)
N : ℕ := N₁ + N₂ + N₃ + N₅ + N₇
h1 : ψ (x ^ (↑1)⁻¹) = ∑ k ∈ Icc 1 (1 + 6 * N), b x (1 * k)
⊢ ψ x - θ x ≤ ψ (x ^ 2⁻¹) + ψ (x ^ 3⁻¹) + ψ (x ^ 5⁻¹) ∧ ψ (x ^ 2⁻¹) + ψ (x ^ 3⁻¹) + ψ (x ^ 7⁻¹) ≤ ψ x - θ x
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
⊢ ↑r.num - ↑r.num * (↑r.den * ↑(r.den.gcdA p)) = 0

Tactic:
← this

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
⊢ ↑r.num - ↑r.num * ↑(r.den.gcd p) = 0
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ (√x - 2) / log 2 ^ 2 + ∫ (x : ℝ) in √x..x, 1 / log x ^ 2 ≤ 4 * x / log x ^ 2 + √x / log 2 ^ 2

Tactic:
integral_1_div_log_sq_le sqrt_le_x (by linarith)

Goal state after:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ (√x - 2) / log 2 ^ 2 + (x - √x) / log √x ^ 2 ≤ 4 * x / log x ^ 2 + √x / log 2 ^ 2
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Fintype ι
b : ι → B
f : B ≃ₐ[A] C
i✝ j✝ : ι
⊢ (trace A B) (b i✝ * b j✝) = (trace A C) (f (b i✝ * b j✝))

Tactic:
trace_eq_of_algEquiv

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case neg.inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)
x : ℤ_[p]
h : ¬x - ↑(x.appr n) = 0
c : ℤ_[p]
hc : x - ↑(x.appr n) = ↑p ^ n * c
hc' : c ≠ 0
hc0 : c.valuation ≠ 0
⊢ ↑p ∣ c

Tactic:
unitCoeff_spec hc'

Goal state after:
case neg.inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)
x : ℤ_[p]
h : ¬x - ↑(x.appr n) = 0
c : ℤ_[p]
hc : x - ↑(x.appr n) = ↑p ^ n * c
hc' : c ≠ 0
hc0 : c.valuation ≠ 0
⊢ ↑p ∣ ↑(unitCoeff hc') * ↑p ^ c.valuation
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
a✝ : 4 ≤ x
t : ℝ
x✝ : t ∈ Set.Icc 2 x
ht : 2 ≤ t
right✝ : t ≤ x
⊢ 0 ≤ θ t / (t * log t ^ 2)

Tactic:
by positivity [theta_nonneg t]

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g : L ≃+* L
c : ZMod (Nat.card ↥(rootsOfUnity n L))
hc : ∀ (t : ↥(rootsOfUnity n L)), g ↑↑t = ↑(↑t ^ c.val)
⊢ c = χ₀ n g

Tactic:
apply IsCyclic.ext rfl (fun ζ ↦ ?_)
  specialize hc ζ
  suffices ((ζ ^ c.val : Lˣ) : L) = (ζ ^ (χ₀ n g).val : Lˣ) by exact_mod_cast this
  rw [← toFun_spec g ζ, hc]

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ (↑(x.appr n)).cast = 0 ↔ ↑(x.appr m) = 0

Tactic:
rw [ZMod.cast_natCast (pow_dvd_pow p h),
    zmod_congr_of_sub_mem_span m (x.appr n) (x.appr n) (x.appr m)]

Goal state after:
case ha
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ↑(x.appr n) - ↑(x.appr n) ∈ Ideal.span {↑p ^ m}

case hb
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ↑(x.appr n) - ↑(x.appr m) ∈ Ideal.span {↑p ^ m}
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case inr.inr
n : ℕ
h : 1 < n
⊢ ↑n * log 2 - log (↑n + 1) ≤ ↑(π n) * log ↑n

Tactic:
← psi_le_primeCounting_mul_log,

Goal state after:
case inr.inr
n : ℕ
h : 1 < n
⊢ ↑n * log 2 - log (↑n + 1) ≤ ψ ↑n
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
r : R
i j : ℕ
h : i ≤ j
f_compat : (ZMod.castHom ⋯ (ZMod (p ^ i))).comp (f j) = f i
⊢ ↑(nthHom f r j) - ↑(nthHom f r i) = 0

Tactic:
dsimp [nthHom]

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
r : R
i j : ℕ
h : i ≤ j
f_compat : (ZMod.castHom ⋯ (ZMod (p ^ i))).comp (f j) = f i
⊢ ↑↑((f j) r).val - ↑↑((f i) r).val = 0
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: case pos.refine_2
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk' : k ≠ 0
hk : ↑p ^ (-↑k) < ε
σ : Gal(L/K)
hσ : σ ∈ id ((fun g ↦ g.carrier) K⟮ζ k⟯.fixingSubgroup)
i : ℕ
hi : i < p ^ k
ht : ⋯.unit ^ i ∈ rootsOfUnity (p ^ k) L
⊢ ((MulSemiringAction.toRingAut Gal(L/K) L) σ) ↑(⋯.unit ^ i) = ↑(⋯.unit ^ i) ^ ZMod.val 1

Tactic:
ZMod.val_one'',

Goal state after:
case pos.refine_2
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk' : k ≠ 0
hk : ↑p ^ (-↑k) < ε
σ : Gal(L/K)
hσ : σ ∈ id ((fun g ↦ g.carrier) K⟮ζ k⟯.fixingSubgroup)
i : ℕ
hi : i < p ^ k
ht : ⋯.unit ^ i ∈ rootsOfUnity (p ^ k) L
⊢ ((MulSemiringAction.toRingAut Gal(L/K) L) σ) ↑(⋯.unit ^ i) = ↑(⋯.unit ^ i) ^ 1

case pos.refine_2
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk' : k ≠ 0
hk : ↑p ^ (-↑k) < ε
σ : Gal(L/K)
hσ : σ ∈ id ((fun g ↦ g.carrier) K⟮ζ k⟯.fixingSubgroup)
i : ℕ
hi : i < p ^ k
ht : ⋯.unit ^ i ∈ rootsOfUnity (p ^ k) L
⊢ p ^ k ≠ 1
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
hj : j ≥ n
⊢ ↑(nthHom f (r + s) j - (nthHom f r j + nthHom f s j)) = 0

Tactic:
dsimp [nthHom]

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
hj : j ≥ n
⊢ ↑(↑((f j) (r + s)).val - (↑((f j) r).val + ↑((f j) s).val)) = 0
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
hj : j ≥ n
⊢ ((f j) r).cast + ((f j) s).cast - (((f j) r).cast + ((f j) s).cast) = 0

Tactic:
simp only [sub_self]

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
hj : j ≥ n
⊢ ↑(nthHom f (r * s) j - nthHom f r j * nthHom f s j) = 0

Tactic:
dsimp [nthHom]

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
hj : j ≥ n
⊢ ↑(↑((f j) (r * s)).val - ↑((f j) r).val * ↑((f j) s).val) = 0
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : ↑ε' < ε
hε'0 : 0 < ε'
⊢ ∃ N, ∀ n ≥ N, ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε

Tactic:
obtain ⟨N, hN⟩ := padicNormE.defn (nthHomSeq f_compat r) hε'0

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : ↑ε' < ε
hε'0 : 0 < ε'
N : ℕ
hN : ∀ i ≥ N, padicNormE (mk (nthHomSeq f_compat r) - ↑(↑(nthHomSeq f_compat r) i)) < ε'
⊢ ∃ N, ∀ n ≥ N, ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
h : d a1 = n * n
this : n * n + 1 = a * a
⊢ n * n < a * a

Tactic:
← this

Goal state after:
a : ℕ
a1 : 1 < a
n : ℕ
h : d a1 = n * n
this : n * n + 1 = a * a
⊢ n * n < n * n + 1
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝² x✝¹ : Poly α
x✝ : α → ℕ
⊢ x✝² x✝ + x✝¹ x✝ = x✝¹ x✝ + x✝² x✝

Tactic:
add_comm

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
⊢ yz a1 (m - n) = yz a1 m * xz a1 n + xz a1 m * -yz a1 n

Tactic:
add_comm

Goal state after:
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
⊢ yz a1 (m - n) = xz a1 m * -yz a1 n + yz a1 m * xz a1 n
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
⊢ yz a1 (m - n) = xz a1 m * -yz a1 n + yz a1 m * xz a1 n

Tactic:
exact congr_arg Zsqrtd.im (pellZd_sub a1 h)

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case h₂
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD yn a1 n ^ 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]
L : xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD yn a1 n ^ 2]
this : k * xn a1 n ^ (k - 1) * yn a1 n * xn a1 n = k * xn a1 n ^ k * yn a1 n
⊢ yn a1 (n * k) * xn a1 n ≡ k * xn a1 n ^ k * yn a1 n [MOD yn a1 n ^ 3]

Tactic:
← this

Goal state after:
case h₂
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD yn a1 n ^ 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]
L : xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD yn a1 n ^ 2]
this : k * xn a1 n ^ (k - 1) * yn a1 n * xn a1 n = k * xn a1 n ^ k * yn a1 n
⊢ yn a1 (n * k) * xn a1 n ≡ k * xn a1 n ^ (k - 1) * yn a1 n * xn a1 n [MOD yn a1 n ^ 3]
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
a : ℤ√↑d
⊢ (a - a).Nonneg

Tactic:
simp only [sub_self]

Goal state after:
d : ℕ
a : ℤ√↑d
⊢ Nonneg 0
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ 2 * n
jn : n ≤ j
this : 2 * n - j + j ≤ n + j
t : xn a1 j + xn a1 (2 * n - j) ≡ 0 [MOD xn a1 n]
⊢ xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n]

Tactic:
add_comm

Goal state after:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ 2 * n
jn : n ≤ j
this : 2 * n - j + j ≤ n + j
t : xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n]
⊢ xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n]
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
⊢ 0 ≡ xn a1 j + xn a1 (2 * n + j) [MOD xn a1 n]

Tactic:
add_comm

Goal state after:
a : ℕ
a1 : 1 < a
n j : ℕ
⊢ 0 ≡ xn a1 (2 * n + j) + xn a1 j [MOD xn a1 n]
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
⊢ 0 ≡ xn a1 j + xn a1 (2 * n - j) [MOD xn a1 n]

Tactic:
add_comm

Goal state after:
a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
⊢ 0 ≡ xn a1 (2 * n - j) + xn a1 j [MOD xn a1 n]
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH :
  List.Forall Dioph l →
    ∃ β pl, ∀ (v : α → ℕ), List.Forall (fun S ↦ v ∈ S) l ↔ ∃ t, List.Forall (fun p ↦ p (v ⊗ t) = 0) pl
d : List.Forall Dioph (S :: l)
dl : List.Forall Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.Forall (fun S ↦ v ∈ S) l ↔ ∃ t, List.Forall (fun p ↦ p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ :
  ∃ t,
    p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0 ∧
      List.Forall ((fun p ↦ p (v ⊗ t) = 0) ∘ fun q ↦ Poly.map (inl ⊗ inr ∘ inr) q) pl
t : β ⊕ γ → ℕ
hl : p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0
hr : List.Forall ((fun p ↦ p (v ⊗ t) = 0) ∘ fun q ↦ Poly.map (inl ⊗ inr ∘ inr) q) pl
⊢ List.Forall (fun p ↦ p (v ⊗ t ∘ inr) = 0) pl

Tactic:
refine List.Forall.imp (fun q hq => ?_) hr; dsimp [Function.comp_def] at hq
                rwa [show
                    (fun x : α ⊕ γ => (v ⊗ t) ((inl ⊗ fun x : γ => inr (inr x)) x)) =
                      v ⊗ t ∘ inr
                    from funext fun s => by rcases s with a | b <;> rfl] at hq

Goal state after:
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : d < 0
this : a.re * a.re = 0
⊢ a.re = re 0 ∧ a.im = im 0

Tactic:
rw [eq_zero_of_mul_self_eq_zero this] at ha ⊢

Goal state after:
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : 0 * 0 = d * a.im * a.im
h : d < 0
this : a.re * a.re = 0
⊢ 0 = re 0 ∧ a.im = im 0
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
hξ : Irrational ξ
q : ℚ
h : 0 < |ξ - ↑q|
m : ℕ
hm : 1 / |ξ - ↑q| < ↑m
⊢ ∃ q', |ξ - ↑q'| < 1 / ↑q'.den ^ 2 ∧ |ξ - ↑q'| < |ξ - ↑q|

Tactic:
have m_pos : (0 : ℝ) < m := (one_div_pos.mpr h).trans hm

Goal state after:
ξ : ℝ
hξ : Irrational ξ
q : ℚ
h : 0 < |ξ - ↑q|
m : ℕ
hm : 1 / |ξ - ↑q| < ↑m
m_pos : 0 < ↑m
⊢ ∃ q', |ξ - ↑q'| < 1 / ↑q'.den ^ 2 ∧ |ξ - ↑q'| < |ξ - ↑q|
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case succ
a : ℕ
a1 : 1 < a
i j✝ n : ℕ
ipos : 0 < i
hin : i ≤ n
h : xn a1 j✝ ≡ xn a1 i [MOD xn a1 n]
j' : ℕ := j✝ % (4 * n)
n4 : 0 < 4 * n
jl : j' < 4 * n
jj : j✝ ≡ j' [MOD 4 * n]
j q : ℕ
IH : xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]
⊢ xn a1 (j + 4 * n * q + 4 * n) ≡ xn a1 j [MOD xn a1 n]

Tactic:
add_comm

Goal state after:
case succ
a : ℕ
a1 : 1 < a
i j✝ n : ℕ
ipos : 0 < i
hin : i ≤ n
h : xn a1 j✝ ≡ xn a1 i [MOD xn a1 n]
j' : ℕ := j✝ % (4 * n)
n4 : 0 < 4 * n
jl : j' < 4 * n
jj : j✝ ≡ j' [MOD 4 * n]
j q : ℕ
IH : xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]
⊢ xn a1 (4 * n + (j + 4 * n * q)) ≡ xn a1 j [MOD xn a1 n]
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case right
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |ξ * ↑q.den - ↑q.num| < 1 / ↑q.den
h₁ : ξ * ↑q.den < 1 + ↑q.num
h₂ : ↑q.num < 1 + ξ * ↑q.den
⊢ ⌈ξ * ↑q.den⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * ↑q.den⌋ + 1

Tactic:
add_comm

Goal state after:
case right
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |ξ * ↑q.den - ↑q.num| < 1 / ↑q.den
h₁ : ξ * ↑q.den < ↑q.num + 1
h₂ : ↑q.num < ξ * ↑q.den + 1
⊢ ⌈ξ * ↑q.den⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * ↑q.den⌋ + 1
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℚ
f : ℚ → ℤ × ℕ := fun q ↦ (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
hinj : Function.Injective f
H : f '' s ⊆ ⋃ y ∈ Ioc 0 ξ.den, Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}
⊢ s.Finite

Tactic:
refine (Finite.subset ?_ H).of_finite_image hinj.injOn

Goal state after:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q ↦ (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
hinj : Function.Injective f
H : f '' s ⊆ ⋃ y ∈ Ioc 0 ξ.den, Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}
⊢ (⋃ y ∈ Ioc 0 ξ.den, Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}).Finite
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case succ
n : ℕ
ih : convergent 0 n = 0
⊢ convergent 0 (n + 1) = 0

Tactic:
simp only [ih, convergent_succ, floor_zero, cast_zero, fract_zero, add_zero, inv_zero]

Goal state after: