ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<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>inst✝⁴ : Module.Free R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : LieAlgebra.IsNilpotent R L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsPrincipalIdealRing R<VAR>z : L<VAR>hzc : z ∈ LieAlgebra.center R L<VAR>x : L<VAR>A : Type u_1 := AlgebraicClosure (FractionRing R)<VAR>hz : 1 ⊗ₜ[R] z ∈ lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] L) 1<GOAL>(trace A (A ⊗[R] M)) ((toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] z) ∘ₗ (toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] x)) = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<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>inst✝⁴ : Module.Free R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : LieAlgebra.IsNilpotent R L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsPrincipalIdealRing R<VAR>z x : L<VAR>A : Type u_1 := AlgebraicClosure (FractionRing R)<VAR>hz : 1 ⊗ₜ[R] z ∈ lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] L) 1<VAR>hzc : 1 ⊗ₜ[R] z ∈ LieAlgebra.center A (A ⊗[R] L)<GOAL>(trace A (A ⊗[R] M)) ((toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] z) ∘ₗ (toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] x)) = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<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>inst✝⁴ : Module.Free R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : LieAlgebra.IsNilpotent R L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsPrincipalIdealRing R<VAR>z x : L<VAR>A : Type u_1 := AlgebraicClosure (FractionRing R)<VAR>hz : 1 ⊗ₜ[R] z ∈ lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] L) 1<VAR>hzc : 1 ⊗ₜ[R] z ∈ LieAlgebra.center A (A ⊗[R] L)<GOAL>⨆ μ, ⨆ k, (((toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] x)).genEigenspace μ) k = ⊤
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<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>inst✝⁴ : Module.Free R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : LieAlgebra.IsNilpotent R L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsPrincipalIdealRing R<VAR>z x : L<VAR>A : Type u_1 := AlgebraicClosure (FractionRing R)<VAR>hz : 1 ⊗ₜ[R] z ∈ lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] L) 1<VAR>hzc : 1 ⊗ₜ[R] z ∈ LieAlgebra.center A (A ⊗[R] L)<GOAL>∀ (μ : A), (trace A ↥(⨆ k, (((toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] x)).genEigenspace μ) k)) (LinearMap.restrict ((toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] z)) ⋯) = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<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>inst✝⁴ : Module.Free R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : LieAlgebra.IsNilpotent R L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsPrincipalIdealRing R<VAR>z x : L<VAR>A : Type u_1 := AlgebraicClosure (FractionRing R)<VAR>hz : 1 ⊗ₜ[R] z ∈ lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] L) 1<VAR>hzc : 1 ⊗ₜ[R] z ∈ LieAlgebra.center A (A ⊗[R] L)<GOAL>Commute ((toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] x)) ((toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] z))
<VAR>C : Type u<VAR>inst✝¹⁰ : Category.{v, u} C<VAR>X Y : C<VAR>D : Type u₂<VAR>inst✝⁹ : Category.{w, u₂} D<VAR>E : Type u₃<VAR>inst✝⁸ : Category.{w', u₃} E<VAR>F✝ : C ⥤ D<VAR>G : D ⥤ E<VAR>A✝ A' B B' : C<VAR>inst✝⁷ : HasBinaryProduct A✝ B<VAR>inst✝⁶ : HasBinaryProduct A' B'<VAR>inst✝⁵ : HasBinaryProduct (F✝.obj A✝) (F✝.obj B)<VAR>inst✝⁴ : HasBinaryProduct (F✝.obj A') (F✝.obj B')<VAR>inst✝³ : HasBinaryProduct (G.obj (F✝.obj A✝)) (G.obj (F✝.obj B))<VAR>inst✝² : HasBinaryProduct ((F✝ ⋙ G).obj A✝) ((F✝ ⋙ G).obj B)<VAR>inst✝¹ : HasBinaryProducts C<VAR>inst✝ : HasBinaryProducts D<VAR>F : C ⥤ D<VAR>A f : C<GOAL>∀ ⦃Y : C⦄ (f_1 : f ⟶ Y), (prod.functor.obj A ⋙ F).map f_1 ≫ (fun B => prodComparison F A B) Y = (fun B => prodComparison F A B) f ≫ (F ⋙ prod.functor.obj (F.obj A)).map f_1
<VAR>x : ℝ<GOAL>cos (x - π / 2) = sin x
<VAR>s : Finset ℕ<VAR>m n✝ p n : ℕ<VAR>h0 : n ≠ 0<GOAL>(filter Squarefree n.divisors).val = Multiset.map (fun x => x.val.prod) (normalizedFactors n).toFinset.powerset.val
<VAR>s : Finset ℕ<VAR>m n✝ p n : ℕ<VAR>h0 : n ≠ 0<GOAL>∀ (a : ℕ), a ∈ (filter Squarefree n.divisors).val ↔ a ∈ Multiset.map (fun x => x.val.prod) (normalizedFactors n).toFinset.powerset.val
<VAR>s : Finset ℕ<VAR>m n✝ p n : ℕ<VAR>h0 : n ≠ 0<GOAL>∀ x ∈ (normalizedFactors n).toFinset.powerset.val, ∀ y ∈ (normalizedFactors n).toFinset.powerset.val, x.val.prod = y.val.prod → x = y
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>n : ℤ<GOAL>(mk W) (W.ψ n) = (mk W) (W.Ψ n)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : InvolutiveInv α<VAR>s : Finset α<VAR>a : α<GOAL>a ∈ s⁻¹ ↔ a⁻¹ ∈ s
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>S : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : CommSemiring A<VAR>inst✝³ : CommSemiring B<VAR>inst✝² : Algebra S R<VAR>inst✝¹ : Algebra S A<VAR>inst✝ : Algebra S B<VAR>g : R →ₐ[S] A<VAR>y : σ → A<VAR>x✝ : σ → S<VAR>i✝ : σ<GOAL>(aevalTower (AlgHom.id S S) x✝) (X i✝) = (aeval x✝) (X i✝)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>inst✝ : EMetricSpace X<VAR>K U : ι → Set X<VAR>hK : ∀ (i : ι), IsClosed (K i)<VAR>hU : ∀ (i : ι), IsOpen (U i)<VAR>hKU : ∀ (i : ι), K i ⊆ U i<VAR>hfin : LocallyFinite K<VAR>x : X<GOAL>∃ r, ∀ᶠ (y : X) in 𝓝 x, r ∈ Ioi 0 ∩ ENNReal.ofReal ⁻¹' ⋂ i, ⋂ (_ : y ∈ K i), {r | closedBall y r ⊆ U i}
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>inst✝ : EMetricSpace X<VAR>K U : ι → Set X<VAR>hK : ∀ (i : ι), IsClosed (K i)<VAR>hU : ∀ (i : ι), IsOpen (U i)<VAR>hKU : ∀ (i : ι), K i ⊆ U i<VAR>hfin : LocallyFinite K<VAR>x : X<VAR>this : ∀ᶠ (x_1 : ℝ) in 𝓝 0, ∀ᶠ (y : X) in 𝓝 x, ∀ (i : ι), (ENNReal.ofReal x_1, y).2 ∈ K i → closedBall (ENNReal.ofReal x_1, y).2 (ENNReal.ofReal x_1, y).1 ⊆ U i<GOAL>∃ r, ∀ᶠ (y : X) in 𝓝 x, r ∈ Ioi 0 ∩ ENNReal.ofReal ⁻¹' ⋂ i, ⋂ (_ : y ∈ K i), {r | closedBall y r ⊆ U i}
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>inst✝ : EMetricSpace X<VAR>K U : ι → Set X<VAR>hK : ∀ (i : ι), IsClosed (K i)<VAR>hU : ∀ (i : ι), IsOpen (U i)<VAR>hKU : ∀ (i : ι), K i ⊆ U i<VAR>hfin : LocallyFinite K<VAR>x : X<VAR>this : ∀ᶠ (x_1 : ℝ) in 𝓝 0, ∀ᶠ (y : X) in 𝓝 x, ∀ (i : ι), (ENNReal.ofReal x_1, y).2 ∈ K i → closedBall (ENNReal.ofReal x_1, y).2 (ENNReal.ofReal x_1, y).1 ⊆ U i<VAR>r : ℝ<VAR>hr0 : r > 0<VAR>hr : ∀ᶠ (y : X) in 𝓝 x, ∀ (i : ι), (ENNReal.ofReal r, y).2 ∈ K i → closedBall (ENNReal.ofReal r, y).2 (ENNReal.ofReal r, y).1 ⊆ U i<GOAL>∃ r, ∀ᶠ (y : X) in 𝓝 x, r ∈ Ioi 0 ∩ ENNReal.ofReal ⁻¹' ⋂ i, ⋂ (_ : y ∈ K i), {r | closedBall y r ⊆ U i}
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>inst✝ : EMetricSpace X<VAR>K U : ι → Set X<VAR>hK : ∀ (i : ι), IsClosed (K i)<VAR>hU : ∀ (i : ι), IsOpen (U i)<VAR>hKU : ∀ (i : ι), K i ⊆ U i<VAR>hfin : LocallyFinite K<VAR>x : X<VAR>this : ∀ᶠ (x_1 : ℝ) in 𝓝 0, ∀ᶠ (y : X) in 𝓝 x, ∀ (i : ι), (ENNReal.ofReal x_1, y).2 ∈ K i → closedBall (ENNReal.ofReal x_1, y).2 (ENNReal.ofReal x_1, y).1 ⊆ U i<VAR>r : ℝ<VAR>hr0 : r > 0<VAR>hr : ∀ᶠ (y : X) in 𝓝 x, ∀ (i : ι), (ENNReal.ofReal r, y).2 ∈ K i → closedBall (ENNReal.ofReal r, y).2 (ENNReal.ofReal r, y).1 ⊆ U i<VAR>y : X<VAR>hy : ∀ (i : ι), (ENNReal.ofReal r, y).2 ∈ K i → closedBall (ENNReal.ofReal r, y).2 (ENNReal.ofReal r, y).1 ⊆ U i<GOAL>r ∈ ENNReal.ofReal ⁻¹' ⋂ i, ⋂ (_ : y ∈ K i), {r | closedBall y r ⊆ U i}
<VAR>R : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝¹⁹ : CommSemiring R<VAR>inst✝¹⁸ : AddCommMonoid M✝<VAR>inst✝¹⁷ : Module R M✝<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹⁶ : CommRing R₁<VAR>inst✝¹⁵ : AddCommGroup M₁<VAR>inst✝¹⁴ : Module R₁ M₁<VAR>R₂ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝¹³ : CommSemiring R₂<VAR>inst✝¹² : AddCommMonoid M₂<VAR>inst✝¹¹ : Module R₂ M₂<VAR>R₃ : Type u_7<VAR>M₃ : Type u_8<VAR>inst✝¹⁰ : CommRing R₃<VAR>inst✝⁹ : AddCommGroup M₃<VAR>inst✝⁸ : Module R₃ M₃<VAR>V : Type u_9<VAR>K : Type u_10<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : Module K V<VAR>B : BilinForm R M✝<VAR>B₁ : BilinForm R₁ M₁<VAR>B₂ : BilinForm R₂ M₂<VAR>A : Type u_11<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : IsDomain A<VAR>inst✝² : Module A M₃<VAR>B₃ : BilinForm A M₃<VAR>ι : Type u_12<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>M : Matrix ι ι R₃<VAR>b : Basis ι R₃ M₃<GOAL>((Matrix.toBilin b) M).Nondegenerate ↔ M.Nondegenerate
<VAR>b c d : ℝ≥0∞<VAR>r p q a : ℝ≥0<VAR>h0 : ¬a = 0<GOAL>a * a⁻¹ = 1
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Zero M<VAR>i : ι<VAR>m : M<VAR>i✝ : ι<GOAL>(single i m).toDFinsupp i✝ = (DFinsupp.single i m) i✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>inst✝ : T2Space β<VAR>di : DenseInducing i<VAR>hd : Dense (range i)ᶜ<VAR>s : Set α<VAR>hs : IsCompact s<GOAL>interior s = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>inst✝ : T2Space β<VAR>di : DenseInducing i<VAR>hd : Dense (range i)ᶜ<VAR>s : Set α<VAR>hs : IsCompact s<VAR>x : α<VAR>hx : x ∈ interior s<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>inst✝ : T2Space β<VAR>di : DenseInducing i<VAR>hd : Dense (range i)ᶜ<VAR>s : Set α<VAR>hs : IsCompact s<VAR>x : α<VAR>hx : s ∈ 𝓝 x<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>inst✝ : T2Space β<VAR>di : DenseInducing i<VAR>hd : Dense (range i)ᶜ<VAR>s : Set α<VAR>hs : IsCompact s<VAR>x : α<VAR>hx : s ∈ 𝓝 x<VAR>this : closure (i '' s) ∈ 𝓝 (i x)<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>inst✝ : T2Space β<VAR>di : DenseInducing i<VAR>hd : Dense (range i)ᶜ<VAR>s : Set α<VAR>hs : IsCompact s<VAR>x : α<VAR>hx : s ∈ 𝓝 x<VAR>this : i '' s ∈ 𝓝 (i x)<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>inst✝ : T2Space β<VAR>di : DenseInducing i<VAR>hd : Dense (range i)ᶜ<VAR>s : Set α<VAR>hs : IsCompact s<VAR>x : α<VAR>hx : s ∈ 𝓝 x<VAR>this : i '' s ∈ 𝓝 (i x)<VAR>y : β<VAR>hyi : y ∈ (range i)ᶜ<VAR>hys : y ∈ i '' s<GOAL>False
<VAR>α✝ : Type ua<VAR>β✝ : Type ub<VAR>γ✝ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝² : UniformSpace α✝<VAR>inst✝¹ : UniformSpace β✝<VAR>inst✝ : UniformSpace γ✝<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>f : α → β → γ<VAR>ua1 ua2 : UniformSpace α<VAR>ub1 ub2 : UniformSpace β<VAR>uc1 : UniformSpace γ<VAR>h : UniformContinuous fun p => f p.1 p.2<GOAL>UniformContinuous fun p => f p.1 p.2
<VAR>α✝ : Type ua<VAR>β✝ : Type ub<VAR>γ✝ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝² : UniformSpace α✝<VAR>inst✝¹ : UniformSpace β✝<VAR>inst✝ : UniformSpace γ✝<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>f : α → β → γ<VAR>ua1 ua2 : UniformSpace α<VAR>ub1 ub2 : UniformSpace β<VAR>uc1 : UniformSpace γ<VAR>h : UniformContinuous fun p => f p.1 p.2<VAR>ha : UniformContinuous id<GOAL>UniformContinuous fun p => f p.1 p.2
<VAR>α✝ : Type ua<VAR>β✝ : Type ub<VAR>γ✝ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝² : UniformSpace α✝<VAR>inst✝¹ : UniformSpace β✝<VAR>inst✝ : UniformSpace γ✝<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>f : α → β → γ<VAR>ua1 ua2 : UniformSpace α<VAR>ub1 ub2 : UniformSpace β<VAR>uc1 : UniformSpace γ<VAR>h : UniformContinuous fun p => f p.1 p.2<VAR>ha : UniformContinuous id<VAR>hb : UniformContinuous id<GOAL>UniformContinuous fun p => f p.1 p.2
<VAR>α✝ : Type ua<VAR>β✝ : Type ub<VAR>γ✝ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝² : UniformSpace α✝<VAR>inst✝¹ : UniformSpace β✝<VAR>inst✝ : UniformSpace γ✝<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>f : α → β → γ<VAR>ua1 ua2 : UniformSpace α<VAR>ub1 ub2 : UniformSpace β<VAR>uc1 : UniformSpace γ<VAR>h : UniformContinuous fun p => f p.1 p.2<VAR>ha : UniformContinuous id<VAR>hb : UniformContinuous id<VAR>h_unif_cont_id : UniformContinuous (Prod.map id id)<GOAL>UniformContinuous fun p => f p.1 p.2
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁹ : NontriviallyNormedField R<VAR>inst✝⁸ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁷ : (x : B) → Module R (E x)<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace R F<VAR>inst✝⁴ : TopologicalSpace B<VAR>inst✝³ : TopologicalSpace (TotalSpace F E)<VAR>inst✝² : (x : B) → TopologicalSpace (E x)<VAR>inst✝¹ : FiberBundle F E<VAR>e : Trivialization F TotalSpace.proj<VAR>inst✝ : Trivialization.IsLinear R e<VAR>x : B<VAR>hx : x ∈ e.baseSet<GOAL>↑e (zeroSection F E x) = (x, 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u_4<VAR>r : ι → ι → Prop<VAR>inst✝ : IsWellOrder ι r<VAR>f : ι → α<VAR>i : ι<GOAL>bfamilyOfFamily' r f (typein r i) ⋯ = f i
<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✝² : CommSemiring α<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>M : Matrix m n α<VAR>a : α<VAR>i✝ : m<VAR>j✝ : n<GOAL>(a • M) i✝ j✝ = (M * diagonal fun x => a) i✝ j✝
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>A : Type u₂<VAR>inst✝² : Category.{v₂, u₂} A<VAR>D : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} D<VAR>inst✝ : HasWeakSheafify J D<VAR>P Q R : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>γ : Q ⟶ R<VAR>hR : Presheaf.IsSheaf J R<GOAL>sheafifyMap J η ≫ sheafifyLift J γ hR = sheafifyLift J (η ≫ γ) hR
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>A : Type u₂<VAR>inst✝² : Category.{v₂, u₂} A<VAR>D : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} D<VAR>inst✝ : HasWeakSheafify J D<VAR>P Q R : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>γ : Q ⟶ R<VAR>hR : Presheaf.IsSheaf J R<GOAL>toSheafify J P ≫ sheafifyMap J η ≫ sheafifyLift J γ hR = η ≫ γ
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>R' : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>inst✝⁴ : FunLike F E ℝ<VAR>inst✝³ : AddGroup E<VAR>inst✝² : SMul R ℝ<VAR>inst✝¹ : SMul R ℝ≥0<VAR>inst✝ : IsScalarTower R ℝ≥0 ℝ<VAR>p✝ : AddGroupSeminorm E<VAR>r : R<VAR>p q : AddGroupSeminorm E<VAR>x y : ℝ<GOAL>r • max x y = max (r • x) (r • y)
<VAR>a b k m n p : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>a✝ : ℕ<GOAL>a✝ ∈ (a.gcd b).primeFactors ↔ a✝ ∈ a.primeFactors ∩ b.primeFactors
<VAR>a b k m n p : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>a✝ : ℕ<GOAL>Prime a✝ ∧ a✝ ∣ a ∧ a✝ ∣ b ↔ (Prime a✝ ∧ a✝ ∣ a) ∧ Prime a✝ ∧ a✝ ∣ b
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig E N τ<VAR>lastc : a.c (last N) = 0<VAR>lastr : a.r (last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>i j : Fin N.succ<VAR>inej : i ≠ j<VAR>hi : 2 < ‖a.c i‖<VAR>hij : ‖a.c i‖ ≤ ‖a.c j‖<GOAL>1 - δ ≤ ‖(2 / ‖a.c i‖) • a.c i - (2 / ‖a.c j‖) • a.c j‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig E N τ<VAR>lastc : a.c (last N) = 0<VAR>lastr : a.r (last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>i j : Fin N.succ<VAR>inej : i ≠ j<VAR>hi : 2 < ‖a.c i‖<VAR>hij : ‖a.c i‖ ≤ ‖a.c j‖<VAR>ah : Pairwise fun i j => a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j<GOAL>1 - δ ≤ ‖(2 / ‖a.c i‖) • a.c i - (2 / ‖a.c j‖) • a.c j‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig E N τ<VAR>lastc : a.c (last N) = 0<VAR>lastr : a.r (last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>i j : Fin N.succ<VAR>inej : i ≠ j<VAR>hi : 2 < ‖a.c i‖<VAR>hij : ‖a.c i‖ ≤ ‖a.c j‖<VAR>ah : Pairwise fun i j => a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j<VAR>δnonneg : 0 ≤ δ<GOAL>1 - δ ≤ ‖(2 / ‖a.c i‖) • a.c i - (2 / ‖a.c j‖) • a.c j‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig E N τ<VAR>lastc : a.c (last N) = 0<VAR>lastr : a.r (last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>i j : Fin N.succ<VAR>inej : i ≠ j<VAR>hi : 2 < ‖a.c i‖<VAR>hij : ‖a.c i‖ ≤ ‖a.c j‖<VAR>ah : Pairwise fun i j => a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j<VAR>δnonneg : 0 ≤ δ<VAR>hcrj : ‖a.c j‖ ≤ a.r j + 1<GOAL>1 - δ ≤ ‖(2 / ‖a.c i‖) • a.c i - (2 / ‖a.c j‖) • a.c j‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig E N τ<VAR>lastc : a.c (last N) = 0<VAR>lastr : a.r (last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>i j : Fin N.succ<VAR>inej : i ≠ j<VAR>hi : 2 < ‖a.c i‖<VAR>hij : ‖a.c i‖ ≤ ‖a.c j‖<VAR>ah : Pairwise fun i j => a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j<VAR>δnonneg : 0 ≤ δ<VAR>hcrj : ‖a.c j‖ ≤ a.r j + 1<VAR>A : a.r i ≤ ‖a.c i‖<GOAL>1 - δ ≤ ‖(2 / ‖a.c i‖) • a.c i - (2 / ‖a.c j‖) • a.c j‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig E N τ<VAR>lastc : a.c (last N) = 0<VAR>lastr : a.r (last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>i j : Fin N.succ<VAR>inej : i ≠ j<VAR>ah : Pairwise fun i j => a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j<VAR>δnonneg : 0 ≤ δ<VAR>hcrj : ‖a.c j‖ ≤ a.r j + 1<VAR>hj : 2 < ‖a.c j‖<VAR>s : ℝ := ‖a.c i‖<VAR>hi : 2 < s<VAR>hij : s ≤ ‖a.c j‖<VAR>A : a.r i ≤ s<GOAL>1 - δ ≤ ‖(2 / s) • a.c i - (2 / ‖a.c j‖) • a.c j‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig E N τ<VAR>lastc : a.c (last N) = 0<VAR>lastr : a.r (last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>i j : Fin N.succ<VAR>inej : i ≠ j<VAR>ah : Pairwise fun i j => a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j<VAR>δnonneg : 0 ≤ δ<VAR>hcrj : ‖a.c j‖ ≤ a.r j + 1<VAR>hj : 2 < ‖a.c j‖<VAR>s : ℝ := ‖a.c i‖<VAR>hi : 2 < s<VAR>hij : s ≤ ‖a.c j‖<VAR>A : a.r i ≤ s<VAR>spos : 0 < s<GOAL>1 - δ ≤ ‖(2 / s) • a.c i - (2 / ‖a.c j‖) • a.c j‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig E N τ<VAR>lastc : a.c (last N) = 0<VAR>lastr : a.r (last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>i j : Fin N.succ<VAR>inej : i ≠ j<VAR>ah : Pairwise fun i j => a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j<VAR>δnonneg : 0 ≤ δ<VAR>hcrj : ‖a.c j‖ ≤ a.r j + 1<VAR>hj : 2 < ‖a.c j‖<VAR>s : ℝ := ‖a.c i‖<VAR>hi : 2 < s<VAR>hij : s ≤ ‖a.c j‖<VAR>A : a.r i ≤ s<VAR>spos : 0 < s<VAR>d : E := (s / ‖a.c j‖) • a.c j<VAR>hd : d = (s / ‖a.c j‖) • a.c j<GOAL>1 - δ ≤ ‖(2 / s) • a.c i - (2 / ‖a.c j‖) • a.c j‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig E N τ<VAR>lastc : a.c (last N) = 0<VAR>lastr : a.r (last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>i j : Fin N.succ<VAR>inej : i ≠ j<VAR>ah : Pairwise fun i j => a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j<VAR>δnonneg : 0 ≤ δ<VAR>hcrj : ‖a.c j‖ ≤ a.r j + 1<VAR>hj : 2 < ‖a.c j‖<VAR>s : ℝ := ‖a.c i‖<VAR>hi : 2 < s<VAR>hij : s ≤ ‖a.c j‖<VAR>A : a.r i ≤ s<VAR>spos : 0 < s<VAR>d : E := (s / ‖a.c j‖) • a.c j<VAR>hd : d = (s / ‖a.c j‖) • a.c j<VAR>I : ‖a.c j - a.c i‖ ≤ ‖a.c j‖ - s + ‖d - a.c i‖<GOAL>1 - δ ≤ ‖(2 / s) • a.c i - (2 / ‖a.c j‖) • a.c j‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig E N τ<VAR>lastc : a.c (last N) = 0<VAR>lastr : a.r (last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>i j : Fin N.succ<VAR>inej : i ≠ j<VAR>ah : Pairwise fun i j => a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j<VAR>δnonneg : 0 ≤ δ<VAR>hcrj : ‖a.c j‖ ≤ a.r j + 1<VAR>hj : 2 < ‖a.c j‖<VAR>s : ℝ := ‖a.c i‖<VAR>hi : 2 < s<VAR>hij : s ≤ ‖a.c j‖<VAR>A : a.r i ≤ s<VAR>spos : 0 < s<VAR>d : E := (s / ‖a.c j‖) • a.c j<VAR>hd : d = (s / ‖a.c j‖) • a.c j<VAR>I : ‖a.c j - a.c i‖ ≤ ‖a.c j‖ - s + ‖d - a.c i‖<VAR>J : a.r j - ‖a.c j - a.c i‖ ≤ s / 2 * δ<GOAL>1 - δ ≤ ‖(2 / s) • a.c i - (2 / ‖a.c j‖) • a.c j‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig E N τ<VAR>lastc : a.c (last N) = 0<VAR>lastr : a.r (last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>i j : Fin N.succ<VAR>inej : i ≠ j<VAR>ah : Pairwise fun i j => a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j<VAR>δnonneg : 0 ≤ δ<VAR>hcrj : ‖a.c j‖ ≤ a.r j + 1<VAR>hj : 2 < ‖a.c j‖<VAR>s : ℝ := ‖a.c i‖<VAR>hi : 2 < s<VAR>hij : s ≤ ‖a.c j‖<VAR>A : a.r i ≤ s<VAR>spos : 0 < s<VAR>d : E := (s / ‖a.c j‖) • a.c j<VAR>hd : d = (s / ‖a.c j‖) • a.c j<VAR>I : ‖a.c j - a.c i‖ ≤ ‖a.c j‖ - s + ‖d - a.c i‖<VAR>J : a.r j - ‖a.c j - a.c i‖ ≤ s / 2 * δ<VAR>invs_nonneg : 0 ≤ 2 / s<GOAL>1 - δ ≤ ‖(2 / s) • a.c i - (2 / ‖a.c j‖) • a.c j‖
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveAt γ v t₀<GOAL>∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt (↑(extChartAt I (γ t₀)) ∘ γ) ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t))) t
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveAt γ v t₀<GOAL>∀ (x : ℝ), γ ⁻¹' (extChartAt I (γ t₀)).source ∈ 𝓝 x ∧ HasMFDerivAt 𝓘(ℝ, ℝ) I γ x (ContinuousLinearMap.smulRight 1 (v (γ x))) → HasDerivAt (↑(extChartAt I (γ t₀)) ∘ γ) ((tangentCoordChange I (γ x) (γ t₀) (γ x)) (v (γ x))) x
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveAt γ v t₀<VAR>t : ℝ<VAR>ht1 : γ ⁻¹' (extChartAt I (γ t₀)).source ∈ 𝓝 t<VAR>ht2 : HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))<GOAL>HasDerivAt (↑(extChartAt I (γ t₀)) ∘ γ) ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t))) t