ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>t : Type u → Type u<VAR>inst✝⁵ : Traversable t<VAR>inst✝⁴ : LawfulTraversable t<VAR>F G : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : LawfulApplicative F<VAR>inst✝¹ : Applicative G<VAR>inst✝ : LawfulApplicative G<VAR>α β γ : Type u<VAR>g : α → F β<VAR>h : β → G γ<VAR>f : β → γ<VAR>x✝ : t β<VAR>x : t α<GOAL>map f <$> traverse g x = traverse (map f ∘ g) x
<VAR>t : Type u → Type u<VAR>inst✝⁵ : Traversable t<VAR>inst✝⁴ : LawfulTraversable t<VAR>F G : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : LawfulApplicative F<VAR>inst✝¹ : Applicative G<VAR>inst✝ : LawfulApplicative G<VAR>α β γ : Type u<VAR>g : α → F β<VAR>h : β → G γ<VAR>f : β → γ<VAR>x✝ : t β<VAR>x : t α<GOAL>traverse (pure ∘ f) <$> traverse g x = traverse (map f ∘ g) x
<VAR>t : Type u → Type u<VAR>inst✝⁵ : Traversable t<VAR>inst✝⁴ : LawfulTraversable t<VAR>F G : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : LawfulApplicative F<VAR>inst✝¹ : Applicative G<VAR>inst✝ : LawfulApplicative G<VAR>α β γ : Type u<VAR>g : α → F β<VAR>h : β → G γ<VAR>f : β → γ<VAR>x✝ : t β<VAR>x : t α<GOAL>traverse (Comp.mk ∘ map (pure ∘ f) ∘ g) x = traverse (map f ∘ g) x
<VAR>t : Type u → Type u<VAR>inst✝⁵ : Traversable t<VAR>inst✝⁴ : LawfulTraversable t<VAR>F G : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : LawfulApplicative F<VAR>inst✝¹ : Applicative G<VAR>inst✝ : LawfulApplicative G<VAR>α β γ : Type u<VAR>g : α → F β<VAR>h : β → G γ<VAR>f : β → γ<VAR>x✝ : t β<VAR>x : t α<GOAL>Comp.instApplicativeComp = inst✝³
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a b : ℤ<GOAL>Finite a b ↔ Finite a.natAbs b.natAbs
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>⌊a⌋₊ = n ↔ ↑n ≤ a ∧ a < ↑n + 1
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>a b c : α<GOAL>Disjoint a (b ⊔ c) ↔ Disjoint a b ∧ Disjoint a c
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>K : Type u_1<VAR>inst✝ : DivisionRing K<VAR>p : K[X]<VAR>hp0 : ¬p = 0<GOAL>Irreducible (p * C p.leadingCoeff⁻¹) ↔ Irreducible p
<VAR>n : ℕ<VAR>i j : Fin n.succ<VAR>h : j < i<GOAL>↑(i.cycleRange j) = ↑j + 1
<VAR>α✝ : Type u_1<VAR>p : α✝ → Prop<VAR>l : RBNode α✝<VAR>v : α✝<VAR>r : RBNode α✝<VAR>hl : All p l<VAR>hv : p v<VAR>hr : All p r<VAR>l✝ : RBNode α✝<VAR>x✝ : ∀ (a : RBNode α✝) (x : α✝) (b : RBNode α✝), ¬l = node red a x b<GOAL>All p (match r with | node black a y b => l.balance2 v (node red a y b) | node red (node black a y b) z c => node red (node black l v a) y (b.balance2 z c.setRed) | r => node red l v r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : SuccOrder α<VAR>a b : α<VAR>ha : ¬IsMax a<VAR>hb : ¬IsMax b<GOAL>succ a = succ b ↔ a = b
<VAR>n : ℕ<VAR>p : Fin (n + 1)<VAR>e : Perm (Fin n)<GOAL>sign (decomposeFin.symm (p, e)) = (if p = 0 then 1 else -1) * sign e
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : CompleteLinearOrder R<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : OrderTopology R<VAR>x : R<VAR>as : ι → R<VAR>x_lt : ∀ (i : ι), x < as i<VAR>F : Filter ι<VAR>inst✝ : F.NeBot<VAR>as_lim : Tendsto as F (𝓝 x)<GOAL>⋃ i, Ici (as i) = Ioi x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : CompleteLinearOrder R<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : OrderTopology R<VAR>x : R<VAR>as : ι → R<VAR>x_lt : ∀ (i : ι), x < as i<VAR>F : Filter ι<VAR>inst✝ : F.NeBot<VAR>as_lim : Tendsto as F (𝓝 x)<VAR>obs : x ∉ range as<GOAL>⋃ i, Ici (as i) = Ioi x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : CompleteLinearOrder R<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : OrderTopology R<VAR>x : R<VAR>as : ι → R<VAR>x_lt : ∀ (i : ι), x < as i<VAR>F : Filter ι<VAR>inst✝ : F.NeBot<VAR>as_lim : Tendsto as F (𝓝 x)<VAR>obs : x ∉ range as<VAR>this : ⨅ i, as i = x<GOAL>⋃ i, Ici (as i) = Ioi x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : CompleteLinearOrder R<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : OrderTopology R<VAR>x : R<VAR>as : ι → R<VAR>x_lt : ∀ (i : ι), x < as i<VAR>F : Filter ι<VAR>inst✝ : F.NeBot<VAR>as_lim : Tendsto as F (𝓝 x)<VAR>obs : ⨅ i, as i ∉ range as<VAR>this : ⨅ i, as i = x<GOAL>⋃ i, Ici (as i) = Ioi (⨅ i, as i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<GOAL>a ≠ 0 → b ≠ 0 → a * b ≠ 0
<VAR>S✝ : Type u<VAR>inst✝¹ : Semiring S✝<VAR>S : Type u_1<VAR>inst✝ : Semiring S<VAR>n : ℕ<VAR>k : S<GOAL>eval k (ascPochhammer S (n + 1)) = eval k (ascPochhammer S n) * (k + ↑n)
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 ≤ x<VAR>h : y - 1 ≠ 0<GOAL>x ^ (y - 1) = x ^ y / x
<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 : Y → Z<VAR>x : Y<VAR>h : x ∈ e.target<GOAL>ContinuousAt f x ↔ ContinuousAt (f ∘ ↑e) (↑e.symm x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<GOAL>2 < card α ↔ ∃ a b c, a ≠ b ∧ a ≠ c ∧ b ≠ c
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>s t u v : Set α<VAR>h : AEDisjoint μ s t<VAR>x : α<VAR>hx : x ∈ s \ toMeasurable μ (s ∩ t)<GOAL>x ∈ ?m.11803 ∧ x ∉ t
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>h : N ≤ N'<VAR>x y : ↥↑N<GOAL>(inclusion h) x = (inclusion h) y → x = y
<VAR>R : Type u<VAR>inst✝³ : NonUnitalSemiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>x : R<GOAL>star x < 0 ↔ x < 0
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_2<VAR>𝔸 : Type u_3<VAR>inst✝³ : NormedField 𝕜'<VAR>inst✝² : NormedRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕜 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝔸<VAR>c✝ d : 𝕜 → 𝔸<VAR>c' d' : 𝔸<VAR>u v : 𝕜 → 𝕜'<VAR>c : 𝕜<GOAL>HasDerivAt (fun x => x * c) c x
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → F'<VAR>s : Set α<VAR>hf : ¬Integrable f μ<VAR>hm : m ≤ m0<VAR>hμm this : SigmaFinite (μ.trim hm)<GOAL>μ[f|m] = 0
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>A B : Matrix (n ⊕ o) (l ⊕ m) α<VAR>x✝ : A.toBlocks₁₁ = B.toBlocks₁₁ ∧ A.toBlocks₁₂ = B.toBlocks₁₂ ∧ A.toBlocks₂₁ = B.toBlocks₂₁ ∧ A.toBlocks₂₂ = B.toBlocks₂₂<VAR>h₁₁ : A.toBlocks₁₁ = B.toBlocks₁₁<VAR>h₁₂ : A.toBlocks₁₂ = B.toBlocks₁₂<VAR>h₂₁ : A.toBlocks₂₁ = B.toBlocks₂₁<VAR>h₂₂ : A.toBlocks₂₂ = B.toBlocks₂₂<GOAL>A = B
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ : MeasurableSpace α<VAR>L : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝⁵ : AddCommMonoid L<VAR>inst✝⁴ : TopologicalSpace L<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : TopologicalSpace N<VAR>m n : MeasurableSpace α<VAR>v : VectorMeasure α M<VAR>hle : m ≤ n<GOAL>(if MeasurableSet ∅ then ↑v ∅ else 0) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ : MeasurableSpace α<VAR>L : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝⁵ : AddCommMonoid L<VAR>inst✝⁴ : TopologicalSpace L<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : TopologicalSpace N<VAR>m n : MeasurableSpace α<VAR>v : VectorMeasure α M<VAR>hle : m ≤ n<VAR>i : Set α<VAR>hi : ¬MeasurableSet i<GOAL>(if MeasurableSet i then ↑v i else 0) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ : MeasurableSpace α<VAR>L : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝⁵ : AddCommMonoid L<VAR>inst✝⁴ : TopologicalSpace L<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : TopologicalSpace N<VAR>m n : MeasurableSpace α<VAR>v : VectorMeasure α M<VAR>hle : m ≤ n<VAR>f : ℕ → Set α<VAR>hf₁ : ∀ (i : ℕ), MeasurableSet (f i)<VAR>hf₂ : Pairwise (Disjoint on f)<VAR>hf₁' : ∀ (k : ℕ), MeasurableSet (f k)<GOAL>HasSum (fun i => if MeasurableSet (f i) then ↑v (f i) else 0) (if MeasurableSet (⋃ i, f i) then ↑v (⋃ i, f i) else 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ : MeasurableSpace α<VAR>L : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝⁵ : AddCommMonoid L<VAR>inst✝⁴ : TopologicalSpace L<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : TopologicalSpace N<VAR>m n : MeasurableSpace α<VAR>v : VectorMeasure α M<VAR>hle : m ≤ n<VAR>f : ℕ → Set α<VAR>hf₁ : ∀ (i : ℕ), MeasurableSet (f i)<VAR>hf₂ : Pairwise (Disjoint on f)<VAR>hf₁' : ∀ (k : ℕ), MeasurableSet (f k)<GOAL>(fun i => if MeasurableSet (f i) then ↑v (f i) else 0) = fun i => ↑v (f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ : MeasurableSpace α<VAR>L : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝⁵ : AddCommMonoid L<VAR>inst✝⁴ : TopologicalSpace L<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : TopologicalSpace N<VAR>m n : MeasurableSpace α<VAR>v : VectorMeasure α M<VAR>hle : m ≤ n<VAR>f : ℕ → Set α<VAR>hf₁ : ∀ (i : ℕ), MeasurableSet (f i)<VAR>hf₂ : Pairwise (Disjoint on f)<VAR>hf₁' : ∀ (k : ℕ), MeasurableSet (f k)<GOAL>(if MeasurableSet (⋃ i, f i) then ↑v (⋃ i, f i) else 0) = ↑v (⋃ i, f i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>κ : Type u_3<VAR>κ' : Type u_4<VAR>R : Type u_5<VAR>M : Type u_6<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>R₂ : Type u_7<VAR>M₂ : Type u_8<VAR>inst✝³ : CommRing R₂<VAR>inst✝² : AddCommGroup M₂<VAR>inst✝¹ : Module R₂ M₂<VAR>e : Basis ι R M<VAR>v : ι' → M<VAR>i : ι<VAR>j : ι'<VAR>inst✝ : DecidableEq ι'<VAR>x : M<VAR>i' : ι<VAR>k : ι'<GOAL>e.toMatrix (update v j x) i' k = (e.toMatrix v).updateColumn j (⇑(e.repr x)) i' k
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>κ : Type u_3<VAR>κ' : Type u_4<VAR>R : Type u_5<VAR>M : Type u_6<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>R₂ : Type u_7<VAR>M₂ : Type u_8<VAR>inst✝³ : CommRing R₂<VAR>inst✝² : AddCommGroup M₂<VAR>inst✝¹ : Module R₂ M₂<VAR>e : Basis ι R M<VAR>v : ι' → M<VAR>i : ι<VAR>j : ι'<VAR>inst✝ : DecidableEq ι'<VAR>x : M<VAR>i' : ι<VAR>k : ι'<GOAL>(e.repr (update v j x k)) i' = if k = j then (e.repr x) i' else (e.repr (v k)) i'
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y✝ : M<VAR>f : E →ₗ.[R] F<VAR>x y : E<VAR>x' y' : F<VAR>hx : (x, x') ∈ f.graph<VAR>hy : (y, y') ∈ f.graph<VAR>hxy : x = y<GOAL>x' = y'
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y✝ : M<VAR>f : E →ₗ.[R] F<VAR>x y : E<VAR>x' y' : F<VAR>hx : ∃ y, ↑y = (x, x').1 ∧ ↑f y = (x, x').2<VAR>hy : ∃ y_1, ↑y_1 = (y, y').1 ∧ ↑f y_1 = (y, y').2<VAR>hxy : x = y<GOAL>x' = y'
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y✝ : M<VAR>f : E →ₗ.[R] F<VAR>x y : E<VAR>x' y' : F<VAR>hxy : x = y<VAR>x'' : ↥f.domain<VAR>hx1 : ↑x'' = x<VAR>hx2 : ↑f x'' = x'<VAR>y'' : ↥f.domain<VAR>hy1 : ↑y'' = y<VAR>hy2 : ↑f y'' = y'<GOAL>x' = y'
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y✝ : M<VAR>f : E →ₗ.[R] F<VAR>x y : E<VAR>x' y' : F<VAR>x'' : ↥f.domain<VAR>hx1 : ↑x'' = x<VAR>hx2 : ↑f x'' = x'<VAR>y'' : ↥f.domain<VAR>hxy : x'' = y''<VAR>hy1 : ↑y'' = y<VAR>hy2 : ↑f y'' = y'<GOAL>x' = y'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝¹ : Ring α<VAR>inst✝ : Ring β<VAR>h : Antiperiodic f c<VAR>n : ℕ<GOAL>f (↑n * c - x) = (-1) ^ n * f (-x)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>I✝ I' : Ideal R<VAR>J J' : Ideal S<VAR>I : Ideal (R × S)<GOAL>I = (map (RingHom.fst R S) I).prod (map (RingHom.snd R S) I)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>I✝ I' : Ideal R<VAR>J J' : Ideal S<VAR>I : Ideal (R × S)<GOAL>∀ (x : R × S), x ∈ I ↔ x ∈ (map (RingHom.fst R S) I).prod (map (RingHom.snd R S) I)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>I✝ I' : Ideal R<VAR>J J' : Ideal S<VAR>I : Ideal (R × S)<VAR>r : R<VAR>s : S<GOAL>(r, s) ∈ I ↔ (r, s) ∈ (map (RingHom.fst R S) I).prod (map (RingHom.snd R S) I)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>I✝ I' : Ideal R<VAR>J J' : Ideal S<VAR>I : Ideal (R × S)<VAR>r : R<VAR>s : S<GOAL>(r, s) ∈ I ↔ (∃ x ∈ I, (RingHom.fst R S) x = r) ∧ ∃ x ∈ I, (RingHom.snd R S) x = s
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>I✝ I' : Ideal R<VAR>J J' : Ideal S<VAR>I : Ideal (R × S)<VAR>r : R<VAR>s' : S<VAR>h₁ : (r, s') ∈ I<VAR>r' : R<VAR>s : S<VAR>h₂ : (r', s) ∈ I<GOAL>((RingHom.fst R S) (r, s'), (RingHom.snd R S) (r', s)) ∈ I
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : Zero α<VAR>inst✝ : LocallyFiniteOrder α<VAR>f g : ι →₀ α<GOAL>(Ico f g).card = ∏ i ∈ f.support ∪ g.support, (Icc (f i) (g i)).card - 1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>M N : ModuleCat R<GOAL>(associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom = tensorHom (rightUnitor M).hom (𝟙 N)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>M N : ModuleCat R<GOAL>∀ (x : ↑M) (y : ↑(of R R)) (z : ↑N), ((associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) = (tensorHom (rightUnitor M).hom (𝟙 N)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>M N : ModuleCat R<VAR>x : ↑M<VAR>z : ↑N<VAR>y : R<GOAL>x ⊗ₜ[R] (leftUnitor N).hom (y ⊗ₜ[R] z) = (rightUnitor M).hom (x ⊗ₜ[R] y) ⊗ₜ[R] z
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>M N : ModuleCat R<VAR>x : ↑M<VAR>z : ↑N<VAR>y : R<GOAL>x ⊗ₜ[R] (y • z) = (y • x) ⊗ₜ[R] z
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>x y z : S<GOAL>(z𝖣x * y) = ((z * x)𝖣y) + (z * y)𝖣x
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>x y z : S<GOAL>single y (z * x) + single x (z * y) - single (x * y) z ∈ kerTotal R S
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>x y z : S<GOAL>z • (single y x + single x y - single (x * y) 1) ∈ kerTotal R S
<VAR>R : Type u_1<VAR>inst✝² : LinearOrderedField R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x y v₁ v₂ : M<VAR>h : SameRay R x y<VAR>hx : x ≠ 0<GOAL>∃ r, 0 ≤ r ∧ r • x = y
<VAR>R : Type u_1<VAR>inst✝² : LinearOrderedField R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x v₁ v₂ : M<VAR>hx : x ≠ 0<VAR>h : SameRay R x 0<GOAL>∃ r, 0 ≤ r ∧ r • x = 0
<VAR>R : Type u_1<VAR>inst✝² : LinearOrderedField R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x y v₁ v₂ : M<VAR>h : SameRay R x y<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>∃ r, 0 ≤ r ∧ r • x = y
<VAR>R✝ : Type u_1<VAR>M : Type u_2<VAR>inst✝⁵ : Semiring R✝<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R✝ M<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>I : (Submodule R A)ˣ<GOAL>(↑I).FG
<VAR>R✝ : Type u_1<VAR>M : Type u_2<VAR>inst✝⁵ : Semiring R✝<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R✝ M<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>I : (Submodule R A)ˣ<VAR>this : 1 ∈ ↑I * ↑I⁻¹<GOAL>(↑I).FG
<VAR>R✝ : Type u_1<VAR>M : Type u_2<VAR>inst✝⁵ : Semiring R✝<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R✝ M<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>I : (Submodule R A)ˣ<VAR>this : 1 ∈ ↑I * ↑I⁻¹<VAR>T T' : Finset A<VAR>hT : ↑T ⊆ ↑↑I<VAR>hT' : ↑T' ⊆ ↑↑I⁻¹<VAR>one_mem : 1 ∈ span R (↑T * ↑T')<GOAL>(↑I).FG
<VAR>R✝ : Type u_1<VAR>M : Type u_2<VAR>inst✝⁵ : Semiring R✝<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R✝ M<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>I : (Submodule R A)ˣ<VAR>this : 1 ∈ ↑I * ↑I⁻¹<VAR>T T' : Finset A<VAR>hT : ↑T ⊆ ↑↑I<VAR>hT' : ↑T' ⊆ ↑↑I⁻¹<VAR>one_mem : 1 ∈ span R (↑T * ↑T')<GOAL>↑I ≤ span R ↑T
<VAR>R✝ : Type u_1<VAR>M : Type u_2<VAR>inst✝⁵ : Semiring R✝<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R✝ M<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>I : (Submodule R A)ˣ<VAR>this : 1 ∈ ↑I * ↑I⁻¹<VAR>T T' : Finset A<VAR>hT : ↑T ⊆ ↑↑I<VAR>hT' : ↑T' ⊆ ↑↑I⁻¹<VAR>one_mem : 1 ∈ span R (↑T * ↑T')<GOAL>↑(1 * I) ≤ span R ↑T * 1
<VAR>R✝ : Type u_1<VAR>M : Type u_2<VAR>inst✝⁵ : Semiring R✝<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R✝ M<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>I : (Submodule R A)ˣ<VAR>this : 1 ∈ ↑I * ↑I⁻¹<VAR>T T' : Finset A<VAR>hT : ↑T ⊆ ↑↑I<VAR>hT' : ↑T' ⊆ ↑↑I⁻¹<VAR>one_mem : 1 ∈ span R (↑T * ↑T')<GOAL>↑(1 * I) ≤ span R ↑T * ↑I⁻¹ * ↑I
<VAR>R✝ : Type u_1<VAR>M : Type u_2<VAR>inst✝⁵ : Semiring R✝<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R✝ M<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>I : (Submodule R A)ˣ<VAR>this : 1 ∈ ↑I * ↑I⁻¹<VAR>T T' : Finset A<VAR>hT : ↑T ⊆ ↑↑I<VAR>hT' : ↑T' ⊆ ↑↑I⁻¹<VAR>one_mem : 1 ∈ span R (↑T * ↑T')<GOAL>↑1 ≤ span R ↑T * span R ↑T'
<VAR>R✝ : Type u_1<VAR>M : Type u_2<VAR>inst✝⁵ : Semiring R✝<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R✝ M<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>I : (Submodule R A)ˣ<VAR>this : 1 ∈ ↑I * ↑I⁻¹<VAR>T T' : Finset A<VAR>hT : ↑T ⊆ ↑↑I<VAR>hT' : ↑T' ⊆ ↑↑I⁻¹<VAR>one_mem : 1 ∈ span R (↑T * ↑T')<GOAL>1 ≤ span R (↑T * ↑T')
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>hf : LiftPropWithinAt (ContDiffWithinAtProp I I' n) f s x<VAR>le : m ≤ n<GOAL>LiftPropWithinAt (ContDiffWithinAtProp I I' m) f s x
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>F : Cᵒᵖ ⥤ Type v₁<VAR>t : F.obj X<GOAL>yonedaEquiv.symm (F.map f t) = yoneda.map f.unop ≫ yonedaEquiv.symm t
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>F : Cᵒᵖ ⥤ Type v₁<VAR>u : yoneda.obj (unop X) ⟶ F<GOAL>yonedaEquiv.symm (F.map f (yonedaEquiv u)) = yoneda.map f.unop ≫ yonedaEquiv.symm (yonedaEquiv u)
<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✝³ : Module.Free R M'<VAR>inst✝² : Module.Finite R M<VAR>inst✝¹ : Module.Finite R M'<VAR>ι : Type v<VAR>inst✝ : Fintype ι<GOAL>finrank R (ι →₀ R) = card ι
<VAR>a : ℝ<VAR>ha : a ∈ Icc 0 1<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>HasSum (fun n => 1 / (↑n + ↑a) ^ s) (hurwitzZeta (↑a) s)
<VAR>a : ℝ<VAR>ha : a ∈ Icc 0 1<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>(fun n => 1 / (↑n + ↑a) ^ s) = fun b => (1 / (↑b + ↑a) ^ s + 1 / (↑b + 1 - ↑a) ^ s) / 2 + (1 / (↑b + ↑a) ^ s - 1 / (↑b + 1 - ↑a) ^ s) / 2
<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✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : AddCommGroup N<VAR>f : M → N<VAR>x y : M<GOAL>polar (-f) x y = -polar f x y