[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : PartialOrder α
inst✝³ : OrderTop α
inst✝² : Preorder β
inst✝¹ : OrderTop β
inst✝ : PseudoEpimorphismClass F α β
f : F
⊢ ↑f ⊤ = ⊤
[PROOFSTEP]
let ⟨b, h⟩ := exists_map_eq_of_map_le f (@le_top _ _ _ <| f ⊤)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : PartialOrder α
inst✝³ : OrderTop α
inst✝² : Preorder β
inst✝¹ : OrderTop β
inst✝ : PseudoEpimorphismClass F α β
f : F
b : α
h : ⊤ ≤ b ∧ ↑f b = ⊤
⊢ ↑f ⊤ = ⊤
[PROOFSTEP]
rw [← top_le_iff.1 h.1, h.2]
[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 δ
f g : PseudoEpimorphism α β
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✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
g : PseudoEpimorphism α β
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
exists_map_eq_of_map_le'✝ :
  ∀ ⦃a : α⦄ ⦃b : β⦄,
    OrderHom.toFun { toFun := toFun✝, monotone' := monotone'✝ } a ≤ b →
      ∃ c, a ≤ c ∧ OrderHom.toFun { toFun := toFun✝, monotone' := monotone'✝ } c = b
h :
  (fun f => f.toFun)
      { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ },
        exists_map_eq_of_map_le' := exists_map_eq_of_map_le'✝ } =
    (fun f => f.toFun) g
⊢ { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ },
      exists_map_eq_of_map_le' := exists_map_eq_of_map_le'✝ } =
    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✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
toFun✝¹ : α → β
monotone'✝¹ : Monotone toFun✝¹
exists_map_eq_of_map_le'✝¹ :
  ∀ ⦃a : α⦄ ⦃b : β⦄,
    OrderHom.toFun { toFun := toFun✝¹, monotone' := monotone'✝¹ } a ≤ b →
      ∃ c, a ≤ c ∧ OrderHom.toFun { toFun := toFun✝¹, monotone' := monotone'✝¹ } c = b
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
exists_map_eq_of_map_le'✝ :
  ∀ ⦃a : α⦄ ⦃b : β⦄,
    OrderHom.toFun { toFun := toFun✝, monotone' := monotone'✝ } a ≤ b →
      ∃ c, a ≤ c ∧ OrderHom.toFun { toFun := toFun✝, monotone' := monotone'✝ } c = b
h :
  (fun f => f.toFun)
      { toOrderHom := { toFun := toFun✝¹, monotone' := monotone'✝¹ },
        exists_map_eq_of_map_le' := exists_map_eq_of_map_le'✝¹ } =
    (fun f => f.toFun)
      { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ },
        exists_map_eq_of_map_le' := exists_map_eq_of_map_le'✝ }
⊢ { toOrderHom := { toFun := toFun✝¹, monotone' := monotone'✝¹ },
      exists_map_eq_of_map_le' := exists_map_eq_of_map_le'✝¹ } =
    { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ },
      exists_map_eq_of_map_le' := exists_map_eq_of_map_le'✝ }
[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 δ
f : PseudoEpimorphism α β
f' : α → β
h : f' = ↑f
⊢ ∀ ⦃a : α⦄ ⦃b : β⦄,
    OrderHom.toFun (OrderHom.copy f.toOrderHom f' h) a ≤ b →
      ∃ c, a ≤ c ∧ OrderHom.toFun (OrderHom.copy f.toOrderHom f' h) c = b
[PROOFSTEP]
simpa only [h.symm, toFun_eq_coe] using f.exists_map_eq_of_map_le'
[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 δ
g : PseudoEpimorphism β γ
f : PseudoEpimorphism α β
a : α
b : γ
h₀ : OrderHom.toFun (OrderHom.comp g.toOrderHom f.toOrderHom) a ≤ b
⊢ ∃ c, a ≤ c ∧ OrderHom.toFun (OrderHom.comp g.toOrderHom f.toOrderHom) c = b
[PROOFSTEP]
obtain ⟨b, h₁, rfl⟩ := g.exists_map_eq_of_map_le' h₀
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
g : PseudoEpimorphism β γ
f : PseudoEpimorphism α β
a : α
b : β
h₁ : ↑f.toOrderHom a ≤ b
h₀ : OrderHom.toFun (OrderHom.comp g.toOrderHom f.toOrderHom) a ≤ OrderHom.toFun g.toOrderHom b
⊢ ∃ c, a ≤ c ∧ OrderHom.toFun (OrderHom.comp g.toOrderHom f.toOrderHom) c = OrderHom.toFun g.toOrderHom b
[PROOFSTEP]
obtain ⟨b, h₂, rfl⟩ := f.exists_map_eq_of_map_le' h₁
[GOAL]
case intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
g : PseudoEpimorphism β γ
f : PseudoEpimorphism α β
a b : α
h₂ : a ≤ b
h₁ : ↑f.toOrderHom a ≤ OrderHom.toFun f.toOrderHom b
h₀ :
  OrderHom.toFun (OrderHom.comp g.toOrderHom f.toOrderHom) a ≤
    OrderHom.toFun g.toOrderHom (OrderHom.toFun f.toOrderHom b)
⊢ ∃ c,
    a ≤ c ∧
      OrderHom.toFun (OrderHom.comp g.toOrderHom f.toOrderHom) c =
        OrderHom.toFun g.toOrderHom (OrderHom.toFun f.toOrderHom b)
[PROOFSTEP]
exact ⟨b, h₂, 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 δ
g : PseudoEpimorphism β γ
f₁ f₂ : PseudoEpimorphism α β
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✝⁷ : TopologicalSpace α
inst✝⁶ : Preorder α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace γ
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace δ
inst✝ : Preorder δ
f g : EsakiaHom α β
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✝⁷ : TopologicalSpace α
inst✝⁶ : Preorder α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace γ
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace δ
inst✝ : Preorder δ
g : EsakiaHom α β
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
continuous_toFun✝ : Continuous { toFun := toFun✝, monotone' := monotone'✝ }.toFun
exists_map_eq_of_map_le'✝ :
  ∀ ⦃a : α⦄ ⦃b : β⦄,
    OrderHom.toFun
          { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ },
              continuous_toFun := continuous_toFun✝ }.toOrderHom
          a ≤
        b →
      ∃ c,
        a ≤ c ∧
          OrderHom.toFun
              { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ },
                  continuous_toFun := continuous_toFun✝ }.toOrderHom
              c =
            b
h :
  (fun f => f.toFun)
      {
        toContinuousOrderHom :=
          { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ }, continuous_toFun := continuous_toFun✝ },
        exists_map_eq_of_map_le' := exists_map_eq_of_map_le'✝ } =
    (fun f => f.toFun) g
⊢ {
      toContinuousOrderHom :=
        { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ }, continuous_toFun := continuous_toFun✝ },
      exists_map_eq_of_map_le' := exists_map_eq_of_map_le'✝ } =
    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✝⁷ : TopologicalSpace α
inst✝⁶ : Preorder α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace γ
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace δ
inst✝ : Preorder δ
toFun✝¹ : α → β
monotone'✝¹ : Monotone toFun✝¹
continuous_toFun✝¹ : Continuous { toFun := toFun✝¹, monotone' := monotone'✝¹ }.toFun
exists_map_eq_of_map_le'✝¹ :
  ∀ ⦃a : α⦄ ⦃b : β⦄,
    OrderHom.toFun
          { toOrderHom := { toFun := toFun✝¹, monotone' := monotone'✝¹ },
              continuous_toFun := continuous_toFun✝¹ }.toOrderHom
          a ≤
        b →
      ∃ c,
        a ≤ c ∧
          OrderHom.toFun
              { toOrderHom := { toFun := toFun✝¹, monotone' := monotone'✝¹ },
                  continuous_toFun := continuous_toFun✝¹ }.toOrderHom
              c =
            b
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
continuous_toFun✝ : Continuous { toFun := toFun✝, monotone' := monotone'✝ }.toFun
exists_map_eq_of_map_le'✝ :
  ∀ ⦃a : α⦄ ⦃b : β⦄,
    OrderHom.toFun
          { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ },
              continuous_toFun := continuous_toFun✝ }.toOrderHom
          a ≤
        b →
      ∃ c,
        a ≤ c ∧
          OrderHom.toFun
              { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ },
                  continuous_toFun := continuous_toFun✝ }.toOrderHom
              c =
            b
h :
  (fun f => f.toFun)
      {
        toContinuousOrderHom :=
          { toOrderHom := { toFun := toFun✝¹, monotone' := monotone'✝¹ }, continuous_toFun := continuous_toFun✝¹ },
        exists_map_eq_of_map_le' := exists_map_eq_of_map_le'✝¹ } =
    (fun f => f.toFun)
      {
        toContinuousOrderHom :=
          { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ }, continuous_toFun := continuous_toFun✝ },
        exists_map_eq_of_map_le' := exists_map_eq_of_map_le'✝ }
⊢ {
      toContinuousOrderHom :=
        { toOrderHom := { toFun := toFun✝¹, monotone' := monotone'✝¹ }, continuous_toFun := continuous_toFun✝¹ },
      exists_map_eq_of_map_le' := exists_map_eq_of_map_le'✝¹ } =
    {
      toContinuousOrderHom :=
        { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ }, continuous_toFun := continuous_toFun✝ },
      exists_map_eq_of_map_le' := exists_map_eq_of_map_le'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : TopologicalSpace α
inst✝⁶ : Preorder α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace γ
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace δ
inst✝ : Preorder δ
f : EsakiaHom α β
f' : α → β
h : f' = ↑f
⊢ ∀ ⦃a : α⦄ ⦃b : β⦄,
    OrderHom.toFun (ContinuousOrderHom.copy f.toContinuousOrderHom f' h).toOrderHom a ≤ b →
      ∃ c, a ≤ c ∧ OrderHom.toFun (ContinuousOrderHom.copy f.toContinuousOrderHom f' h).toOrderHom c = b
[PROOFSTEP]
simpa only [h.symm, toFun_eq_coe] using f.exists_map_eq_of_map_le'
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : TopologicalSpace α
inst✝⁶ : Preorder α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace γ
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace δ
inst✝ : Preorder δ
g : EsakiaHom β γ
f : EsakiaHom α β
a : α
b : γ
h₀ : OrderHom.toFun (ContinuousOrderHom.comp g.toContinuousOrderHom f.toContinuousOrderHom).toOrderHom a ≤ b
⊢ ∃ c, a ≤ c ∧ OrderHom.toFun (ContinuousOrderHom.comp g.toContinuousOrderHom f.toContinuousOrderHom).toOrderHom c = b
[PROOFSTEP]
obtain ⟨b, h₁, rfl⟩ := g.exists_map_eq_of_map_le' h₀
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : TopologicalSpace α
inst✝⁶ : Preorder α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace γ
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace δ
inst✝ : Preorder δ
g : EsakiaHom β γ
f : EsakiaHom α β
a : α
b : β
h₁ : ↑f.toOrderHom a ≤ b
h₀ :
  OrderHom.toFun (ContinuousOrderHom.comp g.toContinuousOrderHom f.toContinuousOrderHom).toOrderHom a ≤
    OrderHom.toFun g.toOrderHom b
⊢ ∃ c,
    a ≤ c ∧
      OrderHom.toFun (ContinuousOrderHom.comp g.toContinuousOrderHom f.toContinuousOrderHom).toOrderHom c =
        OrderHom.toFun g.toOrderHom b
[PROOFSTEP]
obtain ⟨b, h₂, rfl⟩ := f.exists_map_eq_of_map_le' h₁
[GOAL]
case intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : TopologicalSpace α
inst✝⁶ : Preorder α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace γ
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace δ
inst✝ : Preorder δ
g : EsakiaHom β γ
f : EsakiaHom α β
a b : α
h₂ : a ≤ b
h₁ : ↑f.toOrderHom a ≤ OrderHom.toFun f.toOrderHom b
h₀ :
  OrderHom.toFun (ContinuousOrderHom.comp g.toContinuousOrderHom f.toContinuousOrderHom).toOrderHom a ≤
    OrderHom.toFun g.toOrderHom (OrderHom.toFun f.toOrderHom b)
⊢ ∃ c,
    a ≤ c ∧
      OrderHom.toFun (ContinuousOrderHom.comp g.toContinuousOrderHom f.toContinuousOrderHom).toOrderHom c =
        OrderHom.toFun g.toOrderHom (OrderHom.toFun f.toOrderHom b)
[PROOFSTEP]
exact ⟨b, h₂, rfl⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : TopologicalSpace α
inst✝⁶ : Preorder α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace γ
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace δ
inst✝ : Preorder δ
g : EsakiaHom β γ
f₁ f₂ : EsakiaHom α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]
