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

Goal state before:
pp: α : Type u
inst✝¹ : LeftCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : a * b = 1
⊢ b * a = 1

Tactic:
by

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

Goal state before:
pp: G : Type u_1
R : Type u_2
S : Type u_3
F : Type u_5
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
inst✝³ : FunLike F R S
inst✝² : MonoidHomClass F R S
inst✝¹ : FunLike G S R
inst✝ : MonoidHomClass G S R
f : F
g : G
hfg : LeftInverse ⇑g ⇑f
a : R
ha : IsUnit (f a)
⊢ IsUnit a

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : LeftCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : a * b = 1
⊢ b = 1

Tactic:
by

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

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : RightCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : a * b = 1
⊢ b * a = 1

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : RightCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : a * b = 1
⊢ b = 1

Tactic:
by

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

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

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

Tactic:
by

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

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

Tactic:
by

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

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 * y /ₚ (ux * uy)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : CommMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : a * b = 1
⊢ b * a = 1

Tactic:
by

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

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

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

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : Subsingleton M
a : M
⊢ a * a = 1

Tactic:
by

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

Goal state before:
pp: α : Type u
M : Type u_1
inst✝¹ : Monoid M
inst✝ : Subsingleton M
x✝ : Mˣ
⊢ ↑x✝ = 1

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a b : M
h : IsUnit b
⊢ a * b = b ↔ a * b = 1 * b

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a b : M
h : IsUnit b
⊢ a * b = 1 * b ↔ a = 1

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a b : M
h : IsUnit a
⊢ a * b = a ↔ a * b = a * 1

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a b : M
h : IsUnit a
⊢ a * b = a * 1 ↔ b = 1

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
y : M
⊢ (fun x ↦ a * x) (↑h.unit⁻¹ * y) = y

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
h : Bijective fun x ↦ a * x
⊢ (fun x ↦ a * x) (⋯.choose * a) = (fun x ↦ a * x) 1

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
y : M
⊢ (fun x ↦ x * a) (y * ↑h.unit⁻¹) = y

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
h : Bijective fun x ↦ x * a
⊢ (fun x ↦ x * a) (a * ⋯.choose) = (fun x ↦ x * a) 1

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a : α
h : IsUnit a
⊢ a * (1 / a) = 1

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit c
⊢ a / c = b / c ↔ a = b

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit b
⊢ a / b = c ↔ a = c * b

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit c
⊢ a = b / c ↔ a * c = b

Tactic:
by

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

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

Tactic:
h.div_mul_cancel_right,

Goal state after:
α : Type u
inst✝ : DivisionMonoid α
a b : α
h : IsUnit b
⊢ a⁻¹ = 1 / a
Module: Mathlib.Algebra.Group.Units.Basic

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
a : α
h : IsUnit a
b : α
⊢ a / (a * b) = 1 / b

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
a : α
h : IsUnit a
b : α
⊢ a * b / a = b

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
a : α
h : IsUnit a
b : α
⊢ a * (b / a) = b

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
b d : α
hb : IsUnit b
hd : IsUnit d
a c : α
h : a / b = c / d
⊢ a * d = c * b

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
⊢ a / b = c / d ↔ a * d = c * b

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
⊢ a * b⁻¹ = c * d⁻¹ ↔ a * d = c * b

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
⊢ b⁻¹ * a = d⁻¹ * c ↔ a * d = c * b

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
a b : α
h : IsUnit a
⊢ a / (a / b) = b

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
a b : α
h : IsUnit a
⊢ a / b / a = b⁻¹

Tactic:
by

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

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
⊢ (fun k m ↦ g.symm (k (f m))) ((fun h n ↦ g (h (f.symm n))) h) = h

Tactic:
by

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
⊢ (fun h n ↦ g (h (f.symm n))) ((fun k m ↦ g.symm (k (f m))) k) = k

Tactic:
by

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
⊢ (fun n ↦ g ((h * k) (f.symm n))) = (fun n ↦ g (h (f.symm n))) * fun n ↦ g (k (f.symm n))

Tactic:
by

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
⊢ (fun f ↦ f.comp e.toMonoidHom) ((fun f ↦ f.comp e.symm.toMonoidHom) f) = f

Tactic:
by

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
⊢ (fun f ↦ f.comp e.symm.toMonoidHom) ((fun f ↦ f.comp e.toMonoidHom) f) = f

Tactic:
by

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₁
⊢ e.symm.toMonoidHom.comp (e.toMonoidHom.comp f) = f

Tactic:
by

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₂
⊢ e.toMonoidHom.comp (e.symm.toMonoidHom.comp f) = f

Tactic:
by

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
⊢ e.monoidHomCongrLeftEquiv.toFun (f * g) = e.monoidHomCongrLeftEquiv.toFun f * e.monoidHomCongrLeftEquiv.toFun g

Tactic:
by

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₁
⊢ e.monoidHomCongrRightEquiv.toFun (f * g) = e.monoidHomCongrRightEquiv.toFun f * e.monoidHomCongrRightEquiv.toFun g

Tactic:
by

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

Goal state before:
pp: G : Type u_6
inst✝ : Group G
x : Gˣ
⊢ toUnits ↑x = x

Tactic:
by

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

Goal state before:
pp: F : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
inst✝ : Group G
a b : G
⊢ (fun b ↦ b⁻¹ * a) ((fun b ↦ a / b) b) = b

Tactic:
by

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

Goal state before:
pp: F : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
inst✝ : Group G
a b : G
⊢ (fun b ↦ a / b) ((fun b ↦ b⁻¹ * a) b) = b

Tactic:
by

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

Goal state before:
pp: F : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
inst✝ : Group G
a b : G
⊢ (fun b ↦ b * a) ((fun b ↦ b / a) b) = b

Tactic:
by

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

Goal state before:
pp: F : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
inst✝ : Group G
a b : G
⊢ (fun b ↦ b / a) ((fun b ↦ b * a) b) = b

Tactic:
by

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

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

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)
⊢ IsUnit x

Tactic:
by

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

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

Goal state before:
pp: M : Type u_3
N : Type u_4
inst✝¹ : MulOneClass M
inst✝ : Mul N
b₁ b₂ : N
⊢ (1, b₁) * (1, b₂) = (1, b₁ * b₂)

Tactic:
by

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

Goal state before:
pp: M : Type u_3
N : Type u_4
inst✝¹ : Mul M
inst✝ : MulOneClass N
a₁ a₂ : M
⊢ (a₁, 1) * (a₂, 1) = (a₁ * a₂, 1)

Tactic:
by

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✝³ : Mul M
inst✝² : Mul N
inst✝¹ : IsMulCommutative M
inst✝ : IsMulCommutative N
x✝¹ x✝ : M × N
⊢ x✝¹ * x✝ = x✝ * x✝¹

Tactic:
by

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✝¹ : CommMagma M
inst✝ : CommMagma N
x✝¹ x✝ : M × N
⊢ x✝¹ * x✝ = x✝ * x✝¹

Tactic:
by

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✝¹ : Semigroup M
inst✝ : Semigroup N
x✝² x✝¹ x✝ : M × N
⊢ x✝² * x✝¹ * x✝ = x✝² * (x✝¹ * x✝)

Tactic:
by

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✝¹ : MulOneClass M
inst✝ : MulOneClass N
x✝ : M × N
⊢ 1 * x✝ = x✝

Tactic:
by

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✝¹ : MulOneClass M
inst✝ : MulOneClass N
x✝ : M × N
⊢ x✝ * 1 = x✝

Tactic:
by

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

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

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
inst✝¹ : IsMulTorsionFree M
inst✝ : IsMulTorsionFree N
n : ℕ
hn : n ≠ 0
a b : M × N
hab : (fun a ↦ a ^ n) a = (fun a ↦ a ^ n) b
⊢ a = b

Tactic:
by

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✝¹ : DivInvMonoid G
inst✝ : DivInvMonoid H
x✝¹ x✝ : G × H
⊢ x✝¹ / x✝ = x✝¹ * x✝⁻¹

Tactic:
by

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✝¹ : DivInvMonoid G
inst✝ : DivInvMonoid H
x✝ : G × H
⊢ x✝ ^ 0 = 1

Tactic:
by

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✝¹ : DivInvMonoid G
inst✝ : DivInvMonoid H
x✝¹ : ℕ
x✝ : G × H
⊢ x✝ ^ ↑x✝¹.succ = x✝ ^ ↑x✝¹ * x✝

Tactic:
by

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✝¹ : DivInvMonoid G
inst✝ : DivInvMonoid H
x✝¹ : ℕ
x✝ : G × H
⊢ x✝ ^ Int.negSucc x✝¹ = (x✝ ^ ↑x✝¹.succ)⁻¹

Tactic:
by

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

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✝¹ : DivisionCommMonoid G
inst✝ : DivisionCommMonoid H
x✝¹ x✝ : G × H
g₁ : G
h₁ : H
fst✝ : G
snd✝ : H
⊢ (g₁, h₁) * (fst✝, snd✝) = (fst✝, snd✝) * (g₁, h₁)

Tactic:
by

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✝¹ : Group G
inst✝ : Group H
x✝ : G × H
⊢ x✝⁻¹ * x✝ = 1

Tactic:
by

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

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

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✝¹ : CancelMonoid M
inst✝ : CancelMonoid N
x✝¹ x✝ : M × N
⊢ ∀ ⦃a₂ : M × N⦄, (fun x ↦ x * x✝¹) x✝ = (fun x ↦ x * x✝¹) a₂ → x✝ = a₂

Tactic:
by

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✝¹ : CommMonoid M
inst✝ : CommMonoid N
x✝¹ x✝ : M × N
m₁ : M
n₁ : N
fst✝ : M
snd✝ : N
⊢ (m₁, n₁) * (fst✝, snd✝) = (fst✝, snd✝) * (m₁, n₁)

Tactic:
by

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

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✝¹ : CommGroup G
inst✝ : CommGroup H
x✝¹ x✝ : G × H
g₁ : G
h₁ : H
fst✝ : G
snd✝ : H
⊢ (g₁, h₁) * (fst✝, snd✝) = (fst✝, snd✝) * (g₁, h₁)

Tactic:
by

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✝ : Mul P
f : M →ₙ* N × P
x : M
⊢ (((fst N P).comp f).prod ((snd N P).comp f)) x = f x

Tactic:
by

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

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

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
f : M →* P
g : N →* P
x : M
⊢ ((f.coprod g).comp (inl M N)) x = f x

Tactic:
by

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
f : M →* P
g : N →* P
x : N
⊢ ((f.coprod g).comp (inr M N)) x = g x

Tactic:
by

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
f : M × N →* P
x : M × N
⊢ ((f.comp (inl M N)).coprod (f.comp (inr M N))) x = f x

Tactic:
by

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

Goal state after: