[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
