awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Lex (goal)
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : LinearOrderedCommGroupWithZero M₀
inst_1 : GroupWithZero N₀
inst_2 : Preorder N₀
inst_3 : DecidablePred fun (x : M₀) ↦ x = 0
y : M₀
x : M₀ˣ
inr :
  (↑x : M₀) ≤ 0 →
    LE.le (α := WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) (↑x : M₀) :
        WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) 0 :
        WithZero M₀ˣ)
⊢ (↑x : M₀) ≤ y →
    LE.le (α := WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) (↑x : M₀) :
        WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) y :
        WithZero M₀ˣ)
have inr₁ : ∀ (y : M₀ˣ),
  (↑x : M₀) ≤ (↑y : M₀) →
    LE.le (α := WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) (↑x : M₀) :
        WithZero M₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : M₀ →*₀ WithZero M₀ˣ) : (a : M₀) → WithZero M₀ˣ) (↑y : M₀) :
        WithZero M₀ˣ)
Tactic: obtain rfl | ⟨y, rfl⟩ := GroupWithZero.eq_zero_or_unit y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Lex (goal)
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : GroupWithZero M₀
inst_1 : Preorder M₀
inst_2 : LinearOrderedCommGroupWithZero N₀
inst_3 : DecidablePred fun (x : N₀) ↦ x = 0
⊢ Monotone (α := N₀) (β := WithZero (Prod.{u_1, u_2} M₀ˣ N₀ˣ)) (⇑(inr M₀ N₀) : (a : N₀) → WithZero (M₀ˣ × N₀ˣ))
have refine : Monotone (α := N₀) (β := WithZero N₀ˣ)
  (⇑(↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ)
Tactic: refine (WithZero.map'_mono MonoidHom.inr_mono).comp ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Lex (goal)
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : GroupWithZero M₀
inst_1 : Preorder M₀
inst_2 : LinearOrderedCommGroupWithZero N₀
inst_3 : DecidablePred fun (x : N₀) ↦ x = 0
x y : N₀
⊢ x ≤ y →
    LE.le (α := WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) x :
        WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) y :
        WithZero N₀ˣ)
have inl : 0 ≤ y →
  LE.le (α := WithZero N₀ˣ)
    (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) 0 : WithZero N₀ˣ)
    (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) y : WithZero N₀ˣ)
Tactic: obtain rfl | ⟨x, rfl⟩ := GroupWithZero.eq_zero_or_unit x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Lex (goal)
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : GroupWithZero M₀
inst_1 : Preorder M₀
inst_2 : LinearOrderedCommGroupWithZero N₀
inst_3 : DecidablePred fun (x : N₀) ↦ x = 0
x y : N₀
inl :
  0 ≤ y →
    LE.le (α := WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) 0 :
        WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) y :
        WithZero N₀ˣ)
⊢ x ≤ y →
    LE.le (α := WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) x :
        WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) y :
        WithZero N₀ˣ)
have inr : ∀ (x : N₀ˣ),
  (↑x : N₀) ≤ y →
    LE.le (α := WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) (↑x : N₀) :
        WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) y :
        WithZero N₀ˣ)
Tactic: obtain rfl | ⟨x, rfl⟩ := GroupWithZero.eq_zero_or_unit x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Lex (goal)
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : GroupWithZero M₀
inst_1 : Preorder M₀
inst_2 : LinearOrderedCommGroupWithZero N₀
inst_3 : DecidablePred fun (x : N₀) ↦ x = 0
y : N₀
⊢ 0 ≤ y →
    LE.le (α := WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) 0 :
        WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) y :
        WithZero N₀ˣ)
have inl : LE.le.{u_2} (α := N₀) 0 0 →
  LE.le (α := WithZero N₀ˣ)
    (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) 0 : WithZero N₀ˣ)
    (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) 0 : WithZero N₀ˣ)
Tactic: obtain rfl | ⟨y, rfl⟩ := GroupWithZero.eq_zero_or_unit y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Lex (goal)
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : GroupWithZero M₀
inst_1 : Preorder M₀
inst_2 : LinearOrderedCommGroupWithZero N₀
inst_3 : DecidablePred fun (x : N₀) ↦ x = 0
y : N₀
inl :
  LE.le.{u_2} (α := N₀) 0 0 →
    LE.le (α := WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) 0 :
        WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) 0 :
        WithZero N₀ˣ)
⊢ 0 ≤ y →
    LE.le (α := WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) 0 :
        WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) y :
        WithZero N₀ˣ)
have inl₁ : ∀ (y : N₀ˣ),
  0 ≤ (↑y : N₀) →
    LE.le (α := WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) 0 :
        WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) (↑y : N₀) :
        WithZero N₀ˣ)
Tactic: obtain rfl | ⟨y, rfl⟩ := GroupWithZero.eq_zero_or_unit y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Lex (goal)
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : GroupWithZero M₀
inst_1 : Preorder M₀
inst_2 : LinearOrderedCommGroupWithZero N₀
inst_3 : DecidablePred fun (x : N₀) ↦ x = 0
y : N₀
x : N₀ˣ
⊢ (↑x : N₀) ≤ y →
    LE.le (α := WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) (↑x : N₀) :
        WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) y :
        WithZero N₀ˣ)
have inr : (↑x : N₀) ≤ 0 →
  LE.le (α := WithZero N₀ˣ)
    (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) (↑x : N₀) :
      WithZero N₀ˣ)
    (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) 0 : WithZero N₀ˣ)
Tactic: obtain rfl | ⟨y, rfl⟩ := GroupWithZero.eq_zero_or_unit y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Lex (goal)
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : GroupWithZero M₀
inst_1 : Preorder M₀
inst_2 : LinearOrderedCommGroupWithZero N₀
inst_3 : DecidablePred fun (x : N₀) ↦ x = 0
y : N₀
x : N₀ˣ
inr :
  (↑x : N₀) ≤ 0 →
    LE.le (α := WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) (↑x : N₀) :
        WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) 0 :
        WithZero N₀ˣ)
⊢ (↑x : N₀) ≤ y →
    LE.le (α := WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) (↑x : N₀) :
        WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) y :
        WithZero N₀ˣ)
have inr₁ : ∀ (y : N₀ˣ),
  (↑x : N₀) ≤ (↑y : N₀) →
    LE.le (α := WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) (↑x : N₀) :
        WithZero N₀ˣ)
      (((↑(MulEquiv.symm WithZero.withZeroUnitsEquiv) : N₀ →*₀ WithZero N₀ˣ) : (a : N₀) → WithZero N₀ˣ) (↑y : N₀) :
        WithZero N₀ˣ)
Tactic: obtain rfl | ⟨y, rfl⟩ := GroupWithZero.eq_zero_or_unit y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Lex (goal)
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : LinearOrderedCommGroupWithZero M₀
inst_1 : GroupWithZero N₀
inst_2 : Preorder N₀
⊢ Monotone (α := WithZero (Prod.{u_1, u_2} M₀ˣ N₀ˣ)) (β := M₀) (⇑(fst M₀ N₀) : (a : WithZero (M₀ˣ × N₀ˣ)) → M₀)
have refine : (∀ ⦃b : WithZero (Prod.{u_1, u_2} M₀ˣ N₀ˣ)⦄,
    0 ≤ b →
      LE.le.{u_1} (α := M₀) ((fst M₀ N₀ : (a : WithZero (M₀ˣ × N₀ˣ)) → M₀) 0 : M₀)
        ((fst M₀ N₀ : (a : WithZero (M₀ˣ × N₀ˣ)) → M₀) b : M₀)) ∧
  ∀ (a : Prod.{u_1, u_2} M₀ˣ N₀ˣ) ⦃b : WithZero (Prod.{u_1, u_2} M₀ˣ N₀ˣ)⦄,
    (↑a : WithZero (M₀ˣ × N₀ˣ)) ≤ b →
      LE.le.{u_1} (α := M₀) ((fst M₀ N₀ : (a : WithZero (M₀ˣ × N₀ˣ)) → M₀) (↑a : WithZero (M₀ˣ × N₀ˣ)) : M₀)
        ((fst M₀ N₀ : (a : WithZero (M₀ˣ × N₀ˣ)) → M₀) b : M₀)
Tactic: refine WithZero.forall.mpr ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Lex (goal)
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : GroupWithZero M₀
inst_1 : Preorder M₀
inst_2 : LinearOrderedCommGroupWithZero N₀
⊢ Monotone (α := WithZero (Prod.{u_1, u_2} M₀ˣ N₀ˣ)) (β := N₀) (⇑(snd M₀ N₀) : (a : WithZero (M₀ˣ × N₀ˣ)) → N₀)
have refine : (∀ ⦃b : WithZero (Prod.{u_1, u_2} M₀ˣ N₀ˣ)⦄,
    0 ≤ b →
      LE.le.{u_2} (α := N₀) ((snd M₀ N₀ : (a : WithZero (M₀ˣ × N₀ˣ)) → N₀) 0 : N₀)
        ((snd M₀ N₀ : (a : WithZero (M₀ˣ × N₀ˣ)) → N₀) b : N₀)) ∧
  ∀ (a : Prod.{u_1, u_2} M₀ˣ N₀ˣ) ⦃b : WithZero (Prod.{u_1, u_2} M₀ˣ N₀ˣ)⦄,
    (↑a : WithZero (M₀ˣ × N₀ˣ)) ≤ b →
      LE.le.{u_2} (α := N₀) ((snd M₀ N₀ : (a : WithZero (M₀ˣ × N₀ˣ)) → N₀) (↑a : WithZero (M₀ˣ × N₀ˣ)) : N₀)
        ((snd M₀ N₀ : (a : WithZero (M₀ˣ × N₀ˣ)) → N₀) b : N₀)
