awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
x : α
c : Chain (Part α)
h : some x ∈ c
h' : ∃ (a : α), some a ∈ c
⊢ Membership.mem (γ := Part α)
    (if h : ∃ (a : α), some a ∈ c then some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h) else none) x
have mpr : x ∈ some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h')
Tactic: rw [dif_pos h']
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (hypothesis)
Goal:
α : Type u_2
x : α
c : Chain (Part α)
h : some x ∈ c
h' : ∃ (a : α), some a ∈ c
⊢ x ∈ some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h')
have hh : some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h') ∈ c
Tactic: have hh := Classical.choose_spec h'
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
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 (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h')
have mpr : x ∈ some x
Tactic: rw [eq_of_chain hh h]
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
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 γ
⊢ f (ωSup c) = ωSup (c.map { toFun := f, monotone' := ⋯ })
have h : ∀ (a : α), f (ωSup c) a = ωSup (c.map { toFun := f, monotone' := sorry }) a
Tactic: ext a
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
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, map_ωSup' := map_ωSup' : α →𝒄 β } =
    { toOrderHom := toOrderHom_1, map_ωSup' := map_ωSup'_1 }
have e_toOrderHom : toOrderHom = toOrderHom_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : OrderHom.{u_2, v} α (Part β)
g : OrderHom.{u_2, v} α (β → Part γ)
⊢ ωSup (c.map (f.partBind g)) = ωSup (c.map f) >>= ωSup (c.map g)
have H : ∀ (c_1 : Part γ), ωSup (c.map (f.partBind g)) ≤ c_1 ↔ ωSup (c.map f) >>= ωSup (c.map g) ≤ c_1
Tactic: apply eq_of_forall_ge_iff
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : OrderHom.{u_2, v} α (Part β)
g : OrderHom.{u_2, v} α (β → Part γ)
x : Part γ
⊢ ωSup (c.map (f.partBind g)) ≤ x ↔ ωSup (c.map f) >>= ωSup (c.map g) ≤ x
have H : (∀ (i : ℕ), (c.map (f.partBind g) : (a : ℕ) → Part γ) i ≤ x) ↔ ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
Tactic: simp only [ωSup_le_iff, Part.bind_le]
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : OrderHom.{u_2, v} α (Part β)
g : OrderHom.{u_2, v} α (β → Part γ)
x : Part γ
⊢ (∀ (i : ℕ), (c.map (f.partBind g) : (a : ℕ) → Part γ) i ≤ x) ↔ ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
have H : (∀ (i : ℕ), (c.map (f.partBind g) : (a : ℕ) → Part γ) i ≤ x) → ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
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
⊢ (∀ (i : ℕ), (c.map (f.partBind g) : (a : ℕ) → Part γ) i ≤ x) ↔ ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
have H₁ : (∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x) → ∀ (i : ℕ), (c.map (f.partBind g) : (a : ℕ) → Part γ) i ≤ x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
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)
⊢ ωSup (c.map g) b ≤ x
have apply : ∀ (i : ℕ), ((c.map g).map (Pi.evalOrderHom (π := fun (a : β) ↦ Part γ) b) : (a : ℕ) → Part γ) i ≤ x
Tactic: apply ωSup_le _ _ _
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (hypothesis)
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
⊢ y ∈ x
have hb₁ : Part.some b ∈ c.map f
Tactic: simp only [Part.mem_ωSup] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
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
⊢ y ∈ x
have rcases : ∀ (j : ℕ) (hb : Part.some b = (c.map f : (a : ℕ) → Part β) j), y ∈ x
Tactic: rcases hb with ⟨j, hb⟩
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (hypothesis)
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
⊢ y ∈ x
have hb₁ : (c.map f : (a : ℕ) → Part β) j = Part.some b
Tactic: replace hb := hb.symm
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (hypothesis)
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
⊢ y ∈ x
have hb₁ : 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
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (hypothesis)
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
⊢ y ∈ x
have hb₁ : 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
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (hypothesis)
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
⊢ y ∈ x
have hy₁ : 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
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
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
⊢ y ∈ x
have a : Membership.mem (γ := Part γ) ((c.map (f.partBind g) : (a : ℕ) → Part γ) (max i j) : Part γ) y
Tactic: apply h''' (max i j)
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
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
⊢ Membership.mem (γ := Part γ) ((c.map (f.partBind g) : (a : ℕ) → Part γ) (max i j) : Part γ) y
have 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
Tactic: simp only [Part.mem_bind_iff, Chain.coe_map,
      Function.comp_apply, OrderHom.partBind_coe]
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (hypothesis)
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
⊢ y ∈ x
have 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
Tactic: simp only [Part.mem_bind_iff, Chain.coe_map,
      Function.comp_apply, OrderHom.partBind_coe] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
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
⊢ y ∈ x
have 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
Tactic: rcases hy with ⟨b, hb₀, hb₁⟩
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
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 ∈ x
have H : y ∈ ωSup (c.map g) b
Tactic: apply h''' b _
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
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
⊢ y ∈ x
have apply : b ∈ ωSup (c.map f)
Tactic: apply h''' b _
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
β γ : Type u_6
f : α → Part β
g : α → β → Part γ
hf : ωScottContinuous f
hg : ωScottContinuous g
c : Chain α
⊢ f (ωSup c) >>= g (ωSup c) =
    ωSup (c.map { toFun := fun (x : α) ↦ f x >>= g x, monotone' := ⋯ : OrderHom.{u_2, u_6} α (Part γ) })
have rw : ωSup
    (c.map
      ({ toFun := f, monotone' := sorry : OrderHom.{u_2, u_6} α (Part β) }.partBind
        { toFun := g, monotone' := sorry : OrderHom.{u_2, u_6} α (β → Part γ) })) =
  ωSup (c.map { toFun := fun (x : α) ↦ f x >>= g x, monotone' := sorry : OrderHom.{u_2, u_6} α (Part γ) })
Tactic: rw [hf.map_ωSup, hg.map_ωSup, ← ωSup_bind]
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
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 : α) ↦ f x <*> g x
have simp : ωScottContinuous.{u_2, u_6} (β := Part γ) fun (x : α) ↦ do
  let x_1 ← f x
  x_1 <$> g x
Tactic: simp only [seq_eq_bind_map]
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
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.copy f h).toFun (ωSup c) = ωSup (c.map (g.copy f h))
have rw : ∀ (c : Chain α), g.toFun (ωSup c) = ωSup (c.map g.toOrderHom)
Tactic: rw [OrderHom.copy_eq]
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
⊢ (∀ (i j : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) j : α) ≤ z) ↔
    ∀ (i : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) i : α) ≤ z
have mp : (∀ (i j : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) j : α) ≤ z) →
  ∀ (i : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) i : α) ≤ z
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
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
⊢ (∀ (i j : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) j : α) ≤ z) ↔
    ∀ (i : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) i : α) ≤ z
have mpr : (∀ (i : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) i : α) ≤ z) →
  ∀ (i j : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) j : α) ≤ z
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
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 : ℕ
⊢ (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) j : α) ≤ z
have apply : LE.le.{u_3} (α := β) ((((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) j : α) : β)
  ((((c₀ : (a : ℕ) → α →𝒄 β) (max i j) : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) (max i j) : α) : β)
Tactic: apply le_trans _ (h (max i j))
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
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 : ℕ
⊢ LE.le.{u_3} (α := β) ((((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) j : α) : β)
    ((((c₀ : (a : ℕ) → α →𝒄 β) (max i j) : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) (max i j) : α) : β)
have trans : LE.le.{u_3} (α := β) ((((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) j : α) : β)
  ((((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) (max i j) : α) : β)
Tactic: trans c₀ i (c₁ (max i j))
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
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) : α) : β)
⊢ LE.le.{u_3} (α := β) ((((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) j : α) : β)
    ((((c₀ : (a : ℕ) → α →𝒄 β) (max i j) : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) (max i j) : α) : β)
have 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) : α) : β)
Tactic: trans c₀ i (c₁ (max i j))
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
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 : ℕ
⊢ LE.le.{u_3} (α := β) ((((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) j : α) : β)
    ((((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) (max i j) : α) : β)
have a : LE.le (α := α) ((c₁ : (a : ℕ) → α) j : α) ((c₁ : (a : ℕ) → α) (max i j) : α)
Tactic: apply (c₀ i).monotone
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
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 : ℕ
⊢ LE.le (α := α) ((c₁ : (a : ℕ) → α) j : α) ((c₁ : (a : ℕ) → α) (max i j) : α)
have a : j ≤ max i j
Tactic: apply c₁.monotone
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
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 : ℕ
⊢ LE.le.{u_3} (α := β) ((((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) (max i j) : α) : β)
    ((((c₀ : (a : ℕ) → α →𝒄 β) (max i j) : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) (max i j) : α) : β)
have a : i ≤ max i j
Tactic: apply c₀.monotone
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
⊢ (∀ (j i : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) j : α) ≤ z) ↔
    ∀ (i : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) i : α) ≤ z
have rw : (∀ (b a : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) b : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) a : α) ≤ z) ↔
  ∀ (i : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) i : α) ≤ z
Tactic: rw [forall_comm, forall_forall_merge]
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
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
⊢ (∀ (j i : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) j : α) ≤ z) ↔
    ∀ (i : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) i : α) ≤ z
have rw₁ : (∀ (i : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) i : α) ≤ z) ↔
  ∀ (i : ℕ), (((c₀ : (a : ℕ) → α →𝒄 β) i : α →𝒄 β) : (a : α) → β) ((c₁ : (a : ℕ) → α) i : α) ≤ z
Tactic: rw [forall_comm, forall_forall_merge]
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
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.{u_2, u_4} (β := γ) fun (x : α) ↦ (f x : (a : β) → γ) (g x)
have apply : Monotone.{u_2, u_4} (β := γ) fun (x : α) ↦ (f x : (a : β) → γ) (g x)
Tactic: apply ωScottContinuous.of_monotone_map_ωSup ⟨?_, fun c ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
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
apply : Monotone.{u_2, u_4} (β := γ) fun (x : α) ↦ (f x : (a : β) → γ) (g x)
⊢ ωScottContinuous.{u_2, u_4} (β := γ) fun (x : α) ↦ (f x : (a : β) → γ) (g x)
have apply₁ : ∀ (c : Chain α),
  Eq.{u_4 + 1} (α := γ) ((f (ωSup c) : (a : β) → γ) (g (ωSup c)) : γ)
    (ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := sorry }) : γ)
Tactic: apply ωScottContinuous.of_monotone_map_ωSup ⟨?_, fun c ↦ ?_⟩