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>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁶ : NormedField 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : Nonempty ι<VAR>inst✝² : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝¹ : SemilatticeSup F<VAR>inst✝ : Nonempty F<VAR>hp : WithSeminorms p<VAR>u : F → E<VAR>y₀ : E<GOAL>Tendsto u atTop (𝓝 y₀) ↔ ∀ (i : ι) (ε : ℝ), 0 < ε → ∃ x₀, ∀ (x : F), x₀ ≤ x → (p i) (u x - y₀) < ε
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁶ : NormedField 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : Nonempty ι<VAR>inst✝² : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝¹ : SemilatticeSup F<VAR>inst✝ : Nonempty F<VAR>hp : WithSeminorms p<VAR>u : F → E<VAR>y₀ : E<GOAL>(∀ (i : ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in atTop, (p i) (u x - y₀) < ε) ↔ ∀ (i : ι) (ε : ℝ), 0 < ε → ∃ x₀, ∀ (x : F), x₀ ≤ x → (p i) (u x - y₀) < ε
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝ : CommSemiring R<VAR>f : ι → R[X]<VAR>t : Multiset R[X]<VAR>h : (Multiset.map leadingCoeff t).prod ≠ 0<GOAL>t.prod.leadingCoeff = (Multiset.map leadingCoeff t).prod
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝ : CommSemiring R<VAR>f : ι → R[X]<VAR>t : Multiset R[X]<VAR>h : (Multiset.map leadingCoeff 0).prod ≠ 0<GOAL>(prod 0).leadingCoeff = (Multiset.map leadingCoeff 0).prod
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝ : CommSemiring R<VAR>f : ι → R[X]<VAR>t✝ : Multiset R[X]<VAR>a : R[X]<VAR>t : Multiset R[X]<VAR>ih : (Multiset.map leadingCoeff t).prod ≠ 0 → t.prod.leadingCoeff = (Multiset.map leadingCoeff t).prod<VAR>h : (Multiset.map leadingCoeff (a ::ₘ t)).prod ≠ 0<GOAL>(a ::ₘ t).prod.leadingCoeff = (Multiset.map leadingCoeff (a ::ₘ t)).prod
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝ : CommSemiring R<VAR>f : ι → R[X]<VAR>t✝ : Multiset R[X]<VAR>a : R[X]<VAR>t : Multiset R[X]<VAR>ih : (Multiset.map leadingCoeff t).prod ≠ 0 → t.prod.leadingCoeff = (Multiset.map leadingCoeff t).prod<VAR>h : a.leadingCoeff * (Multiset.map leadingCoeff t).prod ≠ 0<GOAL>(a * t.prod).leadingCoeff = a.leadingCoeff * (Multiset.map leadingCoeff t).prod
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝ : CommSemiring R<VAR>f : ι → R[X]<VAR>t✝ : Multiset R[X]<VAR>a : R[X]<VAR>t : Multiset R[X]<VAR>ih : (Multiset.map leadingCoeff t).prod ≠ 0 → t.prod.leadingCoeff = (Multiset.map leadingCoeff t).prod<VAR>h : a.leadingCoeff * (Multiset.map leadingCoeff t).prod ≠ 0<GOAL>a.leadingCoeff * t.prod.leadingCoeff = a.leadingCoeff * (Multiset.map leadingCoeff t).prod
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝ : CommSemiring R<VAR>f : ι → R[X]<VAR>t✝ : Multiset R[X]<VAR>a : R[X]<VAR>t : Multiset R[X]<VAR>ih : (Multiset.map leadingCoeff t).prod ≠ 0 → t.prod.leadingCoeff = (Multiset.map leadingCoeff t).prod<VAR>h : a.leadingCoeff * (Multiset.map leadingCoeff t).prod ≠ 0<GOAL>a.leadingCoeff * t.prod.leadingCoeff ≠ 0
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>l : List I<VAR>a : I<VAR>hla : List.Chain' (fun x x_1 => x > x_1) (a :: l)<GOAL>eval C ⟨a :: l, hla⟩ = e C a * eval C ⟨l, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>inst✝² : One M<VAR>inst✝¹ : One N<VAR>inst✝ : One P<VAR>f g : α → M<VAR>x✝ : mulSupport f = mulSupport g ∧ ∀ x ∈ mulSupport f, f x = g x<VAR>h₁ : mulSupport f = mulSupport g<VAR>h₂ : ∀ x ∈ mulSupport f, f x = g x<VAR>x : α<GOAL>f x = g x
<VAR>α : Type u<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : LT α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c d : α<GOAL>a * b⁻¹ < c * d⁻¹ ↔ a * d < c * b
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝² : DecidableEq o<VAR>inst✝¹ : Zero α<VAR>inst✝ : Zero β<VAR>M : (i : o) → Matrix (m' i) (n' i) α<VAR>f : α → β<VAR>hf : f 0 = 0<VAR>i✝ : (i : o) × m' i<VAR>j✝ : (i : o) × n' i<GOAL>(blockDiagonal' M).map f i✝ j✝ = blockDiagonal' (fun k => (M k).map f) i✝ j✝
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝² : DecidableEq o<VAR>inst✝¹ : Zero α<VAR>inst✝ : Zero β<VAR>M : (i : o) → Matrix (m' i) (n' i) α<VAR>f : α → β<VAR>hf : f 0 = 0<VAR>i✝ : (i : o) × m' i<VAR>j✝ : (i : o) × n' i<GOAL>f (if h : i✝.fst = j✝.fst then M i✝.fst i✝.snd (cast ⋯ j✝.snd) else 0) = if h : i✝.fst = j✝.fst then f (M i✝.fst i✝.snd (cast ⋯ j✝.snd)) else 0
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>M : Comon_ C<VAR>inst✝ : BraidedCategory C<VAR>A B : Comon_ C<GOAL>(A ⊗ B).comul = (A.comul ⊗ B.comul) ≫ tensor_μ C (A.X, A.X) (B.X, B.X)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>M : Comon_ C<VAR>inst✝ : BraidedCategory C<VAR>A B : Comon_ C<GOAL>(A.comul ⊗ B.comul) ≫ (tensor_μ Cᵒᵖ (op A.X, op B.X) (op A.X, op B.X)).unop = (A.comul ⊗ B.comul) ≫ tensor_μ C (A.X, A.X) (B.X, B.X)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>M : Comon_ C<VAR>inst✝ : BraidedCategory C<VAR>A B : Comon_ C<GOAL>tensor_μ Cᵒᵖ (op A.X, op B.X) (op A.X, op B.X) = op ((α_ (A.X, A.X).1 (A.X, A.X).2 ((B.X, B.X).1 ⊗ (B.X, B.X).2)).hom ≫ (A.X, A.X).1 ◁ (α_ (A.X, A.X).2 (B.X, B.X).1 (B.X, B.X).2).inv ≫ (A.X, A.X).1 ◁ (β_ (A.X, A.X).2 (B.X, B.X).1).hom ▷ (B.X, B.X).2 ≫ (A.X, A.X).1 ◁ (α_ (B.X, B.X).1 (A.X, A.X).2 (B.X, B.X).2).hom ≫ (α_ (A.X, A.X).1 (B.X, B.X).1 ((A.X, A.X).2 ⊗ (B.X, B.X).2)).inv)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>M : Comon_ C<VAR>inst✝ : BraidedCategory C<VAR>A B : Comon_ C<GOAL>(α_ (op A.X) (op B.X) (op A.X ⊗ op B.X)).hom ≫ op A.X ◁ (α_ (op B.X) (op A.X) (op B.X)).inv ≫ op A.X ◁ (β_ (op B.X) (op A.X)).hom ▷ op B.X ≫ op A.X ◁ (α_ (op A.X) (op B.X) (op B.X)).hom ≫ (α_ (op A.X) (op A.X) (op B.X ⊗ op B.X)).inv = op ((α_ A.X A.X (B.X ⊗ B.X)).hom ≫ A.X ◁ (α_ A.X B.X B.X).inv ≫ A.X ◁ (β_ A.X B.X).hom ▷ B.X ≫ A.X ◁ (α_ B.X A.X B.X).hom ≫ (α_ A.X B.X (A.X ⊗ B.X)).inv)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>M : Comon_ C<VAR>inst✝ : BraidedCategory C<VAR>A B : Comon_ C<GOAL>((α_ (op A.X) (op B.X) (op A.X ⊗ op B.X)).hom ≫ op A.X ◁ (α_ (op B.X) (op A.X) (op B.X)).inv ≫ op A.X ◁ (β_ (op B.X) (op A.X)).hom ▷ op B.X ≫ op A.X ◁ (α_ (op A.X) (op B.X) (op B.X)).hom ≫ (α_ (op A.X) (op A.X) (op B.X ⊗ op B.X)).inv).unop = Quiver.Hom.unop (op ((α_ A.X A.X (B.X ⊗ B.X)).hom ≫ A.X ◁ (α_ A.X B.X B.X).inv ≫ A.X ◁ (β_ A.X B.X).hom ▷ B.X ≫ A.X ◁ (α_ B.X A.X B.X).hom ≫ (α_ A.X B.X (A.X ⊗ B.X)).inv))
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>M : Comon_ C<VAR>inst✝ : BraidedCategory C<VAR>A B : Comon_ C<GOAL>((((α_ A.X A.X (B.X ⊗ B.X)).hom ≫ A.X ◁ (α_ A.X B.X B.X).inv) ≫ A.X ◁ (β_ A.X B.X).hom ▷ B.X) ≫ A.X ◁ (α_ B.X A.X B.X).hom) ≫ (α_ A.X B.X (A.X ⊗ B.X)).inv = (α_ A.X A.X (B.X ⊗ B.X)).hom ≫ A.X ◁ (α_ A.X B.X B.X).inv ≫ A.X ◁ (β_ A.X B.X).hom ▷ B.X ≫ A.X ◁ (α_ B.X A.X B.X).hom ≫ (α_ A.X B.X (A.X ⊗ B.X)).inv
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>x y : α<GOAL>¬Monotone f ∧ ¬Antitone f ↔ ∃ a b c, a < b ∧ b < c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>x y : α<GOAL>(∃ a b c, (a ≤ b ∧ b ≤ c) ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)) ↔ ∃ a b c, (a < b ∧ b < c) ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → R<VAR>hz : P z = Q z<VAR>mem : Q z ∈ nonZeroDivisors R<GOAL>P ≈ Q ↔ P = Q
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → R<VAR>hz : P z = Q z<VAR>mem : Q z ∈ nonZeroDivisors R<GOAL>P ≈ Q → P = Q
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>Q : Fin 3 → R<VAR>mem : Q z ∈ nonZeroDivisors R<VAR>u : Rˣ<VAR>hz : (fun m => m • Q) u z = Q z<GOAL>(fun m => m • Q) u = Q
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>Q : Fin 3 → R<VAR>mem : Q z ∈ nonZeroDivisors R<VAR>u : Rˣ<VAR>hz : (fun m => m • Q) u z = 1 * Q z<GOAL>(fun m => m • Q) u = Q
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : SemilatticeSup α<VAR>s t : Set α<VAR>a : α<GOAL>a ∈ ↑(upperClosure (s ⊻ t)) ↔ a ∈ ↑(upperClosure s ⊔ upperClosure t)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : SemilatticeSup α<VAR>s t : Set α<VAR>a : α<GOAL>(∃ a_1, (∃ a ∈ s, ∃ b ∈ t, a ⊔ b = a_1) ∧ a_1 ≤ a) ↔ (∃ a_1 ∈ s, a_1 ≤ a) ∧ ∃ a_1 ∈ t, a_1 ≤ a
<VAR>ι : Type u_1<VAR>I J : Box ι<VAR>π π₁ π₂ : TaggedPrepartition I<VAR>x✝ : ι → ℝ<VAR>inst✝ : Fintype ι<VAR>h : π.IsHenstock<VAR>x : ι → ℝ<GOAL>(Finset.filter (fun J => π.tag J = x) π.boxes).card ≤ (Finset.filter (fun J => x ∈ Box.Icc J) π.boxes).card
<VAR>ι : Type u_1<VAR>I J✝ : Box ι<VAR>π π₁ π₂ : TaggedPrepartition I<VAR>x✝ : ι → ℝ<VAR>inst✝ : Fintype ι<VAR>h : π.IsHenstock<VAR>x : ι → ℝ<VAR>J : Box ι<VAR>hJ : J ∈ Finset.filter (fun J => π.tag J = x) π.boxes<GOAL>J ∈ Finset.filter (fun J => x ∈ Box.Icc J) π.boxes
<VAR>ι : Type u_1<VAR>I J✝ : Box ι<VAR>π π₁ π₂ : TaggedPrepartition I<VAR>x✝ : ι → ℝ<VAR>inst✝ : Fintype ι<VAR>h : π.IsHenstock<VAR>x : ι → ℝ<VAR>J : Box ι<VAR>hJ : J ∈ π.boxes ∧ π.tag J = x<GOAL>J ∈ π.boxes ∧ x ∈ Box.Icc J
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁷ : DecidableEq α'<VAR>inst✝⁶ : DecidableEq β'<VAR>inst✝⁵ : DecidableEq γ<VAR>inst✝⁴ : DecidableEq γ'<VAR>inst✝³ : DecidableEq δ<VAR>inst✝² : DecidableEq δ'<VAR>inst✝¹ : DecidableEq ε<VAR>inst✝ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<GOAL>image₂ f s t ⊆ u ↔ ∀ a ∈ s, image (fun b => f a b) t ⊆ u
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>inst✝⁵ : MeasurableSpace E<VAR>inst✝⁴ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : Nontrivial E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : ℝ → F<GOAL>∫ (x : E), f ‖x‖ ∂μ = ∫ (x : ↑{0}ᶜ), f ‖↑x‖ ∂Measure.comap Subtype.val μ
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>inst✝⁵ : MeasurableSpace E<VAR>inst✝⁴ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : Nontrivial E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : ℝ → F<GOAL>((μ.toSphere univ).toReal • ∫ (x : ↑(Ioi 0)), f ↑x ∂(Measure.comap Subtype.val volume).withDensity fun r => ↑(↑r ^ (dim E - 1)).toNNReal) = dim E • (μ (ball 0 1)).toReal • ∫ (y : ℝ) in Ioi 0, y ^ (dim E - 1) • f y
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>inst✝⁵ : MeasurableSpace E<VAR>inst✝⁴ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : Nontrivial E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : ℝ → F<VAR>x : ℝ<VAR>hx : x ∈ Ioi 0<GOAL>(x ^ (dim E - 1)).toNNReal • f x = x ^ (dim E - 1) • f x
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>inst✝⁵ : MeasurableSpace E<VAR>inst✝⁴ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : Nontrivial E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : ℝ → F<GOAL>Measurable fun r => (↑r ^ (dim E - 1)).toNNReal
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>s1 : WSeq α<VAR>s2 : WSeq β<VAR>h✝ : LiftRel R s1 s2<VAR>s : WSeq β<VAR>t : WSeq α<VAR>h : LiftRel R t s<GOAL>Computation.LiftRel (LiftRelO (swap R) (swap (LiftRel R))) s.destruct t.destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>s1 : WSeq α<VAR>s2 : WSeq β<VAR>h✝ : LiftRel R s1 s2<VAR>s : WSeq β<VAR>t : WSeq α<VAR>h : LiftRel R t s<GOAL>Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct s.destruct
<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✝⁵ : AddCommMonoid α<VAR>inst✝⁴ : Mul α<VAR>inst✝³ : Fintype n<VAR>inst✝² : Monoid R<VAR>inst✝¹ : DistribMulAction R α<VAR>inst✝ : IsScalarTower R α α<VAR>a : R<VAR>M : Matrix m n α<VAR>N : Matrix n l α<VAR>i✝ : m<VAR>j✝ : l<GOAL>(a • M * N) i✝ j✝ = (a • (M * N)) i✝ j✝
<VAR>R : Type u_1<VAR>n : ℕ<GOAL>(σ 1) n = ∑ d ∈ n.divisors, d
<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✝⁴ : MeasurableSpace E<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>q : ℝ<VAR>p : ℝ≥0∞<VAR>inst✝¹ : BorelSpace E<VAR>f : β → E<VAR>hp_ne_top : p ≠ ⊤<VAR>μ : Measure β<VAR>fmeas : Measurable f<VAR>inst✝ : SeparableSpace ↑(Set.range f ∪ {0})<VAR>hf : eLpNorm f p μ < ⊤<GOAL>Tendsto (fun n => eLpNorm (↑(approxOn f fmeas (Set.range f ∪ {0}) 0 ⋯ n) - f) p μ) atTop (𝓝 0)
<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✝⁴ : MeasurableSpace E<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>q : ℝ<VAR>p : ℝ≥0∞<VAR>inst✝¹ : BorelSpace E<VAR>f : β → E<VAR>hp_ne_top : p ≠ ⊤<VAR>μ : Measure β<VAR>fmeas : Measurable f<VAR>inst✝ : SeparableSpace ↑(Set.range f ∪ {0})<VAR>hf : eLpNorm f p μ < ⊤<GOAL>∀ᵐ (x : β) ∂μ, f x ∈ closure (Set.range f ∪ {0})
<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✝⁴ : MeasurableSpace E<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>q : ℝ<VAR>p : ℝ≥0∞<VAR>inst✝¹ : BorelSpace E<VAR>f : β → E<VAR>hp_ne_top : p ≠ ⊤<VAR>μ : Measure β<VAR>fmeas : Measurable f<VAR>inst✝ : SeparableSpace ↑(Set.range f ∪ {0})<VAR>hf : eLpNorm f p μ < ⊤<GOAL>eLpNorm (fun x => f x - 0) p μ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>ι : Type u_5<VAR>m : MeasurableSpace α<VAR>f : α → β<VAR>μ : ι → Measure α<VAR>s : Finset ι<GOAL>Integrable f (∑ i ∈ s, μ i) ↔ ∀ i ∈ s, Integrable f (μ i)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℤ<GOAL>(W.ΨSq n).coeff (n.natAbs ^ 2 - 1) = ↑n ^ 2
<VAR>α : Type u_1<VAR>x✝ y z : ℝ<VAR>l : Filter α<VAR>n : ℕ<VAR>x : ℝ<GOAL>((fun r => r⁻¹) ∘ fun x => rexp x / x ^ n) x = x ^ n * rexp (-x)
<VAR>K : Type u_1<VAR>inst✝ : DivisionSemiring K<VAR>q : ℚ≥0<VAR>n : ℕ<GOAL>↑(q ^ n) = ↑q ^ n
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionRing α<VAR>p q : ℚ<VAR>n : ℤ<GOAL>↑n / ↑1 = ↑n
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>m✝ m : OuterMeasure α<VAR>s : Set α<GOAL>∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = m.trim s
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>m✝ m : OuterMeasure α<VAR>s : Set α<GOAL>∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℤ<VAR>r : R<GOAL>trunc (C r * T n) = if 0 ≤ n then (monomial n.toNat) r else 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℤ<VAR>r : R<GOAL>(toFinsuppIso R) (trunc (C r * T n)) = (toFinsuppIso R) (if 0 ≤ n then (monomial n.toNat) r else 0)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℤ<VAR>r : R<GOAL>(toFinsuppIso R) ((toFinsuppIso R).symm.toAddMonoidHom ((comapDomain.addMonoidHom ⋯) (Finsupp.single n r))) = (toFinsuppIso R) (if 0 ≤ n then (monomial n.toNat) r else 0)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℤ<VAR>r : R<GOAL>comapDomain Int.ofNat (Finsupp.single n r) ⋯ = (toFinsuppIso R) (if 0 ≤ n then (monomial n.toNat) r else 0)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℤ<VAR>r : R<GOAL>comapDomain Int.ofNat (Finsupp.single n r) ⋯ = (if 0 ≤ n then (monomial n.toNat) r else 0).toFinsupp
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : Zero M<VAR>a a' : α<VAR>b : M<VAR>inst✝ : Decidable (a = a')<GOAL>(single a b) a' = if a = a' then b else 0
<VAR>s : Finset ℕ<VAR>N : ℕ<VAR>hN : ¬Prime N<VAR>m : ℕ<GOAL>m ∈ factoredNumbers (insert N s) ↔ m ∈ factoredNumbers s
<VAR>s : Finset ℕ<VAR>N : ℕ<VAR>hN : ¬Prime N<VAR>m : ℕ<VAR>hm : m ∈ factoredNumbers (insert N s)<VAR>p : ℕ<VAR>hp : p ∈ m.primeFactorsList<GOAL>p ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>S : Set (UpperSet α)<VAR>s t : UpperSet α<VAR>a : α<VAR>f : (i : ι) → κ i → UpperSet α<GOAL>↑(⨅ i, ⨅ j, f i j) = ⋃ i, ⋃ j, ↑(f i j)
<VAR>M : Type u<VAR>G : Type v<VAR>X : Type w<VAR>inst✝⁵ : PseudoMetricSpace X<VAR>inst✝⁴ : Group G<VAR>inst✝³ : MulAction G X<VAR>inst✝² : IsometricSMul G X<VAR>inst✝¹ : PseudoMetricSpace G<VAR>inst✝ : IsometricSMul Gᵐᵒᵖ G<VAR>a b : G<VAR>r : ℝ<GOAL>(fun x => x * a) ⁻¹' ball b r = ball (b / a) r
<VAR>M : Type u<VAR>G : Type v<VAR>X : Type w<VAR>inst✝⁵ : PseudoMetricSpace X<VAR>inst✝⁴ : Group G<VAR>inst✝³ : MulAction G X<VAR>inst✝² : IsometricSMul G X<VAR>inst✝¹ : PseudoMetricSpace G<VAR>inst✝ : IsometricSMul Gᵐᵒᵖ G<VAR>a b : G<VAR>r : ℝ<GOAL>(fun x => x * a) ⁻¹' ball b r = ball (b * a⁻¹) r
<VAR>B : Type u<VAR>inst✝ : Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<GOAL>f ◁ eqToHom ⋯ = eqToHom ⋯
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>h : p = C (p.coeff 0)<GOAL>p.natDegree = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<GOAL>Continuous (uncurry inner)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>inner' : E →+ E →+ 𝕜 := { toFun := fun x => ((innerₛₗ 𝕜) x).toAddMonoidHom, map_zero' := ⋯, map_add' := ⋯ }<GOAL>Continuous (uncurry inner)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>inner' : E →+ E →+ 𝕜 := { toFun := fun x => ((innerₛₗ 𝕜) x).toAddMonoidHom, map_zero' := ⋯, map_add' := ⋯ }<VAR>this : Continuous fun p => (inner' p.1) p.2<GOAL>Continuous (uncurry inner)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>inner' : E →+ E →+ 𝕜 := { toFun := fun x => ((innerₛₗ 𝕜) x).toAddMonoidHom, map_zero' := ⋯, map_add' := ⋯ }<VAR>this : Continuous fun p => (inner' p.1) p.2<GOAL>Continuous (⋯.extend (uncurry inner))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>inner' : E →+ E →+ 𝕜 := { toFun := fun x => ((innerₛₗ 𝕜) x).toAddMonoidHom, map_zero' := ⋯, map_add' := ⋯ }<VAR>this : Continuous fun p => (inner' p.1) p.2<GOAL>Continuous (⋯.extend fun p => (inner' p.1) p.2)
<VAR>θ : ℂ<GOAL>tan θ = 0 ↔ ∃ k, ↑k * ↑π / 2 = θ
<VAR>θ : ℂ<GOAL>(∃ k, 2 * θ = ↑k * ↑π) ↔ ∃ k, ↑k * ↑π / 2 = θ
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Computation α<VAR>f : α → Computation β<VAR>a : α<VAR>b : β<VAR>h1 : s ~> a<VAR>h2 : f a ~> b<VAR>b' : β<VAR>bB : b' ∈ s.bind f<GOAL>b = b'
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Computation α<VAR>f : α → Computation β<VAR>a : α<VAR>b : β<VAR>h1 : s ~> a<VAR>h2 : f a ~> b<VAR>b' : β<VAR>bB : b' ∈ s.bind f<VAR>a' : α<VAR>a's : a' ∈ s<VAR>ba' : b' ∈ f a'<GOAL>b = b'
<VAR>α : Type u_1<VAR>s✝ t✝ : Set α<VAR>a : α<VAR>inst✝¹ : Mul α<VAR>inst✝ : StarMul α<VAR>s t : Set α<GOAL>(s * t)⋆ = t⋆ * s⋆
<VAR>α : Type u_1<VAR>s t : Set α<GOAL>val ⁻¹' (s ∩ t) = val ⁻¹' t
<VAR>R : Type u_1<VAR>inst✝³ : NonAssocRing R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : BinomialRing R<VAR>inst✝ : NatPowAssoc R<VAR>n k : ℕ<GOAL>(ascPochhammer ℕ k).smeval ↑n = ↑((ascPochhammer ℕ k).smeval n)
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α β : TypeVec.{u} n<VAR>g : α ::: P.M α ⟹ β ::: P.M β<VAR>x : P.M α<VAR>h : ∀ (x : P.M α), lastFun g x = dropFun g <$$> x<GOAL>g <$$> dest P x = dest P (dropFun g <$$> x)
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α β : TypeVec.{u} n<VAR>g : α ::: P.M α ⟹ β ::: P.M β<VAR>x : P.M α<VAR>h : ∀ (x : P.M α), lastFun g x = dropFun g <$$> x<GOAL>g <$$> dest P x = (dropFun g ::: fun x => dropFun g <$$> x) <$$> dest P x
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α β : TypeVec.{u} n<VAR>g : α ::: P.M α ⟹ β ::: P.M β<VAR>x : P.M α<VAR>h : ∀ (x : P.M α), lastFun g x = dropFun g <$$> x<GOAL>g = (dropFun g ::: fun x => dropFun g <$$> x)
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α β : TypeVec.{u} n<VAR>g : α ::: P.M α ⟹ β ::: P.M β<VAR>x : P.M α<VAR>h : ∀ (x : P.M α), lastFun g x = dropFun g <$$> x<GOAL>lastFun g = fun x => dropFun g <$$> x
<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>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x✝¹ : E<VAR>s t : Set E<VAR>L✝ L₁ L₂ : Filter E<VAR>c : F<VAR>x : E<VAR>L : Filter E<VAR>x✝ : E<GOAL>0 = c - c - 0 (x✝ - x)
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>X : Type u_5<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<GOAL>IsNowhereDense s ↔ interior s = ∅
<VAR>x✝ y x : ℝ<GOAL>arccos x = π ↔ x ≤ -1
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>X₀ X₁ X₂ : V<VAR>d₀ : X₁ ⟶ X₀<VAR>d₁ : X₂ ⟶ X₁<VAR>s : d₁ ≫ d₀ = 0<VAR>succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0<GOAL>(if 1 = 0 + 1 then 𝟙 X₁ ≫ d₀ else 0) = d₀
<VAR>X Y : TopCat<VAR>f g : C(↑X, ↑Y)<VAR>H : f.Homotopy g<VAR>x₀ x₁ : ↑X<VAR>p : fromTop x₀ ⟶ fromTop x₁<VAR>p' : Path (fromTop x₀).as (fromTop x₁).as<GOAL>(π.map f).map ⟦p'⟧ = hcast ⋯ ≫ (π.map H.uliftMap).map (prodToProdTopI (𝟙 (fromTop { down := 0 })) ⟦p'⟧) ≫ hcast ⋯