Theorem: HTPI.image_fqn_unbdd (HTPILib/Chap8Part2.lean)

State before:
⊢ ∀ (m : ℕ), ∃ n ∈ image fqn (Univ ℚ), n ≥ m
Tactic:
fix m : Nat
State after:
m : ℕ
⊢ ∃ n ∈ image fqn (Univ ℚ), n ≥ m

State before:
m : ℕ
⊢ ∃ n ∈ image fqn (Univ ℚ), n ≥ m
Tactic:
set n : Nat := fqn ↑m
State after:
m : ℕ
n : ℕ := fqn ↑m
⊢ ∃ n ∈ image fqn (Univ ℚ), n ≥ m

State before:
m : ℕ
n : ℕ := fqn ↑m
⊢ ∃ n ∈ image fqn (Univ ℚ), n ≥ m
Tactic:
apply Exists.intro n
State after:
m : ℕ
n : ℕ := fqn ↑m
⊢ n ∈ image fqn (Univ ℚ) ∧ n ≥ m

State before:
m : ℕ
n : ℕ := fqn ↑m
⊢ n ∈ image fqn (Univ ℚ) ∧ n ≥ m
Tactic:
apply And.intro
State after:
case left
m : ℕ
n : ℕ := fqn ↑m
⊢ n ∈ image fqn (Univ ℚ)

case right
m : ℕ
n : ℕ := fqn ↑m
⊢ n ≥ m

State before:
case left
m : ℕ
n : ℕ := fqn ↑m
⊢ n ∈ image fqn (Univ ℚ)
Tactic:
define
State after:
case left
m : ℕ
n : ℕ := fqn ↑m
⊢ ∃ x ∈ Univ ℚ, fqn x = n

State before:
case left
m : ℕ
n : ℕ := fqn ↑m
⊢ ∃ x ∈ Univ ℚ, fqn x = n
Tactic:
apply Exists.intro ↑m
State after:
case left
m : ℕ
n : ℕ := fqn ↑m
⊢ ↑m ∈ Univ ℚ ∧ fqn ↑m = n

State before:
case left
m : ℕ
n : ℕ := fqn ↑m
⊢ ↑m ∈ Univ ℚ ∧ fqn ↑m = n
Tactic:
apply And.intro (elt_Univ (↑m : Rat))
State after:
case left
m : ℕ
n : ℕ := fqn ↑m
⊢ fqn ↑m = n

State before:
case left
m : ℕ
n : ℕ := fqn ↑m
⊢ fqn ↑m = n
Tactic:
rfl
State after:
no goals

State before:
case right
m : ℕ
n : ℕ := fqn ↑m
⊢ n ≥ m
Tactic:
show n ≥ m from
  calc n
    _ = tri (2 * m + 1) + 2 * m := by rfl
    _ ≥ m := by linarith
State after:
no goals

State before:
m : ℕ
n : ℕ := fqn ↑m
⊢ n = tri (2 * m + 1) + 2 * m
Tactic:
rfl
State after:
no goals

State before:
m : ℕ
n : ℕ := fqn ↑m
⊢ tri (2 * m + 1) + 2 * m ≥ m
Tactic:
linarith
State after:
no goals