mathlib-initiative/mathlib-tactics huggingface dataset:
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 : A →ₑ*[φ] B
x : A
⊢ ((MulDistribMulActionHom.id N).comp f) x = f 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
⊢ ((Pi.evalRingHom f i) fun x_1 ↦ if h : x_1 = i then ⋯ ▸ x else 0) = x

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 : A →ₑ*[φ] B
x : A
⊢ (f.comp (MulDistribMulActionHom.id M)) x = f x

Tactic:
by

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

Goal state before:
pp: R : Type u_10
inst✝³ : Semiring R
S : Type u_11
inst✝² : Semiring S
N' : Type u_13
inst✝¹ : AddMonoid N'
inst✝ : DistribMulAction S N'
σ : R →* S
f g : R →ₑ+[σ] N'
h : f 1 = g 1
⊢ f = g

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'
R : Type u_10
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_11
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_12
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction N S
S' : Type u_13
inst✝³ : Ring S'
inst✝² : MulSemiringAction N S'
T : Type u_14
inst✝¹ : Semiring T
inst✝ : MulSemiringAction P T
f g : R →ₑ+*[φ] S
h : (fun m ↦ m.toFun) f = (fun m ↦ m.toFun) g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Regular.Opposite

Goal state before:
pp: R : Type u_1
inst✝ : Mul R
a : R
⊢ IsRegular (op a) ↔ IsRegular a

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
R : Type u_10
inst✝³ : Semiring R
inst✝² : MulSemiringAction M R
S : Type u_12
inst✝¹ : Semiring S
inst✝ : MulSemiringAction N S
f : R →ₑ+*[φ] S
x : R
⊢ ((MulSemiringActionHom.id N).comp f) x = f x

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
R : Type u_10
inst✝³ : Semiring R
inst✝² : MulSemiringAction M R
S : Type u_12
inst✝¹ : Semiring S
inst✝ : MulSemiringAction N S
f : R →ₑ+*[φ] S
x : R
⊢ (f.comp (MulSemiringActionHom.id M)) x = f x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
σ : Rᵐᵒᵖ →+* S
f g : R →ₛₗ[σ] M
h : f 1 = g 1
x : R
⊢ f x = g x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : IsTorsionFree R N
f : M → N
hf : Injective f
smul : ∀ (r : R) (m : M), f (r • m) = r • f m
r : R
hr : IsRegular r
m₁ m₂ : M
hm : (fun x ↦ r • x) m₁ = (fun x ↦ r • x) m₂
⊢ (fun x ↦ r • x) (f m₁) = (fun x ↦ r • x) (f m₂)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
r : R
m m₁ m₂ : M
inst✝ : IsAddTorsionFree M
n : ℕ
hn : IsRegular n
⊢ n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
r : R
m : M
inst✝ : IsTorsionFree R M
hr : IsRegular r
⊢ r • m = 0 ↔ m = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsTorsionFree R M
inst✝⁴ : Module S R
inst✝³ : IsTorsionFree S R
inst✝² : IsScalarTower S R R
inst✝¹ : SMulCommClass S R R
inst✝ : IsScalarTower S R M
s : S
hs : IsRegular s
x y : M
hxy : (fun x ↦ s • x) x = (fun x ↦ s • x) y
⊢ (fun x ↦ (s • 1) • x) x = (fun x ↦ (s • 1) • x) y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsTorsionFree R M
inst✝⁴ : Module S R
inst✝³ : IsTorsionFree S R
inst✝² : IsScalarTower S R R
inst✝¹ : SMulCommClass S R R
inst✝ : IsScalarTower S R M
s : S
hs : IsRegular s
x✝ y✝ : M
hxy✝ : (fun x ↦ s • x) x✝ = (fun x ↦ s • x) y✝
x y : R
hxy : (fun x ↦ s • 1 * x) x = (fun x ↦ s • 1 * x) y
⊢ (fun x ↦ s • x) x = (fun x ↦ s • x) y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsTorsionFree R M
inst✝⁴ : Module S R
inst✝³ : IsTorsionFree S R
inst✝² : IsScalarTower S R R
inst✝¹ : SMulCommClass S R R
inst✝ : IsScalarTower S R M
s : S
hs : IsRegular s
x✝ y✝ : M
hxy✝ : (fun x ↦ s • x) x✝ = (fun x ↦ s • x) y✝
x y : R
hxy : (fun x ↦ x * s • 1) x = (fun x ↦ x * s • 1) y
⊢ (fun x ↦ s • x) x = (fun x ↦ s • x) y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsTorsionFree R M
inst✝⁴ : Module S R
inst✝³ : IsTorsionFree S R
inst✝² : IsScalarTower S R R
inst✝¹ : SMulCommClass S R R
inst✝ : IsScalarTower S R M
s : S
hs : IsRegular s
x y : M
hxy : (fun x ↦ s • x) x = (fun x ↦ s • x) y
⊢ x = y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r : R
m : M
inst✝¹ : IsTorsionFree R M
inst✝ : IsCancelMulZero R
⊢ r • m = 0 ↔ r = 0 ∨ m = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r : R
m : M
inst✝¹ : IsTorsionFree R M
inst✝ : IsCancelMulZero R
⊢ r • m ≠ 0 ↔ r ≠ 0 ∧ m ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r : R
m : M
inst✝¹ : IsTorsionFree R M
inst✝ : IsCancelMulZero R
hr : r ≠ 0
hm : m ≠ 0
⊢ r • m ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r : R
m : M
inst✝¹ : IsTorsionFree R M
inst✝ : IsCancelMulZero R
hm : m ≠ 0
⊢ r • m = 0 ↔ r = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r : R
m : M
inst✝¹ : IsTorsionFree R M
inst✝ : IsCancelMulZero R
hm : m ≠ 0
⊢ r • m ≠ 0 ↔ r ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : IsTorsionFree R M
inst✝¹ : IsCancelMulZero R
inst✝ : CharZero R
n : ℕ
hn : n ≠ 0
⊢ Function.Injective fun a ↦ n • a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
m : M
inst✝ : IsAddTorsionFree M
n : ℤ
hn : IsRegular n
⊢ n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
h : ∀ (r : R) (m : M), r • m = 0 → r = 0 ∨ m = 0
r : R
hr : IsRegular r
m₁ m₂ : M
hm : (fun x ↦ r • x) m₁ = (fun x ↦ r • x) m₂
⊢ r • (m₁ - m₂) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
h : ∀ (r : R) (m : M), r • m = 0 → r = 0 ∨ m = 0
r : R
hr : IsRegular r
m₁ m₂ : M
hm : (fun x ↦ r • x) m₁ = (fun x ↦ r • x) m₂
⊢ m₁ = m₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : M
inst✝¹ : IsCancelMulZero R
inst✝ : IsTorsionFree R M
hm : m ≠ 0
⊢ Function.Injective fun x ↦ x • m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial M
inst✝ : IsAddTorsionFree M
n m : ℕ
h : ↑n = ↑m
x : M
hx : x ≠ 0
⊢ ↑n • x = ↑m • x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial M
inst✝ : IsAddTorsionFree M
⊢ CharZero R

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝² x✝¹ : R
x✝ : M × N
⊢ (x✝² + x✝¹) • x✝ = x✝² • x✝ + x✝¹ • x✝

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ : M × N
⊢ 0 • x✝ = 0

Tactic:
by

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

Goal state before:
pp: M : Type u_1
β : Type u_4
inst✝³ : SMul M β
α : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction M α
a : M
c : β
⊢ a • (0, c) = (0, a • c)

Tactic:
by

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

Goal state before:
pp: M : Type u_1
α : Type u_3
inst✝³ : SMul M α
β : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid β
inst✝ : DistribMulAction M β
a : M
b : α
⊢ a • (b, 0) = (a • b, 0)

Tactic:
by

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

Goal state before:
pp: M✝ : Type u_1
N✝ : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
M : Type u_6
N : Type u_7
inst✝³ : Zero M
inst✝² : Zero N
inst✝¹ : SMulZeroClass R M
inst✝ : SMulZeroClass R N
x✝ : R
⊢ x✝ • 0 = 0

Tactic:
by

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

Goal state before:
pp: M✝ : Type u_1
N✝ : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
M : Type u_6
N : Type u_7
inst✝³ : AddZeroClass M
inst✝² : AddZeroClass N
inst✝¹ : DistribSMul R M
inst✝ : DistribSMul R N
x✝² : R
x✝¹ x✝ : M × N
⊢ x✝² • (x✝¹ + x✝) = x✝² • x✝¹ + x✝² • x✝

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R'
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M
inst✝⁶ : Module R' M'
σ₁₂ : R →+* R'
S' : Type u_6
T' : Type u_7
inst✝⁵ : Monoid S'
inst✝⁴ : DistribMulAction S' M
inst✝³ : SMulCommClass R S' M
inst✝² : Monoid T'
inst✝¹ : DistribMulAction T' M
inst✝ : SMulCommClass R T' M
a : S'ᵈᵐᵃ
f : M →ₛₗ[σ₁₂] M'
x y : M
⊢ (a • ⇑f) (x + y) = (a • ⇑f) x + (a • ⇑f) y

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
inst✝⁴ : Monoid R
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : MulDistribMulAction R M
inst✝ : MulDistribMulAction R N
x✝ : R
⊢ x✝ • 1 = 1

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
inst✝⁴ : Monoid R
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : MulDistribMulAction R M
inst✝ : MulDistribMulAction R N
x✝² : R
x✝¹ x✝ : M × N
⊢ x✝² • (x✝¹ * x✝) = x✝² • x✝¹ * x✝² • x✝

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
inst✝⁴ : Zero R
inst✝³ : Zero M
inst✝² : Zero N
inst✝¹ : SMulWithZero R M
inst✝ : SMulWithZero R N
x✝ : M × N
⊢ 0 • x✝ = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R'
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M
inst✝⁶ : Module R' M'
σ₁₂ : R →+* R'
S' : Type u_6
T' : Type u_7
inst✝⁵ : Monoid S'
inst✝⁴ : DistribMulAction S' M
inst✝³ : SMulCommClass R S' M
inst✝² : Monoid T'
inst✝¹ : DistribMulAction T' M
inst✝ : SMulCommClass R T' M
a : S'ᵈᵐᵃ
f : M →ₛₗ[σ₁₂] M'
c : R
x : M
⊢ (a • ⇑f) (c • x) = σ₁₂ c • (a • ⇑f) x

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : AddMonoid α
inst✝² : DistribMulAction M α
inst✝¹ : DistribMulAction N α
inst✝ : SMulCommClass M N α
mn : M × N
⊢ mn • 0 = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
inst✝¹² : Semiring R
inst✝¹¹ : Semiring R'
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : Module R M
inst✝⁷ : Module R' M'
σ₁₂ : R →+* R'
S' : Type u_6
T' : Type u_7
inst✝⁶ : Monoid S'
inst✝⁵ : DistribMulAction S' M
inst✝⁴ : SMulCommClass R S' M
inst✝³ : Monoid T'
inst✝² : DistribMulAction T' M
inst✝¹ : SMulCommClass R T' M
inst✝ : SMulCommClass S' T' M
s : S'ᵈᵐᵃ
t : T'ᵈᵐᵃ
f : M →ₛₗ[σ₁₂] M'
m : M
⊢ (s • t • f) m = (t • s • f) m

Tactic:
simp_rw [DomMulAct.smul_linearMap_apply, smul_comm]

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
inst✝¹² : Semiring R
inst✝¹¹ : Semiring R'
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : Module R M
inst✝⁷ : Module R' M'
σ₁₂ : R →+* R'
S' : Type u_6
T' : Type u_7
inst✝⁶ : Monoid S'
inst✝⁵ : DistribMulAction S' M
inst✝⁴ : SMulCommClass R S' M
inst✝³ : Monoid T'
inst✝² : DistribMulAction T' M
inst✝¹ : SMulCommClass R T' M
inst✝ : SMulCommClass S' T' M
s : S'ᵈᵐᵃ
t : T'ᵈᵐᵃ
f : M →ₛₗ[σ₁₂] M'
m : M
⊢ (s • t • f) m = (t • s • f) m

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : AddMonoid α
inst✝² : DistribMulAction M α
inst✝¹ : DistribMulAction N α
inst✝ : SMulCommClass M N α
mn : M × N
a a' : α
⊢ mn • (a + a') = mn • a + mn • a'

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
x✝ : DistribMulAction (M × N) α
⊢ (fun _insts ↦
        have this := ⋯;
        prodOfSMulCommClass M N α)
      ((fun x ↦ ⟨compHom α (MonoidHom.inl M N), ⟨compHom α (MonoidHom.inr M N), ⋯⟩⟩) x✝) =
    x✝

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring R'
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R M
inst✝⁵ : Module R' M'
σ₁₂ : R →+* R'
inst✝⁴ : Semiring S
inst✝³ : Module S M
inst✝² : Module S M'
inst✝¹ : SMulCommClass R' S M'
inst✝ : SMulCommClass R S M
x✝³ x✝² : Sᵈᵐᵃ
x✝¹ : M →ₛₗ[σ₁₂] M'
x✝ : M
⊢ ((x✝³ + x✝²) • x✝¹) x✝ = (x✝³ • x✝¹ + x✝² • x✝¹) x✝

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring R'
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R M
inst✝⁵ : Module R' M'
σ₁₂ : R →+* R'
inst✝⁴ : Semiring S
inst✝³ : Module S M
inst✝² : Module S M'
inst✝¹ : SMulCommClass R' S M'
inst✝ : SMulCommClass R S M
x✝¹ : M →ₛₗ[σ₁₂] M'
x✝ : M
⊢ (0 • x✝¹) x✝ = 0 x✝

Tactic:
by

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

Goal state before:
pp: R : Type u_6
A : Type u_7
inst✝³ : Semiring R
inst✝² : NonUnitalSemiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a b : A
⊢ mulLeft R (a * b) = mulLeft R a ∘ₗ mulLeft R b

Tactic:
by

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

Goal state before:
pp: R : Type u_6
A : Type u_7
inst✝³ : Semiring R
inst✝² : NonUnitalSemiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a b : A
⊢ mulRight R (a * b) = mulRight R b ∘ₗ mulRight R a

Tactic:
by

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

Goal state before:
pp: R : Type u_6
A : Type u_7
inst✝³ : Semiring R
inst✝² : NonAssocSemiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a b : A
h : mulLeft R a = mulLeft R b
⊢ a = b

Tactic:
by

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

Goal state before:
pp: R : Type u_6
A : Type u_7
inst✝³ : Semiring R
inst✝² : NonAssocSemiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a b : A
h : mulRight R a = mulRight R b
⊢ a = b

Tactic:
by

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

Goal state before:
pp: R✝ : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst✝ : Semiring R
f g : ι → R
⊢ Sum.elim 0 (f + g) = Sum.elim 0 f + Sum.elim 0 g

Tactic:
by

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

Goal state before:
pp: R✝ : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst✝ : Semiring R
t : R
f : ι → R
⊢ Sum.elim 0 (t • f) = (RingHom.id R) t • Sum.elim 0 f

Tactic:
by

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

Goal state before:
pp: R✝ : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst✝ : Semiring R
f g : ι → R
⊢ Sum.elim (f + g) 0 = Sum.elim f 0 + Sum.elim g 0

Tactic:
by

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

Goal state before:
pp: R✝ : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst✝ : Semiring R
t : R
f : ι → R
⊢ Sum.elim (t • f) 0 = (RingHom.id R) t • Sum.elim f 0

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
⊢ Function.RightInverse
    (fun _insts ↦
      have this := ⋯;
      prodOfSMulCommClass M N α)
    fun x ↦ ⟨compHom α (MonoidHom.inl M N), ⟨compHom α (MonoidHom.inr M N), ⋯⟩⟩

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommGroup N₁
inst✝² : Module R M
inst✝¹ : Module R N₁
inst✝ : Nontrivial M
⊢ Nontrivial (End R M)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
h : IsUnit f
x : M
⊢ (h.unit.inv * f) x = x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
m : M
k l : ℕ
hk : k ≤ l
hm : (f ^ k) m = 0
⊢ (f ^ l) m = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
g : End R M
g₂ : End R₂ M₂
h : g₂ ∘ₛₗ f = f ∘ₛₗ g
k : ℕ
⊢ (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ k)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : End R M
n : ℕ
⊢ f' ^ (n + 1) = (f' ^ n) ∘ₗ f'

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : End R M
n : ℕ
⊢ f' ^ (n + 1) = f' ∘ₗ f' ^ n

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : End R M
h : Surjective ⇑f'
n : ℕ
⊢ Surjective ⇑(f' ^ (n + 1))

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : End R M
h : Injective ⇑f'
n : ℕ
⊢ Injective ⇑(f' ^ (n + 1))

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : End R M
h : Bijective ⇑f'
n : ℕ
⊢ Bijective ⇑(f' ^ (n + 1))

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : End R M
n : ℕ
hn : n ≠ 0
h : Injective ⇑(f' ^ n)
⊢ Injective ⇑f'

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : End R M
n : ℕ
hn : n ≠ 0
h : Surjective ⇑(f' ^ n)
⊢ Surjective ⇑f'

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R M
inst✝³ : Module R N₁
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass R S M
f' : End R M
α : R
hα : α ∈ Set.center R
β : R
x✝ : M
⊢ α • β • x✝ = (RingHom.id R) β • α • x✝

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
f : M₁ →ₗ[R] S
x✝ : M
x y : M₁
⊢ f (x + y) • x✝ = f x • x✝ + f y • x✝

Tactic:
by

Goal state after: