awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
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 : N₀ˣ
⊢ (↑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:
simp [WithZero.withZeroUnitsEquiv]

Premises used: WithZero.withZeroUnitsEquiv
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
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 : 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:
simp [WithZero.withZeroUnitsEquiv]

Premises used: WithZero.withZeroUnitsEquiv
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : GroupWithZero M₀
inst_1 : PartialOrder M₀
inst_2 : LinearOrderedCommGroupWithZero N₀
inst_3 : DecidablePred fun (x : N₀) ↦ x = 0
⊢ StrictMono (α := N₀) (β := WithZero (Prod.{u_1, u_2} M₀ˣ N₀ˣ)) (⇑(inr M₀ N₀) : (a : N₀) → WithZero (M₀ˣ × N₀ˣ))

Tactic:
inr_mono.strictMono_of_injective inr_injective

Premises used: Monotone.strictMono_of_injective, MonoidWithZeroHom.inr_injective
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
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₀)

Tactic:
WithZero.forall.mpr ?_

Premises used: Iff.mpr, Monotone, WithZero.forall
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : LinearOrderedCommGroupWithZero M₀
inst_1 : GroupWithZero N₀
inst_2 : Preorder N₀
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₀)
⊢ Monotone (α := WithZero (Prod.{u_1, u_2} M₀ˣ N₀ˣ)) (β := M₀) (⇑(fst M₀ N₀) : (a : WithZero (M₀ˣ × N₀ˣ)) → M₀)

Tactic:
refine WithZero.forall.mpr ?_

Premises used: Iff.mpr, WithZero.forall
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : LinearOrderedCommGroupWithZero M₀
inst_1 : GroupWithZero N₀
inst_2 : Preorder N₀
⊢ (∀ ⦃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:
simp +contextual [WithZero.forall, Prod.le_def]

Premises used: WithZero.forall, Prod.le_def
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
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₀)

Tactic:
WithZero.forall.mpr ?_

Premises used: Iff.mpr, Monotone, WithZero.forall
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : GroupWithZero M₀
inst_1 : Preorder M₀
inst_2 : LinearOrderedCommGroupWithZero N₀
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₀)
⊢ Monotone (α := WithZero (Prod.{u_1, u_2} M₀ˣ N₀ˣ)) (β := N₀) (⇑(snd M₀ N₀) : (a : WithZero (M₀ˣ × N₀ˣ)) → N₀)

Tactic:
refine WithZero.forall.mpr ?_

Premises used: Iff.mpr, WithZero.forall
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : GroupWithZero M₀
inst_1 : Preorder M₀
inst_2 : LinearOrderedCommGroupWithZero N₀
⊢ (∀ ⦃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:
simp [WithZero.forall, Prod.le_def]

Premises used: WithZero.forall, Prod.le_def
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
inst_1 : LinearOrderedCommGroupWithZero β
⊢ Monotone (β := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
    (ZeroHom.toFun
      (↑(comp (WithZero.map' (MulEquiv.toMonoidHom (toLexMulEquiv (Prod.{u_1, u_2} αˣ βˣ))))
            (MonoidWithZeroHom.inl α β)) :
        ZeroHom α (WithZero (Lex (αˣ × βˣ)))))

Tactic:
simpa using (WithZero.map'_mono (Prod.Lex.toLex_mono)).comp inl_mono

Premises used: WithZero.map'_mono, Monotone.comp, MonoidWithZeroHom.inl_mono
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
inst_1 : LinearOrderedCommGroupWithZero β
⊢ Monotone (β := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
    (ZeroHom.toFun
      (↑(comp (WithZero.map' (MulEquiv.toMonoidHom (toLexMulEquiv (Prod.{u_1, u_2} αˣ βˣ))))
            (MonoidWithZeroHom.inr α β)) :
        ZeroHom β (WithZero (Lex (αˣ × βˣ)))))

Tactic:
simpa using (WithZero.map'_mono (Prod.Lex.toLex_mono)).comp inr_mono

Premises used: WithZero.map'_mono, Monotone.comp, MonoidWithZeroHom.inr_mono
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
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
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
⊢ 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

Tactic:
cases x
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
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
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 (αˣ × βˣ)))
⊢ 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 y
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
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
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 (αˣ × βˣ)))
⊢ (↑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 y
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
inst_1 : LinearOrderedCommGroupWithZero β
⊢ 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:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
inst_1 : LinearOrderedCommGroupWithZero β
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:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
inst_1 : LinearOrderedCommGroupWithZero β
a : Lex (Prod.{u_1, u_2} αˣ βˣ)
⊢ (↑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:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
inst_1 : LinearOrderedCommGroupWithZero β
a 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:
simpa using Prod.Lex.monotone_fst _ _

Premises used: Prod.Lex.monotone_fst
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
inst_1 : LinearOrderedCommGroupWithZero β
h :
  ∀ (x : α),
    Eq (α := α)
      ((OrderMonoidWithZeroHom.comp (β := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) (fst α β) (inl α β) : (a : α) → α) x :
        α)
      ((OrderMonoidWithZeroHom.id α : (a : α) → α) x : α)
⊢ Eq (α := α →*₀o α) (OrderMonoidWithZeroHom.comp (β := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) (fst α β) (inl α β))
    (OrderMonoidWithZeroHom.id α)

Tactic:
ext x
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
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 : α)
h₁ :
  ∀ (w : αˣ),
    Eq (α := α)
      ((OrderMonoidWithZeroHom.comp (β := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) (fst α β) (inl α β) : (a : α) → α)
          (↑w : α) :
        α)
      ((OrderMonoidWithZeroHom.id α : (a : α) → α) (↑w : α) : α)
⊢ Eq (α := α)
    ((OrderMonoidWithZeroHom.comp (β := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) (fst α β) (inl α β) : (a : α) → α) x :
      α)
    ((OrderMonoidWithZeroHom.id α : (a : α) → α) x : α)

Tactic:
obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit x

Premises used: GroupWithZero.eq_zero_or_unit, rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
inst_1 : LinearOrderedCommGroupWithZero β
⊢ Eq (α := α)
    ((OrderMonoidWithZeroHom.comp (β := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) (fst α β) (inl α β) : (a : α) → α) 0 :
      α)
    ((OrderMonoidWithZeroHom.id α : (a : α) → α) 0 : α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
inst_1 : LinearOrderedCommGroupWithZero β
w : αˣ
⊢ Eq (α := α)
    ((OrderMonoidWithZeroHom.comp (β := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) (fst α β) (inl α β) : (a : α) → α)
        (↑w : α) :
      α)
    ((OrderMonoidWithZeroHom.id α : (a : α) → α) (↑w : α) : α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
inst_1 : LinearOrderedCommGroupWithZero β
m : α
hm : m ≠ 0
⊢ IsUnit m

Tactic:
isUnit_iff_ne_zero.mpr hm

Premises used: Iff.mpr, isUnit_iff_ne_zero
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
inst_1 : LinearOrderedCommGroupWithZero β
m : α
hm : m ≠ 0
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} αˣ βˣ)))
⊢ 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

Premises used: Iff.mpr, isUnit_iff_ne_zero
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
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} αˣ βˣ)))

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
inst_1 : LinearOrderedCommGroupWithZero β
n : β
hn : n ≠ 0
⊢ IsUnit n

Tactic:
isUnit_iff_ne_zero.mpr hn

Premises used: Iff.mpr, isUnit_iff_ne_zero
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
inst_1 : LinearOrderedCommGroupWithZero β
n : β
hn : n ≠ 0
lift :
  ∀ (n : βˣ) (hn : (↑n : β) ≠ 0),
    Eq (α := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
      ((inr α β : (a : β) → WithZero (Lex (αˣ × βˣ))) (↑n : β) : WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
      ((↑((OrderMonoidHom.inrₗ αˣ βˣ : (a : βˣ) → Lex (αˣ × βˣ)) (Units.mk0 (↑n : β) hn)) :
          WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) :
        WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
⊢ Eq (α := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
    ((inr α β : (a : β) → WithZero (Lex (αˣ × βˣ))) n : WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
    ((↑((OrderMonoidHom.inrₗ αˣ βˣ : (a : βˣ) → Lex (αˣ × βˣ)) (Units.mk0 n hn)) :
        WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) :
      WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))

Tactic:
lift n to βˣ using isUnit_iff_ne_zero.mpr hn

Premises used: Iff.mpr, isUnit_iff_ne_zero
-- Module: Mathlib.Algebra.Order.GroupWithZero.Lex
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
inst_1 : LinearOrderedCommGroupWithZero β
n : βˣ
hn : (↑n : β) ≠ 0
⊢ Eq (α := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
    ((inr α β : (a : β) → WithZero (Lex (αˣ × βˣ))) (↑n : β) : WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
    ((↑((OrderMonoidHom.inrₗ αˣ βˣ : (a : βˣ) → Lex (αˣ × βˣ)) (Units.mk0 (↑n : β) hn)) :
        WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) :
      WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))

Tactic:
simp