Theorem: exercise4_6 (LeanCourse/Assignments/Solutions/Solutions4.lean)

State before:
a b : ℕ
ha : 0 < a
hb : 0 < b
⊢ ¬IsSquare (a ^ 2 + b) ∨ ¬IsSquare (b ^ 2 + a)
Tactic:
have h1 : ∀ {a b : ℕ}, 0 < a → a ≤ b → ¬ IsSquare (b ^ 2 + a)
State after:
case h1
a b : ℕ
ha : 0 < a
hb : 0 < b
⊢ ∀ {a b : ℕ}, 0 < a → a ≤ b → ¬IsSquare (b ^ 2 + a)

a b : ℕ
ha : 0 < a
hb : 0 < b
h1 : ∀ {a b : ℕ}, 0 < a → a ≤ b → ¬IsSquare (b ^ 2 + a)
⊢ ¬IsSquare (a ^ 2 + b) ∨ ¬IsSquare (b ^ 2 + a)

State before:
a b : ℕ
ha : 0 < a
hb : 0 < b
h1 : ∀ {a b : ℕ}, 0 < a → a ≤ b → ¬IsSquare (b ^ 2 + a)
⊢ ¬IsSquare (a ^ 2 + b) ∨ ¬IsSquare (b ^ 2 + a)
Tactic:
obtain h|h := le_total a b
State after:
case inl
a b : ℕ
ha : 0 < a
hb : 0 < b
h1 : ∀ {a b : ℕ}, 0 < a → a ≤ b → ¬IsSquare (b ^ 2 + a)
h : a ≤ b
⊢ ¬IsSquare (a ^ 2 + b) ∨ ¬IsSquare (b ^ 2 + a)

case inr
a b : ℕ
ha : 0 < a
hb : 0 < b
h1 : ∀ {a b : ℕ}, 0 < a → a ≤ b → ¬IsSquare (b ^ 2 + a)
h : b ≤ a
⊢ ¬IsSquare (a ^ 2 + b) ∨ ¬IsSquare (b ^ 2 + a)

State before:
case h1
a b : ℕ
ha : 0 < a
hb : 0 < b
⊢ ∀ {a b : ℕ}, 0 < a → a ≤ b → ¬IsSquare (b ^ 2 + a)
Tactic:
intro a b ha hab ⟨c, hc⟩
State after:
case h1
a✝ b✝ : ℕ
ha✝ : 0 < a✝
hb : 0 < b✝
a b : ℕ
ha : 0 < a
hab : a ≤ b
c : ℕ
hc : b ^ 2 + a = c * c
⊢ False

State before:
case h1
a✝ b✝ : ℕ
ha✝ : 0 < a✝
hb : 0 < b✝
a b : ℕ
ha : 0 < a
hab : a ≤ b
c : ℕ
hc : b ^ 2 + a = c * c
⊢ False
Tactic:
rw [pow_two] at hc
State after:
case h1
a✝ b✝ : ℕ
ha✝ : 0 < a✝
hb : 0 < b✝
a b : ℕ
ha : 0 < a
hab : a ≤ b
c : ℕ
hc : b * b + a = c * c
⊢ False

State before:
case h1
a✝ b✝ : ℕ
ha✝ : 0 < a✝
hb : 0 < b✝
a b : ℕ
ha : 0 < a
hab : a ≤ b
c : ℕ
hc : b * b + a = c * c
⊢ False
Tactic:
have : b * b < c * c := by linarith
State after:
case h1
a✝ b✝ : ℕ
ha✝ : 0 < a✝
hb : 0 < b✝
a b : ℕ
ha : 0 < a
hab : a ≤ b
c : ℕ
hc : b * b + a = c * c
this : b * b < c * c
⊢ False

State before:
case h1
a✝ b✝ : ℕ
ha✝ : 0 < a✝
hb : 0 < b✝
a b : ℕ
ha : 0 < a
hab : a ≤ b
c : ℕ
hc : b * b + a = c * c
this : b * b < c * c
⊢ False
Tactic:
have : b < c := by exact?
State after:
case h1
a✝ b✝ : ℕ
ha✝ : 0 < a✝
hb : 0 < b✝
a b : ℕ
ha : 0 < a
hab : a ≤ b
c : ℕ
hc : b * b + a = c * c
this✝ : b * b < c * c
this : b < c
⊢ False

State before:
case h1
a✝ b✝ : ℕ
ha✝ : 0 < a✝
hb : 0 < b✝
a b : ℕ
ha : 0 < a
hab : a ≤ b
c : ℕ
hc : b * b + a = c * c
this✝ : b * b < c * c
this : b < c
⊢ False
Tactic:
have : c * c < (b + 1) * (b + 1) := by linarith
State after:
case h1
a✝ b✝ : ℕ
ha✝ : 0 < a✝
hb : 0 < b✝
a b : ℕ
ha : 0 < a
hab : a ≤ b
c : ℕ
hc : b * b + a = c * c
this✝¹ : b * b < c * c
this✝ : b < c
this : c * c < (b + 1) * (b + 1)
⊢ False

State before:
case h1
a✝ b✝ : ℕ
ha✝ : 0 < a✝
hb : 0 < b✝
a b : ℕ
ha : 0 < a
hab : a ≤ b
c : ℕ
hc : b * b + a = c * c
this✝¹ : b * b < c * c
this✝ : b < c
this : c * c < (b + 1) * (b + 1)
⊢ False
Tactic:
have : c < b + 1 := by exact?
State after:
case h1
a✝ b✝ : ℕ
ha✝ : 0 < a✝
hb : 0 < b✝
a b : ℕ
ha : 0 < a
hab : a ≤ b
c : ℕ
hc : b * b + a = c * c
this✝² : b * b < c * c
this✝¹ : b < c
this✝ : c * c < (b + 1) * (b + 1)
this : c < b + 1
⊢ False

State before:
case h1
a✝ b✝ : ℕ
ha✝ : 0 < a✝
hb : 0 < b✝
a b : ℕ
ha : 0 < a
hab : a ≤ b
c : ℕ
hc : b * b + a = c * c
this✝² : b * b < c * c
this✝¹ : b < c
this✝ : c * c < (b + 1) * (b + 1)
this : c < b + 1
⊢ False
Tactic:
exact?
State after:
no goals

State before:
a✝ b✝ : ℕ
ha✝ : 0 < a✝
hb : 0 < b✝
a b : ℕ
ha : 0 < a
hab : a ≤ b
c : ℕ
hc : b * b + a = c * c
⊢ b * b < c * c
Tactic:
linarith
State after:
no goals

State before:
a✝ b✝ : ℕ
ha✝ : 0 < a✝
hb : 0 < b✝
a b : ℕ
ha : 0 < a
hab : a ≤ b
c : ℕ
hc : b * b + a = c * c
this : b * b < c * c
⊢ b < c
Tactic:
exact?
State after:
no goals

State before:
a✝ b✝ : ℕ
ha✝ : 0 < a✝
hb : 0 < b✝
a b : ℕ
ha : 0 < a
hab : a ≤ b
c : ℕ
hc : b * b + a = c * c
this✝ : b * b < c * c
this : b < c
⊢ c * c < (b + 1) * (b + 1)
Tactic:
linarith
State after:
no goals

State before:
a✝ b✝ : ℕ
ha✝ : 0 < a✝
hb : 0 < b✝
a b : ℕ
ha : 0 < a
hab : a ≤ b
c : ℕ
hc : b * b + a = c * c
this✝¹ : b * b < c * c
this✝ : b < c
this : c * c < (b + 1) * (b + 1)
⊢ c < b + 1
Tactic:
exact?
State after:
no goals

State before:
case inl
a b : ℕ
ha : 0 < a
hb : 0 < b
h1 : ∀ {a b : ℕ}, 0 < a → a ≤ b → ¬IsSquare (b ^ 2 + a)
h : a ≤ b
⊢ ¬IsSquare (a ^ 2 + b) ∨ ¬IsSquare (b ^ 2 + a)
Tactic:
exact .inr (h1 ha h)
State after:
no goals

State before:
case inr
a b : ℕ
ha : 0 < a
hb : 0 < b
h1 : ∀ {a b : ℕ}, 0 < a → a ≤ b → ¬IsSquare (b ^ 2 + a)
h : b ≤ a
⊢ ¬IsSquare (a ^ 2 + b) ∨ ¬IsSquare (b ^ 2 + a)
Tactic:
exact .inl (h1 hb h)
State after:
no goals