ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹⁴ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹³ : TopologicalSpace β<VAR>inst✝¹² : TopologicalSpace γ<VAR>inst✝¹¹ : TopologicalSpace δ<VAR>inst✝¹⁰ : MeasurableSpace β<VAR>inst✝⁹ : PseudoMetrizableSpace β<VAR>inst✝⁸ : BorelSpace β<VAR>inst✝⁷ : MeasurableSpace γ<VAR>inst✝⁶ : PseudoMetrizableSpace γ<VAR>inst✝⁵ : BorelSpace γ<VAR>inst✝⁴ : SecondCountableTopologyEither β γ<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : PseudoMetrizableSpace δ<VAR>inst✝¹ : OpensMeasurableSpace δ<VAR>inst✝ : SecondCountableTopology δ<VAR>g : β → γ → δ<VAR>hg : Measurable (uncurry g)<VAR>f₁ : α →ₘ[μ] β<VAR>f₂ : α →ₘ[μ] γ<GOAL>↑(comp₂Measurable g hg f₁ f₂) =ᶠ[ae μ] fun a => g (↑f₁ a) (↑f₂ a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹⁴ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹³ : TopologicalSpace β<VAR>inst✝¹² : TopologicalSpace γ<VAR>inst✝¹¹ : TopologicalSpace δ<VAR>inst✝¹⁰ : MeasurableSpace β<VAR>inst✝⁹ : PseudoMetrizableSpace β<VAR>inst✝⁸ : BorelSpace β<VAR>inst✝⁷ : MeasurableSpace γ<VAR>inst✝⁶ : PseudoMetrizableSpace γ<VAR>inst✝⁵ : BorelSpace γ<VAR>inst✝⁴ : SecondCountableTopologyEither β γ<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : PseudoMetrizableSpace δ<VAR>inst✝¹ : OpensMeasurableSpace δ<VAR>inst✝ : SecondCountableTopology δ<VAR>g : β → γ → δ<VAR>hg : Measurable (uncurry g)<VAR>f₁ : α →ₘ[μ] β<VAR>f₂ : α →ₘ[μ] γ<GOAL>↑(mk (fun a => g (↑f₁ a) (↑f₂ a)) ⋯) =ᶠ[ae μ] fun a => g (↑f₁ a) (↑f₂ a)
<VAR>z✝ : ℂ<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>z w : ℂ<VAR>h : z.re = w.re<GOAL>edist z w = edist z.im w.im
<VAR>t t' : Type u → Type u<VAR>eqv : (α : Type u) → t α ≃ t' α<VAR>inst✝⁵ : Traversable t<VAR>inst✝⁴ : LawfulTraversable t<VAR>F G : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : Applicative G<VAR>inst✝¹ : LawfulApplicative F<VAR>inst✝ : LawfulApplicative G<VAR>η : ApplicativeTransformation F G<VAR>α β γ : Type u<VAR>x : t' α<GOAL>Equiv.traverse eqv pure x = x
<VAR>a b m n✝ p : ℕ<VAR>P : ℕ → Prop<VAR>zero : P 0<VAR>one : P 1<VAR>prime : ∀ (p : ℕ), Prime p → P p<VAR>composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)<VAR>n : ℕ<GOAL>P n
<VAR>a b m n✝ p : ℕ<VAR>P : ℕ → Prop<VAR>zero : P 0<VAR>one : P 1<VAR>prime : ∀ (p : ℕ), Prime p → P p<VAR>composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)<VAR>n : ℕ<GOAL>∀ (p a : ℕ), Prime p → P a → P (p * a)
<VAR>α✝ : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>α : Type u<VAR>a : Set α<VAR>h : a.Finite<GOAL>{b | b ⊆ a}.Finite
<VAR>α✝ : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>α : Type u<VAR>a : Set α<VAR>h : a.Finite<GOAL>{b | b ⊆ a} = ↑(Finset.map Finset.coeEmb.toEmbedding h.toFinset.powerset)
<VAR>α✝ : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>α : Type u<VAR>a : Set α<VAR>h : a.Finite<VAR>s : Set α<GOAL>s ∈ {b | b ⊆ a} ↔ s ∈ ↑(Finset.map Finset.coeEmb.toEmbedding h.toFinset.powerset)
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>x y : E<VAR>s t : Set E<VAR>a b : ℝ<VAR>hab : a < b<GOAL>(interior (Icc a b)).Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Preorder α<VAR>inst✝³ : AddCommSemigroup α<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>a b c d : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>a + b ≤ a - c + (b + c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Preorder α<VAR>inst✝³ : AddCommSemigroup α<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>a b c d : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>b + a ≤ b + c + (a - c)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>n : ℕ<GOAL>constantCoeff (wittSub p n) = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>n : ℕ<GOAL>constantCoeff (X 0 - X 1) = 0
<VAR>𝕜 : Type u_1<VAR>S : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝¹³ : SeminormedCommRing S<VAR>inst✝¹² : SeminormedRing R<VAR>inst✝¹¹ : SeminormedAddCommGroup M<VAR>inst✝¹⁰ : Algebra S R<VAR>inst✝⁹ : Module S M<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Module Rᵐᵒᵖ M<VAR>inst✝⁶ : BoundedSMul S R<VAR>inst✝⁵ : BoundedSMul S M<VAR>inst✝⁴ : BoundedSMul R M<VAR>inst✝³ : BoundedSMul Rᵐᵒᵖ M<VAR>inst✝² : SMulCommClass R Rᵐᵒᵖ M<VAR>inst✝¹ : IsScalarTower S R M<VAR>inst✝ : IsScalarTower S Rᵐᵒᵖ M<VAR>m : M<GOAL>‖inr m‖₊ = ‖m‖₊
<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 : Finset β<VAR>h : s.Nonempty<VAR>f : β → α<GOAL>↑(s.sup f) = s.sup (WithBot.some ∘ f)
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra F K<VAR>S : Set E<VAR>x : Lifts F E K<VAR>s : E<VAR>h1 : IsIntegral (↥x.carrier) s<VAR>h2 : Splits x.emb.toRingHom (minpoly (↥x.carrier) s)<VAR>I2 : (minpoly (↥x.carrier) s).degree ≠ 0<VAR>this✝ : Algebra (↥x.carrier) K := x.emb.toAlgebra<VAR>carrier : IntermediateField F E := restrictScalars F (↥x.carrier)⟮s⟯<VAR>this : Algebra ↥x.carrier ↥carrier := (↥x.carrier)⟮s⟯.algebra<GOAL>rootOfSplits x.emb.toRingHom h2 I2 ∈ (minpoly (↥x.carrier) s).aroots K
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra F K<VAR>S : Set E<VAR>x : Lifts F E K<VAR>s : E<VAR>h1 : IsIntegral (↥x.carrier) s<VAR>h2 : Splits x.emb.toRingHom (minpoly (↥x.carrier) s)<VAR>I2 : (minpoly (↥x.carrier) s).degree ≠ 0<VAR>this✝ : Algebra (↥x.carrier) K := x.emb.toAlgebra<VAR>carrier : IntermediateField F E := restrictScalars F (↥x.carrier)⟮s⟯<VAR>this : Algebra ↥x.carrier ↥carrier := (↥x.carrier)⟮s⟯.algebra<GOAL>(aeval (rootOfSplits x.emb.toRingHom h2 I2)) (minpoly (↥x.carrier) s) = 0
<VAR>x✝ y z x : ℝ<GOAL>0 ≤ 0 ^ x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>m n✝ n : ℕ<GOAL>∃ k, Xor' (n = 2 * k) (n = 2 * k + 1)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>m n k : ℕ<GOAL>Xor' (k + k = 2 * k) (k + k = 2 * k + 1)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>m n k : ℕ<GOAL>Xor' (2 * k + 1 = 2 * k) (2 * k + 1 = 2 * k + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : Countable α<VAR>inst✝ : MeasurableSingletonClass α<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (a : α), f a ∂μ = ∑' (a : α), f a * μ {a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : Countable α<VAR>inst✝ : MeasurableSingletonClass α<VAR>f : α → ℝ≥0∞<GOAL>∑' (i : α), ∫⁻ (a : α), f a ∂μ {i} • dirac i = ∑' (a : α), f a * μ {a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : Countable α<VAR>inst✝ : MeasurableSingletonClass α<VAR>f : α → ℝ≥0∞<VAR>a : α<GOAL>∫⁻ (a : α), f a ∂μ {a} • dirac a = f a * μ {a}
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝ : CommMonoid M<VAR>f : α → M<VAR>s : Finset (Option α)<GOAL>∏ x ∈ eraseNone s, f x = ∏ x ∈ s, Option.elim' 1 f x
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>hμm : SigmaFinite (μ.trim hm)<VAR>f : α → F'<GOAL>μ[f|m] =ᶠ[ae μ] ↑↑(condexpL1 hm μ f)
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>hμm : SigmaFinite (μ.trim hm)<VAR>f : α → F'<GOAL>(if Integrable f μ then if StronglyMeasurable f then f else AEStronglyMeasurable'.mk ↑↑(condexpL1 hm μ f) ⋯ else 0) =ᶠ[ae μ] ↑↑(condexpL1 hm μ f)
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>hμm : SigmaFinite (μ.trim hm)<VAR>f : α → F'<VAR>hfi : ¬Integrable f μ<GOAL>(if Integrable f μ then if StronglyMeasurable f then f else AEStronglyMeasurable'.mk ↑↑(condexpL1 hm μ f) ⋯ else 0) =ᶠ[ae μ] ↑↑(condexpL1 hm μ f)
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>hμm : SigmaFinite (μ.trim hm)<VAR>f : α → F'<VAR>hfi : ¬Integrable f μ<GOAL>0 =ᶠ[ae μ] ↑↑0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a b c d : α<GOAL>b ⇨ b ⇨ a = b ⇨ a
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : CompleteSpace E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>μ ν✝ : Measure α<VAR>s t : Set α<VAR>f✝ g : α → E<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>ν : Measure α<VAR>inst✝ : IsFiniteMeasure ν<VAR>f : α → E<VAR>hμ : Integrable f μ<VAR>hν : Integrable f ν<GOAL>⨍ (x : α), f x ∂(μ + ν) = ((μ univ).toReal / ((μ univ).toReal + (ν univ).toReal)) • ⨍ (x : α), f x ∂μ + ((ν univ).toReal / ((μ univ).toReal + (ν univ).toReal)) • ⨍ (x : α), f x ∂ν
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : CompleteSpace E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>μ ν✝ : Measure α<VAR>s t : Set α<VAR>f✝ g : α → E<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>ν : Measure α<VAR>inst✝ : IsFiniteMeasure ν<VAR>f : α → E<VAR>hμ : Integrable f μ<VAR>hν : Integrable f ν<GOAL>⨍ (x : α), f x ∂(μ + ν) = (μ univ + ν univ).toReal⁻¹ • ∫ (x : α), f x ∂(μ + ν)
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₂.LeftHomologyData<VAR>inst✝² : Epi φ.τ₁<VAR>inst✝¹ : IsIso φ.τ₂<VAR>inst✝ : Mono φ.τ₃<GOAL>(ofEpiOfIsIsoOfMono' φ h).f' = φ.τ₁ ≫ h.f'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>s : Set α<VAR>a : α<VAR>ha : MeasurableSet {a}<GOAL>count {a} = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>s : Set α<VAR>a : α<VAR>ha : MeasurableSet {a}<GOAL>↑{a}.toFinset.card = 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : SMul α β<VAR>s s₁ s₂ t u : Finset β<VAR>a : α<VAR>b x : β<GOAL>x ∈ a • s ↔ ∃ y ∈ s, a • y = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>l✝ m : Language α<VAR>a b x : List α<VAR>l : Language α<GOAL>l∗.reverse = l.reverse∗
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : Set 𝕜<VAR>hs : 0 ∉ s<VAR>r : ℝ<VAR>c : 𝕜<VAR>hc : c ∈ s<GOAL>c • sphere 0 r = sphere 0 (‖c‖ * r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : Set 𝕜<VAR>hs : 0 ∉ s<VAR>r : ℝ<VAR>x✝ : E<GOAL>x✝ ∈ ⋃ c ∈ s, sphere 0 (‖c‖ * r) ↔ x✝ ∈ (fun x => ‖x‖) ⁻¹' ((fun x => ‖x‖ * r) '' s)
<VAR>n m m' : ℕ<VAR>h : n ^^^ m = n ^^^ m'<GOAL>m = m'
<VAR>cs₁ cs₂ : List Char<GOAL>utf8Len (cs₁ ++ cs₂) = utf8Len cs₁ + utf8Len cs₂
<VAR>α : Type u_1<VAR>inst✝ : OmegaCompletePartialOrder α<VAR>y : Scott α<GOAL>IsOpen (notBelow y)
<VAR>α : Type u_1<VAR>inst✝ : OmegaCompletePartialOrder α<VAR>y : Scott α<VAR>h : Monotone (notBelow y)<GOAL>IsOpen (notBelow y)
<VAR>α : Type u_1<VAR>inst✝ : OmegaCompletePartialOrder α<VAR>y : Scott α<VAR>h : Monotone (notBelow y)<VAR>c : Chain α<VAR>z : Prop<GOAL>{ toFun := fun x => x ∈ notBelow y, monotone' := h } (ωSup c) ≤ z ↔ ωSup (c.map { toFun := fun x => x ∈ notBelow y, monotone' := h }) ≤ z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α → ℕ → σ<VAR>g : α → List σ → Option σ<VAR>hg : Primrec₂ g<VAR>H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = some (f a n)<VAR>this : Primrec₂ fun a n => List.map (f a) (List.range n)<VAR>a : α<VAR>n : ℕ<GOAL>(List.map (f (a, n).1) (List.range (a, n).2.succ)).get? (a, n).2 = some (f a n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α → ℕ → σ<VAR>g : α → List σ → Option σ<VAR>hg : Primrec₂ g<VAR>H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = some (f a n)<VAR>a : α<VAR>n : ℕ<VAR>IH : Nat.rec (some []) (fun n IH => (a, n, IH).2.2.bind fun b => Option.map (fun b_1 => (((a, n, IH), b), b_1).1.2 ++ [(((a, n, IH), b), b_1).2]) (g ((a, n, IH), b).1.1 ((a, n, IH), b).2)) n = some (List.map (f a) (List.range n))<GOAL>Nat.rec (some []) (fun n IH => (a, n, IH).2.2.bind fun b => Option.map (fun b_1 => (((a, n, IH), b), b_1).1.2 ++ [(((a, n, IH), b), b_1).2]) (g ((a, n, IH), b).1.1 ((a, n, IH), b).2)) (n + 1) = some (List.map (f a) (List.range (n + 1)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ r : Rel α β<VAR>s : Rel β γ<VAR>x : γ<VAR>z : α<GOAL>(r • s).inv x z ↔ (s.inv • r.inv) x z
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁷ : CommSemiring R<VAR>inst✝¹⁶ : AddCommMonoid M<VAR>inst✝¹⁵ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹⁴ : CommRing R₁<VAR>inst✝¹³ : AddCommGroup M₁<VAR>inst✝¹² : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : AddCommGroup V<VAR>inst✝⁹ : Module K V<VAR>M'✝ : Type u_7<VAR>M'' : Type u_8<VAR>inst✝⁸ : AddCommMonoid M'✝<VAR>inst✝⁷ : AddCommMonoid M''<VAR>inst✝⁶ : Module R M'✝<VAR>inst✝⁵ : Module R M''<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M' : Type u_9<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : Module R M'<VAR>inst✝² : FiniteDimensional K V<VAR>ι : Type u_10<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Finite ι<VAR>B : BilinForm K V<VAR>hB : B.Nondegenerate<VAR>b : Basis ι K V<VAR>x : V<VAR>i : ι<GOAL>((B.dualBasis hB b).repr x) i = (B x) (b i)
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Semiring S<VAR>inst✝³ : Module S M<VAR>inst✝² : Module R M<VAR>inst✝¹ : SMul S R<VAR>inst✝ : IsScalarTower S R M<VAR>p : Submodule R M<GOAL>restrictScalars S p = ⊤ ↔ p = ⊤
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra 𝕜 A<VAR>inst✝ : IsAlgClosed 𝕜<VAR>a : A<VAR>ha : (σ a).Nonempty<VAR>n : ℕ<GOAL>σ (a ^ n) = (fun x => x ^ n) '' σ a
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<GOAL>closedBall x ε \ sphere x ε = ball x ε
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>x : ↥U<GOAL>toOpen R U ≫ (structureSheaf R).presheaf.germ x = toStalk R ↑x
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>x : ↥U<GOAL>toOpen R ⊤ ≫ germ (structureSheaf R).val ((fun x => ⟨↑x, ⋯⟩) x) = toStalk R ↑x
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝⁷ : NormedField 𝕜<VAR>inst✝⁶ : NormedRing 𝕝<VAR>inst✝⁵ : NormedSpace 𝕜 𝕝<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : SMulWithZero 𝕝 E<VAR>inst✝¹ : IsScalarTower 𝕜 𝕝 E<VAR>s t u v A B : Set E<VAR>x : E<VAR>a✝ b✝ : 𝕜<VAR>inst✝ : SMulCommClass 𝕝 𝕜 E<VAR>hs : Balanced 𝕝 s<VAR>a : 𝕜<VAR>b : 𝕝<VAR>ha : a • x ∈ s<VAR>hba : ‖b‖ ≤ ‖a‖<GOAL>b • x ∈ s
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝⁷ : NormedField 𝕜<VAR>inst✝⁶ : NormedRing 𝕝<VAR>inst✝⁵ : NormedSpace 𝕜 𝕝<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : SMulWithZero 𝕝 E<VAR>inst✝¹ : IsScalarTower 𝕜 𝕝 E<VAR>s t u v A B : Set E<VAR>x : E<VAR>a b✝ : 𝕜<VAR>inst✝ : SMulCommClass 𝕝 𝕜 E<VAR>hs : Balanced 𝕝 s<VAR>b : 𝕝<VAR>ha : 0 • x ∈ s<VAR>hba : ‖b‖ ≤ ‖0‖<GOAL>b • x ∈ s
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝⁷ : NormedField 𝕜<VAR>inst✝⁶ : NormedRing 𝕝<VAR>inst✝⁵ : NormedSpace 𝕜 𝕝<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : SMulWithZero 𝕝 E<VAR>inst✝¹ : IsScalarTower 𝕜 𝕝 E<VAR>s t u v A B : Set E<VAR>x : E<VAR>a✝ b✝ : 𝕜<VAR>inst✝ : SMulCommClass 𝕝 𝕜 E<VAR>hs : Balanced 𝕝 s<VAR>a : 𝕜<VAR>b : 𝕝<VAR>ha : a • x ∈ s<VAR>hba : ‖b‖ ≤ ‖a‖<VAR>ha₀ : a ≠ 0<GOAL>b • x ∈ s
<VAR>b o : Ordinal.{u_1}<VAR>hb : 1 < b<VAR>ho : o ≠ 0<VAR>hbo : b ≤ o<GOAL>log b (o % b ^ log b o) < log b o
<VAR>b o : Ordinal.{u_1}<VAR>hb : 1 < b<VAR>ho : o ≠ 0<VAR>hbo : b ≤ o<VAR>h : o % b ^ log b o = 0<GOAL>log b (o % b ^ log b o) < log b o
<VAR>b o : Ordinal.{u_1}<VAR>hb : 1 < b<VAR>ho : o ≠ 0<VAR>hbo : b ≤ o<VAR>h : o % b ^ log b o ≠ 0<GOAL>log b (o % b ^ log b o) < log b o
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f✝ f₁ f₂ : Filter α<VAR>g✝ g₁ g₂ : Filter β<VAR>m✝ : α → β<VAR>m' : β → γ<VAR>s✝ : Set α<VAR>t : Set β<VAR>f g : Filter α<VAR>m : α → β<VAR>s : Set α<VAR>hsf : s ∈ f<VAR>hsg : s ∈ g<VAR>hm : InjOn m s<GOAL>map m f = map m g ↔ f = g
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : LinearOrderedRing G<VAR>a x : G<GOAL>orderOf x ≤ 2
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : LinearOrderedRing G<VAR>a x : G<VAR>h : |x| ≠ 1<GOAL>orderOf x ≤ 2
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : LinearOrderedRing G<VAR>a x : G<VAR>h : |x| = 1<GOAL>orderOf x ≤ 2
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : LinearOrderedRing G<VAR>a : G<VAR>h : |1| = 1<GOAL>orderOf 1 ≤ 2
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : LinearOrderedRing G<VAR>a : G<VAR>h : |(-1)| = 1<GOAL>orderOf (-1) ≤ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<GOAL>{ ofColex := {a} } ≤ { ofColex := {b} } ↔ a ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Union α<VAR>a b : Part α<VAR>ma mb : α<VAR>ha : ma ∈ a<VAR>hb : mb ∈ b<GOAL>ma ∪ mb ∈ a ∪ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Union α<VAR>a b : Part α<VAR>ma mb : α<VAR>ha : ma ∈ a<VAR>hb : mb ∈ b<GOAL>∃ a_1 ∈ a, ∃ a ∈ b, a_1 ∪ a = ma ∪ mb
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>x✝ : Bornology α<VAR>s t : Set α<VAR>x : α<VAR>h : ¬IsBounded s<GOAL>s.Nonempty
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>x✝ : Bornology α<VAR>s t : Set α<VAR>x : α<VAR>h : ¬IsBounded s<GOAL>s ≠ ∅
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>x✝ : Bornology α<VAR>t : Set α<VAR>x : α<VAR>h : ¬IsBounded ∅<GOAL>False
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : Fintype τ<GOAL>esymm σ R 0 = 1
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : IsDomain R<VAR>inst✝⁶ : IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>b✝ : ι → M<VAR>S : Type u_4<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Finite ι<VAR>b : Basis ι R S<VAR>I : Ideal S<VAR>hI : I ≠ ⊥<GOAL>∃ b' a ab', ∀ (i : ι), ↑(ab' i) = a i • b' i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : IsDomain R<VAR>inst✝⁶ : IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>b✝ : ι → M<VAR>S : Type u_4<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Finite ι<VAR>b : Basis ι R S<VAR>I : Ideal S<VAR>hI : I ≠ ⊥<VAR>val✝ : Fintype ι<GOAL>∃ b' a ab', ∀ (i : ι), ↑(ab' i) = a i • b' i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : IsDomain R<VAR>inst✝⁶ : IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>b✝ : ι → M<VAR>S : Type u_4<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Finite ι<VAR>b : Basis ι R S<VAR>I : Ideal S<VAR>hI : I ≠ ⊥<VAR>val✝ : Fintype ι<VAR>bS : Basis ι R S<VAR>bI : Basis (Fin (Fintype.card ι)) R ↥(restrictScalars R I)<VAR>f : Fin (Fintype.card ι) ↪ ι<VAR>a : Fin (Fintype.card ι) → R<VAR>snf : ∀ (i : Fin (Fintype.card ι)), ↑(bI i) = a i • bS (f i)<GOAL>∃ b' a ab', ∀ (i : ι), ↑(ab' i) = a i • b' i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : IsDomain R<VAR>inst✝⁶ : IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>b✝ : ι → M<VAR>S : Type u_4<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Finite ι<VAR>b : Basis ι R S<VAR>I : Ideal S<VAR>hI : I ≠ ⊥<VAR>val✝ : Fintype ι<VAR>bS : Basis ι R S<VAR>bI : Basis (Fin (Fintype.card ι)) R ↥(restrictScalars R I)<VAR>f : Fin (Fintype.card ι) ↪ ι<VAR>a : Fin (Fintype.card ι) → R<VAR>snf : ∀ (i : Fin (Fintype.card ι)), ↑(bI i) = a i • bS (f i)<VAR>e : Fin (Fintype.card ι) ≃ ι := Equiv.ofBijective ⇑f ⋯<GOAL>∃ b' a ab', ∀ (i : ι), ↑(ab' i) = a i • b' i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : IsDomain R<VAR>inst✝⁶ : IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>b✝ : ι → M<VAR>S : Type u_4<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Finite ι<VAR>b : Basis ι R S<VAR>I : Ideal S<VAR>hI : I ≠ ⊥<VAR>val✝ : Fintype ι<VAR>bS : Basis ι R S<VAR>bI : Basis (Fin (Fintype.card ι)) R ↥(restrictScalars R I)<VAR>f : Fin (Fintype.card ι) ↪ ι<VAR>a : Fin (Fintype.card ι) → R<VAR>snf : ∀ (i : Fin (Fintype.card ι)), ↑(bI i) = a i • bS (f i)<VAR>e : Fin (Fintype.card ι) ≃ ι := Equiv.ofBijective ⇑f ⋯<VAR>fe : ∀ (i : ι), f (e.symm i) = i<GOAL>∃ b' a ab', ∀ (i : ι), ↑(ab' i) = a i • b' i