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>s s' : Set α<VAR>x : α<VAR>p : Filter ι✝<VAR>g : ι✝ → α<VAR>inst✝² : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>ι : Type u_5<VAR>inst✝¹ : Preorder ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>t : ι → Set α<VAR>V : ι → Set (β × β)<VAR>ht : ∀ (n : ι), t n ∈ 𝔖<VAR>hmono : Monotone t<VAR>hex : ∀ s ∈ 𝔖, ∃ n, s ⊆ t n<VAR>hb : (𝓤 β).HasAntitoneBasis V<VAR>this : Nonempty ι<GOAL>∀ (i : ι × ι), True → ∃ i', True ∧ UniformOnFun.gen 𝔖 (t i') (V i') ⊆ UniformOnFun.gen 𝔖 (t i.1) (V i.2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι✝<VAR>g : ι✝ → α<VAR>inst✝² : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>ι : Type u_5<VAR>inst✝¹ : Preorder ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>t : ι → Set α<VAR>V : ι → Set (β × β)<VAR>ht : ∀ (n : ι), t n ∈ 𝔖<VAR>hmono : Monotone t<VAR>hex : ∀ s ∈ 𝔖, ∃ n, s ⊆ t n<VAR>hb : (𝓤 β).HasAntitoneBasis V<VAR>this : Nonempty ι<GOAL>Antitone fun n => UniformOnFun.gen 𝔖 (t n) (V n)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : σ → τ<VAR>hf : Injective f<GOAL>Injective ⇑(rename f)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : σ → τ<VAR>hf : Injective f<VAR>this : ⇑(rename f) = Finsupp.mapDomain (Finsupp.mapDomain f)<GOAL>Injective ⇑(rename f)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : σ → τ<VAR>hf : Injective f<VAR>this : ⇑(rename f) = Finsupp.mapDomain (Finsupp.mapDomain f)<GOAL>Injective (Finsupp.mapDomain (Finsupp.mapDomain f))
<VAR>X : Type u_1<VAR>x : X<VAR>a : FreeAbelianGroup X<GOAL>x ∉ a.support ↔ (coeff x) a = 0
<VAR>X : Type u_1<VAR>x : X<VAR>a : FreeAbelianGroup X<GOAL>(toFinsupp a) x = 0 ↔ (coeff x) a = 0
<VAR>a : UnitAddCircle<VAR>x : ℝ<VAR>hx : x ≤ 0<GOAL>cosKernel a x = 0
<VAR>x : ℝ<VAR>hx : x ≤ 0<VAR>a' : ℝ<GOAL>cosKernel (↑a') x = 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Module R (Additive ℤˣ)<VAR>u : ℤˣ<VAR>n : ℕ<GOAL>Additive.toMul (↑n • Additive.ofMul u) = u ^ n
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>h : IsUniform<VAR>α : Type u<VAR>a : (P F).A<VAR>f : (P F).B a → α<VAR>u : α<GOAL>u ∈ supp (abs ⟨a, f⟩) ↔ u ∈ f '' univ
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>h : IsUniform<VAR>α : Type u<VAR>a : (P F).A<VAR>f : (P F).B a → α<VAR>u : α<GOAL>(∀ (a_1 : (P F).A) (f_1 : (P F).B a_1 → α), abs ⟨a_1, f_1⟩ = abs ⟨a, f⟩ → u ∈ f_1 '' univ) ↔ u ∈ f '' univ
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>h : IsUniform<VAR>α : Type u<VAR>a : (P F).A<VAR>f : (P F).B a → α<VAR>u : α<VAR>h' : u ∈ f '' univ<VAR>a' : (P F).A<VAR>f' : (P F).B a' → α<VAR>e : abs ⟨a', f'⟩ = abs ⟨a, f⟩<GOAL>u ∈ f' '' univ
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>h : IsUniform<VAR>α : Type u<VAR>a : (P F).A<VAR>f : (P F).B a → α<VAR>u : α<VAR>h' : u ∈ f '' univ<VAR>a' : (P F).A<VAR>f' : (P F).B a' → α<VAR>e : abs ⟨a', f'⟩ = abs ⟨a, f⟩<GOAL>u ∈ f '' univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>h : ¬μ.HaveLebesgueDecomposition ν<GOAL>μ.rnDeriv ν = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>hb : 0 < b<GOAL>a ≤ a * b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>hb : 0 < b<GOAL>a = a * 1
<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<GOAL>HasFDerivAt f f' x ↔ (fun h => f (x + h) - f x - f' h) =o[𝓝 0] fun h => h
<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<GOAL>((fun x' => f x' - f x - f' (x' - x)) ∘ fun x_1 => x + x_1) =o[𝓝 0] ((fun x' => x' - x) ∘ fun x_1 => x + x_1) ↔ (fun h => f (x + h) - f x - f' h) =o[𝓝 0] fun h => h
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>r₁ r₂ : ℝ<GOAL>(o.oangle (r₁ • x + r₂ • y) y).sign = SignType.sign r₁ * (o.oangle x y).sign
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁸ : OrderedCommRing R<VAR>inst✝¹⁷ : Nontrivial R<VAR>inst✝¹⁶ : StarRing R<VAR>inst✝¹⁵ : StarOrderedRing R<VAR>inst✝¹⁴ : MetricSpace R<VAR>inst✝¹³ : TopologicalRing R<VAR>inst✝¹² : ContinuousStar R<VAR>inst✝¹¹ : ∀ (α : Type ?u.1322990) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀<VAR>inst✝¹⁰ : TopologicalSpace A<VAR>inst✝⁹ : NonUnitalRing A<VAR>inst✝⁸ : StarRing A<VAR>inst✝⁷ : PartialOrder A<VAR>inst✝⁶ : StarOrderedRing A<VAR>inst✝⁵ : Module R A<VAR>inst✝⁴ : IsScalarTower R A A<VAR>inst✝³ : SMulCommClass R A A<VAR>inst✝² : StarModule R A<VAR>inst✝¹ : NonUnitalContinuousFunctionalCalculus R p<VAR>inst✝ : NonnegSpectrumClass R A<VAR>f : R → R<VAR>a : A<VAR>hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝<VAR>h0 : autoParam (f 0 = 0) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>cfcₙ f a ≤ 0 ↔ ∀ x ∈ σₙ R a, f x ≤ 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁸ : OrderedCommRing R<VAR>inst✝¹⁷ : Nontrivial R<VAR>inst✝¹⁶ : StarRing R<VAR>inst✝¹⁵ : StarOrderedRing R<VAR>inst✝¹⁴ : MetricSpace R<VAR>inst✝¹³ : TopologicalRing R<VAR>inst✝¹² : ContinuousStar R<VAR>inst✝¹¹ : ∀ (α : Type ?u.1322990) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀<VAR>inst✝¹⁰ : TopologicalSpace A<VAR>inst✝⁹ : NonUnitalRing A<VAR>inst✝⁸ : StarRing A<VAR>inst✝⁷ : PartialOrder A<VAR>inst✝⁶ : StarOrderedRing A<VAR>inst✝⁵ : Module R A<VAR>inst✝⁴ : IsScalarTower R A A<VAR>inst✝³ : SMulCommClass R A A<VAR>inst✝² : StarModule R A<VAR>inst✝¹ : NonUnitalContinuousFunctionalCalculus R p<VAR>inst✝ : NonnegSpectrumClass R A<VAR>f : R → R<VAR>a : A<VAR>hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝<VAR>h0 : autoParam (f 0 = 0) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>0 ≤ cfcₙ (fun x => -f x) a ↔ ∀ x ∈ σₙ R a, 0 ≤ -f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>p : β → Prop<VAR>inst✝ : DecidablePred p<VAR>f : α ≃ Subtype p<VAR>g g₁ g₂ : Perm α<VAR>s t : Set α<VAR>h : RightInvOn (⇑g₁) (⇑g₂) t<VAR>a : α<VAR>ha : a ∈ t<GOAL>(g₂.extendDomain f) ((g₁.extendDomain f) ((Subtype.val ∘ ⇑f) a)) = (Subtype.val ∘ ⇑f) a
<VAR>a✝ b n✝ n a : ℕ<GOAL>(n.floorRoot a).factorization = a.factorization ⌊/⌋ n
<VAR>a✝ b n✝ n a : ℕ<GOAL>(if n = 0 ∨ a = 0 then 0 else (a.factorization ⌊/⌋ n).prod fun x x_1 => x ^ x_1).factorization = a.factorization ⌊/⌋ n
<VAR>a✝ b n✝ n a : ℕ<VAR>h : ¬(n = 0 ∨ a = 0)<GOAL>((a.factorization ⌊/⌋ n).prod fun x x_1 => x ^ x_1).factorization = a.factorization ⌊/⌋ n
<VAR>a✝ b n✝ n a : ℕ<VAR>h : ¬(n = 0 ∨ a = 0)<VAR>p : ℕ<VAR>hp : p ∈ (a.factorization ⌊/⌋ n).support<GOAL>Prime p
<VAR>a✝ b n✝ n a : ℕ<VAR>h : ¬(n = 0 ∨ a = 0)<VAR>p : ℕ<VAR>hp : p ∈ (a.factorization ⌊/⌋ n).support<VAR>this : Prime p ∧ p ∣ a ∧ ¬a = 0<GOAL>Prime p
<VAR>ι : Type u<VAR>f : ι → Scheme<VAR>x : ↑↑(∐ f).toPresheafedSpace<GOAL>x ∈ ↑⊤ → x ∈ ↑(⨆ i, Scheme.Hom.opensRange (Sigma.ι f i))
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : M<VAR>f : F<VAR>h : IsPrimitiveRoot ζ k<VAR>i : ℕ<GOAL>ζ ^ (k * i) = 1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s₁ : AffineSubspace k P<VAR>v : V<GOAL>s₁ = map (↑(constVAdd k P (-v))) (map (↑(constVAdd k P v)) s₁)
<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>V : Type u_5<VAR>K : Type u_6<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : AddCommGroup V<VAR>inst✝⁸ : Module K V<VAR>M'✝ : Type u_7<VAR>M'' : Type u_8<VAR>inst✝⁷ : AddCommMonoid M'✝<VAR>inst✝⁶ : AddCommMonoid M''<VAR>inst✝⁵ : Module R M'✝<VAR>inst✝⁴ : Module R M''<VAR>B : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>F : BilinForm R M<VAR>M' : Type u_9<VAR>inst✝³ : AddCommMonoid M'<VAR>inst✝² : Module R M'<VAR>B' : BilinForm R M'<VAR>f f' : M →ₗ[R] M'<VAR>g g' : M' →ₗ[R] M<VAR>M₁' : Type u_10<VAR>inst✝¹ : AddCommGroup M₁'<VAR>inst✝ : Module R₁ M₁'<VAR>B₁' : BilinForm R₁ M₁'<VAR>f₁ f₁' : M₁ →ₗ[R₁] M₁'<VAR>g₁ g₁' : M₁' →ₗ[R₁] M₁<VAR>B₂' : BilinForm R M'<VAR>f₂ f₂' : M →ₗ[R] M'<VAR>g₂ g₂' : M' →ₗ[R] M<VAR>c : R<VAR>h : B.IsAdjointPair B₂' f₂ g₂<VAR>x : M<VAR>y : M'<GOAL>(B₂' ((c • f₂) x)) y = (B x) ((c • g₂) y)
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x : α✝ (last n)<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p : (i : Fin n) → α✝ i.castSucc<VAR>i : Fin n<VAR>y : α✝ i.castSucc<VAR>z : α✝ (last n)<VAR>α : Type u_1<VAR>a : α<VAR>as : Fin n → α<VAR>bs : Fin m → α<GOAL>append (cons a as) bs = cons a (append as bs) ∘ cast ⋯
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x : α✝ (last n)<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p : (i : Fin n) → α✝ i.castSucc<VAR>i✝ : Fin n<VAR>y : α✝ i✝.castSucc<VAR>z : α✝ (last n)<VAR>α : Type u_1<VAR>a : α<VAR>as : Fin n → α<VAR>bs : Fin m → α<VAR>i : Fin (n + 1 + m)<GOAL>append (cons a as) bs i = (cons a (append as bs) ∘ cast ⋯) i
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x : α✝ (last n)<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p : (i : Fin n) → α✝ i.castSucc<VAR>i✝ : Fin n<VAR>y : α✝ i✝.castSucc<VAR>z : α✝ (last n)<VAR>α : Type u_1<VAR>a : α<VAR>as : Fin n → α<VAR>bs : Fin m → α<VAR>i : ℕ<VAR>isLt✝ : i < n + 1 + m<GOAL>append (cons a as) bs ⟨i, isLt✝⟩ = (cons a (append as bs) ∘ cast ⋯) ⟨i, isLt✝⟩
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x : α✝ (last n)<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p : (i : Fin n) → α✝ i.castSucc<VAR>i✝ : Fin n<VAR>y : α✝ i✝.castSucc<VAR>z : α✝ (last n)<VAR>α : Type u_1<VAR>a : α<VAR>as : Fin n → α<VAR>bs : Fin m → α<VAR>i : ℕ<VAR>isLt✝ : i < n + 1 + m<GOAL>(if h : i < n + 1 then cases a as ⟨i, ⋯⟩ else ⋯ ▸ bs (subNat (n + 1) ⟨i, ⋯⟩ ⋯)) = cases a (addCases as bs) ⟨i, ⋯⟩
<VAR>R : Type u_1<VAR>C : Type u_2<VAR>inst✝³ : Semiring R<VAR>inst✝² : Category.{u_3, u_2} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Linear R C<VAR>S₁ S₂ : ShortComplex C<VAR>φ φ' : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>a : R<VAR>γ : LeftHomologyMapData φ h₁ h₂<GOAL>leftHomologyMap' (a • φ) h₁ h₂ = a • leftHomologyMap' φ h₁ h₂
<VAR>V✝ : Type u<VAR>G : SimpleGraph V✝<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>V : Type u_3<VAR>inst✝ : Infinite V<GOAL>⊤.chromaticNumber = ⊤
<VAR>V✝ : Type u<VAR>G : SimpleGraph V✝<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>V : Type u_3<VAR>inst✝ : Infinite V<VAR>hc : ¬⊤.chromaticNumber = ⊤<GOAL>False
<VAR>V✝ : Type u<VAR>G : SimpleGraph V✝<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>V : Type u_3<VAR>inst✝ : Infinite V<VAR>hc : ∃ n, ⊤.Colorable n<GOAL>False
<VAR>V✝ : Type u<VAR>G : SimpleGraph V✝<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>V : Type u_3<VAR>inst✝ : Infinite V<VAR>n : ℕ<VAR>hn : ⊤.Coloring (Fin n)<GOAL>False
<VAR>m n : ℕ<GOAL>1 < ack (m + 1) (n + 1)
<VAR>m n : ℕ<GOAL>1 < ack m (ack (m + 1) n)
<VAR>m n h✝ : ℕ<VAR>h : ack (m + 1) n = h✝.succ<GOAL>1 < ack m (ack (m + 1) n)
<VAR>J : Type w<VAR>C✝ : Type u<VAR>inst✝² : Category.{v, u} C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>B : C<VAR>objs : J → C<VAR>arrows : (j : J) → B ⟶ objs j<VAR>inst✝ : HasWidePushout B objs arrows<VAR>X : C<VAR>f : B ⟶ X<VAR>fs : (j : J) → objs j ⟶ X<VAR>w : ∀ (j : J), arrows j ≫ fs j = f<VAR>j : J<GOAL>ι arrows j ≫ desc f fs w = fs j
<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>x y : F<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>R : ℝ<VAR>hx' : ‖x‖ ≠ 0<VAR>hy' : ‖y‖ ≠ 0<GOAL>dist ((R / ‖x‖) ^ 2 • x) ((R / ‖y‖) ^ 2 • y) = √(‖(R / ‖x‖) ^ 2 • x - (R / ‖y‖) ^ 2 • y‖ ^ 2)
<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>x y : F<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>R : ℝ<VAR>hx' : ‖x‖ ≠ 0<VAR>hy' : ‖y‖ ≠ 0<GOAL>‖(R / ‖x‖) ^ 2 • x - (R / ‖y‖) ^ 2 • y‖ ^ 2 = (R ^ 2 / (‖x‖ * ‖y‖)) ^ 2 * ‖x - y‖ ^ 2
<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>x y : F<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>R : ℝ<VAR>hx' : ‖x‖ ≠ 0<VAR>hy' : ‖y‖ ≠ 0<GOAL>((R * R * ‖x‖ * (R * R * ‖x‖) * (‖y‖ * ‖y‖ * (‖x‖ * ‖x‖)) - ‖x‖ * ‖x‖ * (‖x‖ * ‖x‖) * (2 * (R * R * (R * R * ⟪x, y⟫_ℝ)))) * (‖y‖ * ‖y‖ * (‖y‖ * ‖y‖)) + R * R * ‖y‖ * (R * R * ‖y‖) * (‖x‖ * ‖x‖ * (‖x‖ * ‖x‖) * (‖y‖ * ‖y‖ * (‖x‖ * ‖x‖)))) * (‖x‖ * ‖y‖ * (‖x‖ * ‖y‖)) = R * R * (R * R) * (‖x‖ * ‖x‖ - 2 * ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖) * (‖x‖ * ‖x‖ * (‖x‖ * ‖x‖) * (‖y‖ * ‖y‖ * (‖x‖ * ‖x‖)) * (‖y‖ * ‖y‖ * (‖y‖ * ‖y‖)))
<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>x y : F<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>R : ℝ<VAR>hx' : ‖x‖ ≠ 0<VAR>hy' : ‖y‖ ≠ 0<GOAL>√((R ^ 2 / (‖x‖ * ‖y‖)) ^ 2 * ‖x - y‖ ^ 2) = R ^ 2 / (‖x‖ * ‖y‖) * dist x y
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle y (y - x)).cos * ‖y - x‖ = ‖y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<VAR>hs : (o.oangle y (y - x)).sign = 1<GOAL>(o.oangle y (y - x)).cos * ‖y - x‖ = ‖y‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>n m : ℕ<VAR>h : n < m<GOAL>MeasureTheory.SignedMeasure.restrictNonposSeq s i n ∩ MeasureTheory.SignedMeasure.restrictNonposSeq s i m = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>n m : ℕ<VAR>h : n < m<GOAL>∀ (x : α), x ∉ MeasureTheory.SignedMeasure.restrictNonposSeq s i n ∩ MeasureTheory.SignedMeasure.restrictNonposSeq s i m
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Set P<VAR>p : P<VAR>hp : p ∈ s<GOAL>vectorSpan k s = Submodule.span k ((fun x => p -ᵥ x) '' (s \ {p}))
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Set P<VAR>p : P<VAR>hp : p ∈ s<GOAL>Submodule.span k (insert (p -ᵥ p) ((fun x => p -ᵥ x) '' (s \ {p}))) = Submodule.span k ((fun x => p -ᵥ x) '' (s \ {p}))
<VAR>ζ : ℂˣ<VAR>n : ℕ+<VAR>hζ : ζ ∈ rootsOfUnity n ℂ<GOAL>‖↑ζ‖ = 1
<VAR>ζ : ℂˣ<VAR>n : ℕ+<VAR>hζ : ζ ∈ rootsOfUnity n ℂ<GOAL>↑ζ ^ ↑n = 1
<VAR>ζ : ℂˣ<VAR>n : ℕ+<VAR>hζ : ζ ∈ rootsOfUnity n ℂ<GOAL>↑(ζ ^ ↑n) = 1
<VAR>ζ : ℂˣ<VAR>n : ℕ+<VAR>hζ : ζ ^ ↑n = 1<GOAL>↑(ζ ^ ↑n) = 1
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f✝ g : α✝ → ℝ≥0∞<VAR>α : Type u_4<VAR>f : α → ℝ≥0∞<VAR>hf : ∑' (x : α), f x ≠ ⊤<GOAL>Tendsto (fun s => ∑' (b : { x // x ∉ s }), f ↑b) atTop (𝓝 0)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f✝ g : α✝ → ℝ≥0∞<VAR>α : Type u_4<VAR>f : α → ℝ≥0<VAR>hf : ∑' (x : α), (fun i => ↑(f i)) x ≠ ⊤<GOAL>Tendsto (fun s => ∑' (b : { x // x ∉ s }), (fun i => ↑(f i)) ↑b) atTop (𝓝 0)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f✝ g : α✝ → ℝ≥0∞<VAR>α : Type u_4<VAR>f : α → ℝ≥0<VAR>hf : ∑' (x : α), (fun i => ↑(f i)) x ≠ ⊤<VAR>x✝ : Finset α<GOAL>∑' (b : { x // x ∉ x✝ }), (fun i => ↑(f i)) ↑b = ↑(∑' (b : { x // x ∉ x✝ }), f ↑b)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f✝ g : α✝ → ℝ≥0∞<VAR>α : Type u_4<VAR>f : α → ℝ≥0<VAR>hf : ∑' (x : α), (fun i => ↑(f i)) x ≠ ⊤<VAR>x✝ : Finset α<GOAL>Summable fun b => f ↑b
<VAR>α : Sort u_2<VAR>β : Sort u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>P : α → Sort u_1<VAR>e : α ≃ β<VAR>f : (a : α) → P a<VAR>b : β<VAR>x : P (e.symm b)<VAR>b' : β<GOAL>(Equiv.piCongrLeft' P e) (update f (e.symm b) x) b' = update ((Equiv.piCongrLeft' P e) f) b x b'
<VAR>α : Sort u_2<VAR>β : Sort u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>P : α → Sort u_1<VAR>e : α ≃ β<VAR>f : (a : α) → P a<VAR>b' : β<VAR>x : P (e.symm b')<GOAL>(Equiv.piCongrLeft' P e) (update f (e.symm b') x) b' = update ((Equiv.piCongrLeft' P e) f) b' x b'
<VAR>α : Sort u_2<VAR>β : Sort u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>P : α → Sort u_1<VAR>e : α ≃ β<VAR>f : (a : α) → P a<VAR>b : β<VAR>x : P (e.symm b)<VAR>b' : β<VAR>h : b' ≠ b<GOAL>(Equiv.piCongrLeft' P e) (update f (e.symm b) x) b' = update ((Equiv.piCongrLeft' P e) f) b x b'
<VAR>y : ℝ<GOAL>Real.toEReal ⁻¹' Ioc ⊥ ↑y = Iic y
<VAR>y : ℝ<GOAL>Real.toEReal ⁻¹' (Ioi ⊥ ∩ Iic ↑y) = Iic y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : OuterMeasure α<VAR>f : α → β<VAR>hf : Surjective f<GOAL>(map f) ⊤ = ⊤
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → β<VAR>s t : List α<VAR>hf : Injective f<VAR>h : s.Disjoint t<GOAL>(map f s).Disjoint (map f t)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → β<VAR>s t : List α<VAR>hf : Injective f<VAR>h : s.Disjoint t<GOAL>(pmap (fun a x => f a) s ⋯).Disjoint (pmap (fun a x => f a) t ⋯)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : ℚ_[p]<VAR>property✝ : ‖k‖ ≤ 1<VAR>h : ‖⟨k, property✝⟩‖ = 1<GOAL>⟨k, property✝⟩ * inv ⟨k, property✝⟩ = 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : ℚ_[p]<VAR>property✝ : ‖k‖ ≤ 1<VAR>h : ‖⟨k, property✝⟩‖ = 1<VAR>hk : k ≠ 0<GOAL>⟨k, property✝⟩ * inv ⟨k, property✝⟩ = 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : ℚ_[p]<VAR>property✝ : ‖k‖ ≤ 1<VAR>h : ‖⟨k, property✝⟩‖ = 1<VAR>hk : k ≠ 0<GOAL>(⟨k, property✝⟩ * match ⟨k, property✝⟩ with | ⟨k, property⟩ => if h : ‖k‖ = 1 then ⟨k⁻¹, ⋯⟩ else 0) = 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : ℚ_[p]<VAR>property✝ : ‖k‖ ≤ 1<VAR>h : ‖k‖ = 1<VAR>hk : k ≠ 0<GOAL>(⟨k, property✝⟩ * match ⟨k, property✝⟩ with | ⟨k, property⟩ => if h : ‖k‖ = 1 then ⟨k⁻¹, ⋯⟩ else 0) = 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : ℚ_[p]<VAR>property✝ : ‖k‖ ≤ 1<VAR>h : ‖k‖ = 1<VAR>hk : k ≠ 0<GOAL>(⟨k, property✝⟩ * if h : ‖k‖ = 1 then ⟨k⁻¹, ⋯⟩ else 0) = 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : ℚ_[p]<VAR>property✝ : ‖k‖ ≤ 1<VAR>h : ‖k‖ = 1<VAR>hk : k ≠ 0<GOAL>⟨k, property✝⟩ * ⟨k⁻¹, ⋯⟩ = 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : ℚ_[p]<VAR>property✝ : ‖k‖ ≤ 1<VAR>h : ‖k‖ = 1<VAR>hk : k ≠ 0<GOAL>↑(⟨k, property✝⟩ * ⟨k⁻¹, ⋯⟩) = ↑1
<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>𝔸 : Type u_6<VAR>𝔸' : Type u_7<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedCommRing 𝔸'<VAR>inst✝¹ : NormedAlgebra 𝕜 𝔸<VAR>inst✝ : NormedAlgebra 𝕜 𝔸'<VAR>a b : E → 𝔸<VAR>a' b' : E →L[𝕜] 𝔸<VAR>c d✝ : E → 𝔸'<VAR>c' d' : E →L[𝕜] 𝔸'<VAR>hc : HasFDerivWithinAt c c' s x<VAR>d : 𝔸'<GOAL>HasFDerivWithinAt (fun y => c y * d) (d • c') s 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>𝔸 : Type u_6<VAR>𝔸' : Type u_7<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedCommRing 𝔸'<VAR>inst✝¹ : NormedAlgebra 𝕜 𝔸<VAR>inst✝ : NormedAlgebra 𝕜 𝔸'<VAR>a b : E → 𝔸<VAR>a' b' : E →L[𝕜] 𝔸<VAR>c d✝ : E → 𝔸'<VAR>c' d' : E →L[𝕜] 𝔸'<VAR>hc : HasFDerivWithinAt c c' s x<VAR>d : 𝔸'<GOAL>d • c' = c'.smulRight d
<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>𝔸 : Type u_6<VAR>𝔸' : Type u_7<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedCommRing 𝔸'<VAR>inst✝¹ : NormedAlgebra 𝕜 𝔸<VAR>inst✝ : NormedAlgebra 𝕜 𝔸'<VAR>a b : E → 𝔸<VAR>a' b' : E →L[𝕜] 𝔸<VAR>c d✝ : E → 𝔸'<VAR>c' d' : E →L[𝕜] 𝔸'<VAR>hc : HasFDerivWithinAt c c' s x<VAR>d : 𝔸'<VAR>z : E<GOAL>(d • c') z = (c'.smulRight d) z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : γ → α → β<VAR>x : α → β<VAR>i : Option γ<VAR>y : α<GOAL>i.elim x f y = i.elim (x y) fun j => f j y
<VAR>α : Type u<VAR>ι : Type v<VAR>a : Cardinal.{u}<VAR>inst✝¹ : Countable ι<VAR>f : ι → Set α<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i<VAR>h'f : ∀ (i : ι), #↑(f i) ≤ a<GOAL>#α ≤ a
<VAR>α : Type u<VAR>ι : Type v<VAR>a : Cardinal.{u}<VAR>inst✝¹ : Countable ι<VAR>f : ι → Set α<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i<VAR>h'f : ∀ (i : ι), #↑(f i) ≤ a<GOAL>#↑Set.univ ≤ a
<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 g : ↥(Lp E p μ)<GOAL>edist f g = ENNReal.ofReal (dist f g)
<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>inst✝ : ConcreteCategory A<VAR>F G : Cᵒᵖ ⥤ A<VAR>f : F ⟶ G<GOAL>IsLocallySurjective J f ↔ IsLocallySurjective J (whiskerRight f (forget A))