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 y : hat K
⊢ Continuous.{u_1, u_2} (X := hat K) extension

Tactic:
have cont : Continuous (Valued.extension : hat K → _) := Valued.continuous_extension
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x y : hat K
cont : Continuous.{u_1, u_2} (X := hat K) extension
⊢ Continuous.{u_1, u_2} (Y := ValueGroup₀ (F := Valuation K Γ₀) v) fun (x : hat K × hat K) ↦ extension (x.1 + x.2)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x y : hat K
cont : Continuous.{u_1, u_2} (X := hat K) extension
⊢ IsClosed.{u_1} (X := hat K × hat K)
    {x : hat K × hat K | extension (x.1 + x.2) ≤ extension x.1 ∨ extension (x.1 + x.2) ≤ extension x.2}

Tactic:
exact (isClosed_le (by fun_prop) <| cont.comp continuous_fst).union
          (isClosed_le (by fun_prop) <| cont.comp continuous_snd)

Premises used: Continuous.comp, IsClosed.union, isClosed_le, continuous_snd, continuous_fst
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x_1 y_1 : hat K
x y : K
ih :
  LE.le.{u_2} (α := ValueGroup₀ (F := Valuation K Γ₀) v)
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (x + y) :
        ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) ∨
    LE.le.{u_2} (α := ValueGroup₀ (F := Valuation K Γ₀) v)
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (x + y) :
        ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) y : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
⊢ extension (HAdd.hAdd (α := hat K) (↑x : hat K) (↑y : hat K)) ≤ extension (↑x : hat K) ∨
    extension (HAdd.hAdd (α := hat K) (↑x : hat K) (↑y : hat K)) ≤ extension (↑y : hat K)

Tactic:
norm_cast
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x_1 y_1 : hat K
x y : K
⊢ LE.le.{u_2} (α := ValueGroup₀ (F := Valuation K Γ₀) v)
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (x + y) :
        ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) ∨
    LE.le.{u_2} (α := ValueGroup₀ (F := Valuation K Γ₀) v)
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (x + y) :
        ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) y : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))

Tactic:
le_max_iff.mp (v.restrict.map_add x y)

Premises used: Valuation.map_add, Valued.v, Iff.mp, le_max_iff, Valuation.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_1 y_1 : hat K
x y : K
⊢ LE.le.{u_2} (α := ValueGroup₀ (F := Valuation K Γ₀) v)
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (x + y) :
        ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) ∨
    LE.le.{u_2} (α := ValueGroup₀ (F := Valuation K Γ₀) v)
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (x + y) :
        ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) y : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))

Tactic:
exact le_max_iff.mp (v.restrict.map_add x y)

Premises used: Valuation.map_add, Valued.v, Iff.mp, le_max_iff, Valuation.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
⊢ Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀)
    ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension x) : Γ₀)

Tactic:
rfl

Premises used: Set.Mem, setOf, 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 : 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 : Γ₀)
rw₃ rw₄ : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
⊢ Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) (↑x : hat K) : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)

Tactic:
rw [extensionValuation_toFun, extension_extends, Valuation.restrict_def, embedding_restrict₀]

Premises used: Valued.extension_extends, Valuation.restrict_def, MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀, Valued.extensionValuation_toFun
-- 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
this : Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀) (0 : Γ₀) ↔ x = 0
⊢ extension x = 0 ↔ x = 0

Tactic:
simpa only [extensionValuation_toFun, map_eq_zero]

Premises used: map_eq_zero, Valued.extensionValuation_toFun
-- 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
suffices : Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀) (0 : Γ₀) ↔ x = 0
⊢ extension x = 0 ↔ x = 0

Tactic:
suffices extensionValuation x = 0 ↔ x = 0 by
    simpa only [extensionValuation_toFun, map_eq_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
rw rw₁ : x = 0 ↔ x = 0
⊢ Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀) (0 : Γ₀) ↔ x = 0

Tactic:
rw [Valuation.zero_iff]

Premises used: Valuation.zero_iff
-- 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
inl : ∃ (r : K), Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) 0 : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)
inr :
  ∀ (h : x ≠ 0),
    ∃ (r : K), Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)
⊢ ∃ (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)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ ∃ (r : K), Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) 0 : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)

Tactic:
⟨0, extensionValuation_apply_coe 0⟩

Premises used: Valued.extensionValuation_apply_coe, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ ∃ (r : K), Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) 0 : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)

Tactic:
exact ⟨0, extensionValuation_apply_coe 0⟩
-- 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
h : x ≠ 0
a : K
⊢ ∃ (r : K),
    Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) (↑a : hat K) : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)

Tactic:
simp [extensionValuation_apply_coe a]

Premises used: Valued.extensionValuation_apply_coe
-- 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
h : x ≠ 0
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 : Γ₀)}
⊢ ∃ (r : K), Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)

Tactic:
refine Completion.denseRange_coe.induction_on x ?_
      (fun a ↦ by simp [extensionValuation_apply_coe a])
-- 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
h : x ≠ 0
inr :
  IsClosed.{u_1} (X := hat K)
    {b : hat K |
      ∃ (r : K), Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension b) : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)}
⊢ 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:
simp only [extensionValuation_toFun]

Premises used: Valued.extensionValuation_toFun
-- 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
h : x ≠ 0
r : K
rw rw₁ : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)
⊢ 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:
rw [embedding_restrict₀]

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
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 : Γ₀)

Tactic:
have hr (r : K) : ValueGroup₀.embedding (restrict₀ hv.v r) = v r := by
        rw [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
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
rw rw₁ : a = b ↔ a = b
⊢ Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) a : Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) b : Γ₀) ↔ a = b

Tactic:
rw [embedding_strictMono.injective.eq_iff]

Premises used: Function.Injective.eq_iff, StrictMono.injective
-- 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
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

Tactic:
have h (a b : ValueGroup₀ hv.v) : ValueGroup₀.embedding a = ValueGroup₀.embedding b ↔
          a = b := by rw [embedding_strictMono.injective.eq_iff]
-- 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
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
inr :
  IsClosed.{u_1} (X := hat K)
    {b : hat K | ∃ (r : K), extension b = (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) r}
⊢ IsClosed.{u_1} (X := hat K)
    {b : hat K |
      ∃ (r : K), Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension b) : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)}

Tactic:
simp_rw [← hr, ← Valuation.restrict_def, h]

Premises used: Valuation.restrict_def
-- 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
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)
    (extension ⁻¹' range.{u_2, u_1 + 1} (ι := K) (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)))

Tactic:
valuation_isClosedMap.isClosed_range.preimage (continuous_extension (hv := hv))

Premises used: Valued.continuous_extension, Valued.valuation_isClosedMap, IsClosed.preimage, IsClosedMap.isClosed_range
-- 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
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
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 →*₀ Γ₀)))
⊢ IsClosed.{u_1} (X := hat K)
    {b : hat K | ∃ (r : K), extension b = (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) r}

Tactic:
convert! valuation_isClosedMap.isClosed_range.preimage (continuous_extension (hv := hv))

Premises used: Valued.continuous_extension, Valued.valuation_isClosedMap, IsClosed.preimage, IsClosedMap.isClosed_range
-- 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
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
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 →*₀ Γ₀)))
⊢ 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:
simp_rw [eq_comm (a := extension _)]

Premises used: eq_comm
-- 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
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
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
⊢ 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:
ext
-- 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
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
x_1 : hat K
⊢ Membership.mem (γ := Set (hat K))
      {b : hat K | ∃ (r : K), (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) r = extension b} x_1 ↔
    Membership.mem (γ := Set (hat K))
      (extension ⁻¹' range.{u_2, u_1 + 1} (ι := K) (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)))
      x_1

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
γ : Γ₀ˣ
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
⊢ Eq.{u_1 + 1} (α := Set (hat K)) (closure (Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)}))
    {x : hat K | (extensionValuation : (a : hat K) → Γ₀) x < (↑γ : Γ₀)}

Tactic:
ext x
-- 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
⊢ let γ₀' := extension x;
  γ₀' = extension x

Tactic:
set γ₀' := extension x with hγ₀'_def

Premises used: Valued.extension
-- 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
⊢ let γ₀ : Γ₀ := (extensionValuation : (a : hat K) → Γ₀) x;
  γ₀ = (extensionValuation : (a : hat K) → Γ₀) x

Tactic:
set γ₀ := extensionValuation x with hγ₀_def

Premises used: Valued.extensionValuation, DFunLike.coe
-- 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
⊢ γ₀ = (embedding : (a : ValueGroup₀ v) → Γ₀) γ₀'

Tactic:
have heq : γ₀ = embedding γ₀' := 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 ↔
      γ₀ < (↑γ : Γ₀))
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
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
⊢ 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

Premises used: eq_or_ne, OfNat.ofNat