ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<VAR>hs : (o.oangle x (x + y)).sign = 1<GOAL>o.oangle x (x + y) = ↑(Real.arccos (‖x‖ / ‖x + y‖))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Semiring R<VAR>h_comm : Commute x y<VAR>n : ℕ<VAR>hn : x ^ n = 0<GOAL>IsNilpotent (x * y)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Semiring R<VAR>h_comm : Commute x y<VAR>n : ℕ<VAR>hn : x ^ n = 0<GOAL>(x * y) ^ n = 0
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B I X R✝ J : Set α<VAR>h : I ⊆ E<VAR>R : Set α<GOAL>uniqueBaseOn I E ↾ R = uniqueBaseOn (I ∩ R) R
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>Fintype.card ↑(Set.Ioc a b) = ↑b - ↑a
<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>A : C<VAR>inst✝² : S.HasHomology<VAR>inst✝¹ : S₁.HasHomology<VAR>inst✝ : S₂.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.RightHomologyData<GOAL>h₁.π ≫ (leftHomologyMap' (𝟙 S₁) h₁ S₁.leftHomologyData ≫ leftHomologyMap' (𝟙 S₁) S₁.leftHomologyData S₁.homologyData.left) ≫ leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left ≫ ((S₂.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S₂) S₂.homologyData.right S₂.rightHomologyData) ≫ rightHomologyMap' (𝟙 S₂) S₂.rightHomologyData h₂) ≫ h₂.ι = h₁.i ≫ φ.τ₂ ≫ h₂.p
<VAR>n : ℕ<VAR>n_large : 2 < n<VAR>no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n<GOAL>n.centralBinom = ∏ p ∈ Finset.range (2 * n / 3 + 1), p ^ n.centralBinom.factorization p
<VAR>n : ℕ<VAR>n_large : 2 < n<VAR>no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n<GOAL>∏ p ∈ Finset.range (2 * n / 3 + 1), p ^ n.centralBinom.factorization p = ∏ p ∈ Finset.range (2 * n + 1), p ^ n.centralBinom.factorization p
<VAR>n : ℕ<VAR>n_large : 2 < n<VAR>no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n<GOAL>Finset.range (2 * n / 3 + 1) ⊆ Finset.range (2 * n + 1)
<VAR>n : ℕ<VAR>n_large : 2 < n<VAR>no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n<GOAL>∀ x ∈ Finset.range (2 * n + 1), x ∉ Finset.range (2 * n / 3 + 1) → x ^ n.centralBinom.factorization x = 1
<VAR>n : ℕ<VAR>n_large : 2 < n<VAR>no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n<VAR>x : ℕ<VAR>hx : x ∈ Finset.range (2 * n + 1)<VAR>h2x : x ∉ Finset.range (2 * n / 3 + 1)<GOAL>x ^ n.centralBinom.factorization x = 1
<VAR>n : ℕ<VAR>n_large : 2 < n<VAR>no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n<VAR>x : ℕ<VAR>hx : x ≤ 2 * n<VAR>h2x : ¬x ≤ 2 * n / 3<GOAL>x ^ n.centralBinom.factorization x = 1
<VAR>n : ℕ<VAR>n_large : 2 < n<VAR>no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n<VAR>x : ℕ<VAR>hx : x ≤ 2 * n<VAR>h2x : 2 * n < 3 * x<GOAL>x ^ n.centralBinom.factorization x = 1
<VAR>n : ℕ<VAR>n_large : 2 < n<VAR>x : ℕ<VAR>hx : x ≤ 2 * n<VAR>h2x : 2 * n < 3 * x<VAR>no_prime : ¬(Nat.Prime x ∧ n < x ∧ x ≤ 2 * n)<GOAL>x ^ n.centralBinom.factorization x = 1
<VAR>n : ℕ<VAR>n_large : 2 < n<VAR>x : ℕ<VAR>hx : x ≤ 2 * n<VAR>h2x : 2 * n < 3 * x<VAR>no_prime : x ≤ 2 * n → ¬Nat.Prime x ∨ x ≤ n<GOAL>x ^ n.centralBinom.factorization x = 1
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝² : Group G<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Finite (Sylow p G)<VAR>P : Sylow p G<VAR>hn : (↑P).normalizer.Normal<GOAL>(↑P).Normal
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>n : ℕ<VAR>ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n<VAR>h : p.leadingCoeff ^ n.succ ≠ 0<GOAL>(p ^ n.succ).leadingCoeff = p.leadingCoeff ^ n.succ
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>n : ℕ<VAR>ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n<VAR>h : p.leadingCoeff ^ n.succ ≠ 0<VAR>h₁ : p.leadingCoeff ^ n ≠ 0<GOAL>(p ^ n.succ).leadingCoeff = p.leadingCoeff ^ n.succ
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>n : ℕ<VAR>ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n<VAR>h : p.leadingCoeff ^ n.succ ≠ 0<VAR>h₁ : p.leadingCoeff ^ n ≠ 0<VAR>h₂ : p.leadingCoeff * (p ^ n).leadingCoeff ≠ 0<GOAL>(p ^ n.succ).leadingCoeff = p.leadingCoeff ^ n.succ
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P : MorphismProperty C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : P.universally f<GOAL>P f
<VAR>n m k : ℕ<VAR>h : m ∈ n.smoothNumbers<VAR>h' : k ∣ m<GOAL>k ∈ n.smoothNumbers
<VAR>n m k : ℕ<VAR>h' : k ∣ m<VAR>h : m ∈ factoredNumbers (Finset.range n)<GOAL>k ∈ factoredNumbers (Finset.range n)
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝³ : TopologicalSpace H<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>inst✝ : HasGroupoid M G<VAR>s U V : Opens M<VAR>hUV : U ≤ V<VAR>x : ↥U<VAR>e : PartialHomeomorph M H := chartAt H ↑x<GOAL>↑(chartAt H (inclusion hUV x)).symm =ᶠ[𝓝 (↑(chartAt H (inclusion hUV x)) (inclusion hUV x))] inclusion hUV ∘ ↑(chartAt H x).symm
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝³ : TopologicalSpace H<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>inst✝ : HasGroupoid M G<VAR>s U V : Opens M<VAR>hUV : U ≤ V<VAR>x : ↥U<VAR>e : PartialHomeomorph M H := chartAt H ↑x<VAR>heUx_nhds : (e.subtypeRestr ⋯).target ∈ 𝓝 (↑e ↑x)<GOAL>↑(chartAt H (inclusion hUV x)).symm =ᶠ[𝓝 (↑(chartAt H (inclusion hUV x)) (inclusion hUV x))] inclusion hUV ∘ ↑(chartAt H x).symm
<VAR>l : List ℕ<VAR>a m n✝ n : ℕ<GOAL>(map fib n.zeckendorf).sum = n
<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✝¹ : Group G<VAR>inst✝ : Finite G<VAR>x y : G<VAR>m n : ℤ<GOAL>x ^ m = x ^ n ↔ m ≡ n [ZMOD ↑(orderOf x)]
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>H1 : IsCoprime x z<VAR>H2 : x ∣ y * z<VAR>a b : R<VAR>H : a * x + b * z = 1<GOAL>x ∣ y
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>H1 : IsCoprime x z<VAR>H2 : x ∣ y * z<VAR>a b : R<VAR>H : a * x + b * z = 1<GOAL>x ∣ y * a * x + b * (y * z)
<VAR>y : ℝ<VAR>hy : 0 < y<GOAL>Tendsto (fun x => x ^ y) atTop atTop
<VAR>y : ℝ<VAR>hy : 0 < y<GOAL>∀ (b : ℝ), ∃ i, ∀ (a : ℝ), i ≤ a → b ≤ a ^ y
<VAR>y : ℝ<VAR>hy : 0 < y<VAR>b : ℝ<GOAL>∃ i, ∀ (a : ℝ), i ≤ a → b ≤ a ^ y
<VAR>y : ℝ<VAR>hy : 0 < y<VAR>b : ℝ<GOAL>∀ (a : ℝ), max b 0 ^ (1 / y) ≤ a → b ≤ a ^ y
<VAR>y : ℝ<VAR>hy : 0 < y<VAR>b x : ℝ<VAR>hx : max b 0 ^ (1 / y) ≤ x<GOAL>b ≤ x ^ y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁷ : Norm E<VAR>inst✝¹⁶ : Norm F<VAR>inst✝¹⁵ : Norm G<VAR>inst✝¹⁴ : SeminormedAddCommGroup E'<VAR>inst✝¹³ : SeminormedAddCommGroup F'<VAR>inst✝¹² : SeminormedAddCommGroup G'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedAddCommGroup G''<VAR>inst✝⁸ : SeminormedRing R<VAR>inst✝⁷ : SeminormedAddGroup E'''<VAR>inst✝⁶ : SeminormedRing R'<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝³ : Module R E'<VAR>inst✝² : BoundedSMul R E'<VAR>inst✝¹ : Module 𝕜' F'<VAR>inst✝ : BoundedSMul 𝕜' F'<VAR>k₁ : α → R<VAR>k₂ : α → 𝕜'<VAR>h₁ : k₁ =O[l] k₂<VAR>h₂ : f' =o[l] g'<GOAL>(fun x => k₁ x • f' x) =o[l] fun x => k₂ x • g' x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁷ : Norm E<VAR>inst✝¹⁶ : Norm F<VAR>inst✝¹⁵ : Norm G<VAR>inst✝¹⁴ : SeminormedAddCommGroup E'<VAR>inst✝¹³ : SeminormedAddCommGroup F'<VAR>inst✝¹² : SeminormedAddCommGroup G'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedAddCommGroup G''<VAR>inst✝⁸ : SeminormedRing R<VAR>inst✝⁷ : SeminormedAddGroup E'''<VAR>inst✝⁶ : SeminormedRing R'<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝³ : Module R E'<VAR>inst✝² : BoundedSMul R E'<VAR>inst✝¹ : Module 𝕜' F'<VAR>inst✝ : BoundedSMul 𝕜' F'<VAR>k₁ : α → R<VAR>k₂ : α → 𝕜'<VAR>h₁ : k₁ =O[l] k₂<VAR>h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f' g'<GOAL>∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun x => k₁ x • f' x) fun x => k₂ x • g' x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁷ : Norm E<VAR>inst✝¹⁶ : Norm F<VAR>inst✝¹⁵ : Norm G<VAR>inst✝¹⁴ : SeminormedAddCommGroup E'<VAR>inst✝¹³ : SeminormedAddCommGroup F'<VAR>inst✝¹² : SeminormedAddCommGroup G'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedAddCommGroup G''<VAR>inst✝⁸ : SeminormedRing R<VAR>inst✝⁷ : SeminormedAddGroup E'''<VAR>inst✝⁶ : SeminormedRing R'<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝³ : Module R E'<VAR>inst✝² : BoundedSMul R E'<VAR>inst✝¹ : Module 𝕜' F'<VAR>inst✝ : BoundedSMul 𝕜' F'<VAR>k₁ : α → R<VAR>k₂ : α → 𝕜'<VAR>h₁ : k₁ =O[l] k₂<VAR>h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f' g'<VAR>c : ℝ<VAR>cpos : 0 < c<GOAL>IsBigOWith c l (fun x => k₁ x • f' x) fun x => k₂ x • g' x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁷ : Norm E<VAR>inst✝¹⁶ : Norm F<VAR>inst✝¹⁵ : Norm G<VAR>inst✝¹⁴ : SeminormedAddCommGroup E'<VAR>inst✝¹³ : SeminormedAddCommGroup F'<VAR>inst✝¹² : SeminormedAddCommGroup G'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedAddCommGroup G''<VAR>inst✝⁸ : SeminormedRing R<VAR>inst✝⁷ : SeminormedAddGroup E'''<VAR>inst✝⁶ : SeminormedRing R'<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : NormedDivisionRing 𝕜'<VAR>c✝ c'✝ c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝³ : Module R E'<VAR>inst✝² : BoundedSMul R E'<VAR>inst✝¹ : Module 𝕜' F'<VAR>inst✝ : BoundedSMul 𝕜' F'<VAR>k₁ : α → R<VAR>k₂ : α → 𝕜'<VAR>h₁ : k₁ =O[l] k₂<VAR>h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f' g'<VAR>c : ℝ<VAR>cpos : 0 < c<VAR>c' : ℝ<VAR>c'pos : c' > 0<VAR>hc' : IsBigOWith c' l k₁ k₂<GOAL>IsBigOWith c l (fun x => k₁ x • f' x) fun x => k₂ x • g' x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α ⊕ β<GOAL>x.getRight? = none ↔ x.isLeft = true
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>(p - 1) * padicValNat p n ! = n - (p.digits n).sum
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>(p - 1) * ∑ i ∈ Finset.Ico 1 (log p n).succ.succ, n / p ^ i = n - (p.digits n).sum
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>(p - 1) * ∑ i ∈ Finset.Ico (0 + 1) (log p n).succ.succ, n / p ^ i = n - (p.digits n).sum
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>a : ZNum<GOAL>↑(0 + a) = ↑0 + ↑a
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>b : ZNum<GOAL>↑(b + 0) = ↑b + ↑0
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>a b : PosNum<GOAL>↑(pos a + neg b) = ↑(pos a) + ↑(neg b)
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>a b : PosNum<GOAL>↑b + -↑a = -↑a + ↑b
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>a b : PosNum<GOAL>↑↑b + ↑(-↑a) = ↑(-↑a + ↑b)
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>a b : PosNum<GOAL>-↑(a + b) = -↑a + -↑b
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra A B<VAR>inst✝¹ : Module.Free A B<VAR>inst✝ : Module.Finite A B<VAR>a : A<VAR>x : B<GOAL>∃ r, (norm A) (1 + a • x) = 1 + (trace A B) x * a + r * a ^ 2
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace β<VAR>μ : ProbabilityMeasure α<VAR>ν : ProbabilityMeasure β<GOAL>(μ.prod ν).map ⋯ = μ
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace β<VAR>μ : ProbabilityMeasure α<VAR>ν : ProbabilityMeasure β<GOAL>↑((μ.prod ν).map ⋯) = ↑μ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>s✝ : Finset ι<VAR>f : ι → Set α<VAR>a : ι<VAR>s : Finset ι<VAR>ha : a ∉ s<VAR>hs : (s.sup f).PartiallyWellOrderedOn r ↔ ∀ i ∈ s, (f i).PartiallyWellOrderedOn r<GOAL>((cons a s ha).sup f).PartiallyWellOrderedOn r ↔ ∀ i ∈ cons a s ha, (f i).PartiallyWellOrderedOn r
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra 𝕜 A<VAR>inst✝ : IsAlgClosed 𝕜<VAR>a : A<VAR>p : 𝕜[X]<VAR>hdeg : 0 < p.degree<GOAL>σ ((aeval a) p) = (fun x => eval x p) '' σ a
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra 𝕜 A<VAR>inst✝ : IsAlgClosed 𝕜<VAR>a : A<VAR>p : 𝕜[X]<VAR>hdeg : 0 < p.degree<VAR>k : 𝕜<VAR>hk : k ∈ σ ((aeval a) p)<GOAL>k ∈ (fun x => eval x p) '' σ a
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra 𝕜 A<VAR>inst✝ : IsAlgClosed 𝕜<VAR>a : A<VAR>p : 𝕜[X]<VAR>hdeg : 0 < p.degree<VAR>k : 𝕜<VAR>hk : k ∈ σ ((aeval a) p)<VAR>hprod : C k - p = C (C k - p).leadingCoeff * (Multiset.map (fun a => X - C a) (C k - p).roots).prod<GOAL>k ∈ (fun x => eval x p) '' σ a
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra 𝕜 A<VAR>inst✝ : IsAlgClosed 𝕜<VAR>a : A<VAR>p : 𝕜[X]<VAR>hdeg : 0 < p.degree<VAR>k : 𝕜<VAR>hk : k ∈ σ ((aeval a) p)<VAR>hprod : C k - p = C (C k - p).leadingCoeff * (Multiset.map (fun a => X - C a) (C k - p).roots).prod<VAR>h_ne : C k - p ≠ 0<GOAL>k ∈ (fun x => eval x p) '' σ a
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra 𝕜 A<VAR>inst✝ : IsAlgClosed 𝕜<VAR>a : A<VAR>p : 𝕜[X]<VAR>hdeg : 0 < p.degree<VAR>k : 𝕜<VAR>hk : k ∈ σ ((aeval a) p)<VAR>hprod : C k - p = C (C k - p).leadingCoeff * (Multiset.map (fun a => X - C a) (C k - p).roots).prod<VAR>h_ne : C k - p ≠ 0<VAR>lead_ne : (C k - p).leadingCoeff ≠ 0<GOAL>k ∈ (fun x => eval x p) '' σ a
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra 𝕜 A<VAR>inst✝ : IsAlgClosed 𝕜<VAR>a : A<VAR>p : 𝕜[X]<VAR>hdeg : 0 < p.degree<VAR>k : 𝕜<VAR>hk : k ∈ σ ((aeval a) p)<VAR>hprod : C k - p = C (C k - p).leadingCoeff * (Multiset.map (fun a => X - C a) (C k - p).roots).prod<VAR>h_ne : C k - p ≠ 0<VAR>lead_ne : (C k - p).leadingCoeff ≠ 0<VAR>lead_unit : IsUnit ↑((Units.map ↑↑ₐ) (Units.mk0 (C k - p).leadingCoeff lead_ne))<GOAL>k ∈ (fun x => eval x p) '' σ a
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra 𝕜 A<VAR>inst✝ : IsAlgClosed 𝕜<VAR>a : A<VAR>p : 𝕜[X]<VAR>hdeg : 0 < p.degree<VAR>k : 𝕜<VAR>hk : k ∈ σ ((aeval a) p)<VAR>hprod : C k - p = C (C k - p).leadingCoeff * (Multiset.map (fun a => X - C a) (C k - p).roots).prod<VAR>h_ne : C k - p ≠ 0<VAR>lead_ne : (C k - p).leadingCoeff ≠ 0<VAR>lead_unit : IsUnit ↑((Units.map ↑↑ₐ) (Units.mk0 (C k - p).leadingCoeff lead_ne))<VAR>p_a_eq : (aeval a) (C k - p) = ↑ₐ k - (aeval a) p<GOAL>k ∈ (fun x => eval x p) '' σ a
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra 𝕜 A<VAR>inst✝ : IsAlgClosed 𝕜<VAR>a : A<VAR>p : 𝕜[X]<VAR>hdeg : 0 < p.degree<VAR>k : 𝕜<VAR>hk : ¬(IsUnit (↑ₐ (C k - p).leadingCoeff) ∧ IsUnit ((aeval a) (Multiset.map (fun a => X - C a) (C k - p).roots).prod))<VAR>hprod : C k - p = C (C k - p).leadingCoeff * (Multiset.map (fun a => X - C a) (C k - p).roots).prod<VAR>h_ne : C k - p ≠ 0<VAR>lead_ne : (C k - p).leadingCoeff ≠ 0<VAR>lead_unit : IsUnit ↑((Units.map ↑↑ₐ) (Units.mk0 (C k - p).leadingCoeff lead_ne))<VAR>p_a_eq : (aeval a) (C k - p) = ↑ₐ k - (aeval a) p<GOAL>k ∈ (fun x => eval x p) '' σ a
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra 𝕜 A<VAR>inst✝ : IsAlgClosed 𝕜<VAR>a : A<VAR>p : 𝕜[X]<VAR>hdeg : 0 < p.degree<VAR>k : 𝕜<VAR>hprod : C k - p = C (C k - p).leadingCoeff * (Multiset.map (fun a => X - C a) (C k - p).roots).prod<VAR>h_ne : C k - p ≠ 0<VAR>lead_ne : (C k - p).leadingCoeff ≠ 0<VAR>lead_unit : IsUnit ↑((Units.map ↑↑ₐ) (Units.mk0 (C k - p).leadingCoeff lead_ne))<VAR>p_a_eq : (aeval a) (C k - p) = ↑ₐ k - (aeval a) p<VAR>hk : ∃ k_1 ∈ σ a, eval k_1 (C k - p) = 0<GOAL>k ∈ (fun x => eval x p) '' σ a
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra 𝕜 A<VAR>inst✝ : IsAlgClosed 𝕜<VAR>a : A<VAR>p : 𝕜[X]<VAR>hdeg : 0 < p.degree<VAR>k : 𝕜<VAR>hprod : C k - p = C (C k - p).leadingCoeff * (Multiset.map (fun a => X - C a) (C k - p).roots).prod<VAR>h_ne : C k - p ≠ 0<VAR>lead_ne : (C k - p).leadingCoeff ≠ 0<VAR>lead_unit : IsUnit ↑((Units.map ↑↑ₐ) (Units.mk0 (C k - p).leadingCoeff lead_ne))<VAR>p_a_eq : (aeval a) (C k - p) = ↑ₐ k - (aeval a) p<VAR>r : 𝕜<VAR>r_mem : r ∈ σ a<VAR>r_ev : eval r (C k - p) = 0<GOAL>k ∈ (fun x => eval x p) '' σ a
<VAR>p : ℕ<VAR>inst✝¹⁰ : Fact (Nat.Prime p)<VAR>R : Type u₁<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : CharP R p<VAR>P : Type u₃<VAR>inst✝⁷ : CommSemiring P<VAR>inst✝⁶ : CharP P p<VAR>inst✝⁵ : PerfectRing P p<VAR>S : Type u₂<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : CharP S p<VAR>Q : Type u₄<VAR>inst✝² : CommSemiring Q<VAR>inst✝¹ : CharP Q p<VAR>inst✝ : PerfectRing Q p<VAR>φ : R →+* S<VAR>f : Ring.Perfection R p<GOAL>(Perfection.coeff S p 0) ((map p ⋯ ⋯ φ) f) = (Perfection.coeff S p 0) ((Perfection.map p φ) f)
<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>ι : Type u_5<VAR>inst✝⁵ : Countable ι<VAR>μ : Measure X<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : BorelSpace X<VAR>inst✝¹ : MetrizableSpace X<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : C(X, E)<VAR>s : ι → Compacts X<VAR>hf : Summable fun i => ‖ContinuousMap.restrict (↑(s i)) f‖ * (μ ↑(s i)).toReal<VAR>hs : ⋃ i, ↑(s i) = univ<GOAL>Integrable (⇑f) μ
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁹ : Fintype n<VAR>inst✝⁸ : Fintype m<VAR>inst✝⁷ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝⁶ : AddCommMonoid M₁<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>M₃ : Type u_7<VAR>inst✝² : AddCommMonoid M₃<VAR>inst✝¹ : Module R M₃<VAR>v₃ : Basis l R M₃<VAR>inst✝ : DecidableEq M₁<VAR>f : M₁ →ₗ[R] M₁<VAR>k i : n<GOAL>(toMatrixAlgEquiv v₁.reindexRange) f ⟨v₁ k, ⋯⟩ ⟨v₁ i, ⋯⟩ = (toMatrixAlgEquiv v₁) f k i
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<GOAL>x ∈ closedBall y ε ↔ y ∈ closedBall x ε
<VAR>a0 a' : ONote<VAR>N0 : a0.NF<VAR>Na' : a'.NF<VAR>m : ℕ<VAR>d : ω ∣ a'.repr<VAR>e0 : a0.repr ≠ 0<VAR>h : a'.repr + ↑m < ω ^ a0.repr<VAR>n : ℕ+<VAR>k : ℕ<VAR>R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr<GOAL>(k ≠ 0 → R' < (ω ^ a0.repr) ^ succ ↑k) ∧ (ω ^ a0.repr) ^ ↑k * (ω ^ a0.repr * ↑↑n + a'.repr) + R' = (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ succ ↑k
<VAR>a0 a' : ONote<VAR>N0 : a0.NF<VAR>Na' : a'.NF<VAR>m : ℕ<VAR>d : ω ∣ a'.repr<VAR>e0 : a0.repr ≠ 0<VAR>h : a'.repr + ↑m < ω ^ a0.repr<VAR>n : ℕ+<VAR>k : ℕ<VAR>R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr<VAR>No : (a0.oadd n a').NF<GOAL>(k ≠ 0 → R' < (ω ^ a0.repr) ^ succ ↑k) ∧ (ω ^ a0.repr) ^ ↑k * (ω ^ a0.repr * ↑↑n + a'.repr) + R' = (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ succ ↑k
<VAR>a0 a' : ONote<VAR>N0 : a0.NF<VAR>Na' : a'.NF<VAR>m : ℕ<VAR>d : ω ∣ a'.repr<VAR>e0 : a0.repr ≠ 0<VAR>h : a'.repr + ↑m < ω ^ a0.repr<VAR>n : ℕ+<VAR>No : (a0.oadd n a').NF<VAR>k : ℕ<VAR>R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr<VAR>R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr<VAR>ω0 : Ordinal.{0} := ω ^ a0.repr<VAR>α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr<VAR>IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k<VAR>RR : R' = ω0 ^ ↑k * (α' * ↑m) + R<GOAL>(k + 1 ≠ 0 → R' < (ω ^ a0.repr) ^ succ ↑(k + 1)) ∧ (ω ^ a0.repr) ^ ↑(k + 1) * (ω ^ a0.repr * ↑↑n + a'.repr) + R' = (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ succ ↑(k + 1)
<VAR>a0 a' : ONote<VAR>N0 : a0.NF<VAR>Na' : a'.NF<VAR>m : ℕ<VAR>d : ω ∣ a'.repr<VAR>e0 : a0.repr ≠ 0<VAR>h : a'.repr + ↑m < ω ^ a0.repr<VAR>n : ℕ+<VAR>No : (a0.oadd n a').NF<VAR>k : ℕ<VAR>R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr<VAR>R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr<VAR>ω0 : Ordinal.{0} := ω ^ a0.repr<VAR>α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr<VAR>IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k<VAR>RR : R' = ω0 ^ ↑k * (α' * ↑m) + R<VAR>α0 : 0 < α'<GOAL>(k + 1 ≠ 0 → R' < (ω ^ a0.repr) ^ succ ↑(k + 1)) ∧ (ω ^ a0.repr) ^ ↑(k + 1) * (ω ^ a0.repr * ↑↑n + a'.repr) + R' = (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ succ ↑(k + 1)
<VAR>a0 a' : ONote<VAR>N0 : a0.NF<VAR>Na' : a'.NF<VAR>m : ℕ<VAR>d : ω ∣ a'.repr<VAR>e0 : a0.repr ≠ 0<VAR>h : a'.repr + ↑m < ω ^ a0.repr<VAR>n : ℕ+<VAR>No : (a0.oadd n a').NF<VAR>k : ℕ<VAR>R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr<VAR>R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr<VAR>ω0 : Ordinal.{0} := ω ^ a0.repr<VAR>α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr<VAR>IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k<VAR>RR : R' = ω0 ^ ↑k * (α' * ↑m) + R<VAR>α0 : 0 < α'<VAR>ω00 : 0 < ω0 ^ ↑k<GOAL>(k + 1 ≠ 0 → R' < (ω ^ a0.repr) ^ succ ↑(k + 1)) ∧ (ω ^ a0.repr) ^ ↑(k + 1) * (ω ^ a0.repr * ↑↑n + a'.repr) + R' = (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ succ ↑(k + 1)
<VAR>a0 a' : ONote<VAR>N0 : a0.NF<VAR>Na' : a'.NF<VAR>m : ℕ<VAR>d : ω ∣ a'.repr<VAR>e0 : a0.repr ≠ 0<VAR>h : a'.repr + ↑m < ω ^ a0.repr<VAR>n : ℕ+<VAR>No : (a0.oadd n a').NF<VAR>k : ℕ<VAR>R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr<VAR>R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr<VAR>ω0 : Ordinal.{0} := ω ^ a0.repr<VAR>α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr<VAR>IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k<VAR>RR : R' = ω0 ^ ↑k * (α' * ↑m) + R<VAR>α0 : 0 < α'<VAR>ω00 : 0 < ω0 ^ ↑k<VAR>Rl : R < ω ^ (a0.repr * succ ↑k)<GOAL>(ω ^ a0.repr) ^ ↑(k + 1) * (ω ^ a0.repr * ↑↑n + a'.repr) + R' = (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ succ ↑(k + 1)
<VAR>a0 a' : ONote<VAR>N0 : a0.NF<VAR>Na' : a'.NF<VAR>m : ℕ<VAR>d : ω ∣ a'.repr<VAR>e0 : a0.repr ≠ 0<VAR>h : a'.repr + ↑m < ω ^ a0.repr<VAR>n : ℕ+<VAR>No : (a0.oadd n a').NF<VAR>k : ℕ<VAR>R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr<VAR>R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr<VAR>ω0 : Ordinal.{0} := ω ^ a0.repr<VAR>α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr<VAR>IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k<VAR>RR : R' = ω0 ^ ↑k * (α' * ↑m) + R<VAR>α0 : 0 < α'<VAR>ω00 : 0 < ω0 ^ ↑k<VAR>Rl : R < ω ^ (a0.repr * succ ↑k)<GOAL>ω0 ^ succ ↑k * α' + (ω0 ^ ↑k * α' * ↑m + R) = (ω0 ^ ↑k * α' + R) * α' + (ω0 ^ ↑k * α' + R) * ↑m
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝ : DiscreteTopology X<VAR>hs : IsLindelof s<GOAL>s.Countable