ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Ring S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : IsDomain B<VAR>inst✝⁴ : Algebra A B<VAR>K : Type u_6<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A S<VAR>S' : Type u_7<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra A S'<VAR>pb : PowerBasis A S<VAR>x : B<GOAL>map (algebraMap A B) (minpoly A pb.gen) ≠ 0
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>l : List (Perm α)<VAR>hl : ∀ g ∈ l, g.IsSwap<GOAL>l.prod ∈ alternatingGroup α ↔ Even l.length
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>l : List (Perm α)<VAR>hl : ∀ g ∈ l, g.IsSwap<GOAL>-1 ≠ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>f : α → β<VAR>hf : Measurable f<VAR>μ : Measure (Measure α)<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>(map (map f) μ).join s = (map f μ.join) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>f : α → β<VAR>hf : Measurable f<VAR>μ : Measure (Measure α)<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∫⁻ (a : Measure α), (map f a) s ∂μ = ∫⁻ (μ : Measure α), μ (f ⁻¹' s) ∂μ
<VAR>X : ℕ → Type u<VAR>inst✝ : (n : ℕ) → MetricSpace (X n)<VAR>f : (n : ℕ) → X n → X (n + 1)<VAR>I : ∀ (n : ℕ), Isometry (f n)<VAR>n : ℕ<VAR>h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I<VAR>x✝ : TopologicalSpace ((n : ℕ) × X n) := UniformSpace.toTopologicalSpace<GOAL>toInductiveLimit I n.succ ∘ f n = toInductiveLimit I n
<VAR>X : ℕ → Type u<VAR>inst✝ : (n : ℕ) → MetricSpace (X n)<VAR>f : (n : ℕ) → X n → X (n + 1)<VAR>I : ∀ (n : ℕ), Isometry (f n)<VAR>n : ℕ<VAR>h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I<VAR>x✝ : TopologicalSpace ((n : ℕ) × X n) := UniformSpace.toTopologicalSpace<VAR>x : X n<GOAL>(toInductiveLimit I n.succ ∘ f n) x = toInductiveLimit I n x
<VAR>X : ℕ → Type u<VAR>inst✝ : (n : ℕ) → MetricSpace (X n)<VAR>f : (n : ℕ) → X n → X (n + 1)<VAR>I : ∀ (n : ℕ), Isometry (f n)<VAR>n : ℕ<VAR>h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I<VAR>x✝ : TopologicalSpace ((n : ℕ) × X n) := UniformSpace.toTopologicalSpace<VAR>x : X n<GOAL>Quotient.mk'' ⟨n.succ, f n x⟩ = Quotient.mk'' ⟨n, x⟩
<VAR>X : ℕ → Type u<VAR>inst✝ : (n : ℕ) → MetricSpace (X n)<VAR>f : (n : ℕ) → X n → X (n + 1)<VAR>I : ∀ (n : ℕ), Isometry (f n)<VAR>n : ℕ<VAR>h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I<VAR>x✝ : TopologicalSpace ((n : ℕ) × X n) := UniformSpace.toTopologicalSpace<VAR>x : X n<GOAL>dist ⟨n.succ, f n x⟩ ⟨n, x⟩ = 0
<VAR>X : ℕ → Type u<VAR>inst✝ : (n : ℕ) → MetricSpace (X n)<VAR>f : (n : ℕ) → X n → X (n + 1)<VAR>I : ∀ (n : ℕ), Isometry (f n)<VAR>n : ℕ<VAR>h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I<VAR>x✝ : TopologicalSpace ((n : ℕ) × X n) := UniformSpace.toTopologicalSpace<VAR>x : X n<GOAL>inductiveLimitDist f ⟨n.succ, f n x⟩ ⟨n, x⟩ = 0
<VAR>X : ℕ → Type u<VAR>inst✝ : (n : ℕ) → MetricSpace (X n)<VAR>f : (n : ℕ) → X n → X (n + 1)<VAR>I : ∀ (n : ℕ), Isometry (f n)<VAR>n : ℕ<VAR>h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I<VAR>x✝ : TopologicalSpace ((n : ℕ) × X n) := UniformSpace.toTopologicalSpace<VAR>x : X n<GOAL>⟨n, x⟩.fst ≤ n + 1
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LE α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c✝ d c : α<GOAL>a / c ≤ b / c ↔ a ≤ b
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi πi₁ πi₂ : (J : Box ι) → Prepartition J<VAR>hJ : J ∈ π.biUnion πi<GOAL>π.biUnionIndex πi J ∈ π
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi πi₁ πi₂ : (J : Box ι) → Prepartition J<VAR>hJ : J ∈ π.biUnion πi<GOAL>⋯.choose ∈ π
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝ : TopologicalSpace X<VAR>S : Set X<VAR>x : ↑S<GOAL>𝓝[≠] x = ⊥ ↔ 𝓝[≠] ↑x ⊓ 𝓟 S = ⊥
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>f : R⟦X⟧<VAR>n : ℕ<GOAL>(coeff R n) f.derivativeFun = (coeff R (n + 1)) f * (↑n + 1)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : Scheme<VAR>f : X.Hom Y<VAR>H : IsOpenImmersion f<VAR>U : X.Opens<GOAL>f ⁻¹ᵁ f ''ᵁ U = U
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : Scheme<VAR>f : X.Hom Y<VAR>H : IsOpenImmersion f<VAR>U : X.Opens<GOAL>↑(f ⁻¹ᵁ f ''ᵁ U) = ↑U
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : Group α<VAR>inst✝¹ : UniformGroup α<VAR>inst✝ : UniformSpace β<VAR>f : β → α<VAR>hf : UniformContinuous f<VAR>n : ℕ<GOAL>UniformContinuous fun x => f x ^ ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : Group α<VAR>inst✝¹ : UniformGroup α<VAR>inst✝ : UniformSpace β<VAR>f : β → α<VAR>hf : UniformContinuous f<VAR>n : ℕ<GOAL>UniformContinuous fun x => f x ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : Group α<VAR>inst✝¹ : UniformGroup α<VAR>inst✝ : UniformSpace β<VAR>f : β → α<VAR>hf : UniformContinuous f<VAR>n : ℕ<GOAL>UniformContinuous fun x => f x ^ Int.negSucc n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : Group α<VAR>inst✝¹ : UniformGroup α<VAR>inst✝ : UniformSpace β<VAR>f : β → α<VAR>hf : UniformContinuous f<VAR>n : ℕ<GOAL>UniformContinuous fun x => (f x ^ (n + 1))⁻¹
<VAR>α : Type u_1<VAR>a : α<VAR>n : Nat<VAR>l : List α<GOAL>(l.set n a)[n]? = (fun x => a) <$> l[n]?
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝⁶ : OrderedSemiring 𝕜<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : TopologicalSpace F<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s✝ : Set E<VAR>s : Set F<VAR>hs : StrictConvex 𝕜 s<VAR>f : E →ₗ[𝕜] F<VAR>hf : Continuous ⇑f<VAR>hfinj : Injective ⇑f<VAR>x : E<VAR>hx : x ∈ ⇑f ⁻¹' s<VAR>y : E<VAR>hy : y ∈ ⇑f ⁻¹' s<VAR>hxy : x ≠ y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>a • x + b • y ∈ interior (⇑f ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝⁶ : OrderedSemiring 𝕜<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : TopologicalSpace F<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s✝ : Set E<VAR>s : Set F<VAR>hs : StrictConvex 𝕜 s<VAR>f : E →ₗ[𝕜] F<VAR>hf : Continuous ⇑f<VAR>hfinj : Injective ⇑f<VAR>x : E<VAR>hx : x ∈ ⇑f ⁻¹' s<VAR>y : E<VAR>hy : y ∈ ⇑f ⁻¹' s<VAR>hxy : x ≠ y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>a • x + b • y ∈ ⇑f ⁻¹' interior s
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝⁶ : OrderedSemiring 𝕜<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : TopologicalSpace F<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s✝ : Set E<VAR>s : Set F<VAR>hs : StrictConvex 𝕜 s<VAR>f : E →ₗ[𝕜] F<VAR>hf : Continuous ⇑f<VAR>hfinj : Injective ⇑f<VAR>x : E<VAR>hx : x ∈ ⇑f ⁻¹' s<VAR>y : E<VAR>hy : y ∈ ⇑f ⁻¹' s<VAR>hxy : x ≠ y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>a • f x + b • f y ∈ interior s
<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b : α<VAR>h : a < b<GOAL>a ::ₘ Ioo a b = Ico a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t✝ t₁ t₂ : Set β<VAR>p : Set γ<VAR>f✝ f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>f : α → β<VAR>t : Set α<VAR>h : InjOn f s<VAR>hst : t ⊆ s<GOAL>f '' (s \ t) = f '' s \ f '' t
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>c : ℝ<VAR>f : ↥(Lp E 1 μ)<GOAL>(setToL1 ⋯) f = c • (setToL1 hT) f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>c : ℝ<VAR>f : ↥(Lp E 1 μ)<GOAL>setToL1 ⋯ = c • setToL1 hT
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>c : ℝ<VAR>f : ↥(Lp E 1 μ)<GOAL>(c • setToL1 hT).comp (coeToLp α E ℝ) = setToL1SCLM α E μ ⋯
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>c : ℝ<VAR>f✝ : ↥(Lp E 1 μ)<VAR>f : ↥(simpleFunc E 1 μ)<GOAL>((c • setToL1 hT).comp (coeToLp α E ℝ)) f = (setToL1SCLM α E μ ⋯) f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>c : ℝ<VAR>f✝ : ↥(Lp E 1 μ)<VAR>f : ↥(simpleFunc E 1 μ)<GOAL>c • (setToL1 hT) ↑f = (setToL1SCLM α E μ ⋯) f
<VAR>f g : CircleDeg1Lift<VAR>x : ℝ<VAR>m : ℤ<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>(⇑f)^[n] x = x + ↑n * ↑m ↔ f x = x + ↑m
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u v s : Set α<VAR>hs : IsPreconnected s<VAR>P : α → α → Prop<VAR>h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x<VAR>h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z<VAR>x y : α<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>Q : ↑s → ↑s → Prop := fun a b => P ↑a ↑b<GOAL>Q ⟨x, hx⟩ ⟨y, hy⟩
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u v s : Set α<VAR>hs : IsPreconnected s<VAR>P : α → α → Prop<VAR>h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x<VAR>h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z<VAR>x y : α<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>Q : ↑s → ↑s → Prop := fun a b => P ↑a ↑b<VAR>this : PreconnectedSpace ↑s<GOAL>Q ⟨x, hx⟩ ⟨y, hy⟩
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u v s : Set α<VAR>hs : IsPreconnected s<VAR>P : α → α → Prop<VAR>h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x<VAR>h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z<VAR>x y : α<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>Q : ↑s → ↑s → Prop := fun a b => P ↑a ↑b<VAR>this : PreconnectedSpace ↑s<GOAL>∀ (x : { x // x ∈ s }), ∀ᶠ (y : { x // x ∈ s }) in 𝓝 x, Q x y ∧ Q y x
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u v s : Set α<VAR>hs : IsPreconnected s<VAR>P : α → α → Prop<VAR>h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x<VAR>h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z<VAR>x y : α<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>Q : ↑s → ↑s → Prop := fun a b => P ↑a ↑b<VAR>this : PreconnectedSpace ↑s<GOAL>Transitive Q
<VAR>n : ℕ<VAR>K : Type u_1<VAR>inst✝² : CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>inst✝¹ : IsDomain K<VAR>inst✝ : CharZero K<GOAL>minpoly ℤ μ ∣ X ^ n - 1
<VAR>K : Type u_1<VAR>inst✝² : CommRing K<VAR>μ : K<VAR>inst✝¹ : IsDomain K<VAR>inst✝ : CharZero K<VAR>h : IsPrimitiveRoot μ 0<GOAL>minpoly ℤ μ ∣ X ^ 0 - 1
<VAR>n : ℕ<VAR>K : Type u_1<VAR>inst✝² : CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>inst✝¹ : IsDomain K<VAR>inst✝ : CharZero K<VAR>h0 : n > 0<GOAL>minpoly ℤ μ ∣ X ^ n - 1
<VAR>n : ℕ<VAR>K : Type u_1<VAR>inst✝² : CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>inst✝¹ : IsDomain K<VAR>inst✝ : CharZero K<VAR>h0 : n > 0<GOAL>(Polynomial.aeval μ) (X ^ n - 1) = 0
<VAR>n p : ℕ<VAR>pp : Prime p<GOAL>p.properDivisors = {1}
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l l₁ l₂ : List α<VAR>a b : α<VAR>inst✝ : IsTrans α R<VAR>hl : Chain R a l₂<VAR>h : l₁ <+ l₂<GOAL>Chain R a l₁
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l l₁ l₂ : List α<VAR>a b : α<VAR>inst✝ : IsTrans α R<VAR>hl : Pairwise R (a :: l₂)<VAR>h : l₁ <+ l₂<GOAL>Pairwise R (a :: l₁)
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>P : Karoubi C<GOAL>(eqToHom ⋯).f = P.p ≫ eqToHom ⋯
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ p₄ p₅ p₆ : P<VAR>h : 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₄ p₅ p₆<GOAL>AffineIndependent ℝ ![p₁, p₂, p₃] ↔ AffineIndependent ℝ ![p₄, p₅, p₆]
<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>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : NormedGroup E<VAR>inst✝ : NormedGroup F<VAR>a b : E<GOAL>comap norm (𝓝[>] 0) = 𝓝[≠] 1
<VAR>a b : ℝ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>r : ℂ<GOAL>(↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r
<VAR>a b : ℝ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<GOAL>(↑a * ↑b) ^ 0 = ↑a ^ 0 * ↑b ^ 0
<VAR>a b : ℝ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>r : ℂ<VAR>hr : r ≠ 0<GOAL>(↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r
<VAR>b : ℝ<VAR>hb : 0 ≤ b<VAR>r : ℂ<VAR>hr : r ≠ 0<VAR>ha : 0 ≤ 0<GOAL>(↑0 * ↑b) ^ r = ↑0 ^ r * ↑b ^ r
<VAR>a b : ℝ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>r : ℂ<VAR>hr : r ≠ 0<VAR>ha' : 0 < a<GOAL>(↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r
<VAR>a : ℝ<VAR>ha : 0 ≤ a<VAR>r : ℂ<VAR>hr : r ≠ 0<VAR>ha' : 0 < a<VAR>hb : 0 ≤ 0<GOAL>(↑a * ↑0) ^ r = ↑a ^ r * ↑0 ^ r
<VAR>a b : ℝ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>r : ℂ<VAR>hr : r ≠ 0<VAR>ha' : 0 < a<VAR>hb' : 0 < b<GOAL>(↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r
<VAR>a b : ℝ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>r : ℂ<VAR>hr : r ≠ 0<VAR>ha' : 0 < a<VAR>hb' : 0 < b<VAR>ha'' : ↑a ≠ 0<GOAL>(↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r
<VAR>a b : ℝ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>r : ℂ<VAR>hr : r ≠ 0<VAR>ha' : 0 < a<VAR>hb' : 0 < b<VAR>ha'' : ↑a ≠ 0<VAR>hb'' : ↑b ≠ 0<GOAL>(↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r
<VAR>n : ℕ<GOAL>(n + 1 - 0) ^ 0 ≤ n.descFactorial 0
<VAR>n k : ℕ<GOAL>(n + 1 - (k + 1)) ^ (k + 1) ≤ n.descFactorial (k + 1)
<VAR>n k : ℕ<GOAL>(n - k) * (n - k) ^ k ≤ (n - k) * n.descFactorial k
<VAR>n k : ℕ<GOAL>(n - k) ^ k ≤ n.descFactorial k
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ inst✝ : CommSemiring R<VAR>p : MvPolynomial σ R<GOAL>p.totalDegree = 0 ↔ p.IsHomogeneous 0
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹¹ : Ring R<VAR>inst✝¹⁰ : StrongRankCondition R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Free R M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : Module R M'<VAR>inst✝⁴ : Free R M'<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Free R M₁<VAR>inst✝ : Infinite R<VAR>h_lt : lift.{v, u} #R < lift.{u, v} #M<GOAL>Module.rank R M = #M
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹¹ : Ring R<VAR>inst✝¹⁰ : StrongRankCondition R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Free R M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : Module R M'<VAR>inst✝⁴ : Free R M'<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Free R M₁<VAR>inst✝ : Infinite R<VAR>h_lt : lift.{v, u} #R < lift.{u, v} #M<VAR>this : Infinite M<GOAL>Module.rank R M = #M
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹¹ : Ring R<VAR>inst✝¹⁰ : StrongRankCondition R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Free R M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : Module R M'<VAR>inst✝⁴ : Free R M'<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Free R M₁<VAR>inst✝ : Infinite R<VAR>h_lt : lift.{v, u} #R < lift.{u, v} #M<VAR>this : Infinite M<VAR>h : lift.{max u v, v} #M = lift.{v, max u v} #(ChooseBasisIndex R M →₀ R)<GOAL>Module.rank R M = #M
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹¹ : Ring R<VAR>inst✝¹⁰ : StrongRankCondition R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Free R M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : Module R M'<VAR>inst✝⁴ : Free R M'<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Free R M₁<VAR>inst✝ : Infinite R<VAR>h_lt : lift.{v, u} #R < lift.{u, v} #M<VAR>this : Infinite M<VAR>h : lift.{max u v, v} #M = max (lift.{max u v, v} (Module.rank R M)) (lift.{v, u} #R)<GOAL>Module.rank R M = #M
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹¹ : Ring R<VAR>inst✝¹⁰ : StrongRankCondition R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Free R M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : Module R M'<VAR>inst✝⁴ : Free R M'<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Free R M₁<VAR>inst✝ : Infinite R<VAR>h_lt : lift.{v, u} #R < lift.{u, v} #M<VAR>this : Infinite M<VAR>h : lift.{max u v, v} #M = max (lift.{max u v, v} (Module.rank R M)) (lift.{v, u} #R)<GOAL>¬lift.{v, u} #R = lift.{max u v, v} #M
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>γ : Type w<VAR>inst✝ : EMetricSpace γ<VAR>s : Set γ<VAR>hs : IsCompact s<GOAL>∃ t ⊆ s, t.Countable ∧ s = closure t
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>γ : Type w<VAR>inst✝ : EMetricSpace γ<VAR>s : Set γ<VAR>hs : IsCompact s<VAR>t : Set γ<VAR>hts : t ⊆ s<VAR>htc : t.Countable<VAR>hsub : s ⊆ closure t<GOAL>∃ t ⊆ s, t.Countable ∧ s = closure t
<VAR>m n : ℕ+<GOAL>m.gcd n = n.gcd m
<VAR>m n : ℕ+<GOAL>↑(m.gcd n) = ↑(n.gcd m)
<VAR>m n : ℕ+<GOAL>(↑m).gcd ↑n = (↑n).gcd ↑m
<VAR>R : Type u_1<VAR>inst✝³ : Semiring R<VAR>r : R<VAR>p : R[X]<VAR>S : Type u_2<VAR>inst✝² : AddCommMonoid S<VAR>inst✝¹ : Pow S ℕ<VAR>inst✝ : MulActionWithZero R S<VAR>x : S<GOAL>smeval 0 x = 0
<VAR>α : Type u_1<VAR>inst✝¹ : BooleanAlgebra α<VAR>inst✝ : Fintype α<VAR>s : Finset α<VAR>hs : (↑s).Intersecting<GOAL>2 * s.card ≤ Fintype.card α
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>R : Type u_3<VAR>inst✝³ : Semiring R<VAR>inst✝² : Module R F<VAR>inst✝¹ : SMulCommClass 𝕜 R F<VAR>inst✝ : ContinuousConstSMul R F<VAR>n : ℕ<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hx : x ∈ s<VAR>h : UniqueDiffOn 𝕜 s<VAR>f✝ g : 𝕜 → F<VAR>c : 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ContDiffOn 𝕜 (↑n) f s<GOAL>iteratedDerivWithin n (fun z => c * f z) s x = c * iteratedDerivWithin n f s x
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>V' : Type u_3<VAR>G' : SimpleGraph V'<VAR>h : ∀ (n : ℕ), G'.Colorable n → G.Colorable n<GOAL>⨅ n ∈ setOf G.Colorable, ↑n ≤ ⨅ n ∈ setOf G'.Colorable, ↑n
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>V' : Type u_3<VAR>G' : SimpleGraph V'<VAR>h : ∀ (n : ℕ), G'.Colorable n → G.Colorable n<GOAL>∀ (i : ℕ), G'.Colorable i → ⨅ n, ⨅ (_ : G.Colorable n), ↑n ≤ ↑i
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>V' : Type u_3<VAR>G' : SimpleGraph V'<VAR>h : ∀ (n : ℕ), G'.Colorable n → G.Colorable n<VAR>m : ℕ<VAR>hc : G'.Colorable m<VAR>this : G.Colorable m<GOAL>⨅ n, ⨅ (_ : G.Colorable n), ↑n ≤ ↑m
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>V' : Type u_3<VAR>G' : SimpleGraph V'<VAR>h : ∀ (n : ℕ), G'.Colorable n → G.Colorable n<VAR>m : ℕ<VAR>hc : G'.Colorable m<VAR>this : G.chromaticNumber ≤ ↑m<GOAL>⨅ n, ⨅ (_ : G.Colorable n), ↑n ≤ ↑m
<VAR>x : ℝ<GOAL>(↑(projIcc 0 1 ⋯ x)).smoothTransition = x.smoothTransition
<VAR>x✝ x : ℝ<VAR>hx : x < 0<GOAL>x.smoothTransition = smoothTransition 0
<VAR>x✝ x : ℝ<VAR>hx : 1 < x<GOAL>x.smoothTransition = smoothTransition 1
<VAR>S : Finset Λ'<VAR>c : Code<VAR>k : Cont'<VAR>Hk : codeSupp c k ⊆ S<GOAL>Λ'.Supports S (trNormal c k)
<VAR>f g : CircleDeg1Lift<VAR>n : ℤ<GOAL>Function.Commute ⇑f fun x => ↑n + x
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>ι : Type u_3<VAR>inst✝ : DecidableEq ι<VAR>φ ψ : R⟦X⟧<VAR>this : antidiagonal 1 = {(0, 1), (1, 0)}<GOAL>(coeff R 1) (φ * ψ) = (coeff R 1) φ * (constantCoeff R) ψ + (coeff R 1) ψ * (constantCoeff R) φ
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>ι : Type u_3<VAR>inst✝ : DecidableEq ι<VAR>φ ψ : R⟦X⟧<VAR>this : antidiagonal 1 = {(0, 1), (1, 0)}<GOAL>(0, 1) ∉ {(1, 0)}
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>y₁ y₂ : β<GOAL>edist ((WithLp.equiv p (α × β)).symm (0, y₁)) ((WithLp.equiv p (α × β)).symm (0, y₂)) = edist y₁ y₂
<VAR>α : Type u_1<VAR>inst✝³ : GeneralizedBooleanAlgebra α<VAR>inst✝² : DecidableRel Disjoint<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s✝ : Finset α<VAR>u✝ v✝ a b : α<VAR>inst✝ : DecidableEq α<VAR>u v : α<VAR>s : Finset α<VAR>h : filter (fun x => compress u v x ∉ 𝓒 u v s) (𝓒 u v s) = ∅<GOAL>𝓒 u v (𝓒 u v s) = 𝓒 u v s
<VAR>α : Type u_1<VAR>inst✝³ : GeneralizedBooleanAlgebra α<VAR>inst✝² : DecidableRel Disjoint<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s✝ : Finset α<VAR>u✝ v✝ a b : α<VAR>inst✝ : DecidableEq α<VAR>u v : α<VAR>s : Finset α<VAR>h : filter (fun x => compress u v x ∉ 𝓒 u v s) (𝓒 u v s) = ∅<GOAL>filter (fun x => compress u v x ∈ 𝓒 u v s) (𝓒 u v s) ∪ filter (fun x => compress u v x ∉ 𝓒 u v s) (𝓒 u v s) = 𝓒 u v s
<VAR>G : Type u<VAR>inst✝ : Group G<VAR>H : Subgroup G<VAR>g : G<VAR>q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)<VAR>k : ℤ<GOAL>(H.quotientEquivSigmaZMod g) (g ^ k • Quotient.out' q) = ⟨q, ↑k⟩
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : DecidableEq R<VAR>n : ℕ<GOAL>wittPolynomial p R n = ∑ i ∈ range (n + 1), C (↑p ^ i) * X i ^ p ^ (n - i)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : DecidableEq R<VAR>n : ℕ<GOAL>∀ x ∈ range (n + 1), (monomial (single x (p ^ (n - x)))) (↑p ^ x) = C (↑p ^ x) * X x ^ p ^ (n - x)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : DecidableEq R<VAR>n i : ℕ<GOAL>(monomial (single i (p ^ (n - i)))) (↑p ^ i) = C (↑p ^ i) * X i ^ p ^ (n - i)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : DecidableEq R<VAR>n i : ℕ<GOAL>X i ^ 0 = 1
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B₁ B₂ : Set α<VAR>e : α<VAR>hB₁ : M.Base B₁<VAR>hB₂ : M.Base B₂<VAR>hxB₁ : e ∈ B₁<VAR>hxB₂ : e ∉ B₂<GOAL>∃ y, (y ∈ B₂ ∧ y ∉ B₁) ∧ M.Base (insert y (B₁ \ {e}))