ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : NormalSpace X<VAR>u : ι → Set X<VAR>s : Set X<VAR>v : PartialRefinement u s<VAR>hs : IsClosed s<VAR>i : ι<VAR>hi : i ∉ v.carrier<VAR>I : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ v.toFun i<VAR>C : IsClosed (s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ)<GOAL>∃ v', v < v'
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : NormalSpace X<VAR>u : ι → Set X<VAR>s : Set X<VAR>v : PartialRefinement u s<VAR>hs : IsClosed s<VAR>i : ι<VAR>hi : i ∉ v.carrier<VAR>I : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ v.toFun i<VAR>C : IsClosed (s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ)<VAR>vi : Set X<VAR>ovi : IsOpen vi<VAR>hvi : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ vi<VAR>cvi : closure vi ⊆ v.toFun i<GOAL>∃ v', v < v'
<VAR>q : ℚ<GOAL>Irrational √↑q ↔ Rat.sqrt q * Rat.sqrt q ≠ q ∧ 0 ≤ q
<VAR>q : ℚ<GOAL>¬IsSquare q ∧ 0 ≤ q ↔ (¬∃ q_1, q_1 * q_1 = q) ∧ 0 ≤ q
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : LinearOrder M<VAR>inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>x : M<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>x ^ n = 1 ↔ x = 1
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : LinearOrder M<VAR>inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>x : M<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>x ^ n ≤ 1 ∧ 1 ≤ x ^ n ↔ x ≤ 1 ∧ 1 ≤ x
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G : SimpleGraph V<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : MulZeroOneClass α<VAR>inst✝ : Nontrivial α<VAR>x✝¹ x✝ : V<GOAL>⋯.toGraph.Adj x✝¹ x✝ ↔ G.Adj x✝¹ x✝
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G : SimpleGraph V<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : MulZeroOneClass α<VAR>inst✝ : Nontrivial α<VAR>x✝¹ x✝ : V<GOAL>¬G.Adj x✝¹ x✝ → False ↔ G.Adj x✝¹ x✝
<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✝¹¹ : Group H<VAR>inst✝¹⁰ : MulAction G α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : MulAction H β<VAR>inst✝⁷ : MeasurableSpace β<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : MeasurableSMul G α<VAR>inst✝³ : SMulInvariantMeasure G α μ<VAR>inst✝² : Countable G<VAR>ν : Measure α<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hs : IsFundamentalDomain G s μ<VAR>htm : NullMeasurableSet t μ<VAR>ht : μ s < μ t<GOAL>∃ x ∈ t, ∃ y ∈ t, ∃ g, g ≠ 1 ∧ g • x = y
<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✝¹¹ : Group H<VAR>inst✝¹⁰ : MulAction G α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : MulAction H β<VAR>inst✝⁷ : MeasurableSpace β<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : MeasurableSMul G α<VAR>inst✝³ : SMulInvariantMeasure G α μ<VAR>inst✝² : Countable G<VAR>ν : Measure α<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hs : IsFundamentalDomain G s μ<VAR>htm : NullMeasurableSet t μ<VAR>ht : ∀ x ∈ t, ∀ y ∈ t, ∀ (g : G), g ≠ 1 → g • x ≠ y<GOAL>μ t ≤ μ s
<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✝¹¹ : Group H<VAR>inst✝¹⁰ : MulAction G α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : MulAction H β<VAR>inst✝⁷ : MeasurableSpace β<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : MeasurableSMul G α<VAR>inst✝³ : SMulInvariantMeasure G α μ<VAR>inst✝² : Countable G<VAR>ν : Measure α<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hs : IsFundamentalDomain G s μ<VAR>htm : NullMeasurableSet t μ<VAR>ht : ∀ x ∈ t, ∀ y ∈ t, ∀ (g : G), g ≠ 1 → g • x ≠ y<VAR>g₁ g₂ : G<VAR>hne : g₁ ≠ g₂<GOAL>(Disjoint on fun g => g • t ∩ s) g₁ g₂
<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✝¹¹ : Group H<VAR>inst✝¹⁰ : MulAction G α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : MulAction H β<VAR>inst✝⁷ : MeasurableSpace β<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : MeasurableSMul G α<VAR>inst✝³ : SMulInvariantMeasure G α μ<VAR>inst✝² : Countable G<VAR>ν : Measure α<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hs : IsFundamentalDomain G s μ<VAR>htm : NullMeasurableSet t μ<VAR>ht : ∀ x ∈ t, ∀ y ∈ t, ∀ (g : G), g ≠ 1 → g • x ≠ y<VAR>g₁ g₂ : G<VAR>hne : g₁ ≠ g₂<GOAL>Disjoint (g₁ • t ∩ s) (g₂ • t ∩ s)
<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✝¹¹ : Group H<VAR>inst✝¹⁰ : MulAction G α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : MulAction H β<VAR>inst✝⁷ : MeasurableSpace β<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : MeasurableSMul G α<VAR>inst✝³ : SMulInvariantMeasure G α μ<VAR>inst✝² : Countable G<VAR>ν : Measure α<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hs : IsFundamentalDomain G s μ<VAR>htm : NullMeasurableSet t μ<VAR>ht : ∀ x ∈ t, ∀ y ∈ t, ∀ (g : G), g ≠ 1 → g • x ≠ y<VAR>g₁ g₂ : G<VAR>hne : g₁ ≠ g₂<GOAL>Disjoint (g₁ • t) (g₂ • t)
<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✝¹¹ : Group H<VAR>inst✝¹⁰ : MulAction G α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : MulAction H β<VAR>inst✝⁷ : MeasurableSpace β<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : MeasurableSMul G α<VAR>inst✝³ : SMulInvariantMeasure G α μ<VAR>inst✝² : Countable G<VAR>ν : Measure α<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hs : IsFundamentalDomain G s μ<VAR>htm : NullMeasurableSet t μ<VAR>ht : ∀ x ∈ t, ∀ y ∈ t, ∀ (g : G), g ≠ 1 → g • x ≠ y<VAR>g₁ g₂ : G<VAR>hne : g₁ ≠ g₂<GOAL>∀ ⦃a : α⦄, a ∈ g₁ • t → a ∉ g₂ • t
<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✝¹¹ : Group H<VAR>inst✝¹⁰ : MulAction G α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : MulAction H β<VAR>inst✝⁷ : MeasurableSpace β<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : MeasurableSMul G α<VAR>inst✝³ : SMulInvariantMeasure G α μ<VAR>inst✝² : Countable G<VAR>ν : Measure α<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hs : IsFundamentalDomain G s μ<VAR>htm : NullMeasurableSet t μ<VAR>ht : ∀ x ∈ t, ∀ y ∈ t, ∀ (g : G), g ≠ 1 → g • x ≠ y<VAR>g₁ g₂ : G<VAR>hne : g₁ ≠ g₂<VAR>x : α<VAR>hx : x ∈ t<VAR>y : α<VAR>hy : y ∈ t<VAR>hxy : g₂ • y = g₁ • x<GOAL>False
<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✝¹¹ : Group H<VAR>inst✝¹⁰ : MulAction G α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : MulAction H β<VAR>inst✝⁷ : MeasurableSpace β<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : MeasurableSMul G α<VAR>inst✝³ : SMulInvariantMeasure G α μ<VAR>inst✝² : Countable G<VAR>ν : Measure α<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hs : IsFundamentalDomain G s μ<VAR>htm : NullMeasurableSet t μ<VAR>ht : ∀ x ∈ t, ∀ y ∈ t, ∀ (g : G), g ≠ 1 → g • x ≠ y<VAR>g₁ g₂ : G<VAR>hne : g₁ ≠ g₂<VAR>x : α<VAR>hx : x ∈ t<VAR>y : α<VAR>hy : y ∈ t<VAR>hxy : g₂ • y = g₁ • x<GOAL>(g₂⁻¹ * g₁) • x = y
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I J : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>h : I ≤ J<VAR>hJ : ¬J = 0<GOAL>count K v J ≤ count K v I
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I J : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>h : I ≤ J<VAR>hJ : ¬J = 0<VAR>this : J⁻¹ * I ≤ J⁻¹ * J<GOAL>count K v J ≤ count K v I
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I J : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>h : I ≤ J<VAR>hJ : ¬J = 0<VAR>this : ∃ I_1, ↑I_1 = J⁻¹ * I<GOAL>count K v J ≤ count K v I
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I J : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>h : I ≤ J<VAR>hJ : ¬J = 0<VAR>J' : Ideal R<VAR>hJ' : ↑J' = J⁻¹ * I<GOAL>count K v J ≤ count K v I
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I J : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>h : I ≤ J<VAR>hJ : ¬J = 0<VAR>J' : Ideal R<VAR>hJ' : ↑J' = J⁻¹ * I<GOAL>0 ≤ count K v ↑J'
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I J : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>h : I ≤ J<VAR>hJ : ¬J = 0<VAR>J' : Ideal R<VAR>hJ' : ↑J' = J⁻¹ * I<GOAL>↑J' ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : Countable α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSingletonClass α<VAR>p : PMF α<VAR>μ✝ : Measure α<VAR>inst✝¹ : IsProbabilityMeasure μ✝<VAR>μ : Measure α<VAR>inst✝ : IsProbabilityMeasure μ<GOAL>μ.toPMF = p ↔ μ = p.toMeasure
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>p : PMF α<VAR>b : β<VAR>s : Set β<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>hf : Measurable f<VAR>hs : MeasurableSet s<GOAL>(map f p).toMeasure s = p.toMeasure (f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>p : PMF α<VAR>b : β<VAR>s : Set β<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>hf : Measurable f<VAR>hs : MeasurableSet s<GOAL>(map f p).toOuterMeasure s = p.toOuterMeasure (f ⁻¹' s)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : OrderBot α<VAR>s s₁ : Finset β<VAR>f✝ g✝ : β → α<VAR>a : α<VAR>f g : β → α<VAR>hfg : ∀ a ∈ s₁, f a = g a<GOAL>s₁.sup f = s₁.sup g
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<GOAL>(coeff R 1) X = 1
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : 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 M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>f : M →ₗ⁅R,L⁆ M₂<GOAL>map f ⁅I, N⁆ = ⁅I, map f N⁆
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : 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 M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>f : M →ₗ⁅R,L⁆ M₂<GOAL>Submodule.span R (⇑↑f '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}) = Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
<VAR>E : Type u_1<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>inst✝⁹ : FiniteDimensional ℝ E<VAR>inst✝⁸ : MeasurableSpace E<VAR>inst✝⁷ : BorelSpace E<VAR>L✝ : AddSubgroup E<VAR>inst✝⁶ : DiscreteTopology ↥L✝<VAR>inst✝⁵ : IsZlattice ℝ L✝<VAR>μ : autoParam (Measure E) _auto✝<VAR>inst✝⁴ : Measure.IsAddHaarMeasure μ<VAR>ι : Type u_2<VAR>inst✝³ : Fintype ι<VAR>inst✝² : DecidableEq ι<VAR>L : AddSubgroup (ι → ℝ)<VAR>inst✝¹ : DiscreteTopology ↥L<VAR>inst✝ : IsZlattice ℝ L<VAR>b : Basis ι ℤ ↥L<GOAL>covolume L volume = |(Matrix.of (Subtype.val ∘ ⇑b)).det|
<VAR>E : Type u_1<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>inst✝⁹ : FiniteDimensional ℝ E<VAR>inst✝⁸ : MeasurableSpace E<VAR>inst✝⁷ : BorelSpace E<VAR>L✝ : AddSubgroup E<VAR>inst✝⁶ : DiscreteTopology ↥L✝<VAR>inst✝⁵ : IsZlattice ℝ L✝<VAR>μ : autoParam (Measure E) _auto✝<VAR>inst✝⁴ : Measure.IsAddHaarMeasure μ<VAR>ι : Type u_2<VAR>inst✝³ : Fintype ι<VAR>inst✝² : DecidableEq ι<VAR>L : AddSubgroup (ι → ℝ)<VAR>inst✝¹ : DiscreteTopology ↥L<VAR>inst✝ : IsZlattice ℝ L<VAR>b : Basis ι ℤ ↥L<GOAL>|(Matrix.of ⇑(Basis.ofZlatticeBasis ℝ L b)).det| = |(Matrix.of (Subtype.val ∘ ⇑b)).det|
<VAR>E : Type u_1<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>inst✝⁹ : FiniteDimensional ℝ E<VAR>inst✝⁸ : MeasurableSpace E<VAR>inst✝⁷ : BorelSpace E<VAR>L✝ : AddSubgroup E<VAR>inst✝⁶ : DiscreteTopology ↥L✝<VAR>inst✝⁵ : IsZlattice ℝ L✝<VAR>μ : autoParam (Measure E) _auto✝<VAR>inst✝⁴ : Measure.IsAddHaarMeasure μ<VAR>ι : Type u_2<VAR>inst✝³ : Fintype ι<VAR>inst✝² : DecidableEq ι<VAR>L : AddSubgroup (ι → ℝ)<VAR>inst✝¹ : DiscreteTopology ↥L<VAR>inst✝ : IsZlattice ℝ L<VAR>b : Basis ι ℤ ↥L<VAR>x✝ : ι<GOAL>(Basis.ofZlatticeBasis ℝ L b) x✝ = (Subtype.val ∘ ⇑b) x✝
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : DivisionRing R<VAR>p q : R[X]<VAR>hp0 : p ≠ 0<VAR>hp : ¬IsUnit p<VAR>h : 0 ≥ p.degree<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : DivisionRing R<VAR>p q : R[X]<VAR>hp0 : C (p.coeff 0) ≠ 0<VAR>hp : ¬IsUnit (C (p.coeff 0))<VAR>h : 0 ≥ p.degree<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s✝ : β → β → Prop<VAR>t : γ → γ → Prop<VAR>s : Set Ordinal.{u}<VAR>hs : Small.{u, u + 1} ↑s<VAR>a : Ordinal.{u}<VAR>ha : a ∈ s<GOAL>a ≤ sup fun x => ↑((equivShrink ↑s).symm x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s✝ : β → β → Prop<VAR>t : γ → γ → Prop<VAR>s : Set Ordinal.{u}<VAR>hs : Small.{u, u + 1} ↑s<VAR>a : Ordinal.{u}<VAR>ha : a ∈ s<GOAL>a = ↑((equivShrink ↑s).symm ((equivShrink ↑s) ⟨a, ha⟩))
<VAR>R : Type u1<VAR>inst✝⁸ : CommRing R<VAR>M : Type u2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>A : Type u_1<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Algebra R A<VAR>N : Type u4<VAR>N' : Type u5<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommGroup N'<VAR>inst✝ : Module R N'<VAR>n : ℕ<VAR>f : M →ₗ[R] N<VAR>m : Fin n → M<GOAL>(map f) ((ιMulti R n) m) = (ιMulti R n) (⇑f ∘ m)
<VAR>R : Type u1<VAR>inst✝⁸ : CommRing R<VAR>M : Type u2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>A : Type u_1<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Algebra R A<VAR>N : Type u4<VAR>N' : Type u5<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommGroup N'<VAR>inst✝ : Module R N'<VAR>n : ℕ<VAR>f : M →ₗ[R] N<VAR>m : Fin n → M<GOAL>(List.map (⇑(map f)) (List.ofFn fun i => (ι R) (m i))).prod = (List.ofFn fun i => (ι R) ((⇑f ∘ m) i)).prod
<VAR>α✝ β✝ γ✝ : Type u<VAR>m✝ : ?m.14964<VAR>m : Type u → Type v<VAR>h : Applicative m<VAR>inst✝ : CommApplicative m<VAR>α β γ : Type u<VAR>a : m α<VAR>b : m β<VAR>f : α → β → γ<GOAL>(Seq.seq (f <$> a) fun x => b) = (fun p => f p.fst p.snd) <$> Seq.seq (Prod.mk <$> a) fun x => b
<VAR>α✝ β✝ γ✝ : Type u<VAR>m✝ : ?m.14964<VAR>m : Type u → Type v<VAR>h : Applicative m<VAR>inst✝ : CommApplicative m<VAR>α β γ : Type u<VAR>a : m α<VAR>b : m β<VAR>f : α → β → γ<GOAL>((fun p => f p.fst p.snd) <$> Seq.seq (Prod.mk <$> a) fun x => b) = Seq.seq ((fun b a => f a b) <$> b) fun x => a
<VAR>α✝ β✝ γ✝ : Type u<VAR>m✝ : ?m.14964<VAR>m : Type u → Type v<VAR>h : Applicative m<VAR>inst✝ : CommApplicative m<VAR>α β γ : Type u<VAR>a : m α<VAR>b : m β<VAR>f : α → β → γ<GOAL>((fun p => f p.fst p.snd) <$> Seq.seq ((fun b a => (a, b)) <$> b) fun x => a) = Seq.seq ((fun b a => f a b) <$> b) fun x => a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>f : α →₀ ℕ<VAR>i : α<GOAL>i ∈ toMultiset f ↔ i ∈ f.support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort u_6<VAR>s t u : Set α<VAR>m : MeasurableSpace α<VAR>s₁ s₂ : Set α<VAR>h₁ : MeasurableSet s₁<VAR>h₂ : MeasurableSet s₂<GOAL>MeasurableSet (s₁ ⇨ s₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort u_6<VAR>s t u : Set α<VAR>m : MeasurableSpace α<VAR>s₁ s₂ : Set α<VAR>h₁ : MeasurableSet s₁<VAR>h₂ : MeasurableSet s₂<GOAL>MeasurableSet (s₂ ⊔ s₁ᶜ)
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>x y : M × ↥S<GOAL>(r S) x y ↔ ∃ c, ↑c * (↑y.2 * x.1) = ↑c * (↑x.2 * y.1)
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>x y : M × ↥S<GOAL>(r' S) x y ↔ ∃ c, ↑c * (↑y.2 * x.1) = ↑c * (↑x.2 * y.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>ζ : M<VAR>f : F<VAR>h✝ : IsPrimitiveRoot ζ k<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : MonoidHomClass F M N<VAR>h : IsPrimitiveRoot ζ k<VAR>hf : Injective ⇑f<GOAL>f ζ ^ k = 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>ζ : M<VAR>f : F<VAR>h✝ : IsPrimitiveRoot ζ k<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : MonoidHomClass F M N<VAR>h : IsPrimitiveRoot ζ k<VAR>hf : Injective ⇑f<GOAL>∀ (l : ℕ), f ζ ^ l = 1 → k ∣ l
<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>ζ : M<VAR>f : F<VAR>h✝ : IsPrimitiveRoot ζ k<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : MonoidHomClass F M N<VAR>h : IsPrimitiveRoot ζ k<VAR>hf : Injective ⇑f<GOAL>∀ (l : ℕ), f ζ ^ l = 1 → orderOf ζ ∣ l
<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>ζ : M<VAR>f : F<VAR>h✝ : IsPrimitiveRoot ζ k<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : MonoidHomClass F M N<VAR>h : IsPrimitiveRoot ζ k<VAR>hf : Injective ⇑f<VAR>l : ℕ<VAR>hl : f ζ ^ l = 1<GOAL>orderOf ζ ∣ l
<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>ζ : M<VAR>f : F<VAR>h✝ : IsPrimitiveRoot ζ k<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : MonoidHomClass F M N<VAR>h : IsPrimitiveRoot ζ k<VAR>hf : Injective ⇑f<VAR>l : ℕ<VAR>hl : f (ζ ^ l) = f 1<GOAL>orderOf ζ ∣ l
<VAR>E : Type uE<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<GOAL>dist (↑(extChartAt I c) c) (↑(extChartAt I c) c) < f.rIn
<VAR>E : Type uE<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<GOAL>0 < f.rIn
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁶ : SeminormedAddCommGroup E<VAR>inst✝¹⁵ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁴ : SeminormedAddCommGroup F<VAR>inst✝¹³ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹² : SeminormedAddCommGroup G<VAR>inst✝¹¹ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁵ : NormedSpace 𝕜₂ F<VAR>inst✝⁴ : NormedSpace 𝕜 Fₗ<VAR>inst✝³ : NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝¹ : FunLike 𝓕 E F<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<GOAL>IsLeast {c | 0 ≤ c ∧ ∀ (x : E), ‖f x‖ ≤ c * ‖x‖} ‖f‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁶ : SeminormedAddCommGroup E<VAR>inst✝¹⁵ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁴ : SeminormedAddCommGroup F<VAR>inst✝¹³ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹² : SeminormedAddCommGroup G<VAR>inst✝¹¹ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁵ : NormedSpace 𝕜₂ F<VAR>inst✝⁴ : NormedSpace 𝕜 Fₗ<VAR>inst✝³ : NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝¹ : FunLike 𝓕 E F<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<GOAL>IsClosed {c | 0 ≤ c ∧ ∀ (x : E), ‖f x‖ ≤ c * ‖x‖}
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁶ : SeminormedAddCommGroup E<VAR>inst✝¹⁵ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁴ : SeminormedAddCommGroup F<VAR>inst✝¹³ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹² : SeminormedAddCommGroup G<VAR>inst✝¹¹ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁵ : NormedSpace 𝕜₂ F<VAR>inst✝⁴ : NormedSpace 𝕜 Fₗ<VAR>inst✝³ : NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝¹ : FunLike 𝓕 E F<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<GOAL>IsClosed ({a | 0 ≤ a} ∩ ⋂ i, {x | ‖f i‖ ≤ x * ‖i‖})
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a b c d : α<GOAL>(fun x => x - a) ⁻¹' [[b, c]] = [[b + a, c + a]]
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>a : α<VAR>l l₁' l₂' : List α<VAR>h : (a :: l).split = (l₁', l₂')<VAR>l₁ l₂ : List α<VAR>e : l.split = (l₁, l₂)<GOAL>l₁'.length ≤ (a :: l).length ∧ l₂'.length ≤ (a :: l).length
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>a : α<VAR>l l₁' l₂' : List α<VAR>h : (a :: l).split = (l₁', l₂')<VAR>l₁ l₂ : List α<VAR>e : l.split = (l₁, l₂)<VAR>fst_eq✝ : a :: l₂ = l₁'<VAR>snd_eq✝ : l₁ = l₂'<GOAL>l₁'.length ≤ (a :: l).length ∧ l₂'.length ≤ (a :: l).length
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>a : α<VAR>l l₁ l₂ : List α<VAR>e : l.split = (l₁, l₂)<VAR>h : (a :: l).split = (a :: l₂, l₁)<VAR>h₁ : l₁.length ≤ l.length<VAR>h₂ : l₂.length ≤ l.length<GOAL>(a :: l₂).length ≤ (a :: l).length ∧ l₁.length ≤ (a :: l).length
<VAR>G : Type u_1<VAR>inst✝ : DivisionMonoid G<VAR>a x y : G<GOAL>SemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Preorder β<VAR>s t : Finset α<VAR>f : Finset α → β<GOAL>Monotone f ↔ ∀ (s : Finset α) ⦃a : α⦄ (ha : a ∉ s), f s ≤ f (cons a s ha)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝³ : AddCommMonoid α<VAR>inst✝² : Neg β<VAR>inst✝¹ : DivisionSemiring γ<VAR>inst✝ : Module γ α<VAR>h : Antiperiodic f c<VAR>a : γ<VAR>ha : a ≠ 0<GOAL>Antiperiodic (fun x => f (a⁻¹ • x)) (a • c)