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

Goal state before:
pp: case refine_1
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 := numberField {p ^ (k + 1)} ℚ K
h : hζ.toInteger - 1 = 0
⊢ False

Tactic:
apply hζ.pow_ne_one_of_pos_of_lt one_ne_zero (one_lt_pow₀ hp.out.one_lt (by simp))

Goal state after:
case refine_1
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 = 0
⊢ ζ ^ 1 = 1
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
n : ℕ
inst✝ : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
h₁ : 2 < n
h₂ : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
this✝ : NumberField K
this : NeZero n
⊢ (Algebra.norm ℚ) ((algebraMap (𝓞 K) K) hζ.toInteger - (algebraMap (𝓞 K) K) 1) = (algebraMap ℤ ℚ) 1

Tactic:
map_one,

Goal state after:
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
n : ℕ
inst✝ : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
h₁ : 2 < n
h₂ : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
this✝ : NumberField K
this : NeZero n
⊢ (Algebra.norm ℚ) ((algebraMap (𝓞 K) K) hζ.toInteger - 1) = (algebraMap ℤ ℚ) 1
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
n : ℕ
inst✝ : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
h₁ : 2 < n
h₂ : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
this✝ : NumberField K
this : NeZero n
⊢ (Algebra.norm ℚ) ((algebraMap (𝓞 K) K) hζ.toInteger - 1) = (algebraMap ℤ ℚ) 1

Tactic:
map_one,

Goal state after:
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
n : ℕ
inst✝ : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
h₁ : 2 < n
h₂ : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
this✝ : NumberField K
this : NeZero n
⊢ (Algebra.norm ℚ) ((algebraMap (𝓞 K) K) hζ.toInteger - 1) = 1
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 ℚ) ((algebraMap (𝓞 K) K) hζ.toInteger - (algebraMap (𝓞 K) K) 1) = (algebraMap ℤ ℚ) 2

Tactic:
map_one,

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.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))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : 1 < pB.dim
h : (pB.basis.repr hζ.toInteger) ⟨1, hdim⟩ = (pB.basis.repr (↑p * x + ↑n)) ⟨1, hdim⟩
this : pB.basis ⟨1, hdim⟩ = hζ.toInteger ^ ↑⟨1, hdim⟩
⊢ False

Tactic:
simp only [PowerBasis.coe_basis, pow_one] at 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))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : 1 < pB.dim
h : (pB.basis.repr hζ.toInteger) ⟨1, hdim⟩ = (pB.basis.repr (↑p * x + ↑n)) ⟨1, hdim⟩
this : pB.gen = hζ.toInteger
⊢ False
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✝⁴ : IsFractionRing A K
inst✝³ : IsDomain A
inst✝² : IsFractionRing B L
inst✝¹ : IsDomain B
inst✝ : FaithfulSMul A B
I : Submodule B (FractionRing B)
x : L
y : FractionRing B
hy : y ∈ I
⊢ (∃ y_1,
      (algebraMap A (FractionRing A)) y_1 =
        (FractionRing.algEquiv A K).toRingEquiv.symm
          ((Algebra.trace K L) ((FractionRing.algEquiv B L).toRingEquiv ((FractionRing.algEquiv B L).symm x * y)))) ↔
    ∃ y_1, (algebraMap A K) y_1 = (Algebra.trace K L) (x * (FractionRing.algEquiv B L) y)

Tactic:
simp only [map_mul, AlgEquiv.coe_ringEquiv,
    AlgEquiv.apply_symm_apply, ← AlgEquiv.symm_toRingEquiv, AlgEquiv.algebraMap_eq_apply]

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✝³ : IsFractionRing A K
inst✝² : IsIntegrallyClosed A
inst✝¹ : FiniteDimensional K L
inst✝ : IsIntegralClosure B A L
x : B
⊢ IsIntegral A ((↑A (Algebra.trace K L)) ((Algebra.linearMap B L) x))

