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

Goal state before:
pp: k : ℕ
K : Type u_1
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {2 ^ (k + 2)} ℚ K
hζ : IsPrimitiveRoot ζ (2 ^ (k + 2))
this : NumberField K
⊢ (Algebra.norm ℤ) (hζ.toInteger - 1) = 2

Tactic:
norm_eq_iff ℤ (Sₘ := K) (Rₘ := ℚ) le_rfl,

Goal state after:
k : ℕ
K : Type u_1
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {2 ^ (k + 2)} ℚ K
hζ : IsPrimitiveRoot ζ (2 ^ (k + 2))
this : NumberField K
⊢ (Algebra.norm ℚ) ((algebraMap (𝓞 K) K) (hζ.toInteger - 1)) = (algebraMap ℤ ℚ) 2
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case e'_3.h₁
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✝ : Decidable (IsField A)
⊢ IsField A ↔ restrictScalars A (Algebra.trace K L).range ≤ 1

Tactic:
rw [← IsFractionRing.surjective_iff_isField (R := A) (K := K),
    LinearMap.range_eq_top.mpr (Algebra.trace_surjective K L),
    ← RingHom.range_eq_top, _root_.eq_top_iff]

Goal state after:
case e'_3.h₁
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✝ : Decidable (IsField A)
⊢ ⊤ ≤ (algebraMap A K).range ↔ restrictScalars A ⊤ ≤ 1
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
hn : 2 ≤ n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
hp : ↑p ∣ (Algebra.norm ℤ) (hζ.toInteger - 1)
this✝ : NeZero n
this : NumberField ↥ℚ⟮ζ⟯
⊢ (Algebra.norm ℤ) (hζ.toInteger - 1) = (Algebra.norm ℤ) (⋯.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K

Tactic:
norm_eq_iff ℤ (Sₘ := K) (Rₘ := ℚ) le_rfl,

Goal state after:
n : ℕ
hn : 2 ≤ n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
hp : ↑p ∣ (Algebra.norm ℤ) (hζ.toInteger - 1)
this✝ : NeZero n
this : NumberField ↥ℚ⟮ζ⟯
⊢ (Algebra.norm ℚ) ((algebraMap (𝓞 K) K) (hζ.toInteger - 1)) =
    (algebraMap ℤ ℚ) ((Algebra.norm ℤ) (⋯.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K)
Module: Mathlib.RingTheory.DedekindDomain.LinearDisjoint

Goal state before:
pp: case a
A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst✝⁵⁶ : CommRing A
inst✝⁵⁵ : Field K
inst✝⁵⁴ : Algebra A K
inst✝⁵³ : IsFractionRing A K
inst✝⁵² : CommRing B
inst✝⁵¹ : Field L
inst✝⁵⁰ : Algebra B L
inst✝⁴⁹ : Algebra A L
inst✝⁴⁸ : Algebra K L
inst✝⁴⁷ : FiniteDimensional K L
inst✝⁴⁶ : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst✝⁴⁵ : CommRing R₁
inst✝⁴⁴ : CommRing R₂
inst✝⁴³ : IsDomain R₁
inst✝⁴² : Algebra A R₁
inst✝⁴¹ : Algebra A R₂
inst✝⁴⁰ : Algebra R₁ B
inst✝³⁹ : Algebra R₂ B
inst✝³⁸ : Algebra R₁ L
inst✝³⁷ : Algebra R₂ L
inst✝³⁶ : IsScalarTower A R₁ L
inst✝³⁵ : IsScalarTower R₁ B L
inst✝³⁴ : IsScalarTower R₂ B L
inst✝³³ : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst✝³² : Algebra R₁ ↥F₁
inst✝³¹ : Algebra R₂ ↥F₂
inst✝³⁰ : IsTorsionFree R₁ ↥F₁
inst✝²⁹ : IsScalarTower A (↥F₂) L
inst✝²⁸ : IsScalarTower A R₂ ↥F₂
inst✝²⁷ : IsScalarTower R₁ (↥F₁) L
inst✝²⁶ : IsScalarTower R₂ (↥F₂) L
inst✝²⁵ : Algebra.IsSeparable K ↥F₂
inst✝²⁴ : Algebra.IsSeparable (↥F₁) L
inst✝²³ : IsDomain A
inst✝²² : IsDedekindDomain B
inst✝²¹ : IsDedekindDomain R₁
inst✝²⁰ : IsDedekindDomain R₂
inst✝¹⁹ : IsFractionRing B L
inst✝¹⁸ : IsFractionRing R₁ ↥F₁
inst✝¹⁷ : IsFractionRing R₂ ↥F₂
inst✝¹⁶ : IsIntegrallyClosed A
inst✝¹⁵ : IsIntegralClosure B R₁ L
inst✝¹⁴ : IsTorsionFree R₁ B
inst✝¹³ : IsTorsionFree R₂ B
inst✝¹² : Algebra A B
inst✝¹¹ : Module.Finite A B
inst✝¹⁰ : IsTorsionFree A B
inst✝⁹ : IsTorsionFree A R₁
inst✝⁸ : IsTorsionFree A R₂
inst✝⁷ : Module.Finite A R₁
inst✝⁶ : Module.Finite R₂ B
inst✝⁵ : IsScalarTower A R₂ B
inst✝⁴ : Module.Finite R₁ B
inst✝³ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
inst✝² : IsScalarTower A R₁ B
inst✝¹ : Free A R₂
inst✝ : IsLocalization (algebraMapSubmonoid R₂ A⁰) ↥F₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
h₃ : IsCoprime (Ideal.map (algebraMap R₁ B) (differentIdeal A R₁)) (Ideal.map (algebraMap R₂ B) (differentIdeal A R₂))
this✝ : Algebra.IsSeparable (FractionRing A) (FractionRing R₂)
this : span B (⇑(algebraMap (↥F₂) L) '' ↑(traceDual A K 1)) ≤ traceDual R₁ (↥F₁) 1
⊢ ↑(span R₁ (⇑(algebraMap (↥F₂) L) '' ↑(traceDual A K 1))) ⊆
    ↑(span B ↑(span R₁ (⇑(algebraMap (↥F₂) L) '' ↑(traceDual A K 1))))

Tactic:
exact Submodule.subset_span

Goal state after:
Module: Mathlib.RingTheory.Fintype

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h : Fintype.card R ≤ 2
h✝ : Subsingleton R
a : R
x✝ : a ∈ univ
⊢ a ∈ {0, 1}

Tactic:
by simp [Subsingleton.elim a 0]

Goal state after:
Module: Mathlib.RingTheory.Fintype

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
⊢ 1 < Fintype.card R

Tactic:
rw [h]

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
⊢ 1 < 3
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : ↥(unitLattice K)
hx : x ∈ Metric.closedBall 0 1
⊢ ↑x ∈ ↑(unitLattice K) ∩ Metric.closedBall 0 1

Tactic:
exact ⟨Subtype.mem x, hx⟩

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

Goal state before:
pp: n : ℤ
h : ¬3 ∣ n
⊢ (castHom ⋯ (ZMod 3)) ↑n ≠ 0

Tactic:
map_intCast,

Goal state after:
n : ℤ
h : ¬3 ∣ n
⊢ ↑n ≠ 0
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case pos.inl
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)
Q : Ideal B
x : B
hxQ : x ∈ Q
hx : (intTrace A B) x ∉ ⊥
⊢ ¬0 ∣ differentIdeal A B

Tactic:
zero_dvd_iff

Goal state after:
case pos.inl
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)
Q : Ideal B
x : B
hxQ : x ∈ Q
hx : (intTrace A B) x ∉ ⊥
⊢ ¬differentIdeal A B = 0
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
h₀ : IsSquare x ↔ x ^ (Fintype.card (ZMod p) / 2) = 1
hs : (∃ y, y ^ 2 = x) ↔ IsSquare x
⊢ IsSquare x ↔ x ^ (p / 2) = 1

Tactic:
rwa [card p] at h₀

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a ≠ 0
h : (quadraticChar F) a = -1
⊢ ¬(quadraticChar F) a = 1

Tactic:
rw [h]

Goal state after:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a ≠ 0
h : (quadraticChar F) a = -1
⊢ ¬-1 = 1
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
hm : FiniteMultiplicity λ S'.c
⊢ λ ^ 2 ∣ S'.c

Tactic:
have := lambda_pow_four_dvd_c_cube S'

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hm : FiniteMultiplicity λ S'.c
this : λ ^ 4 ∣ S'.c ^ 3
⊢ λ ^ 2 ∣ S'.c
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case inl
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)
inst✝ : ⊥.IsPrime
⊢ ¬0 ∣ differentIdeal A B ↔ IsUnramifiedAt A 0

Tactic:
zero_dvd_iff

Goal state after:
case inl
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)
inst✝ : ⊥.IsPrime
⊢ ¬differentIdeal A B = 0 ↔ IsUnramifiedAt A 0
Module: Mathlib.NumberTheory.Harmonic.Bounds

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

Tactic:
Rat.cast_inv,

Goal state after:
case neg
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ∑ x ∈ Finset.Icc 1 n, (↑↑x)⁻¹ ≤ 1 + Real.log ↑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
k k' : 𝓞 K
hk' : S.a + S.b = λ ^ 2 * k'
hk : (S.b * (↑η + 1) + λ * k') * -↑η = λ * k * -↑η
⊢ S.b = λ * ((k - k') * -↑η)

Tactic:
rw [show (S.b * (η + 1) + λ * k') * -η = (-S.b) * (η ^ 2 + η + 1 - 1) - η * λ * k' by ring,
    eta_sq, show -S.b * (-↑η - 1 + ↑η + 1 - 1) = S.b by ring, sub_eq_iff_eq_add] at hk

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
k k' : 𝓞 K
hk' : S.a + S.b = λ ^ 2 * k'
hk : S.b = λ * k * -↑η + ↑η * λ * k'
⊢ S.b = λ * ((k - k') * -↑η)
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
r s t w : 𝓞 K
hr : ¬λ ∣ r
hs : ¬λ ∣ s
Hp : ∀ {p : 𝓞 K}, Prime p → p ∣ t → p ∣ w → Associated p λ
H₁ : ∀ {q : 𝓞 K}, q ∣ r → q ∣ t
H₂ : ∀ {q : 𝓞 K}, q ∣ s → q ∣ w
⊢ IsCoprime r s

Tactic:
by
  refine isCoprime_of_prime_dvd (not_and.2 (fun _ hz ↦ hs (by simp [hz])))
    (fun p hp p_dvd_r p_dvd_s ↦ hr ?_)
  rwa [← Associated.dvd_iff_dvd_left <| Hp hp (H₁ p_dvd_r) (H₂ p_dvd_s)]

Goal state after:
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) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under A P) P
H : IsUnramifiedAt A P
Q : Ideal B
h₁ : P ⊔ Q = ⊤
h₂ : Ideal.map (algebraMap A B) (Ideal.under A P) = P ^ P.ramificationIdx A * Q
⊢ ¬P ∣ differentIdeal A B

Tactic:
Ideal.ramificationIdx_eq_one_of_isUnramifiedAt,

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
Q : Ideal B
h₁ : P ⊔ Q = ⊤
h₂ : Ideal.map (algebraMap A B) (Ideal.under A P) = P ^ 1 * Q
⊢ ¬P ∣ differentIdeal A B
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
this : 2 ≤ S.multiplicity
hh : S.x * (S.y * S.z) = ↑S.u * S.w ^ 3
⊢ S.x * S.y * S.z = ↑S.u * S.w ^ 3

Tactic:
convert! hh using 1

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : 2 ≤ S.multiplicity
hh : S.x * (S.y * S.z) = ↑S.u * S.w ^ 3
⊢ S.x * S.y * S.z = S.x * (S.y * S.z)
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
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
⊢ ∃ 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_Y with
    HY | HY

Goal state after:
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

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
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: α : Type u_2
β : Type u_3
F : Type u_4
inst✝⁴ : AddCommMonoid β
inst✝³ : FunLike F β ℝ
inst✝² : NonnegHomClass F β ℝ
inst✝¹ : ZeroHomClass F β ℝ
v : F
l : α → β
inst✝ : Fintype α
hv : IsNonarchimedean ⇑v
⊢ ⨆ i, v (l ↑i) ≤ ⨆ i, v (l i)

Tactic:
← cbiSup_eq_of_forall (by grind)

Goal state after:
α : Type u_2
β : Type u_3
F : Type u_4
inst✝⁴ : AddCommMonoid β
inst✝³ : FunLike F β ℝ
inst✝² : NonnegHomClass F β ℝ
inst✝¹ : ZeroHomClass F β ℝ
v : F
l : α → β
inst✝ : Fintype α
hv : IsNonarchimedean ⇑v
⊢ ⨆ i, ⨆ (h : i ∈ Finset.univ), v (l ↑⟨i, h⟩) ≤ ⨆ i, v (l i)
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.Solution'_descent.multiplicity = S.multiplicity - 1

Tactic:
by
  refine multiplicity_eq_of_dvd_of_not_dvd
    (by simp [Solution'_descent]) (fun h ↦ S.lambda_not_dvd_X ?_)
  obtain ⟨k, hk : λ ^ (S.multiplicity - 1) * S.X = λ ^ (S.multiplicity - 1 + 1) * k⟩ := h
  rw [pow_succ, mul_assoc] at hk
  simp only [mul_eq_mul_left_iff, pow_eq_zero_iff', hζ.zeta_sub_one_prime'.ne_zero, ne_eq,
    false_and, or_false] at hk
  simp [hk]

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 ∈ s.support, (⨆ i, v (x i)) ^ s i

Tactic:
gcongr with i

Goal state after:
case hab
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
i : ι
a✝ : i ∈ s.support
⊢ v (x i) ≤ ⨆ i, v (x i)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case h₂
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
inst✝ : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
hp₀ : p ≠ 0
s : ι →₀ ℕ
hs₁ : s ∈ p.support
hs₂ : v (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, x i ^ d i) ≤ v (coeff s p * ∏ i ∈ s.support, x i ^ s i)
⊢ ∏ x_1 ∈ s.support, v (x x_1) ^ s x_1 ≤ ∏ i ∈ s.support, (⨆ i, v (x i)) ^ s i

Tactic:
gcongr with i

Goal state after:
case hab
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
inst✝ : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
hp₀ : p ≠ 0
s : ι →₀ ℕ
hs₁ : s ∈ p.support
hs₂ : v (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, x i ^ d i) ≤ v (coeff s p * ∏ i ∈ s.support, x i ^ s i)
i : ι
a✝ : i ∈ s.support
⊢ v (x i) ≤ ⨆ i, v (x i)
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
⊢ ∏ᶠ (w : FinitePlace K), w ((algebraMap (𝓞 K) K) a) / w ((algebraMap (𝓞 K) K) b) =
    ↑|(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b)|⁻¹

Tactic:
Rat.cast_inv,

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
⊢ ∏ᶠ (w : FinitePlace K), w ((algebraMap (𝓞 K) K) a) / w ((algebraMap (𝓞 K) K) b) =
    (↑|(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b)|)⁻¹
Module: Mathlib.RingTheory.RootsOfUnity.Lemmas

Goal state before:
pp: case refine_1.hy.hx
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ ℤ[μ], μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := ⋯
Zdef : ∀ (k : ℕ), Z k ∈ ℤ[μ] ∧ μ ^ k - 1 = Z k * (μ - 1)
x✝¹ : ℕ
x✝ : x✝¹ ∈ Ico k (m + k)
⊢ μ ^ (x✝¹ + 1) ∈ ℤ[μ]

Tactic:
exact Subalgebra.pow_mem _ (self_mem_adjoin_singleton ℤ μ) _

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

Goal state before:
pp: case refine_2
f : ℂ → ℂ := fun s ↦ riemannZeta s - 1 / (s - 1)
C : ℂ
hC : Tendsto f (𝓝[≠] 1) (𝓝 C)
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 1, ↑x ∈ {1}ᶜ

Tactic:
filter_upwards [self_mem_nhdsWithin] with a ha
      rw [mem_compl_singleton_iff, ← Complex.ofReal_one, Ne, Complex.ofReal_inj]
      exact ne_of_gt ha

Goal state after:
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} ≠ ⊥
⊢ ↑(absNorm (span (Set.range x))) * ∏ᶠ (v : FinitePlace K), ⨆ i, v ↑(x i) = 1

Tactic:
span_range_eq_iSup,

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} ≠ ⊥
⊢ ↑(absNorm (⨆ i, span {x i})) * ∏ᶠ (v : FinitePlace K), ⨆ i, v ↑(x i) = 1
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 h' : IsAdjoinRoot S f
eq : h.root = h'.root
x : R[X]
⊢ h.map x = h'.map x

Tactic:
← h.aeval_root_eq_map,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h h' : IsAdjoinRoot S f
eq : h.root = h'.root
x : R[X]
⊢ (aeval h.root) x = h'.map x
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✝¹ : Ring T
inst✝ : Algebra R T
h' : IsAdjoinRoot T f
z : R[X]
⊢ (h.algEquiv h') (h.map z) = h'.map z

Tactic:
by
  rw [← h.algEquiv_map h']; simp [-algEquiv_map]

Goal state after:
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
x : T
inst✝ : Algebra R T
hx' : (aeval x) f = 0
⊢ (h.liftHom x hx') h.root = x

Tactic:
by rw [← lift_algebraMap_apply, lift_root]

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
⊢ ↑N ^ (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s * 1 (-1) =
    ↑N ^ (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s

Tactic:
MulChar.one_apply (isUnit_one.neg),

Goal state after:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
⊢ ↑N ^ (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s * 1 =
    ↑N ^ (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: case inl
n : ℕ
inst✝ : NeZero n
h : Differentiable ℂ (LFunctionTrivChar₁ n)
hw : 1 ∈ {s | s = 1 ∨ LFunctionTrivChar n s ≠ 0}
⊢ LFunctionTrivChar₁ n 1 ≠ 0

Tactic:
exact LFunctionTrivChar₁_apply_one_ne_zero _

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 1
⊢ bernoulliFun k 1 = bernoulliFun k 0

Tactic:
bernoulliFun_eval_zero,

Goal state after:
k : ℕ
hk : k ≠ 1
⊢ bernoulliFun k 1 = ↑(bernoulli k)
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
⊢ Polynomial.eval 1 (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli k)) =
    bernoulliFun k 0 + if k = 1 then 1 else 0

Tactic:
bernoulliFun_eval_zero,

Goal state after:
k : ℕ
⊢ Polynomial.eval 1 (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli k)) = ↑(bernoulli k) + if k = 1 then 1 else 0
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: case pos.hf
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
J' : ↑{d | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))}
hJ :
  ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J') ∈
    normalizedFactors (Ideal.map (algebraMap R S) I)
this :
  Multiset.count (↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J'))
      (normalizedFactors (Ideal.map (algebraMap R S) I)) =
    Multiset.count
      (↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx')
          ⟨↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J'), hJ⟩))
      (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)))
hJ' :
  (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx')
      ⟨↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J'), hJ⟩ =
    J'
⊢ Function.Injective fun f ↦ ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f)

Tactic:
· exact Subtype.coe_injective.comp (Equiv.injective _)

Goal state after:
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: case pos.hb
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
J : Ideal S
hJ : J ∈ normalizedFactors (Ideal.map (algebraMap R S) I)
this :
  emultiplicity J (Ideal.map (algebraMap R S) I) =
    emultiplicity (↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩))
      (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
⊢ Ideal.map (algebraMap R S) I ≠ 0

Tactic:
rwa [← bot_eq_zero, Ne,
      map_eq_bot_iff_of_injective (FaithfulSMul.algebraMap_injective R S)]

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

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
n : ℕ
⊢ 2 * ↑k + 1 ≠ -↑n

Tactic:
refine ne_of_gt ((neg_nonpos_of_nonneg n.cast_nonneg).trans_lt ?_)

Goal state after:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
n : ℕ
⊢ 0 < 2 * ↑k + 1