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

Goal state before:
pp: p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
hp₁ : p % 2 = 1
hq₁ : q % 2 = 1
hq₂ : ringChar (ZMod q) ≠ 2
h : (quadraticChar (ZMod p)) ↑q = (quadraticChar (ZMod q)) (↑(χ₄ ↑p) * ↑p)
nc : ∀ (n r : ℕ), ↑↑n = ↑n
nc' : ↑((-1) ^ (p / 2)) = (-1) ^ (p / 2)
⊢ (quadraticChar (ZMod q)) ((-1) ^ (p / 2)) = ((-1) ^ (q / 2)) ^ (p / 2)

Tactic:
map_pow,

Goal state after:
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
hp₁ : p % 2 = 1
hq₁ : q % 2 = 1
hq₂ : ringChar (ZMod q) ≠ 2
h : (quadraticChar (ZMod p)) ↑q = (quadraticChar (ZMod q)) (↑(χ₄ ↑p) * ↑p)
nc : ∀ (n r : ℕ), ↑↑n = ↑n
nc' : ↑((-1) ^ (p / 2)) = (-1) ^ (p / 2)
⊢ (quadraticChar (ZMod q)) (-1) ^ (p / 2) = ((-1) ^ (q / 2)) ^ (p / 2)
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: a n : ℕ
hP : Prime (a ^ n - 1)
han1 : 1 < a ^ n
hn0 : n ≠ 0
ha1 : 1 < a
ha0 : 0 < a
hn1 : a ≠ 2
h : a ^ n - 1 = a - 1
⊢ n = 1

Tactic:
eq_comm

Goal state after:
a n : ℕ
hP : Prime (a ^ n - 1)
han1 : 1 < a ^ n
hn0 : n ≠ 0
ha1 : 1 < a
ha0 : 0 < a
hn1 : a ≠ 2
h : a - 1 = a ^ n - 1
⊢ n = 1
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: case refine_2.inl
P : Ideal ℕ
h : P.IsPrime
h0 : ∃ x ∈ P, x ∉ ⊥
p : ℕ := Nat.find h0
hp : p ∈ P
hp0 : p ≠ 0
this : p ≠ 1
prime : Nat.Prime p
hsp : ∀ (p : ℕ), Nat.Prime p → P ≠ span {p}
q : ℕ
hq : q ∈ P
hqp : q ∉ span {p}
hn : 0 ∈ maximalIdeal ℕ
⊢ 0 ∈ P

pp: case refine_2.inr
P : Ideal ℕ
h : P.IsPrime
h0 : ∃ x ∈ P, x ∉ ⊥
n : ℕ
hn : n ∈ maximalIdeal ℕ
p : ℕ := Nat.find h0
hp : p ∈ P
hp0 : p ≠ 0
this : p ≠ 1
prime : Nat.Prime p
hsp : ∀ (p : ℕ), Nat.Prime p → P ≠ span {p}
q : ℕ
hq : q ∈ P
hqp : q ∉ span {p}
hn1 : n ≠ 0
⊢ n ∈ P

Tactic:
· exact Ideal.zero_mem _

Goal state after:
case refine_2.inr
P : Ideal ℕ
h : P.IsPrime
h0 : ∃ x ∈ P, x ∉ ⊥
n : ℕ
hn : n ∈ maximalIdeal ℕ
p : ℕ := Nat.find h0
hp : p ∈ P
hp0 : p ≠ 0
this : p ≠ 1
prime : Nat.Prime p
hsp : ∀ (p : ℕ), Nat.Prime p → P ≠ span {p}
q : ℕ
hq : q ∈ P
hqp : q ∉ span {p}
hn1 : n ≠ 0
⊢ n ∈ P
Module: Mathlib.NumberTheory.FrobeniusNumber

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

Tactic:
Set.subset_def,

Goal state after:
s : Set ℕ
⊢ (∀ ⦃x : ℕ⦄, x ∈ s → x = 0) ↔ ∀ x ∈ s, x ∈ {0}
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: case neg
s : Set ℕ
h0 : ¬setGcd s = 0
t : Finset ℕ
hts : ↑t ⊆ s
a : ↥t → ℤ
eq : ∑ i, a i • ↑↑i = ↑(setGcd s)
x : ℕ
hxs : x ∈ s
hx : x ≠ 0
n : ℕ := x / setGcd s * ∑ i, (-a i).toNat * ↑i
c : ℕ
ge : n + c ≥ n
dvd : setGcd s ∣ n + c
q : ℕ := c / x
r : ℕ := c % x
⊢ n + (q * x + r) ∈ span ↑(insert x t)

Tactic:
add_comm,

Goal state after:
case neg
s : Set ℕ
h0 : ¬setGcd s = 0
t : Finset ℕ
hts : ↑t ⊆ s
a : ↥t → ℤ
eq : ∑ i, a i • ↑↑i = ↑(setGcd s)
x : ℕ
hxs : x ∈ s
hx : x ≠ 0
n : ℕ := x / setGcd s * ∑ i, (-a i).toNat * ↑i
c : ℕ
ge : n + c ≥ n
dvd : setGcd s ∣ n + c
q : ℕ := c / x
r : ℕ := c % x
⊢ q * x + r + n ∈ span ↑(insert x t)
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
h1 : multiplicity λ (S'.a + S'.b) < 2
h2 : multiplicity λ (S'.a + ↑η * S'.b) < 2
h3 : multiplicity λ (S'.a + ↑η ^ 2 * S'.b) < 2
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + ↑η * S'.b)
h3' : FiniteMultiplicity λ (S'.a + ↑η ^ 2 * S'.b)
this :
  ↑(2 * 3) ≤
    ↑(multiplicity λ (S'.a + S'.b)) + ↑(multiplicity λ (S'.a + ↑η * S'.b)) + ↑(multiplicity λ (S'.a + ↑η ^ 2 * S'.b))
⊢ False

Tactic:
← Nat.cast_add,

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h1 : multiplicity λ (S'.a + S'.b) < 2
h2 : multiplicity λ (S'.a + ↑η * S'.b) < 2
h3 : multiplicity λ (S'.a + ↑η ^ 2 * S'.b) < 2
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + ↑η * S'.b)
h3' : FiniteMultiplicity λ (S'.a + ↑η ^ 2 * S'.b)
this :
  ↑(2 * 3) ≤
    ↑(multiplicity λ (S'.a + S'.b) + multiplicity λ (S'.a + ↑η * S'.b)) + ↑(multiplicity λ (S'.a + ↑η ^ 2 * S'.b))
⊢ False
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
h1 : multiplicity λ (S'.a + S'.b) < 2
h2 : multiplicity λ (S'.a + ↑η * S'.b) < 2
h3 : multiplicity λ (S'.a + ↑η ^ 2 * S'.b) < 2
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + ↑η * S'.b)
h3' : FiniteMultiplicity λ (S'.a + ↑η ^ 2 * S'.b)
this :
  ↑(2 * 3) ≤
    ↑(multiplicity λ (S'.a + S'.b) + multiplicity λ (S'.a + ↑η * S'.b)) + ↑(multiplicity λ (S'.a + ↑η ^ 2 * S'.b))
⊢ False

Tactic:
← Nat.cast_add,

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h1 : multiplicity λ (S'.a + S'.b) < 2
h2 : multiplicity λ (S'.a + ↑η * S'.b) < 2
h3 : multiplicity λ (S'.a + ↑η ^ 2 * S'.b) < 2
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + ↑η * S'.b)
h3' : FiniteMultiplicity λ (S'.a + ↑η ^ 2 * S'.b)
this :
  ↑(2 * 3) ≤ ↑(multiplicity λ (S'.a + S'.b) + multiplicity λ (S'.a + ↑η * S'.b) + multiplicity λ (S'.a + ↑η ^ 2 * S'.b))
⊢ False
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case inr.mp
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 B
inst✝ : P.IsPrime
hPbot : P ≠ ⊥
hp : Ideal.under A P ≠ ⊥
hp' : ¬Ideal.map (algebraMap A B) (Ideal.under A P) = ⊥
this✝ : P.IsMaximal
this : Algebra (Localization.AtPrime (Ideal.under A P)) (Localization.AtPrime P) := ⋯
⊢ ¬P ∣ differentIdeal A B → IsUnramifiedAt A P

Tactic:
intro H

Goal state after:
case inr.mp
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 B
inst✝ : P.IsPrime
hPbot : P ≠ ⊥
hp : Ideal.under A P ≠ ⊥
hp' : ¬Ideal.map (algebraMap A B) (Ideal.under A P) = ⊥
this✝ : P.IsMaximal
this : Algebra (Localization.AtPrime (Ideal.under A P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under A P) P
H : ¬P ∣ differentIdeal A B
⊢ IsUnramifiedAt A P
Module: Mathlib.NumberTheory.Harmonic.Bounds

Goal state before:
pp: case neg
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ∑ x ∈ (Finset.Icc 1 n).erase 1, (↑x)⁻¹ + (↑1)⁻¹ ≤ 1 + Real.log ↑n

Tactic:
add_comm,

Goal state after:
case neg
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ (↑1)⁻¹ + ∑ x ∈ (Finset.Icc 1 n).erase 1, (↑x)⁻¹ ≤ 1 + Real.log ↑n
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case inr.mpr
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 B
inst✝ : P.IsPrime
hPbot : P ≠ ⊥
hp : Ideal.under A P ≠ ⊥
hp' : ¬Ideal.map (algebraMap A B) (Ideal.under A P) = ⊥
this✝ : P.IsMaximal
this : Algebra (Localization.AtPrime (Ideal.under A P)) (Localization.AtPrime P) := ⋯
⊢ IsUnramifiedAt A P → ¬P ∣ differentIdeal A B

Tactic:
intro H

Goal state after:
case inr.mpr
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 B
inst✝ : P.IsPrime
hPbot : P ≠ ⊥
hp : Ideal.under A P ≠ ⊥
hp' : ¬Ideal.map (algebraMap A B) (Ideal.under A P) = ⊥
this✝ : P.IsMaximal
this : Algebra (Localization.AtPrime (Ideal.under A P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under A P) P
H : IsUnramifiedAt A P
⊢ ¬P ∣ differentIdeal A B
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case zero
⊢ 0 = 0 - 1 + 1

Tactic:
sub_add_cancel

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : span {x} ≠ 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v | x ∈ v.asIdeal}
h_fin₀ : t₀.Finite
⊢ (∏ᶠ (i : HeightOneSpectrum (𝓞 K)), ‖(embedding i) ↑x‖) *
      ↑(absNorm (∏ᶠ (v : HeightOneSpectrum (𝓞 K)), v.maxPowDividing (span {x}))) =
    1

Tactic:
let t₁ := (fun v : HeightOneSpectrum (𝓞 K) ↦ ‖embedding v (x : K)‖).mulSupport

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : span {x} ≠ 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v | x ∈ v.asIdeal}
h_fin₀ : t₀.Finite
t₁ : Set (HeightOneSpectrum (𝓞 K)) := mulSupport fun v ↦ ‖(embedding v) ↑x‖
⊢ (∏ᶠ (i : HeightOneSpectrum (𝓞 K)), ‖(embedding i) ↑x‖) *
      ↑(absNorm (∏ᶠ (v : HeightOneSpectrum (𝓞 K)), v.maxPowDividing (span {x}))) =
    1
Module: Mathlib.NumberTheory.NumberField.ProductFormula

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : span {x} ≠ 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v | x ∈ v.asIdeal}
h_fin₀ : t₀.Finite
t₁ : Set (HeightOneSpectrum (𝓞 K)) := mulSupport fun v ↦ ‖(embedding v) ↑x‖
t₂ : Set (HeightOneSpectrum (𝓞 K)) := mulSupport fun v ↦ ↑(absNorm (v.maxPowDividing (span {x})))
h_fin₁ : t₁.Finite
⊢ ∀ (x_1 : HeightOneSpectrum (𝓞 K)),
    ↑(absNorm (x_1.asIdeal ^ (Associates.mk x_1.asIdeal).count (Associates.mk (span {x})).factors)) ≠ 1 →
      x_1.asIdeal ∣ span {x}

Tactic:
intro v

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : span {x} ≠ 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v | x ∈ v.asIdeal}
h_fin₀ : t₀.Finite
t₁ : Set (HeightOneSpectrum (𝓞 K)) := mulSupport fun v ↦ ‖(embedding v) ↑x‖
t₂ : Set (HeightOneSpectrum (𝓞 K)) := mulSupport fun v ↦ ↑(absNorm (v.maxPowDividing (span {x})))
h_fin₁ : t₁.Finite
v : HeightOneSpectrum (𝓞 K)
⊢ ↑(absNorm (v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk (span {x})).factors)) ≠ 1 → v.asIdeal ∣ span {x}
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case e_a
N : ℕ
s : ℝ
hs : 1 < s
⊢ ∑ x ∈ Finset.range N, ↑(x + 1) / s * (1 / ↑(x + 1) ^ s - 1 / (↑(x + 1) + 1) ^ s) =
    1 / s * (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s)

Tactic:
mul_comm (_ / _),

Goal state after:
case e_a
N : ℕ
s : ℝ
hs : 1 < s
⊢ ∑ x ∈ Finset.range N, (1 / ↑(x + 1) ^ s - 1 / (↑(x + 1) + 1) ^ s) * (↑(x + 1) / s) =
    (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s) * (1 / s)
Module: Mathlib.NumberTheory.NumberField.ProductFormula

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
hb : b ≠ 0
ha : a ≠ 0
⊢ |↑((Algebra.norm ℤ) a)|⁻¹ / |↑((Algebra.norm ℤ) b)|⁻¹ =
    |↑((Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b))|⁻¹

Tactic:
rw [← inv_eq_iff_eq_inv, inv_inv_div_inv, ← abs_div]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
hb : b ≠ 0
ha : a ≠ 0
⊢ |↑((Algebra.norm ℤ) a) / ↑((Algebra.norm ℤ) b)| =
    |↑((Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b))|
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case e_a
N : ℕ
s : ℝ
hs : 1 < s
⊢ ∑ x ∈ Finset.range N, ↑(x + 1) / s * (1 / ↑(x + 1) ^ s - 1 / (↑(x + 1) + 1) ^ s) =
    1 / s * (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s)

Tactic:
· simp_rw [mul_comm (_ / _), ← mul_div_assoc, div_eq_mul_inv _ s, ← Finset.sum_mul, mul_one]
    congr 1
    induction N with
    | zero => simp
    | succ N hN =>
      simp_rw [Finset.sum_range_succ, hN, Nat.cast_add_one, sub_eq_add_neg, add_assoc]
      congr 1
      ring_nf

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

Goal state before:
pp: case h₂.inl
K : Type u_4
inst✝² : Field K
ι : Type u_5
ι' : Type u_6
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι'
p : ι' → MvPolynomial ι K
h : (fun j ↦ constantCoeff (p j)) ≠ 0
this : Nonempty ι'
v : ↑nonarchAbsVal
j : ι'
h₀ : coeff 0 (p j) = 0
⊢ ↑v (coeff 0 (p j)) ≤ max (⨆ s, ↑v (coeff (↑s) (p j))) 1

pp: case h₂.inr
K : Type u_4
inst✝² : Field K
ι : Type u_5
ι' : Type u_6
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι'
p : ι' → MvPolynomial ι K
h : (fun j ↦ constantCoeff (p j)) ≠ 0
this : Nonempty ι'
v : ↑nonarchAbsVal
j : ι'
h₀ : coeff 0 (p j) ≠ 0
⊢ ↑v (coeff 0 (p j)) ≤ max (⨆ s, ↑v (coeff (↑s) (p j))) 1

Tactic:
· simp [h₀]

Goal state after:
case h₂.inr
K : Type u_4
inst✝² : Field K
ι : Type u_5
ι' : Type u_6
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι'
p : ι' → MvPolynomial ι K
h : (fun j ↦ constantCoeff (p j)) ≠ 0
this : Nonempty ι'
v : ↑nonarchAbsVal
j : ι'
h₀ : coeff 0 (p j) ≠ 0
⊢ ↑v (coeff 0 (p j)) ≤ max (⨆ s, ↑v (coeff (↑s) (p j))) 1
Module: Mathlib.RingTheory.RootsOfUnity.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
μ : R
hμ : IsPrimitiveRoot μ (n + 1)
this : (∑ i ∈ range (n + 1), X ^ i) * (X - 1) = (∏ k ∈ range n, (X - C (μ ^ (k + 1) * 1))) * (X - C 1)
⊢ ∏ k ∈ range n, (1 - μ ^ (k + 1)) = ↑n + 1

Tactic:
eq_comm

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
μ : R
hμ : IsPrimitiveRoot μ (n + 1)
this : (∏ k ∈ range n, (X - C (μ ^ (k + 1) * 1))) * (X - C 1) = (∑ i ∈ range (n + 1), X ^ i) * (X - 1)
⊢ ∏ k ∈ range n, (1 - μ ^ (k + 1)) = ↑n + 1
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
ι : Type u_2
inst✝¹ : Finite ι
x : ι → 𝓞 K
inst✝ : Nonempty ι
hx : ∀ (i : ι), x i ≠ 0
H : ∀ (j : ι), span {x j} ≠ ⊥
hx' : ⨆ i, span {x i} ≠ ⊥
v : FinitePlace K
hn : ¬absNorm v.maximalIdeal.asIdeal = 0
h : ∀ {m : ℕ}, 0 < ↑(absNorm v.maximalIdeal.asIdeal ^ m)
⊢ ↑(absNorm (v.maximalIdeal.asIdeal ^ ⨅ i, multiplicity v.maximalIdeal.asIdeal (span {x i}))) * ⨆ i, v ↑(x i) = 1

Tactic:
map_pow,

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
ι : Type u_2
inst✝¹ : Finite ι
x : ι → 𝓞 K
inst✝ : Nonempty ι
hx : ∀ (i : ι), x i ≠ 0
H : ∀ (j : ι), span {x j} ≠ ⊥
hx' : ⨆ i, span {x i} ≠ ⊥
v : FinitePlace K
hn : ¬absNorm v.maximalIdeal.asIdeal = 0
h : ∀ {m : ℕ}, 0 < ↑(absNorm v.maximalIdeal.asIdeal ^ m)
⊢ ↑(absNorm v.maximalIdeal.asIdeal ^ ⨅ i, multiplicity v.maximalIdeal.asIdeal (span {x i})) * ⨆ i, v ↑(x i) = 1
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
F' : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective ⇑(algebraMap F' FF')
Hχφ : χ' * φ' ≠ 1
Hχφ' : χ'⁻¹ * φ'⁻¹ ≠ 1
Hχ : χ' ≠ 1
Hφ : φ' ≠ 1
⊢ ↑(Fintype.card F) ≠ 0

Tactic:
intro H

Goal state after:
F : Type u_1
F' : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective ⇑(algebraMap F' FF')
Hχφ : χ' * φ' ≠ 1
Hχφ' : χ'⁻¹ * φ'⁻¹ ≠ 1
Hχ : χ' ≠ 1
Hφ : φ' ≠ 1
H : ↑(Fintype.card F) = 0
⊢ False
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
F' : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective ⇑(algebraMap F' FF')
Hχφ : χ' * φ' ≠ 1
Hχφ' : χ'⁻¹ * φ'⁻¹ ≠ 1
Hχ : χ' ≠ 1
Hφ : φ' ≠ 1
Hcard : ↑(Fintype.card F) ≠ 0
⊢ jacobiSum (χ.ringHomComp (algebraMap F' FF')) (φ.ringHomComp (algebraMap F' FF')) *
      jacobiSum (χ⁻¹.ringHomComp (algebraMap F' FF')) (φ⁻¹.ringHomComp (algebraMap F' FF')) =
    (algebraMap F' FF') ↑(Fintype.card F)

Tactic:
have H := (gaussSum_mul_gaussSum_eq_card Hχφ ψ.prim).trans_ne Hcard

Goal state after:
F : Type u_1
F' : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective ⇑(algebraMap F' FF')
Hχφ : χ' * φ' ≠ 1
Hχφ' : χ'⁻¹ * φ'⁻¹ ≠ 1
Hχ : χ' ≠ 1
Hφ : φ' ≠ 1
Hcard : ↑(Fintype.card F) ≠ 0
H : gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ ≠ 0
⊢ jacobiSum (χ.ringHomComp (algebraMap F' FF')) (φ.ringHomComp (algebraMap F' FF')) *
      jacobiSum (χ⁻¹.ringHomComp (algebraMap F' FF')) (φ⁻¹.ringHomComp (algebraMap F' FF')) =
    (algebraMap F' FF') ↑(Fintype.card F)
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
F' : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective ⇑(algebraMap F' FF')
Hχφ : χ' * φ' ≠ 1
Hχφ' : χ'⁻¹ * φ'⁻¹ ≠ 1
Hχ : χ' ≠ 1
Hφ : φ' ≠ 1
Hcard : ↑(Fintype.card F) ≠ 0
H : gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ ≠ 0
⊢ ↑(Fintype.card F) * ↑(Fintype.card F) = gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ * ↑(Fintype.card F)

Tactic:
gaussSum_mul_gaussSum_eq_card Hχφ ψ.prim

Goal state after:
F : Type u_1
F' : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective ⇑(algebraMap F' FF')
Hχφ : χ' * φ' ≠ 1
Hχφ' : χ'⁻¹ * φ'⁻¹ ≠ 1
Hχ : χ' ≠ 1
Hφ : φ' ≠ 1
Hcard : ↑(Fintype.card F) ≠ 0
H : gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ ≠ 0
⊢ ↑(Fintype.card F) * ↑(Fintype.card F) = ↑(Fintype.card F) * ↑(Fintype.card F)
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: case e'_3.refine_1
q : ℚ
this : Finset.univ.gcd ![q.num, ↑q.den] = 1
⊢ |q.num| ≤ ⨆ i, |![q.num, ↑q.den] i|

Tactic:
exact Finite.le_ciSup_of_le 0 <| by simp

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z | z ≠ 1} else Set.univ
V : Set ℂ := {z | 1 < z.re}
⊢ IsOpen U

Tactic:
by_cases h : j = 0

Goal state after:
case pos
N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z | z ≠ 1} else Set.univ
V : Set ℂ := {z | 1 < z.re}
h : j = 0
⊢ IsOpen U

case neg
N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z | z ≠ 1} else Set.univ
V : Set ℂ := {z | 1 < z.re}
h : ¬j = 0
⊢ IsOpen U
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z | z ≠ 1} else Set.univ
V : Set ℂ := {z | 1 < z.re}
hUo : IsOpen U
f : ℂ → ℂ := LFunction fun k ↦ 𝕖 (j * k)
g : ℂ → ℂ := expZeta (toAddCircle j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
hg : AnalyticOnNhd ℂ g U
⊢ IsPreconnected U

Tactic:
by_cases h : j = 0

Goal state after:
case pos
N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z | z ≠ 1} else Set.univ
V : Set ℂ := {z | 1 < z.re}
hUo : IsOpen U
f : ℂ → ℂ := LFunction fun k ↦ 𝕖 (j * k)
g : ℂ → ℂ := expZeta (toAddCircle j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
hg : AnalyticOnNhd ℂ g U
h : j = 0
⊢ IsPreconnected U

case neg
N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z | z ≠ 1} else Set.univ
V : Set ℂ := {z | 1 < z.re}
hUo : IsOpen U
f : ℂ → ℂ := LFunction fun k ↦ 𝕖 (j * k)
g : ℂ → ℂ := expZeta (toAddCircle j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
hg : AnalyticOnNhd ℂ g U
h : ¬j = 0
⊢ IsPreconnected U
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
⊢ deriv (bernoulliFun k) = fun x ↦ ↑k * bernoulliFun (k - 1) x

Tactic:
ext x
  exact (hasDerivAt_bernoulliFun _ _).deriv

Goal state after:
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:
rw [QuotientAddGroup.mk_zero, fourier_eval_zero, one_mul, ← ofReal_sub, bernoulliFun_eval_one,
    add_sub_cancel_left]

Goal state after:
k : ℕ
n : ℤ
hn : n ≠ 0
⊢ 1 / (-2 * ↑π * I * ↑n) * (↑(if k = 1 then 1 else 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.PrimesInAP

Goal state before:
pp: case neg
q : ℕ
a : ZMod q
y : ℝ
hy : 1 < y
this : LSeriesSummable (fun n ↦ ↑(Λ n)) ↑y
n : ℕ
hn : ¬↑n = a
⊢ term (fun n ↦ ↑(residueClass a n)) (↑y) n = {n | ↑n = a}.indicator (term (fun n ↦ ↑(Λ n)) ↑y) n

Tactic:
simp +contextual only [term, Set.mem_ofPred_eq, hn, not_false_eq_true, Set.indicator_of_notMem,
      ofReal_zero, zero_div, ite_self]

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

Goal state before:
pp: p : Nat.Primes
k : ℕ
⊢ 2 * (↑↑p)⁻¹ ^ (-1 / 2 + (↑k + 2)) = 2 * (↑↑p)⁻¹ ^ (↑k + 3 / 2)

Tactic:
add_comm,

Goal state after:
p : Nat.Primes
k : ℕ
⊢ 2 * (↑↑p)⁻¹ ^ (↑k + 2 + -1 / 2) = 2 * (↑↑p)⁻¹ ^ (↑k + 3 / 2)