awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
f : α → α
inst_1 : Nonempty α
le_map : ∀ (x : α), x ≤ f x
x : α := Classical.ofNonempty
y : α := cSup { carrier := bot x f, Nonempty' := ⋯, isChain' := ⋯ : NonemptyChain α }
⊢ (fixedPoints f).Nonempty
have h : y ∈ fixedPoints f
Tactic: use y
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
f : α → α
inst_1 : Nonempty α
le_map : ∀ (x : α), x ≤ f x
x : α := Classical.ofNonempty
y : α := cSup { carrier := bot x f, Nonempty' := ⋯, isChain' := ⋯ : NonemptyChain α }
⊢ y ∈ fixedPoints f
have apply : f y ∈ bot x f
Tactic: apply le_antisymm (le_cSup _ _ (_ : f y ∈ bot x f)) (le_map y)
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
f : α → α
inst_1 : Nonempty α
le_map : ∀ (x : α), x ≤ f x
x : α := Classical.ofNonempty
y : α := cSup { carrier := bot x f, Nonempty' := ⋯, isChain' := ⋯ : NonemptyChain α }
⊢ f y ∈ bot x f
have a : f y ∈ f '' bot x f
Tactic: apply (bot_isAdmissible le_map).image_self_subset_self
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
f : α → α
inst_1 : Nonempty α
le_map : ∀ (x : α), x ≤ f x
x : α := Classical.ofNonempty
y : α := cSup { carrier := bot x f, Nonempty' := ⋯, isChain' := ⋯ : NonemptyChain α }
⊢ f y ∈ f '' bot x f
have h : y ∈ bot x f ∧ f y = f y
Tactic: use y
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_3
inst : OmegaCompletePartialOrder α
inst_1 : CompleteLattice β
f : ι → α → β
hf : ∀ (i : ι), ωScottContinuous (f i)
⊢ ωScottContinuous.{u_1, u_2} (α := α) (β := β) (⨆ (i : ι), f i)
have refine : ∀ (c : Chain α) (a : β), (⨆ (i : ι), f i) (ωSup c) ≤ a ↔ ωSup (c.map { toFun := ⨆ (i : ι), f i, monotone' := sorry }) ≤ a
Tactic: refine ωScottContinuous.of_monotone_map_ωSup
    ⟨Monotone.iSup fun i ↦ (hf i).monotone, fun c ↦ eq_of_forall_ge_iff fun a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
Goal:
α : Type u_1
β : Type u_2
inst : OmegaCompletePartialOrder α
inst_1 : CompleteLattice β
s : Set (α → β)
hs : ∀ f ∈ s, ωScottContinuous f
⊢ ωScottContinuous (SupSet.sSup s)
have rw : ωScottContinuous.{u_1, u_2} (α := α) (β := β) (⨆ a ∈ s, a)
Tactic: rw [sSup_eq_iSup]
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
Goal:
α : Type u_1
β : Type u_2
inst : OmegaCompletePartialOrder α
inst_1 : CompleteLattice β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
⊢ ωScottContinuous (f ⊔ g)
have rw : ωScottContinuous.{u_1, u_2} (α := α) (β := β) (SupSet.sSup {f, g})
Tactic: rw [← sSup_pair]
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
Goal:
α : Type u_1
β : Type u_2
inst : OmegaCompletePartialOrder α
inst_1 : CompleteLattice β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
⊢ ωScottContinuous.{u_1, u_2} (α := α) (β := β) (SupSet.sSup {f, g})
have hs : ∀ (f_1 : α → β), Membership.mem (γ := Set (α → β)) {f, g} f_1 → ωScottContinuous f_1
Tactic: apply ωScottContinuous.sSup
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
Goal:
α : Type u_1
β : Type u_2
inst : OmegaCompletePartialOrder α
inst_1 : CompleteLattice β
⊢ ωScottContinuous.{u_1, u_2} (α := α) (β := β) ⊥
have rw : ωScottContinuous.{u_1, u_2} (α := α) (β := β) (SupSet.sSup ∅)
Tactic: rw [← sSup_empty]
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
Goal:
α : Type u_1
β : Type u_2
inst : OmegaCompletePartialOrder α
inst_1 : CompleteLinearOrder β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
⊢ ωScottContinuous (f ⊓ g)
have refine : ∀ (c : Chain α) (a : β), (f ⊓ g) (ωSup c) ≤ a ↔ ωSup (c.map { toFun := f ⊓ g, monotone' := sorry : α →o β }) ≤ a
Tactic: refine ωScottContinuous.of_monotone_map_ωSup
    ⟨hf.monotone.inf hg.monotone, fun c ↦ eq_of_forall_ge_iff fun a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
Goal:
α : Type u_1
β : Type u_2
inst : OmegaCompletePartialOrder α
inst_1 : CompleteLinearOrder β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
c : Chain α
a : β
⊢ (f ⊓ g) (ωSup c) ≤ a ↔ ωSup (c.map { toFun := f ⊓ g, monotone' := ⋯ : α →o β }) ≤ a
have simp : (∀ (x x_1 : ℕ), f ((c : (a : ℕ) → α) x_1) ≤ a ∨ g ((c : (a : ℕ) → α) x) ≤ a) ↔
  ∀ (i : ℕ), f ((c : (a : ℕ) → α) i) ≤ a ∨ g ((c : (a : ℕ) → α) i) ≤ a
Tactic: simp only [Pi.inf_apply, hf.map_ωSup c, hg.map_ωSup c, inf_le_iff, ωSup_le_iff, Chain.coe_map,
    Function.comp, OrderHom.coe_mk, ← forall_or_left, ← forall_or_right]
-- Lean 4 proof step from Mathlib.Order.Category.BddLat (goal)
Goal:
α β : BddLat
e : (↑α.toLat : Type u) ≃o (↑β.toLat : Type u)
⊢ CategoryStruct.comp (Y := β)
      (ofHom
        (let __src : LatticeHom (↑α.1 : Type u) (↑β.1 : Type u) :=
          { toFun := (⇑e : (a : (↑α.1 : Type u)) → (↑β.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := (⇑e : (a : (↑α.1 : Type u)) → (↑β.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯,
          map_bot' := ⋯ }))
      (ofHom
        (let __src : LatticeHom (↑β.1 : Type u) (↑α.1 : Type u) :=
          { toFun := (⇑e.symm : (a : (↑β.1 : Type u)) → (↑α.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := (⇑e.symm : (a : (↑β.1 : Type u)) → (↑α.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯,
          map_bot' := ⋯ })) =
    𝟙 α
have hf : ∀ (a : (↑α.toLat : Type u)),
  Eq (α := (↑α.toLat : Type u))
    ((Hom.hom
            (CategoryStruct.comp (Y := β)
              (ofHom
                (let __src : LatticeHom (↑α.1 : Type u) (↑β.1 : Type u) :=
                  { toFun := (⇑e : (a : (↑α.1 : Type u)) → (↑β.1 : Type u)), map_sup' := sorry, map_inf' := sorry };
                { toFun := (⇑e : (a : (↑α.1 : Type u)) → (↑β.1 : Type u)), map_sup' := sorry, map_inf' := sorry, map_top' := sorry,
                  map_bot' := sorry }))
              (ofHom
                (let __src : LatticeHom (↑β.1 : Type u) (↑α.1 : Type u) :=
                  { toFun := (⇑e.symm : (a : (↑β.1 : Type u)) → (↑α.1 : Type u)), map_sup' := sorry, map_inf' := sorry };
                { toFun := (⇑e.symm : (a : (↑β.1 : Type u)) → (↑α.1 : Type u)), map_sup' := sorry, map_inf' := sorry,
                  map_top' := sorry, map_bot' := sorry }))) :
          (a : (↑α.toLat : Type u)) → (↑α.toLat : Type u))
        a :
      (↑α.toLat : Type u))
    ((Hom.hom (𝟙 α) : (a : (↑α.toLat : Type u)) → (↑α.toLat : Type u)) a : (↑α.toLat : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Category.BddLat (goal)
Goal:
α β : BddLat
e : (↑α.toLat : Type u) ≃o (↑β.toLat : Type u)
⊢ CategoryStruct.comp (Y := α)
      (ofHom
        (let __src : LatticeHom (↑β.1 : Type u) (↑α.1 : Type u) :=
          { toFun := (⇑e.symm : (a : (↑β.1 : Type u)) → (↑α.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := (⇑e.symm : (a : (↑β.1 : Type u)) → (↑α.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯,
          map_bot' := ⋯ }))
      (ofHom
        (let __src : LatticeHom (↑α.1 : Type u) (↑β.1 : Type u) :=
          { toFun := (⇑e : (a : (↑α.1 : Type u)) → (↑β.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := (⇑e : (a : (↑α.1 : Type u)) → (↑β.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯,
          map_bot' := ⋯ })) =
    𝟙 β
have hf : ∀ (a : (↑β.toLat : Type u)),
  Eq (α := (↑β.toLat : Type u))
    ((Hom.hom
            (CategoryStruct.comp (Y := α)
              (ofHom
                (let __src : LatticeHom (↑β.1 : Type u) (↑α.1 : Type u) :=
                  { toFun := (⇑e.symm : (a : (↑β.1 : Type u)) → (↑α.1 : Type u)), map_sup' := sorry, map_inf' := sorry };
                { toFun := (⇑e.symm : (a : (↑β.1 : Type u)) → (↑α.1 : Type u)), map_sup' := sorry, map_inf' := sorry,
                  map_top' := sorry, map_bot' := sorry }))
              (ofHom
                (let __src : LatticeHom (↑α.1 : Type u) (↑β.1 : Type u) :=
                  { toFun := (⇑e : (a : (↑α.1 : Type u)) → (↑β.1 : Type u)), map_sup' := sorry, map_inf' := sorry };
                { toFun := (⇑e : (a : (↑α.1 : Type u)) → (↑β.1 : Type u)), map_sup' := sorry, map_inf' := sorry, map_top' := sorry,
                  map_bot' := sorry }))) :
          (a : (↑β.toLat : Type u)) → (↑β.toLat : Type u))
        a :
      (↑β.toLat : Type u))
    ((Hom.hom (𝟙 β) : (a : (↑β.toLat : Type u)) → (↑β.toLat : Type u)) a : (↑β.toLat : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Category.BddOrd (goal)
Goal:
α β : BddOrd
e : (↑α.toPartOrd : Type u) ≃o (↑β.toPartOrd : Type u)
⊢ CategoryStruct.comp (Y := β) (ofHom (↑e : BoundedOrderHom (↑α.1 : Type u) (↑β.1 : Type u)))
      (ofHom (↑e.symm : BoundedOrderHom (↑β.1 : Type u) (↑α.1 : Type u))) =
    𝟙 α
have hf : ∀ (a : (↑α.toPartOrd : Type u)),
  Eq (α := (↑α.toPartOrd : Type u))
    ((Hom.hom
            (CategoryStruct.comp (Y := β) (ofHom (↑e : BoundedOrderHom (↑α.1 : Type u) (↑β.1 : Type u)))
              (ofHom (↑e.symm : BoundedOrderHom (↑β.1 : Type u) (↑α.1 : Type u)))) :
          (a : (↑α.toPartOrd : Type u)) → (↑α.toPartOrd : Type u))
        a :
      (↑α.toPartOrd : Type u))
    ((Hom.hom (𝟙 α) : (a : (↑α.toPartOrd : Type u)) → (↑α.toPartOrd : Type u)) a : (↑α.toPartOrd : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Category.BddOrd (goal)
Goal:
α β : BddOrd
e : (↑α.toPartOrd : Type u) ≃o (↑β.toPartOrd : Type u)
⊢ CategoryStruct.comp (Y := α) (ofHom (↑e.symm : BoundedOrderHom (↑β.1 : Type u) (↑α.1 : Type u)))
      (ofHom (↑e : BoundedOrderHom (↑α.1 : Type u) (↑β.1 : Type u))) =
    𝟙 β
have hf : ∀ (a : (↑β.toPartOrd : Type u)),
  Eq (α := (↑β.toPartOrd : Type u))
    ((Hom.hom
            (CategoryStruct.comp (Y := α) (ofHom (↑e.symm : BoundedOrderHom (↑β.1 : Type u) (↑α.1 : Type u)))
              (ofHom (↑e : BoundedOrderHom (↑α.1 : Type u) (↑β.1 : Type u)))) :
          (a : (↑β.toPartOrd : Type u)) → (↑β.toPartOrd : Type u))
        a :
      (↑β.toPartOrd : Type u))
    ((Hom.hom (𝟙 β) : (a : (↑β.toPartOrd : Type u)) → (↑β.toPartOrd : Type u)) a : (↑β.toPartOrd : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Category.CompleteLat (goal)
Goal:
α β : CompleteLat
e : (↑α : Type u) ≃o (↑β : Type u)
⊢ CategoryStruct.comp (Y := β)
      (ConcreteCategory.ofHom (FC := fun (x1 x2 : CompleteLat.{u}) ↦ CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u))
        (CC := carrier) { toFun := (⇑e : (a : (↑α : Type u)) → (↑β : Type u)), map_sInf' := ⋯, map_sSup' := ⋯ })
      (ConcreteCategory.ofHom (FC := fun (x1 x2 : CompleteLat.{u}) ↦ CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u))
        (CC := carrier) { toFun := (⇑e.symm : (a : (↑β : Type u)) → (↑α : Type u)), map_sInf' := ⋯, map_sSup' := ⋯ }) =
    𝟙 α
have h : ∀ (a : (↑α : Type u)),
  Eq (α := (↑α : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompleteLat.{u}) ↦ CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u))
            (CC := carrier) (X := α) (Y := α)
            (CategoryStruct.comp (Y := β)
              (ConcreteCategory.ofHom (FC := fun (x1 x2 : CompleteLat.{u}) ↦
                CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u)) (CC := carrier)
                { toFun := (⇑e : (a : (↑α : Type u)) → (↑β : Type u)), map_sInf' := sorry, map_sSup' := sorry })
              (ConcreteCategory.ofHom (FC := fun (x1 x2 : CompleteLat.{u}) ↦
                CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u)) (CC := carrier)
                { toFun := (⇑e.symm : (a : (↑β : Type u)) → (↑α : Type u)), map_sInf' := sorry, map_sSup' := sorry })) :
          (a : (↑α : Type u)) → (↑α : Type u))
        a :
      (↑α : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompleteLat.{u}) ↦ CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u))
            (CC := carrier) (𝟙 α) :
          (a : (↑α : Type u)) → (↑α : Type u))
        a :
      (↑α : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Category.CompleteLat (goal)
Goal:
α β : CompleteLat
e : (↑α : Type u) ≃o (↑β : Type u)
⊢ CategoryStruct.comp (Y := α)
      (ConcreteCategory.ofHom (FC := fun (x1 x2 : CompleteLat.{u}) ↦ CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u))
        (CC := carrier) { toFun := (⇑e.symm : (a : (↑β : Type u)) → (↑α : Type u)), map_sInf' := ⋯, map_sSup' := ⋯ })
      (ConcreteCategory.ofHom (FC := fun (x1 x2 : CompleteLat.{u}) ↦ CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u))
        (CC := carrier) { toFun := (⇑e : (a : (↑α : Type u)) → (↑β : Type u)), map_sInf' := ⋯, map_sSup' := ⋯ }) =
    𝟙 β
have h : ∀ (a : (↑β : Type u)),
  Eq (α := (↑β : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompleteLat.{u}) ↦ CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u))
            (CC := carrier) (X := β) (Y := β)
            (CategoryStruct.comp (Y := α)
              (ConcreteCategory.ofHom (FC := fun (x1 x2 : CompleteLat.{u}) ↦
                CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u)) (CC := carrier)
                { toFun := (⇑e.symm : (a : (↑β : Type u)) → (↑α : Type u)), map_sInf' := sorry, map_sSup' := sorry })
              (ConcreteCategory.ofHom (FC := fun (x1 x2 : CompleteLat.{u}) ↦
                CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u)) (CC := carrier)
                { toFun := (⇑e : (a : (↑α : Type u)) → (↑β : Type u)), map_sInf' := sorry, map_sSup' := sorry })) :
          (a : (↑β : Type u)) → (↑β : Type u))
        a :
      (↑β : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompleteLat.{u}) ↦ CompleteLatticeHom (↑x1 : Type u) (↑x2 : Type u))
            (CC := carrier) (𝟙 β) :
          (a : (↑β : Type u)) → (↑β : Type u))
        a :
      (↑β : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Category.FinBddDistLat (goal)
Goal:
α β : FinBddDistLat
e : (↑α.toDistLat : Type u) ≃o (↑β.toDistLat : Type u)
⊢ CategoryStruct.comp (Y := β)
      (ofHom
        (let __src : LatticeHom (↑α.1.1 : Type u) (↑β.1.1 : Type u) :=
          { toFun := (⇑e : (a : (↑α.1.1 : Type u)) → (↑β.1.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := (⇑e : (a : (↑α.1.1 : Type u)) → (↑β.1.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯,
          map_bot' := ⋯ }))
      (ofHom
        (let __src : LatticeHom (↑β.1.1 : Type u) (↑α.1.1 : Type u) :=
          { toFun := (⇑e.symm : (a : (↑β.1.1 : Type u)) → (↑α.1.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := (⇑e.symm : (a : (↑β.1.1 : Type u)) → (↑α.1.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯,
          map_bot' := ⋯ })) =
    𝟙 α
have hf : ∀ (a : (↑α.toDistLat : Type u)),
  Eq (α := (↑α.toDistLat : Type u))
    ((Hom.hom
            (CategoryStruct.comp (Y := β)
              (ofHom
                (let __src : LatticeHom (↑α.1.1 : Type u) (↑β.1.1 : Type u) :=
                  { toFun := (⇑e : (a : (↑α.1.1 : Type u)) → (↑β.1.1 : Type u)), map_sup' := sorry, map_inf' := sorry };
                { toFun := (⇑e : (a : (↑α.1.1 : Type u)) → (↑β.1.1 : Type u)), map_sup' := sorry, map_inf' := sorry,
                  map_top' := sorry, map_bot' := sorry }))
              (ofHom
                (let __src : LatticeHom (↑β.1.1 : Type u) (↑α.1.1 : Type u) :=
                  { toFun := (⇑e.symm : (a : (↑β.1.1 : Type u)) → (↑α.1.1 : Type u)), map_sup' := sorry, map_inf' := sorry };
                { toFun := (⇑e.symm : (a : (↑β.1.1 : Type u)) → (↑α.1.1 : Type u)), map_sup' := sorry, map_inf' := sorry,
                  map_top' := sorry, map_bot' := sorry }))) :
          (a : (↑α.toDistLat : Type u)) → (↑α.toDistLat : Type u))
        a :
      (↑α.toDistLat : Type u))
    ((Hom.hom (𝟙 α) : (a : (↑α.toDistLat : Type u)) → (↑α.toDistLat : Type u)) a : (↑α.toDistLat : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Category.FinBddDistLat (goal)
Goal:
α β : FinBddDistLat
e : (↑α.toDistLat : Type u) ≃o (↑β.toDistLat : Type u)
⊢ CategoryStruct.comp (Y := α)
      (ofHom
        (let __src : LatticeHom (↑β.1.1 : Type u) (↑α.1.1 : Type u) :=
          { toFun := (⇑e.symm : (a : (↑β.1.1 : Type u)) → (↑α.1.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := (⇑e.symm : (a : (↑β.1.1 : Type u)) → (↑α.1.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯,
          map_bot' := ⋯ }))
      (ofHom
        (let __src : LatticeHom (↑α.1.1 : Type u) (↑β.1.1 : Type u) :=
          { toFun := (⇑e : (a : (↑α.1.1 : Type u)) → (↑β.1.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := (⇑e : (a : (↑α.1.1 : Type u)) → (↑β.1.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯,
          map_bot' := ⋯ })) =
    𝟙 β
have hf : ∀ (a : (↑β.toDistLat : Type u)),
  Eq (α := (↑β.toDistLat : Type u))
    ((Hom.hom
            (CategoryStruct.comp (Y := α)
              (ofHom
                (let __src : LatticeHom (↑β.1.1 : Type u) (↑α.1.1 : Type u) :=
                  { toFun := (⇑e.symm : (a : (↑β.1.1 : Type u)) → (↑α.1.1 : Type u)), map_sup' := sorry, map_inf' := sorry };
                { toFun := (⇑e.symm : (a : (↑β.1.1 : Type u)) → (↑α.1.1 : Type u)), map_sup' := sorry, map_inf' := sorry,
                  map_top' := sorry, map_bot' := sorry }))
              (ofHom
                (let __src : LatticeHom (↑α.1.1 : Type u) (↑β.1.1 : Type u) :=
                  { toFun := (⇑e : (a : (↑α.1.1 : Type u)) → (↑β.1.1 : Type u)), map_sup' := sorry, map_inf' := sorry };
                { toFun := (⇑e : (a : (↑α.1.1 : Type u)) → (↑β.1.1 : Type u)), map_sup' := sorry, map_inf' := sorry,
                  map_top' := sorry, map_bot' := sorry }))) :
          (a : (↑β.toDistLat : Type u)) → (↑β.toDistLat : Type u))
        a :
      (↑β.toDistLat : Type u))
    ((Hom.hom (𝟙 β) : (a : (↑β.toDistLat : Type u)) → (↑β.toDistLat : Type u)) a : (↑β.toDistLat : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Category.FinBoolAlg (goal)
Goal:
X Y : FinBoolAlg
a₁ a₂ : X ⟶ Y
h :
  Eq (α :=
    Functor.obj
        (forget₂ FinBoolAlg (FC := fun (x1 x2 : FinBoolAlg.{u_1}) ↦
          BoundedLatticeHom (↑x1.toBoolAlg : Type u_1) (↑x2.toBoolAlg : Type u_1)) (CC := fun (X : FinBoolAlg.{u_1}) ↦
          (↑X.toBoolAlg : Type u_1)) FinPartOrd (FD := fun (x1 x2 : FinPartOrd.{u_1}) ↦
          (↑x1.toPartOrd : Type u_1) →o (↑x2.toPartOrd : Type u_1)) (CD := fun (X : FinPartOrd.{u_1}) ↦
          (↑X.toPartOrd : Type u_1)))
        X ⟶
      Functor.obj
        (forget₂ FinBoolAlg (FC := fun (x1 x2 : FinBoolAlg.{u_1}) ↦
          BoundedLatticeHom (↑x1.toBoolAlg : Type u_1) (↑x2.toBoolAlg : Type u_1)) (CC := fun (X : FinBoolAlg.{u_1}) ↦
          (↑X.toBoolAlg : Type u_1)) FinPartOrd (FD := fun (x1 x2 : FinPartOrd.{u_1}) ↦
          (↑x1.toPartOrd : Type u_1) →o (↑x2.toPartOrd : Type u_1)) (CD := fun (X : FinPartOrd.{u_1}) ↦
          (↑X.toPartOrd : Type u_1)))
        Y)
    (CategoryTheory.Functor.map
      (forget₂ FinBoolAlg (FC := fun (x1 x2 : FinBoolAlg.{u_1}) ↦
        BoundedLatticeHom (↑x1.toBoolAlg : Type u_1) (↑x2.toBoolAlg : Type u_1)) (CC := fun (X : FinBoolAlg.{u_1}) ↦
        (↑X.toBoolAlg : Type u_1)) FinPartOrd (FD := fun (x1 x2 : FinPartOrd.{u_1}) ↦
        (↑x1.toPartOrd : Type u_1) →o (↑x2.toPartOrd : Type u_1)) (CD := fun (X : FinPartOrd.{u_1}) ↦
        (↑X.toPartOrd : Type u_1)))
      a₁)
    (CategoryTheory.Functor.map
      (forget₂ FinBoolAlg (FC := fun (x1 x2 : FinBoolAlg.{u_1}) ↦
        BoundedLatticeHom (↑x1.toBoolAlg : Type u_1) (↑x2.toBoolAlg : Type u_1)) (CC := fun (X : FinBoolAlg.{u_1}) ↦
        (↑X.toBoolAlg : Type u_1)) FinPartOrd (FD := fun (x1 x2 : FinPartOrd.{u_1}) ↦
        (↑x1.toPartOrd : Type u_1) →o (↑x2.toPartOrd : Type u_1)) (CD := fun (X : FinPartOrd.{u_1}) ↦
        (↑X.toPartOrd : Type u_1)))
      a₂)
⊢ a₁ = a₂
have h₁ : ∀ (x : (↑X.toBoolAlg : Type u_1)),
  Eq (α := (↑Y.toBoolAlg : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : FinBoolAlg.{u_1}) ↦
            BoundedLatticeHom (↑x1.toBoolAlg : Type u_1) (↑x2.toBoolAlg : Type u_1)) (CC := fun (X : FinBoolAlg.{u_1}) ↦
            (↑X.toBoolAlg : Type u_1)) a₁ :
          (a : (↑X.toBoolAlg : Type u_1)) → (↑Y.toBoolAlg : Type u_1))
        x :
      (↑Y.toBoolAlg : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : FinBoolAlg.{u_1}) ↦
            BoundedLatticeHom (↑x1.toBoolAlg : Type u_1) (↑x2.toBoolAlg : Type u_1)) (CC := fun (X : FinBoolAlg.{u_1}) ↦
            (↑X.toBoolAlg : Type u_1)) a₂ :
          (a : (↑X.toBoolAlg : Type u_1)) → (↑Y.toBoolAlg : Type u_1))
        x :
      (↑Y.toBoolAlg : Type u_1))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Category.FinBoolAlg (goal)
Goal:
α β : FinBoolAlg
e : (↑α.toBoolAlg : Type u) ≃o (↑β.toBoolAlg : Type u)
⊢ CategoryStruct.comp (Y := β)
      (InducedCategory.homMk
        (BoolAlg.ofHom
          (let __src : LatticeHom (↑α.1 : Type u) (↑β.1 : Type u) :=
            { toFun := (⇑e : (a : (↑α.1 : Type u)) → (↑β.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯ };
          { toFun := (⇑e : (a : (↑α.1 : Type u)) → (↑β.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯,
            map_bot' := ⋯ })))
      (InducedCategory.homMk
        (BoolAlg.ofHom
          (let __src : LatticeHom (↑β.1 : Type u) (↑α.1 : Type u) :=
            { toFun := (⇑e.symm : (a : (↑β.1 : Type u)) → (↑α.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯ };
          { toFun := (⇑e.symm : (a : (↑β.1 : Type u)) → (↑α.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯,
            map_bot' := ⋯ }))) =
    𝟙 α
have h : ∀ (a : (↑α.toBoolAlg : Type u)),
  Eq (α := (↑α.toBoolAlg : Type u))
    ((@ConcreteCategory.hom FinBoolAlg largeCategory
            (fun (x1 x2 : FinBoolAlg.{u}) ↦ BoundedLatticeHom (↑x1.toBoolAlg : Type u) (↑x2.toBoolAlg : Type u))
            (fun (X : FinBoolAlg.{u}) ↦ (↑X.toBoolAlg : Type u)) _ _ α α
            (CategoryStruct.comp (Y := β)
              (InducedCategory.homMk
                (BoolAlg.ofHom
                  (let __src : LatticeHom (↑α.1 : Type u) (↑β.1 : Type u) :=
                    { toFun := (⇑e : (a : (↑α.1 : Type u)) → (↑β.1 : Type u)), map_sup' := sorry, map_inf' := sorry };
                  { toFun := (⇑e : (a : (↑α.1 : Type u)) → (↑β.1 : Type u)), map_sup' := sorry, map_inf' := sorry,
                    map_top' := sorry, map_bot' := sorry })))
              (InducedCategory.homMk
                (BoolAlg.ofHom
                  (let __src : LatticeHom (↑β.1 : Type u) (↑α.1 : Type u) :=
                    { toFun := (⇑e.symm : (a : (↑β.1 : Type u)) → (↑α.1 : Type u)), map_sup' := sorry, map_inf' := sorry };
                  { toFun := (⇑e.symm : (a : (↑β.1 : Type u)) → (↑α.1 : Type u)), map_sup' := sorry, map_inf' := sorry,
                    map_top' := sorry, map_bot' := sorry })))) :
          (a : (↑α.toBoolAlg : Type u)) → (↑α.toBoolAlg : Type u))
        a :
      (↑α.toBoolAlg : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : FinBoolAlg.{u}) ↦
            BoundedLatticeHom (↑x1.toBoolAlg : Type u) (↑x2.toBoolAlg : Type u)) (CC := fun (X : FinBoolAlg.{u}) ↦
            (↑X.toBoolAlg : Type u)) (𝟙 α) :
          (a : (↑α.toBoolAlg : Type u)) → (↑α.toBoolAlg : Type u))
        a :
      (↑α.toBoolAlg : Type u))
Tactic: ext