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
h : x₀ ≠ 0
preimage_one : Membership.mem (γ := Filter K) (𝓝 1) (preimage (β := Γ₀) (⇑v : (a : K) → Γ₀) {1})
V : Set (hat K)
V_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V
hV : ∀ (x : K), (↑x : hat K) ∈ V → Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
V' : Set (hat K)
V'_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V'
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
nhds_right : (fun (x : hat K) ↦ x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : (↑z₀ : hat K) = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne :
  Ne.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) z₀ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (0 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
a : K
y : hat K
y_in : y ∈ V'
ha : Eq (α := hat K) (↑a : hat K) ((fun (x : hat K) ↦ x * x₀) y)
this :
  Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (a * z₀⁻¹) :
      ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (1 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
rw :
  Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) a : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (a * (z₀⁻¹ * z₀)) :
      ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
rw₁ :
  Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) a : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (a * 1) :
      ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) a : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) a : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
⊢ Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) a : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (a * z₀⁻¹ * z₀) :
      ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))

Tactic:
rw [mul_assoc, inv_mul_cancel₀ z₀_ne, mul_one]

Premises used: mul_assoc, mul_one, inv_mul_cancel₀
-- 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
preimage_one : Membership.mem (γ := Filter K) (𝓝 1) (preimage (β := Γ₀) (⇑v : (a : K) → Γ₀) {1})
V : Set (hat K)
V_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V
hV : ∀ (x : K), (↑x : hat K) ∈ V → Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
V' : Set (hat K)
V'_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V'
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
nhds_right : (fun (x : hat K) ↦ x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : (↑z₀ : hat K) = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne :
  Ne.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) z₀ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (0 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
a : K
y : hat K
y_in : y ∈ V'
ha : Eq (α := hat K) (↑a : hat K) ((fun (x : hat K) ↦ x * x₀) y)
this :
  Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (a * z₀⁻¹) :
      ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (1 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
⊢ (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (a * z₀⁻¹ * z₀) =
    HMul.hMul (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) (β := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (a * z₀⁻¹) :
        ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) z₀ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))

Tactic:
Valuation.map_mul _ _ _

Premises used: Set.Mem, setOf, Valuation.map_mul
-- 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
preimage_one : Membership.mem (γ := Filter K) (𝓝 1) (preimage (β := Γ₀) (⇑v : (a : K) → Γ₀) {1})
V : Set (hat K)
V_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V
hV : ∀ (x : K), (↑x : hat K) ∈ V → Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
V' : Set (hat K)
V'_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V'
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
nhds_right : (fun (x : hat K) ↦ x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : (↑z₀ : hat K) = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne :
  Ne.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) z₀ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (0 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
a : K
y : hat K
y_in : y ∈ V'
ha : Eq (α := hat K) (↑a : hat K) ((fun (x : hat K) ↦ x * x₀) y)
this :
  Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (a * z₀⁻¹) :
      ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (1 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
rw :
  HMul.hMul (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) (β := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
      (1 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) z₀ :
        ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) =
    (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) z₀
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) z₀ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) z₀ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
⊢ HMul.hMul (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) (β := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (a * z₀⁻¹) :
        ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) z₀ :
        ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) =
    (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) z₀

Tactic:
rw [this, one_mul]

Premises used: one_mul
-- 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
preimage_one : Membership.mem (γ := Filter K) (𝓝 1) (preimage (β := Γ₀) (⇑v : (a : K) → Γ₀) {1})
V : Set (hat K)
V_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V
hV : ∀ (x : K), (↑x : hat K) ∈ V → Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
V' : Set (hat K)
V'_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V'
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
nhds_right : (fun (x : hat K) ↦ x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : (↑z₀ : hat K) = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne :
  Ne.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) z₀ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (0 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
a : K
y : hat K
y_in : y ∈ V'
ha : Eq (α := hat K) (↑a : hat K) ((fun (x : hat K) ↦ x * x₀) y)
this :
  Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (a * z₀⁻¹) :
      ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (1 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
a₁ :
  Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) a : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (a * z₀⁻¹ * z₀) :
      ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
a₂ :
  HMul.hMul (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) (β := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (a * z₀⁻¹) :
        ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) z₀ :
        ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) =
    (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) z₀
⊢ Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) a : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) z₀ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))

Tactic:
calc
      v.restrict a = v.restrict (a * z₀⁻¹ * z₀) := by rw [mul_assoc, inv_mul_cancel₀ z₀_ne, mul_one]
      _ = v.restrict (a * z₀⁻¹) * v.restrict z₀ := Valuation.map_mul _ _ _
      _ = v.restrict z₀ := by rw [this, one_mul]

Premises used: HMul.hMul, Valued.v, Valuation.map_mul, Inv.inv, DFunLike.coe, 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 : K
⊢ Eq (α := ValueGroup₀ (F := Valuation K Γ₀) v) (extension (↑x : hat K))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x)

Tactic:
Completion.isDenseInducing_coe.extend_eq_of_tendsto ?_

Premises used: Set.Mem, setOf, IsDenseInducing.extend_eq_of_tendsto, Valued.extension, UniformSpace.Completion.isDenseInducing_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 : K
refine :
  Tendsto.{u_1, u_2} (β := ValueGroup₀ (F := Valuation K Γ₀) v)
    ((⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) :
      (a : K) → ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (Filter.comap (β := hat K) Completion.coe' (𝓝 (↑x : hat K)))
    (𝓝 ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x) :
      Filter (ValueGroup₀ (F := Valuation K Γ₀) v))
⊢ Eq (α := ValueGroup₀ (F := Valuation K Γ₀) v) (extension (↑x : hat K))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x)

Tactic:
refine Completion.isDenseInducing_coe.extend_eq_of_tendsto ?_

Premises used: IsDenseInducing.extend_eq_of_tendsto, UniformSpace.Completion.isDenseInducing_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 : K
rw :
  Tendsto.{u_1, u_2} (β := ValueGroup₀ (F := Valuation K Γ₀) v)
    ((⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) :
      (a : K) → ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (𝓝 x)
    (𝓝 ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x) :
      Filter (ValueGroup₀ (F := Valuation K Γ₀) v))
⊢ Tendsto.{u_1, u_2} (β := ValueGroup₀ (F := Valuation K Γ₀) v)
    ((⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) :
      (a : K) → ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (Filter.comap (β := hat K) Completion.coe' (𝓝 (↑x : hat K)))
    (𝓝 ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x) :
      Filter (ValueGroup₀ (F := Valuation K Γ₀) v))

Tactic:
rw [← Completion.isDenseInducing_coe.nhds_eq_comap]

Premises used: IsDenseInducing.nhds_eq_comap, UniformSpace.Completion.isDenseInducing_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 : K
⊢ Tendsto.{u_1, u_2} (β := ValueGroup₀ (F := Valuation K Γ₀) v)
    ((⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) :
      (a : K) → ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (𝓝 x)
    (𝓝 ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x) :
      Filter (ValueGroup₀ (F := Valuation K Γ₀) v))

Tactic:
Valued.continuous_valuation.continuousAt

Premises used: Set.Mem, ContinuousAt, MonoidWithZeroHomClass.toMonoidWithZeroHom, Valued.continuous_valuation, setOf, Continuous.continuousAt
-- 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
⊢ Tendsto.{u_1, u_2} (β := ValueGroup₀ (F := Valuation K Γ₀) v)
    ((⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) :
      (a : K) → ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (𝓝 x)
    (𝓝 ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x) :
      Filter (ValueGroup₀ (F := Valuation K Γ₀) v))

Tactic:
exact Valued.continuous_valuation.continuousAt

Premises used: Valued.continuous_valuation, Continuous.continuousAt
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
rw : Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension 0) : Γ₀) (0 : Γ₀)
rw₁ : Eq (α := ValueGroup₀ (F := Valuation K Γ₀) v) (extension 0) 0
rw₂ :
  Eq (α := ValueGroup₀ (F := Valuation K Γ₀) v) (extension 0)
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) 0)
rw₃ : Eq (α := ValueGroup₀ (F := Valuation K Γ₀) v) (extension 0) (extension (↑0 : hat K))
rw₄ rw₅ : Eq (α := ValueGroup₀ (F := Valuation K Γ₀) v) (extension 0) (extension 0)
⊢ Eq (α := Γ₀)
    (Function.comp.{u_1 + 1, u_2 + 1, u_2 + 1} (α := hat K) (⇑embedding : (a : ValueGroup₀ v) → Γ₀) extension 0) 0

Tactic:
rw [Function.comp_apply, map_eq_zero, ← v.restrict.map_zero (R := K),
      ← Valued.extension_extends (0 : K), Completion.coe_zero]

Premises used: Valued.extension_extends, Valued.v, map_eq_zero, UniformSpace.Completion.coe_zero, Function.comp_apply, OfNat.ofNat, Valuation.map_zero, 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 Γ₀
rw : Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension 1) : Γ₀) (1 : Γ₀)
rw₁ : Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension (↑1 : hat K)) : Γ₀) (1 : Γ₀)
rw₂ :
  Eq (α := Γ₀)
    ((embedding : (a : ValueGroup₀ v) → Γ₀) ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) 1) : Γ₀)
    (1 : Γ₀)
rw₃ : Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) 1 : Γ₀) (1 : Γ₀)
rw₄ rw₅ : Eq.{u_2 + 1} (α := Γ₀) 1 1
⊢ Eq (α := Γ₀)
    (Function.comp.{u_1 + 1, u_2 + 1, u_2 + 1} (α := hat K) (⇑embedding : (a : ValueGroup₀ v) → Γ₀) extension 1) 1

Tactic:
rw [Function.comp_apply, ← Completion.coe_one, Valued.extension_extends (1 : K),
      Valuation.map_one _, map_one]

Premises used: Valued.extension_extends, Valuation.map_one, map_one, Function.comp_apply, OfNat.ofNat, UniformSpace.Completion.coe_one
-- 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
simp :
  Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension (x * y)) : Γ₀)
    ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension x * extension y) : Γ₀)
⊢ ((⇑embedding : (a : ValueGroup₀ v) → Γ₀) ∘ extension) (x * y) =
    HMul.hMul (α := Γ₀) (((⇑embedding : (a : ValueGroup₀ v) → Γ₀) ∘ extension) x)
      (((⇑embedding : (a : ValueGroup₀ v) → Γ₀) ∘ extension) y)

Tactic:
simp only [Function.comp_apply, ← map_mul]

Premises used: map_mul, Function.comp_apply
-- 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
rw : extension (x * y) = extension x * extension y
⊢ Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension (x * y)) : Γ₀)
    ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension x * extension y) : Γ₀)

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 y : hat K
hp : IsClosed.{u_1} (X := hat K × hat K) {x : hat K × hat K | extension (x.1 * x.2) = extension x.1 * extension x.2}
ih :
  ∀ (a b : K),
    extension (HMul.hMul (α := hat K) (↑a : hat K) (↑b : hat K)) =
      HMul.hMul (α := ValueGroup₀ (F := Valuation K Γ₀) v) (extension (↑a : hat K)) (extension (↑b : hat K))
⊢ extension (x * y) = extension x * extension y

Tactic:
apply Completion.induction_on₂ x y
      (p := fun x y => extension (x * y) = extension x * extension y)

Premises used: UniformSpace.Completion.induction_on₂
-- 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} (Y := ValueGroup₀ (F := Valuation K Γ₀) v) fun (x : hat K × hat K) ↦ extension (x.1 * x.2)

Tactic:
have c1 : Continuous fun x : hat K × hat K => Valued.extension (x.1 * x.2) :=
        Valued.continuous_extension.comp (continuous_fst.mul continuous_snd)
-- 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
c1 : Continuous.{u_1, u_2} (Y := ValueGroup₀ (F := Valuation K Γ₀) v) fun (x : hat K × hat K) ↦ extension (x.1 * x.2)
⊢ Continuous.{u_1, u_2} (Y := ValueGroup₀ (F := Valuation K Γ₀) v) fun (x : hat K × hat K) ↦
    extension x.1 * extension x.2

Tactic:
have c2 : Continuous fun x : hat K × hat K => Valued.extension x.1 * Valued.extension x.2 :=
        (Valued.continuous_extension.comp continuous_fst).mul
          (Valued.continuous_extension.comp continuous_snd)
-- 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
c1 : Continuous.{u_1, u_2} (Y := ValueGroup₀ (F := Valuation K Γ₀) v) fun (x : hat K × hat K) ↦ extension (x.1 * x.2)
c2 :
  Continuous.{u_1, u_2} (Y := ValueGroup₀ (F := Valuation K Γ₀) v) fun (x : hat K × hat K) ↦
    extension x.1 * extension x.2
⊢ IsClosed.{u_1} (X := hat K × hat K) {x : hat K × hat K | extension (x.1 * x.2) = extension x.1 * extension x.2}

Tactic:
isClosed_eq c1 c2

Premises used: isClosed_eq
-- 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
c1 : Continuous.{u_1, u_2} (Y := ValueGroup₀ (F := Valuation K Γ₀) v) fun (x : hat K × hat K) ↦ extension (x.1 * x.2)
c2 :
  Continuous.{u_1, u_2} (Y := ValueGroup₀ (F := Valuation K Γ₀) v) fun (x : hat K × hat K) ↦
    extension x.1 * extension x.2
⊢ IsClosed.{u_1} (X := hat K × hat K) {x : hat K × hat K | extension (x.1 * x.2) = extension x.1 * extension x.2}

Tactic:
exact isClosed_eq c1 c2

Premises used: isClosed_eq
-- 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 :
  (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (x * y) =
    HMul.hMul (α := ValueGroup₀ (F := Valuation K Γ₀) v) (β := ValueGroup₀ (F := Valuation K Γ₀) v)
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) y : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
⊢ extension (HMul.hMul (α := hat K) (↑x : hat K) (↑y : hat K)) =
    HMul.hMul (α := ValueGroup₀ (F := Valuation K Γ₀) v) (extension (↑x : 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
⊢ (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (x * y) =
    HMul.hMul (α := ValueGroup₀ (F := Valuation K Γ₀) v) (β := ValueGroup₀ (F := Valuation K Γ₀) v)
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) y : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))

Tactic:
Valuation.map_mul _ _ _

Premises used: Set.Mem, setOf, Valuation.map_mul
-- 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
⊢ (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (x * y) =
    HMul.hMul (α := ValueGroup₀ (F := Valuation K Γ₀) v) (β := ValueGroup₀ (F := Valuation K Γ₀) v)
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) y : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))

Tactic:
exact Valuation.map_mul _ _ _

Premises used: Valuation.map_mul
-- 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
simp_rw :
  LE.le (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension (x + y)) : Γ₀)
      ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension x) : Γ₀) ∨
    LE.le (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension (x + y)) : Γ₀)
      ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension y) : Γ₀)
⊢ LE.le (α := Γ₀) (((⇑embedding : (a : ValueGroup₀ v) → Γ₀) ∘ extension) (x + y))
    (max (((⇑embedding : (a : ValueGroup₀ v) → Γ₀) ∘ extension) x)
      (((⇑embedding : (a : ValueGroup₀ v) → Γ₀) ∘ extension) y))

Tactic:
simp_rw [le_max_iff, Function.comp_apply]

Premises used: Function.comp_apply, le_max_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 y : hat K
rw : extension (x + y) ≤ extension x ∨ extension (x + y) ≤ extension y
⊢ LE.le (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension (x + y)) : Γ₀)
      ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension x) : Γ₀) ∨
    LE.le (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension (x + y)) : Γ₀)
      ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension y) : Γ₀)

Tactic:
rw [embedding_strictMono.le_iff_le, embedding_strictMono.le_iff_le (f := embedding)]

Premises used: StrictMono.le_iff_le
-- 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
hp :
  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}
ih :
  ∀ (a b : K),
    extension (HAdd.hAdd (α := hat K) (↑a : hat K) (↑b : hat K)) ≤ extension (↑a : hat K) ∨
      extension (HAdd.hAdd (α := hat K) (↑a : hat K) (↑b : hat K)) ≤ extension (↑b : hat K)
⊢ extension (x + y) ≤ extension x ∨ extension (x + y) ≤ extension y

Tactic:
apply Completion.induction_on₂ x y
      (p := fun x y => extension (x + y) ≤ extension x ∨ extension (x + y) ≤ extension y)

Premises used: UniformSpace.Completion.induction_on₂