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

Goal state before:
pp: A : Type u_1
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
inst✝⁶ : IsDedekindDomain B
inst✝⁵ : IsTorsionFree A B
inst✝⁴ : Module.Finite A B
inst✝³ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝² : p.IsMaximal
hp : p ≠ ⊥
P : Ideal B
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P * a
hPa : ¬P ∣ a
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this : ∀ x ∈ a, (intTrace A B) x ∈ p
hP : (↑P)⁻¹ = ↑a / ↑(Ideal.map (algebraMap A B) p)
x : L
hx : ∀ y ∈ ↑(Ideal.map (algebraMap A B) p), x * y ∈ ↑a
⊢ x ∈ comap (↑A (Algebra.trace K L)) 1

Tactic:
rw [Submodule.mem_comap, LinearMap.coe_restrictScalars, ← FractionalIdeal.coe_one,
      ← div_self (G₀ := FractionalIdeal A⁰ K) (a := p) (by simpa using hp),
      FractionalIdeal.mem_coe, FractionalIdeal.mem_div_iff_of_ne_zero (by simpa using hp)]

Goal state after:
A : Type u_1
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
inst✝⁶ : IsDedekindDomain B
inst✝⁵ : IsTorsionFree A B
inst✝⁴ : Module.Finite A B
inst✝³ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝² : p.IsMaximal
hp : p ≠ ⊥
P : Ideal B
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P * a
hPa : ¬P ∣ a
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this : ∀ x ∈ a, (intTrace A B) x ∈ p
hP : (↑P)⁻¹ = ↑a / ↑(Ideal.map (algebraMap A B) p)
x : L
hx : ∀ y ∈ ↑(Ideal.map (algebraMap A B) p), x * y ∈ ↑a
⊢ ∀ y ∈ ↑p, (Algebra.trace K L) x * y ∈ ↑p
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ (b * b ^ (p - 1) - b * 1) * (b ^ p + b) = b * (b ^ (p - 1) - 1) * (b ^ p + b)

Tactic:
by rw [Nat.mul_sub_left_distrib]

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
k : ℕ
hk : p = 2 * k + 1
c : ℕ
hc : p - 1 = 2 * c
this✝ : b ^ 2 - 1 ∣ (b ^ 2) ^ c - 1
this : b ^ 2 - 1 ∣ b ^ (2 * c) - 1
⊢ b ^ 2 - 1 ∣ b ^ (p - 1) - 1

Tactic:
← hc

Goal state after:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
k : ℕ
hk : p = 2 * k + 1
c : ℕ
hc : p - 1 = 2 * c
this✝ : b ^ 2 - 1 ∣ (b ^ 2) ^ c - 1
this : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
⊢ b ^ 2 - 1 ∣ b ^ (p - 1) - 1
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
q₁ : p.Coprime (b ^ 2 - 1)
q₂ : p * (b ^ 2 - 1) ∣ b ^ (p - 1) - 1
q₃ : p * (b ^ 2 - 1) * 2 ∣ (b ^ (p - 1) - 1) * (b ^ p + b)
q₄ : p * (b ^ 2 - 1) * 2 ∣ b * ((b ^ (p - 1) - 1) * (b ^ p + b))
⊢ 2 * p * (b ^ 2 - 1) ∣ b * (b ^ (p - 1) - 1) * (b ^ p + b)

Tactic:
rwa [mul_assoc, mul_comm, mul_assoc b]

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

Goal state before:
pp: case pos
y : ℝ
hy : 0 ≤ y
h0 : y = 0
⊢ Real.log y ≤ ↑(harmonic ⌊y⌋₊)

Tactic:
simp [h0]

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ ↑↑2 ^ Nat.log 2 n = 2 ^ Nat.log 2 n

Tactic:
Rat.cast_natCast,

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ ↑2 ^ Nat.log 2 n = 2 ^ Nat.log 2 n
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ (S.a + S.b) * ((S.a + ↑η * S.b) * (S.a + ↑η ^ 2 * S.b)) = ↑S.u * (λ ^ S.multiplicity * S.w) ^ 3

Tactic:
← w_spec,

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ (S.a + S.b) * ((S.a + ↑η * S.b) * (S.a + ↑η ^ 2 * S.b)) = ↑S.u * S.c ^ 3
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
e : ↑(support x) ⊕ ↑(support x)ᶜ ≃ ι := Equiv.Set.sumCompl (support x)
hx : x ∘ ⇑e = Sum.elim (fun i ↦ x ↑i) 0
⊢ mulHeight x = mulHeight fun i ↦ x ↑i

Tactic:
← mulHeight_comp_equiv e,

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
e : ↑(support x) ⊕ ↑(support x)ᶜ ≃ ι := Equiv.Set.sumCompl (support x)
hx : x ∘ ⇑e = Sum.elim (fun i ↦ x ↑i) 0
⊢ mulHeight (x ∘ ⇑e) = mulHeight fun i ↦ x ↑i
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_5
inst✝ : Subsingleton ι
x : ι → K
⊢ mulHeight x = 1

Tactic:
by
  rcases eq_or_ne x 0 with rfl | hx
  · simp
  obtain ⟨i, hi⟩ := Function.ne_iff.mp hx
  have : Nonempty ι := .intro i
  rw [← mulHeight_smul_eq_mulHeight x (inv_ne_zero hi)]
  convert! mulHeight_one
  ext1 j
  simpa [Subsingleton.elim j i] using inv_mul_cancel₀ hi

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
n : ℕ
x : Fin n → K
e : Fin n ⊕ Fin 1 ≃ Fin n.succ := (Equiv.sumComm (Fin n) (Fin 1)).trans (finSumFinEquiv.trans (finCongr ⋯))
he : vecCons 0 x ∘ ⇑e = Sum.elim x 0
⊢ mulHeight (vecCons 0 x) = mulHeight x

Tactic:
← mulHeight_comp_equiv e,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
n : ℕ
x : Fin n → K
e : Fin n ⊕ Fin 1 ≃ Fin n.succ := (Equiv.sumComm (Fin n) (Fin 1)).trans (finSumFinEquiv.trans (finCongr ⋯))
he : vecCons 0 x ∘ ⇑e = Sum.elim x 0
⊢ mulHeight (vecCons 0 x ∘ ⇑e) = mulHeight x
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case h₁
K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : (fun j ↦ ∑ i, A (j, i) * x i) ≠ 0
hA : A ≠ 0
hx : x ≠ 0
v : AbsoluteValue K ℝ
x✝ : v ∈ archAbsVal
⊢ ⨆ i, v (∑ i_1, A (i, i_1) * x i_1) ≤ ↑(Nat.card ι) * ((⨆ i, v (A i)) * ⨆ i, v (x i))

Tactic:
← mul_assoc

Goal state after:
case h₁
K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : (fun j ↦ ∑ i, A (j, i) * x i) ≠ 0
hA : A ≠ 0
hx : x ≠ 0
v : AbsoluteValue K ℝ
x✝ : v ∈ archAbsVal
⊢ ⨆ i, v (∑ i_1, A (i, i_1) * x i_1) ≤ (↑(Nat.card ι) * ⨆ i, v (A i)) * ⨆ i, v (x i)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case h₁
K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : (fun j ↦ ∑ i, A (j, i) * x i) ≠ 0
hA : A ≠ 0
hx : x ≠ 0
⊢ (map (fun v ↦ ⨆ i, v (∑ i_1, A (i, i_1) * x i_1)) archAbsVal).prod ≤
    ↑(Nat.card ι) ^ totalWeight K * (map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod *
      (map (fun v ↦ ⨆ i, v (A i)) archAbsVal).prod

Tactic:
rw [mul_assoc, ← prod_map_mul, ← prod_replicate, totalWeight, ← map_const', ← prod_map_mul]
    refine prod_map_le_prod_map₀ _ _ (fun v _ ↦ Real.iSup_nonneg_of_nonnegHomClass v _) fun v _ ↦ ?_
    rw [mul_comm (iSup _), ← mul_assoc]
    exact v.iSup_abv_linearMap_apply_le A x

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

Goal state before:
pp: case hbc
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
inst✝ : Finite ι
v : AbsoluteValue K ℝ
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
s : ι →₀ ℕ
hs : s ∈ p.support
⊢ ∏ x_1 ∈ s.support, v (x x_1) ^ s x_1 ≤ (⨆ i, v (x i)) ^ N

Tactic:
hp.degree_eq_sum_deg_support hs,

Goal state after:
case hbc
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
inst✝ : Finite ι
v : AbsoluteValue K ℝ
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
s : ι →₀ ℕ
hs : s ∈ p.support
⊢ ∏ x_1 ∈ s.support, v (x x_1) ^ s x_1 ≤ (⨆ i, v (x i)) ^ ∑ i ∈ s.support, s i
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case h₂
R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : CommSemiring S
inst✝² : LinearOrder S
inst✝¹ : IsOrderedRing S
inst✝ : CharZero S
v : AbsoluteValue R S
ι : Type u_3
s : Finset ι
hs : s.Nonempty
x : ι → R
⊢ 1 ≤ ∏ i ∈ s, max (v (x i)) 1

Tactic:
exact s.one_le_prod fun _ _ ↦ le_max_right ..

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

Goal state before:
pp: case hf
s : ℝ
hs : 1 < s
⊢ Tendsto (fun x ↦ 1 / (s - 1) * (1 - 1 / (↑x + 1) ^ (s - 1))) atTop (𝓝 (1 / (s - 1)))

pp: case hg
s : ℝ
hs : 1 < s
⊢ Tendsto (fun x ↦ 1 / s * (∑ n ∈ Finset.range x, 1 / (↑n + 1) ^ s - ↑x / (↑x + 1) ^ s)) atTop
    (𝓝 (1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s))

Tactic:
· rw [show 𝓝 (1 / (s - 1)) = 𝓝 (1 / (s - 1) - 1 / (s - 1) * 0) by simp]
    simp_rw [mul_sub, mul_one]
    refine tendsto_const_nhds.sub (Tendsto.const_mul _ ?_)
    refine tendsto_const_nhds.div_atTop <| (tendsto_rpow_atTop (by linarith)).comp ?_
    exact tendsto_atTop_add_const_right _ _ tendsto_natCast_atTop_atTop

Goal state after:
case hg
s : ℝ
hs : 1 < s
⊢ Tendsto (fun x ↦ 1 / s * (∑ n ∈ Finset.range x, 1 / (↑n + 1) ^ s - ↑x / (↑x + 1) ^ s)) atTop
    (𝓝 (1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s))
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (AbsoluteValue K ℝ)
v : InfinitePlace K
this : DecidableEq (InfinitePlace K)
⊢ Multiset.count (↑v) (multisetInfinitePlace K) = v.mult

Tactic:
simpa only [multisetInfinitePlace, Multiset.count_bind, Finset.sum_map_val,
    Multiset.count_replicate, ← Subtype.ext_iff] using Fintype.sum_ite_eq' v ..

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

Goal state before:
pp: this :
  Tendsto (fun s ↦ HurwitzZeta.hurwitzZetaEven 0 s - 1 / (s - 1) / s.Gammaℝ) (𝓝[≠] 1)
    (𝓝 (HurwitzZeta.hurwitzZetaEven 0 1))
⊢ riemannZeta 1 = (↑γ - log (4 * ↑π)) / 2

Tactic:
simp only [HurwitzZeta.hurwitzZetaEven_zero, div_right_comm _ _ (Gammaℝ _)] at this

Goal state after:
this : Tendsto (fun s ↦ riemannZeta s - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1) (𝓝 (riemannZeta 1))
⊢ riemannZeta 1 = (↑γ - log (4 * ↑π)) / 2
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case inr
K : Type u_6
inst✝³ : Field K
ι : Type u_7
ι' : Type u_8
inst✝² : Fintype ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h : ∀ (k : ι), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (M + N)
h✝ : Nonempty ι'
q' : ι × ι' → K := fun a ↦ (eval x) (q a)
H : mulHeight x ^ (M + N) ≤ ↑(Nat.card ι') ^ totalWeight K * mulHeight q' * mulHeight fun j ↦ (eval x) (p j)
⊢ mulHeight x ^ N * mulHeight x ^ M ≤
    (↑(Nat.card ι') ^ totalWeight K * max (mulHeightBound q) 1 * mulHeight fun j ↦ (eval x) (p j)) * mulHeight x ^ M

pp: case hC
K : Type u_6
inst✝³ : Field K
ι : Type u_7
ι' : Type u_8
inst✝² : Fintype ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h : ∀ (k : ι), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (M + N)
h✝ : Nonempty ι'
q' : ι × ι' → K := fun a ↦ (eval x) (q a)
H : mulHeight x ^ (M + N) ≤ ↑(Nat.card ι') ^ totalWeight K * mulHeight q' * mulHeight fun j ↦ (eval x) (p j)
⊢ 0 < ↑(Nat.card ι') ^ totalWeight K * max (mulHeightBound q) 1

Tactic:
case hC => exact mul_pos (mod_cast Nat.one_le_pow _ _ Nat.card_pos) <| by positivity

Goal state after:
case inr
K : Type u_6
inst✝³ : Field K
ι : Type u_7
ι' : Type u_8
inst✝² : Fintype ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h : ∀ (k : ι), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (M + N)
h✝ : Nonempty ι'
q' : ι × ι' → K := fun a ↦ (eval x) (q a)
H : mulHeight x ^ (M + N) ≤ ↑(Nat.card ι') ^ totalWeight K * mulHeight q' * mulHeight fun j ↦ (eval x) (p j)
⊢ mulHeight x ^ N * mulHeight x ^ M ≤
    (↑(Nat.card ι') ^ totalWeight K * max (mulHeightBound q) 1 * mulHeight fun j ↦ (eval x) (p j)) * mulHeight x ^ M
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
a : 𝓞 K
⊢ 1 ≤ ↑n ^ totalWeight K * ∏ᶠ (v : FinitePlace K), ⨆ i, v (![↑a, ↑n] i)

Tactic:
by
  have Hw : (0 : ℝ) < n ^ totalWeight K := by positivity
  rw_mod_cast [totalWeight_eq_finrank, ← RingOfIntegers.rank, ← absNorm_span_natCast] at Hw ⊢
  rw [← absNorm_mul_finprod_finitePlace_eq_one (show ![a, n] ≠ 0 by simp [hn])]
  gcongr
  · exact finprod_nonneg fun _ ↦ Real.iSup_nonneg_of_nonnegHomClass ..
  · exact Nat.le_of_dvd Hw <| absNorm_dvd_absNorm_of_le <| span_mono <| by simp
  · apply le_of_eq; congr; ext; congr; ext i; fin_cases i <;> simp

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (InfinitePlace K)
n : ℕ
hn : n ≠ 0
v : InfinitePlace K
⊢ (∏ x ∈ univ.erase v, ↑n ^ x.mult) * (↑n ^ (v.mult - 1) * ↑n) =
    (∏ w ∈ univ.erase v, ↑n ^ w.mult) * ↑n ^ (v.mult - 1) * ↑n

Tactic:
← mul_assoc

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (InfinitePlace K)
n : ℕ
hn : n ≠ 0
v : InfinitePlace K
⊢ (∏ x ∈ univ.erase v, ↑n ^ x.mult) * ↑n ^ (v.mult - 1) * ↑n =
    (∏ w ∈ univ.erase v, ↑n ^ w.mult) * ↑n ^ (v.mult - 1) * ↑n
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 : R[X]
hzw : h.map w = z
⊢ eval₂ i x (h.repr z) = eval₂ i x w

Tactic:
by
  rw [eq_comm, ← sub_eq_zero, ← h.map_repr z, ← map_sub, h.map_eq_zero_iff] at hzw
  obtain ⟨y, hy⟩ := hzw
  rw [← sub_eq_zero, ← eval₂_sub, hy, eval₂_mul, hx, zero_mul]

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

Goal state before:
pp: K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
⊢ ∃ C, ∀ (a b c d : K), logHeight ![a * c, a * d + b * c, b * d] ≤ C + logHeight ![a, b] + logHeight ![c, d]

Tactic:
by
  obtain ⟨C', hC₀, hC⟩ := mulHeight_sym2_le K
  refine ⟨log C', fun a b c d ↦ ?_⟩
  simp only [logHeight_eq_log_mulHeight]
  pull (disch := positivity) log
  exact log_le_log (by positivity) (hC ..)

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
H :
  (fun s ↦ (s - 1) * LFunctionTrivChar N s) =ᶠ[𝓝[≠] 1] fun s ↦
    (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)
⊢ Tendsto (fun s ↦ (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)) (𝓝[≠] 1)
    (𝓝 (∏ p ∈ N.primeFactors, (1 - (↑p)⁻¹)))

Tactic:
conv => enter [3, 1]; rw [← mul_one <| Finset.prod ..]; enter [1, 2, p]; rw [← cpow_neg_one]

Goal state after:
N : ℕ
inst✝ : NeZero N
H :
  (fun s ↦ (s - 1) * LFunctionTrivChar N s) =ᶠ[𝓝[≠] 1] fun s ↦
    (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)
⊢ Tendsto (fun s ↦ (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)) (𝓝[≠] 1)
    (𝓝 ((∏ p ∈ N.primeFactors, (1 - ↑p ^ (-1))) * 1))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ ↑(2 * k)! = 2 * ↑k * Complex.Gamma (2 * ↑k)

Tactic:
(by { norm_cast; lia } : 2 * (k : ℂ) = ↑(2 * k - 1) + 1),

Goal state after:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ ↑(2 * k)! = (↑(2 * k - 1) + 1) * Complex.Gamma (↑(2 * k - 1) + 1)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ ↑(2 * k + 1)! = (2 * ↑k + 1) * Complex.Gamma (2 * ↑k + 1)

Tactic:
rw [(by simp : Complex.Gamma (2 * k + 1) = Complex.Gamma (↑(2 * k) + 1)),
       Complex.Gamma_nat_eq_factorial, ← Nat.cast_ofNat (R := ℂ), ← Nat.cast_mul,
      ← Nat.cast_add_one, ← Nat.cast_mul, ← Nat.factorial_succ]

Goal state after:
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
mem_norm_factors :
  normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) ∈
    normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
⊢ Irreducible (Ideal.map (algebraMap R S) I)

Tactic:
suffices ∃ y, normalizedFactors (I.map (algebraMap R S)) = {y} by
    obtain ⟨y, hy⟩ := this
    have h := prod_normalizedFactors (show I.map (algebraMap R S) ≠ 0 by
          rwa [← bot_eq_zero, Ne,
            map_eq_bot_iff_of_injective (FaithfulSMul.algebraMap_injective R S)])
    rw [associated_iff_eq, hy, Multiset.prod_singleton] at h
    rw [← h]
    exact
      irreducible_of_normalized_factor y
        (show y ∈ normalizedFactors (I.map (algebraMap R S)) by simp [hy])

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
mem_norm_factors :
  normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) ∈
    normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
⊢ ∃ y, normalizedFactors (Ideal.map (algebraMap R S) I) = {y}
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: case e_a.e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k ≠ -↑n
h2 : 2 * ↑k ≠ 1
h3 : (2 * ↑k).Gammaℂ ≠ 0
⊢ Complex.cos (↑π * (2 * ↑k / 2)) * (-1) ^ (k + 1) = -1

Tactic:
mul_div_cancel_left₀ _ two_ne_zero,

Goal state after:
case e_a.e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k ≠ -↑n
h2 : 2 * ↑k ≠ 1
h3 : (2 * ↑k).Gammaℂ ≠ 0
⊢ Complex.cos (↑π * ↑k) * (-1) ^ (k + 1) = -1
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: case e_a.e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k + 1 ≠ -↑n
h3 : (2 * ↑k + 1).Gammaℂ ≠ 0
⊢ Complex.sin (↑π * (2 * ↑k / 2 + 1 / 2)) * (-1) ^ (k + 1) = -1

Tactic:
mul_div_cancel_left₀ _ two_ne_zero,

Goal state after:
case e_a.e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k + 1 ≠ -↑n
h3 : (2 * ↑k + 1).Gammaℂ ≠ 0
⊢ Complex.sin (↑π * (↑k + 1 / 2)) * (-1) ^ (k + 1) = -1
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
hs : s ≠ 1
⊢ DifferentiableAt ℂ B.F s

Tactic:
apply DifferentiableAt.congr_of_eventuallyEq

Goal state after:
case h
N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
hs : s ≠ 1
⊢ DifferentiableAt ℂ ?f s

case hL
N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
hs : s ≠ 1
⊢ B.F =ᶠ[𝓝 s] ?f

case f
N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
hs : s ≠ 1
⊢ ℂ → ℂ
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: case h
N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
hs : s ≠ 1
⊢ DifferentiableAt ℂ ?f s

Tactic:
exact (differentiableAt_riemannZeta hs).mul <| differentiableAt_LFunction B.χ s (.inl hs)

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_6
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
step1 : ∀ (n : ℤ), fourierCoeff (⇑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 : HasSum (fun i ↦ (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • (fourier i) ↑y) (B ↑y)
⊢ ↑(bernoulliFun k y) = B ↑y

Tactic:
ContinuousMap.coe_mk,

Goal state after:
case e'_6
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
step1 : ∀ (n : ℤ), fourierCoeff (⇑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 : HasSum (fun i ↦ (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • (fourier i) ↑y) (B ↑y)
⊢ ↑(bernoulliFun k y) = (ofReal ∘ periodizedBernoulli k) ↑y
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_5
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 / ↑n ^ k * (fourier ↑n) ↑x + 1 / ↑n ^ k * ((-1) ^ k * (fourier (-↑n)) ↑x) =
    1 / ↑↑n ^ k * (fourier ↑n) ↑x + 1 / (-↑↑n) ^ k * (fourier (-↑n)) ↑x

Tactic:
← mul_assoc

Goal state after:
case e'_5
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 / ↑n ^ k * (fourier ↑n) ↑x + 1 / ↑n ^ k * (-1) ^ k * (fourier (-↑n)) ↑x =
    1 / ↑↑n ^ k * (fourier ↑n) ↑x + 1 / (-↑↑n) ^ k * (fourier (-↑n)) ↑x
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_5
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
x✝ : ℕ
⊢ (fourier ↑x✝) ↑x + (fourier (-↑x✝)) ↑x = (fourier ↑x✝) ↑x + (-1) ^ (2 * k) * (fourier (-↑x✝)) ↑x

Tactic:
pow_mul (-1 : ℂ),

Goal state after:
case e'_5
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
x✝ : ℕ
⊢ (fourier ↑x✝) ↑x + (fourier (-↑x✝)) ↑x = (fourier ↑x✝) ↑x + ((-1) ^ 2) ^ k * (fourier (-↑x✝)) ↑x
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: q : ℕ
a : ZMod q
⊢ residueClass a 0 = 0

Tactic:
simp only [Set.indicator_apply_eq_zero, Set.mem_ofPred_eq, Nat.cast_zero, map_zero,
    implies_true]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_5
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x) =
    1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x + (-1) ^ (2 * k) * (-1) ^ 1 * (fourier (-↑n)) ↑x)

Tactic:
pow_mul (-1 : ℂ),

Goal state after:
case e'_5
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x) =
    1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x + ((-1) ^ 2) ^ k * (-1) ^ 1 * (fourier (-↑n)) ↑x)