Theorem: descent1a (Flt/Euler.lean)

State before:
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
⊢ (Even a ∧ ¬Even b ∧ ¬Even c ∨ ¬Even a ∧ Even b ∧ ¬Even c) ∨ ¬Even a ∧ ¬Even b ∧ Even c
Tactic:
have contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False :=
  by
  intro x y hcoprime hx hy
  rw [even_iff_two_dvd] at hx hy
  have := Int.isUnit_eq_one_or (hcoprime.isUnit_of_dvd' hx hy)
  norm_num at this
State after:
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
⊢ (Even a ∧ ¬Even b ∧ ¬Even c ∨ ¬Even a ∧ Even b ∧ ¬Even c) ∨ ¬Even a ∧ ¬Even b ∧ Even c

State before:
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
⊢ (Even a ∧ ¬Even b ∧ ¬Even c ∨ ¬Even a ∧ Even b ∧ ¬Even c) ∨ ¬Even a ∧ ¬Even b ∧ Even c
Tactic:
by_cases haparity : Even a <;> by_cases hbparity : Even b <;> by_cases hcparity : Even c
State after:
case pos
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
haparity : Even a
hbparity : Even b
hcparity : Even c
⊢ (Even a ∧ ¬Even b ∧ ¬Even c ∨ ¬Even a ∧ Even b ∧ ¬Even c) ∨ ¬Even a ∧ ¬Even b ∧ Even c

case neg
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
haparity : Even a
hbparity : Even b
hcparity : ¬Even c
⊢ (Even a ∧ ¬Even b ∧ ¬Even c ∨ ¬Even a ∧ Even b ∧ ¬Even c) ∨ ¬Even a ∧ ¬Even b ∧ Even c

case pos
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
haparity : Even a
hbparity : ¬Even b
hcparity : Even c
⊢ (Even a ∧ ¬Even b ∧ ¬Even c ∨ ¬Even a ∧ Even b ∧ ¬Even c) ∨ ¬Even a ∧ ¬Even b ∧ Even c

case neg
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
haparity : Even a
hbparity : ¬Even b
hcparity : ¬Even c
⊢ (Even a ∧ ¬Even b ∧ ¬Even c ∨ ¬Even a ∧ Even b ∧ ¬Even c) ∨ ¬Even a ∧ ¬Even b ∧ Even c

case pos
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
haparity : ¬Even a
hbparity : Even b
hcparity : Even c
⊢ (Even a ∧ ¬Even b ∧ ¬Even c ∨ ¬Even a ∧ Even b ∧ ¬Even c) ∨ ¬Even a ∧ ¬Even b ∧ Even c

case neg
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
haparity : ¬Even a
hbparity : Even b
hcparity : ¬Even c
⊢ (Even a ∧ ¬Even b ∧ ¬Even c ∨ ¬Even a ∧ Even b ∧ ¬Even c) ∨ ¬Even a ∧ ¬Even b ∧ Even c

case pos
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
haparity : ¬Even a
hbparity : ¬Even b
hcparity : Even c
⊢ (Even a ∧ ¬Even b ∧ ¬Even c ∨ ¬Even a ∧ Even b ∧ ¬Even c) ∨ ¬Even a ∧ ¬Even b ∧ Even c

case neg
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
haparity : ¬Even a
hbparity : ¬Even b
hcparity : ¬Even c
⊢ (Even a ∧ ¬Even b ∧ ¬Even c ∨ ¬Even a ∧ Even b ∧ ¬Even c) ∨ ¬Even a ∧ ¬Even b ∧ Even c

State before:
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
⊢ ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
Tactic:
intro x y hcoprime hx hy
State after:
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
x y : ℤ
hcoprime : IsCoprime x y
hx : Even x
hy : Even y
⊢ False

State before:
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
x y : ℤ
hcoprime : IsCoprime x y
hx : Even x
hy : Even y
⊢ False
Tactic:
rw [even_iff_two_dvd] at hx hy
State after:
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
x y : ℤ
hcoprime : IsCoprime x y
hx : 2 ∣ x
hy : 2 ∣ y
⊢ False

State before:
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
x y : ℤ
hcoprime : IsCoprime x y
hx : 2 ∣ x
hy : 2 ∣ y
⊢ False
Tactic:
have := Int.isUnit_eq_one_or (hcoprime.isUnit_of_dvd' hx hy)
State after:
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
x y : ℤ
hcoprime : IsCoprime x y
hx : 2 ∣ x
hy : 2 ∣ y
this : 2 = 1 ∨ 2 = -1
⊢ False

State before:
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
x y : ℤ
hcoprime : IsCoprime x y
hx : 2 ∣ x
hy : 2 ∣ y
this : 2 = 1 ∨ 2 = -1
⊢ False
Tactic:
norm_num at this
State after:
no goals

State before:
case pos
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
haparity : Even a
hbparity : Even b
hcparity : Even c
⊢ (Even a ∧ ¬Even b ∧ ¬Even c ∨ ¬Even a ∧ Even b ∧ ¬Even c) ∨ ¬Even a ∧ ¬Even b ∧ Even c
Tactic:
exact False.elim (contra habcoprime ‹_› ‹_›)
State after:
no goals

State before:
case neg
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
haparity : Even a
hbparity : Even b
hcparity : ¬Even c
⊢ (Even a ∧ ¬Even b ∧ ¬Even c ∨ ¬Even a ∧ Even b ∧ ¬Even c) ∨ ¬Even a ∧ ¬Even b ∧ Even c
Tactic:
exact False.elim (contra habcoprime ‹_› ‹_›)
State after:
no goals

State before:
case pos
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
haparity : Even a
hbparity : ¬Even b
hcparity : Even c
⊢ (Even a ∧ ¬Even b ∧ ¬Even c ∨ ¬Even a ∧ Even b ∧ ¬Even c) ∨ ¬Even a ∧ ¬Even b ∧ Even c
Tactic:
exact False.elim (contra haccoprime ‹_› ‹_›)
State after:
no goals

State before:
case neg
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
haparity : Even a
hbparity : ¬Even b
hcparity : ¬Even c
⊢ (Even a ∧ ¬Even b ∧ ¬Even c ∨ ¬Even a ∧ Even b ∧ ¬Even c) ∨ ¬Even a ∧ ¬Even b ∧ Even c
Tactic:
tauto
State after:
no goals

State before:
case pos
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
haparity : ¬Even a
hbparity : Even b
hcparity : Even c
⊢ (Even a ∧ ¬Even b ∧ ¬Even c ∨ ¬Even a ∧ Even b ∧ ¬Even c) ∨ ¬Even a ∧ ¬Even b ∧ Even c
Tactic:
exact False.elim (contra hbccoprime ‹_› ‹_›)
State after:
no goals

State before:
case neg
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
haparity : ¬Even a
hbparity : Even b
hcparity : ¬Even c
⊢ (Even a ∧ ¬Even b ∧ ¬Even c ∨ ¬Even a ∧ Even b ∧ ¬Even c) ∨ ¬Even a ∧ ¬Even b ∧ Even c
Tactic:
tauto
State after:
no goals

State before:
case pos
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
haparity : ¬Even a
hbparity : ¬Even b
hcparity : Even c
⊢ (Even a ∧ ¬Even b ∧ ¬Even c ∨ ¬Even a ∧ Even b ∧ ¬Even c) ∨ ¬Even a ∧ ¬Even b ∧ Even c
Tactic:
tauto
State after:
no goals

State before:
case neg
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
haparity : ¬Even a
hbparity : ¬Even b
hcparity : ¬Even c
⊢ (Even a ∧ ¬Even b ∧ ¬Even c ∨ ¬Even a ∧ Even b ∧ ¬Even c) ∨ ¬Even a ∧ ¬Even b ∧ Even c
Tactic:
exfalso
State after:
case neg.h
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
haparity : ¬Even a
hbparity : ¬Even b
hcparity : ¬Even c
⊢ False

State before:
case neg.h
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
haparity : ¬Even a
hbparity : ¬Even b
hcparity : ¬Even c
⊢ False
Tactic:
apply hcparity
State after:
case neg.h
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
haparity : ¬Even a
hbparity : ¬Even b
hcparity : ¬Even c
⊢ Even c

State before:
case neg.h
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
haparity : ¬Even a
hbparity : ¬Even b
hcparity : ¬Even c
⊢ Even c
Tactic:
rw [← Int.even_pow' three_ne_zero, ← h]
State after:
case neg.h
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
haparity : ¬Even a
hbparity : ¬Even b
hcparity : ¬Even c
⊢ Even (a ^ 3 + b ^ 3)

State before:
case neg.h
a b c : ℤ
h : a ^ 3 + b ^ 3 = c ^ 3
habcoprime : IsCoprime a b
haccoprime : IsCoprime a c
hbccoprime : IsCoprime b c
contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False
haparity : ¬Even a
hbparity : ¬Even b
hcparity : ¬Even c
⊢ Even (a ^ 3 + b ^ 3)
Tactic:
simp [haparity, hbparity, three_ne_zero, parity_simps]
State after:
no goals