ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>f : α → E<VAR>hf : Integrable f μ<VAR>I : Integrable (AEStronglyMeasurable.mk f ⋯) μ<VAR>x : α<VAR>hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)<VAR>h'x : f x = AEStronglyMeasurable.mk f ⋯ x<VAR>a : Set α<VAR>y : α<VAR>hy : f y = AEStronglyMeasurable.mk f ⋯ y<GOAL>↑‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖₊ = ↑‖f y - f x‖₊
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>s t : Set α<VAR>a x y : α<GOAL>s ⊆ exterior t ↔ ∀ (U : Set α), IsOpen U → t ⊆ U → s ⊆ U
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_5, u_1} C<VAR>inst✝¹ : Category.{u_4, u_2} D<VAR>inst✝ : Preadditive D<VAR>F G : C ⥤ D<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>X : C<VAR>α : ι → (F ⟶ G)<GOAL>(∑ i ∈ s, α i).app X = ∑ i ∈ s, (α i).app X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>s : Set α<VAR>a b : α<VAR>hab : a ≠ b<GOAL>closure (Ioo a b) = Icc a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>s : Set α<VAR>a b : α<VAR>hab : a ≠ b<GOAL>closure (Ioo a b) ⊆ Icc a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>s : Set α<VAR>a b : α<VAR>hab : a ≠ b<GOAL>Icc a b ⊆ closure (Ioo a b)
<VAR>m n a b c d : ℕ<GOAL>a ≡ b [MOD n] ↔ ↑n ∣ ↑b - ↑a
<VAR>α : Type u<VAR>β : Type v<VAR>l l₁ l₂✝ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>σ : α → Type u_1<VAR>l₂ : (a : α) → List (σ a)<VAR>d₁ : l₁.Nodup<VAR>d₂ : ∀ (a : α), (l₂ a).Nodup<VAR>a₁ a₂ : α<VAR>n : a₁ ≠ a₂<VAR>x : (a : α) × σ a<VAR>h₁ : x ∈ map (Sigma.mk a₁) (l₂ a₁)<VAR>h₂ : x ∈ map (Sigma.mk a₂) (l₂ a₂)<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>l l₁ l₂✝ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>σ : α → Type u_1<VAR>l₂ : (a : α) → List (σ a)<VAR>d₁ : l₁.Nodup<VAR>d₂ : ∀ (a : α), (l₂ a).Nodup<VAR>a₁ a₂ : α<VAR>n : a₁ ≠ a₂<VAR>b₁ : σ a₁<VAR>left✝ : b₁ ∈ l₂ a₁<VAR>h₁ : ⟨a₁, b₁⟩ ∈ map (Sigma.mk a₁) (l₂ a₁)<VAR>h₂ : ⟨a₁, b₁⟩ ∈ map (Sigma.mk a₂) (l₂ a₂)<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>l l₁ l₂✝ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>σ : α → Type u_1<VAR>l₂ : (a : α) → List (σ a)<VAR>d₁ : l₁.Nodup<VAR>d₂ : ∀ (a : α), (l₂ a).Nodup<VAR>a₁ : α<VAR>b₁ : σ a₁<VAR>left✝ : b₁ ∈ l₂ a₁<VAR>h₁ : ⟨a₁, b₁⟩ ∈ map (Sigma.mk a₁) (l₂ a₁)<VAR>n : a₁ ≠ a₁<VAR>h₂ : ⟨a₁, b₁⟩ ∈ map (Sigma.mk a₁) (l₂ a₁)<VAR>mb₂ : b₁ ∈ l₂ a₁<GOAL>False
<VAR>x : ℝ<GOAL>↑x ∈ slitPlane ↔ 0 < x
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIcoMod hp a b = toIcoMod hp 0 (b - a) + a
<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>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>inst✝ : DecidableEq ι<VAR>p : ι → P<VAR>i : ι<VAR>hi : i ∈ s<GOAL>(affineCombination k s p) (affineCombinationSingleWeights k i) = p i
<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>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>inst✝ : DecidableEq ι<VAR>p : ι → P<VAR>i : ι<VAR>hi : i ∈ s<GOAL>∀ i2 ∈ s, i2 ≠ i → affineCombinationSingleWeights k i i2 = 0
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasBinaryBiproducts C<VAR>W X Y Z : C<VAR>f : W ⟶ Y<VAR>g : X ⟶ Z<VAR>inst✝ : IsIso (biprod.map f g)<GOAL>f ≫ biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst = 𝟙 W
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasBinaryBiproducts C<VAR>W X Y Z : C<VAR>f : W ⟶ Y<VAR>g : X ⟶ Z<VAR>inst✝ : IsIso (biprod.map f g)<VAR>t : (fun p => biprod.inl ≫ p ≫ biprod.fst) (biprod.map f g ≫ inv (biprod.map f g)) = (fun p => biprod.inl ≫ p ≫ biprod.fst) (𝟙 (W ⊞ X))<GOAL>f ≫ biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst = 𝟙 W
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasBinaryBiproducts C<VAR>W X Y Z : C<VAR>f : W ⟶ Y<VAR>g : X ⟶ Z<VAR>inst✝ : IsIso (biprod.map f g)<VAR>t : f ≫ biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst = biprod.inl ≫ biprod.fst<GOAL>f ≫ biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst = 𝟙 W
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasBinaryBiproducts C<VAR>W X Y Z : C<VAR>f : W ⟶ Y<VAR>g : X ⟶ Z<VAR>inst✝ : IsIso (biprod.map f g)<GOAL>(biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst) ≫ f = 𝟙 Y
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasBinaryBiproducts C<VAR>W X Y Z : C<VAR>f : W ⟶ Y<VAR>g : X ⟶ Z<VAR>inst✝ : IsIso (biprod.map f g)<VAR>t : (fun p => biprod.inl ≫ p ≫ biprod.fst) (inv (biprod.map f g) ≫ biprod.map f g) = (fun p => biprod.inl ≫ p ≫ biprod.fst) (𝟙 (Y ⊞ Z))<GOAL>(biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst) ≫ f = 𝟙 Y
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasBinaryBiproducts C<VAR>W X Y Z : C<VAR>f : W ⟶ Y<VAR>g : X ⟶ Z<VAR>inst✝ : IsIso (biprod.map f g)<VAR>t : biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst ≫ f = biprod.inl ≫ biprod.fst<GOAL>(biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst) ≫ f = 𝟙 Y
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasBinaryBiproducts C<VAR>W X Y Z : C<VAR>f : W ⟶ Y<VAR>g : X ⟶ Z<VAR>inst✝ : IsIso (biprod.map f g)<VAR>t : biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst ≫ f = biprod.inl ≫ biprod.fst<GOAL>biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst ≫ f = 𝟙 Y
<VAR>x : ℝ<GOAL>cos (arctan x) ^ 2 = 1 / (1 + x ^ 2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f✝ f₁ f₂ : Filter α<VAR>h h₁ h₂ : Set α → Set β<VAR>inst✝ : Nonempty ι<VAR>f : ι → Filter α<VAR>g : Set α → Set β<VAR>hg : ∀ (s t : Set α), g (s ∩ t) = g s ∩ g t<VAR>s t : Set α<GOAL>(𝓟 ∘ g) (s ∩ t) = (𝓟 ∘ g) s ⊓ (𝓟 ∘ g) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : Measure α<VAR>κ η : Kernel α β<VAR>inst✝² : SFinite μ<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>E : Type u_3<VAR>inst✝ : NormedAddCommGroup E<VAR>f : α × β → E<VAR>hf : AEStronglyMeasurable f (μ ⊗ₘ κ)<GOAL>Integrable f (μ ⊗ₘ κ) ↔ (∀ᵐ (x : α) ∂μ, Integrable (fun y => f (x, y)) (κ x)) ∧ Integrable (fun x => ∫ (y : β), ‖f (x, y)‖ ∂κ x) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : Measure α<VAR>κ η : Kernel α β<VAR>inst✝² : SFinite μ<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>E : Type u_3<VAR>inst✝ : NormedAddCommGroup E<VAR>f : α × β → E<VAR>hf : AEStronglyMeasurable f (μ ⊗ₘ κ)<GOAL>(∀ᵐ (x : α) ∂(Kernel.const Unit μ) (), Integrable (fun y => f (x, y)) ((Kernel.prodMkLeft Unit κ) ((), x))) ∧ Integrable (fun x => ∫ (y : β), ‖f (x, y)‖ ∂(Kernel.prodMkLeft Unit κ) ((), x)) ((Kernel.const Unit μ) ()) ↔ (∀ᵐ (x : α) ∂μ, Integrable (fun y => f (x, y)) (κ x)) ∧ Integrable (fun x => ∫ (y : β), ‖f (x, y)‖ ∂κ x) μ
<VAR>x : ℝ<GOAL>Real.toEReal ⁻¹' Ico ↑x ⊤ = Ici x
<VAR>x : ℝ<GOAL>Real.toEReal ⁻¹' (Ici ↑x ∩ Iio ⊤) = Ici x
<VAR>n : ℤ<GOAL>abs ↑n = |↑n|
<VAR>s : ℝ<VAR>hs : s ≠ 0<GOAL>(s + 1).doublingGamma = s * s.doublingGamma
<VAR>s : ℝ<VAR>hs : s ≠ 0<GOAL>Gamma (s / 2 + 1 / 2) * (s / 2 * Gamma (s / 2)) * (2 ^ (s - 1) * 2) / √π = s * (Gamma (s / 2) * Gamma (s / 2 + 1 / 2) * 2 ^ (s - 1) / √π)
<VAR>ι : Type u_1<VAR>inst✝ : Countable ι<VAR>a : ι → ℂ<VAR>p : ι → ℝ<VAR>F : ℝ → ℂ<VAR>s : ℂ<VAR>hp : ∀ (i : ι), 0 ≤ p i<VAR>hs : 0 < s.re<VAR>hF : ∀ t ∈ Ioi 0, HasSum (fun i => if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) (F t)<VAR>h_sum : Summable fun i => ‖a i‖ / p i ^ s.re<GOAL>HasSum (fun i => ↑π ^ (-s) * Complex.Gamma s * a i / ↑(p i) ^ s) (mellin F s)
<VAR>ι : Type u_1<VAR>inst✝ : Countable ι<VAR>a : ι → ℂ<VAR>p : ι → ℝ<VAR>F : ℝ → ℂ<VAR>s : ℂ<VAR>hp : ∀ (i : ι), 0 ≤ p i<VAR>hs : 0 < s.re<VAR>hF : ∀ t ∈ Ioi 0, HasSum (fun i => if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) (F t)<VAR>h_sum : Summable fun i => ‖a i‖ / p i ^ s.re<VAR>hs' : s ≠ 0<GOAL>HasSum (fun i => ↑π ^ (-s) * Complex.Gamma s * a i / ↑(p i) ^ s) (mellin F s)
<VAR>ι : Type u_1<VAR>inst✝ : Countable ι<VAR>a : ι → ℂ<VAR>p : ι → ℝ<VAR>F : ℝ → ℂ<VAR>s : ℂ<VAR>hp : ∀ (i : ι), 0 ≤ p i<VAR>hs : 0 < s.re<VAR>hF : ∀ t ∈ Ioi 0, HasSum (fun i => if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) (F t)<VAR>h_sum : Summable fun i => ‖a i‖ / p i ^ s.re<VAR>hs' : s ≠ 0<VAR>a' : ι → ℂ := fun i => if p i = 0 then 0 else a i<GOAL>HasSum (fun i => ↑π ^ (-s) * Complex.Gamma s * a i / ↑(p i) ^ s) (mellin F s)
<VAR>ι : Type u_1<VAR>inst✝ : Countable ι<VAR>a : ι → ℂ<VAR>p : ι → ℝ<VAR>F : ℝ → ℂ<VAR>s : ℂ<VAR>hp : ∀ (i : ι), 0 ≤ p i<VAR>hs : 0 < s.re<VAR>hF : ∀ t ∈ Ioi 0, HasSum (fun i => if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) (F t)<VAR>h_sum : Summable fun i => ‖a i‖ / p i ^ s.re<VAR>hs' : s ≠ 0<VAR>a' : ι → ℂ := fun i => if p i = 0 then 0 else a i<VAR>hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i<GOAL>HasSum (fun i => ↑π ^ (-s) * Complex.Gamma s * a i / ↑(p i) ^ s) (mellin F s)
<VAR>ι : Type u_1<VAR>inst✝ : Countable ι<VAR>a : ι → ℂ<VAR>p : ι → ℝ<VAR>F : ℝ → ℂ<VAR>s : ℂ<VAR>hp : ∀ (i : ι), 0 ≤ p i<VAR>hs : 0 < s.re<VAR>hF : ∀ t ∈ Ioi 0, HasSum (fun i => if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) (F t)<VAR>h_sum : Summable fun i => ‖a i‖ / p i ^ s.re<VAR>hs' : s ≠ 0<VAR>a' : ι → ℂ := fun i => if p i = 0 then 0 else a i<VAR>hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i<VAR>this : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))<GOAL>HasSum (fun i => ↑π ^ (-s) * Complex.Gamma s * a i / ↑(p i) ^ s) (mellin F s)
<VAR>ι : Type u_1<VAR>inst✝ : Countable ι<VAR>a : ι → ℂ<VAR>p : ι → ℝ<VAR>F : ℝ → ℂ<VAR>s : ℂ<VAR>hp : ∀ (i : ι), 0 ≤ p i<VAR>hs : 0 < s.re<VAR>h_sum : Summable fun i => ‖a i‖ / p i ^ s.re<VAR>hs' : s ≠ 0<VAR>a' : ι → ℂ := fun i => if p i = 0 then 0 else a i<VAR>hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i<VAR>this : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))<VAR>hF : ∀ t ∈ Ioi 0, HasSum (fun i => a' i * ↑(rexp (-π * p i * t))) (F t)<GOAL>HasSum (fun i => ↑π ^ (-s) * Complex.Gamma s * a i / ↑(p i) ^ s) (mellin F s)
<VAR>ι : Type u_1<VAR>inst✝ : Countable ι<VAR>a : ι → ℂ<VAR>p : ι → ℝ<VAR>F : ℝ → ℂ<VAR>s : ℂ<VAR>hp : ∀ (i : ι), 0 ≤ p i<VAR>hs : 0 < s.re<VAR>h_sum : Summable fun i => ‖a i‖ / p i ^ s.re<VAR>hs' : s ≠ 0<VAR>a' : ι → ℂ := fun i => if p i = 0 then 0 else a i<VAR>hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i<VAR>this : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))<VAR>hF : ∀ t ∈ Ioi 0, HasSum (fun i => a' i * ↑(rexp (-π * p i * t))) (F t)<VAR>i : ι<GOAL>↑π ^ (-s) * Complex.Gamma s * a i / ↑(p i) ^ s = ↑π ^ (-s) * Complex.Gamma s * a' i / ↑(p i) ^ s
<VAR>ι : Type u_1<VAR>inst✝ : Countable ι<VAR>a : ι → ℂ<VAR>p : ι → ℝ<VAR>F : ℝ → ℂ<VAR>s : ℂ<VAR>hp : ∀ (i : ι), 0 ≤ p i<VAR>hs : 0 < s.re<VAR>h_sum : Summable fun i => ‖a i‖ / p i ^ s.re<VAR>hs' : s ≠ 0<VAR>a' : ι → ℂ := fun i => if p i = 0 then 0 else a i<VAR>hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i<VAR>this : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))<VAR>hF : ∀ t ∈ Ioi 0, HasSum (fun i => a' i * ↑(rexp (-π * p i * t))) (F t)<GOAL>Summable fun i => ‖a' i‖ / p i ^ s.re
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : HasZeroMorphisms C<VAR>X : C<VAR>hX : IsInitial X<GOAL>IsZero X
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : HasZeroMorphisms C<VAR>X : C<VAR>hX : IsInitial X<GOAL>𝟙 X = 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>I : Type u_3<VAR>J : Type u_4<VAR>inst✝⁷ : Category.{u_6, u_1} C<VAR>inst✝⁶ : Category.{u_5, u_2} D<VAR>inst✝⁵ : Zero I<VAR>inst✝⁴ : DecidableEq I<VAR>inst✝³ : HasInitial C<VAR>F : D ⥤ C ⥤ D<VAR>Y : C<VAR>e : F.flip.obj Y ≅ 𝟭 D<VAR>inst✝² : (X : D) → PreservesColimit (Functor.empty C) (F.obj X)<VAR>p : J × I → J<VAR>hp : ∀ (j : J), p (j, 0) = j<VAR>X X' : GradedObject J D<VAR>φ : X ⟶ X'<VAR>inst✝¹ : (((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).HasMap p<VAR>inst✝ : (((mapBifunctor F J I).obj X').obj ((single₀ I).obj Y)).HasMap p<VAR>Y' : ?m.145927<GOAL>mapBifunctorMapMap F p φ (𝟙 ((single₀ I).obj Y)) ≫ (mapBifunctorRightUnitor F Y e p hp X').hom = (mapBifunctorRightUnitor F Y e p hp X).hom ≫ φ
<VAR>A : Type u_1<VAR>inst✝³ : AddCommGroup A<VAR>inst✝² : Module ℂ A<VAR>inst✝¹ : StarAddMonoid A<VAR>inst✝ : StarModule ℂ A<VAR>z : ℂ<GOAL>↑(ℜ z) = ?m.419985
<VAR>A : Type u_1<VAR>inst✝³ : AddCommGroup A<VAR>inst✝² : Module ℂ A<VAR>inst✝¹ : StarAddMonoid A<VAR>inst✝ : StarModule ℂ A<VAR>z : ℂ<GOAL>↑(ℜ (↑z.re + ↑z.im * I)) = ↑z.re
<VAR>A : Type u_1<VAR>inst✝³ : AddCommGroup A<VAR>inst✝² : Module ℂ A<VAR>inst✝¹ : StarAddMonoid A<VAR>inst✝ : StarModule ℂ A<VAR>z : ℂ<GOAL>↑(ℜ ↑z.re) + ↑(-ℑ ↑z.im) = ↑z.re
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>ι' : Type u_3<VAR>inst✝² : SemilatticeInf α<VAR>inst✝¹ : OrderBot α<VAR>s✝ : Finset ι<VAR>f✝ : ι → α<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>f : ι → α<VAR>hs : (↑s).PairwiseDisjoint f<VAR>g : ι → ι<VAR>hf : ∀ (a : ι), f (g a) ≤ f a<GOAL>(↑(Finset.image g s)).PairwiseDisjoint f
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>ι' : Type u_3<VAR>inst✝² : SemilatticeInf α<VAR>inst✝¹ : OrderBot α<VAR>s✝ : Finset ι<VAR>f✝ : ι → α<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>f : ι → α<VAR>hs : (↑s).PairwiseDisjoint f<VAR>g : ι → ι<VAR>hf : ∀ (a : ι), f (g a) ≤ f a<GOAL>(g '' ↑s).PairwiseDisjoint f
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a x : α<VAR>hx : x ∈ factors a<GOAL>Prime x
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a x : α<VAR>hx : x ∈ factors a<VAR>ane0 : a ≠ 0<GOAL>Prime x
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a x : α<VAR>ane0 : a ≠ 0<VAR>hx : x ∈ Classical.choose ⋯<GOAL>Prime x
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : CharP R p<VAR>n : ℕ<VAR>x y : R<GOAL>(x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x : α<VAR>u : Set α<VAR>hu : u ∈ 𝓝 x<GOAL>∀ᶠ (r : ℝ) in 𝓝 0, closedBall x r ⊆ u
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x : α<VAR>u : Set α<VAR>hu : u ∈ 𝓝 x<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>hε : closedBall x ε ⊆ u<GOAL>∀ᶠ (r : ℝ) in 𝓝 0, closedBall x r ⊆ u
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x : α<VAR>u : Set α<VAR>hu : u ∈ 𝓝 x<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>hε : closedBall x ε ⊆ u<VAR>this : Iic ε ∈ 𝓝 0<GOAL>∀ᶠ (r : ℝ) in 𝓝 0, closedBall x r ⊆ u
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝² : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝¹ : Monoid N<VAR>inst✝ : (i : ι) → DecidableEq (M i)<VAR>i : ι<VAR>m : M i<VAR>w : Word M<VAR>h1 : m ≠ 1<VAR>h2 : w.fstIdx ≠ some i<GOAL>(cons m w h2 h1).prod = of m * w.prod
<VAR>x : ℝ≥0∞<VAR>z : ℝ<GOAL>x.toNNReal ^ z = (x ^ z).toNNReal
<VAR>x : ℝ≥0∞<VAR>z : ℝ<VAR>H : z < 0<GOAL>x.toNNReal ^ z = (x ^ z).toNNReal
<VAR>x : ℝ≥0∞<VAR>z : ℝ<VAR>H : z = 0<GOAL>x.toNNReal ^ z = (x ^ z).toNNReal
<VAR>x : ℝ≥0∞<VAR>z : ℝ<VAR>H : 0 < z<GOAL>x.toNNReal ^ z = (x ^ z).toNNReal
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<GOAL>A⁻¹ᵀ = Aᵀ⁻¹
<VAR>ι : Type u_1<VAR>R' : Type u_2<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : (i : ι) → NonAssocSemiring (A i)<VAR>inst✝² : (i : ι) → Module R (A i)<VAR>inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)<VAR>inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)<VAR>x : ⨂[R] (i : ι), A i<GOAL>(mul ((tprod R) 1)) x = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : OrderTop α<VAR>a : α<GOAL>Icc a ⊤ = Ici a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<VAR>f : Filter β<GOAL>limsup (fun x => ⊥) f = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<VAR>f : Filter β<GOAL>sInf {a | ∀ᶠ (n : β) in f, ⊥ ≤ a} ≤ ⊥
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P (n + 2)<VAR>i₁ i₂ : Fin (n + 3)<VAR>h : ¬i₁ = i₂<GOAL>⟪s.mongePoint -ᵥ centroid ℝ {i₁, i₂}ᶜ s.points, s.points i₁ -ᵥ s.points i₂⟫_ℝ = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P (n + 2)<VAR>i₁ i₂ : Fin (n + 3)<VAR>h : ¬i₁ = i₂<GOAL>⟪(univ.weightedVSub s.pointsWithCircumcenter) (mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂), (univ.weightedVSub s.pointsWithCircumcenter) (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂)⟫_ℝ = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P (n + 2)<VAR>i₁ i₂ : Fin (n + 3)<VAR>h : ¬i₁ = i₂<VAR>hs : ∑ i : PointsWithCircumcenterIndex (n + 2), (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0<GOAL>⟪(univ.weightedVSub s.pointsWithCircumcenter) (mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂), (univ.weightedVSub s.pointsWithCircumcenter) (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂)⟫_ℝ = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P (n + 2)<VAR>i₁ i₂ : Fin (n + 3)<VAR>h : ¬i₁ = i₂<VAR>hs : ∑ i : PointsWithCircumcenterIndex (n + 2), (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0<GOAL>-(∑ i : Fin (n + 2 + 1), ∑ i₂_1 : PointsWithCircumcenterIndex (n + 2), mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ (pointIndex i) * (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i₂_1 * (dist (s.pointsWithCircumcenter (pointIndex i)) (s.pointsWithCircumcenter i₂_1) * dist (s.pointsWithCircumcenter (pointIndex i)) (s.pointsWithCircumcenter i₂_1)) + ∑ i₂_1 : PointsWithCircumcenterIndex (n + 2), mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ circumcenterIndex * (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i₂_1 * (dist s.circumcenter (s.pointsWithCircumcenter i₂_1) * dist s.circumcenter (s.pointsWithCircumcenter i₂_1))) / 2 = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P (n + 2)<VAR>i₁ i₂ : Fin (n + 3)<VAR>h : ¬i₁ = i₂<VAR>hs : ∑ i : PointsWithCircumcenterIndex (n + 2), (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0<GOAL>-(∑ x : Fin (n + 2 + 1), ∑ x_1 : PointsWithCircumcenterIndex (n + 2), (if x = i₁ ∨ x = i₂ then (↑(n + 1))⁻¹ else 0) * (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) x_1 * (dist (s.points x) (s.pointsWithCircumcenter x_1) * dist (s.points x) (s.pointsWithCircumcenter x_1)) + ∑ x : PointsWithCircumcenterIndex (n + 2), -2 / ↑(n + 1) * (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) x * (dist s.circumcenter (s.pointsWithCircumcenter x) * dist s.circumcenter (s.pointsWithCircumcenter x))) / 2 = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P (n + 2)<VAR>i₁ i₂ : Fin (n + 3)<VAR>h : ¬i₁ = i₂<VAR>hs : ∑ i : PointsWithCircumcenterIndex (n + 2), (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0<VAR>fs : Finset (Fin (n + 3)) := {i₁, i₂}<VAR>hfs : ∀ i ∉ fs, i ≠ i₁ ∧ i ≠ i₂<GOAL>-(∑ x : Fin (n + 2 + 1), ∑ x_1 : PointsWithCircumcenterIndex (n + 2), (if x = i₁ ∨ x = i₂ then (↑(n + 1))⁻¹ else 0) * (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) x_1 * (dist (s.points x) (s.pointsWithCircumcenter x_1) * dist (s.points x) (s.pointsWithCircumcenter x_1)) + ∑ x : PointsWithCircumcenterIndex (n + 2), -2 / ↑(n + 1) * (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) x * (dist s.circumcenter (s.pointsWithCircumcenter x) * dist s.circumcenter (s.pointsWithCircumcenter x))) / 2 = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P (n + 2)<VAR>i₁ i₂ : Fin (n + 3)<VAR>h : ¬i₁ = i₂<VAR>hs : ∑ i : PointsWithCircumcenterIndex (n + 2), (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0<VAR>fs : Finset (Fin (n + 3)) := {i₁, i₂}<VAR>hfs : ∀ i ∉ fs, i ≠ i₁ ∧ i ≠ i₂<GOAL>-(∑ x ∈ fs, ∑ x_1 : PointsWithCircumcenterIndex (n + 2), (if x = i₁ ∨ x = i₂ then (↑(n + 1))⁻¹ else 0) * (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) x_1 * (dist (s.points x) (s.pointsWithCircumcenter x_1) * dist (s.points x) (s.pointsWithCircumcenter x_1)) + ∑ x : PointsWithCircumcenterIndex (n + 2), -2 / ↑(n + 1) * (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) x * (dist s.circumcenter (s.pointsWithCircumcenter x) * dist s.circumcenter (s.pointsWithCircumcenter x))) / 2 = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P (n + 2)<VAR>i₁ i₂ : Fin (n + 3)<VAR>h : ¬i₁ = i₂<VAR>hs : ∑ i : PointsWithCircumcenterIndex (n + 2), (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0<VAR>fs : Finset (Fin (n + 3)) := {i₁, i₂}<VAR>hfs : ∀ i ∉ fs, i ≠ i₁ ∧ i ≠ i₂<GOAL>∀ x ∈ univ, x ∉ fs → ∑ x_1 : PointsWithCircumcenterIndex (n + 2), (if x = i₁ ∨ x = i₂ then (↑(n + 1))⁻¹ else 0) * (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) x_1 * (dist (s.points x) (s.pointsWithCircumcenter x_1) * dist (s.points x) (s.pointsWithCircumcenter x_1)) = 0
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : Field 𝕜<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : DecidableEq p<VAR>inst✝¹ : CommRing R<VAR>i j : n<VAR>inst✝ : Finite n<VAR>c : R<GOAL>updateRow 1 i (1 i + c • 1 j) = transvection i j c
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : Field 𝕜<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : DecidableEq p<VAR>inst✝¹ : CommRing R<VAR>i j : n<VAR>inst✝ : Finite n<VAR>c : R<VAR>val✝ : Fintype n<GOAL>updateRow 1 i (1 i + c • 1 j) = transvection i j c
<GOAL>StrictConcaveOn ℝ (Ici 0) fun x => √x
<GOAL>StrictConcaveOn ℝ (Ici 0) fun x => (fun x => x ^ (1 / 2)) x