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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
s t : Set α
h : SurjOn (⇑g) s t
b : α
hb : b ∈ s
ha : g b ∈ t
⊢ (g.extendDomain f) ((Subtype.val ∘ ⇑f) b) = (Subtype.val ∘ ⇑f) (g b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
s t : Set α
h : SurjOn (⇑g) s t
⊢ SurjOn (⇑(g.extendDomain f)) (Subtype.val ∘ ⇑f '' s) (Subtype.val ∘ ⇑f '' t)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
s : Set α
h : LeftInvOn (⇑g₁) (⇑g₂) s
⊢ LeftInvOn (⇑(g₁.extendDomain f)) (⇑(g₂.extendDomain f)) (Subtype.val ∘ ⇑f '' s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
t : Set α
h : RightInvOn (⇑g₁) (⇑g₂) t
⊢ RightInvOn (⇑(g₁.extendDomain f)) (⇑(g₂.extendDomain f)) (Subtype.val ∘ ⇑f '' t)

Tactic:
by

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

Goal state before:
pp: β₁ : Type u_8
β₂ : Type u_9
t₁ : Set β₁
t₂ : Set β₂
h✝ : t₂.Nonempty
x✝ : β₁
h : x✝ ∈ t₁
⊢ x✝ ∈ Prod.fst '' t₁ ×ˢ t₂

Tactic:
by

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

Goal state before:
pp: β₁ : Type u_8
β₂ : Type u_9
t₁ : Set β₁
t₂ : Set β₂
h✝ : t₁.Nonempty
x✝ : β₂
h : x✝ ∈ t₂
⊢ x✝ ∈ Prod.snd '' t₁ ×ˢ t₂

Tactic:
by

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

Goal state before:
pp: β₁ : Type u_8
β₂ : Type u_9
t₁ : Set β₁
t₂ : Set β₂
⊢ SurjOn Prod.fst (t₁ ×ˢ t₂) t₁ → t₁ = ∅ ∨ t₂.Nonempty

Tactic:
by

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

Goal state before:
pp: β₁ : Type u_8
β₂ : Type u_9
t₁ : Set β₁
t₂ : Set β₂
⊢ t₁ = ∅ ∨ t₂.Nonempty → SurjOn Prod.fst (t₁ ×ˢ t₂) t₁

Tactic:
by

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

Goal state before:
pp: β₁ : Type u_8
β₂ : Type u_9
t₁ : Set β₁
t₂ : Set β₂
⊢ SurjOn Prod.snd (t₁ ×ˢ t₂) t₂ → t₁.Nonempty ∨ t₂ = ∅

Tactic:
by

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

Goal state before:
pp: β₁ : Type u_8
β₂ : Type u_9
t₁ : Set β₁
t₂ : Set β₂
⊢ t₁.Nonempty ∨ t₂ = ∅ → SurjOn Prod.snd (t₁ ×ˢ t₂) t₂

Tactic:
by

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

Goal state before:
pp: α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
h₁ : InjOn f₁ s₁
h₂ : InjOn f₂ s₂
x : α₁ × α₂
hx : x ∈ s₁ ×ˢ s₂
y : α₁ × α₂
hy : y ∈ s₁ ×ˢ s₂
⊢ (fun x ↦ (f₁ x.1, f₂ x.2)) x = (fun x ↦ (f₁ x.1, f₂ x.2)) y → x = y

Tactic:
simp_rw [Prod.ext_iff]

Goal state after:
α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
h₁ : InjOn f₁ s₁
h₂ : InjOn f₂ s₂
x : α₁ × α₂
hx : x ∈ s₁ ×ˢ s₂
y : α₁ × α₂
hy : y ∈ s₁ ×ˢ s₂
⊢ f₁ x.1 = f₁ y.1 ∧ f₂ x.2 = f₂ y.2 → x.1 = y.1 ∧ x.2 = y.2
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
h₁ : InjOn f₁ s₁
h₂ : InjOn f₂ s₂
x : α₁ × α₂
hx : x ∈ s₁ ×ˢ s₂
y : α₁ × α₂
hy : y ∈ s₁ ×ˢ s₂
⊢ (fun x ↦ (f₁ x.1, f₂ x.2)) x = (fun x ↦ (f₁ x.1, f₂ x.2)) y → x = y

Tactic:
by

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

Goal state before:
pp: α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
t₁ : Set β₁
t₂ : Set β₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
h₁ : SurjOn f₁ s₁ t₁
h₂ : SurjOn f₂ s₂ t₂
⊢ SurjOn (fun x ↦ (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
t : Set β
h : ∀ (a : α), e a ∈ t ↔ a ∈ s
b : β
hb : b ∈ t
⊢ e (e.symm b) ∈ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : DecidableEq α
a b : α
ha : a ∈ s
hb : b ∈ s
x : α
⊢ (swap a b) x ∈ s ↔ x ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : α
⊢ IsAddRegular (ofMul a) ↔ IsRegular a

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : Additive α
⊢ IsRegular (toMul a) ↔ IsAddRegular a

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : AddMonoid α
a : α
⊢ IsRegular (ofAdd a) ↔ IsAddRegular a

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : AddMonoid α
a : Multiplicative α
⊢ IsAddRegular (toAdd a) ↔ IsRegular a

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : DecidableEq ι
M : ι → Type u_2
inst✝ : (i : ι) → AddMonoid (M i)
i : ι
a : M i
j : ι
⊢ mulSingle i (ofAdd a) j = ofAdd (single i a j)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : DecidableEq ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i : ι
a : M i
j : ι
⊢ single i (ofMul a) j = ofMul (mulSingle i a j)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Pow α β
p : Prop
inst✝ : Decidable p
a : α
b : p → β
c : ¬p → β
⊢ (a ^ if h : p then b h else c h) = if h : p then a ^ b h else a ^ c h

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Pow α β
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
c : β
⊢ (if h : p then a h else b h) ^ c = if h : p then a h ^ c else b h ^ c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Semigroup α
x y : α
⊢ ((fun x_1 ↦ x * x_1) ∘ fun x ↦ y * x) = fun x_1 ↦ x * y * x_1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Semigroup α
x y : α
⊢ ((fun x_1 ↦ x_1 * x) ∘ fun x ↦ x * y) = fun x_1 ↦ x_1 * (y * x)

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝¹ : MulOneClass M
P : Prop
inst✝ : Decidable P
a b : M
⊢ (if P then a * b else 1) = (if P then a else 1) * if P then b else 1

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝¹ : MulOneClass M
P : Prop
inst✝ : Decidable P
a b : M
⊢ (if P then 1 else a * b) = (if P then 1 else a) * if P then 1 else b

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : MulOneClass M
a b : M
h : a * b = 1
⊢ a = 1 ↔ b = 1

Tactic:
by

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

Goal state before:
pp: G : Type u_3
inst✝ : CommSemigroup G
a b c : G
⊢ a * (b * c) = b * (a * c)

Tactic:
by

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

Goal state before:
pp: G : Type u_3
inst✝ : CommSemigroup G
a b c : G
⊢ a * b * c = a * c * b

Tactic:
by

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

Goal state before:
pp: G : Type u_3
inst✝ : CommSemigroup G
a b c d : G
⊢ a * b * (c * d) = a * c * (b * d)

Tactic:
by

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

Goal state before:
pp: G : Type u_3
inst✝ : CommSemigroup G
a b c d : G
⊢ a * b * c * d = a * c * b * d

Tactic:
by

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

Goal state before:
pp: G : Type u_3
inst✝ : CommSemigroup G
a b c : G
⊢ a * b * c = b * c * a

Tactic:
by

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

Goal state before:
pp: G : Type u_3
inst✝ : CommSemigroup G
a b c : G
⊢ a * (b * c) = b * (c * a)

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝¹ : Monoid M
P : Prop
inst✝ : Decidable P
a : M
⊢ (a ^ if P then 1 else 0) = if P then a else 1

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
m n : ℕ
a : M
h : m ≤ n
⊢ a ^ m * a ^ (n - m) = a ^ n

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
m n : ℕ
a : M
h : m ≤ n
⊢ a ^ (n - m) * a ^ m = a ^ n

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
n : ℕ
hn : n ≠ 0
a : M
⊢ a * a ^ (n - 1) = a ^ n

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
n : ℕ
hn : n ≠ 0
a : M
⊢ a ^ (n - 1) * a = a ^ n

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a : M
n m : ℕ
ha : a ^ n = 1
⊢ a ^ m = a ^ (m % n + n * (m / n))

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a : M
n m : ℕ
ha : a ^ n = 1
⊢ a ^ (m % n + n * (m / n)) = a ^ (m % n)

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a : M
n m : ℕ
ha : a ^ n = 1
⊢ a ^ m = a ^ (m % n)

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a b : M
x✝ : a * b = 1
⊢ a ^ 0 * b ^ 0 = 1

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a b : M
n : ℕ
h : a * b = 1
⊢ a ^ n.succ * b ^ n.succ = a ^ n * a * (b * b ^ n)

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a b : M
n : ℕ
h : a * b = 1
⊢ a ^ n * a * (b * b ^ n) = a ^ n * (a * b) * b ^ n

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a b : M
n : ℕ
h : a * b = 1
⊢ a ^ n * (a * b) * b ^ n = 1

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a : M
⊢ (fun x ↦ a * x)^[0] = fun x ↦ a ^ 0 * x

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a : M
n : ℕ
⊢ (fun x ↦ a * x)^[n + 1] = fun x ↦ a ^ (n + 1) * x

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a : M
⊢ (fun x ↦ x * a)^[0] = fun x ↦ x * a ^ 0

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a : M
n : ℕ
⊢ (fun x ↦ x * a)^[n + 1] = fun x ↦ x * a ^ (n + 1)

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
n : ℕ
a b : M
⊢ (fun x ↦ a * x)^[n] b = a ^ n * b

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
n : ℕ
a b : M
⊢ (fun x ↦ x * a)^[n] b = b * a ^ n

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
n : ℕ
a : M
⊢ (fun x ↦ a * x)^[n] 1 = a ^ n

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
n : ℕ
a : M
⊢ (fun x ↦ x * a)^[n] 1 = a ^ n

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
k : ℕ
⊢ (fun x ↦ x ^ k)^[0] = fun x ↦ x ^ k ^ 0

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
k n : ℕ
⊢ (fun x ↦ x ^ k)^[n + 1] = fun x ↦ x ^ k ^ (n + 1)

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
a b : M
⊢ (a * b) ^ 0 = a ^ 0 * b ^ 0

Tactic:
rw [pow_zero, pow_zero, pow_zero, one_mul]

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
a b : M
⊢ (a * b) ^ 0 = a ^ 0 * b ^ 0

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
a b : M
n : ℕ
⊢ (a * b) ^ (n + 1) = a ^ (n + 1) * b ^ (n + 1)

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝¹ : Monoid M
inst✝ : IsLeftCancelMul M
a b : M
⊢ a * b = a ↔ a * b = a * 1

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝¹ : Monoid M
inst✝ : IsRightCancelMul M
a b : M
⊢ a * b = b ↔ a * b = 1 * b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CancelCommMonoid α
a b c d : α
h : a * b = c * d
⊢ a = c ↔ b = d

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CancelCommMonoid α
a b c d : α
h : a * b = c * d
⊢ a ≠ c ↔ b ≠ d

Tactic:
by

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

Goal state before:
pp: G : Type u_3
inst✝ : DivInvMonoid G
x y : G
⊢ x * (1 / y) = x / y

Tactic:
by

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

Goal state before:
pp: G : Type u_3
inst✝ : DivInvMonoid G
a b c : G
⊢ a * (b / c) = a * b / c

Tactic:
by

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

Goal state before:
pp: G : Type u_3
inst✝ : DivInvMonoid G
a b : G
⊢ a / b = a * (1 / b)

Tactic:
by

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

Goal state before:
pp: G : Type u_3
inst✝ : DivInvOneMonoid G
a : G
⊢ a / 1 = a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : b * a = 1
⊢ b = 1 / a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : a * b = 1
⊢ b = 1 / a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : a / b = 1
⊢ a * b⁻¹ = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : a⁻¹ * b = 1
⊢ a = b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : a * b⁻¹ = 1
⊢ a = b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
⊢ 1 / a * (1 / b) = 1 / (b * a)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
⊢ a⁻¹ / b = (b * a)⁻¹

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
⊢ (a / b)⁻¹ = b / a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
⊢ 1 / (a / b) = b / a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
⊢ 1 / (1 / a) = a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b c d : α
⊢ (a / b)⁻¹ = (c / d)⁻¹ ↔ b / a = d / c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Type u_3
M : Type u_4
inst✝ : DivisionMonoid α
a b c d : α
⊢ 1⁻¹ = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
⊢ a⁻¹ ^ 0 = (a ^ 0)⁻¹

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℕ
⊢ a⁻¹ ^ (n + 1) = (a ^ (n + 1))⁻¹

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
n : ℕ
⊢ 1 ^ ↑n = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
n : ℕ
⊢ 1 ^ Int.negSucc n = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
⊢ a ^ (-0) = (a ^ 0)⁻¹

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℕ
⊢ a ^ (-Int.negSucc n) = (a ^ Int.negSucc n)⁻¹

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
⊢ (a * b) ^ (-1) = b ^ (-1) * a ^ (-1)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℕ
⊢ a⁻¹ ^ ↑n = (a ^ ↑n)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Mul M₁
inst✝ : Semigroup M₂
f : M₁ → M₂
hf : Injective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x y z : M₁
⊢ f (x * y * z) = f (x * (y * z))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℕ
⊢ a⁻¹ ^ Int.negSucc n = (a ^ Int.negSucc n)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Mul M₁
inst✝ : CommMagma M₂
f : M₁ → M₂
hf : Injective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x y : M₁
⊢ f (x * y) = f (y * x)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℤ
⊢ a⁻¹ ^ n = a ^ (-n)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝² : Mul M₁
inst✝¹ : Mul M₂
inst✝ : IsLeftCancelMul M₂
f : M₁ → M₂
hf : Injective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x y z : M₁
H : (fun x_1 ↦ x * x_1) y = (fun x_1 ↦ x * x_1) z
⊢ ?m.31 x y z H * f y = ?m.31 x y z H * f z

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℕ
⊢ (1 / a) ^ n = 1 / a ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝² : Mul M₁
inst✝¹ : Mul M₂
inst✝ : IsRightCancelMul M₂
f : M₁ → M₂
hf : Injective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x y z : M₁
H : (fun x_1 ↦ x_1 * x) y = (fun x_1 ↦ x_1 * x) z
⊢ f y * ?m.31 x y z H = f z * ?m.31 x y z H

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℤ
⊢ (1 / a) ^ n = 1 / a ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝² : Mul M₁
inst✝¹ : One M₁
inst✝ : MulOneClass M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
⊢ f (1 * x) = f x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝² : Mul M₁
inst✝¹ : One M₁
inst✝ : MulOneClass M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
⊢ f (x * 1) = f x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : 1 / a = 1 / b
⊢ a = b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Opposite

Goal state before:
pp: α : Type u_1
inst✝ : AddZeroClass α
⊢ unop 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Opposite

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoid α
⊢ unop 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝³ : Mul M₁
inst✝² : One M₁
inst✝¹ : Pow M₁ ℕ
inst✝ : Monoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
x : M₁
⊢ f (x ^ 0) = f 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Opposite

Goal state before:
pp: α : Type u_1
inst✝ : SubNegMonoid α
⊢ unop 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Opposite

Goal state before:
pp: α : Type u_1
inst✝ : AddGroup α
⊢ unop 0 = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (↑m * ↑n) = (a ^ ↑m) ^ ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝³ : Mul M₁
inst✝² : One M₁
inst✝¹ : Pow M₁ ℕ
inst✝ : Monoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
⊢ f (x ^ (n + 1)) = f (x ^ n * x)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Opposite

Goal state before:
pp: α : Type u_1
inst✝ : DivInvMonoid α
x✝¹ : ℕ
x✝ : αᵐᵒᵖ
⊢ unop (x✝ ^ ↑x✝¹.succ) = unop (x✝ ^ ↑x✝¹ * x✝)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Opposite

Goal state before:
pp: α : Type u_1
inst✝ : DivInvMonoid α
x y : α
⊢ op (x / y) = (op y)⁻¹ * op x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Opposite

Goal state before:
pp: α : Type u_1
inst✝ : Mul α
a x y : α
⊢ SemiconjBy (op a) (op y) (op x) ↔ SemiconjBy a x y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁✝ : Type u_1
M₂ : Type u_2
inst✝⁴ : Mul M₁✝
inst✝³ : One M₁✝
inst✝² : Pow M₁✝ ℕ
M₁ : Type u_3
inst✝¹ : Inv M₁
inst✝ : InvolutiveInv M₂
f : M₁ → M₂
hf : Injective f
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
x : M₁
⊢ f x⁻¹⁻¹ = f x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Opposite

Goal state before:
pp: α : Type u_1
inst✝ : Mul α
a x y : αᵐᵒᵖ
⊢ SemiconjBy (unop a) (unop y) (unop x) ↔ SemiconjBy a x y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝⁴ : Mul M₁
inst✝³ : One M₁
inst✝² : Pow M₁ ℕ
inst✝¹ : Inv M₁
inst✝ : InvOneClass M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
⊢ f 1⁻¹ = f 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Opposite

Goal state before:
pp: α : Type u_1
inst✝ : MulOne α
⊢ IsDedekindFiniteMonoid αᵐᵒᵖ ↔ IsDedekindFiniteMonoid α

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Opposite

Goal state before:
pp: α : Type u_1
inst✝ : MulOneClass α
⊢ unop 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Opposite

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
⊢ unop 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Opposite

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
⊢ unop 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Opposite

Goal state before:
pp: α : Type u_1
inst✝ : DivInvMonoid α
⊢ unop 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Opposite

Goal state before:
pp: α : Type u_1
inst✝ : Group α
⊢ unop 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Opposite

Goal state before:
pp: α : Type u_1
inst✝ : CommGroup α
⊢ unop 1 = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (↑m * Int.negSucc n) = (a ^ ↑m) ^ Int.negSucc n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₁
inst✝⁵ : One M₁
inst✝⁴ : Pow M₁ ℕ
inst✝³ : Inv M₁
inst✝² : Div M₁
inst✝¹ : Pow M₁ ℤ
inst✝ : DivInvMonoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x y : M₁
⊢ f (x / y) = f (x * y⁻¹)

Tactic:
by

Goal state after: