case refine_1
R : Type u_2
R₂ : Type ?u.115596
K : Type ?u.115599
M : Type u_1
M₂ : Type ?u.115605
V : Type ?u.115608
S : Type ?u.115611
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
y : M
h : x ∈ span R {y}
⊢ ∀ (x : M), x ∈ {y} → ∃ a, a • y = x

case refine_2
R : Type u_2
R₂ : Type ?u.115596
K : Type ?u.115599
M : Type u_1
M₂ : Type ?u.115605
V : Type ?u.115608
S : Type ?u.115611
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
y : M
h : x ∈ span R {y}
⊢ ∃ a, a • y = 0

case refine_3
R : Type u_2
R₂ : Type ?u.115596
K : Type ?u.115599
M : Type u_1
M₂ : Type ?u.115605
V : Type ?u.115608
S : Type ?u.115611
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
y : M
h : x ∈ span R {y}
⊢ ∀ (x y_1 : M), (∃ a, a • y = x) → (∃ a, a • y = y_1) → ∃ a, a • y = x + y_1

case refine_4
R : Type u_2
R₂ : Type ?u.115596
K : Type ?u.115599
M : Type u_1
M₂ : Type ?u.115605
V : Type ?u.115608
S : Type ?u.115611
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
y : M
h : x ∈ span R {y}
⊢ ∀ (a : R) (x : M), (∃ a, a • y = x) → ∃ a_2, a_2 • y = a • x
R : Type u_2
R₂ : Type ?u.115596
K : Type ?u.115599
M : Type u_1
M₂ : Type ?u.115605
V : Type ?u.115608
S : Type ?u.115611
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
y : M
h : x ∈ span R {y}
⊢ ∃ a, a • y = x
refine span_induction h ?_ ?_ ?_ ?_
case refine_1.refl
R : Type u_2
R₂ : Type ?u.115596
K : Type ?u.115599
M : Type u_1
M₂ : Type ?u.115605
V : Type ?u.115608
S : Type ?u.115611
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
y : M
h : x ∈ span R {y}
⊢ ∃ a, a • y = y
case refine_1
R : Type u_2
R₂ : Type ?u.115596
K : Type ?u.115599
M : Type u_1
M₂ : Type ?u.115605
V : Type ?u.115608
S : Type ?u.115611
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
y : M
h : x ∈ span R {y}
⊢ ∀ (x : M), x ∈ {y} → ∃ a, a • y = x
rintro y (rfl | ⟨⟨_⟩⟩)
no goals
case refine_1.refl
R : Type u_2
R₂ : Type ?u.115596
K : Type ?u.115599
M : Type u_1
M₂ : Type ?u.115605
V : Type ?u.115608
S : Type ?u.115611
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
y : M
h : x ∈ span R {y}
⊢ ∃ a, a • y = y
exact ⟨1, by simp⟩
no goals
R : Type u_2
R₂ : Type ?u.115596
K : Type ?u.115599
M : Type u_1
M₂ : Type ?u.115605
V : Type ?u.115608
S : Type ?u.115611
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
y : M
h : x ∈ span R {y}
⊢ 1 • y = y
simp
no goals
case refine_2
R : Type u_2
R₂ : Type ?u.115596
K : Type ?u.115599
M : Type u_1
M₂ : Type ?u.115605
V : Type ?u.115608
S : Type ?u.115611
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
y : M
h : x ∈ span R {y}
⊢ ∃ a, a • y = 0
exact ⟨0, by simp⟩
no goals
R : Type u_2
R₂ : Type ?u.115596
K : Type ?u.115599
M : Type u_1
M₂ : Type ?u.115605
V : Type ?u.115608
S : Type ?u.115611
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
y : M
h : x ∈ span R {y}
⊢ 0 • y = 0
simp
case refine_3.intro.intro
R : Type u_2
R₂ : Type ?u.115596
K : Type ?u.115599
M : Type u_1
M₂ : Type ?u.115605
V : Type ?u.115608
S : Type ?u.115611
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
y : M
h : x ∈ span R {y}
a b : R
⊢ ∃ a_1, a_1 • y = a • y + b • y
case refine_3
R : Type u_2
R₂ : Type ?u.115596
K : Type ?u.115599
M : Type u_1
M₂ : Type ?u.115605
V : Type ?u.115608
S : Type ?u.115611
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
y : M
h : x ∈ span R {y}
⊢ ∀ (x y_1 : M), (∃ a, a • y = x) → (∃ a, a • y = y_1) → ∃ a, a • y = x + y_1
rintro _ _ ⟨a, rfl⟩ ⟨b, rfl⟩
no goals
case refine_3.intro.intro
R : Type u_2
R₂ : Type ?u.115596
K : Type ?u.115599
M : Type u_1
M₂ : Type ?u.115605
V : Type ?u.115608
S : Type ?u.115611
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
y : M
h : x ∈ span R {y}
a b : R
⊢ ∃ a_1, a_1 • y = a • y + b • y
exact ⟨a + b, by simp [add_smul]⟩
no goals
R : Type u_2
R₂ : Type ?u.115596
K : Type ?u.115599
M : Type u_1
M₂ : Type ?u.115605
V : Type ?u.115608
S : Type ?u.115611
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
y : M
h : x ∈ span R {y}
a b : R
⊢ (a + b) • y = a • y + b • y
simp [add_smul]
case refine_4.intro
R : Type u_2
R₂ : Type ?u.115596
K : Type ?u.115599
M : Type u_1
M₂ : Type ?u.115605
V : Type ?u.115608
S : Type ?u.115611
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
y : M
h : x ∈ span R {y}
a b : R
⊢ ∃ a_1, a_1 • y = a • b • y
case refine_4
R : Type u_2
R₂ : Type ?u.115596
K : Type ?u.115599
M : Type u_1
M₂ : Type ?u.115605
V : Type ?u.115608
S : Type ?u.115611
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
y : M
h : x ∈ span R {y}
⊢ ∀ (a : R) (x : M), (∃ a, a • y = x) → ∃ a_2, a_2 • y = a • x
rintro a _ ⟨b, rfl⟩
no goals
case refine_4.intro
R : Type u_2
R₂ : Type ?u.115596
K : Type ?u.115599
M : Type u_1
M₂ : Type ?u.115605
V : Type ?u.115608
S : Type ?u.115611
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
y : M
h : x ∈ span R {y}
a b : R
⊢ ∃ a_1, a_1 • y = a • b • y
exact ⟨a * b, by simp [smul_smul]⟩
no goals
R : Type u_2
R₂ : Type ?u.115596
K : Type ?u.115599
M : Type u_1
M₂ : Type ?u.115605
V : Type ?u.115608
S : Type ?u.115611
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
y : M
h : x ∈ span R {y}
a b : R
⊢ (a * b) • y = a • b • y
simp [smul_smul]
case intro.refl
R : Type u_2
R₂ : Type ?u.115596
K : Type ?u.115599
M : Type u_1
M₂ : Type ?u.115605
V : Type ?u.115608
S : Type ?u.115611
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
y : M
a : R
⊢ a • y ∈ span R {y}
R : Type u_2
R₂ : Type ?u.115596
K : Type ?u.115599
M : Type u_1
M₂ : Type ?u.115605
V : Type ?u.115608
S : Type ?u.115611
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
y : M
⊢ (∃ a, a • y = x) → x ∈ span R {y}
rintro ⟨a, y, rfl⟩
no goals
case intro.refl
R : Type u_2
R₂ : Type ?u.115596
K : Type ?u.115599
M : Type u_1
M₂ : Type ?u.115605
V : Type ?u.115608
S : Type ?u.115611
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
y : M
a : R
⊢ a • y ∈ span R {y}
exact smul_mem _ _ (subset_span <| by simp)
no goals
R : Type u_2
R₂ : Type ?u.115596
K : Type ?u.115599
M : Type u_1
M₂ : Type ?u.115605
V : Type ?u.115608
S : Type ?u.115611
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
y : M
a : R
⊢ y ∈ {y}
simp