awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
p : ι → Prop
s : (i : ι) → p i → Set α
hp : ∃ (i : ι), p i
f : α → β
h : InjOn f (⋃ (i : ι), ⋃ (hi : p i), s i hi)
this : Nonempty.{max 1 u_5} { i : ι // p i }
⊢ InjOn f (⋃ (i : Subtype p), s (↑i : ι) ⋯)

Tactic:
simpa only [iUnion, iSup_subtype'] using h

Premises used: iSup_subtype', Set.iUnion
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
hf : Bijective f
s : ι → Set α
inl : IsEmpty ι → f '' ⋂ (i : ι), s i = ⋂ (i : ι), f '' s i
inr : Nonempty ι → f '' ⋂ (i : ι), s i = ⋂ (i : ι), f '' s i
⊢ f '' ⋂ (i : ι), s i = ⋂ (i : ι), f '' s i

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
hf : Bijective f
s : ι → Set α
h : IsEmpty ι
inl : f '' univ = univ
⊢ f '' ⋂ (i : ι), s i = ⋂ (i : ι), f '' s i

Tactic:
simp_rw [iInter_of_empty, image_univ_of_surjective hf.surjective]

Premises used: Set.iInter_of_empty, Set.image_univ_of_surjective, Function.Bijective.surjective
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
hf : Bijective f
s : ι → Set α
h : Nonempty ι
⊢ f '' ⋂ (i : ι), s i = ⋂ (i : ι), f '' s i

Tactic:
hf.injective.injOn.image_iInter_eq

Premises used: Function.Injective.injOn, Set.InjOn.image_iInter_eq, Function.Bijective.injective
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
hf : Bijective f
s : ι → Set α
h : Nonempty ι
⊢ f '' ⋂ (i : ι), s i = ⋂ (i : ι), f '' s i

Tactic:
exact hf.injective.injOn.image_iInter_eq

Premises used: Function.Injective.injOn, Set.InjOn.image_iInter_eq, Function.Bijective.injective
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
f : α → β
hf : Bijective f
s : (i : ι) → κ i → Set α
⊢ f '' ⋂ (i : ι), ⋂ (j : κ i), s i j = ⋂ (i : ι), ⋂ (j : κ i), f '' s i j

Tactic:
simp_rw [image_iInter hf]

Premises used: Set.image_iInter
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
hs : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx : Membership.mem (γ := Set α) (⋃ (i : ι), s i) x
y : α
hy : Membership.mem (γ := Set α) (⋃ (i : ι), s i) y
hxy : f x = f y
rcases : ∀ (i : ι) (hx : x ∈ s i), x = y
⊢ x = y

Tactic:
rcases mem_iUnion.1 hx with ⟨i, hx⟩

Premises used: Set.mem_iUnion, Iff.mp
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
hs : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx_1 : Membership.mem (γ := Set α) (⋃ (i : ι), s i) x
y : α
hy : Membership.mem (γ := Set α) (⋃ (i : ι), s i) y
hxy : f x = f y
i : ι
hx : x ∈ s i
rcases : ∀ (j : ι) (hy : y ∈ s j), x = y
⊢ x = y

Tactic:
rcases mem_iUnion.1 hy with ⟨j, hy⟩

Premises used: Set.mem_iUnion, Iff.mp
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
hs : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx_1 : Membership.mem (γ := Set α) (⋃ (i : ι), s i) x
y : α
hy_1 : Membership.mem (γ := Set α) (⋃ (i : ι), s i) y
hxy : f x = f y
i : ι
hx : x ∈ s i
j : ι
hy : y ∈ s j
rcases : ∀ (k : ι) (hi : s i ⊆ s k) (hj : s j ⊆ s k), x = y
⊢ x = y

Tactic:
rcases hs i j with ⟨k, hi, hj⟩
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
hs : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx_1 : Membership.mem (γ := Set α) (⋃ (i : ι), s i) x
y : α
hy_1 : Membership.mem (γ := Set α) (⋃ (i : ι), s i) y
hxy : f x = f y
i : ι
hx : x ∈ s i
j : ι
hy : y ∈ s j
k : ι
hi : s i ⊆ s k
hj : s j ⊆ s k
⊢ x = y

Tactic:
hf k (hi hx) (hj hy) hxy
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
hs : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx_1 : Membership.mem (γ := Set α) (⋃ (i : ι), s i) x
y : α
hy_1 : Membership.mem (γ := Set α) (⋃ (i : ι), s i) y
hxy : f x = f y
i : ι
hx : x ∈ s i
j : ι
hy : y ∈ s j
k : ι
hi : s i ⊆ s k
hj : s j ⊆ s k
⊢ x = y

Tactic:
exact hf k (hi hx) (hj hy) hxy
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
s : Set α
T : Set (Set β)
f : α → β
H : ∀ t ∈ T, SurjOn f s t
⊢ SurjOn f s (⋃₀ T)

Tactic:
fun _ ⟨t, ht, hx⟩ => H t ht hx

Premises used: _private.0.Set.surjOn_sUnion.match_1, Set.SurjOn, Membership.mem, Set.Subset, Set.image
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : Set α
t : ι → Set β
f : α → β
H : ∀ (i : ι), SurjOn f s (t i)
⊢ SurjOn f s (⋃ (i : ι), t i)

Tactic:
surjOn_sUnion <| forall_mem_range.2 H

Premises used: Iff.mpr, Set.forall_mem_range, iSup, Set.surjOn_sUnion, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
t : ι → Set β
f : α → β
H : ∀ (i : ι), SurjOn f (s i) (t i)
⊢ SurjOn f (⋃ (i : ι), s i) (⋃ (i : ι), t i)

Tactic:
surjOn_iUnion fun i => (H i).mono (subset_iUnion _ _) (Subset.refl _)

Premises used: Set.surjOn_iUnion, Set.Subset.refl, Set.SurjOn.mono, Set.subset_iUnion
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
s : Set α
t : (i : ι) → κ i → Set β
f : α → β
H : ∀ (i : ι) (j : κ i), SurjOn f s (t i j)
⊢ SurjOn f s (⋃ (i : ι), ⋃ (j : κ i), t i j)

Tactic:
surjOn_iUnion fun i => surjOn_iUnion (H i)

Premises used: Set.surjOn_iUnion
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
t : (i : ι) → κ i → Set β
f : α → β
H : ∀ (i : ι) (j : κ i), SurjOn f (s i j) (t i j)
⊢ SurjOn f (⋃ (i : ι), ⋃ (j : κ i), s i j) (⋃ (i : ι), ⋃ (j : κ i), t i j)

Tactic:
surjOn_iUnion_iUnion fun i => surjOn_iUnion_iUnion (H i)

Premises used: Set.surjOn_iUnion_iUnion
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
s : ι → Set α
t : Set β
f : α → β
H : ∀ (i : ι), SurjOn f (s i) t
Hinj : InjOn f (⋃ (i : ι), s i)
y : β
hy : y ∈ t
rw : ∀ (i : ι), y ∈ f '' s i
⊢ y ∈ f '' ⋂ (i : ι), s i

Tactic:
rw [Hinj.image_iInter_eq, mem_iInter]

Premises used: Set.InjOn.image_iInter_eq, Set.mem_iInter
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
s : ι → Set α
t : Set β
f : α → β
H : ∀ (i : ι), SurjOn f (s i) t
Hinj : InjOn f (⋃ (i : ι), s i)
y : β
hy : y ∈ t
⊢ ∀ (i : ι), y ∈ f '' s i

Tactic:
fun i => H i hy
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
s : ι → Set α
t : Set β
f : α → β
H : ∀ (i : ι), SurjOn f (s i) t
Hinj : InjOn f (⋃ (i : ι), s i)
y : β
hy : y ∈ t
⊢ ∀ (i : ι), y ∈ f '' s i

Tactic:
exact fun i => H i hy
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
s : ι → Set α
t : ι → Set β
f : α → β
H : ∀ (i : ι), SurjOn f (s i) (t i)
Hinj : InjOn f (⋃ (i : ι), s i)
⊢ SurjOn f (⋂ (i : ι), s i) (⋂ (i : ι), t i)

Tactic:
surjOn_iInter (fun i => (H i).mono (Subset.refl _) (iInter_subset _ _)) Hinj

Premises used: Set.Subset.refl, Set.SurjOn.mono, Set.surjOn_iInter, Set.iInter_subset
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
t : ι → Set β
f : α → β
H : ∀ (i : ι), BijOn f (s i) (t i)
Hinj : InjOn f (⋃ (i : ι), s i)
⊢ BijOn f (⋃ (i : ι), s i) (⋃ (i : ι), t i)

Tactic:
⟨mapsTo_iUnion_iUnion fun i => (H i).mapsTo, Hinj, surjOn_iUnion_iUnion fun i => (H i).surjOn⟩

Premises used: Set.BijOn.surjOn, And.intro, Set.BijOn, Set.BijOn.mapsTo, Set.mapsTo_iUnion_iUnion, Set.surjOn_iUnion_iUnion
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
hi : Nonempty ι
s : ι → Set α
t : ι → Set β
f : α → β
H : ∀ (i : ι), BijOn f (s i) (t i)
Hinj : InjOn f (⋃ (i : ι), s i)
⊢ BijOn f (⋂ (i : ι), s i) (⋂ (i : ι), t i)

Tactic:
⟨mapsTo_iInter_iInter fun i => (H i).mapsTo,
    hi.elim fun i => (H i).injOn.mono (iInter_subset _ _),
    surjOn_iInter_iInter (fun i => (H i).surjOn) Hinj⟩

Premises used: Set.surjOn_iInter_iInter, Set.mapsTo_iInter_iInter, Nonempty.elim, Set.BijOn.injOn, Set.BijOn.surjOn, And.intro, Set.BijOn, Set.BijOn.mapsTo, Set.InjOn.mono, Set.iInter_subset
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
hs : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
t : ι → Set β
f : α → β
H : ∀ (i : ι), BijOn f (s i) (t i)
⊢ BijOn f (⋃ (i : ι), s i) (⋃ (i : ι), t i)

Tactic:
bijOn_iUnion H <| inj_on_iUnion_of_directed hs fun i => (H i).injOn

Premises used: Set.bijOn_iUnion, Set.BijOn.injOn, Set.inj_on_iUnion_of_directed
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
s : ι → Set α
hs : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
t : ι → Set β
f : α → β
H : ∀ (i : ι), BijOn f (s i) (t i)
⊢ BijOn f (⋂ (i : ι), s i) (⋂ (i : ι), t i)

Tactic:
bijOn_iInter H <| inj_on_iUnion_of_directed hs fun i => (H i).injOn

Premises used: Set.BijOn.injOn, Set.bijOn_iInter, Set.inj_on_iUnion_of_directed
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
s : ι → Set α
h : ∀ (x : β), x ∈ f '' ⋃ (i : ι), s i ↔ Membership.mem (γ := Set β) (⋃ (i : ι), f '' s i) x
⊢ f '' ⋃ (i : ι), s i = ⋃ (i : ι), f '' s i

Tactic:
ext1 x
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
s : ι → Set α
x : β
⊢ x ∈ f '' ⋃ (i : ι), s i ↔ Membership.mem (γ := Set β) (⋃ (i : ι), f '' s i) x

Tactic:
simp only [mem_image, mem_iUnion, ← exists_and_right, exists_comm (α := α)]

Premises used: Set.mem_iUnion, Set.mem_image, exists_and_right, exists_comm
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
f : α → β
s : (i : ι) → κ i → Set α
⊢ f '' ⋃ (i : ι), ⋃ (j : κ i), s i j = ⋃ (i : ι), ⋃ (j : κ i), f '' s i j

Tactic:
simp_rw [image_iUnion]

Premises used: Set.image_iUnion
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
p : α → Prop
x_1 : Subtype p
x : α
h : p x
⊢ Membership.mem (γ := Set (Subtype p)) univ (Subtype.mk (p := p) x h) ↔
    Membership.mem (γ := Set (Subtype p)) (⋃ (x : α), ⋃ (h : p x), {Subtype.mk (p := p) x h}) (Subtype.mk (p := p) x h)

Tactic:
simp [h]
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
ι : Sort u_9
f : ι → α
a : α
⊢ a ∈ range f ↔ Membership.mem (γ := Set α) (⋃ (i : ι), {f i}) a

Tactic:
simp [@eq_comm α a]

Premises used: eq_comm
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
b : β
⊢ b ∈ f '' s ↔ Membership.mem (γ := Set β) (⋃ i ∈ s, {f i}) b

Tactic:
simp [@eq_comm β b]

Premises used: eq_comm
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : ι → α
g : α → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋃ x ∈ range f, g x) (⋃ (y : ι), g (f y))

Tactic:
iSup_range

Premises used: iSup_range, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : ι → α
g : α → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋃ (x : α), ⋃ (y : ι), ⋃ (_ : f y = x), g x) (⋃ (y : ι), g (f y))

Tactic:
simpa using biUnion_range

Premises used: Set.biUnion_range
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : ι → α
g : α → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋂ x ∈ range f, g x) (⋂ (y : ι), g (f y))

Tactic:
iInf_range

Premises used: Set.iInter, iInf_range
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : ι → α
g : α → Set β
⊢ Eq.{u_2 + 1} (α := Set β) (⋂ (x : α), ⋂ (y : ι), ⋂ (_ : f y = x), g x) (⋂ (y : ι), g (f y))

Tactic:
simpa using biInter_range

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

Tactic:
iSup_image

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

Tactic:
iInf_image

Premises used: Set.iInter, iInf_image
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f : α → β → γ
g : γ → Set δ
⊢ Eq.{u_4 + 1} (α := Set δ) (⋃ c ∈ image2 f s t, g c) (⋃ a ∈ s, ⋃ b ∈ t, g (f a b))

Tactic:
iSup_image2 ..

Premises used: iSup_image2, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f : α → β → γ
g : γ → Set δ
⊢ Eq.{u_4 + 1} (α := Set δ) (⋂ c ∈ image2 f s t, g c) (⋂ a ∈ s, ⋂ b ∈ t, g (f a b))

Tactic:
iInf_image2 ..

Premises used: Set.iInter, iInf_image2
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
ι : Sort u_9
κ : Sort u_10
f : ι → Set α
g : κ → Set α
simp_rw : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), f i ∩ ⋃ (j : κ), g j) (⋃ (i : ι), ⋃ (j : κ), f i ∩ g j)
⊢ Eq.{u_1 + 1} (α := Set α) ((⋃ (i : ι), f i) ∩ ⋃ (j : κ), g j) (⋃ (i : ι), ⋃ (j : κ), f i ∩ g j)

