ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝¹⁰ : MetricSpace α<VAR>β : Type u<VAR>inst✝⁹ : SecondCountableTopology α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : OpensMeasurableSpace α<VAR>inst✝⁶ : HasBesicovitchCovering α<VAR>inst✝⁵ : MetricSpace β<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : BorelSpace β<VAR>inst✝² : SecondCountableTopology β<VAR>inst✝¹ : HasBesicovitchCovering β<VAR>μ : Measure β<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∀ (a : β), Tendsto (fun a => μ (s ∩ a) / μ a) ((Besicovitch.vitaliFamily μ).filterAt a) (𝓝 (s.indicator 1 a)) → Tendsto (fun r => μ (s ∩ closedBall a r) / μ (closedBall a r)) (𝓝[>] 0) (𝓝 (s.indicator 1 a))
<VAR>α : Type u_1<VAR>inst✝¹⁰ : MetricSpace α<VAR>β : Type u<VAR>inst✝⁹ : SecondCountableTopology α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : OpensMeasurableSpace α<VAR>inst✝⁶ : HasBesicovitchCovering α<VAR>inst✝⁵ : MetricSpace β<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : BorelSpace β<VAR>inst✝² : SecondCountableTopology β<VAR>inst✝¹ : HasBesicovitchCovering β<VAR>μ : Measure β<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>x : β<VAR>hx : Tendsto (fun a => μ (s ∩ a) / μ a) ((Besicovitch.vitaliFamily μ).filterAt x) (𝓝 (s.indicator 1 x))<GOAL>Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 (s.indicator 1 x))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>P : Presentation R S<VAR>r : R<VAR>inst✝ : IsLocalization.Away r S<GOAL>(localizationAway r).dimension = 0
<VAR>c : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ c<GOAL>c + 1 = c
<VAR>c : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ c<GOAL>ω ≤ c.ord
<VAR>C : Type uC<VAR>inst✝¹ : Category.{uC', uC} C<VAR>W : MorphismProperty C<VAR>D : Type uD<VAR>inst✝ : Category.{uD', uD} D<VAR>G : C ⥤ D<VAR>hG : W.IsInvertedBy G<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(W.Q ⋙ lift G hG).map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
<VAR>C : Type uC<VAR>inst✝¹ : Category.{uC', uC} C<VAR>W : MorphismProperty C<VAR>D : Type uD<VAR>inst✝ : Category.{uD', uD} D<VAR>G : C ⥤ D<VAR>hG : W.IsInvertedBy G<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(lift G hG).map (W.Q.map f) = G.map f
<VAR>C : Type uC<VAR>inst✝¹ : Category.{uC', uC} C<VAR>W : MorphismProperty C<VAR>D : Type uD<VAR>inst✝ : Category.{uD', uD} D<VAR>G : C ⥤ D<VAR>hG : W.IsInvertedBy G<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>composePath (G.map f).toPath = G.map f
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>a✝ : α<VAR>b✝ : β<VAR>s : Multiset α<VAR>t : Multiset β<VAR>a : α<VAR>b : β<GOAL>(a, b) ∈ s.product t ↔ (a, b).1 ∈ s ∧ (a, b).2 ∈ t
<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>n : ℕ<VAR>f : Fin n.succ → α<GOAL>(ofFn f).head = f 0
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>v : ℝ → E → E<VAR>tMin t₀ tMax : ℝ<VAR>x₀ : E<VAR>C R : ℝ<VAR>L : ℝ≥0<VAR>hpl : IsPicardLindelof v tMin t₀ tMax x₀ L R C<GOAL>∃ f, f t₀ = x₀ ∧ ∀ t ∈ Icc tMin tMax, HasDerivWithinAt f (v t (f t)) (Icc tMin tMax) t
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>v : ℝ → E → E<VAR>tMin t₀ tMax : ℝ<VAR>x₀ : E<VAR>R : ℝ<VAR>L C : ℝ≥0<VAR>hpl : IsPicardLindelof v tMin t₀ tMax x₀ L R ↑C<GOAL>∃ f, f t₀ = x₀ ∧ ∀ t ∈ Icc tMin tMax, HasDerivWithinAt f (v t (f t)) (Icc tMin tMax) t
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>v : ℝ → E → E<VAR>tMin tMax : ℝ<VAR>x₀ : E<VAR>R : ℝ<VAR>L C : ℝ≥0<VAR>t₀ : { x // x ∈ Icc tMin tMax }<VAR>hpl : IsPicardLindelof v tMin (↑t₀) tMax x₀ L R ↑C<GOAL>∃ f, f ↑t₀ = x₀ ∧ ∀ t ∈ Icc tMin tMax, HasDerivWithinAt f (v t (f t)) (Icc tMin tMax) t
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>f : v.FunSpace<VAR>t : ↑(Icc v.tMin v.tMax)<GOAL>dist (f.toFun t) v.x₀ = dist (f.toFun t) (f.toFun v.t₀)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : LocallyRingedSpace<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : IsOpenImmersion f<VAR>H' : Set.range ⇑g.val.base ⊆ Set.range ⇑f.val.base<GOAL>lift f g H' ≫ f = g
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : LocallyRingedSpace<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : IsOpenImmersion f<VAR>H' : Set.range ⇑g.val.base ⊆ Set.range ⇑f.val.base<GOAL>inv (pullback.snd f g) ≫ pullback.fst f g ≫ f = g
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : LocallyRingedSpace<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : IsOpenImmersion f<VAR>H' : Set.range ⇑g.val.base ⊆ Set.range ⇑f.val.base<GOAL>pullback.fst f g ≫ f = pullback.snd f g ≫ g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : Set (β → γ)<VAR>t : Set (α → β)<VAR>u : Set α<GOAL>s.seq (t.seq u) = (((fun x x_1 => x ∘ x_1) '' s).seq t).seq u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : Set (β → γ)<VAR>t : Set (α → β)<VAR>u : Set α<GOAL>image2 (fun f a => f a) s (image2 (fun f a => f a) t u) = image2 (fun f a => f a) (image2 (fun x x_1 => x ∘ x_1) s t) u
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>this : 1 ≤ a * a<GOAL>↑(Pell.d a1) = az a * az a - 1
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>this : 1 ≤ a * a<GOAL>↑(a * a) - ↑1 = az a * az a - 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : StarMul R<VAR>inst✝⁵ : TrivialStar R<VAR>inst✝⁴ : AddCommGroup A<VAR>inst✝³ : Module R A<VAR>inst✝² : StarAddMonoid A<VAR>inst✝¹ : StarModule R A<VAR>inst✝ : Invertible 2<VAR>x : A<VAR>hx : IsSelfAdjoint x<GOAL>↑((selfAdjointPart R) x) = x
<VAR>E : Type u_1<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : FiniteDimensional ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>L : AddSubgroup E<VAR>inst✝⁴ : DiscreteTopology ↥L<VAR>inst✝³ : IsZlattice ℝ L<VAR>μ : autoParam (Measure E) _auto✝<VAR>inst✝² : Measure.IsAddHaarMeasure μ<VAR>ι : Type u_2<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι ℤ ↥L<VAR>b₀ : Basis ι ℝ E<GOAL>covolume L μ = |b₀.det (Subtype.val ∘ ⇑b)| * (μ (Zspan.fundamentalDomain b₀)).toReal
<VAR>E : Type u_1<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : FiniteDimensional ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>L : AddSubgroup E<VAR>inst✝⁴ : DiscreteTopology ↥L<VAR>inst✝³ : IsZlattice ℝ L<VAR>μ : autoParam (Measure E) _auto✝<VAR>inst✝² : Measure.IsAddHaarMeasure μ<VAR>ι : Type u_2<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι ℤ ↥L<VAR>b₀ : Basis ι ℝ E<GOAL>|b₀.det ⇑(Basis.ofZlatticeBasis ℝ L b)| * (μ (parallelepiped ⇑b₀)).toReal = |b₀.det (Subtype.val ∘ ⇑b)| * (μ (parallelepiped ⇑b₀)).toReal
<VAR>E : Type u_1<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : FiniteDimensional ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>L : AddSubgroup E<VAR>inst✝⁴ : DiscreteTopology ↥L<VAR>inst✝³ : IsZlattice ℝ L<VAR>μ : autoParam (Measure E) _auto✝<VAR>inst✝² : Measure.IsAddHaarMeasure μ<VAR>ι : Type u_2<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι ℤ ↥L<VAR>b₀ : Basis ι ℝ E<VAR>x✝ : ι<GOAL>(Basis.ofZlatticeBasis ℝ L b) x✝ = (Subtype.val ∘ ⇑b) x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : DecidableEq α<VAR>s✝ t : Finset α<VAR>x : α × α<VAR>a : α<VAR>ι : Type u_4<VAR>inst✝³ : PartialOrder ι<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : DecidableRel LE.le<VAR>inst✝ : DecidableRel LT.lt<VAR>s : Finset ι<GOAL>filter (fun i => i.1 < i.2) s.offDiag = filter (fun i => i.1 ≤ i.2) s.offDiag
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : DecidableEq α<VAR>s✝ t : Finset α<VAR>x : α × α<VAR>a : α<VAR>ι : Type u_4<VAR>inst✝³ : PartialOrder ι<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : DecidableRel LE.le<VAR>inst✝ : DecidableRel LT.lt<VAR>s : Finset ι<GOAL>∀ ⦃a : ι × ι⦄, a ∈ s.offDiag → (a.1 < a.2 ↔ a.1 ≤ a.2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : DecidableEq α<VAR>s✝ t : Finset α<VAR>x : α × α<VAR>a : α<VAR>ι : Type u_4<VAR>inst✝³ : PartialOrder ι<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : DecidableRel LE.le<VAR>inst✝ : DecidableRel LT.lt<VAR>s : Finset ι<VAR>i j : ι<GOAL>(i, j) ∈ s.offDiag → ((i, j).1 < (i, j).2 ↔ (i, j).1 ≤ (i, j).2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : DecidableEq α<VAR>s✝ t : Finset α<VAR>x : α × α<VAR>a : α<VAR>ι : Type u_4<VAR>inst✝³ : PartialOrder ι<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : DecidableRel LE.le<VAR>inst✝ : DecidableRel LT.lt<VAR>s : Finset ι<VAR>i j : ι<GOAL>i ∈ s → j ∈ s → i ≠ j → (i < j ↔ i ≤ j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : DecidableEq α<VAR>s✝ t : Finset α<VAR>x : α × α<VAR>a : α<VAR>ι : Type u_4<VAR>inst✝³ : PartialOrder ι<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : DecidableRel LE.le<VAR>inst✝ : DecidableRel LT.lt<VAR>s : Finset ι<VAR>i j : ι<VAR>a✝¹ : i ∈ s<VAR>a✝ : j ∈ s<VAR>h : i ≠ j<GOAL>i < j ↔ i ≤ j
<VAR>a b : Bool<GOAL>(a != b) = xor a b
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_6, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_7, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.106010, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{u_5, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X : Cᵒᵖ<GOAL>(whiskerLeft G.op (sheafHom α)).app X = α.app X
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_6, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_7, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.106010, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{u_5, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X : Cᵒᵖ<GOAL>yoneda.map ((whiskerLeft G.op (sheafHom α)).app X) = yoneda.map (α.app X)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_6, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_7, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.106010, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{u_5, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X : Cᵒᵖ<VAR>U : Aᵒᵖ<VAR>a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U<GOAL>(yoneda.map ((whiskerLeft G.op (sheafHom α)).app X)).app U a✝ = (yoneda.map (α.app X)).app U a✝
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_6, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_7, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.106010, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{u_5, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X : Cᵒᵖ<VAR>U : Aᵒᵖ<VAR>a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U<GOAL>((sheafYonedaHom α).app (G.op.obj X)).app U a✝ = (yoneda.map (α.app X)).app U a✝
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_6, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_7, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.106010, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{u_5, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X : Cᵒᵖ<VAR>U : Aᵒᵖ<VAR>a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U<GOAL>(let_fun this := (yoneda.map (α.app X)).app U a✝; this) = ((sheafYonedaHom α).app (G.op.obj X)).app U a✝
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_6, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_7, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.106010, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{u_5, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X : Cᵒᵖ<VAR>U : Aᵒᵖ<VAR>a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U<GOAL>(pushforwardFamily (homOver α (unop U)) a✝).Compatible
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_6, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_7, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.106010, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{u_5, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X : Cᵒᵖ<VAR>U : Aᵒᵖ<VAR>a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U<GOAL>(pushforwardFamily (homOver α (unop U)) a✝).IsAmalgamation (let_fun this := (yoneda.map (α.app X)).app U a✝; this)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_6, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_7, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.106010, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{u_5, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X : Cᵒᵖ<VAR>U : Aᵒᵖ<VAR>a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U<VAR>Y : D<VAR>f : Y ⟶ G.obj (unop X)<VAR>hf : (Sieve.coverByImage G (G.obj (unop X))).arrows f<GOAL>(ℱ'.val ⋙ coyoneda.obj (op (unop U))).map f.op (let_fun this := (yoneda.map (α.app X)).app U a✝; this) = pushforwardFamily (homOver α (unop U)) a✝ f hf
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_6, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_7, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.106010, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{u_5, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X : Cᵒᵖ<VAR>U : Aᵒᵖ<VAR>a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U<VAR>Y : D<VAR>f : Y ⟶ G.obj (unop X)<VAR>hf : (Sieve.coverByImage G (G.obj (unop X))).arrows f<GOAL>(ℱ'.val ⋙ coyoneda.obj (op (unop U))).map ((Nonempty.some hf).lift ≫ (Nonempty.some hf).map).op (let_fun this := (yoneda.map (α.app X)).app U a✝; this) = pushforwardFamily (homOver α (unop U)) a✝ f hf
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_6, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_7, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.106010, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{u_5, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X : Cᵒᵖ<VAR>U : Aᵒᵖ<VAR>a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U<VAR>Y : D<VAR>f : Y ⟶ G.obj (unop X)<VAR>hf : (Sieve.coverByImage G (G.obj (unop X))).arrows f<GOAL>((a✝ ≫ α.app X) ≫ ℱ'.val.map (Nonempty.some hf).map.op) ≫ ℱ'.val.map (Nonempty.some hf).lift.op = (sheafOver ℱ' (unop U)).val.map (Nonempty.some hf).lift.op ((a✝ ≫ ℱ.map (Nonempty.some hf).map.op) ≫ α.app (op (Nonempty.some hf).1))
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_6, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_7, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.106010, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{u_5, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X : Cᵒᵖ<VAR>U : Aᵒᵖ<VAR>a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U<VAR>Y : D<VAR>f : Y ⟶ G.obj (unop X)<VAR>hf : (Sieve.coverByImage G (G.obj (unop X))).arrows f<GOAL>(a✝ ≫ α.app X) ≫ ℱ'.val.map (Nonempty.some hf).map.op = (a✝ ≫ ℱ.map (Nonempty.some hf).map.op) ≫ α.app (op (Nonempty.some hf).1)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_6, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_7, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.106010, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{u_5, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X : Cᵒᵖ<VAR>U : Aᵒᵖ<VAR>a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U<VAR>Y : D<VAR>f : Y ⟶ G.obj (unop X)<VAR>hf : (Sieve.coverByImage G (G.obj (unop X))).arrows f<GOAL>a✝ ≫ α.app X ≫ ℱ'.val.map (Nonempty.some hf).map.op = a✝ ≫ ℱ.map (Nonempty.some hf).map.op ≫ α.app (op (Nonempty.some hf).1)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_6, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_7, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.106010, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{u_5, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X : Cᵒᵖ<VAR>U : Aᵒᵖ<VAR>a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U<VAR>Y : D<VAR>f : Y ⟶ G.obj (unop X)<VAR>hf : (Sieve.coverByImage G (G.obj (unop X))).arrows f<GOAL>α.app X ≫ ℱ'.val.map (Nonempty.some hf).map.op = ℱ.map (Nonempty.some hf).map.op ≫ α.app (op (Nonempty.some hf).1)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_6, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_7, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.106010, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{u_5, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X : Cᵒᵖ<VAR>U : Aᵒᵖ<VAR>a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U<VAR>Y : D<VAR>f : Y ⟶ G.obj (unop X)<VAR>hf : (Sieve.coverByImage G (G.obj (unop X))).arrows f<VAR>this : { val := ℱ'.val ⋙ coyoneda.obj (op ((G.op ⋙ ℱ).obj X)), cond := ⋯ }.val.map (Nonempty.some hf).map.op ((whiskerRight α (coyoneda.obj (op ((G.op ⋙ ℱ).obj X)))).app (op (unop X)) (𝟙 (unop (op ((G.op ⋙ ℱ).obj X))))) = (whiskerRight α (coyoneda.obj (op ((G.op ⋙ ℱ).obj X)))).app (op (Nonempty.some hf).obj) ((ℱ ⋙ coyoneda.obj (op ((G.op ⋙ ℱ).obj X))).map (Nonempty.some hf).map.op (𝟙 (unop (op ((G.op ⋙ ℱ).obj X)))))<GOAL>α.app X ≫ ℱ'.val.map (Nonempty.some hf).map.op = ℱ.map (Nonempty.some hf).map.op ≫ α.app (op (Nonempty.some hf).1)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>p₁ p₂ p₃ : P<VAR>h : p₁ ∈ affineSpan k {p₂, p₃}<GOAL>Collinear k {p₁, p₂, p₃}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>p₁ p₂ p₃ : P<VAR>h : p₁ ∈ affineSpan k {p₂, p₃}<GOAL>Collinear k {p₂, p₃}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>hs : Convex ℝ s<VAR>absorbs : Absorbent ℝ s<VAR>x y : E<GOAL>gauge s (x + y) ≤ gauge s x + gauge s y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>hs : Convex ℝ s<VAR>absorbs : Absorbent ℝ s<VAR>x y : E<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>gauge s (x + y) < gauge s x + gauge s y + ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x✝ : E<VAR>a✝ : ℝ<VAR>hs : Convex ℝ s<VAR>absorbs : Absorbent ℝ s<VAR>y : E<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>a : ℝ<VAR>ha : 0 < a<VAR>x : E<VAR>hx : x ∈ s<VAR>ha' : a < gauge s ((fun x => a • x) x) + ε / 2<GOAL>gauge s ((fun x => a • x) x + y) < gauge s ((fun x => a • x) x) + gauge s y + ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x✝ : E<VAR>a✝ : ℝ<VAR>hs : Convex ℝ s<VAR>absorbs : Absorbent ℝ s<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>a : ℝ<VAR>ha : 0 < a<VAR>x : E<VAR>hx : x ∈ s<VAR>ha' : a < gauge s ((fun x => a • x) x) + ε / 2<VAR>b : ℝ<VAR>hb : 0 < b<VAR>y : E<VAR>hy : y ∈ s<VAR>hb' : b < gauge s ((fun x => b • x) y) + ε / 2<GOAL>gauge s ((fun x => a • x) x + (fun x => b • x) y) < gauge s ((fun x => a • x) x) + gauge s ((fun x => b • x) y) + ε
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s✝ : Finset α<VAR>H : s✝.Nonempty<VAR>x : α<VAR>s : Finset αᵒᵈ<VAR>hs : s.Nonempty<GOAL>ofDual (s.min' hs) = (image (⇑ofDual) s).max' ⋯
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s✝ : Finset α<VAR>H : s✝.Nonempty<VAR>x : α<VAR>s : Finset αᵒᵈ<VAR>hs : s.Nonempty<GOAL>↑(ofDual (s.min' hs)) = ↑((image (⇑ofDual) s).max' ⋯)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s✝ : Finset α<VAR>H : s✝.Nonempty<VAR>x : α<VAR>s : Finset αᵒᵈ<VAR>hs : s.Nonempty<GOAL>s.sup (WithBot.some ∘ fun x => ofDual x) = s.sup ((WithBot.some ∘ fun x => x) ∘ ⇑ofDual)
<VAR>α : Type u_1<VAR>inst✝⁵ : AddCommSemigroup α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>hac : AddLECancellable (a - c)<VAR>h : c ≤ a<GOAL>a + b = b + c + (a - c)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<GOAL>C a = a • 1
<VAR>α : Type u_1<VAR>inst✝⁵ : AddCommSemigroup α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>h : c ≤ b<VAR>h2 : a - c < b - c<GOAL>a < b
<VAR>α : Type u_1<VAR>inst✝⁵ : AddCommSemigroup α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>h : c ≤ b<VAR>h2 : a - c < b - c<GOAL>a ≠ b
<VAR>α : Type u_1<VAR>inst✝⁵ : AddCommSemigroup α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a c d : α<VAR>h : c ≤ a<VAR>h2 : a - c < a - c<GOAL>False
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s1 s2 : AffineSubspace k P<VAR>hd : s1.direction = s2.direction<VAR>hn : (↑s1 ∩ ↑s2).Nonempty<VAR>p : P<GOAL>p ∈ s1 ↔ p ∈ s2
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s1 s2 : AffineSubspace k P<VAR>hd : s1.direction = s2.direction<VAR>hn : (↑s1 ∩ ↑s2).Nonempty<VAR>p : P<VAR>hq1 : hn.some ∈ ↑s1<GOAL>p ∈ s1 ↔ p ∈ s2
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s1 s2 : AffineSubspace k P<VAR>hd : s1.direction = s2.direction<VAR>hn : (↑s1 ∩ ↑s2).Nonempty<VAR>p : P<VAR>hq1 : hn.some ∈ ↑s1<VAR>hq2 : hn.some ∈ ↑s2<GOAL>p ∈ s1 ↔ p ∈ s2