ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁴ : Fintype ι<VAR>inst✝¹³ : Fintype ι'<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁷ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁶ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁵ : SeminormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>inst✝³ : SeminormedAddCommGroup G'<VAR>inst✝² : NormedSpace 𝕜 G'<VAR>n : ℕ<VAR>A : Type u_1<VAR>inst✝¹ : NormedRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<GOAL>‖1‖ ≤ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A‖
<VAR>α : Type u<VAR>β✝ : Type v<VAR>uniformSpace : UniformSpace α<VAR>β : Type u_1<VAR>inst✝ : SemilatticeSup β<VAR>u : β → α<VAR>h : CauchySeq u<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<GOAL>∃ k₀, ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V
<VAR>α : Type u<VAR>β✝ : Type v<VAR>uniformSpace : UniformSpace α<VAR>β : Type u_1<VAR>inst✝ : SemilatticeSup β<VAR>u : β → α<VAR>h : CauchySeq u<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>this : Nonempty β<GOAL>∃ k₀, ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V
<VAR>α : Type u<VAR>β✝ : Type v<VAR>uniformSpace : UniformSpace α<VAR>β : Type u_1<VAR>inst✝ : SemilatticeSup β<VAR>u : β → α<VAR>h : CauchySeq u<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>this✝ : Nonempty β<VAR>this : Tendsto (Prod.map u u) atTop (𝓤 α)<GOAL>∃ k₀, ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V
<VAR>α : Type u<VAR>β✝ : Type v<VAR>uniformSpace : UniformSpace α<VAR>β : Type u_1<VAR>inst✝ : SemilatticeSup β<VAR>u : β → α<VAR>h : CauchySeq u<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>this✝ : Nonempty β<VAR>this : Tendsto (Prod.map u u) (atTop ×ˢ atTop) (𝓤 α)<GOAL>∃ k₀, ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V
<VAR>α : Type u_1<VAR>inst✝ : OrderedRing α<VAR>a : α<GOAL>Pairwise (Disjoint on fun n => Ico (↑n) (↑n + 1))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : TopologicalSemiring R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a<VAR>inst✝ : UniqueContinuousFunctionalCalculus R A<VAR>φ : C(↑(spectrum R a), R) →⋆ₐ[R] A<VAR>hφ₁ : Continuous ⇑φ<VAR>hφ₂ : φ (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) = a<GOAL>(cfcHom ha) (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) = φ (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R))
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>s : Set X<VAR>t : Set Y<VAR>x✝ : X × Y<VAR>a : X<VAR>b : Y<GOAL>(a, b) ∈ closure (s ×ˢ t) ↔ (a, b) ∈ closure s ×ˢ closure t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E'✝ : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁵ : Norm E<VAR>inst✝¹⁴ : Norm F<VAR>inst✝¹³ : Norm G<VAR>inst✝¹² : SeminormedAddCommGroup E'✝<VAR>inst✝¹¹ : SeminormedAddCommGroup F'<VAR>inst✝¹⁰ : SeminormedAddCommGroup G'<VAR>inst✝⁹ : NormedAddCommGroup E''<VAR>inst✝⁸ : NormedAddCommGroup F''<VAR>inst✝⁷ : NormedAddCommGroup G''<VAR>inst✝⁶ : SeminormedRing R<VAR>inst✝⁵ : SeminormedAddGroup E'''<VAR>inst✝⁴ : SeminormedRing R'<VAR>inst✝³ : NormedDivisionRing 𝕜<VAR>inst✝² : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f✝ : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'✝<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>ι : Type u_17<VAR>inst✝¹ : Fintype ι<VAR>E' : ι → Type u_18<VAR>inst✝ : (i : ι) → NormedAddCommGroup (E' i)<VAR>f : α → (i : ι) → E' i<GOAL>f =O[l] g' ↔ ∀ (i : ι), (fun x => f x i) =O[l] g'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E'✝ : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁵ : Norm E<VAR>inst✝¹⁴ : Norm F<VAR>inst✝¹³ : Norm G<VAR>inst✝¹² : SeminormedAddCommGroup E'✝<VAR>inst✝¹¹ : SeminormedAddCommGroup F'<VAR>inst✝¹⁰ : SeminormedAddCommGroup G'<VAR>inst✝⁹ : NormedAddCommGroup E''<VAR>inst✝⁸ : NormedAddCommGroup F''<VAR>inst✝⁷ : NormedAddCommGroup G''<VAR>inst✝⁶ : SeminormedRing R<VAR>inst✝⁵ : SeminormedAddGroup E'''<VAR>inst✝⁴ : SeminormedRing R'<VAR>inst✝³ : NormedDivisionRing 𝕜<VAR>inst✝² : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f✝ : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'✝<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>ι : Type u_17<VAR>inst✝¹ : Fintype ι<VAR>E' : ι → Type u_18<VAR>inst✝ : (i : ι) → NormedAddCommGroup (E' i)<VAR>f : α → (i : ι) → E' i<GOAL>(∀ᶠ (c : ℝ) in atTop, IsBigOWith c l f g') ↔ ∀ᶠ (x : ℝ) in atTop, ∀ (i : ι), IsBigOWith x l (fun x => f x i) g'
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : SMul M X<VAR>inst✝² : ContinuousSMul M X<VAR>f✝ : Y → M<VAR>g : Y → X<VAR>b : Y<VAR>s : Set Y<VAR>N : Type u_5<VAR>inst✝¹ : SMul N Y<VAR>inst✝ : TopologicalSpace N<VAR>f : N → M<VAR>hg : Inducing g<VAR>hf : Continuous f<VAR>hsmul : ∀ {c : N} {x : Y}, g (c • x) = f c • g x<GOAL>Continuous fun p => p.1 • p.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CommMonoid β<VAR>n : ℕ<VAR>f : Fin n → β<GOAL>∏ i : Fin n, f i = (List.map f (List.finRange n)).prod
<VAR>F : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝³ : Mul M<VAR>inst✝² : Mul N<VAR>a x y : M<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : MulHomClass F M N<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>h : Commute (f x) (f y)<GOAL>f (x * y) = f (y * x)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>m : Multiset α<GOAL>(toFinsupp m).multinomial = (card m).choose (count a m) * (toFinsupp (filter (fun x => a ≠ x) m)).multinomial
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>m : Multiset α<GOAL>card m = (toFinsupp m).sum fun x => id
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>m : Multiset α<GOAL>toFinsupp (filter (fun x => a ≠ x) m) = (toFinsupp m).update a 0
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : Group G'<VAR>H K L : Subgroup G<VAR>ι : Type u_3<VAR>inst✝ : Finite ι<VAR>f : ι → Subgroup G<VAR>hf : ∀ (i : ι), (f i).index ≠ 0<GOAL>(⨅ i, f i).index ≠ 0
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : Group G'<VAR>H K L : Subgroup G<VAR>ι : Type u_3<VAR>inst✝ : Finite ι<VAR>f : ι → Subgroup G<VAR>hf : ∀ (i : ι), (f i).relindex ⊤ ≠ 0<GOAL>(⨅ i, f i).relindex ⊤ ≠ 0
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>F : Type u_3<VAR>inst✝² : FunLike F (Set α) ℝ≥0∞<VAR>inst✝¹ : OuterMeasureClass F α<VAR>μ✝ : F<VAR>s✝ t : Set α<VAR>inst✝ : Fintype ι<VAR>μ : F<VAR>s : ι → Set α<GOAL>μ (⋃ i, s i) ≤ ∑ i : ι, μ (s i)
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → Set (Set Ω)<VAR>s' : Set (Set Ω)<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>hyp : ∀ (n : ι), IndepSets (s n) s' κ μ<VAR>t1 t2 : Set Ω<VAR>ht1 : t1 ∈ ⋃ n, s n<VAR>ht2 : t2 ∈ s'<GOAL>∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → Set (Set Ω)<VAR>s' : Set (Set Ω)<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>hyp : ∀ (n : ι), IndepSets (s n) s' κ μ<VAR>t1 t2 : Set Ω<VAR>ht1 : ∃ i, t1 ∈ s i<VAR>ht2 : t2 ∈ s'<GOAL>∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.322180, u_1} C<VAR>X Y Z : C<VAR>inst✝ : HasPullbacks C<VAR>U V₁ V₂ : C<VAR>f : X ⟶ Y<VAR>i : U ⟶ Y<VAR>i₁ : V₁ ⟶ pullback f i<VAR>i₂ : V₂ ⟶ pullback f i<GOAL>(i₁ ≫ snd f i) ≫ i = (i₁ ≫ fst f i) ≫ f
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.322180, u_1} C<VAR>X Y Z : C<VAR>inst✝ : HasPullbacks C<VAR>U V₁ V₂ : C<VAR>f : X ⟶ Y<VAR>i : U ⟶ Y<VAR>i₁ : V₁ ⟶ pullback f i<VAR>i₂ : V₂ ⟶ pullback f i<GOAL>(i₂ ≫ snd f i) ≫ i = (i₂ ≫ fst f i) ≫ f
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>X Y Z : C<VAR>inst✝ : HasPullbacks C<VAR>U V₁ V₂ : C<VAR>f : X ⟶ Y<VAR>i : U ⟶ Y<VAR>i₁ : V₁ ⟶ pullback f i<VAR>i₂ : V₂ ⟶ pullback f i<GOAL>snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫ snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₂ ≫ fst f i = fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>X Y Z : C<VAR>inst✝ : HasPullbacks C<VAR>U V₁ V₂ : C<VAR>f : X ⟶ Y<VAR>i : U ⟶ Y<VAR>i₁ : V₁ ⟶ pullback f i<VAR>i₂ : V₂ ⟶ pullback f i<GOAL>snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫ snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₂ ≫ fst f i = fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫ 𝟙 X
<VAR>S : LightProfinite<VAR>C : Type u_1<VAR>D : Type u_2<VAR>J : Type u_3<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_5, u_2} D<VAR>inst✝¹ : Category.{u_6, u_3} J<VAR>K : J ⥤ C<VAR>F : C ⥤ D<VAR>inst✝ : CreatesLimit K F<VAR>c : Cone (K ⋙ F)<VAR>t : IsLimit c<VAR>n : J<VAR>this : (liftedLimitMapsToOriginal t).hom.hom ≫ c.π.app n = F.map ((liftLimit t).π.app n)<GOAL>(liftedLimitMapsToOriginal t).inv.hom ≫ F.map ((liftLimit t).π.app n) = c.π.app n
<VAR>S : LightProfinite<VAR>C : Type u_1<VAR>D : Type u_2<VAR>J : Type u_3<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_5, u_2} D<VAR>inst✝¹ : Category.{u_6, u_3} J<VAR>K : J ⥤ C<VAR>F : C ⥤ D<VAR>inst✝ : CreatesLimit K F<VAR>c : Cone (K ⋙ F)<VAR>t : IsLimit c<VAR>n : J<VAR>this : (liftedLimitMapsToOriginal t).hom.hom ≫ c.π.app n = F.map ((liftLimit t).π.app n)<GOAL>((liftedLimitMapsToOriginal t).inv ≫ (liftedLimitMapsToOriginal t).hom).hom ≫ c.π.app n = c.π.app n
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Semiring R<VAR>h_comm : Commute x y<VAR>m n k : ℕ<VAR>hx : x ^ m = 0<VAR>hy : y ^ n = 0<VAR>h : m + n ≤ k + 1<GOAL>(x + y) ^ k = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Semiring R<VAR>h_comm : Commute x y<VAR>m n k : ℕ<VAR>hx : x ^ m = 0<VAR>hy : y ^ n = 0<VAR>h : m + n ≤ k + 1<GOAL>∑ m ∈ Finset.antidiagonal k, k.choose m.1 • (x ^ m.1 * y ^ m.2) = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Semiring R<VAR>h_comm : Commute x y<VAR>m n k : ℕ<VAR>hx : x ^ m = 0<VAR>hy : y ^ n = 0<VAR>h : m + n ≤ k + 1<GOAL>∀ x_1 ∈ Finset.antidiagonal k, k.choose x_1.1 • (x ^ x_1.1 * y ^ x_1.2) = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Semiring R<VAR>h_comm : Commute x y<VAR>m n k : ℕ<VAR>hx : x ^ m = 0<VAR>hy : y ^ n = 0<VAR>h : m + n ≤ k + 1<VAR>i j : ℕ<VAR>hij : (i, j) ∈ Finset.antidiagonal k<GOAL>k.choose (i, j).1 • (x ^ (i, j).1 * y ^ (i, j).2) = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Semiring R<VAR>h_comm : Commute x y<VAR>m n k : ℕ<VAR>hx : x ^ m = 0<VAR>hy : y ^ n = 0<VAR>h : m + n ≤ k + 1<VAR>i j : ℕ<VAR>hij : (i, j) ∈ Finset.antidiagonal k<GOAL>x ^ i * y ^ j = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Semiring R<VAR>h_comm : Commute x y<VAR>m n k : ℕ<VAR>hx : x ^ m = 0<VAR>hy : y ^ n = 0<VAR>h : m + n ≤ k + 1<VAR>i j : ℕ<VAR>hij : (i, j) ∈ Finset.antidiagonal k<VAR>hi : ¬m ≤ i<GOAL>x ^ i * y ^ j = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Semiring R<VAR>h_comm : Commute x y<VAR>m n k : ℕ<VAR>hx : x ^ m = 0<VAR>hy : y ^ n = 0<VAR>h : m + n ≤ k + 1<VAR>i j : ℕ<VAR>hij : (i, j) ∈ Finset.antidiagonal k<VAR>hi : ¬m ≤ i<GOAL>n ≤ j
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>i : ι<VAR>b : B<VAR>a v : F<VAR>h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v<GOAL>Continuous (let_fun this := fun x => { proj := x, snd := v }; this)
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>i : ι<VAR>b : B<VAR>a v : F<VAR>h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v<VAR>x : B<GOAL>ContinuousAt (let_fun this := fun x => { proj := x, snd := v }; this) x
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>i : ι<VAR>b : B<VAR>a v : F<VAR>h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v<VAR>x : B<VAR>A : Z.baseSet (Z.indexAt x) ∈ 𝓝 x<GOAL>ContinuousAt (let_fun this := fun x => { proj := x, snd := v }; this) x
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>i : ι<VAR>b : B<VAR>a v : F<VAR>h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v<VAR>x : B<VAR>A : Z.baseSet (Z.indexAt x) ∈ 𝓝 x<GOAL>(let_fun this := fun x => { proj := x, snd := v }; this) ⁻¹' (Z.localTrivAt x).source ∈ 𝓝 x
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>i : ι<VAR>b : B<VAR>a v : F<VAR>h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v<VAR>x : B<VAR>A : Z.baseSet (Z.indexAt x) ∈ 𝓝 x<GOAL>ContinuousAt (↑(Z.localTrivAt x).toPartialHomeomorph ∘ let_fun this := fun x => { proj := x, snd := v }; this) x
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<GOAL>vars 0 = ∅
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasShift C ℤ<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>a b : ℤ<VAR>T : Triangle C<GOAL>((a + b).negOnePow • (CategoryTheory.shiftFunctor C (a + b)).map T.mor₁) ≫ (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₂ = (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁ ≫ (b.negOnePow • (CategoryTheory.shiftFunctor C b).map (a.negOnePow • (CategoryTheory.shiftFunctor C a).map T.mor₁))
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasShift C ℤ<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>a b : ℤ<VAR>T : Triangle C<GOAL>((a + b).negOnePow • (CategoryTheory.shiftFunctor C (a + b)).map T.mor₂) ≫ (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₃ = (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₂ ≫ (b.negOnePow • (CategoryTheory.shiftFunctor C b).map (a.negOnePow • (CategoryTheory.shiftFunctor C a).map T.mor₂))
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasShift C ℤ<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>a b : ℤ<VAR>T : Triangle C<GOAL>((a + b).negOnePow • (CategoryTheory.shiftFunctor C (a + b)).map T.mor₃ ≫ (shiftFunctorComm C 1 (a + b)).hom.app T.obj₁) ≫ (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁) = (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₃ ≫ (b.negOnePow • (CategoryTheory.shiftFunctor C b).map (a.negOnePow • (CategoryTheory.shiftFunctor C a).map T.mor₃ ≫ (shiftFunctorComm C 1 a).hom.app T.obj₁) ≫ (shiftFunctorComm C 1 b).hom.app ((CategoryTheory.shiftFunctor C a).obj T.obj₁))
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasShift C ℤ<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>a b : ℤ<VAR>T : Triangle C<GOAL>(a + b).negOnePow • (CategoryTheory.shiftFunctor C (a + b)).map T.mor₃ ≫ (shiftFunctorComm C 1 (a + b)).hom.app T.obj₁ ≫ (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁) = (b.negOnePow * a.negOnePow) • (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₃ ≫ (CategoryTheory.shiftFunctor C b).map ((CategoryTheory.shiftFunctor C a).map T.mor₃) ≫ (CategoryTheory.shiftFunctor C b).map ((shiftFunctorComm C 1 a).hom.app T.obj₁) ≫ (shiftFunctorComm C 1 b).hom.app ((CategoryTheory.shiftFunctor C a).obj T.obj₁)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasShift C ℤ<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>a b : ℤ<VAR>T : Triangle C<GOAL>(a + b).negOnePow • (CategoryTheory.shiftFunctor C (a + b)).map T.mor₃ ≫ (shiftFunctorComm C 1 (a + b)).hom.app T.obj₁ ≫ (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁) = (b.negOnePow * a.negOnePow) • (CategoryTheory.shiftFunctor C (a + b)).map T.mor₃ ≫ (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app ((CategoryTheory.shiftFunctor C 1).obj T.obj₁) ≫ (CategoryTheory.shiftFunctor C b).map ((shiftFunctorComm C 1 a).hom.app T.obj₁) ≫ (shiftFunctorComm C 1 b).hom.app ((CategoryTheory.shiftFunctor C a).obj T.obj₁)
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z w : K<GOAL>z < w ↔ re z < re w ∧ im z = im w
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z w : K<GOAL>(re z ≤ re w ∧ im z = im w) ∧ z ≠ w ↔ (re z ≤ re w ∧ re z ≠ re w) ∧ im z = im w
<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>inst✝ : Monoid M<VAR>l : List Mᵐᵒᵖ<GOAL>unop l.prod = (map unop l).reverse.prod
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f✝ : Filter α<VAR>g : Filter β<VAR>f : Filter α<VAR>g₁ g₂ : Filter β<GOAL>f.prod (g₁ ⊔ g₂) = f.prod g₁ ⊔ f.prod g₂
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizedGCDMonoid α<VAR>s s₁ s₂ : Finset β<VAR>f : β → α<VAR>inst✝ : Nontrivial α<GOAL>s.lcm f = 0 ↔ 0 ∈ f '' ↑s
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : DecidableEq L<VAR>inst✝⁷ : Algebra R K<VAR>inst✝⁶ : IsFractionRing R K<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra R L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsDedekindDomain R<VAR>I J : ↥(Ideal R)⁰<GOAL>mk0 I = (mk0 J)⁻¹ ↔ ∃ x, x ≠ 0 ∧ ↑I * ↑J = Ideal.span {x}
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : DecidableEq L<VAR>inst✝⁷ : Algebra R K<VAR>inst✝⁶ : IsFractionRing R K<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra R L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsDedekindDomain R<VAR>I J : ↥(Ideal R)⁰<GOAL>(∃ a, ↑I * ↑J = Submodule.span R {a}) ↔ ∃ x, x ≠ 0 ∧ ↑I * ↑J = Ideal.span {x}
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : DecidableEq L<VAR>inst✝⁷ : Algebra R K<VAR>inst✝⁶ : IsFractionRing R K<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra R L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsDedekindDomain R<VAR>I J : ↥(Ideal R)⁰<VAR>x✝ : ∃ a, ↑I * ↑J = Submodule.span R {a}<VAR>a : R<VAR>ha : ↑I * ↑J = Submodule.span R {a}<VAR>this : a = 0<GOAL>False
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : DecidableEq L<VAR>inst✝⁷ : Algebra R K<VAR>inst✝⁶ : IsFractionRing R K<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra R L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsDedekindDomain R<VAR>I J : ↥(Ideal R)⁰<VAR>x✝ : ∃ a, ↑I * ↑J = Submodule.span R {a}<VAR>a : R<VAR>ha : ↑I * ↑J = ⊥<VAR>this : a = 0<GOAL>False
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>inst✝ : SecondCountableTopology α<VAR>S : Set (Set α)<VAR>H : ∀ s ∈ S, IsOpen s<GOAL>∃ T, T.Countable ∧ T ⊆ S ∧ ⋃₀ T = ⋃₀ S
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : CommSemiring K<VAR>i : R →+* K<VAR>a b : R<VAR>bi : K<VAR>N : ℕ<VAR>f g : R[X]<VAR>x✝¹ : DenomsClearable a b N f i<VAR>x✝ : DenomsClearable a b N g i<VAR>Df : R<VAR>bf : K<VAR>bfu : bf * i b = 1<VAR>Hf : i Df = i b ^ N * eval (i a * bf) (Polynomial.map i f)<VAR>Dg : R<VAR>bg : K<VAR>bgu : bg * i b = 1<VAR>Hg : i Dg = i b ^ N * eval (i a * bg) (Polynomial.map i g)<GOAL>i (Df + Dg) = i b ^ N * eval (i a * bf) (Polynomial.map i (f + g))
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : CommSemiring K<VAR>i : R →+* K<VAR>a b : R<VAR>bi : K<VAR>N : ℕ<VAR>f g : R[X]<VAR>x✝¹ : DenomsClearable a b N f i<VAR>x✝ : DenomsClearable a b N g i<VAR>Df : R<VAR>bf : K<VAR>bfu : bf * i b = 1<VAR>Hf : i Df = i b ^ N * eval (i a * bf) (Polynomial.map i f)<VAR>Dg : R<VAR>bg : K<VAR>bgu : bg * i b = 1<VAR>Hg : i Dg = i b ^ N * eval (i a * bg) (Polynomial.map i g)<GOAL>i b ^ N * eval (i a * bf) (Polynomial.map i f) + i b ^ N * eval (i a * bg) (Polynomial.map i g) = i b ^ N * eval (i a * bf) (Polynomial.map i f) + i b ^ N * eval (i a * bf) (Polynomial.map i g)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : CommSemiring K<VAR>i : R →+* K<VAR>a b : R<VAR>bi : K<VAR>N : ℕ<VAR>f g : R[X]<VAR>x✝¹ : DenomsClearable a b N f i<VAR>x✝ : DenomsClearable a b N g i<VAR>Df : R<VAR>bf : K<VAR>bfu : bf * i b = 1<VAR>Hf : i Df = i b ^ N * eval (i a * bf) (Polynomial.map i f)<VAR>Dg : R<VAR>bg : K<VAR>bgu : bg * i b = 1<VAR>Hg : i Dg = i b ^ N * eval (i a * bg) (Polynomial.map i g)<GOAL>bg = bf
<VAR>n : ℕ<VAR>s : ℝ<VAR>hs : s ∈ Ici 1<GOAL>‖term (n + 1) s‖ ≤ term (n + 1) 1
<VAR>n : ℕ<VAR>s : ℝ<VAR>hs : s ∈ Ici 1<GOAL>∫ (x : ℝ) in ↑(n + 1)..↑(n + 1) + 1, (x - ↑(n + 1)) / x ^ (s + 1) ≤ ∫ (x : ℝ) in ↑(n + 1)..↑(n + 1) + 1, (x - ↑(n + 1)) / x ^ (1 + 1)
<VAR>n : ℕ<VAR>s : ℝ<VAR>hs : s ∈ Ici 1<GOAL>0 ≤ ∫ (x : ℝ) in ↑(n + 1)..↑(n + 1) + 1, (x - ↑(n + 1)) / x ^ (s + 1)
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<GOAL>(C a).coeff n = if n = 0 then a else 0
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<GOAL>n = 0 ↔ 0 = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>f✝ g : β → α<VAR>a a₁ a₂ : α<VAR>f : Bool → α<GOAL>∏' (i : Bool), f i = f false * f true
<VAR>F : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : CommApplicative F<VAR>α' β' : Type u<VAR>f : α' → F β'<VAR>G : Type u_1 → Type u_1<VAR>inst✝¹ : Applicative G<VAR>inst✝ : CommApplicative G<VAR>α β γ : Type u_1<VAR>g : α → G β<VAR>h : β → γ<VAR>x : Multiset α<GOAL>Functor.map h <$> traverse g x = traverse (Functor.map h ∘ g) x
<VAR>F : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : CommApplicative F<VAR>α' β' : Type u<VAR>f : α' → F β'<VAR>G : Type u_1 → Type u_1<VAR>inst✝¹ : Applicative G<VAR>inst✝ : CommApplicative G<VAR>α β γ : Type u_1<VAR>g : α → G β<VAR>h : β → γ<VAR>x : Multiset α<GOAL>∀ (a : List α), Functor.map h <$> traverse g ⟦a⟧ = traverse (Functor.map h ∘ g) ⟦a⟧