awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Regular.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsLocalRing R
inst_3 : IsNoetherianRing R
M : ModuleCat.{v, u} R
inst_4 : Nontrivial.{v} (↑M : Type v)
inst_5 : Module.Finite.{u, v} R (↑M : Type v)
rs : List R
reg : IsWeaklyRegular.{u, v} (↑M : Type v) rs
mem : ∀ r ∈ rs, Membership.mem (γ := Ideal R) (maximalIdeal R) r
n : ℕ
len : rs.length = n
zero :
  ∀ (M : ModuleCat.{v, u} R) [Nontrivial.{v} (↑M : Type v)] [Module.Finite.{u, v} R (↑M : Type v)] (rs : List R)
    (reg : IsWeaklyRegular.{u, v} (↑M : Type v) rs) (mem : ∀ r ∈ rs, Membership.mem (γ := Ideal R) (maximalIdeal R) r)
    (len : rs.length = 0),
    projectiveDimension (C := ModuleCat.{v, u} R)
        (of R ((↑M : Type v) ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (↑M : Type v)) (Ideal.ofList rs) ⊤)) =
      projectiveDimension M + (↑0 : WithBot ℕ∞)
succ :
  ∀ (n : ℕ)
    (hn :
      ∀ (M : ModuleCat.{v, u} R) [Nontrivial.{v} (↑M : Type v)] [Module.Finite.{u, v} R (↑M : Type v)] (rs : List R)
        (reg : IsWeaklyRegular.{u, v} (↑M : Type v) rs)
        (mem : ∀ r ∈ rs, Membership.mem (γ := Ideal R) (maximalIdeal R) r) (len : rs.length = n),
        projectiveDimension (C := ModuleCat.{v, u} R)
            (of R ((↑M : Type v) ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (↑M : Type v)) (Ideal.ofList rs) ⊤)) =
          projectiveDimension M + (↑n : WithBot ℕ∞))
    (M : ModuleCat.{v, u} R) [Nontrivial.{v} (↑M : Type v)] [Module.Finite.{u, v} R (↑M : Type v)] (rs : List R)
    (reg : IsWeaklyRegular.{u, v} (↑M : Type v) rs) (mem : ∀ r ∈ rs, Membership.mem (γ := Ideal R) (maximalIdeal R) r)
    (len : rs.length = n + 1),
    projectiveDimension (C := ModuleCat.{v, u} R)
        (of R ((↑M : Type v) ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (↑M : Type v)) (Ideal.ofList rs) ⊤)) =
      projectiveDimension M + (↑(n + 1) : WithBot ℕ∞)
⊢ projectiveDimension (C := ModuleCat.{v, u} R)
      (of R ((↑M : Type v) ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (↑M : Type v)) (Ideal.ofList rs) ⊤)) =
    projectiveDimension M + (↑n : WithBot ℕ∞)

Tactic:
induction n generalizing M rs with
  | zero =>
    rw [List.length_eq_zero_iff.mp len, Ideal.ofList_nil, Submodule.bot_smul]
    simpa using projectiveDimension_eq_of_iso (Submodule.quotEquivOfEqBot ⊥ rfl).toModuleIso
  | succ n hn =>
    match rs with
    | [] => simp at len
    | x :: rs' =>
      simp only [List.mem_cons, forall_eq_or_imp] at mem
      simp only [isWeaklyRegular_cons_iff] at reg
      have := nontrivial_quotSMulTop_of_mem_maximalIdeal M mem.1
      simp only [List.length_cons, Nat.add_right_cancel_iff] at len
      rw [Nat.cast_add, Nat.cast_one, projectiveDimension_eq_of_iso
        (Submodule.quotOfListConsSMulTopEquivQuotSMulTopInner M x rs').toModuleIso, add_comm _ 1,
        ← add_assoc, ← projectiveDimension_quotSMulTop_eq_succ_of_isSMulRegular M x reg.1 mem.1,
        ← hn (ModuleCat.of R (QuotSMulTop x M)) rs' reg.2 mem.2 len]

Premises used: LinearEquiv.toModuleIso, Submodule.bot_smul, Submodule.quotEquivOfEqBot, Bot.bot, CategoryTheory.projectiveDimension_eq_of_iso, Ideal.ofList_nil, Iff.mp, List.length_eq_zero_iff, rfl
-- Module: Mathlib.RingTheory.Regular.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsLocalRing R
inst_3 : IsNoetherianRing R
rs : List R
reg : RingTheory.Sequence.IsRegular R rs
x : R
hx : x ∈ rs
a : x ∈ HSMul.hSMul (α := Ideal R) (β := Submodule R R) (Ideal.ofList rs) ⊤
⊢ Membership.mem (γ := Ideal R) (maximalIdeal R) x

Tactic:
apply IsLocalRing.le_maximalIdeal reg.2.symm

Premises used: RingTheory.Sequence.IsRegular.top_ne_smul, Ne.symm, IsLocalRing.le_maximalIdeal
-- Module: Mathlib.RingTheory.Regular.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsLocalRing R
inst_3 : IsNoetherianRing R
rs : List R
reg : RingTheory.Sequence.IsRegular R rs
x : R
hx : x ∈ rs
⊢ x ∈ HSMul.hSMul (α := Ideal R) (β := Submodule R R) (Ideal.ofList rs) ⊤

Tactic:
simpa using (Ideal.mem_span x).mpr fun p a ↦ a hx

Premises used: Iff.mpr, Ideal.mem_span
-- Module: Mathlib.RingTheory.Regular.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsLocalRing R
inst_3 : IsNoetherianRing R
rs : List R
reg : RingTheory.Sequence.IsRegular R rs
⊢ ∀ x ∈ rs, Membership.mem (γ := Ideal R) (maximalIdeal R) x

Tactic:
have mem_max : ∀ x ∈ rs, x ∈ maximalIdeal R := by
    intro x hx
    apply IsLocalRing.le_maximalIdeal reg.2.symm
    simpa using (Ideal.mem_span x).mpr fun p a ↦ a hx
-- Module: Mathlib.RingTheory.Regular.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsLocalRing R
inst_3 : IsNoetherianRing R
rs : List R
reg : RingTheory.Sequence.IsRegular R rs
mem_max : ∀ x ∈ rs, Membership.mem (γ := Ideal R) (maximalIdeal R) x
nth_rw :
  HSMul.hSMul (α := Ideal R) (β := Submodule R (Shrink.{v, u} R)) (Ideal.ofList rs)
      (Submodule.map (↑(LinearEquiv.symm (Shrink.linearEquiv R R)) : R →ₗ[R] Shrink.{v, u} R) ⊤) =
    HSMul.hSMul (α := Ideal R) (β := Submodule R (Shrink.{v, u} R)) (Ideal.ofList rs) ⊤
⊢ Submodule.map (↑(LinearEquiv.symm (Shrink.linearEquiv R R)) : R →ₗ[R] Shrink.{v, u} R) (Ideal.ofList rs) =
    HSMul.hSMul (α := Ideal R) (β := Submodule R (Shrink.{v, u} R)) (Ideal.ofList rs) ⊤

Tactic:
nth_rw 1 [← (Ideal.ofList rs).mul_top, ← smul_eq_mul, Submodule.map_smul'']

Premises used: Submodule.map_smul'', Ideal.ofList, smul_eq_mul, Ideal.mul_top
-- Module: Mathlib.RingTheory.Regular.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsLocalRing R
inst_3 : IsNoetherianRing R
rs : List R
reg : RingTheory.Sequence.IsRegular R rs
mem_max : ∀ x ∈ rs, Membership.mem (γ := Ideal R) (maximalIdeal R) x
⊢ HSMul.hSMul (α := Ideal R) (β := Submodule R (Shrink.{v, u} R)) (Ideal.ofList rs)
      (Submodule.map (↑(LinearEquiv.symm (Shrink.linearEquiv R R)) : R →ₗ[R] Shrink.{v, u} R) ⊤) =
    HSMul.hSMul (α := Ideal R) (β := Submodule R (Shrink.{v, u} R)) (Ideal.ofList rs) ⊤

Tactic:
simp
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := Ideal R) (ofList []) ⊥

Tactic:
have : { r | r ∈ [] } = ∅ := Set.eq_empty_of_forall_notMem (fun _ => List.not_mem_nil)
  Eq.trans (congrArg span this) span_empty

Premises used: congrArg, Set.eq_empty_of_forall_notMem, Ideal.span_empty, Ideal.span, List.not_mem_nil, Eq.trans
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
inst : Semiring R
rs₁ rs₂ : List R
⊢ Eq (α := Ideal R) (ofList (rs₁ ++ rs₂)) (ofList rs₁ ⊔ ofList rs₂)

Tactic:
have : { r | r ∈ rs₁ ++ rs₂ } = _ := Set.ext (fun _ => List.mem_append)
  Eq.trans (congrArg span this) (span_union _ _)

Premises used: Set.ext, congrArg, List.mem_append, Ideal.span, Ideal.span_union, List.Mem, Eq.trans
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
inst : Semiring R
r : R
⊢ Eq (α := Ideal R) (ofList [r]) (span {r})

Tactic:
congrArg span (Set.ext fun _ => List.mem_singleton)

Premises used: Set.ext, congrArg, List.mem_singleton, Ideal.span
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
inst : Semiring R
r : R
rs : List R
⊢ Eq (α := Ideal R) (ofList (r :: rs)) (span {r} ⊔ ofList rs)

Tactic:
Eq.trans (ofList_append [r] rs) (congrArg (· ⊔ _) (ofList_singleton r))

Premises used: congrArg, List.cons, Max.max, Ideal.ofList_append, Ideal.ofList_singleton, Eq.trans, List.nil
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
rs : List R
⊢ Eq.{u_2 + 1} (α := Ideal S) (map f (ofList rs)) (ofList (List.map (⇑f : (a : R) → S) rs))

Tactic:
Eq.trans (map_span f { r | r ∈ rs }) <| congrArg span <|
    Set.ext (fun _ => List.mem_map.symm)

Premises used: Set.ext, congrArg, setOf, Membership.mem, Ideal.map_span, Ideal.span, List.mem_map, Iff.symm, Eq.trans
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_7
inst : CommSemiring R
r : R
rs : List R
M : Type u_8
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
rw : HSMul.hSMul (α := Ideal R) (span {r} ⊔ ofList rs) N = r • N ⊔ HSMul.hSMul (α := Ideal R) (ofList rs) N
rw₁ :
  HSMul.hSMul (α := Submodule R R) (span {r}) N ⊔ HSMul.hSMul (α := Submodule R R) (ofList rs) N =
    r • N ⊔ HSMul.hSMul (α := Ideal R) (ofList rs) N
rw₂ rw₃ : r • N ⊔ HSMul.hSMul (α := Submodule R R) (ofList rs) N = r • N ⊔ HSMul.hSMul (α := Ideal R) (ofList rs) N
⊢ HSMul.hSMul (α := Ideal R) (ofList (r :: rs)) N = r • N ⊔ HSMul.hSMul (α := Ideal R) (ofList rs) N

Tactic:
rw [ofList_cons, Submodule.sup_smul, Submodule.ideal_span_singleton_smul]

Premises used: Submodule.ideal_span_singleton_smul, Submodule.sup_smul, Ideal.ofList_cons
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M₂
inst_3 : Module R M
inst_4 : Module R M₂
r : R
rs : List R
rw :
  HSMul.hSMul (α := Ideal R) (Ideal.ofList rs) (map (HSMul.hSMul (β := Submodule R M) r ⊤).mkQ ⊤) =
    HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤
rw₁ :
  HSMul.hSMul (α := Ideal R) (Ideal.ofList rs) (HSMul.hSMul (β := Submodule R M) r ⊤).mkQ.range =
    HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤
rw₂ rw₃ :
  HSMul.hSMul (α := Ideal R) (β := Submodule R (M ⧸ HSMul.hSMul (β := Submodule R M) r ⊤)) (Ideal.ofList rs) ⊤ =
    HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤
⊢ map (HSMul.hSMul (β := Submodule R M) r ⊤).mkQ (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs) ⊤) =
    HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤

Tactic:
rw [map_smul'', map_top, range_mkQ]

Premises used: Submodule.map_smul'', Submodule.map_top, Submodule.range_mkQ
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M₂
inst_3 : Module R M
inst_4 : Module R M₂
r : R
rs : List R
rw :
  r • map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs) ⊤).mkQ ⊤ =
    HSMul.hSMul (β := Submodule R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs) ⊤)) r ⊤
rw₁ :
  r • (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs) ⊤).mkQ.range =
    HSMul.hSMul (β := Submodule R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs) ⊤)) r ⊤
rw₂ rw₃ :
  HSMul.hSMul (β := Submodule R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs) ⊤)) r ⊤ =
    HSMul.hSMul (β := Submodule R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs) ⊤)) r ⊤
⊢ map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs) ⊤).mkQ (HSMul.hSMul (β := Submodule R M) r ⊤) =
    HSMul.hSMul (β := Submodule R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs) ⊤)) r ⊤

Tactic:
rw [map_pointwise_smul, map_top, range_mkQ]

Premises used: Submodule.map_top, Submodule.range_mkQ, Submodule.map_pointwise_smul
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
M : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M₂
inst_3 : Module R M
inst_4 : Module R M₂
r : R
rs : List R
f : M →ₗ[R] M₂
⊢ (↑(quotOfListConsSMulTopEquivQuotSMulTopInner M₂ r rs) :
        M₂ ⧸ Ideal.ofList (r :: rs) • ⊤ →ₗ[R] QuotSMulTop r M₂ ⧸ Ideal.ofList rs • ⊤) ∘ₗ
      (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs)) ⊤).mapQ
        (HSMul.hSMul (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList (r :: rs)) ⊤) f ⋯ =
    (HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤).mapQ
        (HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M₂)) (Ideal.ofList rs) ⊤)
        ((QuotSMulTop.map r : (a : M →ₗ[R] M₂) → QuotSMulTop r M →ₗ[R] QuotSMulTop r M₂) f) ⋯ ∘ₗ
      (↑(quotOfListConsSMulTopEquivQuotSMulTopInner M r rs) :
        M ⧸ Ideal.ofList (r :: rs) • ⊤ →ₗ[R] QuotSMulTop r M ⧸ Ideal.ofList rs • ⊤)

Tactic:
quot_hom_ext _ _ _ fun _ => rfl

Premises used: rfl, Submodule.quot_hom_ext
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
rs : List R
a : ⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs)) ⊤
b : ⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤
| ⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs)) ⊤ ↔
    ⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤

Tactic:
congr
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
rs : List R
a : Subsingleton.{u_3 + 1} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs)) ⊤)
| ⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs)) ⊤

Tactic:
rw [eq_comm, ← Quotient.subsingleton_iff]

Premises used: eq_comm, Submodule.Quotient.subsingleton_iff
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
rs : List R
b :
  Subsingleton.{u_3 + 1}
    (QuotSMulTop r M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤)
| ⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤

Tactic:
rw [eq_comm, ← Quotient.subsingleton_iff]

Premises used: eq_comm, Submodule.Quotient.subsingleton_iff
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
rs : List R
a : Subsingleton.{u_3 + 1} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs)) ⊤)
b :
  Subsingleton.{u_3 + 1}
    (QuotSMulTop r M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤)
| ⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs)) ⊤ ↔
    ⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤

Tactic:
congr <;> rw [eq_comm, ← Quotient.subsingleton_iff]

Premises used: eq_comm, Submodule.Quotient.subsingleton_iff
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
rs : List R
conv :
  Subsingleton.{u_3 + 1} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs)) ⊤) ↔
    Subsingleton.{u_3 + 1}
      (QuotSMulTop r M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤)
⊢ ⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs)) ⊤ ↔
    ⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤

Tactic:
conv => congr <;> rw [eq_comm, ← Quotient.subsingleton_iff]

Premises used: eq_comm, Submodule.Quotient.subsingleton_iff
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
rs : List R
⊢ Subsingleton.{u_3 + 1} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs)) ⊤) ↔
    Subsingleton.{u_3 + 1}
      (QuotSMulTop r M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤)

Tactic:
(quotOfListConsSMulTopEquivQuotSMulTopInner M r rs).toEquiv.subsingleton_congr

Premises used: Equiv.subsingleton_congr, Submodule.quotOfListConsSMulTopEquivQuotSMulTopInner, LinearEquiv.toEquiv
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
rs : List R
⊢ Subsingleton.{u_3 + 1} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs)) ⊤) ↔
    Subsingleton.{u_3 + 1}
      (QuotSMulTop r M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤)

Tactic:
exact (quotOfListConsSMulTopEquivQuotSMulTopInner M r rs).toEquiv.subsingleton_congr

Premises used: Equiv.subsingleton_congr, Submodule.quotOfListConsSMulTopEquivQuotSMulTopInner, LinearEquiv.toEquiv
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
rs : List R
⊢ IsWeaklyRegular M rs ↔
    ∀ (i : Fin rs.length),
      IsSMulRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (ofList (List.take (↑i : ℕ) rs)) ⊤)
        (getElem (valid := fun (xs : List R) (i : Fin rs.length) ↦ (↑i : ℕ) < xs.length) rs i ⋯)

Tactic:
Iff.trans (isWeaklyRegular_iff M rs) (Iff.symm Fin.forall_iff)

Premises used: Fin.forall_iff, Iff.trans, RingTheory.Sequence.isWeaklyRegular_iff, Iff.symm
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
⊢ AddSubgroup.map f ⊥ = ⊥

Tactic:
AddSubgroup.map_bot f

Premises used: AddSubgroup.map_bot
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
h :
  AddSubgroup.map f
      (HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤).toAddSubgroup =
    AddSubgroup.map f ⊥
h₁ : (HSMul.hSMul.{u_2, u_4, u_4} (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList []) ⊤).toAddSubgroup = ⊥
⊢ AddSubgroup.map f
      (HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤).toAddSubgroup =
    (HSMul.hSMul.{u_2, u_4, u_4} (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList []) ⊤).toAddSubgroup

Tactic:
convert! AddSubgroup.map_bot f using 1

Premises used: AddSubgroup.map_bot
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
h :
  AddSubgroup.map f (HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) ⊥ ⊤).toAddSubgroup =
    AddSubgroup.map f ⊥
h₁ : AddSubgroup.map f (toAddSubgroup.{u_1, u_3} (R := R) (module_M := inst_4) ⊥) = AddSubgroup.map f ⊥
h₂ h₃ : AddSubgroup.map f ⊥ = AddSubgroup.map f ⊥
⊢ AddSubgroup.map f
      (HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤).toAddSubgroup =
    AddSubgroup.map f ⊥

Tactic:
rw [Ideal.ofList_nil, bot_smul, bot_toAddSubgroup]

Premises used: Submodule.bot_smul, Ideal.ofList_nil, Submodule.bot_toAddSubgroup
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
h : (HSMul.hSMul.{u_2, u_4, u_4} (α := Ideal S) (β := Submodule S M₂) ⊥ ⊤).toAddSubgroup = ⊥
h₁ : Eq.{u_4 + 1} (α := AddSubgroup M₂) (toAddSubgroup.{u_2, u_4} (R := S) (module_M := inst_5) ⊥) ⊥
h₂ h₃ : Eq.{u_4 + 1} (α := AddSubgroup M₂) ⊥ ⊥
⊢ (HSMul.hSMul.{u_2, u_4, u_4} (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList []) ⊤).toAddSubgroup = ⊥

Tactic:
rw [Ideal.ofList_nil, bot_smul, bot_toAddSubgroup]

Premises used: Submodule.bot_smul, Ideal.ofList_nil, Submodule.bot_toAddSubgroup
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
r : R
s : S
l₁ : List R
l₂ : List S
h : ∀ (x : M), (f : (a : M) → M₂) (r • x) = HSMul.hSMul (β := M₂) s ((f : (a : M) → M₂) x : M₂)
h_1 :
  List.Forall₂
    (fun (r : R) (s : S) ↦ ∀ (x : M), (f : (a : M) → M₂) (r • x) = HSMul.hSMul (β := M₂) s ((f : (a : M) → M₂) x : M₂))
    l₁ l₂
ih :
  AddSubgroup.map f (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList l₁) ⊤).toAddSubgroup =
    (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList l₂) ⊤).toAddSubgroup
a : AddSubgroup.map f (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: l₁)) ⊤).toAddSubgroup
a₁ : (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList (s :: l₂)) ⊤).toAddSubgroup
| AddSubgroup.map f (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: l₁)) ⊤).toAddSubgroup =
    (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList (s :: l₂)) ⊤).toAddSubgroup

Tactic:
congr
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
r : R
s : S
l₁ : List R
l₂ : List S
h : ∀ (x : M), (f : (a : M) → M₂) (r • x) = HSMul.hSMul (β := M₂) s ((f : (a : M) → M₂) x : M₂)
h_1 :
  List.Forall₂
    (fun (r : R) (s : S) ↦ ∀ (x : M), (f : (a : M) → M₂) (r • x) = HSMul.hSMul (β := M₂) s ((f : (a : M) → M₂) x : M₂))
    l₁ l₂
ih :
  AddSubgroup.map f (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList l₁) ⊤).toAddSubgroup =
    (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList l₂) ⊤).toAddSubgroup
a :
  AddSubgroup.map f
    (AddSubgroup.map (G := M)
        (((toAddMonoidEnd R M : MonoidHom.{u_1, u_3} R (AddMonoid.End M)) : (a : R) → AddMonoid.End M) r) ⊤ ⊔
      (HSMul.hSMul (α := Submodule R R) (β := Submodule R M) (Ideal.ofList l₁) ⊤).toAddSubgroup)
| AddSubgroup.map f (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: l₁)) ⊤).toAddSubgroup

Tactic:
rw [Ideal.ofList_cons, sup_smul, sup_toAddSubgroup,
      ideal_span_singleton_smul, pointwise_smul_toAddSubgroup,
      top_toAddSubgroup, AddSubgroup.pointwise_smul_def]

Premises used: Submodule.ideal_span_singleton_smul, Submodule.pointwise_smul_toAddSubgroup, Submodule.top_toAddSubgroup, Submodule.sup_smul, Ideal.ofList_cons, AddSubgroup.pointwise_smul_def, Submodule.sup_toAddSubgroup