Theorem: Bulgaria1998P6.lemma_1 (Compfiles/Bulgaria1998P6.lean)

State before:
s t u : ℤ
hs : 0 < s
ht : 0 < t
hu : 0 < u
h : s ^ 4 - t ^ 4 = u ^ 2
⊢ False
Tactic:
replace h : s^4 = t^4 + u^2 := eq_add_of_sub_eq' h
State after:
s t u : ℤ
hs : 0 < s
ht : 0 < t
hu : 0 < u
h : s ^ 4 = t ^ 4 + u ^ 2
⊢ False

State before:
s t u : ℤ
hs : 0 < s
ht : 0 < t
hu : 0 < u
h : s ^ 4 = t ^ 4 + u ^ 2
⊢ False
Tactic:
lift s to ℕ using Int.le_of_lt hs
State after:
case intro
t u : ℤ
ht : 0 < t
hu : 0 < u
s : ℕ
hs : 0 < ↑s
h : ↑s ^ 4 = t ^ 4 + u ^ 2
⊢ False

State before:
case intro
t u : ℤ
ht : 0 < t
hu : 0 < u
s : ℕ
hs : 0 < ↑s
h : ↑s ^ 4 = t ^ 4 + u ^ 2
⊢ False
Tactic:
lift t to ℕ using Int.le_of_lt ht
State after:
case intro.intro
u : ℤ
hu : 0 < u
s : ℕ
hs : 0 < ↑s
t : ℕ
ht : 0 < ↑t
h : ↑s ^ 4 = ↑t ^ 4 + u ^ 2
⊢ False

State before:
case intro.intro
u : ℤ
hu : 0 < u
s : ℕ
hs : 0 < ↑s
t : ℕ
ht : 0 < ↑t
h : ↑s ^ 4 = ↑t ^ 4 + u ^ 2
⊢ False
Tactic:
lift u to ℕ using Int.le_of_lt hu
State after:
case intro.intro.intro
s : ℕ
hs : 0 < ↑s
t : ℕ
ht : 0 < ↑t
u : ℕ
hu : 0 < ↑u
h : ↑s ^ 4 = ↑t ^ 4 + ↑u ^ 2
⊢ False

State before:
case intro.intro.intro
s : ℕ
hs : 0 < ↑s
t : ℕ
ht : 0 < ↑t
u : ℕ
hu : 0 < ↑u
h : ↑s ^ 4 = ↑t ^ 4 + ↑u ^ 2
⊢ False
Tactic:
replace hs : 0 < s := Int.ofNat_pos.mp hs
State after:
case intro.intro.intro
s t : ℕ
ht : 0 < ↑t
u : ℕ
hu : 0 < ↑u
h : ↑s ^ 4 = ↑t ^ 4 + ↑u ^ 2
hs : 0 < s
⊢ False

State before:
case intro.intro.intro
s t : ℕ
ht : 0 < ↑t
u : ℕ
hu : 0 < ↑u
h : ↑s ^ 4 = ↑t ^ 4 + ↑u ^ 2
hs : 0 < s
⊢ False
Tactic:
replace ht : 0 < t := Int.ofNat_pos.mp ht
State after:
case intro.intro.intro
s t u : ℕ
hu : 0 < ↑u
h : ↑s ^ 4 = ↑t ^ 4 + ↑u ^ 2
hs : 0 < s
ht : 0 < t
⊢ False

State before:
case intro.intro.intro
s t u : ℕ
hu : 0 < ↑u
h : ↑s ^ 4 = ↑t ^ 4 + ↑u ^ 2
hs : 0 < s
ht : 0 < t
⊢ False
Tactic:
replace hy : 0 < u := Int.ofNat_pos.mp hu
State after:
case intro.intro.intro
s t u : ℕ
hu : 0 < ↑u
h : ↑s ^ 4 = ↑t ^ 4 + ↑u ^ 2
hs : 0 < s
ht : 0 < t
hy : 0 < u
⊢ False

State before:
case intro.intro.intro
s t u : ℕ
hu : 0 < ↑u
h : ↑s ^ 4 = ↑t ^ 4 + ↑u ^ 2
hs : 0 < s
ht : 0 < t
hy : 0 < u
⊢ False
Tactic:
have h' : s ^ 4 = t ^ 4 + u ^ 2 := by exact Int.ofNat_inj.mp h
State after:
case intro.intro.intro
s t u : ℕ
hu : 0 < ↑u
h : ↑s ^ 4 = ↑t ^ 4 + ↑u ^ 2
hs : 0 < s
ht : 0 < t
hy : 0 < u
h' : s ^ 4 = t ^ 4 + u ^ 2
⊢ False

State before:
case intro.intro.intro
s t u : ℕ
hu : 0 < ↑u
h : ↑s ^ 4 = ↑t ^ 4 + ↑u ^ 2
hs : 0 < s
ht : 0 < t
hy : 0 < u
h' : s ^ 4 = t ^ 4 + u ^ 2
⊢ False
Tactic:
exact lemma_1' s t u hs ht hy h'
State after:
no goals

State before:
s t u : ℕ
hu : 0 < ↑u
h : ↑s ^ 4 = ↑t ^ 4 + ↑u ^ 2
hs : 0 < s
ht : 0 < t
hy : 0 < u
⊢ s ^ 4 = t ^ 4 + u ^ 2
Tactic:
exact Int.ofNat_inj.mp h
State after:
no goals