ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>s : AffineSubspace ℝ P<VAR>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>x✝ : P<GOAL>(reflection s).symm x✝ = (reflection s) x✝
<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>s : AffineSubspace ℝ P<VAR>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>x✝ : P<GOAL>(reflection s) ((reflection s).symm x✝) = (reflection s) ((reflection s) x✝)
<VAR>θ : Angle<GOAL>θ.cos = 0 ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)
<VAR>α β : Type u<VAR>a : Cardinal.{u}<VAR>b : Cardinal.{v}<GOAL>lift.{max v w, u} a = lift.{max u w, v} b ↔ lift.{v, u} a = lift.{u, v} b
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<VAR>x✝ : ℕ<GOAL>Disjoint (closure ((fun x => univ) x✝)) ∅
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>inst✝ : l.NeBot<GOAL>Tendsto (fun x => r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>inst✝ : l.NeBot<VAR>hr : r < 0<GOAL>Tendsto (fun x => r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>inst✝ : l.NeBot<GOAL>Tendsto (fun x => 0 * f x) l atTop ↔ 0 < 0 ∧ Tendsto f l atTop ∨ 0 < 0 ∧ Tendsto f l atBot
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>inst✝ : l.NeBot<VAR>hr : 0 < r<GOAL>Tendsto (fun x => r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝¹⁰ : OrderedSemiring 𝕜<VAR>inst✝⁹ : TopologicalSpace E<VAR>inst✝⁸ : TopologicalSpace F<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module 𝕜 E<VAR>inst✝⁴ : Module 𝕜 F<VAR>inst✝³ : LinearOrderedField 𝕝<VAR>inst✝² : Module 𝕝 E<VAR>inst✝¹ : ContinuousConstSMul 𝕝 E<VAR>inst✝ : LinearMap.CompatibleSMul E E 𝕜 𝕝<VAR>s : Set E<VAR>x : E<VAR>hs : StrictConvex 𝕜 s<VAR>c : 𝕝<GOAL>StrictConvex 𝕜 (c • s)
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝¹⁰ : OrderedSemiring 𝕜<VAR>inst✝⁹ : TopologicalSpace E<VAR>inst✝⁸ : TopologicalSpace F<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module 𝕜 E<VAR>inst✝⁴ : Module 𝕜 F<VAR>inst✝³ : LinearOrderedField 𝕝<VAR>inst✝² : Module 𝕝 E<VAR>inst✝¹ : ContinuousConstSMul 𝕝 E<VAR>inst✝ : LinearMap.CompatibleSMul E E 𝕜 𝕝<VAR>s : Set E<VAR>x : E<VAR>hs : StrictConvex 𝕜 s<GOAL>StrictConvex 𝕜 (0 • s)
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝¹⁰ : OrderedSemiring 𝕜<VAR>inst✝⁹ : TopologicalSpace E<VAR>inst✝⁸ : TopologicalSpace F<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module 𝕜 E<VAR>inst✝⁴ : Module 𝕜 F<VAR>inst✝³ : LinearOrderedField 𝕝<VAR>inst✝² : Module 𝕝 E<VAR>inst✝¹ : ContinuousConstSMul 𝕝 E<VAR>inst✝ : LinearMap.CompatibleSMul E E 𝕜 𝕝<VAR>s : Set E<VAR>x : E<VAR>hs : StrictConvex 𝕜 s<VAR>c : 𝕝<VAR>hc : c ≠ 0<GOAL>StrictConvex 𝕜 (c • s)
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<GOAL>Continuous fun f i => if ord I i = o then true else f i
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<GOAL>∀ (i : I), Continuous fun a => if ord I i = o then true else a i
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>i : I<GOAL>Continuous fun a => if ord I i = o then true else a i
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>i : I<GOAL>Continuous (ite (ord I i = o) true)
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>i : I<GOAL>Continuous fun x => x i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o o' : Ordinal.{max u v}<VAR>f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}<VAR>hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj<VAR>g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}<VAR>hg : o'.blsub g = o<GOAL>(o'.bsup fun a ha => f (g a ha) ⋯) = o.bsup f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o o' : Ordinal.{max u v}<VAR>f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}<VAR>hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj<VAR>g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}<VAR>hg : o'.blsub g = o<VAR>i : Ordinal.{max u v}<VAR>hi : i < o'<GOAL>f (g i hi) ⋯ ≤ o.bsup f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o o' : Ordinal.{max u v}<VAR>f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}<VAR>hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj<VAR>g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}<VAR>hg : o'.blsub g = o<VAR>i : Ordinal.{max u v}<VAR>hi : i < o<GOAL>f i hi ≤ o'.bsup fun a ha => f (g a ha) ⋯
<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>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<GOAL>‖indicatorConstLp p hs hμs c‖ ≤ ‖c‖ * (μ s).toReal ^ (1 / p.toReal)
<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>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<GOAL>(eLpNorm (s.indicator fun x => c) p μ).toReal ≤ ‖c‖ * (μ s).toReal ^ (1 / p.toReal)
<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>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<GOAL>eLpNorm (s.indicator fun x => c) p μ ≤ ENNReal.ofReal (‖c‖ * (μ s).toReal ^ (1 / p.toReal))
<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>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<GOAL>↑‖c‖₊ * μ s ^ (1 / p.toReal) = ENNReal.ofReal (‖c‖ * (μ s).toReal ^ (1 / p.toReal))
<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>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<GOAL>μ s ^ (1 / p.toReal) ≠ ⊤
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : Algebra.IsAlgebraic K L<VAR>inst✝ : PerfectField K<VAR>f : L[X]<VAR>hf : Irreducible f<GOAL>f.Separable
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : Algebra.IsAlgebraic K L<VAR>inst✝ : PerfectField K<VAR>f : L[X]<VAR>hf : Irreducible f<VAR>w✝ : K[X]<VAR>left✝ : w✝.Monic<VAR>hi : Irreducible w✝<VAR>h : f ∣ map (algebraMap K L) w✝<GOAL>f.Separable
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>σ : Perm n<VAR>M : Matrix n n R<GOAL>(M.submatrix id ⇑σ).det = ↑↑(sign σ) * M.det
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝¹ : ConditionallyCompleteLattice α<VAR>s t : Set α<VAR>a b : α<VAR>inst✝ : SemilatticeSup β<VAR>f g : β → α<VAR>hf : Monotone f<VAR>hg : Antitone g<VAR>h : f ≤ g<GOAL>⨆ n, f n ∈ ⋂ n, Icc (f n) (g n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝¹ : ConditionallyCompleteLattice α<VAR>s t : Set α<VAR>a b : α<VAR>inst✝ : SemilatticeSup β<VAR>f g : β → α<VAR>hf : Monotone f<VAR>hg : Antitone g<VAR>h : f ≤ g<VAR>n : β<GOAL>⨆ n, f n ∈ Icc (f n) (g n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝¹ : ConditionallyCompleteLattice α<VAR>s t : Set α<VAR>a b : α<VAR>inst✝ : SemilatticeSup β<VAR>f g : β → α<VAR>hf : Monotone f<VAR>hg : Antitone g<VAR>h : f ≤ g<VAR>n : β<VAR>this : Nonempty β<GOAL>⨆ n, f n ∈ Icc (f n) (g n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝¹ : ConditionallyCompleteLattice α<VAR>s t : Set α<VAR>a b : α<VAR>inst✝ : SemilatticeSup β<VAR>f g : β → α<VAR>hf : Monotone f<VAR>hg : Antitone g<VAR>h : f ≤ g<VAR>n : β<VAR>this✝ : Nonempty β<VAR>this : ∀ (m : β), f m ≤ g n<GOAL>⨆ n, f n ∈ Icc (f n) (g n)
<VAR>a b✝ c d : ℝ≥0∞<VAR>r p q b : ℝ≥0<VAR>hb : 1 ≤ ↑r * ↑b<GOAL>r⁻¹ ≤ b
<VAR>a b✝ c d : ℝ≥0∞<VAR>r p q b : ℝ≥0<VAR>hb : 1 ≤ ↑r * ↑b<GOAL>1 ≤ r * b
<VAR>M : Type u_1<VAR>inst✝² : Zero M<VAR>l✝ : List M<VAR>inst✝¹ : DecidablePred fun x => l✝.getD x 0 ≠ 0<VAR>n : ℕ<VAR>R : Type u_2<VAR>inst✝ : AddMonoid R<VAR>l : List R<GOAL>∀ [inst : DecidablePred fun x => l.getD x 0 ≠ 0], l.toFinsupp = (map (fun nr => Finsupp.single nr.1 nr.2) l.enum).sum
<GOAL>2 * arctan 2⁻¹ - arctan 7⁻¹ = π / 4
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a✝ b✝ c d a b : α<VAR>h : Codisjoint a b<GOAL>a ⇔ b = a ⊓ b
<VAR>α β γ : Type u<VAR>m : Type u → Type v<VAR>inst✝¹ : Monad m<VAR>inst✝ : LawfulMonad m<VAR>x : m α<VAR>g : α → m β<VAR>f : β → γ<GOAL>f <$> (x >>= g) = do let a ← x f <$> g a
<VAR>α β γ : Type u<VAR>m : Type u → Type v<VAR>inst✝¹ : Monad m<VAR>inst✝ : LawfulMonad m<VAR>x : m α<VAR>g : α → m β<VAR>f : β → γ<GOAL>(do let x ← x let a ← g x pure (f a)) = do let a ← x f <$> g a
<VAR>α : Type u<VAR>inst✝¹ : Monoid α<VAR>a b : α<VAR>inst✝ : Invertible a<GOAL>⅟a * (a * b) = b
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<GOAL>X.content = 1
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>p : Perm α<VAR>x : α<GOAL>toList 1 x = []
<VAR>R : Type u_1<VAR>inst✝ : Rack R<VAR>x y z : R<GOAL>x ◃⁻¹ y ◃⁻¹ z = (x ◃⁻¹ y) ◃⁻¹ x ◃⁻¹ z
<VAR>R : Type u_1<VAR>inst✝ : Rack R<VAR>x y z : R<GOAL>(x ◃ x ◃⁻¹ y) ◃ x ◃ x ◃⁻¹ y ◃⁻¹ z = z
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>hs₂ : s₂.Nonempty<VAR>ht₂ : t₂.Nonempty<GOAL>↑s₂.card / ↑s₁.card * (↑t₂.card / ↑t₁.card) * edgeDensity r s₂ t₂ ≤ edgeDensity r s₁ t₁
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>hs₂ : s₂.Nonempty<VAR>ht₂ : t₂.Nonempty<VAR>hst : ↑s₂.card * ↑t₂.card ≠ 0<GOAL>↑s₂.card / ↑s₁.card * (↑t₂.card / ↑t₁.card) * edgeDensity r s₂ t₂ ≤ edgeDensity r s₁ t₁
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>hs₂ : s₂.Nonempty<VAR>ht₂ : t₂.Nonempty<VAR>hst : ↑s₂.card * ↑t₂.card ≠ 0<GOAL>↑(interedges r s₂ t₂).card / (↑s₁.card * ↑t₁.card) ≤ ↑(interedges r s₁ t₁).card / (↑s₁.card * ↑t₁.card)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>hs₂ : s₂.Nonempty<VAR>ht₂ : t₂.Nonempty<VAR>hst : ↑s₂.card * ↑t₂.card ≠ 0<GOAL>interedges r s₂ t₂ ⊆ interedges r s₁ t₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝² : Zero M<VAR>inst✝¹ : Zero N<VAR>inst✝ : Zero P<VAR>f : M → N<VAR>hf : f 0 = 0<VAR>x✝ : α<GOAL>(mapRange f hf 0) x✝ = 0 x✝
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>x✝¹ : NonAssocSemiring α<VAR>x✝ : NonAssocSemiring β<VAR>f : α →+* β<VAR>x y : α<GOAL>0 = 1 ↔ f 1 = 0
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>c w : ℂ<VAR>R : ℝ<VAR>hw : w ∈ ball c R<GOAL>(∮ (z : ℂ) in C(c, R), (z - w)⁻¹) = 2 * ↑π * I
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>c w : ℂ<VAR>R : ℝ<VAR>hw : w ∈ ball c R<VAR>hR : 0 < R<GOAL>(∮ (z : ℂ) in C(c, R), (z - w)⁻¹) = 2 * ↑π * I
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>c w : ℂ<VAR>R : ℝ<VAR>hw : w ∈ ball c R<VAR>hR : 0 < R<GOAL>HasSum (fun n => ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * ↑π * I)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>c w : ℂ<VAR>R : ℝ<VAR>hw : w ∈ ball c R<VAR>hR : 0 < R<VAR>H : ∀ (n : ℕ), n ≠ 0 → (∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1)) = 0<GOAL>HasSum (fun n => ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * ↑π * I)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>c w : ℂ<VAR>R : ℝ<VAR>hw : w ∈ ball c R<VAR>hR : 0 < R<VAR>H : ∀ (n : ℕ), n ≠ 0 → (∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1)) = 0<VAR>this : (∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹) = 2 * ↑π * I<GOAL>HasSum (fun n => ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * ↑π * I)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>c w : ℂ<VAR>R : ℝ<VAR>hw : w ∈ ball c R<VAR>hR : 0 < R<VAR>H : ∀ (n : ℕ), n ≠ 0 → (∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1)) = 0<VAR>this : (∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹) = 2 * ↑π * I<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>(∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) = 0
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>c w : ℂ<VAR>R : ℝ<VAR>hw : w ∈ ball c R<VAR>hR : 0 < R<VAR>H : ∀ (n : ℕ), n ≠ 0 → (∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1)) = 0<VAR>this : (∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹) = 2 * ↑π * I<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>((w - c) ^ n * ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n * (z - c)⁻¹) = 0
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>c w : ℂ<VAR>R : ℝ<VAR>hw : w ∈ ball c R<VAR>hR : 0 < R<VAR>H : ∀ (n : ℕ), n ≠ 0 → (∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1)) = 0<VAR>this : (∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹) = 2 * ↑π * I<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>∀ z ∈ sphere c R, (z - c)⁻¹ ^ n * (z - c)⁻¹ = (z - c) ^ (-↑n - 1)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>c w : ℂ<VAR>R : ℝ<VAR>hw : w ∈ ball c R<VAR>hR : 0 < R<VAR>H : ∀ (n : ℕ), n ≠ 0 → (∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1)) = 0<VAR>this : (∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹) = 2 * ↑π * I<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>z : ℂ<VAR>hz✝ : z ∈ sphere c R<GOAL>(z - c)⁻¹ ^ n * (z - c)⁻¹ = (z - c) ^ (-↑n - 1)
<VAR>x y z✝ : ℝ<VAR>n : ℕ<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<VAR>z : ℝ<GOAL>(x / y) ^ z = x ^ z / y ^ z
<VAR>X✝ Y Z : Scheme<VAR>𝒰✝ : X✝.OpenCover<VAR>f✝ : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f✝) g<VAR>X W : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : W ⟶ X<VAR>x : ↑↑W.toPresheafedSpace<GOAL>x ∈ Set.range ⇑((fun x => pullback.fst f (𝒰.map x)) ((fun x => 𝒰.f (f.val.base x)) x)).val.base
<VAR>X✝ Y Z : Scheme<VAR>𝒰✝ : X✝.OpenCover<VAR>f✝ : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f✝) g<VAR>X W : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : W ⟶ X<VAR>x : ↑↑W.toPresheafedSpace<GOAL>x ∈ Set.range ⇑((PreservesPullback.iso forgetToTop f (𝒰.map (𝒰.f (f.val.base x)))).hom ≫ pullback.fst (forgetToTop.map f) (forgetToTop.map (𝒰.map (𝒰.f (f.val.base x)))))
<VAR>X✝ Y Z : Scheme<VAR>𝒰✝ : X✝.OpenCover<VAR>f✝ : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f✝) g<VAR>X W : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : W ⟶ X<VAR>x : ↑↑W.toPresheafedSpace<GOAL>x ∈ {x_1 | ∃ y, (forgetToTop.map f) x_1 = (forgetToTop.map (𝒰.map (𝒰.f (f.val.base x)))) y}
<VAR>X✝ Y Z : Scheme<VAR>𝒰✝ : X✝.OpenCover<VAR>f✝ : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f✝) g<VAR>X W : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : W ⟶ X<VAR>x : ↑↑W.toPresheafedSpace<GOAL>Function.Surjective ⇑(PreservesPullback.iso forgetToTop f (𝒰.map (𝒰.f (f.val.base x)))).hom
<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✝⁵ : NonUnitalNonAssocSemiring α<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Monoid R<VAR>inst✝² : NonUnitalNonAssocSemiring S<VAR>inst✝¹ : DistribMulAction R S<VAR>inst✝ : IsScalarTower R S S<VAR>M : Matrix n m S<VAR>b : R<VAR>v : n → S<VAR>i : m<GOAL>((b • v) ᵥ* M) i = (b • v ᵥ* M) i
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝⁶ : NormedField 𝕜<VAR>inst✝⁵ : NormedRing 𝕝<VAR>inst✝⁴ : NormedSpace 𝕜 𝕝<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : SMulWithZero 𝕝 E<VAR>inst✝ : IsScalarTower 𝕜 𝕝 E<VAR>s t u v A B : Set E<VAR>x : E<VAR>a✝ b✝ : 𝕜<VAR>hs : Balanced 𝕝 s<VAR>a : 𝕝<VAR>b : 𝕜<VAR>h : ‖a‖ ≤ ‖b‖<GOAL>a • s ⊆ b • s
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝⁶ : NormedField 𝕜<VAR>inst✝⁵ : NormedRing 𝕝<VAR>inst✝⁴ : NormedSpace 𝕜 𝕝<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : SMulWithZero 𝕝 E<VAR>inst✝ : IsScalarTower 𝕜 𝕝 E<VAR>s t u v A B : Set E<VAR>x : E<VAR>a✝ b : 𝕜<VAR>hs : Balanced 𝕝 s<VAR>a : 𝕝<VAR>h : ‖a‖ ≤ ‖0‖<GOAL>a • s ⊆ 0 • s
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝⁶ : NormedField 𝕜<VAR>inst✝⁵ : NormedRing 𝕝<VAR>inst✝⁴ : NormedSpace 𝕜 𝕝<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : SMulWithZero 𝕝 E<VAR>inst✝ : IsScalarTower 𝕜 𝕝 E<VAR>s t u v A B : Set E<VAR>x : E<VAR>a✝ b✝ : 𝕜<VAR>hs : Balanced 𝕝 s<VAR>a : 𝕝<VAR>b : 𝕜<VAR>h : ‖a‖ ≤ ‖b‖<VAR>hb : b ≠ 0<GOAL>a • s ⊆ b • s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : AddMonoidWithOne α<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : ZeroLEOneClass α<VAR>inst✝ : CharZero α<VAR>m n : ℕ<GOAL>1 < ↑n ↔ 1 < n
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝²⁵ : CommRing R<VAR>inst✝²⁴ : CommRing S<VAR>inst✝²³ : Algebra R S<VAR>P : Generators R S<VAR>R' : Type ?u.724724<VAR>S' : Type ?u.724727<VAR>inst✝²² : CommRing R'<VAR>inst✝²¹ : CommRing S'<VAR>inst✝²⁰ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝¹⁹ : Algebra R R'<VAR>inst✝¹⁸ : Algebra S S'<VAR>inst✝¹⁷ : Algebra R S'<VAR>inst✝¹⁶ : IsScalarTower R R' S'<VAR>inst✝¹⁵ : IsScalarTower R S S'<VAR>R'' : Type ?u.727158<VAR>S'' : Type ?u.727161<VAR>inst✝¹⁴ : CommRing R''<VAR>inst✝¹³ : CommRing S''<VAR>inst✝¹² : Algebra R'' S''<VAR>P'' : Generators R'' S''<VAR>inst✝¹¹ : Algebra R R''<VAR>inst✝¹⁰ : Algebra S S''<VAR>inst✝⁹ : Algebra R S''<VAR>inst✝⁸ : IsScalarTower R R'' S''<VAR>inst✝⁷ : IsScalarTower R S S''<VAR>inst✝⁶ : Algebra R' R''<VAR>inst✝⁵ : Algebra S' S''<VAR>inst✝⁴ : Algebra R' S''<VAR>inst✝³ : IsScalarTower R' R'' S''<VAR>inst✝² : IsScalarTower R' S' S''<VAR>inst✝¹ : IsScalarTower R R' R''<VAR>inst✝ : IsScalarTower S S' S''<VAR>r : R<VAR>x : P.Cotangent<GOAL>(r • x).val = r • x.val
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → ℂ<VAR>s : Set ℝ<VAR>x : ℝ<VAR>f' : ℂ<VAR>h₁ : HasDerivWithinAt f f' s x<VAR>h₂ : f x ∈ slitPlane<GOAL>HasDerivWithinAt (fun t => log (f t)) (f' / f x) s x
<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<GOAL>IsPrincipalIdealRing (𝓞 K)
<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<GOAL>↑|discr K| < (2 * (π / 4) ^ NrComplexPlaces K * (↑(FiniteDimensional.finrank ℚ K) ^ FiniteDimensional.finrank ℚ K / ↑(FiniteDimensional.finrank ℚ K)!)) ^ 2
<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<GOAL>↑|(-1) ^ ((↑3 - 1) / 2) * ↑↑3 ^ (↑3 - 2)| < (2 * (π / 4) ^ ((↑3 - 1) / 2) * (↑(↑3 - 1) ^ (↑3 - 1) / ↑(↑3 - 1)!)) ^ 2
<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<GOAL>3 < (2 * (π / 4) * (2 ^ 2 / 2)) ^ 2
<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<GOAL>(2 * (3 / 4) * (2 ^ 2 / 2)) ^ 2 < (2 * (π / 4) * (2 ^ 2 / 2)) ^ 2
<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<GOAL>3 < π
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝¹³ : CommSemiring R✝<VAR>inst✝¹² : NonUnitalRing A✝<VAR>inst✝¹¹ : Module R✝ A✝<VAR>inst✝¹⁰ : IsScalarTower R✝ A✝ A✝<VAR>inst✝⁹ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁸ : Semifield R<VAR>inst✝⁷ : Field S<VAR>inst✝⁶ : NonUnitalRing A<VAR>inst✝⁵ : Module R A<VAR>inst✝⁴ : Module S A<VAR>inst✝³ : IsScalarTower S A A<VAR>inst✝² : SMulCommClass S A A<VAR>inst✝¹ : Algebra R S<VAR>a : A<VAR>f : S → R<VAR>inst✝ : IsScalarTower R S A<VAR>h : QuasispectrumRestricts a f<GOAL>f '' quasispectrum S a = quasispectrum R a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H✝ : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : AddZeroClass M<VAR>inst✝ : MulOneClass N<VAR>f g : Multiplicative (α →₀ M) →* N<VAR>H : ∀ (x : α) (y : M), f (Multiplicative.ofAdd (single x y)) = g (Multiplicative.ofAdd (single x y))<GOAL>f = g