ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α → γ<VAR>g : β → δ<VAR>f₁ : α → β<VAR>g₁ : γ → δ<VAR>f₂ : β → α<VAR>g₂ : δ → γ<VAR>hf : LeftInverse f₁ f₂<VAR>hg : LeftInverse g₁ g₂<VAR>a : β × δ<GOAL>map f₁ g₁ (map f₂ g₂ a) = a
<VAR>k : ℕ<VAR>n : ℤ<VAR>hn : n ≠ 0<GOAL>fourierCoeffOn bernoulliFourierCoeff.proof_1 (fun x => ↑(bernoulliFun k x)) n = 1 / (-2 * ↑π * I * ↑n) * ((if k = 1 then 1 else 0) - ↑k * fourierCoeffOn bernoulliFourierCoeff.proof_1 (fun x => ↑(bernoulliFun (k - 1) x)) n)
<VAR>k : ℕ<VAR>n : ℤ<VAR>hn : n ≠ 0<GOAL>1 / (-2 * ↑π * I * ↑n) * ((fourier (-n)) ↑0 * (↑(bernoulliFun k 1) - ↑(bernoulliFun k 0)) - (↑1 - ↑0) * fourierCoeffOn ⋯ (fun x => ↑(↑k * bernoulliFun (k - 1) x)) n) = 1 / (-2 * ↑π * I * ↑n) * ((if k = 1 then 1 else 0) - ↑k * fourierCoeffOn bernoulliFourierCoeff.proof_1 (fun x => ↑(bernoulliFun (k - 1) x)) n)
<VAR>k : ℕ<VAR>n : ℤ<VAR>hn : n ≠ 0<GOAL>1 / (-2 * ↑π * I * ↑n) * ((fourier (-n)) ↑0 * (↑(bernoulliFun k 1) - ↑(bernoulliFun k 0)) - fourierCoeffOn ⋯ (fun x => ↑(↑k * bernoulliFun (k - 1) x)) n) = 1 / (-2 * ↑π * I * ↑n) * ((if k = 1 then 1 else 0) - ↑k * fourierCoeffOn bernoulliFourierCoeff.proof_1 (fun x => ↑(bernoulliFun (k - 1) x)) n)
<VAR>k : ℕ<VAR>n : ℤ<VAR>hn : n ≠ 0<GOAL>1 / (-2 * ↑π * I * ↑n) * (↑(if k = 1 then 1 else 0) - fourierCoeffOn ⋯ (fun x => ↑(↑k * bernoulliFun (k - 1) x)) n) = 1 / (-2 * ↑π * I * ↑n) * ((if k = 1 then 1 else 0) - ↑k * fourierCoeffOn bernoulliFourierCoeff.proof_1 (fun x => ↑(bernoulliFun (k - 1) x)) n)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>f : Module.Free.ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ) := (canonicalEmbedding.latticeBasis K).indexEquiv (Pi.basisFun ℂ (K →+* ℂ))<VAR>e : index K ≃ Module.Free.ChooseBasisIndex ℤ (𝓞 K) := (indexEquiv K).trans f.symm<VAR>M : Matrix (index K) (index K) ℝ := (mixedEmbedding.stdBasis K).toMatrix ⇑((latticeBasis K).reindex e.symm)<VAR>N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Algebra.embeddingsMatrixReindex ℚ ℂ (⇑(integralBasis K) ∘ ⇑f.symm) RingHom.equivRatAlgHom<GOAL>volume (fundamentalDomain (latticeBasis K)) = 2⁻¹ ^ NrComplexPlaces K * ↑(sqrt ‖discr K‖₊)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>f : Module.Free.ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ) := (canonicalEmbedding.latticeBasis K).indexEquiv (Pi.basisFun ℂ (K →+* ℂ))<VAR>e : index K ≃ Module.Free.ChooseBasisIndex ℤ (𝓞 K) := (indexEquiv K).trans f.symm<VAR>M : Matrix (index K) (index K) ℝ := (mixedEmbedding.stdBasis K).toMatrix ⇑((latticeBasis K).reindex e.symm)<VAR>N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Algebra.embeddingsMatrixReindex ℚ ℂ (⇑(integralBasis K) ∘ ⇑f.symm) RingHom.equivRatAlgHom<GOAL>M.map ⇑ofReal = matrixToStdBasis K * ((reindex (indexEquiv K).symm (indexEquiv K).symm) N)ᵀ
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>f : Module.Free.ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ) := (canonicalEmbedding.latticeBasis K).indexEquiv (Pi.basisFun ℂ (K →+* ℂ))<VAR>e : index K ≃ Module.Free.ChooseBasisIndex ℤ (𝓞 K) := (indexEquiv K).trans f.symm<VAR>M : Matrix (index K) (index K) ℝ := (mixedEmbedding.stdBasis K).toMatrix ⇑((latticeBasis K).reindex e.symm)<VAR>N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Algebra.embeddingsMatrixReindex ℚ ℂ (⇑(integralBasis K) ∘ ⇑f.symm) RingHom.equivRatAlgHom<VAR>i✝ j✝ : index K<GOAL>((mixedEmbedding.stdBasis K).toMatrix ⇑((latticeBasis K).reindex e.symm)).map (⇑ofReal) i✝ j✝ = (matrixToStdBasis K * ((reindex (indexEquiv K).symm (indexEquiv K).symm) N)ᵀ) i✝ j✝
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>f : Module.Free.ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ) := (canonicalEmbedding.latticeBasis K).indexEquiv (Pi.basisFun ℂ (K →+* ℂ))<VAR>e : index K ≃ Module.Free.ChooseBasisIndex ℤ (𝓞 K) := (indexEquiv K).trans f.symm<VAR>M : Matrix (index K) (index K) ℝ := (mixedEmbedding.stdBasis K).toMatrix ⇑((latticeBasis K).reindex e.symm)<VAR>N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Algebra.embeddingsMatrixReindex ℚ ℂ (⇑(integralBasis K) ∘ ⇑f.symm) RingHom.equivRatAlgHom<VAR>i✝ j✝ : index K<GOAL>(matrixToStdBasis K *ᵥ (canonicalEmbedding K) ((integralBasis K) (e j✝)) ∘ ⇑(indexEquiv K)) i✝ = (matrixToStdBasis K * ((reindex (indexEquiv K).symm (indexEquiv K).symm) N)ᵀ) i✝ j✝
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>a b : 𝕜<VAR>s : Set 𝕜<VAR>h : s ∈ 𝓝 a<GOAL>ContinuousOn (dslope f a) s ↔ ContinuousOn f s ∧ DifferentiableAt 𝕜 f a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>a b : 𝕜<VAR>s : Set 𝕜<VAR>h : s ∈ 𝓝 a<GOAL>ContinuousOn f s ∧ DifferentiableAt 𝕜 f a → ContinuousOn (dslope f a) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>a b : 𝕜<VAR>s : Set 𝕜<VAR>h : s ∈ 𝓝 a<VAR>hc : ContinuousOn f s<VAR>hd : DifferentiableAt 𝕜 f a<VAR>x : 𝕜<VAR>hx : x ∈ s<GOAL>ContinuousWithinAt (dslope f a) s x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>b : 𝕜<VAR>s : Set 𝕜<VAR>hc : ContinuousOn f s<VAR>x : 𝕜<VAR>hx : x ∈ s<VAR>h : s ∈ 𝓝 x<VAR>hd : DifferentiableAt 𝕜 f x<GOAL>ContinuousWithinAt (dslope f x) s x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>a b : 𝕜<VAR>s : Set 𝕜<VAR>h : s ∈ 𝓝 a<VAR>hc : ContinuousOn f s<VAR>hd : DifferentiableAt 𝕜 f a<VAR>x : 𝕜<VAR>hx : x ∈ s<VAR>hne : x ≠ a<GOAL>ContinuousWithinAt (dslope f a) s x
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>r : R<VAR>n : ℤ<GOAL>Finsupp.single n r = C r * T n
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>I : MultispanIndex C<VAR>K : Multicofork I<VAR>a : I.L<GOAL>K.ι.app (WalkingMultispan.left a) = I.snd a ≫ K.π (I.sndFrom a)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>I : MultispanIndex C<VAR>K : Multicofork I<VAR>a : I.L<GOAL>I.multispan.map (WalkingMultispan.Hom.snd a) ≫ K.ι.app (WalkingMultispan.right (I.sndFrom a)) = I.snd a ≫ K.π (I.sndFrom a)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>X Y : C<VAR>inst✝ : ExactPairing X Y<GOAL>η_ X Y ▷ X ⊗≫ X ◁ ε_ X Y = ⊗𝟙
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a b c x : α<GOAL>x ∈ Ici a \ {a} ↔ x ∈ Ioi a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>L : List ℕ<GOAL>L.tail.sum = L.sum - L.headI
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : CompleteLattice β<VAR>f : α → β<VAR>hf : LeftOrdContinuous f<VAR>g : ι → α<GOAL>f (⨆ i, g i) = ⨆ i, f (g i)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : CompleteLattice β<VAR>f : α → β<VAR>hf : LeftOrdContinuous f<VAR>g : ι → α<GOAL>sSup (range (f ∘ fun i => g i)) = sSup (range fun i => f (g i))
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a✝ a₁ a₂ b c : G<VAR>inst✝ : Group G<VAR>s✝ s t : Set G<VAR>ht : IsSubgroup t<VAR>h : s ⊆ t<VAR>a : G<VAR>ha : a ∈ closure s<GOAL>a ∈ t
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : T2Space α<VAR>f : α → α<VAR>x y : α<VAR>hy : Tendsto (fun n => f^[n] x) atTop (𝓝 y)<VAR>hf : ContinuousAt f y<GOAL>IsFixedPt f y
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : T2Space α<VAR>f : α → α<VAR>x y : α<VAR>hy : Tendsto (fun n => f^[n] x) atTop (𝓝 y)<VAR>hf : ContinuousAt f y<GOAL>Tendsto (fun n => f^[n + 1] x) atTop (𝓝 (f y))
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : T2Space α<VAR>f : α → α<VAR>x y : α<VAR>hy : Tendsto (fun n => f^[n] x) atTop (𝓝 y)<VAR>hf : ContinuousAt f y<GOAL>Tendsto (fun n => (f ∘ f^[n]) x) atTop (𝓝 (f y))
<VAR>k m n : Nat<VAR>H : k.Coprime m<GOAL>m.gcd (k * n) = m.gcd n
<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>inst✝³ : CanonicallyOrderedAddCommMonoid α<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>f : ℕ → α<VAR>h : Monotone f<VAR>n : ℕ<GOAL>∑ i ∈ range n, (f (i + 1) - f i) = f n - f 0
<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>inst✝³ : CanonicallyOrderedAddCommMonoid α<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>f : ℕ → α<VAR>h : Monotone f<VAR>n : ℕ<GOAL>f 0 - f 0 = 0
<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>inst✝³ : CanonicallyOrderedAddCommMonoid α<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>f : ℕ → α<VAR>h : Monotone f<VAR>n : ℕ<GOAL>∀ (n : ℕ), f (n + 1) - f 0 = f n - f 0 + (f (n + 1) - f n)
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁹ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁸ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁷ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>E : Type u_9<VAR>inst✝⁴ : AddCommMonoid E<VAR>inst✝³ : Module R E<VAR>F : Type u_10<VAR>inst✝² : AddCommMonoid F<VAR>t : ι → Type u_11<VAR>inst✝¹ : (i : ι) → AddCommMonoid (t i)<VAR>inst✝ : (i : ι) → Module R (t i)<VAR>f : (i : ι) → s i →ₗ[R] t i<VAR>e : ι ≃ ι₂<VAR>m : (i : ι₂) → s (e.symm i)<GOAL>((map f ∘ₗ ↑(reindex R s e).symm).compMultilinearMap (tprod R)) m = ((↑(reindex R t e).symm ∘ₗ map fun i => f (e.symm i)).compMultilinearMap (tprod R)) m
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁹ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁸ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁷ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>E : Type u_9<VAR>inst✝⁴ : AddCommMonoid E<VAR>inst✝³ : Module R E<VAR>F : Type u_10<VAR>inst✝² : AddCommMonoid F<VAR>t : ι → Type u_11<VAR>inst✝¹ : (i : ι) → AddCommMonoid (t i)<VAR>inst✝ : (i : ι) → Module R (t i)<VAR>f : (i : ι) → s i →ₗ[R] t i<VAR>e : ι ≃ ι₂<VAR>m : (i : ι₂) → s (e.symm i)<GOAL>(reindex R t e) (((map f ∘ₗ ↑(reindex R s e).symm).compMultilinearMap (tprod R)) m) = (reindex R t e) (((↑(reindex R t e).symm ∘ₗ map fun i => f (e.symm i)).compMultilinearMap (tprod R)) m)
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>N : Type u_4<VAR>α : Type u_5<VAR>inst✝³ : Monoid M<VAR>inst✝² : MulAction M N<VAR>inst✝¹ : SMul N α<VAR>inst✝ : MulAction M α<VAR>s : Set M<VAR>htop : Submonoid.closure s = ⊤<VAR>hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z<GOAL>IsScalarTower M N α
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>N : Type u_4<VAR>α : Type u_5<VAR>inst✝³ : Monoid M<VAR>inst✝² : MulAction M N<VAR>inst✝¹ : SMul N α<VAR>inst✝ : MulAction M α<VAR>s : Set M<VAR>htop : Submonoid.closure s = ⊤<VAR>hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z<VAR>x : M<GOAL>∀ (y : N) (z : α), (1 • y) • z = 1 • y • z
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>N : Type u_4<VAR>α : Type u_5<VAR>inst✝³ : Monoid M<VAR>inst✝² : MulAction M N<VAR>inst✝¹ : SMul N α<VAR>inst✝ : MulAction M α<VAR>s : Set M<VAR>htop : Submonoid.closure s = ⊤<VAR>hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z<VAR>x : M<GOAL>∀ x ∈ s, ∀ (y : M), (∀ (y_1 : N) (z : α), (y • y_1) • z = y • y_1 • z) → ∀ (y_1 : N) (z : α), ((x * y) • y_1) • z = (x * y) • y_1 • z
<VAR>s : ℂ<VAR>hs : 0 < s.re<GOAL>Tendsto (fun n => ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) atTop (𝓝 (Gamma s))
<VAR>s : ℂ<VAR>hs : 0 < s.re<GOAL>Tendsto (fun n => ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) atTop (𝓝 s.GammaIntegral)
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>f : ℕ → ℝ → ℂ := fun n => (Ioc 0 ↑n).indicator fun x => ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)<VAR>f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))<VAR>f_tends : ∀ x ∈ Ioi 0, Tendsto (fun n => f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))<GOAL>Tendsto (fun n => ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) atTop (𝓝 s.GammaIntegral)
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>f : ℕ → ℝ → ℂ := fun n => (Ioc 0 ↑n).indicator fun x => ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)<VAR>f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))<VAR>f_tends : ∀ x ∈ Ioi 0, Tendsto (fun n => f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))<GOAL>(fun n => ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) = fun n => ∫ (a : ℝ) in Ioi 0, f n a
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>f : ℕ → ℝ → ℂ := fun n => (Ioc 0 ↑n).indicator fun x => ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)<VAR>f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))<VAR>f_tends : ∀ x ∈ Ioi 0, Tendsto (fun n => f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))<GOAL>∀ (n : ℕ), ∀ᵐ (a : ℝ) ∂volume.restrict (Ioi 0), ‖f n a‖ ≤ rexp (-a) * a ^ (s.re - 1)
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>P : Finpartition univ<VAR>u : Finset α<VAR>ε : ℝ<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε : ε ≤ 1<GOAL>0 < ε ^ 5
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>P : Finpartition univ<VAR>u : Finset α<VAR>ε : ℝ<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε : ε ≤ 1<GOAL>0 ≤ ε
<VAR>α : Type u<VAR>β : α → Type v<VAR>x y : α<VAR>b : β y<GOAL>x ∈ ⟦AList.singleton y b⟧ ↔ x = y
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : AddCommMonoid N<VAR>inst✝⁵ : Module R N<VAR>inst✝⁴ : Module S M<VAR>inst✝³ : Module S N<VAR>inst✝² : Algebra S R<VAR>inst✝¹ : IsScalarTower S R M<VAR>inst✝ : IsScalarTower S R N<VAR>Q : QuadraticMap R M N<VAR>a : S<VAR>x : M<GOAL>(fun x => Q x) (a • x) = (a * a) • (fun x => Q x) x
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : AddCommMonoid N<VAR>inst✝⁵ : Module R N<VAR>inst✝⁴ : Module S M<VAR>inst✝³ : Module S N<VAR>inst✝² : Algebra S R<VAR>inst✝¹ : IsScalarTower S R M<VAR>inst✝ : IsScalarTower S R N<VAR>Q : QuadraticMap R M N<VAR>B : BilinMap R M N<VAR>h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y<VAR>x y : M<GOAL>(fun x => Q x) (x + y) = (fun x => Q x) x + (fun x => Q x) y + ((LinearMap.restrictScalars₁₂ S S B) x) y
<VAR>α : Type u<VAR>β : Type v<VAR>f : ℕ → α → β<VAR>l : List α<VAR>e : α<GOAL>List.oldMapIdxCore f 0 (l ++ [e]) = List.oldMapIdxCore f 0 l ++ [f l.length e]
<VAR>α : Type u<VAR>β : Type v<VAR>f : ℕ → α → β<VAR>l : List α<VAR>e : α<GOAL>List.oldMapIdxCore f 0 l ++ List.oldMapIdxCore f (0 + l.length) [e] = List.oldMapIdxCore f 0 l ++ [f l.length e]
<VAR>α : Type u<VAR>β : Type v<VAR>f : ℕ → α → β<VAR>l : List α<VAR>e : α<GOAL>List.oldMapIdxCore f 0 l ++ List.oldMapIdxCore f l.length [e] = List.oldMapIdxCore f 0 l ++ [f l.length e]
<VAR>q : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>x : ℝ<GOAL>Irrational (x / ↑q) ↔ q ≠ 0 ∧ Irrational x
<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>l f✝ f₁ f₂ : Filter α✝<VAR>g g₁ g₂ : Filter β<VAR>m : α✝ → β<VAR>m' : β → γ<VAR>s : Set α✝<VAR>t : Set β<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>i : ι<VAR>f : Filter (α i)<GOAL>(comap (eval i) f).NeBot ↔ (∀ (j : ι), Nonempty (α j)) ∧ f.NeBot
<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>l f✝ f₁ f₂ : Filter α✝<VAR>g g₁ g₂ : Filter β<VAR>m : α✝ → β<VAR>m' : β → γ<VAR>s : Set α✝<VAR>t : Set β<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>i : ι<VAR>f : Filter (α i)<VAR>H : IsEmpty ((j : ι) → α j)<GOAL>(comap (eval i) f).NeBot ↔ (∀ (j : ι), Nonempty (α j)) ∧ f.NeBot
<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>l f✝ f₁ f₂ : Filter α✝<VAR>g g₁ g₂ : Filter β<VAR>m : α✝ → β<VAR>m' : β → γ<VAR>s : Set α✝<VAR>t : Set β<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>i : ι<VAR>f : Filter (α i)<VAR>H : Nonempty ((j : ι) → α j)<GOAL>(comap (eval i) f).NeBot ↔ (∀ (j : ι), Nonempty (α j)) ∧ f.NeBot
<VAR>R✝ : Type u_1<VAR>inst✝¹⁰ : CommRing R✝<VAR>I✝ : Ideal R✝<VAR>M✝ : Type u_2<VAR>inst✝⁹ : AddCommGroup M✝<VAR>inst✝⁸ : Module R✝ M✝<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R✝ N<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : IsNoetherianRing R<VAR>ι : Type<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>f : (ι → R) →ₗ[R] M<VAR>hf : Function.Surjective ⇑f<VAR>k : ℕ<VAR>x✝ : autoParam (k + 2 ≤ 4) _auto✝<GOAL>((AdicCompletion.secondRow I M f).sc ⋯ k ⋯).Exact
<VAR>R✝ : Type u_1<VAR>inst✝¹⁰ : CommRing R✝<VAR>I✝ : Ideal R✝<VAR>M✝ : Type u_2<VAR>inst✝⁹ : AddCommGroup M✝<VAR>inst✝⁸ : Module R✝ M✝<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R✝ N<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : IsNoetherianRing R<VAR>ι : Type<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>f : (ι → R) →ₗ[R] M<VAR>hf : Function.Surjective ⇑f<VAR>k : ℕ<VAR>x✝ : autoParam (k + 2 ≤ 4) _auto✝<GOAL>∀ (x₂ : ↑((AdicCompletion.secondRow I M f).sc ⋯ k ⋯).X₂), ((AdicCompletion.secondRow I M f).sc ⋯ k ⋯).g x₂ = 0 → ∃ x₁, ((AdicCompletion.secondRow I M f).sc ⋯ k ⋯).f x₁ = x₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝ : μ.Regular<GOAL>(∃ K, IsCompact K ∧ μ K ≠ 0) ↔ μ ≠ 0
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>A : C<VAR>inst✝ : S.HasHomology<GOAL>(S.leftHomologyπ ≫ S.leftHomologyIso.hom) ≫ S.rightHomologyIso.inv ≫ S.rightHomologyι = S.iCycles ≫ S.pOpcycles
<VAR>α : Type u_1<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<GOAL>Ioc a b = 0 ↔ ¬a < b
<VAR>ι : Type u<VAR>γ✝ : Type w<VAR>β : ι → Type v<VAR>β₁✝ : ι → Type v₁<VAR>β₂✝ : ι → Type v₂<VAR>inst✝⁵ : DecidableEq ι<VAR>ι₁ : Type u_4<VAR>ι₂ : Type u_5<VAR>β₁ : ι₁ → Type u_1<VAR>β₂ : ι₂ → Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : DecidableEq ι₁<VAR>inst✝³ : DecidableEq ι₂<VAR>inst✝² : (i : ι₁) → AddZeroClass (β₁ i)<VAR>inst✝¹ : (i : ι₂) → AddZeroClass (β₂ i)<VAR>inst✝ : AddCommMonoid γ<VAR>h : (i : ι₁) → (j : ι₂) → β₁ i →+ β₂ j →+ γ<VAR>f₁ : (i : ι₁) → β₁ i<VAR>support'✝¹ : Trunc { s // ∀ (i : ι₁), i ∈ s ∨ f₁ i = 0 }<VAR>s₁ : Multiset ι₁<VAR>h₁ : ∀ (i : ι₁), i ∈ s₁ ∨ f₁ i = 0<VAR>f₂ : (i : ι₂) → β₂ i<VAR>support'✝ : Trunc { s // ∀ (i : ι₂), i ∈ s ∨ f₂ i = 0 }<VAR>s₂ : Multiset ι₂<VAR>h₂ : ∀ (i : ι₂), i ∈ s₂ ∨ f₂ i = 0<GOAL>(sumAddHom fun i₂ => (sumAddHom fun i₁ => h i₁ i₂) { toFun := f₁, support' := Quot.mk Setoid.r ⟨s₁, h₁⟩ }) { toFun := f₂, support' := Quot.mk Setoid.r ⟨s₂, h₂⟩ } = (sumAddHom fun i₁ => (sumAddHom fun i₂ => (h i₁ i₂).flip) { toFun := f₂, support' := Quot.mk Setoid.r ⟨s₂, h₂⟩ }) { toFun := f₁, support' := Quot.mk Setoid.r ⟨s₁, h₁⟩ }
<VAR>ι : Type u<VAR>γ✝ : Type w<VAR>β : ι → Type v<VAR>β₁✝ : ι → Type v₁<VAR>β₂✝ : ι → Type v₂<VAR>inst✝⁵ : DecidableEq ι<VAR>ι₁ : Type u_4<VAR>ι₂ : Type u_5<VAR>β₁ : ι₁ → Type u_1<VAR>β₂ : ι₂ → Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : DecidableEq ι₁<VAR>inst✝³ : DecidableEq ι₂<VAR>inst✝² : (i : ι₁) → AddZeroClass (β₁ i)<VAR>inst✝¹ : (i : ι₂) → AddZeroClass (β₂ i)<VAR>inst✝ : AddCommMonoid γ<VAR>h : (i : ι₁) → (j : ι₂) → β₁ i →+ β₂ j →+ γ<VAR>f₁ : (i : ι₁) → β₁ i<VAR>support'✝¹ : Trunc { s // ∀ (i : ι₁), i ∈ s ∨ f₁ i = 0 }<VAR>s₁ : Multiset ι₁<VAR>h₁ : ∀ (i : ι₁), i ∈ s₁ ∨ f₁ i = 0<VAR>f₂ : (i : ι₂) → β₂ i<VAR>support'✝ : Trunc { s // ∀ (i : ι₂), i ∈ s ∨ f₂ i = 0 }<VAR>s₂ : Multiset ι₂<VAR>h₂ : ∀ (i : ι₂), i ∈ s₂ ∨ f₂ i = 0<GOAL>∑ x ∈ s₂.toFinset, ∑ x_1 ∈ s₁.toFinset, ((h x_1 x) (f₁ x_1)) (f₂ x) = ∑ x ∈ s₁.toFinset, ∑ x_1 ∈ s₂.toFinset, ((h x x_1) (f₁ x)) (f₂ x_1)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>inst✝⁷ : Field 𝕂<VAR>inst✝⁶ : Ring 𝔸<VAR>inst✝⁵ : Algebra 𝕂 𝔸<VAR>inst✝⁴ : TopologicalSpace 𝔸<VAR>inst✝³ : TopologicalRing 𝔸<VAR>inst✝² : T2Space 𝔸<VAR>inst✝¹ : StarRing 𝔸<VAR>inst✝ : ContinuousStar 𝔸<VAR>x : 𝔸<GOAL>star (exp 𝕂 x) = exp 𝕂 (star x)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<GOAL>PathConnectedSpace X ↔ ∃ x, pathComponent x = univ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<GOAL>(x ~ᵢ y) ↔ ∀ (s : Set X), IsOpen s → (x ∈ s ↔ y ∈ s)
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>f : Z → X<VAR>h : f ⁻¹' e.source = univ<GOAL>Continuous f ↔ Continuous (↑e ∘ f)
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>f : Z → X<VAR>h : f ⁻¹' e.source = univ<GOAL>ContinuousOn f univ ↔ ContinuousOn (↑e ∘ f) univ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>g✝ : E → F<VAR>c : ℝ≥0<VAR>inst✝ : Fact (1 ≤ p)<VAR>hg : LipschitzWith c g✝<VAR>g0 : g✝ 0 = 0<VAR>f g : ↥(Lp E p μ)<GOAL>dist (hg.compLp g0 f) (hg.compLp g0 g) ≤ ↑c * dist f g
<VAR>α : Type u_1<VAR>n : ℕ<GOAL>(ofNat' (n + 1)).toZNum = (ofNat' n).toZNum + 1
<VAR>α : Type u_1<GOAL>(ofNat' 0).toZNum = (ofNat' (0 + 1)).toZNumNeg + 1
<VAR>α : Type u_1<GOAL>toZNum 0 = (0 + 1).toZNumNeg + 1
<VAR>α : Type u_1<VAR>n : ℕ<GOAL>(ofNat' (n + 1)).toZNumNeg = (ofNat' (n + 1 + 1)).toZNumNeg + 1
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹³ : Ring R<VAR>inst✝¹² : CommRing S<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : AddCommGroup M'<VAR>inst✝⁹ : AddCommGroup M₁<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Module R M'<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : StrongRankCondition R<VAR>inst✝⁴ : Module.Free R M<VAR>inst✝³ : (i : η) → AddCommGroup (φ i)<VAR>inst✝² : (i : η) → Module R (φ i)<VAR>inst✝¹ : ∀ (i : η), Module.Free R (φ i)<VAR>inst✝ : Finite η<GOAL>Module.rank R ((i : η) → φ i) = sum fun i => Module.rank R (φ i)
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹³ : Ring R<VAR>inst✝¹² : CommRing S<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : AddCommGroup M'<VAR>inst✝⁹ : AddCommGroup M₁<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Module R M'<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : StrongRankCondition R<VAR>inst✝⁴ : Module.Free R M<VAR>inst✝³ : (i : η) → AddCommGroup (φ i)<VAR>inst✝² : (i : η) → Module R (φ i)<VAR>inst✝¹ : ∀ (i : η), Module.Free R (φ i)<VAR>inst✝ : Finite η<VAR>val✝ : Fintype η<GOAL>Module.rank R ((i : η) → φ i) = sum fun i => Module.rank R (φ i)