ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>S' : Subalgebra R S<VAR>ι : Type u_3<VAR>ι' : Finset ι<VAR>s l : ι → S<VAR>e : ∑ i ∈ ι', l i * s i = 1<VAR>hs : ∀ (i : ι), s i ∈ S'<VAR>hl : ∀ (i : ι), l i ∈ S'<VAR>x : S<VAR>_i : Algebra ↥S' ↥S' := Algebra.id ↥S'<VAR>n : ι → ℕ<VAR>hn : ∀ (i : ι), s i ^ n i • x ∈ S'<VAR>s' : ι → ↥S' := fun x => ⟨s x, ⋯⟩<VAR>l' : ι → ↥S' := fun x => ⟨l x, ⋯⟩<VAR>e' : ∑ i ∈ ι', l' i * s' i = 1<VAR>this : Ideal.span (s' '' ↑ι') = ⊤<GOAL>x ∈ toSubmodule (ofId (↥S') S).range
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>S' : Subalgebra R S<VAR>ι : Type u_3<VAR>ι' : Finset ι<VAR>s l : ι → S<VAR>e : ∑ i ∈ ι', l i * s i = 1<VAR>hs : ∀ (i : ι), s i ∈ S'<VAR>hl : ∀ (i : ι), l i ∈ S'<VAR>x : S<VAR>_i : Algebra ↥S' ↥S' := Algebra.id ↥S'<VAR>n : ι → ℕ<VAR>hn : ∀ (i : ι), s i ^ n i • x ∈ S'<VAR>s' : ι → ↥S' := fun x => ⟨s x, ⋯⟩<VAR>l' : ι → ↥S' := fun x => ⟨l x, ⋯⟩<VAR>e' : ∑ i ∈ ι', l' i * s' i = 1<VAR>this : Ideal.span (s' '' ↑ι') = ⊤<VAR>N : ℕ := ι'.sup n<GOAL>x ∈ toSubmodule (ofId (↥S') S).range
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>S' : Subalgebra R S<VAR>ι : Type u_3<VAR>ι' : Finset ι<VAR>s l : ι → S<VAR>e : ∑ i ∈ ι', l i * s i = 1<VAR>hs : ∀ (i : ι), s i ∈ S'<VAR>hl : ∀ (i : ι), l i ∈ S'<VAR>x : S<VAR>_i : Algebra ↥S' ↥S' := Algebra.id ↥S'<VAR>n : ι → ℕ<VAR>hn : ∀ (i : ι), s i ^ n i • x ∈ S'<VAR>s' : ι → ↥S' := fun x => ⟨s x, ⋯⟩<VAR>l' : ι → ↥S' := fun x => ⟨l x, ⋯⟩<VAR>e' : ∑ i ∈ ι', l' i * s' i = 1<VAR>this : Ideal.span (s' '' ↑ι') = ⊤<VAR>N : ℕ := ι'.sup n<VAR>hN : Ideal.span ((fun x => x ^ N) '' (s' '' ↑ι')) = ⊤<GOAL>x ∈ toSubmodule (ofId (↥S') S).range
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>S' : Subalgebra R S<VAR>ι : Type u_3<VAR>ι' : Finset ι<VAR>s l : ι → S<VAR>e : ∑ i ∈ ι', l i * s i = 1<VAR>hs : ∀ (i : ι), s i ∈ S'<VAR>hl : ∀ (i : ι), l i ∈ S'<VAR>x : S<VAR>_i : Algebra ↥S' ↥S' := Algebra.id ↥S'<VAR>n : ι → ℕ<VAR>hn : ∀ (i : ι), s i ^ n i • x ∈ S'<VAR>s' : ι → ↥S' := fun x => ⟨s x, ⋯⟩<VAR>l' : ι → ↥S' := fun x => ⟨l x, ⋯⟩<VAR>e' : ∑ i ∈ ι', l' i * s' i = 1<VAR>this : Ideal.span (s' '' ↑ι') = ⊤<VAR>N : ℕ := ι'.sup n<VAR>hN : Ideal.span ((fun x => x ^ N) '' (s' '' ↑ι')) = ⊤<GOAL>∀ (r : ↑((fun x => x ^ N) '' (s' '' ↑ι'))), ↑r • x ∈ toSubmodule (ofId (↥S') S).range
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>S' : Subalgebra R S<VAR>ι : Type u_3<VAR>ι' : Finset ι<VAR>s l : ι → S<VAR>e : ∑ i ∈ ι', l i * s i = 1<VAR>hs : ∀ (i : ι), s i ∈ S'<VAR>hl : ∀ (i : ι), l i ∈ S'<VAR>x : S<VAR>_i : Algebra ↥S' ↥S' := Algebra.id ↥S'<VAR>n : ι → ℕ<VAR>hn : ∀ (i : ι), s i ^ n i • x ∈ S'<VAR>s' : ι → ↥S' := fun x => ⟨s x, ⋯⟩<VAR>l' : ι → ↥S' := fun x => ⟨l x, ⋯⟩<VAR>e' : ∑ i ∈ ι', l' i * s' i = 1<VAR>this : Ideal.span (s' '' ↑ι') = ⊤<VAR>N : ℕ := ι'.sup n<VAR>hN : Ideal.span ((fun x => x ^ N) '' (s' '' ↑ι')) = ⊤<VAR>i : ι<VAR>hi : i ∈ ↑ι'<GOAL>s' i ^ N • x ∈ toSubmodule (ofId (↥S') S).range
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>S' : Subalgebra R S<VAR>ι : Type u_3<VAR>ι' : Finset ι<VAR>s l : ι → S<VAR>e : ∑ i ∈ ι', l i * s i = 1<VAR>hs : ∀ (i : ι), s i ∈ S'<VAR>hl : ∀ (i : ι), l i ∈ S'<VAR>x : S<VAR>_i : Algebra ↥S' ↥S' := Algebra.id ↥S'<VAR>n : ι → ℕ<VAR>hn : ∀ (i : ι), s i ^ n i • x ∈ S'<VAR>s' : ι → ↥S' := fun x => ⟨s x, ⋯⟩<VAR>l' : ι → ↥S' := fun x => ⟨l x, ⋯⟩<VAR>e' : ∑ i ∈ ι', l' i * s' i = 1<VAR>this : Ideal.span (s' '' ↑ι') = ⊤<VAR>N : ℕ := ι'.sup n<VAR>hN : Ideal.span ((fun x => x ^ N) '' (s' '' ↑ι')) = ⊤<VAR>i : ι<VAR>hi : i ∈ ↑ι'<GOAL>s' i ^ (N - n i) • s' i ^ n i • x ∈ toSubmodule (ofId (↥S') S).range
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>S' : Subalgebra R S<VAR>ι : Type u_3<VAR>ι' : Finset ι<VAR>s l : ι → S<VAR>e : ∑ i ∈ ι', l i * s i = 1<VAR>hs : ∀ (i : ι), s i ∈ S'<VAR>hl : ∀ (i : ι), l i ∈ S'<VAR>x : S<VAR>_i : Algebra ↥S' ↥S' := Algebra.id ↥S'<VAR>n : ι → ℕ<VAR>hn : ∀ (i : ι), s i ^ n i • x ∈ S'<VAR>s' : ι → ↥S' := fun x => ⟨s x, ⋯⟩<VAR>l' : ι → ↥S' := fun x => ⟨l x, ⋯⟩<VAR>e' : ∑ i ∈ ι', l' i * s' i = 1<VAR>this : Ideal.span (s' '' ↑ι') = ⊤<VAR>N : ℕ := ι'.sup n<VAR>hN : Ideal.span ((fun x => x ^ N) '' (s' '' ↑ι')) = ⊤<VAR>i : ι<VAR>hi : i ∈ ↑ι'<GOAL>s' i ^ n i • x ∈ toSubmodule (ofId (↥S') S).range
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>ι2 : Type u_5<VAR>f : ι2 ↪ ι<VAR>p : ι → P<VAR>ha : AffineIndependent k p<GOAL>AffineIndependent k (p ∘ ⇑f)
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>hp : p.Monic<VAR>q : R[X]<VAR>hq : q ≠ 0<VAR>h : ¬p = 1<GOAL>p * q ≠ 0
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>hp : p.Monic<VAR>q : R[X]<VAR>hq : q ≠ 0<VAR>h : ¬p = 1<GOAL>¬q = 0 ∧ ¬p.degree = ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>hp : p.Monic<VAR>q : R[X]<VAR>hq : q ≠ 0<VAR>h : ¬p = 1<GOAL>¬p.degree = ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>hp : p.Monic<VAR>q : R[X]<VAR>hq : q ≠ 0<VAR>h : 0 < p.degree<GOAL>¬p.degree = ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>hp : p.Monic<VAR>q : R[X]<VAR>hq : q ≠ 0<VAR>h : 0 < p.degree<GOAL>⊥ < 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_4}<GOAL>o.pred < o ↔ ¬o.pred = o
<VAR>a : ℝ<GOAL>interior {z | z.im ≤ a} = {z | z.im < a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : AddCommMonoid M<VAR>v v₁ v₂ : α →₀ M<VAR>f : α → β<VAR>hf : Injective f<VAR>x : α →₀ M<VAR>a : α<GOAL>(mapDomain f x) (f a) = x a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : AddCommMonoid M<VAR>v v₁ v₂ : α →₀ M<VAR>f : α → β<VAR>hf : Injective f<VAR>x : α →₀ M<VAR>a : α<GOAL>∀ (b : α), x b ≠ 0 → b ≠ a → (single (f b) (x b)) (f a) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : AddCommMonoid M<VAR>v v₁ v₂ : α →₀ M<VAR>f : α → β<VAR>hf : Injective f<VAR>x : α →₀ M<VAR>a : α<GOAL>x a = 0 → (single (f a) 0) (f a) = 0
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : SeminormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>p : Submodule 𝕜 E<VAR>f : ↥p →L[𝕜] F<VAR>inst✝ : FiniteDimensional 𝕜 ↥(LinearMap.range f)<VAR>b : Basis (Fin (finrank 𝕜 ↥(LinearMap.range f))) 𝕜 ↥(LinearMap.range f) := finBasis 𝕜 ↥(LinearMap.range f)<VAR>e : ↥(LinearMap.range f) ≃L[𝕜] Fin (finrank 𝕜 ↥(LinearMap.range f)) → 𝕜 := b.equivFunL<GOAL>∃ g, f = g.comp p.subtypeL
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : SeminormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>p : Submodule 𝕜 E<VAR>f : ↥p →L[𝕜] F<VAR>inst✝ : FiniteDimensional 𝕜 ↥(LinearMap.range f)<VAR>b : Basis (Fin (finrank 𝕜 ↥(LinearMap.range f))) 𝕜 ↥(LinearMap.range f) := finBasis 𝕜 ↥(LinearMap.range f)<VAR>e : ↥(LinearMap.range f) ≃L[𝕜] Fin (finrank 𝕜 ↥(LinearMap.range f)) → 𝕜 := b.equivFunL<VAR>fi : Fin (finrank 𝕜 ↥(LinearMap.range f)) → ↥p →L[𝕜] 𝕜 := fun i => (LinearMap.toContinuousLinearMap (b.coord i)).comp (f.codRestrict (LinearMap.range f) ⋯)<GOAL>∃ g, f = g.comp p.subtypeL
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : SeminormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>p : Submodule 𝕜 E<VAR>f : ↥p →L[𝕜] F<VAR>inst✝ : FiniteDimensional 𝕜 ↥(LinearMap.range f)<VAR>b : Basis (Fin (finrank 𝕜 ↥(LinearMap.range f))) 𝕜 ↥(LinearMap.range f) := finBasis 𝕜 ↥(LinearMap.range f)<VAR>e : ↥(LinearMap.range f) ≃L[𝕜] Fin (finrank 𝕜 ↥(LinearMap.range f)) → 𝕜 := b.equivFunL<VAR>fi : Fin (finrank 𝕜 ↥(LinearMap.range f)) → ↥p →L[𝕜] 𝕜 := fun i => (LinearMap.toContinuousLinearMap (b.coord i)).comp (f.codRestrict (LinearMap.range f) ⋯)<VAR>gi : Fin (finrank 𝕜 ↥(LinearMap.range f)) → E →L[𝕜] 𝕜<VAR>hgf : ∀ (i : Fin (finrank 𝕜 ↥(LinearMap.range f))) (x : ↥p), (gi i) ↑x = (fi i) x<VAR>a✝ : ∀ (i : Fin (finrank 𝕜 ↥(LinearMap.range f))), ‖gi i‖ = ‖fi i‖<GOAL>∃ g, f = g.comp p.subtypeL
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : SeminormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>p : Submodule 𝕜 E<VAR>f : ↥p →L[𝕜] F<VAR>inst✝ : FiniteDimensional 𝕜 ↥(LinearMap.range f)<VAR>b : Basis (Fin (finrank 𝕜 ↥(LinearMap.range f))) 𝕜 ↥(LinearMap.range f) := finBasis 𝕜 ↥(LinearMap.range f)<VAR>e : ↥(LinearMap.range f) ≃L[𝕜] Fin (finrank 𝕜 ↥(LinearMap.range f)) → 𝕜 := b.equivFunL<VAR>fi : Fin (finrank 𝕜 ↥(LinearMap.range f)) → ↥p →L[𝕜] 𝕜 := fun i => (LinearMap.toContinuousLinearMap (b.coord i)).comp (f.codRestrict (LinearMap.range f) ⋯)<VAR>gi : Fin (finrank 𝕜 ↥(LinearMap.range f)) → E →L[𝕜] 𝕜<VAR>hgf : ∀ (i : Fin (finrank 𝕜 ↥(LinearMap.range f))) (x : ↥p), (gi i) ↑x = (fi i) x<VAR>a✝ : ∀ (i : Fin (finrank 𝕜 ↥(LinearMap.range f))), ‖gi i‖ = ‖fi i‖<GOAL>f = ((LinearMap.range f).subtypeL.comp ((↑e.symm).comp (pi gi))).comp p.subtypeL
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>∫ (x : ℝ) in a..b, sin x ^ 3 = cos a - cos b - (cos a ^ 3 - cos b ^ 3) / 3
<VAR>a b : ℝ<VAR>n : ℕ<VAR>this : ∫ (x : ℝ) in a..b, sin x ^ (2 * 1 + 1) * cos x ^ 0 = ∫ (u : ℝ) in cos b..cos a, u ^ 0 * (1 - u ^ 2) ^ 1<GOAL>∫ (x : ℝ) in a..b, sin x ^ 3 = cos a - cos b - (cos a ^ 3 - cos b ^ 3) / 3
<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>c : F<VAR>h0 : p ≠ 0<VAR>h_top : p ≠ ⊤<GOAL>eLpNorm (fun x => c) p μ = ↑‖c‖₊ * μ Set.univ ^ (1 / p.toReal)
<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>x : X<VAR>hx : x ∈ e.source<GOAL>Tendsto (↑e.symm) (𝓝 (↑e x)) (𝓝 x)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>p✝ q✝ : R[X]<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : Nontrivial S<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>p q : R[X]<VAR>h : IsCoprime p q<VAR>s : S<GOAL>(aeval s) p ≠ 0 ∨ (aeval s) q ≠ 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>p✝ q✝ : R[X]<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : Nontrivial S<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>p q : R[X]<VAR>h : IsCoprime p q<VAR>s : S<VAR>hpq : (aeval s) p = 0 ∧ (aeval s) q = 0<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>p✝ q✝ : R[X]<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : Nontrivial S<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>p q : R[X]<VAR>s : S<VAR>hpq : (aeval s) p = 0 ∧ (aeval s) q = 0<VAR>w✝¹ w✝ : R[X]<VAR>h : (aeval s) (w✝¹ * p + w✝ * q) = (aeval s) 1<GOAL>False
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>N : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module R N<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Qₙ : QuadraticForm R N<VAR>f₁ : Q₁ →qᵢ Qₙ<VAR>f₂ : Q₂ →qᵢ Qₙ<VAR>hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)<VAR>m₁ : CliffordAlgebra Q₁<VAR>m₂ : CliffordAlgebra Q₂<VAR>hm₁ : m₁ ∈ evenOdd Q₁ 1<VAR>hm₂ : m₂ ∈ evenOdd Q₂ 1<GOAL>(map f₁) m₁ * (map f₂) m₂ = -(map f₂) m₂ * (map f₁) m₁
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t : Set α<VAR>h : y ∈ ball x ε<VAR>this : 0 < ε - edist y x<GOAL>∃ ε' > 0, ball y ε' ⊆ ball x ε
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t : Set α<VAR>h : y ∈ ball x ε<VAR>this : 0 < ε - edist y x<GOAL>edist y x + (ε - edist y x) ≤ ε
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>f : R[X]<VAR>T : Type u_1<VAR>inst✝¹ : CommRing T<VAR>inst✝ : Algebra R T<VAR>h : IsAdjoinRoot S f<VAR>h' : IsAdjoinRoot T f<VAR>z : R[X]<GOAL>(h.aequiv h') (h.map z) = h'.map z
<VAR>Ω : Type u_1<VAR>inst✝ : MeasurableSpace Ω<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : Measure Ω<VAR>μs : ι → Measure Ω<VAR>E₀ E E₁ : Set Ω<VAR>E₀_subset : E₀ ⊆ E<VAR>subset_E₁ : E ⊆ E₁<VAR>nulldiff : μ (E₁ \ E₀) = 0<VAR>h_E₀ : μ E₀ ≤ liminf (fun i => (μs i) E₀) L<VAR>h_E₁ : limsup (fun i => (μs i) E₁) L ≤ μ E₁<GOAL>Tendsto (fun i => (μs i) E) L (𝓝 (μ E))
<VAR>Ω : Type u_1<VAR>inst✝ : MeasurableSpace Ω<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : Measure Ω<VAR>μs : ι → Measure Ω<VAR>E₀ E E₁ : Set Ω<VAR>E₀_subset : E₀ ⊆ E<VAR>subset_E₁ : E ⊆ E₁<VAR>nulldiff : μ (E₁ \ E₀) = 0<VAR>h_E₀ : μ E₀ ≤ liminf (fun i => (μs i) E₀) L<VAR>h_E₁ : limsup (fun i => (μs i) E₁) L ≤ μ E₁<GOAL>μ E ≤ liminf (fun i => (μs i) E) L
<VAR>Ω : Type u_1<VAR>inst✝ : MeasurableSpace Ω<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : Measure Ω<VAR>μs : ι → Measure Ω<VAR>E₀ E E₁ : Set Ω<VAR>E₀_subset : E₀ ⊆ E<VAR>subset_E₁ : E ⊆ E₁<VAR>nulldiff : μ (E₁ \ E₀) = 0<VAR>h_E₀ : μ E₀ ≤ liminf (fun i => (μs i) E₀) L<VAR>h_E₁ : limsup (fun i => (μs i) E₁) L ≤ μ E₁<GOAL>limsup (fun i => (μs i) E) L ≤ μ E
<VAR>Ω : Type u_1<VAR>inst✝ : MeasurableSpace Ω<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : Measure Ω<VAR>μs : ι → Measure Ω<VAR>E₀ E E₁ : Set Ω<VAR>E₀_subset : E₀ ⊆ E<VAR>subset_E₁ : E ⊆ E₁<VAR>nulldiff : μ (E₁ \ E₀) = 0<VAR>h_E₀ : μ E₀ ≤ liminf (fun i => (μs i) E₀) L<VAR>h_E₁ : limsup (fun i => (μs i) E₁) L ≤ μ E₁<GOAL>autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) L fun i => (μs i) E) _auto✝
<VAR>Ω : Type u_1<VAR>inst✝ : MeasurableSpace Ω<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : Measure Ω<VAR>μs : ι → Measure Ω<VAR>E₀ E E₁ : Set Ω<VAR>E₀_subset : E₀ ⊆ E<VAR>subset_E₁ : E ⊆ E₁<VAR>nulldiff : μ (E₁ \ E₀) = 0<VAR>h_E₀ : μ E₀ ≤ liminf (fun i => (μs i) E₀) L<VAR>h_E₁ : limsup (fun i => (μs i) E₁) L ≤ μ E₁<GOAL>autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) L fun i => (μs i) E) _auto✝
<VAR>θ : Angle<GOAL>(2 • θ).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2
<VAR>θ : Angle<GOAL>(2 • ↑θ.toReal).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2
<VAR>θ : Angle<GOAL>-3 * π < 2 * θ.toReal ∧ 2 * θ.toReal ≤ -π ↔ θ.toReal ≤ -π / 2
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>inst✝¹ : Inhabited Γ<VAR>inst✝ : Inhabited Γ'<VAR>f : PointedMap Γ Γ'<VAR>l : List Γ<GOAL>(List.map f.f l).headI = f.f l.headI
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>inst✝⁵ : DecidableEq α<VAR>M : α → Type u_3<VAR>P : α → Type u_4<VAR>inst✝⁴ : (a : α) → Zero (N a)<VAR>inst✝³ : (a : α) → Zero (M a)<VAR>inst✝² : (a : α) → Zero (P a)<VAR>inst✝¹ : (a : α) → DecidableEq (N a)<VAR>inst✝ : (a : α) → DecidableEq (P a)<VAR>F : (a : α) → M a → N a → P a<VAR>F0 : ∀ (a : α), F a 0 0 = 0<VAR>f : Π₀ (a : α), M a<VAR>g₁ g₂ : Π₀ (a : α), N a<VAR>hF : ∀ (a : α) (f : M a), Function.Injective fun g => F a f g<VAR>a : α<GOAL>a ∈ (zipWith F F0 f g₁).neLocus (zipWith F F0 f g₂) ↔ a ∈ g₁.neLocus g₂
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.38366, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K✝ K' : ChainComplex C ℕ<VAR>f : K✝ ⟶ K'<VAR>Δ✝ Δ' Δ'' : SimplexCategory<VAR>inst✝ : HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<VAR>Δ : SimplexCategoryᵒᵖ<VAR>x✝ : Discrete (Splitting.IndexSet Δ)<VAR>A : Splitting.IndexSet Δ<GOAL>colimit.ι (Discrete.functor fun A => Obj.summand K Δ A) { as := A } ≫ Obj.map K (𝟙 Δ) = colimit.ι (Discrete.functor fun A => Obj.summand K Δ A) { as := A } ≫ 𝟙 (Obj.obj₂ K Δ)
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.38366, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K✝ K' : ChainComplex C ℕ<VAR>f : K✝ ⟶ K'<VAR>Δ✝ Δ' Δ'' : SimplexCategory<VAR>inst✝ : HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<VAR>Δ : SimplexCategoryᵒᵖ<VAR>x✝ : Discrete (Splitting.IndexSet Δ)<VAR>A : Splitting.IndexSet Δ<VAR>fac : A.e ≫ 𝟙 (unop A.fst) = (𝟙 Δ).unop ≫ A.e<GOAL>colimit.ι (Discrete.functor fun A => Obj.summand K Δ A) { as := A } ≫ Obj.map K (𝟙 Δ) = colimit.ι (Discrete.functor fun A => Obj.summand K Δ A) { as := A } ≫ 𝟙 (Obj.obj₂ K Δ)
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.38366, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K✝ K' : ChainComplex C ℕ<VAR>f : K✝ ⟶ K'<VAR>Δ✝ Δ' Δ'' : SimplexCategory<VAR>inst✝ : HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<VAR>Δ : SimplexCategoryᵒᵖ<VAR>x✝ : Discrete (Splitting.IndexSet Δ)<VAR>A : Splitting.IndexSet Δ<VAR>fac : A.e ≫ 𝟙 (unop A.fst) = (𝟙 Δ).unop ≫ A.e<GOAL>Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk A.e) = colimit.ι (Discrete.functor fun A => Obj.summand K Δ A) { as := A }
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.38366, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K✝ K' : ChainComplex C ℕ<VAR>f : K✝ ⟶ K'<VAR>Δ✝ Δ'✝ Δ''✝ : SimplexCategory<VAR>inst✝ : HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<VAR>Δ'' Δ' Δ : SimplexCategoryᵒᵖ<VAR>θ' : Δ'' ⟶ Δ'<VAR>θ : Δ' ⟶ Δ<VAR>x✝ : Discrete (Splitting.IndexSet Δ'')<VAR>A : Splitting.IndexSet Δ''<GOAL>colimit.ι (Discrete.functor fun A => Obj.summand K Δ'' A) { as := A } ≫ { obj := fun Δ => Obj.obj₂ K Δ, map := fun {X Y} θ => Obj.map K θ }.map (θ' ≫ θ) = colimit.ι (Discrete.functor fun A => Obj.summand K Δ'' A) { as := A } ≫ { obj := fun Δ => Obj.obj₂ K Δ, map := fun {X Y} θ => Obj.map K θ }.map θ' ≫ { obj := fun Δ => Obj.obj₂ K Δ, map := fun {X Y} θ => Obj.map K θ }.map θ
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.38366, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K✝ K' : ChainComplex C ℕ<VAR>f : K✝ ⟶ K'<VAR>Δ✝ Δ'✝ Δ''✝ : SimplexCategory<VAR>inst✝ : HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<VAR>Δ'' Δ' Δ : SimplexCategoryᵒᵖ<VAR>θ' : Δ'' ⟶ Δ'<VAR>θ : Δ' ⟶ Δ<VAR>x✝ : Discrete (Splitting.IndexSet Δ'')<VAR>A : Splitting.IndexSet Δ''<VAR>fac : θ.unop ≫ θ'.unop ≫ A.e = (θ' ≫ θ).unop ≫ A.e<GOAL>colimit.ι (Discrete.functor fun A => Obj.summand K Δ'' A) { as := A } ≫ { obj := fun Δ => Obj.obj₂ K Δ, map := fun {X Y} θ => Obj.map K θ }.map (θ' ≫ θ) = colimit.ι (Discrete.functor fun A => Obj.summand K Δ'' A) { as := A } ≫ { obj := fun Δ => Obj.obj₂ K Δ, map := fun {X Y} θ => Obj.map K θ }.map θ' ≫ { obj := fun Δ => Obj.obj₂ K Δ, map := fun {X Y} θ => Obj.map K θ }.map θ
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.38366, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K✝ K' : ChainComplex C ℕ<VAR>f : K✝ ⟶ K'<VAR>Δ✝ Δ'✝ Δ''✝ : SimplexCategory<VAR>inst✝ : HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<VAR>Δ'' Δ' Δ : SimplexCategoryᵒᵖ<VAR>θ' : Δ'' ⟶ Δ'<VAR>θ : Δ' ⟶ Δ<VAR>x✝ : Discrete (Splitting.IndexSet Δ'')<VAR>A : Splitting.IndexSet Δ''<VAR>fac : factorThruImage (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)) ≫ image.ι (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)) ≫ image.ι (θ'.unop ≫ A.e) = (θ' ≫ θ).unop ≫ A.e<GOAL>colimit.ι (Discrete.functor fun A => Obj.summand K Δ'' A) { as := A } ≫ { obj := fun Δ => Obj.obj₂ K Δ, map := fun {X Y} θ => Obj.map K θ }.map (θ' ≫ θ) = colimit.ι (Discrete.functor fun A => Obj.summand K Δ'' A) { as := A } ≫ { obj := fun Δ => Obj.obj₂ K Δ, map := fun {X Y} θ => Obj.map K θ }.map θ' ≫ { obj := fun Δ => Obj.obj₂ K Δ, map := fun {X Y} θ => Obj.map K θ }.map θ
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.38366, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K✝ K' : ChainComplex C ℕ<VAR>f : K✝ ⟶ K'<VAR>Δ✝ Δ'✝ Δ''✝ : SimplexCategory<VAR>inst✝ : HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<VAR>Δ'' Δ' Δ : SimplexCategoryᵒᵖ<VAR>θ' : Δ'' ⟶ Δ'<VAR>θ : Δ' ⟶ Δ<VAR>x✝ : Discrete (Splitting.IndexSet Δ'')<VAR>A : Splitting.IndexSet Δ''<VAR>fac : factorThruImage (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)) ≫ image.ι (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)) ≫ image.ι (θ'.unop ≫ A.e) = (θ' ≫ θ).unop ≫ A.e<GOAL>Obj.Termwise.mapMono K (image.ι (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)) ≫ image.ι (θ'.unop ≫ A.e)) ≫ Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk (factorThruImage (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)))) = Obj.Termwise.mapMono K (image.ι (θ.unop ≫ (A.pull θ').e) ≫ image.ι (θ'.unop ≫ A.e)) ≫ Sigma.ι (Obj.summand K Δ) ((A.pull θ').pull θ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝¹ : UniformSpace β<VAR>δ : ι → Type u_5<VAR>inst✝ : (i : ι) → UniformSpace (δ i)<VAR>δ₁ : Type u_6<VAR>δ₂ : Type u_7<VAR>φ₁ : δ₁ → α<VAR>φ₂ : δ₂ → α<VAR>h_cover : range φ₁ ∪ range φ₂ = univ<GOAL>𝓤 (α →ᵤ β) = 𝓤 (α →ᵤ β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝¹ : UniformSpace β<VAR>δ : ι → Type u_5<VAR>inst✝ : (i : ι) → UniformSpace (δ i)<VAR>δ₁ : Type u_6<VAR>δ₂ : Type u_7<VAR>φ₁ : δ₁ → α<VAR>φ₂ : δ₂ → α<VAR>h_cover : range φ₁ ∪ range φ₂ = univ<GOAL>𝓤 (α →ᵤ β) ≤ 𝓤 (α →ᵤ β)
<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>σ : α → Type u_6<VAR>s : Finset α<VAR>t : (a : α) → Finset (σ a)<VAR>f : Sigma σ → β<GOAL>∏ x ∈ s.sigma t, f x = ∏ a ∈ s, ∏ s ∈ t a, f ⟨a, s⟩
<VAR>G : Type w<VAR>inst✝³ : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝² : R1Space G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>h : ∀ (g : G) {K : Compacts G}, (fun s => ↑(μ.toFun s)) (Compacts.map (fun b => g * b) ⋯ K) = (fun s => ↑(μ.toFun s)) K<VAR>g : G<VAR>A : Set G<GOAL>μ.outerMeasure ((fun x => g * x) ⁻¹' A) = μ.outerMeasure A
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁵ : LinearOrderedCommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>P : RootPairing ι R M N<VAR>B : M →ₗ[R] M →ₗ[R] R<VAR>inst✝ : P.IsRootPositive B<VAR>i j : ι<GOAL>2 * (B (P.root i)) (P.root j) = P.pairing i j * (B (P.root j)) (P.root j)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁵ : LinearOrderedCommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>P : RootPairing ι R M N<VAR>B : M →ₗ[R] M →ₗ[R] R<VAR>inst✝ : P.IsRootPositive B<VAR>i j : ι<GOAL>(B (P.root i)) (P.root j) = P.pairing i j * (B (P.root j)) (P.root j) - (B (P.root i)) (P.root j)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁵ : LinearOrderedCommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>P : RootPairing ι R M N<VAR>B : M →ₗ[R] M →ₗ[R] R<VAR>inst✝ : P.IsRootPositive B<VAR>i j : ι<GOAL>(B ((P.reflection j) (P.root i))) ((P.reflection j) (P.root j)) = P.pairing i j * (B (P.root j)) (P.root j) - (B (P.root i)) (P.root j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s t✝ : Set α<VAR>inst✝ : Finite ι<VAR>t : ι → Set α<VAR>h : Pairwise (Disjoint on t)<VAR>ht : ∀ (i : ι), (t i).Finite<GOAL>∏ᶠ (a : α) (_ : a ∈ ⋃ i, t i), f a = ∏ᶠ (i : ι) (a : α) (_ : a ∈ t i), f a