ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>H : Subgroup G<VAR>inst✝² : H.Normal<VAR>η : Type u_2<VAR>Gs : η → Type u_3<VAR>inst✝¹ : (i : η) → Group (Gs i)<VAR>inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)<VAR>n : ℕ<VAR>h : ∀ (i : η), Group.nilpotencyClass (Gs i) ≤ n<VAR>i : η<GOAL>lowerCentralSeries (Gs i) n = ⊥
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : PseudoMetricSpace β<VAR>inst✝² : Zero β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : ZeroAtInftyContinuousMapClass F α β<VAR>f g : α →C₀ β<VAR>h : f.toBCF = g.toBCF<VAR>x : α<GOAL>f x = g x
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝¹ : HasHomotopyCofiber φ<VAR>inst✝ : DecidableRel c.Rel<VAR>i : ι<VAR>hi : ¬c.Rel i (c.next i)<VAR>A : C<VAR>f g : X φ i ⟶ A<VAR>h : inrX φ i ≫ f = inrX φ i ≫ g<GOAL>f = g
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝¹ : HasHomotopyCofiber φ<VAR>inst✝ : DecidableRel c.Rel<VAR>i : ι<VAR>hi : ¬c.Rel i (c.next i)<VAR>A : C<VAR>f g : X φ i ⟶ A<VAR>h : inrX φ i ≫ f = inrX φ i ≫ g<GOAL>(XIso φ i hi).inv ≫ f = (XIso φ i hi).inv ≫ g
<VAR>F : Type u_1<VAR>inst✝⁶ : Field F<VAR>E : Type u_2<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>S : Set E<VAR>α : E<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>E1 E2 : IntermediateField K L<VAR>inst✝ : Algebra.IsAlgebraic K ↥E2<GOAL>(E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
<VAR>F : Type u_1<VAR>inst✝⁶ : Field F<VAR>E : Type u_2<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>S : Set E<VAR>α : E<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>E1 E2 : IntermediateField K L<VAR>inst✝ : Algebra.IsAlgebraic K ↥E2<VAR>this : (adjoin ↥E1 ↑E2).toSubalgebra = Algebra.adjoin ↥E1 ↑E2<GOAL>(E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
<VAR>F : Type u_1<VAR>inst✝⁶ : Field F<VAR>E : Type u_2<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>S : Set E<VAR>α : E<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>E1 E2 : IntermediateField K L<VAR>inst✝ : Algebra.IsAlgebraic K ↥E2<VAR>this : Subalgebra.restrictScalars K (adjoin ↥E1 ↑E2).toSubalgebra = Subalgebra.restrictScalars K (Algebra.adjoin ↥E1 ↑E2)<GOAL>(E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
<VAR>F : Type u_1<VAR>inst✝⁶ : Field F<VAR>E : Type u_2<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>S : Set E<VAR>α : E<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>E1 E2 : IntermediateField K L<VAR>inst✝ : Algebra.IsAlgebraic K ↥E2<VAR>this : (adjoin K (↑E1 ∪ ↑E2)).toSubalgebra = Algebra.adjoin K (↑E1.toSubalgebra ∪ ↑E2)<GOAL>(E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t✝ u v s t : Set α<VAR>hs : IsPreconnected s<VAR>ht : IsPreconnected t<VAR>x : α<VAR>hxs : x ∈ s<VAR>hxt : x ∈ t<GOAL>IsPreconnected (s ∪ t)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>f : α ↪ β<VAR>s : Finset β<VAR>t : Finset α<GOAL>s ⊆ map f t ↔ ∃ u ⊆ t, s = map f u
<VAR>K : Type uK<VAR>V : Type uV<VAR>inst✝³ : CommRing K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : Free K V<GOAL>Function.Injective (Submodule.map (eval K V))
<VAR>K : Type uK<VAR>V : Type uV<VAR>inst✝³ : CommRing K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : Free K V<GOAL>Function.Injective ⇑(eval K V)
<VAR>K : Type uK<VAR>V : Type uV<VAR>inst✝³ : CommRing K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : Free K V<GOAL>ker (eval K V) = ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I : Ideal α<VAR>m n k : ℕ<VAR>ha : a ^ m ∈ I<VAR>hb : b ^ n ∈ I<VAR>hk : m + n ≤ k + 1<GOAL>(a + b) ^ k ∈ I
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I : Ideal α<VAR>m n k : ℕ<VAR>ha : a ^ m ∈ I<VAR>hb : b ^ n ∈ I<VAR>hk : m + n ≤ k + 1<GOAL>∑ m ∈ Finset.range (k + 1), a ^ m * b ^ (k - m) * ↑(k.choose m) ∈ I
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I : Ideal α<VAR>m n k : ℕ<VAR>ha : a ^ m ∈ I<VAR>hb : b ^ n ∈ I<VAR>hk : m + n ≤ k + 1<GOAL>∀ c ∈ Finset.range (k + 1), a ^ c * b ^ (k - c) * ↑(k.choose c) ∈ I
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I : Ideal α<VAR>m n k : ℕ<VAR>ha : a ^ m ∈ I<VAR>hb : b ^ n ∈ I<VAR>hk : m + n ≤ k + 1<VAR>c : ℕ<VAR>a✝ : c ∈ Finset.range (k + 1)<GOAL>a ^ c * b ^ (k - c) * ↑(k.choose c) ∈ I
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I : Ideal α<VAR>m n k : ℕ<VAR>ha : a ^ m ∈ I<VAR>hb : b ^ n ∈ I<VAR>hk : m + n ≤ k + 1<VAR>c : ℕ<VAR>a✝ : c ∈ Finset.range (k + 1)<GOAL>a ^ c * b ^ (k - c) ∈ I
<VAR>a₀ a₁ a₂ : Type u<GOAL>(sum fun i => #(Sequence₂ a₀ a₁ a₂ i)) = #a₀ + #a₁ + #a₂
<VAR>a₀ a₁ a₂ : Type u<GOAL>#(Sequence₂ a₀ a₁ a₂ 0) + (#(Sequence₂ a₀ a₁ a₂ (0 + 1)) + (#(Sequence₂ a₀ a₁ a₂ (0 + 1 + 1)) + sum fun i => #(Sequence₂ a₀ a₁ a₂ (i + 1 + 1 + 1)))) = #a₀ + #a₁ + #a₂
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝³ : Semiring R<VAR>inst✝² : Semiring S<VAR>inst✝¹ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f✝ : F<VAR>I✝ J : Ideal R<VAR>K L : Ideal S<VAR>G : Type u_2<VAR>inst✝ : FunLike G S R<VAR>rcg : RingHomClass G S R<VAR>ι : Sort u_3<VAR>I : Ideal R<VAR>f : R ≃+* S<GOAL>comap (↑f) (comap (↑f.symm) I) = I
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>β' : Type u_5<VAR>γ : Type u_6<VAR>γ' : Type u_7<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>q : Type u_12<VAR>r : Type u_13<VAR>l' : Type u_14<VAR>m' : Type u_15<VAR>n' : Type u_16<VAR>p' : Type u_17<VAR>inst✝⁴ : Zero α<VAR>inst✝³ : Zero β<VAR>inst✝² : Zero γ<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : DecidableEq n<VAR>f : α → β → γ<VAR>hf₁ : ∀ (b : β), f 0 b = 0<VAR>hf₂ : ∀ (a : α), f a 0 = 0<VAR>a : m → α<VAR>b : n → β<VAR>i₁ : m<VAR>i₂ : n<VAR>j₁ : m<VAR>j₂ : n<GOAL>kroneckerMap f (diagonal a) (diagonal b) (i₁, i₂) (j₁, j₂) = diagonal (fun mn => f (a mn.1) (b mn.2)) (i₁, i₂) (j₁, j₂)
<VAR>K : Type u_1<VAR>inst✝⁷ : NormedLinearOrderedField K<VAR>inst✝⁶ : HasSolidNorm K<VAR>inst✝⁵ : FloorRing K<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace K E<VAR>inst✝² : FiniteDimensional K E<VAR>inst✝¹ : ProperSpace E<VAR>L : AddSubgroup E<VAR>inst✝ : DiscreteTopology ↥L<VAR>ι : Type u_3<VAR>hs : IsZlattice K L<VAR>b : Basis ι ℤ ↥L<GOAL>(span ℤ (Set.range ⇑(ofZlatticeBasis K L b))).toAddSubgroup = L
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝ : CommSemiring R<VAR>I : Ideal R<GOAL>zeroLocus ↑I ∈ irreducibleComponents (PrimeSpectrum R) ↔ I.radical ∈ minimalPrimes R
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝ : CommSemiring R<VAR>I : Ideal R<GOAL>zeroLocus ↑I ∈ irreducibleComponents (PrimeSpectrum R) ↔ vanishingIdeal (zeroLocus ↑I) ∈ minimalPrimes R
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝ : CommSemiring R<VAR>I : Ideal R<GOAL>closure (zeroLocus ↑I) ∈ irreducibleComponents (PrimeSpectrum R) ↔ vanishingIdeal (zeroLocus ↑I) ∈ minimalPrimes R
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<GOAL>HasSum (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)) z.arctan
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>this : HasSum (fun i => -I / 2 * ((-1) ^ (i + 1) * (z * I) ^ i / ↑i + (z * I) ^ i / ↑i)) (-I / 2 * (log (1 + z * I) + -log (1 - z * I)))<GOAL>HasSum (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)) z.arctan
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>this : HasSum (fun i => -I / 2 * (((-1) ^ (i + 1) + 1) * (z * I) ^ i / ↑i)) (-I / 2 * log ((1 + z * I) / (1 - z * I)))<GOAL>HasSum (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)) z.arctan
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>this : HasSum ((fun i => -I / 2 * (((-1) ^ (i + 1) + 1) * (z * I) ^ i / ↑i)) ∘ ⇑(Nat.divModEquiv 2).symm) (-I / 2 * log ((1 + z * I) / (1 - z * I)))<GOAL>HasSum (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)) z.arctan
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>this : HasSum (fun x => -I / 2 * (((-1) ^ (x.1 * 2 + ↑x.2 + 1) + 1) * (z * I) ^ (x.1 * 2 + ↑x.2) / ↑(x.1 * 2 + ↑x.2))) (-I / 2 * log ((1 + z * I) / (1 - z * I)))<GOAL>HasSum (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)) z.arctan
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>this : HasSum (fun x => -I / 2 * (((-1) ^ (2 * x.1 + ↑x.2 + 1) + 1) * (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2))) (-I / 2 * log ((1 + z * I) / (1 - z * I)))<GOAL>HasSum (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)) z.arctan
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>this : HasSum (fun x => -I / 2 * (((-1) ^ (2 * x.1 + ↑x.2 + 1) + 1) * (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2))) (-I / 2 * log ((1 + z * I) / (1 - z * I)))<VAR>k : ℕ<GOAL>HasSum (fun c => -I / 2 * (((-1) ^ (2 * (k, c).1 + ↑(k, c).2 + 1) + 1) * (z * I) ^ (2 * (k, c).1 + ↑(k, c).2) / ↑(2 * (k, c).1 + ↑(k, c).2))) ((-1) ^ k * z ^ (2 * k + 1) / ↑(2 * k + 1))
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>this : HasSum (fun x => -I / 2 * (((-1) ^ (2 * x.1 + ↑x.2 + 1) + 1) * (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2))) (-I / 2 * log ((1 + z * I) / (1 - z * I)))<VAR>k : ℕ<GOAL>HasSum (fun c => -I / 2 * (((-1) ^ (2 * k + ↑c + 1) + 1) * (z * I) ^ (2 * k + ↑c) / ↑(2 * k + ↑c))) ((-1) ^ k * z ^ (2 * k + 1) / ↑(2 * k + 1))
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>this : HasSum (fun x => -I / 2 * (((-1) ^ (2 * x.1 + ↑x.2 + 1) + 1) * (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2))) (-I / 2 * log ((1 + z * I) / (1 - z * I)))<VAR>k : ℕ<GOAL>(-1) ^ k * z ^ (2 * k + 1) / ↑(2 * k + 1) = ∑ b : Fin 2, -I / 2 * (((-1) ^ (2 * k + ↑b + 1) + 1) * (z * I) ^ (2 * k + ↑b) / ↑(2 * k + ↑b))
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>this : HasSum (fun x => -I / 2 * (((-1) ^ (2 * x.1 + ↑x.2 + 1) + 1) * (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2))) (-I / 2 * log ((1 + z * I) / (1 - z * I)))<VAR>k : ℕ<GOAL>(-1) ^ k * z ^ (2 * k + 1) / ↑(2 * k + 1) = -I * (z * I) ^ (2 * k + 1) / ↑(2 * k + 1)
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>this : HasSum (fun x => -I / 2 * (((-1) ^ (2 * x.1 + ↑x.2 + 1) + 1) * (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2))) (-I / 2 * log ((1 + z * I) / (1 - z * I)))<VAR>k : ℕ<GOAL>(-1) ^ k * z ^ (2 * k + 1) = -I * (z * I) ^ (2 * k + 1)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle (x - y) x).tan = ‖y‖ / ‖x‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (-o).oangle y x = ↑(π / 2)<GOAL>((-o).oangle x (x - y)).tan = ‖y‖ / ‖x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : CompleteLattice β<VAR>f : CompleteLatticeHom α β<VAR>L : CompleteSublattice α<VAR>S : Set ↥L<GOAL>↑(sSup S) = ⨆ N ∈ S, ↑N
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁴ : OrderedCommRing R<VAR>inst✝¹³ : StarRing R<VAR>inst✝¹² : MetricSpace R<VAR>inst✝¹¹ : TopologicalRing R<VAR>inst✝¹⁰ : ContinuousStar R<VAR>inst✝⁹ : ∀ (α : Type ?u.835033) [inst : TopologicalSpace α], StarOrderedRing C(α, R)<VAR>inst✝⁸ : TopologicalSpace A<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : PartialOrder A<VAR>inst✝⁴ : StarOrderedRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : StarModule R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>inst✝ : NonnegSpectrumClass R A<VAR>a : A<VAR>ha : p a<VAR>f g : C(↑(spectrum R a), R)<GOAL>(cfcHom ha) f ≤ (cfcHom ha) g ↔ f ≤ g
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} A<VAR>inst✝² : Category.{v₂, u₂} B<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>inst✝ : Category.{v₄, u₄} D<VAR>G : A ⥤ C<VAR>H : B ⥤ D<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : A ⥤ B<VAR>R₂ : B ⥤ A<VAR>L₃ : C ⥤ D<VAR>R₃ : D ⥤ C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>α : L₂ ⟶ L₁<VAR>β : G ⋙ L₃ ⟶ L₂ ⋙ H<VAR>b : B<GOAL>((mateEquiv adj₁ adj₃) (leftAdjointConjugateSquare.vcomp α β)).app b = (rightAdjointConjugateSquare.vcomp ((conjugateEquiv adj₁ adj₂) α) ((mateEquiv adj₂ adj₃) β)).app b
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} A<VAR>inst✝² : Category.{v₂, u₂} B<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>inst✝ : Category.{v₄, u₄} D<VAR>G : A ⥤ C<VAR>H : B ⥤ D<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : A ⥤ B<VAR>R₂ : B ⥤ A<VAR>L₃ : C ⥤ D<VAR>R₃ : D ⥤ C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>α : L₂ ⟶ L₁<VAR>β : G ⋙ L₃ ⟶ L₂ ⋙ H<VAR>b : B<VAR>vcomp : (mateEquiv adj₁ adj₃) (leftAdjointSquare.vcomp (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) β) = rightAdjointSquare.vcomp ((mateEquiv adj₁ adj₂) (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)) ((mateEquiv adj₂ adj₃) β)<GOAL>((mateEquiv adj₁ adj₃) (leftAdjointConjugateSquare.vcomp α β)).app b = (rightAdjointConjugateSquare.vcomp ((conjugateEquiv adj₁ adj₂) α) ((mateEquiv adj₂ adj₃) β)).app b
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} A<VAR>inst✝² : Category.{v₂, u₂} B<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>inst✝ : Category.{v₄, u₄} D<VAR>G : A ⥤ C<VAR>H : B ⥤ D<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : A ⥤ B<VAR>R₂ : B ⥤ A<VAR>L₃ : C ⥤ D<VAR>R₃ : D ⥤ C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>α : L₂ ⟶ L₁<VAR>β : G ⋙ L₃ ⟶ L₂ ⋙ H<VAR>b : B<VAR>vcomp : (mateEquiv adj₁ adj₃) (whiskerLeft (𝟭 A) β ≫ whiskerRight (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) H) = whiskerRight ((mateEquiv adj₁ adj₂) (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)) G ≫ whiskerLeft (𝟭 B) ((mateEquiv adj₂ adj₃) β)<GOAL>((mateEquiv adj₁ adj₃) (β ≫ whiskerRight α H)).app b = (whiskerRight ((Trans.trans (Trans.trans (L₂.leftUnitor.homCongr L₁.rightUnitor).symm (mateEquiv adj₁ adj₂)) (R₁.rightUnitor.homCongr R₂.leftUnitor)) α) G ≫ (mateEquiv adj₂ adj₃) β).app b
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} A<VAR>inst✝² : Category.{v₂, u₂} B<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>inst✝ : Category.{v₄, u₄} D<VAR>G : A ⥤ C<VAR>H : B ⥤ D<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : A ⥤ B<VAR>R₂ : B ⥤ A<VAR>L₃ : C ⥤ D<VAR>R₃ : D ⥤ C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>α : L₂ ⟶ L₁<VAR>β : G ⋙ L₃ ⟶ L₂ ⋙ H<VAR>b : B<VAR>vcomp : (mateEquiv adj₁ adj₃) (whiskerLeft (𝟭 A) β ≫ whiskerRight (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) H) = whiskerRight ((mateEquiv adj₁ adj₂) (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)) G ≫ whiskerLeft (𝟭 B) ((mateEquiv adj₂ adj₃) β)<VAR>vcompb : ((mateEquiv adj₁ adj₃) (whiskerLeft (𝟭 A) β ≫ whiskerRight (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) H)).app b = (whiskerRight ((mateEquiv adj₁ adj₂) (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)) G ≫ whiskerLeft (𝟭 B) ((mateEquiv adj₂ adj₃) β)).app b<GOAL>((mateEquiv adj₁ adj₃) (β ≫ whiskerRight α H)).app b = (whiskerRight ((Trans.trans (Trans.trans (L₂.leftUnitor.homCongr L₁.rightUnitor).symm (mateEquiv adj₁ adj₂)) (R₁.rightUnitor.homCongr R₂.leftUnitor)) α) G ≫ (mateEquiv adj₂ adj₃) β).app b
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} A<VAR>inst✝² : Category.{v₂, u₂} B<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>inst✝ : Category.{v₄, u₄} D<VAR>G : A ⥤ C<VAR>H : B ⥤ D<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : A ⥤ B<VAR>R₂ : B ⥤ A<VAR>L₃ : C ⥤ D<VAR>R₃ : D ⥤ C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>α : L₂ ⟶ L₁<VAR>β : G ⋙ L₃ ⟶ L₂ ⋙ H<VAR>b : B<VAR>vcomp : (mateEquiv adj₁ adj₃) (whiskerLeft (𝟭 A) β ≫ whiskerRight (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) H) = whiskerRight ((mateEquiv adj₁ adj₂) (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)) G ≫ whiskerLeft (𝟭 B) ((mateEquiv adj₂ adj₃) β)<VAR>vcompb : adj₃.unit.app (G.obj (R₁.obj b)) ≫ R₃.map (β.app (R₁.obj b)) ≫ R₃.map (H.map (α.app (R₁.obj b))) ≫ R₃.map (H.map (adj₁.counit.app b)) = G.map (adj₂.unit.app (R₁.obj b)) ≫ G.map (R₂.map (α.app (R₁.obj b))) ≫ G.map (R₂.map (adj₁.counit.app b)) ≫ adj₃.unit.app (G.obj (R₂.obj b)) ≫ R₃.map (β.app (R₂.obj b)) ≫ R₃.map (H.map (adj₂.counit.app b))<GOAL>({ toFun := fun α => whiskerLeft (R₁ ⋙ G) adj₃.unit ≫ whiskerRight (whiskerLeft R₁ α) R₃ ≫ whiskerRight adj₁.counit (H ⋙ R₃), invFun := fun β => whiskerRight adj₁.unit (G ⋙ L₃) ≫ whiskerRight (whiskerLeft L₁ β) L₃ ≫ whiskerLeft (L₁ ⋙ H) adj₃.counit, left_inv := ⋯, right_inv := ⋯ } (β ≫ whiskerRight α H)).app b = (whiskerRight ((Trans.trans (Trans.trans (L₂.leftUnitor.homCongr L₁.rightUnitor).symm { toFun := fun α => whiskerLeft (R₁ ⋙ 𝟭 A) adj₂.unit ≫ whiskerRight (whiskerLeft R₁ α) R₂ ≫ whiskerRight adj₁.counit (𝟭 B ⋙ R₂), invFun := fun β => whiskerRight adj₁.unit (𝟭 A ⋙ L₂) ≫ whiskerRight (whiskerLeft L₁ β) L₂ ≫ whiskerLeft (L₁ ⋙ 𝟭 B) adj₂.counit, left_inv := ⋯, right_inv := ⋯ }) (R₁.rightUnitor.homCongr R₂.leftUnitor)) α) G ≫ { toFun := fun α => whiskerLeft (R₂ ⋙ G) adj₃.unit ≫ whiskerRight (whiskerLeft R₂ α) R₃ ≫ whiskerRight adj₂.counit (H ⋙ R₃), invFun := fun β => whiskerRight adj₂.unit (G ⋙ L₃) ≫ whiskerRight (whiskerLeft L₂ β) L₃ ≫ whiskerLeft (L₂ ⋙ H) adj₃.counit, left_inv := ⋯, right_inv := ⋯ } β).app b
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} A<VAR>inst✝² : Category.{v₂, u₂} B<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>inst✝ : Category.{v₄, u₄} D<VAR>G : A ⥤ C<VAR>H : B ⥤ D<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : A ⥤ B<VAR>R₂ : B ⥤ A<VAR>L₃ : C ⥤ D<VAR>R₃ : D ⥤ C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>α : L₂ ⟶ L₁<VAR>β : G ⋙ L₃ ⟶ L₂ ⋙ H<VAR>b : B<VAR>vcomp : (mateEquiv adj₁ adj₃) (whiskerLeft (𝟭 A) β ≫ whiskerRight (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) H) = whiskerRight ((mateEquiv adj₁ adj₂) (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)) G ≫ whiskerLeft (𝟭 B) ((mateEquiv adj₂ adj₃) β)<VAR>vcompb : adj₃.unit.app (G.obj (R₁.obj b)) ≫ R₃.map (β.app (R₁.obj b)) ≫ R₃.map (H.map (α.app (R₁.obj b))) ≫ R₃.map (H.map (adj₁.counit.app b)) = G.map (adj₂.unit.app (R₁.obj b)) ≫ G.map (R₂.map (α.app (R₁.obj b))) ≫ G.map (R₂.map (adj₁.counit.app b)) ≫ adj₃.unit.app (G.obj (R₂.obj b)) ≫ R₃.map (β.app (R₂.obj b)) ≫ R₃.map (H.map (adj₂.counit.app b))<GOAL>adj₃.unit.app (G.obj (R₁.obj b)) ≫ R₃.map (β.app (R₁.obj b)) ≫ R₃.map (H.map (α.app (R₁.obj b))) ≫ R₃.map (H.map (adj₁.counit.app b)) = G.map (adj₂.unit.app (R₁.obj b)) ≫ G.map (R₂.map (α.app (R₁.obj b))) ≫ G.map (R₂.map (adj₁.counit.app b)) ≫ adj₃.unit.app (G.obj (R₂.obj b)) ≫ R₃.map (β.app (R₂.obj b)) ≫ R₃.map (H.map (adj₂.counit.app b))
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<GOAL>angle (-x) y = π - angle x y
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<VAR>a : ℝ<GOAL>mellin (fun t => f (t ^ a)) s = |a|⁻¹ • mellin f (s / ↑a)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<GOAL>mellin (fun t => f (t ^ 0)) s = |0|⁻¹ • mellin f (s / ↑0)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<VAR>a : ℝ<VAR>ha : a ≠ 0<GOAL>mellin (fun t => f (t ^ a)) s = |a|⁻¹ • mellin f (s / ↑a)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<VAR>a : ℝ<VAR>ha : a ≠ 0<GOAL>∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) • f (t ^ a) = |a|⁻¹ • ∫ (t : ℝ) in Ioi 0, ↑t ^ (s / ↑a - 1) • f t
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<VAR>a : ℝ<VAR>ha : a ≠ 0<GOAL>∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) • f (t ^ a) = ∫ (a_1 : ℝ) in Ioi 0, |a|⁻¹ • (|a| * a_1 ^ (a - 1)) • ↑(a_1 ^ a) ^ (s / ↑a - 1) • f (a_1 ^ a)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<VAR>a : ℝ<VAR>ha : a ≠ 0<VAR>t : ℝ<VAR>ht : t ∈ Ioi 0<GOAL>↑t ^ (s - 1) • f (t ^ a) = |a|⁻¹ • (|a| * t ^ (a - 1)) • ↑(t ^ a) ^ (s / ↑a - 1) • f (t ^ a)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<VAR>a : ℝ<VAR>ha : a ≠ 0<VAR>t : ℝ<VAR>ht : t ∈ Ioi 0<GOAL>↑t ^ (s - 1) • f (t ^ a) = (↑(t ^ (a - 1)) * ↑(t ^ a) ^ (s / ↑a - 1)) • f (t ^ a)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : OrderedAddCommMonoid α<VAR>inst✝² : SMul 𝕜 α<VAR>inst✝¹ : OrderedAddCommMonoid β<VAR>inst✝ : SMul 𝕜 β<VAR>f : α ≃o β<VAR>hf : StrictConvexOn 𝕜 univ ⇑f<GOAL>StrictConcaveOn 𝕜 univ ⇑f.symm
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : OrderedAddCommMonoid α<VAR>inst✝² : SMul 𝕜 α<VAR>inst✝¹ : OrderedAddCommMonoid β<VAR>inst✝ : SMul 𝕜 β<VAR>f : α ≃o β<VAR>hf : StrictConvexOn 𝕜 univ ⇑f<VAR>x : β<VAR>x✝¹ : x ∈ univ<VAR>y : β<VAR>x✝ : y ∈ univ<VAR>hxy : x ≠ y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>a • f.symm x + b • f.symm y < f.symm (a • x + b • y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : OrderedAddCommMonoid α<VAR>inst✝² : SMul 𝕜 α<VAR>inst✝¹ : OrderedAddCommMonoid β<VAR>inst✝ : SMul 𝕜 β<VAR>f : α ≃o β<VAR>hf : StrictConvexOn 𝕜 univ ⇑f<VAR>x : β<VAR>x✝¹ : x ∈ univ<VAR>y : β<VAR>x✝ : y ∈ univ<VAR>hxy : x ≠ y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>x' : α<VAR>hx'' : x = f x'<GOAL>a • f.symm x + b • f.symm y < f.symm (a • x + b • y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : OrderedAddCommMonoid α<VAR>inst✝² : SMul 𝕜 α<VAR>inst✝¹ : OrderedAddCommMonoid β<VAR>inst✝ : SMul 𝕜 β<VAR>f : α ≃o β<VAR>hf : StrictConvexOn 𝕜 univ ⇑f<VAR>x : β<VAR>x✝¹ : x ∈ univ<VAR>y : β<VAR>x✝ : y ∈ univ<VAR>hxy : x ≠ y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>x' : α<VAR>hx'' : x = f x'<VAR>y' : α<VAR>hy'' : y = f y'<GOAL>a • f.symm x + b • f.symm y < f.symm (a • x + b • y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : OrderedAddCommMonoid α<VAR>inst✝² : SMul 𝕜 α<VAR>inst✝¹ : OrderedAddCommMonoid β<VAR>inst✝ : SMul 𝕜 β<VAR>f : α ≃o β<VAR>hf : StrictConvexOn 𝕜 univ ⇑f<VAR>x : β<VAR>x✝¹ : x ∈ univ<VAR>y : β<VAR>x✝ : y ∈ univ<VAR>hxy : x ≠ y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>x' : α<VAR>hx'' : x = f x'<VAR>y' : α<VAR>hy'' : y = f y'<VAR>hxy' : x' ≠ y'<GOAL>a • f.symm x + b • f.symm y < f.symm (a • x + b • y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : OrderedAddCommMonoid α<VAR>inst✝² : SMul 𝕜 α<VAR>inst✝¹ : OrderedAddCommMonoid β<VAR>inst✝ : SMul 𝕜 β<VAR>f : α ≃o β<VAR>hf : StrictConvexOn 𝕜 univ ⇑f<VAR>x : β<VAR>x✝¹ : x ∈ univ<VAR>y : β<VAR>x✝ : y ∈ univ<VAR>hxy : x ≠ y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>x' : α<VAR>hx'' : x = f x'<VAR>y' : α<VAR>hy'' : y = f y'<VAR>hxy' : x' ≠ y'<GOAL>a • x' + b • y' < f.symm (a • f x' + b • f y')
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : OrderedAddCommMonoid α<VAR>inst✝² : SMul 𝕜 α<VAR>inst✝¹ : OrderedAddCommMonoid β<VAR>inst✝ : SMul 𝕜 β<VAR>f : α ≃o β<VAR>hf : StrictConvexOn 𝕜 univ ⇑f<VAR>x : β<VAR>x✝¹ : x ∈ univ<VAR>y : β<VAR>x✝ : y ∈ univ<VAR>hxy : x ≠ y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>x' : α<VAR>hx'' : x = f x'<VAR>y' : α<VAR>hy'' : y = f y'<VAR>hxy' : x' ≠ y'<GOAL>f (a • x' + b • y') < a • f x' + b • f y'
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁴ : Ring K<VAR>inst✝³ : StrongRankCondition K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module.Free K V<GOAL>Module.rank K V = 1 ↔ ∃ v₀, v₀ ≠ 0 ∧ ∀ (v : V), ∃ r, r • v₀ = v