awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
s : Set α
inst_5 : SeparableSpace.{u_1} (↑s : Type u_1)
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
refine_1 : t \ ({x : α | IsBot x} ∪ {x : α | IsTop x}) ⊆ s
refine_2 : (t \ ({x : α | IsBot x} ∪ {x : α | IsTop x})).Countable
refine_3 : Dense (t \ ({x : α | IsBot x} ∪ {x : α | IsTop x}))
refine_4 : ∀ (x : α) (hx : IsBot x), x ∉ t \ ({x : α | IsBot x} ∪ {x : α | IsTop x})
⊢ ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∉ t) ∧ ∀ (x : α), IsTop x → x ∉ t
have refine_5 : ∀ (x : α) (hx : IsTop x), x ∉ t \ ({x : α | IsBot x} ∪ {x : α | IsTop x})
Tactic: refine ⟨t \ ({ x | IsBot x } ∪ { x | IsTop x }), ?_, ?_, ?_, fun x hx => ?_, fun x hx => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
⊢ IsClosed[inst] (Ico a b) ↔ b ≤ a
have refine : ∀ (h : IsClosed[inst] (Ico a b)) (hab : a < b), False
Tactic: refine ⟨fun h => le_of_not_gt fun hab => ?_, by simp_all⟩
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
h : IsClosed[inst] (Ico a b)
hab : a < b
⊢ False
have this : closure[inst] (Ico a b) = Ico a b
Tactic: have := h.closure_eq
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
h : IsClosed[inst] (Ico a b)
hab : a < b
this : closure[inst] (Ico a b) = Ico a b
⊢ False
have this₁ : ¬a ≤ b
Tactic: rw [closure_Ico hab.ne, Icc_eq_Ico_same_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
⊢ IsClosed[inst] (Ioc a b) ↔ b ≤ a
have refine : ∀ (h : IsClosed[inst] (Ioc a b)) (hab : a < b), False
Tactic: refine ⟨fun h => le_of_not_gt fun hab => ?_, by simp_all⟩
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
h : IsClosed[inst] (Ioc a b)
hab : a < b
⊢ False
have this : closure[inst] (Ioc a b) = Ioc a b
Tactic: have := h.closure_eq
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
h : IsClosed[inst] (Ioc a b)
hab : a < b
this : closure[inst] (Ioc a b) = Ioc a b
⊢ False
have this₁ : ¬a ≤ b
Tactic: rw [closure_Ioc hab.ne, Icc_eq_Ioc_same_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
⊢ IsClosed[inst] (Ioo a b) ↔ b ≤ a
have refine : ∀ (h : IsClosed[inst] (Ioo a b)) (hab : a < b), False
Tactic: refine ⟨fun h => le_of_not_gt fun hab => ?_, by simp_all⟩
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
h : IsClosed[inst] (Ioo a b)
hab : a < b
⊢ False
have this : closure[inst] (Ioo a b) = Ioo a b
Tactic: have := h.closure_eq
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
h : IsClosed[inst] (Ioo a b)
hab : a < b
this : closure[inst] (Ioo a b) = Ioo a b
⊢ False
have this₁ : ¬a ≤ b
Tactic: rw [closure_Ioo hab.ne, Icc_eq_Ioo_same_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Order.ExtrClosure (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Preorder Y
inst_3 : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure[inst] s)
⊢ IsLocalMaxOn f (closure[inst] s) a
have rcases : ∀ (U : Set X) (Uo : IsOpen[inst] U) (aU : a ∈ U) (hU : U ∩ s ⊆ {x : X | (fun (x : X) ↦ f x ≤ f a) x}),
  IsLocalMaxOn f (closure[inst] s) a
Tactic: rcases mem_nhdsWithin.1 h with ⟨U, Uo, aU, hU⟩
-- Lean 4 proof step from Mathlib.Topology.Order.ExtrClosure (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Preorder Y
inst_3 : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure[inst] s)
U : Set X
Uo : IsOpen[inst] U
aU : a ∈ U
hU : U ∩ s ⊆ {x : X | (fun (x : X) ↦ f x ≤ f a) x}
⊢ IsLocalMaxOn f (closure[inst] s) a
have refine : U ∩ closure[inst] s ⊆ {x : X | (fun (x : X) ↦ f x ≤ f a) x}
Tactic: refine mem_nhdsWithin.2 ⟨U, Uo, aU, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.ExtrClosure (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Preorder Y
inst_3 : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure[inst] s)
U : Set X
Uo : IsOpen[inst] U
aU : a ∈ U
hU : U ∩ s ⊆ {x : X | (fun (x : X) ↦ f x ≤ f a) x}
x : X
hxU : x ∈ U
hxs : x ∈ closure[inst] s
⊢ Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ f x ≤ f a) x} x
have refine_1 : x ∈ closure[inst] (U ∩ s)
Tactic: refine ContinuousWithinAt.closure_le ?_ ?_ continuousWithinAt_const hU
-- Lean 4 proof step from Mathlib.Topology.Order.ExtrClosure (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Preorder Y
inst_3 : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure[inst] s)
U : Set X
Uo : IsOpen[inst] U
aU : a ∈ U
hU : U ∩ s ⊆ {x : X | (fun (x : X) ↦ f x ≤ f a) x}
x : X
hxU : x ∈ U
hxs : x ∈ closure[inst] s
refine_1 : x ∈ closure[inst] (U ∩ s)
⊢ Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ f x ≤ f a) x} x
have refine_2 : ContinuousWithinAt f (U ∩ s) x
Tactic: refine ContinuousWithinAt.closure_le ?_ ?_ continuousWithinAt_const hU
-- Lean 4 proof step from Mathlib.Topology.Order.ExtrClosure (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Preorder Y
inst_3 : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure[inst] s)
U : Set X
Uo : IsOpen[inst] U
aU : a ∈ U
hU : U ∩ s ⊆ {x : X | (fun (x : X) ↦ f x ≤ f a) x}
x : X
hxU : x ∈ U
hxs : x ∈ closure[inst] s
⊢ x ∈ closure[inst] (U ∩ s)
have refine_1 : U ∈ 𝓝[s] x
Tactic: rwa [mem_closure_iff_nhdsWithin_neBot, nhdsWithin_inter_of_mem, ←
      mem_closure_iff_nhdsWithin_neBot]
-- Lean 4 proof step from Mathlib.Topology.Order.Hom.Basic (goal)
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 : α →Co β
h : Eq (α := (a : α) → β) ((fun (f : α →Co β) ↦ f.toFun) f) ((fun (f : α →Co β) ↦ f.toFun) g)
⊢ f = g
have obtain : ∀ (toFun : α → β) (monotone' : Monotone toFun)
  (continuous_toFun : Continuous { toFun := toFun, monotone' := monotone' : α →o β }.toFun)
  (h :
    Eq (α := (a : α) → β)
      ((fun (f : α →Co β) ↦ f.toFun) { toFun := toFun, monotone' := monotone', continuous_toFun := continuous_toFun })
      ((fun (f : α →Co β) ↦ f.toFun) g)),
  { toFun := toFun, monotone' := monotone', continuous_toFun := continuous_toFun : α →Co β } = g
Tactic: obtain ⟨⟨_, _⟩, _⟩ := f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Topology.Order.Hom.Basic (goal)
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 : α →Co β
toFun : α → β
monotone' : Monotone toFun
continuous_toFun : Continuous { toFun := toFun, monotone' := monotone' : α →o β }.toFun
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →Co β) ↦ f.toFun) { toFun := toFun, monotone' := monotone', continuous_toFun := continuous_toFun })
    ((fun (f : α →Co β) ↦ f.toFun) g)
⊢ { toFun := toFun, monotone' := monotone', continuous_toFun := continuous_toFun : α →Co β } = g
have obtain : ∀ (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: obtain ⟨⟨_, _⟩, _⟩ := g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Topology.Order.Hom.Basic (goal)
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 : α
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Topology.Order.Hom.Basic (goal)
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 : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Topology.Order.Hom.Basic (goal)
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 : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw₂ : Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
  ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Topology.Order.Hom.Esakia (goal)
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
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ : β) (⊤ : β)
have let : ∀ (b : α) (h : ⊤ ≤ b ∧ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) b : β) (⊤ : β)),
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ : β) (⊤ : β)
Tactic: let ⟨b, h⟩ := exists_map_eq_of_map_le f (@le_top _ _ _ <| f ⊤)
-- Lean 4 proof step from Mathlib.Topology.Order.Hom.Esakia (goal)
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 : β) (⊤ : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ : β) (⊤ : β)
have rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) b : β) (⊤ : β)
Tactic: rw [← top_le_iff.1 h.1, h.2]
-- Lean 4 proof step from Mathlib.Topology.Order.Hom.Esakia (goal)
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 : β) (⊤ : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ : β) (⊤ : β)
have rw₁ : Eq.{u_3 + 1} (α := β) ⊤ ⊤
Tactic: rw [← top_le_iff.1 h.1, h.2]
-- Lean 4 proof step from Mathlib.Topology.Order.Hom.Esakia (goal)
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)
⊢ f = g
have 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
Tactic: obtain ⟨⟨_, _⟩, _⟩ := f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Topology.Order.Hom.Esakia (goal)
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)
⊢ { toFun := toFun, monotone' := monotone', exists_map_eq_of_map_le' := exists_map_eq_of_map_le' :
      PseudoEpimorphism α β } =
    g
have 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 }
Tactic: obtain ⟨⟨_, _⟩, _⟩ := g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Topology.Order.Hom.Esakia (goal)
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
⊢ ∃ (c : α), a ≤ c ∧ (g.comp f.toOrderHom).toFun c = b
have 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
Tactic: obtain ⟨b, h₁, rfl⟩ := g.exists_map_eq_of_map_le' h₀
Cleared hypotheses: b, h₀
-- Lean 4 proof step from Mathlib.Topology.Order.Hom.Esakia (goal)
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
⊢ ∃ (c : α), a ≤ c ∧ (g.comp f.toOrderHom).toFun c = g.toFun b
have 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)
Tactic: obtain ⟨b, h₂, rfl⟩ := f.exists_map_eq_of_map_le' h₁
Cleared hypotheses: b, h₁, h₀
-- Lean 4 proof step from Mathlib.Topology.Order.Hom.Esakia (goal)
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 : α
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Topology.Order.Hom.Esakia (goal)
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 : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Topology.Order.Hom.Esakia (goal)
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 : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw₂ : Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
  ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Topology.Order.Hom.Esakia (goal)
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)
⊢ f = g
have 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
Tactic: obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Topology.Order.Hom.Esakia (goal)
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)
⊢ { toFun := toFun, monotone' := monotone', continuous_toFun := continuous_toFun,
      exists_map_eq_of_map_le' := exists_map_eq_of_map_le' : EsakiaHom α β } =
    g
have 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 }
Tactic: obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g
Cleared hypotheses: g, h