mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : SMul M α
inst✝⁴ : SMul M β
inst✝³ : SMul N α
inst✝² : SMul N β
a : M
x : α × β
inst✝¹ : SMulCommClass M N α
inst✝ : SMulCommClass M N β
x✝² : M
x✝¹ : N
x✝ : α × β
⊢ x✝² • x✝¹ • x✝ = x✝¹ • x✝² • x✝

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : SMul M α
inst✝⁴ : SMul M β
inst✝³ : SMul N α
inst✝² : SMul N β
a✝ : M
x : α × β
inst✝¹ : FaithfulSMul M α
inst✝ : Nonempty β
m₁✝ m₂✝ : M
h : ∀ (a : α × β), m₁✝ • a = m₂✝ • a
b : β
a : α
⊢ m₁✝ • a = m₂✝ • a

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : SMul M α
inst✝⁴ : SMul M β
inst✝³ : SMul N α
inst✝² : SMul N β
a✝ : M
x : α × β
inst✝¹ : Nonempty α
inst✝ : FaithfulSMul M β
m₁✝ m₂✝ : M
h : ∀ (a : α × β), m₁✝ • a = m₂✝ • a
a : α
b : β
⊢ m₁✝ • b = m₂✝ • b

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Mul N
inst✝⁴ : Mul P
inst✝³ : SMul M N
inst✝² : SMul M P
inst✝¹ : SMulCommClass M N N
inst✝ : SMulCommClass M P P
c : M
x y : N × P
⊢ c • x • y = x • c • y

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Mul N
inst✝⁴ : Mul P
inst✝³ : SMul M N
inst✝² : SMul M P
inst✝¹ : IsScalarTower M N N
inst✝ : IsScalarTower M P P
c : M
x y : N × P
⊢ (c • x) • y = c • x • y

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : MulAction M β
x✝² x✝¹ : M
x✝ : α × β
⊢ (x✝² * x✝¹) • x✝ = x✝² • x✝¹ • x✝

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : MulAction M β
x✝ : α × β
⊢ 1 • x✝ = x✝

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
P Q : Algebra R A
h : ∀ (r : R), (algebraMap R A) r = (algebraMap R A) r
⊢ P = Q

Tactic:
by

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

Goal state before:
pp: R✝ : Type u
S : Type v
A✝ : Type w
B : Type u_1
inst✝⁶ : CommSemiring R✝
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
inst✝² : Semiring B
inst✝¹ : Algebra R✝ B
R : Type ?u.22
A : Type ?u.24
x✝¹ : CommSemiring R
x✝ : Semiring A
inst✝ : Algebra R A
⊢ ∀ (x y : R) (b : A), (x * y) • b = x • y • b

Tactic:
by

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

Goal state before:
pp: R✝ : Type u
S : Type v
A✝ : Type w
B : Type u_1
inst✝⁶ : CommSemiring R✝
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
inst✝² : Semiring B
inst✝¹ : Algebra R✝ B
R : Type ?u.22
A : Type ?u.24
x✝² : CommSemiring R
x✝¹ : Semiring A
inst✝ : Algebra R A
x✝ : A
⊢ 1 • x✝ = x✝

Tactic:
by

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

Goal state before:
pp: R✝ : Type u
S : Type v
A✝ : Type w
B : Type u_1
inst✝⁶ : CommSemiring R✝
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
inst✝² : Semiring B
inst✝¹ : Algebra R✝ B
R : Type ?u.22
A : Type ?u.24
x✝¹ : CommSemiring R
x✝ : Semiring A
inst✝ : Algebra R A
⊢ ∀ (a : R), a • 0 = 0

Tactic:
by

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

Goal state before:
pp: R✝ : Type u
S : Type v
A✝ : Type w
B : Type u_1
inst✝⁶ : CommSemiring R✝
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
inst✝² : Semiring B
inst✝¹ : Algebra R✝ B
R : Type ?u.22
A : Type ?u.24
x✝¹ : CommSemiring R
x✝ : Semiring A
inst✝ : Algebra R A
⊢ ∀ (a : R) (x y : A), a • (x + y) = a • x + a • y

Tactic:
by

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

Goal state before:
pp: R✝ : Type u
S : Type v
A✝ : Type w
B : Type u_1
inst✝⁶ : CommSemiring R✝
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
inst✝² : Semiring B
inst✝¹ : Algebra R✝ B
R : Type ?u.22
A : Type ?u.24
x✝¹ : CommSemiring R
x✝ : Semiring A
inst✝ : Algebra R A
⊢ ∀ (r s : R) (x : A), (r + s) • x = r • x + s • x

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : MulAction M α
inst✝¹ : MulAction N α
inst✝ : SMulCommClass M N α
x y : M × N
a : α
⊢ (x * y) • a = x • y • a

Tactic:
by

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

Goal state before:
pp: R✝ : Type u
S : Type v
A✝ : Type w
B : Type u_1
inst✝⁶ : CommSemiring R✝
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
inst✝² : Semiring B
inst✝¹ : Algebra R✝ B
R : Type ?u.22
A : Type ?u.24
x✝¹ : CommSemiring R
x✝ : Semiring A
inst✝ : Algebra R A
⊢ ∀ (x : A), 0 • x = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
r : R
y : A
⊢ x * ((algebraMap R A) r * y) = (algebraMap R A) r * (x * y)

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
x✝ : MulAction (M × N) α
instM : MulAction M α := compHom α (MonoidHom.inl M N)
instN : MulAction N α := compHom α (MonoidHom.inr M N)
m : M
n : N
a : α
⊢ m • n • a = n • m • a

Tactic:
by

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

Goal state before:
pp: R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
r : R
y : A
⊢ x * (algebraMap R A) r * y = x * y * (algebraMap R A) r

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : R
y z : A
⊢ (x • y) • z = x • y • z

Tactic:
by

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

Goal state before:
pp: R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : R
x y : A
⊢ x * s • y = s • (x * y)

Tactic:
by

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

Goal state before:
pp: R : Type u
A : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
α : Type u_2
inst✝² : Monoid α
inst✝¹ : MulDistribMulAction α A
inst✝ : SMulCommClass α R A
a : α
r : R
⊢ a • (algebraMap R A) r = (algebraMap R A) r

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x y : R
⊢ (↑↑(algebraMap R A)).toFun (x • y) = (RingHom.id R) x • (↑↑(algebraMap R A)).toFun y

Tactic:
by

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

Goal state before:
pp: A : Type u_1
B : Type u_2
a : A
b : B
C : Type u_3
inst✝⁵ : SMul A B
inst✝⁴ : CommSemiring B
inst✝³ : Semiring C
inst✝² : Algebra B C
inst✝¹ : SMul A C
inst✝ : IsScalarTower A B C
⊢ ↑(a • b) = a • ↑b

Tactic:
by

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

Goal state before:
pp: A : Type u_1
B : Type u_2
a : A
b : B
C : Type u_3
inst✝⁶ : SMul A B
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra B C
inst✝² : Monoid A
inst✝¹ : MulDistribMulAction A C
inst✝ : SMulDistribClass A B C
⊢ ↑(a • b) = a • ↑b

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ Function.LeftInverse
    (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.GroupWithZero.Prod

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝¹ : MulZeroClass M₀
inst✝ : MulZeroClass N₀
⊢ ∀ (a : M₀ × N₀), 0 * a = 0

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝¹ : MulZeroClass M₀
inst✝ : MulZeroClass N₀
⊢ ∀ (a : M₀ × N₀), a * 0 = 0

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝¹ : SemigroupWithZero M₀
inst✝ : SemigroupWithZero N₀
⊢ ∀ (a : M₀ × N₀), 0 * a = 0

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝¹ : SemigroupWithZero M₀
inst✝ : SemigroupWithZero N₀
⊢ ∀ (a : M₀ × N₀), a * 0 = 0

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝¹ : MulZeroOneClass M₀
inst✝ : MulZeroOneClass N₀
⊢ ∀ (a : M₀ × N₀), 0 * a = 0

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝¹ : MulZeroOneClass M₀
inst✝ : MulZeroOneClass N₀
⊢ ∀ (a : M₀ × N₀), a * 0 = 0

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝¹ : MonoidWithZero M₀
inst✝ : MonoidWithZero N₀
⊢ ∀ (a : M₀ × N₀), 0 * a = 0

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝¹ : MonoidWithZero M₀
inst✝ : MonoidWithZero N₀
⊢ ∀ (a : M₀ × N₀), a * 0 = 0

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝¹ : CommMonoidWithZero M₀
inst✝ : CommMonoidWithZero N₀
⊢ ∀ (a : M₀ × N₀), 0 * a = 0

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝¹ : CommMonoidWithZero M₀
inst✝ : CommMonoidWithZero N₀
⊢ ∀ (a : M₀ × N₀), a * 0 = 0

Tactic:
by

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

Goal state before:
pp: G : Type u_1
R : Type u_7
inst✝⁵ : Group G
inst✝⁴ : Monoid R
inst✝³ : AddGroup R
inst✝² : DistribMulAction G R
inst✝¹ : IsScalarTower G R R
inst✝ : SMulCommClass G R R
r : G
a : R
⊢ IsUnit (r • 1 - a) ↔ IsUnit (1 - r⁻¹ • a)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
G₀ : Type u_2
inst✝⁴ : Group G
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G G₀
inst✝¹ : IsScalarTower G G₀ G₀
inst✝ : SMulCommClass G G₀ G₀
g h : G
a b : G₀
x : G
⊢ x • 0 = 0

Tactic:
by

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

Goal state before:
pp: G : Type u_1
G₀ : Type u_2
inst✝⁴ : Group G
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G G₀
inst✝¹ : IsScalarTower G G₀ G₀
inst✝ : SMulCommClass G G₀ G₀
g h : G
a b : G₀
this : ∀ (x : G), x • 0 = 0
hb : ¬b = 0
⊢ h • b ≠ 0

Tactic:
by

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

Goal state before:
pp: G : Type u_1
G₀ : Type u_2
inst✝⁴ : Group G
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G G₀
inst✝¹ : IsScalarTower G G₀ G₀
inst✝ : SMulCommClass G G₀ G₀
g h : G
a b : G₀
⊢ (g / h) • (a / b) = g • a / h • b

Tactic:
by

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

Goal state before:
pp: G : Type u_1
G₀ : Type u_2
inst✝² : Group G
inst✝¹ : GroupWithZero G₀
inst✝ : MulDistribMulAction G G₀
g : G
x : G₀
n : ℤ
⊢ g • x ^ n = (g • x) ^ n

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ 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.GroupWithZero.Action.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝³ : Zero A
inst✝² : Zero B
inst✝¹ : Zero C
inst✝ : SMulZeroClass M B
r : M
f : ZeroHom A B
⊢ r • f 0 = 0

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝³ : AddZeroClass A
inst✝² : AddZeroClass B
inst✝¹ : AddZeroClass C
inst✝ : DistribSMul M B
r : M
f : A →+ B
⊢ r • f 0 = 0

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝³ : AddZeroClass A
inst✝² : AddZeroClass B
inst✝¹ : AddZeroClass C
inst✝ : DistribSMul M B
r : M
f : A →+ B
x✝¹ x✝ : A
⊢ r • f (x✝¹ + x✝) = r • f x✝¹ + r • f x✝

Tactic:
by

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

Goal state before:
pp: M : Type uM
inst✝ : AddCommGroup M
⊢ instRing.toAddCommGroup.toSubNegMonoid = instRing.toAddGroupWithOne.toAddGroup.toSubNegMonoid

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r✝ s : R
x r : M
⊢ ((↑(DistribMulAction.toAddMonoidEnd R M)).toFun 0) r = 0 r

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r✝ s : R
x✝ : M
x y : R
r : M
⊢ ((↑(DistribMulAction.toAddMonoidEnd R M)).toFun (x + y)) r =
    ((↑(DistribMulAction.toAddMonoidEnd R M)).toFun x + (↑(DistribMulAction.toAddMonoidEnd R M)).toFun y) r

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.DomAct.Basic

Goal state before:
pp: M : Type u_1
β : Type u_2
α : Type u_3
N : Type u_4
inst✝² : SMul M α
inst✝¹ : FaithfulSMul M α
inst✝ : Nontrivial β
c₁ c₂ : Mᵈᵐᵃ
h : ∀ (a : α → β), c₁ • a = c₂ • a
a : α
⊢ mk.symm c₁ • a = mk.symm c₂ • a

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_6
M : Type u_7
M₂ : Type u_9
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
module_M : Module R M
module_S_M₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
re₁ : RingHomInvPair σ σ'
re₂ : RingHomInvPair σ' σ
e : M ≃ₛₗ[σ] M₂
⊢ (↑e).toFun = ⇑e

Tactic:
by

Goal state after:
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
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : Semiring R₁
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring R₃
inst✝⁷ : Semiring R₄
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : AddCommMonoid M₄
inst✝¹ : AddCommMonoid N₁
inst✝ : AddCommMonoid N₂
module_M : Module R M
module_S_M₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
re₁ : RingHomInvPair σ σ'
re₂ : RingHomInvPair σ' σ
e✝ e' e : M ≃ₛₗ[σ] M₂
r : S
x : M₂
⊢ ((↑e).inverse e.invFun ⋯ ⋯) (r • x) = σ' r • ((↑e).inverse e.invFun ⋯ ⋯) x

Tactic:
by

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

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ →ₛₗ[σ₃₂] M₂
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
⊢ ↑e₁₂ ∘ₛₗ ↑e₁₂.symm ∘ₛₗ f = f

Tactic:
by

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

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ →ₛₗ[σ₃₁] M₁
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
⊢ ↑e₁₂.symm ∘ₛₗ ↑e₁₂ ∘ₛₗ f = f

Tactic:
by

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

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
⊢ f = g ∘ₛₗ ↑e₁₂.symm ↔ f ∘ₛₗ ↑e₁₂ = g

Tactic:
by

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

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
⊢ g ∘ₛₗ ↑e₁₂.symm = f ↔ g = f ∘ₛₗ ↑e₁₂

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
M✝ : Type u_3
A : Type u_4
B : Type u_5
S : Type u_6
M : Type u_7
M₂ : Type u_8
inst✝³ : Semiring S
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module S M
s s' : Sᵈᵐᵃ
f : M →+ M₂
m : M
⊢ ((s + s') • f) m = (s • f + s' • f) m

Tactic:
by

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

Goal state before:
pp: R : Type u_14
M : Type u_15
M₂ : Type u_16
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R M₂
F : Type u_17
inst✝¹ : FunLike F M M₂
inst✝ : LinearMapClass F R M M₂
f : F
r : R
x : M
⊢ f (r • x) = r • f x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
M✝ : Type u_3
A : Type u_4
B : Type u_5
S : Type u_6
M : Type u_7
M₂ : Type u_8
inst✝³ : Semiring S
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module S M
x✝¹ : M →+ M₂
x✝ : M
⊢ (0 • x✝¹) x✝ = 0 x✝

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → MulZeroClass (α i)
inst✝ : DecidableEq ι
i : ι
f : (i : ι) → α i
⊢ ∀ (a : (i : ι) → α i), 0 * a = 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → MulZeroClass (α i)
inst✝ : DecidableEq ι
i : ι
f : (i : ι) → α i
⊢ ∀ (a : (i : ι) → α i), a * 0 = 0

Tactic:
by

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

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f : M₃ →ₛₗ[σ₃₁] M₁
g : M₃ →ₛₗ[σ₃₂] M₂
⊢ f = ↑e₁₂.symm ∘ₛₗ g ↔ ↑e₁₂ ∘ₛₗ 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
F : Type u_14
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module R M₂
inst✝² : Module S M₃
σ : R →+* S
inst✝¹ : FunLike F M M₃
inst✝ : SemilinearMapClass F σ M M₃
f : F
c : R
x : M
⊢ f (c • x) = σ c • f x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_5
M : Type u_8
M₃ : Type u_11
F : Type u_14
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module S M₃
σ : R →+* S
f : F
inst✝² : FunLike F M M₃
inst✝¹ : SemilinearMapClass F σ M M₃
σ' : S →+* R
inst✝ : RingHomInvPair σ σ'
c : S
x : M
⊢ c • f x = f (σ' c • 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 S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module S M₃
σ : R →+* S
f g : M →ₛₗ[σ] M₃
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_5
M : Type u_8
M₃ : Type u_11
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module S M₃
σ : R →+* S
F : Type u_14
inst✝¹ : FunLike F M M₃
inst✝ : SemilinearMapClass F σ M M₃
f g : F
h : ↑f = ↑g
⊢ 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 S
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ✝ : R →+* S
σ : R →+* R
inst✝ : RingHomId σ
r : R
x : M
⊢ r • x = σ r • x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_5
M : Type u_8
M₃ : Type u_11
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module S M₃
σ : R →+* S
f : M →ₛₗ[σ] M₃
σ' : S →+* R
inst✝ : RingHomInvPair σ σ'
c : S
x : M
⊢ c • f x = f (σ' c • x)

Tactic:
by

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

Goal state before:
pp: I : Type u
f : I → Type v
g : I → Type u_1
n : (i : I) → Zero (g i)
inst✝ : (i : I) → SMulZeroClass (f i) (g i)
⊢ ∀ (a : (i : I) → f i), a • 0 = 0

Tactic:
by

Goal state after: