ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : AddCommMonoid N<VAR>inst✝⁷ : Module R N<VAR>A₁ : Type u_6<VAR>B₁ : Type u_7<VAR>A₂ : Type u_8<VAR>B₂ : Type u_9<VAR>inst✝⁶ : CommRing A₁<VAR>inst✝⁵ : CommRing B₁<VAR>inst✝⁴ : CommRing A₂<VAR>inst✝³ : CommRing B₂<VAR>inst✝² : Algebra A₁ B₁<VAR>inst✝¹ : Algebra A₂ B₂<VAR>e₁ : A₁ ≃+* A₂<VAR>e₂ : B₁ ≃+* B₂<VAR>he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)<VAR>inst✝ : Finite A₁ B₁<VAR>this✝¹ : Algebra A₁ A₂ := e₁.toRingHom.toAlgebra<VAR>this✝ : Algebra A₂ B₁ := ((algebraMap A₁ B₁).comp e₁.symm.toRingHom).toAlgebra<VAR>this : IsScalarTower A₁ A₂ B₁<VAR>e : B₁ ≃ₐ[A₂] B₂ := { toEquiv := e₂.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }<GOAL>Finite A₂ B₂
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : AddCommMonoid N<VAR>inst✝⁷ : Module R N<VAR>A₁ : Type u_6<VAR>B₁ : Type u_7<VAR>A₂ : Type u_8<VAR>B₂ : Type u_9<VAR>inst✝⁶ : CommRing A₁<VAR>inst✝⁵ : CommRing B₁<VAR>inst✝⁴ : CommRing A₂<VAR>inst✝³ : CommRing B₂<VAR>inst✝² : Algebra A₁ B₁<VAR>inst✝¹ : Algebra A₂ B₂<VAR>e₁ : A₁ ≃+* A₂<VAR>e₂ : B₁ ≃+* B₂<VAR>he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)<VAR>inst✝ : Finite A₁ B₁<VAR>this✝² : Algebra A₁ A₂ := e₁.toRingHom.toAlgebra<VAR>this✝¹ : Algebra A₂ B₁ := ((algebraMap A₁ B₁).comp e₁.symm.toRingHom).toAlgebra<VAR>this✝ : IsScalarTower A₁ A₂ B₁<VAR>e : B₁ ≃ₐ[A₂] B₂ := { toEquiv := e₂.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }<VAR>this : Finite A₂ B₁<GOAL>Finite A₂ B₂
<VAR>G : Type u_1<VAR>inst✝ : DivisionMonoid G<VAR>a b c d : G<VAR>hbc : Commute b c<VAR>hbd : Commute b⁻¹ d<VAR>hcd : Commute c⁻¹ d<GOAL>a / b / (c / d) = a / c / (b / d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>s : Set α<VAR>hs' : s.Nonempty<VAR>s_mble : MeasurableSet s<GOAL>count s ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>s : Set α<VAR>hs' : s.Nonempty<VAR>s_mble : MeasurableSet s<GOAL>¬s = ∅
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>A : Mon_ (C ⥤ D)<VAR>X✝ Y✝ : C<VAR>f : X✝ ⟶ Y✝<GOAL>((fun X => { X := A.X.obj X, one := A.one.app X, mul := A.mul.app X, one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }) X✝).one ≫ A.X.map f = ((fun X => { X := A.X.obj X, one := A.one.app X, mul := A.mul.app X, one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }) Y✝).one
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>A : Mon_ (C ⥤ D)<VAR>X✝ Y✝ : C<VAR>f : X✝ ⟶ Y✝<GOAL>𝟙 (𝟙_ D) ≫ A.one.app Y✝ = ((fun X => { X := A.X.obj X, one := A.one.app X, mul := A.mul.app X, one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }) Y✝).one
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>A : Mon_ (C ⥤ D)<VAR>X✝ Y✝ : C<VAR>f : X✝ ⟶ Y✝<GOAL>𝟙 (𝟙_ D) ≫ A.one.app Y✝ = A.one.app Y✝
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>A : Mon_ (C ⥤ D)<VAR>X✝ Y✝ : C<VAR>f : X✝ ⟶ Y✝<GOAL>A.mul.app X✝ ≫ A.X.map f = (A.X.map f ⊗ A.X.map f) ≫ A.mul.app Y✝
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>A : Mon_ (C ⥤ D)<VAR>X : C<GOAL>A.X.map (𝟙 X) = 𝟙 (A.X.obj X)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>A : Mon_ (C ⥤ D)<VAR>X✝ Y✝ Z✝ : C<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<GOAL>A.X.map (f ≫ g) = A.X.map f ≫ A.X.map g
<VAR>α : Type u_1<VAR>inst✝ : AddCommMonoid α<VAR>k : α<VAR>n : ℕ<VAR>x a a' : α<VAR>h : k + a = a'<GOAL>k + term n x a = term n x a'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>s t : UpperSet α<VAR>a : α<VAR>f : ι → UpperSet α<GOAL>↑(⨆ i, f i).compl = ↑(⨆ i, (f i).compl)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype n'<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis n' R M₂<VAR>J J₂ : Matrix n n R<VAR>J' : Matrix n' n' R<VAR>A : Matrix n' n R<VAR>A' : Matrix n n' R<VAR>A₁ A₂ : Matrix n n R<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : DecidableEq n'<GOAL>((toLinearMap₂' R) J).IsAdjointPair ((toLinearMap₂' R) J') (toLin' A) (toLin' A') ↔ J.IsAdjointPair J' A A'
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype n'<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis n' R M₂<VAR>J J₂ : Matrix n n R<VAR>J' : Matrix n' n' R<VAR>A : Matrix n' n R<VAR>A' : Matrix n n' R<VAR>A₁ A₂ : Matrix n n R<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : DecidableEq n'<GOAL>(toLinearMap₂' R) J' ∘ₗ toLin' A = ((toLinearMap₂' R) J).compl₂ (toLin' A') ↔ J.IsAdjointPair J' A A'
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype n'<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis n' R M₂<VAR>J J₂ : Matrix n n R<VAR>J' : Matrix n' n' R<VAR>A : Matrix n' n R<VAR>A' : Matrix n n' R<VAR>A₁ A₂ : Matrix n n R<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : DecidableEq n'<VAR>h : ∀ (B B' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R), B = B' ↔ (toMatrix₂' R) B = (toMatrix₂' R) B'<GOAL>(toLinearMap₂' R) J' ∘ₗ toLin' A = ((toLinearMap₂' R) J).compl₂ (toLin' A') ↔ J.IsAdjointPair J' A A'
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype n'<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis n' R M₂<VAR>J J₂ : Matrix n n R<VAR>J' : Matrix n' n' R<VAR>A : Matrix n' n R<VAR>A' : Matrix n n' R<VAR>A₁ A₂ : Matrix n n R<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : DecidableEq n'<VAR>h : ∀ (B B' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R), B = B' ↔ (toMatrix₂' R) B = (toMatrix₂' R) B'<GOAL>Aᵀ * J' = J * A' ↔ J.IsAdjointPair J' A A'
<VAR>V : Type u<VAR>G✝ : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G✝.Coloring α<VAR>G : SimpleGraph V<GOAL>G.chromaticNumber = ⨅ n, ↑↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝ : μ.WeaklyRegular<VAR>x : ℝ≥0∞<VAR>hx : x ≠ ⊤<GOAL>(x • μ).WeaklyRegular
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝ : μ.WeaklyRegular<VAR>x : ℝ≥0∞<VAR>hx : x ≠ ⊤<VAR>this : (x • μ).OuterRegular<GOAL>(x • μ).WeaklyRegular
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z✝ : ℤ<VAR>a✝ a : α<VAR>z : ℤ<GOAL>⌈a - ↑z⌉ = ⌈a + ↑(-z)⌉
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : Group G'<VAR>inst✝⁵ : Group G''<VAR>A : Type u_4<VAR>inst✝⁴ : AddGroup A<VAR>M : Type u_5<VAR>S : Type u_6<VAR>inst✝³ : DivInvMonoid M<VAR>inst✝² : SetLike S M<VAR>hSM : SubgroupClass S M<VAR>H✝ K✝ : S<VAR>inst✝¹ : SetLike S G<VAR>inst✝ : SubgroupClass S G<VAR>H K : S<VAR>hH : H ≤ K<VAR>x✝ : ↥H<GOAL>((↑K).comp (inclusion hH)) x✝ = ↑H x✝
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : Semiring S<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>α' : Type u_7<VAR>M' : Type u_8<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>v : α → M<VAR>v' : α' → M'<VAR>s : Set α<GOAL>span R (v '' s) = map (Finsupp.total α M R v) (supported R R s)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : Semiring S<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>α' : Type u_7<VAR>M' : Type u_8<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>v : α → M<VAR>v' : α' → M'<VAR>s : Set α<GOAL>v '' s ⊆ ↑(map (Finsupp.total α M R v) (supported R R s))
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : Semiring S<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>α' : Type u_7<VAR>M' : Type u_8<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>v : α → M<VAR>v' : α' → M'<VAR>s : Set α<GOAL>map (Finsupp.total α M R v) (supported R R s) ≤ span R (v '' s)
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ<VAR>inst✝¹ : Zero R<VAR>a b : Γ<VAR>r : R<VAR>inst✝ : Zero Γ<VAR>x : HahnSeries Γ R<VAR>hx : x ≠ 0<GOAL>x.coeff x.order ≠ 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ<VAR>inst✝¹ : Zero R<VAR>a b : Γ<VAR>r : R<VAR>inst✝ : Zero Γ<VAR>x : HahnSeries Γ R<VAR>hx : x ≠ 0<GOAL>x.coeff (⋯.min ⋯) ≠ 0
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>inst✝ : StrongRankCondition R<VAR>ι : Type v<VAR>v : Basis ι R M<GOAL>#ι = Module.rank R M
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>inst✝ : StrongRankCondition R<VAR>ι : Type v<VAR>v : Basis ι R M<VAR>this : Nontrivial R<GOAL>#ι = Module.rank R M
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>inst✝ : StrongRankCondition R<VAR>ι : Type v<VAR>v : Basis ι R M<VAR>this : Nontrivial R<GOAL>#ι = ⨆ ι, #↑↑ι
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>inst✝ : StrongRankCondition R<VAR>ι : Type v<VAR>v : Basis ι R M<VAR>this : Nontrivial R<GOAL>#ι ≤ ⨆ ι, #↑↑ι
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>inst✝ : StrongRankCondition R<VAR>ι : Type v<VAR>v : Basis ι R M<VAR>this : Nontrivial R<GOAL>⨆ ι, #↑↑ι ≤ #ι
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>hl : l.Balanced<VAR>hr : r.Balanced<VAR>sl : l.Sized<VAR>sr : r.Sized<VAR>H : (∃ l', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'<GOAL>(l.balanceL x r).size = l.size + r.size + 1
<VAR>R : Type u<VAR>inst✝³ : CommSemiring R<VAR>S : Type v<VAR>inst✝² : CommSemiring S<VAR>p q : ℕ<VAR>inst✝¹ : CharP R p<VAR>inst✝ : NoZeroDivisors R<VAR>f : R[X]<VAR>hf : derivative f = 0<VAR>hp : p ≠ 0<VAR>n : ℕ<GOAL>((expand R p) (contract p f)).coeff n = f.coeff n
<VAR>R : Type u<VAR>inst✝³ : CommSemiring R<VAR>S : Type v<VAR>inst✝² : CommSemiring S<VAR>p q : ℕ<VAR>inst✝¹ : CharP R p<VAR>inst✝ : NoZeroDivisors R<VAR>f : R[X]<VAR>hf : derivative f = 0<VAR>hp : p ≠ 0<VAR>n : ℕ<GOAL>(if p ∣ n then f.coeff (n / p * p) else 0) = f.coeff n
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>n : ℕ<GOAL>PInfty.f n ≫ (𝟙 K[X] - PInfty).f n = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : SupSet α<VAR>f✝ g : ι → α<VAR>s : Set β<VAR>f : β → α<GOAL>sSup (f '' s) = ⨆ a, f ↑a
<VAR>α β γ✝ : Type u<VAR>S✝ S' : Set (α → ℕ)<VAR>S : Set (α ⊕ β → ℕ)<VAR>γ : Type u<VAR>p : Poly ((α ⊕ β) ⊕ γ)<VAR>pe : ∀ (v : α ⊕ β → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0<VAR>v : α → ℕ<VAR>x✝ : {v | ∃ x, v ⊗ x ∈ S} v<VAR>x : β → ℕ<VAR>hx : v ⊗ x ∈ S<VAR>t : γ → ℕ<VAR>ht : p ((v ⊗ x) ⊗ t) = 0<GOAL>p ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) = 0
<VAR>α β γ✝ : Type u<VAR>S✝ S' : Set (α → ℕ)<VAR>S : Set (α ⊕ β → ℕ)<VAR>γ : Type u<VAR>p : Poly ((α ⊕ β) ⊕ γ)<VAR>pe : ∀ (v : α ⊕ β → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0<VAR>v : α → ℕ<VAR>x✝ : {v | ∃ x, v ⊗ x ∈ S} v<VAR>x : β → ℕ<VAR>hx : v ⊗ x ∈ S<VAR>t : γ → ℕ<VAR>ht : p ((v ⊗ x) ⊗ t) = 0<GOAL>p ((v ⊗ x) ⊗ t) = 0
<VAR>α β γ✝ : Type u<VAR>S✝ S' : Set (α → ℕ)<VAR>S : Set (α ⊕ β → ℕ)<VAR>γ : Type u<VAR>p : Poly ((α ⊕ β) ⊕ γ)<VAR>pe : ∀ (v : α ⊕ β → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0<VAR>v : α → ℕ<VAR>x✝ : ∃ t, (Poly.map ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) p) (v ⊗ t) = 0<VAR>t : β ⊕ γ → ℕ<VAR>ht : (Poly.map ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) p) (v ⊗ t) = 0<GOAL>p ((v ⊗ t ∘ inl) ⊗ t ∘ inr) = 0
<VAR>α β γ✝ : Type u<VAR>S✝ S' : Set (α → ℕ)<VAR>S : Set (α ⊕ β → ℕ)<VAR>γ : Type u<VAR>p : Poly ((α ⊕ β) ⊕ γ)<VAR>pe : ∀ (v : α ⊕ β → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0<VAR>v : α → ℕ<VAR>x✝ : ∃ t, (Poly.map ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) p) (v ⊗ t) = 0<VAR>t : β ⊕ γ → ℕ<VAR>ht : p ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) = 0<GOAL>p ((v ⊗ t ∘ inl) ⊗ t ∘ inr) = 0
<VAR>α : Type u_1<VAR>inst✝¹ : CommMonoidWithZero α<VAR>inst✝ : WfDvdMonoid α<VAR>a₀ x : α<VAR>h : a₀ ≠ 0<VAR>hx : ¬IsUnit x<GOAL>∃ n a, ¬x ∣ a ∧ a₀ = x ^ n * a
<VAR>α : Type u_1<VAR>inst✝¹ : CommMonoidWithZero α<VAR>inst✝ : WfDvdMonoid α<VAR>x : α<VAR>hx : ¬IsUnit x<VAR>a : α<VAR>n : ℕ<VAR>h : x ^ n * a ≠ 0<VAR>hm : ∀ x_1 ∈ {a_1 | ∃ n_1, x ^ n_1 * a_1 = x ^ n * a}, ¬DvdNotUnit x_1 a<GOAL>∃ n_1 a_1, ¬x ∣ a_1 ∧ x ^ n * a = x ^ n_1 * a_1
<VAR>α : Type u_1<VAR>inst✝¹ : CommMonoidWithZero α<VAR>inst✝ : WfDvdMonoid α<VAR>x : α<VAR>hx : ¬IsUnit x<VAR>n : ℕ<VAR>d : α<VAR>h : x ^ n * (x * d) ≠ 0<VAR>hm : ∀ x_1 ∈ {a | ∃ n_1, x ^ n_1 * a = x ^ n * (x * d)}, ¬DvdNotUnit x_1 (x * d)<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝¹ : Ring R<VAR>a b : R<VAR>inst✝ : NoZeroDivisors R<VAR>h : Commute a b<GOAL>a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field F<VAR>i : K →+* L<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : Algebra R L<VAR>P : K[X]<VAR>hmo : P.Monic<VAR>hP : Splits (RingHom.id K) P<GOAL>P.coeff 0 = (-1) ^ P.natDegree * P.roots.prod
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field F<VAR>i : K →+* L<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : Algebra R L<VAR>P : K[X]<VAR>hmo : P.Monic<VAR>hP : Splits (RingHom.id K) P<GOAL>(Multiset.map (fun a => X - C a) P.roots).prod.coeff 0 = (-1) ^ P.natDegree * P.roots.prod
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field F<VAR>i : K →+* L<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : Algebra R L<VAR>P : K[X]<VAR>hmo : P.Monic<VAR>hP : Splits (RingHom.id K) P<GOAL>(Multiset.map (eval 0 ∘ fun a => X - C a) P.roots).prod = (-1) ^ P.natDegree * P.roots.prod
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field F<VAR>i : K →+* L<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : Algebra R L<VAR>P : K[X]<VAR>hmo : P.Monic<VAR>hP : Splits (RingHom.id K) P<GOAL>(Multiset.map (fun x => -x) P.roots).prod = (-1) ^ P.natDegree * P.roots.prod
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field F<VAR>i : K →+* L<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : Algebra R L<VAR>P : K[X]<VAR>hmo : P.Monic<VAR>hP : Splits (RingHom.id K) P<GOAL>(Multiset.map (HMul.hMul (-1)) P.roots).prod = (-1) ^ P.natDegree * P.roots.prod
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝¹ : ConditionallyCompleteLinearOrderBot α<VAR>s : Set α<VAR>f✝ : ι → α<VAR>a : α<VAR>inst✝ : IsEmpty ι<VAR>f : ι → α<GOAL>⨆ i, f i = ⊥
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>a : α<VAR>s t : Multiset α<VAR>f✝ g : α → Multiset β<VAR>l : List α<VAR>f : α → List β<GOAL>((↑l).bind fun a => ↑(f a)) = ↑(l.bind f)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>a : α<VAR>s t : Multiset α<VAR>f✝ g : α → Multiset β<VAR>l : List α<VAR>f : α → List β<GOAL>((↑l).bind fun a => ↑(f a)) = (↑(List.map (ofList ∘ f) l)).join
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : R1Space X<VAR>x y : X<VAR>K : Set X<VAR>hK : IsCompact K<GOAL>closure K = ⋃ x ∈ K, closure {x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Sort u_4<VAR>f : ι → Cardinal.{u_5}<VAR>hf : BddAbove (range f)<GOAL>(sSup (range f)).ord = sSup (range fun i => (f i).ord)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Sort u_4<VAR>f : ι → Cardinal.{u_5}<VAR>hf : BddAbove (range f)<GOAL>(range fun i => (f i).ord) = ord '' range f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Sort u_4<VAR>f : ι → Cardinal.{u_5}<VAR>hf : BddAbove (range f)<GOAL>range (ord ∘ f) = ord '' range f
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>inst✝⁹ : MeasurableSpace H<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : BorelSpace G<VAR>μ✝ : Measure G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : μ✝.IsMulLeftInvariant<VAR>inst✝³ : WeaklyLocallyCompactSpace G<VAR>inst✝² : NoncompactSpace G<VAR>μ : Measure G<VAR>inst✝¹ : μ.IsOpenPosMeasure<VAR>inst✝ : μ.IsMulLeftInvariant<GOAL>μ univ = ⊤
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>inst✝⁹ : MeasurableSpace H<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : BorelSpace G<VAR>μ✝ : Measure G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : μ✝.IsMulLeftInvariant<VAR>inst✝³ : WeaklyLocallyCompactSpace G<VAR>inst✝² : NoncompactSpace G<VAR>μ : Measure G<VAR>inst✝¹ : μ.IsOpenPosMeasure<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>K : Set G<VAR>K1 : K ∈ 𝓝 1<VAR>hK : IsCompact K<VAR>Kclosed : IsClosed K<GOAL>μ univ = ⊤
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>inst✝⁹ : MeasurableSpace H<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : BorelSpace G<VAR>μ✝ : Measure G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : μ✝.IsMulLeftInvariant<VAR>inst✝³ : WeaklyLocallyCompactSpace G<VAR>inst✝² : NoncompactSpace G<VAR>μ : Measure G<VAR>inst✝¹ : μ.IsOpenPosMeasure<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>K : Set G<VAR>K1 : K ∈ 𝓝 1<VAR>hK : IsCompact K<VAR>Kclosed : IsClosed K<VAR>K_pos : 0 < μ K<GOAL>μ univ = ⊤
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>inst✝⁹ : MeasurableSpace H<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : BorelSpace G<VAR>μ✝ : Measure G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : μ✝.IsMulLeftInvariant<VAR>inst✝³ : WeaklyLocallyCompactSpace G<VAR>inst✝² : NoncompactSpace G<VAR>μ : Measure G<VAR>inst✝¹ : μ.IsOpenPosMeasure<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>K : Set G<VAR>K1 : K ∈ 𝓝 1<VAR>hK : IsCompact K<VAR>Kclosed : IsClosed K<VAR>K_pos : 0 < μ K<VAR>A : ∀ (L : Set G), IsCompact L → ∃ g, Disjoint L (g • K)<GOAL>μ univ = ⊤
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>inst✝⁹ : MeasurableSpace H<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : BorelSpace G<VAR>μ✝ : Measure G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : μ✝.IsMulLeftInvariant<VAR>inst✝³ : WeaklyLocallyCompactSpace G<VAR>inst✝² : NoncompactSpace G<VAR>μ : Measure G<VAR>inst✝¹ : μ.IsOpenPosMeasure<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>K : Set G<VAR>K1 : K ∈ 𝓝 1<VAR>hK : IsCompact K<VAR>Kclosed : IsClosed K<VAR>K_pos : 0 < μ K<VAR>g : Set G → G<VAR>hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)<VAR>L : ℕ → Set G := fun n => (fun T => T ∪ g T • K)^[n] K<VAR>Lcompact : ∀ (n : ℕ), IsCompact (L n)<VAR>Lclosed : ∀ (n : ℕ), IsClosed (L n)<VAR>M : ∀ (n : ℕ), μ (L n) = ↑(n + 1) * μ K<GOAL>μ univ = ⊤
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>inst✝⁹ : MeasurableSpace H<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : BorelSpace G<VAR>μ✝ : Measure G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : μ✝.IsMulLeftInvariant<VAR>inst✝³ : WeaklyLocallyCompactSpace G<VAR>inst✝² : NoncompactSpace G<VAR>μ : Measure G<VAR>inst✝¹ : μ.IsOpenPosMeasure<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>K : Set G<VAR>K1 : K ∈ 𝓝 1<VAR>hK : IsCompact K<VAR>Kclosed : IsClosed K<VAR>K_pos : 0 < μ K<VAR>g : Set G → G<VAR>hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)<VAR>L : ℕ → Set G := fun n => (fun T => T ∪ g T • K)^[n] K<VAR>Lcompact : ∀ (n : ℕ), IsCompact (L n)<VAR>Lclosed : ∀ (n : ℕ), IsClosed (L n)<VAR>M : ∀ (n : ℕ), μ (L n) = ↑(n + 1) * μ K<VAR>N : Tendsto (fun n => μ (L n)) atTop (𝓝 (⊤ * μ K))<GOAL>μ univ = ⊤
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>inst✝⁹ : MeasurableSpace H<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : BorelSpace G<VAR>μ✝ : Measure G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : μ✝.IsMulLeftInvariant<VAR>inst✝³ : WeaklyLocallyCompactSpace G<VAR>inst✝² : NoncompactSpace G<VAR>μ : Measure G<VAR>inst✝¹ : μ.IsOpenPosMeasure<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>K : Set G<VAR>K1 : K ∈ 𝓝 1<VAR>hK : IsCompact K<VAR>Kclosed : IsClosed K<VAR>K_pos : 0 < μ K<VAR>g : Set G → G<VAR>hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)<VAR>L : ℕ → Set G := fun n => (fun T => T ∪ g T • K)^[n] K<VAR>Lcompact : ∀ (n : ℕ), IsCompact (L n)<VAR>Lclosed : ∀ (n : ℕ), IsClosed (L n)<VAR>M : ∀ (n : ℕ), μ (L n) = ↑(n + 1) * μ K<VAR>N : Tendsto (fun n => μ (L n)) atTop (𝓝 ⊤)<GOAL>μ univ = ⊤
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>inst✝⁹ : MeasurableSpace H<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : BorelSpace G<VAR>μ✝ : Measure G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : μ✝.IsMulLeftInvariant<VAR>inst✝³ : WeaklyLocallyCompactSpace G<VAR>inst✝² : NoncompactSpace G<VAR>μ : Measure G<VAR>inst✝¹ : μ.IsOpenPosMeasure<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>K : Set G<VAR>K1 : K ∈ 𝓝 1<VAR>hK : IsCompact K<VAR>Kclosed : IsClosed K<VAR>K_pos : 0 < μ K<VAR>g : Set G → G<VAR>hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)<VAR>L : ℕ → Set G := fun n => (fun T => T ∪ g T • K)^[n] K<VAR>Lcompact : ∀ (n : ℕ), IsCompact (L n)<VAR>Lclosed : ∀ (n : ℕ), IsClosed (L n)<VAR>M : ∀ (n : ℕ), μ (L n) = ↑(n + 1) * μ K<VAR>N : Tendsto (fun n => μ (L n)) atTop (𝓝 ⊤)<GOAL>⊤ ≤ μ univ