ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CommMonoid M<VAR>f : α → M<VAR>a✝ b : α<VAR>inst✝ : LocallyFiniteOrderTop α<VAR>a : α<GOAL>f a * ∏ x ∈ Ioi a, f x = ∏ x ∈ Ici a, f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<GOAL>∀ᵐ (a : α) ∂ρ.fst, Monotone fun r => preCDF ρ r a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<GOAL>∀ (i i_1 : ℚ), i ≤ i_1 → ∀ᵐ (a : α) ∂ρ.fst, preCDF ρ i a ≤ preCDF ρ i_1 a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>r r' : ℚ<VAR>hrr' : r ≤ r'<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>x✝ : ρ.fst s < ⊤<GOAL>∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst ≤ ∫⁻ (x : α) in s, preCDF ρ r' x ∂ρ.fst
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>r r' : ℚ<VAR>hrr' : r ≤ r'<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>x✝ : ρ.fst s < ⊤<GOAL>(ρ.IicSnd ↑r) s ≤ (ρ.IicSnd ↑r') s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>x✝ x : α<VAR>xs : List α<GOAL>(x :: xs).formPerm ((x :: xs).get ⟨xs.length, ⋯⟩) = x
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.31752, u_1} C<VAR>X Y : PresheafedSpace C<VAR>H : ↑X ≅ ↑Y<VAR>α : (Presheaf.pushforward C H.hom).obj X.presheaf ≅ Y.presheaf<VAR>U✝ : Opens ↑↑Y<GOAL>(α.inv.app (op U✝) ≫ (Presheaf.toPushforwardOfIso H α.hom).app (op ((Opens.map H.hom).obj U✝))) ≫ Y.presheaf.map ((eqToHom ⋯).app (op U✝)) = (𝟙 Y).c.app (op U✝)
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.31752, u_1} C<VAR>X Y : PresheafedSpace C<VAR>H : ↑X ≅ ↑Y<VAR>α : (Presheaf.pushforward C H.hom).obj X.presheaf ≅ Y.presheaf<VAR>U✝ : Opens ↑↑Y<GOAL>α.inv.app (op U✝) ≫ X.presheaf.map (eqToHom ⋯) ≫ ((Presheaf.pushforward C H.hom).obj X.presheaf).map ((eqToHom ⋯).app (op U✝)) ≫ α.hom.app (op ((Opens.map (𝟙 ↑Y)).obj U✝)) = (𝟙 Y).c.app (op U✝)
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.31752, u_1} C<VAR>X Y : PresheafedSpace C<VAR>H : ↑X ≅ ↑Y<VAR>α : (Presheaf.pushforward C H.hom).obj X.presheaf ≅ Y.presheaf<VAR>U✝ : Opens ↑↑Y<GOAL>α.inv.app (op U✝) ≫ α.hom.app (op ((Opens.map (𝟙 ↑Y)).obj U✝)) = (𝟙 Y).c.app (op U✝)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousSMul 𝕜 E<VAR>inst✝ : TopologicalAddGroup E<VAR>s t : Set E<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<GOAL>IsVonNBounded 𝕜 (s - t) ↔ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : C<VAR>α : X ≅ Y<GOAL>(α ≪≫ refl Y).hom = α.hom
<VAR>a x✝ z x : ℂ<VAR>hi : x.im < 0<GOAL>(-x).arg = x.arg + π
<VAR>a x✝ z x : ℂ<VAR>hi : x.im < 0<GOAL>Real.arccos ((-x).re / abs (-x)) = -Real.arccos (x.re / abs x) + π
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>f : L.Functions 2<VAR>t₁ t₂ : L.Term α<VAR>v : α → M<GOAL>(funMap f fun i => realize v (![t₁, t₂] i)) = funMap f ![realize v t₁, realize v t₂]
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>f : L.Functions 2<VAR>t₁ t₂ : L.Term α<VAR>v : α → M<GOAL>realize v (![t₁, t₂] 0) = ![realize v t₁, realize v t₂] 0
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>f : L.Functions 2<VAR>t₁ t₂ : L.Term α<VAR>v : α → M<GOAL>∀ (i : Fin 1), realize v (![t₁, t₂] i.succ) = ![realize v t₁, realize v t₂] i.succ
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s✝ : Set α<VAR>inst✝ : TopologicalSpace β<VAR>F : ι → β → α<VAR>f : β → α<VAR>p : Filter ι<VAR>s : Set β<GOAL>TendstoLocallyUniformlyOn F f p s ↔ ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, dist (f y) (F n y) < ε
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x✝ y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s✝ : Set α<VAR>inst✝ : TopologicalSpace β<VAR>F : ι → β → α<VAR>f : β → α<VAR>p : Filter ι<VAR>s : Set β<VAR>H : ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, dist (f y) (F n y) < ε<VAR>u : Set (α × α)<VAR>hu : u ∈ 𝓤 α<VAR>x : β<VAR>hx : x ∈ s<GOAL>∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x✝ y z : α<VAR>δ ε✝ ε₁ ε₂ : ℝ<VAR>s✝ : Set α<VAR>inst✝ : TopologicalSpace β<VAR>F : ι → β → α<VAR>f : β → α<VAR>p : Filter ι<VAR>s : Set β<VAR>H : ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, dist (f y) (F n y) < ε<VAR>u : Set (α × α)<VAR>hu : u ∈ 𝓤 α<VAR>x : β<VAR>hx : x ∈ s<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ u<GOAL>∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x✝ y z : α<VAR>δ ε✝ ε₁ ε₂ : ℝ<VAR>s✝ : Set α<VAR>inst✝ : TopologicalSpace β<VAR>F : ι → β → α<VAR>f : β → α<VAR>p : Filter ι<VAR>s : Set β<VAR>H : ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, dist (f y) (F n y) < ε<VAR>u : Set (α × α)<VAR>hu : u ∈ 𝓤 α<VAR>x : β<VAR>hx : x ∈ s<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ u<VAR>t : Set β<VAR>ht : t ∈ 𝓝[s] x<VAR>Ht : ∀ᶠ (n : ι) in p, ∀ y ∈ t, dist (f y) (F n y) < ε<GOAL>∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : IsPurelyInseparable F E<VAR>L : Type w<VAR>inst✝¹ : CommRing L<VAR>inst✝ : IsReduced L<VAR>f g : E →+* L<VAR>heq : (fun f => f.comp (algebraMap F E)) f = (fun f => f.comp (algebraMap F E)) g<VAR>x : E<VAR>q : ℕ := ringExpChar F<GOAL>f x = g x
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : IsPurelyInseparable F E<VAR>L : Type w<VAR>inst✝¹ : CommRing L<VAR>inst✝ : IsReduced L<VAR>f g : E →+* L<VAR>heq : (fun f => f.comp (algebraMap F E)) f = (fun f => f.comp (algebraMap F E)) g<VAR>x : E<VAR>q : ℕ := ringExpChar F<VAR>n : ℕ<VAR>y : F<VAR>h : (algebraMap F E) y = x ^ q ^ n<GOAL>f x = g x
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : IsPurelyInseparable F E<VAR>L : Type w<VAR>inst✝¹ : CommRing L<VAR>inst✝ : IsReduced L<VAR>f g : E →+* L<VAR>x : E<VAR>q : ℕ := ringExpChar F<VAR>n : ℕ<VAR>y : F<VAR>h : (algebraMap F E) y = x ^ q ^ n<VAR>heq : ((fun f => f.comp (algebraMap F E)) f) y = ((fun f => f.comp (algebraMap F E)) g) y<GOAL>f x = g x
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : IsPurelyInseparable F E<VAR>L : Type w<VAR>inst✝¹ : CommRing L<VAR>inst✝ : IsReduced L<VAR>f g : E →+* L<VAR>x : E<VAR>q : ℕ := ringExpChar F<VAR>n : ℕ<VAR>y : F<VAR>h : (algebraMap F E) y = x ^ q ^ n<VAR>heq : f x ^ q ^ n = g x ^ q ^ n<GOAL>f x = g x
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : IsPurelyInseparable F E<VAR>L : Type w<VAR>inst✝¹ : CommRing L<VAR>inst✝ : IsReduced L<VAR>f g : E →+* L<VAR>x : E<VAR>q : ℕ := ringExpChar F<VAR>n : ℕ<VAR>y : F<VAR>h : (algebraMap F E) y = x ^ q ^ n<VAR>heq : f x ^ q ^ n = g x ^ q ^ n<VAR>a✝ : Nontrivial L<GOAL>f x = g x
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : IsPurelyInseparable F E<VAR>L : Type w<VAR>inst✝¹ : CommRing L<VAR>inst✝ : IsReduced L<VAR>f g : E →+* L<VAR>x : E<VAR>q : ℕ := ringExpChar F<VAR>n : ℕ<VAR>y : F<VAR>h : (algebraMap F E) y = x ^ q ^ n<VAR>heq : f x ^ q ^ n = g x ^ q ^ n<VAR>a✝ : Nontrivial L<VAR>this : ExpChar L q<GOAL>f x = g x
<VAR>J : Type v'<VAR>inst✝⁵ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝³ : Category.{?u.45697, u_1} K<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>F : J ⥤ C<VAR>c : Cocone F<VAR>inst✝¹ : PreservesLimitsOfShape WalkingCospan G<VAR>inst✝ : ReflectsColimitsOfShape J G<VAR>hc : IsUniversalColimit (G.mapCocone c)<VAR>F' : J ⥤ C<VAR>c' : Cocone F'<VAR>α : F' ⟶ F<VAR>f : c'.pt ⟶ c.pt<VAR>h : α ≫ c.ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)<VAR>j : J<GOAL>(whiskerRight α G ≫ (G.mapCocone c).ι).app j = ((G.mapCocone c').ι ≫ (Functor.const J).map (G.map f)).app j
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>f : Filtration ℕ m<VAR>u : ℕ → Ω → β<VAR>τ π : Ω → ℕ<VAR>inst✝ : AddCommGroup β<VAR>hle : τ ≤ π<VAR>N : ℕ<VAR>hbdd : ∀ (ω : Ω), π ω ≤ N<GOAL>stoppedValue u π - stoppedValue u τ = fun ω => (∑ i ∈ Finset.range (N + 1), {ω | τ ω ≤ i ∧ i < π ω}.indicator (u (i + 1) - u i)) ω
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>f : Filtration ℕ m<VAR>u : ℕ → Ω → β<VAR>τ π : Ω → ℕ<VAR>inst✝ : AddCommGroup β<VAR>hle : τ ≤ π<VAR>N : ℕ<VAR>hbdd : ∀ (ω : Ω), π ω ≤ N<GOAL>(fun ω => (∑ i ∈ Finset.Ico (τ ω) (π ω), (u (i + 1) - u i)) ω) = fun ω => (∑ i ∈ Finset.range (N + 1), {ω | τ ω ≤ i ∧ i < π ω}.indicator (u (i + 1) - u i)) ω
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>f : Filtration ℕ m<VAR>u : ℕ → Ω → β<VAR>τ π : Ω → ℕ<VAR>inst✝ : AddCommGroup β<VAR>hle : τ ≤ π<VAR>N : ℕ<VAR>hbdd : ∀ (ω : Ω), π ω ≤ N<VAR>ω : Ω<GOAL>(∑ i ∈ Finset.Ico (τ ω) (π ω), (u (i + 1) - u i)) ω = (∑ i ∈ Finset.range (N + 1), {ω | τ ω ≤ i ∧ i < π ω}.indicator (u (i + 1) - u i)) ω
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>f : Filtration ℕ m<VAR>u : ℕ → Ω → β<VAR>τ π : Ω → ℕ<VAR>inst✝ : AddCommGroup β<VAR>hle : τ ≤ π<VAR>N : ℕ<VAR>hbdd : ∀ (ω : Ω), π ω ≤ N<VAR>ω : Ω<GOAL>∑ c ∈ Finset.Ico (τ ω) (π ω), (u (c + 1) - u c) ω = ∑ c ∈ Finset.filter (fun i => ω ∈ {ω | τ ω ≤ i ∧ i < π ω}) (Finset.range (N + 1)), (u (c + 1) - u c) ω
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>f : Filtration ℕ m<VAR>u : ℕ → Ω → β<VAR>τ π : Ω → ℕ<VAR>inst✝ : AddCommGroup β<VAR>hle : τ ≤ π<VAR>N : ℕ<VAR>hbdd : ∀ (ω : Ω), π ω ≤ N<VAR>ω : Ω<GOAL>Finset.Ico (τ ω) (π ω) = Finset.filter (fun i => ω ∈ {ω | τ ω ≤ i ∧ i < π ω}) (Finset.range (N + 1))
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>f : Filtration ℕ m<VAR>u : ℕ → Ω → β<VAR>τ π : Ω → ℕ<VAR>inst✝ : AddCommGroup β<VAR>hle : τ ≤ π<VAR>N : ℕ<VAR>hbdd : ∀ (ω : Ω), π ω ≤ N<VAR>ω : Ω<VAR>i : ℕ<GOAL>i ∈ Finset.Ico (τ ω) (π ω) ↔ i ∈ Finset.filter (fun i => ω ∈ {ω | τ ω ≤ i ∧ i < π ω}) (Finset.range (N + 1))
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>f : Filtration ℕ m<VAR>u : ℕ → Ω → β<VAR>τ π : Ω → ℕ<VAR>inst✝ : AddCommGroup β<VAR>hle : τ ≤ π<VAR>N : ℕ<VAR>hbdd : ∀ (ω : Ω), π ω ≤ N<VAR>ω : Ω<VAR>i : ℕ<GOAL>τ ω ≤ i ∧ i < π ω ↔ i < N + 1 ∧ τ ω ≤ i ∧ i < π ω
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : ‖x‖ = ‖y‖<VAR>hn : ¬x = y<GOAL>|(o.oangle (y - x) y).toReal| < π / 2
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : ‖x‖ = ‖y‖<VAR>hn : ¬x = y<VAR>hs : (2 • o.oangle (y - x) y).sign = (o.oangle (y - x) y).sign<GOAL>|(o.oangle (y - x) y).toReal| < π / 2
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : ‖x‖ = ‖y‖<VAR>hn : ¬x = y<VAR>hs : o.oangle (y - x) y = ↑π ∨ |(o.oangle (y - x) y).toReal| < π / 2<GOAL>|(o.oangle (y - x) y).toReal| < π / 2
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝⁴ : Category.{v', u'} A<VAR>inst✝³ : ConcreteCategory A<VAR>inst✝² : J.WEqualsLocallyBijective A<VAR>X Y : Cᵒᵖ ⥤ A<VAR>f : X ⟶ Y<VAR>inst✝¹ : Presheaf.IsLocallyInjective J f<VAR>inst✝ : Presheaf.IsLocallySurjective J f<GOAL>J.W f
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝⁴ : Category.{v', u'} A<VAR>inst✝³ : ConcreteCategory A<VAR>inst✝² : J.WEqualsLocallyBijective A<VAR>X Y : Cᵒᵖ ⥤ A<VAR>f : X ⟶ Y<VAR>inst✝¹ : Presheaf.IsLocallyInjective J f<VAR>inst✝ : Presheaf.IsLocallySurjective J f<GOAL>Presheaf.IsLocallyInjective J f ∧ Presheaf.IsLocallySurjective J f
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁹ : NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>inst✝¹⁸ : TopologicalSpace H<VAR>E : Type u_3<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>F : Type u_4<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>inst✝¹⁴ : NormedSpace 𝕜 F<VAR>J : ModelWithCorners 𝕜 F F<VAR>G : Type u_5<VAR>inst✝¹³ : TopologicalSpace G<VAR>inst✝¹² : ChartedSpace H G<VAR>inst✝¹¹ : Group G<VAR>inst✝¹⁰ : LieGroup I G<VAR>E' : Type u_6<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H' M<VAR>E'' : Type u_9<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_10<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M' : Type u_11<VAR>inst✝¹ : TopologicalSpace M'<VAR>inst✝ : ChartedSpace H'' M'<VAR>n : ℕ∞<VAR>f g : M → G<VAR>hf : ContMDiff I' I n f<VAR>hg : ContMDiff I' I n g<GOAL>ContMDiff I' I n fun x => f x / g x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁹ : NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>inst✝¹⁸ : TopologicalSpace H<VAR>E : Type u_3<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>F : Type u_4<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>inst✝¹⁴ : NormedSpace 𝕜 F<VAR>J : ModelWithCorners 𝕜 F F<VAR>G : Type u_5<VAR>inst✝¹³ : TopologicalSpace G<VAR>inst✝¹² : ChartedSpace H G<VAR>inst✝¹¹ : Group G<VAR>inst✝¹⁰ : LieGroup I G<VAR>E' : Type u_6<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H' M<VAR>E'' : Type u_9<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_10<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M' : Type u_11<VAR>inst✝¹ : TopologicalSpace M'<VAR>inst✝ : ChartedSpace H'' M'<VAR>n : ℕ∞<VAR>f g : M → G<VAR>hf : ContMDiff I' I n f<VAR>hg : ContMDiff I' I n g<GOAL>ContMDiff I' I n fun x => f x * (g x)⁻¹
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>hp : p ≠ 0<GOAL>moment 0 p μ = 0
<VAR>t : Type u → Type u → Type u<VAR>inst✝⁵ : Bitraversable t<VAR>β : Type u<VAR>F G : Type u → Type u<VAR>inst✝⁴ : Applicative F<VAR>inst✝³ : Applicative G<VAR>inst✝² : LawfulBitraversable t<VAR>inst✝¹ : LawfulApplicative F<VAR>inst✝ : LawfulApplicative G<VAR>α₀ α₁ β₀ β₁ : Type u<VAR>f : α₀ → F α₁<VAR>f' : β₀ → G β₁<VAR>x : t α₀ β₀<GOAL>Comp.mk (tfst f <$> tsnd f' x) = bitraverse (Comp.mk ∘ pure ∘ f) (Comp.mk ∘ map pure ∘ f') x
<VAR>t : Type u → Type u → Type u<VAR>inst✝⁵ : Bitraversable t<VAR>β : Type u<VAR>F G : Type u → Type u<VAR>inst✝⁴ : Applicative F<VAR>inst✝³ : Applicative G<VAR>inst✝² : LawfulBitraversable t<VAR>inst✝¹ : LawfulApplicative F<VAR>inst✝ : LawfulApplicative G<VAR>α₀ α₁ β₀ β₁ : Type u<VAR>f : α₀ → F α₁<VAR>f' : β₀ → G β₁<VAR>x : t α₀ β₀<GOAL>bitraverse (Comp.mk ∘ map f ∘ pure) (Comp.mk ∘ map pure ∘ f') x = bitraverse (Comp.mk ∘ pure ∘ f) (Comp.mk ∘ map pure ∘ f') x
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>s : Stream' α<GOAL>s.inits = [s.head] :: map (List.cons s.head) s.tail.inits
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>s : Stream' α<GOAL>∀ (n : ℕ), s.inits.get n = ([s.head] :: map (List.cons s.head) s.tail.inits).get n
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>f : α → α<VAR>hf : Involutive f<VAR>m : ℕ<GOAL>f^[m + m] = id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>ι : Type u_17<VAR>A : ι → α → E'<VAR>C : ι → ℝ<VAR>s : Finset ι<VAR>h : ∀ i ∈ s, A i =o[l] g'<GOAL>(fun x => ∑ i ∈ s, A i x) =o[l] g'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>ι : Type u_17<VAR>A : ι → α → E'<VAR>C : ι → ℝ<VAR>s : Finset ι<VAR>h : ∀ i ∈ ∅, A i =o[l] g'<GOAL>(fun x => ∑ i ∈ ∅, A i x) =o[l] g'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>ι : Type u_17<VAR>A : ι → α → E'<VAR>C : ι → ℝ<VAR>s✝ : Finset ι<VAR>i : ι<VAR>s : Finset ι<VAR>is : i ∉ s<VAR>IH : (∀ i ∈ s, A i =o[l] g') → (fun x => ∑ i ∈ s, A i x) =o[l] g'<VAR>h : ∀ i_1 ∈ insert i s, A i_1 =o[l] g'<GOAL>(fun x => ∑ i ∈ insert i s, A i x) =o[l] g'
<VAR>A : Type u_1<VAR>inst✝⁶ : CanonicallyOrderedAddCommMonoid A<VAR>inst✝⁵ : Sub A<VAR>inst✝⁴ : OrderedSub A<VAR>inst✝³ : ContravariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : HasAntidiagonal A<VAR>n m : A<VAR>inst✝¹ : DecidablePred fun x => x = m<VAR>inst✝ : Decidable (m ≤ n)<VAR>a b : A<GOAL>(a, b) ∈ filter (fun x => x.1 = m) (antidiagonal n) ↔ (a, b) ∈ if m ≤ n then {(m, n - m)} else ∅
<VAR>A : Type u_1<VAR>inst✝⁶ : CanonicallyOrderedAddCommMonoid A<VAR>inst✝⁵ : Sub A<VAR>inst✝⁴ : OrderedSub A<VAR>inst✝³ : ContravariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : HasAntidiagonal A<VAR>n m : A<VAR>inst✝¹ : DecidablePred fun x => x = m<VAR>inst✝ : Decidable (m ≤ n)<VAR>a b : A<GOAL>a = m → (a + b = n ↔ m ≤ n ∧ b = n - m)
<VAR>n p : ℕ<GOAL>Prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
<VAR>n p : ℕ<VAR>h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p<GOAL>Prime p
<VAR>n p : ℕ<VAR>h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p<VAR>h1 : 1 < p<GOAL>Prime p
<VAR>n p : ℕ<VAR>h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p<VAR>h1 : 1 < p<VAR>a b : ℕ<VAR>hab : p = a * b<GOAL>IsUnit a ∨ IsUnit b
<VAR>n p : ℕ<VAR>h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p<VAR>h1 : 1 < p<VAR>a b : ℕ<VAR>hab : p = a * b<GOAL>a = 1 ∨ b = 1
<VAR>n p : ℕ<VAR>h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p<VAR>h1 : 1 < p<VAR>a b : ℕ<VAR>hab : p = a * b<GOAL>a = p → b = 1
<VAR>n p : ℕ<VAR>h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p<VAR>h1 : 1 < p<VAR>a b : ℕ<VAR>hab : p = a * b<GOAL>a ∣ p
<VAR>α : Type u_1<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h : a < b<GOAL>∃ q, 0 ≤ q ∧ a < ↑(↑q).toNNReal ∧ ↑(↑q).toNNReal < b
<VAR>α : Type u_1<VAR>b c d : ℝ≥0∞<VAR>r p✝ q p : ℝ≥0<VAR>right✝ h : ↑p < b<GOAL>∃ q, 0 ≤ q ∧ ↑p < ↑(↑q).toNNReal ∧ ↑(↑q).toNNReal < b
<VAR>α : Type u_1<VAR>b c✝ d : ℝ≥0∞<VAR>r p✝ q p : ℝ≥0<VAR>right✝ h : ↑p < b<VAR>c : ℝ≥0∞<VAR>pc : ↑p < c<VAR>cb : c < b<GOAL>∃ q, 0 ≤ q ∧ ↑p < ↑(↑q).toNNReal ∧ ↑(↑q).toNNReal < b
<VAR>α : Type u_1<VAR>b c d : ℝ≥0∞<VAR>r✝ p✝ q p : ℝ≥0<VAR>right✝¹ h : ↑p < b<VAR>r : ℝ≥0<VAR>right✝ : ↑r < b<VAR>pc : ↑p < ↑r<VAR>cb : ↑r < b<GOAL>∃ q, 0 ≤ q ∧ ↑p < ↑(↑q).toNNReal ∧ ↑(↑q).toNNReal < b
<VAR>α : Type u_1<VAR>b c d : ℝ≥0∞<VAR>r✝ p✝ q✝ p : ℝ≥0<VAR>right✝¹ h : ↑p < b<VAR>r : ℝ≥0<VAR>right✝ : ↑r < b<VAR>pc : ↑p < ↑r<VAR>cb : ↑r < b<VAR>q : ℚ<VAR>hq0 : 0 ≤ q<VAR>pq : p < (↑q).toNNReal<VAR>qr : (↑q).toNNReal < r<GOAL>∃ q, 0 ≤ q ∧ ↑p < ↑(↑q).toNNReal ∧ ↑(↑q).toNNReal < b
<VAR>R : Type u<VAR>inst✝¹² : CommRing R<VAR>M N P Q : Type u<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : AddCommGroup N<VAR>inst✝⁹ : AddCommGroup P<VAR>inst✝⁸ : AddCommGroup Q<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Coalgebra R M<VAR>inst✝² : Coalgebra R N<VAR>inst✝¹ : Coalgebra R P<VAR>inst✝ : Coalgebra R Q<GOAL>Coalgebra.comul = Coalgebra.comul
<VAR>R : Type u<VAR>inst✝¹² : CommRing R<VAR>M N P Q : Type u<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : AddCommGroup N<VAR>inst✝⁹ : AddCommGroup P<VAR>inst✝⁸ : AddCommGroup Q<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Coalgebra R M<VAR>inst✝² : Coalgebra R N<VAR>inst✝¹ : Coalgebra R P<VAR>inst✝ : Coalgebra R Q<GOAL>((comonEquivalence R).symm.inverse.obj (of R M) ⊗ (comonEquivalence R).symm.inverse.obj (of R N ⊗ of R P)).comul = Coalgebra.comul