ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>L : Language<VAR>K : Set (Bundled L.Structure)<VAR>M : Type w<VAR>inst✝¹ : L.Structure M<VAR>N✝ : Type w<VAR>inst✝ : L.Structure N✝<VAR>h : L.IsUltrahomogeneous M<VAR>N P Q : Bundled L.Structure<VAR>NP : ↑N ↪[L] ↑P<VAR>NQ : ↑N ↪[L] ↑Q<VAR>Nfg : Structure.FG L ↑N<VAR>Pfg : Structure.FG L ↑P<VAR>PM : ↑P ↪[L] M<VAR>Qfg : Structure.FG L ↑Q<VAR>QM : ↑Q ↪[L] M<VAR>g : M ≃[L] M<VAR>hg : (QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding = g.toEmbedding.comp (PM.comp NP).toHom.range.subtype<VAR>s : L.Substructure M := (g.toHom.comp PM.toHom).range ⊔ QM.toHom.range<VAR>n : ↑N<VAR>hgn : QM (NQ n) = g (PM (NP n))<GOAL>(g.toEmbedding.comp PM) (NP n) = g (PM (NP n))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s s₁ s₂ t t₁ t₂ u v : Finset α<VAR>a✝ b✝ : α<VAR>P : Finset α → Finset α → Prop<VAR>symm : ∀ {a b : Finset α}, P a b → P b a<VAR>empty_right : ∀ {a : Finset α}, P a ∅<VAR>singletons : ∀ {a b : α}, P {a} {b}<VAR>union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c<VAR>a b : Finset α<GOAL>P a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ s₁ s₂ t t₁ t₂ u v : Finset α<VAR>a✝ b✝ : α<VAR>P : Finset α → Finset α → Prop<VAR>symm : ∀ {a b : Finset α}, P a b → P b a<VAR>empty_right : ∀ {a : Finset α}, P a ∅<VAR>singletons : ∀ {a b : α}, P {a} {b}<VAR>union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c<VAR>a b : Finset α<VAR>x : α<VAR>s : Finset α<VAR>_xs : x ∉ s<VAR>hi : P a s<GOAL>P (insert x s) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ s₁ s₂ t t₁ t₂ u v : Finset α<VAR>a✝ b✝ : α<VAR>P : Finset α → Finset α → Prop<VAR>symm : ∀ {a b : Finset α}, P a b → P b a<VAR>empty_right : ∀ {a : Finset α}, P a ∅<VAR>singletons : ∀ {a b : α}, P {a} {b}<VAR>union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c<VAR>a b : Finset α<VAR>x : α<VAR>s : Finset α<VAR>_xs : x ∉ s<VAR>hi : P a s<GOAL>P ({x} ∪ s) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ s₁ s₂ t t₁ t₂ u v : Finset α<VAR>a✝ b✝ : α<VAR>P : Finset α → Finset α → Prop<VAR>symm : ∀ {a b : Finset α}, P a b → P b a<VAR>empty_right : ∀ {a : Finset α}, P a ∅<VAR>singletons : ∀ {a b : α}, P {a} {b}<VAR>union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c<VAR>a b : Finset α<VAR>x : α<VAR>s : Finset α<VAR>_xs : x ∉ s<VAR>hi : P a s<GOAL>P {x} a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α<VAR>a✝¹ b✝ : α<VAR>P : Finset α → Finset α → Prop<VAR>symm : ∀ {a b : Finset α}, P a b → P b a<VAR>empty_right : ∀ {a : Finset α}, P a ∅<VAR>singletons : ∀ {a b : α}, P {a} {b}<VAR>union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c<VAR>a✝ b : Finset α<VAR>x : α<VAR>s : Finset α<VAR>_xs : x ∉ s<VAR>hi✝ : P a✝ s<VAR>a : α<VAR>t : Finset α<VAR>_ta : a ∉ t<VAR>hi : P {x} t<GOAL>P (insert a t) {x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α<VAR>a✝¹ b✝ : α<VAR>P : Finset α → Finset α → Prop<VAR>symm : ∀ {a b : Finset α}, P a b → P b a<VAR>empty_right : ∀ {a : Finset α}, P a ∅<VAR>singletons : ∀ {a b : α}, P {a} {b}<VAR>union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c<VAR>a✝ b : Finset α<VAR>x : α<VAR>s : Finset α<VAR>_xs : x ∉ s<VAR>hi✝ : P a✝ s<VAR>a : α<VAR>t : Finset α<VAR>_ta : a ∉ t<VAR>hi : P {x} t<GOAL>P ({a} ∪ t) {x}
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝² : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>U V✝ W✝ X✝ Y✝ Z✝ V W X Y Z : C<VAR>f : V ≅ W<VAR>g : X ⟶ Y<VAR>h : Y ⟶ Z<GOAL>(g ⊗ f.hom) ≫ (h ⊗ f.inv) = (g ⊗ 𝟙 V) ≫ (h ⊗ 𝟙 V)
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝² : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>U V✝ W✝ X✝ Y✝ Z✝ V W X Y Z : C<VAR>f : V ≅ W<VAR>g : X ⟶ Y<VAR>h : Y ⟶ Z<GOAL>g ≫ h ⊗ 𝟙 V = (g ⊗ 𝟙 V) ≫ (h ⊗ 𝟙 V)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝¹¹ : MeasurableSpace X<VAR>inst✝¹⁰ : TopologicalSpace X<VAR>inst✝⁹ : MeasurableSpace Y<VAR>inst✝⁸ : TopologicalSpace Y<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>f✝ g✝ : X → E<VAR>μ : Measure X<VAR>s✝ : Set X<VAR>inst✝⁵ : OpensMeasurableSpace X<VAR>A K : Set X<VAR>inst✝⁴ : LocallyCompactSpace X<VAR>inst✝³ : T2Space X<VAR>𝕜 : Type u_6<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SecondCountableTopologyEither X 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : X → E<VAR>g : X → 𝕜<VAR>s : Set X<VAR>hs : IsOpen s<VAR>hf : LocallyIntegrableOn f s μ<VAR>hg : ContinuousOn g s<GOAL>LocallyIntegrableOn (fun x => g x • f x) s μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝¹¹ : MeasurableSpace X<VAR>inst✝¹⁰ : TopologicalSpace X<VAR>inst✝⁹ : MeasurableSpace Y<VAR>inst✝⁸ : TopologicalSpace Y<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>f✝ g✝ : X → E<VAR>μ : Measure X<VAR>s✝ : Set X<VAR>inst✝⁵ : OpensMeasurableSpace X<VAR>A K : Set X<VAR>inst✝⁴ : LocallyCompactSpace X<VAR>inst✝³ : T2Space X<VAR>𝕜 : Type u_6<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SecondCountableTopologyEither X 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : X → E<VAR>g : X → 𝕜<VAR>s : Set X<VAR>hs : IsOpen s<VAR>hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ<VAR>hg : ContinuousOn g s<GOAL>∀ k ⊆ s, IsCompact k → IntegrableOn (fun x => g x • f x) k μ
<VAR>Y : Scheme<VAR>U : Y.OpenCover<GOAL>zariskiTopology.sieves Y (Sieve.generate (Presieve.ofArrows U.obj U.map))
<VAR>Y : Scheme<VAR>U : Y.OpenCover<VAR>V : Y.OpenCover := { J := ↑↑Y.toPresheafedSpace, obj := fun y => U.obj (U.f y), map := fun y => U.map (U.f y), f := id, covers := ⋯, IsOpen := ⋯ }<GOAL>zariskiTopology.sieves Y (Sieve.generate (Presieve.ofArrows U.obj U.map))
<VAR>Y : Scheme<VAR>U : Y.OpenCover<VAR>V : Y.OpenCover := { J := ↑↑Y.toPresheafedSpace, obj := fun y => U.obj (U.f y), map := fun y => U.map (U.f y), f := id, covers := ⋯, IsOpen := ⋯ }<GOAL>Presieve.ofArrows V.obj V.map ≤ (Sieve.generate (Presieve.ofArrows U.obj U.map)).arrows
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q✝ p : ℕ<VAR>hp : p ≠ 0<VAR>f : R →+* S<VAR>q : R[X]<VAR>n : ℕ<GOAL>(map f (contract p q)).coeff n = (contract p (map f q)).coeff n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>a : α<VAR>s : Computation α<VAR>m : a ∈ s<GOAL>f a ∈ map f s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>a : α<VAR>s : Computation α<VAR>m : a ∈ s<GOAL>f a ∈ s.bind (pure ∘ f)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>a : α<VAR>s : Computation α<VAR>m : a ∈ s<GOAL>f a ∈ (pure ∘ f) a
<GOAL>UnivLE.{u, v} ∨ UnivLE.{v, u}
<GOAL>univ.{u, v + 1} ≤ univ.{v, u + 1} ∨ univ.{v, u + 1} ≤ univ.{u, v + 1}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : CommSemiring R<GOAL>IsRadical y ↔ (Ideal.span {y}).IsRadical
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : CommSemiring R<GOAL>(∀ (n : ℕ) (x : R), x ^ n ∈ Ideal.span {y} → x ∈ Ideal.span {y}) ↔ (Ideal.span {y}).IsRadical
<VAR>R : Type u_1<VAR>inst✝² : AddCommMonoid R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : BinomialRing R<VAR>r : R<GOAL>multichoose r 0 = r ^ 0
<VAR>R : Type u_1<VAR>inst✝² : AddCommMonoid R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : BinomialRing R<VAR>r : R<GOAL>(fun x => Nat.factorial 0 • x) (multichoose r 0) = (fun x => Nat.factorial 0 • x) (r ^ 0)
<VAR>R : Type u_1<VAR>inst✝² : AddCommMonoid R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : BinomialRing R<VAR>r : R<GOAL>Nat.factorial 0 • multichoose r 0 = Nat.factorial 0 • r ^ 0
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<GOAL>sᶜ ∈ coclosedCompact X ↔ IsCompact (closure s)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁵ : DivisionRing k<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module k V<VAR>inst✝² : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>inst✝¹ : CharZero k<VAR>inst✝ : Fintype ι<VAR>h : s.Nonempty<GOAL>∑ i : ι, centroidWeightsIndicator k s i = 1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁵ : DivisionRing k<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module k V<VAR>inst✝² : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>inst✝¹ : CharZero k<VAR>inst✝ : Fintype ι<VAR>h : s.Nonempty<GOAL>∑ i ∈ s, centroidWeights k s i = 1
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>x y : E<VAR>hx : x ∈ closure s<VAR>hy : y ∈ interior s<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>a • x + b • y ∈ interior s
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>a b : α<VAR>x✝ : a ∣ 1 ∧ b ∣ 1<VAR>c : α<VAR>hc : 1 = a * c<VAR>d : α<VAR>hd : 1 = b * d<GOAL>lcm ↑(Units.mkOfMulEqOne a c ⋯) ↑(Units.mkOfMulEqOne b d ⋯) = 1
<VAR>n : ℕ<GOAL>n.choose 1 = n
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : NonPreadditiveAbelian C<VAR>X Y : C<VAR>a b c d : X ⟶ Y<GOAL>prod.lift a b - prod.lift c d = prod.lift (a - c) (b - d)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : NonPreadditiveAbelian C<VAR>X Y : C<VAR>a b c d : X ⟶ Y<GOAL>prod.lift (prod.lift a b) (prod.lift c d) ≫ σ = prod.lift (prod.lift a c ≫ σ) (prod.lift b d ≫ σ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t : Set β<VAR>f : α → β<VAR>inst✝ : Nonempty α<VAR>h : s ⊆ invFunOn f s '' (f '' s)<VAR>x : α<VAR>hx' : x ∈ s<VAR>hx : invFunOn f s (f x) ∈ s<GOAL>invFunOn f s (f (invFunOn f s (f x))) = invFunOn f s (f x)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>e : β → α<VAR>a : α<GOAL>(∀ (i : ℕ), True → ∃ y ∈ range e, y ∈ ball a (1 / (↑i + 1))) ↔ ∀ (n : ℕ), ∃ k, dist a (e k) < 1 / (↑n + 1)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁶ : CommMonoid M<VAR>inst✝⁵ : CommMonoid N<VAR>inst✝⁴ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>μ : S<VAR>n : ℕ+<VAR>hμ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Algebra R S<VAR>f : S ≃ₐ[R] S<GOAL>μ ^ (↑((autToPow R hμ) f)).val = f μ
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁶ : CommMonoid M<VAR>inst✝⁵ : CommMonoid N<VAR>inst✝⁴ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>μ : S<VAR>n : ℕ+<VAR>hμ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Algebra R S<VAR>f : S ≃ₐ[R] S<GOAL>μ ^ (↑⋯.choose).val = f μ
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁶ : CommMonoid M<VAR>inst✝⁵ : CommMonoid N<VAR>inst✝⁴ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>μ : S<VAR>n : ℕ+<VAR>hμ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Algebra R S<VAR>f : S ≃ₐ[R] S<VAR>h : ∃ m, f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m<GOAL>μ ^ (↑h.choose).val = f μ
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁶ : CommMonoid M<VAR>inst✝⁵ : CommMonoid N<VAR>inst✝⁴ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>μ : S<VAR>n : ℕ+<VAR>hμ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Algebra R S<VAR>f : S ≃ₐ[R] S<VAR>h : ∃ m, f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m<VAR>this : f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ h.choose<GOAL>μ ^ (↑h.choose).val = f μ
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁶ : CommMonoid M<VAR>inst✝⁵ : CommMonoid N<VAR>inst✝⁴ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>μ : S<VAR>n : ℕ+<VAR>hμ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Algebra R S<VAR>f : S ≃ₐ[R] S<VAR>h : ∃ m, f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m<VAR>this : f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ h.choose<GOAL>↑↑hμ.toRootsOfUnity ^ (↑h.choose).val = ↑↑hμ.toRootsOfUnity ^ h.choose
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁶ : CommMonoid M<VAR>inst✝⁵ : CommMonoid N<VAR>inst✝⁴ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>μ : S<VAR>n : ℕ+<VAR>hμ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Algebra R S<VAR>f : S ≃ₐ[R] S<VAR>h : ∃ m, f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m<VAR>this : f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ h.choose<GOAL>↑↑(hμ.toRootsOfUnity ^ (↑h.choose).val) = ↑↑(hμ.toRootsOfUnity ^ h.choose)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁶ : CommMonoid M<VAR>inst✝⁵ : CommMonoid N<VAR>inst✝⁴ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>μ : S<VAR>n : ℕ+<VAR>hμ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Algebra R S<VAR>f : S ≃ₐ[R] S<VAR>h : ∃ m, f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m<VAR>this : f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ h.choose<GOAL>hμ.toRootsOfUnity ^ (↑h.choose).val = hμ.toRootsOfUnity ^ h.choose
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁶ : CommMonoid M<VAR>inst✝⁵ : CommMonoid N<VAR>inst✝⁴ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>μ : S<VAR>n : ℕ+<VAR>hμ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Algebra R S<VAR>f : S ≃ₐ[R] S<VAR>h : ∃ m, f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m<VAR>this : f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ h.choose<GOAL>h.choose % orderOf μ ≡ h.choose [MOD orderOf ↑↑hμ.toRootsOfUnity]
<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₂ p₃ = ↑(π / 2)<GOAL>(∡ p₃ p₁ p₂).cos = dist p₁ p₂ / dist p₁ p₃
<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₂ p₃ = ↑(π / 2)<VAR>hs : (∡ p₃ p₁ p₂).sign = 1<GOAL>(∡ p₃ p₁ p₂).cos = dist p₁ p₂ / dist p₁ p₃
<VAR>T : Type u₁<VAR>inst✝ : Category.{v₁, u₁} T<VAR>X✝ X Y Z : T<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>map (f ≫ g) = map f ⋙ map g
<VAR>T : Type u₁<VAR>inst✝ : Category.{v₁, u₁} T<VAR>X✝ X Y Z : T<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>∀ (X_1 : Over X), (map (f ≫ g)).obj X_1 = (map f ⋙ map g).obj X_1
<VAR>T : Type u₁<VAR>inst✝ : Category.{v₁, u₁} T<VAR>X✝ X Y Z : T<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>autoParam (∀ (X_1 Y_1 : Over X) (f_1 : X_1 ⟶ Y_1), (map (f ≫ g)).map f_1 = eqToHom ⋯ ≫ (map f ⋙ map g).map f_1 ≫ eqToHom ⋯) _auto✝
<VAR>α : Type u_1<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b x : α<GOAL>x ∈ Icc a b ↔ a ≤ x ∧ x ≤ b
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → R<VAR>h : P ≈ Q<VAR>u v : R<VAR>hu : IsUnit u<VAR>hv : IsUnit v<GOAL>W'.add (u • P) (v • Q) = u ^ 4 • W'.add P Q
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → R<VAR>h : P ≈ Q<VAR>u v : R<VAR>hu : IsUnit u<VAR>hv : IsUnit v<VAR>smul : P ≈ Q ↔ u • P ≈ v • Q<GOAL>W'.add (u • P) (v • Q) = u ^ 4 • W'.add P Q
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f✝ : α → E<VAR>s✝ : Set α<VAR>f : α → E<VAR>s : Set α<VAR>hf : LocallyBoundedVariationOn f s<VAR>a b c : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<VAR>hc : c ∈ s<GOAL>variationOnFromTo f s a b = variationOnFromTo f s a c ↔ variationOnFromTo f s b c = 0
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>f : α → α<VAR>x✝ y : ℕ → α<VAR>β : Type u_2<VAR>g : β → β<VAR>h : β → α<VAR>hf : Monotone f<VAR>H : h ∘ g ≤ f ∘ h<VAR>n : ℕ<VAR>x : β<GOAL>(h ∘ g^[n]) x ≤ (f^[n] ∘ h) x
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>f : α → α<VAR>x✝ y : ℕ → α<VAR>β : Type u_2<VAR>g : β → β<VAR>h : β → α<VAR>hf : Monotone f<VAR>H : h ∘ g ≤ f ∘ h<VAR>n : ℕ<VAR>x : β<VAR>k✝ : ℕ<VAR>a✝ : k✝ < n<GOAL>h (g (g^[k✝] x)) ≤ f (h (g^[k✝] x))
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>Base : Set α → Prop<VAR>exch : ExchangeProperty Base<VAR>B B' B₁ B₂ : Set α<VAR>hB₁ : Base B₁<VAR>hB₂ : Base B₂<GOAL>B₁.encard = B₂.encard
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>f✝ : R →+* S<VAR>I✝ J : Ideal S<VAR>inst✝ : Algebra R S<VAR>f : R →+* S<VAR>I : Ideal R<VAR>hf₁ : Function.Injective ⇑f<VAR>hf₂ : f.IsIntegral<GOAL>RingHom.ker f ≤ I
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedField 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>s t : Set E<VAR>x✝ y : E<VAR>r : ℝ≥0<VAR>hc : 1 < ‖c‖<VAR>x : E<GOAL>egauge 𝕜 (ball 0 1) x ≤ ↑‖c‖₊ * ↑‖x‖₊
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>hΦ : Isometry Φ<GOAL>infDist (Φ x) (Φ '' t) = infDist x t
<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 : Mon_ C<VAR>P : Bimod R S<GOAL>((ρ_ P.X).inv ≫ P.X ◁ S.one ≫ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul)) ≫ coequalizer.desc P.actRight ⋯ = 𝟙 P.X
<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 : Mon_ C<VAR>P : Bimod R S<GOAL>(ρ_ P.X).inv ≫ P.X ◁ S.one ≫ P.actRight = 𝟙 P.X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁶ : MeasurableSpace α<VAR>K : Type u_5<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : CompleteLattice β<VAR>inst✝³ : OrderClosedTopology β<VAR>inst✝² : Zero β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : OpensMeasurableSpace β<VAR>i : ℕ → β<VAR>f : α → β<VAR>a : α<VAR>hf : Measurable f<VAR>h_zero : 0 = ⊥<GOAL>⨆ n, ↑(approx i f n) a = ⨆ k, ⨆ (_ : i k ≤ f a), i k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁶ : MeasurableSpace α<VAR>K : Type u_5<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : CompleteLattice β<VAR>inst✝³ : OrderClosedTopology β<VAR>inst✝² : Zero β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : OpensMeasurableSpace β<VAR>i : ℕ → β<VAR>f : α → β<VAR>a : α<VAR>hf : Measurable f<VAR>h_zero : 0 = ⊥<VAR>n : ℕ<GOAL>↑(approx i f n) a ≤ ⨆ k, ⨆ (_ : i k ≤ f a), i k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁶ : MeasurableSpace α<VAR>K : Type u_5<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : CompleteLattice β<VAR>inst✝³ : OrderClosedTopology β<VAR>inst✝² : Zero β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : OpensMeasurableSpace β<VAR>i : ℕ → β<VAR>f : α → β<VAR>a : α<VAR>hf : Measurable f<VAR>h_zero : 0 = ⊥<VAR>k : ℕ<VAR>hk : i k ≤ f a<GOAL>i k ≤ ⨆ n, ↑(approx i f n) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : Monoid α<VAR>a b : α<VAR>h : a ~ᵤ b<VAR>u : αˣ<VAR>hu : a * ↑u = b<VAR>x✝ : IsUnit a<VAR>v : αˣ<VAR>hv : ↑v = a<GOAL>↑(v * u) = b
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>n : ℕ<GOAL>(map f p).coeff n = f (p.coeff n)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>n : ℕ<GOAL>∑ n_1 ∈ p.support, ((C.comp f) (p.coeff n_1) * X ^ n_1).coeff n = f (p.coeff n)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>n : ℕ<GOAL>∑ n_1 ∈ p.support, ((C.comp f) (p.coeff n_1) * X ^ n_1).coeff n = ∑ x ∈ p.support, f ((C (p.coeff x) * X ^ x).coeff n)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>n x : ℕ<VAR>_hx : x ∈ p.support<GOAL>((C.comp f) (p.coeff x) * X ^ x).coeff n = f ((C (p.coeff x) * X ^ x).coeff n)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>n x : ℕ<VAR>_hx : x ∈ p.support<GOAL>(if n = x then f (p.coeff x) else 0) = f (if n = x then p.coeff x else 0)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>addValuationDef 0 = ⊤
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀ : Type u_4<VAR>R : Type u_5<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : NoZeroDivisors M₀<VAR>n : ℕ<VAR>f : ι → M₀<VAR>hn : n ≠ 0<VAR>x✝ : ι<GOAL>(x✝ ∈ support fun a => f a ^ n) ↔ x✝ ∈ support f
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>ha : 2 ≤ a<GOAL>Injective fun x => a ^ x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderTopology β<VAR>inst✝¹ : Nonempty γ<VAR>inst✝ : DenselyOrdered α<VAR>a b x y : α<VAR>s t : Set α<VAR>hxy : x ≤ y<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hab : Icc a b ⊆ s ∪ t<VAR>hx : x ∈ Icc a b ∩ s<VAR>hy : y ∈ Icc a b ∩ t<GOAL>(Icc a b ∩ (s ∩ t)).Nonempty
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderTopology β<VAR>inst✝¹ : Nonempty γ<VAR>inst✝ : DenselyOrdered α<VAR>a b x y : α<VAR>s t : Set α<VAR>hxy : x ≤ y<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hab : Icc a b ⊆ s ∪ t<VAR>hx : x ∈ Icc a b ∩ s<VAR>hy : y ∈ Icc a b ∩ t<VAR>xyab : Icc x y ⊆ Icc a b<GOAL>(Icc a b ∩ (s ∩ t)).Nonempty
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderTopology β<VAR>inst✝¹ : Nonempty γ<VAR>inst✝ : DenselyOrdered α<VAR>a b x y : α<VAR>s t : Set α<VAR>hxy : x ≤ y<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hab : Icc a b ⊆ s ∪ t<VAR>hx : x ∈ Icc a b ∩ s<VAR>hy : y ∈ Icc a b ∩ t<VAR>xyab : Icc x y ⊆ Icc a b<VAR>hst : ¬(Icc a b ∩ (s ∩ t)).Nonempty<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderTopology β<VAR>inst✝¹ : Nonempty γ<VAR>inst✝ : DenselyOrdered α<VAR>a b x y : α<VAR>s t : Set α<VAR>hxy : x ≤ y<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hab : Icc a b ⊆ s ∪ t<VAR>hx : x ∈ Icc a b ∩ s<VAR>hy : y ∈ Icc a b ∩ t<VAR>xyab : Icc x y ⊆ Icc a b<VAR>hst : ¬(Icc a b ∩ (s ∩ t)).Nonempty<GOAL>Icc x y ⊆ s