K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ ∀ (b : hat K), ∃ c, Tendsto (↑v) (Filter.comap (↑K) (𝓝 b)) (𝓝 c)
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ Continuous extension
refine' Completion.denseInducing_coe.continuous_extend _
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
⊢ ∃ c, Tendsto (↑v) (Filter.comap (↑K) (𝓝 x₀)) (𝓝 c)
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ ∀ (b : hat K), ∃ c, Tendsto (↑v) (Filter.comap (↑K) (𝓝 b)) (𝓝 c)
intro x₀
case inl
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ ∃ c, Tendsto (↑v) (Filter.comap (↑K) (𝓝 0)) (𝓝 c)

case inr
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
⊢ ∃ c, Tendsto (↑v) (Filter.comap (↑K) (𝓝 x₀)) (𝓝 c)
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
⊢ ∃ c, Tendsto (↑v) (Filter.comap (↑K) (𝓝 x₀)) (𝓝 c)
rcases eq_or_ne x₀ 0 with (rfl | h)
case inl
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ Tendsto (↑v) (Filter.comap (↑K) (𝓝 0)) (𝓝 0)
case inl
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ ∃ c, Tendsto (↑v) (Filter.comap (↑K) (𝓝 0)) (𝓝 c)
refine' ⟨0, _⟩
case inl
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ Tendsto (↑v) (𝓝 0) (𝓝 0)
case inl
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ Tendsto (↑v) (Filter.comap (↑K) (𝓝 0)) (𝓝 0)
erw [← Completion.denseInducing_coe.toInducing.nhds_eq_comap]
no goals
case inl
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ Tendsto (↑v) (𝓝 0) (𝓝 0)
exact Valued.continuous_valuation.tendsto' 0 0 (map_zero v)
case inr
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
⊢ ∃ c, Tendsto (↑v) (Filter.comap (↑K) (𝓝 x₀)) (𝓝 c)
case inr
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
⊢ ∃ c, Tendsto (↑v) (Filter.comap (↑K) (𝓝 x₀)) (𝓝 c)
have preimage_one : v ⁻¹' {(1 : Γ₀)} ∈ 𝓝 (1 : K) := by
  have : (v (1 : K) : Γ₀) ≠ 0 := by
    rw [Valuation.map_one]
    exact zero_ne_one.symm
  convert Valued.loc_const this
  ext x
  rw [Valuation.map_one, mem_preimage, mem_singleton_iff, mem_setOf_eq]
case inr.intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
⊢ ∃ c, Tendsto (↑v) (Filter.comap (↑K) (𝓝 x₀)) (𝓝 c)
case inr
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
⊢ ∃ c, Tendsto (↑v) (Filter.comap (↑K) (𝓝 x₀)) (𝓝 c)
obtain ⟨V, V_in, hV⟩ : ∃ V ∈ 𝓝 (1 : hat K), ∀ x : K, (x : hat K) ∈ V → (v x : Γ₀) = 1 := by
  rwa [Completion.denseInducing_coe.nhds_eq_comap, mem_comap] at preimage_one
case inr.intro.intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
⊢ ∃ c, Tendsto (↑v) (Filter.comap (↑K) (𝓝 x₀)) (𝓝 c)
case inr.intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
this : ∃ V', V' ∈ 𝓝 1 ∧ ¬0 ∈ V' ∧ ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
⊢ ∃ c, Tendsto (↑v) (Filter.comap (↑K) (𝓝 x₀)) (𝓝 c)
rcases this with ⟨V', V'_in, zeroV', hV'⟩
case inr.intro.intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
⊢ ∃ c, Tendsto (↑v) (Filter.comap (↑K) (𝓝 x₀)) (𝓝 c)
case inr.intro.intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
⊢ ∃ c, Tendsto (↑v) (Filter.comap (↑K) (𝓝 x₀)) (𝓝 c)
have nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀ := by
  have l : Function.LeftInverse (fun x : hat K => x * x₀⁻¹) fun x : hat K => x * x₀ := by
    intro x
    simp only [mul_assoc, mul_inv_cancel h, mul_one]
  have r : Function.RightInverse (fun x : hat K => x * x₀⁻¹) fun x : hat K => x * x₀ := by
    intro x
    simp only [mul_assoc, inv_mul_cancel h, mul_one]
  have c : Continuous fun x : hat K => x * x₀⁻¹ := continuous_id.mul continuous_const
  rw [image_eq_preimage_of_inverse l r]
  rw [← mul_inv_cancel h] at V'_in
  exact c.continuousAt V'_in
case inr.intro.intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
this : ∃ z₀ y₀, y₀ ∈ V' ∧ ↑K z₀ = y₀ * x₀ ∧ z₀ ≠ 0
⊢ ∃ c, Tendsto (↑v) (Filter.comap (↑K) (𝓝 x₀)) (𝓝 c)
case inr.intro.intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
⊢ ∃ c, Tendsto (↑v) (Filter.comap (↑K) (𝓝 x₀)) (𝓝 c)
have : ∃ z₀ : K, ∃ y₀ ∈ V', ↑z₀ = y₀ * x₀ ∧ z₀ ≠ 0 := by
  rcases Completion.denseRange_coe.mem_nhds nhds_right with ⟨z₀, y₀, y₀_in, H : y₀ * x₀ = z₀⟩
  refine' ⟨z₀, y₀, y₀_in, ⟨H.symm, _⟩⟩
  rintro rfl
  exact mul_ne_zero (ne_of_mem_of_not_mem y₀_in zeroV') h H
case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑K z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
⊢ ∃ c, Tendsto (↑v) (Filter.comap (↑K) (𝓝 x₀)) (𝓝 c)
case inr.intro.intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
this : ∃ z₀ y₀, y₀ ∈ V' ∧ ↑K z₀ = y₀ * x₀ ∧ z₀ ≠ 0
⊢ ∃ c, Tendsto (↑v) (Filter.comap (↑K) (𝓝 x₀)) (𝓝 c)
rcases this with ⟨z₀, y₀, y₀_in, hz₀, z₀_ne⟩
case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑K z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : ↑v z₀ ≠ 0
⊢ ∃ c, Tendsto (↑v) (Filter.comap (↑K) (𝓝 x₀)) (𝓝 c)
case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑K z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
⊢ ∃ c, Tendsto (↑v) (Filter.comap (↑K) (𝓝 x₀)) (𝓝 c)
have vz₀_ne : (v z₀ : Γ₀) ≠ 0 := by rwa [Valuation.ne_zero_iff]
case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑K z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : ↑v z₀ ≠ 0
⊢ Tendsto (↑v) (Filter.comap (↑K) (𝓝 x₀)) (𝓝 (↑v z₀))
case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑K z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : ↑v z₀ ≠ 0
⊢ ∃ c, Tendsto (↑v) (Filter.comap (↑K) (𝓝 x₀)) (𝓝 c)
refine' ⟨v z₀, _⟩
case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑K z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : ↑v z₀ ≠ 0
⊢ ∀ᶠ (b : hat K) in 𝓝 x₀, ∀ (a : K), ↑K a = b → ↑v a = ↑v z₀
case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑K z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : ↑v z₀ ≠ 0
⊢ Tendsto (↑v) (Filter.comap (↑K) (𝓝 x₀)) (𝓝 (↑v z₀))
rw [WithZeroTopology.tendsto_of_ne_zero vz₀_ne, eventually_comap]
case h
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑K z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : ↑v z₀ ≠ 0
x : hat K
x_in : x ∈ (fun x => x * x₀) '' V'
a : K
ha : ↑K a = x
⊢ ↑v a = ↑v z₀
case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑K z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : ↑v z₀ ≠ 0
⊢ ∀ᶠ (b : hat K) in 𝓝 x₀, ∀ (a : K), ↑K a = b → ↑v a = ↑v z₀
filter_upwards [nhds_right]with x x_in a ha
case h.intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑K z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : ↑v z₀ ≠ 0
a : K
y : hat K
y_in : y ∈ V'
ha : ↑K a = (fun x => x * x₀) y
⊢ ↑v a = ↑v z₀
case h
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑K z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : ↑v z₀ ≠ 0
x : hat K
x_in : x ∈ (fun x => x * x₀) '' V'
a : K
ha : ↑K a = x
⊢ ↑v a = ↑v z₀
rcases x_in with ⟨y, y_in, rfl⟩
case h.intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑K z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : ↑v z₀ ≠ 0
a : K
y : hat K
y_in : y ∈ V'
ha : ↑K a = (fun x => x * x₀) y
this : ↑v (a * z₀⁻¹) = 1
⊢ ↑v a = ↑v z₀
case h.intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑K z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : ↑v z₀ ≠ 0
a : K
y : hat K
y_in : y ∈ V'
ha : ↑K a = (fun x => x * x₀) y
⊢ ↑v a = ↑v z₀
have : (v (a * z₀⁻¹) : Γ₀) = 1 := by
  apply hV
  have : (z₀⁻¹ : K) = (z₀ : hat K)⁻¹ := map_inv₀ (Completion.coeRingHom : K →+* hat K) z₀
  rw [Completion.coe_mul, this, ha, hz₀, mul_inv, mul_comm y₀⁻¹, ← mul_assoc, mul_assoc y,
    mul_inv_cancel h, mul_one]
  solve_by_elim
no goals
case h.intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑K z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : ↑v z₀ ≠ 0
a : K
y : hat K
y_in : y ∈ V'
ha : ↑K a = (fun x => x * x₀) y
this : ↑v (a * z₀⁻¹) = 1
⊢ ↑v a = ↑v z₀
calc
  v a = v (a * z₀⁻¹ * z₀) := by rw [mul_assoc, inv_mul_cancel z₀_ne, mul_one]
  _ = v (a * z₀⁻¹) * v z₀ := (Valuation.map_mul _ _ _)
  _ = v z₀ := by rw [this, one_mul]
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
this : ↑v 1 ≠ 0
⊢ ↑v ⁻¹' {1} ∈ 𝓝 1
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
⊢ ↑v ⁻¹' {1} ∈ 𝓝 1
have : (v (1 : K) : Γ₀) ≠ 0 := by
  rw [Valuation.map_one]
  exact zero_ne_one.symm
case h.e'_4
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
this : ↑v 1 ≠ 0
⊢ ↑v ⁻¹' {1} = {y | ↑v y = ↑v 1}
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
this : ↑v 1 ≠ 0
⊢ ↑v ⁻¹' {1} ∈ 𝓝 1
convert Valued.loc_const this
case h.e'_4.h
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
this : ↑v 1 ≠ 0
x : K
⊢ x ∈ ↑v ⁻¹' {1} ↔ x ∈ {y | ↑v y = ↑v 1}
case h.e'_4
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
this : ↑v 1 ≠ 0
⊢ ↑v ⁻¹' {1} = {y | ↑v y = ↑v 1}
ext x
no goals
case h.e'_4.h
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
this : ↑v 1 ≠ 0
x : K
⊢ x ∈ ↑v ⁻¹' {1} ↔ x ∈ {y | ↑v y = ↑v 1}
rw [Valuation.map_one, mem_preimage, mem_singleton_iff, mem_setOf_eq]
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
⊢ 1 ≠ 0
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
⊢ ↑v 1 ≠ 0
rw [Valuation.map_one]
no goals
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
⊢ 1 ≠ 0
exact zero_ne_one.symm
no goals
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
⊢ ∃ V, V ∈ 𝓝 1 ∧ ∀ (x : K), ↑K x ∈ V → ↑v x = 1
rwa [Completion.denseInducing_coe.nhds_eq_comap, mem_comap] at preimage_one
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
this : Tendsto (fun p => p.fst * p.snd⁻¹) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
⊢ ∃ V', V' ∈ 𝓝 1 ∧ ¬0 ∈ V' ∧ ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
⊢ ∃ V', V' ∈ 𝓝 1 ∧ ¬0 ∈ V' ∧ ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
have : Tendsto (fun p : hat K × hat K => p.1 * p.2⁻¹) ((𝓝 1) ×ˢ (𝓝 1)) (𝓝 1) := by
  rw [← nhds_prod_eq]
  conv =>
    congr
    rfl
    rfl
    rw [← one_mul (1 : hat K)]
  refine'
    Tendsto.mul continuous_fst.continuousAt (Tendsto.comp _ continuous_snd.continuousAt)
  convert continuousAt_inv₀ (zero_ne_one.symm : 1 ≠ (0 : hat K))
  rw [ContinuousAt._eq_1, inv_one]
case intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
this : Tendsto (fun p => p.fst * p.snd⁻¹) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
U : Set (hat K)
U_in : U ∈ 𝓝 1
hU : ∀ (x x' : hat K), x ∈ U → x' ∈ U → (x, x').fst * (x, x').snd⁻¹ ∈ V
⊢ ∃ V', V' ∈ 𝓝 1 ∧ ¬0 ∈ V' ∧ ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
this : Tendsto (fun p => p.fst * p.snd⁻¹) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
⊢ ∃ V', V' ∈ 𝓝 1 ∧ ¬0 ∈ V' ∧ ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
rcases tendsto_prod_self_iff.mp this V V_in with ⟨U, U_in, hU⟩
case intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
this : Tendsto (fun p => p.fst * p.snd⁻¹) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
U : Set (hat K)
U_in : U ∈ 𝓝 1
hU : ∀ (x x' : hat K), x ∈ U → x' ∈ U → (x, x').fst * (x, x').snd⁻¹ ∈ V
hatKstar : Set (hat K) := {0}ᶜ
⊢ ∃ V', V' ∈ 𝓝 1 ∧ ¬0 ∈ V' ∧ ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
case intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
this : Tendsto (fun p => p.fst * p.snd⁻¹) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
U : Set (hat K)
U_in : U ∈ 𝓝 1
hU : ∀ (x x' : hat K), x ∈ U → x' ∈ U → (x, x').fst * (x, x').snd⁻¹ ∈ V
⊢ ∃ V', V' ∈ 𝓝 1 ∧ ¬0 ∈ V' ∧ ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
let hatKstar := ({0}ᶜ : Set <| hat K)
case intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
this✝ : Tendsto (fun p => p.fst * p.snd⁻¹) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
U : Set (hat K)
U_in : U ∈ 𝓝 1
hU : ∀ (x x' : hat K), x ∈ U → x' ∈ U → (x, x').fst * (x, x').snd⁻¹ ∈ V
hatKstar : Set (hat K) := {0}ᶜ
this : hatKstar ∈ 𝓝 1
⊢ ∃ V', V' ∈ 𝓝 1 ∧ ¬0 ∈ V' ∧ ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
case intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
this : Tendsto (fun p => p.fst * p.snd⁻¹) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
U : Set (hat K)
U_in : U ∈ 𝓝 1
hU : ∀ (x x' : hat K), x ∈ U → x' ∈ U → (x, x').fst * (x, x').snd⁻¹ ∈ V
hatKstar : Set (hat K) := {0}ᶜ
⊢ ∃ V', V' ∈ 𝓝 1 ∧ ¬0 ∈ V' ∧ ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
have : hatKstar ∈ 𝓝 (1 : hat K) := compl_singleton_mem_nhds zero_ne_one.symm
case intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
this✝ : Tendsto (fun p => p.fst * p.snd⁻¹) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
U : Set (hat K)
U_in : U ∈ 𝓝 1
hU : ∀ (x x' : hat K), x ∈ U → x' ∈ U → (x, x').fst * (x, x').snd⁻¹ ∈ V
hatKstar : Set (hat K) := {0}ᶜ
this : hatKstar ∈ 𝓝 1
⊢ ¬0 ∈ U ∩ hatKstar ∧ ∀ (x : hat K), x ∈ U ∩ hatKstar → ∀ (y : hat K), y ∈ U ∩ hatKstar → x * y⁻¹ ∈ V
case intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
this✝ : Tendsto (fun p => p.fst * p.snd⁻¹) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
U : Set (hat K)
U_in : U ∈ 𝓝 1
hU : ∀ (x x' : hat K), x ∈ U → x' ∈ U → (x, x').fst * (x, x').snd⁻¹ ∈ V
hatKstar : Set (hat K) := {0}ᶜ
this : hatKstar ∈ 𝓝 1
⊢ ∃ V', V' ∈ 𝓝 1 ∧ ¬0 ∈ V' ∧ ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
use U ∩ hatKstar, Filter.inter_mem U_in this
case intro.intro.left
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
this✝ : Tendsto (fun p => p.fst * p.snd⁻¹) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
U : Set (hat K)
U_in : U ∈ 𝓝 1
hU : ∀ (x x' : hat K), x ∈ U → x' ∈ U → (x, x').fst * (x, x').snd⁻¹ ∈ V
hatKstar : Set (hat K) := {0}ᶜ
this : hatKstar ∈ 𝓝 1
⊢ ¬0 ∈ U ∩ hatKstar

case intro.intro.right
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
this✝ : Tendsto (fun p => p.fst * p.snd⁻¹) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
U : Set (hat K)
U_in : U ∈ 𝓝 1
hU : ∀ (x x' : hat K), x ∈ U → x' ∈ U → (x, x').fst * (x, x').snd⁻¹ ∈ V
hatKstar : Set (hat K) := {0}ᶜ
this : hatKstar ∈ 𝓝 1
⊢ ∀ (x : hat K), x ∈ U ∩ hatKstar → ∀ (y : hat K), y ∈ U ∩ hatKstar → x * y⁻¹ ∈ V
case intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
this✝ : Tendsto (fun p => p.fst * p.snd⁻¹) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
U : Set (hat K)
U_in : U ∈ 𝓝 1
hU : ∀ (x x' : hat K), x ∈ U → x' ∈ U → (x, x').fst * (x, x').snd⁻¹ ∈ V
hatKstar : Set (hat K) := {0}ᶜ
this : hatKstar ∈ 𝓝 1
⊢ ¬0 ∈ U ∩ hatKstar ∧ ∀ (x : hat K), x ∈ U ∩ hatKstar → ∀ (y : hat K), y ∈ U ∩ hatKstar → x * y⁻¹ ∈ V
constructor
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
⊢ Tendsto (fun p => p.fst * p.snd⁻¹) (𝓝 (1, 1)) (𝓝 1)
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
⊢ Tendsto (fun p => p.fst * p.snd⁻¹) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
rw [← nhds_prod_eq]
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
⊢ Tendsto (fun p => p.fst * p.snd⁻¹) (𝓝 (1, 1)) (𝓝 (1 * 1))
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
⊢ Tendsto (fun p => p.fst * p.snd⁻¹) (𝓝 (1, 1)) (𝓝 1)
conv =>
  congr
  rfl
  rfl
  rw [← one_mul (1 : hat K)]
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
⊢ Tendsto Inv.inv (𝓝 (1, 1).snd) (𝓝 1)
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
⊢ Tendsto (fun p => p.fst * p.snd⁻¹) (𝓝 (1, 1)) (𝓝 (1 * 1))
refine'
  Tendsto.mul continuous_fst.continuousAt (Tendsto.comp _ continuous_snd.continuousAt)
case a
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
⊢ Tendsto Inv.inv (𝓝 (1, 1).snd) (𝓝 1) ↔ ContinuousAt Inv.inv 1
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
⊢ Tendsto Inv.inv (𝓝 (1, 1).snd) (𝓝 1)
convert continuousAt_inv₀ (zero_ne_one.symm : 1 ≠ (0 : hat K))
no goals
case a
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
⊢ Tendsto Inv.inv (𝓝 (1, 1).snd) (𝓝 1) ↔ ContinuousAt Inv.inv 1
rw [ContinuousAt._eq_1, inv_one]
case intro.intro.left.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
this✝ : Tendsto (fun p => p.fst * p.snd⁻¹) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
U : Set (hat K)
U_in : U ∈ 𝓝 1
hU : ∀ (x x' : hat K), x ∈ U → x' ∈ U → (x, x').fst * (x, x').snd⁻¹ ∈ V
hatKstar : Set (hat K) := {0}ᶜ
this : hatKstar ∈ 𝓝 1
left✝ : 0 ∈ U
h' : 0 ∈ hatKstar
⊢ False
case intro.intro.left
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
this✝ : Tendsto (fun p => p.fst * p.snd⁻¹) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
U : Set (hat K)
U_in : U ∈ 𝓝 1
hU : ∀ (x x' : hat K), x ∈ U → x' ∈ U → (x, x').fst * (x, x').snd⁻¹ ∈ V
hatKstar : Set (hat K) := {0}ᶜ
this : hatKstar ∈ 𝓝 1
⊢ ¬0 ∈ U ∩ hatKstar
rintro ⟨_, h'⟩
case intro.intro.left.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
this✝ : Tendsto (fun p => p.fst * p.snd⁻¹) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
U : Set (hat K)
U_in : U ∈ 𝓝 1
hU : ∀ (x x' : hat K), x ∈ U → x' ∈ U → (x, x').fst * (x, x').snd⁻¹ ∈ V
hatKstar : Set (hat K) := {0}ᶜ
this : hatKstar ∈ 𝓝 1
left✝ : 0 ∈ U
h' : 0 ≠ 0
⊢ False
case intro.intro.left.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
this✝ : Tendsto (fun p => p.fst * p.snd⁻¹) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
U : Set (hat K)
U_in : U ∈ 𝓝 1
hU : ∀ (x x' : hat K), x ∈ U → x' ∈ U → (x, x').fst * (x, x').snd⁻¹ ∈ V
hatKstar : Set (hat K) := {0}ᶜ
this : hatKstar ∈ 𝓝 1
left✝ : 0 ∈ U
h' : 0 ∈ hatKstar
⊢ False
rw [mem_compl_singleton_iff] at h'
no goals
case intro.intro.left.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
this✝ : Tendsto (fun p => p.fst * p.snd⁻¹) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
U : Set (hat K)
U_in : U ∈ 𝓝 1
hU : ∀ (x x' : hat K), x ∈ U → x' ∈ U → (x, x').fst * (x, x').snd⁻¹ ∈ V
hatKstar : Set (hat K) := {0}ᶜ
this : hatKstar ∈ 𝓝 1
left✝ : 0 ∈ U
h' : 0 ≠ 0
⊢ False
exact h' rfl
case intro.intro.right.intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
this✝ : Tendsto (fun p => p.fst * p.snd⁻¹) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
U : Set (hat K)
U_in : U ∈ 𝓝 1
hU : ∀ (x x' : hat K), x ∈ U → x' ∈ U → (x, x').fst * (x, x').snd⁻¹ ∈ V
hatKstar : Set (hat K) := {0}ᶜ
this : hatKstar ∈ 𝓝 1
x : hat K
hx : x ∈ U
right✝¹ : x ∈ hatKstar
y : hat K
hy : y ∈ U
right✝ : y ∈ hatKstar
⊢ x * y⁻¹ ∈ V
case intro.intro.right
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
this✝ : Tendsto (fun p => p.fst * p.snd⁻¹) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
U : Set (hat K)
U_in : U ∈ 𝓝 1
hU : ∀ (x x' : hat K), x ∈ U → x' ∈ U → (x, x').fst * (x, x').snd⁻¹ ∈ V
hatKstar : Set (hat K) := {0}ᶜ
this : hatKstar ∈ 𝓝 1
⊢ ∀ (x : hat K), x ∈ U ∩ hatKstar → ∀ (y : hat K), y ∈ U ∩ hatKstar → x * y⁻¹ ∈ V
rintro x ⟨hx, _⟩ y ⟨hy, _⟩
no goals
case intro.intro.right.intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
this✝ : Tendsto (fun p => p.fst * p.snd⁻¹) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
U : Set (hat K)
U_in : U ∈ 𝓝 1
hU : ∀ (x x' : hat K), x ∈ U → x' ∈ U → (x, x').fst * (x, x').snd⁻¹ ∈ V
hatKstar : Set (hat K) := {0}ᶜ
this : hatKstar ∈ 𝓝 1
x : hat K
hx : x ∈ U
right✝¹ : x ∈ hatKstar
y : hat K
hy : y ∈ U
right✝ : y ∈ hatKstar
⊢ x * y⁻¹ ∈ V
apply hU <;> assumption
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
l : Function.LeftInverse (fun x => x * x₀⁻¹) fun x => x * x₀
⊢ (fun x => x * x₀) '' V' ∈ 𝓝 x₀
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
⊢ (fun x => x * x₀) '' V' ∈ 𝓝 x₀
have l : Function.LeftInverse (fun x : hat K => x * x₀⁻¹) fun x : hat K => x * x₀ := by
  intro x
  simp only [mul_assoc, mul_inv_cancel h, mul_one]
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
l : Function.LeftInverse (fun x => x * x₀⁻¹) fun x => x * x₀
r : Function.RightInverse (fun x => x * x₀⁻¹) fun x => x * x₀
⊢ (fun x => x * x₀) '' V' ∈ 𝓝 x₀
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
l : Function.LeftInverse (fun x => x * x₀⁻¹) fun x => x * x₀
⊢ (fun x => x * x₀) '' V' ∈ 𝓝 x₀
have r : Function.RightInverse (fun x : hat K => x * x₀⁻¹) fun x : hat K => x * x₀ := by
  intro x
  simp only [mul_assoc, inv_mul_cancel h, mul_one]
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
l : Function.LeftInverse (fun x => x * x₀⁻¹) fun x => x * x₀
r : Function.RightInverse (fun x => x * x₀⁻¹) fun x => x * x₀
c : Continuous fun x => x * x₀⁻¹
⊢ (fun x => x * x₀) '' V' ∈ 𝓝 x₀
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
l : Function.LeftInverse (fun x => x * x₀⁻¹) fun x => x * x₀
r : Function.RightInverse (fun x => x * x₀⁻¹) fun x => x * x₀
⊢ (fun x => x * x₀) '' V' ∈ 𝓝 x₀
have c : Continuous fun x : hat K => x * x₀⁻¹ := continuous_id.mul continuous_const
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
l : Function.LeftInverse (fun x => x * x₀⁻¹) fun x => x * x₀
r : Function.RightInverse (fun x => x * x₀⁻¹) fun x => x * x₀
c : Continuous fun x => x * x₀⁻¹
⊢ (fun x => x * x₀⁻¹) ⁻¹' V' ∈ 𝓝 x₀
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
l : Function.LeftInverse (fun x => x * x₀⁻¹) fun x => x * x₀
r : Function.RightInverse (fun x => x * x₀⁻¹) fun x => x * x₀
c : Continuous fun x => x * x₀⁻¹
⊢ (fun x => x * x₀) '' V' ∈ 𝓝 x₀
rw [image_eq_preimage_of_inverse l r]
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 (x₀ * x₀⁻¹)
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
l : Function.LeftInverse (fun x => x * x₀⁻¹) fun x => x * x₀
r : Function.RightInverse (fun x => x * x₀⁻¹) fun x => x * x₀
c : Continuous fun x => x * x₀⁻¹
⊢ (fun x => x * x₀⁻¹) ⁻¹' V' ∈ 𝓝 x₀
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
l : Function.LeftInverse (fun x => x * x₀⁻¹) fun x => x * x₀
r : Function.RightInverse (fun x => x * x₀⁻¹) fun x => x * x₀
c : Continuous fun x => x * x₀⁻¹
⊢ (fun x => x * x₀⁻¹) ⁻¹' V' ∈ 𝓝 x₀
rw [← mul_inv_cancel h] at V'_in
no goals
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 (x₀ * x₀⁻¹)
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
l : Function.LeftInverse (fun x => x * x₀⁻¹) fun x => x * x₀
r : Function.RightInverse (fun x => x * x₀⁻¹) fun x => x * x₀
c : Continuous fun x => x * x₀⁻¹
⊢ (fun x => x * x₀⁻¹) ⁻¹' V' ∈ 𝓝 x₀
exact c.continuousAt V'_in
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
x : hat K
⊢ (fun x => x * x₀⁻¹) ((fun x => x * x₀) x) = x
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
⊢ Function.LeftInverse (fun x => x * x₀⁻¹) fun x => x * x₀
intro x
no goals
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
x : hat K
⊢ (fun x => x * x₀⁻¹) ((fun x => x * x₀) x) = x
simp only [mul_assoc, mul_inv_cancel h, mul_one]
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
l : Function.LeftInverse (fun x => x * x₀⁻¹) fun x => x * x₀
x : hat K
⊢ (fun x => x * x₀) ((fun x => x * x₀⁻¹) x) = x
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
l : Function.LeftInverse (fun x => x * x₀⁻¹) fun x => x * x₀
⊢ Function.RightInverse (fun x => x * x₀⁻¹) fun x => x * x₀
intro x
no goals
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
l : Function.LeftInverse (fun x => x * x₀⁻¹) fun x => x * x₀
x : hat K
⊢ (fun x => x * x₀) ((fun x => x * x₀⁻¹) x) = x
simp only [mul_assoc, inv_mul_cancel h, mul_one]
case intro.intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
H : y₀ * x₀ = ↑K z₀
⊢ ∃ z₀ y₀, y₀ ∈ V' ∧ ↑K z₀ = y₀ * x₀ ∧ z₀ ≠ 0
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
⊢ ∃ z₀ y₀, y₀ ∈ V' ∧ ↑K z₀ = y₀ * x₀ ∧ z₀ ≠ 0
rcases Completion.denseRange_coe.mem_nhds nhds_right with ⟨z₀, y₀, y₀_in, H : y₀ * x₀ = z₀⟩
case intro.intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
H : y₀ * x₀ = ↑K z₀
⊢ z₀ ≠ 0
case intro.intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
H : y₀ * x₀ = ↑K z₀
⊢ ∃ z₀ y₀, y₀ ∈ V' ∧ ↑K z₀ = y₀ * x₀ ∧ z₀ ≠ 0
refine' ⟨z₀, y₀, y₀_in, ⟨H.symm, _⟩⟩
case intro.intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
y₀ : hat K
y₀_in : y₀ ∈ V'
H : y₀ * x₀ = ↑K 0
⊢ False
case intro.intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
H : y₀ * x₀ = ↑K z₀
⊢ z₀ ≠ 0
rintro rfl
no goals
case intro.intro.intro
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
y₀ : hat K
y₀_in : y₀ ∈ V'
H : y₀ * x₀ = ↑K 0
⊢ False
exact mul_ne_zero (ne_of_mem_of_not_mem y₀_in zeroV') h H
no goals
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑K z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
⊢ ↑v z₀ ≠ 0
rwa [Valuation.ne_zero_iff]
case a
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑K z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : ↑v z₀ ≠ 0
a : K
y : hat K
y_in : y ∈ V'
ha : ↑K a = (fun x => x * x₀) y
⊢ ↑K (a * z₀⁻¹) ∈ V
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑K z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : ↑v z₀ ≠ 0
a : K
y : hat K
y_in : y ∈ V'
ha : ↑K a = (fun x => x * x₀) y
⊢ ↑v (a * z₀⁻¹) = 1
apply hV
case a
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑K z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : ↑v z₀ ≠ 0
a : K
y : hat K
y_in : y ∈ V'
ha : ↑K a = (fun x => x * x₀) y
this : ↑K z₀⁻¹ = (↑K z₀)⁻¹
⊢ ↑K (a * z₀⁻¹) ∈ V
case a
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑K z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : ↑v z₀ ≠ 0
a : K
y : hat K
y_in : y ∈ V'
ha : ↑K a = (fun x => x * x₀) y
⊢ ↑K (a * z₀⁻¹) ∈ V
have : (z₀⁻¹ : K) = (z₀ : hat K)⁻¹ := map_inv₀ (Completion.coeRingHom : K →+* hat K) z₀
case a
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑K z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : ↑v z₀ ≠ 0
a : K
y : hat K
y_in : y ∈ V'
ha : ↑K a = (fun x => x * x₀) y
this : ↑K z₀⁻¹ = (↑K z₀)⁻¹
⊢ y * y₀⁻¹ ∈ V
case a
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑K z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : ↑v z₀ ≠ 0
a : K
y : hat K
y_in : y ∈ V'
ha : ↑K a = (fun x => x * x₀) y
this : ↑K z₀⁻¹ = (↑K z₀)⁻¹
⊢ ↑K (a * z₀⁻¹) ∈ V
rw [Completion.coe_mul, this, ha, hz₀, mul_inv, mul_comm y₀⁻¹, ← mul_assoc, mul_assoc y,
  mul_inv_cancel h, mul_one]
no goals
case a
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑K z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : ↑v z₀ ≠ 0
a : K
y : hat K
y_in : y ∈ V'
ha : ↑K a = (fun x => x * x₀) y
this : ↑K z₀⁻¹ = (↑K z₀)⁻¹
⊢ y * y₀⁻¹ ∈ V
solve_by_elim
no goals
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑K z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : ↑v z₀ ≠ 0
a : K
y : hat K
y_in : y ∈ V'
ha : ↑K a = (fun x => x * x₀) y
this : ↑v (a * z₀⁻¹) = 1
⊢ ↑v a = ↑v (a * z₀⁻¹ * z₀)
rw [mul_assoc, inv_mul_cancel z₀_ne, mul_one]
no goals
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ↑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑K x ∈ V → ↑v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : ¬0 ∈ V'
hV' : ∀ (x : hat K), x ∈ V' → ∀ (y : hat K), y ∈ V' → x * y⁻¹ ∈ V
nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑K z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : ↑v z₀ ≠ 0
a : K
y : hat K
y_in : y ∈ V'
ha : ↑K a = (fun x => x * x₀) y
this : ↑v (a * z₀⁻¹) = 1
⊢ ↑v (a * z₀⁻¹) * ↑v z₀ = ↑v z₀
rw [this, one_mul]