mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.ModelTheory.Topology.Types

Goal state before:
pp: case refine_1
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
⊢ (L.lhomWithConstants α).onTheory T ⊆ {φ | T.typesWith φ ∈ F}

Tactic:
intro φ

Goal state after:
case refine_1
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
φ : L[[α]].Sentence
⊢ φ ∈ (L.lhomWithConstants α).onTheory T → φ ∈ {φ | T.typesWith φ ∈ F}
Module: Mathlib.ModelTheory.Topology.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
x : Finset L[[α]].Sentence
hx : ↑x ⊆ {φ | T.typesWith φ ∈ F}
⊢ ∀ φ ∈ x, T.typesWith φ ∈ ↑F

Tactic:
intro φ

Goal state after:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
x : Finset L[[α]].Sentence
hx : ↑x ⊆ {φ | T.typesWith φ ∈ F}
φ : L[[α]].Sentence
⊢ φ ∈ x → T.typesWith φ ∈ ↑F
Module: Mathlib.ModelTheory.Topology.Types

Goal state before:
pp: case refine_2.refine_2
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
⊢ ∀ (φ : L[[α]].Sentence), φ ∈ {φ | T.typesWith φ ∈ F} ∨ Formula.not φ ∈ {φ | T.typesWith φ ∈ F}

Tactic:
intro φ

Goal state after:
case refine_2.refine_2
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
φ : L[[α]].Sentence
⊢ φ ∈ {φ | T.typesWith φ ∈ F} ∨ Formula.not φ ∈ {φ | T.typesWith φ ∈ F}
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: case zero
hn : 0 ≠ 0
⊢ λ 0 = exponent (ZMod 0)ˣ

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: n : ℕ
hn : 3 ≤ n
⊢ 2 * λ (2 ^ n) = φ (2 ^ n)

Tactic:
by
  rw [carmichael_two_pow_of_ne_two, ← pow_succ', totient_prime_pow prime_two] <;>
  · #adaptation_note /-- After https://github.com/leanprover/lean4/pull/13593
    we need to re-enable model-based theory combination in `lia` for this to go through. -/
    lia +mbtc

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: case refine_3
n : ℕ
⊢ ∀ (a b : ℕ),
    1 < a →
      1 < b →
        a.Coprime b →
          ∑ i ∈ a.divisors, Λ i = Real.log ↑a →
            ∑ i ∈ b.divisors, Λ i = Real.log ↑b → ∑ i ∈ (a * b).divisors, Λ i = Real.log ↑(a * b)

Tactic:
intro a

Goal state after:
case refine_3
n a : ℕ
⊢ ∀ (b : ℕ),
    1 < a →
      1 < b →
        a.Coprime b →
          ∑ i ∈ a.divisors, Λ i = Real.log ↑a →
            ∑ i ∈ b.divisors, Λ i = Real.log ↑b → ∑ i ∈ (a * b).divisors, Λ i = Real.log ↑(a * b)
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: case refine_3
n a b : ℕ
ha' : 1 < a
⊢ 1 < b →
    a.Coprime b →
      ∑ i ∈ a.divisors, Λ i = Real.log ↑a →
        ∑ i ∈ b.divisors, Λ i = Real.log ↑b → ∑ i ∈ (a * b).divisors, Λ i = Real.log ↑(a * b)

Tactic:
hb'

Goal state after:
case refine_3
n a b : ℕ
ha' : 1 < a
hb' : 1 < b
⊢ a.Coprime b →
    ∑ i ∈ a.divisors, Λ i = Real.log ↑a →
      ∑ i ∈ b.divisors, Λ i = Real.log ↑b → ∑ i ∈ (a * b).divisors, Λ i = Real.log ↑(a * b)
Module: Mathlib.NumberTheory.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
h : ↑p ∣ a - b
⊢ ↑p ^ (0 + 1) ∣ a ^ p ^ 0 - b ^ p ^ 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Derivative

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

Tactic:
| zero =>

Goal state after:
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case neg.inl
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
h4 : ¬n = 4
hn : Odd n
⊢ ¬∃ x x_1, Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ n = 2 * x ^ x_1

Tactic:
· rintro ⟨p, m, -, -, -, rfl⟩
      simp [← Nat.not_even_iff_odd] at hn

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Exp

Goal state before:
pp: case zero
A : Type u_3
inst✝² : CommRing A
inst✝¹ : Algebra ℚ A
inst✝ : IsAddTorsionFree A
f : A⟦X⟧
hd : (d⁄dX A) f = f
hc : constantCoeff f = 1
⊢ (coeff 0) f = (coeff 0) (exp A)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Exp

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

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: ⊢ eval (1 / 4) (∑ i ∈ range 0, (monomial (3 - i)) (_root_.bernoulli i * ↑(Nat.choose 3 i))) +
            eval (1 / 4) ((monomial (3 - 0)) (_root_.bernoulli 0 * ↑(Nat.choose 3 0))) +
          eval (1 / 4) ((monomial (3 - 1)) (_root_.bernoulli 1 * ↑(Nat.choose 3 1))) +
        eval (1 / 4) ((monomial (3 - 2)) (_root_.bernoulli 2 * ↑(Nat.choose 3 2))) +
      eval (1 / 4) ((monomial (3 - 3)) (_root_.bernoulli 3 * ↑(Nat.choose 3 3))) =
    3 / 64

Tactic:
Polynomial.eval_monomial

Goal state after:
⊢ eval (1 / 4) (∑ i ∈ range 0, (monomial (3 - i)) (_root_.bernoulli i * ↑(Nat.choose 3 i))) +
            _root_.bernoulli 0 * ↑(Nat.choose 3 0) * (1 / 4) ^ (3 - 0) +
          _root_.bernoulli 1 * ↑(Nat.choose 3 1) * (1 / 4) ^ (3 - 1) +
        _root_.bernoulli 2 * ↑(Nat.choose 3 2) * (1 / 4) ^ (3 - 2) +
      _root_.bernoulli 3 * ↑(Nat.choose 3 3) * (1 / 4) ^ (3 - 3) =
    3 / 64
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case zero
⊢ derivative (bernoulli 0) = ↑0 * bernoulli (0 - 1)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case zero
n : ℕ
hd : ∀ m < 0, (bernoulli m).comp (1 + X) = bernoulli m + m • X ^ (m - 1)
⊢ (bernoulli 0).comp (1 + X) = bernoulli 0 + 0 • X ^ (0 - 1)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case zero
⊢ ∑ k ∈ range 0, ↑(Nat.choose 0 k) * bernoulli' k = ↑0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case zero
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ (coeff 0) (bernoulli'PowerSeries A * (exp A - 1)) = (coeff 0) (X * exp A)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case zero
⊢ (bernoulli 0).comp (-X) = (-1) ^ 0 • (bernoulli 0 + 0 • X ^ (0 - 1))

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
hn : n ≠ 1
⊢ bernoulli n = bernoulli' n

Tactic:
by
  cases hn.lt_or_gt with
  | inl hlt => simp [lt_one_iff.mp hlt]
  | inr hgt =>
    cases n.even_or_odd with
    | inl heven => rw [bernoulli, heven.neg_one_pow, one_mul]
    | inr hodd => rw [bernoulli'_eq_zero_of_odd hodd hgt, bernoulli_eq_zero_of_odd hodd hgt]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case zero
⊢ ∑ k ∈ range 0, ↑(Nat.choose 0 k) * bernoulli k = if 0 = 1 then 1 else 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ.zero
⊢ ∑ k ∈ range (0 + 1), ↑((0 + 1).choose k) * bernoulli k = if 0 + 1 = 1 then 1 else 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case zero
⊢ ∑ k ∈ antidiagonal 0, ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli k.1 = if 0 = 0 then 1 else 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case zero
⊢ (bernoulli 0).comp (1 - X) = (-1) ^ 0 * bernoulli 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case zero
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
⊢ (PowerSeries.coeff 0) ((PowerSeries.mk fun n ↦ (aeval t) ((1 / ↑n !) • bernoulli n)) * (exp A - 1)) =
    (PowerSeries.coeff 0) (PowerSeries.X * (rescale t) (exp A))

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case zero
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ (coeff 0) (bernoulliPowerSeries A * (exp A - 1)) = (coeff 0) X

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ.zero
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ (algebraMap ℚ A) (bernoulli (0 + 1) / ((↑0 + 1) * ↑0!)) * ((algebraMap ℚ A) (↑0 + 1)⁻¹ - 1) +
      (algebraMap ℚ A) (∑ x ∈ antidiagonal 0, bernoulli x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹) =
    if 0 + 1 = 1 then 1 else 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case zero
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
h_bdd : (fun n ↦ ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖) =O[atTop] fun x ↦ 1
hf_int : LocallyIntegrableOn (deriv fun t ↦ ‖f t‖) (Set.Ici ↑m) volume
hf :
  ∀ (n : ℕ),
    ∑ k ∈ Icc 0 n, ‖f ↑k‖ * ‖c k‖ =
      ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖ - ∫ (t : ℝ) in Set.Ioc ↑m ↑n, deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖
g : ℝ → ℝ
hg₁ : (fun t ↦ deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖) =O[atTop] g
hg₂ : IntegrableAtFilter g atTop volume
C₁ : ℝ
hC₁ : ∀ (n : ℕ), ‖‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖‖ ≤ C₁
C₂ : ℝ := ∫ (t : ℝ) in Set.Ioi ↑m, ‖deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖‖
⊢ ∑ i ∈ range 0, ‖f ↑i * c i‖ ≤ max (C₁ + C₂) 1

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case zero
n : ℕ
⊢ ∑ k ∈ Ico 1 (n + 1), ↑k ^ 0 = ∑ i ∈ range (0 + 1), bernoulli' i * ↑((0 + 1).choose i) * ↑n ^ (0 + 1 - i) / ↑(succ 0)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : abv.IsAdmissible
this : DecidableEq R
⊢ ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (h.card ε ^ 0).succ → Fin 0 → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin 0), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case hxy
x : ℝ
h : 1 ≤ x
⊢ ↑⌊x⌋₊ ≤ x

Tactic:
· exact floor_le (by positivity)

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

Goal state before:
pp: case zero
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < cardPowDegree b • ε
A : Fin 0 → Fq[X]
⊢ ∃ t, ∀ (i₀ i₁ : Fin 0), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε

Tactic:
| zero =>

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
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
hε : 0 < ε
ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
s : ι →₀ R := bS.repr a
s_eq : ∀ (i : ι), s i = (bS.repr a) i
⊢ ∃ q, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))

Tactic:
let qs : Fin (cardM bS adm).succ → ι → R := fun j i => μ j * s i / b

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
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
hε : 0 < ε
ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
s : ι →₀ R := bS.repr a
s_eq : ∀ (i : ι), s i = (bS.repr a) i
qs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i / b
⊢ ∃ q, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case zero
x : ℝ
⊢ ∑ n ∈ Icc 1 (1 + 6 * 0), b x n =
    b x 1 + ∑ n ∈ Icc 1 (3 * 0), b x (2 * n) + ∑ n ∈ Icc 1 (2 * 0), b x (3 * n) + ∑ n ∈ Icc 1 0, c x n

Tactic:
| zero =>

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

Goal state before:
pp: case zero
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ x.appr 0 < p ^ 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ 1
f : ℝ → ℝ
u : ℝ
x✝ : u ∈ Set.uIcc 2 x
⊢ deriv (fun x ↦ log x) u * f u = f u / u

Tactic:
rw [deriv_log, mul_comm, div_eq_mul_inv]

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

Goal state before:
pp: case zero
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m : ℕ
⊢ p ^ m ∣ x.appr (m + 0) - x.appr m

Tactic:
| zero =>

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

Goal state before:
pp: case zero
p : ℕ
hp_prime : Fact (Nat.Prime p)
⊢ ∀ (x : ℤ_[p]), ↑p ^ 0 ∣ x - ↑(x.appr 0)

