ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : CommSemiring S<VAR>p : R[X]<VAR>f : R →+* S<VAR>z : S<VAR>hz : eval₂ f z p = 0<VAR>inj : ∀ (x : R), f x = 0 → x = 0<GOAL>f p.leadingCoeff ^ (p.natDegree - 1) * ∑ i ∈ p.support.attach, f (p.coeff ↑i) * z ^ ↑i = f p.leadingCoeff ^ (p.natDegree - 1) * ∑ n ∈ p.support, f (p.coeff n) * z ^ n
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : CommSemiring S<VAR>p : R[X]<VAR>f : R →+* S<VAR>z : S<VAR>hz : eval₂ f z p = 0<VAR>inj : ∀ (x : R), f x = 0 → x = 0<GOAL>∑ i ∈ p.support.attach, f (p.coeff ↑i) * z ^ ↑i = ∑ n ∈ p.support, f (p.coeff n) * z ^ n
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : CommSemiring S<VAR>p : R[X]<VAR>f : R →+* S<VAR>z : S<VAR>hz : eval₂ f z p = 0<VAR>inj : ∀ (x : R), f x = 0 → x = 0<GOAL>f p.leadingCoeff ^ (p.natDegree - 1) * eval₂ f z p = 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{?u.23741, u_1} C<VAR>inst✝⁵ : Category.{?u.23745, u_2} D<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>ψ : LeftHomologyMapData φ h₁ h₂<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>inst✝¹ : h₁.IsPreservedBy F<VAR>inst✝ : h₂.IsPreservedBy F<GOAL>F.map ψ.φK ≫ (h₂.map F).i = (h₁.map F).i ≫ (F.mapShortComplex.map φ).τ₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{?u.23741, u_1} C<VAR>inst✝⁵ : Category.{?u.23745, u_2} D<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>ψ : LeftHomologyMapData φ h₁ h₂<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>inst✝¹ : h₁.IsPreservedBy F<VAR>inst✝ : h₂.IsPreservedBy F<GOAL>(h₁.map F).f' ≫ F.map ψ.φK = (F.mapShortComplex.map φ).τ₁ ≫ (h₂.map F).f'
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{?u.23741, u_1} C<VAR>inst✝⁵ : Category.{?u.23745, u_2} D<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>ψ : LeftHomologyMapData φ h₁ h₂<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>inst✝¹ : h₁.IsPreservedBy F<VAR>inst✝ : h₂.IsPreservedBy F<GOAL>(h₁.map F).π ≫ F.map ψ.φH = F.map ψ.φK ≫ (h₂.map F).π
<VAR>α : Sort u_1<VAR>inst✝ : IsEmpty α<VAR>f : α → ℝ<GOAL>sSup (Set.range fun i => f i) = 0
<VAR>α : Sort u_1<VAR>inst✝ : IsEmpty α<VAR>f : α → ℝ<GOAL>(Set.range fun i => f i) = ∅
<VAR>α : Sort u_1<VAR>inst✝ : IsEmpty α<VAR>f : α → ℝ<GOAL>IsEmpty α
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝² : NormedAddCommGroup V<VAR>inst✝¹ : NormedSpace ℝ V<VAR>inst✝ : FiniteDimensional ℝ V<VAR>s : Set V<VAR>hs : Convex ℝ s<GOAL>(intrinsicInterior ℝ s).Nonempty → s.Nonempty
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝² : NormedAddCommGroup V<VAR>inst✝¹ : NormedSpace ℝ V<VAR>inst✝ : FiniteDimensional ℝ V<VAR>s : Set V<VAR>hs : Convex ℝ s<GOAL>intrinsicInterior ℝ s ≠ ∅ → s ≠ ∅
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝² : NormedAddCommGroup V<VAR>inst✝¹ : NormedSpace ℝ V<VAR>inst✝ : FiniteDimensional ℝ V<VAR>hs : Convex ℝ ∅<VAR>h : intrinsicInterior ℝ ∅ ≠ ∅<GOAL>False
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u v w u' v' : V<VAR>p : G.Walk u' v'<GOAL>(p.copy ⋯ ⋯).IsTrail ↔ p.IsTrail
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q✝ f g q r : R[X]<VAR>hg : g.Monic<VAR>h : r + g * q = f ∧ r.degree < g.degree<VAR>a✝ : Nontrivial R<GOAL>f /ₘ g = q ∧ f %ₘ g = r
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q✝ f g q r : R[X]<VAR>hg : g.Monic<VAR>h : r + g * q = f ∧ r.degree < g.degree<VAR>a✝ : Nontrivial R<VAR>h₁ : r - f %ₘ g = -g * (q - f /ₘ g)<GOAL>f /ₘ g = q ∧ f %ₘ g = r
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q✝ f g q r : R[X]<VAR>hg : g.Monic<VAR>h : r + g * q = f ∧ r.degree < g.degree<VAR>a✝ : Nontrivial R<VAR>h₁ : r - f %ₘ g = -g * (q - f /ₘ g)<VAR>h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree<GOAL>f /ₘ g = q ∧ f %ₘ g = r
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q✝ f g q r : R[X]<VAR>hg : g.Monic<VAR>h : r + g * q = f ∧ r.degree < g.degree<VAR>a✝ : Nontrivial R<VAR>h₁ : r - f %ₘ g = -g * (q - f /ₘ g)<VAR>h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree<VAR>h₄ : (r - f %ₘ g).degree < g.degree<GOAL>f /ₘ g = q ∧ f %ₘ g = r
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q✝ f g q r : R[X]<VAR>hg : g.Monic<VAR>h : r + g * q = f ∧ r.degree < g.degree<VAR>a✝ : Nontrivial R<VAR>h₁ : r - f %ₘ g = -g * (q - f /ₘ g)<VAR>h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree<VAR>h₄ : (r - f %ₘ g).degree < g.degree<VAR>h₅ : q - f /ₘ g = 0<GOAL>f /ₘ g = q ∧ f %ₘ g = r
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>φ : R →+* S<GOAL>(map φ P).toPoly = Polynomial.map φ P.toPoly
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : NontriviallyNormedField α<VAR>x : α<GOAL>(𝓝[≠] x).NeBot
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : NontriviallyNormedField α<VAR>x : α<GOAL>∀ ε > 0, ∃ b ∈ {x}ᶜ, dist x b < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : NontriviallyNormedField α<VAR>x : α<VAR>ε : ℝ<VAR>ε0 : ε > 0<GOAL>∃ b ∈ {x}ᶜ, dist x b < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : NontriviallyNormedField α<VAR>x : α<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>b : α<VAR>hb0 : 0 < ‖b‖<VAR>hbε : ‖b‖ < ε<GOAL>∃ b ∈ {x}ᶜ, dist x b < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : NontriviallyNormedField α<VAR>x : α<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>b : α<VAR>hb0 : 0 < ‖b‖<VAR>hbε : ‖b‖ < ε<GOAL>dist x (x + b) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>a : α<VAR>l : List α<GOAL>Tendsto (fun p => p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a :: l))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>a : α<VAR>l : List α<GOAL>(Filter.map (fun a b => (a, b).1 :: (a, b).2) (𝓝 a)).seq (𝓝 l) ≤ Seq.seq (cons <$> 𝓝 a) fun x => 𝓝 l
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : CommRing R<VAR>a b : R<GOAL>(a - b) ^ 2 = a ^ 2 + b ^ 2 - 2 * a * b
<VAR>α : Type u_1<VAR>l : RBNode α<VAR>v : α<VAR>r : RBNode α<GOAL>(l.balance2 v r).reverse = r.reverse.balance1 v l.reverse
<VAR>α : Type u_1<VAR>l : RBNode α<VAR>v : α<VAR>r : RBNode α<GOAL>(l.balance2 v r).reverse = (r.reverse.balance1 v l.reverse).reverse.reverse
<VAR>α : Type u_1<VAR>l : RBNode α<VAR>v : α<VAR>r : RBNode α<GOAL>(l.balance2 v r).reverse = (l.reverse.reverse.balance2 v r.reverse.reverse).reverse
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : ℕ × α<VAR>n : ℕ<VAR>l : List α<VAR>h : x ∈ enumFrom n l<GOAL>x.1 < n + l.length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>l : List α<VAR>i : Fin (enumFrom n l).length<VAR>h : (enumFrom n l).get i ∈ enumFrom n l<GOAL>((enumFrom n l).get i).1 < n + l.length
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.225052, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>K : CochainComplex C ℤ<VAR>α : Cocycle K F 1<VAR>β : Cochain K G 0<VAR>eq : δ 0 1 β + (↑α).comp (Cochain.ofHom φ) ⋯ = 0<VAR>p q : ℤ<VAR>hpq : p + 1 = q<GOAL>(lift φ α β eq).f p = (↑α).v p q hpq ≫ (inl φ).v q p ⋯ + β.v p p ⋯ ≫ (inr φ).f p
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q U : Cᵒᵖ ⥤ Type w<VAR>X Y✝ : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>x : FamilyOfElements P R<VAR>t : P.obj (op X)<VAR>f : P ⟶ Q<VAR>h : x.IsAmalgamation t<VAR>Y : C<VAR>g : Y ⟶ X<VAR>hg : R g<GOAL>(f.app (op X) ≫ Q.map g.op) t = f.app (op Y) (x g hg)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : DecidableEq β<VAR>f g : α →. β<VAR>inst✝² : (x : α) → Decidable (f x).Dom<VAR>inst✝¹ : (x : α) → Decidable (g x).Dom<VAR>s t : Finset α<VAR>b : β<VAR>inst✝ : DecidableEq α<GOAL>↑(pimage f (s ∪ t)) = ↑(pimage f s ∪ pimage f t)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>D' : Type u_3<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_5, u_2} D<VAR>inst✝¹ : Category.{?u.12961, u_3} D'<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝ : L.IsLocalization W<VAR>X : C<VAR>P : StructuredArrow (L.obj X) L → Prop<VAR>hP₀ : P (StructuredArrow.mk (𝟙 (L.obj X)))<VAR>hP₁ : ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ L.map f))<VAR>hP₂ : ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom L W w hw).inv))<VAR>g : StructuredArrow (L.obj X) L<VAR>P' : StructuredArrow (W.Q.obj X) W.Q → Prop := fun g => P ((structuredArrowEquiv W W.Q L) g)<GOAL>P g
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>D' : Type u_3<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_5, u_2} D<VAR>inst✝¹ : Category.{?u.12961, u_3} D'<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝ : L.IsLocalization W<VAR>X : C<VAR>P : StructuredArrow (L.obj X) L → Prop<VAR>hP₀ : P (StructuredArrow.mk (𝟙 (L.obj X)))<VAR>hP₁ : ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ L.map f))<VAR>hP₂ : ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom L W w hw).inv))<VAR>g : StructuredArrow (L.obj X) L<VAR>P' : StructuredArrow (W.Q.obj X) W.Q → Prop := fun g => P ((structuredArrowEquiv W W.Q L) g)<GOAL>P ((structuredArrowEquiv W W.Q L) ((structuredArrowEquiv W W.Q L).symm g))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>D' : Type u_3<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_5, u_2} D<VAR>inst✝¹ : Category.{?u.12961, u_3} D'<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝ : L.IsLocalization W<VAR>X : C<VAR>P : StructuredArrow (L.obj X) L → Prop<VAR>hP₀ : P (StructuredArrow.mk (𝟙 (L.obj X)))<VAR>hP₁ : ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ L.map f))<VAR>hP₂ : ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom L W w hw).inv))<VAR>g : StructuredArrow (L.obj X) L<VAR>P' : StructuredArrow (W.Q.obj X) W.Q → Prop := fun g => P ((structuredArrowEquiv W W.Q L) g)<GOAL>P' (StructuredArrow.mk (𝟙 (W.Q.obj X)))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>D' : Type u_3<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_5, u_2} D<VAR>inst✝¹ : Category.{?u.12961, u_3} D'<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝ : L.IsLocalization W<VAR>X : C<VAR>P : StructuredArrow (L.obj X) L → Prop<VAR>hP₀ : P (StructuredArrow.mk (𝟙 (L.obj X)))<VAR>hP₁ : ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ L.map f))<VAR>hP₂ : ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom L W w hw).inv))<VAR>g : StructuredArrow (L.obj X) L<VAR>P' : StructuredArrow (W.Q.obj X) W.Q → Prop := fun g => P ((structuredArrowEquiv W W.Q L) g)<GOAL>∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁), P' (StructuredArrow.mk φ) → P' (StructuredArrow.mk (φ ≫ W.Q.map f))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>D' : Type u_3<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_5, u_2} D<VAR>inst✝¹ : Category.{?u.12961, u_3} D'<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝ : L.IsLocalization W<VAR>X : C<VAR>P : StructuredArrow (L.obj X) L → Prop<VAR>hP₀ : P (StructuredArrow.mk (𝟙 (L.obj X)))<VAR>hP₁ : ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ L.map f))<VAR>hP₂ : ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom L W w hw).inv))<VAR>g : StructuredArrow (L.obj X) L<VAR>P' : StructuredArrow (W.Q.obj X) W.Q → Prop := fun g => P ((structuredArrowEquiv W W.Q L) g)<GOAL>∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂), P' (StructuredArrow.mk φ) → P' (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
<VAR>α : Type u_1<VAR>𝒜 : Set (Set α)<VAR>s✝ t : Set α<VAR>ℬ : Set (Set α)<VAR>h : 𝒜 ⊆ ℬ<VAR>hℬ : IsSetAlgebra ℬ<VAR>s : Set α<VAR>hs : s ∈ generateSetAlgebra 𝒜<GOAL>s ∈ ℬ
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>m✝ : Set X → ℝ≥0∞<VAR>r✝ : ℝ≥0∞<VAR>μ : OuterMeasure X<VAR>s : Set X<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : OpensMeasurableSpace X<VAR>m : Set X → ℝ≥0∞<VAR>hcl : ∀ (s : Set X), m (closure s) = m s<VAR>r : ℝ≥0∞<GOAL>(pre m r).trim = pre m r
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>m✝ : Set X → ℝ≥0∞<VAR>r✝ : ℝ≥0∞<VAR>μ : OuterMeasure X<VAR>s✝ : Set X<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : OpensMeasurableSpace X<VAR>m : Set X → ℝ≥0∞<VAR>hcl : ∀ (s : Set X), m (closure s) = m s<VAR>r : ℝ≥0∞<VAR>s : Set X<VAR>hs : diam s ≤ r<GOAL>(pre m r).trim s ≤ m s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>m✝ : Set X → ℝ≥0∞<VAR>r✝ : ℝ≥0∞<VAR>μ : OuterMeasure X<VAR>s✝ : Set X<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : OpensMeasurableSpace X<VAR>m : Set X → ℝ≥0∞<VAR>hcl : ∀ (s : Set X), m (closure s) = m s<VAR>r : ℝ≥0∞<VAR>s : Set X<VAR>hs : diam s ≤ r<GOAL>⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (pre m r) t ≤ m s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>m✝ : Set X → ℝ≥0∞<VAR>r✝ : ℝ≥0∞<VAR>μ : OuterMeasure X<VAR>s✝ : Set X<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : OpensMeasurableSpace X<VAR>m : Set X → ℝ≥0∞<VAR>hcl : ∀ (s : Set X), m (closure s) = m s<VAR>r : ℝ≥0∞<VAR>s : Set X<VAR>hs : diam s ≤ r<GOAL>diam (closure s) ≤ r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f✝ : α → ℝ≥0∞<VAR>ι : Type u_3<VAR>inst✝¹ : Countable ι<VAR>inst✝ : LinearOrder ι<VAR>f : ι → α → ℝ≥0∞<GOAL>limsup (fun x => liminf (fun n => f n x) atTop) (ae μ) ≤ liminf (fun n => limsup (fun x => f n x) (ae μ)) atTop
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Category.{?u.2869, u_2} D<VAR>inst✝³ : ConcreteCategory D<VAR>inst✝² : FinitaryPreExtensive C<VAR>F G : Cᵒᵖ ⥤ Type w<VAR>f : F ⟶ G<VAR>inst✝¹ : PreservesFiniteProducts F<VAR>inst✝ : PreservesFiniteProducts G<VAR>h : Presheaf.IsLocallySurjective (extensiveTopology C) f<VAR>X : C<VAR>x : G.obj (op X)<GOAL>∃ a, f.app (op X) a = x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Category.{?u.2869, u_2} D<VAR>inst✝³ : ConcreteCategory D<VAR>inst✝² : FinitaryPreExtensive C<VAR>F G : Cᵒᵖ ⥤ Type w<VAR>f : F ⟶ G<VAR>inst✝¹ : PreservesFiniteProducts F<VAR>inst✝ : PreservesFiniteProducts G<VAR>X : C<VAR>x : G.obj (op X)<VAR>h : Presheaf.imageSieve f x ∈ (extensiveTopology C).sieves X<GOAL>∃ a, f.app (op X) a = x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Category.{?u.2869, u_2} D<VAR>inst✝³ : ConcreteCategory D<VAR>inst✝² : FinitaryPreExtensive C<VAR>F G : Cᵒᵖ ⥤ Type w<VAR>f : F ⟶ G<VAR>inst✝¹ : PreservesFiniteProducts F<VAR>inst✝ : PreservesFiniteProducts G<VAR>X : C<VAR>x : G.obj (op X)<VAR>h : ∃ α, ∃ (_ : Finite α), ∃ Y π, Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), (Presheaf.imageSieve f x).arrows (π a)<GOAL>∃ a, f.app (op X) a = x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Category.{?u.2869, u_2} D<VAR>inst✝³ : ConcreteCategory D<VAR>inst✝² : FinitaryPreExtensive C<VAR>F G : Cᵒᵖ ⥤ Type w<VAR>f : F ⟶ G<VAR>inst✝¹ : PreservesFiniteProducts F<VAR>inst✝ : PreservesFiniteProducts G<VAR>X : C<VAR>x : G.obj (op X)<VAR>α : Type<VAR>w✝ : Finite α<VAR>Y : α → C<VAR>π : (a : α) → Y a ⟶ X<VAR>h : Nonempty (IsColimit (Cofan.mk X π))<VAR>h' : ∀ (a : α), (Presheaf.imageSieve f x).arrows (π a)<VAR>y : (a : α) → F.obj (op (Y a)) := fun a => Exists.choose ⋯<VAR>x✝ : Fintype α := Fintype.ofFinite α<VAR>ht : IsLimit (Types.productLimitCone fun a => F.obj (op (Y a))).cone := (Types.productLimitCone fun a => F.obj (op (Y a))).isLimit<VAR>ht' : IsLimit (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))) := (Functor.Initial.isLimitWhiskerEquiv (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))).symm h.some.op<VAR>i : ((a : α) → F.obj (op (Y a))) ≅ F.obj (op X) := ht.conePointsIsoOfNatIso (isLimitOfPreserves F ht') (Discrete.natIso fun x => Iso.refl (F.obj (op (Y x.as))))<GOAL>f.app (op X) (i.hom y) = x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Category.{?u.2869, u_2} D<VAR>inst✝³ : ConcreteCategory D<VAR>inst✝² : FinitaryPreExtensive C<VAR>F G : Cᵒᵖ ⥤ Type w<VAR>f : F ⟶ G<VAR>inst✝¹ : PreservesFiniteProducts F<VAR>inst✝ : PreservesFiniteProducts G<VAR>X : C<VAR>x : G.obj (op X)<VAR>α : Type<VAR>w✝ : Finite α<VAR>Y : α → C<VAR>π : (a : α) → Y a ⟶ X<VAR>h : Nonempty (IsColimit (Cofan.mk X π))<VAR>h' : ∀ (a : α), (Presheaf.imageSieve f x).arrows (π a)<VAR>y : (a : α) → F.obj (op (Y a)) := fun a => Exists.choose ⋯<VAR>x✝ : Fintype α := Fintype.ofFinite α<VAR>ht : IsLimit (Types.productLimitCone fun a => F.obj (op (Y a))).cone := (Types.productLimitCone fun a => F.obj (op (Y a))).isLimit<VAR>ht' : IsLimit (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))) := (Functor.Initial.isLimitWhiskerEquiv (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))).symm h.some.op<VAR>i : ((a : α) → F.obj (op (Y a))) ≅ F.obj (op X) := ht.conePointsIsoOfNatIso (isLimitOfPreserves F ht') (Discrete.natIso fun x => Iso.refl (F.obj (op (Y x.as))))<GOAL>∀ (j : Discrete α), ((G.mapCone (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π)))).π.app j) (f.app (op X) (i.hom y)) = ((G.mapCone (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π)))).π.app j) x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Category.{?u.2869, u_2} D<VAR>inst✝³ : ConcreteCategory D<VAR>inst✝² : FinitaryPreExtensive C<VAR>F G : Cᵒᵖ ⥤ Type w<VAR>f : F ⟶ G<VAR>inst✝¹ : PreservesFiniteProducts F<VAR>inst✝ : PreservesFiniteProducts G<VAR>X : C<VAR>x : G.obj (op X)<VAR>α : Type<VAR>w✝ : Finite α<VAR>Y : α → C<VAR>π : (a : α) → Y a ⟶ X<VAR>h : Nonempty (IsColimit (Cofan.mk X π))<VAR>h' : ∀ (a : α), (Presheaf.imageSieve f x).arrows (π a)<VAR>y : (a : α) → F.obj (op (Y a)) := fun a => Exists.choose ⋯<VAR>x✝ : Fintype α := Fintype.ofFinite α<VAR>ht : IsLimit (Types.productLimitCone fun a => F.obj (op (Y a))).cone := (Types.productLimitCone fun a => F.obj (op (Y a))).isLimit<VAR>ht' : IsLimit (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))) := (Functor.Initial.isLimitWhiskerEquiv (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))).symm h.some.op<VAR>i : ((a : α) → F.obj (op (Y a))) ≅ F.obj (op X) := ht.conePointsIsoOfNatIso (isLimitOfPreserves F ht') (Discrete.natIso fun x => Iso.refl (F.obj (op (Y x.as))))<VAR>a : α<GOAL>((G.mapCone (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π)))).π.app { as := a }) (f.app (op X) (i.hom y)) = ((G.mapCone (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π)))).π.app { as := a }) x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Category.{?u.2869, u_2} D<VAR>inst✝³ : ConcreteCategory D<VAR>inst✝² : FinitaryPreExtensive C<VAR>F G : Cᵒᵖ ⥤ Type w<VAR>f : F ⟶ G<VAR>inst✝¹ : PreservesFiniteProducts F<VAR>inst✝ : PreservesFiniteProducts G<VAR>X : C<VAR>x : G.obj (op X)<VAR>α : Type<VAR>w✝ : Finite α<VAR>Y : α → C<VAR>π : (a : α) → Y a ⟶ X<VAR>h : Nonempty (IsColimit (Cofan.mk X π))<VAR>h' : ∀ (a : α), (Presheaf.imageSieve f x).arrows (π a)<VAR>y : (a : α) → F.obj (op (Y a)) := fun a => Exists.choose ⋯<VAR>x✝ : Fintype α := Fintype.ofFinite α<VAR>ht : IsLimit (Types.productLimitCone fun a => F.obj (op (Y a))).cone := (Types.productLimitCone fun a => F.obj (op (Y a))).isLimit<VAR>ht' : IsLimit (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))) := (Functor.Initial.isLimitWhiskerEquiv (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))).symm h.some.op<VAR>i : ((a : α) → F.obj (op (Y a))) ≅ F.obj (op X) := ht.conePointsIsoOfNatIso (isLimitOfPreserves F ht') (Discrete.natIso fun x => Iso.refl (F.obj (op (Y x.as))))<VAR>a : α<GOAL>(G.map (π a).op) (f.app (op X) (i.hom y)) = (G.map (π a).op) x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Category.{?u.2869, u_2} D<VAR>inst✝³ : ConcreteCategory D<VAR>inst✝² : FinitaryPreExtensive C<VAR>F G : Cᵒᵖ ⥤ Type w<VAR>f : F ⟶ G<VAR>inst✝¹ : PreservesFiniteProducts F<VAR>inst✝ : PreservesFiniteProducts G<VAR>X : C<VAR>x : G.obj (op X)<VAR>α : Type<VAR>w✝ : Finite α<VAR>Y : α → C<VAR>π : (a : α) → Y a ⟶ X<VAR>h : Nonempty (IsColimit (Cofan.mk X π))<VAR>h' : ∀ (a : α), (Presheaf.imageSieve f x).arrows (π a)<VAR>y : (a : α) → F.obj (op (Y a)) := fun a => Exists.choose ⋯<VAR>x✝ : Fintype α := Fintype.ofFinite α<VAR>ht : IsLimit (Types.productLimitCone fun a => F.obj (op (Y a))).cone := (Types.productLimitCone fun a => F.obj (op (Y a))).isLimit<VAR>ht' : IsLimit (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))) := (Functor.Initial.isLimitWhiskerEquiv (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))).symm h.some.op<VAR>i : ((a : α) → F.obj (op (Y a))) ≅ F.obj (op X) := ht.conePointsIsoOfNatIso (isLimitOfPreserves F ht') (Discrete.natIso fun x => Iso.refl (F.obj (op (Y x.as))))<VAR>a : α<VAR>this : f.app (op (Y a)) (y a) = G.map (π a).op x<GOAL>(G.map (π a).op) (f.app (op X) (i.hom y)) = (G.map (π a).op) x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Category.{?u.2869, u_2} D<VAR>inst✝³ : ConcreteCategory D<VAR>inst✝² : FinitaryPreExtensive C<VAR>F G : Cᵒᵖ ⥤ Type w<VAR>f : F ⟶ G<VAR>inst✝¹ : PreservesFiniteProducts F<VAR>inst✝ : PreservesFiniteProducts G<VAR>X : C<VAR>x : G.obj (op X)<VAR>α : Type<VAR>w✝ : Finite α<VAR>Y : α → C<VAR>π : (a : α) → Y a ⟶ X<VAR>h : Nonempty (IsColimit (Cofan.mk X π))<VAR>h' : ∀ (a : α), (Presheaf.imageSieve f x).arrows (π a)<VAR>y : (a : α) → F.obj (op (Y a)) := fun a => Exists.choose ⋯<VAR>x✝ : Fintype α := Fintype.ofFinite α<VAR>ht : IsLimit (Types.productLimitCone fun a => F.obj (op (Y a))).cone := (Types.productLimitCone fun a => F.obj (op (Y a))).isLimit<VAR>ht' : IsLimit (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))) := (Functor.Initial.isLimitWhiskerEquiv (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))).symm h.some.op<VAR>i : ((a : α) → F.obj (op (Y a))) ≅ F.obj (op X) := ht.conePointsIsoOfNatIso (isLimitOfPreserves F ht') (Discrete.natIso fun x => Iso.refl (F.obj (op (Y x.as))))<VAR>a : α<VAR>this : f.app (op (Y a)) (y a) = G.map (π a).op x<GOAL>(G.map (π a).op) (f.app (op X) (i.hom y)) = G.map (π a).op x