Tactic:
simp_rw [iUnion_inter, inter_iUnion]

Premises used: Set.iUnion_inter, Set.inter_iUnion
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
ι : Sort u_9
κ : Sort u_10
f : ι → Set α
g : κ → Set α
simp_rw : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), f i ∪ ⋂ (j : κ), g j) (⋂ (i : ι), ⋂ (j : κ), f i ∪ g j)
⊢ Eq.{u_1 + 1} (α := Set α) ((⋂ (i : ι), f i) ∪ ⋂ (j : κ), g j) (⋂ (i : ι), ⋂ (j : κ), f i ∪ g j)

Tactic:
simp_rw [iInter_union, union_iInter]

Premises used: Set.union_iInter, Set.iInter_union
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
ι₁ : Sort u_9
κ₁ : Sort u_10
ι₂ : ι₁ → Sort u_11
k₂ : κ₁ → Sort u_12
f : (i₁ : ι₁) → ι₂ i₁ → Set α
g : (j₁ : κ₁) → k₂ j₁ → Set α
simp_rw :
  Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι₁), ⋃ (i_1 : ι₂ i), f i i_1 ∩ ⋃ (j₁ : κ₁), ⋃ (j₂ : k₂ j₁), g j₁ j₂)
    (⋃ (i₁ : ι₁), ⋃ (i₂ : ι₂ i₁), ⋃ (j₁ : κ₁), ⋃ (j₂ : k₂ j₁), f i₁ i₂ ∩ g j₁ j₂)
⊢ Eq.{u_1 + 1} (α := Set α) ((⋃ (i₁ : ι₁), ⋃ (i₂ : ι₂ i₁), f i₁ i₂) ∩ ⋃ (j₁ : κ₁), ⋃ (j₂ : k₂ j₁), g j₁ j₂)
    (⋃ (i₁ : ι₁), ⋃ (i₂ : ι₂ i₁), ⋃ (j₁ : κ₁), ⋃ (j₂ : k₂ j₁), f i₁ i₂ ∩ g j₁ j₂)

Tactic:
simp_rw [iUnion_inter, inter_iUnion]

Premises used: Set.iUnion_inter, Set.inter_iUnion
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
ι₁ : Sort u_9
κ₁ : Sort u_10
ι₂ : ι₁ → Sort u_11
k₂ : κ₁ → Sort u_12
f : (i₁ : ι₁) → ι₂ i₁ → Set α
g : (j₁ : κ₁) → k₂ j₁ → Set α
simp_rw :
  Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι₁), ⋂ (i_1 : ι₂ i), f i i_1 ∪ ⋂ (j₁ : κ₁), ⋂ (j₂ : k₂ j₁), g j₁ j₂)
    (⋂ (i₁ : ι₁), ⋂ (i₂ : ι₂ i₁), ⋂ (j₁ : κ₁), ⋂ (j₂ : k₂ j₁), f i₁ i₂ ∪ g j₁ j₂)
⊢ Eq.{u_1 + 1} (α := Set α) ((⋂ (i₁ : ι₁), ⋂ (i₂ : ι₂ i₁), f i₁ i₂) ∪ ⋂ (j₁ : κ₁), ⋂ (j₂ : k₂ j₁), g j₁ j₂)
    (⋂ (i₁ : ι₁), ⋂ (i₂ : ι₂ i₁), ⋂ (j₁ : κ₁), ⋂ (j₂ : k₂ j₁), f i₁ i₂ ∪ g j₁ j₂)

Tactic:
simp_rw [iInter_union, union_iInter]

Premises used: Set.union_iInter, Set.iInter_union
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
ι : Type u_9
f : ι → Set α
h : Pairwise (Disjoint on f)
s t : Set ι
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ s ∩ t, f i) ((⋃ i ∈ s, f i) ∩ ⋃ i ∈ t, f i)

Tactic:
biSup_inter_of_pairwise_disjoint h s t

Premises used: Set.iUnion, biSup_inter_of_pairwise_disjoint
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
ι : Type u_9
κ : Type u_10
hκ : Nonempty κ
f : ι → Set α
h : Pairwise (Disjoint on f)
s : κ → Set ι
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) (⋂ (j : κ), s j) i), f i)
    (⋂ (j : κ), ⋃ i ∈ s j, f i)

Tactic:
biSup_iInter_of_pairwise_disjoint h s

Premises used: Set.iInter, biSup_iInter_of_pairwise_disjoint, Set.iUnion
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ Monotone (preimage f)

Tactic:
fun _ _ h => preimage_mono h

Premises used: Monotone, Set.preimage_mono
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
s : ι → Set β
⊢ ∀ (x : α), x ∈ f ⁻¹' ⋃ (i : ι), s i ↔ Membership.mem (γ := Set α) (⋃ (i : ι), f ⁻¹' s i) x

Tactic:
simp [preimage]

Premises used: Set.preimage
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
f : α → β
s : (i : ι) → κ i → Set β
⊢ f ⁻¹' ⋃ (i : ι), ⋃ (j : κ i), s i j = ⋃ (i : ι), ⋃ (j : κ i), f ⁻¹' s i j

Tactic:
simp_rw [preimage_iUnion]

Premises used: Set.preimage_iUnion
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set (Set α)
h : ∀ (x : β), x ∈ f '' ⋃₀ s ↔ x ∈ ⋃₀ (image f '' s)
⊢ f '' ⋃₀ s = ⋃₀ (image f '' s)

Tactic:
ext
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set (Set α)
x : β
h : x ∈ f '' ⋃₀ s ↔ ∃ (i : Set α) (_ : i ∈ s), x ∈ f '' i
⊢ x ∈ f '' ⋃₀ s ↔ x ∈ ⋃₀ (image f '' s)

Tactic:
simp only [Set.mem_iUnion, Set.sUnion_image]

Premises used: Set.mem_iUnion, Set.sUnion_image
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set (Set α)
x : β
⊢ x ∈ f '' ⋃₀ s ↔ ∃ (i : Set α) (_ : i ∈ s), x ∈ f '' i

Tactic:
grind
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set (Set β)
rw : f ⁻¹' ⋃ i ∈ s, i = ⋃ t ∈ s, f ⁻¹' t
rw₁ rw₂ : Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ s, f ⁻¹' i) (⋃ t ∈ s, f ⁻¹' t)
⊢ f ⁻¹' ⋃₀ s = ⋃ t ∈ s, f ⁻¹' t

Tactic:
rw [sUnion_eq_biUnion, preimage_iUnion₂]

Premises used: Set.sUnion_eq_biUnion, Set.preimage_iUnion₂
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
s : ι → Set β
h : ∀ (x : α), x ∈ f ⁻¹' ⋂ (i : ι), s i ↔ Membership.mem (γ := Set α) (⋂ (i : ι), f ⁻¹' s i) x
⊢ f ⁻¹' ⋂ (i : ι), s i = ⋂ (i : ι), f ⁻¹' s i

Tactic:
ext
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
s : ι → Set β
x : α
⊢ x ∈ f ⁻¹' ⋂ (i : ι), s i ↔ Membership.mem (γ := Set α) (⋂ (i : ι), f ⁻¹' s i) x

Tactic:
simp
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
f : α → β
s : (i : ι) → κ i → Set β
⊢ f ⁻¹' ⋂ (i : ι), ⋂ (j : κ i), s i j = ⋂ (i : ι), ⋂ (j : κ i), f ⁻¹' s i j

Tactic:
simp_rw [preimage_iInter]

Premises used: Set.preimage_iInter
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set (Set β)
rw : f ⁻¹' ⋂ i ∈ s, i = ⋂ t ∈ s, f ⁻¹' t
rw₁ rw₂ : Eq.{u_1 + 1} (α := Set α) (⋂ i ∈ s, f ⁻¹' i) (⋂ t ∈ s, f ⁻¹' t)
⊢ f ⁻¹' ⋂₀ s = ⋂ t ∈ s, f ⁻¹' t

Tactic:
rw [sInter_eq_biInter, preimage_iInter₂]

Premises used: Set.sInter_eq_biInter, Set.preimage_iInter₂
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
rw : f ⁻¹' ⋃ i ∈ s, {i} = f ⁻¹' s
rw₁ rw₂ : f ⁻¹' s = f ⁻¹' s
⊢ ⋃ y ∈ s, f ⁻¹' {y} = f ⁻¹' s

Tactic:
rw [← preimage_iUnion₂, biUnion_of_singleton]

Premises used: Set.biUnion_of_singleton, Set.preimage_iUnion₂
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
rw : f ⁻¹' range f = univ
rw₁ rw₂ : Eq.{u_1 + 1} (α := Set α) univ univ
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ y ∈ range f, f ⁻¹' {y}) univ

Tactic:
rw [biUnion_preimage_singleton, preimage_range]

Premises used: Set.biUnion_preimage_singleton, Set.preimage_range
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : Set α
t : ι → Set β
h :
  ∀ (x : α × β),
    x ∈ SProd.sprod (β := Set β) s (⋃ (i : ι), t i) ↔ Membership.mem (γ := Set (α × β)) (⋃ (i : ι), s ×ˢ t i) x
⊢ SProd.sprod (β := Set β) s (⋃ (i : ι), t i) = ⋃ (i : ι), s ×ˢ t i

Tactic:
ext
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : Set α
t : ι → Set β
x : α × β
⊢ x ∈ SProd.sprod (β := Set β) s (⋃ (i : ι), t i) ↔ Membership.mem (γ := Set (α × β)) (⋃ (i : ι), s ×ˢ t i) x

Tactic:
simp
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
s : Set α
t : (i : ι) → κ i → Set β
⊢ SProd.sprod (β := Set β) s (⋃ (i : ι), ⋃ (j : κ i), t i j) = ⋃ (i : ι), ⋃ (j : κ i), s ×ˢ t i j

Tactic:
simp_rw [prod_iUnion]

Premises used: Set.prod_iUnion
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
s : Set α
C : Set (Set β)
simp_rw :
  SProd.sprod (β := Set β) s (⋃ i ∈ C, i) =
    ⋃ (i : Set (α × β)), ⋃ (_ : Membership.mem (γ := Set (Set (α × β))) ((fun (t : Set β) ↦ s ×ˢ t) '' C) i), i
simp_rw₁ : SProd.sprod (β := Set β) s (⋃ i ∈ C, i) = ⋃ y ∈ C, s ×ˢ y
⊢ s ×ˢ ⋃₀ C = ⋃₀ ((fun (t : Set β) ↦ s ×ˢ t) '' C)

Tactic:
simp_rw [sUnion_eq_biUnion, biUnion_image, prod_iUnion₂]

Premises used: Set.sUnion_eq_biUnion, Set.prod_iUnion₂, Set.biUnion_image
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
t : Set β
h :
  ∀ (x : α × β),
    x ∈ SProd.sprod (α := Set α) (⋃ (i : ι), s i) t ↔ Membership.mem (γ := Set (α × β)) (⋃ (i : ι), s i ×ˢ t) x
⊢ SProd.sprod (α := Set α) (⋃ (i : ι), s i) t = ⋃ (i : ι), s i ×ˢ t

Tactic:
ext
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
t : Set β
x : α × β
⊢ x ∈ SProd.sprod (α := Set α) (⋃ (i : ι), s i) t ↔ Membership.mem (γ := Set (α × β)) (⋃ (i : ι), s i ×ˢ t) x

Tactic:
simp
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
t : Set β
⊢ SProd.sprod (α := Set α) (⋃ (i : ι), ⋃ (j : κ i), s i j) t = ⋃ (i : ι), ⋃ (j : κ i), s i j ×ˢ t

Tactic:
simp_rw [iUnion_prod_const]

Premises used: Set.iUnion_prod_const
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
C : Set (Set α)
t : Set β
⊢ ⋃₀ C ×ˢ t = ⋃₀ ((fun (s : Set α) ↦ s ×ˢ t) '' C)

Tactic:
simp only [sUnion_eq_biUnion, iUnion₂_prod_const, biUnion_image]

Premises used: Set.iUnion₂_prod_const, Set.sUnion_eq_biUnion, Set.biUnion_image
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
ι : Type u_9
ι' : Type u_10
α : Type u_11
β : Type u_12
s : ι → Set α
t : ι' → Set β
h :
  ∀ (x : α × β),
    Membership.mem (γ := Set (α × β)) (⋃ (x : ι × ι'), s x.1 ×ˢ t x.2) x ↔
      x ∈ SProd.sprod (α := Set α) (β := Set β) (⋃ (i : ι), s i) (⋃ (i : ι'), t i)
⊢ ⋃ (x : ι × ι'), s x.1 ×ˢ t x.2 = SProd.sprod (α := Set α) (β := Set β) (⋃ (i : ι), s i) (⋃ (i : ι'), t i)

Tactic:
ext
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
ι : Type u_9
ι' : Type u_10
α : Type u_11
β : Type u_12
s : ι → Set α
t : ι' → Set β
x : α × β
⊢ Membership.mem (γ := Set (α × β)) (⋃ (x : ι × ι'), s x.1 ×ˢ t x.2) x ↔
    x ∈ SProd.sprod (α := Set α) (β := Set β) (⋃ (i : ι), s i) (⋃ (i : ι'), t i)

Tactic:
simp
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β × γ → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (x : β × γ), f x) (⋃ (i : β), ⋃ (j : γ), f (i, j))

Tactic:
iSup_prod

Premises used: Set.iUnion, iSup_prod
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
h :
  ∀ (z : β) (w : γ),
    Membership.mem (γ := Set (β × γ)) (⋃ (x : α), s x ×ˢ t x) (z, w) ↔
      (z, w) ∈ SProd.sprod (α := Set β) (β := Set γ) (⋃ (x : α), s x) (⋃ (x : α), t x)
⊢ ⋃ (x : α), s x ×ˢ t x = SProd.sprod (α := Set β) (β := Set γ) (⋃ (x : α), s x) (⋃ (x : α), t x)

Tactic:
ext ⟨z, w⟩
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
h :
  (∀ (x : α), z ∈ s x → w ∈ t x → (∃ (i : α), z ∈ s i) ∧ ∃ (i : α), w ∈ t i) ∧
    ∀ (x : α), z ∈ s x → ∀ (x : α), w ∈ t x → ∃ (i : α), z ∈ s i ∧ w ∈ t i
⊢ Membership.mem (γ := Set (β × γ)) (⋃ (x : α), s x ×ˢ t x) (z, w) ↔
    (z, w) ∈ SProd.sprod (α := Set β) (β := Set γ) (⋃ (x : α), s x) (⋃ (x : α), t x)

Tactic:
simp only [mem_prod, mem_iUnion, exists_imp, and_imp, iff_def]

Premises used: and_imp, Set.mem_iUnion, iff_def, Set.mem_prod, exists_imp