awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
s : Set α
inst : Bornology α
inst_1 : Preorder α
inst_2 : IsOrderBornology α
hs : IsBounded s
⊢ BddAbove s

Tactic:
(isBounded_iff_bddBelow_bddAbove.1 hs).2

Premises used: And.right, Iff.mp, isBounded_iff_bddBelow_bddAbove
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
s : Set α
inst : Bornology α
inst_1 : Preorder α
inst_2 : IsOrderBornology α
hs₀ : BddBelow s
hs₁ : BddAbove s
⊢ IsBounded s

Tactic:
isBounded_iff_bddBelow_bddAbove.2 ⟨hs₀, hs₁⟩

Premises used: Iff.mpr, And.intro, isBounded_iff_bddBelow_bddAbove
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
s : Set α
inst : Bornology α
inst_1 : Preorder α
inst_2 : IsOrderBornology α
hs₀ : BddAbove s
hs₁ : BddBelow s
⊢ IsBounded s

Tactic:
isBounded_iff_bddBelow_bddAbove.2 ⟨hs₁, hs₀⟩

Premises used: Iff.mpr, And.intro, isBounded_iff_bddBelow_bddAbove
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
s t : Set α
inst : Bornology α
inst_1 : Preorder α
inst_2 : IsOrderBornology α
hs : BddBelow s
ht : BddAbove t
⊢ IsBounded (s ∩ t)

Tactic:
(hs.mono inter_subset_left).isBounded <| ht.mono inter_subset_right

Premises used: Set.inter_subset_left, BddBelow.isBounded, BddBelow.mono, Set.inter_subset_right, BddAbove.mono
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
s t : Set α
inst : Bornology α
inst_1 : Preorder α
inst_2 : IsOrderBornology α
hs : BddAbove s
ht : BddBelow t
⊢ IsBounded (s ∩ t)

Tactic:
(hs.mono inter_subset_left).isBounded <| ht.mono inter_subset_right

Premises used: Set.inter_subset_left, BddBelow.mono, Set.inter_subset_right, BddAbove.mono, BddAbove.isBounded
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
s_1 t : Set α
inst : Bornology α
inst_1 : Preorder α
inst_2 : IsOrderBornology α
s : Set αᵒᵈ
rw : IsBounded (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ↔ BddBelow s ∧ BddAbove s
rw₁ :
  IsBounded (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ↔
    BddBelow s ∧ BddBelow (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s)
rw₂ :
  IsBounded (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ↔
    BddAbove (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ∧ BddBelow (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s)
rw₃ :
  BddBelow (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ∧ BddAbove (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ↔
    BddAbove (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ∧ BddBelow (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s)
rw₄ rw₅ :
  BddAbove (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ∧ BddBelow (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ↔
    BddAbove (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ∧ BddBelow (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s)
⊢ IsBounded s ↔ BddBelow s ∧ BddAbove s

Tactic:
rw [← isBounded_preimage_toDual, ← bddBelow_preimage_toDual, ← bddAbove_preimage_toDual,
      isBounded_iff_bddBelow_bddAbove, and_comm]

Premises used: OrderDual.isBounded_preimage_toDual, bddBelow_preimage_toDual, and_comm, isBounded_iff_bddBelow_bddAbove, bddAbove_preimage_toDual
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
s_1 t : Set α
inst : Bornology α
inst_1 : Preorder α
inst_2 : IsOrderBornology α
β : Type u_2
inst_3 : Preorder β
inst_4 : Bornology β
inst_5 : IsOrderBornology β
s : Set (α × β)
rw : IsBounded (fst '' s) ∧ IsBounded (snd '' s) ↔ BddBelow s ∧ BddAbove s
rw₁ : IsBounded (fst '' s) ∧ IsBounded (snd '' s) ↔ (BddBelow (fst '' s) ∧ BddBelow (snd '' s)) ∧ BddAbove s
rw₂ :
  IsBounded (fst '' s) ∧ IsBounded (snd '' s) ↔
    (BddBelow (fst '' s) ∧ BddBelow (snd '' s)) ∧ BddAbove (fst '' s) ∧ BddAbove (snd '' s)
rw₃ :
  IsBounded (fst '' s) ∧ IsBounded (snd '' s) ↔
    (BddBelow (fst '' s) ∧ BddAbove (fst '' s)) ∧ BddBelow (snd '' s) ∧ BddAbove (snd '' s)
rw₄ :
  (BddBelow (fst '' s) ∧ BddAbove (fst '' s)) ∧ IsBounded (snd '' s) ↔
    (BddBelow (fst '' s) ∧ BddAbove (fst '' s)) ∧ BddBelow (snd '' s) ∧ BddAbove (snd '' s)
rw₅ rw₆ :
  (BddBelow (fst '' s) ∧ BddAbove (fst '' s)) ∧ BddBelow (snd '' s) ∧ BddAbove (snd '' s) ↔
    (BddBelow (fst '' s) ∧ BddAbove (fst '' s)) ∧ BddBelow (snd '' s) ∧ BddAbove (snd '' s)
⊢ IsBounded s ↔ BddBelow s ∧ BddAbove s

Tactic:
rw [← isBounded_image_fst_and_snd, bddBelow_prod, bddAbove_prod, and_and_and_comm,
      isBounded_iff_bddBelow_bddAbove, isBounded_iff_bddBelow_bddAbove]

Premises used: bddAbove_prod, bddBelow_prod, Bornology.isBounded_image_fst_and_snd, and_and_and_comm, isBounded_iff_bddBelow_bddAbove
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α_1 : Type u_1
s_1 t : Set α_1
inst : Bornology α_1
inst_1 : Preorder α_1
inst_2 : IsOrderBornology α_1
ι : Type u_2
α : ι → Type u_3
inst_3 : (i : ι) → Preorder (α i)
inst_4 : (i : ι) → Bornology (α i)
inst_5 : ∀ (i : ι), IsOrderBornology.{u_3} (α i)
s : Set ((i : ι) → α i)
simp_rw : (∀ (i : ι), IsBounded (Function.eval (β := α) i '' s)) ↔ BddBelow s ∧ BddAbove s
simp_rw₁ :
  (∀ (i : ι), IsBounded (Function.eval (β := α) i '' s)) ↔
    (∀ (a : ι), BddBelow (Function.eval (β := α) a '' s)) ∧ BddAbove s
simp_rw₂ :
  (∀ (i : ι), IsBounded (Function.eval (β := α) i '' s)) ↔
    (∀ (a : ι), BddBelow (Function.eval (β := α) a '' s)) ∧ ∀ (a : ι), BddAbove (Function.eval (β := α) a '' s)
simp_rw₃ :
  (∀ (i : ι), IsBounded (Function.eval (β := α) i '' s)) ↔
    ∀ (x : ι), BddBelow (Function.eval (β := α) x '' s) ∧ BddAbove (Function.eval (β := α) x '' s)
⊢ IsBounded s ↔ BddBelow s ∧ BddAbove s

Tactic:
simp_rw [← forall_isBounded_image_eval_iff, bddBelow_pi, bddAbove_pi, ← forall_and,
      isBounded_iff_bddBelow_bddAbove]

Premises used: bddAbove_pi, Bornology.forall_isBounded_image_eval_iff, isBounded_iff_bddBelow_bddAbove, bddBelow_pi, forall_and
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
inst_4 : NoMaxOrder α
s : Set α
rw : BddBelow sᶜ ∧ BddAbove sᶜ → ∃ (i : α), True ∧ Ioi i ⊆ s
⊢ s ∈ cobounded α → Membership.mem (γ := Filter α) Filter.atTop s

Tactic:
rw [← compl_compl s, ← isBounded_def, isBounded_iff_bddBelow_bddAbove, compl_compl s,
    Filter.atTop_basis_Ioi.mem_iff]

Premises used: Filter.HasBasis.mem_iff, compl_compl, Bornology.isBounded_def, Filter.atTop_basis_Ioi, isBounded_iff_bddBelow_bddAbove
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
inst_4 : NoMaxOrder α
s : Set α
left : BddBelow sᶜ
b : α
hb : b ∈ upperBounds sᶜ
⊢ Ioi b ⊆ s

Tactic:
rw [mem_upperBounds_iff_subset_Iic, ← compl_compl (Iic b), compl_subset_compl, compl_Iic] at hb

Premises used: compl_compl, mem_upperBounds_iff_subset_Iic, Set.compl_Iic, Set.compl_subset_compl, Set.Iic
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
inst_4 : NoMaxOrder α
s : Set α
left : BddBelow sᶜ
b : α
hb : Ioi b ⊆ s
w : α
h : True ∧ Ioi b ⊆ s
⊢ ∃ (i : α), True ∧ Ioi i ⊆ s

Tactic:
use b
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
inst_4 : NoMinOrder α
⊢ Filter.atBot ≤ cobounded α

Tactic:
atTop_le_cobounded (α := αᵒᵈ)

Premises used: Set.Mem, IsOrderBornology.atTop_le_cobounded, setOf, Set.Iic, OrderDual
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
s : Set α
rw : ((∃ (i : α), True ∧ Iic i ⊆ s) ∧ ∃ (i : α), True ∧ Ici i ⊆ s) → BddBelow sᶜ ∧ BddAbove sᶜ
⊢ Membership.mem (γ := Filter α) (Filter.atBot ⊔ Filter.atTop) s → s ∈ cobounded α

Tactic:
rw [Filter.mem_sup, Filter.atTop_basis.mem_iff, Filter.atBot_basis.mem_iff,
    ← compl_compl s, ← isBounded_def, isBounded_iff_bddBelow_bddAbove, compl_compl s]

Premises used: Filter.atTop_basis, Filter.HasBasis.mem_iff, compl_compl, Filter.atBot_basis, Bornology.isBounded_def, Filter.mem_sup, isBounded_iff_bddBelow_bddAbove
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
s : Set α
b : α
left : True
hb : Iic b ⊆ s
a : α
left_1 : True
ha : Ici a ⊆ s
⊢ BddBelow sᶜ ∧ BddAbove sᶜ

Tactic:
⟨⟨b, fun x hx ↦ ?_⟩, ⟨a, fun x hx ↦ ?_⟩⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
s : Set α
b : α
left : True
hb : Iic b ⊆ s
a : α
left_1 : True
ha : Ici a ⊆ s
refine_1 : ∀ (x : α) (hx : x ∈ sᶜ), b ≤ x
refine_2 : ∀ (x : α) (hx : x ∈ sᶜ), x ≤ a
⊢ BddBelow sᶜ ∧ BddAbove sᶜ

Tactic:
refine ⟨⟨b, fun x hx ↦ ?_⟩, ⟨a, fun x hx ↦ ?_⟩⟩
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
s : Set α
b : α
left : True
hb : Iic b ⊆ s
a : α
left_1 : True
ha : Ici a ⊆ s
x : α
hx : x ∈ sᶜ
refine_1 : ∀ (hx' : x < b), False
⊢ b ≤ x

Tactic:
by_contra! hx'
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
s : Set α
b : α
left : True
hb : Iic b ⊆ s
a : α
left_1 : True
ha : Ici a ⊆ s
x : α
hx : x ∈ sᶜ
refine_2 : ∀ (hx' : a < x), False
⊢ x ≤ a

Tactic:
by_contra! hx'
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
s : Set α
b : α
left : True
hb : Iic b ⊆ s
a : α
left_1 : True
ha : Ici a ⊆ s
x : α
hx : x ∈ sᶜ
hx' : x < b
⊢ False

Tactic:
hx (hb hx'.le)

Premises used: LT.lt.le
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
s : Set α
b : α
left : True
hb : Iic b ⊆ s
a : α
left_1 : True
ha : Ici a ⊆ s
x : α
hx : x ∈ sᶜ
hx' : x < b
⊢ False

Tactic:
exact hx (hb hx'.le)

Premises used: LT.lt.le
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
s : Set α
b : α
left : True
hb : Iic b ⊆ s
a : α
left_1 : True
ha : Ici a ⊆ s
x : α
hx : x ∈ sᶜ
hx' : a < x
⊢ False

Tactic:
hx (ha hx'.le)

Premises used: LT.lt.le
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
s : Set α
b : α
left : True
hb : Iic b ⊆ s
a : α
left_1 : True
ha : Ici a ⊆ s
x : α
hx : x ∈ sᶜ
hx' : a < x
⊢ False

Tactic:
exact hx (ha hx'.le)

Premises used: LT.lt.le
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
inst_4 : NoMaxOrder α
inst_5 : NoMinOrder α
⊢ cobounded α = Filter.atBot ⊔ Filter.atTop

Tactic:
cobounded_le_atBot_sup_atTop.antisymm <|
    sup_le IsOrderBornology.atBot_le_cobounded IsOrderBornology.atTop_le_cobounded

Premises used: IsOrderBornology.cobounded_le_atBot_sup_atTop, IsOrderBornology.atTop_le_cobounded, LE.le.antisymm, IsOrderBornology.atBot_le_cobounded, sup_le
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
inst_4 : NoMaxOrder α
inst_5 : OrderBot α
⊢ cobounded α = Filter.atTop

Tactic:
atTop_le_cobounded.antisymm' fun s ↦ ?_

Premises used: LE.le.antisymm', IsOrderBornology.atTop_le_cobounded
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
inst_4 : NoMaxOrder α
inst_5 : OrderBot α
refine : ∀ (s : Set α), Membership.mem (γ := Filter α) Filter.atTop s → s ∈ cobounded α
⊢ cobounded α = Filter.atTop

Tactic:
refine atTop_le_cobounded.antisymm' fun s ↦ ?_

Premises used: LE.le.antisymm', IsOrderBornology.atTop_le_cobounded
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
inst_4 : NoMaxOrder α
inst_5 : OrderBot α
s : Set α
rw : (∃ (i : α), True ∧ Ici i ⊆ s) → BddBelow sᶜ ∧ BddAbove sᶜ
⊢ Membership.mem (γ := Filter α) Filter.atTop s → s ∈ cobounded α

Tactic:
rw [Filter.atTop_basis.mem_iff,
    ← compl_compl s, ← isBounded_def, isBounded_iff_bddBelow_bddAbove, compl_compl s]

Premises used: Filter.atTop_basis, Filter.HasBasis.mem_iff, compl_compl, Bornology.isBounded_def, isBounded_iff_bddBelow_bddAbove
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
inst_4 : NoMaxOrder α
inst_5 : OrderBot α
s : Set α
h : ∃ (i : α), True ∧ Ici i ⊆ s
b : α
left : True
hb : Ici b ⊆ s
x : α
hx : x ∈ sᶜ
⊢ ⊥ ≤ x

Tactic:
simp
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
inst_4 : NoMaxOrder α
inst_5 : OrderBot α
s : Set α
refine : (∃ (i : α), True ∧ Ici i ⊆ s) → ∀ (b : α), True → ∀ (hb : Ici b ⊆ s) (x : α) (hx : x ∈ sᶜ), x ≤ b
⊢ (∃ (i : α), True ∧ Ici i ⊆ s) → BddBelow sᶜ ∧ BddAbove sᶜ

Tactic:
refine fun ⟨b, _, hb⟩ ↦ ⟨⟨⊥, fun x hx ↦ by simp⟩, ⟨b, fun x hx ↦ ?_⟩⟩
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
inst_4 : NoMaxOrder α
inst_5 : OrderBot α
s : Set α
h : ∃ (i : α), True ∧ Ici i ⊆ s
b : α
left : True
hb : Ici b ⊆ s
x : α
hx : x ∈ sᶜ
by_contra! : ∀ (hx' : b < x), False
⊢ x ≤ b

Tactic:
by_contra! hx'
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
inst_4 : NoMaxOrder α
inst_5 : OrderBot α
s : Set α
h : ∃ (i : α), True ∧ Ici i ⊆ s
b : α
left : True
hb : Ici b ⊆ s
x : α
hx : x ∈ sᶜ
hx' : b < x
⊢ False

Tactic:
hx (hb hx'.le)

Premises used: LT.lt.le
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
inst_4 : NoMaxOrder α
inst_5 : OrderBot α
s : Set α
h : ∃ (i : α), True ∧ Ici i ⊆ s
b : α
left : True
hb : Ici b ⊆ s
x : α
hx : x ∈ sᶜ
hx' : b < x
⊢ False

Tactic:
exact hx (hb hx'.le)

Premises used: LT.lt.le
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
inst_4 : NoMinOrder α
inst_5 : OrderTop α
⊢ cobounded α = Filter.atBot

Tactic:
cobounded_eq_atTop (α := αᵒᵈ)

Premises used: setOf, IsOrderBornology.cobounded_eq_atTop, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
inst : Bornology α
inst_1 : ConditionallyCompleteLattice α
inst_2 : IsOrderBornology α
s : Set α
hs : IsBounded s
⊢ s ⊆ Icc (sInf s) (sSup s)

Tactic:
subset_Icc_csInf_csSup hs.bddBelow hs.bddAbove

Premises used: Bornology.IsBounded.bddBelow, subset_Icc_csInf_csSup, Bornology.IsBounded.bddAbove
-- Module: Mathlib.Topology.Order.Category.AlexDisc
Goal:
X Y : AlexDisc
f g : X ⟶ Y
h :
  Eq (α :=
    Functor.obj
        (forget₂ AlexDisc (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦ C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1)))
          (CC := fun (X : AlexDisc.{u_1}) ↦ (↑X.toTopCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦
          C((↑X : Type u_1), (↑Y : Type u_1))) (CD := TopCat.carrier))
        X ⟶
      Functor.obj
        (forget₂ AlexDisc (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦ C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1)))
          (CC := fun (X : AlexDisc.{u_1}) ↦ (↑X.toTopCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦
          C((↑X : Type u_1), (↑Y : Type u_1))) (CD := TopCat.carrier))
        Y)
    (CategoryTheory.Functor.map
      (forget₂ AlexDisc (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦ C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1)))
        (CC := fun (X : AlexDisc.{u_1}) ↦ (↑X.toTopCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦
        C((↑X : Type u_1), (↑Y : Type u_1))) (CD := TopCat.carrier))
      f)
    (CategoryTheory.Functor.map
      (forget₂ AlexDisc (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦ C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1)))
        (CC := fun (X : AlexDisc.{u_1}) ↦ (↑X.toTopCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦
        C((↑X : Type u_1), (↑Y : Type u_1))) (CD := TopCat.carrier))
      g)
h₁ :
  ∀ (x : (↑X.toTopCat : Type u_1)),
    Eq (α := (↑Y.toTopCat : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦
              C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1))) (CC := fun (X : AlexDisc.{u_1}) ↦
              (↑X.toTopCat : Type u_1)) f :
            (a : (↑X.toTopCat : Type u_1)) → (↑Y.toTopCat : Type u_1))
          x :
        (↑Y.toTopCat : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦
              C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1))) (CC := fun (X : AlexDisc.{u_1}) ↦
              (↑X.toTopCat : Type u_1)) g :
            (a : (↑X.toTopCat : Type u_1)) → (↑Y.toTopCat : Type u_1))
          x :
        (↑Y.toTopCat : Type u_1))
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.Topology.Order.Category.AlexDisc
Goal:
X Y : AlexDisc
f g : X ⟶ Y
h :
  Eq (α :=
    Functor.obj
        (forget₂ AlexDisc (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦ C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1)))
          (CC := fun (X : AlexDisc.{u_1}) ↦ (↑X.toTopCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦
          C((↑X : Type u_1), (↑Y : Type u_1))) (CD := TopCat.carrier))
        X ⟶
      Functor.obj
        (forget₂ AlexDisc (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦ C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1)))
          (CC := fun (X : AlexDisc.{u_1}) ↦ (↑X.toTopCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦
          C((↑X : Type u_1), (↑Y : Type u_1))) (CD := TopCat.carrier))
        Y)
    (CategoryTheory.Functor.map
      (forget₂ AlexDisc (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦ C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1)))
        (CC := fun (X : AlexDisc.{u_1}) ↦ (↑X.toTopCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦
        C((↑X : Type u_1), (↑Y : Type u_1))) (CD := TopCat.carrier))
      f)
    (CategoryTheory.Functor.map
      (forget₂ AlexDisc (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦ C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1)))
        (CC := fun (X : AlexDisc.{u_1}) ↦ (↑X.toTopCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦
        C((↑X : Type u_1), (↑Y : Type u_1))) (CD := TopCat.carrier))
      g)
x : (↑X.toTopCat : Type u_1)
⊢ Eq (α := (↑Y.toTopCat : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦
            C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1))) (CC := fun (X : AlexDisc.{u_1}) ↦
            (↑X.toTopCat : Type u_1)) f :
          (a : (↑X.toTopCat : Type u_1)) → (↑Y.toTopCat : Type u_1))
        x :
      (↑Y.toTopCat : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦
            C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1))) (CC := fun (X : AlexDisc.{u_1}) ↦
            (↑X.toTopCat : Type u_1)) g :
          (a : (↑X.toTopCat : Type u_1)) → (↑Y.toTopCat : Type u_1))
        x :
      (↑Y.toTopCat : Type u_1))

Tactic:
ConcreteCategory.congr_hom h x

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.Topology.Order.Category.AlexDisc
Goal:
X Y : AlexDisc
f g : X ⟶ Y
h :
  Eq (α :=
    Functor.obj
        (forget₂ AlexDisc (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦ C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1)))
          (CC := fun (X : AlexDisc.{u_1}) ↦ (↑X.toTopCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦
          C((↑X : Type u_1), (↑Y : Type u_1))) (CD := TopCat.carrier))
        X ⟶
      Functor.obj
        (forget₂ AlexDisc (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦ C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1)))
          (CC := fun (X : AlexDisc.{u_1}) ↦ (↑X.toTopCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦
          C((↑X : Type u_1), (↑Y : Type u_1))) (CD := TopCat.carrier))
        Y)
    (CategoryTheory.Functor.map
      (forget₂ AlexDisc (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦ C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1)))
        (CC := fun (X : AlexDisc.{u_1}) ↦ (↑X.toTopCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦
        C((↑X : Type u_1), (↑Y : Type u_1))) (CD := TopCat.carrier))
      f)
    (CategoryTheory.Functor.map
      (forget₂ AlexDisc (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦ C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1)))
        (CC := fun (X : AlexDisc.{u_1}) ↦ (↑X.toTopCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦
        C((↑X : Type u_1), (↑Y : Type u_1))) (CD := TopCat.carrier))
      g)
x : (↑X.toTopCat : Type u_1)
⊢ Eq (α := (↑Y.toTopCat : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦
            C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1))) (CC := fun (X : AlexDisc.{u_1}) ↦
            (↑X.toTopCat : Type u_1)) f :
          (a : (↑X.toTopCat : Type u_1)) → (↑Y.toTopCat : Type u_1))
        x :
      (↑Y.toTopCat : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦
            C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1))) (CC := fun (X : AlexDisc.{u_1}) ↦
            (↑X.toTopCat : Type u_1)) g :
          (a : (↑X.toTopCat : Type u_1)) → (↑Y.toTopCat : Type u_1))
        x :
      (↑Y.toTopCat : Type u_1))

Tactic:
exact ConcreteCategory.congr_hom h x

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.Topology.Order.Category.AlexDisc
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
⊢ (↑(of α).toTopCat : Type u_1) = α

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.Category.AlexDisc
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
⊢ Functor.obj
      (forget₂ AlexDisc (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦ C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1)))
        (CC := fun (X : AlexDisc.{u_1}) ↦ (↑X.toTopCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦
        C((↑X : Type u_1), (↑Y : Type u_1))) (CD := TopCat.carrier))
      (of α) =
    TopCat.of α

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.Category.AlexDisc
Goal:
X : AlexDisc
⊢ (↑(Functor.obj
          (forget₂ AlexDisc (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦
            C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1))) (CC := fun (X : AlexDisc.{u_1}) ↦
            (↑X.toTopCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1)))
            (CD := TopCat.carrier))
          X) :
      Type u_1) =
    (↑X.toTopCat : Type u_1)

Tactic:
rfl

Premises used: rfl