mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity

Goal state before:
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
⊢ 1 = 1

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 % 4 = 3

Tactic:
]

Goal state after:
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 % 4 = 3
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity

Goal state before:
pp: case inr
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp1 : p % 4 = 1
hq1 : q ≠ 2
h : p ≠ q
⊢ legendreSym p ↑q = 1 ↔ legendreSym p ↑q = 1

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: case ha
n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
this : Fact (2 < 2 ^ 2 ^ n + 1)
key : 2 ^ n = 2 ^ n - 1 + 1
⊢ 1 = 1

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)
hp3 : p % 4 = 3
hq3 : q % 4 = 3
hpq : p ≠ q
⊢ legendreSym p ↑q = 1 ↔ legendreSym p ↑q = 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)
x : L
hx : ∀ y ∈ ↑(Ideal.map (algebraMap A B) p), x * y ∈ ↑a
⊢ x ∈ 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)
x : L
hx : ∀ y ∈ ↑(Ideal.map (algebraMap A B) p), x * y ∈ ↑a
⊢ x ∈ comap (↑A (Algebra.trace K L)) 1
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: case pos
k : ℕ
hk : Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : k ∣ (k * j) ^ (k * m - 1) - 1
⊢ k ∣ (k * j) ^ (k * m - 1)

Tactic:
]

Goal state after:
case pos
k : ℕ
hk : Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : k ∣ (k * j) ^ (k * m - 1) - 1
⊢ k ∣ (k * j) ^ (k * m - 1)
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: case neg
n b : ℕ
h : n.ProbablePrime b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : ¬2 ≤ n
⊢ Coprime 1 b

Tactic:
]

Goal state after:
case neg
n b : ℕ
h : n.ProbablePrime b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : ¬2 ≤ n
⊢ Coprime 1 b
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: case hd
n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
this : Fact (2 < 2 ^ 2 ^ n + 1)
key : 2 ^ n = 2 ^ n - 1 + 1
p : ℕ
hp1 : Prime p
hp2 : p ∣ 2 ^ 2 ^ n + 1 - 1
⊢ -1 ≠ 1

Tactic:
]

Goal state after:
case hd
n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
this : Fact (2 < 2 ^ 2 ^ n + 1)
key : 2 ^ n = 2 ^ n - 1 + 1
p : ℕ
hp1 : Prime p
hp2 : p ∣ 2 ^ 2 ^ n + 1 - 1
⊢ -1 ≠ 1
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
⊢ n.ProbablePrime b ↔ 1 ≡ b ^ (n - 1) [MOD n]

Tactic:
]

Goal state after:
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
⊢ n.ProbablePrime b ↔ 1 ≡ b ^ (n - 1) [MOD n]
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: n : ℕ
h : 3 ^ ((n.fermatNumber - 1) / 2) = -1
⊢ 3 ^ 2 ^ (2 ^ n - 1) = 3 ^ ((n.fermatNumber - 1) / 2)

Tactic:
]

Goal state after:
n : ℕ
h : 3 ^ ((n.fermatNumber - 1) / 2) = -1
⊢ 3 ^ 2 ^ (2 ^ n - 1) = 3 ^ ((n.fermatNumber - 1) / 2)
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: case e_a
n : ℕ
h : 3 ^ ((n.fermatNumber - 1) / 2) = -1
⊢ 2 ^ (2 ^ n - 1) = 2 ^ (2 ^ n - 1)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
⊢ ↑a ^ 2 ^ n + 1 = 0

Tactic:
]

Goal state after:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
⊢ ↑a ^ 2 ^ n + 1 = 0
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
ha1 : 1 = 0
h : ↑a = 0
⊢ False

Tactic:
]

Goal state after:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
ha1 : 1 = 0
h : ↑a = 0
⊢ False
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
x : 𝓞 K
hx : S'.a ^ 3 - 1 = λ ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 + 1 = λ ^ 4 * y
⊢ λ ^ 4 * (↑S'.u⁻¹ * (x + y)) = ↑S'.u⁻¹ * (λ ^ 4 * x + λ ^ 4 * y)

Tactic:
by ring

Goal state after:
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: case hnot
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
ha1 : ↑a ^ 2 ^ n = -1
ha0 : ↑a ≠ 0
⊢ ¬-1 = 1

Tactic:
]

Goal state after:
case hnot
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
ha1 : ↑a ^ 2 ^ n = -1
ha0 : ↑a ≠ 0
⊢ ¬-1 = 1
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ b < ∑ k ∈ Finset.range b, a ^ k

Tactic:
]

Goal state after:
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ b < ∑ k ∈ Finset.range b, a ^ k
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: case hfin
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
ha1 : ↑a ^ 2 ^ n = -1
ha0 : ↑a ≠ 0
⊢ 1 = 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
x : 𝓞 K
hx : S'.a ^ 3 - 1 = λ ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 + 1 = λ ^ 4 * y
⊢ ↑S'.u⁻¹ * (S'.a ^ 3 - 1 + (S'.b ^ 3 + 1)) = ↑S'.u⁻¹ * (S'.a ^ 3 + S'.b ^ 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
x : 𝓞 K
hx : S'.a ^ 3 - 1 = λ ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 + 1 = λ ^ 4 * y
⊢ ↑S'.u⁻¹ * (S'.a ^ 3 - 1 + (S'.b ^ 3 + 1)) = ↑S'.u⁻¹ * (S'.a ^ 3 + S'.b ^ 3)
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ ∃ i ∈ Finset.range b, 1 < a ^ i

Tactic:
exact ⟨1, Finset.mem_range.mpr (by lia), by simpa using! ha⟩

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

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

Tactic:
]

Goal state after:
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ 2 * a.succ ≤ a ^ b + 1
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
hx : S'.a ^ 3 - 1 = λ ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 + 1 = λ ^ 4 * y
⊢ ↑S'.u⁻¹ * (↑S'.u * S'.c ^ 3) = ↑S'.u⁻¹ * (↑S'.u * S'.c ^ 3)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

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

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)
x : L
hx : ∀ y ∈ ↑(Ideal.map (algebraMap A B) p), x * y ∈ ↑a
⊢ ∀ y ∈ ↑p, (Algebra.trace K L) x * y ∈ ↑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 ≠ ⊥
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)
x : L
hx : ∀ y ∈ ↑(Ideal.map (algebraMap A B) p), x * y ∈ ↑a
⊢ ∀ y ∈ ↑p, (Algebra.trace K L) x * y ∈ ↑p
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: case e'_5
b p : ℕ
x✝ : 2 ≤ b
hp : Odd p
q₁ : b - 1 ∣ b ^ p - 1
q₂ : b + 1 ∣ b ^ p + 1
⊢ b ^ (2 * p) - 1 = (b ^ p) ^ 2 - 1 ^ 2

Tactic:
]

Goal state after:
case e'_5
b p : ℕ
x✝ : 2 ≤ b
hp : Odd p
q₁ : b - 1 ∣ b ^ p - 1
q₂ : b + 1 ∣ b ^ p + 1
⊢ b ^ (2 * p) - 1 = (b ^ p) ^ 2 - 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
x : 𝓞 K
hx : S'.a ^ 3 + 1 = λ ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 - 1 = λ ^ 4 * y
⊢ λ ^ 4 * (↑S'.u⁻¹ * (x + y)) = ↑S'.u⁻¹ * (λ ^ 4 * x + λ ^ 4 * y)

Tactic:
by ring

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: case e'_6
b p : ℕ
x✝ : 2 ≤ b
hp : Odd p
q₁ : b - 1 ∣ b ^ p - 1
q₂ : b + 1 ∣ b ^ p + 1
⊢ b ^ 2 - 1 = b ^ 2 - 1 ^ 2

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: k n : ℕ
hn : 1 < n + succ 1
hp : Prime (k * 2 ^ (n + succ 1 + 1) + 1)
hpdvd : k * 2 ^ (n + succ 1 + 1) + 1 ∣ (n + succ 1).fermatNumber
this : Fact (Prime (k * 2 ^ (n + succ 1 + 1) + 1))
hp2 : k * 2 ^ (n + succ 1 + 1) + 1 ≠ 2
⊢ (k * 2 ^ n % 8 * (2 ^ (succ 1 + 1) % 8) % 8 + 1) % 8 = 1

Tactic:
]

