ι : Type ?u.78863
𝕜 : Type u_2
R : Type ?u.78869
M : Type u_1
N : Type ?u.78875
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
ι : Type ?u.78863
𝕜 : Type u_2
R : Type ?u.78869
M : Type u_1
N : Type ?u.78875
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
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
ι : Type ?u.78863
𝕜 : Type u_2
R : Type ?u.78869
M : Type u_1
N : Type ?u.78875
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
ι : Type ?u.78863
𝕜 : Type u_2
R : Type ?u.78869
M : Type u_1
N : Type ?u.78875
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
refine' { smul_lt_smul_of_pos := fun {a b c} => hlt' a b c..}
ι : Type ?u.78863
𝕜 : Type u_2
R : Type ?u.78869
M : Type u_1
N : Type ?u.78875
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
ι : Type ?u.78863
𝕜 : Type u_2
R : Type ?u.78869
M : Type u_1
N : Type ?u.78875
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
intro a b c hab hc
case intro
ι : Type ?u.78863
𝕜 : Type u_2
R : Type ?u.78869
M : Type u_1
N : Type ?u.78875
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
ι : Type ?u.78863
𝕜 : Type u_2
R : Type ?u.78869
M : Type u_1
N : Type ?u.78875
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
obtain ⟨c, rfl⟩ := hc.ne'.isUnit
case intro
ι : Type ?u.78863
𝕜 : Type u_2
R : Type ?u.78869
M : Type u_1
N : Type ?u.78875
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
case intro
ι : Type ?u.78863
𝕜 : Type u_2
R : Type ?u.78869
M : Type u_1
N : Type ?u.78875
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
rw [← inv_smul_smul c a, ← inv_smul_smul c b]
case intro
ι : Type ?u.78863
𝕜 : Type u_2
R : Type ?u.78869
M : Type u_1
N : Type ?u.78875
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⁻¹
case intro
ι : Type ?u.78863
𝕜 : Type u_2
R : Type ?u.78869
M : Type u_1
N : Type ?u.78875
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
refine' hlt' _ _ _ hab (pos_of_mul_pos_right _ hc.le)
no goals
case intro
ι : Type ?u.78863
𝕜 : Type u_2
R : Type ?u.78869
M : Type u_1
N : Type ?u.78875
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⁻¹
simp only [c.mul_inv, zero_lt_one]
ι : Type ?u.78863
𝕜 : Type u_2
R : Type ?u.78869
M : Type u_1
N : Type ?u.78875
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
ι : Type ?u.78863
𝕜 : Type u_2
R : Type ?u.78869
M : Type u_1
N : Type ?u.78875
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
refine' fun a b c hab hc => (h hab hc).lt_of_ne _
ι : Type ?u.78863
𝕜 : Type u_2
R : Type ?u.78869
M : Type u_1
N : Type ?u.78875
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
ι : Type ?u.78863
𝕜 : Type u_2
R : Type ?u.78869
M : Type u_1
N : Type ?u.78875
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
rw [Ne.def, hc.ne'.isUnit.smul_left_cancel]
no goals
ι : Type ?u.78863
𝕜 : Type u_2
R : Type ?u.78869
M : Type u_1
N : Type ?u.78875
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
exact hab.ne