-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
inst_3 : LinearOrderedCommGroupWithZero Γ''₀
inst_4 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
x y : ValueGroup₀ v
hx0 : ¬x = 0
hy0 : ¬y = 0
pf : MonoidWithZeroHomClass (Valuation R Γ'₀) R Γ'₀
pf_1 : MonoidWithZeroHomClass (Valuation R Γ₀) R Γ₀
pf_2 :
  ∀
    (d :
      { xy : R × R //
        ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
          ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }),
    Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (↑d : R × R).1 : Γ₀) (0 : Γ₀)
pf_3 :
  ∀
    (d :
      { xy : R × R //
        ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
          ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }),
    Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (↑d : R × R).2 : Γ₀) (0 : Γ₀)
hx :
  ∃ (d :
    { xy : R × R //
      ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
        ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }),
    x = (↑(valueGroup.mk v (↑d : R × R).1 (↑d : R × R).2 ⋯ ⋯) : WithZero ↥(valueGroup v))
pf_4 :
  Ne.{u_5 + 1} (α := Γ'₀)
    ((w : (a : R) → Γ'₀)
        (↑(hx.choose (p :=
                fun
                  (d :
                    { xy : R × R //
                      ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                        ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                x = (↑(valueGroup.mk v (↑d : R × R).1 (↑d : R × R).2 ⋯ ⋯) : WithZero ↥(valueGroup v)))) :
            R × R).1 :
      Γ'₀)
    (0 : Γ'₀)
pf_5 :
  Ne.{u_5 + 1} (α := Γ'₀)
    ((w : (a : R) → Γ'₀)
        (↑(hx.choose (p :=
                fun
                  (d :
                    { xy : R × R //
                      ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                        ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                x = (↑(valueGroup.mk v (↑d : R × R).1 (↑d : R × R).2 ⋯ ⋯) : WithZero ↥(valueGroup v)))) :
            R × R).2 :
      Γ'₀)
    (0 : Γ'₀)
hy :
  ∃ (d :
    { xy : R × R //
      ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
        ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }),
    y = (↑(valueGroup.mk v (↑d : R × R).1 (↑d : R × R).2 ⋯ ⋯) : WithZero ↥(valueGroup v))
pf_6 :
  Ne.{u_5 + 1} (α := Γ'₀)
    ((w : (a : R) → Γ'₀)
        (↑(hy.choose (p :=
                fun
                  (d :
                    { xy : R × R //
                      ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                        ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                y = (↑(valueGroup.mk v (↑d : R × R).1 (↑d : R × R).2 ⋯ ⋯) : WithZero ↥(valueGroup v)))) :
            R × R).1 :
      Γ'₀)
    (0 : Γ'₀)
pf_7 :
  Ne.{u_5 + 1} (α := Γ'₀)
    ((w : (a : R) → Γ'₀)
        (↑(hy.choose (p :=
                fun
                  (d :
                    { xy : R × R //
                      ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                        ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                y = (↑(valueGroup.mk v (↑d : R × R).1 (↑d : R × R).2 ⋯ ⋯) : WithZero ↥(valueGroup v)))) :
            R × R).2 :
      Γ'₀)
    (0 : Γ'₀)
pf_8 :
  ∀
    (d :
      { xy : R × R //
        ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
          ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }),
    Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v)
      (HMul.hMul (α := Γ₀ˣ) (β := Γ₀ˣ) ((Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).1) ⋯)⁻¹ : Γ₀ˣ)
        (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) ⋯ : Γ₀ˣ))
hx' :
  ∃ (d :
    { xy : R × R //
      ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
        ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }),
    x =
      (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
            (HMul.hMul (α := Γ₀ˣ) (β := Γ₀ˣ) ((Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).1) ⋯)⁻¹ : Γ₀ˣ)
              (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) ⋯ : Γ₀ˣ))
            ⋯) :
        WithZero ↥(valueGroup v))
hy' :
  ∃ (d :
    { xy : R × R //
      ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
        ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }),
    y =
      (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
            (HMul.hMul (α := Γ₀ˣ) (β := Γ₀ˣ) ((Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).1) ⋯)⁻¹ : Γ₀ˣ)
              (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) ⋯ : Γ₀ˣ))
            ⋯) :
        WithZero ↥(valueGroup v))
hx20 :
  Ne.{u_4 + 1} (α := Γ₀)
    ((v : (a : R) → Γ₀)
        (↑(hx'.choose (p :=
                fun
                  (d :
                    { xy : R × R //
                      ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                        ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                x =
                  (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                        (HMul.hMul (α := Γ₀ˣ) (β := Γ₀ˣ) ((Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).1) ⋯)⁻¹ : Γ₀ˣ)
                          (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) ⋯ : Γ₀ˣ))
                        ⋯) :
                    WithZero ↥(valueGroup v)))) :
            R × R).2 :
      Γ₀)
    (0 : Γ₀)
hy10 :
  Ne.{u_4 + 1} (α := Γ₀)
    ((v : (a : R) → Γ₀)
        (↑(hy'.choose (p :=
                fun
                  (d :
                    { xy : R × R //
                      ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                        ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                y =
                  (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                        (HMul.hMul (α := Γ₀ˣ) (β := Γ₀ˣ) ((Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).1) ⋯)⁻¹ : Γ₀ˣ)
                          (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) ⋯ : Γ₀ˣ))
                        ⋯) :
                    WithZero ↥(valueGroup v)))) :
            R × R).1 :
      Γ₀)
    (0 : Γ₀)
hx10 :
  Ne.{u_4 + 1} (α := Γ₀)
    ((v : (a : R) → Γ₀)
        (↑(hy'.choose (p :=
                fun
                  (d :
                    { xy : R × R //
                      ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                        ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                y =
                  (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                        (HMul.hMul (α := Γ₀ˣ) (β := Γ₀ˣ) ((Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).1) ⋯)⁻¹ : Γ₀ˣ)
                          (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) ⋯ : Γ₀ˣ))
                        ⋯) :
                    WithZero ↥(valueGroup v)))) :
            R × R).2 :
      Γ₀)
    (0 : Γ₀)
hy20 :
  Ne.{u_4 + 1} (α := Γ₀)
    ((v : (a : R) → Γ₀)
        (↑(hx'.choose (p :=
                fun
                  (d :
                    { xy : R × R //
                      ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                        ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                x =
                  (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                        (HMul.hMul (α := Γ₀ˣ) (β := Γ₀ˣ) ((Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).1) ⋯)⁻¹ : Γ₀ˣ)
                          (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) ⋯ : Γ₀ˣ))
                        ⋯) :
                    WithZero ↥(valueGroup v)))) :
            R × R).1 :
      Γ₀)
    (0 : Γ₀)
⊢ LE.le (α := Γ'₀ˣ)
      (Units.mk0
        (HMul.hMul (α := Γ'₀) (β := Γ'₀)
          ((w : (a : R) → Γ'₀)
              (↑(hx'.choose (p :=
                      fun
                        (d :
                          { xy : R × R //
                            ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                              ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                      x =
                        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                              (HMul.hMul (α := Γ₀ˣ) (β := Γ₀ˣ)
                                ((Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).1) ⋯)⁻¹ : Γ₀ˣ)
                                (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) ⋯ : Γ₀ˣ))
                              ⋯) :
                          WithZero ↥(valueGroup v)))) :
                  R × R).2 :
            Γ'₀)
          ((w : (a : R) → Γ'₀)
              (↑(hy'.choose (p :=
                      fun
                        (d :
                          { xy : R × R //
                            ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                              ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                      y =
                        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                              (HMul.hMul (α := Γ₀ˣ) (β := Γ₀ˣ)
                                ((Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).1) ⋯)⁻¹ : Γ₀ˣ)
                                (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) ⋯ : Γ₀ˣ))
                              ⋯) :
                          WithZero ↥(valueGroup v)))) :
                  R × R).1 :
            Γ'₀))
        ⋯)
      (Units.mk0
        (HMul.hMul (α := Γ'₀) (β := Γ'₀)
          ((w : (a : R) → Γ'₀)
              (↑(hy'.choose (p :=
                      fun
                        (d :
                          { xy : R × R //
                            ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                              ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                      y =
                        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                              (HMul.hMul (α := Γ₀ˣ) (β := Γ₀ˣ)
                                ((Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).1) ⋯)⁻¹ : Γ₀ˣ)
                                (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) ⋯ : Γ₀ˣ))
                              ⋯) :
                          WithZero ↥(valueGroup v)))) :
                  R × R).2 :
            Γ'₀)
          ((w : (a : R) → Γ'₀)
              (↑(hx'.choose (p :=
                      fun
                        (d :
                          { xy : R × R //
                            ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                              ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                      x =
                        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                              (HMul.hMul (α := Γ₀ˣ) (β := Γ₀ˣ)
                                ((Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).1) ⋯)⁻¹ : Γ₀ˣ)
                                (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) ⋯ : Γ₀ˣ))
                              ⋯) :
                          WithZero ↥(valueGroup v)))) :
                  R × R).1 :
            Γ'₀))
        ⋯) ↔
    Units.mk0
        (HMul.hMul (α := Γ₀) (β := Γ₀)
          ((v : (a : R) → Γ₀)
              (↑(hx'.choose (p :=
                      fun
                        (d :
                          { xy : R × R //
                            ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                              ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                      x =
                        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                              (HMul.hMul (α := Γ₀ˣ) (β := Γ₀ˣ)
                                ((Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).1) ⋯)⁻¹ : Γ₀ˣ)
                                (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) ⋯ : Γ₀ˣ))
                              ⋯) :
                          WithZero ↥(valueGroup v)))) :
                  R × R).2 :
            Γ₀)
          ((v : (a : R) → Γ₀)
              (↑(hy'.choose (p :=
                      fun
                        (d :
                          { xy : R × R //
                            ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                              ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                      y =
                        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                              (HMul.hMul (α := Γ₀ˣ) (β := Γ₀ˣ)
                                ((Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).1) ⋯)⁻¹ : Γ₀ˣ)
                                (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) ⋯ : Γ₀ˣ))
                              ⋯) :
                          WithZero ↥(valueGroup v)))) :
                  R × R).1 :
            Γ₀))
        ⋯ ≤
      Units.mk0
        (HMul.hMul (α := Γ₀) (β := Γ₀)
          ((v : (a : R) → Γ₀)
              (↑(hy'.choose (p :=
                      fun
                        (d :
                          { xy : R × R //
                            ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                              ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                      y =
                        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                              (HMul.hMul (α := Γ₀ˣ) (β := Γ₀ˣ)
                                ((Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).1) ⋯)⁻¹ : Γ₀ˣ)
                                (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) ⋯ : Γ₀ˣ))
                              ⋯) :
                          WithZero ↥(valueGroup v)))) :
                  R × R).2 :
            Γ₀)
          ((v : (a : R) → Γ₀)
              (↑(hx'.choose (p :=
                      fun
                        (d :
                          { xy : R × R //
                            ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                              ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                      x =
                        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                              (HMul.hMul (α := Γ₀ˣ) (β := Γ₀ˣ)
                                ((Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).1) ⋯)⁻¹ : Γ₀ˣ)
                                (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) ⋯ : Γ₀ˣ))
                              ⋯) :
                          WithZero ↥(valueGroup v)))) :
                  R × R).1 :
            Γ₀))
        ⋯
have neg : (↑(Units.mk0
          (HMul.hMul (α := Γ'₀) (β := Γ'₀)
            ((w : (a : R) → Γ'₀)
                (↑(hx'.choose (p :=
                        fun
                          (d :
                            { xy : R × R //
                              ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                                ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                        x =
                          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                                (HMul.hMul (α := Γ₀ˣ) (β := Γ₀ˣ)
                                  ((Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).1) sorry)⁻¹ : Γ₀ˣ)
                                  (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) sorry : Γ₀ˣ))
                                sorry) :
                            WithZero ↥(valueGroup v)))) :
                    R × R).2 :
              Γ'₀)
            ((w : (a : R) → Γ'₀)
                (↑(hy'.choose (p :=
                        fun
                          (d :
                            { xy : R × R //
                              ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                                ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                        y =
                          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                                (HMul.hMul (α := Γ₀ˣ) (β := Γ₀ˣ)
                                  ((Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).1) sorry)⁻¹ : Γ₀ˣ)
                                  (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) sorry : Γ₀ˣ))
                                sorry) :
                            WithZero ↥(valueGroup v)))) :
                    R × R).1 :
              Γ'₀))
          sorry) :
      Γ'₀) ≤
    (↑(Units.mk0
          (HMul.hMul (α := Γ'₀) (β := Γ'₀)
            ((w : (a : R) → Γ'₀)
                (↑(hy'.choose (p :=
                        fun
                          (d :
                            { xy : R × R //
                              ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                                ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                        y =
                          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                                (HMul.hMul (α := Γ₀ˣ) (β := Γ₀ˣ)
                                  ((Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).1) sorry)⁻¹ : Γ₀ˣ)
                                  (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) sorry : Γ₀ˣ))
                                sorry) :
                            WithZero ↥(valueGroup v)))) :
                    R × R).2 :
              Γ'₀)
            ((w : (a : R) → Γ'₀)
                (↑(hx'.choose (p :=
                        fun
                          (d :
                            { xy : R × R //
                              ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                                ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                        x =
                          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                                (HMul.hMul (α := Γ₀ˣ) (β := Γ₀ˣ)
                                  ((Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).1) sorry)⁻¹ : Γ₀ˣ)
                                  (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) sorry : Γ₀ˣ))
                                sorry) :
                            WithZero ↥(valueGroup v)))) :
                    R × R).1 :
              Γ'₀))
          sorry) :
      Γ'₀) ↔
  (↑(Units.mk0
          (HMul.hMul (α := Γ₀) (β := Γ₀)
            ((v : (a : R) → Γ₀)
                (↑(hx'.choose (p :=
                        fun
                          (d :
                            { xy : R × R //
                              ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                                ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                        x =
                          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                                (HMul.hMul (α := Γ₀ˣ) (β := Γ₀ˣ)
                                  ((Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).1) sorry)⁻¹ : Γ₀ˣ)
                                  (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) sorry : Γ₀ˣ))
                                sorry) :
                            WithZero ↥(valueGroup v)))) :
                    R × R).2 :
              Γ₀)
            ((v : (a : R) → Γ₀)
                (↑(hy'.choose (p :=
                        fun
                          (d :
                            { xy : R × R //
                              ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                                ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                        y =
                          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                                (HMul.hMul (α := Γ₀ˣ) (β := Γ₀ˣ)
                                  ((Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).1) sorry)⁻¹ : Γ₀ˣ)
                                  (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) sorry : Γ₀ˣ))
                                sorry) :
                            WithZero ↥(valueGroup v)))) :
                    R × R).1 :
              Γ₀))
          sorry) :
      Γ₀) ≤
    (↑(Units.mk0
          (HMul.hMul (α := Γ₀) (β := Γ₀)
            ((v : (a : R) → Γ₀)
                (↑(hy'.choose (p :=
                        fun
                          (d :
                            { xy : R × R //
                              ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                                ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                        y =
                          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                                (HMul.hMul (α := Γ₀ˣ) (β := Γ₀ˣ)
                                  ((Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).1) sorry)⁻¹ : Γ₀ˣ)
                                  (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) sorry : Γ₀ˣ))
                                sorry) :
                            WithZero ↥(valueGroup v)))) :
                    R × R).2 :
              Γ₀)
            ((v : (a : R) → Γ₀)
                (↑(hx'.choose (p :=
                        fun
                          (d :
                            { xy : R × R //
                              ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                                ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                        x =
                          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                                (HMul.hMul (α := Γ₀ˣ) (β := Γ₀ˣ)
                                  ((Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).1) sorry)⁻¹ : Γ₀ˣ)
                                  (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) sorry : Γ₀ˣ))
                                sorry) :
                            WithZero ↥(valueGroup v)))) :
                    R × R).1 :
              Γ₀))
          sorry) :
      Γ₀)
Tactic: simp only [← Units.val_le_val]