-- Module: Mathlib.RingTheory.Valuation.Basic
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 : Γ'₀)
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) ⋯)⁻¹ : Γ₀ˣ)
            (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 : Γ₀)),
    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) ⋯)⁻¹ : Γ₀ˣ)
                                  (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) ⋯ : Γ₀ˣ))
                                ⋯) :
                            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) ⋯)⁻¹ : Γ₀ˣ)
                                  (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) ⋯ : Γ₀ˣ))
                                ⋯) :
                            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) ⋯)⁻¹ : Γ₀ˣ)
                                  (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) ⋯ : Γ₀ˣ))
                                ⋯) :
                            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) ⋯)⁻¹ : Γ₀ˣ)
                                  (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) ⋯ : Γ₀ˣ))
                                ⋯) :
                            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) ⋯)⁻¹ : Γ₀ˣ)
                                  (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) ⋯ : Γ₀ˣ))
                                ⋯) :
                            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) ⋯)⁻¹ : Γ₀ˣ)
                                  (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) ⋯ : Γ₀ˣ))
                                ⋯) :
                            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) ⋯)⁻¹ : Γ₀ˣ)
                                  (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) ⋯ : Γ₀ˣ))
                                ⋯) :
                            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) ⋯)⁻¹ : Γ₀ˣ)
                                  (Units.mk0 ((v : (a : R) → Γ₀) (↑d : R × R).2) ⋯ : Γ₀ˣ))
                                ⋯) :
                            WithZero ↥(valueGroup v)))) :
                    R × R).1)
              hy20 :
            Γ₀ˣ)
⊢ 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)
            ⋯ :
          Γ₀ˣ)

Tactic:
generalize_proofs _ hx' hy' hx20 hy10 hx10 hy20