mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I J : FractionalIdeal B⁰ L
hI : I ≠ 0
hIJ : I * J ≤ 1
x : L
hx : x ∈ J
y : L
hy : y ∈ Submodule.restrictScalars A ↑I
⊢ ∃ y_1, (algebraMap B L) y_1 = ((lmul K L).toLinearMap x) y

Tactic:
have ⟨z, _, hz⟩ := hIJ (FractionalIdeal.mul_mem_mul hy hx)

Goal state after:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I J : FractionalIdeal B⁰ L
hI : I ≠ 0
hIJ : I * J ≤ 1
x : L
hx : x ∈ J
y : L
hy : y ∈ Submodule.restrictScalars A ↑I
z : B
left✝ : z ∈ ↑⊤
hz : (Algebra.linearMap B L) z = y * x
⊢ ∃ y_1, (algebraMap B L) y_1 = ((lmul K L).toLinearMap x) y
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
inst✝¹¹ : CommRing A
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsDomain A
inst✝³ : IsFractionRing A K
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsIntegrallyClosed A
x : L
hx : K[x] = ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L
pbgen : pb.gen = x
hnondeg : (traceForm K L).Nondegenerate
hpb :
  ⇑((traceForm K L).dualBasis hnondeg pb.basis) = fun x ↦
    (minpolyDiv K pb.gen).coeff ↑x / (aeval pb.gen) (derivative (minpoly K pb.gen))
this : Subalgebra.toSubmodule A[x] = span A (Set.range ⇑pb.basis)
⊢ (traceForm K L).dualSubmodule (Subalgebra.toSubmodule A[x]) =
    ((aeval x) (derivative (minpoly K x)))⁻¹ • Subalgebra.toSubmodule A[x]

Tactic:
conv_lhs => rw [this]

Goal state after:
A : Type u_1
K : Type u_2
L : Type u
inst✝¹¹ : CommRing A
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsDomain A
inst✝³ : IsFractionRing A K
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsIntegrallyClosed A
x : L
hx : K[x] = ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L
pbgen : pb.gen = x
hnondeg : (traceForm K L).Nondegenerate
hpb :
  ⇑((traceForm K L).dualBasis hnondeg pb.basis) = fun x ↦
    (minpolyDiv K pb.gen).coeff ↑x / (aeval pb.gen) (derivative (minpoly K pb.gen))
this : Subalgebra.toSubmodule A[x] = span A (Set.range ⇑pb.basis)
⊢ (traceForm K L).dualSubmodule (span A (Set.range ⇑pb.basis)) =
    ((aeval x) (derivative (minpoly K x)))⁻¹ • Subalgebra.toSubmodule A[x]
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x)‖ ≤ r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑w.mult * x
hw : ¬w = w₀
hyp : |(logEmbedding K) (Additive.ofMul (Additive.ofMul x)) ⟨w, hw⟩| ≤ r
⊢ |Real.log (w ((algebraMap (𝓞 K) K) ↑x))| ≤ ↑(Fintype.card (InfinitePlace K)) * r

Tactic:
rw [logEmbedding_component, abs_mul, Nat.abs_cast] at hyp

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x)‖ ≤ r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑w.mult * x
hw : ¬w = w₀
hyp : ↑(↑⟨w, hw⟩).mult * |Real.log (↑⟨w, hw⟩ ((algebraMap (𝓞 K) K) ↑(Additive.ofMul x)))| ≤ r
⊢ |Real.log (w ((algebraMap (𝓞 K) K) ↑x))| ≤ ↑(Fintype.card (InfinitePlace K)) * r
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = ↑(x, e).1 * ∏ i, fundSystem K i ^ (x, e).2 i
⊢ ↑(x, e).1 * ∏ i, fundSystem K i ^ (x, e).2 i = ↑x * 1

Tactic:
apply congr_arg

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = ↑(x, e).1 * ∏ i, fundSystem K i ^ (x, e).2 i
⊢ ∏ i, fundSystem K i ^ (x, e).2 i = 1
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : a = 0
⊢ 0 = 0 * quadraticCharFun F b

Tactic:
zero_mul

Goal state after:
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : a = 0
⊢ 0 = 0
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: case neg.inr
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
hb' : b ^ (Fintype.card F / 2) = -1
h : -1 ≠ 1
⊢ (if -a ^ (Fintype.card F / 2) = 1 then 1 else -1) = -if a ^ (Fintype.card F / 2) = 1 then 1 else -1

Tactic:
rcases FiniteField.pow_dichotomy hF ha with ha' | ha' <;>
        simp only [ha', h, neg_neg, if_true, if_false]

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case refine_1
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
H : FermatLastTheoremForThreeGen hζ
a b c : ℤ
hc : c ≠ 0
ha : ¬3 ∣ a
hb : ¬3 ∣ b
x✝ : 3 ∣ c
hcoprime : IsCoprime a b
h : a ^ 3 + b ^ 3 = c ^ 3
x : ℤ
hx : c = 3 * x
hdvd : λ ∣ ↑a
⊢ 3 ∣ a

Tactic:
rwa [← Ideal.norm_dvd_iff (hζ.prime_norm_toInteger_sub_one_of_prime_ne_two' (by decide)),
      hζ.norm_toInteger_sub_one_of_prime_ne_two' (by decide)] at hdvd

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case refine_2
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
H : FermatLastTheoremForThreeGen hζ
a b c : ℤ
hc : c ≠ 0
ha : ¬3 ∣ a
hb : ¬3 ∣ b
x✝ : 3 ∣ c
hcoprime : IsCoprime a b
h : a ^ 3 + b ^ 3 = c ^ 3
x : ℤ
hx : c = 3 * x
hdvd : λ ∣ ↑b
⊢ 3 ∣ b

Tactic:
rwa [← Ideal.norm_dvd_iff (hζ.prime_norm_toInteger_sub_one_of_prime_ne_two' (by decide)),
      hζ.norm_toInteger_sub_one_of_prime_ne_two' (by decide)] at hdvd

Goal state after:
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: s : Set ℕ
⊢ (∀ ⦃x : ℕ⦄, x ∈ s → x = 0) ↔ ∀ x ∈ s, x ∈ {0}

Tactic:
Set.mem_singleton_iff

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

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
ι : Type u_2
hι : IsEmpty ι
⊢ mulHeight 1 = 1

Tactic:
show (1 : ι → K) = 0 from Subsingleton.elim ..

Goal state after:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
ι : Type u_2
hι : IsEmpty ι
⊢ mulHeight 0 = 1
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case inr
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
A : ι' × ι → K
x : ι → K
h✝ : Nonempty ι'
j : ι'
⊢ ∑ i, (⨆ ji, v (A ji)) * ⨆ i, v (x i) ≤ (↑(Nat.card ι) * ⨆ ji, v (A ji)) * ⨆ i, v (x i)

Tactic:
rw [Finset.sum_const, nsmul_eq_mul, mul_assoc, Finset.card_univ, Nat.card_eq_fintype_card]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
⊢ mulHeight₁ x = mulHeight ![x, 1]

Tactic:
have H (v : AbsoluteValue K ℝ) (x : K) : v x ⊔ 1 = ⨆ i, v (![x, 1] i) := by
    have (i : Fin 2) : v (![x, 1] i) = ![v x, 1] i := by fin_cases i <;> simp
    simpa [this] using max_eq_iSup (v x) 1

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
H : ∀ (v : AbsoluteValue K ℝ) (x : K), max (v x) 1 = ⨆ i, v (![x, 1] i)
⊢ mulHeight₁ x = mulHeight ![x, 1]
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
n : ℕ
⊢ mulHeight₁ (x ^ n) = mulHeight₁ x ^ n

Tactic:
simp only [mulHeight₁_eq_mulHeight, ← mulHeight_pow _ n]
  congr 1
  ext1 i
  fin_cases i <;> simp

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
⊢ ContinuousOn (fun x ↦ ∫ (x_1 : ℝ) in Ioc (↑(n + 1)) (↑(n + 1) + 1), (x_1 - ↑(n + 1)) / x_1 ^ (x + 1) ∂volume) (Ici 1)

Tactic:
apply continuousOn_of_dominated (bound := fun x ↦ (x - ↑(n + 1)) / x ^ (2 : ℝ))

Goal state after:
case hF_meas
n : ℕ
⊢ ∀ x ∈ Ici 1,
    AEStronglyMeasurable (fun a ↦ (a - ↑(n + 1)) / a ^ (x + 1)) (volume.restrict (Ioc (↑(n + 1)) (↑(n + 1) + 1)))

case h_bound
n : ℕ
⊢ ∀ x ∈ Ici 1,
    ∀ᵐ (a : ℝ) ∂volume.restrict (Ioc (↑(n + 1)) (↑(n + 1) + 1)), ‖(a - ↑(n + 1)) / a ^ (x + 1)‖ ≤ (a - ↑(n + 1)) / a ^ 2

case bound_integrable
n : ℕ
⊢ Integrable (fun x ↦ (x - ↑(n + 1)) / x ^ 2) (volume.restrict (Ioc (↑(n + 1)) (↑(n + 1) + 1)))

case h_cont
n : ℕ
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioc (↑(n + 1)) (↑(n + 1) + 1)),
    ContinuousOn (fun x ↦ (a - ↑(n + 1)) / a ^ (x + 1)) (Ici 1)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
α : Type u_2
s : Finset α
x : α → K
hs : s.Nonempty
this : ∀ a ∈ s, mulHeight₁ (x a) ≠ 0
⊢ log (mulHeight₁ (∑ a ∈ s, x a)) ≤ ↑(totalWeight K) * log ↑(#s) + ∑ a ∈ s, log (mulHeight₁ (x a))

Tactic:
have : (#s : ℝ) ^ totalWeight K ≠ 0 := by simp [hs.ne_empty]

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
α : Type u_2
s : Finset α
x : α → K
hs : s.Nonempty
this✝ : ∀ a ∈ s, mulHeight₁ (x a) ≠ 0
this : ↑(#s) ^ totalWeight K ≠ 0
⊢ log (mulHeight₁ (∑ a ∈ s, x a)) ≤ ↑(totalWeight K) * log ↑(#s) + ∑ a ∈ s, log (mulHeight₁ (x a))
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: f : ℂ → ℂ := fun s ↦ riemannZeta s - 1 / (s - 1)
t : ℂ
ht : t ∈ {1}ᶜ
ht' : t - 1 = 0
⊢ f t - f 1 = 0

Tactic:
sub_eq_zero

Goal state after:
f : ℂ → ℂ := fun s ↦ riemannZeta s - 1 / (s - 1)
t : ℂ
ht : t ∈ {1}ᶜ
ht' : t = 1
⊢ f t - f 1 = 0
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ archAbsVal.card = ∑ v, v.mult

Tactic:
convert! sum_archAbsVal_eq (fun _ ↦ (1 : ℕ))

Goal state after:
case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ archAbsVal.card = (Multiset.map (fun x ↦ 1) archAbsVal).sum

case e'_3.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : InfinitePlace K
a✝ : x✝ ∈ Finset.univ
⊢ x✝.mult = x✝.mult • 1
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 0 < totalWeight K

Tactic:
have : Inhabited (InfinitePlace K) := Classical.inhabited_of_nonempty'

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : Inhabited (InfinitePlace K)
⊢ 0 < totalWeight K
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: case hc
F : Type u_1
R : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : CommRing R
x : F
hx : x ≠ 0 ∧ x ≠ 1
⊢ IsUnit (x * (1 - x))

Tactic:
simpa only [isUnit_iff_ne_zero, mul_ne_zero_iff, ne_eq, sub_eq_zero, @eq_comm _ _ x] using hx

Goal state after:
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
x : 𝓞 K
h : ∏ v, (⨆ i, v (![↑x, ↑n] i)) ^ v.mult ≤ B
v : InfinitePlace K
⊢ ↑n ^ (totalWeight K - 1) * ⨆ i, v (![↑x, ↑n] i) ≤
    (∏ v' ∈ univ.erase v, (⨆ i, v' (![↑x, ↑n] i)) ^ v'.mult) * (⨆ i, v (![↑x, ↑n] i)) ^ (v.mult - 1) *
      ⨆ i, v (![↑x, ↑n] i)

Tactic:
pow_totalWeight_sub_one_eq hn

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
x : 𝓞 K
h : ∏ v, (⨆ i, v (![↑x, ↑n] i)) ^ v.mult ≤ B
v : InfinitePlace K
⊢ (∏ w ∈ univ.erase ?m.206, ↑n ^ w.mult) * ↑n ^ (InfinitePlace.mult ?m.206 - 1) * ⨆ i, v (![↑x, ↑n] i) ≤
    (∏ v' ∈ univ.erase v, (⨆ i, v' (![↑x, ↑n] i)) ^ v'.mult) * (⨆ i, v (![↑x, ↑n] i)) ^ (v.mult - 1) *
      ⨆ i, v (![↑x, ↑n] i)

K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
x : 𝓞 K
h : ∏ v, (⨆ i, v (![↑x, ↑n] i)) ^ v.mult ≤ B
v : InfinitePlace K
⊢ InfinitePlace K
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝⁴ : Field F
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Finite F
n : ℕ
inst✝ : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
⊢ 0 = 0 * (μ - 1) ^ 2

Tactic:
zero_mul

Goal state after:
F : Type u_1
R : Type u_2
inst✝⁴ : Field F
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Finite F
n : ℕ
inst✝ : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
⊢ 0 = 0
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝⁴ : Field F
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Finite F
n : ℕ
inst✝ : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
hx₀ : 1 ≠ 0
⊢ 0 = 0 * (μ - 1) ^ 2

Tactic:
zero_mul

Goal state after:
F : Type u_1
R : Type u_2
inst✝⁴ : Field F
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Finite F
n : ℕ
inst✝ : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
hx₀ : 1 ≠ 0
⊢ 0 = 0
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
z : S
w y : R[X]
hy : h.repr z - w = f * y
⊢ 0 * eval₂ i x y = 0

Tactic:
zero_mul

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
z : S
w y : R[X]
hy : h.repr z - w = f * y
⊢ 0 = 0
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : R[X]
⊢ h.map (g %ₘ f) = h.map g

Tactic:
by
  rw [← RingHom.sub_mem_ker_iff, mem_ker_map, modByMonic_eq_sub_mul_div, sub_right_comm,
    sub_self, zero_sub, dvd_neg]
  exact ⟨_, rfl⟩

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: case neg
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hn : n < f.natDegree
i : ℕ
hi : ¬i < f.natDegree
⊢ 0 = Pi.single n 1 i

Tactic:
Pi.single_eq_of_ne

Goal state after:
case neg
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hn : n < f.natDegree
i : ℕ
hi : ¬i < f.natDegree
⊢ 0 = 0

case neg.h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hn : n < f.natDegree
i : ℕ
hi : ¬i < f.natDegree
⊢ i ≠ n
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: case neg
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
j : ZMod N
h : j = 0 ∧ s = 1
⊢ 0 = 0 * expZeta (toAddCircle (-0)) s

Tactic:
zero_mul

Goal state after:
case neg
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
j : ZMod N
h : j = 0 ∧ s = 1
⊢ 0 = 0
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j, Φ j = 0
h : Φ 0 = 0
⊢ DifferentiableAt ℂ (HDiv.hDiv (Φ 0)) s

Tactic:
by simp only [h, funext zero_div, differentiableAt_const]

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
B : BadChar N
this : riemannZeta (-2) = 0
⊢ 0 * LFunction B.χ (-2) = 0

Tactic:
zero_mul

Goal state after:
N : ℕ
inst✝ : NeZero N
B : BadChar N
this : riemannZeta (-2) = 0
⊢ 0 = 0
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * completedLFunction (𝓕 Φ) t
U : Set ℂ := {t | (t ≠ 0 ∨ ∑ j, Φ j = 0) ∧ (t ≠ 1 ∨ Φ 0 = 0)}
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
hUp : IsPreconnected U
hF : AnalyticOnNhd ℂ F U
t : ℂ
ht : t ∈ U
⊢ DifferentiableAt ℂ G t

Tactic:
apply ((differentiableAt_id.sub_const 1).const_cpow (.inl (NeZero.ne _))).mul

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := ⋯
G : ℂ → ℂ := ⋯
U : Set ℂ := ⋯
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
hUp : IsPreconnected U
hF : AnalyticOnNhd ℂ F U
t : ℂ
ht : t ∈ U
⊢ DifferentiableAt ℂ (completedLFunction (𝓕 Φ)) t
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
H₀ : Summable fun p ↦ -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))
H₁ : Summable fun p ↦ -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))
H₂ : Summable fun p ↦ -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y)))
hsum₀ : Summable fun i ↦ 3 * (-log (1 - 1 ↑↑i * ↑↑i ^ (-(1 + ↑x)))).re
hsum₁ : Summable fun i ↦ 4 * (-log (1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y)))).re
⊢ ‖L (fun n ↦ 1 ↑n) (1 + ↑x) ^ 3 * L (fun n ↦ χ ↑n) (1 + ↑x + I * ↑y) ^ 4 *
        L (fun n ↦ (χ ^ 2) ↑n) (1 + ↑x + 2 * I * ↑y)‖ ≥
    1

Tactic:
have hsum₂ := (hasSum_re H₂.hasSum).summable

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
H₀ : Summable fun p ↦ -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))
H₁ : Summable fun p ↦ -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))
H₂ : Summable fun p ↦ -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y)))
hsum₀ : Summable fun i ↦ 3 * (-log (1 - 1 ↑↑i * ↑↑i ^ (-(1 + ↑x)))).re
hsum₁ : Summable fun i ↦ 4 * (-log (1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y)))).re
hsum₂ : Summable fun x_1 ↦ (-log (1 - (χ ^ 2) ↑↑x_1 * ↑↑x_1 ^ (-(1 + ↑x + 2 * I * ↑y)))).re
⊢ ‖L (fun n ↦ 1 ↑n) (1 + ↑x) ^ 3 * L (fun n ↦ χ ↑n) (1 + ↑x + I * ↑y) ^ 4 *
        L (fun n ↦ (χ ^ 2) ↑n) (1 + ↑x + 2 * I * ↑y)‖ ≥
    1
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
⊢ deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s + ∑ χ ∈ {1}ᶜ, χ a⁻¹ * deriv (LFunction χ) s / LFunction χ s =
    deriv (LFunction 1) s / LFunction 1 s + ∑ i ∈ {1}ᶜ, i a⁻¹ * (deriv (LFunction i) s / LFunction i s) + 1 / (s - 1)

