ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁵ : Category.{max v u, w} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>P : Cᵒᵖ ⥤ D<VAR>hsep : ∀ (X : C) (S : J.Cover X) (x y : (forget D).obj (P.obj (op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y<VAR>X : C<VAR>S : J.Cover X<VAR>s : Meq (J.plusObj P) S<VAR>inj : ∀ (X : C), Function.Injective ⇑((J.toPlus P).app (op X))<VAR>T : (I : S.Arrow) → J.Cover I.Y<VAR>t : (I : S.Arrow) → Meq P (T I)<VAR>ht : ∀ (I : S.Arrow), ↑s I = mk (t I)<VAR>B : J.Cover X := S.bind T<VAR>Z : B.Arrow → C<VAR>e1 : (I : B.Arrow) → I.Y ⟶ Z I<VAR>e2 : (I : B.Arrow) → Z I ⟶ X<VAR>he2 : ∀ (I : B.Arrow), S.sieve.arrows (e2 I)<VAR>h✝ : ∀ (I : B.Arrow), (fun Y f h => ((fun Y f hf => (T { Y := Y, f := f, hf := hf }).sieve) Y f h).arrows) (Z I) (e2 I) ⋯ (e1 I)<VAR>a✝ : ∀ (I : B.Arrow), e1 I ≫ e2 I = I.f<VAR>w : Meq P B := meqOfSep P hsep X S s T t ht<VAR>I : S.Arrow<GOAL>mk (w.pullback I.f) = mk (t I)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁵ : Category.{max v u, w} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>P : Cᵒᵖ ⥤ D<VAR>hsep : ∀ (X : C) (S : J.Cover X) (x y : (forget D).obj (P.obj (op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y<VAR>X : C<VAR>S : J.Cover X<VAR>s : Meq (J.plusObj P) S<VAR>inj : ∀ (X : C), Function.Injective ⇑((J.toPlus P).app (op X))<VAR>T : (I : S.Arrow) → J.Cover I.Y<VAR>t : (I : S.Arrow) → Meq P (T I)<VAR>ht : ∀ (I : S.Arrow), ↑s I = mk (t I)<VAR>B : J.Cover X := S.bind T<VAR>Z : B.Arrow → C<VAR>e1 : (I : B.Arrow) → I.Y ⟶ Z I<VAR>e2 : (I : B.Arrow) → Z I ⟶ X<VAR>he2 : ∀ (I : B.Arrow), S.sieve.arrows (e2 I)<VAR>h✝ : ∀ (I : B.Arrow), (fun Y f h => ((fun Y f hf => (T { Y := Y, f := f, hf := hf }).sieve) Y f h).arrows) (Z I) (e2 I) ⋯ (e1 I)<VAR>a✝ : ∀ (I : B.Arrow), e1 I ≫ e2 I = I.f<VAR>w : Meq P B := meqOfSep P hsep X S s T t ht<VAR>I : S.Arrow<GOAL>∀ (I_1 : (T I).Arrow), ((J.plusObj P).map I_1.f.op) (mk (w.pullback I.f)) = ((J.plusObj P).map I_1.f.op) (mk (t I))
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁵ : Category.{max v u, w} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>P : Cᵒᵖ ⥤ D<VAR>hsep : ∀ (X : C) (S : J.Cover X) (x y : (forget D).obj (P.obj (op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y<VAR>X : C<VAR>S : J.Cover X<VAR>s : Meq (J.plusObj P) S<VAR>inj : ∀ (X : C), Function.Injective ⇑((J.toPlus P).app (op X))<VAR>T : (I : S.Arrow) → J.Cover I.Y<VAR>t : (I : S.Arrow) → Meq P (T I)<VAR>ht : ∀ (I : S.Arrow), ↑s I = mk (t I)<VAR>B : J.Cover X := S.bind T<VAR>Z : B.Arrow → C<VAR>e1 : (I : B.Arrow) → I.Y ⟶ Z I<VAR>e2 : (I : B.Arrow) → Z I ⟶ X<VAR>he2 : ∀ (I : B.Arrow), S.sieve.arrows (e2 I)<VAR>h✝ : ∀ (I : B.Arrow), (fun Y f h => ((fun Y f hf => (T { Y := Y, f := f, hf := hf }).sieve) Y f h).arrows) (Z I) (e2 I) ⋯ (e1 I)<VAR>a✝ : ∀ (I : B.Arrow), e1 I ≫ e2 I = I.f<VAR>w : Meq P B := meqOfSep P hsep X S s T t ht<VAR>I : S.Arrow<VAR>II : (T I).Arrow<GOAL>((J.plusObj P).map II.f.op) (mk (w.pullback I.f)) = ((J.plusObj P).map II.f.op) (mk (t I))
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁵ : Category.{max v u, w} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>P : Cᵒᵖ ⥤ D<VAR>hsep : ∀ (X : C) (S : J.Cover X) (x y : (forget D).obj (P.obj (op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y<VAR>X : C<VAR>S : J.Cover X<VAR>s : Meq (J.plusObj P) S<VAR>inj : ∀ (X : C), Function.Injective ⇑((J.toPlus P).app (op X))<VAR>T : (I : S.Arrow) → J.Cover I.Y<VAR>t : (I : S.Arrow) → Meq P (T I)<VAR>ht : ∀ (I : S.Arrow), ↑s I = mk (t I)<VAR>B : J.Cover X := S.bind T<VAR>Z : B.Arrow → C<VAR>e1 : (I : B.Arrow) → I.Y ⟶ Z I<VAR>e2 : (I : B.Arrow) → Z I ⟶ X<VAR>he2 : ∀ (I : B.Arrow), S.sieve.arrows (e2 I)<VAR>h✝ : ∀ (I : B.Arrow), (fun Y f h => ((fun Y f hf => (T { Y := Y, f := f, hf := hf }).sieve) Y f h).arrows) (Z I) (e2 I) ⋯ (e1 I)<VAR>a✝ : ∀ (I : B.Arrow), e1 I ≫ e2 I = I.f<VAR>w : Meq P B := meqOfSep P hsep X S s T t ht<VAR>I : S.Arrow<VAR>II : (T I).Arrow<GOAL>∃ W h1 h2, ((w.pullback I.f).pullback II.f).refine h1 = ((t I).pullback II.f).refine h2
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁵ : Category.{max v u, w} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>P : Cᵒᵖ ⥤ D<VAR>hsep : ∀ (X : C) (S : J.Cover X) (x y : (forget D).obj (P.obj (op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y<VAR>X : C<VAR>S : J.Cover X<VAR>s : Meq (J.plusObj P) S<VAR>inj : ∀ (X : C), Function.Injective ⇑((J.toPlus P).app (op X))<VAR>T : (I : S.Arrow) → J.Cover I.Y<VAR>t : (I : S.Arrow) → Meq P (T I)<VAR>ht : ∀ (I : S.Arrow), ↑s I = mk (t I)<VAR>B : J.Cover X := S.bind T<VAR>Z : B.Arrow → C<VAR>e1 : (I : B.Arrow) → I.Y ⟶ Z I<VAR>e2 : (I : B.Arrow) → Z I ⟶ X<VAR>he2 : ∀ (I : B.Arrow), S.sieve.arrows (e2 I)<VAR>h✝ : ∀ (I : B.Arrow), (fun Y f h => ((fun Y f hf => (T { Y := Y, f := f, hf := hf }).sieve) Y f h).arrows) (Z I) (e2 I) ⋯ (e1 I)<VAR>a✝ : ∀ (I : B.Arrow), e1 I ≫ e2 I = I.f<VAR>w : Meq P B := meqOfSep P hsep X S s T t ht<VAR>I : S.Arrow<VAR>II : (T I).Arrow<GOAL>∃ h1 h2, ((w.pullback I.f).pullback II.f).refine h1 = ((t I).pullback II.f).refine h2
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁵ : Category.{max v u, w} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>P : Cᵒᵖ ⥤ D<VAR>hsep : ∀ (X : C) (S : J.Cover X) (x y : (forget D).obj (P.obj (op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y<VAR>X : C<VAR>S : J.Cover X<VAR>s : Meq (J.plusObj P) S<VAR>inj : ∀ (X : C), Function.Injective ⇑((J.toPlus P).app (op X))<VAR>T : (I : S.Arrow) → J.Cover I.Y<VAR>t : (I : S.Arrow) → Meq P (T I)<VAR>ht : ∀ (I : S.Arrow), ↑s I = mk (t I)<VAR>B : J.Cover X := S.bind T<VAR>Z : B.Arrow → C<VAR>e1 : (I : B.Arrow) → I.Y ⟶ Z I<VAR>e2 : (I : B.Arrow) → Z I ⟶ X<VAR>he2 : ∀ (I : B.Arrow), S.sieve.arrows (e2 I)<VAR>h✝ : ∀ (I : B.Arrow), (fun Y f h => ((fun Y f hf => (T { Y := Y, f := f, hf := hf }).sieve) Y f h).arrows) (Z I) (e2 I) ⋯ (e1 I)<VAR>a✝ : ∀ (I : B.Arrow), e1 I ≫ e2 I = I.f<VAR>w : Meq P B := meqOfSep P hsep X S s T t ht<VAR>I : S.Arrow<VAR>II : (T I).Arrow<VAR>e0 : (J.pullback II.f).obj (T I) ⟶ (J.pullback II.f).obj ((J.pullback I.f).obj B) := homOfLE ⋯<GOAL>∃ h1 h2, ((w.pullback I.f).pullback II.f).refine h1 = ((t I).pullback II.f).refine h2
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁵ : Category.{max v u, w} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>P : Cᵒᵖ ⥤ D<VAR>hsep : ∀ (X : C) (S : J.Cover X) (x y : (forget D).obj (P.obj (op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y<VAR>X : C<VAR>S : J.Cover X<VAR>s : Meq (J.plusObj P) S<VAR>inj : ∀ (X : C), Function.Injective ⇑((J.toPlus P).app (op X))<VAR>T : (I : S.Arrow) → J.Cover I.Y<VAR>t : (I : S.Arrow) → Meq P (T I)<VAR>ht : ∀ (I : S.Arrow), ↑s I = mk (t I)<VAR>B : J.Cover X := S.bind T<VAR>Z : B.Arrow → C<VAR>e1 : (I : B.Arrow) → I.Y ⟶ Z I<VAR>e2 : (I : B.Arrow) → Z I ⟶ X<VAR>he2 : ∀ (I : B.Arrow), S.sieve.arrows (e2 I)<VAR>h✝ : ∀ (I : B.Arrow), (fun Y f h => ((fun Y f hf => (T { Y := Y, f := f, hf := hf }).sieve) Y f h).arrows) (Z I) (e2 I) ⋯ (e1 I)<VAR>a✝ : ∀ (I : B.Arrow), e1 I ≫ e2 I = I.f<VAR>w : Meq P B := meqOfSep P hsep X S s T t ht<VAR>I : S.Arrow<VAR>II : (T I).Arrow<VAR>e0 : (J.pullback II.f).obj (T I) ⟶ (J.pullback II.f).obj ((J.pullback I.f).obj B) := homOfLE ⋯<GOAL>((w.pullback I.f).pullback II.f).refine e0 = ((t I).pullback II.f).refine (𝟙 ((J.pullback II.f).obj (T I)))
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁵ : Category.{max v u, w} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>P : Cᵒᵖ ⥤ D<VAR>hsep : ∀ (X : C) (S : J.Cover X) (x y : (forget D).obj (P.obj (op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y<VAR>X : C<VAR>S : J.Cover X<VAR>s : Meq (J.plusObj P) S<VAR>inj : ∀ (X : C), Function.Injective ⇑((J.toPlus P).app (op X))<VAR>T : (I : S.Arrow) → J.Cover I.Y<VAR>t : (I : S.Arrow) → Meq P (T I)<VAR>ht : ∀ (I : S.Arrow), ↑s I = mk (t I)<VAR>B : J.Cover X := S.bind T<VAR>Z : B.Arrow → C<VAR>e1 : (I : B.Arrow) → I.Y ⟶ Z I<VAR>e2 : (I : B.Arrow) → Z I ⟶ X<VAR>he2 : ∀ (I : B.Arrow), S.sieve.arrows (e2 I)<VAR>h✝ : ∀ (I : B.Arrow), (fun Y f h => ((fun Y f hf => (T { Y := Y, f := f, hf := hf }).sieve) Y f h).arrows) (Z I) (e2 I) ⋯ (e1 I)<VAR>a✝ : ∀ (I : B.Arrow), e1 I ≫ e2 I = I.f<VAR>w : Meq P B := meqOfSep P hsep X S s T t ht<VAR>I : S.Arrow<VAR>II : (T I).Arrow<VAR>e0 : (J.pullback II.f).obj (T I) ⟶ (J.pullback II.f).obj ((J.pullback I.f).obj B) := homOfLE ⋯<VAR>IV : ((J.pullback II.f).obj (T I)).Arrow<GOAL>↑(((w.pullback I.f).pullback II.f).refine e0) IV = ↑(((t I).pullback II.f).refine (𝟙 ((J.pullback II.f).obj (T I)))) IV
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁵ : Category.{max v u, w} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>P : Cᵒᵖ ⥤ D<VAR>hsep : ∀ (X : C) (S : J.Cover X) (x y : (forget D).obj (P.obj (op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y<VAR>X : C<VAR>S : J.Cover X<VAR>s : Meq (J.plusObj P) S<VAR>inj : ∀ (X : C), Function.Injective ⇑((J.toPlus P).app (op X))<VAR>T : (I : S.Arrow) → J.Cover I.Y<VAR>t : (I : S.Arrow) → Meq P (T I)<VAR>ht : ∀ (I : S.Arrow), ↑s I = mk (t I)<VAR>B : J.Cover X := S.bind T<VAR>Z : B.Arrow → C<VAR>e1 : (I : B.Arrow) → I.Y ⟶ Z I<VAR>e2 : (I : B.Arrow) → Z I ⟶ X<VAR>he2 : ∀ (I : B.Arrow), S.sieve.arrows (e2 I)<VAR>h✝ : ∀ (I : B.Arrow), (fun Y f h => ((fun Y f hf => (T { Y := Y, f := f, hf := hf }).sieve) Y f h).arrows) (Z I) (e2 I) ⋯ (e1 I)<VAR>a✝ : ∀ (I : B.Arrow), e1 I ≫ e2 I = I.f<VAR>w : Meq P B := meqOfSep P hsep X S s T t ht<VAR>I : S.Arrow<VAR>II : (T I).Arrow<VAR>e0 : (J.pullback II.f).obj (T I) ⟶ (J.pullback II.f).obj ((J.pullback I.f).obj B) := homOfLE ⋯<VAR>IV : ((J.pullback II.f).obj (T I)).Arrow<VAR>IA : B.Arrow := { Y := IV.Y, f := (IV.f ≫ II.f) ≫ I.f, hf := ⋯ }<GOAL>↑(((w.pullback I.f).pullback II.f).refine e0) IV = ↑(((t I).pullback II.f).refine (𝟙 ((J.pullback II.f).obj (T I)))) IV
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁵ : Category.{max v u, w} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>P : Cᵒᵖ ⥤ D<VAR>hsep : ∀ (X : C) (S : J.Cover X) (x y : (forget D).obj (P.obj (op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y<VAR>X : C<VAR>S : J.Cover X<VAR>s : Meq (J.plusObj P) S<VAR>inj : ∀ (X : C), Function.Injective ⇑((J.toPlus P).app (op X))<VAR>T : (I : S.Arrow) → J.Cover I.Y<VAR>t : (I : S.Arrow) → Meq P (T I)<VAR>ht : ∀ (I : S.Arrow), ↑s I = mk (t I)<VAR>B : J.Cover X := S.bind T<VAR>Z : B.Arrow → C<VAR>e1 : (I : B.Arrow) → I.Y ⟶ Z I<VAR>e2 : (I : B.Arrow) → Z I ⟶ X<VAR>he2 : ∀ (I : B.Arrow), S.sieve.arrows (e2 I)<VAR>h✝ : ∀ (I : B.Arrow), (fun Y f h => ((fun Y f hf => (T { Y := Y, f := f, hf := hf }).sieve) Y f h).arrows) (Z I) (e2 I) ⋯ (e1 I)<VAR>a✝ : ∀ (I : B.Arrow), e1 I ≫ e2 I = I.f<VAR>w : Meq P B := meqOfSep P hsep X S s T t ht<VAR>I : S.Arrow<VAR>II : (T I).Arrow<VAR>e0 : (J.pullback II.f).obj (T I) ⟶ (J.pullback II.f).obj ((J.pullback I.f).obj B) := homOfLE ⋯<VAR>IV : ((J.pullback II.f).obj (T I)).Arrow<VAR>IA : B.Arrow := { Y := IV.Y, f := (IV.f ≫ II.f) ≫ I.f, hf := ⋯ }<VAR>IB : S.Arrow := IA.fromMiddle<VAR>IC : (T IB).Arrow := IA.toMiddle<GOAL>↑(((w.pullback I.f).pullback II.f).refine e0) IV = ↑(((t I).pullback II.f).refine (𝟙 ((J.pullback II.f).obj (T I)))) IV
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁵ : Category.{max v u, w} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>P : Cᵒᵖ ⥤ D<VAR>hsep : ∀ (X : C) (S : J.Cover X) (x y : (forget D).obj (P.obj (op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y<VAR>X : C<VAR>S : J.Cover X<VAR>s : Meq (J.plusObj P) S<VAR>inj : ∀ (X : C), Function.Injective ⇑((J.toPlus P).app (op X))<VAR>T : (I : S.Arrow) → J.Cover I.Y<VAR>t : (I : S.Arrow) → Meq P (T I)<VAR>ht : ∀ (I : S.Arrow), ↑s I = mk (t I)<VAR>B : J.Cover X := S.bind T<VAR>Z : B.Arrow → C<VAR>e1 : (I : B.Arrow) → I.Y ⟶ Z I<VAR>e2 : (I : B.Arrow) → Z I ⟶ X<VAR>he2 : ∀ (I : B.Arrow), S.sieve.arrows (e2 I)<VAR>h✝ : ∀ (I : B.Arrow), (fun Y f h => ((fun Y f hf => (T { Y := Y, f := f, hf := hf }).sieve) Y f h).arrows) (Z I) (e2 I) ⋯ (e1 I)<VAR>a✝ : ∀ (I : B.Arrow), e1 I ≫ e2 I = I.f<VAR>w : Meq P B := meqOfSep P hsep X S s T t ht<VAR>I : S.Arrow<VAR>II : (T I).Arrow<VAR>e0 : (J.pullback II.f).obj (T I) ⟶ (J.pullback II.f).obj ((J.pullback I.f).obj B) := homOfLE ⋯<VAR>IV : ((J.pullback II.f).obj (T I)).Arrow<VAR>IA : B.Arrow := { Y := IV.Y, f := (IV.f ≫ II.f) ≫ I.f, hf := ⋯ }<VAR>IB : S.Arrow := IA.fromMiddle<VAR>IC : (T IB).Arrow := IA.toMiddle<VAR>ID : (T I).Arrow := { Y := IV.Y, f := IV.f ≫ II.f, hf := ⋯ }<GOAL>↑(((w.pullback I.f).pullback II.f).refine e0) IV = ↑(((t I).pullback II.f).refine (𝟙 ((J.pullback II.f).obj (T I)))) IV
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁵ : Category.{max v u, w} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>P : Cᵒᵖ ⥤ D<VAR>hsep : ∀ (X : C) (S : J.Cover X) (x y : (forget D).obj (P.obj (op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y<VAR>X : C<VAR>S : J.Cover X<VAR>s : Meq (J.plusObj P) S<VAR>inj : ∀ (X : C), Function.Injective ⇑((J.toPlus P).app (op X))<VAR>T : (I : S.Arrow) → J.Cover I.Y<VAR>t : (I : S.Arrow) → Meq P (T I)<VAR>ht : ∀ (I : S.Arrow), ↑s I = mk (t I)<VAR>B : J.Cover X := S.bind T<VAR>Z : B.Arrow → C<VAR>e1 : (I : B.Arrow) → I.Y ⟶ Z I<VAR>e2 : (I : B.Arrow) → Z I ⟶ X<VAR>he2 : ∀ (I : B.Arrow), S.sieve.arrows (e2 I)<VAR>h✝ : ∀ (I : B.Arrow), (fun Y f h => ((fun Y f hf => (T { Y := Y, f := f, hf := hf }).sieve) Y f h).arrows) (Z I) (e2 I) ⋯ (e1 I)<VAR>a✝ : ∀ (I : B.Arrow), e1 I ≫ e2 I = I.f<VAR>w : Meq P B := meqOfSep P hsep X S s T t ht<VAR>I : S.Arrow<VAR>II : (T I).Arrow<VAR>e0 : (J.pullback II.f).obj (T I) ⟶ (J.pullback II.f).obj ((J.pullback I.f).obj B) := homOfLE ⋯<VAR>IV : ((J.pullback II.f).obj (T I)).Arrow<VAR>IA : B.Arrow := { Y := IV.Y, f := (IV.f ≫ II.f) ≫ I.f, hf := ⋯ }<VAR>IB : S.Arrow := IA.fromMiddle<VAR>IC : (T IB).Arrow := IA.toMiddle<VAR>ID : (T I).Arrow := { Y := IV.Y, f := IV.f ≫ II.f, hf := ⋯ }<GOAL>((J.toPlus P).app (op IV.Y)) (↑(t IB) IC) = ((J.toPlus P).app (op IV.Y)) (↑(t I) ID)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁵ : Category.{max v u, w} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>P : Cᵒᵖ ⥤ D<VAR>hsep : ∀ (X : C) (S : J.Cover X) (x y : (forget D).obj (P.obj (op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y<VAR>X : C<VAR>S : J.Cover X<VAR>s : Meq (J.plusObj P) S<VAR>inj : ∀ (X : C), Function.Injective ⇑((J.toPlus P).app (op X))<VAR>T : (I : S.Arrow) → J.Cover I.Y<VAR>t : (I : S.Arrow) → Meq P (T I)<VAR>ht : ∀ (I : S.Arrow), ↑s I = mk (t I)<VAR>B : J.Cover X := S.bind T<VAR>Z : B.Arrow → C<VAR>e1 : (I : B.Arrow) → I.Y ⟶ Z I<VAR>e2 : (I : B.Arrow) → Z I ⟶ X<VAR>he2 : ∀ (I : B.Arrow), S.sieve.arrows (e2 I)<VAR>h✝ : ∀ (I : B.Arrow), (fun Y f h => ((fun Y f hf => (T { Y := Y, f := f, hf := hf }).sieve) Y f h).arrows) (Z I) (e2 I) ⋯ (e1 I)<VAR>a✝ : ∀ (I : B.Arrow), e1 I ≫ e2 I = I.f<VAR>w : Meq P B := meqOfSep P hsep X S s T t ht<VAR>I : S.Arrow<VAR>II : (T I).Arrow<VAR>e0 : (J.pullback II.f).obj (T I) ⟶ (J.pullback II.f).obj ((J.pullback I.f).obj B) := homOfLE ⋯<VAR>IV : ((J.pullback II.f).obj (T I)).Arrow<VAR>IA : B.Arrow := { Y := IV.Y, f := (IV.f ≫ II.f) ≫ I.f, hf := ⋯ }<VAR>IB : S.Arrow := IA.fromMiddle<VAR>IC : (T IB).Arrow := IA.toMiddle<VAR>ID : (T I).Arrow := { Y := IV.Y, f := IV.f ≫ II.f, hf := ⋯ }<GOAL>((J.plusObj P).map IC.f.op) (↑s IB) = ((J.plusObj P).map ID.f.op) (↑s I)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁵ : Category.{max v u, w} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>P : Cᵒᵖ ⥤ D<VAR>hsep : ∀ (X : C) (S : J.Cover X) (x y : (forget D).obj (P.obj (op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y<VAR>X : C<VAR>S : J.Cover X<VAR>s : Meq (J.plusObj P) S<VAR>inj : ∀ (X : C), Function.Injective ⇑((J.toPlus P).app (op X))<VAR>T : (I : S.Arrow) → J.Cover I.Y<VAR>t : (I : S.Arrow) → Meq P (T I)<VAR>ht : ∀ (I : S.Arrow), ↑s I = mk (t I)<VAR>B : J.Cover X := S.bind T<VAR>Z : B.Arrow → C<VAR>e1 : (I : B.Arrow) → I.Y ⟶ Z I<VAR>e2 : (I : B.Arrow) → Z I ⟶ X<VAR>he2 : ∀ (I : B.Arrow), S.sieve.arrows (e2 I)<VAR>h✝ : ∀ (I : B.Arrow), (fun Y f h => ((fun Y f hf => (T { Y := Y, f := f, hf := hf }).sieve) Y f h).arrows) (Z I) (e2 I) ⋯ (e1 I)<VAR>a✝ : ∀ (I : B.Arrow), e1 I ≫ e2 I = I.f<VAR>w : Meq P B := meqOfSep P hsep X S s T t ht<VAR>I : S.Arrow<VAR>II : (T I).Arrow<VAR>e0 : (J.pullback II.f).obj (T I) ⟶ (J.pullback II.f).obj ((J.pullback I.f).obj B) := homOfLE ⋯<VAR>IV : ((J.pullback II.f).obj (T I)).Arrow<VAR>IA : B.Arrow := { Y := IV.Y, f := (IV.f ≫ II.f) ≫ I.f, hf := ⋯ }<VAR>IB : S.Arrow := IA.fromMiddle<VAR>IC : (T IB).Arrow := IA.toMiddle<VAR>ID : (T I).Arrow := { Y := IV.Y, f := IV.f ≫ II.f, hf := ⋯ }<VAR>IR : S.Relation := { fst := { Y := IB.Y, f := IB.f, hf := ⋯ }, snd := { Y := I.Y, f := I.f, hf := ⋯ }, r := { Z := IA.Y, g₁ := IA.toMiddleHom, g₂ := IV.f ≫ II.f, w := ⋯ } }<GOAL>((J.plusObj P).map IC.f.op) (↑s IB) = ((J.plusObj P).map ID.f.op) (↑s I)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq β<VAR>f g : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>a : α<VAR>b c : β<VAR>s₁ s₂ : Finset α<VAR>h : s₁ ⊆ s₂<GOAL>image f s₁ ⊆ image f s₂
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n m : ℕ<VAR>inst✝ : DivisionRing K<VAR>s : Stream'.Seq (Pair K)<VAR>terminatedAt_n : s.get? n = none<GOAL>convs'Aux s (n + 1) = convs'Aux s n
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : PseudoMetricSpace β<VAR>inst✝² : PseudoMetricSpace γ<VAR>f✝ g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>δ : Type u_2<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : DiscreteTopology δ<VAR>f : α ↪ δ<VAR>h : δ →ᵇ β<VAR>g₁ g₂ : α →ᵇ β<GOAL>dist (extend f g₁ h) (extend f g₂ h) = dist g₁ g₂
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ✝ : S₁ ⟶ S₂<VAR>h₁✝ : S₁.HomologyData<VAR>h₂✝ : S₂.HomologyData<VAR>inst✝¹ : S₁.HasHomology<VAR>inst✝ : S₂.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<GOAL>h₁.homologyIso.hom ≫ rightHomologyMap' φ h₁ h₂ = homologyMap φ ≫ h₂.homologyIso.hom
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>N i : ℕ<VAR>h : N < i<GOAL>(revAt N) i = i
<VAR>J : Type u<VAR>inst✝⁴ : SmallCategory J<VAR>F✝ : J ⥤ TopCat<VAR>F : J ⥤ TopCat<VAR>inst✝³ : IsCofilteredOrEmpty J<VAR>inst✝² : ∀ (j : J), Nonempty ↑(F.obj j)<VAR>inst✝¹ : ∀ (j : J), CompactSpace ↑(F.obj j)<VAR>inst✝ : ∀ (j : J), T2Space ↑(F.obj j)<GOAL>Nonempty ↑(limitCone F).pt
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hn : 2 ≤ n<VAR>h : m ≤ m / n<GOAL>n * m ≤ m
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hn : 2 ≤ n<VAR>h : m ≤ m / n<GOAL>m * n ≤ m
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝¹² : Group G<VAR>inst✝¹¹ : Group H<VAR>inst✝¹⁰ : MulAction G α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : MulAction H β<VAR>inst✝⁷ : MeasurableSpace β<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : MeasurableSMul G α<VAR>inst✝³ : SMulInvariantMeasure G α μ<VAR>inst✝² : Countable G<VAR>ν : Measure α<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hs : IsFundamentalDomain G s μ<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ (γ : G) (x : α), f (γ • x) = f x<GOAL>essSup f (μ.restrict s) = essSup f μ
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝¹² : Group G<VAR>inst✝¹¹ : Group H<VAR>inst✝¹⁰ : MulAction G α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : MulAction H β<VAR>inst✝⁷ : MeasurableSpace β<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : MeasurableSMul G α<VAR>inst✝³ : SMulInvariantMeasure G α μ<VAR>inst✝² : Countable G<VAR>ν : Measure α<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hs : IsFundamentalDomain G s μ<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ (γ : G) (x : α), f (γ • x) = f x<GOAL>essSup f μ ≤ essSup f (μ.restrict s)