internlm/Lean-Github huggingface dataset:
Theorem: FltRegular.CaseI.may_assume
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
hp5 : 5 ≤ p
Hxyz : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hunit : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprodxyx : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
hdiv : ¬↑p ∣ a / d * (b / d) * (c / d)
X Y Z : ℤ
H1 : X ^ p + Y ^ p = Z ^ p
H2 : {X, Y, Z}.gcd id = 1
H3 : ¬X ≡ Y [ZMOD ↑p]
left✝ : X * Y * Z ≠ 0
H5 : ¬↑p ∣ X * Y * Z
⊢ False
Tactic:
exact Heasy hreg hp5 H2 H3 (fun hfin => H5 hfin) H1
Proof state after:
no goals
Theorem: FltRegular.CaseI.may_assume
Proof state before:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
⊢ p ≠ 2
Tactic:
intro h
Proof state after:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
h : p = 2
⊢ False
Theorem: FltRegular.CaseI.may_assume
Proof state before:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
h : p = 2
⊢ False
Tactic:
rw [h] at H hI
Proof state after:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑2 ∣ a * b * c
H : a ^ 2 + b ^ 2 = c ^ 2
h : p = 2
⊢ False
Theorem: FltRegular.CaseI.may_assume
Proof state before:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑2 ∣ a * b * c
H : a ^ 2 + b ^ 2 = c ^ 2
h : p = 2
⊢ False
Tactic:
refine' hI _
Proof state after:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑2 ∣ a * b * c
H : a ^ 2 + b ^ 2 = c ^ 2
h : p = 2
⊢ ↑2 ∣ a * b * c
Theorem: FltRegular.CaseI.may_assume
Proof state before:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑2 ∣ a * b * c
H : a ^ 2 + b ^ 2 = c ^ 2
h : p = 2
⊢ ↑2 ∣ a * b * c
Tactic:
refine' Dvd.dvd.mul_left _ _
Proof state after:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑2 ∣ a * b * c
H : a ^ 2 + b ^ 2 = c ^ 2
h : p = 2
⊢ ↑2 ∣ c
Theorem: FltRegular.CaseI.may_assume
Proof state before:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑2 ∣ a * b * c
H : a ^ 2 + b ^ 2 = c ^ 2
h : p = 2
⊢ ↑2 ∣ c
Tactic:
simp only [Nat.cast_ofNat] at hI ⊢
Proof state after:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬2 ∣ a * b * c
H : a ^ 2 + b ^ 2 = c ^ 2
h : p = 2
⊢ 2 ∣ c
Theorem: FltRegular.CaseI.may_assume
Proof state before:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬2 ∣ a * b * c
H : a ^ 2 + b ^ 2 = c ^ 2
h : p = 2
⊢ 2 ∣ c
Tactic:
rw [← even_iff_two_dvd, ← Int.odd_iff_not_even] at hI
Proof state after:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : Odd (a * b * c)
H : a ^ 2 + b ^ 2 = c ^ 2
h : p = 2
⊢ 2 ∣ c
Theorem: FltRegular.CaseI.may_assume
Proof state before:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : Odd (a * b * c)
H : a ^ 2 + b ^ 2 = c ^ 2
h : p = 2
⊢ 2 ∣ c
Tactic:
rw [← even_iff_two_dvd, ← Int.even_pow' (show 2 ≠ 0 by norm_num), ← H]
Proof state after:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : Odd (a * b * c)
H : a ^ 2 + b ^ 2 = c ^ 2
h : p = 2
⊢ Even (a ^ 2 + b ^ 2)
Theorem: FltRegular.CaseI.may_assume
Proof state before:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : Odd (a * b * c)
H : a ^ 2 + b ^ 2 = c ^ 2
h : p = 2
⊢ Even (a ^ 2 + b ^ 2)
Tactic:
exact (Int.Odd.of_mul_left (Odd.of_mul_left hI)).pow.add_odd
  (Int.Odd.of_mul_right (Odd.of_mul_left hI)).pow
Proof state after:
no goals
Theorem: FltRegular.CaseI.may_assume
Proof state before:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : Odd (a * b * c)
H : a ^ 2 + b ^ 2 = c ^ 2
h : p = 2
⊢ 2 ≠ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: FltRegular.CaseI.may_assume
Proof state before:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
⊢ a * b * c ≠ 0
Tactic:
intro h
Proof state after:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
h : a * b * c = 0
⊢ False
Theorem: FltRegular.CaseI.may_assume
Proof state before:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
h : a * b * c = 0
⊢ False
Tactic:
simp [h] at hI
Proof state after:
no goals
Theorem: FltRegular.CaseI.may_assume
Proof state before:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
⊢ 5 ≤ p
Tactic:
by_contra! habs
Proof state after:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
habs : p < 5
⊢ False
Theorem: FltRegular.CaseI.may_assume
Proof state before:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
habs : p < 5
⊢ False
Tactic:
have : p ∈ Finset.Ioo 2 5 :=
  (Finset.mem_Ioo).2 ⟨Nat.lt_of_le_of_ne hpri.out.two_le hodd.symm, by linarith⟩
Proof state after:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
habs : p < 5
this : p ∈ Ioo 2 5
⊢ False
Theorem: FltRegular.CaseI.may_assume
Proof state before:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
habs : p < 5
this : p ∈ Ioo 2 5
⊢ False
Tactic:
fin_cases this
Proof state after:
case head
p : ℕ
hpri✝ : Fact p.Prime
Heasy : SlightlyEasier
a b c : ℤ
hprod : a * b * c ≠ 0
hpri : Fact (2 + 1).Prime
hreg : IsRegularPrime (2 + 1)
hI : ¬↑(2 + 1) ∣ a * b * c
H : a ^ (2 + 1) + b ^ (2 + 1) = c ^ (2 + 1)
hodd : 2 + 1 ≠ 2
habs : 2 + 1 < 5
⊢ False

case tail.head
p : ℕ
hpri✝ : Fact p.Prime
Heasy : SlightlyEasier
a b c : ℤ
hprod : a * b * c ≠ 0
hpri : Fact (2 + 1 + 1).Prime
hreg : IsRegularPrime (2 + 1 + 1)
hI : ¬↑(2 + 1 + 1) ∣ a * b * c
H : a ^ (2 + 1 + 1) + b ^ (2 + 1 + 1) = c ^ (2 + 1 + 1)
hodd : 2 + 1 + 1 ≠ 2
habs : 2 + 1 + 1 < 5
⊢ False
Theorem: FltRegular.CaseI.may_assume
Proof state before:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
habs : p < 5
⊢ p < 5
Tactic:
linarith
Proof state after:
no goals
Theorem: FltRegular.CaseI.may_assume
Proof state before:
case head
p : ℕ
hpri✝ : Fact p.Prime
Heasy : SlightlyEasier
a b c : ℤ
hprod : a * b * c ≠ 0
hpri : Fact (2 + 1).Prime
hreg : IsRegularPrime (2 + 1)
hI : ¬↑(2 + 1) ∣ a * b * c
H : a ^ (2 + 1) + b ^ (2 + 1) = c ^ (2 + 1)
hodd : 2 + 1 ≠ 2
habs : 2 + 1 < 5
⊢ False
Tactic:
exact MayAssume.p_ne_three hprod H rfl
Proof state after:
no goals
Theorem: FltRegular.CaseI.may_assume
Proof state before:
case tail.head
p : ℕ
hpri✝ : Fact p.Prime
Heasy : SlightlyEasier
a b c : ℤ
hprod : a * b * c ≠ 0
hpri : Fact (2 + 1 + 1).Prime
hreg : IsRegularPrime (2 + 1 + 1)
hI : ¬↑(2 + 1 + 1) ∣ a * b * c
H : a ^ (2 + 1 + 1) + b ^ (2 + 1 + 1) = c ^ (2 + 1 + 1)
hodd : 2 + 1 + 1 ≠ 2
habs : 2 + 1 + 1 < 5
⊢ False
Tactic:
rw [show 2 + 1 + 1 = 2 * 2 from rfl] at hpri
Proof state after:
case tail.head
p : ℕ
hpri✝¹ : Fact p.Prime
Heasy : SlightlyEasier
a b c : ℤ
hprod : a * b * c ≠ 0
hpri✝ : Fact (2 + 1 + 1).Prime
hpri : Fact (2 * 2).Prime
hreg : IsRegularPrime (2 + 1 + 1)
hI : ¬↑(2 + 1 + 1) ∣ a * b * c
H : a ^ (2 + 1 + 1) + b ^ (2 + 1 + 1) = c ^ (2 + 1 + 1)
hodd : 2 + 1 + 1 ≠ 2
habs : 2 + 1 + 1 < 5
⊢ False
Theorem: FltRegular.CaseI.may_assume
Proof state before:
case tail.head
p : ℕ
hpri✝¹ : Fact p.Prime
Heasy : SlightlyEasier
a b c : ℤ
hprod : a * b * c ≠ 0
hpri✝ : Fact (2 + 1 + 1).Prime
hpri : Fact (2 * 2).Prime
hreg : IsRegularPrime (2 + 1 + 1)
hI : ¬↑(2 + 1 + 1) ∣ a * b * c
H : a ^ (2 + 1 + 1) + b ^ (2 + 1 + 1) = c ^ (2 + 1 + 1)
hodd : 2 + 1 + 1 ≠ 2
habs : 2 + 1 + 1 < 5
⊢ False
Tactic:
refine' Nat.not_prime_mul one_lt_two.ne' one_lt_two.ne' hpri.out
Proof state after:
no goals
Theorem: FltRegular.CaseI.may_assume
Proof state before:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
hp5 : 5 ≤ p
Hxyz : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hunit : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprodxyx : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
⊢ ¬↑p ∣ a / d * (b / d) * (c / d)
Tactic:
have hadiv : d ∣ a := gcd_dvd (by simp)
Proof state after:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
hp5 : 5 ≤ p
Hxyz : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hunit : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprodxyx : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
hadiv : d ∣ a
⊢ ¬↑p ∣ a / d * (b / d) * (c / d)
Theorem: FltRegular.CaseI.may_assume
Proof state before:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
hp5 : 5 ≤ p
Hxyz : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hunit : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprodxyx : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
hadiv : d ∣ a
⊢ ¬↑p ∣ a / d * (b / d) * (c / d)
Tactic:
have hbdiv : d ∣ b := gcd_dvd (by simp)
Proof state after:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
hp5 : 5 ≤ p
Hxyz : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hunit : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprodxyx : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
⊢ ¬↑p ∣ a / d * (b / d) * (c / d)
Theorem: FltRegular.CaseI.may_assume
Proof state before:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
hp5 : 5 ≤ p
Hxyz : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hunit : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprodxyx : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
⊢ ¬↑p ∣ a / d * (b / d) * (c / d)
Tactic:
have hcdiv : d ∣ c := gcd_dvd (by simp)
Proof state after:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
hp5 : 5 ≤ p
Hxyz : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hunit : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprodxyx : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
⊢ ¬↑p ∣ a / d * (b / d) * (c / d)
Theorem: FltRegular.CaseI.may_assume
Proof state before:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
hp5 : 5 ≤ p
Hxyz : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hunit : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprodxyx : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
⊢ ¬↑p ∣ a / d * (b / d) * (c / d)
Tactic:
intro hdiv
Proof state after:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
hp5 : 5 ≤ p
Hxyz : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hunit : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprodxyx : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdiv : ↑p ∣ a / d * (b / d) * (c / d)
⊢ False
Theorem: FltRegular.CaseI.may_assume
Proof state before:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
hp5 : 5 ≤ p
Hxyz : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hunit : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprodxyx : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdiv : ↑p ∣ a / d * (b / d) * (c / d)
⊢ False
Tactic:
replace hdiv := dvd_mul_of_dvd_right hdiv (d * d * d)
Proof state after:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
hp5 : 5 ≤ p
Hxyz : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hunit : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprodxyx : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdiv : ↑p ∣ d * d * d * (a / d * (b / d) * (c / d))
⊢ False
Theorem: FltRegular.CaseI.may_assume
Proof state before:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
hp5 : 5 ≤ p
Hxyz : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hunit : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprodxyx : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdiv : ↑p ∣ d * d * d * (a / d * (b / d) * (c / d))
⊢ False
Tactic:
rw [mul_assoc, ← mul_assoc d, ← mul_assoc d, Int.mul_ediv_cancel' hadiv, mul_assoc, mul_comm a,
  mul_assoc (b / d), ← mul_assoc _ (b / d), Int.mul_ediv_cancel' hbdiv, mul_comm, mul_assoc,
  mul_assoc, Int.ediv_mul_cancel hcdiv, mul_comm, mul_assoc, mul_comm c, ← mul_assoc] at hdiv
Proof state after:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
hp5 : 5 ≤ p
Hxyz : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hunit : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprodxyx : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdiv : ↑p ∣ a * b * c
⊢ False
Theorem: FltRegular.CaseI.may_assume
Proof state before:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
hp5 : 5 ≤ p
Hxyz : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hunit : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprodxyx : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdiv : ↑p ∣ a * b * c
⊢ False
Tactic:
exact hI hdiv
Proof state after:
no goals
Theorem: FltRegular.CaseI.may_assume
Proof state before:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
hp5 : 5 ≤ p
Hxyz : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hunit : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprodxyx : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
⊢ a ∈ {a, b, c}
Tactic:
simp
Proof state after:
no goals
Theorem: FltRegular.CaseI.may_assume
Proof state before:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
hp5 : 5 ≤ p
Hxyz : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hunit : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprodxyx : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
hadiv : d ∣ a
⊢ b ∈ {a, b, c}
Tactic:
simp
Proof state after:
no goals
Theorem: FltRegular.CaseI.may_assume
Proof state before:
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
hp5 : 5 ≤ p
Hxyz : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hunit : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprodxyx : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
⊢ c ∈ {a, b, c}
Tactic:
simp
Proof state after:
no goals
Theorem: FltRegular.ab_coprime
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
⊢ IsCoprime a b
Tactic:
rw [← gcd_eq_one_iff_coprime]
Proof state after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
⊢ a.gcd b = 1
Theorem: FltRegular.ab_coprime
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
⊢ a.gcd b = 1
Tactic:
by_contra! h
Proof state after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
⊢ False
Theorem: FltRegular.ab_coprime
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
⊢ False
Tactic:
obtain ⟨q, hqpri, hq⟩ := exists_prime_and_dvd h
Proof state after:
case intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : q.Prime
hq : q ∣ a.gcd b
⊢ False
Theorem: FltRegular.ab_coprime
Proof state before:
case intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : q.Prime
hq : q ∣ a.gcd b
⊢ False
Tactic:
replace hqpri : Prime (q : ℤ) := prime_iff_natAbs_prime.2 (by simp [hqpri])
Proof state after:
case intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hq : q ∣ a.gcd b
hqpri : _root_.Prime ↑q
⊢ False
Theorem: FltRegular.ab_coprime
Proof state before:
case intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hq : q ∣ a.gcd b
hqpri : _root_.Prime ↑q
⊢ False
Tactic:
obtain ⟨n, hn⟩ := hq
Proof state after:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
⊢ False
Theorem: FltRegular.ab_coprime
Proof state before:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
⊢ False
Tactic:
have haq : ↑q ∣ a := by
  obtain ⟨m, hm⟩ := @Int.gcd_dvd_left a b
  exact ⟨n * m, by rw [hm, hn]; simp [mul_assoc]⟩
Proof state after:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
⊢ False
Theorem: FltRegular.ab_coprime
Proof state before:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
⊢ False
Tactic:
have hbq : ↑q ∣ b := by
  obtain ⟨m, hm⟩ := @Int.gcd_dvd_right a b
  exact ⟨n * m, by rw [hm, hn]; simp [mul_assoc]⟩
Proof state after:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
⊢ False
Theorem: FltRegular.ab_coprime
Proof state before:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
⊢ False
Tactic:
have hcq : ↑q ∣ c := by
  suffices ↑q ∣ c ^ p by exact hqpri.dvd_of_dvd_pow this
  rw [← H]
  exact dvd_add (dvd_pow haq hpzero) (dvd_pow hbq hpzero)
Proof state after:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
hcq : ↑q ∣ c
⊢ False