ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>C₂₃ : Type u_6<VAR>inst✝⁷ : Category.{u_11, u_1} C₁<VAR>inst✝⁶ : Category.{u_12, u_2} C₂<VAR>inst✝⁵ : Category.{u_13, u_3} C₃<VAR>inst✝⁴ : Category.{u_14, u_4} C₄<VAR>inst✝³ : Category.{?u.57419, u_5} C₁₂<VAR>inst✝² : Category.{?u.57423, u_6} C₂₃<VAR>F F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>p : I₁ × I₂ × I₃ → J<VAR>X₁ Y₁ : GradedObject I₁ C₁<VAR>f₁ : X₁ ⟶ Y₁<VAR>X₂ Y₂ : GradedObject I₂ C₂<VAR>f₂ : X₂ ⟶ Y₂<VAR>X₃ Y₃ : GradedObject I₃ C₃<VAR>f₃ : X₃ ⟶ Y₃<VAR>inst✝¹ : ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p<VAR>inst✝ : ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).HasMap p<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₃ : I₃<VAR>j : J<VAR>h : p (i₁, i₂, i₃) = j<GOAL>((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).ιMapObj p (i₁, i₂, i₃) j h ≫ mapMap ((((mapTrifunctor F I₁ I₂ I₃).map f₁).app X₂).app X₃ ≫ (((mapTrifunctor F I₁ I₂ I₃).obj Y₁).map f₂).app X₃ ≫ (((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).map f₃) p j = ((F.map (f₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫ ((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃) ≫ ((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃) ≫ ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>C₂₃ : Type u_6<VAR>inst✝⁷ : Category.{u_11, u_1} C₁<VAR>inst✝⁶ : Category.{u_12, u_2} C₂<VAR>inst✝⁵ : Category.{u_13, u_3} C₃<VAR>inst✝⁴ : Category.{u_14, u_4} C₄<VAR>inst✝³ : Category.{?u.57419, u_5} C₁₂<VAR>inst✝² : Category.{?u.57423, u_6} C₂₃<VAR>F F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>p : I₁ × I₂ × I₃ → J<VAR>X₁ Y₁ : GradedObject I₁ C₁<VAR>f₁ : X₁ ⟶ Y₁<VAR>X₂ Y₂ : GradedObject I₂ C₂<VAR>f₂ : X₂ ⟶ Y₂<VAR>X₃ Y₃ : GradedObject I₃ C₃<VAR>f₃ : X₃ ⟶ Y₃<VAR>inst✝¹ : ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p<VAR>inst✝ : ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).HasMap p<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₃ : I₃<VAR>j : J<VAR>h : p (i₁, i₂, i₃) = j<GOAL>((((mapTrifunctor F I₁ I₂ I₃).map f₁).app X₂).app X₃ ≫ (((mapTrifunctor F I₁ I₂ I₃).obj Y₁).map f₂).app X₃ ≫ (((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).map f₃) (i₁, i₂, i₃) ≫ ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h = ((F.map (f₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫ ((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃) ≫ ((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃) ≫ ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>C₂₃ : Type u_6<VAR>inst✝⁷ : Category.{u_11, u_1} C₁<VAR>inst✝⁶ : Category.{u_12, u_2} C₂<VAR>inst✝⁵ : Category.{u_13, u_3} C₃<VAR>inst✝⁴ : Category.{u_14, u_4} C₄<VAR>inst✝³ : Category.{?u.57419, u_5} C₁₂<VAR>inst✝² : Category.{?u.57423, u_6} C₂₃<VAR>F F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>p : I₁ × I₂ × I₃ → J<VAR>X₁ Y₁ : GradedObject I₁ C₁<VAR>f₁ : X₁ ⟶ Y₁<VAR>X₂ Y₂ : GradedObject I₂ C₂<VAR>f₂ : X₂ ⟶ Y₂<VAR>X₃ Y₃ : GradedObject I₃ C₃<VAR>f₃ : X₃ ⟶ Y₃<VAR>inst✝¹ : ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p<VAR>inst✝ : ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).HasMap p<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₃ : I₃<VAR>j : J<VAR>h : p (i₁, i₂, i₃) = j<GOAL>(((F.map (f₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫ ((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃) ≫ ((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃)) ≫ (((mapTrifunctorObj F Y₁ I₂ I₃).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h = ((F.map (f₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫ ((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃) ≫ ((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃) ≫ (((mapTrifunctorObj F Y₁ I₂ I₃).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x y : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsUpperSet s<VAR>hx : x ∈ closure s<VAR>hδ : 0 < δ<GOAL>∃ y, closedBall y (δ / 4) ⊆ closedBall x δ ∧ closedBall y (δ / 4) ⊆ interior s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x y : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsUpperSet s<VAR>hx : x ∈ closure s<VAR>hδ : 0 < δ<GOAL>δ / 4 + dist (x + const ι (3 / 4 * δ)) x ≤ δ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x y : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsUpperSet s<VAR>hx : x ∈ closure s<VAR>hδ : 0 < δ<GOAL>closedBall (x + const ι (3 / 4 * δ)) (δ / 4) ⊆ interior s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x y✝ : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsUpperSet s<VAR>hx : x ∈ closure s<VAR>hδ : 0 < δ<VAR>y : ι → ℝ<VAR>hy : y ∈ s<VAR>hxy : dist x y < δ / 4<GOAL>closedBall (x + const ι (3 / 4 * δ)) (δ / 4) ⊆ interior s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x y✝ : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsUpperSet s<VAR>hx : x ∈ closure s<VAR>hδ : 0 < δ<VAR>y : ι → ℝ<VAR>hy : y ∈ s<VAR>hxy : dist x y < δ / 4<VAR>z : ι → ℝ<VAR>hz : z ∈ closedBall (x + const ι (3 / 4 * δ)) (δ / 4)<VAR>i : ι<GOAL>y i < z i
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x y✝ : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsUpperSet s<VAR>hx : x ∈ closure s<VAR>hδ : 0 < δ<VAR>y : ι → ℝ<VAR>hy : y ∈ s<VAR>hxy : dist x y < δ / 4<VAR>z : ι → ℝ<VAR>hz : ‖x + const ι (3 / 4 * δ) - z‖ ≤ δ / 4<VAR>i : ι<GOAL>y i < z i
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x y✝ : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsUpperSet s<VAR>hx : x ∈ closure s<VAR>hδ : 0 < δ<VAR>y : ι → ℝ<VAR>hy : y ∈ s<VAR>hxy : ‖x - y‖ < δ / 4<VAR>z : ι → ℝ<VAR>hz : ‖x + const ι (3 / 4 * δ) - z‖ ≤ δ / 4<VAR>i : ι<GOAL>y i < z i
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x y✝ : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsUpperSet s<VAR>hx : x ∈ closure s<VAR>hδ : 0 < δ<VAR>y : ι → ℝ<VAR>hy : y ∈ s<VAR>z : ι → ℝ<VAR>hz : ‖x + const ι (3 / 4 * δ) - z‖ ≤ δ / 4<VAR>i : ι<VAR>hxy : ‖(x - y) i‖ ≤ δ / 4<GOAL>y i < z i
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x y✝ : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsUpperSet s<VAR>hx : x ∈ closure s<VAR>hδ : 0 < δ<VAR>y : ι → ℝ<VAR>hy : y ∈ s<VAR>z : ι → ℝ<VAR>i : ι<VAR>hxy : ‖(x - y) i‖ ≤ δ / 4<VAR>hz : ‖(x + const ι (3 / 4 * δ) - z) i‖ ≤ δ / 4<GOAL>y i < z i
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x y✝ : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsUpperSet s<VAR>hx : x ∈ closure s<VAR>hδ : 0 < δ<VAR>y : ι → ℝ<VAR>hy : y ∈ s<VAR>z : ι → ℝ<VAR>i : ι<VAR>hxy : |x i - y i| ≤ δ / 4<VAR>hz : |x i + 3 / 4 * δ - z i| ≤ δ / 4<GOAL>y i < z i
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x y✝ : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsUpperSet s<VAR>hx : x ∈ closure s<VAR>hδ : 0 < δ<VAR>y : ι → ℝ<VAR>hy : y ∈ s<VAR>z : ι → ℝ<VAR>i : ι<VAR>hxy : x i - y i ≤ δ / 4 ∧ y i - x i ≤ δ / 4<VAR>hz : x i + 3 / 4 * δ - z i ≤ δ / 4 ∧ z i - (x i + 3 / 4 * δ) ≤ δ / 4<GOAL>y i < z i
<VAR>s : ℝ<VAR>hs : -1 ≤ s<VAR>p : ℝ<VAR>hp1 : 0 ≤ p<VAR>hp2 : p ≤ 1<GOAL>(1 + s) ^ p ≤ 1 + p * s
<VAR>s : ℝ<VAR>hs : -1 ≤ s<VAR>hp1 : 0 ≤ 0<VAR>hp2 : 0 ≤ 1<GOAL>(1 + s) ^ 0 ≤ 1 + 0 * s
<VAR>s : ℝ<VAR>hs : -1 ≤ s<VAR>p : ℝ<VAR>hp1✝ : 0 ≤ p<VAR>hp2 : p ≤ 1<VAR>hp1 : 0 < p<GOAL>(1 + s) ^ p ≤ 1 + p * s
<VAR>s : ℝ<VAR>hs : -1 ≤ s<VAR>hp1✝ : 0 ≤ 1<VAR>hp2 : 1 ≤ 1<VAR>hp1 : 0 < 1<GOAL>(1 + s) ^ 1 ≤ 1 + 1 * s
<VAR>s : ℝ<VAR>hs : -1 ≤ s<VAR>p : ℝ<VAR>hp1✝ : 0 ≤ p<VAR>hp2✝ : p ≤ 1<VAR>hp1 : 0 < p<VAR>hp2 : p < 1<GOAL>(1 + s) ^ p ≤ 1 + p * s
<VAR>s : ℝ<VAR>hs : -1 ≤ s<VAR>p : ℝ<VAR>hp1✝ : 0 ≤ p<VAR>hp2✝ : p ≤ 1<VAR>hp1 : 0 < p<VAR>hp2 : p < 1<VAR>hs' : ¬s = 0<GOAL>(1 + s) ^ p ≤ 1 + p * s
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝¹ : Category.{?u.11466, u_1} D<VAR>P : MorphismProperty C<VAR>hP : P.RespectsIso<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝ : IsIso f<VAR>h : P (f ≫ g)<GOAL>P g
<VAR>R : Type u_1<VAR>inst✝⁴ : LinearOrderedCommRing R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>ι : Type u_3<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>e : Basis ι R M<VAR>f : M ≃ₗ[R] M<GOAL>(e.map f).orientation = -e.orientation ↔ LinearMap.det ↑f < 0
<VAR>M : Type u_1<VAR>inst✝³ : Mul M<VAR>inst✝² : Finite M<VAR>G : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>H : Subgroup G<VAR>n : ℕ<VAR>h0 : ¬n = 0<VAR>h1 : ¬n = 1<GOAL>commProb (Product (reciprocalFactors n)) = 1 / ↑n
<VAR>M : Type u_1<VAR>inst✝³ : Mul M<VAR>inst✝² : Finite M<VAR>G : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>H : Subgroup G<VAR>n : ℕ<VAR>h0 : ¬n = 0<VAR>h1 : ¬n = 1<VAR>h2 : Even n<GOAL>commProb (Product (reciprocalFactors n)) = 1 / ↑n
<VAR>M : Type u_1<VAR>inst✝³ : Mul M<VAR>inst✝² : Finite M<VAR>G : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>H : Subgroup G<VAR>n : ℕ<VAR>h0 : ¬n = 0<VAR>h1 : ¬n = 1<VAR>h2 : Odd n<GOAL>commProb (Product (reciprocalFactors n)) = 1 / ↑n
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₃ : Type u_9<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>inst✝¹¹ : Ring R<VAR>inst✝¹⁰ : Ring R₂<VAR>inst✝⁹ : Ring R₃<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : AddCommGroup M₃<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R₂ M₂<VAR>inst✝³ : Module R₃ M₃<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝² : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>F : Type u_12<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>f : F<VAR>x y : M<GOAL>x - y ∈ ker f ↔ f x = f y
<VAR>d : ℤ<VAR>a₁ : Solution₁ d<VAR>h : IsFundamental a₁<VAR>a : Solution₁ d<GOAL>∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n
<VAR>d : ℤ<VAR>a₁ : Solution₁ d<VAR>h : IsFundamental a₁<VAR>a b : Solution₁ d<VAR>hbx : 0 < b.x<VAR>hby : 0 ≤ b.y<VAR>hb : a ∈ {b, b⁻¹, -b, -b⁻¹}<GOAL>∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n
<VAR>d : ℤ<VAR>a₁ : Solution₁ d<VAR>h : IsFundamental a₁<VAR>a b : Solution₁ d<VAR>hbx : 0 < b.x<VAR>hby : 0 ≤ b.y<VAR>hb : a ∈ {b, b⁻¹, -b, -b⁻¹}<VAR>n : ℕ<VAR>hn : b = a₁ ^ n<GOAL>∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<GOAL>reindex R s (Equiv.refl ι) = LinearEquiv.refl R (⨂[R] (i : ι), s i)
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<GOAL>↑(reindex R s (Equiv.refl ι)) = ↑(LinearEquiv.refl R (⨂[R] (i : ι), s i))
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>x✝ : (i : ι) → s i<GOAL>((↑(reindex R s (Equiv.refl ι))).compMultilinearMap (tprod R)) x✝ = ((↑(LinearEquiv.refl R (⨂[R] (i : ι), s i))).compMultilinearMap (tprod R)) x✝
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>x✝ : (i : ι) → s i<GOAL>(LinearEquiv.ofLinear (lift { toFun := ⇑(tprod R) ∘ ⇑(Equiv.piCongrLeft' s (Equiv.refl ι)), map_add' := ⋯, map_smul' := ⋯ }) (lift ({ toFun := fun f => { toFun := ⇑f ∘ ⇑(Equiv.piCongrLeft' s (Equiv.refl ι)).symm, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯, invFun := fun f => { toFun := ⇑f ∘ ⇑(Equiv.piCongrLeft' s (Equiv.refl ι)), map_add' := ⋯, map_smul' := ⋯ }, left_inv := ⋯, right_inv := ⋯ } (tprod R))) ⋯ ⋯) ((tprod R) x✝) = (tprod R) x✝
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>x✝ : (i : ι) → s i<GOAL>{ toFun := ⇑(tprod R) ∘ ⇑(Equiv.piCongrLeft' s (Equiv.refl ι)), map_add' := ⋯, map_smul' := ⋯ } x✝ = (tprod R) x✝
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : DecidableEq (Associates α)<VAR>a : Associates α<VAR>ha : a ≠ 0<VAR>b : Associates α<VAR>hb : b ≠ 0<VAR>hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d<VAR>p : Associates α<VAR>hp : Irreducible p<GOAL>p.count a.factors = 0 ∨ p.count b.factors = 0
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : DecidableEq (Associates α)<VAR>a : Associates α<VAR>ha : a ≠ 0<VAR>b : Associates α<VAR>hb : b ≠ 0<VAR>hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d<VAR>p : Associates α<VAR>hp : Irreducible p<GOAL>p.count a.factors ≠ 0 → p.count b.factors = 0
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : DecidableEq (Associates α)<VAR>a : Associates α<VAR>ha : a ≠ 0<VAR>b : Associates α<VAR>hb : b ≠ 0<VAR>hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d<VAR>p : Associates α<VAR>hp : Irreducible p<VAR>hca : p.count a.factors ≠ 0<GOAL>p.count b.factors = 0
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : DecidableEq (Associates α)<VAR>a : Associates α<VAR>ha : a ≠ 0<VAR>b : Associates α<VAR>hb : b ≠ 0<VAR>p : Associates α<VAR>hp : Irreducible p<VAR>hca : p.count a.factors ≠ 0<VAR>hcb : p.count b.factors ≠ 0<GOAL>∃ d, d ∣ a ∧ d ∣ b ∧ Prime d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>hl : l.HasBasis p s<VAR>hl' : l'.HasBasis p' s'<GOAL>(∀ {i : PProd ι ι'}, p i.fst ∧ p' i.snd → (s i.fst ∩ s' i.snd).Nonempty) ↔ ∀ ⦃i : ι⦄, p i → ∀ ⦃i' : ι'⦄, p' i' → (s i ∩ s' i').Nonempty
<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>ha : P.a = 0<GOAL>P.toPoly = C P.b * X ^ 2 + C P.c * X + C P.d
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p q : RelSeries r<VAR>connect : r p.last q.head<VAR>i : Fin (p.length + 1)<GOAL>{ length := p.length + q.length + 1, toFun := Fin.append p.toFun q.toFun ∘ Fin.cast ⋯, step := ⋯ }.toFun (Fin.cast ⋯ (Fin.castAdd (q.length + 1) i)) = p.toFun i
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p q : RelSeries r<VAR>connect : r p.last q.head<VAR>i : Fin (p.length + 1)<GOAL>Fin.append p.toFun q.toFun (Fin.cast ⋯ (Fin.cast ⋯ (Fin.castAdd (q.length + 1) i))) = p.toFun i
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>a b : M<VAR>d : ↥S<GOAL>f.mk' a d = f.mk' b d ↔ ∃ c, ↑c * a = ↑c * b
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>a b : M<VAR>d : ↥S<GOAL>f.toMap a * f.toMap ↑d = f.toMap b * f.toMap ↑d ↔ f.toMap a = f.toMap b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>i : ι<GOAL>f i ≤ (iSup (succ ∘ card ∘ f)).ord
<VAR>α : Type u<VAR>β : Type u_1<VAR>m n✝ : ℕ<VAR>s : Finset ℕ<VAR>hm : 2 ≤ m<VAR>n : ℕ<GOAL>∑ k ∈ range n, m ^ k = (m ^ n - 1) / (m - 1)
<VAR>α : Type u<VAR>β : Type u_1<VAR>m n✝ : ℕ<VAR>s : Finset ℕ<VAR>hm : 2 ≤ m<VAR>n : ℕ<GOAL>m ^ n = (∑ k ∈ range n, m ^ k) * (m - 1) + 1
<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>p₁ p₂ p₃ : P<VAR>h : ∠ p₁ p₂ p₃ = π / 2<VAR>h0 : p₁ = p₂ ∨ p₃ ≠ p₂<GOAL>dist p₃ p₂ / Real.cos (∠ p₂ p₃ p₁) = dist p₁ p₃
<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>p₁ p₂ p₃ : P<VAR>h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫_ℝ = 0<VAR>h0 : p₁ = p₂ ∨ p₃ ≠ p₂<GOAL>dist p₃ p₂ / Real.cos (∠ p₂ p₃ p₁) = dist p₁ p₃
<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>p₁ p₂ p₃ : P<VAR>h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫_ℝ = 0<VAR>h0 : p₂ -ᵥ p₃ ≠ 0 ∨ p₁ -ᵥ p₂ = 0<GOAL>dist p₃ p₂ / Real.cos (∠ p₂ p₃ p₁) = dist p₁ p₃
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : NormedGroup E<VAR>inst✝ : NormedGroup F<VAR>a b : E<GOAL>‖a / b‖ = 0 ↔ a = b
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : NormedAddCommGroup E''<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>f✝ f' : G → E<VAR>g✝ g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>f : ℝ → E<VAR>g : ℝ → E'<VAR>μ ν : Measure ℝ<VAR>inst✝³ : SFinite μ<VAR>inst✝² : SFinite ν<VAR>inst✝¹ : μ.IsAddRightInvariant<VAR>inst✝ : NoAtoms ν<VAR>hf : IntegrableOn f (Ioi 0) ν<VAR>hg : IntegrableOn g (Ioi 0) μ<VAR>L : E →L[ℝ] E' →L[ℝ] F<GOAL>Integrable (posConvolution f g L ν) μ
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : NormedAddCommGroup E''<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>f✝ f' : G → E<VAR>g✝ g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>f : ℝ → E<VAR>g : ℝ → E'<VAR>μ ν : Measure ℝ<VAR>inst✝³ : SFinite μ<VAR>inst✝² : SFinite ν<VAR>inst✝¹ : μ.IsAddRightInvariant<VAR>inst✝ : NoAtoms ν<VAR>hf : Integrable ((Ioi 0).indicator f) ν<VAR>hg : Integrable ((Ioi 0).indicator g) μ<VAR>L : E →L[ℝ] E' →L[ℝ] F<GOAL>Integrable (posConvolution f g L ν) μ
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : NormedAddCommGroup E''<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>f✝ f' : G → E<VAR>g✝ g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>f : ℝ → E<VAR>g : ℝ → E'<VAR>μ ν : Measure ℝ<VAR>inst✝³ : SFinite μ<VAR>inst✝² : SFinite ν<VAR>inst✝¹ : μ.IsAddRightInvariant<VAR>inst✝ : NoAtoms ν<VAR>hf : Integrable ((Ioi 0).indicator f) ν<VAR>hg : Integrable ((Ioi 0).indicator g) μ<VAR>L : E →L[ℝ] E' →L[ℝ] F<GOAL>Integrable ((Ioi 0).indicator f ⋆[L, ν] (Ioi 0).indicator g) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E✝ : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : PseudoEMetricSpace X<VAR>μ : Measure X<VAR>E : Set X<VAR>E_mble : MeasurableSet E<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<GOAL>μ E ≤ ∫⁻ (x : X), ↑((thickenedIndicator δ_pos E) x) ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E✝ : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : PseudoEMetricSpace X<VAR>μ : Measure X<VAR>E : Set X<VAR>E_mble : MeasurableSet E<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>x✝ : X<GOAL>↑((thickenedIndicator δ_pos E) x✝) = thickenedIndicatorAux δ E x✝
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E✝ : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : PseudoEMetricSpace X<VAR>μ : Measure X<VAR>E : Set X<VAR>E_mble : MeasurableSet E<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>x✝ : X<GOAL>↑(thickenedIndicatorAux δ E x✝).toNNReal = thickenedIndicatorAux δ E x✝
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>c : ℝ<VAR>hc : c ≠ 0<VAR>x : ℝ<GOAL>gaussianPDFReal μ v (c⁻¹ * x) = |c| * gaussianPDFReal (c * μ) (⟨c ^ 2, ⋯⟩ * v) x
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>c : ℝ<VAR>hc : c ≠ 0<VAR>x : ℝ<GOAL>(√↑v)⁻¹ * (√(2 * π))⁻¹ * rexp (-(c⁻¹ * x - μ) ^ 2 / (2 * ↑v)) = |c| * ((√(2 * π * (c ^ 2 * ↑v)))⁻¹ * rexp (-(x - c * μ) ^ 2 / (2 * (c ^ 2 * ↑v))))
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>c : ℝ<VAR>hc : c ≠ 0<VAR>x : ℝ<GOAL>(√↑v)⁻¹ * (√(2 * π))⁻¹ * rexp (-(c⁻¹ * x - μ) ^ 2 / (2 * ↑v)) = |c| * (√(2 * π * (c ^ 2 * ↑v)))⁻¹ * rexp (-(x - c * μ) ^ 2 / (2 * (c ^ 2 * ↑v)))
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : AddMonoid A<VAR>x : A<GOAL>↑(Submonoid.powers (Multiplicative.ofAdd x)) = ⇑Multiplicative.ofAdd '' ↑(AddSubmonoid.multiples x)
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : AddMonoid A<VAR>x : A<GOAL>⇑Multiplicative.ofAdd.symm '' ↑(Submonoid.powers (Multiplicative.ofAdd x)) = ↑(AddSubmonoid.multiples x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : Nonempty β<VAR>f : α → γ<VAR>g : β → δ<GOAL>Bijective (map f g) ↔ Bijective f ∧ Bijective g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : Nonempty β<VAR>f : α → γ<VAR>g : β → δ<VAR>this : Nonempty γ<GOAL>Bijective (map f g) ↔ Bijective f ∧ Bijective g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : Nonempty β<VAR>f : α → γ<VAR>g : β → δ<VAR>this✝ : Nonempty γ<VAR>this : Nonempty δ<GOAL>Bijective (map f g) ↔ Bijective f ∧ Bijective g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : SuccOrder α<VAR>a : α<VAR>inst✝ : NoMaxOrder α<GOAL>a ⋖ succ a
<VAR>α : Type u_1<VAR>inst✝ : SeminormedCommGroup α<VAR>n : ℤ<VAR>a : α<GOAL>‖a ^ n‖ ≤ ‖n‖ * ‖a‖
<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>r : ℝ<GOAL>(o.oangle x (y - r • x)).sign = (o.oangle x y).sign
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>M : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} M<VAR>inst✝ : MonoidalCategory M<VAR>F : MonoidalFunctor M (C ⥤ C)<VAR>m₁ m₂ m₃ : M<VAR>X : C<GOAL>(F.obj m₃).map ((F.μ m₁ m₂).app X) ≫ (F.μ (m₁ ⊗ m₂) m₃).app X ≫ (F.map (α_ m₁ m₂ m₃).hom).app X = (F.μ m₂ m₃).app ((F.obj m₁).obj X) ≫ (F.μ m₁ (m₂ ⊗ m₃)).app X