ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : LocallyRingedSpace<VAR>r✝ : ↑(Γ.obj (op X))<VAR>x : ↑↑X.toPresheafedSpace<VAR>p : PrimeSpectrum ↑(Γ.obj (op X)) := X.toΓSpecFun x<VAR>S : CommRingCat := (structureSheaf ↑(Γ.obj (op X))).presheaf.stalk p<VAR>t : ↑S<VAR>ht : IsUnit ((PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace x) t)<VAR>r : ↑(Γ.obj (op X))<VAR>s : ↥p.asIdeal.primeCompl<VAR>t' : ↑S := (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) ↑s<VAR>he : t * t' = (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) r<GOAL>IsUnit ((PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace x) t * (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace x) t')
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s t : Set α<VAR>x : α<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>E : Set α<GOAL>closure E ⊆ thickening δ E
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s t : Set α<VAR>x : α<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>E : Set α<GOAL>cthickening 0 E ⊆ thickening δ E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝¹ : CompleteLattice α<VAR>f✝ g✝ s t : ι → α<VAR>a b : α<VAR>p : ι → Prop<VAR>inst✝ : DecidablePred p<VAR>f : (i : ι) → p i → α<VAR>g : (i : ι) → ¬p i → α<GOAL>(⨆ i, if h : p i then f i h else g i h) = (⨆ i, ⨆ (h : p i), f i h) ⊔ ⨆ i, ⨆ (h : ¬p i), g i h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝¹ : CompleteLattice α<VAR>f✝ g✝ s t : ι → α<VAR>a b : α<VAR>p : ι → Prop<VAR>inst✝ : DecidablePred p<VAR>f : (i : ι) → p i → α<VAR>g : (i : ι) → ¬p i → α<GOAL>(⨆ i, if h : p i then f i h else g i h) = ⨆ x, (⨆ (h : p x), f x h) ⊔ ⨆ (h : ¬p x), g x h
<VAR>X✝ X : CondensedSet<VAR>S : CompHausᵒᵖ<VAR>x : X.val.obj S<GOAL>∀ (i : (T : CompHaus) × X.val.obj (Opposite.op T)), Continuous fun a => CondensedSet.coinducingCoprod X ⟨i, a⟩
<VAR>X✝ X : CondensedSet<VAR>S : CompHausᵒᵖ<VAR>x : X.val.obj S<GOAL>Continuous (CondensedSet.coinducingCoprod X)
<VAR>X✝ X : CondensedSet<VAR>x✝² x✝¹ : CompHausᵒᵖ<VAR>x✝ : x✝² ⟶ x✝¹<VAR>a✝ : X.val.obj x✝²<GOAL>(X.val.map x✝ ≫ (fun S x => { toFun := fun s => X.val.map (CompHaus.const (Opposite.unop S) s).op x, continuous_toFun := ⋯ }) x✝¹) a✝ = ((fun S x => { toFun := fun s => X.val.map (CompHaus.const (Opposite.unop S) s).op x, continuous_toFun := ⋯ }) x✝² ≫ X.toTopCat.toCondensedSet.val.map x✝) a✝
<VAR>X✝ X : CondensedSet<VAR>x✝² x✝¹ : CompHausᵒᵖ<VAR>x✝ : x✝² ⟶ x✝¹<VAR>a✝ : X.val.obj x✝²<GOAL>{ toFun := fun s => X.val.map (x✝ ≫ (CompHaus.const (Opposite.unop x✝¹) s).op) a✝, continuous_toFun := ⋯ } = { toFun := fun s => X.val.map (CompHaus.const (Opposite.unop x✝²) s).op a✝, continuous_toFun := ⋯ }.comp x✝.unop
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝¹⁶ : AddCommMonoid M<VAR>inst✝¹⁵ : AddCommMonoid N<VAR>inst✝¹⁴ : CommSemiring R<VAR>inst✝¹³ : CommSemiring S<VAR>inst✝¹² : Algebra R S<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module R N<VAR>inst✝⁹ : Module S N<VAR>inst✝⁸ : IsScalarTower R S N<VAR>f : M →ₗ[R] N<VAR>h✝ : IsBaseChange S f<VAR>P : Type u_2<VAR>Q✝ : Type u_3<VAR>inst✝⁷ : AddCommMonoid P<VAR>inst✝⁶ : Module R P<VAR>inst✝⁵ : AddCommMonoid Q✝<VAR>inst✝⁴ : Module S Q✝<VAR>h : IsBaseChange S f<VAR>Q : Type (max v₁ v₂ v₃)<VAR>inst✝³ : AddCommMonoid Q<VAR>inst✝² : Module R Q<VAR>inst✝¹ : Module S Q<VAR>inst✝ : IsScalarTower R S Q<VAR>g : M →ₗ[R] Q<GOAL>∃! g', ↑R g' ∘ₗ f = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Encodable α<VAR>n : ℕ<GOAL>decode₂ α n ≠ none ↔ n ∈ Set.range encode
<VAR>R : Type<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CharZero R<VAR>d : ℤ<VAR>r : { r // r * r = ↑d }<VAR>hd : ∀ (n : ℤ), d ≠ n * n<VAR>a : ℤ√d<VAR>ha : (lift r) a = 0<GOAL>a = 0
<VAR>R : Type<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CharZero R<VAR>d : ℤ<VAR>r : { r // r * r = ↑d }<VAR>hd : ∀ (n : ℤ), d ≠ n * n<VAR>a : ℤ√d<VAR>ha : (lift r) a = 0<VAR>h_inj : Function.Injective Int.cast<GOAL>a = 0
<VAR>R : Type<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CharZero R<VAR>d : ℤ<VAR>r : { r // r * r = ↑d }<VAR>hd : ∀ (n : ℤ), d ≠ n * n<VAR>a : ℤ√d<VAR>ha : (lift r) a = 0<VAR>h_inj : Function.Injective Int.cast<GOAL>(lift r) ↑a.norm = 0
<VAR>x y : ℝ<GOAL>rexp (log 1) = rexp 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : LieAlgebra.IsNilpotent R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x : L<GOAL>posFittingCompOf R M x ≤ ⨆ x, posFittingCompOf R M x
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.LeftHomologyData<VAR>inst✝ : S.HasLeftHomology<GOAL>h.π ≫ h.leftHomologyIso.inv = h.cyclesIso.inv ≫ S.leftHomologyπ
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>H1 : x ∣ z<VAR>H2 : y ∣ z<VAR>a b : R<VAR>h : a * x + b * y = 1<GOAL>x * y ∣ z
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>H1 : x ∣ z<VAR>H2 : y ∣ z<VAR>a b : R<VAR>h : a * x + b * y = 1<GOAL>x * y ∣ z * (a * x) + z * (b * y)
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>H1 : x ∣ z<VAR>H2 : y ∣ z<VAR>a b : R<VAR>h : a * x + b * y = 1<GOAL>x * y ∣ z * (a * x)
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>H1 : x ∣ z<VAR>H2 : y ∣ z<VAR>a b : R<VAR>h : a * x + b * y = 1<GOAL>x * y ∣ z * (b * y)
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_3}<GOAL>(type fun x x_1 => x < x_1).card = o.card
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>m : ℕ<GOAL>W.ΨSq (2 * (↑m + 2) + 1) = ((W.preΨ' (m + 4) * W.preΨ' (m + 2) ^ 3 * if Even m then W.Ψ₂Sq ^ 2 else 1) - W.preΨ' (m + 1) * W.preΨ' (m + 3) ^ 3 * if Even m then 1 else W.Ψ₂Sq ^ 2) ^ 2
<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝ : SemilatticeSup α✝<VAR>a b c d : α✝<VAR>α : Type u_1<VAR>A B : SemilatticeSup α<VAR>H : ∀ (x y : α), x ≤ y ↔ x ≤ y<GOAL>A = B
<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝ : SemilatticeSup α✝<VAR>a b c d : α✝<VAR>α : Type u_1<VAR>A B : SemilatticeSup α<VAR>H : ∀ (x y : α), x ≤ y ↔ x ≤ y<VAR>ss : toSup = toSup<GOAL>A = B
<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝ : SemilatticeSup α✝<VAR>a b c d : α✝<VAR>α : Type u_1<VAR>toSup✝¹ : Sup α<VAR>toPartialOrder✝¹ : PartialOrder α<VAR>le_sup_left✝¹ : ∀ (a b : α), a ≤ a ⊔ b<VAR>le_sup_right✝¹ : ∀ (a b : α), b ≤ a ⊔ b<VAR>sup_le✝¹ : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c<VAR>toSup✝ : Sup α<VAR>toPartialOrder✝ : PartialOrder α<VAR>le_sup_left✝ : ∀ (a b : α), a ≤ a ⊔ b<VAR>le_sup_right✝ : ∀ (a b : α), b ≤ a ⊔ b<VAR>sup_le✝ : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c<VAR>H : ∀ (x y : α), x ≤ y ↔ x ≤ y<VAR>ss : toSup = toSup<GOAL>mk le_sup_left✝¹ le_sup_right✝¹ sup_le✝¹ = mk le_sup_left✝ le_sup_right✝ sup_le✝
<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝ : SemilatticeSup α✝<VAR>a b c d : α✝<VAR>α : Type u_1<VAR>toSup✝¹ : Sup α<VAR>toPartialOrder✝ : PartialOrder α<VAR>le_sup_left✝¹ : ∀ (a b : α), a ≤ a ⊔ b<VAR>le_sup_right✝¹ : ∀ (a b : α), b ≤ a ⊔ b<VAR>sup_le✝¹ : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c<VAR>toSup✝ : Sup α<VAR>le_sup_left✝ : ∀ (a b : α), a ≤ a ⊔ b<VAR>le_sup_right✝ : ∀ (a b : α), b ≤ a ⊔ b<VAR>sup_le✝ : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c<VAR>H : ∀ (x y : α), x ≤ y ↔ x ≤ y<VAR>ss : toSup = toSup<GOAL>mk le_sup_left✝¹ le_sup_right✝¹ sup_le✝¹ = mk le_sup_left✝ le_sup_right✝ sup_le✝
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : TopologicalSpace H<VAR>inst✝⁷ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>inst✝⁴ : TopologicalSpace H'<VAR>inst✝³ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : ChartedSpace H' M'<VAR>x✝ : ?m.181632<VAR>inst✝ : I.Boundaryless<VAR>x : M<VAR>hx : s ∈ 𝓝 x<GOAL>↑((chartAt H x).extend I) '' s ∈ 𝓝 (↑((chartAt H x).extend I) x)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : OrderedCommGroup α<VAR>m n : ℤ<VAR>a✝ b✝ : α<VAR>hn : 0 < n<VAR>a b : α<VAR>hab : a < b<GOAL>(fun x => x ^ n) a < (fun x => x ^ n) b
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : OrderedCommGroup α<VAR>m n : ℤ<VAR>a✝ b✝ : α<VAR>hn : 0 < n<VAR>a b : α<VAR>hab : a < b<GOAL>1 < (b / a) ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>a a' : α<VAR>b : β<VAR>v : Vector α 0<VAR>f : α → β<GOAL>b ∉ (map f v).toList
<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>γ' : Type u_7<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>q : Type u_12<VAR>r : Type u_13<VAR>l' : Type u_14<VAR>m' : Type u_15<VAR>n' : Type u_16<VAR>p' : Type u_17<VAR>inst✝² : Zero α<VAR>inst✝¹ : Zero γ<VAR>inst✝ : DecidableEq l<VAR>f : α → β → γ<VAR>hf : ∀ (b : β), f 0 b = 0<VAR>a : l → α<VAR>B : Matrix m n β<VAR>i₁ : l<VAR>i₂ : m<VAR>j₁ : l<VAR>j₂ : n<GOAL>kroneckerMap f (diagonal a) B (i₁, i₂) (j₁, j₂) = (reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (blockDiagonal fun i => B.map fun b => f (a i) b) (i₁, i₂) (j₁, j₂)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : Preadditive D<VAR>n i i' : ℤ<VAR>hi : n + i = i'<VAR>K : CochainComplex C ℤ<GOAL>i + n = i'
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁵ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝⁴ : TopologicalSpace M''<VAR>inst✝³ : ChartedSpace H'' M''<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SmoothManifoldWithCorners I' M'<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>e : PartialHomeomorph M H<VAR>p q : TangentBundle I M<VAR>h : q.proj ∈ (chartAt H p.proj).source<GOAL>{ proj := ↑(chartAt H p.proj) q.proj, snd := (mfderiv I I (↑(chartAt H p.proj)) q.proj) q.snd } = (TotalSpace.toProd H E).symm (↑(chartAt (ModelProd H E) p) q)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁵ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝⁴ : TopologicalSpace M''<VAR>inst✝³ : ChartedSpace H'' M''<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SmoothManifoldWithCorners I' M'<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>e : PartialHomeomorph M H<VAR>p q : TangentBundle I M<VAR>h : q.proj ∈ (chartAt H p.proj).source<GOAL>{ proj := ↑(chartAt H p.proj) q.proj, snd := (fderivWithin 𝕜 (writtenInExtChartAt I I q.proj ↑(chartAt H p.proj)) (range ↑I) (↑(extChartAt I q.proj) q.proj)) q.snd } = (TotalSpace.toProd H E).symm (↑(chartAt (ModelProd H E) p) q)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁵ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝⁴ : TopologicalSpace M''<VAR>inst✝³ : ChartedSpace H'' M''<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SmoothManifoldWithCorners I' M'<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>e : PartialHomeomorph M H<VAR>p q : TangentBundle I M<VAR>h : q.proj ∈ (chartAt H p.proj).source<GOAL>MDifferentiableAt I I (↑(chartAt H p.proj)) q.proj
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : StandardBorelSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>this : UpgradedStandardBorel α := upgradeStandardBorel α<GOAL>∃ x, BorelSpace α ∧ PolishSpace α ∧ IsClosed s ∧ IsOpen s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : StandardBorelSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>this : UpgradedStandardBorel α := upgradeStandardBorel α<VAR>t : TopologicalSpace α<VAR>hle : t ≤ UpgradedStandardBorel.toTopologicalSpace<VAR>ht : PolishSpace α<VAR>s_clopen : IsClosed s ∧ IsOpen s<GOAL>∃ x, BorelSpace α ∧ PolishSpace α ∧ IsClosed s ∧ IsOpen s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : StandardBorelSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>this : UpgradedStandardBorel α := upgradeStandardBorel α<VAR>t : TopologicalSpace α<VAR>hle : t ≤ UpgradedStandardBorel.toTopologicalSpace<VAR>ht : PolishSpace α<VAR>s_clopen : IsClosed s ∧ IsOpen s<GOAL>inst✝¹ = borel α
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : StandardBorelSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>this : UpgradedStandardBorel α := upgradeStandardBorel α<VAR>t : TopologicalSpace α<VAR>hle : t ≤ UpgradedStandardBorel.toTopologicalSpace<VAR>ht : PolishSpace α<VAR>s_clopen : IsClosed s ∧ IsOpen s<GOAL>PolishSpace α
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : AddCommMonoid γ<VAR>S : ι → AddSubmonoid γ<GOAL>iSup S = AddMonoidHom.mrange (sumAddHom fun i => (S i).subtype)
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : AddCommMonoid γ<VAR>S : ι → AddSubmonoid γ<GOAL>iSup S ≤ AddMonoidHom.mrange (sumAddHom fun i => (S i).subtype)
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : AddCommMonoid γ<VAR>S : ι → AddSubmonoid γ<GOAL>AddMonoidHom.mrange (sumAddHom fun i => (S i).subtype) ≤ iSup S
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X Y : C<VAR>inst✝¹ : HasTerminal C<VAR>P : C<VAR>inst✝ : HasBinaryProduct P (⊤_ C)<GOAL>fst ≫ lift (𝟙 P) (terminal.from P) = 𝟙 (P ⨯ ⊤_ C)
<VAR>n✝ : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsDomain B<VAR>ζ : B<VAR>n : ℕ+<VAR>hζ : IsPrimitiveRoot ζ ↑n<GOAL>adjoin A ((cyclotomic (↑n) A).rootSet B) = adjoin A {b | ∃ a ∈ {n}, b ^ ↑a = 1}
<VAR>n✝ : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsDomain B<VAR>ζ : B<VAR>n : ℕ+<VAR>hζ : IsPrimitiveRoot ζ ↑n<GOAL>adjoin A ((cyclotomic (↑n) A).rootSet B) = adjoin A {b | b ^ ↑n = 1}
<VAR>n✝ : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsDomain B<VAR>ζ : B<VAR>n : ℕ+<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>x : B<VAR>hx : x ∈ (cyclotomic (↑n) A).rootSet B<GOAL>x ∈ {b | b ^ ↑n = 1}
<VAR>n✝ : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsDomain B<VAR>ζ : B<VAR>n : ℕ+<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>x : B<VAR>hx : x ∈ {b | b ^ ↑n = 1}<GOAL>x ∈ ↑(adjoin A ((cyclotomic (↑n) A).rootSet B))
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>a : α<GOAL>(if a ≤ a then (eVariationOn f (s ∩ Icc a a)).toReal else -(eVariationOn f (s ∩ Icc a a)).toReal) = 0
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>a : α<GOAL>(s ∩ {a}).Subsingleton
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t : Set α<VAR>f✝ g : α → ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α → ℝ≥0∞<GOAL>μ univ * ⨍⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t : Set α<VAR>f✝ g : α → ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α → ℝ≥0∞<VAR>hμ : μ = 0<GOAL>μ univ * ⨍⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t : Set α<VAR>f✝ g : α → ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α → ℝ≥0∞<VAR>hμ : μ ≠ 0<GOAL>μ univ * ⨍⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>a : ℝ<VAR>h : ∀ (ε : ℝ), 0 < ε → ∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f vol π) y ≤ a * ε<GOAL>HasIntegral I l f vol y
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>a : ℝ<VAR>h : ∀ (ε : ℝ), 0 < ε → ∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f vol π) y ≤ a * ε<VAR>ε : ℝ<VAR>hε : ε > 0<GOAL>∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f vol π) y ≤ ε
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>a : ℝ<VAR>h : ∀ (ε : ℝ), 0 < ε → ∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f vol π) y ≤ a * ε<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>ε' : ℝ<VAR>hε' : 0 < ε'<VAR>ha : a * ε' < ε<GOAL>∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f vol π) y ≤ ε
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : M.Basis I X<VAR>hY : I ⊆ Y<VAR>h : M.closure X = M.closure Y<VAR>hYE : autoParam (Y ⊆ M.E) _auto✝<GOAL>M.Basis I Y
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : M.Basis I X<VAR>hY : I ⊆ Y<VAR>h : M.closure X = M.closure Y<VAR>hYE : autoParam (Y ⊆ M.E) _auto✝<GOAL>Y ⊆ M.closure I
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : M.Basis I X<VAR>hY : I ⊆ Y<VAR>h : M.closure X = M.closure Y<VAR>hYE : autoParam (Y ⊆ M.E) _auto✝<GOAL>Y ⊆ M.closure Y
<VAR>J : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>F : J ⥤ C<VAR>inst✝² : HasColimitsOfShape J C<VAR>G : J ⥤ C<VAR>α : F ⟶ G<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : HasColimitsOfShape J D<VAR>H : C ⥤ D<VAR>j✝ : J<GOAL>ι (F ⋙ H) j✝ ≫ post F H ≫ H.map (colim.map α) = ι (F ⋙ H) j✝ ≫ colim.map (whiskerRight α H) ≫ post G H
<VAR>J : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>F : J ⥤ C<VAR>inst✝² : HasColimitsOfShape J C<VAR>G : J ⥤ C<VAR>α : F ⟶ G<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : HasColimitsOfShape J D<VAR>H : C ⥤ D<VAR>j✝ : J<GOAL>H.map (α.app j✝) ≫ H.map (ι G j✝) = ι (F ⋙ H) j✝ ≫ colim.map (whiskerRight α H) ≫ post G H
<VAR>J : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>F : J ⥤ C<VAR>inst✝² : HasColimitsOfShape J C<VAR>G : J ⥤ C<VAR>α : F ⟶ G<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : HasColimitsOfShape J D<VAR>H : C ⥤ D<VAR>j✝ : J<GOAL>H.map (α.app j✝) ≫ H.map (ι G j✝) = (whiskerRight α H).app j✝ ≫ H.map (ι G j✝)
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : Group G<VAR>k p : ℕ<VAR>hp : Nat.Prime p<VAR>h : IsPGroup p G<VAR>H : Subgroup G<VAR>hk : k ≤ Nat.card ↥H<VAR>hk₀ : k ≠ 0<GOAL>∃ H' ≤ H, Nat.card ↥H' ≤ k ∧ k < p * Nat.card ↥H'
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : Group G<VAR>k p : ℕ<VAR>hp : Nat.Prime p<VAR>h : IsPGroup p G<VAR>H : Subgroup G<VAR>hk : k ≤ Nat.card ↥H<VAR>hk₀ : k ≠ 0<VAR>m : ℕ<VAR>hmk : p ^ m ≤ k<VAR>hkm : k < p ^ (m + 1)<GOAL>∃ H' ≤ H, Nat.card ↥H' ≤ k ∧ k < p * Nat.card ↥H'
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : Group G<VAR>k p : ℕ<VAR>hp : Nat.Prime p<VAR>h : IsPGroup p G<VAR>H : Subgroup G<VAR>hk : k ≤ Nat.card ↥H<VAR>hk₀ : k ≠ 0<VAR>m : ℕ<VAR>hmk : p ^ m ≤ k<VAR>hkm : k < p ^ (m + 1)<VAR>H' : Subgroup G<VAR>H'H : H' ≤ H<VAR>H'card : Nat.card ↥H' = p ^ m<GOAL>∃ H' ≤ H, Nat.card ↥H' ≤ k ∧ k < p * Nat.card ↥H'
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : Group G<VAR>k p : ℕ<VAR>hp : Nat.Prime p<VAR>h : IsPGroup p G<VAR>H : Subgroup G<VAR>hk : k ≤ Nat.card ↥H<VAR>hk₀ : k ≠ 0<VAR>m : ℕ<VAR>hmk : p ^ m ≤ k<VAR>hkm : k < p ^ (m + 1)<VAR>H' : Subgroup G<VAR>H'H : H' ≤ H<VAR>H'card : Nat.card ↥H' = p ^ m<GOAL>Nat.card ↥H' ≤ k ∧ k < p * Nat.card ↥H'