internlm/Lean-Github huggingface dataset:
Theorem: descent1left
Proof state before:
a : ℤ
hapos : a ≠ 0
p : ℤ
hpnezero : p ≠ 0
hc : ¬Even (p + 0)
hb : ¬Even (0 - p)
h : a ^ 3 + (-p) ^ 3 = p ^ 3
hbccoprime : IsCoprime (0 - p) (p + 0)
hp : p + 0 - (0 - p) = 2 * p
hq : p + 0 + (0 - p) = 2 * 0
⊢ ¬Even 3
Tactic:
decide
Proof state after:
no goals
Theorem: descent1left
Proof state before:
case intro.intro.refine'_1
a : ℤ
hapos : a ≠ 0
p q : ℤ
hc : ¬Even (p + q)
hb : ¬Even (q - p)
h : a ^ 3 + (q - p) ^ 3 = (p + q) ^ 3
hbccoprime : IsCoprime (q - p) (p + q)
hp : p + q - (q - p) = 2 * p
hq : p + q + (q - p) = 2 * q
hpnezero : p ≠ 0
hqnezero : q ≠ 0
⊢ IsCoprime p q
Tactic:
apply isCoprime_of_dvd _ _ (not_and_of_not_left _ hpnezero)
Proof state after:
case intro.intro.refine'_1
a : ℤ
hapos : a ≠ 0
p q : ℤ
hc : ¬Even (p + q)
hb : ¬Even (q - p)
h : a ^ 3 + (q - p) ^ 3 = (p + q) ^ 3
hbccoprime : IsCoprime (q - p) (p + q)
hp : p + q - (q - p) = 2 * p
hq : p + q + (q - p) = 2 * q
hpnezero : p ≠ 0
hqnezero : q ≠ 0
⊢ ∀ z ∈ nonunits ℤ, z ≠ 0 → z ∣ p → ¬z ∣ q
Theorem: descent1left
Proof state before:
case intro.intro.refine'_1
a : ℤ
hapos : a ≠ 0
p q : ℤ
hc : ¬Even (p + q)
hb : ¬Even (q - p)
h : a ^ 3 + (q - p) ^ 3 = (p + q) ^ 3
hbccoprime : IsCoprime (q - p) (p + q)
hp : p + q - (q - p) = 2 * p
hq : p + q + (q - p) = 2 * q
hpnezero : p ≠ 0
hqnezero : q ≠ 0
⊢ ∀ z ∈ nonunits ℤ, z ≠ 0 → z ∣ p → ¬z ∣ q
Tactic:
rintro z hznu - hzp hzq
Proof state after:
case intro.intro.refine'_1
a : ℤ
hapos : a ≠ 0
p q : ℤ
hc : ¬Even (p + q)
hb : ¬Even (q - p)
h : a ^ 3 + (q - p) ^ 3 = (p + q) ^ 3
hbccoprime : IsCoprime (q - p) (p + q)
hp : p + q - (q - p) = 2 * p
hq : p + q + (q - p) = 2 * q
hpnezero : p ≠ 0
hqnezero : q ≠ 0
z : ℤ
hznu : z ∈ nonunits ℤ
hzp : z ∣ p
hzq : z ∣ q
⊢ False
Theorem: descent1left
Proof state before:
case intro.intro.refine'_1
a : ℤ
hapos : a ≠ 0
p q : ℤ
hc : ¬Even (p + q)
hb : ¬Even (q - p)
h : a ^ 3 + (q - p) ^ 3 = (p + q) ^ 3
hbccoprime : IsCoprime (q - p) (p + q)
hp : p + q - (q - p) = 2 * p
hq : p + q + (q - p) = 2 * q
hpnezero : p ≠ 0
hqnezero : q ≠ 0
z : ℤ
hznu : z ∈ nonunits ℤ
hzp : z ∣ p
hzq : z ∣ q
⊢ False
Tactic:
apply hznu
Proof state after:
case intro.intro.refine'_1
a : ℤ
hapos : a ≠ 0
p q : ℤ
hc : ¬Even (p + q)
hb : ¬Even (q - p)
h : a ^ 3 + (q - p) ^ 3 = (p + q) ^ 3
hbccoprime : IsCoprime (q - p) (p + q)
hp : p + q - (q - p) = 2 * p
hq : p + q + (q - p) = 2 * q
hpnezero : p ≠ 0
hqnezero : q ≠ 0
z : ℤ
hznu : z ∈ nonunits ℤ
hzp : z ∣ p
hzq : z ∣ q
⊢ IsUnit z
Theorem: descent1left
Proof state before:
case intro.intro.refine'_1
a : ℤ
hapos : a ≠ 0
p q : ℤ
hc : ¬Even (p + q)
hb : ¬Even (q - p)
h : a ^ 3 + (q - p) ^ 3 = (p + q) ^ 3
hbccoprime : IsCoprime (q - p) (p + q)
hp : p + q - (q - p) = 2 * p
hq : p + q + (q - p) = 2 * q
hpnezero : p ≠ 0
hqnezero : q ≠ 0
z : ℤ
hznu : z ∈ nonunits ℤ
hzp : z ∣ p
hzq : z ∣ q
⊢ IsUnit z
Tactic:
exact hbccoprime.isUnit_of_dvd' (dvd_sub hzq hzp) (dvd_add hzp hzq)
Proof state after:
no goals
Theorem: descent1left
Proof state before:
case intro.intro.refine'_2
a : ℤ
hapos : a ≠ 0
p q : ℤ
hc : ¬Even (p + q)
hb : ¬Even (q - p)
h : a ^ 3 + (q - p) ^ 3 = (p + q) ^ 3
hbccoprime : IsCoprime (q - p) (p + q)
hp : p + q - (q - p) = 2 * p
hq : p + q + (q - p) = 2 * q
hpnezero : p ≠ 0
hqnezero : q ≠ 0
⊢ Even p ↔ ¬Even q
Tactic:
constructor <;> intro H <;> simpa [H, parity_simps] using hc
Proof state after:
no goals
Theorem: descent1left
Proof state before:
case intro.intro.refine'_3
a : ℤ
hapos : a ≠ 0
p q : ℤ
hc : ¬Even (p + q)
hb : ¬Even (q - p)
h : a ^ 3 + (q - p) ^ 3 = (p + q) ^ 3
hbccoprime : IsCoprime (q - p) (p + q)
hp : p + q - (q - p) = 2 * p
hq : p + q + (q - p) = 2 * q
hpnezero : p ≠ 0
hqnezero : q ≠ 0
⊢ 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3
Tactic:
rw [eq_sub_of_add_eq h]
Proof state after:
case intro.intro.refine'_3
a : ℤ
hapos : a ≠ 0
p q : ℤ
hc : ¬Even (p + q)
hb : ¬Even (q - p)
h : a ^ 3 + (q - p) ^ 3 = (p + q) ^ 3
hbccoprime : IsCoprime (q - p) (p + q)
hp : p + q - (q - p) = 2 * p
hq : p + q + (q - p) = 2 * q
hpnezero : p ≠ 0
hqnezero : q ≠ 0
⊢ 2 * p * (p ^ 2 + 3 * q ^ 2) = (p + q) ^ 3 - (q - p) ^ 3
Theorem: descent1left
Proof state before:
case intro.intro.refine'_3
a : ℤ
hapos : a ≠ 0
p q : ℤ
hc : ¬Even (p + q)
hb : ¬Even (q - p)
h : a ^ 3 + (q - p) ^ 3 = (p + q) ^ 3
hbccoprime : IsCoprime (q - p) (p + q)
hp : p + q - (q - p) = 2 * p
hq : p + q + (q - p) = 2 * q
hpnezero : p ≠ 0
hqnezero : q ≠ 0
⊢ 2 * p * (p ^ 2 + 3 * q ^ 2) = (p + q) ^ 3 - (q - p) ^ 3
Tactic:
ring
Proof state after:
no goals
Theorem: descent1
Proof state before:
a b c : ℤ
h : FltCoprime 3 a b c
⊢ ∃ p q,
    p ≠ 0 ∧
      q ≠ 0 ∧
        IsCoprime p q ∧
          (Even p ↔ ¬Even q) ∧
            (2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
              2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3)
Tactic:
obtain ⟨⟨hapos, hbpos, hcpos, h⟩, habcoprime, haccoprime, hbccoprime⟩ := h
Proof state after:
case intro.intro.intro.intro.intro.intro
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
⊢ ∃ p q,
    p ≠ 0 ∧
      q ≠ 0 ∧
        IsCoprime p q ∧
          (Even p ↔ ¬Even q) ∧
            (2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
              2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3)
Theorem: descent1
Proof state before:
case intro.intro.intro.intro.intro.intro
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
⊢ ∃ p q,
    p ≠ 0 ∧
      q ≠ 0 ∧
        IsCoprime p q ∧
          (Even p ↔ ¬Even q) ∧
            (2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
              2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3)
Tactic:
obtain (⟨-, hb, hc⟩ | ⟨ha, hb, hc⟩) | ⟨ha, hb, -⟩ :=
  descent1a h habcoprime haccoprime hbccoprime
Proof state after:
case intro.intro.intro.intro.intro.intro.inl.inl.intro.intro
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
hb : ¬Even b
hc : ¬Even c
⊢ ∃ p q,
    p ≠ 0 ∧
      q ≠ 0 ∧
        IsCoprime p q ∧
          (Even p ↔ ¬Even q) ∧
            (2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
              2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3)

case intro.intro.intro.intro.intro.intro.inl.inr.intro.intro
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
ha : ¬Even a
hb : Even b
hc : ¬Even c
⊢ ∃ p q,
    p ≠ 0 ∧
      q ≠ 0 ∧
        IsCoprime p q ∧
          (Even p ↔ ¬Even q) ∧
            (2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
              2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3)

case intro.intro.intro.intro.intro.intro.inr.intro.intro
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
ha : ¬Even a
hb : ¬Even b
⊢ ∃ p q,
    p ≠ 0 ∧
      q ≠ 0 ∧
        IsCoprime p q ∧
          (Even p ↔ ¬Even q) ∧
            (2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
              2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3)
Theorem: descent1
Proof state before:
case intro.intro.intro.intro.intro.intro.inl.inl.intro.intro
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
hb : ¬Even b
hc : ¬Even c
⊢ ∃ p q,
    p ≠ 0 ∧
      q ≠ 0 ∧
        IsCoprime p q ∧
          (Even p ↔ ¬Even q) ∧
            (2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
              2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3)
Tactic:
obtain ⟨p, q, hp, hq, hcoprime, hodd, hcube⟩ := descent1left hapos h hbccoprime hb hc
Proof state after:
case intro.intro.intro.intro.intro.intro.inl.inl.intro.intro.intro.intro.intro.intro.intro.intro
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
hb : ¬Even b
hc : ¬Even c
p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3
⊢ ∃ p q,
    p ≠ 0 ∧
      q ≠ 0 ∧
        IsCoprime p q ∧
          (Even p ↔ ¬Even q) ∧
            (2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
              2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3)
Theorem: descent1
Proof state before:
case intro.intro.intro.intro.intro.intro.inl.inl.intro.intro.intro.intro.intro.intro.intro.intro
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
hb : ¬Even b
hc : ¬Even c
p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3
⊢ ∃ p q,
    p ≠ 0 ∧
      q ≠ 0 ∧
        IsCoprime p q ∧
          (Even p ↔ ¬Even q) ∧
            (2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
              2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3)
Tactic:
exact ⟨p, q, hp, hq, hcoprime, hodd, Or.inl hcube⟩
Proof state after:
no goals
Theorem: descent1
Proof state before:
case intro.intro.intro.intro.intro.intro.inl.inr.intro.intro
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
ha : ¬Even a
hb : Even b
hc : ¬Even c
⊢ ∃ p q,
    p ≠ 0 ∧
      q ≠ 0 ∧
        IsCoprime p q ∧
          (Even p ↔ ¬Even q) ∧
            (2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
              2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3)
Tactic:
rw [add_comm] at h
Proof state after:
case intro.intro.intro.intro.intro.intro.inl.inr.intro.intro
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : b ^ 3 + a ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
ha : ¬Even a
hb : Even b
hc : ¬Even c
⊢ ∃ p q,
    p ≠ 0 ∧
      q ≠ 0 ∧
        IsCoprime p q ∧
          (Even p ↔ ¬Even q) ∧
            (2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
              2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3)
Theorem: descent1
Proof state before:
case intro.intro.intro.intro.intro.intro.inl.inr.intro.intro
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : b ^ 3 + a ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
ha : ¬Even a
hb : Even b
hc : ¬Even c
⊢ ∃ p q,
    p ≠ 0 ∧
      q ≠ 0 ∧
        IsCoprime p q ∧
          (Even p ↔ ¬Even q) ∧
            (2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
              2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3)
Tactic:
obtain ⟨p, q, hp, hq, hcoprime, hodd, hcube⟩ := descent1left hbpos h haccoprime ha hc
Proof state after:
case intro.intro.intro.intro.intro.intro.inl.inr.intro.intro.intro.intro.intro.intro.intro.intro
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : b ^ 3 + a ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
ha : ¬Even a
hb : Even b
hc : ¬Even c
p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3
⊢ ∃ p q,
    p ≠ 0 ∧
      q ≠ 0 ∧
        IsCoprime p q ∧
          (Even p ↔ ¬Even q) ∧
            (2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
              2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3)
Theorem: descent1
Proof state before:
case intro.intro.intro.intro.intro.intro.inl.inr.intro.intro.intro.intro.intro.intro.intro.intro
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : b ^ 3 + a ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
ha : ¬Even a
hb : Even b
hc : ¬Even c
p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3
⊢ ∃ p q,
    p ≠ 0 ∧
      q ≠ 0 ∧
        IsCoprime p q ∧
          (Even p ↔ ¬Even q) ∧
            (2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
              2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3)
Tactic:
refine' ⟨p, q, hp, hq, hcoprime, hodd, Or.inr <| Or.inl hcube⟩
Proof state after:
no goals
Theorem: descent1
Proof state before:
case intro.intro.intro.intro.intro.intro.inr.intro.intro
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
ha : ¬Even a
hb : ¬Even b
⊢ ∃ p q,
    p ≠ 0 ∧
      q ≠ 0 ∧
        IsCoprime p q ∧
          (Even p ↔ ¬Even q) ∧
            (2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
              2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3)
Tactic:
have := descent1left hcpos ?_ habcoprime.neg_left ?_ hb
Proof state after:
case intro.intro.intro.intro.intro.intro.inr.intro.intro.refine_3
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
ha : ¬Even a
hb : ¬Even b
this : ∃ p q, p ≠ 0 ∧ q ≠ 0 ∧ IsCoprime p q ∧ (Even p ↔ ¬Even q) ∧ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
⊢ ∃ p q,
    p ≠ 0 ∧
      q ≠ 0 ∧
        IsCoprime p q ∧
          (Even p ↔ ¬Even q) ∧
            (2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
              2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3)

case intro.intro.intro.intro.intro.intro.inr.intro.intro.refine_1
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
ha : ¬Even a
hb : ¬Even b
⊢ c ^ 3 + (-a) ^ 3 = b ^ 3

case intro.intro.intro.intro.intro.intro.inr.intro.intro.refine_2
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
ha : ¬Even a
hb : ¬Even b
⊢ ¬Even (-a)
Theorem: descent1
Proof state before:
case intro.intro.intro.intro.intro.intro.inr.intro.intro.refine_3
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
ha : ¬Even a
hb : ¬Even b
this : ∃ p q, p ≠ 0 ∧ q ≠ 0 ∧ IsCoprime p q ∧ (Even p ↔ ¬Even q) ∧ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
⊢ ∃ p q,
    p ≠ 0 ∧
      q ≠ 0 ∧
        IsCoprime p q ∧
          (Even p ↔ ¬Even q) ∧
            (2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
              2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3)

case intro.intro.intro.intro.intro.intro.inr.intro.intro.refine_1
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
ha : ¬Even a
hb : ¬Even b
⊢ c ^ 3 + (-a) ^ 3 = b ^ 3

case intro.intro.intro.intro.intro.intro.inr.intro.intro.refine_2
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
ha : ¬Even a
hb : ¬Even b
⊢ ¬Even (-a)
Tactic:
obtain ⟨p, q, hp, hq, hcoprime, hodd, hcube⟩ := this
Proof state after:
case intro.intro.intro.intro.intro.intro.inr.intro.intro.refine_3.intro.intro.intro.intro.intro.intro
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
ha : ¬Even a
hb : ¬Even b
p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
⊢ ∃ p q,
    p ≠ 0 ∧
      q ≠ 0 ∧
        IsCoprime p q ∧
          (Even p ↔ ¬Even q) ∧
            (2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
              2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3)

case intro.intro.intro.intro.intro.intro.inr.intro.intro.refine_1
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
ha : ¬Even a
hb : ¬Even b
⊢ c ^ 3 + (-a) ^ 3 = b ^ 3

case intro.intro.intro.intro.intro.intro.inr.intro.intro.refine_2
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
ha : ¬Even a
hb : ¬Even b
⊢ ¬Even (-a)
Theorem: descent1
Proof state before:
case intro.intro.intro.intro.intro.intro.inr.intro.intro.refine_3.intro.intro.intro.intro.intro.intro
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
ha : ¬Even a
hb : ¬Even b
p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
⊢ ∃ p q,
    p ≠ 0 ∧
      q ≠ 0 ∧
        IsCoprime p q ∧
          (Even p ↔ ¬Even q) ∧
            (2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
              2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3)

case intro.intro.intro.intro.intro.intro.inr.intro.intro.refine_1
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
ha : ¬Even a
hb : ¬Even b
⊢ c ^ 3 + (-a) ^ 3 = b ^ 3

case intro.intro.intro.intro.intro.intro.inr.intro.intro.refine_2
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
ha : ¬Even a
hb : ¬Even b
⊢ ¬Even (-a)
Tactic:
exact ⟨p, q, hp, hq, hcoprime, hodd, Or.inr <| Or.inr hcube⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.inr.intro.intro.refine_1
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
ha : ¬Even a
hb : ¬Even b
⊢ c ^ 3 + (-a) ^ 3 = b ^ 3

case intro.intro.intro.intro.intro.intro.inr.intro.intro.refine_2
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
ha : ¬Even a
hb : ¬Even b
⊢ ¬Even (-a)
Theorem: descent1
Proof state before:
case intro.intro.intro.intro.intro.intro.inr.intro.intro.refine_1
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
ha : ¬Even a
hb : ¬Even b
⊢ c ^ 3 + (-a) ^ 3 = b ^ 3
Tactic:
rw [← h]
Proof state after:
case intro.intro.intro.intro.intro.intro.inr.intro.intro.refine_1
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
ha : ¬Even a
hb : ¬Even b
⊢ a ^ 3 + b ^ 3 + (-a) ^ 3 = b ^ 3
Theorem: descent1
Proof state before:
case intro.intro.intro.intro.intro.intro.inr.intro.intro.refine_1
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
ha : ¬Even a
hb : ¬Even b
⊢ a ^ 3 + b ^ 3 + (-a) ^ 3 = b ^ 3
Tactic:
ring
Proof state after:
no goals
Theorem: descent1
Proof state before:
case intro.intro.intro.intro.intro.intro.inr.intro.intro.refine_2
a b c : ℤ
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
ha : ¬Even a
hb : ¬Even b
⊢ ¬Even (-a)
Tactic:
simp [ha, parity_simps]
Proof state after:
no goals
Theorem: descent11
Proof state before:
a b c d : ℤ
h : d = a ∨ d = b ∨ d = c
⊢ d ∣ a * b * c
Tactic:
rcases h with (rfl | rfl | rfl)
Proof state after:
case inl
b c d : ℤ
⊢ d ∣ d * b * c

case inr.inl
a c d : ℤ
⊢ d ∣ a * d * c

case inr.inr
a b d : ℤ
⊢ d ∣ a * b * d
Theorem: descent11
Proof state before:
case inl
b c d : ℤ
⊢ d ∣ d * b * c
Tactic:
exact (dvd_mul_right _ _).mul_right _
Proof state after:
no goals
Theorem: descent11
Proof state before:
case inr.inl
a c d : ℤ
⊢ d ∣ a * d * c
Tactic:
exact (dvd_mul_left _ _).mul_right _
Proof state after:
no goals
Theorem: descent11
Proof state before:
case inr.inr
a b d : ℤ
⊢ d ∣ a * b * d
Tactic:
exact dvd_mul_left _ _
Proof state after:
no goals
Theorem: descent2
Proof state before:
a b c : ℤ
h : FltCoprime 3 a b c
⊢ ∃ p q,
    p ≠ 0 ∧
      q ≠ 0 ∧
        IsCoprime p q ∧
          (Even p ↔ ¬Even q) ∧
            (2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
                2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3) ∧
              (2 * p).natAbs < (a ^ 3 * b ^ 3 * c ^ 3).natAbs
Tactic:
obtain ⟨p, q, hp, hq, hcoprime, hodd, hcube⟩ := descent1 a b c h
Proof state after:
case intro.intro.intro.intro.intro.intro
a b c : ℤ
h : FltCoprime 3 a b c
p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
⊢ ∃ p q,
    p ≠ 0 ∧
      q ≠ 0 ∧
        IsCoprime p q ∧
          (Even p ↔ ¬Even q) ∧
            (2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
                2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3) ∧
              (2 * p).natAbs < (a ^ 3 * b ^ 3 * c ^ 3).natAbs
Theorem: descent2
Proof state before:
case intro.intro.intro.intro.intro.intro
a b c : ℤ
h : FltCoprime 3 a b c
p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
⊢ ∃ p q,
    p ≠ 0 ∧
      q ≠ 0 ∧
        IsCoprime p q ∧
          (Even p ↔ ¬Even q) ∧
            (2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨
                2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3) ∧
              (2 * p).natAbs < (a ^ 3 * b ^ 3 * c ^ 3).natAbs
Tactic:
refine' ⟨p, q, hp, hq, hcoprime, hodd, hcube, _⟩
Proof state after:
case intro.intro.intro.intro.intro.intro
a b c : ℤ
h : FltCoprime 3 a b c
p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
⊢ (2 * p).natAbs < (a ^ 3 * b ^ 3 * c ^ 3).natAbs
Theorem: descent2
Proof state before:
case intro.intro.intro.intro.intro.intro
a b c : ℤ
h : FltCoprime 3 a b c
p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
⊢ (2 * p).natAbs < (a ^ 3 * b ^ 3 * c ^ 3).natAbs
Tactic:
obtain ⟨⟨hapos, hbpos, hcpos, -⟩, -⟩ := h
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
a b c p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
⊢ (2 * p).natAbs < (a ^ 3 * b ^ 3 * c ^ 3).natAbs
Theorem: descent2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
a b c p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
⊢ (2 * p).natAbs < (a ^ 3 * b ^ 3 * c ^ 3).natAbs
Tactic:
set P : ℤ√(-3) := ⟨p, q⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
a b c p q : ℤ
hp : p ≠ 0
hq : q ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hapos : a ≠ 0
hbpos : b ≠ 0
hcpos : c ≠ 0
P : ℤ√(-3) := { re := p, im := q }
⊢ (2 * p).natAbs < (a ^ 3 * b ^ 3 * c ^ 3).natAbs