-- Mathlib/RingTheory/Regular/RegularSequence.lean
lemma isWeaklyRegular_append_iff (rs₁ rs₂ : List R) :
    IsWeaklyRegular M (rs₁ ++ rs₂) ↔
      IsWeaklyRegular M rs₁ ∧
        IsWeaklyRegular (M ⧸ (Ideal.ofList rs₁ • ⊤ : Submodule R M)) rs₂

Proof state:
case cons
R : Type u_1
inst✝² : CommRing R
rs₂ : List R
r : R
rs₁ : List R
ih :
  ∀ (M : Type u_3) [inst : AddCommGroup M] [inst_1 : Module R M],
    IsWeaklyRegular M (rs₁ ++ rs₂) ↔ IsWeaklyRegular M rs₁ ∧ IsWeaklyRegular (M ⧸ Ideal.ofList rs₁ • ⊤) rs₂
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ IsWeaklyRegular M (r :: rs₁ ++ rs₂) ↔
    IsWeaklyRegular M (r :: rs₁) ∧ IsWeaklyRegular (M ⧸ Ideal.ofList (r :: rs₁) • ⊤) rs₂

Tactic:
let e := quotOfListConsSMulTopEquivQuotSMulTopInner M r rs₁

Result:
case cons
R : Type u_1
inst✝² : CommRing R
rs₂ : List R
r : R
rs₁ : List R
ih :
  ∀ (M : Type u_3) [inst : AddCommGroup M] [inst_1 : Module R M],
    IsWeaklyRegular M (rs₁ ++ rs₂) ↔ IsWeaklyRegular M rs₁ ∧ IsWeaklyRegular (M ⧸ Ideal.ofList rs₁ • ⊤) rs₂
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : (M ⧸ Ideal.ofList (r :: rs₁) • ⊤) ≃ₗ[R] QuotSMulTop r M ⧸ Ideal.ofList rs₁ • ⊤ :=
  quotOfListConsSMulTopEquivQuotSMulTopInner M r rs₁
⊢ IsWeaklyRegular M (r :: rs₁ ++ rs₂) ↔
    IsWeaklyRegular M (r :: rs₁) ∧ IsWeaklyRegular (M ⧸ Ideal.ofList (r :: rs₁) • ⊤) rs₂

Proof state:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
rs₁ rs₂ : List R
⊢ IsWeaklyRegular M (rs₁ ++ rs₂) ↔ IsWeaklyRegular M rs₁ ∧ IsWeaklyRegular (M ⧸ Ideal.ofList rs₁ • ⊤) rs₂

Tactic:
induction rs₁ generalizing M with
| nil =>
  refine Iff.symm <| Iff.trans (and_iff_right (.nil R M)) ?_
  refine (quotEquivOfEqBot _ ?_).isWeaklyRegular_congr rs₂
  rw [Ideal.ofList_nil, bot_smul]
| cons r rs₁ ih =>
  let e := quotOfListConsSMulTopEquivQuotSMulTopInner M r rs₁
  rw [List.cons_append, isWeaklyRegular_cons_iff, isWeaklyRegular_cons_iff,
    ih, ← and_assoc, ← e.isWeaklyRegular_congr rs₂]

Result:
no goals

Proof state:
case nil
R : Type u_1
inst✝² : CommRing R
rs₂ : List R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ IsWeaklyRegular M ([] ++ rs₂) ↔ IsWeaklyRegular M [] ∧ IsWeaklyRegular (M ⧸ Ideal.ofList [] • ⊤) rs₂

Tactic:
refine Iff.symm <| Iff.trans (and_iff_right (.nil R M)) ?_

Result:
case nil
R : Type u_1
inst✝² : CommRing R
rs₂ : List R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ IsWeaklyRegular (M ⧸ Ideal.ofList [] • ⊤) rs₂ ↔ IsWeaklyRegular M ([] ++ rs₂)

Proof state:
case nil
R : Type u_1
inst✝² : CommRing R
rs₂ : List R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Ideal.ofList [] • ⊤ = ⊥

Tactic:
rw [Ideal.ofList_nil, bot_smul]

Result:
no goals

Proof state:
case nil
R : Type u_1
inst✝² : CommRing R
rs₂ : List R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ IsWeaklyRegular (M ⧸ Ideal.ofList [] • ⊤) rs₂ ↔ IsWeaklyRegular M ([] ++ rs₂)

Tactic:
refine (quotEquivOfEqBot _ ?_).isWeaklyRegular_congr rs₂

Result:
case nil
R : Type u_1
inst✝² : CommRing R
rs₂ : List R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Ideal.ofList [] • ⊤ = ⊥

Proof state:
case cons
R : Type u_1
inst✝² : CommRing R
rs₂ : List R
r : R
rs₁ : List R
ih :
  ∀ (M : Type u_3) [inst : AddCommGroup M] [inst_1 : Module R M],
    IsWeaklyRegular M (rs₁ ++ rs₂) ↔ IsWeaklyRegular M rs₁ ∧ IsWeaklyRegular (M ⧸ Ideal.ofList rs₁ • ⊤) rs₂
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : (M ⧸ Ideal.ofList (r :: rs₁) • ⊤) ≃ₗ[R] QuotSMulTop r M ⧸ Ideal.ofList rs₁ • ⊤ :=
  quotOfListConsSMulTopEquivQuotSMulTopInner M r rs₁
⊢ IsWeaklyRegular M (r :: rs₁ ++ rs₂) ↔
    IsWeaklyRegular M (r :: rs₁) ∧ IsWeaklyRegular (M ⧸ Ideal.ofList (r :: rs₁) • ⊤) rs₂

Tactic:
rw [List.cons_append, isWeaklyRegular_cons_iff, isWeaklyRegular_cons_iff,
  ih, ← and_assoc, ← e.isWeaklyRegular_congr rs₂]

Result:
no goals