ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝⁷ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>𝕜 : Type u_2<VAR>inst✝⁶ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>F✝ : H → α → E<VAR>x₀ : H<VAR>bound✝ : α → ℝ<VAR>ε : ℝ<VAR>inst✝ : NormedSpace ℝ H<VAR>μ : Measure ℝ<VAR>F : H → ℝ → E<VAR>F' : ℝ → H →L[ℝ] E<VAR>a b : ℝ<VAR>bound : ℝ → ℝ<VAR>ε_pos : 0 < ε<VAR>hF_int : IntervalIntegrable (F x₀) μ a b<VAR>h_lip : (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), LipschitzOnWith (Real.nnabs (bound x)) (fun x_1 => F x_1 x) (ball x₀ ε)) ∧ ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), LipschitzOnWith (Real.nnabs (bound x)) (fun x_1 => F x_1 x) (ball x₀ ε)<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_diff : (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), HasFDerivAt (fun x_1 => F x_1 x) (F' x) x₀) ∧ ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), HasFDerivAt (fun x_1 => F x_1 x) (F' x) x₀<VAR>hF'_meas : AEStronglyMeasurable F' (μ.restrict (Set.Ioc a b)) ∧ AEStronglyMeasurable F' (μ.restrict (Set.Ioc b a))<VAR>hF_meas : (∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Set.Ioc a b))) ∧ ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Set.Ioc b a))<VAR>H₁ : Integrable F' (μ.restrict (Set.Ioc a b)) ∧ HasFDerivAt (fun x => ∫ (a : ℝ) in Set.Ioc a b, F x a ∂μ) (∫ (a : ℝ) in Set.Ioc a b, F' a ∂μ) x₀<VAR>H₂ : Integrable F' (μ.restrict (Set.Ioc b a)) ∧ HasFDerivAt (fun x => ∫ (a : ℝ) in Set.Ioc b a, F x a ∂μ) (∫ (a : ℝ) in Set.Ioc b a, F' a ∂μ) x₀<GOAL>IntervalIntegrable F' μ a b ∧ HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>n : ℕ<GOAL>s.tail.drop n = s.drop (n + 1)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>n : ℕ<GOAL>s.tail.drop n = s.drop (1 + n)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>n : ℕ<GOAL>s.drop (1 + n) = s.tail.drop n
<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>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>v : Basis ι 𝕜 E<GOAL>∃ C > 0, ∀ {u : E →L[𝕜] F} (M : ℝ≥0), (∀ (i : ι), ‖u (v i)‖₊ ≤ M) → ‖u‖₊ ≤ C * M
<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>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>v : Basis ι 𝕜 E<VAR>val✝ : Fintype ι<GOAL>∃ C > 0, ∀ {u : E →L[𝕜] F} (M : ℝ≥0), (∀ (i : ι), ‖u (v i)‖₊ ≤ M) → ‖u‖₊ ≤ C * M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>ι : Type u_5<VAR>ι₁ : Type u_6<VAR>ι₂ : Type u_7<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M₁<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Module R M₁<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype ι₁<VAR>inst✝³ : Fintype ι₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : DecidableEq ι₁<VAR>inst✝ : DecidableEq ι₂<VAR>b : Basis ι R M<VAR>b₁ : Basis ι₁ R M₁<VAR>b₂ : Basis ι₂ R M₂<VAR>k : ι₁<VAR>this : DecidableEq ι₂<VAR>i : ι₂<VAR>j : ι₁<GOAL>((b₁.linearMap b₂) (i, j)) (b₁ k) = if (i, j).2 = k then b₂ (i, j).1 else 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>ι : Type u_5<VAR>ι₁ : Type u_6<VAR>ι₂ : Type u_7<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M₁<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Module R M₁<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype ι₁<VAR>inst✝³ : Fintype ι₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : DecidableEq ι₁<VAR>inst✝ : DecidableEq ι₂<VAR>b : Basis ι R M<VAR>b₁ : Basis ι₁ R M₁<VAR>b₂ : Basis ι₂ R M₂<VAR>k : ι₁<VAR>this : DecidableEq ι₂<VAR>i : ι₂<VAR>j : ι₁<GOAL>∑ j_1 : ι₂, stdBasisMatrix i j 1 j_1 k • b₂ j_1 = if (i, j).2 = k then b₂ (i, j).1 else 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>ι : Type u_5<VAR>ι₁ : Type u_6<VAR>ι₂ : Type u_7<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M₁<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Module R M₁<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype ι₁<VAR>inst✝³ : Fintype ι₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : DecidableEq ι₁<VAR>inst✝ : DecidableEq ι₂<VAR>b : Basis ι R M<VAR>b₁ : Basis ι₁ R M₁<VAR>b₂ : Basis ι₂ R M₂<VAR>k : ι₁<VAR>this : DecidableEq ι₂<VAR>i : ι₂<VAR>j : ι₁<GOAL>∑ j_1 : ι₂, (if i = j_1 ∧ j = k then 1 else 0) • b₂ j_1 = if j = k then b₂ i else 0
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝ : AddGroup G<VAR>T : AddTorsor G P<VAR>p₁ p₂ p₃ : P<GOAL>p₁ -ᵥ p₂ + (p₂ -ᵥ p₃) = p₁ -ᵥ p₃
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝ : AddGroup G<VAR>T : AddTorsor G P<VAR>p₁ p₂ p₃ : P<GOAL>p₁ -ᵥ p₂ + (p₂ -ᵥ p₃) +ᵥ p₃ = p₁ -ᵥ p₃ +ᵥ p₃
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a b ad bd a' b' gcd : α<VAR>ha : ad * a = a'<VAR>hb : bd * b = b'<VAR>had : 0 < ad<VAR>hbd : 0 < bd<VAR>hgcd : 0 < gcd<GOAL>(a ≤ b) = (1 / gcd * (bd * a') ≤ 1 / gcd * (ad * b'))
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a b ad bd a' b' gcd : α<VAR>ha : ad * a = a'<VAR>hb : bd * b = b'<VAR>had : 0 < ad<VAR>hbd : 0 < bd<VAR>hgcd : 0 < gcd<GOAL>0 < ad * bd
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a b ad bd a' b' gcd : α<VAR>ha : ad * a = a'<VAR>hb : bd * b = b'<VAR>had : 0 < ad<VAR>hbd : 0 < bd<VAR>hgcd : 0 < gcd<GOAL>0 < 1 / gcd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableRel G.Adj<VAR>hG : G.EdgeDisjointTriangles<GOAL>3 * (G.cliqueFinset 3).card ≤ G.edgeFinset.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableRel G.Adj<VAR>hG : G.EdgeDisjointTriangles<GOAL>(G.cliqueFinset 3).card * 3 ≤ G.edgeFinset.card * 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableRel G.Adj<VAR>hG : G.EdgeDisjointTriangles<GOAL>∀ a ∈ G.cliqueFinset 3, 3 ≤ (bipartiteAbove (fun s e => e ∈ s.sym2) G.edgeFinset a).card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableRel G.Adj<VAR>hG : G.EdgeDisjointTriangles<VAR>e : Sym2 α<VAR>he : e ∈ G.edgeFinset<GOAL>(bipartiteBelow (fun s e => e ∈ s.sym2) (G.cliqueFinset 3) e).card ≤ 1
<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>inst✝⁹ : PolishSpace G<VAR>Γ : Subgroup G<VAR>inst✝⁸ : Countable ↥Γ<VAR>inst✝⁷ : Γ.Normal<VAR>inst✝⁶ : T2Space (G ⧸ Γ)<VAR>inst✝⁵ : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝⁴ : SigmaFinite ν<VAR>inst✝³ : ν.IsHaarMeasure<VAR>inst✝² : ν.IsMulRightInvariant<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : SigmaFinite μ<VAR>V : Set (G ⧸ Γ)<VAR>hV : (interior V).Nonempty<VAR>meas_V : MeasurableSet V<VAR>hμK : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ 𝓕)<VAR>neTopV : μ V ≠ ⊤<GOAL>QuotientMeasureEqMeasurePreimage ν μ
<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>inst✝⁹ : PolishSpace G<VAR>Γ : Subgroup G<VAR>inst✝⁸ : Countable ↥Γ<VAR>inst✝⁷ : Γ.Normal<VAR>inst✝⁶ : T2Space (G ⧸ Γ)<VAR>inst✝⁵ : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝⁴ : SigmaFinite ν<VAR>inst✝³ : ν.IsHaarMeasure<VAR>inst✝² : ν.IsMulRightInvariant<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : SigmaFinite μ<VAR>V : Set (G ⧸ Γ)<VAR>hV : (interior V).Nonempty<VAR>meas_V : MeasurableSet V<VAR>hμK : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ 𝓕)<VAR>neTopV : μ V ≠ ⊤<GOAL>μ V ≠ 0
<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>inst✝⁹ : PolishSpace G<VAR>Γ : Subgroup G<VAR>inst✝⁸ : Countable ↥Γ<VAR>inst✝⁷ : Γ.Normal<VAR>inst✝⁶ : T2Space (G ⧸ Γ)<VAR>inst✝⁵ : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝⁴ : SigmaFinite ν<VAR>inst✝³ : ν.IsHaarMeasure<VAR>inst✝² : ν.IsMulRightInvariant<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : SigmaFinite μ<VAR>V : Set (G ⧸ Γ)<VAR>hV : (interior V).Nonempty<VAR>meas_V : MeasurableSet V<VAR>hμK : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ 𝓕)<VAR>neTopV : μ V ≠ ⊤<GOAL>μ V = ν (QuotientGroup.mk ⁻¹' V ∩ 𝓕)
<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>inst✝⁹ : PolishSpace G<VAR>Γ : Subgroup G<VAR>inst✝⁸ : Countable ↥Γ<VAR>inst✝⁷ : Γ.Normal<VAR>inst✝⁶ : T2Space (G ⧸ Γ)<VAR>inst✝⁵ : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝⁴ : SigmaFinite ν<VAR>inst✝³ : ν.IsHaarMeasure<VAR>inst✝² : ν.IsMulRightInvariant<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : SigmaFinite μ<VAR>V : Set (G ⧸ Γ)<VAR>hV : (interior V).Nonempty<VAR>meas_V : MeasurableSet V<VAR>hμK : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ 𝓕)<VAR>neTopV : μ V ≠ ⊤<GOAL>μ V ≠ ⊤
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>f g : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>hg : g.IsMultiplicative<VAR>n : ℕ<VAR>hn : Squarefree n<GOAL>(ArithmeticFunction.prodPrimeFactors fun p => (f + g) p) n = (f * g) n
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>f g : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>hg : g.IsMultiplicative<VAR>n : ℕ<VAR>hn : Squarefree n<GOAL>∏ p ∈ n.primeFactors, (f + g) p = (f * g) n
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>f g : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>hg : g.IsMultiplicative<VAR>n : ℕ<VAR>hn : Squarefree n<GOAL>∏ x ∈ n.primeFactors, (f x + g x) = (f * g) n
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>f g : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>hg : g.IsMultiplicative<VAR>n : ℕ<VAR>hn : Squarefree n<GOAL>∑ t ∈ n.primeFactors.powerset, (∏ i ∈ t, f i) * ∏ i ∈ n.primeFactors \ t, g i = ∑ i ∈ (↑n.primeFactorsList).toFinset.powerset, f i.val.prod * g (n / i.val.prod)
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>f g : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>hg : g.IsMultiplicative<VAR>n : ℕ<VAR>hn : Squarefree n<GOAL>∀ x ∈ n.primeFactors.powerset, (∏ i ∈ x, f i) * ∏ i ∈ n.primeFactors \ x, g i = f x.val.prod * g (n / x.val.prod)
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>f g : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>hg : g.IsMultiplicative<VAR>n : ℕ<VAR>hn : Squarefree n<VAR>t : Finset ℕ<VAR>ht : t ∈ n.primeFactors.powerset<GOAL>(∏ i ∈ t, f i) * ∏ i ∈ n.primeFactors \ t, g i = f t.val.prod * g (n / t.val.prod)
<VAR>m n a b c d : ℕ<VAR>h : a ≡ b [MOD m]<GOAL>a.gcd m = b.gcd m
<VAR>m n a b c d : ℕ<VAR>h : a ≡ b [MOD m]<VAR>h1 : a.gcd m ∣ m<GOAL>a.gcd m = b.gcd m
<VAR>m n a b c d : ℕ<VAR>h : a ≡ b [MOD m]<VAR>h1 : a.gcd m ∣ m<VAR>h2 : b.gcd m ∣ m<GOAL>a.gcd m = b.gcd m
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x : E<GOAL>o.rightAngleRotation (o.rightAngleRotation x) = -x
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x : E<GOAL>(LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯) ((LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯) x) = -x
<VAR>ι : Type u_1<VAR>inst✝³ : LinearOrder ι<VAR>inst✝² : SuccOrder ι<VAR>inst✝¹ : IsSuccArchimedean ι<VAR>inst✝ : PredOrder ι<VAR>i0 i : ι<GOAL>toZ i0 i0 = 0
<VAR>ι : Type u_1<VAR>inst✝³ : LinearOrder ι<VAR>inst✝² : SuccOrder ι<VAR>inst✝¹ : IsSuccArchimedean ι<VAR>inst✝ : PredOrder ι<VAR>i0 i : ι<GOAL>↑(Nat.find ⋯) = 0
<VAR>ι : Type u_1<VAR>inst✝³ : LinearOrder ι<VAR>inst✝² : SuccOrder ι<VAR>inst✝¹ : IsSuccArchimedean ι<VAR>inst✝ : PredOrder ι<VAR>i0 i : ι<GOAL>Nat.find ⋯ = 0
<VAR>ι : Type u_1<VAR>inst✝³ : LinearOrder ι<VAR>inst✝² : SuccOrder ι<VAR>inst✝¹ : IsSuccArchimedean ι<VAR>inst✝ : PredOrder ι<VAR>i0 i : ι<GOAL>succ^[0] i0 = i0
<VAR>α : Type u<VAR>β : Type v<VAR>G : Type u<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<GOAL>∃ G' x x_1, Nonempty (G ≃* G')
<VAR>α : Type u<VAR>β : Type v<VAR>G : Type u<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>n : ℕ<VAR>e : G ≃ Fin n<GOAL>∃ G' x x_1, Nonempty (G ≃* G')
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>a b : α<VAR>h : a ≤ b<GOAL>0 ≤ variationOnFromTo f s a b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>s t u v : Set α<VAR>h : Disjoint s t<GOAL>AEDisjoint μ s t
<VAR>q : ℍ<VAR>hq : q.re = 0<VAR>n : ℕ<GOAL>((expSeries ℝ ℍ (2 * n)) fun x => q) = ↑((-1) ^ n * ‖q‖ ^ (2 * n) / ↑(2 * n)!)
<VAR>q : ℍ<VAR>hq : q.re = 0<VAR>n : ℕ<GOAL>(↑(2 * n)!)⁻¹ • q ^ (2 * n) = ↑((-1) ^ n * ‖q‖ ^ (2 * n) / ↑(2 * n)!)
<VAR>q : ℍ<VAR>hq : q.re = 0<VAR>n : ℕ<VAR>hq2 : q ^ 2 = -↑(normSq q)<GOAL>(↑(2 * n)!)⁻¹ • q ^ (2 * n) = ↑((-1) ^ n * ‖q‖ ^ (2 * n) / ↑(2 * n)!)
<VAR>q : ℍ<VAR>hq : q.re = 0<VAR>n : ℕ<VAR>hq2 : q ^ 2 = -↑(normSq q)<VAR>k : ℝ := ↑(2 * n)!<GOAL>(↑(2 * n)!)⁻¹ • q ^ (2 * n) = ↑((-1) ^ n * ‖q‖ ^ (2 * n) / ↑(2 * n)!)
<VAR>q : ℍ<VAR>hq : q.re = 0<VAR>n : ℕ<VAR>hq2 : q ^ 2 = -↑(normSq q)<VAR>k : ℝ := ↑(2 * n)!<GOAL>k⁻¹ • (-↑(normSq q)) ^ n = k⁻¹ • ↑((-1) ^ n * ‖q‖ ^ (2 * n))
<VAR>q : ℍ<VAR>hq : q.re = 0<VAR>n : ℕ<VAR>hq2 : q ^ 2 = -↑(normSq q)<VAR>k : ℝ := ↑(2 * n)!<GOAL>k⁻¹ • ↑((-1) ^ n * ‖q‖ ^ (2 * n)) = ↑((-1) ^ n * ‖q‖ ^ (2 * n) / k)
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>A B : Set X<VAR>x : X<GOAL>x ∈ derivedSet (A ∪ B) ↔ x ∈ derivedSet A ∪ derivedSet B
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<GOAL>index (↑K) V ≤ index ↑K ↑K₀ * index (↑K₀) V
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>s : Finset G<VAR>h1s : ↑K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' ↑K₀<VAR>h2s : s.card = index ↑K ↑K₀<GOAL>index (↑K) V ≤ index ↑K ↑K₀ * index (↑K₀) V
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>s : Finset G<VAR>h1s : ↑K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' ↑K₀<VAR>h2s : s.card = index ↑K ↑K₀<VAR>t : Finset G<VAR>h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V<VAR>h2t : t.card = index (↑K₀) V<GOAL>index (↑K) V ≤ index ↑K ↑K₀ * index (↑K₀) V
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>s : Finset G<VAR>h1s : ↑K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' ↑K₀<VAR>h2s : s.card = index ↑K ↑K₀<VAR>t : Finset G<VAR>h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V<VAR>h2t : t.card = index (↑K₀) V<GOAL>index (↑K) V ≤ t.card * s.card
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>s : Finset G<VAR>h1s : ↑K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' ↑K₀<VAR>h2s : s.card = index ↑K ↑K₀<VAR>t : Finset G<VAR>h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V<VAR>h2t : t.card = index (↑K₀) V<GOAL>index (↑K) V ≤ (t * s).card
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>s : Finset G<VAR>h1s : ↑K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' ↑K₀<VAR>h2s : s.card = index ↑K ↑K₀<VAR>t : Finset G<VAR>h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V<VAR>h2t : t.card = index (↑K₀) V<GOAL>(t * s).card ∈ Finset.card '' {t | ↑K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>s : Finset G<VAR>h1s : ↑K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' ↑K₀<VAR>h2s : s.card = index ↑K ↑K₀<VAR>t : Finset G<VAR>h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V<VAR>h2t : t.card = index (↑K₀) V<GOAL>t * s ∈ {t | ↑K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>s : Finset G<VAR>h1s : ↑K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' ↑K₀<VAR>h2s : s.card = index ↑K ↑K₀<VAR>t : Finset G<VAR>h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V<VAR>h2t : t.card = index (↑K₀) V<GOAL>↑K ⊆ ⋃ g ∈ t * s, (fun h => g * h) ⁻¹' V
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>s : Finset G<VAR>h1s : ↑K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' ↑K₀<VAR>h2s : s.card = index ↑K ↑K₀<VAR>t : Finset G<VAR>h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V<VAR>h2t : t.card = index (↑K₀) V<GOAL>⋃ g ∈ s, (fun h => g * h) ⁻¹' ↑K₀ ⊆ ⋃ g ∈ t * s, (fun h => g * h) ⁻¹' V
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>s : Finset G<VAR>h1s : ↑K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' ↑K₀<VAR>h2s : s.card = index ↑K ↑K₀<VAR>t : Finset G<VAR>h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V<VAR>h2t : t.card = index (↑K₀) V<GOAL>∀ i ∈ s, (fun h => i * h) ⁻¹' ↑K₀ ⊆ ⋃ g ∈ t * s, (fun h => g * h) ⁻¹' V
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>s : Finset G<VAR>h1s : ↑K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' ↑K₀<VAR>h2s : s.card = index ↑K ↑K₀<VAR>t : Finset G<VAR>h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V<VAR>h2t : t.card = index (↑K₀) V<VAR>g₁ : G<VAR>hg₁ : g₁ ∈ s<GOAL>(fun h => g₁ * h) ⁻¹' ↑K₀ ⊆ ⋃ g ∈ t * s, (fun h => g * h) ⁻¹' V
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>s : Finset G<VAR>h1s : ↑K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' ↑K₀<VAR>h2s : s.card = index ↑K ↑K₀<VAR>t : Finset G<VAR>h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V<VAR>h2t : t.card = index (↑K₀) V<VAR>g₁ : G<VAR>hg₁ : g₁ ∈ s<GOAL>∀ (a : G), g₁ * a ∈ ↑K₀ → a ∈ ⋃ g ∈ t * s, (fun h => g * h) ⁻¹' V
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>s : Finset G<VAR>h1s : ↑K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' ↑K₀<VAR>h2s : s.card = index ↑K ↑K₀<VAR>t : Finset G<VAR>h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V<VAR>h2t : t.card = index (↑K₀) V<VAR>g₁ : G<VAR>hg₁ : g₁ ∈ s<VAR>g₂ : G<VAR>hg₂ : g₁ * g₂ ∈ ↑K₀<VAR>g₃ : G<VAR>hg₃ : g₃ ∈ t<VAR>h2V : g₁ * g₂ ∈ (fun h => (fun h => g₃ * h) ⁻¹' V) hg₃<GOAL>g₂ ∈ ⋃ g ∈ t * s, (fun h => g * h) ⁻¹' V
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>s : Finset G<VAR>h1s : ↑K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' ↑K₀<VAR>h2s : s.card = index ↑K ↑K₀<VAR>t : Finset G<VAR>h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V<VAR>h2t : t.card = index (↑K₀) V<VAR>g₁ : G<VAR>hg₁ : g₁ ∈ s<VAR>g₂ : G<VAR>hg₂ : g₁ * g₂ ∈ ↑K₀<VAR>g₃ : G<VAR>hg₃ : g₃ ∈ t<VAR>h2V : g₃ * g₁ * g₂ ∈ V<GOAL>g₂ ∈ ⋃ g ∈ t * s, (fun h => g * h) ⁻¹' V
<VAR>f : ℝ → ℝ<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<GOAL>∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => x) u ∈ Set.Icc (c₁ * (fun x => x) x) (c₂ * (fun x => x) x)
<VAR>f : ℝ → ℝ<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<GOAL>∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => x) u ∈ Set.Icc (b * (fun x => x) x) (c₂ * (fun x => x) x)
<VAR>f : ℝ → ℝ<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<GOAL>∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => x) u ∈ Set.Icc (b * (fun x => x) x) (1 * (fun x => x) x)
<VAR>f : ℝ → ℝ<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>x u : ℝ<VAR>hu : u ∈ Set.Icc (b * x) x<GOAL>u ∈ Set.Icc (b * x) (1 * x)
<VAR>f : ℝ → ℝ<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>x u : ℝ<VAR>hu : u ∈ Set.Icc (b * x) x<GOAL>b * x ≤ u ∧ u ≤ x
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>R : Type u_4<VAR>A : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : AddMonoid A<VAR>s✝ t u : Set M<VAR>inst✝ : Group G<VAR>s : Set G<GOAL>closure s⁻¹ = (closure s)⁻¹
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>R : Type u_4<VAR>A : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : AddMonoid A<VAR>s✝ t u : Set M<VAR>inst✝ : Group G<VAR>s : Set G<GOAL>closure s⁻¹ ≤ (closure s)⁻¹
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>R : Type u_4<VAR>A : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : AddMonoid A<VAR>s✝ t u : Set M<VAR>inst✝ : Group G<VAR>s : Set G<GOAL>(closure s)⁻¹ ≤ closure s⁻¹
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝⁴ : FunLike F α β<VAR>inst✝³ : CoheytingAlgebra α<VAR>inst✝² : CoheytingAlgebra β<VAR>inst✝¹ : CoheytingAlgebra γ<VAR>inst✝ : CoheytingAlgebra δ<VAR>f f₁ f₂ : CoheytingHom α β<VAR>g g₁ g₂ : CoheytingHom β γ<VAR>hg : Injective ⇑g<VAR>h : g.comp f₁ = g.comp f₂<VAR>a : α<GOAL>g (f₁ a) = g (f₂ a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : ι → α → β<VAR>hp : p ≠ 0<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (i : ι), StronglyMeasurable (f i)<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hfu : UnifIntegrable f p μ<VAR>M : ℝ≥0<VAR>hM : ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑M<VAR>δ : ℝ<VAR>hδpos : 0 < δ<VAR>hδ : ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε<GOAL>∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε