awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
Goal:
X : Type u_1
inst : SemilatticeInf X
n m : Nucleus X
x y : X
f g : Nucleus X
h : Eq.{u_1 + 1} (α := (a : X) → X) ((fun (x : Nucleus X) ↦ x.toFun) f) ((fun (x : Nucleus X) ↦ x.toFun) g)
⊢ f = g
have obtain : ∀ (toFun : X → X) (map_inf' : ∀ (a b : X), toFun (a ⊓ b) = toFun a ⊓ toFun b)
  (idempotent' :
    ∀ (x : X),
      { toFun := toFun, map_inf' := map_inf' : InfHom X X }.toFun
          ({ toFun := toFun, map_inf' := map_inf' : InfHom X X }.toFun x) ≤
        { toFun := toFun, map_inf' := map_inf' : InfHom X X }.toFun x)
  (le_apply' : ∀ (x : X), x ≤ { toFun := toFun, map_inf' := map_inf' : InfHom X X }.toFun x)
  (h :
    Eq.{u_1 + 1} (α := (a : X) → X)
      ((fun (x : Nucleus X) ↦ x.toFun)
        { toFun := toFun, map_inf' := map_inf', idempotent' := idempotent', le_apply' := le_apply' })
      ((fun (x : Nucleus X) ↦ x.toFun) g)),
  { toFun := toFun, map_inf' := map_inf', idempotent' := idempotent', le_apply' := le_apply' : Nucleus X } = g
Tactic: obtain ⟨⟨_, _⟩, _⟩ := f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
Goal:
X : Type u_1
inst : SemilatticeInf X
n_1 m_1 : Nucleus X
x_1 y : X
m n : Nucleus X
x : X
⊢ LE.le (α := X) (((⇑m : (a : X) → X) ⊓ (⇑n : (a : X) → X)) (((⇑m : (a : X) → X) ⊓ (⇑n : (a : X) → X)) x) : X)
    (((⇑m : (a : X) → X) ⊓ (⇑n : (a : X) → X)) x : X)
have simp : LE.le (α := X)
  ((m : (a : X) → X) x ⊓ (m : (a : X) → X) ((n : (a : X) → X) x : X) ⊓
      ((n : (a : X) → X) ((m : (a : X) → X) x : X) ⊓ (n : (a : X) → X) x) :
    X)
  ((m : (a : X) → X) x ⊓ (n : (a : X) → X) x : X)
Tactic: simp only [Pi.inf_apply, map_inf, idempotent]
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
Goal:
X : Type u_1
inst : CompleteLattice X
s : Set (Nucleus X)
x y : X
⊢ Eq.{u_1 + 1} (α := X) (⨅ f ∈ s, (f : (a : X) → X) (x ⊓ y))
    ((⨅ f ∈ s, (f : (a : X) → X) x) ⊓ ⨅ f ∈ s, (f : (a : X) → X) y)
have simp : ((∀ (i : Nucleus X) (i_1 : i ∈ s),
      LE.le (α := X) (⨅ f ∈ s, (f : (a : X) → X) x ⊓ (f : (a : X) → X) y : X) ((i : (a : X) → X) x : X)) ∧
    ∀ (i : Nucleus X) (i_1 : i ∈ s),
      LE.le (α := X) (⨅ f ∈ s, (f : (a : X) → X) x ⊓ (f : (a : X) → X) y : X) ((i : (a : X) → X) y : X)) ∧
  ∀ (i : Nucleus X) (i_1 : i ∈ s),
    LE.le (α := X) ((⨅ f ∈ s, (f : (a : X) → X) x) ⊓ ⨅ f ∈ s, (f : (a : X) → X) y : X) ((i : (a : X) → X) x : X) ∧
      LE.le (α := X) ((⨅ f ∈ s, (f : (a : X) → X) x) ⊓ ⨅ f ∈ s, (f : (a : X) → X) y : X) ((i : (a : X) → X) y : X)
Tactic: simp only [InfHomClass.map_inf, le_antisymm_iff, le_inf_iff, le_iInf_iff]
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
Goal:
X : Type u_1
inst : CompleteLattice X
s : Set (Nucleus X)
x y : X
⊢ ((∀ (i : Nucleus X) (i_1 : i ∈ s),
        LE.le (α := X) (⨅ f ∈ s, (f : (a : X) → X) x ⊓ (f : (a : X) → X) y : X) ((i : (a : X) → X) x : X)) ∧
      ∀ (i : Nucleus X) (i_1 : i ∈ s),
        LE.le (α := X) (⨅ f ∈ s, (f : (a : X) → X) x ⊓ (f : (a : X) → X) y : X) ((i : (a : X) → X) y : X)) ∧
    ∀ (i : Nucleus X) (i_1 : i ∈ s),
      LE.le (α := X) ((⨅ f ∈ s, (f : (a : X) → X) x) ⊓ ⨅ f ∈ s, (f : (a : X) → X) y : X) ((i : (a : X) → X) x : X) ∧
        LE.le (α := X) ((⨅ f ∈ s, (f : (a : X) → X) x) ⊓ ⨅ f ∈ s, (f : (a : X) → X) y : X) ((i : (a : X) → X) y : X)
have refine_1 : ∀ (i : Nucleus X) (i_1 : i ∈ s),
  LE.le (α := X) (⨅ f ∈ s, (f : (a : X) → X) x ⊓ (f : (a : X) → X) y : X) ((i : (a : X) → X) x : X)
Tactic: refine ⟨⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
Goal:
X : Type u_1
inst : CompleteLattice X
s : Set (Nucleus X)
x y : X
refine_1 :
  ∀ (i : Nucleus X) (i_1 : i ∈ s),
    LE.le (α := X) (⨅ f ∈ s, (f : (a : X) → X) x ⊓ (f : (a : X) → X) y : X) ((i : (a : X) → X) x : X)
⊢ ((∀ (i : Nucleus X) (i_1 : i ∈ s),
        LE.le (α := X) (⨅ f ∈ s, (f : (a : X) → X) x ⊓ (f : (a : X) → X) y : X) ((i : (a : X) → X) x : X)) ∧
      ∀ (i : Nucleus X) (i_1 : i ∈ s),
        LE.le (α := X) (⨅ f ∈ s, (f : (a : X) → X) x ⊓ (f : (a : X) → X) y : X) ((i : (a : X) → X) y : X)) ∧
    ∀ (i : Nucleus X) (i_1 : i ∈ s),
      LE.le (α := X) ((⨅ f ∈ s, (f : (a : X) → X) x) ⊓ ⨅ f ∈ s, (f : (a : X) → X) y : X) ((i : (a : X) → X) x : X) ∧
        LE.le (α := X) ((⨅ f ∈ s, (f : (a : X) → X) x) ⊓ ⨅ f ∈ s, (f : (a : X) → X) y : X) ((i : (a : X) → X) y : X)
have refine_2 : ∀ (i : Nucleus X) (i_1 : i ∈ s),
  LE.le (α := X) (⨅ f ∈ s, (f : (a : X) → X) x ⊓ (f : (a : X) → X) y : X) ((i : (a : X) → X) y : X)
Tactic: refine ⟨⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
Goal:
X : Type u_1
inst : CompleteLattice X
s : Set (Nucleus X)
x y : X
refine_1 :
  ∀ (i : Nucleus X) (i_1 : i ∈ s),
    LE.le (α := X) (⨅ f ∈ s, (f : (a : X) → X) x ⊓ (f : (a : X) → X) y : X) ((i : (a : X) → X) x : X)
refine_2 :
  ∀ (i : Nucleus X) (i_1 : i ∈ s),
    LE.le (α := X) (⨅ f ∈ s, (f : (a : X) → X) x ⊓ (f : (a : X) → X) y : X) ((i : (a : X) → X) y : X)
⊢ ((∀ (i : Nucleus X) (i_1 : i ∈ s),
        LE.le (α := X) (⨅ f ∈ s, (f : (a : X) → X) x ⊓ (f : (a : X) → X) y : X) ((i : (a : X) → X) x : X)) ∧
      ∀ (i : Nucleus X) (i_1 : i ∈ s),
        LE.le (α := X) (⨅ f ∈ s, (f : (a : X) → X) x ⊓ (f : (a : X) → X) y : X) ((i : (a : X) → X) y : X)) ∧
    ∀ (i : Nucleus X) (i_1 : i ∈ s),
      LE.le (α := X) ((⨅ f ∈ s, (f : (a : X) → X) x) ⊓ ⨅ f ∈ s, (f : (a : X) → X) y : X) ((i : (a : X) → X) x : X) ∧
        LE.le (α := X) ((⨅ f ∈ s, (f : (a : X) → X) x) ⊓ ⨅ f ∈ s, (f : (a : X) → X) y : X) ((i : (a : X) → X) y : X)
have refine_3 : ∀ (i : Nucleus X) (i_1 : i ∈ s),
  LE.le (α := X) ((⨅ f ∈ s, (f : (a : X) → X) x) ⊓ ⨅ f ∈ s, (f : (a : X) → X) y : X) ((i : (a : X) → X) x : X) ∧
    LE.le (α := X) ((⨅ f ∈ s, (f : (a : X) → X) x) ⊓ ⨅ f ∈ s, (f : (a : X) → X) y : X) ((i : (a : X) → X) y : X)
Tactic: refine ⟨⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
Goal:
X : Type u_1
inst : CompleteLattice X
ι : Type u_2
f : ι → Nucleus X
x : X
⊢ Eq (α := X) ((iInf f : (a : X) → X) x : X) (⨅ (j : ι), (f j : (a : X) → X) x : X)
have rw : Eq (α := X) ((sInf (range f) : (a : X) → X) x : X) (⨅ (j : ι), (f j : (a : X) → X) x : X)
Tactic: rw [iInf, sInf_apply, iInf_range]
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
Goal:
X : Type u_1
inst : CompleteLattice X
ι : Type u_2
f : ι → Nucleus X
x : X
rw : Eq (α := X) ((sInf (range f) : (a : X) → X) x : X) (⨅ (j : ι), (f j : (a : X) → X) x : X)
⊢ Eq (α := X) ((iInf f : (a : X) → X) x : X) (⨅ (j : ι), (f j : (a : X) → X) x : X)
have rw₁ : Eq.{u_1 + 1} (α := X) (⨅ j ∈ range f, (j : (a : X) → X) x) (⨅ (j : ι), (f j : (a : X) → X) x)
Tactic: rw [iInf, sInf_apply, iInf_range]
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
Goal:
X : Type u_1
inst : CompleteLattice X
ι : Type u_2
f : ι → Nucleus X
x : X
rw : Eq (α := X) ((sInf (range f) : (a : X) → X) x : X) (⨅ (j : ι), (f j : (a : X) → X) x : X)
rw₁ : Eq.{u_1 + 1} (α := X) (⨅ j ∈ range f, (j : (a : X) → X) x) (⨅ (j : ι), (f j : (a : X) → X) x)
⊢ Eq (α := X) ((iInf f : (a : X) → X) x : X) (⨅ (j : ι), (f j : (a : X) → X) x : X)
have rw₂ : Eq.{u_1 + 1} (α := X) (⨅ (i : ι), (f i : (a : X) → X) x) (⨅ (j : ι), (f j : (a : X) → X) x)
Tactic: rw [iInf, sInf_apply, iInf_range]
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
Goal:
X : Type u_1
inst : Frame X
n : Nucleus X
x y : X
⊢ (n : (a : X) → X) (x ⇨ y) ≤ x ⇨ (n : (a : X) → X) y
have rw : LE.le (α := X) ((n : (a : X) → X) (x ⇨ y) ⊓ x : X) ((n : (a : X) → X) y : X)
Tactic: rw [le_himp_iff]
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
Goal:
X : Type u_1
inst : Frame X
n : Nucleus X
x y : X
⊢ LE.le (α := X) ((n : (a : X) → X) (x ⇨ y) ⊓ x : X) ((n : (a : X) → X) (x ⇨ y) ⊓ (n : (a : X) → X) x : X)
have h₂ : x ≤ (n : (a : X) → X) x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
Goal:
X : Type u_1
inst : Frame X
n : Nucleus X
x y : X
⊢ Eq (α := X) ((n : (a : X) → X) (x ⇨ y) ⊓ (n : (a : X) → X) x : X) ((n : (a : X) → X) (y ⊓ x) : X)
have rw : Eq (α := X) ((n : (a : X) → X) ((x ⇨ y) ⊓ x) : X) ((n : (a : X) → X) (y ⊓ x) : X)
Tactic: rw [← map_inf, himp_inf_self]
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
Goal:
X : Type u_1
inst : Frame X
n : Nucleus X
x y : X
rw : Eq (α := X) ((n : (a : X) → X) ((x ⇨ y) ⊓ x) : X) ((n : (a : X) → X) (y ⊓ x) : X)
⊢ Eq (α := X) ((n : (a : X) → X) (x ⇨ y) ⊓ (n : (a : X) → X) x : X) ((n : (a : X) → X) (y ⊓ x) : X)
have rw₁ : Eq (α := X) ((n : (a : X) → X) (y ⊓ x) : X) ((n : (a : X) → X) (y ⊓ x) : X)
Tactic: rw [← map_inf, himp_inf_self]
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
Goal:
X : Type u_1
inst : Frame X
n : Nucleus X
x y : X
⊢ LE.le (α := X) ((n : (a : X) → X) (y ⊓ x) : X) ((n : (a : X) → X) y : X)
have a : y ⊓ x ≤ y
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
Goal:
X : Type u_1
inst : Frame X
n : Nucleus X
x y : X
⊢ LE.le (α := X) ((n : (a : X) → X) (x ⇨ y) ⊓ x : X) ((n : (a : X) → X) y : X)
have n₁ : LE.le (α := X) ((n : (a : X) → X) (x ⇨ y) ⊓ x : X) ((n : (a : X) → X) (x ⇨ y) ⊓ (n : (a : X) → X) x : X)
Tactic: calc
    n (x ⇨ y) ⊓ x
    _ ≤ n (x ⇨ y) ⊓ n x := by gcongr; exact n.le_apply
    _ = n (y ⊓ x) := by rw [← map_inf, himp_inf_self]
    _ ≤ n y := by gcongr; exact inf_le_left
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
Goal:
X : Type u_1
inst : Frame X
n : Nucleus X
x y : X
n₁ : LE.le (α := X) ((n : (a : X) → X) (x ⇨ y) ⊓ x : X) ((n : (a : X) → X) (x ⇨ y) ⊓ (n : (a : X) → X) x : X)
⊢ LE.le (α := X) ((n : (a : X) → X) (x ⇨ y) ⊓ x : X) ((n : (a : X) → X) y : X)
have n₂ : Eq (α := X) ((n : (a : X) → X) (x ⇨ y) ⊓ (n : (a : X) → X) x : X) ((n : (a : X) → X) (y ⊓ x) : X)
Tactic: calc
    n (x ⇨ y) ⊓ x
    _ ≤ n (x ⇨ y) ⊓ n x := by gcongr; exact n.le_apply
    _ = n (y ⊓ x) := by rw [← map_inf, himp_inf_self]
    _ ≤ n y := by gcongr; exact inf_le_left
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
Goal:
X : Type u_1
inst : Frame X
n : Nucleus X
x y : X
n₁ : LE.le (α := X) ((n : (a : X) → X) (x ⇨ y) ⊓ x : X) ((n : (a : X) → X) (x ⇨ y) ⊓ (n : (a : X) → X) x : X)
n₂ : Eq (α := X) ((n : (a : X) → X) (x ⇨ y) ⊓ (n : (a : X) → X) x : X) ((n : (a : X) → X) (y ⊓ x) : X)
⊢ LE.le (α := X) ((n : (a : X) → X) (x ⇨ y) ⊓ x : X) ((n : (a : X) → X) y : X)
have n₃ : LE.le (α := X) ((n : (a : X) → X) (y ⊓ x) : X) ((n : (a : X) → X) y : X)
Tactic: calc
    n (x ⇨ y) ⊓ x
    _ ≤ n (x ⇨ y) ⊓ n x := by gcongr; exact n.le_apply
    _ = n (y ⊓ x) := by rw [← map_inf, himp_inf_self]
    _ ≤ n y := by gcongr; exact inf_le_left
-- Lean 4 proof step from Mathlib.Order.Nucleus (goal)
Goal:
X : Type u_1
inst : Frame X
n : Nucleus X
x y : X
⊢ x ⇨ (n : (a : X) → X) ((n : (a : X) → X) y : X) = x ⇨ (n : (a : X) → X) y
have rw : x ⇨ (n : (a : X) → X) y = x ⇨ (n : (a : X) → X) y
Tactic: rw [n.idempotent]
-- 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
⊢ Eq.{u_1 + 1} (α := X) (⨅ (y_2 : X), ⨅ (_ : y_2 ≥ x ⊓ y), (m : (a : X) → X) y_2 ⇨ (n : (a : X) → X) y_2)
    ((⨅ (y : X), ⨅ (_ : y ≥ x), (m : (a : X) → X) y ⇨ (n : (a : X) → X) y) ⊓
      ⨅ (y_2 : X), ⨅ (_ : y_2 ≥ y), (m : (a : X) → X) y_2 ⇨ (n : (a : X) → X) y_2)
have simp : (∀ (i : X) (i_1 : i ≥ x),
    LE.le (α := X) (⨅ (y_2 : X), ⨅ (_ : y_2 ≥ x ⊓ y), (m : (a : X) → X) y_2 ⇨ (n : (a : X) → X) y_2 : X)
      ((m : (a : X) → X) i ⇨ (n : (a : X) → X) i : X)) ∧
  (∀ (i : X) (i_1 : i ≥ y),
      LE.le (α := X) (⨅ (y_2 : X), ⨅ (_ : y_2 ≥ x ⊓ y), (m : (a : X) → X) y_2 ⇨ (n : (a : X) → X) y_2 : X)
        ((m : (a : X) → X) i ⇨ (n : (a : X) → X) i : X)) ∧
    ∀ (i : X) (i_1 : i ≥ x ⊓ y),
      LE.le (α := X)
        ((⨅ (y : X), ⨅ (_ : y ≥ x), (m : (a : X) → X) y ⇨ (n : (a : X) → X) y) ⊓
            ⨅ (y_2 : X), ⨅ (_ : y_2 ≥ y), (m : (a : X) → X) y_2 ⇨ (n : (a : X) → X) y_2 :
          X)
        ((m : (a : X) → X) i ⇨ (n : (a : X) → X) i : X)
Tactic: simp only [and_assoc, le_antisymm_iff, le_inf_iff, le_iInf_iff]
-- 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
⊢ (∀ (i : X) (i_1 : i ≥ x),
      LE.le (α := X) (⨅ (y_2 : X), ⨅ (_ : y_2 ≥ x ⊓ y), (m : (a : X) → X) y_2 ⇨ (n : (a : X) → X) y_2 : X)
        ((m : (a : X) → X) i ⇨ (n : (a : X) → X) i : X)) ∧
    (∀ (i : X) (i_1 : i ≥ y),
        LE.le (α := X) (⨅ (y_2 : X), ⨅ (_ : y_2 ≥ x ⊓ y), (m : (a : X) → X) y_2 ⇨ (n : (a : X) → X) y_2 : X)
          ((m : (a : X) → X) i ⇨ (n : (a : X) → X) i : X)) ∧
      ∀ (i : X) (i_1 : i ≥ x ⊓ y),
        LE.le (α := X)
          ((⨅ (y : X), ⨅ (_ : y ≥ x), (m : (a : X) → X) y ⇨ (n : (a : X) → X) y) ⊓
              ⨅ (y_2 : X), ⨅ (_ : y_2 ≥ y), (m : (a : X) → X) y_2 ⇨ (n : (a : X) → X) y_2 :
            X)
          ((m : (a : X) → X) i ⇨ (n : (a : X) → X) i : X)
have refine : ∀ (i : X) (i_1 : i ≥ x ⊓ y),
  LE.le (α := X)
    ((⨅ (y : X), ⨅ (_ : y ≥ x), (m : (a : X) → X) y ⇨ (n : (a : X) → X) y) ⊓
        ⨅ (y_2 : X), ⨅ (_ : y_2 ≥ y), (m : (a : X) → X) y_2 ⇨ (n : (a : X) → X) y_2 :
      X)
    ((m : (a : X) → X) i ⇨ (n : (a : X) → X) i : X)
Tactic: refine ⟨fun z hxz ↦ iInf₂_le _ <| inf_le_of_left_le hxz,
        fun z hyz ↦ iInf₂_le _ <| inf_le_of_right_le hyz, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Nucleus (hypothesis)
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
⊢ ∀ (i : X) (i_1 : i ≥ x ⊓ y),
    LE.le (α := X)
      ((⨅ (y : X), ⨅ (_ : y ≥ x), (m : (a : X) → X) y ⇨ (n : (a : X) → X) y) ⊓
          ⨅ (y_2 : X), ⨅ (_ : y_2 ≥ y), (m : (a : X) → X) y_2 ⇨ (n : (a : X) → X) y_2 :
        X)
      ((m : (a : X) → X) i ⇨ (n : (a : X) → X) i : X)
have this : Nonempty X
Tactic: have : Nonempty X := ⟨x⟩
-- 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
this : Nonempty X
⊢ ∀ (i : X) (i_1 : i ≥ x ⊓ y),
    LE.le (α := X)
      ((⨅ (y : X), ⨅ (_ : y ≥ x), (m : (a : X) → X) y ⇨ (n : (a : X) → X) y) ⊓
          ⨅ (y_2 : X), ⨅ (_ : y_2 ≥ y), (m : (a : X) → X) y_2 ⇨ (n : (a : X) → X) y_2 :
        X)
      ((m : (a : X) → X) i ⇨ (n : (a : X) → X) i : X)
have simp : ∀ (i : X) (i_1 : i ≥ x ⊓ y) (b : X),
  (∀ (x_2 : X) (i : x_2 ≥ x), b ⊓ (m : (a : X) → X) x_2 ≤ (n : (a : X) → X) x_2) →
    (∀ (i : X) (i_2 : i ≥ y), b ⊓ (m : (a : X) → X) i ≤ (n : (a : X) → X) i) →
      b ≤ (m : (a : X) → X) i → b ≤ (n : (a : X) → X) i
Tactic: simp only [iInf_inf, le_iInf_iff, le_himp_iff, iInf_le_iff, le_inf_iff, forall_and,
        forall_const, and_imp]
-- 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
this : Nonempty X
k : X
hxyk : k ≥ x ⊓ y
l : X
hlx : ∀ (x_2 : X) (i : x_2 ≥ x), l ⊓ (m : (a : X) → X) x_2 ≤ (n : (a : X) → X) x_2
hly : ∀ (i : X) (i_1 : i ≥ y), l ⊓ (m : (a : X) → X) i ≤ (n : (a : X) → X) i
hlk : l ≤ (m : (a : X) → X) k
⊢ l = l ⊓ (m : (a : X) → X) (x ⊔ k) ⊓ (l ⊓ (m : (a : X) → X) (y ⊔ k))
have rw : l = l ⊓ ((m : (a : X) → X) (x ⊔ k) ⊓ (m : (a : X) → X) (y ⊔ k))
Tactic: rw [← inf_inf_distrib_left, ← map_inf, ← sup_inf_right, sup_eq_right.2 hxyk,
            inf_eq_left.2 hlk]
-- 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
this : Nonempty X
k : X
hxyk : k ≥ x ⊓ y
l : X
hlx : ∀ (x_2 : X) (i : x_2 ≥ x), l ⊓ (m : (a : X) → X) x_2 ≤ (n : (a : X) → X) x_2
hly : ∀ (i : X) (i_1 : i ≥ y), l ⊓ (m : (a : X) → X) i ≤ (n : (a : X) → X) i
hlk : l ≤ (m : (a : X) → X) k
rw : l = l ⊓ ((m : (a : X) → X) (x ⊔ k) ⊓ (m : (a : X) → X) (y ⊔ k))
⊢ l = l ⊓ (m : (a : X) → X) (x ⊔ k) ⊓ (l ⊓ (m : (a : X) → X) (y ⊔ k))
have rw₁ : l = l ⊓ (m : (a : X) → X) ((x ⊔ k) ⊓ (y ⊔ k))
Tactic: rw [← inf_inf_distrib_left, ← map_inf, ← sup_inf_right, sup_eq_right.2 hxyk,
            inf_eq_left.2 hlk]
-- 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
this : Nonempty X
k : X
hxyk : k ≥ x ⊓ y
l : X
hlx : ∀ (x_2 : X) (i : x_2 ≥ x), l ⊓ (m : (a : X) → X) x_2 ≤ (n : (a : X) → X) x_2
hly : ∀ (i : X) (i_1 : i ≥ y), l ⊓ (m : (a : X) → X) i ≤ (n : (a : X) → X) i
hlk : l ≤ (m : (a : X) → X) k
rw : l = l ⊓ ((m : (a : X) → X) (x ⊔ k) ⊓ (m : (a : X) → X) (y ⊔ k))
rw₁ : l = l ⊓ (m : (a : X) → X) ((x ⊔ k) ⊓ (y ⊔ k))
⊢ l = l ⊓ (m : (a : X) → X) (x ⊔ k) ⊓ (l ⊓ (m : (a : X) → X) (y ⊔ k))
have rw₂ : l = l ⊓ (m : (a : X) → X) (x ⊓ y ⊔ k)
Tactic: rw [← inf_inf_distrib_left, ← map_inf, ← sup_inf_right, sup_eq_right.2 hxyk,
            inf_eq_left.2 hlk]
-- 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
this : Nonempty X
k : X
hxyk : k ≥ x ⊓ y
l : X
hlx : ∀ (x_2 : X) (i : x_2 ≥ x), l ⊓ (m : (a : X) → X) x_2 ≤ (n : (a : X) → X) x_2
hly : ∀ (i : X) (i_1 : i ≥ y), l ⊓ (m : (a : X) → X) i ≤ (n : (a : X) → X) i
hlk : l ≤ (m : (a : X) → X) k
rw : l = l ⊓ ((m : (a : X) → X) (x ⊔ k) ⊓ (m : (a : X) → X) (y ⊔ k))
rw₁ : l = l ⊓ (m : (a : X) → X) ((x ⊔ k) ⊓ (y ⊔ k))
rw₂ : l = l ⊓ (m : (a : X) → X) (x ⊓ y ⊔ k)
⊢ l = l ⊓ (m : (a : X) → X) (x ⊔ k) ⊓ (l ⊓ (m : (a : X) → X) (y ⊔ k))
have rw₃ : l = l ⊓ (m : (a : X) → X) k
Tactic: rw [← inf_inf_distrib_left, ← map_inf, ← sup_inf_right, sup_eq_right.2 hxyk,
            inf_eq_left.2 hlk]
-- 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
this : Nonempty X
k : X
hxyk : k ≥ x ⊓ y
l : X
hlx : ∀ (x_2 : X) (i : x_2 ≥ x), l ⊓ (m : (a : X) → X) x_2 ≤ (n : (a : X) → X) x_2
hly : ∀ (i : X) (i_1 : i ≥ y), l ⊓ (m : (a : X) → X) i ≤ (n : (a : X) → X) i
hlk : l ≤ (m : (a : X) → X) k
rw : l = l ⊓ ((m : (a : X) → X) (x ⊔ k) ⊓ (m : (a : X) → X) (y ⊔ k))
rw₁ : l = l ⊓ (m : (a : X) → X) ((x ⊔ k) ⊓ (y ⊔ k))
rw₂ : l = l ⊓ (m : (a : X) → X) (x ⊓ y ⊔ k)
rw₃ : l = l ⊓ (m : (a : X) → X) k
⊢ l = l ⊓ (m : (a : X) → X) (x ⊔ k) ⊓ (l ⊓ (m : (a : X) → X) (y ⊔ k))
have rw₄ : l = l
Tactic: rw [← inf_inf_distrib_left, ← map_inf, ← sup_inf_right, sup_eq_right.2 hxyk,
            inf_eq_left.2 hlk]
-- 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
this : Nonempty X
k : X
hxyk : k ≥ x ⊓ y
l : X
hlx : ∀ (x_2 : X) (i : x_2 ≥ x), l ⊓ (m : (a : X) → X) x_2 ≤ (n : (a : X) → X) x_2
hly : ∀ (i : X) (i_1 : i ≥ y), l ⊓ (m : (a : X) → X) i ≤ (n : (a : X) → X) i
hlk : l ≤ (m : (a : X) → X) k
⊢ l ⊓ (m : (a : X) → X) (x ⊔ k) ⊓ (l ⊓ (m : (a : X) → X) (y ⊔ k)) ≤
    (n : (a : X) → X) (x ⊔ k) ⊓ (n : (a : X) → X) (y ⊔ k)
have h₁ : l ⊓ (m : (a : X) → X) (x ⊔ k) ≤ (n : (a : X) → X) (x ⊔ k)
Tactic: gcongr
-- 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
this : Nonempty X
k : X
hxyk : k ≥ x ⊓ y
l : X
hlx : ∀ (x_2 : X) (i : x_2 ≥ x), l ⊓ (m : (a : X) → X) x_2 ≤ (n : (a : X) → X) x_2
hly : ∀ (i : X) (i_1 : i ≥ y), l ⊓ (m : (a : X) → X) i ≤ (n : (a : X) → X) i
hlk : l ≤ (m : (a : X) → X) k
h₁ : l ⊓ (m : (a : X) → X) (x ⊔ k) ≤ (n : (a : X) → X) (x ⊔ k)
⊢ l ⊓ (m : (a : X) → X) (x ⊔ k) ⊓ (l ⊓ (m : (a : X) → X) (y ⊔ k)) ≤
    (n : (a : X) → X) (x ⊔ k) ⊓ (n : (a : X) → X) (y ⊔ k)
have h₂ : l ⊓ (m : (a : X) → X) (y ⊔ k) ≤ (n : (a : X) → X) (y ⊔ k)
Tactic: gcongr
-- 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
this : Nonempty X
k : X
hxyk : k ≥ x ⊓ y
l : X
hlx : ∀ (x_2 : X) (i : x_2 ≥ x), l ⊓ (m : (a : X) → X) x_2 ≤ (n : (a : X) → X) x_2
hly : ∀ (i : X) (i_1 : i ≥ y), l ⊓ (m : (a : X) → X) i ≤ (n : (a : X) → X) i
hlk : l ≤ (m : (a : X) → X) k
⊢ Eq (α := X) ((n : (a : X) → X) (x ⊔ k) ⊓ (n : (a : X) → X) (y ⊔ k) : X) ((n : (a : X) → X) k : X)
have rw : Eq (α := X) ((n : (a : X) → X) ((x ⊔ k) ⊓ (y ⊔ k)) : X) ((n : (a : X) → X) k : X)
Tactic: rw [← map_inf, ← sup_inf_right, sup_eq_right.2 hxyk]
-- 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
this : Nonempty X
k : X
hxyk : k ≥ x ⊓ y
l : X
hlx : ∀ (x_2 : X) (i : x_2 ≥ x), l ⊓ (m : (a : X) → X) x_2 ≤ (n : (a : X) → X) x_2
hly : ∀ (i : X) (i_1 : i ≥ y), l ⊓ (m : (a : X) → X) i ≤ (n : (a : X) → X) i
hlk : l ≤ (m : (a : X) → X) k
rw : Eq (α := X) ((n : (a : X) → X) ((x ⊔ k) ⊓ (y ⊔ k)) : X) ((n : (a : X) → X) k : X)
⊢ Eq (α := X) ((n : (a : X) → X) (x ⊔ k) ⊓ (n : (a : X) → X) (y ⊔ k) : X) ((n : (a : X) → X) k : X)
have rw₁ : Eq (α := X) ((n : (a : X) → X) (x ⊓ y ⊔ k) : X) ((n : (a : X) → X) k : X)
Tactic: rw [← map_inf, ← sup_inf_right, sup_eq_right.2 hxyk]
-- 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
this : Nonempty X
k : X
hxyk : k ≥ x ⊓ y
l : X
hlx : ∀ (x_2 : X) (i : x_2 ≥ x), l ⊓ (m : (a : X) → X) x_2 ≤ (n : (a : X) → X) x_2
hly : ∀ (i : X) (i_1 : i ≥ y), l ⊓ (m : (a : X) → X) i ≤ (n : (a : X) → X) i
hlk : l ≤ (m : (a : X) → X) k
rw : Eq (α := X) ((n : (a : X) → X) ((x ⊔ k) ⊓ (y ⊔ k)) : X) ((n : (a : X) → X) k : X)
rw₁ : Eq (α := X) ((n : (a : X) → X) (x ⊓ y ⊔ k) : X) ((n : (a : X) → X) k : X)
⊢ Eq (α := X) ((n : (a : X) → X) (x ⊔ k) ⊓ (n : (a : X) → X) (y ⊔ k) : X) ((n : (a : X) → X) k : X)
have rw₂ : Eq (α := X) ((n : (a : X) → X) k : X) ((n : (a : X) → X) k : X)
Tactic: rw [← map_inf, ← sup_inf_right, sup_eq_right.2 hxyk]
-- 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
this : Nonempty X
k : X
hxyk : k ≥ x ⊓ y
l : X
hlx : ∀ (x_2 : X) (i : x_2 ≥ x), l ⊓ (m : (a : X) → X) x_2 ≤ (n : (a : X) → X) x_2
hly : ∀ (i : X) (i_1 : i ≥ y), l ⊓ (m : (a : X) → X) i ≤ (n : (a : X) → X) i
hlk : l ≤ (m : (a : X) → X) k
⊢ l ≤ (n : (a : X) → X) k
have l₁ : l = l ⊓ (m : (a : X) → X) (x ⊔ k) ⊓ (l ⊓ (m : (a : X) → X) (y ⊔ k))
Tactic: calc
        l = (l ⊓ m (x ⊔ k)) ⊓ (l ⊓ m (y ⊔ k)) := by
          rw [← inf_inf_distrib_left, ← map_inf, ← sup_inf_right, sup_eq_right.2 hxyk,
            inf_eq_left.2 hlk]
        _ ≤ n (x ⊔ k) ⊓ n (y ⊔ k) := by
          gcongr; exacts [hlx (x ⊔ k) le_sup_left, hly (y ⊔ k) le_sup_left]
        _ = n k := by rw [← map_inf, ← sup_inf_right, sup_eq_right.2 hxyk]
-- 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
this : Nonempty X
k : X
hxyk : k ≥ x ⊓ y
l : X
hlx : ∀ (x_2 : X) (i : x_2 ≥ x), l ⊓ (m : (a : X) → X) x_2 ≤ (n : (a : X) → X) x_2
hly : ∀ (i : X) (i_1 : i ≥ y), l ⊓ (m : (a : X) → X) i ≤ (n : (a : X) → X) i
hlk : l ≤ (m : (a : X) → X) k
l₁ : l = l ⊓ (m : (a : X) → X) (x ⊔ k) ⊓ (l ⊓ (m : (a : X) → X) (y ⊔ k))
⊢ l ≤ (n : (a : X) → X) k
have l₂ : l ⊓ (m : (a : X) → X) (x ⊔ k) ⊓ (l ⊓ (m : (a : X) → X) (y ⊔ k)) ≤ (n : (a : X) → X) (x ⊔ k) ⊓ (n : (a : X) → X) (y ⊔ k)
Tactic: calc
        l = (l ⊓ m (x ⊔ k)) ⊓ (l ⊓ m (y ⊔ k)) := by
          rw [← inf_inf_distrib_left, ← map_inf, ← sup_inf_right, sup_eq_right.2 hxyk,
            inf_eq_left.2 hlk]
        _ ≤ n (x ⊔ k) ⊓ n (y ⊔ k) := by
          gcongr; exacts [hlx (x ⊔ k) le_sup_left, hly (y ⊔ k) le_sup_left]
        _ = n k := by rw [← map_inf, ← sup_inf_right, sup_eq_right.2 hxyk]
-- 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
this : Nonempty X
k : X
hxyk : k ≥ x ⊓ y
l : X
hlx : ∀ (x_2 : X) (i : x_2 ≥ x), l ⊓ (m : (a : X) → X) x_2 ≤ (n : (a : X) → X) x_2
hly : ∀ (i : X) (i_1 : i ≥ y), l ⊓ (m : (a : X) → X) i ≤ (n : (a : X) → X) i
hlk : l ≤ (m : (a : X) → X) k
l₁ : l = l ⊓ (m : (a : X) → X) (x ⊔ k) ⊓ (l ⊓ (m : (a : X) → X) (y ⊔ k))
l₂ :
  l ⊓ (m : (a : X) → X) (x ⊔ k) ⊓ (l ⊓ (m : (a : X) → X) (y ⊔ k)) ≤
    (n : (a : X) → X) (x ⊔ k) ⊓ (n : (a : X) → X) (y ⊔ k)
⊢ l ≤ (n : (a : X) → X) k
have l₃ : Eq (α := X) ((n : (a : X) → X) (x ⊔ k) ⊓ (n : (a : X) → X) (y ⊔ k) : X) ((n : (a : X) → X) k : X)
Tactic: calc
        l = (l ⊓ m (x ⊔ k)) ⊓ (l ⊓ m (y ⊔ k)) := by
          rw [← inf_inf_distrib_left, ← map_inf, ← sup_inf_right, sup_eq_right.2 hxyk,
            inf_eq_left.2 hlk]
        _ ≤ n (x ⊔ k) ⊓ n (y ⊔ k) := by
          gcongr; exacts [hlx (x ⊔ k) le_sup_left, hly (y ⊔ k) le_sup_left]
        _ = n k := by rw [← map_inf, ← sup_inf_right, sup_eq_right.2 hxyk]