-- 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 : Γ'₀)
⊢ HMul.hMul (α := Γ'₀ˣ) (β := Γ'₀ˣ)
        (Units.mk0
            ((w : (a : R) → Γ'₀)
              (↑(⋯.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)
            pf_5 :
          Γ'₀ˣ)
        (Units.mk0
            ((w : (a : R) → Γ'₀)
              (↑(⋯.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)
            pf_6 :
          Γ'₀ˣ) ≤
      HMul.hMul (α := Γ'₀ˣ) (β := Γ'₀ˣ)
        (Units.mk0
            ((w : (a : R) → Γ'₀)
              (↑(⋯.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)
            pf_7 :
          Γ'₀ˣ)
        (Units.mk0
            ((w : (a : R) → Γ'₀)
              (↑(⋯.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)
            pf_4 :
          Γ'₀ˣ) ↔
    HMul.hMul (α := Γ₀ˣ) (β := Γ₀ˣ)
        (Units.mk0
            ((v : (a : R) → Γ₀)
              (↑(⋯.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)
            ⋯ :
          Γ₀ˣ)
        (Units.mk0
            ((v : (a : R) → Γ₀)
              (↑(⋯.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)
            ⋯ :
          Γ₀ˣ) ≤
      HMul.hMul (α := Γ₀ˣ) (β := Γ₀ˣ)
        (Units.mk0
            ((v : (a : R) → Γ₀)
              (↑(⋯.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)
            ⋯ :
          Γ₀ˣ)
        (Units.mk0
            ((v : (a : R) → Γ₀)
              (↑(⋯.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 : ∀
  (pf :
    ∀
      (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) sorry)⁻¹ : Γ₀ˣ)
          (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) sorry : Γ₀ˣ)))
  (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) sorry)⁻¹ : Γ₀ˣ)
                (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) sorry : Γ₀ˣ))
              sorry) :
          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) sorry)⁻¹ : Γ₀ˣ)
                (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) sorry : Γ₀ˣ))
              sorry) :
          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) sorry)⁻¹ : Γ₀ˣ)
                            (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) sorry : Γ₀ˣ))
                          sorry) :
                      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) sorry)⁻¹ : Γ₀ˣ)
                            (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) sorry : Γ₀ˣ))
                          sorry) :
                      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) sorry)⁻¹ : Γ₀ˣ)
                            (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) sorry : Γ₀ˣ))
                          sorry) :
                      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) sorry)⁻¹ : Γ₀ˣ)
                            (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) sorry : Γ₀ˣ))
                          sorry) :
                      WithZero ↥(valueGroup v)))) :
              R × R).1 :
        Γ₀)
      (0 : Γ₀)),
  HMul.hMul (α := Γ'₀ˣ) (β := Γ'₀ˣ)
        (Units.mk0
            ((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)
            pf_5 :
          Γ'₀ˣ)
        (Units.mk0
            ((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)
            pf_6 :
          Γ'₀ˣ) ≤
      HMul.hMul (α := Γ'₀ˣ) (β := Γ'₀ˣ)
        (Units.mk0
            ((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)
            pf_7 :
          Γ'₀ˣ)
        (Units.mk0
            ((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)
            pf_4 :
          Γ'₀ˣ) ↔
    HMul.hMul (α := Γ₀ˣ) (β := Γ₀ˣ)
        (Units.mk0
            ((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)
            hx20 :
          Γ₀ˣ)
        (Units.mk0
            ((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)
            hy10 :
          Γ₀ˣ) ≤
      HMul.hMul (α := Γ₀ˣ) (β := Γ₀ˣ)
        (Units.mk0
            ((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)
            hx10 :
          Γ₀ˣ)
        (Units.mk0
            ((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)
            hy20 :
          Γ₀ˣ)
Tactic: generalize_proofs _ hx' hy' hx20 hy10 hx10 hy20