awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.MonoidWithZero (goal)
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 : G ≃*o 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))
      ((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)))
        x) =
    x
have h : ∀ (a : G),
  Eq.{u_7 + 1} (α := 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' := sorry } :
                G ≃*o H))
            ((fun (e : G ≃*o H) ↦
                ({ toMulEquiv := (MulEquiv.withZero : (a : G ≃* H) → WithZero G ≃* WithZero H) e.toMulEquiv,
                    map_le_map_iff' := sorry } :
                  OrderMonoidIso.{u_6, u_7} (WithZero G) (WithZero H)))
              x) :
          (a : G) → H)
        a :
      H)
    ((x : (a : G) → H) a : H)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.MonoidWithZero (goal)
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)
⊢ (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) =
    x
have h : ∀ (x_1 : WithZero 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' := sorry } :
                  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' := sorry } :
                    G ≃*o H))
                x) :
            OrderMonoidIso.{u_6, u_7} (WithZero G) (WithZero H)) :
          (a : WithZero G) → WithZero H)
        x_1 :
      WithZero H)
    ((x : (a : WithZero G) → WithZero H) x_1 : WithZero H)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.MonoidWithZero (goal)
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
⊢ 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)
have 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' := sorry } :
              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' := sorry } :
                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)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.MonoidWithZero (goal)
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)
⊢ 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)
have 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' := sorry } :
                  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' := sorry } :
                    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)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.MonoidWithZero (goal)
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 αˣ
⊢ Equiv.toFun (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) a ≤
      Equiv.toFun (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) b ↔
    a ≤ b
have zero : Equiv.toFun (α := WithZero αˣ) (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) 0 ≤
    Equiv.toFun (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) b ↔
  0 ≤ b
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.MonoidWithZero (goal)
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
⊢ Equiv.toFun (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) a ≤
      Equiv.toFun (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) b ↔
    a ≤ b
have coe : ∀ (a : αˣ),
  Equiv.toFun (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) (↑a : WithZero αˣ) ≤
      Equiv.toFun (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) b ↔
    (↑a : WithZero αˣ) ≤ b
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.MonoidWithZero (goal)
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 αˣ
⊢ Equiv.toFun (α := WithZero αˣ) (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) 0 ≤
      Equiv.toFun (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) b ↔
    0 ≤ b
have 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
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.MonoidWithZero (goal)
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
⊢ Equiv.toFun (α := WithZero αˣ) (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) 0 ≤
      Equiv.toFun (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) b ↔
    0 ≤ b
have zero₁ : ∀ (a : αˣ),
  Equiv.toFun (α := WithZero αˣ) (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) 0 ≤
      Equiv.toFun (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) (↑a : WithZero αˣ) ↔
    0 ≤ (↑a : WithZero αˣ)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.MonoidWithZero (goal)
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 : αˣ
⊢ Equiv.toFun (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) (↑a : WithZero αˣ) ≤
      Equiv.toFun (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) b ↔
    (↑a : WithZero αˣ) ≤ b
have coe : Equiv.toFun (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) (↑a : WithZero αˣ) ≤
    Equiv.toFun (α := WithZero αˣ) (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) 0 ↔
  (↑a : WithZero αˣ) ≤ 0
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.MonoidWithZero (goal)
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
⊢ Equiv.toFun (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) (↑a : WithZero αˣ) ≤
      Equiv.toFun (MulEquiv.toEquiv WithZero.withZeroUnitsEquiv) b ↔
    (↑a : WithZero αˣ) ≤ b
have 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 αˣ)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Ring (goal)
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)
⊢ f = g
have 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
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Ring (goal)
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)
⊢ { toRingHom := toRingHom, monotone' := monotone' : α →+*o β } = g
have 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 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Ring (goal)
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, monotone' := monotone' : α →+*o β } = { toRingHom := toRingHom_1, monotone' := monotone'_1 }
have mk : toRingHom = toRingHom_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Ring (goal)
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₂
⊢ f₁.comp g = f₂.comp g
have rw : f₂.comp g = f₂.comp g
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Ring (goal)
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 : α
⊢ Eq.{u_4 + 1} (α := γ) ((f : (a : β) → γ) ((g₁ : (a : α) → β) a : β) : γ)
    ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
have rw : Eq.{u_4 + 1} (α := γ) ((f.comp g₁ : (a : α) → γ) a : γ) ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Ring (goal)
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 : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((f : (a : β) → γ) ((g₁ : (a : α) → β) a : β) : γ)
    ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
have rw₁ : Eq.{u_4 + 1} (α := γ) ((f.comp g₂ : (a : α) → γ) a : γ) ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Ring (goal)
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 : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((f : (a : β) → γ) ((g₁ : (a : α) → β) a : β) : γ)
    ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
have rw₂ : Eq.{u_4 + 1} (α := γ) ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
  ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Ring (goal)
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
⊢ f = g
have 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
Tactic: obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f
Cleared hypotheses: f, h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Ring (goal)
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 : β
⊢ e.symm.toFun a ≤ e.symm.toFun b ↔ a ≤ b
have erw : LE.le.{u_3} (α := β) ((e : (a : α) → β) (e.symm.toFun a) : β) ((e : (a : α) → β) (e.symm.toFun b) : β) ↔ a ≤ b
Tactic: erw [← map_le_map_iff e, e.1.apply_symm_apply, e.1.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Ring (goal)
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
⊢ e.symm.toFun a ≤ e.symm.toFun b ↔ a ≤ b
have erw₁ : a ≤ (e : (a : α) → β) (e.symm.toFun b) ↔ a ≤ b
Tactic: erw [← map_le_map_iff e, e.1.apply_symm_apply, e.1.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Ring (goal)
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
⊢ e.symm.toFun a ≤ e.symm.toFun b ↔ a ≤ b
have erw₂ : a ≤ b ↔ a ≤ b
Tactic: erw [← map_le_map_iff e, e.1.apply_symm_apply, e.1.apply_symm_apply]