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

Goal state before:
pp: p : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ (n✝ + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (n✝ + 1))
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ (n✝ + 1)} ℚ K
hun : Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑p ^ n
H : (algebraMap ℚ K) ↑p ^ n * x ∈ ℤ[B.gen]
h₁ : minpoly ℚ (ζ - 1) = map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1))
h₂ : minpoly ℚ (ζ - 1) = (cyclotomic (p ^ (n✝ + 1)) ℚ).comp (X + 1)
⊢ (minpoly ℤ B.gen).IsEisensteinAt (ℤ ∙ ↑p)

Tactic:
rw [h₁, ← map_cyclotomic_int, ← algebraMap_int_eq,
        show X + 1 = map (algebraMap ℤ ℚ) (X + 1) by simp, ← map_comp] at h₂

Goal state after:
p : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ (n✝ + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (n✝ + 1))
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ (n✝ + 1)} ℚ K
hun : Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑p ^ n
H : (algebraMap ℚ K) ↑p ^ n * x ∈ ℤ[B.gen]
h₁ : minpoly ℚ (ζ - 1) = map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1))
h₂ : map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1)) = map (algebraMap ℤ ℚ) ((cyclotomic (p ^ (n✝ + 1)) ℤ).comp (X + 1))
⊢ (minpoly ℤ B.gen).IsEisensteinAt (ℤ ∙ ↑p)
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
B : Type ?u.10
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
I : Submodule B L
c : B
x : L
hx : x ∈ ((traceForm K L).dualSubmodule (restrictScalars A I)).carrier
a : L
ha : a ∈ restrictScalars A I
⊢ (Algebra.trace K L) (x * c • a) ∈ 1

Tactic:
exact hx _ (Submodule.smul_mem _ c ha)

Goal state after:
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
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K
h : ↑p ∣ 2
⊢ False

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

Tactic:
· refine hodd <| (prime_dvd_prime_iff_eq ?_ ?_).1 ?_
    · exact Nat.prime_iff.1 hp.1
    · exact Nat.prime_iff.1 Nat.prime_two
    · exact Int.ofNat_dvd.mp h

Goal state after:
case hx
p k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K
h : hζ.toInteger - 1 ∣ ↑2
⊢ Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
⊢ I⁻¹ ≤ dual A K I

Tactic:
exact if hI : I = 0 then by simp [hI] else le_dual_inv_aux A K hI (le_of_eq (mul_inv_cancel₀ hI))

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case neg.a
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
hI : ¬I = 0
⊢ dual A K I ≤ dual A K 1 * I⁻¹

Tactic:
rw [le_mul_inv_iff₀ (pos_iff_ne_zero.2 hI), ← le_dual_iff A K hI]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I J : FractionalIdeal B⁰ L
hI : I ≠ 0
hJ : J ≠ 0
⊢ dual A K I ≤ dual A K J ↔ J ≤ I

Tactic:
← dual_dual A K I

Goal state after:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I J : FractionalIdeal B⁰ L
hI : I ≠ 0
hJ : J ≠ 0
⊢ dual A K I ≤ dual A K J ↔ J ≤ dual A K (dual A K I)
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 := (adjoin.powerBasis' hKx).map ((K[x].equivOfEq ⊤ hx).trans Subalgebra.topEquiv)
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))
y : L
⊢ (minpoly A x).natDegree = (minpoly K x).natDegree

Tactic:
minpoly.isIntegrallyClosed_eq_field_fractions' K hAx,

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 := (adjoin.powerBasis' hKx).map ((K[x].equivOfEq ⊤ hx).trans Subalgebra.topEquiv)
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))
y : L
⊢ (minpoly A x).natDegree = (Polynomial.map (algebraMap A K) (minpoly A x)).natDegree
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
⊢ ⊤ ≤ Submodule.span ℝ ↑(unitLattice K)

Tactic:
suffices B.det v ≠ 0 by
    rw [← isUnit_iff_ne_zero, ← Basis.is_basis_iff_det] at this
    rw [← this.2]
    refine Submodule.span_monotone fun _ ⟨w, hw⟩ ↦ ⟨(exists_unit K w).choose, trivial, hw⟩

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
⊢ B.det v ≠ 0
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
ζ : (𝓞 K)ˣ := x * (∏ i, fundSystem K i ^ ((basisModTorsion K).repr (Additive.ofMul ↑x)) i)⁻¹
⊢ Additive.ofMul (↑x * (↑(∏ i, fundSystem K i ^ ((basisModTorsion K).repr (Additive.ofMul ↑x)) i))⁻¹) = 0

Tactic:
ofMul_mul,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
ζ : (𝓞 K)ˣ := x * (∏ i, fundSystem K i ^ ((basisModTorsion K).repr (Additive.ofMul ↑x)) i)⁻¹
⊢ Additive.ofMul ↑x + Additive.ofMul (↑(∏ i, fundSystem K i ^ ((basisModTorsion K).repr (Additive.ofMul ↑x)) i))⁻¹ = 0
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inl.inl.inl
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 1
hb : ↑b ^ 3 = 1
hc : ↑c ^ 3 = 1
⊢ ¬↑a ^ 3 + ↑b ^ 3 = ↑c ^ 3

Tactic:
rw [ha, hb, hc]

Goal state after:
case inl.inl.inl
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 1
hb : ↑b ^ 3 = 1
hc : ↑c ^ 3 = 1
⊢ ¬1 + 1 = 1
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inl.inl.inr
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 1
hb : ↑b ^ 3 = 1
hc : ↑c ^ 3 = 8
⊢ ¬↑a ^ 3 + ↑b ^ 3 = ↑c ^ 3

Tactic:
rw [ha, hb, hc]

Goal state after:
case inl.inl.inr
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 1
hb : ↑b ^ 3 = 1
hc : ↑c ^ 3 = 8
⊢ ¬1 + 1 = 8
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inl.inr.inl
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 1
hb : ↑b ^ 3 = 8
hc : ↑c ^ 3 = 1
⊢ ¬↑a ^ 3 + ↑b ^ 3 = ↑c ^ 3

Tactic:
rw [ha, hb, hc]

Goal state after:
case inl.inr.inl
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 1
hb : ↑b ^ 3 = 8
hc : ↑c ^ 3 = 1
⊢ ¬1 + 8 = 1
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inl.inr.inr
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 1
hb : ↑b ^ 3 = 8
hc : ↑c ^ 3 = 8
⊢ ¬↑a ^ 3 + ↑b ^ 3 = ↑c ^ 3

Tactic:
rw [ha, hb, hc]

Goal state after:
case inl.inr.inr
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 1
hb : ↑b ^ 3 = 8
hc : ↑c ^ 3 = 8
⊢ ¬1 + 8 = 8
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inr.inl.inl
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 8
hb : ↑b ^ 3 = 1
hc : ↑c ^ 3 = 1
⊢ ¬↑a ^ 3 + ↑b ^ 3 = ↑c ^ 3

Tactic:
rw [ha, hb, hc]

Goal state after:
case inr.inl.inl
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 8
hb : ↑b ^ 3 = 1
hc : ↑c ^ 3 = 1
⊢ ¬8 + 1 = 1
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inr.inl.inr
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 8
hb : ↑b ^ 3 = 1
hc : ↑c ^ 3 = 8
⊢ ¬↑a ^ 3 + ↑b ^ 3 = ↑c ^ 3

Tactic:
rw [ha, hb, hc]

Goal state after:
case inr.inl.inr
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 8
hb : ↑b ^ 3 = 1
hc : ↑c ^ 3 = 8
⊢ ¬8 + 1 = 8
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inr.inr.inl
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 8
hb : ↑b ^ 3 = 8
hc : ↑c ^ 3 = 1
⊢ ¬↑a ^ 3 + ↑b ^ 3 = ↑c ^ 3

Tactic:
rw [ha, hb, hc]

Goal state after:
case inr.inr.inl
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 8
hb : ↑b ^ 3 = 8
hc : ↑c ^ 3 = 1
⊢ ¬8 + 8 = 1
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inr.inr.inr
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 8
hb : ↑b ^ 3 = 8
hc : ↑c ^ 3 = 8
⊢ ¬↑a ^ 3 + ↑b ^ 3 = ↑c ^ 3

Tactic:
rw [ha, hb, hc]

Goal state after:
case inr.inr.inr
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 8
hb : ↑b ^ 3 = 8
hc : ↑c ^ 3 = 8
⊢ ¬8 + 8 = 8
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case neg
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
Hgcd : {a, b, c}.gcd id = 1
hF : a ^ 3 + b ^ 3 = c ^ 3
h1 : ¬3 ∣ a * b * c
⊢ False

pp: case pos
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
Hgcd : {a, b, c}.gcd id = 1
hF : a ^ 3 + b ^ 3 = c ^ 3
h1 : 3 ∣ a * b * c
⊢ False

Tactic:
· exact fermatLastTheoremThree_case_1 h1 hF

Goal state after:
case pos
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
Hgcd : {a, b, c}.gcd id = 1
hF : a ^ 3 + b ^ 3 = c ^ 3
h1 : 3 ∣ a * b * c
⊢ False
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
this : Fact (2 < n.fermatNumber)
⊢ Prime n.fermatNumber

Tactic:
unfold fermatNumber at h this

Goal state after:
n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
this : Fact (2 < 2 ^ 2 ^ n + 1)
⊢ Prime n.fermatNumber
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: s : Set ℕ
hs : ∀ n ∈ s, n = 0
⊢ setGcd s = 0

Tactic:
exact setGcd_eq_zero_iff.mpr hs

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

Goal state before:
pp: n : ℕ
h : 2 ≤ n
⊢ 1 < padicNorm 2 (harmonic n)

Tactic:
padicNorm.eq_zpow_of_nonzero (harmonic_pos (ne_zero_of_lt h)).ne',

Goal state after:
n : ℕ
h : 2 ≤ n
⊢ 1 < ↑2 ^ (-padicValRat 2 (harmonic 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
⊢ IsCoprime S.Y S.Z

Tactic:
rw [← IsCoprime.pow_iff (m := 3) (n := 3) (by decide) (by decide),
    ← isCoprime_mul_unit_right_left S.u₂.isUnit, ← isCoprime_mul_unit_right_right S.u₃.isUnit,
    Y_u₂_spec, Z_u₃_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
⊢ IsCoprime 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
⊢ λ ^ 2 ∣ ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3

Tactic:
use λ^(3*S.multiplicity-5)*S.u₅*(S.X^3)

Goal state after:
case h
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * (λ ^ (3 * S.multiplicity - 5) * ↑S.u₅ * S.X ^ 3)
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
⊢ ∏ᶠ (w : FinitePlace K), w x = ↑|(Algebra.norm ℚ) x|⁻¹

Tactic:
by
  --reduce to 𝓞 K
  rcases IsFractionRing.div_surjective (𝓞 K) x with ⟨a, b, hb, rfl⟩
  apply nonZeroDivisors.ne_zero at hb
  have ha : a ≠ 0 := by
    rintro rfl
    simp at h_x_nezero
  simp_rw [map_div₀, Rat.cast_inv, Rat.cast_abs,
    finprod_div_distrib (hasFiniteMulSupport_int ha) (hasFiniteMulSupport_int hb),
    prod_eq_inv_abs_norm_int ha, prod_eq_inv_abs_norm_int hb]
  rw [← inv_eq_iff_eq_inv, inv_inv_div_inv, ← abs_div]
  congr
  have hb₀ : ((Algebra.norm ℤ) b : ℝ) ≠ 0 := by simp [hb]
  refine (eq_div_of_mul_eq hb₀ ?_).symm
  norm_cast
  rw [coe_norm_int a, coe_norm_int b, ← map_mul,
    div_mul_cancel₀ _ (RingOfIntegers.coe_ne_zero_iff.mpr hb)]

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

Tactic:
have H j : span {x j} ≠ ⊥ := mt span_singleton_eq_bot.mp (hx j)
  have hx' : ⨆ i, span {x i} ≠ ⊥ :=
    iSup_eq_bot.not.mpr <| not_forall.mpr ⟨Classical.ofNonempty, H _⟩
  rw [span_range_eq_iSup, ← finprod_finitePlace_pow_multiplicity hx',
    map_finprod _ <| hasFiniteMulSupport_fun_pow_multiplicity hx' (·), Nat.cast_finprod',
    ← finprod_mul_distrib ?hf <| .iSup (FinitePlace.hasFiniteMulSupport <| mod_cast hx ·)]
  case hf =>
    simp only [map_pow, Nat.cast_pow]
    exact hasFiniteMulSupport_fun_pow_multiplicity hx' fun v ↦ (v.absNorm : ℝ)
  refine finprod_eq_one_of_forall_eq_one fun v ↦ ?_
  have hn := absNorm_eq_zero_iff.not.mpr v.maximalIdeal.ne_bot
  have h {m : ℕ} : (0 : ℝ) < ↑(absNorm v.maximalIdeal.asIdeal ^ m) := by positivity
  rw [multiplicity_iSup _ H, map_pow, mul_eq_one_iff_inv_eq₀ h.ne',
    map_iInf_of_monotone (fun _ ↦ multiplicity ..) (pow_right_monotone <| by lia),
    map_iInf_of_monotone _ Nat.mono_cast,
    map_iInf_of_antitoneOn antitoneOn_inv_pos fun _ ↦ Set.mem_ofPred.mpr h]
  refine iSup_congr fun i ↦ ?_
  rw [← mul_eq_one_iff_inv_eq₀ h.ne', mul_comm, Nat.cast_pow]
  exact apply_mul_absNorm_pow_eq_one v (hx i)

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
hx : x ≠ 0
i₀ : ι
hi₀ : x i₀ ≠ 0 i₀
i' : { j // ↑(x j) ≠ 0 } := ⟨i₀, ⋯⟩
this : Nonempty { j // ↑(x j) ≠ 0 }
hI : span (Set.range x) = span (Set.range fun i ↦ x ↑i)
hx₀ : (fun i ↦ ↑(x i)) ≠ 0
⊢ ↑(absNorm (span (Set.range x))) * ∏ᶠ (v : FinitePlace K), ⨆ i, v ↑(x i) = 1

Tactic:
simp_rw [Finite.iSup_eq_iSup_subtype hx₀, hI]

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
ι : Type u_2
inst✝ : Finite ι
x : ι → 𝓞 K
hx : x ≠ 0
i₀ : ι
hi₀ : x i₀ ≠ 0 i₀
i' : { j // ↑(x j) ≠ 0 } := ⟨i₀, ⋯⟩
this : Nonempty { j // ↑(x j) ≠ 0 }
hI : span (Set.range x) = span (Set.range fun i ↦ x ↑i)
hx₀ : (fun i ↦ ↑(x i)) ≠ 0
⊢ ↑(absNorm (span (Set.range fun i ↦ x ↑i))) * ∏ᶠ (v : FinitePlace K), ⨆ i, v ↑(x ↑i) = 1
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: 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
⊢ (logHeight fun j ↦ (eval x) (p j)) ≤ log (max (mulHeightBound p) 1) + ↑N * logHeight x

Tactic:
by
  simp_rw [logHeight_eq_log_mulHeight]
  pull (disch := positivity) log
  exact (log_le_log <| by positivity) <| mulHeight_eval_le hp x

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

Goal state before:
pp: K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
⊢ mulHeight ![a, b] * mulHeight ![c, d] = mulHeight ![a * c, a * d, b * c, b * d]

Tactic:
simp only [← mulHeight_fun_mul_eq hab hcd]

Goal state after:
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
⊢ (mulHeight fun a_1 ↦ ![a, b] a_1.1 * ![c, d] a_1.2) = mulHeight ![a * c, a * d, b * c, b * d]
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ ∀ᶠ (s : ℂ) in 𝓝[≠] 1, deriv riemannZeta s / riemannZeta s = -(s - 1)⁻¹ + deriv riemannZeta₁ s / riemannZeta₁ s

Tactic:
filter_upwards [eventually_mem_nhdsWithin,
    riemannZeta₁_ne_zero_of_near_one.filter_mono nhdsWithin_le_nhds]

Goal state after:
⊢ ∀ a ∈ {1}ᶜ,
    riemannZeta₁ a ≠ 0 → deriv riemannZeta a / riemannZeta a = -(a - 1)⁻¹ + deriv riemannZeta₁ a / riemannZeta₁ a
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
x : ι → ℤ
hx : x = 0
⊢ 0 ≠ 1

Tactic:
exact zero_ne_one

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

Goal state before:
pp: case succ
F : Type u_1
R : Type u_2
inst✝³ : Fintype F
inst✝² : Field F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
ψ : AddChar F R
n✝ n : ℕ
hn : Nat.succ 0 ≤ n
hn₂ : n + 1 < orderOf χ
gauss_rw : gaussSum (χ ^ n) ψ * gaussSum χ ψ = jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ
ih : gaussSum χ ψ ^ (n + 1) = jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j)
⊢ jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j) =
    gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 (n + 1), jacobiSum χ (χ ^ j)

Tactic:
Finset.prod_Ico_succ_top hn,

Goal state after:
case succ
F : Type u_1
R : Type u_2
inst✝³ : Fintype F
inst✝² : Field F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
ψ : AddChar F R
n✝ n : ℕ
hn : Nat.succ 0 ≤ n
hn₂ : n + 1 < orderOf χ
gauss_rw : gaussSum (χ ^ n) ψ * gaussSum χ ψ = jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ
ih : gaussSum χ ψ ^ (n + 1) = jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j)
⊢ jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j) =
    gaussSum (χ ^ (n + 1)) ψ * ((∏ k ∈ Ico (Nat.succ 0) n, jacobiSum χ (χ ^ k)) * jacobiSum χ (χ ^ n))
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝³ : Fintype F
inst✝² : Field F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
ψ : AddChar F R
hχ : 2 ≤ orderOf χ
hψ : ψ.IsPrimitive
⊢ gaussSum χ ψ ^ orderOf χ = χ (-1) * ↑(Fintype.card F) * ∏ i ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ i)

Tactic:
have := gaussSum_pow_eq_prod_jacobiSum_aux χ ψ (n := orderOf χ - 1) (by lia) (by lia)

Goal state after:
F : Type u_1
R : Type u_2
inst✝³ : Fintype F
inst✝² : Field F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
ψ : AddChar F R
hχ : 2 ≤ orderOf χ
hψ : ψ.IsPrimitive
this :
  gaussSum χ ψ ^ (orderOf χ - 1) = gaussSum (χ ^ (orderOf χ - 1)) ψ * ∏ j ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ j)
⊢ gaussSum χ ψ ^ orderOf χ = χ (-1) * ↑(Fintype.card F) * ∏ i ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ i)
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
h : χ ≠ 1
hχ : (changeLevel hMN) χ ≠ 1
p : ℕ
hp : p ∈ N.primeFactors
⊢ Continuous fun s ↦ 1 - χ ↑p * ↑p ^ (-s)

Tactic:
have : NeZero p := ⟨(Nat.prime_of_mem_primeFactors hp).ne_zero⟩

Goal state after:
M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
h : χ ≠ 1
hχ : (changeLevel hMN) χ ≠ 1
p : ℕ
hp : p ∈ N.primeFactors
this : NeZero p
⊢ Continuous fun s ↦ 1 - χ ↑p * ↑p ^ (-s)
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)
p : ℕ
hp : p ∈ N.primeFactors
⊢ Continuous fun s ↦ 1 - ↑p ^ (-s)

Tactic:
have : NeZero p := ⟨(Nat.prime_of_mem_primeFactors hp).ne_zero⟩

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)
p : ℕ
hp : p ∈ N.primeFactors
this : NeZero p
⊢ Continuous fun s ↦ 1 - ↑p ^ (-s)