awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : SemilatticeInf X
n m : Nucleus X
x y : X
⊢ ∀ (x : X), x ≤ x

Tactic:
simp
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : SemilatticeInf X
⊢ Eq.{u_1 + 1} (α := (a : X) → X) (⇑⊥ : (a : X) → X) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : SemilatticeInf X
x : X
⊢ (⊥ : (a : X) → X) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : SemilatticeInf X
n m : Nucleus X
x y : X
inst_1 : OrderTop X
⊢ ∀ (a b : X), Eq.{u_1 + 1} (α := X) (⊤ (a ⊓ b)) (⊤ a ⊓ ⊤ b)

Tactic:
simp
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : SemilatticeInf X
n m : Nucleus X
x y : X
inst_1 : OrderTop X
⊢ ∀ (x : X), LE.le.{u_1} (α := X) (⊤ (⊤ x)) (⊤ x)

Tactic:
simp
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : SemilatticeInf X
n m : Nucleus X
x y : X
inst_1 : OrderTop X
⊢ ∀ (x : X), x ≤ ⊤ x

Tactic:
simp
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : SemilatticeInf X
inst_1 : OrderTop X
⊢ Eq.{u_1 + 1} (α := (a : X) → X) (⇑⊤ : (a : X) → X) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : SemilatticeInf X
inst_1 : OrderTop X
x : X
⊢ Eq (α := X) ((⊤ : (a : X) → X) x : X) (⊤ : X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : SemilatticeInf X
n m : Nucleus X
x y : X
inst_1 : OrderTop X
x_1 : Nucleus X
x_2 : X
⊢ LE.le (α := (fun (a : X) ↦ X) x_2) ((x_1 : (a : X) → X) x_2 : X) ((⊤ : (a : X) → X) x_2 : X)

Tactic:
simp
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : CompleteLattice X
s : Set (Nucleus X)
x y : X
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)
⊢ 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)

Tactic:
simp only [InfHomClass.map_inf, le_antisymm_iff, le_inf_iff, le_iInf_iff]

Premises used: le_iInf_iff, le_inf_iff, InfHomClass.map_inf, le_antisymm_iff
-- Module: Mathlib.Order.Nucleus
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)

Tactic:
⟨⟨?_, ?_⟩, ?_⟩

Premises used: And.intro
-- Module: Mathlib.Order.Nucleus
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)
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)
⊢ ((∀ (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:
refine ⟨⟨?_, ?_⟩, ?_⟩
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : CompleteLattice X
s : Set (Nucleus X)
x y : X
f : Nucleus X
hf : f ∈ s
⊢ LE.le (α := X) (⨅ f ∈ s, (f : (a : X) → X) x ⊓ (f : (a : X) → X) y : X) ((f : (a : X) → X) x : X)

Tactic:
iInf₂_le_of_le f hf inf_le_left

Premises used: iInf₂_le_of_le, inf_le_left
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : CompleteLattice X
s : Set (Nucleus X)
x y : X
f : Nucleus X
hf : f ∈ s
⊢ LE.le (α := X) (⨅ f ∈ s, (f : (a : X) → X) x ⊓ (f : (a : X) → X) y : X) ((f : (a : X) → X) x : X)

Tactic:
exact iInf₂_le_of_le f hf inf_le_left

Premises used: iInf₂_le_of_le
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : CompleteLattice X
s : Set (Nucleus X)
x y : X
f : Nucleus X
hf : f ∈ s
⊢ LE.le (α := X) (⨅ f ∈ s, (f : (a : X) → X) x ⊓ (f : (a : X) → X) y : X) ((f : (a : X) → X) y : X)

Tactic:
iInf₂_le_of_le f hf inf_le_right

Premises used: inf_le_right, iInf₂_le_of_le
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : CompleteLattice X
s : Set (Nucleus X)
x y : X
f : Nucleus X
hf : f ∈ s
⊢ LE.le (α := X) (⨅ f ∈ s, (f : (a : X) → X) x ⊓ (f : (a : X) → X) y : X) ((f : (a : X) → X) y : X)

Tactic:
exact iInf₂_le_of_le f hf inf_le_right

Premises used: iInf₂_le_of_le
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : CompleteLattice X
s : Set (Nucleus X)
x y : X
f : Nucleus X
hf : f ∈ s
⊢ LE.le (α := X) ((⨅ f ∈ s, (f : (a : X) → X) x) ⊓ ⨅ f ∈ s, (f : (a : X) → X) y : X) ((f : (a : X) → X) x : X) ∧
    LE.le (α := X) ((⨅ f ∈ s, (f : (a : X) → X) x) ⊓ ⨅ f ∈ s, (f : (a : X) → X) y : X) ((f : (a : X) → X) y : X)

Tactic:
⟨inf_le_of_left_le <| iInf₂_le f hf, inf_le_of_right_le <| iInf₂_le f hf⟩

Premises used: iInf₂_le, inf_le_of_right_le, inf_le_of_left_le, And.intro
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : CompleteLattice X
s : Set (Nucleus X)
x y : X
f : Nucleus X
hf : f ∈ s
⊢ LE.le (α := X) ((⨅ f ∈ s, (f : (a : X) → X) x) ⊓ ⨅ f ∈ s, (f : (a : X) → X) y : X) ((f : (a : X) → X) x : X) ∧
    LE.le (α := X) ((⨅ f ∈ s, (f : (a : X) → X) x) ⊓ ⨅ f ∈ s, (f : (a : X) → X) y : X) ((f : (a : X) → X) y : X)

Tactic:
exact ⟨inf_le_of_left_le <| iInf₂_le f hf, inf_le_of_right_le <| iInf₂_le f hf⟩
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : CompleteLattice X
s : Set (Nucleus X)
x : X
⊢ x ≤ ⨅ f ∈ s, (f : (a : X) → X) x

Tactic:
simp [le_apply]

Premises used: Nucleus.le_apply
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : CompleteLattice X
s : Set (Nucleus X)
x : X
⊢ Eq (α := X) ((sInf s : (a : X) → X) x : X) (⨅ j ∈ s, (j : (a : X) → X) x : X)

Tactic:
rfl

Premises used: iInf, rfl
-- Module: Mathlib.Order.Nucleus
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)
rw₂ rw₃ : Eq.{u_1 + 1} (α := X) (⨅ (i : ι), (f i : (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)

Tactic:
rw [iInf, sInf_apply, iInf_range]

Premises used: iInf, iInf_range, Nucleus.sInf_apply
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : CompleteLattice X
x : Set (Nucleus X)
⊢ sInf x ∈ lowerBounds x

Tactic:
simp +contextual [mem_lowerBounds, ← coe_le_coe, Pi.le_def, iInf_le_iff]

Premises used: mem_lowerBounds, iInf_le_iff, Nucleus.coe_le_coe, Pi.le_def
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : CompleteLattice X
x : Set (Nucleus X)
⊢ sInf x ∈ upperBounds (lowerBounds x)

Tactic:
simp +contextual [mem_lowerBounds, mem_upperBounds, ← coe_le_coe, Pi.le_def]

Premises used: mem_lowerBounds, Nucleus.coe_le_coe, Pi.le_def, mem_upperBounds
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : Frame X
n : Nucleus X
x y : X
rw : LE.le (α := X) ((n : (a : X) → X) (x ⇨ y) ⊓ x : X) ((n : (a : X) → X) y : X)
⊢ (n : (a : X) → X) (x ⇨ y) ≤ x ⇨ (n : (a : X) → X) y

Tactic:
rw [le_himp_iff]

Premises used: le_himp_iff
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : Frame X
n : Nucleus X
x y : X
h₂ : x ≤ (n : (a : X) → X) x
⊢ LE.le (α := X) ((n : (a : X) → X) (x ⇨ y) ⊓ x : X) ((n : (a : X) → X) (x ⇨ y) ⊓ (n : (a : X) → X) x : X)

Tactic:
gcongr
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : Frame X
n : Nucleus X
x y : X
⊢ x ≤ (n : (a : X) → X) x

Tactic:
n.le_apply

Premises used: Nucleus.le_apply
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : Frame X
n : Nucleus X
x y : X
⊢ x ≤ (n : (a : X) → X) x

Tactic:
exact n.le_apply

Premises used: Nucleus.le_apply
-- Module: Mathlib.Order.Nucleus
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)
rw₁ rw₂ : Eq (α := X) ((n : (a : 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)

Tactic:
rw [← map_inf, himp_inf_self]

Premises used: himp_inf_self, Nucleus.map_inf
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : Frame X
n : Nucleus X
x y : X
a : y ⊓ x ≤ y
⊢ LE.le (α := X) ((n : (a : X) → X) (y ⊓ x) : X) ((n : (a : X) → X) y : X)

Tactic:
gcongr
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : Frame X
n : Nucleus X
x y : X
⊢ y ⊓ x ≤ y

Tactic:
inf_le_left

Premises used: inf_le_left
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : Frame X
n : Nucleus X
x y : X
⊢ y ⊓ x ≤ y

Tactic:
exact inf_le_left

Premises used: inf_le_left
-- Module: Mathlib.Order.Nucleus
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)
n₃ : LE.le (α := X) ((n : (a : X) → X) (y ⊓ x) : X) ((n : (a : X) → X) y : X)
⊢ LE.le (α := X) ((n : (a : X) → 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

Premises used: DFunLike.coe, Min.min, HImp.himp
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : Frame X
n : Nucleus X
x y : X
rw rw₁ : x ⇨ (n : (a : X) → X) y = x ⇨ (n : (a : X) → X) y
⊢ x ⇨ (n : (a : X) → X) ((n : (a : X) → X) y : X) = x ⇨ (n : (a : X) → X) y

Tactic:
rw [n.idempotent]

Premises used: Nucleus.idempotent
-- Module: Mathlib.Order.Nucleus
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
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)
⊢ 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)

Tactic:
simp only [and_assoc, le_antisymm_iff, le_inf_iff, le_iInf_iff]

Premises used: le_iInf_iff, le_inf_iff, le_antisymm_iff, and_assoc
-- Module: Mathlib.Order.Nucleus
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)

Tactic:
⟨fun z hxz ↦ iInf₂_le _ <| inf_le_of_left_le hxz,
        fun z hyz ↦ iInf₂_le _ <| inf_le_of_right_le hyz, ?_⟩

Premises used: iInf₂_le, inf_le_of_right_le, inf_le_of_left_le, And.intro
-- Module: Mathlib.Order.Nucleus
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
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)
⊢ (∀ (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:
refine ⟨fun z hxz ↦ iInf₂_le _ <| inf_le_of_left_le hxz,
        fun z hyz ↦ iInf₂_le _ <| inf_le_of_right_le hyz, ?_⟩
-- Module: Mathlib.Order.Nucleus
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
⊢ Nonempty X

Tactic:
have : Nonempty X := ⟨x⟩
-- Module: Mathlib.Order.Nucleus
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
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
⊢ ∀ (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 [iInf_inf, le_iInf_iff, le_himp_iff, iInf_le_iff, le_inf_iff, forall_and,
        forall_const, and_imp]

Premises used: iInf_inf, and_imp, le_iInf_iff, iInf_le_iff, le_inf_iff, le_himp_iff, forall_const, forall_and
-- Module: Mathlib.Order.Nucleus
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
rw₄ rw₅ : l = l
⊢ l = l ⊓ (m : (a : X) → X) (x ⊔ k) ⊓ (l ⊓ (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]

Premises used: Iff.mpr, inf_inf_distrib_left, sup_inf_right, sup_eq_right, inf_eq_left, Nucleus.map_inf
-- Module: Mathlib.Order.Nucleus
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)
h₂ : l ⊓ (m : (a : X) → X) (y ⊔ k) ≤ (n : (a : X) → X) (y ⊔ 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)

Tactic:
gcongr
-- Module: Mathlib.Order.Nucleus
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) ≤ (n : (a : X) → X) (x ⊔ k)

Tactic:
hlx (x ⊔ k) le_sup_left

Premises used: le_sup_left, Max.max
-- Module: Mathlib.Order.Nucleus
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) (y ⊔ k) ≤ (n : (a : X) → X) (y ⊔ k)

Tactic:
hly (y ⊔ k) le_sup_left

Premises used: le_sup_left, Max.max
-- Module: Mathlib.Order.Nucleus
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) ≤ (n : (a : X) → X) (x ⊔ k)

Tactic:
exacts [hlx (x ⊔ k) le_sup_left, hly (y ⊔ k) le_sup_left]

Premises used: le_sup_left, Max.max
-- Module: Mathlib.Order.Nucleus
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)
rw₂ rw₃ : Eq (α := X) ((n : (a : X) → X) 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)

Tactic:
rw [← map_inf, ← sup_inf_right, sup_eq_right.2 hxyk]

Premises used: Iff.mpr, sup_inf_right, sup_eq_right, Nucleus.map_inf
-- Module: Mathlib.Order.Nucleus
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₃ : Eq (α := X) ((n : (a : X) → X) (x ⊔ k) ⊓ (n : (a : X) → X) (y ⊔ k) : X) ((n : (a : X) → X) k : X)
⊢ l ≤ (n : (a : X) → X) 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]

Premises used: Max.max, DFunLike.coe, Min.min
-- Module: Mathlib.Order.Nucleus
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)
rw₃ 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)
⊢ 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)

Tactic:
rw [map_himp_apply, himp_himp, ← map_inf, inf_of_le_right (le_trans n.le_apply le_himp)]

Premises used: Nucleus.map_himp_apply, inf_of_le_right, himp_himp, Nucleus.map_inf, le_himp, le_trans, Nucleus.le_apply
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : Frame X
n_1 m_1 : Nucleus X
x y : X
m n : Nucleus X
⊢ ∀ (x : X), x ≤ ⨅ (y : X), ⨅ (_ : y ≥ x), (m : (a : X) → X) y ⇨ (n : (a : X) → X) y

Tactic:
simpa using fun _ _ h ↦ inf_le_of_left_le <| h.trans n.le_apply

Premises used: inf_le_of_left_le
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : Frame X
m n : Nucleus X
x : X
⊢ Eq (α := X) ((m ⇨ n : (a : X) → X) x : X) (⨅ (y : X), ⨅ (_ : y ≥ x), (m : (a : X) → X) y ⇨ (n : (a : X) → X) y : X)

Tactic:
rfl

Premises used: iInf, rfl
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : Frame X
n_1 m : Nucleus X
x y : X
x_1 n x_2 : Nucleus X
h : ∀ (i : X), LE.le (α := X) ((x_1 : (a : X) → X) i ⊓ (n : (a : X) → X) i : X) ((x_2 : (a : X) → X) i : X)
i j : X
h_1 : i ≤ j
⊢ LE.le (α := X) ((x_1 : (a : X) → X) i ⊓ (n : (a : X) → X) j : X) ((x_1 : (a : X) → X) j ⊓ (n : (a : X) → X) j : X)

Tactic:
gcongr
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : Frame X
n_1 m : Nucleus X
x y : X
x_1 n x_2 : Nucleus X
⊢ x_1 ≤ n ⇨ x_2 ↔ x_1 ⊓ n ≤ x_2

Tactic:
simpa [← coe_le_coe, Pi.le_def]
      using ⟨fun h i ↦ h i i le_rfl, fun h i j _ ↦ (h j).trans' <| by gcongr⟩

Premises used: Nucleus.coe_le_coe, Pi.le_def
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : Frame X
n : Nucleus X
x : X
⊢ Eq (α := X) ((n : (a : X) → X) ((n : (a : X) → X) x : X) : X) ((n : (a : X) → X) x : X)

Tactic:
idempotent _

Premises used: Nucleus.idempotent
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : Frame X
n : Nucleus X
x : X
⊢ Eq (α := X) ((n : (a : X) → X) ((n : (a : X) → X) x : X) : X) ((n : (a : X) → X) x : X)

Tactic:
exact idempotent _

Premises used: Nucleus.idempotent
-- 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
a :
  (↑(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)
⊢ Subtype.mk (p := fun (x : X) ↦ Membership.mem (γ := Set X) (range (ι := X) (⇑n : (a : X) → X)) x) x ⋯ =
    rangeFactorization (⇑n : (a : X) → X) x

Tactic:
ext