case refine_1
F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.52366
δ : Type ?u.52369
inst✝³ : OrderedAddCommGroup α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : AddMonoidHomClass F α β
f : F
inst✝ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x < x_1
h : StrictMono ↑f
a : α
⊢ 0 < a → 0 < ↑f a

case refine_2
F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.52366
δ : Type ?u.52369
inst✝³ : OrderedAddCommGroup α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : AddMonoidHomClass F α β
f : F
inst✝ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x < x_1
h : ∀ (a : α), 0 < a → 0 < ↑f a
a b : α
hl : a < b
⊢ ↑f a < ↑f b
F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.52366
δ : Type ?u.52369
inst✝³ : OrderedAddCommGroup α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : AddMonoidHomClass F α β
f : F
inst✝ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x < x_1
⊢ StrictMono ↑f ↔ ∀ (a : α), 0 < a → 0 < ↑f a
refine ⟨fun h a => ?_, fun h a b hl => ?_⟩
case refine_1
F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.52366
δ : Type ?u.52369
inst✝³ : OrderedAddCommGroup α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : AddMonoidHomClass F α β
f : F
inst✝ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x < x_1
h : StrictMono ↑f
a : α
⊢ 0 < a → ↑f 0 < ↑f a
case refine_1
F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.52366
δ : Type ?u.52369
inst✝³ : OrderedAddCommGroup α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : AddMonoidHomClass F α β
f : F
inst✝ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x < x_1
h : StrictMono ↑f
a : α
⊢ 0 < a → 0 < ↑f a
rw [← map_zero f]
no goals
case refine_1
F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.52366
δ : Type ?u.52369
inst✝³ : OrderedAddCommGroup α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : AddMonoidHomClass F α β
f : F
inst✝ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x < x_1
h : StrictMono ↑f
a : α
⊢ 0 < a → ↑f 0 < ↑f a
apply h
case refine_2
F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.52366
δ : Type ?u.52369
inst✝³ : OrderedAddCommGroup α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : AddMonoidHomClass F α β
f : F
inst✝ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x < x_1
h : ∀ (a : α), 0 < a → 0 < ↑f a
a b : α
hl : a < b
⊢ ↑f a < ↑f (b - a) + ↑f a
case refine_2
F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.52366
δ : Type ?u.52369
inst✝³ : OrderedAddCommGroup α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : AddMonoidHomClass F α β
f : F
inst✝ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x < x_1
h : ∀ (a : α), 0 < a → 0 < ↑f a
a b : α
hl : a < b
⊢ ↑f a < ↑f b
rw [← sub_add_cancel b a, map_add f]
no goals
case refine_2
F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.52366
δ : Type ?u.52369
inst✝³ : OrderedAddCommGroup α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : AddMonoidHomClass F α β
f : F
inst✝ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x < x_1
h : ∀ (a : α), 0 < a → 0 < ↑f a
a b : α
hl : a < b
⊢ ↑f a < ↑f (b - a) + ↑f a
exact lt_add_of_pos_left _ (h _ <| sub_pos.2 hl)