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

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ val ⁻¹' (t ∩ s) = val ⁻¹' 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 ι
i : ι
inst✝ : DecidableEq ι
hi : ¬i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
j : ι
hj : j ∈ s
⊢ t j (update f i a j) = t j (f j)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t u : Set α
⊢ val ⁻¹' t ⊆ val ⁻¹' u ↔ s ∩ t ⊆ s ∩ u

Tactic:
by

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

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

Tactic:
by

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

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

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 ι
i : ι
inst✝ : DecidableEq ι
hi : i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ (s.pi fun j ↦ t j (update f i a j)) = ({i} ∪ s \ {i}).pi fun j ↦ t j (update f i a j)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ val ⁻¹' t = ∅ ↔ s ∩ t = ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Option α → β
⊢ Injective f ↔ Injective (f ∘ some) ∧ ¬f none ∈ range (f ∘ some)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
b : β
f : α → β
⊢ (range fun o ↦ o.elim b f) = insert b (range f)

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 ι
i : ι
inst✝ : DecidableEq ι
hi : i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ (({i} ∪ s \ {i}).pi fun j ↦ t j (update f i a j)) = {x | x i ∈ t i a} ∩ (s \ {i}).pi fun j ↦ t j (f j)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
⊢ (fun o ↦ o.elim b f) '' range some = range f

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : DecidableEq ι
β : ι → Type u_4
i : ι
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ (univ.pi fun j ↦ t j (update f i a j)) = {x | x i ∈ t i a} ∩ {i}ᶜ.pi fun j ↦ t j (f j)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : DecidableEq ι
i : ι
s : Set (α i)
⊢ univ.pi (update (fun j ↦ univ) i s) = eval i ⁻¹' s

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ Surjective (image 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 : (i : ι) → Set (α i)
ht : (s.pi t).Nonempty
i : ι
⊢ t i ⊆ eval i '' s.pi t

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ Injective (image f) ↔ Injective f

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
hf : Bijective f
s : Set β
t : Set α
⊢ f ⁻¹' s = t ↔ s = f '' t

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
hf : Bijective f
s : Set α
t : Set β
⊢ 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 t : Set β
h : Codisjoint s t
⊢ Codisjoint (f ⁻¹' s) (f ⁻¹' t)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f₁ f₂ : α → β
a : α
⊢ EqOn f₁ f₂ {a} ↔ f₁ a = f₂ a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f₁ f₂ : α → β
⊢ EqOn f₁ f₂ univ ↔ f₁ = 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 : γ → α
s : Set β
t : Set γ
h : ∀ (b : β), b ∈ s → ∀ (c : γ), c ∈ t → f b ≠ g c
⊢ f '' s ⊓ g '' t ⊆ ⊥

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
heq : EqOn f₁ f₂ s
⊢ f₁ '' s = f₂ '' s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
f : α → α
h : EqOn f id s
⊢ f '' s = s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s t : Set β
h : Disjoint (f ⁻¹' s) (f ⁻¹' t)
⊢ Disjoint 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 : Disjoint s (range f)
⊢ f ⁻¹' 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 : f ⁻¹' s = ∅
⊢ Disjoint s (range f)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Set α
v : Set β
⊢ ∀ (b : α), b ∈ u → ∀ (c : β), c ∈ v → Sum.inl b ≠ Sum.inr c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
heq : EqOn f₁ f₂ s
t : Set β
⊢ s ∩ f₁ ⁻¹' t = s ∩ f₂ ⁻¹' t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
v : Set β
⊢ Disjoint (range Sum.inl) (Sum.inr '' v)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : Decidable (s.pi t).Nonempty
hi : ¬i ∈ s
⊢ eval i '' s.pi t = if (s.pi t).Nonempty then univ else ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Set α
⊢ Disjoint (Sum.inl '' u) (range Sum.inr)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : α → Type u_2
i : α
s : Set (β i)
⊢ Sigma.mk i ⁻¹' Sigma.mk i '' s = s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ MapsTo f s ∅ ↔ s = ∅

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 ι
f : (i : ι) → α i → β i
hf : ∀ (i : ι), ¬i ∈ s → Surjective (f i)
t : (i : ι) → Set (α i)
b : (i : ι) → β i
hb : b ∈ s.pi fun i ↦ f i '' t i
i : ι
⊢ ∃ a, f i a = b i ∧ (i ∈ s → a ∈ t i)

Tactic:
by

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

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

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 ι
f : (i : ι) → α i → β i
hf : ∀ (i : ι), ¬i ∈ s → Surjective (f i)
t : (i : ι) → Set (α i)
⊢ Pi.map f '' s.pi t = s.pi fun i ↦ f i '' t i

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
f : (i : ι) → α i → β i
t : (i : ι) → Set (α i)
⊢ ∀ (i : ι), ¬i ∈ univ → Surjective (f i)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
f : (i : ι) → α i → β i
⊢ range (Pi.map f) = univ.pi fun i ↦ range (f i)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
s' : Set ((i : ι) → α i)
⊢ s' ⊆ s.pi t ↔ ∀ (i : ι), i ∈ s → s' ⊆ (fun x ↦ x i) ⁻¹' t i

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
inst✝ : DecidableEq ι
a : (i : ι) → α i
i : ι
b : α i
⊢ update a i b ∈ s.pi t ↔ a ∈ (s \ {i}).pi t ∧ (i ∈ s → b ∈ t i)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
x : α
⊢ MapsTo f (Insert.insert x s) (Insert.insert (f x) t)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
inst✝ : DecidableEq ι
a : (i : ι) → α i
i : ι
b : α i
ha : a ∈ s.pi t
⊢ update a i b ∈ s.pi t ↔ i ∈ s → b ∈ t i

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
a : (i : ι) → α i
x✝ : a ∈ univ.pi t ∧ ∀ (x : (i : ι) → α i), x ∈ univ.pi t → x = a
i : ι
h₁ : a ∈ univ.pi t
h₂ : ∀ (x : (i : ι) → α i), x ∈ univ.pi t → x = a
⊢ a i ∈ t i

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
a : (i : ι) → α i
⊢ (∀ (i : ι), a i ∈ t i ∧ ∀ (x : α i), x ∈ t i → x = a i) → a ∈ univ.pi t ∧ ∀ (x : (i : ι) → α i), x ∈ univ.pi t → x = a

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
a : (i : ι) → α i
⊢ univ.pi t = {a} ↔ ∀ (i : ι), t i = {a 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₂ : (i : ι) → Set (α i)
⊢ s.pi t₁ ⊆ s.pi t₂ ↔ (∀ (i : ι), i ∈ s → t₁ i ⊆ t₂ i) ∨ s.pi t₁ = ∅

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
t₁ t₂ : (i : ι) → Set (α i)
⊢ univ.pi t₁ ⊆ univ.pi t₂ ↔ (∀ (i : ι), t₁ i ⊆ t₂ i) ∨ ∃ i, t₁ i = ∅

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
i : ι
inst✝ : DecidableEq ι
s : Set (α i)
⊢ eval i ⁻¹' s = univ.pi (update (fun x ↦ univ) i s)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
i : ι
inst✝ : DecidableEq ι
s : Set (α i)
⊢ eval i ⁻¹' s = {i}.pi (update (fun x ↦ univ) i s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
⊢ InjOn f (s₁ ∪ s₂) ↔ InjOn f s₁ ∧ InjOn f s₂ ∧ ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
a : α
has : ¬a ∈ s
⊢ InjOn f (insert a s) ↔ InjOn f s ∧ ¬f a ∈ f '' s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ InjOn f univ ↔ Injective f

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
⊢ update f i ⁻¹' s.pi t = t i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
f : α → β
g : β → γ
h : InjOn (g ∘ f) s
x✝¹ : α
hx : x✝¹ ∈ s
x✝ : α
hy : x✝ ∈ s
heq : f x✝¹ = f x✝
⊢ (g ∘ f) x✝¹ = (g ∘ f) x✝

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
h : Injective (g ∘ f)
⊢ InjOn g (range f)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
β : ι → Type u_3
inst✝ : DecidableEq ι
x : (i : ι) → β i
i : ι
s : Set (β i)
⊢ update x i '' s = univ.pi (update (fun j ↦ {x j}) i s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
s : Set β
h✝ : InjOn g s
hs : range f ⊆ s
h : Injective f
x✝ : α
⊢ ∀ ⦃a₂ : α⦄, (g ∘ f) x✝ = (g ∘ f) a₂ → x✝ = a₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : Nonempty β
x✝ : ∃ f, Injective f
f : ↑s → β
hf : Injective f
⊢ ∃ f, InjOn f s

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
κ : Type u_4
α : Type u_5
s : Set ι
t : Set κ
u : ι × κ → Set α
⊢ uncurry ⁻¹' (s ×ˢ t).pi u = s.pi fun i ↦ t.pi fun j ↦ u (i, j)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
⊢ x ∈ f '' s ∩ f '' t → x ∈ f '' (s ∩ t)

Tactic:
⟨⟨y, ys, hy⟩, ⟨z, zt, hz⟩⟩

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : z ∈ t
hz : f z = x
⊢ x ∈ f '' (s ∩ t)
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
s : Set ι'
t : (i : ι) → Set (α i)
⊢ (⇑(piCongrLeft α f).symm ⁻¹' s.pi fun i' ↦ t (f i')) = (⇑f '' s).pi t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : z ∈ t
hz : f z = x
⊢ y = z

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
t : (i : ι) → Set (α i)
⊢ (⇑(piCongrLeft α f).symm ⁻¹' univ.pi fun i' ↦ t (f i')) = univ.pi t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
⊢ f '' (s ∩ t) = f '' s ∩ f '' t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : InjOn f s
s₁ : Set α
hs₁ : s₁ ∈ 𝒫 s
s₂ : Set α
hs₂ : s₂ ∈ 𝒫 s
h' : f '' s₁ = f '' s₂
⊢ s₁ = s₂

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
s : Set ι'
t : (i : ι) → Set (α i)
⊢ ⇑(piCongrLeft α f) ⁻¹' (⇑f '' s).pi t = s.pi fun i ↦ t (f i)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
t : (i : ι) → Set (α i)
⊢ ⇑(piCongrLeft α f) ⁻¹' univ.pi t = univ.pi fun i ↦ t (f i)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
f : α → β
h : InjOn f s
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
⊢ f '' s₁ ⊆ f '' s₂ ↔ s₁ ⊆ s₂

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
π : ι ⊕ ι' → Type u_4
t : (i : ι ⊕ ι') → Set (π i)
⊢ ⇑(sumPiEquivProdPi π).symm ⁻¹' univ.pi t = (univ.pi fun i ↦ t (Sum.inl i)) ×ˢ univ.pi fun i ↦ t (Sum.inr i)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
f : α → β
h : InjOn f s
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
⊢ f '' s₁ ⊂ f '' s₂ ↔ s₁ ⊂ s₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
x : α × β
⊢ x ∈ graphOn f s ↔ x.1 ∈ s ∧ f x.1 = x.2

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ Prod.fst '' graphOn f s = s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ Prod.snd '' graphOn f s = f '' s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s t u : Set α
f : α → β
h : Disjoint s t
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
⊢ Disjoint (f '' s) (f '' t)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ InjOn Prod.fst (graphOn f s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
t : Set α
h : InjOn f s
⊢ f '' s ⊆ f '' (s ∩ 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 α
f : α → β
g : β → γ
⊢ graphOn (g ∘ f) s = (fun x ↦ (x.1, g x.2)) '' graphOn f s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f g : α → β
⊢ graphOn f s = graphOn g s ↔ EqOn f g s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
t : Set α
h : InjOn f s
⊢ f '' (s \ t) = f '' s \ 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
δ : Type u_4
s : Set α
t : Set β
f : α → γ
g : β → δ
⊢ graphOn f s ×ˢ graphOn g t = ⇑(Equiv.prodProdProdComm α γ β δ) ⁻¹' graphOn (Prod.map f g) (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
s : Set α
t : Set β
f : α → γ
g : β → δ
⊢ graphOn (Prod.map f g) (s ×ˢ t) = ⇑(Equiv.prodProdProdComm α β γ δ) ⁻¹' graphOn f s ×ˢ graphOn g t

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : InjOn f s
x✝¹ x✝ : ↑s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h' : imageFactorization f s ⟨x, hx⟩ = imageFactorization f s ⟨y, hy⟩
⊢ ⟨x, hx⟩ = ⟨y, hy⟩

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : Injective (imageFactorization f s)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
x✝ : f x = f y
⊢ imageFactorization f s ⟨x, hx⟩ = imageFactorization f s ⟨y, hy⟩

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : Injective (imageFactorization f s)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
x✝ : f x = f y
⊢ x = y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : α → β
⊢ graphOn f univ = graphOn g univ ↔ f = g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
⊢ ∃ f', range f = graphOn f' univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
⊢ Surjective (Prod.fst ∘ ⇑(Equiv.prodComm β γ) ∘ f)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
⊢ ∀ (g₁ g₂ : α),
    ((⇑(Equiv.prodComm β γ) ∘ f) g₁).1 = ((⇑(Equiv.prodComm β γ) ∘ f) g₂).1 →
      ((⇑(Equiv.prodComm β γ) ∘ f) g₁).2 = ((⇑(Equiv.prodComm β γ) ∘ f) g₂).2

Tactic:
by

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
f : α → β
hf : ∀ ⦃x : α × β⦄, x ∈ s → (x.1, f x.1) ∈ s
⊢ s = graphOn f (Prod.fst '' s)

Tactic:
graphOn,

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
f : α → β
hf : ∀ ⦃x : α × β⦄, x ∈ s → (x.1, f x.1) ∈ s
⊢ s = (fun x ↦ (x, f x)) '' Prod.fst '' s
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
e₂ : γ → β
he₂ : range (⇑(Equiv.prodComm β γ) ∘ f) = graphOn e₂ univ
h : β
i : γ
⊢ e₁ h = i ↔ e₂ i = h

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
e₂ : γ → β
he₂ : range (⇑(Equiv.prodComm β γ) ∘ f) = graphOn e₂ univ
he₁₂ : ∀ (h : β) (i : γ), e₁ h = i ↔ e₂ i = h
h : β
⊢ e₂ (e₁ h) = h

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
⊢ (∃ f, s = graphOn f (Prod.fst '' s)) ↔ InjOn Prod.fst s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝¹ : One M
inst✝ : One N
f g : OneHom M N
h : f.toFun = g.toFun
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
F : Type u_9
inst✝³ : One M
inst✝² : One N
inst✝¹ : FunLike F M N
inst✝ : OneHomClass F M N
f : F
⊢ ⇑f ∘ 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: M : Type u_4
N : Type u_5
F : Type u_9
inst✝⁴ : One M
inst✝³ : One N
inst✝² : FunLike F M N
inst✝¹ : Subsingleton M
inst✝ : OneHomClass F M N
f g : F
x : M
⊢ f x = g x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
x✝ : ∃ f t, s = graphOn f t
f : α → β
t : Set α
hs : s = graphOn f t
⊢ s = graphOn f (Prod.fst '' s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
e₂ : γ → β
he₂ : range (⇑(Equiv.prodComm β γ) ∘ f) = graphOn e₂ univ
he₁₂ : ∀ (h : β) (i : γ), e₁ h = i ↔ e₂ i = h
i : γ
⊢ e₁ (e₂ i) = i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: R : Type u_10
S : Type u_11
F : Type u_12
inst✝³ : One R
inst✝² : One S
inst✝¹ : FunLike F R S
inst✝ : OneHomClass F R S
f : F
x : R
hx : f x ≠ 1
⊢ f x ≠ f 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
⊢ ∃ e, range f = graphOn (⇑e) univ

Tactic:
by

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

Goal state before:
pp: β : Type u_2
γ : Type u_3
s : Set (β × γ)
hs₁ : Bijective (Prod.fst ∘ Subtype.val)
⊢ ∃ f, s = graphOn f univ

Tactic:
by

Goal state after: