awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 Γ₀
γ : Γ₀ˣ
x : hat K
γ₀' : ValueGroup₀ (F := Valuation K Γ₀) v := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := (extensionValuation : (a : hat K) → Γ₀) x
hγ₀_def : γ₀ = (extensionValuation : (a : hat K) → Γ₀) x
heq : γ₀ = (embedding : (a : ValueGroup₀ v) → Γ₀) γ₀'
h : γ₀ ≠ 0
h' : γ₀' ≠ 0
hγ₀ : extension ⁻¹' {γ₀'} ∈ 𝓝 x
⊢ Membership.mem (γ := Set (hat K)) (closure (Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)})) x ↔
    γ₀ < (↑γ : Γ₀)
have h₁ : (∀ t ∈ 𝓝 x, ∃ (y : (↑(Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)}) : Type u_1)), (↑y : hat K) ∈ t) ↔
  γ₀ < (↑γ : Γ₀)
Tactic: rw [mem_closure_iff_nhds']
-- 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 Γ₀
γ : Γ₀ˣ
x : hat K
γ₀' : ValueGroup₀ (F := Valuation K Γ₀) v := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := (extensionValuation : (a : hat K) → Γ₀) x
hγ₀_def : γ₀ = (extensionValuation : (a : hat K) → Γ₀) x
heq : γ₀ = (embedding : (a : ValueGroup₀ v) → Γ₀) γ₀'
h : γ₀ ≠ 0
h' : γ₀' ≠ 0
hγ₀ : extension ⁻¹' {γ₀'} ∈ 𝓝 x
⊢ (∀ t ∈ 𝓝 x, ∃ (y : (↑(Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)}) : Type u_1)), (↑y : hat K) ∈ t) ↔
    γ₀ < (↑γ : Γ₀)
have h₁ : ∀
  (hx :
    ∀ t ∈ 𝓝 x, ∃ (y : (↑(Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)}) : Type u_1)), (↑y : hat K) ∈ t),
  γ₀ < (↑γ : Γ₀)
Tactic: refine ⟨fun hx => ?_, fun hx s hs => ?_⟩
-- 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 Γ₀
γ : Γ₀ˣ
x : hat K
γ₀' : ValueGroup₀ (F := Valuation K Γ₀) v := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := (extensionValuation : (a : hat K) → Γ₀) x
hγ₀_def : γ₀ = (extensionValuation : (a : hat K) → Γ₀) x
heq : γ₀ = (embedding : (a : ValueGroup₀ v) → Γ₀) γ₀'
h : γ₀ ≠ 0
h' : γ₀' ≠ 0
hγ₀ : extension ⁻¹' {γ₀'} ∈ 𝓝 x
h₁ :
  ∀
    (hx :
      ∀ t ∈ 𝓝 x,
        ∃ (y : (↑(Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)}) : Type u_1)), (↑y : hat K) ∈ t),
    γ₀ < (↑γ : Γ₀)
⊢ (∀ t ∈ 𝓝 x, ∃ (y : (↑(Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)}) : Type u_1)), (↑y : hat K) ∈ t) ↔
    γ₀ < (↑γ : Γ₀)
have h₂ : ∀ (hx : γ₀ < (↑γ : Γ₀)) (s : Set (hat K)) (hs : s ∈ 𝓝 x),
  ∃ (y : (↑(Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)}) : Type u_1)), (↑y : hat K) ∈ s
Tactic: refine ⟨fun hx => ?_, fun hx s hs => ?_⟩
-- 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 Γ₀
γ : Γ₀ˣ
x : hat K
γ₀' : ValueGroup₀ (F := Valuation K Γ₀) v := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := (extensionValuation : (a : hat K) → Γ₀) x
hγ₀_def : γ₀ = (extensionValuation : (a : hat K) → Γ₀) x
heq : γ₀ = (embedding : (a : ValueGroup₀ v) → Γ₀) γ₀'
h : γ₀ ≠ 0
h' : γ₀' ≠ 0
hγ₀ : extension ⁻¹' {γ₀'} ∈ 𝓝 x
hx : ∀ t ∈ 𝓝 x, ∃ (y : (↑(Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)}) : Type u_1)), (↑y : hat K) ∈ t
⊢ γ₀ < (↑γ : Γ₀)
have h₁ : ∀ (y : K) (hy₁ : (v : (a : K) → Γ₀) y < (↑γ : Γ₀))
  (hy₂ :
    Membership.mem (γ := Set (hat K)) (extension ⁻¹' {γ₀'})
      (↑(Subtype.mk (p := fun (x : hat K) ↦
            Membership.mem (γ := Set (hat K)) (Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)}) x)
            (↑y : hat K) sorry) :
        hat K)),
  γ₀ < (↑γ : Γ₀)
Tactic: obtain ⟨⟨-, y, hy₁ : v y < (γ : Γ₀), rfl⟩, hy₂⟩ := hx _ hγ₀
-- 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 Γ₀
γ : Γ₀ˣ
x : hat K
γ₀' : ValueGroup₀ (F := Valuation K Γ₀) v := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := (extensionValuation : (a : hat K) → Γ₀) x
hγ₀_def : γ₀ = (extensionValuation : (a : hat K) → Γ₀) x
heq : γ₀ = (embedding : (a : ValueGroup₀ v) → Γ₀) γ₀'
h : γ₀ ≠ 0
h' : γ₀' ≠ 0
hγ₀ : extension ⁻¹' {γ₀'} ∈ 𝓝 x
hx : ∀ t ∈ 𝓝 x, ∃ (y : (↑(Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)}) : Type u_1)), (↑y : hat K) ∈ t
y : K
hy₁ : (v : (a : K) → Γ₀) y < (↑γ : Γ₀)
hy₂ :
  Membership.mem (γ := Set (hat K)) (extension ⁻¹' {γ₀'})
    (↑(Subtype.mk (p := fun (x : hat K) ↦
          Membership.mem (γ := Set (hat K)) (Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)}) x)
          (↑y : hat K) ⋯) :
      hat K)
⊢ (v : (a : K) → Γ₀) y = γ₀
have hy₃ : ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) y = γ₀'
Tactic: simp only [mem_preimage, extension_extends, mem_singleton_iff, v.restrict_def] at hy₂
Cleared hypotheses: hy₂
-- 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 Γ₀
γ : Γ₀ˣ
x : hat K
γ₀' : ValueGroup₀ (F := Valuation K Γ₀) v := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := (extensionValuation : (a : hat K) → Γ₀) x
hγ₀_def : γ₀ = (extensionValuation : (a : hat K) → Γ₀) x
heq : γ₀ = (embedding : (a : ValueGroup₀ v) → Γ₀) γ₀'
h : γ₀ ≠ 0
h' : γ₀' ≠ 0
hγ₀ : extension ⁻¹' {γ₀'} ∈ 𝓝 x
hx : ∀ t ∈ 𝓝 x, ∃ (y : (↑(Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)}) : Type u_1)), (↑y : hat K) ∈ t
y : K
hy₁ : (v : (a : K) → Γ₀) y < (↑γ : Γ₀)
hy₂ :
  ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) y =
    γ₀'
⊢ (v : (a : K) → Γ₀) y = γ₀
have rw : (embedding : (a : ValueGroup₀ v) → Γ₀)
    (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
        y :
      ValueGroup₀ (F := Valuation K Γ₀) v) =
  γ₀
Tactic: rw [← embedding_restrict₀, hy₂, heq]
-- 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 Γ₀
γ : Γ₀ˣ
x : hat K
γ₀' : ValueGroup₀ (F := Valuation K Γ₀) v := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := (extensionValuation : (a : hat K) → Γ₀) x
hγ₀_def : γ₀ = (extensionValuation : (a : hat K) → Γ₀) x
heq : γ₀ = (embedding : (a : ValueGroup₀ v) → Γ₀) γ₀'
h : γ₀ ≠ 0
h' : γ₀' ≠ 0
hγ₀ : extension ⁻¹' {γ₀'} ∈ 𝓝 x
hx : ∀ t ∈ 𝓝 x, ∃ (y : (↑(Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)}) : Type u_1)), (↑y : hat K) ∈ t
y : K
hy₁ : (v : (a : K) → Γ₀) y < (↑γ : Γ₀)
hy₂ :
  ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) y =
    γ₀'
rw :
  (embedding : (a : ValueGroup₀ v) → Γ₀)
      (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
          y :
        ValueGroup₀ (F := Valuation K Γ₀) v) =
    γ₀
⊢ (v : (a : K) → Γ₀) y = γ₀
have rw₁ : (embedding : (a : ValueGroup₀ v) → Γ₀) γ₀' = γ₀
Tactic: rw [← embedding_restrict₀, hy₂, heq]
-- 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 Γ₀
γ : Γ₀ˣ
x : hat K
γ₀' : ValueGroup₀ (F := Valuation K Γ₀) v := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := (extensionValuation : (a : hat K) → Γ₀) x
hγ₀_def : γ₀ = (extensionValuation : (a : hat K) → Γ₀) x
heq : γ₀ = (embedding : (a : ValueGroup₀ v) → Γ₀) γ₀'
h : γ₀ ≠ 0
h' : γ₀' ≠ 0
hγ₀ : extension ⁻¹' {γ₀'} ∈ 𝓝 x
hx : ∀ t ∈ 𝓝 x, ∃ (y : (↑(Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)}) : Type u_1)), (↑y : hat K) ∈ t
y : K
hy₁ : (v : (a : K) → Γ₀) y < (↑γ : Γ₀)
hy₂ :
  ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) y =
    γ₀'
rw :
  (embedding : (a : ValueGroup₀ v) → Γ₀)
      (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
          y :
        ValueGroup₀ (F := Valuation K Γ₀) v) =
    γ₀
rw₁ : (embedding : (a : ValueGroup₀ v) → Γ₀) γ₀' = γ₀
⊢ (v : (a : K) → Γ₀) y = γ₀
have rw₂ : Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) γ₀' : Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) γ₀' : Γ₀)
Tactic: rw [← embedding_restrict₀, hy₂, heq]
-- 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 Γ₀
γ : Γ₀ˣ
x : hat K
γ₀' : ValueGroup₀ (F := Valuation K Γ₀) v := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := (extensionValuation : (a : hat K) → Γ₀) x
hγ₀_def : γ₀ = (extensionValuation : (a : hat K) → Γ₀) x
heq : γ₀ = (embedding : (a : ValueGroup₀ v) → Γ₀) γ₀'
h : γ₀ ≠ 0
h' : γ₀' ≠ 0
hγ₀ : extension ⁻¹' {γ₀'} ∈ 𝓝 x
hx : ∀ t ∈ 𝓝 x, ∃ (y : (↑(Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)}) : Type u_1)), (↑y : hat K) ∈ t
y : K
hy₁ : (v : (a : K) → Γ₀) y < (↑γ : Γ₀)
hy₂ :
  Membership.mem (γ := Set (hat K)) (extension ⁻¹' {γ₀'})
    (↑(Subtype.mk (p := fun (x : hat K) ↦
          Membership.mem (γ := Set (hat K)) (Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)}) x)
          (↑y : hat K) ⋯) :
      hat K)
⊢ γ₀ < (↑γ : Γ₀)
have hy₃ : (v : (a : K) → Γ₀) y = γ₀
Tactic: replace hy₂ : v y = γ₀ := by
      simp only [mem_preimage, extension_extends, mem_singleton_iff, v.restrict_def] at hy₂
      rw [← embedding_restrict₀, hy₂, heq]
Cleared hypotheses: hy₂
-- 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 Γ₀
γ : Γ₀ˣ
x : hat K
γ₀' : ValueGroup₀ (F := Valuation K Γ₀) v := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := (extensionValuation : (a : hat K) → Γ₀) x
hγ₀_def : γ₀ = (extensionValuation : (a : hat K) → Γ₀) x
heq : γ₀ = (embedding : (a : ValueGroup₀ v) → Γ₀) γ₀'
h : γ₀ ≠ 0
h' : γ₀' ≠ 0
hγ₀ : extension ⁻¹' {γ₀'} ∈ 𝓝 x
hx : γ₀ < (↑γ : Γ₀)
s : Set (hat K)
hs : s ∈ 𝓝 x
⊢ ∃ (y : (↑(Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)}) : Type u_1)), (↑y : hat K) ∈ s
have h₁ : ∀ (y : K) (hy₁ : Membership.mem (γ := Set (hat K)) (extension ⁻¹' {γ₀'}) (↑y : hat K)) (hy₂ : (↑y : hat K) ∈ s),
  ∃ (y : (↑(Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)}) : Type u_1)), (↑y : hat K) ∈ s
Tactic: obtain ⟨y, hy₁, hy₂⟩ := Completion.denseRange_coe.mem_nhds (inter_mem hγ₀ hs)
-- 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 Γ₀
γ : Γ₀ˣ
x : hat K
γ₀' : ValueGroup₀ (F := Valuation K Γ₀) v := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := (extensionValuation : (a : hat K) → Γ₀) x
hγ₀_def : γ₀ = (extensionValuation : (a : hat K) → Γ₀) x
heq : γ₀ = (embedding : (a : ValueGroup₀ v) → Γ₀) γ₀'
h : γ₀ ≠ 0
h' : γ₀' ≠ 0
hγ₀ : extension ⁻¹' {γ₀'} ∈ 𝓝 x
hx : γ₀ < (↑γ : Γ₀)
s : Set (hat K)
hs : s ∈ 𝓝 x
y : K
hy₁ : Membership.mem (γ := Set (hat K)) (extension ⁻¹' {γ₀'}) (↑y : hat K)
hy₂ : (↑y : hat K) ∈ s
⊢ (v : (a : K) → Γ₀) y = γ₀
have hy₃ : ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) y = γ₀'
Tactic: simp only [mem_preimage, extension_extends, mem_singleton_iff, v.restrict_def] at hy₁
Cleared hypotheses: hy₁
-- 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 Γ₀
γ : Γ₀ˣ
x : hat K
γ₀' : ValueGroup₀ (F := Valuation K Γ₀) v := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := (extensionValuation : (a : hat K) → Γ₀) x
hγ₀_def : γ₀ = (extensionValuation : (a : hat K) → Γ₀) x
heq : γ₀ = (embedding : (a : ValueGroup₀ v) → Γ₀) γ₀'
h : γ₀ ≠ 0
h' : γ₀' ≠ 0
hγ₀ : extension ⁻¹' {γ₀'} ∈ 𝓝 x
hx : γ₀ < (↑γ : Γ₀)
s : Set (hat K)
hs : s ∈ 𝓝 x
y : K
hy₂ : (↑y : hat K) ∈ s
hy₁ :
  ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) y =
    γ₀'
⊢ (v : (a : K) → Γ₀) y = γ₀
have rw : (embedding : (a : ValueGroup₀ v) → Γ₀)
    (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
        y :
      ValueGroup₀ (F := Valuation K Γ₀) v) =
  γ₀
Tactic: rw [← embedding_restrict₀, hy₁, heq]
-- 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 Γ₀
γ : Γ₀ˣ
x : hat K
γ₀' : ValueGroup₀ (F := Valuation K Γ₀) v := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := (extensionValuation : (a : hat K) → Γ₀) x
hγ₀_def : γ₀ = (extensionValuation : (a : hat K) → Γ₀) x
heq : γ₀ = (embedding : (a : ValueGroup₀ v) → Γ₀) γ₀'
h : γ₀ ≠ 0
h' : γ₀' ≠ 0
hγ₀ : extension ⁻¹' {γ₀'} ∈ 𝓝 x
hx : γ₀ < (↑γ : Γ₀)
s : Set (hat K)
hs : s ∈ 𝓝 x
y : K
hy₂ : (↑y : hat K) ∈ s
hy₁ :
  ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) y =
    γ₀'
rw :
  (embedding : (a : ValueGroup₀ v) → Γ₀)
      (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
          y :
        ValueGroup₀ (F := Valuation K Γ₀) v) =
    γ₀
⊢ (v : (a : K) → Γ₀) y = γ₀
have rw₁ : (embedding : (a : ValueGroup₀ v) → Γ₀) γ₀' = γ₀
Tactic: rw [← embedding_restrict₀, hy₁, heq]
-- 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 Γ₀
γ : Γ₀ˣ
x : hat K
γ₀' : ValueGroup₀ (F := Valuation K Γ₀) v := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := (extensionValuation : (a : hat K) → Γ₀) x
hγ₀_def : γ₀ = (extensionValuation : (a : hat K) → Γ₀) x
heq : γ₀ = (embedding : (a : ValueGroup₀ v) → Γ₀) γ₀'
h : γ₀ ≠ 0
h' : γ₀' ≠ 0
hγ₀ : extension ⁻¹' {γ₀'} ∈ 𝓝 x
hx : γ₀ < (↑γ : Γ₀)
s : Set (hat K)
hs : s ∈ 𝓝 x
y : K
hy₂ : (↑y : hat K) ∈ s
hy₁ :
  ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) y =
    γ₀'
rw :
  (embedding : (a : ValueGroup₀ v) → Γ₀)
      (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
          y :
        ValueGroup₀ (F := Valuation K Γ₀) v) =
    γ₀
rw₁ : (embedding : (a : ValueGroup₀ v) → Γ₀) γ₀' = γ₀
⊢ (v : (a : K) → Γ₀) y = γ₀
have rw₂ : Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) γ₀' : Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) γ₀' : Γ₀)
Tactic: rw [← embedding_restrict₀, hy₁, heq]
-- 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 Γ₀
γ : Γ₀ˣ
x : hat K
γ₀' : ValueGroup₀ (F := Valuation K Γ₀) v := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := (extensionValuation : (a : hat K) → Γ₀) x
hγ₀_def : γ₀ = (extensionValuation : (a : hat K) → Γ₀) x
heq : γ₀ = (embedding : (a : ValueGroup₀ v) → Γ₀) γ₀'
h : γ₀ ≠ 0
h' : γ₀' ≠ 0
hγ₀ : extension ⁻¹' {γ₀'} ∈ 𝓝 x
hx : γ₀ < (↑γ : Γ₀)
s : Set (hat K)
hs : s ∈ 𝓝 x
y : K
hy₁ : Membership.mem (γ := Set (hat K)) (extension ⁻¹' {γ₀'}) (↑y : hat K)
hy₂ : (↑y : hat K) ∈ s
⊢ ∃ (y : (↑(Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)}) : Type u_1)), (↑y : hat K) ∈ s
have hy₃ : (v : (a : K) → Γ₀) y = γ₀
Tactic: replace hy₁ : v y = γ₀ := by
      simp only [mem_preimage, extension_extends, mem_singleton_iff, v.restrict_def] at hy₁
      rw [← embedding_restrict₀, hy₁, heq]
Cleared hypotheses: hy₁
-- 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 Γ₀
γ : Γ₀ˣ
x : hat K
γ₀' : ValueGroup₀ (F := Valuation K Γ₀) v := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := (extensionValuation : (a : hat K) → Γ₀) x
hγ₀_def : γ₀ = (extensionValuation : (a : hat K) → Γ₀) x
heq : γ₀ = (embedding : (a : ValueGroup₀ v) → Γ₀) γ₀'
h : γ₀ ≠ 0
h' : γ₀' ≠ 0
hγ₀ : extension ⁻¹' {γ₀'} ∈ 𝓝 x
hx : γ₀ < (↑γ : Γ₀)
s : Set (hat K)
hs : s ∈ 𝓝 x
y : K
hy₂ : (↑y : hat K) ∈ s
hy₁ : (v : (a : K) → Γ₀) y = γ₀
⊢ ∃ (y : (↑(Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)}) : Type u_1)), (↑y : hat K) ∈ s
have hx₁ : (v : (a : K) → Γ₀) y < (↑γ : Γ₀)
Tactic: rw [← hy₁] at hx
Cleared hypotheses: hx, hy₂, hy₁
-- 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 Γ₀
r s : K
hr : r ≠ 0
hs : s ≠ 0
⊢ Eq.{u_1 + 1} (α := Set (hat K))
    (closure
      (Completion.coe' ''
        {x : K |
          HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) <
            (v : (a : K) → Γ₀) s}))
    {x : hat K |
      HMul.hMul (α := Γ₀) (β := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) <
        (v : (a : K) → Γ₀) s}
have hrs : HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) ≠ 0
Tactic: have hrs : v s / v r ≠ 0 := by simp [hr, hs]
-- 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 Γ₀
r s : K
hr : r ≠ 0
hs : s ≠ 0
hrs : HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) ≠ 0
⊢ Eq.{u_1 + 1} (α := Set (hat K))
    (closure
      (Completion.coe' ''
        {x : K |
          HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) <
            (v : (a : K) → Γ₀) s}))
    {x : hat K |
      HMul.hMul (α := Γ₀) (β := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) <
        (v : (a : K) → Γ₀) s}
have h : Eq.{u_1 + 1} (α := Set K)
  {x : K | HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) < (v : (a : K) → Γ₀) s}
  {x : K |
    (v : (a : K) → Γ₀) x <
      (↑(Units.mk0 (HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)) hrs) : Γ₀)}
Tactic: convert! closure_coe_completion_v_lt (γ := .mk0 _ hrs) using 3
-- 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 Γ₀
r s : K
hr : r ≠ 0
hs : s ≠ 0
hrs : HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) ≠ 0
h :
  Eq.{u_1 + 1} (α := Set K)
    {x : K |
      HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) < (v : (a : K) → Γ₀) s}
    {x : K |
      (v : (a : K) → Γ₀) x <
        (↑(Units.mk0 (HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)) hrs) : Γ₀)}
⊢ Eq.{u_1 + 1} (α := Set (hat K))
    (closure
      (Completion.coe' ''
        {x : K |
          HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) <
            (v : (a : K) → Γ₀) s}))
    {x : hat K |
      HMul.hMul (α := Γ₀) (β := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) <
        (v : (a : K) → Γ₀) s}
have h₁ : ∀ (x : hat K),
  HMul.hMul (α := Γ₀) (β := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) <
      (v : (a : K) → Γ₀) s ↔
    (extensionValuation : (a : hat K) → Γ₀) x <
      (↑(Units.mk0 (HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)) hrs) : Γ₀)
Tactic: convert! closure_coe_completion_v_lt (γ := .mk0 _ hrs) using 3
-- 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 Γ₀
⊢ Eq.{u_2 + 1} (α := ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)
    ((Valuation.restrict extensionValuation : (a : hat K) → ValueGroup₀ (↑extensionValuation : hat K →*₀ Γ₀))
        (↑(Exists.choose (p := fun (a : K) ↦
              Eq.{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)
                    a :
                  ValueGroup₀ (F := Valuation K Γ₀) v)
                (1 : ValueGroup₀ (F := Valuation K Γ₀) v))
              ⋯) :
          hat K) :
      ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑extensionValuation : hat K →*₀ Γ₀))
    (1 : ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)
have rw : Eq (α := Γ₀)
  ((embedding : (a : ValueGroup₀ extensionValuation.toMonoidWithZeroHom) → Γ₀)
      (((restrict₀ extensionValuation :
              MonoidWithZeroHom.{u_1, u_2} (hat K)
                (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)) :
            (a : hat K) → ValueGroup₀ extensionValuation)
          (↑(Exists.choose (p := fun (a : K) ↦
                Eq.{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)
                      a :
                    ValueGroup₀ (F := Valuation K Γ₀) v)
                  (1 : ValueGroup₀ (F := Valuation K Γ₀) v))
                sorry) :
            hat K) :
        ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) :
    Γ₀)
  (1 : Γ₀)
Tactic: rw [← embedding_strictMono.injective.eq_iff, Valuation.restrict_def, map_one]
-- 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 Γ₀
⊢ Eq (α := Γ₀)
    ((embedding : (a : ValueGroup₀ extensionValuation.toMonoidWithZeroHom) → Γ₀)
        (((restrict₀ extensionValuation :
                MonoidWithZeroHom.{u_1, u_2} (hat K)
                  (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)) :
              (a : hat K) → ValueGroup₀ extensionValuation)
            (↑(Exists.choose (p := fun (a : K) ↦
                  Eq.{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)
                        a :
                      ValueGroup₀ (F := Valuation K Γ₀) v)
                    (1 : ValueGroup₀ (F := Valuation K Γ₀) v))
                  ⋯) :
              hat K) :
          ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) :
      Γ₀)
    (1 : Γ₀)
have erw : Eq.{u_2 + 1} (α := Γ₀)
  ((Valuation.toMonoidWithZeroHom extensionValuation : (a : hat K) → Γ₀)
      (↑(Exists.choose (p := fun (a : K) ↦
            Eq.{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)
                  a :
                ValueGroup₀ (F := Valuation K Γ₀) v)
              (1 : ValueGroup₀ (F := Valuation K Γ₀) v))
            sorry) :
        hat K) :
    Γ₀)
  (1 : Γ₀)
Tactic: erw [embedding_restrict₀]