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

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

Tactic:
]

Goal state after:
case neg
a b c : ℤ
ha : a ≠ 0
Hgcd : {a, b, c}.gcd id = 1
h3a : 3 ∣ a
HF : a ^ 3 + b ^ 3 = (-c) ^ 3
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : ¬3 ∣ c
⊢ (-b) ^ 3 + (-c) ^ 3 = a ^ 3
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ringChar F = 2
⊢ 1 = 1

Tactic:
]

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

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

Tactic:
]

Goal state after:
case neg
a b c : ℤ
ha : a ≠ 0
Hgcd : {a, b, c}.gcd id = 1
h3a : 3 ∣ a
HF : a ^ 3 + b ^ 3 = (-c) ^ 3
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : ¬3 ∣ c
⊢ (-b) ^ 3 + (a ^ 3 + b ^ 3) = a ^ 3
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
⊢ (if a ^ (Fintype.card F / 2) * b ^ (Fintype.card F / 2) = 1 then 1 else -1) =
    (if a ^ (Fintype.card F / 2) = 1 then 1 else -1) * if b ^ (Fintype.card F / 2) = 1 then 1 else -1

Tactic:
]

Goal state after:
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
⊢ (if a ^ (Fintype.card F / 2) * b ^ (Fintype.card F / 2) = 1 then 1 else -1) =
    (if a ^ (Fintype.card F / 2) = 1 then 1 else -1) * if b ^ (Fintype.card F / 2) = 1 then 1 else -1
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
hp_odd : p % 2 = 1
⊢ a ^ (p - 1) = 1

Tactic:
]

Goal state after:
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
hp_odd : p % 2 = 1
⊢ a ^ (p - 1) = 1
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
ha : ↑a = 0
⊢ ↑0 = 0

Tactic:
]

Goal state after:
case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
ha : ↑a = 0
⊢ ↑0 = 0
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: case neg
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
ha : ¬↑a = 0
⊢ ↑1 = ↑a ^ (2 / 2)

Tactic:
]

Goal state after:
case neg
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
ha : ¬↑a = 0
⊢ ↑1 = ↑a ^ (2 / 2)
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: case inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
⊢ ↑(legendreSym p a) = ↑a ^ (p / 2)

Tactic:
by_cases ha : (a : ZMod p) = 0
    · rw [legendreSym, ha, quadraticChar_zero,
        zero_pow (Nat.div_pos (@Fact.out p.Prime).two_le (succ_pos 1)).ne']
      norm_cast
    · have := (ringChar_zmod_n p).symm.trans hc
      -- p = 2
      subst p
      rw [legendreSym, quadraticChar_eq_one_of_char_two hc ha]
      revert ha
      push_cast
      generalize (a : ZMod 2) = b; fin_cases b
      · tauto
      · simp

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ 0 = 0

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
⊢ (quadraticChar (ZMod p)) (↑a ^ 2) = 1

Tactic:
]

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
⊢ (quadraticChar (ZMod p)) (↑a ^ 2) = 1
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
ha0 : ↑a ≠ 0
⊢ IsSquare ↑↑a ↔ IsSquare ↑a

pp: case ha0
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
ha0 : ↑a ≠ 0
⊢ ↑↑a ≠ 0

Tactic:
]

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
ha0 : ↑a ≠ 0
⊢ IsSquare ↑↑a ↔ IsSquare ↑a

case ha0
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
ha0 : ↑a ≠ 0
⊢ ↑↑a ≠ 0
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬IsUnit a
⊢ quadraticCharFun F 0 = 0

Tactic:
]

Goal state after:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬IsUnit a
⊢ quadraticCharFun F 0 = 0
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
⊢ ¬IsSquare ↑↑a ↔ ¬IsSquare ↑a

Tactic:
]

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
⊢ ¬IsSquare ↑↑a ↔ ¬IsSquare ↑a
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a ≠ 0
⊢ 1 = 1

pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a ≠ 0
⊢ a ≠ 0

Tactic:
]

Goal state after:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a ≠ 0
⊢ a ≠ 0
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x y : ZMod p
hy : y ≠ 0
hxy : (x ^ 2 - ↑a * y ^ 2) * y⁻¹ ^ 2 = 0
⊢ (x ^ 2 - ↑a * y ^ 2) * y⁻¹ ^ 2 = (x * y⁻¹) ^ 2 - ↑a * (y * y⁻¹) ^ 2

Tactic:
by ring

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
a : F
ha : a ≠ 0
h : (quadraticChar F) a = -1
⊢ ¬-1 = 1

Tactic:
]

Goal state after:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a ≠ 0
h : (quadraticChar F) a = -1
⊢ ¬-1 = 1
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x y : ZMod p
hy : y ≠ 0
hxy : x * y⁻¹ * (x * y⁻¹) = ↑a
⊢ legendreSym p a = 1

Tactic:
]

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x y : ZMod p
hy : y ≠ 0
hxy : x * y⁻¹ * (x * y⁻¹) = ↑a
⊢ legendreSym p a = 1
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬a = 0
⊢ ¬IsSquare a ↔ ¬IsSquare a

Tactic:
]

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x : ZMod p
hx : x ≠ 0
hxy : x = 0
⊢ False

Tactic:
]

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x : ZMod p
hx : x ≠ 0
hxy : x = 0
⊢ False
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : 0 = -1
x y : ZMod p
hxy : x ^ 2 - ↑a * y ^ 2 = 0
hf : ↑a = 0
⊢ False

Tactic:
]

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : 0 = -1
x y : ZMod p
hxy : x ^ 2 - ↑a * y ^ 2 = 0
hf : ↑a = 0
⊢ False
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : ¬a = 0
⊢ ↑(if a ^ (Fintype.card F / 2) = 1 then 1 else -1) = a ^ (Fintype.card F / 2)

Tactic:
]

Goal state after:
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : ¬a = 0
⊢ ↑(if a ^ (Fintype.card F / 2) = 1 then 1 else -1) = a ^ (Fintype.card F / 2)
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
⊢ FermatLastTheoremWith ℤ 3

Tactic:
]

Goal state after:
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
⊢ FermatLastTheoremWith ℤ 3
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: case inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : 1 = 0
x y : ZMod p
hxy : x ^ 2 - ↑a * y ^ 2 = 0
ha : ↑a ≠ 0
hf : ¬(x = 0 ∧ y = 0)
hx : ¬x = 0
⊢ False

Tactic:
]

Goal state after:
case inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : 1 = 0
x y : ZMod p
hxy : x ^ 2 - ↑a * y ^ 2 = 0
ha : ↑a ≠ 0
hf : ¬(x = 0 ∧ y = 0)
hx : ¬x = 0
⊢ False
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : 1 = 0
x y : ZMod p
hxy : x ^ 2 - ↑a * y ^ 2 = 0
ha : ↑a ≠ 0
hf : ¬(x = 0 ∧ y = 0)
hy : ¬y = 0
⊢ False

Tactic:
]

Goal state after:
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : 1 = 0
x y : ZMod p
hxy : x ^ 2 - ↑a * y ^ 2 = 0
ha : ↑a ≠ 0
hf : ¬(x = 0 ∧ y = 0)
hy : ¬y = 0
⊢ False
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case neg.refine_1.mem
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
y✝ : B
x : L
hx : x ∈ FractionalIdeal.dual A K 1
y : A
hy : y ∈ ↑p
z : A
hz : (algebraMap A K) z = (Algebra.trace K L) x
⊢ (algebraMap A K) y * (algebraMap A K) z = (algebraMap A K) y * (algebraMap A K) z

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a = 0
⊢ (quadraticChar F) 0 = 0

Tactic:
]

Goal state after:
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a = 0
⊢ (quadraticChar F) 0 = 0
Module: Mathlib.NumberTheory.FLT.Three

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

Tactic:
]

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℤ
⊢ χ₄ ↑p * legendreSym p a = χ₄ ↑p * legendreSym p a

Tactic:
]

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ p % 4 ≠ 3 ↔ p % 4 ≠ 3

Tactic:
]

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x y : ZMod p
hy : y ≠ 0
hxy : (x / y) ^ 2 = -1
⊢ (x / y) ^ 2 = -1

Tactic:
]

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
x y : ZMod p
hy : y ≠ 0
hxy : (x / y) ^ 2 = -1
⊢ (x / y) ^ 2 = -1
Module: Mathlib.NumberTheory.FLT.Three

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

Tactic:
]

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

Goal state before:
pp: case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := {x | x ^ 2 = a}.toFinset
h : IsSquare a
⊢ ↑(#s) = 1 + 1

Tactic:
]

Goal state after:
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := {x | x ^ 2 = a}.toFinset
h : IsSquare a
⊢ ↑(#s) = 1 + 1
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: case pos
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) = 1 + 1

Tactic:
]

Goal state after:
case pos
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) = 1 + 1
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum

Goal state before:
pp: case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 2 = 1
⊢ (if Fintype.card F % 2 = 0 then 0 else if Fintype.card F % 8 = 1 ∨ Fintype.card F % 8 = 7 then 1 else -1) = 1 ↔
    Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5

Tactic:
]

Goal state after:
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 2 = 1
⊢ (if Fintype.card F % 2 = 0 then 0 else if Fintype.card F % 8 = 1 ∨ Fintype.card F % 8 = 7 then 1 else -1) = 1 ↔
    Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
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 ^ 2
a✝ : F
⊢ a✝ ∈ s ↔ a✝ ∈ [b, -b].toFinset

Tactic:
]

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 ^ 2
a✝ : F
⊢ a✝ ∈ s ↔ a✝ ∈ [b, -b].toFinset
Module: Mathlib.NumberTheory.FLT.Three

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

Tactic:
]

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
⊢ χ₄ ↑(Fintype.card F) * χ₈ ↑(Fintype.card F) = χ₄ ↑(Fintype.card F) * χ₈ ↑(Fintype.card F)

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 2 = 1
⊢ (if Fintype.card F % 2 = 0 then 0 else if Fintype.card F % 8 = 1 ∨ Fintype.card F % 8 = 3 then 1 else -1) = 1 ↔
    Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7

Tactic:
]

Goal state after:
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 2 = 1
⊢ (if Fintype.card F % 2 = 0 then 0 else if Fintype.card F % 8 = 1 ∨ Fintype.card F % 8 = 3 then 1 else -1) = 1 ↔
    Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum

Goal state before:
pp: F : Type u_1
inst✝⁵ : Field F
inst✝⁴ : Fintype F
inst✝³ : DecidableEq F
hF : ringChar F ≠ 2
F' : Type u_2
inst✝² : Field F'
inst✝¹ : Fintype F'
inst✝ : DecidableEq F'
hF' : ringChar F' ≠ 2
h✝ : ringChar F' ≠ ringChar F
χ : MulChar F F' := (quadraticChar F).ringHomComp (algebraMap ℤ F')
hχ₁ : χ ≠ 1
h : ↑((quadraticChar F') (χ (-1) * ↑(Fintype.card F))) = χ ↑(Fintype.card F')
⊢ (quadraticChar F) ↑(Fintype.card F') = (quadraticChar F') (↑((quadraticChar F) (-1)) * ↑(Fintype.card F))

Tactic:
]

Goal state after:
F : Type u_1
inst✝⁵ : Field F
inst✝⁴ : Fintype F
inst✝³ : DecidableEq F
hF : ringChar F ≠ 2
F' : Type u_2
inst✝² : Field F'
inst✝¹ : Fintype F'
inst✝ : DecidableEq F'
hF' : ringChar F' ≠ 2
h✝ : ringChar F' ≠ ringChar F
χ : MulChar F F' := (quadraticChar F).ringHomComp (algebraMap ℤ F')
hχ₁ : χ ≠ 1
h : ↑((quadraticChar F') (χ (-1) * ↑(Fintype.card F))) = χ ↑(Fintype.card F')
⊢ (quadraticChar F) ↑(Fintype.card F') = (quadraticChar F') (↑((quadraticChar F) (-1)) * ↑(Fintype.card F))
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: case pos
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
h₁ : s = [b, -b].toFinset
⊢ #(insert b (insert (-b) ∅)) = 1 + 1

Tactic:
]

Goal state after:
case pos
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
h₁ : s = [b, -b].toFinset
⊢ #(insert b (insert (-b) ∅)) = 1 + 1
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := {x | x ^ 2 = a}.toFinset
h : ¬IsSquare a
⊢ ↑(#s) = -1 + 1

Tactic:
]

Goal state after:
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := {x | x ^ 2 = a}.toFinset
h : ¬IsSquare a
⊢ ↑(#s) = -1 + 1
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp₁ : p ≠ 2
hp₂ : ringChar F ≠ p
⊢ (quadraticChar F) ↑p = (quadraticChar (ZMod p)) (↑((quadraticChar F) (-1)) * ↑(Fintype.card F))

Tactic:
]

Goal state after:
F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp₁ : p ≠ 2
hp₂ : ringChar F ≠ p
⊢ (quadraticChar F) ↑p = (quadraticChar (ZMod p)) (↑((quadraticChar F) (-1)) * ↑(Fintype.card F))
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
h : (quadraticChar F) (-1) = if (-1) ^ (Fintype.card F / 2) = 1 then 1 else -1
⊢ (if (-1) ^ (Fintype.card F / 2) = 1 then 1 else -1) = (-1) ^ (Fintype.card F / 2)

Tactic:
]

Goal state after:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
h : (quadraticChar F) (-1) = if (-1) ^ (Fintype.card F / 2) = 1 then 1 else -1
⊢ (if (-1) ^ (Fintype.card F / 2) = 1 then 1 else -1) = (-1) ^ (Fintype.card F / 2)
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp₁ : p ≠ 2
hp₂ : ringChar F ≠ p
h : (quadraticChar F) ↑p = (quadraticChar (ZMod p)) (↑((quadraticChar F) (-1)) * ↑(Fintype.card F))
⊢ (quadraticChar F) ↑p = (quadraticChar (ZMod p)) (↑((quadraticChar F) (-1)) * ↑(Fintype.card F))

Tactic:
]

Goal state after:
F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp₁ : p ≠ 2
hp₂ : ringChar F ≠ p
h : (quadraticChar F) ↑p = (quadraticChar (ZMod p)) (↑((quadraticChar F) (-1)) * ↑(Fintype.card F))
⊢ (quadraticChar F) ↑p = (quadraticChar (ZMod p)) (↑((quadraticChar F) (-1)) * ↑(Fintype.card F))
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case refine_1
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 ∣ a
⊢ 3 ∣ a

Tactic:
]

Goal state after:
case refine_1
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 ∣ a
⊢ 3 ∣ a
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h₁ : Fintype.card F % 2 = 1
⊢ (if 1 = 0 then 0 else if Fintype.card F % 4 = 1 then 1 else -1) = 1 ↔ Fintype.card F % 4 ≠ 3

Tactic:
]

Goal state after:
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h₁ : Fintype.card F % 2 = 1
⊢ (if 1 = 0 then 0 else if Fintype.card F % 4 = 1 then 1 else -1) = 1 ↔ Fintype.card F % 4 ≠ 3
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum

Goal state before:
pp: case inr
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F ≠ p
⊢ ¬(quadraticChar (ZMod p)) (↑(χ₄ ↑(Fintype.card F)) * ↑(Fintype.card F)) = -1 ↔
    (quadraticChar (ZMod p)) (↑(χ₄ ↑(Fintype.card F)) * ↑(Fintype.card F)) ≠ -1

pp: case inr
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F ≠ p
⊢ ringChar F ≠ p

Tactic:
]

Goal state after:
case inr
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F ≠ p
⊢ ringChar F ≠ p