awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.UpperLower.Principal
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Membership.mem (γ := UpperSet α) (Ioi a) b ↔ a < b

Tactic:
Iff.rfl

Premises used: Set.Ioi, Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Order.UpperLower.Principal
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
a : α
a₁ :
  ∀ (x : β),
    x ∈ (↑((map f : (a : UpperSet α) → UpperSet β) (Ici a) : UpperSet β) : Set β) ↔
      x ∈ (↑(Ici ((f : (a : α) → β) a) : UpperSet β) : Set β)
⊢ Eq.{u_2 + 1} (α := UpperSet β) ((map f : (a : UpperSet α) → UpperSet β) (Ici a) : UpperSet β)
    (Ici ((f : (a : α) → β) a) : UpperSet β)

Tactic:
ext
-- Module: Mathlib.Order.UpperLower.Principal
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
a : α
x : β
⊢ x ∈ (↑((map f : (a : UpperSet α) → UpperSet β) (Ici a) : UpperSet β) : Set β) ↔
    x ∈ (↑(Ici ((f : (a : α) → β) a) : UpperSet β) : Set β)

Tactic:
simp
-- Module: Mathlib.Order.UpperLower.Principal
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
a : α
a₁ :
  ∀ (x : β),
    x ∈ (↑((map f : (a : UpperSet α) → UpperSet β) (Ioi a) : UpperSet β) : Set β) ↔
      x ∈ (↑(Ioi ((f : (a : α) → β) a) : UpperSet β) : Set β)
⊢ Eq.{u_2 + 1} (α := UpperSet β) ((map f : (a : UpperSet α) → UpperSet β) (Ioi a) : UpperSet β)
    (Ioi ((f : (a : α) → β) a) : UpperSet β)

Tactic:
ext
-- Module: Mathlib.Order.UpperLower.Principal
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
a : α
x : β
⊢ x ∈ (↑((map f : (a : UpperSet α) → UpperSet β) (Ioi a) : UpperSet β) : Set β) ↔
    x ∈ (↑(Ioi ((f : (a : α) → β) a) : UpperSet β) : Set β)

Tactic:
simp
-- Module: Mathlib.Order.UpperLower.Principal
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ LE.le (α := UpperSet α) (Ici a) (Ioi a)

Tactic:
Ioi_subset_Ici_self

Premises used: Set.Ioi, Set.Ici, setOf, Set.Ioi_subset_Ici_self
-- Module: Mathlib.Order.UpperLower.Principal
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderBot α
⊢ Eq.{u_1 + 1} (α := UpperSet α) (Ici ⊥) ⊥

Tactic:
SetLike.coe_injective Ici_bot

Premises used: SetLike.coe_injective, Set.Ici_bot
-- Module: Mathlib.Order.UpperLower.Principal
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderTop α
⊢ Eq.{u_1 + 1} (α := UpperSet α) (Ioi ⊤) ⊤

Tactic:
SetLike.coe_injective Ioi_top

Premises used: Set.Ioi_top, SetLike.coe_injective
-- Module: Mathlib.Order.UpperLower.Principal
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ Ne (α := UpperSet α) (Ici a) ⊤

Tactic:
SetLike.coe_ne_coe.1 nonempty_Ici.ne_empty

Premises used: Set.Nonempty.ne_empty, SetLike.coe_ne_coe, Iff.mp, Set.nonempty_Ici
-- Module: Mathlib.Order.UpperLower.Principal
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ LT.lt (α := UpperSet α) (Ici a) ⊤

Tactic:
lt_top_iff_ne_top.2 Ici_ne_top

Premises used: Iff.mpr, UpperSet.Ici_ne_top, lt_top_iff_ne_top
-- Module: Mathlib.Order.UpperLower.Principal
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
a : α
⊢ s ≤ Ici a ↔ a ∈ s

Tactic:
⟨fun h ↦ h le_rfl, fun ha ↦ s.upper.Ici_subset ha⟩

Premises used: le_rfl, IsUpperSet.Ici_subset, Iff.intro, UpperSet.upper
-- Module: Mathlib.Order.UpperLower.Principal
Goal:
α : Type u_1
inst : Preorder α
⊢ StrictMono.{u_1, u_1} (α := α) (β := UpperSet α) Ici

Tactic:
fun _ _ h ↦ (Set.Ici_ssubset_Ici).mpr h

Premises used: Iff.mpr, Set.Ici, StrictMono, Set.Ici_ssubset_Ici, setOf
-- Module: Mathlib.Order.UpperLower.Principal
Goal:
α : Type u_1
inst : Preorder α
⊢ StrictMono.{u_1, u_1} (α := α) (β := UpperSet α) Ioi

Tactic:
fun _ _ h ↦ Set.Ioi_ssubset_Ioi h

Premises used: Set.Ioi, Set.Ioi_ssubset_Ioi, StrictMono, setOf
-- Module: Mathlib.Order.UpperLower.Principal
Goal:
α : Type u_1
inst : PartialOrder α
⊢ Injective.{u_1 + 1, u_1 + 1} (α := α) (β := UpperSet α) Ici

Tactic:
fun _a _b hab ↦
  Set.Ici_injective <| congr_arg ((↑) : _ → Set α) hab

Premises used: Set.Ici_injective, Function.Injective
-- Module: Mathlib.Order.UpperLower.Principal
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
⊢ Eq (α := UpperSet α) (Ici a) (Ici b) ↔ a = b

Tactic:
Ici_injective.eq_iff

Premises used: UpperSet.Ici_injective, Function.Injective.eq_iff
-- Module: Mathlib.Order.UpperLower.Principal
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
⊢ Ne (α := UpperSet α) (Ici a) (Ici b) ↔ a ≠ b

Tactic:
Ici_inj.not

Premises used: Iff.not, UpperSet.Ici_inj
-- Module: Mathlib.Order.UpperLower.Principal
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
a : α
⊢ Eq (α := UpperSet α) (Ioi a) ⊤ ↔ a = ⊤

Tactic:
simp [UpperSet.ext_iff]

Premises used: UpperSet.ext_iff
-- Module: Mathlib.Order.UpperLower.Principal
Goal:
α : Type u_1
inst : SemilatticeSup α
a b : α
⊢ Eq (α := UpperSet α) (Ici (a ⊔ b)) (Ici a ⊔ Ici b)

Tactic:
ext Ici_inter_Ici.symm

Premises used: UpperSet.ext, Set.Ici_inter_Ici, Eq.symm
-- Module: Mathlib.Order.UpperLower.Principal
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
c : α
⊢ Membership.mem (γ := UpperSet α) (Ici (sSup S)) c ↔ Membership.mem (γ := UpperSet α) (⨆ a ∈ S, Ici a) c

Tactic:
simp only [mem_Ici_iff, mem_iSup_iff, sSup_le_iff]

Premises used: UpperSet.mem_iSup_iff, UpperSet.mem_Ici_iff, sSup_le_iff
-- Module: Mathlib.Order.UpperLower.Principal
Goal:
α : Type u_1
ι : Sort u_3
inst : CompleteLattice α
f : ι → α
c : α
⊢ Membership.mem (γ := UpperSet α) (Ici (⨆ (i : ι), f i)) c ↔ Membership.mem (γ := UpperSet α) (⨆ (i : ι), Ici (f i)) c

Tactic:
simp only [mem_Ici_iff, mem_iSup_iff, iSup_le_iff]

Premises used: UpperSet.mem_iSup_iff, UpperSet.mem_Ici_iff, iSup_le_iff
-- Module: Mathlib.Order.UpperLower.Principal
Goal:
α : Type u_1
ι : Sort u_3
κ : ι → Sort u_4
inst : CompleteLattice α
f : (i : ι) → κ i → α
⊢ Eq.{u_1 + 1} (α := UpperSet α) (Ici (⨆ (i : ι), ⨆ (j : κ i), f i j)) (⨆ (i : ι), ⨆ (j : κ i), Ici (f i j))

Tactic:
simp
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set α
t : Set β
hs : IsUpperSet s
ht : IsUpperSet t
⊢ IsUpperSet (s ×ˢ t)

Tactic:
fun _ _ h ha => ⟨hs h.1 ha.1, ht h.2 ha.2⟩

Premises used: Set.Mem, setOf, IsUpperSet, Set.prod, And.right, And.left, And.intro
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set α
t : Set β
hs : IsLowerSet s
ht : IsLowerSet t
⊢ IsLowerSet (s ×ˢ t)

Tactic:
fun _ _ h ha => ⟨hs h.1 ha.1, ht h.2 ha.2⟩

Premises used: Set.Mem, setOf, Set.prod, And.right, And.left, IsLowerSet, And.intro
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : UpperSet α
t : UpperSet β
⊢ (↑(s ×ˢ t) : Set (α × β)) = (↑s : Set α) ×ˢ (↑t : Set β)

Tactic:
rfl

Premises used: setOf, Set.prod, rfl
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
x : α × β
s : UpperSet α
t : UpperSet β
⊢ x ∈ s ×ˢ t ↔ x.1 ∈ s ∧ x.2 ∈ t

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.prod
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
x : α × β
⊢ Ici x = SProd.sprod (α := UpperSet α) (β := UpperSet β) (Ici x.1) (Ici x.2)

Tactic:
rfl

Premises used: Set.Ici, Set.Mem, setOf, Set.prod, UpperSet.Ici, UpperSet.prod, rfl
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a : α
b : β
⊢ SProd.sprod (α := UpperSet α) (β := UpperSet β) (Ici a) (Ici b) = Ici (a, b)

Tactic:
rfl

Premises used: Set.Ici, Set.Mem, setOf, Set.prod, UpperSet.Ici, UpperSet.prod, rfl
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : UpperSet α
⊢ SProd.sprod (β := UpperSet β) s ⊤ = ⊤

Tactic:
ext prod_empty

Premises used: Set.prod_empty, UpperSet.ext
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
t : UpperSet β
⊢ SProd.sprod (α := UpperSet α) ⊤ t = ⊤

Tactic:
ext empty_prod

Premises used: Set.empty_prod, UpperSet.ext
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
⊢ SProd.sprod (α := UpperSet α) (β := UpperSet β) ⊥ ⊥ = ⊥

Tactic:
ext univ_prod_univ

Premises used: Set.univ_prod_univ, UpperSet.ext
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s₁ s₂ : UpperSet α
t : UpperSet β
⊢ (s₁ ⊔ s₂) ×ˢ t = s₁ ×ˢ t ⊔ s₂ ×ˢ t

Tactic:
ext inter_prod

Premises used: UpperSet.ext, Set.inter_prod
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : UpperSet α
t₁ t₂ : UpperSet β
⊢ s ×ˢ (t₁ ⊔ t₂) = s ×ˢ t₁ ⊔ s ×ˢ t₂

Tactic:
ext prod_inter

Premises used: Set.prod_inter, UpperSet.ext
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s₁ s₂ : UpperSet α
t : UpperSet β
⊢ (s₁ ⊓ s₂) ×ˢ t = s₁ ×ˢ t ⊓ s₂ ×ˢ t

Tactic:
ext union_prod

Premises used: Set.union_prod, UpperSet.ext
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : UpperSet α
t₁ t₂ : UpperSet β
⊢ s ×ˢ (t₁ ⊓ t₂) = s ×ˢ t₁ ⊓ s ×ˢ t₂

Tactic:
ext prod_union

Premises used: UpperSet.ext, Set.prod_union
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s₁ s₂ : UpperSet α
t₁ t₂ : UpperSet β
⊢ s₁ ×ˢ t₁ ⊔ s₂ ×ˢ t₂ = (s₁ ⊔ s₂) ×ˢ (t₁ ⊔ t₂)

Tactic:
ext prod_inter_prod

Premises used: UpperSet.ext, Set.prod_inter_prod
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s₁ s₂ : UpperSet α
t₁ t₂ : UpperSet β
⊢ s₁ ≤ s₂ → t₁ ≤ t₂ → s₁ ×ˢ t₁ ≤ s₂ ×ˢ t₂

Tactic:
Set.prod_mono

Premises used: Set.Mem, setOf, Set.prod, Set.prod_mono
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s₁ s₂ : UpperSet α
t : UpperSet β
⊢ s₁ ≤ s₂ → s₁ ×ˢ t ≤ s₂ ×ˢ t

Tactic:
Set.prod_mono_left

Premises used: Set.Mem, setOf, Set.prod, Set.prod_mono_left
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : UpperSet α
t₁ t₂ : UpperSet β
⊢ t₁ ≤ t₂ → s ×ˢ t₁ ≤ s ×ˢ t₂

Tactic:
Set.prod_mono_right

Premises used: Set.prod_mono_right, Set.Mem, setOf, Set.prod
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
inst : Preorder α
s₁ s₂ : UpperSet α
⊢ s₁ ×ˢ s₁ ≤ s₂ ×ˢ s₂ ↔ s₁ ≤ s₂

Tactic:
prod_self_subset_prod_self

Premises used: setOf, Set.prod, Set.prod_self_subset_prod_self
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
inst : Preorder α
s₁ s₂ : UpperSet α
⊢ s₁ ×ˢ s₁ < s₂ ×ˢ s₂ ↔ s₁ < s₂

Tactic:
prod_self_ssubset_prod_self

Premises used: setOf, Set.prod, Set.prod_self_ssubset_prod_self
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s₁ s₂ : UpperSet α
t₁ t₂ : UpperSet β
⊢ (↑s₂ : Set α) ⊆ (↑s₁ : Set α) ∧ (↑t₂ : Set β) ⊆ (↑t₁ : Set β) ∨ (↑s₂ : Set α) = ∅ ∨ (↑t₂ : Set β) = ∅ ↔
    s₁ ≤ s₂ ∧ t₁ ≤ t₂ ∨ s₂ = ⊤ ∨ t₂ = ⊤

Tactic:
simp
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : UpperSet α
t : UpperSet β
simp_rw : (↑(s ×ˢ t) : Set (α × β)) = (↑⊤ : Set (α × β)) ↔ (↑s : Set α) = (↑⊤ : Set α) ∨ (↑t : Set β) = (↑⊤ : Set β)
⊢ s ×ˢ t = ⊤ ↔ s = ⊤ ∨ t = ⊤

Tactic:
simp_rw [SetLike.ext'_iff]

Premises used: SetLike.ext'_iff
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : UpperSet α
t : UpperSet β
⊢ (↑(s ×ˢ t) : Set (α × β)) = (↑⊤ : Set (α × β)) ↔ (↑s : Set α) = (↑⊤ : Set α) ∨ (↑t : Set β) = (↑⊤ : Set β)

Tactic:
prod_eq_empty_iff

Premises used: setOf, Set.prod, Set.prod_eq_empty_iff
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : UpperSet α
t : UpperSet β
⊢ (↑(s ×ˢ t) : Set (α × β)) = (↑⊤ : Set (α × β)) ↔ (↑s : Set α) = (↑⊤ : Set α) ∨ (↑t : Set β) = (↑⊤ : Set β)

Tactic:
exact prod_eq_empty_iff

Premises used: Set.prod_eq_empty_iff
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s₁ s₂ : UpperSet α
t₁ t₂ : UpperSet β
simp_rw : s₁ ×ˢ t₁ ⊔ s₂ ×ˢ t₂ = ⊤ ↔ s₁ ⊔ s₂ = ⊤ ∨ t₁ ⊔ t₂ = ⊤
simp_rw₁ : (s₁ ⊔ s₂) ×ˢ (t₁ ⊔ t₂) = ⊤ ↔ s₁ ⊔ s₂ = ⊤ ∨ t₁ ⊔ t₂ = ⊤
⊢ Codisjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Codisjoint s₁ s₂ ∨ Codisjoint t₁ t₂

Tactic:
simp_rw [codisjoint_iff, prod_sup_prod, prod_eq_top]

Premises used: codisjoint_iff, UpperSet.prod_sup_prod, UpperSet.prod_eq_top
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : LowerSet α
t : LowerSet β
⊢ (↑(s ×ˢ t) : Set (α × β)) = (↑s : Set α) ×ˢ (↑t : Set β)

Tactic:
rfl

Premises used: setOf, Set.prod, rfl
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
x : α × β
s : LowerSet α
t : LowerSet β
⊢ x ∈ s ×ˢ t ↔ x.1 ∈ s ∧ x.2 ∈ t

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.prod
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
x : α × β
⊢ Iic x = SProd.sprod (α := LowerSet α) (β := LowerSet β) (Iic x.1) (Iic x.2)

Tactic:
rfl

Premises used: LowerSet.prod, Set.Mem, setOf, Set.prod, Set.Iic, rfl, LowerSet.Iic
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a : α
b : β
⊢ SProd.sprod (α := LowerSet α) (β := LowerSet β) (Iic a) (Iic b) = Iic (a, b)

Tactic:
rfl

Premises used: LowerSet.prod, Set.Mem, setOf, Set.prod, Set.Iic, rfl, LowerSet.Iic
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : LowerSet α
⊢ SProd.sprod (β := LowerSet β) s ⊥ = ⊥

Tactic:
ext prod_empty

Premises used: Set.prod_empty, LowerSet.ext
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
t : LowerSet β
⊢ SProd.sprod (α := LowerSet α) ⊥ t = ⊥

Tactic:
ext empty_prod

Premises used: Set.empty_prod, LowerSet.ext
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
⊢ SProd.sprod (α := LowerSet α) (β := LowerSet β) ⊤ ⊤ = ⊤

Tactic:
ext univ_prod_univ

Premises used: Set.univ_prod_univ, LowerSet.ext
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s₁ s₂ : LowerSet α
t : LowerSet β
⊢ (s₁ ⊓ s₂) ×ˢ t = s₁ ×ˢ t ⊓ s₂ ×ˢ t

Tactic:
ext inter_prod

Premises used: LowerSet.ext, Set.inter_prod
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : LowerSet α
t₁ t₂ : LowerSet β
⊢ s ×ˢ (t₁ ⊓ t₂) = s ×ˢ t₁ ⊓ s ×ˢ t₂

Tactic:
ext prod_inter

Premises used: LowerSet.ext, Set.prod_inter
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s₁ s₂ : LowerSet α
t : LowerSet β
⊢ (s₁ ⊔ s₂) ×ˢ t = s₁ ×ˢ t ⊔ s₂ ×ˢ t

Tactic:
ext union_prod

Premises used: LowerSet.ext, Set.union_prod
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : LowerSet α
t₁ t₂ : LowerSet β
⊢ s ×ˢ (t₁ ⊔ t₂) = s ×ˢ t₁ ⊔ s ×ˢ t₂

Tactic:
ext prod_union

Premises used: LowerSet.ext, Set.prod_union
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s₁ s₂ : LowerSet α
t₁ t₂ : LowerSet β
⊢ s₁ ×ˢ t₁ ⊓ s₂ ×ˢ t₂ = (s₁ ⊓ s₂) ×ˢ (t₁ ⊓ t₂)

Tactic:
ext prod_inter_prod

Premises used: LowerSet.ext, Set.prod_inter_prod
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s₁ s₂ : LowerSet α
t₁ t₂ : LowerSet β
⊢ s₁ ≤ s₂ → t₁ ≤ t₂ → s₁ ×ˢ t₁ ≤ s₂ ×ˢ t₂

Tactic:
Set.prod_mono

Premises used: setOf, Set.prod, Set.prod_mono
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s₁ s₂ : LowerSet α
t : LowerSet β
⊢ s₁ ≤ s₂ → s₁ ×ˢ t ≤ s₂ ×ˢ t

Tactic:
Set.prod_mono_left

Premises used: setOf, Set.prod, Set.prod_mono_left
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : LowerSet α
t₁ t₂ : LowerSet β
⊢ t₁ ≤ t₂ → s ×ˢ t₁ ≤ s ×ˢ t₂

Tactic:
Set.prod_mono_right

Premises used: Set.prod_mono_right, setOf, Set.prod
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
inst : Preorder α
s₁ s₂ : LowerSet α
⊢ s₁ ×ˢ s₁ ≤ s₂ ×ˢ s₂ ↔ s₁ ≤ s₂

Tactic:
prod_self_subset_prod_self

Premises used: setOf, Set.prod, Set.prod_self_subset_prod_self
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
inst : Preorder α
s₁ s₂ : LowerSet α
⊢ s₁ ×ˢ s₁ < s₂ ×ˢ s₂ ↔ s₁ < s₂

Tactic:
prod_self_ssubset_prod_self

Premises used: setOf, Set.prod, Set.prod_self_ssubset_prod_self
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s₁ s₂ : LowerSet α
t₁ t₂ : LowerSet β
⊢ (↑s₁ : Set α) ⊆ (↑s₂ : Set α) ∧ (↑t₁ : Set β) ⊆ (↑t₂ : Set β) ∨ (↑s₁ : Set α) = ∅ ∨ (↑t₁ : Set β) = ∅ ↔
    s₁ ≤ s₂ ∧ t₁ ≤ t₂ ∨ s₁ = ⊥ ∨ t₁ = ⊥

Tactic:
simp
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : LowerSet α
t : LowerSet β
simp_rw : (↑(s ×ˢ t) : Set (α × β)) = (↑⊥ : Set (α × β)) ↔ (↑s : Set α) = (↑⊥ : Set α) ∨ (↑t : Set β) = (↑⊥ : Set β)
⊢ s ×ˢ t = ⊥ ↔ s = ⊥ ∨ t = ⊥

Tactic:
simp_rw [SetLike.ext'_iff]

Premises used: SetLike.ext'_iff
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : LowerSet α
t : LowerSet β
⊢ (↑(s ×ˢ t) : Set (α × β)) = (↑⊥ : Set (α × β)) ↔ (↑s : Set α) = (↑⊥ : Set α) ∨ (↑t : Set β) = (↑⊥ : Set β)

Tactic:
prod_eq_empty_iff

Premises used: setOf, Set.prod, Set.prod_eq_empty_iff
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : LowerSet α
t : LowerSet β
⊢ (↑(s ×ˢ t) : Set (α × β)) = (↑⊥ : Set (α × β)) ↔ (↑s : Set α) = (↑⊥ : Set α) ∨ (↑t : Set β) = (↑⊥ : Set β)

Tactic:
exact prod_eq_empty_iff

Premises used: Set.prod_eq_empty_iff
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s₁ s₂ : LowerSet α
t₁ t₂ : LowerSet β
simp_rw : s₁ ×ˢ t₁ ⊓ s₂ ×ˢ t₂ = ⊥ ↔ s₁ ⊓ s₂ = ⊥ ∨ t₁ ⊓ t₂ = ⊥
simp_rw₁ : (s₁ ⊓ s₂) ×ˢ (t₁ ⊓ t₂) = ⊥ ↔ s₁ ⊓ s₂ = ⊥ ∨ t₁ ⊓ t₂ = ⊥
⊢ Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂

Tactic:
simp_rw [disjoint_iff, prod_inf_prod, prod_eq_bot]

Premises used: disjoint_iff, LowerSet.prod_eq_bot, LowerSet.prod_inf_prod
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set α
t : Set β
a :
  ∀ (x : α × β),
    x ∈ (↑(upperClosure (s ×ˢ t)) : Set (α × β)) ↔
      x ∈ (↑(SProd.sprod (α := UpperSet α) (β := UpperSet β) (upperClosure s) (upperClosure t)) : Set (α × β))
⊢ upperClosure (s ×ˢ t) = SProd.sprod (α := UpperSet α) (β := UpperSet β) (upperClosure s) (upperClosure t)

Tactic:
ext
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set α
t : Set β
x : α × β
⊢ x ∈ (↑(upperClosure (s ×ˢ t)) : Set (α × β)) ↔
    x ∈ (↑(SProd.sprod (α := UpperSet α) (β := UpperSet β) (upperClosure s) (upperClosure t)) : Set (α × β))

Tactic:
simp [Prod.le_def, @and_and_and_comm _ (_ ∈ t)]

Premises used: and_and_and_comm, Prod.le_def
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set α
t : Set β
a :
  ∀ (x : α × β),
    x ∈ (↑(lowerClosure (s ×ˢ t)) : Set (α × β)) ↔
      x ∈ (↑(SProd.sprod (α := LowerSet α) (β := LowerSet β) (lowerClosure s) (lowerClosure t)) : Set (α × β))
⊢ lowerClosure (s ×ˢ t) = SProd.sprod (α := LowerSet α) (β := LowerSet β) (lowerClosure s) (lowerClosure t)

Tactic:
ext
-- Module: Mathlib.Order.UpperLower.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set α
t : Set β
x : α × β
⊢ x ∈ (↑(lowerClosure (s ×ˢ t)) : Set (α × β)) ↔
    x ∈ (↑(SProd.sprod (α := LowerSet α) (β := LowerSet β) (lowerClosure s) (lowerClosure t)) : Set (α × β))

Tactic:
simp [Prod.le_def, @and_and_and_comm _ (_ ∈ t)]

Premises used: and_and_and_comm, Prod.le_def
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
s : Set α
inst : LE α
⊢ (IsRelUpperSet s fun (x : α) ↦ True) ↔ IsUpperSet s

Tactic:
grind [IsUpperSet, IsRelUpperSet]

Premises used: IsUpperSet, IsRelUpperSet
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
s : Set α
inst : LE α
⊢ (IsRelLowerSet s fun (x : α) ↦ True) ↔ IsLowerSet s

Tactic:
grind [IsLowerSet, IsRelLowerSet]

Premises used: IsRelLowerSet, IsLowerSet
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
s : Set α
P : α → Prop
inst : LE α
hs : IsUpperSet s
⊢ IsRelUpperSet {x : α | x ∈ s ∧ P x} P

Tactic:
fun _ h => ⟨h.2, fun _ ht hp => ⟨hs ht h.1, hp⟩⟩

Premises used: IsRelUpperSet, And.right, And.left, And.intro
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
s : Set α
P : α → Prop
inst : LE α
hs : IsLowerSet s
⊢ IsRelLowerSet {x : α | x ∈ s ∧ P x} P

Tactic:
fun _ h => ⟨h.2, fun _ ht hp => ⟨hs ht h.1, hp⟩⟩

Premises used: IsRelLowerSet, And.right, And.left, And.intro
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
s t : Set α
P : α → Prop
inst : LE α
ht : IsRelLowerSet t P
hs : IsLowerSet s
hst : s ⊆ t
⊢ IsRelLowerSet s P

Tactic:
fun _ h => ⟨(ht (hst h)).1, fun _ ht _ => hs ht h⟩

Premises used: IsRelLowerSet, And.left, And.intro
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
s t : Set α
P : α → Prop
inst : LE α
ht : IsRelUpperSet t P
hs : IsUpperSet s
hst : s ⊆ t
⊢ IsRelUpperSet s P

Tactic:
fun _ h => ⟨(ht (hst h)).1, fun _ ht _ => hs ht h⟩

Premises used: IsRelUpperSet, And.left, And.intro
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
s : Set α
a : α
P : α → Prop
inst : LE α
hs : IsRelUpperSet s P
h : a ∈ s
⊢ P a

Tactic:
(hs h).1

Premises used: And.left
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
s : Set α
a : α
P : α → Prop
inst : LE α
hs : IsRelLowerSet s P
h : a ∈ s
⊢ P a

Tactic:
(hs h).1

Premises used: And.left
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
s : Set α
a b : α
P : α → Prop
inst : LE α
hs : IsRelUpperSet s P
h : a ∈ s
h₁ : a ≤ b
h₂ : P b
⊢ b ∈ s

Tactic:
(hs h).2 h₁ h₂

Premises used: And.right
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
s : Set α
a b : α
P : α → Prop
inst : LE α
hs : IsRelLowerSet s P
h : a ∈ s
h₁ : b ≤ a
h₂ : P b
⊢ b ∈ s

Tactic:
(hs h).2 h₁ h₂

Premises used: And.right
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
P : α → Prop
inst : LE α
⊢ IsRelUpperSet ∅ P

Tactic:
fun _ ↦ False.elim

Premises used: Set.Mem, False.elim, IsRelUpperSet
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
P : α → Prop
inst : LE α
⊢ IsRelLowerSet ∅ P

Tactic:
fun _ ↦ False.elim

Premises used: Set.Mem, IsRelLowerSet, False.elim
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
s : Set α
inst : LE α
⊢ IsRelUpperSet s fun (x : α) ↦ x ∈ s

Tactic:
fun _ b ↦ ⟨b, fun _ _ ↦ id⟩

Premises used: id, IsRelUpperSet, And.intro
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
s : Set α
inst : LE α
⊢ IsRelLowerSet s fun (x : α) ↦ x ∈ s

Tactic:
fun _ b ↦ ⟨b, fun _ _ ↦ id⟩

Premises used: IsRelLowerSet, id, And.intro
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
s t : Set α
P : α → Prop
inst : LE α
hs : IsRelUpperSet s P
ht : IsRelUpperSet t P
b : α
h : b ∈ s
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ s ∪ t

Tactic:
⟨(hs h).1, fun _ x y ↦ .inl ((hs h).2 x y)⟩

Premises used: And.right, And.left, And.intro, Or.inl
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
s t : Set α
P : α → Prop
inst : LE α
hs : IsRelUpperSet s P
ht : IsRelUpperSet t P
b : α
h : b ∈ s
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ s ∪ t

Tactic:
exact ⟨(hs h).1, fun _ x y ↦ .inl ((hs h).2 x y)⟩