ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>L : Language<VAR>ι : Type v<VAR>inst✝⁵ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁴ : (i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>inst✝³ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>inst✝² : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝¹ : Nonempty ι<VAR>P : Type u₁<VAR>inst✝ : L.Structure P<VAR>g : (i : ι) → G i ↪[L] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>i : ι<VAR>x : G i<GOAL>(lift L ι G f g Hg).toFun ⟦Structure.Sigma.mk f i x⟧ = (g i) x
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝² : CommMonoid β<VAR>s : Finset α<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : (x : α) → Decidable ¬p x<VAR>f : α → β<VAR>this : DecidableEq α<GOAL>(∏ x ∈ filter p s, f x) * ∏ x ∈ filter (fun x => ¬p x) s, f x = ∏ x ∈ s, f x
<VAR>R : Type u_1<VAR>n✝ x p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hp1 : Odd p<VAR>hx : ¬p ∣ x<VAR>n : ℕ<VAR>hn : Odd n<VAR>y : ℕ<VAR>hxy : p ∣ x + (y + 1)<GOAL>padicValNat p (x ^ n + (y + 1) ^ n) = padicValNat p (x + (y + 1)) + padicValNat p n
<VAR>R : Type u_1<VAR>n✝ x p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hp1 : Odd p<VAR>hx : ¬p ∣ x<VAR>n : ℕ<VAR>hn : Odd n<VAR>y : ℕ<VAR>hxy : p ∣ x + (y + 1)<GOAL>↑(padicValNat p (x ^ n + (y + 1) ^ n)) = ↑(padicValNat p (x + (y + 1))) + ↑(padicValNat p n)
<VAR>R : Type u_1<VAR>n✝ x p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hp1 : Odd p<VAR>hx : ¬p ∣ x<VAR>n : ℕ<VAR>hn : Odd n<VAR>y : ℕ<VAR>hxy : p ∣ x + (y + 1)<GOAL>multiplicity p (x ^ n + (y + 1) ^ n) = multiplicity p (x + (y + 1)) + multiplicity p n
<VAR>R : Type u_1<VAR>n✝ x p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hp1 : Odd p<VAR>hx : ¬p ∣ x<VAR>n : ℕ<VAR>hn : Odd n<VAR>y : ℕ<VAR>hxy : p ∣ x + (y + 1)<GOAL>0 < n
<VAR>R : Type u_1<VAR>n✝ x p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hp1 : Odd p<VAR>hx : ¬p ∣ x<VAR>n : ℕ<VAR>hn : Odd n<VAR>y : ℕ<VAR>hxy : p ∣ x + (y + 1)<GOAL>0 < x + (y + 1)
<VAR>R : Type u_1<VAR>n✝ x p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hp1 : Odd p<VAR>hx : ¬p ∣ x<VAR>n : ℕ<VAR>hn : Odd n<VAR>y : ℕ<VAR>hxy : p ∣ x + (y + 1)<GOAL>0 < x ^ n + (y + 1) ^ n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : List α<VAR>a : α<GOAL>(l ++ [a]).sublists = l.sublists ++ map (fun x => x ++ [a]) l.sublists
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q✝ r p q : R[X]<VAR>n : ℕ<VAR>hp : p.natDegree ≤ n<VAR>hq : q.natDegree ≤ n<GOAL>p = q ↔ ∀ i ≤ n, p.coeff i = q.coeff i
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q✝ r p q : R[X]<VAR>n : ℕ<VAR>hp : p.natDegree ≤ n<VAR>hq : q.natDegree ≤ n<GOAL>(∀ (n : ℕ), p.coeff n = q.coeff n) ↔ ∀ i ≤ n, p.coeff i = q.coeff i
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q✝ r p q : R[X]<VAR>n : ℕ<VAR>hp : p.natDegree ≤ n<VAR>hq : q.natDegree ≤ n<VAR>i : ℕ<VAR>h : i ≤ n → p.coeff i = q.coeff i<GOAL>p.coeff i = q.coeff i
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q✝ r p q : R[X]<VAR>n : ℕ<VAR>hp : p.natDegree ≤ n<VAR>hq : q.natDegree ≤ n<VAR>i : ℕ<VAR>h : i ≤ n → p.coeff i = q.coeff i<VAR>k : n < i<GOAL>p.coeff i = q.coeff i
<VAR>R : Type u_1<VAR>inst✝⁴ : StrictOrderedCommRing R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>x y : M<VAR>f : M ≃ₗ[R] N<VAR>v : Ray R M<GOAL>(map f) (-v) = -(map f) v
<VAR>R : Type u_1<VAR>inst✝⁴ : StrictOrderedCommRing R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>x y : M<VAR>f : M ≃ₗ[R] N<VAR>g : M<VAR>hg : g ≠ 0<GOAL>(map f) (-rayOfNeZero R g hg) = -(map f) (rayOfNeZero R g hg)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>b : R<VAR>s : S<VAR>inst✝¹ : Monoid R<VAR>inst✝ : MulAction R M<VAR>a : Rˣ<GOAL>IsSMulRegular M ↑a
<VAR>α : Type u<VAR>β✝ : Type v<VAR>δ : Type w<VAR>a : α<VAR>β : Type u<VAR>fr : Stream' α → β<VAR>ch : fr (cycle [a] ⋯) = fr (const a)<GOAL>fr (cycle [a] ⋯).tail = fr (const a).tail
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : LinearOrderedSemiring R<VAR>a b : R<VAR>m n : ℕ<VAR>ha : 0 ≤ a<VAR>hn : n ≠ 0<GOAL>a ^ n = 1 ↔ a = 1
<VAR>𝕜 : Type u_1<VAR>A✝ : Type u_2<VAR>A : Type u_3<VAR>inst✝³ : NonUnitalRing A<VAR>inst✝² : Module ℝ A<VAR>inst✝¹ : IsScalarTower ℝ A A<VAR>inst✝ : SMulCommClass ℝ A A<VAR>a : A<GOAL>QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ ∀ x ∈ σₙ ℝ a, 0 ≤ x
<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>ha : IsOfFinOrder a<GOAL>Nat.card ↑↑(powers a) ≤ orderOf a
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : SimplicialCategory C<VAR>K L : C<GOAL>sHomWhiskerRight (𝟙 K) L = 𝟙 (sHom K L)
<VAR>ι : Type u_1<VAR>I J✝ J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J<VAR>πi' : Box ι → (J : Box ι) → Prepartition J<VAR>J : Box ι<GOAL>(J ∈ π.biUnion fun J => (πi J).biUnion (πi' J)) ↔ J ∈ (π.biUnion πi).biUnion fun J => πi' (π.biUnionIndex πi J) J
<VAR>ι : Type u_1<VAR>I J✝ J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J<VAR>πi' : Box ι → (J : Box ι) → Prepartition J<VAR>J : Box ι<GOAL>(∃ J' ∈ π, ∃ J'_1 ∈ πi J', J ∈ πi' J' J'_1) ↔ ∃ J', (∃ J'_1 ∈ π, J' ∈ πi J'_1) ∧ J ∈ πi' (π.biUnionIndex πi J') 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>G : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup G'<VAR>inst✝⁴ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>𝔸 : Type u_6<VAR>𝔸' : Type u_7<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedCommRing 𝔸'<VAR>inst✝¹ : NormedAlgebra 𝕜 𝔸<VAR>inst✝ : NormedAlgebra 𝕜 𝔸'<VAR>a b : E → 𝔸<VAR>a' b' : E →L[𝕜] 𝔸<VAR>c d : E → 𝔸'<VAR>c' d' : E →L[𝕜] 𝔸'<VAR>hc : HasFDerivWithinAt c c' s x<VAR>hd : HasFDerivWithinAt d d' s x<GOAL>HasFDerivWithinAt (fun y => c y * d y) (c x • d' + d x • c') s x
<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>G : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup G'<VAR>inst✝⁴ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>𝔸 : Type u_6<VAR>𝔸' : Type u_7<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedCommRing 𝔸'<VAR>inst✝¹ : NormedAlgebra 𝕜 𝔸<VAR>inst✝ : NormedAlgebra 𝕜 𝔸'<VAR>a b : E → 𝔸<VAR>a' b' : E →L[𝕜] 𝔸<VAR>c d : E → 𝔸'<VAR>c' d' : E →L[𝕜] 𝔸'<VAR>hc : HasFDerivWithinAt c c' s x<VAR>hd : HasFDerivWithinAt d d' s x<GOAL>d x • c' = c'.smulRight (d x)
<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>G : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup G'<VAR>inst✝⁴ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>𝔸 : Type u_6<VAR>𝔸' : Type u_7<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedCommRing 𝔸'<VAR>inst✝¹ : NormedAlgebra 𝕜 𝔸<VAR>inst✝ : NormedAlgebra 𝕜 𝔸'<VAR>a b : E → 𝔸<VAR>a' b' : E →L[𝕜] 𝔸<VAR>c d : E → 𝔸'<VAR>c' d' : E →L[𝕜] 𝔸'<VAR>hc : HasFDerivWithinAt c c' s x<VAR>hd : HasFDerivWithinAt d d' s x<VAR>z : E<GOAL>(d x • c') z = (c'.smulRight (d x)) z
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : Algebra.IsAlgebraic E K<GOAL>finSepDegree F E * finSepDegree E K = finSepDegree F K
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : AddCommMonoid M'<VAR>inst✝⁸ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁷ : CommSemiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Module A M'<VAR>inst✝⁴ : IsLocalization S A<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>inst✝ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝ g : M →ₗ[R] M''<VAR>h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)<VAR>x y : LocalizedModule S M<VAR>a a' : M<VAR>b b' : ↥S<GOAL>lift' S g h (mk a b + mk a' b') = lift' S g h (mk a b) + lift' S g h (mk a' b')
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : AddCommMonoid M'<VAR>inst✝⁸ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁷ : CommSemiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Module A M'<VAR>inst✝⁴ : IsLocalization S A<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>inst✝ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝ g : M →ₗ[R] M''<VAR>h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)<VAR>x y : LocalizedModule S M<VAR>a a' : M<VAR>b b' : ↥S<GOAL>↑⋯.unit⁻¹ (g ((a', b').2 • (a, b).1 + (a, b).2 • (a', b').1)) = ↑⋯.unit⁻¹ (g a) + ↑⋯.unit⁻¹ (g a')
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : AddCommMonoid M'<VAR>inst✝⁸ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁷ : CommSemiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Module A M'<VAR>inst✝⁴ : IsLocalization S A<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>inst✝ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝ g : M →ₗ[R] M''<VAR>h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)<VAR>x y : LocalizedModule S M<VAR>a a' : M<VAR>b b' : ↥S<GOAL>g ((a', b').2 • (a, b).1) + g ((a, b).2 • (a', b').1) = ↑⋯.unit⁻¹ (g (↑((a, b).2 * (a', b').2) • a)) + ↑⋯.unit⁻¹ (↑((a, b).2 * (a', b').2) • g a')
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>inst✝ : StarRing R<VAR>a : R<VAR>ha : ¬IsUnit a<GOAL>inverse (star a) = star (inverse a)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>hG : Group.FG G<VAR>inst✝ : H.FiniteIndex<VAR>this : Group.FG ↥H<GOAL>Group.rank ↥H ≤ H.index * Group.rank G
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>R S✝ : Set G<VAR>hG : Group.FG G<VAR>inst✝ : H.FiniteIndex<VAR>this : Group.FG ↥H<VAR>S : Finset G<VAR>hS₀ : S.card = Group.rank G<VAR>hS : closure ↑S = ⊤<GOAL>Group.rank ↥H ≤ H.index * Group.rank G
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>R S✝ : Set G<VAR>hG : Group.FG G<VAR>inst✝ : H.FiniteIndex<VAR>this : Group.FG ↥H<VAR>S : Finset G<VAR>hS₀ : S.card = Group.rank G<VAR>hS : closure ↑S = ⊤<VAR>T : Finset ↥H<VAR>hT₀ : T.card ≤ H.index * S.card<VAR>hT : closure ↑T = ⊤<GOAL>Group.rank ↥H ≤ H.index * Group.rank G
<VAR>ι : Type u_1<VAR>κ✝ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f g✝ : α → β<VAR>κ : Type u_6<VAR>inst✝ : DecidableEq κ<VAR>s : Finset ι<VAR>t : Finset κ<VAR>g : ι → κ<GOAL>∑ j ∈ t, (filter (fun i => g i = j) s).card = (filter (fun i => g i ∈ t) s).card
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹⁰ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : OrderTopology α<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : OrderTopology β<VAR>inst✝⁴ : Nonempty γ<VAR>inst✝³ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>δ : Type u_1<VAR>inst✝² : LinearOrder δ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : OrderClosedTopology δ<VAR>a b : α<VAR>f : α → δ<VAR>hf : ContinuousOn f (uIcc a b)<GOAL>uIcc (f a) (f b) ⊆ f '' uIcc a b
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f : X → Y<VAR>s : Set X<VAR>x : X<VAR>y : Y<VAR>hf : Continuous f<VAR>t : Set Y<GOAL>closure (f ⁻¹' t) ⊆ f ⁻¹' closure t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f : X → Y<VAR>s : Set X<VAR>x : X<VAR>y : Y<VAR>hf : Continuous f<VAR>t : Set Y<GOAL>closure (f ⁻¹' t) ⊆ closure (f ⁻¹' closure t)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>α : Type u_3<VAR>k : ℕ<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype (Sym α k)<GOAL>Fintype.card (Sym α k) = (Fintype.card α).multichoose k
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>α : Type u_3<VAR>k : ℕ<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype (Sym α k)<GOAL>Fintype.card (Sym α k) = Fintype.card (Sym (Fin (Fintype.card α)) k)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<GOAL>IsPathConnected F ↔ PathConnectedSpace ↑F
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<GOAL>(F.Nonempty ∧ ∀ x ∈ F, ∀ y ∈ F, JoinedIn F x y) ↔ PathConnectedSpace ↑F
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>x y : X<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>x ≤ y ∨ y ≤ x
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>y : X<VAR>hy : y ∈ s<VAR>i : Fin (s.length + 1)<VAR>hx : s.toFun i ∈ s<GOAL>s.toFun i ≤ y ∨ y ≤ s.toFun i
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>i : Fin (s.length + 1)<VAR>hx : s.toFun i ∈ s<VAR>j : Fin (s.length + 1)<VAR>hy : s.toFun j ∈ s<GOAL>s.toFun i ≤ s.toFun j ∨ s.toFun j ≤ s.toFun i
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>i : Fin (s.length + 1)<VAR>hx : s.toFun i ∈ s<VAR>j : Fin (s.length + 1)<VAR>hy : s.toFun j ∈ s<GOAL>i ≤ j ∨ j ≤ i
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>x✝ : α × α<VAR>a b : α<GOAL>(a, b) ∈ Prod.swap '' idRel ↔ (a, b) ∈ idRel
<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>C : CochainComplex V ℕ<VAR>i : ℕ<GOAL>C.d 0 (i + 2) = 0
<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>C : CochainComplex V ℕ<VAR>i : ℕ<GOAL>¬(ComplexShape.up ℕ).Rel 0 (i + 2)
<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>C : CochainComplex V ℕ<VAR>i : ℕ<GOAL>¬1 = i + 2
<VAR>α : Type u_1<VAR>s : Set α<VAR>x✝ : MeasurableSet s<VAR>t : Set α<VAR>ht : t.Nonempty<GOAL>⊤ (t ∩ s) + ⊤ (t \ s) ≤ ⊤ t
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ ψ φ' ψ' : L.BoundedFormula α n<VAR>h : T.SemanticallyEquivalent φ ψ<VAR>h' : T.SemanticallyEquivalent φ' ψ'<GOAL>T.SemanticallyEquivalent (φ ⟹ φ') (ψ ⟹ ψ')
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ ψ φ' ψ' : L.BoundedFormula α n<VAR>h : T.SemanticallyEquivalent φ ψ<VAR>h' : T.SemanticallyEquivalent φ' ψ'<GOAL>∀ (M : T.ModelType) (v : α → ↑M) (xs : Fin n → ↑M), φ.Realize v xs → φ'.Realize v xs ↔ ψ.Realize v xs → ψ'.Realize v xs
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>Γ₀ : Type u_2<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>hv : Valued K Γ₀<GOAL>Continuous extension
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>Γ₀ : Type u_2<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>hv : Valued K Γ₀<GOAL>∀ (b : hat K), ∃ c, Tendsto (⇑v) (Filter.comap (↑K) (𝓝 b)) (𝓝 c)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>Γ₀ : Type u_2<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>hv : Valued K Γ₀<VAR>x₀ : hat K<GOAL>∃ c, Tendsto (⇑v) (Filter.comap (↑K) (𝓝 x₀)) (𝓝 c)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>Γ₀ : Type u_2<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>hv : Valued K Γ₀<GOAL>∃ c, Tendsto (⇑v) (Filter.comap (↑K) (𝓝 0)) (𝓝 c)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>Γ₀ : Type u_2<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>hv : Valued K Γ₀<VAR>x₀ : hat K<VAR>h : x₀ ≠ 0<GOAL>∃ c, Tendsto (⇑v) (Filter.comap (↑K) (𝓝 x₀)) (𝓝 c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>x : α → ℕ<VAR>p : Poly α<VAR>ps : List (Poly α)<GOAL>(sumsq (p :: ps)) x = 0 ↔ List.Forall (fun a => a x = 0) (p :: ps)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>x : α → ℕ<VAR>p : Poly α<VAR>ps : List (Poly α)<GOAL>(sumsq (p :: ps)) x = 0 ↔ p x = 0 ∧ (sumsq ps) x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>x : α → ℕ<VAR>p : Poly α<VAR>ps : List (Poly α)<GOAL>(p * p + sumsq ps) x = 0 ↔ p x = 0 ∧ (sumsq ps) x = 0
<VAR>n k : ℕ<VAR>h : k ≤ n<VAR>aux₁ : (fun a => k ≤ a.2) = (fun a => k ≤ a.1) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm<GOAL>filter (fun a => k ≤ a.2) (antidiagonal n) = map ((Embedding.refl ℕ).prodMap { toFun := fun x => x + k, inj' := ⋯ }) (antidiagonal (n - k))
<VAR>n k : ℕ<VAR>h : k ≤ n<VAR>aux₁ : (fun a => k ≤ a.2) = (fun a => k ≤ a.1) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm<VAR>aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j<GOAL>filter (fun a => k ≤ a.2) (antidiagonal n) = map ((Embedding.refl ℕ).prodMap { toFun := fun x => x + k, inj' := ⋯ }) (antidiagonal (n - k))
<VAR>n k : ℕ<VAR>h : k ≤ n<VAR>aux₁ : (fun a => k ≤ a.2) = (fun a => k ≤ a.1) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm<VAR>aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j<GOAL>filter (fun a => k ≤ a.2) (map (Equiv.prodComm ℕ ℕ).toEmbedding (antidiagonal n)) = map ((Embedding.refl ℕ).prodMap { toFun := fun x => x + k, inj' := ⋯ }) (antidiagonal (n - k))
<VAR>n k : ℕ<VAR>h : k ≤ n<VAR>aux₁ : (fun a => k ≤ a.2) = (fun a => k ≤ a.1) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm<VAR>aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j<GOAL>map (({ toFun := fun x => x + k, inj' := ⋯ }.prodMap (Embedding.refl ℕ)).trans (Equiv.prodComm ℕ ℕ).toEmbedding) (antidiagonal (n - k)) = map ((Embedding.refl ℕ).prodMap { toFun := fun x => x + k, inj' := ⋯ }) (antidiagonal (n - k))
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>A : Type u₂<VAR>inst✝ : Category.{v₂, u₂} A<VAR>P : Cᵒᵖ ⥤ Type w<VAR>hP : IsSheaf J P<VAR>X : C<VAR>S : Sieve X<VAR>hS : S ∈ J.sieves X<GOAL>Presieve.IsSheafFor P S.arrows
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>A : Type u₂<VAR>inst✝ : Category.{v₂, u₂} A<VAR>P : Cᵒᵖ ⥤ Type w<VAR>hP : Presieve.IsSheaf J P<VAR>X : C<VAR>S : Sieve X<VAR>hS : S ∈ J.sieves X<GOAL>Presieve.IsSheafFor P S.arrows
<VAR>m : ℕ∞<GOAL>0 < ↑m ↔ 0 < m
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>x : M<VAR>y : ↥S<GOAL>mk x y * (monoidOf S).toMap ↑y = (monoidOf S).toMap x
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>x : M<VAR>y : ↥S<GOAL>mk (x * ↑y) (1 * y) = mk x 1
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>x : M<VAR>y : ↥S<GOAL>mk (x * ↑y) (1 * y) = mk (x * 1) (1 * 1)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : T2Space α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace α<VAR>f g : (ℕ → ℕ) → α<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>h : Disjoint (range f) (range g)<GOAL>MeasurablySeparable (range f) (range g)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : T2Space α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace α<VAR>f g : (ℕ → ℕ) → α<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>h : Disjoint (range f) (range g)<VAR>hfg : ¬MeasurablySeparable (range f) (range g)<GOAL>False
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : T2Space α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace α<VAR>f g : (ℕ → ℕ) → α<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>h : Disjoint (range f) (range g)<VAR>hfg : ¬MeasurablySeparable (range f) (range g)<VAR>I : ∀ (n : ℕ) (x y : ℕ → ℕ), ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n) → ∃ x' y', x' ∈ cylinder x n ∧ y' ∈ cylinder y n ∧ ¬MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))<GOAL>False
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : T2Space α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace α<VAR>f g : (ℕ → ℕ) → α<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>h : Disjoint (range f) (range g)<VAR>hfg : ¬MeasurablySeparable (range f) (range g)<VAR>I : ∀ (n : ℕ) (x y : ℕ → ℕ), ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n) → ∃ x' y', x' ∈ cylinder x n ∧ y' ∈ cylinder y n ∧ ¬MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))<VAR>A : Type := { p // ¬MeasurablySeparable (f '' cylinder p.2.1 p.1) (g '' cylinder p.2.2 p.1) }<VAR>F : A → A<VAR>hFn : ∀ (p : A), (↑(F p)).1 = (↑p).1 + 1<VAR>hFx : ∀ (p : A), (↑(F p)).2.1 ∈ cylinder (↑p).2.1 (↑p).1<VAR>hFy : ∀ (p : A), (↑(F p)).2.2 ∈ cylinder (↑p).2.2 (↑p).1<VAR>p0 : A := ⟨(0, fun x => 0, fun x => 0), ⋯⟩<VAR>p : ℕ → A := fun n => F^[n] p0<GOAL>False
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : T2Space α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace α<VAR>f g : (ℕ → ℕ) → α<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>h : Disjoint (range f) (range g)<VAR>hfg : ¬MeasurablySeparable (range f) (range g)<VAR>I : ∀ (n : ℕ) (x y : ℕ → ℕ), ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n) → ∃ x' y', x' ∈ cylinder x n ∧ y' ∈ cylinder y n ∧ ¬MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))<VAR>A : Type := { p // ¬MeasurablySeparable (f '' cylinder p.2.1 p.1) (g '' cylinder p.2.2 p.1) }<VAR>F : A → A<VAR>hFn : ∀ (p : A), (↑(F p)).1 = (↑p).1 + 1<VAR>hFx : ∀ (p : A), (↑(F p)).2.1 ∈ cylinder (↑p).2.1 (↑p).1<VAR>hFy : ∀ (p : A), (↑(F p)).2.2 ∈ cylinder (↑p).2.2 (↑p).1<VAR>p0 : A := ⟨(0, fun x => 0, fun x => 0), ⋯⟩<VAR>p : ℕ → A := fun n => F^[n] p0<VAR>prec : ∀ (n : ℕ), p (n + 1) = F (p n)<GOAL>False
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : T2Space α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace α<VAR>f g : (ℕ → ℕ) → α<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>h : Disjoint (range f) (range g)<VAR>hfg : ¬MeasurablySeparable (range f) (range g)<VAR>I : ∀ (n : ℕ) (x y : ℕ → ℕ), ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n) → ∃ x' y', x' ∈ cylinder x n ∧ y' ∈ cylinder y n ∧ ¬MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))<VAR>A : Type := { p // ¬MeasurablySeparable (f '' cylinder p.2.1 p.1) (g '' cylinder p.2.2 p.1) }<VAR>F : A → A<VAR>hFn : ∀ (p : A), (↑(F p)).1 = (↑p).1 + 1<VAR>hFx : ∀ (p : A), (↑(F p)).2.1 ∈ cylinder (↑p).2.1 (↑p).1<VAR>hFy : ∀ (p : A), (↑(F p)).2.2 ∈ cylinder (↑p).2.2 (↑p).1<VAR>p0 : A := ⟨(0, fun x => 0, fun x => 0), ⋯⟩<VAR>p : ℕ → A := fun n => F^[n] p0<VAR>prec : ∀ (n : ℕ), p (n + 1) = F (p n)<VAR>pn_fst : ∀ (n : ℕ), (↑(p n)).1 = n<VAR>Ix : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.1 m = (↑(p (m + 1))).2.1 m<VAR>Iy : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.2 m = (↑(p (m + 1))).2.2 m<VAR>x : ℕ → ℕ := fun n => (↑(p (n + 1))).2.1 n<VAR>hx : x = fun n => (↑(p (n + 1))).2.1 n<VAR>y : ℕ → ℕ := fun n => (↑(p (n + 1))).2.2 n<VAR>hy : y = fun n => (↑(p (n + 1))).2.2 n<VAR>M : ∀ (n : ℕ), ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n)<GOAL>False