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

Goal state before:
pp: ι : Type u_5
s : Set ι
⊢ ⋃ s', Subtype.val '' ↑s' = s

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
P : Finset α → Prop
s : Finset α
hP : ∀ ⦃s t : Finset α⦄, P t → s ⊆ t → P s
⊢ Maximal P s ↔ P s ∧ ∀ x ∉ s, ¬P (insert x s)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
P : Finset α → Prop
s : Finset α
hP : ∀ ⦃s t : Finset α⦄, P t → t ⊆ s → P s
h : Minimal P s
x : α
hxs : x ∈ s
hx : P (s.erase x)
⊢ False

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : CompleteLattice β
a : α
s : α → β
⊢ ⨆ x ∈ {a}, s x = s a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : CompleteLattice β
o : Option α
f : α → β
⊢ ⨆ x ∈ o.toFinset, f x = ⨆ x ∈ o, f x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
h : a ≤ b
⊢ ¬a ⩿ b ↔ ∃ c, a < c ∧ c < b

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ (∀ ⦃c : α⦄, a < c → ¬c < b) ↔ Ioo a b = ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
a : α
s : Finset α
t : α → β
⊢ ⨆ x ∈ insert a s, t x = t a ⊔ ⨆ x ∈ s, t x

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
f : γ → α
g : α → β
s : Finset γ
⊢ ⨆ x ∈ image f s, g x = ⨆ y ∈ s, g (f y)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α
f : α ↪o β
hab : a ⩿ b
h : (range ⇑f).OrdConnected
⊢ f a ⩿ f b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
x : α
t : Finset α
f : α → β
s : β
hx : x ∉ t
⊢ ⨆ i ∈ insert x t, update f x s i = s ⊔ ⨆ i ∈ t, f i

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
s : Finset γ
t : γ → Finset α
f : α → β
⊢ ⨆ y ∈ s.biUnion t, f y = ⨆ x ∈ s, ⨆ y ∈ t x, f y

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inr.refine_2
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range f)
⊢ ∀ w < sSup ∅, ∃ i, w < ⨆ (h : p i), f ⟨i, h⟩

Tactic:
· exact fun w hw ↦ ⟨i, hw.trans_eq (ciSup_neg hi).symm⟩

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

Goal state before:
pp: α : Type u_2
β : Type u_3
s : Finset α
f : α → Set β
x : α
h : x ∈ s
⊢ f x ⊆ ⋃ (_ : x ∈ s), f x

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = max (iSup f) (sSup ∅)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2 : a ≤ c
h3 : c ≤ b
⊢ c = a ∨ c = b

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
i : ι
⊢ range (Sigma.mk i) = Sigma.fst ⁻¹' {i}

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
i j : ι
h : i ≠ j
s : Set (α j)
⊢ Sigma.mk i ⁻¹' Sigma.mk j '' s = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
⊢ a ≤ c ∧ c ≤ b ↔ c = a ∨ c = b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ⩿ b
⊢ Icc a b = {a, b}

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι' → Type u_4
f : ι → ι'
hf : Function.Injective f
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
⊢ Sigma.mk i '' g i ⁻¹' s = Sigma.map f g ⁻¹' Sigma.mk (f i) '' s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ⩿ b
⊢ Ico a b ⊆ {a}

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
⊢ s.sigma t ⊆ u ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃a : α i⦄, a ∈ t i → ⟨i, a⟩ ∈ u

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ⩿ b
⊢ Ioc a b ⊆ {b}

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
p : (i : ι) × α i → Prop
⊢ (∀ x ∈ s.sigma t, p x) ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃a : α i⦄, a ∈ t i → p ⟨i, a⟩

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
p : (i : ι) × α i → Prop
⊢ (∃ x ∈ s.sigma t, p x) ↔ ∃ i ∈ s, ∃ a ∈ t i, p ⟨i, a⟩

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Nonempty ι
f : ι → α
n : α
⊢ ⨅ i, f i = n ↔ (∃ i, f i = n) ∧ ∀ (i : ι), n ≤ f i

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
⊢ (s.sigma fun i ↦ ∅) = ∅

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
t : (i : ι) → Set (α i)
⊢ ∅.sigma t = ∅

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
i : ι
⊢ (univ.sigma fun x ↦ univ) = univ

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
⊢ (s.sigma fun x ↦ univ) = Sigma.fst ⁻¹' s

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : IsEmpty ι
f : ι → α
⊢ ⨆ i, f i = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LT α
a b : α
h : a < b
⊢ ¬a ⋖ b ↔ ∃ c, a < c ∧ c < b

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ((i : ι) × α i)
⊢ (univ.sigma fun i ↦ Sigma.mk i ⁻¹' s) = s

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
t : (i : ι) → Set (α i)
i : ι
⊢ {i}.sigma t = Sigma.mk i '' t i

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
s : ι → α
a : α
h : BddAbove (range s)
⊢ a ≤ iSup s ↔ ∀ (b : α), (∀ (i : ι), s i ≤ b) → a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ ¬a ⋖ a

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
a : (i : ι) → α i
⊢ (s.sigma fun i ↦ {a i}) = (fun i ↦ ⟨i, a i⟩) '' s

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
i : ι
a : (i : ι) → α i
⊢ ({i}.sigma fun i ↦ {a i}) = {⟨i, a i⟩}

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
a : α
f : ι → α
h : BddAbove (range f)
⊢ a < iSup f ↔ ∃ i, a < f i

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t : (i : ι) → Set (α i)
⊢ (s₁ ∪ s₂).sigma t = s₁.sigma t ∪ s₂.sigma t

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ a ⩿ b ↔ a ⋖ b ∨ a = b

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
⊢ (s.sigma fun i ↦ t₁ i ∪ t₂ i) = s.sigma t₁ ∪ s.sigma t₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
a : α
h : a < ⨆ i, f i
⊢ ∃ i, a < f i

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
⊢ s₁.sigma t₁ ∩ s₂.sigma t₂ = (s₁ ∩ s₂).sigma fun i ↦ t₁ i ∩ t₂ i

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
p : ι → Prop
f : Exists p → α
⊢ ⨆ (ih : Exists p), f ih = ⨆ i, ⨆ (h : p i), f ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ⋖ b
⊢ Ico a b = {a}

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
β : Type u_4
inst✝ : CompleteLattice β
s : Set ι
t : (i : ι) → Set (α i)
f : Sigma α → β
x✝ : β
⊢ ⨆ ij ∈ s.sigma t, f ij ≤ x✝ → ⨆ i ∈ s, ⨆ j ∈ t i, f ⟨i, j⟩ ≤ x✝

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
β : Type u_4
inst✝ : CompleteLattice β
s : Set ι
t : (i : ι) → Set (α i)
f : Sigma α → β
x✝ : β
⊢ ⨆ i ∈ s, ⨆ j ∈ t i, f ⟨i, j⟩ ≤ x✝ → ⨆ ij ∈ s.sigma t, f ij ≤ x✝

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : Ico a b = {c}
⊢ a = c ∧ a ⋖ b

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
i : ι
⊢ (insert i s).sigma t = Sigma.mk i '' t i ∪ s.sigma t

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ Ico a b = {a} ↔ a ⋖ b

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
a : (i : ι) → α i
⊢ (s.sigma fun i ↦ insert (a i) (t i)) = (fun i ↦ ⟨i, a i⟩) '' s ∪ s.sigma t

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ⋖ b
⊢ Ioi a = Ici b

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
i : ι
hi : i ∈ s
⊢ Sigma.mk i ⁻¹' s.sigma t = t i

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
i : ι
hi : i ∉ s
⊢ Sigma.mk i ⁻¹' s.sigma t = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ⋖ b
⊢ Iio b = Iic a

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ Sigma.mk i ⁻¹' s.sigma t = if i ∈ s then t i else ∅

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
i : ι
β : Type u_7
inst✝ : DecidablePred fun x ↦ x ∈ s
g : β → α i
⊢ (fun b ↦ ⟨i, g b⟩) ⁻¹' s.sigma t = if i ∈ s then g ⁻¹' t i else ∅

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
β : ι → Type u_6
f : (i : ι) → α i → β i
⊢ ∀ (x : (i : ι) × β i), (x ∈ univ.sigma fun i ↦ range (f i)) ↔ x ∈ range fun x ↦ ⟨x.fst, f x.fst x.snd⟩

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
⊢ (¬∃ i ∈ s, (t i).Nonempty) ↔ ∀ i ∈ s, t i = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : Ioo a b = {c}
⊢ a ⋖ c ∧ c ⋖ b

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
γ : Type u_7
f : (i : ι) × α i → γ
⊢ f '' s.sigma t = ⋃ i ∈ s, f ∘ Sigma.mk i '' t i

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
⊢ ⨆ (h : p ∨ q), f h = max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
x✝ : a ⋖ c ∧ c ⋖ b
hac : a ⋖ c
hcb : c ⋖ b
⊢ Ioo a b = {c}

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : ConditionallyCompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
⊢ l (sSup s) = sSup (l '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : Ioi a = {b}
⊢ IsTop b ∧ a ⋖ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
x✝ : IsTop b ∧ a ⋖ b
hb : IsTop b
hab : a ⋖ b
⊢ Ioi a = {b}

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : α
⊢ x ⋖ y ↔ ∀ {z : α}, z ≤ x ↔ z < y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ ∃ a' > a, ∃ b' < b, ∀ x < a', ∀ y > b', x < y

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : Nonempty ι
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
hf : BddAbove (range f)
⊢ l (⨆ i, f i) = ⨆ i, l (f i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ⊢ ∀ {a b : Bool}, a ⩿ b ↔ a ≤ b

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
⊢ x ∈ s₁.sigma t₁ \ s₂.sigma t₂ ↔ x ∈ s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
⊢ s.sigma t = ⋃ i ∈ s, Sigma.mk i '' t i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ⊢ ∀ {a b : Bool}, a ⋖ b ↔ a < b

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
β : (i : ι) → α i → Type u_7
s : Set ι
t : (i : ι) → Set (α i)
u : (p : (i : ι) × α i) → Set (β p.fst p.snd)
⊢ Sigma.uncurry ⁻¹' (s.sigma t).pi u = s.pi fun i ↦ (t i).pi fun j ↦ u ⟨i, j⟩

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : ConditionallyCompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hf : BddAbove (f '' s)
hne : s.Nonempty
⊢ l (⨆ i, f ↑i) = ⨆ i, l (f ↑i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
x : α
s : Set α
⊢ s ⩿ insert x s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
s : Set α
a : α
⊢ s \ {a} ⩿ s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ (∃ a ∉ s, insert a s = t) → s ⋖ t

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ (∃ a ∈ t, t \ {a} = s) → s ⋖ t

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
⊢ (fun x1 x2 ↦ x1 ⩿ x2) = ReflGen fun x1 x2 ↦ x1 ⋖ x2

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
⊢ (TransGen fun x1 x2 ↦ x1 ⩿ x2) = ReflTransGen fun x1 x2 ↦ x1 ⋖ x2

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrderBot β
e : α ≃o β
f : ι → α
h✝ : Nonempty ι
hf : ¬BddAbove (range f)
⊢ ¬BddAbove (range fun i ↦ e (f i))

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
⊢ (ReflTransGen fun x1 x2 ↦ x1 ⩿ x2) = ReflTransGen fun x1 x2 ↦ x1 ⋖ x2

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrderBot β
e : α ≃o β
f : ι → α
h✝ : Nonempty ι
hf : ¬BddAbove (range f)
⊢ e (⨆ i, f i) = ⨆ i, e (f i)

Tactic:
have hfe : ¬ BddAbove (range fun i ↦ e (f i)) := by
      simpa [Set.Nonempty, BddAbove, upperBounds, e.surjective.forall] using hf

Goal state after:
case neg
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrderBot β
e : α ≃o β
f : ι → α
h✝ : Nonempty ι
hf : ¬BddAbove (range f)
hfe : ¬BddAbove (range fun i ↦ e (f i))
⊢ e (⨆ i, f i) = ⨆ i, e (f i)
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
x y : α × β
⊢ x ⩿ y → x.1 = y.1 ∨ x.2 = y.2

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrderBot β
e : α ≃o β
f : ι → α
⊢ e (⨆ i, f i) = ⨆ i, e (f i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b : β
⊢ (a₁, b) ⩿ (a₂, b) ↔ a₁ ⩿ a₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b : β
⊢ (a₁, b) ⋖ (a₂, b) ↔ a₁ ⋖ a₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a : α
b₁ b₂ : β
⊢ (a, b₁) ⋖ (a, b₂) ↔ b₁ ⋖ b₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ b₂ : β
⊢ (a₁, b₁) ⩿ (a₂, b₂) ↔ a₁ ⩿ a₂ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ b₂ : β
⊢ (a₁, b₁) ⋖ (a₂, b₂) ↔ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
x y : α × β
⊢ x ⩿ y ↔ x.1 ⩿ y.1 ∧ x.2 = y.2 ∨ x.2 ⩿ y.2 ∧ x.1 = y.1

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
x y : α × β
⊢ x ⋖ y ↔ x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ x.2 ⋖ y.2 ∧ x.1 = y.1

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⩿ b
i : ι
ci : α i
h₁ : a i < ci
h₂ : ci < b i
⊢ Function.update a i ci ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⩿ b
i : ι
ci : α i
h₁ : a i < ci
h₂ : ci < b i
hcb : Function.update a i ci ≤ b
⊢ a < Function.update a i ci

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⩿ b
i : ι
⊢ a i ⩿ b i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι), a x < c x → c ≤ b → ∀ (x : ι), ¬c x < b x
hab : a ≤ b
i : ι
hi : a i < b i
j : ι
hj : j ≠ i
c : (i : ι) → α i := Function.update a i (b i)
⊢ c ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ (x : α), ∃ y ∈ range f, x < y
a : WithTop α
ha : a < ⊤
i : ι
hi : a.untop ⋯ < f i
⊢ a < ↑(f i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι), a x < c x → c ≤ b → ∀ (x : ι), ¬c x < b x
hab : a ≤ b
i : ι
hi : a i < b i
j : ι
hj : j ≠ i
c : (i : ι) → α i := Function.update a i (b i)
h₁ : c ≤ b
⊢ a ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι), a x < c x → c ≤ b → ∀ (x : ι), ¬c x < b x
hab : a ≤ b
i : ι
hi : a i < b i
j : ι
hj : j ≠ i
c : (i : ι) → α i := Function.update a i (b i)
h₁ : c ≤ b
⊢ a i < c i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι), a x < c x → c ≤ b → ∀ (x : ι), ¬c x < b x
hab : a ≤ b
i : ι
hi : a i < b i
j : ι
hj : j ≠ i
c : (i : ι) → α i := Function.update a i (b i)
h₁ : c ≤ b
h₂ : ¬c j < b j
⊢ (fun x1 x2 ↦ x1 ≤ x2) (b j) (a j)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⋖ b
⊢ ∃ i, ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
⊢ ⨆ x, ↑(f x) = ⊤ ↔ ¬BddAbove (range f)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst✝ : Nonempty ι
h : a ⩿ b
⊢ ∃ i, ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)

Tactic:
by

Goal state after: