mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case refine_2
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
H : FermatLastTheoremForThreeGen hζ
a b c : ℤ
hc : c ≠ 0
ha : ¬3 ∣ a
hb : ¬3 ∣ b
x✝ : 3 ∣ c
hcoprime : IsCoprime a b
h : a ^ 3 + b ^ 3 = c ^ 3
x : ℤ
hx : c = 3 * x
hdvd : ↑3 ∣ b
⊢ 3 ∣ b

Tactic:
]

Goal state after:
case refine_2
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
H : FermatLastTheoremForThreeGen hζ
a b c : ℤ
hc : c ≠ 0
ha : ¬3 ∣ a
hb : ¬3 ∣ b
x✝ : 3 ∣ c
hcoprime : IsCoprime a b
h : a ^ 3 + b ^ 3 = c ^ 3
x : ℤ
hx : c = 3 * x
hdvd : ↑3 ∣ b
⊢ 3 ∣ b
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 Q : Ideal B
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (algebraMap A B) p
inst✝ : Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
⊢ P * Q ≤ Q

Tactic:
]

Goal state after:
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 Q : Ideal B
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (algebraMap A B) p
inst✝ : Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
⊢ P * Q ≤ Q
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
z : 𝓞 K
hz : S'.c = λ * z
x : 𝓞 K
hx : S'.a ^ 3 - 1 = λ ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 - 1 = λ ^ 4 * y
⊢ IsPrimitiveRoot ζ 3

Tactic:
]

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = λ * z
x : 𝓞 K
hx : S'.a ^ 3 - 1 = λ ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 - 1 = λ ^ 4 * y
⊢ IsPrimitiveRoot ζ 3
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
z : 𝓞 K
hz : S'.c = (hζ✝.toInteger - 1) * z
x : 𝓞 K
hx : S'.a ^ 3 - 1 = (hζ✝.toInteger - 1) ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 - 1 = (hζ✝.toInteger - 1) ^ 4 * y
hζ : IsPrimitiveRoot ζ (3 ^ 1)
⊢ (hζ.toInteger - 1) * (↑S'.u * (hζ✝.toInteger - 1) ^ 2 * z ^ 3 - (hζ✝.toInteger - 1) ^ 3 * (x + y)) =
    ↑S'.u * ((hζ✝.toInteger - 1) * z) ^ 3 - (hζ✝.toInteger - 1) ^ 4 * x - (hζ✝.toInteger - 1) ^ 4 * y

Tactic:
by ring

Goal state after:
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
z : 𝓞 K
hz : S'.c = (hζ✝.toInteger - 1) * z
x : 𝓞 K
hx : S'.a ^ 3 - 1 = (hζ✝.toInteger - 1) ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 - 1 = (hζ✝.toInteger - 1) ^ 4 * y
hζ : IsPrimitiveRoot ζ (3 ^ 1)
⊢ S'.a ^ 3 + S'.b ^ 3 - (S'.a ^ 3 - 1) - (S'.b ^ 3 - 1) = S'.a ^ 3 + S'.b ^ 3 - (S'.a ^ 3 - 1) - (S'.b ^ 3 - 1)

Tactic:
]

Goal state after:
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
z : 𝓞 K
hz : S'.c = (hζ✝.toInteger - 1) * z
x : 𝓞 K
hx : S'.a ^ 3 - 1 = (hζ✝.toInteger - 1) ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 - 1 = (hζ✝.toInteger - 1) ^ 4 * y
hζ : IsPrimitiveRoot ζ (3 ^ 1)
⊢ S'.a ^ 3 + S'.b ^ 3 - (S'.a ^ 3 - 1) - (S'.b ^ 3 - 1) = 2

Tactic:
by ring

Goal state after:
Module: Mathlib.NumberTheory.LucasPrimality

Goal state before:
pp: p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h : p ≠ 0 ∧ p ≠ 1
hp1 : 1 < p
this : NeZero p
⊢ Fintype.card (ZMod p)ˣ = p - 1

Tactic:
]

Goal state after:
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h : p ≠ 0 ∧ p ≠ 1
hp1 : 1 < p
this : NeZero p
⊢ Fintype.card (ZMod p)ˣ = p - 1
Module: Mathlib.NumberTheory.LucasPrimality

Goal state before:
pp: p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h : p ≠ 0 ∧ p ≠ 1
hp1 : 1 < p
this : NeZero p
⊢ Nat.Prime p

Tactic:
rw [Nat.prime_iff_card_units]

Goal state after:
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h : p ≠ 0 ∧ p ≠ 1
hp1 : 1 < p
this : NeZero p
⊢ Fintype.card (ZMod p)ˣ = p - 1
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case refine_2
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 Q : Ideal B
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (algebraMap A B) p
inst✝ : Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
this✝¹ : Algebra (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
this✝ : IsScalarTower A (A ⧸ p) (B ⧸ Q)
this : Module.Finite (A ⧸ p) (B ⧸ Q)
e : (B ⧸ Ideal.map (algebraMap A B) p) ≃ₐ[A ⧸ p] (B ⧸ P) × B ⧸ Q :=
  let __spread.0 := (Ideal.quotEquivOfEq ⋯).trans (P.quotientMulEquivQuotientProd Q hPQ);
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
x : B ⧸ P
hx : (Algebra.trace (A ⧸ p) (B ⧸ P)) x ≠ 0
y : B
hy : (Ideal.Quotient.mk (Ideal.map (algebraMap A B) p)) y = e.symm (x, 0)
⊢ ¬(Algebra.trace (A ⧸ p) (B ⧸ P)) (x, 0).1 + (Algebra.trace (A ⧸ p) (B ⧸ Q)) (x, 0).2 = 0

Tactic:
]

Goal state after:
case refine_2
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 Q : Ideal B
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (algebraMap A B) p
inst✝ : Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
this✝¹ : Algebra (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
this✝ : IsScalarTower A (A ⧸ p) (B ⧸ Q)
this : Module.Finite (A ⧸ p) (B ⧸ Q)
e : (B ⧸ Ideal.map (algebraMap A B) p) ≃ₐ[A ⧸ p] (B ⧸ P) × B ⧸ Q :=
  let __spread.0 := (Ideal.quotEquivOfEq ⋯).trans (P.quotientMulEquivQuotientProd Q hPQ);
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
x : B ⧸ P
hx : (Algebra.trace (A ⧸ p) (B ⧸ P)) x ≠ 0
y : B
hy : (Ideal.Quotient.mk (Ideal.map (algebraMap A B) p)) y = e.symm (x, 0)
⊢ ¬(Algebra.trace (A ⧸ p) (B ⧸ P)) (x, 0).1 + (Algebra.trace (A ⧸ p) (B ⧸ Q)) (x, 0).2 = 0
Module: Mathlib.NumberTheory.LucasPrimality

Goal state before:
pp: p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h : p ≠ 0 ∧ p ≠ 1
hp1 : 1 < p
this : NeZero p
⊢ a ^ (p + 1 - Nat.succ 1) = 1

Tactic:
]

Goal state after:
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h : p ≠ 0 ∧ p ≠ 1
hp1 : 1 < p
this : NeZero p
⊢ a ^ (p + 1 - Nat.succ 1) = 1
Module: Mathlib.NumberTheory.LucasPrimality

Goal state before:
pp: p : ℕ
hP : Nat.Prime p
this : Fact (Nat.Prime p)
g : (ZMod p)ˣ
hg : ∀ (x : (ZMod p)ˣ), x ∈ Subgroup.zpowers g
⊢ Nat.Prime p

Tactic:
]

Goal state after:
p : ℕ
hP : Nat.Prime p
this : Fact (Nat.Prime p)
g : (ZMod p)ˣ
hg : ∀ (x : (ZMod p)ˣ), x ∈ Subgroup.zpowers g
⊢ Nat.Prime p
Module: Mathlib.NumberTheory.LucasPrimality

Goal state before:
pp: p : ℕ
hP : Nat.Prime p
this : Fact (Nat.Prime p)
g : (ZMod p)ˣ
hg : ∀ (x : (ZMod p)ˣ), x ∈ Subgroup.zpowers g
h1 : (Units.coeHom (ZMod p)) g ^ (p - 1) = 1 ∧ ∀ m < p - 1, 0 < m → (Units.coeHom (ZMod p)) g ^ m ≠ 1
h2 : 0 < p - 1
⊢ ∃ a, a ^ (p - 1) = 1 ∧ ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1

Tactic:
]

Goal state after:
p : ℕ
hP : Nat.Prime p
this : Fact (Nat.Prime p)
g : (ZMod p)ˣ
hg : ∀ (x : (ZMod p)ˣ), x ∈ Subgroup.zpowers g
h1 : (Units.coeHom (ZMod p)) g ^ (p - 1) = 1 ∧ ∀ m < p - 1, 0 < m → (Units.coeHom (ZMod p)) g ^ m ≠ 1
h2 : 0 < p - 1
⊢ ∃ a, a ^ (p - 1) = 1 ∧ ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case refine_2
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
inst✝¹ : Finite (A ⧸ p)
P Q : Ideal B
inst✝ : P.IsMaximal
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (algebraMap A B) p
⊢ P * Q ≤ P

Tactic:
]

Goal state after:
case refine_2
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
inst✝¹ : Finite (A ⧸ p)
P Q : Ideal B
inst✝ : P.IsMaximal
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (algebraMap A B) p
⊢ P * Q ≤ P
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
this : 2 = ↑2
⊢ χ₈ ↑p = χ₈ ↑p

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
this : -2 = ↑(-2)
⊢ χ₈' ↑p = χ₈' ↑p

Tactic:
]

Goal state after:
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
z : 𝓞 K
hz : S'.c = λ * z
x : 𝓞 K
hx : S'.a ^ 3 + 1 = λ ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 + 1 = λ ^ 4 * y
⊢ IsPrimitiveRoot ζ 3

Tactic:
]

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = λ * z
x : 𝓞 K
hx : S'.a ^ 3 + 1 = λ ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 + 1 = λ ^ 4 * y
⊢ IsPrimitiveRoot ζ 3
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ p % 8 ≠ 3 ∧ p % 8 ≠ 5 ↔ p % 8 = 1 ∨ p % 8 = 7

Tactic:
]

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ p % 8 ≠ 3 ∧ p % 8 ≠ 5 ↔ p % 8 = 1 ∨ p % 8 = 7
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ p % 8 ≠ 5 ∧ p % 8 ≠ 7 ↔ p % 8 = 1 ∨ p % 8 = 3

Tactic:
]

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ p % 8 ≠ 5 ∧ p % 8 ≠ 7 ↔ p % 8 = 1 ∨ p % 8 = 3
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
hp : p ≠ ⊥
P : Ideal B
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P * a
hPa : P ∣ a
⊢ P * P ∣ P * a

Tactic:
]

Goal state after:
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
hp : p ≠ ⊥
P : Ideal B
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P * a
hPa : P ∣ a
⊢ P * P ∣ P * a
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity

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

Tactic:
]

Goal state after:
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
hp₁ : p % 2 = 1
hq₁ : q % 2 = 1
hq₂ : ringChar (ZMod q) ≠ 2
h : (quadraticChar (ZMod p)) ↑q = (quadraticChar (ZMod q)) (↑(χ₄ ↑p) * ↑p)
⊢ legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))
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
z : 𝓞 K
hz : S'.c = (hζ✝.toInteger - 1) * z
x : 𝓞 K
hx : S'.a ^ 3 + 1 = (hζ✝.toInteger - 1) ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 + 1 = (hζ✝.toInteger - 1) ^ 4 * y
hζ : IsPrimitiveRoot ζ (3 ^ 1)
⊢ (hζ.toInteger - 1) * ((hζ✝.toInteger - 1) ^ 3 * (x + y) - ↑S'.u * (hζ✝.toInteger - 1) ^ 2 * z ^ 3) =
    (hζ✝.toInteger - 1) ^ 4 * x + (hζ✝.toInteger - 1) ^ 4 * y - ↑S'.u * ((hζ✝.toInteger - 1) * z) ^ 3

Tactic:
by ring

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
hp : p ≠ ⊥
a : Ideal B
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
inst✝¹ : ⊥.IsMaximal
inst✝ : ⊥.LiesOver p
H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ ⊥)
ha : Ideal.map (algebraMap A B) p = ⊥
hPa : ¬⊥ ∣ a
⊢ Ideal.map (algebraMap A B) p = ⊥

Tactic:
]

Goal state after:
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
hp : p ≠ ⊥
a : Ideal B
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
inst✝¹ : ⊥.IsMaximal
inst✝ : ⊥.LiesOver p
H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ ⊥)
ha : Ideal.map (algebraMap A B) p = ⊥
hPa : ¬⊥ ∣ a
⊢ Ideal.map (algebraMap A B) p = ⊥
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
z : 𝓞 K
hz : S'.c = (hζ✝.toInteger - 1) * z
x : 𝓞 K
hx : S'.a ^ 3 + 1 = (hζ✝.toInteger - 1) ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 + 1 = (hζ✝.toInteger - 1) ^ 4 * y
hζ : IsPrimitiveRoot ζ (3 ^ 1)
⊢ S'.a ^ 3 + 1 + (S'.b ^ 3 + 1) - (S'.a ^ 3 + S'.b ^ 3) = S'.a ^ 3 + 1 + (S'.b ^ 3 + 1) - (S'.a ^ 3 + S'.b ^ 3)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity

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

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity

Goal state before:
pp: case inl
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
hp : p ≠ 2
inst✝ : Fact (Nat.Prime p)
hq : p ≠ 2
⊢ 0 = 0

Tactic:
]

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
hp : p ≠ ⊥
P : Ideal B
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P * a
hPa : ¬P ∣ a
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this : ∀ x ∈ a, (intTrace A B) x ∈ p
⊢ ↑P = ↑P

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: case succ
n : ℕ
hn : ∏ k ∈ range n, k.fermatNumber = n.fermatNumber - 2
⊢ (2 ^ 2 ^ n) ^ 2 - 1 ^ 2 = 2 ^ 2 ^ (n + 1) + 1 - 2

