awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
i : ℕ
y : γ
hy :
  Membership.mem (γ := Part γ)
    (((c.map g).map (Pi.evalOrderHom (π := fun (a : β) ↦ Part γ) b) : (a : ℕ) → Part γ) i : Part γ) y
⊢ Part.some b ∈ c.map f

Tactic:
simp only [Part.mem_ωSup] at hb

Premises used: Part.mem_ωSup
-- 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 : β
i : ℕ
y : γ
hy :
  Membership.mem (γ := Part γ)
    (((c.map g).map (Pi.evalOrderHom (π := fun (a : β) ↦ Part γ) b) : (a : ℕ) → Part γ) i : Part γ) y
hb : Part.some b ∈ c.map f
rcases : ∀ (j : ℕ) (hb : Part.some b = (c.map f : (a : ℕ) → Part β) j), y ∈ x
⊢ y ∈ x

Tactic:
rcases hb with ⟨j, hb⟩
-- 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 : β
i : ℕ
y : γ
hy :
  Membership.mem (γ := Part γ)
    (((c.map g).map (Pi.evalOrderHom (π := fun (a : β) ↦ Part γ) b) : (a : ℕ) → Part γ) i : Part γ) y
j : ℕ
hb : Part.some b = (c.map f : (a : ℕ) → Part β) j
⊢ (c.map f : (a : ℕ) → Part β) j = Part.some b

Tactic:
replace hb := hb.symm
-- 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 : β
i : ℕ
y : γ
hy :
  Membership.mem (γ := Part γ)
    (((c.map g).map (Pi.evalOrderHom (π := fun (a : β) ↦ Part γ) b) : (a : ℕ) → Part γ) i : Part γ) y
j : ℕ
hb : (c.map f : (a : ℕ) → Part β) j = Part.some b
⊢ Membership.mem (γ := Part β) ((f : (a : α) → Part β) ((c : (a : ℕ) → α) j) : Part β) b

Tactic:
simp only [Part.eq_some_iff, Chain.coe_map, Function.comp_apply] at hy hb

Premises used: OmegaCompletePartialOrder.Chain.coe_map, Part.eq_some_iff, Function.comp_apply
-- 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 : β
i : ℕ
y : γ
hy :
  Membership.mem (γ := Part γ)
    ((Pi.evalOrderHom (π := fun (a : β) ↦ Part γ) b : (a : (a : β) → Part γ) → Part γ)
        ((g : (a : α) → β → Part γ) ((c : (a : ℕ) → α) i : α) : β → Part γ) :
      Part γ)
    y
j : ℕ
hb : Membership.mem (γ := Part β) ((f : (a : α) → Part β) ((c : (a : ℕ) → α) j) : Part β) b
⊢ Membership.mem (γ := Part β) ((f : (a : α) → Part β) ((c : (a : ℕ) → α) (max i j)) : Part β) b

Tactic:
replace hb : b ∈ f (c (max i j)) := f.mono (c.mono (le_max_right i j)) _ hb
-- 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 : β
i : ℕ
y : γ
hy :
  Membership.mem (γ := Part γ)
    ((Pi.evalOrderHom (π := fun (a : β) ↦ Part γ) b : (a : (a : β) → Part γ) → Part γ)
        ((g : (a : α) → β → Part γ) ((c : (a : ℕ) → α) i : α) : β → Part γ) :
      Part γ)
    y
j : ℕ
hb : Membership.mem (γ := Part β) ((f : (a : α) → Part β) ((c : (a : ℕ) → α) (max i j)) : Part β) b
⊢ Membership.mem (γ := Part γ) ((g : (a : α) → β → Part γ) ((c : (a : ℕ) → α) (max i j) : α) b : Part γ) y

Tactic:
replace hy : y ∈ g (c (max i j)) b := g.mono (c.mono (le_max_left i j)) _ _ hy
-- 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 : β
i : ℕ
y : γ
j : ℕ
hb : Membership.mem (γ := Part β) ((f : (a : α) → Part β) ((c : (a : ℕ) → α) (max i j)) : Part β) b
hy : Membership.mem (γ := Part γ) ((g : (a : α) → β → Part γ) ((c : (a : ℕ) → α) (max i j) : α) b : Part γ) y
a : Membership.mem (γ := Part γ) ((c.map (f.partBind g) : (a : ℕ) → Part γ) (max i j) : Part γ) y
⊢ y ∈ x

Tactic:
apply h''' (max i j)

Premises used: Max.max
-- 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 : β
i : ℕ
y : γ
j : ℕ
hb : Membership.mem (γ := Part β) ((f : (a : α) → Part β) ((c : (a : ℕ) → α) (max i j)) : Part β) b
hy : Membership.mem (γ := Part γ) ((g : (a : α) → β → Part γ) ((c : (a : ℕ) → α) (max i j) : α) b : Part γ) y
a :
  ∃ (a : β),
    Membership.mem (γ := Part β) ((f : (a : α) → Part β) ((c : (a : ℕ) → α) (max i j)) : Part β) a ∧
      Membership.mem (γ := Part γ) ((g : (a : α) → β → Part γ) ((c : (a : ℕ) → α) (max i j) : α) a : Part γ) y
⊢ Membership.mem (γ := Part γ) ((c.map (f.partBind g) : (a : ℕ) → Part γ) (max i j) : Part γ) y

Tactic:
simp only [Part.mem_bind_iff, Chain.coe_map,
      Function.comp_apply, OrderHom.partBind_coe]

Premises used: Part.mem_bind_iff, OmegaCompletePartialOrder.Chain.coe_map, Function.comp_apply, OrderHom.partBind_coe
-- 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 : β
i : ℕ
y : γ
j : ℕ
hb : Membership.mem (γ := Part β) ((f : (a : α) → Part β) ((c : (a : ℕ) → α) (max i j)) : Part β) b
hy : Membership.mem (γ := Part γ) ((g : (a : α) → β → Part γ) ((c : (a : ℕ) → α) (max i j) : α) b : Part γ) y
⊢ ∃ (a : β),
    Membership.mem (γ := Part β) ((f : (a : α) → Part β) ((c : (a : ℕ) → α) (max i j)) : Part β) a ∧
      Membership.mem (γ := Part γ) ((g : (a : α) → β → Part γ) ((c : (a : ℕ) → α) (max i j) : α) a : Part γ) y

Tactic:
⟨_, hb, hy⟩

Premises used: And.intro, Exists.intro
-- 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 : β
i : ℕ
y : γ
j : ℕ
hb : Membership.mem (γ := Part β) ((f : (a : α) → Part β) ((c : (a : ℕ) → α) (max i j)) : Part β) b
hy : Membership.mem (γ := Part γ) ((g : (a : α) → β → Part γ) ((c : (a : ℕ) → α) (max i j) : α) b : Part γ) y
⊢ ∃ (a : β),
    Membership.mem (γ := Part β) ((f : (a : α) → Part β) ((c : (a : ℕ) → α) (max i j)) : Part β) a ∧
      Membership.mem (γ := Part γ) ((g : (a : α) → β → Part γ) ((c : (a : ℕ) → α) (max i j) : α) a : Part γ) y

Tactic:
exact ⟨_, hb, hy⟩
-- 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''' : ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
i : ℕ
y : γ
hy : Membership.mem (γ := Part γ) ((c.map (f.partBind g) : (a : ℕ) → Part γ) i : Part γ) y
⊢ ∃ (a : β),
    Membership.mem (γ := Part β) ((f : (a : α) → Part β) ((c : (a : ℕ) → α) i) : Part β) a ∧
      Membership.mem (γ := Part γ) ((g : (a : α) → β → Part γ) ((c : (a : ℕ) → α) i : α) a : Part γ) y

Tactic:
simp only [Part.mem_bind_iff, Chain.coe_map,
      Function.comp_apply, OrderHom.partBind_coe] at hy

Premises used: Part.mem_bind_iff, OmegaCompletePartialOrder.Chain.coe_map, Function.comp_apply, OrderHom.partBind_coe
-- 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''' : ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
i : ℕ
y : γ
hy :
  ∃ (a : β),
    Membership.mem (γ := Part β) ((f : (a : α) → Part β) ((c : (a : ℕ) → α) i) : Part β) a ∧
      Membership.mem (γ := Part γ) ((g : (a : α) → β → Part γ) ((c : (a : ℕ) → α) i : α) a : Part γ) y
H :
  ∀ (b : β) (hb₀ : Membership.mem (γ := Part β) ((f : (a : α) → Part β) ((c : (a : ℕ) → α) i) : Part β) b)
    (hb₁ : Membership.mem (γ := Part γ) ((g : (a : α) → β → Part γ) ((c : (a : ℕ) → α) i : α) b : Part γ) y), y ∈ x
⊢ y ∈ x

Tactic:
rcases hy with ⟨b, hb₀, hb₁⟩
-- 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''' : ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
i : ℕ
y : γ
b : β
hb₀ : Membership.mem (γ := Part β) ((f : (a : α) → Part β) ((c : (a : ℕ) → α) i) : Part β) b
hb₁ : Membership.mem (γ := Part γ) ((g : (a : α) → β → Part γ) ((c : (a : ℕ) → α) i : α) b : Part γ) y
H : y ∈ ωSup (c.map g) b
apply : b ∈ ωSup (c.map f)
⊢ y ∈ x

Tactic:
apply h''' b _
-- 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''' : ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
i : ℕ
y : γ
b : β
hb₀ : Membership.mem (γ := Part β) ((f : (a : α) → Part β) ((c : (a : ℕ) → α) i) : Part β) b
hb₁ : Membership.mem (γ := Part γ) ((g : (a : α) → β → Part γ) ((c : (a : ℕ) → α) i : α) b : Part γ) y
⊢ y ∈ ωSup (c.map g) b

Tactic:
apply le_ωSup (c.map g) _ _ _ hb₁

Premises used: OmegaCompletePartialOrder.le_ωSup, OmegaCompletePartialOrder.Chain.map
-- 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''' : ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
i : ℕ
y : γ
b : β
hb₀ : Membership.mem (γ := Part β) ((f : (a : α) → Part β) ((c : (a : ℕ) → α) i) : Part β) b
hb₁ : Membership.mem (γ := Part γ) ((g : (a : α) → β → Part γ) ((c : (a : ℕ) → α) i : α) b : Part γ) y
⊢ b ∈ ωSup (c.map f)

Tactic:
apply le_ωSup (c.map f) i _ hb₀

Premises used: OmegaCompletePartialOrder.le_ωSup, OmegaCompletePartialOrder.Chain.map
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
β γ : Type u_6
f : α → Part β
g : α → β → Part γ
hf : ωScottContinuous f
hg : ωScottContinuous g
c : Chain α
rw :
  ωSup
      (c.map
        ({ toFun := f, monotone' := ⋯ : OrderHom.{u_2, u_6} α (Part β) }.partBind
          { toFun := g, monotone' := ⋯ : OrderHom.{u_2, u_6} α (β → Part γ) })) =
    ωSup (c.map { toFun := fun (x : α) ↦ f x >>= g x, monotone' := ⋯ : OrderHom.{u_2, u_6} α (Part γ) })
⊢ f (ωSup c) >>= g (ωSup c) =
    ωSup (c.map { toFun := fun (x : α) ↦ f x >>= g x, monotone' := ⋯ : OrderHom.{u_2, u_6} α (Part γ) })

Tactic:
rw [hf.map_ωSup, hg.map_ωSup, ← ωSup_bind]

Premises used: OmegaCompletePartialOrder.ωScottContinuous.map_ωSup, OmegaCompletePartialOrder.ContinuousHom.ωSup_bind
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
β γ : Type u_6
f : α → Part β
g : α → β → Part γ
hf : ωScottContinuous f
hg : ωScottContinuous g
c : Chain α
⊢ ωSup
      (c.map
        ({ toFun := f, monotone' := ⋯ : OrderHom.{u_2, u_6} α (Part β) }.partBind
          { toFun := g, monotone' := ⋯ : OrderHom.{u_2, u_6} α (β → Part γ) })) =
    ωSup (c.map { toFun := fun (x : α) ↦ f x >>= g x, monotone' := ⋯ : OrderHom.{u_2, u_6} α (Part γ) })

Tactic:
rfl
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
β γ : Type u_6
f : β → γ
g : α → Part β
hg : ωScottContinuous g
⊢ ωScottContinuous.{u_2, u_6} (β := Part γ) fun (x : α) ↦ f <$> g x

Tactic:
simpa only [map_eq_bind_pure_comp] using ωScottContinuous.bind hg ωScottContinuous.const

Premises used: OmegaCompletePartialOrder.ωScottContinuous.const, map_eq_bind_pure_comp, OmegaCompletePartialOrder.ContinuousHom.ωScottContinuous.bind
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
β γ : Type u_6
f : α → Part (β → γ)
g : α → Part β
hf : ωScottContinuous f
hg : ωScottContinuous g
simp :
  ωScottContinuous.{u_2, u_6} (β := Part γ) fun (x : α) ↦ do
    let x_1 ← f x
    x_1 <$> g x
⊢ ωScottContinuous.{u_2, u_6} (β := Part γ) fun (x : α) ↦ f x <*> g x

Tactic:
simp only [seq_eq_bind_map]

Premises used: seq_eq_bind_map
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
β γ : Type u_6
f : α → Part (β → γ)
g : α → Part β
hf : ωScottContinuous f
hg : ωScottContinuous g
⊢ ωScottContinuous.{u_2, u_6} (β := Part γ) fun (x : α) ↦ do
    let x_1 ← f x
    x_1 <$> g x

Tactic:
ωScottContinuous.bind hf <| ωScottContinuous.of_apply₂ fun _ ↦ ωScottContinuous.map hg

Premises used: OmegaCompletePartialOrder.ωScottContinuous.of_apply₂, OmegaCompletePartialOrder.ContinuousHom.ωScottContinuous.map, OmegaCompletePartialOrder.ContinuousHom.ωScottContinuous.bind
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
β γ : Type u_6
f : α → Part (β → γ)
g : α → Part β
hf : ωScottContinuous f
hg : ωScottContinuous g
⊢ ωScottContinuous.{u_2, u_6} (β := Part γ) fun (x : α) ↦ do
    let x_1 ← f x
    x_1 <$> g x

Tactic:
exact ωScottContinuous.bind hf <| ωScottContinuous.of_apply₂ fun _ ↦ ωScottContinuous.map hg

Premises used: OmegaCompletePartialOrder.ωScottContinuous.of_apply₂, OmegaCompletePartialOrder.ContinuousHom.ωScottContinuous.map, OmegaCompletePartialOrder.ContinuousHom.ωScottContinuous.bind
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
F : α →𝒄 β
C : Chain α
⊢ (F : (a : α) → β) (ωSup C) = ωSup (C.map (↑F : α →o β))

Tactic:
F.ωScottContinuous.map_ωSup _

Premises used: OmegaCompletePartialOrder.ContinuousHom.ωScottContinuous, OmegaCompletePartialOrder.ωScottContinuous.map_ωSup, OrderHomClass.toOrderHom
-- 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 δ
f : α → β
g : α →𝒄 β
h : f = (⇑g : (a : α) → β)
rw : ∀ (c : Chain α), g.toFun (ωSup c) = ωSup (c.map g.toOrderHom)
⊢ ∀ (c : Chain α), (g.copy f h).toFun (ωSup c) = ωSup (c.map (g.copy f h))

Tactic:
rw [OrderHom.copy_eq]

Premises used: OrderHom.copy_eq
-- 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 δ
f : α → β
g : α →𝒄 β
h : f = (⇑g : (a : α) → β)
⊢ ∀ (c : Chain α), g.toFun (ωSup c) = ωSup (c.map g.toOrderHom)

Tactic:
g.map_ωSup'

Premises used: OmegaCompletePartialOrder.ContinuousHom.map_ωSup'
-- 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 δ
f : α → β
g : α →𝒄 β
h : f = (⇑g : (a : α) → β)
⊢ ∀ (c : Chain α), g.toFun (ωSup c) = ωSup (c.map g.toOrderHom)

Tactic:
exact g.map_ωSup'

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

Tactic:
DFunLike.ext f g h

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

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder β
inst_1 : OmegaCompletePartialOrder γ
f : β →𝒄 γ
⊢ f.comp id = f

Tactic:
rfl

Premises used: OrderHom.comp, OmegaCompletePartialOrder.ContinuousHom.comp, rfl
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder β
inst_1 : OmegaCompletePartialOrder γ
f : β →𝒄 γ
⊢ comp id f = f

Tactic:
rfl

Premises used: OrderHom.comp, OmegaCompletePartialOrder.ContinuousHom.comp, rfl
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
inst_3 : OmegaCompletePartialOrder δ
f : γ →𝒄 δ
g : β →𝒄 γ
h : α →𝒄 β
⊢ f.comp (g.comp h) = (f.comp g).comp h

Tactic:
rfl

Premises used: OrderHom.comp, OmegaCompletePartialOrder.ContinuousHom.comp, rfl
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
a : α
f : α →𝒄 β
⊢ Eq.{u_3 + 1} (α := β) (((↑f : α →o β) : (a : α) → β) a : β) ((f : (a : α) → β) a : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
mp :
  (∀ (i j : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) j : α) ≤ z) →
    ∀ (i : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) i : α) ≤ z
mpr :
  (∀ (i : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) i : α) ≤ z) →
    ∀ (i j : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) j : α) ≤ z
⊢ (∀ (i j : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) j : α) ≤ z) ↔
    ∀ (i : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) i : α) ≤ z

Tactic:
constructor
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
h : ∀ (i j : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) j : α) ≤ z
i : ℕ
⊢ (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) i : α) ≤ z

Tactic:
apply h
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
h : ∀ (i : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) i : α) ≤ z
i j : ℕ
apply :
  LE.le.{u_3} (α := β) ((((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) j : α) : β)
    ((((c₀ : (a : ℕ) → α →𝒄 β) (max i j) : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) (max i j) : α) : β)
⊢ (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) j : α) ≤ z

Tactic:
apply le_trans _ (h (max i j))

Premises used: Max.max, le_trans
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
h : ∀ (i : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) i : α) ≤ z
i j : ℕ
trans :
  LE.le.{u_3} (α := β) ((((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) j : α) : β)
    ((((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) (max i j) : α) : β)
trans₁ :
  LE.le.{u_3} (α := β) ((((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) (max i j) : α) : β)
    ((((c₀ : (a : ℕ) → α →𝒄 β) (max i j) : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) (max i j) : α) : β)
⊢ LE.le.{u_3} (α := β) ((((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) j : α) : β)
    ((((c₀ : (a : ℕ) → α →𝒄 β) (max i j) : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) (max i j) : α) : β)

Tactic:
trans c₀ i (c₁ (max i j))

Premises used: Max.max, DFunLike.coe
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
h : ∀ (i : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) i : α) ≤ z
i j : ℕ
a : LE.le (α := α) ((c₁ : (a : ℕ) → α) j : α) ((c₁ : (a : ℕ) → α) (max i j) : α)
⊢ LE.le.{u_3} (α := β) ((((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) j : α) : β)
    ((((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) (max i j) : α) : β)

Tactic:
apply (c₀ i).monotone

Premises used: OmegaCompletePartialOrder.ContinuousHom.monotone, DFunLike.coe
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
h : ∀ (i : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) i : α) ≤ z
i j : ℕ
a : j ≤ max i j
⊢ LE.le (α := α) ((c₁ : (a : ℕ) → α) j : α) ((c₁ : (a : ℕ) → α) (max i j) : α)

Tactic:
apply c₁.monotone

Premises used: OrderHom.monotone, OmegaCompletePartialOrder.Chain.toOrderHom
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
h : ∀ (i : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) i : α) ≤ z
i j : ℕ
⊢ j ≤ max i j

Tactic:
apply le_max_right

Premises used: le_max_right
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
h : ∀ (i : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) i : α) ≤ z
i j : ℕ
a : i ≤ max i j
⊢ LE.le.{u_3} (α := β) ((((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) (max i j) : α) : β)
    ((((c₀ : (a : ℕ) → α →𝒄 β) (max i j) : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) (max i j) : α) : β)

Tactic:
apply c₀.monotone

Premises used: OrderHom.monotone, OmegaCompletePartialOrder.Chain.toOrderHom
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
h : ∀ (i : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) i : α) ≤ z
i j : ℕ
⊢ i ≤ max i j

Tactic:
apply le_max_left

Premises used: le_max_left
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
rw :
  (∀ (b a : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) b : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) a : α) ≤ z) ↔
    ∀ (i : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) i : α) ≤ z
rw₁ rw₂ :
  (∀ (i : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) i : α) ≤ z) ↔
    ∀ (i : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) i : α) ≤ z
⊢ (∀ (j i : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) j : α) ≤ z) ↔
    ∀ (i : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) i : α) ≤ z

Tactic:
rw [forall_comm, forall_forall_merge]

Premises used: forall_comm, OmegaCompletePartialOrder.ContinuousHom.forall_forall_merge