awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : Frame X
n_1 m : Nucleus X
x_1 y : X
n : Nucleus X
x : X
hx : (↑(rangeFactorization (⇑n : (a : X) → X) x) : X) ≤ x
⊢ (↑(Subtype.mk (p := fun (x : X) ↦ Membership.mem (γ := Set X) (range (ι := X) (⇑n : (a : X) → X)) x) x ⋯) : X) =
    (↑(rangeFactorization (⇑n : (a : X) → X) x) : X)

Tactic:
le_apply.antisymm hx

Premises used: LE.le.antisymm, Nucleus.le_apply
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : Frame X
n_1 m : Nucleus X
x_1 y : X
n : Nucleus X
x : X
hx : (↑(rangeFactorization (⇑n : (a : X) → X) x) : X) ≤ x
⊢ (↑(Subtype.mk (p := fun (x : X) ↦ Membership.mem (γ := Set X) (range (ι := X) (⇑n : (a : X) → X)) x) x ⋯) : X) =
    (↑(rangeFactorization (⇑n : (a : X) → X) x) : X)

Tactic:
exact le_apply.antisymm hx

Premises used: LE.le.antisymm, Nucleus.le_apply
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : Frame X
n m : Nucleus X
x y : X
a : (↑(range (ι := X) (⇑n : (a : X) → X)) : Type u_1)
s : Set (↑(range (ι := X) (⇑n : (a : X) → X)) : Type u_1)
simp_rw :
  (↑a : X) ⊓
      (↑(rangeFactorization (⇑n : (a : X) → X)
            (sSup
              (Subtype.val (p := fun (x : X) ↦ Membership.mem (γ := Set X) (range (ι := X) (⇑n : (a : X) → X)) x) ''
                s))) :
        X) ≤
    (↑(rangeFactorization (⇑n : (a : X) → X)
          (sSup
            (image (α := (↑(range (ι := X) (⇑n : (a : X) → X)) : Type u_1))
              (Subtype.val (p := fun (x : X) ↦ Membership.mem (γ := Set X) (range (ι := X) (⇑n : (a : X) → X)) x))
              (range fun (x : Subtype (Membership.mem s)) ↦ a ⊓ (↑x : (↑(range (⇑n : (a : X) → X)) : Type u_1)))))) :
      X)
⊢ a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b

