-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : Set (hat K)
this_1 :
  HasBasis.{u_1, u_2 + 1} (α := hat K) (𝓝 0) (fun (x : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ) ↦ True)
    fun (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ) ↦
    {x : hat K |
      LT.lt.{u_2} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀)
        ((↑((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ) : Γ₀) : Γ₀)}
this :
  ∀ (x : hat K) (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
    LT.lt.{u_2} (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑extensionValuation : hat K →*₀ Γ₀))
        ((Valuation.restrict extensionValuation : (a : hat K) → ValueGroup₀ (↑extensionValuation : hat K →*₀ Γ₀)) x :
          ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑extensionValuation : hat K →*₀ Γ₀))
        ((↑((Units.map (MulEquiv.toMonoidHom valueGroup₀_equiv_extensionValuation) :
                  (a : (ValueGroup₀ v)ˣ) → (ValueGroup₀ extensionValuation)ˣ)
                γ) :
            ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) :
          ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) ↔
      LT.lt (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension x) : Γ₀)
        ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)
refine_1 :
  (∃ (i : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
      {x : hat K |
          LT.lt (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension x) : Γ₀)
            ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑i : ValueGroup₀ v) : Γ₀)} ⊆
        s) →
    ∀ (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ)
      (h :
        {x : hat K |
            LT.lt (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension x) : Γ₀)
              ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)} ⊆
          s),
      ∃ (γ : (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)ˣ),
        {x : hat K |
            (Valuation.restrict extensionValuation : (a : hat K) → ValueGroup₀ (↑extensionValuation : hat K →*₀ Γ₀)) x <
              (↑γ : ValueGroup₀ extensionValuation)} ⊆
          s
refine_2 :
  (∃ (γ : (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)ˣ),
      {x : hat K |
          (Valuation.restrict extensionValuation : (a : hat K) → ValueGroup₀ (↑extensionValuation : hat K →*₀ Γ₀)) x <
            (↑γ : ValueGroup₀ extensionValuation)} ⊆
        s) →
    ∀ (γ : (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)ˣ)
      (h :
        {x : hat K |
            (Valuation.restrict extensionValuation : (a : hat K) → ValueGroup₀ (↑extensionValuation : hat K →*₀ Γ₀)) x <
              (↑γ : ValueGroup₀ extensionValuation)} ⊆
          s),
      ∃ (i : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
        {x : hat K |
            LT.lt (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension x) : Γ₀)
              ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑i : ValueGroup₀ v) : Γ₀)} ⊆
          s
⊢ (∃ (i : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
      {x : hat K |
          LT.lt (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension x) : Γ₀)
            ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑i : ValueGroup₀ v) : Γ₀)} ⊆
        s) ↔
    ∃ (γ : (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)ˣ),
      {x : hat K |
          (Valuation.restrict extensionValuation : (a : hat K) → ValueGroup₀ (↑extensionValuation : hat K →*₀ Γ₀)) x <
            (↑γ : ValueGroup₀ extensionValuation)} ⊆
        s

Tactic:
refine ⟨fun ⟨γ, h⟩ ↦ ?_, fun ⟨γ, h⟩ ↦ ?_⟩