[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : OrderedAddCommMonoid α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : OrderAddMonoidHomClass F α β
f : F
a : α
ha : 0 ≤ a
⊢ 0 ≤ ↑f a
[PROOFSTEP]
rw [← map_zero f]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : OrderedAddCommMonoid α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : OrderAddMonoidHomClass F α β
f : F
a : α
ha : 0 ≤ a
⊢ ↑f 0 ≤ ↑f a
[PROOFSTEP]
exact OrderHomClass.mono _ ha
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : OrderedAddCommMonoid α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : OrderAddMonoidHomClass F α β
f : F
a : α
ha : a ≤ 0
⊢ ↑f a ≤ 0
[PROOFSTEP]
rw [← map_zero f]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : OrderedAddCommMonoid α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : OrderAddMonoidHomClass F α β
f : F
a : α
ha : a ≤ 0
⊢ ↑f a ≤ ↑f 0
[PROOFSTEP]
exact OrderHomClass.mono _ ha
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : OrderedAddCommGroup α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : AddMonoidHomClass F α β
f : F
h : Monotone ↑f
a : α
⊢ 0 ≤ a → 0 ≤ ↑f a
[PROOFSTEP]
rw [← map_zero f]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : OrderedAddCommGroup α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : AddMonoidHomClass F α β
f : F
h : Monotone ↑f
a : α
⊢ 0 ≤ a → ↑f 0 ≤ ↑f a
[PROOFSTEP]
apply h
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : OrderedAddCommGroup α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : AddMonoidHomClass F α β
f : F
h : ∀ (a : α), 0 ≤ a → 0 ≤ ↑f a
a b : α
hl : a ≤ b
⊢ ↑f a ≤ ↑f b
[PROOFSTEP]
rw [← sub_add_cancel b a, map_add f]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : OrderedAddCommGroup α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : AddMonoidHomClass F α β
f : F
h : ∀ (a : α), 0 ≤ a → 0 ≤ ↑f a
a b : α
hl : a ≤ b
⊢ ↑f a ≤ ↑f (b - a) + ↑f a
[PROOFSTEP]
exact le_add_of_nonneg_left (h _ <| sub_nonneg.2 hl)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
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
[PROOFSTEP]
refine ⟨fun h a => ?_, fun h a b hl => ?_⟩
[GOAL]
case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
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
[PROOFSTEP]
rw [← map_zero f]
[GOAL]
case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
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
[PROOFSTEP]
apply h
[GOAL]
case refine_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
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
[PROOFSTEP]
rw [← sub_add_cancel b a, map_add f]
[GOAL]
case refine_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
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
[PROOFSTEP]
exact lt_add_of_pos_left _ (h _ <| sub_pos.2 hl)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : MulOneClass γ
inst✝ : MulOneClass δ
f✝ g✝ f g : α →*o β
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨⟨_, _⟩⟩, _⟩ := f
[GOAL]
case mk.mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : MulOneClass γ
inst✝ : MulOneClass δ
f g✝ g : α →*o β
toFun✝ : α → β
map_one'✝ : toFun✝ 1 = 1
map_mul'✝ :
  ∀ (x y : α),
    OneHom.toFun { toFun := toFun✝, map_one' := map_one'✝ } (x * y) =
      OneHom.toFun { toFun := toFun✝, map_one' := map_one'✝ } x *
        OneHom.toFun { toFun := toFun✝, map_one' := map_one'✝ } y
monotone'✝ : Monotone (↑{ toOneHom := { toFun := toFun✝, map_one' := map_one'✝ }, map_mul' := map_mul'✝ }).toFun
h :
  (fun f => f.toFun)
      { toMonoidHom := { toOneHom := { toFun := toFun✝, map_one' := map_one'✝ }, map_mul' := map_mul'✝ },
        monotone' := monotone'✝ } =
    (fun f => f.toFun) g
⊢ { toMonoidHom := { toOneHom := { toFun := toFun✝, map_one' := map_one'✝ }, map_mul' := map_mul'✝ },
      monotone' := monotone'✝ } =
    g
[PROOFSTEP]
obtain ⟨⟨⟨_, _⟩⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk.mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : MulOneClass γ
inst✝ : MulOneClass δ
f g : α →*o β
toFun✝¹ : α → β
map_one'✝¹ : toFun✝¹ 1 = 1
map_mul'✝¹ :
  ∀ (x y : α),
    OneHom.toFun { toFun := toFun✝¹, map_one' := map_one'✝¹ } (x * y) =
      OneHom.toFun { toFun := toFun✝¹, map_one' := map_one'✝¹ } x *
        OneHom.toFun { toFun := toFun✝¹, map_one' := map_one'✝¹ } y
monotone'✝¹ : Monotone (↑{ toOneHom := { toFun := toFun✝¹, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ }).toFun
toFun✝ : α → β
map_one'✝ : toFun✝ 1 = 1
map_mul'✝ :
  ∀ (x y : α),
    OneHom.toFun { toFun := toFun✝, map_one' := map_one'✝ } (x * y) =
      OneHom.toFun { toFun := toFun✝, map_one' := map_one'✝ } x *
        OneHom.toFun { toFun := toFun✝, map_one' := map_one'✝ } y
monotone'✝ : Monotone (↑{ toOneHom := { toFun := toFun✝, map_one' := map_one'✝ }, map_mul' := map_mul'✝ }).toFun
h :
  (fun f => f.toFun)
      { toMonoidHom := { toOneHom := { toFun := toFun✝¹, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ },
        monotone' := monotone'✝¹ } =
    (fun f => f.toFun)
      { toMonoidHom := { toOneHom := { toFun := toFun✝, map_one' := map_one'✝ }, map_mul' := map_mul'✝ },
        monotone' := monotone'✝ }
⊢ { toMonoidHom := { toOneHom := { toFun := toFun✝¹, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ },
      monotone' := monotone'✝¹ } =
    { toMonoidHom := { toOneHom := { toFun := toFun✝, map_one' := map_one'✝ }, map_mul' := map_mul'✝ },
      monotone' := monotone'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : MulOneClass γ
inst✝ : MulOneClass δ
f✝ g f : α →*o β
h : Monotone (↑↑f).toFun
⊢ { toMonoidHom := ↑f, monotone' := h } = f
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : MulOneClass γ
inst✝ : MulOneClass δ
f✝ g f : α →*o β
h : Monotone (↑↑f).toFun
a✝ : α
⊢ ↑{ toMonoidHom := ↑f, monotone' := h } a✝ = ↑f a✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : MulOneClass γ
inst✝ : MulOneClass δ
f✝ g✝ f g : α →*o β
h : f.toMonoidHom = g.toMonoidHom
⊢ ∀ (a : α), ↑f a = ↑g a
[PROOFSTEP]
convert FunLike.ext_iff.1 h using 0
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : MulOneClass γ
inst✝ : MulOneClass δ
f✝ g✝ f g : α →*o β
h : toOrderHom f = toOrderHom g
⊢ ∀ (a : α), ↑f a = ↑g a
[PROOFSTEP]
convert FunLike.ext_iff.1 h using 0
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : MulOneClass γ
inst✝ : MulOneClass δ
f✝ g : α →*o β
g₁ g₂ : β →*o γ
f : α →*o β
hf : Surjective ↑f
x✝ : g₁ = g₂
⊢ comp g₁ f = comp g₂ f
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : MulOneClass γ
inst✝ : MulOneClass δ
f g✝ : α →*o β
g : β →*o γ
f₁ f₂ : α →*o β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulZeroOneClass α
inst✝² : MulZeroOneClass β
inst✝¹ : MulZeroOneClass γ
inst✝ : MulZeroOneClass δ
f✝ g✝ f g : α →*₀o β
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨⟨_, _⟩⟩, _⟩ := f
[GOAL]
case mk.mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulZeroOneClass α
inst✝² : MulZeroOneClass β
inst✝¹ : MulZeroOneClass γ
inst✝ : MulZeroOneClass δ
f g✝ g : α →*₀o β
toFun✝ : α → β
map_zero'✝ : toFun✝ 0 = 0
map_one'✝ : ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } 1 = 1
map_mul'✝ :
  ∀ (x y : α),
    ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } (x * y) =
      ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } x *
        ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } y
monotone'✝ :
  Monotone
    (↑{ toZeroHom := { toFun := toFun✝, map_zero' := map_zero'✝ }, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun
h :
  (fun f => f.toFun)
      {
        toMonoidWithZeroHom :=
          { toZeroHom := { toFun := toFun✝, map_zero' := map_zero'✝ }, map_one' := map_one'✝, map_mul' := map_mul'✝ },
        monotone' := monotone'✝ } =
    (fun f => f.toFun) g
⊢ {
      toMonoidWithZeroHom :=
        { toZeroHom := { toFun := toFun✝, map_zero' := map_zero'✝ }, map_one' := map_one'✝, map_mul' := map_mul'✝ },
      monotone' := monotone'✝ } =
    g
[PROOFSTEP]
obtain ⟨⟨⟨_, _⟩⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk.mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulZeroOneClass α
inst✝² : MulZeroOneClass β
inst✝¹ : MulZeroOneClass γ
inst✝ : MulZeroOneClass δ
f g : α →*₀o β
toFun✝¹ : α → β
map_zero'✝¹ : toFun✝¹ 0 = 0
map_one'✝¹ : ZeroHom.toFun { toFun := toFun✝¹, map_zero' := map_zero'✝¹ } 1 = 1
map_mul'✝¹ :
  ∀ (x y : α),
    ZeroHom.toFun { toFun := toFun✝¹, map_zero' := map_zero'✝¹ } (x * y) =
      ZeroHom.toFun { toFun := toFun✝¹, map_zero' := map_zero'✝¹ } x *
        ZeroHom.toFun { toFun := toFun✝¹, map_zero' := map_zero'✝¹ } y
monotone'✝¹ :
  Monotone
    (↑{ toZeroHom := { toFun := toFun✝¹, map_zero' := map_zero'✝¹ }, map_one' := map_one'✝¹,
          map_mul' := map_mul'✝¹ }).toFun
toFun✝ : α → β
map_zero'✝ : toFun✝ 0 = 0
map_one'✝ : ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } 1 = 1
map_mul'✝ :
  ∀ (x y : α),
    ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } (x * y) =
      ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } x *
        ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } y
monotone'✝ :
  Monotone
    (↑{ toZeroHom := { toFun := toFun✝, map_zero' := map_zero'✝ }, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun
h :
  (fun f => f.toFun)
      {
        toMonoidWithZeroHom :=
          { toZeroHom := { toFun := toFun✝¹, map_zero' := map_zero'✝¹ }, map_one' := map_one'✝¹,
            map_mul' := map_mul'✝¹ },
        monotone' := monotone'✝¹ } =
    (fun f => f.toFun)
      {
        toMonoidWithZeroHom :=
          { toZeroHom := { toFun := toFun✝, map_zero' := map_zero'✝ }, map_one' := map_one'✝, map_mul' := map_mul'✝ },
        monotone' := monotone'✝ }
⊢ {
      toMonoidWithZeroHom :=
        { toZeroHom := { toFun := toFun✝¹, map_zero' := map_zero'✝¹ }, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ },
      monotone' := monotone'✝¹ } =
    {
      toMonoidWithZeroHom :=
        { toZeroHom := { toFun := toFun✝, map_zero' := map_zero'✝ }, map_one' := map_one'✝, map_mul' := map_mul'✝ },
      monotone' := monotone'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulZeroOneClass α
inst✝² : MulZeroOneClass β
inst✝¹ : MulZeroOneClass γ
inst✝ : MulZeroOneClass δ
f✝ g✝ f g : α →*₀o β
h : toOrderMonoidHom f = toOrderMonoidHom g
⊢ ∀ (a : α), ↑f a = ↑g a
[PROOFSTEP]
convert FunLike.ext_iff.1 h using 0
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulZeroOneClass α
inst✝² : MulZeroOneClass β
inst✝¹ : MulZeroOneClass γ
inst✝ : MulZeroOneClass δ
f✝ g✝ f g : α →*₀o β
h : f.toMonoidWithZeroHom = g.toMonoidWithZeroHom
⊢ ∀ (a : α), ↑f a = ↑g a
[PROOFSTEP]
convert FunLike.ext_iff.1 h using 0
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulZeroOneClass α
inst✝² : MulZeroOneClass β
inst✝¹ : MulZeroOneClass γ
inst✝ : MulZeroOneClass δ
f✝ g : α →*₀o β
g₁ g₂ : β →*₀o γ
f : α →*₀o β
hf : Surjective ↑f
x✝ : g₁ = g₂
⊢ comp g₁ f = comp g₂ f
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulZeroOneClass α
inst✝² : MulZeroOneClass β
inst✝¹ : MulZeroOneClass γ
inst✝ : MulZeroOneClass δ
f g✝ : α →*₀o β
g : β →*₀o γ
f₁ f₂ : α →*₀o β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
hα : Preorder α
hα' : MulZeroOneClass α
hβ : Preorder β
hβ' : MulZeroOneClass β
f : α →*₀o β
⊢ f.toMonoidWithZeroHom = ↑f
[PROOFSTEP]
rfl