Tactic:
| zero =>

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
m : ℤ
hm : ∀ (g_1 : ↥(rootsOfUnity n L)), ((↑g).restrictRootsOfUnity n).toMonoidHom g_1 = g_1 ^ m
⊢ ∃ m, ∀ (t : ↥(rootsOfUnity n L)), g ↑↑t = ↑(↑t ^ m)

Tactic:
exact ⟨m, fun t ↦ Units.ext_iff.1 <| SetCoe.ext_iff.2 <| hm t⟩

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

Goal state before:
pp: case refine_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ∀ (a : ℕ), ↑a ∈ closure (Set.range Int.cast)

Tactic:
intro a

Goal state after:
case refine_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
a : ℕ
⊢ ↑a ∈ closure (Set.range Int.cast)
Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ (𝓞 K)
⊢ Algebra.discr ℤ ⇑b = discr K

Tactic:
let b₀ := Basis.reindex (RingOfIntegers.basis K) (Basis.indexEquiv (RingOfIntegers.basis K) b)
  rw [Algebra.discr_eq_discr (𝓞 K) b b₀, Basis.coe_reindex, Algebra.discr_reindex]

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 : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : ↑ε' < ε
hε'0 : 0 < ε'
N : ℕ
hN : ∀ i ≥ N, padicNormE (mk (nthHomSeq f_compat r) - ↑(↑(nthHomSeq f_compat r) i)) < ε'
n : ℕ
hn : n ≥ N
⊢ ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ↑ε'

Tactic:
change (padicNormE _ : ℝ) < _

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 : ℕ
hn : n ≥ N
⊢ ↑(padicNormE ↑(limNthHom f_compat r - ↑(nthHom f r n))) < ↑ε'
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
⊢ (-1) ^ (Module.finrank K L * (Module.finrank K L - 1) / 2) *
      (Algebra.norm K)
        ((aeval (IsPrimitiveRoot.powerBasis K hζ).gen) (derivative (minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen))) =
    (-1) ^ (φ (p ^ (k + 1)) / 2) * ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))

Tactic:
finrank L hirr,

Goal state after:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
⊢ (-1) ^ (φ (p ^ (k + 1)) * (φ (p ^ (k + 1)) - 1) / 2) *
      (Algebra.norm K)
        ((aeval (IsPrimitiveRoot.powerBasis K hζ).gen) (derivative (minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen))) =
    (-1) ^ (φ (p ^ (k + 1)) / 2) * ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
hg : ∀ (n : ℕ), (toZModPow n).comp g = (toZModPow n).comp g'
x : R
n : ℕ
⊢ (toZModPow n) (g x) = (toZModPow n) (g' x)

Tactic:
change (toZModPow n).comp g x = (toZModPow n).comp g' x

Goal state after:
case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
hg : ∀ (n : ℕ), (toZModPow n).comp g = (toZModPow n).comp g'
x : R
n : ℕ
⊢ ((toZModPow n).comp g) x = ((toZModPow n).comp g') x
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case zero
f : ℕ → ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i
ε : ℚ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
⊢ ↑(p ^ k) ∣ f (k + 0) - f k

Tactic:
| zero =>

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

Goal state before:
pp: case succ
f : ℕ → ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i
ε : ℚ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
n : ℕ
IH : ↑(p ^ k) ∣ f (k + n) - f k
⊢ ↑(p ^ k) ∣ f (k + (n + 1)) - f k

Tactic:
have : (↑(p ^ k) : ℤ) ∣ ↑p ^ (k + n) := ⟨p ^ n, by simp [pow_add]⟩
    simpa using! (this.trans (hi _)).add IH

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

Goal state before:
pp: f : ℕ → ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := ⟨fun x ↦ ↑(f x), ⋯⟩
hs : ↑x = mk s
e : ℤ_[p]
he : x = ↑p ^ n * e + ↑(x.appr n)
N : ℕ
hN : padicNormE (mk s - ↑(↑s (N + n))) < ↑p ^ (-↑n)
⊢ (toZModPow n) x = ↑(f n)

Tactic:
← hs,

Goal state after:
f : ℕ → ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := ⟨fun x ↦ ↑(f x), ⋯⟩
hs : ↑x = mk s
e : ℤ_[p]
he : x = ↑p ^ n * e + ↑(x.appr n)
N : ℕ
hN : padicNormE (↑x - ↑(↑s (N + n))) < ↑p ^ (-↑n)
⊢ (toZModPow n) x = ↑(f n)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case zero
f : ℕ → ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i
n : ℕ
⊢ ↑(f (0 + n)) = ↑(f n)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
⊢ a ≤ a * a

Tactic:
have := @Nat.mul_le_mul_left 1 a a (le_of_lt a1); rwa [mul_one] at this

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

Goal state before:
pp: case e_a
p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
H :
  (Algebra.norm K) ((aeval ζ) (derivative (minpoly K ζ))) * ↑p ^ p ^ k =
    ↑(p ^ (k + 1)) ^ Module.finrank K L * (Algebra.norm K) (ζ ^ (p ^ (k + 1) - 1))
hnorm : (Algebra.norm K) (ζ ^ p ^ k - 1) = ↑p ^ p ^ k
⊢ (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) = ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))

Tactic:
finrank L hirr,

Goal state after:
case e_a
p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
H :
  (Algebra.norm K) ((aeval ζ) (derivative (minpoly K ζ))) * ↑p ^ p ^ k =
    ↑(p ^ (k + 1)) ^ φ (p ^ (k + 1)) * (Algebra.norm K) (ζ ^ (p ^ (k + 1) - 1))
hnorm : (Algebra.norm K) (ζ ^ p ^ k - 1) = ↑p ^ p ^ k
⊢ (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) = ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
C : Poly α → Prop
H1 : ∀ (i : α), C (proj i)
H2 : ∀ (n : ℤ), C (const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f : Poly α
⊢ C f

Tactic:
obtain ⟨f, pf⟩ := f

Goal state after:
α : Type u_1
C : Poly α → Prop
H1 : ∀ (i : α), C (proj i)
H2 : ∀ (n : ℤ), C (const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f : (α → ℕ) → ℤ
pf : IsPoly f
⊢ C ⟨f, pf⟩
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_2
d : ℤ
a : ℤ√d
hgcd : 0 < a.re.gcd a.im
re im : ℤ
H1 : re.gcd im = 1
Hre : a.re = ↑(a.re.gcd a.im) * re
Him : a.im = ↑(a.re.gcd a.im) * im
⊢ IsCoprime { re := re, im := im }.re { re := re, im := im }.im

Tactic:
rw [Int.isCoprime_iff_gcd_eq_one, H1]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
⊢ xz a1 (n + 2) + xz a1 n = ↑(2 * a) * xz a1 (n + 1)

Tactic:
delta xz; rw [← Int.natCast_add, ← Int.natCast_mul, xn_succ_succ]

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

Goal state before:
pp: case pos
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (cyclotomic (2 ^ (0 + 1)) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
⊢ discr K ((fun i ↦ (-1) ^ ↑i) ∘ ⇑e.symm) = 1

Tactic:
show (-1 : L) = algebraMap K L (-1) by simp

Goal state after:
case pos
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (cyclotomic (2 ^ (0 + 1)) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
⊢ discr K ((fun i ↦ (algebraMap K L) (-1) ^ ↑i) ∘ ⇑e.symm) = 1
Module: Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions

Goal state before:
pp: case zero
ξ : ℝ
⊢ (GenContFract.of ξ).convs 0 = ↑(ξ.convergent 0)

Tactic:
| zero =>

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

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

Tactic:
obtain ⟨q', hbd, hden⟩ := exists_rat_abs_sub_le_and_den_le ξ (Nat.cast_pos.mp m_pos)

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

Goal state before:
pp: case zero
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 : ℕ
⊢ xn a1 (j + 4 * n * 0) ≡ xn a1 j [MOD xn a1 n]

Tactic:
| zero =>

Goal state after: