mathlib-initiative/mathlib-tactics huggingface dataset:
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 σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₁ →ₛₗ[σ₁₃] M₃
⊢ (f ∘ₛₗ ↑e.symm) ∘ₛₗ ↑e = f

Tactic:
ext

Goal state after:
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 σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₁ →ₛₗ[σ₁₃] M₃
x✝ : M₁
⊢ ((f ∘ₛₗ ↑e.symm) ∘ₛₗ ↑e) x✝ = f x✝
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₁
inst✝⁵ : RingHomInvPair σ₁₃ σ₃₁
inst✝⁴ : RingHomInvPair σ₃₁ σ₁₃
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₁ ≃ₛₗ[σ₁₃] M₃
⊢ e.trans (e.symm.trans f) = f

Tactic:
ext

Goal state after:
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₁
inst✝⁵ : RingHomInvPair σ₁₃ σ₃₁
inst✝⁴ : RingHomInvPair σ₃₁ σ₁₃
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₁ ≃ₛₗ[σ₁₃] M₃
x✝ : M₁
⊢ (e.trans (e.symm.trans f)) x✝ = f x✝
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₁
inst✝⁵ : RingHomInvPair σ₁₃ σ₃₁
inst✝⁴ : RingHomInvPair σ₃₁ σ₁₃
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₂ ≃ₛₗ[σ₂₃] M₃
⊢ e.symm.trans (e.trans f) = f

Tactic:
ext

Goal state after:
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₁
inst✝⁵ : RingHomInvPair σ₁₃ σ₃₁
inst✝⁴ : RingHomInvPair σ₃₁ σ₁₃
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₂ ≃ₛₗ[σ₂₃] M₃
x✝ : M₂
⊢ (e.symm.trans (e.trans f)) x✝ = f x✝
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₁
inst✝⁵ : RingHomInvPair σ₁₃ σ₃₁
inst✝⁴ : RingHomInvPair σ₃₁ σ₁₃
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ ≃ₛₗ[σ₃₁] M₁
⊢ (f.trans e).trans e.symm = f

Tactic:
ext

Goal state after:
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₁
inst✝⁵ : RingHomInvPair σ₁₃ σ₃₁
inst✝⁴ : RingHomInvPair σ₃₁ σ₁₃
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ ≃ₛₗ[σ₃₁] M₁
x✝ : M₃
⊢ ((f.trans e).trans e.symm) x✝ = f x✝
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₁
inst✝⁵ : RingHomInvPair σ₁₃ σ₃₁
inst✝⁴ : RingHomInvPair σ₃₁ σ₁₃
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ ≃ₛₗ[σ₃₂] M₂
⊢ (f.trans e.symm).trans e = f

Tactic:
ext

Goal state after:
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₁
inst✝⁵ : RingHomInvPair σ₁₃ σ₃₁
inst✝⁴ : RingHomInvPair σ₃₁ σ₁₃
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ ≃ₛₗ[σ₃₂] M₂
x✝ : M₃
⊢ ((f.trans e.symm).trans e) x✝ = f x✝
Module: Mathlib.Algebra.Module.Equiv.Defs

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

Tactic:
ext

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

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

Tactic:
ext

Goal state after:
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✝
Module: Mathlib.Algebra.Module.LinearMap.Defs

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

Tactic:
ext

Goal state after:
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✝ : M
⊢ (toAddMonoidHom 0) x✝ = 0 x✝
Module: Mathlib.Algebra.Module.LinearMap.Defs

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

Tactic:
ext

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

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

Tactic:
ext

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

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

Tactic:
ext

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

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

Tactic:
ext

Goal state after:
I : Type u
f : I → Type v
i : I
inst✝ : (i : I) → Distrib (f i)
a✝ b✝ c✝ : (i : I) → f i
x✝ : I
⊢ (a✝ * (b✝ + c✝)) x✝ = (a✝ * b✝ + a✝ * c✝) x✝
Module: Mathlib.Algebra.Ring.Pi

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

Tactic:
ext

Goal state after:
I : Type u
f : I → Type v
i : I
inst✝ : (i : I) → Distrib (f i)
a✝ b✝ c✝ : (i : I) → f i
x✝ : I
⊢ ((a✝ + b✝) * c✝) x✝ = (a✝ * c✝ + b✝ * c✝) x✝
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:
ext

Goal state after:
case fst
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✝).1 = (x✝² • x✝ + x✝¹ • x✝).1

case snd
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✝).2 = (x✝² • x✝ + x✝¹ • x✝).2
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:
ext

Goal state after:
case fst
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✝).1 = 0.1

case snd
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✝).2 = 0.2
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:
ext

Goal state after:
case fst
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).1 = 0.1

case snd
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).2 = 0.2
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:
ext

Goal state after:
case fst
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✝)).1 = (x✝² • x✝¹ + x✝² • x✝).1

case snd
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✝)).2 = (x✝² • x✝¹ + x✝² • x✝).2
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:
ext

Goal state after:
case fst
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 = 1.1

case snd
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).2 = 1.2
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:
ext

Goal state after:
case fst
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✝)).1 = (x✝² • x✝¹ * x✝² • x✝).1

case snd
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✝)).2 = (x✝² • x✝¹ * x✝² • x✝).2
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:
ext

Goal state after:
case fst
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✝).1 = 0.1

case snd
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✝).2 = 0.2
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:
ext

Goal state after:
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 x✝ : A
⊢ (mulLeft R (a * b)) x✝ = (mulLeft R a ∘ₗ mulLeft R b) x✝
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:
ext

Goal state after:
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 x✝ : A
⊢ (mulRight R (a * b)) x✝ = (mulRight R b ∘ₗ mulRight R a) x✝
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
⊢ f.smulRight 0 = 0

Tactic:
ext

Goal state after:
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✝
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
⊢ smulRight 0 x = 0

Tactic:
ext

Goal state after:
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✝
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
m m' : M
⊢ f.smulRight (m + m') = f.smulRight m + 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
m m' : M
x✝ : M₂
⊢ (f.smulRight (m + m')) x✝ = (f.smulRight m + f.smulRight m') x✝