awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : Membership.mem (γ := Part α) ((c : (a : ℕ) → Part α) i : Part α) a
j : ℕ
hb : Membership.mem (γ := Part α) ((c : (a : ℕ) → Part α) j : Part α) b
hij : i ≤ j
⊢ Membership.mem (γ := Part α) ((c.toOrderHom : (a : ℕ) → Part α) j : Part α) a

Tactic:
have := c.monotone hij _ ha
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : Membership.mem (γ := Part α) ((c : (a : ℕ) → Part α) i : Part α) a
j : ℕ
hb : Membership.mem (γ := Part α) ((c : (a : ℕ) → Part α) j : Part α) b
hij : i ≤ j
this : Membership.mem (γ := Part α) ((c.toOrderHom : (a : ℕ) → Part α) j : Part α) a
⊢ a = b

Tactic:
apply mem_unique this hb

Premises used: Part.mem_unique
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : Membership.mem (γ := Part α) ((c : (a : ℕ) → Part α) i : Part α) a
j : ℕ
hb : Membership.mem (γ := Part α) ((c : (a : ℕ) → Part α) j : Part α) b
hji : j ≤ i
⊢ Membership.mem (γ := Part α) ((c.toOrderHom : (a : ℕ) → Part α) i : Part α) b

Tactic:
have := c.monotone hji _ hb
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : Membership.mem (γ := Part α) ((c : (a : ℕ) → Part α) i : Part α) a
j : ℕ
hb : Membership.mem (γ := Part α) ((c : (a : ℕ) → Part α) j : Part α) b
hji : j ≤ i
this : Membership.mem (γ := Part α) ((c.toOrderHom : (a : ℕ) → Part α) i : Part α) b
inr : b = a
⊢ a = b

Tactic:
apply Eq.symm

Premises used: Eq.symm
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : Membership.mem (γ := Part α) ((c : (a : ℕ) → Part α) i : Part α) a
j : ℕ
hb : Membership.mem (γ := Part α) ((c : (a : ℕ) → Part α) j : Part α) b
hji : j ≤ i
this : Membership.mem (γ := Part α) ((c.toOrderHom : (a : ℕ) → Part α) i : Part α) b
⊢ b = a

Tactic:
apply mem_unique this ha

Premises used: Part.mem_unique
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
c : Chain (Part α)
a : α
h : some a ∈ c
⊢ Part.ωSup c = some a

Tactic:
have : ∃ a, some a ∈ c := ⟨a, h⟩
  have a' : some (Classical.choose this) ∈ c := Classical.choose_spec this
  calc
    Part.ωSup c = some (Classical.choose this) := dif_pos this
    _ = some a := congr_arg _ (eq_of_chain a' h)

Premises used: Part.eq_of_chain, Trans.trans, Part.some, dif_pos, congr_arg, Classical.choose_spec, Exists.intro
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
c : Chain (Part α)
h : ¬∃ (a : α), some a ∈ c
⊢ Part.ωSup c = none

Tactic:
dif_neg h

Premises used: Part.ωSup, dif_neg
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
c : Chain (Part α)
a : α
h :
  Membership.mem (γ := Part α)
    (if h : ∃ (a : α), some a ∈ c then some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h) else none) a
pos : ∀ (h_1 : ∃ (a : α), some a ∈ c) (h : a ∈ some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h_1)), some a ∈ c
neg : ∀ (h_1 : ¬∃ (a : α), some a ∈ c) (h : Membership.mem (γ := Part α) none a), some a ∈ c
⊢ some a ∈ c

Tactic:
split_ifs at h with h_1
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
c : Chain (Part α)
a : α
h_1 : ∃ (a : α), some a ∈ c
h : a ∈ some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h_1)
⊢ some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h_1) ∈ c

Tactic:
have h' := Classical.choose_spec h_1
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
c : Chain (Part α)
a : α
h_1 : ∃ (a : α), some a ∈ c
h : a ∈ some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h_1)
h' : some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h_1) ∈ c
⊢ some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h_1) = some a

Tactic:
rw [← eq_some_iff] at h

Premises used: Part.eq_some_iff
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
c : Chain (Part α)
a : α
h_1 : ∃ (a : α), some a ∈ c
h : a ∈ some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h_1)
h' : some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h_1) ∈ c
h₁ : some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h_1) = some a
⊢ some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h_1) ∈ c

Tactic:
rw [← eq_some_iff] at h

Premises used: Part.eq_some_iff
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
c : Chain (Part α)
a : α
h_1 : ∃ (a : α), some a ∈ c
h : some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h_1) = some a
h' : some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h_1) ∈ c
pos : some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h_1) ∈ c
⊢ some a ∈ c

Tactic:
rw [← h]
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
c : Chain (Part α)
a : α
h_1 : ∃ (a : α), some a ∈ c
h : some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h_1) = some a
h' : some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h_1) ∈ c
⊢ some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h_1) ∈ c

Tactic:
h'
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
c : Chain (Part α)
a : α
h_1 : ∃ (a : α), some a ∈ c
h : some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h_1) = some a
h' : some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h_1) ∈ c
⊢ some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h_1) ∈ c

Tactic:
exact h'
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
c : Chain (Part α)
a : α
h_1 : ¬∃ (a : α), some a ∈ c
h : Membership.mem (γ := Part α) none a
⊢ some a ∈ c

Tactic:
rcases h with ⟨⟨⟩⟩
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
i : ℕ
x : α
hx : Membership.mem (γ := Part α) ((c : (a : ℕ) → Part α) i : Part α) x
rw : ∀ (hx : (c : (a : ℕ) → Part α) i = some x), Part.ωSup c = some x
⊢ x ∈ Part.ωSup c

Tactic:
rw [← eq_some_iff] at hx ⊢

Premises used: Part.eq_some_iff
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
i : ℕ
x : α
hx : (c : (a : ℕ) → Part α) i = some x
rw : some x ∈ c
⊢ Part.ωSup c = some x

Tactic:
rw [ωSup_eq_some]

Premises used: Part.ωSup_eq_some
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
i : ℕ
x : α
hx : (c : (a : ℕ) → Part α) i = some x
rw : Membership.mem (α := Part α) c ((c : (a : ℕ) → Part α) i : Part α)
⊢ some x ∈ c

Tactic:
rw [← hx]
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
i : ℕ
x : α
hx : (c : (a : ℕ) → Part α) i = some x
⊢ Membership.mem (α := Part α) c ((c : (a : ℕ) → Part α) i : Part α)

Tactic:
⟨i, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
i : ℕ
x : α
hx : (c : (a : ℕ) → Part α) i = some x
⊢ Membership.mem (α := Part α) c ((c : (a : ℕ) → Part α) i : Part α)

Tactic:
exact ⟨i, rfl⟩
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
x : Part α
hx : ∀ (i : ℕ), (c : (a : ℕ) → Part α) i ≤ x
a : α
ha : a ∈ Part.ωSup c
⊢ some a ∈ c

Tactic:
replace ha := mem_chain_of_mem_ωSup ha
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
x : Part α
hx : ∀ (i : ℕ), (c : (a : ℕ) → Part α) i ≤ x
a : α
ha : some a ∈ c
obtain : ∀ (i : ℕ) (ha : some a = (c : (a : ℕ) → Part α) i), a ∈ x
⊢ a ∈ x

Tactic:
obtain ⟨i, ha⟩ := ha
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
x : Part α
hx : ∀ (i : ℕ), (c : (a : ℕ) → Part α) i ≤ x
a : α
i : ℕ
ha : some a = (c : (a : ℕ) → Part α) i
a₁ : Membership.mem (γ := Part α) ((c : (a : ℕ) → Part α) i : Part α) a
⊢ a ∈ x

Tactic:
apply hx i
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
x : Part α
hx : ∀ (i : ℕ), (c : (a : ℕ) → Part α) i ≤ x
a : α
i : ℕ
ha : some a = (c : (a : ℕ) → Part α) i
a₁ : a ∈ some a
⊢ Membership.mem (γ := Part α) ((c : (a : ℕ) → Part α) i : Part α) a

Tactic:
rw [← ha]
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
x : Part α
hx : ∀ (i : ℕ), (c : (a : ℕ) → Part α) i ≤ x
a : α
i : ℕ
ha : some a = (c : (a : ℕ) → Part α) i
⊢ a ∈ some a

Tactic:
apply mem_some

Premises used: Part.mem_some
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
x : α
c : Chain (Part α)
mp :
  Membership.mem (γ := Part α)
      (if h : ∃ (a : α), some a ∈ c then some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h) else none) x →
    some x ∈ c
mpr :
  some x ∈ c →
    Membership.mem (γ := Part α)
      (if h : ∃ (a : α), some a ∈ c then some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h) else none) x
⊢ Membership.mem (γ := Part α)
      (if h : ∃ (a : α), some a ∈ c then some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h) else none) x ↔
    some x ∈ c

Tactic:
constructor
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
x : α
c : Chain (Part α)
⊢ Membership.mem (γ := Part α)
      (if h : ∃ (a : α), some a ∈ c then some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h) else none) x →
    some x ∈ c

Tactic:
fun a ↦ mem_chain_of_mem_ωSup a

Premises used: Part.mem_chain_of_mem_ωSup
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
x : α
c : Chain (Part α)
⊢ Membership.mem (γ := Part α)
      (if h : ∃ (a : α), some a ∈ c then some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h) else none) x →
    some x ∈ c

Tactic:
exact fun a ↦ mem_chain_of_mem_ωSup a

Premises used: Part.mem_chain_of_mem_ωSup
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
x : α
c : Chain (Part α)
h : some x ∈ c
⊢ ∃ (a : α), some a ∈ c

Tactic:
have h' : ∃ a : α, some a ∈ c := ⟨_, h⟩
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
x : α
c : Chain (Part α)
h : some x ∈ c
h' : ∃ (a : α), some a ∈ c
mpr : x ∈ some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h')
⊢ Membership.mem (γ := Part α)
    (if h : ∃ (a : α), some a ∈ c then some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h) else none) x

Tactic:
rw [dif_pos h']

Premises used: dif_pos
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
x : α
c : Chain (Part α)
h : some x ∈ c
h' : ∃ (a : α), some a ∈ c
⊢ some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h') ∈ c

Tactic:
have hh := Classical.choose_spec h'
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
x : α
c : Chain (Part α)
h : some x ∈ c
h' : ∃ (a : α), some a ∈ c
hh : some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h') ∈ c
mpr : x ∈ some x
⊢ x ∈ some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h')

Tactic:
rw [eq_of_chain hh h]

Premises used: Part.eq_of_chain
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
x : α
c : Chain (Part α)
h : some x ∈ c
h' : ∃ (a : α), some a ∈ c
hh : some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h') ∈ c
⊢ x ∈ some x

Tactic:
simp
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
ι : Sort u_1
α : Type u_2
β_1 : Type u_3
γ : Type u_4
δ : Type u_5
β : α → Type u_6
inst : (a : α) → OmegaCompletePartialOrder (β a)
x : Chain ((a : α) → β a)
x_1 : (a : α) → β a
hf : ∀ (i : ℕ), (x : (a : ℕ) → (a : α) → β a) i ≤ x_1
a : α
i : ℕ
⊢ (x.map (Pi.evalOrderHom (π := β) a) : (a_1 : ℕ) → β a) i ≤ x_1 a

Tactic:
apply hf
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
γ : Type u_4
β : α → Type u_6
inst : (x : α) → OmegaCompletePartialOrder (β x)
inst_1 : OmegaCompletePartialOrder γ
f : γ → (x : α) → β x
hf : ωScottContinuous f
a : α
⊢ ωScottContinuous.{u_4, u_6} (β := β a) fun (x : γ) ↦ f x a

Tactic:
ωScottContinuous.of_monotone_map_ωSup
    ⟨fun _ _ h ↦ hf.monotone h a, fun c ↦ congr_fun (hf.map_ωSup c) a⟩

Premises used: OmegaCompletePartialOrder.ωScottContinuous.map_ωSup, OmegaCompletePartialOrder.ωScottContinuous.monotone, Exists.intro, OmegaCompletePartialOrder.ωScottContinuous.of_monotone_map_ωSup, congr_fun
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : α → Type u_6
inst : (x : α) → OmegaCompletePartialOrder (β x)
x : α
⊢ ωScottContinuous (β := β x) fun (f : (x : α) → β x) ↦ f x

Tactic:
apply₂ id x

Premises used: OmegaCompletePartialOrder.ωScottContinuous.apply₂, OmegaCompletePartialOrder.ωScottContinuous.id
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
γ : Type u_4
β : α → Type u_6
inst : (x : α) → OmegaCompletePartialOrder (β x)
inst_1 : OmegaCompletePartialOrder γ
f : γ → (x : α) → β x
hf : ∀ (a : α), ωScottContinuous.{u_4, u_6} (β := β a) fun (x : γ) ↦ f x a
c : Chain γ
h : ∀ (a : α), f (ωSup c) a = ωSup (c.map { toFun := f, monotone' := ⋯ }) a
⊢ f (ωSup c) = ωSup (c.map { toFun := f, monotone' := ⋯ })

Tactic:
ext a
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
γ : Type u_4
β : α → Type u_6
inst : (x : α) → OmegaCompletePartialOrder (β x)
inst_1 : OmegaCompletePartialOrder γ
f : γ → (x : α) → β x
hf : ∀ (a : α), ωScottContinuous.{u_4, u_6} (β := β a) fun (x : γ) ↦ f x a
c : Chain γ
a : α
⊢ f (ωSup c) a = ωSup (c.map { toFun := f, monotone' := ⋯ }) a

Tactic:
apply (hf a).map_ωSup c

Premises used: OmegaCompletePartialOrder.ωScottContinuous.map_ωSup
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
γ : Type u_4
β : α → Type u_6
inst : (x : α) → OmegaCompletePartialOrder (β x)
inst_1 : OmegaCompletePartialOrder γ
f : γ → (x : α) → β x
⊢ ωScottContinuous f ↔ ∀ (a : α), ωScottContinuous.{u_4, u_6} (β := β a) fun (x : γ) ↦ f x a

Tactic:
⟨ωScottContinuous.apply₂, ωScottContinuous.of_apply₂⟩

Premises used: OmegaCompletePartialOrder.ωScottContinuous.of_apply₂, OmegaCompletePartialOrder.ωScottContinuous.apply₂, Iff.intro
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
c₀ : Chain α
c₁ : Chain β
⊢ ωSup (c₀.zip c₁) = (ωSup c₀, ωSup c₁)

Tactic:
rfl

Premises used: OrderHom.comp, OmegaCompletePartialOrder.Chain.map, rfl, Prod.ωSupImpl
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β
hf : ωScottContinuous f
g : α → γ
hg : ωScottContinuous g
⊢ ωScottContinuous (β := β × γ) fun (x : α) ↦ (f x, g x)

Tactic:
ScottContinuousOn.prodMk (fun a b hab ↦ ⟨pair a b hab, range_pair a b hab⟩) hf hg

Premises used: OmegaCompletePartialOrder.Chain.pair, OmegaCompletePartialOrder.Chain.range_pair, ScottContinuousOn.prodMk, Exists.intro, OmegaCompletePartialOrder.ωScottContinuous
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
⊢ ωScottContinuous (α := α × β) fst

Tactic:
ScottContinuousOn.fst

Premises used: ScottContinuousOn.fst, OmegaCompletePartialOrder.ωScottContinuous
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
⊢ ωScottContinuous (α := α × β) snd

Tactic:
ScottContinuousOn.snd

Premises used: ScottContinuousOn.snd, OmegaCompletePartialOrder.ωScottContinuous
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
inst_3 : OmegaCompletePartialOrder δ
toOrderHom : α →o β
map_ωSup' : ∀ (c : Chain α), toOrderHom.toFun (ωSup c) = ωSup (c.map toOrderHom)
toOrderHom_1 : α →o β
map_ωSup'_1 : ∀ (c : Chain α), toOrderHom_1.toFun (ωSup c) = ωSup (c.map toOrderHom_1)
h :
  Eq (α := (a : α) → β) ((fun (f : α →𝒄 β) ↦ f.toFun) { toOrderHom := toOrderHom, map_ωSup' := map_ωSup' })
    ((fun (f : α →𝒄 β) ↦ f.toFun) { toOrderHom := toOrderHom_1, map_ωSup' := map_ωSup'_1 })
e_toOrderHom : toOrderHom = toOrderHom_1
⊢ { toOrderHom := toOrderHom, map_ωSup' := map_ωSup' : α →𝒄 β } =
    { toOrderHom := toOrderHom_1, map_ωSup' := map_ωSup'_1 }

Tactic:
congr
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
inst_3 : OmegaCompletePartialOrder δ
toOrderHom : α →o β
map_ωSup' : ∀ (c : Chain α), toOrderHom.toFun (ωSup c) = ωSup (c.map toOrderHom)
toOrderHom_1 : α →o β
map_ωSup'_1 : ∀ (c : Chain α), toOrderHom_1.toFun (ωSup c) = ωSup (c.map toOrderHom_1)
h :
  Eq (α := (a : α) → β) ((fun (f : α →𝒄 β) ↦ f.toFun) { toOrderHom := toOrderHom, map_ωSup' := map_ωSup' })
    ((fun (f : α →𝒄 β) ↦ f.toFun) { toOrderHom := toOrderHom_1, map_ωSup' := map_ωSup'_1 })
⊢ toOrderHom = toOrderHom_1

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
inst_3 : OmegaCompletePartialOrder δ
toOrderHom : α →o β
map_ωSup' : ∀ (c : Chain α), toOrderHom.toFun (ωSup c) = ωSup (c.map toOrderHom)
toOrderHom_1 : α →o β
map_ωSup'_1 : ∀ (c : Chain α), toOrderHom_1.toFun (ωSup c) = ωSup (c.map toOrderHom_1)
h :
  Eq (α := (a : α) → β) ((fun (f : α →𝒄 β) ↦ f.toFun) { toOrderHom := toOrderHom, map_ωSup' := map_ωSup' })
    ((fun (f : α →𝒄 β) ↦ f.toFun) { toOrderHom := toOrderHom_1, map_ωSup' := map_ωSup'_1 })
⊢ toOrderHom = toOrderHom_1

Tactic:
exact DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
inst_3 : OmegaCompletePartialOrder δ
toFun : α → β
monotone' : Monotone toFun
map_ωSup' :
  ∀ (c : Chain α),
    { toFun := toFun, monotone' := monotone' : α →o β }.toFun (ωSup c) =
      ωSup (c.map { toFun := toFun, monotone' := monotone' : α →o β })
toFun_1 : α → β
monotone'_1 : Monotone toFun_1
map_ωSup'_1 :
  ∀ (c : Chain α),
    { toFun := toFun_1, monotone' := monotone'_1 : α →o β }.toFun (ωSup c) =
      ωSup (c.map { toFun := toFun_1, monotone' := monotone'_1 : α →o β })
h :
  Eq (α := α → β) ((fun (f : α →𝒄 β) ↦ f.toFun) { toFun := toFun, monotone' := monotone', map_ωSup' := map_ωSup' })
    ((fun (f : α →𝒄 β) ↦ f.toFun) { toFun := toFun_1, monotone' := monotone'_1, map_ωSup' := map_ωSup'_1 })
⊢ { toFun := toFun, monotone' := monotone', map_ωSup' := map_ωSup' : α →𝒄 β } =
    { toFun := toFun_1, monotone' := monotone'_1, map_ωSup' := map_ωSup'_1 }

Tactic:
congr
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α →𝒄 β
⊢ ωScottContinuous.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β)

Tactic:
ωScottContinuous.of_map_ωSup_of_orderHom f.map_ωSup'

Premises used: OmegaCompletePartialOrder.ωScottContinuous.of_map_ωSup_of_orderHom, OmegaCompletePartialOrder.ContinuousHom.map_ωSup'
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α →𝒄 β
⊢ f.toOrderHom = (↑f : α →o β)

Tactic:
rfl

Premises used: OrderHomClass.toOrderHom, rfl
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α →o β
hf : ∀ (c : Chain α), f.toFun (ωSup c) = ωSup (c.map f)
⊢ Eq (α := (a : α) → β) (⇑{ toOrderHom := f, map_ωSup' := hf : α →𝒄 β } : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α →𝒄 β
⊢ Eq (α := (a : α) → β) (⇑f.toOrderHom : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f g : α →𝒄 β
h : f = g
x : α
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)

Tactic:
DFunLike.congr_fun h x

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α →𝒄 β
x y : α
h : x = y
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)

Tactic:
congr_arg f h

Premises used: congr_arg, DFunLike.coe
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α →𝒄 β
⊢ Monotone.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β)

Tactic:
f.monotone'

Premises used: OmegaCompletePartialOrder.ContinuousHom.toOrderHom, OrderHom.monotone'
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f g : α →𝒄 β
x y : α
h₁ : f ≤ g
h₂ : x ≤ y
⊢ LE.le.{u_3} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) y : β)

Tactic:
OrderHom.apply_mono (show (f : α →o β) ≤ g from h₁) h₂

Premises used: OrderHom.apply_mono
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : OrderHom.{u_2, v} α (Part β)
g : OrderHom.{u_2, v} α (β → Part γ)
H : ∀ (c_1 : Part γ), ωSup (c.map (f.partBind g)) ≤ c_1 ↔ ωSup (c.map f) >>= ωSup (c.map g) ≤ c_1
⊢ ωSup (c.map (f.partBind g)) = ωSup (c.map f) >>= ωSup (c.map g)

Tactic:
apply eq_of_forall_ge_iff

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : OrderHom.{u_2, v} α (Part β)
g : OrderHom.{u_2, v} α (β → Part γ)
x : Part γ
H : (∀ (i : ℕ), (c.map (f.partBind g) : (a : ℕ) → Part γ) i ≤ x) ↔ ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
⊢ ωSup (c.map (f.partBind g)) ≤ x ↔ ωSup (c.map f) >>= ωSup (c.map g) ≤ x

Tactic:
simp only [ωSup_le_iff, Part.bind_le]

Premises used: OmegaCompletePartialOrder.ωSup_le_iff, Part.bind_le
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : OrderHom.{u_2, v} α (Part β)
g : OrderHom.{u_2, v} α (β → Part γ)
x : Part γ
H : (∀ (i : ℕ), (c.map (f.partBind g) : (a : ℕ) → Part γ) i ≤ x) → ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
H₁ : (∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x) → ∀ (i : ℕ), (c.map (f.partBind g) : (a : ℕ) → Part γ) i ≤ x
⊢ (∀ (i : ℕ), (c.map (f.partBind g) : (a : ℕ) → Part γ) i ≤ x) ↔ ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x

Tactic:
constructor
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : OrderHom.{u_2, v} α (Part β)
g : OrderHom.{u_2, v} α (β → Part γ)
x : Part γ
h''' : ∀ (i : ℕ), (c.map (f.partBind g) : (a : ℕ) → Part γ) i ≤ x
b : β
hb : b ∈ ωSup (c.map f)
apply : ∀ (i : ℕ), ((c.map g).map (Pi.evalOrderHom (π := fun (a : β) ↦ Part γ) b) : (a : ℕ) → Part γ) i ≤ x
⊢ ωSup (c.map g) b ≤ x

Tactic:
apply ωSup_le _ _ _

Premises used: OmegaCompletePartialOrder.ωSup_le