case mk
α : Type u
α' : Type ?u.64625
β : Type v
β' : Type ?u.64630
γ : Type ?u.64633
φ : Type ?u.64636
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
g : α →𝒄 β
toOrderHom✝ : α →o β
cont✝ : ∀ {Monotone' : Monotone ↑toOrderHom✝}, Continuous { toFun := ↑toOrderHom✝, monotone' := Monotone' }
h : ∀ (x : α), ↑{ toOrderHom := toOrderHom✝, cont := cont✝ }.toOrderHom x = ↑g.toOrderHom x
⊢ { toOrderHom := toOrderHom✝, cont := cont✝ } = g
α : Type u
α' : Type ?u.64625
β : Type v
β' : Type ?u.64630
γ : Type ?u.64633
φ : Type ?u.64636
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
f g : α →𝒄 β
h : ∀ (x : α), ↑f.toOrderHom x = ↑g.toOrderHom x
⊢ f = g
cases f
case mk.mk
α : Type u
α' : Type ?u.64625
β : Type v
β' : Type ?u.64630
γ : Type ?u.64633
φ : Type ?u.64636
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
toOrderHom✝¹ : α →o β
cont✝¹ : ∀ {Monotone' : Monotone ↑toOrderHom✝¹}, Continuous { toFun := ↑toOrderHom✝¹, monotone' := Monotone' }
toOrderHom✝ : α →o β
cont✝ : ∀ {Monotone' : Monotone ↑toOrderHom✝}, Continuous { toFun := ↑toOrderHom✝, monotone' := Monotone' }
h :
  ∀ (x : α),
    ↑{ toOrderHom := toOrderHom✝¹, cont := cont✝¹ }.toOrderHom x =
      ↑{ toOrderHom := toOrderHom✝, cont := cont✝ }.toOrderHom x
⊢ { toOrderHom := toOrderHom✝¹, cont := cont✝¹ } = { toOrderHom := toOrderHom✝, cont := cont✝ }
case mk
α : Type u
α' : Type ?u.64625
β : Type v
β' : Type ?u.64630
γ : Type ?u.64633
φ : Type ?u.64636
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
g : α →𝒄 β
toOrderHom✝ : α →o β
cont✝ : ∀ {Monotone' : Monotone ↑toOrderHom✝}, Continuous { toFun := ↑toOrderHom✝, monotone' := Monotone' }
h : ∀ (x : α), ↑{ toOrderHom := toOrderHom✝, cont := cont✝ }.toOrderHom x = ↑g.toOrderHom x
⊢ { toOrderHom := toOrderHom✝, cont := cont✝ } = g
cases g
case mk.mk.e_toOrderHom
α : Type u
α' : Type ?u.64625
β : Type v
β' : Type ?u.64630
γ : Type ?u.64633
φ : Type ?u.64636
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
toOrderHom✝¹ : α →o β
cont✝¹ : ∀ {Monotone' : Monotone ↑toOrderHom✝¹}, Continuous { toFun := ↑toOrderHom✝¹, monotone' := Monotone' }
toOrderHom✝ : α →o β
cont✝ : ∀ {Monotone' : Monotone ↑toOrderHom✝}, Continuous { toFun := ↑toOrderHom✝, monotone' := Monotone' }
h :
  ∀ (x : α),
    ↑{ toOrderHom := toOrderHom✝¹, cont := cont✝¹ }.toOrderHom x =
      ↑{ toOrderHom := toOrderHom✝, cont := cont✝ }.toOrderHom x
⊢ toOrderHom✝¹ = toOrderHom✝
case mk.mk
α : Type u
α' : Type ?u.64625
β : Type v
β' : Type ?u.64630
γ : Type ?u.64633
φ : Type ?u.64636
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
toOrderHom✝¹ : α →o β
cont✝¹ : ∀ {Monotone' : Monotone ↑toOrderHom✝¹}, Continuous { toFun := ↑toOrderHom✝¹, monotone' := Monotone' }
toOrderHom✝ : α →o β
cont✝ : ∀ {Monotone' : Monotone ↑toOrderHom✝}, Continuous { toFun := ↑toOrderHom✝, monotone' := Monotone' }
h :
  ∀ (x : α),
    ↑{ toOrderHom := toOrderHom✝¹, cont := cont✝¹ }.toOrderHom x =
      ↑{ toOrderHom := toOrderHom✝, cont := cont✝ }.toOrderHom x
⊢ { toOrderHom := toOrderHom✝¹, cont := cont✝¹ } = { toOrderHom := toOrderHom✝, cont := cont✝ }
congr
case mk.mk.e_toOrderHom.h.h
α : Type u
α' : Type ?u.64625
β : Type v
β' : Type ?u.64630
γ : Type ?u.64633
φ : Type ?u.64636
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
toOrderHom✝¹ : α →o β
cont✝¹ : ∀ {Monotone' : Monotone ↑toOrderHom✝¹}, Continuous { toFun := ↑toOrderHom✝¹, monotone' := Monotone' }
toOrderHom✝ : α →o β
cont✝ : ∀ {Monotone' : Monotone ↑toOrderHom✝}, Continuous { toFun := ↑toOrderHom✝, monotone' := Monotone' }
h :
  ∀ (x : α),
    ↑{ toOrderHom := toOrderHom✝¹, cont := cont✝¹ }.toOrderHom x =
      ↑{ toOrderHom := toOrderHom✝, cont := cont✝ }.toOrderHom x
x✝ : α
⊢ ↑toOrderHom✝¹ x✝ = ↑toOrderHom✝ x✝
case mk.mk.e_toOrderHom
α : Type u
α' : Type ?u.64625
β : Type v
β' : Type ?u.64630
γ : Type ?u.64633
φ : Type ?u.64636
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
toOrderHom✝¹ : α →o β
cont✝¹ : ∀ {Monotone' : Monotone ↑toOrderHom✝¹}, Continuous { toFun := ↑toOrderHom✝¹, monotone' := Monotone' }
toOrderHom✝ : α →o β
cont✝ : ∀ {Monotone' : Monotone ↑toOrderHom✝}, Continuous { toFun := ↑toOrderHom✝, monotone' := Monotone' }
h :
  ∀ (x : α),
    ↑{ toOrderHom := toOrderHom✝¹, cont := cont✝¹ }.toOrderHom x =
      ↑{ toOrderHom := toOrderHom✝, cont := cont✝ }.toOrderHom x
⊢ toOrderHom✝¹ = toOrderHom✝
ext
no goals
case mk.mk.e_toOrderHom.h.h
α : Type u
α' : Type ?u.64625
β : Type v
β' : Type ?u.64630
γ : Type ?u.64633
φ : Type ?u.64636
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
toOrderHom✝¹ : α →o β
cont✝¹ : ∀ {Monotone' : Monotone ↑toOrderHom✝¹}, Continuous { toFun := ↑toOrderHom✝¹, monotone' := Monotone' }
toOrderHom✝ : α →o β
cont✝ : ∀ {Monotone' : Monotone ↑toOrderHom✝}, Continuous { toFun := ↑toOrderHom✝, monotone' := Monotone' }
h :
  ∀ (x : α),
    ↑{ toOrderHom := toOrderHom✝¹, cont := cont✝¹ }.toOrderHom x =
      ↑{ toOrderHom := toOrderHom✝, cont := cont✝ }.toOrderHom x
x✝ : α
⊢ ↑toOrderHom✝¹ x✝ = ↑toOrderHom✝ x✝
apply h