awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
Goal:
X : Type u_1
inst : Frame X
n_1 m_1 : Nucleus X
x_1 y_1 : X
m n : Nucleus X
x y : X
hy : y ≥ x
⊢ Eq (α := X)
    ((m : (a : X) → X) ((m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X) ⇨
        (n : (a : X) → X) ((m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X) :
      X)
    ((m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X)
have rw : Eq (α := X)
  ((m : (a : X) → X) ((m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X) ⇨ (m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X)
  ((m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X)
Tactic: rw [map_himp_apply, himp_himp, ← map_inf, inf_of_le_right (le_trans n.le_apply le_himp)]
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
Goal:
X : Type u_1
inst : Frame X
n_1 m_1 : Nucleus X
x_1 y_1 : X
m n : Nucleus X
x y : X
hy : y ≥ x
rw :
  Eq (α := X)
    ((m : (a : X) → X) ((m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X) ⇨ (m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X)
    ((m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X)
⊢ Eq (α := X)
    ((m : (a : X) → X) ((m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X) ⇨
        (n : (a : X) → X) ((m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X) :
      X)
    ((m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X)
have rw₁ : Eq (α := X)
  ((m : (a : X) → X) ((m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X) ⊓ (m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X)
  ((m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X)
Tactic: rw [map_himp_apply, himp_himp, ← map_inf, inf_of_le_right (le_trans n.le_apply le_himp)]
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
Goal:
X : Type u_1
inst : Frame X
n_1 m_1 : Nucleus X
x_1 y_1 : X
m n : Nucleus X
x y : X
hy : y ≥ x
rw :
  Eq (α := X)
    ((m : (a : X) → X) ((m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X) ⇨ (m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X)
    ((m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X)
rw₁ :
  Eq (α := X)
    ((m : (a : X) → X) ((m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X) ⊓ (m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X)
    ((m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X)
⊢ Eq (α := X)
    ((m : (a : X) → X) ((m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X) ⇨
        (n : (a : X) → X) ((m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X) :
      X)
    ((m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X)
have rw₂ : Eq (α := X) ((m : (a : X) → X) (((m : (a : X) → X) y ⇨ (n : (a : X) → X) y) ⊓ y : X) ⇨ (n : (a : X) → X) y : X)
  ((m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X)
Tactic: rw [map_himp_apply, himp_himp, ← map_inf, inf_of_le_right (le_trans n.le_apply le_himp)]
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
Goal:
X : Type u_1
inst : Frame X
n_1 m_1 : Nucleus X
x_1 y_1 : X
m n : Nucleus X
x y : X
hy : y ≥ x
rw :
  Eq (α := X)
    ((m : (a : X) → X) ((m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X) ⇨ (m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X)
    ((m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X)
rw₁ :
  Eq (α := X)
    ((m : (a : X) → X) ((m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X) ⊓ (m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X)
    ((m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X)
rw₂ :
  Eq (α := X) ((m : (a : X) → X) (((m : (a : X) → X) y ⇨ (n : (a : X) → X) y) ⊓ y : X) ⇨ (n : (a : X) → X) y : X)
    ((m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X)
⊢ Eq (α := X)
    ((m : (a : X) → X) ((m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X) ⇨
        (n : (a : X) → X) ((m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X) :
      X)
    ((m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X)
have rw₃ : Eq (α := X) ((m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X) ((m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X)
Tactic: rw [map_himp_apply, himp_himp, ← map_inf, inf_of_le_right (le_trans n.le_apply le_himp)]
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
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 ⋯ =
    rangeFactorization (⇑n : (a : X) → X) x
have a : (↑(Subtype.mk (p := fun (x : X) ↦ Membership.mem (γ := Set X) (range (ι := X) (⇑n : (a : X) → X)) x) x sorry) : X) =
  (↑(rangeFactorization (⇑n : (a : X) → X) x) : X)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
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 ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b
have 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)
Tactic: simp_rw [← Subtype.coe_le_coe, iSup_subtype', iSup, sSup, n.giAux.gc.u_inf]
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
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 : 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)
have 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)
Tactic: rw [rangeFactorization_coe, ← mem_range.1 a.prop, ← map_inf]
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
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)
⊢ 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)
have 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))))
Tactic: apply n.monotone
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
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 : 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))))
have 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)))))
Tactic: simp_rw [inf_sSup_eq, sSup_image, iSup_range, iSup_image, iSup_subtype', n.giAux.gc.u_inf,
      le_rfl]
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
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 : 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))))
have 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))
Tactic: simp_rw [inf_sSup_eq, sSup_image, iSup_range, iSup_image, iSup_subtype', n.giAux.gc.u_inf,
      le_rfl]
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
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 : 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))))
have 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))
Tactic: simp_rw [inf_sSup_eq, sSup_image, iSup_range, iSup_image, iSup_subtype', n.giAux.gc.u_inf,
      le_rfl]
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
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 : 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))))
have 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))
Tactic: simp_rw [inf_sSup_eq, sSup_image, iSup_range, iSup_image, iSup_subtype', n.giAux.gc.u_inf,
      le_rfl]
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
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 : 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))))
have 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))
Tactic: simp_rw [inf_sSup_eq, sSup_image, iSup_range, iSup_image, iSup_subtype', n.giAux.gc.u_inf,
      le_rfl]
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
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 : 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))))
have 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))
Tactic: simp_rw [inf_sSup_eq, sSup_image, iSup_range, iSup_image, iSup_subtype', n.giAux.gc.u_inf,
      le_rfl]
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
Goal:
X : Type u_1
inst : Frame X
n_1 m : Nucleus X
x y : X
n : Nucleus X
a 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)
have a₁ : Eq (α := X) (↑(rangeFactorization (⇑n : (a : X) → X) (a ⊓ b)) : X)
  (↑(rangeFactorization (⇑n : (a : X) → X) a ⊓ rangeFactorization (⇑n : (a : X) → X) b) : X)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
Goal:
X : Type u_1
inst : Frame X
n_1 m : Nucleus X
x y : X
n : Nucleus X
⊢ Eq (α := (↑(range (ι := X) (⇑n : (a : X) → X)) : Type u_1)) (rangeFactorization (⇑n : (a : X) → X) ⊤) ⊤
have a : Eq (α := X) (↑(rangeFactorization (⇑n : (a : X) → X) ⊤) : X) (↑⊤ : X)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
Goal:
X : Type u_1
inst : Frame X
n_1 m : Nucleus X
x y : X
n : Nucleus X
s : Set X
⊢ Eq (α := (↑(range (ι := X) (⇑n : (a : X) → X)) : Type u_1)) (rangeFactorization (⇑n : (a : X) → X) (sSup s))
    (sSup (rangeFactorization (⇑n : (a : X) → X) '' s))
have 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))
Tactic: rw [n.giAux.gc.l_sSup, sSup_image]
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
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))
⊢ Eq (α := (↑(range (ι := X) (⇑n : (a : X) → X)) : Type u_1)) (rangeFactorization (⇑n : (a : X) → X) (sSup s))
    (sSup (rangeFactorization (⇑n : (a : X) → X) '' s))
have 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)
Tactic: rw [n.giAux.gc.l_sSup, sSup_image]
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
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)
⊢ n ≤ m
have rw : LE.le (α := (a : X) → X) (⇑n : (a : X) → X) (Function.comp (β := X) (⇑n : (a : X) → X) (⇑m : (a : X) → X))
Tactic: rw [← coe_le_coe, ← h]
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
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) ((m : (a : X) → X) x : X)
have 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)
Tactic: rw [← mem_range.mp (Set.range_subset_iff.mp h x)]
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
c : Chain α
f : α →o β
b : β
h : ∃ a ∈ c, (f : (a : α) → β) a = b
⊢ b ∈ c.map f
have rcases : ∀ (w : α) (h : w ∈ c) (h' : (f : (a : α) → β) w = b), b ∈ c.map f
Tactic: rcases h with ⟨w, h, h'⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
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
⊢ b ∈ c.map f
have subst : Membership.mem (α := β) (c.map f) ((f : (a : α) → β) w : β)
Tactic: subst b
Cleared hypotheses: b, h'
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
inst : Preorder α
c : Chain α
⊢ c.map OrderHom.id = c
have h : ∀ (x : ℕ), Eq (α := α) ((c.map OrderHom.id : (a : ℕ) → α) x : α) ((c : (a : ℕ) → α) x : α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
inst : Preorder α
a b : α
hab : a ≤ b
⊢ Eq (α := Set α) (Set.range (ι := ℕ) (⇑(pair a b hab) : (a : ℕ) → α)) {a, b}
have h : ∀ (x : α),
  Membership.mem (γ := Set α) (Set.range (ι := ℕ) (⇑(pair a b hab) : (a : ℕ) → α)) x ↔
    Membership.mem (γ := Set α) {a, b} x
Tactic: ext