Theorem: Usa2023P4.halve_even (Compfiles/Usa2023P4.lean)

State before:
x : ℕ+
he : Even ↑x
⊢ 0 < ↑x / 2
Tactic:
obtain ⟨x, hx⟩ := x
State after:
case mk
x : ℕ
hx : 0 < x
he : Even ↑⟨x, hx⟩
⊢ 0 < ↑⟨x, hx⟩ / 2

State before:
case mk
x : ℕ
hx : 0 < x
he : Even ↑⟨x, hx⟩
⊢ 0 < ↑⟨x, hx⟩ / 2
Tactic:
obtain ⟨t, ht⟩ := he
State after:
case mk.intro
x : ℕ
hx : 0 < x
t : ℕ
ht : ↑⟨x, hx⟩ = t + t
⊢ 0 < ↑⟨x, hx⟩ / 2

State before:
case mk.intro
x : ℕ
hx : 0 < x
t : ℕ
ht : ↑⟨x, hx⟩ = t + t
⊢ 0 < ↑⟨x, hx⟩ / 2
Tactic:
dsimp at *
State after:
case mk.intro
x : ℕ
hx : 0 < x
t : ℕ
ht : x = t + t
⊢ 0 < x / 2

State before:
case mk.intro
x : ℕ
hx : 0 < x
t : ℕ
ht : x = t + t
⊢ 0 < x / 2
Tactic:
omega
State after:
no goals