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

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
aux1 : ↑⌊a⌋₊ ≤ a
aux2 : b ≤ ↑⌊b⌋₊ + 1
hb : ⌊a⌋₊ < ⌊b⌋₊
aux3 : a ≤ ↑⌊a⌋₊ + 1
aux4 : ↑⌊a⌋₊ + 1 ≤ b
aux5 : ↑⌊b⌋₊ ≤ b
aux6 : a ≤ ↑⌊b⌋₊
⊢ ∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f ↑k * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊a⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k

Tactic:
simp_rw [← smul_eq_mul, sum_Ioc_by_parts (fun k ↦ f k) _ hb, range_eq_Ico,
    Ico_add_one_right_eq_Icc, smul_eq_mul]

Goal state after:
case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
aux1 : ↑⌊a⌋₊ ≤ a
aux2 : b ≤ ↑⌊b⌋₊ + 1
hb : ⌊a⌋₊ < ⌊b⌋₊
aux3 : a ≤ ↑⌊a⌋₊ + 1
aux4 : ↑⌊a⌋₊ + 1 ≤ b
aux5 : ↑⌊b⌋₊ ≤ b
aux6 : a ≤ ↑⌊b⌋₊
⊢ f ↑⌊b⌋₊ * ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f ↑(⌊a⌋₊ + 1) * ∑ x ∈ Icc 0 ⌊a⌋₊, c x -
      ∑ x ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f ↑(x + 1) - f ↑x) * ∑ x ∈ Icc 0 x, c x =
    f b * ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f a * ∑ x ∈ Icc 0 ⌊a⌋₊, c x - ∫ (x : ℝ) in a..b, deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
i : σ
r : R
n : σ →₀ ℕ
⊢ (coeff (n + single i 1)) (C r) * (↑(n i) + 1) = (coeff n) 0

Tactic:
coeff_add_single_C,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
i : σ
r : R
n : σ →₀ ℕ
⊢ 0 * (↑(n i) + 1) = (coeff n) 0
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case inr.inr.inr
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
h2n : ¬2 ∣ n
this : Nat.Coprime 4 n
⊢ ¬IsCyclic ((ZMod 4)ˣ × (ZMod n)ˣ)

Tactic:
Group.isCyclic_prod_iff

Goal state after:
case inr.inr.inr
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
h2n : ¬2 ∣ n
this : Nat.Coprime 4 n
⊢ ¬(IsCyclic (ZMod 4)ˣ ∧ IsCyclic (ZMod n)ˣ ∧ (Nat.card (ZMod 4)ˣ).Coprime (Nat.card (ZMod n)ˣ))
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: m n : ℕ
hm : Odd m
hm1 : m ≠ 1
hn : Odd n
hn1 : n ≠ 1
hmn : m.Coprime n
x✝¹ : NeZero m
x✝ : NeZero n
e : (ZMod (m * n))ˣ ≃* (ZMod m)ˣ × (ZMod n)ˣ :=
  (Units.mapEquiv (chineseRemainder hmn).toMulEquiv).trans MulEquiv.prodUnits
⊢ ¬IsCyclic ((ZMod m)ˣ × (ZMod n)ˣ)

Tactic:
Group.isCyclic_prod_iff

Goal state after:
m n : ℕ
hm : Odd m
hm1 : m ≠ 1
hn : Odd n
hn1 : n ≠ 1
hmn : m.Coprime n
x✝¹ : NeZero m
x✝ : NeZero n
e : (ZMod (m * n))ˣ ≃* (ZMod m)ˣ × (ZMod n)ˣ :=
  (Units.mapEquiv (chineseRemainder hmn).toMulEquiv).trans MulEquiv.prodUnits
⊢ ¬(IsCyclic (ZMod m)ˣ ∧ IsCyclic (ZMod n)ˣ ∧ (Nat.card (ZMod m)ˣ).Coprime (Nat.card (ZMod n)ˣ))
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case neg.inr.inl
n : ℕ
h0 : ¬2 * n = 0
h1 : ¬2 * n = 1
h2 : ¬2 * n = 2
h4 : ¬2 * n = 4
hn✝ : Even (2 * n)
hn : Odd n
p m : ℕ
odd : Odd p
eq : 2 * n = p ^ m
this : Odd (2 * n)
⊢ False

Tactic:
simp [← Nat.not_even_iff_odd] at this

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

Goal state before:
pp: case e_a
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
h : ↑n ! = 0
⊢ False

Tactic:
apply factorial_ne_zero n

Goal state after:
case e_a
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
h : ↑n ! = 0
⊢ n ! = 0
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n p : ℕ
⊢ eval (↑n) (bernoulli p.succ) - _root_.bernoulli p.succ = (↑p + 1) * ∑ k ∈ range n, ↑k ^ p

Tactic:
sum_range_pow_eq_bernoulli_sub

Goal state after:
n p : ℕ
⊢ eval (↑n) (bernoulli p.succ) - _root_.bernoulli p.succ = eval (↑n) (bernoulli p.succ) - _root_.bernoulli p.succ
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p ↦ bernoulli p / ↑p !) * PowerSeries.mk fun q ↦ (coeff (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
this :
  (PowerSeries.mk fun p ↦ ∑ k ∈ range n, ↑k ^ p * (algebraMap ℚ ℚ) (↑p !)⁻¹) =
    PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
⊢ ∑ i ∈ range n, ↑i ^ p * (↑p !)⁻¹ =
    ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!

Tactic:
rw [PowerSeries.ext_iff] at this

Goal state after:
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p ↦ bernoulli p / ↑p !) * PowerSeries.mk fun q ↦ (coeff (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
this :
  ∀ (n_1 : ℕ),
    (coeff n_1) (PowerSeries.mk fun p ↦ ∑ k ∈ range n, ↑k ^ p * (algebraMap ℚ ℚ) (↑p !)⁻¹) =
      (coeff n_1)
        (PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!)
⊢ ∑ i ∈ range n, ↑i ^ p * (↑p !)⁻¹ =
    ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: n : ℕ
hn0 : n ≠ 0
⊢ ∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n

Tactic:
rcases lt_or_ge 511 n with h | h
  -- If `n` is large, apply the lemma derived from the inequalities on the central binomial
  -- coefficient.
  · exact exists_prime_lt_and_le_two_mul_eventually n h
  replace h : n < 521 := h.trans_lt (by norm_num1)
  revert h
  -- For small `n`, supply a list of primes to cover the initial cases.
  open Lean Elab Tactic in
  run_tac do
    for i in [317, 163, 83, 43, 23, 13, 7, 5, 3, 2] do
      let i : Term := quote i
      evalTactic <| ←
        `(tactic| refine exists_prime_lt_and_le_two_mul_succ $i (by norm_num1) (by norm_num1) ?_)
  exact fun h2 => ⟨2, prime_two, h2, Nat.mul_le_mul_left 2 (Nat.pos_of_ne_zero hn0)⟩

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (deriv fun t ↦ ‖f t‖) (Set.Ici 1) volume
h_bdd : (fun n ↦ ‖f ↑n‖ * ∑ k ∈ Icc 1 n, ‖c k‖) =O[atTop] fun x ↦ 1
g : ℝ → ℝ
hg₁ : (fun t ↦ deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 1 ⌊t⌋₊, ‖c k‖) =O[atTop] g
hg₂ : IntegrableAtFilter g atTop volume
n x✝ : ℕ
h : x✝ ∈ Icc 1 n
⊢ ‖c x✝‖ = ‖if x✝ = 0 then 0 else c x✝‖

Tactic:
if_neg (zero_lt_one.trans_le (mem_Icc.mp h).1).ne'

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (deriv fun t ↦ ‖f t‖) (Set.Ici 1) volume
h_bdd : (fun n ↦ ‖f ↑n‖ * ∑ k ∈ Icc 1 n, ‖c k‖) =O[atTop] fun x ↦ 1
g : ℝ → ℝ
hg₁ : (fun t ↦ deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 1 ⌊t⌋₊, ‖c k‖) =O[atTop] g
hg₂ : IntegrableAtFilter g atTop volume
n x✝ : ℕ
h : x✝ ∈ Icc 1 n
⊢ ‖c x✝‖ = ‖c x✝‖
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_1
n p : ℕ
hp : Prime p
this : 1 < p
⊢ ((Icc 1 n).sup fun a ↦ (id a).factorization p) ≤ log p n

Tactic:
simp only [Finset.sup_le_iff, mem_Icc, and_imp]
    exact fun m _ h ↦ le_log_of_pow_le this (le_of_dvd (by grind) (ordProj_dvd m p) |>.trans h)

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
n : ℕ
hn : n ∈ Set.Ici 1
⊢ ∀ ⦃b : ℕ⦄, b ∈ Set.Ici 1 → n ≤ b → Chebyshev.b x b ≤ Chebyshev.b x n

Tactic:
m

Goal state after:
x : ℝ
hx : 0 ≤ x
n : ℕ
hn : n ∈ Set.Ici 1
m : ℕ
⊢ m ∈ Set.Ici 1 → n ≤ m → b x m ≤ b x n
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ∃! n, n < p ∧ x - ↑n ∈ maximalIdeal ℤ_[p]

Tactic:
by
  obtain ⟨n, hn₁, hn₂⟩ := exists_mem_range x
  use n, ⟨hn₁, hn₂⟩, fun m ⟨hm₁, hm₂⟩ ↦ ?_
  have := (zmod_congr_of_sub_mem_max_ideal x n m hn₂ hm₂).symm
  rwa [ZMod.natCast_eq_natCast_iff, ModEq, mod_eq_of_lt hn₁, mod_eq_of_lt hm₁] at this

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

Goal state before:
pp: case refine_2
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
inst✝¹ : IsDedekindDomain S
inst✝ : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ∏ m ∈ finsetApprox bS adm, m
hM : (algebraMap R S) M ≠ 0
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
b_min : ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0
J : Ideal S
hJ : Ideal.span {(algebraMap R S) M} * ↑I = Ideal.span {b} * J
⊢ ∃ x y, ∃ (_ : x ≠ 0) (_ : y ≠ 0), Ideal.span {x} * ↑I = Ideal.span {y} * ↑⟨J, ⋯⟩

Tactic:
exact ⟨algebraMap _ _ M, b, hM, b_ne_zero, hJ⟩

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

Goal state before:
pp: case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ x.appr (m + k) - x.appr m
h : ¬x - ↑(x.appr (m + k)) = 0
⊢ p ^ m ∣
    p ^ (m + k) * (toZMod (↑(unitCoeff h) * ↑p ^ (↑(x - ↑(x.appr (m + k))).valuation - (↑m + ↑k)).natAbs)).val +
        x.appr (m + k) -
      x.appr m

Tactic:
add_tsub_assoc_of_le (appr_mono _ (Nat.le_add_right m k))

Goal state after:
case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ x.appr (m + k) - x.appr m
h : ¬x - ↑(x.appr (m + k)) = 0
⊢ p ^ m ∣
    p ^ (m + k) * (toZMod (↑(unitCoeff h) * ↑p ^ (↑(x - ↑(x.appr (m + k))).valuation - (↑m + ↑k)).natAbs)).val +
      (x.appr (m + k) - x.appr m)
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
this : ∀ (x : Fin pb.dim), ↑x + 1 ≤ pb.dim
⊢ n = pb.dim

Tactic:
rw [← AlgHom.card K L E, ← Fintype.card_fin pb.dim]

Goal state after:
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
this : ∀ (x : Fin pb.dim), ↑x + 1 ≤ pb.dim
⊢ Fintype.card (L →ₐ[K] E) = Fintype.card (Fin pb.dim)
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
⊢ discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis =
    (-1) ^ (φ (p ^ (k + 1)) / 2) * ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))

Tactic:
discr_powerBasis_eq_norm,

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) ^ (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))
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
⊢ g x = g' x

Tactic:
apply ext_of_toZModPow.mp

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) (g x) = (toZModPow n) (g' x)
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℤ
⊢ AddCommGroup (ℤ√d)

Tactic:
refine
  { sub := fun a b => a + -b
    nsmul := @nsmulRec (ℤ√d) ⟨0⟩ ⟨(· + ·)⟩
    zsmul := @zsmulRec (ℤ√d) ⟨0⟩ ⟨(· + ·)⟩ ⟨Neg.neg⟩ (@nsmulRec (ℤ√d) ⟨0⟩ ⟨(· + ·)⟩)
    add_assoc := ?_
    zero_add := ?_
    add_zero := ?_
    neg_add_cancel := ?_
    add_comm := ?_ } <;>
  intros <;>
  ext

Goal state after:
case refine_1.re
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝ + b✝ + c✝).re = (a✝ + (b✝ + c✝)).re

case refine_1.im
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝ + b✝ + c✝).im = (a✝ + (b✝ + c✝)).im

case refine_2.re
d : ℤ
a✝ : ℤ√d
⊢ (0 + a✝).re = a✝.re

case refine_2.im
d : ℤ
a✝ : ℤ√d
⊢ (0 + a✝).im = a✝.im

case refine_3.re
d : ℤ
a✝ : ℤ√d
⊢ (a✝ + 0).re = a✝.re

case refine_3.im
d : ℤ
a✝ : ℤ√d
⊢ (a✝ + 0).im = a✝.im

case refine_4.re
d : ℤ
a✝ : ℤ√d
⊢ (-a✝ + a✝).re = re 0

case refine_4.im
d : ℤ
a✝ : ℤ√d
⊢ (-a✝ + a✝).im = im 0

case refine_5.re
d : ℤ
a✝ b✝ : ℤ√d
⊢ (a✝ + b✝).re = (b✝ + a✝).re

case refine_5.im
d : ℤ
a✝ b✝ : ℤ√d
⊢ (a✝ + b✝).im = (b✝ + a✝).im
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
by
  rw [sub_eq_add_neg, ← mul_neg]
  exact congr_arg Zsqrtd.re (pellZd_sub a1 h)

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

Goal state before:
pp: case mp.re
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
hb : -(d * (z.im * z.im)) = 0
⊢ z.re * z.re = 0

Tactic:
exact ha

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

Goal state before:
pp: case succ
d : ℕ
a : ℤ√↑d
x y : ℕ
h✝ : a ≤ { re := ↑x, im := ↑(y + 1) }
h : ∀ (y : ℕ), SqLe y d (d * y) 1
⊢ { re := ↑x + ↑d * ↑(y + 1) - ↑x, im := 0 - ↑(y + 1) }.Nonneg

Tactic:
show (x : ℤ) + d * Nat.succ y - x = d * Nat.succ y by simp

Goal state after:
case succ
d : ℕ
a : ℤ√↑d
x y : ℕ
h✝ : a ≤ { re := ↑x, im := ↑(y + 1) }
h : ∀ (y : ℕ), SqLe y d (d * y) 1
⊢ { re := ↑d * ↑y.succ, im := 0 - ↑(y + 1) }.Nonneg
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: ⊢ factoredNumbers ∅ = {1}

Tactic:
by
  ext m
  simp only [mem_factoredNumbers, Finset.notMem_empty, ← List.eq_nil_iff_forall_not_mem,
    primeFactorsList_eq_nil, and_or_left, not_and_self_iff, ne_and_eq_iff_right zero_ne_one,
    false_or, Set.mem_singleton_iff]

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: case refine_1
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
s : Finset ℕ
hs : s ∈ k.primesBelow.powerset
m : ℕ
hm : n = m ^ 2 * s.prod id
this : m ^ 2 * s.prod id ≠ 0
⊢ m ≠ 0

Tactic:
simp only [ne_eq, _root_.mul_eq_zero, sq_eq_zero_iff, not_or] at this

Goal state after:
case refine_1
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
s : Finset ℕ
hs : s ∈ k.primesBelow.powerset
m : ℕ
hm : n = m ^ 2 * s.prod id
this : ¬m = 0 ∧ ¬s.prod id = 0
⊢ m ≠ 0
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case refine_1
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
hu₁ : u - ⌊ξ⌋ * v ≤ v
huv_cop : IsCoprime (u - ⌊ξ⌋ * v) v
hf : u - ⌊ξ⌋ * v = 0
⊢ False

Tactic:
rw [hf] at huv_cop

Goal state after:
case refine_1
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
hu₁ : u - ⌊ξ⌋ * v ≤ v
huv_cop : IsCoprime 0 v
hf : u - ⌊ξ⌋ * v = 0
⊢ False
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case refine_2
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
hu₁ : u - ⌊ξ⌋ * v ≤ v
huv_cop : IsCoprime (u - ⌊ξ⌋ * v) v
hf : u - ⌊ξ⌋ * v = v
⊢ False

Tactic:
rw [hf] at huv_cop

Goal state after:
case refine_2
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
hu₁ : u - ⌊ξ⌋ * v ≤ v
huv_cop : IsCoprime v v
hf : u - ⌊ξ⌋ * v = v
⊢ False
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:

Tactic:
n ^ k ≤ n ^ w := Nat.pow_le_pow_right hn kw
        _ < (w + 1) ^ w := Nat.pow_lt_pow_left (Nat.lt_succ_of_le nw) wpos.ne'
        _ ≤ a := xn_ge_a_pow w1 w

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

Goal state before:
pp: case h.inr.inl
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
h : ContfracLegendre.Ass ξ u ↑1
⊢ ∃ n, ↑u / ↑1 = ξ.convergent n

Tactic:
rw [Nat.cast_one, div_one]
    obtain ⟨_, h₁, h₂⟩ := h
    rcases le_or_gt (u : ℝ) ξ with ht | ht
    · use 0
      rw [convergent_zero, Rat.intCast_inj, eq_comm, floor_eq_iff]
      convert! And.intro ht (sub_lt_iff_lt_add'.mp (abs_lt.mp h₂).2) <;> norm_num
    · replace h₁ := lt_sub_iff_add_lt'.mp (h₁ rfl)
      have hξ₁ : ⌊ξ⌋ = u - 1 := by
        rw [floor_eq_iff, cast_sub, cast_one, sub_add_cancel]
        exact ⟨(((sub_lt_sub_iff_left _).mpr one_half_lt_one).trans h₁).le, ht⟩
      rcases eq_or_ne ξ ⌊ξ⌋ with Hξ | Hξ
      · rw [Hξ, hξ₁, cast_sub, cast_one, ← sub_eq_add_neg, sub_lt_sub_iff_left] at h₁
        exact False.elim (lt_irrefl _ <| h₁.trans one_half_lt_one)
      · have hξ₂ : ⌊(fract ξ)⁻¹⌋ = 1 := by
          rw [floor_eq_iff, cast_one, le_inv_comm₀ zero_lt_one (fract_pos.mpr Hξ), inv_one,
            one_add_one_eq_two, inv_lt_comm₀ (fract_pos.mpr Hξ) zero_lt_two]
          refine ⟨(fract_lt_one ξ).le, ?_⟩
          rw [fract, hξ₁, cast_sub, cast_one, lt_sub_iff_add_lt', sub_add]
          convert! h₁ using 1
          rw [sub_eq_add_neg]
          norm_num
        use 1
        simp [convergent, hξ₁, hξ₂, cast_sub, cast_one]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case refine_2
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ ‖π‖ * ‖↑n ^ 2‖ * ‖ContinuousLinearMap.snd ℂ ℂ ℂ‖ ≤ π * ↑|n| ^ 2

Tactic:
norm_of_nonneg pi_pos.le,

Goal state after:
case refine_2
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ π * ‖↑n ^ 2‖ * ‖ContinuousLinearMap.snd ℂ ℂ ℂ‖ ≤ π * ↑|n| ^ 2
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: n : ℤ
z τ : ℂ
this : ‖(jacobiTheta₂_term_fderiv n z τ) (0, 1)‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
⊢ π * ↑|n| ^ 2 = ‖π‖ * ‖I‖ * ‖↑n ^ 2‖

Tactic:
norm_of_nonneg pi_pos.le,

Goal state after:
n : ℤ
z τ : ℂ
this : ‖(jacobiTheta₂_term_fderiv n z τ) (0, 1)‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
⊢ π * ↑|n| ^ 2 = π * ‖I‖ * ‖↑n ^ 2‖
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : x < 1
this : 1 < 1 / x
⊢ (P.ε * ↑(x ^ P.k)) • P.g x - P.f₀ + 0 = (P.ε * ↑(x ^ P.k)) • (0 + (P.g x - (P.ε⁻¹ * ↑(x ^ P.k)⁻¹) • P.f₀))

Tactic:
match_scalars <;> field [(rpow_pos_of_pos hx P.k).ne', P.hε]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
h : Summable fun x ↦ jacobiTheta₂_term_fderiv x z τ
this✝ : Summable fun x ↦ ‖jacobiTheta₂_term_fderiv x z τ‖
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 ≤ ↑|n| ^ 2

Tactic:
rw [one_le_sq_iff_one_le_abs, ← Int.cast_abs, abs_abs, ← Int.cast_one, Int.cast_le]

Goal state after:
z τ : ℂ
h : Summable fun x ↦ jacobiTheta₂_term_fderiv x z τ
this✝ : Summable fun x ↦ ‖jacobiTheta₂_term_fderiv x z τ‖
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 ≤ |n|
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
h : Summable fun x ↦ jacobiTheta₂'_term x z τ
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 ≤ (2 * π)⁻¹ * (‖2‖ * ‖π‖ * ‖↑n‖)

Tactic:
norm_of_nonneg pi_pos.le,

Goal state after:
z τ : ℂ
h : Summable fun x ↦ jacobiTheta₂'_term x z τ
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 ≤ (2 * π)⁻¹ * (‖2‖ * π * ‖↑n‖)
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
i : ι
⊢ a' i = 0 ∨ 0 < p i

Tactic:
simp only [a']

Goal state after:
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
i : ι
⊢ (if p i = 0 then 0 else a i) = 0 ∨ 0 < p i
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a' i * ↑(rexp (-π * p i * t))) (F t)
i : ι
⊢ ‖‖a' i‖ / p i ^ s.re‖ ≤ ‖a i‖ / p i ^ s.re

Tactic:
simp only [a']

Goal state after:
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a' i * ↑(rexp (-π * p i * t))) (F t)
i : ι
⊢ ‖‖if p i = 0 then 0 else a i‖ / p i ^ s.re‖ ≤ ‖a i‖ / p i ^ s.re