awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Lattice
Goal:
β : Type u_2
ι : Sort u_5
s : ι → Set β
t : Set β
⊢ (⋂ (i : ι), s i) ∪ t = ⋂ (i : ι), s i ∪ t

Tactic:
iInf_sup_eq _ _

Premises used: Set.iInter, iInf_sup_eq
-- Module: Mathlib.Data.Set.Lattice
Goal:
β : Type u_2
ι : Sort u_5
x : β
t : ι → Set β
simp_rw : Eq (α := Set β) ((⋂ (i : ι), t i) ∪ {x}) (⋂ (i : ι), t i ∪ {x})
⊢ Eq (α := Set β) (insert x (⋂ (i : ι), t i)) (⋂ (i : ι), insert x (t i))

Tactic:
simp_rw [← union_singleton, iInter_union]

Premises used: Set.iInter_union, Set.union_singleton
-- Module: Mathlib.Data.Set.Lattice
Goal:
β : Type u_2
ι : Sort u_5
s : Set β
t : ι → Set β
⊢ (⋃ (i : ι), t i) \ s = ⋃ (i : ι), t i \ s

Tactic:
simp only [diff_eq, iUnion_inter]

Premises used: Set.diff_eq, Set.iUnion_inter
-- Module: Mathlib.Data.Set.Lattice
Goal:
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
s : Set β
t : ι → Set β
⊢ s \ ⋃ (i : ι), t i = ⋂ (i : ι), s \ t i

Tactic:
simp only [diff_eq, compl_iUnion, inter_iInter]

Premises used: Set.diff_eq, Set.compl_iUnion, Set.inter_iInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
β : Type u_2
ι : Sort u_5
s : Set β
t : ι → Set β
⊢ s \ ⋂ (i : ι), t i = ⋃ (i : ι), s \ t i

Tactic:
simp only [diff_eq, compl_iInter, inter_iUnion]

Premises used: Set.compl_iInter, Set.diff_eq, Set.inter_iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
s : Set α
inst : Nonempty ι
f : ι → Set α
⊢ (⋃ (n : ι), f n) ∆ s ⊆ ⋃ (n : ι), f n ∆ s

Tactic:
iSup_symmDiff_le

Premises used: iSup_symmDiff_le, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
s : Set α
inst : Nonempty ι
f : ι → Set α
⊢ s ∆ ⋃ (n : ι), f n ⊆ ⋃ (n : ι), s ∆ f n

Tactic:
symmDiff_iSup_le

Premises used: symmDiff_iSup_le, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
f g : ι → Set α
⊢ Subset.{u_1} (α := Set α) ((⋃ (n : ι), f n) ∆ ⋃ (n : ι), g n) (⋃ (n : ι), f n ∆ g n)

Tactic:
iSup_symmDiff_iSup_le

Premises used: iSup_symmDiff_iSup_le, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s : Set α
S : Set (Set α)
hS : S.Nonempty
⊢ ⋃₀ S ∆ s ⊆ ⋃₀ ((fun (x : Set α) ↦ x ∆ s) '' S)

Tactic:
sSup_symmDiff_le hS

Premises used: Set.Mem, setOf, Set.sUnion, sSup_symmDiff_le
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s : Set α
S : Set (Set α)
hS : S.Nonempty
⊢ s ∆ ⋃₀ S ⊆ ⋃₀ ((fun (x : Set α) ↦ s ∆ x) '' S)

Tactic:
symmDiff_sSup_le hS

Premises used: Set.Mem, setOf, Set.sUnion, symmDiff_sSup_le
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
S T : Set (Set α)
hS : S.Nonempty
hT : T.Nonempty
⊢ ⋃₀ S ∆ ⋃₀ T ⊆ ⋃₀ image2 (fun (x1 x2 : Set α) ↦ x1 ∆ x2) S T

Tactic:
sSup_symmDiff_sSup_le hS hT

Premises used: sSup_symmDiff_sSup_le, Set.Mem, setOf, Set.sUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
ι : Sort u_12
α : Type u_13
s t : ι → Set α
⊢ Subset.{u_13} (α := Set α) (⋃ (i : ι), s i ∩ t i) ((⋃ (i : ι), s i) ∩ ⋃ (i : ι), t i)

Tactic:
le_iSup_inf_iSup s t

Premises used: le_iSup_inf_iSup, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
ι : Type u_12
α : Type u_13
inst : Preorder ι
inst_1 : IsDirectedOrder ι
s t : ι → Set α
hs : Monotone s
ht : Monotone t
⊢ Eq.{u_13 + 1} (α := Set α) (⋃ (i : ι), s i ∩ t i) ((⋃ (i : ι), s i) ∩ ⋃ (i : ι), t i)

Tactic:
iSup_inf_of_monotone hs ht

Premises used: iSup_inf_of_monotone, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
ι : Type u_12
α : Type u_13
inst : Preorder ι
inst_1 : IsCodirectedOrder ι
s t : ι → Set α
hs : Antitone s
ht : Antitone t
⊢ Eq.{u_13 + 1} (α := Set α) (⋃ (i : ι), s i ∩ t i) ((⋃ (i : ι), s i) ∩ ⋃ (i : ι), t i)

Tactic:
iSup_inf_of_antitone hs ht

Premises used: Set.iUnion, iSup_inf_of_antitone
-- Module: Mathlib.Data.Set.Lattice
Goal:
ι : Type u_12
α : Type u_13
inst : Preorder ι
inst_1 : IsCodirectedOrder ι
s t : ι → Set α
hs : Monotone s
ht : Monotone t
⊢ Eq.{u_13 + 1} (α := Set α) (⋂ (i : ι), s i ∪ t i) ((⋂ (i : ι), s i) ∪ ⋂ (i : ι), t i)

Tactic:
iInf_sup_of_monotone hs ht

Premises used: Set.iInter, iInf_sup_of_monotone
-- Module: Mathlib.Data.Set.Lattice
Goal:
ι : Type u_12
α : Type u_13
inst : Preorder ι
inst_1 : IsDirectedOrder ι
s t : ι → Set α
hs : Antitone s
ht : Antitone t
⊢ Eq.{u_13 + 1} (α := Set α) (⋂ (i : ι), s i ∪ t i) ((⋂ (i : ι), s i) ∪ ⋂ (i : ι), t i)

Tactic:
iInf_sup_of_antitone hs ht

Premises used: Set.iInter, iInf_sup_of_antitone
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
ι' : Sort u_6
s : ι → ι' → Set α
⊢ Subset.{u_1} (α := Set α) (⋃ (j : ι'), ⋂ (i : ι), s i j) (⋂ (i : ι), ⋃ (j : ι'), s i j)

Tactic:
iSup_iInf_le_iInf_iSup (flip s)

Premises used: Set.iInter, iSup_iInf_le_iInf_iSup, flip, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Type u_12
s : Option ι → Set α
⊢ ⋃ (o : Option ι), s o = s none ∪ ⋃ (i : ι), s (some i)

Tactic:
iSup_option s

Premises used: iSup_option, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Type u_12
s : Option ι → Set α
⊢ ⋂ (o : Option ι), s o = s none ∩ ⋂ (i : ι), s (some i)

Tactic:
iInf_option s

Premises used: iInf_option, Set.iInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
p : ι → Prop
inst : DecidablePred p
f : (i : ι) → p i → Set α
g : (i : ι) → ¬p i → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), if h : p i then f i h else g i h)
    ((⋃ (i : ι), ⋃ (h : p i), f i h) ∪ ⋃ (i : ι), ⋃ (h : ¬p i), g i h)

Tactic:
iSup_dite _ _ _

Premises used: iSup_dite, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
p : ι → Prop
inst : DecidablePred p
f g : ι → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), if p i then f i else g i)
    ((⋃ (i : ι), ⋃ (_ : p i), f i) ∪ ⋃ (i : ι), ⋃ (_ : ¬p i), g i)

Tactic:
iUnion_dite _ _ _

Premises used: Set.iUnion_dite, ite
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
p : ι → Prop
inst : DecidablePred p
f : (i : ι) → p i → Set α
g : (i : ι) → ¬p i → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), if h : p i then f i h else g i h)
    ((⋂ (i : ι), ⋂ (h : p i), f i h) ∩ ⋂ (i : ι), ⋂ (h : ¬p i), g i h)

Tactic:
iInf_dite _ _ _

Premises used: Set.iInter, iInf_dite
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
p : ι → Prop
inst : DecidablePred p
f g : ι → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), if p i then f i else g i)
    ((⋂ (i : ι), ⋂ (_ : p i), f i) ∩ ⋂ (i : ι), ⋂ (_ : ¬p i), g i)

Tactic:
iInter_dite _ _ _

Premises used: Set.iInter_dite, ite
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s : False → Set α
⊢ iInter s = univ

Tactic:
iInf_false

Premises used: iInf_false, Set.iInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s : False → Set α
⊢ iUnion s = ∅

Tactic:
iSup_false

Premises used: iSup_false, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s : True → Set α
⊢ iInter s = s trivial

Tactic:
iInf_true

Premises used: Set.iInter, iInf_true
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s : True → Set α
⊢ iUnion s = s trivial

Tactic:
iSup_true

Premises used: iSup_true, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
p : ι → Prop
f : Exists p → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (x : Exists p), f x) (⋂ (i : ι), ⋂ (h : p i), f ⋯)

Tactic:
iInf_exists

Premises used: Set.iInter, iInf_exists
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
p : ι → Prop
f : Exists p → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (x : Exists p), f x) (⋃ (i : ι), ⋃ (h : p i), f ⋯)

Tactic:
iSup_exists

Premises used: iSup_exists, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (x : ι), ∅) ∅

Tactic:
iSup_bot

Premises used: Set.iUnion, iSup_bot
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (x : ι), univ) univ

Tactic:
iInf_top

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

Tactic:
iSup_eq_bot

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

Tactic:
iInf_eq_top

Premises used: iInf_eq_top, Set.iInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
s : ι → Set α
⊢ Set.Nonempty.{u_1} (α := α) (⋃ (i : ι), s i) ↔ ∃ (i : ι), (s i).Nonempty

Tactic:
simp [nonempty_iff_ne_empty]

Premises used: Set.nonempty_iff_ne_empty
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
t : Set α
s : α → Set β
⊢ Set.Nonempty.{u_2} (α := β) (⋃ i ∈ t, s i) ↔ ∃ i ∈ t, (s i).Nonempty

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

Tactic:
iSup_exists

Premises used: iSup_exists, Set.Nonempty, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
b : β
s : (x : β) → x = b → Set α
⊢ ⋂ (x : β), ⋂ (h : x = b), s x h = s b ⋯

Tactic:
iInf_iInf_eq_left

Premises used: Set.iInter, iInf_iInf_eq_left
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
b : β
s : (x : β) → b = x → Set α
⊢ ⋂ (x : β), ⋂ (h : b = x), s x h = s b ⋯

Tactic:
iInf_iInf_eq_right

Premises used: iInf_iInf_eq_right, Set.iInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
b : β
s : (x : β) → x = b → Set α
⊢ ⋃ (x : β), ⋃ (h : x = b), s x h = s b ⋯

Tactic:
iSup_iSup_eq_left

Premises used: Set.iUnion, iSup_iSup_eq_left
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
b : β
s : (x : β) → b = x → Set α
⊢ ⋃ (x : β), ⋃ (h : b = x), s x h = s b ⋯

Tactic:
iSup_iSup_eq_right

Premises used: iSup_iSup_eq_right, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
p q : Prop
s : p ∨ q → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (h : p ∨ q), s h) ((⋂ (h : p), s ⋯) ∩ ⋂ (h : q), s ⋯)

Tactic:
iInf_or

Premises used: Set.iInter, iInf_or
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
p q : Prop
s : p ∨ q → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (h : p ∨ q), s h) ((⋃ (i : p), s ⋯) ∪ ⋃ (j : q), s ⋯)

Tactic:
iSup_or

Premises used: Set.iUnion, iSup_or
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
p q : Prop
s : p ∧ q → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (h : p ∧ q), s h) (⋃ (hp : p), ⋃ (hq : q), s ⋯)

Tactic:
iSup_and

Premises used: Set.iUnion, iSup_and
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
p q : Prop
s : p ∧ q → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (h : p ∧ q), s h) (⋂ (hp : p), ⋂ (hq : q), s ⋯)

Tactic:
iInf_and

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

Tactic:
iSup_comm

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

Tactic:
iInf_comm

Premises used: Set.iInter, iInf_comm
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
γ : α → Type u_12
s : Sigma γ → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋃ (ia : Sigma γ), s ia) (⋃ (i : α), ⋃ (a : γ i), s (Sigma.mk (β := γ) i a))

Tactic:
iSup_sigma

Premises used: iSup_sigma, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
γ : α → Type u_12
s : (i : α) → γ i → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋃ (i : α), ⋃ (a : γ i), s i a) (⋃ (ia : Sigma γ), s (ia.fst (β := γ)) (ia.snd (β := γ)))

Tactic:
iSup_sigma' _

Premises used: iSup_sigma', Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
γ : α → Type u_12
s : Sigma γ → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋂ (ia : Sigma γ), s ia) (⋂ (i : α), ⋂ (a : γ i), s (Sigma.mk (β := γ) i a))

Tactic:
iInf_sigma

Premises used: Set.iInter, iInf_sigma
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
γ : α → Type u_12
s : (i : α) → γ i → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋂ (i : α), ⋂ (a : γ i), s i a) (⋂ (ia : Sigma γ), s (ia.fst (β := γ)) (ia.snd (β := γ)))

Tactic:
iInf_sigma' _

Premises used: Set.iInter, iInf_sigma'
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_8
κ' : ι' → Sort u_11
s : (i : ι) → κ i → (i' : ι') → κ' i' → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), ⋃ (j : κ i), ⋃ (i' : ι'), ⋃ (j' : κ' i'), s i j i' j')
    (⋃ (i' : ι'), ⋃ (j' : κ' i'), ⋃ (i : ι), ⋃ (j : κ i), s i j i' j')

Tactic:
iSup₂_comm _

Premises used: iSup₂_comm, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_8
κ' : ι' → Sort u_11
s : (i : ι) → κ i → (i' : ι') → κ' i' → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), ⋂ (j : κ i), ⋂ (i' : ι'), ⋂ (j' : κ' i'), s i j i' j')
    (⋂ (i' : ι'), ⋂ (j' : κ' i'), ⋂ (i : ι), ⋂ (j : κ i), s i j i' j')

Tactic:
iInf₂_comm _

Premises used: Set.iInter, iInf₂_comm
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
ι' : Sort u_6
p : ι → Prop
q : ι → ι' → Prop
s : (x : ι) → (y : ι') → p x ∧ q x y → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (x : ι), ⋃ (y : ι'), ⋃ (h : p x ∧ q x y), s x y h)
    (⋃ (x : ι), ⋃ (hx : p x), ⋃ (y : ι'), ⋃ (hy : q x y), s x y ⋯)

Tactic:
simp only [iUnion_and, @iUnion_comm _ ι']

Premises used: Set.iUnion_comm, Set.iUnion_and
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
ι' : Sort u_6
p : ι' → Prop
q : ι → ι' → Prop
s : (x : ι) → (y : ι') → p y ∧ q x y → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (x : ι), ⋃ (y : ι'), ⋃ (h : p y ∧ q x y), s x y h)
    (⋃ (y : ι'), ⋃ (hy : p y), ⋃ (x : ι), ⋃ (hx : q x y), s x y ⋯)

Tactic:
simp only [iUnion_and, @iUnion_comm _ ι]

Premises used: Set.iUnion_comm, Set.iUnion_and
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
ι' : Sort u_6
p : ι → Prop
q : ι → ι' → Prop
s : (x : ι) → (y : ι') → p x ∧ q x y → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (x : ι), ⋂ (y : ι'), ⋂ (h : p x ∧ q x y), s x y h)
    (⋂ (x : ι), ⋂ (hx : p x), ⋂ (y : ι'), ⋂ (hy : q x y), s x y ⋯)

Tactic:
simp only [iInter_and, @iInter_comm _ ι']

Premises used: Set.iInter_comm, Set.iInter_and
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
ι' : Sort u_6
p : ι' → Prop
q : ι → ι' → Prop
s : (x : ι) → (y : ι') → p y ∧ q x y → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (x : ι), ⋂ (y : ι'), ⋂ (h : p y ∧ q x y), s x y h)
    (⋂ (y : ι'), ⋂ (hy : p y), ⋂ (x : ι), ⋂ (hx : q x y), s x y ⋯)

Tactic:
simp only [iInter_and, @iInter_comm _ ι]

Premises used: Set.iInter_comm, Set.iInter_and
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
b : β
p : β → Prop
s : (x : β) → x = b ∨ p x → Set α
⊢ ⋃ (x : β), ⋃ (h : x = b ∨ p x), s x h = s b ⋯ ∪ ⋃ (x : β), ⋃ (h : p x), s x ⋯

Tactic:
simp only [iUnion_or, iUnion_union_distrib, iUnion_iUnion_eq_left]

Premises used: Set.iUnion_union_distrib, Set.iUnion_iUnion_eq_left, Set.iUnion_or
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
b : β
p : β → Prop
s : (x : β) → x = b ∨ p x → Set α
⊢ ⋂ (x : β), ⋂ (h : x = b ∨ p x), s x h = s b ⋯ ∩ ⋂ (x : β), ⋂ (h : p x), s x ⋯

Tactic:
simp only [iInter_or, iInter_inter_distrib, iInter_iInter_eq_left]

Premises used: Set.iInter_iInter_eq_left, Set.iInter_or, Set.iInter_inter_distrib
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : α ⊕ β → Set γ
⊢ Eq.{u_3 + 1} (α := Set γ) (⋃ (x : α ⊕ β), s x) ((⋃ (x : α), s (Sum.inl x)) ∪ ⋃ (x : β), s (Sum.inr x))

Tactic:
iSup_sum

Premises used: Set.iUnion, iSup_sum
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : α ⊕ β → Set γ
⊢ Eq.{u_3 + 1} (α := Set γ) (⋂ (x : α ⊕ β), s x) ((⋂ (x : α), s (Sum.inl x)) ∩ ⋂ (x : β), s (Sum.inr x))

Tactic:
iInf_sum

Premises used: iInf_sum, Set.iInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
γ : α → Type u_12
s : PSigma γ → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋃ (ia : PSigma γ), s ia) (⋃ (i : α), ⋃ (a : γ i), s (PSigma.mk (β := γ) i a))

Tactic:
iSup_psigma _

Premises used: iSup_psigma, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
γ : α → Type u_12
s : (i : α) → γ i → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋃ (i : α), ⋃ (a : γ i), s i a) (⋃ (ia : PSigma γ), s (ia.fst (β := γ)) (ia.snd (β := γ)))

Tactic:
iSup_psigma' _

Premises used: iSup_psigma', Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
γ : α → Type u_12
s : PSigma γ → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋂ (ia : PSigma γ), s ia) (⋂ (i : α), ⋂ (a : γ i), s (PSigma.mk (β := γ) i a))

Tactic:
iInf_psigma _

Premises used: Set.iInter, iInf_psigma
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
γ : α → Type u_12
s : (i : α) → γ i → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋂ (i : α), ⋂ (a : γ i), s i a) (⋂ (ia : PSigma γ), s (ia.fst (β := γ)) (ia.snd (β := γ)))

Tactic:
iInf_psigma' _

Premises used: iInf_psigma', Set.iInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : α → Set β
x : α
y : β
xs : x ∈ s
ytx : y ∈ t x
⊢ Membership.mem (γ := Set β) (⋃ x ∈ s, t x) y

Tactic:
mem_iUnion₂_of_mem xs ytx

Premises used: Set.mem_iUnion₂_of_mem
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : α → Set β
y : β
h : ∀ x ∈ s, y ∈ t x
⊢ Membership.mem (γ := Set β) (⋂ x ∈ s, t x) y

Tactic:
mem_iInter₂_of_mem h

Premises used: Set.mem_iInter₂_of_mem
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
s : Set α
u : α → Set β
x : α
xs : x ∈ s
⊢ u x ⊆ ⋃ x ∈ s, u x

Tactic:
subset_iUnion₂ (s := fun i _ => u i) x xs

Premises used: Set.subset_iUnion₂
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : α → Set β
x : α
xs : x ∈ s
⊢ ⋂ x ∈ s, t x ⊆ t x

Tactic:
iInter₂_subset x xs

Premises used: Set.iInter₂_subset
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
s : Set α
hs : s.Nonempty
t : α → Set β
⊢ Subset.{u_2} (α := Set β) (⋂ x ∈ s, t x) (⋃ x ∈ s, t x)

Tactic:
biInf_le_biSup hs

Premises used: Set.iInter, biInf_le_biSup, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
s s' : Set α
t : α → Set β
h : s ⊆ s'
⊢ Subset.{u_2} (α := Set β) (⋃ x ∈ s, t x) (⋃ x ∈ s', t x)

Tactic:
iUnion₂_subset fun _ hx => subset_biUnion_of_mem <| h hx

Premises used: Set.iUnion₂_subset, Set.subset_biUnion_of_mem
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
s s' : Set α
t : α → Set β
h : s' ⊆ s
⊢ Subset.{u_2} (α := Set β) (⋂ x ∈ s, t x) (⋂ x ∈ s', t x)

Tactic:
subset_iInter₂ fun _ hx => biInter_subset_of_mem <| h hx

Premises used: Set.subset_iInter₂, Set.biInter_subset_of_mem
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
s s' : Set α
t t' : α → Set β
hs : s' ⊆ s
h : ∀ x ∈ s, t x ⊆ t' x
⊢ Subset.{u_2} (α := Set β) (⋃ x ∈ s', t x) (⋃ x ∈ s, t' x)

Tactic:
(biUnion_subset_biUnion_left hs).trans <| iUnion₂_mono h

Premises used: HasSubset.Subset.trans, Set.iUnion₂_mono, Set.biUnion_subset_biUnion_left
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
s s' : Set α
t t' : α → Set β
hs : s ⊆ s'
h : ∀ x ∈ s, t x ⊆ t' x
⊢ Subset.{u_2} (α := Set β) (⋂ x ∈ s', t x) (⋂ x ∈ s, t' x)

Tactic:
(biInter_subset_biInter_left hs).trans <| iInter₂_mono h

Premises used: Set.iInter₂_mono, HasSubset.Subset.trans, Set.biInter_subset_biInter_left
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : (x : α) → x ∈ s → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋃ (x : α), ⋃ (h : x ∈ s), t x h) (⋃ (x : (↑s : Type u_1)), t (↑x : α) ⋯)

Tactic:
iSup_subtype'

Premises used: iSup_subtype', Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : (x : α) → x ∈ s → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋂ (x : α), ⋂ (h : x ∈ s), t x h) (⋂ (x : (↑s : Type u_1)), t (↑x : α) ⋯)

Tactic:
iInf_subtype'

Premises used: Set.iInter, iInf_subtype'
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
s : Set α
hs : s.Nonempty
t : Set β
⊢ ⋃ a ∈ s, t = t

Tactic:
biSup_const hs

Premises used: biSup_const, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
s : Set α
hs : s.Nonempty
t : Set β
⊢ ⋂ a ∈ s, t = t

Tactic:
biInf_const hs

Premises used: Set.iInter, biInf_const
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
p : α → Prop
s : { x : α // p x } → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋃ (x : { x : α // p x }), s x)
    (⋃ (x : α), ⋃ (hx : p x), s (Subtype.mk (p := fun (x : α) ↦ p x) x hx))

Tactic:
iSup_subtype

Premises used: iSup_subtype, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
p : α → Prop
s : { x : α // p x } → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋂ (x : { x : α // p x }), s x)
    (⋂ (x : α), ⋂ (hx : p x), s (Subtype.mk (p := fun (x : α) ↦ p x) x hx))

Tactic:
iInf_subtype

Premises used: Set.iInter, iInf_subtype
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
u : α → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋂ (x : α), ⋂ (_ : Membership.mem (γ := Set α) ∅ x), u x) univ

Tactic:
iInf_emptyset

Premises used: Set.iInter, iInf_emptyset
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
u : α → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋂ (x : α), ⋂ (_ : Membership.mem (γ := Set α) univ x), u x) (⋂ (x : α), u x)

Tactic:
iInf_univ

Premises used: Set.iInter, iInf_univ
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s : Set α
⊢ ⋃ x ∈ s, s = s

Tactic:
Subset.antisymm (iUnion₂_subset fun _ _ => Subset.refl s) fun _ hx => mem_biUnion hx hx

Premises used: Set.Subset.antisymm, Set.iUnion₂_subset, Set.Subset.refl, Set.mem_biUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
s : Set α
rw : ⋃ x ∈ s, s = s
rw₁ rw₂ : s = s
⊢ ⋃ (_ : s.Nonempty), s = s

Tactic:
rw [iUnion_nonempty_index, biUnion_self]

Premises used: Set.iUnion_nonempty_index, Set.biUnion_self
-- 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:
iInf_singleton

Premises used: Set.iInter, iInf_singleton
-- 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:
iInf_union

Premises used: Set.iInter, iInf_union
-- 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 β
rw : s a ∩ ⋂ (x : α), ⋂ (_ : Membership.mem (γ := Set α) {b} x), s x = s a ∩ s b
rw₁ rw₂ : s a ∩ s b = s a ∩ s b
⊢ ⋂ (x : α), ⋂ (_ : Membership.mem (γ := Set α) {a, b} x), s x = s a ∩ s b

Tactic:
rw [biInter_insert, biInter_singleton]

Premises used: Set.biInter_insert, Set.biInter_singleton
-- Module: Mathlib.Data.Set.Lattice
Goal:
ι : Type u_12
α : Type u_13
s : Set ι
hs : s.Nonempty
f : ι → Set α
t : Set α
⊢ Nonempty.{u_12 + 1} (↑s : Type u_12)

Tactic:
haveI : Nonempty s := hs.to_subtype
-- Module: Mathlib.Data.Set.Lattice
Goal:
ι : Type u_12
α : Type u_13
s : Set ι
hs : s.Nonempty
f : ι → Set α
t : Set α
this : Nonempty.{u_12 + 1} (↑s : Type u_12)
⊢ ⋂ i ∈ s, f i ∩ t = (⋂ i ∈ s, f i) ∩ t

Tactic:
simp [biInter_eq_iInter, ← iInter_inter]

Premises used: Set.biInter_eq_iInter, Set.iInter_inter
-- Module: Mathlib.Data.Set.Lattice
Goal:
ι : Type u_12
α : Type u_13
s : Set ι
hs : s.Nonempty
f : ι → Set α
t : Set α
rw : Eq.{u_13 + 1} (α := Set α) (⋂ i ∈ s, t ∩ f i) (⋂ i ∈ s, f i ∩ t)
⊢ ⋂ i ∈ s, t ∩ f i = t ∩ ⋂ i ∈ s, f i

Tactic:
rw [inter_comm, ← biInter_inter hs]

Premises used: Set.biInter_inter, Set.inter_comm
-- Module: Mathlib.Data.Set.Lattice
Goal:
ι : Type u_12
α : Type u_13
s : Set ι
hs : s.Nonempty
f : ι → Set α
t : Set α
⊢ Eq.{u_13 + 1} (α := Set α) (⋂ i ∈ s, t ∩ f i) (⋂ i ∈ s, f i ∩ t)

Tactic:
simp [inter_comm]

Premises used: Set.inter_comm
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋃ (x : α), ⋃ (_ : Membership.mem (γ := Set α) ∅ x), s x) ∅

Tactic:
iSup_emptyset

Premises used: iSup_emptyset, Set.iUnion