[GOAL]
R : Type u_1
inst✝³² : Semiring R
S : Type u_2
inst✝³¹ : Semiring S
R₂ : Type u_3
inst✝³⁰ : Semiring R₂
S₂ : Type u_4
inst✝²⁹ : Semiring S₂
M : Type u_5
N : Type u_6
P : Type u_7
M₂ : Type u_8
N₂ : Type u_9
P₂ : Type u_10
Nₗ : Type u_11
Pₗ : Type u_12
M' : Type u_13
N' : Type u_14
P' : Type u_15
inst✝²⁸ : AddCommMonoid M
inst✝²⁷ : AddCommMonoid N
inst✝²⁶ : AddCommMonoid P
inst✝²⁵ : AddCommMonoid M₂
inst✝²⁴ : AddCommMonoid N₂
inst✝²³ : AddCommMonoid P₂
inst✝²² : AddCommMonoid Nₗ
inst✝²¹ : AddCommMonoid Pₗ
inst✝²⁰ : AddCommGroup M'
inst✝¹⁹ : AddCommGroup N'
inst✝¹⁸ : AddCommGroup P'
inst✝¹⁷ : Module R M
inst✝¹⁶ : Module S N
inst✝¹⁵ : Module R₂ P
inst✝¹⁴ : Module S₂ P
inst✝¹³ : Module R M₂
inst✝¹² : Module S N₂
inst✝¹¹ : Module R P₂
inst✝¹⁰ : Module S₂ P₂
inst✝⁹ : Module R Pₗ
inst✝⁸ : Module S Pₗ
inst✝⁷ : Module R M'
inst✝⁶ : Module S N'
inst✝⁵ : Module R₂ P'
inst✝⁴ : Module S₂ P'
inst✝³ : SMulCommClass S₂ R₂ P
inst✝² : SMulCommClass S R Pₗ
inst✝¹ : SMulCommClass S₂ R₂ P'
inst✝ : SMulCommClass S₂ R P₂
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
n : N
m₁ m₂ : M
⊢ (fun n m => ↑(↑f m) n) n (m₁ + m₂) = (fun n m => ↑(↑f m) n) n m₁ + (fun n m => ↑(↑f m) n) n m₂
[PROOFSTEP]
simp only [map_add, add_apply]
[GOAL]
R : Type u_1
inst✝³² : Semiring R
S : Type u_2
inst✝³¹ : Semiring S
R₂ : Type u_3
inst✝³⁰ : Semiring R₂
S₂ : Type u_4
inst✝²⁹ : Semiring S₂
M : Type u_5
N : Type u_6
P : Type u_7
M₂ : Type u_8
N₂ : Type u_9
P₂ : Type u_10
Nₗ : Type u_11
Pₗ : Type u_12
M' : Type u_13
N' : Type u_14
P' : Type u_15
inst✝²⁸ : AddCommMonoid M
inst✝²⁷ : AddCommMonoid N
inst✝²⁶ : AddCommMonoid P
inst✝²⁵ : AddCommMonoid M₂
inst✝²⁴ : AddCommMonoid N₂
inst✝²³ : AddCommMonoid P₂
inst✝²² : AddCommMonoid Nₗ
inst✝²¹ : AddCommMonoid Pₗ
inst✝²⁰ : AddCommGroup M'
inst✝¹⁹ : AddCommGroup N'
inst✝¹⁸ : AddCommGroup P'
inst✝¹⁷ : Module R M
inst✝¹⁶ : Module S N
inst✝¹⁵ : Module R₂ P
inst✝¹⁴ : Module S₂ P
inst✝¹³ : Module R M₂
inst✝¹² : Module S N₂
inst✝¹¹ : Module R P₂
inst✝¹⁰ : Module S₂ P₂
inst✝⁹ : Module R Pₗ
inst✝⁸ : Module S Pₗ
inst✝⁷ : Module R M'
inst✝⁶ : Module S N'
inst✝⁵ : Module R₂ P'
inst✝⁴ : Module S₂ P'
inst✝³ : SMulCommClass S₂ R₂ P
inst✝² : SMulCommClass S R Pₗ
inst✝¹ : SMulCommClass S₂ R₂ P'
inst✝ : SMulCommClass S₂ R P₂
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
c : R
n : N
m : M
⊢ (fun n m => ↑(↑f m) n) n (c • m) = ↑ρ₁₂ c • (fun n m => ↑(↑f m) n) n m
[PROOFSTEP]
simp only [map_smulₛₗ, smul_apply]
[GOAL]
R : Type u_1
inst✝³² : Semiring R
S : Type u_2
inst✝³¹ : Semiring S
R₂ : Type u_3
inst✝³⁰ : Semiring R₂
S₂ : Type u_4
inst✝²⁹ : Semiring S₂
M : Type u_5
N : Type u_6
P : Type u_7
M₂ : Type u_8
N₂ : Type u_9
P₂ : Type u_10
Nₗ : Type u_11
Pₗ : Type u_12
M' : Type u_13
N' : Type u_14
P' : Type u_15
inst✝²⁸ : AddCommMonoid M
inst✝²⁷ : AddCommMonoid N
inst✝²⁶ : AddCommMonoid P
inst✝²⁵ : AddCommMonoid M₂
inst✝²⁴ : AddCommMonoid N₂
inst✝²³ : AddCommMonoid P₂
inst✝²² : AddCommMonoid Nₗ
inst✝²¹ : AddCommMonoid Pₗ
inst✝²⁰ : AddCommGroup M'
inst✝¹⁹ : AddCommGroup N'
inst✝¹⁸ : AddCommGroup P'
inst✝¹⁷ : Module R M
inst✝¹⁶ : Module S N
inst✝¹⁵ : Module R₂ P
inst✝¹⁴ : Module S₂ P
inst✝¹³ : Module R M₂
inst✝¹² : Module S N₂
inst✝¹¹ : Module R P₂
inst✝¹⁰ : Module S₂ P₂
inst✝⁹ : Module R Pₗ
inst✝⁸ : Module S Pₗ
inst✝⁷ : Module R M'
inst✝⁶ : Module S N'
inst✝⁵ : Module R₂ P'
inst✝⁴ : Module S₂ P'
inst✝³ : SMulCommClass S₂ R₂ P
inst✝² : SMulCommClass S R Pₗ
inst✝¹ : SMulCommClass S₂ R₂ P'
inst✝ : SMulCommClass S₂ R P₂
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
H : flip f = flip g
m : M
n : N
⊢ ↑(↑(flip f) n) m = ↑(↑(flip g) n) m
[PROOFSTEP]
rw [H]
[GOAL]
R : Type u_1
inst✝³² : Semiring R
S : Type u_2
inst✝³¹ : Semiring S
R₂ : Type u_3
inst✝³⁰ : Semiring R₂
S₂ : Type u_4
inst✝²⁹ : Semiring S₂
M : Type u_5
N : Type u_6
P : Type u_7
M₂ : Type u_8
N₂ : Type u_9
P₂ : Type u_10
Nₗ : Type u_11
Pₗ : Type u_12
M' : Type u_13
N' : Type u_14
P' : Type u_15
inst✝²⁸ : AddCommMonoid M
inst✝²⁷ : AddCommMonoid N
inst✝²⁶ : AddCommMonoid P
inst✝²⁵ : AddCommMonoid M₂
inst✝²⁴ : AddCommMonoid N₂
inst✝²³ : AddCommMonoid P₂
inst✝²² : AddCommMonoid Nₗ
inst✝²¹ : AddCommMonoid Pₗ
inst✝²⁰ : AddCommGroup M'
inst✝¹⁹ : AddCommGroup N'
inst✝¹⁸ : AddCommGroup P'
inst✝¹⁷ : Module R M
inst✝¹⁶ : Module S N
inst✝¹⁵ : Module R₂ P
inst✝¹⁴ : Module S₂ P
inst✝¹³ : Module R M₂
inst✝¹² : Module S N₂
inst✝¹¹ : Module R P₂
inst✝¹⁰ : Module S₂ P₂
inst✝⁹ : Module R Pₗ
inst✝⁸ : Module S Pₗ
inst✝⁷ : Module R M'
inst✝⁶ : Module S N'
inst✝⁵ : Module R₂ P'
inst✝⁴ : Module S₂ P'
inst✝³ : SMulCommClass S₂ R₂ P
inst✝² : SMulCommClass S R Pₗ
inst✝¹ : SMulCommClass S₂ R₂ P'
inst✝ : SMulCommClass S₂ R P₂
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
q : Submodule S N
m₁ m₂ : M
x✝ : { x // x ∈ q }
⊢ ↑((fun m => domRestrict (↑f m) q) (m₁ + m₂)) x✝ =
    ↑((fun m => domRestrict (↑f m) q) m₁ + (fun m => domRestrict (↑f m) q) m₂) x✝
[PROOFSTEP]
simp only [map_add, domRestrict_apply, add_apply]
[GOAL]
R : Type u_1
inst✝³² : Semiring R
S : Type u_2
inst✝³¹ : Semiring S
R₂ : Type u_3
inst✝³⁰ : Semiring R₂
S₂ : Type u_4
inst✝²⁹ : Semiring S₂
M : Type u_5
N : Type u_6
P : Type u_7
M₂ : Type u_8
N₂ : Type u_9
P₂ : Type u_10
Nₗ : Type u_11
Pₗ : Type u_12
M' : Type u_13
N' : Type u_14
P' : Type u_15
inst✝²⁸ : AddCommMonoid M
inst✝²⁷ : AddCommMonoid N
inst✝²⁶ : AddCommMonoid P
inst✝²⁵ : AddCommMonoid M₂
inst✝²⁴ : AddCommMonoid N₂
inst✝²³ : AddCommMonoid P₂
inst✝²² : AddCommMonoid Nₗ
inst✝²¹ : AddCommMonoid Pₗ
inst✝²⁰ : AddCommGroup M'
inst✝¹⁹ : AddCommGroup N'
inst✝¹⁸ : AddCommGroup P'
inst✝¹⁷ : Module R M
inst✝¹⁶ : Module S N
inst✝¹⁵ : Module R₂ P
inst✝¹⁴ : Module S₂ P
inst✝¹³ : Module R M₂
inst✝¹² : Module S N₂
inst✝¹¹ : Module R P₂
inst✝¹⁰ : Module S₂ P₂
inst✝⁹ : Module R Pₗ
inst✝⁸ : Module S Pₗ
inst✝⁷ : Module R M'
inst✝⁶ : Module S N'
inst✝⁵ : Module R₂ P'
inst✝⁴ : Module S₂ P'
inst✝³ : SMulCommClass S₂ R₂ P
inst✝² : SMulCommClass S R Pₗ
inst✝¹ : SMulCommClass S₂ R₂ P'
inst✝ : SMulCommClass S₂ R P₂
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
q : Submodule S N
c : R
m : M
x✝ : { x // x ∈ q }
⊢ ↑(AddHom.toFun
          { toFun := fun m => domRestrict (↑f m) q,
            map_add' :=
              (_ :
                ∀ (m₁ m₂ : M),
                  (fun m => domRestrict (↑f m) q) (m₁ + m₂) =
                    (fun m => domRestrict (↑f m) q) m₁ + (fun m => domRestrict (↑f m) q) m₂) }
          (c • m))
      x✝ =
    ↑(↑ρ₁₂ c •
          AddHom.toFun
            { toFun := fun m => domRestrict (↑f m) q,
              map_add' :=
                (_ :
                  ∀ (m₁ m₂ : M),
                    (fun m => domRestrict (↑f m) q) (m₁ + m₂) =
                      (fun m => domRestrict (↑f m) q) m₁ + (fun m => domRestrict (↑f m) q) m₂) }
            m)
      x✝
[PROOFSTEP]
simp only [f.map_smulₛₗ, domRestrict_apply, smul_apply]
[GOAL]
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type u_2
inst✝²² : CommSemiring R₂
R₃ : Type u_3
inst✝²¹ : CommSemiring R₃
R₄ : Type u_4
inst✝²⁰ : CommSemiring R₄
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
⊢ compl₂ f id = f
[PROOFSTEP]
ext
[GOAL]
case h.h
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type u_2
inst✝²² : CommSemiring R₂
R₃ : Type u_3
inst✝²¹ : CommSemiring R₃
R₄ : Type u_4
inst✝²⁰ : CommSemiring R₄
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
x✝¹ : M
x✝ : N
⊢ ↑(↑(compl₂ f id) x✝¹) x✝ = ↑(↑f x✝¹) x✝
[PROOFSTEP]
rw [compl₂_apply, id_coe, id.def]
[GOAL]
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type u_2
inst✝²² : CommSemiring R₂
R₃ : Type u_3
inst✝²¹ : CommSemiring R₃
R₄ : Type u_4
inst✝²⁰ : CommSemiring R₄
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f✝ : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
⊢ compl₁₂ f id id = f
[PROOFSTEP]
ext
[GOAL]
case h.h
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type u_2
inst✝²² : CommSemiring R₂
R₃ : Type u_3
inst✝²¹ : CommSemiring R₃
R₄ : Type u_4
inst✝²⁰ : CommSemiring R₄
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f✝ : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
x✝¹ : Mₗ
x✝ : Nₗ
⊢ ↑(↑(compl₁₂ f id id) x✝¹) x✝ = ↑(↑f x✝¹) x✝
[PROOFSTEP]
simp_rw [compl₁₂_apply, id_coe, id.def]
[GOAL]
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type u_2
inst✝²² : CommSemiring R₂
R₃ : Type u_3
inst✝²¹ : CommSemiring R₃
R₄ : Type u_4
inst✝²⁰ : CommSemiring R₄
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
⊢ compl₁₂ f₁ g g' = compl₁₂ f₂ g g' ↔ f₁ = f₂
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type u_2
inst✝²² : CommSemiring R₂
R₃ : Type u_3
inst✝²¹ : CommSemiring R₃
R₄ : Type u_4
inst✝²⁰ : CommSemiring R₄
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
⊢ compl₁₂ f₁ g g' = compl₁₂ f₂ g g' → f₁ = f₂
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type u_2
inst✝²² : CommSemiring R₂
R₃ : Type u_3
inst✝²¹ : CommSemiring R₃
R₄ : Type u_4
inst✝²⁰ : CommSemiring R₄
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
⊢ f₁ = f₂ → compl₁₂ f₁ g g' = compl₁₂ f₂ g g'
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type u_2
inst✝²² : CommSemiring R₂
R₃ : Type u_3
inst✝²¹ : CommSemiring R₃
R₄ : Type u_4
inst✝²⁰ : CommSemiring R₄
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
h : compl₁₂ f₁ g g' = compl₁₂ f₂ g g'
⊢ f₁ = f₂
[PROOFSTEP]
ext x y
[GOAL]
case mp.h.h
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type u_2
inst✝²² : CommSemiring R₂
R₃ : Type u_3
inst✝²¹ : CommSemiring R₃
R₄ : Type u_4
inst✝²⁰ : CommSemiring R₄
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
h : compl₁₂ f₁ g g' = compl₁₂ f₂ g g'
x : Mₗ
y : Nₗ
⊢ ↑(↑f₁ x) y = ↑(↑f₂ x) y
[PROOFSTEP]
cases' hₗ x with x' hx
[GOAL]
case mp.h.h.intro
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type u_2
inst✝²² : CommSemiring R₂
R₃ : Type u_3
inst✝²¹ : CommSemiring R₃
R₄ : Type u_4
inst✝²⁰ : CommSemiring R₄
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
h : compl₁₂ f₁ g g' = compl₁₂ f₂ g g'
x : Mₗ
y : Nₗ
x' : Qₗ
hx : ↑g x' = x
⊢ ↑(↑f₁ x) y = ↑(↑f₂ x) y
[PROOFSTEP]
subst hx
[GOAL]
case mp.h.h.intro
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type u_2
inst✝²² : CommSemiring R₂
R₃ : Type u_3
inst✝²¹ : CommSemiring R₃
R₄ : Type u_4
inst✝²⁰ : CommSemiring R₄
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
h : compl₁₂ f₁ g g' = compl₁₂ f₂ g g'
y : Nₗ
x' : Qₗ
⊢ ↑(↑f₁ (↑g x')) y = ↑(↑f₂ (↑g x')) y
[PROOFSTEP]
cases' hᵣ y with y' hy
[GOAL]
case mp.h.h.intro.intro
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type u_2
inst✝²² : CommSemiring R₂
R₃ : Type u_3
inst✝²¹ : CommSemiring R₃
R₄ : Type u_4
inst✝²⁰ : CommSemiring R₄
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
h : compl₁₂ f₁ g g' = compl₁₂ f₂ g g'
y : Nₗ
x' : Qₗ
y' : Qₗ'
hy : ↑g' y' = y
⊢ ↑(↑f₁ (↑g x')) y = ↑(↑f₂ (↑g x')) y
[PROOFSTEP]
subst hy
[GOAL]
case mp.h.h.intro.intro
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type u_2
inst✝²² : CommSemiring R₂
R₃ : Type u_3
inst✝²¹ : CommSemiring R₃
R₄ : Type u_4
inst✝²⁰ : CommSemiring R₄
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
h : compl₁₂ f₁ g g' = compl₁₂ f₂ g g'
x' : Qₗ
y' : Qₗ'
⊢ ↑(↑f₁ (↑g x')) (↑g' y') = ↑(↑f₂ (↑g x')) (↑g' y')
[PROOFSTEP]
convert LinearMap.congr_fun₂ h x' y' using 0
[GOAL]
case mpr
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type u_2
inst✝²² : CommSemiring R₂
R₃ : Type u_3
inst✝²¹ : CommSemiring R₃
R₄ : Type u_4
inst✝²⁰ : CommSemiring R₄
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
h : f₁ = f₂
⊢ compl₁₂ f₁ g g' = compl₁₂ f₂ g g'
[PROOFSTEP]
subst h
[GOAL]
case mpr
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type u_2
inst✝²² : CommSemiring R₂
R₃ : Type u_3
inst✝²¹ : CommSemiring R₃
R₄ : Type u_4
inst✝²⁰ : CommSemiring R₄
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
f₁ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
⊢ compl₁₂ f₁ g g' = compl₁₂ f₁ g g'
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type u_2
inst✝²² : CommSemiring R₂
R₃ : Type u_3
inst✝²¹ : CommSemiring R₃
R₄ : Type u_4
inst✝²⁰ : CommSemiring R₄
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
r s : R
m : M
⊢ (fun x x_1 => x • x_1) s (r • m) = r • (fun x x_1 => x • x_1) s m
[PROOFSTEP]
simp only [smul_smul, smul_eq_mul, mul_comm]
