awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : Mul α
inst_1 : Add α
inst_2 : LE α
inst_3 : Mul β
inst_4 : Add β
inst_5 : LE β
inst_6 : Mul γ
inst_7 : Add γ
inst_8 : LE γ
f g : α ≃+*o β
h₁ : f.toFun = g.toFun
h₂ : f.invFun = g.invFun
obtain :
  ∀ (toFun : α → β) (invFun : β → α) (left_inv : LeftInverse invFun toFun) (right_inv : RightInverse invFun toFun)
    (map_mul' :
      ∀ (x y : α),
        { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ β }.toFun (x * y) =
          { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ β }.toFun x *
            { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ β }.toFun y)
    (map_add' :
      ∀ (x y : α),
        { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ β }.toFun (x + y) =
          { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ β }.toFun x +
            { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ β }.toFun y)
    (map_le_map_iff' :
      ∀ {a b : α},
        { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
                  map_add' := map_add' : α ≃+* β }.toFun
              a ≤
            { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
                  map_add' := map_add' : α ≃+* β }.toFun
              b ↔
          a ≤ b)
    (h₁ :
      { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
            map_add' := map_add', map_le_map_iff' := @map_le_map_iff' : α ≃+*o β }.toFun =
        g.toFun)
    (h₂ :
      { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
            map_add' := map_add', map_le_map_iff' := @map_le_map_iff' : α ≃+*o β }.invFun =
        g.invFun),
    { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
        map_add' := map_add', map_le_map_iff' := @map_le_map_iff' : α ≃+*o β } =
      g
⊢ f = g

Tactic:
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Add α
inst_2 : LE α
inst_3 : Mul β
inst_4 : Add β
inst_5 : LE β
f : α ≃+*o β
⊢ f.toFun = (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Add α
inst_2 : LE α
inst_3 : Mul β
inst_4 : Add β
inst_5 : LE β
f g : α ≃+*o β
h : ∀ (a : α), Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) ((g : (a : α) → β) a : β)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Add α
inst_2 : LE α
inst_3 : Mul β
inst_4 : Add β
inst_5 : LE β
e : α ≃+* β
h : ∀ {a b : α}, e.toFun a ≤ e.toFun b ↔ a ≤ b
⊢ Eq (α := (a : α) → β) (⇑{ toRingEquiv := e, map_le_map_iff' := @h : α ≃+*o β } : (a : α) → β) (⇑e : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Add α
inst_2 : LE α
inst_3 : Mul β
inst_4 : Add β
inst_5 : LE β
e : α ≃+*o β
h : ∀ {a b : α}, e.toFun a ≤ e.toFun b ↔ a ≤ b
⊢ { toRingEquiv := e.toRingEquiv, map_le_map_iff' := @h : α ≃+*o β } = e

Tactic:
ext fun _ => rfl

Premises used: OrderRingIso.ext, rfl
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Add α
inst_2 : LE α
inst_3 : Mul β
inst_4 : Add β
inst_5 : LE β
f : α ≃+*o β
⊢ f.toRingEquiv = f.toRingEquiv

Tactic:
RingEquiv.ext fun _ => rfl

Premises used: RingEquiv.ext, rfl
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Add α
inst_2 : LE α
inst_3 : Mul β
inst_4 : Add β
inst_5 : LE β
f : α ≃+*o β
⊢ (↑f : α ≃o β) = (↑f : α ≃o β)

Tactic:
OrderIso.ext rfl

Premises used: OrderIso.ext, rfl
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Add α
inst_2 : LE α
inst_3 : Mul β
inst_4 : Add β
inst_5 : LE β
f : α ≃+*o β
⊢ Eq (α := (a : α) → β) (⇑f.toRingEquiv : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Add α
inst_2 : LE α
inst_3 : Mul β
inst_4 : Add β
inst_5 : LE β
f : α ≃+*o β
⊢ Eq (α := (a : α) → β) (⇑(↑f : α ≃o β) : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
α : Type u_2
inst : Mul α
inst_1 : Add α
inst_2 : LE α
x : α
⊢ (OrderRingIso.refl α : (a : α) → α) x = x

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
α : Type u_2
inst : Mul α
inst_1 : Add α
inst_2 : LE α
⊢ Eq (α := α ≃+* α) (toRingEquiv (OrderRingIso.refl α)) (RingEquiv.refl α)

Tactic:
rfl

Premises used: RingEquiv.refl, rfl
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
α : Type u_2
inst : Mul α
inst_1 : Add α
inst_2 : LE α
⊢ Eq (α := α ≃o α) (↑(OrderRingIso.refl α) : α ≃o α) (OrderIso.refl α)

Tactic:
rfl

Premises used: RelIso.refl, Equiv.refl, rfl, OrderIso.refl
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : Mul α
inst_1 : Add α
inst_2 : LE α
inst_3 : Mul β
inst_4 : Add β
inst_5 : LE β
inst_6 : Mul γ
inst_7 : Add γ
inst_8 : LE γ
e : α ≃+*o β
a b : β
erw : LE.le.{u_3} (α := β) ((e : (a : α) → β) (e.symm.toFun a) : β) ((e : (a : α) → β) (e.symm.toFun b) : β) ↔ a ≤ b
erw₁ : a ≤ (e : (a : α) → β) (e.symm.toFun b) ↔ a ≤ b
erw₂ erw₃ : a ≤ b ↔ a ≤ b
⊢ e.symm.toFun a ≤ e.symm.toFun b ↔ a ≤ b

Tactic:
erw [← map_le_map_iff e, e.1.apply_symm_apply, e.1.apply_symm_apply]

Premises used: OrderIsoClass.map_le_map_iff, RingEquiv.apply_symm_apply, OrderRingIso.toRingEquiv
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Add α
inst_2 : LE α
inst_3 : Mul β
inst_4 : Add β
inst_5 : LE β
e : α ≃+*o β
⊢ e.symm.symm = e

Tactic:
rfl

Premises used: OrderRingIso.symm, Equiv.symm, RingEquiv.symm, rfl
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Add α
inst_2 : LE α
inst_3 : Mul β
inst_4 : Add β
inst_5 : LE β
⊢ Bijective (α := α ≃+*o β) OrderRingIso.symm

Tactic:
Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Premises used: Iff.mpr, OrderRingIso.symm_symm, Function.bijective_iff_has_inverse, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Add α
inst_2 : LE α
inst_3 : Mul β
inst_4 : Add β
inst_5 : LE β
e : α ≃+*o β
a : α
⊢ (e.symm : (a : β) → α) ((e : (a : α) → β) a : β) = a

Tactic:
e.toRingEquiv.symm_apply_apply a

Premises used: RingEquiv.symm_apply_apply, OrderRingIso.toRingEquiv
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Add α
inst_2 : LE α
inst_3 : Mul β
inst_4 : Add β
inst_5 : LE β
e : α ≃+*o β
b : β
⊢ (e : (a : α) → β) ((e.symm : (a : β) → α) b : α) = b

Tactic:
e.toRingEquiv.apply_symm_apply b

Premises used: RingEquiv.apply_symm_apply, OrderRingIso.toRingEquiv
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Mul α
inst_1 : Add α
inst_2 : LE α
inst_3 : Mul β
inst_4 : Add β
inst_5 : LE β
inst_6 : Mul γ
inst_7 : Add γ
inst_8 : LE γ
f : α ≃+*o β
g : β ≃+*o γ
⊢ (f.trans g).toRingEquiv = f.trans g.toRingEquiv

Tactic:
rfl

Premises used: RingEquiv.trans, rfl
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Mul α
inst_1 : Add α
inst_2 : LE α
inst_3 : Mul β
inst_4 : Add β
inst_5 : LE β
inst_6 : Mul γ
inst_7 : Add γ
inst_8 : LE γ
f : α ≃+*o β
g : β ≃+*o γ
⊢ (↑(f.trans g) : α ≃+* γ) = f.trans g.toRingEquiv

Tactic:
rfl

Premises used: Equiv.trans, RingEquiv.trans, rfl
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Mul α
inst_1 : Add α
inst_2 : LE α
inst_3 : Mul β
inst_4 : Add β
inst_5 : LE β
inst_6 : Mul γ
inst_7 : Add γ
inst_8 : LE γ
f : α ≃+*o β
g : β ≃+*o γ
a : α
⊢ Eq.{u_4 + 1} (α := γ) ((f.trans g : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f : (a : α) → β) a : β) : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Add α
inst_2 : LE α
inst_3 : Mul β
inst_4 : Add β
inst_5 : LE β
e : α ≃+*o β
⊢ e.trans e.symm = OrderRingIso.refl α

Tactic:
ext e.left_inv

Premises used: RingEquiv.toEquiv, OrderRingIso.ext, OrderRingIso.toRingEquiv, Equiv.left_inv
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
α : Type u_2
β : Type u_3
inst : Mul α
inst_1 : Add α
inst_2 : LE α
inst_3 : Mul β
inst_4 : Add β
inst_5 : LE β
e : α ≃+*o β
⊢ e.symm.trans e = OrderRingIso.refl β

Tactic:
ext e.right_inv

Premises used: RingEquiv.toEquiv, Equiv.right_inv, OrderRingIso.ext, OrderRingIso.toRingEquiv
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
R : Type u_6
S : Type u_7
inst : Mul R
inst_1 : Add R
inst_2 : Mul S
inst_3 : Add S
inst_4 : Preorder R
inst_5 : Preorder S
e : R ≃+*o S
x : R
y : S
⊢ x < (e.symm : (a : S) → R) y ↔ (e : (a : R) → S) x < y

Tactic:
simpa using e.toOrderIso.lt_symm_apply

Premises used: OrderRingIso.toOrderIso, OrderIso.lt_symm_apply
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
R : Type u_6
S : Type u_7
inst : Mul R
inst_1 : Add R
inst_2 : Mul S
inst_3 : Add S
inst_4 : Preorder R
inst_5 : Preorder S
e : R ≃+*o S
x : R
y : S
⊢ (e.symm : (a : S) → R) y < x ↔ y < (e : (a : R) → S) x

Tactic:
simpa using e.toOrderIso.symm_apply_lt

Premises used: OrderRingIso.toOrderIso, OrderIso.symm_apply_lt
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
α : Type u_2
β : Type u_3
inst : NonAssocSemiring α
inst_1 : Preorder α
inst_2 : NonAssocSemiring β
inst_3 : Preorder β
f : α ≃+*o β
⊢ f.toOrderRingHom = (↑f : α →+*o β)

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, MulEquiv.toMonoidHom, RingHomClass.toRingHom, RingEquiv.toRingHom, OrderRingIso.toOrderRingHom, OrderRingHomClass.toOrderRingHom, rfl
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
α : Type u_2
β : Type u_3
inst : NonAssocSemiring α
inst_1 : Preorder α
inst_2 : NonAssocSemiring β
inst_3 : Preorder β
f : α ≃+*o β
⊢ Eq (α := (a : α) → β) (⇑(↑f : α →+*o β) : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
α : Type u_2
inst : NonAssocSemiring α
inst_1 : Preorder α
⊢ Eq (α := α →+*o α) (↑(OrderRingIso.refl α) : α →+*o α) (OrderRingHom.id α)

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, OrderRingHom.id, OrderRingHomClass.toOrderRingHom, rfl
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
α : Type u_2
β : Type u_3
inst : NonAssocSemiring α
inst_1 : Preorder α
inst_2 : NonAssocSemiring β
inst_3 : Preorder β
f g : α ≃+*o β
h : f.toOrderRingHom = g.toOrderRingHom
⊢ Eq (α := (a : α) → β) (⇑f.toOrderRingHom : (a : α) → β) (⇑g.toOrderRingHom : (a : α) → β)

Tactic:
DFunLike.ext'_iff.1 h

Premises used: DFunLike.ext'_iff, Iff.mp
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
α : Type u_2
β : Type u_3
inst : NonAssocSemiring α
inst_1 : Preorder α
inst_2 : NonAssocSemiring β
inst_3 : Preorder β
f g : α ≃+*o β
h : f.toOrderRingHom = g.toOrderRingHom
⊢ Eq (α := (a : α) → β) ((fun (f : α ≃+*o β) ↦ ((⇑f : (a : α) → β) : (a : α) → β)) f)
    ((fun (f : α ≃+*o β) ↦ ((⇑f : (a : α) → β) : (a : α) → β)) g)

Tactic:
convert! DFunLike.ext'_iff.1 h using 0

Premises used: DFunLike.ext'_iff, Iff.mp
-- Module: Mathlib.Algebra.Order.Hom.TypeTags
Goal:
G : Type u_1
H : Type u_2
inst : CommMonoid G
inst_1 : PartialOrder G
inst_2 : CommMonoid H
inst_3 : PartialOrder H
e : G ≃*o H
⊢ ∀ {a b : Additive G},
    LE.le.{u_2} (α := Additive H)
        (Equiv.toFun (AddEquiv.toEquiv ((MulEquiv.toAdditive : (a : G ≃* H) → Additive G ≃+ Additive H) (↑e : G ≃* H)))
          a)
        (Equiv.toFun (AddEquiv.toEquiv ((MulEquiv.toAdditive : (a : G ≃* H) → Additive G ≃+ Additive H) (↑e : G ≃* H)))
          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 : CommMonoid H
inst_3 : PartialOrder H
e : OrderAddMonoidIso.{u_1, u_2} (Additive G) (Additive H)
⊢ ∀ {a b : G},
    LE.le.{u_2} (α := H)
        (Equiv.toFun
          (MulEquiv.toEquiv
            ((Equiv.symm MulEquiv.toAdditive : (a : Additive G ≃+ Additive H) → G ≃* H)
              (↑e : Additive G ≃+ Additive H)))
          a)
        (Equiv.toFun
          (MulEquiv.toEquiv
            ((Equiv.symm MulEquiv.toAdditive : (a : Additive G ≃+ Additive H) → G ≃* H)
              (↑e : Additive G ≃+ Additive H)))
          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 : CommMonoid H
inst_3 : PartialOrder H
e : G ≃*o H
h :
  ∀ (a : G),
    Eq.{u_2 + 1} (α := H)
      (((fun (e : OrderAddMonoidIso.{u_1, u_2} (Additive G) (Additive H)) ↦
                {
                  toMulEquiv :=
                    (Equiv.symm MulEquiv.toAdditive : (a : Additive G ≃+ Additive H) → G ≃* H)
                      (↑e : Additive G ≃+ Additive H),
                  map_le_map_iff' := ⋯ : G ≃*o H })
              ((fun (e : G ≃*o H) ↦
                  { toAddEquiv := (MulEquiv.toAdditive : (a : G ≃* H) → Additive G ≃+ Additive H) (↑e : G ≃* H),
                    map_le_map_iff' := ⋯ : OrderAddMonoidIso.{u_1, u_2} (Additive G) (Additive H) })
                e) :
            (a : G) → H)
          a :
        H)
      ((e : (a : G) → H) a : H)
⊢ (fun (e : OrderAddMonoidIso.{u_1, u_2} (Additive G) (Additive H)) ↦
        {
          toMulEquiv :=
            (Equiv.symm MulEquiv.toAdditive : (a : Additive G ≃+ Additive H) → G ≃* H) (↑e : Additive G ≃+ Additive H),
          map_le_map_iff' := ⋯ : G ≃*o H })
      ((fun (e : G ≃*o H) ↦
          { toAddEquiv := (MulEquiv.toAdditive : (a : G ≃* H) → Additive G ≃+ Additive H) (↑e : G ≃* H),
            map_le_map_iff' := ⋯ : OrderAddMonoidIso.{u_1, u_2} (Additive G) (Additive 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 : CommMonoid H
inst_3 : PartialOrder H
e : G ≃*o H
a : G
⊢ Eq.{u_2 + 1} (α := H)
    (((fun (e : OrderAddMonoidIso.{u_1, u_2} (Additive G) (Additive H)) ↦
              {
                toMulEquiv :=
                  (Equiv.symm MulEquiv.toAdditive : (a : Additive G ≃+ Additive H) → G ≃* H)
                    (↑e : Additive G ≃+ Additive H),
                map_le_map_iff' := ⋯ : G ≃*o H })
            ((fun (e : G ≃*o H) ↦
                { toAddEquiv := (MulEquiv.toAdditive : (a : G ≃* H) → Additive G ≃+ Additive H) (↑e : G ≃* H),
                  map_le_map_iff' := ⋯ : OrderAddMonoidIso.{u_1, u_2} (Additive G) (Additive H) })
              e) :
          (a : G) → H)
        a :
      H)
    ((e : (a : 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 : CommMonoid H
inst_3 : PartialOrder H
e : OrderAddMonoidIso.{u_1, u_2} (Additive G) (Additive H)
h :
  ∀ (a : Additive G),
    Eq.{u_2 + 1} (α := H)
      ((Additive.toMul : (a : Additive H) → H)
          ((((fun (e : G ≃*o H) ↦
                      { toAddEquiv := (MulEquiv.toAdditive : (a : G ≃* H) → Additive G ≃+ Additive H) (↑e : G ≃* H),
                        map_le_map_iff' := ⋯ : OrderAddMonoidIso.{u_1, u_2} (Additive G) (Additive H) })
                    ((fun (e : OrderAddMonoidIso.{u_1, u_2} (Additive G) (Additive H)) ↦
                        {
                          toMulEquiv :=
                            (Equiv.symm MulEquiv.toAdditive : (a : Additive G ≃+ Additive H) → G ≃* H)
                              (↑e : Additive G ≃+ Additive H),
                          map_le_map_iff' := ⋯ : G ≃*o H })
                      e) :
                  OrderAddMonoidIso.{u_1, u_2} (Additive G) (Additive H)) :
                (a : Additive G) → Additive H)
              a :
            Additive H) :
        H)
      ((Additive.toMul : (a : Additive H) → H) ((e : (a : Additive G) → Additive H) a : Additive H) : H)
⊢ (fun (e : G ≃*o H) ↦
        { toAddEquiv := (MulEquiv.toAdditive : (a : G ≃* H) → Additive G ≃+ Additive H) (↑e : G ≃* H),
          map_le_map_iff' := ⋯ : OrderAddMonoidIso.{u_1, u_2} (Additive G) (Additive H) })
      ((fun (e : OrderAddMonoidIso.{u_1, u_2} (Additive G) (Additive H)) ↦
          {
            toMulEquiv :=
              (Equiv.symm MulEquiv.toAdditive : (a : Additive G ≃+ Additive H) → G ≃* H)
                (↑e : Additive G ≃+ Additive 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 : CommMonoid G
inst_1 : PartialOrder G
inst_2 : CommMonoid H
inst_3 : PartialOrder H
e : OrderAddMonoidIso.{u_1, u_2} (Additive G) (Additive H)
a : Additive G
⊢ Eq.{u_2 + 1} (α := H)
    ((Additive.toMul : (a : Additive H) → H)
        ((((fun (e : G ≃*o H) ↦
                    { toAddEquiv := (MulEquiv.toAdditive : (a : G ≃* H) → Additive G ≃+ Additive H) (↑e : G ≃* H),
                      map_le_map_iff' := ⋯ : OrderAddMonoidIso.{u_1, u_2} (Additive G) (Additive H) })
                  ((fun (e : OrderAddMonoidIso.{u_1, u_2} (Additive G) (Additive H)) ↦
                      {
                        toMulEquiv :=
                          (Equiv.symm MulEquiv.toAdditive : (a : Additive G ≃+ Additive H) → G ≃* H)
                            (↑e : Additive G ≃+ Additive H),
                        map_le_map_iff' := ⋯ : G ≃*o H })
                    e) :
                OrderAddMonoidIso.{u_1, u_2} (Additive G) (Additive H)) :
              (a : Additive G) → Additive H)
            a :
          Additive H) :
      H)
    ((Additive.toMul : (a : Additive H) → H) ((e : (a : Additive 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 : AddCommMonoid H
inst_3 : PartialOrder H
e : G ≃+o H
⊢ ∀ {a b : Multiplicative G},
    LE.le.{u_2} (α := Multiplicative H)
        (Equiv.toFun
          (MulEquiv.toEquiv
            ((AddEquiv.toMultiplicative : (a : G ≃+ H) → Multiplicative G ≃* Multiplicative H) (↑e : G ≃+ H)))
          a)
        (Equiv.toFun
          (MulEquiv.toEquiv
            ((AddEquiv.toMultiplicative : (a : G ≃+ H) → Multiplicative G ≃* Multiplicative H) (↑e : G ≃+ H)))
          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 : AddCommMonoid H
inst_3 : PartialOrder H
e : OrderMonoidIso.{u_1, u_2} (Multiplicative G) (Multiplicative H)
⊢ ∀ {a b : G},
    LE.le.{u_2} (α := H)
        (Equiv.toFun
          (AddEquiv.toEquiv
            ((Equiv.symm AddEquiv.toMultiplicative : (a : Multiplicative G ≃* Multiplicative H) → G ≃+ H)
              (↑e : Multiplicative G ≃* Multiplicative H)))
          a)
        (Equiv.toFun
          (AddEquiv.toEquiv
            ((Equiv.symm AddEquiv.toMultiplicative : (a : Multiplicative G ≃* Multiplicative H) → G ≃+ H)
              (↑e : Multiplicative G ≃* Multiplicative H)))
          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 : AddCommMonoid H
inst_3 : PartialOrder H
e : G ≃+o H
h :
  ∀ (a : G),
    Eq.{u_2 + 1} (α := 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 })
              ((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) })
                e) :
            (a : G) → H)
          a :
        H)
      ((e : (a : G) → H) a : 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 })
      ((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) })
        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 : G ≃+o H
a : G
⊢ Eq.{u_2 + 1} (α := 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 })
            ((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) })
              e) :
          (a : G) → H)
        a :
      H)
    ((e : (a : G) → H) a : H)

Tactic:
simp