Tactic:
add_right_comm

Goal state after:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
⊢ deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s + ∑ χ ∈ {1}ᶜ, χ a⁻¹ * deriv (LFunction χ) s / LFunction χ s =
    deriv (LFunction 1) s / LFunction 1 s + 1 / (s - 1) + ∑ i ∈ {1}ᶜ, i a⁻¹ * (deriv (LFunction i) s / LFunction i s)
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable fun n ↦ (if Nat.Prime n then residueClass a n else 0) / ↑n
⊢ False

Tactic:
have key : Summable fun n : ℕ ↦ residueClass a n / n := by
    convert! (summable_residueClass_non_primes_div a).add H using 2 with n
    simp only [← add_div, ite_add_ite, zero_add, add_zero, ite_self]

Goal state after:
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable fun n ↦ (if Nat.Prime n then residueClass a n else 0) / ↑n
key : Summable fun n ↦ residueClass a n / ↑n
⊢ False
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: case succ
f : ℕ → ℂ
hf : f 0 = 0 ∧ abscissaOfAbsConv f < ⊤
g : ℕ → ℂ
hg : g 0 = 0 ∧ abscissaOfAbsConv g < ⊤
h : ∀ (n : ℕ), n ≠ 0 → f n = g n
n : ℕ
⊢ f (n + 1) = g (n + 1)

Tactic:
exact h _ n.zero_ne_add_one.symm

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha2 : 2 * a % 2 = 0
⊢ (if b % 8 = 3 ∨ b % 8 = 5 then -J(2 * a / 2 | b) else J(2 * a / 2 | b)) = J(2 * a | b)

Tactic:
rw [Int.mul_ediv_cancel_left _ (by decide), jacobiSym.mul_left,
    jacobiSym.at_two (Nat.odd_iff.mpr hb2), ZMod.χ₈_nat_eq_if_mod_eight,
    if_neg (Nat.mod_two_ne_zero.mpr hb2)]

Goal state after:
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha2 : 2 * a % 2 = 0
⊢ (if b % 8 = 3 ∨ b % 8 = 5 then -J(a | b) else J(a | b)) = (if b % 8 = 1 ∨ b % 8 = 7 then 1 else -1) * J(a | b)
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: n : ℕ
h : 2 ≤ n
⊢ mersenne n % 4 = 3

Tactic:
induction n, h using Nat.le_induction with

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: n : ℕ
h : 3 ≤ n
⊢ mersenne n % 8 = 7

Tactic:
induction n, h using Nat.le_induction with

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
⊢ (↑(Finset.Icc (fun x ↦ ⌈B₁ x⌉) fun x ↦ ⌊B₂ x⌋)).ncard = ∏ i, (⌊B₂ i⌋ - ⌈B₁ i⌉ + 1).toNat

Tactic:
norm_cast
    grind [Pi.card_Icc, card_Icc]

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

Goal state before:
pp: f : ℕ → ℝ
l : ℝ
hf : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hf' : ∀ (n : ℕ), 0 ≤ f n
⊢ Tendsto (fun s ↦ (↑s - 1) * LSeries (fun n ↦ ↑(f n)) ↑s) (𝓝[>] 1) (𝓝 ↑l)

Tactic:
refine LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div (f := fun n ↦ f n)
    (hf.ofReal.congr fun _ ↦ ?_) fun s hs ↦ ?_

Goal state after:
case refine_1
f : ℕ → ℝ
l : ℝ
hf : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hf' : ∀ (n : ℕ), 0 ≤ f n
x✝ : ℕ
⊢ ↑((∑ k ∈ Icc 1 x✝, f k) / ↑x✝) = (∑ k ∈ Icc 1 x✝, ↑(f k)) / ↑x✝

case refine_2
f : ℕ → ℝ
l : ℝ
hf : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hf' : ∀ (n : ℕ), 0 ≤ f n
s : ℝ
hs : 1 < s
⊢ LSeriesSummable (fun n ↦ ↑(f n)) ↑s
Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete

Goal state before:
pp: case mpr
G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
H : Subgroup G
a✝ : Nontrivial G
this : Dense ↑H ∨ ∃ a, zpowers a = H
⊢ DiscreteTopology ↥H → ∃ g, zpowers g = H

Tactic:
refine fun hA ↦ this.elim (fun h ↦ ?_) id

Goal state after:
case mpr
G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
H : Subgroup G
a✝ : Nontrivial G
this : Dense ↑H ∨ ∃ a, zpowers a = H
hA : DiscreteTopology ↥H
h : Dense ↑H
⊢ ∃ g, zpowers g = H
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case inl.inl
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
a✝ b✝ : GL n R
ha : a✝ ∈ 𝒢
hb : b✝ ∈ 𝒢
⊢ a✝ * b✝ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}

Tactic:
· have := mul_mem ha hb
        aesop

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: g : ConjAct SL(2, ℤ)
Γ : Subgroup SL(2, ℤ)
N : ℕ
HN : N ≠ 0 ∧ Γ(N) ≤ Γ
⊢ N ≠ 0 ∧ Γ(N) ≤ Γ

Tactic:
exact HN

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case inl.inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
a✝ b✝ : GL n R
ha : a✝ ∈ 𝒢
hb : -b✝ ∈ 𝒢
⊢ a✝ * b✝ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}

Tactic:
· have := mul_mem ha hb
        aesop

Goal state after: