awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : NonemptyInterval α
n : ℕ
⊢ (↑(s ^ n) : Interval α) = (↑s : Interval α) ^ n

Tactic:
map_pow (⟨⟨(↑), coe_one_interval⟩, coe_mul_interval⟩ : NonemptyInterval α →* Interval α) _ _

Premises used: WithBot.some, NonemptyInterval.coe_one_interval, OneHom.mk, MonoidHom.mk, map_pow, Interval.coe, NonemptyInterval.coe_mul_interval
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : NatCast α
n : ℕ
⊢ Eq.{u_2 + 1} (α := α) (toProd (↑n : NonemptyInterval α)).1 (↑n : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : NatCast α
n : ℕ
⊢ Eq.{u_2 + 1} (α := α) (toProd (↑n : NonemptyInterval α)).2 (↑n : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : NatCast α
n : ℕ
⊢ Eq.{u_2 + 1} (α := NonemptyInterval α) (pure (↑n : α)) (↑n : NonemptyInterval α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
inst_4 : AddLeftMono α
s t : NonemptyInterval α
⊢ (s - t).toProd.1 = s.toProd.1 - t.toProd.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
inst_4 : AddLeftMono α
s t : NonemptyInterval α
⊢ (s - t).toProd.2 = s.toProd.2 - t.toProd.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
inst_4 : AddLeftMono α
s t : NonemptyInterval α
⊢ (↑(s - t) : Interval α) = (↑s : Interval α) - (↑t : Interval α)

Tactic:
rfl

Premises used: WithBot.some, Interval.coe, WithBot.map₂, rfl, Option.map₂
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
inst_4 : AddLeftMono α
s t : NonemptyInterval α
a b : α
ha : a ∈ s
hb : b ∈ t
⊢ a - b ∈ s - t

Tactic:
⟨tsub_le_tsub ha.1 hb.2, tsub_le_tsub ha.2 hb.1⟩

Premises used: Set.Mem, setOf, tsub_le_tsub, Set.Icc, And.right, And.left, And.intro
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
inst_4 : AddLeftMono α
a b : α
⊢ HSub.hSub (α := NonemptyInterval α) (pure a) (pure b) = pure (a - b)

Tactic:
rfl

Premises used: NonemptyInterval.pure, rfl
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
inst_4 : AddLeftMono α
t : Interval α
⊢ ⊥ - t = ⊥

Tactic:
WithBot.map₂_bot_left _ _

Premises used: WithBot.map₂_bot_left, Interval
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
inst_4 : AddLeftMono α
s : Interval α
⊢ s - ⊥ = ⊥

Tactic:
WithBot.map₂_bot_right _ _

Premises used: Interval, WithBot.map₂_bot_right
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
s t : NonemptyInterval α
⊢ (s / t).toProd.1 = s.toProd.1 / t.toProd.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
s t : NonemptyInterval α
⊢ (s / t).toProd.2 = s.toProd.2 / t.toProd.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
s t : NonemptyInterval α
⊢ (↑(s / t) : Interval α) = (↑s : Interval α) / (↑t : Interval α)

Tactic:
rfl

Premises used: WithBot.some, Interval.coe, WithBot.map₂, rfl, Option.map₂
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
s t : NonemptyInterval α
a b : α
ha : a ∈ s
hb : b ∈ t
⊢ a / b ∈ s / t

Tactic:
⟨div_le_div'' ha.1 hb.2, div_le_div'' ha.2 hb.1⟩

Premises used: Set.Mem, setOf, div_le_div'', Set.Icc, And.right, And.left, And.intro
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
⊢ HDiv.hDiv (α := NonemptyInterval α) (pure a) (pure b) = pure (a / b)

Tactic:
rfl

Premises used: NonemptyInterval.pure, rfl
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
t : Interval α
⊢ ⊥ / t = ⊥

Tactic:
WithBot.map₂_bot_left _ _

Premises used: WithBot.map₂_bot_left, Interval
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
s : Interval α
⊢ s / ⊥ = ⊥

Tactic:
WithBot.map₂_bot_right _ _

Premises used: Interval, WithBot.map₂_bot_right
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s : NonemptyInterval α
⊢ s⁻¹.toProd.1 = s.toProd.2⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s : NonemptyInterval α
⊢ s⁻¹.toProd.2 = s.toProd.1⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s : NonemptyInterval α
⊢ (↑s⁻¹ : Interval α) = (↑s : Interval α)⁻¹

Tactic:
rfl

Premises used: WithBot.some, Interval.coe, WithBot.map, rfl
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s : NonemptyInterval α
a : α
ha : a ∈ s
⊢ a⁻¹ ∈ s⁻¹

Tactic:
⟨inv_le_inv' ha.2, inv_le_inv' ha.1⟩

Premises used: Set.Mem, setOf, Set.Icc, And.right, And.left, And.intro, inv_le_inv'
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : α
⊢ Eq (α := NonemptyInterval α) (pure a)⁻¹ (pure a⁻¹)

Tactic:
rfl

Premises used: NonemptyInterval.pure, rfl
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
⊢ Eq.{u_2 + 1} (α := Interval α) ⊥⁻¹ ⊥

Tactic:
rfl

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

Tactic:
⟨fun h => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : NonemptyInterval α
refine_1 : ∀ (h : s * t = 1), ∃ (a : α) (b : α), s = pure a ∧ t = pure b ∧ a * b = 1
refine_2 : (∃ (a : α) (b : α), s = pure a ∧ t = pure b ∧ a * b = 1) → s * t = 1
⊢ s * t = 1 ↔ ∃ (a : α) (b : α), s = pure a ∧ t = pure b ∧ a * b = 1

Tactic:
refine ⟨fun h => ?_, ?_⟩
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : NonemptyInterval α
h : s * t = 1
⊢ (s * t).toProd.1 = (toProd 1).1 ∧ (s * t).toProd.2 = (toProd 1).2

Tactic:
rw [NonemptyInterval.ext_iff, Prod.ext_iff] at h

Premises used: Prod.ext_iff, NonemptyInterval.ext_iff
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : NonemptyInterval α
h : (s * t).toProd.1 = (toProd 1).1 ∧ (s * t).toProd.2 = (toProd 1).2
⊢ s.toProd.1 = s.toProd.2 ∧ t.toProd.1 = t.toProd.2

Tactic:
have := (mul_le_mul_iff_of_ge s.fst_le_snd t.fst_le_snd).1 (h.2.trans h.1.symm).le
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : NonemptyInterval α
h : (s * t).toProd.1 = (toProd 1).1 ∧ (s * t).toProd.2 = (toProd 1).2
this : s.toProd.1 = s.toProd.2 ∧ t.toProd.1 = t.toProd.2
⊢ ∃ (a : α) (b : α), s = pure a ∧ t = pure b ∧ a * b = 1

Tactic:
⟨s.fst, t.fst, ?_, ?_, h.1⟩

Premises used: Prod.fst, And.left, And.intro, Exists.intro, NonemptyInterval.toProd
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : NonemptyInterval α
h : (s * t).toProd.1 = (toProd 1).1 ∧ (s * t).toProd.2 = (toProd 1).2
this : s.toProd.1 = s.toProd.2 ∧ t.toProd.1 = t.toProd.2
refine_1 : s = pure s.toProd.1
refine_1₁ : t = pure t.toProd.1
⊢ ∃ (a : α) (b : α), s = pure a ∧ t = pure b ∧ a * b = 1

Tactic:
refine ⟨s.fst, t.fst, ?_, ?_, h.1⟩
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : NonemptyInterval α
h : (s * t).toProd.1 = (toProd 1).1 ∧ (s * t).toProd.2 = (toProd 1).2
this : s.toProd.1 = s.toProd.2 ∧ t.toProd.1 = t.toProd.2
refine_1 : s.toProd = toProd (pure s.toProd.1)
⊢ s = pure s.toProd.1

Tactic:
apply NonemptyInterval.ext

Premises used: NonemptyInterval.ext
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : NonemptyInterval α
h : (s * t).toProd.1 = (toProd 1).1 ∧ (s * t).toProd.2 = (toProd 1).2
this : s.toProd.1 = s.toProd.2 ∧ t.toProd.1 = t.toProd.2
refine_1 : t.toProd = toProd (pure t.toProd.1)
⊢ t = pure t.toProd.1

Tactic:
apply NonemptyInterval.ext

Premises used: NonemptyInterval.ext
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : NonemptyInterval α
h : (s * t).toProd.1 = (toProd 1).1 ∧ (s * t).toProd.2 = (toProd 1).2
this : s.toProd.1 = s.toProd.2 ∧ t.toProd.1 = t.toProd.2
refine_1 refine_1₁ : s.toProd = (s.toProd.1, s.toProd.2)
⊢ s.toProd = (s.toProd.1, s.toProd.1)

Tactic:
nth_rw 2 [this.1]

Premises used: And.left
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : NonemptyInterval α
h : (s * t).toProd.1 = (toProd 1).1 ∧ (s * t).toProd.2 = (toProd 1).2
this : s.toProd.1 = s.toProd.2 ∧ t.toProd.1 = t.toProd.2
refine_1 refine_1₁ : t.toProd = (t.toProd.1, t.toProd.2)
⊢ t.toProd = (t.toProd.1, t.toProd.1)

Tactic:
nth_rw 2 [this.2]

Premises used: And.right
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
b c : α
h : b * c = 1
refine_2 : Eq (α := NonemptyInterval α) (pure (b * c)) 1
refine_2₁ : Eq.{u_2 + 1} (α := NonemptyInterval α) (pure 1) 1
refine_2₂ refine_2₃ : Eq.{u_2 + 1} (α := NonemptyInterval α) 1 1
⊢ HMul.hMul (α := NonemptyInterval α) (pure b) (pure c) = 1

Tactic:
rw [pure_mul_pure, h, pure_one]

Premises used: NonemptyInterval.pure_mul_pure, NonemptyInterval.pure_one
-- 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 : NonemptyInterval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s t : NonemptyInterval α
⊢ s - t = s + -t

Tactic:
NonemptyInterval.ext (Prod.ext ?_ ?_)

Premises used: NonemptyInterval.ext, Prod.ext
-- 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 : NonemptyInterval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s t : NonemptyInterval α
refine_1 : (s - t).toProd.1 = (s + -t).toProd.1
refine_2 : (s - t).toProd.2 = (s + -t).toProd.2
⊢ s - t = s + -t

Tactic:
refine NonemptyInterval.ext (Prod.ext ?_ ?_)

Premises used: NonemptyInterval.ext, Prod.ext
-- 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 : NonemptyInterval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s t : NonemptyInterval α
⊢ (s - t).toProd.1 = (s + -t).toProd.1

Tactic:
sub_eq_add_neg _ _

Premises used: sub_eq_add_neg
-- 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 : NonemptyInterval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s t : NonemptyInterval α
⊢ (s - t).toProd.1 = (s + -t).toProd.1

Tactic:
exact sub_eq_add_neg _ _

Premises used: sub_eq_add_neg
-- 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 : NonemptyInterval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s t : NonemptyInterval α
⊢ (s - t).toProd.2 = (s + -t).toProd.2

Tactic:
sub_eq_add_neg _ _

Premises used: sub_eq_add_neg
-- 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 : NonemptyInterval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s t : NonemptyInterval α
⊢ (s - t).toProd.2 = (s + -t).toProd.2

Tactic:
exact sub_eq_add_neg _ _

Premises used: sub_eq_add_neg
-- 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 : NonemptyInterval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s : NonemptyInterval α
toProd : (- -s).toProd = s.toProd
⊢ - -s = s

Tactic:
apply NonemptyInterval.ext

Premises used: NonemptyInterval.ext
-- 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 : NonemptyInterval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s : NonemptyInterval α
⊢ (- -s).toProd = s.toProd

Tactic:
neg_neg _

Premises used: neg_neg
-- 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 : NonemptyInterval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s : NonemptyInterval α
⊢ (- -s).toProd = s.toProd

Tactic:
exact neg_neg _

Premises used: neg_neg
-- 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 : NonemptyInterval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s t : NonemptyInterval α
⊢ -(s + t) = -t + -s

Tactic:
NonemptyInterval.ext (Prod.ext ?_ ?_)

Premises used: NonemptyInterval.ext, Prod.ext
-- 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 : NonemptyInterval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s t : NonemptyInterval α
refine_1 : (-(s + t)).toProd.1 = (-t + -s).toProd.1
refine_2 : (-(s + t)).toProd.2 = (-t + -s).toProd.2
⊢ -(s + t) = -t + -s

Tactic:
refine NonemptyInterval.ext (Prod.ext ?_ ?_)

Premises used: NonemptyInterval.ext, Prod.ext
-- 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 : NonemptyInterval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s t : NonemptyInterval α
⊢ (-(s + t)).toProd.1 = (-t + -s).toProd.1

Tactic:
neg_add_rev _ _

Premises used: neg_add_rev
-- 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 : NonemptyInterval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s t : NonemptyInterval α
⊢ (-(s + t)).toProd.1 = (-t + -s).toProd.1

Tactic:
exact neg_add_rev _ _

Premises used: neg_add_rev
-- 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 : NonemptyInterval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s t : NonemptyInterval α
⊢ (-(s + t)).toProd.2 = (-t + -s).toProd.2

Tactic:
neg_add_rev _ _

Premises used: neg_add_rev
-- 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 : NonemptyInterval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s t : NonemptyInterval α
⊢ (-(s + t)).toProd.2 = (-t + -s).toProd.2

Tactic:
exact neg_add_rev _ _

Premises used: neg_add_rev
-- 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 : NonemptyInterval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s t : NonemptyInterval α
h : s + t = 0
obtain :
  ∀ (a b : α) (hab : a + b = 0) (h : HAdd.hAdd (α := NonemptyInterval α) (pure a) (pure b) = 0),
    Eq (α := NonemptyInterval α) (-pure a) (pure b)
⊢ -s = t

Tactic:
obtain ⟨a, b, rfl, rfl, hab⟩ := NonemptyInterval.add_eq_zero_iff.1 h

Premises used: NonemptyInterval.add_eq_zero_iff, Iff.mp, 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 : NonemptyInterval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
a b : α
hab : a + b = 0
h : HAdd.hAdd (α := NonemptyInterval α) (pure a) (pure b) = 0
rw : Eq (α := NonemptyInterval α) (pure (-a)) (pure b)
rw₁ rw₂ : Eq (α := NonemptyInterval α) (pure b) (pure b)
⊢ Eq (α := NonemptyInterval α) (-pure a) (pure b)

Tactic:
rw [neg_pure, neg_eq_of_add_eq_zero_right hab]

Premises used: NonemptyInterval.neg_pure, 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_1 t_1 s t : NonemptyInterval α
⊢ s / t = s * t⁻¹

Tactic:
NonemptyInterval.ext (Prod.ext ?_ ?_)

Premises used: NonemptyInterval.ext, Prod.ext
-- 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 s t : NonemptyInterval α
refine_1 : (s / t).toProd.1 = (s * t⁻¹).toProd.1
refine_2 : (s / t).toProd.2 = (s * t⁻¹).toProd.2
⊢ s / t = s * t⁻¹

Tactic:
refine NonemptyInterval.ext (Prod.ext ?_ ?_)

Premises used: NonemptyInterval.ext, Prod.ext
-- 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 s t : NonemptyInterval α
⊢ (s / t).toProd.1 = (s * t⁻¹).toProd.1

Tactic:
div_eq_mul_inv _ _

Premises used: div_eq_mul_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_1 s t : NonemptyInterval α
⊢ (s / t).toProd.1 = (s * t⁻¹).toProd.1

Tactic:
exact div_eq_mul_inv _ _

Premises used: div_eq_mul_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_1 s t : NonemptyInterval α
⊢ (s / t).toProd.2 = (s * t⁻¹).toProd.2

Tactic:
div_eq_mul_inv _ _

Premises used: div_eq_mul_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_1 s t : NonemptyInterval α
⊢ (s / t).toProd.2 = (s * t⁻¹).toProd.2

Tactic:
exact div_eq_mul_inv _ _

Premises used: div_eq_mul_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 s : NonemptyInterval α
toProd : s⁻¹⁻¹.toProd = s.toProd
⊢ s⁻¹⁻¹ = s

Tactic:
apply NonemptyInterval.ext

Premises used: NonemptyInterval.ext
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s_1 t s : NonemptyInterval α
⊢ s⁻¹⁻¹.toProd = s.toProd

Tactic:
inv_inv _

Premises used: 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 s : NonemptyInterval α
⊢ s⁻¹⁻¹.toProd = s.toProd

Tactic:
exact inv_inv _

Premises used: 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_1 s t : NonemptyInterval α
⊢ (s * t)⁻¹ = t⁻¹ * s⁻¹

Tactic:
NonemptyInterval.ext (Prod.ext ?_ ?_)

Premises used: NonemptyInterval.ext, Prod.ext
-- 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 s t : NonemptyInterval α
refine_1 : (s * t)⁻¹.toProd.1 = (t⁻¹ * s⁻¹).toProd.1
refine_2 : (s * t)⁻¹.toProd.2 = (t⁻¹ * s⁻¹).toProd.2
⊢ (s * t)⁻¹ = t⁻¹ * s⁻¹

Tactic:
refine NonemptyInterval.ext (Prod.ext ?_ ?_)

Premises used: NonemptyInterval.ext, Prod.ext
-- 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 s t : NonemptyInterval α
⊢ (s * t)⁻¹.toProd.1 = (t⁻¹ * s⁻¹).toProd.1

Tactic:
mul_inv_rev _ _

Premises used: 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 s t : NonemptyInterval α
⊢ (s * t)⁻¹.toProd.1 = (t⁻¹ * s⁻¹).toProd.1

Tactic:
exact mul_inv_rev _ _

Premises used: 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 s t : NonemptyInterval α
⊢ (s * t)⁻¹.toProd.2 = (t⁻¹ * s⁻¹).toProd.2

Tactic:
mul_inv_rev _ _

Premises used: 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 s t : NonemptyInterval α
⊢ (s * t)⁻¹.toProd.2 = (t⁻¹ * s⁻¹).toProd.2

Tactic:
exact mul_inv_rev _ _

Premises used: 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 s t : NonemptyInterval α
h : s * t = 1
obtain :
  ∀ (a b : α) (hab : a * b = 1) (h : HMul.hMul (α := NonemptyInterval α) (pure a) (pure b) = 1),
    Eq (α := NonemptyInterval α) (pure a)⁻¹ (pure b)
⊢ s⁻¹ = t

Tactic:
obtain ⟨a, b, rfl, rfl, hab⟩ := NonemptyInterval.mul_eq_one_iff.1 h

Premises used: Iff.mp, rfl, NonemptyInterval.mul_eq_one_iff
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : NonemptyInterval α
a b : α
hab : a * b = 1
h : HMul.hMul (α := NonemptyInterval α) (pure a) (pure b) = 1
rw : Eq (α := NonemptyInterval α) (pure a⁻¹) (pure b)
rw₁ rw₂ : Eq (α := NonemptyInterval α) (pure b) (pure b)
⊢ Eq (α := NonemptyInterval α) (pure a)⁻¹ (pure b)

Tactic:
rw [inv_pure, inv_eq_of_mul_eq_one_right hab]

Premises used: inv_eq_of_mul_eq_one_right, NonemptyInterval.inv_pure