awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hI : I.FG
obtain : ∀ (s : Finset R) (hs : Ideal.span (↑s : Set R) = I), (reesAlgebra I).FG
obtain₁ :
  ∀ (s : Finset R) (hs : Ideal.span (↑s : Set R) = I),
    Subalgebra.FG (Algebra.adjoin R (↑(Submodule.map (monomial 1) (Ideal.span (↑s : Set R))) : Set R[X]))
h :
  ∀ (s : Finset R) (hs : Ideal.span (↑s : Set R) = I),
    Eq (α := Subalgebra R R[X]) (Algebra.adjoin R (↑(Finset.image (⇑(monomial 1) : (a : R) → R[X]) s) : Set R[X]))
      (Algebra.adjoin R (↑(Submodule.map (monomial 1) (Ideal.span (↑s : Set R))) : Set R[X]))
h₁ :
  ∀ (s : Finset R) (hs : Ideal.span (↑s : Set R) = I),
    Eq (α := Subalgebra R R[X]) (Algebra.adjoin R ((⇑(monomial 1) : (a : R) → R[X]) '' (↑s : Set R)))
      (Algebra.adjoin R (↑(Submodule.map (monomial 1) (Ideal.span (↑s : Set R))) : Set R[X]))
⊢ (reesAlgebra I).FG
have h₂ : ∀ (s : Finset R) (hs : Ideal.span (↑s : Set R) = I),
  Eq (α := Subalgebra R R[X]) (Algebra.adjoin R ((⇑(monomial 1) : (a : R) → R[X]) '' (↑s : Set R)))
    (Algebra.adjoin R (↑(Submodule.map (monomial 1) (Submodule.span R (↑s : Set R))) : Set R[X]))
Tactic: classical
    obtain ⟨s, hs⟩ := hI
    rw [← adjoin_monomial_eq_reesAlgebra, ← hs]
    use s.image (monomial 1)
    rw [Finset.coe_image]
    change
      _ =
        Algebra.adjoin R
          (Submodule.map (monomial 1 : R →ₗ[R] R[X]) (Submodule.span R ↑s) : Set R[X])
    rw [Submodule.map_span, Algebra.adjoin_span]
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.RingTheory.Regular.Flat (goal)
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)
⊢ IsWeaklyRegular.{u_2, u_4} (R := S) N (List.map (⇑(algebraMap R S) : (a : R) → S) (x :: tail))
have 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)
Tactic: simp only [List.map_cons, isWeaklyRegular_cons_iff] at reg ⊢
Cleared hypotheses: reg
-- Lean 4 proof step from Mathlib.RingTheory.Regular.Flat (goal)
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
⊢ 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)
have 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)
Tactic: have e := (QuotSMulTop.algebraMapTensorEquivTensorQuotSMulTop x M S).symm ≪≫ₗ
      QuotSMulTop.congr ((algebraMap R S) x) hf.equiv
-- Lean 4 proof step from Mathlib.RingTheory.Regular.Flat (hypothesis)
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
⊢ 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)
have 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)
Tactic: have hg : IsBaseChange S <|
        e.toLinearMap.restrictScalars R ∘ₗ TensorProduct.mk R S (QuotSMulTop x M) 1 :=
      IsBaseChange.of_equiv e (fun _ ↦ by simp)
-- Lean 4 proof step from Mathlib.RingTheory.Regular.Flat (goal)
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
⊢ IsWeaklyRegular.{u_2, u_4} (R := S) N (List.map (⇑(algebraMap R S) : (a : R) → S) rs)
have 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) [])
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⟩
Cleared hypotheses: M, N, inst_3, inst_4, inst_5, inst_6, inst_7, inst_8, f, hf, rs, reg
-- Lean 4 proof step from Mathlib.RingTheory.Regular.Flat (goal)
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) [])
⊢ IsWeaklyRegular.{u_2, u_4} (R := S) N (List.map (⇑(algebraMap R S) : (a : R) → S) rs)
have 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))
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⟩
Cleared hypotheses: M, N, inst_3, inst_4, inst_5, inst_6, inst_7, inst_8, f, hf, rs, reg
-- Lean 4 proof step from Mathlib.RingTheory.Regular.Flat (hypothesis)
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
⊢ IsRegular.{u_2, u_4} (R := S) N (List.map (⇑(algebraMap R S) : (a : R) → S) rs)
have this : IsLocalRing S
Tactic: have : IsLocalRing S := IsLocalization.AtPrime.isLocalRing S p
-- Lean 4 proof step from Mathlib.RingTheory.Regular.Flat (goal)
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)
have 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
Tactic: refine (IsLocalRing.isRegular_iff_isWeaklyRegular_of_subset_maximalIdeal (fun _ hr ↦ ?_)).mpr <|
    reg.of_isLocalizedModule S p.primeCompl f
-- Lean 4 proof step from Mathlib.RingTheory.Regular.Flat (goal)
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
⊢ Membership.mem (γ := Ideal S) (IsLocalRing.maximalIdeal S) x
have rcases : ∀ (r : R) (hr : r ∈ rs) (eq : (algebraMap R S : (a : R) → S) r = x),
  Membership.mem (γ := Ideal S) (IsLocalRing.maximalIdeal S) x
Tactic: rcases List.mem_map.mp hr with ⟨r, hr, eq⟩
-- Lean 4 proof step from Mathlib.RingTheory.Regular.Flat (goal)
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)
have 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)) ⊤
Tactic: refine ⟨reg.1.of_flat_of_isBaseChange hf, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Regular.Flat (goal)
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
⊢ ⊤ ≠
    HSMul.hSMul.{u_2, u_4, u_4} (α := Ideal S) (β := Submodule S N)
      (Ideal.ofList (List.map (⇑(algebraMap R S) : (a : R) → S) rs)) ⊤
have 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)) ⊤
Tactic: rw [← Ideal.map_ofList]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.IsSMulRegular (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
r : R
⊢ (∀ (x : M),
      HSMul.hSMul (β := M ⧸ N) r ((N.mkQ : (a : M) → M ⧸ N) x : M ⧸ N) = 0 →
        Eq (α := M ⧸ N) ((N.mkQ : (a : M) → M ⧸ N) x : M ⧸ N) (0 : M ⧸ N)) ↔
    ∀ (x : M), r • x ∈ N → x ∈ N
have simp_rw : (∀ (x : M),
    Eq (α := M ⧸ N) ((N.mkQ : (a : M) → M ⧸ N) (r • x) : M ⧸ N) (0 : M ⧸ N) →
      Eq (α := M ⧸ N) ((N.mkQ : (a : M) → M ⧸ N) x : M ⧸ N) (0 : M ⧸ N)) ↔
  ∀ (x : M), r • x ∈ N → x ∈ N
Tactic: simp_rw [← map_smul, N.mkQ_apply, Submodule.Quotient.mk_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.IsSMulRegular (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
r : R
simp_rw :
  (∀ (x : M),
      Eq (α := M ⧸ N) ((N.mkQ : (a : M) → M ⧸ N) (r • x) : M ⧸ N) (0 : M ⧸ N) →
        Eq (α := M ⧸ N) ((N.mkQ : (a : M) → M ⧸ N) x : M ⧸ N) (0 : M ⧸ N)) ↔
    ∀ (x : M), r • x ∈ N → x ∈ N
⊢ (∀ (x : M),
      HSMul.hSMul (β := M ⧸ N) r ((N.mkQ : (a : M) → M ⧸ N) x : M ⧸ N) = 0 →
        Eq (α := M ⧸ N) ((N.mkQ : (a : M) → M ⧸ N) x : M ⧸ N) (0 : M ⧸ N)) ↔
    ∀ (x : M), r • x ∈ N → x ∈ N
have simp_rw₁ : (∀ (x : M), Eq (α := M ⧸ N) (Submodule.Quotient.mk (r • x)) 0 → Eq (α := M ⧸ N) (Submodule.Quotient.mk x) 0) ↔
  ∀ (x : M), r • x ∈ N → x ∈ N
Tactic: simp_rw [← map_smul, N.mkQ_apply, Submodule.Quotient.mk_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.IsSMulRegular (goal)
Goal:
R : Type u_1
M : Type u_3
M' : Type u_4
M'' : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
inst_5 : AddCommGroup M''
inst_6 : Module R M''
r : R
f : M →ₗ[R] M'
g : M' →ₗ[R] M''
hf : Function.Injective.{u_3 + 1, u_4 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : f.range = g.ker
h1 : IsSMulRegular M r
h2 : IsSMulRegular M'' r
⊢ IsSMulRegular M' r
have refine : ∀ (m : M'), r • m = 0 → m = 0
Tactic: refine IsSMulRegular.of_right_eq_zero_of_smul ?_
-- Lean 4 proof step from Mathlib.RingTheory.Regular.IsSMulRegular (goal)
Goal:
R : Type u_1
M : Type u_3
M' : Type u_4
M'' : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
inst_5 : AddCommGroup M''
inst_6 : Module R M''
r : R
f : M →ₗ[R] M'
g : M' →ₗ[R] M''
hf : Function.Injective.{u_3 + 1, u_4 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : f.range = g.ker
h1 : IsSMulRegular M r
h2 : IsSMulRegular M'' r
x : M'
hx : r • x = 0
⊢ x = 0
have obtain : ∀ (y : M) (hx : HSMul.hSMul (β := M') r ((f : (a : M) → M') y : M') = 0),
  Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') y : M') (0 : M')
Tactic: obtain ⟨y, ⟨⟩⟩ := (congrArg (x ∈ ·) hfg).mpr <| h2.right_eq_zero_of_smul <|
    (g.map_smul r x).symm.trans <| (congrArg _ hx).trans g.map_zero
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Regular.IsSMulRegular (goal)
Goal:
R : Type u_1
M : Type u_3
M' : Type u_4
M'' : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
inst_5 : AddCommGroup M''
inst_6 : Module R M''
r : R
f : M →ₗ[R] M'
g : M' →ₗ[R] M''
hf : Function.Injective.{u_3 + 1, u_4 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
hfg : f.range = g.ker
h1 : IsSMulRegular M r
h2 : IsSMulRegular M'' r
y : M
hx : HSMul.hSMul (β := M') r ((f : (a : M) → M') y : M') = 0
⊢ Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') y : M') (0 : M')
have refine : r • y = 0
Tactic: refine (congrArg f (h1.right_eq_zero_of_smul ?_)).trans f.map_zero
-- Lean 4 proof step from Mathlib.RingTheory.Regular.IsSMulRegular (goal)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
⊢ Eq.{u_1 + 1} (α := Set R) {r : R | ∃ (x : M), x ≠ 0 ∧ r • x = 0} {r : R | IsSMulRegular M r}ᶜ
have simp_rw : Eq.{u_1 + 1} (α := Set R) {r : R | ∃ (x : M), x ≠ 0 ∧ r • x = 0} {a : R | ¬IsSMulRegular M a}
Tactic: simp_rw [Set.compl_setOf, isSMulRegular_iff_right_eq_zero_of_smul,
      not_forall, exists_prop, and_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.IsSMulRegular (goal)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
simp_rw : Eq.{u_1 + 1} (α := Set R) {r : R | ∃ (x : M), x ≠ 0 ∧ r • x = 0} {a : R | ¬IsSMulRegular M a}
⊢ Eq.{u_1 + 1} (α := Set R) {r : R | ∃ (x : M), x ≠ 0 ∧ r • x = 0} {r : R | IsSMulRegular M r}ᶜ
have simp_rw₁ : Eq.{u_1 + 1} (α := Set R) {r : R | ∃ (x : M), x ≠ 0 ∧ r • x = 0} {a : R | ¬∀ (m : M), a • m = 0 → m = 0}
Tactic: simp_rw [Set.compl_setOf, isSMulRegular_iff_right_eq_zero_of_smul,
      not_forall, exists_prop, and_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.IsSMulRegular (goal)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
simp_rw : Eq.{u_1 + 1} (α := Set R) {r : R | ∃ (x : M), x ≠ 0 ∧ r • x = 0} {a : R | ¬IsSMulRegular M a}
simp_rw₁ : Eq.{u_1 + 1} (α := Set R) {r : R | ∃ (x : M), x ≠ 0 ∧ r • x = 0} {a : R | ¬∀ (m : M), a • m = 0 → m = 0}
⊢ Eq.{u_1 + 1} (α := Set R) {r : R | ∃ (x : M), x ≠ 0 ∧ r • x = 0} {r : R | IsSMulRegular M r}ᶜ
have simp_rw₂ : Eq.{u_1 + 1} (α := Set R) {r : R | ∃ (x : M), x ≠ 0 ∧ r • x = 0} {a : R | ∃ (x : M) (_ : a • x = 0), ¬x = 0}
Tactic: simp_rw [Set.compl_setOf, isSMulRegular_iff_right_eq_zero_of_smul,
      not_forall, exists_prop, and_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.IsSMulRegular (goal)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
simp_rw : Eq.{u_1 + 1} (α := Set R) {r : R | ∃ (x : M), x ≠ 0 ∧ r • x = 0} {a : R | ¬IsSMulRegular M a}
simp_rw₁ : Eq.{u_1 + 1} (α := Set R) {r : R | ∃ (x : M), x ≠ 0 ∧ r • x = 0} {a : R | ¬∀ (m : M), a • m = 0 → m = 0}
simp_rw₂ : Eq.{u_1 + 1} (α := Set R) {r : R | ∃ (x : M), x ≠ 0 ∧ r • x = 0} {a : R | ∃ (x : M) (_ : a • x = 0), ¬x = 0}
⊢ Eq.{u_1 + 1} (α := Set R) {r : R | ∃ (x : M), x ≠ 0 ∧ r • x = 0} {r : R | IsSMulRegular M r}ᶜ
have simp_rw₃ : Eq.{u_1 + 1} (α := Set R) {r : R | ∃ (x : M), x ≠ 0 ∧ r • x = 0} {a : R | ∃ (x : M), a • x = 0 ∧ ¬x = 0}
Tactic: simp_rw [Set.compl_setOf, isSMulRegular_iff_right_eq_zero_of_smul,
      not_forall, exists_prop, and_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.IsSMulRegular (goal)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
r : R
h : Function.Injective (α := M) (β := M) (⇑(DistribSMul.toLinearMap R M r) : (a : M) → M)
⊢ IsSMulRegular.{u_1, u_3} (M ⧸ N) r ↔ HSMul.hSMul (β := Submodule R M) r ⊤ ⊓ N ≤ r • N
have rw : map (R := R) (M := M) (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r) ⊤ ⊓ N ≤
    map (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r) N ↔
  HSMul.hSMul (β := Submodule R M) r ⊤ ⊓ N ≤ r • N
Tactic: rw [isSMulRegular_on_quot_iff_lsmul_comap_le, ← map_le_map_iff_of_injective h,
    ← LinearMap.lsmul_eq_distribSMultoLinearMap,
    map_comap_eq, LinearMap.range_eq_map]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.IsSMulRegular (goal)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
r : R
⊢ IsSMulRegular.{u_1, u_3} (M ⧸ N) r → HSMul.hSMul (β := Submodule R M) r ⊤ ⊓ N ≤ r • N
have h : IsSMulRegular.{u_1, u_3} (M ⧸ N) r →
  HSMul.hSMul (β := Submodule R M) r ⊤ ⊓ N =
    map (DistribSMul.toLinearMap R M r) (comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r) N)
Tactic: convert! map_mono ∘ (isSMulRegular_on_quot_iff_lsmul_comap_le N r).mp using 2
-- Lean 4 proof step from Mathlib.RingTheory.Regular.IsSMulRegular (goal)
Goal:
R : Type u_1
M : Type u_3
M' : Type u_4
M'' : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
inst_5 : AddCommGroup M''
inst_6 : Module R M''
M''' : Type u_6
inst_7 : AddCommGroup M'''
inst_8 : Module R M'''
r : R
f₁ : M →ₗ[R] M'
f₂ : M' →ₗ[R] M''
f₃ : M'' →ₗ[R] M'''
h₁₂ : Exact.{u_3, u_4, u_5} (M := M) (N := M') (P := M'') (⇑f₁ : (a : M) → M') (⇑f₂ : (a : M') → M'')
h₂₃ : Exact.{u_4, u_5, u_6} (M := M') (N := M'') (P := M''') (⇑f₂ : (a : M') → M'') (⇑f₃ : (a : M'') → M''')
h : IsSMulRegular M''' r
this : IsSMulRegular.{u_1, u_5} (M'' ⧸ f₂.range) r
⊢ Exact.{u_3, u_4, u_5} (M := QuotSMulTop r M) (N := QuotSMulTop r M') (P := QuotSMulTop r M'')
    (⇑((map r : (a : M →ₗ[R] M') → QuotSMulTop r M →ₗ[R] QuotSMulTop r M') f₁ :
          LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) (QuotSMulTop r M) (QuotSMulTop r M')) :
      (a : QuotSMulTop r M) → QuotSMulTop r M')
    (⇑((map r : (a : M' →ₗ[R] M'') → QuotSMulTop r M' →ₗ[R] QuotSMulTop r M'') f₂ :
          LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) (QuotSMulTop r M') (QuotSMulTop r M'')) :
      (a : QuotSMulTop r M') → QuotSMulTop r M'')
have dsimp : Exact.{u_3, u_4, u_5} (M := QuotSMulTop r M) (N := QuotSMulTop r M') (P := QuotSMulTop r M'')
  (⇑((HSMul.hSMul (β := Submodule R M) r ⊤).mapQ (HSMul.hSMul (β := Submodule R M') r ⊤) f₁ sorry) :
    (a : QuotSMulTop r M) → QuotSMulTop r M')
  (⇑((HSMul.hSMul (β := Submodule R M') r ⊤).mapQ (HSMul.hSMul (β := Submodule R M'') r ⊤) f₂ sorry) :
    (a : QuotSMulTop r M') → QuotSMulTop r M'')
Tactic: dsimp [map, mapQLinear]