-- Lean 4 proof step from Mathlib.GroupTheory.ArchimedeanDensely (goal)
Goal:
G : Type u_2
inst : LinearOrderedCommGroupWithZero G
inst_1 : Nontrivial.{u_2} Gˣ
inst_2 : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
a b : G
pos :
  a = 0 →
    b = 0 →
      (LE.le (α := WithZero (Multiplicative ℤ))
          (((map' (↑(↑f : Gˣ ≃* Multiplicative ℤ) : Gˣ →* Multiplicative ℤ) :
                  WithZero Gˣ →*₀ WithZero (Multiplicative ℤ)) :
                (a : WithZero Gˣ) → WithZero (Multiplicative ℤ))
              0 :
            WithZero (Multiplicative ℤ))
          (((map' (↑(↑f : Gˣ ≃* Multiplicative ℤ) : Gˣ →* Multiplicative ℤ) :
                  WithZero Gˣ →*₀ WithZero (Multiplicative ℤ)) :
                (a : WithZero Gˣ) → WithZero (Multiplicative ℤ))
              0 :
            WithZero (Multiplicative ℤ)) ↔
        a ≤ b)
neg :
  a = 0 →
    ∀ (h : ¬b = 0),
      LE.le (α := WithZero (Multiplicative ℤ))
          (((map' (↑(↑f : Gˣ ≃* Multiplicative ℤ) : Gˣ →* Multiplicative ℤ) :
                  WithZero Gˣ →*₀ WithZero (Multiplicative ℤ)) :
                (a : WithZero Gˣ) → WithZero (Multiplicative ℤ))
              0 :
            WithZero (Multiplicative ℤ))
          (((map' (↑(↑f : Gˣ ≃* Multiplicative ℤ) : Gˣ →* Multiplicative ℤ) :
                  WithZero Gˣ →*₀ WithZero (Multiplicative ℤ)) :
                (a : WithZero Gˣ) → WithZero (Multiplicative ℤ))
              (↑(Units.mk0 b h) : WithZero Gˣ) :
            WithZero (Multiplicative ℤ)) ↔
        a ≤ b
pos₁ :
  ∀ (h : ¬a = 0),
    b = 0 →
      (LE.le (α := WithZero (Multiplicative ℤ))
          (((map' (↑(↑f : Gˣ ≃* Multiplicative ℤ) : Gˣ →* Multiplicative ℤ) :
                  WithZero Gˣ →*₀ WithZero (Multiplicative ℤ)) :
                (a : WithZero Gˣ) → WithZero (Multiplicative ℤ))
              (↑(Units.mk0 a h) : WithZero Gˣ) :
            WithZero (Multiplicative ℤ))
          (((map' (↑(↑f : Gˣ ≃* Multiplicative ℤ) : Gˣ →* Multiplicative ℤ) :
                  WithZero Gˣ →*₀ WithZero (Multiplicative ℤ)) :
                (a : WithZero Gˣ) → WithZero (Multiplicative ℤ))
              0 :
            WithZero (Multiplicative ℤ)) ↔
        a ≤ b)
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      (((map' (↑(↑f : Gˣ ≃* Multiplicative ℤ) : Gˣ →* Multiplicative ℤ) : WithZero Gˣ →*₀ WithZero (Multiplicative ℤ)) :
            (a : WithZero Gˣ) → WithZero (Multiplicative ℤ))
          (if h : a = 0 then 0 else (↑(Units.mk0 a h) : WithZero Gˣ)) :
        WithZero (Multiplicative ℤ))
      (((map' (↑(↑f : Gˣ ≃* Multiplicative ℤ) : Gˣ →* Multiplicative ℤ) : WithZero Gˣ →*₀ WithZero (Multiplicative ℤ)) :
            (a : WithZero Gˣ) → WithZero (Multiplicative ℤ))
          (if h : b = 0 then 0 else (↑(Units.mk0 b h) : WithZero Gˣ)) :
        WithZero (Multiplicative ℤ)) ↔
    a ≤ b
have neg₁ : ∀ (h : ¬a = 0) (h_1 : ¬b = 0),
  LE.le (α := WithZero (Multiplicative ℤ))
      (((map' (↑(↑f : Gˣ ≃* Multiplicative ℤ) : Gˣ →* Multiplicative ℤ) : WithZero Gˣ →*₀ WithZero (Multiplicative ℤ)) :
            (a : WithZero Gˣ) → WithZero (Multiplicative ℤ))
          (↑(Units.mk0 a h) : WithZero Gˣ) :
        WithZero (Multiplicative ℤ))
      (((map' (↑(↑f : Gˣ ≃* Multiplicative ℤ) : Gˣ →* Multiplicative ℤ) : WithZero Gˣ →*₀ WithZero (Multiplicative ℤ)) :
            (a : WithZero Gˣ) → WithZero (Multiplicative ℤ))
          (↑(Units.mk0 b h_1) : WithZero Gˣ) :
        WithZero (Multiplicative ℤ)) ↔
    a ≤ b
Tactic: split_ifs