awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s t₁ t₂ : Set α
⊢ s ⊻ (t₁ ∩ t₂) ⊆ s ⊻ t₁ ∩ s ⊻ t₂

Tactic:
image2_inter_subset_right

Premises used: Set.image2_inter_subset_right
-- Module: Mathlib.Data.Set.Sups
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
inst_2 : FunLike F α β
inst_3 : SupHomClass F α β
f : F
s t : Set α
⊢ Eq.{u_3 + 1} (α := Set β) ((⇑f : (a : α) → β) '' (s ⊻ t)) ((⇑f : (a : α) → β) '' s ⊻ (⇑f : (a : α) → β) '' t)

Tactic:
image_image2_distrib <| map_sup f

Premises used: Set.image_image2_distrib, SupHomClass.map_sup
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s : Set α
⊢ s ⊆ s ⊻ s

Tactic:
fun _a ha ↦ mem_sups.2 ⟨_, ha, _, ha, sup_idem _⟩

Premises used: Iff.mpr, Set.mem_sups, sup_idem, Set.Subset, And.intro, Exists.intro
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s : Set α
⊢ s ⊻ s ⊆ s ↔ SupClosed s

Tactic:
sups_subset_iff

Premises used: SupClosed, Set.sups_subset_iff
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s : Set α
⊢ s ⊻ s = s ↔ SupClosed s

Tactic:
subset_sups_self.le.ge_iff_eq'.symm.trans sups_subset_self

Premises used: Set.subset_sups_self, HasSubset.Subset.le, LE.le.ge_iff_eq', Iff.trans, Set.sups_subset_self, Iff.symm
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s t : Set α
a : α
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) {b : α | b ∈ s ⊻ t ∧ b ≤ a} x ↔
      Membership.mem (γ := Set α) ({b : α | b ∈ s ∧ b ≤ a} ⊻ {b : α | b ∈ t ∧ b ≤ a}) x
⊢ Eq.{u_2 + 1} (α := Set α) {b : α | b ∈ s ⊻ t ∧ b ≤ a} ({b : α | b ∈ s ∧ b ≤ a} ⊻ {b : α | b ∈ t ∧ b ≤ a})

Tactic:
ext
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s t : Set α
a x : α
⊢ Membership.mem (γ := Set α) {b : α | b ∈ s ⊻ t ∧ b ≤ a} x ↔
    Membership.mem (γ := Set α) ({b : α | b ∈ s ∧ b ≤ a} ⊻ {b : α | b ∈ t ∧ b ≤ a}) x

Tactic:
aesop
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s t : Set α
⊢ ⋃ a ∈ s, (fun (x1 x2 : α) ↦ x1 ⊔ x2) a '' t = s ⊻ t

Tactic:
iUnion_image_left _

Premises used: Set.iUnion_image_left
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s t : Set α
⊢ ⋃ b ∈ t, (fun (x : α) ↦ x ⊔ b) '' s = s ⊻ t

Tactic:
iUnion_image_right _

Premises used: Set.iUnion_image_right
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s t : Set α
⊢ image2 (fun (x1 x2 : α) ↦ x1 ⊔ x2) s t = s ⊻ t

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s t u : Set α
⊢ s ⊻ t ⊻ u = s ⊻ (t ⊻ u)

Tactic:
image2_assoc sup_assoc

Premises used: Set.image2_assoc, sup_assoc
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s t : Set α
⊢ s ⊻ t = t ⊻ s

Tactic:
image2_comm sup_comm

Premises used: Set.image2_comm, sup_comm
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s t u : Set α
⊢ s ⊻ (t ⊻ u) = t ⊻ (s ⊻ u)

Tactic:
image2_left_comm sup_left_comm

Premises used: Set.image2_left_comm, sup_left_comm
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s t u : Set α
⊢ s ⊻ t ⊻ u = s ⊻ u ⊻ t

Tactic:
image2_right_comm sup_right_comm

Premises used: Set.image2_right_comm, sup_right_comm
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s t u v : Set α
⊢ s ⊻ t ⊻ (u ⊻ v) = s ⊻ u ⊻ (t ⊻ v)

Tactic:
image2_image2_image2_comm sup_sup_sup_comm

Premises used: sup_sup_sup_comm, Set.image2_image2_image2_comm
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s t : Set α
c : α
⊢ c ∈ s ⊼ t ↔ ∃ a ∈ s, ∃ b ∈ t, a ⊓ b = c

Tactic:
simp [(· ⊼ ·)]

Premises used: HasInfs.infs
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s t : Set α
a b : α
⊢ a ∈ s → b ∈ t → a ⊓ b ∈ s ⊼ t

Tactic:
mem_image2_of_mem

Premises used: Set.Mem, Set.mem_image2_of_mem
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s₁ s₂ t₁ t₂ : Set α
⊢ s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ ⊼ t₁ ⊆ s₂ ⊼ t₂

Tactic:
image2_subset

Premises used: Set.image2_subset
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s t₁ t₂ : Set α
⊢ t₁ ⊆ t₂ → s ⊼ t₁ ⊆ s ⊼ t₂

Tactic:
image2_subset_left

Premises used: Set.image2_subset_left
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s₁ s₂ t : Set α
⊢ s₁ ⊆ s₂ → s₁ ⊼ t ⊆ s₂ ⊼ t

Tactic:
image2_subset_right

Premises used: Set.image2_subset_right
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s t : Set α
b : α
⊢ b ∈ t → (fun (a : α) ↦ a ⊓ b) '' s ⊆ s ⊼ t

Tactic:
image_subset_image2_left

Premises used: Set.image_subset_image2_left
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s t : Set α
a : α
⊢ a ∈ s → (fun (x : α) ↦ a ⊓ x) '' t ⊆ s ⊼ t

Tactic:
image_subset_image2_right

Premises used: Set.image_subset_image2_right
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s t : Set α
p : α → Prop
⊢ (∀ c ∈ s ⊼ t, p c) ↔ ∀ a ∈ s, ∀ b ∈ t, p (a ⊓ b)

Tactic:
forall_mem_image2

Premises used: Set.forall_mem_image2, Set.Mem
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s t u : Set α
⊢ s ⊼ t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a ⊓ b ∈ u

Tactic:
image2_subset_iff

Premises used: Set.image2_subset_iff
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s t : Set α
⊢ (s ⊼ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Tactic:
image2_nonempty_iff

Premises used: Set.image2_nonempty_iff
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s t : Set α
⊢ s.Nonempty → t.Nonempty → (s ⊼ t).Nonempty

Tactic:
Nonempty.image2

Premises used: Set.Nonempty.image2
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s t : Set α
⊢ (s ⊼ t).Nonempty → s.Nonempty

Tactic:
Nonempty.of_image2_left

Premises used: Set.Nonempty.of_image2_left
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s t : Set α
⊢ (s ⊼ t).Nonempty → t.Nonempty

Tactic:
Nonempty.of_image2_right

Premises used: Set.Nonempty.of_image2_right
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
t : Set α
⊢ ∅ ⊼ t = ∅

Tactic:
image2_empty_left

Premises used: Set.image2_empty_left
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s : Set α
⊢ s ⊼ ∅ = ∅

Tactic:
image2_empty_right

Premises used: Set.image2_empty_right
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s t : Set α
⊢ s ⊼ t = ∅ ↔ s = ∅ ∨ t = ∅

Tactic:
image2_eq_empty_iff

Premises used: Set.image2_eq_empty_iff
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
t : Set α
a : α
⊢ {a} ⊼ t = (fun (b : α) ↦ a ⊓ b) '' t

Tactic:
image2_singleton_left

Premises used: Set.image2_singleton_left
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s : Set α
b : α
⊢ s ⊼ {b} = (fun (a : α) ↦ a ⊓ b) '' s

Tactic:
image2_singleton_right

Premises used: Set.image2_singleton_right
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
a b : α
⊢ Eq (α := Set α) ({a} ⊼ {b}) {a ⊓ b}

Tactic:
image2_singleton

Premises used: Set.image2_singleton
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s₁ s₂ t : Set α
⊢ (s₁ ∪ s₂) ⊼ t = s₁ ⊼ t ∪ s₂ ⊼ t

Tactic:
image2_union_left

Premises used: Set.image2_union_left
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s t₁ t₂ : Set α
⊢ s ⊼ (t₁ ∪ t₂) = s ⊼ t₁ ∪ s ⊼ t₂

Tactic:
image2_union_right

Premises used: Set.image2_union_right
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s₁ s₂ t : Set α
⊢ (s₁ ∩ s₂) ⊼ t ⊆ s₁ ⊼ t ∩ s₂ ⊼ t

Tactic:
image2_inter_subset_left

Premises used: Set.image2_inter_subset_left
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s t₁ t₂ : Set α
⊢ s ⊼ (t₁ ∩ t₂) ⊆ s ⊼ t₁ ∩ s ⊼ t₂

Tactic:
image2_inter_subset_right

Premises used: Set.image2_inter_subset_right
-- Module: Mathlib.Data.Set.Sups
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
inst_2 : FunLike F α β
inst_3 : InfHomClass F α β
f : F
s t : Set α
⊢ Eq.{u_3 + 1} (α := Set β) ((⇑f : (a : α) → β) '' (s ⊼ t)) ((⇑f : (a : α) → β) '' s ⊼ (⇑f : (a : α) → β) '' t)

Tactic:
image_image2_distrib <| map_inf f

Premises used: InfHomClass.map_inf, Set.image_image2_distrib
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s : Set α
⊢ s ⊆ s ⊼ s

Tactic:
fun _a ha ↦ mem_infs.2 ⟨_, ha, _, ha, inf_idem _⟩

Premises used: Iff.mpr, Set.mem_infs, Set.Subset, And.intro, Exists.intro, inf_idem
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s : Set α
⊢ s ⊼ s ⊆ s ↔ InfClosed s

Tactic:
infs_subset_iff

Premises used: Set.infs_subset_iff, InfClosed
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s : Set α
⊢ s ⊼ s = s ↔ InfClosed s

Tactic:
subset_infs_self.le.ge_iff_eq'.symm.trans infs_self_subset

Premises used: Set.subset_infs_self, Set.infs_self_subset, HasSubset.Subset.le, LE.le.ge_iff_eq', Iff.trans, Iff.symm
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s t : Set α
a : α
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) {b : α | b ∈ s ⊼ t ∧ a ≤ b} x ↔
      Membership.mem (γ := Set α) ({b : α | b ∈ s ∧ a ≤ b} ⊼ {b : α | b ∈ t ∧ a ≤ b}) x
⊢ Eq.{u_2 + 1} (α := Set α) {b : α | b ∈ s ⊼ t ∧ a ≤ b} ({b : α | b ∈ s ∧ a ≤ b} ⊼ {b : α | b ∈ t ∧ a ≤ b})

Tactic:
ext
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s t : Set α
a x : α
⊢ Membership.mem (γ := Set α) {b : α | b ∈ s ⊼ t ∧ a ≤ b} x ↔
    Membership.mem (γ := Set α) ({b : α | b ∈ s ∧ a ≤ b} ⊼ {b : α | b ∈ t ∧ a ≤ b}) x

Tactic:
aesop
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s t : Set α
⊢ ⋃ a ∈ s, (fun (x : α) ↦ a ⊓ x) '' t = s ⊼ t

Tactic:
iUnion_image_left _

Premises used: Set.iUnion_image_left
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s t : Set α
⊢ ⋃ b ∈ t, (fun (x : α) ↦ x ⊓ b) '' s = s ⊼ t

Tactic:
iUnion_image_right _

Premises used: Set.iUnion_image_right
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s t : Set α
⊢ image2 (fun (x x_1 : α) ↦ x ⊓ x_1) s t = s ⊼ t

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s t u : Set α
⊢ s ⊼ t ⊼ u = s ⊼ (t ⊼ u)

Tactic:
image2_assoc inf_assoc

Premises used: Set.image2_assoc, inf_assoc
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s t : Set α
⊢ s ⊼ t = t ⊼ s

Tactic:
image2_comm inf_comm

Premises used: inf_comm, Set.image2_comm
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s t u : Set α
⊢ s ⊼ (t ⊼ u) = t ⊼ (s ⊼ u)

Tactic:
image2_left_comm inf_left_comm

Premises used: Set.image2_left_comm, inf_left_comm
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s t u : Set α
⊢ s ⊼ t ⊼ u = s ⊼ u ⊼ t

Tactic:
image2_right_comm inf_right_comm

Premises used: Set.image2_right_comm, inf_right_comm
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s t u v : Set α
⊢ s ⊼ t ⊼ (u ⊼ v) = s ⊼ u ⊼ (t ⊼ v)

Tactic:
image2_image2_image2_comm inf_inf_inf_comm

Premises used: inf_inf_inf_comm, Set.image2_image2_image2_comm
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : DistribLattice α
s t u : Set α
⊢ s ⊻ t ⊼ u ⊆ (s ⊻ t) ⊼ (s ⊻ u)

Tactic:
image2_distrib_subset_left sup_inf_left

Premises used: Set.image2_distrib_subset_left, sup_inf_left
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : DistribLattice α
s t u : Set α
⊢ t ⊼ u ⊻ s ⊆ (t ⊻ s) ⊼ (u ⊻ s)

Tactic:
image2_distrib_subset_right sup_inf_right

Premises used: Set.image2_distrib_subset_right, sup_inf_right
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : DistribLattice α
s t u : Set α
⊢ s ⊼ (t ⊻ u) ⊆ s ⊼ t ⊻ s ⊼ u

Tactic:
image2_distrib_subset_left inf_sup_left

Premises used: Set.image2_distrib_subset_left, inf_sup_left
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : DistribLattice α
s t u : Set α
⊢ (t ⊻ u) ⊼ s ⊆ t ⊼ s ⊻ u ⊼ s

Tactic:
image2_distrib_subset_right inf_sup_right

Premises used: Set.image2_distrib_subset_right, inf_sup_right
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s t : Set α
a : ∀ (a : α), a ∈ (↑(upperClosure (s ⊻ t)) : Set α) ↔ a ∈ (↑(upperClosure s ⊔ upperClosure t) : Set α)
⊢ Eq (α := UpperSet α) (upperClosure (s ⊻ t)) (upperClosure s ⊔ upperClosure t)

Tactic:
ext a
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s t : Set α
a : α
a₁ : (∃ (a_1 : α), (∃ a ∈ s, ∃ b ∈ t, a ⊔ b = a_1) ∧ a_1 ≤ a) → (∃ a_2 ∈ s, a_2 ≤ a) ∧ ∃ a_2 ∈ t, a_2 ≤ a
a₂ : ((∃ a_1 ∈ s, a_1 ≤ a) ∧ ∃ a_1 ∈ t, a_1 ≤ a) → ∃ (a_2 : α), (∃ a ∈ s, ∃ b ∈ t, a ⊔ b = a_2) ∧ a_2 ≤ a
⊢ (∃ (a_1 : α), (∃ a ∈ s, ∃ b ∈ t, a ⊔ b = a_1) ∧ a_1 ≤ a) ↔ (∃ a_1 ∈ s, a_1 ≤ a) ∧ ∃ a_1 ∈ t, a_1 ≤ a

Tactic:
constructor
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s t : Set α
a b : α
hb : b ∈ s
c : α
hc : c ∈ t
ha : b ⊔ c ≤ a
⊢ (∃ a_1 ∈ s, a_1 ≤ a) ∧ ∃ a_1 ∈ t, a_1 ≤ a

Tactic:
⟨⟨b, hb, le_sup_left.trans ha⟩, c, hc, le_sup_right.trans ha⟩

Premises used: le_sup_left, le_sup_right, And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s t : Set α
a b : α
hb : b ∈ s
c : α
hc : c ∈ t
ha : b ⊔ c ≤ a
⊢ (∃ a_1 ∈ s, a_1 ≤ a) ∧ ∃ a_1 ∈ t, a_1 ≤ a

Tactic:
exact ⟨⟨b, hb, le_sup_left.trans ha⟩, c, hc, le_sup_right.trans ha⟩
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s t : Set α
a b : α
hb : b ∈ s
hab : b ≤ a
c : α
hc : c ∈ t
hac : c ≤ a
⊢ ∃ (a_1 : α), (∃ a ∈ s, ∃ b ∈ t, a ⊔ b = a_1) ∧ a_1 ≤ a

Tactic:
⟨_, ⟨b, hb, c, hc, rfl⟩, sup_le hab hac⟩

Premises used: And.intro, Exists.intro, sup_le, rfl
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s t : Set α
a b : α
hb : b ∈ s
hab : b ≤ a
c : α
hc : c ∈ t
hac : c ≤ a
⊢ ∃ (a_1 : α), (∃ a ∈ s, ∃ b ∈ t, a ⊔ b = a_1) ∧ a_1 ≤ a

Tactic:
exact ⟨_, ⟨b, hb, c, hc, rfl⟩, sup_le hab hac⟩
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s t : Set α
a : ∀ (a : α), a ∈ (↑(lowerClosure (s ⊼ t)) : Set α) ↔ a ∈ (↑(lowerClosure s ⊓ lowerClosure t) : Set α)
⊢ Eq (α := LowerSet α) (lowerClosure (s ⊼ t)) (lowerClosure s ⊓ lowerClosure t)

Tactic:
ext a
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s t : Set α
a : α
a₁ :
  (∃ (a_1 : α), (∃ a ∈ s, ∃ b ∈ t, a ⊓ b = a_1) ∧ a ≤ a_1) →
    Membership.mem (γ := LowerSet α) (lowerClosure s ⊓ lowerClosure t) a
a₂ :
  Membership.mem (γ := LowerSet α) (lowerClosure s ⊓ lowerClosure t) a →
    ∃ (a_2 : α), (∃ a ∈ s, ∃ b ∈ t, a ⊓ b = a_2) ∧ a ≤ a_2
⊢ (∃ (a_1 : α), (∃ a ∈ s, ∃ b ∈ t, a ⊓ b = a_1) ∧ a ≤ a_1) ↔
    Membership.mem (γ := LowerSet α) (lowerClosure s ⊓ lowerClosure t) a

Tactic:
constructor
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s t : Set α
a b : α
hb : b ∈ s
c : α
hc : c ∈ t
ha : a ≤ b ⊓ c
⊢ Membership.mem (γ := LowerSet α) (lowerClosure s ⊓ lowerClosure t) a

Tactic:
⟨⟨b, hb, ha.trans inf_le_left⟩, c, hc, ha.trans inf_le_right⟩

Premises used: Set.Mem, setOf, inf_le_right, Set.inter, And.intro, Exists.intro, inf_le_left, LE.le.trans
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s t : Set α
a b : α
hb : b ∈ s
c : α
hc : c ∈ t
ha : a ≤ b ⊓ c
⊢ Membership.mem (γ := LowerSet α) (lowerClosure s ⊓ lowerClosure t) a

Tactic:
exact ⟨⟨b, hb, ha.trans inf_le_left⟩, c, hc, ha.trans inf_le_right⟩
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s t : Set α
a b : α
hb : b ∈ s
hab : a ≤ b
c : α
hc : c ∈ t
hac : a ≤ c
⊢ ∃ (a_1 : α), (∃ a ∈ s, ∃ b ∈ t, a ⊓ b = a_1) ∧ a ≤ a_1

Tactic:
⟨_, ⟨b, hb, c, hc, rfl⟩, le_inf hab hac⟩

Premises used: le_inf, And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeInf α
s t : Set α
a b : α
hb : b ∈ s
hab : a ≤ b
c : α
hc : c ∈ t
hac : a ≤ c
⊢ ∃ (a_1 : α), (∃ a ∈ s, ∃ b ∈ t, a ⊓ b = a_1) ∧ a ≤ a_1

Tactic:
exact ⟨_, ⟨b, hb, c, hc, rfl⟩, le_inf hab hac⟩
-- Module: Mathlib.Data.Set.SymmDiff
Goal:
α : Type u
a : α
s t : Set α
⊢ a ∈ s ∆ t ↔ a ∈ s ∧ ¬a ∈ t ∨ a ∈ t ∧ ¬a ∈ s

Tactic:
Iff.rfl

Premises used: Set.union, Set.Mem, Set.diff, Iff.rfl, setOf, symmDiff
-- Module: Mathlib.Data.Set.SymmDiff
Goal:
α : Type u
s t : Set α
⊢ s ∆ t = s \ t ∪ t \ s

Tactic:
rfl

Premises used: symmDiff, rfl
-- Module: Mathlib.Data.Set.SymmDiff
Goal:
α : Type u
s t : Set α
⊢ s ∆ t ⊆ s ∪ t

Tactic:
@symmDiff_le_sup (Set α) _ _ _

Premises used: symmDiff_le_sup
-- Module: Mathlib.Data.Set.SymmDiff
Goal:
α : Type u
s t : Set α
⊢ s ∆ t = ∅ ↔ s = t

Tactic:
symmDiff_eq_bot

Premises used: symmDiff_eq_bot
-- Module: Mathlib.Data.Set.SymmDiff
Goal:
α : Type u
s t : Set α
⊢ (s ∆ t).Nonempty ↔ s ≠ t

Tactic:
nonempty_iff_ne_empty.trans symmDiff_eq_empty.not

Premises used: Iff.not, Set.nonempty_iff_ne_empty, Iff.trans, Set.symmDiff_eq_empty
-- Module: Mathlib.Data.Set.SymmDiff
Goal:
α : Type u
s t u : Set α
⊢ s ∩ t ∆ u = (s ∩ t) ∆ (s ∩ u)

Tactic:
inf_symmDiff_distrib_left _ _ _

Premises used: inf_symmDiff_distrib_left
-- Module: Mathlib.Data.Set.SymmDiff
Goal:
α : Type u
s t u : Set α
⊢ s ∆ t ∩ u = (s ∩ u) ∆ (t ∩ u)

Tactic:
inf_symmDiff_distrib_right _ _ _

Premises used: inf_symmDiff_distrib_right
-- Module: Mathlib.Data.Set.SymmDiff
Goal:
α : Type u
s t u : Set α
h : Disjoint s t
⊢ u ⊆ s ∆ u ∪ t ∆ u

Tactic:
h.le_symmDiff_sup_symmDiff_left

Premises used: Disjoint.le_symmDiff_sup_symmDiff_left
-- Module: Mathlib.Data.Set.SymmDiff
Goal:
α : Type u
s t u : Set α
h : Disjoint t u
⊢ s ⊆ s ∆ t ∪ s ∆ u

Tactic:
h.le_symmDiff_sup_symmDiff_right

Premises used: Disjoint.le_symmDiff_sup_symmDiff_right
-- Module: Mathlib.Data.Set.SymmDiff
Goal:
α : Type u
s t u : Set α
⊢ (s ∪ t) ∆ u ⊆ s ∆ u ∪ t ∆ u

Tactic:
grind
-- Module: Mathlib.Data.Set.SymmDiff
Goal:
α : Type u
s t u : Set α
⊢ s ∆ (t ∪ u) ⊆ s ∆ t ∪ s ∆ u

Tactic:
grind
-- Module: Mathlib.Data.Set.SymmDiff
Goal:
α : Type u
s t u v : Set α
⊢ (s ∪ t) ∆ (u ∪ v) ⊆ s ∆ u ∪ t ∆ v

Tactic:
grind
-- Module: Mathlib.Data.Set.UnionLift
Goal:
α : Type u_1
ι : Sort u_3
β : Sort u_2
S : ι → Set α
f : (i : ι) → (↑(S i) : Type u_1) → β
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hxi) = f j (Subtype.mk (p := fun (x : α) ↦ x ∈ S j) x hxj)
T : Set α
hT : T ⊆ iUnion S
i : ι
x : (↑(S i) : Type u_1)
hx : (↑x : α) ∈ T
⊢ iUnionLift S f hf T hT (Subtype.mk (p := fun (x : α) ↦ x ∈ T) (↑x : α) hx) = f i x

Tactic:
hf _ i x _ _

Premises used: Subtype.val, Set.iUnionLift
-- Module: Mathlib.Data.Set.UnionLift
Goal:
α : Type u_1
ι : Sort u_3
β : Sort u_2
S : ι → Set α
f : (i : ι) → (↑(S i) : Type u_1) → β
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hxi) = f j (Subtype.mk (p := fun (x : α) ↦ x ∈ S j) x hxj)
T : Set α
hT : T ⊆ iUnion S
i : ι
x : (↑(S i) : Type u_1)
h : S i ⊆ T
⊢ iUnionLift S f hf T hT (inclusion (s := S i) (t := T) h x) = f i x

Tactic:
iUnionLift_mk x _

Premises used: Set.iUnionLift_mk
-- Module: Mathlib.Data.Set.UnionLift
Goal:
α : Type u_1
ι : Sort u_3
β : Sort u_2
S : ι → Set α
f : (i : ι) → (↑(S i) : Type u_1) → β
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hxi) = f j (Subtype.mk (p := fun (x : α) ↦ x ∈ S j) x hxj)
T : Set α
hT : T ⊆ iUnion S
x : (↑T : Type u_1)
i : ι
hx : (↑x : α) ∈ S i
obtain :
  ∀ (x : α) (hx : x ∈ T) (hx_1 : (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ T) x hx) : α) ∈ S i),
    iUnionLift S f hf T hT (Subtype.mk (p := fun (x : α) ↦ x ∈ T) x hx) =
      f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ T) x hx) : α) hx_1)
⊢ iUnionLift S f hf T hT x = f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑x : α) hx)

Tactic:
obtain ⟨x, hx⟩ := x
-- Module: Mathlib.Data.Set.UnionLift
Goal:
α : Type u_1
ι : Sort u_3
β : Sort u_2
S : ι → Set α
f : (i : ι) → (↑(S i) : Type u_1) → β
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hxi) = f j (Subtype.mk (p := fun (x : α) ↦ x ∈ S j) x hxj)
T : Set α
hT : T ⊆ iUnion S
i : ι
x : α
hx_1 : x ∈ T
hx : (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ T) x hx_1) : α) ∈ S i
⊢ iUnionLift S f hf T hT (Subtype.mk (p := fun (x : α) ↦ x ∈ T) x hx_1) =
    f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ T) x hx_1) : α) hx)

Tactic:
hf _ _ _ _ _

Premises used: Set.iUnionLift
-- Module: Mathlib.Data.Set.UnionLift
Goal:
α : Type u_1
ι : Sort u_3
β : Sort u_2
S : ι → Set α
f : (i : ι) → (↑(S i) : Type u_1) → β
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hxi) = f j (Subtype.mk (p := fun (x : α) ↦ x ∈ S j) x hxj)
T : Set α
hT : T ⊆ iUnion S
i : ι
x : α
hx_1 : x ∈ T
hx : (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ T) x hx_1) : α) ∈ S i
⊢ iUnionLift S f hf T hT (Subtype.mk (p := fun (x : α) ↦ x ∈ T) x hx_1) =
    f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ T) x hx_1) : α) hx)

Tactic:
exact hf _ _ _ _ _
-- Module: Mathlib.Data.Set.UnionLift
Goal:
α : Type u_1
ι : Sort u_3
β : Type u_2
S : ι → Set α
f : (i : ι) → (↑(S i) : Type u_1) → β
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hxi) = f j (Subtype.mk (p := fun (x : α) ↦ x ∈ S j) x hxj)
T : Set α
hT : T ⊆ iUnion S
t : Set β
h :
  ∀ (x : (↑T : Type u_1)),
    x ∈ iUnionLift S f hf T hT ⁻¹' t ↔
      x ∈ inclusion (s := T) (t := iUnion S) hT ⁻¹' ⋃ (i : ι), inclusion (s := S i) (t := iUnion S) ⋯ '' f i ⁻¹' t
⊢ iUnionLift S f hf T hT ⁻¹' t =
    inclusion (s := T) (t := iUnion S) hT ⁻¹' ⋃ (i : ι), inclusion (s := S i) (t := iUnion S) ⋯ '' f i ⁻¹' t

Tactic:
ext x
-- Module: Mathlib.Data.Set.UnionLift
Goal:
α : Type u_1
ι : Sort u_3
β : Type u_2
S : ι → Set α
f : (i : ι) → (↑(S i) : Type u_1) → β
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hxi) = f j (Subtype.mk (p := fun (x : α) ↦ x ∈ S j) x hxj)
T : Set α
hT : T ⊆ iUnion S
t : Set β
x : (↑T : Type u_1)
h :
  iUnionLift S f hf T hT x ∈ t ↔
    ∃ (i : ι) (x_1 : (↑(S i) : Type u_1)),
      f i x_1 ∈ t ∧ inclusion (s := S i) (t := iUnion S) ⋯ x_1 = inclusion (s := T) (t := iUnion S) hT x
⊢ x ∈ iUnionLift S f hf T hT ⁻¹' t ↔
    x ∈ inclusion (s := T) (t := iUnion S) hT ⁻¹' ⋃ (i : ι), inclusion (s := S i) (t := iUnion S) ⋯ '' f i ⁻¹' t

Tactic:
simp only [mem_preimage, mem_iUnion, mem_image]

Premises used: Set.mem_iUnion, Set.mem_image, Set.mem_preimage
-- Module: Mathlib.Data.Set.UnionLift
Goal:
α : Type u_1
ι : Sort u_3
β : Type u_2
S : ι → Set α
f : (i : ι) → (↑(S i) : Type u_1) → β
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hxi) = f j (Subtype.mk (p := fun (x : α) ↦ x ∈ S j) x hxj)
T : Set α
hT : T ⊆ iUnion S
t : Set β
x : (↑T : Type u_1)
h :
  iUnionLift S f hf T hT x ∈ t →
    ∃ (i : ι) (x_1 : (↑(S i) : Type u_1)),
      f i x_1 ∈ t ∧ inclusion (s := S i) (t := iUnion S) ⋯ x_1 = inclusion (s := T) (t := iUnion S) hT x
h₁ :
  (∃ (i : ι) (x_1 : (↑(S i) : Type u_1)),
      f i x_1 ∈ t ∧ inclusion (s := S i) (t := iUnion S) ⋯ x_1 = inclusion (s := T) (t := iUnion S) hT x) →
    iUnionLift S f hf T hT x ∈ t
⊢ iUnionLift S f hf T hT x ∈ t ↔
    ∃ (i : ι) (x_1 : (↑(S i) : Type u_1)),
      f i x_1 ∈ t ∧ inclusion (s := S i) (t := iUnion S) ⋯ x_1 = inclusion (s := T) (t := iUnion S) hT x

Tactic:
constructor