-- Mathlib/Algebra/Order/Module/OrderedSMul.lean
theorem OrderedSMul.mk' (h : ∀ ⦃a b : M⦄ ⦃c : 𝕜⦄, a < b → 0 < c → c • a ≤ c • b) :
    OrderedSMul 𝕜 M

Proof state:
𝕜 : Type u_2
M : Type u_4
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : OrderedAddCommMonoid M
inst✝ : MulActionWithZero 𝕜 M
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

Tactic:
exact hab.ne

Result:
no goals

Proof state:
case intro
𝕜 : Type u_2
M : Type u_4
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : OrderedAddCommMonoid M
inst✝ : MulActionWithZero 𝕜 M
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

Tactic:
refine hlt' _ _ _ hab (pos_of_mul_pos_right ?_ hc.le)

Result:
case intro
𝕜 : Type u_2
M : Type u_4
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : OrderedAddCommMonoid M
inst✝ : MulActionWithZero 𝕜 M
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⁻¹

Proof state:
𝕜 : Type u_2
M : Type u_4
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : OrderedAddCommMonoid M
inst✝ : MulActionWithZero 𝕜 M
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

Tactic:
obtain ⟨c, rfl⟩ := hc.ne'.isUnit

Result:
case intro
𝕜 : Type u_2
M : Type u_4
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : OrderedAddCommMonoid M
inst✝ : MulActionWithZero 𝕜 M
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

Proof state:
𝕜 : Type u_2
M : Type u_4
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : OrderedAddCommMonoid M
inst✝ : MulActionWithZero 𝕜 M
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

Tactic:
refine fun a b c hab hc => (h hab hc).lt_of_ne ?_

Result:
𝕜 : Type u_2
M : Type u_4
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : OrderedAddCommMonoid M
inst✝ : MulActionWithZero 𝕜 M
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

Proof state:
𝕜 : Type u_2
M : Type u_4
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : OrderedAddCommMonoid M
inst✝ : MulActionWithZero 𝕜 M
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

Tactic:
refine ⟨fun {a b c} => hlt' a b c, fun {a b c hab hc} => ?_⟩

Result:
𝕜 : Type u_2
M : Type u_4
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : OrderedAddCommMonoid M
inst✝ : MulActionWithZero 𝕜 M
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

Proof state:
case intro
𝕜 : Type u_2
M : Type u_4
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : OrderedAddCommMonoid M
inst✝ : MulActionWithZero 𝕜 M
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⁻¹

Tactic:
simp only [c.mul_inv, zero_lt_one]

Result:
no goals

Proof state:
case intro
𝕜 : Type u_2
M : Type u_4
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : OrderedAddCommMonoid M
inst✝ : MulActionWithZero 𝕜 M
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

Tactic:
rw [← inv_smul_smul c a, ← inv_smul_smul c b]

Result:
case intro
𝕜 : Type u_2
M : Type u_4
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : OrderedAddCommMonoid M
inst✝ : MulActionWithZero 𝕜 M
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

Proof state:
𝕜 : Type u_2
M : Type u_4
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : OrderedAddCommMonoid M
inst✝ : MulActionWithZero 𝕜 M
h : ∀ ⦃a b : M⦄ ⦃c : 𝕜⦄, a < b → 0 < c → c • a ≤ c • b
⊢ OrderedSMul 𝕜 M

Tactic:
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, hc.ne'.isUnit.smul_left_cancel]
  exact hab.ne

Result:
𝕜 : Type u_2
M : Type u_4
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : OrderedAddCommMonoid M
inst✝ : MulActionWithZero 𝕜 M
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

Proof state:
𝕜 : Type u_2
M : Type u_4
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : OrderedAddCommMonoid M
inst✝ : MulActionWithZero 𝕜 M
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

Tactic:
rw [Ne, hc.ne'.isUnit.smul_left_cancel]

Result:
𝕜 : Type u_2
M : Type u_4
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : OrderedAddCommMonoid M
inst✝ : MulActionWithZero 𝕜 M
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