ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E'<VAR>inst✝³ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝² : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝¹ : TopologicalSpace M'<VAR>inst✝ : ChartedSpace H' M'<VAR>s : Set H<VAR>x : H<VAR>f : H → H'<VAR>e' : PartialHomeomorph H' H'<VAR>he' : e' ∈ contDiffGroupoid ⊤ I'<VAR>hs : s ⊆ f ⁻¹' e'.source<VAR>hx : f x ∈ e'.source<VAR>h : DifferentiableWithinAt 𝕜 (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)<VAR>A : (↑I' ∘ f ∘ ↑I.symm) (↑I x) ∈ ↑I'.symm ⁻¹' e'.source ∩ range ↑I'<GOAL>DifferentiableWithinAt 𝕜 (↑I' ∘ (↑e' ∘ f) ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E'<VAR>inst✝³ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝² : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝¹ : TopologicalSpace M'<VAR>inst✝ : ChartedSpace H' M'<VAR>s : Set H<VAR>x : H<VAR>f : H → H'<VAR>e' : PartialHomeomorph H' H'<VAR>he' : e' ∈ contDiffGroupoid ⊤ I'<VAR>hs : s ⊆ f ⁻¹' e'.source<VAR>hx : f x ∈ e'.source<VAR>h : DifferentiableWithinAt 𝕜 (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)<VAR>A : (↑I' ∘ f ∘ ↑I.symm) (↑I x) ∈ ↑I'.symm ⁻¹' e'.source ∩ range ↑I'<VAR>this : ContDiffWithinAt 𝕜 ⊤ (↑I' ∘ ↑e' ∘ ↑I'.symm) (↑I'.symm ⁻¹' e'.source ∩ range ↑I') ((↑I' ∘ f ∘ ↑I.symm) (↑I x))<GOAL>DifferentiableWithinAt 𝕜 (↑I' ∘ (↑e' ∘ f) ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E'<VAR>inst✝³ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝² : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝¹ : TopologicalSpace M'<VAR>inst✝ : ChartedSpace H' M'<VAR>s : Set H<VAR>x : H<VAR>f : H → H'<VAR>e' : PartialHomeomorph H' H'<VAR>he' : e' ∈ contDiffGroupoid ⊤ I'<VAR>hs : s ⊆ f ⁻¹' e'.source<VAR>hx : f x ∈ e'.source<VAR>h : DifferentiableWithinAt 𝕜 (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)<VAR>A : (↑I' ∘ f ∘ ↑I.symm) (↑I x) ∈ ↑I'.symm ⁻¹' e'.source ∩ range ↑I'<VAR>this : ContDiffWithinAt 𝕜 ⊤ (↑I' ∘ ↑e' ∘ ↑I'.symm) (↑I'.symm ⁻¹' e'.source ∩ range ↑I') ((↑I' ∘ f ∘ ↑I.symm) (↑I x))<GOAL>↑I' ∘ (↑e' ∘ f) ∘ ↑I.symm = (↑I' ∘ ↑e' ∘ ↑I'.symm) ∘ ↑I' ∘ f ∘ ↑I.symm
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E'<VAR>inst✝³ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝² : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝¹ : TopologicalSpace M'<VAR>inst✝ : ChartedSpace H' M'<VAR>s : Set H<VAR>x : H<VAR>f : H → H'<VAR>e' : PartialHomeomorph H' H'<VAR>he' : e' ∈ contDiffGroupoid ⊤ I'<VAR>hs : s ⊆ f ⁻¹' e'.source<VAR>hx : f x ∈ e'.source<VAR>h : DifferentiableWithinAt 𝕜 (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)<VAR>A : (↑I' ∘ f ∘ ↑I.symm) (↑I x) ∈ ↑I'.symm ⁻¹' e'.source ∩ range ↑I'<VAR>this : ContDiffWithinAt 𝕜 ⊤ (↑I' ∘ ↑e' ∘ ↑I'.symm) (↑I'.symm ⁻¹' e'.source ∩ range ↑I') ((↑I' ∘ f ∘ ↑I.symm) (↑I x))<GOAL>MapsTo (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I'.symm ⁻¹' e'.source ∩ range ↑I')
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : OrderedCancelAddCommMonoid α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<GOAL>map (addLeftEmbedding c) (Ioo a b) = Ioo (c + a) (c + b)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : OrderedCancelAddCommMonoid α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<GOAL>⇑(addLeftEmbedding c) '' Set.Ioo a b = Set.Ioo (c + a) (c + b)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β✝ : Type u_3<VAR>β' : Type u_4<VAR>γ✝ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β✝<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ✝<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β✝<VAR>τ : Measure γ✝<VAR>inst✝¹ : NormedAddCommGroup E<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>inst✝ : MeasurableSingletonClass α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>x : α<VAR>f : γ → β<VAR>hf : MeasurableEmbedding f<VAR>y y' : γ<GOAL>(fun y => (x, f y)) y = (fun y => (x, f y)) y' → y = y'
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β✝ : Type u_3<VAR>β' : Type u_4<VAR>γ✝ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β✝<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ✝<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β✝<VAR>τ : Measure γ✝<VAR>inst✝¹ : NormedAddCommGroup E<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>inst✝ : MeasurableSingletonClass α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>x : α<VAR>f : γ → β<VAR>hf : MeasurableEmbedding f<VAR>y y' : γ<GOAL>f y = f y' → y = y'
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β✝ : Type u_3<VAR>β' : Type u_4<VAR>γ✝ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β✝<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ✝<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β✝<VAR>τ : Measure γ✝<VAR>inst✝¹ : NormedAddCommGroup E<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>inst✝ : MeasurableSingletonClass α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>x : α<VAR>f : γ → β<VAR>hf : MeasurableEmbedding f<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>MeasurableSet ((fun y => (x, f y)) '' s)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β✝ : Type u_3<VAR>β' : Type u_4<VAR>γ✝ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β✝<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ✝<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β✝<VAR>τ : Measure γ✝<VAR>inst✝¹ : NormedAddCommGroup E<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>inst✝ : MeasurableSingletonClass α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>x : α<VAR>f : γ → β<VAR>hf : MeasurableEmbedding f<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>(fun y => (x, f y)) '' s = {x} ×ˢ (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>p : PMF α<VAR>s t : Set α<VAR>a : α<VAR>h : MeasurableSet {a}<GOAL>p.toMeasure {a} = p a
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f : Y ⟶ X<GOAL>(ofArrows (fun x => Y) fun x => f) = singleton f
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y✝ Z : C<VAR>f : Y✝ ⟶ X<VAR>Y : C<GOAL>(ofArrows (fun x => Y✝) fun x => f) = singleton f
<VAR>α✝ : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α✝<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α✝ Ω<VAR>μα : Measure α✝<VAR>μ : Measure Ω<VAR>inst✝¹ : IsMarkovKernel κ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>α : Type u_4<VAR>p : Set ι → Prop<VAR>f : Filter ι<VAR>ns : α → Set ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : iIndep s κ μα<VAR>hf : ∀ (t : Set ι), p t → tᶜ ∈ f<VAR>t : Set ι<VAR>ht : p t<GOAL>Indep (⨆ n ∈ t, s n) (limsup s f) κ μα
<VAR>α✝ : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α✝<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α✝ Ω<VAR>μα : Measure α✝<VAR>μ : Measure Ω<VAR>inst✝¹ : IsMarkovKernel κ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>α : Type u_4<VAR>p : Set ι → Prop<VAR>f : Filter ι<VAR>ns : α → Set ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : iIndep s κ μα<VAR>hf : ∀ (t : Set ι), p t → tᶜ ∈ f<VAR>t : Set ι<VAR>ht : p t<GOAL>limsup s f ≤ ⨆ n ∈ tᶜ, s n
<VAR>α✝ : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α✝<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α✝ Ω<VAR>μα : Measure α✝<VAR>μ : Measure Ω<VAR>inst✝¹ : IsMarkovKernel κ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>α : Type u_4<VAR>p : Set ι → Prop<VAR>f : Filter ι<VAR>ns : α → Set ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : iIndep s κ μα<VAR>hf : ∀ (t : Set ι), p t → tᶜ ∈ f<VAR>t : Set ι<VAR>ht : p t<GOAL>∀ᶠ (n : MeasurableSpace Ω) in Filter.map s f, n ≤ ⨆ n ∈ tᶜ, s n
<VAR>α✝ : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α✝<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α✝ Ω<VAR>μα : Measure α✝<VAR>μ : Measure Ω<VAR>inst✝¹ : IsMarkovKernel κ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>α : Type u_4<VAR>p : Set ι → Prop<VAR>f : Filter ι<VAR>ns : α → Set ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : iIndep s κ μα<VAR>hf : ∀ (t : Set ι), p t → tᶜ ∈ f<VAR>t : Set ι<VAR>ht : p t<GOAL>∀ᶠ (a : ι) in f, s a ≤ ⨆ n, ⨆ (_ : n ∉ t), s n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f fab : α → β<VAR>fbc : β → γ<VAR>ga ga' : α → α<VAR>gb gb' : β → β<VAR>gc gc' : γ → γ<VAR>hab : Semiconj fab ga gb<VAR>hbc : Semiconj fbc gb gc<VAR>x : α<GOAL>(fbc ∘ fab) (ga x) = gc ((fbc ∘ fab) x)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : SeminormedAddCommGroup F<VAR>f : ι → E<VAR>g : ι → ℝ≥0<VAR>a : ℝ≥0<VAR>hg : HasSum g a<VAR>h : ∀ (i : ι), ‖f i‖₊ ≤ g i<GOAL>‖∑' (i : ι), f i‖₊ ≤ a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : SeminormedAddCommGroup F<VAR>f : ι → E<VAR>g : ι → ℝ≥0<VAR>a : ℝ≥0<VAR>hg : HasSum (fun a => ↑(g a)) ↑a<VAR>h : ∀ (i : ι), ‖f i‖ ≤ ↑(g i)<GOAL>‖∑' (i : ι), f i‖ ≤ ↑a
<VAR>R : Type u_1<VAR>S✝ : Type u_2<VAR>x✝ y : R<VAR>n : ℕ<VAR>S : Type u_3<VAR>inst✝ : MonoidWithZero S<VAR>x : S<VAR>hx : IsNilpotent x<VAR>hn : n ≠ 0<GOAL>IsNilpotent (x ^ n)
<VAR>α : Type u_1<VAR>x✝ y z : ℝ<VAR>l : Filter α<VAR>x : ℝ<GOAL>rexp (x / 2) = √(rexp x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CompleteLattice α<VAR>s t : Set α<GOAL>DirSupInacc s ↔ ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x x_1 => x ≤ x_1) d → sSup d ∈ s → (d ∩ s).Nonempty
<VAR>α : Type u<VAR>inst✝³ : DecidableEq α<VAR>β : Type v<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Fintype β<VAR>σa : Perm α<VAR>σb : Perm β<GOAL>sign (σa.sumCongr σb) = sign σa * sign σb
<VAR>α : Type u<VAR>inst✝³ : DecidableEq α<VAR>β : Type v<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Fintype β<VAR>σa : Perm α<VAR>σb : Perm β<GOAL>sign (σa.sumCongr 1) = sign σa ∧ sign (sumCongr 1 σb) = sign σb
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hodd : p ≠ 2<GOAL>(Algebra.norm ℤ) (hζ.toInteger - 1) = ↑↑p
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : Nontrivial E<VAR>c : ℝ<VAR>hc : 0 ≤ c<GOAL>∃ x, ‖x‖ = c
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : Nontrivial E<VAR>c : ℝ<VAR>hc : 0 ≤ c<VAR>x : E<VAR>hx : x ≠ 0<GOAL>∃ x, ‖x‖ = c
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : Nontrivial E<VAR>c : ℝ<VAR>hc : 0 ≤ c<VAR>x : E<VAR>hx : ‖x‖ ≠ 0<GOAL>∃ x, ‖x‖ = c
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : Nontrivial E<VAR>c : ℝ<VAR>hc : 0 ≤ c<VAR>x : E<VAR>hx : ‖x‖ ≠ 0<GOAL>‖c • ‖x‖⁻¹ • x‖ = c
<VAR>B : Type u<VAR>inst✝ : Bicategory B<VAR>a b c d e : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<VAR>i : d ⟶ e<GOAL>(α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom ≫ (α_ f g (h ≫ i)).hom = (α_ f (g ≫ h) i).hom ≫ f ◁ (α_ g h i).hom
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>κ : Type u_7<VAR>inst✝ : TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>f✝ : X → (i : ι) → π i<VAR>f : Y → (i : ι) → π i<VAR>g : (i : ι) → π i<VAR>u : Filter Y<GOAL>Tendsto f u (𝓝 g) ↔ ∀ (x : ι), Tendsto (fun i => f i x) u (𝓝 (g x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>a : α<VAR>l : List α<VAR>m : ℕ<GOAL>(enumFrom n (a :: l))[m + 1]? = Option.map (fun a => (n + (m + 1), a)) (a :: l)[m + 1]?
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>a : α<VAR>l : List α<VAR>m : ℕ<GOAL>(enumFrom (n + 1) l)[m]? = Option.map (fun a => (n + (m + 1), a)) l[m]?
<VAR>𝓕 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : SeminormedGroup E<VAR>inst✝ : SeminormedGroup F<VAR>s : Set E<VAR>a✝ a₁ a₂ b✝ b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>a b : E<GOAL>dist (a * b) b = ‖a‖
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝²⁵ : CommRing R<VAR>inst✝²⁴ : CommRing S<VAR>inst✝²³ : Algebra R S<VAR>P : Generators R S<VAR>R' : Type u_1<VAR>S' : Type u_2<VAR>inst✝²² : CommRing R'<VAR>inst✝²¹ : CommRing S'<VAR>inst✝²⁰ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝¹⁹ : Algebra R R'<VAR>inst✝¹⁸ : Algebra S S'<VAR>inst✝¹⁷ : Algebra R S'<VAR>inst✝¹⁶ : IsScalarTower R R' S'<VAR>inst✝¹⁵ : IsScalarTower R S S'<VAR>R'' : Type ?u.199790<VAR>S'' : Type ?u.199793<VAR>inst✝¹⁴ : CommRing R''<VAR>inst✝¹³ : CommRing S''<VAR>inst✝¹² : Algebra R'' S''<VAR>P'' : Generators R'' S''<VAR>inst✝¹¹ : Algebra R R''<VAR>inst✝¹⁰ : Algebra S S''<VAR>inst✝⁹ : Algebra R S''<VAR>inst✝⁸ : IsScalarTower R R'' S''<VAR>inst✝⁷ : IsScalarTower R S S''<VAR>inst✝⁶ : Algebra R' R''<VAR>inst✝⁵ : Algebra S' S''<VAR>inst✝⁴ : Algebra R' S''<VAR>inst✝³ : IsScalarTower R' R'' S''<VAR>inst✝² : IsScalarTower R' S' S''<VAR>inst✝¹ : IsScalarTower R R' R''<VAR>inst✝ : IsScalarTower S S' S''<VAR>f : P.Hom P'<VAR>x : P.Ring<GOAL>(aeval P'.val) (f.toAlgHom x) = (algebraMap S S') ((aeval P.val) x)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝²⁵ : CommRing R<VAR>inst✝²⁴ : CommRing S<VAR>inst✝²³ : Algebra R S<VAR>P : Generators R S<VAR>R' : Type u_1<VAR>S' : Type u_2<VAR>inst✝²² : CommRing R'<VAR>inst✝²¹ : CommRing S'<VAR>inst✝²⁰ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝¹⁹ : Algebra R R'<VAR>inst✝¹⁸ : Algebra S S'<VAR>inst✝¹⁷ : Algebra R S'<VAR>inst✝¹⁶ : IsScalarTower R R' S'<VAR>inst✝¹⁵ : IsScalarTower R S S'<VAR>R'' : Type ?u.199790<VAR>S'' : Type ?u.199793<VAR>inst✝¹⁴ : CommRing R''<VAR>inst✝¹³ : CommRing S''<VAR>inst✝¹² : Algebra R'' S''<VAR>P'' : Generators R'' S''<VAR>inst✝¹¹ : Algebra R R''<VAR>inst✝¹⁰ : Algebra S S''<VAR>inst✝⁹ : Algebra R S''<VAR>inst✝⁸ : IsScalarTower R R'' S''<VAR>inst✝⁷ : IsScalarTower R S S''<VAR>inst✝⁶ : Algebra R' R''<VAR>inst✝⁵ : Algebra S' S''<VAR>inst✝⁴ : Algebra R' S''<VAR>inst✝³ : IsScalarTower R' R'' S''<VAR>inst✝² : IsScalarTower R' S' S''<VAR>inst✝¹ : IsScalarTower R R' R''<VAR>inst✝ : IsScalarTower S S' S''<VAR>f : P.Hom P'<VAR>x : P.Ring<GOAL>(AlgHom.restrictScalars R (aeval P'.val)).comp f.toAlgHom = (IsScalarTower.toAlgHom R S S').comp (aeval P.val)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝²⁵ : CommRing R<VAR>inst✝²⁴ : CommRing S<VAR>inst✝²³ : Algebra R S<VAR>P : Generators R S<VAR>R' : Type u_1<VAR>S' : Type u_2<VAR>inst✝²² : CommRing R'<VAR>inst✝²¹ : CommRing S'<VAR>inst✝²⁰ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝¹⁹ : Algebra R R'<VAR>inst✝¹⁸ : Algebra S S'<VAR>inst✝¹⁷ : Algebra R S'<VAR>inst✝¹⁶ : IsScalarTower R R' S'<VAR>inst✝¹⁵ : IsScalarTower R S S'<VAR>R'' : Type ?u.199790<VAR>S'' : Type ?u.199793<VAR>inst✝¹⁴ : CommRing R''<VAR>inst✝¹³ : CommRing S''<VAR>inst✝¹² : Algebra R'' S''<VAR>P'' : Generators R'' S''<VAR>inst✝¹¹ : Algebra R R''<VAR>inst✝¹⁰ : Algebra S S''<VAR>inst✝⁹ : Algebra R S''<VAR>inst✝⁸ : IsScalarTower R R'' S''<VAR>inst✝⁷ : IsScalarTower R S S''<VAR>inst✝⁶ : Algebra R' R''<VAR>inst✝⁵ : Algebra S' S''<VAR>inst✝⁴ : Algebra R' S''<VAR>inst✝³ : IsScalarTower R' R'' S''<VAR>inst✝² : IsScalarTower R' S' S''<VAR>inst✝¹ : IsScalarTower R R' R''<VAR>inst✝ : IsScalarTower S S' S''<VAR>f : P.Hom P'<VAR>x : P.Ring<GOAL>∀ (i : P.vars), ((AlgHom.restrictScalars R (aeval P'.val)).comp f.toAlgHom) (X i) = ((IsScalarTower.toAlgHom R S S').comp (aeval P.val)) (X i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>π : ι → Type u_6<VAR>s : ℕ → Set α<VAR>ω : α<GOAL>ω ∈ limsup s atTop ↔ ω ∈ {ω | Tendsto (fun n => ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 ω) atTop atTop}
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>π : ι → Type u_6<VAR>s : ℕ → Set α<VAR>ω : α<GOAL>(∀ (i : ℕ), ∃ i_1 ≥ i, ω ∈ s i_1) ↔ ω ∈ {ω | Tendsto (fun n => ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 ω) atTop atTop}
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.77057, u_1} C<VAR>inst✝ : Preadditive C<VAR>X✝ X Y : SimplicialObject C<VAR>f : X ⟶ Y<VAR>n : ℕ<GOAL>((alternatingFaceMapComplex C).map f ≫ (fun x => PInfty) Y).f n = ((fun x => PInfty) X ≫ (alternatingFaceMapComplex C).map f).f n
<VAR>α : Type u_1<VAR>inst✝² : CommRing α<VAR>inst✝¹ : IsDomain α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>a b c : α<VAR>h : a ∣ b - c<GOAL>gcd b a = gcd c a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝ : μ.OuterRegular<VAR>A : Set α<VAR>r : ℝ≥0∞<VAR>hr : μ A < r<GOAL>∃ U ⊇ A, IsOpen U ∧ μ U < r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝ : μ.OuterRegular<VAR>A : Set α<VAR>r : ℝ≥0∞<VAR>hr : μ A < r<VAR>U : Set α<VAR>hAU : U ⊇ toMeasurable μ A<VAR>hUo : IsOpen U<VAR>hU : μ U < r<GOAL>∃ U ⊇ A, IsOpen U ∧ μ U < r
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>v w : V<VAR>hvw : G.Adj v w<VAR>u : V<GOAL>u ∈ (G.subgraphOfAdj hvw).neighborSet v ↔ u ∈ {w}
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>v w : V<VAR>hvw : G.Adj v w<VAR>u : V<GOAL>w = u ↔ u = w
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>A : Type u_2<VAR>inst✝¹ : Field A<VAR>inst✝ : CharZero A<VAR>N : ℕ<VAR>hK : |discr K| ≤ ↑N<VAR>a : 𝓞 K<VAR>h : ℚ⟮↑a⟯ = ⊤<GOAL>(minpoly ℤ ↑a).natDegree ≤ rankOfDiscrBdd N
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>A : Type u_2<VAR>inst✝¹ : Field A<VAR>inst✝ : CharZero A<VAR>N : ℕ<VAR>hK : |discr K| ≤ ↑N<VAR>a : 𝓞 K<VAR>h : (minpoly ℤ ((algebraMap (𝓞 K) K) a)).natDegree = finrank ℚ K<GOAL>(minpoly ℤ ↑a).natDegree ≤ rankOfDiscrBdd N
<VAR>α : Type u_1<VAR>l : List α<GOAL>ofFn (get ⟨l, ⋯⟩) = ⟨l, ⋯⟩
<VAR>α : Type u_1<VAR>l : List α<GOAL>(ofFn (get ⟨l, ⋯⟩)).toList = toList ⟨l, ⋯⟩
<VAR>α : Type u_1<VAR>l : List α<GOAL>(ofFn (get ⟨l, ⋯⟩)).toList = l
<VAR>𝕜 : Type u_1<VAR>inst✝²⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁹ : NormedAddCommGroup E<VAR>inst✝¹⁸ : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹⁷ : NormedAddCommGroup E'<VAR>inst✝¹⁶ : NormedSpace 𝕜 E'<VAR>F : Type u_4<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>inst✝¹⁴ : NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>inst✝¹³ : TopologicalSpace H<VAR>H' : Type u_6<VAR>inst✝¹² : TopologicalSpace H'<VAR>G : Type u_7<VAR>inst✝¹¹ : TopologicalSpace G<VAR>G' : Type u_8<VAR>inst✝¹⁰ : TopologicalSpace G'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>J : ModelWithCorners 𝕜 F G<VAR>J' : ModelWithCorners 𝕜 F G'<VAR>M : Type u_9<VAR>inst✝⁹ : TopologicalSpace M<VAR>inst✝⁸ : ChartedSpace H M<VAR>M' : Type u_10<VAR>inst✝⁷ : TopologicalSpace M'<VAR>inst✝⁶ : ChartedSpace H' M'<VAR>N : Type u_11<VAR>inst✝⁵ : TopologicalSpace N<VAR>inst✝⁴ : ChartedSpace G N<VAR>N' : Type u_12<VAR>inst✝³ : TopologicalSpace N'<VAR>inst✝² : ChartedSpace G' N'<VAR>n : ℕ∞<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>inst✝ : SmoothManifoldWithCorners J N<VAR>h : E ≃ₘ^n⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F<VAR>hn : 1 ≤ n<VAR>s : Set E<GOAL>UniqueDiffOn 𝕜 (⇑h '' s) ↔ UniqueDiffOn 𝕜 s
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t s : Set α<VAR>p : α → Prop<VAR>h : ∀ᵐ (x : α) ∂μ.restrict s, p x<GOAL>∀ᵐ (x : α) ∂μ, x ∈ s → p x
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t s : Set α<VAR>p : α → Prop<VAR>h : (μ.restrict s) {a | ¬p a} = 0<GOAL>μ {a | ¬(a ∈ s → p a)} = 0
<VAR>𝕜 : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>s : Set H<VAR>hs : IsOpen s<GOAL>UniqueDiffOn 𝕜 (↑I.symm ⁻¹' s ∩ range ↑I)
<VAR>𝕜 : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>s : Set H<VAR>hs : IsOpen s<GOAL>UniqueDiffOn 𝕜 (range ↑I ∩ ↑I.symm ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace 𝕜 V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace 𝕜 W<VAR>n : ℕ∞<VAR>f : V →ᴬ[𝕜] W<GOAL>ContDiff 𝕜 n ⇑f
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace 𝕜 V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace 𝕜 W<VAR>n : ℕ∞<VAR>f : V →ᴬ[𝕜] W<GOAL>ContDiff 𝕜 n (⇑f.contLinear + Function.const V (f 0))
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace 𝕜 V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace 𝕜 W<VAR>n : ℕ∞<VAR>f : V →ᴬ[𝕜] W<GOAL>ContDiff 𝕜 n (Function.const V (f 0))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormalSpace Y<VAR>s : Set Y<VAR>f : ↑s →ᵇ ℝ<VAR>hs : IsClosed s<VAR>t : Set ℝ<VAR>inst✝ : t.OrdConnected<VAR>hf : ∀ (x : ↑s), f x ∈ t<VAR>hne : t.Nonempty<GOAL>∃ g, (∀ (y : Y), g y ∈ t) ∧ g.restrict s = f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormalSpace Y<VAR>s : Set Y<VAR>f : ↑s →ᵇ ℝ<VAR>hs : IsClosed s<VAR>t : Set ℝ<VAR>inst✝ : t.OrdConnected<VAR>hf : ∀ (x : ↑s), f x ∈ t<VAR>hne : t.Nonempty<VAR>g : Y →ᵇ ℝ<VAR>hg : ∀ (y : Y), g y ∈ t<VAR>hgf : ⇑g ∘ Subtype.val = ⇑f<GOAL>∃ g, (∀ (y : Y), g y ∈ t) ∧ g.restrict s = f
<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 α<VAR>f : β → α<VAR>inst✝ : TopologicalSpace β<VAR>hf : Inducing f<VAR>s : Set α<VAR>hs : IsSeparable s<GOAL>IsSeparable (f ⁻¹' s)
<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 α<VAR>f : β → α<VAR>inst✝ : TopologicalSpace β<VAR>hf : Inducing f<VAR>s : Set α<VAR>hs : IsSeparable s<VAR>this : SeparableSpace ↑s<GOAL>IsSeparable (f ⁻¹' s)
<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 α<VAR>f : β → α<VAR>inst✝ : TopologicalSpace β<VAR>hf : Inducing f<VAR>s : Set α<VAR>hs : IsSeparable s<VAR>this✝ : SeparableSpace ↑s<VAR>this : SecondCountableTopology ↑s<GOAL>IsSeparable (f ⁻¹' s)