ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_3<VAR>Sup α<VAR>Bot α<GOAL>(SupBotHom.id α).toSupHom = SupHom.id α
<VAR>α : Type u_3<VAR>Sup α<VAR>Bot α<GOAL>⇑(SupBotHom.id α) = id
<VAR>α : Type u_3<VAR>Sup α<VAR>Bot α<VAR>a : α<GOAL>(SupBotHom.id α) a = a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Sup α<VAR>Bot α<VAR>Sup β<VAR>Bot β<VAR>Sup γ<VAR>Bot γ<VAR>f : SupBotHom β γ<VAR>g : SupBotHom α β<GOAL>⇑(f.comp g) = ⇑f ∘ ⇑g
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Sup α<VAR>Bot α<VAR>Sup β<VAR>Bot β<VAR>Sup γ<VAR>Bot γ<VAR>f : SupBotHom β γ<VAR>g : SupBotHom α β<VAR>a : α<GOAL>(f.comp g) a = f (g a)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>Sup α<VAR>Bot α<VAR>Sup β<VAR>Bot β<VAR>Sup γ<VAR>Bot γ<VAR>Sup δ<VAR>Bot δ<VAR>f : SupBotHom γ δ<VAR>g : SupBotHom β γ<VAR>h : SupBotHom α β<GOAL>(f.comp g).comp h = f.comp (g.comp h)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Sup α<VAR>Bot α<VAR>Sup β<VAR>Bot β<VAR>f : SupBotHom α β<GOAL>f.comp (SupBotHom.id α) = f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Sup α<VAR>Bot α<VAR>Sup β<VAR>Bot β<VAR>f : SupBotHom α β<GOAL>(SupBotHom.id β).comp f = f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Sup α<VAR>Bot α<VAR>Sup β<VAR>Bot β<VAR>Sup γ<VAR>Bot γ<VAR>g₁ g₂ : SupBotHom β γ<VAR>f : SupBotHom α β<VAR>hf : Function.Surjective ⇑f<GOAL>g₁.comp f = g₂.comp f ↔ g₁ = g₂
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Sup α<VAR>Bot α<VAR>Sup β<VAR>Bot β<VAR>Sup γ<VAR>Bot γ<VAR>g : SupBotHom β γ<VAR>f₁ f₂ : SupBotHom α β<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Sup α<VAR>Bot α<VAR>SemilatticeSup β<VAR>OrderBot β<VAR>f g : SupBotHom α β<GOAL>⇑(f ⊔ g) = ⇑(f ⊔ g)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Sup α<VAR>Bot α<VAR>SemilatticeSup β<VAR>OrderBot β<GOAL>⇑⊥ = ⊥
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Sup α<VAR>Bot α<VAR>SemilatticeSup β<VAR>OrderBot β<VAR>f g : SupBotHom α β<VAR>a : α<GOAL>(f ⊔ g) a = f a ⊔ g a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Sup α<VAR>Bot α<VAR>SemilatticeSup β<VAR>OrderBot β<VAR>a : α<GOAL>⊥ a = ⊥
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Inf α<VAR>Top α<VAR>Inf β<VAR>Top β<VAR>f : InfTopHom α β<GOAL>f.toFun = ⇑f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Inf α<VAR>Top α<VAR>Inf β<VAR>Top β<VAR>f : InfTopHom α β<GOAL>⇑f.toInfHom = ⇑f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Inf α<VAR>Top α<VAR>Inf β<VAR>Top β<VAR>f : InfTopHom α β<GOAL>⇑f.toTopHom = ⇑f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Inf α<VAR>Top α<VAR>Inf β<VAR>Top β<VAR>f : InfHom α β<VAR>hf : f.toFun ⊤ = ⊤<GOAL>⇑{ toInfHom := f, map_top' := hf } = ⇑f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Inf α<VAR>Top α<VAR>Inf β<VAR>Top β<VAR>f g : InfTopHom α β<VAR>h : ∀ (a : α), f a = g a<GOAL>f = g
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Inf α<VAR>Top α<VAR>Inf β<VAR>Top β<VAR>f : InfTopHom α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Inf α<VAR>Top α<VAR>Inf β<VAR>Top β<VAR>f : InfTopHom α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>α : Type u_3<VAR>Inf α<VAR>Top α<GOAL>(InfTopHom.id α).toInfHom = InfHom.id α
<VAR>α : Type u_3<VAR>Inf α<VAR>Top α<GOAL>⇑(InfTopHom.id α) = id
<VAR>α : Type u_3<VAR>Inf α<VAR>Top α<VAR>a : α<GOAL>(InfTopHom.id α) a = a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Inf α<VAR>Top α<VAR>Inf β<VAR>Top β<VAR>Inf γ<VAR>Top γ<VAR>f : InfTopHom β γ<VAR>g : InfTopHom α β<GOAL>⇑(f.comp g) = ⇑f ∘ ⇑g
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Inf α<VAR>Top α<VAR>Inf β<VAR>Top β<VAR>Inf γ<VAR>Top γ<VAR>f : InfTopHom β γ<VAR>g : InfTopHom α β<VAR>a : α<GOAL>(f.comp g) a = f (g a)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>Inf α<VAR>Top α<VAR>Inf β<VAR>Top β<VAR>Inf γ<VAR>Top γ<VAR>Inf δ<VAR>Top δ<VAR>f : InfTopHom γ δ<VAR>g : InfTopHom β γ<VAR>h : InfTopHom α β<GOAL>(f.comp g).comp h = f.comp (g.comp h)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Inf α<VAR>Top α<VAR>Inf β<VAR>Top β<VAR>f : InfTopHom α β<GOAL>f.comp (InfTopHom.id α) = f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Inf α<VAR>Top α<VAR>Inf β<VAR>Top β<VAR>f : InfTopHom α β<GOAL>(InfTopHom.id β).comp f = f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Inf α<VAR>Top α<VAR>Inf β<VAR>Top β<VAR>Inf γ<VAR>Top γ<VAR>g₁ g₂ : InfTopHom β γ<VAR>f : InfTopHom α β<VAR>hf : Function.Surjective ⇑f<GOAL>g₁.comp f = g₂.comp f ↔ g₁ = g₂
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Inf α<VAR>Top α<VAR>Inf β<VAR>Top β<VAR>Inf γ<VAR>Top γ<VAR>g : InfTopHom β γ<VAR>f₁ f₂ : InfTopHom α β<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Inf α<VAR>Top α<VAR>SemilatticeInf β<VAR>OrderTop β<VAR>f g : InfTopHom α β<GOAL>⇑(f ⊓ g) = ⇑(f ⊓ g)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Inf α<VAR>Top α<VAR>SemilatticeInf β<VAR>OrderTop β<GOAL>⇑⊤ = ⊤
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Inf α<VAR>Top α<VAR>SemilatticeInf β<VAR>OrderTop β<VAR>f g : InfTopHom α β<VAR>a : α<GOAL>(f ⊓ g) a = f a ⊓ g a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Inf α<VAR>Top α<VAR>SemilatticeInf β<VAR>OrderTop β<VAR>a : α<GOAL>⊤ a = ⊤
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>f : LatticeHom α β<GOAL>f.toFun = ⇑f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>f : LatticeHom α β<GOAL>⇑f.toSupHom = ⇑f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>f : LatticeHom α β<GOAL>⇑f.toInfHom = ⇑f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>f : SupHom α β<VAR>hf : ∀ (a b : α), f.toFun (a ⊓ b) = f.toFun a ⊓ f.toFun b<GOAL>⇑{ toSupHom := f, map_inf' := hf } = ⇑f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>f g : LatticeHom α β<VAR>h : ∀ (a : α), f a = g a<GOAL>f = g
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>f : LatticeHom α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>f : LatticeHom α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>α : Type u_3<VAR>Lattice α<GOAL>⇑(LatticeHom.id α) = id
<VAR>α : Type u_3<VAR>Lattice α<VAR>a : α<GOAL>(LatticeHom.id α) a = a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Lattice α<VAR>Lattice β<VAR>Lattice γ<VAR>f : LatticeHom β γ<VAR>g : LatticeHom α β<GOAL>⇑(f.comp g) = ⇑f ∘ ⇑g
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Lattice α<VAR>Lattice β<VAR>Lattice γ<VAR>f : LatticeHom β γ<VAR>g : LatticeHom α β<VAR>a : α<GOAL>(f.comp g) a = f (g a)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Lattice α<VAR>Lattice β<VAR>Lattice γ<VAR>f : LatticeHom β γ<VAR>g : LatticeHom α β<GOAL>{ toFun := ⇑f ∘ ⇑g, map_sup' := ⋯ } = { toFun := ⇑f, map_sup' := ⋯ }.comp { toFun := ⇑g, map_sup' := ⋯ }
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Lattice α<VAR>Lattice β<VAR>Lattice γ<VAR>f : LatticeHom β γ<VAR>g : LatticeHom α β<GOAL>{ toFun := ⇑(f.comp g), map_sup' := ⋯ } = { toFun := ⇑f, map_sup' := ⋯ }.comp { toFun := ⇑g, map_sup' := ⋯ }
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Lattice α<VAR>Lattice β<VAR>Lattice γ<VAR>f : LatticeHom β γ<VAR>g : LatticeHom α β<GOAL>{ toFun := ⇑f ∘ ⇑g, map_inf' := ⋯ } = { toFun := ⇑f, map_inf' := ⋯ }.comp { toFun := ⇑g, map_inf' := ⋯ }
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Lattice α<VAR>Lattice β<VAR>Lattice γ<VAR>f : LatticeHom β γ<VAR>g : LatticeHom α β<GOAL>{ toFun := ⇑(f.comp g), map_inf' := ⋯ } = { toFun := ⇑f, map_inf' := ⋯ }.comp { toFun := ⇑g, map_inf' := ⋯ }
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>Lattice α<VAR>Lattice β<VAR>Lattice γ<VAR>Lattice δ<VAR>f : LatticeHom γ δ<VAR>g : LatticeHom β γ<VAR>h : LatticeHom α β<GOAL>(f.comp g).comp h = f.comp (g.comp h)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>f : LatticeHom α β<GOAL>f.comp (LatticeHom.id α) = f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>f : LatticeHom α β<GOAL>(LatticeHom.id β).comp f = f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Lattice α<VAR>Lattice β<VAR>Lattice γ<VAR>g₁ g₂ : LatticeHom β γ<VAR>f : LatticeHom α β<VAR>hf : Function.Surjective ⇑f<GOAL>g₁.comp f = g₂.comp f ↔ g₁ = g₂
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Lattice α<VAR>Lattice β<VAR>Lattice γ<VAR>g : LatticeHom β γ<VAR>f₁ f₂ : LatticeHom α β<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>F : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrder α<VAR>Lattice β<VAR>FunLike F α β<VAR>OrderHomClass F α β<VAR>f : F<GOAL>⇑(OrderHomClass.toLatticeHom α β f) = ⇑f
<VAR>F : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrder α<VAR>Lattice β<VAR>FunLike F α β<VAR>OrderHomClass F α β<VAR>f : F<VAR>a : α<GOAL>(OrderHomClass.toLatticeHom α β f) a = f a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>f : BoundedLatticeHom α β<GOAL>f.toFun = ⇑f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>f : BoundedLatticeHom α β<GOAL>⇑f.toLatticeHom = ⇑f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>f : BoundedLatticeHom α β<GOAL>⇑f.toSupBotHom = ⇑f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>f : BoundedLatticeHom α β<GOAL>⇑f.toInfTopHom = ⇑f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>f : BoundedLatticeHom α β<GOAL>⇑f.toBoundedOrderHom = ⇑f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>f : LatticeHom α β<VAR>hf : f.toFun ⊤ = ⊤<VAR>hf' : f.toFun ⊥ = ⊥<GOAL>⇑{ toLatticeHom := f, map_top' := hf, map_bot' := hf' } = ⇑f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>f g : BoundedLatticeHom α β<VAR>h : ∀ (a : α), f a = g a<GOAL>f = g
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>f : BoundedLatticeHom α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>f : BoundedLatticeHom α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>α : Type u_3<VAR>Lattice α<VAR>BoundedOrder α<GOAL>⇑(BoundedLatticeHom.id α) = id
<VAR>α : Type u_3<VAR>Lattice α<VAR>BoundedOrder α<VAR>a : α<GOAL>(BoundedLatticeHom.id α) a = a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Lattice α<VAR>Lattice β<VAR>Lattice γ<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>BoundedOrder γ<VAR>f : BoundedLatticeHom β γ<VAR>g : BoundedLatticeHom α β<GOAL>⇑(f.comp g) = ⇑f ∘ ⇑g
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Lattice α<VAR>Lattice β<VAR>Lattice γ<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>BoundedOrder γ<VAR>f : BoundedLatticeHom β γ<VAR>g : BoundedLatticeHom α β<VAR>a : α<GOAL>(f.comp g) a = f (g a)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Lattice α<VAR>Lattice β<VAR>Lattice γ<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>BoundedOrder γ<VAR>f : BoundedLatticeHom β γ<VAR>g : BoundedLatticeHom α β<GOAL>{ toSupHom := { toFun := ⇑f, map_sup' := ⋯ }.comp { toFun := ⇑g, map_sup' := ⋯ }, map_inf' := ⋯ } = { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯ }.comp { toFun := ⇑g, map_sup' := ⋯, map_inf' := ⋯ }
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Lattice α<VAR>Lattice β<VAR>Lattice γ<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>BoundedOrder γ<VAR>f : BoundedLatticeHom β γ<VAR>g : BoundedLatticeHom α β<GOAL>{ toFun := ⇑(f.comp g), map_sup' := ⋯, map_inf' := ⋯ } = { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯ }.comp { toFun := ⇑g, map_sup' := ⋯, map_inf' := ⋯ }
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Lattice α<VAR>Lattice β<VAR>Lattice γ<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>BoundedOrder γ<VAR>f : BoundedLatticeHom β γ<VAR>g : BoundedLatticeHom α β<GOAL>{ toFun := ⇑f ∘ ⇑g, map_sup' := ⋯ } = { toFun := ⇑f, map_sup' := ⋯ }.comp { toFun := ⇑g, map_sup' := ⋯ }
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Lattice α<VAR>Lattice β<VAR>Lattice γ<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>BoundedOrder γ<VAR>f : BoundedLatticeHom β γ<VAR>g : BoundedLatticeHom α β<GOAL>{ toFun := ⇑(f.comp g), map_sup' := ⋯ } = { toFun := ⇑f, map_sup' := ⋯ }.comp { toFun := ⇑g, map_sup' := ⋯ }
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Lattice α<VAR>Lattice β<VAR>Lattice γ<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>BoundedOrder γ<VAR>f : BoundedLatticeHom β γ<VAR>g : BoundedLatticeHom α β<GOAL>{ toFun := ⇑f ∘ ⇑g, map_inf' := ⋯ } = { toFun := ⇑f, map_inf' := ⋯ }.comp { toFun := ⇑g, map_inf' := ⋯ }
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Lattice α<VAR>Lattice β<VAR>Lattice γ<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>BoundedOrder γ<VAR>f : BoundedLatticeHom β γ<VAR>g : BoundedLatticeHom α β<GOAL>{ toFun := ⇑(f.comp g), map_inf' := ⋯ } = { toFun := ⇑f, map_inf' := ⋯ }.comp { toFun := ⇑g, map_inf' := ⋯ }
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>Lattice α<VAR>Lattice β<VAR>Lattice γ<VAR>Lattice δ<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>BoundedOrder γ<VAR>BoundedOrder δ<VAR>f : BoundedLatticeHom γ δ<VAR>g : BoundedLatticeHom β γ<VAR>h : BoundedLatticeHom α β<GOAL>(f.comp g).comp h = f.comp (g.comp h)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>f : BoundedLatticeHom α β<GOAL>f.comp (BoundedLatticeHom.id α) = f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>f : BoundedLatticeHom α β<GOAL>(BoundedLatticeHom.id β).comp f = f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Lattice α<VAR>Lattice β<VAR>Lattice γ<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>BoundedOrder γ<VAR>g₁ g₂ : BoundedLatticeHom β γ<VAR>f : BoundedLatticeHom α β<VAR>hf : Function.Surjective ⇑f<GOAL>g₁.comp f = g₂.comp f ↔ g₁ = g₂
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Lattice α<VAR>Lattice β<VAR>Lattice γ<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>BoundedOrder γ<VAR>g : BoundedLatticeHom β γ<VAR>f₁ f₂ : BoundedLatticeHom α β<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Sup α<VAR>Sup β<VAR>f : SupHom α β<VAR>a : α<GOAL>(SupHom.dual f) a = f a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Sup α<VAR>Sup β<VAR>f : InfHom αᵒᵈ βᵒᵈ<VAR>a : αᵒᵈ<GOAL>(SupHom.dual.symm f) a = f a
<VAR>α : Type u_3<VAR>Sup α<GOAL>SupHom.dual (SupHom.id α) = InfHom.id αᵒᵈ
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Sup α<VAR>Sup β<VAR>Sup γ<VAR>g : SupHom β γ<VAR>f : SupHom α β<GOAL>SupHom.dual (g.comp f) = (SupHom.dual g).comp (SupHom.dual f)
<VAR>α : Type u_3<VAR>Sup α<GOAL>SupHom.dual.symm (InfHom.id αᵒᵈ) = SupHom.id α
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Sup α<VAR>Sup β<VAR>Sup γ<VAR>g : InfHom βᵒᵈ γᵒᵈ<VAR>f : InfHom αᵒᵈ βᵒᵈ<GOAL>SupHom.dual.symm (g.comp f) = (SupHom.dual.symm g).comp (SupHom.dual.symm f)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Inf α<VAR>Inf β<VAR>f : SupHom αᵒᵈ βᵒᵈ<VAR>a : αᵒᵈ<GOAL>(InfHom.dual.symm f) a = f a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Inf α<VAR>Inf β<VAR>f : InfHom α β<VAR>a : α<GOAL>(InfHom.dual f) a = f a
<VAR>α : Type u_3<VAR>Inf α<GOAL>InfHom.dual (InfHom.id α) = SupHom.id αᵒᵈ
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Inf α<VAR>Inf β<VAR>Inf γ<VAR>g : InfHom β γ<VAR>f : InfHom α β<GOAL>InfHom.dual (g.comp f) = (InfHom.dual g).comp (InfHom.dual f)
<VAR>α : Type u_3<VAR>Inf α<GOAL>InfHom.dual.symm (SupHom.id αᵒᵈ) = InfHom.id α
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Inf α<VAR>Inf β<VAR>Inf γ<VAR>g : SupHom βᵒᵈ γᵒᵈ<VAR>f : SupHom αᵒᵈ βᵒᵈ<GOAL>InfHom.dual.symm (g.comp f) = (InfHom.dual.symm g).comp (InfHom.dual.symm f)
<VAR>α : Type u_3<VAR>Sup α<VAR>Bot α<GOAL>SupBotHom.dual (SupBotHom.id α) = InfTopHom.id αᵒᵈ
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Sup α<VAR>Bot α<VAR>Sup β<VAR>Bot β<VAR>Sup γ<VAR>Bot γ<VAR>g : SupBotHom β γ<VAR>f : SupBotHom α β<GOAL>SupBotHom.dual (g.comp f) = (SupBotHom.dual g).comp (SupBotHom.dual f)
<VAR>α : Type u_3<VAR>Sup α<VAR>Bot α<GOAL>SupBotHom.dual.symm (InfTopHom.id αᵒᵈ) = SupBotHom.id α
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Sup α<VAR>Bot α<VAR>Sup β<VAR>Bot β<VAR>Sup γ<VAR>Bot γ<VAR>g : InfTopHom βᵒᵈ γᵒᵈ<VAR>f : InfTopHom αᵒᵈ βᵒᵈ<GOAL>SupBotHom.dual.symm (g.comp f) = (SupBotHom.dual.symm g).comp (SupBotHom.dual.symm f)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Inf α<VAR>Top α<VAR>Inf β<VAR>Top β<VAR>f : SupBotHom αᵒᵈ βᵒᵈ<GOAL>(InfTopHom.dual.symm f).toInfHom = InfHom.dual.symm f.toSupHom
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Inf α<VAR>Top α<VAR>Inf β<VAR>Top β<VAR>f : InfTopHom α β<GOAL>(InfTopHom.dual f).toSupHom = InfHom.dual f.toInfHom
<VAR>α : Type u_3<VAR>Inf α<VAR>Top α<GOAL>InfTopHom.dual (InfTopHom.id α) = SupBotHom.id αᵒᵈ
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Inf α<VAR>Top α<VAR>Inf β<VAR>Top β<VAR>Inf γ<VAR>Top γ<VAR>g : InfTopHom β γ<VAR>f : InfTopHom α β<GOAL>InfTopHom.dual (g.comp f) = (InfTopHom.dual g).comp (InfTopHom.dual f)
<VAR>α : Type u_3<VAR>Inf α<VAR>Top α<GOAL>InfTopHom.dual.symm (SupBotHom.id αᵒᵈ) = InfTopHom.id α
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Inf α<VAR>Top α<VAR>Inf β<VAR>Top β<VAR>Inf γ<VAR>Top γ<VAR>g : SupBotHom βᵒᵈ γᵒᵈ<VAR>f : SupBotHom αᵒᵈ βᵒᵈ<GOAL>InfTopHom.dual.symm (g.comp f) = (InfTopHom.dual.symm g).comp (InfTopHom.dual.symm f)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>f : LatticeHom α β<GOAL>(LatticeHom.dual f).toSupHom = InfHom.dual f.toInfHom
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>f : LatticeHom αᵒᵈ βᵒᵈ<GOAL>(LatticeHom.dual.symm f).toSupHom = SupHom.dual.symm f.toInfHom
<VAR>α : Type u_3<VAR>Lattice α<GOAL>LatticeHom.dual (LatticeHom.id α) = LatticeHom.id αᵒᵈ
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Lattice α<VAR>Lattice β<VAR>Lattice γ<VAR>g : LatticeHom β γ<VAR>f : LatticeHom α β<GOAL>LatticeHom.dual (g.comp f) = (LatticeHom.dual g).comp (LatticeHom.dual f)
<VAR>α : Type u_3<VAR>Lattice α<GOAL>LatticeHom.dual.symm (LatticeHom.id αᵒᵈ) = LatticeHom.id α
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Lattice α<VAR>Lattice β<VAR>Lattice γ<VAR>g : LatticeHom βᵒᵈ γᵒᵈ<VAR>f : LatticeHom αᵒᵈ βᵒᵈ<GOAL>LatticeHom.dual.symm (g.comp f) = (LatticeHom.dual.symm g).comp (LatticeHom.dual.symm f)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>BoundedOrder α<VAR>Lattice β<VAR>BoundedOrder β<VAR>f : BoundedLatticeHom α β<GOAL>(BoundedLatticeHom.dual f).toLatticeHom = LatticeHom.dual f.toLatticeHom
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>BoundedOrder α<VAR>Lattice β<VAR>BoundedOrder β<VAR>f : BoundedLatticeHom αᵒᵈ βᵒᵈ<GOAL>(BoundedLatticeHom.dual.symm f).toLatticeHom = LatticeHom.dual.symm f.toLatticeHom
<VAR>α : Type u_3<VAR>Lattice α<VAR>BoundedOrder α<GOAL>BoundedLatticeHom.dual (BoundedLatticeHom.id α) = BoundedLatticeHom.id αᵒᵈ
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Lattice α<VAR>BoundedOrder α<VAR>Lattice β<VAR>BoundedOrder β<VAR>Lattice γ<VAR>BoundedOrder γ<VAR>g : BoundedLatticeHom β γ<VAR>f : BoundedLatticeHom α β<GOAL>BoundedLatticeHom.dual (g.comp f) = (BoundedLatticeHom.dual g).comp (BoundedLatticeHom.dual f)
<VAR>α : Type u_3<VAR>Lattice α<VAR>BoundedOrder α<GOAL>BoundedLatticeHom.dual.symm (BoundedLatticeHom.id αᵒᵈ) = BoundedLatticeHom.id α
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Lattice α<VAR>BoundedOrder α<VAR>Lattice β<VAR>BoundedOrder β<VAR>Lattice γ<VAR>BoundedOrder γ<VAR>g : BoundedLatticeHom βᵒᵈ γᵒᵈ<VAR>f : BoundedLatticeHom αᵒᵈ βᵒᵈ<GOAL>BoundedLatticeHom.dual.symm (g.comp f) = (BoundedLatticeHom.dual.symm g).comp (BoundedLatticeHom.dual.symm f)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<GOAL>⇑LatticeHom.fst = Prod.fst
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<GOAL>⇑LatticeHom.snd = Prod.snd
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>x : α × β<GOAL>LatticeHom.fst x = x.1
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>x : α × β<GOAL>LatticeHom.snd x = x.2
<VAR>ι : Type u_7<VAR>α : ι → Type u_8<VAR>(i : ι) → Lattice (α i)<VAR>i : ι<GOAL>⇑(Pi.evalLatticeHom i) = Function.eval i
<VAR>ι : Type u_7<VAR>α : ι → Type u_8<VAR>(i : ι) → Lattice (α i)<VAR>i : ι<VAR>f : (i : ι) → α i<GOAL>(Pi.evalLatticeHom i) f = f i
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>SemilatticeSup α<VAR>SemilatticeSup β<VAR>f : SupHom α β<GOAL>∀ (a : WithTop α), f.withTop a = WithTop.map (⇑f) a
<VAR>α : Type u_3<VAR>SemilatticeSup α<GOAL>(SupHom.id α).withTop = SupHom.id (WithTop α)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>SemilatticeSup α<VAR>SemilatticeSup β<VAR>SemilatticeSup γ<VAR>f : SupHom β γ<VAR>g : SupHom α β<GOAL>(f.comp g).withTop = f.withTop.comp g.withTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>SemilatticeSup α<VAR>SemilatticeSup β<VAR>f : SupHom α β<GOAL>∀ (a : Option α), f.withBot.toSupHom a = Option.map (⇑f) a
<VAR>α : Type u_3<VAR>SemilatticeSup α<GOAL>(SupHom.id α).withBot = SupBotHom.id (WithBot α)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>SemilatticeSup α<VAR>SemilatticeSup β<VAR>SemilatticeSup γ<VAR>f : SupHom β γ<VAR>g : SupHom α β<GOAL>(f.comp g).withBot = f.withBot.comp g.withBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>SemilatticeSup α<VAR>SemilatticeSup β<VAR>OrderTop β<VAR>f : SupHom α β<VAR>a : WithTop α<GOAL>f.withTop' a = Option.elim a ⊤ ⇑f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>SemilatticeSup α<VAR>SemilatticeSup β<VAR>OrderBot β<VAR>f : SupHom α β<VAR>a : WithBot α<GOAL>f.withBot'.toSupHom a = Option.elim a ⊥ ⇑f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>f : InfHom α β<GOAL>∀ (a : Option α), f.withTop.toInfHom a = Option.map (⇑f) a
<VAR>α : Type u_3<VAR>SemilatticeInf α<GOAL>(InfHom.id α).withTop = InfTopHom.id (WithTop α)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>SemilatticeInf γ<VAR>f : InfHom β γ<VAR>g : InfHom α β<GOAL>(f.comp g).withTop = f.withTop.comp g.withTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>f : InfHom α β<GOAL>∀ (a : Option α), f.withBot a = Option.map (⇑f) a
<VAR>α : Type u_3<VAR>SemilatticeInf α<GOAL>(InfHom.id α).withBot = InfHom.id (WithBot α)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>SemilatticeInf γ<VAR>f : InfHom β γ<VAR>g : InfHom α β<GOAL>(f.comp g).withBot = f.withBot.comp g.withBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>OrderTop β<VAR>f : InfHom α β<VAR>a : WithTop α<GOAL>f.withTop'.toInfHom a = Option.elim a ⊤ ⇑f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>OrderBot β<VAR>f : InfHom α β<VAR>a : WithBot α<GOAL>f.withBot' a = Option.elim a ⊥ ⇑f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>f : LatticeHom α β<GOAL>f.withTop.toSupHom = f.withTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>f : LatticeHom α β<GOAL>⇑f.withTop = WithTop.map ⇑f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>f : LatticeHom α β<VAR>a : WithTop α<GOAL>f.withTop a = WithTop.map (⇑f) a
<VAR>α : Type u_3<VAR>Lattice α<GOAL>(LatticeHom.id α).withTop = LatticeHom.id (WithTop α)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Lattice α<VAR>Lattice β<VAR>Lattice γ<VAR>f : LatticeHom β γ<VAR>g : LatticeHom α β<GOAL>(f.comp g).withTop = f.withTop.comp g.withTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>f : LatticeHom α β<VAR>a : WithBot α<GOAL>f.withBot.toSupHom a = f.withBot a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>f : LatticeHom α β<GOAL>⇑f.withBot = Option.map ⇑f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>f : LatticeHom α β<VAR>a : WithBot α<GOAL>f.withBot a = WithBot.map (⇑f) a
<VAR>α : Type u_3<VAR>Lattice α<GOAL>(LatticeHom.id α).withBot = LatticeHom.id (WithBot α)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Lattice α<VAR>Lattice β<VAR>Lattice γ<VAR>f : LatticeHom β γ<VAR>g : LatticeHom α β<GOAL>(f.comp g).withBot = f.withBot.comp g.withBot