ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>R R₁ R₂ : ℝ<VAR>f : ℂ → E<VAR>c z✝ z₀ : ℂ<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : StrictConvexSpace ℝ E<VAR>hd : DifferentiableOn ℂ f (ball c R₁)<VAR>h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)<VAR>h_z₀ : z₀ ∈ ball c R₁<VAR>g : ℂ → E := dslope f c<VAR>h_eq : ‖g z₀‖ = R₂ / R₁<VAR>z : ℂ<VAR>hz : z ∈ ball c R₁<VAR>h : ¬z = c<VAR>h_R₁ : 0 < R₁<VAR>g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁<VAR>g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀<GOAL>f z = (fun z => f c + (z - c) • g z₀) z
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>R R₁ R₂ : ℝ<VAR>f : ℂ → E<VAR>c z✝ z₀ : ℂ<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : StrictConvexSpace ℝ E<VAR>hd : DifferentiableOn ℂ f (ball c R₁)<VAR>h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)<VAR>h_z₀ : z₀ ∈ ball c R₁<VAR>g : ℂ → E := dslope f c<VAR>h_eq : ‖g z₀‖ = R₂ / R₁<VAR>z : ℂ<VAR>hz : z ∈ ball c R₁<VAR>h : ¬z = c<VAR>h_R₁ : 0 < R₁<VAR>g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁<VAR>g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀<VAR>g_diff : DifferentiableOn ℂ g (ball c R₁)<GOAL>f z = (fun z => f c + (z - c) • g z₀) z
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>R R₁ R₂ : ℝ<VAR>f : ℂ → E<VAR>c z✝ z₀ : ℂ<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : StrictConvexSpace ℝ E<VAR>hd : DifferentiableOn ℂ f (ball c R₁)<VAR>h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)<VAR>h_z₀ : z₀ ∈ ball c R₁<VAR>g : ℂ → E := dslope f c<VAR>h_eq : ‖g z₀‖ = R₂ / R₁<VAR>z : ℂ<VAR>hz : z ∈ ball c R₁<VAR>h : ¬z = c<VAR>h_R₁ : 0 < R₁<VAR>g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁<VAR>g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀<VAR>g_diff : DifferentiableOn ℂ g (ball c R₁)<VAR>this : g z = g z₀<GOAL>f z = (fun z => f c + (z - c) • g z₀) z
<VAR>α : Type u_1<VAR>f : SignType → α<GOAL>Set.range f = {f zero, f neg, f pos}
<VAR>α : Type u_1<VAR>f : SignType → α<GOAL>↑(Finset.image f {0, -1, 1}) = {f zero, f neg, f pos}
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>p q : R[X]<GOAL>p.mirror.leadingCoeff = p.trailingCoeff
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>L : List (List α)<VAR>i : ℕ<GOAL>take (take i (map length L)).sum L.join = (take i L).join
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>a b : α<GOAL>some ⁻¹' Ioi ⊥ = univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : SuccOrder α<VAR>a b : α<VAR>ha : ¬IsMax a<GOAL>Ico (succ a) b = Ioo a b
<VAR>r : ℝ<VAR>z : ℂ<VAR>hz : ↑r ≤ z<GOAL>z = ↑z.re
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Preorder α<VAR>inst✝³ : AddCommSemigroup α<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>a b c d : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>a + c - (b + c) ≤ a - b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Preorder α<VAR>inst✝³ : AddCommSemigroup α<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>a b c d : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>a + c ≤ b + (a - b) + c
<VAR>n p : ℕ<VAR>h : n ≤ p<GOAL>↑((p - 1).descFactorial n) = (-1) ^ n * ↑n !
<VAR>n p : ℕ<VAR>h : n ≤ p<GOAL>↑(∏ i ∈ range n, (p - 1 - i)) = (-1) ^ n * ↑(∏ x ∈ range n, (x + 1))
<VAR>n p : ℕ<VAR>h : n ≤ p<GOAL>∏ i ∈ range n, ↑(p - 1 - i) = (-1) ^ n * ∏ i ∈ range n, ↑(i + 1)
<VAR>n p : ℕ<VAR>h : n ≤ p<GOAL>∏ i ∈ range n, ↑(p - 1 - i) = (-1) ^ (range n).card * ∏ i ∈ range n, ↑(i + 1)
<VAR>n p : ℕ<VAR>h : n ≤ p<GOAL>∏ i ∈ range n, ↑(p - 1 - i) = ∏ a ∈ range n, -1 * ↑(a + 1)
<VAR>n p : ℕ<VAR>h : n ≤ p<GOAL>∀ x ∈ range n, ↑(p - 1 - x) = -1 * ↑(x + 1)
<VAR>n p : ℕ<VAR>h : n ≤ p<VAR>x : ℕ<VAR>hx : x ∈ range n<GOAL>↑(p - 1 - x) = -1 * ↑(x + 1)
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z✝ X Y Z : TopCat<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(pullback f g).topologicalSpace_coe = induced (⇑(prod.lift (pullback.fst f g) (pullback.snd f g))) (X ⨯ Y).topologicalSpace_coe
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>n : ℕ<GOAL>(QInfty ≫ QInfty).f n = QInfty.f n
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>inst✝ : Nontrivial α<VAR>a b : FactorSet α<GOAL>a.prod ≤ b.prod ↔ a ≤ b
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>inst✝ : Nontrivial α<VAR>a b : FactorSet α<VAR>h : a.prod ≤ b.prod<GOAL>a ≤ b
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>inst✝ : Nontrivial α<VAR>a b : FactorSet α<VAR>h : a.prod ≤ b.prod<VAR>this : a.prod.factors ≤ b.prod.factors<GOAL>a ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>μa : Measure α<VAR>μb : Measure β<VAR>μc : Measure γ<VAR>μd : Measure δ<VAR>g : β → γ<VAR>f : α → β<VAR>hg : MeasurePreserving g μb μc<VAR>hf : MeasurePreserving f μa μb<GOAL>map (g ∘ f) μa = μc
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a<GOAL>∀ (a : Args), ArgsRel a (Args.P24 x₂ x₁ y) → P124 a
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>ih' : ∀ (a : Args), TransGen (CutExpand IsOption) (match a with | Args.P1 x y => {y, x} | Args.P24 x₁ x₂ y => {x₁, y, x₂}) {x₁, y, x₂} → P124 a<GOAL>∀ (a : Args), TransGen (CutExpand IsOption) (match a with | Args.P1 x y => {y, x} | Args.P24 x₁ x₂ y => {x₁, y, x₂}) {x₂, y, x₁} → P124 a
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>ih' : ∀ (a : Args), TransGen (CutExpand IsOption) (match a with | Args.P1 x y => {y, x} | Args.P24 x₁ x₂ y => {x₁, y, x₂}) {x₁, y, x₂} → P124 a<GOAL>{x₁, y, x₂} = {x₂, y, x₁}
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>ih' : ∀ (a : Args), TransGen (CutExpand IsOption) (match a with | Args.P1 x y => {y} + {x} | Args.P24 x₁ x₂ y => {x₁} + ({y} + {x₂})) ({x₁} + ({y} + {x₂})) → P124 a<GOAL>{x₁} + ({y} + {x₂}) = {x₂} + ({y} + {x₁})
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : Fintype ι<VAR>v : ι → E<VAR>inst✝ : Fintype ι'<VAR>b : OrthonormalBasis ι 𝕜 E<VAR>e : ι ≃ ι'<VAR>i' : ι'<GOAL>(b.reindex e) i' = b (e.symm i')
<VAR>R : Type u<VAR>inst✝ : EuclideanDomain R<VAR>m k : R<GOAL>m % k + m / k * k = m
<VAR>R : Type u<VAR>inst✝ : EuclideanDomain R<VAR>m k : R<GOAL>m % k + k * (m / k) = m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>f : α → β<VAR>inst✝ : IsEmpty ι<VAR>μ : ι → Measure α<GOAL>sum μ = 0
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c✝ d✝ : ℝ<VAR>f : ℝ → E<VAR>c d : ℝ<GOAL>c • ∫ (x : ℝ) in a..b, f (c * x - d) = ∫ (x : ℝ) in c * a - d..c * b - d, f x
<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>t : L.Term α<GOAL>(fun l => (do let a ← (listDecode l).head? pure (some a)).join) t.listEncode = some t
<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>t : L.Term α<VAR>h : listDecode ([t].bind listEncode) = [t]<GOAL>(fun l => (do let a ← (listDecode l).head? pure (some a)).join) t.listEncode = some t
<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>t : L.Term α<VAR>h : listDecode t.listEncode = [t]<GOAL>(fun l => (do let a ← (listDecode l).head? pure (some a)).join) t.listEncode = some t
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n : ℕ<VAR>ha : 0 ≤ a<GOAL>⌊a + 1⌋₊ = ⌊a⌋₊ + 1
<VAR>k✝ : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹² : CommSemiring k✝<VAR>inst✝¹¹ : Monoid G<VAR>inst✝¹⁰ : Monoid H<VAR>A✝ : Type u₃<VAR>inst✝⁹ : Semiring A✝<VAR>inst✝⁸ : Algebra k✝ A✝<VAR>B : Type u_3<VAR>inst✝⁷ : Semiring B<VAR>inst✝⁶ : Algebra k✝ B<VAR>k : Type u_4<VAR>A : Type u_5<VAR>G₁ : Type u_6<VAR>G₂ : Type u_7<VAR>G₃ : Type u_8<VAR>inst✝⁵ : CommSemiring k<VAR>inst✝⁴ : Semiring A<VAR>inst✝³ : Algebra k A<VAR>inst✝² : Monoid G₁<VAR>inst✝¹ : Monoid G₂<VAR>inst✝ : Monoid G₃<VAR>f : G₁ →* G₂<VAR>g : G₂ →* G₃<VAR>x✝ : MonoidAlgebra A G₁<GOAL>(mapDomainAlgHom k A (g.comp f)) x✝ = ((mapDomainAlgHom k A g).comp (mapDomainAlgHom k A f)) x✝
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>x : A[X]<GOAL>(toFunAlgHom R A) (invFun R A x) = x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>x : A[X]<GOAL>∀ (p q : A[X]), (toFunAlgHom R A) (invFun R A p) = p → (toFunAlgHom R A) (invFun R A q) = q → (toFunAlgHom R A) (invFun R A (p + q)) = p + q
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>x : A[X]<GOAL>∀ (n : ℕ) (a : A), (toFunAlgHom R A) (invFun R A ((monomial n) a)) = (monomial n) a
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : CommRing α<VAR>A✝ B A : Matrix n n α<VAR>inst✝ : Invertible A<VAR>u v : n → α<VAR>hM : u = A *ᵥ v<GOAL>A⁻¹ *ᵥ u = v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι✝ → Sort u_7<VAR>κ₁ : ι✝ → Sort u_8<VAR>κ₂ : ι✝ → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s t u : Set α<VAR>f : α → β<VAR>ι : Type u_11<VAR>Es : ι → Set α<VAR>Es_union : ⋃ i, Es i = univ<VAR>Es_disj : Pairwise fun i j => Disjoint (Es i) (Es j)<VAR>I : Set ι<VAR>x : α<GOAL>x ∈ (⋃ i ∈ I, Es i)ᶜ ↔ x ∈ ⋃ i ∈ Iᶜ, Es i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι✝ → Sort u_7<VAR>κ₁ : ι✝ → Sort u_8<VAR>κ₂ : ι✝ → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s t u : Set α<VAR>f : α → β<VAR>ι : Type u_11<VAR>Es : ι → Set α<VAR>Es_union : ⋃ i, Es i = univ<VAR>Es_disj : Pairwise fun i j => Disjoint (Es i) (Es j)<VAR>I : Set ι<VAR>x : α<VAR>i : ι<VAR>hix : x ∈ Es i<GOAL>x ∈ (⋃ i ∈ I, Es i)ᶜ ↔ x ∈ ⋃ i ∈ Iᶜ, Es i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι✝ → Sort u_7<VAR>κ₁ : ι✝ → Sort u_8<VAR>κ₂ : ι✝ → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s t u : Set α<VAR>f : α → β<VAR>ι : Type u_11<VAR>Es : ι → Set α<VAR>Es_union : ⋃ i, Es i = univ<VAR>Es_disj : Pairwise fun i j => Disjoint (Es i) (Es j)<VAR>I : Set ι<VAR>x : α<VAR>i : ι<VAR>hix : x ∈ Es i<VAR>obs : ∀ (J : Set ι), x ∈ ⋃ j ∈ J, Es j ↔ i ∈ J<GOAL>x ∈ (⋃ i ∈ I, Es i)ᶜ ↔ x ∈ ⋃ i ∈ Iᶜ, Es i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι✝ → Sort u_7<VAR>κ₁ : ι✝ → Sort u_8<VAR>κ₂ : ι✝ → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s t u : Set α<VAR>f : α → β<VAR>ι : Type u_11<VAR>Es : ι → Set α<VAR>Es_union : ⋃ i, Es i = univ<VAR>Es_disj : Pairwise fun i j => Disjoint (Es i) (Es j)<VAR>I : Set ι<VAR>x : α<VAR>i : ι<VAR>hix : x ∈ Es i<VAR>obs : ∀ (J : Set ι), x ∈ ⋃ j ∈ J, Es j ↔ i ∈ J<VAR>obs' : ∀ (J : Set ι), x ∈ (⋃ j ∈ J, Es j)ᶜ ↔ i ∉ J<GOAL>x ∈ (⋃ i ∈ I, Es i)ᶜ ↔ x ∈ ⋃ i ∈ Iᶜ, Es i
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : NormedAddCommGroup E''<VAR>inst✝¹² : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x✝ x' : G<VAR>y y' : E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : AddGroup G<VAR>inst✝³ : MeasurableAdd₂ G<VAR>inst✝² : MeasurableNeg G<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : μ.IsAddRightInvariant<VAR>h1 : f =ᶠ[ae μ] f'<VAR>h2 : g =ᶠ[ae μ] g'<VAR>x : G<GOAL>(f ⋆[L, μ] g) x = (f' ⋆[L, μ] g') x
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : NormedAddCommGroup E''<VAR>inst✝¹² : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x✝ x' : G<VAR>y y' : E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : AddGroup G<VAR>inst✝³ : MeasurableAdd₂ G<VAR>inst✝² : MeasurableNeg G<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : μ.IsAddRightInvariant<VAR>h1 : f =ᶠ[ae μ] f'<VAR>h2 : g =ᶠ[ae μ] g'<VAR>x : G<GOAL>(fun a => (L (f a)) (g (x - a))) =ᶠ[ae μ] fun a => (L (f' a)) (g' (x - a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ζ : Type u_6<GOAL>@iterate = @iterateTR
<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>f : α → α<VAR>a : α<VAR>n : ℕ<GOAL>iterate f a n = iterateTR f a n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : CompactSpace α<VAR>f : α → β<VAR>h : Continuous f<GOAL>map (Prod.map f f) (𝓤 α) = map (Prod.map f f) (𝓝ˢ (diagonal α))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Hashable α<VAR>data : Buckets α β<VAR>a : α<VAR>b : β<GOAL>(reinsertAux data a b).size = data.size.succ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Hashable α<VAR>data : Buckets α β<VAR>a : α<VAR>b : β<GOAL>Nat.sum (List.map (fun x => x.toList.length) (data.update (mkIdx ⋯ (hash a).toUSize).val (AssocList.cons a b data.val[(mkIdx ⋯ (hash a).toUSize).val.toNat]) ⋯).val.data) = Nat.sum (List.map (fun x => x.toList.length) data.val.data) + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Hashable α<VAR>data : Buckets α β<VAR>a : α<VAR>b : β<VAR>l₁ l₂ : List (AssocList α β)<VAR>h₁ : data.val.data = l₁ ++ data.val[(mkIdx ⋯ (hash a).toUSize).val] :: l₂<VAR>left✝ : l₁.length = (mkIdx ⋯ (hash a).toUSize).val.toNat<VAR>eq : (data.update (mkIdx ⋯ (hash a).toUSize).val (AssocList.cons a b data.val[(mkIdx ⋯ (hash a).toUSize).val.toNat]) ⋯).val.data = l₁ ++ AssocList.cons a b data.val[(mkIdx ⋯ (hash a).toUSize).val.toNat] :: l₂<GOAL>Nat.sum (List.map (fun x => x.toList.length) (l₁ ++ AssocList.cons a b data.val[(mkIdx ⋯ (hash a).toUSize).val.toNat] :: l₂)) = Nat.sum (List.map (fun x => x.toList.length) data.val.data) + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Hashable α<VAR>data : Buckets α β<VAR>a : α<VAR>b : β<VAR>l₁ l₂ : List (AssocList α β)<VAR>h₁ : data.val.data = l₁ ++ data.val[(mkIdx ⋯ (hash a).toUSize).val] :: l₂<VAR>left✝ : l₁.length = (mkIdx ⋯ (hash a).toUSize).val.toNat<VAR>eq : (data.update (mkIdx ⋯ (hash a).toUSize).val (AssocList.cons a b data.val[(mkIdx ⋯ (hash a).toUSize).val.toNat]) ⋯).val.data = l₁ ++ AssocList.cons a b data.val[(mkIdx ⋯ (hash a).toUSize).val.toNat] :: l₂<GOAL>Nat.sum (List.map (fun x => x.toList.length) l₁) + (data.val[(mkIdx ⋯ (hash a).toUSize).val.toNat].toList.length + Nat.sum (List.map (fun x => x.toList.length) l₂) + 1) = Nat.sum (List.map (fun x => x.toList.length) l₁) + (data.val[(mkIdx ⋯ (hash a).toUSize).val.toNat].toList.length + Nat.sum (List.map (fun x => x.toList.length) l₂)) + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t u : Set α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>e : α ≃ᵐ β<VAR>s : Set β<VAR>h : MeasurableSet (⇑e ⁻¹' s)<GOAL>MeasurableSet s
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : SetLike S A<VAR>hSA : NonUnitalSubringClass S A<VAR>hSRA : SMulMemClass S R A<VAR>s : S<VAR>h : ∀ (r : R), r ≠ 0 → (algebraMap R A) r ∉ s<VAR>inst✝¹ : FunLike F (Unitization R ↥s) A<VAR>inst✝ : AlgHomClass F R (Unitization R ↥s) A<VAR>f : F<VAR>hf : ∀ (x : ↥s), f ↑x = ↑x<GOAL>Function.Injective ⇑f
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : SetLike S A<VAR>hSA : NonUnitalSubringClass S A<VAR>hSRA : SMulMemClass S R A<VAR>s : S<VAR>h : ∀ (r : R), r ≠ 0 → (algebraMap R A) r ∉ s<VAR>inst✝¹ : FunLike F (Unitization R ↥s) A<VAR>inst✝ : AlgHomClass F R (Unitization R ↥s) A<VAR>f : F<VAR>hf : ∀ (x : ↥s), f ↑x = ↑x<VAR>x : Unitization R ↥s<VAR>hx : f x = 0<GOAL>x = 0
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : SetLike S A<VAR>hSA : NonUnitalSubringClass S A<VAR>hSRA : SMulMemClass S R A<VAR>s : S<VAR>h : ∀ (r : R), r ≠ 0 → (algebraMap R A) r ∉ s<VAR>inst✝¹ : FunLike F (Unitization R ↥s) A<VAR>inst✝ : AlgHomClass F R (Unitization R ↥s) A<VAR>f : F<VAR>hf : ∀ (x : ↥s), f ↑x = ↑x<VAR>r : R<VAR>a : ↥s<VAR>hx : f (Unitization.inl r + ↑a) = 0<GOAL>Unitization.inl r + ↑a = 0
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : SetLike S A<VAR>hSA : NonUnitalSubringClass S A<VAR>hSRA : SMulMemClass S R A<VAR>s : S<VAR>h : ∀ (r : R), r ≠ 0 → (algebraMap R A) r ∉ s<VAR>inst✝¹ : FunLike F (Unitization R ↥s) A<VAR>inst✝ : AlgHomClass F R (Unitization R ↥s) A<VAR>f : F<VAR>hf : ∀ (x : ↥s), f ↑x = ↑x<VAR>r : R<VAR>a : ↥s<VAR>hx : (algebraMap R A) r + ↑a = 0<GOAL>Unitization.inl r + ↑a = 0
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : SetLike S A<VAR>hSA : NonUnitalSubringClass S A<VAR>hSRA : SMulMemClass S R A<VAR>s : S<VAR>h : ∀ (r : R), r ≠ 0 → (algebraMap R A) r ∉ s<VAR>inst✝¹ : FunLike F (Unitization R ↥s) A<VAR>inst✝ : AlgHomClass F R (Unitization R ↥s) A<VAR>f : F<VAR>hf : ∀ (x : ↥s), f ↑x = ↑x<VAR>r : R<VAR>a : ↥s<VAR>hx : (algebraMap R A) r = -↑a<GOAL>Unitization.inl r = -↑a
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : CommSemiring A'<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R B<VAR>p✝ q : R[X]<VAR>x : A<VAR>p : R[X]<GOAL>(algebraMap R A) (p.coeff 0) = (aeval 0) p
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N : LieSubmodule R L M<GOAL>N.incl.range = N
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>completedCosZeta (-a) s = completedCosZeta a s
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<GOAL>W.ΨSq 1 = 1
<VAR>a n k : ℕ<GOAL>(2 ^ k).bitIndices = [k]
<VAR>a n k : ℕ<GOAL>map (fun x => x + k) (bitIndices 1) = [k]
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>φ : E ≃ₗᵢ[ℝ] E<VAR>hφ : 0 < LinearMap.det ↑φ.toLinearEquiv<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>x : Fin (n + 1) → E<GOAL>o.volumeForm (⇑φ ∘ x) = o.volumeForm x
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>φ : E ≃ₗᵢ[ℝ] E<VAR>hφ : 0 < LinearMap.det ↑φ.toLinearEquiv<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>x : Fin (n + 1) → E<VAR>this : FiniteDimensional ℝ E<GOAL>o.volumeForm (⇑φ ∘ x) = o.volumeForm x
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>φ : E ≃ₗᵢ[ℝ] E<VAR>hφ : 0 < LinearMap.det ↑φ.toLinearEquiv<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>x : Fin (n + 1) → E<VAR>this : FiniteDimensional ℝ E<GOAL>o = (map (Fin (n + 1)) φ.toLinearEquiv) o
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>φ : E ≃ₗᵢ[ℝ] E<VAR>hφ : 0 < LinearMap.det ↑φ.toLinearEquiv<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>x : Fin (n + 1) → E<VAR>this : FiniteDimensional ℝ E<GOAL>x = ⇑φ.symm ∘ ⇑φ ∘ x
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>α : Type u_9<VAR>s : Set (α → Prop)<VAR>a : α<GOAL>sInf s a ↔ ∀ r ∈ s, r a
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>α : Type u_9<VAR>s : Set (α → Prop)<VAR>a : α<GOAL>⨅ f, ↑f a ↔ ∀ r ∈ s, r a
<VAR>s b : ℝ<VAR>hb : 0 < b<GOAL>Tendsto (fun x => rexp (b * x) / x ^ s) atTop atTop
<VAR>s b : ℝ<VAR>hb : 0 < b<GOAL>((fun x => x ^ b) ∘ fun x => rexp x / x ^ (s / b)) =ᶠ[atTop] fun x => rexp (b * x) / x ^ s
<VAR>s b : ℝ<VAR>hb : 0 < b<VAR>x : ℝ<VAR>hx₀ : 0 ≤ x<GOAL>((fun x => x ^ b) ∘ fun x => rexp x / x ^ (s / b)) x = rexp (b * x) / x ^ s
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁸ : SeminormedAddCommGroup V<VAR>inst✝⁷ : PseudoMetricSpace P<VAR>inst✝⁶ : NormedAddTorsor V P<VAR>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : MetricSpace Q<VAR>inst✝³ : NormedAddTorsor W Q<VAR>𝕜 : Type u_6<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 V<VAR>inst✝ : NormedSpace 𝕜 W<VAR>s : AffineSubspace 𝕜 Q<GOAL>IsClosed ↑s.direction ↔ IsClosed ↑s
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁸ : SeminormedAddCommGroup V<VAR>inst✝⁷ : PseudoMetricSpace P<VAR>inst✝⁶ : NormedAddTorsor V P<VAR>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : MetricSpace Q<VAR>inst✝³ : NormedAddTorsor W Q<VAR>𝕜 : Type u_6<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 V<VAR>inst✝ : NormedSpace 𝕜 W<GOAL>IsClosed ↑⊥.direction ↔ IsClosed ↑⊥
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁸ : SeminormedAddCommGroup V<VAR>inst✝⁷ : PseudoMetricSpace P<VAR>inst✝⁶ : NormedAddTorsor V P<VAR>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : MetricSpace Q<VAR>inst✝³ : NormedAddTorsor W Q<VAR>𝕜 : Type u_6<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 V<VAR>inst✝ : NormedSpace 𝕜 W<VAR>s : AffineSubspace 𝕜 Q<VAR>x : Q<VAR>hx : x ∈ ↑s<GOAL>IsClosed ↑s.direction ↔ IsClosed ↑s
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁸ : SeminormedAddCommGroup V<VAR>inst✝⁷ : PseudoMetricSpace P<VAR>inst✝⁶ : NormedAddTorsor V P<VAR>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : MetricSpace Q<VAR>inst✝³ : NormedAddTorsor W Q<VAR>𝕜 : Type u_6<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 V<VAR>inst✝ : NormedSpace 𝕜 W<VAR>s : AffineSubspace 𝕜 Q<VAR>x : Q<VAR>hx : x ∈ ↑s<GOAL>IsClosed ((fun x_1 => x_1 -ᵥ x) '' ↑s) ↔ IsClosed (⇑(IsometryEquiv.vaddConst x).toHomeomorph.symm '' ↑s)