-- Module: Mathlib.GroupTheory.ArchimedeanDensely
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)
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
⊢ 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

Tactic:
split_ifs