mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: case inr
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type ?u.13
val✝ : α
⊢ (fun p ↦ if p.fst = true then inr p.snd else inl p.snd) (Sum.elim (Prod.mk false) (Prod.mk true) (inr val✝)) =
    inr val✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
x✝ : Bool → α
⊢ (fun p b ↦ if b = true then p.snd else p.fst) ((fun f ↦ (f false, f true)) x✝) = x✝

Tactic:
grind

Goal state after:
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : α → Prop
β : α → Type u_10
inst✝ : DecidablePred p
f : (i : α) → β i
⊢ (fun f x ↦ if h : p x then f.fst ⟨x, h⟩ else f.snd ⟨x, h⟩) ((fun f ↦ (fun x ↦ f ↑x, fun x ↦ f ↑x)) f) = f

Tactic:
grind

Goal state after:
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: case fst
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : α → Prop
β : α → Type u_10
inst✝ : DecidablePred p
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
⊢ ((fun f ↦ (fun x ↦ f ↑x, fun x ↦ f ↑x)) ((fun f x ↦ if h : p x then f.fst ⟨x, h⟩ else f.snd ⟨x, h⟩) (f, g))).fst =
    (f, g).fst

Tactic:
grind

Goal state after:
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: case snd
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : α → Prop
β : α → Type u_10
inst✝ : DecidablePred p
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
⊢ ((fun f ↦ (fun x ↦ f ↑x, fun x ↦ f ↑x)) ((fun f x ↦ if h : p x then f.fst ⟨x, h⟩ else f.snd ⟨x, h⟩) (f, g))).snd =
    (f, g).snd

Tactic:
grind

Goal state after:
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
inst✝ : DecidableEq α
i : α
β : α → Type u_10
f : (j : α) → β j
⊢ (fun f j ↦ if h : j = i then ⋯ ▸ f.fst else f.snd ⟨j, h⟩) ((fun f ↦ (f i, fun j ↦ f ↑j)) f) = f

Tactic:
grind

Goal state after:
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: case fst
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
inst✝ : DecidableEq α
i : α
β : α → Type u_10
f : β i × ((j : { j // j ≠ i }) → β ↑j)
⊢ ((fun f ↦ (f i, fun j ↦ f ↑j)) ((fun f j ↦ if h : j = i then ⋯ ▸ f.fst else f.snd ⟨j, h⟩) f)).fst = f.fst

Tactic:
grind

Goal state after:
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: case snd
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
inst✝ : DecidableEq α
i : α
β : α → Type u_10
f : β i × ((j : { j // j ≠ i }) → β ↑j)
x : { j // j ≠ i }
⊢ ((fun f ↦ (f i, fun j ↦ f ↑j)) ((fun f j ↦ if h : j = i then ⋯ ▸ f.fst else f.snd ⟨j, h⟩) f)).snd x = f.snd x

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
b : β
s : Set β
inst✝ : Decidable (b ∈ s)
⊢ (fun x ↦ b) ⁻¹' s = if b ∈ s then univ else ∅

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
p : α → Prop
s : Set (Subtype p)
t : Set α
⊢ s = Subtype.val ⁻¹' t ↔ ∀ (x : α) (h : p x), ⟨x, h⟩ ∈ s ↔ x ∈ t

Tactic:
grind

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

Goal state before:
pp: case mpr
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
⊢ ⟨x, x_in_s⟩ ∈ (Subtype.val ⁻¹' v)ᶜ → ⟨x, x_in_s⟩ ∈ Subtype.val ⁻¹' u

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
a : α
⊢ a ∈ s → f a ∈ f '' s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : α → β
s : Set α
h : ∀ (x : α), f x = g x
⊢ f '' s = g '' s

Tactic:
grind

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

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

Tactic:
grind

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

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

Tactic:
grind

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

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

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
β' : Type u_5
f : β → γ
g : α → β
f' : α → β'
g' : β' → γ
h_comm : ∀ (a : α), f (g a) = g' (f' a)
⊢ f '' g '' s = g' '' f' '' s

Tactic:
grind

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

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

Tactic:
grind

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

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

Tactic:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
⊢ (∀ (a : α) (b : β), a ∈ s₁ ∧ b ∈ t₁ → ¬(a ∈ s₂ ∧ b ∈ t₂)) ↔
    (∀ ⦃a : α⦄, a ∈ s₁ → ¬a ∈ s₂) ∨ ∀ ⦃a : β⦄, a ∈ t₁ → ¬a ∈ t₂

Tactic:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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

Goal state before:
pp: case inr
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a | σ a ≠ a} ⊆ s
i : α
hi : σ i ≠ i
h : σ ((Equiv.symm σ) i) = (Equiv.symm σ) i
⊢ σ i = i

Tactic:
grind

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:
grind

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

Goal state before:
pp: case neg
α : Type u_1
s : Set α
a : α
t : Set α
h : t ∈ 𝒫 insert a s
hs : ¬a ∈ t
⊢ t ∈ 𝒫 s ∪ insert a '' 𝒫 s

Tactic:
grind

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

Goal state before:
pp: case mpr
α : Type u_1
s : Set α
a : α
t : Set α
⊢ t ∈ 𝒫 s ∪ insert a '' 𝒫 s → t ∈ 𝒫 insert a s

Tactic:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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

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

Tactic:
grind

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 simp [piecewise]

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

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

Tactic:
grind

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:
grind

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:
grind

Goal state after:
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:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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) ↔ ∃ a, a ∈ 𝒫 range f ∧ p a

Tactic:
rfl

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

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

Tactic:
grind

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
⊢ s ⊆ t → f ⁻¹' s ⊆ f ⁻¹' t

Tactic:
intro h x

Goal state after:
case mpr
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
h : s ⊆ t
x : β
⊢ x ∈ f ⁻¹' s → x ∈ f ⁻¹' t
Module: Mathlib.Data.Set.Image

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
s : Set α
f : β → α
hs ht : s ⊆ range f
⊢ f ⁻¹' s = f ⁻¹' s

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
ht : t.Nonempty
⊢ ∅ = ∅

Tactic:
rfl

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)
x✝ : β
hxt : x✝ ∈ t
x : α
hxs : x ∈ s
h' : Prod.map f g (x, x✝) = Prod.map f' g' (x, x✝)
⊢ f x = f' x

Tactic:
grind

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)
x✝ : α
hxs : x✝ ∈ s
x : β
hxt : x ∈ t
h' : Prod.map f g (x✝, x) = Prod.map f' g' (x✝, x)
⊢ g x = g' x

Tactic:
grind

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

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

Tactic:
grind

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:
grind

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:
grind

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:
grind

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
p₁ p₂ : Pullback f g
he : (p₁, p₂).1.snd = (p₁, p₂).2.snd
⊢ ⟨(p₁, p₂), he⟩ ∈ map_fst ⁻¹' {p | p.fst = p.snd} ↔ ⟨(p₁, p₂), he⟩ ∈ {p | p.fst = p.snd}

Tactic:
mem_ofPred,

Goal state after:
X : Type u_2
Y : Sort u_3
Z : Type u_1
f : X → Y
g : Z → Y
p₁ p₂ : Pullback f g
he : (p₁, p₂).1.snd = (p₁, p₂).2.snd
⊢ ⟨(p₁, p₂), he⟩ ∈ map_fst ⁻¹' {p | p.fst = p.snd} ↔ fst ⟨(p₁, p₂), he⟩ = snd ⟨(p₁, p₂), he⟩
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:
rfl

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

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_7
α : Type u_8
β : Type u_9
inst✝ : SMul M β
r : M
f : ι → α
g : ι → β
e : α → β
x : α
h✝ : ∃ a, f a = x
⊢ r • g (Classical.choose ⋯) = r • g (Classical.choose h✝)

Tactic:
rfl

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

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_7
α : Type u_8
β : Type u_9
inst✝ : SMul M β
r : M
f : ι → α
g : ι → β
e : α → β
x : α
h✝ : ¬∃ a, f a = x
⊢ r • e x = r • e x

Tactic:
rfl

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:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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

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

Tactic:
rfl

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:
grind

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:
grind

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:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
h : ∀ (x : α), ¬f x ∈ s
⊢ Disjoint s (range f)

Tactic:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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:
rw [disjoint_iff_inter_eq_empty] at h ⊢

Goal state after:
α : Type u_1
β : Type u_2
s t u : Set α
f : α → β
h : s ∩ t = ∅
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
⊢ f '' s ∩ f '' t = ∅
Module: Mathlib.Algebra.Group.Equiv.Defs

Goal state before:
pp: case refl
F : 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
inst✝¹ : EquivLike F α β
ι : Type u_9
M : ι → Type u_10
inst✝ : (i : ι) → Mul (M i)
i : ι
x✝¹ x✝ : M i
__Equiv✝ : M i ≃ M i := Equiv.cast ⋯
⊢ (Equiv.cast ⋯).toFun (x✝¹ * x✝) = (Equiv.cast ⋯).toFun x✝¹ * (Equiv.cast ⋯).toFun x✝

Tactic:
rfl

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f : α → β
p₁ : α → γ
p₂ : β → δ
g : γ → δ
comm : ∀ (a : α), p₂ (f a) = g (p₁ a)
hinj : InjOn g (p₁ '' s)
h1 : MapsTo f s t
h2 : InjOn f s
h3 : SurjOn f s t
a : α
ha : a ∈ s
hb : f a ∈ t
⊢ p₂ (f a) ∈ g '' p₁ '' s

Tactic:
grind

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

Goal state before:
pp: case zero
ι : 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✝ : MulOne M
f : Monoid.End M
⊢ id = ⇑1

Tactic:
rfl

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

Goal state before:
pp: case succ
ι : 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✝ : MulOne M
f : Monoid.End M
n✝ : ℕ
a✝ : (⇑f)^[n✝] = ⇑(npowRec n✝ f)
⊢ ⇑(npowRec n✝ f) ∘ ⇑f = ⇑(npowRec n✝ f * f)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Int.Init

Goal state before:
pp: n : ℕ
h : 0 < n
⊢ ↑(n - 1) = ↑n - 1

Tactic:
grind

Goal state after: