awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.Hom.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
inst_4 : TopologicalSpace γ
inst_5 : Preorder γ
inst_6 : TopologicalSpace δ
inst_7 : Preorder δ
toFun : α → β
monotone' : Monotone toFun
continuous_toFun : Continuous { toFun := toFun, monotone' := monotone' : α →o β }.toFun
toFun_1 : α → β
monotone'_1 : Monotone toFun_1
continuous_toFun_1 : Continuous { toFun := toFun_1, monotone' := monotone'_1 : α →o β }.toFun
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →Co β) ↦ f.toFun) { toFun := toFun, monotone' := monotone', continuous_toFun := continuous_toFun })
    ((fun (f : α →Co β) ↦ f.toFun)
      { toFun := toFun_1, monotone' := monotone'_1, continuous_toFun := continuous_toFun_1 })
⊢ { toFun := toFun, monotone' := monotone', continuous_toFun := continuous_toFun : α →Co β } =
    { toFun := toFun_1, monotone' := monotone'_1, continuous_toFun := continuous_toFun_1 }

Tactic:
congr
-- Module: Mathlib.Topology.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
f : α →Co β
⊢ Eq (α := (a : α) → β) (⇑f.toOrderHom : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
f : α →Co β
⊢ f.toFun = (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
f g : α →Co β
h : ∀ (a : α), Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) ((g : (a : α) → β) a : β)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- Module: Mathlib.Topology.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
f : α →Co β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ (⇑(f.copy f' h) : (a : α) → β) = f'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
f : α →Co β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ f.copy f' h = f

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Topology.Order.Hom.Basic
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : Preorder α
⊢ Eq (α := (a : α) → α) (⇑(ContinuousOrderHom.id α) : (a : α) → α) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.Hom.Basic
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : Preorder α
a : α
⊢ (ContinuousOrderHom.id α : (a : α) → α) a = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
inst_4 : TopologicalSpace γ
inst_5 : Preorder γ
f : β →Co γ
g : α →Co β
⊢ Eq (α := (a : α) → γ) (⇑(f.comp g) : (a : α) → γ)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
inst_4 : TopologicalSpace γ
inst_5 : Preorder γ
f : β →Co γ
g : α →Co β
a : α
⊢ Eq.{u_4 + 1} (α := γ) ((f.comp g : (a : α) → γ) a : γ) ((f : (a : β) → γ) ((g : (a : α) → β) a : β) : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
inst_4 : TopologicalSpace γ
inst_5 : Preorder γ
inst_6 : TopologicalSpace δ
inst_7 : Preorder δ
f : γ →Co δ
g : β →Co γ
h : α →Co β
⊢ (f.comp g).comp h = f.comp (g.comp h)

Tactic:
rfl

Premises used: OrderHom.comp, ContinuousOrderHom.comp, rfl
-- Module: Mathlib.Topology.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
f : α →Co β
⊢ f.comp (ContinuousOrderHom.id α) = f

Tactic:
ext fun _ => rfl

Premises used: ContinuousOrderHom.ext, rfl
-- Module: Mathlib.Topology.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
f : α →Co β
⊢ comp (ContinuousOrderHom.id β) f = f

Tactic:
ext fun _ => rfl

Premises used: ContinuousOrderHom.ext, rfl
-- Module: Mathlib.Topology.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
inst_4 : TopologicalSpace γ
inst_5 : Preorder γ
g₁ g₂ : β →Co γ
f : α →Co β
hf : Surjective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ g₁.comp f = g₂.comp f ↔ g₁ = g₂

Tactic:
⟨fun h => ext <| hf.forall.2 <| DFunLike.ext_iff.1 h, fun h => congr_arg₂ _ h rfl⟩

Premises used: ContinuousOrderHom.ext, Iff.mpr, Function.Surjective.forall, ContinuousOrderHom.comp, DFunLike.ext_iff, Iff.intro, Iff.mp, rfl, congr_arg₂
-- Module: Mathlib.Topology.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
inst_4 : TopologicalSpace γ
inst_5 : Preorder γ
g : β →Co γ
f₁ f₂ : α →Co β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
a : α
rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
rw₂ rw₃ :
  Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)

Tactic:
rw [← comp_apply, h, comp_apply]

Premises used: ContinuousOrderHom.comp_apply
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : PartialOrder α
inst_2 : OrderTop α
inst_3 : Preorder β
inst_4 : OrderTop β
inst_5 : PseudoEpimorphismClass F α β
f : F
let :
  ∀ (b : α) (h : ⊤ ≤ b ∧ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) b : β) (⊤ : β)),
    Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ : β) (⊤ : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ : β) (⊤ : β)

