awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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) → Γ₀) γ₀'
this :
  γ₀ ≠ 0 →
    (Membership.mem (γ := Set (hat K)) (closure (Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)})) x ↔
      γ₀ < (↑γ : Γ₀))
h : γ₀ = 0
inl : Membership.mem (γ := Set (hat K)) (closure (Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)})) 0
⊢ Membership.mem (γ := Set (hat K)) (closure (Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)})) x ↔
    Membership.mem (γ := Set (hat K)) {x : hat K | (extensionValuation : (a : hat K) → Γ₀) x < (↑γ : Γ₀)} x

Tactic:
simp only [(Valuation.zero_iff _).mp h, mem_setOf_eq, Valuation.map_zero, Units.zero_lt,
        iff_true]

Premises used: iff_true, Valuation.zero_iff, Set.mem_setOf_eq, Iff.mp, Units.zero_lt, Valuation.map_zero
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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) → Γ₀) γ₀'
this :
  γ₀ ≠ 0 →
    (Membership.mem (γ := Set (hat K)) (closure (Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)})) x ↔
      γ₀ < (↑γ : Γ₀))
h : γ₀ = 0
inl : Membership.mem (γ := Set (hat K)) (Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)}) 0
⊢ Membership.mem (γ := Set (hat K)) (closure (Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)})) 0

Tactic:
apply subset_closure

Premises used: subset_closure
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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) → Γ₀) γ₀'
this :
  γ₀ ≠ 0 →
    (Membership.mem (γ := Set (hat K)) (closure (Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)})) x ↔
      γ₀ < (↑γ : Γ₀))
h : γ₀ = 0
simp : Eq.{u_1 + 1} (α := hat K) (↑0 : hat K) 0
⊢ Membership.mem (γ := Set K) {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)} 0 ∧ Eq.{u_1 + 1} (α := hat K) (↑0 : hat K) 0

Tactic:
simp only [mem_setOf_eq, Valuation.map_zero, Units.zero_lt, true_and]

Premises used: Set.mem_setOf_eq, Units.zero_lt, Valuation.map_zero, true_and
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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) → Γ₀) γ₀'
this :
  γ₀ ≠ 0 →
    (Membership.mem (γ := Set (hat K)) (closure (Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)})) x ↔
      γ₀ < (↑γ : Γ₀))
h : γ₀ = 0
⊢ Eq.{u_1 + 1} (α := hat K) (↑0 : hat K) 0

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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) → Γ₀) γ₀'
this :
  γ₀ ≠ 0 →
    (Membership.mem (γ := Set (hat K)) (closure (Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)})) x ↔
      γ₀ < (↑γ : Γ₀))
h : γ₀ = 0
⊢ Membership.mem (γ := Set (hat K)) (Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)}) 0

Tactic:
exact ⟨0, by simp only [mem_setOf_eq, Valuation.map_zero, Units.zero_lt, true_and]; rfl⟩
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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) → Γ₀) γ₀'
this :
  γ₀ ≠ 0 →
    (Membership.mem (γ := Set (hat K)) (closure (Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)})) x ↔
      γ₀ < (↑γ : Γ₀))
h : γ₀ ≠ 0
⊢ Membership.mem (γ := Set (hat K)) (closure (Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)})) x ↔
    Membership.mem (γ := Set (hat K)) {x : hat K | (extensionValuation : (a : hat K) → Γ₀) x < (↑γ : Γ₀)} x

Tactic:
this h

Premises used: Set.Mem, setOf
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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) → Γ₀) γ₀'
this :
  γ₀ ≠ 0 →
    (Membership.mem (γ := Set (hat K)) (closure (Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)})) x ↔
      γ₀ < (↑γ : Γ₀))
h : γ₀ ≠ 0
⊢ Membership.mem (γ := Set (hat K)) (closure (Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)})) x ↔
    Membership.mem (γ := Set (hat K)) {x : hat K | (extensionValuation : (a : hat K) → Γ₀) x < (↑γ : Γ₀)} x

Tactic:
exact this h
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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 →
    (Membership.mem (γ := Set (hat K)) (closure (Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)})) x ↔
      γ₀ < (↑γ : Γ₀))
⊢ Membership.mem (γ := Set (hat K)) (closure (Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)})) x ↔
    Membership.mem (γ := Set (hat K)) {x : hat K | (extensionValuation : (a : hat K) → Γ₀) x < (↑γ : Γ₀)} x

Tactic:
suffices γ₀ ≠ 0 → (x ∈ closure ((↑) '' { x : K | v x < (γ : Γ₀) }) ↔ γ₀ < (γ : Γ₀)) by
    rcases eq_or_ne γ₀ 0 with h | h
    · simp only [(Valuation.zero_iff _).mp h, mem_setOf_eq, Valuation.map_zero, Units.zero_lt,
        iff_true]
      apply subset_closure
      exact ⟨0, by simp only [mem_setOf_eq, Valuation.map_zero, Units.zero_lt, true_and]; rfl⟩
    · exact this h
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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
⊢ γ₀' ≠ 0

Tactic:
simpa only [heq, map_ne_zero] using h

Premises used: map_ne_zero
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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
⊢ γ₀' ≠ 0

Tactic:
have h' : γ₀' ≠ 0 := by simpa only [heq, map_ne_zero] using h
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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
⊢ extension ⁻¹' {γ₀'} ∈ 𝓝 x

Tactic:
have hγ₀ : extension ⁻¹' {γ₀'} ∈ 𝓝 x :=
    continuous_extension.continuousAt.preimage_mem_nhds
      (WithZeroTopology.singleton_mem_nhds_of_ne_zero h')
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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₁ :
  (∀ t ∈ 𝓝 x, ∃ (y : (↑(Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)}) : Type u_1)), (↑y : hat K) ∈ t) ↔
    γ₀ < (↑γ : Γ₀)
⊢ Membership.mem (γ := Set (hat K)) (closure (Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)})) x ↔
    γ₀ < (↑γ : Γ₀)

Tactic:
rw [mem_closure_iff_nhds']

Premises used: mem_closure_iff_nhds'
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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) ↔
    γ₀ < (↑γ : Γ₀)

Tactic:
⟨fun hx => ?_, fun hx s hs => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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),
    γ₀ < (↑γ : Γ₀)
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
⊢ (∀ 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 => ?_⟩
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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
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) ⋯) :
          hat K)),
    γ₀ < (↑γ : Γ₀)
⊢ γ₀ < (↑γ : Γ₀)

Tactic:
obtain ⟨⟨-, y, hy₁ : v y < (γ : Γ₀), rfl⟩, hy₂⟩ := hx _ hγ₀

Premises used: Units.val, rfl
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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)
⊢ ((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₂

Premises used: Valued.extension_extends, Valued.v, Valuation.restrict_def, Set.mem_singleton_iff, Set.mem_preimage
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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) → Γ₀) γ₀' = γ₀
rw₂ rw₃ :
  Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) γ₀' : Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) γ₀' : Γ₀)
⊢ (v : (a : K) → Γ₀) y = γ₀

Tactic:
rw [← embedding_restrict₀, hy₂, heq]

Premises used: MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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 = γ₀

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]
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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₂ : (v : (a : K) → Γ₀) y = γ₀
h₁ h₂ h₃ h₄ : (v : (a : K) → Γ₀) y < (↑γ : Γ₀)
⊢ γ₀ < (↑γ : Γ₀)

Tactic:
rwa [← hy₂]
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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
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
⊢ ∃ (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)

Premises used: Filter.inter_mem, UniformSpace.Completion.denseRange_coe, DenseRange.mem_nhds
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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
⊢ ((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₁

Premises used: Valued.extension_extends, Valued.v, Valuation.restrict_def, Set.mem_singleton_iff, Set.mem_preimage
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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) → Γ₀) γ₀' = γ₀
rw₂ rw₃ :
  Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) γ₀' : Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) γ₀' : Γ₀)
⊢ (v : (a : K) → Γ₀) y = γ₀

Tactic:
rw [← embedding_restrict₀, hy₁, heq]

Premises used: MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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 = γ₀

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]
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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 = γ₀
⊢ (v : (a : K) → Γ₀) y < (↑γ : Γ₀)

Tactic:
rw [← hy₁] at hx
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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 = γ₀
hx₁ : (v : (a : K) → Γ₀) y < (↑γ : Γ₀)
⊢ (↑y : hat K) ∈ s

Tactic:
rw [← hy₁] at hx
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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 = γ₀
hx₁ : (v : (a : K) → Γ₀) y < (↑γ : Γ₀)
hy₃ : (↑y : hat K) ∈ s
⊢ (v : (a : K) → Γ₀) y = γ₀

Tactic:
rw [← hy₁] at hx
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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
s : Set (hat K)
hs : s ∈ 𝓝 x
y : K
hx : (v : (a : K) → Γ₀) y < (↑γ : Γ₀)
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

Tactic:
⟨⟨y, ⟨y, hx, rfl⟩⟩, hy₂⟩

Premises used: UniformSpace.Completion.coe', Subtype.mk, And.intro, Exists.intro, rfl