awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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₂ : List R
a b : R
t rs₀ : List R
H₃ : rs₀ ++ a :: b :: t <+~ rs
h :
  IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) [b, a] ∧
    IsWeaklyRegular.{u_1, u_3}
      ((M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) ⧸
        HSMul.hSMul (α := Ideal R) (β :=
          Submodule R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤)) (Ideal.ofList [a, b])
          ⊤)
      t
this : Eq (α := Ideal R) (Ideal.ofList [b, a]) (Ideal.ofList [a, b])
H₁ : [b, a] ++ rs₀ <+~ rs
⊢ IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) [a, b] ∧
    IsWeaklyRegular.{u_1, u_3}
      ((M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) ⧸
        HSMul.hSMul (α := Ideal R) (β :=
          Submodule R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤)) (Ideal.ofList [a, b])
          ⊤)
      t

Tactic:
h.imp_left (swap · (h' b a rs₀ H₁))

Premises used: _private.0.RingTheory.Sequence.IsWeaklyRegular.swap, And.imp_left
-- 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
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₂ : List R
a b : R
t rs₀ : List R
H₃ : rs₀ ++ a :: b :: t <+~ rs
h :
  IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) [b, a] ∧
    IsWeaklyRegular.{u_1, u_3}
      ((M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) ⧸
        HSMul.hSMul (α := Ideal R) (β :=
          Submodule R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤)) (Ideal.ofList [a, b])
          ⊤)
      t
this : Eq (α := Ideal R) (Ideal.ofList [b, a]) (Ideal.ofList [a, b])
H₁ : [b, a] ++ rs₀ <+~ rs
⊢ IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) [a, b] ∧
    IsWeaklyRegular.{u_1, u_3}
      ((M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) ⧸
        HSMul.hSMul (α := Ideal R) (β :=
          Submodule R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤)) (Ideal.ofList [a, b])
          ⊤)
      t

Tactic:
exact h.imp_left (swap · (h' b a rs₀ H₁))

Premises used: _private.0.RingTheory.Sequence.IsWeaklyRegular.swap, And.imp_left
-- 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
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₂ l₁ l₂ l₃ : List R
h₁₂ : l₁ ~ l₂
h_2 : 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₂
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₀ ++ l₁ <+~ rs
H₃ : rs₀ ++ l₃ <+~ rs
h : IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) l₁
⊢ rs₀ ++ l₂ <+~ rs

Tactic:
have H₂ := (h₁₂.append_left rs₀).subperm_right.mp H₁
-- 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
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₂ l₁ l₂ l₃ : List R
h₁₂ : l₁ ~ l₂
h_2 : 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₂
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₀ ++ l₁ <+~ rs
H₃ : rs₀ ++ l₃ <+~ rs
h : IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) l₁
H₂ : rs₀ ++ l₂ <+~ rs
⊢ IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) l₃

Tactic:
ih₂₃ rs₀ H₂ H₃ (ih₁₂ rs₀ H₁ H₂ h)
-- 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
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₂ l₁ l₂ l₃ : List R
h₁₂ : l₁ ~ l₂
h_2 : 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₂
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₀ ++ l₁ <+~ rs
H₃ : rs₀ ++ l₃ <+~ rs
h : IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) l₁
H₂ : rs₀ ++ l₂ <+~ rs
⊢ IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) l₃

Tactic:
exact ih₂₃ rs₀ H₂ H₃ (ih₁₂ rs₀ H₁ H₂ h)
-- 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
inst_3 : IsNoetherian R M
rs rs' : List R
h1 : IsWeaklyRegular M rs
h2 : rs ~ rs'
h3 : ∀ r ∈ rs, Membership.mem (γ := Ideal R) (Ideal.jacobson (Module.annihilator R M)) r
⊢ IsWeaklyRegular M rs'

Tactic:
h1.prototype_perm h2 fun r _ _ h h' =>
    eq_bot_of_eq_pointwise_smul_of_mem_jacobson_annihilator
      (IsNoetherian.noetherian _) h'
      (Ideal.jacobson_mono
        (le_trans
          -- The named argument `(R := R)` below isn't necessary, but
          -- typechecking is much slower without it
          (LinearMap.annihilator_le_of_surjective (R := R) _ (mkQ_surjective _))
          (LinearMap.annihilator_le_of_injective _ (injective_subtype _)))
        (h3 r (h.subset List.mem_cons_self)))

Premises used: Submodule.torsionBy, IsNoetherian.noetherian, LinearMap.annihilator_le_of_injective, RingTheory.Sequence.IsWeaklyRegular.prototype_perm, Submodule.injective_subtype, HasQuotient.Quotient, Ideal.jacobson_mono, Ideal.ofList, Submodule.subtype, Submodule.mkQ, HSMul.hSMul, Submodule.mkQ_surjective, List.mem_cons_self, LinearMap.annihilator_le_of_surjective, List.Subperm.subset, Top.top, Submodule.eq_bot_of_eq_pointwise_smul_of_mem_jacobson_annihilator, le_trans
-- 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
inst_3 : IsNoetherian R M
rs rs' : List R
h1 : IsRegular M rs
h2 : rs ~ rs'
h3 : ∀ r ∈ rs, Membership.mem (γ := Ideal R) (Ideal.jacobson (Module.annihilator R M)) r
⊢ IsRegular M rs'

Tactic:
⟨h1.toIsWeaklyRegular.of_perm_of_subset_jacobson_annihilator h2 h3,
    letI := h1.nontrivial
    top_ne_ideal_smul_of_le_jacobson_annihilator <|
      Ideal.span_le.mpr (h3 · <| h2.mem_iff.mpr ·)⟩

Premises used: Ideal.span_le, Iff.mpr, RingTheory.Sequence.IsWeaklyRegular.of_perm_of_subset_jacobson_annihilator, RingTheory.Sequence.IsRegular.mk, Submodule.top_ne_ideal_smul_of_le_jacobson_annihilator, RingTheory.Sequence.IsRegular.toIsWeaklyRegular, List.Perm.mem_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
inst_3 : IsLocalRing R
inst_4 : IsNoetherian R M
rs rs' : List R
h1 : IsWeaklyRegular M rs
h2 : rs ~ rs'
h3 : ∀ r ∈ rs, Membership.mem (γ := Ideal R) (IsLocalRing.maximalIdeal R) r
⊢ IsWeaklyRegular M rs'

Tactic:
IsWeaklyRegular.of_perm_of_subset_jacobson_annihilator h1 h2 fun r hr =>
    IsLocalRing.maximalIdeal_le_jacobson _ (h3 r hr)

Premises used: Module.annihilator, IsLocalRing.maximalIdeal_le_jacobson, RingTheory.Sequence.IsWeaklyRegular.of_perm_of_subset_jacobson_annihilator
-- 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
inst_3 : IsLocalRing R
inst_4 : IsNoetherian R M
rs rs' : List R
h1 : IsRegular M rs
h2 : rs ~ rs'
⊢ IsWeaklyRegular M rs

Tactic:
obtain ⟨h3, h4⟩ := h1
-- 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
inst_3 : IsLocalRing R
inst_4 : IsNoetherian R M
rs rs' : List R
h1 : IsRegular M rs
h2 : rs ~ rs'
h3 : IsWeaklyRegular M rs
⊢ ⊤ ≠ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs) ⊤

Tactic:
obtain ⟨h3, h4⟩ := h1
-- 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
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'

Tactic:
⟨IsLocalRing.isWeaklyRegular_of_perm_of_subset_maximalIdeal h3 h2 ?_, ?_⟩

Premises used: RingTheory.Sequence.IsRegular.mk, IsLocalRing.isWeaklyRegular_of_perm_of_subset_maximalIdeal
-- 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
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
refine_2 : ⊤ ≠ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs') ⊤
⊢ IsRegular M rs'

Tactic:
refine ⟨IsLocalRing.isWeaklyRegular_of_perm_of_subset_maximalIdeal h3 h2 ?_, ?_⟩
-- 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
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
refine_1 :
  ∀ (h6 : Membership.mem (γ := Set R) {r : R | r ∈ rs} x), Membership.mem (γ := Ideal R) (IsLocalRing.maximalIdeal R) x
⊢ x ∈ rs → Membership.mem (γ := Ideal R) (IsLocalRing.maximalIdeal R) x

Tactic:
(h6 : x ∈ { r | r ∈ rs })
-- 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
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

Tactic:
IsLocalRing.le_maximalIdeal ?_ (Ideal.subset_span h6)

Premises used: Ideal.subset_span, Set.Mem, IsLocalRing.le_maximalIdeal
-- 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
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
refine_1 : Ne.{u_1 + 1} (α := Ideal R) (Ideal.span {r : R | r ∈ rs}) ⊤
⊢ Membership.mem (γ := Ideal R) (IsLocalRing.maximalIdeal R) x

Tactic:
refine IsLocalRing.le_maximalIdeal ?_ (Ideal.subset_span h6)

Premises used: Ideal.subset_span, IsLocalRing.le_maximalIdeal
-- 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
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
⊢ Ne.{u_1 + 1} (α := Ideal R) (Ideal.span {r : R | r ∈ rs}) ⊤

Tactic:
h4 ∘ Eq.trans (top_smul _).symm ∘ Eq.symm ∘ congrArg (· • ⊤)

Premises used: congrArg, Function.comp, HSMul.hSMul, Submodule.top_smul, Top.top, Eq.symm, Not, Eq.trans
-- 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
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
⊢ Ne.{u_1 + 1} (α := Ideal R) (Ideal.span {r : R | r ∈ rs}) ⊤

Tactic:
exact h4 ∘ Eq.trans (top_smul _).symm ∘ Eq.symm ∘ congrArg (· • ⊤)

Premises used: congrArg, HSMul.hSMul, Submodule.top_smul, Top.top, Eq.symm, Eq.trans
-- 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
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') ⊤

Tactic:
ne_of_ne_of_eq h4 (congrArg (Ideal.span · • ⊤) ?_)

Premises used: congrArg, HSMul.hSMul, Ideal.span, Top.top, ne_of_ne_of_eq
-- 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
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_2 : Eq.{u_1 + 1} (α := Set R) {r : R | r ∈ rs} {r : R | r ∈ rs'}
⊢ ⊤ ≠ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs') ⊤

Tactic:
refine ne_of_ne_of_eq h4 (congrArg (Ideal.span · • ⊤) ?_)

Premises used: congrArg, HSMul.hSMul, Ideal.span, Top.top, ne_of_ne_of_eq
-- 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
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) ⊤
⊢ Eq.{u_1 + 1} (α := Set R) {r : R | r ∈ rs} {r : R | r ∈ rs'}

Tactic:
Set.ext fun _ => h2.mem_iff

Premises used: Set.ext, List.Perm.mem_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
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) ⊤
⊢ Eq.{u_1 + 1} (α := Set R) {r : R | r ∈ rs} {r : R | r ∈ rs'}

Tactic:
exact Set.ext fun _ => h2.mem_iff

Premises used: Set.ext, List.Perm.mem_iff
-- Module: Mathlib.RingTheory.Regular.RegularSequence
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
apply : ⊤ ≠ HSMul.hSMul (β := Submodule R L) x ⊤
⊢ Nontrivial.{u_8} (QuotSMulTop x L)

Tactic:
apply Submodule.Quotient.nontrivial_iff.mpr (Ne.symm _)

Premises used: Iff.mpr, Ne.symm, Submodule.Quotient.nontrivial_iff
-- Module: Mathlib.RingTheory.Regular.RegularSequence
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
⊢ ⊤ ≠ HSMul.hSMul (β := Submodule R L) x ⊤

Tactic:
Submodule.top_ne_pointwise_smul_of_mem_jacobson_annihilator (maximalIdeal_le_jacobson _ mem)

Premises used: IsLocalRing.maximalIdeal_le_jacobson, Submodule.top_ne_pointwise_smul_of_mem_jacobson_annihilator
-- Module: Mathlib.RingTheory.Regular.RegularSequence
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
⊢ ⊤ ≠ HSMul.hSMul (β := Submodule R L) x ⊤

Tactic:
exact Submodule.top_ne_pointwise_smul_of_mem_jacobson_annihilator (maximalIdeal_le_jacobson _ mem)

Premises used: IsLocalRing.maximalIdeal_le_jacobson, Submodule.top_ne_pointwise_smul_of_mem_jacobson_annihilator
-- Module: Mathlib.RingTheory.Regular.RegularSequence
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
rs : List R
mem : ∀ r ∈ rs, Membership.mem (γ := Ideal R) (maximalIdeal R) r
reg : IsWeaklyRegular L rs
⊢ IsRegular L rs

Tactic:
⟨reg, Submodule.top_ne_ideal_smul_of_le_jacobson_annihilator
    ((Ideal.span_le.mpr mem).trans (maximalIdeal_le_jacobson _))⟩

Premises used: Ideal.span_le, Iff.mpr, IsLocalRing.maximalIdeal_le_jacobson, RingTheory.Sequence.IsRegular.mk, LE.le.trans, Submodule.top_ne_ideal_smul_of_le_jacobson_annihilator
-- Module: Mathlib.RingTheory.RegularLocalRing.Defs
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
⊢ IsRegularLocalRing R ↔ (↑(Submodule.spanFinrank (maximalIdeal R)) : WithBot ℕ∞) = ringKrullDim R

Tactic:
⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩

Premises used: IsRegularLocalRing.mk, IsLocalRing.maximalIdeal, Nat.cast, Submodule.spanFinrank, Iff.intro, ringKrullDim, Eq, _private.0.isRegularLocalRing_iff.match_1
-- Module: Mathlib.RingTheory.RegularLocalRing.Defs
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
le : (↑(Submodule.spanFinrank (maximalIdeal R)) : WithBot ℕ∞) ≤ ringKrullDim R
⊢ IsRegularLocalRing R

Tactic:
(isRegularLocalRing_iff _).mpr (le_antisymm le (ringKrullDim_le_spanFinrank_maximalIdeal R))

Premises used: Iff.mpr, ringKrullDim_le_spanFinrank_maximalIdeal, le_antisymm, isRegularLocalRing_iff
-- Module: Mathlib.RingTheory.RegularLocalRing.Defs
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsRegularLocalRing R
R' : Type u_2
inst_2 : CommRing R'
e : R ≃+* R'
⊢ IsLocalRing R'

Tactic:
have := e.isLocalRing
-- Module: Mathlib.RingTheory.RegularLocalRing.Defs
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'
⊢ IsNoetherianRing R'

Tactic:
have := isNoetherianRing_of_ringEquiv R e
-- Module: Mathlib.RingTheory.RegularLocalRing.Defs
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
rwa₃ : (↑(Submodule.spanFinrank (maximalIdeal R)) : WithBot ℕ∞) = ringKrullDim R
rwa₄ rwa₅ rwa₆ rwa₇ : IsRegularLocalRing R
⊢ IsRegularLocalRing R'

Tactic:
rwa [isRegularLocalRing_iff, ← ringKrullDim_eq_of_ringEquiv e, ← map_ringEquiv_maximalIdeal e,
    Ideal.spanFinrank_map_eq_of_ringEquiv, ← isRegularLocalRing_iff]

Premises used: ringKrullDim_eq_of_ringEquiv, isRegularLocalRing_iff, IsLocalRing.map_ringEquiv_maximalIdeal, Ideal.spanFinrank_map_eq_of_ringEquiv
-- Module: Mathlib.RingTheory.RegularLocalRing.Defs
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
rw₁ 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
⊢ IsRegularLocalRing R ↔
    (↑(Module.finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R)) : WithBot ℕ∞) = ringKrullDim R

Tactic:
rw [isRegularLocalRing_iff, spanFinrank_maximalIdeal_eq_finrank_cotangentSpace]

Premises used: isRegularLocalRing_iff, IsLocalRing.spanFinrank_maximalIdeal_eq_finrank_cotangentSpace
-- Module: Mathlib.RingTheory.RegularLocalRing.Defs
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
neg : ∀ (isf : ¬IsField R), IsRegularLocalRing R
⊢ IsRegularLocalRing R

Tactic:
by_cases isf : IsField R

Premises used: IsField
-- Module: Mathlib.RingTheory.RegularLocalRing.Defs
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsPrincipalIdealRing R
isf : IsField R
this : Field R := isf.toField
⊢ IsRegularLocalRing R

Tactic:
simp [isRegularLocalRing_iff, maximalIdeal_eq_bot]

Premises used: IsLocalRing.maximalIdeal_eq_bot, isRegularLocalRing_iff
-- Module: Mathlib.RingTheory.RegularLocalRing.Defs
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsPrincipalIdealRing R
isf : ¬IsField R
neg : (↑(Submodule.spanFinrank (maximalIdeal R)) : WithBot ℕ∞) ≤ ringKrullDim R
⊢ IsRegularLocalRing R

Tactic:
apply of_spanFinrank_maximalIdeal_le

Premises used: IsRegularLocalRing.of_spanFinrank_maximalIdeal_le