ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : S[X]<VAR>hlifts : p ∈ lifts f<VAR>hp : p.Monic<VAR>hR : Nontrivial S<VAR>p' : R[X]<VAR>h₁ : map f p' = p<VAR>h₂ : p'.degree = p.degree<VAR>h₃ : p'.Monic<GOAL>∃ q, map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<VAR>n : ℕ<GOAL>term (f + g) s n = term f s n + term g s n
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>inst✝⁴ : Monoid M<VAR>inst✝³ : Preorder M<VAR>inst✝² : Preorder β<VAR>inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>f : β → M<VAR>hf : Monotone f<GOAL>Monotone fun a => f a ^ 0
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>inst✝⁴ : Monoid M<VAR>inst✝³ : Preorder M<VAR>inst✝² : Preorder β<VAR>inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>f : β → M<VAR>hf : Monotone f<VAR>n : ℕ<GOAL>Monotone fun a => f a ^ (n + 1)
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>inst✝⁴ : Monoid M<VAR>inst✝³ : Preorder M<VAR>inst✝² : Preorder β<VAR>inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>f : β → M<VAR>hf : Monotone f<VAR>n : ℕ<GOAL>Monotone fun a => f a ^ n * f a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : PreconnectedSpace X<VAR>inst✝ : Nonempty Y<VAR>f : X → Y<VAR>hf : IsLocallyConstant f<GOAL>∃ y, f = Function.const X y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : PreconnectedSpace X<VAR>inst✝ : Nonempty Y<VAR>f : X → Y<VAR>hf : IsLocallyConstant f<VAR>h : IsEmpty X<GOAL>∃ y, f = Function.const X y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : PreconnectedSpace X<VAR>inst✝ : Nonempty Y<VAR>f : X → Y<VAR>hf : IsLocallyConstant f<VAR>h : Nonempty X<GOAL>∃ y, f = Function.const X y
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} A<VAR>A' : Type u₂<VAR>inst✝² : Category.{max v₁ u₁, u₂} A'<VAR>B : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} B<VAR>J : GrothendieckTopology C<VAR>U : C<VAR>R : Presieve U<VAR>P : Cᵒᵖ ⥤ A<VAR>P' : Cᵒᵖ ⥤ A'<VAR>s : A ⥤ B<VAR>inst✝ : ReflectsLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s<VAR>h : IsSheaf J (P ⋙ s)<GOAL>IsSheaf J P
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} A<VAR>A' : Type u₂<VAR>inst✝² : Category.{max v₁ u₁, u₂} A'<VAR>B : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} B<VAR>J : GrothendieckTopology C<VAR>U : C<VAR>R : Presieve U<VAR>P : Cᵒᵖ ⥤ A<VAR>P' : Cᵒᵖ ⥤ A'<VAR>s : A ⥤ B<VAR>inst✝ : ReflectsLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s<VAR>h : ∀ ⦃X : C⦄, ∀ S ∈ J.sieves X, Nonempty (IsLimit ((P ⋙ s).mapCone S.arrows.cocone.op))<GOAL>∀ ⦃X : C⦄, ∀ S ∈ J.sieves X, Nonempty (IsLimit (P.mapCone S.arrows.cocone.op))
<VAR>α : Type u_1<VAR>xs ys : List α<VAR>p : α → Bool<GOAL>findIdx? p (xs ++ ys) = HOrElse.hOrElse (findIdx? p xs) fun x => Option.map (fun i => i + xs.length) (findIdx? p ys)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<GOAL>angle x (x + y) ≤ π / 2
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<GOAL>0 ≤ ‖x‖ / ‖x + y‖
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>a : ℤ<GOAL>↑p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValInt p a
<VAR>α : Type u<VAR>m n o : ℕ<VAR>m' : Type u_1<VAR>n' : Type u_2<VAR>o' : Type u_3<VAR>x y : α<VAR>u : Fin 0 → α<GOAL>Set.range (vecCons x (vecCons y u)) = {x, y}
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<GOAL>[].prod.totalDegree ≤ (List.map totalDegree []).sum
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<GOAL>0 ≤ (List.map totalDegree []).sum
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p✝ q p : MvPolynomial σ R<VAR>ps : List (MvPolynomial σ R)<GOAL>(p :: ps).prod.totalDegree ≤ (List.map totalDegree (p :: ps)).sum
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p✝ q p : MvPolynomial σ R<VAR>ps : List (MvPolynomial σ R)<GOAL>(p * ps.prod).totalDegree ≤ p.totalDegree + (List.map totalDegree ps).sum
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v, u₁} C<VAR>C' : Type u₂<VAR>inst✝ : Category.{v, u₂} C'<VAR>D : GlueData C<VAR>i j k : D.J<GOAL>D.t' i j k ≫ (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ D.t' j i k ≫ (pullbackSymmetry (D.f i k) (D.f i j)).hom = 𝟙 (pullback (D.f i j) (D.f i k))
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v, u₁} C<VAR>C' : Type u₂<VAR>inst✝ : Category.{v, u₂} C'<VAR>D : GlueData C<VAR>i j k : D.J<GOAL>(D.t' i j k ≫ (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ D.t' j i k ≫ (pullbackSymmetry (D.f i k) (D.f i j)).hom) ≫ pullback.fst (D.f i j) (D.f i k) = 𝟙 (pullback (D.f i j) (D.f i k)) ≫ pullback.fst (D.f i j) (D.f i k)
<VAR>m : ℕ<GOAL>↑(m + 1).toPNat' = if 0 < m + 1 then m + 1 else 1
<VAR>m : ℕ<GOAL>↑(m + 1).toPNat' = m + 1
<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>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S : J.Cover X<VAR>x : Meq P S<VAR>I : S.Arrow<GOAL>(Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 => P.map I_1.f.op) ⋯ ≫ colimit.ι (J.diagram P I.Y) (op ⊤)) (↑x I) = (colimMap (J.diagramPullback P I.f) ≫ colimit.pre (J.diagram P I.Y) (J.pullback I.f).op) ((colimit.ι (J.diagram P X) (op S)) ((Meq.equiv P S).symm x))
<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>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S : J.Cover X<VAR>x : Meq P S<VAR>I : S.Arrow<GOAL>(Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 => P.map I_1.f.op) ⋯ ≫ colimit.ι (J.diagram P I.Y) (op ⊤)) (↑x I) = (colimit.ι (J.diagram P X) (op S) ≫ colimMap (J.diagramPullback P I.f) ≫ colimit.pre (J.diagram P I.Y) (J.pullback I.f).op) ((Meq.equiv P S).symm x)
<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>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S : J.Cover X<VAR>x : Meq P S<VAR>I : S.Arrow<GOAL>(colimit.ι (J.diagram P I.Y) (op ⊤)) ((Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 => P.map I_1.f.op) ⋯) (↑x I)) = (colimit.ι (J.diagram P I.Y) ((J.pullback I.f).op.obj (op S))) (((J.diagramPullback P I.f).app (op S)) ((Meq.equiv P S).symm x))
<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>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S : J.Cover X<VAR>x : Meq P S<VAR>I : S.Arrow<GOAL>(colimit.ι (J.diagram P I.Y) (op ⊤)) ((Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 => P.map I_1.f.op) ⋯) (↑x I)) = (colimit.ι (J.diagram P I.Y) (op ((J.pullback I.f).obj S))) (((J.diagramPullback P I.f).app (op S)) ((Meq.equiv P S).symm x))
<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>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S : J.Cover X<VAR>x : Meq P S<VAR>I : S.Arrow<VAR>e : (J.pullback I.f).obj (unop (op S)) ⟶ ⊤ := homOfLE ⋯<GOAL>(colimit.ι (J.diagram P I.Y) (op ⊤)) ((Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 => P.map I_1.f.op) ⋯) (↑x I)) = (colimit.ι (J.diagram P I.Y) (op ((J.pullback I.f).obj S))) (((J.diagramPullback P I.f).app (op S)) ((Meq.equiv P S).symm x))
<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>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S : J.Cover X<VAR>x : Meq P S<VAR>I : S.Arrow<VAR>e : (J.pullback I.f).obj (unop (op S)) ⟶ ⊤ := homOfLE ⋯<GOAL>((J.diagram P I.Y).map e.op ≫ colimit.ι (J.diagram P I.Y) (op ((J.pullback I.f).obj (unop (op S))))) ((Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 => P.map I_1.f.op) ⋯) (↑x I)) = (colimit.ι (J.diagram P I.Y) (op ((J.pullback I.f).obj S))) (((J.diagramPullback P I.f).app (op S)) ((Meq.equiv P S).symm x))
<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>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S : J.Cover X<VAR>x : Meq P S<VAR>I : S.Arrow<VAR>e : (J.pullback I.f).obj (unop (op S)) ⟶ ⊤ := homOfLE ⋯<GOAL>(colimit.ι (J.diagram P I.Y) (op ((J.pullback I.f).obj (unop (op S))))) (((J.diagram P I.Y).map e.op) ((Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 => P.map I_1.f.op) ⋯) (↑x I))) = (colimit.ι (J.diagram P I.Y) (op ((J.pullback I.f).obj S))) (((J.diagramPullback P I.f).app (op S)) ((Meq.equiv P S).symm x))
<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>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S : J.Cover X<VAR>x : Meq P S<VAR>I : S.Arrow<VAR>e : (J.pullback I.f).obj (unop (op S)) ⟶ ⊤ := homOfLE ⋯<GOAL>((J.diagram P I.Y).map e.op) ((Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 => P.map I_1.f.op) ⋯) (↑x I)) = ((J.diagramPullback P I.f).app (op S)) ((Meq.equiv P S).symm x)
<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>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S : J.Cover X<VAR>x : Meq P S<VAR>I : S.Arrow<VAR>e : (J.pullback I.f).obj (unop (op S)) ⟶ ⊤ := homOfLE ⋯<GOAL>∀ (t : ((unop (op ((J.pullback I.f).obj (unop (op S))))).index P).L), (Multiequalizer.ι ((unop (op ((J.pullback I.f).obj (unop (op S))))).index P) t) (((J.diagram P I.Y).map e.op) ((Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 => P.map I_1.f.op) ⋯) (↑x I))) = (Multiequalizer.ι ((unop (op ((J.pullback I.f).obj (unop (op S))))).index P) t) (((J.diagramPullback P I.f).app (op S)) ((Meq.equiv P S).symm x))
<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>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S : J.Cover X<VAR>x : Meq P S<VAR>I : S.Arrow<VAR>e : (J.pullback I.f).obj (unop (op S)) ⟶ ⊤ := homOfLE ⋯<VAR>i : ((unop (op ((J.pullback I.f).obj (unop (op S))))).index P).L<GOAL>(Multiequalizer.ι ((S.pullback I.f).index P) i) ((Multiequalizer.lift ((S.pullback I.f).index P) (multiequalizer (⊤.index P)) (fun I_1 => Multiequalizer.ι (⊤.index P) (I_1.map e)) ⋯) ((Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 => P.map I_1.f.op) ⋯) (↑x I))) = (Multiequalizer.ι ((S.pullback I.f).index P) i) ((Multiequalizer.lift ((S.pullback I.f).index P) (multiequalizer (S.index P)) (fun I_1 => Multiequalizer.ι (S.index P) I_1.base) ⋯) ((Meq.equiv P S).symm x))
<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>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S : J.Cover X<VAR>x : Meq P S<VAR>I : S.Arrow<VAR>e : (J.pullback I.f).obj (unop (op S)) ⟶ ⊤ := homOfLE ⋯<VAR>i : ((unop (op ((J.pullback I.f).obj (unop (op S))))).index P).L<GOAL>(Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 => P.map I_1.f.op) ⋯ ≫ Multiequalizer.lift ((S.pullback I.f).index P) (multiequalizer (⊤.index P)) (fun I_1 => Multiequalizer.ι (⊤.index P) (I_1.map e)) ⋯ ≫ Multiequalizer.ι ((S.pullback I.f).index P) i) (↑x I) = (Multiequalizer.lift ((S.pullback I.f).index P) (multiequalizer (S.index P)) (fun I_1 => Multiequalizer.ι (S.index P) I_1.base) ⋯ ≫ Multiequalizer.ι ((S.pullback I.f).index P) i) ((Meq.equiv P S).symm x)
<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>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S : J.Cover X<VAR>x : Meq P S<VAR>I : S.Arrow<VAR>e : (J.pullback I.f).obj (unop (op S)) ⟶ ⊤ := homOfLE ⋯<VAR>i : ((unop (op ((J.pullback I.f).obj (unop (op S))))).index P).L<GOAL>(P.map (Cover.Arrow.map i e).f.op) (↑x I) = (Multiequalizer.ι (S.index P) (Cover.Arrow.base i)) ((Meq.equiv P S).symm x)
<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>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S : J.Cover X<VAR>x : Meq P S<VAR>I : S.Arrow<VAR>e : (J.pullback I.f).obj (unop (op S)) ⟶ ⊤ := homOfLE ⋯<VAR>i : ((unop (op ((J.pullback I.f).obj (unop (op S))))).index P).L<GOAL>(P.map (Cover.Arrow.map i e).f.op) (↑x I) = ↑x (Cover.Arrow.base i)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<GOAL>S.v₀₁.τ₁ ≫ S.v₁₂.τ₁ = 0
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : SeminormFamily 𝕜 E ι<VAR>q : Seminorm 𝕜 F<VAR>hq : Continuous ⇑q<GOAL>∃ C, 0 < C ∧ ∀ (x : F), q x ≤ C * ‖x‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : SeminormFamily 𝕜 E ι<VAR>q : Seminorm 𝕜 F<VAR>hq : Continuous ⇑q<VAR>hq' : Tendsto (⇑q) (𝓝 0) (𝓝 0)<GOAL>∃ C, 0 < C ∧ ∀ (x : F), q x ≤ C * ‖x‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : SeminormFamily 𝕜 E ι<VAR>q : Seminorm 𝕜 F<VAR>hq : Continuous ⇑q<VAR>hq' : Tendsto (⇑q) (𝓝 0) (𝓝 0)<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>hε : {y | ‖y‖ < ε} ⊆ ⇑q ⁻¹' Iio 1<GOAL>∃ C, 0 < C ∧ ∀ (x : F), q x ≤ C * ‖x‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : SeminormFamily 𝕜 E ι<VAR>q : Seminorm 𝕜 F<VAR>hq : Continuous ⇑q<VAR>hq' : Tendsto (⇑q) (𝓝 0) (𝓝 0)<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>hε : {y | ‖y‖ < ε} ⊆ ⇑q ⁻¹' Iio 1<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<GOAL>∃ C, 0 < C ∧ ∀ (x : F), q x ≤ C * ‖x‖
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f✝ g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>inst✝ : LinearOrder E<VAR>f : X → E<VAR>hf : AEStronglyMeasurable f μ<GOAL>∫ (x : X) in {x | f x < 0}, f x ∂μ = ∫ (x : X) in {x | f x ≤ 0}, f x ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f✝ g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>inst✝ : LinearOrder E<VAR>f : X → E<VAR>hf : AEStronglyMeasurable f μ<VAR>h_union : {x | f x ≤ 0} = {x | f x < 0} ∪ {x | f x = 0}<GOAL>∫ (x : X) in {x | f x < 0}, f x ∂μ = ∫ (x : X) in {x | f x ≤ 0}, f x ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f✝ g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>inst✝ : LinearOrder E<VAR>f : X → E<VAR>hf : AEStronglyMeasurable f μ<VAR>h_union : {x | f x ≤ 0} = {x | f x < 0} ∪ {x | f x = 0}<GOAL>∫ (x : X) in {x | f x < 0}, f x ∂μ = ∫ (x : X) in {x | f x < 0} ∪ {x | f x = 0}, f x ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f✝ g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>inst✝ : LinearOrder E<VAR>f : X → E<VAR>hf : AEStronglyMeasurable f μ<VAR>h_union : {x | f x ≤ 0} = {x | f x < 0} ∪ {x | f x = 0}<VAR>B : NullMeasurableSet {x | f x = 0} μ<GOAL>∫ (x : X) in {x | f x < 0}, f x ∂μ = ∫ (x : X) in {x | f x < 0} ∪ {x | f x = 0}, f x ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f✝ g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>inst✝ : LinearOrder E<VAR>f : X → E<VAR>hf : AEStronglyMeasurable f μ<VAR>h_union : {x | f x ≤ 0} = {x | f x < 0} ∪ {x | f x = 0}<VAR>B : NullMeasurableSet {x | f x = 0} μ<GOAL>∫ (x : X) in {x | f x < 0} ∪ {x | f x = 0}, f x ∂μ = ∫ (x : X) in {x | f x < 0}, f x ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f✝ g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>inst✝ : LinearOrder E<VAR>f : X → E<VAR>hf : AEStronglyMeasurable f μ<VAR>h_union : {x | f x ≤ 0} = {x | f x < 0} ∪ {x | f x = 0}<VAR>B : NullMeasurableSet {x | f x = 0} μ<GOAL>∀ᵐ (x : X) ∂μ.restrict {x | f x = 0}, f x = 0
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>inst✝ : (a : α) → Fintype (β a)<VAR>a✝ : α<VAR>f✝ : β a✝ → WType β<GOAL>0 < (mk a✝ f✝).depth
<VAR>P : PFunctor.{u}<VAR>α : Type u<VAR>r : α → α → Prop<VAR>x y : ↑P α<VAR>a : P.A<VAR>f₀ f₁ : P.B a → α<VAR>xeq : x = ⟨a, f₀⟩<VAR>yeq : y = ⟨a, f₁⟩<VAR>h : ∀ (i : P.B a), r (f₀ i) (f₁ i)<GOAL>Liftr r x y
<VAR>P : PFunctor.{u}<VAR>α : Type u<VAR>r : α → α → Prop<VAR>x y : ↑P α<VAR>a : P.A<VAR>f₀ f₁ : P.B a → α<VAR>xeq : x = ⟨a, f₀⟩<VAR>yeq : y = ⟨a, f₁⟩<VAR>h : ∀ (i : P.B a), r (f₀ i) (f₁ i)<GOAL>(fun t => (↑t).1) <$> ⟨a, fun i => ⟨(f₀ i, f₁ i), ⋯⟩⟩ = x ∧ (fun t => (↑t).2) <$> ⟨a, fun i => ⟨(f₀ i, f₁ i), ⋯⟩⟩ = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>inst✝² : Archimedean 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>r : 𝕜<VAR>h₁ : 0 ≤ r<VAR>h₂ : r < 1<VAR>hr : 0 = r<GOAL>Tendsto (fun n => r ^ (n + 1)) atTop (𝓝 0)
<VAR>α : Type u<VAR>A : α → PSet<VAR>β : Type u<VAR>B : β → PSet<VAR>H : (mk α A).Equiv (mk β B)<VAR>γ : Type u<VAR>C : γ → PSet<VAR>b : (mk β B).Type<VAR>hc : (mk γ C).Equiv ((mk β B).Func b)<GOAL>Acc (fun x x_1 => x ∈ x_1) (mk γ C)
<VAR>α : Type u<VAR>A : α → PSet<VAR>β : Type u<VAR>B : β → PSet<VAR>H : (mk α A).Equiv (mk β B)<VAR>γ : Type u<VAR>C : γ → PSet<VAR>b : (mk β B).Type<VAR>hc : (mk γ C).Equiv ((mk β B).Func b)<VAR>a : (mk α A).Type<VAR>ha : ((mk α A).Func a).Equiv ((mk β B).Func b)<GOAL>Acc (fun x x_1 => x ∈ x_1) (mk γ C)
<VAR>α : Type u<VAR>A : α → PSet<VAR>β : Type u<VAR>B : β → PSet<VAR>H✝ : (mk α A).Equiv (mk β B)<VAR>γ : Type u<VAR>C : γ → PSet<VAR>b : (mk β B).Type<VAR>hc : (mk γ C).Equiv ((mk β B).Func b)<VAR>a : (mk α A).Type<VAR>ha : ((mk α A).Func a).Equiv ((mk β B).Func b)<VAR>H : ((mk α A).Func a).Equiv (mk γ C)<GOAL>Acc (fun x x_1 => x ∈ x_1) (mk γ C)
<VAR>α : Type u<VAR>A : α → PSet<VAR>β : Type u<VAR>B : β → PSet<VAR>H✝ : (mk α A).Equiv (mk β B)<VAR>γ : Type u<VAR>C : γ → PSet<VAR>b : (mk β B).Type<VAR>hc : (mk γ C).Equiv ((mk β B).Func b)<VAR>a : (mk α A).Type<VAR>ha : ((mk α A).Func a).Equiv ((mk β B).Func b)<VAR>H : (A a).Equiv (mk γ C)<GOAL>Acc (fun x x_1 => x ∈ x_1) (mk γ C)
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : SeminormedAddCommGroup β<VAR>f✝ g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>inst✝ : Nonempty α<VAR>f : α →ᵇ β<VAR>M : ℝ<GOAL>‖f‖ ≤ M ↔ ∀ (x : α), ‖f x‖ ≤ M
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : SeminormedAddCommGroup β<VAR>f✝ g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>inst✝ : Nonempty α<VAR>f : α →ᵇ β<VAR>M : ℝ<GOAL>dist f 0 ≤ M ↔ ∀ (x : α), dist (f x) 0 ≤ M
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>x₁ x₂ : M<VAR>y₁ y₂ : ↥S<VAR>H : f.mk' x₁ y₁ = f.mk' x₂ y₂<GOAL>f.toMap (↑y₂ * x₁) = f.toMap (↑y₁ * x₂)
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>x₁ x₂ : M<VAR>y₁ y₂ : ↥S<VAR>H : f.toMap (↑y₂ * x₁) = f.toMap (↑y₁ * x₂)<GOAL>f.mk' x₁ y₁ = f.mk' x₂ y₂