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

State before:
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x✝ y x : ℝ≥0
hx : 2 ≤ x
⊢ f x = 2 / (2 - x)
Tactic:
rwa [tsub_eq_zero_of_le hx, div_zero, hf.map_eq_zero]
State after:
no goals