awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
rw : image2 f s t = image2 (fun (f : β → γ) (a : β) ↦ f a) (f '' s) t
rw₁ rw₂ : image2 f s t = image2 (fun (a : α) (b : β) ↦ f a b) s t
⊢ image2 f s t = (f '' s).seq t

Tactic:
rw [seq_eq_image2, image2_image_left]

Premises used: Set.image2_image_left, Set.seq_eq_image2
-- Module: Mathlib.Data.Set.Lattice
Goal:
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
x : γ
s : (i : ι) → κ i → Set γ
⊢ Membership.mem (γ := Set γ) (⋃ (i : ι), ⋃ (j : κ i), s i j) x ↔ ∃ (i : ι) (j : κ i), x ∈ s i j

Tactic:
simp_rw [mem_iUnion]

Premises used: Set.mem_iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
x : γ
s : (i : ι) → κ i → Set γ
⊢ Membership.mem (γ := Set γ) (⋂ (i : ι), ⋂ (j : κ i), s i j) x ↔ ∀ (i : ι) (j : κ i), x ∈ s i j

Tactic:
simp_rw [mem_iInter]

Premises used: Set.mem_iInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
s : ι → Set α
a : α
i : ι
ha : a ∈ s i
⊢ Membership.mem (γ := Set α) (⋃ (i : ι), s i) a

Tactic:
mem_iUnion.2 ⟨i, ha⟩

Premises used: Iff.mpr, Set.mem_iUnion, Exists.intro
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
a : α
i : ι
j : κ i
ha : a ∈ s i j
⊢ Membership.mem (γ := Set α) (⋃ (i : ι), ⋃ (j : κ i), s i j) a

Tactic:
mem_iUnion₂.2 ⟨i, j, ha⟩

Premises used: Iff.mpr, Set.mem_iUnion₂, Exists.intro
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
s : ι → Set α
a : α
h : ∀ (i : ι), a ∈ s i
⊢ Membership.mem (γ := Set α) (⋂ (i : ι), s i) a

Tactic:
mem_iInter.2 h

Premises used: Iff.mpr, Set.mem_iInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
a : α
h : ∀ (i : ι) (j : κ i), a ∈ s i j
⊢ Membership.mem (γ := Set α) (⋂ (i : ι), ⋂ (j : κ i), s i j) a

Tactic:
mem_iInter₂.2 h

Premises used: Iff.mpr, Set.mem_iInter₂
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
p q : Prop
f₁ : p → Set α
f₂ : q → Set α
pq : p ↔ q
f : ∀ (x : q), f₁ ⋯ = f₂ x
⊢ iUnion f₁ = iUnion f₂

Tactic:
iSup_congr_Prop pq f

Premises used: iSup_congr_Prop, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
p q : Prop
f₁ : p → Set α
f₂ : q → Set α
pq : p ↔ q
f : ∀ (x : q), f₁ ⋯ = f₂ x
⊢ iInter f₁ = iInter f₂

Tactic:
iInf_congr_Prop pq f

Premises used: Set.iInter, iInf_congr_Prop
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
f : PLift ι → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), f { down := i }) (⋃ (i : PLift ι), f i)

Tactic:
iSup_plift_up _

Premises used: iSup_plift_up, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
f : ι → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : PLift ι), f i.down) (⋃ (i : ι), f i)

Tactic:
iSup_plift_down _

Premises used: iSup_plift_down, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
f : PLift ι → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), f { down := i }) (⋂ (i : PLift ι), f i)

Tactic:
iInf_plift_up _

Premises used: Set.iInter, iInf_plift_up
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
f : ι → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (i : PLift ι), f i.down) (⋂ (i : ι), f i)

Tactic:
iInf_plift_down _

Premises used: Set.iInter, iInf_plift_down
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
p : Prop
inst : Decidable p
s : Set α
⊢ ⋃ (_ : p), s = if p then s else ∅

Tactic:
iSup_eq_if _

Premises used: iSup_eq_if, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
p : Prop
inst : Decidable p
s : p → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (h : p), s h) (if h : p then s h else ∅)

Tactic:
iSup_eq_dif _

Premises used: iSup_eq_dif, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
p : Prop
inst : Decidable p
s : Set α
⊢ ⋂ (_ : p), s = if p then s else univ

Tactic:
iInf_eq_if _

Premises used: Set.iInter, iInf_eq_if
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
p : Prop
inst : Decidable p
s : p → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (h : p), s h) (if h : p then s h else univ)

Tactic:
_root_.iInf_eq_dif _

Premises used: Set.iInter, iInf_eq_dif
-- Module: Mathlib.Data.Set.Lattice
Goal:
β : Type u_2
ι : Type u_12
t : Set ι
s : ι → Set β
w : Eq.{u_2 + 1} (α := Set β) (⋃ i ∈ t, s i) ⊤
x : β
⊢ Membership.mem (γ := Set β) ⊤ x

Tactic:
have p : x ∈ ⊤ := Set.mem_univ x
-- Module: Mathlib.Data.Set.Lattice
Goal:
β : Type u_2
ι : Type u_12
t : Set ι
s : ι → Set β
w : Eq.{u_2 + 1} (α := Set β) (⋃ i ∈ t, s i) ⊤
x : β
p : Membership.mem (γ := Set β) ⊤ x
⊢ ∃ (i : ι), Membership.mem (γ := Set β) (⋃ (_ : i ∈ t), s i) x

Tactic:
rw [← w, Set.mem_iUnion] at p

Premises used: Set.mem_iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
β : Type u_2
ι : Type u_12
t : Set ι
s : ι → Set β
w : Eq.{u_2 + 1} (α := Set β) (⋃ i ∈ t, s i) ⊤
x : β
p : ∃ (i : ι), Membership.mem (γ := Set β) (⋃ (_ : i ∈ t), s i) x
⊢ ∃ i ∈ t, x ∈ s i

Tactic:
simpa using p
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Type u_12
t : Set ι
s : ι → Set α
H : Nonempty α
w : Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ t, s i) ⊤
obtain : ∀ (x : ι) (m : x ∈ t), t.Nonempty
⊢ t.Nonempty

Tactic:
obtain ⟨x, m, -⟩ := exists_set_mem_of_union_eq_top t s w H.some

Premises used: Nonempty.some, Set.exists_set_mem_of_union_eq_top
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Type u_12
t : Set ι
s : ι → Set α
H : Nonempty α
w : Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ t, s i) ⊤
x : ι
m : x ∈ t
⊢ t.Nonempty

Tactic:
⟨x, m⟩

Premises used: Set.Nonempty, Exists.intro
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Type u_12
t : Set ι
s : ι → Set α
H : Nonempty α
w : Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ t, s i) ⊤
x : ι
m : x ∈ t
⊢ t.Nonempty

Tactic:
exact ⟨x, m⟩
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
s : ι → Set α
h_Union : Set.Nonempty.{u_1} (α := α) (⋃ (i : ι), s i)
obtain : ∀ (x : α) (hx : Membership.mem (γ := Set α) (⋃ (i : ι), s i) x), Nonempty ι
⊢ Nonempty ι

Tactic:
obtain ⟨x, hx⟩ := h_Union
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
s : ι → Set α
x : α
hx : Membership.mem (γ := Set α) (⋃ (i : ι), s i) x
⊢ Nonempty ι

Tactic:
⟨Classical.choose <| mem_iUnion.mp hx⟩

Premises used: Set.mem_iUnion, Nonempty.intro, Iff.mp, Classical.choose
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
s : ι → Set α
x : α
hx : Membership.mem (γ := Set α) (⋃ (i : ι), s i) x
⊢ Nonempty ι

Tactic:
exact ⟨Classical.choose <| mem_iUnion.mp hx⟩
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
s : ι → Set α
inst : Nonempty α
h_Union : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), s i) univ
⊢ Set.Nonempty.{u_1} (α := α) (⋃ (i : ι), s i)

Tactic:
simpa only [h_Union] using univ_nonempty

Premises used: Set.univ_nonempty
-- Module: Mathlib.Data.Set.Lattice
Goal:
β : Type u_2
ι : Sort u_5
p : ι → β → Prop
⊢ Eq.{u_2 + 1} (α := Set β) {x : β | ∃ (i : ι), p i x} (⋃ (i : ι), {x : β | p i x})

Tactic:
ext fun _ => .symm <| mem_iUnion

Premises used: Set.ext, Set.mem_iUnion, Iff.symm
-- Module: Mathlib.Data.Set.Lattice
Goal:
β : Type u_2
ι : Sort u_5
p : ι → β → Prop
⊢ Eq.{u_2 + 1} (α := Set β) {x : β | ∀ (i : ι), p i x} (⋂ (i : ι), {x : β | p i x})

Tactic:
ext fun _ => .symm <| mem_iInter

Premises used: Set.ext, Set.mem_iInter, Iff.symm
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
s : ι → Set α
t : Set α
h : ∀ (i : ι), s i ⊆ t
⊢ ⋃ (i : ι), s i ⊆ t

Tactic:
iSup_le h

Premises used: iSup_le, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
t : Set α
h : ∀ (i : ι) (j : κ i), s i j ⊆ t
⊢ ⋃ (i : ι), ⋃ (j : κ i), s i j ⊆ t

Tactic:
iUnion_subset fun x => iUnion_subset (h x)

Premises used: Set.iUnion_subset
-- Module: Mathlib.Data.Set.Lattice
Goal:
β : Type u_2
ι : Sort u_5
t : Set β
s : ι → Set β
h : ∀ (i : ι), t ⊆ s i
⊢ t ⊆ ⋂ (i : ι), s i

Tactic:
le_iInf h

Premises used: Set.iInter, le_iInf
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : Set α
t : (i : ι) → κ i → Set α
h : ∀ (i : ι) (j : κ i), s ⊆ t i j
⊢ s ⊆ ⋂ (i : ι), ⋂ (j : κ i), t i j

Tactic:
subset_iInter fun x => subset_iInter <| h x

Premises used: Set.subset_iInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
s : ι → Set α
t : Set α
⊢ ⋃ (i : ι), s i ⊆ t ↔ ∀ (i : ι), s i ⊆ t

Tactic:
⟨fun h _ => Subset.trans (le_iSup s _) h, iUnion_subset⟩

Premises used: Set.iUnion_subset, Set.Subset.trans, le_iSup, Iff.intro
-- 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_subset_iff]

Premises used: Set.iUnion_subset_iff
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
s : Set α
t : ι → Set α
⊢ s ⊆ ⋂ (i : ι), t i ↔ ∀ (i : ι), s ⊆ t i

Tactic:
le_iInf_iff

Premises used: Set.iInter, le_iInf_iff
-- 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 [subset_iInter_iff]

Premises used: Set.subset_iInter_iff
-- Module: Mathlib.Data.Set.Lattice
Goal:
β : Type u_2
ι : Sort u_5
⊢ ∀ (s : ι → Set β) (i : ι), s i ⊆ ⋃ (i : ι), s i

Tactic:
le_iSup

Premises used: le_iSup, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
β : Type u_2
ι : Sort u_5
⊢ ∀ (s : ι → Set β) (i : ι), ⋂ (i : ι), s i ⊆ s i

Tactic:
iInf_le

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

Tactic:
iInf_le_iSup

Premises used: Set.iInter, iInf_le_iSup, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
i : ι
j : κ i
⊢ s i j ⊆ ⋃ (i' : ι), ⋃ (j' : κ i'), s i' j'

Tactic:
le_iSup₂ i j

Premises used: le_iSup₂, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
i : ι
j : κ i
⊢ ⋂ (i : ι), ⋂ (j : κ i), s i j ⊆ s i j

Tactic:
iInf₂_le i j

Premises used: Set.iInter, iInf₂_le
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
s : Set α
t : ι → Set α
i : ι
h : s ⊆ t i
⊢ s ⊆ ⋃ (i : ι), t i

Tactic:
le_iSup_of_le i h

Premises used: le_iSup_of_le, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
s : ι → Set α
t : Set α
i : ι
h : s i ⊆ t
⊢ ⋂ (i : ι), s i ⊆ t

Tactic:
iInf_le_of_le i h

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

Tactic:
le_iSup₂_of_le i j h

Premises used: le_iSup₂_of_le, Set.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
h : s i j ⊆ t
⊢ ⋂ (i : ι), ⋂ (j : κ i), s i j ⊆ t

Tactic:
iInf₂_le_of_le i j h

Premises used: Set.iInter, iInf₂_le_of_le
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
s t : ι → Set α
h : ∀ (i : ι), s i ⊆ t i
⊢ Subset.{u_1} (α := Set α) (⋃ (i : ι), s i) (⋃ (i : ι), t i)

Tactic:
iSup_mono h

Premises used: Set.iUnion, iSup_mono
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
s t : ι → Set α
h : ∀ (i : ι), s i ⊆ t i
⊢ iUnion s ⊆ iUnion t

Tactic:
iSup_mono h

Premises used: Set.iUnion, iSup_mono
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s t : (i : ι) → κ i → Set α
h : ∀ (i : ι) (j : κ i), s i j ⊆ t i j
⊢ Subset.{u_1} (α := Set α) (⋃ (i : ι), ⋃ (j : κ i), s i j) (⋃ (i : ι), ⋃ (j : κ i), t i j)

Tactic:
iSup₂_mono h

Premises used: iSup₂_mono, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
s t : ι → Set α
h : ∀ (i : ι), s i ⊆ t i
⊢ Subset.{u_1} (α := Set α) (⋂ (i : ι), s i) (⋂ (i : ι), t i)

Tactic:
iInf_mono h

Premises used: Set.iInter, iInf_mono
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
s t : ι → Set α
h : ∀ (i : ι), s i ⊆ t i
⊢ iInter s ⊆ iInter t

Tactic:
iInf_mono h

Premises used: Set.iInter, iInf_mono
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s t : (i : ι) → κ i → Set α
h : ∀ (i : ι) (j : κ i), s i j ⊆ t i j
⊢ Subset.{u_1} (α := Set α) (⋂ (i : ι), ⋂ (j : κ i), s i j) (⋂ (i : ι), ⋂ (j : κ i), t i j)

Tactic:
iInf₂_mono h

Premises used: Set.iInter, iInf₂_mono
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
ι₂ : Sort u_7
s : ι → Set α
t : ι₂ → Set α
h : ∀ (i : ι), ∃ (j : ι₂), s i ⊆ t j
⊢ Subset.{u_1} (α := Set α) (⋃ (i : ι), s i) (⋃ (i : ι₂), t i)

Tactic:
iSup_mono' h

Premises used: iSup_mono', 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 → Set α
t : (i' : ι') → κ' i' → Set α
h : ∀ (i : ι) (j : κ i), ∃ (i' : ι') (j' : κ' i'), s i j ⊆ t i' j'
⊢ Subset.{u_1} (α := Set α) (⋃ (i : ι), ⋃ (j : κ i), s i j) (⋃ (i' : ι'), ⋃ (j' : κ' i'), t i' j')

Tactic:
iSup₂_mono' h

Premises used: iSup₂_mono', Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
ι' : Sort u_6
s : ι → Set α
t : ι' → Set α
h : ∀ (j : ι'), ∃ (i : ι), s i ⊆ t j
⊢ Subset.{u_1} (α := Set α) (⋂ (i : ι), s i) (⋂ (j : ι'), t j)

Tactic:
Set.subset_iInter fun j =>
    let ⟨i, hi⟩ := h j
    iInter_subset_of_subset i hi

Premises used: Set.iInter, Set.subset_iInter, HasSubset.Subset, _private.0.Set.iInter_mono'.match_1, Set.iInter_subset_of_subset
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_8
κ' : ι' → Sort u_11
s : (i : ι) → κ i → Set α
t : (i' : ι') → κ' i' → Set α
h : ∀ (i' : ι') (j' : κ' i'), ∃ (i : ι) (j : κ i), s i j ⊆ t i' j'
⊢ Subset.{u_1} (α := Set α) (⋂ (i : ι), ⋂ (j : κ i), s i j) (⋂ (i' : ι'), ⋂ (j' : κ' i'), t i' j')

Tactic:
subset_iInter₂_iff.2 fun i' j' =>
    let ⟨_, _, hst⟩ := h i' j'
    (iInter₂_subset _ _).trans hst

Premises used: Iff.mpr, Set.iInter, Set.iInter₂_subset, _private.0.Set.iInter₂_mono'.match_1, Set.subset_iInter₂_iff, HasSubset.Subset.trans, HasSubset.Subset
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_12
s : ι → Set α
⊢ Subset.{u_1} (α := Set α) (⋃ (i : ι), ⋃ (x : κ i), s i) (⋃ (i : ι), s i)

Tactic:
iUnion_mono fun _ => iUnion_subset fun _ => Subset.rfl

Premises used: Set.iUnion_subset, Set.Subset.rfl, Set.iUnion_mono
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_12
s : ι → Set α
⊢ Subset.{u_1} (α := Set α) (⋂ (i : ι), s i) (⋂ (i : ι), ⋂ (x : κ i), s i)

Tactic:
iInter_mono fun _ => subset_iInter fun _ => Subset.rfl

Premises used: Set.subset_iInter, Set.Subset.rfl, Set.iInter_mono
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
P : ι → α → Prop
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) (⋃ (i : ι), {x : α | P i x}) x ↔
      Membership.mem (γ := Set α) {x : α | ∃ (i : ι), P i x} x
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), {x : α | P i x}) {x : α | ∃ (i : ι), P i x}

Tactic:
ext
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
P : ι → α → Prop
x : α
⊢ Membership.mem (γ := Set α) (⋃ (i : ι), {x : α | P i x}) x ↔ Membership.mem (γ := Set α) {x : α | ∃ (i : ι), P i x} x

Tactic:
mem_iUnion

Premises used: Set.Mem, setOf, Set.mem_iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
P : ι → α → Prop
x : α
⊢ Membership.mem (γ := Set α) (⋃ (i : ι), {x : α | P i x}) x ↔ Membership.mem (γ := Set α) {x : α | ∃ (i : ι), P i x} x

Tactic:
exact mem_iUnion

Premises used: Set.mem_iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
P : ι → α → Prop
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) (⋂ (i : ι), {x : α | P i x}) x ↔
      Membership.mem (γ := Set α) {x : α | ∀ (i : ι), P i x} x
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), {x : α | P i x}) {x : α | ∀ (i : ι), P i x}

Tactic:
ext
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
P : ι → α → Prop
x : α
⊢ Membership.mem (γ := Set α) (⋂ (i : ι), {x : α | P i x}) x ↔ Membership.mem (γ := Set α) {x : α | ∀ (i : ι), P i x} x

Tactic:
mem_iInter

Premises used: Set.Mem, setOf, Set.mem_iInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
P : ι → α → Prop
x : α
⊢ Membership.mem (γ := Set α) (⋂ (i : ι), {x : α | P i x}) x ↔ Membership.mem (γ := Set α) {x : α | ∀ (i : ι), P i x} x

Tactic:
exact mem_iInter

Premises used: Set.mem_iInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
ι₂ : Sort u_7
f : ι → Set α
g : ι₂ → Set α
h : ι → ι₂
h1 : Surjective h
h2 : ∀ (x : ι), g (h x) = f x
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (x : ι), f x) (⋃ (y : ι₂), g y)

Tactic:
h1.iSup_congr h h2

Premises used: Function.Surjective.iSup_congr, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
ι₂ : Sort u_7
f : ι → Set α
g : ι₂ → Set α
h : ι → ι₂
h1 : Surjective h
h2 : ∀ (x : ι), g (h x) = f x
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (x : ι), f x) (⋂ (y : ι₂), g y)

Tactic:
h1.iInf_congr h h2

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

Tactic:
iSup_congr h

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

Tactic:
iInf_congr h

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

Tactic:
iUnion_congr fun i => iUnion_congr <| h i

Premises used: Set.iUnion_congr
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s t : (i : ι) → κ i → Set α
h : ∀ (i : ι) (j : κ i), s i j = t i j
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), ⋂ (j : κ i), s i j) (⋂ (i : ι), ⋂ (j : κ i), t i j)

Tactic:
iInter_congr fun i => iInter_congr <| h i

Premises used: Set.iInter_congr
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set β
t : Set γ
f : β → γ
g : γ → Set α
hf : BijOn f s t
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ x ∈ s, g (f x)) (⋃ y ∈ t, g y)

Tactic:
hf.iSup_comp g

Premises used: Set.BijOn.iSup_comp, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set β
t : Set γ
f : β → γ
g : γ → Set α
hf : BijOn f s t
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ x ∈ s, g (f x)) (⋂ y ∈ t, g y)

Tactic:
hf.iInf_comp g

Premises used: Set.BijOn.iInf_comp, Set.iInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set β
t : Set γ
f : β → Set α
g : γ → Set α
h : β → γ
h1 : BijOn h s t
h2 : ∀ (x : β), g (h x) = f x
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ x ∈ s, f x) (⋃ y ∈ t, g y)

Tactic:
h1.iSup_congr f g h2

Premises used: Set.BijOn.iSup_congr, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set β
t : Set γ
f : β → Set α
g : γ → Set α
h : β → γ
h1 : BijOn h s t
h2 : ∀ (x : β), g (h x) = f x
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ x ∈ s, f x) (⋂ y ∈ t, g y)

Tactic:
h1.iInf_congr f g h2

Premises used: Set.iInter, Set.BijOn.iInf_congr
-- Module: Mathlib.Data.Set.Lattice
Goal:
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
s : Set β
⊢ ⋃ (x : ι), s = s

Tactic:
iSup_const

Premises used: iSup_const, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
s : Set β
⊢ ⋂ (x : ι), s = s

Tactic:
iInf_const

Premises used: Set.iInter, iInf_const
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
inst : Nonempty ι
f : ι → Set α
s : Set α
hf : ∀ (i : ι), f i = s
⊢ ⋃ (i : ι), f i = s

Tactic:
(iUnion_congr hf).trans <| iUnion_const _

Premises used: Set.iUnion_const, Set.iUnion_congr, Eq.trans
-- Module: Mathlib.Data.Set.Lattice
Goal:
α : Type u_1
ι : Sort u_5
inst : Nonempty ι
f : ι → Set α
s : Set α
hf : ∀ (i : ι), f i = s
⊢ ⋂ (i : ι), f i = s

Tactic:
(iInter_congr hf).trans <| iInter_const _

Premises used: Set.iInter_const, Set.iInter_congr, Eq.trans
-- Module: Mathlib.Data.Set.Lattice
Goal:
β : Type u_2
ι : Sort u_5
s : ι → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋃ (i : ι), s i)ᶜ (⋂ (i : ι), (s i)ᶜ)

Tactic:
compl_iSup

Premises used: Set.Mem, Set.iInter, setOf, compl_iSup, Set.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)ᶜ (⋂ (i : ι), ⋂ (j : κ i), (s i j)ᶜ)

Tactic:
simp_rw [compl_iUnion]

Premises used: Set.compl_iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
β : Type u_2
ι : Sort u_5
s : ι → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋂ (i : ι), s i)ᶜ (⋃ (i : ι), (s i)ᶜ)

Tactic:
compl_iInf

Premises used: Set.Mem, Set.iInter, setOf, compl_iInf, Set.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)ᶜ (⋃ (i : ι), ⋃ (j : κ i), (s i j)ᶜ)

Tactic:
simp_rw [compl_iInter]

Premises used: Set.compl_iInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
β : Type u_2
ι : Sort u_5
s : ι → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋃ (i : ι), s i) (⋂ (i : ι), (s i)ᶜ)ᶜ

Tactic:
simp only [compl_iInter, compl_compl]

Premises used: Set.compl_iInter, compl_compl
-- Module: Mathlib.Data.Set.Lattice
Goal:
β : Type u_2
ι : Sort u_5
s : ι → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋂ (i : ι), s i) (⋃ (i : ι), (s i)ᶜ)ᶜ

Tactic:
simp only [compl_iUnion, compl_compl]

Premises used: compl_compl, Set.compl_iUnion
-- 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:
inf_iSup_eq _ _

Premises used: inf_iSup_eq, Set.iUnion
-- 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:
iSup_inf_eq _ _

Premises used: iSup_inf_eq, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
β : Type u_2
ι : Sort u_5
s t : ι → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋃ (i : ι), s i ∪ t i) ((⋃ (i : ι), s i) ∪ ⋃ (i : ι), t i)

Tactic:
iSup_sup_eq

Premises used: iSup_sup_eq, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice
Goal:
β : Type u_2
ι : Sort u_5
s t : ι → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋂ (i : ι), s i ∩ t i) ((⋂ (i : ι), s i) ∩ ⋂ (i : ι), t i)

Tactic:
iInf_inf_eq

Premises used: Set.iInter, iInf_inf_eq
-- 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:
sup_iSup

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

Tactic:
iSup_sup

Premises used: iSup_sup, Set.iUnion
-- 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:
inf_iInf

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

Tactic:
iInf_inf

Premises used: iInf_inf, Set.iInter
-- Module: Mathlib.Data.Set.Lattice
Goal:
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
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, iUnion_union]

Premises used: Set.iUnion_union, Set.union_singleton
-- 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:
sup_iInf_eq _ _

Premises used: Set.iInter, sup_iInf_eq