awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ Monotone (kernImage f)

Tactic:
Set.preimage_kernImage.monotone_u

Premises used: GaloisConnection.monotone_u, Set.preimage_kernImage
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ kernImage f s = (f '' sᶜ)ᶜ

Tactic:
Set.preimage_kernImage.u_unique (Set.image_preimage.compl)
    (fun t ↦ compl_compl (f ⁻¹' t) ▸ Set.preimage_compl)

Premises used: Set.preimage_kernImage, Set.Mem, setOf, GaloisConnection.u_unique, GaloisConnection.compl, Set.image_preimage, Set.image
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
rw : (f '' sᶜᶜ)ᶜ = (f '' s)ᶜ
rw₁ rw₂ : (f '' s)ᶜ = (f '' s)ᶜ
⊢ kernImage f sᶜ = (f '' s)ᶜ

Tactic:
rw [kernImage_eq_compl, compl_compl]

Premises used: compl_compl, Set.kernImage_eq_compl
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
rw : (f '' ∅ᶜ)ᶜ = (range f)ᶜ
rw₁ : (f '' univ)ᶜ = (range f)ᶜ
rw₂ rw₃ : (range f)ᶜ = (range f)ᶜ
⊢ kernImage f ∅ = (range f)ᶜ

Tactic:
rw [kernImage_eq_compl, compl_empty, image_univ]

Premises used: Set.image_univ, Set.compl_empty, Set.kernImage_eq_compl
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
rw : (f '' (f ⁻¹' s)ᶜ)ᶜ = s ↔ (range f)ᶜ ⊆ s
rw₁ : (f '' f ⁻¹' sᶜ)ᶜ = s ↔ (range f)ᶜ ⊆ s
rw₂ : sᶜ = f '' f ⁻¹' sᶜ ↔ (range f)ᶜ ⊆ s
rw₃ : f '' f ⁻¹' sᶜ = sᶜ ↔ (range f)ᶜ ⊆ s
rw₄ : sᶜ ⊆ range f ↔ (range f)ᶜ ⊆ s
rw₅ rw₆ : (range f)ᶜ ⊆ s ↔ (range f)ᶜ ⊆ s
⊢ kernImage f (f ⁻¹' s) = s ↔ (range f)ᶜ ⊆ s

Tactic:
rw [kernImage_eq_compl, ← preimage_compl, compl_eq_comm, eq_comm, image_preimage_eq_iff,
      compl_subset_comm]

Premises used: Set.compl_subset_comm, eq_comm, Set.kernImage_eq_compl, Set.image_preimage_eq_iff, Set.preimage_compl, compl_eq_comm
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
rw : kernImage f ∅ ⊆ kernImage f s
⊢ (range f)ᶜ ⊆ kernImage f s

Tactic:
rw [← kernImage_empty]

Premises used: Set.kernImage_empty
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ kernImage f ∅ ⊆ kernImage f s

Tactic:
kernImage_mono (empty_subset _)

Premises used: Set.kernImage_mono, Set.empty_subset
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ kernImage f ∅ ⊆ kernImage f s

Tactic:
exact kernImage_mono (empty_subset _)

Premises used: Set.kernImage_mono, Set.empty_subset
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
rw : (f '' (s ∪ f ⁻¹' t)ᶜ)ᶜ = kernImage f s ∪ t
rw₁ : (f '' (s ∪ f ⁻¹' t)ᶜ)ᶜ = (f '' sᶜ)ᶜ ∪ t
rw₂ : (f '' (sᶜ ∩ (f ⁻¹' t)ᶜ))ᶜ = (f '' sᶜ)ᶜ ∪ t
rw₃ : (f '' (sᶜ ∩ f ⁻¹' tᶜ))ᶜ = (f '' sᶜ)ᶜ ∪ t
rw₄ : (f '' sᶜ ∩ tᶜ)ᶜ = (f '' sᶜ)ᶜ ∪ t
rw₅ : (f '' sᶜ)ᶜ ∪ tᶜᶜ = (f '' sᶜ)ᶜ ∪ t
rw₆ rw₇ : (f '' sᶜ)ᶜ ∪ t = (f '' sᶜ)ᶜ ∪ t
⊢ kernImage f (s ∪ f ⁻¹' t) = kernImage f s ∪ t

Tactic:
rw [kernImage_eq_compl, kernImage_eq_compl, compl_union, ← preimage_compl, image_inter_preimage,
      compl_inter, compl_compl]

Premises used: Set.compl_union, compl_compl, Set.image_inter_preimage, Set.compl_inter, Set.kernImage_eq_compl, Set.preimage_compl
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
rw : kernImage f (s ∪ f ⁻¹' t) = t ∪ kernImage f s
rw₁ : kernImage f s ∪ t = t ∪ kernImage f s
rw₂ rw₃ : t ∪ kernImage f s = t ∪ kernImage f s
⊢ kernImage f (f ⁻¹' t ∪ s) = t ∪ kernImage f s

Tactic:
rw [union_comm, kernImage_union_preimage, union_comm]

Premises used: Set.union_comm, Set.kernImage_union_preimage
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (pi (α := α) univ v).Nonempty
i : ι
h₁ : (fun (x : (i : ι) → α i) ↦ x i) '' ⋂ (k : ι), (fun (x : (j : ι) → α j) ↦ x k) ⁻¹' v k ⊆ v i
h₂ : v i ⊆ (fun (x : (i : ι) → α i) ↦ x i) '' ⋂ (k : ι), (fun (x : (j : ι) → α j) ↦ x k) ⁻¹' v k
⊢ (fun (x : (i : ι) → α i) ↦ x i) '' ⋂ (k : ι), (fun (x : (j : ι) → α j) ↦ x k) ⁻¹' v k = v i

Tactic:
apply Subset.antisymm

Premises used: Set.Subset.antisymm
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (pi (α := α) univ v).Nonempty
i : ι
⊢ (fun (x : (i : ι) → α i) ↦ x i) '' ⋂ (k : ι), (fun (x : (j : ι) → α j) ↦ x k) ⁻¹' v k ⊆ v i

Tactic:
simp [iInter_subset]

Premises used: Set.iInter_subset
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (pi (α := α) univ v).Nonempty
i : ι
y : α i
y_in : y ∈ v i
h₂ : ∃ (x : (i : ι) → α i), (∀ (i : ι), x i ∈ v i) ∧ x i = y
⊢ Membership.mem (γ := Set (α i))
    ((fun (x : (i : ι) → α i) ↦ x i) '' ⋂ (k : ι), (fun (x : (j : ι) → α j) ↦ x k) ⁻¹' v k) y

Tactic:
simp only [mem_image, mem_iInter, mem_preimage]

Premises used: Set.mem_image, Set.mem_iInter, Set.mem_preimage
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (pi (α := α) univ v).Nonempty
i : ι
y : α i
y_in : y ∈ v i
h₂ : ∀ (z : (i : ι) → α i) (hz : z ∈ pi (α := α) univ v), ∃ (x : (i : ι) → α i), (∀ (i : ι), x i ∈ v i) ∧ x i = y
⊢ ∃ (x : (i : ι) → α i), (∀ (i : ι), x i ∈ v i) ∧ x i = y

Tactic:
rcases hv with ⟨z, hz⟩
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ pi (α := α) univ v
⊢ ∃ (x : (i : ι) → α i), (∀ (i : ι), x i ∈ v i) ∧ x i = y

Tactic:
⟨Function.update z i y, ?_, update_self i y z⟩

Premises used: Function.update, And.intro, Exists.intro, Function.update_self
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ pi (α := α) univ v
h₂ : ∀ (i_1 : ι), update (β := α) z i y i_1 ∈ v i_1
⊢ ∃ (x : (i : ι) → α i), (∀ (i : ι), x i ∈ v i) ∧ x i = y

Tactic:
refine ⟨Function.update z i y, ?_, update_self i y z⟩
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ pi (α := α) univ v
h₂ : y ∈ v i ∧ ∀ (x : ι), x ≠ i → z x ∈ v x
⊢ ∀ (i_1 : ι), update (β := α) z i y i_1 ∈ v i_1

Tactic:
rw [@forall_update_iff ι α _ z i y fun i t => t ∈ v i]

Premises used: Membership.mem, Function.forall_update_iff
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ pi (α := α) univ v
j : ι
h : j ≠ i
⊢ z j ∈ v j

Tactic:
simpa using hz j
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ pi (α := α) univ v
⊢ y ∈ v i ∧ ∀ (x : ι), x ≠ i → z x ∈ v x

Tactic:
exact ⟨y_in, fun j _ => by simpa using hz j⟩
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (pi (α := α) univ v).Nonempty
i : ι
h₁ : (fun (x : (i : ι) → α i) ↦ x i) '' ⋂ (k : ι), (fun (x : (j : ι) → α j) ↦ x k) ⁻¹' v k ⊆ v i
h₂ h₃ : v i ⊆ (fun (x : (i : ι) → α i) ↦ x i) '' ⋂ (k : ι), (fun (x : (j : ι) → α j) ↦ x k) ⁻¹' v k
⊢ (fun (x : (i : ι) → α i) ↦ x i) '' ⋂ (k : ι), (fun (x : (j : ι) → α j) ↦ x k) ⁻¹' v k = v i

Tactic:
classical
    apply Subset.antisymm
    · simp [iInter_subset]
    · intro y y_in
      simp only [mem_image, mem_iInter, mem_preimage]
      rcases hv with ⟨z, hz⟩
      refine ⟨Function.update z i y, ?_, update_self i y z⟩
      rw [@forall_update_iff ι α _ z i y fun i t => t ∈ v i]
      exact ⟨y_in, fun j _ => by simpa using hz j⟩

Premises used: Set.Subset.antisymm, Set.mem_image, Set.mem_iInter, Set.iInter_subset, Set.mem_preimage
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
S : Set (Set α)
t : Set β
f : α → β
⊢ MapsTo f (⋃₀ S) t ↔ ∀ s ∈ S, MapsTo f s t

Tactic:
mapsTo_iff_subset_preimage.trans sUnion_subset_iff

Premises used: Set.mapsTo_iff_subset_preimage, Set.sUnion_subset_iff, Iff.trans
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
t : Set β
f : α → β
⊢ MapsTo f (⋃ (i : ι), s i) t ↔ ∀ (i : ι), MapsTo f (s i) t

Tactic:
mapsTo_iff_subset_preimage.trans iUnion_subset_iff

Premises used: Set.mapsTo_iff_subset_preimage, Set.iUnion_subset_iff, Iff.trans
-- 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 β
f : α → β
⊢ MapsTo f (⋃ (i : ι), ⋃ (j : κ i), s i j) t ↔ ∀ (i : ι) (j : κ i), MapsTo f (s i j) t

Tactic:
mapsTo_iff_subset_preimage.trans iUnion₂_subset_iff

Premises used: Set.mapsTo_iff_subset_preimage, Iff.trans, Set.iUnion₂_subset_iff
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
t : ι → Set β
f : α → β
H : ∀ (i : ι), MapsTo f (s i) (t i)
⊢ MapsTo f (⋃ (i : ι), s i) (⋃ (i : ι), t i)

Tactic:
mapsTo_iUnion.2 fun i ↦ (H i).mono_right (subset_iUnion t i)

Premises used: Iff.mpr, Set.MapsTo.mono_right, Set.subset_iUnion, Set.mapsTo_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), MapsTo f (s i j) (t i j)
⊢ MapsTo f (⋃ (i : ι), ⋃ (j : κ i), s i j) (⋃ (i : ι), ⋃ (j : κ i), t i j)

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

Premises used: Set.mapsTo_iUnion_iUnion
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
s : Set α
T : Set (Set β)
f : α → β
⊢ MapsTo f s (⋂₀ T) ↔ ∀ t ∈ T, MapsTo f s t

Tactic:
forall₂_comm

Premises used: Set.Mem, setOf, Set.MapsTo, Set.sInter, forall₂_comm
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : Set α
t : ι → Set β
f : α → β
⊢ MapsTo f s (⋂ (i : ι), t i) ↔ ∀ (i : ι), MapsTo f s (t i)

Tactic:
mapsTo_sInter.trans forall_mem_range

Premises used: iInf, Set.forall_mem_range, Set.iInter, Set.mapsTo_sInter, Iff.trans
-- 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 : α → β
⊢ MapsTo f s (⋂ (i : ι), ⋂ (j : κ i), t i j) ↔ ∀ (i : ι) (j : κ i), MapsTo f s (t i j)

Tactic:
simp only [mapsTo_iInter]

Premises used: Set.mapsTo_iInter
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
t : ι → Set β
f : α → β
H : ∀ (i : ι), MapsTo f (s i) (t i)
⊢ MapsTo f (⋂ (i : ι), s i) (⋂ (i : ι), t i)

Tactic:
mapsTo_iInter.2 fun i => (H i).mono_left (iInter_subset s i)

Premises used: Iff.mpr, Set.mapsTo_iInter, Set.MapsTo.mono_left, Set.iInter_subset
-- 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), MapsTo f (s i j) (t i j)
⊢ MapsTo f (⋂ (i : ι), ⋂ (j : κ i), s i j) (⋂ (i : ι), ⋂ (j : κ i), t i j)

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

Premises used: Set.mapsTo_iInter_iInter
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
f : α → β
⊢ f '' ⋂ (i : ι), s i ⊆ ⋂ (i : ι), f '' s i

Tactic:
(mapsTo_iInter_iInter fun i => mapsTo_image f (s i)).image_subset

Premises used: Set.mapsTo_iInter_iInter, Set.mapsTo_image, Set.MapsTo.image_subset
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
f : α → β
⊢ f '' ⋂ (i : ι), ⋂ (j : κ i), s i j ⊆ ⋂ (i : ι), ⋂ (j : κ i), f '' s i j

Tactic:
(mapsTo_iInter₂_iInter₂ fun i hi => mapsTo_image f (s i hi)).image_subset

Premises used: Set.mapsTo_image, Set.mapsTo_iInter₂_iInter₂, Set.MapsTo.image_subset
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
S : Set (Set α)
f : α → β
rw : f '' ⋂ i ∈ S, i ⊆ ⋂ s ∈ S, f '' s
⊢ f '' ⋂₀ S ⊆ ⋂ s ∈ S, f '' s

Tactic:
rw [sInter_eq_biInter]

Premises used: Set.sInter_eq_biInter
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
S : Set (Set α)
f : α → β
⊢ f '' ⋂ i ∈ S, i ⊆ ⋂ s ∈ S, f '' s

Tactic:
apply image_iInter₂_subset

Premises used: Set.image_iInter₂_subset
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Set α
S : Set (Set β)
f : α → β → γ
⊢ image2 f t (⋂₀ S) ⊆ ⋂ s ∈ S, image2 f t s

Tactic:
aesop
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
S : Set (Set α)
t : Set β
f : α → β → γ
⊢ image2 f (⋂₀ S) t ⊆ ⋂ s ∈ S, image2 f s t

Tactic:
aesop
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
⊢ Injective f ↔ ∀ (i : ι), Injective ((U i).restrictPreimage f)

Tactic:
⟨fun H i => (U i).restrictPreimage_injective H, fun H x y e => ?_⟩

Premises used: Iff.intro, Set.restrictPreimage_injective
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
refine : ∀ (H : ∀ (i : ι), Injective ((U i).restrictPreimage f)) (x y : α) (e : f x = f y), x = y
⊢ Injective f ↔ ∀ (i : ι), Injective ((U i).restrictPreimage f)

Tactic:
refine ⟨fun H i => (U i).restrictPreimage_injective H, fun H x y e => ?_⟩
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective ((U i).restrictPreimage f)
x y : α
e : f x = f y
rw : Membership.mem (γ := Set β) univ (f x)
⊢ f x ∈ iUnion U

Tactic:
rw [hU]
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective ((U i).restrictPreimage f)
x y : α
e : f x = f y
⊢ Membership.mem (γ := Set β) univ (f x)

Tactic:
trivial
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective ((U i).restrictPreimage f)
x y : α
e : f x = f y
obtain : ∀ (i : ι) (hi : f x ∈ U i), x = y
⊢ x = y

Tactic:
obtain ⟨i, hi⟩ := Set.mem_iUnion.mp
      (show f x ∈ Set.iUnion U by rw [hU]; trivial)

Premises used: Set.mem_iUnion, Iff.mp
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective ((U i).restrictPreimage f)
x y : α
e : f x = f y
i : ι
hi : f x ∈ U i
⊢ x = y

Tactic:
injection @H i ⟨x, hi⟩ ⟨y, show f y ∈ U i from e ▸ hi⟩ (Subtype.ext e)

Premises used: Subtype.ext
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
⊢ Surjective f ↔ ∀ (i : ι), Surjective ((U i).restrictPreimage f)

Tactic:
⟨fun H i => (U i).restrictPreimage_surjective H, fun H x => ?_⟩

Premises used: Set.restrictPreimage_surjective, Iff.intro
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
refine : ∀ (H : ∀ (i : ι), Surjective ((U i).restrictPreimage f)) (x : β), ∃ (a : α), f a = x
⊢ Surjective f ↔ ∀ (i : ι), Surjective ((U i).restrictPreimage f)

Tactic:
refine ⟨fun H i => (U i).restrictPreimage_surjective H, fun H x => ?_⟩
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Surjective ((U i).restrictPreimage f)
x : β
rw : Membership.mem (γ := Set β) univ x
⊢ x ∈ iUnion U

Tactic:
rw [hU]
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Surjective ((U i).restrictPreimage f)
x : β
⊢ Membership.mem (γ := Set β) univ x

Tactic:
trivial
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Surjective ((U i).restrictPreimage f)
x : β
obtain : ∀ (i : ι) (hi : x ∈ U i), ∃ (a : α), f a = x
⊢ ∃ (a : α), f a = x

Tactic:
obtain ⟨i, hi⟩ :=
    Set.mem_iUnion.mp
      (show x ∈ Set.iUnion U by rw [hU]; trivial)

Premises used: Set.mem_iUnion, Iff.mp
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Surjective ((U i).restrictPreimage f)
x : β
i : ι
hi : x ∈ U i
⊢ ∃ (a : α), f a = x

Tactic:
⟨_, congr_arg Subtype.val (H i ⟨x, hi⟩).choose_spec⟩

Premises used: Exists.choose_spec, Subtype.mk, congr_arg, Exists.intro, Subtype.val
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Surjective ((U i).restrictPreimage f)
x : β
i : ι
hi : x ∈ U i
⊢ ∃ (a : α), f a = x

Tactic:
exact ⟨_, congr_arg Subtype.val (H i ⟨x, hi⟩).choose_spec⟩
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
rw :
  ((∀ (i : ι), Injective ((U i).restrictPreimage f)) ∧ ∀ (i : ι), Surjective ((U i).restrictPreimage f)) ↔
    ∀ (i : ι), Bijective ((U i).restrictPreimage f)
⊢ Bijective f ↔ ∀ (i : ι), Bijective ((U i).restrictPreimage f)

Tactic:
rw [Bijective, injective_iff_injective_of_iUnion_eq_univ hU,
    surjective_iff_surjective_of_iUnion_eq_univ hU]

Premises used: Set.injective_iff_injective_of_iUnion_eq_univ, Function.Bijective, Set.surjective_iff_surjective_of_iUnion_eq_univ
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
⊢ ((∀ (i : ι), Injective ((U i).restrictPreimage f)) ∧ ∀ (i : ι), Surjective ((U i).restrictPreimage f)) ↔
    ∀ (i : ι), Bijective ((U i).restrictPreimage f)

Tactic:
simp [Bijective, forall_and]

Premises used: Function.Bijective, forall_and
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabit : ∀ (inhabited_h : Inhabited ι), f '' ⋂ (i : ι), s i = ⋂ (i : ι), f '' s i
⊢ f '' ⋂ (i : ι), s i = ⋂ (i : ι), f '' s i

Tactic:
inhabit ι
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
⊢ f '' ⋂ (i : ι), s i = ⋂ (i : ι), f '' s i

Tactic:
Subset.antisymm (image_iInter_subset s f) fun y hy => ?_

Premises used: Set.Subset.antisymm, Set.image_iInter_subset
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
refine : ∀ (y : β) (hy : Membership.mem (γ := Set β) (⋂ (i : ι), f '' s i) y), y ∈ f '' ⋂ (i : ι), s i
⊢ f '' ⋂ (i : ι), s i = ⋂ (i : ι), f '' s i

Tactic:
refine Subset.antisymm (image_iInter_subset s f) fun y hy => ?_

Premises used: Set.Subset.antisymm, Set.image_iInter_subset
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
hy : Membership.mem (γ := Set β) (⋂ (i : ι), f '' s i) y
⊢ ∀ (i : ι), ∃ x ∈ s i, f x = y

Tactic:
simp only [mem_iInter, mem_image] at hy

Premises used: Set.mem_image, Set.mem_iInter
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
hy : ∀ (i : ι), ∃ x ∈ s i, f x = y
choose : ∀ (x : (i : ι) → α) (hx : ∀ (i : ι), x i ∈ s i) (hy : ∀ (i : ι), f (x i) = y), y ∈ f '' ⋂ (i : ι), s i
⊢ y ∈ f '' ⋂ (i : ι), s i

Tactic:
choose x hx hy using hy
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
x : (i : ι) → α
hx : ∀ (i : ι), x i ∈ s i
hy : ∀ (i : ι), f (x i) = y
⊢ y ∈ f '' ⋂ (i : ι), s i

Tactic:
⟨x default, mem_iInter.2 fun i => ?_, hy _⟩

Premises used: Iff.mpr, Inhabited.default, Set.Mem, setOf, Set.mem_iInter, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
x : (i : ι) → α
hx : ∀ (i : ι), x i ∈ s i
hy : ∀ (i : ι), f (x i) = y
refine : ∀ (i : ι), x default ∈ s i
⊢ y ∈ f '' ⋂ (i : ι), s i

Tactic:
refine ⟨x default, mem_iInter.2 fun i => ?_, hy _⟩
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
x : (i : ι) → α
hx : ∀ (i : ι), x i ∈ s i
hy : ∀ (i : ι), f (x i) = y
i : ι
this : x default = x i
rw : x i ∈ s i
⊢ x default ∈ s i

Tactic:
rw [this]
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
x : (i : ι) → α
hx : ∀ (i : ι), x i ∈ s i
hy : ∀ (i : ι), f (x i) = y
i : ι
this : x default = x i
⊢ x i ∈ s i

Tactic:
apply hx
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
x : (i : ι) → α
hx : ∀ (i : ι), x i ∈ s i
hy : ∀ (i : ι), f (x i) = y
i : ι
suffices : x default = x i
⊢ x default ∈ s i

Tactic:
suffices x default = x i by
    rw [this]
    apply hx
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
x : (i : ι) → α
hx : ∀ (i : ι), x i ∈ s i
hy : ∀ (i : ι), f (x i) = y
i : ι
⊢ ∀ (i : ι), Membership.mem (γ := Set α) (⋃ (j : ι), s j) (x i)

Tactic:
replace hx : ∀ i, x i ∈ ⋃ j, s j := fun i => (subset_iUnion _ _) (hx i)
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
x : (i : ι) → α
hy : ∀ (i : ι), f (x i) = y
i : ι
hx : ∀ (i : ι), Membership.mem (γ := Set α) (⋃ (j : ι), s j) (x i)
apply : f (x default) = f (x i)
⊢ x default = x i

Tactic:
apply h (hx _) (hx _)
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
x : (i : ι) → α
hy : ∀ (i : ι), f (x i) = y
i : ι
hx : ∀ (i : ι), Membership.mem (γ := Set α) (⋃ (j : ι), s j) (x i)
⊢ f (x default) = f (x i)

Tactic:
simp only [hy]
-- 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)
simp : f '' ⨅ (x : Subtype p), s (↑x : ι) ⋯ = ⨅ (x : Subtype p), f '' s (↑x : ι) ⋯
⊢ f '' ⋂ (i : ι), ⋂ (hi : p i), s i hi = ⋂ (i : ι), ⋂ (hi : p i), f '' s i hi

Tactic:
simp only [iInter, iInf_subtype']

Premises used: Set.iInter, iInf_subtype'
-- 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)
⊢ Nonempty.{max 1 u_5} { i : ι // p i }

Tactic:
haveI : Nonempty { i // p i } := nonempty_subtype.2 hp
-- 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 }
h₁ : InjOn f (⋃ (i : Subtype p), s (↑i : ι) ⋯)
⊢ f '' ⨅ (x : Subtype p), s (↑x : ι) ⋯ = ⨅ (x : Subtype p), f '' s (↑x : ι) ⋯

Tactic:
apply InjOn.image_iInter_eq

Premises used: Set.InjOn.image_iInter_eq