ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p : ℕ<VAR>p_prime : Nat.Prime p<VAR>m n : ℤ<VAR>k l : ℕ<VAR>hpm : ↑(p ^ k) ∣ m<VAR>hpn : ↑(p ^ l) ∣ n<VAR>hpmn : ↑(p ^ (k + l + 1)) ∣ m * n<VAR>hpm' : p ^ k ∣ m.natAbs<VAR>hpn' : p ^ l ∣ n.natAbs<VAR>hpmn' : p ^ (k + l + 1) ∣ m.natAbs * n.natAbs<VAR>hsd : p ^ (k + 1) ∣ m.natAbs ∨ p ^ (l + 1) ∣ n.natAbs := Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul p_prime hpm' hpn' hpmn'<VAR>hsd1 : p ^ (k + 1) ∣ m.natAbs<GOAL>↑(p ^ (k + 1)) ∣ m
<VAR>p : ℕ<VAR>p_prime : Nat.Prime p<VAR>m n : ℤ<VAR>k l : ℕ<VAR>hpm : ↑(p ^ k) ∣ m<VAR>hpn : ↑(p ^ l) ∣ n<VAR>hpmn : ↑(p ^ (k + l + 1)) ∣ m * n<VAR>hpm' : p ^ k ∣ m.natAbs<VAR>hpn' : p ^ l ∣ n.natAbs<VAR>hpmn' : p ^ (k + l + 1) ∣ m.natAbs * n.natAbs<VAR>hsd : p ^ (k + 1) ∣ m.natAbs ∨ p ^ (l + 1) ∣ n.natAbs := Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul p_prime hpm' hpn' hpmn'<VAR>hsd1 : p ^ (k + 1) ∣ m.natAbs<GOAL>↑(p ^ (k + 1)) ∣ ↑m.natAbs
<VAR>p : ℕ<VAR>p_prime : Nat.Prime p<VAR>m n : ℤ<VAR>k l : ℕ<VAR>hpm : ↑(p ^ k) ∣ m<VAR>hpn : ↑(p ^ l) ∣ n<VAR>hpmn : ↑(p ^ (k + l + 1)) ∣ m * n<VAR>hpm' : p ^ k ∣ m.natAbs<VAR>hpn' : p ^ l ∣ n.natAbs<VAR>hpmn' : p ^ (k + l + 1) ∣ m.natAbs * n.natAbs<VAR>hsd : p ^ (k + 1) ∣ m.natAbs ∨ p ^ (l + 1) ∣ n.natAbs := Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul p_prime hpm' hpn' hpmn'<VAR>hsd2 : p ^ (l + 1) ∣ n.natAbs<GOAL>↑(p ^ (l + 1)) ∣ n
<VAR>p : ℕ<VAR>p_prime : Nat.Prime p<VAR>m n : ℤ<VAR>k l : ℕ<VAR>hpm : ↑(p ^ k) ∣ m<VAR>hpn : ↑(p ^ l) ∣ n<VAR>hpmn : ↑(p ^ (k + l + 1)) ∣ m * n<VAR>hpm' : p ^ k ∣ m.natAbs<VAR>hpn' : p ^ l ∣ n.natAbs<VAR>hpmn' : p ^ (k + l + 1) ∣ m.natAbs * n.natAbs<VAR>hsd : p ^ (k + 1) ∣ m.natAbs ∨ p ^ (l + 1) ∣ n.natAbs := Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul p_prime hpm' hpn' hpmn'<VAR>hsd2 : p ^ (l + 1) ∣ n.natAbs<GOAL>↑(p ^ (l + 1)) ∣ ↑n.natAbs
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ✝ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>inst✝¹ : S₁.HasHomology<VAR>inst✝ : S₂.HasHomology<VAR>φ : S₁ ⟶ S₂<GOAL>S₁.leftHomologyIso.inv ≫ leftHomologyMap φ = homologyMap φ ≫ S₂.leftHomologyIso.inv
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedRing K<VAR>inst✝ : FloorRing K<VAR>n : ℕ<VAR>a c : K<GOAL>∃ p > n, Nat.Prime p ∧ a * c ^ p < ↑(p - 1)!
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedRing K<VAR>inst✝ : FloorRing K<VAR>n : ℕ<VAR>a c : K<VAR>p : ℕ<VAR>pn : p > n<VAR>pp : Nat.Prime p<VAR>h : ⌈|a|⌉.natAbs * ⌈|c|⌉.natAbs ^ p < (p - 1)!<GOAL>∃ p > n, Nat.Prime p ∧ a * c ^ p < ↑(p - 1)!
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedRing K<VAR>inst✝ : FloorRing K<VAR>n : ℕ<VAR>a c : K<VAR>p : ℕ<VAR>pn : p > n<VAR>pp : Nat.Prime p<VAR>h : ⌈|a|⌉.natAbs * ⌈|c|⌉.natAbs ^ p < (p - 1)!<GOAL>a * c ^ p < ↑(p - 1)!
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedRing K<VAR>inst✝ : FloorRing K<VAR>n : ℕ<VAR>a c : K<VAR>p : ℕ<VAR>pn : p > n<VAR>pp : Nat.Prime p<VAR>h : ⌈|a|⌉.natAbs * ⌈|c|⌉.natAbs ^ p < (p - 1)!<GOAL>|a * c ^ p| ≤ ↑⌈|a|⌉ * ↑⌈|c|⌉ ^ p
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedRing K<VAR>inst✝ : FloorRing K<VAR>n : ℕ<VAR>a c : K<VAR>p : ℕ<VAR>pn : p > n<VAR>pp : Nat.Prime p<VAR>h : ⌈|a|⌉.natAbs * ⌈|c|⌉.natAbs ^ p < (p - 1)!<GOAL>↑⌈|a|⌉ * ↑⌈|c|⌉ ^ p = ↑(⌈|a|⌉.natAbs * ⌈|c|⌉.natAbs ^ p)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : Monoid M<VAR>inst✝ : AddMonoid N<VAR>P : AddSubmonoid N<GOAL>P.FG ↔ (toSubmonoid P).FG
<VAR>x✝ : Substring<VAR>h✝ : x✝.Valid<VAR>l m r : List Char<VAR>h : ValidFor l m r x✝<GOAL>x✝.bsize = utf8Len x✝.toString.data
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(μ.withDensity 1) s = μ s
<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : SuccOrder α<VAR>a b✝ : α<VAR>C : α → Sort u_2<VAR>hs : (a : α) → ¬IsMax a → C (succ a)<VAR>hl : (a : α) → IsSuccLimit a → C a<VAR>b : α<VAR>hb : ¬IsMax b<GOAL>isSuccLimitRecOn (succ b) hs hl = hs b hb
<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : SuccOrder α<VAR>a b✝ : α<VAR>C : α → Sort u_2<VAR>hs : (a : α) → ¬IsMax a → C (succ a)<VAR>hl : (a : α) → IsSuccLimit a → C a<VAR>b : α<VAR>hb : ¬IsMax b<VAR>hb' : ¬IsSuccLimit (succ b)<GOAL>isSuccLimitRecOn (succ b) hs hl = hs b hb
<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : SuccOrder α<VAR>a b✝ : α<VAR>C : α → Sort u_2<VAR>hs : (a : α) → ¬IsMax a → C (succ a)<VAR>hl : (a : α) → IsSuccLimit a → C a<VAR>b : α<VAR>hb : ¬IsMax b<VAR>hb' : ¬IsSuccLimit (succ b)<VAR>H : ¬IsMax (Classical.choose ⋯) ∧ succ (Classical.choose ⋯) = succ b<GOAL>isSuccLimitRecOn (succ b) hs hl = hs b hb
<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : SuccOrder α<VAR>a b✝ : α<VAR>C : α → Sort u_2<VAR>hs : (a : α) → ¬IsMax a → C (succ a)<VAR>hl : (a : α) → IsSuccLimit a → C a<VAR>b : α<VAR>hb : ¬IsMax b<VAR>hb' : ¬IsSuccLimit (succ b)<VAR>H : ¬IsMax (Classical.choose ⋯) ∧ succ (Classical.choose ⋯) = succ b<GOAL>(if hb : IsSuccLimit (succ b) then hl (succ b) hb else let_fun H := ⋯; ⋯.mpr (hs (Classical.choose ⋯) ⋯)) = hs b hb
<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : SuccOrder α<VAR>a b✝ : α<VAR>C : α → Sort u_2<VAR>hs : (a : α) → ¬IsMax a → C (succ a)<VAR>hl : (a : α) → IsSuccLimit a → C a<VAR>b : α<VAR>hb : ¬IsMax b<VAR>hb' : ¬IsSuccLimit (succ b)<VAR>H : ¬IsMax (Classical.choose ⋯) ∧ succ (Classical.choose ⋯) = succ b<GOAL>HEq (hs (Classical.choose ⋯) ⋯) (hs b hb)
<VAR>xl xr : Type u<VAR>x y : PGame<GOAL>x.IsOption (-y) ↔ (-x).IsOption y
<VAR>xl xr : Type u<VAR>x y : PGame<GOAL>((∃ i, x = (-y).moveRight i) ∨ ∃ i, x = (-y).moveLeft i) ↔ (∃ i, -x = y.moveLeft i) ∨ ∃ i, -x = y.moveRight i
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>f : α → α<VAR>n : ℕ<VAR>hf : Involutive f<VAR>hne : f ≠ id<VAR>H : f^[n] = f<VAR>hn : Even n<GOAL>f = id
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : Preorder α<VAR>a✝ b c a : α<GOAL>⋃ b, Ioc a b = Ioi a
<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>f✝ g : Filter α✝<VAR>s✝ t : Set α✝<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>α : Type u_3<VAR>f : ι → Filter α<VAR>s : Set α<GOAL>s ∈ ⨅ i, f i ↔ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ i, t i
<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>f✝ g : Filter α✝<VAR>s✝ t : Set α✝<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>α : Type u_3<VAR>f : ι → Filter α<VAR>s : Set α<GOAL>(∃ t, (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ i, t i) → s ∈ ⨅ i, f i
<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>f✝ g : Filter α✝<VAR>s t✝ : Set α✝<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>α : Type u_3<VAR>f : ι → Filter α<VAR>t : ι → Set α<VAR>ht : ∀ (i : ι), t i ∈ f i<GOAL>⋂ i, t i ∈ ⨅ i, f i
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>X : C<VAR>Y : Over X<VAR>S : Sieve Y<GOAL>S ∈ (J.over X).sieves Y ↔ (Sieve.overEquiv Y) S ∈ J.sieves Y.left
<VAR>x y : ℂ<GOAL>sin ((starRingEnd ℂ) x) = (starRingEnd ℂ) (sin x)
<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>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : Semiring R₂<VAR>inst✝⁹ : Semiring R₃<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : AddCommMonoid M₂<VAR>inst✝⁶ : AddCommMonoid M₃<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R₂ M₂<VAR>inst✝³ : Module R₃ M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>p✝ p' : Submodule R M<VAR>q✝ q' : Submodule R₂ M₂<VAR>x : M<VAR>F : Type u_9<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>p q : Submodule R M<GOAL>Disjoint p q ↔ comap p.subtype q = ⊥
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Monoid G<VAR>a b x✝ y : G<VAR>n✝ m : ℕ<VAR>η : Type u_6<VAR>Gs : η → Type u_7<VAR>inst✝ : (i : η) → Monoid (Gs i)<VAR>x : (i : η) → Gs i<VAR>h : IsOfFinOrder x<VAR>n : ℕ<VAR>npos : 0 < n<VAR>hn : x ^ n = 1<GOAL>∀ (i : η), IsOfFinOrder (x i)
<VAR>α : Type u_1<VAR>inst✝ : CommSemiring α<GOAL>fibRec.IsSolution fun x => φ ^ x
<VAR>α : Type u_1<VAR>inst✝ : CommSemiring α<GOAL>(X ^ 2 - (X + 1)).IsRoot φ
<VAR>x : ZFSet<VAR>h : ∅ ∉ x<VAR>y : ZFSet<VAR>yx : y ∈ x<VAR>n : ¬∃ y_1, y_1 ∈ y<GOAL>∅ ∈ x
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h0 : a ≠ 0<VAR>hI : a ≠ ⊤<GOAL>b / a * a = b
<VAR>k : Type u_1<VAR>inst✝³ : Field k<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : NumberField K<GOAL>card (InfinitePlace K) = NrRealPlaces K + NrComplexPlaces K
<VAR>k : Type u_1<VAR>inst✝³ : Field k<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : NumberField K<GOAL>card (InfinitePlace K) = card { x // x.IsReal ∨ x.IsComplex }
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>c : ℂ<VAR>hs : s ∈ 𝓝 c<GOAL>DifferentiableOn ℂ f (s \ {c}) ∧ ContinuousAt f c ↔ DifferentiableOn ℂ f s
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>c : ℂ<VAR>hs : s ∈ 𝓝 c<GOAL>DifferentiableOn ℂ f (s \ {c}) ∧ ContinuousAt f c → DifferentiableOn ℂ f s
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>c : ℂ<VAR>hs : s ∈ 𝓝 c<VAR>hd : DifferentiableOn ℂ f (s \ {c})<VAR>hc : ContinuousAt f c<VAR>x : ℂ<VAR>hx : x ∈ s<GOAL>DifferentiableWithinAt ℂ f s x
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>x : ℂ<VAR>hx : x ∈ s<VAR>hs : s ∈ 𝓝 x<VAR>hd : DifferentiableOn ℂ f (s \ {x})<VAR>hc : ContinuousAt f x<GOAL>DifferentiableWithinAt ℂ f s x
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>c : ℂ<VAR>hs : s ∈ 𝓝 c<VAR>hd : DifferentiableOn ℂ f (s \ {c})<VAR>hc : ContinuousAt f c<VAR>x : ℂ<VAR>hx : x ∈ s<VAR>hne : x ≠ c<GOAL>DifferentiableWithinAt ℂ f s x
<VAR>z : ℤ<VAR>hz : z ≠ 0<GOAL>|z.sign| = 1
<VAR>α✝ β✝ α : Type u<VAR>β : Type v<VAR>c : Cardinal.{max u v}<VAR>f : α → β<VAR>hf : ∀ (b : β), lift.{v, u} #↑(f ⁻¹' {b}) ≤ c<VAR>b : β<GOAL>↑(⇑Equiv.ulift '' ((fun x => { down := f x.down }) ⁻¹' {{ down := b }})) ≃ ↑(f ⁻¹' {b})
<VAR>α✝ β✝ α : Type u<VAR>β : Type v<VAR>c : Cardinal.{max u v}<VAR>f : α → β<VAR>hf : ∀ (b : β), lift.{v, u} #↑(f ⁻¹' {b}) ≤ c<VAR>b : β<GOAL>↑(⇑Equiv.ulift.symm ⁻¹' ((fun x => { down := f x.down }) ⁻¹' {{ down := b }})) ≃ ↑(f ⁻¹' {b})
<VAR>α✝ β✝ α : Type u<VAR>β : Type v<VAR>c : Cardinal.{max u v}<VAR>f : α → β<VAR>hf : ∀ (b : β), lift.{v, u} #↑(f ⁻¹' {b}) ≤ c<VAR>b : β<VAR>this : ⇑Equiv.ulift.symm = ULift.up<GOAL>↑(ULift.up ⁻¹' ((fun x => { down := f x.down }) ⁻¹' {{ down := b }})) ≃ ↑(f ⁻¹' {b})
<VAR>α✝ β✝ α : Type u<VAR>β : Type v<VAR>c : Cardinal.{max u v}<VAR>f : α → β<VAR>hf : ∀ (b : β), lift.{v, u} #↑(f ⁻¹' {b}) ≤ c<VAR>b : β<VAR>this : ⇑Equiv.ulift.symm = ULift.up<GOAL>{ x // f x = b } ≃ { x // f x = b }
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x : R<GOAL>Sbtw R 0 x 1 ↔ x ∈ Set.Ioo 0 1
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x : R<GOAL>(0 ≤ x ∧ x ≤ 1) ∧ x ≠ 0 ∧ x ≠ 1 ↔ 0 < x ∧ x < 1
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : IsFilteredOrEmpty C<VAR>α : Type w<VAR>f : α → C<GOAL>Small.{max v w, u} (FullSubcategory (FilteredClosure f))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : IsFilteredOrEmpty C<VAR>α : Type w<VAR>f : α → C<GOAL>∀ (b : FullSubcategory (FilteredClosure f)), ∃ a, CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f a = b.obj
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : IsFilteredOrEmpty C<VAR>α : Type w<VAR>f : α → C<VAR>j : C<VAR>h : FilteredClosure f j<GOAL>∃ a, CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f a = { obj := j, property := h }.obj
<VAR>x : Cardinal.{v}<VAR>m : ℕ∞<GOAL>lift.{u, v} x < ↑m ↔ x < ↑m
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u s t : Set α<GOAL>s ∪ t = ∅ ↔ s = ∅ ∧ t = ∅
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u s t : Set α<GOAL>s ∪ t ⊆ ∅ ↔ s ⊆ ∅ ∧ t ⊆ ∅
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>u v w : Fin 3 → R<GOAL>u ⬝ᵥ (crossProduct v) w = v ⬝ᵥ (crossProduct w) u
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>u v w : Fin 3 → R<GOAL>u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 + u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 + u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 = v 0 * ![w 1 * u 2 - w 2 * u 1, w 2 * u 0 - w 0 * u 2, w 0 * u 1 - w 1 * u 0] 0 + v 1 * ![w 1 * u 2 - w 2 * u 1, w 2 * u 0 - w 0 * u 2, w 0 * u 1 - w 1 * u 0] 1 + v 2 * ![w 1 * u 2 - w 2 * u 1, w 2 * u 0 - w 0 * u 2, w 0 * u 1 - w 1 * u 0] 2
<VAR>ι : Type u_2<VAR>α : ι → Type u_1<VAR>C : (i : ι) → Set (Set (α i))<VAR>f : Set ((i : ι) → α i)<GOAL>f ∈ squareCylinders C ↔ f ∈ ⋃ s, (fun t => (↑s).pi t) '' univ.pi C
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>S : Type<VAR>inst✝ : CommRing S<VAR>m : ℕ<VAR>ψ : DirichletCharacter S m<VAR>hψ : ψ.Even<GOAL>(toUnitHom ψ) (-1) = 1
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>S : Type<VAR>inst✝ : CommRing S<VAR>m : ℕ<VAR>ψ : DirichletCharacter S m<VAR>hψ : ψ.Even<GOAL>ψ ↑(-1) = ↑1
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>ν : Measure α<VAR>ι : Type u_7<VAR>m : MeasurableSpace α<VAR>f : α → G<VAR>μ : ι → Measure α<VAR>hf : Integrable f (Measure.sum μ)<GOAL>HasSum (fun i => ∫ (a : α), f a ∂μ i) (∫ (a : α), f a ∂Measure.sum μ)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>ν : Measure α<VAR>ι : Type u_7<VAR>m : MeasurableSpace α<VAR>f : α → G<VAR>μ : ι → Measure α<VAR>hf : Integrable f (Measure.sum μ)<VAR>hfi : ∀ (i : ι), Integrable f (μ i)<GOAL>HasSum (fun i => ∫ (a : α), f a ∂μ i) (∫ (a : α), f a ∂Measure.sum μ)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>ν : Measure α<VAR>ι : Type u_7<VAR>m : MeasurableSpace α<VAR>f : α → G<VAR>μ : ι → Measure α<VAR>hf : Integrable f (Measure.sum μ)<VAR>hfi : ∀ (i : ι), Integrable f (μ i)<GOAL>Tendsto (fun s => ∫ (a : α), f a ∂∑ i ∈ s, μ i) atTop (𝓝 (∫ (a : α), f a ∂Measure.sum μ))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>ν : Measure α<VAR>ι : Type u_7<VAR>m : MeasurableSpace α<VAR>f : α → G<VAR>μ : ι → Measure α<VAR>hf : Integrable f (Measure.sum μ)<VAR>hfi : ∀ (i : ι), Integrable f (μ i)<VAR>ε : ℝ<VAR>ε0 : 0 < ε<GOAL>∀ᶠ (x : Finset ι) in atTop, ∫ (a : α), f a ∂∑ i ∈ x, μ i ∈ Metric.ball (∫ (a : α), f a ∂Measure.sum μ) ε
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>ν : Measure α<VAR>ι : Type u_7<VAR>m : MeasurableSpace α<VAR>f : α → G<VAR>μ : ι → Measure α<VAR>hf : Integrable f (Measure.sum μ)<VAR>hfi : ∀ (i : ι), Integrable f (μ i)<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ↑ε<GOAL>∀ᶠ (x : Finset ι) in atTop, ∫ (a : α), f a ∂∑ i ∈ x, μ i ∈ Metric.ball (∫ (a : α), f a ∂Measure.sum μ) ↑ε
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>ν : Measure α<VAR>ι : Type u_7<VAR>m : MeasurableSpace α<VAR>f : α → G<VAR>μ : ι → Measure α<VAR>hf : Integrable f (Measure.sum μ)<VAR>hfi : ∀ (i : ι), Integrable f (μ i)<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ↑ε<VAR>hf_lt : ∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ < ⊤<GOAL>∀ᶠ (x : Finset ι) in atTop, ∫ (a : α), f a ∂∑ i ∈ x, μ i ∈ Metric.ball (∫ (a : α), f a ∂Measure.sum μ) ↑ε
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>ν : Measure α<VAR>ι : Type u_7<VAR>m : MeasurableSpace α<VAR>f : α → G<VAR>μ : ι → Measure α<VAR>hf : Integrable f (Measure.sum μ)<VAR>hfi : ∀ (i : ι), Integrable f (μ i)<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ↑ε<VAR>hf_lt : ∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ < ⊤<VAR>hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ), ∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ < y + ↑ε<GOAL>∀ᶠ (x : Finset ι) in atTop, ∫ (a : α), f a ∂∑ i ∈ x, μ i ∈ Metric.ball (∫ (a : α), f a ∂Measure.sum μ) ↑ε
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>ν : Measure α<VAR>ι : Type u_7<VAR>m : MeasurableSpace α<VAR>f : α → G<VAR>μ : ι → Measure α<VAR>hf : Integrable f (Measure.sum μ)<VAR>hfi : ∀ (i : ι), Integrable f (μ i)<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ↑ε<VAR>hf_lt : ∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ < ⊤<VAR>hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ), ∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ < y + ↑ε<VAR>s : Finset ι<VAR>hs : ∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ < ∑ b ∈ s, (fun i => ∫⁻ (a : α), ↑‖f a‖₊ ∂μ i) b + ↑ε<GOAL>∫ (a : α), f a ∂∑ i ∈ s, μ i ∈ Metric.ball (∫ (a : α), f a ∂Measure.sum μ) ↑ε
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>ν✝ : Measure α<VAR>ι : Type u_7<VAR>m : MeasurableSpace α<VAR>f : α → G<VAR>μ : ι → Measure α<VAR>hf : Integrable f (Measure.sum μ)<VAR>hfi : ∀ (i : ι), Integrable f (μ i)<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ↑ε<VAR>hf_lt : ∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ < ⊤<VAR>hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ), ∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ < y + ↑ε<VAR>s : Finset ι<VAR>hs : ∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ < ∑ b ∈ s, (fun i => ∫⁻ (a : α), ↑‖f a‖₊ ∂μ i) b + ↑ε<VAR>ν : Measure α<VAR>hν : ∑ i ∈ s, μ i + ν = Measure.sum μ<GOAL>∫ (a : α), f a ∂∑ i ∈ s, μ i ∈ Metric.ball (∫ (a : α), f a ∂Measure.sum μ) ↑ε
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>ν✝ : Measure α<VAR>ι : Type u_7<VAR>m : MeasurableSpace α<VAR>f : α → G<VAR>μ : ι → Measure α<VAR>hf : Integrable f (Measure.sum μ)<VAR>hfi : ∀ (i : ι), Integrable f (μ i)<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ↑ε<VAR>hf_lt : ∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ < ⊤<VAR>hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ), ∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ < y + ↑ε<VAR>s : Finset ι<VAR>hs : ∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ < ∑ b ∈ s, (fun i => ∫⁻ (a : α), ↑‖f a‖₊ ∂μ i) b + ↑ε<VAR>ν : Measure α<VAR>hν : ∑ i ∈ s, μ i + ν = Measure.sum μ<GOAL>↑(nndist (∫ (a : α), f a ∂∑ i ∈ s, μ i) (∫ (a : α), f a ∂(∑ i ∈ s, μ i + ν))) < ↑ε