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

Goal state before:
pp: M : Type u_2
G : Type u_5
H : Type u_6
inst✝² : MulOneClass M
inst✝¹ : CommGroup G
inst✝ : CommGroup H
φ : G →* H
ψ : M →* G
⊢ φ.comp ψ⁻¹ = (φ.comp ψ)⁻¹

Tactic:
ext

Goal state after:
M : Type u_2
G : Type u_5
H : Type u_6
inst✝² : MulOneClass M
inst✝¹ : CommGroup G
inst✝ : CommGroup H
φ : G →* H
ψ : M →* G
x✝ : M
⊢ (φ.comp ψ⁻¹) x✝ = (φ.comp ψ)⁻¹ x✝
Module: Mathlib.Algebra.Group.Hom.Basic

Goal state before:
pp: M : Type u_2
G : Type u_5
H : Type u_6
inst✝² : MulOneClass M
inst✝¹ : CommGroup G
inst✝ : CommGroup H
f : G →* H
g h : M →* G
⊢ f.comp (g / h) = f.comp g / f.comp h

Tactic:
ext

Goal state after:
M : Type u_2
G : Type u_5
H : Type u_6
inst✝² : MulOneClass M
inst✝¹ : CommGroup G
inst✝ : CommGroup H
f : G →* H
g h : M →* G
x✝ : M
⊢ (f.comp (g / h)) x✝ = (f.comp g / f.comp h) x✝
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:
constructor

Goal state after:
case mp
M : Type u_4
inst✝ : MulOneClass M
a b : M
h : a * b = 1
⊢ a = 1 → b = 1

case mpr
M : Type u_4
inst✝ : MulOneClass M
a b : M
h : a * b = 1
⊢ b = 1 → a = 1
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:
ext

Goal state after:
M : Type u_4
inst✝ : Monoid M
a x✝ : M
⊢ (fun x ↦ a * x)^[0] x✝ = a ^ 0 * x✝
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:
ext

Goal state after:
M : Type u_4
inst✝ : Monoid M
a x✝ : M
⊢ (fun x ↦ x * a)^[0] x✝ = x✝ * a ^ 0
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:
ext

Goal state after:
M : Type u_4
inst✝ : Monoid M
k : ℕ
x✝ : M
⊢ (fun x ↦ x ^ k)^[0] x✝ = x✝ ^ k ^ 0
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:
ext

Goal state after:
M : Type u_4
inst✝ : Monoid M
k n : ℕ
x✝ : M
⊢ (fun x ↦ x ^ k)^[n + 1] x✝ = x✝ ^ k ^ (n + 1)
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 rw [zpow_negSucc, zpow_negSucc, inv_pow]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
k : ℤ
⊢ (fun x ↦ x ^ k)^[0] = fun x ↦ x ^ k ^ 0

Tactic:
ext

Goal state after:
G : Type u_3
inst✝ : Group G
k : ℤ
x✝ : G
⊢ (fun x ↦ x ^ k)^[0] x✝ = x✝ ^ k ^ 0
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : Group G
k : ℤ
n : ℕ
⊢ (fun x ↦ x ^ k)^[n + 1] = fun x ↦ x ^ k ^ (n + 1)

Tactic:
ext

Goal state after:
G : Type u_3
inst✝ : Group G
k : ℤ
n : ℕ
x✝ : G
⊢ (fun x ↦ x ^ k)^[n + 1] x✝ = x✝ ^ k ^ (n + 1)
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:
ext

Goal state after:
α : Type u
inst✝ : Monoid α
a✝ b u a : αˣ
⊢ ↑{ val := NPow.npow 0 ↑a, inv := NPow.npow 0 ↑a⁻¹, val_inv := ⋯, inv_val := ⋯ } = ↑1
Module: Mathlib.Algebra.Group.Units.Defs

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

Tactic:
ext

Goal state after:
α : Type u
inst✝ : Monoid α
a✝ b u : αˣ
n : ℕ
a : αˣ
⊢ ↑{ val := NPow.npow (n + 1) ↑a, inv := NPow.npow (n + 1) ↑a⁻¹, val_inv := ⋯, inv_val := ⋯ } =
    ↑({ val := NPow.npow n ↑a, inv := NPow.npow n ↑a⁻¹, val_inv := ⋯, inv_val := ⋯ } * a)
Module: Mathlib.Algebra.Group.Units.Hom

Goal state before:
pp: M : Type u
inst✝ : Monoid M
⊢ map (MonoidHom.id M) = MonoidHom.id Mˣ

Tactic:
ext

Goal state after:
M : Type u
inst✝ : Monoid M
x✝ : Mˣ
⊢ ↑((map (MonoidHom.id M)) x✝) = ↑((MonoidHom.id Mˣ) x✝)
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
⊢ g 1 = 1

Tactic:
ext

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
⊢ ↑(g 1) = ↑1
Module: Mathlib.Algebra.Group.Units.Hom

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝¹ : Group G
inst✝ : CommMonoid M
f g : G →* M
⊢ (f * g).toHomUnits = f.toHomUnits * g.toHomUnits

Tactic:
ext

Goal state after:
G : Type u_1
M : Type u_2
inst✝¹ : Group G
inst✝ : CommMonoid M
f g : G →* M
x✝ : G
⊢ ↑((f * g).toHomUnits x✝) = ↑((f.toHomUnits * g.toHomUnits) x✝)
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:
h.mul_left_inj

Goal state after:
M : Type u_1
inst✝ : Monoid M
a b : M
h : IsUnit b
⊢ a = 1 ↔ a = 1
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:
ext

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

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

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

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

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

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

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

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

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

Goal state after:
case fst
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✝).1 = (x✝ * x✝¹).1

case snd
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✝).2 = (x✝ * x✝¹).2
Module: Mathlib.Algebra.Group.Prod

Goal state before:
pp: case fst
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✝).1 = (x✝ * x✝¹).1

Tactic:
apply mul_comm'

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

Goal state before:
pp: case snd
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✝).2 = (x✝ * x✝¹).2

Tactic:
apply mul_comm'

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

Goal state after:
case fst
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✝).1 = (x✝ * x✝¹).1

case snd
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✝).2 = (x✝ * x✝¹).2
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:
ext

Goal state after:
case fst
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✝).1 = (x✝² * (x✝¹ * x✝)).1

case snd
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✝).2 = (x✝² * (x✝¹ * x✝)).2
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:
ext

Goal state after:
case fst
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✝).1 = x✝.1

case snd
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✝).2 = x✝.2
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:
ext

Goal state after:
case fst
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).1 = x✝.1

case snd
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).2 = x✝.2
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:
ext

Goal state after:
case fst
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.1 = b.1

case snd
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.2 = b.2
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:
ext

Goal state after:
case fst
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✝).1 = (x✝¹ * x✝⁻¹).1

case snd
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✝).2 = (x✝¹ * x✝⁻¹).2
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:
ext

Goal state after:
case fst
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 = 1.1

case snd
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).2 = 1.2
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:
ext

Goal state after:
case fst
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).1 = (x✝ ^ ↑x✝¹ * x✝).1

case snd
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).2 = (x✝ ^ ↑x✝¹ * x✝).2
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:
ext

Goal state after:
case fst
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✝¹).1 = (x✝ ^ ↑x✝¹.succ)⁻¹.1

case snd
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✝¹).2 = (x✝ ^ ↑x✝¹.succ)⁻¹.2
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:
ext

Goal state after:
case fst
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 = 1.1

case snd
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✝).2 = 1.2
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
x : F (α → β)
f : γ → α
y : F γ
⊢ ((fun h ↦ h f) ∘ Function.comp) <$> x <*> y = (pure fun x ↦ x ∘ f) <*> x <*> y

Tactic:
simp [pure_seq]

Goal state after:
α β γ : Type u
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
x : F (α → β)
f : γ → α
y : F γ
⊢ ((fun h ↦ h f) ∘ Function.comp) <$> x <*> y = (fun x ↦ x ∘ f) <$> x <*> y
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
e : Type v
⊢ LawfulFunctor (Sum e)

Tactic:
constructor

Goal state after:
case map_const
α β γ : Type u
e : Type v
⊢ ∀ {α β : Type u}, Functor.mapConst = Functor.map ∘ Function.const β

case id_map
α β γ : Type u
e : Type v
⊢ ∀ {α : Type u} (x : e ⊕ α), id <$> x = x

case comp_map
α β γ : Type u
e : Type v
⊢ ∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : e ⊕ α), (h ∘ g) <$> x = h <$> g <$> x
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:
constructor

Goal state after:
case left
α : Type u_7
β : Type u_8
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
⊢ fst✝¹ = fst✝

case right
α : Type u_7
β : Type u_8
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
⊢ snd✝¹ = snd✝