Tactic:
simp_rw [← Subtype.coe_le_coe, iSup_subtype', iSup, sSup, n.giAux.gc.u_inf]

Premises used: iSup, iSup_subtype', Subtype.coe_le_coe, GaloisConnection.u_inf, _private.0.Nucleus.giAux, SupSet.sSup, GaloisInsertion.gc
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : Frame X
n m : Nucleus X
x y : X
a : (↑(range (ι := X) (⇑n : (a : X) → X)) : Type u_1)
s : Set (↑(range (ι := X) (⇑n : (a : X) → X)) : Type u_1)
rw :
  LE.le (α := X)
    ((n : (a : X) → X)
        ((↑a : X) ⊓
          sSup
            (Subtype.val (p := fun (x : X) ↦ Membership.mem (γ := Set X) (range (ι := X) (⇑n : (a : X) → X)) x) '' s)) :
      X)
    ((↑(rangeFactorization (⇑n : (a : X) → X)
            (sSup
              (image (α := (↑(range (ι := X) (⇑n : (a : X) → X)) : Type u_1))
                (Subtype.val (p := fun (x : X) ↦ Membership.mem (γ := Set X) (range (ι := X) (⇑n : (a : X) → X)) x))
                (range fun (x : Subtype (Membership.mem s)) ↦ a ⊓ (↑x : (↑(range (⇑n : (a : X) → X)) : Type u_1)))))) :
        X) :
      X)
⊢ (↑a : X) ⊓
      (↑(rangeFactorization (⇑n : (a : X) → X)
            (sSup
              (Subtype.val (p := fun (x : X) ↦ Membership.mem (γ := Set X) (range (ι := X) (⇑n : (a : X) → X)) x) ''
                s))) :
        X) ≤
    (↑(rangeFactorization (⇑n : (a : X) → X)
          (sSup
            (image (α := (↑(range (ι := X) (⇑n : (a : X) → X)) : Type u_1))
              (Subtype.val (p := fun (x : X) ↦ Membership.mem (γ := Set X) (range (ι := X) (⇑n : (a : X) → X)) x))
              (range fun (x : Subtype (Membership.mem s)) ↦ a ⊓ (↑x : (↑(range (⇑n : (a : X) → X)) : Type u_1)))))) :
      X)

Tactic:
rw [rangeFactorization_coe, ← mem_range.1 a.prop, ← map_inf]

Premises used: Set.rangeFactorization_coe, Nucleus.mem_range, Subtype.prop, Iff.mp, Nucleus.map_inf
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : Frame X
n m : Nucleus X
x y : X
a : (↑(range (ι := X) (⇑n : (a : X) → X)) : Type u_1)
s : Set (↑(range (ι := X) (⇑n : (a : X) → X)) : Type u_1)
a₁ :
  (↑a : X) ⊓
      sSup (Subtype.val (p := fun (x : X) ↦ Membership.mem (γ := Set X) (range (ι := X) (⇑n : (a : X) → X)) x) '' s) ≤
    sSup
      (image (α := (↑(range (ι := X) (⇑n : (a : X) → X)) : Type u_1))
        (Subtype.val (p := fun (x : X) ↦ Membership.mem (γ := Set X) (range (ι := X) (⇑n : (a : X) → X)) x))
        (range fun (x : Subtype (Membership.mem s)) ↦ a ⊓ (↑x : (↑(range (⇑n : (a : X) → X)) : Type u_1))))
⊢ LE.le (α := X)
    ((n : (a : X) → X)
        ((↑a : X) ⊓
          sSup
            (Subtype.val (p := fun (x : X) ↦ Membership.mem (γ := Set X) (range (ι := X) (⇑n : (a : X) → X)) x) '' s)) :
      X)
    ((↑(rangeFactorization (⇑n : (a : X) → X)
            (sSup
              (image (α := (↑(range (ι := X) (⇑n : (a : X) → X)) : Type u_1))
                (Subtype.val (p := fun (x : X) ↦ Membership.mem (γ := Set X) (range (ι := X) (⇑n : (a : X) → X)) x))
                (range fun (x : Subtype (Membership.mem s)) ↦ a ⊓ (↑x : (↑(range (⇑n : (a : X) → X)) : Type u_1)))))) :
        X) :
      X)

Tactic:
apply n.monotone

Premises used: Nucleus.monotone
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : Frame X
n m : Nucleus X
x y : X
a : (↑(range (ι := X) (⇑n : (a : X) → X)) : Type u_1)
s : Set (↑(range (ι := X) (⇑n : (a : X) → X)) : Type u_1)
a₁ :
  LE.le.{u_1} (α := X)
    (⨆ b ∈ Subtype.val (p := fun (x : X) ↦ Membership.mem (γ := Set X) (range (ι := X) (⇑n : (a : X) → X)) x) '' s,
      (↑a : X) ⊓ b)
    (sSup
      (image (α := (↑(range (ι := X) (⇑n : (a : X) → X)) : Type u_1))
        (Subtype.val (p := fun (x : X) ↦ Membership.mem (γ := Set X) (range (ι := X) (⇑n : (a : X) → X)) x))
        (range fun (x : Subtype (Membership.mem s)) ↦ a ⊓ (↑x : (↑(range (⇑n : (a : X) → X)) : Type u_1)))))
a₂ :
  LE.le.{u_1} (α := X)
    (⨆ b ∈ Subtype.val (p := fun (x : X) ↦ Membership.mem (γ := Set X) (range (ι := X) (⇑n : (a : X) → X)) x) '' s,
      (↑a : X) ⊓ b)
    (⨆ (a_1 : (↑(range (ι := X) (⇑n : (a : X) → X)) : Type u_1)),
      ⨆ (_ :
        Membership.mem (γ := Set (↑(range (ι := X) (⇑n : (a : X) → X)) : Type u_1))
          (range fun (x : Subtype (Membership.mem s)) ↦ a ⊓ (↑x : (↑(range (⇑n : (a : X) → X)) : Type u_1))) a_1),
        (↑a_1 : X))
a₃ :
  LE.le.{u_1} (α := X)
    (⨆ b ∈ Subtype.val (p := fun (x : X) ↦ Membership.mem (γ := Set X) (range (ι := X) (⇑n : (a : X) → X)) x) '' s,
      (↑a : X) ⊓ b)
    (⨆ (i : Subtype (Membership.mem s)), (↑(a ⊓ (↑i : (↑(range (⇑n : (a : X) → X)) : Type u_1))) : X))
a₄ :
  LE.le.{u_1} (α := X) (⨆ b ∈ s, (↑a : X) ⊓ (↑b : X))
    (⨆ (i : Subtype (Membership.mem s)), (↑(a ⊓ (↑i : (↑(range (⇑n : (a : X) → X)) : Type u_1))) : X))
a₅ :
  LE.le.{u_1} (α := X)
    (⨆ (x : Subtype (Membership.mem s)), (↑a : X) ⊓ (↑(↑x : (↑(range (⇑n : (a : X) → X)) : Type u_1)) : X))
    (⨆ (i : Subtype (Membership.mem s)), (↑(a ⊓ (↑i : (↑(range (⇑n : (a : X) → X)) : Type u_1))) : X))
a₆ :
  LE.le.{u_1} (α := X)
    (⨆ (x : Subtype (Membership.mem s)), (↑a : X) ⊓ (↑(↑x : (↑(range (⇑n : (a : X) → X)) : Type u_1)) : X))
    (⨆ (x : Subtype (Membership.mem s)), (↑a : X) ⊓ (↑(↑x : (↑(range (⇑n : (a : X) → X)) : Type u_1)) : X))
⊢ (↑a : X) ⊓
      sSup (Subtype.val (p := fun (x : X) ↦ Membership.mem (γ := Set X) (range (ι := X) (⇑n : (a : X) → X)) x) '' s) ≤
    sSup
      (image (α := (↑(range (ι := X) (⇑n : (a : X) → X)) : Type u_1))
        (Subtype.val (p := fun (x : X) ↦ Membership.mem (γ := Set X) (range (ι := X) (⇑n : (a : X) → X)) x))
        (range fun (x : Subtype (Membership.mem s)) ↦ a ⊓ (↑x : (↑(range (⇑n : (a : X) → X)) : Type u_1))))

Tactic:
simp_rw [inf_sSup_eq, sSup_image, iSup_range, iSup_image, iSup_subtype', n.giAux.gc.u_inf,
      le_rfl]

Premises used: le_rfl, iSup_image, iSup_subtype', iSup_range, inf_sSup_eq, GaloisConnection.u_inf, _private.0.Nucleus.giAux, sSup_image, GaloisInsertion.gc
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : Frame X
n_1 m : Nucleus X
x y : X
n : Nucleus X
a b : X
a₁ :
  Eq (α := X) (↑(rangeFactorization (⇑n : (a : X) → X) (a ⊓ b)) : X)
    (↑(rangeFactorization (⇑n : (a : X) → X) a ⊓ rangeFactorization (⇑n : (a : X) → X) b) : X)
⊢ Eq (α := (↑(range (ι := X) (⇑n : (a : X) → X)) : Type u_1)) (rangeFactorization (⇑n : (a : X) → X) (a ⊓ b))
    (rangeFactorization (⇑n : (a : X) → X) a ⊓ rangeFactorization (⇑n : (a : X) → X) b)

Tactic:
ext
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : Frame X
n_1 m : Nucleus X
x y : X
n : Nucleus X
a b : X
⊢ Eq (α := X) (↑(rangeFactorization (⇑n : (a : X) → X) (a ⊓ b)) : X)
    (↑(rangeFactorization (⇑n : (a : X) → X) a ⊓ rangeFactorization (⇑n : (a : X) → X) b) : X)

Tactic:
map_inf

Premises used: Nucleus.map_inf
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : Frame X
n_1 m : Nucleus X
x y : X
n : Nucleus X
a b : X
⊢ Eq (α := X) (↑(rangeFactorization (⇑n : (a : X) → X) (a ⊓ b)) : X)
    (↑(rangeFactorization (⇑n : (a : X) → X) a ⊓ rangeFactorization (⇑n : (a : X) → X) b) : X)

Tactic:
exact map_inf

Premises used: Nucleus.map_inf
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : Frame X
n_1 m : Nucleus X
x y : X
n : Nucleus X
a : Eq (α := X) (↑(rangeFactorization (⇑n : (a : X) → X) ⊤) : X) (↑⊤ : X)
⊢ Eq (α := (↑(range (ι := X) (⇑n : (a : X) → X)) : Type u_1)) (rangeFactorization (⇑n : (a : X) → X) ⊤) ⊤

Tactic:
ext
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : Frame X
n_1 m : Nucleus X
x y : X
n : Nucleus X
⊢ Eq (α := X) (↑(rangeFactorization (⇑n : (a : X) → X) ⊤) : X) (↑⊤ : X)

Tactic:
map_top n

Premises used: TopHomClass.map_top
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : Frame X
n_1 m : Nucleus X
x y : X
n : Nucleus X
⊢ Eq (α := X) (↑(rangeFactorization (⇑n : (a : X) → X) ⊤) : X) (↑⊤ : X)

Tactic:
exact map_top n

Premises used: TopHomClass.map_top
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : Frame X
n_1 m : Nucleus X
x y : X
n : Nucleus X
s : Set X
rw :
  Eq (α := (↑(range (ι := X) (⇑n : (a : X) → X)) : Type u_1)) (⨆ a ∈ s, rangeFactorization (⇑n : (a : X) → X) a)
    (sSup (rangeFactorization (⇑n : (a : X) → X) '' s))
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := (↑(range (ι := X) (⇑n : (a : X) → X)) : Type u_1))
    (⨆ a ∈ s, rangeFactorization (⇑n : (a : X) → X) a) (⨆ a ∈ s, rangeFactorization (⇑n : (a : X) → X) a)
⊢ Eq (α := (↑(range (ι := X) (⇑n : (a : X) → X)) : Type u_1)) (rangeFactorization (⇑n : (a : X) → X) (sSup s))
    (sSup (rangeFactorization (⇑n : (a : X) → X) '' s))

Tactic:
rw [n.giAux.gc.l_sSup, sSup_image]

Premises used: GaloisConnection.l_sSup, _private.0.Nucleus.giAux, sSup_image, GaloisInsertion.gc
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : Frame X
n m : Nucleus X
h : Eq (α := X → X) (Function.comp (β := X) (⇑n : (a : X) → X) (⇑m : (a : X) → X)) (⇑m : (a : X) → X)
rw : LE.le (α := (a : X) → X) (⇑n : (a : X) → X) (Function.comp (β := X) (⇑n : (a : X) → X) (⇑m : (a : X) → X))
⊢ n ≤ m

Tactic:
rw [← coe_le_coe, ← h]

Premises used: Nucleus.coe_le_coe
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : Frame X
n m : Nucleus X
h : Eq (α := X → X) (Function.comp (β := X) (⇑n : (a : X) → X) (⇑m : (a : X) → X)) (⇑m : (a : X) → X)
⊢ LE.le (α := (a : X) → X) (⇑n : (a : X) → X) (Function.comp (β := X) (⇑n : (a : X) → X) (⇑m : (a : X) → X))

Tactic:
fun _ ↦ monotone le_apply

Premises used: Nucleus.monotone, Nucleus.le_apply
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : Frame X
n m : Nucleus X
h : Eq (α := X → X) (Function.comp (β := X) (⇑n : (a : X) → X) (⇑m : (a : X) → X)) (⇑m : (a : X) → X)
⊢ LE.le (α := (a : X) → X) (⇑n : (a : X) → X) (Function.comp (β := X) (⇑n : (a : X) → X) (⇑m : (a : X) → X))

Tactic:
exact fun _ ↦ monotone le_apply

Premises used: Nucleus.monotone, Nucleus.le_apply
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : Frame X
n m : Nucleus X
h : Subset (α := Set X) (range (ι := X) (⇑m : (a : X) → X)) (range (ι := X) (⇑n : (a : X) → X))
x : X
rw : LE.le (α := (fun (a : X) ↦ X) x) ((n : (a : X) → X) x : X) ((n : (a : X) → X) ((m : (a : X) → X) x : X) : X)
⊢ LE.le (α := (fun (a : X) ↦ X) x) ((n : (a : X) → X) x : X) ((m : (a : X) → X) x : X)

Tactic:
rw [← mem_range.mp (Set.range_subset_iff.mp h x)]

Premises used: Nucleus.mem_range, Iff.mp, Set.range_subset_iff
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : Frame X
n m : Nucleus X
h : Subset (α := Set X) (range (ι := X) (⇑m : (a : X) → X)) (range (ι := X) (⇑n : (a : X) → X))
x : X
⊢ LE.le (α := (fun (a : X) ↦ X) x) ((n : (a : X) → X) x : X) ((n : (a : X) → X) ((m : (a : X) → X) x : X) : X)

Tactic:
n.monotone m.le_apply

Premises used: Nucleus.monotone, Nucleus.le_apply
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : Frame X
n m : Nucleus X
h : Subset (α := Set X) (range (ι := X) (⇑m : (a : X) → X)) (range (ι := X) (⇑n : (a : X) → X))
x : X
⊢ LE.le (α := (fun (a : X) ↦ X) x) ((n : (a : X) → X) x : X) ((n : (a : X) → X) ((m : (a : X) → X) x : X) : X)

Tactic:
exact n.monotone m.le_apply

Premises used: Nucleus.monotone, Nucleus.le_apply
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : ℕ → α
hf : Monotone f
⊢ ∀ ⦃a₂ : Chain α⦄,
    Eq.{max 1 (u_2 + 1)} (α := (a : ℕ) → α)
        ((fun (c : Chain α) ↦ ((⇑c.toOrderHom : (a : ℕ) → α) : (a : ℕ) → α)) { toFun := f, monotone' := hf })
        ((fun (c : Chain α) ↦ ((⇑c.toOrderHom : (a : ℕ) → α) : (a : ℕ) → α)) a₂) →
      { toFun := f, monotone' := hf : Chain α } = a₂

Tactic:
congr!
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : Preorder α
f g : Chain α
h : Eq (α := (a : ℕ) → α) (⇑f : (a : ℕ) → α) (⇑g : (a : ℕ) → α)
⊢ f = g

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : Preorder α
c : Chain α
⊢ Eq (α := (a : ℕ) → α) (⇑c.toOrderHom : (a : ℕ) → α) (⇑c : (a : ℕ) → α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : Preorder α
c : Chain α
⊢ IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α))

Tactic:
Monotone.isChain_range (OrderHomClass.mono c)

Premises used: OrderHomClass.mono, Monotone.isChain_range
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : Preorder α
c : Chain α
⊢ Directed (ι := ℕ) (fun (x1 x2 : α) ↦ x1 ≤ x2) (⇑c : (a : ℕ) → α)

Tactic:
directedOn_range.1 c.isChain_range.directedOn

Premises used: IsChain.directedOn, directedOn_range, Iff.mp, OmegaCompletePartialOrder.Chain.isChain_range
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
c : Chain α
f : α →o β
⊢ Eq (α := (a : ℕ) → β) (⇑(c.map f) : (a : ℕ) → β) (Function.comp (β := α) (⇑f : (a : α) → β) (⇑c : (a : ℕ) → α))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
c : Chain α
f : α →o β
x : α
⊢ x ∈ c → Membership.mem (α := β) (c.map f) ((f : (a : α) → β) x : β)

Tactic:
fun ⟨i, h⟩ => ⟨i, h.symm ▸ rfl⟩

Premises used: Membership.mem, Eq.rec, _private.0.OmegaCompletePartialOrder.Chain.mem_map.match_1, Exists.intro, OmegaCompletePartialOrder.Chain.map, Eq.symm, DFunLike.coe, rfl
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
c : Chain α
f : α →o β
b : β
⊢ b ∈ c.map f → ∃ a ∈ c, (f : (a : α) → β) a = b

Tactic:
fun ⟨i, h⟩ => ⟨c i, ⟨i, rfl⟩, h.symm⟩

Premises used: Membership.mem, Exists, _private.0.OmegaCompletePartialOrder.Chain.exists_of_mem_map.match_1, And, And.intro, Exists.intro, Eq.symm, Eq, DFunLike.coe, rfl
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
c : Chain α
f : α →o β
b : β
h : ∃ a ∈ c, (f : (a : α) → β) a = b
rcases : ∀ (w : α) (h : w ∈ c) (h' : (f : (a : α) → β) w = b), b ∈ c.map f
⊢ b ∈ c.map f

Tactic:
rcases h with ⟨w, h, h'⟩
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
c : Chain α
f : α →o β
b : β
w : α
h : w ∈ c
h' : (f : (a : α) → β) w = b
subst : Membership.mem (α := β) (c.map f) ((f : (a : α) → β) w : β)
⊢ b ∈ c.map f

Tactic:
subst b
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
c : Chain α
f : α →o β
w : α
h : w ∈ c
⊢ Membership.mem (α := β) (c.map f) ((f : (a : α) → β) w : β)

Tactic:
apply mem_map c _ h

Premises used: OmegaCompletePartialOrder.Chain.mem_map
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : Preorder α
c : Chain α
h : ∀ (x : ℕ), Eq (α := α) ((c.map OrderHom.id : (a : ℕ) → α) x : α) ((c : (a : ℕ) → α) x : α)
⊢ c.map OrderHom.id = c

Tactic:
ext
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : Preorder α
c : Chain α
x : ℕ
⊢ Eq (α := α) ((c.map OrderHom.id : (a : ℕ) → α) x : α) ((c : (a : ℕ) → α) x : α)

Tactic:
simp
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
c : Chain α
f : α →o β
g : β →o γ
⊢ (c.map f).map g = c.map (g.comp f)

Tactic:
rfl

Premises used: OrderHom.comp, OmegaCompletePartialOrder.Chain.map, rfl
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
c : Chain α
f g : α →o β
h : f ≤ g
⊢ c.map f ≤ c.map g

Tactic:
fun _ ↦ ⟨_, h _⟩

Premises used: Exists.intro, DFunLike.coe, OmegaCompletePartialOrder.Chain.toOrderHom
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
c₀ : Chain α
c₁ : Chain β
n : ℕ
⊢ Eq (α := α × β) ((c₀.zip c₁ : (a : ℕ) → α × β) n : α × β) (((c₀ : (a : ℕ) → α) n, (c₁ : (a : ℕ) → β) n) : α × β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
c c' : Chain α
f : α →o β
g : β →o γ
a b : α
hab : a ≤ b
x x_1 : ℕ
h : x ≤ x_1
⊢ LE.le.{u_2} (α := α)
    ((fun (x : ℕ) ↦
        (match (motive := ℕ → α) x with
          | 0 => a
          | x => b :
          α))
      x)
    ((fun (x : ℕ) ↦
        (match (motive := ℕ → α) x with
          | 0 => a
          | x => b :
          α))
      x_1)

Tactic:
aesop
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : Preorder α
a b : α
hab : a ≤ b
⊢ (pair a b hab : (a : ℕ) → α) 0 = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : Preorder α
a b : α
hab : a ≤ b
n : ℕ
⊢ (pair a b hab : (a : ℕ) → α) (n + 1) = b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : Preorder α
a b : α
hab : a ≤ b
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) (Set.range (ι := ℕ) (⇑(pair a b hab) : (a : ℕ) → α)) x ↔
      Membership.mem (γ := Set α) {a, b} x
⊢ Eq (α := Set α) (Set.range (ι := ℕ) (⇑(pair a b hab) : (a : ℕ) → α)) {a, b}

Tactic:
ext
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : Preorder α
a b : α
hab : a ≤ b
x : α
⊢ ((pair a b hab : (a : ℕ) → α) 0 = x ∨ ∃ (n : ℕ), (pair a b hab : (a : ℕ) → α) (n + 1) = x) ↔
    Membership.mem (γ := Set α) {a, b} x

Tactic:
aesop
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : Preorder α
a b : α
hab : a ≤ b
x : α
⊢ Membership.mem (γ := Set α) (Set.range (ι := ℕ) (⇑(pair a b hab) : (a : ℕ) → α)) x ↔
    Membership.mem (γ := Set α) {a, b} x

Tactic:
exact Nat.or_exists_add_one.symm.trans (by aesop)

Premises used: Nat.or_exists_add_one, Iff.trans, Iff.symm
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
h :
  ∀ (n : ℕ),
    Eq (α := α × β) (((pair a₁ a₂ ha).zip (pair b₁ b₂ hb) : (a : ℕ) → α × β) n : α × β)
      ((pair (a₁, b₁) (a₂, b₂) ⋯ : (a : ℕ) → α × β) n : α × β)
⊢ (pair a₁ a₂ ha).zip (pair b₁ b₂ hb) = pair (a₁, b₁) (a₂, b₂) ⋯

Tactic:
ext n : 2
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
n : ℕ
h :
  Eq (α := α × β) (((pair a₁ a₂ ha).zip (pair b₁ b₂ hb) : (a : ℕ) → α × β) 0 : α × β)
    ((pair (a₁, b₁) (a₂, b₂) ⋯ : (a : ℕ) → α × β) 0 : α × β)
h₁ :
  ∀ (n : ℕ),
    Eq (α := α × β) (((pair a₁ a₂ ha).zip (pair b₁ b₂ hb) : (a : ℕ) → α × β) (n + 1) : α × β)
      ((pair (a₁, b₁) (a₂, b₂) ⋯ : (a : ℕ) → α × β) (n + 1) : α × β)
⊢ Eq (α := α × β) (((pair a₁ a₂ ha).zip (pair b₁ b₂ hb) : (a : ℕ) → α × β) n : α × β)
    ((pair (a₁, b₁) (a₂, b₂) ⋯ : (a : ℕ) → α × β) n : α × β)

Tactic:
cases n
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
⊢ Eq (α := α × β) (((pair a₁ a₂ ha).zip (pair b₁ b₂ hb) : (a : ℕ) → α × β) 0 : α × β)
    ((pair (a₁, b₁) (a₂, b₂) ⋯ : (a : ℕ) → α × β) 0 : α × β)

Tactic:
rfl
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
n : ℕ
⊢ Eq (α := α × β) (((pair a₁ a₂ ha).zip (pair b₁ b₂ hb) : (a : ℕ) → α × β) (n + 1) : α × β)
    ((pair (a₁, b₁) (a₂, b₂) ⋯ : (a : ℕ) → α × β) (n + 1) : α × β)

Tactic:
rfl
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : OmegaCompletePartialOrder α
inst_1 : PartialOrder β
f : β →o α
ωSup₀ : Chain β → β
h : ∀ (x y : β), LE.le.{u_2} (α := α) ((f : (a : β) → α) x : α) ((f : (a : β) → α) y : α) → x ≤ y
h' : ∀ (c : Chain β), (f : (a : β) → α) (ωSup₀ c) = ωSup (c.map f)
c : Chain β
i : ℕ
rw : (f : (a : β) → α) ((c : (a : ℕ) → β) i : β) ≤ ωSup (c.map f)
⊢ LE.le.{u_2} (α := α) ((f : (a : β) → α) ((c : (a : ℕ) → β) i : β) : α) ((f : (a : β) → α) (ωSup₀ c) : α)

Tactic:
rw [h']
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : OmegaCompletePartialOrder α
inst_1 : PartialOrder β
f : β →o α
ωSup₀ : Chain β → β
h : ∀ (x y : β), LE.le.{u_2} (α := α) ((f : (a : β) → α) x : α) ((f : (a : β) → α) y : α) → x ≤ y
h' : ∀ (c : Chain β), (f : (a : β) → α) (ωSup₀ c) = ωSup (c.map f)
c : Chain β
i : ℕ
⊢ (f : (a : β) → α) ((c : (a : ℕ) → β) i : β) ≤ ωSup (c.map f)

Tactic:
apply le_ωSup (c.map f)

Premises used: OmegaCompletePartialOrder.le_ωSup, OmegaCompletePartialOrder.Chain.map
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : OmegaCompletePartialOrder α
inst_1 : PartialOrder β
f : β →o α
ωSup₀ : Chain β → β
h : ∀ (x y : β), LE.le.{u_2} (α := α) ((f : (a : β) → α) x : α) ((f : (a : β) → α) y : α) → x ≤ y
h' : ∀ (c : Chain β), (f : (a : β) → α) (ωSup₀ c) = ωSup (c.map f)
c : Chain β
x : β
hx : ∀ (i : ℕ), (c : (a : ℕ) → β) i ≤ x
rw : ωSup (c.map f) ≤ (f : (a : β) → α) x
⊢ LE.le.{u_2} (α := α) ((f : (a : β) → α) (ωSup₀ c) : α) ((f : (a : β) → α) x : α)

Tactic:
rw [h']
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : OmegaCompletePartialOrder α
inst_1 : PartialOrder β
f : β →o α
ωSup₀ : Chain β → β
h : ∀ (x y : β), LE.le.{u_2} (α := α) ((f : (a : β) → α) x : α) ((f : (a : β) → α) y : α) → x ≤ y
h' : ∀ (c : Chain β), (f : (a : β) → α) (ωSup₀ c) = ωSup (c.map f)
c : Chain β
x : β
hx : ∀ (i : ℕ), (c : (a : ℕ) → β) i ≤ x
a : ∀ (i : ℕ), LE.le (α := α) ((c.map f : (a : ℕ) → α) i : α) ((f : (a : β) → α) x : α)
⊢ ωSup (c.map f) ≤ (f : (a : β) → α) x

Tactic:
apply ωSup_le

Premises used: OmegaCompletePartialOrder.ωSup_le
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : OmegaCompletePartialOrder α
inst_1 : PartialOrder β
f : β →o α
ωSup₀ : Chain β → β
h : ∀ (x y : β), LE.le.{u_2} (α := α) ((f : (a : β) → α) x : α) ((f : (a : β) → α) y : α) → x ≤ y
h' : ∀ (c : Chain β), (f : (a : β) → α) (ωSup₀ c) = ωSup (c.map f)
c : Chain β
x : β
hx : ∀ (i : ℕ), (c : (a : ℕ) → β) i ≤ x
i : ℕ
⊢ LE.le (α := α) ((c.map f : (a : ℕ) → α) i : α) ((f : (a : β) → α) x : α)

Tactic:
apply f.monotone (hx i)

Premises used: OrderHom.monotone