ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommSemiring S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommSemiring P<VAR>N : Submonoid S<VAR>T : Type u_4<VAR>inst✝⁵ : CommSemiring T<VAR>inst✝⁴ : Algebra R T<VAR>inst✝³ : Algebra S T<VAR>inst✝² : IsScalarTower R S T<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : IsLocalization N T<VAR>H : ∀ (x : S), IsUnit x → x ∈ N<GOAL>Submonoid.comap (algebraMap R S) N = localizationLocalizationSubmodule M N
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommSemiring S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommSemiring P<VAR>N : Submonoid S<VAR>T : Type u_4<VAR>inst✝⁵ : CommSemiring T<VAR>inst✝⁴ : Algebra R T<VAR>inst✝³ : Algebra S T<VAR>inst✝² : IsScalarTower R S T<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : IsLocalization N T<VAR>H : ∀ (x : S), IsUnit x → x ∈ N<GOAL>N ⊔ Submonoid.map (algebraMap R S) M = N
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommSemiring S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommSemiring P<VAR>N : Submonoid S<VAR>T : Type u_4<VAR>inst✝⁵ : CommSemiring T<VAR>inst✝⁴ : Algebra R T<VAR>inst✝³ : Algebra S T<VAR>inst✝² : IsScalarTower R S T<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : IsLocalization N T<VAR>H : ∀ (x : S), IsUnit x → x ∈ N<GOAL>Submonoid.map (algebraMap R S) M ≤ N
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommSemiring S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommSemiring P<VAR>N : Submonoid S<VAR>T : Type u_4<VAR>inst✝⁵ : CommSemiring T<VAR>inst✝⁴ : Algebra R T<VAR>inst✝³ : Algebra S T<VAR>inst✝² : IsScalarTower R S T<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : IsLocalization N T<VAR>H : ∀ (x : S), IsUnit x → x ∈ N<VAR>x : R<VAR>hx : x ∈ ↑M<GOAL>(algebraMap R S) x ∈ N
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : NormedAddCommGroup D<VAR>inst✝⁴ : NormedSpace ℝ D<VAR>inst✝³ : MeasurableSpace D<VAR>inst✝² : BorelSpace D<VAR>inst✝¹ : SecondCountableTopology D<VAR>inst✝ : FiniteDimensional ℝ D<VAR>μ : Measure D<VAR>h : μ.HasTemperateGrowth<GOAL>Integrable (fun x => (1 + ‖x‖) ^ (-↑μ.integrablePower)) μ
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>s t : Set α<VAR>a x y : α<VAR>inst✝¹ : AlexandrovDiscrete α<VAR>inst✝ : AlexandrovDiscrete β<GOAL>exterior s ⊆ s ↔ IsOpen s
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>x : E<VAR>r : ℝ<VAR>hr : r ≠ 0<GOAL>frontier (sphere x r) = sphere x r
<VAR>B : Type u<VAR>inst✝ : Bicategory B<VAR>a b c d e : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<GOAL>(α_ f (𝟙 b) g).inv ≫ (ρ_ f).hom ▷ g = f ◁ (λ_ g).hom
<VAR>B : Type u₁<VAR>inst✝¹ : Bicategory B<VAR>C : Type u₂<VAR>inst✝ : Bicategory C<VAR>F G H : OplaxFunctor B C<VAR>η : OplaxNatTrans F G<VAR>θ : OplaxNatTrans G H<VAR>a b c : B<VAR>a' : C<VAR>f g : a ⟶ b<VAR>β : f ⟶ g<VAR>h : G.obj b ⟶ a'<GOAL>F.map₂ β ▷ η.app b ▷ h ≫ η.naturality g ▷ h = η.naturality f ▷ h ≫ (α_ (η.app a) (G.map f) h).hom ≫ η.app a ◁ G.map₂ β ▷ h ≫ (α_ (η.app a) (G.map g) h).inv
<VAR>α β : Type u<VAR>n : ℕ<GOAL>#(ULift.{u, 0} (Fin (n + 1))) = #(ULift.{u, 0} (Fin n)) + 1
<VAR>α β : Type u<VAR>n : ℕ<GOAL>↑(Fintype.card (ULift.{u, 0} (Fin (n + 1)))) = ↑(Fintype.card (Option (ULift.{u, 0} (Fin n))))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : LinearOrderedCommSemiring β<VAR>inst✝¹ : ExistsAddOfLE β<VAR>𝒜✝ ℬ✝ : Finset (Finset α)<VAR>a : α<VAR>f f₁ f₂ f₃ f₄ g μ : Finset α → β<VAR>s t u : Finset α<VAR>inst✝ : Fintype α<VAR>h₁ : 0 ≤ f₁<VAR>h₂ : 0 ≤ f₂<VAR>h₃ : 0 ≤ f₃<VAR>h₄ : 0 ≤ f₄<VAR>h : ∀ (s t : Finset α), f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)<VAR>𝒜 ℬ : Finset (Finset α)<GOAL>(∑ s ∈ 𝒜, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) * ∑ s ∈ 𝒜 ⊻ ℬ, f₄ s
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>(fun x => -x⁻¹ / log x ^ 2) = fun x => (-x * log x ^ 2)⁻¹
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>(fun x => (-x * log x ^ 2)⁻¹) =o[atTop] fun x => (x * 1)⁻¹
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>(fun x => x * 1) =o[atTop] fun x => -x * log x ^ 2
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∀ᶠ (x : ℝ) in atTop, x * 1 = 0 → -x * log x ^ 2 = 0
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i j : ι<VAR>x y : F<VAR>hxy : x ≠ y<GOAL>basisDivisor x y + basisDivisor y x = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : α → β<VAR>s✝ t : Set α<VAR>f : α → β<VAR>s : Set α<VAR>H : Injective f<GOAL>Disjoint (f '' s) (f '' sᶜ)
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>c : Set (E →ₗ.[R] F)<VAR>hc : DirectedOn (fun x x_1 => x ≤ x_1) c<GOAL>∃ f, { domain := sSup (domain '' c), toFun := f } ∈ upperBounds c
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>c : Set (E →ₗ.[R] F)<VAR>hc : DirectedOn (fun x x_1 => x ≤ x_1) c<VAR>ceq : c = ∅<GOAL>∃ f, { domain := sSup (domain '' c), toFun := f } ∈ upperBounds c
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>c : Set (E →ₗ.[R] F)<VAR>hc : DirectedOn (fun x x_1 => x ≤ x_1) c<VAR>cne : c.Nonempty<GOAL>∃ f, { domain := sSup (domain '' c), toFun := f } ∈ upperBounds c
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>c : Set (E →ₗ.[R] F)<VAR>hc : DirectedOn (fun x x_1 => x ≤ x_1) c<VAR>cne : c.Nonempty<VAR>hdir : DirectedOn (fun x x_1 => x ≤ x_1) (domain '' c)<GOAL>∃ f, { domain := sSup (domain '' c), toFun := f } ∈ upperBounds c
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>c : Set (E →ₗ.[R] F)<VAR>hc : DirectedOn (fun x x_1 => x ≤ x_1) c<VAR>cne : c.Nonempty<VAR>hdir : DirectedOn (fun x x_1 => x ≤ x_1) (domain '' c)<VAR>P : (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }<GOAL>∃ f, { domain := sSup (domain '' c), toFun := f } ∈ upperBounds c
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>c : Set (E →ₗ.[R] F)<VAR>hc : DirectedOn (fun x x_1 => x ≤ x_1) c<VAR>cne : c.Nonempty<VAR>hdir : DirectedOn (fun x x_1 => x ≤ x_1) (domain '' c)<VAR>P : (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }<VAR>f : ↥(sSup (domain '' c)) → F := fun x => ↑↑↑(P x) ⟨↑x, ⋯⟩<GOAL>∃ f, { domain := sSup (domain '' c), toFun := f } ∈ upperBounds c
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>c : Set (E →ₗ.[R] F)<VAR>hc : DirectedOn (fun x x_1 => x ≤ x_1) c<VAR>cne : c.Nonempty<VAR>hdir : DirectedOn (fun x x_1 => x ≤ x_1) (domain '' c)<VAR>P : (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }<VAR>f : ↥(sSup (domain '' c)) → F := fun x => ↑↑↑(P x) ⟨↑x, ⋯⟩<VAR>f_eq : ∀ (p : ↑c) (x : ↥(sSup (domain '' c))) (y : ↥(↑p).domain), ↑x = ↑y → f x = ↑↑p y<GOAL>∃ f, { domain := sSup (domain '' c), toFun := f } ∈ upperBounds c
<VAR>α : Type u_1<VAR>b : Bool<VAR>l : Lists' α b<GOAL>0 < sizeOf l
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>p : ℝ≥0∞<VAR>G : Type u_5<VAR>F' : Type u_6<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>m✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : DecidablePred fun x => x ≠ 0<VAR>m : MeasurableSpace α<VAR>f : α →ₛ F<VAR>μ : Measure α<GOAL>integral μ f = ∑ x ∈ filter (fun x => x ≠ 0) f.range, (μ (↑f ⁻¹' {x})).toReal • x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>p : ℝ≥0∞<VAR>G : Type u_5<VAR>F' : Type u_6<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>m✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : DecidablePred fun x => x ≠ 0<VAR>m : MeasurableSpace α<VAR>f : α →ₛ F<VAR>μ : Measure α<GOAL>∑ x ∈ filter (fun x => x ≠ 0) f.range, (weightedSMul μ (↑f ⁻¹' {x})) x = ∑ x ∈ filter (fun x => x ≠ 0) f.range, (μ (↑f ⁻¹' {x})).toReal • x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>p : ℝ≥0∞<VAR>G : Type u_5<VAR>F' : Type u_6<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>m✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : DecidablePred fun x => x ≠ 0<VAR>m : MeasurableSpace α<VAR>f : α →ₛ F<VAR>μ : Measure α<GOAL>∑ x ∈ filter (fun x => x ≠ 0) f.range, (μ (↑f ⁻¹' {x})).toReal • x = ∑ x ∈ filter (fun x => x ≠ 0) f.range, (μ (↑f ⁻¹' {x})).toReal • x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝² : Monoid M<VAR>inst✝¹ : AddMonoid N<VAR>M' : Type u_3<VAR>inst✝ : Monoid M'<VAR>P : Submonoid M<VAR>e : M →* M'<VAR>he : Function.Injective ⇑e<VAR>s : Finset M'<VAR>hs : closure ↑s = Submonoid.map e P<GOAL>P.FG
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝² : Monoid M<VAR>inst✝¹ : AddMonoid N<VAR>M' : Type u_3<VAR>inst✝ : Monoid M'<VAR>P : Submonoid M<VAR>e : M →* M'<VAR>he : Function.Injective ⇑e<VAR>s : Finset M'<VAR>hs : closure ↑s = Submonoid.map e P<GOAL>closure ↑(s.preimage ⇑e ⋯) = P
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝² : Monoid M<VAR>inst✝¹ : AddMonoid N<VAR>M' : Type u_3<VAR>inst✝ : Monoid M'<VAR>P : Submonoid M<VAR>e : M →* M'<VAR>he : Function.Injective ⇑e<VAR>s : Finset M'<VAR>hs : closure ↑s = Submonoid.map e P<GOAL>Submonoid.map e (closure ↑(s.preimage ⇑e ⋯)) = Submonoid.map e P
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝² : Monoid M<VAR>inst✝¹ : AddMonoid N<VAR>M' : Type u_3<VAR>inst✝ : Monoid M'<VAR>P : Submonoid M<VAR>e : M →* M'<VAR>he : Function.Injective ⇑e<VAR>s : Finset M'<VAR>hs : closure ↑s = Submonoid.map e P<GOAL>closure (⇑e '' (⇑e ⁻¹' ↑s)) = closure ↑s
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝² : Monoid M<VAR>inst✝¹ : AddMonoid N<VAR>M' : Type u_3<VAR>inst✝ : Monoid M'<VAR>P : Submonoid M<VAR>e : M →* M'<VAR>he : Function.Injective ⇑e<VAR>s : Finset M'<VAR>hs : closure ↑s = Submonoid.map e P<GOAL>⇑e '' (⇑e ⁻¹' ↑s) = ↑s
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝² : Monoid M<VAR>inst✝¹ : AddMonoid N<VAR>M' : Type u_3<VAR>inst✝ : Monoid M'<VAR>P : Submonoid M<VAR>e : M →* M'<VAR>he : Function.Injective ⇑e<VAR>s : Finset M'<VAR>hs : closure ↑s = Submonoid.map e P<GOAL>Submonoid.map e P ≤ Submonoid.map e ⊤
<VAR>α : Type u<VAR>inst✝ : DivisionRing α<VAR>x : α<VAR>h : x ≠ 1<VAR>n : ℕ<GOAL>∑ i ∈ range n, x ^ i = (x ^ n - 1) / (x - 1)
<VAR>α : Type u<VAR>inst✝ : DivisionRing α<VAR>x : α<VAR>h : x ≠ 1<VAR>n : ℕ<VAR>this : x - 1 ≠ 0<GOAL>∑ i ∈ range n, x ^ i = (x ^ n - 1) / (x - 1)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ¬p₃ = p₂<GOAL>∡ p₁ p₂ (midpoint ℝ p₃ p₂) = ∡ p₁ p₂ p₃
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CommMonoid β<VAR>s t : Multiset α<VAR>a : α<VAR>m : Multiset ι<VAR>f g : ι → α<VAR>h : ∀ x ∈ s, x = 1<GOAL>s.prod = 1
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CommMonoid β<VAR>s t : Multiset α<VAR>a : α<VAR>m : Multiset ι<VAR>f g : ι → α<VAR>l : List α<VAR>h : ∀ x ∈ ⟦l⟧, x = 1<GOAL>prod ⟦l⟧ = 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>𝔸' : Type u_8<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedCommRing 𝔸'<VAR>inst✝¹ : NormedAlgebra 𝕜 𝔸<VAR>inst✝ : NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>f : ι → E → 𝔸<VAR>f' : ι → E →L[𝕜] 𝔸<VAR>g : ι → E → 𝔸'<VAR>g' : ι → E →L[𝕜] 𝔸'<VAR>n : ℕ<VAR>x : Fin n → 𝔸<GOAL>∀ i ∈ Finset.univ, (List.map x (List.take (↑i) (List.finRange n))).prod • (proj ((List.finRange n).get i)).smulRight (List.map x (List.drop (↑i).succ (List.finRange n))).prod = (List.map x (List.take (↑((finCongr ⋯) i)) (List.finRange n))).prod • (proj ((finCongr ⋯) i)).smulRight (List.map x (List.drop (↑((finCongr ⋯) i)).succ (List.finRange n))).prod
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>K✝ : ℝ≥0<VAR>s t : Set α<VAR>f : α → β<VAR>hf : LocallyLipschitzOn t f<VAR>h : s ⊆ t<VAR>x : α<VAR>hx : x ∈ s<VAR>K : ℝ≥0<VAR>u : Set α<VAR>hu : u ∈ 𝓝[t] x<VAR>hfu : LipschitzOnWith K f u<GOAL>∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>F F' : C ⥤ D<VAR>G : D ⥤ E<VAR>inst✝ : F.Full<VAR>α : F ≅ F'<VAR>X Y : C<VAR>f : F'.obj X ⟶ F'.obj Y<GOAL>F'.map (F.preimage ((α.app X).hom ≫ f ≫ (α.app Y).inv)) = f
<VAR>p : ℝ≥0∞<VAR>h : p ≤ 1<VAR>i : Fin (1 + 1)<GOAL>(binomial p h 1) i = (map (fun x => bif x then 1 else 0) (bernoulli p h)) i
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I✝ : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>f : InfinitePlace K → ℝ≥0<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>B : ℝ<VAR>h : minkowskiBound K 1 ≤ volume (convexBodySum K B)<GOAL>∃ a, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) ↑a| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I✝ : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>f : InfinitePlace K → ℝ≥0<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>B : ℝ<VAR>h : minkowskiBound K 1 ≤ volume (convexBodySum K B)<VAR>w✝ : K<VAR>h_mem : w✝ ∈ ↑1<VAR>h_nz : w✝ ≠ 0<VAR>h_bd : ↑|(Algebra.norm ℚ) w✝| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K<GOAL>∃ a, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) ↑a| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I✝ : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>f : InfinitePlace K → ℝ≥0<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>B : ℝ<VAR>h : minkowskiBound K 1 ≤ volume (convexBodySum K B)<VAR>a : 𝓞 K<VAR>h_mem : (algebraMap (𝓞 K) K) a ∈ ↑1<VAR>h_nz : (algebraMap (𝓞 K) K) a ≠ 0<VAR>h_bd : ↑|(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a)| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K<GOAL>∃ a, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) ↑a| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>inst✝⁵ : CommSemiring k<VAR>inst✝⁴ : Monoid G<VAR>inst✝³ : AddCommMonoid V<VAR>inst✝² : Module k V<VAR>ρ : Representation k G V<VAR>M : Type u_4<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module (MonoidAlgebra k G) M<VAR>r : MonoidAlgebra k G<VAR>m : (ofModule M).asModule<GOAL>(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) (((ofModule M).asAlgebraHom r) ((ofModule M).asModuleEquiv m)) = r • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) ((ofModule M).asModuleEquiv m)
<VAR>P : Type u_1<VAR>inst✝ : SemilatticeInf P<VAR>x✝ y✝ : P<VAR>I : Ideal P<VAR>hI : I.IsPrime<VAR>x y : P<GOAL>x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
<VAR>P : Type u_1<VAR>inst✝ : SemilatticeInf P<VAR>x✝ y✝ : P<VAR>I : Ideal P<VAR>hI : I.IsPrime<VAR>x y : P<GOAL>x ∉ I ∧ y ∉ I → x ⊓ y ∉ I
<VAR>P : Type u_1<VAR>inst✝ : SemilatticeInf P<VAR>x✝ y✝ : P<VAR>I : Ideal P<VAR>hI : I.IsPrime<VAR>x y : P<VAR>F : PFilter P := ⋯.toPFilter<GOAL>x ∉ I ∧ y ∉ I → x ⊓ y ∉ I
<VAR>P : Type u_1<VAR>inst✝ : SemilatticeInf P<VAR>x✝ y✝ : P<VAR>I : Ideal P<VAR>hI : I.IsPrime<VAR>x y : P<VAR>F : PFilter P := ⋯.toPFilter<GOAL>x ∈ F ∧ y ∈ F → x ⊓ y ∈ F
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>inst✝⁵ : CommSemiring k<VAR>inst✝⁴ : Group G<VAR>inst✝³ : AddCommMonoid V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AddCommMonoid W<VAR>inst✝ : Module k W<VAR>ρV : Representation k G V<VAR>ρW : Representation k G W<VAR>g : G<VAR>x✝² : Module.Dual k V<VAR>x✝¹ : W<VAR>x✝ : V<GOAL>(((TensorProduct.AlgebraTensorModule.curry (dualTensorHom k V W ∘ₗ TensorProduct.map (ρV.dual g) (ρW g))) x✝²) x✝¹) x✝ = (((TensorProduct.AlgebraTensorModule.curry ((ρV.linHom ρW) g ∘ₗ dualTensorHom k V W)) x✝²) x✝¹) x✝
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>p : α<VAR>hp : 0 < p<VAR>b : α<GOAL>toIcoMod ⋯ 0 b = Int.fract b
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : Invertible 2<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x✝ y✝ z x x' y y' : P<GOAL>midpoint R x y = midpoint R x' y' ↔ x -ᵥ x' = y' -ᵥ y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : BooleanAlgebra α<VAR>a b c d : α<GOAL>a ∆ b = ⊤ ↔ IsCompl a b
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H K : Subgroup G<VAR>nH : H.Normal<VAR>a b : G<VAR>h : a * b ∈ H<GOAL>b * a ∈ H
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H K : Subgroup G<VAR>nH : H.Normal<VAR>a b : G<VAR>h : a * b ∈ H<VAR>this : a⁻¹ * (a * b) * a⁻¹⁻¹ ∈ H<GOAL>b * a ∈ H
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>s : Set X<VAR>t : Set Y<VAR>x : X<VAR>y : Y<GOAL>e.IsImage s t ↔ e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s) = e.target ∩ t
<VAR>n : ℕ<GOAL>n.smoothNumbers = factoredNumbers (Finset.range n)
<VAR>ι : Type u_1<VAR>I : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : I → Type u_6<VAR>x y : (i : I) → f✝ i<VAR>i : I<VAR>inst✝¹ : One γ<VAR>inst✝ : LE γ<VAR>f : α → β<VAR>g : α → γ<VAR>e : β → γ<VAR>hg : g ≤ 1<VAR>he : e ≤ 1<VAR>_b : β<GOAL>extend f g e _b ≤ 1 _b
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_ne_one : b ≠ 1<VAR>hx : 0 < x<GOAL>b ^ logb b x = x
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_ne_one : b ≠ 1<VAR>hx : 0 < x<GOAL>|x| = 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>h : Differentiable 𝕜 fun y => c + f y<GOAL>Differentiable 𝕜 f
<VAR>n : ℕ<VAR>z : ℂ<VAR>hz : 1 + z ∈ slitPlane<GOAL>HasDerivAt (fun z => log (1 + z) - logTaylor (n + 1) z) ((-z) ^ n * (1 + z)⁻¹) z
<VAR>n : ℕ<VAR>z : ℂ<VAR>hz : 1 + z ∈ slitPlane<GOAL>(-z) ^ n * (1 + z)⁻¹ = (1 + z)⁻¹ - ∑ j ∈ Finset.range n, (-1) ^ j * z ^ j
<VAR>n : ℕ<VAR>z : ℂ<VAR>hz : 1 + z ∈ slitPlane<VAR>hz' : -z ≠ 1<GOAL>(-z) ^ n * (1 + z)⁻¹ = (1 + z)⁻¹ - ∑ j ∈ Finset.range n, (-1) ^ j * z ^ j
<VAR>n : ℕ<VAR>z : ℂ<VAR>hz : 1 + z ∈ slitPlane<VAR>hz' : -z ≠ 1<GOAL>(-z) ^ n * (1 + z)⁻¹ = (1 + z)⁻¹ - -(((-z) ^ n - 1) / (1 + z))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a b c : α<VAR>inst✝ : DecidableEq α<VAR>h : a < b<GOAL>Ico a b \ Ioo a b = {a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : α × β → ℝ≥0∞<VAR>hf : Measurable f<GOAL>Measurable fun a => ∫⁻ (b : β), f (a, b) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : α × β → ℝ≥0∞<VAR>hf : Measurable f<GOAL>Measurable (uncurry fun a b => f (a, b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : α × β → ℝ≥0∞<VAR>hf : Measurable f<VAR>this : (uncurry fun a b => f (a, b)) = f<GOAL>Measurable (uncurry fun a b => f (a, b))
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : FunLike F G H<VAR>a : G<VAR>b : H<VAR>inst✝² : AddMonoid G<VAR>inst✝¹ : AddMonoid H<VAR>inst✝ : AddConstMapClass F G H a b<VAR>f : F<VAR>n : ℕ<GOAL>f (n • a) = f 0 + n • b
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup X<VAR>inst✝² : NormedSpace ℝ X<VAR>inst✝¹ : HasContDiffBump E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<VAR>n : ℕ∞<VAR>inst✝ : FiniteDimensional ℝ E<GOAL>HasCompactSupport ↑f
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>x y : α × β<VAR>h₁ : x.1 < y.1<VAR>h₂ : x.2 ≤ y.2<GOAL>x < y
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : Affine R<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>x y : R<GOAL>(map W f).toAffine.Equation (f x) (f y) ↔ W.Equation x y
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>ab : a ≠ b<VAR>l : List α<GOAL>count a (l.erase b) = count a l
<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 x (x + y) = ↑(Real.arccos (‖x‖ / ‖x + y‖))