Tactic:
let ⟨b, h⟩ := exists_map_eq_of_map_le f (@le_top _ _ _ <| f ⊤)
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : PartialOrder α
inst_2 : OrderTop α
inst_3 : Preorder β
inst_4 : OrderTop β
inst_5 : PseudoEpimorphismClass F α β
f : F
b : α
h : ⊤ ≤ b ∧ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) b : β) (⊤ : β)
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) b : β) (⊤ : β)
rw₁ rw₂ : Eq.{u_3 + 1} (α := β) ⊤ ⊤
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ : β) (⊤ : β)

Tactic:
rw [← top_le_iff.1 h.1, h.2]

Premises used: And.right, And.left, top_le_iff, Iff.mp
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : TopologicalSpace α
inst_2 : Preorder α
inst_3 : TopologicalSpace β
inst_4 : Preorder β
inst_5 : EsakiaHomClass F α β
⊢ PseudoEpimorphismClass F α β

Tactic:
{ ‹EsakiaHomClass F α β› with
    map_rel := ContinuousOrderHomClass.map_monotone }

Premises used: EsakiaHomClass.exists_map_eq_of_map_le, PseudoEpimorphismClass.mk
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : Preorder δ
f g : PseudoEpimorphism α β
h :
  Eq (α := (a : α) → β) ((fun (f : PseudoEpimorphism α β) ↦ f.toFun) f) ((fun (f : PseudoEpimorphism α β) ↦ f.toFun) g)
obtain :
  ∀ (toFun : α → β) (monotone' : Monotone toFun)
    (exists_map_eq_of_map_le' :
      ∀ ⦃a : α⦄ ⦃b : β⦄,
        { toFun := toFun, monotone' := monotone' : α →o β }.toFun a ≤ b →
          ∃ (c : α), a ≤ c ∧ { toFun := toFun, monotone' := monotone' : α →o β }.toFun c = b)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : PseudoEpimorphism α β) ↦ f.toFun)
          { toFun := toFun, monotone' := monotone', exists_map_eq_of_map_le' := exists_map_eq_of_map_le' })
        ((fun (f : PseudoEpimorphism α β) ↦ f.toFun) g)),
    { toFun := toFun, monotone' := monotone', exists_map_eq_of_map_le' := exists_map_eq_of_map_le' :
        PseudoEpimorphism α β } =
      g
⊢ f = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := f
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : Preorder δ
g : PseudoEpimorphism α β
toFun : α → β
monotone' : Monotone toFun
exists_map_eq_of_map_le' :
  ∀ ⦃a : α⦄ ⦃b : β⦄,
    { toFun := toFun, monotone' := monotone' : α →o β }.toFun a ≤ b →
      ∃ (c : α), a ≤ c ∧ { toFun := toFun, monotone' := monotone' : α →o β }.toFun c = b
h :
  Eq (α := (a : α) → β)
    ((fun (f : PseudoEpimorphism α β) ↦ f.toFun)
      { toFun := toFun, monotone' := monotone', exists_map_eq_of_map_le' := exists_map_eq_of_map_le' })
    ((fun (f : PseudoEpimorphism α β) ↦ f.toFun) g)
obtain :
  ∀ (toFun_1 : α → β) (monotone'_1 : Monotone toFun_1)
    (exists_map_eq_of_map_le'_1 :
      ∀ ⦃a : α⦄ ⦃b : β⦄,
        { toFun := toFun_1, monotone' := monotone'_1 : α →o β }.toFun a ≤ b →
          ∃ (c : α), a ≤ c ∧ { toFun := toFun_1, monotone' := monotone'_1 : α →o β }.toFun c = b)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : PseudoEpimorphism α β) ↦ f.toFun)
          { toFun := toFun, monotone' := monotone', exists_map_eq_of_map_le' := exists_map_eq_of_map_le' })
        ((fun (f : PseudoEpimorphism α β) ↦ f.toFun)
          { toFun := toFun_1, monotone' := monotone'_1, exists_map_eq_of_map_le' := exists_map_eq_of_map_le'_1 })),
    { toFun := toFun, monotone' := monotone', exists_map_eq_of_map_le' := exists_map_eq_of_map_le' :
        PseudoEpimorphism α β } =
      { toFun := toFun_1, monotone' := monotone'_1, exists_map_eq_of_map_le' := exists_map_eq_of_map_le'_1 }
⊢ { toFun := toFun, monotone' := monotone', exists_map_eq_of_map_le' := exists_map_eq_of_map_le' :
      PseudoEpimorphism α β } =
    g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := g
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : Preorder δ
toFun : α → β
monotone' : Monotone toFun
exists_map_eq_of_map_le' :
  ∀ ⦃a : α⦄ ⦃b : β⦄,
    { toFun := toFun, monotone' := monotone' : α →o β }.toFun a ≤ b →
      ∃ (c : α), a ≤ c ∧ { toFun := toFun, monotone' := monotone' : α →o β }.toFun c = b
toFun_1 : α → β
monotone'_1 : Monotone toFun_1
exists_map_eq_of_map_le'_1 :
  ∀ ⦃a : α⦄ ⦃b : β⦄,
    { toFun := toFun_1, monotone' := monotone'_1 : α →o β }.toFun a ≤ b →
      ∃ (c : α), a ≤ c ∧ { toFun := toFun_1, monotone' := monotone'_1 : α →o β }.toFun c = b
h :
  Eq (α := (a : α) → β)
    ((fun (f : PseudoEpimorphism α β) ↦ f.toFun)
      { toFun := toFun, monotone' := monotone', exists_map_eq_of_map_le' := exists_map_eq_of_map_le' })
    ((fun (f : PseudoEpimorphism α β) ↦ f.toFun)
      { toFun := toFun_1, monotone' := monotone'_1, exists_map_eq_of_map_le' := exists_map_eq_of_map_le'_1 })
⊢ { toFun := toFun, monotone' := monotone', exists_map_eq_of_map_le' := exists_map_eq_of_map_le' :
      PseudoEpimorphism α β } =
    { toFun := toFun_1, monotone' := monotone'_1, exists_map_eq_of_map_le' := exists_map_eq_of_map_le'_1 }

Tactic:
congr
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f : PseudoEpimorphism α β
⊢ Eq (α := (a : α) → β) (⇑f.toOrderHom : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f : PseudoEpimorphism α β
⊢ f.toFun = (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f g : PseudoEpimorphism α β
h : ∀ (a : α), Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) ((g : (a : α) → β) a : β)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : Preorder δ
f : PseudoEpimorphism α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ ∀ ⦃a : α⦄ ⦃b : β⦄, (f.copy f' h).toFun a ≤ b → ∃ (c : α), a ≤ c ∧ (f.copy f' h).toFun c = b

Tactic:
simpa only [h.symm, toFun_eq_coe] using f.exists_map_eq_of_map_le'

Premises used: PseudoEpimorphism.toFun_eq_coe, PseudoEpimorphism.exists_map_eq_of_map_le', Eq.symm
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f : PseudoEpimorphism α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ (⇑(f.copy f' h) : (a : α) → β) = f'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f : PseudoEpimorphism α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ f.copy f' h = f

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
α : Type u_2
inst : Preorder α
⊢ Eq (α := (a : α) → α) (⇑(PseudoEpimorphism.id α) : (a : α) → α) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
α : Type u_2
inst : Preorder α
⊢ Eq (α := α →o α) (↑(PseudoEpimorphism.id α) : α →o α) OrderHom.id

Tactic:
rfl

Premises used: OrderHom.id, OrderHomClass.toOrderHom, rfl
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
α : Type u_2
inst : Preorder α
a : α
⊢ (PseudoEpimorphism.id α : (a : α) → α) a = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : Preorder δ
g : PseudoEpimorphism β γ
f : PseudoEpimorphism α β
a : α
b : γ
h₀ : (g.comp f.toOrderHom).toFun a ≤ b
obtain :
  ∀ (b : β) (h₁ : (f.toOrderHom : (a : α) → β) a ≤ b) (h₀ : (g.comp f.toOrderHom).toFun a ≤ g.toFun b),
    ∃ (c : α), a ≤ c ∧ (g.comp f.toOrderHom).toFun c = g.toFun b
⊢ ∃ (c : α), a ≤ c ∧ (g.comp f.toOrderHom).toFun c = b

Tactic:
obtain ⟨b, h₁, rfl⟩ := g.exists_map_eq_of_map_le' h₀

Premises used: PseudoEpimorphism.exists_map_eq_of_map_le', rfl
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : Preorder δ
g : PseudoEpimorphism β γ
f : PseudoEpimorphism α β
a : α
b : β
h₁ : (f.toOrderHom : (a : α) → β) a ≤ b
h₀ : (g.comp f.toOrderHom).toFun a ≤ g.toFun b
obtain :
  ∀ (b : α) (h₂ : a ≤ b) (h₁ : (f.toOrderHom : (a : α) → β) a ≤ f.toFun b)
    (h₀ : (g.comp f.toOrderHom).toFun a ≤ g.toFun (f.toFun b)),
    ∃ (c : α), a ≤ c ∧ (g.comp f.toOrderHom).toFun c = g.toFun (f.toFun b)
⊢ ∃ (c : α), a ≤ c ∧ (g.comp f.toOrderHom).toFun c = g.toFun b

Tactic:
obtain ⟨b, h₂, rfl⟩ := f.exists_map_eq_of_map_le' h₁

Premises used: PseudoEpimorphism.exists_map_eq_of_map_le', rfl
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : Preorder δ
g : PseudoEpimorphism β γ
f : PseudoEpimorphism α β
a b : α
h₂ : a ≤ b
h₁ : (f.toOrderHom : (a : α) → β) a ≤ f.toFun b
h₀ : (g.comp f.toOrderHom).toFun a ≤ g.toFun (f.toFun b)
⊢ ∃ (c : α), a ≤ c ∧ (g.comp f.toOrderHom).toFun c = g.toFun (f.toFun b)

Tactic:
⟨b, h₂, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : Preorder δ
g : PseudoEpimorphism β γ
f : PseudoEpimorphism α β
a b : α
h₂ : a ≤ b
h₁ : (f.toOrderHom : (a : α) → β) a ≤ f.toFun b
h₀ : (g.comp f.toOrderHom).toFun a ≤ g.toFun (f.toFun b)
⊢ ∃ (c : α), a ≤ c ∧ (g.comp f.toOrderHom).toFun c = g.toFun (f.toFun b)

Tactic:
exact ⟨b, h₂, rfl⟩
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : PseudoEpimorphism β γ
f : PseudoEpimorphism α β
⊢ Eq (α := (a : α) → γ) (⇑(g.comp f) : (a : α) → γ)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : PseudoEpimorphism β γ
f : PseudoEpimorphism α β
⊢ Eq (α := α →o γ) (↑(g.comp f) : α →o γ) (OrderHom.comp (↑g : β →o γ) (↑f : α →o β))

Tactic:
rfl

Premises used: OrderHom.comp, OrderHomClass.toOrderHom, rfl
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : PseudoEpimorphism β γ
f : PseudoEpimorphism α β
a : α
⊢ Eq.{u_4 + 1} (α := γ) ((g.comp f : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f : (a : α) → β) a : β) : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : Preorder δ
h : PseudoEpimorphism γ δ
g : PseudoEpimorphism β γ
f : PseudoEpimorphism α β
⊢ (h.comp g).comp f = h.comp (g.comp f)

Tactic:
rfl

Premises used: PseudoEpimorphism.comp, OrderHom.comp, rfl
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f : PseudoEpimorphism α β
⊢ f.comp (PseudoEpimorphism.id α) = f

Tactic:
ext fun _ => rfl

Premises used: PseudoEpimorphism.ext, rfl
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f : PseudoEpimorphism α β
⊢ comp (PseudoEpimorphism.id β) f = f

Tactic:
ext fun _ => rfl

Premises used: PseudoEpimorphism.ext, rfl
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g₁ g₂ : PseudoEpimorphism β γ
f : PseudoEpimorphism α β
hf : Surjective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ g₁.comp f = g₂.comp f ↔ g₁ = g₂

Tactic:
⟨fun h => ext <| hf.forall.2 <| DFunLike.ext_iff.1 h, congr_arg (comp · f)⟩

Premises used: Iff.mpr, Function.Surjective.forall, PseudoEpimorphism.comp, PseudoEpimorphism.ext, DFunLike.ext_iff, congr_arg, Iff.intro, Iff.mp
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : PseudoEpimorphism β γ
f₁ f₂ : PseudoEpimorphism α β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
a : α
rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
rw₂ rw₃ :
  Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)

Tactic:
rw [← comp_apply, h, comp_apply]

Premises used: PseudoEpimorphism.comp_apply
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
inst_4 : TopologicalSpace γ
inst_5 : Preorder γ
inst_6 : TopologicalSpace δ
inst_7 : Preorder δ
f g : EsakiaHom α β
h : Eq (α := (a : α) → β) ((fun (f : EsakiaHom α β) ↦ f.toFun) f) ((fun (f : EsakiaHom α β) ↦ f.toFun) g)
obtain :
  ∀ (toFun : α → β) (monotone' : Monotone toFun)
    (continuous_toFun : Continuous { toFun := toFun, monotone' := monotone' : α →o β }.toFun)
    (exists_map_eq_of_map_le' :
      ∀ ⦃a : α⦄ ⦃b : β⦄,
        { toFun := toFun, monotone' := monotone', continuous_toFun := continuous_toFun : α →Co β }.toFun a ≤ b →
          ∃ (c : α),
            a ≤ c ∧
              { toFun := toFun, monotone' := monotone', continuous_toFun := continuous_toFun : α →Co β }.toFun c = b)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : EsakiaHom α β) ↦ f.toFun)
          { toFun := toFun, monotone' := monotone', continuous_toFun := continuous_toFun,
            exists_map_eq_of_map_le' := exists_map_eq_of_map_le' })
        ((fun (f : EsakiaHom α β) ↦ f.toFun) g)),
    { toFun := toFun, monotone' := monotone', continuous_toFun := continuous_toFun,
        exists_map_eq_of_map_le' := exists_map_eq_of_map_le' : EsakiaHom α β } =
      g
⊢ f = g

Tactic:
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f
-- Module: Mathlib.Topology.Order.Hom.Esakia
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
inst_4 : TopologicalSpace γ
inst_5 : Preorder γ
inst_6 : TopologicalSpace δ
inst_7 : Preorder δ
g : EsakiaHom α β
toFun : α → β
monotone' : Monotone toFun
continuous_toFun : Continuous { toFun := toFun, monotone' := monotone' : α →o β }.toFun
exists_map_eq_of_map_le' :
  ∀ ⦃a : α⦄ ⦃b : β⦄,
    { toFun := toFun, monotone' := monotone', continuous_toFun := continuous_toFun : α →Co β }.toFun a ≤ b →
      ∃ (c : α),
        a ≤ c ∧ { toFun := toFun, monotone' := monotone', continuous_toFun := continuous_toFun : α →Co β }.toFun c = b
h :
  Eq (α := (a : α) → β)
    ((fun (f : EsakiaHom α β) ↦ f.toFun)
      { toFun := toFun, monotone' := monotone', continuous_toFun := continuous_toFun,
        exists_map_eq_of_map_le' := exists_map_eq_of_map_le' })
    ((fun (f : EsakiaHom α β) ↦ f.toFun) g)
obtain :
  ∀ (toFun_1 : α → β) (monotone'_1 : Monotone toFun_1)
    (continuous_toFun_1 : Continuous { toFun := toFun_1, monotone' := monotone'_1 : α →o β }.toFun)
    (exists_map_eq_of_map_le'_1 :
      ∀ ⦃a : α⦄ ⦃b : β⦄,
        { toFun := toFun_1, monotone' := monotone'_1, continuous_toFun := continuous_toFun_1 : α →Co β }.toFun a ≤ b →
          ∃ (c : α),
            a ≤ c ∧
              { toFun := toFun_1, monotone' := monotone'_1, continuous_toFun := continuous_toFun_1 : α →Co β }.toFun c =
                b)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : EsakiaHom α β) ↦ f.toFun)
          { toFun := toFun, monotone' := monotone', continuous_toFun := continuous_toFun,
            exists_map_eq_of_map_le' := exists_map_eq_of_map_le' })
        ((fun (f : EsakiaHom α β) ↦ f.toFun)
          { toFun := toFun_1, monotone' := monotone'_1, continuous_toFun := continuous_toFun_1,
            exists_map_eq_of_map_le' := exists_map_eq_of_map_le'_1 })),
    { toFun := toFun, monotone' := monotone', continuous_toFun := continuous_toFun,
        exists_map_eq_of_map_le' := exists_map_eq_of_map_le' : EsakiaHom α β } =
      { toFun := toFun_1, monotone' := monotone'_1, continuous_toFun := continuous_toFun_1,
        exists_map_eq_of_map_le' := exists_map_eq_of_map_le'_1 }
⊢ { toFun := toFun, monotone' := monotone', continuous_toFun := continuous_toFun,
      exists_map_eq_of_map_le' := exists_map_eq_of_map_le' : EsakiaHom α β } =
    g

Tactic:
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g