ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n : ℕ<VAR>hn : Odd n<VAR>u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 ⋯<VAR>hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0<VAR>i j : ZMod n<VAR>h✝ : Commute (sr i, sr j).1 (sr i, sr j).2<VAR>h : i = j<GOAL>↑u⁻¹ * (2 * j) = j
<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>b' : Basis ι' R M'<VAR>e : ι ≃ ι'<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq M<VAR>i : ι<VAR>h : optParam (b i ∈ Finset.image (⇑b) Finset.univ) ⋯<GOAL>b.reindexFinsetRange ⟨b i, h⟩ = b i
<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>b' : Basis ι' R M'<VAR>e : ι ≃ ι'<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq M<VAR>i : ι<VAR>h : optParam (b i ∈ Finset.image (⇑b) Finset.univ) ⋯<GOAL>↑(((Equiv.refl M).subtypeEquiv ⋯).symm ⟨b i, h⟩) = b i
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring A<VAR>inst✝² : Algebra R A<VAR>L : Type v<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<VAR>K : LieSubalgebra R L<VAR>x : ↥K<VAR>n : ℕ<VAR>hn : (LieAlgebra.ad R L) ↑x ^ n = 0<GOAL>IsNilpotent ((LieAlgebra.ad R ↥K) x)
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring A<VAR>inst✝² : Algebra R A<VAR>L : Type v<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<VAR>K : LieSubalgebra R L<VAR>x : ↥K<VAR>n : ℕ<VAR>hn : (LieAlgebra.ad R L) ↑x ^ n = 0<GOAL>(LieAlgebra.ad R ↥K) x ^ n = 0
<VAR>A B A' B' : CommRingCat<VAR>f : A ⟶ B<VAR>f' : A' ⟶ B'<VAR>g : A ⟶ A'<VAR>g' : B ⟶ B'<VAR>fac : g ≫ f' = f ≫ g'<VAR>M : ModuleCat ↑B<VAR>α β : KaehlerDifferential f ⟶ M<VAR>h : ∀ (b : ↑B), α (d b) = β (d b)<GOAL>α = β
<VAR>A B A' B' : CommRingCat<VAR>f : A ⟶ B<VAR>f' : A' ⟶ B'<VAR>g : A ⟶ A'<VAR>g' : B ⟶ B'<VAR>fac : g ≫ f' = f ≫ g'<VAR>M : ModuleCat ↑B<VAR>α β : KaehlerDifferential f ⟶ M<VAR>h : ∀ (b : ↑B), α (d b) = β (d b)<GOAL>α - β = 0
<VAR>A B A' B' : CommRingCat<VAR>f : A ⟶ B<VAR>f' : A' ⟶ B'<VAR>g : A ⟶ A'<VAR>g' : B ⟶ B'<VAR>fac : g ≫ f' = f ≫ g'<VAR>M : ModuleCat ↑B<VAR>α β : KaehlerDifferential f ⟶ M<VAR>h : ∀ (b : ↑B), α (d b) = β (d b)<VAR>this : ⊤ ≤ LinearMap.ker (α - β)<GOAL>α - β = 0
<VAR>A B A' B' : CommRingCat<VAR>f : A ⟶ B<VAR>f' : A' ⟶ B'<VAR>g : A ⟶ A'<VAR>g' : B ⟶ B'<VAR>fac : g ≫ f' = f ≫ g'<VAR>M : ModuleCat ↑B<VAR>α β : KaehlerDifferential f ⟶ M<VAR>h : ∀ (b : ↑B), α (d b) = β (d b)<VAR>this : α - β = 0<GOAL>α - β = 0
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : InvolutiveInv G<VAR>inst✝ : ContinuousInv G<VAR>s : Set G<VAR>hs : IsCompact s<GOAL>IsCompact s⁻¹
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : InvolutiveInv G<VAR>inst✝ : ContinuousInv G<VAR>s : Set G<VAR>hs : IsCompact s<GOAL>IsCompact (Inv.inv '' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<GOAL>SpecializingMap f ↔ ∀ (x : X), StableUnderSpecialization (f '' closure {x})
<VAR>s t : Set ℝ<GOAL>interior (s ×ℂ t) = interior s ×ℂ interior t
<VAR>α : Type u_1<VAR>p q : α → Bool<VAR>l : List α<GOAL>countP (fun x => false) l = 0
<VAR>α : Type u_1<VAR>p q : α → Bool<VAR>l : List α<GOAL>∀ (a : α), a ∈ l → ¬false = true
<VAR>a b c : ℕ<GOAL>(Iic b).card = b + 1
<VAR>L : Language<VAR>α : Type w<VAR>M : Type w'<VAR>n : ℕ<VAR>inst✝ : LE M<GOAL>M ⊨ Language.order.noTopOrderSentence ↔ NoTopOrder M
<VAR>L : Language<VAR>α : Type w<VAR>M : Type w'<VAR>n : ℕ<VAR>inst✝ : LE M<GOAL>(∀ (a : M), ∃ a_1, ¬Fin.snoc (Fin.snoc default a) a_1 1 ≤ Fin.snoc (Fin.snoc default a) a_1 0) ↔ NoTopOrder M
<VAR>L : Language<VAR>α : Type w<VAR>M : Type w'<VAR>n : ℕ<VAR>inst✝ : LE M<VAR>h : NoTopOrder M<VAR>a : M<GOAL>∃ a_1, ¬Fin.snoc (Fin.snoc default a) a_1 1 ≤ Fin.snoc (Fin.snoc default a) a_1 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : CountablySeparated α<GOAL>∃ f, Measurable f ∧ Injective f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : CountablySeparated α<VAR>m' : MeasurableSpace α<VAR>left✝¹ : CountablyGenerated α<VAR>left✝ : SeparatesPoints α<VAR>m'le : m' ≤ inst✝¹<GOAL>∃ f, Measurable f ∧ Injective f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : CountablySeparated α<VAR>m' : MeasurableSpace α<VAR>left✝¹ : CountablyGenerated α<VAR>left✝ : SeparatesPoints α<VAR>m'le : m' ≤ inst✝¹<GOAL>Measurable (mapNatBool α)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>δ : Type u_4<VAR>mδ : MeasurableSpace δ<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>f : β → γ<VAR>g : γ → α<VAR>κ : Kernel α (β × γ)<VAR>a : α<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>(κ.snd a) s = (κ a) {p | p.2 ∈ s}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>δ : Type u_4<VAR>mδ : MeasurableSpace δ<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>f : β → γ<VAR>g : γ → α<VAR>κ : Kernel α (β × γ)<VAR>a : α<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>(κ a) (Prod.snd ⁻¹' s) = (κ a) {p | p.2 ∈ s}
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasureSpace Ω<VAR>inst✝⁵ : IsProbabilityMeasure ℙ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>p : ℝ≥0∞<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>X : ℕ → Ω → E<VAR>hℒp : Memℒp (X 0) p ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<GOAL>Tendsto (fun n => eLpNorm (fun ω => (↑n)⁻¹ • ∑ i ∈ range n, X i ω - ∫ (a : Ω), X 0 a) p ℙ) atTop (𝓝 0)
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasureSpace Ω<VAR>inst✝⁵ : IsProbabilityMeasure ℙ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>p : ℝ≥0∞<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>X : ℕ → Ω → E<VAR>hℒp : Memℒp (X 0) p ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ<GOAL>Tendsto (fun n => eLpNorm (fun ω => (↑n)⁻¹ • ∑ i ∈ range n, X i ω - ∫ (a : Ω), X 0 a) p ℙ) atTop (𝓝 0)
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasureSpace Ω<VAR>inst✝⁵ : IsProbabilityMeasure ℙ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>p : ℝ≥0∞<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>X : ℕ → Ω → E<VAR>hℒp : Memℒp (X 0) p ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ<VAR>hint : Integrable (X 0) ℙ<GOAL>Tendsto (fun n => eLpNorm (fun ω => (↑n)⁻¹ • ∑ i ∈ range n, X i ω - ∫ (a : Ω), X 0 a) p ℙ) atTop (𝓝 0)
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasureSpace Ω<VAR>inst✝⁵ : IsProbabilityMeasure ℙ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>p : ℝ≥0∞<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>X : ℕ → Ω → E<VAR>hℒp : Memℒp (X 0) p ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ<VAR>hint : Integrable (X 0) ℙ<VAR>havg : ∀ (n : ℕ), AEStronglyMeasurable (fun ω => (↑n)⁻¹ • ∑ i ∈ range n, X i ω) ℙ<GOAL>Tendsto (fun n => eLpNorm (fun ω => (↑n)⁻¹ • ∑ i ∈ range n, X i ω - ∫ (a : Ω), X 0 a) p ℙ) atTop (𝓝 0)
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasureSpace Ω<VAR>inst✝⁵ : IsProbabilityMeasure ℙ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>p : ℝ≥0∞<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>X : ℕ → Ω → E<VAR>hℒp : Memℒp (X 0) p ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ<VAR>hint : Integrable (X 0) ℙ<VAR>havg : ∀ (n : ℕ), AEStronglyMeasurable (fun ω => (↑n)⁻¹ • ∑ i ∈ range n, X i ω) ℙ<GOAL>UnifIntegrable (fun n ω => (↑n)⁻¹ • ∑ i ∈ range n, X i ω) p ℙ
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type u_2<VAR>inst✝ : MulAction R X<VAR>r₁ : R<VAR>r₂ : X<VAR>s t : ↥S<GOAL>(r₁ * ↑s /ₒ t) • (r₂ /ₒ s) = r₁ • r₂ /ₒ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : α → M<VAR>s : Set α<VAR>hs : (s ∩ mulSupport f).Infinite<GOAL>∏ᶠ (i : α) (_ : i ∈ s), f i = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : α → M<VAR>s : Set α<VAR>hs : (s ∩ mulSupport f).Infinite<GOAL>∏ᶠ (a : α), s.mulIndicator f a = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : α → M<VAR>s : Set α<VAR>hs : (s ∩ mulSupport f).Infinite<GOAL>(mulSupport (s.mulIndicator f)).Infinite
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : CommMonoid α<VAR>inst✝² : CommMonoid β<VAR>s A : Set α<VAR>t B : Set β<VAR>f✝ : α → β<VAR>a✝ : α<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : MulHomClass F α β<VAR>f : F<VAR>hf : InjOn (⇑f) (s * s)<VAR>h : ThreeGPFree s<VAR>a : α<VAR>ha : a ∈ s<VAR>b : α<VAR>hb : b ∈ s<VAR>c : α<VAR>hc : c ∈ s<VAR>habc : f a * f c = f b * f b<GOAL>f a = f b
<VAR>z✝ : ℂ<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>z : ℂ<GOAL>‖z‖ ≤ ↑(NNReal.sqrt 2) * ‖equivRealProdLm z‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivInvMonoid G<VAR>a✝ b✝ c a b : G<GOAL>a / b = a * (1 / b)
<VAR>t : Type u → Type u<VAR>inst✝⁵ : Traversable t<VAR>inst✝⁴ : LawfulTraversable t<VAR>F G : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : LawfulApplicative F<VAR>inst✝¹ : Applicative G<VAR>inst✝ : LawfulApplicative G<VAR>α β γ : Type u<VAR>g✝ : α → F β<VAR>h✝ : β → G γ<VAR>f : β → γ<VAR>x : t β<VAR>g : α → β<VAR>h : β → G γ<VAR>x✝ : t α<GOAL>traverse (h ∘ g) x✝ = (traverse h ∘ map g) x✝
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝³ : (i : ι) → CanonicallyOrderedAddCommMonoid (α i)<VAR>inst✝² : (i : ι) → Sub (α i)<VAR>inst✝¹ : ∀ (i : ι), OrderedSub (α i)<VAR>f g : Π₀ (i : ι), α i<VAR>i : ι<VAR>a b : α i<VAR>inst✝ : DecidableEq ι<VAR>j : ι<GOAL>(single i (a - b)) j = (single i a - single i b) j
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝³ : (i : ι) → CanonicallyOrderedAddCommMonoid (α i)<VAR>inst✝² : (i : ι) → Sub (α i)<VAR>inst✝¹ : ∀ (i : ι), OrderedSub (α i)<VAR>f g : Π₀ (i : ι), α i<VAR>i : ι<VAR>a b : α i<VAR>inst✝ : DecidableEq ι<GOAL>(single i (a - b)) i = (single i a - single i b) i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝³ : (i : ι) → CanonicallyOrderedAddCommMonoid (α i)<VAR>inst✝² : (i : ι) → Sub (α i)<VAR>inst✝¹ : ∀ (i : ι), OrderedSub (α i)<VAR>f g : Π₀ (i : ι), α i<VAR>i : ι<VAR>a b : α i<VAR>inst✝ : DecidableEq ι<VAR>j : ι<VAR>h : i ≠ j<GOAL>(single i (a - b)) j = (single i a - single i b) j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : AddCommMonoid M<VAR>v v₁ v₂ : α →₀ M<VAR>f : α ≃ β<VAR>x : α →₀ M<VAR>a : β<GOAL>(mapDomain (⇑f) x) a = x (f.symm a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : AddCommMonoid M<VAR>v v₁ v₂ : α →₀ M<VAR>f : α ≃ β<VAR>x : α →₀ M<VAR>a : β<GOAL>(mapDomain (⇑f) x) (f (f.symm a)) = x (f.symm a)
<VAR>ι✝ : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>x : ℕ → ι<VAR>p : ι → Prop<VAR>l : Filter ι<VAR>h_tendsto : Tendsto x atTop l<VAR>h : ∃ᶠ (n : ℕ) in atTop, p (x n)<GOAL>∃ ns, Tendsto (fun n => x (ns n)) atTop l ∧ ∀ (n : ℕ), p (x (ns n))
<VAR>ι✝ : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>x : ℕ → ι<VAR>p : ι → Prop<VAR>l : Filter ι<VAR>h_tendsto : Tendsto x atTop l<VAR>h : ∃ᶠ (n : ℕ) in atTop, p (x n)<VAR>ns : ℕ → ℕ<VAR>hge : ∀ (a : ℕ), ns a ≥ a<VAR>hns : ∀ (a : ℕ), p (x (ns a))<GOAL>∃ ns, Tendsto (fun n => x (ns n)) atTop l ∧ ∀ (n : ℕ), p (x (ns n))
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>p q : Submodule R M<VAR>hpq : p ≤ q<VAR>x : ↥(comap q.subtype p)<GOAL>(fun x => ⟨⟨↑x, ⋯⟩, ⋯⟩) ({ toFun := fun x => ⟨↑↑x, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }.toFun x) = x
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>p q : Submodule R M<VAR>hpq : p ≤ q<VAR>x : ↥p<GOAL>{ toFun := fun x => ⟨↑↑x, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }.toFun ((fun x => ⟨⟨↑x, ⋯⟩, ⋯⟩) x) = x
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>c₁✝ c₂✝ r x y z : R<VAR>a✝ b c : ℍ[R,c₁✝,c₂✝]<VAR>inst✝¹ : NoZeroDivisors R<VAR>inst✝ : CharZero R<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>star a = a ↔ a = ↑a.re
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>a : α<VAR>inst✝ : LinearOrder β<VAR>c : β<GOAL>c > fold min b f s ↔ b < c ∨ ∃ x ∈ s, f x < c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>a : α<VAR>inst✝ : LinearOrder β<VAR>c : β<GOAL>∀ {x y z : β}, x > min y z ↔ x > y ∨ x > z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>a : α<VAR>inst✝ : LinearOrder β<VAR>c x y z : β<GOAL>min y z < x ↔ x > y ∨ x > z
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>S : Type u_3<VAR>inst✝ : Group G<VAR>a b : G<VAR>h : Commute a b<GOAL>a * b * a⁻¹ = b
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>B c : ℝ<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>convexBodySumFun (c • x) = |c| * convexBodySumFun x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>c : F<VAR>hq_pos : 0 < q<VAR>inst✝ : IsProbabilityMeasure μ<GOAL>eLpNorm' (fun x => c) q μ = ↑‖c‖₊
<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>p : Sort u<VAR>f : M → ↥S → p<VAR>H : ∀ {a c : M} {b d : ↥S}, (r S) (a, b) (c, d) → f a b = f c d<VAR>a : M<VAR>b : ↥S<GOAL>((monoidOf S).mk' a b).liftOn f H = f a b
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝² : MetricSpace X<VAR>inst✝¹ : MetricSpace Y<VAR>Φ✝ : Z → X<VAR>Ψ✝ : Z → Y<VAR>ε✝ : ℝ<VAR>inst✝ : Nonempty Z<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>p : Z<GOAL>glueDist Φ Ψ ε (Sum.inl (Φ p)) (Sum.inr (Ψ p)) = ε
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝² : MetricSpace X<VAR>inst✝¹ : MetricSpace Y<VAR>Φ✝ : Z → X<VAR>Ψ✝ : Z → Y<VAR>ε✝ : ℝ<VAR>inst✝ : Nonempty Z<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>p : Z<VAR>this : ⨅ q, dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q) = 0<GOAL>glueDist Φ Ψ ε (Sum.inl (Φ p)) (Sum.inr (Ψ p)) = ε
<VAR>α : Type u_1<VAR>l : List α<VAR>x : α<GOAL>(∃ x, x ∈+ l) ↔ ¬l.Nodup
<VAR>M✝ : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : TopologicalSpace M✝<VAR>inst✝³ : Monoid M✝<VAR>inst✝² : TopologicalSpace X<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>inst✝ : TopologicalSpace M<VAR>f : M → M<VAR>hc : ContinuousOn f {x | IsUnit x}<VAR>hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹<GOAL>Embedding val
<VAR>M✝ : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : TopologicalSpace M✝<VAR>inst✝³ : Monoid M✝<VAR>inst✝² : TopologicalSpace X<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>inst✝ : TopologicalSpace M<VAR>f : M → M<VAR>hc : ContinuousOn f {x | IsUnit x}<VAR>hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹<GOAL>instTopologicalSpaceUnits = TopologicalSpace.induced val inst✝
<VAR>M✝ : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : TopologicalSpace M✝<VAR>inst✝³ : Monoid M✝<VAR>inst✝² : TopologicalSpace X<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>inst✝ : TopologicalSpace M<VAR>f : M → M<VAR>hc : ContinuousOn f {x | IsUnit x}<VAR>hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹<GOAL>∀ (x : Mˣ), ContinuousAt (fun u => ↑u⁻¹) x
<VAR>M✝ : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : TopologicalSpace M✝<VAR>inst✝³ : Monoid M✝<VAR>inst✝² : TopologicalSpace X<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>inst✝ : TopologicalSpace M<VAR>f : M → M<VAR>hc : ContinuousOn f {x | IsUnit x}<VAR>hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹<VAR>u : Mˣ<VAR>s : Set M<VAR>hs : s ∈ 𝓝 ((fun u => ↑u⁻¹) u)<GOAL>s ∈ Filter.map (fun u => ↑u⁻¹) (𝓝 u)
<VAR>M✝ : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : TopologicalSpace M✝<VAR>inst✝³ : Monoid M✝<VAR>inst✝² : TopologicalSpace X<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>inst✝ : TopologicalSpace M<VAR>f : M → M<VAR>hc : ContinuousOn f {x | IsUnit x}<VAR>hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹<VAR>u : Mˣ<VAR>s : Set M<VAR>hs : s ∈ 𝓝 (f ↑u)<GOAL>(fun u => f ↑u) ⁻¹' s ∈ comap val (𝓝 ↑u)
<VAR>R✝ : Type u_1<VAR>M : Type u_2<VAR>inst✝⁵ : CommRing R✝<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R✝ M<VAR>K : Type u_3<VAR>inst✝² : Field K<VAR>inst✝¹ : Module K M<VAR>f g : End K M<VAR>inst✝ : FiniteDimensional K M<VAR>hf : f.IsSemisimple<VAR>p : K[X]<VAR>R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}<VAR>this✝ : Finite K R<VAR>this : IsReduced R<GOAL>(aeval ((aeval f) p)) (minpoly K ((Ideal.Quotient.mkₐ K (Ideal.span {minpoly K f})) p)) = 0
<VAR>R : Type u<VAR>inst✝² : NonUnitalRing R<VAR>inst✝¹ : PartialOrder R<VAR>inst✝ : StarRing R<VAR>h_add : ∀ {x y : R}, x ≤ y → ∀ (z : R), z + x ≤ z + y<VAR>h_nonneg_iff : ∀ (x : R), 0 ≤ x ↔ ∃ s, x = star s * s<VAR>this : CovariantClass R R (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X✝ Y✝ : Ω → ℝ<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace β<VAR>X Y : Ω → β<VAR>inst✝¹ : NormedDivisionRing β<VAR>inst✝ : BorelSpace β<VAR>hXY : IndepFun X Y μ<VAR>h'XY : Integrable (X * Y) μ<VAR>hX : AEStronglyMeasurable X μ<VAR>hY : AEStronglyMeasurable Y μ<VAR>h'X : ¬X =ᶠ[ae μ] 0<GOAL>HasFiniteIntegral Y μ
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X✝ Y✝ : Ω → ℝ<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace β<VAR>X Y : Ω → β<VAR>inst✝¹ : NormedDivisionRing β<VAR>inst✝ : BorelSpace β<VAR>hXY : IndepFun X Y μ<VAR>h'XY : Integrable (X * Y) μ<VAR>hX : AEStronglyMeasurable X μ<VAR>hY : AEStronglyMeasurable Y μ<VAR>h'X : ¬X =ᶠ[ae μ] 0<VAR>I : ∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ ≠ 0<GOAL>HasFiniteIntegral Y μ
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X✝ Y✝ : Ω → ℝ<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace β<VAR>X Y : Ω → β<VAR>inst✝¹ : NormedDivisionRing β<VAR>inst✝ : BorelSpace β<VAR>hXY : IndepFun X Y μ<VAR>h'XY : Integrable (X * Y) μ<VAR>hX : AEStronglyMeasurable X μ<VAR>hY : AEStronglyMeasurable Y μ<VAR>h'X : ¬X =ᶠ[ae μ] 0<VAR>I : ∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ ≠ 0<VAR>H : ∫⁻ (a : Ω), ↑‖Y a‖₊ ∂μ = ⊤<GOAL>False
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X✝ Y✝ : Ω → ℝ<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace β<VAR>X Y : Ω → β<VAR>inst✝¹ : NormedDivisionRing β<VAR>inst✝ : BorelSpace β<VAR>hXY : IndepFun X Y μ<VAR>h'XY : Integrable (X * Y) μ<VAR>hX : AEStronglyMeasurable X μ<VAR>hY : AEStronglyMeasurable Y μ<VAR>h'X : ¬X =ᶠ[ae μ] 0<VAR>I : ∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ ≠ 0<VAR>H : ∫⁻ (a : Ω), ↑‖Y a‖₊ ∂μ = ⊤<VAR>J : IndepFun (fun ω => ↑‖X ω‖₊) (fun ω => ↑‖Y ω‖₊) μ<GOAL>False
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X✝ Y✝ : Ω → ℝ<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace β<VAR>X Y : Ω → β<VAR>inst✝¹ : NormedDivisionRing β<VAR>inst✝ : BorelSpace β<VAR>hXY : IndepFun X Y μ<VAR>h'XY : Integrable (X * Y) μ<VAR>hX : AEStronglyMeasurable X μ<VAR>hY : AEStronglyMeasurable Y μ<VAR>h'X : ¬X =ᶠ[ae μ] 0<VAR>I : ∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ ≠ 0<VAR>H : ∫⁻ (a : Ω), ↑‖Y a‖₊ ∂μ = ⊤<VAR>J : IndepFun (fun ω => ↑‖X ω‖₊) (fun ω => ↑‖Y ω‖₊) μ<VAR>A : ∫⁻ (ω : Ω), ↑‖X ω * Y ω‖₊ ∂μ < ⊤<GOAL>False
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X✝ Y✝ : Ω → ℝ<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace β<VAR>X Y : Ω → β<VAR>inst✝¹ : NormedDivisionRing β<VAR>inst✝ : BorelSpace β<VAR>hXY : IndepFun X Y μ<VAR>h'XY : Integrable (X * Y) μ<VAR>hX : AEStronglyMeasurable X μ<VAR>hY : AEStronglyMeasurable Y μ<VAR>h'X : ¬X =ᶠ[ae μ] 0<VAR>I : ∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ ≠ 0<VAR>H : ∫⁻ (a : Ω), ↑‖Y a‖₊ ∂μ = ⊤<VAR>J : IndepFun (fun ω => ↑‖X ω‖₊) (fun ω => ↑‖Y ω‖₊) μ<VAR>A : ∫⁻ (ω : Ω), ↑‖X ω‖₊ * ↑‖Y ω‖₊ ∂μ < ⊤<GOAL>False
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X✝ Y✝ : Ω → ℝ<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace β<VAR>X Y : Ω → β<VAR>inst✝¹ : NormedDivisionRing β<VAR>inst✝ : BorelSpace β<VAR>hXY : IndepFun X Y μ<VAR>h'XY : Integrable (X * Y) μ<VAR>hX : AEStronglyMeasurable X μ<VAR>hY : AEStronglyMeasurable Y μ<VAR>h'X : ¬X =ᶠ[ae μ] 0<VAR>I : ∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ ≠ 0<VAR>H : ∫⁻ (a : Ω), ↑‖Y a‖₊ ∂μ = ⊤<VAR>J : IndepFun (fun ω => ↑‖X ω‖₊) (fun ω => ↑‖Y ω‖₊) μ<VAR>A : (∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ) * ⊤ < ⊤<GOAL>False
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>t : R<VAR>n : ℤ<GOAL>(C t) n = if n = 0 then t else 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>t : R<VAR>n : ℤ<GOAL>(if 0 = n then t else 0) = if n = 0 then t else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ζ : Type u_6<VAR>r : α → α → Prop<VAR>a✝ b✝ c d : α<VAR>p : β → β → Prop<VAR>a b : α<VAR>f : α → β<VAR>h : ∀ (a b : α), r a b → TransGen p (f a) (f b)<VAR>hab : TransGen r a b<GOAL>TransGen p (f a) (f b)
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>a :: (l ++ []) ~ a :: l
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>s : Set α<VAR>inst✝ : CompleteLattice α<VAR>a : α<VAR>S : Set ↑(Iic a)<VAR>f : ι → ↑(Iic a)<VAR>p : ι → Prop<GOAL>↑(⨆ i, f i) = ⨆ i, ↑(f i)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>s : Set α<VAR>inst✝ : CompleteLattice α<VAR>a : α<VAR>S : Set ↑(Iic a)<VAR>f : ι → ↑(Iic a)<VAR>p : ι → Prop<GOAL>sSup (Subtype.val '' range fun i => f i) = ⨆ i, ↑(f i)
<VAR>x : ℝ*<VAR>r : ℝ<VAR>hxr : x.IsSt r<GOAL>(x - ↑r).Infinitesimal
<VAR>a b : ℤ<GOAL>Associated a b ↔ a = b ∨ a = -b
<VAR>a b : ℤ<GOAL>a.natAbs = b.natAbs ↔ a = b ∨ a = -b
<VAR>a b : Ordinal.{u_1}<GOAL>a.toPGame ≤ b.toPGame → a ≤ b
<VAR>a b : Ordinal.{u_1}<GOAL>¬a ≤ b → ¬a.toPGame ≤ b.toPGame
<VAR>a b : Ordinal.{u_1}<GOAL>b < a → b.toPGame ⧏ a.toPGame
<VAR>α : Type u_1<VAR>l r : Ordnode α<VAR>H : (∃ l', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'<GOAL>(∃ l', Raised l' r.dual.size ∧ BalancedSz l' l.dual.size) ∨ ∃ r', Raised l.dual.size r' ∧ BalancedSz r.dual.size r'