mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Subsemigroup.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
carrier : Set M
mul_mem' : ∀ {a b : M}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier
⊢ { carrier := carrier, mul_mem' := mul_mem' } = ⊤ ↔ carrier = Set.univ

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
carrier : Set M
mul_mem' : ∀ {a b : M}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier
⊢ { carrier := carrier, mul_mem' := mul_mem' } = ⊥ ↔ carrier = ∅

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
inst✝ : Subsingleton (Subsemigroup M)
x y : M
⊢ ∀ (a : M), a ∈ ⊥

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
inst✝ : Subsingleton (Subsemigroup M)
⊢ Subsingleton M

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝ : Mul M
s : Set M
S : Subsemigroup M
hn : Nonempty M
h : ⊥ = ⊤
⊢ False

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Mul M
s : Set M
inst✝ : Mul N
f g : M →ₙ* N
a✝ b✝ : M
hx : f a✝ = g a✝
hy : f b✝ = g b✝
⊢ a✝ * b✝ ∈ {x | f x = g x}

Tactic:
by

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

Goal state before:
pp: S : Type u_3
M : Type u_4
inst✝² : SetLike S M
inst✝¹ : Mul M
inst✝ : MulMemClass S M
s : S
⊢ IsMulCommutative ↥s ↔ ∀ (a : M), a ∈ s → ∀ (b : M), b ∈ s → a * b = b * a

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ univ.pi v
j : ι
x✝ : j ≠ i
⊢ z j ∈ v j

Tactic:
by

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

Goal state before:
pp: ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (univ.pi v).Nonempty
i : ι
⊢ (fun x ↦ x i) '' ⋂ k, (fun x ↦ x k) ⁻¹' v k = v i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
s : Set α
t : (i : ι) → κ i → Set β
f : α → β
⊢ MapsTo f s (⋂ i, ⋂ j, t i j) ↔ ∀ (i : ι) (j : κ i), MapsTo f s (t i j)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
S : Set (Set α)
f : α → β
⊢ f '' ⋂₀ S ⊆ ⋂ s ∈ S, f '' s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Set α
S : Set (Set β)
f : α → β → γ
⊢ image2 f t (⋂₀ S) ⊆ ⋂ s ∈ S, image2 f t s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
S : Set (Set α)
t : Set β
f : α → β → γ
⊢ image2 f (⋂₀ S) t ⊆ ⋂ s ∈ S, image2 f s t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
⊢ Injective f ↔ ∀ (i : ι), Injective ((U i).restrictPreimage f)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
⊢ Surjective f ↔ ∀ (i : ι), Surjective ((U i).restrictPreimage f)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
⊢ Bijective f ↔ ∀ (i : ι), Bijective ((U i).restrictPreimage f)

Tactic:
by

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

Goal state before:
pp: M : Type u_3
A : Type u_4
inst✝² : Monoid M
inst✝¹ : SetLike A M
inst✝ : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
⊢ x ^ 0 ∈ S

Tactic:
by

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

Goal state before:
pp: M : Type u_3
A : Type u_4
inst✝² : Monoid M
inst✝¹ : SetLike A M
inst✝ : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
n : ℕ
⊢ x ^ (n + 1) ∈ S

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
x✝¹ x✝ : Submonoid M
s : Subsemigroup M
hs : 1 ∈ s.carrier
t : Subsemigroup M
ht : 1 ∈ t.carrier
⊢ { toSubsemigroup := s, one_mem' := hs }.toSubsemigroup = { toSubsemigroup := t, one_mem' := ht }.toSubsemigroup →
    { toSubsemigroup := s, one_mem' := hs } = { toSubsemigroup := t, one_mem' := ht }

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝ : MulOneClass M
s : Set M
S : Submonoid M
a✝ b✝ : M
ha : a✝ ∈ {1}
hb : b✝ ∈ {1}
⊢ a✝ * b✝ ∈ {1}

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
toSubsemigroup : Subsemigroup M
one_mem' : 1 ∈ toSubsemigroup.carrier
⊢ { toSubsemigroup := toSubsemigroup, one_mem' := one_mem' } = ⊤ ↔ toSubsemigroup = ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ i, s i)
inhabited_h : Inhabited ι
y : β
x : ι → α
hx : ∀ (i : ι), x i ∈ s i
hy : ∀ (i : ι), f (x i) = y
i : ι
this : x default = x i
⊢ x default ∈ s i

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
toSubsemigroup : Subsemigroup M
one_mem' : 1 ∈ toSubsemigroup.carrier
⊢ { toSubsemigroup := toSubsemigroup, one_mem' := one_mem' } = ⊥ ↔ ↑toSubsemigroup = {1}

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
x✝ : Subsingleton M
x y : Submonoid M
i : M
⊢ i ∈ x ↔ i ∈ y

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
s : Set M
inst✝ : MulOneClass N
f g : M →* N
a✝ b✝ : M
hx : f a✝ = g a✝
hy : f b✝ = g b✝
⊢ a✝ * b✝ ∈ {x | f x = g x}

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
s : Set M
inst✝ : MulOneClass N
f g : M →* N
⊢ 1 ∈ {x | f x = g x}

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
x✝¹ x✝ : ↥S'
⊢ ↑(x✝¹ * x✝) = ↑x✝¹ * ↑x✝

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : MulOneClass M
S : Submonoid M
a : M
ha : a ∈ S
⊢ ⟨a, ha⟩ = 1 ↔ a = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ i, s i)
⊢ f '' ⋂ i, s i = ⋂ i, f '' s i

Tactic:
by

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

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
A : Type u_3
inst✝² : MulOneClass M✝
inst✝¹ : SetLike A M✝
hA : SubmonoidClass A M✝
S' : A
M : Type u_4
inst✝ : MulOneClass M
S : Submonoid M
x✝¹ x✝ : ↥S
⊢ ↑(x✝¹ * x✝) = ↑x✝¹ * ↑x✝

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
p : ι → Prop
s : (i : ι) → p i → Set α
hp : ∃ i, p i
f : α → β
h : InjOn f (⋃ i, ⋃ (hi : p i), s i hi)
⊢ f '' ⋂ i, ⋂ (hi : p i), s i hi = ⋂ i, ⋂ (hi : p i), f '' s i hi

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝ : Mul M
s✝ : Set M
S : Subsemigroup M
s : Set (Subsemigroup M)
a✝ b✝ : M
hx : a✝ ∈ ⋂ t ∈ s, ↑t
hy : b✝ ∈ ⋂ t ∈ s, ↑t
i : Subsemigroup M
h : i ∈ s
⊢ a✝ ∈ i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝ : Mul M
s✝ : Set M
S : Subsemigroup M
s : Set (Subsemigroup M)
a✝ b✝ : M
hx : a✝ ∈ ⋂ t ∈ s, ↑t
hy : b✝ ∈ ⋂ t ∈ s, ↑t
i : Subsemigroup M
h : i ∈ s
⊢ b✝ ∈ i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Basic

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
x : M
⊢ x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Basic

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
⊢ ↑(⨅ i, S i) = ⋂ i, ↑(S i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Basic

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
s : Set M
p : (x y : M) → x ∈ closure s → y ∈ closure s → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
mul_left :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p z x hz hx → p z y hz hy → p z (x * y) hz ⋯
x y : M
hx : x ∈ closure s
hy : y ∈ closure s
⊢ p x y hx hy

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Basic

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
p : M → Prop
s : Set M
closure : Subsemigroup.closure s = ⊤
mem : ∀ x ∈ s, p x
mul : ∀ (x y : M), p x → p y → p (x * y)
x : M
⊢ p x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
hf : Bijective f
s : ι → Set α
⊢ f '' ⋂ i, s i = ⋂ i, f '' s i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝ : Mul M
s✝ : Set M
S : Subsemigroup M
p : M → Prop
s : Set M
closure : Subsemigroup.closure s = ⊤
mem : ∀ x ∈ s, p x
mul : ∀ (x y : M), p x → p y → p (x * y)
x : M
⊢ p x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
f : α → β
hf : Bijective f
s : (i : ι) → κ i → Set α
⊢ f '' ⋂ i, ⋂ j, s i j = ⋂ i, ⋂ j, f '' s i j

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Basic

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
m : M
p : Subsemigroup M
⊢ closure {m} ≤ p ↔ m ∈ p

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
⊢ InjOn f (⋃ i, s i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Basic

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
ι : Sort u_3
p : ι → Subsemigroup M
m : M
⊢ m ∈ ⨆ i, p i ↔ ∀ (N : Subsemigroup M), (∀ (i : ι), p i ≤ N) → m ∈ N

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : ι → Set α
t : Set β
f : α → β
H : ∀ (i : ι), SurjOn f (s i) t
Hinj : InjOn f (⋃ i, s i)
⊢ SurjOn f (⋂ i, s i) t

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Basic

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
ι : Sort u_3
p : ι → Subsemigroup M
⊢ ⨆ i, p i = closure (⋃ i, ↑(p i))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
s : ι → Set α
⊢ f '' ⋃ i, s i = ⋃ i, f '' s i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
f : α → β
s : (i : ι) → κ i → Set α
⊢ f '' ⋃ i, ⋃ j, s i j = ⋃ i, ⋃ j, f '' s i j

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : α → Prop
x✝ : Subtype p
x : α
h : p x
⊢ ⟨x, h⟩ ∈ univ ↔ ⟨x, h⟩ ∈ ⋃ x, ⋃ (h : p x), {⟨x, h⟩}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Basic

Goal state before:
pp: M✝ : Type u_1
N✝ : Type u_2
M : Type ?u.6
N : Type ?u.8
inst✝¹ : Semigroup M
inst✝ : Semigroup N
s : Set M
f : M → N
hs : closure s = ⊤
hmul : ∀ (x y : M), y ∈ s → f (x * y) = f x * f y
x✝ y y₁ y₂ : M
h₁ : ∀ (x : M), f (x * y₁) = f x * f y₁
h₂ : ∀ (x : M), f (x * y₂) = f x * f y₂
x : M
⊢ f (x * (y₁ * y₂)) = f x * f (y₁ * y₂)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Sort u_9
f : ι → α
a : α
⊢ a ∈ range f ↔ a ∈ ⋃ i, {f i}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
b : β
⊢ b ∈ f '' s ↔ b ∈ ⋃ i ∈ s, {f i}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : ι → α
g : α → Set β
⊢ ⋃ x, ⋃ y, ⋃ (_ : f y = x), g x = ⋃ y, g (f y)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : ι → α
g : α → Set β
⊢ ⋂ x, ⋂ y, ⋂ (_ : f y = x), g x = ⋂ y, g (f y)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Sort u_9
κ : Sort u_10
f : ι → Set α
g : κ → Set α
⊢ (⋃ i, f i) ∩ ⋃ j, g j = ⋃ i, ⋃ j, f i ∩ g j

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Sort u_9
κ : Sort u_10
f : ι → Set α
g : κ → Set α
⊢ (⋂ i, f i) ∪ ⋂ j, g j = ⋂ i, ⋂ j, f i ∪ g j

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι₁ : Sort u_9
κ₁ : Sort u_10
ι₂ : ι₁ → Sort u_11
k₂ : κ₁ → Sort u_12
f : (i₁ : ι₁) → ι₂ i₁ → Set α
g : (j₁ : κ₁) → k₂ j₁ → Set α
⊢ (⋃ i₁, ⋃ i₂, f i₁ i₂) ∩ ⋃ j₁, ⋃ j₂, g j₁ j₂ = ⋃ i₁, ⋃ i₂, ⋃ j₁, ⋃ j₂, f i₁ i₂ ∩ g j₁ j₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι₁ : Sort u_9
κ₁ : Sort u_10
ι₂ : ι₁ → Sort u_11
k₂ : κ₁ → Sort u_12
f : (i₁ : ι₁) → ι₂ i₁ → Set α
g : (j₁ : κ₁) → k₂ j₁ → Set α
⊢ (⋂ i₁, ⋂ i₂, f i₁ i₂) ∪ ⋂ j₁, ⋂ j₂, g j₁ j₂ = ⋂ i₁, ⋂ i₂, ⋂ j₁, ⋂ j₂, f i₁ i₂ ∪ g j₁ j₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
s : ι → Set β
⊢ ∀ (x : α), x ∈ f ⁻¹' ⋃ i, s i ↔ x ∈ ⋃ i, f ⁻¹' s i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
f : α → β
s : (i : ι) → κ i → Set β
⊢ f ⁻¹' ⋃ i, ⋃ j, s i j = ⋃ i, ⋃ j, f ⁻¹' s i j

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set (Set α)
⊢ f '' ⋃₀ s = ⋃₀ (image f '' s)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
s : ι → Set β
⊢ f ⁻¹' ⋂ i, s i = ⋂ i, f ⁻¹' s i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
f : α → β
s : (i : ι) → κ i → Set β
⊢ f ⁻¹' ⋂ i, ⋂ j, s i j = ⋂ i, ⋂ j, f ⁻¹' s i j

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ ⋃ y ∈ s, f ⁻¹' {y} = f ⁻¹' s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ ⋃ y ∈ range f, f ⁻¹' {y} = univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
s : Set α
t : ι → Set β
⊢ s ×ˢ ⋃ i, t i = ⋃ i, s ×ˢ t i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
s : Set α
t : (i : ι) → κ i → Set β
⊢ s ×ˢ ⋃ i, ⋃ j, t i j = ⋃ i, ⋃ j, s ×ˢ t i j

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : One α
inst✝ : One β
⊢ 1 ×ˢ 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
s : Set α
a : α
⊢ a⁻¹ ∈ s⁻¹ ↔ a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
s : Set α
⊢ s⁻¹ = ∅ ↔ s = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : InvolutiveInv α
s✝ t : Set α
a : α
s : Set α
⊢ s⁻¹⁻¹ = s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
s t : Set α
⊢ s⁻¹ ⊆ t ↔ s ⊆ t⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
a : α
⊢ {a}⁻¹ = {a⁻¹}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
C : Set (Set β)
⊢ s ×ˢ ⋃₀ C = ⋃₀ ((fun t ↦ s ×ˢ t) '' C)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
a : α
s : Set α
⊢ (insert a s)⁻¹ = insert a⁻¹ s⁻¹

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
t : Set β
⊢ (⋃ i, s i) ×ˢ t = ⋃ i, s i ×ˢ t

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
ι : Sort u_5
f : ι → α
⊢ (range f)⁻¹ = range fun i ↦ (f i)⁻¹

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
M : ι → Type u_3
N : ι → Type u_4
i : I
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : ∀ (i : ι), IsMulTorsionFree (M i)
n : ℕ
hn : n ≠ 0
a b : (i : ι) → M i
hab : (fun a ↦ a ^ n) a = (fun a ↦ a ^ n) b
⊢ a = b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
t : Set β
⊢ (⋃ i, ⋃ j, s i j) ×ˢ t = ⋃ i, ⋃ j, s i j ×ˢ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
C : Set (Set α)
t : Set β
⊢ ⋃₀ C ×ˢ t = ⋃₀ ((fun s ↦ s ×ˢ t) '' C)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
I✝ : Type u
f✝ : I✝ → Type v
M : ι → Type u_3
N : ι → Type u_4
i : I✝
inst✝² : (i : I✝) → Mul (f✝ i)
α : Type u_5
β : Type u_6
inst✝¹ : Mul α
inst✝ : Mul β
f : α →ₙ* β
I : Type u_7
x✝¹ x✝ : I → α
⊢ ⇑f ∘ (x✝¹ * x✝) = ⇑f ∘ x✝¹ * ⇑f ∘ x✝

Tactic:
by

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

Goal state before:
pp: ι : Type u_9
ι' : Type u_10
α : Type u_11
β : Type u_12
s : ι → Set α
t : ι' → Set β
⊢ ⋃ x, s x.1 ×ˢ t x.2 = (⋃ i, s i) ×ˢ ⋃ i, t i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : InvolutiveInv α
s : Set α
f g : α → β
H : ∀ (x : α), x ∈ s → f x⁻¹ = g x
⊢ f '' s⁻¹ = g '' s

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
I✝ : Type u
f✝ : I✝ → Type v
M : ι → Type u_3
N : ι → Type u_4
i : I✝
inst✝² : (i : I✝) → MulOneClass (f✝ i)
α : Type u_5
β : Type u_6
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
I : Type u_7
⊢ ⇑f ∘ 1 = 1

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
I✝ : Type u
f✝ : I✝ → Type v
M : ι → Type u_3
N : ι → Type u_4
i : I✝
inst✝² : (i : I✝) → MulOneClass (f✝ i)
α : Type u_5
β : Type u_6
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
I : Type u_7
x✝¹ x✝ : I → α
⊢ ⇑f ∘ (x✝¹ * x✝) = ⇑f ∘ x✝¹ * ⇑f ∘ x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : InvolutiveInv α
s : Set α
inst✝ : InvolutiveInv β
f g : α → β
H : ∀ (x : α), x ∈ s → f x⁻¹ = (g x)⁻¹
⊢ f '' s⁻¹ = (g '' s)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
s : Set α
p : α → Prop
⊢ (∀ (x : α), x⁻¹ ∈ s → p x) ↔ ∀ (x : α), x ∈ s → p x⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
s : Set α
p : α → Prop
⊢ (∃ x, x⁻¹ ∈ s ∧ p x) ↔ ∃ x, x ∈ s ∧ p x⁻¹

Tactic:
by

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

Goal state before:
pp: I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
⊢ Pairwise fun i j ↦ ∀ (x : f i) (y : f j), Commute (mulSingle i x) (mulSingle j y)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
s : Set α
⊢ op '' s⁻¹ = (op '' s)⁻¹

Tactic:
by

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

Goal state before:
pp: I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
x : (i : I) → f i
i j : I
⊢ Commute (mulSingle i (x i)) (mulSingle j (x j))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
⊢ ⋃ x, s x ×ˢ t x = (⋃ x, s x) ×ˢ ⋃ x, t x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Mul α
inst✝ : Mul β
s₁ s₂ : Set α
t₁ t₂ : Set β
⊢ s₁ ×ˢ t₁ * s₂ ×ˢ t₂ = (s₁ * s₂) ×ˢ (t₁ * t₂)

Tactic:
by

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

Goal state before:
pp: I : Type u
f : I → Type v
i : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Group (f i)
g : (i : I) → f i
x : f i
⊢ Function.update g i x = g / mulSingle i (g i) * mulSingle i x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Div α
inst✝ : Div β
s₁ s₂ : Set α
t₁ t₂ : Set β
⊢ s₁ ×ˢ t₁ / s₂ ×ˢ t₂ = (s₁ / s₂) ×ˢ (t₁ / t₂)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
hs : 1 ∈ s
hn : n ≠ 0
⊢ s ⊆ s ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
n✝ n : ℕ
hn : n + 1 ≠ 0
⊢ ∅ ^ (n + 1) = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
s : Set α
hs : s.Nonempty
⊢ (s ^ 0).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
s : Set α
hs : s.Nonempty
n : ℕ
⊢ (s ^ (n + 1)).Nonempty

Tactic:
by

Goal state after: