Theorem: descent1 (Flt/Euler.lean)

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

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

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

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

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

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

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

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

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

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

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

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

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