case h
R : Type ?u.359475
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.360556
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : Module K E
inst✝ : Module K F
f : E →ₗ.[K] F
x : E
y : F
hx : ¬x ∈ f.domain
x' : E
hx' : x' ∈ f.domain
c : K
⊢ c • x ∈ (mkSpanSingleton' x y (_ : ∀ (c : K), c • x = 0 → c • y = 0)).domain

case hz
R : Type ?u.359475
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.360556
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : Module K E
inst✝ : Module K F
f : E →ₗ.[K] F
x : E
y : F
hx : ¬x ∈ f.domain
x' : E
hx' : x' ∈ f.domain
c : K
⊢ ↑{ val := x', property := hx' } + ↑{ val := c • x, property := ?h } =
    ↑{ val := x' + c • x, property := (_ : x' + c • x ∈ f.domain ⊔ (mkSpanSingleton x y (_ : x = 0 → False)).domain) }
R : Type ?u.359475
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.360556
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : Module K E
inst✝ : Module K F
f : E →ₗ.[K] F
x : E
y : F
hx : ¬x ∈ f.domain
x' : E
hx' : x' ∈ f.domain
c : K
⊢ ↑(supSpanSingleton f x y hx)
      { val := x' + c • x,
        property := (_ : x' + c • x ∈ f.domain ⊔ (mkSpanSingleton x y (_ : x = 0 → False)).domain) } =
    ↑f { val := x', property := hx' } + c • y
erw [sup_apply _ ⟨x', hx'⟩ ⟨c • x, _⟩, mkSpanSingleton'_apply]
case hz
R : Type ?u.359475
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.360556
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : Module K E
inst✝ : Module K F
f : E →ₗ.[K] F
x : E
y : F
hx : ¬x ∈ f.domain
x' : E
hx' : x' ∈ f.domain
c : K
⊢ ↑{ val := x', property := hx' } + ↑{ val := c • x, property := (_ : c • x ∈ span K {x}) } =
    ↑{ val := x' + c • x, property := (_ : x' + c • x ∈ f.domain ⊔ (mkSpanSingleton x y (_ : x = 0 → False)).domain) }
case h
R : Type ?u.359475
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.360556
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : Module K E
inst✝ : Module K F
f : E →ₗ.[K] F
x : E
y : F
hx : ¬x ∈ f.domain
x' : E
hx' : x' ∈ f.domain
c : K
⊢ c • x ∈ (mkSpanSingleton' x y (_ : ∀ (c : K), c • x = 0 → c • y = 0)).domain

case hz
R : Type ?u.359475
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.360556
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : Module K E
inst✝ : Module K F
f : E →ₗ.[K] F
x : E
y : F
hx : ¬x ∈ f.domain
x' : E
hx' : x' ∈ f.domain
c : K
⊢ ↑{ val := x', property := hx' } + ↑{ val := c • x, property := ?h } =
    ↑{ val := x' + c • x, property := (_ : x' + c • x ∈ f.domain ⊔ (mkSpanSingleton x y (_ : x = 0 → False)).domain) }
exact mem_span_singleton.2 ⟨c, rfl⟩
no goals
case hz
R : Type ?u.359475
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.360556
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : Module K E
inst✝ : Module K F
f : E →ₗ.[K] F
x : E
y : F
hx : ¬x ∈ f.domain
x' : E
hx' : x' ∈ f.domain
c : K
⊢ ↑{ val := x', property := hx' } + ↑{ val := c • x, property := (_ : c • x ∈ span K {x}) } =
    ↑{ val := x' + c • x, property := (_ : x' + c • x ∈ f.domain ⊔ (mkSpanSingleton x y (_ : x = 0 → False)).domain) }
rfl