[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
F : Type u_17
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
inst✝ : SemilinearMapClass F σ M M₃
src✝ : AddHomClass F M M₃ := toAddHomClass
f : F
⊢ ↑f 0 = 0
[PROOFSTEP]
rw [← zero_smul R (0 : M), map_smulₛₗ]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
F : Type u_17
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
inst✝ : SemilinearMapClass F σ M M₃
src✝ : AddHomClass F M M₃ := toAddHomClass
f : F
⊢ ↑σ 0 • ↑f 0 = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
F : Type u_17
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
inst✝ : LinearMapClass F R M M₂
src✝ : AddMonoidHomClass F M M₂ := addMonoidHomClass F
f : F
c : R
x : M
⊢ ↑f (c • x) = c • ↑f x
[PROOFSTEP]
rw [map_smulₛₗ, RingHom.id_apply]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
F : Type u_17
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
f : F
i : SemilinearMapClass F σ M M₃
σ' : S →+* R
inst✝ : RingHomInvPair σ σ'
c : S
x : M
⊢ c • ↑f x = ↑f (↑σ' c • x)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring S
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module S M₃
σ : R →+* S
f g : M →ₛₗ[σ] M₃
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring S
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module S M₃
σ : R →+* S
g : M →ₛₗ[σ] M₃
toAddHom✝ : AddHom M M₃
map_smul'✝ : ∀ (r : R) (x : M), AddHom.toFun toAddHom✝ (r • x) = ↑σ r • AddHom.toFun toAddHom✝ x
h : (fun f => f.toFun) { toAddHom := toAddHom✝, map_smul' := map_smul'✝ } = (fun f => f.toFun) g
⊢ { toAddHom := toAddHom✝, map_smul' := map_smul'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring S
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module S M₃
σ : R →+* S
toAddHom✝¹ : AddHom M M₃
map_smul'✝¹ : ∀ (r : R) (x : M), AddHom.toFun toAddHom✝¹ (r • x) = ↑σ r • AddHom.toFun toAddHom✝¹ x
toAddHom✝ : AddHom M M₃
map_smul'✝ : ∀ (r : R) (x : M), AddHom.toFun toAddHom✝ (r • x) = ↑σ r • AddHom.toFun toAddHom✝ x
h :
  (fun f => f.toFun) { toAddHom := toAddHom✝¹, map_smul' := map_smul'✝¹ } =
    (fun f => f.toFun) { toAddHom := toAddHom✝, map_smul' := map_smul'✝ }
⊢ { toAddHom := toAddHom✝¹, map_smul' := map_smul'✝¹ } = { toAddHom := toAddHom✝, map_smul' := map_smul'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toAddHom
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring S
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module S M₃
σ : R →+* S
toAddHom✝¹ : AddHom M M₃
map_smul'✝¹ : ∀ (r : R) (x : M), AddHom.toFun toAddHom✝¹ (r • x) = ↑σ r • AddHom.toFun toAddHom✝¹ x
toAddHom✝ : AddHom M M₃
map_smul'✝ : ∀ (r : R) (x : M), AddHom.toFun toAddHom✝ (r • x) = ↑σ r • AddHom.toFun toAddHom✝ x
h :
  (fun f => f.toFun) { toAddHom := toAddHom✝¹, map_smul' := map_smul'✝¹ } =
    (fun f => f.toFun) { toAddHom := toAddHom✝, map_smul' := map_smul'✝ }
⊢ toAddHom✝¹ = toAddHom✝
[PROOFSTEP]
apply FunLike.coe_injective'
[GOAL]
case mk.mk.e_toAddHom.a
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring S
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module S M₃
σ : R →+* S
toAddHom✝¹ : AddHom M M₃
map_smul'✝¹ : ∀ (r : R) (x : M), AddHom.toFun toAddHom✝¹ (r • x) = ↑σ r • AddHom.toFun toAddHom✝¹ x
toAddHom✝ : AddHom M M₃
map_smul'✝ : ∀ (r : R) (x : M), AddHom.toFun toAddHom✝ (r • x) = ↑σ r • AddHom.toFun toAddHom✝ x
h :
  (fun f => f.toFun) { toAddHom := toAddHom✝¹, map_smul' := map_smul'✝¹ } =
    (fun f => f.toFun) { toAddHom := toAddHom✝, map_smul' := map_smul'✝ }
⊢ ↑toAddHom✝¹ = ↑toAddHom✝
[PROOFSTEP]
exact h
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ✝ : R →+* S
σ : R →+* R
inst✝ : RingHomId σ
r : R
x : M
⊢ AddHom.toFun { toFun := fun x => x, map_add' := (_ : ∀ (x y : M), (fun x => x) (x + y) = (fun x => x) (x + y)) }
      (r • x) =
    ↑σ r •
      AddHom.toFun { toFun := fun x => x, map_add' := (_ : ∀ (x y : M), (fun x => x) (x + y) = (fun x => x) (x + y)) } x
[PROOFSTEP]
have := (RingHomId.eq_id : σ = _)
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ✝ : R →+* S
σ : R →+* R
inst✝ : RingHomId σ
r : R
x : M
this : σ = RingHom.id R
⊢ AddHom.toFun { toFun := fun x => x, map_add' := (_ : ∀ (x y : M), (fun x => x) (x + y) = (fun x => x) (x + y)) }
      (r • x) =
    ↑σ r •
      AddHom.toFun { toFun := fun x => x, map_add' := (_ : ∀ (x y : M), (fun x => x) (x + y) = (fun x => x) (x + y)) } x
[PROOFSTEP]
subst this
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
r : R
x : M
inst✝ : RingHomId (RingHom.id R)
⊢ AddHom.toFun { toFun := fun x => x, map_add' := (_ : ∀ (x y : M), (fun x => x) (x + y) = (fun x => x) (x + y)) }
      (r • x) =
    ↑(RingHom.id R) r •
      AddHom.toFun { toFun := fun x => x, map_add' := (_ : ∀ (x y : M), (fun x => x) (x + y) = (fun x => x) (x + y)) } x
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
fₗ gₗ : M →ₗ[R] M₂
f g : M →ₛₗ[σ] M₃
σ' : S →+* R
inst✝ : RingHomInvPair σ σ'
c : S
x : M
⊢ c • ↑f x = ↑f (↑σ' c • x)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
fₗ gₗ : M →ₗ[R] M₂
f g : M →ₛₗ[σ] M₃
F : Type u_17
h : F
inst✝ : SemilinearMapClass F σ M M₃
c : R
s : Set M
⊢ ↑h '' (c • s) = ↑σ c • ↑h '' s
[PROOFSTEP]
apply Set.Subset.antisymm
[GOAL]
case h₁
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
fₗ gₗ : M →ₗ[R] M₂
f g : M →ₛₗ[σ] M₃
F : Type u_17
h : F
inst✝ : SemilinearMapClass F σ M M₃
c : R
s : Set M
⊢ ↑h '' (c • s) ⊆ ↑σ c • ↑h '' s
[PROOFSTEP]
rintro x ⟨y, ⟨z, zs, rfl⟩, rfl⟩
[GOAL]
case h₁.intro.intro.intro.intro
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
fₗ gₗ : M →ₗ[R] M₂
f g : M →ₛₗ[σ] M₃
F : Type u_17
h : F
inst✝ : SemilinearMapClass F σ M M₃
c : R
s : Set M
z : M
zs : z ∈ s
⊢ ↑h ((fun x => c • x) z) ∈ ↑σ c • ↑h '' s
[PROOFSTEP]
exact ⟨h z, Set.mem_image_of_mem _ zs, (map_smulₛₗ _ _ _).symm⟩
[GOAL]
case h₂
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
fₗ gₗ : M →ₗ[R] M₂
f g : M →ₛₗ[σ] M₃
F : Type u_17
h : F
inst✝ : SemilinearMapClass F σ M M₃
c : R
s : Set M
⊢ ↑σ c • ↑h '' s ⊆ ↑h '' (c • s)
[PROOFSTEP]
rintro x ⟨y, ⟨z, hz, rfl⟩, rfl⟩
[GOAL]
case h₂.intro.intro.intro.intro
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
fₗ gₗ : M →ₗ[R] M₂
f g : M →ₛₗ[σ] M₃
F : Type u_17
h : F
inst✝ : SemilinearMapClass F σ M M₃
c : R
s : Set M
z : M
hz : z ∈ s
⊢ (fun x => ↑σ c • x) (↑h z) ∈ ↑h '' (c • s)
[PROOFSTEP]
exact (Set.mem_image _ _ _).2 ⟨c • z, Set.smul_mem_smul_set hz, map_smulₛₗ _ _ _⟩
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
fₗ gₗ : M →ₗ[R] M₂
f g : M →ₛₗ[σ] M₃
F : Type u_17
h : F
inst✝ : SemilinearMapClass F σ M M₃
c : R
hc : IsUnit c
s : Set M₃
⊢ ↑h ⁻¹' (↑σ c • s) = c • ↑h ⁻¹' s
[PROOFSTEP]
apply Set.Subset.antisymm
[GOAL]
case h₁
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
fₗ gₗ : M →ₗ[R] M₂
f g : M →ₛₗ[σ] M₃
F : Type u_17
h : F
inst✝ : SemilinearMapClass F σ M M₃
c : R
hc : IsUnit c
s : Set M₃
⊢ ↑h ⁻¹' (↑σ c • s) ⊆ c • ↑h ⁻¹' s
[PROOFSTEP]
rintro x ⟨y, ys, hy⟩
[GOAL]
case h₁.intro.intro
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
fₗ gₗ : M →ₗ[R] M₂
f g : M →ₛₗ[σ] M₃
F : Type u_17
h : F
inst✝ : SemilinearMapClass F σ M M₃
c : R
hc : IsUnit c
s : Set M₃
x : M
y : M₃
ys : y ∈ s
hy : (fun x => ↑σ c • x) y = ↑h x
⊢ x ∈ c • ↑h ⁻¹' s
[PROOFSTEP]
refine' ⟨(hc.unit.inv : R) • x, _, _⟩
[GOAL]
case h₁.intro.intro.refine'_1
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
fₗ gₗ : M →ₗ[R] M₂
f g : M →ₛₗ[σ] M₃
F : Type u_17
h : F
inst✝ : SemilinearMapClass F σ M M₃
c : R
hc : IsUnit c
s : Set M₃
x : M
y : M₃
ys : y ∈ s
hy : (fun x => ↑σ c • x) y = ↑h x
⊢ (IsUnit.unit hc).inv • x ∈ ↑h ⁻¹' s
[PROOFSTEP]
simp only [← hy, smul_smul, Set.mem_preimage, Units.inv_eq_val_inv, map_smulₛₗ h, ← map_mul, IsUnit.val_inv_mul,
  one_smul, map_one, ys]
[GOAL]
case h₁.intro.intro.refine'_2
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
fₗ gₗ : M →ₗ[R] M₂
f g : M →ₛₗ[σ] M₃
F : Type u_17
h : F
inst✝ : SemilinearMapClass F σ M M₃
c : R
hc : IsUnit c
s : Set M₃
x : M
y : M₃
ys : y ∈ s
hy : (fun x => ↑σ c • x) y = ↑h x
⊢ (fun x => c • x) ((IsUnit.unit hc).inv • x) = x
[PROOFSTEP]
simp only [smul_smul, IsUnit.mul_val_inv, one_smul, Units.inv_eq_val_inv]
[GOAL]
case h₂
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
fₗ gₗ : M →ₗ[R] M₂
f g : M →ₛₗ[σ] M₃
F : Type u_17
h : F
inst✝ : SemilinearMapClass F σ M M₃
c : R
hc : IsUnit c
s : Set M₃
⊢ c • ↑h ⁻¹' s ⊆ ↑h ⁻¹' (↑σ c • s)
[PROOFSTEP]
rintro x ⟨y, hy, rfl⟩
[GOAL]
case h₂.intro.intro
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
fₗ gₗ : M →ₗ[R] M₂
f g : M →ₛₗ[σ] M₃
F : Type u_17
h : F
inst✝ : SemilinearMapClass F σ M M₃
c : R
hc : IsUnit c
s : Set M₃
y : M
hy : y ∈ ↑h ⁻¹' s
⊢ (fun x => c • x) y ∈ ↑h ⁻¹' (↑σ c • s)
[PROOFSTEP]
refine' ⟨h y, hy, by simp only [RingHom.id_apply, map_smulₛₗ h]⟩
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
fₗ gₗ : M →ₗ[R] M₂
f g : M →ₛₗ[σ] M₃
F : Type u_17
h : F
inst✝ : SemilinearMapClass F σ M M₃
c : R
hc : IsUnit c
s : Set M₃
y : M
hy : y ∈ ↑h ⁻¹' s
⊢ (fun x => ↑σ c • x) (↑h y) = ↑h ((fun x => c • x) y)
[PROOFSTEP]
simp only [RingHom.id_apply, map_smulₛₗ h]
[GOAL]
R✝ : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S✝ : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹⁹ : Semiring R✝
inst✝¹⁸ : Semiring S✝
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : AddCommMonoid M₁
inst✝¹⁵ : AddCommMonoid M₂
inst✝¹⁴ : AddCommMonoid M₃
inst✝¹³ : AddCommMonoid N₁
inst✝¹² : AddCommMonoid N₂
inst✝¹¹ : AddCommMonoid N₃
inst✝¹⁰ : Module R✝ M
inst✝⁹ : Module R✝ M₂
inst✝⁸ : Module S✝ M₃
σ : R✝ →+* S✝
fₗ✝ gₗ : M →ₗ[R✝] M₂
f g : M →ₛₗ[σ] M₃
R : Type u_17
S : Type u_18
inst✝⁷ : Semiring S
inst✝⁶ : SMul R S
inst✝⁵ : SMul R M
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
inst✝² : SMul R M₂
inst✝¹ : Module S M₂
inst✝ : IsScalarTower R S M₂
fₗ : M →ₗ[S] M₂
c : R
x : M
⊢ ↑fₗ (c • x) = c • ↑fₗ x
[PROOFSTEP]
rw [← smul_one_smul S c x, ← smul_one_smul S c (fₗ x), map_smul]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring S
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module S M₃
σ : R →+* S
fₗ gₗ : M →ₗ[R] M₂
f✝ g✝ : M →ₛₗ[σ] M₃
f g : R →ₛₗ[σ] M₃
h : ↑f 1 = ↑g 1
x : R
⊢ ↑f x = ↑g x
[PROOFSTEP]
rw [← mul_one x, ← smul_eq_mul, f.map_smulₛₗ, g.map_smulₛₗ, h]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring S
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module S M₃
σ✝ : R →+* S
fₗ gₗ : M →ₗ[R] M₂
f✝ g✝ : M →ₛₗ[σ✝] M₃
σ : Rᵐᵒᵖ →+* S
f g : R →ₛₗ[σ] M₃
h : ↑f 1 = ↑g 1
x : R
⊢ ↑f x = ↑g x
[PROOFSTEP]
rw [← one_mul x, ← op_smul_eq_mul]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring S
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module S M₃
σ✝ : R →+* S
fₗ gₗ : M →ₗ[R] M₂
f✝ g✝ : M →ₛₗ[σ✝] M₃
σ : Rᵐᵒᵖ →+* S
f g : R →ₛₗ[σ] M₃
h : ↑f 1 = ↑g 1
x : R
⊢ ↑f (MulOpposite.op x • 1) = ↑g (MulOpposite.op x • 1)
[PROOFSTEP]
refine (f.map_smulₛₗ (MulOpposite.op x) 1).trans ?_
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring S
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module S M₃
σ✝ : R →+* S
fₗ gₗ : M →ₗ[R] M₂
f✝ g✝ : M →ₛₗ[σ✝] M₃
σ : Rᵐᵒᵖ →+* S
f g : R →ₛₗ[σ] M₃
h : ↑f 1 = ↑g 1
x : R
⊢ ↑σ (MulOpposite.op x) • ↑f 1 = ↑g (MulOpposite.op x • 1)
[PROOFSTEP]
rw [h]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring S
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module S M₃
σ✝ : R →+* S
fₗ gₗ : M →ₗ[R] M₂
f✝ g✝ : M →ₛₗ[σ✝] M₃
σ : Rᵐᵒᵖ →+* S
f g : R →ₛₗ[σ] M₃
h : ↑f 1 = ↑g 1
x : R
⊢ ↑σ (MulOpposite.op x) • ↑g 1 = ↑g (MulOpposite.op x • 1)
[PROOFSTEP]
exact (g.map_smulₛₗ (MulOpposite.op x) 1).symm
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝⁹ : Semiring R
inst✝⁸ : Semiring S
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M
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₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₂] M₂
⊢ ∀ (x y : M₁), (↑f ∘ ↑g) (x + y) = (↑f ∘ ↑g) x + (↑f ∘ ↑g) y
[PROOFSTEP]
simp only [map_add, forall_const, Function.comp_apply]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝⁹ : Semiring R
inst✝⁸ : Semiring S
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M
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₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₂] M₂
r : R₁
x : M₁
⊢ AddHom.toFun { toFun := ↑f ∘ ↑g, map_add' := (_ : ∀ (a a_1 : M₁), ↑f (↑g (a + a_1)) = ↑f (↑g a) + ↑f (↑g a_1)) }
      (r • x) =
    ↑σ₁₃ r •
      AddHom.toFun { toFun := ↑f ∘ ↑g, map_add' := (_ : ∀ (a a_1 : M₁), ↑f (↑g (a + a_1)) = ↑f (↑g a) + ↑f (↑g a_1)) } x
[PROOFSTEP]
simp only [Function.comp_apply, map_smulₛₗ, RingHomCompTriple.comp_apply]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝⁹ : Semiring R
inst✝⁸ : Semiring S
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M
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₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₂] M₂
f' : M₂ →ₛₗ[σ₂₃] M₃
g' : M₁ →ₛₗ[σ₁₂] M₂
hf : Injective ↑f
h : comp f g = comp f g'
x : M₁
⊢ ↑f (↑g x) = ↑f (↑g' x)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module S M₂
σ : R →+* S
σ' : S →+* R
inst✝ : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ → M
h₁ : LeftInverse g ↑f
h₂ : Function.RightInverse g ↑f
⊢ M₂ →ₛₗ[σ'] M
[PROOFSTEP]
dsimp [LeftInverse, Function.RightInverse] at h₁ h₂ 
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module S M₂
σ : R →+* S
σ' : S →+* R
inst✝ : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ → M
h₁ : ∀ (x : M), g (↑f x) = x
h₂ : ∀ (x : M₂), ↑f (g x) = x
⊢ M₂ →ₛₗ[σ'] M
[PROOFSTEP]
exact
  { toFun := g
    map_add' := fun x y ↦ by rw [← h₁ (g (x + y)), ← h₁ (g x + g y)]; simp [h₂]
    map_smul' := fun a b ↦ by
      dsimp only
      rw [← h₁ (g (a • b)), ← h₁ (σ' a • g b)]
      simp [h₂] }
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module S M₂
σ : R →+* S
σ' : S →+* R
inst✝ : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ → M
h₁ : ∀ (x : M), g (↑f x) = x
h₂ : ∀ (x : M₂), ↑f (g x) = x
x y : M₂
⊢ g (x + y) = g x + g y
[PROOFSTEP]
rw [← h₁ (g (x + y)), ← h₁ (g x + g y)]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module S M₂
σ : R →+* S
σ' : S →+* R
inst✝ : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ → M
h₁ : ∀ (x : M), g (↑f x) = x
h₂ : ∀ (x : M₂), ↑f (g x) = x
x y : M₂
⊢ g (↑f (g (x + y))) = g (↑f (g x + g y))
[PROOFSTEP]
simp [h₂]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module S M₂
σ : R →+* S
σ' : S →+* R
inst✝ : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ → M
h₁ : ∀ (x : M), g (↑f x) = x
h₂ : ∀ (x : M₂), ↑f (g x) = x
a : S
b : M₂
⊢ AddHom.toFun { toFun := g, map_add' := (_ : ∀ (x y : M₂), g (x + y) = g x + g y) } (a • b) =
    ↑σ' a • AddHom.toFun { toFun := g, map_add' := (_ : ∀ (x y : M₂), g (x + y) = g x + g y) } b
[PROOFSTEP]
dsimp only
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module S M₂
σ : R →+* S
σ' : S →+* R
inst✝ : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ → M
h₁ : ∀ (x : M), g (↑f x) = x
h₂ : ∀ (x : M₂), ↑f (g x) = x
a : S
b : M₂
⊢ g (a • b) = ↑σ' a • g b
[PROOFSTEP]
rw [← h₁ (g (a • b)), ← h₁ (σ' a • g b)]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module S M₂
σ : R →+* S
σ' : S →+* R
inst✝ : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ → M
h₁ : ∀ (x : M), g (↑f x) = x
h₂ : ∀ (x : M₂), ↑f (g x) = x
a : S
b : M₂
⊢ g (↑f (g (a • b))) = g (↑f (↑σ' a • g b))
[PROOFSTEP]
simp [h₂]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S✝ : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
module_M : Module R M
module_M₂ : Module S✝ M₂
σ : R →+* S✝
f : M →ₛₗ[σ] M₂
S : Type u_17
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : Module S M₂
fₗ : M →ₗ[S] M₂
c : ℤ
x : M
⊢ ↑fₗ (c • x) = c • ↑fₗ x
[PROOFSTEP]
induction c using Int.induction_on
[GOAL]
case hz
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S✝ : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
module_M : Module R M
module_M₂ : Module S✝ M₂
σ : R →+* S✝
f : M →ₛₗ[σ] M₂
S : Type u_17
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : Module S M₂
fₗ : M →ₗ[S] M₂
x : M
⊢ ↑fₗ (0 • x) = 0 • ↑fₗ x
case hp
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S✝ : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
module_M : Module R M
module_M₂ : Module S✝ M₂
σ : R →+* S✝
f : M →ₛₗ[σ] M₂
S : Type u_17
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : Module S M₂
fₗ : M →ₗ[S] M₂
x : M
i✝ : ℕ
a✝ : ↑fₗ (↑i✝ • x) = ↑i✝ • ↑fₗ x
⊢ ↑fₗ ((↑i✝ + 1) • x) = (↑i✝ + 1) • ↑fₗ x
case hn
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S✝ : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
module_M : Module R M
module_M₂ : Module S✝ M₂
σ : R →+* S✝
f : M →ₛₗ[σ] M₂
S : Type u_17
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : Module S M₂
fₗ : M →ₗ[S] M₂
x : M
i✝ : ℕ
a✝ : ↑fₗ (-↑i✝ • x) = -↑i✝ • ↑fₗ x
⊢ ↑fₗ ((-↑i✝ - 1) • x) = (-↑i✝ - 1) • ↑fₗ x
[PROOFSTEP]
case hz => simp
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S✝ : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
module_M : Module R M
module_M₂ : Module S✝ M₂
σ : R →+* S✝
f : M →ₛₗ[σ] M₂
S : Type u_17
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : Module S M₂
fₗ : M →ₗ[S] M₂
x : M
⊢ ↑fₗ (0 • x) = 0 • ↑fₗ x
[PROOFSTEP]
case hz => simp
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S✝ : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
module_M : Module R M
module_M₂ : Module S✝ M₂
σ : R →+* S✝
f : M →ₛₗ[σ] M₂
S : Type u_17
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : Module S M₂
fₗ : M →ₗ[S] M₂
x : M
⊢ ↑fₗ (0 • x) = 0 • ↑fₗ x
[PROOFSTEP]
simp
[GOAL]
case hp
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S✝ : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
module_M : Module R M
module_M₂ : Module S✝ M₂
σ : R →+* S✝
f : M →ₛₗ[σ] M₂
S : Type u_17
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : Module S M₂
fₗ : M →ₗ[S] M₂
x : M
i✝ : ℕ
a✝ : ↑fₗ (↑i✝ • x) = ↑i✝ • ↑fₗ x
⊢ ↑fₗ ((↑i✝ + 1) • x) = (↑i✝ + 1) • ↑fₗ x
case hn
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S✝ : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
module_M : Module R M
module_M₂ : Module S✝ M₂
σ : R →+* S✝
f : M →ₛₗ[σ] M₂
S : Type u_17
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : Module S M₂
fₗ : M →ₗ[S] M₂
x : M
i✝ : ℕ
a✝ : ↑fₗ (-↑i✝ • x) = -↑i✝ • ↑fₗ x
⊢ ↑fₗ ((-↑i✝ - 1) • x) = (-↑i✝ - 1) • ↑fₗ x
[PROOFSTEP]
case hp n ih => simp [add_smul, ih]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S✝ : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
module_M : Module R M
module_M₂ : Module S✝ M₂
σ : R →+* S✝
f : M →ₛₗ[σ] M₂
S : Type u_17
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : Module S M₂
fₗ : M →ₗ[S] M₂
x : M
n : ℕ
ih : ↑fₗ (↑n • x) = ↑n • ↑fₗ x
⊢ ↑fₗ ((↑n + 1) • x) = (↑n + 1) • ↑fₗ x
[PROOFSTEP]
case hp n ih => simp [add_smul, ih]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S✝ : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
module_M : Module R M
module_M₂ : Module S✝ M₂
σ : R →+* S✝
f : M →ₛₗ[σ] M₂
S : Type u_17
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : Module S M₂
fₗ : M →ₗ[S] M₂
x : M
n : ℕ
ih : ↑fₗ (↑n • x) = ↑n • ↑fₗ x
⊢ ↑fₗ ((↑n + 1) • x) = (↑n + 1) • ↑fₗ x
[PROOFSTEP]
simp [add_smul, ih]
[GOAL]
case hn
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S✝ : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
module_M : Module R M
module_M₂ : Module S✝ M₂
σ : R →+* S✝
f : M →ₛₗ[σ] M₂
S : Type u_17
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : Module S M₂
fₗ : M →ₗ[S] M₂
x : M
i✝ : ℕ
a✝ : ↑fₗ (-↑i✝ • x) = -↑i✝ • ↑fₗ x
⊢ ↑fₗ ((-↑i✝ - 1) • x) = (-↑i✝ - 1) • ↑fₗ x
[PROOFSTEP]
case hn n ih => simp [sub_smul, ih]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S✝ : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
module_M : Module R M
module_M₂ : Module S✝ M₂
σ : R →+* S✝
f : M →ₛₗ[σ] M₂
S : Type u_17
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : Module S M₂
fₗ : M →ₗ[S] M₂
x : M
n : ℕ
ih : ↑fₗ (-↑n • x) = -↑n • ↑fₗ x
⊢ ↑fₗ ((-↑n - 1) • x) = (-↑n - 1) • ↑fₗ x
[PROOFSTEP]
case hn n ih => simp [sub_smul, ih]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S✝ : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
module_M : Module R M
module_M₂ : Module S✝ M₂
σ : R →+* S✝
f : M →ₛₗ[σ] M₂
S : Type u_17
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : Module S M₂
fₗ : M →ₗ[S] M₂
x : M
n : ℕ
ih : ↑fₗ (-↑n • x) = -↑n • ↑fₗ x
⊢ ↑fₗ ((-↑n - 1) • x) = (-↑n - 1) • ↑fₗ x
[PROOFSTEP]
simp [sub_smul, ih]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
f g : M →+[R] M₂
h : ↑f = ↑g
⊢ f = g
[PROOFSTEP]
ext m
[GOAL]
case a
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
f g : M →+[R] M₂
h : ↑f = ↑g
m : M
⊢ ↑f m = ↑g m
[PROOFSTEP]
exact LinearMap.congr_fun h m
[GOAL]
R✝ : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M✝ : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R✝ M✝
inst✝³ : Module R✝ M₂
R : Type u_17
M : Type u_18
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c : R
⊢ IsLinearMap R fun z => c • z
[PROOFSTEP]
refine' IsLinearMap.mk (smul_add c) _
[GOAL]
R✝ : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M✝ : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R✝ M✝
inst✝³ : Module R✝ M₂
R : Type u_17
M : Type u_18
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c : R
⊢ ∀ (c_1 : R) (x : M), c • c_1 • x = c_1 • c • x
[PROOFSTEP]
intro _ _
[GOAL]
R✝ : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M✝ : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R✝ M✝
inst✝³ : Module R✝ M₂
R : Type u_17
M : Type u_18
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c c✝ : R
x✝ : M
⊢ c • c✝ • x✝ = c✝ • c • x✝
[PROOFSTEP]
simp only [smul_smul, mul_comm]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
⊢ Injective toNatLinearMap
[PROOFSTEP]
intro f g h
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
f g : M →+ M₂
h : toNatLinearMap f = toNatLinearMap g
⊢ f = g
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
f g : M →+ M₂
h : toNatLinearMap f = toNatLinearMap g
x : M
⊢ ↑f x = ↑g x
[PROOFSTEP]
exact LinearMap.congr_fun h x
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup M₂
⊢ Injective toIntLinearMap
[PROOFSTEP]
intro f g h
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup M₂
f g : M →+ M₂
h : toIntLinearMap f = toIntLinearMap g
⊢ f = g
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup M₂
f g : M →+ M₂
h : toIntLinearMap f = toIntLinearMap g
x : M
⊢ ↑f x = ↑g x
[PROOFSTEP]
exact LinearMap.congr_fun h x
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝³ : AddCommGroup M
inst✝² : Module ℚ M
inst✝¹ : AddCommGroup M₂
inst✝ : Module ℚ M₂
⊢ Injective toRatLinearMap
[PROOFSTEP]
intro f g h
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝³ : AddCommGroup M
inst✝² : Module ℚ M
inst✝¹ : AddCommGroup M₂
inst✝ : Module ℚ M₂
f g : M →+ M₂
h : toRatLinearMap f = toRatLinearMap g
⊢ f = g
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝³ : AddCommGroup M
inst✝² : Module ℚ M
inst✝¹ : AddCommGroup M₂
inst✝ : Module ℚ M₂
f g : M →+ M₂
h : toRatLinearMap f = toRatLinearMap g
x : M
⊢ ↑f x = ↑g x
[PROOFSTEP]
exact LinearMap.congr_fun h x
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹⁸ : Semiring R
inst✝¹⁷ : Semiring R₂
inst✝¹⁶ : Semiring R₃
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid M₂
inst✝¹³ : AddCommMonoid M₃
inst✝¹² : Module R M
inst✝¹¹ : Module R₂ M₂
inst✝¹⁰ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝⁹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝⁸ : Monoid S
inst✝⁷ : DistribMulAction S M₂
inst✝⁶ : SMulCommClass R₂ S M₂
inst✝⁵ : Monoid S₃
inst✝⁴ : DistribMulAction S₃ M₃
inst✝³ : SMulCommClass R₃ S₃ M₃
inst✝² : Monoid T
inst✝¹ : DistribMulAction T M₂
inst✝ : SMulCommClass R₂ T M₂
a : S
f : M →ₛₗ[σ₁₂] M₂
x y : M
⊢ (a • ↑f) (x + y) = (a • ↑f) x + (a • ↑f) y
[PROOFSTEP]
simp only [Pi.smul_apply, f.map_add, smul_add]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝¹⁸ : Semiring R
inst✝¹⁷ : Semiring R₂
inst✝¹⁶ : Semiring R₃
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid M₂
inst✝¹³ : AddCommMonoid M₃
inst✝¹² : Module R M
inst✝¹¹ : Module R₂ M₂
inst✝¹⁰ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝⁹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝⁸ : Monoid S
inst✝⁷ : DistribMulAction S M₂
inst✝⁶ : SMulCommClass R₂ S M₂
inst✝⁵ : Monoid S₃
inst✝⁴ : DistribMulAction S₃ M₃
inst✝³ : SMulCommClass R₃ S₃ M₃
inst✝² : Monoid T
inst✝¹ : DistribMulAction T M₂
inst✝ : SMulCommClass R₂ T M₂
a : S
f : M →ₛₗ[σ₁₂] M₂
c : R
x : M
⊢ AddHom.toFun { toFun := a • ↑f, map_add' := (_ : ∀ (x y : M), a • ↑f (x + y) = a • ↑f x + a • ↑f y) } (c • x) =
    ↑σ₁₂ c • AddHom.toFun { toFun := a • ↑f, map_add' := (_ : ∀ (x y : M), a • ↑f (x + y) = a • ↑f x + a • ↑f y) } x
[PROOFSTEP]
simp [Pi.smul_apply, smul_comm]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
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✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R₁ M
inst✝⁵ : Module R₂ M₂
inst✝⁴ : Module R₃ M₃
inst✝³ : Module R₁ N₁
inst✝² : Module R₂ N₂
inst✝¹ : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
⊢ ∀ (x y : M), OfNat.ofNat 0 (x + y) = OfNat.ofNat 0 x + OfNat.ofNat 0 y
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
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✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R₁ M
inst✝⁵ : Module R₂ M₂
inst✝⁴ : Module R₃ M₃
inst✝³ : Module R₁ N₁
inst✝² : Module R₂ N₂
inst✝¹ : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
⊢ ∀ (r : R₁) (x : M),
    AddHom.toFun { toFun := 0, map_add' := (_ : M → M → 0 = 0 + 0) } (r • x) =
      ↑σ₁₂ r • AddHom.toFun { toFun := 0, map_add' := (_ : M → M → 0 = 0 + 0) } x
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
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✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R₁ M
inst✝⁵ : Module R₂ M₂
inst✝⁴ : Module R₃ M₃
inst✝³ : Module R₁ N₁
inst✝² : Module R₂ N₂
inst✝¹ : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
g : M₂ →ₛₗ[σ₂₃] M₃
c : M
⊢ ↑(comp g 0) c = ↑0 c
[PROOFSTEP]
rw [comp_apply, zero_apply, zero_apply, g.map_zero]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
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✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R₁ M
inst✝⁵ : Module R₂ M₂
inst✝⁴ : Module R₃ M₃
inst✝³ : Module R₁ N₁
inst✝² : Module R₂ N₂
inst✝¹ : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f g : M →ₛₗ[σ₁₂] M₂
⊢ ∀ (x y : M), (↑f + ↑g) (x + y) = (↑f + ↑g) x + (↑f + ↑g) y
[PROOFSTEP]
simp [add_comm, add_left_comm]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
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✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R₁ M
inst✝⁵ : Module R₂ M₂
inst✝⁴ : Module R₃ M₃
inst✝³ : Module R₁ N₁
inst✝² : Module R₂ N₂
inst✝¹ : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f g : M →ₛₗ[σ₁₂] M₂
⊢ ∀ (r : R₁) (x : M),
    AddHom.toFun
        { toFun := ↑f + ↑g,
          map_add' := (_ : ∀ (a a_1 : M), ↑f (a + a_1) + ↑g (a + a_1) = ↑f a + ↑g a + (↑f a_1 + ↑g a_1)) }
        (r • x) =
      ↑σ₁₂ r •
        AddHom.toFun
          { toFun := ↑f + ↑g,
            map_add' := (_ : ∀ (a a_1 : M), ↑f (a + a_1) + ↑g (a + a_1) = ↑f a + ↑g a + (↑f a_1 + ↑g a_1)) }
          x
[PROOFSTEP]
simp [smul_add]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
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✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R₁ M
inst✝⁵ : Module R₂ M₂
inst✝⁴ : Module R₃ M₃
inst✝³ : Module R₁ N₁
inst✝² : Module R₂ N₂
inst✝¹ : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M →ₛₗ[σ₁₂] N₂
⊢ ∀ (x y : M), (-↑f) (x + y) = (-↑f) x + (-↑f) y
[PROOFSTEP]
simp [add_comm]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
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✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R₁ M
inst✝⁵ : Module R₂ M₂
inst✝⁴ : Module R₃ M₃
inst✝³ : Module R₁ N₁
inst✝² : Module R₂ N₂
inst✝¹ : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M →ₛₗ[σ₁₂] N₂
⊢ ∀ (r : R₁) (x : M),
    AddHom.toFun { toFun := -↑f, map_add' := (_ : ∀ (a a_1 : M), -↑f (a + a_1) = -↑f a + -↑f a_1) } (r • x) =
      ↑σ₁₂ r • AddHom.toFun { toFun := -↑f, map_add' := (_ : ∀ (a a_1 : M), -↑f (a + a_1) = -↑f a + -↑f a_1) } x
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
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✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R₁ M
inst✝⁵ : Module R₂ M₂
inst✝⁴ : Module R₃ M₃
inst✝³ : Module R₁ N₁
inst✝² : Module R₂ N₂
inst✝¹ : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f g : M →ₛₗ[σ₁₂] N₂
x y : M
⊢ (↑f - ↑g) (x + y) = (↑f - ↑g) x + (↑f - ↑g) y
[PROOFSTEP]
simp only [Pi.sub_apply, map_add, add_sub_add_comm]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
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✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R₁ M
inst✝⁵ : Module R₂ M₂
inst✝⁴ : Module R₃ M₃
inst✝³ : Module R₁ N₁
inst✝² : Module R₂ N₂
inst✝¹ : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f g : M →ₛₗ[σ₁₂] N₂
r : R₁
x : M
⊢ AddHom.toFun
      { toFun := ↑f - ↑g, map_add' := (_ : ∀ (x y : M), ↑f (x + y) - ↑g (x + y) = ↑f x - ↑g x + (↑f y - ↑g y)) }
      (r • x) =
    ↑σ₁₂ r •
      AddHom.toFun
        { toFun := ↑f - ↑g, map_add' := (_ : ∀ (x y : M), ↑f (x + y) - ↑g (x + y) = ↑f x - ↑g x + (↑f y - ↑g y)) } x
[PROOFSTEP]
simp [Pi.sub_apply, map_smul, smul_sub]
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R M
inst✝³ : Module R N₁
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass R S M
f : Module.End R M
h : IsUnit f
x : M
⊢ ↑(f * (IsUnit.unit h).inv) x = x
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
k : Type u_5
S : Type u_6
S₃ : Type u_7
T : Type u_8
M : Type u_9
M₁ : Type u_10
M₂ : Type u_11
M₃ : Type u_12
N₁ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
ι : Type u_16
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R M
inst✝³ : Module R N₁
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass R S M
f : Module.End R M
h : IsUnit f
x : M
⊢ ↑((IsUnit.unit h).inv * f) x = x
[PROOFSTEP]
simp
