mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hodd : p ≠ 2
this : (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑p
⊢ Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))

Tactic:
rw [this]

Goal state after:
p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hodd : p ≠ 2
this : (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑p
⊢ Prime ↑p
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])

Tactic:
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))
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✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
a : Ideal B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
b : Ideal B
ha : Ideal.map (algebraMap A B) p ^ (e - 1 + 1) = P ^ ((e - 1) * e) * a ^ e
hb : Ideal.map (algebraMap A B) p ^ (e - 1) = P ^ ((e - 1) * e) * b ^ (e - 1)
⊢ Ideal.map (algebraMap A B) p ∣ a ^ e

Tactic:
pow_add,

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✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
a : Ideal B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
b : Ideal B
ha : Ideal.map (algebraMap A B) p ^ (e - 1) * Ideal.map (algebraMap A B) p ^ 1 = P ^ ((e - 1) * e) * a ^ e
hb : Ideal.map (algebraMap A B) p ^ (e - 1) = P ^ ((e - 1) * e) * b ^ (e - 1)
⊢ Ideal.map (algebraMap A B) p ∣ a ^ e
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (Metric.closedBall 0 1).Finite

Tactic:
refine Set.Finite.of_finite_image ?_ (Set.injOn_of_injective Subtype.val_injective)
    convert! unitLattice_inter_ball_finite K 1
    ext x
    refine ⟨?_, fun ⟨hx1, hx2⟩ ↦ ⟨⟨x, hx1⟩, hx2, rfl⟩⟩
    rintro ⟨x, hx, rfl⟩
    exact ⟨Subtype.mem x, hx⟩

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x ζ : (𝓞 K)ˣ
f : Fin (rank K) → ℤ
hζ : ζ ∈ torsion K
h : x = ζ * ∏ i, fundSystem K i ^ f i
⊢ Additive.ofMul ↑x = ∑ i, f i • Additive.ofMul ↑(fundSystem K i)

Tactic:
rw [h, QuotientGroup.mk_mul, (QuotientGroup.eq_one_iff _).mpr hζ, one_mul,
            QuotientGroup.mk_prod, ofMul_prod]; rfl

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

Goal state before:
pp: case mpr
p : ℕ
inst✝ : Fact (Nat.Prime p)
y : ZMod p
ha : y * y ≠ 0
hy : y ≠ 0
⊢ ∃ y_1, ↑y_1 * ↑y_1 = y * y

Tactic:
refine ⟨Units.mk0 y hy, ?_⟩

Goal state after:
case mpr
p : ℕ
inst✝ : Fact (Nat.Prime p)
y : ZMod p
ha : y * y ≠ 0
hy : y ≠ 0
⊢ ↑(Units.mk0 y hy) * ↑(Units.mk0 y hy) = y * y
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity

Goal state before:
pp: case inr
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp1 : p % 4 = 1
hq1 : q ≠ 2
h : p ≠ q
⊢ IsSquare ↑q ↔ IsSquare ↑p

Tactic:
← eq_one_iff' p (prime_ne_zero p q h),

Goal state after:
case inr
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp1 : p % 4 = 1
hq1 : q ≠ 2
h : p ≠ q
⊢ legendreSym p ↑q = 1 ↔ IsSquare ↑p
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: k n : ℕ
hn : 1 < n + succ 1
hp : Prime (k * 2 ^ (n + succ 1 + 1) + 1)
hpdvd : k * 2 ^ (n + succ 1 + 1) + 1 ∣ (n + succ 1).fermatNumber
this : Fact (Prime (k * 2 ^ (n + succ 1 + 1) + 1))
hp2 : k * 2 ^ (n + succ 1 + 1) + 1 ≠ 2
⊢ (k * 2 ^ (n + (succ 1 + 1)) + 1) % 8 = 1

Tactic:
pow_add,

Goal state after:
k n : ℕ
hn : 1 < n + succ 1
hp : Prime (k * 2 ^ (n + succ 1 + 1) + 1)
hpdvd : k * 2 ^ (n + succ 1 + 1) + 1 ∣ (n + succ 1).fermatNumber
this : Fact (Prime (k * 2 ^ (n + succ 1 + 1) + 1))
hp2 : k * 2 ^ (n + succ 1 + 1) + 1 ≠ 2
⊢ (k * (2 ^ n * 2 ^ (succ 1 + 1)) + 1) % 8 = 1
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: case pos
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n

pp: case neg
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n

Tactic:
· have h := Nat.exists_infinite_primes (b * (b ^ 2 - 1) + 1 + m)
    obtain ⟨p, ⟨hp₁, hp₂⟩⟩ := h
    have h₁ : 0 < b := pos_of_gt (Nat.succ_le_iff.mp b_ge_two)
    have h₂ : 4 ≤ b ^ 2 := pow_le_pow_left' b_ge_two 2
    have h₃ : 0 < b ^ 2 - 1 := tsub_pos_of_lt (lt_of_lt_of_le (by simp) h₂)
    have h₄ : 0 < b * (b ^ 2 - 1) := mul_pos h₁ h₃
    have h₅ : b * (b ^ 2 - 1) < p := by lia
    have h₆ : ¬p ∣ b * (b ^ 2 - 1) := Nat.not_dvd_of_pos_of_lt h₄ h₅
    have h₇ : b ≤ b * (b ^ 2 - 1) := Nat.le_mul_of_pos_right _ h₃
    have h₈ : 2 ≤ b * (b ^ 2 - 1) := le_trans b_ge_two h₇
    have h₉ : 2 < p := lt_of_le_of_lt h₈ h₅
    have h₁₀ := psp_from_prime_gt_p b_ge_two h₉
    use psp_from_prime b p
    constructor
    · exact psp_from_prime_psp b_ge_two hp₂ h₉ h₆
    · exact le_trans (show m ≤ p by lia) (le_of_lt h₁₀)

Goal state after:
case neg
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HY : λ ^ 4 ∣ S.Y ^ 3 - 1
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

Tactic:
rcases lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd
      hζ S.lambda_not_dvd_Z with HZ | HZ

Goal state after:
case inl.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HY : λ ^ 4 ∣ S.Y ^ 3 - 1
HZ : λ ^ 4 ∣ S.Z ^ 3 - 1
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

case inl.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HY : λ ^ 4 ∣ S.Y ^ 3 - 1
HZ : λ ^ 4 ∣ S.Z ^ 3 + 1
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HY : λ ^ 4 ∣ S.Y ^ 3 + 1
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

Tactic:
rcases lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd
      hζ S.lambda_not_dvd_Z with HZ | HZ

Goal state after:
case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HY : λ ^ 4 ∣ S.Y ^ 3 + 1
HZ : λ ^ 4 ∣ S.Z ^ 3 - 1
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HY : λ ^ 4 ∣ S.Y ^ 3 + 1
HZ : λ ^ 4 ∣ S.Z ^ 3 + 1
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case b0
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
hx : x ≠ 0
this : Nonempty ι
H : ∀ (v : AbsoluteValue K ℝ), ⨆ i, v ((x ∘ f) i) ≤ ⨆ i, v (x i)
⊢ 0 ≤ (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod

Tactic:
exact Multiset.prod_map_nonneg fun v _ ↦ Real.iSup_nonneg_of_nonnegHomClass v _

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

Goal state before:
pp: K : Type := CyclotomicField 3 ℚ
hζ : IsPrimitiveRoot (IsCyclotomicExtension.zeta 3 ℚ K) 3 := IsCyclotomicExtension.zeta_spec 3 ℚ K
this : NumberField K
a b c : NumberField.RingOfIntegers K
u : (NumberField.RingOfIntegers K)ˣ
hc : c ≠ 0
ha : ¬hζ.toInteger - 1 ∣ a
hb : ¬hζ.toInteger - 1 ∣ b
hcdvd : hζ.toInteger - 1 ∣ c
coprime : IsCoprime a b
H : a ^ 3 + b ^ 3 = ↑u * c ^ 3
S' : FermatLastTheoremForThreeGen.Solution' hζ :=
  { a := a, b := b, c := c, u := u, ha := ha, hb := hb, hc := hc, coprime := coprime, hcdvd := hcdvd, H := H }
⊢ False

Tactic:
obtain ⟨S, -⟩ := FermatLastTheoremForThreeGen.exists_Solution_of_Solution' S'

Goal state after:
K : Type := CyclotomicField 3 ℚ
hζ : IsPrimitiveRoot (IsCyclotomicExtension.zeta 3 ℚ K) 3 := IsCyclotomicExtension.zeta_spec 3 ℚ K
this : NumberField K
a b c : NumberField.RingOfIntegers K
u : (NumberField.RingOfIntegers K)ˣ
hc : c ≠ 0
ha : ¬hζ.toInteger - 1 ∣ a
hb : ¬hζ.toInteger - 1 ∣ b
hcdvd : hζ.toInteger - 1 ∣ c
coprime : IsCoprime a b
H : a ^ 3 + b ^ 3 = ↑u * c ^ 3
S' : FermatLastTheoremForThreeGen.Solution' hζ :=
  { a := a, b := b, c := c, u := u, ha := ha, hb := hb, hc := hc, coprime := coprime, hcdvd := hcdvd, H := H }
S : FermatLastTheoremForThreeGen.Solution hζ
⊢ False
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: s : ℝ
hs : 1 < s
⊢ HasSum (fun b ↦ term (b + 1) s) (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s)

Tactic:
hasSum_iff_tendsto_nat_of_nonneg (fun n ↦ term_nonneg (n + 1) s)

Goal state after:
s : ℝ
hs : 1 < s
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, term (i + 1) s) atTop (𝓝 (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s))
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: h : Tendsto (fun b ↦ (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))
this✝ : Tendsto ((fun b ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))
this : {z | 0 < z.re} ∈ 𝓝 1
a : ℂ
ha : 0 < a.re
a✝ : a ∈ {1}ᶜ
⊢ ((fun b ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) a = 1 / (a - 1) - 1 / a.Gammaℝ / (a - 1)

Tactic:
rw [Pi.div_apply, ← sub_div, div_right_comm, sub_div' (Gammaℝ_ne_zero_of_re_pos ha), one_mul]

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

Goal state before:
pp: case h₂.refine_1
K : Type u_4
inst✝³ : Field K
ι : Type u_5
ι' : Type u_6
inst✝² : AdmissibleAbsValues K
inst✝¹ : Finite ι'
inst✝ : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
hx : x ≠ 0
h₀ : (fun j ↦ (eval x) (p j)) ≠ 0
H₀ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ ⨆ j, (p j).coeff.sum fun x c ↦ v c
H₁ : 0 ≤ (Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod
H₂ : 0 ≤ (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod
H₃ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((eval x) (p i))
H₄ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)
HH₁ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ (⨆ i, v (x i)) ^ N
HH₂ : ∀ (f : ι' → ℝ) (j : ι'), f j ≤ ⨆ j, f j
this : Nonempty ι'
F : Function.HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x i)
v : ↑nonarchAbsVal
j : ι'
⊢ ↑v ((eval x) (p j)) ≤ (⨆ j, max (⨆ s, ↑v (coeff (↑s) (p j))) 1) * (⨆ i, ↑v (x i)) ^ N

Tactic:
grw [(isNonarchimedean _ v.prop).eval_mvPolynomial_le (hp j) x]
      gcongr
      · exact HH₁ v.val
      · grw [← HH₂, ← le_max_left]

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

Goal state before:
pp: case neg
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ¬![c, d] = 0
⊢ mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a * c, a * d, b * c, b * d]

Tactic:
grw [← le_max_left C 1]

Goal state after:
case neg
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ¬![c, d] = 0
⊢ mulHeight ![a * c, a * d + b * c, b * d] ≤ C * mulHeight ![a * c, a * d, b * c, b * d]
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
B' : ℝ := B / ↑n ^ (totalWeight K - 1)
x : 𝓞 K
hx : ∀ (v : InfinitePlace K), v ↑x ≤ B'
⊢ IsIntegral ℤ ↑x ∧ ∀ (φ : K →+* ℂ), ‖φ ↑x‖ ≤ B'

pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
B' : ℝ := B / ↑n ^ (totalWeight K - 1)
a : K
ha : IsIntegral ℤ a ∧ ∀ (φ : K →+* ℂ), ‖φ a‖ ≤ B'
⊢ ∃ x, (∀ (v : InfinitePlace K), v ↑x ≤ B') ∧ ↑x = a

Tactic:
· exact ⟨x.isIntegral_coe, fun φ ↦ hx <| .mk φ⟩

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
B' : ℝ := B / ↑n ^ (totalWeight K - 1)
a : K
ha : IsIntegral ℤ a ∧ ∀ (φ : K →+* ℂ), ‖φ a‖ ≤ B'
⊢ ∃ x, (∀ (v : InfinitePlace K), v ↑x ≤ B') ∧ ↑x = a
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
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
Q : R[X]
⊢ (((adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I).toRingEquiv.trans (quotEquivOfEq ⋯))
      (((adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I).toRingEquiv.symm
        ((quotEquivOfEq ⋯)
          ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
            (Polynomial.map (Ideal.Quotient.mk I) Q)))) =
    (⇑(((adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I).toRingEquiv.trans (quotEquivOfEq ⋯)) ∘
        ⇑(quotAdjoinEquivQuotMap hx ⋯).symm)
      ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval x) Q))

Tactic:
quotEquivOfEq_mk

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
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
Q : R[X]
⊢ (((adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I).toRingEquiv.trans (quotEquivOfEq ⋯))
      (((adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I).toRingEquiv.symm
        ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R (adjoin.powerBasis' hx').gen)}))
          (Polynomial.map (Ideal.Quotient.mk I) Q))) =
    (⇑(((adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I).toRingEquiv.trans (quotEquivOfEq ⋯)) ∘
        ⇑(quotAdjoinEquivQuotMap hx ⋯).symm)
      ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval x) Q))
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
n : ℤ
hn : n ≠ 0
⊢ 1 / (-2 * ↑π * I * ↑n) *
      ((fourier (-n)) ↑0 * (↑(bernoulliFun k 1) - ↑(bernoulliFun k 0)) -
        fourierCoeffOn ⋯ (fun x ↦ ↑(↑k * bernoulliFun (k - 1) x)) n) =
    1 / (-2 * ↑π * I * ↑n) *
      ((if k = 1 then 1 else 0) -
        ↑k * fourierCoeffOn bernoulliFourierCoeff._proof_1 (fun x ↦ ↑(bernoulliFun (k - 1) x)) n)

Tactic:
QuotientAddGroup.mk_zero,

Goal state after:
k : ℕ
n : ℤ
hn : n ≠ 0
⊢ 1 / (-2 * ↑π * I * ↑n) *
      ((fourier (-n)) 0 * (↑(bernoulliFun k 1) - ↑(bernoulliFun k 0)) -
        fourierCoeffOn ⋯ (fun x ↦ ↑(↑k * bernoulliFun (k - 1) x)) n) =
    1 / (-2 * ↑π * I * ↑n) *
      ((if k = 1 then 1 else 0) -
        ↑k * fourierCoeffOn bernoulliFourierCoeff._proof_1 (fun x ↦ ↑(bernoulliFun (k - 1) x)) n)
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
⊢ B.F s = LSeries (⇑B.χ.zetaMul) s

Tactic:
rw [F, zetaMul, ← coe_mul, LSeries_convolution']

Goal state after:
N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
⊢ Function.update (fun s ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1) s =
    LSeries (⇑↑zeta) s * LSeries (⇑(toArithmeticFunction fun x ↦ B.χ ↑x)) s

case hf
N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
⊢ LSeriesSummable (⇑↑zeta) s

case hg
N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
⊢ LSeriesSummable (⇑(toArithmeticFunction fun x ↦ B.χ ↑x)) s
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: case inr.refine_2
N : ℕ
inst✝ : NeZero N
B : BadChar N
G : ℂ → ℂ := Function.update (fun s ↦ (s - 1) * riemannZeta s) 1 1
H : ℂ → ℂ := Function.update (fun s ↦ (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1 (deriv (LFunction B.χ) 1)
this : B.F = G * H
⊢ ContinuousAt B.F 1

Tactic:
rw [this]

Goal state after:
case inr.refine_2
N : ℕ
inst✝ : NeZero N
B : BadChar N
G : ℂ → ℂ := Function.update (fun s ↦ (s - 1) * riemannZeta s) 1 1
H : ℂ → ℂ := Function.update (fun s ↦ (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1 (deriv (LFunction B.χ) 1)
this : B.F = G * H
⊢ ContinuousAt (G * H) 1
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
Uc : Set ℂ := (if ∑ j, Φ j = 0 then ∅ else {0}) ∪ if Φ 0 = 0 then ∅ else {1}
⊢ IsPreconnected U

Tactic:
have : Uc.Countable := by
      apply Countable.union <;>
      split_ifs <;>
      simp only [countable_singleton, countable_empty]

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 : ℂ → ℂ := 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
Uc : Set ℂ := (if ∑ j, Φ j = 0 then ∅ else {0}) ∪ if Φ 0 = 0 then ∅ else {1}
this : Uc.Countable
⊢ IsPreconnected U
Module: Mathlib.NumberTheory.ZetaValues

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

Tactic:
pow_add,

Goal state after:
case e'_6
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ (-1) ^ k * (-1) ^ 1 * (2 * ↑π) ^ (2 * k) = -(2 * ↑π * I) ^ (2 * k)
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
hG : AnalyticOnNhd ℂ G U
hV : {z | 1 < z.re} ∈ 𝓝 2
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * completedLFunction (𝓕 Φ) s

Tactic:
have hFG : F =ᶠ[𝓝 2] G := eventually_of_mem hV <| fun t ht ↦ by
    simpa only [F, G, pow_zero, mul_one] using completedLFunction_one_sub_of_one_lt_even hΦ ht

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 : ℂ → ℂ := 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
hG : AnalyticOnNhd ℂ G U
hV : {z | 1 < z.re} ∈ 𝓝 2
hFG : F =ᶠ[𝓝 2] G
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * completedLFunction (𝓕 Φ) s
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_6.e_a.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ (-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) = -(2 * ↑π * I) ^ (2 * k + 1)

Tactic:
pow_add,

Goal state after:
case e'_6.e_a.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ (-1) ^ k * (-1) ^ 1 * I * (2 * ↑π) ^ (2 * k + 1) = -(2 * ↑π * I) ^ (2 * k + 1)
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| I ^ (2 * k + 1)

Tactic:
pow_add,

Goal state after:
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| I ^ (2 * k) * I ^ 1
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
h : ¬(χ ^ 2 = 1 ∧ s = 1)
⊢ s = 1 + I * ↑s.im

Tactic:
conv_lhs => rw [← re_add_im s, hs, ofReal_one, mul_comm]

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

Goal state before:
pp: f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : ∃ s ∈ atTop, Set.EqOn (fun x ↦ LSeries f ↑x) 0 s
F : ℕ → ℂ := fun n ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F ↑x = LSeries f ↑x
n : ℕ
⊢ ∃ s ∈ atTop, Set.EqOn (fun x ↦ ↑n ^ ↑x * LSeries f ↑x) (fun x ↦ 0) s

Tactic:
obtain ⟨s, hs⟩ := H

Goal state after:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
F : ℕ → ℂ := fun n ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F ↑x = LSeries f ↑x
n : ℕ
s : Set ℝ
hs : s ∈ atTop ∧ Set.EqOn (fun x ↦ LSeries f ↑x) 0 s
⊢ ∃ s ∈ atTop, Set.EqOn (fun x ↦ ↑n ^ ↑x * LSeries f ↑x) (fun x ↦ 0) s
Module: Mathlib.NumberTheory.LSeries.ZetaZeros

Goal state before:
pp: case refine_1
⊢ riemannZeta 2 ≠ 0

pp: case refine_2
⊢ IsConnected {1}ᶜ

Tactic:
· exact riemannZeta_ne_zero_of_one_le_re Nat.one_le_ofNat

Goal state after:
case refine_2
⊢ IsConnected {1}ᶜ