mathlib-initiative/mathlib-tactics huggingface dataset:
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), 0 (x + y) = 0 x + 0 y

Tactic:
simp

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

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
M₁ : Type u_8
M₂ : Type u_9
inst✝³ : Semiring R₁
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₁
inst✝ : AddCommMonoid M₂
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
f : M₁ ≃ₛₗ[σ₁₂] M₂
x : M₁
⊢ (f.trans f.symm) x = (refl R₁ M₁) x

Tactic:
simp

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 σ₁₂ σ₂₃ σ₁₃
⊢ ∀ (m : R₁) (x : M), 0 (m • x) = σ₁₂ m • 0 x

Tactic:
simp

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

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
M₁ : Type u_8
M₂ : Type u_9
inst✝³ : Semiring R₁
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₁
inst✝ : AddCommMonoid M₂
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
f : M₁ ≃ₛₗ[σ₁₂] M₂
x : M₂
⊢ (f.symm.trans f) x = (refl R₂ M₂) x

Tactic:
simp

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
x✝ : G
⊢ (e ≪≫ₗ (α • f)) x✝ = (α • e ≪≫ₗ f) x✝

Tactic:
simp

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

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

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

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

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

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
a : A
⊢ f a = g a

Tactic:
exact MulActionHom.congr_fun h a

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

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

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

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

Goal state before:
pp: case inl
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
i : κ
⊢ Sum.elim 0 (f + g) (inl i) = (Sum.elim 0 f + Sum.elim 0 g) (inl i)

Tactic:
simp

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

Goal state before:
pp: case inr
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
i : ι
⊢ Sum.elim 0 (f + g) (inr i) = (Sum.elim 0 f + Sum.elim 0 g) (inr i)

Tactic:
simp

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

Goal state before:
pp: case inl
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
i : κ
⊢ Sum.elim 0 (t • f) (inl i) = ((RingHom.id R) t • Sum.elim 0 f) (inl i)

Tactic:
simp

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

Goal state before:
pp: case inr
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
i : ι
⊢ Sum.elim 0 (t • f) (inr i) = ((RingHom.id R) t • Sum.elim 0 f) (inr i)

Tactic:
simp

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

Goal state before:
pp: case inl
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
i : ι
⊢ Sum.elim (f + g) 0 (inl i) = (Sum.elim f 0 + Sum.elim g 0) (inl i)

Tactic:
simp

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

Goal state before:
pp: case inr
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
i : κ
⊢ Sum.elim (f + g) 0 (inr i) = (Sum.elim f 0 + Sum.elim g 0) (inr i)

Tactic:
simp

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

Goal state before:
pp: case inl
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
i : ι
⊢ Sum.elim (t • f) 0 (inl i) = ((RingHom.id R) t • Sum.elim f 0) (inl i)

Tactic:
simp

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

Goal state before:
pp: case inr
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
i : κ
⊢ Sum.elim (t • f) 0 (inr i) = ((RingHom.id R) t • Sum.elim f 0) (inr i)

Tactic:
simp

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
⊢ (f * h.unit.inv) x = x

Tactic:
simp

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

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

Goal state before:
pp: R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
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₁
⊢ (f.smulRight 0) x✝ = 0 x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
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
x : M
x✝ : M₁
⊢ (smulRight 0 x) x✝ = 0 x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_9
M : Type u_10
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
x✝ : M
⊢ (LinearMap.id * f) x✝ = (f * LinearMap.id) x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_9
M : Type u_10
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
x✝ : M
⊢ (f * LinearMap.id) x✝ = (LinearMap.id * f) x✝

Tactic:
simp

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

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
inst✝ : Module.IsTorsionFree R M
⊢ ∀ (r : R) (m : ↥p), ↑(r • m) = r • ↑m

Tactic:
simp

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

Goal state before:
pp: ⊢ ∀ {a : PUnit}, a ≠ 0 → IsLeftRegular a

Tactic:
simp

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

Goal state before:
pp: ⊢ ∀ {a : PUnit}, a ≠ 0 → IsRightRegular a

Tactic:
simp

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

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
inst✝³ : Semiring S
inst✝² : SMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
a : S
⊢ ↑(a • 0) = ↑0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : SMul R S
⊢ ∀ (m : PUnit) (n : R) (a : S), m • n • a = n • m • a

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : SMul R S
⊢ ∀ (x : PUnit) (y : R) (z : S), (x • y) • z = x • y • z

Tactic:
simp

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

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
inst✝³ : Semiring S
inst✝² : SMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
a : ↥p
⊢ ↑(0 • a) = ↑0

Tactic:
simp

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

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Semiring S
inst✝⁶ : Module R M
inst✝⁵ : SMul S R
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : SetLike T M
inst✝¹ : AddSubmonoidClass T M
inst✝ : SMulMemClass T R M
t : T
x✝ : ↥t
⊢ ↑(1 • x✝) = ↑x✝

Tactic:
simp

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

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Semiring S
inst✝⁶ : Module R M
inst✝⁵ : SMul S R
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : SetLike T M
inst✝¹ : AddSubmonoidClass T M
inst✝ : SMulMemClass T R M
t : T
x✝ : S
⊢ ↑(x✝ • 0) = ↑0

Tactic:
simp

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

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Semiring S
inst✝⁶ : Module R M
inst✝⁵ : SMul S R
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : SetLike T M
inst✝¹ : AddSubmonoidClass T M
inst✝ : SMulMemClass T R M
t : T
x✝ : ↥t
⊢ ↑(0 • x✝) = ↑0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Lattice

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✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p q : Submodule R M
⊢ ∀ (c : R) {x : M}, x ∈ {0} → c • x ∈ {0}

Tactic:
simp

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

Goal state before:
pp: S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
⊢ ∀ (c : R) {x : M}, x ∈ ∅ → c • x ∈ ∅

Tactic:
simp

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

Goal state before:
pp: S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
⊢ ∀ (c : R) {x : M}, x ∈ Set.univ → c • x ∈ Set.univ

Tactic:
simp

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

Goal state before:
pp: R : Type u
M : Type v
inst✝ : SMul R M
ι : Sort u_1
p : ι → SubMulAction R M
x : M
⊢ x ∈ ⋃ s ∈ Set.range p, ↑s ↔ ∃ i, x ∈ p i

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
s : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
⊢ ↑(∅.inf p) = ⋂ i ∈ ∅, ↑(p i)

Tactic:
simp

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

Goal state before:
pp: R : Type u
M : Type v
inst✝ : SMul R M
ι : Sort u_1
p : ι → SubMulAction R M
x : M
⊢ x ∈ ⋂ s ∈ Set.range p, ↑s ↔ ∀ (i : ι), x ∈ p i

Tactic:
simp

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

Goal state before:
pp: S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
p : SubMulAction R M
r : R
x : M
⊢ ∀ (m : R) (x : ↥p), ↑(m • x) = id m • ↑x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
s✝ : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
i : ι
s : Finset ι
x✝ : i ∉ s
ih : ↑(s.inf p) = ⋂ i ∈ s, ↑(p i)
⊢ ↑(p i) ∩ ⋂ i ∈ s, ↑(p i) = ⋂ i_1 ∈ insert i s, ↑(p i_1)

Tactic:
simp

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

Goal state before:
pp: S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝¹ : Group R
inst✝ : MulAction R M
s : SubMulAction R M
⊢ ∀ (c : R) {x : M}, x ∈ (↑s)ᶜ → c • x ∈ (↑s)ᶜ

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
y : { v // v ≠ 0 }
a : Rˣ
⊢ (fun m ↦ m • ↑y) a = ↑((fun m ↦ m • y) a)

Tactic:
simp

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

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝¹ : Semiring R
inst✝ : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
⊢ ∀ (x y : ↥p), ↑(x + y) = ↑x + ↑y

Tactic:
simp

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

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝¹ : Semiring R
inst✝ : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
⊢ ∀ (m : R) (x : ↥p), ↑(m • x) = (RingHom.id R) m • ↑x

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
ι : Type u_9
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module R M₁
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f✝ : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
p : Submodule R₂ M₂
f : M →ₛₗ[σ₁₂] M₂
h : ∀ (c : M), f c ∈ p
x✝¹ x✝ : M
⊢ ⟨f (x✝¹ + x✝), ⋯⟩ = ⟨f x✝¹, ⋯⟩ + ⟨f x✝, ⋯⟩

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : M → Type u_9
inst✝² : CommSemiring R
inst✝¹ : (x : M) → AddCommMonoid (V x)
inst✝ : (x : M) → Module R (V x)
e : (x : M) → V x →ₗ[R] R
x✝¹ y✝ : (x : M) → V x
x✝ : M
⊢ (e x✝) ((x✝¹ + y✝) x✝) = ((fun x ↦ (e x) (x✝¹ x)) + fun x ↦ (e x) (y✝ x)) x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
ι : Type u_9
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module R M₁
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f✝ : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
p : Submodule R₂ M₂
f : M →ₛₗ[σ₁₂] M₂
h : ∀ (c : M), f c ∈ p
x✝¹ : R
x✝ : M
⊢ ⟨f (x✝¹ • x✝), ⋯⟩ = σ₁₂ x✝¹ • ⟨f x✝, ⋯⟩

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : M → Type u_9
inst✝² : CommSemiring R
inst✝¹ : (x : M) → AddCommMonoid (V x)
inst✝ : (x : M) → Module R (V x)
e : (x : M) → V x →ₗ[R] R
m✝ : R
x✝¹ : (x : M) → V x
x✝ : M
⊢ (e x✝) ((m✝ • x✝¹) x✝) = ((RingHom.id R) m✝ • fun x ↦ (e x) (x✝¹ x)) x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : M → Type u_9
inst✝² : CommSemiring R
inst✝¹ : (x : M) → AddCommMonoid (V x)
inst✝ : (x : M) → Module R (V x)
x✝² y✝ : (x : M) → V x →ₗ[R] R
x✝¹ : (x : M) → V x
x✝ : M
⊢ { toFun := fun s x ↦ ((x✝² + y✝) x) (s x), map_add' := ⋯, map_smul' := ⋯ } x✝¹ x✝ =
    ({ toFun := fun s x ↦ (x✝² x) (s x), map_add' := ⋯, map_smul' := ⋯ } +
        { toFun := fun s x ↦ (y✝ x) (s x), map_add' := ⋯, map_smul' := ⋯ })
      x✝¹ x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : M → Type u_9
inst✝² : CommSemiring R
inst✝¹ : (x : M) → AddCommMonoid (V x)
inst✝ : (x : M) → Module R (V x)
m✝ : R
x✝² : (x : M) → V x →ₗ[R] R
x✝¹ : (x : M) → V x
x✝ : M
⊢ { toFun := fun s x ↦ ((m✝ • x✝²) x) (s x), map_add' := ⋯, map_smul' := ⋯ } x✝¹ x✝ =
    ((RingHom.id R) m✝ • { toFun := fun s x ↦ (x✝² x) (s x), map_add' := ⋯, map_smul' := ⋯ }) x✝¹ x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
x : M
⊢ (fun f ↦ f 1) (smulRight 1 x) = x

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
⊢ (neg R) x = -x

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
M₂' : Type u_10
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
p : M₂' →ₗ[R₂] M₂
hp : Injective ⇑p
h : ∀ (c : M), f c ∈ range ⇑p
⊢ p ∘ₛₗ f.codLift p hp h = f

Tactic:
ext x
  rw [comp_apply, codLift_apply, (h x).choose_spec]

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

Goal state before:
pp: R : Type u_10
R₂ : Type u_11
M : Type u_12
M₂ : Type u_13
inst✝⁵ : Ring R
inst✝⁴ : Ring R₂
σ₁₂ : R →+* R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
p : Submodule R M
q : Submodule R₂ M₂
f g : M →ₛₗ[σ₁₂] M₂
hf : MapsTo ⇑f ↑p ↑q
hg : MapsTo ⇑g ↑p ↑q
hfg : MapsTo ⇑(f - g) ↑p ↑q
x✝ : ↥p
⊢ ↑((f.restrict hf - g.restrict hg) x✝) = ↑(((f - g).restrict hfg) x✝)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
R₂✝ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁✝ : Type u_6
M₂✝ : Type u_7
M₃ : Type u_8
R₁ : Type u_9
R₂ : Type u_10
R₁' : Type u_11
R₂' : Type u_12
M₁ : Type u_13
M₂ : Type u_14
M₁' : Type u_15
M₂' : Type u_16
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✝¹⁵ : Module R₁ M₁
inst✝¹⁴ : Module R₂ M₂
inst✝¹³ : Module R₁' M₁'
inst✝¹² : Module R₂' M₂'
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁'₂' : R₁' →+* R₂'
σ₂'₁' : R₂' →+* R₁'
σ₁₁' : R₁ →+* R₁'
σ₂₂' : R₂ →+* R₂'
σ₂₁' : R₂ →+* R₁'
σ₁₂' : R₁ →+* R₂'
inst✝¹¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹⁰ : RingHomInvPair σ₂₁ σ₁₂
inst✝⁹ : RingHomInvPair σ₁'₂' σ₂'₁'
inst✝⁸ : RingHomInvPair σ₂'₁' σ₁'₂'
inst✝⁷ : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'
inst✝⁶ : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'
inst✝⁵ : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'
inst✝⁴ : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'
inst✝³ : Semiring S
inst✝² : Module S M₁
inst✝¹ : SMulCommClass R₁ S M₁
inst✝ : RingHomCompTriple σ₁₂' σ₂'₁' σ₁₁'
e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂'
x✝² : S
x✝¹ : M₁ →ₛₗ[σ₁₁'] M₁'
x✝ : M₁
⊢ (((refl R₁ M₁).arrowCongrAddEquiv e₂).toFun (DomMulAct.mk x✝² • x✝¹)) x✝ =
    ((RingHom.id Sᵈᵐᵃ) (DomMulAct.mk x✝²) • ((refl R₁ M₁).arrowCongrAddEquiv e₂).toFun x✝¹) x✝

Tactic:
simp

Goal state after: