-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithVal (goal)
Goal:
Γ₀ : Type u_5
Γ₀' : Type u_6
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : LinearOrderedCommGroupWithZero Γ₀'
K : Type u_7
inst_2 : Field K
v : Valuation K Γ₀
w : Valuation K Γ₀'
h : v.IsEquiv w
h1 :
  ∀ (x : UniformSpace.Completion (WithVal v)),
    LE.le.{u_5} (α := Γ₀) ((Valued.v : (a : UniformSpace.Completion (WithVal v)) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      LE.le.{u_5} (α :=
        ValueGroup₀ (F := MonoidWithZeroHom.{u_7, u_5} (UniformSpace.Completion (WithVal v)) Γ₀)
          (↑Valued.v : UniformSpace.Completion (WithVal v) →*₀ Γ₀))
        ((Valuation.restrict Valued.v :
              (a : UniformSpace.Completion (WithVal v)) →
                ValueGroup₀ (↑Valued.v : UniformSpace.Completion (WithVal v) →*₀ Γ₀))
            x :
          ValueGroup₀ (F := MonoidWithZeroHom.{u_7, u_5} (UniformSpace.Completion (WithVal v)) Γ₀)
            (↑Valued.v : UniformSpace.Completion (WithVal v) →*₀ Γ₀))
        (1 :
          ValueGroup₀ (F := MonoidWithZeroHom.{u_7, u_5} (UniformSpace.Completion (WithVal v)) Γ₀)
            (↑Valued.v : UniformSpace.Completion (WithVal v) →*₀ Γ₀))
⊢ IsClosed.{u_7} (X := UniformSpace.Completion (WithVal v))
    {a : UniformSpace.Completion (WithVal v) |
      LE.le.{u_5} (α :=
          ValueGroup₀ (F := MonoidWithZeroHom.{u_7, u_5} (UniformSpace.Completion (WithVal v)) Γ₀)
            (↑Valued.v : UniformSpace.Completion (WithVal v) →*₀ Γ₀))
          ((Valuation.restrict Valued.v :
                (a : UniformSpace.Completion (WithVal v)) →
                  ValueGroup₀ (↑Valued.v : UniformSpace.Completion (WithVal v) →*₀ Γ₀))
              a :
            ValueGroup₀ (F := MonoidWithZeroHom.{u_7, u_5} (UniformSpace.Completion (WithVal v)) Γ₀)
              (↑Valued.v : UniformSpace.Completion (WithVal v) →*₀ Γ₀))
          (1 :
            ValueGroup₀ (F := MonoidWithZeroHom.{u_7, u_5} (UniformSpace.Completion (WithVal v)) Γ₀)
              (↑Valued.v : UniformSpace.Completion (WithVal v) →*₀ Γ₀)) ↔
        LE.le.{u_6} (α := Γ₀')
          ((Valued.v : (a : UniformSpace.Completion (WithVal w)) → Γ₀')
              ((mapEquiv h.uniformEquiv :
                    (a : UniformSpace.Completion (WithVal v)) → UniformSpace.Completion (WithVal w))
                  a :
                UniformSpace.Completion (WithVal w)) :
            Γ₀')
          (1 : Γ₀')}
have h₁ : ∀ (x : UniformSpace.Completion (WithVal v)),
  LE.le.{u_6} (α := Γ₀')
      ((Valued.v : (a : UniformSpace.Completion (WithVal w)) → Γ₀')
          ((mapEquiv h.uniformEquiv : (a : UniformSpace.Completion (WithVal v)) → UniformSpace.Completion (WithVal w))
              x :
            UniformSpace.Completion (WithVal w)) :
        Γ₀')
      (1 : Γ₀') ↔
    LE.le.{u_6} (α :=
      ValueGroup₀ (F := MonoidWithZeroHom.{u_7, u_6} (UniformSpace.Completion (WithVal w)) Γ₀')
        (↑Valued.v : UniformSpace.Completion (WithVal w) →*₀ Γ₀'))
      ((Valuation.restrict Valued.v :
            (a : UniformSpace.Completion (WithVal w)) →
              ValueGroup₀ (↑Valued.v : UniformSpace.Completion (WithVal w) →*₀ Γ₀'))
          (((mapEquiv h.uniformEquiv).toHomeomorph :
              (a : UniformSpace.Completion (WithVal v)) → UniformSpace.Completion (WithVal w))
            x) :
        ValueGroup₀ (F := MonoidWithZeroHom.{u_7, u_6} (UniformSpace.Completion (WithVal w)) Γ₀')
          (↑Valued.v : UniformSpace.Completion (WithVal w) →*₀ Γ₀'))
      (1 : ValueGroup₀ (F := Valuation.{u_7, u_6} (UniformSpace.Completion (WithVal w)) Γ₀') Valued.v)
Tactic: convert!
      (mapEquiv h.uniformEquiv).toHomeomorph.isClosed_setOf_iff
        (Valued.isClopen_closedBall _ one_ne_zero) (Valued.isClopen_closedBall _ one_ne_zero)