ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁹ : MeasurableSpace X<VAR>μ : Measure X<VAR>𝕜 : Type u_5<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>L : E →L[𝕜] F<VAR>φ : X → E<VAR>φ_int : Integrable φ μ<GOAL>∀ ⦃f g : X → E⦄, f =ᶠ[ae μ] g → Integrable f μ → (fun φ => ∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)) f → (fun φ => ∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)) g
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I J : Ideal R<VAR>K L : Ideal S<VAR>r : R<VAR>hri : r ∈ I<VAR>s : R<VAR>hsj : s ∈ J<GOAL>f (r * s) ∈ map f I * map f J
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I J : Ideal R<VAR>K L : Ideal S<VAR>r : R<VAR>hri : r ∈ I<VAR>s : R<VAR>hsj : s ∈ J<GOAL>f r * f s ∈ map f I * map f J
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I J : Ideal R<VAR>K L : Ideal S<VAR>i : S<VAR>x✝¹ : i ∈ ⇑f '' ↑I<VAR>r : R<VAR>hri : r ∈ ↑I<VAR>hfri : f r = i<VAR>j : S<VAR>x✝ : j ∈ ⇑f '' ↑J<VAR>s : R<VAR>hsj : s ∈ ↑J<VAR>hfsj : f s = j<GOAL>f r * f s ∈ ↑(map f (I * J))
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I J : Ideal R<VAR>K L : Ideal S<VAR>i : S<VAR>x✝¹ : i ∈ ⇑f '' ↑I<VAR>r : R<VAR>hri : r ∈ ↑I<VAR>hfri : f r = i<VAR>j : S<VAR>x✝ : j ∈ ⇑f '' ↑J<VAR>s : R<VAR>hsj : s ∈ ↑J<VAR>hfsj : f s = j<GOAL>f (r * s) ∈ ↑(map f (I * J))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>inst✝ : Invertible 2<GOAL>2 * C ⅟2 = 1
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : Zero X<VAR>r : ℝ≥0<VAR>f : C(X, ℝ)₀<GOAL>(-(r • f)).toNNReal = r • (-f).toNNReal
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>hp : 0 < p.toReal<VAR>f : ↥(lp E p)<VAR>s : Finset α<GOAL>∑ i ∈ s, ‖↑f i‖ ^ p.toReal ≤ ‖f‖ ^ p.toReal
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>hp : 0 < p.toReal<VAR>f : ↥(lp E p)<VAR>s : Finset α<GOAL>∑ i ∈ s, ‖↑f i‖ ^ p.toReal ≤ ∑' (i : α), ‖↑f i‖ ^ p.toReal
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>hp : 0 < p.toReal<VAR>f : ↥(lp E p)<VAR>s : Finset α<VAR>this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal<GOAL>∑ i ∈ s, ‖↑f i‖ ^ p.toReal ≤ ∑' (i : α), ‖↑f i‖ ^ p.toReal
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>hp : 0 < p.toReal<VAR>f : ↥(lp E p)<VAR>s : Finset α<VAR>this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal<GOAL>Summable fun i => ‖↑f i‖ ^ p.toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f g : α → ℝ≥0∞<VAR>R : Type u_4<VAR>inst✝¹ : SMul R ℝ≥0∞<VAR>inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>a : R<GOAL>∑' (i : α), a • f i = a • ∑' (i : α), f i
<VAR>C : Type u_2<VAR>inst✝⁵ : Category.{u_1, u_2} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>S₁ S₂ S₃ S₄ : ShortComplex C<VAR>inst✝³ : S₁.HasHomology<VAR>inst✝² : S₂.HasHomology<VAR>inst✝¹ : S₃.HasHomology<VAR>inst✝ : S₄.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>φ' : S₃ ⟶ S₄<VAR>e : Arrow.mk φ ≅ Arrow.mk φ'<VAR>hφ : QuasiIso φ<VAR>α : S₃ ⟶ S₁ := e.inv.left<VAR>β : S₂ ⟶ S₄ := e.hom.right<GOAL>φ' = α ≫ φ ≫ β
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : CommRing T<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<GOAL>EssFiniteType R S ↔ ∃ σ, ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : CommRing T<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<GOAL>EssFiniteType R S ↔ ∃ σ, IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>s : Set (M ⊗[R] N)<VAR>hs : s.Finite<GOAL>∃ M', Module.Finite R ↥M' ∧ s ⊆ ↑(LinearMap.range (LinearMap.rTensor N M'.subtype))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>s : Set (M ⊗[R] N)<VAR>hs : s.Finite<VAR>M' : Submodule R M<VAR>w✝ : Submodule R N<VAR>hfin : Module.Finite R ↥M'<VAR>left✝ : Module.Finite R ↥w✝<VAR>h : s ⊆ ↑(LinearMap.range (mapIncl M' w✝))<GOAL>∃ M', Module.Finite R ↥M' ∧ s ⊆ ↑(LinearMap.range (LinearMap.rTensor N M'.subtype))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>s : Set (M ⊗[R] N)<VAR>hs : s.Finite<VAR>M' : Submodule R M<VAR>w✝ : Submodule R N<VAR>hfin : Module.Finite R ↥M'<VAR>left✝ : Module.Finite R ↥w✝<VAR>h : s ⊆ ↑(LinearMap.range (mapIncl M' w✝))<GOAL>s ⊆ ↑(LinearMap.range (LinearMap.rTensor N M'.subtype))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>s : Set (M ⊗[R] N)<VAR>hs : s.Finite<VAR>M' : Submodule R M<VAR>w✝ : Submodule R N<VAR>hfin : Module.Finite R ↥M'<VAR>left✝ : Module.Finite R ↥w✝<VAR>h : s ⊆ ↑(LinearMap.range (LinearMap.rTensor N M'.subtype ∘ₗ LinearMap.lTensor (↥M') w✝.subtype))<GOAL>s ⊆ ↑(LinearMap.range (LinearMap.rTensor N M'.subtype))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a✝ b✝ a b c : α<GOAL>Ico a c ⊆ Ico a b ∪ Ico b c
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a✝ b✝ a b c : α<GOAL>Set.Ico a c ⊆ Set.Ico a b ∪ Set.Ico b c
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D<VAR>c : C<VAR>F : C ⥤ D<VAR>d : D<VAR>f : F ⟶ (evaluationRightAdjoint D c).obj d<VAR>x : C<VAR>g : x ⟶ c<GOAL>(Pi.lift fun g => F.map g ≫ f.app c ≫ Pi.π (fun x => d) (𝟙 c)) ≫ Pi.π (fun x => d) g = f.app x ≫ Pi.π (fun x => d) g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>s : SignedMeasure α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>u v w : Set α<VAR>hu : MeasurableSet u<VAR>hv : MeasurableSet v<VAR>hw : MeasurableSet w<VAR>hsu : VectorMeasure.restrict s u ≤ VectorMeasure.restrict 0 u<VAR>hsv : VectorMeasure.restrict s v ≤ VectorMeasure.restrict 0 v<VAR>hs : ↑s (u ∆ v) = 0<GOAL>↑s (w ∩ u) = ↑s (w ∩ v)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>s : SignedMeasure α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>u v w : Set α<VAR>hu : MeasurableSet u<VAR>hv : MeasurableSet v<VAR>hw : MeasurableSet w<VAR>hsu : VectorMeasure.restrict 0 u ≤ (-s).restrict u<VAR>hsv : VectorMeasure.restrict s v ≤ VectorMeasure.restrict 0 v<VAR>hs : ↑s (u ∆ v) = 0<GOAL>↑s (w ∩ u) = ↑s (w ∩ v)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>s : SignedMeasure α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>u v w : Set α<VAR>hu : MeasurableSet u<VAR>hv : MeasurableSet v<VAR>hw : MeasurableSet w<VAR>hsu : VectorMeasure.restrict 0 u ≤ (-s).restrict u<VAR>hsv : VectorMeasure.restrict 0 v ≤ (-s).restrict v<VAR>hs : ↑s (u ∆ v) = 0<GOAL>↑s (w ∩ u) = ↑s (w ∩ v)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>s : SignedMeasure α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>u v w : Set α<VAR>hu : MeasurableSet u<VAR>hv : MeasurableSet v<VAR>hw : MeasurableSet w<VAR>hsu : VectorMeasure.restrict 0 u ≤ (-s).restrict u<VAR>hsv : VectorMeasure.restrict 0 v ≤ (-s).restrict v<VAR>hs : ↑s (u ∆ v) = 0<VAR>this : ↑(-s) (u ∆ v) = 0 → ↑(-s) (w ∩ u) = ↑(-s) (w ∩ v)<GOAL>↑s (w ∩ u) = ↑s (w ∩ v)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>s : SignedMeasure α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>u v w : Set α<VAR>hu : MeasurableSet u<VAR>hv : MeasurableSet v<VAR>hw : MeasurableSet w<VAR>hsu : VectorMeasure.restrict 0 u ≤ (-s).restrict u<VAR>hsv : VectorMeasure.restrict 0 v ≤ (-s).restrict v<VAR>hs : ↑s (u ∆ v) = 0<VAR>this : ↑s (u ∆ v) = 0 → ↑s (w ∩ u) = ↑s (w ∩ v)<GOAL>↑s (w ∩ u) = ↑s (w ∩ v)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup M₁<VAR>inst✝ : Module R M₁<VAR>I I' : R →+* R<VAR>B : M →ₗ[R] M →ₗ[R] M₁<VAR>hB : B.IsRefl<VAR>hB' : B.SeparatingLeft<GOAL>B.SeparatingRight
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup M₁<VAR>inst✝ : Module R M₁<VAR>I I' : R →+* R<VAR>B : M →ₗ[R] M →ₗ[R] M₁<VAR>hB : B.IsRefl<VAR>hB' : B.SeparatingLeft<GOAL>ker B = ⊥
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>α χ : ↥H → R<VAR>x : L<VAR>hx : x ∈ rootSpace H α<VAR>m : M<VAR>hm : m ∈ ↑(weightSpace M χ)<VAR>x' : ↥(rootSpace H α) := ⟨x, hx⟩<VAR>m' : ↥(weightSpace M χ) := ⟨m, hm⟩<GOAL>((toEnd R L M) x) m ∈ ↑(weightSpace M (α + χ))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<GOAL>map m f = ⊥ → f = ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<GOAL>∅ ∈ map m f → ∅ ∈ f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>h : f = ⊥<GOAL>map m f = ⊥
<VAR>n k : ℕ<VAR>h : k ≤ n<VAR>i j : ℕ<GOAL>i + j = n ∧ k ≤ i ↔ ∃ a, a + j = n - k ∧ a + k = i
<VAR>n k : ℕ<VAR>h : k ≤ n<VAR>i j : ℕ<VAR>hi : i + j = n ∧ k ≤ i<GOAL>i - k + j = n - k
<VAR>n k : ℕ<VAR>h : k ≤ n<VAR>i j : ℕ<GOAL>(∃ a, a + j = n - k ∧ a + k = i) → i + j = n ∧ k ≤ i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>f g : α → β<VAR>M : Type u_5<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ContinuousMul M<VAR>l✝ : Multiset (α → M)<VAR>l : List (α → M)<VAR>hl : ∀ f ∈ Quot.mk Setoid.r l, AEStronglyMeasurable f μ<GOAL>AEStronglyMeasurable (Multiset.prod (Quot.mk Setoid.r l)) μ
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>R : Type u_3<VAR>α : Type u_4<VAR>inst✝² : DivisionSemiring α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSemiring α<VAR>f g : ι → α<VAR>a a₁ a₂ : α<VAR>h : a₂ ≠ 0<VAR>H : HasSum (fun i => a₂ * f i) (a₂ * a₁)<GOAL>HasSum f a₁
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AffineSpace V P<VAR>inst✝¹ : Ring k<VAR>inst✝ : Module k V<VAR>b✝ : AffineBasis ι k P<VAR>s : Finset ι<VAR>i j : ι<VAR>e : ι ≃ ι'<VAR>v : V<VAR>b : AffineBasis ι k P<VAR>p : P<GOAL>((v +ᵥ b).coord i) p = ((b.coord i).comp ↑(AffineEquiv.constVAdd k P v).symm) p
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AffineSpace V P<VAR>inst✝¹ : Ring k<VAR>inst✝ : Module k V<VAR>b✝ : AffineBasis ι k P<VAR>s : Finset ι<VAR>i j : ι<VAR>e : ι ≃ ι'<VAR>v : V<VAR>b : AffineBasis ι k P<VAR>p : P<GOAL>(((b.basisOf i).repr (p -ᵥ (v +ᵥ b i))).sum fun x => id) = ((b.basisOf i).repr (-v +ᵥ p -ᵥ b i)).sum fun x => id
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AffineSpace V P<VAR>inst✝¹ : Ring k<VAR>inst✝ : Module k V<VAR>b✝ : AffineBasis ι k P<VAR>s : Finset ι<VAR>i j : ι<VAR>e : ι ≃ ι'<VAR>v : V<VAR>b : AffineBasis ι k P<VAR>p : P<GOAL>(b.basisOf i).repr (p -ᵥ (v +ᵥ b i)) = (b.basisOf i).repr (-v +ᵥ p -ᵥ b i)
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝¹ : Field F<VAR>W : Jacobian F<VAR>inst✝ : Nontrivial R<GOAL>W'.Nonsingular ![1, 1, 0]
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝¹ : Field F<VAR>W : Jacobian F<VAR>inst✝ : Nontrivial R<GOAL>¬(3 * 1 ^ 2 = 0 ∧ 2 * 1 = 0 ∧ W'.a₁ * 1 * 1 = 0)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>r : R<VAR>x y : M<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>p p' : Submodule R M<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝² : Ring R₂<VAR>inst✝¹ : AddCommGroup M₂<VAR>inst✝ : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<GOAL>map p.mkQ p = ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>hp : p.NeBot<VAR>hf : UniformCauchySeqOn F p s<VAR>hx : x ∈ s<GOAL>Cauchy (map (fun i => F i x) p)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>hp : p.NeBot<VAR>hf : UniformCauchySeqOn F p s<VAR>hx : x ∈ s<GOAL>Tendsto (fun p => (F p.1 x, F p.2 x)) (p ×ˢ p) (𝓤 β)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>hp : p.NeBot<VAR>hf : UniformCauchySeqOn F p s<VAR>hx : x ∈ s<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<GOAL>u ∈ map (fun p => (F p.1 x, F p.2 x)) (p ×ˢ p)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>hp : p.NeBot<VAR>hf : UniformCauchySeqOn F p s<VAR>hx : x ∈ s<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<GOAL>(fun p => (F p.1 x, F p.2 x)) ⁻¹' u ∈ p ×ˢ p
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>e : α ≃o β<GOAL>map (⇑e) atTop = atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : MeasurableSingletonClass α<VAR>f : α → E<VAR>μ : Measure α<VAR>a b : α<VAR>inst✝ : NoAtoms μ<GOAL>IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioo a b) μ
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>inst✝³ : LinearOrderedField k<VAR>inst✝² : OrderedAddCommGroup E<VAR>inst✝¹ : Module k E<VAR>inst✝ : OrderedSMul k E<VAR>a b : E<VAR>r r' : k<VAR>h : r < 1<GOAL>(lineMap a b) r ≤ b ↔ (lineMap a b) r ≤ (lineMap a b) 1
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>f : ℝ → E<VAR>g : ℝ → F<VAR>a b : ℝ<VAR>l : Filter ℝ<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : TendstoIxxClass Icc l l<VAR>hl : [[a, b]] ∈ l<VAR>hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x<VAR>hf : Tendsto (fun x => ‖f x‖) l atTop<VAR>hfg : deriv f =O[l] g<GOAL>¬IntervalIntegrable g volume a b
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>f : ℝ → E<VAR>g : ℝ → F<VAR>a b : ℝ<VAR>l : Filter ℝ<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : TendstoIxxClass Icc l l<VAR>hl : [[a, b]] ∈ l<VAR>hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x<VAR>hf : Tendsto (fun x => ‖f x‖) l atTop<VAR>hfg : deriv f =O[l] g<GOAL>¬IntegrableOn g [[a, b]] volume
<VAR>ι : Type u_1<VAR>inst✝³ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → AddCommMonoid (A i)<VAR>inst✝¹ : AddCommMonoid ι<VAR>inst✝ : GCommSemiring A<VAR>a b : ⨁ (i : ι), A i<GOAL>a * b = b * a
<VAR>ι : Type u_1<VAR>inst✝³ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → AddCommMonoid (A i)<VAR>inst✝¹ : AddCommMonoid ι<VAR>inst✝ : GCommSemiring A<VAR>a b : ⨁ (i : ι), A i<GOAL>mulHom A = (mulHom A).flip
<VAR>ι : Type u_1<VAR>inst✝³ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → AddCommMonoid (A i)<VAR>inst✝¹ : AddCommMonoid ι<VAR>inst✝ : GCommSemiring A<VAR>a b : ⨁ (i : ι), A i<GOAL>∀ (i : ι) (y : A i), (mulHom A) ((of A i) y) = (mulHom A).flip ((of A i) y)
<VAR>ι : Type u_1<VAR>inst✝³ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → AddCommMonoid (A i)<VAR>inst✝¹ : AddCommMonoid ι<VAR>inst✝ : GCommSemiring A<VAR>a b : ⨁ (i : ι), A i<VAR>ai : ι<VAR>ax : A ai<GOAL>(mulHom A) ((of A ai) ax) = (mulHom A).flip ((of A ai) ax)
<VAR>ι : Type u_1<VAR>inst✝³ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → AddCommMonoid (A i)<VAR>inst✝¹ : AddCommMonoid ι<VAR>inst✝ : GCommSemiring A<VAR>a b : ⨁ (i : ι), A i<VAR>ai : ι<VAR>ax : A ai<GOAL>∀ (i : ι) (y : A i), ((mulHom A) ((of A ai) ax)) ((of A i) y) = ((mulHom A).flip ((of A ai) ax)) ((of A i) y)
<VAR>ι : Type u_1<VAR>inst✝³ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → AddCommMonoid (A i)<VAR>inst✝¹ : AddCommMonoid ι<VAR>inst✝ : GCommSemiring A<VAR>a b : ⨁ (i : ι), A i<VAR>ai : ι<VAR>ax : A ai<VAR>bi : ι<VAR>bx : A bi<GOAL>((mulHom A) ((of A ai) ax)) ((of A bi) bx) = ((mulHom A).flip ((of A ai) ax)) ((of A bi) bx)
<VAR>ι : Type u_1<VAR>inst✝³ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → AddCommMonoid (A i)<VAR>inst✝¹ : AddCommMonoid ι<VAR>inst✝ : GCommSemiring A<VAR>a b : ⨁ (i : ι), A i<VAR>ai : ι<VAR>ax : A ai<VAR>bi : ι<VAR>bx : A bi<GOAL>(of A (ai + bi)) (GradedMonoid.GMul.mul ax bx) = (of A (bi + ai)) (GradedMonoid.GMul.mul bx ax)
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>ifp_n ifp_succ_n : IntFractPair K<VAR>nth_stream_eq : IntFractPair.stream v n = some ifp_n<VAR>succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n<GOAL>↑ifp_succ_n.b ≤ ifp_n.fr⁻¹
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>ifp_n ifp_succ_n : IntFractPair K<VAR>nth_stream_eq : IntFractPair.stream v n = some ifp_n<VAR>succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n<GOAL>↑⌊ifp_n.fr⁻¹⌋ ≤ ifp_n.fr⁻¹
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>a : α<VAR>inst✝ : DecidableEq α<GOAL>s ⋖ t ↔ ∃ a ∈ t, t.erase a = s
<VAR>a : ℤ<GOAL>a.sign * |a| = a
<VAR>𝕜 : Type u<VAR>𝕜' : Type u'<VAR>E : Type v<VAR>F : Type w<VAR>G : Type x<VAR>inst✝¹⁵ : Ring 𝕜<VAR>inst✝¹⁴ : AddCommGroup E<VAR>inst✝¹³ : Module 𝕜 E<VAR>inst✝¹² : TopologicalSpace E<VAR>inst✝¹¹ : TopologicalAddGroup E<VAR>inst✝¹⁰ : ContinuousConstSMul 𝕜 E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module 𝕜 F<VAR>inst✝⁷ : TopologicalSpace F<VAR>inst✝⁶ : TopologicalAddGroup F<VAR>inst✝⁵ : ContinuousConstSMul 𝕜 F<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module 𝕜 G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : ContinuousConstSMul 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>h : 0 < n<GOAL>p.removeZero n = p n
<VAR>𝕜 : Type u<VAR>𝕜' : Type u'<VAR>E : Type v<VAR>F : Type w<VAR>G : Type x<VAR>inst✝¹⁵ : Ring 𝕜<VAR>inst✝¹⁴ : AddCommGroup E<VAR>inst✝¹³ : Module 𝕜 E<VAR>inst✝¹² : TopologicalSpace E<VAR>inst✝¹¹ : TopologicalAddGroup E<VAR>inst✝¹⁰ : ContinuousConstSMul 𝕜 E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module 𝕜 F<VAR>inst✝⁷ : TopologicalSpace F<VAR>inst✝⁶ : TopologicalAddGroup F<VAR>inst✝⁵ : ContinuousConstSMul 𝕜 F<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module 𝕜 G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : ContinuousConstSMul 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>h : 0 < n<GOAL>p.removeZero n.pred.succ = p n.pred.succ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<GOAL>(Iic s).card = 2 ^ s.card
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X : C<GOAL>IsInitial X → False ↔ Nonempty ↑(F.obj X)
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X : C<GOAL>IsInitial X → False ↔ ¬IsEmpty ↑(F.obj X)
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X : C<VAR>h : IsInitial X → False<VAR>he : IsEmpty ↑(F.obj X)<GOAL>False
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>s✝ : Multiset α<VAR>a✝ a : α<VAR>s t : Multiset α<GOAL>a ::ₘ s ⊆ t ↔ a ∈ t ∧ s ⊆ t
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : CommMonoid α<VAR>g : γ → β<VAR>hg : Injective g<VAR>f : β → α<VAR>hf : ∀ x ∉ Set.range g, f x = 1<VAR>this : DecidableEq β<GOAL>Filter.map (fun s => ∏ i ∈ s, f (g i)) atTop = Filter.map (fun s => ∏ i ∈ s, f i) atTop
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : CommMonoid α<VAR>g : γ → β<VAR>hg : Injective g<VAR>f : β → α<VAR>hf : ∀ x ∉ Set.range g, f x = 1<VAR>this : DecidableEq β<VAR>s : Finset β<GOAL>∃ v, ∀ (v' : Finset γ), v ⊆ v' → ∃ u', s ⊆ u' ∧ ∏ x ∈ u', f x = ∏ b ∈ v', f (g b)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : CommMonoid α<VAR>g : γ → β<VAR>hg : Injective g<VAR>f : β → α<VAR>hf : ∀ x ∉ Set.range g, f x = 1<VAR>this : DecidableEq β<VAR>s : Finset γ<GOAL>∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', s ⊆ u' ∧ ∏ x ∈ u', f (g x) = ∏ b ∈ v', f b
<VAR>R : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero R<VAR>inst✝ : UniqueFactorizationMonoid R<VAR>x : R<VAR>hx : x ≠ 0<GOAL>∃ y n, Squarefree y ∧ y ∣ x ∧ x ∣ y ^ n
<VAR>R : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero R<VAR>inst✝ : UniqueFactorizationMonoid R<VAR>hx : 0 ≠ 0<GOAL>∃ y n, Squarefree y ∧ y ∣ 0 ∧ 0 ∣ y ^ n
<VAR>R : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero R<VAR>inst✝ : UniqueFactorizationMonoid R<VAR>u : R<VAR>hu : IsUnit u<VAR>hx : u ≠ 0<GOAL>∃ y n, Squarefree y ∧ y ∣ u ∧ u ∣ y ^ n
<VAR>R : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero R<VAR>inst✝ : UniqueFactorizationMonoid R<VAR>z p : R<VAR>hz : z ≠ 0<VAR>hp : Irreducible p<VAR>ih : z ≠ 0 → ∃ y n, Squarefree y ∧ y ∣ z ∧ z ∣ y ^ n<VAR>hx : p * z ≠ 0<GOAL>∃ y n, Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n