mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Image

Goal state before:
pp: β : Type u_2
ι : Type u_5
f : ι → β
H : Surjective f
⊢ ∀ (x : β), x ∈ f '' univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
a : α
⊢ f '' {a} = {f a}

Tactic:
by

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

Goal state before:
pp: α : Type u_5
β : Type u_6
f : α → β
s : Set α
⊢ f '' s = ∅ ↔ s = ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_5
β : Type u_6
f : α → β
s : Set α
⊢ ∅ = f '' s ↔ s = ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : BooleanAlgebra α
t : α
s : Set α
⊢ t ∈ compl '' s ↔ tᶜ ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
⊢ image id = id

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ (fun x ↦ x) '' s = s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ id '' s = s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f : α → α
n : ℕ
⊢ image f^[n] = (image f)^[n]

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : BooleanAlgebra α
s : Set α
⊢ compl '' compl '' s = s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
a : α
s : Set α
⊢ f '' insert a s = insert (f a) (f '' s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
a b : α
⊢ f '' {a, b} = {f a, f b}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
g : β → α
hfg : LeftInverse g f
s : Set α
x : α
⊢ f x ∈ g ⁻¹' s ↔ x ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
⊢ (∃ x, x ∈ range f ∩ s' ∧ ¬x ∈ range f ∩ s) ↔ ∃ x, x ∈ f ⁻¹' s' ∧ ¬x ∈ f ⁻¹' s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
p : α × β → Prop
⊢ (∃ x, x ∈ s ×ˢ t ∧ p x) ↔ ∃ x, x ∈ s ∧ ∃ y, y ∈ t ∧ p (x, y)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
⊢ s ×ˢ ∅ = ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
⊢ ∅ ×ˢ t = ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ univ ×ˢ univ = univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
⊢ univ ×ˢ t = Prod.snd ⁻¹' t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
⊢ s ×ˢ univ = Prod.fst ⁻¹' s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
⊢ s ×ˢ t = univ ↔ s = univ ∧ t = univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
⊢ range f ∩ s ⊂ range f ∩ s' ↔ f ⁻¹' s ⊂ f ⁻¹' s'

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
a : α
⊢ {a} ×ˢ t = Prod.mk a '' t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
b : β
⊢ s ×ˢ {b} = (fun a ↦ (a, b)) '' s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
⊢ {a} ×ˢ {b} = {(a, b)}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
g : β → α
b : β
s : Set α
h₁ : LeftInverse g f
h₂ : RightInverse g f
⊢ b ∈ f '' s ↔ g b ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
H : Injective f
⊢ Disjoint (f '' s) (f '' sᶜ)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t : Set β
⊢ (s₁ ∪ s₂) ×ˢ t = s₁ ×ˢ t ∪ s₂ ×ˢ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
H : Surjective f
⊢ f '' s ∪ f '' sᶜ = univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t₁ t₂ : Set β
⊢ s ×ˢ (t₁ ∪ t₂) = s ×ˢ t₁ ∪ s ×ˢ t₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t : Set β
⊢ (s₁ ∩ s₂) ×ˢ t = s₁ ×ˢ t ∩ s₂ ×ˢ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t₁ t₂ : Set β
⊢ s ×ˢ (t₁ ∩ t₂) = s ×ˢ t₁ ∩ s ×ˢ t₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
⊢ s₁ ×ˢ t₁ ∩ s₂ ×ˢ t₂ = (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t : Set α
⊢ f '' s \ f '' t ⊆ f '' (s \ t)

Tactic:
by

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

Goal state before:
pp: α : Type u_5
β : Type u_6
s : Set α
t : Set β
⊢ (s ×ˢ t)ᶜ = sᶜ ×ˢ univ ∪ univ ×ˢ tᶜ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
⊢ Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s t : Set α
⊢ f '' s ∆ t = (f '' s) ∆ (f '' t)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set β
hs : s.Nonempty
f : α → β
hf : Surjective f
y : β
hy : y ∈ s
x : α
hx : f x = y
⊢ x ∈ f ⁻¹' s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : γ → δ
s : Set α
t : Set γ
⊢ Prod.map f g '' s ×ˢ t = (f '' s) ×ˢ (g '' t)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
h : Surjective f
x : β
hx : x ∈ s
y : α
e : f y = x
⊢ y ∈ f ⁻¹' s ∧ f y = x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
a : α
⊢ insert a s ×ˢ t = Prod.mk a '' t ∪ s ×ˢ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
hs : s.Nonempty
t : Set β
a : β
⊢ s ⊆ (fun x ↦ a) ⁻¹' t ↔ a ∈ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ Injective (preimage f) ↔ Surjective f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
b : β
⊢ s ×ˢ insert b t = (fun a ↦ (a, b)) '' s ∪ s ×ˢ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ Surjective (preimage f) ↔ Injective f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t : Set α
⊢ s.domRestrict f '' Subtype.val ⁻¹' t = f '' (t ∩ s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ f '' (s ∩ f ⁻¹' t) = f '' s ∩ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ f '' (f ⁻¹' t ∩ s) = t ∩ f '' s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
⊢ (range f).domRestrict (extend f g g') = fun x ↦ g (Exists.choose ⋯)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
⊢ (range f)ᶜ.domRestrict (extend f g g') = g' ∘ Subtype.val

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
b : β
hb : b ∈ t
⊢ (fun a ↦ (a, b)) ⁻¹' s ×ˢ t = s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ (f '' s ∩ t).Nonempty ↔ (s ∩ f ⁻¹' t).Nonempty

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
a : α
ha : a ∈ s
⊢ Prod.mk a ⁻¹' s ×ˢ t = t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ Disjoint (f '' s) t ↔ Disjoint s (f ⁻¹' t)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
⊢ range (extend f g g') ⊆ range g ∪ g' '' (range f)ᶜ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
b : β
hb : ¬b ∈ t
⊢ (fun a ↦ (a, b)) ⁻¹' s ×ˢ t = ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ Disjoint t (f '' s) ↔ Disjoint (f ⁻¹' t) s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
a : α
ha : ¬a ∈ s
⊢ Prod.mk a ⁻¹' s ×ˢ t = ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
b : β
inst✝ : DecidablePred fun x ↦ x ∈ t
⊢ (fun a ↦ (a, b)) ⁻¹' s ×ˢ t = if b ∈ t then s else ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
a : α
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ Prod.mk a ⁻¹' s ×ˢ t = if a ∈ s then t else ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ f '' (s \ f ⁻¹' t) = f '' s \ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
b : β
inst✝ : DecidablePred fun x ↦ x ∈ t
f : γ → α
⊢ (fun a ↦ (f a, b)) ⁻¹' s ×ˢ t = if b ∈ t then f ⁻¹' s else ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_4
s : Set α
t : Set β
a : α
inst✝ : DecidablePred fun x ↦ x ∈ s
g : δ → β
⊢ (fun b ↦ (a, g b)) ⁻¹' s ×ˢ t = if a ∈ s then g ⁻¹' t else ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Injective f
g : α → γ
g' : β → γ
⊢ range (extend f g g') = range g ∪ g' '' (range f)ᶜ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Set α
f : α → β
hf : Injective f
eq : f '' s = f '' t
⊢ s = t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ Prod.swap ⁻¹' s ×ˢ t = t ×ˢ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ Prod.swap '' s ×ˢ t = t ×ˢ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
m₁ : α → γ
m₂ : β → δ
⊢ ∀ (x : γ × δ), x ∈ (m₁ '' s) ×ˢ (m₂ '' t) ↔ x ∈ (fun p ↦ (m₁ p.1, m₂ p.2)) '' s ×ˢ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m₁ : α → γ
m₂ : β → δ
⊢ ∀ (x : γ × δ), x ∈ range m₁ ×ˢ range m₂ ↔ x ∈ range fun p ↦ (m₁ p.1, m₂ p.2)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m₁ : α → γ
⊢ ∀ (x : γ × β), x ∈ range m₁ ×ˢ univ ↔ x ∈ range fun p ↦ (m₁ p.1, p.2)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_4
m₂ : β → δ
⊢ ∀ (x : α × δ), x ∈ univ ×ˢ range m₂ ↔ x ∈ range fun p ↦ (p.1, m₂ p.2)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
⊢ (range fun x ↦ (f x, g x)) ⊆ range f ×ˢ range g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
W : Set γ
f : α × β → γ
⊢ s ×ˢ t ⊆ f ⁻¹' W ↔ ∀ (a : α) (b : β), a ∈ s → b ∈ t → f (a, b) ∈ W

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ t ⊆ f '' s ↔ ∃ u, u ⊆ s ∧ f '' u = t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
s : Set α
⊢ (fun x ↦ (f x, g x)) '' s ⊆ (f '' s) ×ˢ (g '' s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
j : β → γ
hf : FactorsThrough g f
hg : Injective g
⊢ InjOn (extend f g j) (range f)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
b : β
hb : b ∈ t
⊢ (fun a ↦ (a, b)) '' s ⊆ s ×ˢ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
a : α
ha : a ∈ s
⊢ Prod.mk a '' t ⊆ s ×ˢ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
f : ι → α
s : Set α
h : ∀ (x : ι), f x ∈ s
⊢ Injective (codRestrict f s h) ↔ Injective f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set (α × β)
x✝¹ : α × β
p₁ : α
p₂ : β
x✝ : (p₁, p₂) ∈ s
⊢ (p₁, p₂) ∈ (Prod.fst '' s) ×ˢ (Prod.snd '' s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
⊢ s ×ˢ t \ s₁ ×ˢ t₁ = s ×ˢ (t \ t₁) ∪ (s \ s₁) ×ˢ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
p : Set β → Prop
⊢ (∃ t, t ⊆ f '' s ∧ p t) ↔ ∃ t, t ⊆ s ∧ p (f '' t)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
f : ι → α
s : Set α
h : ∀ (x : ι), f x ∈ s
⊢ range (codRestrict f s h) = Subtype.val ⁻¹' range f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
p : Set β → Prop
⊢ (∀ (t : Set β), t ⊆ f '' s → p t) ↔ ∀ (t : Set α), t ⊆ s → p (f '' t)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
f : ι → α
s : Set α
h : ∀ (x : ι), f x ∈ s
⊢ Surjective (codRestrict f s h) ↔ range f = s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Set α
f : α → β
hf : Injective f
⊢ f '' s ⊆ f '' t ↔ s ⊆ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
f : ι → α
⊢ Surjective (codRestrict f (range f) ⋯)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
f : α → α
h : MapsTo f s s
x : ↑s
k : ℕ
⊢ ↑((restrict f s s h)^[k] x) = f^[k] ↑x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s.Nonempty ∧ t.Nonempty

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
x✝ : ∃ g, ∀ (x : ↑s), f ↑x = ↑(g x)
x : α
hx : x ∈ s
g : ↑s → ↑t
hg : ∀ (x : ↑s), f ↑x = ↑(g x)
⊢ f x ∈ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ t.restrictPreimage f '' Subtype.val ⁻¹' s = Subtype.val ⁻¹' f '' s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
f : α → β
⊢ range (t.restrictPreimage f) = Subtype.val ⁻¹' range f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a | σ a ≠ a} ⊆ s
⊢ ⇑σ '' s = s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
f : α → β
u : Set ↑t
⊢ Subtype.val '' t.restrictPreimage f ⁻¹' u = f ⁻¹' Subtype.val '' u

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
f : α → β
u : Set ↑t
⊢ t.restrictPreimage f ⁻¹' u = (fun a ↦ f ↑a) ⁻¹' Subtype.val '' u

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
⊢ Injective (restrict f s t h) ↔ InjOn f s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
t : Set α
h : t ∈ 𝒫 insert a s
hs : a ∈ t
⊢ t \ {a} ∈ 𝒫 s ∧ insert a (t \ {a}) = t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : Surjective (restrict f s t h)
b : β
hb : b ∈ t
a : α
ha : a ∈ s
ha' : restrict f s t h ⟨a, ha⟩ = ⟨b, hb⟩
⊢ f a = b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
⊢ 𝒫 insert a s = 𝒫 s ∪ insert a '' 𝒫 s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : ¬a ∈ s
⊢ Disjoint (𝒫 s) (insert a '' 𝒫 s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : ¬a ∈ s
u : Set α
u_mem : u ∈ 𝒫 s
v : Set α
v_mem : v ∈ 𝒫 s
eq : insert a u = insert a v
⊢ u = v

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
f : ι → α
p : α → Prop
⊢ (∀ (a : α), a ∈ range f → p a) ↔ ∀ (i : ι), p (f i)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
f : ι → α
p : ↑(range f) → Prop
⊢ (∀ (a : ↑(range f)), p a) ↔ ∀ (i : ι), p ⟨f i, ⋯⟩

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
⊢ Surjective (restrict f s t h) ↔ SurjOn f s t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
f : ι → α
p : α → Prop
⊢ (∃ a, a ∈ range f ∧ p a) ↔ ∃ i, p (f i)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
f : ι → α
p : ↑(range f) → Prop
⊢ (∃ a, p a) ↔ ∃ i, p ⟨f i, ⋯⟩

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ f '' univ = range f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
⊢ f '' sᶜ = range f \ f '' s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
δ : α → Sort u_7
f g : (i : α) → δ i
inst✝ : (i : α) → Decidable (i ∈ ∅)
⊢ ∅.piecewise f g = g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
δ : α → Sort u_7
f g : (i : α) → δ i
inst✝ : (i : α) → Decidable (i ∈ univ)
⊢ univ.piecewise f g = f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
⊢ (insert j s).piecewise f g j = f j

Tactic:
by

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

Goal state before:
pp: α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
⊢ (insert j s).piecewise f g = update (s.piecewise f g) j (f j)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
⊢ range f \ f '' s = f '' sᶜ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
inst✝¹ : (y : α) → Decidable (y ∈ {x})
inst✝ : DecidableEq α
f g : α → β
⊢ {x}.piecewise f g = update g x (f x)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
δ : α → Type u_8
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g i
i : α
h : i ∈ s
⊢ s.piecewise f₁ f₂ i ≤ g i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f ⁻¹' s = univ ↔ range f ⊆ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
δ : α → Type u_8
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g i
i : α
h : ¬i ∈ s
⊢ s.piecewise f₁ f₂ i ≤ g i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
h : t.Nonempty
⊢ s ×ˢ t ⊆ s₁ ×ˢ t ↔ s ⊆ s₁

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ f '' s ⊆ range f

Tactic:
by

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

Goal state before:
pp: i : ℕ
⊢ i ∈ range Nat.succ → 0 < i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t t₁ : Set β
h : s.Nonempty
⊢ s ×ˢ t ⊆ s ×ˢ t₁ ↔ t ⊆ t₁

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set β
hs : s.Nonempty
f : α → β
hf : s ⊆ range f
w✝ : β
hy : w✝ ∈ s
x : α
hx : f x = w✝
⊢ x ∈ f ⁻¹' s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
g : α → β
f : ι → α
⊢ range (g ∘ f) = g '' range f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
⊢ range f ⊆ range g ↔ ∃ h, f = g ∘ h

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ range f = s ↔ (∀ (a : α), f a ∈ s) ∧ ∀ (b : β), b ∈ s → ∃ a, f a = b

Tactic:
by

Goal state after: