awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Regular.ProjectiveDimension (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsLocalRing R
inst_3 : IsNoetherianRing R
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
inst_4 : Nontrivial.{v} (↑M : Type v)
inst_5 : Module.Finite.{u, v} R (↑M : Type v)
rs : List R
x : R
rs' : List R
mem : Membership.mem (γ := Ideal R) (maximalIdeal R) x ∧ ∀ a ∈ rs', Membership.mem (γ := Ideal R) (maximalIdeal R) a
reg : IsSMulRegular.{u, v} (↑M : Type v) x ∧ IsWeaklyRegular.{u, v} (QuotSMulTop x (↑M : Type v)) rs'
this : Nontrivial.{v} (QuotSMulTop x (↑M : Type v))
len : rs'.length = n
rw :
  projectiveDimension (C := ModuleCat.{v, u} R)
      (of R ((↑M : Type v) ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (↑M : Type v)) (Ideal.ofList (x :: rs')) ⊤)) =
    projectiveDimension M + HAdd.hAdd (α := WithBot ℕ∞) (↑n : WithBot ℕ∞) (↑1 : WithBot ℕ∞)
rw₁ :
  projectiveDimension (C := ModuleCat.{v, u} R)
      (of R ((↑M : Type v) ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (↑M : Type v)) (Ideal.ofList (x :: rs')) ⊤)) =
    projectiveDimension M + HAdd.hAdd (α := WithBot ℕ∞) (↑n : WithBot ℕ∞) 1
rw₂ :
  projectiveDimension (C := ModuleCat.{v, u} R)
      (of R
        (QuotSMulTop x (↑M : Type v) ⧸
          HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop x (↑M : Type v))) (Ideal.ofList rs') ⊤)) =
    projectiveDimension M + HAdd.hAdd (α := WithBot ℕ∞) (↑n : WithBot ℕ∞) 1
rw₃ :
  projectiveDimension (C := ModuleCat.{v, u} R)
      (of R
        (QuotSMulTop x (↑M : Type v) ⧸
          HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop x (↑M : Type v))) (Ideal.ofList rs') ⊤)) =
    projectiveDimension M + HAdd.hAdd (α := WithBot ℕ∞) 1 (↑n : WithBot ℕ∞)
⊢ projectiveDimension (C := ModuleCat.{v, u} R)
      (of R ((↑M : Type v) ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (↑M : Type v)) (Ideal.ofList (x :: rs')) ⊤)) =
    projectiveDimension M + (↑(n + 1) : WithBot ℕ∞)
have rw₄ : projectiveDimension (C := ModuleCat.{v, u} R)
    (of R
      (QuotSMulTop x (↑M : Type v) ⧸
        HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop x (↑M : Type v))) (Ideal.ofList rs') ⊤)) =
  projectiveDimension M + 1 + (↑n : WithBot ℕ∞)
Tactic: 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]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.ProjectiveDimension (goal)
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
⊢ 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 ℕ∞)
have 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 ℕ∞)
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]
Cleared hypotheses: M, inst_4, inst_5, rs, reg, mem, n, len
-- Lean 4 proof step from Mathlib.RingTheory.Regular.ProjectiveDimension (goal)
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 ℕ∞)
⊢ 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 ℕ∞)
have 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 ℕ∞)
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]
Cleared hypotheses: M, inst_4, inst_5, rs, reg, mem, n, len
-- Lean 4 proof step from Mathlib.RingTheory.Regular.ProjectiveDimension (goal)
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
⊢ Membership.mem (γ := Ideal R) (maximalIdeal R) x
have a : x ∈ HSMul.hSMul (α := Ideal R) (β := Submodule R R) (Ideal.ofList rs) ⊤
Tactic: apply IsLocalRing.le_maximalIdeal reg.2.symm
-- Lean 4 proof step from Mathlib.RingTheory.Regular.ProjectiveDimension (hypothesis)
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
⊢ projectiveDimension (C := ModuleCat.{v, u} R)
      (of R (Shrink.{v, u} (HasQuotient.Quotient R (B := Ideal R) (Ideal.ofList rs)))) =
    (↑rs.length : WithBot ℕ∞)
have mem_max : ∀ 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
-- Lean 4 proof step from Mathlib.RingTheory.Regular.ProjectiveDimension (goal)
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
⊢ 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) ⊤
have 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) ⊤
Tactic: nth_rw 1 [← (Ideal.ofList rs).mul_top, ← smul_eq_mul, Submodule.map_smul'']
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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
⊢ HSMul.hSMul (α := Ideal R) (ofList (r :: rs)) N = r • N ⊔ HSMul.hSMul (α := Ideal R) (ofList rs) N
have rw : HSMul.hSMul (α := Ideal R) (span {r} ⊔ ofList rs) N = r • N ⊔ HSMul.hSMul (α := Ideal R) (ofList rs) N
Tactic: rw [ofList_cons, Submodule.sup_smul, Submodule.ideal_span_singleton_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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
⊢ HSMul.hSMul (α := Ideal R) (ofList (r :: rs)) N = r • N ⊔ HSMul.hSMul (α := Ideal R) (ofList rs) N
have 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
Tactic: rw [ofList_cons, Submodule.sup_smul, Submodule.ideal_span_singleton_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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
⊢ HSMul.hSMul (α := Ideal R) (ofList (r :: rs)) N = r • N ⊔ HSMul.hSMul (α := Ideal R) (ofList rs) N
have rw₂ : r • N ⊔ HSMul.hSMul (α := Submodule R R) (ofList rs) N = r • N ⊔ HSMul.hSMul (α := Ideal R) (ofList rs) N
Tactic: rw [ofList_cons, Submodule.sup_smul, Submodule.ideal_span_singleton_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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
⊢ 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) ⊤
have 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) ⊤
Tactic: rw [map_smul'', map_top, range_mkQ]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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) ⊤
⊢ 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) ⊤
have 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) ⊤
Tactic: rw [map_smul'', map_top, range_mkQ]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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) ⊤
⊢ 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) ⊤
have 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) ⊤
Tactic: rw [map_smul'', map_top, range_mkQ]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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
⊢ 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 ⊤
have 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 ⊤
Tactic: rw [map_pointwise_smul, map_top, range_mkQ]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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 ⊤
⊢ 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 ⊤
have 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 ⊤
Tactic: rw [map_pointwise_smul, map_top, range_mkQ]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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 ⊤
⊢ 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 ⊤
have 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 ⊤
Tactic: rw [map_pointwise_smul, map_top, range_mkQ]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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
| ⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs)) ⊤ ↔
    ⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤
have a : ⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs)) ⊤
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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)) ⊤
| ⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs)) ⊤ ↔
    ⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤
have b : ⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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
| ⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs)) ⊤
have a : Subsingleton.{u_3 + 1} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs)) ⊤)
Tactic: rw [eq_comm, ← Quotient.subsingleton_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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
| ⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤
have b : Subsingleton.{u_3 + 1}
  (QuotSMulTop r M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤)
Tactic: rw [eq_comm, ← Quotient.subsingleton_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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
| ⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs)) ⊤ ↔
    ⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤
have a : Subsingleton.{u_3 + 1} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs)) ⊤)
Tactic: congr <;> rw [eq_comm, ← Quotient.subsingleton_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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)) ⊤ ↔
    ⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤
have b : Subsingleton.{u_3 + 1}
  (QuotSMulTop r M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤)
Tactic: congr <;> rw [eq_comm, ← Quotient.subsingleton_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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
⊢ ⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs)) ⊤ ↔
    ⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤
have 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) ⊤)
Tactic: conv => congr <;> rw [eq_comm, ← Quotient.subsingleton_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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
      (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
have h : AddSubgroup.map f (HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤).toAddSubgroup =
  AddSubgroup.map f ⊥
Tactic: convert! AddSubgroup.map_bot f using 1
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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 ⊥
⊢ 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
have h₁ : (HSMul.hSMul.{u_2, u_4, u_4} (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList []) ⊤).toAddSubgroup = ⊥
Tactic: convert! AddSubgroup.map_bot f using 1
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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
      (HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤).toAddSubgroup =
    AddSubgroup.map f ⊥
have h : AddSubgroup.map f (HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) ⊥ ⊤).toAddSubgroup =
  AddSubgroup.map f ⊥
Tactic: rw [Ideal.ofList_nil, bot_smul, bot_toAddSubgroup]