[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
e : α ≃ β
h₁ : UniformContinuous e.toFun
h₂ : UniformContinuous e.invFun
e' : α ≃ β
h₁' : UniformContinuous e'.toFun
h₂' : UniformContinuous e'.invFun
h :
  { toEquiv := e, uniformContinuous_toFun := h₁, uniformContinuous_invFun := h₂ }.toEquiv =
    { toEquiv := e', uniformContinuous_toFun := h₁', uniformContinuous_invFun := h₂' }.toEquiv
⊢ { toEquiv := e, uniformContinuous_toFun := h₁, uniformContinuous_invFun := h₂ } =
    { toEquiv := e', uniformContinuous_toFun := h₁', uniformContinuous_invFun := h₂' }
[PROOFSTEP]
simpa only [mk.injEq]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
f : α ≃ᵤ β
g : β → α
hg : Function.RightInverse g ↑f
x : β
⊢ ↑(UniformEquiv.symm f) (↑f (g x)) = ↑(UniformEquiv.symm f) x
[PROOFSTEP]
rw [hg x]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
f : α ≃ᵤ β
g : β → α
hg : Function.RightInverse g ↑f
this : g = ↑(UniformEquiv.symm f)
⊢ Function.LeftInverse g ↑f
[PROOFSTEP]
convert f.left_inv
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
f : α ≃ᵤ β
g : β → α
hg : Function.RightInverse g ↑f
this : g = ↑(UniformEquiv.symm f)
⊢ Function.RightInverse g ↑f
[PROOFSTEP]
convert f.right_inv using 1
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
f : α ≃ᵤ β
g : β → α
hg : Function.RightInverse g ↑f
this : g = ↑(UniformEquiv.symm f)
⊢ UniformContinuous
    { toFun := ↑f, invFun := g, left_inv := (_ : Function.LeftInverse g ↑f),
        right_inv := (_ : Function.RightInverse g ↑f) }.invFun
[PROOFSTEP]
convert f.symm.uniformContinuous
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
h : α ≃ᵤ β
⊢ UniformInducing (↑(UniformEquiv.symm h) ∘ ↑h)
[PROOFSTEP]
simp only [symm_comp_self, uniformInducing_id]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
h : α ≃ᵤ β
⊢ UniformSpace.comap (↑h) inst✝² = inst✝³
[PROOFSTEP]
ext : 1
[GOAL]
case a
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
h : α ≃ᵤ β
⊢ uniformity α = uniformity α
[PROOFSTEP]
exact h.uniformInducing.comap_uniformity
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
f : α → β
hf : UniformEmbedding f
⊢ UniformContinuous (Equiv.ofInjective f (_ : Function.Injective f)).invFun
[PROOFSTEP]
rw [hf.toUniformInducing.uniformContinuous_iff, Equiv.invFun_as_coe, Equiv.self_comp_ofInjective_symm]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
f : α → β
hf : UniformEmbedding f
⊢ UniformContinuous Subtype.val
[PROOFSTEP]
exact uniformContinuous_subtype_val
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
⊢ UniformContinuous (Equiv.prodAssoc α β γ).invFun
[PROOFSTEP]
rw [Equiv.invFun, Equiv.prodAssoc]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
⊢ UniformContinuous
    { toFun := fun p => (p.fst.fst, p.fst.snd, p.snd), invFun := fun p => ((p.fst, p.snd.fst), p.snd.snd),
        left_inv :=
          (_ :
            ∀ (x : (α × β) × γ),
              (fun p => ((p.fst, p.snd.fst), p.snd.snd)) ((fun p => (p.fst.fst, p.fst.snd, p.snd)) x) = x),
        right_inv :=
          (_ :
            ∀ (x : α × β × γ),
              (fun p => (p.fst.fst, p.fst.snd, p.snd)) ((fun p => ((p.fst, p.snd.fst), p.snd.snd)) x) = x) }.2
[PROOFSTEP]
exact
  (uniformContinuous_fst.prod_mk (uniformContinuous_fst.comp uniformContinuous_snd)).prod_mk
    (uniformContinuous_snd.comp uniformContinuous_snd)
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
src✝ : ULift α ≃ α := Equiv.ulift
⊢ UniformContinuous
    { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
        right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }.invFun
[PROOFSTEP]
have hf : UniformInducing (@Equiv.ulift.{v, u} α).toFun := ⟨rfl⟩
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
src✝ : ULift α ≃ α := Equiv.ulift
hf : UniformInducing Equiv.ulift.toFun
⊢ UniformContinuous
    { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
        right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }.invFun
[PROOFSTEP]
simp_rw [hf.uniformContinuous_iff]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
src✝ : ULift α ≃ α := Equiv.ulift
hf : UniformInducing Equiv.ulift.toFun
⊢ UniformContinuous (Equiv.ulift.toFun ∘ Equiv.ulift.invFun)
[PROOFSTEP]
exact uniformContinuous_id
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α ≃ β
hf : UniformInducing ↑f
⊢ UniformContinuous
    (↑f ∘
      { toFun := f.toFun, invFun := f.invFun, left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
          right_inv := (_ : Function.RightInverse f.invFun f.toFun) }.invFun)
[PROOFSTEP]
simpa using uniformContinuous_id


[GOAL]
K✝ : Type u_1
inst✝⁴ : DivisionRing K✝
inst✝³ : TopologicalSpace K✝
α : Type u_2
inst✝² : Field α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalDivisionRing α
K : Subfield α
src✝ : Subring α := Subring.topologicalClosure K.toSubring
x : α
hx :
  x ∈
    {
              toSubsemiring :=
                {
                  toSubmonoid :=
                    {
                      toSubsemigroup :=
                        { carrier := _root_.closure ↑K,
                          mul_mem' := (_ : ∀ {a b : α}, a ∈ src✝.carrier → b ∈ src✝.carrier → a * b ∈ src✝.carrier) },
                      one_mem' := (_ : 1 ∈ src✝.carrier) },
                  add_mem' := (_ : ∀ {a b : α}, a ∈ src✝.carrier → b ∈ src✝.carrier → a + b ∈ src✝.carrier),
                  zero_mem' := (_ : 0 ∈ src✝.carrier) },
              neg_mem' :=
                (_ : ∀ {x : α}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toSubsemiring.toSubmonoid.toSubsemigroup.carrier
⊢ x⁻¹ ∈
    {
              toSubsemiring :=
                {
                  toSubmonoid :=
                    {
                      toSubsemigroup :=
                        { carrier := _root_.closure ↑K,
                          mul_mem' := (_ : ∀ {a b : α}, a ∈ src✝.carrier → b ∈ src✝.carrier → a * b ∈ src✝.carrier) },
                      one_mem' := (_ : 1 ∈ src✝.carrier) },
                  add_mem' := (_ : ∀ {a b : α}, a ∈ src✝.carrier → b ∈ src✝.carrier → a + b ∈ src✝.carrier),
                  zero_mem' := (_ : 0 ∈ src✝.carrier) },
              neg_mem' :=
                (_ : ∀ {x : α}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toSubsemiring.toSubmonoid.toSubsemigroup.carrier
[PROOFSTEP]
dsimp only at hx ⊢
[GOAL]
K✝ : Type u_1
inst✝⁴ : DivisionRing K✝
inst✝³ : TopologicalSpace K✝
α : Type u_2
inst✝² : Field α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalDivisionRing α
K : Subfield α
src✝ : Subring α := Subring.topologicalClosure K.toSubring
x : α
hx : x ∈ _root_.closure ↑K
⊢ x⁻¹ ∈ _root_.closure ↑K
[PROOFSTEP]
rcases eq_or_ne x 0 with (rfl | h)
[GOAL]
case inl
K✝ : Type u_1
inst✝⁴ : DivisionRing K✝
inst✝³ : TopologicalSpace K✝
α : Type u_2
inst✝² : Field α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalDivisionRing α
K : Subfield α
src✝ : Subring α := Subring.topologicalClosure K.toSubring
hx : 0 ∈ _root_.closure ↑K
⊢ 0⁻¹ ∈ _root_.closure ↑K
[PROOFSTEP]
rwa [inv_zero]
[GOAL]
case inr
K✝ : Type u_1
inst✝⁴ : DivisionRing K✝
inst✝³ : TopologicalSpace K✝
α : Type u_2
inst✝² : Field α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalDivisionRing α
K : Subfield α
src✝ : Subring α := Subring.topologicalClosure K.toSubring
x : α
hx : x ∈ _root_.closure ↑K
h : x ≠ 0
⊢ x⁻¹ ∈ _root_.closure ↑K
[PROOFSTEP]
rw [← @inv_coe_set α (Subfield α) _ _ SubfieldClass.toInvMemClass K, ← Set.image_inv]
[GOAL]
case inr
K✝ : Type u_1
inst✝⁴ : DivisionRing K✝
inst✝³ : TopologicalSpace K✝
α : Type u_2
inst✝² : Field α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalDivisionRing α
K : Subfield α
src✝ : Subring α := Subring.topologicalClosure K.toSubring
x : α
hx : x ∈ _root_.closure ↑K
h : x ≠ 0
⊢ x⁻¹ ∈ _root_.closure (Inv.inv '' ↑K)
[PROOFSTEP]
exact mem_closure_image (continuousAt_inv₀ h) hx
[GOAL]
K : Type u_1
inst✝⁴ : DivisionRing K
inst✝³ : TopologicalSpace K
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : TopologicalRing 𝕜
a b : 𝕜
h : a ≠ 0
x : 𝕜
⊢ (fun y => (y - b) / a) ((fun x => a * x + b) x) = x
[PROOFSTEP]
simp only [add_sub_cancel]
[GOAL]
K : Type u_1
inst✝⁴ : DivisionRing K
inst✝³ : TopologicalSpace K
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : TopologicalRing 𝕜
a b : 𝕜
h : a ≠ 0
x : 𝕜
⊢ a * x / a = x
[PROOFSTEP]
exact mul_div_cancel_left x h
[GOAL]
K : Type u_1
inst✝⁴ : DivisionRing K
inst✝³ : TopologicalSpace K
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : TopologicalRing 𝕜
a b : 𝕜
h : a ≠ 0
y : 𝕜
⊢ (fun x => a * x + b) ((fun y => (y - b) / a) y) = y
[PROOFSTEP]
simp [mul_div_cancel' _ h]
[GOAL]
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : TopologicalSpace K
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrderedSemifield β
a✝ : α
f : α → β
a : α
h1 : IsLocalMin f a
h2 : ∀ᶠ (z : α) in 𝓝 a, 0 < f z
⊢ IsLocalMax f⁻¹ a
[PROOFSTEP]
filter_upwards [h1, h2] with z h3 h4 using (inv_le_inv h4 h2.self_of_nhds).mpr h3
[GOAL]
K : Type u_1
inst✝⁶ : DivisionRing K
inst✝⁵ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace 𝕜
inst✝² : T1Space 𝕜
inst✝¹ : Ring 𝕜
inst✝ : NoZeroDivisors 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hsq : EqOn (f ^ 2) 1 S
⊢ EqOn f 1 S ∨ EqOn f (-1) S
[PROOFSTEP]
have : DiscreteTopology ({1, -1} : Set 𝕜) := discrete_of_t1_of_finite
[GOAL]
K : Type u_1
inst✝⁶ : DivisionRing K
inst✝⁵ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace 𝕜
inst✝² : T1Space 𝕜
inst✝¹ : Ring 𝕜
inst✝ : NoZeroDivisors 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hsq : EqOn (f ^ 2) 1 S
this : DiscreteTopology ↑{1, -1}
⊢ EqOn f 1 S ∨ EqOn f (-1) S
[PROOFSTEP]
have hmaps : MapsTo f S {1, -1}
[GOAL]
case hmaps
K : Type u_1
inst✝⁶ : DivisionRing K
inst✝⁵ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace 𝕜
inst✝² : T1Space 𝕜
inst✝¹ : Ring 𝕜
inst✝ : NoZeroDivisors 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hsq : EqOn (f ^ 2) 1 S
this : DiscreteTopology ↑{1, -1}
⊢ MapsTo f S {1, -1}
[PROOFSTEP]
simpa only [EqOn, Pi.one_apply, Pi.pow_apply, sq_eq_one_iff] using hsq
[GOAL]
K : Type u_1
inst✝⁶ : DivisionRing K
inst✝⁵ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace 𝕜
inst✝² : T1Space 𝕜
inst✝¹ : Ring 𝕜
inst✝ : NoZeroDivisors 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hsq : EqOn (f ^ 2) 1 S
this : DiscreteTopology ↑{1, -1}
hmaps : MapsTo f S {1, -1}
⊢ EqOn f 1 S ∨ EqOn f (-1) S
[PROOFSTEP]
simpa using hS.eqOn_const_of_mapsTo hf hmaps
[GOAL]
K : Type u_1
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : HasContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
⊢ EqOn f g S ∨ EqOn f (-g) S
[PROOFSTEP]
have hsq : EqOn ((f / g) ^ 2) 1 S := fun x hx => by simpa [div_eq_one_iff_eq (pow_ne_zero _ (hg_ne hx))] using hsq hx
[GOAL]
K : Type u_1
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : HasContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
x : α
hx : x ∈ S
⊢ ((f / g) ^ 2) x = OfNat.ofNat 1 x
[PROOFSTEP]
simpa [div_eq_one_iff_eq (pow_ne_zero _ (hg_ne hx))] using hsq hx
[GOAL]
K : Type u_1
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : HasContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq✝ : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
hsq : EqOn ((f / g) ^ 2) 1 S
⊢ EqOn f g S ∨ EqOn f (-g) S
[PROOFSTEP]
simpa (config := { contextual := true }) [EqOn, div_eq_iff (hg_ne _)] using
  hS.eq_one_or_eq_neg_one_of_sq_eq (hf.div hg fun z => hg_ne) hsq
[GOAL]
K : Type u_1
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : HasContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : f y = g y
x : α
hx : x ∈ S
⊢ f x = g x
[PROOFSTEP]
rcases hS.eq_or_eq_neg_of_sq_eq hf hg @hsq @hg_ne with (h | h)
[GOAL]
case inl
K : Type u_1
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : HasContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : f y = g y
x : α
hx : x ∈ S
h : EqOn f g S
⊢ f x = g x
[PROOFSTEP]
exact h hx
[GOAL]
case inr
K : Type u_1
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : HasContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : f y = g y
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ f x = g x
[PROOFSTEP]
rw [h _, Pi.neg_apply, neg_eq_iff_add_eq_zero, ← two_mul, mul_eq_zero, iff_false_iff.2 (hg_ne _)] at hy' ⊢
[GOAL]
case inr
K : Type u_1
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : HasContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : 2 = 0 ∨ False
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ 2 = 0 ∨ False
[PROOFSTEP]
assumption
[GOAL]
K : Type u_1
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : HasContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : 2 = 0 ∨ False
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ x ∈ S
[PROOFSTEP]
assumption
[GOAL]
K : Type u_1
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : HasContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : 2 = 0 ∨ g y = 0
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ y ∈ S
[PROOFSTEP]
assumption
[GOAL]
K : Type u_1
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : HasContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : (-g) y = g y
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ x ∈ S
[PROOFSTEP]
assumption
[GOAL]
K : Type u_1
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : HasContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : f y = g y
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ y ∈ S
[PROOFSTEP]
assumption


[GOAL]
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
⊢ ContinuousAt hatInv x
[PROOFSTEP]
haveI : T3Space (hat K) := Completion.t3Space K
[GOAL]
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this : T3Space (hat K)
⊢ ContinuousAt hatInv x
[PROOFSTEP]
refine' denseInducing_coe.continuousAt_extend _
[GOAL]
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this : T3Space (hat K)
⊢ ∀ᶠ (x : hat K) in 𝓝 x, ∃ c, Tendsto (fun x => ↑K x⁻¹) (Filter.comap (↑K) (𝓝 x)) (𝓝 c)
[PROOFSTEP]
apply mem_of_superset (compl_singleton_mem_nhds h)
[GOAL]
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this : T3Space (hat K)
⊢ {0}ᶜ ⊆ {x | (fun x => ∃ c, Tendsto (fun x => ↑K x⁻¹) (Filter.comap (↑K) (𝓝 x)) (𝓝 c)) x}
[PROOFSTEP]
intro y y_ne
[GOAL]
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this : T3Space (hat K)
y : hat K
y_ne : y ∈ {0}ᶜ
⊢ y ∈ {x | (fun x => ∃ c, Tendsto (fun x => ↑K x⁻¹) (Filter.comap (↑K) (𝓝 x)) (𝓝 c)) x}
[PROOFSTEP]
rw [mem_compl_singleton_iff] at y_ne
[GOAL]
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
⊢ y ∈ {x | (fun x => ∃ c, Tendsto (fun x => ↑K x⁻¹) (Filter.comap (↑K) (𝓝 x)) (𝓝 c)) x}
[PROOFSTEP]
apply CompleteSpace.complete
[GOAL]
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
⊢ Cauchy (map (fun x => ↑K x⁻¹) (Filter.comap (↑K) (𝓝 y)))
[PROOFSTEP]
have : (fun (x : K) => (↑x⁻¹ : hat K)) = ((fun (y : K) => (↑y : hat K)) ∘ (fun (x : K) => (x⁻¹ : K))) :=
  by
  unfold Function.comp
  simp
[GOAL]
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
⊢ (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹
[PROOFSTEP]
unfold Function.comp
[GOAL]
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
⊢ (fun x => ↑K x⁻¹) = fun x => (fun y => ↑K y) ((fun x => x⁻¹) x)
[PROOFSTEP]
simp
[GOAL]
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this✝ : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹
⊢ Cauchy (map (fun x => ↑K x⁻¹) (Filter.comap (↑K) (𝓝 y)))
[PROOFSTEP]
rw [this, ← Filter.map_map]
[GOAL]
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this✝ : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹
⊢ Cauchy (map (fun y => ↑K y) (map (fun x => x⁻¹) (Filter.comap (↑K) (𝓝 y))))
[PROOFSTEP]
apply Cauchy.map _ (Completion.uniformContinuous_coe K)
[GOAL]
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this✝ : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹
⊢ Cauchy (map (fun x => x⁻¹) (Filter.comap (↑K) (𝓝 y)))
[PROOFSTEP]
apply CompletableTopField.nice
[GOAL]
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this✝ : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹
⊢ Cauchy (Filter.comap (↑K) (𝓝 y))
[PROOFSTEP]
haveI := denseInducing_coe.comap_nhds_neBot y
[GOAL]
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this✝¹ : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
this✝ : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹
this : NeBot (Filter.comap (↑K) (𝓝 y))
⊢ Cauchy (Filter.comap (↑K) (𝓝 y))
[PROOFSTEP]
apply cauchy_nhds.comap
[GOAL]
case a.hm
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this✝¹ : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
this✝ : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹
this : NeBot (Filter.comap (↑K) (𝓝 y))
⊢ Filter.comap (fun p => (↑K p.fst, ↑K p.snd)) (uniformity (hat K)) ≤ uniformity K
[PROOFSTEP]
rw [Completion.comap_coe_eq_uniformity]
[GOAL]
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this✝ : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹
⊢ 𝓝 0 ⊓ Filter.comap (↑K) (𝓝 y) = ⊥
[PROOFSTEP]
have eq_bot : 𝓝 (0 : hat K) ⊓ 𝓝 y = ⊥ := by
  by_contra h
  exact y_ne (eq_of_nhds_neBot <| neBot_iff.mpr h).symm
[GOAL]
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this✝ : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹
⊢ 𝓝 0 ⊓ 𝓝 y = ⊥
[PROOFSTEP]
by_contra h
[GOAL]
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h✝ : x ≠ 0
this✝ : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹
h : ¬𝓝 0 ⊓ 𝓝 y = ⊥
⊢ False
[PROOFSTEP]
exact y_ne (eq_of_nhds_neBot <| neBot_iff.mpr h).symm
[GOAL]
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this✝ : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹
eq_bot : 𝓝 0 ⊓ 𝓝 y = ⊥
⊢ 𝓝 0 ⊓ Filter.comap (↑K) (𝓝 y) = ⊥
[PROOFSTEP]
erw [denseInducing_coe.nhds_eq_comap (0 : K), ← Filter.comap_inf, eq_bot]
[GOAL]
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this✝ : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹
eq_bot : 𝓝 0 ⊓ 𝓝 y = ⊥
⊢ Filter.comap ↑K ⊥ = ⊥
[PROOFSTEP]
exact comap_bot
[GOAL]
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
⊢ (↑K x)⁻¹ = ↑K x⁻¹
[PROOFSTEP]
by_cases h : x = 0
[GOAL]
case pos
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : x = 0
⊢ (↑K x)⁻¹ = ↑K x⁻¹
[PROOFSTEP]
rw [h, inv_zero]
[GOAL]
case pos
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : x = 0
⊢ (↑K 0)⁻¹ = ↑K 0
[PROOFSTEP]
dsimp [Inv.inv]
[GOAL]
case pos
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : x = 0
⊢ (if ↑K 0 = 0 then 0 else hatInv (↑K 0)) = ↑K 0
[PROOFSTEP]
norm_cast
[GOAL]
case pos
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : x = 0
⊢ (if 0 = 0 then 0 else hatInv 0) = 0
[PROOFSTEP]
simp
[GOAL]
case neg
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
⊢ (↑K x)⁻¹ = ↑K x⁻¹
[PROOFSTEP]
conv_lhs => dsimp [Inv.inv]
[GOAL]
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
| (↑K x)⁻¹
[PROOFSTEP]
dsimp [Inv.inv]
[GOAL]
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
| (↑K x)⁻¹
[PROOFSTEP]
dsimp [Inv.inv]
[GOAL]
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
| (↑K x)⁻¹
[PROOFSTEP]
dsimp [Inv.inv]
[GOAL]
case neg
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
⊢ (if ↑K x = 0 then 0 else hatInv (↑K x)) = ↑K x⁻¹
[PROOFSTEP]
rw [if_neg]
[GOAL]
case neg
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
⊢ hatInv (↑K x) = ↑K x⁻¹
[PROOFSTEP]
exact hatInv_extends h
[GOAL]
case neg.hnc
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
⊢ ¬↑K x = 0
[PROOFSTEP]
exact fun H => h (denseEmbedding_coe.inj H)
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
⊢ x * hatInv x = 1
[PROOFSTEP]
haveI : T1Space (hat K) := T2Space.t1Space
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
⊢ x * hatInv x = 1
[PROOFSTEP]
let f := fun x : hat K => x * hatInv x
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
⊢ x * hatInv x = 1
[PROOFSTEP]
let c := (fun (x : K) => (x : hat K))
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
⊢ x * hatInv x = 1
[PROOFSTEP]
change f x = 1
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
⊢ f x = 1
[PROOFSTEP]
have cont : ContinuousAt f x :=
  by
  letI : TopologicalSpace (hat K × hat K) := instTopologicalSpaceProd
  have : ContinuousAt (fun y : hat K => ((y, hatInv y) : hat K × hat K)) x :=
    continuous_id.continuousAt.prod (continuous_hatInv x_ne)
  exact (_root_.continuous_mul.continuousAt.comp this : _)
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
⊢ ContinuousAt f x
[PROOFSTEP]
letI : TopologicalSpace (hat K × hat K) := instTopologicalSpaceProd
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this✝ : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
this : TopologicalSpace (hat K × hat K) := instTopologicalSpaceProd
⊢ ContinuousAt f x
[PROOFSTEP]
have : ContinuousAt (fun y : hat K => ((y, hatInv y) : hat K × hat K)) x :=
  continuous_id.continuousAt.prod (continuous_hatInv x_ne)
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this✝¹ : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
this✝ : TopologicalSpace (hat K × hat K) := instTopologicalSpaceProd
this : ContinuousAt (fun y => (y, hatInv y)) x
⊢ ContinuousAt f x
[PROOFSTEP]
exact (_root_.continuous_mul.continuousAt.comp this : _)
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
cont : ContinuousAt f x
⊢ f x = 1
[PROOFSTEP]
have clo : x ∈ closure (c '' {0}ᶜ) := by
  have := denseInducing_coe.dense x
  rw [← image_univ, show (univ : Set K) = {0} ∪ {0}ᶜ from (union_compl_self _).symm, image_union] at this
  apply mem_closure_of_mem_closure_union this
  rw [image_singleton]
  exact compl_singleton_mem_nhds x_ne
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
cont : ContinuousAt f x
⊢ x ∈ closure (c '' {0}ᶜ)
[PROOFSTEP]
have := denseInducing_coe.dense x
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this✝ : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
cont : ContinuousAt f x
this : x ∈ closure (range ↑K)
⊢ x ∈ closure (c '' {0}ᶜ)
[PROOFSTEP]
rw [← image_univ, show (univ : Set K) = {0} ∪ {0}ᶜ from (union_compl_self _).symm, image_union] at this
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this✝ : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
cont : ContinuousAt f x
this : x ∈ closure (↑K '' {0} ∪ ↑K '' {0}ᶜ)
⊢ x ∈ closure (c '' {0}ᶜ)
[PROOFSTEP]
apply mem_closure_of_mem_closure_union this
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this✝ : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
cont : ContinuousAt f x
this : x ∈ closure (↑K '' {0} ∪ ↑K '' {0}ᶜ)
⊢ (↑K '' {0})ᶜ ∈ 𝓝 x
[PROOFSTEP]
rw [image_singleton]
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this✝ : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
cont : ContinuousAt f x
this : x ∈ closure (↑K '' {0} ∪ ↑K '' {0}ᶜ)
⊢ {↑K 0}ᶜ ∈ 𝓝 x
[PROOFSTEP]
exact compl_singleton_mem_nhds x_ne
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
⊢ f x = 1
[PROOFSTEP]
have fxclo : f x ∈ closure (f '' (c '' {0}ᶜ)) := mem_closure_image cont clo
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' (c '' {0}ᶜ))
⊢ f x = 1
[PROOFSTEP]
have : f '' (c '' {0}ᶜ) ⊆ {1} := by
  rw [image_image]
  rintro _ ⟨z, z_ne, rfl⟩
  rw [mem_singleton_iff]
  rw [mem_compl_singleton_iff] at z_ne
  dsimp
  rw [hatInv_extends z_ne, ← coe_mul]
  rw [mul_inv_cancel z_ne, coe_one]
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' (c '' {0}ᶜ))
⊢ f '' (c '' {0}ᶜ) ⊆ {1}
[PROOFSTEP]
rw [image_image]
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' (c '' {0}ᶜ))
⊢ (fun x => f (c x)) '' {0}ᶜ ⊆ {1}
[PROOFSTEP]
rintro _ ⟨z, z_ne, rfl⟩
[GOAL]
case intro.intro
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' (c '' {0}ᶜ))
z : K
z_ne : z ∈ {0}ᶜ
⊢ (fun x => f (c x)) z ∈ {1}
[PROOFSTEP]
rw [mem_singleton_iff]
[GOAL]
case intro.intro
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' (c '' {0}ᶜ))
z : K
z_ne : z ∈ {0}ᶜ
⊢ (fun x => f (c x)) z = 1
[PROOFSTEP]
rw [mem_compl_singleton_iff] at z_ne
[GOAL]
case intro.intro
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' (c '' {0}ᶜ))
z : K
z_ne : z ≠ 0
⊢ (fun x => f (c x)) z = 1
[PROOFSTEP]
dsimp
[GOAL]
case intro.intro
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' (c '' {0}ᶜ))
z : K
z_ne : z ≠ 0
⊢ ↑K z * hatInv (↑K z) = 1
[PROOFSTEP]
rw [hatInv_extends z_ne, ← coe_mul]
[GOAL]
case intro.intro
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' (c '' {0}ᶜ))
z : K
z_ne : z ≠ 0
⊢ ↑K (z * z⁻¹) = 1
[PROOFSTEP]
rw [mul_inv_cancel z_ne, coe_one]
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this✝ : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' (c '' {0}ᶜ))
this : f '' (c '' {0}ᶜ) ⊆ {1}
⊢ f x = 1
[PROOFSTEP]
replace fxclo := closure_mono this fxclo
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this✝ : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
this : f '' (c '' {0}ᶜ) ⊆ {1}
fxclo : f x ∈ closure {1}
⊢ f x = 1
[PROOFSTEP]
rwa [closure_singleton, mem_singleton_iff] at fxclo
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
src✝ : Inv (hat K) := instInvCompletion
⊢ CommRing (hat K)
[PROOFSTEP]
infer_instance
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
src✝¹ : Inv (hat K) := instInvCompletion
src✝ : CommRing (hat K) := inferInstance
x : hat K
x_ne : x ≠ 0
⊢ x * x⁻¹ = 1
[PROOFSTEP]
simp only [Inv.inv, if_neg x_ne, mul_hatInv_cancel x_ne]
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
src✝¹ : Inv (hat K) := instInvCompletion
src✝ : CommRing (hat K) := inferInstance
⊢ 0⁻¹ = 0
[PROOFSTEP]
simp only [Inv.inv, ite_true]
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
src✝ : TopologicalRing (hat K) := topologicalRing
⊢ ∀ ⦃x : hat K⦄, x ≠ 0 → ContinuousAt Inv.inv x
[PROOFSTEP]
intro x x_ne
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
src✝ : TopologicalRing (hat K) := topologicalRing
x : hat K
x_ne : x ≠ 0
⊢ ContinuousAt Inv.inv x
[PROOFSTEP]
have : {y | hatInv y = y⁻¹} ∈ 𝓝 x :=
  haveI : {(0 : hat K)}ᶜ ⊆ {y : hat K | hatInv y = y⁻¹} :=
    by
    intro y y_ne
    rw [mem_compl_singleton_iff] at y_ne
    dsimp [Inv.inv]
    rw [if_neg y_ne]
  mem_of_superset (compl_singleton_mem_nhds x_ne) this
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
src✝ : TopologicalRing (hat K) := topologicalRing
x : hat K
x_ne : x ≠ 0
⊢ {0}ᶜ ⊆ {y | hatInv y = y⁻¹}
[PROOFSTEP]
intro y y_ne
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
src✝ : TopologicalRing (hat K) := topologicalRing
x : hat K
x_ne : x ≠ 0
y : hat K
y_ne : y ∈ {0}ᶜ
⊢ y ∈ {y | hatInv y = y⁻¹}
[PROOFSTEP]
rw [mem_compl_singleton_iff] at y_ne
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
src✝ : TopologicalRing (hat K) := topologicalRing
x : hat K
x_ne : x ≠ 0
y : hat K
y_ne : y ≠ 0
⊢ y ∈ {y | hatInv y = y⁻¹}
[PROOFSTEP]
dsimp [Inv.inv]
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
src✝ : TopologicalRing (hat K) := topologicalRing
x : hat K
x_ne : x ≠ 0
y : hat K
y_ne : y ≠ 0
⊢ hatInv y = if y = 0 then 0 else hatInv y
[PROOFSTEP]
rw [if_neg y_ne]
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
src✝ : TopologicalRing (hat K) := topologicalRing
x : hat K
x_ne : x ≠ 0
this : {y | hatInv y = y⁻¹} ∈ 𝓝 x
⊢ ContinuousAt Inv.inv x
[PROOFSTEP]
exact ContinuousAt.congr (continuous_hatInv x_ne) this
[GOAL]
K✝ : Type u_1
inst✝⁴ : Field K✝
inst✝³ : UniformSpace K✝
L : Type u_2
inst✝² : Field L
inst✝¹ : UniformSpace L
inst✝ : CompletableTopField L
K : Subfield L
src✝ : SeparatedSpace ↑↑K := Subtype.separatedSpace ↑K
⊢ ∀ (F : Filter { x // x ∈ K }), Cauchy F → 𝓝 0 ⊓ F = ⊥ → Cauchy (Filter.map (fun x => x⁻¹) F)
[PROOFSTEP]
intro F F_cau inf_F
[GOAL]
K✝ : Type u_1
inst✝⁴ : Field K✝
inst✝³ : UniformSpace K✝
L : Type u_2
inst✝² : Field L
inst✝¹ : UniformSpace L
inst✝ : CompletableTopField L
K : Subfield L
src✝ : SeparatedSpace ↑↑K := Subtype.separatedSpace ↑K
F : Filter { x // x ∈ K }
F_cau : Cauchy F
inf_F : 𝓝 0 ⊓ F = ⊥
⊢ Cauchy (Filter.map (fun x => x⁻¹) F)
[PROOFSTEP]
let i : K →+* L := K.subtype
[GOAL]
K✝ : Type u_1
inst✝⁴ : Field K✝
inst✝³ : UniformSpace K✝
L : Type u_2
inst✝² : Field L
inst✝¹ : UniformSpace L
inst✝ : CompletableTopField L
K : Subfield L
src✝ : SeparatedSpace ↑↑K := Subtype.separatedSpace ↑K
F : Filter { x // x ∈ K }
F_cau : Cauchy F
inf_F : 𝓝 0 ⊓ F = ⊥
i : { x // x ∈ K } →+* L := subtype K
⊢ Cauchy (Filter.map (fun x => x⁻¹) F)
[PROOFSTEP]
have hi : UniformInducing i := uniformEmbedding_subtype_val.toUniformInducing
[GOAL]
K✝ : Type u_1
inst✝⁴ : Field K✝
inst✝³ : UniformSpace K✝
L : Type u_2
inst✝² : Field L
inst✝¹ : UniformSpace L
inst✝ : CompletableTopField L
K : Subfield L
src✝ : SeparatedSpace ↑↑K := Subtype.separatedSpace ↑K
F : Filter { x // x ∈ K }
F_cau : Cauchy F
inf_F : 𝓝 0 ⊓ F = ⊥
i : { x // x ∈ K } →+* L := subtype K
hi : UniformInducing ↑i
⊢ Cauchy (Filter.map (fun x => x⁻¹) F)
[PROOFSTEP]
rw [← hi.cauchy_map_iff] at F_cau ⊢
[GOAL]
K✝ : Type u_1
inst✝⁴ : Field K✝
inst✝³ : UniformSpace K✝
L : Type u_2
inst✝² : Field L
inst✝¹ : UniformSpace L
inst✝ : CompletableTopField L
K : Subfield L
src✝ : SeparatedSpace ↑↑K := Subtype.separatedSpace ↑K
F : Filter { x // x ∈ K }
inf_F : 𝓝 0 ⊓ F = ⊥
i : { x // x ∈ K } →+* L := subtype K
F_cau : Cauchy (Filter.map (↑i) F)
hi : UniformInducing ↑i
⊢ Cauchy (Filter.map (↑i) (Filter.map (fun x => x⁻¹) F))
[PROOFSTEP]
rw [map_comm (show (i ∘ fun x => x⁻¹) = (fun x => x⁻¹) ∘ i by ext; rfl)]
[GOAL]
K✝ : Type u_1
inst✝⁴ : Field K✝
inst✝³ : UniformSpace K✝
L : Type u_2
inst✝² : Field L
inst✝¹ : UniformSpace L
inst✝ : CompletableTopField L
K : Subfield L
src✝ : SeparatedSpace ↑↑K := Subtype.separatedSpace ↑K
F : Filter { x // x ∈ K }
inf_F : 𝓝 0 ⊓ F = ⊥
i : { x // x ∈ K } →+* L := subtype K
F_cau : Cauchy (Filter.map (↑i) F)
hi : UniformInducing ↑i
⊢ (↑i ∘ fun x => x⁻¹) = (fun x => x⁻¹) ∘ ↑i
[PROOFSTEP]
ext
[GOAL]
case h
K✝ : Type u_1
inst✝⁴ : Field K✝
inst✝³ : UniformSpace K✝
L : Type u_2
inst✝² : Field L
inst✝¹ : UniformSpace L
inst✝ : CompletableTopField L
K : Subfield L
src✝ : SeparatedSpace ↑↑K := Subtype.separatedSpace ↑K
F : Filter { x // x ∈ K }
inf_F : 𝓝 0 ⊓ F = ⊥
i : { x // x ∈ K } →+* L := subtype K
F_cau : Cauchy (Filter.map (↑i) F)
hi : UniformInducing ↑i
x✝ : { x // x ∈ K }
⊢ (↑i ∘ fun x => x⁻¹) x✝ = ((fun x => x⁻¹) ∘ ↑i) x✝
[PROOFSTEP]
rfl
[GOAL]
K✝ : Type u_1
inst✝⁴ : Field K✝
inst✝³ : UniformSpace K✝
L : Type u_2
inst✝² : Field L
inst✝¹ : UniformSpace L
inst✝ : CompletableTopField L
K : Subfield L
src✝ : SeparatedSpace ↑↑K := Subtype.separatedSpace ↑K
F : Filter { x // x ∈ K }
inf_F : 𝓝 0 ⊓ F = ⊥
i : { x // x ∈ K } →+* L := subtype K
F_cau : Cauchy (Filter.map (↑i) F)
hi : UniformInducing ↑i
⊢ Cauchy (Filter.map (fun x => x⁻¹) (Filter.map (↑i) F))
[PROOFSTEP]
apply CompletableTopField.nice _ F_cau
[GOAL]
K✝ : Type u_1
inst✝⁴ : Field K✝
inst✝³ : UniformSpace K✝
L : Type u_2
inst✝² : Field L
inst✝¹ : UniformSpace L
inst✝ : CompletableTopField L
K : Subfield L
src✝ : SeparatedSpace ↑↑K := Subtype.separatedSpace ↑K
F : Filter { x // x ∈ K }
inf_F : 𝓝 0 ⊓ F = ⊥
i : { x // x ∈ K } →+* L := subtype K
F_cau : Cauchy (Filter.map (↑i) F)
hi : UniformInducing ↑i
⊢ 𝓝 0 ⊓ Filter.map (↑i) F = ⊥
[PROOFSTEP]
rw [← Filter.push_pull', ← map_zero i, ← hi.inducing.nhds_eq_comap, inf_F, Filter.map_bot]
[GOAL]
K : Type u_1
inst✝⁹ : Field K
inst✝⁸ : UniformSpace K
L✝ : Type u_2
inst✝⁷ : Field L✝
inst✝⁶ : UniformSpace L✝
inst✝⁵ : CompletableTopField L✝
L : Type u_3
inst✝⁴ : Field L
inst✝³ : UniformSpace L
inst✝² : TopologicalDivisionRing L
inst✝¹ : SeparatedSpace L
inst✝ : CompleteSpace L
src✝ : SeparatedSpace L := inst✝¹
F : Filter L
cau_F : Cauchy F
hF : 𝓝 0 ⊓ F = ⊥
⊢ Cauchy (map (fun x => x⁻¹) F)
[PROOFSTEP]
haveI : NeBot F := cau_F.1
[GOAL]
K : Type u_1
inst✝⁹ : Field K
inst✝⁸ : UniformSpace K
L✝ : Type u_2
inst✝⁷ : Field L✝
inst✝⁶ : UniformSpace L✝
inst✝⁵ : CompletableTopField L✝
L : Type u_3
inst✝⁴ : Field L
inst✝³ : UniformSpace L
inst✝² : TopologicalDivisionRing L
inst✝¹ : SeparatedSpace L
inst✝ : CompleteSpace L
src✝ : SeparatedSpace L := inst✝¹
F : Filter L
cau_F : Cauchy F
hF : 𝓝 0 ⊓ F = ⊥
this : NeBot F
⊢ Cauchy (map (fun x => x⁻¹) F)
[PROOFSTEP]
rcases CompleteSpace.complete cau_F with ⟨x, hx⟩
[GOAL]
case intro
K : Type u_1
inst✝⁹ : Field K
inst✝⁸ : UniformSpace K
L✝ : Type u_2
inst✝⁷ : Field L✝
inst✝⁶ : UniformSpace L✝
inst✝⁵ : CompletableTopField L✝
L : Type u_3
inst✝⁴ : Field L
inst✝³ : UniformSpace L
inst✝² : TopologicalDivisionRing L
inst✝¹ : SeparatedSpace L
inst✝ : CompleteSpace L
src✝ : SeparatedSpace L := inst✝¹
F : Filter L
cau_F : Cauchy F
hF : 𝓝 0 ⊓ F = ⊥
this : NeBot F
x : L
hx : F ≤ 𝓝 x
⊢ Cauchy (map (fun x => x⁻¹) F)
[PROOFSTEP]
have hx' : x ≠ 0 := by
  rintro rfl
  rw [inf_eq_right.mpr hx] at hF
  exact cau_F.1.ne hF
[GOAL]
K : Type u_1
inst✝⁹ : Field K
inst✝⁸ : UniformSpace K
L✝ : Type u_2
inst✝⁷ : Field L✝
inst✝⁶ : UniformSpace L✝
inst✝⁵ : CompletableTopField L✝
L : Type u_3
inst✝⁴ : Field L
inst✝³ : UniformSpace L
inst✝² : TopologicalDivisionRing L
inst✝¹ : SeparatedSpace L
inst✝ : CompleteSpace L
src✝ : SeparatedSpace L := inst✝¹
F : Filter L
cau_F : Cauchy F
hF : 𝓝 0 ⊓ F = ⊥
this : NeBot F
x : L
hx : F ≤ 𝓝 x
⊢ x ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
K : Type u_1
inst✝⁹ : Field K
inst✝⁸ : UniformSpace K
L✝ : Type u_2
inst✝⁷ : Field L✝
inst✝⁶ : UniformSpace L✝
inst✝⁵ : CompletableTopField L✝
L : Type u_3
inst✝⁴ : Field L
inst✝³ : UniformSpace L
inst✝² : TopologicalDivisionRing L
inst✝¹ : SeparatedSpace L
inst✝ : CompleteSpace L
src✝ : SeparatedSpace L := inst✝¹
F : Filter L
cau_F : Cauchy F
hF : 𝓝 0 ⊓ F = ⊥
this : NeBot F
hx : F ≤ 𝓝 0
⊢ False
[PROOFSTEP]
rw [inf_eq_right.mpr hx] at hF
[GOAL]
K : Type u_1
inst✝⁹ : Field K
inst✝⁸ : UniformSpace K
L✝ : Type u_2
inst✝⁷ : Field L✝
inst✝⁶ : UniformSpace L✝
inst✝⁵ : CompletableTopField L✝
L : Type u_3
inst✝⁴ : Field L
inst✝³ : UniformSpace L
inst✝² : TopologicalDivisionRing L
inst✝¹ : SeparatedSpace L
inst✝ : CompleteSpace L
src✝ : SeparatedSpace L := inst✝¹
F : Filter L
cau_F : Cauchy F
hF : F = ⊥
this : NeBot F
hx : F ≤ 𝓝 0
⊢ False
[PROOFSTEP]
exact cau_F.1.ne hF
[GOAL]
case intro
K : Type u_1
inst✝⁹ : Field K
inst✝⁸ : UniformSpace K
L✝ : Type u_2
inst✝⁷ : Field L✝
inst✝⁶ : UniformSpace L✝
inst✝⁵ : CompletableTopField L✝
L : Type u_3
inst✝⁴ : Field L
inst✝³ : UniformSpace L
inst✝² : TopologicalDivisionRing L
inst✝¹ : SeparatedSpace L
inst✝ : CompleteSpace L
src✝ : SeparatedSpace L := inst✝¹
F : Filter L
cau_F : Cauchy F
hF : 𝓝 0 ⊓ F = ⊥
this : NeBot F
x : L
hx : F ≤ 𝓝 x
hx' : x ≠ 0
⊢ Cauchy (map (fun x => x⁻¹) F)
[PROOFSTEP]
exact
  Filter.Tendsto.cauchy_map
    (calc
      map (fun x => x⁻¹) F ≤ map (fun x => x⁻¹) (𝓝 x) := map_mono hx
      _ ≤ 𝓝 x⁻¹ := continuousAt_inv₀ hx')


[GOAL]
M : Type u_1
X : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : TopologicalSpace X
⊢ instTopologicalSpaceUnits = TopologicalSpace.induced val inst✝² ⊓ TopologicalSpace.induced (fun u => ↑u⁻¹) inst✝²
[PROOFSTEP]
simp only [inducing_embedProduct.1, instTopologicalSpaceProd, induced_inf, instTopologicalSpaceMulOpposite,
  induced_compose]
[GOAL]
M : Type u_1
X : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : TopologicalSpace X
⊢ TopologicalSpace.induced (Prod.fst ∘ ↑(embedProduct M)) inst✝² ⊓
      TopologicalSpace.induced ((unop ∘ Prod.snd) ∘ ↑(embedProduct M)) inst✝² =
    TopologicalSpace.induced val inst✝² ⊓ TopologicalSpace.induced (fun u => ↑u⁻¹) inst✝²
[PROOFSTEP]
rfl
[GOAL]
M✝ : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Monoid M✝
inst✝² : TopologicalSpace X
M : Type u_3
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x | IsUnit x}
hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹
⊢ Embedding val
[PROOFSTEP]
refine ⟨⟨?_⟩, ext⟩
[GOAL]
M✝ : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Monoid M✝
inst✝² : TopologicalSpace X
M : Type u_3
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x | IsUnit x}
hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹
⊢ instTopologicalSpaceUnits = TopologicalSpace.induced val inst✝
[PROOFSTEP]
rw [topology_eq_inf, inf_eq_left, ← continuous_iff_le_induced, @continuous_iff_continuousAt _ _ (.induced _ _)]
[GOAL]
M✝ : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Monoid M✝
inst✝² : TopologicalSpace X
M : Type u_3
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x | IsUnit x}
hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹
⊢ ∀ (x : Mˣ), ContinuousAt (fun u => ↑u⁻¹) x
[PROOFSTEP]
intros u s hs
[GOAL]
M✝ : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Monoid M✝
inst✝² : TopologicalSpace X
M : Type u_3
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x | IsUnit x}
hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹
u : Mˣ
s : Set M
hs : s ∈ 𝓝 ((fun u => ↑u⁻¹) u)
⊢ s ∈ Filter.map (fun u => ↑u⁻¹) (𝓝 u)
[PROOFSTEP]
simp only [← hf, nhds_induced, Filter.mem_map] at hs ⊢
[GOAL]
M✝ : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Monoid M✝
inst✝² : TopologicalSpace X
M : Type u_3
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x | IsUnit x}
hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹
u : Mˣ
s : Set M
hs : s ∈ 𝓝 (f ↑u)
⊢ (fun u => f ↑u) ⁻¹' s ∈ comap val (𝓝 ↑u)
[PROOFSTEP]
exact ⟨_, mem_inf_principal.1 (hc u u.isUnit hs), fun u' hu' ↦ hu' u'.isUnit⟩
[GOAL]
M : Type u_1
X : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : TopologicalSpace X
f : X → Mˣ
⊢ Continuous f ↔ Continuous (val ∘ f) ∧ Continuous fun x => ↑(f x)⁻¹
[PROOFSTEP]
simp only [inducing_embedProduct.continuous_iff, embedProduct_apply, (· ∘ ·), continuous_prod_mk,
  opHomeomorph.symm.inducing.continuous_iff, opHomeomorph_symm_apply, unop_op]


[GOAL]
M : Type u_1
X : Type u_2
Y : Type u_3
α : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : SMul M X
inst✝² : ContinuousSMul M X
f : Y → M
g : Y → X
b : Y
s : Set Y
inst✝¹ : SMul Mᵐᵒᵖ X
inst✝ : IsCentralScalar M X
⊢ Continuous fun p => p.fst • p.snd
[PROOFSTEP]
suffices Continuous fun p : M × X => MulOpposite.op p.fst • p.snd from
  this.comp (MulOpposite.continuous_unop.prod_map continuous_id)
[GOAL]
M : Type u_1
X : Type u_2
Y : Type u_3
α : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : SMul M X
inst✝² : ContinuousSMul M X
f : Y → M
g : Y → X
b : Y
s : Set Y
inst✝¹ : SMul Mᵐᵒᵖ X
inst✝ : IsCentralScalar M X
⊢ Continuous fun p => MulOpposite.op p.fst • p.snd
[PROOFSTEP]
simpa only [op_smul_eq_smul] using (continuous_smul : Continuous fun p : M × X => _)
[GOAL]
ι : Sort u_1
M : Type u_2
X : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : SMul M X
ts : Set (TopologicalSpace X)
h : ∀ (t : TopologicalSpace X), t ∈ ts → ContinuousSMul M X
⊢ Continuous fun p => p.fst • p.snd
[PROOFSTEP]
rw [← (@sInf_singleton _ _ ‹TopologicalSpace M› :)]
[GOAL]
ι : Sort u_1
M : Type u_2
X : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : SMul M X
ts : Set (TopologicalSpace X)
h : ∀ (t : TopologicalSpace X), t ∈ ts → ContinuousSMul M X
⊢ Continuous fun p => p.fst • p.snd
[PROOFSTEP]
exact
  continuous_sInf_rng.2 fun t ht =>
    continuous_sInf_dom₂ (Eq.refl _) ht (@ContinuousSMul.continuous_smul _ _ _ _ t (h t ht))
[GOAL]
ι : Sort u_1
M : Type u_2
X : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : SMul M X
t₁ t₂ : TopologicalSpace X
inst✝¹ : ContinuousSMul M X
inst✝ : ContinuousSMul M X
⊢ ContinuousSMul M X
[PROOFSTEP]
rw [inf_eq_iInf]
[GOAL]
ι : Sort u_1
M : Type u_2
X : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : SMul M X
t₁ t₂ : TopologicalSpace X
inst✝¹ : ContinuousSMul M X
inst✝ : ContinuousSMul M X
⊢ ContinuousSMul M X
[PROOFSTEP]
refine' continuousSMul_iInf fun b => _
[GOAL]
ι : Sort u_1
M : Type u_2
X : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : SMul M X
t₁ t₂ : TopologicalSpace X
inst✝¹ : ContinuousSMul M X
inst✝ : ContinuousSMul M X
b : Bool
⊢ ContinuousSMul M X
[PROOFSTEP]
cases b
[GOAL]
case false
ι : Sort u_1
M : Type u_2
X : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : SMul M X
t₁ t₂ : TopologicalSpace X
inst✝¹ : ContinuousSMul M X
inst✝ : ContinuousSMul M X
⊢ ContinuousSMul M X
[PROOFSTEP]
assumption
[GOAL]
case true
ι : Sort u_1
M : Type u_2
X : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : SMul M X
t₁ t₂ : TopologicalSpace X
inst✝¹ : ContinuousSMul M X
inst✝ : ContinuousSMul M X
⊢ ContinuousSMul M X
[PROOFSTEP]
assumption
[GOAL]
G : Type u_1
P : Type u_2
inst✝⁵ : AddGroup G
inst✝⁴ : AddTorsor G P
inst✝³ : TopologicalSpace G
inst✝² : PreconnectedSpace G
inst✝¹ : TopologicalSpace P
inst✝ : ContinuousVAdd G P
⊢ IsPreconnected Set.univ
[PROOFSTEP]
convert
  isPreconnected_univ.image (Equiv.vaddConst (Classical.arbitrary P) : G → P)
    (continuous_id.vadd continuous_const).continuousOn
[GOAL]
case h.e'_3
G : Type u_1
P : Type u_2
inst✝⁵ : AddGroup G
inst✝⁴ : AddTorsor G P
inst✝³ : TopologicalSpace G
inst✝² : PreconnectedSpace G
inst✝¹ : TopologicalSpace P
inst✝ : ContinuousVAdd G P
⊢ Set.univ = ↑(Equiv.vaddConst (Classical.arbitrary P)) '' Set.univ
[PROOFSTEP]
rw [Set.image_univ, Equiv.range_eq_univ]