ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X✝ : Type u_1<VAR>inst✝² : MeasurableSpace X✝<VAR>X : Type u_2<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : MeasurableSpace.SeparatesPoints X<VAR>x y : X<VAR>x_eq_y : (fun x => diracProba x) x = (fun x => diracProba x) y<GOAL>x = y
<VAR>X✝ : Type u_1<VAR>inst✝² : MeasurableSpace X✝<VAR>X : Type u_2<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : MeasurableSpace.SeparatesPoints X<VAR>x y : X<VAR>x_eq_y : (fun x => diracProba x) x = (fun x => diracProba x) y<GOAL>Measure.dirac x = Measure.dirac y
<VAR>R : Type u<VAR>inst✝² : Ring R<VAR>P : Type v<VAR>inst✝¹ : AddCommGroup P<VAR>inst✝ : Module R P<VAR>ι : Type u_1<VAR>b : Basis ι R P<GOAL>Projective R P
<VAR>R : Type u<VAR>inst✝² : Ring R<VAR>P : Type v<VAR>inst✝¹ : AddCommGroup P<VAR>inst✝ : Module R P<VAR>ι : Type u_1<VAR>b : Basis ι R P<GOAL>Function.LeftInverse ⇑(Finsupp.total P P R id) ⇑((b.constr ℕ) fun i => Finsupp.single (b i) 1)
<VAR>R : Type u<VAR>inst✝² : Ring R<VAR>P : Type v<VAR>inst✝¹ : AddCommGroup P<VAR>inst✝ : Module R P<VAR>ι : Type u_1<VAR>b : Basis ι R P<VAR>m : P<GOAL>(Finsupp.total P P R id) (((b.constr ℕ) fun i => Finsupp.single (b i) 1) m) = m
<VAR>R : Type u<VAR>inst✝² : Ring R<VAR>P : Type v<VAR>inst✝¹ : AddCommGroup P<VAR>inst✝ : Module R P<VAR>ι : Type u_1<VAR>b : Basis ι R P<VAR>m : P<GOAL>((b.repr m).sum fun a b_1 => b_1 • b a) = m
<VAR>β : Type u_1<VAR>ι : Type u_2<VAR>t : ι → TopologicalSpace β<VAR>T : ι → Set (Set β)<VAR>h_basis : ∀ (i : ι), IsTopologicalBasis (T i)<VAR>x✝ : TopologicalSpace β := ⨅ i, t i<GOAL>IsTopologicalBasis {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i}
<VAR>β : Type u_1<VAR>ι : Type u_2<VAR>t : ι → TopologicalSpace β<VAR>T : ι → Set (Set β)<VAR>h_basis : ∀ (i : ι), IsTopologicalBasis (T i)<VAR>x✝ : TopologicalSpace β := ⨅ i, t i<GOAL>∀ u ∈ {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i}, IsOpen u
<VAR>β : Type u_1<VAR>ι : Type u_2<VAR>t : ι → TopologicalSpace β<VAR>T : ι → Set (Set β)<VAR>h_basis : ∀ (i : ι), IsTopologicalBasis (T i)<VAR>x✝ : TopologicalSpace β := ⨅ i, t i<GOAL>∀ (a : β) (u : Set β), a ∈ u → IsOpen u → ∃ v ∈ {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i}, a ∈ v ∧ v ⊆ u
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝⁸ : Field R<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : TopologicalSpace R<VAR>inst✝⁵ : TopologicalSpace V<VAR>inst✝⁴ : TopologicalRing R<VAR>inst✝³ : TopologicalAddGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : SeparatingDual R V<VAR>inst✝ : ContinuousSMul R V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>∃ A, A x = y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝⁸ : Field R<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : TopologicalSpace R<VAR>inst✝⁵ : TopologicalSpace V<VAR>inst✝⁴ : TopologicalRing R<VAR>inst✝³ : TopologicalAddGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : SeparatingDual R V<VAR>inst✝ : ContinuousSMul R V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>G : V →L[R] R<VAR>Gx : G x = 1<VAR>Gy : G y ≠ 0<GOAL>∃ A, A x = y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝⁸ : Field R<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : TopologicalSpace R<VAR>inst✝⁵ : TopologicalSpace V<VAR>inst✝⁴ : TopologicalRing R<VAR>inst✝³ : TopologicalAddGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : SeparatingDual R V<VAR>inst✝ : ContinuousSMul R V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>G : V →L[R] R<VAR>Gx : G x = 1<VAR>Gy : G y ≠ 0<VAR>A : V ≃L[R] V := { toFun := fun z => z + G z • (y - x), map_add' := ⋯, map_smul' := ⋯, invFun := fun z => z + ((G y)⁻¹ * G z) • (x - y), left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }<GOAL>∃ A, A x = y
<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>g : Y → Z<VAR>hf : ContinuousAt f x<VAR>hg : ContinuousAt g (f x)<GOAL>ContinuousAt (g ∘ f) x
<VAR>α : Type u_1<VAR>inst✝ : CancelCommMonoid α<VAR>s : Submonoid α<VAR>a₁ b₁ : α<VAR>a₂ b₂ : ↥s<GOAL>mk a₁ a₂ = mk b₁ b₂ ↔ ↑b₂ * a₁ = ↑a₂ * b₁
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s✝ t✝ : Set α<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>b : β<VAR>hfs : ∀ b ∈ t, InjOn (fun a => f a b) s<VAR>hft : ∀ a ∈ s, InjOn (f a) t<GOAL>(image2 f s t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s✝ t✝ : Set α<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>b : β<VAR>hfs : ∀ b ∈ t, InjOn (fun a => f a b) s<VAR>hft : ∀ a ∈ s, InjOn (f a) t<VAR>h : (image2 f s t).Infinite<GOAL>(s ×ˢ t).Infinite
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s✝ t✝ : Set α<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>b : β<VAR>hfs : ∀ b ∈ t, InjOn (fun a => f a b) s<VAR>hft : ∀ a ∈ s, InjOn (f a) t<GOAL>s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty → (image2 f s t).Infinite
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>I J K : Ideal R<VAR>hIJ : I ≤ J.radical<VAR>hJ : J.radical.FG<GOAL>∃ k, I ^ k ≤ J
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>I J K : Ideal R<VAR>hIJ : I ≤ J.radical<VAR>hJ : J.radical.FG<VAR>k : ℕ<VAR>hk : J.radical ^ k ≤ J<GOAL>∃ k, I ^ k ≤ J
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>I J K : Ideal R<VAR>hIJ : I ≤ J.radical<VAR>hJ : J.radical.FG<VAR>k : ℕ<VAR>hk : J.radical ^ k ≤ J<GOAL>I ^ k ≤ J
<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>w : W<GOAL>‖fourierIntegral e μ L f w‖ ≤ ∫ (v : V), ‖f v‖ ∂μ
<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>w : W<GOAL>∫ (a : V), ‖e (-(L a) w) • f a‖ ∂μ = ∫ (v : V), ‖f v‖ ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>m1 m2 : Multiset α<GOAL>_root_.Disjoint m1.toFinset m2.toFinset ↔ m1.Disjoint m2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>m1 m2 : Multiset α<GOAL>(∀ a ∈ m1.toFinset, ∀ b ∈ m2.toFinset, a ≠ b) ↔ m1.Disjoint m2
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>s : ι → Set Ω<VAR>hsm : ∀ (n : ι), MeasurableSet (s n)<VAR>hs : iIndepSet s κ μ<VAR>S T : Set ι<VAR>hST : Disjoint S T<GOAL>Indep (generateFrom {t | ∃ n ∈ S, s n = t}) (generateFrom {t | ∃ k ∈ T, s k = t}) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>s : ι → Set Ω<VAR>hsm : ∀ (n : ι), MeasurableSet (s n)<VAR>hs : iIndepSet s κ μ<VAR>S T : Set ι<VAR>hST : Disjoint S T<GOAL>Indep (generateFrom (piiUnionInter (fun k => {s k}) S)) (generateFrom (piiUnionInter (fun k => {s k}) T)) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>s : ι → Set Ω<VAR>hsm : ∀ (n : ι), MeasurableSet (s n)<VAR>hs : iIndepSet s κ μ<VAR>S T : Set ι<VAR>hST : Disjoint S T<VAR>t : Set Ω<VAR>ht : t ∈ piiUnionInter (fun k => {s k}) S<GOAL>∀ (n : ι), generateFrom {s n} ≤ _mΩ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>s : ι → Set Ω<VAR>hsm : ∀ (n : ι), MeasurableSet (s n)<VAR>hs : iIndepSet s κ μ<VAR>S T : Set ι<VAR>hST : Disjoint S T<VAR>t : Set Ω<VAR>ht : t ∈ piiUnionInter (fun k => {s k}) T<GOAL>∀ (n : ι), generateFrom {s n} ≤ _mΩ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>s : ι → Set Ω<VAR>hsm : ∀ (n : ι), MeasurableSet (s n)<VAR>hs : iIndepSet s κ μ<VAR>S T : Set ι<VAR>hST : Disjoint S T<GOAL>IsPiSystem (piiUnionInter (fun k => {s k}) S)
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>s : ι → Set Ω<VAR>hsm : ∀ (n : ι), MeasurableSet (s n)<VAR>hs : iIndepSet s κ μ<VAR>S T : Set ι<VAR>hST : Disjoint S T<GOAL>IsPiSystem (piiUnionInter (fun k => {s k}) T)
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>s : ι → Set Ω<VAR>hsm : ∀ (n : ι), MeasurableSet (s n)<VAR>hs : iIndepSet s κ μ<VAR>S T : Set ι<VAR>hST : Disjoint S T<GOAL>IndepSets (piiUnionInter (fun k => {s k}) S) (piiUnionInter (fun k => {s k}) T) κ μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>F : Filter X<VAR>f_closed : IsClosedMap f<VAR>f_cont : Continuous f<VAR>y : Y<GOAL>MapClusterPt y F f ↔ (F.lift' closure ⊓ 𝓟 (f ⁻¹' {y})).NeBot
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<GOAL>NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<GOAL>(∀ (k : Opens α), CompleteLattice.IsCompactElement k) ↔ ∀ (s : Opens α), IsCompact ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G₀ : Type u_3<VAR>inst✝³ : DivInvMonoid G₀<VAR>inst✝² : TopologicalSpace G₀<VAR>inst✝¹ : ContinuousMul G₀<VAR>f : α → G₀<VAR>s : Set α<VAR>l : Filter α<VAR>inst✝ : TopologicalSpace α<VAR>hf : Continuous f<VAR>y : G₀<GOAL>Continuous fun x => f x / y
<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>n : ℕ<VAR>s : Simplex ℝ P n<VAR>p : P<VAR>hr : ∃ r, ∀ (i : Fin (n + 1)), (fun x => dist x p = r) (s.points i)<GOAL>↑(s.orthogonalProjectionSpan p) = s.circumcenter
<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>n : ℕ<VAR>s : Simplex ℝ P n<VAR>p : P<VAR>hr✝ : ∃ r, ∀ (i : Fin (n + 1)), (fun x => dist x p = r) (s.points i)<VAR>hr : ∃ r, ∀ a ∈ Set.range fun i => s.points i, dist a p = r<GOAL>↑(s.orthogonalProjectionSpan p) = s.circumcenter
<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>n : ℕ<VAR>s : Simplex ℝ P n<VAR>p : P<VAR>hr✝ : ∃ r, ∀ (i : Fin (n + 1)), (fun x => dist x p = r) (s.points i)<VAR>hr : ∃ r, ∀ p1 ∈ Set.range fun i => s.points i, dist p1 ↑((EuclideanGeometry.orthogonalProjection (affineSpan ℝ (Set.range fun i => s.points i))) p) = r<GOAL>↑(s.orthogonalProjectionSpan p) = s.circumcenter
<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>n : ℕ<VAR>s : Simplex ℝ P n<VAR>p : P<VAR>hr✝ : ∃ r, ∀ (i : Fin (n + 1)), (fun x => dist x p = r) (s.points i)<VAR>r : ℝ<VAR>hr : ∀ p1 ∈ Set.range fun i => s.points i, dist p1 ↑((EuclideanGeometry.orthogonalProjection (affineSpan ℝ (Set.range fun i => s.points i))) p) = r<GOAL>↑(s.orthogonalProjectionSpan p) = s.circumcenter
<VAR>ι✝ : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>β : Type u_4<VAR>ι : β → Type u_5<VAR>hι : (n : β) → Fintype (ι n)<VAR>s : Set X<VAR>l : Filter β<VAR>r : β → ℝ≥0∞<VAR>hr : Tendsto r l (𝓝 0)<VAR>t : (n : β) → ι n → Set X<VAR>ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), diam (t n i) ≤ r n<VAR>hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i<VAR>m : ℝ≥0∞ → ℝ≥0∞<GOAL>(mkMetric m) s ≤ liminf (fun n => ∑ i : ι n, m (diam (t n i))) l
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝¹ : Category.{uD', uD} D<VAR>inst✝ : HasZeroMorphisms D<VAR>X Y : C<VAR>b : Bicone (pairFunction X Y)<GOAL>b.ι WalkingPair.left ≫ b.π WalkingPair.left = 𝟙 X
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝¹ : Category.{uD', uD} D<VAR>inst✝ : HasZeroMorphisms D<VAR>X Y : C<VAR>b : Bicone (pairFunction X Y)<GOAL>b.ι WalkingPair.right ≫ b.π WalkingPair.left = 0
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝¹ : Category.{uD', uD} D<VAR>inst✝ : HasZeroMorphisms D<VAR>X Y : C<VAR>b : Bicone (pairFunction X Y)<GOAL>b.ι WalkingPair.left ≫ b.π WalkingPair.right = 0
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝¹ : Category.{uD', uD} D<VAR>inst✝ : HasZeroMorphisms D<VAR>X Y : C<VAR>b : Bicone (pairFunction X Y)<GOAL>b.ι WalkingPair.right ≫ b.π WalkingPair.right = 𝟙 Y
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>↑⌊a⌋₊ = ↑⌊a⌋
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H✝ K H : Subgroup G<GOAL>H = ⊥ ∨ ∃ x ∈ H, x ≠ 1
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H✝ K H : Subgroup G<GOAL>(∃ x ∈ H, x ≠ 1) ↔ Nontrivial ↥H
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>p q : α → Prop<VAR>a' : α<GOAL>∃! a, a' = a
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>HasDerivAt (fun x => x * log x) (log x + 1) x
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>DifferentiableAt ℝ (fun x => x * log x) x
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>{0}ᶜ ∈ 𝓝 x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDedekindDomain A<VAR>I J : FractionalIdeal A⁰ K<VAR>hJ : ¬J = 0<GOAL>I / J = I * J⁻¹
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDedekindDomain A<VAR>I J : FractionalIdeal A⁰ K<VAR>hJ : ¬J = 0<GOAL>I / J * J ≤ I * J⁻¹ * J
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDedekindDomain A<VAR>I J : FractionalIdeal A⁰ K<VAR>hJ : ¬J = 0<GOAL>I * J⁻¹ * J ≤ I
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : Invertible 2<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x✝ y✝ z : P<VAR>x y : V<GOAL>midpoint R (x + y) (x - y) = x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : Invertible 2<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x✝ y✝ z : P<VAR>x y : V<GOAL>midpoint R (x - y) (x + y) = x
<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<VAR>h : Sbtw ℝ p₁ p₂ p₁'<VAR>hp₃p₂ : p₃ ≠ p₂<GOAL>∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃ + ↑π
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>X : Type u_5<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<GOAL>IsMeagre s ↔ ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>X : Type u_5<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<GOAL>(∃ x, (∀ t ∈ compl '' x, IsOpen t) ∧ (∀ t ∈ compl '' x, Dense t) ∧ (compl '' x).Countable ∧ ⋂₀ (compl '' x) ⊆ sᶜ) ↔ ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>X : Type u_5<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<GOAL>(∃ x, (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x) ↔ ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>X : Type u_5<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<VAR>x✝ : ∃ x, (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x<VAR>S : Set (Set X)<VAR>hS : ∀ ⦃x : Set X⦄, x ∈ S → IsClosed x ∧ IsNowhereDense x<VAR>hc : (compl '' S).Countable<VAR>hsub : s ⊆ ⋃₀ S<GOAL>S.Countable
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>X : Type u_5<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<GOAL>(∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S) → ∃ x, (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x
<VAR>R : Type u_1<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>a b x✝ y✝ x y p : R<VAR>h : p ∣ x - y<GOAL>p ∣ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) ↔ p ∣ ↑n * y ^ (n - 1)
<VAR>R : Type u_1<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>a b x✝ y✝ x y p : R<VAR>h : (Ideal.Quotient.mk (span {p})) x = (Ideal.Quotient.mk (span {p})) y<GOAL>p ∣ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) ↔ p ∣ ↑n * y ^ (n - 1)
<GOAL>addHaarMeasure Icc01 = volume ↑Icc01 • addHaarMeasure Icc01
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>n : ℕ<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>c : Composition n<VAR>f : ContinuousMultilinearMap 𝕜 (fun _i => F) G<VAR>v : Fin n → E<GOAL>‖f‖ * ∏ i : Fin c.length, ‖p.applyComposition c v i‖ ≤ ‖f‖ * ∏ i : Fin c.length, ‖p (c.blocksFun i)‖ * ∏ j : Fin (c.blocksFun i), ‖(v ∘ ⇑(c.embedding i)) j‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>n : ℕ<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>c : Composition n<VAR>f : ContinuousMultilinearMap 𝕜 (fun _i => F) G<VAR>v : Fin n → E<GOAL>∏ i : Fin c.length, ‖p.applyComposition c v i‖ ≤ ∏ i : Fin c.length, ‖p (c.blocksFun i)‖ * ∏ j : Fin (c.blocksFun i), ‖(v ∘ ⇑(c.embedding i)) j‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>n : ℕ<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>c : Composition n<VAR>f : ContinuousMultilinearMap 𝕜 (fun _i => F) G<VAR>v : Fin n → E<VAR>i : Fin c.length<VAR>_hi : i ∈ Finset.univ<GOAL>‖p.applyComposition c v i‖ ≤ ‖p (c.blocksFun i)‖ * ∏ j : Fin (c.blocksFun i), ‖(v ∘ ⇑(c.embedding i)) j‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>n : ℕ<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>c : Composition n<VAR>f : ContinuousMultilinearMap 𝕜 (fun _i => F) G<VAR>v : Fin n → E<GOAL>‖f‖ * ∏ i : Fin c.length, ‖p (c.blocksFun i)‖ * ∏ j : Fin (c.blocksFun i), ‖(v ∘ ⇑(c.embedding i)) j‖ = (‖f‖ * ∏ i : Fin c.length, ‖p (c.blocksFun i)‖) * ∏ i : Fin c.length, ∏ j : Fin (c.blocksFun i), ‖(v ∘ ⇑(c.embedding i)) j‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>n : ℕ<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>c : Composition n<VAR>f : ContinuousMultilinearMap 𝕜 (fun _i => F) G<VAR>v : Fin n → E<GOAL>(‖f‖ * ∏ i : Fin c.length, ‖p (c.blocksFun i)‖) * ∏ i : Fin c.length, ∏ j : Fin (c.blocksFun i), ‖(v ∘ ⇑(c.embedding i)) j‖ = (‖f‖ * ∏ i : Fin c.length, ‖p (c.blocksFun i)‖) * ∏ i : Fin n, ‖v i‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>n : ℕ<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>c : Composition n<VAR>f : ContinuousMultilinearMap 𝕜 (fun _i => F) G<VAR>v : Fin n → E<GOAL>(‖f‖ * ∏ i : Fin c.length, ‖p (c.blocksFun i)‖) * ∏ i : Fin c.length, ∏ j : Fin (c.blocksFun i), ‖(v ∘ ⇑(c.embedding i)) j‖ = (‖f‖ * ∏ i : Fin c.length, ‖p (c.blocksFun i)‖) * ∏ a : Fin c.length, ∏ s : Fin (c.blocksFun a), ‖v (c.blocksFinEquiv ⟨a, s⟩)‖
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X Y Z : C<VAR>f g : X ⟶ Y<VAR>h : Y ⟶ Z<VAR>w : f ≫ h = g ≫ h<VAR>inst✝² : HasCoequalizer f g<VAR>inst✝¹ : HasCoequalizer (G.map f) (G.map g)<VAR>inst✝ : PreservesColimit (parallelPair f g) G<GOAL>G.map (coequalizer.π f g) ≫ (PreservesCoequalizer.iso G f g).inv = coequalizer.π (G.map f) (G.map g)
<VAR>a b c : ℤ<VAR>h : Fermat42 a b c<GOAL>∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1
<VAR>a b c : ℤ<VAR>h : Fermat42 a b c<VAR>a0 b0 c0 : ℤ<VAR>hf : Minimal a0 b0 c0<GOAL>∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1
<VAR>a b c : ℤ<VAR>h : Fermat42 a b c<VAR>a0 b0 c0 : ℤ<VAR>hf : Minimal a0 b0 c0<VAR>hap : a0 % 2 = 0<GOAL>∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1
<VAR>a b c : ℤ<VAR>h : Fermat42 a b c<VAR>a0 b0 c0 : ℤ<VAR>hf : Minimal a0 b0 c0<VAR>hap : a0 % 2 = 1<GOAL>∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : LieRing L<VAR>inst✝¹¹ : LieAlgebra R L<VAR>inst✝¹⁰ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : LieRingModule L M<VAR>inst✝⁶ : LieModule R L M<VAR>M₂ : Type u_5<VAR>inst✝⁵ : AddCommGroup M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : LieRingModule L M₂<VAR>inst✝² : LieModule R L M₂<VAR>χ : L → R<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>inst✝¹ : IsNoetherian R M<VAR>inst✝ : IsArtinian R M<VAR>N₁ N₂ : LieSubmodule R L M<VAR>h : Codisjoint N₁ N₂<GOAL>LieSubmodule.map N₁.incl (posFittingComp R L ↥↑N₁) ⊔ LieSubmodule.map N₂.incl (posFittingComp R L ↥↑N₂) = posFittingComp R L M