case h
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
⊢ ∀ (x : A), x ∈ 1 ↔ x ∈ span R {1}
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
⊢ 1 = span R {1}
apply Submodule.ext
case h
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n a : A
⊢ a ∈ 1 ↔ a ∈ span R {1}
case h
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
⊢ ∀ (x : A), x ∈ 1 ↔ x ∈ span R {1}
intro a
no goals
case h
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n a : A
⊢ a ∈ 1 ↔ a ∈ span R {1}
simp only [mem_one, mem_span_singleton, Algebra.smul_def, mul_one]