awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rs : List R
h_1 : IsWeaklyRegular M rs
rs' : List R
h'' : rs ~ rs'
h' :
  ∀ (a b : R) (rs' : List R),
    a :: b :: rs' <+~ rs →
      let K : Submodule R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs') ⊤) :=
        torsionBy.{u_1, u_3} R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs') ⊤) b;
      K = a • K → K = ⊥
rs₁ rs₂ rs₀ : List R
h₁₂ : rs₁ ~ rs₂
H₁ : rs₀ ++ rs₁ <+~ rs
H₃ : rs₀ ++ rs₂ <+~ rs
h : IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) rs₁
⊢ IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) rs₂
have nil : ∀ (rs₀ : List R) (H₁ H₃ : rs₀ ++ [] <+~ rs)
  (h :
    IsWeaklyRegular.{u_1, u_3} (R := R) (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) []),
  IsWeaklyRegular.{u_1, u_3} (R := R) (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) []
Tactic: induction h₁₂ generalizing rs₀ with
  | nil => exact .nil R _
  | cons r _ ih =>
    let e := quotOfListConsSMulTopEquivQuotSMulTopOuter M r rs₀
    rw [isWeaklyRegular_cons_iff, ← e.isWeaklyRegular_congr] at h ⊢
    refine h.imp_right (ih (r :: rs₀) ?_ ?_) <;>
      exact List.perm_middle.subperm_right.mp ‹_›
  | swap a b t =>
    rw [show ∀ x y z, x :: y :: z = [x, y] ++ z from fun _ _ _ => rfl,
      isWeaklyRegular_append_iff] at h ⊢
    have : Ideal.ofList [b, a] = Ideal.ofList [a, b] :=
      congrArg Ideal.span <| Set.ext fun _ => (List.Perm.swap a b []).mem_iff
    rw [(quotEquivOfEq _ _ (congrArg₂ _ this rfl)).isWeaklyRegular_congr] at h
    rw [List.append_cons, List.append_cons, List.append_assoc _ [b] [a]] at H₁
    apply (List.sublist_append_left (rs₀ ++ [b, a]) _).subperm.trans at H₁
    apply List.perm_append_comm.subperm.trans at H₁
    exact h.imp_left (swap · (h' b a rs₀ H₁))
  | trans h₁₂ _ ih₁₂ ih₂₃ =>
    have H₂ := (h₁₂.append_left rs₀).subperm_right.mp H₁
    exact ih₂₃ rs₀ H₂ H₃ (ih₁₂ rs₀ H₁ H₂ h)
Cleared hypotheses: rs₀, h₁₂, H₁, H₃, h
-- 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
rs : List R
h_1 : IsWeaklyRegular M rs
rs' : List R
h'' : rs ~ rs'
h' :
  ∀ (a b : R) (rs' : List R),
    a :: b :: rs' <+~ rs →
      let K : Submodule R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs') ⊤) :=
        torsionBy.{u_1, u_3} R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs') ⊤) b;
      K = a • K → K = ⊥
rs₁ rs₂ rs₀ : List R
h₁₂ : rs₁ ~ rs₂
H₁ : rs₀ ++ rs₁ <+~ rs
H₃ : rs₀ ++ rs₂ <+~ rs
h : IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) rs₁
nil :
  ∀ (rs₀ : List R) (H₁ H₃ : rs₀ ++ [] <+~ rs)
    (h :
      IsWeaklyRegular.{u_1, u_3} (R := R) (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤)
        []),
    IsWeaklyRegular.{u_1, u_3} (R := R) (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) []
⊢ IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) rs₂
have cons : ∀ (r : R) {l₁ l₂ : List R},
  l₁ ~ l₂ →
    ∀
      (ih :
        ∀ (rs₀ : List R) (H₁ : rs₀ ++ l₁ <+~ rs) (H₃ : rs₀ ++ l₂ <+~ rs)
          (h :
            IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) l₁),
          IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) l₂)
      (rs₀ : List R) (H₁ : rs₀ ++ r :: l₁ <+~ rs) (H₃ : rs₀ ++ r :: l₂ <+~ rs)
      (h :
        IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤)
          (r :: l₁)),
      IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) (r :: l₂)
Tactic: induction h₁₂ generalizing rs₀ with
  | nil => exact .nil R _
  | cons r _ ih =>
    let e := quotOfListConsSMulTopEquivQuotSMulTopOuter M r rs₀
    rw [isWeaklyRegular_cons_iff, ← e.isWeaklyRegular_congr] at h ⊢
    refine h.imp_right (ih (r :: rs₀) ?_ ?_) <;>
      exact List.perm_middle.subperm_right.mp ‹_›
  | swap a b t =>
    rw [show ∀ x y z, x :: y :: z = [x, y] ++ z from fun _ _ _ => rfl,
      isWeaklyRegular_append_iff] at h ⊢
    have : Ideal.ofList [b, a] = Ideal.ofList [a, b] :=
      congrArg Ideal.span <| Set.ext fun _ => (List.Perm.swap a b []).mem_iff
    rw [(quotEquivOfEq _ _ (congrArg₂ _ this rfl)).isWeaklyRegular_congr] at h
    rw [List.append_cons, List.append_cons, List.append_assoc _ [b] [a]] at H₁
    apply (List.sublist_append_left (rs₀ ++ [b, a]) _).subperm.trans at H₁
    apply List.perm_append_comm.subperm.trans at H₁
    exact h.imp_left (swap · (h' b a rs₀ H₁))
  | trans h₁₂ _ ih₁₂ ih₂₃ =>
    have H₂ := (h₁₂.append_left rs₀).subperm_right.mp H₁
    exact ih₂₃ rs₀ H₂ H₃ (ih₁₂ rs₀ H₁ H₂ h)
Cleared hypotheses: rs₀, h₁₂, H₁, H₃, h
-- 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
rs : List R
h_1 : IsWeaklyRegular M rs
rs' : List R
h'' : rs ~ rs'
h' :
  ∀ (a b : R) (rs' : List R),
    a :: b :: rs' <+~ rs →
      let K : Submodule R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs') ⊤) :=
        torsionBy.{u_1, u_3} R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs') ⊤) b;
      K = a • K → K = ⊥
rs₁ rs₂ rs₀ : List R
h₁₂ : rs₁ ~ rs₂
H₁ : rs₀ ++ rs₁ <+~ rs
H₃ : rs₀ ++ rs₂ <+~ rs
h : IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) rs₁
⊢ IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) rs₂
have nil : ∀ (rs₀ : List R) (H₁ H₃ : rs₀ ++ [] <+~ rs)
  (h :
    IsWeaklyRegular.{u_1, u_3} (R := R) (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) []),
  IsWeaklyRegular.{u_1, u_3} (R := R) (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) []
Tactic: {
  induction h₁₂ generalizing rs₀ with
  | nil => exact .nil R _
  | cons r _ ih =>
    let e := quotOfListConsSMulTopEquivQuotSMulTopOuter M r rs₀
    rw [isWeaklyRegular_cons_iff, ← e.isWeaklyRegular_congr] at h ⊢
    refine h.imp_right (ih (r :: rs₀) ?_ ?_) <;>
      exact List.perm_middle.subperm_right.mp ‹_›
  | swap a b t =>
    rw [show ∀ x y z, x :: y :: z = [x, y] ++ z from fun _ _ _ => rfl,
      isWeaklyRegular_append_iff] at h ⊢
    have : Ideal.ofList [b, a] = Ideal.ofList [a, b] :=
      congrArg Ideal.span <| Set.ext fun _ => (List.Perm.swap a b []).mem_iff
    rw [(quotEquivOfEq _ _ (congrArg₂ _ this rfl)).isWeaklyRegular_congr] at h
    rw [List.append_cons, List.append_cons, List.append_assoc _ [b] [a]] at H₁
    apply (List.sublist_append_left (rs₀ ++ [b, a]) _).subperm.trans at H₁
    apply List.perm_append_comm.subperm.trans at H₁
    exact h.imp_left (swap · (h' b a rs₀ H₁))
  | trans h₁₂ _ ih₁₂ ih₂₃ =>
    have H₂ := (h₁₂.append_left rs₀).subperm_right.mp H₁
    exact ih₂₃ rs₀ H₂ H₃ (ih₁₂ rs₀ H₁ H₂ h) }
Cleared hypotheses: rs₀, h₁₂, H₁, H₃, h
-- 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
rs : List R
h_1 : IsWeaklyRegular M rs
rs' : List R
h'' : rs ~ rs'
h' :
  ∀ (a b : R) (rs' : List R),
    a :: b :: rs' <+~ rs →
      let K : Submodule R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs') ⊤) :=
        torsionBy.{u_1, u_3} R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs') ⊤) b;
      K = a • K → K = ⊥
rs₁ rs₂ rs₀ : List R
h₁₂ : rs₁ ~ rs₂
H₁ : rs₀ ++ rs₁ <+~ rs
H₃ : rs₀ ++ rs₂ <+~ rs
h : IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) rs₁
nil :
  ∀ (rs₀ : List R) (H₁ H₃ : rs₀ ++ [] <+~ rs)
    (h :
      IsWeaklyRegular.{u_1, u_3} (R := R) (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤)
        []),
    IsWeaklyRegular.{u_1, u_3} (R := R) (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) []
⊢ IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) rs₂
have cons : ∀ (r : R) {l₁ l₂ : List R},
  l₁ ~ l₂ →
    ∀
      (ih :
        ∀ (rs₀ : List R) (H₁ : rs₀ ++ l₁ <+~ rs) (H₃ : rs₀ ++ l₂ <+~ rs)
          (h :
            IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) l₁),
          IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) l₂)
      (rs₀ : List R) (H₁ : rs₀ ++ r :: l₁ <+~ rs) (H₃ : rs₀ ++ r :: l₂ <+~ rs)
      (h :
        IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤)
          (r :: l₁)),
      IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) (r :: l₂)
Tactic: {
  induction h₁₂ generalizing rs₀ with
  | nil => exact .nil R _
  | cons r _ ih =>
    let e := quotOfListConsSMulTopEquivQuotSMulTopOuter M r rs₀
    rw [isWeaklyRegular_cons_iff, ← e.isWeaklyRegular_congr] at h ⊢
    refine h.imp_right (ih (r :: rs₀) ?_ ?_) <;>
      exact List.perm_middle.subperm_right.mp ‹_›
  | swap a b t =>
    rw [show ∀ x y z, x :: y :: z = [x, y] ++ z from fun _ _ _ => rfl,
      isWeaklyRegular_append_iff] at h ⊢
    have : Ideal.ofList [b, a] = Ideal.ofList [a, b] :=
      congrArg Ideal.span <| Set.ext fun _ => (List.Perm.swap a b []).mem_iff
    rw [(quotEquivOfEq _ _ (congrArg₂ _ this rfl)).isWeaklyRegular_congr] at h
    rw [List.append_cons, List.append_cons, List.append_assoc _ [b] [a]] at H₁
    apply (List.sublist_append_left (rs₀ ++ [b, a]) _).subperm.trans at H₁
    apply List.perm_append_comm.subperm.trans at H₁
    exact h.imp_left (swap · (h' b a rs₀ H₁))
  | trans h₁₂ _ ih₁₂ ih₂₃ =>
    have H₂ := (h₁₂.append_left rs₀).subperm_right.mp H₁
    exact ih₂₃ rs₀ H₂ H₃ (ih₁₂ rs₀ H₁ H₂ h) }
Cleared hypotheses: rs₀, h₁₂, H₁, H₃, h
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (hypothesis)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : IsNoetherian R M
rs rs' : List R
h1 : IsRegular M rs
h2 : rs ~ rs'
⊢ IsRegular M rs'
have h3 : IsWeaklyRegular M rs
Tactic: obtain ⟨h3, h4⟩ := h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (hypothesis)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : IsNoetherian R M
rs rs' : List R
h1 : IsRegular M rs
h2 : rs ~ rs'
h3 : IsWeaklyRegular M rs
⊢ IsRegular M rs'
have h4 : ⊤ ≠ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs) ⊤
Tactic: obtain ⟨h3, h4⟩ := h1
Cleared hypotheses: h1
-- 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
inst_3 : IsLocalRing R
inst_4 : IsNoetherian R M
rs rs' : List R
h2 : rs ~ rs'
h3 : IsWeaklyRegular M rs
h4 : ⊤ ≠ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs) ⊤
⊢ IsRegular M rs'
have refine_1 : ∀ r ∈ rs, Membership.mem (γ := Ideal R) (IsLocalRing.maximalIdeal R) r
Tactic: refine ⟨IsLocalRing.isWeaklyRegular_of_perm_of_subset_maximalIdeal h3 h2 ?_, ?_⟩
-- 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
inst_3 : IsLocalRing R
inst_4 : IsNoetherian R M
rs rs' : List R
h2 : rs ~ rs'
h3 : IsWeaklyRegular M rs
h4 : ⊤ ≠ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs) ⊤
refine_1 : ∀ r ∈ rs, Membership.mem (γ := Ideal R) (IsLocalRing.maximalIdeal R) r
⊢ IsRegular M rs'
have refine_2 : ⊤ ≠ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs') ⊤
Tactic: refine ⟨IsLocalRing.isWeaklyRegular_of_perm_of_subset_maximalIdeal h3 h2 ?_, ?_⟩
-- 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
inst_3 : IsLocalRing R
inst_4 : IsNoetherian R M
rs rs' : List R
h2 : rs ~ rs'
h3 : IsWeaklyRegular M rs
h4 : ⊤ ≠ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs) ⊤
x : R
⊢ x ∈ rs → Membership.mem (γ := Ideal R) (IsLocalRing.maximalIdeal R) x
have refine_1 : ∀ (h6 : Membership.mem (γ := Set R) {r : R | r ∈ rs} x), Membership.mem (γ := Ideal R) (IsLocalRing.maximalIdeal R) x
Tactic: (h6 : x ∈ { r | r ∈ rs })
-- 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
inst_3 : IsLocalRing R
inst_4 : IsNoetherian R M
rs rs' : List R
h2 : rs ~ rs'
h3 : IsWeaklyRegular M rs
h4 : ⊤ ≠ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs) ⊤
x : R
h6 : Membership.mem (γ := Set R) {r : R | r ∈ rs} x
⊢ Membership.mem (γ := Ideal R) (IsLocalRing.maximalIdeal R) x
have refine_1 : Ne.{u_1 + 1} (α := Ideal R) (Ideal.span {r : R | r ∈ rs}) ⊤
Tactic: refine IsLocalRing.le_maximalIdeal ?_ (Ideal.subset_span h6)
-- 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
inst_3 : IsLocalRing R
inst_4 : IsNoetherian R M
rs rs' : List R
h2 : rs ~ rs'
h3 : IsWeaklyRegular M rs
h4 : ⊤ ≠ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs) ⊤
⊢ ⊤ ≠ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs') ⊤
have refine_2 : Eq.{u_1 + 1} (α := Set R) {r : R | r ∈ rs} {r : R | r ∈ rs'}
Tactic: refine ne_of_ne_of_eq h4 (congrArg (Ideal.span · • ⊤) ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_7
inst : CommRing R
inst_1 : IsLocalRing R
L : Type u_8
inst_2 : AddCommGroup L
inst_3 : Module R L
inst_4 : Module.Finite R L
inst_5 : Nontrivial L
x : R
mem : Membership.mem (γ := Ideal R) (maximalIdeal R) x
⊢ Nontrivial.{u_8} (QuotSMulTop x L)
have apply : ⊤ ≠ HSMul.hSMul (β := Submodule R L) x ⊤
Tactic: apply Submodule.Quotient.nontrivial_iff.mpr (Ne.symm _)
-- Lean 4 proof step from Mathlib.RingTheory.RegularLocalRing.Defs (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsRegularLocalRing R
R' : Type u_2
inst_2 : CommRing R'
e : R ≃+* R'
⊢ IsRegularLocalRing R'
have this : IsLocalRing R'
Tactic: have := e.isLocalRing
-- Lean 4 proof step from Mathlib.RingTheory.RegularLocalRing.Defs (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsRegularLocalRing R
R' : Type u_2
inst_2 : CommRing R'
e : R ≃+* R'
this : IsLocalRing R'
⊢ IsRegularLocalRing R'
have this₁ : IsNoetherianRing R'
Tactic: have := isNoetherianRing_of_ringEquiv R e
-- Lean 4 proof step from Mathlib.RingTheory.RegularLocalRing.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsRegularLocalRing R
R' : Type u_2
inst_2 : CommRing R'
e : R ≃+* R'
this_1 : IsLocalRing R'
this : IsNoetherianRing R'
⊢ IsRegularLocalRing R'
have rwa : (↑(Submodule.spanFinrank (maximalIdeal R')) : WithBot ℕ∞) = ringKrullDim R'
Tactic: rwa [isRegularLocalRing_iff, ← ringKrullDim_eq_of_ringEquiv e, ← map_ringEquiv_maximalIdeal e,
    Ideal.spanFinrank_map_eq_of_ringEquiv, ← isRegularLocalRing_iff]
-- Lean 4 proof step from Mathlib.RingTheory.RegularLocalRing.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsRegularLocalRing R
R' : Type u_2
inst_2 : CommRing R'
e : R ≃+* R'
this_1 : IsLocalRing R'
this : IsNoetherianRing R'
rwa : (↑(Submodule.spanFinrank (maximalIdeal R')) : WithBot ℕ∞) = ringKrullDim R'
⊢ IsRegularLocalRing R'
have rwa₁ : (↑(Submodule.spanFinrank (maximalIdeal R')) : WithBot ℕ∞) = ringKrullDim R
Tactic: rwa [isRegularLocalRing_iff, ← ringKrullDim_eq_of_ringEquiv e, ← map_ringEquiv_maximalIdeal e,
    Ideal.spanFinrank_map_eq_of_ringEquiv, ← isRegularLocalRing_iff]
-- Lean 4 proof step from Mathlib.RingTheory.RegularLocalRing.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsRegularLocalRing R
R' : Type u_2
inst_2 : CommRing R'
e : R ≃+* R'
this_1 : IsLocalRing R'
this : IsNoetherianRing R'
rwa : (↑(Submodule.spanFinrank (maximalIdeal R')) : WithBot ℕ∞) = ringKrullDim R'
rwa₁ : (↑(Submodule.spanFinrank (maximalIdeal R')) : WithBot ℕ∞) = ringKrullDim R
⊢ IsRegularLocalRing R'
have rwa₂ : (↑(Submodule.spanFinrank.{u_2, u_2} (R := R') (Ideal.map e (maximalIdeal R))) : WithBot ℕ∞) = ringKrullDim R
Tactic: rwa [isRegularLocalRing_iff, ← ringKrullDim_eq_of_ringEquiv e, ← map_ringEquiv_maximalIdeal e,
    Ideal.spanFinrank_map_eq_of_ringEquiv, ← isRegularLocalRing_iff]
-- Lean 4 proof step from Mathlib.RingTheory.RegularLocalRing.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsRegularLocalRing R
R' : Type u_2
inst_2 : CommRing R'
e : R ≃+* R'
this_1 : IsLocalRing R'
this : IsNoetherianRing R'
rwa : (↑(Submodule.spanFinrank (maximalIdeal R')) : WithBot ℕ∞) = ringKrullDim R'
rwa₁ : (↑(Submodule.spanFinrank (maximalIdeal R')) : WithBot ℕ∞) = ringKrullDim R
rwa₂ : (↑(Submodule.spanFinrank.{u_2, u_2} (R := R') (Ideal.map e (maximalIdeal R))) : WithBot ℕ∞) = ringKrullDim R
⊢ IsRegularLocalRing R'
have rwa₃ : (↑(Submodule.spanFinrank (maximalIdeal R)) : WithBot ℕ∞) = ringKrullDim R
Tactic: rwa [isRegularLocalRing_iff, ← ringKrullDim_eq_of_ringEquiv e, ← map_ringEquiv_maximalIdeal e,
    Ideal.spanFinrank_map_eq_of_ringEquiv, ← isRegularLocalRing_iff]
-- Lean 4 proof step from Mathlib.RingTheory.RegularLocalRing.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
⊢ IsRegularLocalRing R ↔
    (↑(Module.finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R)) : WithBot ℕ∞) = ringKrullDim R
have rw : (↑(Submodule.spanFinrank (maximalIdeal R)) : WithBot ℕ∞) = ringKrullDim R ↔
  (↑(Module.finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R)) : WithBot ℕ∞) = ringKrullDim R
Tactic: rw [isRegularLocalRing_iff, spanFinrank_maximalIdeal_eq_finrank_cotangentSpace]
-- Lean 4 proof step from Mathlib.RingTheory.RegularLocalRing.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
rw :
  (↑(Submodule.spanFinrank (maximalIdeal R)) : WithBot ℕ∞) = ringKrullDim R ↔
    (↑(Module.finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R)) : WithBot ℕ∞) = ringKrullDim R
⊢ IsRegularLocalRing R ↔
    (↑(Module.finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R)) : WithBot ℕ∞) = ringKrullDim R
have rw₁ : (↑(Module.finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R)) : WithBot ℕ∞) = ringKrullDim R ↔
  (↑(Module.finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R)) : WithBot ℕ∞) = ringKrullDim R
Tactic: rw [isRegularLocalRing_iff, spanFinrank_maximalIdeal_eq_finrank_cotangentSpace]
-- Lean 4 proof step from Mathlib.RingTheory.RegularLocalRing.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsPrincipalIdealRing R
⊢ IsRegularLocalRing R
have pos : ∀ (isf : IsField R), IsRegularLocalRing R
Tactic: by_cases isf : IsField R
-- Lean 4 proof step from Mathlib.RingTheory.RegularLocalRing.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsPrincipalIdealRing R
pos : ∀ (isf : IsField R), IsRegularLocalRing R
⊢ IsRegularLocalRing R
have neg : ∀ (isf : ¬IsField R), IsRegularLocalRing R
Tactic: by_cases isf : IsField R
-- Lean 4 proof step from Mathlib.RingTheory.RegularLocalRing.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsPrincipalIdealRing R
isf : ¬IsField R
⊢ IsRegularLocalRing R
have neg : (↑(Submodule.spanFinrank (maximalIdeal R)) : WithBot ℕ∞) ≤ ringKrullDim R
Tactic: apply of_spanFinrank_maximalIdeal_le
-- Lean 4 proof step from Mathlib.RingTheory.RegularLocalRing.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsPrincipalIdealRing R
isf : ¬IsField R
⊢ (↑(Submodule.spanFinrank (maximalIdeal R)) : WithBot ℕ∞) ≤ ringKrullDim R
have neg : ∀ (x : R) (hx : Eq (α := Submodule R R) (maximalIdeal R) (R ∙ x)),
  (↑(Submodule.spanFinrank (maximalIdeal R)) : WithBot ℕ∞) ≤ ringKrullDim R
Tactic: rcases IsPrincipalIdealRing.principal (maximalIdeal R) with ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.RingTheory.RegularLocalRing.Defs (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
R' : Type u_2
inst_1 : CommRing R'
e : R ≃+* R'
inst_2 : IsRegularRing R
⊢ IsRegularRing R'
have this : IsNoetherianRing R'
Tactic: have := isNoetherianRing_of_ringEquiv R e
-- Lean 4 proof step from Mathlib.RingTheory.RegularLocalRing.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
R' : Type u_2
inst_1 : CommRing R'
e : R ≃+* R'
inst_2 : IsRegularRing R
this : IsNoetherianRing R'
⊢ IsRegularRing R'
have rw : ∀ (p : Ideal R') [inst : p.IsPrime], IsRegularLocalRing.{u_2} (Localization.AtPrime p)
Tactic: rw [isRegularRing_iff]
-- Lean 4 proof step from Mathlib.RingTheory.RegularLocalRing.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
⊢ IsRegularRing R
have rw : ∀ (p : Ideal R) [inst_2 : p.IsPrime], IsRegularLocalRing.{u_1} (Localization.AtPrime p)
Tactic: rw [isRegularRing_iff]
-- Lean 4 proof step from Mathlib.RingTheory.RegularLocalRing.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
p : Ideal R
hp : p.IsPrime
⊢ IsRegularLocalRing.{u_1} (Localization.AtPrime p)
have pos : ∀ (eqbot : p = ⊥), IsRegularLocalRing.{u_1} (Localization.AtPrime p)
Tactic: by_cases eqbot : p = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.RegularLocalRing.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
p : Ideal R
hp : p.IsPrime
pos : ∀ (eqbot : p = ⊥), IsRegularLocalRing.{u_1} (Localization.AtPrime p)
⊢ IsRegularLocalRing.{u_1} (Localization.AtPrime p)
have neg : ∀ (eqbot : ¬p = ⊥), IsRegularLocalRing.{u_1} (Localization.AtPrime p)
Tactic: by_cases eqbot : p = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.RegularLocalRing.Defs (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
p : Ideal R
hp : p.IsPrime
eqbot : ¬p = ⊥
⊢ IsRegularLocalRing.{u_1} (Localization.AtPrime p)
have this : IsDiscreteValuationRing.{u_1} (Localization.AtPrime p)
Tactic: have := IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain
      R eqbot (Localization.AtPrime p)
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.EssFiniteType (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.EssFiniteType
hg : g.EssFiniteType
⊢ (g.comp f).EssFiniteType
have algebraizeInst : Algebra.EssFiniteType R S
Tactic: algebraize [f, g, g.comp f]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.EssFiniteType (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.EssFiniteType
hg : g.EssFiniteType
algebraizeInst : Algebra.EssFiniteType R S
⊢ (g.comp f).EssFiniteType
have algebraizeInst₁ : Algebra.EssFiniteType S T
Tactic: algebraize [f, g, g.comp f]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.EssFiniteType (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.EssFiniteType
⊢ (g.comp f).EssFiniteType ↔ g.EssFiniteType
have algebraizeInst : Algebra.EssFiniteType R S
Tactic: algebraize [f, g, g.comp f]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.EssFiniteType (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
h : (g.comp f).EssFiniteType
⊢ g.EssFiniteType
have algebraizeInst : Algebra.EssFiniteType R T
Tactic: algebraize [f, g, g.comp f]