Tactic:
]

Goal state after:
case succ
n : ℕ
hn : ∏ k ∈ range n, k.fermatNumber = n.fermatNumber - 2
⊢ (2 ^ 2 ^ n) ^ 2 - 1 ^ 2 = 2 ^ 2 ^ (n + 1) + 1 - 2
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
z : 𝓞 K
hz : S'.c = (hζ✝.toInteger - 1) * z
x : 𝓞 K
hx : S'.a ^ 3 + 1 = (hζ✝.toInteger - 1) ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 + 1 = (hζ✝.toInteger - 1) ^ 4 * y
hζ : IsPrimitiveRoot ζ (3 ^ 1)
⊢ S'.a ^ 3 + 1 + (S'.b ^ 3 + 1) - (S'.a ^ 3 + S'.b ^ 3) = 2

Tactic:
by ring

Goal state after:
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: n : ℕ
⊢ n.fermatNumber = n.fermatNumber

pp: n : ℕ
⊢ 2 ≤ n.fermatNumber

Tactic:
]

Goal state after:
n : ℕ
⊢ 2 ≤ n.fermatNumber
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity

Goal state before:
pp: p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 1
hq : q ≠ 2
⊢ legendreSym p ↑q = legendreSym p ↑q

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Fermat

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

Tactic:
]

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
hp : p ≠ ⊥
P : Ideal B
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P * a
hPa : ¬P ∣ a
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this : ∀ x ∈ a, (intTrace A B) x ∈ p
hP : (↑P)⁻¹ = ↑a / ↑(Ideal.map (algebraMap A B) p)
⊢ Submodule.restrictScalars A ↑(↑a / ↑(Ideal.map (algebraMap A B) p)) ≤ comap (↑A (Algebra.trace K L)) 1

Tactic:
]

Goal state after:
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
hp : p ≠ ⊥
P : Ideal B
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P * a
hPa : ¬P ∣ a
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this : ∀ x ∈ a, (intTrace A B) x ∈ p
hP : (↑P)⁻¹ = ↑a / ↑(Ideal.map (algebraMap A B) p)
⊢ Submodule.restrictScalars A ↑(↑a / ↑(Ideal.map (algebraMap A B) p)) ≤ comap (↑A (Algebra.trace K L)) 1
Module: Mathlib.NumberTheory.Fermat

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

Tactic:
]

Goal state after:
n : ℕ
⊢ 2 ^ 2 ^ (n + 2) + 1 + 2 * 2 ^ 2 ^ (n + 1) - 2 * 2 ^ 2 ^ (n + 1) = (2 ^ 2 ^ (n + 1) + 1) ^ 2 - 2 * (2 ^ 2 ^ n) ^ 2
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: n : ℕ
⊢ ↑((n + 1).fermatNumber ^ 2) - ↑(2 * (n.fermatNumber - 1) ^ 2) =
    ↑(n + 1).fermatNumber ^ 2 - 2 * (↑n.fermatNumber - 1) ^ 2

Tactic:
]

Goal state after:
n : ℕ
⊢ ↑((n + 1).fermatNumber ^ 2) - ↑(2 * (n.fermatNumber - 1) ^ 2) =
    ↑(n + 1).fermatNumber ^ 2 - 2 * (↑n.fermatNumber - 1) ^ 2
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity

Goal state before:
pp: p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ -legendreSym p ↑q = -legendreSym p ↑q

pp: case hp
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ p ≠ 2

pp: case hq
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ q ≠ 2

Tactic:
]

Goal state after:
case hp
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ p ≠ 2

case hq
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ q ≠ 2
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: 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

Tactic:
]

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.LegendreSymbol.QuadraticReciprocity

Goal state before:
pp: case hp
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ 1 = 1

pp: case hp
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ p % 4 = 3

Tactic:
]

Goal state after:
case hp
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ p % 4 = 3
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: case h
a k m : ℕ
hm : Odd m
hn : 2 ^ k * m ≠ 0
hP : Prime ((a ^ 2 ^ k) ^ m + 1)
ha : 1 < a ^ 2 ^ k
h : m = 1
⊢ 2 ^ k * m = 2 ^ k

Tactic:
]

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

Goal state before:
pp: case h
a k m : ℕ
hm : Odd m
hn : 2 ^ k * m ≠ 0
hP : Prime ((a ^ 2 ^ k) ^ m + 1)
ha : 1 < a ^ 2 ^ k
h : m = 1
⊢ 2 ^ k = 2 ^ k

Tactic:
]

Goal state after: