[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup E'
inst✝⁸ : Module ℝ E'
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : AddCommGroup F'
inst✝⁴ : Module ℝ F'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace E'
inst✝¹ : UniformSpace F
inst✝ : UniformAddGroup F
𝔖 : Set (Set E)
⊢ strongTopology σ F 𝔖 = UniformSpace.toTopologicalSpace
[PROOFSTEP]
rw [strongTopology, UniformAddGroup.toUniformSpace_eq]
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup E'
inst✝⁸ : Module ℝ E'
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : AddCommGroup F'
inst✝⁴ : Module ℝ F'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace E'
inst✝¹ : UniformSpace F
inst✝ : UniformAddGroup F
𝔖 : Set (Set E)
⊢ TopologicalSpace.induced FunLike.coe (UniformOnFun.topologicalSpace E F 𝔖) = UniformSpace.toTopologicalSpace
[PROOFSTEP]
rfl
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup E'
inst✝⁸ : Module ℝ E'
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : AddCommGroup F'
inst✝⁴ : Module ℝ F'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace E'
inst✝¹ : UniformSpace F
inst✝ : UniformAddGroup F
𝔖 : Set (Set E)
⊢ UniformAddGroup (E →SL[σ] F)
[PROOFSTEP]
letI : UniformSpace (E →SL[σ] F) := strongUniformity σ F 𝔖
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup E'
inst✝⁸ : Module ℝ E'
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : AddCommGroup F'
inst✝⁴ : Module ℝ F'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace E'
inst✝¹ : UniformSpace F
inst✝ : UniformAddGroup F
𝔖 : Set (Set E)
this : UniformSpace (E →SL[σ] F) := strongUniformity σ F 𝔖
⊢ UniformAddGroup (E →SL[σ] F)
[PROOFSTEP]
rw [strongUniformity, UniformSpace.replaceTopology_eq]
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup E'
inst✝⁸ : Module ℝ E'
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : AddCommGroup F'
inst✝⁴ : Module ℝ F'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace E'
inst✝¹ : UniformSpace F
inst✝ : UniformAddGroup F
𝔖 : Set (Set E)
this : UniformSpace (E →SL[σ] F) := strongUniformity σ F 𝔖
⊢ UniformAddGroup (E →SL[σ] F)
[PROOFSTEP]
let φ : (E →SL[σ] F) →+ E →ᵤ[𝔖] F := ⟨⟨(FunLike.coe : (E →SL[σ] F) → E →ᵤ[𝔖] F), rfl⟩, fun _ _ => rfl⟩
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup E'
inst✝⁸ : Module ℝ E'
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : AddCommGroup F'
inst✝⁴ : Module ℝ F'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace E'
inst✝¹ : UniformSpace F
inst✝ : UniformAddGroup F
𝔖 : Set (Set E)
this : UniformSpace (E →SL[σ] F) := strongUniformity σ F 𝔖
φ : (E →SL[σ] F) →+ E →ᵤ[𝔖] F :=
  { toZeroHom := { toFun := FunLike.coe, map_zero' := (_ : ↑0 = ↑0) },
    map_add' :=
      (_ :
        ∀ (x x_1 : E →SL[σ] F),
          ZeroHom.toFun { toFun := FunLike.coe, map_zero' := (_ : ↑0 = ↑0) } (x + x_1) =
            ZeroHom.toFun { toFun := FunLike.coe, map_zero' := (_ : ↑0 = ↑0) } (x + x_1)) }
⊢ UniformAddGroup (E →SL[σ] F)
[PROOFSTEP]
exact uniformAddGroup_comap φ
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup E'
inst✝⁸ : Module ℝ E'
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : AddCommGroup F'
inst✝⁴ : Module ℝ F'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace E'
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
𝔖 : Set (Set E)
⊢ TopologicalAddGroup (E →SL[σ] F)
[PROOFSTEP]
letI : UniformSpace F := TopologicalAddGroup.toUniformSpace F
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup E'
inst✝⁸ : Module ℝ E'
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : AddCommGroup F'
inst✝⁴ : Module ℝ F'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace E'
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
𝔖 : Set (Set E)
this : UniformSpace F := TopologicalAddGroup.toUniformSpace F
⊢ TopologicalAddGroup (E →SL[σ] F)
[PROOFSTEP]
haveI : UniformAddGroup F := comm_topologicalAddGroup_is_uniform
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup E'
inst✝⁸ : Module ℝ E'
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : AddCommGroup F'
inst✝⁴ : Module ℝ F'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace E'
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
𝔖 : Set (Set E)
this✝ : UniformSpace F := TopologicalAddGroup.toUniformSpace F
this : UniformAddGroup F
⊢ TopologicalAddGroup (E →SL[σ] F)
[PROOFSTEP]
letI : UniformSpace (E →SL[σ] F) := strongUniformity σ F 𝔖
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup E'
inst✝⁸ : Module ℝ E'
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : AddCommGroup F'
inst✝⁴ : Module ℝ F'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace E'
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
𝔖 : Set (Set E)
this✝¹ : UniformSpace F := TopologicalAddGroup.toUniformSpace F
this✝ : UniformAddGroup F
this : UniformSpace (E →SL[σ] F) := strongUniformity σ F 𝔖
⊢ TopologicalAddGroup (E →SL[σ] F)
[PROOFSTEP]
haveI : UniformAddGroup (E →SL[σ] F) := strongUniformity.uniformAddGroup σ F 𝔖
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup E'
inst✝⁸ : Module ℝ E'
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : AddCommGroup F'
inst✝⁴ : Module ℝ F'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace E'
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
𝔖 : Set (Set E)
this✝² : UniformSpace F := TopologicalAddGroup.toUniformSpace F
this✝¹ : UniformAddGroup F
this✝ : UniformSpace (E →SL[σ] F) := strongUniformity σ F 𝔖
this : UniformAddGroup (E →SL[σ] F)
⊢ TopologicalAddGroup (E →SL[σ] F)
[PROOFSTEP]
infer_instance
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁴ : NormedField 𝕜₁
inst✝¹³ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜₁ E
inst✝¹⁰ : AddCommGroup E'
inst✝⁹ : Module ℝ E'
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜₂ F
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module ℝ F'
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace E'
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalAddGroup F
inst✝ : T2Space F
𝔖 : Set (Set E)
h𝔖 : ⋃₀ 𝔖 = Set.univ
⊢ T2Space (E →SL[σ] F)
[PROOFSTEP]
letI : UniformSpace F := TopologicalAddGroup.toUniformSpace F
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁴ : NormedField 𝕜₁
inst✝¹³ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜₁ E
inst✝¹⁰ : AddCommGroup E'
inst✝⁹ : Module ℝ E'
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜₂ F
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module ℝ F'
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace E'
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalAddGroup F
inst✝ : T2Space F
𝔖 : Set (Set E)
h𝔖 : ⋃₀ 𝔖 = Set.univ
this : UniformSpace F := TopologicalAddGroup.toUniformSpace F
⊢ T2Space (E →SL[σ] F)
[PROOFSTEP]
haveI : UniformAddGroup F := comm_topologicalAddGroup_is_uniform
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁴ : NormedField 𝕜₁
inst✝¹³ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜₁ E
inst✝¹⁰ : AddCommGroup E'
inst✝⁹ : Module ℝ E'
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜₂ F
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module ℝ F'
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace E'
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalAddGroup F
inst✝ : T2Space F
𝔖 : Set (Set E)
h𝔖 : ⋃₀ 𝔖 = Set.univ
this✝ : UniformSpace F := TopologicalAddGroup.toUniformSpace F
this : UniformAddGroup F
⊢ T2Space (E →SL[σ] F)
[PROOFSTEP]
letI : TopologicalSpace (E →SL[σ] F) := strongTopology σ F 𝔖
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁴ : NormedField 𝕜₁
inst✝¹³ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜₁ E
inst✝¹⁰ : AddCommGroup E'
inst✝⁹ : Module ℝ E'
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜₂ F
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module ℝ F'
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace E'
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalAddGroup F
inst✝ : T2Space F
𝔖 : Set (Set E)
h𝔖 : ⋃₀ 𝔖 = Set.univ
this✝¹ : UniformSpace F := TopologicalAddGroup.toUniformSpace F
this✝ : UniformAddGroup F
this : TopologicalSpace (E →SL[σ] F) := strongTopology σ F 𝔖
⊢ T2Space (E →SL[σ] F)
[PROOFSTEP]
haveI : T2Space (E →ᵤ[𝔖] F) := UniformOnFun.t2Space_of_covering h𝔖
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁴ : NormedField 𝕜₁
inst✝¹³ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜₁ E
inst✝¹⁰ : AddCommGroup E'
inst✝⁹ : Module ℝ E'
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜₂ F
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module ℝ F'
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace E'
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalAddGroup F
inst✝ : T2Space F
𝔖 : Set (Set E)
h𝔖 : ⋃₀ 𝔖 = Set.univ
this✝² : UniformSpace F := TopologicalAddGroup.toUniformSpace F
this✝¹ : UniformAddGroup F
this✝ : TopologicalSpace (E →SL[σ] F) := strongTopology σ F 𝔖
this : T2Space (E →ᵤ[𝔖] F)
⊢ T2Space (E →SL[σ] F)
[PROOFSTEP]
exact (strongTopology.embedding_coeFn σ F 𝔖).t2Space
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁶ : NormedField 𝕜₁
inst✝¹⁵ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜₁ E
inst✝¹² : AddCommGroup E'
inst✝¹¹ : Module ℝ E'
inst✝¹⁰ : AddCommGroup F
inst✝⁹ : Module 𝕜₂ F
inst✝⁸ : AddCommGroup F'
inst✝⁷ : Module ℝ F'
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace E'
inst✝⁴ : RingHomSurjective σ
inst✝³ : RingHomIsometric σ
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜₂ F
𝔖 : Set (Set E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
h𝔖₃ : ∀ (S : Set E), S ∈ 𝔖 → Bornology.IsVonNBounded 𝕜₁ S
⊢ ContinuousSMul 𝕜₂ (E →SL[σ] F)
[PROOFSTEP]
letI : UniformSpace F := TopologicalAddGroup.toUniformSpace F
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁶ : NormedField 𝕜₁
inst✝¹⁵ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜₁ E
inst✝¹² : AddCommGroup E'
inst✝¹¹ : Module ℝ E'
inst✝¹⁰ : AddCommGroup F
inst✝⁹ : Module 𝕜₂ F
inst✝⁸ : AddCommGroup F'
inst✝⁷ : Module ℝ F'
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace E'
inst✝⁴ : RingHomSurjective σ
inst✝³ : RingHomIsometric σ
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜₂ F
𝔖 : Set (Set E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
h𝔖₃ : ∀ (S : Set E), S ∈ 𝔖 → Bornology.IsVonNBounded 𝕜₁ S
this : UniformSpace F := TopologicalAddGroup.toUniformSpace F
⊢ ContinuousSMul 𝕜₂ (E →SL[σ] F)
[PROOFSTEP]
haveI : UniformAddGroup F := comm_topologicalAddGroup_is_uniform
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁶ : NormedField 𝕜₁
inst✝¹⁵ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜₁ E
inst✝¹² : AddCommGroup E'
inst✝¹¹ : Module ℝ E'
inst✝¹⁰ : AddCommGroup F
inst✝⁹ : Module 𝕜₂ F
inst✝⁸ : AddCommGroup F'
inst✝⁷ : Module ℝ F'
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace E'
inst✝⁴ : RingHomSurjective σ
inst✝³ : RingHomIsometric σ
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜₂ F
𝔖 : Set (Set E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
h𝔖₃ : ∀ (S : Set E), S ∈ 𝔖 → Bornology.IsVonNBounded 𝕜₁ S
this✝ : UniformSpace F := TopologicalAddGroup.toUniformSpace F
this : UniformAddGroup F
⊢ ContinuousSMul 𝕜₂ (E →SL[σ] F)
[PROOFSTEP]
letI : TopologicalSpace (E →SL[σ] F) := strongTopology σ F 𝔖
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁶ : NormedField 𝕜₁
inst✝¹⁵ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜₁ E
inst✝¹² : AddCommGroup E'
inst✝¹¹ : Module ℝ E'
inst✝¹⁰ : AddCommGroup F
inst✝⁹ : Module 𝕜₂ F
inst✝⁸ : AddCommGroup F'
inst✝⁷ : Module ℝ F'
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace E'
inst✝⁴ : RingHomSurjective σ
inst✝³ : RingHomIsometric σ
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜₂ F
𝔖 : Set (Set E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
h𝔖₃ : ∀ (S : Set E), S ∈ 𝔖 → Bornology.IsVonNBounded 𝕜₁ S
this✝¹ : UniformSpace F := TopologicalAddGroup.toUniformSpace F
this✝ : UniformAddGroup F
this : TopologicalSpace (E →SL[σ] F) := strongTopology σ F 𝔖
⊢ ContinuousSMul 𝕜₂ (E →SL[σ] F)
[PROOFSTEP]
let φ : (E →SL[σ] F) →ₗ[𝕜₂] E →ᵤ[𝔖] F := ⟨⟨(FunLike.coe : (E →SL[σ] F) → E → F), fun _ _ => rfl⟩, fun _ _ => rfl⟩
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁶ : NormedField 𝕜₁
inst✝¹⁵ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜₁ E
inst✝¹² : AddCommGroup E'
inst✝¹¹ : Module ℝ E'
inst✝¹⁰ : AddCommGroup F
inst✝⁹ : Module 𝕜₂ F
inst✝⁸ : AddCommGroup F'
inst✝⁷ : Module ℝ F'
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace E'
inst✝⁴ : RingHomSurjective σ
inst✝³ : RingHomIsometric σ
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜₂ F
𝔖 : Set (Set E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
h𝔖₃ : ∀ (S : Set E), S ∈ 𝔖 → Bornology.IsVonNBounded 𝕜₁ S
this✝¹ : UniformSpace F := TopologicalAddGroup.toUniformSpace F
this✝ : UniformAddGroup F
this : TopologicalSpace (E →SL[σ] F) := strongTopology σ F 𝔖
φ : (E →SL[σ] F) →ₗ[𝕜₂] E →ᵤ[𝔖] F :=
  { toAddHom := { toFun := FunLike.coe, map_add' := (_ : ∀ (x x_1 : E →SL[σ] F), ↑(x + x_1) = ↑(x + x_1)) },
    map_smul' :=
      (_ :
        ∀ (x : 𝕜₂) (x_1 : E →SL[σ] F),
          AddHom.toFun { toFun := FunLike.coe, map_add' := (_ : ∀ (x x_2 : E →SL[σ] F), ↑(x + x_2) = ↑(x + x_2)) }
              (x • x_1) =
            AddHom.toFun { toFun := FunLike.coe, map_add' := (_ : ∀ (x x_2 : E →SL[σ] F), ↑(x + x_2) = ↑(x + x_2)) }
              (x • x_1)) }
⊢ ContinuousSMul 𝕜₂ (E →SL[σ] F)
[PROOFSTEP]
exact
  UniformOnFun.continuousSMul_induced_of_image_bounded 𝕜₂ E F (E →SL[σ] F) h𝔖₁ h𝔖₂ φ ⟨rfl⟩ fun u s hs =>
    (h𝔖₃ s hs).image u
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup E'
inst✝⁸ : Module ℝ E'
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : AddCommGroup F'
inst✝⁴ : Module ℝ F'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace E'
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
ι : Type u_7
𝔖 : Set (Set E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
p : ι → Prop
b : ι → Set F
h : Filter.HasBasis (𝓝 0) p b
⊢ Filter.HasBasis (𝓝 0) (fun Si => Si.fst ∈ 𝔖 ∧ p Si.snd) fun Si => {f | ∀ (x : E), x ∈ Si.fst → ↑f x ∈ b Si.snd}
[PROOFSTEP]
letI : UniformSpace F := TopologicalAddGroup.toUniformSpace F
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup E'
inst✝⁸ : Module ℝ E'
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : AddCommGroup F'
inst✝⁴ : Module ℝ F'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace E'
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
ι : Type u_7
𝔖 : Set (Set E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
p : ι → Prop
b : ι → Set F
h : Filter.HasBasis (𝓝 0) p b
this : UniformSpace F := TopologicalAddGroup.toUniformSpace F
⊢ Filter.HasBasis (𝓝 0) (fun Si => Si.fst ∈ 𝔖 ∧ p Si.snd) fun Si => {f | ∀ (x : E), x ∈ Si.fst → ↑f x ∈ b Si.snd}
[PROOFSTEP]
haveI : UniformAddGroup F := comm_topologicalAddGroup_is_uniform
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup E'
inst✝⁸ : Module ℝ E'
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : AddCommGroup F'
inst✝⁴ : Module ℝ F'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace E'
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
ι : Type u_7
𝔖 : Set (Set E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
p : ι → Prop
b : ι → Set F
h : Filter.HasBasis (𝓝 0) p b
this✝ : UniformSpace F := TopologicalAddGroup.toUniformSpace F
this : UniformAddGroup F
⊢ Filter.HasBasis (𝓝 0) (fun Si => Si.fst ∈ 𝔖 ∧ p Si.snd) fun Si => {f | ∀ (x : E), x ∈ Si.fst → ↑f x ∈ b Si.snd}
[PROOFSTEP]
letI : TopologicalSpace (E →SL[σ] F) := strongTopology σ F 𝔖
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup E'
inst✝⁸ : Module ℝ E'
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : AddCommGroup F'
inst✝⁴ : Module ℝ F'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace E'
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
ι : Type u_7
𝔖 : Set (Set E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
p : ι → Prop
b : ι → Set F
h : Filter.HasBasis (𝓝 0) p b
this✝¹ : UniformSpace F := TopologicalAddGroup.toUniformSpace F
this✝ : UniformAddGroup F
this : TopologicalSpace (E →SL[σ] F) := strongTopology σ F 𝔖
⊢ Filter.HasBasis (𝓝 0) (fun Si => Si.fst ∈ 𝔖 ∧ p Si.snd) fun Si => {f | ∀ (x : E), x ∈ Si.fst → ↑f x ∈ b Si.snd}
[PROOFSTEP]
rw [(strongTopology.embedding_coeFn σ F 𝔖).toInducing.nhds_eq_comap]
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup E'
inst✝⁸ : Module ℝ E'
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : AddCommGroup F'
inst✝⁴ : Module ℝ F'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace E'
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
ι : Type u_7
𝔖 : Set (Set E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
p : ι → Prop
b : ι → Set F
h : Filter.HasBasis (𝓝 0) p b
this✝¹ : UniformSpace F := TopologicalAddGroup.toUniformSpace F
this✝ : UniformAddGroup F
this : TopologicalSpace (E →SL[σ] F) := strongTopology σ F 𝔖
⊢ Filter.HasBasis (Filter.comap (↑(UniformOnFun.ofFun 𝔖) ∘ FunLike.coe) (𝓝 ((↑(UniformOnFun.ofFun 𝔖) ∘ FunLike.coe) 0)))
    (fun Si => Si.fst ∈ 𝔖 ∧ p Si.snd) fun Si => {f | ∀ (x : E), x ∈ Si.fst → ↑f x ∈ b Si.snd}
[PROOFSTEP]
exact (UniformOnFun.hasBasis_nhds_zero_of_basis 𝔖 h𝔖₁ h𝔖₂ h).comap FunLike.coe
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst✝²⁰ : NormedField 𝕜₁
inst✝¹⁹ : NormedField 𝕜₂
inst✝¹⁸ : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst✝¹⁷ : RingHomCompTriple σ τ ρ
E : Type u_4
E' : Type u_5
F : Type u_6
F' : Type u_7
G : Type u_8
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜₁ E
inst✝¹⁴ : AddCommGroup E'
inst✝¹³ : Module ℝ E'
inst✝¹² : AddCommGroup F
inst✝¹¹ : Module 𝕜₂ F
inst✝¹⁰ : AddCommGroup F'
inst✝⁹ : Module ℝ F'
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜₃ G
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalAddGroup G
inst✝² : ContinuousConstSMul 𝕜₃ G
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
L : E →SL[σ] F
⊢ Continuous
    {
          toAddHom :=
            { toFun := fun f => comp f L,
              map_add' := (_ : ∀ (f g : F →SL[τ] G), comp (f + g) L = comp f L + comp g L) },
          map_smul' := (_ : ∀ (a : 𝕜₃) (f : F →SL[τ] G), comp (a • f) L = a • comp f L) }.toAddHom.toFun
[PROOFSTEP]
letI : UniformSpace G := TopologicalAddGroup.toUniformSpace G
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst✝²⁰ : NormedField 𝕜₁
inst✝¹⁹ : NormedField 𝕜₂
inst✝¹⁸ : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst✝¹⁷ : RingHomCompTriple σ τ ρ
E : Type u_4
E' : Type u_5
F : Type u_6
F' : Type u_7
G : Type u_8
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜₁ E
inst✝¹⁴ : AddCommGroup E'
inst✝¹³ : Module ℝ E'
inst✝¹² : AddCommGroup F
inst✝¹¹ : Module 𝕜₂ F
inst✝¹⁰ : AddCommGroup F'
inst✝⁹ : Module ℝ F'
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜₃ G
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalAddGroup G
inst✝² : ContinuousConstSMul 𝕜₃ G
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
L : E →SL[σ] F
this : UniformSpace G := TopologicalAddGroup.toUniformSpace G
⊢ Continuous
    {
          toAddHom :=
            { toFun := fun f => comp f L,
              map_add' := (_ : ∀ (f g : F →SL[τ] G), comp (f + g) L = comp f L + comp g L) },
          map_smul' := (_ : ∀ (a : 𝕜₃) (f : F →SL[τ] G), comp (a • f) L = a • comp f L) }.toAddHom.toFun
[PROOFSTEP]
haveI : UniformAddGroup G := comm_topologicalAddGroup_is_uniform
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst✝²⁰ : NormedField 𝕜₁
inst✝¹⁹ : NormedField 𝕜₂
inst✝¹⁸ : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst✝¹⁷ : RingHomCompTriple σ τ ρ
E : Type u_4
E' : Type u_5
F : Type u_6
F' : Type u_7
G : Type u_8
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜₁ E
inst✝¹⁴ : AddCommGroup E'
inst✝¹³ : Module ℝ E'
inst✝¹² : AddCommGroup F
inst✝¹¹ : Module 𝕜₂ F
inst✝¹⁰ : AddCommGroup F'
inst✝⁹ : Module ℝ F'
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜₃ G
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalAddGroup G
inst✝² : ContinuousConstSMul 𝕜₃ G
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
L : E →SL[σ] F
this✝ : UniformSpace G := TopologicalAddGroup.toUniformSpace G
this : UniformAddGroup G
⊢ Continuous
    {
          toAddHom :=
            { toFun := fun f => comp f L,
              map_add' := (_ : ∀ (f g : F →SL[τ] G), comp (f + g) L = comp f L + comp g L) },
          map_smul' := (_ : ∀ (a : 𝕜₃) (f : F →SL[τ] G), comp (a • f) L = a • comp f L) }.toAddHom.toFun
[PROOFSTEP]
rw [(strongTopology.embedding_coeFn _ _ _).continuous_iff]
  -- Porting note: without this, the following doesn't work
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst✝²⁰ : NormedField 𝕜₁
inst✝¹⁹ : NormedField 𝕜₂
inst✝¹⁸ : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst✝¹⁷ : RingHomCompTriple σ τ ρ
E : Type u_4
E' : Type u_5
F : Type u_6
F' : Type u_7
G : Type u_8
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜₁ E
inst✝¹⁴ : AddCommGroup E'
inst✝¹³ : Module ℝ E'
inst✝¹² : AddCommGroup F
inst✝¹¹ : Module 𝕜₂ F
inst✝¹⁰ : AddCommGroup F'
inst✝⁹ : Module ℝ F'
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜₃ G
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalAddGroup G
inst✝² : ContinuousConstSMul 𝕜₃ G
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
L : E →SL[σ] F
this✝ : UniformSpace G := TopologicalAddGroup.toUniformSpace G
this : UniformAddGroup G
⊢ Continuous
    ((↑(UniformOnFun.ofFun {S | Bornology.IsVonNBounded 𝕜₁ S}) ∘ FunLike.coe) ∘
      {
            toAddHom :=
              { toFun := fun f => comp f L,
                map_add' := (_ : ∀ (f g : F →SL[τ] G), comp (f + g) L = comp f L + comp g L) },
            map_smul' := (_ : ∀ (a : 𝕜₃) (f : F →SL[τ] G), comp (a • f) L = a • comp f L) }.toAddHom.toFun)
[PROOFSTEP]
change Continuous ((λ f ↦ UniformOnFun.ofFun _ (f ∘ L)) ∘ FunLike.coe)
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst✝²⁰ : NormedField 𝕜₁
inst✝¹⁹ : NormedField 𝕜₂
inst✝¹⁸ : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst✝¹⁷ : RingHomCompTriple σ τ ρ
E : Type u_4
E' : Type u_5
F : Type u_6
F' : Type u_7
G : Type u_8
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜₁ E
inst✝¹⁴ : AddCommGroup E'
inst✝¹³ : Module ℝ E'
inst✝¹² : AddCommGroup F
inst✝¹¹ : Module 𝕜₂ F
inst✝¹⁰ : AddCommGroup F'
inst✝⁹ : Module ℝ F'
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜₃ G
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalAddGroup G
inst✝² : ContinuousConstSMul 𝕜₃ G
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
L : E →SL[σ] F
this✝ : UniformSpace G := TopologicalAddGroup.toUniformSpace G
this : UniformAddGroup G
⊢ Continuous ((fun f => ↑(UniformOnFun.ofFun {S | Bornology.IsVonNBounded 𝕜₁ S}) (f ∘ ↑L)) ∘ FunLike.coe)
[PROOFSTEP]
exact
  (UniformOnFun.precomp_uniformContinuous fun S hS => hS.image L).continuous.comp
    (strongTopology.embedding_coeFn _ _ _).continuous
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst✝²⁰ : NormedField 𝕜₁
inst✝¹⁹ : NormedField 𝕜₂
inst✝¹⁸ : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst✝¹⁷ : RingHomCompTriple σ τ ρ
E : Type u_4
E' : Type u_5
F : Type u_6
F' : Type u_7
G : Type u_8
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜₁ E
inst✝¹⁴ : AddCommGroup E'
inst✝¹³ : Module ℝ E'
inst✝¹² : AddCommGroup F
inst✝¹¹ : Module 𝕜₂ F
inst✝¹⁰ : AddCommGroup F'
inst✝⁹ : Module ℝ F'
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜₃ G
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalAddGroup F
inst✝² : TopologicalAddGroup G
inst✝¹ : ContinuousConstSMul 𝕜₃ G
inst✝ : ContinuousConstSMul 𝕜₂ F
L : F →SL[τ] G
⊢ Continuous
    {
          toAddHom :=
            { toFun := fun f => comp L f,
              map_add' := (_ : ∀ (f₁ f₂ : E →SL[σ] F), comp L (f₁ + f₂) = comp L f₁ + comp L f₂) },
          map_smul' := (_ : ∀ (c : 𝕜₂) (f : E →SL[σ] F), comp L (c • f) = ↑τ c • comp L f) }.toAddHom.toFun
[PROOFSTEP]
letI : UniformSpace G := TopologicalAddGroup.toUniformSpace G
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst✝²⁰ : NormedField 𝕜₁
inst✝¹⁹ : NormedField 𝕜₂
inst✝¹⁸ : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst✝¹⁷ : RingHomCompTriple σ τ ρ
E : Type u_4
E' : Type u_5
F : Type u_6
F' : Type u_7
G : Type u_8
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜₁ E
inst✝¹⁴ : AddCommGroup E'
inst✝¹³ : Module ℝ E'
inst✝¹² : AddCommGroup F
inst✝¹¹ : Module 𝕜₂ F
inst✝¹⁰ : AddCommGroup F'
inst✝⁹ : Module ℝ F'
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜₃ G
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalAddGroup F
inst✝² : TopologicalAddGroup G
inst✝¹ : ContinuousConstSMul 𝕜₃ G
inst✝ : ContinuousConstSMul 𝕜₂ F
L : F →SL[τ] G
this : UniformSpace G := TopologicalAddGroup.toUniformSpace G
⊢ Continuous
    {
          toAddHom :=
            { toFun := fun f => comp L f,
              map_add' := (_ : ∀ (f₁ f₂ : E →SL[σ] F), comp L (f₁ + f₂) = comp L f₁ + comp L f₂) },
          map_smul' := (_ : ∀ (c : 𝕜₂) (f : E →SL[σ] F), comp L (c • f) = ↑τ c • comp L f) }.toAddHom.toFun
[PROOFSTEP]
haveI : UniformAddGroup G := comm_topologicalAddGroup_is_uniform
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst✝²⁰ : NormedField 𝕜₁
inst✝¹⁹ : NormedField 𝕜₂
inst✝¹⁸ : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst✝¹⁷ : RingHomCompTriple σ τ ρ
E : Type u_4
E' : Type u_5
F : Type u_6
F' : Type u_7
G : Type u_8
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜₁ E
inst✝¹⁴ : AddCommGroup E'
inst✝¹³ : Module ℝ E'
inst✝¹² : AddCommGroup F
inst✝¹¹ : Module 𝕜₂ F
inst✝¹⁰ : AddCommGroup F'
inst✝⁹ : Module ℝ F'
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜₃ G
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalAddGroup F
inst✝² : TopologicalAddGroup G
inst✝¹ : ContinuousConstSMul 𝕜₃ G
inst✝ : ContinuousConstSMul 𝕜₂ F
L : F →SL[τ] G
this✝ : UniformSpace G := TopologicalAddGroup.toUniformSpace G
this : UniformAddGroup G
⊢ Continuous
    {
          toAddHom :=
            { toFun := fun f => comp L f,
              map_add' := (_ : ∀ (f₁ f₂ : E →SL[σ] F), comp L (f₁ + f₂) = comp L f₁ + comp L f₂) },
          map_smul' := (_ : ∀ (c : 𝕜₂) (f : E →SL[σ] F), comp L (c • f) = ↑τ c • comp L f) }.toAddHom.toFun
[PROOFSTEP]
letI : UniformSpace F := TopologicalAddGroup.toUniformSpace F
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst✝²⁰ : NormedField 𝕜₁
inst✝¹⁹ : NormedField 𝕜₂
inst✝¹⁸ : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst✝¹⁷ : RingHomCompTriple σ τ ρ
E : Type u_4
E' : Type u_5
F : Type u_6
F' : Type u_7
G : Type u_8
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜₁ E
inst✝¹⁴ : AddCommGroup E'
inst✝¹³ : Module ℝ E'
inst✝¹² : AddCommGroup F
inst✝¹¹ : Module 𝕜₂ F
inst✝¹⁰ : AddCommGroup F'
inst✝⁹ : Module ℝ F'
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜₃ G
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalAddGroup F
inst✝² : TopologicalAddGroup G
inst✝¹ : ContinuousConstSMul 𝕜₃ G
inst✝ : ContinuousConstSMul 𝕜₂ F
L : F →SL[τ] G
this✝¹ : UniformSpace G := TopologicalAddGroup.toUniformSpace G
this✝ : UniformAddGroup G
this : UniformSpace F := TopologicalAddGroup.toUniformSpace F
⊢ Continuous
    {
          toAddHom :=
            { toFun := fun f => comp L f,
              map_add' := (_ : ∀ (f₁ f₂ : E →SL[σ] F), comp L (f₁ + f₂) = comp L f₁ + comp L f₂) },
          map_smul' := (_ : ∀ (c : 𝕜₂) (f : E →SL[σ] F), comp L (c • f) = ↑τ c • comp L f) }.toAddHom.toFun
[PROOFSTEP]
haveI : UniformAddGroup F := comm_topologicalAddGroup_is_uniform
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst✝²⁰ : NormedField 𝕜₁
inst✝¹⁹ : NormedField 𝕜₂
inst✝¹⁸ : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst✝¹⁷ : RingHomCompTriple σ τ ρ
E : Type u_4
E' : Type u_5
F : Type u_6
F' : Type u_7
G : Type u_8
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜₁ E
inst✝¹⁴ : AddCommGroup E'
inst✝¹³ : Module ℝ E'
inst✝¹² : AddCommGroup F
inst✝¹¹ : Module 𝕜₂ F
inst✝¹⁰ : AddCommGroup F'
inst✝⁹ : Module ℝ F'
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜₃ G
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalAddGroup F
inst✝² : TopologicalAddGroup G
inst✝¹ : ContinuousConstSMul 𝕜₃ G
inst✝ : ContinuousConstSMul 𝕜₂ F
L : F →SL[τ] G
this✝² : UniformSpace G := TopologicalAddGroup.toUniformSpace G
this✝¹ : UniformAddGroup G
this✝ : UniformSpace F := TopologicalAddGroup.toUniformSpace F
this : UniformAddGroup F
⊢ Continuous
    {
          toAddHom :=
            { toFun := fun f => comp L f,
              map_add' := (_ : ∀ (f₁ f₂ : E →SL[σ] F), comp L (f₁ + f₂) = comp L f₁ + comp L f₂) },
          map_smul' := (_ : ∀ (c : 𝕜₂) (f : E →SL[σ] F), comp L (c • f) = ↑τ c • comp L f) }.toAddHom.toFun
[PROOFSTEP]
rw [(strongTopology.embedding_coeFn _ _ _).continuous_iff]
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst✝²⁰ : NormedField 𝕜₁
inst✝¹⁹ : NormedField 𝕜₂
inst✝¹⁸ : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst✝¹⁷ : RingHomCompTriple σ τ ρ
E : Type u_4
E' : Type u_5
F : Type u_6
F' : Type u_7
G : Type u_8
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜₁ E
inst✝¹⁴ : AddCommGroup E'
inst✝¹³ : Module ℝ E'
inst✝¹² : AddCommGroup F
inst✝¹¹ : Module 𝕜₂ F
inst✝¹⁰ : AddCommGroup F'
inst✝⁹ : Module ℝ F'
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜₃ G
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalAddGroup F
inst✝² : TopologicalAddGroup G
inst✝¹ : ContinuousConstSMul 𝕜₃ G
inst✝ : ContinuousConstSMul 𝕜₂ F
L : F →SL[τ] G
this✝² : UniformSpace G := TopologicalAddGroup.toUniformSpace G
this✝¹ : UniformAddGroup G
this✝ : UniformSpace F := TopologicalAddGroup.toUniformSpace F
this : UniformAddGroup F
⊢ Continuous
    ((↑(UniformOnFun.ofFun {S | Bornology.IsVonNBounded 𝕜₁ S}) ∘ FunLike.coe) ∘
      {
            toAddHom :=
              { toFun := fun f => comp L f,
                map_add' := (_ : ∀ (f₁ f₂ : E →SL[σ] F), comp L (f₁ + f₂) = comp L f₁ + comp L f₂) },
            map_smul' := (_ : ∀ (c : 𝕜₂) (f : E →SL[σ] F), comp L (c • f) = ↑τ c • comp L f) }.toAddHom.toFun)
[PROOFSTEP]
exact
  (UniformOnFun.postcomp_uniformContinuous L.uniformContinuous).continuous.comp
    (strongTopology.embedding_coeFn _ _ _).continuous
[GOAL]
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
𝕜₄ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
inst✝³¹ : AddCommGroup E
inst✝³⁰ : AddCommGroup F
inst✝²⁹ : AddCommGroup G
inst✝²⁸ : AddCommGroup H
inst✝²⁷ : NontriviallyNormedField 𝕜
inst✝²⁶ : NontriviallyNormedField 𝕜₂
inst✝²⁵ : NontriviallyNormedField 𝕜₃
inst✝²⁴ : NontriviallyNormedField 𝕜₄
inst✝²³ : Module 𝕜 E
inst✝²² : Module 𝕜₂ F
inst✝²¹ : Module 𝕜₃ G
inst✝²⁰ : Module 𝕜₄ H
inst✝¹⁹ : TopologicalSpace E
inst✝¹⁸ : TopologicalSpace F
inst✝¹⁷ : TopologicalSpace G
inst✝¹⁶ : TopologicalSpace H
inst✝¹⁵ : TopologicalAddGroup G
inst✝¹⁴ : TopologicalAddGroup H
inst✝¹³ : ContinuousConstSMul 𝕜₃ G
inst✝¹² : ContinuousConstSMul 𝕜₄ H
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
σ₃₄ : 𝕜₃ →+* 𝕜₄
σ₄₃ : 𝕜₄ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₁₄ : 𝕜 →+* 𝕜₄
inst✝¹¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹⁰ : RingHomInvPair σ₂₁ σ₁₂
inst✝⁹ : RingHomInvPair σ₃₄ σ₄₃
inst✝⁸ : RingHomInvPair σ₄₃ σ₃₄
inst✝⁷ : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄
inst✝⁶ : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃
inst✝⁵ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝⁴ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝³ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝² : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₁
e₁₂ : E ≃SL[σ₁₂] F
e₄₃ : H ≃SL[σ₄₃] G
src✝ : (E →SL[σ₁₄] H) ≃ (F →SL[σ₂₃] G) := arrowCongrEquiv e₁₂ e₄₃
f g : E →SL[σ₁₄] H
⊢ (fun L => comp (↑e₄₃) (comp L ↑(ContinuousLinearEquiv.symm e₁₂))) (f + g) =
    (fun L => comp (↑e₄₃) (comp L ↑(ContinuousLinearEquiv.symm e₁₂))) f +
      (fun L => comp (↑e₄₃) (comp L ↑(ContinuousLinearEquiv.symm e₁₂))) g
[PROOFSTEP]
simp only [add_comp, comp_add]
[GOAL]
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
𝕜₄ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
inst✝³¹ : AddCommGroup E
inst✝³⁰ : AddCommGroup F
inst✝²⁹ : AddCommGroup G
inst✝²⁸ : AddCommGroup H
inst✝²⁷ : NontriviallyNormedField 𝕜
inst✝²⁶ : NontriviallyNormedField 𝕜₂
inst✝²⁵ : NontriviallyNormedField 𝕜₃
inst✝²⁴ : NontriviallyNormedField 𝕜₄
inst✝²³ : Module 𝕜 E
inst✝²² : Module 𝕜₂ F
inst✝²¹ : Module 𝕜₃ G
inst✝²⁰ : Module 𝕜₄ H
inst✝¹⁹ : TopologicalSpace E
inst✝¹⁸ : TopologicalSpace F
inst✝¹⁷ : TopologicalSpace G
inst✝¹⁶ : TopologicalSpace H
inst✝¹⁵ : TopologicalAddGroup G
inst✝¹⁴ : TopologicalAddGroup H
inst✝¹³ : ContinuousConstSMul 𝕜₃ G
inst✝¹² : ContinuousConstSMul 𝕜₄ H
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
σ₃₄ : 𝕜₃ →+* 𝕜₄
σ₄₃ : 𝕜₄ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₁₄ : 𝕜 →+* 𝕜₄
inst✝¹¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹⁰ : RingHomInvPair σ₂₁ σ₁₂
inst✝⁹ : RingHomInvPair σ₃₄ σ₄₃
inst✝⁸ : RingHomInvPair σ₄₃ σ₃₄
inst✝⁷ : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄
inst✝⁶ : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃
inst✝⁵ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝⁴ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝³ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝² : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₁
e₁₂ : E ≃SL[σ₁₂] F
e₄₃ : H ≃SL[σ₄₃] G
src✝ : (E →SL[σ₁₄] H) ≃ (F →SL[σ₂₃] G) := arrowCongrEquiv e₁₂ e₄₃
t : 𝕜₄
f : E →SL[σ₁₄] H
⊢ AddHom.toFun
      { toFun := fun L => comp (↑e₄₃) (comp L ↑(ContinuousLinearEquiv.symm e₁₂)),
        map_add' :=
          (_ :
            ∀ (f g : E →SL[σ₁₄] H),
              comp (↑e₄₃) (comp (f + g) ↑(ContinuousLinearEquiv.symm e₁₂)) =
                comp (↑e₄₃) (comp f ↑(ContinuousLinearEquiv.symm e₁₂)) +
                  comp (↑e₄₃) (comp g ↑(ContinuousLinearEquiv.symm e₁₂))) }
      (t • f) =
    ↑σ₄₃ t •
      AddHom.toFun
        { toFun := fun L => comp (↑e₄₃) (comp L ↑(ContinuousLinearEquiv.symm e₁₂)),
          map_add' :=
            (_ :
              ∀ (f g : E →SL[σ₁₄] H),
                comp (↑e₄₃) (comp (f + g) ↑(ContinuousLinearEquiv.symm e₁₂)) =
                  comp (↑e₄₃) (comp f ↑(ContinuousLinearEquiv.symm e₁₂)) +
                    comp (↑e₄₃) (comp g ↑(ContinuousLinearEquiv.symm e₁₂))) }
        f
[PROOFSTEP]
simp only [smul_comp, comp_smulₛₗ]


[GOAL]
X : TopCat
F : Presheaf (Type v) X
U U' : (Opens ↑X)ᵒᵖ
f : U ⟶ U'
⊢ F.map f ≫
      (fun U f =>
          { val := fun x => germ F x f,
            property :=
              (_ :
                PrelocalPredicate.pred (PrelocalPredicate.sheafify (Sheafify.isGerm F)).toPrelocalPredicate fun x =>
                  germ F x f) })
        U' =
    (fun U f =>
          { val := fun x => germ F x f,
            property :=
              (_ :
                PrelocalPredicate.pred (PrelocalPredicate.sheafify (Sheafify.isGerm F)).toPrelocalPredicate fun x =>
                  germ F x f) })
        U ≫
      (sheafify F).val.map f
[PROOFSTEP]
ext x
[GOAL]
case h
X : TopCat
F : Presheaf (Type v) X
U U' : (Opens ↑X)ᵒᵖ
f : U ⟶ U'
x : F.obj U
⊢ (F.map f ≫
        (fun U f =>
            { val := fun x => germ F x f,
              property :=
                (_ :
                  PrelocalPredicate.pred (PrelocalPredicate.sheafify (Sheafify.isGerm F)).toPrelocalPredicate fun x =>
                    germ F x f) })
          U')
      x =
    ((fun U f =>
            { val := fun x => germ F x f,
              property :=
                (_ :
                  PrelocalPredicate.pred (PrelocalPredicate.sheafify (Sheafify.isGerm F)).toPrelocalPredicate fun x =>
                    germ F x f) })
          U ≫
        (sheafify F).val.map f)
      x
[PROOFSTEP]
apply Subtype.ext
[GOAL]
case h.a
X : TopCat
F : Presheaf (Type v) X
U U' : (Opens ↑X)ᵒᵖ
f : U ⟶ U'
x : F.obj U
⊢ ↑((F.map f ≫
          (fun U f =>
              { val := fun x => germ F x f,
                property :=
                  (_ :
                    PrelocalPredicate.pred (PrelocalPredicate.sheafify (Sheafify.isGerm F)).toPrelocalPredicate fun x =>
                      germ F x f) })
            U')
        x) =
    ↑(((fun U f =>
              { val := fun x => germ F x f,
                property :=
                  (_ :
                    PrelocalPredicate.pred (PrelocalPredicate.sheafify (Sheafify.isGerm F)).toPrelocalPredicate fun x =>
                      germ F x f) })
            U ≫
          (sheafify F).val.map f)
        x)
[PROOFSTEP]
ext ⟨u, m⟩
[GOAL]
case h.a.h.mk
X : TopCat
F : Presheaf (Type v) X
U U' : (Opens ↑X)ᵒᵖ
f : U ⟶ U'
x : F.obj U
u : ↑X
m : u ∈ U'.unop
⊢ ↑((F.map f ≫
            (fun U f =>
                { val := fun x => germ F x f,
                  property :=
                    (_ :
                      PrelocalPredicate.pred (PrelocalPredicate.sheafify (Sheafify.isGerm F)).toPrelocalPredicate
                        fun x => germ F x f) })
              U')
          x)
      { val := u, property := m } =
    ↑(((fun U f =>
                { val := fun x => germ F x f,
                  property :=
                    (_ :
                      PrelocalPredicate.pred (PrelocalPredicate.sheafify (Sheafify.isGerm F)).toPrelocalPredicate
                        fun x => germ F x f) })
              U ≫
            (sheafify F).val.map f)
          x)
      { val := u, property := m }
[PROOFSTEP]
exact germ_res_apply F f.unop ⟨u, m⟩ x
[GOAL]
X : TopCat
F : Presheaf (Type v) X
x : ↑X
⊢ Function.Surjective (stalkToFiber F x)
[PROOFSTEP]
apply TopCat.stalkToFiber_surjective
[GOAL]
case w
X : TopCat
F : Presheaf (Type v) X
x : ↑X
⊢ ∀ (t : stalk F x), ∃ U f x_1, f { val := x, property := (_ : x ∈ U.obj) } = t
[PROOFSTEP]
intro t
[GOAL]
case w
X : TopCat
F : Presheaf (Type v) X
x : ↑X
t : stalk F x
⊢ ∃ U f x_1, f { val := x, property := (_ : x ∈ U.obj) } = t
[PROOFSTEP]
obtain ⟨U, m, s, rfl⟩ := F.germ_exist _ t
[GOAL]
case w.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U : Opens ↑X
m : x ∈ U
s : (forget (Type v)).obj (F.obj (op U))
⊢ ∃ U_1 f x_1, f { val := x, property := (_ : x ∈ U_1.obj) } = ↑(germ F { val := x, property := m }) s
[PROOFSTEP]
use⟨U, m⟩
[GOAL]
case h
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U : Opens ↑X
m : x ∈ U
s : (forget (Type v)).obj (F.obj (op U))
⊢ ∃ f x_1,
    f { val := x, property := (_ : x ∈ { obj := U, property := m }.obj) } = ↑(germ F { val := x, property := m }) s
[PROOFSTEP]
fconstructor
[GOAL]
case h.w
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U : Opens ↑X
m : x ∈ U
s : (forget (Type v)).obj (F.obj (op U))
⊢ (y : { x_1 // x_1 ∈ { obj := U, property := m }.obj }) → stalk F ↑y
[PROOFSTEP]
exact fun y => F.germ y s
[GOAL]
case h.h
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U : Opens ↑X
m : x ∈ U
s : (forget (Type v)).obj (F.obj (op U))
⊢ ∃ x_1,
    germ F { val := x, property := (_ : x ∈ { obj := U, property := m }.obj) } s =
      ↑(germ F { val := x, property := m }) s
[PROOFSTEP]
exact ⟨PrelocalPredicate.sheafifyOf ⟨s, fun _ => rfl⟩, rfl⟩
[GOAL]
X : TopCat
F : Presheaf (Type v) X
x : ↑X
⊢ Function.Injective (stalkToFiber F x)
[PROOFSTEP]
apply TopCat.stalkToFiber_injective
[GOAL]
case w
X : TopCat
F : Presheaf (Type v) X
x : ↑X
⊢ ∀ (U V : OpenNhds x) (fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y),
    PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU →
      ∀ (fV : (y : { x_2 // x_2 ∈ V.obj }) → stalk F ↑y),
        PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV →
          fU { val := x, property := (_ : x ∈ U.obj) } = fV { val := x, property := (_ : x ∈ V.obj) } →
            ∃ W iU iV,
              ∀ (w : { x_4 // x_4 ∈ W.obj }),
                fU ((fun x_4 => { val := ↑x_4, property := (_ : ↑x_4 ∈ ↑U.obj) }) w) =
                  fV ((fun x_4 => { val := ↑x_4, property := (_ : ↑x_4 ∈ ↑V.obj) }) w)
[PROOFSTEP]
intro U V fU hU fV hV e
[GOAL]
case w
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
e : fU { val := x, property := (_ : x ∈ U.obj) } = fV { val := x, property := (_ : x ∈ V.obj) }
⊢ ∃ W iU iV,
    ∀ (w : { x_1 // x_1 ∈ W.obj }),
      fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.obj) }) w) =
        fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.obj) }) w)
[PROOFSTEP]
rcases hU ⟨x, U.2⟩ with ⟨U', mU, iU, gU, wU⟩
[GOAL]
case w.intro.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
e : fU { val := x, property := (_ : x ∈ U.obj) } = fV { val := x, property := (_ : x ∈ V.obj) }
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
⊢ ∃ W iU iV,
    ∀ (w : { x_1 // x_1 ∈ W.obj }),
      fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.obj) }) w) =
        fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.obj) }) w)
[PROOFSTEP]
rcases hV ⟨x, V.2⟩ with ⟨V', mV, iV, gV, wV⟩
[GOAL]
case w.intro.intro.intro.intro.intro.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
e : fU { val := x, property := (_ : x ∈ U.obj) } = fV { val := x, property := (_ : x ∈ V.obj) }
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
⊢ ∃ W iU iV,
    ∀ (w : { x_1 // x_1 ∈ W.obj }),
      fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.obj) }) w) =
        fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.obj) }) w)
[PROOFSTEP]
have wUx := wU ⟨x, mU⟩
[GOAL]
case w.intro.intro.intro.intro.intro.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
e : fU { val := x, property := (_ : x ∈ U.obj) } = fV { val := x, property := (_ : x ∈ V.obj) }
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
wUx :
  (fun x_1 => fU ((fun x_2 => { val := ↑x_2, property := (_ : ↑x_2 ∈ ↑U.obj) }) x_1)) { val := x, property := mU } =
    germ F { val := x, property := mU } gU
⊢ ∃ W iU iV,
    ∀ (w : { x_1 // x_1 ∈ W.obj }),
      fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.obj) }) w) =
        fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.obj) }) w)
[PROOFSTEP]
dsimp at wUx
[GOAL]
case w.intro.intro.intro.intro.intro.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
e : fU { val := x, property := (_ : x ∈ U.obj) } = fV { val := x, property := (_ : x ∈ V.obj) }
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
wUx : fU { val := x, property := (_ : ↑{ val := x, property := mU } ∈ ↑U.obj) } = germ F { val := x, property := mU } gU
⊢ ∃ W iU iV,
    ∀ (w : { x_1 // x_1 ∈ W.obj }),
      fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.obj) }) w) =
        fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.obj) }) w)
[PROOFSTEP]
erw [wUx] at e
[GOAL]
case w.intro.intro.intro.intro.intro.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
e : germ F { val := x, property := mU } gU = fV { val := x, property := (_ : x ∈ V.obj) }
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
wUx : fU { val := x, property := (_ : ↑{ val := x, property := mU } ∈ ↑U.obj) } = germ F { val := x, property := mU } gU
⊢ ∃ W iU iV,
    ∀ (w : { x_1 // x_1 ∈ W.obj }),
      fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.obj) }) w) =
        fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.obj) }) w)
[PROOFSTEP]
clear wUx
[GOAL]
case w.intro.intro.intro.intro.intro.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
e : germ F { val := x, property := mU } gU = fV { val := x, property := (_ : x ∈ V.obj) }
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
⊢ ∃ W iU iV,
    ∀ (w : { x_1 // x_1 ∈ W.obj }),
      fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.obj) }) w) =
        fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.obj) }) w)
[PROOFSTEP]
have wVx := wV ⟨x, mV⟩
[GOAL]
case w.intro.intro.intro.intro.intro.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
e : germ F { val := x, property := mU } gU = fV { val := x, property := (_ : x ∈ V.obj) }
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
wVx :
  (fun x_1 => fV ((fun x_2 => { val := ↑x_2, property := (_ : ↑x_2 ∈ ↑V.obj) }) x_1)) { val := x, property := mV } =
    germ F { val := x, property := mV } gV
⊢ ∃ W iU iV,
    ∀ (w : { x_1 // x_1 ∈ W.obj }),
      fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.obj) }) w) =
        fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.obj) }) w)
[PROOFSTEP]
dsimp at wVx
[GOAL]
case w.intro.intro.intro.intro.intro.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
e : germ F { val := x, property := mU } gU = fV { val := x, property := (_ : x ∈ V.obj) }
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
wVx : fV { val := x, property := (_ : ↑{ val := x, property := mV } ∈ ↑V.obj) } = germ F { val := x, property := mV } gV
⊢ ∃ W iU iV,
    ∀ (w : { x_1 // x_1 ∈ W.obj }),
      fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.obj) }) w) =
        fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.obj) }) w)
[PROOFSTEP]
erw [wVx] at e
[GOAL]
case w.intro.intro.intro.intro.intro.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
e : germ F { val := x, property := mU } gU = germ F { val := x, property := mV } gV
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
wVx : fV { val := x, property := (_ : ↑{ val := x, property := mV } ∈ ↑V.obj) } = germ F { val := x, property := mV } gV
⊢ ∃ W iU iV,
    ∀ (w : { x_1 // x_1 ∈ W.obj }),
      fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.obj) }) w) =
        fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.obj) }) w)
[PROOFSTEP]
clear wVx
[GOAL]
case w.intro.intro.intro.intro.intro.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
e : germ F { val := x, property := mU } gU = germ F { val := x, property := mV } gV
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
⊢ ∃ W iU iV,
    ∀ (w : { x_1 // x_1 ∈ W.obj }),
      fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.obj) }) w) =
        fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.obj) }) w)
[PROOFSTEP]
rcases F.germ_eq x mU mV gU gV e with ⟨W, mW, iU', iV', (e' : F.map iU'.op gU = F.map iV'.op gV)⟩
[GOAL]
case w.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
e : germ F { val := x, property := mU } gU = germ F { val := x, property := mV } gV
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : F.map iU'.op gU = F.map iV'.op gV
⊢ ∃ W iU iV,
    ∀ (w : { x_1 // x_1 ∈ W.obj }),
      fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.obj) }) w) =
        fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.obj) }) w)
[PROOFSTEP]
use⟨W ⊓ (U' ⊓ V'), ⟨mW, mU, mV⟩⟩
[GOAL]
case h
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
e : germ F { val := x, property := mU } gU = germ F { val := x, property := mV } gV
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : F.map iU'.op gU = F.map iV'.op gV
⊢ ∃ iU iV,
    ∀ (w : { x_1 // x_1 ∈ { obj := W ⊓ (U' ⊓ V'), property := (_ : x ∈ ↑W ∧ x ∈ ↑(U' ⊓ V')) }.obj }),
      fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.obj) }) w) =
        fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.obj) }) w)
[PROOFSTEP]
refine' ⟨_, _, _⟩
[GOAL]
case h.refine'_1
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
e : germ F { val := x, property := mU } gU = germ F { val := x, property := mV } gV
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : F.map iU'.op gU = F.map iV'.op gV
⊢ { obj := W ⊓ (U' ⊓ V'), property := (_ : x ∈ ↑W ∧ x ∈ ↑(U' ⊓ V')) } ⟶ U
[PROOFSTEP]
change W ⊓ (U' ⊓ V') ⟶ U.obj
[GOAL]
case h.refine'_1
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
e : germ F { val := x, property := mU } gU = germ F { val := x, property := mV } gV
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : F.map iU'.op gU = F.map iV'.op gV
⊢ W ⊓ (U' ⊓ V') ⟶ U.obj
[PROOFSTEP]
exact Opens.infLERight _ _ ≫ Opens.infLELeft _ _ ≫ iU
[GOAL]
case h.refine'_2
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
e : germ F { val := x, property := mU } gU = germ F { val := x, property := mV } gV
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : F.map iU'.op gU = F.map iV'.op gV
⊢ { obj := W ⊓ (U' ⊓ V'), property := (_ : x ∈ ↑W ∧ x ∈ ↑(U' ⊓ V')) } ⟶ V
[PROOFSTEP]
change W ⊓ (U' ⊓ V') ⟶ V.obj
[GOAL]
case h.refine'_2
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
e : germ F { val := x, property := mU } gU = germ F { val := x, property := mV } gV
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : F.map iU'.op gU = F.map iV'.op gV
⊢ W ⊓ (U' ⊓ V') ⟶ V.obj
[PROOFSTEP]
exact Opens.infLERight _ _ ≫ Opens.infLERight _ _ ≫ iV
[GOAL]
case h.refine'_3
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
e : germ F { val := x, property := mU } gU = germ F { val := x, property := mV } gV
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : F.map iU'.op gU = F.map iV'.op gV
⊢ ∀ (w : { x_1 // x_1 ∈ { obj := W ⊓ (U' ⊓ V'), property := (_ : x ∈ ↑W ∧ x ∈ ↑(U' ⊓ V')) }.obj }),
    fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.obj) }) w) =
      fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.obj) }) w)
[PROOFSTEP]
intro w
[GOAL]
case h.refine'_3
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
wU :
  ∀ (x_1 : { x // x ∈ U' }),
    (fun x_2 => fU ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑U.obj) }) x_2)) x_1 = germ F x_1 gU
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
e : germ F { val := x, property := mU } gU = germ F { val := x, property := mV } gV
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : F.map iU'.op gU = F.map iV'.op gV
w : { x_1 // x_1 ∈ { obj := W ⊓ (U' ⊓ V'), property := (_ : x ∈ ↑W ∧ x ∈ ↑(U' ⊓ V')) }.obj }
⊢ fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.obj) }) w) =
    fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.obj) }) w)
[PROOFSTEP]
specialize wU ⟨w.1, w.2.2.1⟩
[GOAL]
case h.refine'_3
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
e : germ F { val := x, property := mU } gU = germ F { val := x, property := mV } gV
wV :
  ∀ (x_1 : { x // x ∈ V' }),
    (fun x_2 => fV ((fun x_3 => { val := ↑x_3, property := (_ : ↑x_3 ∈ ↑V.obj) }) x_2)) x_1 = germ F x_1 gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : F.map iU'.op gU = F.map iV'.op gV
w : { x_1 // x_1 ∈ { obj := W ⊓ (U' ⊓ V'), property := (_ : x ∈ ↑W ∧ x ∈ ↑(U' ⊓ V')) }.obj }
wU :
  (fun x_1 => fU ((fun x_2 => { val := ↑x_2, property := (_ : ↑x_2 ∈ ↑U.obj) }) x_1))
      { val := ↑w, property := (_ : ↑w ∈ ↑U') } =
    germ F { val := ↑w, property := (_ : ↑w ∈ ↑U') } gU
⊢ fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.obj) }) w) =
    fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.obj) }) w)
[PROOFSTEP]
specialize wV ⟨w.1, w.2.2.2⟩
[GOAL]
case h.refine'_3
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
e : germ F { val := x, property := mU } gU = germ F { val := x, property := mV } gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : F.map iU'.op gU = F.map iV'.op gV
w : { x_1 // x_1 ∈ { obj := W ⊓ (U' ⊓ V'), property := (_ : x ∈ ↑W ∧ x ∈ ↑(U' ⊓ V')) }.obj }
wU :
  (fun x_1 => fU ((fun x_2 => { val := ↑x_2, property := (_ : ↑x_2 ∈ ↑U.obj) }) x_1))
      { val := ↑w, property := (_ : ↑w ∈ ↑U') } =
    germ F { val := ↑w, property := (_ : ↑w ∈ ↑U') } gU
wV :
  (fun x_1 => fV ((fun x_2 => { val := ↑x_2, property := (_ : ↑x_2 ∈ ↑V.obj) }) x_1))
      { val := ↑w, property := (_ : ↑w ∈ ↑V') } =
    germ F { val := ↑w, property := (_ : ↑w ∈ ↑V') } gV
⊢ fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.obj) }) w) =
    fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.obj) }) w)
[PROOFSTEP]
dsimp at wU wV ⊢
[GOAL]
case h.refine'_3
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : { x_1 // x_1 ∈ U.obj }) → stalk F ↑y
hU : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fU
fV : (y : { x_1 // x_1 ∈ V.obj }) → stalk F ↑y
hV : PrelocalPredicate.pred (Sheafify.isLocallyGerm F).toPrelocalPredicate fV
U' : Opens ↑X
mU : ↑{ val := x, property := (_ : x ∈ U.obj) } ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
V' : Opens ↑X
mV : ↑{ val := x, property := (_ : x ∈ V.obj) } ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
e : germ F { val := x, property := mU } gU = germ F { val := x, property := mV } gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : F.map iU'.op gU = F.map iV'.op gV
w : { x_1 // x_1 ∈ { obj := W ⊓ (U' ⊓ V'), property := (_ : x ∈ ↑W ∧ x ∈ ↑(U' ⊓ V')) }.obj }
wU :
  fU { val := ↑w, property := (_ : ↑{ val := ↑w, property := (_ : ↑w ∈ ↑U') } ∈ ↑U.obj) } =
    germ F { val := ↑w, property := (_ : ↑w ∈ ↑U') } gU
wV :
  fV { val := ↑w, property := (_ : ↑{ val := ↑w, property := (_ : ↑w ∈ ↑V') } ∈ ↑V.obj) } =
    germ F { val := ↑w, property := (_ : ↑w ∈ ↑V') } gV
⊢ fU { val := ↑w, property := (_ : ↑w ∈ ↑U.obj) } = fV { val := ↑w, property := (_ : ↑w ∈ ↑V.obj) }
[PROOFSTEP]
erw [wU, ← F.germ_res iU' ⟨w, w.2.1⟩, wV, ← F.germ_res iV' ⟨w, w.2.1⟩, CategoryTheory.types_comp_apply,
  CategoryTheory.types_comp_apply, e']