ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F✝ : Type u<VAR>K✝ : Type v<VAR>A✝ : Type w<VAR>inst✝¹⁰ : DivisionRing F✝<VAR>inst✝⁹ : DivisionRing K✝<VAR>inst✝⁸ : AddCommGroup A✝<VAR>inst✝⁷ : Module F✝ K✝<VAR>inst✝⁶ : Module K✝ A✝<VAR>inst✝⁵ : Module F✝ A✝<VAR>inst✝⁴ : IsScalarTower F✝ K✝ A✝<VAR>F : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : Field F<VAR>inst✝² : Ring A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : Algebra F A<VAR>hp : Nat.Prime (finrank F A)<VAR>K : Subalgebra F A<VAR>this : FiniteDimensional F A<GOAL>K = ⊥ ∨ K = ⊤
<VAR>F✝ : Type u<VAR>K✝ : Type v<VAR>A✝ : Type w<VAR>inst✝¹⁰ : DivisionRing F✝<VAR>inst✝⁹ : DivisionRing K✝<VAR>inst✝⁸ : AddCommGroup A✝<VAR>inst✝⁷ : Module F✝ K✝<VAR>inst✝⁶ : Module K✝ A✝<VAR>inst✝⁵ : Module F✝ A✝<VAR>inst✝⁴ : IsScalarTower F✝ K✝ A✝<VAR>F : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : Field F<VAR>inst✝² : Ring A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : Algebra F A<VAR>hp : Nat.Prime (finrank F A)<VAR>K : Subalgebra F A<VAR>this✝ : FiniteDimensional F A<VAR>this : DivisionRing ↥K := divisionRingOfFiniteDimensional F ↥K<GOAL>K = ⊥ ∨ K = ⊤
<VAR>F✝ : Type u<VAR>K✝ : Type v<VAR>A✝ : Type w<VAR>inst✝¹⁰ : DivisionRing F✝<VAR>inst✝⁹ : DivisionRing K✝<VAR>inst✝⁸ : AddCommGroup A✝<VAR>inst✝⁷ : Module F✝ K✝<VAR>inst✝⁶ : Module K✝ A✝<VAR>inst✝⁵ : Module F✝ A✝<VAR>inst✝⁴ : IsScalarTower F✝ K✝ A✝<VAR>F : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : Field F<VAR>inst✝² : Ring A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : Algebra F A<VAR>hp : Nat.Prime (finrank F A)<VAR>K : Subalgebra F A<VAR>this✝ : FiniteDimensional F A<VAR>this : DivisionRing ↥K := divisionRingOfFiniteDimensional F ↥K<GOAL>finrank F ↥K = 1 → K = ⊥
<VAR>F✝ : Type u<VAR>K✝ : Type v<VAR>A✝ : Type w<VAR>inst✝¹⁰ : DivisionRing F✝<VAR>inst✝⁹ : DivisionRing K✝<VAR>inst✝⁸ : AddCommGroup A✝<VAR>inst✝⁷ : Module F✝ K✝<VAR>inst✝⁶ : Module K✝ A✝<VAR>inst✝⁵ : Module F✝ A✝<VAR>inst✝⁴ : IsScalarTower F✝ K✝ A✝<VAR>F : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : Field F<VAR>inst✝² : Ring A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : Algebra F A<VAR>hp : Nat.Prime (finrank F A)<VAR>K : Subalgebra F A<VAR>this✝ : FiniteDimensional F A<VAR>this : DivisionRing ↥K := divisionRingOfFiniteDimensional F ↥K<VAR>h : finrank F ↥K = finrank F A<GOAL>K = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>h_mono : Monotone f<VAR>h_surj : Surjective f<VAR>a b x : α<VAR>hp : f x ∈ Ioo (f a) (f b)<GOAL>f x ∈ f '' Ioo a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>h_mono : Monotone f<VAR>h_surj : Surjective f<VAR>a b x : α<VAR>hp : f x ∈ Ioo (f a) (f b)<GOAL>a < x ∧ x < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>h_mono : Monotone f<VAR>h_surj : Surjective f<VAR>a b x : α<VAR>hp : a < x → b ≤ x<GOAL>f x ∉ Ioo (f a) (f b)
<VAR>α : Type u_1<VAR>f : Char → α → α<VAR>l m r : List Char<VAR>a : α<GOAL>foldrAux f a { data := l ++ m ++ r } { byteIdx := utf8Len l + utf8Len m } { byteIdx := utf8Len l } = List.foldr f a m
<VAR>α : Type u_1<VAR>f : Char → α → α<VAR>l m r : List Char<VAR>a : α<GOAL>foldrAux f a { data := l ++ m.reverse.reverse ++ r } { byteIdx := utf8Len l + utf8Len m.reverse.reverse } { byteIdx := utf8Len l } = List.foldr f a m.reverse.reverse
<VAR>R : Type u<VAR>X : Type v<VAR>inst✝ : CommRing R<VAR>a b c : lib R X<VAR>h : Rel R X b c<GOAL>Rel R X (a + b) (a + c)
<VAR>R : Type u<VAR>X : Type v<VAR>inst✝ : CommRing R<VAR>a b c : lib R X<VAR>h : Rel R X b c<GOAL>Rel R X (b + a) (c + a)
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>p : ℕ<VAR>hn : Fact (Nat.Prime p)<GOAL>cyclotomic p R * (X - 1) = X ^ p - 1
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x₀ x₁ : X<VAR>p₁ p₂ : Path x₀ x₁<VAR>hp : ∀ (t : ↑I), p₁ t = p₂ t<GOAL>HEq ⟦p₁⟧ ⟦p₂⟧
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x₀ x₁ : X<VAR>p₁ p₂ : Path x₀ x₁<VAR>hp : ∀ (t : ↑I), p₁ t = p₂ t<GOAL>⟦p₁⟧ = ⟦p₂⟧
<VAR>α : Type u<VAR>β : Type v<GOAL>∀ {l : List (Computation α)} {S : WSeq (Computation α)} {c : Computation α}, c ∈ l → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
<VAR>α : Type u<VAR>β : Type v<VAR>lem1 : ∀ (l : List (Computation α)) (S : WSeq (Computation α)), (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates<GOAL>∀ {l : List (Computation α)} {S : WSeq (Computation α)} {c : Computation α}, c ∈ l → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : SimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 3)<VAR>j : Fin (n + 2)<VAR>H : j.succ < i<VAR>hi : i = 0<GOAL>False
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : SimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 3)<VAR>j : Fin (n + 2)<VAR>H : j.succ < i<GOAL>X.map (SimplexCategory.σ j).op ≫ X.map (SimplexCategory.δ i).op = X.map (SimplexCategory.δ (i.pred ⋯)).op ≫ X.map (SimplexCategory.σ (j.castLT ⋯)).op
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>inst✝³ : NontriviallyNormedField 𝕂<VAR>inst✝² : NormedDivisionRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕂 𝔸<VAR>inst✝ : CompleteSpace 𝔸<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<GOAL>HasSum (fun n => x ^ n / ↑n !) (exp 𝕂 x)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>inst✝³ : NontriviallyNormedField 𝕂<VAR>inst✝² : NormedDivisionRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕂 𝔸<VAR>inst✝ : CompleteSpace 𝔸<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<GOAL>HasSum (fun n => (expSeries 𝕂 𝔸 n) fun x_1 => x) (exp 𝕂 x)
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} D<VAR>inst✝³ : Abelian C<VAR>inst✝² : HasInjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<VAR>n : ℕ<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>P : InjectiveResolution X<VAR>Q : InjectiveResolution Y<VAR>g : P.cocomplex ⟶ Q.cocomplex<VAR>w : P.ι ≫ g = (CochainComplex.single₀ C).map f ≫ Q.ι<GOAL>(F.rightDerived n).map f = (P.isoRightDerivedObj F n).hom ≫ (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map g ≫ (Q.isoRightDerivedObj F n).inv
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} D<VAR>inst✝³ : Abelian C<VAR>inst✝² : HasInjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<VAR>n : ℕ<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>P : InjectiveResolution X<VAR>Q : InjectiveResolution Y<VAR>g : P.cocomplex ⟶ Q.cocomplex<VAR>w : P.ι ≫ g = (CochainComplex.single₀ C).map f ≫ Q.ι<GOAL>P.ι.f 0 ≫ g.f 0 = f ≫ Q.ι.f 0
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>hab : a < b<GOAL>BddAbove {n | upperCrossingTime a b f N n ω < N}
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>hab : a < b<VAR>k : ℕ<VAR>hk : upperCrossingTime a b f N k ω = N<GOAL>BddAbove {n | upperCrossingTime a b f N n ω < N}
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n✝ m : ℕ<VAR>ω : Ω<VAR>hab : a < b<VAR>k : ℕ<VAR>hk : upperCrossingTime a b f N k ω = N<VAR>n : ℕ<VAR>hn : upperCrossingTime a b f N n ω < N<GOAL>n ≤ k
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n✝ m : ℕ<VAR>ω : Ω<VAR>hab : a < b<VAR>k : ℕ<VAR>hk : upperCrossingTime a b f N k ω = N<VAR>n : ℕ<VAR>hn : upperCrossingTime a b f N n ω < N<VAR>hn' : ¬n ≤ k<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>b : β<VAR>p : β → Prop<VAR>s : (x : β) → x = b ∨ p x → Set α<GOAL>⋃ x, ⋃ (h : x = b ∨ p x), s x h = s b ⋯ ∪ ⋃ x, ⋃ (h : p x), s x ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a b : α<VAR>s : Set α<VAR>hb : s ⊆ Iio b<VAR>hs : s.Nonempty → ∃ a < b, Ioo a b ⊆ s<VAR>a✝ : Nontrivial (Filter { x // x ∈ s })<GOAL>comap Subtype.val (𝓝[<] b) = atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a b : α<VAR>s : Set α<VAR>hb : s ⊆ Iio b<VAR>hs : s.Nonempty → ∃ a < b, Ioo a b ⊆ s<VAR>a✝ : Nontrivial (Filter { x // x ∈ s })<VAR>this : Nonempty ↑s<GOAL>comap Subtype.val (𝓝[<] b) = atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a✝¹ b : α<VAR>s : Set α<VAR>hb : s ⊆ Iio b<VAR>hs✝ : s.Nonempty → ∃ a < b, Ioo a b ⊆ s<VAR>a✝ : Nontrivial (Filter { x // x ∈ s })<VAR>this : Nonempty ↑s<VAR>a : α<VAR>h : a < b<VAR>hs : Ioo a b ⊆ s<GOAL>comap Subtype.val (𝓝[<] b) = atTop
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝¹ : HasCoequalizers C<VAR>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<GOAL>coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ T.X ≫ actRight P Q = (α_ P.X Q.X T.X).hom ≫ P.X ◁ Q.actRight ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝¹ : HasCoequalizers C<VAR>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<GOAL>((α_ P.X Q.X T.X).hom ≫ P.X ◁ Q.actRight) ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) = (α_ P.X Q.X T.X).hom ≫ P.X ◁ Q.actRight ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)
<VAR>𝒮 : Type u₁<VAR>inst✝ : Category.{v₁, u₁} 𝒮<VAR>𝒳 : BasedCategory 𝒮<VAR>𝒴 : BasedCategory 𝒮<VAR>F G H : 𝒳 ⥤ᵇ 𝒴<VAR>α : BasedNatTrans F G<VAR>β : BasedNatTrans G H<VAR>a : 𝒳.obj<GOAL>𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) ((α.vcomp β.toNatTrans).app a)
<VAR>𝒮 : Type u₁<VAR>inst✝ : Category.{v₁, u₁} 𝒮<VAR>𝒳 : BasedCategory 𝒮<VAR>𝒴 : BasedCategory 𝒮<VAR>F G H : 𝒳 ⥤ᵇ 𝒴<VAR>α : BasedNatTrans F G<VAR>β : BasedNatTrans G H<VAR>a : 𝒳.obj<GOAL>𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.app a ≫ β.app a)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring S<VAR>inst✝² : Algebra R S<VAR>m : Type u_3<VAR>inst✝¹ : Fintype m<VAR>inst✝ : DecidableEq m<VAR>b : Basis m R S<VAR>x : S<VAR>i j : m<GOAL>(toMatrix b b) ((lmul R S) x) i j = (b.repr (x * b j)) i
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : DecidableEq β<VAR>inst✝² : Group α<VAR>inst✝¹ : MulAction α β<VAR>s✝ t : Finset β<VAR>a✝¹ : α<VAR>b : β<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>a✝ : α<GOAL>a✝ ∈ (op a • s)⁻¹ ↔ a✝ ∈ a⁻¹ • s⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Nontrivial α<VAR>inst✝ : DecidableEq α<VAR>x : α<GOAL>∃ y, y ≠ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Nontrivial α<VAR>inst✝ : DecidableEq α<VAR>x y y' : α<VAR>h : y ≠ y'<GOAL>∃ y, y ≠ x
<VAR>θ : Angle<GOAL>(↑(π / 2) - θ).cos = θ.sin
<VAR>x✝ : ℝ<GOAL>(↑(π / 2) - ↑x✝).cos = (↑x✝).sin
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>P : Karoubi (SimplicialObject C)<GOAL>((𝟙 N₂ ◫ N₂Γ₂.inv) ≫ (N₂.associator Γ₂ N₂).inv ≫ Γ₂N₂.natTrans ◫ 𝟙 N₂).app P = (𝟙 N₂).app P
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>P : Karoubi (SimplicialObject C)<GOAL>(N₂Γ₂.inv.app (N₂.obj P) ≫ N₂.map (Γ₂.map (𝟙 (N₂.obj P)))) ≫ 𝟙 (N₂.obj (Γ₂.obj (N₂.obj P))) ≫ 𝟙 (N₂.obj (Γ₂.obj (N₂.obj P))) ≫ N₂.map (Γ₂N₂.natTrans.app P) = 𝟙 (N₂.obj P)
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁶ : NormedRing 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : MulActionWithZero 𝕜 E<VAR>inst✝³ : BoundedSMul 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : MulActionWithZero 𝕜 F<VAR>inst✝ : BoundedSMul 𝕜 F<VAR>f✝ : α → E<VAR>p : ℝ≥0∞<VAR>f : α → E<VAR>φ : α → 𝕜<VAR>hf : Memℒp f ⊤ μ<VAR>hφ : Memℒp φ p μ<GOAL>Memℒp (φ • f) p μ
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁶ : NormedRing 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : MulActionWithZero 𝕜 E<VAR>inst✝³ : BoundedSMul 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : MulActionWithZero 𝕜 F<VAR>inst✝ : BoundedSMul 𝕜 F<VAR>f✝ : α → E<VAR>p : ℝ≥0∞<VAR>f : α → E<VAR>φ : α → 𝕜<VAR>hf : Memℒp f ⊤ μ<VAR>hφ : Memℒp φ p μ<GOAL>1 / p = 1 / p + 1 / ⊤
<VAR>a x : ℝ<GOAL>↑(⋯.lift ↑a) = cexp (-↑π * ↑a ^ 2 * ↑x) * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : LieRingModule L N<VAR>inst✝ : LieModule R L N<VAR>y : L<GOAL>y ∈ LieModule.ker R L L ↔ y ∈ center R L
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_6, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_5, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.25079, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.25131, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ Type v<VAR>ℱ' : SheafOfTypes K<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X Y : C<VAR>i : G.obj X ⟶ G.obj Y<VAR>x : (G.op ⋙ ℱ).obj (op Y)<GOAL>ℱ'.val.map i.op (α.app (op Y) x) = α.app (op X) (ℱ.map i.op x)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_6, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_5, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.25079, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.25131, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ Type v<VAR>ℱ' : SheafOfTypes K<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X Y : C<VAR>i : G.obj X ⟶ G.obj Y<VAR>x : (G.op ⋙ ℱ).obj (op Y)<VAR>this : ∀ {X Y : C} (i : X ⟶ Y) (x : (G.op ⋙ ℱ).obj (op Y)), ℱ'.val.map (G.map i).op (α.app (op Y) x) = α.app (op X) (ℱ.map (G.map i).op x)<GOAL>ℱ'.val.map i.op (α.app (op Y) x) = α.app (op X) (ℱ.map i.op x)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_6, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_5, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.25079, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.25131, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ Type v<VAR>ℱ' : SheafOfTypes K<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X Y : C<VAR>i : G.obj X ⟶ G.obj Y<VAR>x : (G.op ⋙ ℱ).obj (op Y)<VAR>this : ∀ {X Y : C} (i : X ⟶ Y) (x : (G.op ⋙ ℱ).obj (op Y)), ℱ'.val.map (G.map i).op (α.app (op Y) x) = α.app (op X) (ℱ.map (G.map i).op x)<VAR>V : C<VAR>iVX : V ⟶ X<VAR>iVY : V ⟶ Y<VAR>e : G.map iVY = G.map iVX ≫ i<GOAL>ℱ'.val.map (G.map iVX).op (ℱ'.val.map i.op (α.app (op Y) x)) = ℱ'.val.map (G.map iVX).op (α.app (op X) (ℱ.map i.op x))
<VAR>α : Type u_1<VAR>l m r : List Char<VAR>f : Char → α → α<VAR>init : α<GOAL>Substring.foldr f init { str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l }, stopPos := { byteIdx := utf8Len l + utf8Len m } } = List.foldr f init m
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIocDiv hp a b ⩿ toIcoDiv hp a b
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIocDiv hp a b = toIcoDiv hp a b ∨ toIocDiv hp a b + 1 = toIcoDiv hp a b
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>¬a ≡ b [PMOD p] ∨ a ≡ b [PMOD p]
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Ring S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : IsDomain B<VAR>inst✝⁴ : Algebra A B<VAR>K : Type u_6<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A S<VAR>S' : Type u_7<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra A S'<VAR>pb : PowerBasis A S<VAR>pb' : PowerBasis A S'<VAR>h₁ : (aeval pb.gen) (minpoly A pb'.gen) = 0<VAR>h₂ : (aeval pb'.gen) (minpoly A pb.gen) = 0<VAR>x : S'<GOAL>((pb.lift pb'.gen h₂).comp (pb'.lift pb.gen h₁)) x = (AlgHom.id A S') x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Ring S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : IsDomain B<VAR>inst✝⁴ : Algebra A B<VAR>K : Type u_6<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A S<VAR>S' : Type u_7<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra A S'<VAR>pb : PowerBasis A S<VAR>pb' : PowerBasis A S'<VAR>h₁ : (aeval pb.gen) (minpoly A pb'.gen) = 0<VAR>h₂ : (aeval pb'.gen) (minpoly A pb.gen) = 0<VAR>f : A[X]<GOAL>((pb.lift pb'.gen h₂).comp (pb'.lift pb.gen h₁)) ((aeval pb'.gen) f) = (AlgHom.id A S') ((aeval pb'.gen) f)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Ring S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : IsDomain B<VAR>inst✝⁴ : Algebra A B<VAR>K : Type u_6<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A S<VAR>S' : Type u_7<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra A S'<VAR>pb : PowerBasis A S<VAR>pb' : PowerBasis A S'<VAR>h₁ : (aeval pb.gen) (minpoly A pb'.gen) = 0<VAR>h₂ : (aeval pb'.gen) (minpoly A pb.gen) = 0<VAR>x : S<GOAL>((pb'.lift pb.gen h₁).comp (pb.lift pb'.gen h₂)) x = (AlgHom.id A S) x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Ring S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : IsDomain B<VAR>inst✝⁴ : Algebra A B<VAR>K : Type u_6<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A S<VAR>S' : Type u_7<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra A S'<VAR>pb : PowerBasis A S<VAR>pb' : PowerBasis A S'<VAR>h₁ : (aeval pb.gen) (minpoly A pb'.gen) = 0<VAR>h₂ : (aeval pb'.gen) (minpoly A pb.gen) = 0<VAR>f : A[X]<GOAL>((pb'.lift pb.gen h₁).comp (pb.lift pb'.gen h₂)) ((aeval pb.gen) f) = (AlgHom.id A S) ((aeval pb.gen) f)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : IsAlgClosed k<VAR>m n : ℕ<VAR>r' q' : 𝕎 k<VAR>hr' : r'.coeff 0 ≠ 0<VAR>hq' : q'.coeff 0 ≠ 0<VAR>hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)<VAR>b : 𝕎 k := frobeniusRotation p hr' hq'<GOAL>φ ((algebraMap (𝕎 k) (FractionRing (𝕎 k))) b) * Localization.mk (↑p ^ m * r') ⟨↑p ^ n * q', hq⟩ = ↑p ^ (↑m - ↑n) * (algebraMap (𝕎 k) (FractionRing (𝕎 k))) b
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : IsAlgClosed k<VAR>m n : ℕ<VAR>r' q' : 𝕎 k<VAR>hr' : r'.coeff 0 ≠ 0<VAR>hq' : q'.coeff 0 ≠ 0<VAR>hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)<VAR>b : 𝕎 k := frobeniusRotation p hr' hq'<VAR>key : frobenius b * ↑p ^ m * r' * ↑p ^ n = ↑p ^ m * b * (↑p ^ n * q')<GOAL>φ ((algebraMap (𝕎 k) (FractionRing (𝕎 k))) b) * Localization.mk (↑p ^ m * r') ⟨↑p ^ n * q', hq⟩ = ↑p ^ (↑m - ↑n) * (algebraMap (𝕎 k) (FractionRing (𝕎 k))) b
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : IsAlgClosed k<VAR>m n : ℕ<VAR>r' q' : 𝕎 k<VAR>hr' : r'.coeff 0 ≠ 0<VAR>hq' : q'.coeff 0 ≠ 0<VAR>hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)<VAR>b : 𝕎 k := frobeniusRotation p hr' hq'<VAR>key : frobenius b * ↑p ^ m * r' * ↑p ^ n = ↑p ^ m * b * (↑p ^ n * q')<VAR>hq'' : (algebraMap (𝕎 k) (FractionRing (𝕎 k))) q' ≠ 0<GOAL>φ ((algebraMap (𝕎 k) (FractionRing (𝕎 k))) b) * Localization.mk (↑p ^ m * r') ⟨↑p ^ n * q', hq⟩ = ↑p ^ (↑m - ↑n) * (algebraMap (𝕎 k) (FractionRing (𝕎 k))) b
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : IsAlgClosed k<VAR>m n : ℕ<VAR>r' q' : 𝕎 k<VAR>hr' : r'.coeff 0 ≠ 0<VAR>hq' : q'.coeff 0 ≠ 0<VAR>hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)<VAR>b : 𝕎 k := frobeniusRotation p hr' hq'<VAR>key : frobenius b * ↑p ^ m * r' * ↑p ^ n = ↑p ^ m * b * (↑p ^ n * q')<VAR>hq'' : (algebraMap (𝕎 k) (FractionRing (𝕎 k))) q' ≠ 0<GOAL>φ ((algebraMap (𝕎 k) (FractionRing (𝕎 k))) b) * Localization.mk (↑p ^ m * r') ⟨↑p ^ n * q', hq⟩ = ↑p ^ ↑m / ↑p ^ ↑n * (algebraMap (𝕎 k) (FractionRing (𝕎 k))) b
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : IsAlgClosed k<VAR>m n : ℕ<VAR>r' q' : 𝕎 k<VAR>hr' : r'.coeff 0 ≠ 0<VAR>hq' : q'.coeff 0 ≠ 0<VAR>hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)<VAR>b : 𝕎 k := frobeniusRotation p hr' hq'<VAR>key : frobenius b * ↑p ^ m * r' * ↑p ^ n = ↑p ^ m * b * (↑p ^ n * q')<VAR>hq'' : (algebraMap (𝕎 k) (FractionRing (𝕎 k))) q' ≠ 0<GOAL>φ ((algebraMap (𝕎 k) (FractionRing (𝕎 k))) b) * (↑p ^ m * (algebraMap (𝕎 k) (FractionRing (𝕎 k))) r') * ↑p ^ n = ↑p ^ m * (algebraMap (𝕎 k) (FractionRing (𝕎 k))) b * (↑p ^ n * (algebraMap (𝕎 k) (FractionRing (𝕎 k))) q')
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : IsAlgClosed k<VAR>m n : ℕ<VAR>r' q' : 𝕎 k<VAR>hr' : r'.coeff 0 ≠ 0<VAR>hq' : q'.coeff 0 ≠ 0<VAR>hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)<VAR>b : 𝕎 k := frobeniusRotation p hr' hq'<VAR>key : frobenius b * ↑p ^ m * r' * ↑p ^ n = ↑p ^ m * b * (↑p ^ n * q')<VAR>hq'' : (algebraMap (𝕎 k) (FractionRing (𝕎 k))) q' ≠ 0<GOAL>(algebraMap (𝕎 k) (Localization (nonZeroDivisors (𝕎 k)))) ((frobeniusEquiv p k) b) * (↑p ^ m * (algebraMap (𝕎 k) (FractionRing (𝕎 k))) r') * ↑p ^ n = ↑p ^ m * (algebraMap (𝕎 k) (FractionRing (𝕎 k))) b * (↑p ^ n * (algebraMap (𝕎 k) (FractionRing (𝕎 k))) q')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>dec : DecidableEq α<VAR>a b : α<VAR>P : RegularExpression α<VAR>x : List α<GOAL>P.rmatch x = true ↔ x ∈ P.matches'
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝ : CommMonoid M<VAR>s₂ s₁ s : Finset α<VAR>a : α<VAR>g f : α → M<VAR>n : ℕ<GOAL>∏ x ∈ range (n + 1), (x + 1) = (n + 1)!
<VAR>x✝ y x : ℝ<GOAL>log (-x) = log x
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>h : IsUniform<VAR>α : TypeVec.{u} n<VAR>a : (P F).A<VAR>f : (P F).B a ⟹ α<VAR>i✝ : Fin2 n<VAR>u : α i✝<GOAL>u ∈ supp (abs ⟨a, f⟩) i✝ ↔ u ∈ f i✝ '' univ
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>h : IsUniform<VAR>α : TypeVec.{u} n<VAR>a : (P F).A<VAR>f : (P F).B a ⟹ α<VAR>i✝ : Fin2 n<VAR>u : α i✝<GOAL>(∀ (a_1 : (P F).A) (f_1 : (P F).B a_1 ⟹ α), abs ⟨a_1, f_1⟩ = abs ⟨a, f⟩ → u ∈ f_1 i✝ '' univ) ↔ u ∈ f i✝ '' univ
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>h : IsUniform<VAR>α : TypeVec.{u} n<VAR>a : (P F).A<VAR>f : (P F).B a ⟹ α<VAR>i✝ : Fin2 n<VAR>u : α i✝<VAR>h' : u ∈ f i✝ '' univ<VAR>a' : (P F).A<VAR>f' : (P F).B a' ⟹ α<VAR>e : abs ⟨a', f'⟩ = abs ⟨a, f⟩<GOAL>u ∈ f' i✝ '' univ
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>h : IsUniform<VAR>α : TypeVec.{u} n<VAR>a : (P F).A<VAR>f : (P F).B a ⟹ α<VAR>i✝ : Fin2 n<VAR>u : α i✝<VAR>h' : u ∈ f i✝ '' univ<VAR>a' : (P F).A<VAR>f' : (P F).B a' ⟹ α<VAR>e : abs ⟨a', f'⟩ = abs ⟨a, f⟩<GOAL>u ∈ f i✝ '' univ
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>c : 𝕜<VAR>s t : Set E<VAR>x y : E<VAR>r : ℝ≥0∞<VAR>h : x ∈ s<GOAL>egauge 𝕜 s x ≤ 1
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>c : 𝕜<VAR>s t : Set E<VAR>x y : E<VAR>r : ℝ≥0∞<VAR>h : x ∈ 1 • s<GOAL>egauge 𝕜 s x ≤ 1