ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>t u : Set E<VAR>h'u : μ u ≠ 0<VAR>t_bound : t ⊆ closedBall 0 1<VAR>A : Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>B : Tendsto (fun r => μ (closedBall x r) / μ ({x} + r • u)) (𝓝[>] 0) (𝓝 (μ (closedBall x 1) / μ ({x} + u)))<VAR>C : Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ (closedBall x r) * (μ (closedBall x r) / μ ({x} + r • u))) (𝓝[>] 0) (𝓝 (0 * (μ (closedBall x 1) / μ ({x} + u))))<GOAL>Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)) (𝓝[>] 0) (𝓝 0)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>t u : Set E<VAR>h'u : μ u ≠ 0<VAR>t_bound : t ⊆ closedBall 0 1<VAR>A : Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>B : Tendsto (fun r => μ (closedBall x r) / μ ({x} + r • u)) (𝓝[>] 0) (𝓝 (μ (closedBall x 1) / μ ({x} + u)))<VAR>C : Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ (closedBall x r) * (μ (closedBall x r) / μ ({x} + r • u))) (𝓝[>] 0) (𝓝 0)<GOAL>Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)) (𝓝[>] 0) (𝓝 0)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>t u : Set E<VAR>h'u : μ u ≠ 0<VAR>t_bound : t ⊆ closedBall 0 1<VAR>A : Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>B : Tendsto (fun r => μ (closedBall x r) / μ ({x} + r • u)) (𝓝[>] 0) (𝓝 (μ (closedBall x 1) / μ ({x} + u)))<VAR>C : Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ (closedBall x r) * (μ (closedBall x r) / μ ({x} + r • u))) (𝓝[>] 0) (𝓝 0)<GOAL>(fun r => μ (s ∩ ({x} + r • t)) / μ (closedBall x r) * (μ (closedBall x r) / μ ({x} + r • u))) =ᶠ[𝓝[>] 0] fun r => μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>t u : Set E<VAR>h'u : μ u ≠ 0<VAR>t_bound : t ⊆ closedBall 0 1<VAR>A : Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>B : Tendsto (fun r => μ (closedBall x r) / μ ({x} + r • u)) (𝓝[>] 0) (𝓝 (μ (closedBall x 1) / μ ({x} + u)))<VAR>C : Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ (closedBall x r) * (μ (closedBall x r) / μ ({x} + r • u))) (𝓝[>] 0) (𝓝 0)<GOAL>∀ a ∈ Ioi 0, μ (s ∩ ({x} + a • t)) / μ (closedBall x a) * (μ (closedBall x a) / μ ({x} + a • u)) = μ (s ∩ ({x} + a • t)) / μ ({x} + a • u)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>t u : Set E<VAR>h'u : μ u ≠ 0<VAR>t_bound : t ⊆ closedBall 0 1<VAR>A : Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>B : Tendsto (fun r => μ (closedBall x r) / μ ({x} + r • u)) (𝓝[>] 0) (𝓝 (μ (closedBall x 1) / μ ({x} + u)))<VAR>C : Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ (closedBall x r) * (μ (closedBall x r) / μ ({x} + r • u))) (𝓝[>] 0) (𝓝 0)<VAR>r : ℝ<VAR>rpos : 0 < r<GOAL>μ (s ∩ ({x} + r • t)) / μ (closedBall x r) * (μ (closedBall x r) / μ ({x} + r • u)) = μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>K : Type u_3<VAR>V : Type u_4<VAR>V' : Type u_5<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>p : Submodule K V<VAR>f : ↥p →ₗ[K] V'<VAR>g : V →ₗ[K] ↥p<VAR>hg : g ∘ₗ p.subtype = id<GOAL>(f ∘ₗ g) ∘ₗ p.subtype = f
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝ : Semiring S<VAR>f✝ : R →+* S<VAR>x✝ : S<VAR>f : R →+* S<VAR>p : R[X]<VAR>n : ℕ<VAR>hn : p.natDegree < n<VAR>x : S<GOAL>eval₂ f x p = ∑ i ∈ range n, f (p.coeff i) * x ^ i
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝ : Semiring S<VAR>f✝ : R →+* S<VAR>x✝ : S<VAR>f : R →+* S<VAR>p : R[X]<VAR>n : ℕ<VAR>hn : p.natDegree < n<VAR>x : S<GOAL>∀ (n : ℕ), f 0 * x ^ n = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝ : Semiring S<VAR>f✝ : R →+* S<VAR>x✝ : S<VAR>f : R →+* S<VAR>p : R[X]<VAR>n : ℕ<VAR>hn : p.natDegree < n<VAR>x : S<VAR>i : ℕ<GOAL>f 0 * x ^ i = 0
<VAR>k G✝ : Type u<VAR>inst✝⁴ : CommRing k<VAR>inst✝³ : Group G✝<VAR>A✝ : Rep k G✝<VAR>G : Type u_1<VAR>A : Type u_2<VAR>inst✝² : Monoid G<VAR>inst✝¹ : AddCommGroup A<VAR>inst✝ : MulAction G A<VAR>f : G × G → A<VAR>hf : IsTwoCocycle f<VAR>g : G<GOAL>f (g, 1) = g • f (1, 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>h : s₁ = s₂<GOAL>(∀ x ∈ s₂, f x = g x) → s₂.prod f = s₂.prod g
<VAR>V : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : SeminormedAddCommGroup V₁<VAR>inst✝¹ : SeminormedAddCommGroup V₂<VAR>inst✝ : SeminormedAddCommGroup V₃<VAR>f✝ g✝ f g : NormedAddGroupHom V₁ V₂<VAR>h : f.toAddMonoidHom = g.toAddMonoidHom<GOAL>⇑f = ⇑g
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace T<VAR>K : Set X<VAR>U : Set Y<VAR>g : C(Y, Z)<VAR>hg : Inducing ⇑g<GOAL>compactOpen = induced g.comp compactOpen
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Denumerable α<VAR>inst✝ : Denumerable β<VAR>m : ℕ<VAR>l : List ℕ<VAR>n : ℕ<GOAL>lower (raise (m :: l) n) n = m :: l
<VAR>ι : Type w<VAR>R : Type u<VAR>M : Type v₁<VAR>N : Type v₂<VAR>P : Type v₃<VAR>Q : Type v₄<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid N<VAR>inst✝⁷ : AddCommMonoid P<VAR>inst✝⁶ : AddCommMonoid Q<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : Module R P<VAR>inst✝² : Module R Q<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>b : Basis ι R M<VAR>f : Dual R M<VAR>p : P<GOAL>((dualTensorHom R M P) (f ⊗ₜ[R] p)).prodMap 0 = (dualTensorHom R (M × N) (P × Q)) ((f ∘ₗ fst R M N) ⊗ₜ[R] (inl R P Q) p)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>C : ℝ<VAR>hf'_gt : ∀ x ∈ interior D, C < deriv f x<VAR>x : ℝ<VAR>hx : x ∈ D<VAR>y : ℝ<VAR>hy : y ∈ D<VAR>hxy : x < y<GOAL>C * (y - x) < f y - f x
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>C : ℝ<VAR>hf'_gt : ∀ x ∈ interior D, C < deriv f x<VAR>x : ℝ<VAR>hx : x ∈ D<VAR>y : ℝ<VAR>hy : y ∈ D<VAR>hxy : x < y<VAR>hxyD : Icc x y ⊆ D<GOAL>C * (y - x) < f y - f x
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>C : ℝ<VAR>hf'_gt : ∀ x ∈ interior D, C < deriv f x<VAR>x : ℝ<VAR>hx : x ∈ D<VAR>y : ℝ<VAR>hy : y ∈ D<VAR>hxy : x < y<VAR>hxyD : Icc x y ⊆ D<VAR>hxyD' : Ioo x y ⊆ interior D<GOAL>C * (y - x) < f y - f x
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>C : ℝ<VAR>hf'_gt : ∀ x ∈ interior D, C < deriv f x<VAR>x : ℝ<VAR>hx : x ∈ D<VAR>y : ℝ<VAR>hy : y ∈ D<VAR>hxy : x < y<VAR>hxyD : Icc x y ⊆ D<VAR>hxyD' : Ioo x y ⊆ interior D<VAR>a : ℝ<VAR>a_mem : a ∈ Ioo x y<VAR>ha : deriv f a = (f y - f x) / (y - x)<GOAL>C * (y - x) < f y - f x
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>C : ℝ<VAR>hf'_gt : ∀ x ∈ interior D, C < deriv f x<VAR>x : ℝ<VAR>hx : x ∈ D<VAR>y : ℝ<VAR>hy : y ∈ D<VAR>hxy : x < y<VAR>hxyD : Icc x y ⊆ D<VAR>hxyD' : Ioo x y ⊆ interior D<VAR>a : ℝ<VAR>a_mem : a ∈ Ioo x y<VAR>ha : deriv f a = (f y - f x) / (y - x)<VAR>this : C < (f y - f x) / (y - x)<GOAL>C * (y - x) < f y - f x
<VAR>J : Type v<VAR>inst✝ : Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>x y : (j : J) × F.obj j<VAR>x✝ : Quot.Rel F x y<VAR>f : x.fst ⟶ y.fst<VAR>h : y.snd = F.map f x.snd<GOAL>F.map f x.snd = F.map (𝟙 y.fst) y.snd
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>h1 : Disjoint H K<VAR>h2 : ↑H * ↑K = univ<GOAL>H.IsComplement' K
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>h1 : Disjoint H K<VAR>h2 : ↑H * ↑K = univ<VAR>g : G<GOAL>∃ a, (fun x => ↑x.1 * ↑x.2) a = g
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>h1 : Disjoint H K<VAR>h2 : ↑H * ↑K = univ<VAR>g h : G<VAR>hh : h ∈ ↑H<VAR>k : G<VAR>hk : k ∈ ↑K<VAR>hg : (fun x x_1 => x * x_1) h k = g<GOAL>∃ a, (fun x => ↑x.1 * ↑x.2) a = g
<VAR>α : Type u_1<VAR>inst✝² : OrderedCancelAddCommMonoid α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<GOAL>map (fun x => x + c) (Ico a b) = Ico (a + c) (b + c)
<VAR>α : Type u_1<VAR>inst✝² : OrderedCancelAddCommMonoid α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<GOAL>map (fun x => c + x) (Ico a b) = Ico (c + a) (c + b)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.111346, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h₁₂ : Homotopy φ₁ φ₂<VAR>h₂₃ : Homotopy φ₂ φ₃<GOAL>φ₁.τ₁ = S₁.f ≫ (h₁₂.h₁ + h₂₃.h₁) + (h₁₂.h₀ + h₂₃.h₀) + φ₃.τ₁
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.111346, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h₁₂ : Homotopy φ₁ φ₂<VAR>h₂₃ : Homotopy φ₂ φ₃<GOAL>S₁.f ≫ h₁₂.h₁ + h₁₂.h₀ + (S₁.f ≫ h₂₃.h₁ + h₂₃.h₀ + φ₃.τ₁) = S₁.f ≫ h₁₂.h₁ + S₁.f ≫ h₂₃.h₁ + (h₁₂.h₀ + h₂₃.h₀) + φ₃.τ₁
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.111346, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h₁₂ : Homotopy φ₁ φ₂<VAR>h₂₃ : Homotopy φ₂ φ₃<GOAL>φ₁.τ₂ = S₁.g ≫ (h₁₂.h₂ + h₂₃.h₂) + (h₁₂.h₁ + h₂₃.h₁) ≫ S₂.f + φ₃.τ₂
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.111346, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h₁₂ : Homotopy φ₁ φ₂<VAR>h₂₃ : Homotopy φ₂ φ₃<GOAL>S₁.g ≫ h₁₂.h₂ + h₁₂.h₁ ≫ S₂.f + (S₁.g ≫ h₂₃.h₂ + h₂₃.h₁ ≫ S₂.f + φ₃.τ₂) = S₁.g ≫ h₁₂.h₂ + S₁.g ≫ h₂₃.h₂ + (h₁₂.h₁ ≫ S₂.f + h₂₃.h₁ ≫ S₂.f) + φ₃.τ₂
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.111346, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h₁₂ : Homotopy φ₁ φ₂<VAR>h₂₃ : Homotopy φ₂ φ₃<GOAL>φ₁.τ₃ = h₁₂.h₃ + h₂₃.h₃ + (h₁₂.h₂ + h₂₃.h₂) ≫ S₂.g + φ₃.τ₃
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.111346, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h₁₂ : Homotopy φ₁ φ₂<VAR>h₂₃ : Homotopy φ₂ φ₃<GOAL>h₁₂.h₃ + h₁₂.h₂ ≫ S₂.g + (h₂₃.h₃ + h₂₃.h₂ ≫ S₂.g + φ₃.τ₃) = h₁₂.h₃ + h₂₃.h₃ + (h₁₂.h₂ ≫ S₂.g + h₂₃.h₂ ≫ S₂.g) + φ₃.τ₃
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsBezout R<VAR>inst✝ : GCDMonoid R<VAR>a b : R<GOAL>∃ x y, gcd a b = a * x + b * y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c✝ c₁ c₂ c₃ s t : Set α<VAR>a✝ b✝ x y : α<VAR>inst✝¹ : IsRefl α r<VAR>hchain : IsChain r s<VAR>inst✝ : IsTrans α r<VAR>a b c : α<VAR>mem1 : a ∈ s<VAR>mem2 : b ∈ s<VAR>mem3 : c ∈ s<GOAL>∃ z, ∃ (_ : z ∈ s), r a z ∧ r b z ∧ r c z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c✝ c₁ c₂ c₃ s t : Set α<VAR>a✝ b✝ x y : α<VAR>inst✝¹ : IsRefl α r<VAR>hchain : IsChain r s<VAR>inst✝ : IsTrans α r<VAR>a b c : α<VAR>mem1 : a ∈ s<VAR>mem2 : b ∈ s<VAR>mem3 : c ∈ s<VAR>z : α<VAR>mem4 : z ∈ s<VAR>H1 : r a z<VAR>H2 : r b z<GOAL>∃ z, ∃ (_ : z ∈ s), r a z ∧ r b z ∧ r c z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c✝ c₁ c₂ c₃ s t : Set α<VAR>a✝ b✝ x y : α<VAR>inst✝¹ : IsRefl α r<VAR>hchain : IsChain r s<VAR>inst✝ : IsTrans α r<VAR>a b c : α<VAR>mem1 : a ∈ s<VAR>mem2 : b ∈ s<VAR>mem3 : c ∈ s<VAR>z : α<VAR>mem4 : z ∈ s<VAR>H1 : r a z<VAR>H2 : r b z<VAR>z' : α<VAR>mem5 : z' ∈ s<VAR>H3 : r z z'<VAR>H4 : r c z'<GOAL>∃ z, ∃ (_ : z ∈ s), r a z ∧ r b z ∧ r c z
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : CompleteSpace E<GOAL>K.topologicalClosure = ⊤ ↔ Kᗮ = ⊥
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : CompleteSpace E<GOAL>Kᗮᗮ = ⊤ ↔ Kᗮ = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : CompleteSpace 𝕜<VAR>r : 𝕜<VAR>hr : ‖r‖ < 1<GOAL>HasSum (fun n => ↑n * r ^ n) (r / (1 - r) ^ 2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : CompleteSpace 𝕜<VAR>r : 𝕜<VAR>hr : ‖r‖ < 1<VAR>A : Summable fun n => ↑n * r ^ n<GOAL>HasSum (fun n => ↑n * r ^ n) (r / (1 - r) ^ 2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : CompleteSpace 𝕜<VAR>r : 𝕜<VAR>hr : ‖r‖ < 1<VAR>A : Summable fun n => ↑n * r ^ n<VAR>B : HasSum (fun x => r ^ x) (1 - r)⁻¹<GOAL>HasSum (fun n => ↑n * r ^ n) (r / (1 - r) ^ 2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : CompleteSpace 𝕜<VAR>r : 𝕜<VAR>hr : ‖r‖ < 1<VAR>A : Summable fun n => ↑n * r ^ n<VAR>B : HasSum (fun x => r ^ x) (1 - r)⁻¹<GOAL>∑' (b : ℕ), ↑b * r ^ b = r / (1 - r) ^ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : CompleteSpace 𝕜<VAR>r : 𝕜<VAR>hr : ‖r‖ < 1<VAR>A : Summable fun n => ↑n * r ^ n<VAR>B : HasSum (fun x => r ^ x) (1 - r)⁻¹<VAR>hr' : r ≠ 1<GOAL>∑' (b : ℕ), ↑b * r ^ b = r / (1 - r) ^ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : CompleteSpace 𝕜<VAR>r : 𝕜<VAR>hr : ‖r‖ < 1<VAR>A : Summable fun n => ↑n * r ^ n<VAR>B : HasSum (fun x => r ^ x) (1 - r)⁻¹<VAR>hr' : r ≠ 1<VAR>s : 𝕜 := ∑' (n : ℕ), ↑n * r ^ n<GOAL>s = r / (1 - r) ^ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : CompleteSpace 𝕜<VAR>r : 𝕜<VAR>hr : ‖r‖ < 1<VAR>A : Summable fun n => ↑n * r ^ n<VAR>B : HasSum (fun x => r ^ x) (1 - r)⁻¹<VAR>hr' : r ≠ 1<VAR>s : 𝕜 := ∑' (n : ℕ), ↑n * r ^ n<VAR>this : Commute (1 - r) s<GOAL>s = r / (1 - r) ^ 2
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : CommSemiring R<VAR>p : R[X]<VAR>t : Multiset ι<VAR>f : ι → R[X]<GOAL>(∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.Monic
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : CommSemiring R<VAR>p : R[X]<VAR>t : Multiset ι<VAR>f : ι → R[X]<GOAL>(∀ i ∈ 0, (f i).Monic) → (Multiset.map f 0).prod.Monic
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : CommSemiring R<VAR>p : R[X]<VAR>t : Multiset ι<VAR>f : ι → R[X]<GOAL>∀ (a : ι) (s : Multiset ι), ((∀ i ∈ s, (f i).Monic) → (Multiset.map f s).prod.Monic) → (∀ i ∈ a ::ₘ s, (f i).Monic) → (Multiset.map f (a ::ₘ s)).prod.Monic
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : CommSemiring R<VAR>p : R[X]<VAR>t✝ : Multiset ι<VAR>f : ι → R[X]<VAR>a : ι<VAR>t : Multiset ι<VAR>ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.Monic<VAR>ht : ∀ i ∈ a ::ₘ t, (f i).Monic<GOAL>(Multiset.map f (a ::ₘ t)).prod.Monic
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : CommSemiring R<VAR>p : R[X]<VAR>t✝ : Multiset ι<VAR>f : ι → R[X]<VAR>a : ι<VAR>t : Multiset ι<VAR>ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.Monic<VAR>ht : ∀ i ∈ a ::ₘ t, (f i).Monic<GOAL>(f a * (Multiset.map f t).prod).Monic
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>σ : Type u_2<VAR>s : Finset σ<VAR>r : σ → R<VAR>k : ℕ<VAR>h : k ≤ s.card<GOAL>(∏ i ∈ s, (X + C (r i))).coeff k = ∑ t ∈ Finset.powersetCard (s.card - k) s, ∏ i ∈ t, r i
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>σ : Type u_2<VAR>s : Finset σ<VAR>r : σ → R<VAR>k : ℕ<VAR>h : k ≤ s.card<GOAL>∑ t ∈ Finset.powersetCard (card s.val - k) s, t.prod r = ∑ t ∈ Finset.powersetCard (s.card - k) s, ∏ i ∈ t, r i
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>h'f : Measurable f<GOAL>Measure.map f ((μ.restrict s).withDensity fun x => ENNReal.ofReal |(f' x).det|) = μ.restrict (f '' s)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>h'f : Measurable f<VAR>t : Set E<VAR>ht : MeasurableSet t<GOAL>(Measure.map f ((μ.restrict s).withDensity fun x => ENNReal.ofReal |(f' x).det|)) t = (μ.restrict (f '' s)) t
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : PartialOrder G<VAR>inst✝² : PartialOrder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>s : Set G<VAR>t : Set P<VAR>hs✝ : s.IsPWO<VAR>ht✝ : t.IsPWO<VAR>a✝ : P<VAR>u : Set G<VAR>hu : u.IsPWO<VAR>v : Set P<VAR>hv : v.IsPWO<VAR>x : G × P<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : P<VAR>x✝ : a ∈ {a | (SMulAntidiagonal hs ht a).Nonempty}<VAR>b : G × P<VAR>hb : b ∈ SMulAntidiagonal hs ht a<GOAL>a ∈ s • t
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : PartialOrder G<VAR>inst✝² : PartialOrder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>s : Set G<VAR>t : Set P<VAR>hs✝ : s.IsPWO<VAR>ht✝ : t.IsPWO<VAR>a✝ : P<VAR>u : Set G<VAR>hu : u.IsPWO<VAR>v : Set P<VAR>hv : v.IsPWO<VAR>x : G × P<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : P<VAR>x✝ : a ∈ {a | (SMulAntidiagonal hs ht a).Nonempty}<VAR>b : G × P<VAR>hb : b.1 ∈ s ∧ b.2 ∈ t ∧ b.1 • b.2 = a<GOAL>a ∈ s • t
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : PartialOrder G<VAR>inst✝² : PartialOrder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>s : Set G<VAR>t : Set P<VAR>hs✝ : s.IsPWO<VAR>ht✝ : t.IsPWO<VAR>a✝ : P<VAR>u : Set G<VAR>hu : u.IsPWO<VAR>v : Set P<VAR>hv : v.IsPWO<VAR>x : G × P<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : P<VAR>x✝ : a ∈ {a | (SMulAntidiagonal hs ht a).Nonempty}<VAR>b : G × P<VAR>hb : b.1 ∈ s ∧ b.2 ∈ t ∧ b.1 • b.2 = a<GOAL>∃ x ∈ s, ∃ y ∈ t, x • y = a
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : PartialOrder G<VAR>inst✝² : PartialOrder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>s : Set G<VAR>t : Set P<VAR>hs✝ : s.IsPWO<VAR>ht✝ : t.IsPWO<VAR>a✝ : P<VAR>u : Set G<VAR>hu : u.IsPWO<VAR>v : Set P<VAR>hv : v.IsPWO<VAR>x : G × P<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : P<VAR>x✝ : a ∈ {a | (SMulAntidiagonal hs ht a).Nonempty}<VAR>b : G × P<VAR>hb : b.1 ∈ s ∧ b.2 ∈ t ∧ b.1 • b.2 = a<GOAL>b.1 ∈ s ∧ ∃ y ∈ t, b.1 • y = a
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : PartialOrder G<VAR>inst✝² : PartialOrder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>s : Set G<VAR>t : Set P<VAR>hs✝ : s.IsPWO<VAR>ht✝ : t.IsPWO<VAR>a✝ : P<VAR>u : Set G<VAR>hu : u.IsPWO<VAR>v : Set P<VAR>hv : v.IsPWO<VAR>x : G × P<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : P<VAR>x✝ : a ∈ {a | (SMulAntidiagonal hs ht a).Nonempty}<VAR>b : G × P<VAR>hb : b.1 ∈ s ∧ b.2 ∈ t ∧ b.1 • b.2 = a<GOAL>∃ y ∈ t, b.1 • y = a
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : PartialOrder G<VAR>inst✝² : PartialOrder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>s : Set G<VAR>t : Set P<VAR>hs✝ : s.IsPWO<VAR>ht✝ : t.IsPWO<VAR>a✝ : P<VAR>u : Set G<VAR>hu : u.IsPWO<VAR>v : Set P<VAR>hv : v.IsPWO<VAR>x : G × P<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : P<VAR>x✝ : a ∈ {a | (SMulAntidiagonal hs ht a).Nonempty}<VAR>b : G × P<VAR>hb : b.1 ∈ s ∧ b.2 ∈ t ∧ b.1 • b.2 = a<GOAL>b.2 ∈ t ∧ b.1 • b.2 = a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Ring S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : IsDomain B<VAR>inst✝⁴ : Algebra A B<VAR>K : Type u_6<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A S<VAR>S' : Type u_7<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra A S'<VAR>pb : PowerBasis A S<VAR>y : S'<VAR>hy : (aeval y) (minpoly A pb.gen) = 0<GOAL>((pb.basis.constr A) fun i => y ^ ↑i) pb.gen = y
<VAR>n : ℕ<GOAL>∑ d ∈ n.divisors, ↑(μ d) * log d = -Λ n
<VAR>n : ℕ<GOAL>∑ x ∈ n.divisors, ↑(μ x) * Real.log ↑x = ∑ x ∈ n.divisorsAntidiagonal, ↑(μ x.1) * -Real.log ↑x.2
<VAR>n : ℕ<GOAL>∑ x ∈ n.divisors, ↑(μ x) * Real.log ↑x = ∑ i ∈ n.divisors, ↑(μ i) * -Real.log ↑(n / i)
<VAR>n : ℕ<VAR>this : ∑ i ∈ n.divisors, ↑(μ i) * -Real.log ↑(n / i) = ∑ i ∈ n.divisors, (↑(μ i) * Real.log ↑i - ↑(μ i) * Real.log ↑n)<GOAL>∑ x ∈ n.divisors, ↑(μ x) * Real.log ↑x = ∑ i ∈ n.divisors, ↑(μ i) * -Real.log ↑(n / i)
<VAR>n : ℕ<VAR>this : ∑ i ∈ n.divisors, ↑(μ i) * -Real.log ↑(n / i) = ∑ i ∈ n.divisors, (↑(μ i) * Real.log ↑i - ↑(μ i) * Real.log ↑n)<GOAL>↑(1 n) * Real.log ↑n = 0