-- 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 Γ₀
s : Set (hat K)
⊢ Membership.mem (γ := Filter (hat K)) (𝓝 0) 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
have suffices : 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)ˣ) → Γ₀ˣ) γ) : Γ₀) : Γ₀)}
Tactic: suffices HasBasis (𝓝 (0 : hat K)) (fun _ => True)
        fun γ : (ValueGroup₀ hv.v)ˣ => { x | extensionValuation x <
          (Units.map (ValueGroup₀.embedding (f := hv.v)) γ).1 } by
      rw [this.mem_iff]
      simp only [extensionValuation_toFun, Units.coe_map, MonoidHom.coe_coe, true_and]
      have (x : hat K) (γ : (ValueGroup₀ hv.v)ˣ) : extensionValuation.restrict x <
          ((Units.map valueGroup₀_equiv_extensionValuation.toMonoidHom) γ).1 ↔
          embedding (extension x) < embedding γ.1 := by
        simp only [MulEquiv.toMonoidHom_eq_coe, Units.coe_map, MonoidHom.coe_coe]
        rw [embedding_strictMono.lt_iff_lt, Valuation.restrict_def, restrict₀_apply]
        by_cases hx0 : x = 0
        · simp only [hx0]
          rw [dif_pos (map_zero _)]
          · simp only [valueGroup₀_equiv_extensionValuation, valueGroup₀_hom_extensionValuation,
              MulEquiv.ofBijective_apply, coe_mk, ZeroHom.coe_mk]
            rw [Valuation.restrict_def, restrict₀_apply, dif_neg]
            · have hext : hv.extension 0 = 0 := by rw [extension_eq_zero_iff]
              simp [hext]
            · simp [← v.restrict.zero_iff, v.restrict_def,
                (restrict₀_surjective hv.v _).choose_spec]
        · rw [dif_neg (by simp [hx0])]
          · set y := (restrict₀_surjective hv.v γ).choose with hy_def
            set hy := (restrict₀_surjective hv.v γ).choose_spec
            simp only [extensionValuation_toFun, valueGroup₀_equiv_extensionValuation,
              valueGroup₀_hom_extensionValuation,
              MulEquiv.ofBijective_apply, coe_mk, ZeroHom.coe_mk]
            rw [Valuation.restrict_def, restrict₀_apply, ← hy_def, dif_neg]
            · simp only [extensionValuation_toFun, extension_extends, WithZero.coe_lt_coe,
                Subtype.mk_lt_mk, ← Units.val_lt_val, Units.val_mk0]
              rw [embedding_strictMono.lt_iff_lt, v.restrict_def, hy]
            · rw [extensionValuation_apply_coe, ← restrict₀_eq_zero_iff, hy]
              simp
      refine ⟨fun ⟨γ, h⟩ ↦ ?_, fun ⟨γ, h⟩ ↦ ?_⟩
      · use Units.map valueGroup₀_equiv_extensionValuation.toMonoidHom γ
        convert! h
        apply this
      · use Units.map valueGroup₀_equiv_extensionValuation.symm.toMonoidHom γ
        convert! h
        rw [← this]
        simp [Valuation.restrict_def, restrict₀_apply]