Goal state after:
k n : ℕ
hn : 1 < n + succ 1
hp : Prime (k * 2 ^ (n + succ 1 + 1) + 1)
hpdvd : k * 2 ^ (n + succ 1 + 1) + 1 ∣ (n + succ 1).fermatNumber
this : Fact (Prime (k * 2 ^ (n + succ 1 + 1) + 1))
hp2 : k * 2 ^ (n + succ 1 + 1) + 1 ≠ 2
⊢ (k * 2 ^ n % 8 * (2 ^ (succ 1 + 1) % 8) % 8 + 1) % 8 = 1
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
hx : S'.a ^ 3 + 1 = λ ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 - 1 = λ ^ 4 * y
⊢ ↑S'.u⁻¹ * (S'.a ^ 3 + 1 + (S'.b ^ 3 - 1)) = ↑S'.u⁻¹ * (S'.a ^ 3 + S'.b ^ 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
x : 𝓞 K
hx : S'.a ^ 3 + 1 = λ ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 - 1 = λ ^ 4 * y
⊢ ↑S'.u⁻¹ * (S'.a ^ 3 + 1 + (S'.b ^ 3 - 1)) = ↑S'.u⁻¹ * (S'.a ^ 3 + S'.b ^ 3)
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ b ^ (2 * p) - (1 + (b ^ 2 - 1)) = b ^ (2 * p) - (1 + (b ^ 2 - 1))

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ 2 ^ 2 ^ n + 1
this : Fact (Prime p)
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
⊢ p ∣ a.val ^ 2 ^ (n + 1) + 1

Tactic:
]

Goal state after:
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ 2 ^ 2 ^ n + 1
this : Fact (Prime p)
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
⊢ p ∣ a.val ^ 2 ^ (n + 1) + 1
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ b ^ (2 * p) - b ^ 2 = b ^ (2 * p) - b ^ 2

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
x : 𝓞 K
hx : S'.a ^ 3 + 1 = λ ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 - 1 = λ ^ 4 * y
⊢ ↑S'.u⁻¹ * (↑S'.u * S'.c ^ 3) = ↑S'.u⁻¹ * (↑S'.u * S'.c ^ 3)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ b ^ (p * 2) - b ^ 2 = b ^ (p * 2) - b ^ 2

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: n p : ℕ
hn : 1 < n
hp : Prime p
this : Fact (Prime p)
hpdvd : ↑2 ^ 2 ^ n + 1 = 0
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
⊢ ↑a.val ^ 2 ^ (n + 1) + 1 = 0

Tactic:
]

Goal state after:
n p : ℕ
hn : 1 < n
hp : Prime p
this : Fact (Prime p)
hpdvd : ↑2 ^ 2 ^ n + 1 = 0
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
⊢ ↑a.val ^ 2 ^ (n + 1) + 1 = 0
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ (b ^ p) ^ 2 - b ^ 2 = (b ^ p) ^ 2 - b ^ 2

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ (b ^ p + b) * (b ^ p - b) = (b ^ p + b) * (b ^ p - b)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: n p : ℕ
hn : 1 < n
hp : Prime p
this : Fact (Prime p)
hpdvd : ↑2 ^ 2 ^ n + 1 = 0
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
⊢ 2 ^ 2 ^ n + 1 = 0

Tactic:
]

