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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
f : ι → α
⊢ range f = ∅ ↔ IsEmpty ι

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
f : ι → α
inst✝ : Nonempty ι
y : α
h : ∀ (x : α), (∃ y, f y = x) ↔ x = y
x✝ : ι
⊢ f x✝ = y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
f : ι → α
inst✝ : Nonempty ι
y : α
h : ∀ (x : ι), f x = y
x✝ : α
⊢ (∃ y, f y = x✝) ↔ x✝ = y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
f : ι → α
inst✝ : Nonempty ι
y : α
⊢ range f = {y} ↔ ∀ (x : ι), f x = y

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
heq : s ×ˢ t = s₁ ×ˢ t₁
⊢ (s₁ ×ˢ t₁).Nonempty

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
x : α
⊢ insert (f x) (f '' {x}ᶜ) = range f

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
t : Set β
⊢ f '' f ⁻¹' t = t ∩ 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 β
hs : s ⊆ range f
⊢ f '' f ⁻¹' s = 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₁ g₂ : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g₁ i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g₂ i
⊢ s.piecewise f₁ f₂ ≤ s.piecewise g₁ g₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f '' f ⁻¹' s = s ↔ s ⊆ range 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
inst✝¹ : (j : α) → Decidable (j ∈ s)
i j : α
h : i ≠ j
inst✝ : (i : α) → Decidable (i ∈ insert j s)
⊢ (insert j s).piecewise f g i = s.piecewise f g i

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✝ : (i : α) → Decidable (i ∈ sᶜ)
x : α
hx : x ∈ s
⊢ sᶜ.piecewise f g x = s.piecewise g f x

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✝ : (i : α) → Decidable (i ∈ sᶜ)
x : α
hx : ¬x ∈ s
⊢ sᶜ.piecewise f g x = s.piecewise g f x

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
t t₁ t₂ : Set β
f₁ f₂ : α → β
inst✝ : (i : α) → Decidable (i ∈ s)
h₁ : MapsTo f₁ (s₁ ∩ s) (t₁ ∩ t)
h₂ : MapsTo f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ)
⊢ MapsTo (s.piecewise f₁ f₂) (s.ite s₁ s₂) (t.ite t₁ t₂)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t : Set α
⊢ EqOn (s.piecewise f f') g t ↔ EqOn f g (t ∩ s) ∧ EqOn f' g (t ∩ sᶜ)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t t' : Set α
h : EqOn f g (t ∩ s)
h' : EqOn f' g (t' ∩ sᶜ)
⊢ EqOn (s.piecewise f f') g (s.ite t 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 β
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
s t : Set α
f : β → α
hs : s ⊆ range f
⊢ f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
t : Set β
x : α
⊢ x ∈ s.piecewise f g ⁻¹' t ↔ x ∈ s.ite (f ⁻¹' t) (g ⁻¹' t)

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)
δ' : α → Sort u_8
h : (i : α) → δ i → δ' i
x : α
⊢ h x (s.piecewise f g x) = s.piecewise (fun x ↦ h x (f x)) (fun x ↦ h x (g x)) x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
⊢ f ⁻¹' s = f ⁻¹' 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 β
⊢ f ⁻¹' (s ∩ range f) = f ⁻¹' s

Tactic:
preimage_inter_range

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f ⁻¹' s = f ⁻¹' s
Module: Mathlib.Data.Set.Image

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ range Sum.inl = {x | x.isLeft = true}

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)
δ' : α → Sort u_8
δ'' : α → Sort u_9
f' g' : (i : α) → δ' i
h : (i : α) → δ i → δ' i → δ'' i
x : α
⊢ h x (s.piecewise f g x) (s.piecewise f' g' x) = s.piecewise (fun x ↦ h x (f x) (f' x)) (fun x ↦ h x (g x) (g' x)) x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ range Sum.inr = {x | x.isRight = true}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ range Sum.inl ⊓ range Sum.inr ⊆ ⊥

Tactic:
by

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

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

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 = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ ⊤ ⊆ range Sum.inl ⊔ range Sum.inr

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set β
⊢ Sum.inl ⁻¹' Sum.inr '' 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 β
ht : t.Nonempty
⊢ s ×ˢ t = s₁ ×ˢ t ↔ s = s₁

Tactic:
by

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

Goal state before:
pp: α : Type u_1
γ : Type u_3
δ : Type u_4
s : Set α
a b : α → γ × δ
⊢ EqOn a b s ↔ EqOn (Prod.fst ∘ a) (Prod.fst ∘ b) s ∧ EqOn (Prod.snd ∘ a) (Prod.snd ∘ b) s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
⊢ Sum.inr ⁻¹' Sum.inl '' 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 β
f f' : α → γ
g g' : β → δ
h : EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)
ht : t.Nonempty
⊢ EqOn f f' s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ Sum.inl ⁻¹' range Sum.inr = ∅

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 f' : α → γ
g g' : β → δ
h : EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)
hs : s.Nonempty
⊢ EqOn g g' t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ Sum.inr ⁻¹' range Sum.inl = ∅

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 f' : α → γ
g g' : β → δ
hf : EqOn f f' s
hg : EqOn g g' t
⊢ EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
⊢ range (s.piecewise f g) = f '' s ∪ g '' sᶜ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ (Prod.map (fun x ↦ ↑x) fun x ↦ ↑x) ⁻¹' diagonal α = diagonal ↑s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
⊢ range Function.diag = diagonal α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set (α × α)
⊢ diagonal α ⊆ s ↔ ∀ (x : α), (x, x) ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set γ
f : α → γ
g : β → γ
⊢ Sum.elim f g ⁻¹' s = Sum.inl '' f ⁻¹' s ∪ Sum.inr '' g ⁻¹' s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ Function.diag '' s = diagonal α ∩ s ×ˢ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
⊢ diagonal α = univ ↔ Subsingleton α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set (α ⊕ β)
⊢ Sum.inl '' Sum.inl ⁻¹' s ∪ Sum.inr '' Sum.inr ⁻¹' s = s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set (α ⊕ β)
f : α → γ
g : β → γ
⊢ Sum.elim f g '' s = f '' Sum.inl ⁻¹' s ∪ g '' Sum.inr ⁻¹' s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
⊢ range (Subtype.map f h) = Subtype.val ⁻¹' f '' {x | p x}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
hβ : Nonempty β
⊢ range (const α) = {f | ∀ (x y : α), f x = f y}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
f : ι → α
x : α
⊢ range f ⊆ {x} ↔ f = const ι x

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
⊢ Injective (s.piecewise f g) ↔ InjOn f s ∧ InjOn g sᶜ ∧ ∀ (x : α), x ∈ s → ∀ (y : α), ¬y ∈ s → f x ≠ g y

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 fun x ↦ f ↑x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : Prop
inst✝ : Decidable p
f g : α → β
⊢ range (if p then f else g) ⊆ range f ∪ range g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f g : α → β
⊢ (range fun x ↦ if p x then f x else g x) ⊆ range f ∪ range g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
f : ι → α
inst✝ : Unique ι
⊢ range f = {f default}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
s : Set α
f : ↑(insert x s) → β
⊢ range f = insert (f ⟨x, ⋯⟩) (range fun y ↦ f ⟨↑y, ⋯⟩)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
⊢ range (inclusion h) = {x | ↑x ∈ s}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
x : ↑(range f)
⊢ rangeFactorization f (rangeSplitting f x) = x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
hf : Monotone f
⊢ StrictMono (rangeSplitting f)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
δ : α → Type u_8
t : Set α
t' : (i : α) → Set (δ i)
f g : (i : α) → δ i
hf : f ∈ t.pi t'
hg : g ∈ t.pi t'
⊢ s.piecewise f g ∈ t.pi t'

Tactic:
by

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

Goal state before:
pp: ι : Type u_8
α : ι → Type u_9
s : Set ι
t t' : (i : ι) → Set (α i)
inst✝ : (x : ι) → Decidable (x ∈ s)
⊢ univ.pi (s.piecewise t t') = s.pi t ∩ sᶜ.pi t'

Tactic:
by

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

Goal state before:
pp: X : Type u_2
Y : Sort u_3
Z : Type u_1
f : X → Y
g : Z → Y
⊢ map_fst ⁻¹' pullbackDiagonal f = pullbackDiagonal snd

Tactic:
by

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

Goal state before:
pp: ι : Type u_8
α : ι → Type u_9
s : Set ι
t : (i : ι) → Set (α i)
inst✝ : (x : ι) → Decidable (x ∈ s)
⊢ univ.pi (s.piecewise t fun x ↦ univ) = s.pi t

Tactic:
by

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

Goal state before:
pp: X : Type ?u.21
Y : Sort ?u.6
Z : Type ?u.22
f : X → Y
g : Z → X
inj : Injective g
⊢ f ∘ g = id ∘ f ∘ g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pi

Goal state before:
pp: ι : Type u_1
M : Type u_2
α : ι → Type u_4
inst✝² : (i : ι) → SMul M (α i)
inst✝¹ : ∀ (i : ι), Nonempty (α i)
i : ι
inst✝ : FaithfulSMul M (α i)
m₁✝ m₂✝ : M
h : ∀ (a : (i : ι) → α i), m₁✝ • a = m₂✝ • a
a : α i
⊢ m₁✝ • a = m₂✝ • a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pi

Goal state before:
pp: ι : Type u_1
M : Type u_7
α : Type u_8
β : Type u_9
inst✝ : SMul M β
r : M
f : ι → α
g : ι → β
e : α → β
⊢ extend f (r • g) (r • e) = r • extend f g e

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Sort u_2
f : X → Y
s : Set X
⊢ toPullbackDiag f '' s = pullbackDiagonal f ∩ Subtype.val ⁻¹' s ×ˢ s

Tactic:
by

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

Goal state before:
pp: α : Type u_5
β : Type u_6
γ : Type u_7
γ' : Type u_8
δ : Type u_9
δ' : Type u_10
h : β → α
f : γ → β
f₁ : γ' → α
f₂ : γ → γ'
g : δ → β
g₁ : δ' → α
g₂ : δ → δ'
hf : h ∘ f = f₁ ∘ f₂
hg : h ∘ g = g₁ ∘ g₂
hfg : range f ∪ range g = univ
s : Set β
⊢ h '' s = f₁ '' f₂ '' f ⁻¹' s ∪ g₁ '' g₂ '' g ⁻¹' s

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Sort u_2
f : X → Y
⊢ range (toPullbackDiag f) = pullbackDiagonal f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.offDiag.Nonempty ↔ s.Nontrivial

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.offDiag = ∅ ↔ s.Subsingleton

Tactic:
by

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

Goal state before:
pp: α : Type u_1
⊢ ∅.offDiag = ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
⊢ {a}.offDiag = ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (x : α × α), x ∈ univ.offDiag ↔ x ∈ (diagonal α)ᶜ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Set α
x : α × α
⊢ x ∈ (s ∩ t).offDiag ↔ x ∈ s.offDiag ∩ t.offDiag

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 : Set β
hs : (f ⁻¹' s).Subsingleton
fx : β
hx : fx ∈ s
fy : β
hy : fy ∈ s
⊢ fx = fy

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
hs : s.Nontrivial
hf : Surjective f
⊢ (f ⁻¹' s).Nontrivial

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Nontrivial
hf : InjOn f s
⊢ (f '' s).Nontrivial

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
⊢ Surjective (image f)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : Disjoint s t
⊢ (s ∪ t).offDiag = s.offDiag ∪ t.offDiag ∪ s ×ˢ t ∪ t ×ˢ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
ha : ¬a ∈ s
⊢ (insert a s).offDiag = s.offDiag ∪ {a} ×ˢ s ∪ s ×ˢ {a}

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : (i : ι) → Set (α i)
⊢ ∅.pi s = univ

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
inst✝ : DecidablePred fun x ↦ x ∈ s
t : (i : ι) → Set (α i)
⊢ (univ.pi fun i ↦ if i ∈ s then t i else univ) = s.pi 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₁ : (i : ι) → Set (α i)
⊢ (s.pi fun i ↦ t i ∩ t₁ i) = s.pi t ∩ s.pi 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₂ : (i : ι) → Set (α i)
h : s₁ = s₂
h' : ∀ (i : ι), i ∈ s₁ → t₁ i = t₂ i
⊢ s₁.pi t₁ = s₂.pi 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)
i : ι
hs : i ∈ s
ht : 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
s : Set ι
t : (i : ι) → Set (α i)
⊢ (s.pi t).Nonempty ↔ ∀ (i : ι), ∃ x, i ∈ s → x ∈ 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)
⊢ (univ.pi t).Nonempty ↔ ∀ (i : ι), (t i).Nonempty

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 : Set β
⊢ (f ⁻¹' s).Nonempty ↔ s.Nonempty

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.pi t = ∅ ↔ ∃ i, IsEmpty (α i) ∨ i ∈ s ∧ 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)
⊢ univ.pi t = ∅ ↔ ∃ i, t i = ∅

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)
⊢ Disjoint (univ.pi t₁) (univ.pi t₂) ↔ ∃ i, Disjoint (t₁ i) (t₂ i)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : Unique ι
t : (i : ι) → Set (α i)
⊢ uniqueElim ⁻¹' univ.pi t = t default

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✝ : ∀ (i : ι), Nonempty (α i)
⊢ s.pi t = ∅ ↔ ∃ i, i ∈ s ∧ 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₁ t₂ : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), Nonempty (α i)
⊢ Disjoint (s.pi t₁) (s.pi t₂) ↔ ∃ i, i ∈ s ∧ Disjoint (t₁ i) (t₂ i)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
i : ι
s : Set ι
t : (i : ι) → Set (α i)
⊢ (insert i s).pi t = eval 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
i : ι
t : (i : ι) → Set (α i)
⊢ {i}.pi t = eval i ⁻¹' t i

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f g : (i : ι) → α i
⊢ (g ∈ univ.pi fun i ↦ {f i}) ↔ g ∈ {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
⊢ Injective (image f)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
g : β → α
h : LeftInverse g f
s : Set α
⊢ g '' f '' s = s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
g : β → α
h : LeftInverse g f
s : Set α
⊢ f ⁻¹' g ⁻¹' s = s

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 α
⊢ f '' s = range f ∩ g ⁻¹' s

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
⊢ (s.pi fun i ↦ if p i then t₁ i else t₂ i) = {i | i ∈ s ∧ p i}.pi t₁ ∩ {i | i ∈ s ∧ ¬p i}.pi t₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : t ⊆ s
⊢ val '' {x | ↑x ∈ t} = t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ range val = 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 : (i : ι) → Set (α i)
⊢ (s₁ ∪ s₂).pi t = s₁.pi t ∩ s₂.pi t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ val ⁻¹' s = univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
t : Set ↑s
x : α
x✝ : x ∈ val '' t
y : { x // x ∈ s }
left✝ : y ∈ t
yvaleq : ↑y = x
⊢ x ∈ 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₂ : (i : ι) → Set (α i)
ht₁ : ∀ (i : ι), ¬i ∈ s₁ → t₁ i = univ
ht₂ : ∀ (i : ι), ¬i ∈ s₂ → t₂ i = univ
⊢ ((s₁ ∪ s₂).pi fun i ↦ t₁ i ∩ t₂ i) = s₁.pi t₁ ∩ s₂.pi t₂

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.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
s : Set ι
⊢ s.pi t ∩ sᶜ.pi t = univ.pi t

Tactic:
by

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

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

Tactic:
by

Goal state after: