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

Goal state before:
pp: R✝ : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
R₄ : Type u_5
S✝ : Type u_6
M : Type u_7
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
M₄ : Type u_11
N₁ : Type u_12
N₂ : Type u_13
S : Type u_14
R : Type u_15
V : Type u_16
W : Type u_17
G : Type u_18
inst✝¹⁴ : Semiring R
inst✝¹³ : Semiring S
inst✝¹² : AddCommMonoid V
inst✝¹¹ : Module R V
inst✝¹⁰ : Module S V
inst✝⁹ : AddCommMonoid W
inst✝⁸ : Module R W
inst✝⁷ : Module S W
inst✝⁶ : AddCommMonoid G
inst✝⁵ : Module R G
inst✝⁴ : Module S G
inst✝³ : SMulCommClass R S W
inst✝² : SMul S R
inst✝¹ : IsScalarTower S R V
inst✝ : IsScalarTower S R W
α : Sˣ
e : V ≃ₗ[R] W
x✝ : W
⊢ (↑α • ↑e).toFun ((fun x ↦ ↑α⁻¹ • e.symm x) x✝) = x✝

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring R₂
inst✝¹² : Semiring R₃
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommGroup N₂
inst✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R₁ M
inst✝⁵ : Module R₂ M₂
inst✝⁴ : Module R₃ M₃
inst✝³ : Module R₂ N₂
inst✝² : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : Subsingleton M
f : M →ₛₗ[σ₁₂] M₂
x : M
⊢ f x = default x

Tactic:
by

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

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
M : Type u_8
M₂ : Type u_10
inst✝⁶ : Semiring R₁
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₁ M
inst✝¹ : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
inst✝ : Nontrivial M
f : M →ₛₗ[σ₁₂] M₂
hf : Injective ⇑f
x : M
ne : x ≠ 0
h : f = 0
⊢ f x = f 0

Tactic:
by

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

Goal state before:
pp: S : Type u_14
R : Type u_15
V : Type u_16
W : Type u_17
G : Type u_18
inst✝¹⁶ : Semiring R
inst✝¹⁵ : Semiring S
inst✝¹⁴ : AddCommMonoid V
inst✝¹³ : Module R V
inst✝¹² : Module S V
inst✝¹¹ : AddCommMonoid W
inst✝¹⁰ : Module R W
inst✝⁹ : Module S W
inst✝⁸ : AddCommMonoid G
inst✝⁷ : Module R G
inst✝⁶ : Module S G
inst✝⁵ : SMulCommClass R S W
inst✝⁴ : SMul S R
inst✝³ : IsScalarTower S R V
inst✝² : IsScalarTower S R W
inst✝¹ : SMulCommClass R S V
inst✝ : IsScalarTower S R G
α : Sˣ
e : G ≃ₗ[R] V
f : V ≃ₗ[R] W
⊢ (α • e) ≪≫ₗ f = α • e ≪≫ₗ f

Tactic:
by

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

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
M : Type u_8
M₂ : Type u_10
inst✝⁶ : Semiring R₁
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₁ M
inst✝¹ : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
inst✝ : Nontrivial M₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective ⇑f
⊢ f ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommGroup N₂
inst✝⁶ : AddCommGroup N₃
inst✝⁵ : Module R₁ M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
inst✝² : Module R₂ N₂
inst✝¹ : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f g : M →ₛₗ[σ₁₂] M₂
⊢ ∀ (x y : M), (⇑f + ⇑g) (x + y) = (⇑f + ⇑g) x + (⇑f + ⇑g) y

Tactic:
by

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

Goal state before:
pp: S : Type u_14
R : Type u_15
V : Type u_16
W : Type u_17
G : Type u_18
inst✝¹⁵ : Semiring R
inst✝¹⁴ : Semiring S
inst✝¹³ : AddCommMonoid V
inst✝¹² : Module R V
inst✝¹¹ : Module S V
inst✝¹⁰ : AddCommMonoid W
inst✝⁹ : Module R W
inst✝⁸ : Module S W
inst✝⁷ : AddCommMonoid G
inst✝⁶ : Module R G
inst✝⁵ : Module S G
inst✝⁴ : SMulCommClass R S W
inst✝³ : SMul S R
inst✝² : IsScalarTower S R V
inst✝¹ : IsScalarTower S R W
inst✝ : IsScalarTower S R G
α : Sˣ
e : G ≃ₗ[R] V
f : V ≃ₗ[R] W
⊢ e ≪≫ₗ (α • f) = α • e ≪≫ₗ f

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommGroup N₂
inst✝⁶ : AddCommGroup N₃
inst✝⁵ : Module R₁ M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
inst✝² : Module R₂ N₂
inst✝¹ : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f g : M →ₛₗ[σ₁₂] M₂
⊢ ∀ (m : R₁) (x : M), (⇑f + ⇑g) (m • x) = σ₁₂ m • (⇑f + ⇑g) x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁴ : SMul M X
inst✝³ : SMul M' X
Y : Type u_6
inst✝² : SMul N Y
inst✝¹ : SMul M' Y
Z : Type u_7
inst✝ : SMul P Z
f g : X →ₑ[φ] Y
h : f.toFun = g.toFun
⊢ f = g

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommGroup N₂
inst✝⁶ : AddCommGroup N₃
inst✝⁵ : Module R₁ M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
inst✝² : Module R₂ N₂
inst✝¹ : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M →ₛₗ[σ₁₂] N₂
⊢ ∀ (x y : M), (-⇑f) (x + y) = (-⇑f) x + (-⇑f) y

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommGroup N₂
inst✝⁶ : AddCommGroup N₃
inst✝⁵ : Module R₁ M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
inst✝² : Module R₂ N₂
inst✝¹ : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M →ₛₗ[σ₁₂] N₂
⊢ ∀ (m : R₁) (x : M), (-⇑f) (m • x) = σ₁₂ m • (-⇑f) x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommGroup N₂
inst✝⁶ : AddCommGroup N₃
inst✝⁵ : Module R₁ M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
inst✝² : Module R₂ N₂
inst✝¹ : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f g : M →ₛₗ[σ₁₂] N₂
x y : M
⊢ (⇑f - ⇑g) (x + y) = (⇑f - ⇑g) x + (⇑f - ⇑g) y

Tactic:
simp only [Pi.sub_apply, map_add, add_sub_add_comm]

Goal state after:
Module: Mathlib.Algebra.Module.Pi

Goal state before:
pp: I : Type u
f : I → Type v
g : I → Type u_1
r : (i : I) → Semiring (f i)
m : (i : I) → AddCommMonoid (g i)
inst✝ : (i : I) → Module (f i) (g i)
⊢ ∀ (r_1 s : (i : I) → f i) (x : (i : I) → g i), (r_1 + s) • x = r_1 • x + s • x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Pi

Goal state before:
pp: I : Type u
f : I → Type v
g : I → Type u_1
r : (i : I) → Semiring (f i)
m : (i : I) → AddCommMonoid (g i)
inst✝ : (i : I) → Module (f i) (g i)
⊢ ∀ (x : (i : I) → g i), 0 • x = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommGroup N₂
inst✝⁶ : AddCommGroup N₃
inst✝⁵ : Module R₁ M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
inst✝² : Module R₂ N₂
inst✝¹ : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f g : M →ₛₗ[σ₁₂] N₂
x y : M
⊢ (⇑f - ⇑g) (x + y) = (⇑f - ⇑g) x + (⇑f - ⇑g) y

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M' : Type u_1
X : Type u_5
inst✝⁶ : SMul M' X
Y : Type u_6
inst✝⁵ : SMul M' Y
F : Type u_8
inst✝⁴ : FunLike F X Y
inst✝³ : MulOneClass X
inst✝² : SMul X Y
inst✝¹ : IsScalarTower M' X Y
inst✝ : MulActionHomClass F X X Y
f : F
m : M'
x : X
⊢ f (m • x) = id m • f x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M' : Type u_1
X : Type u_5
inst✝⁴ : SMul M' X
Y : Type u_6
inst✝³ : SMul M' Y
F : Type u_8
inst✝² : FunLike F X Y
inst✝¹ : FaithfulSMul M' X
inst✝ : MulActionHomClass F M' X Y
f : F
hf : Function.Injective ⇑f
x✝¹ x✝ : M'
h : ∀ (a : Y), x✝¹ • a = x✝ • a
m : X
⊢ f (x✝¹ • m) = f (x✝ • m)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommGroup N₂
inst✝⁶ : AddCommGroup N₃
inst✝⁵ : Module R₁ M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
inst✝² : Module R₂ N₂
inst✝¹ : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f g : M →ₛₗ[σ₁₂] N₂
r : R₁
x : M
⊢ (⇑f - ⇑g) (r • x) = σ₁₂ r • (⇑f - ⇑g) x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁴ : SMul M X
inst✝³ : SMul M' X
Y : Type u_6
inst✝² : SMul N Y
inst✝¹ : SMul M' Y
Z : Type u_7
inst✝ : SMul P Z
g : Y →ₑ[ψ] Z
f : X →ₑ[φ] Y
κ : CompTriple φ ψ χ
m : M
x : X
⊢ g (f (m • x)) = g (φ m • f x)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommGroup N₂
inst✝⁶ : AddCommGroup N₃
inst✝⁵ : Module R₁ M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
inst✝² : Module R₂ N₂
inst✝¹ : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
⊢ toAddMonoidHom 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁴ : SMul M X
inst✝³ : SMul M' X
Y : Type u_6
inst✝² : SMul N Y
inst✝¹ : SMul M' Y
Z : Type u_7
inst✝ : SMul P Z
g : Y →ₑ[ψ] Z
f : X →ₑ[φ] Y
κ : CompTriple φ ψ χ
m : M
x : X
⊢ g (φ m • f x) = ψ (φ m) • g (f x)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁴ : SMul M X
inst✝³ : SMul M' X
Y : Type u_6
inst✝² : SMul N Y
inst✝¹ : SMul M' Y
Z : Type u_7
inst✝ : SMul P Z
g : Y →ₑ[ψ] Z
f : X →ₑ[φ] Y
κ : CompTriple φ ψ χ
m : M
x : X
⊢ (ψ ∘ φ) m • g (f x) = χ m • g (f x)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst✝¹ : SMul M X
Y : Type u_6
inst✝ : SMul N Y
f : X →ₑ[φ] Y
x : X
⊢ ((MulActionHom.id N).comp f) x = f x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst✝¹ : SMul M X
Y : Type u_6
inst✝ : SMul N Y
f : X →ₑ[φ] Y
x : X
⊢ (f.comp (MulActionHom.id M)) x = f x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommGroup N₂
inst✝⁶ : AddCommGroup N₃
inst✝⁵ : Module R₁ M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
inst✝² : Module R₂ N₂
inst✝¹ : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
⊢ ∀ (x y : M →ₛₗ[σ₁₂] M₂), (x + y).toAddMonoidHom = x.toAddMonoidHom + y.toAddMonoidHom

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁵ : SMul M X
inst✝⁴ : SMul M' X
Y : Type u_6
inst✝³ : SMul N Y
inst✝² : SMul M' Y
Z : Type u_7
inst✝¹ : SMul P Z
φ' : N → M
Y₁ : Type u_8
inst✝ : SMul M Y₁
f : X →ₑ[id] Y₁
g : Y₁ → X
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
m : M
x : Y₁
⊢ g (m • x) = g (m • f (g x))

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁵ : SMul M X
inst✝⁴ : SMul M' X
Y : Type u_6
inst✝³ : SMul N Y
inst✝² : SMul M' Y
Z : Type u_7
inst✝¹ : SMul P Z
φ' : N → M
Y₁ : Type u_8
inst✝ : SMul M Y₁
f : X →ₑ[id] Y₁
g : Y₁ → X
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
m : M
x : Y₁
⊢ g (m • f (g x)) = g (f (m • g x))

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁵ : SMul M X
inst✝⁴ : SMul M' X
Y : Type u_6
inst✝³ : SMul N Y
inst✝² : SMul M' Y
Z : Type u_7
inst✝¹ : SMul P Z
φ' : N → M
Y₁ : Type u_8
inst✝ : SMul M Y₁
f : X →ₑ[id] Y₁
g : Y₁ → X
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
m : M
x : Y₁
⊢ g (f (m • g x)) = m • g x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁵ : SMul M X
inst✝⁴ : SMul M' X
Y : Type u_6
inst✝³ : SMul N Y
inst✝² : SMul M' Y
Z : Type u_7
inst✝¹ : SMul P Z
φ' : N → M
Y₁ : Type u_8
inst✝ : SMul M Y₁
f : X →ₑ[φ] Y
g : Y → X
k : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
m : N
x : Y
⊢ g (m • x) = g (m • f (g x))

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁵ : SMul M X
inst✝⁴ : SMul M' X
Y : Type u_6
inst✝³ : SMul N Y
inst✝² : SMul M' Y
Z : Type u_7
inst✝¹ : SMul P Z
φ' : N → M
Y₁ : Type u_8
inst✝ : SMul M Y₁
f : X →ₑ[φ] Y
g : Y → X
k : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
m : N
x : Y
⊢ g (m • f (g x)) = g (φ (φ' m) • f (g x))

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁵ : SMul M X
inst✝⁴ : SMul M' X
Y : Type u_6
inst✝³ : SMul N Y
inst✝² : SMul M' Y
Z : Type u_7
inst✝¹ : SMul P Z
φ' : N → M
Y₁ : Type u_8
inst✝ : SMul M Y₁
f : X →ₑ[φ] Y
g : Y → X
k : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
m : N
x : Y
⊢ g (φ (φ' m) • f (g x)) = g (f (φ' m • g x))

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁵ : SMul M X
inst✝⁴ : SMul M' X
Y : Type u_6
inst✝³ : SMul N Y
inst✝² : SMul M' Y
Z : Type u_7
inst✝¹ : SMul P Z
φ' : N → M
Y₁ : Type u_8
inst✝ : SMul M Y₁
f : X →ₑ[φ] Y
g : Y → X
k : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
m : N
x : Y
⊢ g (f (φ' m • g x)) = φ' m • g x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M : Type u_2
X : Type u_5
inst✝¹ : SMul M X
Y₁ : Type u_8
inst✝ : SMul M Y₁
f : X →ₑ[id] Y₁
g : Y₁ → X
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
⊢ f.inverse g h₁ h₂ = f.inverse' g ⋯ h₁ h₂

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst✝¹ : SMul M X
Y : Type u_6
inst✝ : SMul N Y
φ' : N → M
f : X →ₑ[φ] Y
g : Y → X
k₁ : Function.LeftInverse φ' φ
k₂ : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
⊢ (f.inverse' g k₂ h₁ h₂).comp f = MulActionHom.id M

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst✝¹ : SMul M X
Y : Type u_6
inst✝ : SMul N Y
φ' : N → M
f : X →ₑ[φ] Y
g : Y → X
k₂ : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
⊢ f.comp (f.inverse' g k₂ h₁ h₂) = MulActionHom.id N

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝³ : SMul M X
inst✝² : SMul N Y
inst✝¹ : SMul R Y
inst✝ : SMulCommClass N R Y
h : R
f : X →ₑ[σ] Y
⊢ ∀ (m : M) (x : X), (h • ⇑f) (m • x) = σ m • (h • ⇑f) x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝² : SMul M X
inst✝¹ : Zero Y
inst✝ : SMulZeroClass N Y
⊢ ∀ (m : M) (x : X), 0 (m • x) = σ m • 0 x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝² : SMul M X
inst✝¹ : AddZeroClass Y
inst✝ : DistribSMul N Y
f g : X →ₑ[σ] Y
⊢ ∀ (m : M) (x : X), (⇑f + ⇑g) (m • x) = σ m • (⇑f + ⇑g) x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝² : SMul M X
inst✝¹ : AddGroup Y
inst✝ : DistribSMul N Y
f : X →ₑ[σ] Y
⊢ ∀ (m : M) (x : X), (-⇑f) (m • x) = σ m • (-⇑f) x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝² : SMul M X
inst✝¹ : AddGroup Y
inst✝ : DistribSMul N Y
f g : X →ₑ[σ] Y
⊢ ∀ (m : M) (x : X), (⇑f - ⇑g) (m • x) = σ m • (⇑f - ⇑g) x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝³ : SMul M X
inst✝² : Monoid N
inst✝¹ : Monoid Y
inst✝ : MulDistribMulAction N Y
f g : X →ₑ[σ] Y
⊢ ∀ (m : M) (x : X), (⇑f * ⇑g) (m • x) = σ m • (⇑f * ⇑g) x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝³ : SMul M X
inst✝² : Monoid N
inst✝¹ : Monoid Y
inst✝ : MulDistribMulAction N Y
⊢ ∀ (m : M) (x : X), 1 (m • x) = σ m • 1 x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝ : Monoid M
f : M →ₑ[id] M
⊢ (fun m ↦ { toFun := fun x ↦ x * MulOpposite.unop m, map_smul' := ⋯ }) ((fun f ↦ MulOpposite.op (f 1)) f) = f

Tactic:
by

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

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
m₁✝ m₂✝ : αᵐᵒᵖ
h : ∀ (a : α), m₁✝ • a = m₂✝ • a
⊢ m₁✝ = m₂✝

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝ : Monoid M
f g : M →ₑ[id] M
⊢ (f * g) 1 = MulOpposite.unop (MulOpposite.op (g 1)) * MulOpposite.unop (MulOpposite.op (f 1))

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝ : Monoid M
f : M →ₑ[id] M
⊢ (fun m ↦ { toFun := fun x ↦ m * x, map_smul' := ⋯ }) ((fun f ↦ f 1) f) = f

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M : Type u_1
inst✝¹⁴ : Monoid M
N : Type u_2
inst✝¹³ : Monoid N
P : Type u_3
inst✝¹² : Monoid P
φ : M →* N
φ' : N →* M
ψ : N →* P
χ : M →* P
A : Type u_4
inst✝¹¹ : Monoid A
inst✝¹⁰ : MulDistribMulAction M A
B : Type u_5
inst✝⁹ : Monoid B
inst✝⁸ : MulDistribMulAction N B
B₁ : Type u_6
inst✝⁷ : Monoid B₁
inst✝⁶ : MulDistribMulAction M B₁
C : Type u_7
inst✝⁵ : Monoid C
inst✝⁴ : MulDistribMulAction P C
A' : Type u_8
inst✝³ : Group A'
inst✝² : MulDistribMulAction M A'
B' : Type u_9
inst✝¹ : Group B'
inst✝ : MulDistribMulAction N B'
f g : A →ₑ*[φ] B
h : (fun m ↦ m.toFun) f = (fun m ↦ m.toFun) g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Pi

Goal state before:
pp: I : Type u
f : I → Type v
i : I
inst✝ : (i : I) → Distrib (f i)
⊢ ∀ (a b c : (i : I) → f i), a * (b + c) = a * b + a * c

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M : Type u_1
inst✝⁵ : Monoid M
N : Type u_2
inst✝⁴ : Monoid N
φ : M →* N
A : Type u_4
inst✝³ : Monoid A
inst✝² : MulDistribMulAction M A
B : Type u_5
inst✝¹ : Monoid B
inst✝ : MulDistribMulAction N B
f g : A →ₑ*[φ] B
h : ↑f = ↑g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
A : Type u_4
inst✝¹ : Monoid A
inst✝ : MulDistribMulAction M A
x : A
⊢ (MulDistribMulActionHom.id M) x = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Pi

Goal state before:
pp: I : Type u
f : I → Type v
i : I
inst✝ : (i : I) → Distrib (f i)
⊢ ∀ (a b c : (i : I) → f i), (a + b) * c = a * c + b * c

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M : Type u_1
inst✝¹⁹ : Monoid M
N : Type u_2
inst✝¹⁸ : Monoid N
P : Type u_3
inst✝¹⁷ : Monoid P
φ : M →* N
φ' : N →* M
ψ : N →* P
χ : M →* P
A✝ : Type u_4
inst✝¹⁶ : Monoid A✝
inst✝¹⁵ : MulDistribMulAction M A✝
B✝ : Type u_5
inst✝¹⁴ : Monoid B✝
inst✝¹³ : MulDistribMulAction N B✝
B₁ : Type u_6
inst✝¹² : Monoid B₁
inst✝¹¹ : MulDistribMulAction M B₁
C : Type u_7
inst✝¹⁰ : Monoid C
inst✝⁹ : MulDistribMulAction P C
A' : Type u_8
inst✝⁸ : Group A'
inst✝⁷ : MulDistribMulAction M A'
B' : Type u_9
inst✝⁶ : Group B'
inst✝⁵ : MulDistribMulAction N B'
F : Type u_10
inst✝⁴ : FunLike F A✝ B✝
A : Type u_11
inst✝³ : AddMonoid A
inst✝² : DistribMulAction M A
B : Type u_12
inst✝¹ : AddMonoid B
inst✝ : DistribMulAction N B
m : M
x✝ : A
⊢ (↑0).toFun (m • x✝) = φ m • (↑0).toFun x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Pi

Goal state before:
pp: I : Type u
f : I → Type u_1
inst✝ : (i : I) → Semiring (f i)
i : I
x : f i
⊢ (i : I) → f i

Tactic:
by

Goal state after: