[GOAL]
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : OrderedSemiring R
inst✝² : OrderedAddCommMonoid M
inst✝¹ : SMulWithZero R M
inst✝ : OrderedSMul R M
s : Set M
a b : M
c : R
h₁ : a ≤ b
h₂ : 0 ≤ c
⊢ c • a ≤ c • b
[PROOFSTEP]
rcases h₁.eq_or_lt with (rfl | hab)
[GOAL]
case inl
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : OrderedSemiring R
inst✝² : OrderedAddCommMonoid M
inst✝¹ : SMulWithZero R M
inst✝ : OrderedSMul R M
s : Set M
a : M
c : R
h₂ : 0 ≤ c
h₁ : a ≤ a
⊢ c • a ≤ c • a
[PROOFSTEP]
rfl
[GOAL]
case inr
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : OrderedSemiring R
inst✝² : OrderedAddCommMonoid M
inst✝¹ : SMulWithZero R M
inst✝ : OrderedSMul R M
s : Set M
a b : M
c : R
h₁ : a ≤ b
h₂ : 0 ≤ c
hab : a < b
⊢ c • a ≤ c • b
[PROOFSTEP]
rcases h₂.eq_or_lt with (rfl | hc)
[GOAL]
case inr.inl
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : OrderedSemiring R
inst✝² : OrderedAddCommMonoid M
inst✝¹ : SMulWithZero R M
inst✝ : OrderedSMul R M
s : Set M
a b : M
h₁ : a ≤ b
hab : a < b
h₂ : 0 ≤ 0
⊢ 0 • a ≤ 0 • b
[PROOFSTEP]
rw [zero_smul, zero_smul]
[GOAL]
case inr.inr
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : OrderedSemiring R
inst✝² : OrderedAddCommMonoid M
inst✝¹ : SMulWithZero R M
inst✝ : OrderedSMul R M
s : Set M
a b : M
c : R
h₁ : a ≤ b
h₂ : 0 ≤ c
hab : a < b
hc : 0 < c
⊢ c • a ≤ c • b
[PROOFSTEP]
exact (smul_lt_smul_of_pos hab hc).le
[GOAL]
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : OrderedSemiring R
inst✝² : OrderedAddCommMonoid M
inst✝¹ : SMulWithZero R M
inst✝ : OrderedSMul R M
s : Set M
a b : M
c : R
h : c • a < c • b
hc✝ : 0 ≤ c
hc : 0 = c
⊢ 0 < 0
[PROOFSTEP]
rwa [← hc, zero_smul, zero_smul] at h 
[GOAL]
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : OrderedSemiring R
inst✝² : OrderedAddCommMonoid M
inst✝¹ : SMulWithZero R M
inst✝ : OrderedSMul R M
s : Set M
a b : M
c : R
hc : 0 < c
⊢ 0 < c • a ↔ c • 0 < c • a
[PROOFSTEP]
rw [smul_zero]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝ : LinearOrderedCancelAddCommMonoid M
n : ℕ
hn : 0 < n
a b : M
hab : a < b
⊢ (fun a => n • a) a < (fun a => n • a) b
[PROOFSTEP]
cases n with
| zero => cases hn
| succ n =>
  induction n with
  | zero => dsimp; rwa [one_nsmul, one_nsmul]
  | succ n ih => simp only [succ_nsmul _ n.succ, _root_.add_lt_add hab (ih n.succ_pos)]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝ : LinearOrderedCancelAddCommMonoid M
n : ℕ
hn : 0 < n
a b : M
hab : a < b
⊢ (fun a => n • a) a < (fun a => n • a) b
[PROOFSTEP]
cases n with
| zero => cases hn
| succ n =>
  induction n with
  | zero => dsimp; rwa [one_nsmul, one_nsmul]
  | succ n ih => simp only [succ_nsmul _ n.succ, _root_.add_lt_add hab (ih n.succ_pos)]
[GOAL]
case zero
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝ : LinearOrderedCancelAddCommMonoid M
a b : M
hab : a < b
hn : 0 < zero
⊢ (fun a => zero • a) a < (fun a => zero • a) b
[PROOFSTEP]

| zero => cases hn
[GOAL]
case zero
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝ : LinearOrderedCancelAddCommMonoid M
a b : M
hab : a < b
hn : 0 < zero
⊢ (fun a => zero • a) a < (fun a => zero • a) b
[PROOFSTEP]
cases hn
[GOAL]
case succ
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝ : LinearOrderedCancelAddCommMonoid M
a b : M
hab : a < b
n : ℕ
hn : 0 < succ n
⊢ (fun a => succ n • a) a < (fun a => succ n • a) b
[PROOFSTEP]

| succ n =>
  induction n with
  | zero => dsimp; rwa [one_nsmul, one_nsmul]
  | succ n ih => simp only [succ_nsmul _ n.succ, _root_.add_lt_add hab (ih n.succ_pos)]
[GOAL]
case succ
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝ : LinearOrderedCancelAddCommMonoid M
a b : M
hab : a < b
n : ℕ
hn : 0 < succ n
⊢ (fun a => succ n • a) a < (fun a => succ n • a) b
[PROOFSTEP]
induction n with
| zero => dsimp; rwa [one_nsmul, one_nsmul]
| succ n ih => simp only [succ_nsmul _ n.succ, _root_.add_lt_add hab (ih n.succ_pos)]
[GOAL]
case succ
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝ : LinearOrderedCancelAddCommMonoid M
a b : M
hab : a < b
n : ℕ
hn : 0 < succ n
⊢ (fun a => succ n • a) a < (fun a => succ n • a) b
[PROOFSTEP]
induction n with
| zero => dsimp; rwa [one_nsmul, one_nsmul]
| succ n ih => simp only [succ_nsmul _ n.succ, _root_.add_lt_add hab (ih n.succ_pos)]
[GOAL]
case succ.zero
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝ : LinearOrderedCancelAddCommMonoid M
a b : M
hab : a < b
hn : 0 < succ zero
⊢ (fun a => succ zero • a) a < (fun a => succ zero • a) b
[PROOFSTEP]

| zero => dsimp; rwa [one_nsmul, one_nsmul]
[GOAL]
case succ.zero
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝ : LinearOrderedCancelAddCommMonoid M
a b : M
hab : a < b
hn : 0 < succ zero
⊢ (fun a => succ zero • a) a < (fun a => succ zero • a) b
[PROOFSTEP]
dsimp
[GOAL]
case succ.zero
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝ : LinearOrderedCancelAddCommMonoid M
a b : M
hab : a < b
hn : 0 < succ zero
⊢ succ 0 • a < succ 0 • b
[PROOFSTEP]
rwa [one_nsmul, one_nsmul]
[GOAL]
case succ.succ
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝ : LinearOrderedCancelAddCommMonoid M
a b : M
hab : a < b
n : ℕ
ih : 0 < succ n → (fun a => succ n • a) a < (fun a => succ n • a) b
hn : 0 < succ (succ n)
⊢ (fun a => succ (succ n) • a) a < (fun a => succ (succ n) • a) b
[PROOFSTEP]

| succ n ih => simp only [succ_nsmul _ n.succ, _root_.add_lt_add hab (ih n.succ_pos)]
[GOAL]
case succ.succ
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝ : LinearOrderedCancelAddCommMonoid M
a b : M
hab : a < b
n : ℕ
ih : 0 < succ n → (fun a => succ n • a) a < (fun a => succ n • a) b
hn : 0 < succ (succ n)
⊢ (fun a => succ (succ n) • a) a < (fun a => succ (succ n) • a) b
[PROOFSTEP]
simp only [succ_nsmul _ n.succ, _root_.add_lt_add hab (ih n.succ_pos)]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝ : LinearOrderedAddCommGroup M
n : ℤ
hn : 0 < n
⊢ StrictMono fun a => n • a
[PROOFSTEP]
cases n
[GOAL]
case ofNat
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝ : LinearOrderedAddCommGroup M
a✝ : ℕ
hn : 0 < ofNat a✝
⊢ StrictMono fun a => ofNat a✝ • a
[PROOFSTEP]
simp only [Int.ofNat_eq_coe, Int.coe_nat_pos, coe_nat_zsmul] at hn ⊢
[GOAL]
case ofNat
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝ : LinearOrderedAddCommGroup M
a✝ : ℕ
hn : 0 < a✝
⊢ StrictMono fun a => a✝ • a
[PROOFSTEP]
exact strictMono_smul_left hn
[GOAL]
case negSucc
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝ : LinearOrderedAddCommGroup M
a✝ : ℕ
hn : 0 < -[a✝+1]
⊢ StrictMono fun a => -[a✝+1] • a
[PROOFSTEP]
cases (Int.negSucc_not_pos _).1 hn
[GOAL]
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : LinearOrderedSemifield 𝕜
inst✝³ : OrderedAddCommMonoid M
inst✝² : OrderedAddCommMonoid N
inst✝¹ : MulActionWithZero 𝕜 M
inst✝ : MulActionWithZero 𝕜 N
h : ∀ ⦃a b : M⦄ ⦃c : 𝕜⦄, a < b → 0 < c → c • a ≤ c • b
⊢ OrderedSMul 𝕜 M
[PROOFSTEP]
have hlt' : ∀ (a b : M) (c : 𝕜), a < b → 0 < c → c • a < c • b :=
  by
  refine' fun a b c hab hc => (h hab hc).lt_of_ne _
  rw [Ne.def, hc.ne'.isUnit.smul_left_cancel]
  exact hab.ne
[GOAL]
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : LinearOrderedSemifield 𝕜
inst✝³ : OrderedAddCommMonoid M
inst✝² : OrderedAddCommMonoid N
inst✝¹ : MulActionWithZero 𝕜 M
inst✝ : MulActionWithZero 𝕜 N
h : ∀ ⦃a b : M⦄ ⦃c : 𝕜⦄, a < b → 0 < c → c • a ≤ c • b
⊢ ∀ (a b : M) (c : 𝕜), a < b → 0 < c → c • a < c • b
[PROOFSTEP]
refine' fun a b c hab hc => (h hab hc).lt_of_ne _
[GOAL]
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : LinearOrderedSemifield 𝕜
inst✝³ : OrderedAddCommMonoid M
inst✝² : OrderedAddCommMonoid N
inst✝¹ : MulActionWithZero 𝕜 M
inst✝ : MulActionWithZero 𝕜 N
h : ∀ ⦃a b : M⦄ ⦃c : 𝕜⦄, a < b → 0 < c → c • a ≤ c • b
a b : M
c : 𝕜
hab : a < b
hc : 0 < c
⊢ c • a ≠ c • b
[PROOFSTEP]
rw [Ne.def, hc.ne'.isUnit.smul_left_cancel]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : LinearOrderedSemifield 𝕜
inst✝³ : OrderedAddCommMonoid M
inst✝² : OrderedAddCommMonoid N
inst✝¹ : MulActionWithZero 𝕜 M
inst✝ : MulActionWithZero 𝕜 N
h : ∀ ⦃a b : M⦄ ⦃c : 𝕜⦄, a < b → 0 < c → c • a ≤ c • b
a b : M
c : 𝕜
hab : a < b
hc : 0 < c
⊢ ¬a = b
[PROOFSTEP]
exact hab.ne
[GOAL]
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : LinearOrderedSemifield 𝕜
inst✝³ : OrderedAddCommMonoid M
inst✝² : OrderedAddCommMonoid N
inst✝¹ : MulActionWithZero 𝕜 M
inst✝ : MulActionWithZero 𝕜 N
h : ∀ ⦃a b : M⦄ ⦃c : 𝕜⦄, a < b → 0 < c → c • a ≤ c • b
hlt' : ∀ (a b : M) (c : 𝕜), a < b → 0 < c → c • a < c • b
⊢ OrderedSMul 𝕜 M
[PROOFSTEP]
refine' { smul_lt_smul_of_pos := fun {a b c} => hlt' a b c .. }
[GOAL]
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : LinearOrderedSemifield 𝕜
inst✝³ : OrderedAddCommMonoid M
inst✝² : OrderedAddCommMonoid N
inst✝¹ : MulActionWithZero 𝕜 M
inst✝ : MulActionWithZero 𝕜 N
h : ∀ ⦃a b : M⦄ ⦃c : 𝕜⦄, a < b → 0 < c → c • a ≤ c • b
hlt' : ∀ (a b : M) (c : 𝕜), a < b → 0 < c → c • a < c • b
⊢ ∀ {a b : M} {c : 𝕜}, c • a < c • b → 0 < c → a < b
[PROOFSTEP]
intro a b c hab hc
[GOAL]
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : LinearOrderedSemifield 𝕜
inst✝³ : OrderedAddCommMonoid M
inst✝² : OrderedAddCommMonoid N
inst✝¹ : MulActionWithZero 𝕜 M
inst✝ : MulActionWithZero 𝕜 N
h : ∀ ⦃a b : M⦄ ⦃c : 𝕜⦄, a < b → 0 < c → c • a ≤ c • b
hlt' : ∀ (a b : M) (c : 𝕜), a < b → 0 < c → c • a < c • b
a b : M
c : 𝕜
hab : c • a < c • b
hc : 0 < c
⊢ a < b
[PROOFSTEP]
obtain ⟨c, rfl⟩ := hc.ne'.isUnit
[GOAL]
case intro
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : LinearOrderedSemifield 𝕜
inst✝³ : OrderedAddCommMonoid M
inst✝² : OrderedAddCommMonoid N
inst✝¹ : MulActionWithZero 𝕜 M
inst✝ : MulActionWithZero 𝕜 N
h : ∀ ⦃a b : M⦄ ⦃c : 𝕜⦄, a < b → 0 < c → c • a ≤ c • b
hlt' : ∀ (a b : M) (c : 𝕜), a < b → 0 < c → c • a < c • b
a b : M
c : 𝕜ˣ
hab : ↑c • a < ↑c • b
hc : 0 < ↑c
⊢ a < b
[PROOFSTEP]
rw [← inv_smul_smul c a, ← inv_smul_smul c b]
[GOAL]
case intro
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : LinearOrderedSemifield 𝕜
inst✝³ : OrderedAddCommMonoid M
inst✝² : OrderedAddCommMonoid N
inst✝¹ : MulActionWithZero 𝕜 M
inst✝ : MulActionWithZero 𝕜 N
h : ∀ ⦃a b : M⦄ ⦃c : 𝕜⦄, a < b → 0 < c → c • a ≤ c • b
hlt' : ∀ (a b : M) (c : 𝕜), a < b → 0 < c → c • a < c • b
a b : M
c : 𝕜ˣ
hab : ↑c • a < ↑c • b
hc : 0 < ↑c
⊢ c⁻¹ • c • a < c⁻¹ • c • b
[PROOFSTEP]
refine' hlt' _ _ _ hab (pos_of_mul_pos_right _ hc.le)
[GOAL]
case intro
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : LinearOrderedSemifield 𝕜
inst✝³ : OrderedAddCommMonoid M
inst✝² : OrderedAddCommMonoid N
inst✝¹ : MulActionWithZero 𝕜 M
inst✝ : MulActionWithZero 𝕜 N
h : ∀ ⦃a b : M⦄ ⦃c : 𝕜⦄, a < b → 0 < c → c • a ≤ c • b
hlt' : ∀ (a b : M) (c : 𝕜), a < b → 0 < c → c • a < c • b
a b : M
c : 𝕜ˣ
hab : ↑c • a < ↑c • b
hc : 0 < ↑c
⊢ 0 < ↑c * ↑c⁻¹
[PROOFSTEP]
simp only [c.mul_inv, zero_lt_one]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : LinearOrderedSemifield 𝕜
inst✝⁴ : OrderedAddCommMonoid M
inst✝³ : OrderedAddCommMonoid N
inst✝² : MulActionWithZero 𝕜 M
inst✝¹ : MulActionWithZero 𝕜 N
inst✝ : OrderedSMul 𝕜 M
s : Set M
a b : M
c : 𝕜
h : 0 < c
⊢ c⁻¹ • a ≤ b ↔ a ≤ c • b
[PROOFSTEP]
rw [← smul_le_smul_iff_of_pos h, smul_inv_smul₀ h.ne']
[GOAL]
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : LinearOrderedSemifield 𝕜
inst✝⁴ : OrderedAddCommMonoid M
inst✝³ : OrderedAddCommMonoid N
inst✝² : MulActionWithZero 𝕜 M
inst✝¹ : MulActionWithZero 𝕜 N
inst✝ : OrderedSMul 𝕜 M
s : Set M
a b : M
c : 𝕜
h : 0 < c
⊢ c⁻¹ • a < b ↔ a < c • b
[PROOFSTEP]
rw [← smul_lt_smul_iff_of_pos h, smul_inv_smul₀ h.ne']
[GOAL]
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : LinearOrderedSemifield 𝕜
inst✝⁴ : OrderedAddCommMonoid M
inst✝³ : OrderedAddCommMonoid N
inst✝² : MulActionWithZero 𝕜 M
inst✝¹ : MulActionWithZero 𝕜 N
inst✝ : OrderedSMul 𝕜 M
s : Set M
a b : M
c : 𝕜
h : 0 < c
⊢ a ≤ c⁻¹ • b ↔ c • a ≤ b
[PROOFSTEP]
rw [← smul_le_smul_iff_of_pos h, smul_inv_smul₀ h.ne']
[GOAL]
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : LinearOrderedSemifield 𝕜
inst✝⁴ : OrderedAddCommMonoid M
inst✝³ : OrderedAddCommMonoid N
inst✝² : MulActionWithZero 𝕜 M
inst✝¹ : MulActionWithZero 𝕜 N
inst✝ : OrderedSMul 𝕜 M
s : Set M
a b : M
c : 𝕜
h : 0 < c
⊢ a < c⁻¹ • b ↔ c • a < b
[PROOFSTEP]
rw [← smul_lt_smul_iff_of_pos h, smul_inv_smul₀ h.ne']
