awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Regular.Category
Goal:
R : Type u
inst : CommRing R
M : ModuleCat.{v, u} R
r : R
⊢ Epi (M.smulShortComplex r).g

Tactic:
simpa [smulShortComplex, ModuleCat.epi_iff_surjective] using Submodule.mkQ_surjective _

Premises used: ModuleCat.epi_iff_surjective, Submodule.mkQ_surjective, ModuleCat.smulShortComplex
-- Module: Mathlib.RingTheory.Regular.Category
Goal:
R : Type u
inst : CommRing R
M : ModuleCat.{v, u} R
r : R
reg : IsSMulRegular.{u, v} (↑M : Type v) r
⊢ Mono (M.smulShortComplex r).f

Tactic:
simpa [ModuleCat.smulShortComplex, ModuleCat.mono_iff_injective] using reg

Premises used: ModuleCat.mono_iff_injective, ModuleCat.smulShortComplex
-- Module: Mathlib.RingTheory.Regular.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Flat R S
M : Type u_3
N : Type u_4
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
inst_8 : Module S N
inst_9 : IsScalarTower R S N
f : M →ₗ[R] N
hf : IsBaseChange S f
reg : IsWeaklyRegular.{u_1, u_3} (R := R) M []
⊢ IsWeaklyRegular.{u_2, u_4} (R := S) N (List.map.{u_1, u_2} (α := R) (⇑(algebraMap R S) : (a : R) → S) [])

Tactic:
simp
-- Module: Mathlib.RingTheory.Regular.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Flat R S
x : R
tail : List R
ih :
  ∀ {M : Type u_3} {N : Type u_4} [inst_10 : AddCommGroup M] [inst_11 : Module R M] [inst_12 : AddCommGroup N]
    [inst_13 : Module R N] [inst_14 : Module S N] [inst_15 : IsScalarTower R S N] {f : M →ₗ[R] N}
    (hf : IsBaseChange S f) (reg : IsWeaklyRegular M tail),
    IsWeaklyRegular.{u_2, u_4} (R := S) N (List.map (⇑(algebraMap R S) : (a : R) → S) tail)
M : Type u_3
N : Type u_4
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
inst_8 : Module S N
inst_9 : IsScalarTower R S N
f : M →ₗ[R] N
hf : IsBaseChange S f
reg : IsWeaklyRegular M (x :: tail)
cons :
  ∀ (reg : IsSMulRegular M x ∧ IsWeaklyRegular.{u_1, u_3} (QuotSMulTop x M) tail),
    IsSMulRegular.{u_2, u_4} (R := S) N ((algebraMap R S : (a : R) → S) x : S) ∧
      IsWeaklyRegular.{u_2, u_4} (R := S) (QuotSMulTop.{u_4, u_2} (R := S) ((algebraMap R S : (a : R) → S) x : S) N)
        (List.map (⇑(algebraMap R S) : (a : R) → S) tail)
⊢ IsWeaklyRegular.{u_2, u_4} (R := S) N (List.map (⇑(algebraMap R S) : (a : R) → S) (x :: tail))

Tactic:
simp only [List.map_cons, isWeaklyRegular_cons_iff] at reg ⊢

Premises used: RingTheory.Sequence.isWeaklyRegular_cons_iff, List.map_cons
-- Module: Mathlib.RingTheory.Regular.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Flat R S
x : R
tail : List R
ih :
  ∀ {M : Type u_3} {N : Type u_4} [inst_10 : AddCommGroup M] [inst_11 : Module R M] [inst_12 : AddCommGroup N]
    [inst_13 : Module R N] [inst_14 : Module S N] [inst_15 : IsScalarTower R S N] {f : M →ₗ[R] N}
    (hf : IsBaseChange S f) (reg : IsWeaklyRegular M tail),
    IsWeaklyRegular.{u_2, u_4} (R := S) N (List.map (⇑(algebraMap R S) : (a : R) → S) tail)
M : Type u_3
N : Type u_4
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
inst_8 : Module S N
inst_9 : IsScalarTower R S N
f : M →ₗ[R] N
hf : IsBaseChange S f
reg : IsSMulRegular M x ∧ IsWeaklyRegular.{u_1, u_3} (QuotSMulTop x M) tail
cons :
  ∀
    (e :
      TensorProduct.{u_1, u_2, u_3} R S (QuotSMulTop x M) ≃ₗ[S]
        QuotSMulTop.{u_4, u_2} (R := S) ((algebraMap R S : (a : R) → S) x : S) N),
    IsSMulRegular.{u_2, u_4} (R := S) N ((algebraMap R S : (a : R) → S) x : S) ∧
      IsWeaklyRegular.{u_2, u_4} (R := S) (QuotSMulTop.{u_4, u_2} (R := S) ((algebraMap R S : (a : R) → S) x : S) N)
        (List.map (⇑(algebraMap R S) : (a : R) → S) tail)
⊢ IsSMulRegular.{u_2, u_4} (R := S) N ((algebraMap R S : (a : R) → S) x : S) ∧
    IsWeaklyRegular.{u_2, u_4} (R := S) (QuotSMulTop.{u_4, u_2} (R := S) ((algebraMap R S : (a : R) → S) x : S) N)
      (List.map (⇑(algebraMap R S) : (a : R) → S) tail)

Tactic:
have e := (QuotSMulTop.algebraMapTensorEquivTensorQuotSMulTop x M S).symm ≪≫ₗ
      QuotSMulTop.congr ((algebraMap R S) x) hf.equiv
-- Module: Mathlib.RingTheory.Regular.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Flat R S
x : R
tail : List R
ih :
  ∀ {M : Type u_3} {N : Type u_4} [inst_10 : AddCommGroup M] [inst_11 : Module R M] [inst_12 : AddCommGroup N]
    [inst_13 : Module R N] [inst_14 : Module S N] [inst_15 : IsScalarTower R S N] {f : M →ₗ[R] N}
    (hf : IsBaseChange S f) (reg : IsWeaklyRegular M tail),
    IsWeaklyRegular.{u_2, u_4} (R := S) N (List.map (⇑(algebraMap R S) : (a : R) → S) tail)
M : Type u_3
N : Type u_4
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
inst_8 : Module S N
inst_9 : IsScalarTower R S N
f : M →ₗ[R] N
hf : IsBaseChange S f
reg : IsSMulRegular M x ∧ IsWeaklyRegular.{u_1, u_3} (QuotSMulTop x M) tail
e :
  TensorProduct.{u_1, u_2, u_3} R S (QuotSMulTop x M) ≃ₗ[S]
    QuotSMulTop.{u_4, u_2} (R := S) ((algebraMap R S : (a : R) → S) x : S) N
x_1 : QuotSMulTop x M
⊢ Eq.{u_4 + 1} (α := QuotSMulTop.{u_4, u_2} (R := S) ((algebraMap R S : (a : R) → S) x : S) N)
    ((e : (a : TensorProduct R S (QuotSMulTop x M)) → QuotSMulTop ((algebraMap R S : (a : R) → S) x) N) (1 ⊗ₜ[R] x_1) :
      QuotSMulTop.{u_4, u_2} (R := S) ((algebraMap R S : (a : R) → S) x : S) N)
    (((↑R :
                {S : Type u_2} →
                  {M : Type (max u_2 u_3)} →
                    {M₂ : Type u_4} →
                      [inst : Semiring R] →
                        [inst_10 : Semiring S] →
                          [inst_11 : AddCommMonoid M] →
                            [inst_12 : AddCommMonoid M₂] →
                              [inst_13 : Module R M] →
                                [inst_14 : Module R M₂] →
                                  [inst_15 : Module S M] →
                                    [inst_16 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (↑e : TensorProduct R S (QuotSMulTop x M) →ₗ[S] QuotSMulTop ((algebraMap R S : (a : R) → S) x) N) ∘ₗ
            (TensorProduct.mk R S (QuotSMulTop x M) :
                (a : S) → QuotSMulTop x M →ₗ[R] TensorProduct R S (QuotSMulTop x M))
              1 :
          (a : QuotSMulTop x M) → QuotSMulTop ((algebraMap R S : (a : R) → S) x) N)
        x_1 :
      QuotSMulTop.{u_4, u_2} (R := S) ((algebraMap R S : (a : R) → S) x : S) N)

Tactic:
simp
-- Module: Mathlib.RingTheory.Regular.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Flat R S
x : R
tail : List R
ih :
  ∀ {M : Type u_3} {N : Type u_4} [inst_10 : AddCommGroup M] [inst_11 : Module R M] [inst_12 : AddCommGroup N]
    [inst_13 : Module R N] [inst_14 : Module S N] [inst_15 : IsScalarTower R S N] {f : M →ₗ[R] N}
    (hf : IsBaseChange S f) (reg : IsWeaklyRegular M tail),
    IsWeaklyRegular.{u_2, u_4} (R := S) N (List.map (⇑(algebraMap R S) : (a : R) → S) tail)
M : Type u_3
N : Type u_4
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
inst_8 : Module S N
inst_9 : IsScalarTower R S N
f : M →ₗ[R] N
hf : IsBaseChange S f
reg : IsSMulRegular M x ∧ IsWeaklyRegular.{u_1, u_3} (QuotSMulTop x M) tail
e :
  TensorProduct.{u_1, u_2, u_3} R S (QuotSMulTop x M) ≃ₗ[S]
    QuotSMulTop.{u_4, u_2} (R := S) ((algebraMap R S : (a : R) → S) x : S) N
⊢ IsBaseChange.{u_3, u_4, u_2, u_1} (M := QuotSMulTop x M) S
    ((↑R :
          {S : Type u_2} →
            {M : Type (max u_2 u_3)} →
              {M₂ : Type u_4} →
                [inst : Semiring R] →
                  [inst_10 : Semiring S] →
                    [inst_11 : AddCommMonoid M] →
                      [inst_12 : AddCommMonoid M₂] →
                        [inst_13 : Module R M] →
                          [inst_14 : Module R M₂] →
                            [inst_15 : Module S M] →
                              [inst_16 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (↑e : TensorProduct R S (QuotSMulTop x M) →ₗ[S] QuotSMulTop ((algebraMap R S : (a : R) → S) x) N) ∘ₗ
      (TensorProduct.mk R S (QuotSMulTop x M) : (a : S) → QuotSMulTop x M →ₗ[R] TensorProduct R S (QuotSMulTop x M)) 1)

Tactic:
have hg : IsBaseChange S <|
        e.toLinearMap.restrictScalars R ∘ₗ TensorProduct.mk R S (QuotSMulTop x M) 1 :=
      IsBaseChange.of_equiv e (fun _ ↦ by simp)
-- Module: Mathlib.RingTheory.Regular.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Flat R S
x : R
tail : List R
ih :
  ∀ {M : Type u_3} {N : Type u_4} [inst_10 : AddCommGroup M] [inst_11 : Module R M] [inst_12 : AddCommGroup N]
    [inst_13 : Module R N] [inst_14 : Module S N] [inst_15 : IsScalarTower R S N] {f : M →ₗ[R] N}
    (hf : IsBaseChange S f) (reg : IsWeaklyRegular M tail),
    IsWeaklyRegular.{u_2, u_4} (R := S) N (List.map (⇑(algebraMap R S) : (a : R) → S) tail)
M : Type u_3
N : Type u_4
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
inst_8 : Module S N
inst_9 : IsScalarTower R S N
f : M →ₗ[R] N
hf : IsBaseChange S f
reg : IsSMulRegular M x ∧ IsWeaklyRegular.{u_1, u_3} (QuotSMulTop x M) tail
e :
  TensorProduct.{u_1, u_2, u_3} R S (QuotSMulTop x M) ≃ₗ[S]
    QuotSMulTop.{u_4, u_2} (R := S) ((algebraMap R S : (a : R) → S) x : S) N
hg :
  IsBaseChange.{u_3, u_4, u_2, u_1} (M := QuotSMulTop x M) S
    ((↑R :
          {S : Type u_2} →
            {M : Type (max u_2 u_3)} →
              {M₂ : Type u_4} →
                [inst : Semiring R] →
                  [inst_10 : Semiring S] →
                    [inst_11 : AddCommMonoid M] →
                      [inst_12 : AddCommMonoid M₂] →
                        [inst_13 : Module R M] →
                          [inst_14 : Module R M₂] →
                            [inst_15 : Module S M] →
                              [inst_16 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (↑e : TensorProduct R S (QuotSMulTop x M) →ₗ[S] QuotSMulTop ((algebraMap R S : (a : R) → S) x) N) ∘ₗ
      (TensorProduct.mk R S (QuotSMulTop x M) : (a : S) → QuotSMulTop x M →ₗ[R] TensorProduct R S (QuotSMulTop x M)) 1)
⊢ IsSMulRegular.{u_2, u_4} (R := S) N ((algebraMap R S : (a : R) → S) x : S) ∧
    IsWeaklyRegular.{u_2, u_4} (R := S) (QuotSMulTop.{u_4, u_2} (R := S) ((algebraMap R S : (a : R) → S) x : S) N)
      (List.map (⇑(algebraMap R S) : (a : R) → S) tail)

Tactic:
⟨reg.1.of_flat_of_isBaseChange hf, ih hg reg.2⟩

Premises used: And.right, IsSMulRegular.of_flat_of_isBaseChange, And.left, And.intro
-- Module: Mathlib.RingTheory.Regular.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Flat R S
x : R
tail : List R
ih :
  ∀ {M : Type u_3} {N : Type u_4} [inst_10 : AddCommGroup M] [inst_11 : Module R M] [inst_12 : AddCommGroup N]
    [inst_13 : Module R N] [inst_14 : Module S N] [inst_15 : IsScalarTower R S N] {f : M →ₗ[R] N}
    (hf : IsBaseChange S f) (reg : IsWeaklyRegular M tail),
    IsWeaklyRegular.{u_2, u_4} (R := S) N (List.map (⇑(algebraMap R S) : (a : R) → S) tail)
M : Type u_3
N : Type u_4
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
inst_8 : Module S N
inst_9 : IsScalarTower R S N
f : M →ₗ[R] N
hf : IsBaseChange S f
reg : IsSMulRegular M x ∧ IsWeaklyRegular.{u_1, u_3} (QuotSMulTop x M) tail
e :
  TensorProduct.{u_1, u_2, u_3} R S (QuotSMulTop x M) ≃ₗ[S]
    QuotSMulTop.{u_4, u_2} (R := S) ((algebraMap R S : (a : R) → S) x : S) N
hg :
  IsBaseChange.{u_3, u_4, u_2, u_1} (M := QuotSMulTop x M) S
    ((↑R :
          {S : Type u_2} →
            {M : Type (max u_2 u_3)} →
              {M₂ : Type u_4} →
                [inst : Semiring R] →
                  [inst_10 : Semiring S] →
                    [inst_11 : AddCommMonoid M] →
                      [inst_12 : AddCommMonoid M₂] →
                        [inst_13 : Module R M] →
                          [inst_14 : Module R M₂] →
                            [inst_15 : Module S M] →
                              [inst_16 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (↑e : TensorProduct R S (QuotSMulTop x M) →ₗ[S] QuotSMulTop ((algebraMap R S : (a : R) → S) x) N) ∘ₗ
      (TensorProduct.mk R S (QuotSMulTop x M) : (a : S) → QuotSMulTop x M →ₗ[R] TensorProduct R S (QuotSMulTop x M)) 1)
⊢ IsSMulRegular.{u_2, u_4} (R := S) N ((algebraMap R S : (a : R) → S) x : S) ∧
    IsWeaklyRegular.{u_2, u_4} (R := S) (QuotSMulTop.{u_4, u_2} (R := S) ((algebraMap R S : (a : R) → S) x : S) N)
      (List.map (⇑(algebraMap R S) : (a : R) → S) tail)

Tactic:
exact ⟨reg.1.of_flat_of_isBaseChange hf, ih hg reg.2⟩
-- Module: Mathlib.RingTheory.Regular.Flat
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
inst_9 : Flat R S
f : M →ₗ[R] N
hf : IsBaseChange S f
rs : List R
reg : IsWeaklyRegular M rs
nil :
  ∀ {M : Type u_3} {N : Type u_4} [inst_10 : AddCommGroup M] [inst_11 : Module R M] [inst_12 : AddCommGroup N]
    [inst_13 : Module R N] [inst_14 : Module S N] [inst_15 : IsScalarTower R S N] {f : M →ₗ[R] N}
    (hf : IsBaseChange S f) (reg : IsWeaklyRegular.{u_1, u_3} (R := R) M []),
    IsWeaklyRegular.{u_2, u_4} (R := S) N (List.map.{u_1, u_2} (α := R) (⇑(algebraMap R S) : (a : R) → S) [])
cons :
  ∀ (x : R) (tail : List R)
    (ih :
      ∀ {M : Type u_3} {N : Type u_4} [inst_10 : AddCommGroup M] [inst_11 : Module R M] [inst_12 : AddCommGroup N]
        [inst_13 : Module R N] [inst_14 : Module S N] [inst_15 : IsScalarTower R S N] {f : M →ₗ[R] N}
        (hf : IsBaseChange S f) (reg : IsWeaklyRegular M tail),
        IsWeaklyRegular.{u_2, u_4} (R := S) N (List.map (⇑(algebraMap R S) : (a : R) → S) tail))
    {M : Type u_3} {N : Type u_4} [inst_10 : AddCommGroup M] [inst_11 : Module R M] [inst_12 : AddCommGroup N]
    [inst_13 : Module R N] [inst_14 : Module S N] [inst_15 : IsScalarTower R S N] {f : M →ₗ[R] N}
    (hf : IsBaseChange S f) (reg : IsWeaklyRegular M (x :: tail)),
    IsWeaklyRegular.{u_2, u_4} (R := S) N (List.map (⇑(algebraMap R S) : (a : R) → S) (x :: tail))
⊢ IsWeaklyRegular.{u_2, u_4} (R := S) N (List.map (⇑(algebraMap R S) : (a : R) → S) rs)

Tactic:
induction rs generalizing M N with
  | nil => simp
  | cons x _ ih =>
    simp only [List.map_cons, isWeaklyRegular_cons_iff] at reg ⊢
    have e := (QuotSMulTop.algebraMapTensorEquivTensorQuotSMulTop x M S).symm ≪≫ₗ
      QuotSMulTop.congr ((algebraMap R S) x) hf.equiv
    have hg : IsBaseChange S <|
        e.toLinearMap.restrictScalars R ∘ₗ TensorProduct.mk R S (QuotSMulTop x M) 1 :=
      IsBaseChange.of_equiv e (fun _ ↦ by simp)
    exact ⟨reg.1.of_flat_of_isBaseChange hf, ih hg reg.2⟩

Premises used: RingTheory.Sequence.isWeaklyRegular_cons_iff, List.map_cons, RingTheory.Sequence.IsWeaklyRegular.cons, RingTheory.Sequence.IsWeaklyRegular.nil
-- Module: Mathlib.RingTheory.Regular.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Flat R S
rs : List R
reg : IsWeaklyRegular R rs
⊢ IsWeaklyRegular (R := S) S (List.map (⇑(algebraMap R S) : (a : R) → S) rs)

Tactic:
reg.of_flat_of_isBaseChange (IsBaseChange.linearMap R S)

Premises used: RingTheory.Sequence.IsWeaklyRegular.of_flat_of_isBaseChange, IsBaseChange.linearMap
-- Module: Mathlib.RingTheory.Regular.Flat
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
T : Submonoid R
inst_9 : IsLocalization T S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule T f
rs : List R
reg : IsWeaklyRegular M rs
⊢ IsWeaklyRegular.{u_2, u_4} (R := S) N (List.map (⇑(algebraMap R S) : (a : R) → S) rs)

Tactic:
have : Flat R S := IsLocalization.flat S T
  reg.of_flat_of_isBaseChange (IsLocalizedModule.isBaseChange T S f)

Premises used: IsLocalizedModule.isBaseChange, RingTheory.Sequence.IsWeaklyRegular.of_flat_of_isBaseChange, IsLocalization.flat
-- Module: Mathlib.RingTheory.Regular.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Submonoid R
inst_3 : IsLocalization T S
rs : List R
reg : IsWeaklyRegular R rs
⊢ IsWeaklyRegular (R := S) S (List.map (⇑(algebraMap R S) : (a : R) → S) rs)

Tactic:
reg.of_isLocalizedModule S T (Algebra.linearMap R S)

Premises used: Algebra.linearMap, RingTheory.Sequence.IsWeaklyRegular.of_isLocalizedModule
-- Module: Mathlib.RingTheory.Regular.Flat
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Ideal R
inst_9 : p.IsPrime
inst_10 : IsLocalization.AtPrime S p
inst_11 : Nontrivial N
inst_12 : Module.Finite S N
f : M →ₗ[R] N
inst_13 : IsLocalizedModule.AtPrime p f
rs : List R
reg : IsWeaklyRegular M rs
mem : ∀ r ∈ rs, r ∈ p
⊢ IsLocalRing S

Tactic:
have : IsLocalRing S := IsLocalization.AtPrime.isLocalRing S p
-- Module: Mathlib.RingTheory.Regular.Flat
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Ideal R
inst_9 : p.IsPrime
inst_10 : IsLocalization.AtPrime S p
inst_11 : Nontrivial N
inst_12 : Module.Finite S N
f : M →ₗ[R] N
inst_13 : IsLocalizedModule.AtPrime p f
rs : List R
reg : IsWeaklyRegular M rs
mem : ∀ r ∈ rs, r ∈ p
this : IsLocalRing S
⊢ IsRegular.{u_2, u_4} (R := S) N (List.map (⇑(algebraMap R S) : (a : R) → S) rs)

Tactic:
(IsLocalRing.isRegular_iff_isWeaklyRegular_of_subset_maximalIdeal (fun _ hr ↦ ?_)).mpr <|
    reg.of_isLocalizedModule S p.primeCompl f

Premises used: Iff.mpr, IsLocalRing.isRegular_iff_isWeaklyRegular_of_subset_maximalIdeal, Ideal.primeCompl, RingTheory.Sequence.IsWeaklyRegular.of_isLocalizedModule
-- Module: Mathlib.RingTheory.Regular.Flat
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Ideal R
inst_9 : p.IsPrime
inst_10 : IsLocalization.AtPrime S p
inst_11 : Nontrivial N
inst_12 : Module.Finite S N
f : M →ₗ[R] N
inst_13 : IsLocalizedModule.AtPrime p f
rs : List R
reg : IsWeaklyRegular M rs
mem : ∀ r ∈ rs, r ∈ p
this : IsLocalRing S
refine :
  ∀ (x : S) (hr : Membership.mem (γ := List S) (List.map (⇑(algebraMap R S) : (a : R) → S) rs) x),
    Membership.mem (γ := Ideal S) (IsLocalRing.maximalIdeal S) x
⊢ IsRegular.{u_2, u_4} (R := S) N (List.map (⇑(algebraMap R S) : (a : R) → S) rs)

Tactic:
refine (IsLocalRing.isRegular_iff_isWeaklyRegular_of_subset_maximalIdeal (fun _ hr ↦ ?_)).mpr <|
    reg.of_isLocalizedModule S p.primeCompl f

Premises used: Iff.mpr, IsLocalRing.isRegular_iff_isWeaklyRegular_of_subset_maximalIdeal, Ideal.primeCompl, RingTheory.Sequence.IsWeaklyRegular.of_isLocalizedModule
-- Module: Mathlib.RingTheory.Regular.Flat
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Ideal R
inst_9 : p.IsPrime
inst_10 : IsLocalization.AtPrime S p
inst_11 : Nontrivial N
inst_12 : Module.Finite S N
f : M →ₗ[R] N
inst_13 : IsLocalizedModule.AtPrime p f
rs : List R
reg : IsWeaklyRegular M rs
mem : ∀ r ∈ rs, r ∈ p
this : IsLocalRing S
x : S
hr : Membership.mem (γ := List S) (List.map (⇑(algebraMap R S) : (a : R) → S) rs) x
rcases :
  ∀ (r : R) (hr : r ∈ rs) (eq : (algebraMap R S : (a : R) → S) r = x),
    Membership.mem (γ := Ideal S) (IsLocalRing.maximalIdeal S) x
⊢ Membership.mem (γ := Ideal S) (IsLocalRing.maximalIdeal S) x

Tactic:
rcases List.mem_map.mp hr with ⟨r, hr, eq⟩

Premises used: Iff.mp, List.mem_map
-- Module: Mathlib.RingTheory.Regular.Flat
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Ideal R
inst_9 : p.IsPrime
inst_10 : IsLocalization.AtPrime S p
inst_11 : Nontrivial N
inst_12 : Module.Finite S N
f : M →ₗ[R] N
inst_13 : IsLocalizedModule.AtPrime p f
rs : List R
reg : IsWeaklyRegular M rs
mem : ∀ r ∈ rs, r ∈ p
this : IsLocalRing S
x : S
hr_1 : Membership.mem (γ := List S) (List.map (⇑(algebraMap R S) : (a : R) → S) rs) x
r : R
hr : r ∈ rs
eq : (algebraMap R S : (a : R) → S) r = x
⊢ Membership.mem (γ := Ideal S) (IsLocalRing.maximalIdeal S) x

Tactic:
simpa only [← eq, IsLocalization.AtPrime.to_map_mem_maximal_iff S p] using mem r hr

Premises used: IsLocalization.AtPrime.to_map_mem_maximal_iff, IsLocalization.AtPrime.isLocalRing
-- Module: Mathlib.RingTheory.Regular.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
inst_4 : IsLocalization.AtPrime S p
rs : List R
reg : IsWeaklyRegular R rs
mem : ∀ r ∈ rs, r ∈ p
⊢ IsRegular (R := S) S (List.map (⇑(algebraMap R S) : (a : R) → S) rs)

Tactic:
have : Nontrivial S := IsLocalization.AtPrime.nontrivial S p
  reg.isRegular_of_isLocalizedModule_of_mem S p (Algebra.linearMap R S) mem

Premises used: Algebra.linearMap, IsLocalization.AtPrime.nontrivial, RingTheory.Sequence.IsWeaklyRegular.isRegular_of_isLocalizedModule_of_mem
-- Module: Mathlib.RingTheory.Regular.Flat
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
inst_9 : FaithfullyFlat R S
f : M →ₗ[R] N
hf : IsBaseChange S f
rs : List R
reg : IsRegular M rs
⊢ IsRegular.{u_2, u_4} (R := S) N (List.map (⇑(algebraMap R S) : (a : R) → S) rs)

Tactic:
⟨reg.1.of_flat_of_isBaseChange hf, ?_⟩

Premises used: RingTheory.Sequence.IsRegular.mk, RingTheory.Sequence.IsWeaklyRegular.of_flat_of_isBaseChange, RingTheory.Sequence.IsRegular.toIsWeaklyRegular
-- Module: Mathlib.RingTheory.Regular.Flat
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
inst_9 : FaithfullyFlat R S
f : M →ₗ[R] N
hf : IsBaseChange S f
rs : List R
reg : IsRegular M rs
refine :
  ⊤ ≠
    HSMul.hSMul.{u_2, u_4, u_4} (α := Ideal S) (β := Submodule S N)
      (Ideal.ofList (List.map (⇑(algebraMap R S) : (a : R) → S) rs)) ⊤
⊢ IsRegular.{u_2, u_4} (R := S) N (List.map (⇑(algebraMap R S) : (a : R) → S) rs)

Tactic:
refine ⟨reg.1.of_flat_of_isBaseChange hf, ?_⟩
-- Module: Mathlib.RingTheory.Regular.Flat
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
inst_9 : FaithfullyFlat R S
f : M →ₗ[R] N
hf : IsBaseChange S f
rs : List R
reg : IsRegular M rs
rw :
  ⊤ ≠
    HSMul.hSMul.{u_2, u_4, u_4} (α := Ideal S) (β := Submodule S N)
      (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.ofList rs)) ⊤
⊢ ⊤ ≠
    HSMul.hSMul.{u_2, u_4, u_4} (α := Ideal S) (β := Submodule S N)
      (Ideal.ofList (List.map (⇑(algebraMap R S) : (a : R) → S) rs)) ⊤

Tactic:
rw [← Ideal.map_ofList]

Premises used: Ideal.map_ofList