-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
x : K
x_in₁ : x ∈ M₁
y : K
left : y ∈ M₀
y_in₁ : y ∈ M₁
H₁ :
  (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
    (↑(min (γ * γ₀ * γ₀) γ₀) : MonoidWithZeroHom.ValueGroup₀ v)
x_in₀ :
  (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
    (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x
h :
  min (↑(γ * γ₀ * γ₀) : MonoidWithZeroHom.ValueGroup₀ v) (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
    min
      ((↑γ : MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) *
        HMul.hMul (α := MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) (β :=
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
          ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x :
            MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
          ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x :
            MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)))
      ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x)
h₁ :
  min (↑(γ * (γ₀ * γ₀)) : MonoidWithZeroHom.ValueGroup₀ v) (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
    min
      ((↑γ : MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) *
        HMul.hMul (α := MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) (β :=
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
          ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x :
            MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
          ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x :
            MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)))
      ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x)
⊢ (↑(min (γ * γ₀ * γ₀) γ₀) : MonoidWithZeroHom.ValueGroup₀ v) ≤
    min
      ((↑γ : MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) *
        HMul.hMul (α := MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) (β :=
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
          ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x :
            MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
          ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x :
            MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)))
      ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x)
have h₂ : min ((↑γ : MonoidWithZeroHom.ValueGroup₀ v) * (↑(γ₀ * γ₀) : MonoidWithZeroHom.ValueGroup₀ v))
    (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
  min
    ((↑γ : MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) *
      HMul.hMul (α := MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) (β :=
        MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
        ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x :
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
        ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x :
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)))
    ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x)
Tactic: grw [Units.min_val, mul_assoc, Units.val_mul, Units.val_mul, x_in₀]