Tactic:
apply isIntegral_trace

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✝³ : IsFractionRing A K
inst✝² : IsIntegrallyClosed A
inst✝¹ : FiniteDimensional K L
inst✝ : IsIntegralClosure B A L
x : B
⊢ IsIntegral A ((Algebra.linearMap B L) x)
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 ℚ) ((algebraMap (𝓞 K) K) hζ.toInteger - (algebraMap (𝓞 K) K) 1) =
    (algebraMap ℤ ℚ) ((Algebra.norm ℤ) (⋯.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K)

Tactic:
map_one,

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.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case pos
n : ℕ
hn✝ : 2 ≤ n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp : ↑p ∣ (Algebra.norm ℤ) (hμ.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
h✝ : (Algebra.norm ℤ) (hζ.toInteger - 1) = (Algebra.norm ℤ) (hμ.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
hn : 2 < n
h : ∃ q, Nat.Prime q ∧ ∃ t, q ^ t = n
⊢ ∃ q, Nat.Prime q ∧ ∃ t s, t ≠ 0 ∧ n = q ^ t ∧ ↑p ∣ ↑q ^ s

pp: case neg
n : ℕ
hn✝ : 2 ≤ n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp : ↑p ∣ (Algebra.norm ℤ) (hμ.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
h✝ : (Algebra.norm ℤ) (hζ.toInteger - 1) = (Algebra.norm ℤ) (hμ.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
hn : 2 < n
h : ∀ (q : ℕ), Nat.Prime q → ∀ (t : ℕ), q ^ t ≠ n
⊢ ∃ q, Nat.Prime q ∧ ∃ t s, t ≠ 0 ∧ n = q ^ t ∧ ↑p ∣ ↑q ^ s

Tactic:
· obtain ⟨q, hq, t, hn'⟩ := h
        have : Fact (Nat.Prime q) := ⟨hq⟩
        cases t with
        | zero => simp [← hn'] at hn
        | succ r =>
          rw [← hn'] at hC hμ
          refine ⟨q, hq, r + 1, Module.finrank (ℚ⟮ζ⟯) K, r.add_one_ne_zero, hn'.symm, ?_⟩
          by_cases hq' : q = 2
          · cases r with
            | zero =>
                rw [← hn', hq', zero_add, pow_one] at hn
                exact hn.false.elim
            | succ k =>
                rw [hq'] at hC hμ ⊢
                rwa [hμ.norm_toInteger_sub_one_of_eq_two_pow] at hp
          · rwa [hμ.norm_toInteger_sub_one_of_prime_ne_two hq'] at hp

Goal state after:
case neg
n : ℕ
hn✝ : 2 ≤ n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp : ↑p ∣ (Algebra.norm ℤ) (hμ.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
h✝ : (Algebra.norm ℤ) (hζ.toInteger - 1) = (Algebra.norm ℤ) (hμ.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
hn : 2 < n
h : ∀ (q : ℕ), Nat.Prime q → ∀ (t : ℕ), q ^ t ≠ n
⊢ ∃ q, Nat.Prime q ∧ ∃ t s, t ≠ 0 ∧ n = q ^ t ∧ ↑p ∣ ↑q ^ s
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
hI : I ≠ 0
b : B
hb : b ∈ B⁰
hb' : ∀ b_1 ∈ ↑I, IsInteger B (b • b_1)
a : L
ha : a ∈ I
⊢ IsIntegral A (((traceForm K L) ((algebraMap B L) b)) a)

Tactic:
apply isIntegral_trace

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 : FractionalIdeal B⁰ L
hI : I ≠ 0
b : B
hb : b ∈ B⁰
hb' : ∀ b_1 ∈ ↑I, IsInteger B (b • b_1)
a : L
ha : a ∈ I
⊢ IsIntegral A (((lmul K L).toLinearMap ((algebraMap B L) b)) a)
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
hIJ : I * J ≤ 1
x : L
hx : x ∈ J
y : L
hy : y ∈ Submodule.restrictScalars A ↑I
⊢ IsIntegral A (((traceForm K L) x) y)

Tactic:
apply isIntegral_trace

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
hIJ : I * J ≤ 1
x : L
hx : x ∈ J
y : L
hy : y ∈ Submodule.restrictScalars A ↑I
⊢ IsIntegral A (((lmul K L).toLinearMap x) y)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case e'_3
p k : ℕ
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) (p ^ k)
this : NumberField K
pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
⊢ (-(Int.castRingHom ℚ) 1) ^ (φ (p ^ k) / 2) * (Int.castRingHom ℚ) ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1)) =
    (-1) ^ (φ (p ^ k) / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1))

Tactic:
map_one,

Goal state after:
case e'_3
p k : ℕ
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) (p ^ k)
this : NumberField K
pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
⊢ (-1) ^ (φ (p ^ k) / 2) * (Int.castRingHom ℚ) ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1)) =
    (-1) ^ (φ (p ^ k) / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1))
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
⊢ 1 ≤ B

Tactic:
contrapose! hB

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : B < 1
⊢ ↑(convexBodyLTFactor K) * ↑B ≤ minkowskiBound K 1
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : ↥(unitLattice K)
a : logSpace K
b : Additive (𝓞 K)ˣ
left✝ : b ∈ ↑⊤
ha : (logEmbedding K).toIntLinearMap b = a
⊢ ((logEmbeddingQuot K).codRestrict (unitLattice K) ⋯).toIntLinearMap ⟦b⟧ = ⟨a, ⋯⟩

Tactic:
simpa using! ha

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: case neg
n : ℕ
h : ¬n = 0
⊢ 2 * n < ∑ i ∈ n.divisors, i ↔ 2 < ↑(∑ i ∈ n.divisors, i) / ↑n

Tactic:
lt_div_iff₀ (by positivity)

Goal state after:
case neg
n : ℕ
h : ¬n = 0
⊢ 2 * n < ∑ i ∈ n.divisors, i ↔ 2 * ↑n < ↑(∑ i ∈ n.divisors, i)
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: a : ℕ
ha : Abundant 945
⊢ ∃ b ∈ {n | Odd n ∧ n.Abundant}, a < b

Tactic:
use (2 * a + 1) * 945

Goal state after:
case h
a : ℕ
ha : Abundant 945
⊢ (2 * a + 1) * 945 ∈ {n | Odd n ∧ n.Abundant} ∧ a < (2 * a + 1) * 945
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

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

Tactic:
have h₀ := FiniteField.unit_isSquare_iff (by rwa [ringChar_zmod_n]) x
    have hs : (∃ y : (ZMod p)ˣ, y ^ 2 = x) ↔ IsSquare x := by
      rw [isSquare_iff_exists_sq x]
      simp_rw [eq_comm]
    rw [hs]
    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
hF : ringChar F ≠ 2
a : F
s : Finset F := {x | x ^ 2 = a}.toFinset
b : F
h₀ : ¬b = 0
h : a = b * b
⊢ s = [b, -b].toFinset

Tactic:
ext1

Goal state after:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := {x | x ^ 2 = a}.toFinset
b : F
h₀ : ¬b = 0
h : a = b * b
a✝ : F
⊢ a✝ ∈ s ↔ a✝ ∈ [b, -b].toFinset
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: a n : ℕ
ha : 1 < a
hn : n ≠ 0
hP : Prime (a ^ n + 1)
⊢ ∃ m, n = 2 ^ m

Tactic:
obtain ⟨k, m, hm, rfl⟩ := exists_eq_two_pow_mul_odd hn

Goal state after:
a : ℕ
ha : 1 < a
k m : ℕ
hm : Odd m
hn : 2 ^ k * m ≠ 0
hP : Prime (a ^ (2 ^ k * m) + 1)
⊢ ∃ m_1, 2 ^ k * m = 2 ^ m_1
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ 1 < a ^ 1

Tactic:
simpa using! ha

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

Goal state before:

Tactic:
_ = S'.u⁻¹ * (λ ^ 4 * x + λ ^ 4 * y) := by ring
    _ = S'.u⁻¹ * (S'.a ^ 3 + S'.b ^ 3) := by rw [← hx, ← hy]; ring
    _ = S'.u⁻¹ * (S'.u * S'.c ^ 3) := by rw [S'.H]
    _ = S'.c ^ 3 := by simp

Goal state after:
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: 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
rx : ℕ
hrx : r = setGcd s * rx
⊢ r + n = ∑ c, (if 0 ≤ a c then rx else x / setGcd s - rx) * (a c).natAbs * ↑c

Tactic:
← Int.natCast_inj,

Goal state after:
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
rx : ℕ
hrx : r = setGcd s * rx
⊢ ↑(r + n) = ↑(∑ c, (if 0 ≤ a c then rx else x / setGcd s - rx) * (a c).natAbs * ↑c)
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: 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
rx : ℕ
hrx : r = setGcd s * rx
⊢ ∑ x_1, (↑rx * a x_1 + ↑(x / setGcd s) * ↑(-a x_1).toNat) * ↑↑x_1 =
    ∑ x_1, ↑(if 0 ≤ a x_1 then rx else x / setGcd s - rx) * ↑(a x_1).natAbs * ↑↑x_1

Tactic:
congr! 2 with i

Goal state after:
case a
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
rx : ℕ
hrx : r = setGcd s * rx
i : ↥t
a✝ : i ∈ Finset.univ
⊢ ↑rx * a i + ↑(x / setGcd s) * ↑(-a i).toNat = ↑(if 0 ≤ a i then rx else x / setGcd s - rx) * ↑(a i).natAbs
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.X ^ 3 * ↑S.u₁ * λ ^ (3 * S.multiplicity - 2) + S.Y ^ 3 * ↑S.u₂ * λ * ↑η + S.Z ^ 3 * ↑S.u₃ * λ * ↑η ^ 2 = 0

Tactic:
by
  rw [X_u₁_spec, Y_u₂_spec, Z_u₃_spec, mul_comm S.x, ← x_spec, mul_comm S.y, ← y_spec, mul_comm S.z,
    ← z_spec, eta_sq]
  calc _ = S.a+S.b+η^2*S.b-S.a+η^2*S.b+2*η*S.b+S.b := by ring
  _ = 0 := by rw [eta_sq]; ring

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
hx : x ≠ 0
this✝¹ : Nonempty { j // x j ≠ 0 }
this✝ : HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x ↑i)
v : ↑nonarchAbsVal
i : ι
hi : x i ≠ 0
this : Nonempty ι
j : ι
⊢ ↑v (x j) ≤ ⨆ i, ↑v (x ↑i)

Tactic:
rcases eq_or_ne (x j) 0 with h | h

Goal state after:
case inl
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
hx : x ≠ 0
this✝¹ : Nonempty { j // x j ≠ 0 }
this✝ : HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x ↑i)
v : ↑nonarchAbsVal
i : ι
hi : x i ≠ 0
this : Nonempty ι
j : ι
h : x j = 0
⊢ ↑v (x j) ≤ ⨆ i, ↑v (x ↑i)

case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
hx : x ≠ 0
this✝¹ : Nonempty { j // x j ≠ 0 }
this✝ : HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x ↑i)
v : ↑nonarchAbsVal
i : ι
hi : x i ≠ 0
this : Nonempty ι
j : ι
h : x j ≠ 0
⊢ ↑v (x j) ≤ ⨆ i, ↑v (x ↑i)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
⊢ mulHeight x = mulHeight fun i ↦ x ↑i

Tactic:
classical
  let e := Equiv.Set.sumCompl x.support
  have hx : x ∘ e = Sum.elim (fun i : x.support ↦ x i.val) 0 := by
    ext1 i
    simp only [comp_apply]
    cases i with
    | inl val => simp [e]
    | inr val => exact notMem_support.mp <| (Set.mem_compl_iff _ _).mp val.prop
  rw [← mulHeight_comp_equiv e, hx]
  exact mulHeight_sumElim_zero_eq ..

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

Goal state before:
pp: case e'_5
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_5
inst✝ : Subsingleton ι
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
j : ι
⊢ ((x i)⁻¹ • x) j = 1 j

Tactic:
simpa [Subsingleton.elim j i] using inv_mul_cancel₀ hi

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x y : ι → K
hι : Nonempty ι
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y = (fun a ↦ x a.1 * y a.2) ∘ Function.diag

Tactic:
ext1

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x y : ι → K
hι : Nonempty ι
hx : x ≠ 0
hy : y ≠ 0
x✝ : ι
⊢ (x * y) x✝ = ((fun a ↦ x a.1 * y a.2) ∘ Function.diag) x✝
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case inr
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
ι' : Type u_6
inst✝ : AdmissibleAbsValues K
h✝ : Nonempty ι'
⊢ (if archAbsVal.card = 0 then 1 else 0) * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ j, 1 ≤ 1

Tactic:
simp
    grind

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

Goal state before:
pp: case inr.inr
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
⊢ (mulHeight fun j ↦ (eval x) (p j)) ≤ max (mulHeightBound p) 1 * mulHeight x ^ N

Tactic:
have H₁ :
     0 ≤ (archAbsVal.map (fun v ↦ ⨆ j, (AddMonoidAlgebra.coeff <| p j).sum fun _ c ↦ v c)).prod :=
    prod_map_nonneg fun v _ ↦ H₀ v

Goal state after:
case inr.inr
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
⊢ (mulHeight fun j ↦ (eval x) (p j)) ≤ max (mulHeightBound p) 1 * mulHeight x ^ N
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case inl
h : riemannZeta 1 = ↑((γ - Real.log (4 * π)) / 2)
⊢ riemannZeta ((starRingEnd ℂ) 1) = (starRingEnd ℂ) (riemannZeta 1)

Tactic:
map_one,

Goal state after:
case inl
h : riemannZeta 1 = ↑((γ - Real.log (4 * π)) / 2)
⊢ riemannZeta 1 = (starRingEnd ℂ) (riemannZeta 1)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: s : ℂ
hs : s ≠ 1
hg_an : AnalyticOnNhd ℂ (fun z ↦ (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z))) {1}ᶜ
z : ℂ
hz : 1 < z.re
n : ℕ
⊢ (starRingEnd ℂ) 1 / (starRingEnd ℂ) (↑n ^ (starRingEnd ℂ) z) = 1 / ↑n ^ z

Tactic:
map_one,

Goal state after:
s : ℂ
hs : s ≠ 1
hg_an : AnalyticOnNhd ℂ (fun z ↦ (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z))) {1}ᶜ
z : ℂ
hz : 1 < z.re
n : ℕ
⊢ 1 / (starRingEnd ℂ) (↑n ^ (starRingEnd ℂ) z) = 1 / ↑n ^ z