awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Hom.TypeTags
Goal:
G : Type u_1
H : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : AddCommMonoid H
inst_3 : PartialOrder H
e : OrderMonoidIso.{u_1, u_2} (Multiplicative G) (Multiplicative H)
h :
  ∀ (a : Multiplicative G),
    Eq.{u_2 + 1} (α := H)
      ((Multiplicative.toAdd : (a : Multiplicative H) → H)
          ((((fun (e : G ≃+o H) ↦
                      {
                        toMulEquiv :=
                          (AddEquiv.toMultiplicative : (a : G ≃+ H) → Multiplicative G ≃* Multiplicative H)
                            (↑e : G ≃+ H),
                        map_le_map_iff' := ⋯ : OrderMonoidIso.{u_1, u_2} (Multiplicative G) (Multiplicative H) })
                    ((fun (e : OrderMonoidIso.{u_1, u_2} (Multiplicative G) (Multiplicative H)) ↦
                        {
                          toAddEquiv :=
                            (Equiv.symm AddEquiv.toMultiplicative : (a : Multiplicative G ≃* Multiplicative H) → G ≃+ H)
                              (↑e : Multiplicative G ≃* Multiplicative H),
                          map_le_map_iff' := ⋯ : G ≃+o H })
                      e) :
                  OrderMonoidIso.{u_1, u_2} (Multiplicative G) (Multiplicative H)) :
                (a : Multiplicative G) → Multiplicative H)
              a :
            Multiplicative H) :
        H)
      ((Multiplicative.toAdd : (a : Multiplicative H) → H)
          ((e : (a : Multiplicative G) → Multiplicative H) a : Multiplicative H) :
        H)
⊢ (fun (e : G ≃+o H) ↦
        { toMulEquiv := (AddEquiv.toMultiplicative : (a : G ≃+ H) → Multiplicative G ≃* Multiplicative H) (↑e : G ≃+ H),
          map_le_map_iff' := ⋯ : OrderMonoidIso.{u_1, u_2} (Multiplicative G) (Multiplicative H) })
      ((fun (e : OrderMonoidIso.{u_1, u_2} (Multiplicative G) (Multiplicative H)) ↦
          {
            toAddEquiv :=
              (Equiv.symm AddEquiv.toMultiplicative : (a : Multiplicative G ≃* Multiplicative H) → G ≃+ H)
                (↑e : Multiplicative G ≃* Multiplicative H),
            map_le_map_iff' := ⋯ : G ≃+o H })
        e) =
    e

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Hom.TypeTags
Goal:
G : Type u_1
H : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : AddCommMonoid H
inst_3 : PartialOrder H
e : OrderMonoidIso.{u_1, u_2} (Multiplicative G) (Multiplicative H)
a : Multiplicative G
⊢ Eq.{u_2 + 1} (α := H)
    ((Multiplicative.toAdd : (a : Multiplicative H) → H)
        ((((fun (e : G ≃+o H) ↦
                    {
                      toMulEquiv :=
                        (AddEquiv.toMultiplicative : (a : G ≃+ H) → Multiplicative G ≃* Multiplicative H) (↑e : G ≃+ H),
                      map_le_map_iff' := ⋯ : OrderMonoidIso.{u_1, u_2} (Multiplicative G) (Multiplicative H) })
                  ((fun (e : OrderMonoidIso.{u_1, u_2} (Multiplicative G) (Multiplicative H)) ↦
                      {
                        toAddEquiv :=
                          (Equiv.symm AddEquiv.toMultiplicative : (a : Multiplicative G ≃* Multiplicative H) → G ≃+ H)
                            (↑e : Multiplicative G ≃* Multiplicative H),
                        map_le_map_iff' := ⋯ : G ≃+o H })
                    e) :
                OrderMonoidIso.{u_1, u_2} (Multiplicative G) (Multiplicative H)) :
              (a : Multiplicative G) → Multiplicative H)
            a :
          Multiplicative H) :
      H)
    ((Multiplicative.toAdd : (a : Multiplicative H) → H)
        ((e : (a : Multiplicative G) → Multiplicative H) a : Multiplicative H) :
      H)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Hom.TypeTags
Goal:
G : Type u_1
H : Type u_2
inst : CommMonoid G
inst_1 : PartialOrder G
inst_2 : AddCommMonoid H
inst_3 : PartialOrder H
e : OrderAddMonoidIso.{u_1, u_2} (Additive G) H
⊢ ∀ {a b : G},
    LE.le.{u_2} (α := Multiplicative H)
        (Equiv.toFun
          (MulEquiv.toEquiv
            ((AddEquiv.toMultiplicativeRight : (a : Additive G ≃+ H) → G ≃* Multiplicative H) e.toAddEquiv))
          a)
        (Equiv.toFun
          (MulEquiv.toEquiv
            ((AddEquiv.toMultiplicativeRight : (a : Additive G ≃+ H) → G ≃* Multiplicative H) e.toAddEquiv))
          b) ↔
      a ≤ b

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Hom.TypeTags
Goal:
G : Type u_1
H : Type u_2
inst : CommMonoid G
inst_1 : PartialOrder G
inst_2 : AddCommMonoid H
inst_3 : PartialOrder H
e : OrderMonoidIso.{u_1, u_2} G (Multiplicative H)
⊢ ∀ {a b : Additive G},
    LE.le.{u_2} (α := H)
        (Equiv.toFun
          (AddEquiv.toEquiv ((MulEquiv.toAdditiveLeft : (a : G ≃* Multiplicative H) → Additive G ≃+ H) e.toMulEquiv)) a)
        (Equiv.toFun
          (AddEquiv.toEquiv ((MulEquiv.toAdditiveLeft : (a : G ≃* Multiplicative H) → Additive G ≃+ H) e.toMulEquiv))
          b) ↔
      a ≤ b

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Hom.TypeTags
Goal:
G : Type u_1
H : Type u_2
inst : CommMonoid G
inst_1 : PartialOrder G
inst_2 : AddCommMonoid H
inst_3 : PartialOrder H
e : OrderAddMonoidIso.{u_1, u_2} (Additive G) H
h :
  ∀ (a : Additive G),
    Eq.{u_2 + 1} (α := H)
      (((fun (e : OrderMonoidIso.{u_1, u_2} G (Multiplicative H)) ↦
                { toAddEquiv := (MulEquiv.toAdditiveLeft : (a : G ≃* Multiplicative H) → Additive G ≃+ H) e.toMulEquiv,
                  map_le_map_iff' := ⋯ : OrderAddMonoidIso.{u_1, u_2} (Additive G) H })
              ((fun (e : OrderAddMonoidIso.{u_1, u_2} (Additive G) H) ↦
                  {
                    toMulEquiv :=
                      (AddEquiv.toMultiplicativeRight : (a : Additive G ≃+ H) → G ≃* Multiplicative H) e.toAddEquiv,
                    map_le_map_iff' := ⋯ : OrderMonoidIso.{u_1, u_2} G (Multiplicative H) })
                e) :
            (a : Additive G) → H)
          a :
        H)
      ((e : (a : Additive G) → H) a : H)
⊢ (fun (e : OrderMonoidIso.{u_1, u_2} G (Multiplicative H)) ↦
        { toAddEquiv := (MulEquiv.toAdditiveLeft : (a : G ≃* Multiplicative H) → Additive G ≃+ H) e.toMulEquiv,
          map_le_map_iff' := ⋯ : OrderAddMonoidIso.{u_1, u_2} (Additive G) H })
      ((fun (e : OrderAddMonoidIso.{u_1, u_2} (Additive G) H) ↦
          { toMulEquiv := (AddEquiv.toMultiplicativeRight : (a : Additive G ≃+ H) → G ≃* Multiplicative H) e.toAddEquiv,
            map_le_map_iff' := ⋯ : OrderMonoidIso.{u_1, u_2} G (Multiplicative H) })
        e) =
    e

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Hom.TypeTags
Goal:
G : Type u_1
H : Type u_2
inst : CommMonoid G
inst_1 : PartialOrder G
inst_2 : AddCommMonoid H
inst_3 : PartialOrder H
e : OrderAddMonoidIso.{u_1, u_2} (Additive G) H
a : Additive G
⊢ Eq.{u_2 + 1} (α := H)
    (((fun (e : OrderMonoidIso.{u_1, u_2} G (Multiplicative H)) ↦
              { toAddEquiv := (MulEquiv.toAdditiveLeft : (a : G ≃* Multiplicative H) → Additive G ≃+ H) e.toMulEquiv,
                map_le_map_iff' := ⋯ : OrderAddMonoidIso.{u_1, u_2} (Additive G) H })
            ((fun (e : OrderAddMonoidIso.{u_1, u_2} (Additive G) H) ↦
                {
                  toMulEquiv :=
                    (AddEquiv.toMultiplicativeRight : (a : Additive G ≃+ H) → G ≃* Multiplicative H) e.toAddEquiv,
                  map_le_map_iff' := ⋯ : OrderMonoidIso.{u_1, u_2} G (Multiplicative H) })
              e) :
          (a : Additive G) → H)
        a :
      H)
    ((e : (a : Additive G) → H) a : H)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Hom.TypeTags
Goal:
G : Type u_1
H : Type u_2
inst : CommMonoid G
inst_1 : PartialOrder G
inst_2 : AddCommMonoid H
inst_3 : PartialOrder H
e : OrderMonoidIso.{u_1, u_2} G (Multiplicative H)
h :
  ∀ (a : G),
    Eq.{u_2 + 1} (α := H)
      ((Multiplicative.toAdd : (a : Multiplicative H) → H)
          ((((fun (e : OrderAddMonoidIso.{u_1, u_2} (Additive G) H) ↦
                      {
                        toMulEquiv :=
                          (AddEquiv.toMultiplicativeRight : (a : Additive G ≃+ H) → G ≃* Multiplicative H) e.toAddEquiv,
                        map_le_map_iff' := ⋯ : OrderMonoidIso.{u_1, u_2} G (Multiplicative H) })
                    ((fun (e : OrderMonoidIso.{u_1, u_2} G (Multiplicative H)) ↦
                        {
                          toAddEquiv :=
                            (MulEquiv.toAdditiveLeft : (a : G ≃* Multiplicative H) → Additive G ≃+ H) e.toMulEquiv,
                          map_le_map_iff' := ⋯ : OrderAddMonoidIso.{u_1, u_2} (Additive G) H })
                      e) :
                  OrderMonoidIso.{u_1, u_2} G (Multiplicative H)) :
                (a : G) → Multiplicative H)
              a :
            Multiplicative H) :
        H)
      ((Multiplicative.toAdd : (a : Multiplicative H) → H) ((e : (a : G) → Multiplicative H) a : Multiplicative H) : H)
⊢ (fun (e : OrderAddMonoidIso.{u_1, u_2} (Additive G) H) ↦
        { toMulEquiv := (AddEquiv.toMultiplicativeRight : (a : Additive G ≃+ H) → G ≃* Multiplicative H) e.toAddEquiv,
          map_le_map_iff' := ⋯ : OrderMonoidIso.{u_1, u_2} G (Multiplicative H) })
      ((fun (e : OrderMonoidIso.{u_1, u_2} G (Multiplicative H)) ↦
          { toAddEquiv := (MulEquiv.toAdditiveLeft : (a : G ≃* Multiplicative H) → Additive G ≃+ H) e.toMulEquiv,
            map_le_map_iff' := ⋯ : OrderAddMonoidIso.{u_1, u_2} (Additive G) H })
        e) =
    e

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Hom.TypeTags
Goal:
G : Type u_1
H : Type u_2
inst : CommMonoid G
inst_1 : PartialOrder G
inst_2 : AddCommMonoid H
inst_3 : PartialOrder H
e : OrderMonoidIso.{u_1, u_2} G (Multiplicative H)
a : G
⊢ Eq.{u_2 + 1} (α := H)
    ((Multiplicative.toAdd : (a : Multiplicative H) → H)
        ((((fun (e : OrderAddMonoidIso.{u_1, u_2} (Additive G) H) ↦
                    {
                      toMulEquiv :=
                        (AddEquiv.toMultiplicativeRight : (a : Additive G ≃+ H) → G ≃* Multiplicative H) e.toAddEquiv,
                      map_le_map_iff' := ⋯ : OrderMonoidIso.{u_1, u_2} G (Multiplicative H) })
                  ((fun (e : OrderMonoidIso.{u_1, u_2} G (Multiplicative H)) ↦
                      {
                        toAddEquiv :=
                          (MulEquiv.toAdditiveLeft : (a : G ≃* Multiplicative H) → Additive G ≃+ H) e.toMulEquiv,
                        map_le_map_iff' := ⋯ : OrderAddMonoidIso.{u_1, u_2} (Additive G) H })
                    e) :
                OrderMonoidIso.{u_1, u_2} G (Multiplicative H)) :
              (a : G) → Multiplicative H)
            a :
          Multiplicative H) :
      H)
    ((Multiplicative.toAdd : (a : Multiplicative H) → H) ((e : (a : G) → Multiplicative H) a : Multiplicative H) : H)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Hom.TypeTags
Goal:
G : Type u_1
H : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CommMonoid H
inst_3 : PartialOrder H
e : OrderAddMonoidIso.{u_1, u_2} G (Additive H)
⊢ ∀ {a b : Multiplicative G},
    LE.le.{u_2} (α := H)
        (Equiv.toFun
          (MulEquiv.toEquiv
            ((AddEquiv.toMultiplicativeLeft : (a : G ≃+ Additive H) → Multiplicative G ≃* H) e.toAddEquiv))
          a)
        (Equiv.toFun
          (MulEquiv.toEquiv
            ((AddEquiv.toMultiplicativeLeft : (a : G ≃+ Additive H) → Multiplicative G ≃* H) e.toAddEquiv))
          b) ↔
      a ≤ b

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Hom.TypeTags
Goal:
G : Type u_1
H : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CommMonoid H
inst_3 : PartialOrder H
e : OrderMonoidIso.{u_1, u_2} (Multiplicative G) H
⊢ ∀ {a b : G},
    LE.le.{u_2} (α := Additive H)
        (Equiv.toFun
          (AddEquiv.toEquiv ((MulEquiv.toAdditiveRight : (a : Multiplicative G ≃* H) → G ≃+ Additive H) e.toMulEquiv))
          a)
        (Equiv.toFun
          (AddEquiv.toEquiv ((MulEquiv.toAdditiveRight : (a : Multiplicative G ≃* H) → G ≃+ Additive H) e.toMulEquiv))
          b) ↔
      a ≤ b

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Hom.TypeTags
Goal:
G : Type u_1
H : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CommMonoid H
inst_3 : PartialOrder H
e : OrderAddMonoidIso.{u_1, u_2} G (Additive H)
h :
  ∀ (a : G),
    Eq.{u_2 + 1} (α := H)
      ((Additive.toMul : (a : Additive H) → H)
          ((((fun (e : OrderMonoidIso.{u_1, u_2} (Multiplicative G) H) ↦
                      {
                        toAddEquiv :=
                          (MulEquiv.toAdditiveRight : (a : Multiplicative G ≃* H) → G ≃+ Additive H) e.toMulEquiv,
                        map_le_map_iff' := ⋯ : OrderAddMonoidIso.{u_1, u_2} G (Additive H) })
                    ((fun (e : OrderAddMonoidIso.{u_1, u_2} G (Additive H)) ↦
                        {
                          toMulEquiv :=
                            (AddEquiv.toMultiplicativeLeft : (a : G ≃+ Additive H) → Multiplicative G ≃* H)
                              e.toAddEquiv,
                          map_le_map_iff' := ⋯ : OrderMonoidIso.{u_1, u_2} (Multiplicative G) H })
                      e) :
                  OrderAddMonoidIso.{u_1, u_2} G (Additive H)) :
                (a : G) → Additive H)
              a :
            Additive H) :
        H)
      ((Additive.toMul : (a : Additive H) → H) ((e : (a : G) → Additive H) a : Additive H) : H)
⊢ (fun (e : OrderMonoidIso.{u_1, u_2} (Multiplicative G) H) ↦
        { toAddEquiv := (MulEquiv.toAdditiveRight : (a : Multiplicative G ≃* H) → G ≃+ Additive H) e.toMulEquiv,
          map_le_map_iff' := ⋯ : OrderAddMonoidIso.{u_1, u_2} G (Additive H) })
      ((fun (e : OrderAddMonoidIso.{u_1, u_2} G (Additive H)) ↦
          { toMulEquiv := (AddEquiv.toMultiplicativeLeft : (a : G ≃+ Additive H) → Multiplicative G ≃* H) e.toAddEquiv,
            map_le_map_iff' := ⋯ : OrderMonoidIso.{u_1, u_2} (Multiplicative G) H })
        e) =
    e

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Hom.TypeTags
Goal:
G : Type u_1
H : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CommMonoid H
inst_3 : PartialOrder H
e : OrderAddMonoidIso.{u_1, u_2} G (Additive H)
a : G
⊢ Eq.{u_2 + 1} (α := H)
    ((Additive.toMul : (a : Additive H) → H)
        ((((fun (e : OrderMonoidIso.{u_1, u_2} (Multiplicative G) H) ↦
                    {
                      toAddEquiv :=
                        (MulEquiv.toAdditiveRight : (a : Multiplicative G ≃* H) → G ≃+ Additive H) e.toMulEquiv,
                      map_le_map_iff' := ⋯ : OrderAddMonoidIso.{u_1, u_2} G (Additive H) })
                  ((fun (e : OrderAddMonoidIso.{u_1, u_2} G (Additive H)) ↦
                      {
                        toMulEquiv :=
                          (AddEquiv.toMultiplicativeLeft : (a : G ≃+ Additive H) → Multiplicative G ≃* H) e.toAddEquiv,
                        map_le_map_iff' := ⋯ : OrderMonoidIso.{u_1, u_2} (Multiplicative G) H })
                    e) :
                OrderAddMonoidIso.{u_1, u_2} G (Additive H)) :
              (a : G) → Additive H)
            a :
          Additive H) :
      H)
    ((Additive.toMul : (a : Additive H) → H) ((e : (a : G) → Additive H) a : Additive H) : H)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Hom.TypeTags
Goal:
G : Type u_1
H : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CommMonoid H
inst_3 : PartialOrder H
e : OrderMonoidIso.{u_1, u_2} (Multiplicative G) H
h :
  ∀ (a : Multiplicative G),
    Eq.{u_2 + 1} (α := H)
      (((fun (e : OrderAddMonoidIso.{u_1, u_2} G (Additive H)) ↦
                {
                  toMulEquiv :=
                    (AddEquiv.toMultiplicativeLeft : (a : G ≃+ Additive H) → Multiplicative G ≃* H) e.toAddEquiv,
                  map_le_map_iff' := ⋯ : OrderMonoidIso.{u_1, u_2} (Multiplicative G) H })
              ((fun (e : OrderMonoidIso.{u_1, u_2} (Multiplicative G) H) ↦
                  {
                    toAddEquiv :=
                      (MulEquiv.toAdditiveRight : (a : Multiplicative G ≃* H) → G ≃+ Additive H) e.toMulEquiv,
                    map_le_map_iff' := ⋯ : OrderAddMonoidIso.{u_1, u_2} G (Additive H) })
                e) :
            (a : Multiplicative G) → H)
          a :
        H)
      ((e : (a : Multiplicative G) → H) a : H)
⊢ (fun (e : OrderAddMonoidIso.{u_1, u_2} G (Additive H)) ↦
        { toMulEquiv := (AddEquiv.toMultiplicativeLeft : (a : G ≃+ Additive H) → Multiplicative G ≃* H) e.toAddEquiv,
          map_le_map_iff' := ⋯ : OrderMonoidIso.{u_1, u_2} (Multiplicative G) H })
      ((fun (e : OrderMonoidIso.{u_1, u_2} (Multiplicative G) H) ↦
          { toAddEquiv := (MulEquiv.toAdditiveRight : (a : Multiplicative G ≃* H) → G ≃+ Additive H) e.toMulEquiv,
            map_le_map_iff' := ⋯ : OrderAddMonoidIso.{u_1, u_2} G (Additive H) })
        e) =
    e

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Hom.TypeTags
Goal:
G : Type u_1
H : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CommMonoid H
inst_3 : PartialOrder H
e : OrderMonoidIso.{u_1, u_2} (Multiplicative G) H
a : Multiplicative G
⊢ Eq.{u_2 + 1} (α := H)
    (((fun (e : OrderAddMonoidIso.{u_1, u_2} G (Additive H)) ↦
              {
                toMulEquiv :=
                  (AddEquiv.toMultiplicativeLeft : (a : G ≃+ Additive H) → Multiplicative G ≃* H) e.toAddEquiv,
                map_le_map_iff' := ⋯ : OrderMonoidIso.{u_1, u_2} (Multiplicative G) H })
            ((fun (e : OrderMonoidIso.{u_1, u_2} (Multiplicative G) H) ↦
                { toAddEquiv := (MulEquiv.toAdditiveRight : (a : Multiplicative G ≃* H) → G ≃+ Additive H) e.toMulEquiv,
                  map_le_map_iff' := ⋯ : OrderAddMonoidIso.{u_1, u_2} G (Additive H) })
              e) :
          (a : Multiplicative G) → H)
        a :
      H)
    ((e : (a : Multiplicative G) → H) a : H)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Hom.Units
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Monoid α
inst_2 : Preorder β
inst_3 : Monoid β
e : α ≃*o β
x y : αˣ
⊢ (Units.mapEquiv e.toMulEquiv).toFun x ≤ (Units.mapEquiv e.toMulEquiv).toFun y ↔ x ≤ y

Tactic:
simp [← Units.val_le_val]

Premises used: Units.val_le_val
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : One α
⊢ Eq.{u_2 + 1} (α := α × α) (toProd 1) 1

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: Interval.pure, rfl
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : One α
⊢ Ne.{u_2 + 1} (α := Interval α) 1 ⊥

Tactic:
pure_ne_bot

Premises used: Interval.pure, Interval.pure_ne_bot
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : One α
⊢ Ne.{u_2 + 1} (α := Interval α) ⊥ 1

Tactic:
bot_ne_pure

Premises used: Interval.pure, Interval.bot_ne_pure
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : One α
⊢ (↑1 : Set α) = 1

Tactic:
coe_pure _

Premises used: NonemptyInterval.coe_pure
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : One α
⊢ Membership.mem (γ := NonemptyInterval α) 1 1

Tactic:
⟨le_rfl, le_rfl⟩

Premises used: le_rfl, Set.Mem, setOf, Set.Icc, And.intro
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : One α
⊢ (↑1 : Set α) = 1

Tactic:
Icc_self _

Premises used: Set.Icc_self, setOf, Set.Icc
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : One α
⊢ Membership.mem (γ := Interval α) 1 1

Tactic:
⟨le_rfl, le_rfl⟩

Premises used: le_rfl, Set.Mem, setOf, Set.Icc, And.intro
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : Mul α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
s t : NonemptyInterval α
⊢ (s * t).toProd = s.toProd * t.toProd

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : Mul α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
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 : Mul α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b : α
⊢ HMul.hMul (α := 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 : Mul α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
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 : Mul α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
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 : Monoid α
inst_1 : Preorder α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
s : NonemptyInterval α
n : ℕ
⊢ (s ^ n).toProd = s.toProd ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : Monoid α
inst_1 : Preorder α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
s : NonemptyInterval α
n : ℕ
⊢ (s ^ n).toProd.1 = s.toProd.1 ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : Monoid α
inst_1 : Preorder α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
s : NonemptyInterval α
n : ℕ
⊢ (s ^ n).toProd.2 = s.toProd.2 ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
α : Type u_2
inst : Monoid α
inst_1 : Preorder α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a : α
n : ℕ
⊢ HPow.hPow (α := NonemptyInterval α) (pure a) n = pure (a ^ n)

Tactic:
rfl

Premises used: NonemptyInterval.pure, rfl
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Interval α
simp_rw : WithBot.map (fun (b : NonemptyInterval α) ↦ b) s = s
simp_rw₁ : WithBot.map id s = s
simp_rw₂ : id s = s
⊢ WithBot.map (fun (b : NonemptyInterval α) ↦ 1 * b) s = s

Tactic:
simp_rw [one_mul, ← Function.id_def, WithBot.map_id, id]

Premises used: Function.id_def, id, WithBot.map_id, one_mul
-- Module: Mathlib.Algebra.Order.Interval.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Interval α
simp_rw : WithBot.map (fun (x : NonemptyInterval α) ↦ x) s = s
simp_rw₁ : WithBot.map id s = s
simp_rw₂ : id s = s
⊢ WithBot.map (fun (x : NonemptyInterval α) ↦ x * 1) s = s

Tactic:
simp_rw [mul_one, ← Function.id_def, WithBot.map_id, id]

Premises used: Function.id_def, id, mul_one, WithBot.map_id