Theorem: Imo1986P5.IsGood.map_eq_zero (Compfiles/Imo1986P5.lean)

State before:
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
⊢ f x = 0 ↔ 2 ≤ x
Tactic:
refine ⟨fun hx₀ ↦ not_lt.1 fun hlt ↦ hf.map_ne_zero x hlt hx₀, fun hle ↦ ?_⟩
State after:
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
hle : 2 ≤ x
⊢ f x = 0

State before:
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
hle : 2 ≤ x
⊢ f x = 0
Tactic:
rcases exists_add_of_le hle with ⟨x, rfl⟩
State after:
case intro
f : ℝ≥0 → ℝ≥0
hf : IsGood f
y x : ℝ≥0
hle : 2 ≤ 2 + x
⊢ f (2 + x) = 0

State before:
case intro
f : ℝ≥0 → ℝ≥0
hf : IsGood f
y x : ℝ≥0
hle : 2 ≤ 2 + x
⊢ f (2 + x) = 0
Tactic:
rw [add_comm, hf.map_add, hf.map_two, mul_zero]
State after:
no goals