-- 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 : Γ'₀)
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 : Γ₀)
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) ⋯)⁻¹ : Γ₀ˣ)
                                    (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 :
                Γ₀))
            ⋯) :
        Γ₀)
⊢ 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 :
            Γ₀))
        ⋯

Tactic:
simp only [← Units.val_le_val]

Premises used: Units.val_le_val