ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁸ : Countable ι<VAR>f✝ g : α → β<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OpensMeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : PseudoMetrizableSpace β<VAR>inst✝¹ : BorelSpace β<VAR>inst✝ : One β<VAR>f : α → β<VAR>hf : Continuous f<VAR>k : Set α<VAR>hk : IsCompact k<VAR>h'f : mulSupport f ⊆ k<VAR>this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β<GOAL>StronglyMeasurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁸ : Countable ι<VAR>f✝ g : α → β<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OpensMeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : PseudoMetrizableSpace β<VAR>inst✝¹ : BorelSpace β<VAR>inst✝ : One β<VAR>f : α → β<VAR>hf : Continuous f<VAR>k : Set α<VAR>hk : IsCompact k<VAR>h'f : mulSupport f ⊆ k<VAR>this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β<GOAL>Measurable f ∧ IsSeparable (range f)
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderClosedTopology α<VAR>a b c d : α<VAR>h : a < b<GOAL>𝓝ˢ (Ico a b) = 𝓝 a ⊔ 𝓟 (Ioo a b)
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.LeftHomologyData<VAR>inst✝ : S.HasLeftHomology<GOAL>cyclesMap' (𝟙 S) S.leftHomologyData h ≫ h.i = S.leftHomologyData.i
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MulAction G α<VAR>inst✝⁴ : MeasurableSpace α<VAR>ν : Measure α<VAR>inst✝³ : Countable G<VAR>inst✝² : MeasurableSpace G<VAR>inst✝¹ : SMulInvariantMeasure G α ν<VAR>inst✝ : MeasurableSMul G α<VAR>μ : Measure (Quotient α_mod_G)<VAR>s : Set α<VAR>fund_dom_s : IsFundamentalDomain G s ν<VAR>h : μ = Measure.map (Quotient.mk α_mod_G) (ν.restrict s)<GOAL>QuotientMeasureEqMeasurePreimage ν μ
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : SMulCommClass ℝ 𝕜 F<VAR>k n : ℕ<VAR>f : 𝓢(E, F)<VAR>c : 𝕜<VAR>x : E<GOAL>‖x‖ ^ k * ‖iteratedFDeriv ℝ n (c • ⇑f) x‖ = ‖c‖ * ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Ring α<VAR>inst✝ : StarRing α<VAR>M : Matrix n n α<VAR>d : ℤ<GOAL>M = (↑d)ᴴ ↔ M = ↑d
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : NonAssocSemiring α<VAR>n : α<GOAL>1 * n + 1 * n = n + n
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₂ : Type u_3<VAR>M₃ : Type u_4<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module R M₃<VAR>f : M →ₗ[R] M₂<VAR>p p' : Submodule R M<GOAL>Function.Surjective ⇑(quotientInfToSupQuotient p p')
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₂ : Type u_3<VAR>M₃ : Type u_4<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module R M₃<VAR>f : M →ₗ[R] M₂<VAR>p p' : Submodule R M<GOAL>∀ (x : ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p'), x ∈ range (subToSupQuotient p p')
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₂ : Type u_3<VAR>M₃ : Type u_4<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module R M₃<VAR>f : M →ₗ[R] M₂<VAR>p p' : Submodule R M<VAR>x✝ : ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p'<VAR>x : M<VAR>hx : x ∈ p ⊔ p'<GOAL>Quot.mk Setoid.r ⟨x, hx⟩ ∈ range (subToSupQuotient p p')
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₂ : Type u_3<VAR>M₃ : Type u_4<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module R M₃<VAR>f : M →ₗ[R] M₂<VAR>p p' : Submodule R M<VAR>x✝ : ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p'<VAR>y : M<VAR>hy : y ∈ p<VAR>z : M<VAR>hz : z ∈ p'<VAR>hx : y + z ∈ p ⊔ p'<GOAL>Quot.mk Setoid.r ⟨y + z, hx⟩ ∈ range (subToSupQuotient p p')
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₂ : Type u_3<VAR>M₃ : Type u_4<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module R M₃<VAR>f : M →ₗ[R] M₂<VAR>p p' : Submodule R M<VAR>x✝ : ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p'<VAR>y : M<VAR>hy : y ∈ p<VAR>z : M<VAR>hz : z ∈ p'<VAR>hx : y + z ∈ p ⊔ p'<GOAL>(subToSupQuotient p p') ⟨y, hy⟩ = Quot.mk Setoid.r ⟨y + z, hx⟩
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₂ : Type u_3<VAR>M₃ : Type u_4<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module R M₃<VAR>f : M →ₗ[R] M₂<VAR>p p' : Submodule R M<VAR>x✝ : ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p'<VAR>y : M<VAR>hy : y ∈ p<VAR>z : M<VAR>hz : z ∈ p'<VAR>hx : y + z ∈ p ⊔ p'<GOAL>(inclusion ⋯) ⟨y, hy⟩ - ⟨y + z, hx⟩ ∈ comap (p ⊔ p').subtype p'
<VAR>n m : ℕ<VAR>inst✝ : NeZero n<VAR>h : optParam (1 ≠ 0) ⋯<GOAL>pred 1 h = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>S : Type u_10<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Nontrivial S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Module S M<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsScalarTower R S M<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>b : Basis ι S M<VAR>i : ι<GOAL>↑((restrictScalars R b) i) = b i
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>c : ℂ<VAR>R : ℝ<VAR>h0 : 0 < R<VAR>f : ℂ → E<VAR>y : E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hc : ContinuousOn f (closedBall c R \ {c})<VAR>hd : ∀ z ∈ (ball c R \ {c}) \ s, DifferentiableAt ℂ f z<VAR>hy : Tendsto f (𝓝[≠] c) (𝓝 y)<GOAL>(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) = (2 * ↑π * I) • y
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>c : ℂ<VAR>R : ℝ<VAR>h0 : 0 < R<VAR>f : ℂ → E<VAR>y : E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hc : ContinuousOn f (closedBall c R \ {c})<VAR>hd : ∀ z ∈ (ball c R \ {c}) \ s, DifferentiableAt ℂ f z<VAR>hy : Tendsto f (𝓝[≠] c) (𝓝 y)<GOAL>‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • y‖ ≤ 0
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>c : ℂ<VAR>R : ℝ<VAR>h0 : 0 < R<VAR>f : ℂ → E<VAR>y : E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hc : ContinuousOn f (closedBall c R \ {c})<VAR>hd : ∀ z ∈ (ball c R \ {c}) \ s, DifferentiableAt ℂ f z<VAR>hy : Tendsto f (𝓝[≠] c) (𝓝 y)<VAR>ε : ℝ<VAR>ε0 : 0 < ε<GOAL>‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • y‖ ≤ ε
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>c : ℂ<VAR>R : ℝ<VAR>h0 : 0 < R<VAR>f : ℂ → E<VAR>y : E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hc : ContinuousOn f (closedBall c R \ {c})<VAR>hd : ∀ z ∈ (ball c R \ {c}) \ s, DifferentiableAt ℂ f z<VAR>hy : Tendsto f (𝓝[≠] c) (𝓝 y)<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>δ : ℝ<VAR>δ0 : δ > 0<VAR>hδ : ∀ z ∈ closedBall c δ \ {c}, dist (f z) y < ε / (2 * π)<GOAL>‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • y‖ ≤ ε
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>c : ℂ<VAR>R : ℝ<VAR>h0 : 0 < R<VAR>f : ℂ → E<VAR>y : E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hc : ContinuousOn f (closedBall c R \ {c})<VAR>hd : ∀ z ∈ (ball c R \ {c}) \ s, DifferentiableAt ℂ f z<VAR>hy : Tendsto f (𝓝[≠] c) (𝓝 y)<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>δ : ℝ<VAR>δ0 : δ > 0<VAR>hδ : ∀ z ∈ closedBall c δ \ {c}, dist (f z) y < ε / (2 * π)<VAR>r : ℝ<VAR>hr0 : 0 < r<VAR>hrδ : r ≤ δ<VAR>hrR : r ≤ R<GOAL>‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • y‖ ≤ ε
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>c : ℂ<VAR>R : ℝ<VAR>h0 : 0 < R<VAR>f : ℂ → E<VAR>y : E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hc : ContinuousOn f (closedBall c R \ {c})<VAR>hd : ∀ z ∈ (ball c R \ {c}) \ s, DifferentiableAt ℂ f z<VAR>hy : Tendsto f (𝓝[≠] c) (𝓝 y)<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>δ : ℝ<VAR>δ0 : δ > 0<VAR>hδ : ∀ z ∈ closedBall c δ \ {c}, dist (f z) y < ε / (2 * π)<VAR>r : ℝ<VAR>hr0 : 0 < r<VAR>hrδ : r ≤ δ<VAR>hrR : r ≤ R<VAR>hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}<GOAL>‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • y‖ ≤ ε
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>c : ℂ<VAR>R : ℝ<VAR>h0 : 0 < R<VAR>f : ℂ → E<VAR>y : E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hc : ContinuousOn f (closedBall c R \ {c})<VAR>hd : ∀ z ∈ (ball c R \ {c}) \ s, DifferentiableAt ℂ f z<VAR>hy : Tendsto f (𝓝[≠] c) (𝓝 y)<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>δ : ℝ<VAR>δ0 : δ > 0<VAR>hδ : ∀ z ∈ closedBall c δ \ {c}, dist (f z) y < ε / (2 * π)<VAR>r : ℝ<VAR>hr0 : 0 < r<VAR>hrδ : r ≤ δ<VAR>hrR : r ≤ R<VAR>hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}<VAR>hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}<GOAL>‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • y‖ ≤ ε
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>c : ℂ<VAR>R : ℝ<VAR>h0 : 0 < R<VAR>f : ℂ → E<VAR>y : E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hc : ContinuousOn f (closedBall c R \ {c})<VAR>hd : ∀ z ∈ (ball c R \ {c}) \ s, DifferentiableAt ℂ f z<VAR>hy : Tendsto f (𝓝[≠] c) (𝓝 y)<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>δ : ℝ<VAR>δ0 : δ > 0<VAR>hδ : ∀ z ∈ closedBall c δ \ {c}, dist (f z) y < ε / (2 * π)<VAR>r : ℝ<VAR>hr0 : 0 < r<VAR>hrδ : r ≤ δ<VAR>hrR : r ≤ R<VAR>hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}<VAR>hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}<VAR>hzne : ∀ z ∈ sphere c r, z ≠ c<GOAL>‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • y‖ ≤ ε
<VAR>m n k : ℕ<VAR>hk : k + 1 < n + 2<GOAL>⟨k + 1, hk⟩ < ⟨k + 1, hk⟩ - 1 ↔ ⟨k + 1, hk⟩ = 0
<VAR>m n k : ℕ<VAR>hk : k + 1 < n + 2<VAR>this : (n + 1 + (k + 1)) % (n + 2) = k % (n + 2)<GOAL>⟨k + 1, hk⟩ < ⟨k + 1, hk⟩ - 1 ↔ ⟨k + 1, hk⟩ = 0
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Subsingleton A<VAR>a : A<GOAL>resolventSet R a = univ
<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<GOAL>IsPGroup (Nat.card ↥N).minFac ↥N
<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>this : Fact (Nat.Prime (Nat.card ↥N).minFac)<GOAL>IsPGroup (Nat.card ↥N).minFac ↥N
<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>this : Fact (Nat.Prime (Nat.card ↥N).minFac)<VAR>P : Sylow (Nat.card ↥N).minFac ↥N<GOAL>Function.Surjective ⇑(↑P).subtype
<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>this : Fact (Nat.Prime (Nat.card ↥N).minFac)<VAR>P : Sylow (Nat.card ↥N).minFac ↥N<GOAL>↑P = ⊤
<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>this✝ : Fact (Nat.Prime (Nat.card ↥N).minFac)<VAR>P : Sylow (Nat.card ↥N).minFac ↥N<VAR>this : (map N.subtype ↑P).Normal<GOAL>↑P = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : PseudoEMetricSpace α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>f✝ f : β → α<VAR>hf : Measurable f<VAR>s : Set α<VAR>y₀ : α<VAR>h₀ : y₀ ∈ s<VAR>inst✝ : SeparableSpace ↑s<VAR>x : β<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>edist (↑(approxOn f hf s y₀ h₀ n) x) (f x) ≤ edist (↑(approxOn f hf s y₀ h₀ m) x) (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : PseudoEMetricSpace α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>f✝ f : β → α<VAR>hf : Measurable f<VAR>s : Set α<VAR>y₀ : α<VAR>h₀ : y₀ ∈ s<VAR>inst✝ : SeparableSpace ↑s<VAR>x : β<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>edist (↑(nearestPt (fun k => Nat.rec y₀ (fun n n_ih => ↑(denseSeq (↑s) n)) k) n) (f x)) (f x) ≤ edist (↑(nearestPt (fun k => Nat.rec y₀ (fun n n_ih => ↑(denseSeq (↑s) n)) k) m) (f x)) (f x)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p✝ q : R[X]<VAR>c : R[X]ˣ<VAR>p : R[X]<GOAL>(↑c).coeff 0 • p = ↑c * p
<VAR>L : Language<VAR>L' : Language<VAR>M✝ : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : L.Structure M✝<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n l : ℕ<VAR>φ✝ ψ : L.BoundedFormula α l<VAR>θ : L.BoundedFormula α l.succ<VAR>v✝ : α → M✝<VAR>xs✝ : Fin l → M✝<VAR>inst✝ : Nonempty M✝<VAR>φ : L.BoundedFormula α n<VAR>M : ∅.ModelType<VAR>v : α → ↑M<VAR>xs : Fin n → ↑M<GOAL>(φ ⇔ φ.toPrenex).Realize v xs
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type w'<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>P : Type u_1<VAR>inst✝¹ : L.Structure P<VAR>Q : Type u_2<VAR>inst✝ : L.Structure Q<VAR>h : N ↪[L] P<VAR>f g : M →[L] N<VAR>hfg : h.toHom.comp f = h.toHom.comp g<VAR>x : M<GOAL>f x = g x
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>X✝ Y Z : C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>X : C<VAR>p : Subobject X → Prop<VAR>h : ∀ ⦃A : C⦄ (f : A ⟶ X) [inst : Mono f], p (mk f)<VAR>P : Subobject X<GOAL>p P
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>X✝ Y Z : C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>X : C<VAR>p : Subobject X → Prop<VAR>h : ∀ ⦃A : C⦄ (f : A ⟶ X) [inst : Mono f], p (mk f)<VAR>P : Subobject X<GOAL>∀ (a : MonoOver X), p (Quotient.mk'' a)
<VAR>M : Type u_1<VAR>inst✝⁵ : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝⁴ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝³ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>T : Submonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>inst✝² : CommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>A : Type u_5<VAR>inst✝¹ : CommMonoid A<VAR>U : Submonoid A<VAR>R : Type u_6<VAR>inst✝ : CommMonoid R<VAR>j : U.LocalizationMap R<VAR>l : P →* A<VAR>hl : ∀ (w : ↥T), l ↑w ∈ U<VAR>x : N<GOAL>(k.map hl j) ((f.map hy k) x) = (f.map ⋯ j) x
<VAR>M : Type u_1<VAR>inst✝⁵ : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝⁴ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝³ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>T : Submonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>inst✝² : CommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>A : Type u_5<VAR>inst✝¹ : CommMonoid A<VAR>U : Submonoid A<VAR>R : Type u_6<VAR>inst✝ : CommMonoid R<VAR>j : U.LocalizationMap R<VAR>l : P →* A<VAR>hl : ∀ (w : ↥T), l ↑w ∈ U<VAR>x : N<GOAL>(k.map hl j) ((f.map hy k) x) = ((k.map hl j).comp (f.map hy k)) x
<VAR>α✝ : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α✝<VAR>α : Type u_3<VAR>inst✝ : PseudoMetricSpace α<VAR>r : ℝ<VAR>hpos : 0 < r<VAR>hr : Pairwise fun x x_1 => r ≤ dist x x_1<GOAL>UniformSpace.toTopologicalSpace = ⊥
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>P : Set X → Prop<VAR>c : CU P<VAR>x : X<GOAL>c.lim x = midpoint ℝ (c.left.lim x) (c.right.lim x)
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>P : Set X → Prop<VAR>c : CU P<VAR>x : X<GOAL>Tendsto (fun n => approx (n + 1) c x) atTop (𝓝 (midpoint ℝ (c.left.lim x) (c.right.lim x)))
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>P : Set X → Prop<VAR>c : CU P<VAR>x : X<GOAL>Tendsto (fun n => midpoint ℝ (approx n c.left x) (approx n c.right x)) atTop (𝓝 (midpoint ℝ (c.left.lim x) (c.right.lim x)))
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : AffineSubspace k P<VAR>p : P<VAR>hp : p ∈ s<GOAL>↑s.direction = (fun x => x -ᵥ p) '' ↑s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : AffineSubspace k P<VAR>p : P<VAR>hp : p ∈ s<GOAL>↑s -ᵥ ↑s = (fun x => x -ᵥ p) '' ↑s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : AffineSubspace k P<VAR>p : P<VAR>hp : p ∈ s<GOAL>↑s -ᵥ ↑s ≤ (fun x => x -ᵥ p) '' ↑s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : AffineSubspace k P<VAR>p : P<VAR>hp : p ∈ s<GOAL>(fun x => x -ᵥ p) '' ↑s ≤ ↑s -ᵥ ↑s
<VAR>α : Type u_1<VAR>inst✝¹ : BEq α<VAR>inst✝ : LawfulBEq α<VAR>a : α<VAR>l₁ l₂ : List α<GOAL>(a :: l₁).diff l₂ = if a ∈ l₂ then l₁.diff (l₂.erase a) else a :: l₁.diff l₂
<VAR>α✝ : Sort u<VAR>β✝ : Sort v<VAR>γ : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Injective f<VAR>u s : Set α<VAR>a : α<VAR>has : a ∈ s<GOAL>⟨f a, ⋯⟩ ∈ (fun x => ↑((Set.image f s hf).symm x)) ⁻¹' u ↔ ⟨f a, ⋯⟩ ∈ Subtype.val ⁻¹' (f '' u)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<GOAL>(ReflTransGen fun x x_1 => x ⩿ x_1) = ReflTransGen fun x x_1 => x ⋖ x_1
<VAR>x y : PartENat<VAR>h : x < y<GOAL>x + 1 ≤ y
<VAR>x : PartENat<VAR>h : x < ⊤<GOAL>x + 1 ≤ ⊤
<VAR>x : PartENat<VAR>n : ℕ<VAR>h : x < ↑n<GOAL>x + 1 ≤ ↑n
<VAR>n m : ℕ<VAR>h : ↑m < ↑n<GOAL>↑m + 1 ≤ ↑n
<VAR>n m : ℕ<VAR>h : ↑m < ↑n<GOAL>m + 1 ≤ n
<VAR>n m : ℕ<VAR>h : ↑m < ↑n<GOAL>m < n
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝ : MeasurableSpace X<VAR>f : X → ℝ<VAR>m m0 : MeasurableSpace X<VAR>μ : Measure X<VAR>g : SimpleFunc X ℝ<VAR>hf : Integrable f μ<GOAL>Integrable (↑g * f) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝ : MeasurableSpace X<VAR>f : X → ℝ<VAR>m m0 : MeasurableSpace X<VAR>μ : Measure X<VAR>g : SimpleFunc X ℝ<VAR>hf : Integrable f μ<VAR>c : ℝ<VAR>s : Set X<VAR>hs : MeasurableSet s<GOAL>Integrable (↑(SimpleFunc.piecewise s hs (SimpleFunc.const X c) (SimpleFunc.const X 0)) * f) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝ : MeasurableSpace X<VAR>f : X → ℝ<VAR>m m0 : MeasurableSpace X<VAR>μ : Measure X<VAR>g : SimpleFunc X ℝ<VAR>hf : Integrable f μ<VAR>c : ℝ<VAR>s : Set X<VAR>hs : MeasurableSet s<GOAL>Integrable (s.indicator (const X c) * f) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝ : MeasurableSpace X<VAR>f : X → ℝ<VAR>m m0 : MeasurableSpace X<VAR>μ : Measure X<VAR>g : SimpleFunc X ℝ<VAR>hf : Integrable f μ<VAR>c : ℝ<VAR>s : Set X<VAR>hs : MeasurableSet s<VAR>this : s.indicator (const X c) * f = s.indicator (c • f)<GOAL>Integrable (s.indicator (const X c) * f) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝ : MeasurableSpace X<VAR>f : X → ℝ<VAR>m m0 : MeasurableSpace X<VAR>μ : Measure X<VAR>g : SimpleFunc X ℝ<VAR>hf : Integrable f μ<VAR>c : ℝ<VAR>s : Set X<VAR>hs : MeasurableSet s<VAR>this : s.indicator (const X c) * f = s.indicator (c • f)<GOAL>IntegrableOn (c • f) s μ
<VAR>P : MorphismProperty Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>inst✝ : HasRingHomProperty P Q<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>R S : CommRingCat<VAR>φ : R ⟶ S<GOAL>P (Spec.map φ) ↔ Q φ
<VAR>P : MorphismProperty Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>inst✝ : HasRingHomProperty P Q<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>R S : CommRingCat<VAR>φ : R ⟶ S<VAR>H : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q<GOAL>P (Spec.map φ) ↔ Q φ
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>x ∈ Submodule.span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I)) ↔ x ∈ ⇑(mixedEmbedding K) '' ↑↑I
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>x ∈ Submodule.span ℤ (⇑(mixedEmbedding K).toIntAlgHom.toLinearMap '' Set.range ⇑(basisOfFractionalIdeal K I)) ↔ x ∈ ⇑(mixedEmbedding K) '' ↑↑I
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>x ∈ ⇑(mixedEmbedding K).toIntAlgHom.toLinearMap '' ↑(Submodule.span ℤ (Set.range ⇑(basisOfFractionalIdeal K I))) ↔ x ∈ ⇑(mixedEmbedding K) '' ↑↑I
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>x ∈ ⇑(mixedEmbedding K).toIntAlgHom.toLinearMap '' ↑↑I ↔ x ∈ ⇑(mixedEmbedding K) '' ↑↑I
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_6, u_1} C<VAR>inst✝² : Category.{u_4, u_2} D<VAR>L : C ⥤ D<VAR>H : Type u_3<VAR>inst✝¹ : Category.{u_5, u_3} H<VAR>inst✝ : ∀ (F : C ⥤ H), L.HasRightKanExtension F<VAR>G : D ⥤ H<GOAL>whiskerLeft L ((L.ranAdjunction H).unit.app G) ≫ L.ranCounit.app (L ⋙ G) = 𝟙 (L ⋙ G)
<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>W X Y Z : C<VAR>h : X ⟶ Z<VAR>k : Y ⟶ Z<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>comm : f ≫ h = g ≫ k<VAR>inst✝² : PreservesColimit (span f g) G<VAR>inst✝¹ : HasPushout f g<VAR>inst✝ : HasPushout (G.map f) (G.map g)<GOAL>G.map (pushout.inr f g) ≫ (iso G f g).inv = pushout.inr (G.map f) (G.map g)
<VAR>α β : Type u<VAR>c : Cardinal.{?u.225151}<VAR>S T : Set α<VAR>h : T ⊆ S<GOAL>#↑(S \ T) + #↑T = #↑S
<VAR>α β : Type u<VAR>c : Cardinal.{?u.225151}<VAR>S T : Set α<VAR>h : T ⊆ S<GOAL>Disjoint (S \ T) T
<VAR>I✝ : Type u<VAR>f : I✝ → Type v<VAR>I : Type u_1<VAR>J : Type u_2<VAR>α : Type u_3<VAR>x✝ : I → α<VAR>y : J → α<VAR>inst✝ : Star α<VAR>x : I ⊕ J<GOAL>star (Sum.elim x✝ y) x = Sum.elim (star x✝) (star y) x