-- 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 : Γ'₀)
⊢ LE.le (α := ValueGroup₀ w)
      (↑(valueGroup.mk w
            (↑(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
            (↑(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
            pf_4 pf_5) :
        WithZero ↥(valueGroup w))
      (↑(valueGroup.mk w
            (↑(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
            (↑(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
            pf_6 pf_7) :
        WithZero ↥(valueGroup w)) ↔
    LE.le (α := ValueGroup₀ v)
      (↑(valueGroup.mk v
            (↑(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
            (↑(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
            ⋯ ⋯) :
        WithZero ↥(valueGroup v))
      (↑(valueGroup.mk v
            (↑(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
            (↑(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
            ⋯ ⋯) :
        WithZero ↥(valueGroup v))
have neg : HMul.hMul (α := Γ'₀ˣ) (β := Γ'₀ˣ)
      ((Units.mk0
            ((w : (a : R) → Γ'₀)
              (↑(sorry.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)⁻¹ :
        Γ'₀ˣ)
      (Units.mk0
          ((w : (a : R) → Γ'₀)
            (↑(sorry.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 :
        Γ'₀ˣ) ≤
    HMul.hMul (α := Γ'₀ˣ) (β := Γ'₀ˣ)
      ((Units.mk0
            ((w : (a : R) → Γ'₀)
              (↑(sorry.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)⁻¹ :
        Γ'₀ˣ)
      (Units.mk0
          ((w : (a : R) → Γ'₀)
            (↑(sorry.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 :
        Γ'₀ˣ) ↔
  HMul.hMul (α := Γ₀ˣ) (β := Γ₀ˣ)
      ((Units.mk0
            ((v : (a : R) → Γ₀)
              (↑(sorry.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
          ((v : (a : R) → Γ₀)
            (↑(sorry.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)
          sorry :
        Γ₀ˣ) ≤
    HMul.hMul (α := Γ₀ˣ) (β := Γ₀ˣ)
      ((Units.mk0
            ((v : (a : R) → Γ₀)
              (↑(sorry.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
          ((v : (a : R) → Γ₀)
            (↑(sorry.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)
          sorry :
        Γ₀ˣ)
Tactic: simp only [valueGroup.mk, WithZero.coe_le_coe, Subtype.mk_le_mk]