Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁶ : Ring R
R₂ : Type u_5
inst✝¹⁵ : Ring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝¹⁴ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹³ : RingHomInvPair σ₂₁ σ₁₂
M : Type u_6
N : Type u_7
inst✝¹² : AddCommGroup M
inst✝¹¹ : Module R M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module R₂ N
P : Submodule R M
Q : Submodule R₂ N
R₃ : Type u_8
O : Type u_9
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup O
inst✝⁶ : Module R₃ O
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
inst✝⁵ : RingHomInvPair σ₂₃ σ₃₂
inst✝⁴ : RingHomInvPair σ₃₂ σ₂₃
inst✝³ : RingHomInvPair σ₁₃ σ₃₁
inst✝² : RingHomInvPair σ₃₁ σ₁₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
S : Submodule R₃ O
e : M ≃ₛₗ[σ₁₂] N
f : N ≃ₛₗ[σ₂₃] O
he : map (↑e) P = Q
hf : map (↑f) Q = S
hef : map (↑(e.trans f)) P = S
x✝ : M ⧸ P
⊢ (P.mapQ S (↑f ∘ₛₗ ↑e) ⋯) x✝ = (Q.mapQ S ↑f ⋯) ((P.mapQ Q ↑e ⋯) x✝)

Tactic:
mapQ_comp,

Goal state after:
R : Type u_1
inst✝¹⁶ : Ring R
R₂ : Type u_5
inst✝¹⁵ : Ring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝¹⁴ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹³ : RingHomInvPair σ₂₁ σ₁₂
M : Type u_6
N : Type u_7
inst✝¹² : AddCommGroup M
inst✝¹¹ : Module R M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module R₂ N
P : Submodule R M
Q : Submodule R₂ N
R₃ : Type u_8
O : Type u_9
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup O
inst✝⁶ : Module R₃ O
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
inst✝⁵ : RingHomInvPair σ₂₃ σ₃₂
inst✝⁴ : RingHomInvPair σ₃₂ σ₂₃
inst✝³ : RingHomInvPair σ₁₃ σ₃₁
inst✝² : RingHomInvPair σ₃₁ σ₁₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
S : Submodule R₃ O
e : M ≃ₛₗ[σ₁₂] N
f : N ≃ₛₗ[σ₂₃] O
he : map (↑e) P = Q
hf : map (↑f) Q = S
hef : map (↑(e.trans f)) P = S
x✝ : M ⧸ P
⊢ (mapQ ?p₂ S ↑f ?hg ∘ₛₗ P.mapQ ?p₂ ↑e ?hf) x✝ = (Q.mapQ S ↑f ⋯) ((P.mapQ Q ↑e ⋯) x✝)

case p₂
R : Type u_1
inst✝¹⁶ : Ring R
R₂ : Type u_5
inst✝¹⁵ : Ring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝¹⁴ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹³ : RingHomInvPair σ₂₁ σ₁₂
M : Type u_6
N : Type u_7
inst✝¹² : AddCommGroup M
inst✝¹¹ : Module R M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module R₂ N
P : Submodule R M
Q : Submodule R₂ N
R₃ : Type u_8
O : Type u_9
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup O
inst✝⁶ : Module R₃ O
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
inst✝⁵ : RingHomInvPair σ₂₃ σ₃₂
inst✝⁴ : RingHomInvPair σ₃₂ σ₂₃
inst✝³ : RingHomInvPair σ₁₃ σ₃₁
inst✝² : RingHomInvPair σ₃₁ σ₁₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
S : Submodule R₃ O
e : M ≃ₛₗ[σ₁₂] N
f : N ≃ₛₗ[σ₂₃] O
he : map (↑e) P = Q
hf : map (↑f) Q = S
hef : map (↑(e.trans f)) P = S
x✝ : M ⧸ P
⊢ Submodule R₂ N

case hf
R : Type u_1
inst✝¹⁶ : Ring R
R₂ : Type u_5
inst✝¹⁵ : Ring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝¹⁴ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹³ : RingHomInvPair σ₂₁ σ₁₂
M : Type u_6
N : Type u_7
inst✝¹² : AddCommGroup M
inst✝¹¹ : Module R M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module R₂ N
P : Submodule R M
Q : Submodule R₂ N
R₃ : Type u_8
O : Type u_9
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup O
inst✝⁶ : Module R₃ O
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
inst✝⁵ : RingHomInvPair σ₂₃ σ₃₂
inst✝⁴ : RingHomInvPair σ₃₂ σ₂₃
inst✝³ : RingHomInvPair σ₁₃ σ₃₁
inst✝² : RingHomInvPair σ₃₁ σ₁₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
S : Submodule R₃ O
e : M ≃ₛₗ[σ₁₂] N
f : N ≃ₛₗ[σ₂₃] O
he : map (↑e) P = Q
hf : map (↑f) Q = S
hef : map (↑(e.trans f)) P = S
x✝ : M ⧸ P
⊢ P ≤ comap ↑e ?p₂

case hg
R : Type u_1
inst✝¹⁶ : Ring R
R₂ : Type u_5
inst✝¹⁵ : Ring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝¹⁴ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹³ : RingHomInvPair σ₂₁ σ₁₂
M : Type u_6
N : Type u_7
inst✝¹² : AddCommGroup M
inst✝¹¹ : Module R M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module R₂ N
P : Submodule R M
Q : Submodule R₂ N
R₃ : Type u_8
O : Type u_9
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup O
inst✝⁶ : Module R₃ O
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
inst✝⁵ : RingHomInvPair σ₂₃ σ₃₂
inst✝⁴ : RingHomInvPair σ₃₂ σ₂₃
inst✝³ : RingHomInvPair σ₁₃ σ₃₁
inst✝² : RingHomInvPair σ₃₁ σ₁₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
S : Submodule R₃ O
e : M ≃ₛₗ[σ₁₂] N
f : N ≃ₛₗ[σ₂₃] O
he : map (↑e) P = Q
hf : map (↑f) Q = S
hef : map (↑(e.trans f)) P = S
x✝ : M ⧸ P
⊢ ?p₂ ≤ comap (↑f) S