ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : Field R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : CompleteSpace R<VAR>inst✝⁶ : TopologicalRing R<VAR>inst✝⁵ : ContinuousStar R<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : TopologicalSpace A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>h_cpct : ∀ (a : A), CompactSpace ↑(spectrum R a)<VAR>a : A<VAR>ha : p a<VAR>f : C(↑(spectrum R a), ↑(σₙ R a)) := { toFun := inclusion ⋯, continuous_toFun := ⋯ }<VAR>h_cpct' : CompactSpace ↑(σₙ R a)<VAR>this : inferInstanceAs (UniformSpace C(↑(σₙ R a), R)) = UniformSpace.comap (fun x => x.comp f) inferInstance ⊓ UniformSpace.comap (fun x => x.comp 0) inferInstance<GOAL>Filter.comap (fun x => (↑((↑(compStarAlgHom' R R { toFun := inclusion ⋯, continuous_toFun := ⋯ })).comp toContinuousMapHom).toNonUnitalAlgHom x.1, ↑((↑(compStarAlgHom' R R { toFun := inclusion ⋯, continuous_toFun := ⋯ })).comp toContinuousMapHom).toNonUnitalAlgHom x.2)) (𝓤 C(↑(spectrum R a), R)) = Filter.comap ((Prod.map (fun x => x.comp f) fun x => x.comp f) ∘ Prod.map ContinuousMapZero.toContinuousMap ContinuousMapZero.toContinuousMap) (𝓤 C(↑(spectrum R a), R)) ⊓ Filter.comap ((Prod.map (fun x => x.comp 0) fun x => x.comp 0) ∘ Prod.map ContinuousMapZero.toContinuousMap ContinuousMapZero.toContinuousMap) (𝓤 C(Unit, R))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : Field R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : CompleteSpace R<VAR>inst✝⁶ : TopologicalRing R<VAR>inst✝⁵ : ContinuousStar R<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : TopologicalSpace A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>h_cpct : ∀ (a : A), CompactSpace ↑(spectrum R a)<VAR>a : A<VAR>ha : p a<VAR>f : C(↑(spectrum R a), ↑(σₙ R a)) := { toFun := inclusion ⋯, continuous_toFun := ⋯ }<VAR>h_cpct' : CompactSpace ↑(σₙ R a)<VAR>this : inferInstanceAs (UniformSpace C(↑(σₙ R a), R)) = UniformSpace.comap (fun x => x.comp f) inferInstance ⊓ UniformSpace.comap (fun x => x.comp 0) inferInstance<GOAL>Filter.comap ((Prod.map (fun x => x.comp 0) fun x => x.comp 0) ∘ Prod.map ContinuousMapZero.toContinuousMap ContinuousMapZero.toContinuousMap) (𝓤 C(Unit, R)) = ⊤
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : Field R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : CompleteSpace R<VAR>inst✝⁶ : TopologicalRing R<VAR>inst✝⁵ : ContinuousStar R<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : TopologicalSpace A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>h_cpct : ∀ (a : A), CompactSpace ↑(spectrum R a)<VAR>a : A<VAR>ha : p a<VAR>f : C(↑(spectrum R a), ↑(σₙ R a)) := { toFun := inclusion ⋯, continuous_toFun := ⋯ }<VAR>h_cpct' : CompactSpace ↑(σₙ R a)<VAR>this✝ : inferInstanceAs (UniformSpace C(↑(σₙ R a), R)) = UniformSpace.comap (fun x => x.comp f) inferInstance ⊓ UniformSpace.comap (fun x => x.comp 0) inferInstance<VAR>this : ∀ U ∈ 𝓤 C(Unit, R), (0, 0) ∈ U<GOAL>Filter.comap ((Prod.map (fun x => x.comp 0) fun x => x.comp 0) ∘ Prod.map ContinuousMapZero.toContinuousMap ContinuousMapZero.toContinuousMap) (𝓤 C(Unit, R)) = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : IsScott α<GOAL>scottHausdorff α ≤ inst✝¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : IsScott α<GOAL>scottHausdorff α ≤ upperSet α ⊔ scottHausdorff α
<VAR>α : Type u_1<VAR>l : List α<VAR>x : α<GOAL>l.Nodup ↔ ∀ (x : α), ¬x ∈+ l
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>J : Type<VAR>inst✝¹ : Fintype J<VAR>f : J → C<VAR>inst✝ : HasBiproduct f<VAR>T U : C<VAR>g : (j : J) → T ⟶ f j<VAR>h : (j : J) → f j ⟶ U<GOAL>lift g ≫ desc h = ∑ j : J, g j ≫ h j
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : SMul 𝕜 E<VAR>S✝ S : ConvexCone 𝕜 E<GOAL>S.Blunt ↔ ¬S.Pointed
<VAR>x y : ℂ<VAR>h : ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), y * I ≠ (2 * ↑l + 1) * ↑π / 2) ∨ (∃ k, x = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, y * I = (2 * ↑l + 1) * ↑π / 2<GOAL>tan (x + y * I) = (tan x + tanh y * I) / (1 - tan x * tanh y * I)
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝² : DivInvMonoid G<VAR>inst✝¹ : MeasurableSpace G<VAR>inst✝ : MeasurableMul G<VAR>g : G<GOAL>Measurable fun h => h / g
<VAR>E✝ : Type u_1<VAR>inst✝¹² : NormedAddCommGroup E✝<VAR>inst✝¹¹ : NormedSpace ℝ E✝<VAR>inst✝¹⁰ : MeasurableSpace E✝<VAR>inst✝⁹ : BorelSpace E✝<VAR>inst✝⁸ : FiniteDimensional ℝ E✝<VAR>μ✝ : Measure E✝<VAR>inst✝⁷ : μ✝.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>s : Set E✝<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>x : E<VAR>r : ℝ<VAR>this : ball 0 r = (fun x_1 => x + x_1) ⁻¹' ball x r<GOAL>μ (ball x r) = μ (ball 0 r)
<VAR>σ : Type u_1<VAR>inst✝² : Fintype σ<VAR>inst✝¹ : DecidableEq σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>a : ℕ × ℕ<VAR>ha : a ∈ antidiagonal k<GOAL>∑ A ∈ powersetCard a.1 univ, ∑ j : σ, MvPolynomial.NewtonIdentities.weight σ R k (A, j) = (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
<VAR>σ : Type u_1<VAR>inst✝² : Fintype σ<VAR>inst✝¹ : DecidableEq σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>a : ℕ × ℕ<VAR>ha : a ∈ antidiagonal k<GOAL>∑ x ∈ powersetCard a.1 univ, ∑ x_1 : σ, ((-1) ^ x.card * ∏ a ∈ x, X a) * X x_1 ^ (k - x.card) = ∑ i : σ, (∑ i ∈ powersetCard a.1 univ, (-1) ^ a.1 * ∏ a ∈ i, X a) * X i ^ a.2
<VAR>σ : Type u_1<VAR>inst✝² : Fintype σ<VAR>inst✝¹ : DecidableEq σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>a : ℕ × ℕ<VAR>ha : a ∈ antidiagonal k<GOAL>∑ y : σ, ∑ x ∈ powersetCard a.1 univ, ((-1) ^ x.card * ∏ a ∈ x, X a) * X y ^ (k - x.card) = ∑ i : σ, (∑ i ∈ powersetCard a.1 univ, (-1) ^ a.1 * ∏ a ∈ i, X a) * X i ^ a.2
<VAR>σ : Type u_1<VAR>inst✝² : Fintype σ<VAR>inst✝¹ : DecidableEq σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>a : ℕ × ℕ<VAR>ha : a ∈ antidiagonal k<VAR>x : σ<VAR>x✝ : x ∈ univ<GOAL>∑ x_1 ∈ powersetCard a.1 univ, ((-1) ^ x_1.card * ∏ a ∈ x_1, X a) * X x ^ (k - x_1.card) = (∑ i ∈ powersetCard a.1 univ, (-1) ^ a.1 * ∏ a ∈ i, X a) * X x ^ a.2
<VAR>σ : Type u_1<VAR>inst✝² : Fintype σ<VAR>inst✝¹ : DecidableEq σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>a : ℕ × ℕ<VAR>ha : a ∈ antidiagonal k<VAR>x : σ<VAR>x✝ : x ∈ univ<GOAL>∑ x_1 ∈ powersetCard a.1 univ, ((-1) ^ x_1.card * ∏ a ∈ x_1, X a) * X x ^ (k - x_1.card) = ∑ i ∈ powersetCard a.1 univ, ((-1) ^ a.1 * ∏ a ∈ i, X a) * X x ^ a.2
<VAR>σ : Type u_1<VAR>inst✝² : Fintype σ<VAR>inst✝¹ : DecidableEq σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>a : ℕ × ℕ<VAR>ha : a ∈ antidiagonal k<VAR>x : σ<VAR>x✝ : x ∈ univ<VAR>s : Finset σ<VAR>hs : s ∈ powersetCard a.1 univ<GOAL>((-1) ^ s.card * ∏ a ∈ s, X a) * X x ^ (k - s.card) = ((-1) ^ a.1 * ∏ a ∈ s, X a) * X x ^ a.2
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<GOAL>∃ f, ∀ (a b : { x // x ∈ s }), P.part ↑a = P.part ↑b ↔ ↑(f a) % P.parts.card = ↑(f b) % P.parts.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<VAR>f : { x // x ∈ s } ≃ (t : { x // x ∈ P.parts }) × Fin (↑t).card<VAR>hf : ∀ (a b : { x // x ∈ s }), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst<GOAL>∃ f, ∀ (a b : { x // x ∈ s }), P.part ↑a = P.part ↑b ↔ ↑(f a) % P.parts.card = ↑(f b) % P.parts.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<VAR>f : { x // x ∈ s } ≃ (t : { x // x ∈ P.parts }) × Fin (↑t).card<VAR>hf : ∀ (a b : { x // x ∈ s }), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst<VAR>g : { x // x ∈ P.parts } ≃ Fin P.parts.card<VAR>hg : ∀ (t : { x // x ∈ P.parts }), (↑t).card = s.card / P.parts.card + 1 ↔ ↑(g t) < s.card % P.parts.card<GOAL>∃ f, ∀ (a b : { x // x ∈ s }), P.part ↑a = P.part ↑b ↔ ↑(f a) % P.parts.card = ↑(f b) % P.parts.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<VAR>f : { x // x ∈ s } ≃ (t : { x // x ∈ P.parts }) × Fin (↑t).card<VAR>hf : ∀ (a b : { x // x ∈ s }), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst<VAR>g : { x // x ∈ P.parts } ≃ Fin P.parts.card<VAR>hg : ∀ (t : { x // x ∈ P.parts }), (↑t).card = s.card / P.parts.card + 1 ↔ ↑(g t) < s.card % P.parts.card<VAR>z : { x // x ∈ s } → ℕ := fun a => P.parts.card * ↑(f a).snd + ↑(g (f a).fst)<GOAL>∃ f, ∀ (a b : { x // x ∈ s }), P.part ↑a = P.part ↑b ↔ ↑(f a) % P.parts.card = ↑(f b) % P.parts.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<VAR>f : { x // x ∈ s } ≃ (t : { x // x ∈ P.parts }) × Fin (↑t).card<VAR>hf : ∀ (a b : { x // x ∈ s }), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst<VAR>g : { x // x ∈ P.parts } ≃ Fin P.parts.card<VAR>hg : ∀ (t : { x // x ∈ P.parts }), (↑t).card = s.card / P.parts.card + 1 ↔ ↑(g t) < s.card % P.parts.card<VAR>z : { x // x ∈ s } → ℕ := fun a => P.parts.card * ↑(f a).snd + ↑(g (f a).fst)<VAR>gl : ∀ (a : { x // x ∈ s }), ↑(g (f a).fst) < P.parts.card<GOAL>∃ f, ∀ (a b : { x // x ∈ s }), P.part ↑a = P.part ↑b ↔ ↑(f a) % P.parts.card = ↑(f b) % P.parts.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<VAR>f : { x // x ∈ s } ≃ (t : { x // x ∈ P.parts }) × Fin (↑t).card<VAR>hf : ∀ (a b : { x // x ∈ s }), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst<VAR>g : { x // x ∈ P.parts } ≃ Fin P.parts.card<VAR>hg : ∀ (t : { x // x ∈ P.parts }), (↑t).card = s.card / P.parts.card + 1 ↔ ↑(g t) < s.card % P.parts.card<VAR>z : { x // x ∈ s } → ℕ := fun a => P.parts.card * ↑(f a).snd + ↑(g (f a).fst)<VAR>gl : ∀ (a : { x // x ∈ s }), ↑(g (f a).fst) < P.parts.card<VAR>less : ∀ (a : { x // x ∈ s }), z a < s.card<VAR>z' : { x // x ∈ s } → Fin s.card := fun a => ⟨z a, ⋯⟩<GOAL>∃ f, ∀ (a b : { x // x ∈ s }), P.part ↑a = P.part ↑b ↔ ↑(f a) % P.parts.card = ↑(f b) % P.parts.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<VAR>f : { x // x ∈ s } ≃ (t : { x // x ∈ P.parts }) × Fin (↑t).card<VAR>hf : ∀ (a b : { x // x ∈ s }), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst<VAR>g : { x // x ∈ P.parts } ≃ Fin P.parts.card<VAR>hg : ∀ (t : { x // x ∈ P.parts }), (↑t).card = s.card / P.parts.card + 1 ↔ ↑(g t) < s.card % P.parts.card<VAR>z : { x // x ∈ s } → ℕ := fun a => P.parts.card * ↑(f a).snd + ↑(g (f a).fst)<VAR>gl : ∀ (a : { x // x ∈ s }), ↑(g (f a).fst) < P.parts.card<VAR>less : ∀ (a : { x // x ∈ s }), z a < s.card<VAR>z' : { x // x ∈ s } → Fin s.card := fun a => ⟨z a, ⋯⟩<VAR>bij : Function.Bijective z'<GOAL>∃ f, ∀ (a b : { x // x ∈ s }), P.part ↑a = P.part ↑b ↔ ↑(f a) % P.parts.card = ↑(f b) % P.parts.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<VAR>f : { x // x ∈ s } ≃ (t : { x // x ∈ P.parts }) × Fin (↑t).card<VAR>hf : ∀ (a b : { x // x ∈ s }), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst<VAR>g : { x // x ∈ P.parts } ≃ Fin P.parts.card<VAR>hg : ∀ (t : { x // x ∈ P.parts }), (↑t).card = s.card / P.parts.card + 1 ↔ ↑(g t) < s.card % P.parts.card<VAR>z : { x // x ∈ s } → ℕ := fun a => P.parts.card * ↑(f a).snd + ↑(g (f a).fst)<VAR>gl : ∀ (a : { x // x ∈ s }), ↑(g (f a).fst) < P.parts.card<VAR>less : ∀ (a : { x // x ∈ s }), z a < s.card<VAR>z' : { x // x ∈ s } → Fin s.card := fun a => ⟨z a, ⋯⟩<VAR>bij : Function.Bijective z'<GOAL>∀ (a b : { x // x ∈ s }), P.part ↑a = P.part ↑b ↔ ↑((Equiv.ofBijective z' bij) a) % P.parts.card = ↑((Equiv.ofBijective z' bij) b) % P.parts.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<VAR>f : { x // x ∈ s } ≃ (t : { x // x ∈ P.parts }) × Fin (↑t).card<VAR>hf : ∀ (a b : { x // x ∈ s }), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst<VAR>g : { x // x ∈ P.parts } ≃ Fin P.parts.card<VAR>hg : ∀ (t : { x // x ∈ P.parts }), (↑t).card = s.card / P.parts.card + 1 ↔ ↑(g t) < s.card % P.parts.card<VAR>z : { x // x ∈ s } → ℕ := fun a => P.parts.card * ↑(f a).snd + ↑(g (f a).fst)<VAR>gl : ∀ (a : { x // x ∈ s }), ↑(g (f a).fst) < P.parts.card<VAR>less : ∀ (a : { x // x ∈ s }), z a < s.card<VAR>z' : { x // x ∈ s } → Fin s.card := fun a => ⟨z a, ⋯⟩<VAR>bij : Function.Bijective z'<VAR>a b : { x // x ∈ s }<GOAL>P.part ↑a = P.part ↑b ↔ ↑((Equiv.ofBijective z' bij) a) % P.parts.card = ↑((Equiv.ofBijective z' bij) b) % P.parts.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology β<GOAL>{x | ¬ContinuousAt f x}.Countable
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology β<GOAL>{x | ¬ContinuousAt f x} ⊆ {x | ¬ContinuousWithinAt f (Ioi x) x} ∪ {x | ¬ContinuousWithinAt f (Iio x) x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology β<GOAL>({x | ¬ContinuousWithinAt f (Ioi x) x} ∪ {x | ¬ContinuousWithinAt f (Iio x) x})ᶜ ⊆ {x | ¬ContinuousAt f x}ᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology β<GOAL>{x | ¬ContinuousWithinAt f (Ioi x) x}ᶜ ∩ {x | ¬ContinuousWithinAt f (Iio x) x}ᶜ ⊆ {x | ¬ContinuousAt f x}ᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x✝ y : α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology β<VAR>x : α<VAR>hx : x ∈ {x | ¬ContinuousWithinAt f (Ioi x) x}ᶜ<VAR>h'x : x ∈ {x | ¬ContinuousWithinAt f (Iio x) x}ᶜ<GOAL>x ∈ {x | ¬ContinuousAt f x}ᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x✝ y : α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology β<VAR>x : α<VAR>hx : ContinuousWithinAt f (Ioi x) x<VAR>h'x : ContinuousWithinAt f (Iio x) x<GOAL>ContinuousAt f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν✝ : Measure α<VAR>mb : MeasurableSpace β<VAR>ν : Measure β<VAR>g : α → β<VAR>hg : MeasurePreserving g μ ν<VAR>hge : MeasurableEmbedding g<VAR>f : β → ℝ≥0∞<VAR>s : Set α<GOAL>∫⁻ (a : α) in s, f (g a) ∂μ = ∫⁻ (b : β) in g '' s, f b ∂ν
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β → β<VAR>op : α → α → α<VAR>inst✝² : Monoid α<VAR>inst✝¹ : Monoid β<VAR>inst✝ : FunLike F α β<VAR>s : Multiset α<VAR>comm : {x | x ∈ s}.Pairwise Commute<VAR>m : α<VAR>h : ∀ x ∈ s, x = m<GOAL>s.noncommProd comm = m ^ card s
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β → β<VAR>op : α → α → α<VAR>inst✝² : Monoid α<VAR>inst✝¹ : Monoid β<VAR>inst✝ : FunLike F α β<VAR>m : α<VAR>a✝ : List α<VAR>comm : {x | x ∈ ⟦a✝⟧}.Pairwise Commute<VAR>h : ∀ x ∈ ⟦a✝⟧, x = m<GOAL>noncommProd ⟦a✝⟧ comm = m ^ card ⟦a✝⟧
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β → β<VAR>op : α → α → α<VAR>inst✝² : Monoid α<VAR>inst✝¹ : Monoid β<VAR>inst✝ : FunLike F α β<VAR>m : α<VAR>a✝ : List α<VAR>comm : {x | x ∈ ⟦a✝⟧}.Pairwise Commute<VAR>h : ∀ x ∈ a✝, x = m<GOAL>a✝.prod = m ^ a✝.length
<VAR>α : Type u<VAR>β : Type v<VAR>s : Finset α<VAR>f : Perm α<VAR>h : ∀ x ∈ s, f x ∈ s<VAR>y : α<VAR>hy : y ∈ s<GOAL>f⁻¹ y ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>s : Finset α<VAR>f : Perm α<VAR>h : ∀ x ∈ s, f x ∈ s<VAR>y : α<VAR>hy : y ∈ s<VAR>h0 : ∀ y ∈ s, ∃ x, ∃ (hx : x ∈ s), y = (fun i x => f i) x hx<GOAL>f⁻¹ y ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>s : Finset α<VAR>f : Perm α<VAR>h : ∀ x ∈ s, f x ∈ s<VAR>y : α<VAR>hy : y ∈ s<VAR>h0 : ∀ y ∈ s, ∃ x, ∃ (hx : x ∈ s), y = (fun i x => f i) x hx<VAR>y2 : α<VAR>hy2 : y2 ∈ s<VAR>heq : y = (fun i x => f i) y2 hy2<GOAL>f⁻¹ ((fun i x => f i) y2 hy2) = y2
<VAR>n : ℤ<GOAL>|n|.negOnePow = n.negOnePow
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : NormedLinearOrderedField K<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace K E<VAR>b : Basis ι K E<VAR>inst✝¹ : FloorRing K<VAR>inst✝ : Fintype ι<VAR>y : ↥(span ℤ (Set.range ⇑b))<VAR>x : E<GOAL>y +ᵥ x ∈ fundamentalDomain b ↔ y = -floor b x
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace α'<VAR>inst✝² : One β<VAR>inst✝¹ : One γ<VAR>inst✝ : One δ<VAR>g : β → γ<VAR>f : α → β<VAR>f₂ : α → γ<VAR>m : β → γ → δ<VAR>x : α<VAR>K : Set α<VAR>hK : IsCompact K<VAR>h'K : IsClosed K<VAR>hfK : ∀ x ∉ K, f x = 1<GOAL>HasCompactMulSupport f
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace α'<VAR>inst✝² : One β<VAR>inst✝¹ : One γ<VAR>inst✝ : One δ<VAR>g : β → γ<VAR>f : α → β<VAR>f₂ : α → γ<VAR>m : β → γ → δ<VAR>x : α<VAR>K : Set α<VAR>hK : IsCompact K<VAR>h'K : IsClosed K<VAR>hfK : ∀ x ∉ K, f x = 1<VAR>this : mulTSupport f ⊆ K<GOAL>HasCompactMulSupport f
<VAR>E : Type u<VAR>F : Type v<VAR>inst✝¹ : PseudoEMetricSpace F<VAR>inst✝ : PseudoEMetricSpace E<VAR>K : Set E<VAR>comp : IsCompact K<VAR>f : E → F<VAR>D : Set E<VAR>ε : ℝ≥0∞<VAR>hK : ∀ x ∈ K, oscillationWithin f D x < ε<VAR>S : ℝ → Set E := fun r => {x | ∃ a > r, diam (f '' (ball x (ENNReal.ofReal a) ∩ D)) ≤ ε}<GOAL>∃ δ > 0, ∀ x ∈ K, diam (f '' (ball x (ENNReal.ofReal δ) ∩ D)) ≤ ε
<VAR>E : Type u<VAR>F : Type v<VAR>inst✝¹ : PseudoEMetricSpace F<VAR>inst✝ : PseudoEMetricSpace E<VAR>K : Set E<VAR>comp : IsCompact K<VAR>f : E → F<VAR>D : Set E<VAR>ε : ℝ≥0∞<VAR>hK : ∀ x ∈ K, oscillationWithin f D x < ε<VAR>S : ℝ → Set E := fun r => {x | ∃ a > r, diam (f '' (ball x (ENNReal.ofReal a) ∩ D)) ≤ ε}<VAR>S_open : ∀ r > 0, IsOpen (S r)<GOAL>∃ δ > 0, ∀ x ∈ K, diam (f '' (ball x (ENNReal.ofReal δ) ∩ D)) ≤ ε
<VAR>E : Type u<VAR>F : Type v<VAR>inst✝¹ : PseudoEMetricSpace F<VAR>inst✝ : PseudoEMetricSpace E<VAR>K : Set E<VAR>comp : IsCompact K<VAR>f : E → F<VAR>D : Set E<VAR>ε : ℝ≥0∞<VAR>hK : ∀ x ∈ K, oscillationWithin f D x < ε<VAR>S : ℝ → Set E := fun r => {x | ∃ a > r, diam (f '' (ball x (ENNReal.ofReal a) ∩ D)) ≤ ε}<VAR>S_open : ∀ r > 0, IsOpen (S r)<VAR>S_cover : K ⊆ ⋃ r, ⋃ (_ : r > 0), S r<GOAL>∃ δ > 0, ∀ x ∈ K, diam (f '' (ball x (ENNReal.ofReal δ) ∩ D)) ≤ ε
<VAR>E : Type u<VAR>F : Type v<VAR>inst✝¹ : PseudoEMetricSpace F<VAR>inst✝ : PseudoEMetricSpace E<VAR>K : Set E<VAR>comp : IsCompact K<VAR>f : E → F<VAR>D : Set E<VAR>ε : ℝ≥0∞<VAR>hK : ∀ x ∈ K, oscillationWithin f D x < ε<VAR>S : ℝ → Set E := fun r => {x | ∃ a > r, diam (f '' (ball x (ENNReal.ofReal a) ∩ D)) ≤ ε}<VAR>S_open : ∀ r > 0, IsOpen (S r)<VAR>S_cover : K ⊆ ⋃ r, ⋃ (_ : r > 0), S r<VAR>S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁<GOAL>∃ δ > 0, ∀ x ∈ K, diam (f '' (ball x (ENNReal.ofReal δ) ∩ D)) ≤ ε
<VAR>E : Type u<VAR>F : Type v<VAR>inst✝¹ : PseudoEMetricSpace F<VAR>inst✝ : PseudoEMetricSpace E<VAR>K : Set E<VAR>comp : IsCompact K<VAR>f : E → F<VAR>D : Set E<VAR>ε : ℝ≥0∞<VAR>hK : ∀ x ∈ K, oscillationWithin f D x < ε<VAR>S : ℝ → Set E := fun r => {x | ∃ a > r, diam (f '' (ball x (ENNReal.ofReal a) ∩ D)) ≤ ε}<VAR>S_open : ∀ r > 0, IsOpen (S r)<VAR>S_cover : K ⊆ ⋃ r, ⋃ (_ : r > 0), S r<VAR>S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁<VAR>δ : ℝ<VAR>δ0 : δ > 0<VAR>hδ : K ⊆ S δ<GOAL>∃ δ > 0, ∀ x ∈ K, diam (f '' (ball x (ENNReal.ofReal δ) ∩ D)) ≤ ε
<VAR>E : Type u<VAR>F : Type v<VAR>inst✝¹ : PseudoEMetricSpace F<VAR>inst✝ : PseudoEMetricSpace E<VAR>K : Set E<VAR>comp : IsCompact K<VAR>f : E → F<VAR>D : Set E<VAR>ε : ℝ≥0∞<VAR>hK : ∀ x ∈ K, oscillationWithin f D x < ε<VAR>S : ℝ → Set E := fun r => {x | ∃ a > r, diam (f '' (ball x (ENNReal.ofReal a) ∩ D)) ≤ ε}<VAR>S_open : ∀ r > 0, IsOpen (S r)<VAR>S_cover : K ⊆ ⋃ r, ⋃ (_ : r > 0), S r<VAR>S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁<VAR>δ : ℝ<VAR>δ0 : δ > 0<VAR>hδ : K ⊆ S δ<GOAL>∀ x ∈ K, diam (f '' (ball x (ENNReal.ofReal δ) ∩ D)) ≤ ε
<VAR>E : Type u<VAR>F : Type v<VAR>inst✝¹ : PseudoEMetricSpace F<VAR>inst✝ : PseudoEMetricSpace E<VAR>K : Set E<VAR>comp : IsCompact K<VAR>f : E → F<VAR>D : Set E<VAR>ε : ℝ≥0∞<VAR>hK : ∀ x ∈ K, oscillationWithin f D x < ε<VAR>S : ℝ → Set E := fun r => {x | ∃ a > r, diam (f '' (ball x (ENNReal.ofReal a) ∩ D)) ≤ ε}<VAR>S_open : ∀ r > 0, IsOpen (S r)<VAR>S_cover : K ⊆ ⋃ r, ⋃ (_ : r > 0), S r<VAR>S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁<VAR>δ : ℝ<VAR>δ0 : δ > 0<VAR>hδ : K ⊆ S δ<VAR>x : E<VAR>xK : x ∈ K<VAR>a : ℝ<VAR>δa : a > δ<VAR>ha : diam (f '' (ball x (ENNReal.ofReal a) ∩ D)) ≤ ε<GOAL>diam (f '' (ball x (ENNReal.ofReal δ) ∩ D)) ≤ ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>x✝ : E<GOAL>(reflection ⊥) x✝ = (LinearIsometryEquiv.neg 𝕜) 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>V' : Type u_3<VAR>P' : Type u_4<VAR>inst✝³ : NormedAddCommGroup V'<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : MetricSpace P'<VAR>inst✝ : NormedAddTorsor V' P'<VAR>f : P → P'<VAR>h : Isometry f<VAR>p₁ p₂ x : P<GOAL>x ∈ f ⁻¹' ↑(perpBisector (f p₁) (f p₂)) ↔ x ∈ ↑(perpBisector p₁ p₂)
<VAR>α : Type u_1<VAR>inst✝¹ : AddCommGroupWithOne α<VAR>inst✝ : CharZero α<VAR>a b z : ℤ<GOAL>↑a ≡ ↑b [PMOD ↑z] ↔ a ≡ b [PMOD z]
<VAR>α : Type u_1<VAR>inst✝¹ : AddCommGroupWithOne α<VAR>inst✝ : CharZero α<VAR>a b z : ℤ<GOAL>(∃ z_1, ↑b - ↑a = ↑(z_1 * z)) ↔ ∃ z_1, b - a = z_1 • z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Preorder ι<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : SupConvergenceClass α<VAR>f : ι → α<VAR>a : α<VAR>h_mono : Monotone f<VAR>ha : IsLUB (range f) a<GOAL>Tendsto f atTop (𝓝 a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Preorder ι<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : SupConvergenceClass α<VAR>f : ι → α<VAR>a : α<VAR>h_mono : Monotone f<VAR>ha : IsLUB (range f) a<GOAL>Tendsto (rangeFactorization f) atTop atTop
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a : A<VAR>u : Aˣ<GOAL>spectrum R (↑u⁻¹ * a * ↑u) = spectrum R a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>x : β<VAR>ε : α<VAR>ε0 : ε > 0<VAR>j : ℕ<VAR>x✝ : j ≥ 0<GOAL>abv ((fun x_1 => x) j - (fun x_1 => x) 0) < ε