mathlib-initiative/mathlib-tactics huggingface dataset:
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✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f✝ : M →ₗ[R] M₂
f : M₂ →ₗ[R] R
c : R
m : M
⊢ f.smulRight (c • m) = (RingHom.id R) c • f.smulRight m

Tactic:
ext

Goal state after:
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✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f✝ : M →ₗ[R] M₂
f : M₂ →ₗ[R] R
c : R
m : M
x✝ : M₂
⊢ (f.smulRight (c • m)) x✝ = ((RingHom.id R) c • f.smulRight m) x✝
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✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f✝ : M →ₗ[R] M₂
f f' : M₂ →ₗ[R] R
⊢ { toFun := (f + f').smulRight, map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := f.smulRight, map_add' := ⋯, map_smul' := ⋯ } + { toFun := f'.smulRight, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext

Goal state after:
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✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f✝ : M →ₗ[R] M₂
f f' : M₂ →ₗ[R] R
x✝¹ : M
x✝ : M₂
⊢ ({ toFun := (f + f').smulRight, map_add' := ⋯, map_smul' := ⋯ } x✝¹) x✝ =
    (({ toFun := f.smulRight, map_add' := ⋯, map_smul' := ⋯ } +
          { toFun := f'.smulRight, map_add' := ⋯, map_smul' := ⋯ })
        x✝¹)
      x✝
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✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f✝ : M →ₗ[R] M₂
c : R
f : M₂ →ₗ[R] R
⊢ { toFun := (c • f).smulRight, map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id R) c • { toFun := f.smulRight, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext

Goal state after:
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✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f✝ : M →ₗ[R] M₂
c : R
f : M₂ →ₗ[R] R
x✝¹ : M
x✝ : M₂
⊢ ({ toFun := (c • f).smulRight, map_add' := ⋯, map_smul' := ⋯ } x✝¹) x✝ =
    (((RingHom.id R) c • { toFun := f.smulRight, map_add' := ⋯, map_smul' := ⋯ }) x✝¹) x✝
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
⊢ Commute LinearMap.id f

Tactic:
ext

Goal state after:
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✝
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
⊢ Commute f LinearMap.id

Tactic:
ext

Goal state after:
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✝
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
inst✝ : Module R M
p✝ q p : Submodule R M
s : Set M
hs : s = ↑p
⊢ ∀ (c : R) {x : M}, x ∈ s → c • x ∈ s

Tactic:
simpa [hs] using p.smul_mem'

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

Goal state after:
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
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
x y : ↥p
⊢ a • (x + y) = a • x + a • y

Tactic:
ext

Goal state after:
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
x y : ↥p
⊢ ↑(a • (x + y)) = ↑(a • x + a • y)
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 b : S
x : ↥p
⊢ (a + b) • x = a • x + b • x

Tactic:
ext

Goal state after:
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 b : S
x : ↥p
⊢ ↑((a + b) • x) = ↑(a • x + b • x)
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:
ext

Goal state after:
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
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✝² x✝¹ : S
x✝ : ↥t
⊢ (x✝² * x✝¹) • x✝ = x✝² • x✝¹ • x✝

Tactic:
ext

Goal state after:
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✝² x✝¹ : S
x✝ : ↥t
⊢ ↑((x✝² * x✝¹) • x✝) = ↑(x✝² • x✝¹ • x✝)
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:
ext

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

Goal state after:
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
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✝¹ x✝ : ↥t
⊢ x✝² • (x✝¹ + x✝) = x✝² • x✝¹ + x✝² • x✝

Tactic:
ext

Goal state after:
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✝¹ x✝ : ↥t
⊢ ↑(x✝² • (x✝¹ + x✝)) = ↑(x✝² • x✝¹ + x✝² • x✝)
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✝² x✝¹ : S
x✝ : ↥t
⊢ (x✝² + x✝¹) • x✝ = x✝² • x✝ + x✝¹ • x✝

Tactic:
ext

Goal state after:
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✝² x✝¹ : S
x✝ : ↥t
⊢ ↑((x✝² + x✝¹) • x✝) = ↑(x✝² • x✝ + x✝¹ • x✝)
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:
ext

Goal state after:
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
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: R : Type u
M : Type v
inst✝¹ : Monoid R
inst✝ : MulAction R M
p : SubMulAction R M
m : ↥p
⊢ MulAction.stabilizerSubmonoid R m = MulAction.stabilizerSubmonoid R ↑m

Tactic:
ext

Goal state after:
R : Type u
M : Type v
inst✝¹ : Monoid R
inst✝ : MulAction R M
p : SubMulAction R M
m : ↥p
x✝ : R
⊢ x✝ ∈ MulAction.stabilizerSubmonoid R m ↔ x✝ ∈ MulAction.stabilizerSubmonoid R ↑m
Module: Mathlib.Algebra.Module.Equiv.Basic

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton M
⊢ ofSubsingleton M M = refl R M

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton M
x✝ : M
⊢ (ofSubsingleton M M) x✝ = (refl R M) x✝
Module: Mathlib.Algebra.Module.Equiv.Basic

Goal state before:
pp: M : Type u_5
M₂ : Type u_7
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup M₂
modM : Module ℤ M
modM₂ : Module ℤ M₂
e : M ≃+ M₂
⊢ ↑e.toIntLinearEquiv = e

Tactic:
ext

Goal state after:
M : Type u_5
M₂ : Type u_7
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup M₂
modM : Module ℤ M
modM₂ : Module ℤ M₂
e : M ≃+ M₂
x✝ : M
⊢ ↑e.toIntLinearEquiv x✝ = e x✝
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
x y : { v // v ≠ 0 }
a : Rˣ
ha : (fun m ↦ m • ↑y) a = ↑x
⊢ (fun m ↦ m • y) a = x

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
x y : { v // v ≠ 0 }
a : Rˣ
ha : (fun m ↦ m • ↑y) a = ↑x
⊢ ↑((fun m ↦ m • y) a) = ↑x
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
⊢ (fun x ↦ (e x) ((x✝ + y✝) x)) = (fun x ↦ (e x) (x✝ x)) + fun x ↦ (e x) (y✝ x)

Tactic:
ext

Goal state after:
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✝
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
⊢ (fun x ↦ (e x) ((m✝ • x✝) x)) = (RingHom.id R) m✝ • fun x ↦ (e x) (x✝ x)

Tactic:
ext

Goal state after:
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✝
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
⊢ { toFun := fun s x ↦ ((x✝ + y✝) x) (s x), map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := fun s x ↦ (x✝ x) (s x), map_add' := ⋯, map_smul' := ⋯ } +
      { toFun := fun s x ↦ (y✝ x) (s x), map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext

Goal state after:
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✝
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
⊢ { toFun := fun s x ↦ ((m✝ • x✝) x) (s x), map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id R) m✝ • { toFun := fun s x ↦ (x✝ x) (s x), map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext

Goal state after:
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✝
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
f : R →ₗ[R] M
⊢ smulRight 1 ((fun f ↦ f 1) f) = f

Tactic:
ext

Goal state after:
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
f : R →ₗ[R] M
⊢ (smulRight 1 ((fun f ↦ f 1) f)) 1 = f 1
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: case add
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m x✝ y✝ : M
hx✝ : x✝ ∈ ⨆ i, ↑i
hy✝ : y✝ ∈ ⨆ i, ↑i
mx : t • x✝ ∈ ⨆ a, ↑a
my : t • y✝ ∈ ⨆ a, ↑a
⊢ t • (x✝ + y✝) ∈ ⨆ a, ↑a

Tactic:
revert mx my

Goal state after:
case add
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m x✝ y✝ : M
hx✝ : x✝ ∈ ⨆ i, ↑i
hy✝ : y✝ ∈ ⨆ i, ↑i
⊢ t • x✝ ∈ ⨆ a, ↑a → t • y✝ ∈ ⨆ a, ↑a → t • (x✝ + y✝) ∈ ⨆ a, ↑a
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
⊢ f.restrict hf - g.restrict hg = (f - g).restrict hfg

Tactic:
ext

Goal state after:
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✝)
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 σ₁₂ σ₂₁' σ₁₁'
e : M₁ ≃ₛₗ[σ₁₂] M₂
x✝¹ x✝ : Module.End R₁ M₁
⊢ (e.arrowCongrAddEquiv e).toFun (x✝¹ * x✝) = (e.arrowCongrAddEquiv e).toFun x✝¹ * (e.arrowCongrAddEquiv e).toFun x✝

Tactic:
ext

Goal state after:
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 σ₁₂ σ₂₁' σ₁₁'
e : M₁ ≃ₛₗ[σ₁₂] M₂
x✝² x✝¹ : Module.End R₁ M₁
x✝ : M₂
⊢ ((e.arrowCongrAddEquiv e).toFun (x✝² * x✝¹)) x✝ =
    ((e.arrowCongrAddEquiv e).toFun x✝² * (e.arrowCongrAddEquiv e).toFun x✝¹) x✝
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₁'
⊢ ((refl R₁ M₁).arrowCongrAddEquiv e₂).toFun (DomMulAct.mk x✝¹ • x✝) =
    (RingHom.id Sᵈᵐᵃ) (DomMulAct.mk x✝¹) • ((refl R₁ M₁).arrowCongrAddEquiv e₂).toFun x✝

Tactic:
ext

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