ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field K<VAR>inst✝² inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {n} ℚ K<VAR>hno : Odd ↑n<VAR>ζ x : K<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>hx : IsOfFinOrder x<VAR>hnegζ : IsPrimitiveRoot (-ζ) (2 * ↑n)<VAR>k : ℕ<VAR>hkpos : 0 < k<VAR>hkn : x ^ k = 1<VAR>l : ℕ<VAR>hl : l ∈ k.divisors<VAR>hlzero : NeZero l<VAR>this : NeZero ↑l<VAR>a : ℕ<VAR>ha : 2 * ↑n = l * a<VAR>hlroot : x ^ (2 * ↑n) = 1<GOAL>∃ r, x = (-ζ) ^ r
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field K<VAR>inst✝² inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {n} ℚ K<VAR>hno : Odd ↑n<VAR>ζ x : K<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>hx : IsOfFinOrder x<VAR>hnegζ : IsPrimitiveRoot (-ζ) (2 * ↑n)<VAR>k : ℕ<VAR>hkpos : 0 < k<VAR>hkn : x ^ k = 1<VAR>l : ℕ<VAR>hl : l ∈ k.divisors<VAR>hlzero : NeZero l<VAR>this : NeZero ↑l<VAR>a : ℕ<VAR>ha : 2 * ↑n = l * a<VAR>hlroot : x ^ (2 * ↑n) = 1<VAR>s : ℕ<VAR>hs : (-ζ) ^ s = x<GOAL>∃ r, x = (-ζ) ^ r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ζ : Type u_6<VAR>r : α → α → Prop<VAR>a b : α<VAR>h✝ : Equivalence r<VAR>h : EqvGen r a b<GOAL>r a b
<VAR>f : ℕ → ℂ<VAR>l : ℂ<VAR>h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i<GOAL>Tendsto (fun n => (1 - z) * ∑ i ∈ range n, (l - ∑ j ∈ range (i + 1), f j) * z ^ i) atTop (𝓝 (l - ∑' (n : ℕ), f n * z ^ n))
<VAR>f : ℕ → ℂ<VAR>l : ℂ<VAR>h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i<VAR>k : Tendsto (fun x => ∑ i ∈ range x, f i - ∑ i ∈ range x, f i * z ^ i) atTop (𝓝 (l - ∑' (b : ℕ), f b * z ^ b))<GOAL>Tendsto (fun n => (1 - z) * ∑ i ∈ range n, (l - ∑ j ∈ range (i + 1), f j) * z ^ i) atTop (𝓝 (l - ∑' (n : ℕ), f n * z ^ n))
<VAR>f : ℕ → ℂ<VAR>l : ℂ<VAR>h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i<VAR>k : Tendsto (fun x => (1 - z) * ∑ x_1 ∈ range x, (∑ i ∈ Ico (x_1 + 1) x, f i) * z ^ x_1) atTop (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))<GOAL>Tendsto (fun n => (1 - z) * ∑ i ∈ range n, (l - ∑ j ∈ range (i + 1), f j) * z ^ i) atTop (𝓝 (l - ∑' (n : ℕ), f n * z ^ n))
<VAR>f : ℕ → ℂ<VAR>l : ℂ<VAR>h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i<VAR>k : Tendsto (fun n => (1 - z) * ∑ j ∈ range n, (∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k) * z ^ j) atTop (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))<GOAL>Tendsto (fun n => (1 - z) * ∑ i ∈ range n, (l - ∑ j ∈ range (i + 1), f j) * z ^ i) atTop (𝓝 (l - ∑' (n : ℕ), f n * z ^ n))
<VAR>f : ℕ → ℂ<VAR>l : ℂ<VAR>h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i<VAR>k : Tendsto (fun n => (1 - z) * ∑ j ∈ range n, (∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k) * z ^ j) atTop (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))<GOAL>Tendsto (fun n => (l - s n) * ∑ i ∈ range n, z ^ i) atTop (𝓝 0)
<VAR>f : ℕ → ℂ<VAR>l : ℂ<VAR>h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i<VAR>k : Tendsto (fun n => (1 - z) * ∑ j ∈ range n, (∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k) * z ^ j) atTop (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))<GOAL>Tendsto (fun n => (l - s n) * ∑ i ∈ range n, z ^ i) atTop (𝓝 (0 * (-1 / (z - 1))))
<VAR>f : ℕ → ℂ<VAR>l : ℂ<VAR>h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i<VAR>k : Tendsto (fun n => (1 - z) * ∑ j ∈ range n, (∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k) * z ^ j) atTop (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))<GOAL>Tendsto (fun x => l - s x) atTop (𝓝 0)
<VAR>f : ℕ → ℂ<VAR>l : ℂ<VAR>h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i<VAR>k : Tendsto (fun n => (1 - z) * ∑ j ∈ range n, (∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k) * z ^ j) atTop (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))<GOAL>Tendsto (fun x => ∑ i ∈ range x, z ^ i) atTop (𝓝 (-1 / (z - 1)))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 G<VAR>T : E →ₗ[𝕜] E<VAR>x : E<GOAL>im ⟪x, (adjoint T) (T x)⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 G<VAR>T : E →ₗ[𝕜] E<VAR>x : E<GOAL>im (↑‖T x‖ ^ 2) = 0
<VAR>ι : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L M K' L' : HomologicalComplex C c<VAR>f : K ⟶ L<VAR>i : ι<VAR>inst✝¹ : K.HasHomology i<VAR>inst✝ : L.HasHomology i<VAR>hL : L.ExactAt i<GOAL>QuasiIsoAt f i ↔ K.ExactAt i
<VAR>ι : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L M K' L' : HomologicalComplex C c<VAR>f : K ⟶ L<VAR>i : ι<VAR>inst✝¹ : K.HasHomology i<VAR>inst✝ : L.HasHomology i<VAR>hL : IsZero (L.sc i).homology<GOAL>IsIso (ShortComplex.homologyMap ((shortComplexFunctor C c i).map f)) ↔ IsZero (K.sc i).homology
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>u : ↥K<VAR>v : E<GOAL>⟪↑((orthogonalProjection K) v), ↑u⟫_𝕜 = ⟪↑((orthogonalProjection K) v), ↑u⟫_𝕜 + ⟪v - ↑((orthogonalProjection K) v), ↑u⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>u : ↥K<VAR>v : E<GOAL>⟪↑((orthogonalProjection K) v), ↑u⟫_𝕜 + ⟪v - ↑((orthogonalProjection K) v), ↑u⟫_𝕜 = ⟪v, ↑u⟫_𝕜
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>p : ℕ × Fin n<GOAL>(fun a => (a / n, ↑a)) ((fun p => p.1 * n + ↑p.2) p) = p
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>p : ℕ × Fin n<GOAL>((fun a => (a / n, ↑a)) ((fun p => p.1 * n + ↑p.2) p)).1 = p.1
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>p : ℕ × Fin n<GOAL>(p.1 * n + ↑p.2) / n = p.1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>hb : b < 0<GOAL>1 < a / b ↔ a < b
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.1617, u_1} C<VAR>inst✝¹ : Category.{?u.1621, u_2} D<VAR>inst✝ : Category.{?u.1625, u_3} E<VAR>F : C ⥤ Karoubi D<VAR>P : Karoubi C<GOAL>(F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.1617, u_1} C<VAR>inst✝¹ : Category.{?u.1621, u_2} D<VAR>inst✝ : Category.{?u.1625, u_3} E<VAR>F : C ⥤ Karoubi D<VAR>X✝ Y✝ : Karoubi C<VAR>f : X✝ ⟶ Y✝<GOAL>(F.map f.f).f = ((fun P => { X := (F.obj P.X).X, p := (F.map P.p).f, idem := ⋯ }) X✝).p ≫ (F.map f.f).f ≫ ((fun P => { X := (F.obj P.X).X, p := (F.map P.p).f, idem := ⋯ }) Y✝).p
<VAR>M : Type u_1<VAR>inst✝¹ : Monoid M<VAR>s✝ : Set M<VAR>A : Type u_2<VAR>inst✝ : AddMonoid A<VAR>t✝ : Set A<VAR>s t : Set M<VAR>ht : IsSubmonoid t<VAR>h : s ⊆ t<VAR>a : M<VAR>ha : a ∈ Closure s<GOAL>a ∈ t
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>inst✝² : CanonicallyOrderedCommMonoid α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderClosedTopology α<VAR>f : ι → α<VAR>a : α<VAR>hf : Multipliable f<GOAL>∏' (i : ι), f i ≠ 1 ↔ ∃ x, f x ≠ 1
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>b' : Pseudoelement S.X₂<VAR>b : Over S.X₂<VAR>hb : pseudoApply S.g ⟦b⟧ = 0<GOAL>∃ a, pseudoApply S.f a = ⟦b⟧
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>b' : Pseudoelement S.X₂<VAR>b : Over S.X₂<VAR>hb : pseudoApply S.g ⟦b⟧ = 0<VAR>hb' : b.hom ≫ S.g = 0<GOAL>∃ a, pseudoApply S.f a = ⟦b⟧
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>b' : Pseudoelement S.X₂<VAR>b : Over S.X₂<VAR>hb : pseudoApply S.g ⟦b⟧ = 0<VAR>hb' : b.hom ≫ S.g = 0<VAR>c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt<VAR>hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom<GOAL>∃ a, pseudoApply S.f a = ⟦b⟧
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>b' : Pseudoelement S.X₂<VAR>b : Over S.X₂<VAR>hb : pseudoApply S.g ⟦b⟧ = 0<VAR>hb' : b.hom ≫ S.g = 0<VAR>c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt<VAR>hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom<GOAL>pseudoApply S.f (Quot.mk (PseudoEqual S.X₁) (Over.mk (pullback.fst (Abelian.factorThruImage S.f) c))) = ⟦b⟧
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>b' : Pseudoelement S.X₂<VAR>b : Over S.X₂<VAR>hb : pseudoApply S.g ⟦b⟧ = 0<VAR>hb' : b.hom ≫ S.g = 0<VAR>c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt<VAR>hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom<GOAL>(fun g => app S.f g) (Over.mk (pullback.fst (Abelian.factorThruImage S.f) c)) ≈ b
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>b' : Pseudoelement S.X₂<VAR>b : Over S.X₂<VAR>hb : pseudoApply S.g ⟦b⟧ = 0<VAR>hb' : b.hom ≫ S.g = 0<VAR>c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt<VAR>hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom<GOAL>𝟙 (pullback (Abelian.factorThruImage S.f) c) ≫ ((fun g => app S.f g) (Over.mk (pullback.fst (Abelian.factorThruImage S.f) c))).hom = pullback.snd (Abelian.factorThruImage S.f) c ≫ b.hom
<VAR>J : Type v'<VAR>inst✝³ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝¹ : Category.{?u.27917, u_1} K<VAR>D : Type u_2<VAR>inst✝ : Category.{?u.27924, u_2} D<VAR>F : J ⥤ C<VAR>c c' : Cocone F<VAR>H : IsVanKampenColimit c<VAR>e : c ≅ c'<VAR>F' : J ⥤ C<VAR>c'' : Cocone F'<VAR>α : F' ⟶ F<VAR>f : c''.pt ⟶ c'.pt<VAR>h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<GOAL>Nonempty (IsColimit c'') ↔ ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
<VAR>J : Type v'<VAR>inst✝³ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝¹ : Category.{?u.27917, u_1} K<VAR>D : Type u_2<VAR>inst✝ : Category.{?u.27924, u_2} D<VAR>F : J ⥤ C<VAR>c c' : Cocone F<VAR>H : IsVanKampenColimit c<VAR>e : c ≅ c'<VAR>F' : J ⥤ C<VAR>c'' : Cocone F'<VAR>α : F' ⟶ F<VAR>f : c''.pt ⟶ c'.pt<VAR>h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>this : c'.ι ≫ (Functor.const J).map e.inv.hom = c.ι<GOAL>Nonempty (IsColimit c'') ↔ ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
<VAR>J : Type v'<VAR>inst✝³ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝¹ : Category.{?u.27917, u_1} K<VAR>D : Type u_2<VAR>inst✝ : Category.{?u.27924, u_2} D<VAR>F : J ⥤ C<VAR>c c' : Cocone F<VAR>H : IsVanKampenColimit c<VAR>e : c ≅ c'<VAR>F' : J ⥤ C<VAR>c'' : Cocone F'<VAR>α : F' ⟶ F<VAR>f : c''.pt ⟶ c'.pt<VAR>h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>this : c'.ι ≫ (Functor.const J).map e.inv.hom = c.ι<GOAL>(∀ (j : J), IsPullback (c''.ι.app j) (α.app j) (f ≫ e.inv.hom) (c.ι.app j)) ↔ ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
<VAR>J : Type v'<VAR>inst✝³ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝¹ : Category.{?u.27917, u_1} K<VAR>D : Type u_2<VAR>inst✝ : Category.{?u.27924, u_2} D<VAR>F : J ⥤ C<VAR>c c' : Cocone F<VAR>H : IsVanKampenColimit c<VAR>e : c ≅ c'<VAR>F' : J ⥤ C<VAR>c'' : Cocone F'<VAR>α : F' ⟶ F<VAR>f : c''.pt ⟶ c'.pt<VAR>h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>this : c'.ι ≫ (Functor.const J).map e.inv.hom = c.ι<GOAL>∀ (a : J), IsPullback (c''.ι.app a) (α.app a) (f ≫ e.inv.hom) (c.ι.app a) ↔ IsPullback (c''.ι.app a) (α.app a) f (c'.ι.app a)
<VAR>J : Type v'<VAR>inst✝³ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝¹ : Category.{?u.27917, u_1} K<VAR>D : Type u_2<VAR>inst✝ : Category.{?u.27924, u_2} D<VAR>F : J ⥤ C<VAR>c c' : Cocone F<VAR>H : IsVanKampenColimit c<VAR>e : c ≅ c'<VAR>F' : J ⥤ C<VAR>c'' : Cocone F'<VAR>α : F' ⟶ F<VAR>f : c''.pt ⟶ c'.pt<VAR>h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>this : c'.ι ≫ (Functor.const J).map e.inv.hom = c.ι<VAR>j : J<GOAL>IsPullback (c''.ι.app j) (α.app j) (f ≫ e.inv.hom) (c.ι.app j) ↔ IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
<VAR>J : Type v'<VAR>inst✝³ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝¹ : Category.{?u.27917, u_1} K<VAR>D : Type u_2<VAR>inst✝ : Category.{?u.27924, u_2} D<VAR>F : J ⥤ C<VAR>c c' : Cocone F<VAR>H : IsVanKampenColimit c<VAR>e : c ≅ c'<VAR>F' : J ⥤ C<VAR>c'' : Cocone F'<VAR>α : F' ⟶ F<VAR>f : c''.pt ⟶ c'.pt<VAR>h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>this : c'.ι ≫ (Functor.const J).map e.inv.hom = c.ι<VAR>j : J<GOAL>IsPullback (c''.ι.app j) (α.app j ≫ 𝟙 (F.obj j)) (f ≫ e.inv.hom) (c.ι.app j) ↔ IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
<VAR>J : Type v'<VAR>inst✝³ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝¹ : Category.{?u.27917, u_1} K<VAR>D : Type u_2<VAR>inst✝ : Category.{?u.27924, u_2} D<VAR>F : J ⥤ C<VAR>c c' : Cocone F<VAR>H : IsVanKampenColimit c<VAR>e : c ≅ c'<VAR>F' : J ⥤ C<VAR>c'' : Cocone F'<VAR>α : F' ⟶ F<VAR>f : c''.pt ⟶ c'.pt<VAR>h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>this✝ : c'.ι ≫ (Functor.const J).map e.inv.hom = c.ι<VAR>j : J<VAR>this : IsIso e.inv.hom<GOAL>IsPullback (c''.ι.app j) (α.app j ≫ 𝟙 (F.obj j)) (f ≫ e.inv.hom) (c.ι.app j) ↔ IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Finite F<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>χ : MulChar F R<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hχ : χ ^ n = 1<VAR>a : F<VAR>ha : a ≠ 0<GOAL>∃ ζ ∈ rootsOfUnity ⟨n, ⋯⟩ R, ↑ζ = χ a
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Finite F<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>χ : MulChar F R<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hχ : χ ^ n = 1<VAR>a : F<VAR>ha : a ≠ 0<VAR>μ : Rˣ<VAR>hμ₁ : μ ∈ rootsOfUnity ⟨orderOf χ, ⋯⟩ R<VAR>hμ₂ : ↑μ = χ a<GOAL>∃ ζ ∈ rootsOfUnity ⟨n, ⋯⟩ R, ↑ζ = χ a
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Finite F<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>χ : MulChar F R<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hχ : χ ^ n = 1<VAR>a : F<VAR>ha : a ≠ 0<VAR>μ : Rˣ<VAR>hμ₁ : μ ∈ rootsOfUnity ⟨orderOf χ, ⋯⟩ R<VAR>hμ₂ : ↑μ = χ a<VAR>hχ' : ↑⟨orderOf χ, ⋯⟩ ∣ ↑⟨n, ⋯⟩<GOAL>∃ ζ ∈ rootsOfUnity ⟨n, ⋯⟩ R, ↑ζ = χ a
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M✝ : Matrix n n R<VAR>M : Matrix n n R[X]<VAR>r : R<GOAL>eval r M.det = (eval ((scalar n) r) (matPolyEquiv M)).det
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M✝ : Matrix n n R<VAR>M : Matrix n n R[X]<VAR>r : R<GOAL>((eval₂RingHom (RingHom.id R) r).mapMatrix M).det = (eval ((scalar n) r) (matPolyEquiv M)).det
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M✝ : Matrix n n R<VAR>M : Matrix n n R[X]<VAR>r : R<VAR>i✝ j✝ : n<GOAL>eval ((scalar n) r) (matPolyEquiv M) i✝ j✝ = (eval₂RingHom (RingHom.id R) r).mapMatrix M i✝ j✝
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>inst✝⁷ : InnerProductSpace 𝕜 F<VAR>inst✝⁶ : InnerProductSpace 𝕜 G<VAR>m : Type u_5<VAR>n : Type u_6<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : FiniteDimensional 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 F<VAR>v₁ : OrthonormalBasis n 𝕜 E<VAR>v₂ : OrthonormalBasis m 𝕜 F<VAR>A : Matrix m n 𝕜<GOAL>(toLin v₂.toBasis v₁.toBasis) Aᴴ = adjoint ((toLin v₁.toBasis v₂.toBasis) A)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>inst✝⁷ : InnerProductSpace 𝕜 F<VAR>inst✝⁶ : InnerProductSpace 𝕜 G<VAR>m : Type u_5<VAR>n : Type u_6<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : FiniteDimensional 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 F<VAR>v₁ : OrthonormalBasis n 𝕜 E<VAR>v₂ : OrthonormalBasis m 𝕜 F<VAR>A : Matrix m n 𝕜<VAR>i : m<VAR>j : n<GOAL>⟪((toLin v₂.toBasis v₁.toBasis) Aᴴ) (v₂.toBasis i), v₁.toBasis j⟫_𝕜 = ⟪v₂.toBasis i, ((toLin v₁.toBasis v₂.toBasis) A) (v₁.toBasis j)⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>inst✝⁷ : InnerProductSpace 𝕜 F<VAR>inst✝⁶ : InnerProductSpace 𝕜 G<VAR>m : Type u_5<VAR>n : Type u_6<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : FiniteDimensional 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 F<VAR>v₁ : OrthonormalBasis n 𝕜 E<VAR>v₂ : OrthonormalBasis m 𝕜 F<VAR>A : Matrix m n 𝕜<VAR>i : m<VAR>j : n<GOAL>⟪∑ j : n, Aᴴ j i • v₁.toBasis j, v₁.toBasis j⟫_𝕜 = ⟪v₂.toBasis i, ∑ j_1 : m, A j_1 j • v₂.toBasis j_1⟫_𝕜
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<GOAL>∃ a, cs.wordProd a = w
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<GOAL>∃ a, cs.wordProd a = 1
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<GOAL>∀ (w : W) (i : B), (∃ a, cs.wordProd a = w) → ∃ a, cs.wordProd a = cs.simple i * w
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s : Set α<VAR>t : Set β<VAR>x✝ : α × β<GOAL>x✝ ∈ ↑(lowerClosure (s ×ˢ t)) ↔ x✝ ∈ ↑(lowerClosure s ×ˢ lowerClosure t)
<VAR>F : Type u → Type v<VAR>inst✝³ : Applicative F<VAR>inst✝² : LawfulApplicative F<VAR>G : Type u → Type w<VAR>inst✝¹ : Applicative G<VAR>inst✝ : LawfulApplicative G<VAR>η : ApplicativeTransformation F G<VAR>α β : Type u<VAR>x : α → β<VAR>y : F α<GOAL>((fun {α} => η.app α) ∘ Functor.map x) y = (Functor.map x ∘ fun {α} => η.app α) y
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I : Submodule R P<VAR>J : FractionalIdeal S P<VAR>hIJ : I ≤ ↑J<GOAL>IsFractional S I
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I : Submodule R P<VAR>J : FractionalIdeal S P<VAR>hIJ : I ≤ ↑J<VAR>a : R<VAR>a_mem : a ∈ S<VAR>ha : ∀ b ∈ ↑J, IsInteger R (a • b)<GOAL>IsFractional S I
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I : Submodule R P<VAR>J : FractionalIdeal S P<VAR>hIJ : I ≤ ↑J<VAR>a : R<VAR>a_mem : a ∈ S<VAR>ha : ∀ b ∈ ↑J, IsInteger R (a • b)<GOAL>∀ b ∈ I, IsInteger R (a • b)
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q✝ : R[X]<VAR>S : Type u_1<VAR>inst✝ : AddCommMonoid S<VAR>p q : R[X]<VAR>f : ℕ → R → S<VAR>hf : ∀ (i : ℕ), f i 0 = 0<VAR>h_add : ∀ (a : ℕ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂<GOAL>(p + q).sum f = p.sum f + q.sum f
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q✝ : R[X]<VAR>S : Type u_1<VAR>inst✝ : AddCommMonoid S<VAR>p q : R[X]<VAR>f : ℕ → R → S<VAR>hf : ∀ (i : ℕ), f i 0 = 0<VAR>h_add : ∀ (a : ℕ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂<GOAL>{ toFinsupp := p.toFinsupp + q.toFinsupp }.sum f = p.sum f + q.sum f
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : OrderedRing α<VAR>l : Filter β<VAR>f g : β → α<VAR>hf : Tendsto f l atBot<VAR>hg : Tendsto g l atBot<GOAL>Tendsto (fun x => f x * g x) l atTop
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : OrderedRing α<VAR>l : Filter β<VAR>f g : β → α<VAR>hf : Tendsto f l atBot<VAR>hg : Tendsto g l atBot<VAR>this : Tendsto (fun x => -f x * -g x) l atTop<GOAL>Tendsto (fun x => f x * g x) l atTop
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝¹ : CanonicallyOrderedAddCommMonoid M<VAR>w : σ → M<VAR>φ : MvPolynomial σ R<VAR>inst✝ : NoZeroSMulDivisors ℕ M<VAR>hw : ∀ (i : σ), w i ≠ 0<VAR>n : ℕ<VAR>x : σ<GOAL>n • w x = 0 → n = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝¹ : CanonicallyOrderedAddCommMonoid M<VAR>w : σ → M<VAR>φ : MvPolynomial σ R<VAR>inst✝ : NoZeroSMulDivisors ℕ M<VAR>hw : ∀ (i : σ), w i ≠ 0<VAR>n : ℕ<VAR>x : σ<GOAL>n = 0 ∨ w x = 0 → n = 0
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>w : A.SeparatesPoints<VAR>f : C(X, ℝ)<GOAL>f ∈ A.topologicalClosure
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>w : A.SeparatesPoints<VAR>f : C(X, ℝ)<GOAL>f ∈ ⊤
<VAR>α β : Type u<VAR>s : Set Cardinal.{u_1}<VAR>hs : BddAbove s<GOAL>lift.{u, u_1} (sSup s) = sSup (lift.{u, u_1} '' s)
<VAR>α β : Type u<VAR>s : Set Cardinal.{u_1}<VAR>hs : BddAbove s<GOAL>∀ c ∈ upperBounds (lift.{u, u_1} '' s), lift.{u, u_1} (sSup s) ≤ c
<VAR>α β : Type u<VAR>s : Set Cardinal.{u_1}<VAR>hs : BddAbove s<GOAL>lift.{u, u_1} (sSup s) ∈ upperBounds (lift.{u, u_1} '' s)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>μ' : Measure α<VAR>T : Set α → E →L[ℝ] F<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : FinMeasAdditive μ T<VAR>hμ : μ ≪ μ'<VAR>f : ↥(simpleFunc E 1 μ)<VAR>f' : ↥(simpleFunc E 1 μ')<VAR>h : ↑↑↑f =ᶠ[ae μ] ↑↑↑f'<GOAL>setToL1S T f = setToL1S T f'