Tactic: refine WithZero.forall.mpr ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
inst_1 : LinearOrderedCommGroupWithZero β
x y : WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))
⊢ x ≤ y →
    ZeroHom.toFun
        (↑(comp (MonoidWithZeroHom.fst α β)
              (WithZero.map' (MulEquiv.toMonoidHom (MulEquiv.symm (toLexMulEquiv (Prod.{u_1, u_2} αˣ βˣ)))))) :
          ZeroHom (WithZero (Lex (αˣ × βˣ))) α)
        x ≤
      ZeroHom.toFun
        (↑(comp (MonoidWithZeroHom.fst α β)
              (WithZero.map' (MulEquiv.toMonoidHom (MulEquiv.symm (toLexMulEquiv (Prod.{u_1, u_2} αˣ βˣ)))))) :
          ZeroHom (WithZero (Lex (αˣ × βˣ))) α)
        y
have zero : 0 ≤ y →
  ZeroHom.toFun (M := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
      (↑(comp (MonoidWithZeroHom.fst α β)
            (WithZero.map' (MulEquiv.toMonoidHom (MulEquiv.symm (toLexMulEquiv (Prod.{u_1, u_2} αˣ βˣ)))))) :
        ZeroHom (WithZero (Lex (αˣ × βˣ))) α)
      0 ≤
    ZeroHom.toFun
      (↑(comp (MonoidWithZeroHom.fst α β)
            (WithZero.map' (MulEquiv.toMonoidHom (MulEquiv.symm (toLexMulEquiv (Prod.{u_1, u_2} αˣ βˣ)))))) :
        ZeroHom (WithZero (Lex (αˣ × βˣ))) α)
      y
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
inst_1 : LinearOrderedCommGroupWithZero β
x y : WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))
zero :
  0 ≤ y →
    ZeroHom.toFun (M := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
        (↑(comp (MonoidWithZeroHom.fst α β)
              (WithZero.map' (MulEquiv.toMonoidHom (MulEquiv.symm (toLexMulEquiv (Prod.{u_1, u_2} αˣ βˣ)))))) :
          ZeroHom (WithZero (Lex (αˣ × βˣ))) α)
        0 ≤
      ZeroHom.toFun
        (↑(comp (MonoidWithZeroHom.fst α β)
              (WithZero.map' (MulEquiv.toMonoidHom (MulEquiv.symm (toLexMulEquiv (Prod.{u_1, u_2} αˣ βˣ)))))) :
          ZeroHom (WithZero (Lex (αˣ × βˣ))) α)
        y
⊢ x ≤ y →
    ZeroHom.toFun
        (↑(comp (MonoidWithZeroHom.fst α β)
              (WithZero.map' (MulEquiv.toMonoidHom (MulEquiv.symm (toLexMulEquiv (Prod.{u_1, u_2} αˣ βˣ)))))) :
          ZeroHom (WithZero (Lex (αˣ × βˣ))) α)
        x ≤
      ZeroHom.toFun
        (↑(comp (MonoidWithZeroHom.fst α β)
              (WithZero.map' (MulEquiv.toMonoidHom (MulEquiv.symm (toLexMulEquiv (Prod.{u_1, u_2} αˣ βˣ)))))) :
          ZeroHom (WithZero (Lex (αˣ × βˣ))) α)
        y
have coe : ∀ (a : Lex (Prod.{u_1, u_2} αˣ βˣ)),
  (↑a : WithZero (Lex (αˣ × βˣ))) ≤ y →
    ZeroHom.toFun
        (↑(comp (MonoidWithZeroHom.fst α β)
              (WithZero.map' (MulEquiv.toMonoidHom (MulEquiv.symm (toLexMulEquiv (Prod.{u_1, u_2} αˣ βˣ)))))) :
          ZeroHom (WithZero (Lex (αˣ × βˣ))) α)
        (↑a : WithZero (Lex (αˣ × βˣ))) ≤
      ZeroHom.toFun
        (↑(comp (MonoidWithZeroHom.fst α β)
              (WithZero.map' (MulEquiv.toMonoidHom (MulEquiv.symm (toLexMulEquiv (Prod.{u_1, u_2} αˣ βˣ)))))) :
          ZeroHom (WithZero (Lex (αˣ × βˣ))) α)
        y
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
inst_1 : LinearOrderedCommGroupWithZero β
y : WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))
⊢ 0 ≤ y →
    ZeroHom.toFun (M := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
        (↑(comp (MonoidWithZeroHom.fst α β)
              (WithZero.map' (MulEquiv.toMonoidHom (MulEquiv.symm (toLexMulEquiv (Prod.{u_1, u_2} αˣ βˣ)))))) :
          ZeroHom (WithZero (Lex (αˣ × βˣ))) α)
        0 ≤
      ZeroHom.toFun
        (↑(comp (MonoidWithZeroHom.fst α β)
              (WithZero.map' (MulEquiv.toMonoidHom (MulEquiv.symm (toLexMulEquiv (Prod.{u_1, u_2} αˣ βˣ)))))) :
          ZeroHom (WithZero (Lex (αˣ × βˣ))) α)
        y
have zero : LE.le (α := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) 0 0 →
  ZeroHom.toFun (M := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
      (↑(comp (MonoidWithZeroHom.fst α β)
            (WithZero.map' (MulEquiv.toMonoidHom (MulEquiv.symm (toLexMulEquiv (Prod.{u_1, u_2} αˣ βˣ)))))) :
        ZeroHom (WithZero (Lex (αˣ × βˣ))) α)
      0 ≤
    ZeroHom.toFun (M := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
      (↑(comp (MonoidWithZeroHom.fst α β)
            (WithZero.map' (MulEquiv.toMonoidHom (MulEquiv.symm (toLexMulEquiv (Prod.{u_1, u_2} αˣ βˣ)))))) :
        ZeroHom (WithZero (Lex (αˣ × βˣ))) α)
      0
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
inst_1 : LinearOrderedCommGroupWithZero β
y : WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))
zero :
  LE.le (α := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) 0 0 →
    ZeroHom.toFun (M := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
        (↑(comp (MonoidWithZeroHom.fst α β)
              (WithZero.map' (MulEquiv.toMonoidHom (MulEquiv.symm (toLexMulEquiv (Prod.{u_1, u_2} αˣ βˣ)))))) :
          ZeroHom (WithZero (Lex (αˣ × βˣ))) α)
        0 ≤
      ZeroHom.toFun (M := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
        (↑(comp (MonoidWithZeroHom.fst α β)
              (WithZero.map' (MulEquiv.toMonoidHom (MulEquiv.symm (toLexMulEquiv (Prod.{u_1, u_2} αˣ βˣ)))))) :
          ZeroHom (WithZero (Lex (αˣ × βˣ))) α)
        0
⊢ 0 ≤ y →
    ZeroHom.toFun (M := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
        (↑(comp (MonoidWithZeroHom.fst α β)
              (WithZero.map' (MulEquiv.toMonoidHom (MulEquiv.symm (toLexMulEquiv (Prod.{u_1, u_2} αˣ βˣ)))))) :
          ZeroHom (WithZero (Lex (αˣ × βˣ))) α)
        0 ≤
      ZeroHom.toFun
        (↑(comp (MonoidWithZeroHom.fst α β)
              (WithZero.map' (MulEquiv.toMonoidHom (MulEquiv.symm (toLexMulEquiv (Prod.{u_1, u_2} αˣ βˣ)))))) :
          ZeroHom (WithZero (Lex (αˣ × βˣ))) α)
        y
have zero₁ : ∀ (a : Lex (Prod.{u_1, u_2} αˣ βˣ)),
  0 ≤ (↑a : WithZero (Lex (αˣ × βˣ))) →
    ZeroHom.toFun (M := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
        (↑(comp (MonoidWithZeroHom.fst α β)
              (WithZero.map' (MulEquiv.toMonoidHom (MulEquiv.symm (toLexMulEquiv (Prod.{u_1, u_2} αˣ βˣ)))))) :
          ZeroHom (WithZero (Lex (αˣ × βˣ))) α)
        0 ≤
      ZeroHom.toFun
        (↑(comp (MonoidWithZeroHom.fst α β)
              (WithZero.map' (MulEquiv.toMonoidHom (MulEquiv.symm (toLexMulEquiv (Prod.{u_1, u_2} αˣ βˣ)))))) :
          ZeroHom (WithZero (Lex (αˣ × βˣ))) α)
        (↑a : WithZero (Lex (αˣ × βˣ)))
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
inst_1 : LinearOrderedCommGroupWithZero β
y : WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))
a : Lex (Prod.{u_1, u_2} αˣ βˣ)
⊢ (↑a : WithZero (Lex (αˣ × βˣ))) ≤ y →
    ZeroHom.toFun
        (↑(comp (MonoidWithZeroHom.fst α β)
              (WithZero.map' (MulEquiv.toMonoidHom (MulEquiv.symm (toLexMulEquiv (Prod.{u_1, u_2} αˣ βˣ)))))) :
          ZeroHom (WithZero (Lex (αˣ × βˣ))) α)
        (↑a : WithZero (Lex (αˣ × βˣ))) ≤
      ZeroHom.toFun
        (↑(comp (MonoidWithZeroHom.fst α β)
              (WithZero.map' (MulEquiv.toMonoidHom (MulEquiv.symm (toLexMulEquiv (Prod.{u_1, u_2} αˣ βˣ)))))) :
          ZeroHom (WithZero (Lex (αˣ × βˣ))) α)
        y
have coe : (↑a : WithZero (Lex (αˣ × βˣ))) ≤ 0 →
  ZeroHom.toFun
      (↑(comp (MonoidWithZeroHom.fst α β)
            (WithZero.map' (MulEquiv.toMonoidHom (MulEquiv.symm (toLexMulEquiv (Prod.{u_1, u_2} αˣ βˣ)))))) :
        ZeroHom (WithZero (Lex (αˣ × βˣ))) α)
      (↑a : WithZero (Lex (αˣ × βˣ))) ≤
    ZeroHom.toFun (M := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
      (↑(comp (MonoidWithZeroHom.fst α β)
            (WithZero.map' (MulEquiv.toMonoidHom (MulEquiv.symm (toLexMulEquiv (Prod.{u_1, u_2} αˣ βˣ)))))) :
        ZeroHom (WithZero (Lex (αˣ × βˣ))) α)
      0
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
inst_1 : LinearOrderedCommGroupWithZero β
y : WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))
a : Lex (Prod.{u_1, u_2} αˣ βˣ)
coe :
  (↑a : WithZero (Lex (αˣ × βˣ))) ≤ 0 →
    ZeroHom.toFun
        (↑(comp (MonoidWithZeroHom.fst α β)
              (WithZero.map' (MulEquiv.toMonoidHom (MulEquiv.symm (toLexMulEquiv (Prod.{u_1, u_2} αˣ βˣ)))))) :
          ZeroHom (WithZero (Lex (αˣ × βˣ))) α)
        (↑a : WithZero (Lex (αˣ × βˣ))) ≤
      ZeroHom.toFun (M := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
        (↑(comp (MonoidWithZeroHom.fst α β)
              (WithZero.map' (MulEquiv.toMonoidHom (MulEquiv.symm (toLexMulEquiv (Prod.{u_1, u_2} αˣ βˣ)))))) :
          ZeroHom (WithZero (Lex (αˣ × βˣ))) α)
        0
⊢ (↑a : WithZero (Lex (αˣ × βˣ))) ≤ y →
    ZeroHom.toFun
        (↑(comp (MonoidWithZeroHom.fst α β)
              (WithZero.map' (MulEquiv.toMonoidHom (MulEquiv.symm (toLexMulEquiv (Prod.{u_1, u_2} αˣ βˣ)))))) :
          ZeroHom (WithZero (Lex (αˣ × βˣ))) α)
        (↑a : WithZero (Lex (αˣ × βˣ))) ≤
      ZeroHom.toFun
        (↑(comp (MonoidWithZeroHom.fst α β)
              (WithZero.map' (MulEquiv.toMonoidHom (MulEquiv.symm (toLexMulEquiv (Prod.{u_1, u_2} αˣ βˣ)))))) :
          ZeroHom (WithZero (Lex (αˣ × βˣ))) α)
        y
have coe₁ : ∀ (a_1 : Lex (Prod.{u_1, u_2} αˣ βˣ)),
  (↑a : WithZero (Lex (αˣ × βˣ))) ≤ (↑a_1 : WithZero (Lex (αˣ × βˣ))) →
    ZeroHom.toFun
        (↑(comp (MonoidWithZeroHom.fst α β)
              (WithZero.map' (MulEquiv.toMonoidHom (MulEquiv.symm (toLexMulEquiv (Prod.{u_1, u_2} αˣ βˣ)))))) :
          ZeroHom (WithZero (Lex (αˣ × βˣ))) α)
        (↑a : WithZero (Lex (αˣ × βˣ))) ≤
      ZeroHom.toFun
        (↑(comp (MonoidWithZeroHom.fst α β)
              (WithZero.map' (MulEquiv.toMonoidHom (MulEquiv.symm (toLexMulEquiv (Prod.{u_1, u_2} αˣ βˣ)))))) :
          ZeroHom (WithZero (Lex (αˣ × βˣ))) α)
        (↑a_1 : WithZero (Lex (αˣ × βˣ)))
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
inst_1 : LinearOrderedCommGroupWithZero β
⊢ Eq (α := α →*₀o α) (OrderMonoidWithZeroHom.comp (β := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) (fst α β) (inl α β))
    (OrderMonoidWithZeroHom.id α)
have h : ∀ (x : α),
  Eq (α := α)
    ((OrderMonoidWithZeroHom.comp (β := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) (fst α β) (inl α β) : (a : α) → α) x :
      α)
    ((OrderMonoidWithZeroHom.id α : (a : α) → α) x : α)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
inst_1 : LinearOrderedCommGroupWithZero β
x : α
⊢ Eq (α := α)
    ((OrderMonoidWithZeroHom.comp (β := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) (fst α β) (inl α β) : (a : α) → α) x :
      α)
    ((OrderMonoidWithZeroHom.id α : (a : α) → α) x : α)
have h : Eq (α := α)
  ((OrderMonoidWithZeroHom.comp (β := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) (fst α β) (inl α β) : (a : α) → α) 0 : α)
  ((OrderMonoidWithZeroHom.id α : (a : α) → α) 0 : α)
Tactic: obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
inst_1 : LinearOrderedCommGroupWithZero β
x : α
h :
  Eq (α := α)
    ((OrderMonoidWithZeroHom.comp (β := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) (fst α β) (inl α β) : (a : α) → α) 0 :
      α)
    ((OrderMonoidWithZeroHom.id α : (a : α) → α) 0 : α)
⊢ Eq (α := α)
    ((OrderMonoidWithZeroHom.comp (β := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) (fst α β) (inl α β) : (a : α) → α) x :
      α)
    ((OrderMonoidWithZeroHom.id α : (a : α) → α) x : α)
have h₁ : ∀ (w : αˣ),
  Eq (α := α)
    ((OrderMonoidWithZeroHom.comp (β := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) (fst α β) (inl α β) : (a : α) → α)
        (↑w : α) :
      α)
    ((OrderMonoidWithZeroHom.id α : (a : α) → α) (↑w : α) : α)
Tactic: obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
inst_1 : LinearOrderedCommGroupWithZero β
m : α
hm : m ≠ 0
⊢ Eq (α := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
    ((inl α β : (a : α) → WithZero (Lex (αˣ × βˣ))) m : WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
    ((↑((OrderMonoidHom.inlₗ αˣ βˣ : (a : αˣ) → Lex (αˣ × βˣ)) (Units.mk0 m hm)) :
        WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) :
      WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
have lift : ∀ (m : αˣ) (hm : (↑m : α) ≠ 0),
  Eq (α := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
    ((inl α β : (a : α) → WithZero (Lex (αˣ × βˣ))) (↑m : α) : WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
    ((↑((OrderMonoidHom.inlₗ αˣ βˣ : (a : αˣ) → Lex (αˣ × βˣ)) (Units.mk0 (↑m : α) hm)) :
        WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) :
      WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
Tactic: lift m to αˣ using isUnit_iff_ne_zero.mpr hm
Cleared hypotheses: m, hm