ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X Y : TopCat<VAR>f g : C(↑X, ↑Y)<VAR>H : f.Homotopy g<VAR>x₀ x₁ : ↑X<VAR>p : fromTop x₀ ⟶ fromTop x₁<VAR>p' : Path (fromTop x₀).as (fromTop x₁).as<GOAL>∀ (t : ↑I), f (p' t) = H.uliftMap (((Path.refl { down := 0 }).prod p') t)
<VAR>X Y : TopCat<VAR>f g : C(↑X, ↑Y)<VAR>H : f.Homotopy g<VAR>x₀ x₁ : ↑X<VAR>p : fromTop x₀ ⟶ fromTop x₁<VAR>p' : Path (fromTop x₀).as (fromTop x₁).as<GOAL>∀ (t : ↑I), f (p' t) = H.uliftMap ((fun t => ((Path.refl { down := 0 }) t, p' t)) t)
<VAR>X Y : TopCat<VAR>f g : C(↑X, ↑Y)<VAR>H : f.Homotopy g<VAR>x₀ x₁ : ↑X<VAR>p : fromTop x₀ ⟶ fromTop x₁<VAR>p' : Path (fromTop x₀).as (fromTop x₁).as<GOAL>∀ (t : ↑I), f (p' t) = H (((Path.refl { down := 0 }) t).down, p' t)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>n✝ : ℕ<VAR>S✝ : ComposableArrows C n✝<VAR>n : ℕ<VAR>S : ComposableArrows C (n + 2)<VAR>h₁ : S.δlast.Exact<VAR>h₂ : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact<GOAL>S.Exact
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>n✝ : ℕ<VAR>S✝ : ComposableArrows C n✝<VAR>n : ℕ<VAR>S : ComposableArrows C (n + 2)<VAR>h₁ : S.δlast.Exact<VAR>h₂ : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact<GOAL>S.δlast.Exact ∧ (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>n : ℕ<VAR>hst : s ⊆ t<VAR>hsn : s.ncard ≤ n<VAR>hnt : n ≤ t.ncard<GOAL>∃ u, s ⊆ u ∧ u ⊆ t ∧ u.ncard = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>n : ℕ<VAR>hst : s ⊆ t<VAR>hsn : s.ncard ≤ n<VAR>hnt : n ≤ t.ncard<VAR>ht : t.Infinite<GOAL>∃ u, s ⊆ u ∧ u ⊆ t ∧ u.ncard = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>n : ℕ<VAR>hst : s ⊆ t<VAR>hsn : s.ncard ≤ n<VAR>hnt : n ≤ t.ncard<VAR>ht : t.Finite<GOAL>∃ u, s ⊆ u ∧ u ⊆ t ∧ u.ncard = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Set α<VAR>f : α → β<VAR>n : ℕ<VAR>hnt : n ≤ t.ncard<VAR>ht : t.Finite<VAR>s : Finset α<VAR>hst : ↑s ⊆ t<VAR>hsn : (↑s).ncard ≤ n<GOAL>∃ u, ↑s ⊆ u ∧ u ⊆ t ∧ u.ncard = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>n : ℕ<VAR>s : Finset α<VAR>hsn : (↑s).ncard ≤ n<VAR>t : Finset α<VAR>hnt : n ≤ (↑t).ncard<VAR>hst : ↑s ⊆ ↑t<GOAL>∃ u, ↑s ⊆ u ∧ u ⊆ ↑t ∧ u.ncard = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>n : ℕ<VAR>s : Finset α<VAR>hsn : (↑s).ncard ≤ n<VAR>t : Finset α<VAR>hnt : n ≤ (↑t).ncard<VAR>hst : ↑s ⊆ ↑t<VAR>u : Finset α<VAR>hsu : s ⊆ u<VAR>hut : u ⊆ t<VAR>hu : u.card = n<GOAL>∃ u, ↑s ⊆ u ∧ u ⊆ ↑t ∧ u.ncard = n
<VAR>R : Type u_1<VAR>inst✝⁴ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>N : Type u_3<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>ι : Type u_4<VAR>ι' : Type u_5<GOAL>map ι (LinearEquiv.refl R M) = Equiv.refl (Orientation R M ι)
<VAR>G : Type w<VAR>inst✝ : TopologicalSpace G<VAR>μ : Content G<VAR>U : Opens G<VAR>hU : μ.innerContent U ≠ ⊤<VAR>ε : ℝ≥0<VAR>hε : ε ≠ 0<GOAL>∃ K, ↑K ⊆ ↑U ∧ μ.innerContent U ≤ (fun s => ↑(μ.toFun s)) K + ↑ε
<VAR>G : Type w<VAR>inst✝ : TopologicalSpace G<VAR>μ : Content G<VAR>U : Opens G<VAR>hU : μ.innerContent U ≠ ⊤<VAR>ε : ℝ≥0<VAR>hε : ε ≠ 0<VAR>h'ε : ↑ε ≠ 0<GOAL>∃ K, ↑K ⊆ ↑U ∧ μ.innerContent U ≤ (fun s => ↑(μ.toFun s)) K + ↑ε
<VAR>G : Type w<VAR>inst✝ : TopologicalSpace G<VAR>μ : Content G<VAR>U : Opens G<VAR>hU : μ.innerContent U ≠ ⊤<VAR>ε : ℝ≥0<VAR>hε : ε ≠ 0<VAR>h'ε : ↑ε ≠ 0<VAR>h : μ.innerContent U ≤ ↑ε<GOAL>∃ K, ↑K ⊆ ↑U ∧ μ.innerContent U ≤ (fun s => ↑(μ.toFun s)) K + ↑ε
<VAR>G : Type w<VAR>inst✝ : TopologicalSpace G<VAR>μ : Content G<VAR>U : Opens G<VAR>hU : μ.innerContent U ≠ ⊤<VAR>ε : ℝ≥0<VAR>hε : ε ≠ 0<VAR>h'ε : ↑ε ≠ 0<VAR>h : ↑ε < μ.innerContent U<GOAL>∃ K, ↑K ⊆ ↑U ∧ μ.innerContent U ≤ (fun s => ↑(μ.toFun s)) K + ↑ε
<VAR>G : Type w<VAR>inst✝ : TopologicalSpace G<VAR>μ : Content G<VAR>U : Opens G<VAR>hU : μ.innerContent U ≠ ⊤<VAR>ε : ℝ≥0<VAR>hε : ε ≠ 0<VAR>h'ε : ↑ε ≠ 0<VAR>h : ↑ε < μ.innerContent U<VAR>h₂ : μ.innerContent U - ↑ε < μ.innerContent U<GOAL>∃ K, ↑K ⊆ ↑U ∧ μ.innerContent U ≤ (fun s => ↑(μ.toFun s)) K + ↑ε
<VAR>G : Type w<VAR>inst✝ : TopologicalSpace G<VAR>μ : Content G<VAR>U : Opens G<VAR>hU : μ.innerContent U ≠ ⊤<VAR>ε : ℝ≥0<VAR>hε : ε ≠ 0<VAR>h'ε : ↑ε ≠ 0<VAR>h : ↑ε < μ.innerContent U<VAR>h₂ : μ.innerContent U - ↑ε < ⨆ K, ⨆ (_ : ↑K ⊆ ↑U), (fun s => ↑(μ.toFun s)) K<GOAL>∃ K, ↑K ⊆ ↑U ∧ μ.innerContent U ≤ (fun s => ↑(μ.toFun s)) K + ↑ε
<VAR>G : Type w<VAR>inst✝ : TopologicalSpace G<VAR>μ : Content G<VAR>U : Opens G<VAR>hU : μ.innerContent U ≠ ⊤<VAR>ε : ℝ≥0<VAR>hε : ε ≠ 0<VAR>h'ε : ↑ε ≠ 0<VAR>h : ↑ε < μ.innerContent U<VAR>h₂ : ∃ i, ∃ (_ : ↑i ⊆ ↑U), μ.innerContent U - ↑ε < ↑(μ.toFun i)<GOAL>∃ K, ↑K ⊆ ↑U ∧ μ.innerContent U ≤ (fun s => ↑(μ.toFun s)) K + ↑ε
<VAR>G : Type w<VAR>inst✝ : TopologicalSpace G<VAR>μ : Content G<VAR>U✝ : Opens G<VAR>hU : μ.innerContent U✝ ≠ ⊤<VAR>ε : ℝ≥0<VAR>hε : ε ≠ 0<VAR>h'ε : ↑ε ≠ 0<VAR>h : ↑ε < μ.innerContent U✝<VAR>U : Compacts G<VAR>h1U : ↑U ⊆ ↑U✝<VAR>h2U : μ.innerContent U✝ - ↑ε < ↑(μ.toFun U)<GOAL>μ.innerContent U✝ ≤ (fun s => ↑(μ.toFun s)) U + ↑ε
<VAR>G : Type w<VAR>inst✝ : TopologicalSpace G<VAR>μ : Content G<VAR>U✝ : Opens G<VAR>hU : μ.innerContent U✝ ≠ ⊤<VAR>ε : ℝ≥0<VAR>hε : ε ≠ 0<VAR>h'ε : ↑ε ≠ 0<VAR>h : ↑ε < μ.innerContent U✝<VAR>U : Compacts G<VAR>h1U : ↑U ⊆ ↑U✝<VAR>h2U : μ.innerContent U✝ - ↑ε < ↑(μ.toFun U)<GOAL>μ.innerContent U✝ - ↑ε ≤ (fun s => ↑(μ.toFun s)) U
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<GOAL>homologyMap' φ₁ h₁ h₂ = homologyMap' φ₂ h₁ h₂
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b : α<GOAL>a ≤ max a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : CompleteLattice α<VAR>f : (i : ι) → κ i → α<GOAL>Iic (⨅ i, ⨅ j, f i j) = ⨅ i, ⨅ j, Iic (f i j)
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : AddCommMonoid N<VAR>inst✝⁶ : Module R N<VAR>Q : QuadraticMap R M N<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra S R<VAR>inst✝³ : Module S M<VAR>inst✝² : IsScalarTower S R M<VAR>inst✝¹ : Module S N<VAR>inst✝ : IsScalarTower S R N<VAR>a : S<VAR>x : M<GOAL>Q (a • x) = (a * a) • Q x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>inst✝ : CompleteLattice α<VAR>s : Set α<GOAL>Iic (sInf s) = ⋂ a ∈ s, Iic a
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : AddGroup G<VAR>inst✝ : AddAction G α<VAR>g : G<VAR>a : α<VAR>h : G<GOAL>h ∈ stabilizer G (g +ᵥ a) ↔ h ∈ AddSubgroup.map (AddEquiv.toAddMonoidHom (AddAut.conj g)) (stabilizer G a)
<VAR>σ K : Type u<VAR>inst✝² : Fintype K<VAR>inst✝¹ : Field K<VAR>inst✝ : Fintype σ<GOAL>Module.rank K (↑{s | ∀ (n : σ), s n ≤ Fintype.card K - 1} →₀ K) = #↑{s | ∀ (n : σ), s n ≤ Fintype.card K - 1}
<VAR>σ K : Type u<VAR>inst✝² : Fintype K<VAR>inst✝¹ : Field K<VAR>inst✝ : Fintype σ<GOAL>#↑{s | ∀ (n : σ), s n ≤ Fintype.card K - 1} = #↑{s | ∀ (n : σ), s n < Fintype.card K}
<VAR>σ K : Type u<VAR>inst✝² : Fintype K<VAR>inst✝¹ : Field K<VAR>inst✝ : Fintype σ<VAR>f : σ →₀ ℕ<GOAL>f ∈ {s | ∀ (n : σ), s n ≤ Fintype.card K - 1} ↔ Finsupp.equivFunOnFinite f ∈ {s | ∀ (n : σ), s n < Fintype.card K}
<VAR>σ K : Type u<VAR>inst✝² : Fintype K<VAR>inst✝¹ : Field K<VAR>inst✝ : Fintype σ<VAR>f : σ →₀ ℕ<VAR>n : σ<GOAL>1 ≤ Fintype.card K
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<VAR>h : Disjoint a b<GOAL>a \ b = a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<VAR>h : Disjoint a b<GOAL>a \ b = a \ ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝¹ : One M<VAR>inst✝ : One N<VAR>s✝ t✝ : Set α<VAR>f✝ g : α → M<VAR>a : α<VAR>s : Set α<VAR>f : α → M<VAR>t : Set M<VAR>ht : 1 ∉ t<GOAL>s.mulIndicator f ⁻¹' t = f ⁻¹' t ∩ s
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>P : MorphismProperty C<VAR>inst✝¹ : HasPullbacks C<VAR>inst✝ : P.RespectsIso<VAR>hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S), P g → P (pullback.fst f g)<VAR>X Y Y' S : C<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>f' : Y' ⟶ Y<VAR>g' : Y' ⟶ X<VAR>sq : IsPullback f' g' g f<VAR>hg : P g<GOAL>P g'
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>P : MorphismProperty C<VAR>inst✝¹ : HasPullbacks C<VAR>inst✝ : P.RespectsIso<VAR>hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S), P g → P (pullback.fst f g)<VAR>X Y Y' S : C<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>f' : Y' ⟶ Y<VAR>g' : Y' ⟶ X<VAR>sq : IsPullback f' g' g f<VAR>hg : P g<VAR>e : Y' ≅ pullback f g := ⋯.isoPullback<GOAL>P g'
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>P : MorphismProperty C<VAR>inst✝¹ : HasPullbacks C<VAR>inst✝ : P.RespectsIso<VAR>hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S), P g → P (pullback.fst f g)<VAR>X Y Y' S : C<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>f' : Y' ⟶ Y<VAR>g' : Y' ⟶ X<VAR>sq : IsPullback f' g' g f<VAR>hg : P g<VAR>e : Y' ≅ pullback f g := ⋯.isoPullback<GOAL>P (pullback.fst f g)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q✝ : MvPolynomial σ R<VAR>f q : R →+* S₁<VAR>r : R<VAR>hr : ∀ (r' : R), q r' = 0 ↔ r ∣ r'<VAR>φ : MvPolynomial σ R<GOAL>C r ∣ φ ↔ (map q) φ = 0
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q✝ : MvPolynomial σ R<VAR>f q : R →+* S₁<VAR>r : R<VAR>hr : ∀ (r' : R), q r' = 0 ↔ r ∣ r'<VAR>φ : MvPolynomial σ R<GOAL>(∀ (i : σ →₀ ℕ), r ∣ coeff i φ) ↔ ∀ (m : σ →₀ ℕ), coeff m ((map q) φ) = coeff m 0
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>t : Set X<GOAL>Tendsto some (coclosedCompact X) (𝓝 ∞)
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>t : Set X<GOAL>Tendsto some (coclosedCompact X) (map some (coclosedCompact X) ⊔ pure ∞)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>z w : ℂ<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])<VAR>Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s, DifferentiableAt ℂ f x<GOAL>(((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I)) + I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) - I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I) = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>f : α → ℝ≥0∞<VAR>t : Set α<VAR>ht : MeasurableSet t<GOAL>(μ.withDensity (s.indicator f)) t = ((μ.restrict s).withDensity f) t
<VAR>V : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : SeminormedAddCommGroup V₁<VAR>inst✝¹ : SeminormedAddCommGroup V₂<VAR>inst✝ : SeminormedAddCommGroup V₃<VAR>f g : NormedAddGroupHom V₁ V₂<VAR>x : V₁<GOAL>‖f x‖ ≤ ‖f‖ * ‖x‖
<VAR>V : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : SeminormedAddCommGroup V₁<VAR>inst✝¹ : SeminormedAddCommGroup V₂<VAR>inst✝ : SeminormedAddCommGroup V₃<VAR>f g : NormedAddGroupHom V₁ V₂<VAR>x : V₁<VAR>C : ℝ<VAR>_Cpos : 0 < C<VAR>hC : ∀ (x : V₁), ‖f x‖ ≤ C * ‖x‖<GOAL>‖f x‖ ≤ ‖f‖ * ‖x‖
<VAR>V : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : SeminormedAddCommGroup V₁<VAR>inst✝¹ : SeminormedAddCommGroup V₂<VAR>inst✝ : SeminormedAddCommGroup V₃<VAR>f g : NormedAddGroupHom V₁ V₂<VAR>x : V₁<VAR>C : ℝ<VAR>_Cpos : 0 < C<VAR>hC : ‖f x‖ ≤ C * ‖x‖<VAR>h : ¬‖x‖ = 0<GOAL>‖f x‖ ≤ ‖f‖ * ‖x‖
<VAR>V : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : SeminormedAddCommGroup V₁<VAR>inst✝¹ : SeminormedAddCommGroup V₂<VAR>inst✝ : SeminormedAddCommGroup V₃<VAR>f g : NormedAddGroupHom V₁ V₂<VAR>x : V₁<VAR>C : ℝ<VAR>_Cpos : 0 < C<VAR>hC : ‖f x‖ ≤ C * ‖x‖<VAR>h : ¬‖x‖ = 0<VAR>hlt : 0 < ‖x‖<GOAL>‖f x‖ ≤ ‖f‖ * ‖x‖
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Monoid S<VAR>inst✝ : DistribMulAction S N<VAR>f : M → N<VAR>s : S<VAR>x y : M<GOAL>polar (s • f) x y = s • polar f x y
<VAR>σ✝ : Type u_1<VAR>τ : Type u_2<VAR>R✝ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ inst✝⁴ : CommSemiring R✝<VAR>inst✝³ : CommSemiring S<VAR>φ ψ : MvPolynomial σ✝ R✝<VAR>m n✝¹ : ℕ<VAR>R : Type u_5<VAR>σ : Type u_6<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>F✝ G : MvPolynomial σ R<VAR>n✝ : ℕ<VAR>inst✝ : Infinite R<VAR>F : MvPolynomial σ R<VAR>n : ℕ<VAR>hF : F.IsHomogeneous n<VAR>h : ∀ (r : σ → R), (eval r) F = 0<GOAL>F = 0
<VAR>σ✝ : Type u_1<VAR>τ : Type u_2<VAR>R✝ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ inst✝⁴ : CommSemiring R✝<VAR>inst✝³ : CommSemiring S<VAR>φ ψ : MvPolynomial σ✝ R✝<VAR>m n✝¹ : ℕ<VAR>R : Type u_5<VAR>σ : Type u_6<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>F✝ G : MvPolynomial σ R<VAR>n✝ : ℕ<VAR>inst✝ : Infinite R<VAR>F : MvPolynomial σ R<VAR>n : ℕ<VAR>hF : F.IsHomogeneous n<VAR>h : ∀ (r : σ → R), (eval r) F = 0<GOAL>↑n ≤ #R
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>hfg : TendstoInMeasure μ f atTop g<GOAL>StrictMono (seqTendstoAeSeq hfg)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>hfg : TendstoInMeasure μ f atTop g<VAR>n : ℕ<GOAL>seqTendstoAeSeq hfg n < seqTendstoAeSeq hfg (n + 1)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>hfg : TendstoInMeasure μ f atTop g<VAR>n : ℕ<GOAL>seqTendstoAeSeq hfg n < max (seqTendstoAeSeqAux hfg (n + 1)) (seqTendstoAeSeq hfg n + 1)
<VAR>α : Type u_1<VAR>inst✝³ : GeneralizedBooleanAlgebra α<VAR>inst✝² : DecidableRel Disjoint<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>u v a✝ b✝ : α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>ha : a ∈ ↑(filter (fun x => compress u v x ∉ s) s)<VAR>b : α<VAR>hb : b ∈ ↑(filter (fun x => compress u v x ∉ s) s)<VAR>hab : compress u v a = compress u v b<GOAL>a = b
<VAR>α : Type u_1<VAR>inst✝³ : GeneralizedBooleanAlgebra α<VAR>inst✝² : DecidableRel Disjoint<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>u v a✝ b✝ : α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>ha : a ∈ s ∧ compress u v a ∉ s<VAR>b : α<VAR>hb : b ∈ s ∧ compress u v b ∉ s<VAR>hab : compress u v a = compress u v b<GOAL>a = b
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x✝ : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ LiftPropOn P g (s ∩ u)<VAR>x : M<VAR>hx : x ∈ s<VAR>u : Set M<VAR>u_open : IsOpen u<VAR>xu : x ∈ u<VAR>hu : LiftPropOn P g (s ∩ u)<VAR>this : LiftPropWithinAt P g (s ∩ u) x<GOAL>LiftPropWithinAt P g s x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x✝ : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ LiftPropOn P g (s ∩ u)<VAR>x : M<VAR>hx : x ∈ s<VAR>u : Set M<VAR>u_open : IsOpen u<VAR>xu : x ∈ u<VAR>hu : LiftPropOn P g (s ∩ u)<VAR>this : LiftPropWithinAt P g (s ∩ u) x<GOAL>u ∈ 𝓝 x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁸ : Category.{u_3, u_1} C<VAR>inst✝⁷ : Category.{u_4, u_2} D<VAR>inst✝⁶ : HasZeroMorphisms C<VAR>inst✝⁵ : HasZeroMorphisms D<VAR>S : ShortComplex C<VAR>h₁✝ : S.LeftHomologyData<VAR>h₂✝ : S.RightHomologyData<VAR>F✝ : C ⥤ D<VAR>inst✝⁴ : F✝.PreservesZeroMorphisms<VAR>hl : S.LeftHomologyData<VAR>hr : S.RightHomologyData<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hl₁ : S₁.LeftHomologyData<VAR>hr₁ : S₁.RightHomologyData<VAR>hl₂ : S₂.LeftHomologyData<VAR>hr₂ : S₂.RightHomologyData<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>F : C ⥤ D<VAR>inst✝³ : F.PreservesZeroMorphisms<VAR>inst✝² : S.HasHomology<VAR>inst✝¹ : (S.map F).HasHomology<VAR>inst✝ : F.PreservesRightHomologyOf S<GOAL>(((S.map F).homologyData.iso.hom ≫ rightHomologyMap' (𝟙 (S.map F)) (S.map F).homologyData.right (S.map F).rightHomologyData) ≫ rightHomologyMap' (𝟙 (S.map F)) (S.map F).rightHomologyData (S.homologyData.right.map F)) ≫ F.map (rightHomologyMap' (𝟙 S) S.homologyData.right S.rightHomologyData ≫ rightHomologyMap' (𝟙 S) S.rightHomologyData S.homologyData.right ≫ S.homologyData.iso.inv) = (((S.map F).homologyData.iso.hom ≫ rightHomologyMap' (𝟙 (S.map F)) (S.map F).homologyData.right (S.map F).rightHomologyData) ≫ rightHomologyMap' (𝟙 (S.map F)) (S.map F).rightHomologyData (hr.map F)) ≫ F.map (rightHomologyMap' (𝟙 S) hr S.rightHomologyData ≫ rightHomologyMap' (𝟙 S) S.rightHomologyData S.homologyData.right ≫ S.homologyData.iso.inv)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : T2Space M<VAR>v : VectorMeasure α M<VAR>f✝ : ℕ → Set α<VAR>inst✝ : Countable β<VAR>f : β → Set α<VAR>hf₁ : ∀ (i : β), MeasurableSet (f i)<VAR>hf₂ : Pairwise (Disjoint on f)<GOAL>HasSum (fun i => ↑v (f i)) (↑v (⋃ i, f i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : T2Space M<VAR>v : VectorMeasure α M<VAR>f✝ : ℕ → Set α<VAR>inst✝ : Countable β<VAR>f : β → Set α<VAR>hf₁ : ∀ (i : β), MeasurableSet (f i)<VAR>hf₂ : Pairwise (Disjoint on f)<VAR>val✝ : Encodable β<GOAL>HasSum (fun i => ↑v (f i)) (↑v (⋃ i, f i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : T2Space M<VAR>v : VectorMeasure α M<VAR>f✝ : ℕ → Set α<VAR>inst✝ : Countable β<VAR>f : β → Set α<VAR>hf₁ : ∀ (i : β), MeasurableSet (f i)<VAR>hf₂ : Pairwise (Disjoint on f)<VAR>val✝ : Encodable β<VAR>g : ℕ → Set α := fun i => ⋃ b ∈ Encodable.decode₂ β i, f b<VAR>hg : g = fun i => ⋃ b ∈ Encodable.decode₂ β i, f b<GOAL>HasSum (fun i => ↑v (f i)) (↑v (⋃ i, f i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : T2Space M<VAR>v : VectorMeasure α M<VAR>f✝ : ℕ → Set α<VAR>inst✝ : Countable β<VAR>f : β → Set α<VAR>hf₁ : ∀ (i : β), MeasurableSet (f i)<VAR>hf₂ : Pairwise (Disjoint on f)<VAR>val✝ : Encodable β<VAR>g : ℕ → Set α := fun i => ⋃ b ∈ Encodable.decode₂ β i, f b<VAR>hg : g = fun i => ⋃ b ∈ Encodable.decode₂ β i, f b<VAR>hg₁ : ∀ (i : ℕ), MeasurableSet (g i)<GOAL>HasSum (fun i => ↑v (f i)) (↑v (⋃ i, f i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : T2Space M<VAR>v : VectorMeasure α M<VAR>f✝ : ℕ → Set α<VAR>inst✝ : Countable β<VAR>f : β → Set α<VAR>hf₁ : ∀ (i : β), MeasurableSet (f i)<VAR>hf₂ : Pairwise (Disjoint on f)<VAR>val✝ : Encodable β<VAR>g : ℕ → Set α := fun i => ⋃ b ∈ Encodable.decode₂ β i, f b<VAR>hg : g = fun i => ⋃ b ∈ Encodable.decode₂ β i, f b<VAR>hg₁ : ∀ (i : ℕ), MeasurableSet (g i)<VAR>hg₂ : Pairwise (Disjoint on g)<GOAL>HasSum (fun i => ↑v (f i)) (↑v (⋃ i, f i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : T2Space M<VAR>v : VectorMeasure α M<VAR>f✝ : ℕ → Set α<VAR>inst✝ : Countable β<VAR>f : β → Set α<VAR>hf₁ : ∀ (i : β), MeasurableSet (f i)<VAR>hf₂ : Pairwise (Disjoint on f)<VAR>val✝ : Encodable β<VAR>g : ℕ → Set α := fun i => ⋃ b ∈ Encodable.decode₂ β i, f b<VAR>hg : g = fun i => ⋃ b ∈ Encodable.decode₂ β i, f b<VAR>hg₁ : ∀ (i : ℕ), MeasurableSet (g i)<VAR>hg₂ : Pairwise (Disjoint on g)<VAR>this : ↑v (⋃ i, g i) = ∑' (i : ℕ), ↑v (g i)<GOAL>HasSum (fun i => ↑v (f i)) (↑v (⋃ i, f i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : T2Space M<VAR>v : VectorMeasure α M<VAR>f✝ : ℕ → Set α<VAR>inst✝ : Countable β<VAR>f : β → Set α<VAR>hf₁ : ∀ (i : β), MeasurableSet (f i)<VAR>hf₂ : Pairwise (Disjoint on f)<VAR>val✝ : Encodable β<VAR>g : ℕ → Set α := fun i => ⋃ b ∈ Encodable.decode₂ β i, f b<VAR>hg : g = fun i => ⋃ b ∈ Encodable.decode₂ β i, f b<VAR>hg₁ : ∀ (i : ℕ), MeasurableSet (g i)<VAR>hg₂ : Pairwise (Disjoint on g)<VAR>this : ↑v (⋃ b, f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ b ∈ Encodable.decode₂ β i, f b) i)<GOAL>HasSum (fun i => ↑v (f i)) (↑v (⋃ i, f i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : T2Space M<VAR>v : VectorMeasure α M<VAR>f✝ : ℕ → Set α<VAR>inst✝ : Countable β<VAR>f : β → Set α<VAR>hf₁ : ∀ (i : β), MeasurableSet (f i)<VAR>hf₂ : Pairwise (Disjoint on f)<VAR>val✝ : Encodable β<VAR>g : ℕ → Set α := fun i => ⋃ b ∈ Encodable.decode₂ β i, f b<VAR>hg : g = fun i => ⋃ b ∈ Encodable.decode₂ β i, f b<VAR>hg₁ : ∀ (i : ℕ), MeasurableSet (g i)<VAR>hg₂ : Pairwise (Disjoint on g)<VAR>this : ↑v (⋃ b, f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ b ∈ Encodable.decode₂ β i, f b) i)<VAR>hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))<GOAL>HasSum (fun i => ↑v (f i)) (↑v (⋃ i, f i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : T2Space M<VAR>v : VectorMeasure α M<VAR>f✝ : ℕ → Set α<VAR>inst✝ : Countable β<VAR>f : β → Set α<VAR>hf₁ : ∀ (i : β), MeasurableSet (f i)<VAR>hf₂ : Pairwise (Disjoint on f)<VAR>val✝ : Encodable β<VAR>g : ℕ → Set α := fun i => ⋃ b ∈ Encodable.decode₂ β i, f b<VAR>hg : g = fun i => ⋃ b ∈ Encodable.decode₂ β i, f b<VAR>hg₁ : ∀ (i : ℕ), MeasurableSet (g i)<VAR>hg₂ : Pairwise (Disjoint on g)<VAR>this : ↑v (⋃ b, f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ b ∈ Encodable.decode₂ β i, f b) i)<VAR>hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))<GOAL>↑v ∅ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : T2Space M<VAR>v : VectorMeasure α M<VAR>f✝ : ℕ → Set α<VAR>inst✝ : Countable β<VAR>f : β → Set α<VAR>hf₁ : ∀ (i : β), MeasurableSet (f i)<VAR>hf₂ : Pairwise (Disjoint on f)<VAR>val✝ : Encodable β<VAR>g : ℕ → Set α := fun i => ⋃ b ∈ Encodable.decode₂ β i, f b<VAR>hg : g = fun i => ⋃ b ∈ Encodable.decode₂ β i, f b<VAR>hg₁ : ∀ (i : ℕ), MeasurableSet (g i)<VAR>hg₂ : Pairwise (Disjoint on g)<VAR>this : ↑v (⋃ b, f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ b ∈ Encodable.decode₂ β i, f b) i)<VAR>hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))<GOAL>Summable fun i => ↑v (f i)