-- Module: Mathlib.NumberTheory.LocalField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : TopologicalSpace K
inst_3 : IsNonarchimedeanLocalField K
γ : K
hγ : ¬γ = 0
this_1 : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this : IsUniformAddGroup K := ⋯
s : Set K
hs : Membership.mem (γ := Filter K) (nhds 0) s
hs' : IsCompact s
r : K
hr : r ≠ 0
hr1 :
  LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r : ValueGroupWithZero K)
    (1 : ValueGroupWithZero K)
H :
  {x : K |
      LE.le (α :=
        MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K) (↑(valuation K) : K →*₀ ValueGroupWithZero K))
        ((Valuation.restrict (valuation K) :
              (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑(valuation K) : K →*₀ ValueGroupWithZero K))
            x :
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K) (↑(valuation K) : K →*₀ ValueGroupWithZero K))
        ((Valuation.restrict (valuation K) :
              (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑(valuation K) : K →*₀ ValueGroupWithZero K))
            r :
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K)
            (↑(valuation K) : K →*₀ ValueGroupWithZero K))} ⊆
    s
x : K
h :
  LE.le (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) x : ValueGroupWithZero K)
      ((valuation K : (a : K) → ValueGroupWithZero K) γ : ValueGroupWithZero K) ↔
    HMul.hMul (β :=
        MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K) (↑Valued.v : K →*₀ ValueGroupWithZero K))
        (HDiv.hDiv (α :=
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K) (↑Valued.v : K →*₀ ValueGroupWithZero K))
          (β :=
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K) (↑Valued.v : K →*₀ ValueGroupWithZero K))
          ((Valuation.restrict Valued.v :
                (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : K →*₀ ValueGroupWithZero K))
              r :
            MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K) (↑Valued.v : K →*₀ ValueGroupWithZero K))
          ((Valuation.restrict Valued.v :
                (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : K →*₀ ValueGroupWithZero K))
              γ :
            MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K) (↑Valued.v : K →*₀ ValueGroupWithZero K)))
        ((Valuation.restrict Valued.v :
              (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : K →*₀ ValueGroupWithZero K))
            x :
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K) (↑Valued.v : K →*₀ ValueGroupWithZero K)) ≤
      (Valuation.restrict (valuation K) :
          (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑(valuation K) : K →*₀ ValueGroupWithZero K))
        r
⊢ Membership.mem (γ := Set K)
      {x : K |
        LE.le (α :=
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K) (↑(valuation K) : K →*₀ ValueGroupWithZero K))
          ((Valuation.restrict (valuation K) :
                (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑(valuation K) : K →*₀ ValueGroupWithZero K))
              x :
            MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K)
              (↑(valuation K) : K →*₀ ValueGroupWithZero K))
          ((Valuation.restrict (valuation K) :
                (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑(valuation K) : K →*₀ ValueGroupWithZero K))
              γ :
            MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K)
              (↑(valuation K) : K →*₀ ValueGroupWithZero K))}
      x ↔
    Membership.mem (γ := Set K)
      (Set.preimage (β := K) (⇑(Homeomorph.toEquiv (Homeomorph.mulLeft₀ (γ / r) ⋯)).symm : (a : K) → K)
        {x : K |
          LE.le (α :=
            MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K) (↑Valued.v : K →*₀ ValueGroupWithZero K))
            ((Valuation.restrict Valued.v :
                  (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : K →*₀ ValueGroupWithZero K))
                x :
              MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K) (↑Valued.v : K →*₀ ValueGroupWithZero K))
            ((Valuation.restrict (valuation K) :
                  (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑(valuation K) : K →*₀ ValueGroupWithZero K))
                r :
              MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K)
                (↑(valuation K) : K →*₀ ValueGroupWithZero K))})
      x

Tactic:
simp only [Set.mem_setOf_eq, Homeomorph.coe_symm_toEquiv, Homeomorph.mulLeft₀_symm_apply, inv_div,
    Set.preimage_setOf_eq, map_mul, map_div₀, Valuation.restrict_le_iff]

Premises used: Homeomorph.coe_symm_toEquiv, Valuation.restrict_le_iff, Set.mem_setOf_eq, Homeomorph.mulLeft₀_symm_apply, Set.preimage_setOf_eq, map_mul, map_div₀, inv_div