awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : ValueGroup₀ (F := Valuation R Γ₀) v
inl :
  ∀ (x : R),
    Membership.mem (γ := Set R)
        {x : R |
          LT.lt.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
            ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x :
              ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
            (0 : ValueGroup₀ (F := Valuation R Γ₀) v)}
        x →
      {x : R |
          LT.lt.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
            ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x :
              ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
            (0 : ValueGroup₀ (F := Valuation R Γ₀) v)} ∈
        𝓝 x
⊢ ∀ (x : R),
    Membership.mem (γ := Set R) {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r} x →
      {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r} ∈ 𝓝 x
have inr : ∀ (hr : r ≠ 0) (x : R),
  Membership.mem (γ := Set R) {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r} x →
    {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r} ∈ 𝓝 x
Tactic: rcases eq_or_ne r 0 with rfl | hr
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : ValueGroup₀ (F := Valuation R Γ₀) v
hr : r ≠ 0
x : R
hx : Membership.mem (γ := Set R) {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r} x
⊢ {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r} ∈ 𝓝 x
have inr : ∃ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
  Subset.{u} (α := Set R)
    {y : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)}
    {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r}
Tactic: rw [mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : ValueGroup₀ (F := Valuation R Γ₀) v
⊢ IsClosed[_i.toTopologicalSpace] {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r}
have inl : IsClosed[_i.toTopologicalSpace]
  {x : R |
    LT.lt.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (0 : ValueGroup₀ (F := Valuation R Γ₀) v)}
Tactic: rcases eq_or_ne r 0 with rfl | hr
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : ValueGroup₀ (F := Valuation R Γ₀) v
inl :
  IsClosed[_i.toTopologicalSpace]
    {x : R |
      LT.lt.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        (0 : ValueGroup₀ (F := Valuation R Γ₀) v)}
⊢ IsClosed[_i.toTopologicalSpace] {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r}
have inr : ∀ (hr : r ≠ 0),
  IsClosed[_i.toTopologicalSpace] {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r}
Tactic: rcases eq_or_ne r 0 with rfl | hr
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : ValueGroup₀ (F := Valuation R Γ₀) v
hr : r ≠ 0
⊢ IsOpen[_i.toTopologicalSpace] {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r}
have rw : ∀ (x : R),
  Membership.mem (γ := Set R) {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} x →
    {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} ∈ 𝓝 x
Tactic: rw [isOpen_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : ValueGroup₀ (F := Valuation R Γ₀) v
hr : r ≠ 0
x : R
hx : Membership.mem (γ := Set R) {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} x
⊢ {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} ∈ 𝓝 x
have rw : ∃ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
  Subset.{u} (α := Set R)
    {y : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)}
    {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r}
Tactic: rw [mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : ValueGroup₀ (F := Valuation R Γ₀) v
⊢ IsClosed[_i.toTopologicalSpace] {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r}
have rw : ∀ (x : R),
  Membership.mem (γ := Set R) {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r}ᶜ x →
    {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r}ᶜ ∈ 𝓝 x
Tactic: rw [← isOpen_compl_iff, isOpen_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (hypothesis)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : ValueGroup₀ (F := Valuation R Γ₀) v
x : R
hx : Membership.mem (γ := Set R) {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r}ᶜ x
⊢ {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r}ᶜ ∈ 𝓝 x
have hx₁ : r < (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x
Tactic: simp only [mem_compl_iff, mem_setOf_eq, not_le] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : ValueGroup₀ (F := Valuation R Γ₀) v
x : R
hx : r < (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x
⊢ {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r}ᶜ ∈ 𝓝 x
have rw : ∃ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
  Subset.{u} (α := Set R)
    {y : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)}
    {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r}ᶜ
Tactic: rw [mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (hypothesis)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : ValueGroup₀ (F := Valuation R Γ₀) v
x : R
hx : r < (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x
⊢ ∃ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
    Subset.{u} (α := Set R)
      {y : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)}
      {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r}ᶜ
have hx' : Ne.{v + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
  ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
  (0 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
Tactic: have hx' : v.restrict x ≠ 0 := ne_of_gt <| lt_of_le_of_lt zero_le' <| hx
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : ValueGroup₀ (F := Valuation R Γ₀) v
hr : r ≠ 0
⊢ Eq.{u + 1} (α := Set R) {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x = r}
    ({x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} \
      {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r})
have h : ∀ (x : R),
  Membership.mem (γ := Set R) {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x = r} x ↔
    Membership.mem (γ := Set R)
      ({x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} \
        {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r})
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (hypothesis)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : ValueGroup₀ (F := Valuation R Γ₀) v
hr : r ≠ 0
⊢ IsClopen.{u} (X := R) {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x = r}
have h : Eq.{u + 1} (α := Set R) {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x = r}
  ({x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} \
    {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r})
Tactic: have h : {x : R | v.restrict x = r} = {x | v.restrict x ≤ r} \ {x | v.restrict x < r} := by
    ext x
    simp [← le_antisymm_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : ValueGroup₀ (F := Valuation R Γ₀) v
hr : r ≠ 0
h :
  Eq.{u + 1} (α := Set R) {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x = r}
    ({x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} \
      {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r})
⊢ IsClopen.{u} (X := R) {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x = r}
have rw : IsClopen.{u} (X := R)
  ({x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} \
    {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r})
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : ValueGroup₀ (F := Valuation R Γ₀) v
⊢ IsClosed[_i.toTopologicalSpace] {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x = r}
have inl : IsClosed[_i.toTopologicalSpace]
  {x : R |
    Eq.{v + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (0 : ValueGroup₀ (F := Valuation R Γ₀) v)}
Tactic: rcases eq_or_ne r 0 with rfl | hr
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : ValueGroup₀ (F := Valuation R Γ₀) v
inl :
  IsClosed[_i.toTopologicalSpace]
    {x : R |
      Eq.{v + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        (0 : ValueGroup₀ (F := Valuation R Γ₀) v)}
⊢ IsClosed[_i.toTopologicalSpace] {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x = r}
have inr : ∀ (hr : r ≠ 0),
  IsClosed[_i.toTopologicalSpace] {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x = r}
Tactic: rcases eq_or_ne r 0 with rfl | hr
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ IsOpen[_i.toTopologicalSpace] (↑(integer v) : Set R)
have simp : IsOpen[_i.toTopologicalSpace]
  {x : R |
    LE.le.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (1 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))}
Tactic: simp only [integer, Subring.coe_set_mk, Subsemiring.coe_set_mk, Submonoid.coe_set_mk,
    Subsemigroup.coe_set_mk, ← v.restrict_le_one_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ IsClosed[_i.toTopologicalSpace] (↑(integer v) : Set R)
have simp : IsClosed[_i.toTopologicalSpace]
  {x : R |
    LE.le.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (1 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))}
Tactic: simp only [integer, Subring.coe_set_mk, Subsemiring.coe_set_mk, Submonoid.coe_set_mk,
    Subsemigroup.coe_set_mk, ← v.restrict_le_one_iff]
-- 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 Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h :
  (v : (a : K) → Γ₀) (x - y) <
    min ((↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
⊢ (v : (a : K) → Γ₀) (x⁻¹ - y⁻¹) < (↑γ : Γ₀)
have hyp1 : (v : (a : K) → Γ₀) (x - y) <
  (↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
Tactic: have hyp1 : v (x - y) < γ * (v y * v y) := lt_of_lt_of_le h (min_le_left _ _)
-- 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 Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h :
  (v : (a : K) → Γ₀) (x - y) <
    min ((↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hyp1 :
  (v : (a : K) → Γ₀) (x - y) <
    (↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
⊢ (v : (a : K) → Γ₀) (x⁻¹ - y⁻¹) < (↑γ : Γ₀)
have hyp1' : HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
    (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ <
  (↑γ : Γ₀)
Tactic: have hyp1' : v (x - y) * (v y * v y)⁻¹ < γ := mul_inv_lt_of_lt_mul₀ hyp1
-- 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 Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h :
  (v : (a : K) → Γ₀) (x - y) <
    min ((↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hyp1 :
  (v : (a : K) → Γ₀) (x - y) <
    (↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
hyp1' :
  HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ <
    (↑γ : Γ₀)
⊢ (v : (a : K) → Γ₀) (x⁻¹ - y⁻¹) < (↑γ : Γ₀)
have hyp2 : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
Tactic: have hyp2 : v (x - y) < v y := lt_of_lt_of_le h (min_le_right _ _)
-- 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 Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h :
  (v : (a : K) → Γ₀) (x - y) <
    min ((↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hyp1 :
  (v : (a : K) → Γ₀) (x - y) <
    (↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
hyp1' :
  HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ <
    (↑γ : Γ₀)
hyp2 : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
⊢ (v : (a : K) → Γ₀) (x⁻¹ - y⁻¹) < (↑γ : Γ₀)
have key : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
Tactic: have key : v x = v y := Valuation.map_eq_of_sub_lt v hyp2
-- 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 Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h_1 :
  (v : (a : K) → Γ₀) (x - y) <
    min ((↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hyp1 :
  (v : (a : K) → Γ₀) (x - y) <
    (↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
hyp1' :
  HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ <
    (↑γ : Γ₀)
hyp2 : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
key : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
h : x = 0
⊢ False
have apply : y = 0
Tactic: apply y_ne
-- 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 Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h_1 :
  (v : (a : K) → Γ₀) (x - y) <
    min ((↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hyp1 :
  (v : (a : K) → Γ₀) (x - y) <
    (↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
hyp1' :
  HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ <
    (↑γ : Γ₀)
hyp2 : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
key : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
h : x = 0
⊢ y = 0
have key₁ : Eq.{u_2 + 1} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
Tactic: rw [h, v.map_zero] at key
Cleared hypotheses: key, 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 Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h :
  (v : (a : K) → Γ₀) (x - y) <
    min ((↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hyp1 :
  (v : (a : K) → Γ₀) (x - y) <
    (↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
hyp1' :
  HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ <
    (↑γ : Γ₀)
hyp2 : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
key : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
⊢ (v : (a : K) → Γ₀) (x⁻¹ - y⁻¹) < (↑γ : Γ₀)
have x_ne : x ≠ 0
Tactic: have x_ne : x ≠ 0 := by
    intro h
    apply y_ne
    rw [h, v.map_zero] at key
    exact v.zero_iff.1 key.symm
-- 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 Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h :
  (v : (a : K) → Γ₀) (x - y) <
    min ((↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hyp1 :
  (v : (a : K) → Γ₀) (x - y) <
    (↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
hyp1' :
  HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ <
    (↑γ : Γ₀)
hyp2 : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
key : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
x_ne : x ≠ 0
⊢ x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
have rw : x⁻¹ - y⁻¹ = (x⁻¹ * y - x⁻¹ * x) * y⁻¹
Tactic: rw [mul_sub_left_distrib, sub_mul, mul_assoc, show y * y⁻¹ = 1 from mul_inv_cancel₀ y_ne,
      show x⁻¹ * x = 1 from inv_mul_cancel₀ x_ne, mul_one, one_mul]
-- 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 Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h :
  (v : (a : K) → Γ₀) (x - y) <
    min ((↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hyp1 :
  (v : (a : K) → Γ₀) (x - y) <
    (↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
hyp1' :
  HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ <
    (↑γ : Γ₀)
hyp2 : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
key : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
x_ne : x ≠ 0
rw : x⁻¹ - y⁻¹ = (x⁻¹ * y - x⁻¹ * x) * y⁻¹
⊢ x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
have rw₁ : x⁻¹ - y⁻¹ = x⁻¹ * y * y⁻¹ - x⁻¹ * x * y⁻¹
Tactic: rw [mul_sub_left_distrib, sub_mul, mul_assoc, show y * y⁻¹ = 1 from mul_inv_cancel₀ y_ne,
      show x⁻¹ * x = 1 from inv_mul_cancel₀ x_ne, mul_one, one_mul]
-- 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 Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h :
  (v : (a : K) → Γ₀) (x - y) <
    min ((↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hyp1 :
  (v : (a : K) → Γ₀) (x - y) <
    (↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
hyp1' :
  HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ <
    (↑γ : Γ₀)
hyp2 : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
key : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
x_ne : x ≠ 0
rw : x⁻¹ - y⁻¹ = (x⁻¹ * y - x⁻¹ * x) * y⁻¹
rw₁ : x⁻¹ - y⁻¹ = x⁻¹ * y * y⁻¹ - x⁻¹ * x * y⁻¹
⊢ x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
have rw₂ : x⁻¹ - y⁻¹ = x⁻¹ * (y * y⁻¹) - x⁻¹ * x * y⁻¹
Tactic: rw [mul_sub_left_distrib, sub_mul, mul_assoc, show y * y⁻¹ = 1 from mul_inv_cancel₀ y_ne,
      show x⁻¹ * x = 1 from inv_mul_cancel₀ x_ne, mul_one, one_mul]