R : Type u_2
R₂ : Type ?u.24742
K : Type ?u.24745
M : Type u_1
M₂ : Type ?u.24751
V : Type ?u.24754
S : Type ?u.24757
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
p : (x : M) → x ∈ span R s → Prop
Hs : ∀ (x : M) (h : x ∈ s), p x (_ : x ∈ ↑(span R s))
H0 : p 0 (_ : 0 ∈ span R s)
H1 : ∀ (x : M) (hx : x ∈ span R s) (y : M) (hy : y ∈ span R s), p x hx → p y hy → p (x + y) (_ : x + y ∈ span R s)
H2 : ∀ (a : R) (x : M) (hx : x ∈ span R s), p x hx → p (a • x) (_ : a • x ∈ span R s)
x : M
hx : x ∈ span R s
⊢ ∃ x_1, p x x_1
R : Type u_2
R₂ : Type ?u.24742
K : Type ?u.24745
M : Type u_1
M₂ : Type ?u.24751
V : Type ?u.24754
S : Type ?u.24757
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
p : (x : M) → x ∈ span R s → Prop
Hs : ∀ (x : M) (h : x ∈ s), p x (_ : x ∈ ↑(span R s))
H0 : p 0 (_ : 0 ∈ span R s)
H1 : ∀ (x : M) (hx : x ∈ span R s) (y : M) (hy : y ∈ span R s), p x hx → p y hy → p (x + y) (_ : x + y ∈ span R s)
H2 : ∀ (a : R) (x : M) (hx : x ∈ span R s), p x hx → p (a • x) (_ : a • x ∈ span R s)
x : M
hx : x ∈ span R s
⊢ p x hx
refine' Exists.elim _ fun (hx : x ∈ span R s) (hc : p x hx) => hc
no goals
R : Type u_2
R₂ : Type ?u.24742
K : Type ?u.24745
M : Type u_1
M₂ : Type ?u.24751
V : Type ?u.24754
S : Type ?u.24757
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
p : (x : M) → x ∈ span R s → Prop
Hs : ∀ (x : M) (h : x ∈ s), p x (_ : x ∈ ↑(span R s))
H0 : p 0 (_ : 0 ∈ span R s)
H1 : ∀ (x : M) (hx : x ∈ span R s) (y : M) (hy : y ∈ span R s), p x hx → p y hy → p (x + y) (_ : x + y ∈ span R s)
H2 : ∀ (a : R) (x : M) (hx : x ∈ span R s), p x hx → p (a • x) (_ : a • x ∈ span R s)
x : M
hx : x ∈ span R s
⊢ ∃ x_1, p x x_1
refine'
  span_induction hx (fun m hm => ⟨subset_span hm, Hs m hm⟩) ⟨zero_mem _, H0⟩
    (fun x y hx hy =>
      Exists.elim hx fun hx' hx =>
        Exists.elim hy fun hy' hy => ⟨add_mem hx' hy', H1 _ _ _ _ hx hy⟩)
    fun r x hx => Exists.elim hx fun hx' hx => ⟨smul_mem _ _ hx', H2 r _ _ hx⟩