mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : Countable α
inst✝¹ : DenselyOrdered β
inst✝ : Nontrivial β
⊢ Nonempty (α ↪o β)

Tactic:
by
  cases nonempty_encodable α
  rcases exists_pair_lt β with ⟨x, y, hxy⟩
  obtain ⟨a, ha⟩ := exists_between hxy
  have : Nonempty (Set.Ioo x y) := ⟨⟨a, ha⟩⟩
  let our_ideal : Ideal (PartialIso α _) :=
    idealOfCofinals default (definedAtLeft (Set.Ioo x y))
  let F a := funOfIdeal a our_ideal (cofinal_meets_idealOfCofinals _ _ a)
  refine
    ⟨RelEmbedding.trans (OrderEmbedding.ofStrictMono (fun a ↦ (F a).val) fun a₁ a₂ ↦ ?_)
        (OrderEmbedding.subtype _)⟩
  rcases (F a₁).prop with ⟨f, hf, ha₁⟩
  rcases (F a₂).prop with ⟨g, hg, ha₂⟩
  rcases our_ideal.directed _ hf _ hg with ⟨m, _hm, fm, gm⟩
  exact (lt_iff_lt_of_cmp_eq_cmp <| m.prop (a₁, _) (fm ha₁) (a₂, _) (gm ha₂)).mp

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case mpr
L : Language
M : Type w
inst✝ : L.Structure M
M_CG : Structure.CG L M
⊢ L.IsExtensionPair M M → L.IsUltrahomogeneous M

Tactic:
intro h S S_FG f
    let ⟨g, ⟨dom_le_dom, eq⟩⟩ :=
      equiv_between_cg M_CG M_CG ⟨⟨S, f.toHom.range, f.equivRange⟩, S_FG⟩ h h
    use g
    simp only [Embedding.subtype_equivRange] at eq
    rw [← eq]
    ext
    rfl

Goal state after:
Module: Mathlib.ModelTheory.Topology.Types

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

Tactic:
rw[Theory.IsFinitelySatisfiable]
      intro x hx
      have : ∀ φ ∈ x, T.typesWith φ ∈ F.toFilter := by intro φ hφ; exact hx hφ
      rw [← Filter.biInter_finset_mem x] at this
      obtain ⟨T, T_inter⟩ := F.neBot.nonempty_of_mem this
      have subset : (x : Set _) ⊆ T.toTheory := by rwa [Set.mem_iInter₂] at T_inter
      exact T.isMaximal.1.mono subset

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
m n : ℕ
t : ℝ
h : Set.Ico ?m.55 ?m.56 t = Set.Icc ?m.55 ?m.56 t
ht : t ∈ Set.Icc (↑n) (↑n + 1)
⊢ ∑ k ∈ Icc m ⌊t⌋₊, c k = ∑ k ∈ Icc m n, c k

Tactic:
Nat.floor_eq_on_Ico _ _ (h.mpr ht)

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
m n : ℕ
t : ℝ
h : Set.Ico (↑n) (↑n + 1) t = Set.Icc (↑n) (↑n + 1) t
ht : t ∈ Set.Icc (↑n) (↑n + 1)
⊢ ∑ k ∈ Icc m n, c k = ∑ k ∈ Icc m n, c k
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = ↑p * u * v * b
i : ℕ
hi : ¬i = p ∧ ¬i = 1 ∧ ¬i = 0 ∧ i < p + 1
hi' : 2 ≤ i
⊢ u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * ↑(p.choose i) = u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * ↑(p * (p.choose i / p))

Tactic:
rw [Nat.mul_div_cancel' (hp.dvd_choose_self hi.2.2.1 <| by lia)]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: ⊢ bernoulli' 0 = 1

Tactic:
rw [bernoulli'_def]

Goal state after:
⊢ 1 - ∑ k ∈ range 0, ↑(Nat.choose 0 k) / (↑0 - ↑k + 1) * bernoulli' k = 1
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: ⊢ bernoulli' 1 = 1 / 2

Tactic:
rw [bernoulli'_def]

Goal state after:
⊢ 1 - ∑ k ∈ range 1, ↑(Nat.choose 1 k) / (↑1 - ↑k + 1) * bernoulli' k = 1 / 2
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: ⊢ bernoulli' 2 = 1 / 6

Tactic:
rw [bernoulli'_def]

Goal state after:
⊢ 1 - ∑ k ∈ range 2, ↑(Nat.choose 2 k) / (↑2 - ↑k + 1) * bernoulli' k = 1 / 6
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: ⊢ bernoulli' 3 = 0

Tactic:
rw [bernoulli'_def]

Goal state after:
⊢ 1 - ∑ k ∈ range 3, ↑(Nat.choose 3 k) / (↑3 - ↑k + 1) * bernoulli' k = 0
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: this : Nat.choose 4 2 = 6
⊢ bernoulli' 4 = -1 / 30

Tactic:
rw [bernoulli'_def]

Goal state after:
this : Nat.choose 4 2 = 6
⊢ 1 - ∑ k ∈ range 4, ↑(Nat.choose 4 k) / (↑4 - ↑k + 1) * bernoulli' k = -1 / 30
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
cases n with | zero => simp | succ n =>
  cases n with
  | zero => simp
  | succ n =>
  suffices (∑ i ∈ range n, ↑((n + 2).choose (i + 2)) * bernoulli (i + 2)) = n / 2 by
    simp only [this, sum_range_succ', cast_succ, bernoulli_one, bernoulli_zero, choose_one_right,
      mul_one, choose_zero_right, cast_zero, if_false, zero_add, succ_succ_ne_one]
    ring
  have f := sum_bernoulli' n.succ.succ
  simp_rw [sum_range_succ', cast_succ, ← eq_sub_iff_add_eq] at f
  refine Eq.trans ?_ (Eq.trans f ?_)
  · congr
    funext x
    rw [bernoulli_eq_bernoulli'_of_ne_one (succ_ne_zero x ∘ succ.inj)]
  · simp only [mul_one, bernoulli'_zero, choose_zero_right,
      zero_add, choose_one_right, cast_succ, bernoulli'_one]
    ring

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
⊢ Squarefree (n#)

Tactic:
by
  rw [primorial_eq_prod_primesLE]
  refine Finset.squarefree_prod_of_pairwise_isCoprime (fun _ hp _ hq hpq ↦ ?_)
    fun _ hp ↦ (prime_of_mem_primesLE hp).squarefree
  simp only [← coprime_iff_isRelPrime]
  exact (coprime_primes (prime_of_mem_primesLE hp) (prime_of_mem_primesLE hq)).mpr hpq

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

Goal state before:
pp: case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff (b.natDegree - ↑j.succ)
this✝ : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj✝ : b.natDegree - d ≤ j
hbj✝ : ↑j < ↑b.natDegree
hbj : j < b.natDegree
hj : b.natDegree - j.succ < d
this : j = b.natDegree - (b.natDegree - j.succ).succ
⊢ (A i₁).coeff j = (A i₀).coeff j

Tactic:
convert! congr_fun i_eq.symm ⟨natDegree b - j.succ, hj⟩

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

Goal state before:
pp: Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]
hbε : 0 < cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < ↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
this : ↑(A i₁ % b - A i₀ % b).natDegree < ↑b.natDegree + log ε / log ↑(Fintype.card Fq)
⊢ ↑(A i₁ % b - A i₀ % b).natDegree < (↑b.natDegree * log ↑(Fintype.card Fq) + log ε) / log ↑(Fintype.card Fq)

Tactic:
add_div,

Goal state after:
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]
hbε : 0 < cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < ↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
this : ↑(A i₁ % b - A i₀ % b).natDegree < ↑b.natDegree + log ε / log ↑(Fintype.card Fq)
⊢ ↑(A i₁ % b - A i₀ % b).natDegree <
    ↑b.natDegree * log ↑(Fintype.card Fq) / log ↑(Fintype.card Fq) + log ε / log ↑(Fintype.card Fq)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ (∑ x ∈ Icc 1 N ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) with
      match x with
      | (k, p) => p ≤ ⌊x ^ (↑k)⁻¹⌋₊,
      match x with
      | (k, p) => f (p ^ k)) =
    ∑ k ∈ Icc 1 N, ∑ p ∈ Ioc 0 ⌊x ^ (1 / ↑k)⌋₊ with Nat.Prime p, f (p ^ k)

Tactic:
rw [sum_filter, sum_product]
    refine sum_congr rfl fun k _ ↦ ?_
    simp only [sum_ite, not_le, sum_const_zero, add_zero]
    congr 1
    ext p
    simp only [mem_filter, mem_Ioc]
    refine ⟨fun _ ↦ (by simp_all), fun h ↦ ?_⟩
    simp_all only [mem_Icc, one_div, true_and, and_true]
    grw [h.1.2, floor_le_floor]
    apply rpow_le_self_of_one_le _ (by bound)
    have := one_le_floor_iff _ |>.mp <| le_trans (one_le_cast.mp h.2.one_le) h.1.2
    contrapose! this
    apply rpow_lt_one hx this (by bound)

Goal state after:
Module: Mathlib.NumberTheory.FunctionField

Goal state before:
pp: case mp
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
Ft : Type u_3
inst✝⁷ : Field Ft
inst✝⁶ : Algebra F[X] Ft
inst✝⁵ : IsFractionRing F[X] Ft
inst✝⁴ : Algebra F⟮X⟯ K
inst✝³ : Algebra Ft K
inst✝² : Algebra F[X] K
inst✝¹ : IsScalarTower F[X] Ft K
inst✝ : IsScalarTower F[X] F⟮X⟯ K
e : F⟮X⟯ ≃ₐ[F[X]] Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
this : ∀ (c : F⟮X⟯) (x : K), e c • x = c • x
h : FunctionField F K
b : Module.Basis (Fin (Module.finrank F⟮X⟯ K)) F⟮X⟯ K := Module.finBasis F⟮X⟯ K
⊢ FiniteDimensional Ft K

Tactic:
exact (b.mapCoeffs e this).finiteDimensional_of_finite

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ x - ↑x.zmodRepr ∈ maximalIdeal ℤ_[p]

Tactic:
exact sub_zmodRepr_mem _

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ ∀ (x : ℤ_[p]), x - ↑x.zmodRepr ∈ Ideal.span {↑p}

Tactic:
← maximalIdeal_eq_span_p

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ ∀ (x : ℤ_[p]), x - ↑x.zmodRepr ∈ maximalIdeal ℤ_[p]
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑p} → x - ↑b ∈ Ideal.span {↑p} → ↑a = ↑b

Tactic:
← maximalIdeal_eq_span_p

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ maximalIdeal ℤ_[p] → x - ↑b ∈ maximalIdeal ℤ_[p] → ↑a = ↑b
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: 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 : ↑(unitCoeff h) * ↑p ^ (x - ↑(x.appr n)).valuation = c * ↑p ^ n
hc' : c ≠ 0
hc0 : c.valuation = 0
this : c = ↑(unitCoeff h)
⊢ c - (toZMod c).cast ∈ Ideal.span {↑p}

Tactic:
← maximalIdeal_eq_span_p

Goal state after:
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 : ↑(unitCoeff h) * ↑p ^ (x - ↑(x.appr n)).valuation = c * ↑p ^ n
hc' : c ≠ 0
hc0 : c.valuation = 0
this : c = ↑(unitCoeff h)
⊢ c - (toZMod c).cast ∈ maximalIdeal ℤ_[p]
Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs

Goal state before:
pp: b : Basis (Fin 1) ℤ (𝓞 ℚ) := (Basis.singleton (Fin 1) ℤ).map ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm
⊢ discr ℚ = Algebra.discr ℤ ⇑b

Tactic:
by convert! (discr_eq_discr ℚ b).symm

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

Goal state before:
pp: n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ✝ : IsPrimitiveRoot μ n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
h✝ : Irreducible (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n
h : ∃ i < n, zeta n K L ^ i = μ
pf✝¹ : h.choose.Coprime n
hμ : IsPrimitiveRoot (zeta n K L ^ (↑(ZMod.unitOfCoprime h.choose pf✝¹)).val) n
pf✝ : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K hμ).gen
⊢ (IsPrimitiveRoot.powerBasis K hμ).gen = μ

Tactic:
hμ.powerBasis_gen K

Goal state after:
n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ✝ : IsPrimitiveRoot μ n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
h✝ : Irreducible (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n
h : ∃ i < n, zeta n K L ^ i = μ
pf✝¹ : h.choose.Coprime n
hμ : IsPrimitiveRoot (zeta n K L ^ (↑(ZMod.unitOfCoprime h.choose pf✝¹)).val) n
pf✝ : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K hμ).gen
⊢ zeta n K L ^ (↑(ZMod.unitOfCoprime h.choose pf✝¹)).val = μ
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
pn : xz a1 n * xz a1 n - ↑(d a1) * yz a1 n * yz a1 n = 1 := pell_eqz a1 n
⊢ ↑(xn a1 n) * ↑(xn a1 n) - ↑(d a1 * yn a1 n * yn a1 n) = 1

Tactic:
exact pn

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

Goal state before:
pp: c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
⊢ SqLe z c w d

Tactic:
by
  apply le_of_not_gt
  intro l
  refine not_le_of_gt ?_ h
  simp only [mul_add, mul_comm, mul_left_comm, add_assoc]
  have hm := sqLe_add_mixed zw (le_of_lt l)
  simp only [SqLe, mul_assoc] at l zw
  grw [zw, hm]
  gcongr

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

Goal state before:
pp: d : ℤ
x : ℤ√d
h : IsUnit x
y : ℤ√d
hy : 1 = x * y
this : (Int.natAbs ∘ norm) 1 = (Int.natAbs ∘ norm) (x * y)
⊢ x.norm.natAbs = 1

Tactic:
rw [Function.comp_apply, Function.comp_apply, norm_mul, Int.natAbs_mul, norm_one,
      Int.natAbs_one, eq_comm, mul_eq_one] at this

Goal state after:
d : ℤ
x : ℤ√d
h : IsUnit x
y : ℤ√d
hy : 1 = x * y
this : x.norm.natAbs = 1 ∧ y.norm.natAbs = 1
⊢ x.norm.natAbs = 1
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case inl.inr.inr.refine_1
d x y : ℕ
ha : { re := ↑x, im := ↑y }.Nonneg
z w : ℕ
hb : { re := -↑z, im := ↑w }.Nonneg
i : ℕ
h : { re := ↑x, im := ↑y }.re + { re := -↑z, im := ↑w }.re = -↑i
⊢ i ≤ z

pp: case inl.inr.inr.refine_2
d x y : ℕ
ha : { re := ↑x, im := ↑y }.Nonneg
z w : ℕ
hb : { re := -↑z, im := ↑w }.Nonneg
i : ℕ
h : { re := ↑x, im := ↑y }.re + { re := -↑z, im := ↑w }.re = -↑i
⊢ w ≤ y + w

Tactic:
· dsimp only at h
      exact Int.ofNat_le.1 (le_of_neg_le_neg (Int.le.intro x (by simp [add_comm, *])))

Goal state after:
case inl.inr.inr.refine_2
d x y : ℕ
ha : { re := ↑x, im := ↑y }.Nonneg
z w : ℕ
hb : { re := -↑z, im := ↑w }.Nonneg
i : ℕ
h : { re := ↑x, im := ↑y }.re + { re := -↑z, im := ↑w }.re = -↑i
⊢ w ≤ y + w
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
simp [_root_.pow_succ, mul_comm, mul_left_comm]

Goal state after:
a : ℕ
a1 : 1 < a
y n : ℕ
⊢ ↑y * (↑y * ↑y ^ n) - ↑a * (↑y * ↑y ^ n * 2) + ↑y ^ n = -(↑y ^ n * (↑a * (↑y * 2) - ↑y * ↑y - 1))
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb : b.Nonneg
x y z w : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
x✝ : { re := ↑z, im := ↑w }.Nonneg
⊢ ({ re := -↑x, im := ↑y } * { re := ↑z, im := ↑w }).Nonneg

Tactic:
by
    rw [mul_comm]; exact nonneg_mul_lem ha

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

Goal state before:
pp: d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb : b.Nonneg
x y z w : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
x✝ : { re := ↑z, im := ↑w }.Nonneg
⊢ ({ re := ↑x, im := -↑y } * { re := ↑z, im := ↑w }).Nonneg

Tactic:
by
    rw [mul_comm]; exact nonneg_mul_lem ha

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Duality

Goal state before:
pp: M : Type u_1
R : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : CommRing R
inst✝² : Finite M
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
inst✝ : Nontrivial R
a : M
ha : a ≠ 1
hu : ¬IsUnit a
⊢ 1 a ≠ 1

Tactic:
simpa only [map_nonunit _ hu] using zero_ne_one

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Duality

Goal state before:
pp: M : Type u_1
R : Type u_2
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : Finite M
inst✝ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
H : Subgroup Mˣ
χ : MulChar M R
⊢ χ ∈ OrderDual.ofDual ((subgroupOrderIsoSubgroupMulChar M R) H) ↔ ∀ m ∈ H, χ ↑m = 1

Tactic:
subgroupOrderIsoSubgroupMulChar,

Goal state after:
M : Type u_1
R : Type u_2
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : Finite M
inst✝ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
H : Subgroup Mˣ
χ : MulChar M R
⊢ χ ∈
      OrderDual.ofDual
        (((CommGroup.subgroupOrderIsoSubgroupMonoidHom Mˣ R).trans mulEquivToUnitHom.symm.mapSubgroup.dual) H) ↔
    ∀ m ∈ H, χ ↑m = 1
Module: Mathlib.NumberTheory.MulChar.Duality

Goal state before:
pp: M : Type u_1
R : Type u_2
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : Finite M
inst✝ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
H : Subgroup Mˣ
⊢ Nat.card ↥(OrderDual.ofDual ((subgroupOrderIsoSubgroupMulChar M R) H)) = Nat.card (Mˣ ⧸ H)

Tactic:
subgroupOrderIsoSubgroupMulChar,

Goal state after:
M : Type u_1
R : Type u_2
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : Finite M
inst✝ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
H : Subgroup Mˣ
⊢ Nat.card
      ↥(OrderDual.ofDual
          (((CommGroup.subgroupOrderIsoSubgroupMonoidHom Mˣ R).trans mulEquivToUnitHom.symm.mapSubgroup.dual) H)) =
    Nat.card (Mˣ ⧸ H)
Module: Mathlib.NumberTheory.DirichletCharacter.Orthogonality

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
⊢ Nat.card (DirichletCharacter R n) = Nat.card (ZMod n)ˣ

Tactic:
exact Nat.card_congr (mulEquiv_units R n).some.toEquiv

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: case right
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e m : ℕ
hm₀ : m ≠ 0
hm : ∀ p ∈ m.primeFactorsList, p ∈ s
hpm : ¬p ∣ m
⊢ (List.filter (fun x ↦ decide (x ∈ s)) (p ^ e * m).primeFactorsList).prod = m

Tactic:
conv_rhs => rw [← prod_primeFactorsList hm₀]
      refine prod_eq <|
        (filter _ <| perm_primeFactorsList_mul (pow_ne_zero e hp.ne_zero) hm₀).trans ?_
      rw [filter_append, hp.primeFactorsList_pow, filter_eq_nil_iff.mpr <| by grind, nil_append,
        filter_eq_self.mpr <| by grind]

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

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h : |ξ - (↑u' + ↑⌊ξ⌋ * ↑v) / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
⊢ |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹

Tactic:
add_div,

Goal state after:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h : |ξ - (↑u' / ↑v + ↑⌊ξ⌋ * ↑v / ↑v)| < (↑v * (2 * ↑v - 1))⁻¹
⊢ |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h : -(↑v * (2 * ↑v - 1))⁻¹ < ξ - (↑u' + ↑⌊ξ⌋ * ↑v) / ↑v
this : (2 * ↑v - 1) * (-(↑v * (2 * ↑v - 1))⁻¹ + ↑u' / ↑v) = 2 * ↑u' - (1 + ↑u') / ↑v
⊢ 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ

Tactic:
add_div,

Goal state after:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h : -(↑v * (2 * ↑v - 1))⁻¹ < ξ - (↑u' / ↑v + ↑⌊ξ⌋ * ↑v / ↑v)
this : (2 * ↑v - 1) * (-(↑v * (2 * ↑v - 1))⁻¹ + ↑u' / ↑v) = 2 * ↑u' - (1 + ↑u') / ↑v
⊢ 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ
Module: Mathlib.NumberTheory.EulerProduct.Basic

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →*₀ F
hsum : Summable fun x ↦ ‖f x‖
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
this :
  Tendsto (fun n ↦ ∏ i ∈ range n, {p | Nat.Prime p}.mulIndicator (fun p ↦ ∑' (e : ℕ), f (p ^ e)) i) atTop
    (𝓝 (∑' (n : ℕ), f n))
H : ∀ (n : ℕ), ∏ p ∈ range n, {p | Nat.Prime p}.mulIndicator (fun p ↦ (1 - f p)⁻¹) p = ∏ p ∈ n.primesBelow, (1 - f p)⁻¹
H' : ({p | Nat.Prime p}.mulIndicator fun p ↦ (1 - f p)⁻¹) = {p | Nat.Prime p}.mulIndicator fun p ↦ ∑' (e : ℕ), f (p ^ e)
⊢ Tendsto (fun n ↦ ∏ p ∈ n.primesBelow, (1 - f p)⁻¹) atTop (𝓝 (∑' (n : ℕ), f n))

Tactic:
simpa only [← H, H'] using this

Goal state after:
Module: Mathlib.NumberTheory.LSeries.Deriv

Goal state before:
pp: case a
f : ℕ → ℂ
s : ℝ
hs : abscissaOfAbsConv (logMul f) < ↑s
⊢ LSeriesSummable f ↑s

Tactic:
· refine (LSeriesSummable_of_abscissaOfAbsConv_lt_re <| by simp [hs])
      |>.norm.of_norm_bounded_eventually_nat (g := fun n ↦ ‖term (logMul f) s n‖) ?_
    filter_upwards [Filter.eventually_ge_atTop <| max 1 (Nat.ceil (Real.exp 1))] with n hn
    simp only [term_of_ne_zero (show n ≠ 0 by omega), logMul, norm_mul, mul_div_assoc,
      ← natCast_log, norm_real]
    refine le_mul_of_one_le_left (norm_nonneg _) (.trans ?_ <| Real.le_norm_self _)
    simpa using Real.log_le_log (Real.exp_pos 1) <| Nat.ceil_le.mp <| (le_max_right _ _).trans hn

Goal state after:
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case e'_5
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
i : ι
⊢ ‖‖a i‖‖ * ‖∫ (a : ℝ) in Ioi 0, ‖↑a ^ (s - 1) * ↑(rexp (-p i * a))‖ ∂volume‖ = ‖a i‖ * (Real.Gamma s.re / p i ^ s.re)

Tactic:
norm_norm

Goal state after:
case e'_5
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
i : ι
⊢ ‖a i‖ * ‖∫ (a : ℝ) in Ioi 0, ‖↑a ^ (s - 1) * ↑(rexp (-p i * a))‖ ∂volume‖ = ‖a i‖ * (Real.Gamma s.re / p i ^ s.re)
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : 1 < x
⊢ P.f_modif (1 / x) = (P.ε * ↑(x ^ P.k)) • P.g_modif x

Tactic:
have : 1 / x < 1 := by rwa [one_div_lt hx one_pos, div_one]

Goal state after:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : 1 < x
this : 1 / x < 1
⊢ P.f_modif (1 / x) = (P.ε * ↑(x ^ P.k)) • P.g_modif x
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: k : ℕ
a : UnitAddCircle
t b : ℝ
⊢ (fun b ↦ ∑' (n : ℤ), f_int k b t n) (b + 1) = (fun b ↦ ∑' (n : ℤ), f_int k b t n) b

Tactic:
simp_rw [← (Equiv.addRight (1 : ℤ)).tsum_eq (f := fun n ↦ f_int k b t n)]

Goal state after:
k : ℕ
a : UnitAddCircle
t b : ℝ
⊢ ∑' (n : ℤ), f_int k (b + 1) t n = ∑' (c : ℤ), f_int k b t ((Equiv.addRight 1) c)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
x : ℝ
⊢ cosKernel (-a) x = cosKernel a x

Tactic:
by
  induction a using QuotientAddGroup.induction_on with
  | H => simp [← QuotientAddGroup.mk_neg, ← ofReal_inj, cosKernel_def]

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

Goal state before:
pp: z τ : ℂ
⊢ jacobiTheta₂' z (τ + 2) = jacobiTheta₂' z τ

Tactic:
refine tsum_congr (fun n ↦ ?_)
  simp_rw [jacobiTheta₂'_term, jacobiTheta₂_term, Complex.exp_add]
  suffices cexp (π * I * n ^ 2 * 2 : ℂ) = 1 by rw [mul_add, Complex.exp_add, this, mul_one]
  rw [(by push_cast; ring : (π * I * n ^ 2 * 2 : ℂ) = (n ^ 2 :) * (2 * π * I)), exp_int_mul,
    exp_two_pi_mul_I, one_zpow]

Goal state after: