ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : DecidableEq R<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)<GOAL>n ∈ (xInTermsOfW p ℚ n).vars ∧ (xInTermsOfW p ℚ n).vars ⊆ range (n + 1)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : DecidableEq R<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)<GOAL>n ∈ {n} ∪ (∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)).vars ∧ {n} ∪ (∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)).vars ⊆ {n} ∪ range n
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : DecidableEq R<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)<GOAL>Disjoint (X n).vars (∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)).vars
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : DecidableEq R<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)<VAR>i : ℕ<GOAL>i ∈ (∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)).vars → i ∈ range n
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : DecidableEq R<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)<GOAL>n ∉ (∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)).vars
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>x : L<VAR>hx : x ∈ rootSpace H ⇑(chainTop (⇑α) β)<GOAL>↑(chainLength α β) • x = ⁅coroot α, x⁆
<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✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<GOAL>b ∈ ball a r ↔ ‖b / a‖ < r
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : Semiring R₂<VAR>inst✝¹⁰ : Semiring R₃<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R₂ M₂<VAR>inst✝⁴ : Module R₃ M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>p p' : Submodule R M<VAR>q q' : Submodule R₂ M₂<VAR>x : M<VAR>inst✝² : RingHomSurjective σ₁₂<VAR>F : Type u_9<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>this : ∃ x, x ∈ p<GOAL>∀ (x : M₂), x ∈ map 0 p ↔ x ∈ ⊥
<VAR>η : Type u_1<VAR>α : Type u_2<VAR>ι : Type u_3<VAR>κ✝ : Type u_4<VAR>M : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : AddCommMonoid M<VAR>S : Finset M<VAR>inst✝ : Finite κ<VAR>C : M → κ<GOAL>∃ a > 0, ∃ b c, ∀ s ∈ S, C (a • s + b) = c
<VAR>η : Type u_1<VAR>α : Type u_2<VAR>ι✝ : Type u_3<VAR>κ✝ : Type u_4<VAR>M : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : AddCommMonoid M<VAR>S : Finset M<VAR>inst✝ : Finite κ<VAR>C : M → κ<VAR>ι : Type<VAR>_inst : Fintype ι<VAR>hι : ∀ (C : (ι → { x // x ∈ S }) → κ), ∃ l, Line.IsMono C l<GOAL>∃ a > 0, ∃ b c, ∀ s ∈ S, C (a • s + b) = c
<VAR>η : Type u_1<VAR>α : Type u_2<VAR>ι✝ : Type u_3<VAR>κ✝ : Type u_4<VAR>M : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : AddCommMonoid M<VAR>S : Finset M<VAR>inst✝ : Finite κ<VAR>C : M → κ<VAR>ι : Type<VAR>_inst : Fintype ι<VAR>l : Line { x // x ∈ S } ι<VAR>c : κ<VAR>hl : ∀ (x : { x // x ∈ S }), (fun v => C (∑ i : ι, ↑(v i))) ((fun x i => (l.idxFun i).getD x) x) = c<VAR>s : Finset ι := Finset.filter (fun i => l.idxFun i = none) Finset.univ<VAR>hs : s = Finset.filter (fun i => l.idxFun i = none) Finset.univ<GOAL>∃ a > 0, ∃ b c, ∀ s ∈ S, C (a • s + b) = c
<VAR>η : Type u_1<VAR>α : Type u_2<VAR>ι✝ : Type u_3<VAR>κ✝ : Type u_4<VAR>M : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : AddCommMonoid M<VAR>S : Finset M<VAR>inst✝ : Finite κ<VAR>C : M → κ<VAR>ι : Type<VAR>_inst : Fintype ι<VAR>l : Line { x // x ∈ S } ι<VAR>c : κ<VAR>hl : ∀ (x : { x // x ∈ S }), (fun v => C (∑ i : ι, ↑(v i))) ((fun x i => (l.idxFun i).getD x) x) = c<VAR>s : Finset ι := Finset.filter (fun i => l.idxFun i = none) Finset.univ<VAR>hs : s = Finset.filter (fun i => l.idxFun i = none) Finset.univ<GOAL>⋯.choose ∈ s
<VAR>η : Type u_1<VAR>α : Type u_2<VAR>ι✝ : Type u_3<VAR>κ✝ : Type u_4<VAR>M : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : AddCommMonoid M<VAR>S : Finset M<VAR>inst✝ : Finite κ<VAR>C : M → κ<VAR>ι : Type<VAR>_inst : Fintype ι<VAR>l : Line { x // x ∈ S } ι<VAR>c : κ<VAR>hl : ∀ (x : { x // x ∈ S }), (fun v => C (∑ i : ι, ↑(v i))) ((fun x i => (l.idxFun i).getD x) x) = c<VAR>s : Finset ι := Finset.filter (fun i => l.idxFun i = none) Finset.univ<VAR>hs : s = Finset.filter (fun i => l.idxFun i = none) Finset.univ<VAR>i : ι<GOAL>{ x // x ∈ S } → M
<VAR>η : Type u_1<VAR>α : Type u_2<VAR>ι✝ : Type u_3<VAR>κ✝ : Type u_4<VAR>M : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : AddCommMonoid M<VAR>S : Finset M<VAR>inst✝ : Finite κ<VAR>C : M → κ<VAR>ι : Type<VAR>_inst : Fintype ι<VAR>l : Line { x // x ∈ S } ι<VAR>c : κ<VAR>hl : ∀ (x : { x // x ∈ S }), (fun v => C (∑ i : ι, ↑(v i))) ((fun x i => (l.idxFun i).getD x) x) = c<VAR>s : Finset ι := Finset.filter (fun i => l.idxFun i = none) Finset.univ<VAR>hs : s = Finset.filter (fun i => l.idxFun i = none) Finset.univ<GOAL>∀ s_1 ∈ S, C (s.card • s_1 + ∑ i ∈ sᶜ, (Option.map (?m.43407 i) (l.idxFun i)).getD 0) = c
<VAR>η : Type u_1<VAR>α : Type u_2<VAR>ι✝ : Type u_3<VAR>κ✝ : Type u_4<VAR>M : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : AddCommMonoid M<VAR>S : Finset M<VAR>inst✝ : Finite κ<VAR>C : M → κ<VAR>ι : Type<VAR>_inst : Fintype ι<VAR>l : Line { x // x ∈ S } ι<VAR>c : κ<VAR>s : Finset ι := Finset.filter (fun i => l.idxFun i = none) Finset.univ<VAR>hs : s = Finset.filter (fun i => l.idxFun i = none) Finset.univ<VAR>x : M<VAR>xs : x ∈ S<GOAL>s.card • x + ∑ i ∈ sᶜ, (Option.map (fun m => ↑m) (l.idxFun i)).getD 0 = ∑ i : ι, ↑((fun x i => (l.idxFun i).getD x) ⟨x, xs⟩ i)
<VAR>η : Type u_1<VAR>α : Type u_2<VAR>ι✝ : Type u_3<VAR>κ✝ : Type u_4<VAR>M : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : AddCommMonoid M<VAR>S : Finset M<VAR>inst✝ : Finite κ<VAR>C : M → κ<VAR>ι : Type<VAR>_inst : Fintype ι<VAR>l : Line { x // x ∈ S } ι<VAR>c : κ<VAR>s : Finset ι := Finset.filter (fun i => l.idxFun i = none) Finset.univ<VAR>hs : s = Finset.filter (fun i => l.idxFun i = none) Finset.univ<VAR>x : M<VAR>xs : x ∈ S<GOAL>s.card • x + ∑ i ∈ sᶜ, (Option.map (fun m => ↑m) (l.idxFun i)).getD 0 = ∑ i ∈ s, ↑((fun x i => (l.idxFun i).getD x) ⟨x, xs⟩ i) + ∑ i ∈ sᶜ, ↑((fun x i => (l.idxFun i).getD x) ⟨x, xs⟩ i)
<VAR>n : ℕ<VAR>h : 2 ≤ n<GOAL>(finRotate n).support = Finset.univ
<VAR>m : ℕ<VAR>h : 2 ≤ 2 + m<GOAL>(finRotate (2 + m)).support = Finset.univ
<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>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>s : Set M<VAR>x✝ : M<VAR>x : M × M'<GOAL>HasMFDerivAt (I.prod I') I Prod.fst x (ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))
<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>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>s : Set M<VAR>x✝ : M<VAR>x : M × M'<GOAL>HasFDerivWithinAt (writtenInExtChartAt (I.prod I') I x Prod.fst) (ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)) (range ↑(I.prod I')) (↑(extChartAt (I.prod I') x) 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>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>s : Set M<VAR>x✝ : M<VAR>x : M × M'<VAR>this : ∀ᶠ (y : E × E') in 𝓝[range ↑(I.prod I')] ↑(extChartAt (I.prod I') x) x, (↑(extChartAt I x.1) ∘ Prod.fst ∘ ↑(extChartAt (I.prod I') x).symm) y = y.1<GOAL>HasFDerivWithinAt (writtenInExtChartAt (I.prod I') I x Prod.fst) (ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)) (range ↑(I.prod I')) (↑(extChartAt (I.prod I') x) 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>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>s : Set M<VAR>x✝ : M<VAR>x : M × M'<VAR>this : ∀ᶠ (y : E × E') in 𝓝[range ↑(I.prod I')] ↑(extChartAt (I.prod I') x) x, (↑(extChartAt I x.1) ∘ Prod.fst ∘ ↑(extChartAt (I.prod I') x).symm) y = y.1<GOAL>(↑(extChartAt I x.1) ∘ Prod.fst ∘ ↑(extChartAt (I.prod I') x).symm) (↑(extChartAt (I.prod I') x) x) = (↑(extChartAt (I.prod I') x) x).1
<VAR>d✝ : ℤ<VAR>c d x y z w : ℕ<VAR>xy : SqLe x c y d<VAR>zw : SqLe z c w d<GOAL>c * (x * z) * (c * (x * z)) ≤ d * (y * w) * (d * (y * w))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>c : Cardinal.{u_3}<GOAL>↑n < toPartENat c ↔ ↑n < c
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x : α<VAR>s✝ t : Set α<VAR>r : ℝ<VAR>f : β → α<VAR>s : Set β<GOAL>(∃ C, ∀ ⦃x : α⦄, x ∈ f '' s → ∀ ⦃y : α⦄, y ∈ f '' s → dist x y ≤ C) ↔ ∃ C, ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ C
<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>s : Sphere P<VAR>p₁ p₂ p₃ p₄ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₃ : p₃ ∈ s<VAR>hp₄ : p₄ ∈ s<VAR>hp₂p₁ : p₂ ≠ p₁<VAR>hp₂p₄ : p₂ ≠ p₄<VAR>hp₃p₁ : p₃ ≠ p₁<VAR>hp₃p₄ : p₃ ≠ p₄<GOAL>2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ 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>s : Sphere P<VAR>p₁ p₂ p₃ p₄ : P<VAR>hp₁ : ‖p₁ -ᵥ s.center‖ = s.radius<VAR>hp₂ : ‖p₂ -ᵥ s.center‖ = s.radius<VAR>hp₃ : ‖p₃ -ᵥ s.center‖ = s.radius<VAR>hp₄ : ‖p₄ -ᵥ s.center‖ = s.radius<VAR>hp₂p₁ : p₂ ≠ p₁<VAR>hp₂p₄ : p₂ ≠ p₄<VAR>hp₃p₁ : p₃ ≠ p₁<VAR>hp₃p₄ : p₃ ≠ p₄<GOAL>2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
<VAR>e : ℝ<VAR>d : ℕ<VAR>n : ℤ<VAR>inv : Invertible ↑d<VAR>eq : e = ↑n * ⅟↑d<VAR>h : decide (1 < ↑n / ↑d) = true<GOAL>0 < Real.log e
<VAR>e : ℝ<VAR>d : ℕ<VAR>n : ℤ<VAR>inv : Invertible ↑d<VAR>eq : e = ↑n * ⅟↑d<VAR>h : decide (1 < ↑n / ↑d) = true<GOAL>0 < Real.log (↑n / ↑d)
<VAR>e : ℝ<VAR>d : ℕ<VAR>n : ℤ<VAR>inv : Invertible ↑d<VAR>eq : e = ↑n * ⅟↑d<VAR>h : decide (1 < ↑n / ↑d) = true<VAR>this : 1 < ↑n / ↑d<GOAL>0 < Real.log (↑n / ↑d)
<VAR>α β : Type u<VAR>c : Cardinal.{?u.211873}<VAR>n : ℕ<GOAL>#α = ↑n ↔ ∃ t, ↑t = univ ∧ t.card = n
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>n : ℤ<GOAL>↑↑n = ↑n
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : NormedSpace ℝ V<VAR>inst✝² : StrictConvexSpace ℝ V<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₁ p₂ p₃ : P<VAR>h : Sbtw ℝ p₁ p₂ p₃<GOAL>dist p₂ p < max (dist p₁ p) (dist p₃ p)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : NormedSpace ℝ V<VAR>inst✝² : StrictConvexSpace ℝ V<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₁ p₂ p₃ : P<VAR>h : Sbtw ℝ p₁ p₂ p₃<VAR>hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p<GOAL>dist p₂ p < max (dist p₁ p) (dist p₃ p)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : NormedSpace ℝ V<VAR>inst✝² : StrictConvexSpace ℝ V<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₁ p₂ p₃ : P<VAR>h : (p₂ -ᵥ p = p₁ -ᵥ p ∨ p₂ -ᵥ p = p₃ -ᵥ p ∨ p₂ -ᵥ p ∈ openSegment ℝ (p₁ -ᵥ p) (p₃ -ᵥ p)) ∧ p₂ ≠ p₁ ∧ p₂ ≠ p₃<VAR>hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p<GOAL>dist p₂ p < max (dist p₁ p) (dist p₃ p)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<GOAL>Measurable fun a => (hf.stieltjesFunction a).measure
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<GOAL>∀ (s : Set ℝ), MeasurableSet s → Measurable fun b => (hf.stieltjesFunction b).measure s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>s : Set ℝ<VAR>hs : MeasurableSet s<GOAL>(fun s => Measurable fun b => (hf.stieltjesFunction b).measure s) ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>s : Set ℝ<VAR>hs : MeasurableSet s<GOAL>∀ t ∈ range Iic, (fun s => Measurable fun b => (hf.stieltjesFunction b).measure s) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>s : Set ℝ<VAR>hs : MeasurableSet s<GOAL>∀ (t : Set ℝ), MeasurableSet t → (fun s => Measurable fun b => (hf.stieltjesFunction b).measure s) t → (fun s => Measurable fun b => (hf.stieltjesFunction b).measure s) tᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>s : Set ℝ<VAR>hs : MeasurableSet s<GOAL>∀ (f_1 : ℕ → Set ℝ), Pairwise (Disjoint on f_1) → (∀ (i : ℕ), MeasurableSet (f_1 i)) → (∀ (i : ℕ), (fun s => Measurable fun b => (hf.stieltjesFunction b).measure s) (f_1 i)) → (fun s => Measurable fun b => (hf.stieltjesFunction b).measure s) (⋃ i, f_1 i)
<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₃ ≠ 0<GOAL>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₃ ≠ 0<GOAL>p₁ -ᵥ p₂ ≠ p₃ -ᵥ p₂
<VAR>R : Type u_1<VAR>x y : R<VAR>n m p : ℕ<VAR>inst✝ : Ring R<VAR>hp : n + m ≤ p + 1<VAR>h_comm : Commute x y<VAR>hx : x ^ n = 0<GOAL>y ^ m ∣ (x - y) ^ p
<VAR>R : Type u_1<VAR>x y : R<VAR>n m p : ℕ<VAR>inst✝ : Ring R<VAR>hp : n + m ≤ p + 1<VAR>h_comm : Commute x y<VAR>hx : x ^ n = 0<GOAL>y ^ m ∣ (y - x) ^ p * (-1) ^ p
<VAR>R : Type u_1<VAR>x y : R<VAR>n m p : ℕ<VAR>inst✝ : Ring R<VAR>hp : n + m ≤ p + 1<VAR>h_comm : Commute x y<VAR>hx : x ^ n = 0<GOAL>y ^ m ∣ (y - x) ^ p
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : TopologicalSpace B<VAR>b : B<VAR>v : F<GOAL>(Trivialization.coordChangeL 𝕜 (trivialization B F) (trivialization B F) b) v = (ContinuousLinearEquiv.refl 𝕜 F) v
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : TopologicalSpace B<VAR>b : B<VAR>v : F<GOAL>(↑(trivialization B F) (↑(trivialization B F).symm (b, v))).2 = (ContinuousLinearEquiv.refl 𝕜 F) v
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : TopologicalSpace B<VAR>b : B<VAR>v : F<GOAL>b ∈ (trivialization B F).baseSet ∩ (trivialization B F).baseSet
<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✝ : Monoid α<VAR>f g : Filter α<VAR>s : Set α<VAR>a : α<VAR>m n✝ n : ℕ<VAR>x✝ : n + 2 ≠ 0<GOAL>⊤ ^ (n + 2) = ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>f : M →ₗ⁅R,L⁆ M₂<GOAL>map N.incl (comap N.incl N') = N ⊓ N'
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>f : M →ₗ⁅R,L⁆ M₂<GOAL>↑(map N.incl (comap N.incl N')) = ↑(N ⊓ N')
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.70958, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>hf : S.f = 0<VAR>hg : S.g = 0<GOAL>IsZero S.X₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.70958, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>hf : S.f = 0<VAR>hg : S.g = 0<VAR>this : Mono S.g<GOAL>IsZero S.X₂
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ : Filter α<VAR>l₂ : Filter β<VAR>f : α → β<GOAL>Tendsto f l₁ l₂ ↔ PTendsto (PFun.res f Set.univ) l₁ l₂
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ : Filter α<VAR>l₂ : Filter β<VAR>f : α → β<GOAL>Tendsto f l₁ l₂ ↔ Tendsto f (l₁ ⊓ 𝓟 Set.univ) l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>f : (a : α) → a ∈ p.support → PMF β<GOAL>(p.bindOnSupport f).support = ⋃ a, ⋃ (h : a ∈ p.support), (f a h).support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>f : (a : α) → a ∈ p.support → PMF β<VAR>b : β<GOAL>b ∈ (p.bindOnSupport f).support ↔ b ∈ ⋃ a, ⋃ (h : a ∈ p.support), (f a h).support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>f : (a : α) → a ∈ p.support → PMF β<VAR>b : β<GOAL>(∃ x, ¬p x = 0 ∧ ¬(if h : p x = 0 then 0 else (f x h) b) = 0) ↔ ∃ i, ∃ (h : ¬p i = 0), ¬(f i ⋯) b = 0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction G α<VAR>a✝ : G<VAR>f : G →* H<VAR>s : Set G<VAR>a : H<GOAL>a ∈ Subgroup.map f (stabilizer G s) → a ∈ stabilizer H (⇑f '' s)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction G α<VAR>a✝ : G<VAR>f : G →* H<VAR>s : Set G<VAR>a : H<GOAL>∀ (x : G), x • s = s → f x = a → a • ⇑f '' s = ⇑f '' s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction G α<VAR>a✝ : G<VAR>f : G →* H<VAR>s : Set G<VAR>a : G<VAR>ha : a • s = s<GOAL>f a • ⇑f '' s = ⇑f '' s
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t s a b : Set X<VAR>h : IsClopen s<VAR>cover : s ⊆ a ∪ b<VAR>ha : IsOpen a<VAR>hb : IsOpen b<VAR>hab : Disjoint a b<GOAL>IsClopen (s ∩ a)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t s a b : Set X<VAR>h : IsClopen s<VAR>cover : s ⊆ a ∪ b<VAR>ha : IsOpen a<VAR>hb : IsOpen b<VAR>hab : Disjoint a b<GOAL>IsClosed (s ∩ a)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t s a b : Set X<VAR>h : IsClopen s<VAR>cover : s ⊆ a ∪ b<VAR>ha : IsOpen a<VAR>hb : IsOpen b<VAR>hab : Disjoint a b<VAR>this : IsClosed (s ∩ bᶜ)<GOAL>IsClosed (s ∩ a)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t s a b : Set X<VAR>h : IsClopen s<VAR>cover : s ⊆ a ∪ b<VAR>ha : IsOpen a<VAR>hb : IsOpen b<VAR>hab : Disjoint a b<VAR>this : IsClosed (s ∩ bᶜ)<GOAL>s ∩ a = s ∩ bᶜ
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t s a b : Set X<VAR>h : IsClopen s<VAR>cover : s ⊆ a ∪ b<VAR>ha : IsOpen a<VAR>hb : IsOpen b<VAR>hab : Disjoint a b<VAR>this : IsClosed (s ∩ bᶜ)<GOAL>s ∩ bᶜ ⊆ s ∩ a
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t s a b : Set X<VAR>h : IsClopen s<VAR>cover : s ⊆ a ∪ b<VAR>ha : IsOpen a<VAR>hb : IsOpen b<VAR>hab : Disjoint a b<VAR>this : IsClosed (s ∩ bᶜ)<VAR>x : X<VAR>hx₁ : x ∈ s<VAR>hx₂ : x ∈ bᶜ<GOAL>x ∈ s ∩ a
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>n : ℕ<VAR>S S₁ S₂ : ComposableArrows C n<VAR>e : S₁ ≅ S₂<VAR>h₁ : S₁.IsComplex<VAR>i : ℕ<VAR>hi : autoParam (i + 2 ≤ n) _auto✝<GOAL>S₂.map' i (i + 1) ⋯ ⋯ ≫ S₂.map' (i + 1) (i + 2) ⋯ hi = 0
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : PseudoEMetricSpace Ω<VAR>μ ν : Measure Ω<GOAL>levyProkhorovDist μ ν = levyProkhorovDist ν μ