awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ bot x f
z : α
hz : z ∈ bot x f
h : y ≠ z
rw :
  ∀ (hy : IsExtremePt x f y) ⦃z : α⦄ (hz : z ∈ bot x f),
    y ≠ z → (fun (x1 x2 : α) ↦ x1 ≤ x2) y z ∨ (fun (x1 x2 : α) ↦ x1 ≤ x2) z y
⊢ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z ∨ (fun (x1 x2 : α) ↦ x1 ≤ x2) z y

Tactic:
rw [mem_bot_iff_isExtremePt le_map] at hy

Premises used: ChainCompletePartialOrder.IsExtremePt.mem_bot_iff_isExtremePt
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : IsExtremePt x f y
z : α
hz : z ∈ bot x f
h : y ≠ z
⊢ Membership.mem (γ := Set α) {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} z

Tactic:
rw [← bot_eq_of_le_or_map_le le_map hy] at hz

Premises used: ChainCompletePartialOrder.IsExtremePt.bot_eq_of_le_or_map_le
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : IsExtremePt x f y
z : α
hz : z ∈ bot x f
h : y ≠ z
hz₁ : Membership.mem (γ := Set α) {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} z
⊢ y ≠ z

Tactic:
rw [← bot_eq_of_le_or_map_le le_map hy] at hz

Premises used: ChainCompletePartialOrder.IsExtremePt.bot_eq_of_le_or_map_le
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : IsExtremePt x f y
z : α
hz : Membership.mem (γ := Set α) {z : α | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} z
h : y ≠ z
inl : z ∈ bot x f → ∀ (hz : z ≤ y), (fun (x1 x2 : α) ↦ x1 ≤ x2) y z ∨ (fun (x1 x2 : α) ↦ x1 ≤ x2) z y
inr : z ∈ bot x f → ∀ (hz : f y ≤ z), (fun (x1 x2 : α) ↦ x1 ≤ x2) y z ∨ (fun (x1 x2 : α) ↦ x1 ≤ x2) z y
⊢ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z ∨ (fun (x1 x2 : α) ↦ x1 ≤ x2) z y

Tactic:
obtain ⟨_, (hz | hz)⟩ := hz
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : IsExtremePt x f y
z : α
h : y ≠ z
left : z ∈ bot x f
hz : z ≤ y
inl : (fun (x1 x2 : α) ↦ x1 ≤ x2) z y
⊢ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z ∨ (fun (x1 x2 : α) ↦ x1 ≤ x2) z y

Tactic:
right
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : IsExtremePt x f y
z : α
h : y ≠ z
left : z ∈ bot x f
hz : z ≤ y
⊢ (fun (x1 x2 : α) ↦ x1 ≤ x2) z y

Tactic:
hz
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : IsExtremePt x f y
z : α
h : y ≠ z
left : z ∈ bot x f
hz : z ≤ y
⊢ (fun (x1 x2 : α) ↦ x1 ≤ x2) z y

Tactic:
exact hz
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : IsExtremePt x f y
z : α
h : y ≠ z
left : z ∈ bot x f
hz : f y ≤ z
inr : (fun (x1 x2 : α) ↦ x1 ≤ x2) y z
⊢ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z ∨ (fun (x1 x2 : α) ↦ x1 ≤ x2) z y

Tactic:
left
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : IsExtremePt x f y
z : α
h : y ≠ z
left : z ∈ bot x f
hz : f y ≤ z
⊢ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z

Tactic:
le_trans (le_map y) hz

Premises used: le_trans
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : IsExtremePt x f y
z : α
h : y ≠ z
left : z ∈ bot x f
hz : f y ≤ z
⊢ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z

Tactic:
exact le_trans (le_map y) hz

Premises used: le_trans
-- Module: Mathlib.Order.BourbakiWitt
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 α }
h : y ∈ fixedPoints f
⊢ (fixedPoints f).Nonempty

Tactic:
use y
-- Module: Mathlib.Order.BourbakiWitt
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 α }
apply : f y ∈ bot x f
⊢ y ∈ fixedPoints f

Tactic:
apply le_antisymm (le_cSup _ _ (_ : f y ∈ bot x f)) (le_map y)

Premises used: ChainCompletePartialOrder.le_cSup, le_antisymm
-- Module: Mathlib.Order.BourbakiWitt
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 α }
a : f y ∈ f '' bot x f
⊢ f y ∈ bot x f

Tactic:
apply (bot_isAdmissible le_map).image_self_subset_self

Premises used: ChainCompletePartialOrder.bot_isAdmissible, ChainCompletePartialOrder.IsAdmissible.image_self_subset_self
-- Module: Mathlib.Order.BourbakiWitt
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 α }
h : y ∈ bot x f ∧ f y = f y
⊢ f y ∈ f '' bot x f

Tactic:
use y
-- Module: Mathlib.Order.BourbakiWitt
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 ∈ bot x f ∧ f y = f y

Tactic:
⟨(bot_isAdmissible le_map).cSup_mem _ (subset_refl _), rfl⟩

Premises used: subset_refl, ChainCompletePartialOrder.bot_isAdmissible, ChainCompletePartialOrder.IsAdmissible.cSup_mem, And.intro, rfl
-- Module: Mathlib.Order.BourbakiWitt
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 ∈ bot x f ∧ f y = f y

Tactic:
exact ⟨(bot_isAdmissible le_map).cSup_mem _ (subset_refl _), rfl⟩
-- Module: Mathlib.Order.BourbakiWitt
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)

Tactic:
ωScottContinuous.of_monotone_map_ωSup
    ⟨Monotone.iSup fun i ↦ (hf i).monotone, fun c ↦ eq_of_forall_ge_iff fun a ↦ ?_⟩

Premises used: eq_of_forall_ge_iff, OmegaCompletePartialOrder.ωScottContinuous.monotone, Exists.intro, OmegaCompletePartialOrder.ωScottContinuous.of_monotone_map_ωSup, Monotone.iSup
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_3
inst : OmegaCompletePartialOrder α
inst_1 : CompleteLattice β
f : ι → α → β
hf : ∀ (i : ι), ωScottContinuous (f i)
refine :
  ∀ (c : Chain α) (a : β), (⨆ (i : ι), f i) (ωSup c) ≤ a ↔ ωSup (c.map { toFun := ⨆ (i : ι), f i, monotone' := ⋯ }) ≤ a
⊢ ωScottContinuous.{u_1, u_2} (α := α) (β := β) (⨆ (i : ι), f i)

Tactic:
refine ωScottContinuous.of_monotone_map_ωSup
    ⟨Monotone.iSup fun i ↦ (hf i).monotone, fun c ↦ eq_of_forall_ge_iff fun a ↦ ?_⟩

Premises used: eq_of_forall_ge_iff, OmegaCompletePartialOrder.ωScottContinuous.monotone, Exists.intro, OmegaCompletePartialOrder.ωScottContinuous.of_monotone_map_ωSup, Monotone.iSup
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_3
inst : OmegaCompletePartialOrder α
inst_1 : CompleteLattice β
f : ι → α → β
hf : ∀ (i : ι), ωScottContinuous (f i)
c : Chain α
a : β
⊢ (⨆ (i : ι), f i) (ωSup c) ≤ a ↔ ωSup (c.map { toFun := ⨆ (i : ι), f i, monotone' := ⋯ }) ≤ a

Tactic:
simp +contextual [ωSup_le_iff, (hf _).map_ωSup, @forall_comm ι]

Premises used: OmegaCompletePartialOrder.ωSup_le_iff, forall_comm, OmegaCompletePartialOrder.ωScottContinuous.map_ωSup
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
β : Type u_2
inst : OmegaCompletePartialOrder α
inst_1 : CompleteLattice β
s : Set (α → β)
hs : ∀ f ∈ s, ωScottContinuous f
rw : ωScottContinuous.{u_1, u_2} (α := α) (β := β) (⨆ a ∈ s, a)
⊢ ωScottContinuous (SupSet.sSup s)

Tactic:
rw [sSup_eq_iSup]

Premises used: sSup_eq_iSup
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
β : Type u_2
inst : OmegaCompletePartialOrder α
inst_1 : CompleteLattice β
s : Set (α → β)
hs : ∀ f ∈ s, ωScottContinuous f
⊢ ωScottContinuous.{u_1, u_2} (α := α) (β := β) (⨆ a ∈ s, a)

Tactic:
apply ωScottContinuous.iSup fun f ↦ ωScottContinuous.iSup <| hs f

Premises used: CompleteLattice.ωScottContinuous.iSup
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
β : Type u_2
inst : OmegaCompletePartialOrder α
inst_1 : CompleteLattice β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
rw : ωScottContinuous.{u_1, u_2} (α := α) (β := β) (SupSet.sSup {f, g})
⊢ ωScottContinuous (f ⊔ g)

Tactic:
rw [← sSup_pair]

Premises used: sSup_pair
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
β : Type u_2
inst : OmegaCompletePartialOrder α
inst_1 : CompleteLattice β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
hs : ∀ (f_1 : α → β), Membership.mem (γ := Set (α → β)) {f, g} f_1 → ωScottContinuous f_1
⊢ ωScottContinuous.{u_1, u_2} (α := α) (β := β) (SupSet.sSup {f, g})

Tactic:
apply ωScottContinuous.sSup

Premises used: CompleteLattice.ωScottContinuous.sSup
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
β : Type u_2
inst : OmegaCompletePartialOrder α
inst_1 : CompleteLattice β
g : α → β
hg : ωScottContinuous g
f : α → β
hf : ωScottContinuous f
⊢ ωScottContinuous f

Tactic:
assumption
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
β : Type u_2
inst : OmegaCompletePartialOrder α
inst_1 : CompleteLattice β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
⊢ ωScottContinuous g

Tactic:
assumption
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
β : Type u_2
inst : OmegaCompletePartialOrder α
inst_1 : CompleteLattice β
c : Chain α
a : β
⊢ ⊤ (ωSup c) ≤ a ↔ ωSup (c.map { toFun := ⊤, monotone' := ⋯ }) ≤ a

Tactic:
simp
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
β : Type u_2
inst : OmegaCompletePartialOrder α
inst_1 : CompleteLattice β
rw : ωScottContinuous.{u_1, u_2} (α := α) (β := β) (SupSet.sSup ∅)
⊢ ωScottContinuous.{u_1, u_2} (α := α) (β := β) ⊥

Tactic:
rw [← sSup_empty]

Premises used: sSup_empty
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
β : Type u_2
inst : OmegaCompletePartialOrder α
inst_1 : CompleteLattice β
⊢ ∀ (f : α → β), Membership.mem (γ := Set (α → β)) ∅ f → ωScottContinuous f

Tactic:
simp
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
β : Type u_2
inst : OmegaCompletePartialOrder α
inst_1 : CompleteLattice β
⊢ ωScottContinuous.{u_1, u_2} (α := α) (β := β) (SupSet.sSup ∅)

Tactic:
exact ωScottContinuous.sSup (by simp)

Premises used: CompleteLattice.ωScottContinuous.sSup
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
β : Type u_2
inst : OmegaCompletePartialOrder α
inst_1 : CompleteLinearOrder β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
⊢ ωScottContinuous (f ⊓ g)

Tactic:
ωScottContinuous.of_monotone_map_ωSup
    ⟨hf.monotone.inf hg.monotone, fun c ↦ eq_of_forall_ge_iff fun a ↦ ?_⟩

Premises used: eq_of_forall_ge_iff, OmegaCompletePartialOrder.ωScottContinuous.monotone, Exists.intro, OmegaCompletePartialOrder.ωScottContinuous.of_monotone_map_ωSup, Monotone.inf
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
β : Type u_2
inst : OmegaCompletePartialOrder α
inst_1 : CompleteLinearOrder β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
refine : ∀ (c : Chain α) (a : β), (f ⊓ g) (ωSup c) ≤ a ↔ ωSup (c.map { toFun := f ⊓ g, monotone' := ⋯ : α →o β }) ≤ a
⊢ ωScottContinuous (f ⊓ g)

Tactic:
refine ωScottContinuous.of_monotone_map_ωSup
    ⟨hf.monotone.inf hg.monotone, fun c ↦ eq_of_forall_ge_iff fun a ↦ ?_⟩

Premises used: eq_of_forall_ge_iff, OmegaCompletePartialOrder.ωScottContinuous.monotone, Exists.intro, OmegaCompletePartialOrder.ωScottContinuous.of_monotone_map_ωSup, Monotone.inf
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
β : Type u_2
inst : OmegaCompletePartialOrder α
inst_1 : CompleteLinearOrder β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
c : Chain α
a : β
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
⊢ (f ⊓ g) (ωSup c) ≤ a ↔ ωSup (c.map { toFun := f ⊓ g, monotone' := ⋯ : α →o β }) ≤ 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]

Premises used: OmegaCompletePartialOrder.Chain.coe_map, OmegaCompletePartialOrder.ωSup_le_iff, inf_le_iff, Function.comp, OmegaCompletePartialOrder.ωScottContinuous.map_ωSup, forall_or_right, OrderHom.coe_mk, forall_or_left, Pi.inf_apply
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
β : Type u_2
inst : OmegaCompletePartialOrder α
inst_1 : CompleteLinearOrder β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
c : Chain α
a : β
⊢ (∀ (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:
⟨fun h _ ↦ h _ _, fun h i j ↦
    (h (max j i)).imp (le_trans <| hf.monotone <| c.mono <| le_max_left _ _)
      (le_trans <| hg.monotone <| c.mono <| le_max_right _ _)⟩

Premises used: le_max_right, OrderHom.mono, Max.max, OmegaCompletePartialOrder.ωScottContinuous.monotone, Iff.intro, Or.imp, le_max_left, OmegaCompletePartialOrder.Chain.toOrderHom, le_trans
-- Module: Mathlib.Order.BourbakiWitt
Goal:
α : Type u_1
β : Type u_2
inst : OmegaCompletePartialOrder α
inst_1 : CompleteLinearOrder β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
c : Chain α
a : β
⊢ (∀ (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:
exact ⟨fun h _ ↦ h _ _, fun h i j ↦
    (h (max j i)).imp (le_trans <| hf.monotone <| c.mono <| le_max_left _ _)
      (le_trans <| hg.monotone <| c.mono <| le_max_right _ _)⟩
-- Module: Mathlib.Order.Category.BddDistLat
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
⊢ (↑(of α).toDistLat : Type u_1) = α

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.BddDistLat
Goal:
X : BddDistLat
⊢ Eq (α :=
    (a : (fun (X : BddDistLat.{u_1}) ↦ (↑X.toDistLat : Type u_1)) X) →
      (fun (X : BddDistLat.{u_1}) ↦ (↑X.toDistLat : Type u_1)) X)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : BddDistLat.{u_1}) ↦
          BoundedLatticeHom (↑x1.toDistLat : Type u_1) (↑x2.toDistLat : Type u_1)) (CC := fun (X : BddDistLat.{u_1}) ↦
          (↑X.toDistLat : Type u_1)) (𝟙 X)) :
      (a : (fun (X : BddDistLat) ↦ (↑X.toDistLat : Type u_1)) X) → (fun (X : BddDistLat) ↦ (↑X.toDistLat : Type u_1)) X)
    id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.BddDistLat
Goal:
X Y Z : BddDistLat
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α :=
    (a : (fun (X : BddDistLat.{u_1}) ↦ (↑X.toDistLat : Type u_1)) X) →
      (fun (X : BddDistLat.{u_1}) ↦ (↑X.toDistLat : Type u_1)) Z)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : BddDistLat.{u_1}) ↦
          BoundedLatticeHom (↑x1.toDistLat : Type u_1) (↑x2.toDistLat : Type u_1)) (CC := fun (X : BddDistLat.{u_1}) ↦
          (↑X.toDistLat : Type u_1)) (f ≫ g)) :
      (a : (fun (X : BddDistLat) ↦ (↑X.toDistLat : Type u_1)) X) → (fun (X : BddDistLat) ↦ (↑X.toDistLat : Type u_1)) Z)
    (Function.comp (β := (fun (X : BddDistLat.{u_1}) ↦ (↑X.toDistLat : Type u_1)) Y)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : BddDistLat.{u_1}) ↦
            BoundedLatticeHom (↑x1.toDistLat : Type u_1) (↑x2.toDistLat : Type u_1)) (CC := fun (X : BddDistLat.{u_1}) ↦
            (↑X.toDistLat : Type u_1)) g) :
        (a : (fun (X : BddDistLat) ↦ (↑X.toDistLat : Type u_1)) Y) →
          (fun (X : BddDistLat) ↦ (↑X.toDistLat : Type u_1)) Z)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : BddDistLat.{u_1}) ↦
            BoundedLatticeHom (↑x1.toDistLat : Type u_1) (↑x2.toDistLat : Type u_1)) (CC := fun (X : BddDistLat.{u_1}) ↦
            (↑X.toDistLat : Type u_1)) f) :
        (a : (fun (X : BddDistLat) ↦ (↑X.toDistLat : Type u_1)) X) →
          (fun (X : BddDistLat) ↦ (↑X.toDistLat : Type u_1)) Y))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.BddDistLat
Goal:
X Y : BddDistLat
f : X ⟶ Y
⊢ Eq (α :=
    (a :
        (fun (X : Type u_1) ↦ X)
          (Functor.obj
            (forget BddDistLat (FC := fun (x1 x2 : BddDistLat.{u_1}) ↦
              BoundedLatticeHom (↑x1.toDistLat : Type u_1) (↑x2.toDistLat : Type u_1)) (CC :=
              fun (X : BddDistLat.{u_1}) ↦ (↑X.toDistLat : Type u_1)))
            X)) →
      (fun (X : Type u_1) ↦ X)
        (Functor.obj
          (forget BddDistLat (FC := fun (x1 x2 : BddDistLat.{u_1}) ↦
            BoundedLatticeHom (↑x1.toDistLat : Type u_1) (↑x2.toDistLat : Type u_1)) (CC := fun (X : BddDistLat.{u_1}) ↦
            (↑X.toDistLat : Type u_1)))
          Y))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map
            (forget BddDistLat (FC := fun (x1 x2 : BddDistLat.{u_1}) ↦
              BoundedLatticeHom (↑x1.toDistLat : Type u_1) (↑x2.toDistLat : Type u_1)) (CC :=
              fun (X : BddDistLat.{u_1}) ↦ (↑X.toDistLat : Type u_1)))
            f)) :
      (a : (fun (X : Type u_1) ↦ X) ((forget BddDistLat).obj X)) → (fun (X : Type u_1) ↦ X) ((forget BddDistLat).obj Y))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : BddDistLat.{u_1}) ↦
          BoundedLatticeHom (↑x1.toDistLat : Type u_1) (↑x2.toDistLat : Type u_1)) (CC := fun (X : BddDistLat.{u_1}) ↦
          (↑X.toDistLat : Type u_1)) f) :
      (a : (fun (X : BddDistLat) ↦ (↑X.toDistLat : Type u_1)) X) → (fun (X : BddDistLat) ↦ (↑X.toDistLat : Type u_1)) Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.BddDistLat
Goal:
X Y : BddDistLat
f g : X ⟶ Y
w :
  ∀ (x : (↑X.toDistLat : Type u_1)),
    Eq (α := (fun (X : BddDistLat.{u_1}) ↦ (↑X.toDistLat : Type u_1)) Y)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : BddDistLat.{u_1}) ↦
              BoundedLatticeHom (↑x1.toDistLat : Type u_1) (↑x2.toDistLat : Type u_1)) (CC :=
              fun (X : BddDistLat.{u_1}) ↦ (↑X.toDistLat : Type u_1)) f :
            (a : (fun (X : BddDistLat) ↦ (↑X.toDistLat : Type u_1)) X) →
              (fun (X : BddDistLat) ↦ (↑X.toDistLat : Type u_1)) Y)
          x :
        (fun (X : BddDistLat.{u_1}) ↦ (↑X.toDistLat : Type u_1)) Y)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : BddDistLat.{u_1}) ↦
              BoundedLatticeHom (↑x1.toDistLat : Type u_1) (↑x2.toDistLat : Type u_1)) (CC :=
              fun (X : BddDistLat.{u_1}) ↦ (↑X.toDistLat : Type u_1)) g :
            (a : (fun (X : BddDistLat) ↦ (↑X.toDistLat : Type u_1)) X) →
              (fun (X : BddDistLat) ↦ (↑X.toDistLat : Type u_1)) Y)
          x :
        (fun (X : BddDistLat.{u_1}) ↦ (↑X.toDistLat : Type u_1)) Y)
⊢ f = g

Tactic:
ConcreteCategory.hom_ext _ _ w

Premises used: CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.Order.Category.BddDistLat
Goal:
X : BddDistLat
⊢ Hom.hom (𝟙 X) = BoundedLatticeHom.id (↑X.toDistLat : Type u_1)

Tactic:
rfl

Premises used: BoundedLatticeHom.id, rfl
-- Module: Mathlib.Order.Category.BddDistLat
Goal:
X : BddDistLat
x : (↑X.toDistLat : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : BddDistLat.{u_1}) ↦
          BoundedLatticeHom (↑x1.toDistLat : Type u_1) (↑x2.toDistLat : Type u_1)) (CC := fun (X : BddDistLat.{u_1}) ↦
          (↑X.toDistLat : Type u_1)) (𝟙 X) :
        (a : (fun (X : BddDistLat) ↦ (↑X.toDistLat : Type u_1)) X) →
          (fun (X : BddDistLat) ↦ (↑X.toDistLat : Type u_1)) X)
      x =
    x

Tactic:
simp
-- Module: Mathlib.Order.Category.BddDistLat
Goal:
X Y Z : BddDistLat
f : X ⟶ Y
g : Y ⟶ Z
⊢ Hom.hom (f ≫ g) = (Hom.hom g).comp (Hom.hom f)

Tactic:
rfl

Premises used: BoundedLatticeHom.comp, rfl
-- Module: Mathlib.Order.Category.BddDistLat
Goal:
X Y Z : BddDistLat
f : X ⟶ Y
g : Y ⟶ Z
x : (↑X.toDistLat : Type u_1)
⊢ Eq (α := (fun (X : BddDistLat.{u_1}) ↦ (↑X.toDistLat : Type u_1)) Z)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : BddDistLat.{u_1}) ↦
            BoundedLatticeHom (↑x1.toDistLat : Type u_1) (↑x2.toDistLat : Type u_1)) (CC := fun (X : BddDistLat.{u_1}) ↦
            (↑X.toDistLat : Type u_1)) (f ≫ g) :
          (a : (fun (X : BddDistLat) ↦ (↑X.toDistLat : Type u_1)) X) →
            (fun (X : BddDistLat) ↦ (↑X.toDistLat : Type u_1)) Z)
        x :
      (fun (X : BddDistLat.{u_1}) ↦ (↑X.toDistLat : Type u_1)) Z)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : BddDistLat.{u_1}) ↦
            BoundedLatticeHom (↑x1.toDistLat : Type u_1) (↑x2.toDistLat : Type u_1)) (CC := fun (X : BddDistLat.{u_1}) ↦
            (↑X.toDistLat : Type u_1)) g :
          (a : (fun (X : BddDistLat) ↦ (↑X.toDistLat : Type u_1)) Y) →
            (fun (X : BddDistLat) ↦ (↑X.toDistLat : Type u_1)) Z)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : BddDistLat.{u_1}) ↦
                BoundedLatticeHom (↑x1.toDistLat : Type u_1) (↑x2.toDistLat : Type u_1)) (CC :=
                fun (X : BddDistLat.{u_1}) ↦ (↑X.toDistLat : Type u_1)) f :
              (a : (fun (X : BddDistLat) ↦ (↑X.toDistLat : Type u_1)) X) →
                (fun (X : BddDistLat) ↦ (↑X.toDistLat : Type u_1)) Y)
            x :
          (fun (X : BddDistLat.{u_1}) ↦ (↑X.toDistLat : Type u_1)) Y) :
      (fun (X : BddDistLat.{u_1}) ↦ (↑X.toDistLat : Type u_1)) Z)

Tactic:
simp
-- Module: Mathlib.Order.Category.BddDistLat
Goal:
X Y : BddDistLat
f g : X ⟶ Y
hf : Hom.hom f = Hom.hom g
⊢ f = g

Tactic:
Hom.ext hf

Premises used: BddDistLat.Hom.ext
-- Module: Mathlib.Order.Category.BddDistLat
Goal:
X Y : Type u
inst : DistribLattice X
inst_1 : BoundedOrder X
inst_2 : DistribLattice Y
inst_3 : BoundedOrder Y
f : BoundedLatticeHom X Y
⊢ Hom.hom (ofHom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.BddDistLat
Goal:
X Y : BddDistLat
f : X ⟶ Y
⊢ ofHom (Hom.hom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.BddDistLat
Goal:
X : Type u
inst : DistribLattice X
inst_1 : BoundedOrder X
⊢ ofHom (BoundedLatticeHom.id X) = 𝟙 (of X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.BddDistLat
Goal:
X Y Z : Type u
inst : DistribLattice X
inst_1 : BoundedOrder X
inst_2 : DistribLattice Y
inst_3 : BoundedOrder Y
inst_4 : DistribLattice Z
inst_5 : BoundedOrder Z
f : BoundedLatticeHom X Y
g : BoundedLatticeHom Y Z
⊢ ofHom (g.comp f) = ofHom f ≫ ofHom g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.BddDistLat
Goal:
X Y : Type u
inst : DistribLattice X
inst_1 : BoundedOrder X
inst_2 : DistribLattice Y
inst_3 : BoundedOrder Y
f : BoundedLatticeHom X Y
x : X
⊢ Eq (α := (fun (X : BddDistLat.{u}) ↦ (↑X.toDistLat : Type u)) (of Y))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : BddDistLat.{u}) ↦
            BoundedLatticeHom (↑x1.toDistLat : Type u) (↑x2.toDistLat : Type u)) (CC := fun (X : BddDistLat.{u}) ↦
            (↑X.toDistLat : Type u)) (ofHom f) :
          (a : (fun (X : BddDistLat) ↦ (↑X.toDistLat : Type u)) (of X)) →
            (fun (X : BddDistLat) ↦ (↑X.toDistLat : Type u)) (of Y))
        x :
      (fun (X : BddDistLat.{u}) ↦ (↑X.toDistLat : Type u)) (of Y))
    ((f : (a : X) → Y) x : Y)

Tactic:
rfl

Premises used: rfl