-- Mathlib/Algebra/Algebra/Operations.lean
theorem one_smul : (1 : Submodule R A) • N = N

Proof state:
case refine_2
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
N : Submodule R M
m : M
hm : m ∈ N
⊢ m ∈ 1 • N

Tactic:
rw [← one_smul A m]

Result:
case refine_2
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
N : Submodule R M
m : M
hm : m ∈ N
⊢ 1 • m ∈ 1 • N

Proof state:
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
N : Submodule R M
⊢ 1 • N = N

Tactic:
refine le_antisymm (smul_le.mpr fun r hr m hm ↦ ?_) fun m hm ↦ ?_

Result:
case refine_1
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
N : Submodule R M
r : A
hr : r ∈ 1
m : M
hm : m ∈ N
⊢ r • m ∈ N

case refine_2
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
N : Submodule R M
m : M
hm : m ∈ N
⊢ m ∈ 1 • N

Proof state:
case refine_1.intro
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
N : Submodule R M
m : M
hm : m ∈ N
r : R
⊢ (LinearMap.toSpanSingleton R A 1) r • m ∈ N

Tactic:
rw [LinearMap.toSpanSingleton_apply, smul_one_smul]

Result:
case refine_1.intro
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
N : Submodule R M
m : M
hm : m ∈ N
r : R
⊢ r • m ∈ N

Proof state:
case refine_2
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
N : Submodule R M
m : M
hm : m ∈ N
⊢ 1 • m ∈ 1 • N

Tactic:
exact smul_mem_smul (one_le.mp le_rfl) hm

Result:
no goals

Proof state:
case refine_1
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
N : Submodule R M
r : A
hr : r ∈ 1
m : M
hm : m ∈ N
⊢ r • m ∈ N

Tactic:
obtain ⟨r, rfl⟩ := hr

Result:
case refine_1.intro
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
N : Submodule R M
m : M
hm : m ∈ N
r : R
⊢ (LinearMap.toSpanSingleton R A 1) r • m ∈ N

Proof state:
case refine_1.intro
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
N : Submodule R M
m : M
hm : m ∈ N
r : R
⊢ r • m ∈ N

Tactic:
exact N.smul_mem r hm

Result:
no goals