awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
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 →*₀ Γ₀))
⊢ 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 →*₀ Γ₀))
have 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 →*₀ Γ₀))
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]
-- 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
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 →*₀ Γ₀))
⊢ 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 →*₀ Γ₀))
have 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₀
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]
-- 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
⊢ Eq (α := ValueGroup₀ (F := Valuation K Γ₀) v) (extension (↑x : hat K))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x)
have 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))
Tactic: refine Completion.isDenseInducing_coe.extend_eq_of_tendsto ?_
-- 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
⊢ 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))
have 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))
Tactic: rw [← Completion.isDenseInducing_coe.nhds_eq_comap]
-- 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 (α := Γ₀)
    (Function.comp.{u_1 + 1, u_2 + 1, u_2 + 1} (α := hat K) (⇑embedding : (a : ValueGroup₀ v) → Γ₀) extension 0) 0
have rw : Eq (α := Γ₀) ((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]
-- 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 Γ₀
rw : Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension 0) : Γ₀) (0 : Γ₀)
⊢ Eq (α := Γ₀)
    (Function.comp.{u_1 + 1, u_2 + 1, u_2 + 1} (α := hat K) (⇑embedding : (a : ValueGroup₀ v) → Γ₀) extension 0) 0
have rw₁ : Eq (α := ValueGroup₀ (F := Valuation K Γ₀) 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]
-- 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 Γ₀
rw : Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension 0) : Γ₀) (0 : Γ₀)
rw₁ : Eq (α := ValueGroup₀ (F := Valuation K Γ₀) v) (extension 0) 0
⊢ Eq (α := Γ₀)
    (Function.comp.{u_1 + 1, u_2 + 1, u_2 + 1} (α := hat K) (⇑embedding : (a : ValueGroup₀ v) → Γ₀) extension 0) 0
have rw₂ : Eq (α := ValueGroup₀ (F := Valuation K Γ₀) v) (extension 0)
  ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) 0)
Tactic: rw [Function.comp_apply, map_eq_zero, ← v.restrict.map_zero (R := K),
      ← Valued.extension_extends (0 : K), Completion.coe_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 Γ₀
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)
⊢ Eq (α := Γ₀)
    (Function.comp.{u_1 + 1, u_2 + 1, u_2 + 1} (α := hat K) (⇑embedding : (a : ValueGroup₀ v) → Γ₀) extension 0) 0
have rw₃ : Eq (α := ValueGroup₀ (F := Valuation K Γ₀) v) (extension 0) (extension (↑0 : hat K))
Tactic: rw [Function.comp_apply, map_eq_zero, ← v.restrict.map_zero (R := K),
      ← Valued.extension_extends (0 : K), Completion.coe_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 Γ₀
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))
⊢ Eq (α := Γ₀)
    (Function.comp.{u_1 + 1, u_2 + 1, u_2 + 1} (α := hat K) (⇑embedding : (a : ValueGroup₀ v) → Γ₀) extension 0) 0
have rw₄ : Eq (α := ValueGroup₀ (F := Valuation K Γ₀) v) (extension 0) (extension 0)
Tactic: rw [Function.comp_apply, map_eq_zero, ← v.restrict.map_zero (R := K),
      ← Valued.extension_extends (0 : K), Completion.coe_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 Γ₀
⊢ Eq (α := Γ₀)
    (Function.comp.{u_1 + 1, u_2 + 1, u_2 + 1} (α := hat K) (⇑embedding : (a : ValueGroup₀ v) → Γ₀) extension 1) 1
have rw : Eq (α := Γ₀) ((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]
-- 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 Γ₀
rw : Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension 1) : Γ₀) (1 : Γ₀)
⊢ Eq (α := Γ₀)
    (Function.comp.{u_1 + 1, u_2 + 1, u_2 + 1} (α := hat K) (⇑embedding : (a : ValueGroup₀ v) → Γ₀) extension 1) 1
have rw₁ : Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension (↑1 : hat K)) : Γ₀) (1 : Γ₀)
Tactic: rw [Function.comp_apply, ← Completion.coe_one, Valued.extension_extends (1 : K),
      Valuation.map_one _, map_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
rw : Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension 1) : Γ₀) (1 : Γ₀)
rw₁ : Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension (↑1 : hat K)) : Γ₀) (1 : Γ₀)
⊢ Eq (α := Γ₀)
    (Function.comp.{u_1 + 1, u_2 + 1, u_2 + 1} (α := hat K) (⇑embedding : (a : ValueGroup₀ v) → Γ₀) extension 1) 1
have rw₂ : Eq (α := Γ₀)
  ((embedding : (a : ValueGroup₀ v) → Γ₀) ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) 1) : Γ₀)
  (1 : Γ₀)
Tactic: rw [Function.comp_apply, ← Completion.coe_one, Valued.extension_extends (1 : K),
      Valuation.map_one _, map_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
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 : Γ₀)
⊢ Eq (α := Γ₀)
    (Function.comp.{u_1 + 1, u_2 + 1, u_2 + 1} (α := hat K) (⇑embedding : (a : ValueGroup₀ v) → Γ₀) extension 1) 1
have rw₃ : Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) 1 : Γ₀) (1 : Γ₀)
Tactic: rw [Function.comp_apply, ← Completion.coe_one, Valued.extension_extends (1 : K),
      Valuation.map_one _, map_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
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 : Γ₀)
⊢ Eq (α := Γ₀)
    (Function.comp.{u_1 + 1, u_2 + 1, u_2 + 1} (α := hat K) (⇑embedding : (a : ValueGroup₀ v) → Γ₀) extension 1) 1
have rw₄ : Eq.{u_2 + 1} (α := Γ₀) 1 1
Tactic: rw [Function.comp_apply, ← Completion.coe_one, Valued.extension_extends (1 : K),
      Valuation.map_one _, map_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x y : hat K
⊢ ((⇑embedding : (a : ValueGroup₀ v) → Γ₀) ∘ extension) (x * y) =
    HMul.hMul (α := Γ₀) (((⇑embedding : (a : ValueGroup₀ v) → Γ₀) ∘ extension) x)
      (((⇑embedding : (a : ValueGroup₀ v) → Γ₀) ∘ extension) y)
have simp : Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension (x * y)) : Γ₀)
  ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension x * extension y) : Γ₀)
Tactic: simp only [Function.comp_apply, ← map_mul]
-- 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 y : hat K
⊢ Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension (x * y)) : Γ₀)
    ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension x * extension y) : Γ₀)
have rw : extension (x * y) = extension x * extension y
Tactic: 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 y : hat K
⊢ extension (x * y) = extension x * extension y
have 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}
Tactic: apply Completion.induction_on₂ x y
      (p := fun x y => extension (x * y) = extension x * extension y)
-- 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 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}
⊢ extension (x * y) = extension x * extension y
have 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))
Tactic: apply Completion.induction_on₂ x y
      (p := fun x y => extension (x * y) = extension x * extension y)
-- 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 y : hat K
⊢ IsClosed.{u_1} (X := hat K × hat K) {x : hat K × hat K | extension (x.1 * x.2) = extension x.1 * extension x.2}
have c1 : 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)
-- 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 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)
⊢ IsClosed.{u_1} (X := hat K × hat K) {x : hat K × hat K | extension (x.1 * x.2) = extension x.1 * extension x.2}
have c2 : 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)
-- 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_1 y_1 : hat K
x y : 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))
have 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 →*₀ Γ₀))
Tactic: norm_cast
-- 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 y : hat K
⊢ LE.le (α := Γ₀) (((⇑embedding : (a : ValueGroup₀ v) → Γ₀) ∘ extension) (x + y))
    (max (((⇑embedding : (a : ValueGroup₀ v) → Γ₀) ∘ extension) x)
      (((⇑embedding : (a : ValueGroup₀ v) → Γ₀) ∘ extension) y))
have 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) : Γ₀)
Tactic: simp_rw [le_max_iff, Function.comp_apply]
-- 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 y : hat K
⊢ 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) : Γ₀)
have rw : extension (x + y) ≤ extension x ∨ extension (x + y) ≤ extension y
Tactic: rw [embedding_strictMono.le_iff_le, embedding_strictMono.le_iff_le (f := embedding)]
-- 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 y : hat K
⊢ extension (x + y) ≤ extension x ∨ extension (x + y) ≤ extension y
have 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}
Tactic: apply Completion.induction_on₂ x y
      (p := fun x y => extension (x + y) ≤ extension x ∨ extension (x + y) ≤ extension y)
-- 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 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}
⊢ extension (x + y) ≤ extension x ∨ extension (x + y) ≤ extension y
have 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)
Tactic: apply Completion.induction_on₂ x y
      (p := fun x y => extension (x + y) ≤ extension x ∨ extension (x + y) ≤ extension y)
-- 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 y : hat K
⊢ 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}
have cont : Continuous.{u_1, u_2} (X := hat K) extension
Tactic: have cont : Continuous (Valued.extension : hat K → _) := Valued.continuous_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_1 y_1 : hat K
x y : 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)
have 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 →*₀ Γ₀))
Tactic: norm_cast
-- 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
⊢ Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) (↑x : hat K) : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
have rw : Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension (↑x : hat K)) : Γ₀) ((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 : Γ₀)
⊢ Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) (↑x : hat K) : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
have rw₁ : Eq (α := Γ₀)
  ((embedding : (a : ValueGroup₀ v) → Γ₀)
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) :
    Γ₀)
  ((v : (a : K) → Γ₀) x : Γ₀)
Tactic: rw [extensionValuation_toFun, extension_extends, Valuation.restrict_def, embedding_restrict₀]