awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ ⊤ ≠
    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:
((hf.map_smul_top_ne_top_iff_of_faithfullyFlat R M _).mpr reg.2.symm).symm

Premises used: Iff.mpr, IsBaseChange.map_smul_top_ne_top_iff_of_faithfullyFlat, RingTheory.Sequence.IsRegular.top_ne_smul, Ne.symm
-- 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
⊢ ⊤ ≠
    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:
exact ((hf.map_smul_top_ne_top_iff_of_faithfullyFlat R M _).mpr reg.2.symm).symm

Premises used: Iff.mpr, IsBaseChange.map_smul_top_ne_top_iff_of_faithfullyFlat, RingTheory.Sequence.IsRegular.top_ne_smul, Ne.symm
-- 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 : FaithfullyFlat R S
rs : List R
reg : IsRegular R rs
⊢ IsRegular (R := S) S (List.map (⇑(algebraMap R S) : (a : R) → S) rs)

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

Premises used: RingTheory.Sequence.IsRegular.of_faithfullyFlat_of_isBaseChange, IsBaseChange.linearMap
-- Module: Mathlib.RingTheory.Regular.IsSMulRegular
Goal:
R : Type u_3
S : Type u_2
M : Type u_4
N : Type u_1
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
σ' : S →+* R
inst_2 : RingHomInvPair σ σ'
inst_3 : RingHomInvPair σ' σ
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid N
inst_7 : Module S N
e : M ≃ₛₗ[σ] N
r : R
⊢ IsSMulRegular M r ↔ IsSMulRegular.{u_2, u_1} (R := S) N ((σ : (a : R) → S) r : S)

Tactic:
e.toEquiv.isSMulRegular_congr (e.map_smul' r)

Premises used: Equiv.isSMulRegular_congr, LinearEquiv.toLinearMap, LinearMap.map_smul'
-- Module: Mathlib.RingTheory.Regular.IsSMulRegular
Goal:
R : Type u_2
M : Type u_3
N : Type u_1
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
e : M ≃ₗ[R] N
r : R
⊢ IsSMulRegular M r ↔ IsSMulRegular N r

Tactic:
e.isSMulRegular_congr' r

Premises used: LinearEquiv.isSMulRegular_congr'
-- Module: Mathlib.RingTheory.Regular.IsSMulRegular
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
r : R
h : IsSMulRegular M r
⊢ IsSMulRegular.{u_1, u_3} (↥N) r

Tactic:
h.of_injective N.subtype N.injective_subtype

Premises used: Submodule.injective_subtype, Submodule.subtype, IsSMulRegular.of_injective
-- Module: Mathlib.RingTheory.Regular.IsSMulRegular
Goal:
R : Type u_1
M : Type u_3
M' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
inst_5 : Module.Flat R M
r : R
h : IsSMulRegular M' r
⊢ IsSMulRegular (M ⊗[R] M') r

Tactic:
have h1 := congrArg DFunLike.coe (LinearMap.lTensor_smul_action M M' r)
  h1.subst (Module.Flat.lTensor_preserves_injective_linearMap _ h)

Premises used: Module.Flat.lTensor_preserves_injective_linearMap, DistribSMul.toLinearMap, Quotient.liftOn', congrArg, AddCon.liftOn, Eq.subst, LinearMap.lTensor_smul_action, IsSMulRegular, DFunLike.coe
-- Module: Mathlib.RingTheory.Regular.IsSMulRegular
Goal:
R : Type u_1
M : Type u_3
M' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
inst_5 : Module.Flat R M
r : R
h : IsSMulRegular M' r
⊢ IsSMulRegular (M' ⊗[R] M) r

Tactic:
have h1 := congrArg DFunLike.coe (LinearMap.rTensor_smul_action M M' r)
  h1.subst (Module.Flat.rTensor_preserves_injective_linearMap _ h)

Premises used: LinearMap.rTensor_smul_action, DistribSMul.toLinearMap, Quotient.liftOn', congrArg, AddCon.liftOn, Eq.subst, IsSMulRegular, DFunLike.coe, Module.Flat.rTensor_preserves_injective_linearMap
-- Module: Mathlib.RingTheory.Regular.IsSMulRegular
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
⊢ (∀ (a : M) (b : a ∈ N),
      r • Subtype.mk (p := fun (a : M) ↦ a ∈ N) a b = 0 → Subtype.mk (p := fun (a : M) ↦ a ∈ N) a b = 0) ↔
    ∀ x ∈ N, r • x = 0 → x = 0

Tactic:
simp only [SetLike.mk_smul_mk, Submodule.mk_eq_zero]

Premises used: Submodule.mk_eq_zero, SetLike.mk_smul_mk
-- Module: Mathlib.RingTheory.Regular.IsSMulRegular
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
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
⊢ (∀ (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

Tactic:
simp_rw [← map_smul, N.mkQ_apply, Submodule.Quotient.mk_eq_zero]

Premises used: Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero, map_smul
-- Module: Mathlib.RingTheory.Regular.IsSMulRegular
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
h1 : IsSMulRegular.{u_1, u_3} (M ⧸ N) r
x : M
h2 : r • x ∈ N
⊢ x ∈ N

Tactic:
(isSMulRegular_quotient_iff_mem_of_smul_mem N r).mp h1 x h2

Premises used: isSMulRegular_quotient_iff_mem_of_smul_mem, Iff.mp
-- Module: Mathlib.RingTheory.Regular.IsSMulRegular
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

Tactic:
IsSMulRegular.of_right_eq_zero_of_smul ?_

Premises used: IsSMulRegular.of_right_eq_zero_of_smul
-- Module: Mathlib.RingTheory.Regular.IsSMulRegular
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
refine : ∀ (m : M'), r • m = 0 → m = 0
⊢ IsSMulRegular M' r

Tactic:
refine IsSMulRegular.of_right_eq_zero_of_smul ?_

Premises used: IsSMulRegular.of_right_eq_zero_of_smul
-- Module: Mathlib.RingTheory.Regular.IsSMulRegular
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
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')
⊢ x = 0

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

Premises used: Eq.mpr, congrArg, Membership.mem, LinearMap.map_zero, LinearMap.map_smul, Eq.symm, IsSMulRegular.right_eq_zero_of_smul, Eq.trans
-- Module: Mathlib.RingTheory.Regular.IsSMulRegular
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')

Tactic:
(congrArg f (h1.right_eq_zero_of_smul ?_)).trans f.map_zero

Premises used: congrArg, LinearMap.map_zero, DFunLike.coe, IsSMulRegular.right_eq_zero_of_smul, Eq.trans
-- Module: Mathlib.RingTheory.Regular.IsSMulRegular
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
refine : r • y = 0
⊢ Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') y : M') (0 : M')

Tactic:
refine (congrArg f (h1.right_eq_zero_of_smul ?_)).trans f.map_zero

Premises used: congrArg, LinearMap.map_zero, DFunLike.coe, IsSMulRegular.right_eq_zero_of_smul, Eq.trans
-- Module: Mathlib.RingTheory.Regular.IsSMulRegular
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
⊢ r • y = 0

Tactic:
hf <| (f.map_smul r y).trans <| hx.trans f.map_zero.symm

Premises used: LinearMap.map_zero, LinearMap.map_smul, Eq.symm, Eq.trans
-- Module: Mathlib.RingTheory.Regular.IsSMulRegular
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
⊢ r • y = 0

Tactic:
exact hf <| (f.map_smul r y).trans <| hx.trans f.map_zero.symm

Premises used: LinearMap.map_zero, LinearMap.map_smul, Eq.symm, Eq.trans
-- Module: Mathlib.RingTheory.Regular.IsSMulRegular
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
h1 : IsSMulRegular.{u_1, u_3} (↥N) r
h2 : IsSMulRegular.{u_1, u_3} (M ⧸ N) r
⊢ IsSMulRegular M r

Tactic:
isSMulRegular_of_range_eq_ker N.injective_subtype
    (N.range_subtype.trans N.ker_mkQ.symm) h1 h2

Premises used: Submodule.injective_subtype, Submodule.ker_mkQ, Eq.symm, Submodule.range_subtype, isSMulRegular_of_range_eq_ker, Eq.trans
-- Module: Mathlib.RingTheory.Regular.IsSMulRegular
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}
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}ᶜ

Tactic:
simp_rw [Set.compl_setOf, isSMulRegular_iff_right_eq_zero_of_smul,
      not_forall, exists_prop, and_comm]

Premises used: and_comm, exists_prop, Classical.not_forall, isSMulRegular_iff_right_eq_zero_of_smul, Set.compl_setOf
-- Module: Mathlib.RingTheory.Regular.IsSMulRegular
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
⊢ IsSMulRegular M r ↔
    Eq.{u_3 + 1} (α := Submodule R M)
      (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r)) ⊥

Tactic:
isSMulRegular_iff_torsionBy_eq_bot M r

Premises used: DistribSMul.toLinearMap, Submodule.torsionBy, isSMulRegular_iff_torsionBy_eq_bot
-- Module: Mathlib.RingTheory.Regular.IsSMulRegular
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} (↥N) r ↔
    Disjoint (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r)) N

Tactic:
Iff.trans (isSMulRegular_submodule_iff_right_eq_zero_of_smul N r) <|
    Iff.symm <| Iff.trans disjoint_comm disjoint_def

Premises used: isSMulRegular_submodule_iff_right_eq_zero_of_smul, disjoint_comm, Iff.trans, Submodule.disjoint_def, Iff.symm
-- Module: Mathlib.RingTheory.Regular.IsSMulRegular
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 ↔ comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r) N ≤ N

Tactic:
isSMulRegular_quotient_iff_mem_of_smul_mem N r

Premises used: Set.Mem, setOf, isSMulRegular_quotient_iff_mem_of_smul_mem, Set.preimage
-- Module: Mathlib.RingTheory.Regular.IsSMulRegular
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 ↔ comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r) N = N

Tactic:
Iff.trans (isSMulRegular_on_quot_iff_lsmul_comap_le N r) <|
    LE.le.ge_iff_eq' (fun _ => N.smul_mem r)

Premises used: LE.le.ge_iff_eq', Iff.trans, isSMulRegular_on_quot_iff_lsmul_comap_le, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Regular.IsSMulRegular
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)
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
⊢ IsSMulRegular.{u_1, u_3} (M ⧸ N) r ↔ 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]

Premises used: Submodule.map_comap_eq, Submodule.map_le_map_iff_of_injective, LinearMap.range_eq_map, isSMulRegular_on_quot_iff_lsmul_comap_le, LinearMap.lsmul_eq_distribSMultoLinearMap
-- Module: Mathlib.RingTheory.Regular.IsSMulRegular
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)
⊢ 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:
rfl
-- Module: Mathlib.RingTheory.Regular.IsSMulRegular
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
h :
  Eq.{u_3 + 1} (α := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r)) ⊥
⊢ IsSMulRegular M r

Tactic:
(isSMulRegular_iff_ker_lsmul_eq_bot M r).mpr h

Premises used: Iff.mpr, isSMulRegular_iff_ker_lsmul_eq_bot
-- Module: Mathlib.RingTheory.Regular.IsSMulRegular
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 →
    map (DistribSMul.toLinearMap R M r)
        (comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r) N) ≤
      map (DistribSMul.toLinearMap R M r) N

Tactic:
map_mono ∘ (isSMulRegular_on_quot_iff_lsmul_comap_le N r).mp

Premises used: Function.comp, Submodule.map_mono, Iff.mp, isSMulRegular_on_quot_iff_lsmul_comap_le
-- Module: Mathlib.RingTheory.Regular.IsSMulRegular
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 :
  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)
⊢ IsSMulRegular.{u_1, u_3} (M ⧸ N) r → HSMul.hSMul (β := Submodule R M) r ⊤ ⊓ N ≤ r • N

Tactic:
convert! map_mono ∘ (isSMulRegular_on_quot_iff_lsmul_comap_le N r).mp using 2

Premises used: Submodule.map_mono, Iff.mp, isSMulRegular_on_quot_iff_lsmul_comap_le
-- Module: Mathlib.RingTheory.Regular.IsSMulRegular
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 : 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:
Eq.trans (congrArg (· ⊓ N) (map_top _)) (map_comap_eq _ _).symm

Premises used: congrArg, Submodule.map_comap_eq, Submodule.map_top, Eq.symm, Min.min, Eq.trans
-- Module: Mathlib.RingTheory.Regular.IsSMulRegular
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 : 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:
exact Eq.trans (congrArg (· ⊓ N) (map_top _)) (map_comap_eq _ _).symm
-- Module: Mathlib.RingTheory.Regular.IsSMulRegular
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
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₁ ⋯) :
      (a : QuotSMulTop r M) → QuotSMulTop r M')
    (⇑((HSMul.hSMul (β := Submodule R M') r ⊤).mapQ (HSMul.hSMul (β := Submodule R M'') r ⊤) f₂ ⋯) :
      (a : QuotSMulTop r M') → QuotSMulTop r M'')
⊢ 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'')

Tactic:
dsimp [map, mapQLinear]

Premises used: Submodule.mapQLinear, QuotSMulTop.map
-- Module: Mathlib.RingTheory.Regular.IsSMulRegular
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
rw : HSMul.hSMul (β := Submodule R M'') r ⊤ ⊓ f₂.range ≤ r • f₂.range
⊢ 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₁ ⋯) :
      (a : QuotSMulTop r M) → QuotSMulTop r M')
    (⇑((HSMul.hSMul (β := Submodule R M') r ⊤).mapQ (HSMul.hSMul (β := Submodule R M'') r ⊤) f₂ ⋯) :
      (a : QuotSMulTop r M') → QuotSMulTop r M'')

Tactic:
rw [Exact.exact_mapQ_iff h₁₂, map_pointwise_smul, Submodule.map_top, inf_comm]

Premises used: Submodule.map_top, Function.Exact.exact_mapQ_iff, inf_comm, Submodule.map_pointwise_smul
-- Module: Mathlib.RingTheory.Regular.IsSMulRegular
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
⊢ HSMul.hSMul (β := Submodule R M'') r ⊤ ⊓ f₂.range ≤ r • f₂.range

Tactic:
smul_top_inf_eq_smul_of_isSMulRegular_on_quot this

Premises used: Set.Mem, smul_top_inf_eq_smul_of_isSMulRegular_on_quot
-- Module: Mathlib.RingTheory.Regular.IsSMulRegular
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
⊢ HSMul.hSMul (β := Submodule R M'') r ⊤ ⊓ f₂.range ≤ r • f₂.range

Tactic:
exact smul_top_inf_eq_smul_of_isSMulRegular_on_quot this

Premises used: smul_top_inf_eq_smul_of_isSMulRegular_on_quot
-- Module: Mathlib.RingTheory.Regular.LinearMap
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
r : R
reg : IsSMulRegular M r
mem_ann : Membership.mem (γ := Ideal R) (annihilator R N) r
apply : ∀ (f : N →ₗ[R] M) (x : N), Eq.{u_2 + 1} (α := M) ((f : (a : N) → M) x : M) ((0 : (a : N) → M) x : M)
⊢ Subsingleton (N →ₗ[R] M)

Tactic:
apply subsingleton_of_forall_eq 0 (fun f ↦ ext fun x ↦ ?_)

Premises used: subsingleton_of_forall_eq, LinearMap.ext, OfNat.ofNat