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 : K
rw : Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension (↑x : hat K)) : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
rw₁ :
  Eq (α := Γ₀)
    ((embedding : (a : ValueGroup₀ v) → Γ₀)
        ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x :
          ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) :
      Γ₀)
    ((v : (a : K) → Γ₀) x : Γ₀)
⊢ Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) (↑x : hat K) : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
have rw₂ : Eq (α := Γ₀)
  ((embedding : (a : ValueGroup₀ v) → Γ₀)
      (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
          x :
        ValueGroup₀ (F := Valuation K Γ₀) v) :
    Γ₀)
  ((v : (a : K) → Γ₀) x : Γ₀)
Tactic: rw [extensionValuation_toFun, extension_extends, Valuation.restrict_def, embedding_restrict₀]
-- 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 : K
rw : Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension (↑x : hat K)) : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
rw₁ :
  Eq (α := Γ₀)
    ((embedding : (a : ValueGroup₀ v) → Γ₀)
        ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x :
          ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) :
      Γ₀)
    ((v : (a : K) → Γ₀) x : Γ₀)
rw₂ :
  Eq (α := Γ₀)
    ((embedding : (a : ValueGroup₀ v) → Γ₀)
        (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) :
              (a : K) → ValueGroup₀ v)
            x :
          ValueGroup₀ (F := Valuation K Γ₀) v) :
      Γ₀)
    ((v : (a : K) → Γ₀) x : Γ₀)
⊢ Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) (↑x : hat K) : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
have rw₃ : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
Tactic: rw [extensionValuation_toFun, extension_extends, Valuation.restrict_def, embedding_restrict₀]
-- 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
⊢ extension x = 0 ↔ x = 0
have suffices : Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀) (0 : Γ₀) ↔ x = 0
Tactic: suffices extensionValuation x = 0 ↔ x = 0 by
    simpa only [extensionValuation_toFun, map_eq_zero]
-- 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
⊢ Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀) (0 : Γ₀) ↔ x = 0
have rw : x = 0 ↔ x = 0
Tactic: rw [Valuation.zero_iff]
-- 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
⊢ ∃ (r : K), Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)
have inl : ∃ (r : K), Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) 0 : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)
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 : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : hat K
inl : ∃ (r : K), Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) 0 : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)
⊢ ∃ (r : K), Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)
have inr : ∀ (h : x ≠ 0),
  ∃ (r : K), Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)
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 : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : hat K
h : x ≠ 0
⊢ ∃ (r : K), Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)
have inr : IsClosed.{u_1} (X := hat K)
  {b : hat K |
    ∃ (r : K), Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) b : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)}
Tactic: refine Completion.denseRange_coe.induction_on x ?_
      (fun a ↦ by simp [extensionValuation_apply_coe a])
-- 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
h : x ≠ 0
⊢ IsClosed.{u_1} (X := hat K)
    {b : hat K |
      ∃ (r : K), Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) b : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)}
have inr : IsClosed.{u_1} (X := hat K)
  {b : hat K |
    ∃ (r : K), Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension b) : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)}
Tactic: simp only [extensionValuation_toFun]
-- 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
h : x ≠ 0
r : K
⊢ Eq (α := Γ₀)
    ((embedding : (a : ValueGroup₀ v) → Γ₀)
        (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) :
              (a : K) → ValueGroup₀ v)
            r :
          ValueGroup₀ (F := Valuation K Γ₀) v) :
      Γ₀)
    ((v : (a : K) → Γ₀) r : Γ₀)
have rw : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)
Tactic: rw [embedding_restrict₀]
-- 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
h : x ≠ 0
⊢ IsClosed.{u_1} (X := hat K)
    {b : hat K |
      ∃ (r : K), Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension b) : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)}
have hr : ∀ (r : K),
  Eq (α := Γ₀)
    ((embedding : (a : ValueGroup₀ v) → Γ₀)
        (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) :
              (a : K) → ValueGroup₀ v)
            r :
          ValueGroup₀ (F := Valuation K Γ₀) v) :
      Γ₀)
    ((v : (a : K) → Γ₀) r : Γ₀)
Tactic: have hr (r : K) : ValueGroup₀.embedding (restrict₀ hv.v r) = v r := by
        rw [embedding_restrict₀]
-- 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
h : x ≠ 0
hr :
  ∀ (r : K),
    Eq (α := Γ₀)
      ((embedding : (a : ValueGroup₀ v) → Γ₀)
          (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) :
                (a : K) → ValueGroup₀ v)
              r :
            ValueGroup₀ (F := Valuation K Γ₀) v) :
        Γ₀)
      ((v : (a : K) → Γ₀) r : Γ₀)
a b : ValueGroup₀ (F := Valuation K Γ₀) v
⊢ Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) a : Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) b : Γ₀) ↔ a = b
have rw : a = b ↔ a = b
Tactic: rw [embedding_strictMono.injective.eq_iff]
-- 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
h : x ≠ 0
hr :
  ∀ (r : K),
    Eq (α := Γ₀)
      ((embedding : (a : ValueGroup₀ v) → Γ₀)
          (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) :
                (a : K) → ValueGroup₀ v)
              r :
            ValueGroup₀ (F := Valuation K Γ₀) v) :
        Γ₀)
      ((v : (a : K) → Γ₀) r : Γ₀)
⊢ IsClosed.{u_1} (X := hat K)
    {b : hat K |
      ∃ (r : K), Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension b) : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)}
have h₁ : ∀ (a b : ValueGroup₀ (F := Valuation K Γ₀) v),
  Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) a : Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) b : Γ₀) ↔ a = b
Tactic: have h (a b : ValueGroup₀ hv.v) : ValueGroup₀.embedding a = ValueGroup₀.embedding b ↔
          a = b := by rw [embedding_strictMono.injective.eq_iff]
-- 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
h_1 : x ≠ 0
hr :
  ∀ (r : K),
    Eq (α := Γ₀)
      ((embedding : (a : ValueGroup₀ v) → Γ₀)
          (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) :
                (a : K) → ValueGroup₀ v)
              r :
            ValueGroup₀ (F := Valuation K Γ₀) v) :
        Γ₀)
      ((v : (a : K) → Γ₀) r : Γ₀)
h :
  ∀ (a b : ValueGroup₀ (F := Valuation K Γ₀) v),
    Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) a : Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) b : Γ₀) ↔ a = b
⊢ IsClosed.{u_1} (X := hat K)
    {b : hat K |
      ∃ (r : K), Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension b) : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)}
have inr : IsClosed.{u_1} (X := hat K)
  {b : hat K | ∃ (r : K), extension b = (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) r}
Tactic: simp_rw [← hr, ← Valuation.restrict_def, 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 Γ₀
x : hat K
h_1 : x ≠ 0
hr :
  ∀ (r : K),
    Eq (α := Γ₀)
      ((embedding : (a : ValueGroup₀ v) → Γ₀)
          (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) :
                (a : K) → ValueGroup₀ v)
              r :
            ValueGroup₀ (F := Valuation K Γ₀) v) :
        Γ₀)
      ((v : (a : K) → Γ₀) r : Γ₀)
h :
  ∀ (a b : ValueGroup₀ (F := Valuation K Γ₀) v),
    Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) a : Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) b : Γ₀) ↔ a = b
⊢ IsClosed.{u_1} (X := hat K)
    {b : hat K | ∃ (r : K), extension b = (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) r}
have h₁ : Eq.{u_1 + 1} (α := Set (hat K))
  {b : hat K | ∃ (r : K), extension b = (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) r}
  (extension ⁻¹' range.{u_2, u_1 + 1} (ι := K) (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)))
Tactic: convert! valuation_isClosedMap.isClosed_range.preimage (continuous_extension (hv := hv))
-- 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
h_1 : x ≠ 0
hr :
  ∀ (r : K),
    Eq (α := Γ₀)
      ((embedding : (a : ValueGroup₀ v) → Γ₀)
          (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) :
                (a : K) → ValueGroup₀ v)
              r :
            ValueGroup₀ (F := Valuation K Γ₀) v) :
        Γ₀)
      ((v : (a : K) → Γ₀) r : Γ₀)
h :
  ∀ (a b : ValueGroup₀ (F := Valuation K Γ₀) v),
    Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) a : Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) b : Γ₀) ↔ a = b
⊢ Eq.{u_1 + 1} (α := Set (hat K))
    {b : hat K | ∃ (r : K), extension b = (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) r}
    (extension ⁻¹' range.{u_2, u_1 + 1} (ι := K) (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)))
have h₁ : Eq.{u_1 + 1} (α := Set (hat K))
  {b : hat K | ∃ (r : K), (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) r = extension b}
  (extension ⁻¹' range.{u_2, u_1 + 1} (ι := K) (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)))
Tactic: simp_rw [eq_comm (a := extension _)]
-- 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
h_1 : x ≠ 0
hr :
  ∀ (r : K),
    Eq (α := Γ₀)
      ((embedding : (a : ValueGroup₀ v) → Γ₀)
          (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) :
                (a : K) → ValueGroup₀ v)
              r :
            ValueGroup₀ (F := Valuation K Γ₀) v) :
        Γ₀)
      ((v : (a : K) → Γ₀) r : Γ₀)
h :
  ∀ (a b : ValueGroup₀ (F := Valuation K Γ₀) v),
    Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) a : Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) b : Γ₀) ↔ a = b
⊢ Eq.{u_1 + 1} (α := Set (hat K))
    {b : hat K | ∃ (r : K), (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) r = extension b}
    (extension ⁻¹' range.{u_2, u_1 + 1} (ι := K) (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)))
have h₁ : ∀ (x : hat K),
  Membership.mem (γ := Set (hat K))
      {b : hat K | ∃ (r : K), (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) r = extension b} x ↔
    Membership.mem (γ := Set (hat K))
      (extension ⁻¹' range.{u_2, u_1 + 1} (ι := K) (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀))) x
Tactic: ext
-- 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_1 + 1} (α := Set (hat K)) (closure (Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)}))
    {x : hat K | (extensionValuation : (a : hat K) → Γ₀) x < (↑γ : Γ₀)}
have h : ∀ (x : hat K),
  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: ext x
-- 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
⊢ 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
have hγ₀'_def : let γ₀' := extension x;
γ₀' = extension x
Tactic: set γ₀' := extension x with hγ₀'_def
-- 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
⊢ 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
have hγ₀_def : let γ₀ : Γ₀ := (extensionValuation : (a : hat K) → Γ₀) x;
γ₀ = (extensionValuation : (a : hat K) → Γ₀) x
Tactic: set γ₀ := extensionValuation x with hγ₀_def
-- 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
⊢ 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
have heq : γ₀ = (embedding : (a : ValueGroup₀ v) → Γ₀) γ₀'
Tactic: have heq : γ₀ = embedding γ₀' := rfl
-- 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) → Γ₀) γ₀'
this :
  γ₀ ≠ 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
have inl : ∀ (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: rcases eq_or_ne γ₀ 0 with h | 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 Γ₀
γ : Γ₀ˣ
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 ↔
      γ₀ < (↑γ : Γ₀))
inl :
  ∀ (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
⊢ 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
have inr : ∀ (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: rcases eq_or_ne γ₀ 0 with h | 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 Γ₀
γ : Γ₀ˣ
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
have inl : Membership.mem (γ := Set (hat K)) (closure (Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)})) 0
Tactic: simp only [(Valuation.zero_iff _).mp h, mem_setOf_eq, Valuation.map_zero, Units.zero_lt,
        iff_true]
-- 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) → Γ₀) γ₀'
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 < (↑γ : Γ₀)})) 0
have inl : Membership.mem (γ := Set (hat K)) (Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)}) 0
Tactic: apply subset_closure
-- 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) → Γ₀) γ₀'
this :
  γ₀ ≠ 0 →
    (Membership.mem (γ := Set (hat K)) (closure (Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)})) x ↔
      γ₀ < (↑γ : Γ₀))
h : γ₀ = 0
⊢ Membership.mem (γ := Set K) {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)} 0 ∧ Eq.{u_1 + 1} (α := hat K) (↑0 : hat K) 0
have simp : Eq.{u_1 + 1} (α := hat K) (↑0 : hat K) 0
Tactic: simp only [mem_setOf_eq, Valuation.map_zero, Units.zero_lt, true_and]
-- 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) → Γ₀) γ₀'
⊢ 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
have h : γ₀ ≠ 0 →
  (Membership.mem (γ := Set (hat K)) (closure (Completion.coe' '' {x : K | (v : (a : 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
-- 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
⊢ Membership.mem (γ := Set (hat K)) (closure (Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)})) x ↔
    γ₀ < (↑γ : Γ₀)
have h' : γ₀' ≠ 0
Tactic: have h' : γ₀' ≠ 0 := by simpa only [heq, map_ne_zero] using 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
⊢ Membership.mem (γ := Set (hat K)) (closure (Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)})) x ↔
    γ₀ < (↑γ : Γ₀)
have hγ₀ : extension ⁻¹' {γ₀'} ∈ 𝓝 x
Tactic: have hγ₀ : extension ⁻¹' {γ₀'} ∈ 𝓝 x :=
    continuous_extension.continuousAt.preimage_mem_nhds
      (WithZeroTopology.singleton_mem_nhds_of_ne_zero h')