ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>MetricSpace Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<VAR>fA : f ∈ GromovHausdorff.candidates X Y<GOAL>f (x, y) - f (z, t) ≤ 2 * ↑(GromovHausdorff.maxVar X Y) * dist (x, y) (z, t)
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>MetricSpace Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>fA : f ∈ GromovHausdorff.candidates X Y<GOAL>LipschitzWith (2 * GromovHausdorff.maxVar X Y) f
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>CompactSpace X<VAR>MetricSpace Y<VAR>CompactSpace Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>fA : f ∈ GromovHausdorff.candidates X Y<GOAL>GromovHausdorff.candidatesBOfCandidates f fA ∈ GromovHausdorff.candidatesB X Y
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>CompactSpace X<VAR>Nonempty X<VAR>MetricSpace Y<VAR>CompactSpace Y<VAR>Nonempty Y<GOAL>(fun p => dist p.1 p.2) ∈ GromovHausdorff.candidates X Y
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>CompactSpace X<VAR>Nonempty X<VAR>MetricSpace Y<VAR>CompactSpace Y<VAR>Nonempty Y<GOAL>GromovHausdorff.candidatesBDist X Y ∈ GromovHausdorff.candidatesB X Y
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>CompactSpace X<VAR>Nonempty X<VAR>MetricSpace Y<VAR>CompactSpace Y<VAR>Nonempty Y<GOAL>(GromovHausdorff.candidatesB X Y).Nonempty
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>MetricSpace Y<GOAL>IsClosed (GromovHausdorff.candidatesB X Y)
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>CompactSpace X<VAR>MetricSpace Y<VAR>CompactSpace Y<GOAL>IsCompact (GromovHausdorff.candidatesB X Y)
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>MetricSpace Y<VAR>f : GromovHausdorff.Cb X Y<VAR>C : ℝ<VAR>x : X<GOAL>BddBelow (Set.range fun y => f (Sum.inl x, Sum.inr y) + C)
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>MetricSpace Y<VAR>Nonempty Y<VAR>f : GromovHausdorff.Cb X Y<VAR>C : ℝ<GOAL>BddAbove (Set.range fun x => ⨅ y, f (Sum.inl x, Sum.inr y) + C)
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>MetricSpace Y<VAR>f : GromovHausdorff.Cb X Y<VAR>C : ℝ<VAR>y : Y<GOAL>BddBelow (Set.range fun x => f (Sum.inl x, Sum.inr y) + C)
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>Nonempty X<VAR>MetricSpace Y<VAR>f : GromovHausdorff.Cb X Y<VAR>C : ℝ<GOAL>BddAbove (Set.range fun y => ⨅ x, f (Sum.inl x, Sum.inr y) + C)
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>CompactSpace X<VAR>Nonempty X<VAR>MetricSpace Y<VAR>CompactSpace Y<VAR>Nonempty Y<GOAL>GromovHausdorff.HD (GromovHausdorff.candidatesBDist X Y) ≤ Metric.diam Set.univ + 1 + Metric.diam Set.univ
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>Nonempty X<VAR>MetricSpace Y<VAR>Nonempty Y<VAR>f g : GromovHausdorff.Cb X Y<GOAL>⨆ x, ⨅ y, f (Sum.inl x, Sum.inr y) ≤ (⨆ x, ⨅ y, g (Sum.inl x, Sum.inr y)) + dist f g
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>Nonempty X<VAR>MetricSpace Y<VAR>Nonempty Y<VAR>f g : GromovHausdorff.Cb X Y<GOAL>⨆ y, ⨅ x, f (Sum.inl x, Sum.inr y) ≤ (⨆ y, ⨅ x, g (Sum.inl x, Sum.inr y)) + dist f g
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>Nonempty X<VAR>MetricSpace Y<VAR>Nonempty Y<VAR>f g : GromovHausdorff.Cb X Y<GOAL>GromovHausdorff.HD f ≤ GromovHausdorff.HD g + dist f g
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>Nonempty X<VAR>MetricSpace Y<VAR>Nonempty Y<GOAL>Continuous GromovHausdorff.HD
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>CompactSpace X<VAR>Nonempty X<VAR>MetricSpace Y<VAR>CompactSpace Y<VAR>Nonempty Y<GOAL>∃ f ∈ GromovHausdorff.candidatesB X Y, ∀ g ∈ GromovHausdorff.candidatesB X Y, GromovHausdorff.HD f ≤ GromovHausdorff.HD g
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>CompactSpace X<VAR>Nonempty X<VAR>MetricSpace Y<VAR>CompactSpace Y<VAR>Nonempty Y<GOAL>GromovHausdorff.optimalGHDist X Y ∈ GromovHausdorff.candidatesB X Y
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>CompactSpace X<VAR>Nonempty X<VAR>MetricSpace Y<VAR>CompactSpace Y<VAR>Nonempty Y<VAR>g : GromovHausdorff.Cb X Y<VAR>hg : g ∈ GromovHausdorff.candidatesB X Y<GOAL>GromovHausdorff.HD (GromovHausdorff.optimalGHDist X Y) ≤ GromovHausdorff.HD g
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>CompactSpace X<VAR>Nonempty X<VAR>MetricSpace Y<VAR>CompactSpace Y<VAR>Nonempty Y<GOAL>Isometry (GromovHausdorff.optimalGHInjl X Y)
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>CompactSpace X<VAR>Nonempty X<VAR>MetricSpace Y<VAR>CompactSpace Y<VAR>Nonempty Y<GOAL>Isometry (GromovHausdorff.optimalGHInjr X Y)
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>CompactSpace X<VAR>Nonempty X<VAR>MetricSpace Y<VAR>CompactSpace Y<VAR>Nonempty Y<VAR>f : GromovHausdorff.Cb X Y<VAR>h : f ∈ GromovHausdorff.candidatesB X Y<GOAL>Metric.hausdorffDist (Set.range (GromovHausdorff.optimalGHInjl X Y)) (Set.range (GromovHausdorff.optimalGHInjr X Y)) ≤ GromovHausdorff.HD f
<VAR>ι : Type u_1<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>Finite ι<VAR>f : ι → Set X<GOAL>LocallyFinite f
<VAR>ι : Type u_1<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>f : ι → Set X<VAR>hf : LocallyFinite f<VAR>x : X<GOAL>{b | x ∈ f b}.Finite
<VAR>ι : Type u_1<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>f g : ι → Set X<VAR>hf : LocallyFinite f<VAR>hg : ∀ (i : ι), g i ⊆ f i<GOAL>LocallyFinite g
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>f : ι → Set X<VAR>g : ι' → ι<VAR>hf : LocallyFinite f<VAR>hg : Set.InjOn g {i | (f (g i)).Nonempty}<GOAL>LocallyFinite (f ∘ g)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>f : ι → Set X<VAR>g : ι' → ι<VAR>hf : LocallyFinite f<VAR>hg : Function.Injective g<GOAL>LocallyFinite (f ∘ g)
<VAR>ι : Type u_1<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>f : ι → Set X<GOAL>LocallyFinite f ↔ ∀ (x : X), ∀ᶠ (s : Set X) in (𝓝 x).smallSets, {i | (f i ∩ s).Nonempty}.Finite
<VAR>ι : Type u_1<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>f : ι → Set X<VAR>hf : LocallyFinite f<VAR>x : X<GOAL>∀ᶠ (s : Set X) in (𝓝 x).smallSets, {i | (f i ∩ s).Nonempty}.Finite
<VAR>ι : Type u_1<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>f : ι → Set X<VAR>ι' : Sort u_6<VAR>hf : LocallyFinite f<VAR>p : ι' → Prop<VAR>s : ι' → Set X<VAR>x : X<VAR>hb : (𝓝 x).HasBasis p s<GOAL>∃ i, p i ∧ {j | (f j ∩ s i).Nonempty}.Finite
<VAR>ι : Type u_1<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>f : ι → Set X<VAR>hf : LocallyFinite f<VAR>a : X<GOAL>𝓝[⋃ i, f i] a = ⨆ i, 𝓝[f i] a
<VAR>ι : Type u_1<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : ι → Set X<VAR>g : X → Y<VAR>hf : LocallyFinite f<VAR>hc : ∀ (i : ι), ∀ x ∈ closure (f i), ContinuousWithinAt g (f i) x<GOAL>ContinuousOn g (⋃ i, f i)
<VAR>ι : Type u_1<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : ι → Set X<VAR>g : X → Y<VAR>hf : LocallyFinite f<VAR>h_cl : ∀ (i : ι), IsClosed (f i)<VAR>h_cont : ∀ (i : ι), ContinuousOn g (f i)<GOAL>ContinuousOn g (⋃ i, f i)
<VAR>ι : Type u_1<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : ι → Set X<VAR>g : X → Y<VAR>hf : LocallyFinite f<VAR>h_cov : ⋃ i, f i = Set.univ<VAR>hc : ∀ (i : ι), ∀ x ∈ closure (f i), ContinuousWithinAt g (f i) x<GOAL>Continuous g
<VAR>ι : Type u_1<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : ι → Set X<VAR>g : X → Y<VAR>hf : LocallyFinite f<VAR>h_cov : ⋃ i, f i = Set.univ<VAR>h_cl : ∀ (i : ι), IsClosed (f i)<VAR>h_cont : ∀ (i : ι), ContinuousOn g (f i)<GOAL>Continuous g
<VAR>ι : Type u_1<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>f : ι → Set X<VAR>hf : LocallyFinite f<GOAL>LocallyFinite fun i => closure (f i)
<VAR>ι : Type u_1<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>f : ι → Set X<VAR>h : LocallyFinite f<GOAL>closure (⋃ i, f i) = ⋃ i, closure (f i)
<VAR>ι : Type u_1<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>f : ι → Set X<VAR>hf : LocallyFinite f<VAR>hc : ∀ (i : ι), IsClosed (f i)<GOAL>IsClosed (⋃ i, f i)
<VAR>ι : Type u_1<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>f : ι → Set X<VAR>hf : LocallyFinite f<VAR>hc : ∀ (i : ι), IsClosed (f i)<VAR>x : X<GOAL>⋂ i, ⋂ (_ : x ∉ f i), (f i)ᶜ ∈ 𝓝 x
<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>π : X → Sort u_6<VAR>f : ℕ → (x : X) → π x<VAR>hf : LocallyFinite fun n => {x | f (n + 1) x ≠ f n x}<GOAL>∃ F, ∀ (x : X), ∀ᶠ (p : ℕ × X) in Filter.atTop ×ˢ 𝓝 x, f p.1 p.2 = F p.2
<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>π : X → Sort u_6<VAR>f : ℕ → (x : X) → π x<VAR>hf : LocallyFinite fun n => {x | f (n + 1) x ≠ f n x}<GOAL>∃ F, ∀ (x : X), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ᶠ (y : X) in 𝓝 x, f n y = F y
<VAR>α : Type u_3<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>f : ℕ → X → α<VAR>hf : LocallyFinite fun n => {x | f (n + 1) x ≠ f n x}<GOAL>∃ F, ∀ (x : X), ∀ᶠ (n : ℕ) in Filter.atTop, f n =ᶠ[𝓝 x] F
<VAR>ι : Type u_1<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : ι → Set X<VAR>g : Y → X<VAR>hf : LocallyFinite f<VAR>hg : Continuous g<GOAL>LocallyFinite fun x => g ⁻¹' f x
<VAR>ι : Type u_1<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : ι → Set X<VAR>hf : LocallyFinite f<VAR>g : ι → Set Y<GOAL>LocallyFinite fun i => f i ×ˢ g i
<VAR>ι : Type u_1<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>g : ι → Set Y<VAR>hg : LocallyFinite g<VAR>f : ι → Set X<GOAL>LocallyFinite fun i => f i ×ˢ g i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>f : ι → Set X<VAR>e : ι' ≃ ι<GOAL>LocallyFinite (f ∘ ⇑e) ↔ LocallyFinite f
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>f : ι ⊕ ι' → Set X<GOAL>LocallyFinite f ↔ LocallyFinite (f ∘ Sum.inl) ∧ LocallyFinite (f ∘ Sum.inr)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>f : ι → Set X<VAR>g : ι' → Set X<VAR>hf : LocallyFinite f<VAR>hg : LocallyFinite g<GOAL>LocallyFinite (Sum.elim f g)
<VAR>ι : Type u_1<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>f : Option ι → Set X<GOAL>LocallyFinite f ↔ LocallyFinite (f ∘ some)
<VAR>ι : Type u_1<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>f : ι → Set X<VAR>hf : LocallyFinite f<VAR>s : Set X<GOAL>LocallyFinite (Option.elim' s f)
<VAR>ι : Type u_1<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>s : ι → Set X<VAR>hs : LocallyFinite s<VAR>hs' : ∀ (i : ι), IsClosed (s i)<VAR>x : X<GOAL>∀ᶠ (y : X) in 𝓝 x, {i | y ∈ s i} ⊆ {i | x ∈ s i}
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : TopCat<VAR>U : (TopologicalSpace.Opens ↑X)ᵒᵖ<VAR>P Q R : TopCat.Presheaf C X<VAR>f : P ⟶ Q<VAR>g : Q ⟶ R<GOAL>(f ≫ g).app U = f.app U ≫ g.app U
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : TopCat<VAR>P Q : TopCat.Presheaf C X<VAR>f g : P ⟶ Q<VAR>w : ∀ (U : TopologicalSpace.Opens ↑X), f.app (Opposite.op U) = g.app (Opposite.op U)<GOAL>f = g
<VAR>X : TopCat<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.ConcreteCategory C<VAR>F : TopCat.Presheaf C X<VAR>U V W : TopologicalSpace.Opens ↑X<VAR>e₁ : U ≤ V<VAR>e₂ : V ≤ W<VAR>x : (CategoryTheory.forget C).obj (F.obj (Opposite.op W))<GOAL>TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen x V e₂) U e₁ = TopCat.Presheaf.restrictOpen x U ⋯
<VAR>X : TopCat<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.ConcreteCategory C<VAR>F G : TopCat.Presheaf C X<VAR>e : F ⟶ G<VAR>U V : TopologicalSpace.Opens ↑X<VAR>h : U ≤ V<VAR>x : (CategoryTheory.forget C).obj (F.obj (Opposite.op V))<GOAL>(e.app (Opposite.op U)) (TopCat.Presheaf.restrictOpen x U h) = TopCat.Presheaf.restrictOpen ((e.app (Opposite.op V)) x) U h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>G : (TopologicalSpace.Opens ↑X)ᵒᵖ ⥤ C<GOAL>∀ (X_1 : (TopologicalSpace.Opens ↑Y)ᵒᵖ), ((TopCat.Presheaf.pushforward C f).obj G).obj X_1 = G.obj (Opposite.op ((TopologicalSpace.Opens.map f).obj (Opposite.unop X_1)))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : TopCat<VAR>f : X ⟶ Y<GOAL>∀ {X_1 Y_1 : (TopologicalSpace.Opens ↑X)ᵒᵖ ⥤ C} (α : X_1 ⟶ Y_1) (X_2 : (TopologicalSpace.Opens ↑Y)ᵒᵖ), ((TopCat.Presheaf.pushforward C f).map α).app X_2 = α.app (Opposite.op ((TopologicalSpace.Opens.map f).obj (Opposite.unop X_2)))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>G : (TopologicalSpace.Opens ↑X)ᵒᵖ ⥤ C<GOAL>∀ {X_1 Y_1 : (TopologicalSpace.Opens ↑Y)ᵒᵖ} (f_1 : X_1 ⟶ Y_1), ((TopCat.Presheaf.pushforward C f).obj G).map f_1 = G.map ((TopologicalSpace.Opens.map f).map f_1.unop).op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>ℱ 𝒢 : TopCat.Presheaf C X<VAR>α : ℱ ⟶ 𝒢<VAR>U : (TopologicalSpace.Opens ↑Y)ᵒᵖ<GOAL>((TopCat.Presheaf.pushforward C f).map α).app U = α.app (Opposite.op ((TopologicalSpace.Opens.map f).obj (Opposite.unop U)))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : TopCat<GOAL>TopCat.Presheaf.pushforward C (𝟙 X) = 𝟭 (TopCat.Presheaf C X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : TopCat<VAR>ℱ : TopCat.Presheaf C X<VAR>U : (TopologicalSpace.Opens ↑X)ᵒᵖ<GOAL>(TopCat.Presheaf.Pushforward.id ℱ).hom.app U = 𝟙 (((TopCat.Presheaf.pushforward C (𝟙 X)).obj ℱ).obj U)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : TopCat<VAR>ℱ : TopCat.Presheaf C X<VAR>U : (TopologicalSpace.Opens ↑X)ᵒᵖ<GOAL>(TopCat.Presheaf.Pushforward.id ℱ).inv.app U = 𝟙 (ℱ.obj U)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : TopCat<VAR>ℱ : TopCat.Presheaf C X<GOAL>(TopCat.Presheaf.pushforward C (𝟙 X)).obj ℱ = ℱ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : TopCat<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>ℱ : TopCat.Presheaf C X<GOAL>(TopCat.Presheaf.pushforward C (f ≫ g)).obj ℱ = (TopCat.Presheaf.pushforward C g).obj ((TopCat.Presheaf.pushforward C f).obj ℱ)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : TopCat<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>ℱ : TopCat.Presheaf C X<VAR>U : (TopologicalSpace.Opens ↑Z)ᵒᵖ<GOAL>(TopCat.Presheaf.Pushforward.comp f g ℱ).hom.app U = 𝟙 (((TopCat.Presheaf.pushforward C (f ≫ g)).obj ℱ).obj U)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : TopCat<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>ℱ : TopCat.Presheaf C X<VAR>U : (TopologicalSpace.Opens ↑Z)ᵒᵖ<GOAL>(TopCat.Presheaf.Pushforward.comp f g ℱ).inv.app U = 𝟙 (((TopCat.Presheaf.pushforward C g).obj ((TopCat.Presheaf.pushforward C f).obj ℱ)).obj U)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : TopCat<VAR>f g : X ⟶ Y<VAR>h : f = g<VAR>ℱ : TopCat.Presheaf C X<GOAL>(TopCat.Presheaf.pushforward C f).obj ℱ = (TopCat.Presheaf.pushforward C g).obj ℱ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : TopCat<VAR>f g : X ⟶ Y<VAR>h : f = g<VAR>ℱ : TopCat.Presheaf C X<VAR>U : (TopologicalSpace.Opens ↑Y)ᵒᵖ<GOAL>(TopCat.Presheaf.pushforwardEq h ℱ).hom.app U = ℱ.map (CategoryTheory.eqToHom ⋯)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : TopCat<VAR>H : X ≅ Y<VAR>G : (TopologicalSpace.Opens ↑X)ᵒᵖ ⥤ C<GOAL>∀ (X_1 : (TopologicalSpace.Opens ↑Y)ᵒᵖ), ((TopCat.Presheaf.presheafEquivOfIso C H).functor.obj G).obj X_1 = G.obj (Opposite.op ((TopologicalSpace.Opens.map H.hom).obj (Opposite.unop X_1)))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : TopCat<VAR>H : X ≅ Y<VAR>G : (TopologicalSpace.Opens ↑Y)ᵒᵖ ⥤ C<GOAL>∀ (X_1 : (TopologicalSpace.Opens ↑X)ᵒᵖ), ((TopCat.Presheaf.presheafEquivOfIso C H).inverse.obj G).obj X_1 = G.obj (Opposite.op ((TopologicalSpace.Opens.map H.inv).obj (Opposite.unop X_1)))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : TopCat<VAR>H : X ≅ Y<GOAL>∀ (X_1 : (TopologicalSpace.Opens ↑X)ᵒᵖ ⥤ C) (X_2 : (TopologicalSpace.Opens ↑X)ᵒᵖ), ((TopCat.Presheaf.presheafEquivOfIso C H).unitIso.inv.app X_1).app X_2 = X_1.map ((TopologicalSpace.Opens.mapMapIso H).symm.op.unit.app (Opposite.op ((TopologicalSpace.Opens.map H.hom).obj ((TopologicalSpace.Opens.map H.inv).obj (Opposite.unop X_2))))) ≫ X_1.map ((TopologicalSpace.Opens.map H.hom).map ((TopologicalSpace.Opens.mapMapIso H).symm.op.counit.app (Opposite.op ((TopologicalSpace.Opens.map H.inv).obj (Opposite.unop X_2)))).unop).op ≫ X_1.map ((TopologicalSpace.Opens.mapMapIso H).symm.op.unitInv.app X_2)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : TopCat<VAR>H : X ≅ Y<VAR>G : (TopologicalSpace.Opens ↑Y)ᵒᵖ ⥤ C<GOAL>∀ {X_1 Y_1 : (TopologicalSpace.Opens ↑X)ᵒᵖ} (f : X_1 ⟶ Y_1), ((TopCat.Presheaf.presheafEquivOfIso C H).inverse.obj G).map f = G.map ((TopologicalSpace.Opens.map H.inv).map f.unop).op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : TopCat<VAR>H : X ≅ Y<GOAL>∀ (X_1 : (TopologicalSpace.Opens ↑X)ᵒᵖ ⥤ C) (X_2 : (TopologicalSpace.Opens ↑X)ᵒᵖ), ((TopCat.Presheaf.presheafEquivOfIso C H).unitIso.hom.app X_1).app X_2 = X_1.map ((TopologicalSpace.Opens.mapMapIso H).symm.op.unit.app X_2) ≫ X_1.map ((TopologicalSpace.Opens.map H.hom).map ((TopologicalSpace.Opens.mapMapIso H).symm.op.counitInv.app (Opposite.op ((TopologicalSpace.Opens.map H.inv).obj (Opposite.unop X_2)))).unop).op ≫ X_1.map ((TopologicalSpace.Opens.mapMapIso H).symm.op.unitInv.app (Opposite.op ((TopologicalSpace.Opens.map H.hom).obj ((TopologicalSpace.Opens.map H.inv).obj (Opposite.unop X_2)))))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : TopCat<VAR>H : X ≅ Y<GOAL>∀ {X_1 Y_1 : (TopologicalSpace.Opens ↑X)ᵒᵖ ⥤ C} (α : X_1 ⟶ Y_1) (X_2 : (TopologicalSpace.Opens ↑Y)ᵒᵖ), ((TopCat.Presheaf.presheafEquivOfIso C H).functor.map α).app X_2 = α.app (Opposite.op ((TopologicalSpace.Opens.map H.hom).obj (Opposite.unop X_2)))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : TopCat<VAR>H : X ≅ Y<GOAL>∀ (X_1 : (TopologicalSpace.Opens ↑Y)ᵒᵖ ⥤ C) (X_2 : (TopologicalSpace.Opens ↑Y)ᵒᵖ), ((TopCat.Presheaf.presheafEquivOfIso C H).counitIso.hom.app X_1).app X_2 = X_1.map (CategoryTheory.eqToHom ⋯)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : TopCat<VAR>H : X ≅ Y<GOAL>∀ (X_1 : (TopologicalSpace.Opens ↑Y)ᵒᵖ ⥤ C) (X_2 : (TopologicalSpace.Opens ↑Y)ᵒᵖ), ((TopCat.Presheaf.presheafEquivOfIso C H).counitIso.inv.app X_1).app X_2 = X_1.map (CategoryTheory.eqToHom ⋯)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : TopCat<VAR>H : X ≅ Y<VAR>G : (TopologicalSpace.Opens ↑X)ᵒᵖ ⥤ C<GOAL>∀ {X_1 Y_1 : (TopologicalSpace.Opens ↑Y)ᵒᵖ} (f : X_1 ⟶ Y_1), ((TopCat.Presheaf.presheafEquivOfIso C H).functor.obj G).map f = G.map ((TopologicalSpace.Opens.map H.hom).map f.unop).op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : TopCat<VAR>H : X ≅ Y<GOAL>∀ {X_1 Y_1 : (TopologicalSpace.Opens ↑Y)ᵒᵖ ⥤ C} (α : X_1 ⟶ Y_1) (X_2 : (TopologicalSpace.Opens ↑X)ᵒᵖ), ((TopCat.Presheaf.presheafEquivOfIso C H).inverse.map α).app X_2 = α.app (Opposite.op ((TopologicalSpace.Opens.map H.inv).obj (Opposite.unop X_2)))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : TopCat<VAR>H₁ : X ≅ Y<VAR>ℱ : TopCat.Presheaf C X<VAR>𝒢 : TopCat.Presheaf C Y<VAR>H₂ : (TopCat.Presheaf.pushforward C H₁.hom).obj ℱ ⟶ 𝒢<VAR>U : (TopologicalSpace.Opens ↑X)ᵒᵖ<GOAL>(TopCat.Presheaf.toPushforwardOfIso H₁ H₂).app U = ℱ.map (CategoryTheory.eqToHom ⋯) ≫ H₂.app (Opposite.op ((TopologicalSpace.Opens.map H₁.inv).obj (Opposite.unop U)))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : TopCat<VAR>H₁ : X ≅ Y<VAR>ℱ : TopCat.Presheaf C Y<VAR>𝒢 : TopCat.Presheaf C X<VAR>H₂ : ℱ ⟶ (TopCat.Presheaf.pushforward C H₁.hom).obj 𝒢<VAR>U : (TopologicalSpace.Opens ↑X)ᵒᵖ<GOAL>(TopCat.Presheaf.pushforwardToOfIso H₁ H₂).app U = H₂.app (Opposite.op ((TopologicalSpace.Opens.map H₁.inv).obj (Opposite.unop U))) ≫ 𝒢.map (CategoryTheory.eqToHom ⋯)
<VAR>X : TopCat<VAR>ι : Type w<VAR>U : ι → TopologicalSpace.Opens ↑X<VAR>Y : TopologicalSpace.Opens ↑X<VAR>hY : Y = iSup U<VAR>f : CategoryTheory.FullSubcategory fun f => (CategoryTheory.Sieve.generate (TopCat.Presheaf.presieveOfCoveringAux U Y)).arrows f.hom<GOAL>((TopCat.Presheaf.generateEquivalenceOpensLe_functor' U hY).obj f).obj = f.obj.left
<VAR>X : TopCat<VAR>ι : Type w<VAR>U : ι → TopologicalSpace.Opens ↑X<VAR>Y : TopologicalSpace.Opens ↑X<VAR>hY : Y = iSup U<GOAL>∀ {x x_1 : CategoryTheory.FullSubcategory fun f => (CategoryTheory.Sieve.generate (TopCat.Presheaf.presieveOfCoveringAux U Y)).arrows f.hom} (g : x ⟶ x_1), (TopCat.Presheaf.generateEquivalenceOpensLe_functor' U hY).map g = g.left
<VAR>X : TopCat<VAR>ι : Type w<VAR>U : ι → TopologicalSpace.Opens ↑X<VAR>Y : TopologicalSpace.Opens ↑X<VAR>hY : Y = iSup U<GOAL>∀ {x x_1 : TopCat.Presheaf.SheafCondition.OpensLeCover U} (g : x ⟶ x_1), (TopCat.Presheaf.generateEquivalenceOpensLe_inverse' U hY).map g = CategoryTheory.Over.homMk g ⋯
<VAR>X : TopCat<VAR>ι : Type w<VAR>U : ι → TopologicalSpace.Opens ↑X<VAR>Y : TopologicalSpace.Opens ↑X<VAR>hY : Y = iSup U<VAR>V : TopCat.Presheaf.SheafCondition.OpensLeCover U<GOAL>((TopCat.Presheaf.generateEquivalenceOpensLe_inverse' U hY).obj V).obj.hom = CategoryTheory.homOfLE ⋯
<VAR>X : TopCat<VAR>ι : Type w<VAR>U : ι → TopologicalSpace.Opens ↑X<VAR>Y : TopologicalSpace.Opens ↑X<VAR>hY : Y = iSup U<VAR>V : TopCat.Presheaf.SheafCondition.OpensLeCover U<GOAL>((TopCat.Presheaf.generateEquivalenceOpensLe_inverse' U hY).obj V).obj.left = V.obj
<VAR>X : TopCat<VAR>ι : Type w<VAR>U : ι → TopologicalSpace.Opens ↑X<VAR>Y : TopologicalSpace.Opens ↑X<VAR>hY : Y = iSup U<VAR>V : TopCat.Presheaf.SheafCondition.OpensLeCover U<GOAL>((TopCat.Presheaf.generateEquivalenceOpensLe_inverse' U hY).obj V).obj.right.as = PUnit.unit
<VAR>X : TopCat<VAR>ι : Type w<VAR>U : ι → TopologicalSpace.Opens ↑X<VAR>Y : TopologicalSpace.Opens ↑X<VAR>hY : Y = iSup U<GOAL>(TopCat.Presheaf.generateEquivalenceOpensLe U hY).counitIso = CategoryTheory.eqToIso ⋯
<VAR>X : TopCat<VAR>ι : Type w<VAR>U : ι → TopologicalSpace.Opens ↑X<VAR>Y : TopologicalSpace.Opens ↑X<VAR>hY : Y = iSup U<GOAL>(TopCat.Presheaf.generateEquivalenceOpensLe U hY).functor = TopCat.Presheaf.generateEquivalenceOpensLe_functor' U ⋯
<VAR>X : TopCat<VAR>ι : Type w<VAR>U : ι → TopologicalSpace.Opens ↑X<VAR>Y : TopologicalSpace.Opens ↑X<VAR>hY : Y = iSup U<GOAL>(TopCat.Presheaf.generateEquivalenceOpensLe U hY).unitIso = CategoryTheory.eqToIso ⋯
<VAR>X : TopCat<VAR>ι : Type w<VAR>U : ι → TopologicalSpace.Opens ↑X<VAR>Y : TopologicalSpace.Opens ↑X<VAR>hY : Y = iSup U<GOAL>(TopCat.Presheaf.generateEquivalenceOpensLe U hY).inverse = TopCat.Presheaf.generateEquivalenceOpensLe_inverse' U ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>ι : Type w<VAR>U : ι → TopologicalSpace.Opens ↑X<VAR>Y : TopologicalSpace.Opens ↑X<VAR>hY : Y = iSup U<GOAL>(F.whiskerIsoMapGenerateCocone U hY).inv.hom = F.map (CategoryTheory.eqToHom ⋯)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>ι : Type w<VAR>U : ι → TopologicalSpace.Opens ↑X<VAR>Y : TopologicalSpace.Opens ↑X<VAR>hY : Y = iSup U<GOAL>(F.whiskerIsoMapGenerateCocone U hY).hom.hom = F.map (CategoryTheory.eqToHom ⋯)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<GOAL>F.IsSheaf ↔ F.IsSheafOpensLeCover
<VAR>X : TopCat<VAR>p₀ : ↑X<VAR>(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)<VAR>C : Type v<VAR>CategoryTheory.Category.{w, v} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>A : C<VAR>U V : (TopologicalSpace.Opens ↑X)ᵒᵖ<VAR>i : U ⟶ V<GOAL>(skyscraperPresheaf p₀ A).map i = if h : p₀ ∈ Opposite.unop V then CategoryTheory.eqToHom ⋯ else (⋯ ▸ CategoryTheory.Limits.terminalIsTerminal).from ((fun U => if p₀ ∈ Opposite.unop U then A else ⊤_ C) U)
<VAR>X : TopCat<VAR>p₀ : ↑X<VAR>(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)<VAR>C : Type v<VAR>CategoryTheory.Category.{w, v} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>A : C<VAR>U : (TopologicalSpace.Opens ↑X)ᵒᵖ<GOAL>(skyscraperPresheaf p₀ A).obj U = if p₀ ∈ Opposite.unop U then A else ⊤_ C
<VAR>X : TopCat<VAR>p₀ : ↑X<VAR>(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)<VAR>C : Type v<VAR>CategoryTheory.Category.{w, v} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>A : C<VAR>hd : (U : TopologicalSpace.Opens ↑(TopCat.of PUnit.{u + 1})) → Decidable (PUnit.unit ∈ U)<GOAL>skyscraperPresheaf p₀ A = (TopCat.Presheaf.pushforward C (ContinuousMap.const (↑(TopCat.of PUnit.{u + 1})) p₀)).obj (skyscraperPresheaf PUnit.unit A)