ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>n : ℕ<VAR>p : ℕ → ℝ<VAR>hp : ∀ (k : ℕ), 0 ≤ p k<VAR>r a : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<GOAL>∑ e ∈ compPartialSumSource 2 (n + 1) n, ∏ j : Fin e.fst, r * (a ^ e.snd j * p (e.snd j)) = ∑ j ∈ Ico 2 (n + 1), r ^ j * (∑ k ∈ Ico 1 n, a ^ k * p k) ^ j
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>n : ℕ<VAR>p : ℕ → ℝ<VAR>hp : ∀ (k : ℕ), 0 ≤ p k<VAR>r a : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<GOAL>∑ a_1 ∈ Ico 2 (n + 1), ∑ s ∈ Fintype.piFinset fun x => Ico 1 n, ∏ j : Fin a_1, r * (a ^ s j * p (s j)) = ∑ j ∈ Ico 2 (n + 1), r ^ j * (∑ k ∈ Ico 1 n, a ^ k * p k) ^ j
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>n : ℕ<VAR>p : ℕ → ℝ<VAR>hp : ∀ (k : ℕ), 0 ≤ p k<VAR>r a : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<VAR>j : ℕ<VAR>a✝ : j ∈ Ico 2 (n + 1)<GOAL>∑ s ∈ Fintype.piFinset fun x => Ico 1 n, ∏ j : Fin j, r * (a ^ s j * p (s j)) = r ^ j * (∑ k ∈ Ico 1 n, a ^ k * p k) ^ j
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>n : ℕ<VAR>p : ℕ → ℝ<VAR>hp : ∀ (k : ℕ), 0 ≤ p k<VAR>r a : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<VAR>j : ℕ<VAR>a✝ : j ∈ Ico 2 (n + 1)<GOAL>(∑ x ∈ Fintype.piFinset fun x => Ico 1 n, (MultilinearMap.mkPiAlgebra ℝ (Fin j) ℝ) fun j => r * (a ^ x j * p (x j))) = r ^ j * (∑ k ∈ Ico 1 n, a ^ k * p k) ^ j
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>n : ℕ<VAR>p : ℕ → ℝ<VAR>hp : ∀ (k : ℕ), 0 ≤ p k<VAR>r a : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<VAR>j : ℕ<VAR>a✝ : j ∈ Ico 2 (n + 1)<GOAL>((MultilinearMap.mkPiAlgebra ℝ (Fin j) ℝ) fun i => ∑ j ∈ Ico 1 n, r * (a ^ j * p j)) = r ^ j * (∑ k ∈ Ico 1 n, a ^ k * p k) ^ j
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>n : ℕ<VAR>p : ℕ → ℝ<VAR>hp : ∀ (k : ℕ), 0 ≤ p k<VAR>r a : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<VAR>j : ℕ<VAR>a✝ : j ∈ Ico 2 (n + 1)<GOAL>∏ i : Fin j, ∑ j ∈ Ico 1 n, r * (a ^ j * p j) = r ^ j * (∑ k ∈ Ico 1 n, a ^ k * p k) ^ j
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a<VAR>z w : PGame<VAR>h : w.IsOption y<GOAL>z.IsOption x₁ → P2 z x₂ w
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a<VAR>z w : PGame<VAR>h : w.IsOption y<GOAL>z.IsOption x₂ → P2 x₁ z w
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>x : E<VAR>r : ℝ<VAR>hr : r ≠ 0<GOAL>interior (closedBall x r) = ball x r
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>x : E<VAR>r : ℝ<VAR>hr✝ : r ≠ 0<VAR>hr : r < 0<GOAL>interior (closedBall x r) = ball x r
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>x : E<VAR>r : ℝ<VAR>hr✝ : r ≠ 0<VAR>hr : 0 < r<GOAL>interior (closedBall x r) = ball x r
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>x : E<VAR>r : ℝ<VAR>hr✝ : r ≠ 0<VAR>hr : 0 < r<GOAL>interior (closedBall x r) ⊆ ball x r
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>x : E<VAR>r : ℝ<VAR>hr✝ : r ≠ 0<VAR>hr : 0 < r<VAR>y : E<VAR>hy : y ∈ interior (closedBall x r)<GOAL>y ∈ ball x r
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>x : E<VAR>r : ℝ<VAR>hr✝¹ : r ≠ 0<VAR>hr✝ : 0 < r<VAR>y : E<VAR>hy : y ∈ interior (closedBall x r)<VAR>hr : dist y x < r<GOAL>y ∈ ball x r
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y : E<VAR>hr✝ : dist y x ≠ 0<VAR>hr : 0 < dist y x<VAR>hy : y ∈ interior (closedBall x (dist y x))<GOAL>y ∈ ball x (dist y x)
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y : E<VAR>hr✝ : dist y x ≠ 0<VAR>hr : 0 < dist y x<VAR>hy : y ∈ interior (closedBall x (dist y x))<VAR>f : ℝ → E := fun c => c • (y - x) + x<GOAL>y ∈ ball x (dist y x)
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y : E<VAR>hr✝ : dist y x ≠ 0<VAR>hr : 0 < dist y x<VAR>hy : y ∈ interior (closedBall x (dist y x))<VAR>f : ℝ → E := fun c => c • (y - x) + x<GOAL>f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y : E<VAR>hr✝ : dist y x ≠ 0<VAR>hr : 0 < dist y x<VAR>hy : y ∈ interior (closedBall x (dist y x))<VAR>f : ℝ → E := fun c => c • (y - x) + x<VAR>c : ℝ<VAR>hc : c ∈ f ⁻¹' closedBall x (dist y x)<GOAL>c ∈ Icc (-1) 1
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y : E<VAR>hr✝ : dist y x ≠ 0<VAR>hr : 0 < dist y x<VAR>hy : y ∈ interior (closedBall x (dist y x))<VAR>f : ℝ → E := fun c => c • (y - x) + x<VAR>c : ℝ<VAR>hc : c ∈ f ⁻¹' closedBall x (dist y x)<GOAL>‖c‖ * dist y x ≤ 1 * dist y x
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>S : L.Substructure M<VAR>A s : Set M<VAR>h : A ⊆ ↑S<GOAL>(closure (L[[↑A]])).toFun s = ((closure L).toFun (A ∪ s)).withConstants ⋯
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>S : L.Substructure M<VAR>A s : Set M<VAR>h : A ⊆ ↑S<GOAL>((closure L).toFun (A ∪ s)).withConstants ⋯ ≤ (closure (L[[↑A]])).toFun s
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>S : L.Substructure M<VAR>A s : Set M<VAR>h : A ⊆ ↑S<GOAL>(L.lhomWithConstants ↑A).substructureReduct (((closure L).toFun (A ∪ s)).withConstants ⋯) ≤ (L.lhomWithConstants ↑A).substructureReduct ((closure (L[[↑A]])).toFun s)
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>S : L.Substructure M<VAR>A s : Set M<VAR>h : A ⊆ ↑S<GOAL>A ⊆ ↑((closure (L[[↑A]])).toFun s)
<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.HasLeftHomology<VAR>inst✝ : S.HasRightHomology<VAR>h : IsIso S.leftRightHomologyComparison<VAR>this : IsIso (leftRightHomologyComparison' S.leftHomologyData S.rightHomologyData)<GOAL>S.HasHomology
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>z : Cochain F G 0<VAR>p q : ℤ<VAR>hpq : p + 1 = q<GOAL>(δ 0 1 z).v p q hpq = z.v p p ⋯ ≫ G.d p q - F.d p q ≫ z.v q q ⋯
<VAR>R : Type u<VAR>inst✝ : Semiring R<VAR>q : ℕ<VAR>h : Nat.Prime q<VAR>hchar✝ : CharP R q<GOAL>ringExpChar R = q
<VAR>R : Type u<VAR>inst✝ : Semiring R<VAR>q : ℕ<VAR>h : Nat.Prime q<VAR>hchar✝ : CharP R q<GOAL>max q 1 = q
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : MulAction G β<VAR>x : Quotient G α<GOAL>x.orbit.Nonempty
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : MulAction G β<VAR>x : Quotient G α<GOAL>(MulAction.orbit G (Quotient.out' x)).Nonempty
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁴ : Semiring α<VAR>inst✝³ : Preorder α<VAR>a b c d : α<VAR>inst✝² : ZeroLEOneClass α<VAR>inst✝¹ : PosMulMono α<VAR>inst✝ : MulPosMono α<VAR>ha₀ : 0 ≤ a<VAR>ha₁ : a ≤ 1<VAR>n✝ m✝ : ℕ<VAR>h : n✝.le m✝<GOAL>a ^ m✝.succ ≤ a ^ n✝
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁴ : Semiring α<VAR>inst✝³ : Preorder α<VAR>a b c d : α<VAR>inst✝² : ZeroLEOneClass α<VAR>inst✝¹ : PosMulMono α<VAR>inst✝ : MulPosMono α<VAR>ha₀ : 0 ≤ a<VAR>ha₁ : a ≤ 1<VAR>n✝ m✝ : ℕ<VAR>h : n✝.le m✝<GOAL>a * a ^ m✝ ≤ a ^ n✝
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s t : Set α<GOAL>univ.Infinite ↔ Infinite α
<VAR>R : Type u<VAR>a✝ b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q a : R[X]<GOAL>a.toFinsupp = 1 ↔ a = 1
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>γ : Cochain F G n<VAR>p q : ℤ<VAR>hpq : p + n = q<GOAL>γ.v p q hpq ≫ (HomologicalComplex.XIsoOfEq G ⋯).hom = γ.v p q ⋯
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>x : O<GOAL>v ↑p < v ((algebraMap O K) x) ↔ (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝ : AddGroup G<GOAL>AddMonoid.IsTorsionFree G ↔ NoZeroSMulDivisors ℤ G
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝ : AddGroup G<GOAL>(∀ (y : ℤ) (x : G), x ≠ 0 → y ≠ 0 → ¬y • x = 0) ↔ ∀ {c : ℤ} {x : G}, c • x = 0 → c = 0 ∨ x = 0
<VAR>a b : Ordinal.{u_1}<VAR>h : a ≤ b<GOAL>a.toPGame ≤ b.toPGame
<VAR>a b : Ordinal.{u_1}<VAR>h : a ≤ b<VAR>i : a.toPGame.LeftMoves<GOAL>a.toPGame.moveLeft i ⧏ b.toPGame
<VAR>a b : Ordinal.{u_1}<VAR>h : a ≤ b<VAR>i : a.toPGame.LeftMoves<GOAL>(↑(toLeftMovesToPGame.symm i)).toPGame ⧏ b.toPGame
<VAR>b✝ x y a b : ℝ<VAR>h₁ : a ≠ 0<VAR>h₂ : b ≠ 0<VAR>c : ℝ<GOAL>logb (a * b) c = ((logb a c)⁻¹ + (logb b c)⁻¹)⁻¹
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝³ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝² : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝ : (i : ι) → MetricSpace (α i)<VAR>x : (i : ι) → α i<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>(Measure.pi μ) (Metric.ball x r) = ∏ i : ι, (μ i) (Metric.ball (x i) r)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>α : Type u_6<VAR>f : Filter α<VAR>inst✝² : f.NeBot<VAR>R : Type u_7<VAR>inst✝¹ : Preorder R<VAR>κ : Type u_8<VAR>inst✝ : AddCommMonoid R<VAR>r : R → R → Prop<VAR>hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)<VAR>hr₀ : r 0 0<VAR>u : κ → α → R<VAR>s : Finset κ<VAR>h : ∀ k ∈ s, IsBoundedUnder r f (u k)<GOAL>IsBoundedUnder r f (∑ k ∈ s, u k)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>α : Type u_6<VAR>f : Filter α<VAR>inst✝² : f.NeBot<VAR>R : Type u_7<VAR>inst✝¹ : Preorder R<VAR>κ : Type u_8<VAR>inst✝ : AddCommMonoid R<VAR>r : R → R → Prop<VAR>hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)<VAR>hr₀ : r 0 0<VAR>u : κ → α → R<VAR>h : ∀ k ∈ ∅, IsBoundedUnder r f (u k)<GOAL>IsBoundedUnder r f (∑ k ∈ ∅, u k)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>α : Type u_6<VAR>f : Filter α<VAR>inst✝² : f.NeBot<VAR>R : Type u_7<VAR>inst✝¹ : Preorder R<VAR>κ : Type u_8<VAR>inst✝ : AddCommMonoid R<VAR>r : R → R → Prop<VAR>hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)<VAR>hr₀ : r 0 0<VAR>u : κ → α → R<VAR>a✝¹ : κ<VAR>s✝ : Finset κ<VAR>h✝ : a✝¹ ∉ s✝<VAR>a✝ : (∀ k ∈ s✝, IsBoundedUnder r f (u k)) → IsBoundedUnder r f (∑ k ∈ s✝, u k)<VAR>h : ∀ k ∈ Finset.cons a✝¹ s✝ h✝, IsBoundedUnder r f (u k)<GOAL>IsBoundedUnder r f (∑ k ∈ Finset.cons a✝¹ s✝ h✝, u k)
<VAR>x : ℂ<VAR>hx : cos x = 0<GOAL>Tendsto (fun x => abs (tan x)) (𝓝[≠] x) atTop
<VAR>x : ℂ<VAR>hx : cos x = 0<GOAL>Tendsto (fun x => ‖sin x‖ / ‖cos x‖) (𝓝[≠] x) atTop
<VAR>x : ℂ<VAR>hx : cos x = 0<VAR>A : sin x ≠ 0<GOAL>Tendsto (fun x => ‖sin x‖ / ‖cos x‖) (𝓝[≠] x) atTop
<VAR>x : ℂ<VAR>hx : cos x = 0<VAR>A : sin x ≠ 0<VAR>B : Tendsto cos (𝓝[≠] x) (𝓝[≠] 0)<GOAL>Tendsto (fun x => ‖sin x‖ / ‖cos x‖) (𝓝[≠] x) atTop
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : MeasurableSpace α'<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace β'<VAR>inst✝⁴ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : SFinite ν<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : SFinite τ<GOAL>map (⇑MeasurableEquiv.prodAssoc) ((μ.prod ν).prod τ) = μ.prod (ν.prod τ)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : MeasurableSpace α'<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace β'<VAR>inst✝⁴ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : SFinite ν<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : SFinite τ<VAR>this : (sum fun p => (sFiniteSeq μ p.1).prod ((sFiniteSeq ν p.2.1).prod (sFiniteSeq τ p.2.2))) = sum fun p => (sFiniteSeq μ p.1.1).prod ((sFiniteSeq ν p.1.2).prod (sFiniteSeq τ p.2))<GOAL>map (⇑MeasurableEquiv.prodAssoc) ((μ.prod ν).prod τ) = μ.prod (ν.prod τ)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : MeasurableSpace α'<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace β'<VAR>inst✝⁴ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : SFinite ν<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : SFinite τ<VAR>this : (sum fun p => (sFiniteSeq μ p.1).prod ((sFiniteSeq ν p.2.1).prod (sFiniteSeq τ p.2.2))) = sum fun p => (sFiniteSeq μ p.1.1).prod ((sFiniteSeq ν p.1.2).prod (sFiniteSeq τ p.2))<GOAL>(sum fun i => map (⇑MeasurableEquiv.prodAssoc) (((sFiniteSeq μ i.1.1).prod (sFiniteSeq ν i.1.2)).prod (sFiniteSeq τ i.2))) = sum fun p => (sFiniteSeq μ p.1.1).prod ((sFiniteSeq ν p.1.2).prod (sFiniteSeq τ p.2))
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : MeasurableSpace α'<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace β'<VAR>inst✝⁴ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : SFinite ν<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : SFinite τ<VAR>this : (sum fun p => (sFiniteSeq μ p.1).prod ((sFiniteSeq ν p.2.1).prod (sFiniteSeq τ p.2.2))) = sum fun p => (sFiniteSeq μ p.1.1).prod ((sFiniteSeq ν p.1.2).prod (sFiniteSeq τ p.2))<VAR>i : (ℕ × ℕ) × ℕ<GOAL>map (⇑MeasurableEquiv.prodAssoc) (((sFiniteSeq μ i.1.1).prod (sFiniteSeq ν i.1.2)).prod (sFiniteSeq τ i.2)) = (sFiniteSeq μ i.1.1).prod ((sFiniteSeq ν i.1.2).prod (sFiniteSeq τ i.2))
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : MeasurableSpace α'<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace β'<VAR>inst✝⁴ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : SFinite ν<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : SFinite τ<VAR>this : (sum fun p => (sFiniteSeq μ p.1).prod ((sFiniteSeq ν p.2.1).prod (sFiniteSeq τ p.2.2))) = sum fun p => (sFiniteSeq μ p.1.1).prod ((sFiniteSeq ν p.1.2).prod (sFiniteSeq τ p.2))<VAR>i : (ℕ × ℕ) × ℕ<GOAL>∀ s ∈ {s | MeasurableSet s}, ∀ t ∈ image2 (fun x x_1 => x ×ˢ x_1) {s | MeasurableSet s} {t | MeasurableSet t}, (map (⇑MeasurableEquiv.prodAssoc) (((sFiniteSeq μ i.1.1).prod (sFiniteSeq ν i.1.2)).prod (sFiniteSeq τ i.2))) (s ×ˢ t) = (sFiniteSeq μ i.1.1) s * ((sFiniteSeq ν i.1.2).prod (sFiniteSeq τ i.2)) t
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : MeasurableSpace α'<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace β'<VAR>inst✝⁴ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : SFinite ν<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : SFinite τ<VAR>this : (sum fun p => (sFiniteSeq μ p.1).prod ((sFiniteSeq ν p.2.1).prod (sFiniteSeq τ p.2.2))) = sum fun p => (sFiniteSeq μ p.1.1).prod ((sFiniteSeq ν p.1.2).prod (sFiniteSeq τ p.2))<VAR>i : (ℕ × ℕ) × ℕ<VAR>s : Set α<VAR>hs : s ∈ {s | MeasurableSet s}<VAR>t : Set β<VAR>ht : t ∈ {s | MeasurableSet s}<VAR>u : Set γ<VAR>hu : u ∈ {t | MeasurableSet t}<GOAL>(map (⇑MeasurableEquiv.prodAssoc) (((sFiniteSeq μ i.1.1).prod (sFiniteSeq ν i.1.2)).prod (sFiniteSeq τ i.2))) (s ×ˢ (fun x x_1 => x ×ˢ x_1) t u) = (sFiniteSeq μ i.1.1) s * ((sFiniteSeq ν i.1.2).prod (sFiniteSeq τ i.2)) ((fun x x_1 => x ×ˢ x_1) t u)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : MeasurableSpace α'<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace β'<VAR>inst✝⁴ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : SFinite ν<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : SFinite τ<VAR>this : (sum fun p => (sFiniteSeq μ p.1).prod ((sFiniteSeq ν p.2.1).prod (sFiniteSeq τ p.2.2))) = sum fun p => (sFiniteSeq μ p.1.1).prod ((sFiniteSeq ν p.1.2).prod (sFiniteSeq τ p.2))<VAR>i : (ℕ × ℕ) × ℕ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : Set β<VAR>ht : MeasurableSet t<VAR>u : Set γ<VAR>hu : MeasurableSet u<GOAL>(map (⇑MeasurableEquiv.prodAssoc) (((sFiniteSeq μ i.1.1).prod (sFiniteSeq ν i.1.2)).prod (sFiniteSeq τ i.2))) (s ×ˢ (fun x x_1 => x ×ˢ x_1) t u) = (sFiniteSeq μ i.1.1) s * ((sFiniteSeq ν i.1.2).prod (sFiniteSeq τ i.2)) ((fun x x_1 => x ×ˢ x_1) t u)
<VAR>α β γ : Type u<VAR>S S' : Set (α → ℕ)<VAR>d : Dioph S<VAR>H : ∀ (v : α → ℕ), v ∈ S ↔ v ∈ S'<GOAL>Dioph S'
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>F' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>E' : Type u_6<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace ℝ E'<VAR>inst✝ : NormedSpace 𝕜 E'<VAR>f : ↥(simpleFunc ℝ 1 μ)<VAR>eq : ∀ (a : α), ↑(toSimpleFunc f).posPart a = max (↑(toSimpleFunc f) a) 0<GOAL>↑(toSimpleFunc (posPart f)) =ᶠ[ae μ] ↑(toSimpleFunc f).posPart
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>F' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>E' : Type u_6<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace ℝ E'<VAR>inst✝ : NormedSpace 𝕜 E'<VAR>f : ↥(simpleFunc ℝ 1 μ)<VAR>eq : ∀ (a : α), ↑(toSimpleFunc f).posPart a = max (↑(toSimpleFunc f) a) 0<VAR>ae_eq : ∀ᵐ (a : α) ∂μ, ↑(toSimpleFunc (posPart f)) a = max (↑(toSimpleFunc f) a) 0<GOAL>↑(toSimpleFunc (posPart f)) =ᶠ[ae μ] ↑(toSimpleFunc f).posPart
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>F' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>E' : Type u_6<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace ℝ E'<VAR>inst✝ : NormedSpace 𝕜 E'<VAR>f : ↥(simpleFunc ℝ 1 μ)<VAR>eq : ∀ (a : α), ↑(toSimpleFunc f).posPart a = max (↑(toSimpleFunc f) a) 0<VAR>ae_eq : ∀ᵐ (a : α) ∂μ, ↑(toSimpleFunc (posPart f)) a = max (↑(toSimpleFunc f) a) 0<VAR>a : α<VAR>h : ↑(toSimpleFunc (posPart f)) a = max (↑(toSimpleFunc f) a) 0<GOAL>↑(toSimpleFunc (posPart f)) a = ↑(toSimpleFunc f).posPart a
<VAR>α β : Type u<VAR>β' : Type v<VAR>inst✝ : Infinite α<VAR>leq : lift.{v, u} #α = lift.{u, v} #β'<GOAL>#(α ≃ β') = 2 ^ lift.{v, u} #α
<VAR>α β : Type u<VAR>β' : Type v<VAR>inst✝ : Infinite α<VAR>leq : lift.{v, u} #α = lift.{u, v} #β'<GOAL>↑2 ^ lift.{v, u} #α = 2 ^ lift.{v, u} #α
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t : Set α<GOAL>diam {x, y, z} = max (max (edist x y) (edist x z)) (edist y z)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>p : R[X]<VAR>s : R<VAR>this : (a : Prop) → Decidable a<VAR>hp : ¬p = 0<GOAL>(p.scaleRoots s).degree = p.degree
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>p : R[X]<VAR>s : R<VAR>this : (a : Prop) → Decidable a<VAR>hp : ¬p = 0<GOAL>(p.scaleRoots s).coeff p.natDegree ≠ 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>p : R[X]<VAR>s : R<VAR>this : (a : Prop) → Decidable a<VAR>hp : ¬p = 0<GOAL>p.leadingCoeff ≠ 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>p : R[X]<VAR>s : R<VAR>this : (a : Prop) → Decidable a<VAR>hp : ¬p = 0<VAR>h : p.leadingCoeff = 0<GOAL>False
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>p : R[X]<VAR>s : R<VAR>this✝ : (a : Prop) → Decidable a<VAR>hp : ¬p = 0<VAR>h : p.leadingCoeff = 0<VAR>this : p = 0<GOAL>False
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R[X]<VAR>x : ↥((Quotient.mk I).comp C).range<VAR>hx : C x ∈ map (mapRingHom ((Quotient.mk I).comp C).rangeRestrict) I<VAR>i : R →+* ↥((Quotient.mk I).comp C).range := ((Quotient.mk I).comp C).rangeRestrict<GOAL>x = 0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R[X]<VAR>x : ↥((Quotient.mk I).comp C).range<VAR>hx : C x ∈ map (mapRingHom ((Quotient.mk I).comp C).rangeRestrict) I<VAR>i : R →+* ↥((Quotient.mk I).comp C).range := ((Quotient.mk I).comp C).rangeRestrict<VAR>hi' : RingHom.ker (mapRingHom i) ≤ I<GOAL>x = 0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R[X]<VAR>i : R →+* ↥((Quotient.mk I).comp C).range := ((Quotient.mk I).comp C).rangeRestrict<VAR>hi' : RingHom.ker (mapRingHom i) ≤ I<VAR>x : R[X] ⧸ I<VAR>hx' : x ∈ ((Quotient.mk I).comp C).range<VAR>hx : C ⟨x, hx'⟩ ∈ map (mapRingHom ((Quotient.mk I).comp C).rangeRestrict) I<GOAL>⟨x, hx'⟩ = 0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R[X]<VAR>i : R →+* ↥((Quotient.mk I).comp C).range := ((Quotient.mk I).comp C).rangeRestrict<VAR>hi' : RingHom.ker (mapRingHom i) ≤ I<VAR>y : R<VAR>hx' : ((Quotient.mk I).comp C) y ∈ ((Quotient.mk I).comp C).range<VAR>hx : C ⟨((Quotient.mk I).comp C) y, hx'⟩ ∈ map (mapRingHom ((Quotient.mk I).comp C).rangeRestrict) I<GOAL>⟨((Quotient.mk I).comp C) y, hx'⟩ = 0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R[X]<VAR>i : R →+* ↥((Quotient.mk I).comp C).range := ((Quotient.mk I).comp C).rangeRestrict<VAR>hi' : RingHom.ker (mapRingHom i) ≤ I<VAR>y : R<VAR>hx' : ((Quotient.mk I).comp C) y ∈ ((Quotient.mk I).comp C).range<VAR>hx : C ⟨((Quotient.mk I).comp C) y, hx'⟩ ∈ map (mapRingHom ((Quotient.mk I).comp C).rangeRestrict) I<GOAL>↑⟨((Quotient.mk I).comp C) y, hx'⟩ = ↑0