ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>inst✝ : StarRing α<VAR>M : Matrix n n α<GOAL>M = 1ᴴ ↔ M = 1
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>T : L.Theory<VAR>inst✝ : Finite γ<VAR>f : α → β ⊕ γ<VAR>φ : L.Formula α<VAR>v : β → M<VAR>v' : Fin 0 → M<GOAL>Realize (Formula.iAlls f φ) v v' ↔ ∀ (i : γ → M), φ.Realize fun a => Sum.elim v i (f a)
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>T : L.Theory<VAR>inst✝ : Finite γ<VAR>f : α → β ⊕ γ<VAR>φ : L.Formula α<VAR>v : β → M<VAR>v' : Fin 0 → M<GOAL>Realize (Formula.iAlls f φ) v v' = (Formula.iAlls f φ).Realize v
<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>X P Q ◁ T.one ≫ actRight P Q = (ρ_ (X P Q)).hom
<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>(tensorRight (𝟙_ C)).map (coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) ≫ X P Q ◁ T.one ≫ actRight P Q = (tensorRight (𝟙_ C)).map (coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) ≫ (ρ_ (X P Q)).hom
<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) ▷ 𝟙_ C ≫ coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ◁ T.one ≫ actRight P Q = coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ 𝟙_ C ≫ (ρ_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft))).hom
<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.one ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ T.X) ≫ actRight P Q = coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ 𝟙_ C ≫ (ρ_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft))).hom
<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.one ≫ (α_ 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) = coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ 𝟙_ C ≫ (ρ_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft))).hom
<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 (𝟙_ C)).hom ≫ P.X ◁ Q.X ◁ T.one) ≫ P.X ◁ Q.actRight) ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) = coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ 𝟙_ C ≫ (ρ_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft))).hom
<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 (𝟙_ C)).hom ≫ P.X ◁ (ρ_ Q.X).hom ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) = coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ 𝟙_ C ≫ (ρ_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft))).hom
<VAR>α : Type u_1<VAR>inst✝ : CommSemiring α<VAR>n : ℕ<GOAL>↑(Nat.fib (n + 2)) = ∑ x : Fin 2, ![1, 1] x * ↑(Nat.fib (n + ↑x))
<VAR>α : Type u_1<VAR>inst✝ : CommSemiring α<VAR>n : ℕ<GOAL>↑(Nat.fib (n + 1) + Nat.fib n) = ∑ x : Fin 2, ![1, 1] x * ↑(Nat.fib (n + ↑x))
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ s : Multiset α<VAR>b : α<GOAL>filter (Eq b) s = replicate (count b s) b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l : List α<VAR>h : a ∉ l.dedup<GOAL>∀ b ∈ pwFilter (fun x x_1 => x ≠ x_1) l, a ≠ b
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i : ι<VAR>c : R<VAR>x : M<VAR>s : Set ι<VAR>m : M<VAR>hm : m ∈ span R (⇑b '' s)<GOAL>↑(b.repr m).support ⊆ s
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i : ι<VAR>c : R<VAR>x : M<VAR>s : Set ι<VAR>l : ι →₀ R<VAR>hl : l ∈ Finsupp.supported R R s<VAR>hm : (Finsupp.total ι M R ⇑b) l ∈ span R (⇑b '' s)<GOAL>↑(b.repr ((Finsupp.total ι M R ⇑b) l)).support ⊆ s
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : CommRing A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsDomain B<VAR>p : A[X]<VAR>f : A →+* B<VAR>hf : Function.Injective ⇑f<VAR>hp0 : ¬p = 0<GOAL>Multiset.card p.roots ≤ Multiset.card (map f p).roots
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>n : ℕ<VAR>hp : p ≠ 0<VAR>H : ↑n ≤ p.trailingDegree<GOAL>n ≤ p.natTrailingDegree
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>inst✝¹⁴ : NormedSpace 𝕜 F<VAR>inst✝¹³ : TopologicalSpace (TotalSpace F E)<VAR>inst✝¹² : (x : B) → TopologicalSpace (E x)<VAR>EB : Type u_7<VAR>inst✝¹¹ : NormedAddCommGroup EB<VAR>inst✝¹⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>E' : B → Type u_9<VAR>inst✝⁸ : (x : B) → Zero (E' x)<VAR>EM : Type u_10<VAR>inst✝⁷ : NormedAddCommGroup EM<VAR>inst✝⁶ : NormedSpace 𝕜 EM<VAR>HM : Type u_11<VAR>inst✝⁵ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : ChartedSpace HB B<VAR>inst✝ : FiberBundle F E<VAR>x : TotalSpace F E<GOAL>ContMDiffAt (IB.prod 𝓘(𝕜, F)) IB n TotalSpace.proj x
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>inst✝¹⁴ : NormedSpace 𝕜 F<VAR>inst✝¹³ : TopologicalSpace (TotalSpace F E)<VAR>inst✝¹² : (x : B) → TopologicalSpace (E x)<VAR>EB : Type u_7<VAR>inst✝¹¹ : NormedAddCommGroup EB<VAR>inst✝¹⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>E' : B → Type u_9<VAR>inst✝⁸ : (x : B) → Zero (E' x)<VAR>EM : Type u_10<VAR>inst✝⁷ : NormedAddCommGroup EM<VAR>inst✝⁶ : NormedSpace 𝕜 EM<VAR>HM : Type u_11<VAR>inst✝⁵ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : ChartedSpace HB B<VAR>inst✝ : FiberBundle F E<VAR>x : TotalSpace F E<VAR>this : ContMDiffAt (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n id x<GOAL>ContMDiffAt (IB.prod 𝓘(𝕜, F)) IB n TotalSpace.proj x
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>inst✝¹⁴ : NormedSpace 𝕜 F<VAR>inst✝¹³ : TopologicalSpace (TotalSpace F E)<VAR>inst✝¹² : (x : B) → TopologicalSpace (E x)<VAR>EB : Type u_7<VAR>inst✝¹¹ : NormedAddCommGroup EB<VAR>inst✝¹⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>E' : B → Type u_9<VAR>inst✝⁸ : (x : B) → Zero (E' x)<VAR>EM : Type u_10<VAR>inst✝⁷ : NormedAddCommGroup EM<VAR>inst✝⁶ : NormedSpace 𝕜 EM<VAR>HM : Type u_11<VAR>inst✝⁵ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : ChartedSpace HB B<VAR>inst✝ : FiberBundle F E<VAR>x : TotalSpace F E<VAR>this : ContMDiffAt (IB.prod 𝓘(𝕜, F)) IB n (fun x => (id x).proj) x ∧ ContMDiffAt (IB.prod 𝓘(𝕜, F)) 𝓘(𝕜, F) n (fun x_1 => (↑(trivializationAt F E (id x).proj) (id x_1)).2) x<GOAL>ContMDiffAt (IB.prod 𝓘(𝕜, F)) IB n TotalSpace.proj x
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>f : α → β<VAR>s t : Multiset α<VAR>h : s < t<GOAL>map f s < map f t
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>f : α → β<VAR>s t : Multiset α<VAR>h : s < t<VAR>H : map f t ≤ map f s<GOAL>card t ≤ card s
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>f : α → β<VAR>s t : Multiset α<VAR>h : s < t<VAR>H : map f t ≤ map f s<GOAL>card (map f t) ≤ card (map f s)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁰ : MeasurableSpace α<VAR>inst✝⁹ : MeasurableSpace α'<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : MeasurableSpace β'<VAR>inst✝⁶ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f : α × β → E<VAR>s : Set α<VAR>t : Set β<VAR>hf : IntegrableOn f (s ×ˢ t) (μ.prod ν)<GOAL>∫ (z : α × β) in s ×ˢ t, f z ∂μ.prod ν = ∫ (x : α) in s, ∫ (y : β) in t, f (x, y) ∂ν ∂μ
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁰ : MeasurableSpace α<VAR>inst✝⁹ : MeasurableSpace α'<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : MeasurableSpace β'<VAR>inst✝⁶ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f : α × β → E<VAR>s : Set α<VAR>t : Set β<VAR>hf : Integrable f ((μ.restrict s).prod (ν.restrict t))<GOAL>∫ (z : α × β), f z ∂(μ.restrict s).prod (ν.restrict t) = ∫ (x : α) in s, ∫ (y : β) in t, f (x, y) ∂ν ∂μ
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : CancelMonoidWithZero M₀<VAR>a b c : M₀<VAR>hb : b ≠ 0<GOAL>a * b = b ↔ a = 1
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : ∀ (x : α), (𝓝[<] x).NeBot<VAR>s : Set α<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) s<GOAL>interior s = ∅
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : ∀ (x : α), (𝓝[<] x).NeBot<VAR>s : Set α<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) s<VAR>x : α<VAR>hx : x ∈ interior s<GOAL>False
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : ∀ (x : α), (𝓝[<] x).NeBot<VAR>s : Set α<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) s<VAR>x : α<VAR>hx : x ∈ interior s<VAR>this : ∀ᶠ (y : α) in 𝓝 x, y ∈ s<GOAL>False
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : ∀ (x : α), (𝓝[<] x).NeBot<VAR>s : Set α<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) s<VAR>x : α<VAR>hx : x ∈ interior s<VAR>this : ∀ᶠ (y : α) in 𝓝 x, y ∈ s<VAR>y : α<VAR>hyx : y < x<VAR>hys : y ∈ s<GOAL>False
<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>e : ι₂ ↪ ι<VAR>p : ι → P<GOAL>centroid k (map e s₂) p = centroid k s₂ (p ∘ ⇑e)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g✝ : α → β<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq γ<VAR>f : γ → β<VAR>g : α → γ<GOAL>∏ a ∈ s, f (g a) = ∏ b ∈ image g s, f b ^ (filter (fun a => g a = b) s).card
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x✝ y : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>hs : IsCompact s<VAR>hne : s.Nonempty<VAR>x : α<GOAL>∃ y ∈ s, infEdist x s = edist x y
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x✝ y : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>hs : IsCompact s<VAR>hne : s.Nonempty<VAR>x : α<VAR>A : Continuous fun y => edist x y<GOAL>∃ y ∈ s, infEdist x s = edist x y
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x✝ y✝ : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>hs : IsCompact s<VAR>hne : s.Nonempty<VAR>x : α<VAR>A : Continuous fun y => edist x y<VAR>y : α<VAR>ys : y ∈ s<VAR>hy : IsMinOn (fun y => edist x y) s y<GOAL>∃ y ∈ s, infEdist x s = edist x y
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>j : ℕ<GOAL>(cs.leftInvSeq ω).getD j 1 * (cs.leftInvSeq ω).getD j 1 = 1
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>j : ℕ<GOAL>cs.wordProd (take j ω) * ((Option.map cs.simple (ω.get? j)).getD 1 * ((cs.wordProd (take j ω))⁻¹ * (cs.wordProd (take j ω) * ((Option.map cs.simple (ω.get? j)).getD 1 * (cs.wordProd (take j ω))⁻¹)))) = 1
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>A : Type u_2<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>M : Type u_3<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module A M<VAR>inst✝³ : Module R M<VAR>D✝ D1 D2 : Derivation R A M<VAR>r : R<VAR>a✝ b✝ : A<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Module K M<VAR>inst✝ : Algebra R K<VAR>D : Derivation R K M<VAR>a b : K<VAR>h : D b = 0<GOAL>D (a / b) = b⁻¹ • D a
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>A : Type u_2<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>M : Type u_3<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module A M<VAR>inst✝³ : Module R M<VAR>D✝ D1 D2 : Derivation R A M<VAR>r : R<VAR>a✝ b✝ : A<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Module K M<VAR>inst✝ : Algebra R K<VAR>D : Derivation R K M<VAR>a b : K<VAR>h : D b = 0<GOAL>((b ^ 2)⁻¹ * b) • D a = b⁻¹ • D a
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>A : Type u_2<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>M : Type u_3<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module A M<VAR>inst✝³ : Module R M<VAR>D✝ D1 D2 : Derivation R A M<VAR>r : R<VAR>a✝ b✝ : A<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Module K M<VAR>inst✝ : Algebra R K<VAR>D : Derivation R K M<VAR>a b : K<VAR>h : D b = 0<GOAL>((b ^ 2)⁻¹ * b) • D a = (b⁻¹ * b⁻¹ * b) • D a
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝² : Preorder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝¹ : atTop.IsCountablyGenerated<VAR>inst✝ : atTop.NeBot<VAR>hτ : IsStoppingTime f τ<VAR>s : Set Ω<VAR>hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})<GOAL>MeasurableSet s
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝² : Preorder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝¹ : atTop.IsCountablyGenerated<VAR>inst✝ : atTop.NeBot<VAR>hτ : IsStoppingTime f τ<VAR>s : Set Ω<VAR>hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})<VAR>seq : ℕ → ι<VAR>h_seq_tendsto : Tendsto seq atTop atTop<GOAL>MeasurableSet s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>hdomain : IsDomain R<VAR>r s : R<VAR>p q : R[X]<VAR>f : RatFunc R<GOAL>(laurent r) X = X + C r
<VAR>l : List ℕ+<VAR>h : ∀ p ∈ l, p.Prime<GOAL>(ofPNatList l h).prod = l.prod
<VAR>l : List ℕ+<VAR>h : ∀ p ∈ l, p.Prime<VAR>this : (ofPNatMultiset (↑l) h).prod = (↑l).prod<GOAL>(ofPNatList l h).prod = l.prod
<VAR>l : List ℕ+<VAR>h : ∀ p ∈ l, p.Prime<VAR>this : (ofPNatMultiset (↑l) h).prod = l.prod<GOAL>(ofPNatList l h).prod = l.prod
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m m₁ m₂ : OuterMeasure α<VAR>s : Set α<GOAL>(m₁ ⊔ m₂) s = m₁ s ⊔ m₂ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m m₁ m₂ : OuterMeasure α<VAR>s : Set α<VAR>this : (⨆ i, bif i then m₁ else m₂) s = ⨆ i, (bif i then m₁ else m₂) s<GOAL>(m₁ ⊔ m₂) s = m₁ s ⊔ m₂ s
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>h : a * c ≤ b * c<VAR>hc : 0 < c<GOAL>c * a ≤ c * b
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsPrincipalIdealRing R<VAR>S : Ideal R<VAR>hpi : S.IsPrime<VAR>hS : S ≠ ⊥<VAR>T : Ideal R<VAR>x : R<VAR>hST : S ≤ T<VAR>hxS : x ∉ S<VAR>hxT : x ∈ T<GOAL>1 ∈ T
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsPrincipalIdealRing R<VAR>S : Ideal R<VAR>hpi : S.IsPrime<VAR>hS : S ≠ ⊥<VAR>T : Ideal R<VAR>x : R<VAR>hST : S ≤ T<VAR>hxS : x ∉ S<VAR>hxT : x ∈ T<VAR>z : R<VAR>hz : generator S = generator T * z<GOAL>1 ∈ T
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<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✝¹¹ : Module.Free R M<VAR>inst✝¹⁰ : Module.Finite R M<VAR>inst✝⁹ : Module.Free R L<VAR>inst✝⁸ : Module.Finite R L<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : LieAlgebra K L<VAR>inst✝⁵ : Module K M<VAR>inst✝⁴ : LieModule K L M<VAR>inst✝³ : FiniteDimensional K M<VAR>inst✝² : LieAlgebra.IsNilpotent K L<VAR>inst✝¹ : LinearWeights K L M<VAR>inst✝ : IsTriangularizable K L M<VAR>x✝ y✝ : L<GOAL>((traceForm K L M) x✝) y✝ = ((∑ χ : Weight K L M, finrank K ↥↑(weightSpace M ⇑χ) • (Weight.toLinear K L M χ).smulRight (Weight.toLinear K L M χ)) x✝) y✝
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<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✝¹¹ : Module.Free R M<VAR>inst✝¹⁰ : Module.Finite R M<VAR>inst✝⁹ : Module.Free R L<VAR>inst✝⁸ : Module.Finite R L<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : LieAlgebra K L<VAR>inst✝⁵ : Module K M<VAR>inst✝⁴ : LieModule K L M<VAR>inst✝³ : FiniteDimensional K M<VAR>inst✝² : LieAlgebra.IsNilpotent K L<VAR>inst✝¹ : LinearWeights K L M<VAR>inst✝ : IsTriangularizable K L M<VAR>x✝ y✝ : L<GOAL>∑ x ∈ Finset.univ.attach, finrank K ↥↑(weightSpace M ⇑↑x) • (↑x x✝ * ↑x y✝) = ((∑ χ : Weight K L M, finrank K ↥↑(weightSpace M ⇑χ) • (Weight.toLinear K L M χ).smulRight (Weight.toLinear K L M χ)) x✝) y✝
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : Monoid M<VAR>a x y : M<GOAL>y ∈ closure {x} ↔ ∃ n, x ^ n = y
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : Monoid M<VAR>a x y : M<GOAL>(∃ x_1, ((powersHom M) x) x_1 = y) ↔ ∃ n, x ^ n = y
<VAR>a x z✝ z : ℂ<VAR>h₁ : 0 ≤ z.im<VAR>h₂ : z ≠ 0<GOAL>z.arg = Real.arccos (z.re / abs z)
<VAR>b o : Ordinal.{u_1}<VAR>hb : 1 < b<VAR>ho : o ≠ 0<VAR>hbo : b ≤ o<GOAL>0 < log b o
<VAR>ι : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : ConditionallyCompleteLattice G<VAR>inst✝¹ : CovariantClass G G (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : Nonempty ι<VAR>f : ι → G<VAR>hf : BddAbove (range f)<VAR>a : G<GOAL>(⨆ i, f i) / a = ⨆ i, f i / a
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : MulAction G α<VAR>inst✝⁵ : MeasurableSpace α<VAR>ν : Measure α<VAR>inst✝⁴ : Countable G<VAR>inst✝³ : MeasurableSpace G<VAR>inst✝² : SMulInvariantMeasure G α ν<VAR>inst✝¹ : MeasurableSMul G α<VAR>μ : Measure (Quotient α_mod_G)<VAR>inst✝ : QuotientMeasureEqMeasurePreimage ν μ<VAR>hasFun : HasFundamentalDomain G α ν<VAR>h : covolume G α ν ≠ ⊤<GOAL>IsFiniteMeasure μ
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : MulAction G α<VAR>inst✝⁵ : MeasurableSpace α<VAR>ν : Measure α<VAR>inst✝⁴ : Countable G<VAR>inst✝³ : MeasurableSpace G<VAR>inst✝² : SMulInvariantMeasure G α ν<VAR>inst✝¹ : MeasurableSMul G α<VAR>μ : Measure (Quotient α_mod_G)<VAR>inst✝ : QuotientMeasureEqMeasurePreimage ν μ<VAR>hasFun : HasFundamentalDomain G α ν<VAR>h : covolume G α ν ≠ ⊤<VAR>𝓕 : Set α<VAR>h𝓕 : IsFundamentalDomain G 𝓕 ν<GOAL>IsFiniteMeasure μ
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : MulAction G α<VAR>inst✝⁵ : MeasurableSpace α<VAR>ν : Measure α<VAR>inst✝⁴ : Countable G<VAR>inst✝³ : MeasurableSpace G<VAR>inst✝² : SMulInvariantMeasure G α ν<VAR>inst✝¹ : MeasurableSMul G α<VAR>μ : Measure (Quotient α_mod_G)<VAR>inst✝ : QuotientMeasureEqMeasurePreimage ν μ<VAR>hasFun : HasFundamentalDomain G α ν<VAR>h : covolume G α ν ≠ ⊤<VAR>𝓕 : Set α<VAR>h𝓕 : IsFundamentalDomain G 𝓕 ν<GOAL>IsFiniteMeasure (Measure.map (Quotient.mk α_mod_G) (ν.restrict 𝓕))
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : MulAction G α<VAR>inst✝⁵ : MeasurableSpace α<VAR>ν : Measure α<VAR>inst✝⁴ : Countable G<VAR>inst✝³ : MeasurableSpace G<VAR>inst✝² : SMulInvariantMeasure G α ν<VAR>inst✝¹ : MeasurableSMul G α<VAR>μ : Measure (Quotient α_mod_G)<VAR>inst✝ : QuotientMeasureEqMeasurePreimage ν μ<VAR>hasFun : HasFundamentalDomain G α ν<VAR>h : covolume G α ν ≠ ⊤<VAR>𝓕 : Set α<VAR>h𝓕 : IsFundamentalDomain G 𝓕 ν<VAR>this : Fact (ν 𝓕 < ⊤)<GOAL>IsFiniteMeasure (Measure.map (Quotient.mk α_mod_G) (ν.restrict 𝓕))
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>s t : Set α<VAR>a : α<VAR>hs : IsUpperSet s<GOAL>IsUpperSet (s / t)
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>s t : Set α<VAR>a : α<VAR>hs : IsUpperSet s<GOAL>IsUpperSet (s * t⁻¹)
<VAR>U : Type u_1<VAR>inst✝ : Quiver U<VAR>u v u' v' : U<VAR>hu : u = u'<VAR>hv : v = v'<VAR>e : u ⟶ v<VAR>e' : u' ⟶ v'<GOAL>e' = cast hu hv e ↔ HEq e' e
<VAR>U : Type u_1<VAR>inst✝ : Quiver U<VAR>u v u' v' : U<VAR>hu : u = u'<VAR>hv : v = v'<VAR>e : u ⟶ v<VAR>e' : u' ⟶ v'<GOAL>HEq e e' ↔ HEq e' e
<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<VAR>f : X → Y<VAR>inst✝ : LindelofSpace X<VAR>hf : Continuous f<VAR>hsur : Function.Surjective f<GOAL>IsLindelof univ
<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<VAR>f : X → Y<VAR>inst✝ : LindelofSpace X<VAR>hf : Continuous f<VAR>hsur : Function.Surjective f<GOAL>IsLindelof (f '' univ)