ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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✝³ : Group α<VAR>inst✝² : DivisionMonoid β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : MonoidHomClass F α β<VAR>m : F<VAR>f g f₁ g₁ : Filter α<VAR>f₂ g₂ : Filter β<VAR>h : f.NeBot<VAR>s t₁ : Set α<VAR>h₁ : t₁ ∈ f<VAR>t₂ : Set α<VAR>h₂ : t₂ ∈ f<VAR>hs : t₁ / t₂ ⊆ s<VAR>a : α<VAR>ha₁ : a ∈ t₁<VAR>ha₂ : a ∈ t₂<GOAL>a / a ∈ s
<VAR>G : Type u_1<VAR>H✝ : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x✝ y : G<VAR>n m : ℕ<VAR>H : Submonoid G<VAR>x : ↥H<GOAL>IsOfFinOrder ↑x ↔ IsOfFinOrder x
<VAR>G : Type u_1<VAR>H✝ : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x✝ y : G<VAR>n m : ℕ<VAR>H : Submonoid G<VAR>x : ↥H<GOAL>(∃ n, 0 < n ∧ ↑x ^ n = 1) ↔ ∃ n, 0 < n ∧ x ^ n = 1
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Fintype F<VAR>inst✝ : DecidableEq F<VAR>a : F<VAR>ha : a ≠ 0<GOAL>(quadraticChar F) (a ^ 2) = 1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<GOAL>(C 4 * X ^ 3 + C W.b₂ * X ^ 2 + C (2 * W.b₄) * X + C W.b₆).coeff 3 = 4
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F : C × D ⥤ E<VAR>X X' : C<VAR>f : X ⟶ X'<VAR>Y Y' : D<VAR>g : Y ⟶ Y'<GOAL>F.map (f, 𝟙 Y) ≫ F.map (𝟙 X', g) = F.map (f, g)
<VAR>B : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} B<VAR>C : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>inst✝² : Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>inst✝¹ : Category.{v₄, u₄} E<VAR>H : Type u₅<VAR>inst✝ : Category.{v₅, u₅} H<VAR>F₁ F₂ : B ⥤ C ⥤ D<VAR>h : F₁.flip = F₂.flip<GOAL>F₁ = F₂
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>n : ℕ<VAR>a : Composition n<VAR>b : Composition a.length<VAR>i : Fin b.length<VAR>j : Fin (b.blocksFun i)<GOAL>((a.blocks.splitWrtComposition b).get ⟨↑⟨↑i, ⋯⟩, ⋯⟩).get ⟨↑j, ⋯⟩ = a.blocks.get ⟨↑((Fin.natAddOrderEmb (b.sizeUpTo ↑i)).toEmbedding j), ⋯⟩
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>n : ℕ<VAR>a : Composition n<VAR>b : Composition a.length<VAR>i : Fin b.length<VAR>j : Fin (b.blocksFun i)<GOAL>a.blocks.get ⟨↑⟨b.sizeUpTo ↑⟨↑⟨↑i, ⋯⟩, ⋯⟩ + ↑⟨↑⟨↑j, ⋯⟩, ⋯⟩, ⋯⟩, ⋯⟩ = a.blocks.get ⟨↑((Fin.natAddOrderEmb (b.sizeUpTo ↑i)).toEmbedding j), ⋯⟩
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>f_lim : α → E<VAR>B : ℕ → ℝ≥0∞<VAR>hB : ∑' (i : ℕ), B i ≠ ⊤<VAR>h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<GOAL>Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>f_lim : α → E<VAR>B : ℕ → ℝ≥0∞<VAR>hB : ∑' (i : ℕ), B i ≠ ⊤<VAR>h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<GOAL>∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>f_lim : α → E<VAR>B : ℕ → ℝ≥0∞<VAR>hB : ∑' (i : ℕ), B i ≠ ⊤<VAR>h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<GOAL>∃ N, ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>f_lim : α → E<VAR>B : ℕ → ℝ≥0∞<VAR>hB : ∑' (i : ℕ), B i ≠ ⊤<VAR>h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>h_B : ∃ N, B N ≤ ε<GOAL>∃ N, ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>f_lim : α → E<VAR>B : ℕ → ℝ≥0∞<VAR>hB : ∑' (i : ℕ), B i ≠ ⊤<VAR>h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>N : ℕ<VAR>h_B : B N ≤ ε<VAR>n : ℕ<VAR>hn : n ≥ N<GOAL>eLpNorm (f n - f_lim) p μ ≤ ε
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>f_lim : α → E<VAR>B : ℕ → ℝ≥0∞<VAR>hB : ∑' (i : ℕ), B i ≠ ⊤<VAR>h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>N : ℕ<VAR>h_B : B N ≤ ε<VAR>n : ℕ<VAR>hn : n ≥ N<VAR>h_sub : eLpNorm (f n - f_lim) p μ ≤ liminf (fun m => eLpNorm (f n - f m) p μ) atTop<GOAL>eLpNorm (f n - f_lim) p μ ≤ ε
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>f_lim : α → E<VAR>B : ℕ → ℝ≥0∞<VAR>hB : ∑' (i : ℕ), B i ≠ ⊤<VAR>h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>N : ℕ<VAR>h_B : B N ≤ ε<VAR>n : ℕ<VAR>hn : n ≥ N<VAR>h_sub : eLpNorm (f n - f_lim) p μ ≤ liminf (fun m => eLpNorm (f n - f m) p μ) atTop<GOAL>liminf (fun m => eLpNorm (f n - f m) p μ) atTop ≤ ε
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>f_lim : α → E<VAR>B : ℕ → ℝ≥0∞<VAR>hB : ∑' (i : ℕ), B i ≠ ⊤<VAR>h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>N : ℕ<VAR>h_B : B N ≤ ε<VAR>n : ℕ<VAR>hn : n ≥ N<VAR>h_sub : eLpNorm (f n - f_lim) p μ ≤ liminf (fun m => eLpNorm (f n - f m) p μ) atTop<GOAL>∀ (a : ℕ), ∃ b ≥ a, eLpNorm (f n - f b) p μ ≤ ε
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>f_lim : α → E<VAR>B : ℕ → ℝ≥0∞<VAR>hB : ∑' (i : ℕ), B i ≠ ⊤<VAR>h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>N : ℕ<VAR>h_B : B N ≤ ε<VAR>n : ℕ<VAR>hn : n ≥ N<VAR>h_sub : eLpNorm (f n - f_lim) p μ ≤ liminf (fun m => eLpNorm (f n - f m) p μ) atTop<VAR>N1 : ℕ<GOAL>eLpNorm (f n - f (max N N1)) p μ ≤ ε
<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>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f✝ g✝ : X → E<VAR>s✝ t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>Y : Type u_5<VAR>x✝ : MeasurableSpace Y<VAR>f : X → Y<VAR>hf : MeasurableEmbedding f<VAR>g : Y → E<VAR>s : Set Y<GOAL>∫ (y : Y) in s, g y ∂Measure.map f μ = ∫ (x : X) in f ⁻¹' s, g (f x) ∂μ
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>inst✝ : Fintype I<VAR>e : I → R<VAR>he : CompleteOrthogonalIdempotents fun x => 1 - e x<GOAL>Function.Bijective ⇑(Pi.ringHom fun i => Ideal.Quotient.mk (Ideal.span {e i}))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>inst✝ : Fintype I<VAR>e' : I → R<VAR>h : Function.Bijective ⇑(Pi.ringHom fun i => Ideal.Quotient.mk (Ideal.span {e' i}))<VAR>he : CompleteOrthogonalIdempotents fun x => 1 - e' x<GOAL>Function.Bijective ⇑(Pi.ringHom fun i => Ideal.Quotient.mk (Ideal.span {e' i}))
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ φ' : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>γ : LeftHomologyMapData φ h₁ h₂<VAR>γ' : LeftHomologyMapData φ' h₁ h₂<GOAL>cyclesMap' (φ + φ') h₁ h₂ = cyclesMap' φ h₁ h₂ + cyclesMap' φ' h₁ h₂
<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 : ZMod 2<GOAL>Submodule.map reverse (evenOdd Q n) = evenOdd Q n
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → Preorder (π i)<VAR>x y : (i : ι) → π i<VAR>i : ι<VAR>a b : π i<GOAL>x < update x i a ↔ x i < a
<VAR>𝕂 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕂<VAR>inst✝¹ : CompleteSpace 𝕂<VAR>inst✝ : CharZero 𝕂<VAR>x : 𝕂<VAR>hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝕂).radius<GOAL>HasStrictDerivAt (exp 𝕂) (exp 𝕂 x) x
<VAR>C✝ : Type u_1<VAR>inst✝⁵ : Category.{?u.4955, u_1} C✝<VAR>inst✝⁴ : MonoidalCategory C✝<VAR>inst✝³ : BraidedCategory C✝<VAR>C : Type u_2<VAR>inst✝² : Category.{u_3, u_2} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X Y W Z : C<GOAL>(tensor_μ C (X, W) (Y, Z)).op = tensor_μ Cᵒᵖ (op X, op Y) (op W, op Z)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>hr : (type r).IsLimit<VAR>x : α<GOAL>Bounded r {x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>hr : (type r).IsLimit<VAR>x : α<GOAL>∀ b ∈ {x}, r b (enum r (succ (typein r x)) ⋯)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>hr : (type r).IsLimit<VAR>x b : α<VAR>hb : b ∈ {x}<GOAL>r b (enum r (succ (typein r x)) ⋯)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>hr : (type r).IsLimit<VAR>x b : α<VAR>hb : b ∈ {x}<GOAL>r x (enum r (succ (typein r x)) ⋯)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>hr : (type r).IsLimit<VAR>x b : α<VAR>hb : b ∈ {x}<GOAL>r (enum r (typein r x) ⋯) (enum r (succ (typein r x)) ⋯)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>hr : (type r).IsLimit<VAR>x b : α<VAR>hb : b ∈ {x}<GOAL>typein r x < succ (typein r x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : Ring B<VAR>inst✝⁴ : CommRing S<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>f✝ : R →+* S<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : IsScalarTower R A B<VAR>x : A<VAR>f : R[X]<VAR>hf : f.Monic<VAR>hx : eval₂ (algebraMap R A) x f = 0<GOAL>IsIntegral R ((algebraMap A B) x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : Ring B<VAR>inst✝⁴ : CommRing S<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>f✝ : R →+* S<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : IsScalarTower R A B<VAR>x : A<VAR>f : R[X]<VAR>hf : f.Monic<VAR>hx : eval₂ (algebraMap R A) x f = 0<GOAL>eval₂ (algebraMap R B) ((algebraMap A B) x) f = 0
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w : V<VAR>inst✝ : DecidableEq V<VAR>u v : V<VAR>c : G.Walk v v<VAR>hc : c.IsCircuit<VAR>h : u ∈ c.support<GOAL>(c.rotate h).IsCircuit
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w : V<VAR>inst✝ : DecidableEq V<VAR>u v : V<VAR>c : G.Walk v v<VAR>hc : c.IsCircuit<VAR>h : u ∈ c.support<GOAL>c.rotate h ≠ nil
<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>S : L.Substructure M<VAR>A s : Set M<VAR>h : A ⊆ ↑S<VAR>a : M<VAR>ha : a ∈ A<GOAL>a ∈ ↑((closure (L[[↑A]])).toFun s)
<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>S : L.Substructure M<VAR>A s : Set M<VAR>h : A ⊆ ↑S<VAR>a : M<VAR>ha : a ∈ A<GOAL>a ∈ (closure (L[[↑A]])).toFun s
<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>S : L.Substructure M<VAR>A s : Set M<VAR>h : A ⊆ ↑S<VAR>a : M<VAR>ha : a ∈ A<VAR>a' : L[[↑A]].Constants := Sum.inr ⟨a, ha⟩<GOAL>a ∈ (closure (L[[↑A]])).toFun s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>x : α<GOAL>x ∈ r.inv.codom ↔ x ∈ r.dom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f✝ : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f : E'' → F''<VAR>x₀ : E''<VAR>n : ℕ<VAR>h : f =O[𝓝 x₀] fun x => ‖x - x₀‖ ^ n<VAR>hn : n ≠ 0<GOAL>f x₀ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f✝ : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f : E'' → F''<VAR>x₀ : E''<VAR>n : ℕ<VAR>h : f =O[𝓝[univ] x₀] fun x => ‖x - x₀‖ ^ n<VAR>hn : n ≠ 0<GOAL>f x₀ = 0
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : SeminormedRing 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SeminormedRing 𝕜₂<VAR>inst✝² : AddCommGroup E₂<VAR>inst✝¹ : Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>p : Seminorm 𝕜₂ E₂<VAR>f : E →ₛₗ[σ₁₂] E₂<VAR>x : E<VAR>r : ℝ<VAR>x✝ : E<GOAL>x✝ ∈ (p.comp f).ball x r ↔ x✝ ∈ ⇑f ⁻¹' p.ball (f x) r
<GOAL>UniformContinuous fun x => ↑x.1 + ↑x.2
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : CommRing T<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : Algebra R T<VAR>ι κ : Type w<VAR>inst✝⁴ : Fintype ι<VAR>b : Basis ι R S<VAR>inst✝³ : Module.Free R S<VAR>inst✝² : Module.Free R T<VAR>inst✝¹ : Module.Finite R S<VAR>inst✝ : Module.Finite R T<VAR>p : S × T<GOAL>(trace R (S × T)) p = ((trace R S).coprod (trace R T)) p
<VAR>P : TopCat → Prop<VAR>X✝ : Type u<VAR>inst✝³ : TopologicalSpace X✝<VAR>inst✝² : CompactSpace X✝<VAR>inst✝¹ : T2Space X✝<VAR>inst✝ : HasProp P X✝<VAR>X Y : CompHausLike P<VAR>f : X ⟶ Y<VAR>bij : Function.Bijective ⇑f<VAR>E : (forget (CompHausLike P)).obj X ≃ (forget (CompHausLike P)).obj Y := Equiv.ofBijective (⇑f) bij<GOAL>IsIso f
<VAR>P : TopCat → Prop<VAR>X✝ : Type u<VAR>inst✝³ : TopologicalSpace X✝<VAR>inst✝² : CompactSpace X✝<VAR>inst✝¹ : T2Space X✝<VAR>inst✝ : HasProp P X✝<VAR>X Y : CompHausLike P<VAR>f : X ⟶ Y<VAR>bij : Function.Bijective ⇑f<VAR>E : (forget (CompHausLike P)).obj X ≃ (forget (CompHausLike P)).obj Y := Equiv.ofBijective (⇑f) bij<VAR>hE : Continuous ⇑E.symm<GOAL>IsIso f
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroupWithZero α<VAR>a✝ b✝ c✝ d✝ : α<VAR>m n : ℕ<VAR>a b c d : α<VAR>hb : b ≠ 0<VAR>hd : d ≠ 0<GOAL>a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b
<VAR>C : Type u_1<VAR>inst✝³ : Category.{?u.117978, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>inst✝¹ : S₁.HasLeftHomology<VAR>inst✝ : S₂.HasLeftHomology<GOAL>leftHomologyMap e.hom ≫ leftHomologyMap e.inv = 𝟙 S₁.leftHomology
<VAR>C : Type u_1<VAR>inst✝³ : Category.{?u.117978, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>inst✝¹ : S₁.HasLeftHomology<VAR>inst✝ : S₂.HasLeftHomology<GOAL>leftHomologyMap e.inv ≫ leftHomologyMap e.hom = 𝟙 S₂.leftHomology
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>p✝ q✝ : Seminorm 𝕜 E<VAR>x : E<VAR>inst✝² : SMul R ℝ<VAR>inst✝¹ : SMul R ℝ≥0<VAR>inst✝ : IsScalarTower R ℝ≥0 ℝ<VAR>r : R<VAR>p q : Seminorm 𝕜 E<VAR>x✝ : E<GOAL>(r • (p ⊓ q)) x✝ = (r • p ⊓ r • q) x✝
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>h : P.toPoly = Q.toPoly<GOAL>P.b = Q.b
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>f : β → α → β<VAR>H : RightCommutative f<VAR>x : β<VAR>q : α → Prop<VAR>p : β → Prop<VAR>s : Multiset α<VAR>hpqf : ∀ (a : α) (b : β), q a → p b → p (f b a)<VAR>px : p x<VAR>q_s : ∀ a ∈ s, q a<GOAL>p (foldl f H x s)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>f : β → α → β<VAR>H : RightCommutative f<VAR>x : β<VAR>q : α → Prop<VAR>p : β → Prop<VAR>s : Multiset α<VAR>hpqf : ∀ (a : α) (b : β), q a → p b → p (f b a)<VAR>px : p x<VAR>q_s : ∀ a ∈ s, q a<GOAL>p (foldr (fun x y => f y x) ⋯ x s)
<VAR>α : Type u_1<VAR>a b c : α<VAR>inst✝² : Lattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : IsModularLattice α<VAR>h : Disjoint a b<VAR>hsup : Disjoint (a ⊔ b) c<GOAL>Disjoint a (b ⊔ c)
<VAR>α : Type u_1<VAR>a b c : α<VAR>inst✝² : Lattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : IsModularLattice α<VAR>h : Disjoint a b<VAR>hsup : Disjoint (a ⊔ b) c<GOAL>a ⊓ (c ⊔ b) ≤ a ⊓ b
<VAR>α : Type u_1<VAR>a b c : α<VAR>inst✝² : Lattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : IsModularLattice α<VAR>h : Disjoint a b<VAR>hsup : Disjoint (a ⊔ b) c<GOAL>a ⊓ (c ⊔ b) ≤ b
<VAR>α : Type u_1<VAR>a b c : α<VAR>inst✝² : Lattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : IsModularLattice α<VAR>h : Disjoint a b<VAR>hsup : Disjoint (a ⊔ b) c<GOAL>(?m.25858 ⊔ a) ⊓ (c ⊔ b) ≤ b
<VAR>α : Type u_1<VAR>a b c : α<VAR>inst✝² : Lattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : IsModularLattice α<VAR>h : Disjoint a b<VAR>hsup : Disjoint (a ⊔ b) c<GOAL>α
<VAR>x y : ℝ<GOAL>Real.toEReal '' Ico x y = Ico ↑x ↑y
<VAR>x y : ℝ<GOAL>WithBot.some '' (WithTop.some '' Ico x y) = Ico ↑x ↑y
<VAR>x y : ℝ<GOAL>Ico ↑↑x ↑↑y = Ico ↑x ↑y
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>hf'_nonpos : ∀ x ∈ interior D, deriv f x ≤ 0<VAR>x : ℝ<VAR>hx : x ∈ D<VAR>y : ℝ<VAR>hy : y ∈ D<VAR>hxy : x ≤ y<GOAL>f y ≤ f x
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>δ : ℕ → ℝ<VAR>hδ : Tendsto δ atTop (𝓝 0)<VAR>this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup Irreducible<VAR>μ : Measure 𝕊 := volume<VAR>u : Nat.Primes → 𝕊 := fun p => ↑(↑1 / ↑↑p * T)<GOAL>(∀ᵐ (x : 𝕊) ∂μ, ¬addWellApproximable 𝕊 δ x) ∨ ∀ᵐ (x : 𝕊) ∂μ, addWellApproximable 𝕊 δ x
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>δ : ℕ → ℝ<VAR>hδ : Tendsto δ atTop (𝓝 0)<VAR>this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup Irreducible<VAR>μ : Measure 𝕊 := volume<VAR>u : Nat.Primes → 𝕊 := fun p => ↑(↑1 / ↑↑p * T)<VAR>hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p<GOAL>(∀ᵐ (x : 𝕊) ∂μ, ¬addWellApproximable 𝕊 δ x) ∨ ∀ᵐ (x : 𝕊) ∂μ, addWellApproximable 𝕊 δ x
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>δ : ℕ → ℝ<VAR>hδ : Tendsto δ atTop (𝓝 0)<VAR>this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup Irreducible<VAR>μ : Measure 𝕊 := volume<VAR>u : Nat.Primes → 𝕊 := fun p => ↑(↑1 / ↑↑p * T)<VAR>hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p<VAR>hu : Tendsto (addOrderOf ∘ u) atTop atTop<GOAL>(∀ᵐ (x : 𝕊) ∂μ, ¬addWellApproximable 𝕊 δ x) ∨ ∀ᵐ (x : 𝕊) ∂μ, addWellApproximable 𝕊 δ x
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>δ : ℕ → ℝ<VAR>hδ : Tendsto δ atTop (𝓝 0)<VAR>this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup Irreducible<VAR>μ : Measure 𝕊 := volume<VAR>u : Nat.Primes → 𝕊 := fun p => ↑(↑1 / ↑↑p * T)<VAR>hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p<VAR>hu : Tendsto (addOrderOf ∘ u) atTop atTop<VAR>E : Set 𝕊 := addWellApproximable 𝕊 δ<VAR>X : ℕ → Set 𝕊 := fun n => approxAddOrderOf 𝕊 n (δ n)<VAR>A : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ ¬p ∣ n<VAR>B : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n<VAR>C : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ p ^ 2 ∣ n<GOAL>(∀ᵐ (x : 𝕊) ∂μ, ¬E x) ∨ ∀ᵐ (x : 𝕊) ∂μ, E x