Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: R : Type u_1
M₄ : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M₄
inst✝⁸ : Module R M₄
rs : List R
M✝ : Type u_6
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
M : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f₁ : M →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
f₃ : M₃ →ₗ[R] M✝
h₁₂ : Exact ⇑f₁ ⇑f₂
h₂₃ : Exact ⇑f₂ ⇑f₃
h₃ : Surjective ⇑f₃
⊢ (M ⧸ Ideal.ofList [] • ⊤) ≃ₗ[R] M

pp: R : Type u_1
M₄ : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M₄
inst✝⁸ : Module R M₄
rs : List R
M✝ : Type u_6
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
M : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f₁ : M →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
f₃ : M₃ →ₗ[R] M✝
h₁₂ : Exact ⇑f₁ ⇑f₂
h₂₃ : Exact ⇑f₂ ⇑f₃
h₃ : Surjective ⇑f₃
⊢ (M₂ ⧸ Ideal.ofList [] • ⊤) ≃ₗ[R] M₂

pp: R : Type u_1
M₄ : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M₄
inst✝⁸ : Module R M₄
rs : List R
M✝ : Type u_6
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
M : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f₁ : M →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
f₃ : M₃ →ₗ[R] M✝
h₁₂ : Exact ⇑f₁ ⇑f₂
h₂₃ : Exact ⇑f₂ ⇑f₃
h₃ : Surjective ⇑f₃
⊢ (M₃ ⧸ Ideal.ofList [] • ⊤) ≃ₗ[R] M₃

pp: R : Type u_1
M₄ : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M₄
inst✝⁸ : Module R M₄
rs : List R
M✝ : Type u_6
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
M : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f₁ : M →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
f₃ : M₃ →ₗ[R] M✝
h₁₂ : Exact ⇑f₁ ⇑f₂
h₂₃ : Exact ⇑f₂ ⇑f₃
h₃ : Surjective ⇑f₃
⊢ f₁ ∘ₗ ↑?m.155 = ↑?m.156 ∘ₗ (Ideal.ofList [] • ⊤).mapQ (Ideal.ofList [] • ⊤) f₁ ⋯

pp: R : Type u_1
M₄ : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M₄
inst✝⁸ : Module R M₄
rs : List R
M✝ : Type u_6
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
M : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f₁ : M →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
f₃ : M₃ →ₗ[R] M✝
h₁₂ : Exact ⇑f₁ ⇑f₂
h₂₃ : Exact ⇑f₂ ⇑f₃
h₃ : Surjective ⇑f₃
⊢ f₂ ∘ₗ ↑?m.156 = ↑?m.157 ∘ₗ (Ideal.ofList [] • ⊤).mapQ (Ideal.ofList [] • ⊤) f₂ ⋯

Tactic:
any_goals exact quotEquivOfEqBot _ <|
      Eq.trans (congrArg (· • ⊤) Ideal.ofList_nil) (bot_smul ⊤)

Goal state after:
R : Type u_1
M₄ : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M₄
inst✝⁸ : Module R M₄
rs : List R
M✝ : Type u_6
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
M : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f₁ : M →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
f₃ : M₃ →ₗ[R] M✝
h₁₂ : Exact ⇑f₁ ⇑f₂
h₂₃ : Exact ⇑f₂ ⇑f₃
h₃ : Surjective ⇑f₃
⊢ f₁ ∘ₗ ↑((Ideal.ofList [] • ⊤).quotEquivOfEqBot ⋯) =
    ↑((Ideal.ofList [] • ⊤).quotEquivOfEqBot ⋯) ∘ₗ (Ideal.ofList [] • ⊤).mapQ (Ideal.ofList [] • ⊤) f₁ ⋯

R : Type u_1
M₄ : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M₄
inst✝⁸ : Module R M₄
rs : List R
M✝ : Type u_6
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
M : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f₁ : M →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
f₃ : M₃ →ₗ[R] M✝
h₁₂ : Exact ⇑f₁ ⇑f₂
h₂₃ : Exact ⇑f₂ ⇑f₃
h₃ : Surjective ⇑f₃
⊢ f₂ ∘ₗ ↑((Ideal.ofList [] • ⊤).quotEquivOfEqBot ⋯) =
    ↑((Ideal.ofList [] • ⊤).quotEquivOfEqBot ⋯) ∘ₗ (Ideal.ofList [] • ⊤).mapQ (Ideal.ofList [] • ⊤) f₂ ⋯