R : Type u_2
inst✝⁶ : Ring R
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.87505
inst✝¹ : AddCommGroup G
inst✝ : Module R G
x : E
y : F
H : ∀ (c : R), c • x = 0 → c • y = 0
h : x ∈ (mkSpanSingleton' x y H).domain
this : ↑(mkSpanSingleton' x y H) { val := 1 • x, property := (_ : 1 • x ∈ (mkSpanSingleton' x y H).domain) } = 1 • y
⊢ ↑(mkSpanSingleton' x y H) { val := x, property := h } = y
R : Type u_2
inst✝⁶ : Ring R
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.87505
inst✝¹ : AddCommGroup G
inst✝ : Module R G
x : E
y : F
H : ∀ (c : R), c • x = 0 → c • y = 0
h : x ∈ (mkSpanSingleton' x y H).domain
⊢ ↑(mkSpanSingleton' x y H) { val := x, property := h } = y
have := by refine mkSpanSingleton'_apply x y H 1 ?_; rwa [one_smul]
no goals
R : Type u_2
inst✝⁶ : Ring R
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.87505
inst✝¹ : AddCommGroup G
inst✝ : Module R G
x : E
y : F
H : ∀ (c : R), c • x = 0 → c • y = 0
h : x ∈ (mkSpanSingleton' x y H).domain
this : ↑(mkSpanSingleton' x y H) { val := 1 • x, property := (_ : 1 • x ∈ (mkSpanSingleton' x y H).domain) } = 1 • y
⊢ ↑(mkSpanSingleton' x y H) { val := x, property := h } = y
convert this <;> rw [one_smul]
R : Type u_2
inst✝⁶ : Ring R
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.87505
inst✝¹ : AddCommGroup G
inst✝ : Module R G
x : E
y : F
H : ∀ (c : R), c • x = 0 → c • y = 0
h : x ∈ (mkSpanSingleton' x y H).domain
⊢ 1 • x ∈ (mkSpanSingleton' x y H).domain
R : Type u_2
inst✝⁶ : Ring R
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.87505
inst✝¹ : AddCommGroup G
inst✝ : Module R G
x : E
y : F
H : ∀ (c : R), c • x = 0 → c • y = 0
h : x ∈ (mkSpanSingleton' x y H).domain
⊢ ?m.91161
refine mkSpanSingleton'_apply x y H 1 ?_
no goals
R : Type u_2
inst✝⁶ : Ring R
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.87505
inst✝¹ : AddCommGroup G
inst✝ : Module R G
x : E
y : F
H : ∀ (c : R), c • x = 0 → c • y = 0
h : x ∈ (mkSpanSingleton' x y H).domain
⊢ 1 • x ∈ (mkSpanSingleton' x y H).domain
rwa [one_smul]