-- Module: Mathlib.Topology.Algebra.Valued.WithVal
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) →*₀ Γ₀))
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)
⊢ 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 : Γ₀')}

Tactic:
convert!
      (mapEquiv h.uniformEquiv).toHomeomorph.isClosed_setOf_iff
        (Valued.isClopen_closedBall _ one_ne_zero) (Valued.isClopen_closedBall _ one_ne_zero)

Premises used: Valuation.IsEquiv.uniformEquiv, UniformSpace.Completion.mapEquiv, UniformEquiv.toHomeomorph, Homeomorph.isClosed_setOf_iff, one_ne_zero, Valued.isClopen_closedBall