case pos
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : x = 0
⊢ span R {x} = span R {y} ↔ ∃ z, z • x = y

case neg
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
⊢ span R {x} = span R {y} ↔ ∃ z, z • x = y
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
⊢ span R {x} = span R {y} ↔ ∃ z, z • x = y
by_cases hx : x = 0
case pos
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : y = 0
⊢ span R {x} = span R {y} ↔ ∃ z, z • x = y

case neg
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
⊢ span R {x} = span R {y} ↔ ∃ z, z • x = y
case neg
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
⊢ span R {x} = span R {y} ↔ ∃ z, z • x = y
by_cases hy : y = 0
case neg.mp
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
⊢ span R {x} = span R {y} → ∃ z, z • x = y

case neg.mpr
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
⊢ (∃ z, z • x = y) → span R {x} = span R {y}
case neg
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
⊢ span R {x} = span R {y} ↔ ∃ z, z • x = y
constructor
case pos
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : x = 0
⊢ y = 0 ↔ ∃ z, z • 0 = y
case pos
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : x = 0
⊢ span R {x} = span R {y} ↔ ∃ z, z • x = y
rw [hx, span_zero_singleton, eq_comm, span_singleton_eq_bot]
no goals
case pos
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : x = 0
⊢ y = 0 ↔ ∃ z, z • 0 = y
exact ⟨fun hy => ⟨1, by rw [hy, smul_zero]⟩, fun ⟨_, hz⟩ => by rw [← hz, smul_zero]⟩
no goals
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : x = 0
hy : y = 0
⊢ 1 • 0 = y
rw [hy, smul_zero]
no goals
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : x = 0
x✝ : ∃ z, z • 0 = y
w✝ : Rˣ
hz : w✝ • 0 = y
⊢ y = 0
rw [← hz, smul_zero]
case pos
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : y = 0
⊢ x = 0 ↔ ∃ z, z • x = 0
case pos
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : y = 0
⊢ span R {x} = span R {y} ↔ ∃ z, z • x = y
rw [hy, span_zero_singleton, span_singleton_eq_bot]
no goals
case pos
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : y = 0
⊢ x = 0 ↔ ∃ z, z • x = 0
exact ⟨fun hx => ⟨1, by rw [hx, smul_zero]⟩, fun ⟨z, hz⟩ => (smul_eq_zero_iff_eq z).mp hz⟩
no goals
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx✝ : ¬x = 0
hy : y = 0
hx : x = 0
⊢ 1 • x = 0
rw [hx, smul_zero]
case neg.mp
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hxy : span R {x} = span R {y}
⊢ ∃ z, z • x = y
case neg.mp
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
⊢ span R {x} = span R {y} → ∃ z, z • x = y
intro hxy
case neg.mp.intro
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hxy : span R {x} = span R {y}
v : R
hv : v • x = y
⊢ ∃ z, z • x = y
case neg.mp
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hxy : span R {x} = span R {y}
⊢ ∃ z, z • x = y
cases'
  mem_span_singleton.mp
    (by
      rw [hxy]
      apply mem_span_singleton_self) with
  v hv
case neg.mp.intro.intro
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hxy : span R {x} = span R {y}
v : R
hv : v • x = y
i : R
hi : i • y = x
⊢ ∃ z, z • x = y
case neg.mp.intro
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hxy : span R {x} = span R {y}
v : R
hv : v • x = y
⊢ ∃ z, z • x = y
cases'
  mem_span_singleton.mp
    (by
      rw [← hxy]
      apply mem_span_singleton_self) with
  i hi
case neg.mp.intro.intro
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hxy : span R {x} = span R {y}
v : R
hv : v • x = y
i : R
hi : i • y = x
vi : v * i = 1
⊢ ∃ z, z • x = y
case neg.mp.intro.intro
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hxy : span R {x} = span R {y}
v : R
hv : v • x = y
i : R
hi : i • y = x
⊢ ∃ z, z • x = y
have vi : v * i = 1 := by
  rw [← one_smul R y, ← hi, smul_smul] at hv
  exact smul_left_injective R hy hv
case neg.mp.intro.intro
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hxy : span R {x} = span R {y}
v : R
hv : v • x = y
i : R
hi : i • y = x
vi : v * i = 1
iv : i * v = 1
⊢ ∃ z, z • x = y
case neg.mp.intro.intro
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hxy : span R {x} = span R {y}
v : R
hv : v • x = y
i : R
hi : i • y = x
vi : v * i = 1
⊢ ∃ z, z • x = y
have iv : i * v = 1 := by
  rw [← one_smul R x, ← hv, smul_smul] at hi
  exact smul_left_injective R hx hi
no goals
case neg.mp.intro.intro
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hxy : span R {x} = span R {y}
v : R
hv : v • x = y
i : R
hi : i • y = x
vi : v * i = 1
iv : i * v = 1
⊢ ∃ z, z • x = y
exact ⟨⟨v, i, vi, iv⟩, hv⟩
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hxy : span R {x} = span R {y}
⊢ ?m.197857 ∈ span R {y}

R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hxy : span R {x} = span R {y}
⊢ M
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hxy : span R {x} = span R {y}
⊢ ?m.197857 ∈ span ?m.197747 {?m.197858}
rw [hxy]
no goals
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hxy : span R {x} = span R {y}
⊢ ?m.197857 ∈ span R {y}

R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hxy : span R {x} = span R {y}
⊢ M
apply mem_span_singleton_self
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hxy : span R {x} = span R {y}
v : R
hv : v • x = y
⊢ ?m.198638 ∈ span R {x}

R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hxy : span R {x} = span R {y}
v : R
hv : v • x = y
⊢ M
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hxy : span R {x} = span R {y}
v : R
hv : v • x = y
⊢ ?m.198638 ∈ span ?m.198528 {?m.198639}
rw [← hxy]
no goals
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hxy : span R {x} = span R {y}
v : R
hv : v • x = y
⊢ ?m.198638 ∈ span R {x}

R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hxy : span R {x} = span R {y}
v : R
hv : v • x = y
⊢ M
apply mem_span_singleton_self
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hxy : span R {x} = span R {y}
v i : R
hv : (v * i) • y = 1 • y
hi : i • y = x
⊢ v * i = 1
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hxy : span R {x} = span R {y}
v : R
hv : v • x = y
i : R
hi : i • y = x
⊢ v * i = 1
rw [← one_smul R y, ← hi, smul_smul] at hv
no goals
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hxy : span R {x} = span R {y}
v i : R
hv : (v * i) • y = 1 • y
hi : i • y = x
⊢ v * i = 1
exact smul_left_injective R hy hv
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hxy : span R {x} = span R {y}
v : R
hv : v • x = y
i : R
hi : (i * v) • x = 1 • x
vi : v * i = 1
⊢ i * v = 1
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hxy : span R {x} = span R {y}
v : R
hv : v • x = y
i : R
hi : i • y = x
vi : v * i = 1
⊢ i * v = 1
rw [← one_smul R x, ← hv, smul_smul] at hi
no goals
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hxy : span R {x} = span R {y}
v : R
hv : v • x = y
i : R
hi : (i * v) • x = 1 • x
vi : v * i = 1
⊢ i * v = 1
exact smul_left_injective R hx hi
case neg.mpr.intro
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x : M
hx : ¬x = 0
v : Rˣ
hy : ¬v • x = 0
⊢ span R {x} = span R {v • x}
case neg.mpr
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
⊢ (∃ z, z • x = y) → span R {x} = span R {y}
rintro ⟨v, rfl⟩
no goals
case neg.mpr.intro
R✝ : Type ?u.186339
R₂ : Type ?u.186342
K : Type ?u.186345
M✝ : Type ?u.186348
M₂ : Type ?u.186351
V : Type ?u.186354
S : Type ?u.186357
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✝
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x : M
hx : ¬x = 0
v : Rˣ
hy : ¬v • x = 0
⊢ span R {x} = span R {v • x}
rw [span_singleton_group_smul_eq]