case map_add
R : Type u_1
R₁ : Type ?u.1518516
R₂ : Type ?u.1518519
R₃ : Type ?u.1518522
R₄ : Type ?u.1518525
S : Type ?u.1518528
K : Type ?u.1518531
K₂ : Type ?u.1518534
M : Type u_2
M' : Type ?u.1518540
M₁ : Type ?u.1518543
M₂ : Type ?u.1518546
M₃ : Type ?u.1518549
M₄ : Type ?u.1518552
N : Type ?u.1518555
N₂ : Type ?u.1518558
ι : Type ?u.1518561
V : Type ?u.1518564
V₂ : Type ?u.1518567
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ∀ (x y : M × M), (x + y).fst + (x + y).snd = x.fst + x.snd + (y.fst + y.snd)

case map_smul
R : Type u_1
R₁ : Type ?u.1518516
R₂ : Type ?u.1518519
R₃ : Type ?u.1518522
R₄ : Type ?u.1518525
S : Type ?u.1518528
K : Type ?u.1518531
K₂ : Type ?u.1518534
M : Type u_2
M' : Type ?u.1518540
M₁ : Type ?u.1518543
M₂ : Type ?u.1518546
M₃ : Type ?u.1518549
M₄ : Type ?u.1518552
N : Type ?u.1518555
N₂ : Type ?u.1518558
ι : Type ?u.1518561
V : Type ?u.1518564
V₂ : Type ?u.1518567
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ∀ (c : R) (x : M × M), (c • x).fst + (c • x).snd = c • (x.fst + x.snd)
R : Type u_1
R₁ : Type ?u.1518516
R₂ : Type ?u.1518519
R₃ : Type ?u.1518522
R₄ : Type ?u.1518525
S : Type ?u.1518528
K : Type ?u.1518531
K₂ : Type ?u.1518534
M : Type u_2
M' : Type ?u.1518540
M₁ : Type ?u.1518543
M₂ : Type ?u.1518546
M₃ : Type ?u.1518549
M₄ : Type ?u.1518552
N : Type ?u.1518555
N₂ : Type ?u.1518558
ι : Type ?u.1518561
V : Type ?u.1518564
V₂ : Type ?u.1518567
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ IsLinearMap R fun x => x.fst + x.snd
apply IsLinearMap.mk
case map_add
R : Type u_1
R₁ : Type ?u.1518516
R₂ : Type ?u.1518519
R₃ : Type ?u.1518522
R₄ : Type ?u.1518525
S : Type ?u.1518528
K : Type ?u.1518531
K₂ : Type ?u.1518534
M : Type u_2
M' : Type ?u.1518540
M₁ : Type ?u.1518543
M₂ : Type ?u.1518546
M₃ : Type ?u.1518549
M₄ : Type ?u.1518552
N : Type ?u.1518555
N₂ : Type ?u.1518558
ι : Type ?u.1518561
V : Type ?u.1518564
V₂ : Type ?u.1518567
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M × M
⊢ (x + y).fst + (x + y).snd = x.fst + x.snd + (y.fst + y.snd)
case map_add
R : Type u_1
R₁ : Type ?u.1518516
R₂ : Type ?u.1518519
R₃ : Type ?u.1518522
R₄ : Type ?u.1518525
S : Type ?u.1518528
K : Type ?u.1518531
K₂ : Type ?u.1518534
M : Type u_2
M' : Type ?u.1518540
M₁ : Type ?u.1518543
M₂ : Type ?u.1518546
M₃ : Type ?u.1518549
M₄ : Type ?u.1518552
N : Type ?u.1518555
N₂ : Type ?u.1518558
ι : Type ?u.1518561
V : Type ?u.1518564
V₂ : Type ?u.1518567
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ∀ (x y : M × M), (x + y).fst + (x + y).snd = x.fst + x.snd + (y.fst + y.snd)
intro x y
case map_add
R : Type u_1
R₁ : Type ?u.1518516
R₂ : Type ?u.1518519
R₃ : Type ?u.1518522
R₄ : Type ?u.1518525
S : Type ?u.1518528
K : Type ?u.1518531
K₂ : Type ?u.1518534
M : Type u_2
M' : Type ?u.1518540
M₁ : Type ?u.1518543
M₂ : Type ?u.1518546
M₃ : Type ?u.1518549
M₄ : Type ?u.1518552
N : Type ?u.1518555
N₂ : Type ?u.1518558
ι : Type ?u.1518561
V : Type ?u.1518564
V₂ : Type ?u.1518567
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M × M
⊢ x.fst + y.fst + (x.snd + y.snd) = x.fst + x.snd + (y.fst + y.snd)
case map_add
R : Type u_1
R₁ : Type ?u.1518516
R₂ : Type ?u.1518519
R₃ : Type ?u.1518522
R₄ : Type ?u.1518525
S : Type ?u.1518528
K : Type ?u.1518531
K₂ : Type ?u.1518534
M : Type u_2
M' : Type ?u.1518540
M₁ : Type ?u.1518543
M₂ : Type ?u.1518546
M₃ : Type ?u.1518549
M₄ : Type ?u.1518552
N : Type ?u.1518555
N₂ : Type ?u.1518558
ι : Type ?u.1518561
V : Type ?u.1518564
V₂ : Type ?u.1518567
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M × M
⊢ (x + y).fst + (x + y).snd = x.fst + x.snd + (y.fst + y.snd)
simp only [Prod.fst_add, Prod.snd_add]
no goals
case map_add
R : Type u_1
R₁ : Type ?u.1518516
R₂ : Type ?u.1518519
R₃ : Type ?u.1518522
R₄ : Type ?u.1518525
S : Type ?u.1518528
K : Type ?u.1518531
K₂ : Type ?u.1518534
M : Type u_2
M' : Type ?u.1518540
M₁ : Type ?u.1518543
M₂ : Type ?u.1518546
M₃ : Type ?u.1518549
M₄ : Type ?u.1518552
N : Type ?u.1518555
N₂ : Type ?u.1518558
ι : Type ?u.1518561
V : Type ?u.1518564
V₂ : Type ?u.1518567
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M × M
⊢ x.fst + y.fst + (x.snd + y.snd) = x.fst + x.snd + (y.fst + y.snd)
abel
case map_smul
R : Type u_1
R₁ : Type ?u.1518516
R₂ : Type ?u.1518519
R₃ : Type ?u.1518522
R₄ : Type ?u.1518525
S : Type ?u.1518528
K : Type ?u.1518531
K₂ : Type ?u.1518534
M : Type u_2
M' : Type ?u.1518540
M₁ : Type ?u.1518543
M₂ : Type ?u.1518546
M₃ : Type ?u.1518549
M₄ : Type ?u.1518552
N : Type ?u.1518555
N₂ : Type ?u.1518558
ι : Type ?u.1518561
V : Type ?u.1518564
V₂ : Type ?u.1518567
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : R
y : M × M
⊢ (x • y).fst + (x • y).snd = x • (y.fst + y.snd)
case map_smul
R : Type u_1
R₁ : Type ?u.1518516
R₂ : Type ?u.1518519
R₃ : Type ?u.1518522
R₄ : Type ?u.1518525
S : Type ?u.1518528
K : Type ?u.1518531
K₂ : Type ?u.1518534
M : Type u_2
M' : Type ?u.1518540
M₁ : Type ?u.1518543
M₂ : Type ?u.1518546
M₃ : Type ?u.1518549
M₄ : Type ?u.1518552
N : Type ?u.1518555
N₂ : Type ?u.1518558
ι : Type ?u.1518561
V : Type ?u.1518564
V₂ : Type ?u.1518567
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ∀ (c : R) (x : M × M), (c • x).fst + (c • x).snd = c • (x.fst + x.snd)
intro x y
no goals
case map_smul
R : Type u_1
R₁ : Type ?u.1518516
R₂ : Type ?u.1518519
R₃ : Type ?u.1518522
R₄ : Type ?u.1518525
S : Type ?u.1518528
K : Type ?u.1518531
K₂ : Type ?u.1518534
M : Type u_2
M' : Type ?u.1518540
M₁ : Type ?u.1518543
M₂ : Type ?u.1518546
M₃ : Type ?u.1518549
M₄ : Type ?u.1518552
N : Type ?u.1518555
N₂ : Type ?u.1518558
ι : Type ?u.1518561
V : Type ?u.1518564
V₂ : Type ?u.1518567
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : R
y : M × M
⊢ (x • y).fst + (x • y).snd = x • (y.fst + y.snd)
simp [smul_add]