ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f✝ f : R →+* S<VAR>p : R[X]<VAR>x : S<VAR>h : p ≠ 0<GOAL>p = 0 → 0 = 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ inst✝² : Group α<VAR>inst✝¹ : MulAction α β<VAR>x : β<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H : Subgroup G<VAR>x✝ : G<GOAL>x✝ ∈ stabilizer G ↑1 ↔ x✝ ∈ H
<VAR>n m : ℕ<VAR>p i : Fin n<GOAL>p.predAbove (p.castSucc.succAbove i) = i
<VAR>n m : ℕ<VAR>p i : Fin n<VAR>h : p ≤ i<GOAL>p.predAbove (p.castSucc.succAbove i) = i
<VAR>n m : ℕ<VAR>p i : Fin n<VAR>h : i < p<GOAL>p.predAbove (p.castSucc.succAbove i) = i
<VAR>α : Type ?u.1065<VAR>β : Type ?u.1066<VAR>f : Option α ↪ β<GOAL>∀ (x : Option α), ((fun f => f.fst.optionElim ↑f.snd ⋯) ((fun f => ⟨coeWithTop.trans f, ⟨f none, ⋯⟩⟩) f)) x = f x
<VAR>α : Type ?u.1065<VAR>β : Type ?u.1066<VAR>f : Option α ↪ β<VAR>val✝ : α<GOAL>f ↑val✝ = f (some val✝)
<VAR>α : Type ?u.1065<VAR>β : Type ?u.1066<VAR>x✝ : (f : α ↪ β) × ↑(range ⇑f)ᶜ<VAR>f : α ↪ β<VAR>y : β<VAR>hy : y ∈ (range ⇑f)ᶜ<GOAL>(fun f => ⟨coeWithTop.trans f, ⟨f none, ⋯⟩⟩) ((fun f => f.fst.optionElim ↑f.snd ⋯) ⟨f, ⟨y, hy⟩⟩) = ⟨f, ⟨y, hy⟩⟩
<VAR>α : Type ?u.1065<VAR>β : Type ?u.1066<VAR>x✝¹ : (f : α ↪ β) × ↑(range ⇑f)ᶜ<VAR>f : α ↪ β<VAR>y : β<VAR>hy : y ∈ (range ⇑f)ᶜ<VAR>x✝ : α<GOAL>(f.optionElim y ⋯) ↑x✝ = f x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u v : Finset α<VAR>a✝ b a : α<VAR>s : Finset α<VAR>hs : s ∈ {s | a ∈ s}<VAR>t : Finset α<VAR>ht : t ∈ {s | a ∈ s}<VAR>h : s.erase a = (fun s => s.erase a) t<GOAL>s = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<VAR>f'' : γ ≃ δ<GOAL>(e.trans e').transEquiv f'' = e.trans (e'.transEquiv f'')
<VAR>p a b : ℕ<VAR>hpb : p ∈ b.primeFactorsList<VAR>ha : a ≠ 0<GOAL>p ∈ (a * b).primeFactorsList
<VAR>p a b : ℕ<VAR>hpb : p ∈ b.primeFactorsList<VAR>ha : a ≠ 0<GOAL>p ∈ (b * a).primeFactorsList
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁵ : AddCommGroup F'<VAR>inst✝⁴ : Module 𝕜 F'<VAR>inst✝³ : TopologicalSpace F'<VAR>inst✝² : TopologicalAddGroup F'<VAR>inst✝¹ : ContinuousSMul 𝕜 F'<VAR>inst✝ : CompleteSpace 𝕜<VAR>r : ℝ<VAR>rpos : 0 < r<VAR>c : E<VAR>h : IsCompact (closedBall c r)<GOAL>IsCompact (closedBall 0 r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x✝ : α<VAR>inst✝¹ : AddCommGroup α<VAR>inst✝ : InvolutiveNeg β<VAR>h : Antiperiodic f c<VAR>a x : α<GOAL>(fun x => f (a - x)) (x + c) = -(fun x => f (a - x)) x
<VAR>α : Type u<VAR>m n o : ℕ<VAR>m' : Type u_1<VAR>n' : Type u_2<VAR>o' : Type u_3<VAR>x : α<VAR>u : Fin n → α<VAR>i : Fin (n + 1)<GOAL>vecCons x u (i + i + 1) = vecAlt1 ⋯ (vecAppend ⋯ (vecCons x u) (vecCons x u)) i
<VAR>α : Type u<VAR>m n o : ℕ<VAR>m' : Type u_1<VAR>n' : Type u_2<VAR>o' : Type u_3<VAR>x : α<VAR>u : Fin n → α<VAR>i : Fin (n + 1)<GOAL>vecCons x u (i + i + 1) = (vecCons x u ∘ fun n_1 => n_1 + n_1 + 1) i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>s : Set α<GOAL>ContinuousOn f s ↔ ∀ x ∈ s, ∀ (t : Set β), IsOpen t → f x ∈ t → ∃ u, IsOpen u ∧ x ∈ u ∧ u ∩ s ⊆ f ⁻¹' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : CommGroup G<VAR>a b c d : G<GOAL>a / b = c ↔ a = b * c
<VAR>M : Type u_1<VAR>inst✝⁵ : CommMonoid M<VAR>inst✝⁴ : TopologicalSpace M<VAR>m✝ m' : M<VAR>G : Type u_2<VAR>inst✝³ : CommGroup G<VAR>g g' : G<VAR>inst✝² : T2Space M<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : Encodable β<VAR>inst✝ : CompleteLattice α<VAR>m : α → M<VAR>m0 : m ⊥ = 1<VAR>s : β → α<GOAL>∏' (i : ℕ), m (⨆ b ∈ decode₂ β i, s b) = ∏' (b : β), m (s b)
<VAR>M : Type u_1<VAR>inst✝⁵ : CommMonoid M<VAR>inst✝⁴ : TopologicalSpace M<VAR>m✝ m' : M<VAR>G : Type u_2<VAR>inst✝³ : CommGroup G<VAR>g g' : G<VAR>inst✝² : T2Space M<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : Encodable β<VAR>inst✝ : CompleteLattice α<VAR>m : α → M<VAR>m0 : m ⊥ = 1<VAR>s : β → α<GOAL>∏' (i : ℕ), m (⨆ b ∈ decode₂ β i, s b) = ∏' (y : ℕ), extend encode (fun b => m (s b)) 1 y
<VAR>M : Type u_1<VAR>inst✝⁵ : CommMonoid M<VAR>inst✝⁴ : TopologicalSpace M<VAR>m✝ m' : M<VAR>G : Type u_2<VAR>inst✝³ : CommGroup G<VAR>g g' : G<VAR>inst✝² : T2Space M<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : Encodable β<VAR>inst✝ : CompleteLattice α<VAR>m : α → M<VAR>m0 : m ⊥ = 1<VAR>s : β → α<VAR>n : ℕ<GOAL>m (⨆ b ∈ decode₂ β n, s b) = extend encode (fun b => m (s b)) 1 n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>b : β<VAR>t : Set γ<VAR>f : β × γ → α<GOAL>∏' (x : ↑({b} ×ˢ t)), f ↑x = ∏' (c : ↑t), f (b, ↑c)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>x : E<VAR>p : ℝ<VAR>hp : 1 < p<GOAL>‖fderiv ℝ (fun x => ‖x‖ ^ p) x‖ = p * ‖x‖ ^ (p - 1)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>x : E<VAR>p : ℝ<VAR>hp : 1 < p<GOAL>‖p‖ * ‖‖x‖ ^ (p - 2)‖ * ‖(innerSL ℝ) x‖ = p * ‖x‖ ^ (p - 1)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>x : E<VAR>p : ℝ<VAR>hp : 1 < p<GOAL>p * (‖x‖ ^ (p - 2) * ‖x‖) = p * ‖x‖ ^ (p - 1)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>x : E<VAR>p : ℝ<VAR>hp : 1 < p<GOAL>p * ‖x‖ ^ (p - 2 + 1) = p * ‖x‖ ^ (p - 1)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : BooleanAlgebra α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α<VAR>a b c : α<VAR>s t : Finset α<VAR>a✝ : α<GOAL>a✝ ∈ s ⊼ tᶜˢ ↔ a✝ ∈ s \\ t
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : BooleanAlgebra α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α<VAR>a b c : α<VAR>s t : Finset α<VAR>a✝ : α<GOAL>(∃ a ∈ s, ∃ b, bᶜ ∈ t ∧ a ⊓ b = a✝) ↔ ∃ a ∈ s, ∃ b ∈ t, a ⊓ bᶜ = a✝
<VAR>m e : Nat<GOAL>Rat.ofScientific m false e = if false = true then mkRat (↑m) (10 ^ e) else ↑(m * 10 ^ e)
<VAR>m e : Nat<GOAL>Rat.ofScientific m true e = if true = true then mkRat (↑m) (10 ^ e) else ↑(m * 10 ^ e)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>h : X ≃ₜ Y<VAR>f : Y → Z<GOAL>IsOpenMap (f ∘ ⇑h) ↔ IsOpenMap f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>h : X ≃ₜ Y<VAR>f : Y → Z<GOAL>IsOpenMap (f ∘ ⇑h) → IsOpenMap f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>h : X ≃ₜ Y<VAR>f : Y → Z<VAR>hf : IsOpenMap (f ∘ ⇑h)<GOAL>IsOpenMap f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>h : X ≃ₜ Y<VAR>f : Y → Z<VAR>hf : IsOpenMap (f ∘ ⇑h)<GOAL>IsOpenMap ((f ∘ ⇑h) ∘ ⇑h.symm)
<VAR>R : Type uR<VAR>inst✝³ : Semiring R<VAR>S : Type uS<VAR>inst✝² : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra S A<VAR>r : R → R → Prop<VAR>a b c : R<VAR>h : Rel r b c<GOAL>Rel r (a + b) (a + c)
<VAR>R : Type uR<VAR>inst✝³ : Semiring R<VAR>S : Type uS<VAR>inst✝² : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra S A<VAR>r : R → R → Prop<VAR>a b c : R<VAR>h : Rel r b c<GOAL>Rel r (b + a) (c + a)
<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>‖x‖ / (o.oangle (x - y) x).cos = ‖x - y‖
<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>‖x‖ / ((-o).oangle x (x - y)).cos = ‖x - y‖
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>n : ℕ<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NeZero ↑n<GOAL>(cyclotomic n R).roots.Nodup
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>n : ℕ<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NeZero ↑n<VAR>h : (cyclotomic n R).roots = 0<GOAL>(cyclotomic n R).roots.Nodup
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>n : ℕ<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NeZero ↑n<VAR>ζ : R<VAR>hζ : ζ ∈ (cyclotomic n R).roots<GOAL>(cyclotomic n R).roots.Nodup
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>n : ℕ<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NeZero ↑n<VAR>ζ : R<VAR>hζ : IsPrimitiveRoot ζ n<GOAL>(cyclotomic n R).roots.Nodup
<VAR>R : Type u_1<VAR>A✝ : Type u_2<VAR>B : Type u_3<VAR>A : Type u_4<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>fe : { fe // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 (fe.1 a) }<VAR>a : A<VAR>ad : A[ε]<GOAL>(lift fe) (a • ad) = (↑fe).1 a * (lift fe) ad
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>x y : α<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Finite β<VAR>f : Perm β<VAR>hf : f.IsCycle<VAR>hf' : Nat.Prime (orderOf f)<VAR>n : ℕ<VAR>hn : 0 < n<VAR>hn' : n < orderOf f<GOAL>(f ^ n).IsCycle
<VAR>μ : YoungDiagram<VAR>i j : ℕ<GOAL>(i, j) ∈ μ ↔ i < μ.colLen j
<VAR>μ : YoungDiagram<VAR>i j : ℕ<GOAL>(i, j) ∈ μ ↔ (j, i) ∈ μ.transpose
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : Monoid M<VAR>u : Mˣ<VAR>x✝ : IsUnit ↑u<GOAL>∃ b, ↑u * b = 1 ∧ b * ↑u = 1
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>ι : Type u_1<VAR>inst✝ : Unique ι<VAR>h : finrank K V = 1<VAR>v : V<VAR>hv : v ≠ 0<VAR>i : ι<GOAL>(basisSingleton ι h v hv) i = v
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>ι : Type u_1<VAR>inst✝ : Unique ι<VAR>h : finrank K V = 1<VAR>v : V<VAR>hv : v ≠ 0<GOAL>(basisSingleton ι h v hv) default = v
<VAR>k : Type u<VAR>inst✝¹ : Field k<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>V W : FDRep k G<VAR>g : G<GOAL>(V ⊗ W).character g = (V.character * W.character) g
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>C : Type u_3<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : NonUnitalSemiring A<VAR>inst✝⁸ : StarRing A<VAR>inst✝⁷ : Module R A<VAR>inst✝⁶ : SMulCommClass R A A<VAR>inst✝⁵ : IsScalarTower R A A<VAR>inst✝⁴ : StarModule R A<VAR>inst✝³ : Semiring C<VAR>inst✝² : Algebra R C<VAR>inst✝¹ : StarRing C<VAR>inst✝ : StarModule R C<VAR>φ : A →⋆ₙₐ[R] C<VAR>r✝ : R<VAR>a✝ : A<GOAL>(↑↑(lift φ.toNonUnitalAlgHom).toRingHom).toFun (star (inl r✝ + ↑a✝)) = star ((↑↑(lift φ.toNonUnitalAlgHom).toRingHom).toFun (inl r✝ + ↑a✝))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : NonUnitalSemiring A<VAR>inst✝² : Module R A<VAR>inst✝¹ : IsScalarTower R A A<VAR>inst✝ : SMulCommClass R A A<VAR>s : Set A<VAR>r : R<VAR>a : A<VAR>ha : a ∈ s.centralizer<VAR>x : A<VAR>hx : x ∈ s<GOAL>x * r • a = r • a * x
<VAR>G : Type u_1<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : BorelSpace G<VAR>μ : Measure G<VAR>Γ : Subgroup G<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ<VAR>inst✝³ : Countable ↥Γ<VAR>inst✝² : MeasurableSpace (G ⧸ Γ)<VAR>inst✝¹ : BorelSpace (G ⧸ Γ)<VAR>inst✝ : μ.IsMulRightInvariant<VAR>g : G ⧸ Γ → ℝ≥0∞<VAR>g_ae_measurable : AEMeasurable g (map QuotientGroup.mk (μ.restrict 𝓕))<GOAL>essSup g (map QuotientGroup.mk (μ.restrict 𝓕)) = essSup (fun x => g ↑x) μ
<VAR>G : Type u_1<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : BorelSpace G<VAR>μ : Measure G<VAR>Γ : Subgroup G<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ<VAR>inst✝³ : Countable ↥Γ<VAR>inst✝² : MeasurableSpace (G ⧸ Γ)<VAR>inst✝¹ : BorelSpace (G ⧸ Γ)<VAR>inst✝ : μ.IsMulRightInvariant<VAR>g : G ⧸ Γ → ℝ≥0∞<VAR>g_ae_measurable : AEMeasurable g (map QuotientGroup.mk (μ.restrict 𝓕))<VAR>hπ : Measurable QuotientGroup.mk<GOAL>essSup g (map QuotientGroup.mk (μ.restrict 𝓕)) = essSup (fun x => g ↑x) μ
<VAR>G : Type u_1<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : BorelSpace G<VAR>μ : Measure G<VAR>Γ : Subgroup G<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ<VAR>inst✝³ : Countable ↥Γ<VAR>inst✝² : MeasurableSpace (G ⧸ Γ)<VAR>inst✝¹ : BorelSpace (G ⧸ Γ)<VAR>inst✝ : μ.IsMulRightInvariant<VAR>g : G ⧸ Γ → ℝ≥0∞<VAR>g_ae_measurable : AEMeasurable g (map QuotientGroup.mk (μ.restrict 𝓕))<VAR>hπ : Measurable QuotientGroup.mk<GOAL>essSup (g ∘ QuotientGroup.mk) (μ.restrict 𝓕) = essSup (fun x => g ↑x) μ
<VAR>G : Type u_1<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : BorelSpace G<VAR>μ : Measure G<VAR>Γ : Subgroup G<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ<VAR>inst✝³ : Countable ↥Γ<VAR>inst✝² : MeasurableSpace (G ⧸ Γ)<VAR>inst✝¹ : BorelSpace (G ⧸ Γ)<VAR>inst✝ : μ.IsMulRightInvariant<VAR>g : G ⧸ Γ → ℝ≥0∞<VAR>g_ae_measurable : AEMeasurable g (map QuotientGroup.mk (μ.restrict 𝓕))<VAR>hπ : Measurable QuotientGroup.mk<GOAL>∀ (γ : ↥Γ.op) (x : G), (g ∘ QuotientGroup.mk) (γ • x) = (g ∘ QuotientGroup.mk) x
<VAR>G : Type u_1<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : BorelSpace G<VAR>μ : Measure G<VAR>Γ : Subgroup G<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ<VAR>inst✝³ : Countable ↥Γ<VAR>inst✝² : MeasurableSpace (G ⧸ Γ)<VAR>inst✝¹ : BorelSpace (G ⧸ Γ)<VAR>inst✝ : μ.IsMulRightInvariant<VAR>g : G ⧸ Γ → ℝ≥0∞<VAR>g_ae_measurable : AEMeasurable g (map QuotientGroup.mk (μ.restrict 𝓕))<VAR>hπ : Measurable QuotientGroup.mk<VAR>γ : Gᵐᵒᵖ<VAR>hγ : γ ∈ Γ.op<VAR>x : G<GOAL>↑(x * MulOpposite.unop γ) = ↑x
<VAR>i j : ℕ<GOAL>(i + j).choose j = (i + j)! / (i ! * j !)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>p s : Submodule R A<VAR>h1 : 1 ∈ s<VAR>hmul : ∀ (x y : A), x ∈ s → y ∈ s → x * y ∈ s<VAR>r : R<GOAL>(algebraMap R A) r ∈ { carrier := ↑s, mul_mem' := hmul, one_mem' := h1, add_mem' := ⋯, zero_mem' := ⋯ }.carrier
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>p s : Submodule R A<VAR>h1 : 1 ∈ s<VAR>hmul : ∀ (x y : A), x ∈ s → y ∈ s → x * y ∈ s<VAR>r : R<GOAL>r • 1 ∈ { carrier := ↑s, mul_mem' := hmul, one_mem' := h1, add_mem' := ⋯, zero_mem' := ⋯ }.carrier
<VAR>ι : Type u<VAR>s : Finset ι<VAR>z₁ z₂ : ℝ≥0<VAR>p : ℝ<VAR>hp : 1 ≤ p<GOAL>(z₁ + z₂) ^ p ≤ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>z₁ z₂ : ℝ≥0<VAR>hp : 1 ≤ 1<GOAL>(z₁ + z₂) ^ 1 ≤ 2 ^ (1 - 1) * (z₁ ^ 1 + z₂ ^ 1)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>z₁ z₂ : ℝ≥0<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h'p : 1 < p<GOAL>(z₁ + z₂) ^ p ≤ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>z₁ z₂ : ℝ≥0<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h'p : 1 < p<GOAL>(z₁ + z₂) ^ p = (1 / 2 * (2 * z₁) + 1 / 2 * (2 * z₂)) ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>z₁ z₂ : ℝ≥0<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h'p : 1 < p<GOAL>2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p) = 1 / 2 * (2 * z₁) ^ p + 1 / 2 * (2 * z₂) ^ p
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : SemilatticeSup α<GOAL>atTop = generate (range Ici)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : SemilatticeSup α<VAR>hα : IsEmpty α<GOAL>atTop = generate (range Ici)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : SemilatticeSup α<VAR>hα : Nonempty α<GOAL>atTop = generate (range Ici)
<VAR>Ω : Type u_1<VAR>inst✝ : Nonempty Ω<VAR>m0✝ : MeasurableSpace Ω<VAR>μ✝ : FiniteMeasure Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : ProbabilityMeasure Ω<GOAL>μ.toFiniteMeasure.normalize = μ
<VAR>Ω : Type u_1<VAR>inst✝ : Nonempty Ω<VAR>m0✝ : MeasurableSpace Ω<VAR>μ✝ : FiniteMeasure Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : ProbabilityMeasure Ω<GOAL>∀ (s : Set Ω), MeasurableSet s → μ.toFiniteMeasure.normalize s = μ s
<VAR>Ω : Type u_1<VAR>inst✝ : Nonempty Ω<VAR>m0✝ : MeasurableSpace Ω<VAR>μ✝ : FiniteMeasure Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : ProbabilityMeasure Ω<VAR>s : Set Ω<VAR>_s_mble : MeasurableSet s<GOAL>μ.toFiniteMeasure.normalize s = μ s
<VAR>Ω : Type u_1<VAR>inst✝ : Nonempty Ω<VAR>m0✝ : MeasurableSpace Ω<VAR>μ✝ : FiniteMeasure Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : ProbabilityMeasure Ω<VAR>s : Set Ω<VAR>_s_mble : MeasurableSet s<GOAL>μ.toFiniteMeasure.mass⁻¹ * μ.toFiniteMeasure s = μ s
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>u : Rˣ<GOAL>invUnitsSub u * ((C R) ↑u - X) = 1
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g✝ : α → β<VAR>inst✝ : CommMonoid β<VAR>s : Finset α<VAR>p : α → Prop<VAR>hp : DecidablePred p<VAR>f g : α → β<GOAL>(∏ x ∈ s, if p x then f x else g x) = (∏ x ∈ filter p s, f x) * ∏ x ∈ filter (fun x => ¬p x) s, g x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Lattice α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<VAR>h₁ : a₁ ∈ [[a₂, b₂]]<VAR>h₂ : b₁ ∈ [[a₂, b₂]]<GOAL>[[a₁, b₁]] ⊆ [[a₂, b₂]]
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Lattice α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<VAR>h₁ : a₂ ⊓ b₂ ≤ a₁ ∧ a₁ ≤ a₂ ⊔ b₂<VAR>h₂ : a₂ ⊓ b₂ ≤ b₁ ∧ b₁ ≤ a₂ ⊔ b₂<GOAL>[[a₁, b₁]] ⊆ [[a₂, b₂]]
<VAR>a x✝ z x : ℂ<VAR>hx_re : x.re < 0<VAR>hx_im : 0 ≤ x.im<GOAL>x.arg = Real.arcsin ((-x).im / abs x) + π
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹⁰ : LinearOrderedCommRing 𝕜<VAR>inst✝⁹ : LinearOrderedCommRing E<VAR>inst✝⁸ : LinearOrderedAddCommGroup F<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜 F<VAR>inst✝⁵ : Module E F<VAR>inst✝⁴ : IsScalarTower 𝕜 E F<VAR>inst✝³ : SMulCommClass 𝕜 E F<VAR>inst✝² : OrderedSMul 𝕜 E<VAR>inst✝¹ : OrderedSMul 𝕜 F<VAR>inst✝ : OrderedSMul E F<VAR>s : Set 𝕜<VAR>f : 𝕜 → E<VAR>g : 𝕜 → F<VAR>hf : ConcaveOn 𝕜 s f<VAR>hg : ConvexOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → f x ≤ 0<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x<VAR>hfg : AntivaryOn f g s<GOAL>ConcaveOn 𝕜 s (f • g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹⁰ : LinearOrderedCommRing 𝕜<VAR>inst✝⁹ : LinearOrderedCommRing E<VAR>inst✝⁸ : LinearOrderedAddCommGroup F<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜 F<VAR>inst✝⁵ : Module E F<VAR>inst✝⁴ : IsScalarTower 𝕜 E F<VAR>inst✝³ : SMulCommClass 𝕜 E F<VAR>inst✝² : OrderedSMul 𝕜 E<VAR>inst✝¹ : OrderedSMul 𝕜 F<VAR>inst✝ : OrderedSMul E F<VAR>s : Set 𝕜<VAR>f : 𝕜 → E<VAR>g : 𝕜 → F<VAR>hf : ConcaveOn 𝕜 s f<VAR>hg : ConvexOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → f x ≤ 0<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x<VAR>hfg : AntivaryOn f g s<GOAL>ConvexOn 𝕜 s (f • -g)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Algebra F<VAR>α β : A₁ ⟶ A₂<GOAL>F.map (α.f + β.f) ≫ A₂.str = A₁.str ≫ (α.f + β.f)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Algebra F<GOAL>F.map 0 ≫ A₂.str = A₁.str ≫ 0
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Algebra F<VAR>n : ℕ<VAR>α : A₁ ⟶ A₂<GOAL>F.map (n • α.f) ≫ A₂.str = A₁.str ≫ (n • α.f)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Algebra F<VAR>α : A₁ ⟶ A₂<GOAL>F.map (-α.f) ≫ A₂.str = A₁.str ≫ (-α.f)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Algebra F<VAR>α β : A₁ ⟶ A₂<GOAL>F.map (α.f - β.f) ≫ A₂.str = A₁.str ≫ (α.f - β.f)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Algebra F<VAR>r : ℤ<VAR>α : A₁ ⟶ A₂<GOAL>F.map (r • α.f) ≫ A₂.str = A₁.str ≫ (r • α.f)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Algebra F<VAR>a✝ b✝ c✝ : A₁ ⟶ A₂<GOAL>(a✝ + b✝ + c✝).f = (a✝ + (b✝ + c✝)).f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Algebra F<VAR>a✝ : A₁ ⟶ A₂<GOAL>(0 + a✝).f = a✝.f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Algebra F<VAR>a✝ : A₁ ⟶ A₂<GOAL>(a✝ + 0).f = a✝.f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Algebra F<VAR>x✝ : A₁ ⟶ A₂<GOAL>((fun n α => { f := n • α.f, h := ⋯ }) 0 x✝).f = Algebra.Hom.f 0
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Algebra F<VAR>n✝ : ℕ<VAR>x✝ : A₁ ⟶ A₂<GOAL>((fun n α => { f := n • α.f, h := ⋯ }) (n✝ + 1) x✝).f = ((fun n α => { f := n • α.f, h := ⋯ }) n✝ x✝ + x✝).f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Algebra F<VAR>a✝ b✝ : A₁ ⟶ A₂<GOAL>(a✝ - b✝).f = (a✝ + -b✝).f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Algebra F<VAR>a✝ : A₁ ⟶ A₂<GOAL>((fun r α => { f := r • α.f, h := ⋯ }) 0 a✝).f = Algebra.Hom.f 0
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Algebra F<VAR>n✝ : ℕ<VAR>a✝ : A₁ ⟶ A₂<GOAL>↑(n✝ + 1) • a✝.f = ({ f := ↑n✝ • a✝.f, h := ⋯ } + a✝).f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Algebra F<VAR>n✝ : ℕ<VAR>a✝ : A₁ ⟶ A₂<GOAL>n✝ • a✝.f + a✝.f = ({ f := n✝ • a✝.f, h := ⋯ } + a✝).f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Algebra F<VAR>n✝ : ℕ<VAR>a✝ : A₁ ⟶ A₂<GOAL>((fun r α => { f := r • α.f, h := ⋯ }) (Int.negSucc n✝) a✝).f = (-(fun r α => { f := r • α.f, h := ⋯ }) (↑n✝.succ) a✝).f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Algebra F<VAR>a✝ : A₁ ⟶ A₂<GOAL>(-a✝ + a✝).f = Algebra.Hom.f 0
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Algebra F<VAR>a✝ b✝ : A₁ ⟶ A₂<GOAL>(a✝ + b✝).f = (b✝ + a✝).f