case map_add
R✝ : Type ?u.1522508
R₁ : Type ?u.1522511
R₂ : Type ?u.1522514
R₃ : Type ?u.1522517
R₄ : Type ?u.1522520
S : Type ?u.1522523
K : Type ?u.1522526
K₂ : Type ?u.1522529
M✝ : Type ?u.1522532
M' : Type ?u.1522535
M₁ : Type ?u.1522538
M₂ : Type ?u.1522541
M₃ : Type ?u.1522544
M₄ : Type ?u.1522547
N : Type ?u.1522550
N₂ : Type ?u.1522553
ι : Type ?u.1522556
V : Type ?u.1522559
V₂ : Type ?u.1522562
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommGroup 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.1522508
R₁ : Type ?u.1522511
R₂ : Type ?u.1522514
R₃ : Type ?u.1522517
R₄ : Type ?u.1522520
S : Type ?u.1522523
K : Type ?u.1522526
K₂ : Type ?u.1522529
M✝ : Type ?u.1522532
M' : Type ?u.1522535
M₁ : Type ?u.1522538
M₂ : Type ?u.1522541
M₃ : Type ?u.1522544
M₄ : Type ?u.1522547
N : Type ?u.1522550
N₂ : Type ?u.1522553
ι : Type ?u.1522556
V : Type ?u.1522559
V₂ : Type ?u.1522562
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ∀ (c : R) (x : M × M), (c • x).fst - (c • x).snd = c • (x.fst - x.snd)
R✝ : Type ?u.1522508
R₁ : Type ?u.1522511
R₂ : Type ?u.1522514
R₃ : Type ?u.1522517
R₄ : Type ?u.1522520
S : Type ?u.1522523
K : Type ?u.1522526
K₂ : Type ?u.1522529
M✝ : Type ?u.1522532
M' : Type ?u.1522535
M₁ : Type ?u.1522538
M₂ : Type ?u.1522541
M₃ : Type ?u.1522544
M₄ : Type ?u.1522547
N : Type ?u.1522550
N₂ : Type ?u.1522553
ι : Type ?u.1522556
V : Type ?u.1522559
V₂ : Type ?u.1522562
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ IsLinearMap R fun x => x.fst - x.snd
apply IsLinearMap.mk
case map_add
R✝ : Type ?u.1522508
R₁ : Type ?u.1522511
R₂ : Type ?u.1522514
R₃ : Type ?u.1522517
R₄ : Type ?u.1522520
S : Type ?u.1522523
K : Type ?u.1522526
K₂ : Type ?u.1522529
M✝ : Type ?u.1522532
M' : Type ?u.1522535
M₁ : Type ?u.1522538
M₂ : Type ?u.1522541
M₃ : Type ?u.1522544
M₄ : Type ?u.1522547
N : Type ?u.1522550
N₂ : Type ?u.1522553
ι : Type ?u.1522556
V : Type ?u.1522559
V₂ : Type ?u.1522562
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommGroup 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.1522508
R₁ : Type ?u.1522511
R₂ : Type ?u.1522514
R₃ : Type ?u.1522517
R₄ : Type ?u.1522520
S : Type ?u.1522523
K : Type ?u.1522526
K₂ : Type ?u.1522529
M✝ : Type ?u.1522532
M' : Type ?u.1522535
M₁ : Type ?u.1522538
M₂ : Type ?u.1522541
M₃ : Type ?u.1522544
M₄ : Type ?u.1522547
N : Type ?u.1522550
N₂ : Type ?u.1522553
ι : Type ?u.1522556
V : Type ?u.1522559
V₂ : Type ?u.1522562
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommGroup 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.1522508
R₁ : Type ?u.1522511
R₂ : Type ?u.1522514
R₃ : Type ?u.1522517
R₄ : Type ?u.1522520
S : Type ?u.1522523
K : Type ?u.1522526
K₂ : Type ?u.1522529
M✝ : Type ?u.1522532
M' : Type ?u.1522535
M₁ : Type ?u.1522538
M₂ : Type ?u.1522541
M₃ : Type ?u.1522544
M₄ : Type ?u.1522547
N : Type ?u.1522550
N₂ : Type ?u.1522553
ι : Type ?u.1522556
V : Type ?u.1522559
V₂ : Type ?u.1522562
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommGroup 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.1522508
R₁ : Type ?u.1522511
R₂ : Type ?u.1522514
R₃ : Type ?u.1522517
R₄ : Type ?u.1522520
S : Type ?u.1522523
K : Type ?u.1522526
K₂ : Type ?u.1522529
M✝ : Type ?u.1522532
M' : Type ?u.1522535
M₁ : Type ?u.1522538
M₂ : Type ?u.1522541
M₃ : Type ?u.1522544
M₄ : Type ?u.1522547
N : Type ?u.1522550
N₂ : Type ?u.1522553
ι : Type ?u.1522556
V : Type ?u.1522559
V₂ : Type ?u.1522562
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M × M
⊢ (x + y).fst - (x + y).snd = x.fst - x.snd + (y.fst - y.snd)
rw [Prod.fst_add, Prod.snd_add]
no goals
case map_add
R✝ : Type ?u.1522508
R₁ : Type ?u.1522511
R₂ : Type ?u.1522514
R₃ : Type ?u.1522517
R₄ : Type ?u.1522520
S : Type ?u.1522523
K : Type ?u.1522526
K₂ : Type ?u.1522529
M✝ : Type ?u.1522532
M' : Type ?u.1522535
M₁ : Type ?u.1522538
M₂ : Type ?u.1522541
M₃ : Type ?u.1522544
M₄ : Type ?u.1522547
N : Type ?u.1522550
N₂ : Type ?u.1522553
ι : Type ?u.1522556
V : Type ?u.1522559
V₂ : Type ?u.1522562
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommGroup 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.1522508
R₁ : Type ?u.1522511
R₂ : Type ?u.1522514
R₃ : Type ?u.1522517
R₄ : Type ?u.1522520
S : Type ?u.1522523
K : Type ?u.1522526
K₂ : Type ?u.1522529
M✝ : Type ?u.1522532
M' : Type ?u.1522535
M₁ : Type ?u.1522538
M₂ : Type ?u.1522541
M₃ : Type ?u.1522544
M₄ : Type ?u.1522547
N : Type ?u.1522550
N₂ : Type ?u.1522553
ι : Type ?u.1522556
V : Type ?u.1522559
V₂ : Type ?u.1522562
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommGroup 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.1522508
R₁ : Type ?u.1522511
R₂ : Type ?u.1522514
R₃ : Type ?u.1522517
R₄ : Type ?u.1522520
S : Type ?u.1522523
K : Type ?u.1522526
K₂ : Type ?u.1522529
M✝ : Type ?u.1522532
M' : Type ?u.1522535
M₁ : Type ?u.1522538
M₂ : Type ?u.1522541
M₃ : Type ?u.1522544
M₄ : Type ?u.1522547
N : Type ?u.1522550
N₂ : Type ?u.1522553
ι : Type ?u.1522556
V : Type ?u.1522559
V₂ : Type ?u.1522562
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommGroup 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.1522508
R₁ : Type ?u.1522511
R₂ : Type ?u.1522514
R₃ : Type ?u.1522517
R₄ : Type ?u.1522520
S : Type ?u.1522523
K : Type ?u.1522526
K₂ : Type ?u.1522529
M✝ : Type ?u.1522532
M' : Type ?u.1522535
M₁ : Type ?u.1522538
M₂ : Type ?u.1522541
M₃ : Type ?u.1522544
M₄ : Type ?u.1522547
N : Type ?u.1522550
N₂ : Type ?u.1522553
ι : Type ?u.1522556
V : Type ?u.1522559
V₂ : Type ?u.1522562
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : R
y : M × M
⊢ (x • y).fst - (x • y).snd = x • (y.fst - y.snd)
simp [smul_sub]