ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>s : Set Ω<GOAL>IndepSet s ∅ κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>s : Set Ω<GOAL>Indep (generateFrom {s}) ⊥ κ μ
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z x : K<GOAL>‖x + (starRingEnd K) x‖ ^ 2 = re (x + (starRingEnd K) x) ^ 2
<VAR>α : Type u_1<VAR>s✝¹ t✝ : Finset α<VAR>n : ?m.28461<VAR>s✝ t s a✝ : Finset α<GOAL>a✝ ∈ powersetCard s.card s ↔ a✝ ∈ {s}
<VAR>α : Type u_1<VAR>s✝¹ t✝ : Finset α<VAR>n : ?m.28461<VAR>s✝ t s a✝ : Finset α<GOAL>a✝ ⊆ s ∧ a✝.card = s.card ↔ a✝ = s
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>u : (𝓞 K)ˣ<GOAL>u ∈ [1, -1, η, -η, η ^ 2, -η ^ 2]
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>u : (𝓞 K)ˣ<VAR>hrank : rank K = 0<GOAL>u ∈ [1, -1, η, -η, η ^ 2, -η ^ 2]
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>u : (𝓞 K)ˣ<VAR>hrank : rank K = 0<VAR>x : ↥(torsion K)<VAR>e : Fin (rank K) → ℤ<VAR>hxu : u = ↑(x, e).1 * ∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i<GOAL>u ∈ [1, -1, η, -η, η ^ 2, -η ^ 2]
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>u : (𝓞 K)ˣ<VAR>hrank : rank K = 0<VAR>x : ↥(torsion K)<VAR>e : Fin (rank K) → ℤ<VAR>hxu : u = ↑x<GOAL>u ∈ [1, -1, η, -η, η ^ 2, -η ^ 2]
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>u : (𝓞 K)ˣ<VAR>hrank : rank K = 0<VAR>x : ↥(torsion K)<VAR>e : Fin (rank K) → ℤ<VAR>hxu : u = ↑x<VAR>n : ℕ<VAR>hnpos : 0 < n<VAR>hn : ↑x ^ n = 1<GOAL>u ∈ [1, -1, η, -η, η ^ 2, -η ^ 2]
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>u : (𝓞 K)ˣ<VAR>hrank : rank K = 0<VAR>x : ↥(torsion K)<VAR>e : Fin (rank K) → ℤ<VAR>hxu : u = ↑x<VAR>n : ℕ<VAR>hnpos : 0 < n<VAR>hn : (algebraMap (𝓞 K) K) ↑u ^ ↑⟨n, hnpos⟩ = 1<GOAL>u ∈ [1, -1, η, -η, η ^ 2, -η ^ 2]
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>u : (𝓞 K)ˣ<VAR>hrank : rank K = 0<VAR>x : ↥(torsion K)<VAR>e : Fin (rank K) → ℤ<VAR>hxu : u = ↑x<VAR>n : ℕ<VAR>hnpos : 0 < n<VAR>hn : (algebraMap (𝓞 K) K) ↑u ^ ↑⟨n, hnpos⟩ = 1<VAR>r : ℕ<VAR>hr3 : r < ↑3<VAR>hru : (algebraMap (𝓞 K) K) ↑u = ζ ^ r ∨ (algebraMap (𝓞 K) K) ↑u = -ζ ^ r<GOAL>u ∈ [1, -1, η, -η, η ^ 2, -η ^ 2]
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>u : (𝓞 K)ˣ<VAR>hrank : rank K = 0<VAR>x : ↥(torsion K)<VAR>e : Fin (rank K) → ℤ<VAR>hxu : u = ↑x<VAR>n : ℕ<VAR>hnpos : 0 < n<VAR>hn : (algebraMap (𝓞 K) K) ↑u ^ ↑⟨n, hnpos⟩ = 1<VAR>r : ℕ<VAR>hr3 : r < ↑3<VAR>hru : (algebraMap (𝓞 K) K) ↑u = ζ ^ r ∨ (algebraMap (𝓞 K) K) ↑u = -ζ ^ r<VAR>hr : r ∈ Finset.Ico 0 3<GOAL>u ∈ [1, -1, η, -η, η ^ 2, -η ^ 2]
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>K : 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_9<VAR>V₂ : Type u_10<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring R₂<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R₂ M₂<VAR>p✝ p'✝ : Submodule R M<VAR>q : Submodule R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_11<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>p p' : Submodule R M<GOAL>map p.subtype ⊤ ≤ p' ↔ p ≤ p'
<VAR>v : Vector ℕ 0<GOAL>0 = encode v
<VAR>v : Vector ℕ 0<GOAL>0 = encode nil
<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✝¹ : CompleteLattice α<VAR>f✝ g s✝ t : ι → α<VAR>a b : α<VAR>inst✝ : CompleteLattice β<VAR>s : Set α<VAR>f : α → β<VAR>hf : Antitone f<GOAL>f (sSup s) ≤ ⨅ a ∈ s, f a
<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✝¹ : CompleteLattice α<VAR>f✝ g s✝ t : ι → α<VAR>a b : α<VAR>inst✝ : CompleteLattice β<VAR>s : Set α<VAR>f : α → β<VAR>hf : Antitone f<GOAL>f (⨆ a ∈ s, a) ≤ ⨅ a ∈ s, f a
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizationMonoid α<GOAL>normalize 0 = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a✝ b : R<VAR>x y : M<VAR>hv✝ hv : LinearIndependent R v<VAR>i : ι<VAR>a : R<VAR>ha : a • v i ∈ span R (v '' (univ \ {i}))<GOAL>a = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a✝ b : R<VAR>x y : M<VAR>hv✝ hv : LinearIndependent R v<VAR>i : ι<VAR>a : R<VAR>ha : ∃ y ∈ Finsupp.supported R R (univ \ {i}), (Finsupp.total ι M R v) y = a • v i<GOAL>a = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a✝ b : R<VAR>x y : M<VAR>hv✝ hv : LinearIndependent R v<VAR>i : ι<VAR>a : R<VAR>l : ι →₀ R<VAR>hl : l ∈ Finsupp.supported R R (univ \ {i})<VAR>e : (Finsupp.total ι M R v) l = a • v i<GOAL>a = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a✝ b : R<VAR>x y : M<VAR>hv✝ hv : LinearIndependent R v<VAR>i : ι<VAR>a : R<VAR>l : ι →₀ R<VAR>hl : Finsupp.single i a ∈ Finsupp.supported R R (univ \ {i})<VAR>e : (Finsupp.total ι M R v) l = a • v i<GOAL>a = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a✝ b : R<VAR>x y : M<VAR>hv✝ hv : LinearIndependent R v<VAR>i : ι<VAR>a : R<VAR>l : ι →₀ R<VAR>hl : Finsupp.single i a ∈ Finsupp.supported R R (univ \ {i})<VAR>e : (Finsupp.total ι M R v) l = a • v i<VAR>hn : ¬a = 0<GOAL>False
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>hv : LinearIndependent R v<VAR>H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0<VAR>l : ι →₀ R<VAR>hl : (Finsupp.total ι M R v) l = 0<VAR>i : ι<GOAL>l i = 0 i
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>hv : LinearIndependent R v<VAR>H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0<VAR>l : ι →₀ R<VAR>hl : (Finsupp.total ι M R v) l = 0<VAR>i : ι<GOAL>l i = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>hv : LinearIndependent R v<VAR>H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0<VAR>l : ι →₀ R<VAR>hl : (Finsupp.total ι M R v) l = 0<VAR>i : ι<VAR>hn : ¬l i = 0<GOAL>False
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>hv : LinearIndependent R v<VAR>H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0<VAR>l : ι →₀ R<VAR>hl : (Finsupp.total ι M R v) l = 0<VAR>i : ι<VAR>hn : ¬l i = 0<GOAL>l i • v i ∈ span R (v '' (univ \ {i}))
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>hv : LinearIndependent R v<VAR>H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0<VAR>l : ι →₀ R<VAR>hl : (Finsupp.total ι M R v) l = 0<VAR>i : ι<VAR>hn : ¬l i = 0<GOAL>Finsupp.single i (l i) - l ∈ Finsupp.supported R R (univ \ {i})
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>hv : LinearIndependent R v<VAR>H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0<VAR>l : ι →₀ R<VAR>hl : (Finsupp.total ι M R v) l = 0<VAR>i : ι<VAR>hn : ¬l i = 0<GOAL>(Finsupp.total ι M R v) (Finsupp.single i (l i) - l) = l i • v i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : Ring S<VAR>M : Type u_4<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>m : Submodule R M<VAR>N : Type u_5<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : IsSemisimpleModule R M<VAR>inst✝ : Nontrivial M<GOAL>∃ m, IsSimpleModule R ↥m
<VAR>G : Type u<VAR>inst✝ : Group G<VAR>B✝ B : GroupFilterBasis G<VAR>x₀ : G<GOAL>(𝓝 x₀).HasBasis (fun V => V ∈ B) fun V => (fun y => x₀ * y) '' V
<VAR>G : Type u<VAR>inst✝ : Group G<VAR>B✝ B : GroupFilterBasis G<VAR>x₀ : G<GOAL>(B.N x₀).HasBasis (fun V => V ∈ B) fun V => (fun y => x₀ * y) '' V
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>K : Type u_5<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>x : K<VAR>hx : x ≠ 0<GOAL>(algebraMap A K) (num A x⁻¹ * num A x) / (algebraMap A K) (↑(den A x⁻¹) * ↑(den A x)) = 1
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>K : Type u_5<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>x : K<VAR>hx : x ≠ 0<GOAL>(algebraMap A K) (num A x * num A x⁻¹) / (algebraMap A K) (↑(den A x) * ↑(den A x⁻¹)) = 1
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>s t : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>h : _root_.Disjoint s t<GOAL>(s ∪ t).dens = s.dens + t.dens
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>v : E<VAR>hv : v ∈ (⨆ μ, eigenspace T μ)ᗮ<GOAL>T v ∈ (⨆ μ, eigenspace T μ)ᗮ
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>v : E<VAR>hv : v ∈ ⨅ i, (eigenspace T i)ᗮ<GOAL>T v ∈ ⨅ i, (eigenspace T i)ᗮ
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>s : Set (ι → ℝ)<GOAL>∏ _i : ι, ↑1 * EMetric.diam s = EMetric.diam s ^ Fintype.card ι
<VAR>R : Type uR<VAR>inst✝⁴ : Semiring R<VAR>S : Type uS<VAR>inst✝³ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra S A<VAR>r✝ : R → R → Prop<VAR>inst✝ : Semiring T<VAR>f : R →+* T<VAR>r : R → R → Prop<VAR>w : ∀ ⦃x y : R⦄, r x y → f x = f y<VAR>x : R<GOAL>(lift ⟨f, w⟩) ((mkRingHom r) x) = f x
<VAR>R : Type uR<VAR>inst✝⁴ : Semiring R<VAR>S : Type uS<VAR>inst✝³ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra S A<VAR>r✝ : R → R → Prop<VAR>inst✝ : Semiring T<VAR>f : R →+* T<VAR>r : R → R → Prop<VAR>w : ∀ ⦃x y : R⦄, r x y → f x = f y<VAR>x : R<GOAL>({ toFun := fun f => { toFun := fun x => Quot.lift ⇑↑f ⋯ x.toQuot, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }, invFun := fun F => ⟨F.comp { toFun := fun x => { toQuot := Quot.mk (Rel r) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } ⟨f, w⟩) ({ toFun := fun x => { toQuot := Quot.mk (Rel r) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } x) = f x
<VAR>s n : Nat<GOAL>range.loop (s + 1) (range' (s + 1) n) = range' 0 (n + (s + 1))
<VAR>s n : Nat<GOAL>range.loop (s + 1) (range' (s + 1) n) = range' 0 (n + 1 + s)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : ℤ → R<VAR>f : R →+* S<VAR>b c d : R<VAR>n : ℕ<GOAL>f (preNormEDS' b c d n) = preNormEDS' (f b) (f c) (f d) n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>E : Type u_3<VAR>inst✝¹ : Norm E<VAR>F : Type u_4<VAR>inst✝ : Norm F<VAR>e : PartialHomeomorph α β<VAR>b : β<VAR>hb : b ∈ e.target<VAR>f : β → E<VAR>g : β → F<VAR>C : ℝ<VAR>h : IsBigOWith C (𝓝 b) f g<GOAL>Tendsto (↑e) (𝓝 (↑e.symm b)) (𝓝 b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>E : Type u_3<VAR>inst✝¹ : Norm E<VAR>F : Type u_4<VAR>inst✝ : Norm F<VAR>e : PartialHomeomorph α β<VAR>b : β<VAR>hb : b ∈ e.target<VAR>f : β → E<VAR>g : β → F<VAR>C : ℝ<VAR>h : IsBigOWith C (𝓝 b) f g<VAR>this : ContinuousAt (↑e) (↑e.symm b)<GOAL>Tendsto (↑e) (𝓝 (↑e.symm b)) (𝓝 b)
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<VAR>hf : Function.Injective f<GOAL>(ofFn f).Nodup
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<VAR>hf : Function.Injective f<GOAL>(pmap (fun i hi => f ⟨i, hi⟩) (range n) ⋯).Nodup
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NormedAddCommGroup β<VAR>u v w : α → β<VAR>l : Filter α<VAR>h : u ~[l] v<GOAL>v =O[l] u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NormedAddCommGroup β<VAR>u v w : α → β<VAR>l : Filter α<VAR>h : u ~[l] v<VAR>x✝ : α<GOAL>u x✝ = (u - v) x✝ + v x✝
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>ψ : (p : ℤ) → F.X p ⟶ G.X p<VAR>p' p q : ℤ<VAR>hpq : p + 0 = q<GOAL>F.d p' p ≫ (ofHoms ψ).v p q hpq = F.d p' q ≫ ψ q
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>ψ : (p : ℤ) → F.X p ⟶ G.X p<VAR>p' p q : ℤ<VAR>hpq✝ : p + 0 = q<VAR>hpq : p = q<GOAL>F.d p' p ≫ (ofHoms ψ).v p q hpq✝ = F.d p' q ≫ ψ q
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>ψ : (p : ℤ) → F.X p ⟶ G.X p<VAR>p' p : ℤ<VAR>hpq : p + 0 = p<GOAL>F.d p' p ≫ (ofHoms ψ).v p p hpq = F.d p' p ≫ ψ p
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>n : ℕ<GOAL>rtakeWhile p l <:+ l
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>n : ℕ<GOAL>takeWhile p l.reverse <+: l.reverse
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>hv : v ≠ 0<GOAL>ℙ ≪ gaussianReal μ v
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>hv : v ≠ 0<GOAL>ℙ ≪ ℙ.withDensity (gaussianPDF μ v)
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>hv : v ≠ 0<GOAL>AEMeasurable (gaussianPDF μ v) ℙ
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>hv : v ≠ 0<GOAL>∀ᵐ (x : ℝ), gaussianPDF μ v x ≠ 0
<VAR>α : Type u_1<VAR>inst✝ : MetricSpace α<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig α N τ<VAR>i : Fin N.succ<GOAL>dist (a.c i) (a.c (last N)) ≤ a.r i + a.r (last N)
<VAR>α : Type u_1<VAR>inst✝ : MetricSpace α<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig α N τ<VAR>i : Fin N.succ<VAR>H : i < last N<GOAL>dist (a.c i) (a.c (last N)) ≤ a.r i + a.r (last N)
<VAR>α : Type u_1<VAR>inst✝ : MetricSpace α<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig α N τ<VAR>i : Fin N.succ<VAR>H : last N ≤ i<GOAL>dist (a.c i) (a.c (last N)) ≤ a.r i + a.r (last N)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>a : SatelliteConfig E (multiplicity E) (goodτ E)<VAR>b : SatelliteConfig E (multiplicity E) (goodτ E) := a.centerAndRescale<GOAL>False
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>a : SatelliteConfig E (multiplicity E) (goodτ E)<VAR>b : SatelliteConfig E (multiplicity E) (goodτ E) := a.centerAndRescale<VAR>c' : Fin (multiplicity E).succ → E<VAR>c'_le_two : ∀ (n : Fin (multiplicity E).succ), ‖c' n‖ ≤ 2<VAR>hc' : Pairwise fun i j => 1 - goodδ E ≤ ‖c' i - c' j‖<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : LocallyFiniteOrderTop α<VAR>a : Subtype p<VAR>hp : ∀ ⦃a x : α⦄, a ≤ x → p a → p x<GOAL>map (Embedding.subtype p) (Ioi a) = Ioi ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : LocallyFiniteOrderTop α<VAR>a : Subtype p<VAR>hp : ∀ ⦃a x : α⦄, a ≤ x → p a → p x<GOAL>map (Embedding.subtype p) (Finset.subtype p (Ioi ↑a)) = Ioi ↑a
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddCommMonoid A<VAR>inst✝ : HasShift C A<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>i j : A<GOAL>(shiftComm X i j).hom ≫ (shiftFunctor C i).map ((shiftFunctor C j).map f) = (shiftFunctor C j).map ((shiftFunctor C i).map f) ≫ (shiftComm Y i j).hom
<VAR>a : ℝ<GOAL>frontier {z | z.im < a} = {z | z.im = a}
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.337009, u_1} C<VAR>n m : ℕ<VAR>F G : ComposableArrows C n<VAR>f g : ComposableArrows C 4<VAR>app₀ : f.obj' 0 ⋯ ≅ g.obj' 0 ⋯<VAR>app₁ : f.obj' 1 ⋯ ≅ g.obj' 1 ⋯<VAR>app₂ : f.obj' 2 ⋯ ≅ g.obj' 2 ⋯<VAR>app₃ : f.obj' 3 ⋯ ≅ g.obj' 3 ⋯<VAR>app₄ : f.obj' 4 ⋯ ≅ g.obj' 4 ⋯<VAR>w₀ : f.map' 0 1 ⋯ ⋯ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 ⋯ ⋯<VAR>w₁ : f.map' 1 2 ⋯ ⋯ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 ⋯ ⋯<VAR>w₂ : f.map' 2 3 ⋯ ⋯ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 ⋯ ⋯<VAR>w₃ : f.map' 3 4 ⋯ ⋯ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 ⋯ ⋯<GOAL>g.map' 0 1 ⋯ ⋯ ≫ app₁.inv = app₀.inv ≫ f.map' 0 1 ⋯ ⋯
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.337009, u_1} C<VAR>n m : ℕ<VAR>F G : ComposableArrows C n<VAR>f g : ComposableArrows C 4<VAR>app₀ : f.obj' 0 ⋯ ≅ g.obj' 0 ⋯<VAR>app₁ : f.obj' 1 ⋯ ≅ g.obj' 1 ⋯<VAR>app₂ : f.obj' 2 ⋯ ≅ g.obj' 2 ⋯<VAR>app₃ : f.obj' 3 ⋯ ≅ g.obj' 3 ⋯<VAR>app₄ : f.obj' 4 ⋯ ≅ g.obj' 4 ⋯<VAR>w₀ : f.map' 0 1 ⋯ ⋯ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 ⋯ ⋯<VAR>w₁ : f.map' 1 2 ⋯ ⋯ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 ⋯ ⋯<VAR>w₂ : f.map' 2 3 ⋯ ⋯ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 ⋯ ⋯<VAR>w₃ : f.map' 3 4 ⋯ ⋯ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 ⋯ ⋯<GOAL>g.map' 1 2 ⋯ ⋯ ≫ app₂.inv = app₁.inv ≫ f.map' 1 2 ⋯ ⋯
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.337009, u_1} C<VAR>n m : ℕ<VAR>F G : ComposableArrows C n<VAR>f g : ComposableArrows C 4<VAR>app₀ : f.obj' 0 ⋯ ≅ g.obj' 0 ⋯<VAR>app₁ : f.obj' 1 ⋯ ≅ g.obj' 1 ⋯<VAR>app₂ : f.obj' 2 ⋯ ≅ g.obj' 2 ⋯<VAR>app₃ : f.obj' 3 ⋯ ≅ g.obj' 3 ⋯<VAR>app₄ : f.obj' 4 ⋯ ≅ g.obj' 4 ⋯<VAR>w₀ : f.map' 0 1 ⋯ ⋯ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 ⋯ ⋯<VAR>w₁ : f.map' 1 2 ⋯ ⋯ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 ⋯ ⋯<VAR>w₂ : f.map' 2 3 ⋯ ⋯ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 ⋯ ⋯<VAR>w₃ : f.map' 3 4 ⋯ ⋯ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 ⋯ ⋯<GOAL>g.map' 2 3 ⋯ ⋯ ≫ app₃.inv = app₂.inv ≫ f.map' 2 3 ⋯ ⋯
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.337009, u_1} C<VAR>n m : ℕ<VAR>F G : ComposableArrows C n<VAR>f g : ComposableArrows C 4<VAR>app₀ : f.obj' 0 ⋯ ≅ g.obj' 0 ⋯<VAR>app₁ : f.obj' 1 ⋯ ≅ g.obj' 1 ⋯<VAR>app₂ : f.obj' 2 ⋯ ≅ g.obj' 2 ⋯<VAR>app₃ : f.obj' 3 ⋯ ≅ g.obj' 3 ⋯<VAR>app₄ : f.obj' 4 ⋯ ≅ g.obj' 4 ⋯<VAR>w₀ : f.map' 0 1 ⋯ ⋯ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 ⋯ ⋯<VAR>w₁ : f.map' 1 2 ⋯ ⋯ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 ⋯ ⋯<VAR>w₂ : f.map' 2 3 ⋯ ⋯ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 ⋯ ⋯<VAR>w₃ : f.map' 3 4 ⋯ ⋯ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 ⋯ ⋯<GOAL>g.map' 3 4 ⋯ ⋯ ≫ app₄.inv = app₃.inv ≫ f.map' 3 4 ⋯ ⋯
<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✝¹ : DecidableEq α<VAR>inst✝ : CommMonoid α<VAR>S : Multiset α<GOAL>S.toFinset.prod id ∣ S.prod
<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✝¹ : DecidableEq α<VAR>inst✝ : CommMonoid α<VAR>S : Multiset α<GOAL>(map id S.toFinset.val).prod ∣ S.prod
<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✝¹ : DecidableEq α<VAR>inst✝ : CommMonoid α<VAR>S : Multiset α<GOAL>map id S.toFinset.val ≤ S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Mul α<VAR>inst✝² : LinearOrder α<VAR>a b c d : α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>h : a * b ≤ c * d<GOAL>min a b ≤ max c d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Mul α<VAR>inst✝² : LinearOrder α<VAR>a b c d : α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>h : a * b ≤ c * d<GOAL>(a ≤ c ∨ a ≤ d) ∨ b ≤ c ∨ b ≤ d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Mul α<VAR>inst✝² : LinearOrder α<VAR>a b c d : α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>h : (c < a ∧ d < a) ∧ c < b ∧ d < b<GOAL>c * d < a * b
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>q n : ℕ<VAR>x y : R<VAR>hprime : Nat.Prime q<VAR>hchar✝ : CharP R q<VAR>this : Fact (Nat.Prime q)<GOAL>(x - y) ^ q ^ n = x ^ q ^ n - y ^ q ^ n