awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
L : Sublattice α
s : Set α
hs : s = (↑L : Set α)
⊢ L.copy s hs = L

Tactic:
SetLike.coe_injective hs

Premises used: SetLike.coe_injective
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
L M : Sublattice α
⊢ (∀ (a : α), a ∈ L ↔ a ∈ M) → L = M

Tactic:
SetLike.ext

Premises used: SetLike.ext
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
L : Sublattice α
a b : ↥L
⊢ (↑(a ⊔ b) : α) = (↑a : α) ⊔ (↑b : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
L : Sublattice α
a b : ↥L
⊢ (↑(a ⊓ b) : α) = (↑a : α) ⊓ (↑b : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
L : Sublattice α
a b : α
ha : a ∈ L
hb : b ∈ L
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ L) a ha ⊔ Subtype.mk (p := fun (x : α) ↦ x ∈ L) b hb =
    Subtype.mk (p := fun (x : α) ↦ x ∈ L) (a ⊔ b) ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
L : Sublattice α
a b : α
ha : a ∈ L
hb : b ∈ L
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ L) a ha ⊓ Subtype.mk (p := fun (x : α) ↦ x ∈ L) b hb =
    Subtype.mk (p := fun (x : α) ↦ x ∈ L) (a ⊓ b) ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
L : Sublattice α
⊢ Eq (α := (a : ↥L) → α) (⇑L.subtype : (a : ↥L) → α) (Subtype.val (p := fun (x : α) ↦ x ∈ L))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
L : Sublattice α
a : ↥L
⊢ (L.subtype : (a : ↥L) → α) a = (↑a : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
L : Sublattice α
⊢ Injective (α := ↥L) (β := α) (⇑L.subtype : (a : ↥L) → α)

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
L M : Sublattice α
h : L ≤ M
⊢ (⇑(inclusion h) : (a : ↥L) → ↥M) = Set.inclusion (s := (↑L : Set α)) (t := (↑M : Set α)) h

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
L M : Sublattice α
h : L ≤ M
a : ↥L
⊢ (inclusion h : (a : ↥L) → ↥M) a = Set.inclusion (s := (↑L : Set α)) (t := (↑M : Set α)) h a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
L M : Sublattice α
h : L ≤ M
⊢ Injective (α := ↥L) (β := ↥M) (⇑(inclusion h) : (a : ↥L) → ↥M)

Tactic:
Set.inclusion_injective h

Premises used: Set.inclusion_injective
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
L : Sublattice α
⊢ Eq.{u_2 + 1} (α := LatticeHom ↥L ↥L) (inclusion ⋯) (LatticeHom.id ↥L)

Tactic:
rfl

Premises used: LatticeHom.id, rfl, Sublattice.inclusion
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
L M : Sublattice α
h : L ≤ M
⊢ M.subtype.comp (inclusion h) = L.subtype

Tactic:
rfl

Premises used: Sublattice.subtype, Set.Mem, LatticeHom.comp, SupHom.comp, rfl
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
⊢ (↑⊤ : Set α) = univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
⊢ (↑⊥ : Set α) = ∅

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
L M : Sublattice α
⊢ (↑(L ⊓ M) : Set α) = (↑L : Set α) ∩ (↑M : Set α)

Tactic:
rfl

Premises used: setOf, Set.inter, rfl
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
S : Set (Sublattice α)
⊢ (↑(sInf S) : Set α) = ⋂ L ∈ S, (↑L : Set α)

Tactic:
rfl

Premises used: iInf, Set.Mem, Set.iInter, setOf, rfl
-- Module: Mathlib.Order.Sublattice
Goal:
ι : Sort u_1
α : Type u_2
inst : Lattice α
f : ι → Sublattice α
⊢ (↑(⨅ (i : ι), f i) : Set α) = ⋂ (i : ι), (↑(f i) : Set α)

Tactic:
simp [iInf]

Premises used: iInf
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
L : Sublattice α
rw : (↑L : Set α) = (↑⊤ : Set α) ↔ L = ⊤
rw₁ rw₂ : L = ⊤ ↔ L = ⊤
⊢ (↑L : Set α) = univ ↔ L = ⊤

Tactic:
rw [← coe_top, coe_inj]

Premises used: Sublattice.coe_inj, Sublattice.coe_top
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
L : Sublattice α
rw : (↑L : Set α) = (↑⊥ : Set α) ↔ L = ⊥
rw₁ rw₂ : L = ⊥ ↔ L = ⊥
⊢ (↑L : Set α) = ∅ ↔ L = ⊥

Tactic:
rw [← coe_bot, coe_inj]

Premises used: Sublattice.coe_bot, Sublattice.coe_inj
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
a : α
⊢ a ∉ ⊥

Tactic:
id

Premises used: Set.Mem, id, Not
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
a : α
⊢ Membership.mem (γ := Sublattice α) ⊤ a

Tactic:
mem_univ _

Premises used: Set.Mem, Set.univ, setOf, Set.mem_univ
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
L M : Sublattice α
a : α
⊢ a ∈ L ⊓ M ↔ a ∈ L ∧ a ∈ M

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
a : α
S : Set (Sublattice α)
⊢ a ∈ (↑(sInf S) : Set α) ↔ ∀ L ∈ S, a ∈ L

Tactic:
simp
-- Module: Mathlib.Order.Sublattice
Goal:
ι : Sort u_1
α : Type u_2
inst : Lattice α
a : α
f : ι → Sublattice α
⊢ a ∈ (↑(⨅ (i : ι), f i) : Set α) ↔ ∀ (i : ι), a ∈ f i

Tactic:
simp
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
⊢ Subsingleton.{u_2 + 1} (Sublattice α) ↔ IsEmpty α

Tactic:
⟨fun _ ↦ univ_eq_empty_iff.1 <| coe_inj.2 <| Subsingleton.elim ⊤ ⊥,
    fun _ ↦ SetLike.coe_injective.subsingleton⟩

Premises used: Iff.mpr, Function.Injective.subsingleton, Set.univ_eq_empty_iff, Bot.bot, Sublattice.coe_inj, SetLike.coe_injective, Iff.intro, Iff.mp, Subsingleton.elim, Top.top
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
L : Sublattice β
f : LatticeHom α β
⊢ (↑(comap f L) : Set α) = (⇑f : (a : α) → β) ⁻¹' (↑L : Set β)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
f : LatticeHom α β
a : α
L : Sublattice β
⊢ a ∈ comap f L ↔ Membership.mem (α := β) L ((f : (a : α) → β) a : β)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
f : LatticeHom α β
⊢ Monotone (comap f)

Tactic:
fun _ _ ↦ preimage_mono

Premises used: Set.Mem, Monotone, setOf, Set.Subset, Set.preimage_mono, Set.preimage
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
L : Sublattice α
⊢ comap (LatticeHom.id α) L = L

Tactic:
rfl

Premises used: Sublattice.comap, Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Lattice α
inst_1 : Lattice β
inst_2 : Lattice γ
L : Sublattice γ
g : LatticeHom β γ
f : LatticeHom α β
⊢ comap f (comap g L) = comap (g.comp f) L

Tactic:
rfl

Premises used: Sublattice.comap, Set.Mem, setOf, LatticeHom.comp, Set.preimage, rfl
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
f : LatticeHom α β
L : Sublattice α
⊢ (↑(map f L) : Set β) = (⇑f : (a : α) → β) '' (↑L : Set α)

Tactic:
rfl

Premises used: setOf, Set.image, rfl
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
L : Sublattice α
f : LatticeHom α β
b : β
⊢ b ∈ map f L ↔ ∃ a ∈ L, (f : (a : α) → β) a = b

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.image
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
L : Sublattice α
f : LatticeHom α β
a : α
⊢ a ∈ L → Membership.mem (α := β) (map f L) ((f : (a : α) → β) a : β)

Tactic:
mem_image_of_mem f

Premises used: Set.Mem, setOf, Set.mem_image_of_mem, Set.image, DFunLike.coe
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
L : Sublattice α
f : LatticeHom α β
a : ↥L
⊢ Membership.mem (α := β) (map f L) ((f : (a : α) → β) (↑a : α) : β)

Tactic:
mem_map_of_mem f a.prop

Premises used: Sublattice.mem_map_of_mem, Subtype.prop
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
f : LatticeHom α β
⊢ Monotone (map f)

Tactic:
fun _ _ ↦ image_mono

Premises used: Set.Mem, Set.image_mono, Monotone, setOf, Set.Subset, Set.image
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
L : Sublattice α
⊢ map (LatticeHom.id α) L = L

Tactic:
SetLike.coe_injective <| image_id _

Premises used: SetLike.coe_injective, Set.image_id
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Lattice α
inst_1 : Lattice β
inst_2 : Lattice γ
L : Sublattice α
g : LatticeHom β γ
f : LatticeHom α β
⊢ map g (map f L) = map (g.comp f) L

Tactic:
SetLike.coe_injective <| image_image _ _ _

Premises used: Set.image_image, SetLike.coe_injective
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
L : Sublattice α
f : α ≃o β
a : β
⊢ Membership.mem (γ := Sublattice β) (map { toFun := (⇑f : (a : α) → β), map_sup' := ⋯, map_inf' := ⋯ } L) a ↔
    Membership.mem (α := α) L ((f.symm : (a : β) → α) a : α)

Tactic:
Set.mem_image_equiv

Premises used: Set.Mem, setOf, Set.image, Set.mem_image_equiv
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
L : Sublattice α
f : LatticeHom α β
a : α
hf : Injective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ Membership.mem (α := β) (map f L) ((f : (a : α) → β) a : β) ↔ a ∈ L

Tactic:
hf.mem_set_image

Premises used: Set.Mem, setOf, Set.image, Function.Injective.mem_set_image
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
f : α ≃o β
L : Sublattice α
⊢ Eq.{u_3 + 1} (α := Sublattice β) (map { toFun := (⇑f : (a : α) → β), map_sup' := ⋯, map_inf' := ⋯ } L)
    (comap { toFun := (⇑f.symm : (a : β) → α), map_sup' := ⋯, map_inf' := ⋯ } L)

Tactic:
SetLike.coe_injective <| f.toEquiv.image_eq_preimage_symm L

Premises used: SetLike.coe_injective, Equiv.image_eq_preimage_symm, SetLike.coe, RelIso.toEquiv
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
f : β ≃o α
L : Sublattice α
⊢ Eq.{u_3 + 1} (α := Sublattice β) (comap { toFun := (⇑f : (a : β) → α), map_sup' := ⋯, map_inf' := ⋯ } L)
    (map { toFun := (⇑f.symm : (a : α) → β), map_sup' := ⋯, map_inf' := ⋯ } L)

Tactic:
(map_equiv_eq_comap_symm f.symm L).symm

Premises used: Sublattice.map_equiv_eq_comap_symm, OrderIso.symm, Eq.symm
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
L : Sublattice α
M : Sublattice β
e : β ≃o α
simp_rw :
  (↑(map { toFun := (⇑e.symm : (a : α) → β), map_sup' := ⋯, map_inf' := ⋯ : LatticeHom α β } L) : Set β) =
      (↑M : Set β) ↔
    (↑L : Set α) = (↑(map { toFun := (⇑e : (a : β) → α), map_sup' := ⋯, map_inf' := ⋯ } M) : Set α)
⊢ map { toFun := (⇑e.symm : (a : α) → β), map_sup' := ⋯, map_inf' := ⋯ } L = M ↔
    L = map { toFun := (⇑e : (a : β) → α), map_sup' := ⋯, map_inf' := ⋯ } M

Tactic:
simp_rw [← coe_inj]

Premises used: Sublattice.coe_inj
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
L : Sublattice α
M : Sublattice β
e : β ≃o α
⊢ (↑(map { toFun := (⇑e.symm : (a : α) → β), map_sup' := ⋯, map_inf' := ⋯ : LatticeHom α β } L) : Set β) =
      (↑M : Set β) ↔
    (↑L : Set α) = (↑(map { toFun := (⇑e : (a : β) → α), map_sup' := ⋯, map_inf' := ⋯ } M) : Set α)

Tactic:
(Equiv.eq_image_iff_symm_image_eq _ _ _).symm

Premises used: setOf, Equiv.eq_image_iff_symm_image_eq, Set.image, Iff.symm
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
L : Sublattice α
M : Sublattice β
e : β ≃o α
⊢ (↑(map { toFun := (⇑e.symm : (a : α) → β), map_sup' := ⋯, map_inf' := ⋯ : LatticeHom α β } L) : Set β) =
      (↑M : Set β) ↔
    (↑L : Set α) = (↑(map { toFun := (⇑e : (a : β) → α), map_sup' := ⋯, map_inf' := ⋯ } M) : Set α)

Tactic:
exact (Equiv.eq_image_iff_symm_image_eq _ _ _).symm

Premises used: Equiv.eq_image_iff_symm_image_eq, Iff.symm
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
L : Sublattice α
f : LatticeHom α β
M : Sublattice β
⊢ map f L ≤ M ↔ L ≤ comap f M

Tactic:
image_subset_iff

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage, Set.image, Set.image_subset_iff
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
f : LatticeHom α β
⊢ GaloisConnection (map f) (comap f)

Tactic:
fun _ _ ↦ map_le_iff_le_comap

Premises used: Sublattice.map_le_iff_le_comap, GaloisConnection
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
f : LatticeHom α β
⊢ map f ⊥ = ⊥

Tactic:
(gc_map_comap f).l_bot

Premises used: Sublattice.gc_map_comap, GaloisConnection.l_bot
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
f : LatticeHom α β
L M : Sublattice α
⊢ map f (L ⊔ M) = map f L ⊔ map f M

Tactic:
(gc_map_comap f).l_sup

Premises used: Sublattice.gc_map_comap, GaloisConnection.l_sup
-- Module: Mathlib.Order.Sublattice
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
f : LatticeHom α β
L : ι → Sublattice α
⊢ map f (⨆ (i : ι), L i) = ⨆ (i : ι), map f (L i)

Tactic:
(gc_map_comap f).l_iSup

Premises used: Sublattice.gc_map_comap, GaloisConnection.l_iSup
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
f : LatticeHom α β
⊢ comap f ⊤ = ⊤

Tactic:
(gc_map_comap f).u_top

Premises used: Sublattice.gc_map_comap, GaloisConnection.u_top
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
L M : Sublattice β
f : LatticeHom α β
⊢ comap f (L ⊓ M) = comap f L ⊓ comap f M

Tactic:
(gc_map_comap f).u_inf

Premises used: Sublattice.gc_map_comap, GaloisConnection.u_inf
-- Module: Mathlib.Order.Sublattice
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
f : LatticeHom α β
s : ι → Sublattice β
⊢ comap f (iInf s) = ⨅ (i : ι), comap f (s i)

Tactic:
(gc_map_comap f).u_iInf

Premises used: Sublattice.gc_map_comap, GaloisConnection.u_iInf
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
L M : Sublattice α
f : LatticeHom α β
⊢ map f (L ⊓ M) ≤ map f L ⊓ map f M

Tactic:
map_mono.map_inf_le _ _

Premises used: Set.Mem, Sublattice.map_mono, Monotone.map_inf_le
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
L M : Sublattice β
f : LatticeHom α β
⊢ comap f L ⊔ comap f M ≤ comap f (L ⊔ M)

Tactic:
comap_mono.le_map_sup _ _

Premises used: Monotone.le_map_sup, Sublattice.comap_mono
-- Module: Mathlib.Order.Sublattice
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
f : LatticeHom α β
L : ι → Sublattice β
⊢ ⨆ (i : ι), comap f (L i) ≤ comap f (⨆ (i : ι), L i)

Tactic:
comap_mono.le_map_iSup

Premises used: Set.Mem, Monotone.le_map_iSup, Sublattice.comap_mono
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
L M : Sublattice α
f : LatticeHom α β
hf : Injective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
rw : (↑(map f (L ⊓ M)) : Set β) = (↑(map f L ⊓ map f M) : Set β)
⊢ map f (L ⊓ M) = map f L ⊓ map f M

Tactic:
rw [← SetLike.coe_set_eq]

Premises used: SetLike.coe_set_eq
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
L M : Sublattice α
f : LatticeHom α β
hf : Injective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ (↑(map f (L ⊓ M)) : Set β) = (↑(map f L ⊓ map f M) : Set β)

Tactic:
simp [Set.image_inter hf]

Premises used: Set.image_inter
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
f : LatticeHom α β
h : Surjective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ (↑(map f ⊤) : Set β) = (↑⊤ : Set β)

Tactic:
simp [h.range_eq]

Premises used: Function.Surjective.range_eq
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
L : Sublattice α
M : Sublattice β
p : α × β
⊢ p ∈ L.prod M ↔ p.1 ∈ L ∧ p.2 ∈ M

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.prod
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
L₁ L₂ : Sublattice α
M₁ M₂ : Sublattice β
hL : L₁ ≤ L₂
hM : M₁ ≤ M₂
⊢ L₁.prod M₁ ≤ L₂.prod M₂

Tactic:
Set.prod_mono hL hM

Premises used: Set.Mem, setOf, Set.prod, Set.Subset, Set.prod_mono
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
L₁ L₂ : Sublattice α
M : Sublattice β
hL : L₁ ≤ L₂
⊢ L₁.prod M ≤ L₂.prod M

Tactic:
prod_mono hL le_rfl

Premises used: le_rfl, Sublattice.prod_mono
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
L : Sublattice α
M₁ M₂ : Sublattice β
hM : M₁ ≤ M₂
⊢ L.prod M₁ ≤ L.prod M₂

Tactic:
prod_mono le_rfl hM

Premises used: le_rfl, Sublattice.prod_mono
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
M : Sublattice α
⊢ Monotone (β := Sublattice (α × α)) fun (L : Sublattice α) ↦ L.prod M

Tactic:
fun _ _ ↦ prod_mono_left

Premises used: Sublattice.prod_mono_left, Set.Mem, Monotone
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
L : Sublattice α
⊢ Monotone (β := Sublattice (α × β)) fun (M : Sublattice β) ↦ L.prod M

Tactic:
fun _ _ ↦ prod_mono_right

Premises used: Set.Mem, Monotone, Sublattice.prod_mono_right
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
L : Sublattice α
a : α × β
⊢ Membership.mem (γ := Sublattice (α × β)) (L.prod ⊤) a ↔
    Membership.mem (γ := Sublattice (α × β)) (comap LatticeHom.fst L) a

Tactic:
simp [mem_prod, LatticeHom.coe_fst]

Premises used: Sublattice.mem_prod, LatticeHom.coe_fst
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
L : Sublattice β
a : α × β
⊢ Membership.mem (γ := Sublattice (α × β)) (prod ⊤ L) a ↔
    Membership.mem (γ := Sublattice (α × β)) (comap LatticeHom.snd L) a

Tactic:
simp [mem_prod, LatticeHom.coe_snd]

Premises used: Sublattice.mem_prod, LatticeHom.coe_snd
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
⊢ Eq (α := Sublattice (α × β)) (prod ⊤ ⊤) ⊤

Tactic:
(top_prod _).trans <| comap_top _

Premises used: Sublattice.comap_top, Sublattice.top_prod, Eq.trans
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
L : Sublattice α
⊢ Eq (α := Sublattice (α × β)) (L.prod ⊥) ⊥

Tactic:
SetLike.coe_injective prod_empty

Premises used: Set.prod_empty, SetLike.coe_injective
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
M : Sublattice β
⊢ Eq (α := Sublattice (α × β)) (prod ⊥ M) ⊥

Tactic:
SetLike.coe_injective empty_prod

Premises used: Set.empty_prod, SetLike.coe_injective
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
L : Sublattice α
M : Sublattice β
N : Sublattice (α × β)
⊢ N ≤ L.prod M ↔ N ≤ comap LatticeHom.fst L ∧ N ≤ comap LatticeHom.snd M

Tactic:
simp [SetLike.le_def, forall_and]

Premises used: SetLike.le_def, forall_and
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
L : Sublattice α
M : Sublattice β
⊢ L.prod M = ⊥ ↔ L = ⊥ ∨ M = ⊥

Tactic:
simpa only [← coe_inj] using Set.prod_eq_empty_iff

Premises used: Sublattice.coe_inj, Set.prod_eq_empty_iff
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
L : Sublattice α
inst_2 : Nonempty α
inst_3 : Nonempty β
M : Sublattice β
⊢ L.prod M = ⊤ ↔ L = ⊤ ∧ M = ⊤

Tactic:
simpa only [← coe_inj] using Set.prod_eq_univ

Premises used: Sublattice.coe_inj, Set.prod_eq_univ
-- Module: Mathlib.Order.Sublattice
Goal:
κ : Type u_5
π : κ → Type u_6
inst : (i : κ) → Lattice (π i)
s : Set κ
L : (i : κ) → Sublattice (π i)
x : (i : κ) → π i
⊢ x ∈ pi (π := π) s L ↔ ∀ i ∈ s, x i ∈ L i

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.pi
-- Module: Mathlib.Order.Sublattice
Goal:
κ : Type u_5
π : κ → Type u_6
inst : (i : κ) → Lattice (π i)
L : (i : κ) → Sublattice (π i)
a : (i : κ) → π i
⊢ a ∈ pi (π := π) ∅ L ↔ Membership.mem (γ := Sublattice ((i : κ) → π i)) ⊤ a

Tactic:
simp [mem_pi]

Premises used: Sublattice.mem_pi
-- Module: Mathlib.Order.Sublattice
Goal:
κ : Type u_5
π : κ → Type u_6
inst : (i : κ) → Lattice (π i)
s : Set κ
a : (i : κ) → π i
⊢ Membership.mem (γ := Sublattice ((i : κ) → π i)) (pi (π := π) s fun (x : κ) ↦ ⊤) a ↔
    Membership.mem (γ := Sublattice ((i : κ) → π i)) ⊤ a

Tactic:
simp [mem_pi]

Premises used: Sublattice.mem_pi
-- Module: Mathlib.Order.Sublattice
Goal:
κ : Type u_5
π : κ → Type u_6
inst : (i : κ) → Lattice (π i)
s : Set κ
hs : s.Nonempty
a : (i : κ) → π i
⊢ Membership.mem (γ := Sublattice ((i : κ) → π i)) (pi (π := π) s fun (x : κ) ↦ ⊥) a ↔
    Membership.mem (γ := Sublattice ((i : κ) → π i)) ⊥ a

Tactic:
simpa [mem_pi] using hs

Premises used: Sublattice.mem_pi
-- Module: Mathlib.Order.Sublattice
Goal:
κ : Type u_5
π : κ → Type u_6
inst : (i : κ) → Lattice (π i)
inst_1 : Nonempty κ
⊢ Eq (α := Sublattice ((i : κ) → π i)) (pi (π := π) univ fun (x : κ) ↦ ⊥) ⊥

Tactic:
simp
-- Module: Mathlib.Order.Sublattice
Goal:
κ : Type u_5
π : κ → Type u_6
inst : (i : κ) → Lattice (π i)
s : Set κ
L : (i : κ) → Sublattice (π i)
M : Sublattice ((i : κ) → π i)
simp : (∀ ⦃x : (i : κ) → π i⦄, x ∈ M → ∀ i ∈ s, x i ∈ L i) ↔ ∀ i ∈ s, ∀ ⦃x : (i : κ) → π i⦄, x ∈ M → x i ∈ L i
⊢ M ≤ pi (π := π) s L ↔ ∀ i ∈ s, M ≤ comap (Pi.evalLatticeHom (α := π) i) (L i)

Tactic:
simp [SetLike.le_def]

Premises used: SetLike.le_def
-- Module: Mathlib.Order.Sublattice
Goal:
κ : Type u_5
π : κ → Type u_6
inst : (i : κ) → Lattice (π i)
s : Set κ
L : (i : κ) → Sublattice (π i)
M : Sublattice ((i : κ) → π i)
⊢ (∀ ⦃x : (i : κ) → π i⦄, x ∈ M → ∀ i ∈ s, x i ∈ L i) ↔ ∀ i ∈ s, ∀ ⦃x : (i : κ) → π i⦄, x ∈ M → x i ∈ L i

Tactic:
grind
-- Module: Mathlib.Order.Sublattice
Goal:
κ : Type u_5
π : κ → Type u_6
inst : (i : κ) → Lattice (π i)
L : (i : κ) → Sublattice (π i)
simp_rw :
  (↑(pi (π := π) univ L) : Set ((i : κ) → π i)) = (↑⊥ : Set ((i : κ) → π i)) ↔
    ∃ (i : κ), (↑(L i) : Set (π i)) = (↑⊥ : Set (π i))
⊢ pi (π := π) univ L = ⊥ ↔ ∃ (i : κ), L i = ⊥

Tactic:
simp_rw [← coe_inj]

Premises used: Sublattice.coe_inj
-- Module: Mathlib.Order.Sublattice
Goal:
κ : Type u_5
π : κ → Type u_6
inst : (i : κ) → Lattice (π i)
L : (i : κ) → Sublattice (π i)
⊢ (↑(pi (π := π) univ L) : Set ((i : κ) → π i)) = (↑⊥ : Set ((i : κ) → π i)) ↔
    ∃ (i : κ), (↑(L i) : Set (π i)) = (↑⊥ : Set (π i))

Tactic:
simp
-- Module: Mathlib.Order.Sublattice
Goal:
κ : Type u_5
π : κ → Type u_6
inst : (i : κ) → Lattice (π i)
L : (i : κ) → Sublattice (π i)
i : κ
hL : L i = ⊥
⊢ pi (π := π) univ L = ⊥

Tactic:
pi_univ_eq_bot_iff.2 ⟨i, hL⟩

Premises used: Iff.mpr, Sublattice.pi_univ_eq_bot_iff, Exists.intro
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
f : LatticeHom α β
⊢ (↑(range f) : Set β) = Set.range.{u_3, u_2 + 1} (ι := α) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: setOf, Set.range, rfl