-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : LinearOrderedCommGroupWithZero Γ'₀
inst_2 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
h : v.IsEquiv w
r s : R
hr : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) (0 : Γ₀)
hs : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) s : Γ₀) (0 : Γ₀)
⊢ Eq (α := ValueGroup₀ w)
    (have c :=
      ⋯.choose (p :=
        fun
          (d :
            { xy : R × R //
              Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
        Eq (α := ValueGroup₀ v) (↑(valueGroup.mk v r s hr hs) : WithZero ↥(valueGroup v))
          (↑(valueGroup.mk v (↑d : R × R).1 (↑d : R × R).2 ⋯ ⋯) : WithZero ↥(valueGroup v)));
    (↑(valueGroup.mk w (↑c : R × R).1 (↑c : R × R).2 ⋯ ⋯) : WithZero ↥(valueGroup w)))
    (↑(valueGroup.mk w r s ⋯ ⋯) : WithZero ↥(valueGroup w))
have generalize_proofs : ∀ (pf : MonoidWithZeroHomClass (Valuation R Γ'₀) R Γ'₀) (pf_1 : MonoidWithZeroHomClass (Valuation R Γ₀) R Γ₀)
  (pf_2 :
    ∀
      (d :
        { xy : R × R //
          Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
            Ne.{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 //
          Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
            Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }),
      Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (↑d : R × R).2 : Γ₀) (0 : Γ₀))
  (H :
    ∃ (d :
      { xy : R × R //
        Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
          Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }),
      Eq (α := ValueGroup₀ v) (↑(valueGroup.mk v r s hr hs) : WithZero ↥(valueGroup v))
        (↑(valueGroup.mk v (↑d : R × R).1 (↑d : R × R).2 sorry sorry) : WithZero ↥(valueGroup v)))
  (pf_4 :
    ∀
      (c :
        { xy : R × R //
          Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
            Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }),
      Ne.{u_5 + 1} (α := Γ'₀) ((w : (a : R) → Γ'₀) (↑c : R × R).1 : Γ'₀) (0 : Γ'₀))
  (pf_5 :
    ∀
      (c :
        { xy : R × R //
          Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
            Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }),
      Ne.{u_5 + 1} (α := Γ'₀) ((w : (a : R) → Γ'₀) (↑c : R × R).2 : Γ'₀) (0 : Γ'₀))
  (pf_6 : Ne.{u_5 + 1} (α := Γ'₀) ((w : (a : R) → Γ'₀) r : Γ'₀) (0 : Γ'₀))
  (pf_7 : Ne.{u_5 + 1} (α := Γ'₀) ((w : (a : R) → Γ'₀) s : Γ'₀) (0 : Γ'₀)),
  Eq (α := ValueGroup₀ w)
    (have c :=
      H.choose (p :=
        fun
          (d :
            { xy : R × R //
              Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
        Eq (α := ValueGroup₀ v) (↑(valueGroup.mk v r s hr hs) : WithZero ↥(valueGroup v))
          (↑(valueGroup.mk v (↑d : R × R).1 (↑d : R × R).2 sorry sorry) : WithZero ↥(valueGroup v)));
    (↑(valueGroup.mk w (↑c : R × R).1 (↑c : R × R).2 sorry sorry) : WithZero ↥(valueGroup w)))
    (↑(valueGroup.mk w r s pf_6 pf_7) : WithZero ↥(valueGroup w))
Tactic: generalize_proofs _ _ _ _ H _