Theorem: FltRegular.CaseI.may_assume (FltRegular/CaseI/Statement.lean)

State before:
p : ℕ
hpri : Fact p.Prime
⊢ SlightlyEasier → Statement
Tactic:
intro Heasy
State after:
p : ℕ
hpri : Fact p.Prime
Heasy : SlightlyEasier
⊢ Statement

State before:
p : ℕ
hpri : Fact p.Prime
Heasy : SlightlyEasier
⊢ Statement
Tactic:
intro a b c p hpri hreg hI H
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
⊢ False

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
⊢ False
Tactic:
have hodd : p ≠ 2 := by
  intro h
  rw [h] at H hI
  refine' hI _
  refine' Dvd.dvd.mul_left _ _
  simp only [Nat.cast_ofNat] at hI ⊢
  rw [← even_iff_two_dvd, ← Int.odd_iff_not_even] at hI
  rw [← even_iff_two_dvd, ← Int.even_pow' (show 2 ≠ 0 by norm_num), ← H]
  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
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
⊢ False

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
⊢ False
Tactic:
have hprod : a * b * c ≠ 0 := by
  intro h
  simp [h] at hI
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
⊢ False

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
⊢ False
Tactic:
rcases MayAssume.coprime H hprod with ⟨Hxyz, hunit, hprodxyx⟩
State after:
case 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
⊢ False

State before:
case 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
⊢ False
Tactic:
let d := ({a, b, c} : Finset ℤ).gcd id
State after:
case 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
⊢ False

State before:
case 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
⊢ False
Tactic:
have hdiv : ¬↑p ∣ a / d * (b / d) * (c / d) :=
  by
  have hadiv : d ∣ a := gcd_dvd (by simp)
  have hbdiv : d ∣ b := gcd_dvd (by simp)
  have hcdiv : d ∣ c := gcd_dvd (by simp)
  intro hdiv
  replace hdiv := dvd_mul_of_dvd_right hdiv (d * d * d)
  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
  exact hI hdiv
State after:
case 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)
⊢ False

State before:
case 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)
⊢ False
Tactic:
obtain ⟨X, Y, Z, H1, H2, H3, _, H5⟩ := a_not_cong_b hpri.out hp5 hprodxyx Hxyz hunit hdiv
State after:
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

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
State after:
no goals

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
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

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
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

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 _
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

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 _ _
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

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 ⊢
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

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
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

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]
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)

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
State after:
no goals

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
State after:
no goals

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
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

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
State after:
no goals

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
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

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⟩
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

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
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

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
State after:
no goals

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
State after:
no goals

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
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

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
State after:
no goals

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)
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)

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)
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)

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)
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)

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
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

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)
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

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
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

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals