ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹³ : NormedAddCommGroup D<VAR>inst✝¹² : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup X<VAR>inst✝⁴ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>E' : Type u_3<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>F' : Type u_4<VAR>inst✝¹ : NormedAddCommGroup F'<VAR>inst✝ : NormedSpace 𝕜 F'<VAR>f : E → F<VAR>g : E' → F'<VAR>x : E<VAR>y : E'<VAR>hf : ContDiffWithinAt 𝕜 n f univ x<VAR>hg : ContDiffWithinAt 𝕜 n g univ y<GOAL>ContDiffWithinAt 𝕜 n (Prod.map f g) univ (x, y)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹³ : NormedAddCommGroup D<VAR>inst✝¹² : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup X<VAR>inst✝⁴ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>E' : Type u_3<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>F' : Type u_4<VAR>inst✝¹ : NormedAddCommGroup F'<VAR>inst✝ : NormedSpace 𝕜 F'<VAR>f : E → F<VAR>g : E' → F'<VAR>x : E<VAR>y : E'<VAR>hf : ContDiffWithinAt 𝕜 n f univ x<VAR>hg : ContDiffWithinAt 𝕜 n g univ y<GOAL>univ = univ ×ˢ univ
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>x : E<GOAL>((p.derivSeries n) fun x_1 => x) x = (n + 1) • (p (n + 1)) fun x_1 => x
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>x : E<GOAL>∑ x_1 : { s // s.card = n }, ((p.changeOriginSeriesTerm 1 n ↑x_1 ⋯) fun x_2 => x) (Fin.snoc ![] x) = (n + 1) • (p (n + 1)) fun x_1 => x
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>x : E<VAR>x✝ : { s // s.card = n }<VAR>a✝ : x✝ ∈ Finset.univ<GOAL>((p.changeOriginSeriesTerm 1 n ↑x✝ ⋯) fun x_1 => x) (Fin.snoc ![] x) = (p (n + 1)) fun x_1 => x
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>x : E<GOAL>n + 1 = Finset.univ.card
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.60536, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>i : ℤ<VAR>A : C<VAR>f : A ⟶ (mappingCone φ).X i<VAR>j : ℤ<VAR>hij : i + 1 = j<GOAL>f = (f ≫ (↑(fst φ)).v i j hij) ≫ (inl φ).v j i ⋯ + (f ≫ (snd φ).v i i ⋯) ≫ (inr φ).f i
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → E<VAR>z : ℂ<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>x : ℝ<GOAL>0 < ε + sSupNormIm f x
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>p : PosNum<GOAL>↑(pos p).bit0 = ↑(pos p) + ↑(pos p)
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>p : PosNum<GOAL>↑p.bit0 = ↑p + ↑p
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>p : PosNum<GOAL>↑(neg p).bit0 = ↑(neg p) + ↑(neg p)
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>a b : α<GOAL>Pairwise (Disjoint on fun n => Ioo (b ^ n) (b ^ (n + 1)))
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X✝ Y✝ Z✝ : C<VAR>f✝ g✝ : X✝ ⟶ Y✝<VAR>h : Y✝ ⟶ Z✝<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝¹ : IsIso g<VAR>inst✝ : IsIso (f ≫ g)<GOAL>IsIso f
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X✝ Y✝ Z✝ : C<VAR>f✝ g✝ : X✝ ⟶ Y✝<VAR>h : Y✝ ⟶ Z✝<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝¹ : IsIso g<VAR>inst✝ : IsIso (f ≫ g)<GOAL>IsIso ((f ≫ g) ≫ inv g)
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝³ : TopologicalSpace H<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : LocallyConnectedSpace H<VAR>e : M → PartialHomeomorph M H := chartAt H<GOAL>LocallyConnectedSpace M
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝³ : TopologicalSpace H<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : LocallyConnectedSpace H<VAR>e : M → PartialHomeomorph M H := chartAt H<GOAL>∀ (x : M), (𝓝 x).HasBasis ((fun x s => (IsOpen s ∧ ↑(e x) x ∈ s ∧ IsConnected s) ∧ s ⊆ (e x).target) x) ((fun x s => ↑(e x).symm '' s) x)
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝³ : TopologicalSpace H<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : LocallyConnectedSpace H<VAR>e : M → PartialHomeomorph M H := chartAt H<GOAL>∀ (x : M) (i : Set H), (fun x s => (IsOpen s ∧ ↑(e x) x ∈ s ∧ IsConnected s) ∧ s ⊆ (e x).target) x i → IsPreconnected ((fun x s => ↑(e x).symm '' s) x i)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<GOAL>LiftRel R nil nil
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<GOAL>Computation.LiftRel (LiftRelO R (LiftRel R)) nil.destruct nil.destruct
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>p : Submodule R (CliffordAlgebra Q)<VAR>n : ℕ<GOAL>Submodule.map reverse (p ^ n) = Submodule.map reverse p ^ n
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K L : HomologicalComplex₂ C (up ℤ) (up ℤ)<VAR>f : K ⟶ L<VAR>x y : ℤ<VAR>inst✝ : K.HasTotal (up ℤ)<VAR>n n₁ n₂ : ℤ<VAR>h : n₁ + n₂ = n<GOAL>((shiftFunctor₁ C x).obj ((shiftFunctor₂ C y).obj K)).ιTotal (up ℤ) n₁ n₂ n h ≫ (((shiftFunctor₂ C y).obj K).totalShift₁Iso x).hom.f n ≫ (K.totalShift₂Iso y).hom.f (n + x) = ((shiftFunctor₁ C x).obj ((shiftFunctor₂ C y).obj K)).ιTotal (up ℤ) n₁ n₂ n h ≫ ((x * y).negOnePow • (total.map ((shiftFunctor₁₂CommIso C x y).hom.app K) (up ℤ)).f n ≫ (((shiftFunctor₁ C x).obj K).totalShift₂Iso y).hom.f n ≫ (K.totalShift₁Iso x).hom.f (n + y) ≫ ((shiftFunctorComm (CochainComplex C ℤ) x y).hom.app (K.total (up ℤ))).f n)
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K L : HomologicalComplex₂ C (up ℤ) (up ℤ)<VAR>f : K ⟶ L<VAR>x y : ℤ<VAR>inst✝ : K.HasTotal (up ℤ)<VAR>n n₁ n₂ : ℤ<VAR>h : n₁ + n₂ = n<GOAL>(((shiftFunctor₂ C y).obj K).shiftFunctor₁XXIso n₁ x (n₁ + x) ⋯ n₂).hom ≫ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) (n₁ + x) n₂ (n + x) ⋯ ≫ (CochainComplex.shiftFunctorObjXIso (((shiftFunctor₂ C y).obj K).total (up ℤ)) x n (n + x) ⋯).inv ≫ (K.totalShift₂Iso y).hom.f (n + x) = (x * y).negOnePow • (n₁ * y).negOnePow • (((shiftFunctor₁₂CommIso C x y).hom.app K).f n₁).f n₂ ≫ ((((shiftFunctor₁ C x).obj K).shiftFunctor₂XXIso n₁ n₂ y (n₂ + y) ⋯).hom ≫ ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) n₁ (n₂ + y) (n + y) ⋯ ≫ (CochainComplex.shiftFunctorObjXIso (((shiftFunctor₁ C x).obj K).total (up ℤ)) y n (n + y) ⋯).inv) ≫ (K.totalShift₁Iso x).hom.f (n + y) ≫ ((shiftFunctorComm (CochainComplex C ℤ) x y).hom.app (K.total (up ℤ))).f n
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K L : HomologicalComplex₂ C (up ℤ) (up ℤ)<VAR>f : K ⟶ L<VAR>x y : ℤ<VAR>inst✝ : K.HasTotal (up ℤ)<VAR>n n₁ n₂ : ℤ<VAR>h : n₁ + n₂ = n<GOAL>𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) (n₁ + x) n₂ (n + x) ⋯ ≫ 𝟙 ((((shiftFunctor₂ C y).obj K).total (up ℤ)).X (n + x)) ≫ (K.totalShift₂Iso y).hom.f (n + x) = (x * y).negOnePow • (n₁ * y).negOnePow • 𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫ (𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫ ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) n₁ (n₂ + y) (n + y) ⋯ ≫ 𝟙 ((((shiftFunctor₁ C x).obj K).total (up ℤ)).X (n + y))) ≫ (K.totalShift₁Iso x).hom.f (n + y) ≫ ((shiftFunctorComm (CochainComplex C ℤ) x y).hom.app (K.total (up ℤ))).f n
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K L : HomologicalComplex₂ C (up ℤ) (up ℤ)<VAR>f : K ⟶ L<VAR>x y : ℤ<VAR>inst✝ : K.HasTotal (up ℤ)<VAR>n n₁ n₂ : ℤ<VAR>h : n₁ + n₂ = n<GOAL>(n₁ * y + x * y).negOnePow • (K.shiftFunctor₂XXIso (n₁ + x) n₂ y (n₂ + y) ⋯).hom ≫ K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯ ≫ (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y (n + x) (n + x + y) ⋯).inv = (n₁ * y + x * y).negOnePow • ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) n₁ (n₂ + y) (n + y) ⋯ ≫ (K.totalShift₁Iso x).hom.f (n + y) ≫ ((shiftFunctorComm (CochainComplex C ℤ) x y).hom.app (K.total (up ℤ))).f n
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K L : HomologicalComplex₂ C (up ℤ) (up ℤ)<VAR>f : K ⟶ L<VAR>x y : ℤ<VAR>inst✝ : K.HasTotal (up ℤ)<VAR>n n₁ n₂ : ℤ<VAR>h : n₁ + n₂ = n<GOAL>(n₁ * y + x * y).negOnePow • 𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫ K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + x + y)) = (n₁ * y + x * y).negOnePow • ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) n₁ (n₂ + y) (n + y) ⋯ ≫ (K.totalShift₁Iso x).hom.f (n + y) ≫ ((shiftFunctorComm (CochainComplex C ℤ) x y).hom.app (K.total (up ℤ))).f n
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K L : HomologicalComplex₂ C (up ℤ) (up ℤ)<VAR>f : K ⟶ L<VAR>x y : ℤ<VAR>inst✝ : K.HasTotal (up ℤ)<VAR>n n₁ n₂ : ℤ<VAR>h : n₁ + n₂ = n<GOAL>(n₁ * y + x * y).negOnePow • K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯ = (n₁ * y + x * y).negOnePow • (K.shiftFunctor₁XXIso n₁ x (n₁ + x) ⋯ (n₂ + y)).hom ≫ K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯ ≫ (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x (n + y) (n + x + y) ⋯).inv ≫ ((K.total (up ℤ)).XIsoOfEq ⋯).hom
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K L : HomologicalComplex₂ C (up ℤ) (up ℤ)<VAR>f : K ⟶ L<VAR>x y : ℤ<VAR>inst✝ : K.HasTotal (up ℤ)<VAR>n n₁ n₂ : ℤ<VAR>h : n₁ + n₂ = n<GOAL>(n₁ * y + x * y).negOnePow • K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯ = (n₁ * y + x * y).negOnePow • 𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫ K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯ ≫ ((K.total (up ℤ)).XIsoOfEq ⋯).inv ≫ ((K.total (up ℤ)).XIsoOfEq ⋯).hom
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>E : Type<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>a : ℝ<VAR>f : ℝ → ℂ<VAR>n : ℤ<GOAL>fourierCoeff (liftIoc T a f) n = fourierCoeffOn ⋯ f n
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>E : Type<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>a : ℝ<VAR>f : ℝ → ℂ<VAR>n : ℤ<GOAL>(1 / T) • ∫ (x : ℝ) in ?a..?a + T, (fourier (-n)) ↑x • liftIoc T a f ↑x = (1 / T) • ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • f x
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>E : Type<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>a : ℝ<VAR>f : ℝ → ℂ<VAR>n : ℤ<GOAL>ℝ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>b : Set (Set X)<VAR>hb : IsTopologicalBasis b<VAR>x y : X<VAR>h : x ≠ y<GOAL>∃ a ∈ b, x ∈ a ∧ y ∉ a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>b : Set (Set X)<VAR>hb : IsTopologicalBasis b<VAR>x y : X<VAR>h : x ≠ y<VAR>a : Set X<VAR>ab : a ∈ b<VAR>xa : x ∈ a<VAR>ha : a ⊆ {y_1 | y_1 ≠ y}<GOAL>∃ a ∈ b, x ∈ a ∧ y ∉ a
<VAR>α : Type u_1<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<GOAL>⋃ n, Icc a ↑n = Ici a \ {⊤}
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Field K<VAR>T : Type u_4<VAR>inst✝¹ : CommRing T<VAR>inst✝ : IsDedekindDomain T<VAR>I J : Ideal T<VAR>hI : I ≠ ⊥<VAR>hJ : Irreducible J<VAR>n : ℕ<VAR>hn : multiplicity J I ≤ ↑n<GOAL>J ^ n ⊔ I = J ^ (multiplicity J I).get ⋯
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Field K<VAR>T : Type u_4<VAR>inst✝¹ : CommRing T<VAR>inst✝ : IsDedekindDomain T<VAR>I J : Ideal T<VAR>hI : I ≠ ⊥<VAR>hJ : Irreducible J<VAR>n : ℕ<VAR>hn : multiplicity J I ≤ ↑n<GOAL>J ^ count J (normalizedFactors I) = J ^ (multiplicity J I).get ⋯
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Field K<VAR>T : Type u_4<VAR>inst✝¹ : CommRing T<VAR>inst✝ : IsDedekindDomain T<VAR>I J : Ideal T<VAR>hI : I ≠ ⊥<VAR>hJ : Irreducible J<VAR>n : ℕ<VAR>hn : multiplicity J I ≤ ↑n<GOAL>count J (normalizedFactors I) ≤ n
<VAR>p q : ℕ+ → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>h : ∃ n, p n<VAR>n m : ℕ+<GOAL>PNat.find h = 1 ↔ p 1
<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>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w : ι → k<VAR>p : ι → P<VAR>b : P<VAR>c : k<GOAL>(s.weightedVSubOfPoint p b) (c • w) = c • (s.weightedVSubOfPoint p b) w
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>𝔹 : Type u_3<VAR>inst✝⁵ : RCLike 𝕂<VAR>inst✝⁴ : NormedRing 𝔸<VAR>inst✝³ : NormedAlgebra 𝕂 𝔸<VAR>inst✝² : NormedRing 𝔹<VAR>inst✝¹ : NormedAlgebra 𝕂 𝔹<VAR>inst✝ : CompleteSpace 𝔸<GOAL>Continuous (exp 𝕂)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>𝔹 : Type u_3<VAR>inst✝⁵ : RCLike 𝕂<VAR>inst✝⁴ : NormedRing 𝔸<VAR>inst✝³ : NormedAlgebra 𝕂 𝔸<VAR>inst✝² : NormedRing 𝔹<VAR>inst✝¹ : NormedAlgebra 𝕂 𝔹<VAR>inst✝ : CompleteSpace 𝔸<GOAL>ContinuousOn (exp 𝕂) (EMetric.ball 0 (expSeries 𝕂 𝔸).radius)
<VAR>M : Type u<VAR>inst✝⁵ : Monoid M<VAR>G : Type u<VAR>inst✝⁴ : Group G<VAR>F : Type v<VAR>inst✝³ : Field F<VAR>inst✝² : MulSemiringAction M F<VAR>inst✝¹ : MulSemiringAction G F<VAR>m : M<VAR>inst✝ : Finite G<VAR>x : F<GOAL>IsIntegral (↥(subfield G F)) x
<VAR>M : Type u<VAR>inst✝⁵ : Monoid M<VAR>G : Type u<VAR>inst✝⁴ : Group G<VAR>F : Type v<VAR>inst✝³ : Field F<VAR>inst✝² : MulSemiringAction M F<VAR>inst✝¹ : MulSemiringAction G F<VAR>m : M<VAR>inst✝ : Finite G<VAR>x : F<VAR>val✝ : Fintype G<GOAL>IsIntegral (↥(subfield G F)) x
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>m1 : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ : Measure β<VAR>t : Set β<VAR>ht : MeasurableSet t<GOAL>(Measure.map f (Measure.comap f μ)) t = (μ.restrict (range f)) t
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>U : TopCat<VAR>X : PresheafedSpace C<VAR>f : U ⟶ ↑X<VAR>h : OpenEmbedding ⇑f<VAR>x : ↑U<GOAL>(X.restrictStalkIso h x).inv = Hom.stalkMap (X.ofRestrict h) x
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>U : TopCat<VAR>X : PresheafedSpace C<VAR>f : U ⟶ ↑X<VAR>h : OpenEmbedding ⇑f<VAR>x : ↑U<VAR>V : (OpenNhds (f x))ᵒᵖ<GOAL>colimit.ι (((whiskeringLeft (OpenNhds (f x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion (f x)).op).obj X.presheaf) V ≫ (X.restrictStalkIso h x).inv = colimit.ι (((whiskeringLeft (OpenNhds (f x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion (f x)).op).obj X.presheaf) V ≫ Hom.stalkMap (X.ofRestrict h) x
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>U : TopCat<VAR>X : PresheafedSpace C<VAR>f : U ⟶ ↑X<VAR>h : OpenEmbedding ⇑f<VAR>x : ↑U<VAR>V : OpenNhds (f x)<GOAL>colimit.ι (((whiskeringLeft (OpenNhds (f x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion (f x)).op).obj X.presheaf) (op V) ≫ (X.restrictStalkIso h x).inv = colimit.ι (((whiskeringLeft (OpenNhds (f x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion (f x)).op).obj X.presheaf) (op V) ≫ Hom.stalkMap (X.ofRestrict h) x
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>U : TopCat<VAR>X : PresheafedSpace C<VAR>f : U ⟶ ↑X<VAR>h : OpenEmbedding ⇑f<VAR>x : ↑U<VAR>V : OpenNhds (f x)<VAR>i : (⋯.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V := homOfLE ⋯<GOAL>colimit.ι (((whiskeringLeft (OpenNhds (f x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion (f x)).op).obj X.presheaf) (op V) ≫ (X.restrictStalkIso h x).inv = colimit.ι (((whiskeringLeft (OpenNhds (f x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion (f x)).op).obj X.presheaf) (op V) ≫ Hom.stalkMap (X.ofRestrict h) x
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>U : TopCat<VAR>X : PresheafedSpace C<VAR>f : U ⟶ ↑X<VAR>h : OpenEmbedding ⇑f<VAR>x : ↑U<VAR>V : OpenNhds (f x)<VAR>i : (⋯.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V := homOfLE ⋯<GOAL>colimit.ι (((whiskeringLeft (OpenNhds (f x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion (f x)).op).obj X.presheaf) (op V) = ((((whiskeringLeft (OpenNhds ((X.ofRestrict h).base x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion ((X.ofRestrict h).base x)).op).map (X.ofRestrict h).c).app (op V) ≫ (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso (X.ofRestrict h).base x).inv) (X.restrict h).presheaf).app (op V) ≫ colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑↑(X.restrict h))ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj (X.restrict h).presheaf) ((OpenNhds.map (X.ofRestrict h).base x).op.obj (op V))) ≫ (X.restrictStalkIso h x).hom
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>U : TopCat<VAR>X : PresheafedSpace C<VAR>f : U ⟶ ↑X<VAR>h : OpenEmbedding ⇑f<VAR>x : ↑U<VAR>V : OpenNhds (f x)<VAR>i : (⋯.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V := homOfLE ⋯<GOAL>colimit.ι (((whiskeringLeft (OpenNhds (f x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion (f x)).op).obj X.presheaf) (op V) = (((whiskeringLeft (OpenNhds ((X.ofRestrict h).base x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion ((X.ofRestrict h).base x)).op).map (X.ofRestrict h).c).app (op V) ≫ (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso (X.ofRestrict h).base x).inv) (X.restrict h).presheaf).app (op V) ≫ colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑↑(X.restrict h))ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj (X.restrict h).presheaf) ((OpenNhds.map (X.ofRestrict h).base x).op.obj (op V)) ≫ (X.restrictStalkIso h x).hom
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>U : TopCat<VAR>X : PresheafedSpace C<VAR>f : U ⟶ ↑X<VAR>h : OpenEmbedding ⇑f<VAR>x : ↑U<VAR>V : OpenNhds (f x)<VAR>i : (⋯.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V := homOfLE ⋯<GOAL>colimit.ι (((whiskeringLeft (OpenNhds (f x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion (f x)).op).obj X.presheaf) (op V) = (((whiskeringLeft (OpenNhds ((X.ofRestrict h).base x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion ((X.ofRestrict h).base x)).op).map (X.ofRestrict h).c).app (op V) ≫ (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso (X.ofRestrict h).base x).inv) (X.restrict h).presheaf).app (op V) ≫ colimit.ι ((OpenNhds.inclusion (f x)).op ⋙ X.presheaf) ((⋯.functorNhds x).op.obj ((OpenNhds.map (X.ofRestrict h).base x).op.obj (op V)))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>U : TopCat<VAR>X : PresheafedSpace C<VAR>f : U ⟶ ↑X<VAR>h : OpenEmbedding ⇑f<VAR>x : ↑U<VAR>V : OpenNhds (f x)<VAR>i : (⋯.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V := homOfLE ⋯<GOAL>colimit.ι (((whiskeringLeft (OpenNhds (f x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion (f x)).op).obj X.presheaf) (op V) = X.presheaf.map ((⋯.adjunction.counit.app (unop ((OpenNhds.inclusion ((X.ofRestrict h).base x)).op.obj (op V)))).op ≫ ⋯.functor.op.map ((NatTrans.op (OpenNhds.inclusionMapIso (X.ofRestrict h).base x).inv).app (op V))) ≫ colimit.ι ((OpenNhds.inclusion (f x)).op ⋙ X.presheaf) ((⋯.functorNhds x).op.obj ((OpenNhds.map (X.ofRestrict h).base x).op.obj (op V)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : DistribLattice α<VAR>inst✝² : BoundedOrder α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a : α<VAR>ha : a ∉ upperClosure ↑s ⊔ upperClosure ↑t<GOAL>a ∉ upperClosure ↑(s ⊻ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>inst✝ : DecidableEq β<VAR>H : (image f s).card = s.card<GOAL>Set.InjOn f ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>inst✝ : DecidableEq β<VAR>H : Multiset.card { val := (Multiset.map f s.val).dedup, nodup := ⋯ }.val = Multiset.card s.val<GOAL>Set.InjOn f ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>inst✝ : DecidableEq β<VAR>H : Multiset.card (Multiset.map f s.val).dedup = Multiset.card s.val<GOAL>Set.InjOn f ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>inst✝ : DecidableEq β<VAR>H : Multiset.card (Multiset.map f s.val).dedup = Multiset.card s.val<VAR>this : (Multiset.map f s.val).dedup = Multiset.map f s.val<GOAL>Set.InjOn f ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>inst✝ : DecidableEq β<VAR>H : Multiset.card (Multiset.map f s.val).dedup = Multiset.card s.val<VAR>this : (Multiset.map f s.val).Nodup<GOAL>Set.InjOn f ↑s
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Fintype σ<VAR>inst✝² : Fintype τ<VAR>n : ℕ<VAR>inst✝¹ : DecidableEq σ<VAR>inst✝ : Nontrivial R<GOAL>(esymm σ R n).support = image (fun t => ∑ i ∈ t, Finsupp.single i 1) (powersetCard n univ)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Fintype σ<VAR>inst✝² : Fintype τ<VAR>n : ℕ<VAR>inst✝¹ : DecidableEq σ<VAR>inst✝ : Nontrivial R<GOAL>((powersetCard n univ).biUnion fun t => {∑ i ∈ t, Finsupp.single i 1}) = image (fun t => ∑ i ∈ t, Finsupp.single i 1) (powersetCard n univ)
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>ha : a ≠ 0<VAR>ha' : a ≠ ⊤<VAR>hb : b ≠ 0<VAR>hb' : b ≠ ⊤<GOAL>c / b = d / a ↔ a * c = b * d
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>ha : a ≠ 0<VAR>ha' : a ≠ ⊤<VAR>hb : b ≠ 0<VAR>hb' : b ≠ ⊤<GOAL>a * (c / b) = d ↔ a * c = b * d
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>ha : a ≠ 0<VAR>ha' : a ≠ ⊤<VAR>hb : b ≠ 0<VAR>hb' : b ≠ ⊤<GOAL>a * (c / b) = d ↔ b * d = a * c
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>l : List α<VAR>ih : indexOf a l ≤ l.length<GOAL>indexOf a (b :: l) ≤ (b :: l).length
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>l : List α<VAR>ih : indexOf a l ≤ l.length<GOAL>(if b = a then 0 else indexOf a l + 1) ≤ l.length + 1
<VAR>R : Type u<VAR>a✝ b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q p : R[X]<VAR>n : ℕ<VAR>a : R<VAR>ha : a ≠ 0<GOAL>(p.update n a).support = insert n p.support
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>H : ¬1 = 0<GOAL>X.support = {1}
<VAR>A : Type u_1<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra ℝ A<VAR>a b : ℝ<VAR>a' b' : A<VAR>u v u' v' : ℝ → A<VAR>inst✝ : CompleteSpace A<VAR>hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x<VAR>hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x<VAR>huv' : IntegrableOn (u * v') (Ioi a) volume<VAR>hu'v : IntegrableOn (u' * v) (Ioi a) volume<VAR>h_zero : Tendsto (u * v) (𝓝[>] a) (𝓝 a')<VAR>h_infty : Tendsto (u * v) atTop (𝓝 b')<GOAL>∫ (x : ℝ) in Ioi a, u x * v' x = b' - a' - ∫ (x : ℝ) in Ioi a, u' x * v x