awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
hsurj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := K) (β := Γ₀) (⇑v : (a : K) → Γ₀)
x : K
inl : ContinuousAt.{u_1, u_2} (X := K) (Y := Γ₀) (⇑v : (a : K) → Γ₀) 0
inr : ∀ (h : x ≠ 0), ContinuousAt.{u_1, u_2} (Y := Γ₀) (⇑v : (a : K) → Γ₀) x
⊢ ContinuousAt.{u_1, u_2} (Y := Γ₀) (⇑v : (a : K) → Γ₀) x

Tactic:
rcases eq_or_ne x 0 with (rfl | h)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
hsurj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := K) (β := Γ₀) (⇑v : (a : K) → Γ₀)
inl : ∀ (γ₀ : Γ₀), γ₀ ≠ 0 → ∀ᶠ (x : K) in 𝓝 0, (v : (a : K) → Γ₀) x < γ₀
⊢ ContinuousAt.{u_1, u_2} (X := K) (Y := Γ₀) (⇑v : (a : K) → Γ₀) 0

Tactic:
rw [ContinuousAt, map_zero, WithZeroTopology.tendsto_zero]

Premises used: ContinuousAt, map_zero, WithZeroTopology.tendsto_zero
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
hsurj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := K) (β := Γ₀) (⇑v : (a : K) → Γ₀)
γ : Γ₀
hγ : γ ≠ 0
inl :
  ∃ (γ_1 : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
    Subset.{u_1} (α := Set K)
      {x : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x < (↑γ_1 : ValueGroup₀ v)}
      {x : K | (v : (a : K) → Γ₀) x < γ}
⊢ ∀ᶠ (x : K) in 𝓝 0, (v : (a : K) → Γ₀) x < γ

Tactic:
rw [Filter.Eventually, Valued.mem_nhds_zero]

Premises used: Filter.Eventually, Valued.mem_nhds_zero
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
hsurj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := K) (β := Γ₀) (⇑v : (a : K) → Γ₀)
γ : Γ₀
hγ : γ ≠ 0
inl :
  ∀ (x : K) (hx : (v : (a : K) → Γ₀) x = γ),
    ∃ (γ_1 : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
      Subset.{u_1} (α := Set K)
        {x : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x < (↑γ_1 : ValueGroup₀ v)}
        {x : K | (v : (a : K) → Γ₀) x < γ}
⊢ ∃ (γ_1 : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
    Subset.{u_1} (α := Set K)
      {x : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x < (↑γ_1 : ValueGroup₀ v)}
      {x : K | (v : (a : K) → Γ₀) x < γ}

Tactic:
obtain ⟨x, hx⟩ := hsurj γ
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
hsurj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := K) (β := Γ₀) (⇑v : (a : K) → Γ₀)
γ : Γ₀
hγ : γ ≠ 0
x : K
hx : (v : (a : K) → Γ₀) x = γ
⊢ Ne.{u_2 + 1} (α := ValueGroup₀ (F := Valuation K Γ₀) v)
    (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
        x :
      ValueGroup₀ (F := Valuation K Γ₀) v)
    (0 : ValueGroup₀ (F := Valuation K Γ₀) v)

Tactic:
simp [restrict₀_apply, hx, hγ]

Premises used: MonoidWithZeroHom.ValueGroup₀.restrict₀_apply
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
hsurj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := K) (β := Γ₀) (⇑v : (a : K) → Γ₀)
γ : Γ₀
hγ : γ ≠ 0
x : K
hx : (v : (a : K) → Γ₀) x = γ
h :
  Subset.{u_1} (α := Set K)
    {x_1 : K |
      LT.lt.{u_2} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
        ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x_1 :
          ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
        ((↑(Units.mk0
                (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) :
                    (a : K) → ValueGroup₀ v)
                  x)
                ⋯) :
            ValueGroup₀ (F := Valuation K Γ₀) v) :
          ValueGroup₀ (F := Valuation K Γ₀) v)}
    {x : K | (v : (a : K) → Γ₀) x < γ}
⊢ ∃ (γ_1 : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
    Subset.{u_1} (α := Set K)
      {x : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x < (↑γ_1 : ValueGroup₀ v)}
      {x : K | (v : (a : K) → Γ₀) x < γ}

Tactic:
use Units.mk0 (restrict₀ hv.v x) (by simp [restrict₀_apply, hx, hγ])

Premises used: Valued.v, Units.mk0, MonoidWithZeroHom.ValueGroup₀.restrict₀, DFunLike.coe
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
hsurj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := K) (β := Γ₀) (⇑v : (a : K) → Γ₀)
γ : Γ₀
hγ : γ ≠ 0
x : K
hx : (v : (a : K) → Γ₀) x = γ
⊢ Subset.{u_1} (α := Set K)
    {x_1 : K |
      LT.lt.{u_2} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
        ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x_1 :
          ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
        ((↑(Units.mk0
                (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) :
                    (a : K) → ValueGroup₀ v)
                  x)
                ⋯) :
            ValueGroup₀ (F := Valuation K Γ₀) v) :
          ValueGroup₀ (F := Valuation K Γ₀) v)}
    {x : K | (v : (a : K) → Γ₀) x < γ}

Tactic:
simp only [Units.val_mk0, setOf_subset_setOf, ← v.restrict_def, Valuation.restrict_lt_iff, hx,
      imp_self, implies_true]

Premises used: Valued.v, Valuation.restrict_def, imp_self, Set.setOf_subset_setOf, implies_true, Valuation.restrict_lt_iff, Units.val_mk0
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
hsurj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := K) (β := Γ₀) (⇑v : (a : K) → Γ₀)
x : K
h : x ≠ 0
⊢ Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)

Tactic:
have h0 : hv.v x ≠ 0 := (Valuation.ne_zero_iff _).mpr h
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
hsurj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := K) (β := Γ₀) (⇑v : (a : K) → Γ₀)
x : K
h : x ≠ 0
h0 : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)
inr : ∀ᶠ (x_1 : K) in 𝓝 x, Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x_1 : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
⊢ ContinuousAt.{u_1, u_2} (Y := Γ₀) (⇑v : (a : K) → Γ₀) x

Tactic:
rw [ContinuousAt, WithZeroTopology.tendsto_of_ne_zero h0]

Premises used: WithZeroTopology.tendsto_of_ne_zero, ContinuousAt
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
hsurj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := K) (β := Γ₀) (⇑v : (a : K) → Γ₀)
x : K
h : x ≠ 0
h0 : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)
⊢ Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)

Tactic:
simpa using h0
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
hsurj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := K) (β := Γ₀) (⇑v : (a : K) → Γ₀)
x : K
h : x ≠ 0
h0 : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)
⊢ ∀ᶠ (x_1 : K) in 𝓝 x, Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x_1 : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)

Tactic:
exact Valued.locally_const (by simpa using h0)

Premises used: Valued.locally_const
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
F : Filter K
hF : Cauchy F
h0 : 𝓝 0 ⊓ F = ⊥
rcases :
  ∀ (U : Set K) (U_in : Membership.mem (γ := Filter K) (𝓝 0) U) (M : Set K) (M_in : M ∈ F) (H : U ∩ M = ∅),
    ∃ (γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
      ∃ M ∈ F,
        ∀ x ∈ M,
          (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
            (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x
⊢ ∃ (γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
    ∃ M ∈ F,
      ∀ x ∈ M,
        (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
          (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x

Tactic:
rcases Filter.inf_eq_bot_iff.mp h0 with ⟨U, U_in, M, M_in, H⟩

Premises used: Iff.mp, Filter.inf_eq_bot_iff
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
F : Filter K
hF : Cauchy F
h0 : 𝓝 0 ⊓ F = ⊥
U : Set K
U_in : Membership.mem (γ := Filter K) (𝓝 0) U
M : Set K
M_in : M ∈ F
H : U ∩ M = ∅
rcases :
  ∀ (γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ)
    (hU :
      {x : K |
          (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x <
            (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v)} ⊆
        U),
    ∃ (γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
      ∃ M ∈ F,
        ∀ x ∈ M,
          (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
            (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x
⊢ ∃ (γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
    ∃ M ∈ F,
      ∀ x ∈ M,
        (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
          (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x

Tactic:
rcases Valued.mem_nhds_zero.mp U_in with ⟨γ₀, hU⟩

Premises used: Valued.mem_nhds_zero, Iff.mp
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
F : Filter K
hF : Cauchy F
h0 : 𝓝 0 ⊓ F = ⊥
U : Set K
U_in : Membership.mem (γ := Filter K) (𝓝 0) U
M : Set K
M_in : M ∈ F
H : U ∩ M = ∅
γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
hU :
  {x : K |
      (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x <
        (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v)} ⊆
    U
exists :
  ∀ x ∈ M,
    (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
      (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x
⊢ ∃ (γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
    ∃ M ∈ F,
      ∀ x ∈ M,
        (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
          (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x

Tactic:
exists γ₀, M, M_in
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
F : Filter K
hF : Cauchy F
h0 : 𝓝 0 ⊓ F = ⊥
U : Set K
U_in : Membership.mem (γ := Filter K) (𝓝 0) U
M : Set K
M_in : M ∈ F
H : U ∩ M = ∅
γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
hU :
  {x : K |
      (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x <
        (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v)} ⊆
    U
x : K
xM : x ∈ M
apply :
  ¬(Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x <
      (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v)
⊢ (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
    (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x

Tactic:
apply le_of_not_gt _

Premises used: le_of_not_gt
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
F : Filter K
hF : Cauchy F
h0 : 𝓝 0 ⊓ F = ⊥
U : Set K
U_in : Membership.mem (γ := Filter K) (𝓝 0) U
M : Set K
M_in : M ∈ F
H : U ∩ M = ∅
γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
hU :
  {x : K |
      (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x <
        (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v)} ⊆
    U
x : K
xM : x ∈ M
hyp :
  (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x <
    (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v)
⊢ x ∈ U ∩ M

Tactic:
have : x ∈ U ∩ M := ⟨hU hyp, xM⟩
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
F : Filter K
hF : Cauchy F
h0 : 𝓝 0 ⊓ F = ⊥
U : Set K
U_in : Membership.mem (γ := Filter K) (𝓝 0) U
M : Set K
M_in : M ∈ F
H : U ∩ M = ∅
γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
hU :
  {x : K |
      (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x <
        (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v)} ⊆
    U
x : K
xM : x ∈ M
hyp :
  (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x <
    (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v)
this : x ∈ U ∩ M
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : Membership.mem (γ := Set K) ∅ x), False
⊢ False

Tactic:
rwa [H] at this
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
F : Filter K
hF : Cauchy F
h0 : 𝓝 0 ⊓ F = ⊥
⊢ ∃ (γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
    ∃ M ∈ F,
      ∀ x ∈ M,
        (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
          (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x

Tactic:
have : ∃ γ₀ : (MonoidWithZeroHom.ValueGroup₀ hv.v)ˣ, ∃ M ∈ F,
          ∀ x ∈ M, (γ₀.1) ≤ v.restrict x := by
        rcases Filter.inf_eq_bot_iff.mp h0 with ⟨U, U_in, M, M_in, H⟩
        rcases Valued.mem_nhds_zero.mp U_in with ⟨γ₀, hU⟩
        exists γ₀, M, M_in
        intro x xM
        apply le_of_not_gt _
        intro hyp
        have : x ∈ U ∩ M := ⟨hU hyp, xM⟩
        rwa [H] at this
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
F : Filter K
hF : Cauchy F
h0 : 𝓝 0 ⊓ F = ⊥
this :
  ∃ (γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
    ∃ M ∈ F,
      ∀ x ∈ M,
        (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
          (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x
rcases :
  ∀ (γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ) (M₀ : Set K) (M₀_in : M₀ ∈ F)
    (H₀ :
      ∀ x ∈ M₀,
        (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
          (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x),
    Cauchy (α := K) (map (fun (x : K) ↦ x⁻¹) F)
⊢ Cauchy (α := K) (map (fun (x : K) ↦ x⁻¹) F)

Tactic:
rcases this with ⟨γ₀, M₀, M₀_in, H₀⟩
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
F : Filter K
hF : Cauchy F
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
H₀ :
  ∀ x ∈ M₀,
    (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
      (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x
rw :
  ∀
    (hF :
      F.NeBot ∧
        ∀ (γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
          ∃ M ∈ F,
            ∀ x ∈ M,
              ∀ y ∈ M,
                (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
                  (↑γ : MonoidWithZeroHom.ValueGroup₀ v))
    (h0 : 𝓝 0 ⊓ F = ⊥) (γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ) (M₀ : Set K) (M₀_in : M₀ ∈ F)
    (H₀ :
      ∀ x ∈ M₀,
        (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
          (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x),
    NeBot (α := K) (map (fun (x : K) ↦ x⁻¹) F) ∧
      ∀ (γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
        ∃ (M : Set K),
          Membership.mem (γ := Filter K) (map (fun (x : K) ↦ x⁻¹) F) M ∧
            ∀ x ∈ M,
              ∀ y ∈ M,
                (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
                  (↑γ : MonoidWithZeroHom.ValueGroup₀ v)
⊢ Cauchy (α := K) (map (fun (x : K) ↦ x⁻¹) F)

Tactic:
rw [Valued.cauchy_iff] at hF ⊢

Premises used: Valued.cauchy_iff
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
F : Filter K
hF :
  F.NeBot ∧
    ∀ (γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
      ∃ M ∈ F,
        ∀ x ∈ M,
          ∀ y ∈ M,
            (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
              (↑γ : MonoidWithZeroHom.ValueGroup₀ v)
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
H₀ :
  ∀ x ∈ M₀,
    (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
      (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x
⊢ NeBot (α := K) (map (fun (x : K) ↦ x⁻¹) F) ∧
    ∀ (γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
      ∃ (M : Set K),
        Membership.mem (γ := Filter K) (map (fun (x : K) ↦ x⁻¹) F) M ∧
          ∀ x ∈ M,
            ∀ y ∈ M,
              (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
                (↑γ : MonoidWithZeroHom.ValueGroup₀ v)

Tactic:
⟨hF.1.map _, ?_⟩

Premises used: Filter.NeBot.map, And.left, And.intro
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
F : Filter K
hF :
  F.NeBot ∧
    ∀ (γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
      ∃ M ∈ F,
        ∀ x ∈ M,
          ∀ y ∈ M,
            (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
              (↑γ : MonoidWithZeroHom.ValueGroup₀ v)
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
H₀ :
  ∀ x ∈ M₀,
    (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
      (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x
refine :
  ∀ (γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
    ∃ (M : Set K),
      Membership.mem (γ := Filter K) (map (fun (x : K) ↦ x⁻¹) F) M ∧
        ∀ x ∈ M,
          ∀ y ∈ M,
            (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
              (↑γ : MonoidWithZeroHom.ValueGroup₀ v)
⊢ NeBot (α := K) (map (fun (x : K) ↦ x⁻¹) F) ∧
    ∀ (γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
      ∃ (M : Set K),
        Membership.mem (γ := Filter K) (map (fun (x : K) ↦ x⁻¹) F) M ∧
          ∀ x ∈ M,
            ∀ y ∈ M,
              (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
                (↑γ : MonoidWithZeroHom.ValueGroup₀ v)

Tactic:
refine ⟨hF.1.map _, ?_⟩
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
F : Filter K
hF :
  F.NeBot ∧
    ∀ (γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
      ∃ M ∈ F,
        ∀ x ∈ M,
          ∀ y ∈ M,
            (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
              (↑γ : MonoidWithZeroHom.ValueGroup₀ v)
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
H₀ :
  ∀ x ∈ M₀,
    (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
      (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x
⊢ ∀ (γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
    ∃ M ∈ F,
      ∀ x ∈ M,
        ∀ y ∈ M,
          (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
            (↑γ : MonoidWithZeroHom.ValueGroup₀ v)

Tactic:
replace hF := hF.2
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
H₀ :
  ∀ x ∈ M₀,
    (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
      (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x
hF :
  ∀ (γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
    ∃ M ∈ F,
      ∀ x ∈ M,
        ∀ y ∈ M,
          (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
            (↑γ : MonoidWithZeroHom.ValueGroup₀ v)
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
rcases :
  ∀ (M₁ : Set K) (M₁_in : M₁ ∈ F)
    (H₁ :
      ∀ x ∈ M₁,
        ∀ y ∈ M₁,
          (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
            (↑(min (γ * γ₀ * γ₀) γ₀) : MonoidWithZeroHom.ValueGroup₀ v)),
    ∃ (M : Set K),
      Membership.mem (γ := Filter K) (map (fun (x : K) ↦ x⁻¹) F) M ∧
        ∀ x ∈ M,
          ∀ y ∈ M,
            (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
              (↑γ : MonoidWithZeroHom.ValueGroup₀ v)
⊢ ∃ (M : Set K),
    Membership.mem (γ := Filter K) (map (fun (x : K) ↦ x⁻¹) F) M ∧
      ∀ x ∈ M,
        ∀ y ∈ M,
          (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
            (↑γ : MonoidWithZeroHom.ValueGroup₀ v)

Tactic:
rcases hF (min (γ * γ₀ * γ₀) γ₀) with ⟨M₁, M₁_in, H₁⟩

Premises used: HMul.hMul, Min.min
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
H₀ :
  ∀ x ∈ M₀,
    (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
      (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
H₁ :
  ∀ x ∈ M₁,
    ∀ y ∈ M₁,
      (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
        (↑(min (γ * γ₀ * γ₀) γ₀) : MonoidWithZeroHom.ValueGroup₀ v)
h :
  Membership.mem (γ := Filter K) (map (fun (x : K) ↦ x⁻¹) F) ((fun (x : K) ↦ x⁻¹) '' (M₀ ∩ M₁)) ∧
    ∀ (x : K),
      Membership.mem (γ := Set K) ((fun (x : K) ↦ x⁻¹) '' (M₀ ∩ M₁)) x →
        ∀ (y : K),
          Membership.mem (γ := Set K) ((fun (x : K) ↦ x⁻¹) '' (M₀ ∩ M₁)) y →
            (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
              (↑γ : MonoidWithZeroHom.ValueGroup₀ v)
⊢ ∃ (M : Set K),
    Membership.mem (γ := Filter K) (map (fun (x : K) ↦ x⁻¹) F) M ∧
      ∀ x ∈ M,
        ∀ y ∈ M,
          (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
            (↑γ : MonoidWithZeroHom.ValueGroup₀ v)

Tactic:
use (fun x : K => x⁻¹) '' (M₀ ∩ M₁)

Premises used: Inter.inter, Inv.inv