Goal state after:
n p : ℕ
hn : 1 < n
hp : Prime p
this : Fact (Prime p)
hpdvd : ↑2 ^ 2 ^ n + 1 = 0
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
⊢ 2 ^ 2 ^ n + 1 = 0
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ (b ^ p - b) * (b ^ p + b) = (b ^ p - b) * (b ^ p + b)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: a n : ℕ
hP : Prime (a ^ n - 1)
han1 : 1 < a ^ n
hn0 : n ≠ 0
ha1 : 1 < a
ha0 : 0 < a
hn1 : a ≠ 2
h : a - 1 = a ^ n - 1
⊢ n = 1

Tactic:
]

Goal state after:
a n : ℕ
hP : Prime (a ^ n - 1)
han1 : 1 < a ^ n
hn0 : n ≠ 0
ha1 : 1 < a
ha0 : 0 < a
hn1 : a ≠ 2
h : a - 1 = a ^ n - 1
⊢ n = 1
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ (b * b ^ (p - 1) - b) * (b ^ p + b) = (b * b ^ (p - 1) - b) * (b ^ p + b)

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
hm : FiniteMultiplicity λ S'.c
this : ↑4 ≤ ↑3 * ↑(multiplicity λ S'.c)
⊢ λ ^ 2 ∣ S'.c

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
hm : FiniteMultiplicity λ S'.c
this : ↑4 ≤ ↑3 * ↑(multiplicity λ S'.c)
⊢ λ ^ 2 ∣ S'.c
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: n : ℕ
hn1 : n ≠ 1
hn0 : n ≠ 0
hP : Prime (2 ^ n - 1)
han1 : 1 < 2 ^ n
ha1 : 1 < 2
ha0 : 0 < 2
d : ℕ
hdn : d ∣ n
hinj : ∀ (x y : ℕ), 2 ^ x - 1 = 2 ^ y - 1 → x = y
h : 2 ^ d - 1 ∣ 2 ^ n - 1
⊢ d = 1 ∨ d = n

Tactic:
]

Goal state after:
n : ℕ
hn1 : n ≠ 1
hn0 : n ≠ 0
hP : Prime (2 ^ n - 1)
han1 : 1 < 2 ^ n
ha1 : 1 < 2
ha0 : 0 < 2
d : ℕ
hdn : d ∣ n
hinj : ∀ (x y : ℕ), 2 ^ x - 1 = 2 ^ y - 1 → x = y
h : 2 ^ d - 1 ∣ 2 ^ n - 1
⊢ d = 1 ∨ d = n
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ (b * b ^ (p - 1) - b * 1) * (b ^ p + b) = (b * b ^ (p - 1) - b * 1) * (b ^ p + b)

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)
x : L
hx : ∀ a_1 ∈ Ideal.map (algebraMap A B) p, ∃ x' ∈ a, (algebraMap B L) x' = x * (algebraMap B L) a_1
y : A
hy : y ∈ p
hy' : (algebraMap A K) y ∈ ↑p
z : B
hz : z ∈ a
hz' : (algebraMap B L) z = x * (algebraMap B L) ((algebraMap A B) y)
⊢ (algebraMap A K) ((intTrace A B) z) ∈ ↑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 ≠ ⊥
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)
x : L
hx : ∀ a_1 ∈ Ideal.map (algebraMap A B) p, ∃ x' ∈ a, (algebraMap B L) x' = x * (algebraMap B L) a_1
y : A
hy : y ∈ p
hy' : (algebraMap A K) y ∈ ↑p
z : B
hz : z ∈ a
hz' : (algebraMap B L) z = x * (algebraMap B L) ((algebraMap A B) y)
⊢ (algebraMap A K) ((intTrace A B) z) ∈ ↑p
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
⊢ (S'.a + S'.b) * (S'.a + ↑η * S'.b) * (S'.a + ↑η ^ 2 * S'.b) =
    S'.a ^ 3 + S'.a ^ 2 * S'.b * (↑η ^ 2 + ↑η + 1) + S'.a * S'.b ^ 2 * (↑η ^ 2 + ↑η + ↑η ^ 3) + ↑η ^ 3 * S'.b ^ 3

Tactic:
by ring

Goal state after:
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: s : Set ℕ
⊢ 1 ∉ ↑(span s) ↔ 1 ∉ s

Tactic:
]

Goal state after:
s : Set ℕ
⊢ 1 ∉ ↑(span s) ↔ 1 ∉ s
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: s : Set ℕ
⊢ s ⊆ ↑(maximalIdeal ℕ) ↔ s ⊆ ↑(maximalIdeal ℕ)

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: s : Set ℕ
⊢ 1 ∈ (Submodule.span ℕ s).toAddSubmonoid ↔ 1 ∈ s

Tactic:
]

Goal state after:
s : Set ℕ
⊢ 1 ∈ (Submodule.span ℕ s).toAddSubmonoid ↔ 1 ∈ s
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: case refine_1.inr.inr
p : ℕ
hp : Nat.Prime p
⊢ Nat.Prime p

Tactic:
]

Goal state after:
case refine_1.inr.inr
p : ℕ
hp : Nat.Prime p
⊢ Nat.Prime p
Module: Mathlib.NumberTheory.FLT.Three

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

Tactic:
]

Goal state after:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
⊢ S'.a ^ 3 + S'.a ^ 2 * S'.b * (-↑⋯.unit - 1 + ↑η + 1) + S'.a * S'.b ^ 2 * (-↑⋯.unit - 1 + ↑η + 1) + S'.b ^ 3 =
    S'.a ^ 3 + S'.b ^ 3
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: case refine_2
P : Ideal ℕ
h : P.IsPrime
h0 : ∃ x ∈ P, x ∉ ⊥
hsp : ¬∃ p, Nat.Prime p ∧ P = span {p}
n : ℕ
hn : n ∈ maximalIdeal ℕ
⊢ n ∈ P

Tactic:
]

Goal state after:
case refine_2
P : Ideal ℕ
h : P.IsPrime
h0 : ∃ x ∈ P, x ∉ ⊥
hsp : ¬∃ p, Nat.Prime p ∧ P = span {p}
n : ℕ
hn : n ∈ maximalIdeal ℕ
⊢ n ∈ 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
h1 : emultiplicity λ (S'.a + S'.b) < ↑2
h2 : emultiplicity λ (S'.a + ↑η * S'.b) < ↑2
h3 : emultiplicity λ (S'.a + ↑η ^ 2 * S'.b) < ↑2
⊢ False

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
h1 : emultiplicity λ (S'.a + S'.b) < ↑2
h2 : emultiplicity λ (S'.a + ↑η * S'.b) < ↑2
h3 : emultiplicity λ (S'.a + ↑η ^ 2 * S'.b) < ↑2
⊢ False
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
AB_id : A * B * (b ^ 2 - 1) = b ^ (2 * p) - 1
⊢ (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)

Tactic:
]

Goal state after:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
AB_id : A * B * (b ^ 2 - 1) = b ^ (2 * p) - 1
⊢ (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h1 : emultiplicity λ (S'.a + S'.b) < ↑2
h2 : emultiplicity λ (S'.a + ↑η * S'.b) < ↑2
h3 : emultiplicity λ (S'.a + ↑η ^ 2 * S'.b) < ↑2
h1' : FiniteMultiplicity λ (S'.a + S'.b)
ht : emultiplicity λ (S'.a + hζ.toInteger * S'.b) = ⊤
⊢ False

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
h1 : emultiplicity λ (S'.a + S'.b) < ↑2
h2 : emultiplicity λ (S'.a + ↑η * S'.b) < ↑2
h3 : emultiplicity λ (S'.a + ↑η ^ 2 * S'.b) < ↑2
h1' : FiniteMultiplicity λ (S'.a + S'.b)
ht : emultiplicity λ (S'.a + hζ.toInteger * S'.b) = ⊤
⊢ False