mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst✝ : SupSet α
f : ι → α
g : ι' → α
h : ι → ι'
h1 : Surjective h
h2 : ∀ (x : ι), g (h x) = f x
⊢ ⨆ x, f x = ⨆ y, g y

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : SupSet α
p q : Prop
f₁ : p → α
f₂ : q → α
pq : p ↔ q
f : ∀ (x : q), f₁ ⋯ = f₂ x
⊢ iSup f₁ = iSup f₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : SupSet α
g : β → α
f : ι → β
⊢ ⨆ b, g ↑b = ⨆ i, g (f i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : SupSet α
s : Set β
f : β → α
⊢ sSup (f '' s) = ⨆ a, f ↑a

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
κ : ι → Sort u_6
inst✝ : CompleteLattice α
a : α
f : (i : ι) → κ i → α
⊢ ⨆ i, ⨆ j, f i j ≤ a ↔ ∀ (i : ι) (j : κ i), f i j ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
s : Set α
f : α → β
hf : Monotone f
⊢ ⨆ a ∈ s, f a ≤ f (sSup s)

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : α ≃o β
x✝ : ι → α
x : α
⊢ f (⨆ i, x✝ i) ≤ f x ↔ ⨆ i, f (x✝ i) ≤ f x

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
κ : ι → Sort u_6
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : α ≃o β
x✝ : (i : ι) → κ i → α
x : α
⊢ f (⨆ i, ⨆ j, x✝ i j) ≤ f x ↔ ⨆ i, ⨆ j, f (x✝ i j) ≤ f x

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : α ≃o β
s : Set α
⊢ f (sSup s) = ⨆ a ∈ s, f a

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
a : α
inst✝ : Nonempty ι
⊢ ⨆ x, a = a

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
inst✝ : Unique ι
f : ι → α
⊢ ⨆ i, f i = f default

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
s : ι → α
⊢ ⊥ < ⨆ i, s i ↔ ∃ i, ⊥ < s i

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
κ : ι → Sort u_6
inst✝ : CompleteLattice α
f : (i : ι) → κ i → α
⊢ ⨆ i, ⨆ j, f i j = ⊥ ↔ ∀ (i : ι) (j : κ i), f i j = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
p : Prop
inst✝ : Decidable p
a : p → α
⊢ ⨆ (h : p), a h = if h : p then a h else ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
ι₁ : Sort u_8
ι₂ : Sort u_9
κ₁ : ι₁ → Sort u_10
κ₂ : ι₂ → Sort u_11
f : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → α
⊢ ⨆ i₁, ⨆ j₁, ⨆ i₂, ⨆ j₂, f i₁ j₁ i₂ j₂ = ⨆ i₂, ⨆ j₂, ⨆ i₁, ⨆ j₁, f i₁ j₁ i₂ j₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
a : α
s : Set β
hs : s.Nonempty
⊢ ⨆ i ∈ s, a = a

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
ι : Type u_8
ι' : Type u_9
g : ι' → α
e : ι ≃ ι'
s : Set ι'
⊢ ⨆ i ∈ ⇑e.symm '' s, g (e i) = ⨆ i ∈ s, g i

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
inst✝ : Nonempty ι
f : ι → α
a : α
⊢ (⨆ x, f x) ⊔ a = ⨆ x, f x ⊔ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
inst✝ : Nonempty ι
f : ι → α
a : α
⊢ a ⊔ ⨆ x, f x = ⨆ x, a ⊔ f x

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
p : ι → Prop
f : (i : ι) → p i → α
a : α
h : ∃ i, p i
⊢ (⨆ i, ⨆ (h : p i), f i h) ⊔ a = ⨆ i, ⨆ (h : p i), f i h ⊔ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
p : ι → Prop
f : (i : ι) → p i → α
a : α
h : ∃ i, p i
⊢ a ⊔ ⨆ i, ⨆ (h : p i), f i h = ⨆ i, ⨆ (h : p i), a ⊔ f i h

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CompleteLattice α
ι : Type u_8
inst✝¹ : LT ι
inst✝ : NoMaxOrder ι
f : ι → α
⊢ ⨆ i, ⨆ j, ⨆ (_ : j < i), f j = ⨆ i, f i

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : Preorder ι
f : ι → α
⊢ ⨆ i, ⨆ j, ⨆ (_ : j ≤ i), f j = ⨆ i, f i

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CompleteLattice α
ι : Type u_8
inst✝¹ : LT ι
inst✝ : NoMinOrder ι
f : ι → α
⊢ ⨆ i, ⨆ j, ⨆ (_ : j > i), f j = ⨆ i, f i

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : Preorder ι
f : ι → α
⊢ ⨆ i, ⨆ j, ⨆ (_ : j ≥ i), f j = ⨆ i, f i

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
s : False → α
⊢ iSup s = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
x : γ
s : (i : ι) → κ i → Set γ
⊢ x ∈ ⋃ i, ⋃ j, s i j ↔ ∃ i j, x ∈ s i j

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
p : ι → Prop
inst✝ : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
⊢ (⨆ 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:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
x : γ
s : (i : ι) → κ i → Set γ
⊢ x ∈ ⋂ i, ⋂ j, s i j ↔ ∀ (i : ι) (j : κ i), x ∈ s i j

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : CompleteLattice α
g : β → α
f : ι → β
⊢ ⨆ b ∈ range f, g b = ⨆ i, g (f i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
s : Set β
f : β → α
⊢ sSup (f '' s) = ⨆ a ∈ s, f a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: β : Type u_2
ι : Type u_12
t : Set ι
s : ι → Set β
w : ⋃ i ∈ t, s i = ⊤
x : β
⊢ ∃ i ∈ t, x ∈ s i

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Type u_12
t : Set ι
s : ι → Set α
H : Nonempty α
w : ⋃ i ∈ t, s i = ⊤
⊢ t.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : α ≃o β
s : Set α
⊢ f (sSup s) = sSup (⇑f.symm ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
⊢ ⨆ x ∈ ∅, f x = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
s : ι → Set α
h_Union : (⋃ i, s i).Nonempty
⊢ Nonempty ι

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
⊢ ⨆ x ∈ univ, f x = ⨆ x, f x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
s : ι → Set α
inst✝ : Nonempty α
h_Union : ⋃ i, s i = univ
⊢ (⋃ i, s i).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
s t : Set β
⊢ ⨆ x ∈ s ∪ t, f x = (⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
p : β → Prop
⊢ ⨆ i, f i = (⨆ i, ⨆ (_ : p i), f i) ⊔ ⨆ i, ⨆ (_ : ¬p i), f i

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
i₀ : β
⊢ ⨆ i, f i = f i₀ ⊔ ⨆ i, ⨆ (_ : i ≠ i₀), f i

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
t : Set α
⊢ ⋃ i, ⋃ j, s i j ⊆ t ↔ ∀ (i : ι) (j : κ i), s i j ⊆ t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : Set α
t : (i : ι) → κ i → Set α
⊢ s ⊆ ⋂ i, ⋂ j, t i j ↔ ∀ (i : ι) (j : κ i), s ⊆ t i j

Tactic:
subset_iInter_iff

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : Set α
t : (i : ι) → κ i → Set α
⊢ s ⊆ ⋂ i, ⋂ j, t i j ↔ ∀ (i : ι) (j : κ i), s ⊆ t i j

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
s : Set β
b : β
⊢ ⨆ x ∈ insert b s, f x = f b ⊔ ⨆ x ∈ s, f x

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
b : β
⊢ ⨆ x ∈ {b}, f x = f b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
P : ι → α → Prop
⊢ ⋃ i, {x | P i x} = {x | ∃ i, P i x}

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
a b : β
⊢ ⨆ x ∈ {a, b}, f x = f a ⊔ f b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
P : ι → α → Prop
⊢ ⋂ i, {x | P i x} = {x | ∀ (i : ι), P i x}

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
γ : Type u_8
f : β → γ
g : γ → α
t : Set β
⊢ ⨆ c ∈ f '' t, g c = ⨆ b ∈ t, g (f b)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
⊢ (⋃ i, ⋃ j, s i j)ᶜ = ⋂ i, ⋂ j, (s i j)ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : CompleteLattice α
e : ι → β
he : Injective e
f : ι → α
⊢ ⨆ j, extend e f ⊥ j = ⨆ i, f i

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
⊢ (⋂ i, ⋂ j, s i j)ᶜ = ⋃ i, ⋃ j, (s i j)ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: β : Type u_2
ι : Sort u_5
s : ι → Set β
⊢ ⋃ i, s i = (⋂ i, (s i)ᶜ)ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CompleteLattice α
s : Set β
t : Set γ
f : β → γ
g : γ → α
hf : BijOn f s t
⊢ ⨆ x ∈ s, g (f x) = ⨆ y ∈ t, g y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: β : Type u_2
ι : Sort u_5
s : ι → Set β
⊢ ⋂ i, s i = (⋃ i, (s i)ᶜ)ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
x : β
t : ι → Set β
⊢ insert x (⋃ i, t i) = ⋃ i, insert x (t i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CompleteLattice α
s : Set β
t : Set γ
f : β → α
g : γ → α
h : β → γ
h1 : BijOn h s t
h2 : ∀ (x : β), g (h x) = f x
⊢ ⨆ x ∈ s, f x = ⨆ y ∈ t, g y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: β : Type u_2
ι : Sort u_5
x : β
t : ι → Set β
⊢ insert x (⋂ i, t i) = ⋂ i, insert x (t i)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: β : Type u_2
ι : Sort u_5
s : Set β
t : ι → Set β
⊢ (⋃ i, t i) \ s = ⋃ i, t i \ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : Set β
t : ι → Set β
⊢ s \ ⋃ i, t i = ⋂ i, s \ t i

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: β : Type u_2
ι : Sort u_5
s : Set β
t : ι → Set β
⊢ s \ ⋂ i, t i = ⋃ i, s \ t i

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
s : ι → Set α
⊢ (⋃ i, s i).Nonempty ↔ ∃ i, (s i).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set α
s : α → Set β
⊢ (⋃ i ∈ t, s i).Nonempty ↔ ∃ i ∈ t, (s i).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
ι' : Sort u_6
p : ι → Prop
q : ι → ι' → Prop
s : (x : ι) → (y : ι') → p x ∧ q x y → 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:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : PartialOrder ι
f : ι → α
i : ι
⊢ ⨆ j, ⨆ (_ : j ≤ i), f j = (⨆ j, ⨆ (_ : j < i), f j) ⊔ f i

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
ι' : Sort u_6
p : ι' → Prop
q : ι → ι' → Prop
s : (x : ι) → (y : ι') → p y ∧ q x y → 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:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
ι' : Sort u_6
p : ι → Prop
q : ι → ι' → Prop
s : (x : ι) → (y : ι') → p x ∧ q x y → 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:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
ι' : Sort u_6
p : ι' → Prop
q : ι → ι' → Prop
s : (x : ι) → (y : ι') → p y ∧ q x y → 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:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : 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:
by

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
s : Set α
b : α
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
⊢ sSup s ⊓ b = ⨆ a ∈ s, a ⊓ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : PartialOrder ι
f : ι → α
i : ι
⊢ ⨆ j, ⨆ (_ : j ≥ i), f j = f i ⊔ ⨆ j, ⨆ (_ : j > i), f j

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : 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:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
s : Set β
f : β → α
⊢ IsLUB (f '' s) (⨆ x ∈ s, f x)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
s : Set α
⊢ ⋃ (_ : s.Nonempty), s = s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
s : Set α
t : α → Set β
⊢ ⋂ x ∈ insert a s, t x = t a ∩ ⋂ x ∈ s, t x

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
p : β → Type u_8
f : Sigma p → α
c : α
⊢ ⨆ x, f x ≤ c ↔ ⨆ i, ⨆ j, f ⟨i, j⟩ ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
a b : α
s : α → Set β
⊢ ⋂ x ∈ {a, b}, s x = s a ∩ s b

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
ι : Sort u_8
κ : ι → Sort u_9
f : (i : ι) ×' κ i → α
c : α
⊢ ⨆ ij, f ij ≤ c ↔ ⨆ i, ⨆ j, f ⟨i, j⟩ ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: ι : Type u_12
α : Type u_13
s : Set ι
hs : s.Nonempty
f : ι → Set α
t : Set α
⊢ ⋂ i ∈ s, f i ∩ t = (⋂ i ∈ s, f i) ∩ t

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CompleteLattice α
f : β × γ → α
c : α
⊢ ⨆ x, f x ≤ c ↔ ⨆ i, ⨆ j, f (i, j) ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
f : ι → α
a : α
⊢ (⨆ i, f i) ⊓ a = ⨆ i, f i ⊓ a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: ι : Type u_12
α : Type u_13
s : Set ι
hs : s.Nonempty
f : ι → Set α
t : Set α
⊢ ⋂ i ∈ s, t ∩ f i = t ∩ ⋂ i ∈ s, f i

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
s : Set α
⊢ ∀ (x : α), x ∈ ⋃ x ∈ s, {x} ↔ x ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
s : Set α
t : α → Set β
⊢ ⋃ x ∈ insert a s, t x = t a ∪ ⋃ x ∈ s, t x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
a b : α
s : α → Set β
⊢ ⋃ x ∈ {a, b}, s x = s a ∪ s b

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CompleteLattice α
f : β × γ → α
s : Set β
t : Set γ
⊢ ⨆ x ∈ s ×ˢ t, f x = ⨆ a ∈ s, ⨆ b ∈ t, f (a, b)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : Set α
t : (i : ι) → κ i → Set α
⊢ s ∩ ⋃ i, ⋃ j, t i j = ⋃ i, ⋃ j, s ∩ t i j

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
a : α
f : ι → α
⊢ a ⊓ ⨆ i, f i = ⨆ i, a ⊓ f i

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
t : Set α
⊢ (⋃ i, ⋃ j, s i j) ∩ t = ⋃ i, ⋃ j, s i j ∩ t

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
a : α
⊢ a ⊓ ⨆ i, ⨆ j, f i j = ⨆ i, ⨆ j, a ⊓ f i j

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : Set α
t : (i : ι) → κ i → Set α
⊢ s ∪ ⋂ i, ⋂ j, t i j = ⋂ i, ⋂ j, s ∪ t i j

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
t : Set α
⊢ (⋂ i, ⋂ j, s i j) ∪ t = ⋂ i, ⋂ j, s i j ∪ t

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
γ : Type u_8
δ : Type u_9
f : β → γ → δ
s : Set β
t : Set γ
g : δ → α
⊢ ⨆ d ∈ image2 f s t, g d = ⨆ b ∈ s, ⨆ c ∈ t, g (f b c)

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CompleteLattice α
f : β ⊕ γ → α
c : α
⊢ ⨆ x, f x ≤ c ↔ (⨆ i, f (Sum.inl i)) ⊔ ⨆ j, f (Sum.inr j) ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : S ⊆ {∅, univ}
⊢ ⋃₀ S ∈ {∅, univ}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
S : Set (Set α)
⊢ (⋃₀ S).Nonempty ↔ ∃ s ∈ S, s.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Option β → α
c : α
⊢ ⨆ o, f o ≤ c ↔ f none ⊔ ⨆ b, f (some b) ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
f : ι → Set α
⊢ ⋃ i, f i = univ ↔ ∀ (x : α), ∃ i, x ∈ f i

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
⊢ ⋃ i, ⋃ j, s i j = univ ↔ ∀ (a : α), ∃ i j, a ∈ s i j

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
x✝ b c : α
h : x✝ ≤ sSup {c_1 | c_1 ⊓ b ≤ c}
⊢ sSup {c_1 | c_1 ⊓ b ≤ c} ⊓ b ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
a : α
f : β → α
⊢ ⨆ o, o.elim a f = a ⊔ ⨆ b, f b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
c : Set (Set α)
⊢ ⋃₀ c = univ ↔ ∀ (a : α), ∃ b ∈ c, a ∈ b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
f : ι → Set α
⊢ ⋂ i, f i = ∅ ↔ ∀ (x : α), ∃ i, x ∉ f i

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
⊢ ⋂ i, ⋂ j, s i j = ∅ ↔ ∀ (a : α), ∃ i j, a ∉ s i j

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
c : Set (Set α)
⊢ ⋂₀ c = ∅ ↔ ∀ (a : α), ∃ b ∈ c, a ∉ b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
f : ι → Set α
⊢ (⋂ i, f i).Nonempty ↔ ∃ x, ∀ (i : ι), x ∈ f i

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
⊢ (⋂ i, ⋂ j, s i j).Nonempty ↔ ∃ a, ∀ (i : ι) (j : κ i), a ∈ s i j

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
a b x✝ : α
h : sInf {c | a ≤ b ⊔ c} ≤ x✝
⊢ a ≤ b ⊔ sInf {c | a ≤ b ⊔ c}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
c : Set (Set α)
⊢ (⋂₀ c).Nonempty ↔ ∃ a, ∀ b ∈ c, a ∈ b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
S : Set (Set α)
x : α
⊢ x ∈ (⋃₀ S)ᶜ ↔ x ∈ ⋂₀ (compl '' S)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
S : Set (Set α)
⊢ ⋃₀ S = (⋂₀ (compl '' S))ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
S : Set (Set α)
⊢ (⋂₀ S)ᶜ = ⋃₀ (compl '' S)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
S : Set (Set α)
⊢ ⋂₀ S = (⋃₀ (compl '' S))ᶜ

Tactic:
by

Goal state after: