R : Type u_2
R₂ : Type ?u.381021
K : Type ?u.381024
M : Type u_1
M₂ : Type ?u.381030
V : Type ?u.381033
S : Type ?u.381036
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x : M
h : x ≠ 0
⊢ ↑(↑(toSpanNonzeroSingleton R M x h) 1) = ↑{ val := x, property := (_ : x ∈ Submodule.span R {x}) }
R : Type u_2
R₂ : Type ?u.381021
K : Type ?u.381024
M : Type u_1
M₂ : Type ?u.381030
V : Type ?u.381033
S : Type ?u.381036
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x : M
h : x ≠ 0
⊢ ↑(toSpanNonzeroSingleton R M x h) 1 = { val := x, property := (_ : x ∈ Submodule.span R {x}) }
apply SetLike.coe_eq_coe.mp
R : Type u_2
R₂ : Type ?u.381021
K : Type ?u.381024
M : Type u_1
M₂ : Type ?u.381030
V : Type ?u.381033
S : Type ?u.381036
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x : M
h : x ≠ 0
this : ↑(↑(toSpanNonzeroSingleton R M x h) 1) = ↑(toSpanSingleton R M x) 1
⊢ ↑(↑(toSpanNonzeroSingleton R M x h) 1) = ↑{ val := x, property := (_ : x ∈ Submodule.span R {x}) }
R : Type u_2
R₂ : Type ?u.381021
K : Type ?u.381024
M : Type u_1
M₂ : Type ?u.381030
V : Type ?u.381033
S : Type ?u.381036
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x : M
h : x ≠ 0
⊢ ↑(↑(toSpanNonzeroSingleton R M x h) 1) = ↑{ val := x, property := (_ : x ∈ Submodule.span R {x}) }
have : ↑(toSpanNonzeroSingleton R M x h 1) = toSpanSingleton R M x 1 := rfl
no goals
R : Type u_2
R₂ : Type ?u.381021
K : Type ?u.381024
M : Type u_1
M₂ : Type ?u.381030
V : Type ?u.381033
S : Type ?u.381036
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x : M
h : x ≠ 0
this : ↑(↑(toSpanNonzeroSingleton R M x h) 1) = ↑(toSpanSingleton R M x) 1
⊢ ↑(↑(toSpanNonzeroSingleton R M x h) 1) = ↑{ val := x, property := (_ : x ∈ Submodule.span R {x}) }
rw [this, toSpanSingleton_one, Submodule.coe_mk]