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

Goal state before:
pp: M : Type u_3
inst✝ : Monoid M
u : Mˣ
a : M
x✝ : IsUnit (↑u * a)
v : Mˣ
hv : ↑v = ↑u * a
⊢ ↑u⁻¹ * ↑v = ↑u⁻¹ * ↑v

Tactic:
]

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

Goal state before:
pp: M : Type u_3
inst✝ : Monoid M
u : Mˣ
a : M
x✝ : IsUnit (↑u * a)
v : Mˣ
hv : ↑v = ↑u * a
this : IsUnit a
⊢ IsUnit a

Tactic:
]

Goal state after:
M : Type u_3
inst✝ : Monoid M
u : Mˣ
a : M
x✝ : IsUnit (↑u * a)
v : Mˣ
hv : ↑v = ↑u * a
this : IsUnit a
⊢ IsUnit a
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : IsDedekindFiniteMonoid M
x y : M
hu : IsUnit (x * y)
z : M
hz : x * y * z = 1
⊢ x * y * z = 1

Tactic:
]

Goal state after:
M : Type u_1
inst✝¹ : Monoid M
inst✝ : IsDedekindFiniteMonoid M
x y : M
hu : IsUnit (x * y)
z : M
hz : x * y * z = 1
⊢ x * y * z = 1
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : IsDedekindFiniteMonoid M
x y : M
hu : IsUnit (x * y)
z : M
hz : z * (x * y) = 1
⊢ z * (x * y) = 1

Tactic:
]

Goal state after:
M : Type u_1
inst✝¹ : Monoid M
inst✝ : IsDedekindFiniteMonoid M
x y : M
hu : IsUnit (x * y)
z : M
hz : z * (x * y) = 1
⊢ z * (x * y) = 1
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
⊢ a * ↑h.unit⁻¹ = ↑h.unit * ↑h.unit⁻¹

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
⊢ a * ↑h.unit⁻¹ = ↑h.unit * ↑h.unit⁻¹
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
u : αˣ
⊢ 1 = 1

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a : α
u : αˣ
hu : ↑u = a
⊢ IsUnit ↑u⁻¹

Tactic:
]

Goal state after:
α : Type u
inst✝ : DivisionMonoid α
a : α
u : αˣ
hu : ↑u = a
⊢ IsUnit ↑u⁻¹
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: M : Type u_4
F : Type u_5
inst✝ : Monoid F
c : F → M → M
h1 : c 1 = id
hmul : ∀ (f g : F), c (f * g) = c f ∘ c g
f : F
⊢ id = (c f)^[0]

Tactic:
]

Goal state after:
M : Type u_4
F : Type u_5
inst✝ : Monoid F
c : F → M → M
h1 : c 1 = id
hmul : ∀ (f g : F), c (f * g) = c f ∘ c g
f : F
⊢ id = (c f)^[0]
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a b : α
ha : IsUnit a
hb : IsUnit b
⊢ IsUnit (a * b⁻¹)

Tactic:
]

Goal state after:
α : Type u
inst✝ : DivisionMonoid α
a b : α
ha : IsUnit a
hb : IsUnit b
⊢ IsUnit (a * b⁻¹)
Module: Mathlib.Algebra.Group.Units.Defs

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

Tactic:
]

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

Goal state before:
pp: M : Type u_4
F : Type u_5
inst✝ : Monoid F
c : F → M → M
h1 : c 1 = id
hmul : ∀ (f g : F), c (f * g) = c f ∘ c g
f : F
n : ℕ
⊢ (c f)^[n] ∘ c f = (c f)^[n] ∘ c f

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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 : AddCommMonoid α
n : ℕ
a : α
⊢ n • a + a = n • a + a

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a : α
u : αˣ
⊢ a * (↑u)⁻¹ = a * (↑u)⁻¹

Tactic:
]

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

Goal state before:
pp: α : Type u
M : Type u_1
hM : Monoid M
h : ∀ (a : M), IsUnit a
a : M
⊢ a = a

Tactic:
]

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

Goal state before:
pp: α : Type u
M : Type u_1
hM : CommMonoid M
h : ∀ (a : M), IsUnit a
a : M
⊢ a = a

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : α
b : αˣ
⊢ a = a

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
c : αˣ
a b : α
h : a = b * ↑c⁻¹
⊢ b = b

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
c : αˣ
a b : α
h : a * ↑c = b
⊢ a = a

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
b : αˣ
a c : α
h : a = ↑b⁻¹ * c
⊢ c = c

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
b : αˣ
a c : α
h : ↑b * a = c
⊢ a = a

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
b : αˣ
a c : α
h : a * ↑b⁻¹ = c
⊢ a = a

Tactic:
]

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
⊢ f 1 = ↑1

Tactic:
]

Goal state after:
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
⊢ f 1 = ↑1
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : Monoid α
b : αˣ
a c : α
h : a = c * ↑b
⊢ c = c

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u : αˣ
a : α
h : a * ↑u = 1
⊢ ↑u⁻¹ = ↑u⁻¹

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u : αˣ
a : α
h : a * ↑u = 1
⊢ a = a

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u : αˣ
a : α
h : ↑u * a = 1
⊢ ↑u⁻¹ = ↑u⁻¹

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u : αˣ
a : α
h : ↑u * a = 1
⊢ a = a

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u : αˣ
a : α
⊢ a * ↑u = 1 ↔ a * ↑u = 1

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u : αˣ
a : α
⊢ ↑u * a = 1 ↔ ↑u * a = 1

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u₁ u₂ : αˣ
h : ↑u₁ = ↑u₂
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝ : CommMonoid α
a c : α
b d : αˣ
⊢ a * ↑d = c * ↑b ↔ a * ↑d = c * ↑b

Tactic:
]

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

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

Tactic:
]

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✝ : Monoid α
x : α
u : αˣ
y : α
⊢ x * ↑u = y ↔ x * ↑u = y

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : α
u : αˣ
⊢ a = ↑u ↔ a = ↑u

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u : αˣ
⊢ ↑u⁻¹ = ↑u⁻¹

Tactic:
]

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
⊢ a = a

Tactic:
]

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 a
⊢ IsUnit a

Tactic:
]

Goal state after:
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 a
⊢ IsUnit a
Module: Mathlib.Algebra.Group.Units.Basic

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

Tactic:
]

Goal state after:
α : Type u
inst✝¹ : LeftCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : b = 1
⊢ b = 1
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:
]

Goal state after:
α : Type u
inst✝¹ : LeftCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ ¬(a ≠ 1 ∨ b ≠ 1) ↔ a * b = 1
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:
← mul_right_cancel_iff (a := b),

Goal state after:
α : Type u
inst✝¹ : RightCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : a * b = 1
⊢ b * a * b = 1 * b
Module: Mathlib.Algebra.Group.Units.Basic

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
α : Type u
inst✝¹ : RightCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : b = 1
⊢ b = 1
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:
]

Goal state after:
α : Type u
inst✝¹ : RightCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ ¬(a ≠ 1 ∨ b ≠ 1) ↔ a * b = 1
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : CommMonoid α
x y : α
u : αˣ
⊢ x * y * ↑u⁻¹ = x * y * ↑u⁻¹

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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
⊢ a * b = 1

Tactic:
]

Goal state after:
α : Type u
inst✝¹ : CommMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : a * b = 1
⊢ a * b = 1
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:
]

Goal state after:
α : Type u
inst✝¹ : CommMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ ¬(a ≠ 1 ∨ b ≠ 1) ↔ a * b = 1
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 = b

Tactic:
]

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 = 1 ↔ a = 1

Tactic:
]

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

Tactic:
]

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
⊢ b = 1 ↔ b = 1

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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 ↔ a * c = b

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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
⊢ c * b = c * b

Tactic:
]

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 * d = c * b ↔ a * d = c * b

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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₁ * b₂) = (1, b₁ * b₂)

Tactic:
]

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₁ * a₂, 1) = (a₁ * a₂, 1)

Tactic:
]

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
⊢ (fst✝ * g₁, snd✝ * h₁) = (fst✝, snd✝) * (g₁, h₁)

Tactic:
]

Goal state after:
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
⊢ (fst✝ * g₁, snd✝ * h₁) = (fst✝, snd✝) * (g₁, h₁)
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
⊢ (fst✝ * m₁, snd✝ * n₁) = (fst✝ * m₁, snd✝ * n₁)

Tactic:
]

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
⊢ (fst✝ * g₁, snd✝ * h₁) = (fst✝ * g₁, snd✝ * h₁)

Tactic:
]

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: m : Type u → Type v
h : Applicative m
inst✝ : CommApplicative m
α β γ : Type u
a : m α
b : m β
f : α → β → γ
⊢ (fun p ↦ f p.fst p.snd) <$> ((fun b a ↦ (a, b)) <$> b <*> a) = (fun b a ↦ f a b) <$> b <*> a

Tactic:
]

Goal state after:
m : Type u → Type v
h : Applicative m
inst✝ : CommApplicative m
α β γ : Type u
a : m α
b : m β
f : α → β → γ
⊢ (fun p ↦ f p.fst p.snd) <$> ((fun b a ↦ (a, b)) <$> b <*> a) = (fun b a ↦ f a b) <$> b <*> a
Module: Mathlib.Algebra.GroupWithZero.NeZero

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_2
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
h : 1 = 0
x y : M₀
hx : x ≠ y
⊢ x = x

Tactic:
]

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

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_2
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
h : 1 = 0
x y : M₀
hx : x ≠ y
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_2
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
h : 1 = 0
x y : M₀
hx : x ≠ y
⊢ y = y

Tactic:
]

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

Goal state before:
pp: case zero
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
M : Type u_2
inst✝ : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
y : M₀
⊢ f y = f y

Tactic:
]

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

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_2
inst✝³ : MulZeroOneClass M₀
inst✝² : Nontrivial M₀
inst✝¹ : Zero M₀'
inst✝ : One M₀'
f : M₀' → M₀
zero : f 0 = 0
one : f 1 = 1
⊢ ¬0 = 1

Tactic:
]

Goal state after:
M₀ : Type u_1
M₀' : Type u_2
inst✝³ : MulZeroOneClass M₀
inst✝² : Nontrivial M₀
inst✝¹ : Zero M₀'
inst✝ : One M₀'
f : M₀' → M₀
zero : f 0 = 0
one : f 1 = 1
⊢ ¬0 = 1
Module: Mathlib.Algebra.GroupWithZero.Defs

Goal state before:
pp: case succ
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
M : Type u_2
inst✝ : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
n : ℕ
hn : ∀ (y : M₀), f (x ^ n * y) = f x ^ n * f y
y : M₀
⊢ f x * (f x ^ n * f y) = f x * (f x ^ n * f y)

Tactic:
]

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

Goal state before:
pp: M₀ : Type u_1
inst✝² : CommMonoidWithZero M₀
inst✝¹ : Div M₀
inst✝ : MulDivCancelClass M₀
b a : M₀
ha : a ≠ 0
⊢ b = b

Tactic:
]

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

Goal state before:
pp: G₀ : Type u
M₀ : Type u_1
inst✝ : GroupWithZero G₀
a✝ a b : G₀
hb : b ≠ 0
⊢ a = a

Tactic:
]

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

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : NoZeroDivisors M₀'
a b : M₀
H : a * b = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : NoZeroDivisors M₀'
a b : M₀
H✝ : a * b = 0
this : f a * f b = 0
H : f a = 0
⊢ f a = 0

Tactic:
]

Goal state after:
M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : NoZeroDivisors M₀'
a b : M₀
H✝ : a * b = 0
this : f a * f b = 0
H : f a = 0
⊢ f a = 0
Module: Mathlib.Algebra.GroupWithZero.InjSurj

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : NoZeroDivisors M₀'
a b : M₀
H✝ : a * b = 0
this : f a * f b = 0
H : f b = 0
⊢ f b = 0

Tactic:
]

Goal state after:
M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : NoZeroDivisors M₀'
a b : M₀
H✝ : a * b = 0
this : f a * f b = 0
H : f b = 0
⊢ f b = 0
Module: Mathlib.Algebra.GroupWithZero.InjSurj

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsLeftCancelMulZero M₀'
a✝ : M₀
Hne : a✝ ≠ 0
x✝¹ x✝ : M₀
He : (fun x ↦ a✝ * x) x✝¹ = (fun x ↦ a✝ * x) x✝
this : f a✝ * f x✝¹ = f a✝ * f x✝
⊢ x✝¹ = x✝

Tactic:
]

Goal state after:
M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsLeftCancelMulZero M₀'
a✝ : M₀
Hne : a✝ ≠ 0
x✝¹ x✝ : M₀
He : (fun x ↦ a✝ * x) x✝¹ = (fun x ↦ a✝ * x) x✝
this : f a✝ * f x✝¹ = f a✝ * f x✝
⊢ x✝¹ = x✝
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_7
σ : Perm α
m n : ℤ
x : α
⊢ (σ ^ n * σ ^ m) x = (σ ^ n * σ ^ m) x

Tactic:
]

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

Goal state before:
pp: α : Type u_7
β : Type u_8
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
⊢ fst✝¹ = fst✝ ∧ snd✝¹ = snd✝

Tactic:
]

Goal state after:
α : Type u_7
β : Type u_8
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
⊢ fst✝¹ = fst✝ ∧ snd✝¹ = snd✝
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)
⊢ fst✝¹ = fst✝ ∧ snd✝¹ = snd✝

Tactic:
]

Goal state after:
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)
⊢ fst✝¹ = fst✝ ∧ snd✝¹ = snd✝
Module: Mathlib.Algebra.GroupWithZero.InjSurj

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsLeftCancelMulZero M₀'
a✝ : M₀
Hne : a✝ ≠ 0
x✝¹ x✝ : M₀
He : (fun x ↦ a✝ * x) x✝¹ = (fun x ↦ a✝ * x) x✝
this : f a✝ * f x✝¹ = f a✝ * f x✝
Hfa : f a✝ = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsRightCancelMulZero M₀'
a✝ : M₀
Hne : a✝ ≠ 0
x✝¹ x✝ : M₀
He : (fun x ↦ x * a✝) x✝¹ = (fun x ↦ x * a✝) x✝
this : f x✝¹ * f a✝ = f x✝ * f a✝
⊢ x✝¹ = x✝

Tactic:
]

Goal state after:
M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsRightCancelMulZero M₀'
a✝ : M₀
Hne : a✝ ≠ 0
x✝¹ x✝ : M₀
He : (fun x ↦ x * a✝) x✝¹ = (fun x ↦ x * a✝) x✝
this : f x✝¹ * f a✝ = f x✝ * f a✝
⊢ x✝¹ = x✝
Module: Mathlib.Algebra.GroupWithZero.InjSurj

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsRightCancelMulZero M₀'
a✝ : M₀
Hne : a✝ ≠ 0
x✝¹ x✝ : M₀
He : (fun x ↦ x * a✝) x✝¹ = (fun x ↦ x * a✝) x✝
this : f x✝¹ * f a✝ = f x✝ * f a✝
Hfa : f a✝ = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p (f x) ↔ p x
n : ℕ
⊢ ∀ (x : α), p ((f ^ (n + 1))⁻¹ x) ↔ p x

Tactic:
]

Goal state after:
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p (f x) ↔ p x
n : ℕ
⊢ ∀ (x : α), p ((f ^ (n + 1))⁻¹ x) ↔ p x
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
⊢ 0 = 0

Tactic:
]

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
⊢ 0 = 0

Tactic:
]

Goal state after: