awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : Interval α
bot : ⊥ * t = 1 ↔ ∃ (a : α) (b : α), Eq (α := Interval α) ⊥ (pure a) ∧ t = pure b ∧ a * b = 1
coe :
  ∀ (a : NonemptyInterval α),
    (↑a : Interval α) * t = 1 ↔ ∃ (a_1 : α) (b : α), (↑a : Interval α) = pure a_1 ∧ t = pure b ∧ a_1 * b = 1
⊢ s * t = 1 ↔ ∃ (a : α) (b : α), s = pure a ∧ t = pure b ∧ a * b = 1

Tactic:
cases s
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
t : Interval α
⊢ ⊥ * t = 1 ↔ ∃ (a : α) (b : α), Eq (α := Interval α) ⊥ (pure a) ∧ t = pure b ∧ a * b = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
t : Interval α
a : NonemptyInterval α
coe :
  (↑a : Interval α) * ⊥ = 1 ↔
    ∃ (a_1 : α) (b : α), (↑a : Interval α) = pure a_1 ∧ Eq (α := Interval α) ⊥ (pure b) ∧ a_1 * b = 1
coe₁ :
  ∀ (a_1 : NonemptyInterval α),
    (↑a : Interval α) * (↑a_1 : Interval α) = 1 ↔
      ∃ (a_2 : α) (b : α), (↑a : Interval α) = pure a_2 ∧ (↑a_1 : Interval α) = pure b ∧ a_2 * b = 1
⊢ (↑a : Interval α) * t = 1 ↔ ∃ (a_1 : α) (b : α), (↑a : Interval α) = pure a_1 ∧ t = pure b ∧ a_1 * b = 1

Tactic:
cases t
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : NonemptyInterval α
⊢ (↑a : Interval α) * ⊥ = 1 ↔
    ∃ (a_1 : α) (b : α), (↑a : Interval α) = pure a_1 ∧ Eq (α := Interval α) ⊥ (pure b) ∧ a_1 * b = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a a_1 : NonemptyInterval α
coe : a * a_1 = 1 ↔ ∃ (a_2 : α) (b : α), a = NonemptyInterval.pure a_2 ∧ a_1 = NonemptyInterval.pure b ∧ a_2 * b = 1
⊢ (↑a : Interval α) * (↑a_1 : Interval α) = 1 ↔
    ∃ (a_2 : α) (b : α), (↑a : Interval α) = pure a_2 ∧ (↑a_1 : Interval α) = pure b ∧ a_2 * b = 1

Tactic:
simp_rw [← NonemptyInterval.coe_mul_interval, ← NonemptyInterval.coe_one_interval,
      Interval.coe_inj, NonemptyInterval.coe_eq_pure]

Premises used: NonemptyInterval.coe_one_interval, Interval.coe_inj, NonemptyInterval.coe_eq_pure, NonemptyInterval.coe_mul_interval
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a a_1 : NonemptyInterval α
⊢ a * a_1 = 1 ↔ ∃ (a_2 : α) (b : α), a = NonemptyInterval.pure a_2 ∧ a_1 = NonemptyInterval.pure b ∧ a_2 * b = 1

Tactic:
NonemptyInterval.mul_eq_one_iff

Premises used: NonemptyInterval.mul_eq_one_iff
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a a_1 : NonemptyInterval α
⊢ a * a_1 = 1 ↔ ∃ (a_2 : α) (b : α), a = NonemptyInterval.pure a_2 ∧ a_1 = NonemptyInterval.pure b ∧ a_2 * b = 1

Tactic:
exact NonemptyInterval.mul_eq_one_iff

Premises used: NonemptyInterval.mul_eq_one_iff
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s t : Interval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
⊢ HSub.hSub (α := Interval α) none none = HAdd.hAdd (α := Interval α) none (-none)

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s t : Interval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
⊢ HSub.hSub (α := Interval α) none none = HAdd.hAdd (α := Interval α) none (-none)

Tactic:
first | rfl | exact congr_arg WithBot.some (sub_eq_add_neg _ _)

Premises used: WithBot.some, sub_eq_add_neg, congr_arg
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s t_1 : Interval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
t : NonemptyInterval α
⊢ none - some t = none + -some t

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s t_1 : Interval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
t : NonemptyInterval α
⊢ none - some t = none + -some t

Tactic:
first | rfl | exact congr_arg WithBot.some (sub_eq_add_neg _ _)

Premises used: WithBot.some, sub_eq_add_neg, congr_arg
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s_1 t : Interval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s : NonemptyInterval α
⊢ some s - none = some s + -none

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s_1 t : Interval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s : NonemptyInterval α
⊢ some s - none = some s + -none

Tactic:
first | rfl | exact congr_arg WithBot.some (sub_eq_add_neg _ _)

Premises used: WithBot.some, sub_eq_add_neg, congr_arg
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s_1 t_1 : Interval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s t : NonemptyInterval α
⊢ some s - some t = some s + -some t

Tactic:
congr_arg WithBot.some (sub_eq_add_neg _ _)

Premises used: WithBot.some, sub_eq_add_neg, Interval, congr_arg, WithBot.map₂, Option.map₂
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s_1 t_1 : Interval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s t : NonemptyInterval α
⊢ some s - some t = some s + -some t

Tactic:
exact congr_arg WithBot.some (sub_eq_add_neg _ _)

Premises used: WithBot.some, sub_eq_add_neg, congr_arg
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s_1 t_1 : Interval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s t : NonemptyInterval α
⊢ some s - some t = some s + -some t

Tactic:
first | rfl | exact congr_arg WithBot.some (sub_eq_add_neg _ _)

Premises used: WithBot.some, sub_eq_add_neg, congr_arg
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s t : Interval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
⊢ Eq.{u + 1} (α := Interval α) (- -none) none

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s t : Interval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
⊢ Eq.{u + 1} (α := Interval α) (- -none) none

Tactic:
first | rfl | exact congr_arg WithBot.some (neg_neg _)

Premises used: WithBot.some, neg_neg, congr_arg
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s_1 t : Interval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s : NonemptyInterval α
⊢ - -some s = some s

Tactic:
congr_arg WithBot.some (neg_neg _)

Premises used: WithBot.some, neg_neg, Interval, congr_arg, WithBot.map
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s_1 t : Interval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s : NonemptyInterval α
⊢ - -some s = some s

Tactic:
exact congr_arg WithBot.some (neg_neg _)

Premises used: WithBot.some, neg_neg, congr_arg
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s_1 t : Interval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s : NonemptyInterval α
⊢ - -some s = some s

Tactic:
first | rfl | exact congr_arg WithBot.some (neg_neg _)

Premises used: WithBot.some, neg_neg, congr_arg
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s t : Interval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
⊢ -HAdd.hAdd (α := Interval α) none none = HAdd.hAdd (α := Interval α) (-none) (-none)

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s t : Interval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
⊢ -HAdd.hAdd (α := Interval α) none none = HAdd.hAdd (α := Interval α) (-none) (-none)

Tactic:
first | rfl | exact congr_arg WithBot.some (neg_add_rev _ _)

Premises used: neg_add_rev, WithBot.some, congr_arg
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s t_1 : Interval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
t : NonemptyInterval α
⊢ -(none + some t) = -some t + -none

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s t_1 : Interval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
t : NonemptyInterval α
⊢ -(none + some t) = -some t + -none

Tactic:
first | rfl | exact congr_arg WithBot.some (neg_add_rev _ _)

Premises used: neg_add_rev, WithBot.some, congr_arg
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s_1 t : Interval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s : NonemptyInterval α
⊢ -(some s + none) = -none + -some s

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s_1 t : Interval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s : NonemptyInterval α
⊢ -(some s + none) = -none + -some s

Tactic:
first | rfl | exact congr_arg WithBot.some (neg_add_rev _ _)

Premises used: neg_add_rev, WithBot.some, congr_arg
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s_1 t_1 : Interval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s t : NonemptyInterval α
⊢ -(some s + some t) = -some t + -some s

Tactic:
congr_arg WithBot.some (neg_add_rev _ _)

Premises used: neg_add_rev, WithBot.some, Interval, congr_arg, WithBot.map, WithBot.map₂, Option.map₂
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s_1 t_1 : Interval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s t : NonemptyInterval α
⊢ -(some s + some t) = -some t + -some s

Tactic:
exact congr_arg WithBot.some (neg_add_rev _ _)

Premises used: neg_add_rev, WithBot.some, congr_arg
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s_1 t_1 : Interval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s t : NonemptyInterval α
⊢ -(some s + some t) = -some t + -some s

Tactic:
first | rfl | exact congr_arg WithBot.some (neg_add_rev _ _)

Premises used: neg_add_rev, WithBot.some, congr_arg
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s t : Interval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
h : HAdd.hAdd (α := Interval α) none none = 0
⊢ Eq.{u + 1} (α := Interval α) (-none) none

Tactic:
cases h
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s t : Interval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
h : HAdd.hAdd (α := Interval α) none none = 0
⊢ Eq.{u + 1} (α := Interval α) (-none) none

Tactic:
first
        | cases h
        | exact congr_arg WithBot.some (neg_eq_of_add_eq_zero_right <| WithBot.coe_injective h)
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s t_1 : Interval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
t : NonemptyInterval α
h : none + some t = 0
⊢ -none = some t

Tactic:
cases h
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s t_1 : Interval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
t : NonemptyInterval α
h : none + some t = 0
⊢ -none = some t

Tactic:
first
        | cases h
        | exact congr_arg WithBot.some (neg_eq_of_add_eq_zero_right <| WithBot.coe_injective h)
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s_1 t : Interval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s : NonemptyInterval α
h : some s + none = 0
⊢ -some s = none

Tactic:
cases h
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s_1 t : Interval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s : NonemptyInterval α
h : some s + none = 0
⊢ -some s = none

Tactic:
first
        | cases h
        | exact congr_arg WithBot.some (neg_eq_of_add_eq_zero_right <| WithBot.coe_injective h)
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s_1 t_1 : Interval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s t : NonemptyInterval α
h : some s + some t = 0
⊢ -some s = some t

Tactic:
cases h
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s_1 t_1 : Interval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s t : NonemptyInterval α
h : some s + some t = 0
⊢ -some s = some t

Tactic:
congr_arg WithBot.some (neg_eq_of_add_eq_zero_right <| WithBot.coe_injective h)

Premises used: WithBot.some, WithBot.coe_injective, Interval, congr_arg, WithBot.map, neg_eq_of_add_eq_zero_right
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s_1 t_1 : Interval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s t : NonemptyInterval α
h : some s + some t = 0
⊢ -some s = some t

Tactic:
exact congr_arg WithBot.some (neg_eq_of_add_eq_zero_right <| WithBot.coe_injective h)

Premises used: WithBot.some, WithBot.coe_injective, congr_arg, neg_eq_of_add_eq_zero_right
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s_1 t_1 : Interval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s t : NonemptyInterval α
h : some s + some t = 0
⊢ -some s = some t

Tactic:
first
        | cases h
        | exact congr_arg WithBot.some (neg_eq_of_add_eq_zero_right <| WithBot.coe_injective h)

Premises used: WithBot.some, WithBot.coe_injective, congr_arg, neg_eq_of_add_eq_zero_right
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : Interval α
⊢ HDiv.hDiv (α := Interval α) none none = HMul.hMul (α := Interval α) none none⁻¹

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : Interval α
⊢ HDiv.hDiv (α := Interval α) none none = HMul.hMul (α := Interval α) none none⁻¹

Tactic:
first | rfl | exact congr_arg WithBot.some (div_eq_mul_inv _ _)

Premises used: WithBot.some, div_eq_mul_inv, congr_arg
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t_1 : Interval α
t : NonemptyInterval α
⊢ none / some t = none * (some t)⁻¹

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t_1 : Interval α
t : NonemptyInterval α
⊢ none / some t = none * (some t)⁻¹

Tactic:
first | rfl | exact congr_arg WithBot.some (div_eq_mul_inv _ _)

Premises used: WithBot.some, div_eq_mul_inv, congr_arg
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s_1 t : Interval α
s : NonemptyInterval α
⊢ some s / none = some s * none⁻¹

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s_1 t : Interval α
s : NonemptyInterval α
⊢ some s / none = some s * none⁻¹

Tactic:
first | rfl | exact congr_arg WithBot.some (div_eq_mul_inv _ _)

Premises used: WithBot.some, div_eq_mul_inv, congr_arg
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s_1 t_1 : Interval α
s t : NonemptyInterval α
⊢ some s / some t = some s * (some t)⁻¹

Tactic:
congr_arg WithBot.some (div_eq_mul_inv _ _)

Premises used: WithBot.some, Interval, div_eq_mul_inv, congr_arg, WithBot.map₂, Option.map₂
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s_1 t_1 : Interval α
s t : NonemptyInterval α
⊢ some s / some t = some s * (some t)⁻¹

Tactic:
exact congr_arg WithBot.some (div_eq_mul_inv _ _)

Premises used: WithBot.some, div_eq_mul_inv, congr_arg
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s_1 t_1 : Interval α
s t : NonemptyInterval α
⊢ some s / some t = some s * (some t)⁻¹

Tactic:
first | rfl | exact congr_arg WithBot.some (div_eq_mul_inv _ _)

Premises used: WithBot.some, div_eq_mul_inv, congr_arg
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : Interval α
⊢ Eq.{u_2 + 1} (α := Interval α) none⁻¹⁻¹ none

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : Interval α
⊢ Eq.{u_2 + 1} (α := Interval α) none⁻¹⁻¹ none

Tactic:
first | rfl | exact congr_arg WithBot.some (inv_inv _)

Premises used: WithBot.some, congr_arg, inv_inv
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s_1 t : Interval α
s : NonemptyInterval α
⊢ (some s)⁻¹⁻¹ = some s

Tactic:
congr_arg WithBot.some (inv_inv _)

Premises used: WithBot.some, Interval, congr_arg, inv_inv, WithBot.map
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s_1 t : Interval α
s : NonemptyInterval α
⊢ (some s)⁻¹⁻¹ = some s

Tactic:
exact congr_arg WithBot.some (inv_inv _)

Premises used: WithBot.some, congr_arg, inv_inv
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s_1 t : Interval α
s : NonemptyInterval α
⊢ (some s)⁻¹⁻¹ = some s

Tactic:
first | rfl | exact congr_arg WithBot.some (inv_inv _)

Premises used: WithBot.some, congr_arg, inv_inv
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : Interval α
⊢ (HMul.hMul (α := Interval α) none none)⁻¹ = HMul.hMul (α := Interval α) none⁻¹ none⁻¹

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : Interval α
⊢ (HMul.hMul (α := Interval α) none none)⁻¹ = HMul.hMul (α := Interval α) none⁻¹ none⁻¹

Tactic:
first | rfl | exact congr_arg WithBot.some (mul_inv_rev _ _)

Premises used: WithBot.some, congr_arg, mul_inv_rev
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t_1 : Interval α
t : NonemptyInterval α
⊢ (none * some t)⁻¹ = (some t)⁻¹ * none⁻¹

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t_1 : Interval α
t : NonemptyInterval α
⊢ (none * some t)⁻¹ = (some t)⁻¹ * none⁻¹

Tactic:
first | rfl | exact congr_arg WithBot.some (mul_inv_rev _ _)

Premises used: WithBot.some, congr_arg, mul_inv_rev
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s_1 t : Interval α
s : NonemptyInterval α
⊢ (some s * none)⁻¹ = none⁻¹ * (some s)⁻¹

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s_1 t : Interval α
s : NonemptyInterval α
⊢ (some s * none)⁻¹ = none⁻¹ * (some s)⁻¹

Tactic:
first | rfl | exact congr_arg WithBot.some (mul_inv_rev _ _)

Premises used: WithBot.some, congr_arg, mul_inv_rev
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s_1 t_1 : Interval α
s t : NonemptyInterval α
⊢ (some s * some t)⁻¹ = (some t)⁻¹ * (some s)⁻¹

Tactic:
congr_arg WithBot.some (mul_inv_rev _ _)

Premises used: WithBot.some, Interval, congr_arg, mul_inv_rev, WithBot.map, WithBot.map₂, Option.map₂
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s_1 t_1 : Interval α
s t : NonemptyInterval α
⊢ (some s * some t)⁻¹ = (some t)⁻¹ * (some s)⁻¹

Tactic:
exact congr_arg WithBot.some (mul_inv_rev _ _)

Premises used: WithBot.some, congr_arg, mul_inv_rev