[GOAL]
R : Type u_1
inst✝⁶ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_4
inst✝¹ : DecidableEq ι
x✝ y✝ z : M
inst✝ : Subsingleton M
x y : M
⊢ SameRay R x y
[PROOFSTEP]
rw [Subsingleton.elim x 0]
[GOAL]
R : Type u_1
inst✝⁶ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_4
inst✝¹ : DecidableEq ι
x✝ y✝ z : M
inst✝ : Subsingleton M
x y : M
⊢ SameRay R 0 y
[PROOFSTEP]
exact zero_left _
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x✝ y z x : M
⊢ SameRay R x x
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u_1
inst✝⁶ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_4
inst✝¹ : DecidableEq ι
x✝ y z x : M
inst✝ : Nontrivial R
⊢ SameRay R x x
[PROOFSTEP]
exact Or.inr (Or.inr <| ⟨1, 1, zero_lt_one, zero_lt_one, rfl⟩)
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy : y = 0 → x = 0 ∨ z = 0
⊢ SameRay R x z
[PROOFSTEP]
rcases eq_or_ne x 0 with (rfl | hx)
[GOAL]
case inl
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
y z : M
hyz : SameRay R y z
hxy : SameRay R 0 y
hy : y = 0 → 0 = 0 ∨ z = 0
⊢ SameRay R 0 z
[PROOFSTEP]
exact zero_left z
[GOAL]
case inr
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
⊢ SameRay R x z
[PROOFSTEP]
rcases eq_or_ne z 0 with (rfl | hz)
[GOAL]
case inr.inl
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y : M
hxy : SameRay R x y
hx : x ≠ 0
hyz : SameRay R y 0
hy : y = 0 → x = 0 ∨ 0 = 0
⊢ SameRay R x 0
[PROOFSTEP]
exact zero_right x
[GOAL]
case inr.inr
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
hz : z ≠ 0
⊢ SameRay R x z
[PROOFSTEP]
rcases eq_or_ne y 0 with (rfl | hy)
[GOAL]
case inr.inr.inl
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x z : M
hx : x ≠ 0
hz : z ≠ 0
hxy : SameRay R x 0
hyz : SameRay R 0 z
hy : 0 = 0 → x = 0 ∨ z = 0
⊢ SameRay R x z
[PROOFSTEP]
exact (hy rfl).elim (fun h => (hx h).elim) fun h => (hz h).elim
[GOAL]
case inr.inr.inr
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy✝ : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
hz : z ≠ 0
hy : y ≠ 0
⊢ SameRay R x z
[PROOFSTEP]
rcases hxy.exists_pos hx hy with ⟨r₁, r₂, hr₁, hr₂, h₁⟩
[GOAL]
case inr.inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy✝ : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
hz : z ≠ 0
hy : y ≠ 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h₁ : r₁ • x = r₂ • y
⊢ SameRay R x z
[PROOFSTEP]
rcases hyz.exists_pos hy hz with ⟨r₃, r₄, hr₃, hr₄, h₂⟩
[GOAL]
case inr.inr.inr.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy✝ : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
hz : z ≠ 0
hy : y ≠ 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h₁ : r₁ • x = r₂ • y
r₃ r₄ : R
hr₃ : 0 < r₃
hr₄ : 0 < r₄
h₂ : r₃ • y = r₄ • z
⊢ SameRay R x z
[PROOFSTEP]
refine' Or.inr (Or.inr <| ⟨r₃ * r₁, r₂ * r₄, mul_pos hr₃ hr₁, mul_pos hr₂ hr₄, _⟩)
[GOAL]
case inr.inr.inr.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy✝ : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
hz : z ≠ 0
hy : y ≠ 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h₁ : r₁ • x = r₂ • y
r₃ r₄ : R
hr₃ : 0 < r₃
hr₄ : 0 < r₄
h₂ : r₃ • y = r₄ • z
⊢ (r₃ * r₁) • x = (r₂ * r₄) • z
[PROOFSTEP]
rw [mul_smul, mul_smul, h₁, ← h₂, smul_comm]
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z v : M
r : R
h✝ : 0 ≤ r
h : 0 < r
⊢ 0 < 1
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u_1
inst✝⁶ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_4
inst✝¹ : DecidableEq ι
x y z v : M
r : R
h✝ : 0 ≤ r
h : 0 < r
inst✝ : Nontrivial R
⊢ 0 < 1
[PROOFSTEP]
exact zero_lt_one
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
r : R
h : SameRay R x y
hr : 0 ≤ r
hy : y = 0
⊢ r • y = 0
[PROOFSTEP]
rw [hy, smul_zero]
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
f : M →ₗ[R] N
h : SameRay R x y
hx : x = 0
⊢ ↑f x = 0
[PROOFSTEP]
rw [hx, map_zero]
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
f : M →ₗ[R] N
h : SameRay R x y
hy : y = 0
⊢ ↑f y = 0
[PROOFSTEP]
rw [hy, map_zero]
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
f : M →ₗ[R] N
h✝ : SameRay R x y
x✝ : ∃ r₁ r₂, 0 < r₁ ∧ 0 < r₂ ∧ r₁ • x = r₂ • y
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • x = r₂ • y
⊢ r₁ • ↑f x = r₂ • ↑f y
[PROOFSTEP]
rw [← f.map_smul, ← f.map_smul, h]
[GOAL]
R : Type u_1
inst✝⁶ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_4
inst✝¹ : DecidableEq ι
x y z : M
F : Type u_5
inst✝ : LinearMapClass F R M N
f : F
hf : Function.Injective ↑f
⊢ SameRay R (↑f x) (↑f y) ↔ SameRay R x y
[PROOFSTEP]
simp only [SameRay, map_zero, ← hf.eq_iff, map_smul]
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
hx : SameRay R x z
hy : SameRay R y z
⊢ SameRay R (x + y) z
[PROOFSTEP]
rcases eq_or_ne x 0 with (rfl | hx₀)
[GOAL]
case inl
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
y z : M
hy : SameRay R y z
hx : SameRay R 0 z
⊢ SameRay R (0 + y) z
[PROOFSTEP]
rwa [zero_add]
[GOAL]
case inr
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
⊢ SameRay R (x + y) z
[PROOFSTEP]
rcases eq_or_ne y 0 with (rfl | hy₀)
[GOAL]
case inr.inl
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x z : M
hx : SameRay R x z
hx₀ : x ≠ 0
hy : SameRay R 0 z
⊢ SameRay R (x + 0) z
[PROOFSTEP]
rwa [add_zero]
[GOAL]
case inr.inr
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ SameRay R (x + y) z
[PROOFSTEP]
rcases eq_or_ne z 0 with (rfl | hz₀)
[GOAL]
case inr.inr.inl
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y : M
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hx : SameRay R x 0
hy : SameRay R y 0
⊢ SameRay R (x + y) 0
[PROOFSTEP]
apply zero_right
[GOAL]
case inr.inr.inr
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hz₀ : z ≠ 0
⊢ SameRay R (x + y) z
[PROOFSTEP]
rcases hx.exists_pos hx₀ hz₀ with ⟨rx, rz₁, hrx, hrz₁, Hx⟩
[GOAL]
case inr.inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hz₀ : z ≠ 0
rx rz₁ : R
hrx : 0 < rx
hrz₁ : 0 < rz₁
Hx : rx • x = rz₁ • z
⊢ SameRay R (x + y) z
[PROOFSTEP]
rcases hy.exists_pos hy₀ hz₀ with ⟨ry, rz₂, hry, hrz₂, Hy⟩
[GOAL]
case inr.inr.inr.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hz₀ : z ≠ 0
rx rz₁ : R
hrx : 0 < rx
hrz₁ : 0 < rz₁
Hx : rx • x = rz₁ • z
ry rz₂ : R
hry : 0 < ry
hrz₂ : 0 < rz₂
Hy : ry • y = rz₂ • z
⊢ SameRay R (x + y) z
[PROOFSTEP]
refine' Or.inr (Or.inr ⟨rx * ry, ry * rz₁ + rx * rz₂, mul_pos hrx hry, _, _⟩)
[GOAL]
case inr.inr.inr.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hz₀ : z ≠ 0
rx rz₁ : R
hrx : 0 < rx
hrz₁ : 0 < rz₁
Hx : rx • x = rz₁ • z
ry rz₂ : R
hry : 0 < ry
hrz₂ : 0 < rz₂
Hy : ry • y = rz₂ • z
⊢ 0 < ry * rz₁ + rx * rz₂
[PROOFSTEP]
apply_rules [add_pos, mul_pos]
[GOAL]
case inr.inr.inr.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hz₀ : z ≠ 0
rx rz₁ : R
hrx : 0 < rx
hrz₁ : 0 < rz₁
Hx : rx • x = rz₁ • z
ry rz₂ : R
hry : 0 < ry
hrz₂ : 0 < rz₂
Hy : ry • y = rz₂ • z
⊢ (rx * ry) • (x + y) = (ry * rz₁ + rx * rz₂) • z
[PROOFSTEP]
simp only [mul_smul, smul_add, add_smul, ← Hx, ← Hy]
[GOAL]
case inr.inr.inr.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hz₀ : z ≠ 0
rx rz₁ : R
hrx : 0 < rx
hrz₁ : 0 < rz₁
Hx : rx • x = rz₁ • z
ry rz₂ : R
hry : 0 < ry
hrz₂ : 0 < rz₂
Hy : ry • y = rz₂ • z
⊢ rx • ry • x + rx • ry • y = ry • rx • x + rx • ry • y
[PROOFSTEP]
rw [smul_comm]
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
⊢ ∀ {x y z : RayVector R M}, SameRay R ↑x ↑y → SameRay R ↑y ↑z → SameRay R ↑x ↑z
[PROOFSTEP]
intros x y z hxy hyz
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : RayVector R M
hxy : SameRay R ↑x ↑y
hyz : SameRay R ↑y ↑z
⊢ SameRay R ↑x ↑z
[PROOFSTEP]
exact hxy.trans hyz fun hy => (y.2 hy).elim
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
u : Rˣ
hu : 0 < ↑u
v : Ray R M
⊢ u • v = v
[PROOFSTEP]
induction v using Module.Ray.ind
[GOAL]
case h
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
u : Rˣ
hu : 0 < ↑u
v✝ : M
hv✝ : v✝ ≠ 0
⊢ u • rayOfNeZero R v✝ hv✝ = rayOfNeZero R v✝ hv✝
[PROOFSTEP]
rw [smul_rayOfNeZero, ray_eq_iff]
[GOAL]
case h
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
u : Rˣ
hu : 0 < ↑u
v✝ : M
hv✝ : v✝ ≠ 0
⊢ SameRay R (u • v✝) v✝
[PROOFSTEP]
exact SameRay.sameRay_pos_smul_left _ hu
[GOAL]
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M
⊢ SameRay R (-x) (-y) ↔ SameRay R x y
[PROOFSTEP]
simp only [SameRay, neg_eq_zero, smul_neg, neg_inj]
[GOAL]
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M
⊢ SameRay R (-x) y ↔ SameRay R x (-y)
[PROOFSTEP]
rw [← sameRay_neg_iff, neg_neg]
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x y : M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : r < 0
h : SameRay R x (r • x)
⊢ x = 0
[PROOFSTEP]
rcases h with (rfl | h₀ | ⟨r₁, r₂, hr₁, hr₂, h⟩)
[GOAL]
case inl
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
y : M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : r < 0
⊢ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case inr.inl
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x y : M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : r < 0
h₀ : r • x = 0
⊢ x = 0
[PROOFSTEP]
simpa [hr.ne] using h₀
[GOAL]
case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x y : M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : r < 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • x = r₂ • r • x
⊢ x = 0
[PROOFSTEP]
rw [← sub_eq_zero, smul_smul, ← sub_smul, smul_eq_zero] at h
[GOAL]
case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x y : M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : r < 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h✝ : r₁ • x = r₂ • r • x
h : r₁ - r₂ * r = 0 ∨ x = 0
⊢ x = 0
[PROOFSTEP]
refine' h.resolve_left (ne_of_gt <| sub_pos.2 _)
[GOAL]
case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x y : M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : r < 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h✝ : r₁ • x = r₂ • r • x
h : r₁ - r₂ * r = 0 ∨ x = 0
⊢ r₂ * r < r₁
[PROOFSTEP]
exact (mul_neg_of_pos_of_neg hr₂ hr).trans hr₁
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x y : M
inst✝ : NoZeroSMulDivisors R M
h : SameRay R x (-x)
⊢ x = 0
[PROOFSTEP]
nontriviality M
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x y : M
inst✝ : NoZeroSMulDivisors R M
h : SameRay R x (-x)
✝ : Nontrivial M
⊢ x = 0
[PROOFSTEP]
haveI : Nontrivial R := Module.nontrivial R M
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x y : M
inst✝ : NoZeroSMulDivisors R M
h : SameRay R x (-x)
✝ : Nontrivial M
this : Nontrivial R
⊢ x = 0
[PROOFSTEP]
refine' eq_zero_of_sameRay_neg_smul_right (neg_lt_zero.2 (zero_lt_one' R)) _
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x y : M
inst✝ : NoZeroSMulDivisors R M
h : SameRay R x (-x)
✝ : Nontrivial M
this : Nontrivial R
⊢ SameRay R x (-1 • x)
[PROOFSTEP]
rwa [neg_one_smul]
[GOAL]
R✝ : Type u_1
inst✝⁴ : StrictOrderedCommRing R✝
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R✝ M
inst✝ : Module R✝ N
x y : M
R : Type u_4
v : RayVector R M
⊢ - -v = v
[PROOFSTEP]
rw [Subtype.ext_iff, coe_neg, coe_neg, neg_neg]
[GOAL]
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ y : M
x : Ray R M
⊢ - -x = x
[PROOFSTEP]
apply ind R (by simp) x
[GOAL]
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ y : M
x : Ray R M
⊢ ∀ (v : M) (hv : v ≠ 0), - -rayOfNeZero R v hv = rayOfNeZero R v hv
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x✝ y : M
inst✝ : NoZeroSMulDivisors R M
x : Ray R M
⊢ x ≠ -x
[PROOFSTEP]
induction' x using Module.Ray.ind with x hx
[GOAL]
case h
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x✝ y : M
inst✝ : NoZeroSMulDivisors R M
x : M
hx : x ≠ 0
⊢ rayOfNeZero R x hx ≠ -rayOfNeZero R x hx
[PROOFSTEP]
rw [neg_rayOfNeZero, Ne.def, ray_eq_iff]
[GOAL]
case h
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x✝ y : M
inst✝ : NoZeroSMulDivisors R M
x : M
hx : x ≠ 0
⊢ ¬SameRay R x (-x)
[PROOFSTEP]
exact mt eq_zero_of_sameRay_self_neg hx
[GOAL]
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M
u : Rˣ
v : Ray R M
⊢ -u • v = -(u • v)
[PROOFSTEP]
induction v using Module.Ray.ind
[GOAL]
case h
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M
u : Rˣ
v✝ : M
hv✝ : v✝ ≠ 0
⊢ -u • rayOfNeZero R v✝ hv✝ = -(u • rayOfNeZero R v✝ hv✝)
[PROOFSTEP]
simp only [smul_rayOfNeZero, Units.smul_def, Units.val_neg, neg_smul, neg_rayOfNeZero]
[GOAL]
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M
u : Rˣ
hu : ↑u < 0
v : Ray R M
⊢ u • v = -v
[PROOFSTEP]
rw [← neg_inj, neg_neg, ← neg_units_smul, units_smul_of_pos]
[GOAL]
case hu
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M
u : Rˣ
hu : ↑u < 0
v : Ray R M
⊢ 0 < ↑(-u)
[PROOFSTEP]
rwa [Units.val_neg, Right.neg_pos_iff]
[GOAL]
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M
f : M ≃ₗ[R] N
v : Ray R M
⊢ ↑(map f) (-v) = -↑(map f) v
[PROOFSTEP]
induction' v using Module.Ray.ind with g hg
[GOAL]
case h
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M
f : M ≃ₗ[R] N
g : M
hg : g ≠ 0
⊢ ↑(map f) (-rayOfNeZero R g hg) = -↑(map f) (rayOfNeZero R g hg)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝² : LinearOrderedCommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v₁ v₂ : M
h : v₁ ∈ MulAction.orbit { x // x ∈ Units.posSubgroup R } v₂
⊢ SameRay R v₁ v₂
[PROOFSTEP]
rcases h with ⟨⟨r, hr : 0 < r.1⟩, rfl : r • v₂ = v₁⟩
[GOAL]
case intro.mk
R : Type u_1
inst✝² : LinearOrderedCommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v₂ : M
r : Rˣ
hr : 0 < ↑r
⊢ SameRay R (r • v₂) v₂
[PROOFSTEP]
exact SameRay.sameRay_pos_smul_left _ hr
[GOAL]
R : Type u_1
inst✝² : LinearOrderedCommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
u : Rˣ
v : Module.Ray R M
this : 0 < ↑u * ↑u
⊢ 0 < ↑(u * u)
[PROOFSTEP]
exact this
[GOAL]
R : Type u_1
inst✝² : LinearOrderedCommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
u : Rˣ
v : Module.Ray R M
this : 0 < ↑u * ↑u
⊢ (u * u) • u⁻¹ • v = u • v
[PROOFSTEP]
rw [mul_smul, smul_inv_smul]
[GOAL]
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
v : M
hv : v ≠ 0
r : R
hr : r ≠ 0
⊢ SameRay R v (r • v) ↔ 0 < r
[PROOFSTEP]
simp only [sameRay_smul_right_iff, hv, or_false_iff, hr.symm.le_iff_lt]
[GOAL]
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
v : M
r : R
⊢ SameRay R (-v) (r • v) ↔ r ≤ 0 ∨ v = 0
[PROOFSTEP]
rw [← sameRay_neg_iff, neg_neg, ← neg_smul, sameRay_smul_right_iff, neg_nonneg]
[GOAL]
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
v : M
r : R
hv : v ≠ 0
hr : r ≠ 0
⊢ SameRay R (-v) (r • v) ↔ r < 0
[PROOFSTEP]
simp only [sameRay_neg_smul_right_iff, hv, or_false_iff, hr.le_iff_lt]
[GOAL]
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
u : Rˣ
v : Module.Ray R M
⊢ u • v = v ↔ 0 < ↑u
[PROOFSTEP]
induction' v using Module.Ray.ind with v hv
[GOAL]
case h
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
u : Rˣ
v : M
hv : v ≠ 0
⊢ u • rayOfNeZero R v hv = rayOfNeZero R v hv ↔ 0 < ↑u
[PROOFSTEP]
simp only [smul_rayOfNeZero, ray_eq_iff, Units.smul_def, sameRay_smul_left_iff_of_ne hv u.ne_zero]
[GOAL]
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
u : Rˣ
v : Module.Ray R M
⊢ u • v = -v ↔ ↑u < 0
[PROOFSTEP]
rw [← neg_inj, neg_neg, ← Module.Ray.neg_units_smul, units_smul_eq_self_iff, Units.val_neg, neg_pos]
[GOAL]
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
⊢ SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : x = 0
⊢ SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]
[PROOFSTEP]
simpa [hx] using fun h : LinearIndependent R ![0, y] => h.ne_zero 0 rfl
[GOAL]
case neg
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
⊢ SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]
[PROOFSTEP]
by_cases hy : y = 0
[GOAL]
case pos
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : y = 0
⊢ SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]
[PROOFSTEP]
simpa [hy] using fun h : LinearIndependent R ![x, 0] => h.ne_zero 1 rfl
[GOAL]
case neg
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
⊢ SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]
[PROOFSTEP]
simp_rw [Fintype.not_linearIndependent_iff]
[GOAL]
case neg
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
⊢ SameRay R x y ∨ SameRay R x (-y) ↔
    ∃ g, ∑ i : Fin (Nat.succ (Nat.succ 0)), g i • Matrix.vecCons x ![y] i = 0 ∧ ∃ i, g i ≠ 0
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case neg.refine'_1
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
h : SameRay R x y ∨ SameRay R x (-y)
⊢ ∃ g, ∑ i : Fin (Nat.succ (Nat.succ 0)), g i • Matrix.vecCons x ![y] i = 0 ∧ ∃ i, g i ≠ 0
[PROOFSTEP]
rcases h with ((hx0 | hy0 | ⟨r₁, r₂, hr₁, _, h⟩) | (hx0 | hy0 | ⟨r₁, r₂, hr₁, _, h⟩))
[GOAL]
case neg.refine'_1.inl.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hx0 : x = 0
⊢ ∃ g, ∑ i : Fin (Nat.succ (Nat.succ 0)), g i • Matrix.vecCons x ![y] i = 0 ∧ ∃ i, g i ≠ 0
[PROOFSTEP]
exact False.elim (hx hx0)
[GOAL]
case neg.refine'_1.inl.inr.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hy0 : y = 0
⊢ ∃ g, ∑ i : Fin (Nat.succ (Nat.succ 0)), g i • Matrix.vecCons x ![y] i = 0 ∧ ∃ i, g i ≠ 0
[PROOFSTEP]
exact False.elim (hy hy0)
[GOAL]
case neg.refine'_1.inl.inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
r₁ r₂ : R
hr₁ : 0 < r₁
left✝ : 0 < r₂
h : r₁ • x = r₂ • y
⊢ ∃ g, ∑ i : Fin (Nat.succ (Nat.succ 0)), g i • Matrix.vecCons x ![y] i = 0 ∧ ∃ i, g i ≠ 0
[PROOFSTEP]
refine' ⟨![r₁, -r₂], _⟩
[GOAL]
case neg.refine'_1.inl.inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
r₁ r₂ : R
hr₁ : 0 < r₁
left✝ : 0 < r₂
h : r₁ • x = r₂ • y
⊢ ∑ i : Fin (Nat.succ (Nat.succ 0)), Matrix.vecCons r₁ ![-r₂] i • Matrix.vecCons x ![y] i = 0 ∧
    ∃ i, Matrix.vecCons r₁ ![-r₂] i ≠ 0
[PROOFSTEP]
rw [Fin.sum_univ_two, Fin.exists_fin_two]
[GOAL]
case neg.refine'_1.inl.inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
r₁ r₂ : R
hr₁ : 0 < r₁
left✝ : 0 < r₂
h : r₁ • x = r₂ • y
⊢ Matrix.vecCons r₁ ![-r₂] 0 • Matrix.vecCons x ![y] 0 + Matrix.vecCons r₁ ![-r₂] 1 • Matrix.vecCons x ![y] 1 = 0 ∧
    (Matrix.vecCons r₁ ![-r₂] 0 ≠ 0 ∨ Matrix.vecCons r₁ ![-r₂] 1 ≠ 0)
[PROOFSTEP]
simp [h, hr₁.ne.symm]
[GOAL]
case neg.refine'_1.inr.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hx0 : x = 0
⊢ ∃ g, ∑ i : Fin (Nat.succ (Nat.succ 0)), g i • Matrix.vecCons x ![y] i = 0 ∧ ∃ i, g i ≠ 0
[PROOFSTEP]
exact False.elim (hx hx0)
[GOAL]
case neg.refine'_1.inr.inr.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hy0 : -y = 0
⊢ ∃ g, ∑ i : Fin (Nat.succ (Nat.succ 0)), g i • Matrix.vecCons x ![y] i = 0 ∧ ∃ i, g i ≠ 0
[PROOFSTEP]
exact False.elim (hy (neg_eq_zero.1 hy0))
[GOAL]
case neg.refine'_1.inr.inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
r₁ r₂ : R
hr₁ : 0 < r₁
left✝ : 0 < r₂
h : r₁ • x = r₂ • -y
⊢ ∃ g, ∑ i : Fin (Nat.succ (Nat.succ 0)), g i • Matrix.vecCons x ![y] i = 0 ∧ ∃ i, g i ≠ 0
[PROOFSTEP]
refine' ⟨![r₁, r₂], _⟩
[GOAL]
case neg.refine'_1.inr.inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
r₁ r₂ : R
hr₁ : 0 < r₁
left✝ : 0 < r₂
h : r₁ • x = r₂ • -y
⊢ ∑ i : Fin (Nat.succ (Nat.succ 0)), Matrix.vecCons r₁ ![r₂] i • Matrix.vecCons x ![y] i = 0 ∧
    ∃ i, Matrix.vecCons r₁ ![r₂] i ≠ 0
[PROOFSTEP]
rw [Fin.sum_univ_two, Fin.exists_fin_two]
[GOAL]
case neg.refine'_1.inr.inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
r₁ r₂ : R
hr₁ : 0 < r₁
left✝ : 0 < r₂
h : r₁ • x = r₂ • -y
⊢ Matrix.vecCons r₁ ![r₂] 0 • Matrix.vecCons x ![y] 0 + Matrix.vecCons r₁ ![r₂] 1 • Matrix.vecCons x ![y] 1 = 0 ∧
    (Matrix.vecCons r₁ ![r₂] 0 ≠ 0 ∨ Matrix.vecCons r₁ ![r₂] 1 ≠ 0)
[PROOFSTEP]
simp [h, hr₁.ne.symm]
[GOAL]
case neg.refine'_2
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
h : ∃ g, ∑ i : Fin (Nat.succ (Nat.succ 0)), g i • Matrix.vecCons x ![y] i = 0 ∧ ∃ i, g i ≠ 0
⊢ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
rcases h with ⟨m, hm, hmne⟩
[GOAL]
case neg.refine'_2.intro.intro
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : ∑ i : Fin (Nat.succ (Nat.succ 0)), m i • Matrix.vecCons x ![y] i = 0
hmne : ∃ i, m i ≠ 0
⊢ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
rw [Fin.sum_univ_two, add_eq_zero_iff_eq_neg, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons] at hm
[GOAL]
case neg.refine'_2.intro.intro
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
⊢ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
rcases lt_trichotomy (m 0) 0 with (hm0 | hm0 | hm0)
[GOAL]
case neg.refine'_2.intro.intro.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 < 0
⊢ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
rcases lt_trichotomy (m 1) 0 with (hm1 | hm1 | hm1)
[GOAL]
case neg.refine'_2.intro.intro.inr.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 = 0
⊢ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
rcases lt_trichotomy (m 1) 0 with (hm1 | hm1 | hm1)
[GOAL]
case neg.refine'_2.intro.intro.inr.inr
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
⊢ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
rcases lt_trichotomy (m 1) 0 with (hm1 | hm1 | hm1)
[GOAL]
case neg.refine'_2.intro.intro.inl.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 < 0
hm1 : m 1 < 0
⊢ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
refine' Or.inr (Or.inr (Or.inr ⟨-m 0, -m 1, Left.neg_pos_iff.2 hm0, Left.neg_pos_iff.2 hm1, _⟩))
[GOAL]
case neg.refine'_2.intro.intro.inl.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 < 0
hm1 : m 1 < 0
⊢ -m 0 • x = -m 1 • -y
[PROOFSTEP]
rw [neg_smul_neg, neg_smul, hm, neg_neg]
[GOAL]
case neg.refine'_2.intro.intro.inl.inr.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 < 0
hm1 : m 1 = 0
⊢ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
exfalso
[GOAL]
case neg.refine'_2.intro.intro.inl.inr.inl.h
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 < 0
hm1 : m 1 = 0
⊢ False
[PROOFSTEP]
simp [hm1, hx, hm0.ne] at hm
[GOAL]
case neg.refine'_2.intro.intro.inl.inr.inr
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 < 0
hm1 : 0 < m 1
⊢ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
refine' Or.inl (Or.inr (Or.inr ⟨-m 0, m 1, Left.neg_pos_iff.2 hm0, hm1, _⟩))
[GOAL]
case neg.refine'_2.intro.intro.inl.inr.inr
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 < 0
hm1 : 0 < m 1
⊢ -m 0 • x = m 1 • y
[PROOFSTEP]
rw [neg_smul, hm, neg_neg]
[GOAL]
case neg.refine'_2.intro.intro.inr.inl.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 = 0
hm1 : m 1 < 0
⊢ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
exfalso
[GOAL]
case neg.refine'_2.intro.intro.inr.inl.inl.h
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 = 0
hm1 : m 1 < 0
⊢ False
[PROOFSTEP]
simp [hm0, hy, hm1.ne] at hm
[GOAL]
case neg.refine'_2.intro.intro.inr.inl.inr.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 = 0
hm1 : m 1 = 0
⊢ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
rw [Fin.exists_fin_two] at hmne
[GOAL]
case neg.refine'_2.intro.intro.inr.inl.inr.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : m 0 ≠ 0 ∨ m 1 ≠ 0
hm0 : m 0 = 0
hm1 : m 1 = 0
⊢ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
exact False.elim (not_and_or.2 hmne ⟨hm0, hm1⟩)
[GOAL]
case neg.refine'_2.intro.intro.inr.inl.inr.inr
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 = 0
hm1 : 0 < m 1
⊢ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
exfalso
[GOAL]
case neg.refine'_2.intro.intro.inr.inl.inr.inr.h
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 = 0
hm1 : 0 < m 1
⊢ False
[PROOFSTEP]
simp [hm0, hy, hm1.ne.symm] at hm
[GOAL]
case neg.refine'_2.intro.intro.inr.inr.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
hm1 : m 1 < 0
⊢ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
refine' Or.inl (Or.inr (Or.inr ⟨m 0, -m 1, hm0, Left.neg_pos_iff.2 hm1, _⟩))
[GOAL]
case neg.refine'_2.intro.intro.inr.inr.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
hm1 : m 1 < 0
⊢ m 0 • x = -m 1 • y
[PROOFSTEP]
rwa [neg_smul]
[GOAL]
case neg.refine'_2.intro.intro.inr.inr.inr.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
hm1 : m 1 = 0
⊢ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
exfalso
[GOAL]
case neg.refine'_2.intro.intro.inr.inr.inr.inl.h
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
hm1 : m 1 = 0
⊢ False
[PROOFSTEP]
simp [hm1, hx, hm0.ne.symm] at hm
[GOAL]
case neg.refine'_2.intro.intro.inr.inr.inr.inr
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
hm1 : 0 < m 1
⊢ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
refine' Or.inr (Or.inr (Or.inr ⟨m 0, m 1, hm0, hm1, _⟩))
[GOAL]
case neg.refine'_2.intro.intro.inr.inr.inr.inr
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
hm1 : 0 < m 1
⊢ m 0 • x = m 1 • -y
[PROOFSTEP]
rwa [smul_neg]
[GOAL]
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
⊢ SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]
[PROOFSTEP]
rw [← sameRay_or_sameRay_neg_iff_not_linearIndependent]
[GOAL]
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
⊢ SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : x = 0
⊢ SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
simp [hx]
[GOAL]
case neg
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
⊢ SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
by_cases hy : y = 0
[GOAL]
case pos
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : y = 0
⊢ SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
simp [hx, hy]
[GOAL]
case neg
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
⊢ SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
simp [hx, hy]
[GOAL]
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y v₁ v₂ : M
h✝ : SameRay R x y
hx : x ≠ 0
hy : y ≠ 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • x = r₂ • y
⊢ (r₂⁻¹ * r₁) • x = y
[PROOFSTEP]
rw [mul_smul, h, inv_smul_smul₀ hr₂.ne']
[GOAL]
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y v₁ v₂ : M
h : SameRay R x y
hx : x ≠ 0
⊢ ∃ r, 0 ≤ r ∧ r • x = y
[PROOFSTEP]
obtain rfl | hy := eq_or_ne y 0
[GOAL]
case inl
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x v₁ v₂ : M
hx : x ≠ 0
h : SameRay R x 0
⊢ ∃ r, 0 ≤ r ∧ r • x = 0
[PROOFSTEP]
exact ⟨0, le_rfl, zero_smul _ _⟩
[GOAL]
case inr
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y v₁ v₂ : M
h : SameRay R x y
hx : x ≠ 0
hy : y ≠ 0
⊢ ∃ r, 0 ≤ r ∧ r • x = y
[PROOFSTEP]
exact (h.exists_pos_left hx hy).imp fun _ => And.imp_left le_of_lt
[GOAL]
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y v₁ v₂ : M
h : SameRay R v₁ v₂
⊢ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • (v₁ + v₂) ∧ v₂ = b • (v₁ + v₂)
[PROOFSTEP]
rcases h with (rfl | rfl | ⟨r₁, r₂, h₁, h₂, H⟩)
[GOAL]
case inl
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y v₂ : M
⊢ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ 0 = a • (0 + v₂) ∧ v₂ = b • (0 + v₂)
[PROOFSTEP]
use 0, 1
[GOAL]
case h
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y v₂ : M
⊢ 0 ≤ 0 ∧ 0 ≤ 1 ∧ 0 + 1 = 1 ∧ 0 = 0 • (0 + v₂) ∧ v₂ = 1 • (0 + v₂)
[PROOFSTEP]
simp
[GOAL]
case inr.inl
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y v₁ : M
⊢ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • (v₁ + 0) ∧ 0 = b • (v₁ + 0)
[PROOFSTEP]
use 1, 0
[GOAL]
case h
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y v₁ : M
⊢ 0 ≤ 1 ∧ 0 ≤ 0 ∧ 1 + 0 = 1 ∧ v₁ = 1 • (v₁ + 0) ∧ 0 = 0 • (v₁ + 0)
[PROOFSTEP]
simp
[GOAL]
case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y v₁ v₂ : M
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
⊢ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • (v₁ + v₂) ∧ v₂ = b • (v₁ + v₂)
[PROOFSTEP]
have h₁₂ : 0 < r₁ + r₂ := add_pos h₁ h₂
[GOAL]
case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y v₁ v₂ : M
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
⊢ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • (v₁ + v₂) ∧ v₂ = b • (v₁ + v₂)
[PROOFSTEP]
refine' ⟨r₂ / (r₁ + r₂), r₁ / (r₁ + r₂), div_nonneg h₂.le h₁₂.le, div_nonneg h₁.le h₁₂.le, _, _, _⟩
[GOAL]
case inr.inr.intro.intro.intro.intro.refine'_1
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y v₁ v₂ : M
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
⊢ r₂ / (r₁ + r₂) + r₁ / (r₁ + r₂) = 1
[PROOFSTEP]
rw [← add_div, add_comm, div_self h₁₂.ne']
[GOAL]
case inr.inr.intro.intro.intro.intro.refine'_2
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y v₁ v₂ : M
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
⊢ v₁ = (r₂ / (r₁ + r₂)) • (v₁ + v₂)
[PROOFSTEP]
rw [div_eq_inv_mul, mul_smul, smul_add, ← H, ← add_smul, add_comm r₂, inv_smul_smul₀ h₁₂.ne']
[GOAL]
case inr.inr.intro.intro.intro.intro.refine'_3
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y v₁ v₂ : M
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
⊢ v₂ = (r₁ / (r₁ + r₂)) • (v₁ + v₂)
[PROOFSTEP]
rw [div_eq_inv_mul, mul_smul, smul_add, H, ← add_smul, add_comm r₂, inv_smul_smul₀ h₁₂.ne']
[GOAL]
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ r • x = y) ↔ SameRay R x y
[PROOFSTEP]
refine' ⟨fun h => _, fun h => h.exists_pos_left hx hy⟩
[GOAL]
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
hy : y ≠ 0
h : ∃ r, 0 < r ∧ r • x = y
⊢ SameRay R x y
[PROOFSTEP]
rcases h with ⟨r, hr, rfl⟩
[GOAL]
case intro.intro
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
hx : x ≠ 0
r : R
hr : 0 < r
hy : r • x ≠ 0
⊢ SameRay R x (r • x)
[PROOFSTEP]
exact SameRay.sameRay_pos_smul_right x hr
[GOAL]
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
⊢ (∃ r, 0 < r ∧ r • x = y) ↔ SameRay R x y ∧ y ≠ 0
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
⊢ (∃ r, 0 < r ∧ r • x = y) → SameRay R x y ∧ y ≠ 0
[PROOFSTEP]
rintro ⟨r, hr, rfl⟩
[GOAL]
case mp.intro.intro
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
hx : x ≠ 0
r : R
hr : 0 < r
⊢ SameRay R x (r • x) ∧ r • x ≠ 0
[PROOFSTEP]
simp [hx, hr.le, hr.ne']
[GOAL]
case mpr
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
⊢ SameRay R x y ∧ y ≠ 0 → ∃ r, 0 < r ∧ r • x = y
[PROOFSTEP]
rintro ⟨hxy, hy⟩
[GOAL]
case mpr.intro
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
hxy : SameRay R x y
hy : y ≠ 0
⊢ ∃ r, 0 < r ∧ r • x = y
[PROOFSTEP]
exact (exists_pos_left_iff_sameRay hx hy).2 hxy
[GOAL]
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
⊢ (∃ r, 0 ≤ r ∧ r • x = y) ↔ SameRay R x y
[PROOFSTEP]
refine' ⟨fun h => _, fun h => h.exists_nonneg_left hx⟩
[GOAL]
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
h : ∃ r, 0 ≤ r ∧ r • x = y
⊢ SameRay R x y
[PROOFSTEP]
rcases h with ⟨r, hr, rfl⟩
[GOAL]
case intro.intro
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
hx : x ≠ 0
r : R
hr : 0 ≤ r
⊢ SameRay R x (r • x)
[PROOFSTEP]
exact SameRay.sameRay_nonneg_smul_right x hr
[GOAL]
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ x = r • y) ↔ SameRay R x y
[PROOFSTEP]
rw [SameRay.sameRay_comm]
[GOAL]
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ x = r • y) ↔ SameRay R y x
[PROOFSTEP]
simp_rw [eq_comm (a := x)]
[GOAL]
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ r • y = x) ↔ SameRay R y x
[PROOFSTEP]
exact exists_pos_left_iff_sameRay hy hx
[GOAL]
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ x = r • y) ↔ SameRay R x y ∧ x ≠ 0
[PROOFSTEP]
rw [SameRay.sameRay_comm]
[GOAL]
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ x = r • y) ↔ SameRay R y x ∧ x ≠ 0
[PROOFSTEP]
simp_rw [eq_comm (a := x)]
[GOAL]
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ r • y = x) ↔ SameRay R y x ∧ x ≠ 0
[PROOFSTEP]
exact exists_pos_left_iff_sameRay_and_ne_zero hy
[GOAL]
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ r, 0 ≤ r ∧ x = r • y) ↔ SameRay R x y
[PROOFSTEP]
rw [SameRay.sameRay_comm]
[GOAL]
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ r, 0 ≤ r ∧ x = r • y) ↔ SameRay R y x
[PROOFSTEP]
simp_rw [eq_comm (a := x)]
[GOAL]
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ r, 0 ≤ r ∧ r • y = x) ↔ SameRay R y x
[PROOFSTEP]
exact exists_nonneg_left_iff_sameRay (R := R) hy


[GOAL]
R : Type u_1
M : Type u_2
r : R
x✝ y✝ : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
x y : M
⊢ Setoid.r x y ↔ -(x - y) ∈ p
[PROOFSTEP]
rw [leftRel_apply, sub_eq_add_neg, neg_add, neg_neg]
[GOAL]
R : Type u_1
M : Type u_2
r : R
x✝ y✝ : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
x y : M
⊢ -x + y ∈ toAddSubgroup p ↔ -x + y ∈ p
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ mk x = 0 ↔ x ∈ p
[PROOFSTEP]
simpa using (Quotient.eq' p : mk x = 0 ↔ _)
[GOAL]
R : Type u_1
M : Type u_2
r : R
x✝ y✝ : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
S : Type u_3
inst✝² : SMul S R
inst✝¹ : SMul S M
inst✝ : IsScalarTower S R M
P : Submodule R M
a : S
x y : M
h : Setoid.r x y
⊢ -(fun x x_1 => x • x_1) a x + (fun x x_1 => x • x_1) a y ∈ toAddSubgroup P
[PROOFSTEP]
simpa using Submodule.smul_mem P (a • (1 : R)) (leftRel_apply.mp h)
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ Function.Surjective mk
[PROOFSTEP]
rintro ⟨x⟩
[GOAL]
case mk
R : Type u_1
M : Type u_2
r : R
x✝ y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
b✝ : M ⧸ p
x : M
⊢ ∃ a, mk a = Quot.mk Setoid.r x
[PROOFSTEP]
exact ⟨x, rfl⟩
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
h : p < ⊤
⊢ Nontrivial (M ⧸ p)
[PROOFSTEP]
obtain ⟨x, _, not_mem_s⟩ := SetLike.exists_of_lt h
[GOAL]
case intro.intro
R : Type u_1
M : Type u_2
r : R
x✝ y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
h : p < ⊤
x : M
left✝ : x ∈ ⊤
not_mem_s : ¬x ∈ p
⊢ Nontrivial (M ⧸ p)
[PROOFSTEP]
refine' ⟨⟨mk x, 0, _⟩⟩
[GOAL]
case intro.intro
R : Type u_1
M : Type u_2
r : R
x✝ y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
h : p < ⊤
x : M
left✝ : x ∈ ⊤
not_mem_s : ¬x ∈ p
⊢ mk x ≠ 0
[PROOFSTEP]
simpa using not_mem_s
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ Subsingleton (M ⧸ p) ↔ p = ⊤
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ Subsingleton (M ⧸ p) → p = ⊤
[PROOFSTEP]
rintro h
[GOAL]
case mp
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
h : Subsingleton (M ⧸ p)
⊢ p = ⊤
[PROOFSTEP]
refine' eq_top_iff.mpr fun x _ => _
[GOAL]
case mp
R : Type u_1
M : Type u_2
r : R
x✝¹ y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
h : Subsingleton (M ⧸ p)
x : M
x✝ : x ∈ ⊤
⊢ x ∈ p
[PROOFSTEP]
have : x - 0 ∈ p := (Submodule.Quotient.eq p).mp (Subsingleton.elim _ _)
[GOAL]
case mp
R : Type u_1
M : Type u_2
r : R
x✝¹ y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
h : Subsingleton (M ⧸ p)
x : M
x✝ : x ∈ ⊤
this : x - 0 ∈ p
⊢ x ∈ p
[PROOFSTEP]
rwa [sub_zero] at this
[GOAL]
case mpr
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ p = ⊤ → Subsingleton (M ⧸ p)
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p' : Submodule R M
⊢ Subsingleton (M ⧸ ⊤)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ p = ⊤ → Nonempty (Unique (M ⧸ p))
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p' : Submodule R M
⊢ Nonempty (Unique (M ⧸ ⊤))
[PROOFSTEP]
exact ⟨QuotientTop.unique⟩
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
p p' : Submodule R M
inst✝¹ : Fintype M
S : Submodule R M
inst✝ : DecidablePred fun x => x ∈ S
⊢ Fintype.card M = Fintype.card { x // x ∈ S } * Fintype.card (M ⧸ S)
[PROOFSTEP]
rw [mul_comm, ← Fintype.card_prod]
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
p p' : Submodule R M
inst✝¹ : Fintype M
S : Submodule R M
inst✝ : DecidablePred fun x => x ∈ S
⊢ Fintype.card M = Fintype.card ((M ⧸ S) × { x // x ∈ S })
[PROOFSTEP]
exact Fintype.card_congr AddSubgroup.addGroupEquivQuotientProdAddSubgroup
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
p p' : Submodule R M
M₂ : Type u_3
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
⊢ ∀ (x y : M), Quotient.mk (x + y) = Quotient.mk x + Quotient.mk y
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
p p' : Submodule R M
M₂ : Type u_3
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
⊢ ∀ (r : R) (x : M),
    AddHom.toFun
        { toFun := Quotient.mk,
          map_add' := (_ : ∀ (a a_1 : M), Quotient.mk a + Quotient.mk a_1 = Quotient.mk a + Quotient.mk a_1) }
        (r • x) =
      ↑(RingHom.id R) r •
        AddHom.toFun
          { toFun := Quotient.mk,
            map_add' := (_ : ∀ (a a_1 : M), Quotient.mk a + Quotient.mk a_1 = Quotient.mk a + Quotient.mk a_1) }
          x
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
p p' : Submodule R M
M₂ : Type u_3
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
A : Submodule R M
⊢ Function.Surjective ↑(mkQ A)
[PROOFSTEP]
rintro ⟨x⟩
[GOAL]
case mk
R : Type u_1
M : Type u_2
r : R
x✝ y : M
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
p p' : Submodule R M
M₂ : Type u_3
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
A : Submodule R M
b✝ : M ⧸ A
x : M
⊢ ∃ a, ↑(mkQ A) a = Quot.mk Setoid.r x
[PROOFSTEP]
exact ⟨x, rfl⟩
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
src✝ : M ⧸ toAddSubgroup p →+ M₂ := lift (toAddSubgroup p) (toAddMonoidHom f) h
⊢ ∀ (r : R) (x : M ⧸ p),
    AddHom.toFun
        { toFun := src✝.toFun,
          map_add' :=
            (_ :
              ∀ (x y : M ⧸ toAddSubgroup p),
                ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) }
        (r • x) =
      ↑τ₁₂ r •
        AddHom.toFun
          { toFun := src✝.toFun,
            map_add' :=
              (_ :
                ∀ (x y : M ⧸ toAddSubgroup p),
                  ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) }
          x
[PROOFSTEP]
rintro a ⟨x⟩
[GOAL]
case mk
R : Type u_1
M : Type u_2
r : R
x✝¹ y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
src✝ : M ⧸ toAddSubgroup p →+ M₂ := lift (toAddSubgroup p) (toAddMonoidHom f) h
a : R
x✝ : M ⧸ p
x : M
⊢ AddHom.toFun
      { toFun := src✝.toFun,
        map_add' :=
          (_ :
            ∀ (x y : M ⧸ toAddSubgroup p),
              ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) }
      (a • Quot.mk Setoid.r x) =
    ↑τ₁₂ a •
      AddHom.toFun
        { toFun := src✝.toFun,
          map_add' :=
            (_ :
              ∀ (x y : M ⧸ toAddSubgroup p),
                ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) }
        (Quot.mk Setoid.r x)
[PROOFSTEP]
exact f.map_smulₛₗ a x
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
⊢ comp (liftQ p f h) (mkQ p) = f
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
x✝ : M
⊢ ↑(comp (liftQ p f h) (mkQ p)) x✝ = ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
M : Type u_2
r : R
x✝ y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
x : M
f : M →ₛₗ[τ₁₂] M₂
h : ↑f x = 0
⊢ span R {x} ≤ ker f
[PROOFSTEP]
rw [span_singleton_le_iff_mem, LinearMap.mem_ker, h]
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
⊢ ∀ (x : M ⧸ p), x ∈ range (mkQ p)
[PROOFSTEP]
rintro ⟨x⟩
[GOAL]
case mk
R : Type u_1
M : Type u_2
r : R
x✝¹ y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
x✝ : M ⧸ p
x : M
⊢ Quot.mk Setoid.r x ∈ range (mkQ p)
[PROOFSTEP]
exact ⟨x, rfl⟩
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
⊢ ker (mkQ p) = p
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
x✝ : M
⊢ x✝ ∈ ker (mkQ p) ↔ x✝ ∈ p
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p'✝ : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
p' : Submodule R (M ⧸ p)
⊢ p ≤ comap (mkQ p) p'
[PROOFSTEP]
simpa using (comap_mono bot_le : ker p.mkQ ≤ comap p.mkQ p')
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
⊢ map (mkQ p) p = ⊥
[PROOFSTEP]
rw [eq_bot_iff, map_le_iff_le_comap, comap_bot, ker_mkQ]
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
⊢ comap (mkQ p) (map (mkQ p) p') = p ⊔ p'
[PROOFSTEP]
simp [comap_map_eq, sup_comm]
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
⊢ map (mkQ p) p' = ⊤ ↔ p ⊔ p' = ⊤
[PROOFSTEP]
simp only [LinearMap.map_eq_top_iff p.range_mkQ, sup_comm, ker_mkQ]
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ comap f q
⊢ p ≤ ker (comp (mkQ q) f)
[PROOFSTEP]
simpa [ker_comp] using h
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ comap f q
⊢ comp (mapQ p q f h) (mkQ p) = comp (mkQ q) f
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u_1
M : Type u_2
r : R
x✝ y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ comap f q
x : M
⊢ ↑(comp (mapQ p q f h) (mkQ p)) x = ↑(comp (mkQ q) f) x
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
⊢ p ≤ comap 0 q
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
h : optParam (p ≤ comap 0 q) (_ : p ≤ comap 0 q)
⊢ mapQ p q 0 h = 0
[PROOFSTEP]
ext
[GOAL]
case h.h
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
h : optParam (p ≤ comap 0 q) (_ : p ≤ comap 0 q)
x✝ : M
⊢ ↑(comp (mapQ p q 0 h) (mkQ p)) x✝ = ↑(comp 0 (mkQ p)) x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R₂
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
R₃ : Type u_5
M₃ : Type u_6
inst✝³ : Ring R₃
inst✝² : AddCommGroup M₃
inst✝¹ : Module R₃ M₃
p₂ : Submodule R₂ M₂
p₃ : Submodule R₃ M₃
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
hf : p ≤ comap f p₂
hg : p₂ ≤ comap g p₃
h : optParam (p ≤ comap f (comap g p₃)) (_ : p ≤ comap f (comap g p₃))
⊢ mapQ p p₃ (comp g f) h = comp (mapQ p₂ p₃ g hg) (mapQ p p₂ f hf)
[PROOFSTEP]
ext
[GOAL]
case h.h
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R₂
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
R₃ : Type u_5
M₃ : Type u_6
inst✝³ : Ring R₃
inst✝² : AddCommGroup M₃
inst✝¹ : Module R₃ M₃
p₂ : Submodule R₂ M₂
p₃ : Submodule R₃ M₃
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
hf : p ≤ comap f p₂
hg : p₂ ≤ comap g p₃
h : optParam (p ≤ comap f (comap g p₃)) (_ : p ≤ comap f (comap g p₃))
x✝ : M
⊢ ↑(comp (mapQ p p₃ (comp g f) h) (mkQ p)) x✝ = ↑(comp (comp (mapQ p₂ p₃ g hg) (mapQ p p₂ f hf)) (mkQ p)) x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
⊢ p ≤ comap LinearMap.id p
[PROOFSTEP]
rw [comap_id]
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
h : optParam (p ≤ comap LinearMap.id p) (_ : p ≤ comap LinearMap.id p)
⊢ mapQ p p LinearMap.id h = LinearMap.id
[PROOFSTEP]
ext
[GOAL]
case h.h
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
h : optParam (p ≤ comap LinearMap.id p) (_ : p ≤ comap LinearMap.id p)
x✝ : M
⊢ ↑(comp (mapQ p p LinearMap.id h) (mkQ p)) x✝ = ↑(comp LinearMap.id (mkQ p)) x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
h' : optParam (p ≤ comap (f ^ k) p) (_ : p ≤ comap (f ^ k) p)
⊢ mapQ p p (f ^ k) h' = mapQ p p f h ^ k
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
h'✝ : optParam (p ≤ comap (f ^ k) p) (_ : p ≤ comap (f ^ k) p)
h' : optParam (p ≤ comap (f ^ Nat.zero) p) (_ : p ≤ comap (f ^ Nat.zero) p)
⊢ mapQ p p (f ^ Nat.zero) h' = mapQ p p f h ^ Nat.zero
[PROOFSTEP]
simp [LinearMap.one_eq_id]
[GOAL]
case succ
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₗ[R] M
h : p ≤ comap f p
k✝ : ℕ
h'✝ : optParam (p ≤ comap (f ^ k✝) p) (_ : p ≤ comap (f ^ k✝) p)
k : ℕ
ih : ∀ (h' : optParam (p ≤ comap (f ^ k) p) (_ : p ≤ comap (f ^ k) p)), mapQ p p (f ^ k) h' = mapQ p p f h ^ k
h' : optParam (p ≤ comap (f ^ Nat.succ k) p) (_ : p ≤ comap (f ^ Nat.succ k) p)
⊢ mapQ p p (f ^ Nat.succ k) h' = mapQ p p f h ^ Nat.succ k
[PROOFSTEP]
simp only [LinearMap.iterate_succ]
  -- porting note: why does any of these `optParams` need to be applied? Why didn't `simp` handle
      -- all of this for us?
[GOAL]
case succ
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₗ[R] M
h : p ≤ comap f p
k✝ : ℕ
h'✝ : optParam (p ≤ comap (f ^ k✝) p) (_ : p ≤ comap (f ^ k✝) p)
k : ℕ
ih : ∀ (h' : optParam (p ≤ comap (f ^ k) p) (_ : p ≤ comap (f ^ k) p)), mapQ p p (f ^ k) h' = mapQ p p f h ^ k
h' : optParam (p ≤ comap (f ^ Nat.succ k) p) (_ : p ≤ comap (f ^ Nat.succ k) p)
⊢ mapQ p p (comp (f ^ k) f) (_ : p ≤ comap (comp (f ^ k) f) p) = comp (mapQ p p f h ^ k) (mapQ p p f h)
[PROOFSTEP]
convert
  mapQ_comp p p p f (f ^ k) h (p.le_comap_pow_of_le_comap h k) (h.trans (comap_mono <| p.le_comap_pow_of_le_comap h k))
[GOAL]
case h.e'_3.h.e'_20
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₗ[R] M
h : p ≤ comap f p
k✝ : ℕ
h'✝ : optParam (p ≤ comap (f ^ k✝) p) (_ : p ≤ comap (f ^ k✝) p)
k : ℕ
ih : ∀ (h' : optParam (p ≤ comap (f ^ k) p) (_ : p ≤ comap (f ^ k) p)), mapQ p p (f ^ k) h' = mapQ p p f h ^ k
h' : optParam (p ≤ comap (f ^ Nat.succ k) p) (_ : p ≤ comap (f ^ Nat.succ k) p)
⊢ mapQ p p f h ^ k = mapQ p p (f ^ k) (_ : p ≤ comap (f ^ k) p)
[PROOFSTEP]
exact (ih _).symm
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
⊢ comap (liftQ p f h) q ≤ map (mkQ p) (comap f q)
[PROOFSTEP]
rintro ⟨x⟩ hx
[GOAL]
case mk
R : Type u_1
M : Type u_2
r : R
x✝¹ y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
x✝ : M ⧸ p
x : M
hx : Quot.mk Setoid.r x ∈ comap (liftQ p f h) q
⊢ Quot.mk Setoid.r x ∈ map (mkQ p) (comap f q)
[PROOFSTEP]
exact ⟨_, hx, rfl⟩
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
⊢ map (mkQ p) (comap f q) ≤ comap (liftQ p f h) q
[PROOFSTEP]
rw [map_le_iff_le_comap, ← comap_comp, liftQ_mkQ]
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q✝ : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
q : Submodule R (M ⧸ p)
⊢ map (liftQ p f h) q ≤ map f (comap (mkQ p) q)
[PROOFSTEP]
rintro _ ⟨⟨x⟩, hxq, rfl⟩
[GOAL]
case intro.mk.intro
R : Type u_1
M : Type u_2
r : R
x✝ y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q✝ : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
q : Submodule R (M ⧸ p)
w✝ : M ⧸ p
x : M
hxq : Quot.mk Setoid.r x ∈ ↑q
⊢ ↑(liftQ p f h) (Quot.mk Setoid.r x) ∈ map f (comap (mkQ p) q)
[PROOFSTEP]
exact ⟨x, hxq, rfl⟩
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q✝ : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
q : Submodule R (M ⧸ p)
⊢ map f (comap (mkQ p) q) ≤ map (liftQ p f h) q
[PROOFSTEP]
rintro _ ⟨x, hxq, rfl⟩
[GOAL]
case intro.intro
R : Type u_1
M : Type u_2
r : R
x✝ y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q✝ : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
q : Submodule R (M ⧸ p)
x : M
hxq : x ∈ ↑(comap (mkQ p) q)
⊢ ↑f x ∈ map (liftQ p f h) q
[PROOFSTEP]
exact ⟨Quotient.mk x, hxq, rfl⟩
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
⊢ range (liftQ p f h) = range f
[PROOFSTEP]
simpa only [range_eq_map] using map_liftQ _ _ _ _
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
h' : ker f ≤ p
⊢ ker (liftQ p f h) = ⊥
[PROOFSTEP]
rw [ker_liftQ, le_antisymm h h', mkQ_map_self]
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p'✝ : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
p' : Submodule R (M ⧸ p)
⊢ p' ≤ range (mkQ p)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q✝ : Submodule R₂ M₂
x✝ : { p' // p ≤ p' }
q : Submodule R M
hq : p ≤ q
⊢ ↑((fun p' => { val := comap (mkQ p) p', property := (_ : p ≤ comap (mkQ p) p') })
        ((fun q => map (mkQ p) ↑q) { val := q, property := hq })) =
    ↑{ val := q, property := hq }
[PROOFSTEP]
simpa [comap_map_mkQ p]
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
⊢ span R (↑f ⁻¹' s) = comap f (span R₂ s)
[PROOFSTEP]
suffices (span R₂ s).comap f ≤ span R (f ⁻¹' s) by exact le_antisymm (span_preimage_le f s) this
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
this : comap f (span R₂ s) ≤ span R (↑f ⁻¹' s)
⊢ span R (↑f ⁻¹' s) = comap f (span R₂ s)
[PROOFSTEP]
exact le_antisymm (span_preimage_le f s) this
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
⊢ comap f (span R₂ s) ≤ span R (↑f ⁻¹' s)
[PROOFSTEP]
have hk : ker f ≤ span R (f ⁻¹' s) := by
  let y := Classical.choose h₀
  have hy : y ∈ s := Classical.choose_spec h₀
  rw [ker_le_iff]
  use y, h₁ hy
  rw [← Set.singleton_subset_iff] at hy
  exact Set.Subset.trans subset_span (span_mono (Set.preimage_mono hy))
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
⊢ ker f ≤ span R (↑f ⁻¹' s)
[PROOFSTEP]
let y := Classical.choose h₀
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y✝ : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
y : M₂ := Classical.choose h₀
⊢ ker f ≤ span R (↑f ⁻¹' s)
[PROOFSTEP]
have hy : y ∈ s := Classical.choose_spec h₀
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y✝ : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
y : M₂ := Classical.choose h₀
hy : y ∈ s
⊢ ker f ≤ span R (↑f ⁻¹' s)
[PROOFSTEP]
rw [ker_le_iff]
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y✝ : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
y : M₂ := Classical.choose h₀
hy : y ∈ s
⊢ ∃ y, y ∈ range f ∧ ↑f ⁻¹' {y} ⊆ ↑(span R (↑f ⁻¹' s))
[PROOFSTEP]
use y, h₁ hy
[GOAL]
case right
R : Type u_1
M : Type u_2
r : R
x y✝ : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
y : M₂ := Classical.choose h₀
hy : y ∈ s
⊢ ↑f ⁻¹' {y} ⊆ ↑(span R (↑f ⁻¹' s))
[PROOFSTEP]
rw [← Set.singleton_subset_iff] at hy
[GOAL]
case right
R : Type u_1
M : Type u_2
r : R
x y✝ : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
y : M₂ := Classical.choose h₀
hy : {y} ⊆ s
⊢ ↑f ⁻¹' {y} ⊆ ↑(span R (↑f ⁻¹' s))
[PROOFSTEP]
exact Set.Subset.trans subset_span (span_mono (Set.preimage_mono hy))
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
hk : ker f ≤ span R (↑f ⁻¹' s)
⊢ comap f (span R₂ s) ≤ span R (↑f ⁻¹' s)
[PROOFSTEP]
rw [← left_eq_sup] at hk
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ ↑(range f)
hk : span R (↑f ⁻¹' s) = span R (↑f ⁻¹' s) ⊔ ker f
⊢ comap f (span R₂ s) ≤ span R (↑f ⁻¹' s)
[PROOFSTEP]
rw [range_coe f] at h₁
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ Set.range ↑f
hk : span R (↑f ⁻¹' s) = span R (↑f ⁻¹' s) ⊔ ker f
⊢ comap f (span R₂ s) ≤ span R (↑f ⁻¹' s)
[PROOFSTEP]
rw [hk, ← LinearMap.map_le_map_iff, map_span, map_comap_eq, Set.image_preimage_eq_of_subset h₁]
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : Set.Nonempty s
h₁ : s ⊆ Set.range ↑f
hk : span R (↑f ⁻¹' s) = span R (↑f ⁻¹' s) ⊔ ker f
⊢ range f ⊓ span R₂ s ≤ span R₂ s
[PROOFSTEP]
exact inf_le_right
[GOAL]
R : Type u_1
M : Type u_2
r : R
x✝ y : M
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
Q : Submodule R N
f : M ≃ₗ[R] N
hf : map f P = Q
src✝ : M ⧸ P →ₗ[R] N ⧸ Q := mapQ P Q ↑f (_ : ∀ (x : M), x ∈ P → x ∈ comap (↑f) Q)
x : N
hx : x ∈ Q
⊢ x ∈ comap (↑(LinearEquiv.symm f)) P
[PROOFSTEP]
rw [← hf, Submodule.mem_map] at hx
[GOAL]
R : Type u_1
M : Type u_2
r : R
x✝ y : M
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
Q : Submodule R N
f : M ≃ₗ[R] N
hf : map f P = Q
src✝ : M ⧸ P →ₗ[R] N ⧸ Q := mapQ P Q ↑f (_ : ∀ (x : M), x ∈ P → x ∈ comap (↑f) Q)
x : N
hx : ∃ y, y ∈ P ∧ ↑f y = x
⊢ x ∈ comap (↑(LinearEquiv.symm f)) P
[PROOFSTEP]
obtain ⟨y, hy, rfl⟩ := hx
[GOAL]
case intro.intro
R : Type u_1
M : Type u_2
r : R
x y✝ : M
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
Q : Submodule R N
f : M ≃ₗ[R] N
hf : map f P = Q
src✝ : M ⧸ P →ₗ[R] N ⧸ Q := mapQ P Q ↑f (_ : ∀ (x : M), x ∈ P → x ∈ comap (↑f) Q)
y : M
hy : y ∈ P
⊢ ↑f y ∈ comap (↑(LinearEquiv.symm f)) P
[PROOFSTEP]
simpa
[GOAL]
R : Type u_1
M : Type u_2
r : R
x✝ y : M
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
Q : Submodule R N
f : M ≃ₗ[R] N
hf : map f P = Q
src✝ : M ⧸ P →ₗ[R] N ⧸ Q := mapQ P Q ↑f (_ : ∀ (x : M), x ∈ P → x ∈ comap (↑f) Q)
x : M ⧸ P
⊢ ∀ (a : M),
    ↑(mapQ Q P ↑(LinearEquiv.symm f) (_ : ∀ (x : N), x ∈ Q → x ∈ comap (↑(LinearEquiv.symm f)) P))
        (AddHom.toFun
          {
              toAddHom :=
                { toFun := ↑(mapQ P Q ↑f (_ : ∀ (x : M), x ∈ P → x ∈ comap (↑f) Q)),
                  map_add' :=
                    (_ :
                      ∀ (x y : M ⧸ P),
                        AddHom.toFun src✝.toAddHom (x + y) =
                          AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
              map_smul' :=
                (_ :
                  ∀ (r : R) (x : M ⧸ P),
                    AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
          (Quotient.mk'' a)) =
      Quotient.mk'' a
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
r : R
x✝ y : M
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : Submodule R M
Q : Submodule R N
f : M ≃ₗ[R] N
hf : map f P = Q
src✝ : M ⧸ P →ₗ[R] N ⧸ Q := mapQ P Q ↑f (_ : ∀ (x : M), x ∈ P → x ∈ comap (↑f) Q)
x : N ⧸ Q
⊢ ∀ (a : N),
    AddHom.toFun
        {
            toAddHom :=
              { toFun := ↑(mapQ P Q ↑f (_ : ∀ (x : M), x ∈ P → x ∈ comap (↑f) Q)),
                map_add' :=
                  (_ :
                    ∀ (x y : M ⧸ P),
                      AddHom.toFun src✝.toAddHom (x + y) =
                        AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
            map_smul' :=
              (_ :
                ∀ (r : R) (x : M ⧸ P),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        (↑(mapQ Q P ↑(LinearEquiv.symm f) (_ : ∀ (x : N), x ∈ Q → x ∈ comap (↑(LinearEquiv.symm f)) P))
          (Quotient.mk'' a)) =
      Quotient.mk'' a
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R₂
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
N : Type u_5
O : Type u_6
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup O
inst✝ : Module R O
P : Submodule R M
Q : Submodule R N
S : Submodule R O
e : M ≃ₗ[R] N
f : N ≃ₗ[R] O
he : map e P = Q
hf : map f Q = S
hef : map (LinearEquiv.trans e f) P = S
⊢ equiv P S (LinearEquiv.trans e f) hef = LinearEquiv.trans (equiv P Q e he) (equiv Q S f hf)
[PROOFSTEP]
ext
  -- `simp` can deal with `hef` depending on `e` and `f`
[GOAL]
case h
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R₂
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
N : Type u_5
O : Type u_6
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup O
inst✝ : Module R O
P : Submodule R M
Q : Submodule R N
S : Submodule R O
e : M ≃ₗ[R] N
f : N ≃ₗ[R] O
he : map e P = Q
hf : map f Q = S
hef : map (LinearEquiv.trans e f) P = S
x✝ : M ⧸ P
⊢ ↑(equiv P S (LinearEquiv.trans e f) hef) x✝ = ↑(LinearEquiv.trans (equiv P Q e he) (equiv Q S f hf)) x✝
[PROOFSTEP]
simp only [Quotient.equiv_apply, LinearEquiv.trans_apply, LinearEquiv.coe_trans]
  -- `rw` can deal with `mapQ_comp` needing extra hypotheses coming from the RHS
[GOAL]
case h
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R₂
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
N : Type u_5
O : Type u_6
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup O
inst✝ : Module R O
P : Submodule R M
Q : Submodule R N
S : Submodule R O
e : M ≃ₗ[R] N
f : N ≃ₗ[R] O
he : map e P = Q
hf : map f Q = S
hef : map (LinearEquiv.trans e f) P = S
x✝ : M ⧸ P
⊢ ↑(mapQ P S (comp ↑f ↑e) (_ : P ≤ comap (comp ↑f ↑e) S)) x✝ =
    ↑(mapQ Q S ↑f (_ : ∀ (x : N), x ∈ Q → x ∈ comap (↑f) S))
      (↑(mapQ P Q ↑e (_ : ∀ (x : M), x ∈ P → x ∈ comap (↑e) Q)) x✝)
[PROOFSTEP]
rw [mapQ_comp, LinearMap.comp_apply]
[GOAL]
R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
R₃ : Type u_5
M₃ : Type u_6
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
x : M
⊢ ↑(comp (mkQ (range f)) f) x = ↑0 x
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
R₃ : Type u_5
M₃ : Type u_6
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
⊢ ker g ≤ range f ↔ comp (mkQ (range f)) (Submodule.subtype (ker g)) = 0
[PROOFSTEP]
rw [← range_le_ker_iff, Submodule.ker_mkQ, Submodule.range_subtype]
[GOAL]
R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
R₃ : Type u_5
M₃ : Type u_6
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : M₂ →ₗ[R₂] M₂ ⧸ range f), comp u f = comp v f → u = v
⊢ range f = ⊤
[PROOFSTEP]
have h₁ : (0 : M₂ →ₗ[R₂] M₂ ⧸ (range f)).comp f = 0 := zero_comp _
[GOAL]
R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
R₃ : Type u_5
M₃ : Type u_6
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : M₂ →ₗ[R₂] M₂ ⧸ range f), comp u f = comp v f → u = v
h₁ : comp 0 f = 0
⊢ range f = ⊤
[PROOFSTEP]
rw [← Submodule.ker_mkQ (range f), ← h 0 f.range.mkQ (Eq.trans h₁ (range_mkQ_comp _).symm)]
[GOAL]
R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
R₃ : Type u_5
M₃ : Type u_6
inst✝¹⁰ : Ring R
inst✝⁹ : Ring R₂
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : M₂ →ₗ[R₂] M₂ ⧸ range f), comp u f = comp v f → u = v
h₁ : comp 0 f = 0
⊢ ker 0 = ⊤
[PROOFSTEP]
exact ker_zero
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
h : p = p'
a b : M
⊢ Setoid.r a b ↔ Setoid.r (↑(Equiv.refl M) a) (↑(Equiv.refl M) b)
[PROOFSTEP]
subst h
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
a b : M
⊢ Setoid.r a b ↔ Setoid.r (↑(Equiv.refl M) a) (↑(Equiv.refl M) b)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
h : p = p'
src✝ : Quotient (quotientRel p) ≃ Quotient (quotientRel p') :=
  Quotient.congr (Equiv.refl M) (_ : ∀ (a b : M), Setoid.r a b ↔ Setoid.r (↑(Equiv.refl M) a) (↑(Equiv.refl M) b))
⊢ ∀ (x y : M ⧸ p), Equiv.toFun src✝ (x + y) = Equiv.toFun src✝ x + Equiv.toFun src✝ y
[PROOFSTEP]
rintro ⟨x⟩ ⟨y⟩
[GOAL]
case mk.mk
R : Type u_1
M : Type u_2
r : R
x✝¹ y✝¹ : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
h : p = p'
src✝ : Quotient (quotientRel p) ≃ Quotient (quotientRel p') :=
  Quotient.congr (Equiv.refl M) (_ : ∀ (a b : M), Setoid.r a b ↔ Setoid.r (↑(Equiv.refl M) a) (↑(Equiv.refl M) b))
x✝ : M ⧸ p
x : M
y✝ : M ⧸ p
y : M
⊢ Equiv.toFun src✝ (Quot.mk Setoid.r x + Quot.mk Setoid.r y) =
    Equiv.toFun src✝ (Quot.mk Setoid.r x) + Equiv.toFun src✝ (Quot.mk Setoid.r y)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
h : p = p'
src✝ : Quotient (quotientRel p) ≃ Quotient (quotientRel p') :=
  Quotient.congr (Equiv.refl M) (_ : ∀ (a b : M), Setoid.r a b ↔ Setoid.r (↑(Equiv.refl M) a) (↑(Equiv.refl M) b))
⊢ ∀ (r : R) (x : M ⧸ p),
    AddHom.toFun
        { toFun := src✝.toFun,
          map_add' := (_ : ∀ (x y : M ⧸ p), Equiv.toFun src✝ (x + y) = Equiv.toFun src✝ x + Equiv.toFun src✝ y) }
        (r • x) =
      ↑(RingHom.id R) r •
        AddHom.toFun
          { toFun := src✝.toFun,
            map_add' := (_ : ∀ (x y : M ⧸ p), Equiv.toFun src✝ (x + y) = Equiv.toFun src✝ x + Equiv.toFun src✝ y) }
          x
[PROOFSTEP]
rintro x ⟨y⟩
[GOAL]
case mk
R : Type u_1
M : Type u_2
r : R
x✝¹ y✝ : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
h : p = p'
src✝ : Quotient (quotientRel p) ≃ Quotient (quotientRel p') :=
  Quotient.congr (Equiv.refl M) (_ : ∀ (a b : M), Setoid.r a b ↔ Setoid.r (↑(Equiv.refl M) a) (↑(Equiv.refl M) b))
x : R
x✝ : M ⧸ p
y : M
⊢ AddHom.toFun
      { toFun := src✝.toFun,
        map_add' := (_ : ∀ (x y : M ⧸ p), Equiv.toFun src✝ (x + y) = Equiv.toFun src✝ x + Equiv.toFun src✝ y) }
      (x • Quot.mk Setoid.r y) =
    ↑(RingHom.id R) x •
      AddHom.toFun
        { toFun := src✝.toFun,
          map_add' := (_ : ∀ (x y : M ⧸ p), Equiv.toFun src✝ (x + y) = Equiv.toFun src✝ x + Equiv.toFun src✝ y) }
        (Quot.mk Setoid.r y)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' P Q : Submodule R M
hf : map (↑(LinearEquiv.refl R M)) P = Q
⊢ P = Q
[PROOFSTEP]
simpa using hf
[GOAL]
R : Type u_1
M : Type u_2
M₂ : Type u_3
r : R
x✝ y✝ : M
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
x y : { x // x ∈ compatibleMaps p q }
⊢ (fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) (x + y) =
    (fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) x + (fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) y
[PROOFSTEP]
ext
[GOAL]
case h.h
R : Type u_1
M : Type u_2
M₂ : Type u_3
r : R
x✝¹ y✝ : M
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
x y : { x // x ∈ compatibleMaps p q }
x✝ : M
⊢ ↑(LinearMap.comp ((fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) (x + y)) (mkQ p)) x✝ =
    ↑(LinearMap.comp
          ((fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) x +
            (fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) y)
          (mkQ p))
      x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
M : Type u_2
M₂ : Type u_3
r : R
x y : M
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
c : R
f : { x // x ∈ compatibleMaps p q }
⊢ AddHom.toFun
      { toFun := fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q),
        map_add' :=
          (_ :
            ∀ (x y : { x // x ∈ compatibleMaps p q }),
              (fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) (x + y) =
                (fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) x +
                  (fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) y) }
      (c • f) =
    ↑(RingHom.id R) c •
      AddHom.toFun
        { toFun := fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q),
          map_add' :=
            (_ :
              ∀ (x y : { x // x ∈ compatibleMaps p q }),
                (fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) (x + y) =
                  (fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) x +
                    (fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) y) }
        f
[PROOFSTEP]
ext
[GOAL]
case h.h
R : Type u_1
M : Type u_2
M₂ : Type u_3
r : R
x y : M
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
c : R
f : { x // x ∈ compatibleMaps p q }
x✝ : M
⊢ ↑(LinearMap.comp
          (AddHom.toFun
            { toFun := fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q),
              map_add' :=
                (_ :
                  ∀ (x y : { x // x ∈ compatibleMaps p q }),
                    (fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) (x + y) =
                      (fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) x +
                        (fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) y) }
            (c • f))
          (mkQ p))
      x✝ =
    ↑(LinearMap.comp
          (↑(RingHom.id R) c •
            AddHom.toFun
              { toFun := fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q),
                map_add' :=
                  (_ :
                    ∀ (x y : { x // x ∈ compatibleMaps p q }),
                      (fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) (x + y) =
                        (fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) x +
                          (fun f => mapQ p q ↑f (_ : ↑f ∈ compatibleMaps p q)) y) }
              f)
          (mkQ p))
      x✝
[PROOFSTEP]
rfl