awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (hypothesis)
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
x : K
x_ne : x ≠ 0
⊢ ∃ (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
    Subset.{u_1} (α := Set K)
      {y : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - 0) < (↑γ : ValueGroup₀ v)}
      {k : K | LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)}
have hdef : let γ' : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ :=
  Units.mk0
    (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) x)
    sorry;
γ' =
  Units.mk0
    (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) x)
    sorry
Tactic: set γ' := Units.mk0 ((ValueGroup₀.restrict₀ _) x) (v.restrict.ne_zero_iff.mpr x_ne) with hdef
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (hypothesis)
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
x : K
x_ne : x ≠ 0
γ' : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ :=
  Units.mk0
    (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) x)
    ⋯
hdef :
  γ' =
    Units.mk0
      (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
        x)
      ⋯
y : K
hy :
  Membership.mem (γ := Set K)
    {y : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - 0) < (↑γ' : ValueGroup₀ v)} y
⊢ Membership.mem (γ := Set K) {k : K | LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)} y
have hy₁ : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
Tactic: simp only [Valuation.restrict_lt_iff_lt_embedding, hdef, sub_zero, Units.val_mk0,
      mem_setOf_eq, embedding_restrict₀] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ Continuous[hv.toTopologicalSpace, topologicalSpace] (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀))
have rw : ∀ (x : K),
  ContinuousAt.{u_1, u_2} (Y := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x
Tactic: rw [continuous_iff_continuousAt]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
⊢ ContinuousAt.{u_1, u_2} (Y := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x
have inl : ContinuousAt.{u_1, u_2} (X := K) (Y := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
  (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) 0
Tactic: rcases eq_or_ne x 0 with (rfl | h)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
inl :
  ContinuousAt.{u_1, u_2} (X := K) (Y := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) 0
⊢ ContinuousAt.{u_1, u_2} (Y := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x
have inr : ∀ (h : x ≠ 0),
  ContinuousAt.{u_1, u_2} (Y := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x
Tactic: rcases eq_or_ne x 0 with (rfl | h)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ ContinuousAt.{u_1, u_2} (X := K) (Y := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) 0
have inl : ∀ (γ₀ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)),
  γ₀ ≠ 0 → ∀ᶠ (x : K) in 𝓝 0, (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x < γ₀
Tactic: rw [ContinuousAt, map_zero, WithZeroTopology.tendsto_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
γ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)
hγ : γ ≠ 0
⊢ ∀ᶠ (x : K) in 𝓝 0, (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x < γ
have 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 | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x < γ}
Tactic: rw [Filter.Eventually, Valued.mem_nhds_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
γ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)
hγ : γ ≠ 0
⊢ ∃ (γ_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 | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x < γ}
have h : Subset.{u_1} (α := Set K)
  {x : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x < (↑(Units.mk0 γ hγ) : ValueGroup₀ v)}
  {x : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x < (↑(Units.mk0 γ hγ) : ValueGroup₀ v)}
Tactic: use Units.mk0 γ hγ
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (hypothesis)
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
h : x ≠ 0
⊢ ContinuousAt.{u_1, u_2} (Y := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x
have v_ne : Ne.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
  ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
  (0 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
Tactic: have v_ne : (v.restrict x : ValueGroup₀ hv.v) ≠ 0 := (Valuation.ne_zero_iff _).mpr h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
h : x ≠ 0
v_ne :
  Ne.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (0 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
⊢ ContinuousAt.{u_1, u_2} (Y := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x
have inr : ∀ᶠ (x_1 : K) in 𝓝 x,
  Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x_1 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
Tactic: rw [ContinuousAt, WithZeroTopology.tendsto_of_ne_zero v_ne]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
h : x ≠ 0
v_ne :
  Ne.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (0 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
⊢ ∀ᶠ (x_1 : K) in 𝓝 x,
    Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x_1 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
have inr : ∀ᶠ (x_1 : K) in 𝓝 x, Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x_1 : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
Tactic: simp_rw [v.restrict_inj]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
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) → Γ₀)
⊢ Continuous[hv.toTopologicalSpace, topologicalSpace] (⇑v : (a : K) → Γ₀)
have rw : ∀ (x : K), ContinuousAt.{u_1, u_2} (Y := Γ₀) (⇑v : (a : K) → Γ₀) x
Tactic: rw [continuous_iff_continuousAt]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
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
⊢ ContinuousAt.{u_1, u_2} (Y := Γ₀) (⇑v : (a : K) → Γ₀) x
have inl : ContinuousAt.{u_1, u_2} (X := K) (Y := Γ₀) (⇑v : (a : K) → Γ₀) 0
Tactic: rcases eq_or_ne x 0 with (rfl | h)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
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
⊢ ContinuousAt.{u_1, u_2} (Y := Γ₀) (⇑v : (a : K) → Γ₀) x
have inr : ∀ (h : x ≠ 0), ContinuousAt.{u_1, u_2} (Y := Γ₀) (⇑v : (a : K) → Γ₀) x
Tactic: rcases eq_or_ne x 0 with (rfl | h)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
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) → Γ₀)
⊢ ContinuousAt.{u_1, u_2} (X := K) (Y := Γ₀) (⇑v : (a : K) → Γ₀) 0
have inl : ∀ (γ₀ : Γ₀), γ₀ ≠ 0 → ∀ᶠ (x : K) in 𝓝 0, (v : (a : K) → Γ₀) x < γ₀
Tactic: rw [ContinuousAt, map_zero, WithZeroTopology.tendsto_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
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) in 𝓝 0, (v : (a : K) → Γ₀) x < γ
have 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 < γ}
Tactic: rw [Filter.Eventually, Valued.mem_nhds_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
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
⊢ ∃ (γ_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 < γ}
have 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 < γ}
Tactic: obtain ⟨x, hx⟩ := hsurj γ
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
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 = γ
⊢ ∃ (γ_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 < γ}
have 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)
              sorry) :
          ValueGroup₀ (F := Valuation K Γ₀) v) :
        ValueGroup₀ (F := Valuation K Γ₀) v)}
  {x : K | (v : (a : K) → Γ₀) x < γ}
Tactic: use Units.mk0 (restrict₀ hv.v x) (by simp [restrict₀_apply, hx, hγ])
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (hypothesis)
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
⊢ ContinuousAt.{u_1, u_2} (Y := Γ₀) (⇑v : (a : K) → Γ₀) x
have h0 : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)
Tactic: have h0 : hv.v x ≠ 0 := (Valuation.ne_zero_iff _).mpr h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
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 : Γ₀)
⊢ ContinuousAt.{u_1, u_2} (Y := Γ₀) (⇑v : (a : K) → Γ₀) x
have inr : ∀ᶠ (x_1 : K) in 𝓝 x, Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x_1 : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
Tactic: rw [ContinuousAt, WithZeroTopology.tendsto_of_ne_zero h0]
-- 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 Γ₀
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
have 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
Tactic: rcases Filter.inf_eq_bot_iff.mp h0 with ⟨U, U_in, M, M_in, H⟩
-- 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 Γ₀
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)ˣ),
    ∃ M ∈ F,
      ∀ x ∈ M,
        (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
          (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x
have 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
Tactic: rcases Valued.mem_nhds_zero.mp U_in with ⟨γ₀, hU⟩
-- 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 Γ₀
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
⊢ ∃ (γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
    ∃ M ∈ F,
      ∀ x ∈ M,
        (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
          (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x
have exists : ∀ x ∈ M,
  (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
    (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x
Tactic: exists γ₀, M, M_in
-- 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 Γ₀
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
⊢ (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
    (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x
have apply : ¬(Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x <
    (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v)
Tactic: apply le_of_not_gt _
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (hypothesis)
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)
⊢ False
have this : x ∈ U ∩ M
Tactic: have : x ∈ U ∩ M := ⟨hU hyp, xM⟩
-- 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 Γ₀
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
⊢ False
have rwa : ∀ (this : Membership.mem (γ := Set K) ∅ x), False
Tactic: rwa [H] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (hypothesis)
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 = ⊥
⊢ Cauchy (α := K) (map (fun (x : K) ↦ x⁻¹) F)
have this : ∃ (γ₀ : (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
-- 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 Γ₀
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
⊢ Cauchy (α := K) (map (fun (x : K) ↦ x⁻¹) F)
have 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)
Tactic: rcases this with ⟨γ₀, M₀, M₀_in, H₀⟩
Cleared hypotheses: this
-- 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 Γ₀
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
⊢ Cauchy (α := K) (map (fun (x : K) ↦ x⁻¹) F)
have 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)
Tactic: rw [Valued.cauchy_iff] at hF ⊢
Cleared hypotheses: hF, h0, γ₀, M₀, M₀_in, H₀