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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionCommMonoid α
a b c : α
⊢ a * b / c = a / c * b

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionCommMonoid α
a b c : α
⊢ a / b * c = a * c / b

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionCommMonoid α
a b c : α
⊢ a / b * c = c / b * a

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a / b / (c / d) = a * d / (b * c)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a / b / (c / d) = a / c / (b / d)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a / b * (c / d) = a * c / (b * d)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a * b / (c * d) = a / c * (b / d)

Tactic:
simp

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

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

Tactic:
div_mul_eq_div_div_swap

Goal state after:
G : Type u_3
inst✝ : Group G
a b c : G
⊢ a * c / c / b = a / b
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b : G
⊢ a / b = a ↔ b = 1

Tactic:
rw [div_eq_mul_inv, mul_eq_left, inv_eq_one]

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

Goal state before:
pp: case ofNat
G : Type u_3
inst✝ : Group G
a : G
a✝ : ℕ
⊢ a ^ (Int.ofNat a✝).natAbs = 1 ↔ a ^ Int.ofNat a✝ = 1

Tactic:
simp

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

Goal state before:
pp: case negSucc
G : Type u_3
inst✝ : Group G
a : G
a✝ : ℕ
⊢ a ^ (Int.negSucc a✝).natAbs = 1 ↔ a ^ Int.negSucc a✝ = 1

Tactic:
simp

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

Goal state before:
pp: case zero
G : Type u_3
inst✝ : Group G
a : G
m : ℤ
⊢ a ^ (m + 0) = a ^ m * a ^ 0

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b : G
⊢ a / b / a = b⁻¹

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a✝ b u : αˣ
n : ℕ
a : αˣ
⊢ (↑a * ↑a⁻¹) ^ n = 1

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a✝ b u : αˣ
n : ℕ
a : αˣ
⊢ (↑a⁻¹ * ↑a) ^ n = 1

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a✝ b u a : αˣ
⊢ ↑{ val := NPow.npow 0 ↑a, inv := NPow.npow 0 ↑a⁻¹, val_inv := ⋯, inv_val := ⋯ } = ↑1

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a✝ b u a : αˣ
⊢ NPow.npow 0 a = 1

Tactic:
simp

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
α : Type u_5
s : AddCommGroup α
n : ℕ
a : α
⊢ ↑n • a = n • a

Tactic:
simp

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

Goal state before:
pp: M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
x✝¹ x✝ : Mˣ
⊢ ↑{ val := f ↑(x✝¹ * x✝), inv := f (x✝¹ * x✝).inv, val_inv := ⋯, inv_val := ⋯ } =
    ↑({ val := f ↑x✝¹, inv := f x✝¹.inv, val_inv := ⋯, inv_val := ⋯ } *
        { val := f ↑x✝, inv := f x✝.inv, val_inv := ⋯, inv_val := ⋯ })

Tactic:
simp

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

Goal state before:
pp: M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = f x
x y : M
⊢ ↑(g (x * y)) = ↑(g x * g y)

Tactic:
simp only [h, val_mul, f.map_mul]

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

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝¹ : Group G
inst✝ : CommMonoid M
⊢ ∀ (x y : G →* M), (x * y).toHomUnits = x.toHomUnits * y.toHomUnits

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
x : α
u : αˣ
y : α
⊢ x /ₚ u * ↑u = y * ↑u ↔ y * ↑u = x

Tactic:
divp_mul_cancel

Goal state after:
α : Type u
inst✝ : Monoid α
x : α
u : αˣ
y : α
⊢ x = y * ↑u ↔ y * ↑u = x
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝¹ : LeftCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ ¬(a ≠ 1 ∨ b ≠ 1) ↔ a * b = 1

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝¹ : RightCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ ¬(a ≠ 1 ∨ b ≠ 1) ↔ a * b = 1

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝ : CommMonoid α
x y : α
ux uy : αˣ
⊢ x /ₚ ux = y /ₚ uy ↔ x * ↑uy = y * ↑ux

Tactic:
divp_eq_iff_mul_eq,

Goal state after:
α : Type u
inst✝ : CommMonoid α
x y : α
ux uy : αˣ
⊢ y /ₚ uy * ↑ux = x ↔ x * ↑uy = y * ↑ux
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝¹ : CommMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ ¬(a ≠ 1 ∨ b ≠ 1) ↔ a * b = 1

Tactic:
simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst✝⁴ : EquivLike F α β
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : Mul P
inst✝ : Unique α
⊢ ∀ (x y : α → M), (Equiv.funUnique α M).toFun (x * y) = (Equiv.funUnique α M).toFun x * (Equiv.funUnique α M).toFun y

Tactic:
simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
M✝ : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N✝ : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P✝ : Type u_12
Q✝ : Type u_13
G : Type u_14
H : Type u_15
inst✝² : EquivLike F α β
M : Type u_16
N : Type u_17
P : Type u_18
Q : Type u_19
inst✝¹ : Mul P
inst✝ : Mul Q
f : M ≃ N
g : P ≃* Q
h : M → P
x✝ : M
⊢ (fun k m ↦ g.symm (k (f m))) ((fun h n ↦ g (h (f.symm n))) h) x✝ = h x✝

Tactic:
simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
M✝ : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N✝ : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P✝ : Type u_12
Q✝ : Type u_13
G : Type u_14
H : Type u_15
inst✝² : EquivLike F α β
M : Type u_16
N : Type u_17
P : Type u_18
Q : Type u_19
inst✝¹ : Mul P
inst✝ : Mul Q
f : M ≃ N
g : P ≃* Q
k : N → Q
x✝ : N
⊢ (fun h n ↦ g (h (f.symm n))) ((fun k m ↦ g.symm (k (f m))) k) x✝ = k x✝

Tactic:
simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
M✝ : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N✝ : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P✝ : Type u_12
Q✝ : Type u_13
G : Type u_14
H : Type u_15
inst✝² : EquivLike F α β
M : Type u_16
N : Type u_17
P : Type u_18
Q : Type u_19
inst✝¹ : Mul P
inst✝ : Mul Q
f : M ≃ N
g : P ≃* Q
h k : M → P
x✝ : N
⊢ g ((h * k) (f.symm x✝)) = ((fun n ↦ g (h (f.symm n))) * fun n ↦ g (k (f.symm n))) x✝

Tactic:
simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst✝⁸ : EquivLike F α β
inst✝⁷ : MulOneClass M
inst✝⁶ : MulOneClass M₁
inst✝⁵ : MulOneClass M₂
inst✝⁴ : MulOneClass M₃
inst✝³ : Monoid N
inst✝² : Monoid N₁
inst✝¹ : Monoid N₂
inst✝ : Monoid N₃
e : M₁ ≃* M₂
f : M₁ →* N
x✝ : M₁
⊢ ((fun f ↦ f.comp e.toMonoidHom) ((fun f ↦ f.comp e.symm.toMonoidHom) f)) x✝ = f x✝

Tactic:
simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst✝⁸ : EquivLike F α β
inst✝⁷ : MulOneClass M
inst✝⁶ : MulOneClass M₁
inst✝⁵ : MulOneClass M₂
inst✝⁴ : MulOneClass M₃
inst✝³ : Monoid N
inst✝² : Monoid N₁
inst✝¹ : Monoid N₂
inst✝ : Monoid N₃
e : M₁ ≃* M₂
f : M₂ →* N
x✝ : M₂
⊢ ((fun f ↦ f.comp e.symm.toMonoidHom) ((fun f ↦ f.comp e.toMonoidHom) f)) x✝ = f x✝

Tactic:
simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst✝⁸ : EquivLike F α β
inst✝⁷ : MulOneClass M
inst✝⁶ : MulOneClass M₁
inst✝⁵ : MulOneClass M₂
inst✝⁴ : MulOneClass M₃
inst✝³ : Monoid N
inst✝² : Monoid N₁
inst✝¹ : Monoid N₂
inst✝ : Monoid N₃
e : N₁ ≃* N₂
f : M →* N₁
x✝ : M
⊢ (e.symm.toMonoidHom.comp (e.toMonoidHom.comp f)) x✝ = f x✝

Tactic:
simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst✝⁸ : EquivLike F α β
inst✝⁷ : MulOneClass M
inst✝⁶ : MulOneClass M₁
inst✝⁵ : MulOneClass M₂
inst✝⁴ : MulOneClass M₃
inst✝³ : Monoid N
inst✝² : Monoid N₁
inst✝¹ : Monoid N₂
inst✝ : Monoid N₃
e : N₁ ≃* N₂
f : M →* N₂
x✝ : M
⊢ (e.toMonoidHom.comp (e.symm.toMonoidHom.comp f)) x✝ = f x✝

Tactic:
simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst✝⁸ : EquivLike F α β
inst✝⁷ : MulOneClass M
inst✝⁶ : MulOneClass M₁
inst✝⁵ : MulOneClass M₂
inst✝⁴ : MulOneClass M₃
inst✝³ : CommMonoid N
inst✝² : CommMonoid N₁
inst✝¹ : CommMonoid N₂
inst✝ : CommMonoid N₃
e : M₁ ≃* M₂
f g : M₁ →* N
x✝ : M₂
⊢ (e.monoidHomCongrLeftEquiv.toFun (f * g)) x✝ =
    (e.monoidHomCongrLeftEquiv.toFun f * e.monoidHomCongrLeftEquiv.toFun g) x✝

Tactic:
simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_8
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
P : Type u_12
Q : Type u_13
G : Type u_14
H : Type u_15
inst✝⁸ : EquivLike F α β
inst✝⁷ : MulOneClass M
inst✝⁶ : MulOneClass M₁
inst✝⁵ : MulOneClass M₂
inst✝⁴ : MulOneClass M₃
inst✝³ : CommMonoid N
inst✝² : CommMonoid N₁
inst✝¹ : CommMonoid N₂
inst✝ : CommMonoid N₃
e : N₁ ≃* N₂
f g : M →* N₁
x✝ : M
⊢ (e.monoidHomCongrRightEquiv.toFun (f * g)) x✝ =
    (e.monoidHomCongrRightEquiv.toFun f * e.monoidHomCongrRightEquiv.toFun g) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Units.Equiv

Goal state before:
pp: F : Type u_1
M : Type u_3
N : Type u_4
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : EquivLike F M N
inst✝ : MulEquivClass F M N
f : F
x : M
hx : IsUnit (f x)
⊢ f (EquivLike.inv f 1) = f 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Units.Equiv

