awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Hom.Basic
Goal:
X : Type u_6
Y : Type u_7
F : Type u_8
inst : LinearOrder X
inst_1 : Preorder Y
inst_2 : EquivLike F X Y
f : F
hf : StrictAnti.{u_6, u_7} (α := X) (β := Y) (⇑f : (a : X) → Y)
a b : X
refine_1 refine_1₁ : b ≤ a ↔ b ≤ a
⊢ LE.le.{u_7} (α := Y) ((f : (a : X) → Y) a : Y) ((f : (a : X) → Y) b : Y) ↔ b ≤ a

Tactic:
rw [hf.le_iff_ge]

Premises used: StrictAnti.le_iff_ge
-- Module: Mathlib.Order.Hom.Bounded
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : EquivLike F α β
inst_1 : LE α
inst_2 : OrderTop α
inst_3 : PartialOrder β
inst_4 : OrderTop β
inst_5 : OrderIsoClass F α β
f : F
a : α
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) ⊤ : β) ↔ a = ⊤
rw₁ rw₂ : a = ⊤ ↔ a = ⊤
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) (⊤ : β) ↔ a = ⊤

Tactic:
rw [← map_top f, (EquivLike.injective f).eq_iff]

Premises used: Function.Injective.eq_iff, TopHomClass.map_top, EquivLike.injective
-- Module: Mathlib.Order.Hom.Bounded
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Top α
inst_2 : Top β
inst_3 : Top γ
inst_4 : Top δ
f g : TopHom α β
h : f.toFun = g.toFun
mk :
  ∀ (toFun : α → β) (map_top' : toFun ⊤ = ⊤)
    (h : { toFun := toFun, map_top' := map_top' : TopHom α β }.toFun = g.toFun),
    { toFun := toFun, map_top' := map_top' : TopHom α β } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Order.Hom.Bounded
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Top α
inst_2 : Top β
inst_3 : Top γ
inst_4 : Top δ
g : TopHom α β
toFun : α → β
map_top' : toFun ⊤ = ⊤
h : { toFun := toFun, map_top' := map_top' : TopHom α β }.toFun = g.toFun
mk :
  ∀ (toFun_1 : α → β) (map_top'_1 : toFun_1 ⊤ = ⊤)
    (h :
      { toFun := toFun, map_top' := map_top' : TopHom α β }.toFun =
        { toFun := toFun_1, map_top' := map_top'_1 : TopHom α β }.toFun),
    { toFun := toFun, map_top' := map_top' : TopHom α β } = { toFun := toFun_1, map_top' := map_top'_1 }
⊢ { toFun := toFun, map_top' := map_top' : TopHom α β } = g

Tactic:
cases g
-- Module: Mathlib.Order.Hom.Bounded
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Top α
inst_2 : Top β
inst_3 : Top γ
inst_4 : Top δ
toFun : α → β
map_top' : toFun ⊤ = ⊤
toFun_1 : α → β
map_top'_1 : toFun_1 ⊤ = ⊤
h :
  { toFun := toFun, map_top' := map_top' : TopHom α β }.toFun =
    { toFun := toFun_1, map_top' := map_top'_1 : TopHom α β }.toFun
⊢ { toFun := toFun, map_top' := map_top' : TopHom α β } = { toFun := toFun_1, map_top' := map_top'_1 }

Tactic:
congr
-- Module: Mathlib.Order.Hom.Bounded
Goal:
α : Type u_2
β : Type u_3
inst : Top α
inst_1 : Top β
f g : TopHom α β
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.Order.Hom.Bounded
Goal:
α : Type u_2
β : Type u_3
inst : Top α
inst_1 : Top β
f : TopHom α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ (⇑(f.copy f' h) : (a : α) → β) = f'

Tactic:
rfl

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

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Order.Hom.Bounded
Goal:
α : Type u_2
inst : Top α
⊢ Eq (α := (a : α) → α) (⇑(TopHom.id α) : (a : α) → α) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Bounded
Goal:
α : Type u_2
inst : Top α
a : α
⊢ (TopHom.id α : (a : α) → α) a = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Bounded
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Top α
inst_2 : Top β
inst_3 : Top γ
inst_4 : Top δ
f : TopHom β γ
g : TopHom α β
rw : Eq.{u_4 + 1} (α := γ) ((f : (a : β) → γ) ((g : (a : α) → β) ⊤ : β) : γ) (⊤ : γ)
rw₁ : Eq.{u_4 + 1} (α := γ) ((f : (a : β) → γ) ⊤ : γ) (⊤ : γ)
rw₂ rw₃ : Eq.{u_4 + 1} (α := γ) ⊤ ⊤
⊢ Eq.{u_4 + 1} (α := γ)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β) ⊤) ⊤

Tactic:
rw [comp_apply, map_top, map_top]

Premises used: TopHomClass.map_top, Function.comp_apply
-- Module: Mathlib.Order.Hom.Bounded
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Top α
inst_1 : Top β
inst_2 : Top γ
f : TopHom β γ
g : TopHom α β
⊢ 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.Order.Hom.Bounded
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Top α
inst_1 : Top β
inst_2 : Top γ
f : TopHom β γ
g : TopHom α β
a : α
⊢ Eq.{u_4 + 1} (α := γ) ((f.comp g : (a : α) → γ) a : γ) ((f : (a : β) → γ) ((g : (a : α) → β) a : β) : γ)

Tactic:
rfl

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

Tactic:
rfl

Premises used: TopHom.comp, rfl
-- Module: Mathlib.Order.Hom.Bounded
Goal:
α : Type u_2
β : Type u_3
inst : Top α
inst_1 : Top β
f : TopHom α β
⊢ f.comp (TopHom.id α) = f

Tactic:
TopHom.ext fun _ => rfl

Premises used: TopHom.ext, rfl
-- Module: Mathlib.Order.Hom.Bounded
Goal:
α : Type u_2
β : Type u_3
inst : Top α
inst_1 : Top β
f : TopHom α β
⊢ comp (TopHom.id β) f = f

Tactic:
TopHom.ext fun _ => rfl

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

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

Premises used: Iff.mpr, Function.Surjective.forall, DFunLike.ext_iff, congr_arg, TopHom.ext, Iff.intro, Iff.mp, TopHom.comp
-- Module: Mathlib.Order.Hom.Bounded
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Top α
inst_1 : Top β
inst_2 : Top γ
g : TopHom β γ
f₁ f₂ : TopHom α β
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 [← TopHom.comp_apply, h, TopHom.comp_apply]

Premises used: TopHom.comp_apply
-- Module: Mathlib.Order.Hom.Bounded
Goal:
α : Type u_2
β : Type u_3
inst : Top α
inst_1 : LE β
inst_2 : OrderTop β
⊢ Eq (α := (a : α) → β) (⇑⊤ : (a : α) → β) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Bounded
Goal:
α : Type u_2
β : Type u_3
inst : Top α
inst_1 : LE β
inst_2 : OrderTop β
a : α
⊢ Eq.{u_3 + 1} (α := β) ((⊤ : (a : α) → β) a : β) (⊤ : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Bounded
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Top α
inst_2 : SemilatticeInf β
inst_3 : OrderTop β
f_1 g_1 f g : TopHom α β
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ ⊓ (g : (a : α) → β) ⊤ : β) (⊤ : β)
rw₁ : Eq.{u_3 + 1} (α := β) (⊤ ⊓ (g : (a : α) → β) ⊤ : β) (⊤ : β)
rw₂ : Eq.{u_3 + 1} (α := β) (⊤ ⊓ ⊤) ⊤
rw₃ rw₄ : Eq.{u_3 + 1} (α := β) ⊤ ⊤
⊢ Eq.{u_3 + 1} (α := β) (((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β)) ⊤ : β) (⊤ : β)

Tactic:
rw [Pi.inf_apply, map_top, map_top, inf_top_eq]

Premises used: inf_top_eq, TopHomClass.map_top, Pi.inf_apply
-- Module: Mathlib.Order.Hom.Bounded
Goal:
α : Type u_2
β : Type u_3
inst : Top α
inst_1 : SemilatticeInf β
inst_2 : OrderTop β
f g : TopHom α β
⊢ Eq (α := (a : α) → β) (⇑(f ⊓ g) : (a : α) → β) ((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Bounded
Goal:
α : Type u_2
β : Type u_3
inst : Top α
inst_1 : SemilatticeInf β
inst_2 : OrderTop β
f g : TopHom α β
a : α
⊢ Eq.{u_3 + 1} (α := β) ((f ⊓ g : (a : α) → β) a : β) ((f : (a : α) → β) a ⊓ (g : (a : α) → β) a : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Bounded
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Top α
inst_2 : SemilatticeSup β
inst_3 : OrderTop β
f_1 g_1 f g : TopHom α β
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ ⊔ (g : (a : α) → β) ⊤ : β) (⊤ : β)
rw₁ : Eq.{u_3 + 1} (α := β) (⊤ ⊔ (g : (a : α) → β) ⊤ : β) (⊤ : β)
rw₂ : Eq.{u_3 + 1} (α := β) (⊤ ⊔ ⊤) ⊤
rw₃ rw₄ : Eq.{u_3 + 1} (α := β) ⊤ ⊤
⊢ Eq.{u_3 + 1} (α := β) (((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β)) ⊤ : β) (⊤ : β)

Tactic:
rw [Pi.sup_apply, map_top, map_top, sup_top_eq]

Premises used: sup_top_eq, TopHomClass.map_top, Pi.sup_apply
-- Module: Mathlib.Order.Hom.Bounded
Goal:
α : Type u_2
β : Type u_3
inst : Top α
inst_1 : SemilatticeSup β
inst_2 : OrderTop β
f g : TopHom α β
⊢ Eq (α := (a : α) → β) (⇑(f ⊔ g) : (a : α) → β) ((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Bounded
Goal:
α : Type u_2
β : Type u_3
inst : Top α
inst_1 : SemilatticeSup β
inst_2 : OrderTop β
f g : TopHom α β
a : α
⊢ Eq.{u_3 + 1} (α := β) ((f ⊔ g : (a : α) → β) a : β) ((f : (a : α) → β) a ⊔ (g : (a : α) → β) a : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Bounded
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Preorder γ
inst_4 : Preorder δ
inst_5 : BoundedOrder α
inst_6 : BoundedOrder β
inst_7 : BoundedOrder γ
inst_8 : BoundedOrder δ
f g : BoundedOrderHom α β
h : Eq (α := (a : α) → β) ((fun (f : BoundedOrderHom α β) ↦ f.toFun) f) ((fun (f : BoundedOrderHom α β) ↦ f.toFun) g)
obtain :
  ∀ (toFun : α → β) (monotone' : Monotone toFun)
    (map_top' : { toFun := toFun, monotone' := monotone' : α →o β }.toFun ⊤ = ⊤)
    (map_bot' : { toFun := toFun, monotone' := monotone' : α →o β }.toFun ⊥ = ⊥)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : BoundedOrderHom α β) ↦ f.toFun)
          { toFun := toFun, monotone' := monotone', map_top' := map_top', map_bot' := map_bot' })
        ((fun (f : BoundedOrderHom α β) ↦ f.toFun) g)),
    { toFun := toFun, monotone' := monotone', map_top' := map_top', map_bot' := map_bot' : BoundedOrderHom α β } = g
⊢ f = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := f
-- Module: Mathlib.Order.Hom.Bounded
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Preorder γ
inst_4 : Preorder δ
inst_5 : BoundedOrder α
inst_6 : BoundedOrder β
inst_7 : BoundedOrder γ
inst_8 : BoundedOrder δ
g : BoundedOrderHom α β
toFun : α → β
monotone' : Monotone toFun
map_top' : { toFun := toFun, monotone' := monotone' : α →o β }.toFun ⊤ = ⊤
map_bot' : { toFun := toFun, monotone' := monotone' : α →o β }.toFun ⊥ = ⊥
h :
  Eq (α := (a : α) → β)
    ((fun (f : BoundedOrderHom α β) ↦ f.toFun)
      { toFun := toFun, monotone' := monotone', map_top' := map_top', map_bot' := map_bot' })
    ((fun (f : BoundedOrderHom α β) ↦ f.toFun) g)
obtain :
  ∀ (toFun_1 : α → β) (monotone'_1 : Monotone toFun_1)
    (map_top'_1 : { toFun := toFun_1, monotone' := monotone'_1 : α →o β }.toFun ⊤ = ⊤)
    (map_bot'_1 : { toFun := toFun_1, monotone' := monotone'_1 : α →o β }.toFun ⊥ = ⊥)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : BoundedOrderHom α β) ↦ f.toFun)
          { toFun := toFun, monotone' := monotone', map_top' := map_top', map_bot' := map_bot' })
        ((fun (f : BoundedOrderHom α β) ↦ f.toFun)
          { toFun := toFun_1, monotone' := monotone'_1, map_top' := map_top'_1, map_bot' := map_bot'_1 })),
    { toFun := toFun, monotone' := monotone', map_top' := map_top', map_bot' := map_bot' : BoundedOrderHom α β } =
      { toFun := toFun_1, monotone' := monotone'_1, map_top' := map_top'_1, map_bot' := map_bot'_1 }
⊢ { toFun := toFun, monotone' := monotone', map_top' := map_top', map_bot' := map_bot' : BoundedOrderHom α β } = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := g
-- Module: Mathlib.Order.Hom.Bounded
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Preorder γ
inst_4 : Preorder δ
inst_5 : BoundedOrder α
inst_6 : BoundedOrder β
inst_7 : BoundedOrder γ
inst_8 : BoundedOrder δ
toFun : α → β
monotone' : Monotone toFun
map_top' : { toFun := toFun, monotone' := monotone' : α →o β }.toFun ⊤ = ⊤
map_bot' : { toFun := toFun, monotone' := monotone' : α →o β }.toFun ⊥ = ⊥
toFun_1 : α → β
monotone'_1 : Monotone toFun_1
map_top'_1 : { toFun := toFun_1, monotone' := monotone'_1 : α →o β }.toFun ⊤ = ⊤
map_bot'_1 : { toFun := toFun_1, monotone' := monotone'_1 : α →o β }.toFun ⊥ = ⊥
h :
  Eq (α := (a : α) → β)
    ((fun (f : BoundedOrderHom α β) ↦ f.toFun)
      { toFun := toFun, monotone' := monotone', map_top' := map_top', map_bot' := map_bot' })
    ((fun (f : BoundedOrderHom α β) ↦ f.toFun)
      { toFun := toFun_1, monotone' := monotone'_1, map_top' := map_top'_1, map_bot' := map_bot'_1 })
⊢ { toFun := toFun, monotone' := monotone', map_top' := map_top', map_bot' := map_bot' : BoundedOrderHom α β } =
    { toFun := toFun_1, monotone' := monotone'_1, map_top' := map_top'_1, map_bot' := map_bot'_1 }

Tactic:
congr
-- Module: Mathlib.Order.Hom.Bounded
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : BoundedOrder α
inst_3 : BoundedOrder β
f g : BoundedOrderHom α β
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.Order.Hom.Bounded
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : BoundedOrder α
inst_3 : BoundedOrder β
f : BoundedOrderHom α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ (⇑(f.copy f' h) : (a : α) → β) = f'

Tactic:
rfl

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

Tactic:
DFunLike.ext' h

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Bounded
Goal:
α : Type u_2
inst : Preorder α
inst_1 : BoundedOrder α
a : α
⊢ (BoundedOrderHom.id α : (a : α) → α) a = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Bounded
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : BoundedOrder α
inst_4 : BoundedOrder β
inst_5 : BoundedOrder γ
f : BoundedOrderHom β γ
g : BoundedOrderHom α β
⊢ 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.Order.Hom.Bounded
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : BoundedOrder α
inst_4 : BoundedOrder β
inst_5 : BoundedOrder γ
f : BoundedOrderHom β γ
g : BoundedOrderHom α β
a : α
⊢ Eq.{u_4 + 1} (α := γ) ((f.comp g : (a : α) → γ) a : γ) ((f : (a : β) → γ) ((g : (a : α) → β) a : β) : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Bounded
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : BoundedOrder α
inst_4 : BoundedOrder β
inst_5 : BoundedOrder γ
f : BoundedOrderHom β γ
g : BoundedOrderHom α β
⊢ Eq (α := α →o γ) (↑(f.comp g) : α →o γ) (OrderHom.comp (↑f : β →o γ) (↑g : α →o β))

Tactic:
rfl

Premises used: OrderHom.comp, OrderHomClass.toOrderHom, rfl
-- Module: Mathlib.Order.Hom.Bounded
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : BoundedOrder α
inst_4 : BoundedOrder β
inst_5 : BoundedOrder γ
f : BoundedOrderHom β γ
g : BoundedOrderHom α β
⊢ Eq (α := TopHom α γ) (↑(f.comp g) : TopHom α γ) (TopHom.comp (↑f : TopHom β γ) (↑g : TopHom α β))

Tactic:
rfl

Premises used: TopHomClass.toTopHom, TopHom.comp, rfl
-- Module: Mathlib.Order.Hom.Bounded
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : Preorder δ
inst_4 : BoundedOrder α
inst_5 : BoundedOrder β
inst_6 : BoundedOrder γ
inst_7 : BoundedOrder δ
f : BoundedOrderHom γ δ
g : BoundedOrderHom β γ
h : BoundedOrderHom α β
⊢ (f.comp g).comp h = f.comp (g.comp h)

Tactic:
rfl

Premises used: OrderHom.comp, BoundedOrderHom.comp, rfl
-- Module: Mathlib.Order.Hom.Bounded
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : BoundedOrder α
inst_3 : BoundedOrder β
f : BoundedOrderHom α β
⊢ f.comp (BoundedOrderHom.id α) = f

Tactic:
BoundedOrderHom.ext fun _ => rfl

Premises used: BoundedOrderHom.ext, rfl
-- Module: Mathlib.Order.Hom.Bounded
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : BoundedOrder α
inst_3 : BoundedOrder β
f : BoundedOrderHom α β
⊢ comp (BoundedOrderHom.id β) f = f

Tactic:
BoundedOrderHom.ext fun _ => rfl

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

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

Premises used: Iff.mpr, Function.Surjective.forall, DFunLike.ext_iff, congr_arg, BoundedOrderHom.ext, Iff.intro, Iff.mp, BoundedOrderHom.comp
-- Module: Mathlib.Order.Hom.Bounded
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : BoundedOrder α
inst_4 : BoundedOrder β
inst_5 : BoundedOrder γ
g : BoundedOrderHom β γ
f₁ f₂ : BoundedOrderHom α β
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 [← BoundedOrderHom.comp_apply, h, BoundedOrderHom.comp_apply]

Premises used: BoundedOrderHom.comp_apply
-- Module: Mathlib.Order.Hom.Bounded
Goal:
α : Type u_2
inst : LE α
inst_1 : OrderTop α
⊢ Eq (α := BotHom αᵒᵈ αᵒᵈ) ((TopHom.dual : (a : TopHom α α) → BotHom αᵒᵈ αᵒᵈ) (TopHom.id α) : BotHom αᵒᵈ αᵒᵈ)
    (BotHom.id αᵒᵈ : BotHom αᵒᵈ αᵒᵈ)

Tactic:
rfl

Premises used: OrderDual, rfl, BotHom.id
-- Module: Mathlib.Order.Hom.Bounded
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : LE α
inst_1 : OrderTop α
inst_2 : LE β
inst_3 : OrderTop β
inst_4 : LE γ
inst_5 : OrderTop γ
g : TopHom β γ
f : TopHom α β
⊢ Eq (α := BotHom.{u_2, u_4} αᵒᵈ γᵒᵈ)
    ((TopHom.dual : (a : TopHom α γ) → BotHom αᵒᵈ γᵒᵈ) (g.comp f) : BotHom.{u_2, u_4} αᵒᵈ γᵒᵈ)
    (BotHom.comp.{u_2, u_3, u_4} (β := βᵒᵈ) ((TopHom.dual : (a : TopHom β γ) → BotHom βᵒᵈ γᵒᵈ) g)
        ((TopHom.dual : (a : TopHom α β) → BotHom αᵒᵈ βᵒᵈ) f) :
      BotHom.{u_2, u_4} αᵒᵈ γᵒᵈ)

Tactic:
rfl

Premises used: BotHom.comp, OrderDual, rfl
-- Module: Mathlib.Order.Hom.Bounded
Goal:
α : Type u_2
inst : LE α
inst_1 : OrderTop α
⊢ Eq.{u_2 + 1} (α := TopHom α α)
    ((Equiv.symm TopHom.dual : (a : BotHom αᵒᵈ αᵒᵈ) → TopHom α α) (BotHom.id αᵒᵈ) : TopHom α α)
    (TopHom.id α : TopHom α α)

Tactic:
rfl

Premises used: TopHom.id, OrderDual, rfl
-- Module: Mathlib.Order.Hom.Bounded
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : LE α
inst_1 : OrderTop α
inst_2 : LE β
inst_3 : OrderTop β
inst_4 : LE γ
inst_5 : OrderTop γ
g : BotHom.{u_3, u_4} βᵒᵈ γᵒᵈ
f : BotHom.{u_2, u_3} αᵒᵈ βᵒᵈ
⊢ Eq (α := TopHom α γ) ((Equiv.symm TopHom.dual : (a : BotHom αᵒᵈ γᵒᵈ) → TopHom α γ) (g.comp f) : TopHom α γ)
    (comp.{u_2, u_3, u_4} (β := β) ((Equiv.symm TopHom.dual : (a : BotHom βᵒᵈ γᵒᵈ) → TopHom β γ) g)
        ((Equiv.symm TopHom.dual : (a : BotHom αᵒᵈ βᵒᵈ) → TopHom α β) f) :
      TopHom α γ)

Tactic:
rfl

Premises used: OrderDual, TopHom.comp, rfl
-- Module: Mathlib.Order.Hom.Bounded
Goal:
α : Type u_2
inst : Preorder α
inst_1 : BoundedOrder α
⊢ Eq (α := BoundedOrderHom αᵒᵈ αᵒᵈ)
    ((BoundedOrderHom.dual : (a : BoundedOrderHom α α) → BoundedOrderHom αᵒᵈ αᵒᵈ) (BoundedOrderHom.id α) :
      BoundedOrderHom αᵒᵈ αᵒᵈ)
    (BoundedOrderHom.id αᵒᵈ : BoundedOrderHom αᵒᵈ αᵒᵈ)

Tactic:
rfl

Premises used: OrderHom.id, BoundedOrderHom.id, rfl
-- Module: Mathlib.Order.Hom.Bounded
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : BoundedOrder α
inst_2 : Preorder β
inst_3 : BoundedOrder β
inst_4 : Preorder γ
inst_5 : BoundedOrder γ
g : BoundedOrderHom β γ
f : BoundedOrderHom α β
⊢ Eq (α := BoundedOrderHom.{u_2, u_4} αᵒᵈ γᵒᵈ)
    ((BoundedOrderHom.dual : (a : BoundedOrderHom α γ) → BoundedOrderHom αᵒᵈ γᵒᵈ) (g.comp f) :
      BoundedOrderHom.{u_2, u_4} αᵒᵈ γᵒᵈ)
    (comp.{u_2, u_3, u_4} (β := βᵒᵈ) ((BoundedOrderHom.dual : (a : BoundedOrderHom β γ) → BoundedOrderHom βᵒᵈ γᵒᵈ) g)
        ((BoundedOrderHom.dual : (a : BoundedOrderHom α β) → BoundedOrderHom αᵒᵈ βᵒᵈ) f) :
      BoundedOrderHom.{u_2, u_4} αᵒᵈ γᵒᵈ)

Tactic:
rfl

Premises used: OrderHom.comp, BoundedOrderHom.comp, rfl
-- Module: Mathlib.Order.Hom.Bounded
Goal:
α : Type u_2
inst : Preorder α
inst_1 : BoundedOrder α
⊢ Eq.{u_2 + 1} (α := BoundedOrderHom α α)
    ((Equiv.symm BoundedOrderHom.dual : (a : BoundedOrderHom αᵒᵈ αᵒᵈ) → BoundedOrderHom α α) (BoundedOrderHom.id αᵒᵈ) :
      BoundedOrderHom α α)
    (BoundedOrderHom.id α : BoundedOrderHom α α)

Tactic:
rfl

Premises used: OrderHom.id, BoundedOrderHom.id, rfl
-- Module: Mathlib.Order.Hom.Bounded
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : BoundedOrder α
inst_2 : Preorder β
inst_3 : BoundedOrder β
inst_4 : Preorder γ
inst_5 : BoundedOrder γ
g : BoundedOrderHom.{u_3, u_4} βᵒᵈ γᵒᵈ
f : BoundedOrderHom.{u_2, u_3} αᵒᵈ βᵒᵈ
⊢ Eq (α := BoundedOrderHom α γ)
    ((Equiv.symm BoundedOrderHom.dual : (a : BoundedOrderHom αᵒᵈ γᵒᵈ) → BoundedOrderHom α γ) (g.comp f) :
      BoundedOrderHom α γ)
    (comp.{u_2, u_3, u_4} (β := β)
        ((Equiv.symm BoundedOrderHom.dual : (a : BoundedOrderHom βᵒᵈ γᵒᵈ) → BoundedOrderHom β γ) g)
        ((Equiv.symm BoundedOrderHom.dual : (a : BoundedOrderHom αᵒᵈ βᵒᵈ) → BoundedOrderHom α β) f) :
      BoundedOrderHom α γ)

Tactic:
rfl

Premises used: OrderHom.comp, BoundedOrderHom.comp, rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Max α
inst_2 : Max β
inst_3 : Bot α
inst_4 : Bot β
inst_5 : SupBotHomClass F α β
⊢ BotHomClass F α β

Tactic:
{ ‹SupBotHomClass F α β› with }

Premises used: SupBotHomClass.map_bot, BotHomClass.mk
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Lattice α
inst_2 : Lattice β
inst_3 : BoundedOrder α
inst_4 : BoundedOrder β
inst_5 : BoundedLatticeHomClass F α β
⊢ SupBotHomClass F α β

Tactic:
{ ‹BoundedLatticeHomClass F α β› with }

Premises used: SupBotHomClass.mk, BoundedLatticeHomClass.map_bot