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

State before:
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
hx : x < 2
⊢ f x = 2 / (2 - x)
Tactic:
have hx' : 2 - x ≠ 0 := (tsub_pos_of_lt hx).ne'
State after:
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
hx : x < 2
hx' : 2 - x ≠ 0
⊢ f x = 2 / (2 - x)

State before:
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
hx : x < 2
hx' : 2 - x ≠ 0
⊢ f x = 2 / (2 - x)
Tactic:
have hfx : f x ≠ 0 := hf.map_ne_zero_iff.2 hx
State after:
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
hx : x < 2
hx' : 2 - x ≠ 0
hfx : f x ≠ 0
⊢ f x = 2 / (2 - x)

State before:
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
hx : x < 2
hx' : 2 - x ≠ 0
hfx : f x ≠ 0
⊢ f x = 2 / (2 - x)
Tactic:
apply le_antisymm
State after:
case a
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
hx : x < 2
hx' : 2 - x ≠ 0
hfx : f x ≠ 0
⊢ f x ≤ 2 / (2 - x)

case a
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
hx : x < 2
hx' : 2 - x ≠ 0
hfx : f x ≠ 0
⊢ 2 / (2 - x) ≤ f x

State before:
case a
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
hx : x < 2
hx' : 2 - x ≠ 0
hfx : f x ≠ 0
⊢ f x ≤ 2 / (2 - x)
Tactic:
rw [NNReal.le_div_iff hx', ← NNReal.le_div_iff' hfx, tsub_le_iff_right, ← hf.map_eq_zero,
 hf.map_add, div_mul_cancel₀ _ hfx, hf.map_two, zero_mul]
State after:
no goals

State before:
case a
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
hx : x < 2
hx' : 2 - x ≠ 0
hfx : f x ≠ 0
⊢ 2 / (2 - x) ≤ f x
Tactic:
rw [NNReal.div_le_iff' hx', ← hf.map_eq_zero]
State after:
case a
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
hx : x < 2
hx' : 2 - x ≠ 0
hfx : f x ≠ 0
⊢ f ((2 - x) * f x) = 0

State before:
case a
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
hx : x < 2
hx' : 2 - x ≠ 0
hfx : f x ≠ 0
⊢ f ((2 - x) * f x) = 0
Tactic:
refine (mul_eq_zero.1 ?_).resolve_right hfx
State after:
case a
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
hx : x < 2
hx' : 2 - x ≠ 0
hfx : f x ≠ 0
⊢ f ((2 - x) * f x) * f x = 0

State before:
case a
f : ℝ≥0 → ℝ≥0
hf : IsGood f
x y : ℝ≥0
hx : x < 2
hx' : 2 - x ≠ 0
hfx : f x ≠ 0
⊢ f ((2 - x) * f x) * f x = 0
Tactic:
rw [hf.map_add_rev, hf.map_eq_zero, tsub_add_cancel_of_le hx.le]
State after:
no goals