awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋃ (x : α), ⋃ (_ : Membership.mem (γ := Set α) univ x), s x) (⋃ (x : α), s x)

Tactic:
iSup_univ

Premises used: iSup_univ, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
a : α
s : α → Set β
⊢ ⋃ (x : α), ⋃ (_ : Membership.mem (γ := Set α) {a} x), s x = s a

Tactic:
iSup_singleton

Premises used: iSup_singleton, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s : Set α
⊢ ∀ (x : α), Membership.mem (γ := Set α) (⋃ x ∈ s, {x}) x ↔ x ∈ s

Tactic:
simp
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
s t : Set α
u : α → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋃ x ∈ s ∪ t, u x) ((⋃ x ∈ s, u x) ∪ ⋃ x ∈ t, u x)

Tactic:
iSup_union

Premises used: Set.iUnion, iSup_union
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_12
β : Type u_13
s : Set α
f : (↑s : Type u_12) → Set β
⊢ Eq.{u_13 + 1} (α := Set β) (⋃ (i : (↑s : Type u_12)), f i)
    (⋃ (i : α), ⋃ (h : i ∈ s), f (Subtype.mk (p := fun (x : α) ↦ x ∈ s) i h))

Tactic:
iUnion_subtype _ _

Premises used: Set.iUnion_subtype
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_12
β : Type u_13
s : Set α
f : (↑s : Type u_12) → Set β
⊢ Eq.{u_13 + 1} (α := Set β) (⋂ (i : (↑s : Type u_12)), f i)
    (⋂ (i : α), ⋂ (h : i ∈ s), f (Subtype.mk (p := fun (x : α) ↦ x ∈ s) i h))

Tactic:
iInter_subtype _ _

Premises used: Set.iInter_subtype
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
a : α
s : Set α
t : α → Set β
⊢ ⋃ x ∈ insert a s, t x = t a ∪ ⋃ x ∈ s, t x

Tactic:
simp
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
a b : α
s : α → Set β
⊢ ⋃ (x : α), ⋃ (_ : Membership.mem (γ := Set α) {a, b} x), s x = s a ∪ s b

Tactic:
simp
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : Set α
t : (i : ι) → κ i → Set α
⊢ s ∩ ⋃ (i : ι), ⋃ (j : κ i), t i j = ⋃ (i : ι), ⋃ (j : κ i), s ∩ t i j

Tactic:
simp only [inter_iUnion]

Premises used: Set.inter_iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
t : Set α
⊢ (⋃ (i : ι), ⋃ (j : κ i), s i j) ∩ t = ⋃ (i : ι), ⋃ (j : κ i), s i j ∩ t

Tactic:
simp_rw [iUnion_inter]

Premises used: Set.iUnion_inter
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : Set α
t : (i : ι) → κ i → Set α
⊢ s ∪ ⋂ (i : ι), ⋂ (j : κ i), t i j = ⋂ (i : ι), ⋂ (j : κ i), s ∪ t i j

Tactic:
simp_rw [union_iInter]

Premises used: Set.union_iInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
t : Set α
⊢ (⋂ (i : ι), ⋂ (j : κ i), s i j) ∪ t = ⋂ (i : ι), ⋂ (j : κ i), s i j ∪ t

Tactic:
simp_rw [iInter_union]

Premises used: Set.iInter_union
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
x : α
t : Set α
S : Set (Set α)
hx : x ∈ t
ht : t ∈ S
⊢ x ∈ ⋃₀ S

Tactic:
⟨t, ht, hx⟩

Premises used: Set.Mem, setOf, Set.sUnion, And.intro, Exists.intro
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
x : α
t : Set α
S : Set (Set α)
hx : x ∉ ⋃₀ S
ht : t ∈ S
⊢ x ∉ t

Tactic:
fun h => hx ⟨t, ht, h⟩

Premises used: And.intro, Exists.intro, Not
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
S : Set (Set α)
t : Set α
tS : t ∈ S
⊢ ⋂₀ S ⊆ t

Tactic:
sInf_le tS

Premises used: sInf_le, Set.sInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
S : Set (Set α)
t : Set α
tS : t ∈ S
⊢ t ⊆ ⋃₀ S

Tactic:
le_sSup tS

Premises used: Set.sUnion, le_sSup
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s : Set α
t : Set (Set α)
u : Set α
h₁ : s ⊆ u
h₂ : u ∈ t
⊢ s ⊆ ⋃₀ t

Tactic:
Subset.trans h₁ (subset_sUnion_of_mem h₂)

Premises used: Set.Subset.trans, Set.subset_sUnion_of_mem
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
S : Set (Set α)
t : Set α
h : ∀ t' ∈ S, t' ⊆ t
⊢ ⋃₀ S ⊆ t

Tactic:
sSup_le h

Premises used: Set.sUnion, sSup_le
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s : Set (Set α)
t : Set α
⊢ ⋃₀ s ⊆ t ↔ ∀ t' ∈ s, t' ⊆ t

Tactic:
sSup_le_iff

Premises used: Set.sUnion, sSup_le_iff
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s : Set (Set α)
f : Set α → Set α
hf : ∀ (t : Set α), t ⊆ f t
⊢ ⋃₀ s ⊆ ⋃₀ (f '' s)

Tactic:
fun _ ⟨t, htx, hxt⟩ ↦ ⟨f t, mem_image_of_mem f htx, hf t hxt⟩

Premises used: Set.sUnion, Membership.mem, Set.Subset, Set.mem_image_of_mem, And.intro, Exists.intro, Set.image, _private.0.Set.sUnion_mono_subsets.match_1
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s : Set (Set α)
f : Set α → Set α
hf : ∀ (t : Set α), f t ⊆ t
⊢ ⋃₀ (f '' s) ⊆ ⋃₀ s

Tactic:
fun _ ⟨_, ⟨u, hus, hut⟩, hxt⟩ ↦ ⟨u, hus, (hut ▸ hf u) hxt⟩

Premises used: Set.sUnion, Membership.mem, Set.Subset, And.intro, _private.0.Set.sUnion_mono_supsets.match_1, Exists.intro
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
S : Set (Set α)
t : Set α
h : ∀ t' ∈ S, t ⊆ t'
⊢ t ⊆ ⋂₀ S

Tactic:
le_sInf h

Premises used: le_sInf, Set.sInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
S : Set (Set α)
t : Set α
⊢ t ⊆ ⋂₀ S ↔ ∀ t' ∈ S, t ⊆ t'

Tactic:
le_sInf_iff

Premises used: le_sInf_iff, Set.sInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
S T : Set (Set α)
h : S ⊆ T
⊢ ⋃₀ S ⊆ ⋃₀ T

Tactic:
sUnion_subset fun _ hs => subset_sUnion_of_mem (h hs)

Premises used: Set.sUnion_subset, Set.subset_sUnion_of_mem
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
S T : Set (Set α)
h : S ⊆ T
⊢ ⋂₀ T ⊆ ⋂₀ S

Tactic:
subset_sInter fun _ hs => sInter_subset_of_mem (h hs)

Premises used: Set.sInter_subset_of_mem, Set.subset_sInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Set α) (⋃₀ ∅) ∅

Tactic:
sSup_empty

Premises used: sSup_empty, Set.sUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Set α) (⋂₀ ∅) univ

Tactic:
sInf_empty

Premises used: sInf_empty, Set.sInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s : Set α
⊢ ⋃₀ {s} = s

Tactic:
sSup_singleton

Premises used: sSup_singleton, Set.sUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s : Set α
⊢ ⋂₀ {s} = s

Tactic:
sInf_singleton

Premises used: Set.sInter, sInf_singleton
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
S : Set (Set α)
⊢ ⋃₀ S = ∅ ↔ ∀ s ∈ S, s = ∅

Tactic:
sSup_eq_bot

Premises used: sSup_eq_bot, Set.sUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
S : Set (Set α)
⊢ ⋂₀ S = univ ↔ ∀ s ∈ S, s = univ

Tactic:
sInf_eq_top

Premises used: sInf_eq_top, Set.sInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s : Set (Set α)
t : Set α
⊢ s ⊆ 𝒫 t ↔ ⋃₀ s ⊆ t

Tactic:
sUnion_subset_iff.symm

Premises used: Set.Mem, setOf, Set.powerset, Set.Subset, Set.sUnion_subset_iff, Iff.symm
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
⊢ GaloisConnection (fun (x : Set (Set α)) ↦ ⋃₀ x) fun (x : Set α) ↦ 𝒫 x

Tactic:
gc_sSup_Iic

Premises used: setOf, Set.sUnion, Set.powerset, gc_sSup_Iic, Set.Iic
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
S : Set (Set α)
h : S ⊆ {∅, univ}
⊢ Membership.mem (γ := Set (Set α)) {∅, univ} (⋃₀ S)

Tactic:
grind
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
S : Set (Set α)
⊢ (⋃₀ S).Nonempty ↔ ∃ s ∈ S, s.Nonempty

Tactic:
simp [nonempty_iff_ne_empty]

Premises used: Set.nonempty_iff_ne_empty
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s : Set (Set α)
h : (⋃₀ s).Nonempty
⊢ s.Nonempty

Tactic:
let ⟨s, hs, _⟩ := nonempty_sUnion.1 h
  ⟨s, hs⟩

Premises used: _private.0.Set.Nonempty.of_sUnion.match_1, Set.Nonempty, Set.nonempty_sUnion, Exists.intro, Iff.mp
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
inst : Nonempty α
s : Set (Set α)
h : ⋃₀ s = univ
⊢ s.Nonempty

Tactic:
Nonempty.of_sUnion <| h.symm ▸ univ_nonempty

Premises used: Set.univ_nonempty, Eq.rec, Set.Nonempty.of_sUnion, Eq.symm
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
S T : Set (Set α)
⊢ ⋃₀ (S ∪ T) = ⋃₀ S ∪ ⋃₀ T

Tactic:
sSup_union

Premises used: sSup_union, Set.sUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
S T : Set (Set α)
⊢ ⋂₀ (S ∪ T) = ⋂₀ S ∩ ⋂₀ T

Tactic:
sInf_union

Premises used: sInf_union, Set.sInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s : Set α
T : Set (Set α)
⊢ ⋃₀ insert s T = s ∪ ⋃₀ T

Tactic:
sSup_insert

Premises used: sSup_insert, Set.sUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s : Set α
T : Set (Set α)
⊢ ⋂₀ insert s T = s ∩ ⋂₀ T

Tactic:
sInf_insert

Premises used: sInf_insert, Set.sInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s : Set (Set α)
⊢ ⋃₀ (s \ {∅}) = ⋃₀ s

Tactic:
sSup_diff_singleton_bot s

Premises used: Set.Mem, setOf, Set.sUnion, sSup_diff_singleton_bot
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s : Set (Set α)
⊢ ⋂₀ (s \ {univ}) = ⋂₀ s

Tactic:
sInf_diff_singleton_top s

Premises used: Set.Mem, setOf, sInf_diff_singleton_top, Set.sInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s t : Set α
⊢ ⋃₀ {s, t} = s ∪ t

Tactic:
sSup_pair

Premises used: Set.sUnion, sSup_pair
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s t : Set α
⊢ ⋂₀ {s, t} = s ∩ t

Tactic:
sInf_pair

Premises used: sInf_pair, Set.sInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
f : α → Set β
s : Set α
⊢ ⋃₀ (f '' s) = ⋃ a ∈ s, f a

Tactic:
sSup_image

Premises used: Set.sUnion, sSup_image, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
f : α → Set β
s : Set α
⊢ ⋂₀ (f '' s) = ⋂ a ∈ s, f a

Tactic:
sInf_image

Premises used: Set.iInter, sInf_image, Set.sInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → Set γ
s : Set α
t : Set β
⊢ ⋃₀ image2 f s t = ⋃ a ∈ s, ⋃ b ∈ t, f a b

Tactic:
sSup_image2

Premises used: sSup_image2, Set.sUnion, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → Set γ
s : Set α
t : Set β
⊢ ⋂₀ image2 f s t = ⋂ a ∈ s, ⋂ b ∈ t, f a b

Tactic:
sInf_image2

Premises used: Set.iInter, sInf_image2, Set.sInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
β : Type u_2
ι : Sort u_5
f : ι → Set β
⊢ ⋃₀ range f = ⋃ (x : ι), f x

Tactic:
rfl

Premises used: Set.Mem, iSup, setOf, Set.iUnion, rfl
-- Module: Mathlib.Data.Set.Lattice
Goal:
β : Type u_2
ι : Sort u_5
f : ι → Set β
⊢ ⋂₀ range f = ⋂ (x : ι), f x

Tactic:
rfl

Premises used: iInf, Set.Mem, Set.iInter, setOf, rfl
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
f : ι → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), f i) univ ↔ ∀ (x : α), ∃ (i : ι), x ∈ f i

Tactic:
simp only [eq_univ_iff_forall, mem_iUnion]

Premises used: Set.eq_univ_iff_forall, Set.mem_iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), ⋃ (j : κ i), s i j) univ ↔ ∀ (a : α), ∃ (i : ι) (j : κ i), a ∈ s i j

Tactic:
simp only [iUnion_eq_univ_iff, mem_iUnion]

Premises used: Set.iUnion_eq_univ_iff, Set.mem_iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
c : Set (Set α)
⊢ ⋃₀ c = univ ↔ ∀ (a : α), ∃ b ∈ c, a ∈ b

Tactic:
simp only [eq_univ_iff_forall, mem_sUnion]

Premises used: Set.eq_univ_iff_forall, Set.mem_sUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
i : ι
f : ι → Set α
h : f i = ∅
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (j : ι), f j) ∅

Tactic:
subset_eq_empty (iInter_subset _ i) h

Premises used: Set.iInter_subset, Set.subset_eq_empty
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
f : ι → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), f i) ∅ ↔ ∀ (x : α), ∃ (i : ι), x ∉ f i

Tactic:
simp [Set.eq_empty_iff_forall_notMem]

Premises used: Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), ⋂ (j : κ i), s i j) ∅ ↔ ∀ (a : α), ∃ (i : ι) (j : κ i), a ∉ s i j

Tactic:
simp only [eq_empty_iff_forall_notMem, mem_iInter, not_forall]

Premises used: Set.mem_iInter, Set.eq_empty_iff_forall_notMem, Classical.not_forall
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
c : Set (Set α)
⊢ ⋂₀ c = ∅ ↔ ∀ (a : α), ∃ b ∈ c, a ∉ b

Tactic:
simp [Set.eq_empty_iff_forall_notMem]

Premises used: Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
f : ι → Set α
⊢ Set.Nonempty.{u_1} (α := α) (⋂ (i : ι), f i) ↔ ∃ (x : α), ∀ (i : ι), x ∈ f i

Tactic:
simp [nonempty_iff_ne_empty, iInter_eq_empty_iff]

Premises used: Set.nonempty_iff_ne_empty, Set.iInter_eq_empty_iff
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
⊢ Set.Nonempty.{u_1} (α := α) (⋂ (i : ι), ⋂ (j : κ i), s i j) ↔ ∃ (a : α), ∀ (i : ι) (j : κ i), a ∈ s i j

Tactic:
simp
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
c : Set (Set α)
⊢ (⋂₀ c).Nonempty ↔ ∃ (a : α), ∀ b ∈ c, a ∈ b

Tactic:
simp [nonempty_iff_ne_empty, sInter_eq_empty_iff]

Premises used: Set.nonempty_iff_ne_empty, Set.sInter_eq_empty_iff
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
S : Set (Set α)
x : α
⊢ x ∈ (⋃₀ S)ᶜ ↔ x ∈ ⋂₀ (compl '' S)

Tactic:
simp
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
S : Set (Set α)
rw : (⋃₀ S)ᶜᶜ = (⋂₀ (compl '' S))ᶜ
rw₁ rw₂ : (⋂₀ (compl '' S))ᶜ = (⋂₀ (compl '' S))ᶜ
⊢ ⋃₀ S = (⋂₀ (compl '' S))ᶜ

Tactic:
rw [← compl_compl (⋃₀ S), compl_sUnion]

Premises used: compl_compl, Set.sUnion, Set.compl_sUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
S : Set (Set α)
rw : (⋂₀ S)ᶜ = (⋂₀ (compl '' compl '' S))ᶜ
rw₁ rw₂ : (⋂₀ S)ᶜ = (⋂₀ S)ᶜ
⊢ (⋂₀ S)ᶜ = ⋃₀ (compl '' S)

Tactic:
rw [sUnion_eq_compl_sInter_compl, compl_compl_image]

Premises used: Set.compl_compl_image, Set.sUnion_eq_compl_sInter_compl
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
S : Set (Set α)
rw : (⋂₀ S)ᶜᶜ = (⋃₀ (compl '' S))ᶜ
rw₁ rw₂ : (⋃₀ (compl '' S))ᶜ = (⋃₀ (compl '' S))ᶜ
⊢ ⋂₀ S = (⋃₀ (compl '' S))ᶜ

Tactic:
rw [← compl_compl (⋂₀ S), compl_sInter]

Premises used: Set.compl_sInter, compl_compl, Set.sInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s t : Set α
S : Set (Set α)
hs : t ∈ S
h : s ∩ ⋃₀ S = ∅
rw : s ∩ t ⊆ s ∩ ⋃₀ S
⊢ s ∩ t ⊆ ∅

Tactic:
rw [← h]
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s t : Set α
S : Set (Set α)
hs : t ∈ S
h : s ∩ ⋃₀ S = ∅
⊢ s ∩ t ⊆ s ∩ ⋃₀ S

Tactic:
inter_subset_inter_right _ (subset_sUnion_of_mem hs)

Premises used: Set.inter_subset_inter_right, Set.subset_sUnion_of_mem
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s t : Set α
S : Set (Set α)
hs : t ∈ S
h : s ∩ ⋃₀ S = ∅
⊢ s ∩ t ⊆ s ∩ ⋃₀ S

Tactic:
exact inter_subset_inter_right _ (subset_sUnion_of_mem hs)

Premises used: Set.inter_subset_inter_right, Set.subset_sUnion_of_mem
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
γ : α → Type u_12
f : Sigma γ → β
⊢ ∀ (x : β), x ∈ range f ↔ Membership.mem (γ := Set β) (⋃ (a : α), range fun (b : γ a) ↦ f (Sigma.mk (β := γ) a b)) x

Tactic:
simp
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋃ (i : α), s i)
    (range fun (a : (i : α) × (↑(s i) : Type u_2)) ↦ (↑(a.snd (β := fun (i : α) ↦ (↑(s i) : Type u_2))) : β))

Tactic:
simp [Set.ext_iff]

Premises used: Set.ext_iff
-- Module: Mathlib.Data.Set.Lattice
Goal:
β : Type u_2
ι : Sort u_5
s : ι → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋃ (i : ι), s i)
    (range fun (a : (i : ι) ×' (↑(s i) : Type u_2)) ↦ (↑(a.snd (β := fun (i : ι) ↦ (↑(s i) : Type u_2))) : β))

Tactic:
simp [Set.ext_iff]

Premises used: Set.ext_iff
-- Module: Mathlib.Data.Set.Lattice
Goal:
ι : Type u_12
σ : ι → Type u_13
s : Set (Sigma σ)
h :
  ∀ (x : (i : ι) × σ i),
    Membership.mem (γ := Set ((i : ι) × σ i))
        (⋃ (i : ι), Sigma.mk (β := fun (i : ι) ↦ σ i) i '' Sigma.mk (β := σ) i ⁻¹' s) x ↔
      x ∈ s
⊢ ⋃ (i : ι), Sigma.mk (β := fun (i : ι) ↦ σ i) i '' Sigma.mk (β := σ) i ⁻¹' s = s

Tactic:
ext x
-- Module: Mathlib.Data.Set.Lattice
Goal:
ι : Type u_12
σ : ι → Type u_13
s : Set (Sigma σ)
x : (i : ι) × σ i
h : (∃ (i : ι) (x_1 : σ i), Sigma.mk (β := σ) i x_1 ∈ s ∧ Sigma.mk (β := fun (i : ι) ↦ σ i) i x_1 = x) ↔ x ∈ s
⊢ Membership.mem (γ := Set ((i : ι) × σ i))
      (⋃ (i : ι), Sigma.mk (β := fun (i : ι) ↦ σ i) i '' Sigma.mk (β := σ) i ⁻¹' s) x ↔
    x ∈ s

Tactic:
simp only [mem_iUnion, mem_image, mem_preimage]

Premises used: Set.mem_iUnion, Set.mem_image, Set.mem_preimage
-- Module: Mathlib.Data.Set.Lattice
Goal:
ι : Type u_12
σ : ι → Type u_13
s : Set (Sigma σ)
x : (i : ι) × σ i
⊢ (∃ (i : ι) (x_1 : σ i), Sigma.mk (β := σ) i x_1 ∈ s ∧ Sigma.mk (β := fun (i : ι) ↦ σ i) i x_1 = x) ↔ x ∈ s

Tactic:
grind
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
X : α → Type u_12
⊢ Eq (α := Set ((a : α) × X a)) Set.univ (⋃ (a : α), range (Sigma.mk (β := fun (a : α) ↦ X a) a))

Tactic:
Set.ext fun x =>
    iff_of_true trivial ⟨range (Sigma.mk x.1), Set.mem_range_self _, x.2, Sigma.eta x⟩

Premises used: Set.mem_range_self, Set.ext, trivial, Sigma.eta, Sigma.fst, iff_of_true, And.intro, Exists.intro, Sigma.mk, Set.range, Sigma.snd
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
ι₂ : Sort u_7
s : Set α
h : ι → ι₂
⊢ Subset.{u_1} (α := Set α) (⋃ (x : ι), s) (⋃ (x : ι₂), s)

Tactic:
iSup_const_mono (α := Set α) h

Premises used: iSup_const_mono, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
f : α → β
h : ∀ (x : β), Membership.mem (γ := Set β) (⋃ (x : α), {f x}) x ↔ x ∈ range f
⊢ ⋃ (x : α), {f x} = range f

Tactic:
ext x
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
f : α → β
x : β
⊢ Membership.mem (γ := Set β) (⋃ (x : α), {f x}) x ↔ x ∈ range f

Tactic:
simp [@eq_comm _ x]

Premises used: eq_comm
-- Module: Mathlib.Data.Set.Lattice
Goal:
β : Type u_2
ι : Type u_12
x : ι → β
t : ι → Set β
simp_rw : ⋃ (i : ι), t i ∪ {x i} = range x ∪ ⋃ (i : ι), t i
simp_rw₁ : (⋃ (i : ι), t i) ∪ ⋃ (i : ι), {x i} = range x ∪ ⋃ (i : ι), t i
simp_rw₂ : (⋃ (i : ι), t i) ∪ ⋃ (i : ι), {x i} = (⋃ (i : ι), t i) ∪ range x
⊢ ⋃ (i : ι), insert (x i) (t i) = range x ∪ ⋃ (i : ι), t i

Tactic:
simp_rw [← union_singleton, iUnion_union_distrib, union_comm, iUnion_singleton_eq_range]

Premises used: Set.iUnion_union_distrib, Set.iUnion_singleton_eq_range, Set.union_comm, Set.union_singleton
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_12
⊢ Eq.{u_12 + 1} (α := Set α) (⋃ (x : α), {x}) univ

Tactic:
simp [Set.ext_iff]

Premises used: Set.ext_iff
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s : Set α
⊢ ⋃ (i : (↑s : Type u_1)), {(↑i : α)} = s

Tactic:
simp
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s : Set (Set α)
rw : ⋃₀ s = ⋃₀ ((fun (i : Set α) ↦ i) '' s)
rw₁ rw₂ : ⋃₀ s = ⋃₀ s
⊢ ⋃₀ s = ⋃ i ∈ s, i

Tactic:
rw [← sUnion_image, image_id']

Premises used: Set.image_id', Set.sUnion_image
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s : Set (Set α)
rw : ⋂₀ s = ⋂₀ ((fun (i : Set α) ↦ i) '' s)
rw₁ rw₂ : ⋂₀ s = ⋂₀ s
⊢ ⋂₀ s = ⋂ i ∈ s, i

Tactic:
rw [← sInter_image, image_id']

Premises used: Set.image_id', Set.sInter_image
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s : Set (Set α)
⊢ ⋃₀ s = ⋃ (i : (↑s : Type u_1)), (↑i : Set α)

Tactic:
simp only [← sUnion_range, Subtype.range_coe]

Premises used: Set.sUnion_range, Subtype.range_coe
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s : Set (Set α)
⊢ ⋂₀ s = ⋂ (i : (↑s : Type u_1)), (↑i : Set α)

Tactic:
simp only [← sInter_range, Subtype.range_coe]

Premises used: Subtype.range_coe, Set.sInter_range
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
inst : IsEmpty ι
s : ι → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), s i) ∅

Tactic:
iSup_of_empty _

Premises used: iSup_of_empty, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
inst : IsEmpty ι
s : ι → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), s i) univ

Tactic:
iInf_of_empty _

Premises used: iInf_of_empty, Set.iInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s₁ s₂ : Set α
⊢ s₁ ∪ s₂ = ⋃ (b : Bool), bif b then s₁ else s₂

Tactic:
sup_eq_iSup s₁ s₂

Premises used: sup_eq_iSup, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s₁ s₂ : Set α
⊢ s₁ ∩ s₂ = ⋂ (b : Bool), bif b then s₁ else s₂

Tactic:
inf_eq_iInf s₁ s₂

Premises used: inf_eq_iInf, Set.iInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
S T : Set (Set α)
⊢ ⋂₀ S ∪ ⋂₀ T = ⋂ p ∈ S ×ˢ T, p.1 ∪ p.2

Tactic:
sInf_sup_sInf

Premises used: Set.iInter, Set.sInter, sInf_sup_sInf
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s t : Set (Set α)
⊢ ⋃₀ s ∩ ⋃₀ t = ⋃ p ∈ s ×ˢ t, p.1 ∩ p.2

Tactic:
sSup_inf_sSup

Premises used: sSup_inf_sSup, Set.sUnion, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
t : α → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋃ (x : α), ⋃ (_ : Membership.mem (γ := Set α) (⋃ (i : ι), s i) x), t x)
    (⋃ (i : ι), ⋃ x ∈ s i, t x)

Tactic:
simp [@iUnion_comm _ ι]

Premises used: Set.iUnion_comm
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
t : α → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋂ (x : α), ⋂ (_ : Membership.mem (γ := Set α) (⋃ (i : ι), s i) x), t x)
    (⋂ (i : ι), ⋂ x ∈ s i, t x)

Tactic:
simp [@iInter_comm _ ι]

Premises used: Set.iInter_comm
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
s : ι → Set (Set α)
⊢ Eq.{u_1 + 1} (α := Set α) (⋃₀ ⋃ (i : ι), s i) (⋃ (i : ι), ⋃₀ s i)

Tactic:
simp only [sUnion_eq_biUnion, biUnion_iUnion]

Premises used: Set.biUnion_iUnion, Set.sUnion_eq_biUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
s : ι → Set (Set α)
⊢ Eq.{u_1 + 1} (α := Set α) (⋂₀ ⋃ (i : ι), s i) (⋂ (i : ι), ⋂₀ s i)

Tactic:
simp only [sInter_eq_biInter, biInter_iUnion]

Premises used: Set.biInter_iUnion, Set.sInter_eq_biInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : (↑C : Type u_12)) → β → (↑(↑s : Set α) : Type u_12)
hf : ∀ (s : (↑C : Type u_12)), Surjective (f s)
h : ∀ (x : α), Membership.mem (γ := Set α) (⋃ (y : β), range fun (s : (↑C : Type u_12)) ↦ (↑(f s y) : α)) x ↔ x ∈ ⋃₀ C
⊢ (⋃ (y : β), range fun (s : (↑C : Type u_12)) ↦ (↑(f s y) : α)) = ⋃₀ C

Tactic:
ext x
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : (↑C : Type u_12)) → β → (↑(↑s : Set α) : Type u_12)
hf : ∀ (s : (↑C : Type u_12)), Surjective (f s)
x : α
h : Membership.mem (γ := Set α) (⋃ (y : β), range fun (s : (↑C : Type u_12)) ↦ (↑(f s y) : α)) x → x ∈ ⋃₀ C
h₁ : x ∈ ⋃₀ C → Membership.mem (γ := Set α) (⋃ (y : β), range fun (s : (↑C : Type u_12)) ↦ (↑(f s y) : α)) x
⊢ Membership.mem (γ := Set α) (⋃ (y : β), range fun (s : (↑C : Type u_12)) ↦ (↑(f s y) : α)) x ↔ x ∈ ⋃₀ C

Tactic:
constructor
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : (↑C : Type u_12)) → β → (↑(↑s : Set α) : Type u_12)
hf : ∀ (s : (↑C : Type u_12)), Surjective (f s)
y : β
s : Set α
hs : s ∈ C
⊢ (fun (s : (↑C : Type u_12)) ↦ (↑(f s y) : α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ C) s hs) ∈ ⋃₀ C

Tactic:
⟨_, hs, ?_⟩

Premises used: Set.Mem, setOf, Set.sUnion, And.intro, Exists.intro
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : (↑C : Type u_12)) → β → (↑(↑s : Set α) : Type u_12)
hf : ∀ (s : (↑C : Type u_12)), Surjective (f s)
y : β
s : Set α
hs : s ∈ C
h : (fun (s : (↑C : Type u_12)) ↦ (↑(f s y) : α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ C) s hs) ∈ s
⊢ (fun (s : (↑C : Type u_12)) ↦ (↑(f s y) : α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ C) s hs) ∈ ⋃₀ C

Tactic:
refine ⟨_, hs, ?_⟩
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : (↑C : Type u_12)) → β → (↑(↑s : Set α) : Type u_12)
hf : ∀ (s : (↑C : Type u_12)), Surjective (f s)
y : β
s : Set α
hs : s ∈ C
⊢ (fun (s : (↑C : Type u_12)) ↦ (↑(f s y) : α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ C) s hs) ∈ s

Tactic:
(f ⟨s, hs⟩ y).2

Premises used: Set.Mem, Subtype.mk, Subtype.property