awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst : Group G
inst_1 : PartialOrder G
inst_2 : Group H
inst_3 : PartialOrder H
x_1 : OrderMonoidIso.{u_6, u_7} (WithZero G) (WithZero H)
x : WithZero G
h :
  Eq.{u_7 + 1} (α := WithZero H)
    ((((fun (e : G ≃*o H) ↦
              ({ toMulEquiv := (MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv,
                  map_le_map_iff' := ⋯ } :
                OrderMonoidIso.{u_6, u_7} (WithZero G) (WithZero H)))
            ((fun (e : OrderMonoidIso.{u_6, u_7} (WithZero G) (WithZero H)) ↦
                ({
                    toMulEquiv :=
                      (Equiv.symm MulEquiv.withZero : (a : WithZero G ≃* WithZero H) → G ≃* H)
                        (↑e : WithZero G ≃* WithZero H),
                    map_le_map_iff' := ⋯ } :
                  G ≃*o H))
              x_1) :
          OrderMonoidIso.{u_6, u_7} (WithZero G) (WithZero H)) :
        (a : WithZero G) → WithZero H)
      0)
    ((x_1 : (a : WithZero G) → WithZero H) 0)
h₁ :
  ∀ (a : G),
    Eq.{u_7 + 1} (α := WithZero H)
      ((((fun (e : G ≃*o H) ↦
                  ({ toMulEquiv := (MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv,
                      map_le_map_iff' := ⋯ } :
                    OrderMonoidIso.{u_6, u_7} (WithZero G) (WithZero H)))
                ((fun (e : OrderMonoidIso.{u_6, u_7} (WithZero G) (WithZero H)) ↦
                    ({
                        toMulEquiv :=
                          (Equiv.symm MulEquiv.withZero : (a : WithZero G ≃* WithZero H) → G ≃* H)
                            (↑e : WithZero G ≃* WithZero H),
                        map_le_map_iff' := ⋯ } :
                      G ≃*o H))
                  x_1) :
              OrderMonoidIso.{u_6, u_7} (WithZero G) (WithZero H)) :
            (a : WithZero G) → WithZero H)
          (↑a : WithZero G) :
        WithZero H)
      ((x_1 : (a : WithZero G) → WithZero H) (↑a : WithZero G) : WithZero H)
⊢ Eq.{u_7 + 1} (α := WithZero H)
    ((((fun (e : G ≃*o H) ↦
                ({ toMulEquiv := (MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv,
                    map_le_map_iff' := ⋯ } :
                  OrderMonoidIso.{u_6, u_7} (WithZero G) (WithZero H)))
              ((fun (e : OrderMonoidIso.{u_6, u_7} (WithZero G) (WithZero H)) ↦
                  ({
                      toMulEquiv :=
                        (Equiv.symm MulEquiv.withZero : (a : WithZero G ≃* WithZero H) → G ≃* H)
                          (↑e : WithZero G ≃* WithZero H),
                      map_le_map_iff' := ⋯ } :
                    G ≃*o H))
                x_1) :
            OrderMonoidIso.{u_6, u_7} (WithZero G) (WithZero H)) :
          (a : WithZero G) → WithZero H)
        x :
      WithZero H)
    ((x_1 : (a : WithZero G) → WithZero H) x : WithZero H)

Tactic:
cases x
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst : Group G
inst_1 : PartialOrder G
inst_2 : Group H
inst_3 : PartialOrder H
x : OrderMonoidIso.{u_6, u_7} (WithZero G) (WithZero H)
⊢ Eq.{u_7 + 1} (α := WithZero H)
    ((((fun (e : G ≃*o H) ↦
              ({ toMulEquiv := (MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv,
                  map_le_map_iff' := ⋯ } :
                OrderMonoidIso.{u_6, u_7} (WithZero G) (WithZero H)))
            ((fun (e : OrderMonoidIso.{u_6, u_7} (WithZero G) (WithZero H)) ↦
                ({
                    toMulEquiv :=
                      (Equiv.symm MulEquiv.withZero : (a : WithZero G ≃* WithZero H) → G ≃* H)
                        (↑e : WithZero G ≃* WithZero H),
                    map_le_map_iff' := ⋯ } :
                  G ≃*o H))
              x) :
          OrderMonoidIso.{u_6, u_7} (WithZero G) (WithZero H)) :
        (a : WithZero G) → WithZero H)
      0)
    ((x : (a : WithZero G) → WithZero H) 0)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst : Group G
inst_1 : PartialOrder G
inst_2 : Group H
inst_3 : PartialOrder H
x : OrderMonoidIso.{u_6, u_7} (WithZero G) (WithZero H)
a : G
⊢ Eq.{u_7 + 1} (α := WithZero H)
    ((((fun (e : G ≃*o H) ↦
                ({ toMulEquiv := (MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv,
                    map_le_map_iff' := ⋯ } :
                  OrderMonoidIso.{u_6, u_7} (WithZero G) (WithZero H)))
              ((fun (e : OrderMonoidIso.{u_6, u_7} (WithZero G) (WithZero H)) ↦
                  ({
                      toMulEquiv :=
                        (Equiv.symm MulEquiv.withZero : (a : WithZero G ≃* WithZero H) → G ≃* H)
                          (↑e : WithZero G ≃* WithZero H),
                      map_le_map_iff' := ⋯ } :
                    G ≃*o H))
                x) :
            OrderMonoidIso.{u_6, u_7} (WithZero G) (WithZero H)) :
          (a : WithZero G) → WithZero H)
        (↑a : WithZero G) :
      WithZero H)
    ((x : (a : WithZero G) → WithZero H) (↑a : WithZero G) : WithZero H)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
F : Type u_1
α_1 : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst : LinearOrderedCommGroupWithZero α
inst_1 : DecidablePred fun (a : α) ↦ a = 0
a b : WithZero αˣ
zero :
  Equiv.toFun (α := WithZero αˣ) (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) 0 ≤
      Equiv.toFun (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) b ↔
    0 ≤ b
coe :
  ∀ (a : αˣ),
    Equiv.toFun (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) (↑a : WithZero αˣ) ≤
        Equiv.toFun (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) b ↔
      (↑a : WithZero αˣ) ≤ b
⊢ Equiv.toFun (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) a ≤
      Equiv.toFun (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) b ↔
    a ≤ b

Tactic:
cases a
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
F : Type u_1
α_1 : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst : LinearOrderedCommGroupWithZero α
inst_1 : DecidablePred fun (a : α) ↦ a = 0
b : WithZero αˣ
zero :
  LE.le.{u_6} (α := α) (Equiv.toFun (α := WithZero αˣ) (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) 0)
      (Equiv.toFun (α := WithZero αˣ) (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) 0) ↔
    LE.le.{u_6} (α := WithZero αˣ) 0 0
zero₁ :
  ∀ (a : αˣ),
    Equiv.toFun (α := WithZero αˣ) (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) 0 ≤
        Equiv.toFun (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) (↑a : WithZero αˣ) ↔
      0 ≤ (↑a : WithZero αˣ)
⊢ Equiv.toFun (α := WithZero αˣ) (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) 0 ≤
      Equiv.toFun (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) b ↔
    0 ≤ b

Tactic:
cases b
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
F : Type u_1
α_1 : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst : LinearOrderedCommGroupWithZero α
inst_1 : DecidablePred fun (a : α) ↦ a = 0
b : WithZero αˣ
a : αˣ
coe :
  Equiv.toFun (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) (↑a : WithZero αˣ) ≤
      Equiv.toFun (α := WithZero αˣ) (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) 0 ↔
    (↑a : WithZero αˣ) ≤ 0
coe₁ :
  ∀ (a_1 : αˣ),
    Equiv.toFun (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) (↑a : WithZero αˣ) ≤
        Equiv.toFun (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) (↑a_1 : WithZero αˣ) ↔
      (↑a : WithZero αˣ) ≤ (↑a_1 : WithZero αˣ)
⊢ Equiv.toFun (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) (↑a : WithZero αˣ) ≤
      Equiv.toFun (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) b ↔
    (↑a : WithZero αˣ) ≤ b

Tactic:
cases b
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
F : Type u_1
α_1 : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst : LinearOrderedCommGroupWithZero α
inst_1 : DecidablePred fun (a : α) ↦ a = 0
⊢ LE.le.{u_6} (α := α) (Equiv.toFun (α := WithZero αˣ) (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) 0)
      (Equiv.toFun (α := WithZero αˣ) (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) 0) ↔
    LE.le.{u_6} (α := WithZero αˣ) 0 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
F : Type u_1
α_1 : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst : LinearOrderedCommGroupWithZero α
inst_1 : DecidablePred fun (a : α) ↦ a = 0
a : αˣ
⊢ Equiv.toFun (α := WithZero αˣ) (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) 0 ≤
      Equiv.toFun (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) (↑a : WithZero αˣ) ↔
    0 ≤ (↑a : WithZero αˣ)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
F : Type u_1
α_1 : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst : LinearOrderedCommGroupWithZero α
inst_1 : DecidablePred fun (a : α) ↦ a = 0
a : αˣ
⊢ Equiv.toFun (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) (↑a : WithZero αˣ) ≤
      Equiv.toFun (α := WithZero αˣ) (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) 0 ↔
    (↑a : WithZero αˣ) ≤ 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Hom.MonoidWithZero
Goal:
F : Type u_1
α_1 : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst : LinearOrderedCommGroupWithZero α
inst_1 : DecidablePred fun (a : α) ↦ a = 0
a a_1 : αˣ
⊢ Equiv.toFun (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) (↑a : WithZero αˣ) ≤
      Equiv.toFun (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) (↑a_1 : WithZero αˣ) ↔
    (↑a : WithZero αˣ) ≤ (↑a_1 : WithZero αˣ)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : NonAssocSemiring α
inst_1 : Preorder α
inst_2 : NonAssocSemiring β
inst_3 : Preorder β
inst_4 : NonAssocSemiring γ
inst_5 : Preorder γ
inst_6 : NonAssocSemiring δ
inst_7 : Preorder δ
f g : α →+*o β
h :
  Eq (α := (a : α) → β) ((fun (f : α →+*o β) ↦ (↑(↑f.toRingHom : α →* β) : OneHom α β).toFun) f)
    ((fun (f : α →+*o β) ↦ (↑(↑f.toRingHom : α →* β) : OneHom α β).toFun) g)
mk :
  ∀ (toRingHom : α →+* β) (monotone' : Monotone (↑(↑toRingHom : α →* β) : OneHom α β).toFun)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : α →+*o β) ↦ (↑(↑f.toRingHom : α →* β) : OneHom α β).toFun)
          { toRingHom := toRingHom, monotone' := monotone' })
        ((fun (f : α →+*o β) ↦ (↑(↑f.toRingHom : α →* β) : OneHom α β).toFun) g)),
    { toRingHom := toRingHom, monotone' := monotone' : α →+*o β } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : NonAssocSemiring α
inst_1 : Preorder α
inst_2 : NonAssocSemiring β
inst_3 : Preorder β
inst_4 : NonAssocSemiring γ
inst_5 : Preorder γ
inst_6 : NonAssocSemiring δ
inst_7 : Preorder δ
g : α →+*o β
toRingHom : α →+* β
monotone' : Monotone (↑(↑toRingHom : α →* β) : OneHom α β).toFun
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →+*o β) ↦ (↑(↑f.toRingHom : α →* β) : OneHom α β).toFun)
      { toRingHom := toRingHom, monotone' := monotone' })
    ((fun (f : α →+*o β) ↦ (↑(↑f.toRingHom : α →* β) : OneHom α β).toFun) g)
mk :
  ∀ (toRingHom_1 : α →+* β) (monotone'_1 : Monotone (↑(↑toRingHom_1 : α →* β) : OneHom α β).toFun)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : α →+*o β) ↦ (↑(↑f.toRingHom : α →* β) : OneHom α β).toFun)
          { toRingHom := toRingHom, monotone' := monotone' })
        ((fun (f : α →+*o β) ↦ (↑(↑f.toRingHom : α →* β) : OneHom α β).toFun)
          { toRingHom := toRingHom_1, monotone' := monotone'_1 })),
    { toRingHom := toRingHom, monotone' := monotone' : α →+*o β } =
      { toRingHom := toRingHom_1, monotone' := monotone'_1 }
⊢ { toRingHom := toRingHom, monotone' := monotone' : α →+*o β } = g

Tactic:
cases g
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : NonAssocSemiring α
inst_1 : Preorder α
inst_2 : NonAssocSemiring β
inst_3 : Preorder β
inst_4 : NonAssocSemiring γ
inst_5 : Preorder γ
inst_6 : NonAssocSemiring δ
inst_7 : Preorder δ
toRingHom : α →+* β
monotone' : Monotone (↑(↑toRingHom : α →* β) : OneHom α β).toFun
toRingHom_1 : α →+* β
monotone'_1 : Monotone (↑(↑toRingHom_1 : α →* β) : OneHom α β).toFun
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →+*o β) ↦ (↑(↑f.toRingHom : α →* β) : OneHom α β).toFun)
      { toRingHom := toRingHom, monotone' := monotone' })
    ((fun (f : α →+*o β) ↦ (↑(↑f.toRingHom : α →* β) : OneHom α β).toFun)
      { toRingHom := toRingHom_1, monotone' := monotone'_1 })
mk : toRingHom = toRingHom_1
⊢ { toRingHom := toRingHom, monotone' := monotone' : α →+*o β } = { toRingHom := toRingHom_1, monotone' := monotone'_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : NonAssocSemiring α
inst_1 : Preorder α
inst_2 : NonAssocSemiring β
inst_3 : Preorder β
inst_4 : NonAssocSemiring γ
inst_5 : Preorder γ
inst_6 : NonAssocSemiring δ
inst_7 : Preorder δ
toRingHom : α →+* β
monotone' : Monotone (↑(↑toRingHom : α →* β) : OneHom α β).toFun
toRingHom_1 : α →+* β
monotone'_1 : Monotone (↑(↑toRingHom_1 : α →* β) : OneHom α β).toFun
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →+*o β) ↦ (↑(↑f.toRingHom : α →* β) : OneHom α β).toFun)
      { toRingHom := toRingHom, monotone' := monotone' })
    ((fun (f : α →+*o β) ↦ (↑(↑f.toRingHom : α →* β) : OneHom α β).toFun)
      { toRingHom := toRingHom_1, monotone' := monotone'_1 })
⊢ toRingHom = toRingHom_1

Tactic:
DFunLike.coe_injective' h

Premises used: DFunLike.coe_injective'
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : NonAssocSemiring α
inst_1 : Preorder α
inst_2 : NonAssocSemiring β
inst_3 : Preorder β
inst_4 : NonAssocSemiring γ
inst_5 : Preorder γ
inst_6 : NonAssocSemiring δ
inst_7 : Preorder δ
toRingHom : α →+* β
monotone' : Monotone (↑(↑toRingHom : α →* β) : OneHom α β).toFun
toRingHom_1 : α →+* β
monotone'_1 : Monotone (↑(↑toRingHom_1 : α →* β) : OneHom α β).toFun
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →+*o β) ↦ (↑(↑f.toRingHom : α →* β) : OneHom α β).toFun)
      { toRingHom := toRingHom, monotone' := monotone' })
    ((fun (f : α →+*o β) ↦ (↑(↑f.toRingHom : α →* β) : OneHom α β).toFun)
      { toRingHom := toRingHom_1, monotone' := monotone'_1 })
⊢ toRingHom = toRingHom_1

Tactic:
exact DFunLike.coe_injective' h

Premises used: DFunLike.coe_injective'
-- 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.toRingHom : α →* β) : OneHom α β).toFun = (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: 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 : ∀ (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 : NonAssocSemiring α
inst_1 : Preorder α
inst_2 : NonAssocSemiring β
inst_3 : Preorder β
f : α →+*o β
⊢ f.toRingHom = (↑f : α →+* β)

Tactic:
RingHom.ext fun _ => rfl

Premises used: RingHom.ext, 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 β
⊢ f.toOrderAddMonoidHom = (↑f : α →+o β)

Tactic:
rfl

Premises used: OrderMonoidHomClass.toOrderAddMonoidHom, AddMonoidHomClass.toAddMonoidHom, OrderRingHom.toOrderAddMonoidHom, 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 β
⊢ f.toOrderMonoidWithZeroHom = (↑f : α →*₀o β)

Tactic:
rfl

Premises used: OrderRingHom.toOrderMonoidWithZeroHom, MonoidWithZeroHomClass.toMonoidWithZeroHom, OrderMonoidWithZeroHomClass.toOrderMonoidWithZeroHom, 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 : α →+* β) : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: 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
β : 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
β : Type u_3
inst : NonAssocSemiring α
inst_1 : Preorder α
inst_2 : NonAssocSemiring β
inst_3 : Preorder β
f : α →+*o β
a : α
⊢ Eq.{u_3 + 1} (α := β) (((↑f : α →+* β) : (a : α) → β) a : β) ((f : (a : α) → β) a : β)

Tactic:
rfl

Premises used: 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 β
a : α
⊢ Eq.{u_3 + 1} (α := β) (((↑f : α →+o β) : (a : α) → β) a : β) ((f : (a : α) → β) a : β)

Tactic:
rfl

Premises used: 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 β
a : α
⊢ Eq.{u_3 + 1} (α := β) (((↑f : α →*₀o β) : (a : α) → β) a : β) ((f : (a : α) → β) a : β)

Tactic:
rfl

Premises used: 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 β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ (⇑(f.copy f' h) : (a : α) → β) = f'

Tactic:
rfl

Premises used: 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 β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ f.copy f' h = f

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
α : Type u_2
inst : NonAssocSemiring α
inst_1 : Preorder α
⊢ Eq (α := (a : α) → α) (⇑(OrderRingHom.id α) : (a : α) → α) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
α : Type u_2
inst : NonAssocSemiring α
inst_1 : Preorder α
a : α
⊢ (OrderRingHom.id α : (a : α) → α) a = a

Tactic:
rfl

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

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, rfl
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
α : Type u_2
inst : NonAssocSemiring α
inst_1 : Preorder α
⊢ Eq (α := α →+o α) (↑(OrderRingHom.id α) : α →+o α) (OrderAddMonoidHom.id α)

Tactic:
rfl

Premises used: AddMonoidHomClass.toAddMonoidHom, rfl, OrderAddMonoidHom.id
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
α : Type u_2
inst : NonAssocSemiring α
inst_1 : Preorder α
⊢ Eq (α := α →*₀o α) (↑(OrderRingHom.id α) : α →*₀o α) (OrderMonoidWithZeroHom.id α)

Tactic:
rfl

Premises used: MonoidWithZeroHomClass.toMonoidWithZeroHom, MonoidWithZeroHom.id, OrderMonoidWithZeroHom.id, OrderMonoidWithZeroHomClass.toOrderMonoidWithZeroHom, rfl
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : NonAssocSemiring α
inst_1 : Preorder α
inst_2 : NonAssocSemiring β
inst_3 : Preorder β
inst_4 : NonAssocSemiring γ
inst_5 : Preorder γ
f : β →+*o γ
g : α →+*o β
⊢ Eq (α := (a : α) → γ) (⇑(f.comp g) : (a : α) → γ)
    (comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : NonAssocSemiring α
inst_1 : Preorder α
inst_2 : NonAssocSemiring β
inst_3 : Preorder β
inst_4 : NonAssocSemiring γ
inst_5 : Preorder γ
f : β →+*o γ
g : α →+*o β
a : α
⊢ Eq.{u_4 + 1} (α := γ) ((f.comp g : (a : α) → γ) a : γ) ((f : (a : β) → γ) ((g : (a : α) → β) a : β) : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : NonAssocSemiring α
inst_1 : Preorder α
inst_2 : NonAssocSemiring β
inst_3 : Preorder β
inst_4 : NonAssocSemiring γ
inst_5 : Preorder γ
inst_6 : NonAssocSemiring δ
inst_7 : Preorder δ
f : γ →+*o δ
g : β →+*o γ
h : α →+*o β
⊢ (f.comp g).comp h = f.comp (g.comp h)

Tactic:
rfl

Premises used: OrderRingHom.comp, 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 β
⊢ f.comp (OrderRingHom.id α) = f

Tactic:
rfl

Premises used: OrderRingHom.comp, 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 β
⊢ OrderRingHom.comp (OrderRingHom.id β) f = f

Tactic:
rfl

Premises used: OrderRingHom.comp, rfl
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : NonAssocSemiring α
inst_1 : Preorder α
inst_2 : NonAssocSemiring β
inst_3 : Preorder β
inst_4 : NonAssocSemiring γ
inst_5 : Preorder γ
f₁ f₂ : β →+*o γ
g : α →+*o β
hg : Surjective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑g : (a : α) → β)
h : f₁ = f₂
rw rw₁ : f₂.comp g = f₂.comp g
⊢ f₁.comp g = f₂.comp g

Tactic:
rw [h]
-- Module: Mathlib.Algebra.Order.Hom.Ring
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : NonAssocSemiring α
inst_1 : Preorder α
inst_2 : NonAssocSemiring β
inst_3 : Preorder β
inst_4 : NonAssocSemiring γ
inst_5 : Preorder γ
f : β →+*o γ
g₁ g₂ : α →+*o β
hf : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑f : (a : β) → γ)
h : f.comp g₁ = f.comp g₂
a : α
rw : Eq.{u_4 + 1} (α := γ) ((f.comp g₁ : (a : α) → γ) a : γ) ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
rw₁ : Eq.{u_4 + 1} (α := γ) ((f.comp g₂ : (a : α) → γ) a : γ) ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
rw₂ rw₃ :
  Eq.{u_4 + 1} (α := γ) ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
    ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((f : (a : β) → γ) ((g₁ : (a : α) → β) a : β) : γ)
    ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)

Tactic:
rw [← comp_apply, h, comp_apply]

Premises used: OrderRingHom.comp_apply