ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F✝ : Type u_1<VAR>inst✝⁴ : Field F✝<VAR>E✝ : Type u_2<VAR>inst✝³ : Field E✝<VAR>inst✝² : Algebra F✝ E✝<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>E : Type u_4<VAR>inst✝ : Field E<VAR>i : F →+* E<VAR>n : ℕ<VAR>a : F<VAR>ha : a ≠ 0<VAR>h : Splits i (X ^ n - C a)<VAR>ha' : i a ≠ 0<VAR>hn : ¬n = 0<VAR>hn' : 0 < n<VAR>hn'' : (X ^ n - C a).degree ≠ 0<VAR>b : E<VAR>hb : b ^ n = i a<VAR>hb' : b ≠ 0<VAR>s : Multiset E := (Polynomial.map i (X ^ n - C a)).roots<VAR>hs : Polynomial.map i (X ^ n - C a) = (Multiset.map (fun a => X - C a) s).prod<VAR>hs' : Multiset.card s = n<VAR>C_mul_C : C (i a⁻¹) * C (i a) = 1<VAR>key1 : Polynomial.map i (X ^ n - 1) = C (i a⁻¹) * (Polynomial.map i (X ^ n - C a)).comp (C b * X)<VAR>key2 : ((fun q => q.comp (C b * X)) ∘ fun c => X - C c) = fun c => C b * (X - C (c / b))<GOAL>Polynomial.map i (X ^ n - 1) = (Multiset.map ((fun a => X - C a) ∘ fun c => c / b) s).prod
<VAR>F✝ : Type u_1<VAR>inst✝⁴ : Field F✝<VAR>E✝ : Type u_2<VAR>inst✝³ : Field E✝<VAR>inst✝² : Algebra F✝ E✝<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>E : Type u_4<VAR>inst✝ : Field E<VAR>i : F →+* E<VAR>n : ℕ<VAR>a : F<VAR>ha : a ≠ 0<VAR>h : Splits i (X ^ n - C a)<VAR>ha' : i a ≠ 0<VAR>hn : ¬n = 0<VAR>hn' : 0 < n<VAR>hn'' : (X ^ n - C a).degree ≠ 0<VAR>b : E<VAR>hb : b ^ n = i a<VAR>hb' : b ≠ 0<VAR>s : Multiset E := (Polynomial.map i (X ^ n - C a)).roots<VAR>hs : Polynomial.map i (X ^ n - C a) = (Multiset.map (fun a => X - C a) s).prod<VAR>hs' : Multiset.card s = n<VAR>C_mul_C : C (i a⁻¹) * C (i a) = 1<VAR>key1 : Polynomial.map i (X ^ n - 1) = C (i a⁻¹) * (Polynomial.map i (X ^ n - C a)).comp (C b * X)<VAR>key2 : ((fun q => q.comp (C b * X)) ∘ fun c => X - C c) = fun c => C b * (X - C (c / b))<GOAL>(Multiset.map (fun c => X - C (c / b)) s).prod = (Multiset.map ((fun a => X - C a) ∘ fun c => c / b) s).prod
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t u : Multiset α<VAR>a b : α<GOAL>s ∪ 0 = s
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝³ : CommMonoid M<VAR>inst✝² : CommMonoid N<VAR>inst✝¹ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>inst✝ : CommRing R<VAR>ζ : Rˣ<VAR>h : IsPrimitiveRoot ζ k<VAR>i : ℕ<VAR>this : ↑i = ↑↑i<GOAL>h.zmodEquivZPowers ↑i = Additive.ofMul ⟨ζ ^ i, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α →ₘ[μ] β<GOAL>mk ↑f ⋯ = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α →ₘ[μ] β<GOAL>mk ↑f ⋯ = Quotient.mk'' (Quotient.out' f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α →ₘ[μ] β<VAR>g : { f // AEStronglyMeasurable f μ } := Quotient.out' f<GOAL>mk ↑f ⋯ = Quotient.mk'' g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α →ₘ[μ] β<VAR>g : { f // AEStronglyMeasurable f μ } := Quotient.out' f<VAR>this : g = ⟨↑g, ⋯⟩<GOAL>mk ↑f ⋯ = Quotient.mk'' g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α →ₘ[μ] β<VAR>g : { f // AEStronglyMeasurable f μ } := Quotient.out' f<VAR>this : g = ⟨↑g, ⋯⟩<GOAL>↑f =ᶠ[ae μ] ↑g
<VAR>α : Type u_1<VAR>t t₁ t₂ : TopologicalSpace α<VAR>s : Set α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : DiscreteTopology α<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>f : ι → α<GOAL>DenseRange f ↔ Surjective f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDF f κ ν<VAR>a : α<VAR>q : ℚ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∫ (b : β) in s, ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑q ∂ν a = ((κ a) (s ×ˢ Iic ↑q)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDF f κ ν<VAR>a : α<VAR>q : ℚ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∀ᵐ (x : β) ∂ν a, x ∈ s → ↑(stieltjesOfMeasurableRat f ⋯ (a, x)) ↑q = (fun b => f (a, b) q) x
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>x : M<VAR>y : M'<VAR>hs : s ⊆ (extChartAt I x).source<VAR>h2s : MapsTo f s (extChartAt I' y).source<GOAL>ContMDiffOn I I' n f s ↔ ContDiffOn 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) '' s)
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>x : M<VAR>y : M'<VAR>hs : s ⊆ (chartAt H x).source<VAR>h2s : MapsTo f s (chartAt H' y).source<GOAL>ContMDiffOn I I' n f s ↔ ContDiffOn 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) '' s)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>s : Finset ℕ<GOAL>∀ (f : R[X]), f.support = s → (toLaurent f).support = Finset.map Nat.castEmbedding s
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<GOAL>∀ (f : R[X]), f.support = ∅ → (toLaurent f).support = Finset.map Nat.castEmbedding ∅
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<GOAL>∀ ⦃a : ℕ⦄ {s : Finset ℕ}, a ∉ s → (∀ (f : R[X]), f.support = s → (toLaurent f).support = Finset.map Nat.castEmbedding s) → ∀ (f : R[X]), f.support = insert a s → (toLaurent f).support = Finset.map Nat.castEmbedding (insert a s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r : α → α → Prop<VAR>f✝ g : Filter α<VAR>inst✝ : Preorder α<VAR>f : Filter β<VAR>u : β → α<VAR>b : α<VAR>hb : b ∈ lowerBounds (range u)<GOAL>∀ (x : β), u x ≥ b
<VAR>R : Type u<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : IsPrincipalIdealRing R<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type (max u v)<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : R<VAR>hp : Irreducible p<VAR>hM : IsTorsion' M ↥(Submonoid.powers p)<VAR>dec : (x : M) → Decidable (x = 0)<VAR>x : M<GOAL>torsionOf R M x = Ideal.span {p ^ Nat.find ⋯}
<VAR>R : Type u<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : IsPrincipalIdealRing R<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type (max u v)<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : R<VAR>hp : Irreducible p<VAR>hM : IsTorsion' M ↥(Submonoid.powers p)<VAR>dec : (x : M) → Decidable (x = 0)<VAR>x : M<GOAL>Associates.mk (generator (torsionOf R M x)) = Associates.mk p ^ Nat.find ⋯
<VAR>R : Type u<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : IsPrincipalIdealRing R<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type (max u v)<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : R<VAR>hp : Irreducible p<VAR>hM : IsTorsion' M ↥(Submonoid.powers p)<VAR>dec : (x : M) → Decidable (x = 0)<VAR>x : M<VAR>prop : (fun n => p ^ n • x = 0) = fun n => Associates.mk (generator (torsionOf R M x)) ∣ Associates.mk p ^ n<GOAL>Associates.mk (generator (torsionOf R M x)) = Associates.mk p ^ Nat.find ⋯
<VAR>R : Type u<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : IsPrincipalIdealRing R<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type (max u v)<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : R<VAR>hp : Irreducible p<VAR>hM : IsTorsion' M ↥(Submonoid.powers p)<VAR>dec : (x : M) → Decidable (x = 0)<VAR>x : M<VAR>prop : (fun n => p ^ n • x = 0) = fun n => Associates.mk (generator (torsionOf R M x)) ∣ Associates.mk p ^ n<VAR>this : ∃ n, p ^ n • x = 0<GOAL>Associates.mk (generator (torsionOf R M x)) = Associates.mk p ^ Nat.find ⋯
<VAR>R : Type u<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : IsPrincipalIdealRing R<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type (max u v)<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : R<VAR>hp : Irreducible p<VAR>hM : IsTorsion' M ↥(Submonoid.powers p)<VAR>dec : (x : M) → Decidable (x = 0)<VAR>x : M<VAR>prop : (fun n => p ^ n • x = 0) = fun n => Associates.mk (generator (torsionOf R M x)) ∣ Associates.mk p ^ n<VAR>this : ∃ n, Associates.mk (generator (torsionOf R M x)) ∣ Associates.mk p ^ n<GOAL>Associates.mk (generator (torsionOf R M x)) = Associates.mk p ^ Nat.find ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLattice α<VAR>s t : Set α<VAR>a✝ b : α<VAR>hι : Nonempty ι<VAR>a : α<GOAL>⨆ x, a = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → α<VAR>g : β → β<VAR>x : α × β<VAR>a : α<VAR>b : β<VAR>m n : ℕ<GOAL>minimalPeriod f x.1 ∣ minimalPeriod (Prod.map f g) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → α<VAR>g : β → β<VAR>x : α × β<VAR>a : α<VAR>b : β<VAR>m n : ℕ<GOAL>minimalPeriod f x.1 ∣ (minimalPeriod f x.1).lcm (minimalPeriod g x.2)
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v w : V<GOAL>G.edist u v = 0 ↔ u = v
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s : Finset β<VAR>f : β → α<VAR>h : s.Nonempty<GOAL>∃ x ∈ s, ∀ x' ∈ s, f x' ≤ f x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s : Finset β<VAR>f : β → α<VAR>h : s.Nonempty<VAR>y : α<VAR>hy : (image f s).max = ↑y<GOAL>∃ x ∈ s, ∀ x' ∈ s, f x' ≤ f x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s : Finset β<VAR>f : β → α<VAR>h : s.Nonempty<VAR>x : β<VAR>hx : x ∈ s<VAR>hy : (image f s).max = ↑(f x)<GOAL>∃ x ∈ s, ∀ x' ∈ s, f x' ≤ f x
<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>ha : a ≠ 0<GOAL>(C a * X + C b).degree = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h : c ≤ max a b<GOAL>Ioc a b ∪ Ioi c = Ioi (min a c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>hab : a ≤ b<VAR>h : c ≤ b<GOAL>Ioc a b ∪ Ioi c = Ioi (min a c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>hab : b ≤ a<VAR>h : c ≤ a<GOAL>Ioc a b ∪ Ioi c = Ioi (min a c)
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p q : ℕ<VAR>f : R[X]<VAR>n : ℕ<GOAL>(contract 1 f).coeff n = f.coeff n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>H : a % b = 0<GOAL>a = b * (a / b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : NormedAddCommGroup β<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>𝕜 : Type u_5<VAR>inst✝ : RCLike 𝕜<VAR>f : α → 𝕜<VAR>hf : Integrable f μ<GOAL>Integrable (fun x => RCLike.im (f x)) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : NormedAddCommGroup β<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>𝕜 : Type u_5<VAR>inst✝ : RCLike 𝕜<VAR>f : α → 𝕜<VAR>hf : Memℒp f 1 μ<GOAL>Memℒp (fun x => RCLike.im (f x)) 1 μ
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>i : ℕ<VAR>s : Stream' α<VAR>n✝ : ℕ<GOAL>(drop i s).tail.get n✝ = (drop (i + 1) s).get n✝
<VAR>α✝ : Sort u_1<VAR>cmp : α✝ → α✝ → Ordering<VAR>x y : α✝<VAR>inst✝ : OrientedCmp cmp<GOAL>cmp x y = Ordering.gt ↔ cmp y x = Ordering.lt
<VAR>α✝ : Sort u_1<VAR>cmp : α✝ → α✝ → Ordering<VAR>x y : α✝<VAR>inst✝ : OrientedCmp cmp<GOAL>cmp y x = Ordering.gt.swap ↔ cmp y x = Ordering.lt
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>inst✝² : (i : ι) → AddCommMonoid (β i)<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>x : ⨁ (i : ι), β i<GOAL>∑ i : ι, (of β i) (x i) = x
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>inst✝² : (i : ι) → AddCommMonoid (β i)<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>x : ⨁ (i : ι), β i<VAR>i : ι<GOAL>(∑ i : ι, (of β i) (x i)) i = x i
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>inst✝² : (i : ι) → AddCommMonoid (β i)<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>x : ⨁ (i : ι), β i<VAR>i : ι<GOAL>∑ a : ι, ((of β a) (x a)) i = x i
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i : N<VAR>p : ↑(Ω^ N X x)<VAR>y✝ : N → ↑I<GOAL>(fromLoop i (toLoop i p)) y✝ = p y✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : (a : α) → DecidablePred (Associated a)<VAR>s : Multiset α<VAR>n : α<VAR>h : ∀ a ∈ s, Prime a<VAR>div : ∀ a ∈ s, a ∣ n<VAR>uniq : ∀ (a : α), countP (Associated a) s ≤ 1<GOAL>s.prod ∣ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : (a : α) → DecidablePred (Associated a)<VAR>n : α<VAR>h : ∀ a ∈ 0, Prime a<VAR>div : ∀ a ∈ 0, a ∣ n<VAR>uniq : ∀ (a : α), countP (Associated a) 0 ≤ 1<GOAL>prod 0 ∣ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : (a : α) → DecidablePred (Associated a)<VAR>a : α<VAR>s : Multiset α<VAR>induct : ∀ (n : α), (∀ a ∈ s, Prime a) → (∀ a ∈ s, a ∣ n) → (∀ (a : α), countP (Associated a) s ≤ 1) → s.prod ∣ n<VAR>n : α<VAR>h : ∀ a_1 ∈ a ::ₘ s, Prime a_1<VAR>div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ n<VAR>uniq : ∀ (a_1 : α), countP (Associated a_1) (a ::ₘ s) ≤ 1<GOAL>(a ::ₘ s).prod ∣ n
<VAR>R : Type u_1<VAR>inst✝⁵ : Ring R<VAR>A : Type u_2<VAR>inst✝⁴ : CommRing A<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>U U₁ U₂ : Submodule R M<VAR>x x₁ x₂ y y₁ y₂ z z₁ z₂ : M<VAR>N : Type u_4<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>V V₁ V₂ : Submodule R N<VAR>hxy : x ≡ y [SMOD U]<VAR>c : R<GOAL>c • x ≡ c • y [SMOD U]
<VAR>R : Type u_1<VAR>inst✝⁵ : Ring R<VAR>A : Type u_2<VAR>inst✝⁴ : CommRing A<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>U U₁ U₂ : Submodule R M<VAR>x x₁ x₂ y y₁ y₂ z z₁ z₂ : M<VAR>N : Type u_4<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>V V₁ V₂ : Submodule R N<VAR>hxy : Submodule.Quotient.mk x = Submodule.Quotient.mk y<VAR>c : R<GOAL>Submodule.Quotient.mk (c • x) = Submodule.Quotient.mk (c • y)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p✝ q : R[X]<VAR>iR : DecidableEq R<VAR>p : R[X]<VAR>ip0 : Decidable (p = 0)<GOAL>p.roots = if h : p = 0 then ∅ else Classical.choose ⋯
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p✝ q p : R[X]<VAR>ip0 : Decidable (p = 0)<GOAL>p.roots = if h : p = 0 then ∅ else Classical.choose ⋯
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p✝ q p : R[X]<GOAL>p.roots = if h : p = 0 then ∅ else Classical.choose ⋯
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>s : (i : ι) → Set (π i)<GOAL>IsConnected (univ.pi s) ↔ ∀ (i : ι), IsConnected (s i)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>s : (i : ι) → Set (π i)<GOAL>(univ.pi s).Nonempty → (IsPreconnected (univ.pi s) ↔ ∀ (x : ι), IsPreconnected (s x))
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>s : (i : ι) → Set (π i)<VAR>hne : (univ.pi s).Nonempty<VAR>hc : IsPreconnected (univ.pi s)<VAR>i : ι<GOAL>IsPreconnected (s i)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>s : (i : ι) → Set (π i)<VAR>hne : (univ.pi s).Nonempty<VAR>hc : IsPreconnected (univ.pi s)<VAR>i : ι<GOAL>IsPreconnected ((fun f => f i) '' univ.pi s)
<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<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>(∡ p₂ p₃ p₁).sin * dist p₁ p₃ = dist p₁ p₂
<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<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<VAR>hs : (∡ p₂ p₃ p₁).sign = 1<GOAL>(∡ p₂ p₃ p₁).sin * dist p₁ p₃ = dist p₁ p₂
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : CommRing 𝕜<VAR>V : Type u_2<VAR>inst✝¹⁰ : AddCommGroup V<VAR>inst✝⁹ : Module 𝕜 V<VAR>inst✝⁸ : MeasurableSpace V<VAR>W : Type u_3<VAR>inst✝⁷ : AddCommGroup W<VAR>inst✝⁶ : Module 𝕜 W<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℂ F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℂ G<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : Measure V<VAR>L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜<VAR>f : V → E<VAR>r : ℂ<VAR>w : W<GOAL>fourierIntegral e μ L (r • f) w = (r • fourierIntegral e μ L f) w
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : CommRing 𝕜<VAR>V : Type u_2<VAR>inst✝¹⁰ : AddCommGroup V<VAR>inst✝⁹ : Module 𝕜 V<VAR>inst✝⁸ : MeasurableSpace V<VAR>W : Type u_3<VAR>inst✝⁷ : AddCommGroup W<VAR>inst✝⁶ : Module 𝕜 W<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℂ F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℂ G<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : Measure V<VAR>L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜<VAR>f : V → E<VAR>r : ℂ<VAR>w : W<GOAL>∫ (v : V), e (-(L v) w) • r • f v ∂μ = ∫ (a : V), r • e (-(L a) w) • f a ∂μ
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : CommRing 𝕜<VAR>V : Type u_2<VAR>inst✝¹⁰ : AddCommGroup V<VAR>inst✝⁹ : Module 𝕜 V<VAR>inst✝⁸ : MeasurableSpace V<VAR>W : Type u_3<VAR>inst✝⁷ : AddCommGroup W<VAR>inst✝⁶ : Module 𝕜 W<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℂ F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℂ G<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : Measure V<VAR>L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜<VAR>f : V → E<VAR>r : ℂ<VAR>w : W<VAR>v : V<GOAL>e (-(L v) w) • r • f v = r • e (-(L v) w) • f v
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>u : α<VAR>p : G.Walk u u<VAR>hOdd : Odd p.length<VAR>h : ¬3 ≤ G.chromaticNumber<GOAL>False
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>u : α<VAR>p : G.Walk u u<VAR>hOdd : Odd p.length<VAR>h : ¬3 ≤ G.chromaticNumber<VAR>h' : G.chromaticNumber ≤ 2<GOAL>False
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>u : α<VAR>p : G.Walk u u<VAR>hOdd : Odd p.length<VAR>h : ¬3 ≤ G.chromaticNumber<VAR>h' : G.chromaticNumber ≤ 2<VAR>c : G.Coloring (Fin 2) := Nonempty.some ⋯<GOAL>False
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>u : α<VAR>p : G.Walk u u<VAR>hOdd : Odd p.length<VAR>h : ¬3 ≤ G.chromaticNumber<VAR>h' : G.chromaticNumber ≤ 2<VAR>c : G.Coloring (Fin 2) := Nonempty.some ⋯<VAR>c' : G.Coloring Bool := (G.recolorOfEquiv finTwoEquiv) c<GOAL>False
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>u : α<VAR>p : G.Walk u u<VAR>hOdd : Odd p.length<VAR>h : ¬3 ≤ G.chromaticNumber<VAR>h' : G.chromaticNumber ≤ 2<VAR>c : G.Coloring (Fin 2) := Nonempty.some ⋯<VAR>c' : G.Coloring Bool := (G.recolorOfEquiv finTwoEquiv) c<VAR>this : ¬c' u = true ↔ c' u = true<GOAL>False
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>α : Type u_3<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : NoBotOrder α<VAR>a : α<GOAL>∃ b, b < a