case refine'_1
R : Type u_2
R₂ : Type ?u.30116
K : Type ?u.30119
M : Type u_1
M₂ : Type ?u.30125
V : Type ?u.30128
S : Type ?u.30131
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝² : M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
x✝¹ : { x // x ∈ ↑(span R s) }
x : M
hx : x ∈ ↑(span R s)
x✝ : { val := x, property := hx } ∈ ⊤
⊢ (fun x hx => { val := x, property := hx } ∈ span R (Subtype.val ⁻¹' s)) 0 (_ : 0 ∈ span R s)

case refine'_2
R : Type u_2
R₂ : Type ?u.30116
K : Type ?u.30119
M : Type u_1
M₂ : Type ?u.30125
V : Type ?u.30128
S : Type ?u.30131
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝⁵ : M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
x✝⁴ : { x // x ∈ ↑(span R s) }
x✝³ : M
hx : x✝³ ∈ ↑(span R s)
x✝² : { val := x✝³, property := hx } ∈ ⊤
x : M
x✝¹ : x ∈ span R s
y : M
x✝ : y ∈ span R s
⊢ (fun x hx => { val := x, property := hx } ∈ span R (Subtype.val ⁻¹' s)) x x✝¹ →
    (fun x hx => { val := x, property := hx } ∈ span R (Subtype.val ⁻¹' s)) y x✝ →
      (fun x hx => { val := x, property := hx } ∈ span R (Subtype.val ⁻¹' s)) (x + y) (_ : x + y ∈ span R s)

case refine'_3
R : Type u_2
R₂ : Type ?u.30116
K : Type ?u.30119
M : Type u_1
M₂ : Type ?u.30125
V : Type ?u.30128
S : Type ?u.30131
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝⁴ : M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
x✝³ : { x // x ∈ ↑(span R s) }
x✝² : M
hx : x✝² ∈ ↑(span R s)
x✝¹ : { val := x✝², property := hx } ∈ ⊤
r : R
x : M
x✝ : x ∈ span R s
⊢ (fun x hx => { val := x, property := hx } ∈ span R (Subtype.val ⁻¹' s)) x x✝ →
    (fun x hx => { val := x, property := hx } ∈ span R (Subtype.val ⁻¹' s)) (r • x) (_ : r • x ∈ span R s)
R : Type u_2
R₂ : Type ?u.30116
K : Type ?u.30119
M : Type u_1
M₂ : Type ?u.30125
V : Type ?u.30128
S : Type ?u.30131
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝² : M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
x✝¹ : { x // x ∈ ↑(span R s) }
x : M
hx : x ∈ ↑(span R s)
x✝ : { val := x, property := hx } ∈ ⊤
⊢ { val := x, property := hx } ∈ span R (Subtype.val ⁻¹' s)
refine' span_induction' (p := fun x hx ↦ (⟨x, hx⟩ : span R s) ∈ span R (Subtype.val ⁻¹' s))
  (fun x' hx' ↦ subset_span hx') _ (fun x _ y _ ↦ _) (fun r x _ ↦ _) hx
no goals
case refine'_1
R : Type u_2
R₂ : Type ?u.30116
K : Type ?u.30119
M : Type u_1
M₂ : Type ?u.30125
V : Type ?u.30128
S : Type ?u.30131
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝² : M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
x✝¹ : { x // x ∈ ↑(span R s) }
x : M
hx : x ∈ ↑(span R s)
x✝ : { val := x, property := hx } ∈ ⊤
⊢ (fun x hx => { val := x, property := hx } ∈ span R (Subtype.val ⁻¹' s)) 0 (_ : 0 ∈ span R s)
exact zero_mem _
no goals
case refine'_2
R : Type u_2
R₂ : Type ?u.30116
K : Type ?u.30119
M : Type u_1
M₂ : Type ?u.30125
V : Type ?u.30128
S : Type ?u.30131
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝⁵ : M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
x✝⁴ : { x // x ∈ ↑(span R s) }
x✝³ : M
hx : x✝³ ∈ ↑(span R s)
x✝² : { val := x✝³, property := hx } ∈ ⊤
x : M
x✝¹ : x ∈ span R s
y : M
x✝ : y ∈ span R s
⊢ (fun x hx => { val := x, property := hx } ∈ span R (Subtype.val ⁻¹' s)) x x✝¹ →
    (fun x hx => { val := x, property := hx } ∈ span R (Subtype.val ⁻¹' s)) y x✝ →
      (fun x hx => { val := x, property := hx } ∈ span R (Subtype.val ⁻¹' s)) (x + y) (_ : x + y ∈ span R s)
exact add_mem
no goals
case refine'_3
R : Type u_2
R₂ : Type ?u.30116
K : Type ?u.30119
M : Type u_1
M₂ : Type ?u.30125
V : Type ?u.30128
S : Type ?u.30131
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝⁴ : M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
x✝³ : { x // x ∈ ↑(span R s) }
x✝² : M
hx : x✝² ∈ ↑(span R s)
x✝¹ : { val := x✝², property := hx } ∈ ⊤
r : R
x : M
x✝ : x ∈ span R s
⊢ (fun x hx => { val := x, property := hx } ∈ span R (Subtype.val ⁻¹' s)) x x✝ →
    (fun x hx => { val := x, property := hx } ∈ span R (Subtype.val ⁻¹' s)) (r • x) (_ : r • x ∈ span R s)
exact smul_mem _ _