[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
h : a ≤ b
⊢ a + (b - a) = b
[PROOFSTEP]
refine' le_antisymm _ le_add_tsub
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
h : a ≤ b
⊢ a + (b - a) ≤ b
[PROOFSTEP]
obtain ⟨c, rfl⟩ := exists_add_of_le h
[GOAL]
case intro
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a c✝ d c : α
h : a ≤ a + c
⊢ a + (a + c - a) ≤ a + c
[PROOFSTEP]
exact add_le_add_left add_tsub_le_left a
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
h : a ≤ b
⊢ b - a + a = b
[PROOFSTEP]
rw [add_comm]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
h : a ≤ b
⊢ a + (b - a) = b
[PROOFSTEP]
exact add_tsub_cancel_of_le h
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
h : c ≤ b
⊢ a - c ≤ b - c ↔ a ≤ b
[PROOFSTEP]
rw [tsub_le_iff_right, tsub_add_cancel_of_le h]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
h1 : c ≤ a
h2 : c ≤ b
⊢ a - c = b - c ↔ a = b
[PROOFSTEP]
simp_rw [le_antisymm_iff, tsub_le_tsub_iff_right h1, tsub_le_tsub_iff_right h2]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
h : c ≤ b
h2 : a - c < b - c
⊢ a < b
[PROOFSTEP]
refine' ((tsub_le_tsub_iff_right h).mp h2.le).lt_of_ne _
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
h : c ≤ b
h2 : a - c < b - c
⊢ a ≠ b
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a c d : α
h : c ≤ a
h2 : a - c < a - c
⊢ False
[PROOFSTEP]
exact h2.false
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hab : b ≤ a
hcb : c ≤ b
⊢ a - b + (b - c) = a - c
[PROOFSTEP]
convert tsub_add_cancel_of_le (tsub_le_tsub_right hab c) using 2
[GOAL]
case h.e'_2.h.e'_5
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hab : b ≤ a
hcb : c ≤ b
⊢ a - b = a - c - (b - c)
[PROOFSTEP]
rw [tsub_tsub, add_tsub_cancel_of_le hcb]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
h : c ≤ b
⊢ a - c - (b - c) = a - b
[PROOFSTEP]
rw [tsub_tsub, add_tsub_cancel_of_le h]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hc : AddLECancellable c
h : c ≤ b
⊢ a = b - c → a + c = b
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
b c d : α
hc : AddLECancellable c
h : c ≤ b
⊢ b - c + c = b
[PROOFSTEP]
exact tsub_add_cancel_of_le h
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
h : b ≤ a
⊢ a - b = c ↔ a = c + b
[PROOFSTEP]
rw [eq_comm, hb.eq_tsub_iff_add_eq_of_le h, eq_comm]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝ b c d : α
hc : AddLECancellable c
h : c ≤ b
a : α
⊢ a + b - c = a + (b - c)
[PROOFSTEP]
conv_lhs => rw [← add_tsub_cancel_of_le h, add_comm c, ← add_assoc, hc.add_tsub_cancel_right]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝ b c d : α
hc : AddLECancellable c
h : c ≤ b
a : α
| a + b - c
[PROOFSTEP]
rw [← add_tsub_cancel_of_le h, add_comm c, ← add_assoc, hc.add_tsub_cancel_right]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝ b c d : α
hc : AddLECancellable c
h : c ≤ b
a : α
| a + b - c
[PROOFSTEP]
rw [← add_tsub_cancel_of_le h, add_comm c, ← add_assoc, hc.add_tsub_cancel_right]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝ b c d : α
hc : AddLECancellable c
h : c ≤ b
a : α
| a + b - c
[PROOFSTEP]
rw [← add_tsub_cancel_of_le h, add_comm c, ← add_assoc, hc.add_tsub_cancel_right]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
h : b ≤ a
⊢ a - b + c = a + c - b
[PROOFSTEP]
rw [add_comm a, hb.add_tsub_assoc_of_le h, add_comm]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hbc : AddLECancellable (b - c)
h₁ : b ≤ a
h₂ : c ≤ b
⊢ a = a - b + c + (b - c)
[PROOFSTEP]
rw [add_assoc, add_tsub_cancel_of_le h₂, tsub_add_cancel_of_le h₁]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
hd : AddLECancellable d
hba : b ≤ a
hdc : d ≤ c
⊢ a - b + (c - d) = a + c - (b + d)
[PROOFSTEP]
rw [hb.tsub_add_eq_add_tsub hba, ← hd.add_tsub_assoc_of_le hdc, tsub_tsub, add_comm d]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
ha : AddLECancellable a
h : a ≤ c
⊢ b ≤ c - a ↔ b + a ≤ c
[PROOFSTEP]
rw [add_comm]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
ha : AddLECancellable a
h : a ≤ c
⊢ b ≤ c - a ↔ a + b ≤ c
[PROOFSTEP]
exact ha.le_tsub_iff_left h
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
hba : b ≤ a
⊢ a - b < c ↔ a < b + c
[PROOFSTEP]
refine' ⟨hb.lt_add_of_tsub_lt_left, _⟩
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
hba : b ≤ a
⊢ a < b + c → a - b < c
[PROOFSTEP]
intro h
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
hba : b ≤ a
h : a < b + c
⊢ a - b < c
[PROOFSTEP]
refine' (tsub_le_iff_left.mpr h.le).lt_of_ne _
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
hba : b ≤ a
h : a < b + c
⊢ a - b ≠ c
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b d : α
hb : AddLECancellable b
hba : b ≤ a
h : a < b + (a - b)
⊢ False
[PROOFSTEP]
exact h.ne' (add_tsub_cancel_of_le hba)
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
hba : b ≤ a
⊢ a - b < c ↔ a < c + b
[PROOFSTEP]
rw [add_comm]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
hba : b ≤ a
⊢ a - b < c ↔ a < b + c
[PROOFSTEP]
exact hb.tsub_lt_iff_left hba
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
hc : AddLECancellable c
h₁ : b ≤ a
h₂ : c ≤ a
⊢ a - b < c ↔ a - c < b
[PROOFSTEP]
rw [hb.tsub_lt_iff_left h₁, hc.tsub_lt_iff_right h₂]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
ha : AddLECancellable a
hc : AddLECancellable c
h₁ : a ≤ b
h₂ : c ≤ b
⊢ a ≤ b - c ↔ c ≤ b - a
[PROOFSTEP]
rw [ha.le_tsub_iff_left h₁, hc.le_tsub_iff_right h₂]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hc : AddLECancellable c
h : c ≤ b
⊢ a < b - c ↔ a + c < b
[PROOFSTEP]
refine' ⟨fun h' => (add_le_of_le_tsub_right_of_le h h'.le).lt_of_ne _, hc.lt_tsub_of_add_lt_right⟩
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hc : AddLECancellable c
h : c ≤ b
h' : a < b - c
⊢ a + c ≠ b
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a c d : α
hc : AddLECancellable c
h : c ≤ a + c
h' : a < a + c - c
⊢ False
[PROOFSTEP]
exact h'.ne' hc.add_tsub_cancel_right
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hc : AddLECancellable c
h : c ≤ b
⊢ a < b - c ↔ c + a < b
[PROOFSTEP]
rw [add_comm]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hc : AddLECancellable c
h : c ≤ b
⊢ a < b - c ↔ a + c < b
[PROOFSTEP]
exact hc.lt_tsub_iff_right_of_le h
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hab : AddLECancellable (a - b)
h₁ : b ≤ a
h₂ : c ≤ a
h₃ : a - b = a - c
⊢ b = c
[PROOFSTEP]
rw [← hab.inj]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hab : AddLECancellable (a - b)
h₁ : b ≤ a
h₂ : c ≤ a
h₃ : a - b = a - c
⊢ a - b + b = a - b + c
[PROOFSTEP]
rw [tsub_add_cancel_of_le h₁, h₃, tsub_add_cancel_of_le h₂]
[GOAL]
α : Type u_1
inst✝⁶ : AddCommSemigroup α
inst✝⁵ : PartialOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
hb : AddLECancellable b
hca : c ≤ a
h : a - b < a - c
⊢ c < b
[PROOFSTEP]
conv_lhs at h => rw [← tsub_add_cancel_of_le hca]
[GOAL]
α : Type u_1
inst✝⁶ : AddCommSemigroup α
inst✝⁵ : PartialOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
hb : AddLECancellable b
hca : c ≤ a
h : a - b < a - c
| a - b
[PROOFSTEP]
rw [← tsub_add_cancel_of_le hca]
[GOAL]
α : Type u_1
inst✝⁶ : AddCommSemigroup α
inst✝⁵ : PartialOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
hb : AddLECancellable b
hca : c ≤ a
h : a - b < a - c
| a - b
[PROOFSTEP]
rw [← tsub_add_cancel_of_le hca]
[GOAL]
α : Type u_1
inst✝⁶ : AddCommSemigroup α
inst✝⁵ : PartialOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
hb : AddLECancellable b
hca : c ≤ a
h : a - b < a - c
| a - b
[PROOFSTEP]
rw [← tsub_add_cancel_of_le hca]
[GOAL]
α : Type u_1
inst✝⁶ : AddCommSemigroup α
inst✝⁵ : PartialOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
hb : AddLECancellable b
hca : c ≤ a
h : a - c + c - b < a - c
⊢ c < b
[PROOFSTEP]
exact lt_of_add_lt_add_left (hb.lt_add_of_tsub_lt_right h)
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hc : AddLECancellable c
h : c ≤ a
h2 : a < b
⊢ a - c < b - c
[PROOFSTEP]
apply hc.lt_tsub_of_add_lt_left
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hc : AddLECancellable c
h : c ≤ a
h2 : a < b
⊢ c + (a - c) < b
[PROOFSTEP]
rwa [add_tsub_cancel_of_le h]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hac : AddLECancellable (a - c)
h : c ≤ a
⊢ a + b = b + c + (a - c)
[PROOFSTEP]
rw [add_assoc, add_tsub_cancel_of_le h, add_comm]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hab : AddLECancellable (a - b)
h : b ≤ a
⊢ a - c - (a - b) = b - c
[PROOFSTEP]
rw [tsub_right_comm, hab.tsub_tsub_cancel_of_le h]
[GOAL]
α : Type u_1
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
⊢ b - a + a = b ↔ a ≤ b
[PROOFSTEP]
rw [add_comm]
[GOAL]
α : Type u_1
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
⊢ a + (b - a) = b ↔ a ≤ b
[PROOFSTEP]
exact add_tsub_cancel_iff_le
[GOAL]
α : Type u_1
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
⊢ a - b = 0 ↔ a ≤ b
[PROOFSTEP]
rw [← nonpos_iff_eq_zero, tsub_le_iff_left, add_zero]
[GOAL]
α : Type u_1
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
⊢ 0 < a - b ↔ ¬a ≤ b
[PROOFSTEP]
rw [pos_iff_ne_zero, Ne.def, tsub_eq_zero_iff_le]
[GOAL]
α : Type u_1
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
ha : AddLECancellable a
hc : AddLECancellable c
h : c ≤ a
⊢ a - b ≤ a - c ↔ c ≤ b
[PROOFSTEP]
refine' ⟨_, fun h => tsub_le_tsub_left h a⟩
[GOAL]
α : Type u_1
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
ha : AddLECancellable a
hc : AddLECancellable c
h : c ≤ a
⊢ a - b ≤ a - c → c ≤ b
[PROOFSTEP]
rw [tsub_le_iff_left, ← hc.add_tsub_assoc_of_le h, hc.le_tsub_iff_right (h.trans le_add_self), add_comm b]
[GOAL]
α : Type u_1
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
ha : AddLECancellable a
hc : AddLECancellable c
h : c ≤ a
⊢ a + c ≤ a + b → c ≤ b
[PROOFSTEP]
apply ha
[GOAL]
α : Type u_1
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
ha : AddLECancellable a
hb : AddLECancellable b
hc : AddLECancellable c
hba : b ≤ a
hca : c ≤ a
⊢ a - b = a - c ↔ b = c
[PROOFSTEP]
simp_rw [le_antisymm_iff, ha.tsub_le_tsub_iff_left hb hba, ha.tsub_le_tsub_iff_left hc hca, and_comm]
[GOAL]
α : Type u_1
inst✝³ : CanonicallyOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ AddCommMonoid α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
inst✝³ : CanonicallyOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a✝ b✝ c✝ d : α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
src✝ : AddCommMonoid α := inferInstance
a b c : α
h : a + b = a + c
⊢ b = c
[PROOFSTEP]
simpa only [add_tsub_cancel_left] using congr_arg (fun x => x - a) h
[GOAL]
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
⊢ 0 < a - b ↔ b < a
[PROOFSTEP]
rw [tsub_pos_iff_not_le, not_le]
[GOAL]
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝ b✝ c d a b : α
⊢ a - b = a - min a b
[PROOFSTEP]
cases' le_total a b with h h
[GOAL]
case inl
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝ b✝ c d a b : α
h : a ≤ b
⊢ a - b = a - min a b
[PROOFSTEP]
rw [min_eq_left h, tsub_self, tsub_eq_zero_of_le h]
[GOAL]
case inr
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝ b✝ c d a b : α
h : b ≤ a
⊢ a - b = a - min a b
[PROOFSTEP]
rw [min_eq_right h]
[GOAL]
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hc : AddLECancellable c
h : c ≤ a
⊢ a - c < b - c ↔ a < b
[PROOFSTEP]
rw [hc.lt_tsub_iff_left, add_tsub_cancel_of_le h]
[GOAL]
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
ha : AddLECancellable a
h₁ : 0 < a
h₂ : 0 < b
⊢ a - b < a
[PROOFSTEP]
refine' tsub_le_self.lt_of_ne fun h => _
[GOAL]
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
ha : AddLECancellable a
h₁ : 0 < a
h₂ : 0 < b
h : a - b = a
⊢ False
[PROOFSTEP]
rw [← h, tsub_pos_iff_lt] at h₁
[GOAL]
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
ha : AddLECancellable a
h₁ : b < a
h₂ : 0 < b
h : a - b = a
⊢ False
[PROOFSTEP]
exact h₂.not_le (ha.add_le_iff_nonpos_left.1 <| add_le_of_le_tsub_left_of_le h₁.le h.ge)
[GOAL]
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
ha : AddLECancellable a
⊢ a - b < a ↔ 0 < a ∧ 0 < b
[PROOFSTEP]
refine' ⟨fun h => ⟨(zero_le _).trans_lt h, (zero_le b).lt_of_ne _⟩, fun h => ha.tsub_lt_self h.1 h.2⟩
[GOAL]
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
ha : AddLECancellable a
h : a - b < a
⊢ 0 ≠ b
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a c d : α
ha : AddLECancellable a
h : a - 0 < a
⊢ False
[PROOFSTEP]
rw [tsub_zero] at h
[GOAL]
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a c d : α
ha : AddLECancellable a
h : a < a
⊢ False
[PROOFSTEP]
exact h.false
[GOAL]
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
⊢ a - b + b = max a b
[PROOFSTEP]
cases' le_total a b with h h
[GOAL]
case inl
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
h : a ≤ b
⊢ a - b + b = max a b
[PROOFSTEP]
rw [max_eq_right h, tsub_eq_zero_of_le h, zero_add]
[GOAL]
case inr
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
h : b ≤ a
⊢ a - b + b = max a b
[PROOFSTEP]
rw [max_eq_left h, tsub_add_cancel_of_le h]
[GOAL]
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
⊢ a + (b - a) = max a b
[PROOFSTEP]
rw [add_comm, max_comm, tsub_add_eq_max]
[GOAL]
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
⊢ a - min a b = a - b
[PROOFSTEP]
cases' le_total a b with h h
[GOAL]
case inl
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
h : a ≤ b
⊢ a - min a b = a - b
[PROOFSTEP]
rw [min_eq_left h, tsub_self, tsub_eq_zero_of_le h]
[GOAL]
case inr
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
h : b ≤ a
⊢ a - min a b = a - b
[PROOFSTEP]
rw [min_eq_right h]
[GOAL]
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
⊢ a - b + min a b = a
[PROOFSTEP]
rw [← tsub_min, @tsub_add_cancel_of_le]
[GOAL]
case h
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
⊢ min a b ≤ a
[PROOFSTEP]
apply min_le_left


[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
src✝¹ : LinearOrderedAddCommMonoidWithTop (WithTop α) := linearOrderedAddCommMonoidWithTop
src✝ : Nontrivial (Option α) := Option.nontrivial
⊢ ∀ (a : WithTop α), a ≠ ⊤ → a + -a = 0
[PROOFSTEP]
rintro (a | a) ha
[GOAL]
case none
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
src✝¹ : LinearOrderedAddCommMonoidWithTop (WithTop α) := linearOrderedAddCommMonoidWithTop
src✝ : Nontrivial (Option α) := Option.nontrivial
ha : none ≠ ⊤
⊢ none + -none = 0
[PROOFSTEP]
exact (ha rfl).elim
[GOAL]
case some
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b c d : α
src✝¹ : LinearOrderedAddCommMonoidWithTop (WithTop α) := linearOrderedAddCommMonoidWithTop
src✝ : Nontrivial (Option α) := Option.nontrivial
a : α
ha : Option.some a ≠ ⊤
⊢ Option.some a + -Option.some a = 0
[PROOFSTEP]
exact WithTop.coe_add.symm.trans (WithTop.coe_eq_coe.2 (add_neg_self a))


[GOAL]
α : Type u_1
inst✝¹ : AddGroup α
inst✝ : LinearOrder α
a : α
⊢ |(-a)| = |a|
[PROOFSTEP]
rw [abs_eq_max_neg, max_comm, neg_neg, abs_eq_max_neg]
[GOAL]
α : Type u_1
inst✝¹ : AddGroup α
inst✝ : LinearOrder α
a b : α
h : |a| = b
⊢ a = b ∨ a = -b
[PROOFSTEP]
simpa only [← h, eq_comm (a := |a|), neg_eq_iff_eq_neg] using abs_choice a
[GOAL]
α : Type u_1
inst✝¹ : AddGroup α
inst✝ : LinearOrder α
a b : α
⊢ |a| = |b| ↔ a = b ∨ a = -b
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
α : Type u_1
inst✝¹ : AddGroup α
inst✝ : LinearOrder α
a b : α
h : |a| = |b|
⊢ a = b ∨ a = -b
[PROOFSTEP]
obtain rfl | rfl := eq_or_eq_neg_of_abs_eq h
[GOAL]
case refine'_1.inl
α : Type u_1
inst✝¹ : AddGroup α
inst✝ : LinearOrder α
b : α
h : |(|b|)| = |b|
⊢ |b| = b ∨ |b| = -b
[PROOFSTEP]
simpa only [neg_eq_iff_eq_neg (a := |b|), neg_inj, or_comm] using abs_choice b
[GOAL]
case refine'_1.inr
α : Type u_1
inst✝¹ : AddGroup α
inst✝ : LinearOrder α
b : α
h : |(-|b|)| = |b|
⊢ -|b| = b ∨ -|b| = -b
[PROOFSTEP]
simpa only [neg_eq_iff_eq_neg (a := |b|), neg_inj, or_comm] using abs_choice b
[GOAL]
case refine'_2
α : Type u_1
inst✝¹ : AddGroup α
inst✝ : LinearOrder α
a b : α
h : a = b ∨ a = -b
⊢ |a| = |b|
[PROOFSTEP]
cases' h with h h
[GOAL]
case refine'_2.inl
α : Type u_1
inst✝¹ : AddGroup α
inst✝ : LinearOrder α
a b : α
h : a = b
⊢ |a| = |b|
[PROOFSTEP]
simp [h, abs_neg]
[GOAL]
case refine'_2.inr
α : Type u_1
inst✝¹ : AddGroup α
inst✝ : LinearOrder α
a b : α
h : a = -b
⊢ |a| = |b|
[PROOFSTEP]
simp [h, abs_neg]
[GOAL]
α : Type u_1
inst✝² : AddGroup α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b c : α
ha : 0 ≤ a
hab : a ≤ b
⊢ |a| ≤ |b|
[PROOFSTEP]
rwa [abs_of_nonneg ha, abs_of_nonneg (ha.trans hab)]
[GOAL]
α : Type u_1
inst✝² : AddGroup α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ 0 < |a| ↔ a ≠ 0
[PROOFSTEP]
rcases lt_trichotomy a 0 with (ha | rfl | ha)
[GOAL]
case inl
α : Type u_1
inst✝² : AddGroup α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b c : α
ha : a < 0
⊢ 0 < |a| ↔ a ≠ 0
[PROOFSTEP]
simp [abs_of_neg ha, neg_pos, ha.ne, ha]
[GOAL]
case inr.inl
α : Type u_1
inst✝² : AddGroup α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b c : α
⊢ 0 < |0| ↔ 0 ≠ 0
[PROOFSTEP]
simp
[GOAL]
case inr.inr
α : Type u_1
inst✝² : AddGroup α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b c : α
ha : 0 < a
⊢ 0 < |a| ↔ a ≠ 0
[PROOFSTEP]
simp [abs_of_pos ha, ha, ha.ne.symm]
[GOAL]
α : Type u_1
inst✝² : AddGroup α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a✝ b c a : α
⊢ -|a| ≤ a
[PROOFSTEP]
cases' le_total 0 a with h h
[GOAL]
case inl
α : Type u_1
inst✝² : AddGroup α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a✝ b c a : α
h : 0 ≤ a
⊢ -|a| ≤ a
[PROOFSTEP]
calc
  -|a| = -a := congr_arg Neg.neg (abs_of_nonneg h)
  _ ≤ 0 := (neg_nonpos.mpr h)
  _ ≤ a := h
[GOAL]
case inr
α : Type u_1
inst✝² : AddGroup α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a✝ b c a : α
h : a ≤ 0
⊢ -|a| ≤ a
[PROOFSTEP]
calc
  -|a| = - -a := congr_arg Neg.neg (abs_of_nonpos h)
  _ ≤ a := (neg_neg a).le
[GOAL]
α : Type u_1
inst✝² : AddGroup α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a✝ b c a : α
⊢ 0 ≤ a + |a|
[PROOFSTEP]
rw [← add_right_neg a]
[GOAL]
α : Type u_1
inst✝² : AddGroup α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a✝ b c a : α
⊢ a + -a ≤ a + |a|
[PROOFSTEP]
apply add_le_add_left
[GOAL]
case bc
α : Type u_1
inst✝² : AddGroup α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a✝ b c a : α
⊢ -a ≤ |a|
[PROOFSTEP]
exact neg_le_abs_self a
[GOAL]
α : Type u_1
inst✝² : AddGroup α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a✝ b c a : α
⊢ -|a| ≤ -a
[PROOFSTEP]
simpa using neg_abs_le_self (-a)
[GOAL]
α : Type u_1
inst✝³ : AddGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b c : α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
ha : a ≤ 0
hab : b ≤ a
⊢ |a| ≤ |b|
[PROOFSTEP]
rw [abs_of_nonpos ha, abs_of_nonpos (hab.trans ha)]
[GOAL]
α : Type u_1
inst✝³ : AddGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b c : α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
ha : a ≤ 0
hab : b ≤ a
⊢ -a ≤ -b
[PROOFSTEP]
exact neg_le_neg_iff.mpr hab
[GOAL]
α : Type u_1
inst✝³ : AddGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b c : α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ -a < b ∧ a < b ↔ -b < a ∧ a < b
[PROOFSTEP]
rw [neg_lt]
[GOAL]
α : Type u_1
inst✝³ : AddGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a✝ b✝ c : α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ max a b - min a b = |a - b|
[PROOFSTEP]
cases' le_total a b with ab ba
[GOAL]
case inl
α : Type u_1
inst✝³ : AddGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a✝ b✝ c : α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
ab : a ≤ b
⊢ max a b - min a b = |a - b|
[PROOFSTEP]
rw [max_eq_right ab, min_eq_left ab, abs_of_nonpos, neg_sub]
[GOAL]
case inl
α : Type u_1
inst✝³ : AddGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a✝ b✝ c : α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
ab : a ≤ b
⊢ a - b ≤ 0
[PROOFSTEP]
rwa [sub_nonpos]
[GOAL]
case inr
α : Type u_1
inst✝³ : AddGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a✝ b✝ c : α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
ba : b ≤ a
⊢ max a b - min a b = |a - b|
[PROOFSTEP]
rw [max_eq_left ba, min_eq_right ba, abs_of_nonneg]
[GOAL]
case inr
α : Type u_1
inst✝³ : AddGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a✝ b✝ c : α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
ba : b ≤ a
⊢ 0 ≤ a - b
[PROOFSTEP]
rwa [sub_nonneg]
[GOAL]
α : Type u_1
inst✝³ : AddGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a✝ b✝ c : α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ max a b - min a b = |b - a|
[PROOFSTEP]
rw [abs_sub_comm]
[GOAL]
α : Type u_1
inst✝³ : AddGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a✝ b✝ c : α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ max a b - min a b = |a - b|
[PROOFSTEP]
exact max_sub_min_eq_abs' _ _
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ |a| ≤ b ↔ -b ≤ a ∧ a ≤ b
[PROOFSTEP]
rw [abs_le', and_comm, @neg_le α]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ a ≤ |b| ↔ b ≤ -a ∨ a ≤ b
[PROOFSTEP]
rw [le_abs, or_comm, @le_neg α]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c d a b : α
⊢ |a| ≤ |b| + |b + a|
[PROOFSTEP]
simpa using abs_add (-b) (b + a)
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c d a b : α
⊢ |a - b| ≤ |a| + |b|
[PROOFSTEP]
rw [sub_eq_add_neg, ← abs_neg b]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c d a b : α
⊢ |a + -b| ≤ |a| + |(-b)|
[PROOFSTEP]
exact abs_add a _
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ |a - b| ≤ c ↔ a - b ≤ c ∧ b - a ≤ c
[PROOFSTEP]
rw [abs_le, neg_le_sub_iff_le_add, sub_le_iff_le_add', and_comm, sub_le_iff_le_add']
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ |a - b| < c ↔ a - b < c ∧ b - a < c
[PROOFSTEP]
rw [@abs_lt α, neg_lt_sub_iff_lt_add', sub_lt_iff_lt_add', and_comm, sub_lt_iff_lt_add']
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c d a b : α
⊢ |a| = |a - b + b|
[PROOFSTEP]
rw [sub_add_cancel]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c d a b : α
⊢ |b| - |a| ≤ |a - b|
[PROOFSTEP]
rw [abs_sub_comm]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c d a b : α
⊢ |b| - |a| ≤ |b - a|
[PROOFSTEP]
apply abs_sub_abs_le_abs_sub
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
hb : 0 ≤ b
⊢ |a| = b ↔ a = b ∨ a = -b
[PROOFSTEP]
refine' ⟨eq_or_eq_neg_of_abs_eq, _⟩
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
hb : 0 ≤ b
⊢ a = b ∨ a = -b → |a| = b
[PROOFSTEP]
rintro (rfl | rfl)
[GOAL]
case inl
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a c d : α
hb : 0 ≤ a
⊢ |a| = a
[PROOFSTEP]
simp only [abs_neg, abs_of_nonneg hb]
[GOAL]
case inr
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
b c d : α
hb : 0 ≤ b
⊢ |(-b)| = b
[PROOFSTEP]
simp only [abs_neg, abs_of_nonneg hb]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
hab : a ≤ b
hbc : b ≤ c
⊢ b ≤ max |a| |c|
[PROOFSTEP]
simp [hbc.trans (le_abs_self c)]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
hab : a ≤ b
hbc : b ≤ c
⊢ -b ≤ max |a| |c|
[PROOFSTEP]
simp [((@neg_le_neg_iff α ..).mpr hab).trans (neg_le_abs_self a)]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c✝ d a b c : α
⊢ |a - c| = |a - b + (b - c)|
[PROOFSTEP]
rw [sub_add_sub_cancel]


[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommMonoid α
s : Interval α
⊢ Option.map (fun b => NonemptyInterval.pure 1 * b) s = s
[PROOFSTEP]
simp_rw [NonemptyInterval.pure_one, one_mul, ← id_def, Option.map_id, id]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommMonoid α
s : Interval α
⊢ Option.map (fun a => a * NonemptyInterval.pure 1) s = s
[PROOFSTEP]
simp_rw [NonemptyInterval.pure_one, mul_one, ← id_def, Option.map_id, id]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
⊢ s * t = 1 ↔ ∃ a b, s = pure a ∧ t = pure b ∧ a * b = 1
[PROOFSTEP]
refine' ⟨fun h => _, _⟩
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
h : s * t = 1
⊢ ∃ a b, s = pure a ∧ t = pure b ∧ a * b = 1
[PROOFSTEP]
rw [ext_iff, Prod.ext_iff] at h
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
h : (s * t).fst = 1.fst ∧ (s * t).snd = 1.snd
⊢ ∃ a b, s = pure a ∧ t = pure b ∧ a * b = 1
[PROOFSTEP]
have := (mul_le_mul_iff_of_ge s.fst_le_snd t.fst_le_snd).1 (h.2.trans h.1.symm).le
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
h : (s * t).fst = 1.fst ∧ (s * t).snd = 1.snd
this : s.fst = s.snd ∧ t.fst = t.snd
⊢ ∃ a b, s = pure a ∧ t = pure b ∧ a * b = 1
[PROOFSTEP]
refine' ⟨s.fst, t.fst, _, _, h.1⟩
[GOAL]
case refine'_1.refine'_1
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
h : (s * t).fst = 1.fst ∧ (s * t).snd = 1.snd
this : s.fst = s.snd ∧ t.fst = t.snd
⊢ s = pure s.fst
[PROOFSTEP]
apply NonemptyInterval.ext
[GOAL]
case refine'_1.refine'_2
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
h : (s * t).fst = 1.fst ∧ (s * t).snd = 1.snd
this : s.fst = s.snd ∧ t.fst = t.snd
⊢ t = pure t.fst
[PROOFSTEP]
apply NonemptyInterval.ext
[GOAL]
case refine'_1.refine'_1.h
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
h : (s * t).fst = 1.fst ∧ (s * t).snd = 1.snd
this : s.fst = s.snd ∧ t.fst = t.snd
⊢ s.toProd = (pure s.fst).toProd
[PROOFSTEP]
dsimp [pure]
[GOAL]
case refine'_1.refine'_2.h
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
h : (s * t).fst = 1.fst ∧ (s * t).snd = 1.snd
this : s.fst = s.snd ∧ t.fst = t.snd
⊢ t.toProd = (pure t.fst).toProd
[PROOFSTEP]
dsimp [pure]
[GOAL]
case refine'_1.refine'_1.h
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
h : (s * t).fst = 1.fst ∧ (s * t).snd = 1.snd
this : s.fst = s.snd ∧ t.fst = t.snd
⊢ s.toProd = (s.fst, s.fst)
[PROOFSTEP]
nth_rw 2 [this.1]
[GOAL]
case refine'_1.refine'_2.h
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
h : (s * t).fst = 1.fst ∧ (s * t).snd = 1.snd
this : s.fst = s.snd ∧ t.fst = t.snd
⊢ t.toProd = (t.fst, t.fst)
[PROOFSTEP]
nth_rw 2 [this.2]
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
⊢ (∃ a b, s = pure a ∧ t = pure b ∧ a * b = 1) → s * t = 1
[PROOFSTEP]
rintro ⟨b, c, rfl, rfl, h⟩
[GOAL]
case refine'_2.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
b c : α
h : b * c = 1
⊢ pure b * pure c = 1
[PROOFSTEP]
rw [pure_mul_pure, h, pure_one]
[GOAL]
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s✝ t✝ : NonemptyInterval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (NonemptyInterval α) := addCommMonoid
s t : NonemptyInterval α
⊢ s - t = s + -t
[PROOFSTEP]
refine NonemptyInterval.ext _ _ (Prod.ext ?_ ?_)
[GOAL]
case refine_1
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s✝ t✝ : NonemptyInterval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (NonemptyInterval α) := addCommMonoid
s t : NonemptyInterval α
⊢ (s - t).fst = (s + -t).fst
[PROOFSTEP]
exact sub_eq_add_neg _ _
[GOAL]
case refine_2
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s✝ t✝ : NonemptyInterval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (NonemptyInterval α) := addCommMonoid
s t : NonemptyInterval α
⊢ (s - t).snd = (s + -t).snd
[PROOFSTEP]
exact sub_eq_add_neg _ _
[GOAL]
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s✝ t : NonemptyInterval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (NonemptyInterval α) := addCommMonoid
s : NonemptyInterval α
⊢ - -s = s
[PROOFSTEP]
apply NonemptyInterval.ext
[GOAL]
case h
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s✝ t : NonemptyInterval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (NonemptyInterval α) := addCommMonoid
s : NonemptyInterval α
⊢ (- -s).toProd = s.toProd
[PROOFSTEP]
exact neg_neg _
[GOAL]
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s✝ t✝ : NonemptyInterval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (NonemptyInterval α) := addCommMonoid
s t : NonemptyInterval α
⊢ -(s + t) = -t + -s
[PROOFSTEP]
refine NonemptyInterval.ext _ _ (Prod.ext ?_ ?_)
[GOAL]
case refine_1
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s✝ t✝ : NonemptyInterval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (NonemptyInterval α) := addCommMonoid
s t : NonemptyInterval α
⊢ (-(s + t)).fst = (-t + -s).fst
[PROOFSTEP]
exact neg_add_rev _ _
[GOAL]
case refine_2
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s✝ t✝ : NonemptyInterval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (NonemptyInterval α) := addCommMonoid
s t : NonemptyInterval α
⊢ (-(s + t)).snd = (-t + -s).snd
[PROOFSTEP]
exact neg_add_rev _ _
[GOAL]
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s✝ t✝ : NonemptyInterval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (NonemptyInterval α) := addCommMonoid
s t : NonemptyInterval α
h : s + t = 0
⊢ -s = t
[PROOFSTEP]
obtain ⟨a, b, rfl, rfl, hab⟩ := NonemptyInterval.add_eq_zero_iff.1 h
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s t : NonemptyInterval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (NonemptyInterval α) := addCommMonoid
a b : α
hab : a + b = 0
h : pure a + pure b = 0
⊢ -pure a = pure b
[PROOFSTEP]
rw [neg_pure, neg_eq_of_add_eq_zero_right hab]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s✝ t✝ : NonemptyInterval α
src✝ : CommMonoid (NonemptyInterval α) := commMonoid
s t : NonemptyInterval α
⊢ s / t = s * t⁻¹
[PROOFSTEP]
refine NonemptyInterval.ext _ _ (Prod.ext ?_ ?_)
[GOAL]
case refine_1
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s✝ t✝ : NonemptyInterval α
src✝ : CommMonoid (NonemptyInterval α) := commMonoid
s t : NonemptyInterval α
⊢ (s / t).fst = (s * t⁻¹).fst
[PROOFSTEP]
exact div_eq_mul_inv _ _
[GOAL]
case refine_2
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s✝ t✝ : NonemptyInterval α
src✝ : CommMonoid (NonemptyInterval α) := commMonoid
s t : NonemptyInterval α
⊢ (s / t).snd = (s * t⁻¹).snd
[PROOFSTEP]
exact div_eq_mul_inv _ _
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s✝ t : NonemptyInterval α
src✝ : CommMonoid (NonemptyInterval α) := commMonoid
s : NonemptyInterval α
⊢ s⁻¹⁻¹ = s
[PROOFSTEP]
apply NonemptyInterval.ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s✝ t : NonemptyInterval α
src✝ : CommMonoid (NonemptyInterval α) := commMonoid
s : NonemptyInterval α
⊢ s⁻¹⁻¹.toProd = s.toProd
[PROOFSTEP]
exact inv_inv _
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s✝ t✝ : NonemptyInterval α
src✝ : CommMonoid (NonemptyInterval α) := commMonoid
s t : NonemptyInterval α
⊢ (s * t)⁻¹ = t⁻¹ * s⁻¹
[PROOFSTEP]
refine NonemptyInterval.ext _ _ (Prod.ext ?_ ?_)
[GOAL]
case refine_1
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s✝ t✝ : NonemptyInterval α
src✝ : CommMonoid (NonemptyInterval α) := commMonoid
s t : NonemptyInterval α
⊢ (s * t)⁻¹.fst = (t⁻¹ * s⁻¹).fst
[PROOFSTEP]
exact mul_inv_rev _ _
[GOAL]
case refine_2
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s✝ t✝ : NonemptyInterval α
src✝ : CommMonoid (NonemptyInterval α) := commMonoid
s t : NonemptyInterval α
⊢ (s * t)⁻¹.snd = (t⁻¹ * s⁻¹).snd
[PROOFSTEP]
exact mul_inv_rev _ _
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s✝ t✝ : NonemptyInterval α
src✝ : CommMonoid (NonemptyInterval α) := commMonoid
s t : NonemptyInterval α
h : s * t = 1
⊢ s⁻¹ = t
[PROOFSTEP]
obtain ⟨a, b, rfl, rfl, hab⟩ := NonemptyInterval.mul_eq_one_iff.1 h
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
src✝ : CommMonoid (NonemptyInterval α) := commMonoid
a b : α
hab : a * b = 1
h : pure a * pure b = 1
⊢ (pure a)⁻¹ = pure b
[PROOFSTEP]
rw [inv_pure, inv_eq_of_mul_eq_one_right hab]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t : Interval α
⊢ s * t = 1 ↔ ∃ a b, s = pure a ∧ t = pure b ∧ a * b = 1
[PROOFSTEP]
cases s
[GOAL]
case none
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
t : Interval α
⊢ none * t = 1 ↔ ∃ a b, none = pure a ∧ t = pure b ∧ a * b = 1
[PROOFSTEP]
simp [WithBot.none_eq_bot]
[GOAL]
case some
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
t : Interval α
val✝ : NonemptyInterval α
⊢ some val✝ * t = 1 ↔ ∃ a b, some val✝ = pure a ∧ t = pure b ∧ a * b = 1
[PROOFSTEP]
cases t
[GOAL]
case some.none
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
val✝ : NonemptyInterval α
⊢ some val✝ * none = 1 ↔ ∃ a b, some val✝ = pure a ∧ none = pure b ∧ a * b = 1
[PROOFSTEP]
simp [WithBot.none_eq_bot]
[GOAL]
case some.some
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
val✝¹ val✝ : NonemptyInterval α
⊢ some val✝¹ * some val✝ = 1 ↔ ∃ a b, some val✝¹ = pure a ∧ some val✝ = pure b ∧ a * b = 1
[PROOFSTEP]
simp_rw [WithBot.some_eq_coe, ← NonemptyInterval.coe_mul_interval, ← NonemptyInterval.coe_one_interval, WithBot.coe_inj,
  NonemptyInterval.coe_eq_pure]
[GOAL]
case some.some
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
val✝¹ val✝ : NonemptyInterval α
⊢ val✝¹ * val✝ = 1 ↔ ∃ a b, val✝¹ = NonemptyInterval.pure a ∧ val✝ = NonemptyInterval.pure b ∧ a * b = 1
[PROOFSTEP]
exact NonemptyInterval.mul_eq_one_iff
[GOAL]
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s t : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
⊢ ∀ (a b : Interval α), a - b = a + -b
[PROOFSTEP]
rintro (_ | s) (_ | t)
[GOAL]
case none.none
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s t : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
⊢ none - none = none + -none
[PROOFSTEP]
first
| rfl
| exact congr_arg some (sub_eq_add_neg _ _)
[GOAL]
case none.none
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s t : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
⊢ none - none = none + -none
[PROOFSTEP]
rfl
[GOAL]
case none.some
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s t✝ : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
t : NonemptyInterval α
⊢ none - some t = none + -some t
[PROOFSTEP]
first
| rfl
| exact congr_arg some (sub_eq_add_neg _ _)
[GOAL]
case none.some
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s t✝ : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
t : NonemptyInterval α
⊢ none - some t = none + -some t
[PROOFSTEP]
rfl
[GOAL]
case some.none
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s✝ t : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
s : NonemptyInterval α
⊢ some s - none = some s + -none
[PROOFSTEP]
first
| rfl
| exact congr_arg some (sub_eq_add_neg _ _)
[GOAL]
case some.none
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s✝ t : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
s : NonemptyInterval α
⊢ some s - none = some s + -none
[PROOFSTEP]
rfl
[GOAL]
case some.some
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s✝ t✝ : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
s t : NonemptyInterval α
⊢ some s - some t = some s + -some t
[PROOFSTEP]
first
| rfl
| exact congr_arg some (sub_eq_add_neg _ _)
[GOAL]
case some.some
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s✝ t✝ : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
s t : NonemptyInterval α
⊢ some s - some t = some s + -some t
[PROOFSTEP]
rfl
[GOAL]
case some.some
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s✝ t✝ : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
s t : NonemptyInterval α
⊢ some s - some t = some s + -some t
[PROOFSTEP]
exact congr_arg some (sub_eq_add_neg _ _)
[GOAL]
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s t : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
⊢ ∀ (x : Interval α), - -x = x
[PROOFSTEP]
rintro (_ | s)
[GOAL]
case none
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s t : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
⊢ - -none = none
[PROOFSTEP]
first
| rfl
| exact congr_arg some (neg_neg _)
[GOAL]
case none
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s t : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
⊢ - -none = none
[PROOFSTEP]
rfl
[GOAL]
case some
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s✝ t : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
s : NonemptyInterval α
⊢ - -some s = some s
[PROOFSTEP]
first
| rfl
| exact congr_arg some (neg_neg _)
[GOAL]
case some
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s✝ t : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
s : NonemptyInterval α
⊢ - -some s = some s
[PROOFSTEP]
rfl
[GOAL]
case some
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s✝ t : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
s : NonemptyInterval α
⊢ - -some s = some s
[PROOFSTEP]
exact congr_arg some (neg_neg _)
[GOAL]
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s t : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
⊢ ∀ (a b : Interval α), -(a + b) = -b + -a
[PROOFSTEP]
rintro (_ | s) (_ | t)
[GOAL]
case none.none
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s t : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
⊢ -(none + none) = -none + -none
[PROOFSTEP]
first
| rfl
| exact congr_arg some (neg_add_rev _ _)
[GOAL]
case none.none
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s t : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
⊢ -(none + none) = -none + -none
[PROOFSTEP]
rfl
[GOAL]
case none.some
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s t✝ : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
t : NonemptyInterval α
⊢ -(none + some t) = -some t + -none
[PROOFSTEP]
first
| rfl
| exact congr_arg some (neg_add_rev _ _)
[GOAL]
case none.some
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s t✝ : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
t : NonemptyInterval α
⊢ -(none + some t) = -some t + -none
[PROOFSTEP]
rfl
[GOAL]
case some.none
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s✝ t : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
s : NonemptyInterval α
⊢ -(some s + none) = -none + -some s
[PROOFSTEP]
first
| rfl
| exact congr_arg some (neg_add_rev _ _)
[GOAL]
case some.none
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s✝ t : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
s : NonemptyInterval α
⊢ -(some s + none) = -none + -some s
[PROOFSTEP]
rfl
[GOAL]
case some.some
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s✝ t✝ : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
s t : NonemptyInterval α
⊢ -(some s + some t) = -some t + -some s
[PROOFSTEP]
first
| rfl
| exact congr_arg some (neg_add_rev _ _)
[GOAL]
case some.some
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s✝ t✝ : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
s t : NonemptyInterval α
⊢ -(some s + some t) = -some t + -some s
[PROOFSTEP]
rfl
[GOAL]
case some.some
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s✝ t✝ : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
s t : NonemptyInterval α
⊢ -(some s + some t) = -some t + -some s
[PROOFSTEP]
exact congr_arg some (neg_add_rev _ _)
[GOAL]
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s t : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
⊢ ∀ (a b : Interval α), a + b = 0 → -a = b
[PROOFSTEP]
rintro (_ | s) (_ | t) h
[GOAL]
case none.none
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s t : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
h : none + none = 0
⊢ -none = none
[PROOFSTEP]
first
| cases h
| exact congr_arg some (neg_eq_of_add_eq_zero_right <| Option.some_injective _ h)
[GOAL]
case none.none
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s t : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
h : none + none = 0
⊢ -none = none
[PROOFSTEP]
cases h
[GOAL]
case none.some
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s t✝ : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
t : NonemptyInterval α
h : none + some t = 0
⊢ -none = some t
[PROOFSTEP]
first
| cases h
| exact congr_arg some (neg_eq_of_add_eq_zero_right <| Option.some_injective _ h)
[GOAL]
case none.some
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s t✝ : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
t : NonemptyInterval α
h : none + some t = 0
⊢ -none = some t
[PROOFSTEP]
cases h
[GOAL]
case some.none
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s✝ t : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
s : NonemptyInterval α
h : some s + none = 0
⊢ -some s = none
[PROOFSTEP]
first
| cases h
| exact congr_arg some (neg_eq_of_add_eq_zero_right <| Option.some_injective _ h)
[GOAL]
case some.none
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s✝ t : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
s : NonemptyInterval α
h : some s + none = 0
⊢ -some s = none
[PROOFSTEP]
cases h
[GOAL]
case some.some
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s✝ t✝ : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
s t : NonemptyInterval α
h : some s + some t = 0
⊢ -some s = some t
[PROOFSTEP]
first
| cases h
| exact congr_arg some (neg_eq_of_add_eq_zero_right <| Option.some_injective _ h)
[GOAL]
case some.some
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s✝ t✝ : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
s t : NonemptyInterval α
h : some s + some t = 0
⊢ -some s = some t
[PROOFSTEP]
cases h
[GOAL]
case some.some
ι : Type u_1
α✝ : Type u_2
inst✝¹ : OrderedCommGroup α✝
s✝ t✝ : Interval α✝
α : Type u
inst✝ : OrderedAddCommGroup α
src✝ : AddCommMonoid (Interval α) := addCommMonoid
s t : NonemptyInterval α
h : some s + some t = 0
⊢ -some s = some t
[PROOFSTEP]
exact congr_arg some (neg_eq_of_add_eq_zero_right <| Option.some_injective _ h)
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
⊢ ∀ (a b : Interval α), a / b = a * b⁻¹
[PROOFSTEP]
rintro (_ | s) (_ | t)
[GOAL]
case none.none
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
⊢ none / none = none * none⁻¹
[PROOFSTEP]
first
| rfl
| exact congr_arg some (div_eq_mul_inv _ _)
[GOAL]
case none.none
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
⊢ none / none = none * none⁻¹
[PROOFSTEP]
rfl
[GOAL]
case none.some
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t✝ : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
t : NonemptyInterval α
⊢ none / some t = none * (some t)⁻¹
[PROOFSTEP]
first
| rfl
| exact congr_arg some (div_eq_mul_inv _ _)
[GOAL]
case none.some
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t✝ : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
t : NonemptyInterval α
⊢ none / some t = none * (some t)⁻¹
[PROOFSTEP]
rfl
[GOAL]
case some.none
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s✝ t : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
s : NonemptyInterval α
⊢ some s / none = some s * none⁻¹
[PROOFSTEP]
first
| rfl
| exact congr_arg some (div_eq_mul_inv _ _)
[GOAL]
case some.none
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s✝ t : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
s : NonemptyInterval α
⊢ some s / none = some s * none⁻¹
[PROOFSTEP]
rfl
[GOAL]
case some.some
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s✝ t✝ : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
s t : NonemptyInterval α
⊢ some s / some t = some s * (some t)⁻¹
[PROOFSTEP]
first
| rfl
| exact congr_arg some (div_eq_mul_inv _ _)
[GOAL]
case some.some
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s✝ t✝ : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
s t : NonemptyInterval α
⊢ some s / some t = some s * (some t)⁻¹
[PROOFSTEP]
rfl
[GOAL]
case some.some
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s✝ t✝ : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
s t : NonemptyInterval α
⊢ some s / some t = some s * (some t)⁻¹
[PROOFSTEP]
exact congr_arg some (div_eq_mul_inv _ _)
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
⊢ ∀ (x : Interval α), x⁻¹⁻¹ = x
[PROOFSTEP]
rintro (_ | s)
[GOAL]
case none
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
⊢ none⁻¹⁻¹ = none
[PROOFSTEP]
first
| rfl
| exact congr_arg some (inv_inv _)
[GOAL]
case none
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
⊢ none⁻¹⁻¹ = none
[PROOFSTEP]
rfl
[GOAL]
case some
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s✝ t : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
s : NonemptyInterval α
⊢ (some s)⁻¹⁻¹ = some s
[PROOFSTEP]
first
| rfl
| exact congr_arg some (inv_inv _)
[GOAL]
case some
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s✝ t : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
s : NonemptyInterval α
⊢ (some s)⁻¹⁻¹ = some s
[PROOFSTEP]
rfl
[GOAL]
case some
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s✝ t : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
s : NonemptyInterval α
⊢ (some s)⁻¹⁻¹ = some s
[PROOFSTEP]
exact congr_arg some (inv_inv _)
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
⊢ ∀ (a b : Interval α), (a * b)⁻¹ = b⁻¹ * a⁻¹
[PROOFSTEP]
rintro (_ | s) (_ | t)
[GOAL]
case none.none
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
⊢ (none * none)⁻¹ = none⁻¹ * none⁻¹
[PROOFSTEP]
first
| rfl
| exact congr_arg some (mul_inv_rev _ _)
[GOAL]
case none.none
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
⊢ (none * none)⁻¹ = none⁻¹ * none⁻¹
[PROOFSTEP]
rfl
[GOAL]
case none.some
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t✝ : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
t : NonemptyInterval α
⊢ (none * some t)⁻¹ = (some t)⁻¹ * none⁻¹
[PROOFSTEP]
first
| rfl
| exact congr_arg some (mul_inv_rev _ _)
[GOAL]
case none.some
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t✝ : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
t : NonemptyInterval α
⊢ (none * some t)⁻¹ = (some t)⁻¹ * none⁻¹
[PROOFSTEP]
rfl
[GOAL]
case some.none
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s✝ t : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
s : NonemptyInterval α
⊢ (some s * none)⁻¹ = none⁻¹ * (some s)⁻¹
[PROOFSTEP]
first
| rfl
| exact congr_arg some (mul_inv_rev _ _)
[GOAL]
case some.none
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s✝ t : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
s : NonemptyInterval α
⊢ (some s * none)⁻¹ = none⁻¹ * (some s)⁻¹
[PROOFSTEP]
rfl
[GOAL]
case some.some
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s✝ t✝ : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
s t : NonemptyInterval α
⊢ (some s * some t)⁻¹ = (some t)⁻¹ * (some s)⁻¹
[PROOFSTEP]
first
| rfl
| exact congr_arg some (mul_inv_rev _ _)
[GOAL]
case some.some
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s✝ t✝ : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
s t : NonemptyInterval α
⊢ (some s * some t)⁻¹ = (some t)⁻¹ * (some s)⁻¹
[PROOFSTEP]
rfl
[GOAL]
case some.some
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s✝ t✝ : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
s t : NonemptyInterval α
⊢ (some s * some t)⁻¹ = (some t)⁻¹ * (some s)⁻¹
[PROOFSTEP]
exact congr_arg some (mul_inv_rev _ _)
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
⊢ ∀ (a b : Interval α), a * b = 1 → a⁻¹ = b
[PROOFSTEP]
rintro (_ | s) (_ | t) h
[GOAL]
case none.none
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
h : none * none = 1
⊢ none⁻¹ = none
[PROOFSTEP]
first
| cases h
| exact congr_arg some (inv_eq_of_mul_eq_one_right <| Option.some_injective _ h)
[GOAL]
case none.none
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
h : none * none = 1
⊢ none⁻¹ = none
[PROOFSTEP]
cases h
[GOAL]
case none.some
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t✝ : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
t : NonemptyInterval α
h : none * some t = 1
⊢ none⁻¹ = some t
[PROOFSTEP]
first
| cases h
| exact congr_arg some (inv_eq_of_mul_eq_one_right <| Option.some_injective _ h)
[GOAL]
case none.some
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t✝ : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
t : NonemptyInterval α
h : none * some t = 1
⊢ none⁻¹ = some t
[PROOFSTEP]
cases h
[GOAL]
case some.none
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s✝ t : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
s : NonemptyInterval α
h : some s * none = 1
⊢ (some s)⁻¹ = none
[PROOFSTEP]
first
| cases h
| exact congr_arg some (inv_eq_of_mul_eq_one_right <| Option.some_injective _ h)
[GOAL]
case some.none
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s✝ t : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
s : NonemptyInterval α
h : some s * none = 1
⊢ (some s)⁻¹ = none
[PROOFSTEP]
cases h
[GOAL]
case some.some
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s✝ t✝ : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
s t : NonemptyInterval α
h : some s * some t = 1
⊢ (some s)⁻¹ = some t
[PROOFSTEP]
first
| cases h
| exact congr_arg some (inv_eq_of_mul_eq_one_right <| Option.some_injective _ h)
[GOAL]
case some.some
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s✝ t✝ : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
s t : NonemptyInterval α
h : some s * some t = 1
⊢ (some s)⁻¹ = some t
[PROOFSTEP]
cases h
[GOAL]
case some.some
ι : Type u_1
α : Type u_2
inst✝ : OrderedCommGroup α
s✝ t✝ : Interval α
src✝ : CommMonoid (Interval α) := commMonoid
s t : NonemptyInterval α
h : some s * some t = 1
⊢ (some s)⁻¹ = some t
[PROOFSTEP]
exact congr_arg some (inv_eq_of_mul_eq_one_right <| Option.some_injective _ h)
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : OrderedAddCommGroup α
s t : NonemptyInterval α
a : α
⊢ length (s - t) = length s + length t
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : OrderedAddCommGroup α
s t : Interval α
a : α
x✝ : Interval α
⊢ length (⊥ + x✝) ≤ length ⊥ + length x✝
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : OrderedAddCommGroup α
s t : Interval α
a : α
x✝ : Interval α
⊢ length (x✝ + ⊥) ≤ length x✝ + length ⊥
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : OrderedAddCommGroup α
s t : Interval α
a : α
⊢ length (s - t) ≤ length s + length t
[PROOFSTEP]
simpa [sub_eq_add_neg] using length_add_le s (-t)
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : OrderedAddCommGroup α
s✝ t : Interval α
a : α
f : ι → Interval α
s : Finset ι
⊢ length (∑ i in s, f i) ≤ ∑ i in s, length (f i)
[PROOFSTEP]
apply Finset.le_sum_of_subadditive
[GOAL]
case h_one
ι : Type u_1
α : Type u_2
inst✝ : OrderedAddCommGroup α
s✝ t : Interval α
a : α
f : ι → Interval α
s : Finset ι
⊢ length 0 = 0
case h_mul
ι : Type u_1
α : Type u_2
inst✝ : OrderedAddCommGroup α
s✝ t : Interval α
a : α
f : ι → Interval α
s : Finset ι
⊢ ∀ (x y : Interval α), length (x + y) ≤ length x + length y
[PROOFSTEP]
exact length_zero
[GOAL]
case h_mul
ι : Type u_1
α : Type u_2
inst✝ : OrderedAddCommGroup α
s✝ t : Interval α
a : α
f : ι → Interval α
s : Finset ι
⊢ ∀ (x y : Interval α), length (x + y) ≤ length x + length y
[PROOFSTEP]
exact length_add_le


[GOAL]
α : Type u_1
ι : Type u_2
inst✝² : LinearOrderedSemifield α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
α : Type u_1
ι : Type u_2
inst✝² : LinearOrderedSemifield α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i
[PROOFSTEP]
cases isEmpty_or_nonempty ι
[GOAL]
case intro.inl
α : Type u_1
ι : Type u_2
inst✝² : LinearOrderedSemifield α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
h✝ : IsEmpty ι
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i
[PROOFSTEP]
exact ⟨1, zero_lt_one, isEmptyElim⟩
[GOAL]
case intro.inr
α : Type u_1
ι : Type u_2
inst✝² : LinearOrderedSemifield α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
h✝ : Nonempty ι
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i
[PROOFSTEP]
choose ε hε hxε using fun i => exists_pos_add_of_lt' (h i)
[GOAL]
case intro.inr
α : Type u_1
ι : Type u_2
inst✝² : LinearOrderedSemifield α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
h✝ : Nonempty ι
ε : ι → α
hε : ∀ (i : ι), 0 < ε i
hxε : ∀ (i : ι), x i + ε i = y i
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i
[PROOFSTEP]
obtain rfl : x + ε = y := funext hxε
[GOAL]
case intro.inr
α : Type u_1
ι : Type u_2
inst✝² : LinearOrderedSemifield α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x : ι → α
val✝ : Fintype ι
h✝ : Nonempty ι
ε : ι → α
hε : ∀ (i : ι), 0 < ε i
h : ∀ (i : ι), x i < (x + ε) i
hxε : ∀ (i : ι), x i + ε i = (x + ε) i
⊢ ∃ ε_1, 0 < ε_1 ∧ ∀ (i : ι), x i + ε_1 < (x + ε) i
[PROOFSTEP]
have hε : 0 < Finset.univ.inf' Finset.univ_nonempty ε := (Finset.lt_inf'_iff _).2 fun i _ => hε _
[GOAL]
case intro.inr
α : Type u_1
ι : Type u_2
inst✝² : LinearOrderedSemifield α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x : ι → α
val✝ : Fintype ι
h✝ : Nonempty ι
ε : ι → α
hε✝ : ∀ (i : ι), 0 < ε i
h : ∀ (i : ι), x i < (x + ε) i
hxε : ∀ (i : ι), x i + ε i = (x + ε) i
hε : 0 < Finset.inf' Finset.univ (_ : Finset.Nonempty Finset.univ) ε
⊢ ∃ ε_1, 0 < ε_1 ∧ ∀ (i : ι), x i + ε_1 < (x + ε) i
[PROOFSTEP]
exact ⟨_, half_pos hε, fun i => add_lt_add_left ((half_lt_self hε).trans_le <| Finset.inf'_le _ <| Finset.mem_univ _) _⟩


[GOAL]
α : Type u_1
inst✝² : CanonicallyLinearOrderedSemifield α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
⊢ (a - b) / c = a / c - b / c
[PROOFSTEP]
simp_rw [div_eq_mul_inv, tsub_mul]


[GOAL]
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ max a 1 / max a⁻¹ 1 = a
[PROOFSTEP]
rcases le_total a 1 with (h | h)
[GOAL]
case inl
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
h : a ≤ 1
⊢ max a 1 / max a⁻¹ 1 = a
[PROOFSTEP]
simp [h]
[GOAL]
case inr
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
h : 1 ≤ a
⊢ max a 1 / max a⁻¹ 1 = a
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedCommGroup α
a✝ b✝ c✝ a b c : α
⊢ min (a / c) (b / c) = min a b / c
[PROOFSTEP]
simpa only [div_eq_mul_inv] using min_mul_mul_right a b c⁻¹
[GOAL]
α : Type u_1
inst✝ : LinearOrderedCommGroup α
a✝ b✝ c✝ a b c : α
⊢ max (a / c) (b / c) = max a b / c
[PROOFSTEP]
simpa only [div_eq_mul_inv] using max_mul_mul_right a b c⁻¹
[GOAL]
α : Type u_1
inst✝ : LinearOrderedCommGroup α
a✝ b✝ c✝ a b c : α
⊢ min (a / b) (a / c) = a / max b c
[PROOFSTEP]
simp only [div_eq_mul_inv, min_mul_mul_left, min_inv_inv']
[GOAL]
α : Type u_1
inst✝ : LinearOrderedCommGroup α
a✝ b✝ c✝ a b c : α
⊢ max (a / b) (a / c) = a / min b c
[PROOFSTEP]
simp only [div_eq_mul_inv, max_mul_mul_left, max_inv_inv']
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c✝ a b c d : α
⊢ max a b - max c d ≤ max (a - c) (b - d)
[PROOFSTEP]
simp only [sub_le_iff_le_add, max_le_iff]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c✝ a b c d : α
⊢ a ≤ max (a - c) (b - d) + max c d ∧ b ≤ max (a - c) (b - d) + max c d
[PROOFSTEP]
constructor
[GOAL]
case left
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c✝ a b c d : α
⊢ a ≤ max (a - c) (b - d) + max c d
case right α : Type u_1 inst✝ : LinearOrderedAddCommGroup α a✝ b✝ c✝ a b c d : α ⊢ b ≤ max (a - c) (b - d) + max c d
[PROOFSTEP]
calc
  a = a - c + c := (sub_add_cancel a c).symm
  _ ≤ max (a - c) (b - d) + max c d := add_le_add (le_max_left _ _) (le_max_left _ _)
[GOAL]
case right
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c✝ a b c d : α
⊢ b ≤ max (a - c) (b - d) + max c d
[PROOFSTEP]
calc
  b = b - d + d := (sub_add_cancel b d).symm
  _ ≤ max (a - c) (b - d) + max c d := add_le_add (le_max_right _ _) (le_max_right _ _)
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c✝ a b c d : α
⊢ |max a b - max c d| ≤ max |a - c| |b - d|
[PROOFSTEP]
refine' abs_sub_le_iff.2 ⟨_, _⟩
[GOAL]
case refine'_1
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c✝ a b c d : α
⊢ max a b - max c d ≤ max |a - c| |b - d|
[PROOFSTEP]
exact (max_sub_max_le_max _ _ _ _).trans (max_le_max (le_abs_self _) (le_abs_self _))
[GOAL]
case refine'_2
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c✝ a b c d : α
⊢ max c d - max a b ≤ max |a - c| |b - d|
[PROOFSTEP]
rw [abs_sub_comm a c, abs_sub_comm b d]
[GOAL]
case refine'_2
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c✝ a b c d : α
⊢ max c d - max a b ≤ max |c - a| |d - b|
[PROOFSTEP]
exact (max_sub_max_le_max _ _ _ _).trans (max_le_max (le_abs_self _) (le_abs_self _))
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c✝ a b c d : α
⊢ |min a b - min c d| ≤ max |a - c| |b - d|
[PROOFSTEP]
simpa only [max_neg_neg, neg_sub_neg, abs_sub_comm] using abs_max_sub_max_le_max (-a) (-b) (-c) (-d)
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c✝ a b c : α
⊢ |max a c - max b c| ≤ |a - b|
[PROOFSTEP]
simpa only [sub_self, abs_zero, max_eq_left (abs_nonneg (a - b))] using abs_max_sub_max_le_max a c b c