mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝²¹ : CommRing A
inst✝²⁰ : Field K
inst✝¹⁹ : CommRing B
inst✝¹⁸ : Field L
inst✝¹⁷ : Algebra A K
inst✝¹⁶ : Algebra B L
inst✝¹⁵ : Algebra A B
inst✝¹⁴ : Algebra K L
inst✝¹³ : Algebra A L
inst✝¹² : IsScalarTower A K L
inst✝¹¹ : IsScalarTower A B L
inst✝¹⁰ : IsDomain A
inst✝⁹ : IsFractionRing A K
inst✝⁸ : FiniteDimensional K L
inst✝⁷ : Algebra.IsSeparable K L
inst✝⁶ : IsIntegralClosure B A L
inst✝⁵ : IsFractionRing B L
inst✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this✝ : Ideal.map (algebraMap A B) p ∣ a ^ e
this : ∀ x ∈ a, (intTrace A B) x ∈ p
⊢ P ^ (e - 1) ∣ differentIdeal A B

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑(⋯.unit ^ 2) - ↑n
⊢ Nat.Coprime 2 3

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑(⋯.unit ^ 2) - ↑n
⊢ 3 ≠ 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑(-⋯.unit ^ 2) - ↑n
⊢ Nat.Coprime 2 3

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑(-⋯.unit ^ 2) - ↑n
⊢ 3 ≠ 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
n : ℤ
x : 𝓞 K
hx : ↑(-⋯.unit ^ 2) - ↑n = 3 * x
⊢ Nat.Coprime 2 3

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
n : ℤ
x : 𝓞 K
hx : ↑(-⋯.unit ^ 2) - ↑n = 3 * x
⊢ ⋯.toInteger = hζ.toInteger ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, λ ^ 2 ∣ ↑u - ↑n
⊢ u = 1 ∨ u = -1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ 1 < 3

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this✝ : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := (Ideal.Quotient.commRing (Ideal.span {λ})).toRing
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := x✝¹.toAddGroupWithOne.toAddGroup
this : (Ideal.Quotient.mk (Ideal.span {λ})) x ∈ Finset.univ
⊢ 3 ≠ 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this✝ : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := (Ideal.Quotient.commRing (Ideal.span {λ})).toRing
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := x✝¹.toAddGroupWithOne.toAddGroup
this : (Ideal.Quotient.mk (Ideal.span {λ})) x ∈ Finset.univ
⊢ Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Submodule.span ℝ ↑(unitLattice K) = ⊤

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 0 < 1

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ DiscreteTopology ↥(unitLattice K)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ finrank ℝ (logSpace K) = rank K

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ finrank ℤ ↥(unitLattice K) = rank K

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ torsion K = (AddMonoidHom.toMultiplicativeRight (logEmbedding K)).ker

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Function.Injective ⇑(logEmbeddingQuot K)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝¹ x✝ : Additive ((𝓞 K)ˣ ⧸ torsion K)
⊢ ((logEmbeddingQuot K).codRestrict (unitLattice K) ⋯).toIntLinearMap x✝¹ =
      ((logEmbeddingQuot K).codRestrict (unitLattice K) ⋯).toIntLinearMap x✝ →
    x✝¹ = x✝

Tactic:
by

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

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Free ℤ (Additive ((𝓞 K)ˣ ⧸ torsion K))

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Module.Finite ℤ (Additive ((𝓞 K)ˣ ⧸ torsion K))

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Function.Surjective ⇑(MonoidHom.toAdditive (QuotientGroup.mk' (torsion K))).toIntLinearMap

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Module.Finite ℤ (Additive (𝓞 K)ˣ)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Monoid.FG (𝓞 K)ˣ

Tactic:
by

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✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
⊢ P ^ (e - 1) ∣ differentIdeal A B

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ finrank ℤ (Additive ((𝓞 K)ˣ ⧸ torsion K)) = rank K

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ finrank ℤ (Additive (𝓞 K)ˣ) = rank K

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Fintype.card (Free.ChooseBasisIndex ℤ (Additive ((𝓞 K)ˣ ⧸ torsion K))) = Fintype.card (Fin (rank K))

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i : Fin (rank K)
⊢ Additive.ofMul ↑(fundSystem K i) = (basisModTorsion K) i

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i : Fin (rank K)
⊢ (logEmbedding K) (Additive.ofMul (fundSystem K i)) = ↑((basisUnitLattice K) i)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
⊢ ↑⋯.unit ^ 2 + ↑⋯.unit + 1 = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
⊢ (x - 1) * (x - ↑⋯.unit) * (x - ↑⋯.unit ^ 2) = x ^ 3 - x ^ 2 * (↑η ^ 2 + ↑η + 1) + x * (↑η ^ 2 + ↑η + ↑η ^ 3) - ↑η ^ 3

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
⊢ x ^ 3 - x ^ 2 * (↑η ^ 2 + ↑η + 1) + x * (↑η ^ 2 + ↑η + ↑η ^ 3) - ↑η ^ 3 =
    x ^ 3 - x ^ 2 * (↑η ^ 2 + ↑η + 1) + x * (↑η ^ 2 + ↑η + 1) - 1

Tactic:
by

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

Goal state before:
pp: 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 A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
⊢ P ^ (e - 1) ∣ differentIdeal A B

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
⊢ x ^ 3 - x ^ 2 * (↑η ^ 2 + ↑η + 1) + x * (↑η ^ 2 + ↑η + 1) - 1 = x ^ 3 - 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
⊢ x ^ 3 - 1 = (x - 1) * (x - ↑⋯.unit) * (x - ↑⋯.unit ^ 2)

Tactic:
by

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

Goal state before:
pp: n : ZMod 9
⊢ (castHom ⋯ (ZMod 3)) n ≠ 0 → n ^ 3 = 1 ∨ n ^ 3 = 8

Tactic:
by

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

Goal state before:
pp: n : ℤ
h : ¬3 ∣ n
⊢ ↑n ^ 3 = 1 ∨ ↑n ^ 3 = 8

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ λ ∣ x * (x - 1) * (x - (↑⋯.unit + 1))

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: 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 A
P Q : Ideal B
hP : P * Q = Ideal.map (algebraMap A B) p
x : B
hxQ : x ∈ Q
hx : (intTrace A B) x ∉ p
hp : ¬p = ⊥
⊢ p ≤ Ideal.comap (algebraMap A B) Q

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x y : 𝓞 K
hy : x - 1 = λ * y
⊢ x ^ 3 - 1 = (x - 1) * (x - 1 - λ) * (x - 1 - λ * (↑η + 1))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x y : 𝓞 K
hy : x - 1 = λ * y
⊢ (x - 1) * (x - 1 - λ) * (x - 1 - λ * (↑η + 1)) = λ ^ 3 * (y * (y - 1) * (y - (↑η + 1)))

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
⊢ ∃! ζe, x = ↑ζe.1 * ∏ i, fundSystem K i ^ ζe.2 i

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x y : 𝓞 K
hy : x - 1 = λ * y
⊢ x ^ 3 - 1 = λ ^ 3 * (y * (y - 1) * (y - (↑η + 1)))

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Subgroup.closure (Set.range (fundSystem K)) ⊔ torsion K = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : λ ∣ x - 1
⊢ λ ^ 4 ∣ x ^ 3 - 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n : ℕ
⊢ ¬n.Pseudoperfect ↔ n = 0 ∨ ∀ s ⊆ n.properDivisors, ∑ i ∈ s, i ≠ n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: ⊢ ¬Deficient 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: ⊢ Deficient 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: ⊢ Deficient 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: ⊢ Deficient 3

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: ⊢ ¬Abundant 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: ⊢ Abundant 12

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: ⊢ ¬Weird 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: ⊢ Weird 70

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n : ℕ
h : n.Deficient
⊢ 0 < n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n : ℕ
h : n.Abundant
⊢ 0 < n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n : ℕ
h : n.Weird
⊢ 0 < n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ n.Deficient ↔ ¬n.Abundant ∧ ¬n.Perfect

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n : ℕ
hn : 0 ≠ n
⊢ n.Perfect ↔ ¬n.Abundant ∧ ¬n.Deficient

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n : ℕ
hn : 0 ≠ n
⊢ n.Abundant ↔ ¬n.Perfect ∧ ¬n.Deficient

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n : ℕ
hn : 0 ≠ n
⊢ n.Deficient ∨ n.Abundant ∨ n.Perfect

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n : ℕ
h : Prime n
⊢ ¬n.Weird

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: p : ℕ
h : Prime p
⊢ ¬p.Pseudoperfect

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : λ ∣ x + 1
⊢ λ ∣ -x - 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n m : ℕ
h : Prime n
h✝ : m > 0
⊢ ∑ x ∈ map { toFun := fun x ↦ n ^ x, inj' := ⋯ } (range m), x = ∑ i ∈ range m, n ^ i

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n m : ℕ
h : Prime n
⊢ (n ^ m).Deficient

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n : ℕ
h : IsPrimePow n
⊢ n.Deficient

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : λ ∣ x + 1
⊢ λ ^ 4 ∣ x ^ 3 + 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: ⊢ {n | n.Deficient}.Infinite

Tactic:
by

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

Goal state before:
pp: a b c : ℤ
hdvd : ¬3 ∣ a * b * c
⊢ a ^ 3 + b ^ 3 ≠ c ^ 3

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n : ℕ
⊢ 2 ^ (n + 1) = 2 ^ n + 2 ^ n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: ⊢ {n | Even n ∧ n.Deficient}.Infinite

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n p : ℕ
left✝ : max (n + 1) 3 ≤ p
h2 : Prime p
⊢ 2 < p

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n p : ℕ
left✝ : max (n + 1) 3 ≤ p
h2 : Prime p
⊢ n < p

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: ⊢ {n | Odd n ∧ n.Deficient}.Infinite

Tactic:
by

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

Goal state before:
pp: a b c : ℤ
ha : a ≠ 0
Hgcd : {a, b, c}.gcd id = 1
h3a : 3 ∣ a
HF : b ^ 3 + c ^ 3 + a ^ 3 = 0
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
⊢ {b, c, a}.gcd id = 1

Tactic:
convert! Hgcd using 2

Goal state after:
a b c : ℤ
ha : a ≠ 0
Hgcd : {a, b, c}.gcd id = 1
h3a : 3 ∣ a
HF : b ^ 3 + c ^ 3 + a ^ 3 = 0
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
⊢ {b, c, a} = {a, b, c}
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n : ℕ
⊢ n.Abundant ↔ 2 * n < ∑ i ∈ n.divisors, i

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n : ℕ
h : ¬n = 0
⊢ 0 < ↑n

Tactic:
by

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

Goal state before:
pp: a b c : ℤ
ha : a ≠ 0
Hgcd : {a, b, c}.gcd id = 1
h3a : 3 ∣ a
HF : a ^ 3 + b ^ 3 + c ^ 3 = 0
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
⊢ IsCoprime (-b) (-c)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n : ℕ
⊢ n.Abundant ↔ 2 < n.abundancyIndex

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n m : ℕ
hn : n ≠ 0
k : ℕ
hk : n = m * k
⊢ k ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n m : ℕ
hn : n ≠ 0
k : ℕ
hk : n = m * k
hk0 : k ≠ 0
⊢ 0 < ↑k

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n m : ℕ
hn : n ≠ 0
k : ℕ
hk : n = m * k
hk0 : k ≠ 0
⊢ image (fun a ↦ a * k) m.divisors ⊆ (m * k).divisors

Tactic:
by

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

Goal state before:
pp: 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 A
P Q : Ideal B
hP : P * Q = Ideal.map (algebraMap A B) p
x : B
hxQ : x ∈ Q
hx : (intTrace A B) x ∉ p
hp : ¬p = ⊥
this✝² : Algebra (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
this✝¹ : IsLocalization (algebraMapSubmonoid B A⁰) L
this✝ : FiniteDimensional K L
H : ↑Q ≤ FractionalIdeal.dual A K 1 * ↑(Ideal.map (algebraMap A B) p)
hne : 1 ≠ 0
this : (Algebra.trace K L) ((algebraMap B L) x) ∈ ↑p
⊢ (intTrace A B) x ∈ p

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n m : ℕ
hn : n ≠ 0
hd : m ∣ n
⊢ m.abundancyIndex ≤ n.abundancyIndex

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n m : ℕ
h : m.Abundant
hd : m ∣ n
hn : n ≠ 0
⊢ n.Abundant

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n m : ℕ
h : n.Abundant
hm : m ≠ 0
⊢ n ≠ 0

Tactic:
by

Goal state after: