ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>n : ℕ<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁴ : Fintype ι<VAR>inst✝¹³ : Fintype ι'<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁹ : (i : ι) → NormedAddCommGroup (E₁ i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁷ : (i : ι') → NormedAddCommGroup (E' i)<VAR>inst✝⁶ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁵ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>inst✝⁴ : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : ContinuousMultilinearMap 𝕜 (fun i => G) G'<VAR>x : Fin 0 → G<GOAL>‖f x‖ = ‖f‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>n : ℕ<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁴ : Fintype ι<VAR>inst✝¹³ : Fintype ι'<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁹ : (i : ι) → NormedAddCommGroup (E₁ i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁷ : (i : ι') → NormedAddCommGroup (E' i)<VAR>inst✝⁶ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁵ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>inst✝⁴ : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : ContinuousMultilinearMap 𝕜 (fun i => G) G'<GOAL>‖f 0‖ = ‖f‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>n : ℕ<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁴ : Fintype ι<VAR>inst✝¹³ : Fintype ι'<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁹ : (i : ι) → NormedAddCommGroup (E₁ i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁷ : (i : ι') → NormedAddCommGroup (E' i)<VAR>inst✝⁶ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁵ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>inst✝⁴ : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : ContinuousMultilinearMap 𝕜 (fun i => G) G'<GOAL>‖f‖ ≤ ‖f 0‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>n : ℕ<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁴ : Fintype ι<VAR>inst✝¹³ : Fintype ι'<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁹ : (i : ι) → NormedAddCommGroup (E₁ i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁷ : (i : ι') → NormedAddCommGroup (E' i)<VAR>inst✝⁶ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁵ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>inst✝⁴ : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : ContinuousMultilinearMap 𝕜 (fun i => G) G'<VAR>this : ‖curry0 𝕜 G f.uncurry0‖ ≤ ‖f.uncurry0‖<GOAL>‖f‖ ≤ ‖f 0‖
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a : A<VAR>s : R<VAR>r : Rˣ<GOAL>r • s ∈ σ (r • a) ↔ s ∈ σ a
<VAR>T : ℝ<VAR>x : AddCircle T<GOAL>(fourier 0) x = 1
<VAR>T z✝ : ℝ<GOAL>(fourier 0) ↑z✝ = 1
<VAR>T z✝ : ℝ<GOAL>Complex.exp (2 * ↑π * Complex.I * ↑0 * ↑z✝ / ↑T) = 1
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>n : Type u_2<VAR>inst✝¹ : Fintype n<VAR>A : Matrix n n 𝕜<VAR>inst✝ : DecidableEq n<VAR>hA : A.IsHermitian<GOAL>A.det = ∏ i : n, ↑(hA.eigenvalues i)
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>n : Type u_2<VAR>inst✝¹ : Fintype n<VAR>A : Matrix n n 𝕜<VAR>inst✝ : DecidableEq n<VAR>hA : A.IsHermitian<GOAL>∏ i : n, ↑(hA.eigenvalues i) = (↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ hA.eigenvalues) * star ↑hA.eigenvectorUnitary).det
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>n : Type u_2<VAR>inst✝¹ : Fintype n<VAR>A : Matrix n n 𝕜<VAR>inst✝ : DecidableEq n<VAR>hA : A.IsHermitian<GOAL>∏ i : n, ↑(hA.eigenvalues i) = (↑hA.eigenvectorUnitary * star ↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ hA.eigenvalues)).det
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace 𝕜 G'<VAR>ε : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f (↑f') a<GOAL>∃ s, a ∈ s ∧ IsOpen s ∧ ApproximatesLinearOn f (↑f') s (‖↑f'.symm‖₊⁻¹ / 2)
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace 𝕜 G'<VAR>ε : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f (↑f') a<GOAL>∃ s, (a ∈ s ∧ IsOpen s) ∧ ApproximatesLinearOn f (↑f') s (‖↑f'.symm‖₊⁻¹ / 2)
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace 𝕜 G'<VAR>ε : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f (↑f') a<GOAL>∃ s ∈ 𝓝 a, ApproximatesLinearOn f (↑f') s (‖↑f'.symm‖₊⁻¹ / 2)
<VAR>M : Type u_1<VAR>inst✝¹ : OrderedCancelAddCommMonoid M<VAR>inst✝ : ExistsAddOfLE M<VAR>a b c d : M<GOAL>(fun x => a + x) '' Ioi b = Ioi (a + b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : EMetricSpace β<VAR>a : β<VAR>r : ℝ≥0∞<VAR>x y : ↑(EMetric.ball a r)<GOAL>edist a ↑x + edist a ↑y < r + r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : EMetricSpace β<VAR>a : β<VAR>r : ℝ≥0∞<VAR>x y : ↑(EMetric.ball a r)<GOAL>edist (↑x) a + edist (↑y) a < r + r
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>g : G<VAR>j : ℤ<VAR>a : α<VAR>a_in_fixedBy : a ∈ fixedBy α g<GOAL>a ∈ fixedBy α (g ^ j)
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>g : G<VAR>j : ℤ<VAR>a : α<VAR>a_in_fixedBy : a ∈ fixedBy α g<GOAL>1 ∣ j
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<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>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>n m : ℕ<VAR>hf : CPolynomialAt 𝕜 f x<VAR>hg : CPolynomialAt 𝕜 g x<GOAL>CPolynomialAt 𝕜 (f - g) x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>π : ι → Type u_3<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : (i : ι) → PseudoMetricSpace (π i)<VAR>x y x' y' : ι → ℝ<VAR>hx : x ∈ Icc x' y'<VAR>hy : y ∈ Icc x' y'<GOAL>dist x y ≤ dist x' y'
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>π : ι → Type u_3<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : (i : ι) → PseudoMetricSpace (π i)<VAR>x y x' y' : ι → ℝ<VAR>hx : x ∈ Icc x' y'<VAR>hy : y ∈ Icc x' y'<VAR>b : ι<GOAL>x b ∈ Icc (x' b) (y' b)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>π : ι → Type u_3<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : (i : ι) → PseudoMetricSpace (π i)<VAR>x y x' y' : ι → ℝ<VAR>hx : x ∈ Icc x' y'<VAR>hy : y ∈ Icc x' y'<VAR>b : ι<GOAL>y b ∈ Icc (x' b) (y' b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α<VAR>a b : α<VAR>s t : Finset α<GOAL>(s ∪ t) ∩ t = t
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A✝ : Type u_3<VAR>inst✝³ : Semiring A✝<VAR>inst✝² : Algebra R A✝<VAR>A : Type u_4<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>f : M →ₗ[R] A<VAR>hf : ∀ (x : M), f x * f x = (algebraMap R A) (Q x)<VAR>a b : M<GOAL>f a * f b + f b * f a = f (a + b) * f (a + b) - f a * f a - f b * f b
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A✝ : Type u_3<VAR>inst✝³ : Semiring A✝<VAR>inst✝² : Algebra R A✝<VAR>A : Type u_4<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>f : M →ₗ[R] A<VAR>hf : ∀ (x : M), f x * f x = (algebraMap R A) (Q x)<VAR>a b : M<GOAL>f a * f b + f b * f a = f a * f a + f b * f a + (f a * f b + f b * f b) - f a * f a - f b * f b
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A✝ : Type u_3<VAR>inst✝³ : Semiring A✝<VAR>inst✝² : Algebra R A✝<VAR>A : Type u_4<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>f : M →ₗ[R] A<VAR>hf : ∀ (x : M), f x * f x = (algebraMap R A) (Q x)<VAR>a b : M<GOAL>(algebraMap R A) (Q (a + b)) - (algebraMap R A) (Q a) - (algebraMap R A) (Q b) = (algebraMap R A) (Q (a + b) - Q a - Q b)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : MulAction G α<VAR>s : Set α<VAR>hs : s.Finite<VAR>g : G<GOAL>g ∈ stabilizer G s ↔ s ⊆ g • s
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : MulAction G α<VAR>s : Set α<VAR>hs : s.Finite<VAR>g : G<GOAL>g⁻¹ • s ⊆ s ↔ s ⊆ g • s
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s✝ t : Set M<VAR>f : F<VAR>s : Set M₂<GOAL>span R (⇑f ⁻¹' s) ≤ comap f (span R₂ s)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s✝ t : Set M<VAR>f : F<VAR>s : Set M₂<GOAL>⇑f ⁻¹' s ⊆ ⇑f ⁻¹' ↑(span R₂ s)
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f g : Perm α<VAR>n : ℕ<VAR>x : α<GOAL>(f ^ n) x ∈ f.support ↔ x ∈ f.support
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁸ : SeminormedAddCommGroup V<VAR>inst✝⁷ : PseudoMetricSpace P<VAR>inst✝⁶ : NormedAddTorsor V P<VAR>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : MetricSpace Q<VAR>inst✝³ : NormedAddTorsor W Q<VAR>𝕜 : Type u_6<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 V<VAR>inst✝ : NormedSpace 𝕜 W<VAR>x : Q<VAR>s t : Set Q<VAR>ht : t.Finite<VAR>h : t ⊆ interior s<GOAL>∀ᶠ (δ : 𝕜) in 𝓝 1, ⇑(homothety x δ) '' t ⊆ s
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁸ : SeminormedAddCommGroup V<VAR>inst✝⁷ : PseudoMetricSpace P<VAR>inst✝⁶ : NormedAddTorsor V P<VAR>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : MetricSpace Q<VAR>inst✝³ : NormedAddTorsor W Q<VAR>𝕜 : Type u_6<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 V<VAR>inst✝ : NormedSpace 𝕜 W<VAR>x : Q<VAR>s t : Set Q<VAR>ht : t.Finite<VAR>h : t ⊆ interior s<GOAL>∀ y ∈ t, ∀ᶠ (δ : 𝕜) in 𝓝 1, (homothety x δ) y ∈ s
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁸ : SeminormedAddCommGroup V<VAR>inst✝⁷ : PseudoMetricSpace P<VAR>inst✝⁶ : NormedAddTorsor V P<VAR>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : MetricSpace Q<VAR>inst✝³ : NormedAddTorsor W Q<VAR>𝕜 : Type u_6<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 V<VAR>inst✝ : NormedSpace 𝕜 W<VAR>x : Q<VAR>s t : Set Q<VAR>ht : t.Finite<VAR>h : t ⊆ interior s<VAR>y : Q<VAR>hy : y ∈ t<GOAL>∀ᶠ (δ : 𝕜) in 𝓝 1, (homothety x δ) y ∈ s
<VAR>X : Type u_1<VAR>x : OnePoint X<GOAL>x ∉ range some ↔ x = ∞
<VAR>z : ℂ<GOAL>↑z.re = (z + (starRingEnd ℂ) z) / 2
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ<VAR>hμ : μ s ≠ 0<VAR>hμ₁ : μ s ≠ ⊤<VAR>hf : IntegrableOn f s μ<GOAL>0 < μ {x | x ∈ s ∧ f x ≤ ⨍ (a : α) in s, f a ∂μ}
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ<VAR>hμ : μ s ≠ 0<VAR>hμ₁ : μ s ≠ ⊤<VAR>hf : IntegrableOn f s μ<VAR>H : μ {x | x ∈ s ∧ f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0<GOAL>False
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ<VAR>hμ : μ s ≠ 0<VAR>hμ₁ : μ s ≠ ⊤<VAR>hf : IntegrableOn f s μ<VAR>H : (μ.restrict s) {x | f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0<GOAL>False
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ<VAR>hμ : μ s ≠ 0<VAR>hμ₁ : μ s ≠ ⊤<VAR>hf : IntegrableOn f s μ<VAR>H : (μ.restrict s) {x | f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0<VAR>this : Fact (μ s < ⊤)<GOAL>False
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ<VAR>hμ : μ s ≠ 0<VAR>hμ₁ : μ s ≠ ⊤<VAR>hf : IntegrableOn f s μ<VAR>H : (μ.restrict s) {x | f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0<VAR>this : Fact (μ s < ⊤)<GOAL>0 < ∫ (x : α) in s, f x - ⨍ (a : α) in s, f a ∂μ ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ<VAR>hμ : μ s ≠ 0<VAR>hμ₁ : μ s ≠ ⊤<VAR>hf : IntegrableOn f s μ<VAR>H : (μ.restrict s) {x | f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0<VAR>this : Fact (μ s < ⊤)<GOAL>0 ≤ᶠ[ae (μ.restrict s)] fun x => f x - ⨍ (a : α) in s, f a ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ<VAR>hμ : μ s ≠ 0<VAR>hμ₁ : μ s ≠ ⊤<VAR>hf : IntegrableOn f s μ<VAR>H : (μ.restrict s) {x | f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0<VAR>this : Fact (μ s < ⊤)<GOAL>IntegrableOn (fun x => f x - ⨍ (a : α) in s, f a ∂μ) s μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ<VAR>hμ : μ s ≠ 0<VAR>hμ₁ : μ s ≠ ⊤<VAR>hf : IntegrableOn f s μ<VAR>H : (μ.restrict s) {x | f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0<VAR>this : Fact (μ s < ⊤)<GOAL>0 < μ ((support fun x => f x - ⨍ (a : α) in s, f a ∂μ) ∩ s)
<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₁ p₂ : P<GOAL>p₂ -ᵥ midpoint R p₁ p₂ = ⅟2 • (p₂ -ᵥ p₁)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>ι : Type ui<VAR>inst✝¹ : CommSemiring k<VAR>inst✝ : CommMonoid G<VAR>s✝ : Finset ι<VAR>a✝ : ι → G<VAR>b : ι → k<VAR>a : ι<VAR>s : Finset ι<VAR>has : a ∉ s<VAR>ih : ∏ i ∈ s, single (a✝ i) (b i) = single (∏ i ∈ s, a✝ i) (∏ i ∈ s, b i)<GOAL>∏ i ∈ Finset.cons a s has, single (a✝ i) (b i) = single (∏ i ∈ Finset.cons a s has, a✝ i) (∏ i ∈ Finset.cons a s has, b i)
<VAR>n m : ℕ<VAR>h : m ≤ n<GOAL>n.dist m = n - m
<VAR>n m : ℕ<VAR>h : m ≤ n<GOAL>m.dist n = n - m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : α → β<VAR>g : β → γ<VAR>f : α → α<VAR>n : ℕ<VAR>ih : preimage f^[n] = (preimage f)^[n]<GOAL>preimage f^[n + 1] = (preimage f)^[n + 1]
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace ℝ E<VAR>inst✝² : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>hF : Fact (finrank ℝ F = 2)<VAR>φ : E ≃ₗᵢ[ℝ] F<VAR>x : F<GOAL>((map (Fin 2) φ.toLinearEquiv) o).rightAngleRotation x = φ (o.rightAngleRotation (φ.symm x))
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace ℝ E<VAR>inst✝² : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>hF : Fact (finrank ℝ F = 2)<VAR>φ : E ≃ₗᵢ[ℝ] F<VAR>x : F<GOAL>∀ (v : F), ⟪((map (Fin 2) φ.toLinearEquiv) o).rightAngleRotation x, v⟫_ℝ = ⟪φ (o.rightAngleRotation (φ.symm x)), v⟫_ℝ
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace ℝ E<VAR>inst✝² : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>hF : Fact (finrank ℝ F = 2)<VAR>φ : E ≃ₗᵢ[ℝ] F<VAR>x y : F<GOAL>⟪((map (Fin 2) φ.toLinearEquiv) o).rightAngleRotation x, y⟫_ℝ = ⟪φ (o.rightAngleRotation (φ.symm x)), y⟫_ℝ
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace ℝ E<VAR>inst✝² : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>hF : Fact (finrank ℝ F = 2)<VAR>φ : E ≃ₗᵢ[ℝ] F<VAR>x y : F<GOAL>(((map (Fin 2) φ.toLinearEquiv) o).areaForm x) y = ⟪φ (o.rightAngleRotation (φ.symm 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>s : Set P<VAR>t : Triangle ℝ P<VAR>hto : t.orthocenter ∉ Set.range t.points<VAR>hts : s = insert t.orthocenter (Set.range t.points)<GOAL>∃ r, ∀ (t : Triangle ℝ P), Set.range t.points ⊆ s → Simplex.circumradius t = r
<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>s : Set P<VAR>t : Triangle ℝ P<VAR>hto : t.orthocenter ∉ Set.range t.points<VAR>hts : s = insert t.orthocenter (Set.range t.points)<GOAL>∀ (t_1 : Triangle ℝ P), Set.range t_1.points ⊆ s → Simplex.circumradius t_1 = Simplex.circumradius t
<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>s : Set P<VAR>t : Triangle ℝ P<VAR>hto : t.orthocenter ∉ Set.range t.points<VAR>hts : s = insert t.orthocenter (Set.range t.points)<VAR>t₂ : Triangle ℝ P<VAR>ht₂ : Set.range t₂.points ⊆ insert t.orthocenter (Set.range t.points)<VAR>ht₂s : Set.range t₂.points ⊆ s<GOAL>Simplex.circumradius t₂ = Simplex.circumradius t
<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>s : Set P<VAR>t : Triangle ℝ P<VAR>hto : t.orthocenter ∉ Set.range t.points<VAR>hts : s = insert t.orthocenter (Set.range t.points)<VAR>t₂ : Triangle ℝ P<VAR>ht₂ : Set.range t₂.points ⊆ insert t.orthocenter (Set.range t.points)<VAR>ht₂s : Set.range t₂.points ⊆ s<VAR>c : P<VAR>hc : c ∈ affineSpan ℝ (Set.range t.points)<VAR>h : ∀ p₁ ∈ Set.range t₂.points, dist p₁ c = Simplex.circumradius t<GOAL>Simplex.circumradius t₂ = Simplex.circumradius t
<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>s : Set P<VAR>t : Triangle ℝ P<VAR>hto : t.orthocenter ∉ Set.range t.points<VAR>hts : s = insert t.orthocenter (Set.range t.points)<VAR>t₂ : Triangle ℝ P<VAR>ht₂ : Set.range t₂.points ⊆ insert t.orthocenter (Set.range t.points)<VAR>ht₂s : Set.range t₂.points ⊆ s<VAR>c : P<VAR>hc : c ∈ affineSpan ℝ (Set.range t.points)<VAR>h : ∀ (i : Fin 3), dist (t₂.points i) c = Simplex.circumradius t<GOAL>Simplex.circumradius t₂ = Simplex.circumradius t
<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>s : Set P<VAR>t : Triangle ℝ P<VAR>hto : t.orthocenter ∉ Set.range t.points<VAR>hts : s = insert t.orthocenter (Set.range t.points)<VAR>t₂ : Triangle ℝ P<VAR>ht₂ : Set.range t₂.points ⊆ insert t.orthocenter (Set.range t.points)<VAR>ht₂s : Set.range t₂.points ⊆ s<VAR>c : P<VAR>hc : c ∈ affineSpan ℝ (Set.range t.points)<VAR>h : ∀ (i : Fin 3), dist (t₂.points i) c = Simplex.circumradius t<VAR>hs : Set.range t.points ⊆ s<GOAL>Simplex.circumradius t₂ = Simplex.circumradius t
<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>s : Set P<VAR>t : Triangle ℝ P<VAR>hto : t.orthocenter ∉ Set.range t.points<VAR>hts : s = insert t.orthocenter (Set.range t.points)<VAR>t₂ : Triangle ℝ P<VAR>ht₂ : Set.range t₂.points ⊆ insert t.orthocenter (Set.range t.points)<VAR>ht₂s : Set.range t₂.points ⊆ s<VAR>c : P<VAR>hc : c ∈ affineSpan ℝ (Set.range t₂.points)<VAR>h : ∀ (i : Fin 3), dist (t₂.points i) c = Simplex.circumradius t<VAR>hs : Set.range t.points ⊆ s<GOAL>Simplex.circumradius t₂ = Simplex.circumradius t
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>inst✝¹ : Finite G<VAR>N : Subgroup G<VAR>inst✝ : N.Normal<VAR>h1 : (Nat.card ↥N).Coprime N.index<VAR>h2 : ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'], Nat.card G' < Nat.card G → ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'<VAR>h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H<VAR>P : Sylow (Nat.card ↥N).minFac ↥N<GOAL>↑P ≠ ⊥