awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S T : Sublocale X
s : Set X
f : ι → X
a b : X
s1 s2 : Sublocale X
h : Eq.{u_1 + 1} (α := Set X) ((fun (x : Sublocale X) ↦ x.carrier) s1) ((fun (x : Sublocale X) ↦ x.carrier) s2)
mk :
  ∀ (carrier : Set X) (sInf_mem' : ∀ s ⊆ carrier, sInf s ∈ carrier)
    (himp_mem' : ∀ (a b : X), b ∈ carrier → a ⇨ b ∈ carrier)
    (h :
      Eq.{u_1 + 1} (α := Set X)
        ((fun (x : Sublocale X) ↦ x.carrier) { carrier := carrier, sInf_mem' := sInf_mem', himp_mem' := himp_mem' })
        ((fun (x : Sublocale X) ↦ x.carrier) s2)),
    { carrier := carrier, sInf_mem' := sInf_mem', himp_mem' := himp_mem' : Sublocale X } = s2
⊢ s1 = s2

Tactic:
cases s1
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S T : Sublocale X
s : Set X
f : ι → X
a b : X
s2 : Sublocale X
carrier : Set X
sInf_mem' : ∀ s ⊆ carrier, sInf s ∈ carrier
himp_mem' : ∀ (a b : X), b ∈ carrier → a ⇨ b ∈ carrier
h :
  Eq.{u_1 + 1} (α := Set X)
    ((fun (x : Sublocale X) ↦ x.carrier) { carrier := carrier, sInf_mem' := sInf_mem', himp_mem' := himp_mem' })
    ((fun (x : Sublocale X) ↦ x.carrier) s2)
⊢ { carrier := carrier, sInf_mem' := sInf_mem', himp_mem' := himp_mem' : Sublocale X } = s2

Tactic:
congr
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
S : Sublocale X
a : X
⊢ a ∈ S.carrier ↔ a ∈ S

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
a : X
carrier : Set X
sInf_mem' : ∀ s ⊆ carrier, sInf s ∈ carrier
himp_mem' : ∀ (a b : X), b ∈ carrier → a ⇨ b ∈ carrier
⊢ a ∈ { carrier := carrier, sInf_mem' := sInf_mem', himp_mem' := himp_mem' : Sublocale X } ↔ a ∈ carrier

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
carrier₁ carrier₂ : Set X
sInf_mem'₁ : ∀ s ⊆ carrier₁, sInf s ∈ carrier₁
sInf_mem'₂ : ∀ s ⊆ carrier₂, sInf s ∈ carrier₂
himp_mem'₁ : ∀ (a b : X), b ∈ carrier₁ → a ⇨ b ∈ carrier₁
himp_mem'₂ : ∀ (a b : X), b ∈ carrier₂ → a ⇨ b ∈ carrier₂
⊢ { carrier := carrier₁, sInf_mem' := sInf_mem'₁, himp_mem' := himp_mem'₁ : Sublocale X } ≤
      { carrier := carrier₂, sInf_mem' := sInf_mem'₂, himp_mem' := himp_mem'₂ } ↔
    carrier₁ ⊆ carrier₂

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, Set.Subset
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
S T : Sublocale X
h : ∀ (x : X), x ∈ S ↔ x ∈ T
⊢ S = T

Tactic:
SetLike.ext h

Premises used: SetLike.ext
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
S : Sublocale X
s : Set X
hs : s ⊆ (↑S : Set X)
⊢ sInf s ∈ S

Tactic:
S.sInf_mem' _ hs

Premises used: Set.Mem, Sublocale.sInf_mem'
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S : Sublocale X
f : ι → X
hf : ∀ (i : ι), f i ∈ S
⊢ (range fun (i : ι) ↦ f i) ⊆ (↑S : Set X)

Tactic:
simpa [range_subset_iff]

Premises used: Set.range_subset_iff
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
S : Sublocale X
a : X
ha : a ∈ (↑S : Set X)
b : X
hb : b ∈ (↑S : Set X)
rw : sInf {a, b} ∈ (↑S : Set X)
⊢ a ⊓ b ∈ (↑S : Set X)

Tactic:
rw [← sInf_pair]

Premises used: sInf_pair
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
S : Sublocale X
a : X
ha : a ∈ (↑S : Set X)
b : X
hb : b ∈ (↑S : Set X)
⊢ sInf {a, b} ∈ (↑S : Set X)

Tactic:
S.sInf_mem (pair_subset ha hb)

Premises used: Set.pair_subset, Set.Mem, Sublocale.sInf_mem
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
S : Sublocale X
a : X
ha : a ∈ (↑S : Set X)
b : X
hb : b ∈ (↑S : Set X)
⊢ sInf {a, b} ∈ (↑S : Set X)

Tactic:
exact S.sInf_mem (pair_subset ha hb)

Premises used: Set.pair_subset, Sublocale.sInf_mem
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
S : Sublocale X
a b : X
ha : a ∈ S
hb : b ∈ S
⊢ a ⊓ b ∈ S

Tactic:
S.infClosed ha hb

Premises used: Sublocale.infClosed
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
S : Sublocale X
⊢ ⊤ ∈ S

Tactic:
simpa using S.sInf_mem <| empty_subset _

Premises used: Sublocale.sInf_mem, Set.empty_subset
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
S : Sublocale X
a b : X
hb : b ∈ S
⊢ a ⇨ b ∈ S

Tactic:
S.himp_mem' _ _ hb

Premises used: Set.Mem, Sublocale.himp_mem'
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S T : Sublocale X
s : Set X
f : ι → X
a b : X
x : Set ↥S
simp_rw : ∀ x_1 ∈ x, Membership.mem (γ := Set ↥S) (Subtype.val (p := fun (x : X) ↦ x ∈ S) ⁻¹' S.carrier) x_1
⊢ Subtype.val (p := fun (x : X) ↦ x ∈ S) '' x ⊆ S.carrier

Tactic:
simp_rw [image_subset_iff, subset_def]

Premises used: Set.subset_def, Set.image_subset_iff
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S T : Sublocale X
s : Set X
f : ι → X
a b : X
x : Set ↥S
⊢ ∀ x_1 ∈ x, Membership.mem (γ := Set ↥S) (Subtype.val (p := fun (x : X) ↦ x ∈ S) ⁻¹' S.carrier) x_1

Tactic:
simp
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
S : Sublocale X
a b : ↥S
⊢ (↑(a ⊓ b) : X) = (↑a : X) ⊓ (↑b : X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
S : Sublocale X
s : Set ↥S
⊢ (↑(sInf s) : X) = sInf (Subtype.val (p := fun (x : X) ↦ x ∈ S) '' s)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S : Sublocale X
f : ι → ↥S
⊢ Eq.{u_1 + 1} (α := X) (↑(⨅ (i : ι), f i) : X) (⨅ (i : ι), (↑(f i) : X))

Tactic:
simp [iInf, ← range_comp, Function.comp_def]

Premises used: Set.range_comp, iInf, Function.comp_def
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S T : Sublocale X
s : Set X
f : ι → X
a b : X
⊢ ∀ (s : Set ↥S), IsGLB s (sInf s)

Tactic:
simp [isGLB_iff_le_iff, lowerBounds, ← Subtype.coe_le_coe]

Premises used: lowerBounds, isGLB_iff_le_iff, Subtype.coe_le_coe
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
S : Sublocale X
a b : ↥S
⊢ (↑(a ⇨ b) : X) = (↑a : X) ⇨ (↑b : X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S T : Sublocale X
s : Set X
f : ι → X
a_1 b_1 : X
a b c : ↥S
⊢ a ≤ b ⇨ c ↔ a ⊓ b ≤ c

Tactic:
simp [← Subtype.coe_le_coe, ← @Sublocale.coe_inf, himp]

Premises used: Sublocale.coe_inf, Subtype.coe_le_coe, HImp.himp
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
S : Sublocale X
a : X
⊢ a ≤ (↑(S.restrictAux a) : X)

Tactic:
simp +contextual [restrictAux]

Premises used: _private.0.Sublocale.restrictAux
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s : Set X
f : ι → X
a b : X
S : Sublocale X
x : X
hx : (↑(S.restrictAux x) : X) ≤ x
rw : (↑(S.restrictAux x) : X) ∈ S
⊢ x ∈ S

Tactic:
rw [le_antisymm le_restrictAux hx]

Premises used: _private.0.Sublocale.le_restrictAux, le_antisymm
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s : Set X
f : ι → X
a b : X
S : Sublocale X
x : X
hx : (↑(S.restrictAux x) : X) ≤ x
⊢ image (α := ↥S) (Subtype.val (p := fun (x : X) ↦ x ∈ S)) {s : ↥S | x ≤ (↑s : X)} ⊆ (↑S : Set X)

Tactic:
simp +contextual [Set.subset_def]

Premises used: Set.subset_def
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s : Set X
f : ι → X
a b : X
S : Sublocale X
x : X
hx : (↑(S.restrictAux x) : X) ≤ x
⊢ (↑(S.restrictAux x) : X) ∈ S

Tactic:
exact S.sInf_mem <| by simp +contextual [Set.subset_def]

Premises used: Sublocale.sInf_mem
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s : Set X
f : ι → X
a_1 b_1 : X
S : Sublocale X
a : X
b : ↥S
mp : S.restrictAux a ≤ b → a ≤ (↑b : X)
mpr : a ≤ (↑b : X) → S.restrictAux a ≤ b
⊢ S.restrictAux a ≤ b ↔ a ≤ (↑b : X)

Tactic:
constructor
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s : Set X
f : ι → X
a_1 b_1 : X
S : Sublocale X
a : X
b : ↥S
h : S.restrictAux a ≤ b
⊢ a ≤ (↑(S.restrictAux a) : X)

Tactic:
simp +contextual [restrictAux]

Premises used: _private.0.Sublocale.restrictAux
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s : Set X
f : ι → X
a_1 b_1 : X
S : Sublocale X
a : X
b : ↥S
h : S.restrictAux a ≤ b
⊢ a ≤ (↑b : X)

Tactic:
exact le_trans (by simp +contextual [restrictAux]) h

Premises used: le_trans
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s : Set X
f : ι → X
a_1 b_1 : X
S : Sublocale X
a : X
b : ↥S
h : a ≤ (↑b : X)
⊢ Membership.mem (γ := Set ↥S) {s : ↥S | a ≤ (↑s : X)} b

Tactic:
simp [h]
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s : Set X
f : ι → X
a_1 b_1 : X
S : Sublocale X
a : X
b : ↥S
h : a ≤ (↑b : X)
⊢ S.restrictAux a ≤ b

Tactic:
exact sInf_le (by simp [h])

Premises used: sInf_le
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s : Set X
f : ι → X
a b : X
S : Sublocale X
x : ↥S
⊢ x ≤ S.restrictAux (↑x : X)

Tactic:
simp [restrictAux]

Premises used: _private.0.Sublocale.restrictAux
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s : Set X
f : ι → X
a_1 b : X
S : Sublocale X
a : X
h : (↑(S.restrictAux a) : X) ≤ a
⊢ Subtype.mk (p := fun (x : X) ↦ x ∈ S) a ⋯ = S.restrictAux a

Tactic:
simp [le_antisymm_iff, restrictAux, sInf_le]

Premises used: le_antisymm_iff, sInf_le, _private.0.Sublocale.restrictAux
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s : Set X
f : ι → X
a_1 b_1 : X
S : Sublocale X
a b : X
change : S.restrictAux (a ⊓ b) = S.restrictAux a ⊓ S.restrictAux b
⊢ Eq.{u_1 + 1} (α := ↥S) (sInf {s : ↥S | a ⊓ b ≤ (↑s : X)})
    (sInf {s : ↥S | a ≤ (↑s : X)} ⊓ sInf {s : ↥S | b ≤ (↑s : X)})

Tactic:
change Sublocale.restrictAux S (a ⊓ b) = Sublocale.restrictAux S a ⊓ Sublocale.restrictAux S b

Premises used: _private.0.Sublocale.restrictAux, Min.min
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s : Set X
f : ι → X
a_1 b_1 : X
S : Sublocale X
a b : X
⊢ S.restrictAux (a ⊓ b) = S.restrictAux a ⊓ S.restrictAux b

Tactic:
eq_of_forall_ge_iff (fun s ↦ Iff.symm ?_)

Premises used: eq_of_forall_ge_iff, Iff.symm
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s : Set X
f : ι → X
a_1 b_1 : X
S : Sublocale X
a b : X
refine : ∀ (s : ↥S), S.restrictAux a ⊓ S.restrictAux b ≤ s ↔ S.restrictAux (a ⊓ b) ≤ s
⊢ S.restrictAux (a ⊓ b) = S.restrictAux a ⊓ S.restrictAux b

Tactic:
refine eq_of_forall_ge_iff (fun s ↦ Iff.symm ?_)

Premises used: eq_of_forall_ge_iff, Iff.symm
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s_1 : Set X
f : ι → X
a_1 b_1 : X
S : Sublocale X
a b : X
s : ↥S
⊢ S.restrictAux a ⊓ S.restrictAux b ≤ s ↔ S.restrictAux a ≤ S.restrictAux b ⇨ s

Tactic:
simp
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s_1 : Set X
f : ι → X
a_1 b_1 : X
S : Sublocale X
a b : X
s : ↥S
rw : a ≤ (↑(S.restrictAux b ⇨ s) : X) ↔ (↑(S.restrictAux b) : X) ≤ a ⇨ (↑s : X)
rw₁ : a ≤ (↑(S.restrictAux b ⇨ s) : X) ↔ a ≤ (↑(S.restrictAux b) : X) ⇨ (↑s : X)
rw₂ rw₃ : a ≤ (↑(S.restrictAux b) : X) ⇨ (↑s : X) ↔ a ≤ (↑(S.restrictAux b) : X) ⇨ (↑s : X)
⊢ S.restrictAux a ≤ S.restrictAux b ⇨ s ↔ (↑(S.restrictAux b) : X) ≤ a ⇨ (↑s : X)

Tactic:
rw [S.giAux.gc.le_iff_le, @le_himp_comm, coe_himp]

Premises used: le_himp_comm, GaloisConnection.le_iff_le, Sublocale.coe_himp, _private.0.Sublocale.giAux, GaloisInsertion.gc
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s_1 : Set X
f : ι → X
a_1 b_1 : X
S : Sublocale X
a b : X
s : ↥S
c : ↥S := Subtype.mk (p := fun (x : X) ↦ x ∈ S) (a ⇨ (↑s : X)) ⋯
change : (↑(S.restrictAux b) : X) ≤ (↑c : X) ↔ b ≤ (↑c : X)
⊢ (↑(S.restrictAux b) : X) ≤ a ⇨ (↑s : X) ↔ b ≤ a ⇨ (↑s : X)

Tactic:
change Sublocale.restrictAux S b ≤ c.val ↔ b ≤ c

Premises used: _private.0.Sublocale.restrictAux, Subtype.val
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s_1 : Set X
f : ι → X
a_1 b_1 : X
S : Sublocale X
a b : X
s : ↥S
c : ↥S := Subtype.mk (p := fun (x : X) ↦ x ∈ S) (a ⇨ (↑s : X)) ⋯
rw : S.restrictAux b ≤ c ↔ b ≤ (↑c : X)
rw₁ rw₂ : b ≤ (↑c : X) ↔ b ≤ (↑c : X)
⊢ (↑(S.restrictAux b) : X) ≤ (↑c : X) ↔ b ≤ (↑c : X)

Tactic:
rw [S.giAux.u_le_u_iff, S.giAux.gc.le_iff_le]

Premises used: GaloisConnection.le_iff_le, _private.0.Sublocale.giAux, GaloisInsertion.u_le_u_iff, GaloisInsertion.gc
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s_1 : Set X
f : ι → X
a_1 b_1 : X
S : Sublocale X
a b : X
s : ↥S
⊢ b ≤ a ⇨ (↑s : X) ↔ S.restrictAux (a ⊓ b) ≤ s

Tactic:
simp [inf_comm, S.giAux.gc.le_iff_le]

Premises used: GaloisConnection.le_iff_le, inf_comm, _private.0.Sublocale.giAux, GaloisInsertion.gc
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s_1 : Set X
f : ι → X
a_1 b_1 : X
S : Sublocale X
a b : X
s : ↥S
_ : S.restrictAux a ⊓ S.restrictAux b ≤ s ↔ S.restrictAux a ≤ S.restrictAux b ⇨ s
_₁ : S.restrictAux a ≤ S.restrictAux b ⇨ s ↔ (↑(S.restrictAux b) : X) ≤ a ⇨ (↑s : X)
_₂ : (↑(S.restrictAux b) : X) ≤ a ⇨ (↑s : X) ↔ b ≤ a ⇨ (↑s : X)
_₃ : b ≤ a ⇨ (↑s : X) ↔ S.restrictAux (a ⊓ b) ≤ s
⊢ S.restrictAux a ⊓ S.restrictAux b ≤ s ↔ S.restrictAux (a ⊓ b) ≤ s

Tactic:
calc
      _ ↔ S.restrictAux a ≤ S.restrictAux b ⇨ s := by simp
      _ ↔ S.restrictAux b ≤ a ⇨ s := by rw [S.giAux.gc.le_iff_le, @le_himp_comm, coe_himp]
      _ ↔ b ≤ a ⇨ s := by
        set c : S := ⟨a ⇨ s, S.himp_mem s.coe_prop⟩
        change Sublocale.restrictAux S b ≤ c.val ↔ b ≤ c
        rw [S.giAux.u_le_u_iff, S.giAux.gc.le_iff_le]
      _ ↔ S.restrictAux (a ⊓ b) ≤ s := by simp [inf_comm, S.giAux.gc.le_iff_le]

Premises used: _private.0.Sublocale.restrictAux, Min.min
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s : Set X
f : ι → X
a b : X
S : Sublocale X
⊢ Eq.{u_1 + 1} (α := ↥S) (sInf {s : ↥S | ⊤ ≤ (↑s : X)}) ⊤

Tactic:
le_antisymm le_top ?_

Premises used: le_antisymm, le_top
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s : Set X
f : ι → X
a b : X
S : Sublocale X
refine : LE.le.{u_1} (α := ↥S) ⊤ (sInf {s : ↥S | ⊤ ≤ (↑s : X)})
⊢ Eq.{u_1 + 1} (α := ↥S) (sInf {s : ↥S | ⊤ ≤ (↑s : X)}) ⊤

Tactic:
refine le_antisymm le_top ?_

Premises used: le_antisymm, le_top
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s : Set X
f : ι → X
a b : X
S : Sublocale X
change : ⊤ ≤ S.restrictAux ⊤
⊢ LE.le.{u_1} (α := ↥S) ⊤ (sInf {s : ↥S | ⊤ ≤ (↑s : X)})

Tactic:
change _ ≤ restrictAux S ⊤

Premises used: _private.0.Sublocale.restrictAux, Top.top
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s : Set X
f : ι → X
a b : X
S : Sublocale X
rw : ⊤ ≤ (↑(S.restrictAux ⊤) : X)
⊢ ⊤ ≤ S.restrictAux ⊤

Tactic:
rw [← Subtype.coe_le_coe, S.giAux.gc.u_top]

Premises used: Subtype.coe_le_coe, GaloisConnection.u_top, _private.0.Sublocale.giAux, GaloisInsertion.gc
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s : Set X
f : ι → X
a b : X
S : Sublocale X
⊢ ⊤ ≤ (↑(S.restrictAux ⊤) : X)

Tactic:
simp [restrictAux, sInf]

Premises used: _private.0.Sublocale.restrictAux, InfSet.sInf
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s_1 : Set X
f : ι → X
a b : X
S : Sublocale X
s : Set X
change : S.restrictAux (sSup s) = sSup ((fun (x : X) ↦ sInf {s : ↥S | x ≤ (↑s : X)}) '' s)
⊢ Eq (α := ↥S) (sInf {s_2 : ↥S | sSup s ≤ (↑s_2 : X)}) (sSup ((fun (x : X) ↦ sInf {s : ↥S | x ≤ (↑s : X)}) '' s))

Tactic:
change Sublocale.restrictAux S (sSup s) = _

Premises used: _private.0.Sublocale.restrictAux, SupSet.sSup
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s_1 : Set X
f : ι → X
a b : X
S : Sublocale X
s : Set X
rw : Eq.{u_1 + 1} (α := ↥S) (⨆ a ∈ s, S.restrictAux a) (⨆ a ∈ s, sInf {s : ↥S | a ≤ (↑s : X)})
⊢ S.restrictAux (sSup s) = sSup ((fun (x : X) ↦ sInf {s : ↥S | x ≤ (↑s : X)}) '' s)

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

Premises used: GaloisConnection.l_sSup, _private.0.Sublocale.giAux, sSup_image, GaloisInsertion.gc
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s_1 : Set X
f : ι → X
a b : X
S : Sublocale X
s : Set X
⊢ Eq.{u_1 + 1} (α := ↥S) (⨆ a ∈ s, S.restrictAux a) (⨆ a ∈ s, sInf {s : ↥S | a ≤ (↑s : X)})

Tactic:
rfl
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
S : Sublocale X
a : X
ha : a ∈ S
⊢ (S.restrict : (a : X) → ↥S) a = Subtype.mk (p := fun (x : X) ↦ x ∈ S) a ha

Tactic:
S.giRestrict.l_u_eq ⟨a, ha⟩

Premises used: setOf, Subtype.mk, Sublocale.giRestrict, GaloisInsertion.l_u_eq
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s : Set X
f : ι → X
a b : X
S : Sublocale X
x x_1 : X
⊢ Eq.{u_1 + 1} (α := X) (↑((S.restrict : (a : X) → ↥S) (x ⊓ x_1)) : X)
    ((↑((S.restrict : (a : X) → ↥S) x) : X) ⊓ (↑((S.restrict : (a : X) → ↥S) x_1) : X))

Tactic:
simp [S.giRestrict.gc.u_inf]

Premises used: GaloisConnection.u_inf, Sublocale.giRestrict, GaloisInsertion.gc
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s : Set X
f : ι → X
a b : X
S : Sublocale X
x : X
rw rw₁ : LE.le.{u_1} (α := X) (↑((S.restrict : (a : X) → ↥S) x) : X) (↑((S.restrict : (a : X) → ↥S) x) : X)
⊢ LE.le (α := X) (↑((S.restrict : (a : X) → ↥S) (↑((S.restrict : (a : X) → ↥S) x) : X)) : X)
    (↑((S.restrict : (a : X) → ↥S) x) : X)

Tactic:
rw [S.giRestrict.gc.l_u_l_eq_l]

Premises used: GaloisConnection.l_u_l_eq_l, Sublocale.giRestrict, GaloisInsertion.gc
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
S : Sublocale X
h : ∀ (x : X), Membership.mem (γ := Set X) (range (ι := X) (⇑S.toNucleus : (a : X) → X)) x ↔ x ∈ (↑S : Set X)
⊢ range (ι := X) (⇑S.toNucleus : (a : X) → X) = (↑S : Set X)

Tactic:
ext x
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
S : Sublocale X
x : X
h : Membership.mem (γ := Set X) (range (ι := X) (⇑S.toNucleus : (a : X) → X)) x → x ∈ (↑S : Set X)
h₁ : x ∈ (↑S : Set X) → Membership.mem (γ := Set X) (range (ι := X) (⇑S.toNucleus : (a : X) → X)) x
⊢ Membership.mem (γ := Set X) (range (ι := X) (⇑S.toNucleus : (a : X) → X)) x ↔ x ∈ (↑S : Set X)

Tactic:
constructor
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
S : Sublocale X
x : X
⊢ Membership.mem (γ := Set X) (range (ι := X) (⇑S.toNucleus : (a : X) → X)) x → x ∈ (↑S : Set X)

Tactic:
simp +contextual [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
S : Sublocale X
x : X
hx : x ∈ (↑S : Set X)
⊢ (S.toNucleus : (a : X) → X) x = x

Tactic:
simp_all
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
S : Sublocale X
x : X
hx : x ∈ (↑S : Set X)
⊢ Membership.mem (γ := Set X) (range (ι := X) (⇑S.toNucleus : (a : X) → X)) x

Tactic:
exact ⟨x, by simp_all⟩
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
S T : Sublocale X
⊢ S.toNucleus ≤ T.toNucleus ↔ T ≤ S

Tactic:
simp [← Nucleus.range_subset_range]

Premises used: Nucleus.range_subset_range
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
n : Nucleus X
a : Set X
h : a ⊆ range (ι := X) (⇑n : (a : X) → X)
rw : (n : (a : X) → X) (sInf a) = sInf a
⊢ Membership.mem (γ := Set X) (range (ι := X) (⇑n : (a : X) → X)) (sInf a)

Tactic:
rw [mem_range]

Premises used: Nucleus.mem_range
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
n : Nucleus X
a : Set X
h : a ⊆ range (ι := X) (⇑n : (a : X) → X)
⊢ (n : (a : X) → X) (sInf a) = sInf a

Tactic:
le_antisymm (le_sInf_iff.mpr (fun b h1 ↦ ?_)) le_apply

Premises used: Iff.mpr, le_sInf_iff, le_antisymm, Nucleus.le_apply
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
n : Nucleus X
a : Set X
h : a ⊆ range (ι := X) (⇑n : (a : X) → X)
refine : ∀ (b : X) (h1 : b ∈ a), (n : (a : X) → X) (sInf a) ≤ b
⊢ (n : (a : X) → X) (sInf a) = sInf a

Tactic:
refine le_antisymm (le_sInf_iff.mpr (fun b h1 ↦ ?_)) le_apply

Premises used: Iff.mpr, le_sInf_iff, le_antisymm
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
n : Nucleus X
a : Set X
h : a ⊆ range (ι := X) (⇑n : (a : X) → X)
b : X
h1 : b ∈ a
⊢ ∀ x ∈ a, (n : (a : X) → X) x = x

Tactic:
simp_rw [subset_def, mem_range] at h

Premises used: Set.subset_def, Nucleus.mem_range
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
n : Nucleus X
a : Set X
b : X
h1 : b ∈ a
h : ∀ x ∈ a, (n : (a : X) → X) x = x
rw : LE.le (α := X) ((n : (a : X) → X) (sInf a) : X) ((n : (a : X) → X) b : X)
⊢ (n : (a : X) → X) (sInf a) ≤ b

Tactic:
rw [← h b h1]
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
n : Nucleus X
a : Set X
b : X
h1 : b ∈ a
h : ∀ x ∈ a, (n : (a : X) → X) x = x
⊢ LE.le (α := X) ((n : (a : X) → X) (sInf a) : X) ((n : (a : X) → X) b : X)

Tactic:
n.monotone (sInf_le h1)

Premises used: Nucleus.monotone, sInf_le
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
n : Nucleus X
a : Set X
b : X
h1 : b ∈ a
h : ∀ x ∈ a, (n : (a : X) → X) x = x
⊢ LE.le (α := X) ((n : (a : X) → X) (sInf a) : X) ((n : (a : X) → X) b : X)

Tactic:
exact n.monotone (sInf_le h1)

Premises used: Nucleus.monotone, sInf_le
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
n : Nucleus X
a b : X
h : Membership.mem (γ := Set X) (range (ι := X) (⇑n : (a : X) → X)) b
rw : ∀ (h : (n : (a : X) → X) b = b), (n : (a : X) → X) (a ⇨ b) = a ⇨ b
rw₁ :
  ∀ (h : Eq (α := X) ((n : (a : X) → X) ((n : (a : X) → X) b : X) : X) ((n : (a : X) → X) b : X)),
    (n : (a : X) → X) (a ⇨ (n : (a : X) → X) b) = a ⇨ (n : (a : X) → X) b
rw₂ rw₃ :
  ∀ (h : Eq (α := X) ((n : (a : X) → X) ((n : (a : X) → X) b : X) : X) ((n : (a : X) → X) b : X)),
    a ⇨ (n : (a : X) → X) b = a ⇨ (n : (a : X) → X) b
⊢ Membership.mem (γ := Set X) (range (ι := X) (⇑n : (a : X) → X)) (a ⇨ b)

Tactic:
rw [mem_range, ← h, map_himp_apply] at *

Premises used: Nucleus.map_himp_apply, Nucleus.mem_range
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
n : Nucleus X
x : X
⊢ x ∈ n.toSublocale ↔ ∃ (y : X), (n : (a : X) → X) y = x

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.range
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
m n : Nucleus X
⊢ m.toSublocale ≤ n.toSublocale ↔ n ≤ m

Tactic:
simp [← SetLike.coe_subset_coe]

Premises used: SetLike.coe_subset_coe
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
n : Nucleus X
x : X
a :
  Eq (α := X) ((↑((n.toSublocale.restrict : (a : X) → ↥n.toSublocale) x) : X) : X)
    ((↑(Subtype.mk (p := fun (x : X) ↦ x ∈ n.toSublocale) ((n : (a : X) → X) x) ⋯) : X) : X)
⊢ Eq (α := ↥n.toSublocale) ((n.toSublocale.restrict : (a : X) → ↥n.toSublocale) x : ↥n.toSublocale)
    (Subtype.mk (p := fun (x : X) ↦ x ∈ n.toSublocale) ((n : (a : X) → X) x) ⋯ : ↥n.toSublocale)

Tactic:
ext
-- Module: Mathlib.Order.Sublocale
Goal:
X : Type u_1
inst : Order.Frame X
n : Nucleus X
x y : X
hxy : x ≤ (n : (a : X) → X) y
⊢ LE.le (α := X) ((n : (a : X) → X) x : X) ((n : (a : X) → X) y : X)

Tactic:
simpa using n.monotone hxy

Premises used: Nucleus.monotone