[GOAL]
⊢ Subalgebra.topologicalClosure (polynomialFunctions I) = ⊤
[PROOFSTEP]
apply eq_top_iff.mpr
[GOAL]
⊢ ⊤ ≤ Subalgebra.topologicalClosure (polynomialFunctions I)
[PROOFSTEP]
rintro f -
[GOAL]
f : C(↑I, ℝ)
⊢ f ∈ Subalgebra.topologicalClosure (polynomialFunctions I)
[PROOFSTEP]
refine' Filter.Frequently.mem_closure _
[GOAL]
f : C(↑I, ℝ)
⊢ ∃ᶠ (x : C(↑I, ℝ)) in nhds f, x ∈ ↑(polynomialFunctions I)
[PROOFSTEP]
refine' Filter.Tendsto.frequently (bernsteinApproximation_uniform f) _
[GOAL]
f : C(↑I, ℝ)
⊢ ∃ᶠ (x : ℕ) in atTop, bernsteinApproximation x f ∈ ↑(polynomialFunctions I)
[PROOFSTEP]
apply frequently_of_forall
[GOAL]
case h
f : C(↑I, ℝ)
⊢ ∀ (x : ℕ), bernsteinApproximation x f ∈ ↑(polynomialFunctions I)
[PROOFSTEP]
intro n
[GOAL]
case h
f : C(↑I, ℝ)
n : ℕ
⊢ bernsteinApproximation n f ∈ ↑(polynomialFunctions I)
[PROOFSTEP]
simp only [SetLike.mem_coe]
[GOAL]
case h
f : C(↑I, ℝ)
n : ℕ
⊢ bernsteinApproximation n f ∈ polynomialFunctions I
[PROOFSTEP]
apply Subalgebra.sum_mem
[GOAL]
case h.h
f : C(↑I, ℝ)
n : ℕ
⊢ ∀ (x : Fin (n + 1)), x ∈ Finset.univ → ↑f (bernstein.z x) • bernstein n ↑x ∈ polynomialFunctions I
[PROOFSTEP]
rintro n -
[GOAL]
case h.h
f : C(↑I, ℝ)
n✝ : ℕ
n : Fin (n✝ + 1)
⊢ ↑f (bernstein.z n) • bernstein n✝ ↑n ∈ polynomialFunctions I
[PROOFSTEP]
apply Subalgebra.smul_mem
[GOAL]
case h.h.hx
f : C(↑I, ℝ)
n✝ : ℕ
n : Fin (n✝ + 1)
⊢ bernstein n✝ ↑n ∈ polynomialFunctions I
[PROOFSTEP]
dsimp [bernstein, polynomialFunctions]
[GOAL]
case h.h.hx
f : C(↑I, ℝ)
n✝ : ℕ
n : Fin (n✝ + 1)
⊢ Polynomial.toContinuousMapOn (bernsteinPolynomial ℝ n✝ ↑n) I ∈ Subalgebra.map (Polynomial.toContinuousMapOnAlgHom I) ⊤
[PROOFSTEP]
simp
[GOAL]
a b : ℝ
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
[PROOFSTEP]
cases' lt_or_le a b with h h
[GOAL]
case inl
a b : ℝ
h : a < b
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
[PROOFSTEP]
let W : C(Set.Icc a b, ℝ) →ₐ[ℝ] C(I, ℝ) := compRightAlgHom ℝ ℝ (iccHomeoI a b h).symm.toContinuousMap
[GOAL]
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) :=
  compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
[PROOFSTEP]
let W' : C(Set.Icc a b, ℝ) ≃ₜ C(I, ℝ) := compRightHomeomorph ℝ (iccHomeoI a b h).symm
[GOAL]
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) :=
  compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := compRightHomeomorph ℝ (Homeomorph.symm (iccHomeoI a b h))
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
[PROOFSTEP]
have w : (W : C(Set.Icc a b, ℝ) → C(I, ℝ)) = W' := rfl
[GOAL]
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) :=
  compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := compRightHomeomorph ℝ (Homeomorph.symm (iccHomeoI a b h))
w : ↑W = ↑W'
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
[PROOFSTEP]
have p := polynomialFunctions_closure_eq_top'
[GOAL]
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) :=
  compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := compRightHomeomorph ℝ (Homeomorph.symm (iccHomeoI a b h))
w : ↑W = ↑W'
p : Subalgebra.topologicalClosure (polynomialFunctions I) = ⊤
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
[PROOFSTEP]
apply_fun fun s => s.comap W at p
[GOAL]
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) :=
  compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := compRightHomeomorph ℝ (Homeomorph.symm (iccHomeoI a b h))
w : ↑W = ↑W'
p : Subalgebra.comap W (Subalgebra.topologicalClosure (polynomialFunctions I)) = Subalgebra.comap W ⊤
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
[PROOFSTEP]
simp only [Algebra.comap_top] at p
[GOAL]
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) :=
  compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := compRightHomeomorph ℝ (Homeomorph.symm (iccHomeoI a b h))
w : ↑W = ↑W'
p :
  Subalgebra.comap (compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h))))
      (Subalgebra.topologicalClosure (polynomialFunctions I)) =
    ⊤
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
[PROOFSTEP]
rw [Subalgebra.topologicalClosure_comap_homeomorph _ W W' w] at p
[GOAL]
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) :=
  compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := compRightHomeomorph ℝ (Homeomorph.symm (iccHomeoI a b h))
w : ↑W = ↑W'
p : Subalgebra.topologicalClosure (Subalgebra.comap W (polynomialFunctions I)) = ⊤
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
[PROOFSTEP]
rw [polynomialFunctions.comap_compRightAlgHom_iccHomeoI] at p
[GOAL]
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) :=
  compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := compRightHomeomorph ℝ (Homeomorph.symm (iccHomeoI a b h))
w : ↑W = ↑W'
p : Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
[PROOFSTEP]
exact p
[GOAL]
case inr
a b : ℝ
h : b ≤ a
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
[PROOFSTEP]
have : Subsingleton (Set.Icc a b) := (Set.subsingleton_coe _).mpr $ Set.subsingleton_Icc_of_ge h
[GOAL]
case inr
a b : ℝ
h : b ≤ a
this : Subsingleton ↑(Set.Icc a b)
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
⊢ f ∈ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b))
[PROOFSTEP]
rw [polynomialFunctions_closure_eq_top _ _]
[GOAL]
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
⊢ f ∈ ⊤
[PROOFSTEP]
simp
[GOAL]
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
ε : ℝ
pos : 0 < ε
⊢ ∃ p, ‖Polynomial.toContinuousMapOn p (Set.Icc a b) - f‖ < ε
[PROOFSTEP]
have w := mem_closure_iff_frequently.mp (continuousMap_mem_polynomialFunctions_closure _ _ f)
[GOAL]
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
ε : ℝ
pos : 0 < ε
w : ∃ᶠ (x : C(↑(Set.Icc a b), ℝ)) in nhds f, x ∈ ↑(polynomialFunctions (Set.Icc a b))
⊢ ∃ p, ‖Polynomial.toContinuousMapOn p (Set.Icc a b) - f‖ < ε
[PROOFSTEP]
rw [Metric.nhds_basis_ball.frequently_iff] at w
[GOAL]
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
ε : ℝ
pos : 0 < ε
w : ∀ (i : ℝ), 0 < i → ∃ x, x ∈ Metric.ball f i ∧ x ∈ ↑(polynomialFunctions (Set.Icc a b))
⊢ ∃ p, ‖Polynomial.toContinuousMapOn p (Set.Icc a b) - f‖ < ε
[PROOFSTEP]
obtain ⟨-, H, ⟨m, ⟨-, rfl⟩⟩⟩ := w ε pos
[GOAL]
case intro.intro.intro.intro
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
ε : ℝ
pos : 0 < ε
w : ∀ (i : ℝ), 0 < i → ∃ x, x ∈ Metric.ball f i ∧ x ∈ ↑(polynomialFunctions (Set.Icc a b))
m : ℝ[X]
H : ↑↑(Polynomial.toContinuousMapOnAlgHom (Set.Icc a b)) m ∈ Metric.ball f ε
⊢ ∃ p, ‖Polynomial.toContinuousMapOn p (Set.Icc a b) - f‖ < ε
[PROOFSTEP]
rw [Metric.mem_ball, dist_eq_norm] at H
[GOAL]
case intro.intro.intro.intro
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
ε : ℝ
pos : 0 < ε
w : ∀ (i : ℝ), 0 < i → ∃ x, x ∈ Metric.ball f i ∧ x ∈ ↑(polynomialFunctions (Set.Icc a b))
m : ℝ[X]
H : ‖↑↑(Polynomial.toContinuousMapOnAlgHom (Set.Icc a b)) m - f‖ < ε
⊢ ∃ p, ‖Polynomial.toContinuousMapOn p (Set.Icc a b) - f‖ < ε
[PROOFSTEP]
exact ⟨m, H⟩
[GOAL]
a b : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b)
ε : ℝ
pos : 0 < ε
⊢ ∃ p, ∀ (x : ℝ), x ∈ Set.Icc a b → |Polynomial.eval x p - f x| < ε
[PROOFSTEP]
let f' : C(Set.Icc a b, ℝ) := ⟨fun x => f x, continuousOn_iff_continuous_restrict.mp c⟩
[GOAL]
a b : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b)
ε : ℝ
pos : 0 < ε
f' : C(↑(Set.Icc a b), ℝ) := ContinuousMap.mk fun x => f ↑x
⊢ ∃ p, ∀ (x : ℝ), x ∈ Set.Icc a b → |Polynomial.eval x p - f x| < ε
[PROOFSTEP]
obtain ⟨p, b⟩ := exists_polynomial_near_continuousMap a b f' ε pos
[GOAL]
case intro
a b✝ : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b✝)
ε : ℝ
pos : 0 < ε
f' : C(↑(Set.Icc a b✝), ℝ) := ContinuousMap.mk fun x => f ↑x
p : ℝ[X]
b : ‖Polynomial.toContinuousMapOn p (Set.Icc a b✝) - f'‖ < ε
⊢ ∃ p, ∀ (x : ℝ), x ∈ Set.Icc a b✝ → |Polynomial.eval x p - f x| < ε
[PROOFSTEP]
use p
[GOAL]
case h
a b✝ : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b✝)
ε : ℝ
pos : 0 < ε
f' : C(↑(Set.Icc a b✝), ℝ) := ContinuousMap.mk fun x => f ↑x
p : ℝ[X]
b : ‖Polynomial.toContinuousMapOn p (Set.Icc a b✝) - f'‖ < ε
⊢ ∀ (x : ℝ), x ∈ Set.Icc a b✝ → |Polynomial.eval x p - f x| < ε
[PROOFSTEP]
rw [norm_lt_iff _ pos] at b
[GOAL]
case h
a b✝ : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b✝)
ε : ℝ
pos : 0 < ε
f' : C(↑(Set.Icc a b✝), ℝ) := ContinuousMap.mk fun x => f ↑x
p : ℝ[X]
b : ∀ (x : ↑(Set.Icc a b✝)), ‖↑(Polynomial.toContinuousMapOn p (Set.Icc a b✝) - f') x‖ < ε
⊢ ∀ (x : ℝ), x ∈ Set.Icc a b✝ → |Polynomial.eval x p - f x| < ε
[PROOFSTEP]
intro x m
[GOAL]
case h
a b✝ : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b✝)
ε : ℝ
pos : 0 < ε
f' : C(↑(Set.Icc a b✝), ℝ) := ContinuousMap.mk fun x => f ↑x
p : ℝ[X]
b : ∀ (x : ↑(Set.Icc a b✝)), ‖↑(Polynomial.toContinuousMapOn p (Set.Icc a b✝) - f') x‖ < ε
x : ℝ
m : x ∈ Set.Icc a b✝
⊢ |Polynomial.eval x p - f x| < ε
[PROOFSTEP]
exact b ⟨x, m⟩


[GOAL]
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
⊢ #↑s < 𝔠
[PROOFSTEP]
by_contra' h
[GOAL]
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
⊢ False
[PROOFSTEP]
rcases exists_countable_dense X with ⟨t, htc, htd⟩
[GOAL]
case intro.intro
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : Set.Countable t
htd : Dense t
⊢ False
[PROOFSTEP]
haveI := htc.to_subtype
[GOAL]
case intro.intro
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : Set.Countable t
htd : Dense t
this : Countable ↑t
⊢ False
[PROOFSTEP]
refine (Cardinal.cantor 𝔠).not_le ?_
[GOAL]
case intro.intro
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : Set.Countable t
htd : Dense t
this : Countable ↑t
⊢ 2 ^ 𝔠 ≤ 𝔠
[PROOFSTEP]
calc
  -- Any function `s → ℝ` is continuous, hence `2 ^ 𝔠 ≤ #C(s, ℝ)`
  2 ^ 𝔠 ≤ #C(s, ℝ) :=
    by
    rw [(ContinuousMap.equivFnOfDiscrete _ _).cardinal_eq, mk_arrow, mk_real, lift_continuum, lift_uzero]
    exact
      (power_le_power_left two_ne_zero h).trans
        (power_le_power_right (nat_lt_continuum 2).le)
          -- By the Tietze Extension Theorem, any function `f : C(s, ℝ)` can be extended to `C(X, ℝ)`,
              -- hence `#C(s, ℝ) ≤ #C(X, ℝ)`
  _ ≤ #C(X, ℝ) := by
    choose f hf using (ContinuousMap.exists_restrict_eq_of_closed · hs)
    have hfi : Injective f := LeftInverse.injective hf
    exact mk_le_of_injective hfi
  _ ≤ #C(t, ℝ) := (mk_le_of_injective <| ContinuousMap.injective_restrict htd)
  _ ≤ #(t → ℝ) := (mk_le_of_injective FunLike.coe_injective)
  _ ≤ 𝔠 := by
    rw [mk_arrow, mk_real, lift_uzero, lift_continuum, continuum, ← power_mul]
    exact power_le_power_left two_ne_zero mk_le_aleph0
[GOAL]
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : Set.Countable t
htd : Dense t
this : Countable ↑t
⊢ 2 ^ 𝔠 ≤ #C(↑s, ℝ)
[PROOFSTEP]
rw [(ContinuousMap.equivFnOfDiscrete _ _).cardinal_eq, mk_arrow, mk_real, lift_continuum, lift_uzero]
[GOAL]
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : Set.Countable t
htd : Dense t
this : Countable ↑t
⊢ 2 ^ 𝔠 ≤ 𝔠 ^ #↑s
[PROOFSTEP]
exact
  (power_le_power_left two_ne_zero h).trans
    (power_le_power_right (nat_lt_continuum 2).le)
      -- By the Tietze Extension Theorem, any function `f : C(s, ℝ)` can be extended to `C(X, ℝ)`,
          -- hence `#C(s, ℝ) ≤ #C(X, ℝ)`
[GOAL]
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : Set.Countable t
htd : Dense t
this : Countable ↑t
⊢ #C(↑s, ℝ) ≤ #C(X, ℝ)
[PROOFSTEP]
choose f hf using (ContinuousMap.exists_restrict_eq_of_closed · hs)
[GOAL]
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : Set.Countable t
htd : Dense t
this : Countable ↑t
f : C(↑s, ℝ) → C(X, ℝ)
hf : ∀ (x : C(↑s, ℝ)), ContinuousMap.restrict s (f x) = x
⊢ #C(↑s, ℝ) ≤ #C(X, ℝ)
[PROOFSTEP]
have hfi : Injective f := LeftInverse.injective hf
[GOAL]
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : Set.Countable t
htd : Dense t
this : Countable ↑t
f : C(↑s, ℝ) → C(X, ℝ)
hf : ∀ (x : C(↑s, ℝ)), ContinuousMap.restrict s (f x) = x
hfi : Injective f
⊢ #C(↑s, ℝ) ≤ #C(X, ℝ)
[PROOFSTEP]
exact mk_le_of_injective hfi
[GOAL]
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : Set.Countable t
htd : Dense t
this : Countable ↑t
⊢ #(↑t → ℝ) ≤ 𝔠
[PROOFSTEP]
rw [mk_arrow, mk_real, lift_uzero, lift_continuum, continuum, ← power_mul]
[GOAL]
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : Set.Countable t
htd : Dense t
this : Countable ↑t
⊢ 2 ^ (ℵ₀ * #↑t) ≤ 2 ^ ℵ₀
[PROOFSTEP]
exact power_le_power_left two_ne_zero mk_le_aleph0


[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : α →CO β
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := f
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
g : α →CO β
toFun✝ : α → β
continuous_toFun✝ : Continuous toFun✝
map_open'✝ : IsOpenMap (ContinuousMap.mk toFun✝).toFun
h : (fun f => f.toFun) { toContinuousMap := ContinuousMap.mk toFun✝, map_open' := map_open'✝ } = (fun f => f.toFun) g
⊢ { toContinuousMap := ContinuousMap.mk toFun✝, map_open' := map_open'✝ } = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
toFun✝¹ : α → β
continuous_toFun✝¹ : Continuous toFun✝¹
map_open'✝¹ : IsOpenMap (ContinuousMap.mk toFun✝¹).toFun
toFun✝ : α → β
continuous_toFun✝ : Continuous toFun✝
map_open'✝ : IsOpenMap (ContinuousMap.mk toFun✝).toFun
h :
  (fun f => f.toFun) { toContinuousMap := ContinuousMap.mk toFun✝¹, map_open' := map_open'✝¹ } =
    (fun f => f.toFun) { toContinuousMap := ContinuousMap.mk toFun✝, map_open' := map_open'✝ }
⊢ { toContinuousMap := ContinuousMap.mk toFun✝¹, map_open' := map_open'✝¹ } =
    { toContinuousMap := ContinuousMap.mk toFun✝, map_open' := map_open'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
g : β →CO γ
f₁ f₂ : α →CO β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]


[GOAL]
X✝ Y✝ : CompHaus
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : (compHausToTop ⋙ topToLocale).map a₁✝ = (compHausToTop ⋙ topToLocale).map a₂✝
⊢ a₁✝ = a₂✝
[PROOFSTEP]
dsimp at h
[GOAL]
X✝ Y✝ : CompHaus
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : (Opens.comap a₁✝).op = (Opens.comap a₂✝).op
⊢ a₁✝ = a₂✝
[PROOFSTEP]
exact Opens.comap_injective (Quiver.Hom.op_inj h)


[GOAL]
⊢ T2Space Empty
[PROOFSTEP]
infer_instance
[GOAL]
X : UniformSpaceCat
Y : CpltSepUniformSpace
f : toUniformSpace (CpltSepUniformSpace.of (Completion ↑X)) ⟶ toUniformSpace Y
⊢ extensionHom (completionHom X ≫ f) = f
[PROOFSTEP]
apply Subtype.eq
[GOAL]
case a
X : UniformSpaceCat
Y : CpltSepUniformSpace
f : toUniformSpace (CpltSepUniformSpace.of (Completion ↑X)) ⟶ toUniformSpace Y
⊢ ↑(extensionHom (completionHom X ≫ f)) = ↑f
[PROOFSTEP]
funext x
[GOAL]
case a.h
X : UniformSpaceCat
Y : CpltSepUniformSpace
f : toUniformSpace (CpltSepUniformSpace.of (Completion ↑X)) ⟶ toUniformSpace Y
x : ↑(toUniformSpace (completionFunctor.obj X))
⊢ ↑(extensionHom (completionHom X ≫ f)) x = ↑f x
[PROOFSTEP]
exact congr_fun (Completion.extension_comp_coe f.property) x
[GOAL]
X : UniformSpaceCat
Y : CpltSepUniformSpace
f : completionFunctor.obj X ⟶ Y
⊢ (fun f => extensionHom f) ((fun f => completionHom X ≫ f) f) = f
[PROOFSTEP]
dsimp
[GOAL]
X : UniformSpaceCat
Y : CpltSepUniformSpace
f : completionFunctor.obj X ⟶ Y
⊢ extensionHom (completionHom X ≫ f) = f
[PROOFSTEP]
erw [extension_comp_coe]
[GOAL]
X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y
⊢ (fun f => completionHom X ≫ f) ((fun f => extensionHom f) f) = f
[PROOFSTEP]
apply Subtype.eq
[GOAL]
case a
X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y
⊢ ↑((fun f => completionHom X ≫ f) ((fun f => extensionHom f) f)) = ↑f
[PROOFSTEP]
funext x
[GOAL]
case a.h
X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y
x : ↑X
⊢ ↑((fun f => completionHom X ≫ f) ((fun f => extensionHom f) f)) x = ↑f x
[PROOFSTEP]
cases f
[GOAL]
case a.h.mk
X : UniformSpaceCat
Y : CpltSepUniformSpace
x : ↑X
val✝ : ↑X → ↑((forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y)
property✝ : UniformContinuous val✝
⊢ ↑((fun f => completionHom X ≫ f) ((fun f => extensionHom f) { val := val✝, property := property✝ })) x =
    ↑{ val := val✝, property := property✝ } x
[PROOFSTEP]
exact @Completion.extension_coe _ _ _ _ _ (CpltSepUniformSpace.separatedSpace _) ‹_› _
[GOAL]
X' X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X' ⟶ X
g : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y
⊢ ↑((fun X Y =>
              { toFun := fun f => completionHom X ≫ f, invFun := fun f => extensionHom f,
                left_inv :=
                  (_ :
                    ∀ (f : completionFunctor.obj X ⟶ Y),
                      (fun f => extensionHom f) ((fun f => completionHom X ≫ f) f) = f),
                right_inv :=
                  (_ :
                    ∀ (f : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y),
                      (fun f => completionHom X ≫ f) ((fun f => extensionHom f) f) = f) })
            X' Y).symm
      (f ≫ g) =
    completionFunctor.map f ≫
      ↑((fun X Y =>
                { toFun := fun f => completionHom X ≫ f, invFun := fun f => extensionHom f,
                  left_inv :=
                    (_ :
                      ∀ (f : completionFunctor.obj X ⟶ Y),
                        (fun f => extensionHom f) ((fun f => completionHom X ≫ f) f) = f),
                  right_inv :=
                    (_ :
                      ∀ (f : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y),
                        (fun f => completionHom X ≫ f) ((fun f => extensionHom f) f) = f) })
              X Y).symm
        g
[PROOFSTEP]
apply hom_ext
[GOAL]
case a
X' X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X' ⟶ X
g : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y
⊢ (forget UniformSpaceCat).map
      (↑((fun X Y =>
                { toFun := fun f => completionHom X ≫ f, invFun := fun f => extensionHom f,
                  left_inv :=
                    (_ :
                      ∀ (f : completionFunctor.obj X ⟶ Y),
                        (fun f => extensionHom f) ((fun f => completionHom X ≫ f) f) = f),
                  right_inv :=
                    (_ :
                      ∀ (f : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y),
                        (fun f => completionHom X ≫ f) ((fun f => extensionHom f) f) = f) })
              X' Y).symm
        (f ≫ g)) =
    (forget UniformSpaceCat).map
      (completionFunctor.map f ≫
        ↑((fun X Y =>
                  { toFun := fun f => completionHom X ≫ f, invFun := fun f => extensionHom f,
                    left_inv :=
                      (_ :
                        ∀ (f : completionFunctor.obj X ⟶ Y),
                          (fun f => extensionHom f) ((fun f => completionHom X ≫ f) f) = f),
                    right_inv :=
                      (_ :
                        ∀ (f : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y),
                          (fun f => completionHom X ≫ f) ((fun f => extensionHom f) f) = f) })
                X Y).symm
          g)
[PROOFSTEP]
funext x
[GOAL]
case a.h
X' X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X' ⟶ X
g : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y
x : (forget UniformSpaceCat).obj (toUniformSpace (completionFunctor.obj X'))
⊢ (forget UniformSpaceCat).map
      (↑((fun X Y =>
                { toFun := fun f => completionHom X ≫ f, invFun := fun f => extensionHom f,
                  left_inv :=
                    (_ :
                      ∀ (f : completionFunctor.obj X ⟶ Y),
                        (fun f => extensionHom f) ((fun f => completionHom X ≫ f) f) = f),
                  right_inv :=
                    (_ :
                      ∀ (f : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y),
                        (fun f => completionHom X ≫ f) ((fun f => extensionHom f) f) = f) })
              X' Y).symm
        (f ≫ g))
      x =
    (forget UniformSpaceCat).map
      (completionFunctor.map f ≫
        ↑((fun X Y =>
                  { toFun := fun f => completionHom X ≫ f, invFun := fun f => extensionHom f,
                    left_inv :=
                      (_ :
                        ∀ (f : completionFunctor.obj X ⟶ Y),
                          (fun f => extensionHom f) ((fun f => completionHom X ≫ f) f) = f),
                    right_inv :=
                      (_ :
                        ∀ (f : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y),
                          (fun f => completionHom X ≫ f) ((fun f => extensionHom f) f) = f) })
                X Y).symm
          g)
      x
[PROOFSTEP]
dsimp
[GOAL]
case a.h
X' X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X' ⟶ X
g : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y
x : (forget UniformSpaceCat).obj (toUniformSpace (completionFunctor.obj X'))
⊢ (forget UniformSpaceCat).map (extensionHom (f ≫ g)) x =
    (forget UniformSpaceCat).map (completionFunctor.map f ≫ extensionHom g) x
[PROOFSTEP]
erw [coe_comp]
  -- Porting note : used to be `erw [← Completion.extension_map]`
[GOAL]
case a.h
X' X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X' ⟶ X
g : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y
x : (forget UniformSpaceCat).obj (toUniformSpace (completionFunctor.obj X'))
⊢ (forget UniformSpaceCat).map (extensionHom (f ≫ g)) x =
    ((forget UniformSpaceCat).map (extensionHom g) ∘ (forget UniformSpaceCat).map (completionFunctor.map f)) x
[PROOFSTEP]
have := (Completion.extension_map (γ := Y) (f := g) g.2 f.2)
[GOAL]
case a.h
X' X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X' ⟶ X
g : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y
x : (forget UniformSpaceCat).obj (toUniformSpace (completionFunctor.obj X'))
this :
  Completion.extension ((forget UniformSpaceCat).map g) ∘ Completion.map ↑f =
    Completion.extension ((forget UniformSpaceCat).map g ∘ ↑f)
⊢ (forget UniformSpaceCat).map (extensionHom (f ≫ g)) x =
    ((forget UniformSpaceCat).map (extensionHom g) ∘ (forget UniformSpaceCat).map (completionFunctor.map f)) x
[PROOFSTEP]
simp only [forget_map_eq_coe] at this ⊢
[GOAL]
case a.h
X' X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X' ⟶ X
g : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y
x : (forget UniformSpaceCat).obj (toUniformSpace (completionFunctor.obj X'))
this : Completion.extension ↑g ∘ Completion.map ↑f = Completion.extension (↑g ∘ ↑f)
⊢ ↑(extensionHom (f ≫ g)) x = (↑(extensionHom g) ∘ ↑(completionFunctor.map f)) x
[PROOFSTEP]
erw [this]
[GOAL]
case a.h
X' X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X' ⟶ X
g : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y
x : (forget UniformSpaceCat).obj (toUniformSpace (completionFunctor.obj X'))
this : Completion.extension ↑g ∘ Completion.map ↑f = Completion.extension (↑g ∘ ↑f)
⊢ ↑(extensionHom (f ≫ g)) x = Completion.extension (↑g ∘ ↑f) x
[PROOFSTEP]
rfl


[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : MetricSpace β
inst✝ : NormedAddCommGroup E
f : C(α, β)
⊢ (mkOfCompact f).toContinuousMap = f
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : MetricSpace β
inst✝ : NormedAddCommGroup E
f : C(α, β)
a✝ : α
⊢ ↑(mkOfCompact f).toContinuousMap a✝ = ↑f a✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : MetricSpace β
inst✝ : NormedAddCommGroup E
f : α →ᵇ β
⊢ mkOfCompact f.toContinuousMap = f
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : MetricSpace β
inst✝ : NormedAddCommGroup E
f : α →ᵇ β
x✝ : α
⊢ ↑(mkOfCompact f.toContinuousMap) x✝ = ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : MetricSpace β
inst✝ : NormedAddCommGroup E
⊢ ∀ (s : Set (C(α, β) × C(α, β))),
    s ∈ uniformity C(α, β) ↔
      ∃ t,
        t ∈ uniformity (α →ᵇ β) ∧
          ∀ (x y : C(α, β)), (↑(equivBoundedOfCompact α β) x, ↑(equivBoundedOfCompact α β) y) ∈ t → (x, y) ∈ s
[PROOFSTEP]
simp only [hasBasis_compactConvergenceUniformity.mem_iff, uniformity_basis_dist_le.mem_iff]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : MetricSpace β
inst✝ : NormedAddCommGroup E
⊢ ∀ (s : Set (C(α, β) × C(α, β))),
    (∃ i,
        (IsCompact i.fst ∧ ∃ i_1, 0 < i_1 ∧ {p | dist p.fst p.snd ≤ i_1} ⊆ i.snd) ∧
          {fg | ∀ (x : α), x ∈ i.fst → (↑fg.fst x, ↑fg.snd x) ∈ i.snd} ⊆ s) ↔
      ∃ t,
        (∃ i, 0 < i ∧ {p | dist p.fst p.snd ≤ i} ⊆ t) ∧
          ∀ (x y : C(α, β)), (↑(equivBoundedOfCompact α β) x, ↑(equivBoundedOfCompact α β) y) ∈ t → (x, y) ∈ s
[PROOFSTEP]
exact fun s =>
  ⟨fun ⟨⟨a, b⟩, ⟨_, ⟨ε, hε, hb⟩⟩, hs⟩ =>
    ⟨{p | ∀ x, (p.1 x, p.2 x) ∈ b}, ⟨ε, hε, fun _ h x => hb ((dist_le hε.le).mp h x)⟩, fun f g h => hs fun x _ => h x⟩,
    fun ⟨_, ⟨ε, hε, ht⟩, hs⟩ =>
    ⟨⟨Set.univ, {p | dist p.1 p.2 ≤ ε}⟩, ⟨isCompact_univ, ⟨ε, hε, fun _ h => h⟩⟩, fun ⟨f, g⟩ h =>
      hs _ _ (ht ((dist_le hε.le).mpr fun x => h x (mem_univ x)))⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : MetricSpace β
inst✝ : NormedAddCommGroup E
f g : C(α, β)
C : ℝ
x : α
⊢ dist (↑f x) (↑g x) ≤ dist f g
[PROOFSTEP]
simp only [← dist_mkOfCompact, dist_coe_le_dist, ← mkOfCompact_apply]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : MetricSpace β
inst✝ : NormedAddCommGroup E
f g : C(α, β)
C : ℝ
C0 : 0 ≤ C
⊢ dist f g ≤ C ↔ ∀ (x : α), dist (↑f x) (↑g x) ≤ C
[PROOFSTEP]
simp only [← dist_mkOfCompact, BoundedContinuousFunction.dist_le C0, mkOfCompact_apply]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : CompactSpace α
inst✝² : MetricSpace β
inst✝¹ : NormedAddCommGroup E
f g : C(α, β)
C : ℝ
inst✝ : Nonempty α
⊢ dist f g ≤ C ↔ ∀ (x : α), dist (↑f x) (↑g x) ≤ C
[PROOFSTEP]
simp only [← dist_mkOfCompact, BoundedContinuousFunction.dist_le_iff_of_nonempty, mkOfCompact_apply]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : CompactSpace α
inst✝² : MetricSpace β
inst✝¹ : NormedAddCommGroup E
f g : C(α, β)
C : ℝ
inst✝ : Nonempty α
⊢ dist f g < C ↔ ∀ (x : α), dist (↑f x) (↑g x) < C
[PROOFSTEP]
simp only [← dist_mkOfCompact, dist_lt_iff_of_nonempty_compact, mkOfCompact_apply]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : MetricSpace β
inst✝ : NormedAddCommGroup E
f g : C(α, β)
C : ℝ
C0 : 0 < C
⊢ dist f g < C ↔ ∀ (x : α), dist (↑f x) (↑g x) < C
[PROOFSTEP]
rw [← dist_mkOfCompact, dist_lt_iff_of_compact C0]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : MetricSpace β
inst✝ : NormedAddCommGroup E
f g : C(α, β)
C : ℝ
C0 : 0 < C
⊢ (∀ (x : α), dist (↑(mkOfCompact f) x) (↑(mkOfCompact g) x) < C) ↔ ∀ (x : α), dist (↑f x) (↑g x) < C
[PROOFSTEP]
simp only [mkOfCompact_apply]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : MetricSpace β
inst✝ : NormedAddCommGroup E
src✝¹ : MetricSpace C(α, E) := metricSpace α E
src✝ : AddCommGroup C(α, E) := instAddCommGroupContinuousMap
x y : C(α, E)
⊢ dist x y = ‖x - y‖
[PROOFSTEP]
rw [← norm_mkOfCompact, ← dist_mkOfCompact, dist_eq_norm, mkOfCompact_sub]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁶ : TopologicalSpace α
inst✝⁵ : CompactSpace α
inst✝⁴ : MetricSpace β
inst✝³ : NormedAddCommGroup E
inst✝² : Nonempty α
inst✝¹ : One E
inst✝ : NormOneClass E
⊢ ‖1‖ = 1
[PROOFSTEP]
simp only [← norm_mkOfCompact, mkOfCompact_one, norm_one]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : CompactSpace α
inst✝³ : MetricSpace β
inst✝² : NormedAddCommGroup E
𝕜 : Type u_4
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
src✝ : C(α, E) ≃+ (α →ᵇ E) := addEquivBoundedOfCompact α E
c : 𝕜
f : C(α, E)
⊢ AddHom.toFun
      { toFun := src✝.toFun,
        map_add' :=
          (_ :
            ∀ (x y : C(α, E)),
              Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
      (c • f) =
    ↑(RingHom.id 𝕜) c •
      AddHom.toFun
        { toFun := src✝.toFun,
          map_add' :=
            (_ :
              ∀ (x y : C(α, E)),
                Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
        f
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : CompactSpace α
inst✝³ : MetricSpace β
inst✝² : NormedAddCommGroup E
𝕜 : Type u_4
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
src✝ : C(α, E) ≃+ (α →ᵇ E) := addEquivBoundedOfCompact α E
c : 𝕜
f : C(α, E)
x✝ : α
⊢ ↑(AddHom.toFun
          { toFun := src✝.toFun,
            map_add' :=
              (_ :
                ∀ (x y : C(α, E)),
                  Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
          (c • f))
      x✝ =
    ↑(↑(RingHom.id 𝕜) c •
          AddHom.toFun
            { toFun := src✝.toFun,
              map_add' :=
                (_ :
                  ∀ (x y : C(α, E)),
                    Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
            f)
      x✝
[PROOFSTEP]
norm_cast
[GOAL]
X : Type u_1
𝕜 : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁶ : TopologicalSpace X
inst✝⁵ : CompactSpace X
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup β
inst✝² : NormedSpace 𝕜 β
inst✝¹ : NormedAddCommGroup γ
inst✝ : NormedSpace 𝕜 γ
g : β →L[𝕜] γ
⊢ ↑(ContinuousLinearMap.compLeftContinuousCompact X g) = ContinuousLinearMap.compLeftContinuous 𝕜 X g
[PROOFSTEP]
ext f
[GOAL]
case h.h
X : Type u_1
𝕜 : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁶ : TopologicalSpace X
inst✝⁵ : CompactSpace X
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup β
inst✝² : NormedSpace 𝕜 β
inst✝¹ : NormedAddCommGroup γ
inst✝ : NormedSpace 𝕜 γ
g : β →L[𝕜] γ
f : C(X, β)
a✝ : X
⊢ ↑(↑↑(ContinuousLinearMap.compLeftContinuousCompact X g) f) a✝ =
    ↑(↑(ContinuousLinearMap.compLeftContinuous 𝕜 X g) f) a✝
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
Y : Type u_2
T : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace Y
inst✝ : MetricSpace T
f : C(X, Y)
⊢ Continuous fun g => comp g f
[PROOFSTEP]
refine' Metric.continuous_iff.mpr _
[GOAL]
X : Type u_1
Y : Type u_2
T : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace Y
inst✝ : MetricSpace T
f : C(X, Y)
⊢ ∀ (b : C(Y, T)) (ε : ℝ), ε > 0 → ∃ δ, δ > 0 ∧ ∀ (a : C(Y, T)), dist a b < δ → dist (comp a f) (comp b f) < ε
[PROOFSTEP]
intro g ε ε_pos
[GOAL]
X : Type u_1
Y : Type u_2
T : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace Y
inst✝ : MetricSpace T
f : C(X, Y)
g : C(Y, T)
ε : ℝ
ε_pos : ε > 0
⊢ ∃ δ, δ > 0 ∧ ∀ (a : C(Y, T)), dist a g < δ → dist (comp a f) (comp g f) < ε
[PROOFSTEP]
refine' ⟨ε, ε_pos, fun g' h => _⟩
[GOAL]
X : Type u_1
Y : Type u_2
T : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace Y
inst✝ : MetricSpace T
f : C(X, Y)
g : C(Y, T)
ε : ℝ
ε_pos : ε > 0
g' : C(Y, T)
h : dist g' g < ε
⊢ dist (comp g' f) (comp g f) < ε
[PROOFSTEP]
rw [ContinuousMap.dist_lt_iff ε_pos] at h ⊢
[GOAL]
X : Type u_1
Y : Type u_2
T : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace Y
inst✝ : MetricSpace T
f : C(X, Y)
g : C(Y, T)
ε : ℝ
ε_pos : ε > 0
g' : C(Y, T)
h : ∀ (x : Y), dist (↑g' x) (↑g x) < ε
⊢ ∀ (x : X), dist (↑(comp g' f) x) (↑(comp g f) x) < ε
[PROOFSTEP]
exact fun x => h (f x)
[GOAL]
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
⊢ Summable F
[PROOFSTEP]
refine' (ContinuousMap.exists_tendsto_compactOpen_iff_forall _).2 fun K hK => _
[GOAL]
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Set X
hK : IsCompact K
⊢ ∃ f, Tendsto (fun i => restrict K (∑ b in i, F b)) atTop (𝓝 f)
[PROOFSTEP]
lift K to Compacts X using hK
[GOAL]
case intro
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
⊢ ∃ f, Tendsto (fun i => restrict (↑K) (∑ b in i, F b)) atTop (𝓝 f)
[PROOFSTEP]
have A : ∀ s : Finset ι, restrict (↑K) (∑ i in s, F i) = ∑ i in s, restrict K (F i) :=
  by
  intro s
  ext1 x
  simp
[GOAL]
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
⊢ ∀ (s : Finset ι), restrict (↑K) (∑ i in s, F i) = ∑ i in s, restrict (↑K) (F i)
[PROOFSTEP]
intro s
[GOAL]
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
s : Finset ι
⊢ restrict (↑K) (∑ i in s, F i) = ∑ i in s, restrict (↑K) (F i)
[PROOFSTEP]
ext1 x
[GOAL]
case h
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
s : Finset ι
x : ↑↑K
⊢ ↑(restrict (↑K) (∑ i in s, F i)) x = ↑(∑ i in s, restrict (↑K) (F i)) x
[PROOFSTEP]
simp
[GOAL]
case intro
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
A : ∀ (s : Finset ι), restrict (↑K) (∑ i in s, F i) = ∑ i in s, restrict (↑K) (F i)
⊢ ∃ f, Tendsto (fun i => restrict (↑K) (∑ b in i, F b)) atTop (𝓝 f)
[PROOFSTEP]
simpa only [HasSum, A] using summable_of_summable_norm (hF K)
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedAddCommGroup β
inst✝² : StarAddMonoid β
inst✝¹ : NormedStarGroup β
inst✝ : CompactSpace α
f : C(α, β)
⊢ ‖star f‖ = ‖f‖
[PROOFSTEP]
rw [← BoundedContinuousFunction.norm_mkOfCompact, BoundedContinuousFunction.mkOfCompact_star, norm_star,
  BoundedContinuousFunction.norm_mkOfCompact]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedRing β
inst✝² : StarRing β
inst✝¹ : CompactSpace α
inst✝ : CstarRing β
f : C(α, β)
⊢ ‖star f * f‖ = ‖f‖ * ‖f‖
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedRing β
inst✝² : StarRing β
inst✝¹ : CompactSpace α
inst✝ : CstarRing β
f : C(α, β)
⊢ ‖star f * f‖ ≤ ‖f‖ * ‖f‖
[PROOFSTEP]
rw [← sq, ContinuousMap.norm_le _ (sq_nonneg _)]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedRing β
inst✝² : StarRing β
inst✝¹ : CompactSpace α
inst✝ : CstarRing β
f : C(α, β)
⊢ ∀ (x : α), ‖↑(star f * f) x‖ ≤ ‖f‖ ^ 2
[PROOFSTEP]
intro x
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedRing β
inst✝² : StarRing β
inst✝¹ : CompactSpace α
inst✝ : CstarRing β
f : C(α, β)
x : α
⊢ ‖↑(star f * f) x‖ ≤ ‖f‖ ^ 2
[PROOFSTEP]
simp only [ContinuousMap.coe_mul, coe_star, Pi.mul_apply, Pi.star_apply, CstarRing.norm_star_mul_self, ← sq]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedRing β
inst✝² : StarRing β
inst✝¹ : CompactSpace α
inst✝ : CstarRing β
f : C(α, β)
x : α
⊢ ‖↑f x‖ ^ 2 ≤ ‖f‖ ^ 2
[PROOFSTEP]
refine' sq_le_sq' _ _
[GOAL]
case refine'_1.refine'_1
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedRing β
inst✝² : StarRing β
inst✝¹ : CompactSpace α
inst✝ : CstarRing β
f : C(α, β)
x : α
⊢ -‖f‖ ≤ ‖↑f x‖
[PROOFSTEP]
linarith [norm_nonneg (f x), norm_nonneg f]
[GOAL]
case refine'_1.refine'_2
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedRing β
inst✝² : StarRing β
inst✝¹ : CompactSpace α
inst✝ : CstarRing β
f : C(α, β)
x : α
⊢ ‖↑f x‖ ≤ ‖f‖
[PROOFSTEP]
exact ContinuousMap.norm_coe_le_norm f x
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedRing β
inst✝² : StarRing β
inst✝¹ : CompactSpace α
inst✝ : CstarRing β
f : C(α, β)
⊢ ‖f‖ * ‖f‖ ≤ ‖star f * f‖
[PROOFSTEP]
rw [← sq, ← Real.le_sqrt (norm_nonneg _) (norm_nonneg _), ContinuousMap.norm_le _ (Real.sqrt_nonneg _)]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedRing β
inst✝² : StarRing β
inst✝¹ : CompactSpace α
inst✝ : CstarRing β
f : C(α, β)
⊢ ∀ (x : α), ‖↑f x‖ ≤ Real.sqrt ‖star f * f‖
[PROOFSTEP]
intro x
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedRing β
inst✝² : StarRing β
inst✝¹ : CompactSpace α
inst✝ : CstarRing β
f : C(α, β)
x : α
⊢ ‖↑f x‖ ≤ Real.sqrt ‖star f * f‖
[PROOFSTEP]
rw [Real.le_sqrt (norm_nonneg _) (norm_nonneg _), sq, ← CstarRing.norm_star_mul_self]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedRing β
inst✝² : StarRing β
inst✝¹ : CompactSpace α
inst✝ : CstarRing β
f : C(α, β)
x : α
⊢ ‖star (↑f x) * ↑f x‖ ≤ ‖star f * f‖
[PROOFSTEP]
exact ContinuousMap.norm_coe_le_norm (star f * f) x


[GOAL]
α : Type
inst✝ : Fintype α
B✝ : Stonean
X : α → Stonean
B : Stonean
e : (a : α) → X a ⟶ B
⊢ Continuous fun x =>
    match x with
    | { fst := a, snd := x } => ↑(e a) x
[PROOFSTEP]
apply continuous_sigma
[GOAL]
case hf
α : Type
inst✝ : Fintype α
B✝ : Stonean
X : α → Stonean
B : Stonean
e : (a : α) → X a ⟶ B
⊢ ∀ (i : α),
    Continuous fun a =>
      match { fst := i, snd := a } with
      | { fst := a, snd := x } => ↑(e a) x
[PROOFSTEP]
intro a
[GOAL]
case hf
α : Type
inst✝ : Fintype α
B✝ : Stonean
X : α → Stonean
B : Stonean
e : (a : α) → X a ⟶ B
a : α
⊢ Continuous fun a_1 =>
    match { fst := a, snd := a_1 } with
    | { fst := a, snd := x } => ↑(e a) x
[PROOFSTEP]
exact (e a).continuous
[GOAL]
α : Type
inst✝ : Fintype α
B✝ : Stonean
X : α → Stonean
B : Stonean
f g : finiteCoproduct X ⟶ B
h : ∀ (a : α), ι X a ≫ f = ι X a ≫ g
⊢ f = g
[PROOFSTEP]
ext ⟨a, x⟩
[GOAL]
case w.mk
α : Type
inst✝ : Fintype α
B✝ : Stonean
X : α → Stonean
B : Stonean
f g : finiteCoproduct X ⟶ B
h : ∀ (a : α), ι X a ≫ f = ι X a ≫ g
a : α
x : CoeSort.coe (X a)
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }
[PROOFSTEP]
specialize h a
[GOAL]
case w.mk
α : Type
inst✝ : Fintype α
B✝ : Stonean
X : α → Stonean
B : Stonean
f g : finiteCoproduct X ⟶ B
a : α
x : CoeSort.coe (X a)
h : ι X a ≫ f = ι X a ≫ g
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }
[PROOFSTEP]
apply_fun (fun q => q x) at h
[GOAL]
case w.mk
α : Type
inst✝ : Fintype α
B✝ : Stonean
X : α → Stonean
B : Stonean
f g : finiteCoproduct X ⟶ B
a : α
x : CoeSort.coe (X a)
h : ↑(ι X a ≫ f) x = ↑(ι X a ≫ g) x
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }
[PROOFSTEP]
exact h
[GOAL]
α : Type
inst✝ : Fintype α
B : Stonean
X : α → Stonean
F : Discrete α ⥤ Stonean
s : Cocone F
m : (cocone F).pt ⟶ s.pt
hm : ∀ (j : Discrete α), NatTrans.app (cocone F).ι j ≫ m = NatTrans.app s.ι j
a : Discrete α
⊢ ι (fun a => F.obj a) a ≫ m = ι (fun a => F.obj a) a ≫ (fun s => desc (fun a => F.obj a) fun a => NatTrans.app s.ι a) s
[PROOFSTEP]
specialize hm a
[GOAL]
α : Type
inst✝ : Fintype α
B : Stonean
X : α → Stonean
F : Discrete α ⥤ Stonean
s : Cocone F
m : (cocone F).pt ⟶ s.pt
a : Discrete α
hm : NatTrans.app (cocone F).ι a ≫ m = NatTrans.app s.ι a
⊢ ι (fun a => F.obj a) a ≫ m = ι (fun a => F.obj a) a ≫ (fun s => desc (fun a => F.obj a) fun a => NatTrans.app s.ι a) s
[PROOFSTEP]
ext t
[GOAL]
case w
α : Type
inst✝ : Fintype α
B : Stonean
X : α → Stonean
F : Discrete α ⥤ Stonean
s : Cocone F
m : (cocone F).pt ⟶ s.pt
a : Discrete α
hm : NatTrans.app (cocone F).ι a ≫ m = NatTrans.app s.ι a
t : (forget Stonean).obj (F.obj a)
⊢ ↑(ι (fun a => F.obj a) a ≫ m) t =
    ↑(ι (fun a => F.obj a) a ≫ (fun s => desc (fun a => F.obj a) fun a => NatTrans.app s.ι a) s) t
[PROOFSTEP]
apply_fun (fun q => q t) at hm
[GOAL]
case w
α : Type
inst✝ : Fintype α
B : Stonean
X : α → Stonean
F : Discrete α ⥤ Stonean
s : Cocone F
m : (cocone F).pt ⟶ s.pt
a : Discrete α
t : (forget Stonean).obj (F.obj a)
hm : ↑(NatTrans.app (cocone F).ι a ≫ m) t = ↑(NatTrans.app s.ι a) t
⊢ ↑(ι (fun a => F.obj a) a ≫ m) t =
    ↑(ι (fun a => F.obj a) a ≫ (fun s => desc (fun a => F.obj a) fun a => NatTrans.app s.ι a) s) t
[PROOFSTEP]
exact hm


[GOAL]
R : TopCommRingCat
⊢ Continuous ↑(RingHom.id R.α)
[PROOFSTEP]
rw [RingHom.id]
[GOAL]
R : TopCommRingCat
⊢ Continuous
    ↑{
        toMonoidHom :=
          { toOneHom := { toFun := id, map_one' := (_ : id 1 = id 1) },
            map_mul' :=
              (_ :
                ∀ (x y : R.α),
                  OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y) =
                    OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y)) },
        map_zero' :=
          (_ :
            OneHom.toFun
                (↑{ toOneHom := { toFun := id, map_one' := (_ : id 1 = id 1) },
                    map_mul' :=
                      (_ :
                        ∀ (x y : R.α),
                          OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y) =
                            OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y)) })
                0 =
              OneHom.toFun
                (↑{ toOneHom := { toFun := id, map_one' := (_ : id 1 = id 1) },
                    map_mul' :=
                      (_ :
                        ∀ (x y : R.α),
                          OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y) =
                            OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y)) })
                0),
        map_add' :=
          (_ :
            ∀ (x y : R.α),
              OneHom.toFun
                  (↑{ toOneHom := { toFun := id, map_one' := (_ : id 1 = id 1) },
                      map_mul' :=
                        (_ :
                          ∀ (x y : R.α),
                            OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y) =
                              OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y)) })
                  (x + y) =
                OneHom.toFun
                  (↑{ toOneHom := { toFun := id, map_one' := (_ : id 1 = id 1) },
                      map_mul' :=
                        (_ :
                          ∀ (x y : R.α),
                            OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y) =
                              OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y)) })
                  (x + y)) }
[PROOFSTEP]
continuity
[GOAL]
X✝ Y✝ Z✝ : TopCommRingCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Continuous ↑(RingHom.comp ↑g ↑f)
[PROOFSTEP]
cases f
[GOAL]
case mk
X✝ Y✝ Z✝ : TopCommRingCat
g : Y✝ ⟶ Z✝
val✝ : X✝.α →+* Y✝.α
property✝ : Continuous ↑val✝
⊢ Continuous ↑(RingHom.comp ↑g ↑{ val := val✝, property := property✝ })
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
X✝ Y✝ Z✝ : TopCommRingCat
val✝¹ : X✝.α →+* Y✝.α
property✝¹ : Continuous ↑val✝¹
val✝ : Y✝.α →+* Z✝.α
property✝ : Continuous ↑val✝
⊢ Continuous ↑(RingHom.comp ↑{ val := val✝, property := property✝ } ↑{ val := val✝¹, property := property✝¹ })
[PROOFSTEP]
dsimp
[GOAL]
case mk.mk
X✝ Y✝ Z✝ : TopCommRingCat
val✝¹ : X✝.α →+* Y✝.α
property✝¹ : Continuous ↑val✝¹
val✝ : Y✝.α →+* Z✝.α
property✝ : Continuous ↑val✝
⊢ Continuous (↑val✝ ∘ ↑val✝¹)
[PROOFSTEP]
apply Continuous.comp
[GOAL]
case mk.mk.hg
X✝ Y✝ Z✝ : TopCommRingCat
val✝¹ : X✝.α →+* Y✝.α
property✝¹ : Continuous ↑val✝¹
val✝ : Y✝.α →+* Z✝.α
property✝ : Continuous ↑val✝
⊢ Continuous ↑val✝
[PROOFSTEP]
assumption
[GOAL]
case mk.mk.hf
X✝ Y✝ Z✝ : TopCommRingCat
val✝¹ : X✝.α →+* Y✝.α
property✝¹ : Continuous ↑val✝¹
val✝ : Y✝.α →+* Z✝.α
property✝ : Continuous ↑val✝
⊢ Continuous ↑val✝¹
[PROOFSTEP]
assumption
[GOAL]
X Y : TopCommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget₂ TopCommRingCat TopCat).map f)
⊢ IsIso f
[PROOFSTEP]
let i_Top :=
  asIso
    ((forget₂ TopCommRingCat TopCat).map f)
      -- and a `RingEquiv`.
[GOAL]
X Y : TopCommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget₂ TopCommRingCat TopCat).map f)
i_Top : (forget₂ TopCommRingCat TopCat).obj X ≅ (forget₂ TopCommRingCat TopCat).obj Y :=
  asIso ((forget₂ TopCommRingCat TopCat).map f)
⊢ IsIso f
[PROOFSTEP]
let e_Ring : X ≃+* Y :=
  { f.1, ((forget TopCat).mapIso i_Top).toEquiv with }
    -- Putting these together we obtain the isomorphism we're after:
[GOAL]
X Y : TopCommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget₂ TopCommRingCat TopCat).map f)
i_Top : (forget₂ TopCommRingCat TopCat).obj X ≅ (forget₂ TopCommRingCat TopCat).obj Y :=
  asIso ((forget₂ TopCommRingCat TopCat).map f)
e_Ring : X.α ≃+* Y.α :=
  let src := ↑f;
  let src_1 := ((forget TopCat).mapIso i_Top).toEquiv;
  {
    toEquiv :=
      { toFun := src.toFun, invFun := src_1.invFun, left_inv := (_ : Function.LeftInverse src_1.invFun src_1.toFun),
        right_inv := (_ : Function.RightInverse src_1.invFun src_1.toFun) },
    map_mul' := (_ : ∀ (x y : X.α), OneHom.toFun (↑↑src) (x * y) = OneHom.toFun (↑↑src) x * OneHom.toFun (↑↑src) y),
    map_add' := (_ : ∀ (x y : X.α), OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) }
⊢ IsIso f
[PROOFSTEP]
exact
  ⟨⟨⟨e_Ring.symm, i_Top.inv.2⟩,
      ⟨by
        ext x
        exact e_Ring.left_inv x, by
        ext x
        exact e_Ring.right_inv x⟩⟩⟩
[GOAL]
X Y : TopCommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget₂ TopCommRingCat TopCat).map f)
i_Top : (forget₂ TopCommRingCat TopCat).obj X ≅ (forget₂ TopCommRingCat TopCat).obj Y :=
  asIso ((forget₂ TopCommRingCat TopCat).map f)
e_Ring : X.α ≃+* Y.α :=
  let src := ↑f;
  let src_1 := ((forget TopCat).mapIso i_Top).toEquiv;
  {
    toEquiv :=
      { toFun := src.toFun, invFun := src_1.invFun, left_inv := (_ : Function.LeftInverse src_1.invFun src_1.toFun),
        right_inv := (_ : Function.RightInverse src_1.invFun src_1.toFun) },
    map_mul' := (_ : ∀ (x y : X.α), OneHom.toFun (↑↑src) (x * y) = OneHom.toFun (↑↑src) x * OneHom.toFun (↑↑src) y),
    map_add' := (_ : ∀ (x y : X.α), OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) }
⊢ f ≫ { val := ↑(RingEquiv.symm e_Ring), property := (_ : Continuous i_Top.inv.toFun) } = 𝟙 X
[PROOFSTEP]
ext x
[GOAL]
case w
X Y : TopCommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget₂ TopCommRingCat TopCat).map f)
i_Top : (forget₂ TopCommRingCat TopCat).obj X ≅ (forget₂ TopCommRingCat TopCat).obj Y :=
  asIso ((forget₂ TopCommRingCat TopCat).map f)
e_Ring : X.α ≃+* Y.α :=
  let src := ↑f;
  let src_1 := ((forget TopCat).mapIso i_Top).toEquiv;
  {
    toEquiv :=
      { toFun := src.toFun, invFun := src_1.invFun, left_inv := (_ : Function.LeftInverse src_1.invFun src_1.toFun),
        right_inv := (_ : Function.RightInverse src_1.invFun src_1.toFun) },
    map_mul' := (_ : ∀ (x y : X.α), OneHom.toFun (↑↑src) (x * y) = OneHom.toFun (↑↑src) x * OneHom.toFun (↑↑src) y),
    map_add' := (_ : ∀ (x y : X.α), OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) }
x : (forget TopCommRingCat).obj X
⊢ ↑(f ≫ { val := ↑(RingEquiv.symm e_Ring), property := (_ : Continuous i_Top.inv.toFun) }) x = ↑(𝟙 X) x
[PROOFSTEP]
exact e_Ring.left_inv x
[GOAL]
X Y : TopCommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget₂ TopCommRingCat TopCat).map f)
i_Top : (forget₂ TopCommRingCat TopCat).obj X ≅ (forget₂ TopCommRingCat TopCat).obj Y :=
  asIso ((forget₂ TopCommRingCat TopCat).map f)
e_Ring : X.α ≃+* Y.α :=
  let src := ↑f;
  let src_1 := ((forget TopCat).mapIso i_Top).toEquiv;
  {
    toEquiv :=
      { toFun := src.toFun, invFun := src_1.invFun, left_inv := (_ : Function.LeftInverse src_1.invFun src_1.toFun),
        right_inv := (_ : Function.RightInverse src_1.invFun src_1.toFun) },
    map_mul' := (_ : ∀ (x y : X.α), OneHom.toFun (↑↑src) (x * y) = OneHom.toFun (↑↑src) x * OneHom.toFun (↑↑src) y),
    map_add' := (_ : ∀ (x y : X.α), OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) }
⊢ { val := ↑(RingEquiv.symm e_Ring), property := (_ : Continuous i_Top.inv.toFun) } ≫ f = 𝟙 Y
[PROOFSTEP]
ext x
[GOAL]
case w
X Y : TopCommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget₂ TopCommRingCat TopCat).map f)
i_Top : (forget₂ TopCommRingCat TopCat).obj X ≅ (forget₂ TopCommRingCat TopCat).obj Y :=
  asIso ((forget₂ TopCommRingCat TopCat).map f)
e_Ring : X.α ≃+* Y.α :=
  let src := ↑f;
  let src_1 := ((forget TopCat).mapIso i_Top).toEquiv;
  {
    toEquiv :=
      { toFun := src.toFun, invFun := src_1.invFun, left_inv := (_ : Function.LeftInverse src_1.invFun src_1.toFun),
        right_inv := (_ : Function.RightInverse src_1.invFun src_1.toFun) },
    map_mul' := (_ : ∀ (x y : X.α), OneHom.toFun (↑↑src) (x * y) = OneHom.toFun (↑↑src) x * OneHom.toFun (↑↑src) y),
    map_add' := (_ : ∀ (x y : X.α), OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) }
x : (forget TopCommRingCat).obj Y
⊢ ↑({ val := ↑(RingEquiv.symm e_Ring), property := (_ : Continuous i_Top.inv.toFun) } ≫ f) x = ↑(𝟙 Y) x
[PROOFSTEP]
exact e_Ring.right_inv x