Goal state before:
pp: F : Type u_1
M : Type u_3
N : Type u_4
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : EquivLike F M N
inst✝ : MulEquivClass F M N
f : F
x✝ : M
hx : IsUnit (f x✝)
x y : N
⊢ f ({ toFun := EquivLike.inv f, map_one' := ⋯ }.toFun (x * y)) =
    f ({ toFun := EquivLike.inv f, map_one' := ⋯ }.toFun x * { toFun := EquivLike.inv f, map_one' := ⋯ }.toFun y)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Units.Equiv

Goal state before:
pp: F : Type u_1
M : Type u_3
N : Type u_4
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : EquivLike F M N
inst✝ : MulEquivClass F M N
f : F
⊢ ∀ (a : M), IsUnit (f a) → IsUnit a

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ ∀ (a : M × N), 1 * a = a

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ ∀ (a : M × N), a * 1 = a

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : DivisionMonoid G
inst✝ : DivisionMonoid H
⊢ ∀ (x : G × H), x⁻¹⁻¹ = x

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : LeftCancelMonoid M
inst✝ : LeftCancelMonoid N
x✝¹ x✝ : M × N
⊢ ∀ ⦃a₂ : M × N⦄, (fun x ↦ x✝¹ * x) x✝ = (fun x ↦ x✝¹ * x) a₂ → x✝ = a₂

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : RightCancelMonoid M
inst✝ : RightCancelMonoid N
x✝¹ x✝ : M × N
⊢ ∀ ⦃a₂ : M × N⦄, (fun x ↦ x * x✝¹) x✝ = (fun x ↦ x * x✝¹) a₂ → x✝ = a₂

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : CancelCommMonoid M
inst✝ : CancelCommMonoid N
x✝¹ x✝ : M × N
⊢ ∀ ⦃a₂ : M × N⦄, (fun x ↦ x✝¹ * x) x✝ = (fun x ↦ x✝¹ * x) a₂ → x✝ = a₂

Tactic:
simp

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

Goal state before:
pp: M : Type u_3
N : Type u_4
P : Type u_5
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : CommSemigroup P
Q : Type u_6
inst✝ : CommSemigroup Q
h : P →ₙ* Q
f : M →ₙ* P
g : N →ₙ* P
x : M × N
⊢ (h.comp (f.coprod g)) x = ((h.comp f).coprod (h.comp g)) x

Tactic:
simp

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

Goal state before:
pp: M : Type u_3
N : Type u_4
P : Type u_5
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
f : M →* N × P
x✝ : M
⊢ (((fst N P).comp f).prod ((snd N P).comp f)) x✝ = f x✝

Tactic:
simp

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

Goal state before:
pp: M : Type u_3
N : Type u_4
P : Type u_5
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : CommMonoid P
Q : Type u_6
inst✝ : CommMonoid Q
h : P →* Q
f : M →* P
g : N →* P
x : M × N
⊢ (h.comp (f.coprod g)) x = ((h.comp f).coprod (h.comp g)) x

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : Monoid M
inst✝ : Monoid N
u : Mˣ × Nˣ
⊢ (↑u.1, ↑u.2) * (↑u.1⁻¹, ↑u.2⁻¹) = 1

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : Monoid M
inst✝ : Monoid N
u : Mˣ × Nˣ
⊢ (↑u.1⁻¹, ↑u.2⁻¹) * (↑u.1, ↑u.2) = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Defs

Goal state before:
pp: M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
a : M₀
⊢ a * a = 0 ↔ a = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Defs

Goal state before:
pp: M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
a : M₀
⊢ 0 = a * a ↔ a = 0

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
p : α → Prop
f✝ f : Perm α
h : ∀ (x : α), p (f x) ↔ p x
x✝ : { x // p x }
⊢ (fun x ↦ ⟨f⁻¹ ↑x, ⋯⟩) ((fun x ↦ ⟨f ↑x, ⋯⟩) x✝) = x✝

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
p : α → Prop
f✝ f : Perm α
h : ∀ (x : α), p (f x) ↔ p x
x✝ : { x // p x }
⊢ (fun x ↦ ⟨f ↑x, ⋯⟩) ((fun x ↦ ⟨f⁻¹ ↑x, ⋯⟩) x✝) = x✝

Tactic:
simp

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

Goal state before:
pp: case zero
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p (f x) ↔ p x
⊢ f.subtypePerm hf ^ 0 = (f ^ 0).subtypePerm ⋯

Tactic:
simp

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
a b : M₀
h : a ≠ 0 → b = 0
this : Decidable (a = 0)
ha : ¬a = 0
⊢ a * b = 0

Tactic:
rw [h ha, mul_zero]

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
m n : ℕ
hmn : m ≤ n
h : a ^ m * b = 0
⊢ a ^ (n - m) * 0 = 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_4
inst✝ : Group α
a : α
n : ℕ
⊢ Equiv.mulLeft a ^ Int.ofNat n = Equiv.mulLeft (a ^ Int.ofNat n)

Tactic:
simp

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

Goal state before:
pp: α : Type u_4
inst✝ : Group α
a : α
n : ℕ
⊢ Equiv.mulLeft a ^ Int.negSucc n = Equiv.mulLeft (a ^ Int.negSucc n)

Tactic:
simp

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

Goal state before:
pp: α : Type u_4
inst✝ : Group α
a : α
n : ℕ
⊢ Equiv.mulRight a ^ Int.ofNat n = Equiv.mulRight (a ^ Int.ofNat n)

Tactic:
simp

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

Goal state before:
pp: α : Type u_4
inst✝ : Group α
a : α
n : ℕ
⊢ Equiv.mulRight a ^ Int.negSucc n = Equiv.mulRight (a ^ Int.negSucc n)

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝¹ : Mul M
inst✝ : Group G
x✝ : G
⊢ { toFun := fun h ↦ 1 * h * 1⁻¹, invFun := fun h ↦ 1⁻¹ * h * 1, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ } x✝ =
    1 x✝

Tactic:
simp

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

Goal state before:
pp: G : Type u_3
inst✝ : AddGroup G
g h : G
⊢ (-addConj g) h = -g + h + g

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
inst✝⁴ : MulZeroOneClass α
inst✝³ : MulZeroOneClass β
F : Type u_7
inst✝² : FunLike F α β
inst✝¹ : MonoidWithZeroHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
h : p
⊢ f 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: case neg
α : Type u_2
β : Type u_3
inst✝⁴ : MulZeroOneClass α
inst✝³ : MulZeroOneClass β
F : Type u_7
inst✝² : FunLike F α β
inst✝¹ : MonoidWithZeroHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
h : ¬p
⊢ f 1 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
inst✝⁴ : MulZeroOneClass α
inst✝³ : MulZeroOneClass β
F : Type u_7
inst✝² : FunLike F α β
inst✝¹ : MonoidWithZeroHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
h : p
⊢ f 1 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: case neg
α : Type u_2
β : Type u_3
inst✝⁴ : MulZeroOneClass α
inst✝³ : MulZeroOneClass β
F : Type u_7
inst✝² : FunLike F α β
inst✝¹ : MonoidWithZeroHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
h : ¬p
⊢ f 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: case zero
R : Type u_1
inst✝ : AddMonoidWithOne R
m : ℕ
⊢ ↑(m + 0) = ↑m + ↑0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀ : Type u_6
inst✝⁴ : MulZeroOneClass α
inst✝³ : MulZeroOneClass β
inst✝² : MulZeroOneClass γ
inst✝¹ : MulZeroOneClass δ
inst✝ : FunLike F α β
hnp : β →*₀ γ
hmn : α →*₀ β
⊢ (⇑hnp ∘ ⇑hmn) 1 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀ : Type u_6
inst✝⁴ : MulZeroOneClass α
inst✝³ : MulZeroOneClass β
inst✝² : MulZeroOneClass γ
inst✝¹ : MulZeroOneClass δ
inst✝ : FunLike F α β
hnp : β →*₀ γ
hmn : α →*₀ β
⊢ ∀ (x y : α), (⇑hnp ∘ ⇑hmn) (x * y) = (⇑hnp ∘ ⇑hmn) x * (⇑hnp ∘ ⇑hmn) y

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀✝ : Type u_6
inst✝⁹ : MulZeroOneClass α
inst✝⁸ : MulZeroOneClass β
inst✝⁷ : MulZeroOneClass γ
inst✝⁶ : MulZeroOneClass δ
inst✝⁵ : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst✝⁴ : MulZeroOneClass M₀
inst✝³ : MulZeroOneClass N₀
inst✝² : DecidablePred fun x ↦ x = 0
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
⊢ (if 0 = 0 then 0 else 1) = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀✝ : Type u_6
inst✝⁹ : MulZeroOneClass α
inst✝⁸ : MulZeroOneClass β
inst✝⁷ : MulZeroOneClass γ
inst✝⁶ : MulZeroOneClass δ
inst✝⁵ : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst✝⁴ : MulZeroOneClass M₀
inst✝³ : MulZeroOneClass N₀
inst✝² : DecidablePred fun x ↦ x = 0
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
⊢ (if 1 = 0 then 0 else 1) = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: case ind.succ
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
⊢ (k + 1).binCast = ↑(k + 1)

Tactic:
rw [Nat.binCast]
      by_cases h : (k + 1) % 2 = 0
      · conv => rhs; rw [← Nat.mod_add_div (k + 1) 2]
        rw [if_pos h, hk _ <| Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ← Nat.cast_add]
        rw [h, Nat.zero_add, Nat.succ_mul, Nat.one_mul]
      · conv => rhs; rw [← Nat.mod_add_div (k + 1) 2]
        rw [if_neg h, hk _ <| Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ← Nat.cast_add]
        have h1 := Or.resolve_left (Nat.mod_two_eq_zero_or_one (succ k)) h
        rw [h1, Nat.add_comm 1, Nat.succ_mul, Nat.one_mul]
        simp only [Nat.cast_add, Nat.cast_one]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: case pos
M : Type u_1
A : Type u_7
inst✝² : Zero A
inst✝¹ : SMulZeroClass M A
p : Prop
inst✝ : Decidable p
a : M
b : A
h✝ : p
⊢ a • b = a • b

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: case neg
M : Type u_1
A : Type u_7
inst✝² : Zero A
inst✝¹ : SMulZeroClass M A
p : Prop
inst✝ : Decidable p
a : M
b : A
h✝ : ¬p
⊢ a • 0 = 0

Tactic:
simp

Goal state after: