case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ ↑toSubmodule S * ↑toSubmodule S ≤ ↑toSubmodule S

case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ ↑toSubmodule S ≤ ↑toSubmodule S * ↑toSubmodule S
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ ↑toSubmodule S * ↑toSubmodule S = ↑toSubmodule S
apply le_antisymm
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ ↑toSubmodule (S ⊔ S) = ↑toSubmodule S
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ ↑toSubmodule S * ↑toSubmodule S ≤ ↑toSubmodule S
refine' (mul_toSubmodule_le _ _).trans_eq _
no goals
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ ↑toSubmodule (S ⊔ S) = ↑toSubmodule S
rw [sup_idem]
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
x : A
hx1 : x ∈ ↑toSubmodule S
⊢ x ∈ ↑toSubmodule S * ↑toSubmodule S
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ ↑toSubmodule S ≤ ↑toSubmodule S * ↑toSubmodule S
intro x hx1
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
x : A
hx1 : x ∈ ↑toSubmodule S
⊢ x * 1 ∈ ↑toSubmodule S * ↑toSubmodule S
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
x : A
hx1 : x ∈ ↑toSubmodule S
⊢ x ∈ ↑toSubmodule S * ↑toSubmodule S
rw [← mul_one x]
no goals
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
x : A
hx1 : x ∈ ↑toSubmodule S
⊢ x * 1 ∈ ↑toSubmodule S * ↑toSubmodule S
exact Submodule.mul_mem_mul hx1 (show (1 : A) ∈ S from one_mem S)