[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']


[GOAL]
α : Type u
β : Type v
inst✝¹ : Lattice α
inst✝ : Group α
⊢ 1⁻ = 1
[PROOFSTEP]
rw [m_neg_part_def, inv_one, sup_idem]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ a⁻ = (a ⊓ 1)⁻¹
[PROOFSTEP]
rw [m_neg_part_def, ← inv_inj, inv_sup_eq_inv_inf_inv, inv_inv, inv_inv, inv_one]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Lattice α
inst✝ : Group α
a : α
⊢ a⁻¹ ⊔ a⁻¹⁻¹ = a ⊔ a⁻¹
[PROOFSTEP]
rw [inv_inv, sup_comm]
  -- 0 ≤ a⁺
[GOAL]
α : Type u
β : Type v
inst✝¹ : Lattice α
inst✝ : Group α
a : α
⊢ a⁺ ≤ 1 ↔ a ≤ 1
[PROOFSTEP]
rw [m_pos_part_def, sup_le_iff, and_iff_left le_rfl]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Lattice α
inst✝ : Group α
a : α
⊢ a⁻ ≤ 1 ↔ a⁻¹ ≤ 1
[PROOFSTEP]
rw [m_neg_part_def, sup_le_iff, and_iff_left le_rfl]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : CovariantClass α α Mul.mul LE.le
a : α
⊢ a⁻ = 1 ↔ 1 ≤ a
[PROOFSTEP]
rw [le_antisymm_iff, neg_le_one_iff, inv_le_one', and_iff_left (one_le_neg _)]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Lattice α
inst✝ : Group α
a : α
⊢ a⁺ = a⁻¹⁻
[PROOFSTEP]
rw [neg_eq_pos_inv, inv_inv]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ c * (a ⊓ b) = c * a ⊓ c * b
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ c * (a ⊓ b) ≤ c * a ⊓ c * b
case refine'_2
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ c * a ⊓ c * b ≤ c * (a ⊓ b)
[PROOFSTEP]
rw [le_inf_iff, mul_le_mul_iff_left, mul_le_mul_iff_left]
[GOAL]
case refine'_1
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ a ⊓ b ≤ a ∧ a ⊓ b ≤ b
case refine'_2
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ c * a ⊓ c * b ≤ c * (a ⊓ b)
[PROOFSTEP]
simp
[GOAL]
case refine'_2
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ c * a ⊓ c * b ≤ c * (a ⊓ b)
[PROOFSTEP]
rw [← mul_le_mul_iff_left c⁻¹, ← mul_assoc, inv_mul_self, one_mul, le_inf_iff, inv_mul_le_iff_le_mul,
  inv_mul_le_iff_le_mul]
[GOAL]
case refine'_2
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ c * a ⊓ c * b ≤ c * a ∧ c * a ⊓ c * b ≤ c * b
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ a⁺ / a⁻ = a
[PROOFSTEP]
symm
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ a = a⁺ / a⁻
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ a = a⁺ * a⁻⁻¹
[PROOFSTEP]
apply eq_mul_inv_of_mul_eq
[GOAL]
case h
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ a * a⁻ = a⁺
[PROOFSTEP]
rw [m_neg_part_def, mul_sup, mul_one, mul_right_inv, sup_comm, m_pos_part_def]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Lattice α
inst✝ : Group α
a : α
h : 1 ≤ a
⊢ a⁺ = a
[PROOFSTEP]
rw [m_pos_part_def]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Lattice α
inst✝ : Group α
a : α
h : 1 ≤ a
⊢ a ⊔ 1 = a
[PROOFSTEP]
exact sup_of_le_left h
[GOAL]
α : Type u
β : Type v
inst✝¹ : Lattice α
inst✝ : Group α
a : α
h : 1 ≤ a⁻¹
⊢ a⁻ = a⁻¹
[PROOFSTEP]
rw [neg_eq_pos_inv]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Lattice α
inst✝ : Group α
a : α
h : 1 ≤ a⁻¹
⊢ a⁻¹⁺ = a⁻¹
[PROOFSTEP]
exact pos_of_one_le _ h
[GOAL]
α✝ : Type u
β : Type v
inst✝³ : Lattice α✝
inst✝² : Group α✝
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : CommGroup α
x : α
hx : 1 < x⁺
⊢ x⁺ = x
[PROOFSTEP]
rw [m_pos_part_def, right_lt_sup, not_le] at hx
[GOAL]
α✝ : Type u
β : Type v
inst✝³ : Lattice α✝
inst✝² : Group α✝
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : CommGroup α
x : α
hx : 1 < x
⊢ x⁺ = x
[PROOFSTEP]
rw [m_pos_part_def, sup_eq_left]
[GOAL]
α✝ : Type u
β : Type v
inst✝³ : Lattice α✝
inst✝² : Group α✝
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : CommGroup α
x : α
hx : 1 < x
⊢ 1 ≤ x
[PROOFSTEP]
exact hx.le
[GOAL]
α : Type u
β : Type v
inst✝¹ : Lattice α
inst✝ : Group α
a b : α
⊢ |a / b| = |b / a|
[PROOFSTEP]
dsimp only [Abs.abs]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Lattice α
inst✝ : Group α
a b : α
⊢ a / b ⊔ (a / b)⁻¹ = b / a ⊔ (b / a)⁻¹
[PROOFSTEP]
rw [inv_div a b, ← inv_inv (a / b), inv_div, sup_comm]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ 1 ≤ a ^ 2 → 1 ≤ a
[PROOFSTEP]
intro h
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
h : 1 ≤ a ^ 2
⊢ 1 ≤ a
[PROOFSTEP]
have e1 : (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1 := by
  rw [mul_inf, inf_mul, ← pow_two, mul_one, one_mul, inf_assoc, inf_left_idem, inf_comm, inf_assoc, (inf_of_le_left h)]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
h : 1 ≤ a ^ 2
⊢ (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1
[PROOFSTEP]
rw [mul_inf, inf_mul, ← pow_two, mul_one, one_mul, inf_assoc, inf_left_idem, inf_comm, inf_assoc, (inf_of_le_left h)]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
h : 1 ≤ a ^ 2
e1 : (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1
⊢ 1 ≤ a
[PROOFSTEP]
rw [← inf_eq_right]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
h : 1 ≤ a ^ 2
e1 : (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1
⊢ a ⊓ 1 = 1
[PROOFSTEP]
exact mul_right_eq_self.mp e1
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ 1 ≤ |a|
[PROOFSTEP]
apply pow_two_semiclosed _ _
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ 1 ≤ |a| ^ 2
[PROOFSTEP]
rw [abs_eq_sup_inv, pow_two, mul_sup, sup_mul, ← pow_two, mul_left_inv, sup_comm, ← sup_assoc]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ 1 ≤ (a ⊔ a⁻¹) * a⁻¹ ⊔ a ^ 2 ⊔ 1
[PROOFSTEP]
apply le_sup_right
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ |a| = a⁺ * a⁻
[PROOFSTEP]
rw [m_pos_part_def, sup_mul, one_mul, m_neg_part_def, mul_sup, mul_one, mul_inv_self, sup_assoc, ← @sup_assoc _ _ a,
  sup_eq_right.2 le_sup_right]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ |a| = a ⊔ a⁻¹ ⊔ 1
[PROOFSTEP]
exact (sup_eq_left.2 <| one_le_abs a).symm
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ |a|⁺ = |a|
[PROOFSTEP]
rw [m_pos_part_def]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ |a| ⊔ 1 = |a|
[PROOFSTEP]
apply sup_of_le_left
[GOAL]
case a
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ 1 ≤ |a|
[PROOFSTEP]
apply one_le_abs
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ |a|⁻ = 1
[PROOFSTEP]
rw [m_neg_part_def]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ |a|⁻¹ ⊔ 1 = 1
[PROOFSTEP]
apply sup_of_le_right
[GOAL]
case a
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ |a|⁻¹ ≤ 1
[PROOFSTEP]
rw [Left.inv_le_one_iff]
[GOAL]
case a
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ 1 ≤ |a|
[PROOFSTEP]
apply one_le_abs
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ (a ⊔ b) / (a ⊓ b) = (a ⊔ b) * (a⁻¹ ⊔ b⁻¹)
[PROOFSTEP]
rw [div_eq_mul_inv, ← inv_inf_eq_sup_inv]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ (a ⊔ b) * (a⁻¹ ⊔ b⁻¹) = a * a⁻¹ ⊔ b * a⁻¹ ⊔ (a * b⁻¹ ⊔ b * b⁻¹)
[PROOFSTEP]
rw [mul_sup, sup_mul, sup_mul]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a * a⁻¹ ⊔ b * a⁻¹ ⊔ (a * b⁻¹ ⊔ b * b⁻¹) = 1 ⊔ b / a ⊔ (a / b ⊔ 1)
[PROOFSTEP]
rw [mul_right_inv, mul_right_inv, ← div_eq_mul_inv, ← div_eq_mul_inv]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ 1 ⊔ b / a ⊔ (a / b ⊔ 1) = 1 ⊔ b / a ⊔ (1 / (b / a) ⊔ 1)
[PROOFSTEP]
rw [one_div_div]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ 1 ⊔ b / a ⊔ (1 / (b / a) ⊔ 1) = 1 ⊔ b / a ⊔ ((b / a)⁻¹ ⊔ 1)
[PROOFSTEP]
rw [inv_eq_one_div]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ 1 ⊔ b / a ⊔ ((b / a)⁻¹ ⊔ 1) = 1 ⊔ (b / a ⊔ (b / a)⁻¹ ⊔ 1)
[PROOFSTEP]
rw [sup_assoc, sup_assoc]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ 1 ⊔ (b / a ⊔ (b / a)⁻¹ ⊔ 1) = 1 ⊔ (|b / a| ⊔ 1)
[PROOFSTEP]
rw [abs_eq_sup_inv]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ 1 ⊔ (|b / a| ⊔ 1) = 1 ⊔ |b / a|
[PROOFSTEP]
rw [← m_pos_part_def, m_pos_abs]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ 1 ⊔ |b / a| = |b / a| ⊔ 1
[PROOFSTEP]
rw [sup_comm]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ |b / a| ⊔ 1 = |b / a|
[PROOFSTEP]
rw [← m_pos_part_def, m_pos_abs]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ a⁺ ⊓ a⁻ = 1
[PROOFSTEP]
rw [← mul_left_inj (a⁻)⁻¹, inf_mul, one_mul, mul_right_inv, ← div_eq_mul_inv, pos_div_neg, neg_eq_inv_inf_one, inv_inv]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ (a ⊓ b) * (a ⊔ b) = (a ⊓ b) * (a * b * (b⁻¹ ⊔ a⁻¹))
[PROOFSTEP]
rw [mul_sup b⁻¹ a⁻¹ (a * b), mul_inv_cancel_right, mul_inv_cancel_comm]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ (a ⊓ b) * (a * b * (b⁻¹ ⊔ a⁻¹)) = (a ⊓ b) * (a * b * (a ⊓ b)⁻¹)
[PROOFSTEP]
rw [inv_inf_eq_sup_inv, sup_comm]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ (a ⊓ b) * (a * b * (a ⊓ b)⁻¹) = a * b
[PROOFSTEP]
rw [mul_comm, inv_mul_cancel_right]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a ⊔ b = b * (a / b) ⊔ b * 1
[PROOFSTEP]
rw [mul_one b, div_eq_mul_inv, mul_comm a, mul_inv_cancel_left]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ b * (a / b) ⊔ b * 1 = b * (a / b ⊔ 1)
[PROOFSTEP]
rw [← mul_sup (a / b) 1 b]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a ⊓ b = a * 1 ⊓ a * (b / a)
[PROOFSTEP]
rw [mul_one a, div_eq_mul_inv, mul_comm b, mul_inv_cancel_left]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a * 1 ⊓ a * (b / a) = a * (1 ⊓ b / a)
[PROOFSTEP]
rw [← mul_inf 1 (b / a) a]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a * (1 ⊓ b / a) = a * (b / a ⊓ 1)
[PROOFSTEP]
rw [inf_comm]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a * (b / a ⊓ 1) = a * ((a / b)⁻¹ ⊓ 1)
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a * (b * a⁻¹ ⊓ 1) = a * ((a / b)⁻¹ ⊓ 1)
[PROOFSTEP]
nth_rw 1 [← inv_inv b]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a * (b⁻¹⁻¹ * a⁻¹ ⊓ 1) = a * ((a / b)⁻¹ ⊓ 1)
[PROOFSTEP]
rw [← mul_inv, mul_comm b⁻¹, ← div_eq_mul_inv]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a * ((a / b)⁻¹ ⊓ 1) = a * ((a / b)⁻¹ ⊓ 1⁻¹)
[PROOFSTEP]
rw [inv_one]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a * ((a / b)⁻¹ ⊓ 1⁻¹) = a / (a / b ⊔ 1)
[PROOFSTEP]
rw [← inv_sup_eq_inv_inf_inv, ← div_eq_mul_inv]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a ≤ b ↔ a⁺ ≤ b⁺ ∧ b⁻ ≤ a⁻
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a ≤ b → a⁺ ≤ b⁺ ∧ b⁻ ≤ a⁻
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a⁺ ≤ b⁺ ∧ b⁻ ≤ a⁻ → a ≤ b
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
h : a ≤ b
⊢ a⁺ ≤ b⁺ ∧ b⁻ ≤ a⁻
[PROOFSTEP]
constructor
[GOAL]
case mp.left
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
h : a ≤ b
⊢ a⁺ ≤ b⁺
[PROOFSTEP]
exact sup_le (h.trans (m_le_pos b)) (one_le_pos b)
[GOAL]
case mp.right
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
h : a ≤ b
⊢ b⁻ ≤ a⁻
[PROOFSTEP]
rw [← inv_le_inv_iff] at h
[GOAL]
case mp.right
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
h✝ : a ≤ b
h : b⁻¹ ≤ a⁻¹
⊢ b⁻ ≤ a⁻
[PROOFSTEP]
exact sup_le (h.trans (inv_le_neg a)) (one_le_neg a)
[GOAL]
case mpr
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
h : a⁺ ≤ b⁺ ∧ b⁻ ≤ a⁻
⊢ a ≤ b
[PROOFSTEP]
rw [← pos_div_neg a, ← pos_div_neg b]
[GOAL]
case mpr
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
h : a⁺ ≤ b⁺ ∧ b⁻ ≤ a⁻
⊢ a⁺ / a⁻ ≤ b⁺ / b⁻
[PROOFSTEP]
exact div_le_div'' h.1 h.2
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ (a ⊔ b) ^ 2 = a * b * |b / a|
[PROOFSTEP]
rw [← inf_mul_sup a b, ← sup_div_inf_eq_abs_div, div_eq_mul_inv, ← mul_assoc, mul_comm, mul_assoc, ← pow_two,
  inv_mul_cancel_left]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ (a ⊓ b) ^ 2 = a * b / |b / a|
[PROOFSTEP]
rw [← inf_mul_sup a b, ← sup_div_inf_eq_abs_div, div_eq_mul_inv, div_eq_mul_inv, mul_inv_rev, inv_inv, mul_assoc,
  mul_inv_cancel_comm_assoc, ← pow_two]
[GOAL]
α✝ : Type u
β : Type v
inst✝³ : Lattice α✝
inst✝² : CommGroup α✝
α : Type u
s : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
⊢ ∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
[PROOFSTEP]
intros x y z
[GOAL]
α✝ : Type u
β : Type v
inst✝³ : Lattice α✝
inst✝² : CommGroup α✝
α : Type u
s : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x y z : α
⊢ (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
[PROOFSTEP]
rw [← mul_le_mul_iff_left (x ⊓ (y ⊓ z)), inf_mul_sup x (y ⊓ z), ← inv_mul_le_iff_le_mul, le_inf_iff]
[GOAL]
α✝ : Type u
β : Type v
inst✝³ : Lattice α✝
inst✝² : CommGroup α✝
α : Type u
s : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x y z : α
⊢ x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ y ∧ x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ z
[PROOFSTEP]
constructor
[GOAL]
case left
α✝ : Type u
β : Type v
inst✝³ : Lattice α✝
inst✝² : CommGroup α✝
α : Type u
s : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x y z : α
⊢ x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ y
[PROOFSTEP]
rw [inv_mul_le_iff_le_mul, ← inf_mul_sup x y]
[GOAL]
case left
α✝ : Type u
β : Type v
inst✝³ : Lattice α✝
inst✝² : CommGroup α✝
α : Type u
s : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x y z : α
⊢ (x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z)) ≤ (x ⊓ y) * (x ⊔ y)
[PROOFSTEP]
apply mul_le_mul'
[GOAL]
case left.h₁
α✝ : Type u
β : Type v
inst✝³ : Lattice α✝
inst✝² : CommGroup α✝
α : Type u
s : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x y z : α
⊢ x ⊓ (y ⊓ z) ≤ x ⊓ y
[PROOFSTEP]
apply inf_le_inf_left
[GOAL]
case left.h₁.h
α✝ : Type u
β : Type v
inst✝³ : Lattice α✝
inst✝² : CommGroup α✝
α : Type u
s : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x y z : α
⊢ y ⊓ z ≤ y
[PROOFSTEP]
apply inf_le_left
[GOAL]
case left.h₂
α✝ : Type u
β : Type v
inst✝³ : Lattice α✝
inst✝² : CommGroup α✝
α : Type u
s : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x y z : α
⊢ (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y
[PROOFSTEP]
apply inf_le_left
[GOAL]
case right
α✝ : Type u
β : Type v
inst✝³ : Lattice α✝
inst✝² : CommGroup α✝
α : Type u
s : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x y z : α
⊢ x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ z
[PROOFSTEP]
rw [inv_mul_le_iff_le_mul, ← inf_mul_sup x z]
[GOAL]
case right
α✝ : Type u
β : Type v
inst✝³ : Lattice α✝
inst✝² : CommGroup α✝
α : Type u
s : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x y z : α
⊢ (x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z)) ≤ (x ⊓ z) * (x ⊔ z)
[PROOFSTEP]
apply mul_le_mul'
[GOAL]
case right.h₁
α✝ : Type u
β : Type v
inst✝³ : Lattice α✝
inst✝² : CommGroup α✝
α : Type u
s : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x y z : α
⊢ x ⊓ (y ⊓ z) ≤ x ⊓ z
[PROOFSTEP]
apply inf_le_inf_left
[GOAL]
case right.h₁.h
α✝ : Type u
β : Type v
inst✝³ : Lattice α✝
inst✝² : CommGroup α✝
α : Type u
s : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x y z : α
⊢ y ⊓ z ≤ z
[PROOFSTEP]
apply inf_le_right
[GOAL]
case right.h₂
α✝ : Type u
β : Type v
inst✝³ : Lattice α✝
inst✝² : CommGroup α✝
α : Type u
s : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x y z : α
⊢ (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ z
[PROOFSTEP]
apply inf_le_right
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ |(a ⊔ c) / (b ⊔ c)| * |(a ⊓ c) / (b ⊓ c)| = |a / b|
[PROOFSTEP]
letI : DistribLattice α := LatticeOrderedCommGroup.latticeOrderedCommGroupToDistribLattice α
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
this : DistribLattice α := latticeOrderedCommGroupToDistribLattice α
⊢ |(a ⊔ c) / (b ⊔ c)| * |(a ⊓ c) / (b ⊓ c)| = |a / b|
[PROOFSTEP]
calc
  |(a ⊔ c) / (b ⊔ c)| * |(a ⊓ c) / (b ⊓ c)| = (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)| := by
    rw [sup_div_inf_eq_abs_div]
  _ = (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) := by
    rw [sup_div_inf_eq_abs_div (b ⊓ c) (a ⊓ c)]
  _ = (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c)) := by
    rw [← sup_inf_right, ← inf_sup_right, sup_assoc, @sup_comm _ _ c (a ⊔ c), sup_right_idem, sup_assoc, inf_assoc,
      @inf_comm _ _ c (a ⊓ c), inf_right_idem, inf_assoc]
  _ = (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c)) := by rw [div_mul_div_comm]
  _ = (b ⊔ a) * c / ((b ⊓ a) * c) := by rw [mul_comm, inf_mul_sup, mul_comm (b ⊓ a ⊔ c), inf_mul_sup]
  _ = (b ⊔ a) / (b ⊓ a) := by rw [div_eq_mul_inv, mul_inv_rev, mul_assoc, mul_inv_cancel_left, ← div_eq_mul_inv]
  _ = |a / b| := by rw [sup_div_inf_eq_abs_div]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
this : DistribLattice α := latticeOrderedCommGroupToDistribLattice α
⊢ |(a ⊔ c) / (b ⊔ c)| * |(a ⊓ c) / (b ⊓ c)| = (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)|
[PROOFSTEP]
rw [sup_div_inf_eq_abs_div]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
this : DistribLattice α := latticeOrderedCommGroupToDistribLattice α
⊢ (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)| =
    (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c)))
[PROOFSTEP]
rw [sup_div_inf_eq_abs_div (b ⊓ c) (a ⊓ c)]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
this : DistribLattice α := latticeOrderedCommGroupToDistribLattice α
⊢ (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) =
    (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c))
[PROOFSTEP]
rw [← sup_inf_right, ← inf_sup_right, sup_assoc, @sup_comm _ _ c (a ⊔ c), sup_right_idem, sup_assoc, inf_assoc,
  @inf_comm _ _ c (a ⊓ c), inf_right_idem, inf_assoc]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
this : DistribLattice α := latticeOrderedCommGroupToDistribLattice α
⊢ (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c)) = (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c))
[PROOFSTEP]
rw [div_mul_div_comm]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
this : DistribLattice α := latticeOrderedCommGroupToDistribLattice α
⊢ (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c)) = (b ⊔ a) * c / ((b ⊓ a) * c)
[PROOFSTEP]
rw [mul_comm, inf_mul_sup, mul_comm (b ⊓ a ⊔ c), inf_mul_sup]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
this : DistribLattice α := latticeOrderedCommGroupToDistribLattice α
⊢ (b ⊔ a) * c / ((b ⊓ a) * c) = (b ⊔ a) / (b ⊓ a)
[PROOFSTEP]
rw [div_eq_mul_inv, mul_inv_rev, mul_assoc, mul_inv_cancel_left, ← div_eq_mul_inv]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
this : DistribLattice α := latticeOrderedCommGroupToDistribLattice α
⊢ (b ⊔ a) / (b ⊓ a) = |a / b|
[PROOFSTEP]
rw [sup_div_inf_eq_abs_div]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ |(a ⊔ c) / (b ⊔ c)| ≤ |a / b|
[PROOFSTEP]
apply le_of_mul_le_of_one_le_left
[GOAL]
case h
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ |(a ⊔ c) / (b ⊔ c)| * ?b ≤ |a / b|
[PROOFSTEP]
rw [abs_div_sup_mul_abs_div_inf]
[GOAL]
case hle
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ 1 ≤ |(a ⊓ c) / (b ⊓ c)|
[PROOFSTEP]
exact one_le_abs _
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ |(a ⊓ c) / (b ⊓ c)| ≤ |a / b|
[PROOFSTEP]
apply le_of_mul_le_of_one_le_right
[GOAL]
case h
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ ?a * |(a ⊓ c) / (b ⊓ c)| ≤ |a / b|
[PROOFSTEP]
rw [abs_div_sup_mul_abs_div_inf]
[GOAL]
case hle
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ 1 ≤ |(a ⊔ c) / (b ⊔ c)|
[PROOFSTEP]
exact one_le_abs _
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ |a * b| ≤ |a| * |b|
[PROOFSTEP]
apply sup_le
[GOAL]
case a
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a * b ≤ |a| * |b|
[PROOFSTEP]
exact mul_le_mul' (le_mabs a) (le_mabs b)
[GOAL]
case a
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ (a * b)⁻¹ ≤ |a| * |b|
[PROOFSTEP]
rw [mul_inv]
[GOAL]
case a
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a⁻¹ * b⁻¹ ≤ |a| * |b|
[PROOFSTEP]
exact mul_le_mul' (inv_le_abs _) (inv_le_abs _)
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ ||a| / |b|| ≤ |a / b|
[PROOFSTEP]
rw [abs_eq_sup_inv, sup_le_iff]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ |a| / |b| ≤ |a / b| ∧ (|a| / |b|)⁻¹ ≤ |a / b|
[PROOFSTEP]
constructor
[GOAL]
case left
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ |a| / |b| ≤ |a / b|
[PROOFSTEP]
apply div_le_iff_le_mul.2
[GOAL]
case left
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ |a| ≤ |a / b| * |b|
[PROOFSTEP]
convert mabs_mul_le (a / b) b
[GOAL]
case h.e'_3.h.e'_3
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a = a / b * b
[PROOFSTEP]
rw [div_mul_cancel']
[GOAL]
case right
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ (|a| / |b|)⁻¹ ≤ |a / b|
[PROOFSTEP]
rw [div_eq_mul_inv, mul_inv_rev, inv_inv, mul_inv_le_iff_le_mul, abs_div_comm]
[GOAL]
case right
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ |b| ≤ |b / a| * |a|
[PROOFSTEP]
convert mabs_mul_le (b / a) a
[GOAL]
case h.e'_3.h.e'_3
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ b = b / a * a
[PROOFSTEP]
rw [div_mul_cancel']
[GOAL]
α : Type u
β : Type v
inst✝⁷ : Lattice α
inst✝⁶ : CommGroup α
inst✝⁵ : Semiring α
inst✝⁴ : Invertible 2
inst✝³ : Lattice β
inst✝² : AddCommGroup β
inst✝¹ : Module α β
inst✝ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
x y : β
⊢ x ⊓ y = ⅟2 • (x + y - |y - x|)
[PROOFSTEP]
rw [← LatticeOrderedCommGroup.two_inf_eq_add_sub_abs_sub x y, two_smul, ← two_smul α, smul_smul, invOf_mul_self,
  one_smul]
[GOAL]
α : Type u
β : Type v
inst✝⁷ : Lattice α
inst✝⁶ : CommGroup α
inst✝⁵ : Semiring α
inst✝⁴ : Invertible 2
inst✝³ : Lattice β
inst✝² : AddCommGroup β
inst✝¹ : Module α β
inst✝ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
x y : β
⊢ x ⊔ y = ⅟2 • (x + y + |y - x|)
[PROOFSTEP]
rw [← LatticeOrderedCommGroup.two_sup_eq_add_add_abs_sub x y, two_smul, ← two_smul α, smul_smul, invOf_mul_self,
  one_smul]
[GOAL]
α : Type u
β : Type v
inst✝⁷ : Lattice α
inst✝⁶ : CommGroup α
inst✝⁵ : DivisionSemiring α
inst✝⁴ : NeZero 2
inst✝³ : Lattice β
inst✝² : AddCommGroup β
inst✝¹ : Module α β
inst✝ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
x y : β
⊢ x ⊓ y = 2⁻¹ • (x + y - |y - x|)
[PROOFSTEP]
letI := invertibleOfNonzero (two_ne_zero' α)
[GOAL]
α : Type u
β : Type v
inst✝⁷ : Lattice α
inst✝⁶ : CommGroup α
inst✝⁵ : DivisionSemiring α
inst✝⁴ : NeZero 2
inst✝³ : Lattice β
inst✝² : AddCommGroup β
inst✝¹ : Module α β
inst✝ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
x y : β
this : Invertible 2 := invertibleOfNonzero (_ : 2 ≠ 0)
⊢ x ⊓ y = 2⁻¹ • (x + y - |y - x|)
[PROOFSTEP]
exact inf_eq_half_smul_add_sub_abs_sub α x y
[GOAL]
α : Type u
β : Type v
inst✝⁷ : Lattice α
inst✝⁶ : CommGroup α
inst✝⁵ : DivisionSemiring α
inst✝⁴ : NeZero 2
inst✝³ : Lattice β
inst✝² : AddCommGroup β
inst✝¹ : Module α β
inst✝ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
x y : β
⊢ x ⊔ y = 2⁻¹ • (x + y + |y - x|)
[PROOFSTEP]
letI := invertibleOfNonzero (two_ne_zero' α)
[GOAL]
α : Type u
β : Type v
inst✝⁷ : Lattice α
inst✝⁶ : CommGroup α
inst✝⁵ : DivisionSemiring α
inst✝⁴ : NeZero 2
inst✝³ : Lattice β
inst✝² : AddCommGroup β
inst✝¹ : Module α β
inst✝ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
x y : β
this : Invertible 2 := invertibleOfNonzero (_ : 2 ≠ 0)
⊢ x ⊔ y = 2⁻¹ • (x + y + |y - x|)
[PROOFSTEP]
exact sup_eq_half_smul_add_add_abs_sub α x y


[GOAL]
α : Type u_1
inst✝³ : CompleteLattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
s✝ t s : Set α
⊢ sSup s⁻¹ = (sInf s)⁻¹
[PROOFSTEP]
rw [← image_inv, sSup_image]
[GOAL]
α : Type u_1
inst✝³ : CompleteLattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
s✝ t s : Set α
⊢ ⨆ (a : α) (_ : a ∈ s), a⁻¹ = (sInf s)⁻¹
[PROOFSTEP]
exact ((OrderIso.inv α).map_sInf _).symm
[GOAL]
α : Type u_1
inst✝³ : CompleteLattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
s✝ t s : Set α
⊢ sInf s⁻¹ = (sSup s)⁻¹
[PROOFSTEP]
rw [← image_inv, sInf_image]
[GOAL]
α : Type u_1
inst✝³ : CompleteLattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
s✝ t s : Set α
⊢ ⨅ (a : α) (_ : a ∈ s), a⁻¹ = (sSup s)⁻¹
[PROOFSTEP]
exact ((OrderIso.inv α).map_sSup _).symm
[GOAL]
α : Type u_1
inst✝³ : CompleteLattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
s t : Set α
⊢ sSup (s / t) = sSup s / sInf t
[PROOFSTEP]
simp_rw [div_eq_mul_inv, sSup_mul, sSup_inv]
[GOAL]
α : Type u_1
inst✝³ : CompleteLattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
s t : Set α
⊢ sInf (s / t) = sInf s / sSup t
[PROOFSTEP]
simp_rw [div_eq_mul_inv, sInf_mul, sInf_inv]
[GOAL]
α : Type u_1
inst✝³ : ConditionallyCompleteLattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
s t : Set α
hs₀ : Set.Nonempty s
hs₁ : BddBelow s
⊢ sSup s⁻¹ = (sInf s)⁻¹
[PROOFSTEP]
rw [← image_inv]
[GOAL]
α : Type u_1
inst✝³ : ConditionallyCompleteLattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
s t : Set α
hs₀ : Set.Nonempty s
hs₁ : BddBelow s
⊢ sSup (Inv.inv '' s) = (sInf s)⁻¹
[PROOFSTEP]
exact ((OrderIso.inv α).map_csInf' hs₀ hs₁).symm
[GOAL]
α : Type u_1
inst✝³ : ConditionallyCompleteLattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
s t : Set α
hs₀ : Set.Nonempty s
hs₁ : BddAbove s
⊢ sInf s⁻¹ = (sSup s)⁻¹
[PROOFSTEP]
rw [← image_inv]
[GOAL]
α : Type u_1
inst✝³ : ConditionallyCompleteLattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
s t : Set α
hs₀ : Set.Nonempty s
hs₁ : BddAbove s
⊢ sInf (Inv.inv '' s) = (sSup s)⁻¹
[PROOFSTEP]
exact ((OrderIso.inv α).map_csSup' hs₀ hs₁).symm
[GOAL]
α : Type u_1
inst✝³ : ConditionallyCompleteLattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
s t : Set α
hs₀ : Set.Nonempty s
hs₁ : BddAbove s
ht₀ : Set.Nonempty t
ht₁ : BddBelow t
⊢ sSup (s / t) = sSup s / sInf t
[PROOFSTEP]
rw [div_eq_mul_inv, csSup_mul hs₀ hs₁ ht₀.inv ht₁.inv, csSup_inv ht₀ ht₁, div_eq_mul_inv]
[GOAL]
α : Type u_1
inst✝³ : ConditionallyCompleteLattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
s t : Set α
hs₀ : Set.Nonempty s
hs₁ : BddBelow s
ht₀ : Set.Nonempty t
ht₁ : BddAbove t
⊢ sInf (s / t) = sInf s / sSup t
[PROOFSTEP]
rw [div_eq_mul_inv, csInf_mul hs₀ hs₁ ht₀.inv ht₁.inv, csInf_inv ht₀ ht₁, div_eq_mul_inv]
[GOAL]
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
⊢ r • Ioo a b = Ioo (r • a) (r • b)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ x ∈ r • Ioo a b ↔ x ∈ Ioo (r • a) (r • b)
[PROOFSTEP]
simp only [mem_smul_set, smul_eq_mul, mem_Ioo]
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, (a < y ∧ y < b) ∧ r * y = x) ↔ r * a < x ∧ x < r * b
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, (a < y ∧ y < b) ∧ r * y = x) → r * a < x ∧ x < r * b
[PROOFSTEP]
rintro ⟨a, ⟨a_h_left_left, a_h_left_right⟩, rfl⟩
[GOAL]
case h.mp.intro.intro.intro
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a✝ b r : K
hr : 0 < r
a : K
a_h_left_left : a✝ < a
a_h_left_right : a < b
⊢ r * a✝ < r * a ∧ r * a < r * b
[PROOFSTEP]
constructor
[GOAL]
case h.mp.intro.intro.intro.left
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a✝ b r : K
hr : 0 < r
a : K
a_h_left_left : a✝ < a
a_h_left_right : a < b
⊢ r * a✝ < r * a
case h.mp.intro.intro.intro.right
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a✝ b r : K
hr : 0 < r
a : K
a_h_left_left : a✝ < a
a_h_left_right : a < b
⊢ r * a < r * b
[PROOFSTEP]
exact (mul_lt_mul_left hr).mpr a_h_left_left
[GOAL]
case h.mp.intro.intro.intro.right
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a✝ b r : K
hr : 0 < r
a : K
a_h_left_left : a✝ < a
a_h_left_right : a < b
⊢ r * a < r * b
[PROOFSTEP]
exact (mul_lt_mul_left hr).mpr a_h_left_right
[GOAL]
case h.mpr
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ r * a < x ∧ x < r * b → ∃ y, (a < y ∧ y < b) ∧ r * y = x
[PROOFSTEP]
rintro ⟨a_left, a_right⟩
[GOAL]
case h.mpr.intro
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
a_left : r * a < x
a_right : x < r * b
⊢ ∃ y, (a < y ∧ y < b) ∧ r * y = x
[PROOFSTEP]
use x / r
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
a_left : r * a < x
a_right : x < r * b
⊢ (a < x / r ∧ x / r < b) ∧ r * (x / r) = x
[PROOFSTEP]
refine' ⟨⟨(lt_div_iff' hr).mpr a_left, (div_lt_iff' hr).mpr a_right⟩, _⟩
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
a_left : r * a < x
a_right : x < r * b
⊢ r * (x / r) = x
[PROOFSTEP]
rw [mul_div_cancel' _ (ne_of_gt hr)]
[GOAL]
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
⊢ r • Icc a b = Icc (r • a) (r • b)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ x ∈ r • Icc a b ↔ x ∈ Icc (r • a) (r • b)
[PROOFSTEP]
simp only [mem_smul_set, smul_eq_mul, mem_Icc]
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, (a ≤ y ∧ y ≤ b) ∧ r * y = x) ↔ r * a ≤ x ∧ x ≤ r * b
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, (a ≤ y ∧ y ≤ b) ∧ r * y = x) → r * a ≤ x ∧ x ≤ r * b
[PROOFSTEP]
rintro ⟨a, ⟨a_h_left_left, a_h_left_right⟩, rfl⟩
[GOAL]
case h.mp.intro.intro.intro
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a✝ b r : K
hr : 0 < r
a : K
a_h_left_left : a✝ ≤ a
a_h_left_right : a ≤ b
⊢ r * a✝ ≤ r * a ∧ r * a ≤ r * b
[PROOFSTEP]
constructor
[GOAL]
case h.mp.intro.intro.intro.left
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a✝ b r : K
hr : 0 < r
a : K
a_h_left_left : a✝ ≤ a
a_h_left_right : a ≤ b
⊢ r * a✝ ≤ r * a
case h.mp.intro.intro.intro.right
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a✝ b r : K
hr : 0 < r
a : K
a_h_left_left : a✝ ≤ a
a_h_left_right : a ≤ b
⊢ r * a ≤ r * b
[PROOFSTEP]
exact (mul_le_mul_left hr).mpr a_h_left_left
[GOAL]
case h.mp.intro.intro.intro.right
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a✝ b r : K
hr : 0 < r
a : K
a_h_left_left : a✝ ≤ a
a_h_left_right : a ≤ b
⊢ r * a ≤ r * b
[PROOFSTEP]
exact (mul_le_mul_left hr).mpr a_h_left_right
[GOAL]
case h.mpr
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ r * a ≤ x ∧ x ≤ r * b → ∃ y, (a ≤ y ∧ y ≤ b) ∧ r * y = x
[PROOFSTEP]
rintro ⟨a_left, a_right⟩
[GOAL]
case h.mpr.intro
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
a_left : r * a ≤ x
a_right : x ≤ r * b
⊢ ∃ y, (a ≤ y ∧ y ≤ b) ∧ r * y = x
[PROOFSTEP]
use x / r
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
a_left : r * a ≤ x
a_right : x ≤ r * b
⊢ (a ≤ x / r ∧ x / r ≤ b) ∧ r * (x / r) = x
[PROOFSTEP]
refine' ⟨⟨(le_div_iff' hr).mpr a_left, (div_le_iff' hr).mpr a_right⟩, _⟩
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
a_left : r * a ≤ x
a_right : x ≤ r * b
⊢ r * (x / r) = x
[PROOFSTEP]
rw [mul_div_cancel' _ (ne_of_gt hr)]
[GOAL]
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
⊢ r • Ico a b = Ico (r • a) (r • b)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ x ∈ r • Ico a b ↔ x ∈ Ico (r • a) (r • b)
[PROOFSTEP]
simp only [mem_smul_set, smul_eq_mul, mem_Ico]
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, (a ≤ y ∧ y < b) ∧ r * y = x) ↔ r * a ≤ x ∧ x < r * b
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, (a ≤ y ∧ y < b) ∧ r * y = x) → r * a ≤ x ∧ x < r * b
[PROOFSTEP]
rintro ⟨a, ⟨a_h_left_left, a_h_left_right⟩, rfl⟩
[GOAL]
case h.mp.intro.intro.intro
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a✝ b r : K
hr : 0 < r
a : K
a_h_left_left : a✝ ≤ a
a_h_left_right : a < b
⊢ r * a✝ ≤ r * a ∧ r * a < r * b
[PROOFSTEP]
constructor
[GOAL]
case h.mp.intro.intro.intro.left
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a✝ b r : K
hr : 0 < r
a : K
a_h_left_left : a✝ ≤ a
a_h_left_right : a < b
⊢ r * a✝ ≤ r * a
case h.mp.intro.intro.intro.right
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a✝ b r : K
hr : 0 < r
a : K
a_h_left_left : a✝ ≤ a
a_h_left_right : a < b
⊢ r * a < r * b
[PROOFSTEP]
exact (mul_le_mul_left hr).mpr a_h_left_left
[GOAL]
case h.mp.intro.intro.intro.right
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a✝ b r : K
hr : 0 < r
a : K
a_h_left_left : a✝ ≤ a
a_h_left_right : a < b
⊢ r * a < r * b
[PROOFSTEP]
exact (mul_lt_mul_left hr).mpr a_h_left_right
[GOAL]
case h.mpr
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ r * a ≤ x ∧ x < r * b → ∃ y, (a ≤ y ∧ y < b) ∧ r * y = x
[PROOFSTEP]
rintro ⟨a_left, a_right⟩
[GOAL]
case h.mpr.intro
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
a_left : r * a ≤ x
a_right : x < r * b
⊢ ∃ y, (a ≤ y ∧ y < b) ∧ r * y = x
[PROOFSTEP]
use x / r
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
a_left : r * a ≤ x
a_right : x < r * b
⊢ (a ≤ x / r ∧ x / r < b) ∧ r * (x / r) = x
[PROOFSTEP]
refine' ⟨⟨(le_div_iff' hr).mpr a_left, (div_lt_iff' hr).mpr a_right⟩, _⟩
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
a_left : r * a ≤ x
a_right : x < r * b
⊢ r * (x / r) = x
[PROOFSTEP]
rw [mul_div_cancel' _ (ne_of_gt hr)]
[GOAL]
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
⊢ r • Ioc a b = Ioc (r • a) (r • b)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ x ∈ r • Ioc a b ↔ x ∈ Ioc (r • a) (r • b)
[PROOFSTEP]
simp only [mem_smul_set, smul_eq_mul, mem_Ioc]
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, (a < y ∧ y ≤ b) ∧ r * y = x) ↔ r * a < x ∧ x ≤ r * b
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, (a < y ∧ y ≤ b) ∧ r * y = x) → r * a < x ∧ x ≤ r * b
[PROOFSTEP]
rintro ⟨a, ⟨a_h_left_left, a_h_left_right⟩, rfl⟩
[GOAL]
case h.mp.intro.intro.intro
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a✝ b r : K
hr : 0 < r
a : K
a_h_left_left : a✝ < a
a_h_left_right : a ≤ b
⊢ r * a✝ < r * a ∧ r * a ≤ r * b
[PROOFSTEP]
constructor
[GOAL]
case h.mp.intro.intro.intro.left
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a✝ b r : K
hr : 0 < r
a : K
a_h_left_left : a✝ < a
a_h_left_right : a ≤ b
⊢ r * a✝ < r * a
case h.mp.intro.intro.intro.right
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a✝ b r : K
hr : 0 < r
a : K
a_h_left_left : a✝ < a
a_h_left_right : a ≤ b
⊢ r * a ≤ r * b
[PROOFSTEP]
exact (mul_lt_mul_left hr).mpr a_h_left_left
[GOAL]
case h.mp.intro.intro.intro.right
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a✝ b r : K
hr : 0 < r
a : K
a_h_left_left : a✝ < a
a_h_left_right : a ≤ b
⊢ r * a ≤ r * b
[PROOFSTEP]
exact (mul_le_mul_left hr).mpr a_h_left_right
[GOAL]
case h.mpr
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ r * a < x ∧ x ≤ r * b → ∃ y, (a < y ∧ y ≤ b) ∧ r * y = x
[PROOFSTEP]
rintro ⟨a_left, a_right⟩
[GOAL]
case h.mpr.intro
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
a_left : r * a < x
a_right : x ≤ r * b
⊢ ∃ y, (a < y ∧ y ≤ b) ∧ r * y = x
[PROOFSTEP]
use x / r
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
a_left : r * a < x
a_right : x ≤ r * b
⊢ (a < x / r ∧ x / r ≤ b) ∧ r * (x / r) = x
[PROOFSTEP]
refine' ⟨⟨(lt_div_iff' hr).mpr a_left, (div_le_iff' hr).mpr a_right⟩, _⟩
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
a_left : r * a < x
a_right : x ≤ r * b
⊢ r * (x / r) = x
[PROOFSTEP]
rw [mul_div_cancel' _ (ne_of_gt hr)]
[GOAL]
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
⊢ r • Ioi a = Ioi (r • a)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ x ∈ r • Ioi a ↔ x ∈ Ioi (r • a)
[PROOFSTEP]
simp only [mem_smul_set, smul_eq_mul, mem_Ioi]
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, a < y ∧ r * y = x) ↔ r * a < x
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, a < y ∧ r * y = x) → r * a < x
[PROOFSTEP]
rintro ⟨a_w, a_h_left, rfl⟩
[GOAL]
case h.mp.intro.intro
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
a_w : K
a_h_left : a < a_w
⊢ r * a < r * a_w
[PROOFSTEP]
exact (mul_lt_mul_left hr).mpr a_h_left
[GOAL]
case h.mpr
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ r * a < x → ∃ y, a < y ∧ r * y = x
[PROOFSTEP]
rintro h
[GOAL]
case h.mpr
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : r * a < x
⊢ ∃ y, a < y ∧ r * y = x
[PROOFSTEP]
use x / r
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : r * a < x
⊢ a < x / r ∧ r * (x / r) = x
[PROOFSTEP]
constructor
[GOAL]
case h.left
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : r * a < x
⊢ a < x / r
case h.right
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : r * a < x
⊢ r * (x / r) = x
[PROOFSTEP]
exact (lt_div_iff' hr).mpr h
[GOAL]
case h.right
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : r * a < x
⊢ r * (x / r) = x
[PROOFSTEP]
exact mul_div_cancel' _ (ne_of_gt hr)
[GOAL]
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
⊢ r • Iio a = Iio (r • a)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ x ∈ r • Iio a ↔ x ∈ Iio (r • a)
[PROOFSTEP]
simp only [mem_smul_set, smul_eq_mul, mem_Iio]
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, y < a ∧ r * y = x) ↔ x < r * a
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, y < a ∧ r * y = x) → x < r * a
[PROOFSTEP]
rintro ⟨a_w, a_h_left, rfl⟩
[GOAL]
case h.mp.intro.intro
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
a_w : K
a_h_left : a_w < a
⊢ r * a_w < r * a
[PROOFSTEP]
exact (mul_lt_mul_left hr).mpr a_h_left
[GOAL]
case h.mpr
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ x < r * a → ∃ y, y < a ∧ r * y = x
[PROOFSTEP]
rintro h
[GOAL]
case h.mpr
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x < r * a
⊢ ∃ y, y < a ∧ r * y = x
[PROOFSTEP]
use x / r
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x < r * a
⊢ x / r < a ∧ r * (x / r) = x
[PROOFSTEP]
constructor
[GOAL]
case h.left
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x < r * a
⊢ x / r < a
case h.right
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x < r * a
⊢ r * (x / r) = x
[PROOFSTEP]
exact (div_lt_iff' hr).mpr h
[GOAL]
case h.right
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x < r * a
⊢ r * (x / r) = x
[PROOFSTEP]
exact mul_div_cancel' _ (ne_of_gt hr)
[GOAL]
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
⊢ r • Ici a = Ici (r • a)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ x ∈ r • Ici a ↔ x ∈ Ici (r • a)
[PROOFSTEP]
simp only [mem_smul_set, smul_eq_mul, mem_Ioi]
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, y ∈ Ici a ∧ r * y = x) ↔ x ∈ Ici (r * a)
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, y ∈ Ici a ∧ r * y = x) → x ∈ Ici (r * a)
[PROOFSTEP]
rintro ⟨a_w, a_h_left, rfl⟩
[GOAL]
case h.mp.intro.intro
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
a_w : K
a_h_left : a_w ∈ Ici a
⊢ r * a_w ∈ Ici (r * a)
[PROOFSTEP]
exact (mul_le_mul_left hr).mpr a_h_left
[GOAL]
case h.mpr
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ x ∈ Ici (r * a) → ∃ y, y ∈ Ici a ∧ r * y = x
[PROOFSTEP]
rintro h
[GOAL]
case h.mpr
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x ∈ Ici (r * a)
⊢ ∃ y, y ∈ Ici a ∧ r * y = x
[PROOFSTEP]
use x / r
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x ∈ Ici (r * a)
⊢ x / r ∈ Ici a ∧ r * (x / r) = x
[PROOFSTEP]
constructor
[GOAL]
case h.left
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x ∈ Ici (r * a)
⊢ x / r ∈ Ici a
case h.right
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x ∈ Ici (r * a)
⊢ r * (x / r) = x
[PROOFSTEP]
exact (le_div_iff' hr).mpr h
[GOAL]
case h.right
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x ∈ Ici (r * a)
⊢ r * (x / r) = x
[PROOFSTEP]
exact mul_div_cancel' _ (ne_of_gt hr)
[GOAL]
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
⊢ r • Iic a = Iic (r • a)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ x ∈ r • Iic a ↔ x ∈ Iic (r • a)
[PROOFSTEP]
simp only [mem_smul_set, smul_eq_mul, mem_Iio]
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, y ∈ Iic a ∧ r * y = x) ↔ x ∈ Iic (r * a)
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, y ∈ Iic a ∧ r * y = x) → x ∈ Iic (r * a)
[PROOFSTEP]
rintro ⟨a_w, a_h_left, rfl⟩
[GOAL]
case h.mp.intro.intro
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
a_w : K
a_h_left : a_w ∈ Iic a
⊢ r * a_w ∈ Iic (r * a)
[PROOFSTEP]
exact (mul_le_mul_left hr).mpr a_h_left
[GOAL]
case h.mpr
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ x ∈ Iic (r * a) → ∃ y, y ∈ Iic a ∧ r * y = x
[PROOFSTEP]
rintro h
[GOAL]
case h.mpr
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x ∈ Iic (r * a)
⊢ ∃ y, y ∈ Iic a ∧ r * y = x
[PROOFSTEP]
use x / r
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x ∈ Iic (r * a)
⊢ x / r ∈ Iic a ∧ r * (x / r) = x
[PROOFSTEP]
constructor
[GOAL]
case h.left
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x ∈ Iic (r * a)
⊢ x / r ∈ Iic a
case h.right
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x ∈ Iic (r * a)
⊢ r * (x / r) = x
[PROOFSTEP]
exact (div_le_iff' hr).mpr h
[GOAL]
case h.right
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x ∈ Iic (r * a)
⊢ r * (x / r) = x
[PROOFSTEP]
exact mul_div_cancel' _ (ne_of_gt hr)


[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
⊢ a - b ≤ c ↔ a ≤ b + c
[PROOFSTEP]
rw [tsub_le_iff_right, add_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
⊢ a - b ≤ c ↔ a - c ≤ b
[PROOFSTEP]
rw [tsub_le_iff_left, tsub_le_iff_right]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ a + b - c ≤ a + (b - c)
[PROOFSTEP]
rw [tsub_le_iff_left, add_left_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ a + b ≤ a + (c + (b - c))
[PROOFSTEP]
exact add_le_add_left le_add_tsub a
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ a + b - c ≤ a - c + b
[PROOFSTEP]
rw [add_comm, add_comm _ b]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ b + a - c ≤ b + (a - c)
[PROOFSTEP]
exact add_tsub_le_assoc
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ a + b ≤ a + c + (b - c)
[PROOFSTEP]
rw [add_assoc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ a + b ≤ a + (c + (b - c))
[PROOFSTEP]
exact add_le_add_left le_add_tsub a
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ a + b ≤ a - c + (b + c)
[PROOFSTEP]
rw [add_comm a, add_comm (a - c)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ b + a ≤ b + c + (a - c)
[PROOFSTEP]
exact add_le_add_add_tsub
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ a - c ≤ a - b + (b - c)
[PROOFSTEP]
rw [tsub_le_iff_left, ← add_assoc, add_right_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ a ≤ c + (b - c) + (a - b)
[PROOFSTEP]
exact le_add_tsub.trans (add_le_add_right le_add_tsub _)
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ c - a - (c - b) ≤ b - a
[PROOFSTEP]
rw [tsub_le_iff_left, tsub_le_iff_left, add_left_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ c ≤ c - b + (a + (b - a))
[PROOFSTEP]
exact le_tsub_add.trans (add_le_add_left le_add_tsub _)
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ a + b - (c + d) ≤ a - c + (b - d)
[PROOFSTEP]
rw [add_comm c, tsub_le_iff_left, add_assoc, ← tsub_le_iff_left, ← tsub_le_iff_left]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ a + b - d - c ≤ a - c + (b - d)
[PROOFSTEP]
refine' (tsub_le_tsub_right add_tsub_le_assoc c).trans _
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ a + (b - d) - c ≤ a - c + (b - d)
[PROOFSTEP]
rw [add_comm a, add_comm (a - c)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ b - d + a - c ≤ b - d + (a - c)
[PROOFSTEP]
exact add_tsub_le_assoc
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ a + b - (a + c) ≤ b - c
[PROOFSTEP]
rw [tsub_le_iff_left, add_assoc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ a + b ≤ a + (c + (b - c))
[PROOFSTEP]
exact add_le_add_left le_add_tsub _
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ a + c - (b + c) ≤ a - b
[PROOFSTEP]
rw [tsub_le_iff_left, add_right_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ a + c ≤ b + (a - b) + c
[PROOFSTEP]
exact add_le_add_right le_add_tsub c
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
⊢ a ≤ a + b - b
[PROOFSTEP]
rw [add_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
⊢ a ≤ b + a - b
[PROOFSTEP]
exact hb.le_add_tsub_swap
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
h : a + b ≤ c
⊢ b + a ≤ c
[PROOFSTEP]
rwa [add_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : AddCommMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
⊢ a - b ≤ 0 ↔ a ≤ b
[PROOFSTEP]
rw [tsub_le_iff_left, add_zero]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝ b✝ c✝ d b a c : α
⊢ b - a - c = b - (a + c)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝ b✝ c✝ d b a c : α
⊢ b - a - c ≤ b - (a + c)
[PROOFSTEP]
rw [tsub_le_iff_left, tsub_le_iff_left, ← add_assoc, ← tsub_le_iff_left]
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝ b✝ c✝ d b a c : α
⊢ b - (a + c) ≤ b - a - c
[PROOFSTEP]
rw [tsub_le_iff_left, add_assoc, ← tsub_le_iff_left, ← tsub_le_iff_left]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝ b✝ c✝ d a b c : α
⊢ a - (b + c) = a - c - b
[PROOFSTEP]
rw [add_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝ b✝ c✝ d a b c : α
⊢ a - (c + b) = a - c - b
[PROOFSTEP]
apply tsub_add_eq_tsub_tsub
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
⊢ a - b - c = a - c - b
[PROOFSTEP]
rw [← tsub_add_eq_tsub_tsub, tsub_add_eq_tsub_tsub_swap]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
h : a = c + b
⊢ c ≤ a - b
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
h : a = c + b
⊢ c ≤ c + b - b
[PROOFSTEP]
exact hb.le_add_tsub
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
h : a = b + c
⊢ a = c + b
[PROOFSTEP]
rw [add_comm, h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
⊢ a + b = a + b
[PROOFSTEP]
rw [add_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
h : a - b < c
⊢ a < b + c
[PROOFSTEP]
rw [lt_iff_le_and_ne, ← tsub_le_iff_left]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
h : a - b < c
⊢ a - b ≤ c ∧ a ≠ b + c
[PROOFSTEP]
refine' ⟨h.le, _⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
h : a - b < c
⊢ a ≠ b + c
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b c d : α
hb : AddLECancellable b
h : b + c - b < c
⊢ False
[PROOFSTEP]
simp [hb] at h
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hc : AddLECancellable c
h : a - c < b
⊢ a < b + c
[PROOFSTEP]
rw [lt_iff_le_and_ne, ← tsub_le_iff_right]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hc : AddLECancellable c
h : a - c < b
⊢ a - c ≤ b ∧ a ≠ b + c
[PROOFSTEP]
refine' ⟨h.le, _⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hc : AddLECancellable c
h : a - c < b
⊢ a ≠ b + c
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b c d : α
hc : AddLECancellable c
h : b + c - c < b
⊢ False
[PROOFSTEP]
simp [hc] at h
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hc : AddLECancellable c
h : a + c < b
⊢ a ≠ b - c
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b c d : α
hc : AddLECancellable c
h : b - c + c < b
⊢ False
[PROOFSTEP]
exact h.not_le le_tsub_add
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
ha : AddLECancellable a
h : a + c < b
⊢ c + a < b
[PROOFSTEP]
rwa [add_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
a✝ b✝ c✝ d : α
inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a c b : α
⊢ a + c - (b + c) = a - b
[PROOFSTEP]
refine' add_tsub_add_le_tsub_right.antisymm (tsub_le_iff_right.2 <| le_of_add_le_add_right _)
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
a✝ b✝ c✝ d : α
inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a c b : α
⊢ α
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
a✝ b✝ c✝ d : α
inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a c b : α
⊢ a + ?refine'_1 ≤ a + c - (b + c) + b + ?refine'_1
[PROOFSTEP]
exact c
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
a✝ b✝ c✝ d : α
inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a c b : α
⊢ a + c ≤ a + c - (b + c) + b + c
[PROOFSTEP]
rw [add_assoc]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
a✝ b✝ c✝ d : α
inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a c b : α
⊢ a + c ≤ a + c - (b + c) + (b + c)
[PROOFSTEP]
exact le_tsub_add
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
a✝ b✝ c✝ d : α
inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ a + b - (a + c) = b - c
[PROOFSTEP]
rw [add_comm a b, add_comm a c, add_tsub_add_eq_tsub_right]