case h
R : Type u_3
M : Type u_4
r : R
x y : M
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
p p' : Submodule R M
R₂ : Type ?u.395898
M₂ : Type ?u.395901
inst✝⁶ : Ring R₂
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
N : Type u_1
O : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup O
inst✝ : Module R O
P : Submodule R M
Q : Submodule R N
S : Submodule R O
e : M ≃ₗ[R] N
f : N ≃ₗ[R] O
he : map e P = Q
hf : map f Q = S
hef : map (LinearEquiv.trans e f) P = S
x✝ : M ⧸ P
⊢ ↑(equiv P S (LinearEquiv.trans e f) hef) x✝ = ↑(LinearEquiv.trans (equiv P Q e he) (equiv Q S f hf)) x✝
R : Type u_3
M : Type u_4
r : R
x y : M
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
p p' : Submodule R M
R₂ : Type ?u.395898
M₂ : Type ?u.395901
inst✝⁶ : Ring R₂
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
N : Type u_1
O : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup O
inst✝ : Module R O
P : Submodule R M
Q : Submodule R N
S : Submodule R O
e : M ≃ₗ[R] N
f : N ≃ₗ[R] O
he : map e P = Q
hf : map f Q = S
hef : map (LinearEquiv.trans e f) P = S
⊢ equiv P S (LinearEquiv.trans e f) hef = LinearEquiv.trans (equiv P Q e he) (equiv Q S f hf)
ext
case h
R : Type u_3
M : Type u_4
r : R
x y : M
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
p p' : Submodule R M
R₂ : Type ?u.395898
M₂ : Type ?u.395901
inst✝⁶ : Ring R₂
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
N : Type u_1
O : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup O
inst✝ : Module R O
P : Submodule R M
Q : Submodule R N
S : Submodule R O
e : M ≃ₗ[R] N
f : N ≃ₗ[R] O
he : map e P = Q
hf : map f Q = S
hef : map (LinearEquiv.trans e f) P = S
x✝ : M ⧸ P
⊢ ↑(mapQ P S (comp ↑f ↑e) (_ : P ≤ comap (comp ↑f ↑e) S)) x✝ =
    ↑(mapQ Q S ↑f (_ : ∀ (x : N), x ∈ Q → x ∈ comap (↑f) S))
      (↑(mapQ P Q ↑e (_ : ∀ (x : M), x ∈ P → x ∈ comap (↑e) Q)) x✝)
case h
R : Type u_3
M : Type u_4
r : R
x y : M
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
p p' : Submodule R M
R₂ : Type ?u.395898
M₂ : Type ?u.395901
inst✝⁶ : Ring R₂
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
N : Type u_1
O : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup O
inst✝ : Module R O
P : Submodule R M
Q : Submodule R N
S : Submodule R O
e : M ≃ₗ[R] N
f : N ≃ₗ[R] O
he : map e P = Q
hf : map f Q = S
hef : map (LinearEquiv.trans e f) P = S
x✝ : M ⧸ P
⊢ ↑(equiv P S (LinearEquiv.trans e f) hef) x✝ = ↑(LinearEquiv.trans (equiv P Q e he) (equiv Q S f hf)) x✝
simp only [Quotient.equiv_apply, LinearEquiv.trans_apply, LinearEquiv.coe_trans]
no goals
case h
R : Type u_3
M : Type u_4
r : R
x y : M
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
p p' : Submodule R M
R₂ : Type ?u.395898
M₂ : Type ?u.395901
inst✝⁶ : Ring R₂
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
N : Type u_1
O : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup O
inst✝ : Module R O
P : Submodule R M
Q : Submodule R N
S : Submodule R O
e : M ≃ₗ[R] N
f : N ≃ₗ[R] O
he : map e P = Q
hf : map f Q = S
hef : map (LinearEquiv.trans e f) P = S
x✝ : M ⧸ P
⊢ ↑(mapQ P S (comp ↑f ↑e) (_ : P ≤ comap (comp ↑f ↑e) S)) x✝ =
    ↑(mapQ Q S ↑f (_ : ∀ (x : N), x ∈ Q → x ∈ comap (↑f) S))
      (↑(mapQ P Q ↑e (_ : ∀ (x : M), x ∈ P → x ∈ comap (↑e) Q)) x✝)
rw [mapQ_comp, LinearMap.comp_apply]