[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : Preorder α
inst✝⁵ : NonAssocSemiring β
inst✝⁴ : Preorder β
inst✝³ : NonAssocSemiring γ
inst✝² : Preorder γ
inst✝¹ : NonAssocSemiring δ
inst✝ : Preorder δ
f g : α →+*o β
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := f
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : Preorder α
inst✝⁵ : NonAssocSemiring β
inst✝⁴ : Preorder β
inst✝³ : NonAssocSemiring γ
inst✝² : Preorder γ
inst✝¹ : NonAssocSemiring δ
inst✝ : Preorder δ
g : α →+*o β
toMonoidHom✝ : α →* β
map_zero'✝ : OneHom.toFun (↑toMonoidHom✝) 0 = 0
map_add'✝ :
  ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝) (x + y) = OneHom.toFun (↑toMonoidHom✝) x + OneHom.toFun (↑toMonoidHom✝) y
monotone'✝ : Monotone (↑↑{ toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }).toFun
h :
  (fun f => f.toFun)
      { toRingHom := { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ },
        monotone' := monotone'✝ } =
    (fun f => f.toFun) g
⊢ { toRingHom := { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ },
      monotone' := monotone'✝ } =
    g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : Preorder α
inst✝⁵ : NonAssocSemiring β
inst✝⁴ : Preorder β
inst✝³ : NonAssocSemiring γ
inst✝² : Preorder γ
inst✝¹ : NonAssocSemiring δ
inst✝ : Preorder δ
toMonoidHom✝¹ : α →* β
map_zero'✝¹ : OneHom.toFun (↑toMonoidHom✝¹) 0 = 0
map_add'✝¹ :
  ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝¹) (x + y) = OneHom.toFun (↑toMonoidHom✝¹) x + OneHom.toFun (↑toMonoidHom✝¹) y
monotone'✝¹ : Monotone (↑↑{ toMonoidHom := toMonoidHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }).toFun
toMonoidHom✝ : α →* β
map_zero'✝ : OneHom.toFun (↑toMonoidHom✝) 0 = 0
map_add'✝ :
  ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝) (x + y) = OneHom.toFun (↑toMonoidHom✝) x + OneHom.toFun (↑toMonoidHom✝) y
monotone'✝ : Monotone (↑↑{ toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }).toFun
h :
  (fun f => f.toFun)
      { toRingHom := { toMonoidHom := toMonoidHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ },
        monotone' := monotone'✝¹ } =
    (fun f => f.toFun)
      { toRingHom := { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ },
        monotone' := monotone'✝ }
⊢ { toRingHom := { toMonoidHom := toMonoidHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ },
      monotone' := monotone'✝¹ } =
    { toRingHom := { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ },
      monotone' := monotone'✝ }
[PROOFSTEP]
congr
  -- porting note: needed to add the following line
[GOAL]
case mk.mk.mk.mk.e_toRingHom.e_toMonoidHom
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : Preorder α
inst✝⁵ : NonAssocSemiring β
inst✝⁴ : Preorder β
inst✝³ : NonAssocSemiring γ
inst✝² : Preorder γ
inst✝¹ : NonAssocSemiring δ
inst✝ : Preorder δ
toMonoidHom✝¹ : α →* β
map_zero'✝¹ : OneHom.toFun (↑toMonoidHom✝¹) 0 = 0
map_add'✝¹ :
  ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝¹) (x + y) = OneHom.toFun (↑toMonoidHom✝¹) x + OneHom.toFun (↑toMonoidHom✝¹) y
monotone'✝¹ : Monotone (↑↑{ toMonoidHom := toMonoidHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }).toFun
toMonoidHom✝ : α →* β
map_zero'✝ : OneHom.toFun (↑toMonoidHom✝) 0 = 0
map_add'✝ :
  ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝) (x + y) = OneHom.toFun (↑toMonoidHom✝) x + OneHom.toFun (↑toMonoidHom✝) y
monotone'✝ : Monotone (↑↑{ toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }).toFun
h :
  (fun f => f.toFun)
      { toRingHom := { toMonoidHom := toMonoidHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ },
        monotone' := monotone'✝¹ } =
    (fun f => f.toFun)
      { toRingHom := { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ },
        monotone' := monotone'✝ }
⊢ toMonoidHom✝¹ = toMonoidHom✝
[PROOFSTEP]
exact MonoidHom.monoidHomClass.coe_injective' h
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : Preorder α
inst✝⁵ : NonAssocSemiring β
inst✝⁴ : Preorder β
inst✝³ : NonAssocSemiring γ
inst✝² : Preorder γ
inst✝¹ : NonAssocSemiring δ
inst✝ : Preorder δ
f₁ f₂ : β →+*o γ
g : α →+*o β
hg : Surjective ↑g
h : f₁ = f₂
⊢ OrderRingHom.comp f₁ g = OrderRingHom.comp f₂ g
[PROOFSTEP]
rw [h]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : Preorder α
inst✝⁵ : NonAssocSemiring β
inst✝⁴ : Preorder β
inst✝³ : NonAssocSemiring γ
inst✝² : Preorder γ
inst✝¹ : NonAssocSemiring δ
inst✝ : Preorder δ
f : β →+*o γ
g₁ g₂ : α →+*o β
hf : Injective ↑f
h : OrderRingHom.comp f g₁ = OrderRingHom.comp f g₂
a : α
⊢ ↑f (↑g₁ a) = ↑f (↑g₂ 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✝¹¹ : Mul α
inst✝¹⁰ : Add α
inst✝⁹ : LE α
inst✝⁸ : Mul β
inst✝⁷ : Add β
inst✝⁶ : LE β
inst✝⁵ : Mul γ
inst✝⁴ : Add γ
inst✝³ : LE γ
inst✝² : Mul δ
inst✝¹ : Add δ
inst✝ : LE δ
f g : α ≃+*o β
h₁ : (fun f => f.toFun) f = (fun f => f.toFun) g
h₂ : (fun f => f.invFun) f = (fun f => f.invFun) 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✝¹¹ : Mul α
inst✝¹⁰ : Add α
inst✝⁹ : LE α
inst✝⁸ : Mul β
inst✝⁷ : Add β
inst✝⁶ : LE β
inst✝⁵ : Mul γ
inst✝⁴ : Add γ
inst✝³ : LE γ
inst✝² : Mul δ
inst✝¹ : Add δ
inst✝ : LE δ
g : α ≃+*o β
toFun✝ : α → β
invFun✝ : β → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : Function.RightInverse invFun✝ toFun✝
map_mul'✝ :
  ∀ (x y : α),
    Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x * y) =
      Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x *
        Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
map_add'✝ :
  ∀ (x y : α),
    Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x + y) =
      Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x +
        Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
map_le_map_iff'✝ :
  ∀ {a b : α},
    Equiv.toFun
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
              map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
          a ≤
        Equiv.toFun
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
              map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
          b ↔
      a ≤ b
h₁ :
  (fun f => f.toFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
            map_mul' := map_mul'✝, map_add' := map_add'✝ },
        map_le_map_iff' := map_le_map_iff'✝ } =
    (fun f => f.toFun) g
h₂ :
  (fun f => f.invFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
            map_mul' := map_mul'✝, map_add' := map_add'✝ },
        map_le_map_iff' := map_le_map_iff'✝ } =
    (fun f => f.invFun) g
⊢ {
      toRingEquiv :=
        { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
          map_mul' := map_mul'✝, map_add' := map_add'✝ },
      map_le_map_iff' := map_le_map_iff'✝ } =
    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✝¹¹ : Mul α
inst✝¹⁰ : Add α
inst✝⁹ : LE α
inst✝⁸ : Mul β
inst✝⁷ : Add β
inst✝⁶ : LE β
inst✝⁵ : Mul γ
inst✝⁴ : Add γ
inst✝³ : LE γ
inst✝² : Mul δ
inst✝¹ : Add δ
inst✝ : LE δ
toFun✝¹ : α → β
invFun✝¹ : β → α
left_inv✝¹ : LeftInverse invFun✝¹ toFun✝¹
right_inv✝¹ : Function.RightInverse invFun✝¹ toFun✝¹
map_mul'✝¹ :
  ∀ (x y : α),
    Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } (x * y) =
      Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } x *
        Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } y
map_add'✝¹ :
  ∀ (x y : α),
    Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } (x + y) =
      Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } x +
        Equiv.toFun { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } y
map_le_map_iff'✝¹ :
  ∀ {a b : α},
    Equiv.toFun
          { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
              map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }.toEquiv
          a ≤
        Equiv.toFun
          { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
              map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }.toEquiv
          b ↔
      a ≤ b
toFun✝ : α → β
invFun✝ : β → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : Function.RightInverse invFun✝ toFun✝
map_mul'✝ :
  ∀ (x y : α),
    Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x * y) =
      Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x *
        Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
map_add'✝ :
  ∀ (x y : α),
    Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } (x + y) =
      Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x +
        Equiv.toFun { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } y
map_le_map_iff'✝ :
  ∀ {a b : α},
    Equiv.toFun
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
              map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
          a ≤
        Equiv.toFun
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
              map_mul' := map_mul'✝, map_add' := map_add'✝ }.toEquiv
          b ↔
      a ≤ b
h₁ :
  (fun f => f.toFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
            map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ },
        map_le_map_iff' := map_le_map_iff'✝¹ } =
    (fun f => f.toFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
            map_mul' := map_mul'✝, map_add' := map_add'✝ },
        map_le_map_iff' := map_le_map_iff'✝ }
h₂ :
  (fun f => f.invFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
            map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ },
        map_le_map_iff' := map_le_map_iff'✝¹ } =
    (fun f => f.invFun)
      {
        toRingEquiv :=
          { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
            map_mul' := map_mul'✝, map_add' := map_add'✝ },
        map_le_map_iff' := map_le_map_iff'✝ }
⊢ {
      toRingEquiv :=
        { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
          map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ },
      map_le_map_iff' := map_le_map_iff'✝¹ } =
    {
      toRingEquiv :=
        { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
          map_mul' := map_mul'✝, map_add' := map_add'✝ },
      map_le_map_iff' := map_le_map_iff'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹¹ : Mul α
inst✝¹⁰ : Add α
inst✝⁹ : LE α
inst✝⁸ : Mul β
inst✝⁷ : Add β
inst✝⁶ : LE β
inst✝⁵ : Mul γ
inst✝⁴ : Add γ
inst✝³ : LE γ
inst✝² : Mul δ
inst✝¹ : Add δ
inst✝ : LE δ
x : α
⊢ ↑(OrderRingIso.refl α) x = x
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹¹ : Mul α
inst✝¹⁰ : Add α
inst✝⁹ : LE α
inst✝⁸ : Mul β
inst✝⁷ : Add β
inst✝⁶ : LE β
inst✝⁵ : Mul γ
inst✝⁴ : Add γ
inst✝³ : LE γ
inst✝² : Mul δ
inst✝¹ : Add δ
inst✝ : LE δ
e : α ≃+*o β
⊢ ∀ {a b : β},
    Equiv.toFun (RingEquiv.symm e.toRingEquiv).toEquiv a ≤ Equiv.toFun (RingEquiv.symm e.toRingEquiv).toEquiv b ↔ a ≤ b
[PROOFSTEP]
intro a b
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹¹ : Mul α
inst✝¹⁰ : Add α
inst✝⁹ : LE α
inst✝⁸ : Mul β
inst✝⁷ : Add β
inst✝⁶ : LE β
inst✝⁵ : Mul γ
inst✝⁴ : Add γ
inst✝³ : LE γ
inst✝² : Mul δ
inst✝¹ : Add δ
inst✝ : LE δ
e : α ≃+*o β
a b : β
⊢ Equiv.toFun (RingEquiv.symm e.toRingEquiv).toEquiv a ≤ Equiv.toFun (RingEquiv.symm e.toRingEquiv).toEquiv b ↔ a ≤ b
[PROOFSTEP]
erw [← map_le_map_iff e, e.1.apply_symm_apply, e.1.apply_symm_apply]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁵ : NonAssocSemiring α
inst✝⁴ : Preorder α
inst✝³ : NonAssocSemiring β
inst✝² : Preorder β
inst✝¹ : NonAssocSemiring γ
inst✝ : Preorder γ
f g : α ≃+*o β
h : toOrderRingHom f = toOrderRingHom g
⊢ (fun f => ↑f) f = (fun f => ↑f) g
[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✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean β
f g : α →+*o β
⊢ f = g
[PROOFSTEP]
ext x
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean β
f g : α →+*o β
x : α
⊢ ↑f x = ↑g x
[PROOFSTEP]
by_contra' h' : f x ≠ g x
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean β
f g : α →+*o β
x : α
h' : ↑f x ≠ ↑g x
⊢ False
[PROOFSTEP]
wlog h : f x < g x generalizing α β with h₂
[GOAL]
case h.inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean β
f g : α →+*o β
x : α
h' : ↑f x ≠ ↑g x
h₂ :
  ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrderedField α] [inst_1 : LinearOrderedField β] [inst_2 : Archimedean β]
    (f g : α →+*o β) (x : α), ↑f x ≠ ↑g x → ↑f x < ↑g x → False
h : ¬↑f x < ↑g x
⊢ False
[PROOFSTEP]
exact h₂ g f x (Ne.symm h') (h'.lt_or_lt.resolve_left h)
[GOAL]
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean β
f g : α →+*o β
x : α
h' : ↑f x ≠ ↑g x
h : ↑f x < ↑g x
⊢ False
[PROOFSTEP]
obtain ⟨q, hf, hg⟩ := exists_rat_btwn h
[GOAL]
case intro.intro
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean β
f g : α →+*o β
x : α
h' : ↑f x ≠ ↑g x
h : ↑f x < ↑g x
q : ℚ
hf : ↑f x < ↑q
hg : ↑q < ↑g x
⊢ False
[PROOFSTEP]
rw [← map_ratCast f] at hf 
[GOAL]
case intro.intro
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean β
f g : α →+*o β
x : α
h' : ↑f x ≠ ↑g x
h : ↑f x < ↑g x
q : ℚ
hf : ↑f x < ↑f ↑q
hg : ↑q < ↑g x
⊢ False
[PROOFSTEP]
rw [← map_ratCast g] at hg 
[GOAL]
case intro.intro
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean β
f g : α →+*o β
x : α
h' : ↑f x ≠ ↑g x
h : ↑f x < ↑g x
q : ℚ
hf : ↑f x < ↑f ↑q
hg : ↑g ↑q < ↑g x
⊢ False
[PROOFSTEP]
exact (lt_asymm ((OrderHomClass.mono g).reflect_lt hg) <| (OrderHomClass.mono f).reflect_lt hf).elim
