[GOAL]
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b c d : α
⊢ 𝓝ˢ (Ici a) = 𝓝 a ⊔ 𝓟 (Ioi a)
[PROOFSTEP]
rw [← Ioi_insert, nhdsSet_insert, nhdsSet_Ioi]
[GOAL]
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b c d : α
h : a < b
⊢ 𝓝ˢ (Ico a b) = 𝓝 a ⊔ 𝓟 (Ioo a b)
[PROOFSTEP]
rw [← Ioo_insert_left h, nhdsSet_insert, nhdsSet_Ioo]
[GOAL]
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b c d : α
h : a < b
⊢ 𝓝ˢ (Ioc a b) = 𝓝 b ⊔ 𝓟 (Ioo a b)
[PROOFSTEP]
rw [← Ioo_insert_right h, nhdsSet_insert, nhdsSet_Ioo]
[GOAL]
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b c d : α
h : a ≤ b
⊢ 𝓝ˢ (Icc a b) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)
[PROOFSTEP]
rcases h.eq_or_lt with rfl | hlt
[GOAL]
case inl
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a c d : α
h : a ≤ a
⊢ 𝓝ˢ (Icc a a) = 𝓝 a ⊔ 𝓝 a ⊔ 𝓟 (Ioo a a)
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b c d : α
h : a ≤ b
hlt : a < b
⊢ 𝓝ˢ (Icc a b) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)
[PROOFSTEP]
rw [← Ioc_insert_left h, nhdsSet_insert, nhdsSet_Ioc hlt, sup_assoc]
[GOAL]
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b c d : α
⊢ Ioi a ∈ 𝓝ˢ (Ici b) ↔ a < b
[PROOFSTEP]
rw [isOpen_Ioi.mem_nhdsSet, Ici_subset_Ioi]
[GOAL]
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b c d : α
h : b ≤ c
⊢ Iio c ∈ 𝓝ˢ (Iio b)
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b c d : α
h : a ≤ b
⊢ Ioi a ∈ 𝓝ˢ (Ioi b)
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a : α
h : Nonempty ↑(Ioi a)
⊢ HasBasis (𝓝ˢ (Iic a)) (fun x => a < x) Iio
[PROOFSTEP]
refine ⟨fun s ↦ ⟨fun hs ↦ ?_, fun ⟨b, hab, hb⟩ ↦ mem_of_superset (Iio_mem_nhdsSet_Iic hab) hb⟩⟩
[GOAL]
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a : α
h : Nonempty ↑(Ioi a)
s : Set α
hs : s ∈ 𝓝ˢ (Iic a)
⊢ ∃ i, a < i ∧ Iio i ⊆ s
[PROOFSTEP]
rw [nhdsSet_Iic, mem_sup, mem_principal] at hs
[GOAL]
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a : α
h : Nonempty ↑(Ioi a)
s : Set α
hs : s ∈ 𝓝 a ∧ Iio a ⊆ s
⊢ ∃ i, a < i ∧ Iio i ⊆ s
[PROOFSTEP]
rcases exists_Ico_subset_of_mem_nhds hs.1 (Set.nonempty_coe_sort.1 h) with ⟨b, hab, hbs⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a : α
h : Nonempty ↑(Ioi a)
s : Set α
hs : s ∈ 𝓝 a ∧ Iio a ⊆ s
b : α
hab : a < b
hbs : Ico a b ⊆ s
⊢ ∃ i, a < i ∧ Iio i ⊆ s
[PROOFSTEP]
exact ⟨b, hab, Iio_subset_Iio_union_Ico.trans (union_subset hs.2 hbs)⟩
[GOAL]
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
a : α
inst✝ : NeBot (𝓝[Ioi a] a)
⊢ HasBasis (𝓝ˢ (Iic a)) (fun x => a < x) Iic
[PROOFSTEP]
have : Nonempty (Ioi a) := (Filter.nonempty_of_mem (self_mem_nhdsWithin : Ioi a ∈ 𝓝[>] a)).to_subtype
[GOAL]
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
a : α
inst✝ : NeBot (𝓝[Ioi a] a)
this : Nonempty ↑(Ioi a)
⊢ HasBasis (𝓝ˢ (Iic a)) (fun x => a < x) Iic
[PROOFSTEP]
refine (hasBasis_nhdsSet_Iic_Iio _).to_hasBasis (fun c hc ↦ ?_) (fun _ h ↦ ⟨_, h, Iio_subset_Iic_self⟩)
[GOAL]
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
a : α
inst✝ : NeBot (𝓝[Ioi a] a)
this : Nonempty ↑(Ioi a)
c : α
hc : a < c
⊢ ∃ i', a < i' ∧ Iic i' ⊆ Iio c
[PROOFSTEP]
simpa only [Iic_subset_Iio] using (Filter.nonempty_of_mem <| Ioo_mem_nhdsWithin_Ioi' hc)


[GOAL]
K : Subfield ℂ
hc : IsClosed ↑K
⊢ K = RingHom.fieldRange ofReal ∨ K = ⊤
[PROOFSTEP]
suffices range (ofReal' : ℝ → ℂ) ⊆ K
  by
  rw [range_subset_iff, ← coe_algebraMap] at this
  have :=
    (Subalgebra.isSimpleOrder_of_finrank finrank_real_complex).eq_bot_or_eq_top
      (Subfield.toIntermediateField K this).toSubalgebra
  simp_rw [← SetLike.coe_set_eq] at this ⊢
  convert this using 2
  simp only [RingHom.coe_fieldRange, Algebra.coe_bot, coe_algebraMap]
  rfl
[GOAL]
K : Subfield ℂ
hc : IsClosed ↑K
this : range ofReal' ⊆ ↑K
⊢ K = RingHom.fieldRange ofReal ∨ K = ⊤
[PROOFSTEP]
rw [range_subset_iff, ← coe_algebraMap] at this
[GOAL]
K : Subfield ℂ
hc : IsClosed ↑K
this : ∀ (y : ℝ), ↑(algebraMap ℝ ℂ) y ∈ ↑K
⊢ K = RingHom.fieldRange ofReal ∨ K = ⊤
[PROOFSTEP]
have :=
  (Subalgebra.isSimpleOrder_of_finrank finrank_real_complex).eq_bot_or_eq_top
    (Subfield.toIntermediateField K this).toSubalgebra
[GOAL]
K : Subfield ℂ
hc : IsClosed ↑K
this✝ : ∀ (y : ℝ), ↑(algebraMap ℝ ℂ) y ∈ ↑K
this : (Subfield.toIntermediateField K this✝).toSubalgebra = ⊥ ∨ (Subfield.toIntermediateField K this✝).toSubalgebra = ⊤
⊢ K = RingHom.fieldRange ofReal ∨ K = ⊤
[PROOFSTEP]
simp_rw [← SetLike.coe_set_eq] at this ⊢
[GOAL]
K : Subfield ℂ
hc : IsClosed ↑K
this✝ : ∀ (y : ℝ), ↑(algebraMap ℝ ℂ) y ∈ ↑K
this :
  ↑(Subfield.toIntermediateField K this✝).toSubalgebra = ↑⊥ ∨ ↑(Subfield.toIntermediateField K this✝).toSubalgebra = ↑⊤
⊢ ↑K = ↑(RingHom.fieldRange ofReal) ∨ ↑K = ↑⊤
[PROOFSTEP]
convert this using 2
[GOAL]
case h.e'_1.h.e'_3
K : Subfield ℂ
hc : IsClosed ↑K
this✝ : ∀ (y : ℝ), ↑(algebraMap ℝ ℂ) y ∈ ↑K
this :
  ↑(Subfield.toIntermediateField K this✝).toSubalgebra = ↑⊥ ∨ ↑(Subfield.toIntermediateField K this✝).toSubalgebra = ↑⊤
⊢ ↑(RingHom.fieldRange ofReal) = ↑⊥
[PROOFSTEP]
simp only [RingHom.coe_fieldRange, Algebra.coe_bot, coe_algebraMap]
[GOAL]
case h.e'_1.h.e'_3
K : Subfield ℂ
hc : IsClosed ↑K
this✝ : ∀ (y : ℝ), ↑(algebraMap ℝ ℂ) y ∈ ↑K
this :
  ↑(Subfield.toIntermediateField K this✝).toSubalgebra = ↑⊥ ∨ ↑(Subfield.toIntermediateField K this✝).toSubalgebra = ↑⊤
⊢ range ↑ofReal = range ofReal'
[PROOFSTEP]
rfl
[GOAL]
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal' ⊆ ↑K
[PROOFSTEP]
suffices range (ofReal' : ℝ → ℂ) ⊆ closure (Set.range ((ofReal' : ℝ → ℂ) ∘ ((↑) : ℚ → ℝ)))
  by
  refine' subset_trans this _
  rw [← IsClosed.closure_eq hc]
  apply closure_mono
  rintro _ ⟨_, rfl⟩
  simp only [Function.comp_apply, ofReal_rat_cast, SetLike.mem_coe, SubfieldClass.coe_rat_mem]
[GOAL]
K : Subfield ℂ
hc : IsClosed ↑K
this : range ofReal' ⊆ closure (range (ofReal' ∘ Rat.cast))
⊢ range ofReal' ⊆ ↑K
[PROOFSTEP]
refine' subset_trans this _
[GOAL]
K : Subfield ℂ
hc : IsClosed ↑K
this : range ofReal' ⊆ closure (range (ofReal' ∘ Rat.cast))
⊢ closure (range (ofReal' ∘ Rat.cast)) ⊆ ↑K
[PROOFSTEP]
rw [← IsClosed.closure_eq hc]
[GOAL]
K : Subfield ℂ
hc : IsClosed ↑K
this : range ofReal' ⊆ closure (range (ofReal' ∘ Rat.cast))
⊢ closure (range (ofReal' ∘ Rat.cast)) ⊆ closure ↑K
[PROOFSTEP]
apply closure_mono
[GOAL]
case h
K : Subfield ℂ
hc : IsClosed ↑K
this : range ofReal' ⊆ closure (range (ofReal' ∘ Rat.cast))
⊢ range (ofReal' ∘ Rat.cast) ⊆ ↑K
[PROOFSTEP]
rintro _ ⟨_, rfl⟩
[GOAL]
case h.intro
K : Subfield ℂ
hc : IsClosed ↑K
this : range ofReal' ⊆ closure (range (ofReal' ∘ Rat.cast))
w✝ : ℚ
⊢ (ofReal' ∘ Rat.cast) w✝ ∈ ↑K
[PROOFSTEP]
simp only [Function.comp_apply, ofReal_rat_cast, SetLike.mem_coe, SubfieldClass.coe_rat_mem]
[GOAL]
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal' ⊆ closure (range (ofReal' ∘ Rat.cast))
[PROOFSTEP]
nth_rw 1 [range_comp]
[GOAL]
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal' ⊆ closure (ofReal' '' range Rat.cast)
[PROOFSTEP]
refine' subset_trans _ (image_closure_subset_closure_image continuous_ofReal)
[GOAL]
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal' ⊆ ofReal' '' closure (range Rat.cast)
[PROOFSTEP]
rw [DenseRange.closure_range Rat.denseEmbedding_coe_real.dense]
[GOAL]
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal' ⊆ ofReal' '' univ
[PROOFSTEP]
simp only [image_univ]
[GOAL]
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal' ⊆ range ofReal'
[PROOFSTEP]
rfl
[GOAL]
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
⊢ ψ.toFun = ↑(Subfield.subtype K) ∨ ψ.toFun = ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype K)
[PROOFSTEP]
letI : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
[GOAL]
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
⊢ ψ.toFun = ↑(Subfield.subtype K) ∨ ψ.toFun = ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype K)
[PROOFSTEP]
letI : TopologicalRing K.topologicalClosure := Subring.instTopologicalRing K.topologicalClosure.toSubring
[GOAL]
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
⊢ ψ.toFun = ↑(Subfield.subtype K) ∨ ψ.toFun = ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype K)
[PROOFSTEP]
set ι : K → K.topologicalClosure := ⇑(Subfield.inclusion K.le_topologicalClosure)
[GOAL]
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
⊢ ψ.toFun = ↑(Subfield.subtype K) ∨ ψ.toFun = ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype K)
[PROOFSTEP]
have ui : UniformInducing ι :=
  ⟨by
    erw [uniformity_subtype, uniformity_subtype, Filter.comap_comap]
    congr⟩
[GOAL]
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
⊢ Filter.comap (fun x => (ι x.fst, ι x.snd)) (uniformity { x // x ∈ Subfield.topologicalClosure K }) =
    uniformity { x // x ∈ K }
[PROOFSTEP]
erw [uniformity_subtype, uniformity_subtype, Filter.comap_comap]
[GOAL]
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
⊢ Filter.comap ((fun q => (↑q.fst, ↑q.snd)) ∘ fun x => (ι x.fst, ι x.snd)) (uniformity ℂ) =
    Filter.comap (fun q => (↑q.fst, ↑q.snd)) (uniformity ℂ)
[PROOFSTEP]
congr
[GOAL]
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
⊢ ψ.toFun = ↑(Subfield.subtype K) ∨ ψ.toFun = ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype K)
[PROOFSTEP]
let di := ui.denseInducing (?_ : DenseRange ι)
[GOAL]
case refine_2
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
⊢ ψ.toFun = ↑(Subfield.subtype K) ∨ ψ.toFun = ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype K)
[PROOFSTEP]
let extψ := DenseInducing.extendRingHom ui di.dense hc
[GOAL]
case refine_2
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
⊢ ψ.toFun = ↑(Subfield.subtype K) ∨ ψ.toFun = ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype K)
[PROOFSTEP]
haveI hψ := (uniformContinuous_uniformly_extend ui di.dense hc).continuous
[GOAL]
case refine_2
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
⊢ ψ.toFun = ↑(Subfield.subtype K) ∨ ψ.toFun = ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype K)
[PROOFSTEP]
cases' Complex.subfield_eq_of_closed (Subfield.isClosed_topologicalClosure K) with h h
[GOAL]
case refine_2.inl
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = RingHom.fieldRange ofReal
⊢ ψ.toFun = ↑(Subfield.subtype K) ∨ ψ.toFun = ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype K)
[PROOFSTEP]
left
[GOAL]
case refine_2.inl.h
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = RingHom.fieldRange ofReal
⊢ ψ.toFun = ↑(Subfield.subtype K)
[PROOFSTEP]
let j := RingEquiv.subfieldCongr h
[GOAL]
case refine_2.inl.h
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = RingHom.fieldRange ofReal
j : { x // x ∈ Subfield.topologicalClosure K } ≃+* { x // x ∈ RingHom.fieldRange ofReal } := RingEquiv.subfieldCongr h
⊢ ψ.toFun = ↑(Subfield.subtype K)
[PROOFSTEP]
let ψ₁ :=
  RingHom.comp extψ
    (RingHom.comp j.symm.toRingHom ofReal.rangeRestrict)
      -- porting note: was `by continuity!` and was used inline
[GOAL]
case refine_2.inl.h
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = RingHom.fieldRange ofReal
j : { x // x ∈ Subfield.topologicalClosure K } ≃+* { x // x ∈ RingHom.fieldRange ofReal } := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := RingHom.comp extψ (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm j)) (RingHom.rangeRestrict ofReal))
⊢ ψ.toFun = ↑(Subfield.subtype K)
[PROOFSTEP]
have hψ₁ : Continuous ψ₁ := by simpa only [RingHom.coe_comp] using hψ.comp ((continuous_algebraMap ℝ ℂ).subtype_mk _)
[GOAL]
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = RingHom.fieldRange ofReal
j : { x // x ∈ Subfield.topologicalClosure K } ≃+* { x // x ∈ RingHom.fieldRange ofReal } := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := RingHom.comp extψ (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm j)) (RingHom.rangeRestrict ofReal))
⊢ Continuous ↑ψ₁
[PROOFSTEP]
simpa only [RingHom.coe_comp] using hψ.comp ((continuous_algebraMap ℝ ℂ).subtype_mk _)
[GOAL]
case refine_2.inl.h
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = RingHom.fieldRange ofReal
j : { x // x ∈ Subfield.topologicalClosure K } ≃+* { x // x ∈ RingHom.fieldRange ofReal } := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := RingHom.comp extψ (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm j)) (RingHom.rangeRestrict ofReal))
hψ₁ : Continuous ↑ψ₁
⊢ ψ.toFun = ↑(Subfield.subtype K)
[PROOFSTEP]
ext1 x
[GOAL]
case refine_2.inl.h.h
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = RingHom.fieldRange ofReal
j : { x // x ∈ Subfield.topologicalClosure K } ≃+* { x // x ∈ RingHom.fieldRange ofReal } := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := RingHom.comp extψ (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm j)) (RingHom.rangeRestrict ofReal))
hψ₁ : Continuous ↑ψ₁
x : { x // x ∈ K }
⊢ OneHom.toFun (↑↑ψ) x = ↑(Subfield.subtype K) x
[PROOFSTEP]
rsuffices ⟨r, hr⟩ : ∃ r : ℝ, ofReal.rangeRestrict r = j (ι x)
[GOAL]
case refine_2.inl.h.h.intro
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = RingHom.fieldRange ofReal
j : { x // x ∈ Subfield.topologicalClosure K } ≃+* { x // x ∈ RingHom.fieldRange ofReal } := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := RingHom.comp extψ (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm j)) (RingHom.rangeRestrict ofReal))
hψ₁ : Continuous ↑ψ₁
x : { x // x ∈ K }
r : ℝ
hr : ↑(RingHom.rangeRestrict ofReal) r = ↑j (ι x)
⊢ OneHom.toFun (↑↑ψ) x = ↑(Subfield.subtype K) x
[PROOFSTEP]
have := RingHom.congr_fun (ringHom_eq_ofReal_of_continuous hψ₁) r
[GOAL]
case refine_2.inl.h.h.intro
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝¹ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this✝ : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = RingHom.fieldRange ofReal
j : { x // x ∈ Subfield.topologicalClosure K } ≃+* { x // x ∈ RingHom.fieldRange ofReal } := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := RingHom.comp extψ (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm j)) (RingHom.rangeRestrict ofReal))
hψ₁ : Continuous ↑ψ₁
x : { x // x ∈ K }
r : ℝ
hr : ↑(RingHom.rangeRestrict ofReal) r = ↑j (ι x)
this : ↑ψ₁ r = ↑ofReal r
⊢ OneHom.toFun (↑↑ψ) x = ↑(Subfield.subtype K) x
[PROOFSTEP]
rw [RingHom.comp_apply, RingHom.comp_apply, hr, RingEquiv.toRingHom_eq_coe] at this
[GOAL]
case refine_2.inl.h.h.intro
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝¹ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this✝ : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = RingHom.fieldRange ofReal
j : { x // x ∈ Subfield.topologicalClosure K } ≃+* { x // x ∈ RingHom.fieldRange ofReal } := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := RingHom.comp extψ (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm j)) (RingHom.rangeRestrict ofReal))
hψ₁ : Continuous ↑ψ₁
x : { x // x ∈ K }
r : ℝ
hr : ↑(RingHom.rangeRestrict ofReal) r = ↑j (ι x)
this : ↑extψ (↑↑(RingEquiv.symm j) (↑j (ι x))) = ↑ofReal r
⊢ OneHom.toFun (↑↑ψ) x = ↑(Subfield.subtype K) x
[PROOFSTEP]
convert this using 1
[GOAL]
case h.e'_2
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝¹ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this✝ : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = RingHom.fieldRange ofReal
j : { x // x ∈ Subfield.topologicalClosure K } ≃+* { x // x ∈ RingHom.fieldRange ofReal } := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := RingHom.comp extψ (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm j)) (RingHom.rangeRestrict ofReal))
hψ₁ : Continuous ↑ψ₁
x : { x // x ∈ K }
r : ℝ
hr : ↑(RingHom.rangeRestrict ofReal) r = ↑j (ι x)
this : ↑extψ (↑↑(RingEquiv.symm j) (↑j (ι x))) = ↑ofReal r
⊢ OneHom.toFun (↑↑ψ) x = ↑extψ (↑↑(RingEquiv.symm j) (↑j (ι x)))
[PROOFSTEP]
exact (DenseInducing.extend_eq di hc.continuous _).symm
[GOAL]
case h.e'_3
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝¹ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this✝ : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = RingHom.fieldRange ofReal
j : { x // x ∈ Subfield.topologicalClosure K } ≃+* { x // x ∈ RingHom.fieldRange ofReal } := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := RingHom.comp extψ (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm j)) (RingHom.rangeRestrict ofReal))
hψ₁ : Continuous ↑ψ₁
x : { x // x ∈ K }
r : ℝ
hr : ↑(RingHom.rangeRestrict ofReal) r = ↑j (ι x)
this : ↑extψ (↑↑(RingEquiv.symm j) (↑j (ι x))) = ↑ofReal r
⊢ ↑(Subfield.subtype K) x = ↑ofReal r
[PROOFSTEP]
rw [← ofReal.coe_rangeRestrict, hr]
[GOAL]
case h.e'_3
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝¹ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this✝ : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = RingHom.fieldRange ofReal
j : { x // x ∈ Subfield.topologicalClosure K } ≃+* { x // x ∈ RingHom.fieldRange ofReal } := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := RingHom.comp extψ (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm j)) (RingHom.rangeRestrict ofReal))
hψ₁ : Continuous ↑ψ₁
x : { x // x ∈ K }
r : ℝ
hr : ↑(RingHom.rangeRestrict ofReal) r = ↑j (ι x)
this : ↑extψ (↑↑(RingEquiv.symm j) (↑j (ι x))) = ↑ofReal r
⊢ ↑(Subfield.subtype K) x = ↑(↑j (ι x))
[PROOFSTEP]
rfl
[GOAL]
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = RingHom.fieldRange ofReal
j : { x // x ∈ Subfield.topologicalClosure K } ≃+* { x // x ∈ RingHom.fieldRange ofReal } := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := RingHom.comp extψ (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm j)) (RingHom.rangeRestrict ofReal))
hψ₁ : Continuous ↑ψ₁
x : { x // x ∈ K }
⊢ ∃ r, ↑(RingHom.rangeRestrict ofReal) r = ↑j (ι x)
[PROOFSTEP]
obtain ⟨r, hr⟩ := SetLike.coe_mem (j (ι x))
[GOAL]
case intro
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = RingHom.fieldRange ofReal
j : { x // x ∈ Subfield.topologicalClosure K } ≃+* { x // x ∈ RingHom.fieldRange ofReal } := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := RingHom.comp extψ (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm j)) (RingHom.rangeRestrict ofReal))
hψ₁ : Continuous ↑ψ₁
x : { x // x ∈ K }
r : ℝ
hr : ↑ofReal r = ↑(↑j (ι x))
⊢ ∃ r, ↑(RingHom.rangeRestrict ofReal) r = ↑j (ι x)
[PROOFSTEP]
exact ⟨r, Subtype.ext hr⟩
[GOAL]
case refine_2.inr
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = ⊤
⊢ ψ.toFun = ↑(Subfield.subtype K) ∨ ψ.toFun = ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype K)
[PROOFSTEP]
let ψ₁ :=
  RingHom.comp extψ
    (RingHom.comp (RingEquiv.subfieldCongr h).symm.toRingHom (@Subfield.topEquiv ℂ _).symm.toRingHom)
      -- porting note: was `by continuity!` and was used inline
[GOAL]
case refine_2.inr
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = ⊤
ψ₁ : ℂ →+* ℂ :=
  RingHom.comp extψ
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.subfieldCongr h)))
      (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
⊢ ψ.toFun = ↑(Subfield.subtype K) ∨ ψ.toFun = ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype K)
[PROOFSTEP]
have hψ₁ : Continuous ψ₁ := by simpa only [RingHom.coe_comp] using hψ.comp (continuous_id.subtype_mk _)
[GOAL]
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = ⊤
ψ₁ : ℂ →+* ℂ :=
  RingHom.comp extψ
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.subfieldCongr h)))
      (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
⊢ Continuous ↑ψ₁
[PROOFSTEP]
simpa only [RingHom.coe_comp] using hψ.comp (continuous_id.subtype_mk _)
[GOAL]
case refine_2.inr
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = ⊤
ψ₁ : ℂ →+* ℂ :=
  RingHom.comp extψ
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.subfieldCongr h)))
      (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
hψ₁ : Continuous ↑ψ₁
⊢ ψ.toFun = ↑(Subfield.subtype K) ∨ ψ.toFun = ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype K)
[PROOFSTEP]
cases' ringHom_eq_id_or_conj_of_continuous hψ₁ with h h
[GOAL]
case refine_2.inr.inl
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h✝ : Subfield.topologicalClosure K = ⊤
ψ₁ : ℂ →+* ℂ :=
  RingHom.comp extψ
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.subfieldCongr h✝)))
      (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
hψ₁ : Continuous ↑ψ₁
h : ψ₁ = RingHom.id ℂ
⊢ ψ.toFun = ↑(Subfield.subtype K) ∨ ψ.toFun = ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype K)
[PROOFSTEP]
left
[GOAL]
case refine_2.inr.inl.h
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h✝ : Subfield.topologicalClosure K = ⊤
ψ₁ : ℂ →+* ℂ :=
  RingHom.comp extψ
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.subfieldCongr h✝)))
      (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
hψ₁ : Continuous ↑ψ₁
h : ψ₁ = RingHom.id ℂ
⊢ ψ.toFun = ↑(Subfield.subtype K)
[PROOFSTEP]
ext1 z
[GOAL]
case refine_2.inr.inl.h.h
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h✝ : Subfield.topologicalClosure K = ⊤
ψ₁ : ℂ →+* ℂ :=
  RingHom.comp extψ
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.subfieldCongr h✝)))
      (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
hψ₁ : Continuous ↑ψ₁
h : ψ₁ = RingHom.id ℂ
z : { x // x ∈ K }
⊢ OneHom.toFun (↑↑ψ) z = ↑(Subfield.subtype K) z
[PROOFSTEP]
convert RingHom.congr_fun h z using 1
[GOAL]
case h.e'_2
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h✝ : Subfield.topologicalClosure K = ⊤
ψ₁ : ℂ →+* ℂ :=
  RingHom.comp extψ
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.subfieldCongr h✝)))
      (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
hψ₁ : Continuous ↑ψ₁
h : ψ₁ = RingHom.id ℂ
z : { x // x ∈ K }
⊢ OneHom.toFun (↑↑ψ) z = ↑ψ₁ ↑z
[PROOFSTEP]
exact (DenseInducing.extend_eq di hc.continuous z).symm
[GOAL]
case refine_2.inr.inr
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h✝ : Subfield.topologicalClosure K = ⊤
ψ₁ : ℂ →+* ℂ :=
  RingHom.comp extψ
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.subfieldCongr h✝)))
      (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
hψ₁ : Continuous ↑ψ₁
h : ψ₁ = starRingEnd ℂ
⊢ ψ.toFun = ↑(Subfield.subtype K) ∨ ψ.toFun = ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype K)
[PROOFSTEP]
right
[GOAL]
case refine_2.inr.inr.h
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h✝ : Subfield.topologicalClosure K = ⊤
ψ₁ : ℂ →+* ℂ :=
  RingHom.comp extψ
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.subfieldCongr h✝)))
      (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
hψ₁ : Continuous ↑ψ₁
h : ψ₁ = starRingEnd ℂ
⊢ ψ.toFun = ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype K)
[PROOFSTEP]
ext1 z
[GOAL]
case refine_2.inr.inr.h.h
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h✝ : Subfield.topologicalClosure K = ⊤
ψ₁ : ℂ →+* ℂ :=
  RingHom.comp extψ
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.subfieldCongr h✝)))
      (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
hψ₁ : Continuous ↑ψ₁
h : ψ₁ = starRingEnd ℂ
z : { x // x ∈ K }
⊢ OneHom.toFun (↑↑ψ) z = (↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype K)) z
[PROOFSTEP]
convert RingHom.congr_fun h z using 1
[GOAL]
case h.e'_2
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h✝ : Subfield.topologicalClosure K = ⊤
ψ₁ : ℂ →+* ℂ :=
  RingHom.comp extψ
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.subfieldCongr h✝)))
      (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
hψ₁ : Continuous ↑ψ₁
h : ψ₁ = starRingEnd ℂ
z : { x // x ∈ K }
⊢ OneHom.toFun (↑↑ψ) z = ↑ψ₁ ↑z
[PROOFSTEP]
exact (DenseInducing.extend_eq di hc.continuous z).symm
[GOAL]
case refine_1
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
⊢ DenseRange ι
[PROOFSTEP]
let j : { x // x ∈ closure (id '' {x | (K : Set ℂ) x}) } → (K.topologicalClosure : Set ℂ) := fun x =>
  ⟨x, by
    convert x.prop
    simp only [id.def, Set.image_id']
    rfl⟩
[GOAL]
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
x : { x // x ∈ closure (id '' {x | ↑K x}) }
⊢ ↑x ∈ ↑(Subfield.topologicalClosure K)
[PROOFSTEP]
convert x.prop
[GOAL]
case h.e'_5
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
x : { x // x ∈ closure (id '' {x | ↑K x}) }
⊢ ↑(Subfield.topologicalClosure K) = closure (id '' {x | ↑K x})
[PROOFSTEP]
simp only [id.def, Set.image_id']
[GOAL]
case h.e'_5
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
x : { x // x ∈ closure (id '' {x | ↑K x}) }
⊢ ↑(Subfield.topologicalClosure K) = closure {x | ↑K x}
[PROOFSTEP]
rfl
[GOAL]
case refine_1
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
j : { x // x ∈ closure (id '' {x | ↑K x}) } → ↑↑(Subfield.topologicalClosure K) :=
  fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(Subfield.topologicalClosure K)) }
⊢ DenseRange ι
[PROOFSTEP]
convert
  DenseRange.comp (Function.Surjective.denseRange _) (DenseEmbedding.subtype denseEmbedding_id (K : Set ℂ)).dense
    (by continuity : Continuous j)
[GOAL]
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
j : { x // x ∈ closure (id '' {x | ↑K x}) } → ↑↑(Subfield.topologicalClosure K) :=
  fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(Subfield.topologicalClosure K)) }
⊢ Continuous j
[PROOFSTEP]
continuity
[GOAL]
case refine_1
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
j : { x // x ∈ closure (id '' {x | ↑K x}) } → ↑↑(Subfield.topologicalClosure K) :=
  fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(Subfield.topologicalClosure K)) }
⊢ Function.Surjective j
[PROOFSTEP]
rintro ⟨y, hy⟩
[GOAL]
case refine_1.mk
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
j : { x // x ∈ closure (id '' {x | ↑K x}) } → ↑↑(Subfield.topologicalClosure K) :=
  fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(Subfield.topologicalClosure K)) }
y : ℂ
hy : y ∈ ↑(Subfield.topologicalClosure K)
⊢ ∃ a, j a = { val := y, property := hy }
[PROOFSTEP]
use⟨y, by
    convert hy
    simp only [id.def, Set.image_id']
    rfl⟩
[GOAL]
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
j : { x // x ∈ closure (id '' {x | ↑K x}) } → ↑↑(Subfield.topologicalClosure K) :=
  fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(Subfield.topologicalClosure K)) }
y : ℂ
hy : y ∈ ↑(Subfield.topologicalClosure K)
⊢ y ∈ closure (id '' {x | ↑K x})
[PROOFSTEP]
convert hy
[GOAL]
case h.e'_5
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
j : { x // x ∈ closure (id '' {x | ↑K x}) } → ↑↑(Subfield.topologicalClosure K) :=
  fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(Subfield.topologicalClosure K)) }
y : ℂ
hy : y ∈ ↑(Subfield.topologicalClosure K)
⊢ closure (id '' {x | ↑K x}) = ↑(Subfield.topologicalClosure K)
[PROOFSTEP]
simp only [id.def, Set.image_id']
[GOAL]
case h.e'_5
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
j : { x // x ∈ closure (id '' {x | ↑K x}) } → ↑↑(Subfield.topologicalClosure K) :=
  fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(Subfield.topologicalClosure K)) }
y : ℂ
hy : y ∈ ↑(Subfield.topologicalClosure K)
⊢ closure {x | ↑K x} = ↑(Subfield.topologicalClosure K)
[PROOFSTEP]
rfl


[GOAL]
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
⊢ ∀ (s : Set β), IsOpen s → lim f ∈ s → ↑f ⁻¹' s ∈ atTop
[PROOFSTEP]
intro s os lfs
[GOAL]
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
⊢ ↑f ⁻¹' s ∈ atTop
[PROOFSTEP]
suffices ∃ a : ℕ, ∀ b : ℕ, b ≥ a → f b ∈ s by simpa using this
[GOAL]
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
this : ∃ a, ∀ (b : ℕ), b ≥ a → ↑f b ∈ s
⊢ ↑f ⁻¹' s ∈ atTop
[PROOFSTEP]
simpa using this
[GOAL]
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → ↑f b ∈ s
[PROOFSTEP]
rcases Metric.isOpen_iff.1 os _ lfs with ⟨ε, ⟨hε, hεs⟩⟩
[GOAL]
case intro.intro
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
ε : ℝ
hε : ε > 0
hεs : Metric.ball (lim f) ε ⊆ s
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → ↑f b ∈ s
[PROOFSTEP]
cases' Setoid.symm (CauSeq.equiv_lim f) _ hε with N hN
[GOAL]
case intro.intro.intro
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
ε : ℝ
hε : ε > 0
hεs : Metric.ball (lim f) ε ⊆ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(const norm (lim f) - f) j‖ < ε
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → ↑f b ∈ s
[PROOFSTEP]
exists N
[GOAL]
case intro.intro.intro
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
ε : ℝ
hε : ε > 0
hεs : Metric.ball (lim f) ε ⊆ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(const norm (lim f) - f) j‖ < ε
⊢ ∀ (b : ℕ), b ≥ N → ↑f b ∈ s
[PROOFSTEP]
intro b hb
[GOAL]
case intro.intro.intro
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
ε : ℝ
hε : ε > 0
hεs : Metric.ball (lim f) ε ⊆ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(const norm (lim f) - f) j‖ < ε
b : ℕ
hb : b ≥ N
⊢ ↑f b ∈ s
[PROOFSTEP]
apply hεs
[GOAL]
case intro.intro.intro.a
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
ε : ℝ
hε : ε > 0
hεs : Metric.ball (lim f) ε ⊆ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(const norm (lim f) - f) j‖ < ε
b : ℕ
hb : b ≥ N
⊢ ↑f b ∈ Metric.ball (lim f) ε
[PROOFSTEP]
dsimp [Metric.ball]
[GOAL]
case intro.intro.intro.a
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
ε : ℝ
hε : ε > 0
hεs : Metric.ball (lim f) ε ⊆ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(const norm (lim f) - f) j‖ < ε
b : ℕ
hb : b ≥ N
⊢ dist (↑f b) (lim f) < ε
[PROOFSTEP]
rw [dist_comm, dist_eq_norm]
[GOAL]
case intro.intro.intro.a
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
ε : ℝ
hε : ε > 0
hεs : Metric.ball (lim f) ε ⊆ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(const norm (lim f) - f) j‖ < ε
b : ℕ
hb : b ≥ N
⊢ ‖lim f - ↑f b‖ < ε
[PROOFSTEP]
solve_by_elim
[GOAL]
β : Type v
inst✝ : NormedField β
f : ℕ → β
hf : CauchySeq f
⊢ IsCauSeq norm f
[PROOFSTEP]
cases' cauchy_iff.1 hf with hf1 hf2
[GOAL]
case intro
β : Type v
inst✝ : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : NeBot (map f atTop)
hf2 : ∀ (s : Set (β × β)), s ∈ uniformity β → ∃ t, t ∈ map f atTop ∧ t ×ˢ t ⊆ s
⊢ IsCauSeq norm f
[PROOFSTEP]
intro ε hε
[GOAL]
case intro
β : Type v
inst✝ : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : NeBot (map f atTop)
hf2 : ∀ (s : Set (β × β)), s ∈ uniformity β → ∃ t, t ∈ map f atTop ∧ t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → ‖f j - f i‖ < ε
[PROOFSTEP]
rcases hf2 {x | dist x.1 x.2 < ε} (dist_mem_uniformity hε) with ⟨t, ⟨ht, htsub⟩⟩
[GOAL]
case intro.intro.intro
β : Type v
inst✝ : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : NeBot (map f atTop)
hf2 : ∀ (s : Set (β × β)), s ∈ uniformity β → ∃ t, t ∈ map f atTop ∧ t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
t : Set β
ht : t ∈ map f atTop
htsub : t ×ˢ t ⊆ {x | dist x.fst x.snd < ε}
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → ‖f j - f i‖ < ε
[PROOFSTEP]
simp at ht
[GOAL]
case intro.intro.intro
β : Type v
inst✝ : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : NeBot (map f atTop)
hf2 : ∀ (s : Set (β × β)), s ∈ uniformity β → ∃ t, t ∈ map f atTop ∧ t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
t : Set β
htsub : t ×ˢ t ⊆ {x | dist x.fst x.snd < ε}
ht : ∃ a, ∀ (b : ℕ), a ≤ b → f b ∈ t
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → ‖f j - f i‖ < ε
[PROOFSTEP]
cases' ht with N hN
[GOAL]
case intro.intro.intro.intro
β : Type v
inst✝ : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : NeBot (map f atTop)
hf2 : ∀ (s : Set (β × β)), s ∈ uniformity β → ∃ t, t ∈ map f atTop ∧ t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
t : Set β
htsub : t ×ˢ t ⊆ {x | dist x.fst x.snd < ε}
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f b ∈ t
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → ‖f j - f i‖ < ε
[PROOFSTEP]
exists N
[GOAL]
case intro.intro.intro.intro
β : Type v
inst✝ : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : NeBot (map f atTop)
hf2 : ∀ (s : Set (β × β)), s ∈ uniformity β → ∃ t, t ∈ map f atTop ∧ t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
t : Set β
htsub : t ×ˢ t ⊆ {x | dist x.fst x.snd < ε}
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f b ∈ t
⊢ ∀ (j : ℕ), j ≥ N → ‖f j - f N‖ < ε
[PROOFSTEP]
intro j hj
[GOAL]
case intro.intro.intro.intro
β : Type v
inst✝ : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : NeBot (map f atTop)
hf2 : ∀ (s : Set (β × β)), s ∈ uniformity β → ∃ t, t ∈ map f atTop ∧ t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
t : Set β
htsub : t ×ˢ t ⊆ {x | dist x.fst x.snd < ε}
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f b ∈ t
j : ℕ
hj : j ≥ N
⊢ ‖f j - f N‖ < ε
[PROOFSTEP]
rw [← dist_eq_norm]
[GOAL]
case intro.intro.intro.intro
β : Type v
inst✝ : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : NeBot (map f atTop)
hf2 : ∀ (s : Set (β × β)), s ∈ uniformity β → ∃ t, t ∈ map f atTop ∧ t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
t : Set β
htsub : t ×ˢ t ⊆ {x | dist x.fst x.snd < ε}
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f b ∈ t
j : ℕ
hj : j ≥ N
⊢ dist (f j) (f N) < ε
[PROOFSTEP]
apply @htsub (f j, f N)
[GOAL]
case intro.intro.intro.intro
β : Type v
inst✝ : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : NeBot (map f atTop)
hf2 : ∀ (s : Set (β × β)), s ∈ uniformity β → ∃ t, t ∈ map f atTop ∧ t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
t : Set β
htsub : t ×ˢ t ⊆ {x | dist x.fst x.snd < ε}
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f b ∈ t
j : ℕ
hj : j ≥ N
⊢ (f j, f N) ∈ t ×ˢ t
[PROOFSTEP]
apply Set.mk_mem_prod
[GOAL]
case intro.intro.intro.intro.ha
β : Type v
inst✝ : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : NeBot (map f atTop)
hf2 : ∀ (s : Set (β × β)), s ∈ uniformity β → ∃ t, t ∈ map f atTop ∧ t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
t : Set β
htsub : t ×ˢ t ⊆ {x | dist x.fst x.snd < ε}
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f b ∈ t
j : ℕ
hj : j ≥ N
⊢ f j ∈ t
[PROOFSTEP]
solve_by_elim [le_refl]
[GOAL]
case intro.intro.intro.intro.hb
β : Type v
inst✝ : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : NeBot (map f atTop)
hf2 : ∀ (s : Set (β × β)), s ∈ uniformity β → ∃ t, t ∈ map f atTop ∧ t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
t : Set β
htsub : t ×ˢ t ⊆ {x | dist x.fst x.snd < ε}
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f b ∈ t
j : ℕ
hj : j ≥ N
⊢ f N ∈ t
[PROOFSTEP]
solve_by_elim [le_refl]
[GOAL]
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
⊢ CauchySeq ↑f
[PROOFSTEP]
refine' cauchy_iff.2 ⟨by infer_instance, fun s hs => _⟩
[GOAL]
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
⊢ NeBot (map (↑f) atTop)
[PROOFSTEP]
infer_instance
[GOAL]
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
⊢ ∃ t, t ∈ map (↑f) atTop ∧ t ×ˢ t ⊆ s
[PROOFSTEP]
rcases mem_uniformity_dist.1 hs with ⟨ε, ⟨hε, hεs⟩⟩
[GOAL]
case intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
⊢ ∃ t, t ∈ map (↑f) atTop ∧ t ×ˢ t ⊆ s
[PROOFSTEP]
cases' CauSeq.cauchy₂ f hε with N hN
[GOAL]
case intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
⊢ ∃ t, t ∈ map (↑f) atTop ∧ t ×ˢ t ⊆ s
[PROOFSTEP]
exists {n | n ≥ N}.image f
[GOAL]
case intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
⊢ ↑f '' {n | n ≥ N} ∈ map (↑f) atTop ∧ (↑f '' {n | n ≥ N}) ×ˢ (↑f '' {n | n ≥ N}) ⊆ s
[PROOFSTEP]
simp only [exists_prop, mem_atTop_sets, mem_map, mem_image, ge_iff_le, mem_setOf_eq]
[GOAL]
case intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
⊢ (∃ a, ∀ (b : ℕ), a ≤ b → b ∈ ↑f ⁻¹' (↑f '' {n | N ≤ n})) ∧ (↑f '' {n | N ≤ n}) ×ˢ (↑f '' {n | N ≤ n}) ⊆ s
[PROOFSTEP]
constructor
[GOAL]
case intro.intro.intro.left
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → b ∈ ↑f ⁻¹' (↑f '' {n | N ≤ n})
[PROOFSTEP]
exists N
[GOAL]
case intro.intro.intro.left
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
⊢ ∀ (b : ℕ), N ≤ b → b ∈ ↑f ⁻¹' (↑f '' {n | N ≤ n})
[PROOFSTEP]
intro b hb
[GOAL]
case intro.intro.intro.left
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
b : ℕ
hb : N ≤ b
⊢ b ∈ ↑f ⁻¹' (↑f '' {n | N ≤ n})
[PROOFSTEP]
exists b
[GOAL]
case intro.intro.intro.right
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
⊢ (↑f '' {n | N ≤ n}) ×ˢ (↑f '' {n | N ≤ n}) ⊆ s
[PROOFSTEP]
rintro ⟨a, b⟩ ⟨⟨a', ⟨ha'1, ha'2⟩⟩, ⟨b', ⟨hb'1, hb'2⟩⟩⟩
[GOAL]
case intro.intro.intro.right.mk.intro.intro.intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
a b : β
a' : ℕ
ha'1 : a' ∈ {n | N ≤ n}
ha'2 : ↑f a' = (a, b).fst
b' : ℕ
hb'1 : b' ∈ {n | N ≤ n}
hb'2 : ↑f b' = (a, b).snd
⊢ (a, b) ∈ s
[PROOFSTEP]
dsimp at ha'1 ha'2 hb'1 hb'2
[GOAL]
case intro.intro.intro.right.mk.intro.intro.intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
a b : β
a' : ℕ
ha'1 : N ≤ a'
ha'2 : ↑f a' = a
b' : ℕ
hb'1 : N ≤ b'
hb'2 : ↑f b' = b
⊢ (a, b) ∈ s
[PROOFSTEP]
rw [← ha'2, ← hb'2]
[GOAL]
case intro.intro.intro.right.mk.intro.intro.intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
a b : β
a' : ℕ
ha'1 : N ≤ a'
ha'2 : ↑f a' = a
b' : ℕ
hb'1 : N ≤ b'
hb'2 : ↑f b' = b
⊢ (↑f a', ↑f b') ∈ s
[PROOFSTEP]
apply hεs
[GOAL]
case intro.intro.intro.right.mk.intro.intro.intro.intro.intro.a
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
a b : β
a' : ℕ
ha'1 : N ≤ a'
ha'2 : ↑f a' = a
b' : ℕ
hb'1 : N ≤ b'
hb'2 : ↑f b' = b
⊢ dist (↑f a') (↑f b') < ε
[PROOFSTEP]
rw [dist_eq_norm]
[GOAL]
case intro.intro.intro.right.mk.intro.intro.intro.intro.intro.a
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
a b : β
a' : ℕ
ha'1 : N ≤ a'
ha'2 : ↑f a' = a
b' : ℕ
hb'1 : N ≤ b'
hb'2 : ↑f b' = b
⊢ ‖↑f a' - ↑f b'‖ < ε
[PROOFSTEP]
apply hN
[GOAL]
case intro.intro.intro.right.mk.intro.intro.intro.intro.intro.a.x
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
a b : β
a' : ℕ
ha'1 : N ≤ a'
ha'2 : ↑f a' = a
b' : ℕ
hb'1 : N ≤ b'
hb'2 : ↑f b' = b
⊢ a' ≥ N
[PROOFSTEP]
assumption
[GOAL]
case intro.intro.intro.right.mk.intro.intro.intro.intro.intro.a.x
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
a b : β
a' : ℕ
ha'1 : N ≤ a'
ha'2 : ↑f a' = a
b' : ℕ
hb'1 : N ≤ b'
hb'2 : ↑f b' = b
⊢ b' ≥ N
[PROOFSTEP]
assumption
[GOAL]
β : Type v
inst✝¹ : NormedField β
inst✝ : CauSeq.IsComplete β norm
⊢ CompleteSpace β
[PROOFSTEP]
apply complete_of_cauchySeq_tendsto
[GOAL]
case a
β : Type v
inst✝¹ : NormedField β
inst✝ : CauSeq.IsComplete β norm
⊢ ∀ (u : ℕ → β), CauchySeq u → ∃ a, Tendsto u atTop (𝓝 a)
[PROOFSTEP]
intro u hu
[GOAL]
case a
β : Type v
inst✝¹ : NormedField β
inst✝ : CauSeq.IsComplete β norm
u : ℕ → β
hu : CauchySeq u
⊢ ∃ a, Tendsto u atTop (𝓝 a)
[PROOFSTEP]
have C : IsCauSeq norm u := isCauSeq_iff_cauchySeq.2 hu
[GOAL]
case a
β : Type v
inst✝¹ : NormedField β
inst✝ : CauSeq.IsComplete β norm
u : ℕ → β
hu : CauchySeq u
C : IsCauSeq norm u
⊢ ∃ a, Tendsto u atTop (𝓝 a)
[PROOFSTEP]
exists CauSeq.lim ⟨u, C⟩
[GOAL]
case a
β : Type v
inst✝¹ : NormedField β
inst✝ : CauSeq.IsComplete β norm
u : ℕ → β
hu : CauchySeq u
C : IsCauSeq norm u
⊢ Tendsto u atTop (𝓝 (CauSeq.lim { val := u, property := C }))
[PROOFSTEP]
rw [Metric.tendsto_atTop]
[GOAL]
case a
β : Type v
inst✝¹ : NormedField β
inst✝ : CauSeq.IsComplete β norm
u : ℕ → β
hu : CauchySeq u
C : IsCauSeq norm u
⊢ ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → dist (u n) (CauSeq.lim { val := u, property := C }) < ε
[PROOFSTEP]
intro ε εpos
[GOAL]
case a
β : Type v
inst✝¹ : NormedField β
inst✝ : CauSeq.IsComplete β norm
u : ℕ → β
hu : CauchySeq u
C : IsCauSeq norm u
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → dist (u n) (CauSeq.lim { val := u, property := C }) < ε
[PROOFSTEP]
cases' (CauSeq.equiv_lim ⟨u, C⟩) _ εpos with N hN
[GOAL]
case a.intro
β : Type v
inst✝¹ : NormedField β
inst✝ : CauSeq.IsComplete β norm
u : ℕ → β
hu : CauchySeq u
C : IsCauSeq norm u
ε : ℝ
εpos : ε > 0
N : ℕ
hN :
  ∀ (j : ℕ), j ≥ N → ‖↑({ val := u, property := C } - CauSeq.const norm (CauSeq.lim { val := u, property := C })) j‖ < ε
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → dist (u n) (CauSeq.lim { val := u, property := C }) < ε
[PROOFSTEP]
exists N
[GOAL]
case a.intro
β : Type v
inst✝¹ : NormedField β
inst✝ : CauSeq.IsComplete β norm
u : ℕ → β
hu : CauchySeq u
C : IsCauSeq norm u
ε : ℝ
εpos : ε > 0
N : ℕ
hN :
  ∀ (j : ℕ), j ≥ N → ‖↑({ val := u, property := C } - CauSeq.const norm (CauSeq.lim { val := u, property := C })) j‖ < ε
⊢ ∀ (n : ℕ), n ≥ N → dist (u n) (CauSeq.lim { val := u, property := C }) < ε
[PROOFSTEP]
simpa [dist_eq_norm] using hN


[GOAL]
α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
x : α
r✝ : ℝ
s : Set α
r : ι → ℝ
hs : IsClosed s
uf : ∀ (x : α), x ∈ s → Set.Finite {i | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
⊢ ∃ r', s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i < r i
[PROOFSTEP]
rcases exists_subset_iUnion_closed_subset hs (fun i => @isOpen_ball _ _ (c i) (r i)) uf us with ⟨v, hsv, hvc, hcv⟩
[GOAL]
case intro.intro.intro
α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
x : α
r✝ : ℝ
s : Set α
r : ι → ℝ
hs : IsClosed s
uf : ∀ (x : α), x ∈ s → Set.Finite {i | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
v : ι → Set α
hsv : s ⊆ iUnion v
hvc : ∀ (i : ι), IsClosed (v i)
hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)
⊢ ∃ r', s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i < r i
[PROOFSTEP]
have := fun i => exists_lt_subset_ball (hvc i) (hcv i)
[GOAL]
case intro.intro.intro
α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
x : α
r✝ : ℝ
s : Set α
r : ι → ℝ
hs : IsClosed s
uf : ∀ (x : α), x ∈ s → Set.Finite {i | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
v : ι → Set α
hsv : s ⊆ iUnion v
hvc : ∀ (i : ι), IsClosed (v i)
hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)
this : ∀ (i : ι), ∃ r', r' < r i ∧ v i ⊆ ball (c i) r'
⊢ ∃ r', s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i < r i
[PROOFSTEP]
choose r' hlt hsub using this
[GOAL]
case intro.intro.intro
α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
x : α
r✝ : ℝ
s : Set α
r : ι → ℝ
hs : IsClosed s
uf : ∀ (x : α), x ∈ s → Set.Finite {i | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
v : ι → Set α
hsv : s ⊆ iUnion v
hvc : ∀ (i : ι), IsClosed (v i)
hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)
r' : ι → ℝ
hlt : ∀ (i : ι), r' i < r i
hsub : ∀ (i : ι), v i ⊆ ball (c i) (r' i)
⊢ ∃ r', s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i < r i
[PROOFSTEP]
exact ⟨r', hsv.trans <| iUnion_mono <| hsub, hlt⟩
[GOAL]
α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
x : α
r✝ : ℝ
s : Set α
r : ι → ℝ
hr : ∀ (i : ι), 0 < r i
hs : IsClosed s
uf : ∀ (x : α), x ∈ s → Set.Finite {i | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
⊢ ∃ r', s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)
[PROOFSTEP]
rcases exists_subset_iUnion_closed_subset hs (fun i => @isOpen_ball _ _ (c i) (r i)) uf us with ⟨v, hsv, hvc, hcv⟩
[GOAL]
case intro.intro.intro
α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
x : α
r✝ : ℝ
s : Set α
r : ι → ℝ
hr : ∀ (i : ι), 0 < r i
hs : IsClosed s
uf : ∀ (x : α), x ∈ s → Set.Finite {i | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
v : ι → Set α
hsv : s ⊆ iUnion v
hvc : ∀ (i : ι), IsClosed (v i)
hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)
⊢ ∃ r', s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)
[PROOFSTEP]
have := fun i => exists_pos_lt_subset_ball (hr i) (hvc i) (hcv i)
[GOAL]
case intro.intro.intro
α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
x : α
r✝ : ℝ
s : Set α
r : ι → ℝ
hr : ∀ (i : ι), 0 < r i
hs : IsClosed s
uf : ∀ (x : α), x ∈ s → Set.Finite {i | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
v : ι → Set α
hsv : s ⊆ iUnion v
hvc : ∀ (i : ι), IsClosed (v i)
hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)
this : ∀ (i : ι), ∃ r', r' ∈ Ioo 0 (r i) ∧ v i ⊆ ball (c i) r'
⊢ ∃ r', s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)
[PROOFSTEP]
choose r' hlt hsub using this
[GOAL]
case intro.intro.intro
α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
x : α
r✝ : ℝ
s : Set α
r : ι → ℝ
hr : ∀ (i : ι), 0 < r i
hs : IsClosed s
uf : ∀ (x : α), x ∈ s → Set.Finite {i | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
v : ι → Set α
hsv : s ⊆ iUnion v
hvc : ∀ (i : ι), IsClosed (v i)
hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)
r' : ι → ℝ
hlt : ∀ (i : ι), r' i ∈ Ioo 0 (r i)
hsub : ∀ (i : ι), v i ⊆ ball (c i) (r' i)
⊢ ∃ r', s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)
[PROOFSTEP]
exact ⟨r', hsv.trans <| iUnion_mono hsub, hlt⟩
[GOAL]
α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
x : α
r : ℝ
s : Set α
hs : IsClosed s
R : α → ℝ
hR : ∀ (x : α), x ∈ s → 0 < R x
⊢ ∃ ι c r r',
    (∀ (i : ι), c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧
      (LocallyFinite fun i => ball (c i) (r' i)) ∧ s ⊆ ⋃ (i : ι), ball (c i) (r i)
[PROOFSTEP]
have : ∀ x ∈ s, (𝓝 x).HasBasis (fun r : ℝ => 0 < r ∧ r < R x) fun r => ball x r := fun x hx =>
  nhds_basis_uniformity (uniformity_basis_dist_lt (hR x hx))
[GOAL]
α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
x : α
r : ℝ
s : Set α
hs : IsClosed s
R : α → ℝ
hR : ∀ (x : α), x ∈ s → 0 < R x
this : ∀ (x : α), x ∈ s → Filter.HasBasis (𝓝 x) (fun r => 0 < r ∧ r < R x) fun r => ball x r
⊢ ∃ ι c r r',
    (∀ (i : ι), c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧
      (LocallyFinite fun i => ball (c i) (r' i)) ∧ s ⊆ ⋃ (i : ι), ball (c i) (r i)
[PROOFSTEP]
rcases refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set hs this with ⟨ι, c, r', hr', hsub', hfin⟩
[GOAL]
case intro.intro.intro.intro.intro
α : Type u
ι✝ : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c✝ : ι✝ → α
x : α
r : ℝ
s : Set α
hs : IsClosed s
R : α → ℝ
hR : ∀ (x : α), x ∈ s → 0 < R x
this : ∀ (x : α), x ∈ s → Filter.HasBasis (𝓝 x) (fun r => 0 < r ∧ r < R x) fun r => ball x r
ι : Type u
c : ι → α
r' : ι → ℝ
hr' : ∀ (a : ι), c a ∈ s ∧ 0 < r' a ∧ r' a < R (c a)
hsub' : s ⊆ ⋃ (a : ι), ball (c a) (r' a)
hfin : LocallyFinite fun a => ball (c a) (r' a)
⊢ ∃ ι c r r',
    (∀ (i : ι), c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧
      (LocallyFinite fun i => ball (c i) (r' i)) ∧ s ⊆ ⋃ (i : ι), ball (c i) (r i)
[PROOFSTEP]
rcases exists_subset_iUnion_ball_radius_pos_lt (fun i => (hr' i).2.1) hs (fun x _ => hfin.point_finite x) hsub' with
  ⟨r, hsub, hlt⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
α : Type u
ι✝ : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c✝ : ι✝ → α
x : α
r✝ : ℝ
s : Set α
hs : IsClosed s
R : α → ℝ
hR : ∀ (x : α), x ∈ s → 0 < R x
this : ∀ (x : α), x ∈ s → Filter.HasBasis (𝓝 x) (fun r => 0 < r ∧ r < R x) fun r => ball x r
ι : Type u
c : ι → α
r' : ι → ℝ
hr' : ∀ (a : ι), c a ∈ s ∧ 0 < r' a ∧ r' a < R (c a)
hsub' : s ⊆ ⋃ (a : ι), ball (c a) (r' a)
hfin : LocallyFinite fun a => ball (c a) (r' a)
r : ι → ℝ
hsub : s ⊆ ⋃ (i : ι), ball (c i) (r i)
hlt : ∀ (i : ι), r i ∈ Ioo 0 (r' i)
⊢ ∃ ι c r r',
    (∀ (i : ι), c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧
      (LocallyFinite fun i => ball (c i) (r' i)) ∧ s ⊆ ⋃ (i : ι), ball (c i) (r i)
[PROOFSTEP]
exact ⟨ι, c, r, r', fun i => ⟨(hr' i).1, (hlt i).1, (hlt i).2, (hr' i).2.2⟩, hfin, hsub⟩


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g : α →ᵈ β
h : f.toFun = g.toFun
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
g : α →ᵈ β
toFun✝ : α → β
edist_eq'✝ : ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (toFun✝ x) (toFun✝ y) = ↑r * edist x y
h : { toFun := toFun✝, edist_eq' := edist_eq'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, edist_eq' := edist_eq'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
toFun✝¹ : α → β
edist_eq'✝¹ : ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (toFun✝¹ x) (toFun✝¹ y) = ↑r * edist x y
toFun✝ : α → β
edist_eq'✝ : ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (toFun✝ x) (toFun✝ y) = ↑r * edist x y
h : { toFun := toFun✝¹, edist_eq' := edist_eq'✝¹ }.toFun = { toFun := toFun✝, edist_eq' := edist_eq'✝ }.toFun
⊢ { toFun := toFun✝¹, edist_eq' := edist_eq'✝¹ } = { toFun := toFun✝, edist_eq' := edist_eq'✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : Subsingleton α
inst✝ : DilationClass F α β
f : F
x y : α
⊢ edist x y = 0 ∨ edist x y = ⊤
[PROOFSTEP]
simp [Subsingleton.elim x y]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : DilationClass F α β
f : F
⊢ ratio f ≠ 0
[PROOFSTEP]
rw [ratio]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : DilationClass F α β
f : F
⊢ (if ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤ then 1
    else Exists.choose (_ : ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (↑f x) (↑f y) = ↑r * edist x y)) ≠
    0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : DilationClass F α β
f : F
h✝ : ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
⊢ 1 ≠ 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : DilationClass F α β
f : F
h✝ : ¬∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
⊢ Exists.choose (_ : ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (↑f x) (↑f y) = ↑r * edist x y) ≠ 0
[PROOFSTEP]
exact (DilationClass.edist_eq' f).choose_spec.1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : DilationClass F α β
f : F
x y : α
⊢ edist (↑f x) (↑f y) = ↑(ratio f) * edist x y
[PROOFSTEP]
rw [ratio]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : DilationClass F α β
f : F
x y : α
⊢ edist (↑f x) (↑f y) =
    ↑(if ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤ then 1
        else Exists.choose (_ : ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (↑f x) (↑f y) = ↑r * edist x y)) *
      edist x y
[PROOFSTEP]
split_ifs with key
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : DilationClass F α β
f : F
x y : α
key : ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
⊢ edist (↑f x) (↑f y) = ↑1 * edist x y
[PROOFSTEP]
rcases DilationClass.edist_eq' f with ⟨r, hne, hr⟩
[GOAL]
case pos.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : DilationClass F α β
f : F
x y : α
key : ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
r : ℝ≥0
hne : r ≠ 0
hr : ∀ (x y : α), edist (↑f x) (↑f y) = ↑r * edist x y
⊢ edist (↑f x) (↑f y) = ↑1 * edist x y
[PROOFSTEP]
replace hr := hr x y
[GOAL]
case pos.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : DilationClass F α β
f : F
x y : α
key : ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
r : ℝ≥0
hne : r ≠ 0
hr : edist (↑f x) (↑f y) = ↑r * edist x y
⊢ edist (↑f x) (↑f y) = ↑1 * edist x y
[PROOFSTEP]
cases' key x y with h h
[GOAL]
case pos.intro.intro.inl
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : DilationClass F α β
f : F
x y : α
key : ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
r : ℝ≥0
hne : r ≠ 0
hr : edist (↑f x) (↑f y) = ↑r * edist x y
h : edist x y = 0
⊢ edist (↑f x) (↑f y) = ↑1 * edist x y
[PROOFSTEP]
simp only [hr, h, mul_zero]
[GOAL]
case pos.intro.intro.inr
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : DilationClass F α β
f : F
x y : α
key : ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
r : ℝ≥0
hne : r ≠ 0
hr : edist (↑f x) (↑f y) = ↑r * edist x y
h : edist x y = ⊤
⊢ edist (↑f x) (↑f y) = ↑1 * edist x y
[PROOFSTEP]
simp [hr, h, hne]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : DilationClass F α β
f : F
x y : α
key : ¬∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
⊢ edist (↑f x) (↑f y) =
    ↑(Exists.choose (_ : ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (↑f x) (↑f y) = ↑r * edist x y)) * edist x y
[PROOFSTEP]
exact (DilationClass.edist_eq' f).choose_spec.2 x y
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F✝ : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α✝
inst✝³ : PseudoEMetricSpace β✝
α : Type u_6
β : Type u_7
F : Type u_8
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : DilationClass F α β
f : F
x y : α
⊢ nndist (↑f x) (↑f y) = ratio f * nndist x y
[PROOFSTEP]
simp only [← ENNReal.coe_eq_coe, ← edist_nndist, ENNReal.coe_mul, edist_eq]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F✝ : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α✝
inst✝³ : PseudoEMetricSpace β✝
α : Type u_6
β : Type u_7
F : Type u_8
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : DilationClass F α β
f : F
x y : α
⊢ dist (↑f x) (↑f y) = ↑(ratio f) * dist x y
[PROOFSTEP]
simp only [dist_nndist, nndist_eq, NNReal.coe_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : DilationClass F α β
f : F
x y : α
r : ℝ≥0
h₀ : edist x y ≠ 0
htop : edist x y ≠ ⊤
hr : edist (↑f x) (↑f y) = ↑r * edist x y
⊢ r = ratio f
[PROOFSTEP]
simpa only [hr, ENNReal.mul_eq_mul_right h₀ htop, ENNReal.coe_eq_coe] using edist_eq f x y
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F✝ : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α✝
inst✝³ : PseudoEMetricSpace β✝
α : Type u_6
β : Type u_7
F : Type u_8
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : DilationClass F α β
f : F
x y : α
r : ℝ≥0
hxy : nndist x y ≠ 0
hr : nndist (↑f x) (↑f y) = r * nndist x y
⊢ edist x y ≠ 0
[PROOFSTEP]
rwa [edist_nndist, ENNReal.coe_ne_zero]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F✝ : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α✝
inst✝³ : PseudoEMetricSpace β✝
α : Type u_6
β : Type u_7
F : Type u_8
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : DilationClass F α β
f : F
x y : α
r : ℝ≥0
hxy : nndist x y ≠ 0
hr : nndist (↑f x) (↑f y) = r * nndist x y
⊢ edist (↑f x) (↑f y) = ↑r * edist x y
[PROOFSTEP]
rw [edist_nndist, edist_nndist, hr, ENNReal.coe_mul]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F✝ : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α✝
inst✝³ : PseudoEMetricSpace β✝
α : Type u_7
β : Type u_8
F : Type u_6
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : DilationClass F α β
f : F
x y : α
r : ℝ≥0
hxy : dist x y ≠ 0
hr : dist (↑f x) (↑f y) = ↑r * dist x y
⊢ ↑(nndist (↑f x) (↑f y)) = ↑(r * nndist x y)
[PROOFSTEP]
rw [coe_nndist, hr, NNReal.coe_mul, coe_nndist]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝³ : PseudoEMetricSpace α✝
inst✝² : PseudoEMetricSpace β✝
α : Type ?u.24367
β : Type ?u.24370
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
h : ∃ r, r ≠ 0 ∧ ∀ (x y : α), nndist (f x) (f y) = r * nndist x y
⊢ ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (f x) (f y) = ↑r * edist x y
[PROOFSTEP]
rcases h with ⟨r, hne, h⟩
[GOAL]
case intro.intro
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝³ : PseudoEMetricSpace α✝
inst✝² : PseudoEMetricSpace β✝
α : Type ?u.24367
β : Type ?u.24370
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
r : ℝ≥0
hne : r ≠ 0
h : ∀ (x y : α), nndist (f x) (f y) = r * nndist x y
⊢ ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (f x) (f y) = ↑r * edist x y
[PROOFSTEP]
refine' ⟨r, hne, fun x y => _⟩
[GOAL]
case intro.intro
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝³ : PseudoEMetricSpace α✝
inst✝² : PseudoEMetricSpace β✝
α : Type ?u.24367
β : Type ?u.24370
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
r : ℝ≥0
hne : r ≠ 0
h : ∀ (x y : α), nndist (f x) (f y) = r * nndist x y
x y : α
⊢ edist (f x) (f y) = ↑r * edist x y
[PROOFSTEP]
rw [edist_nndist, edist_nndist, ← ENNReal.coe_mul, h x y]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝³ : PseudoEMetricSpace α✝
inst✝² : PseudoEMetricSpace β✝
α : Type ?u.25376
β : Type ?u.25379
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
h : ∃ r, r ≠ 0 ∧ ∀ (x y : α), dist (f x) (f y) = ↑r * dist x y
r : ℝ≥0
hr : r ≠ 0 ∧ ∀ (x y : α), dist (f x) (f y) = ↑r * dist x y
x y : α
⊢ ↑(nndist (f x) (f y)) = ↑(r * nndist x y)
[PROOFSTEP]
rw [coe_nndist, hr.2, NNReal.coe_mul, coe_nndist]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f : F
g : G
x✝ y✝ z : α
s : Set α
x y : α
⊢ edist x y ≤ ↑(ratio f)⁻¹ * edist (↑f x) (↑f y)
[PROOFSTEP]
have hr : ratio f ≠ 0 := ratio_ne_zero f
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f : F
g : G
x✝ y✝ z : α
s : Set α
x y : α
hr : ratio f ≠ 0
⊢ edist x y ≤ ↑(ratio f)⁻¹ * edist (↑f x) (↑f y)
[PROOFSTEP]
exact_mod_cast (ENNReal.mul_le_iff_le_inv (ENNReal.coe_ne_zero.2 hr) ENNReal.coe_ne_top).1 (edist_eq f x y).ge
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : PseudoEMetricSpace α✝
inst✝⁴ : PseudoEMetricSpace β
inst✝³ : PseudoEMetricSpace γ
inst✝² : DilationClass F α✝ β
inst✝¹ : DilationClass G β γ
f : F
g : G
x✝ y✝ z : α✝
s : Set α✝
α : Type ?u.28806
inst✝ : PseudoEMetricSpace α
x y : α
⊢ edist (id x) (id y) = ↑1 * edist x y
[PROOFSTEP]
simp only [id.def, ENNReal.coe_one, one_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f : F
g : G
x y z : α
s : Set α
⊢ ratio (Dilation.id α) = 1
[PROOFSTEP]
by_cases h : ∀ x y : α, edist x y = 0 ∨ edist x y = ∞
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f : F
g : G
x y z : α
s : Set α
h : ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
⊢ ratio (Dilation.id α) = 1
[PROOFSTEP]
rw [ratio, if_pos h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f : F
g : G
x y z : α
s : Set α
h : ¬∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
⊢ ratio (Dilation.id α) = 1
[PROOFSTEP]
push_neg at h
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f : F
g : G
x y z : α
s : Set α
h : ∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ⊤
⊢ ratio (Dilation.id α) = 1
[PROOFSTEP]
rcases h with ⟨x, y, hne⟩
[GOAL]
case neg.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f : F
g : G
x✝ y✝ z : α
s : Set α
x y : α
hne : edist x y ≠ 0 ∧ edist x y ≠ ⊤
⊢ ratio (Dilation.id α) = 1
[PROOFSTEP]
refine' (ratio_unique hne.1 hne.2 _).symm
[GOAL]
case neg.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f : F
g : G
x✝ y✝ z : α
s : Set α
x y : α
hne : edist x y ≠ 0 ∧ edist x y ≠ ⊤
⊢ edist (↑(Dilation.id α) x) (↑(Dilation.id α) y) = ↑1 * edist x y
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f✝ : F
g✝ : G
x✝ y✝ z : α
s : Set α
g : β →ᵈ γ
f : α →ᵈ β
x y : α
⊢ edist ((↑g ∘ ↑f) x) ((↑g ∘ ↑f) y) = ↑(ratio g * ratio f) * edist x y
[PROOFSTEP]
simp_rw [Function.comp, edist_eq, ENNReal.coe_mul, mul_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f✝ : F
g✝ : G
x y z : α
s : Set α
g : β →ᵈ γ
f : α →ᵈ β
hne : ∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ⊤
⊢ ratio (comp g f) = ratio g * ratio f
[PROOFSTEP]
rcases hne with ⟨x, y, hα⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f✝ : F
g✝ : G
x✝ y✝ z : α
s : Set α
g : β →ᵈ γ
f : α →ᵈ β
x y : α
hα : edist x y ≠ 0 ∧ edist x y ≠ ⊤
⊢ ratio (comp g f) = ratio g * ratio f
[PROOFSTEP]
have hgf := (edist_eq (g.comp f) x y).symm
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f✝ : F
g✝ : G
x✝ y✝ z : α
s : Set α
g : β →ᵈ γ
f : α →ᵈ β
x y : α
hα : edist x y ≠ 0 ∧ edist x y ≠ ⊤
hgf : ↑(ratio (comp g f)) * edist x y = edist (↑(comp g f) x) (↑(comp g f) y)
⊢ ratio (comp g f) = ratio g * ratio f
[PROOFSTEP]
simp_rw [coe_comp, Function.comp, edist_eq, ← mul_assoc, ENNReal.mul_eq_mul_right hα.1 hα.2] at hgf
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f✝ : F
g✝ : G
x✝ y✝ z : α
s : Set α
g : β →ᵈ γ
f : α →ᵈ β
x y : α
hα : edist x y ≠ 0 ∧ edist x y ≠ ⊤
hgf : ↑(ratio (comp g f)) = ↑(ratio g) * ↑(ratio f)
⊢ ratio (comp g f) = ratio g * ratio f
[PROOFSTEP]
rwa [← ENNReal.coe_eq_coe, ENNReal.coe_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f✝ : F
g✝ : G
x y z : α
s : Set α
f g : α →ᵈ α
⊢ ratio (f * g) = ratio f * ratio g
[PROOFSTEP]
by_cases h : ∀ x y : α, edist x y = 0 ∨ edist x y = ∞
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f✝ : F
g✝ : G
x y z : α
s : Set α
f g : α →ᵈ α
h : ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
⊢ ratio (f * g) = ratio f * ratio g
[PROOFSTEP]
simp [ratio_of_trivial, h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f✝ : F
g✝ : G
x y z : α
s : Set α
f g : α →ᵈ α
h : ¬∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
⊢ ratio (f * g) = ratio f * ratio g
[PROOFSTEP]
push_neg at h
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f✝ : F
g✝ : G
x y z : α
s : Set α
f g : α →ᵈ α
h : ∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ⊤
⊢ ratio (f * g) = ratio f * ratio g
[PROOFSTEP]
exact ratio_comp' h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f : F
g✝ : G
x✝ y z : α
s : Set α
g : β →ᵈ γ
f₁ f₂ : α →ᵈ β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
x : α
⊢ ↑g (↑f₁ x) = ↑g (↑f₂ x)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f : F
g : G
x y z : α
s✝ s : Set α
⊢ EMetric.diam (↑f '' s) = ↑(ratio f) * EMetric.diam s
[PROOFSTEP]
refine' ((lipschitz f).ediam_image_le s).antisymm _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f : F
g : G
x y z : α
s✝ s : Set α
⊢ ↑(ratio f) * EMetric.diam s ≤ EMetric.diam (↑f '' s)
[PROOFSTEP]
apply ENNReal.mul_le_of_le_div'
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f : F
g : G
x y z : α
s✝ s : Set α
⊢ EMetric.diam s ≤ EMetric.diam (↑f '' s) / ↑(ratio f)
[PROOFSTEP]
rw [div_eq_mul_inv, mul_comm, ← ENNReal.coe_inv]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f : F
g : G
x y z : α
s✝ s : Set α
⊢ EMetric.diam s ≤ ↑(ratio f)⁻¹ * EMetric.diam (↑f '' s)
case h
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f : F
g : G
x y z : α
s✝ s : Set α
⊢ ratio f ≠ 0
[PROOFSTEP]
exacts [(antilipschitz f).le_mul_ediam_image s, ratio_ne_zero f]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f : F
g : G
x y z : α
s : Set α
⊢ EMetric.diam (range ↑f) = ↑(ratio f) * EMetric.diam univ
[PROOFSTEP]
rw [← image_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f : F
g : G
x y z : α
s : Set α
⊢ EMetric.diam (↑f '' univ) = ↑(ratio f) * EMetric.diam univ
[PROOFSTEP]
exact ediam_image f univ
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f : F
g : G
x✝ y✝ z : α
s : Set α
x : α
r' : ℝ≥0∞
y : α
hy : y ∈ EMetric.closedBall x r'
⊢ edist y x ≤ r'
[PROOFSTEP]
exact hy
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : DilationClass F α β
f : F
s : Set α
⊢ Metric.diam (↑f '' s) = ↑(ratio f) * Metric.diam s
[PROOFSTEP]
simp [Metric.diam, ediam_image, ENNReal.toReal_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : DilationClass F α β
f : F
⊢ Metric.diam (range ↑f) = ↑(ratio f) * Metric.diam univ
[PROOFSTEP]
rw [← image_univ, diam_image]