ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>a₁ a₂ : α<VAR>s : Stream' α<GOAL>corec (fun s => s.head) (fun s => s.tail.tail) (a₁ :: a₂ :: s) = a₁ :: corec (fun s => s.head) (fun s => s.tail.tail) s
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>a₁ a₂ : α<VAR>s : Stream' α<GOAL>(a₁ :: a₂ :: s).head :: corec (fun s => s.head) (fun s => s.tail.tail) (a₁ :: a₂ :: s).tail.tail = a₁ :: corec (fun s => s.head) (fun s => s.tail.tail) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : DecidableEq β<VAR>f✝ g✝ : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>a : α<VAR>b c : β<VAR>β' : Type u_4<VAR>inst✝¹ : DecidableEq β'<VAR>inst✝ : DecidableEq γ<VAR>f : β → γ<VAR>g : α → β<VAR>f' : α → β'<VAR>g' : β' → γ<VAR>h_comm : ∀ (a : α), f (g a) = g' (f' a)<GOAL>image f (image g s) = image g' (image f' s)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousSMul 𝕜 E<VAR>ε : ι → 𝕜<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>hε : ∀ᶠ (n : ι) in l, ε n ≠ 0<VAR>S : Set E<VAR>H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)<GOAL>IsVonNBounded 𝕜 S
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousSMul 𝕜 E<VAR>ε : ι → 𝕜<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>hε : ∀ᶠ (n : ι) in l, ε n ≠ 0<VAR>S : Set E<VAR>H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)<GOAL>∀ (i : Set E), i ∈ 𝓝 0 ∧ Balanced 𝕜 i → Absorbs 𝕜 (id i) S
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousSMul 𝕜 E<VAR>ε : ι → 𝕜<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>hε : ∀ᶠ (n : ι) in l, ε n ≠ 0<VAR>S : Set E<VAR>H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)<VAR>H' : ∃ i, (i ∈ 𝓝 0 ∧ Balanced 𝕜 i) ∧ ¬Absorbs 𝕜 (id i) S<GOAL>False
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousSMul 𝕜 E<VAR>ε : ι → 𝕜<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>hε : ∀ᶠ (n : ι) in l, ε n ≠ 0<VAR>S : Set E<VAR>H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)<VAR>V : Set E<VAR>hVS : ¬Absorbs 𝕜 (id V) S<VAR>hV : V ∈ 𝓝 0<VAR>hVb : Balanced 𝕜 V<GOAL>False
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousSMul 𝕜 E<VAR>ε : ι → 𝕜<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>hε : ∀ᶠ (n : ι) in l, ε n ≠ 0<VAR>S : Set E<VAR>H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)<VAR>V : Set E<VAR>hVS : ¬Absorbs 𝕜 (id V) S<VAR>hV : V ∈ 𝓝 0<VAR>hVb : Balanced 𝕜 V<VAR>this : ∀ᶠ (n : ι) in l, ∃ x, ε n • ↑x ∉ V<GOAL>False
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousSMul 𝕜 E<VAR>ε : ι → 𝕜<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>hε : ∀ᶠ (n : ι) in l, ε n ≠ 0<VAR>S : Set E<VAR>H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)<VAR>V : Set E<VAR>hVS : ¬Absorbs 𝕜 (id V) S<VAR>hV : V ∈ 𝓝 0<VAR>hVb : Balanced 𝕜 V<VAR>this : ∀ᶠ (n : ι) in l, ∃ x, ε n • ↑x ∉ V<VAR>x : ι → ↑S<VAR>hx : ∀ᶠ (x_1 : ι) in l, ε x_1 • ↑(x x_1) ∉ V<GOAL>False
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousSMul 𝕜 E<VAR>ε : ι → 𝕜<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>hε : ∀ᶠ (n : ι) in l, ε n ≠ 0<VAR>S : Set E<VAR>H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)<VAR>V : Set E<VAR>hVS : ¬Absorbs 𝕜 (id V) S<VAR>hV : V ∈ 𝓝 0<VAR>hVb : Balanced 𝕜 V<VAR>this : ∀ᶠ (n : ι) in l, ∃ x, ε n • ↑x ∉ V<VAR>x : ι → ↑S<VAR>hx : ∀ᶠ (x_1 : ι) in l, ε x_1 • ↑(x x_1) ∉ V<GOAL>∀ᶠ (x : ι) in l, False
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>f : R[X]<VAR>T : Type u_1<VAR>inst✝¹ : CommRing T<VAR>inst✝ : Algebra R T<VAR>h : IsAdjoinRoot S f<VAR>a : S<GOAL>(h.aequiv h) a = AlgEquiv.refl a
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁹ : Category.{u_3, u_1} C<VAR>inst✝⁸ : Category.{u_4, u_2} D<VAR>inst✝⁷ : HasZeroMorphisms C<VAR>inst✝⁶ : HasZeroMorphisms D<VAR>S : ShortComplex C<VAR>h₁✝ : S.LeftHomologyData<VAR>h₂✝ : S.RightHomologyData<VAR>F✝ : C ⥤ D<VAR>inst✝⁵ : F✝.PreservesZeroMorphisms<VAR>hl : S.LeftHomologyData<VAR>hr : S.RightHomologyData<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hl₁ : S₁.LeftHomologyData<VAR>hr₁ : S₁.RightHomologyData<VAR>hl₂ : S₂.LeftHomologyData<VAR>hr₂ : S₂.RightHomologyData<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>F : C ⥤ D<VAR>inst✝⁴ : F.PreservesZeroMorphisms<VAR>inst✝³ : S₁.HasRightHomology<VAR>inst✝² : S₂.HasRightHomology<VAR>inst✝¹ : F.PreservesRightHomologyOf S₁<VAR>inst✝ : F.PreservesRightHomologyOf S₂<GOAL>opcyclesMap' (F.mapShortComplex.map φ) (F.mapShortComplex.obj S₁).rightHomologyData (F.mapShortComplex.obj S₂).rightHomologyData ≫ opcyclesMap' (𝟙 (S₂.map F)) (S₂.map F).rightHomologyData (S₂.rightHomologyData.map F) = opcyclesMap' (𝟙 (S₁.map F)) (S₁.map F).rightHomologyData (S₁.rightHomologyData.map F) ≫ F.map (opcyclesMap' φ S₁.rightHomologyData S₂.rightHomologyData)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsBezout R<VAR>a b c : R<VAR>hab : IsCoprime a b<VAR>k : ℕ<VAR>h : a * b = c ^ k<GOAL>∃ d, Associated (d ^ k) a
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>x : (Quotient.out 1).α<GOAL>typein (fun x x_1 => x < x_1) x = 0
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J₁ J₂ : GrothendieckTopology C<VAR>X : C<VAR>S : Sieve X<VAR>hS : S ∈ J₁.sieves X<GOAL>Presieve.IsSheafFor (Functor.closedSieves J₁) S.arrows
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J₁ J₂ : GrothendieckTopology C<VAR>X : C<VAR>S : Sieve X<VAR>hS : S ∈ J₁.sieves X<GOAL>Presieve.IsSeparatedFor (Functor.closedSieves J₁) S.arrows ∧ ∀ (x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows), x.Compatible → ∃ t, x.IsAmalgamation t
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w : ι → k<VAR>p : ι → P<VAR>h : ∑ i ∈ s, w i = 1<VAR>b₁ b₂ : P<GOAL>(s.weightedVSubOfPoint p b₁) w +ᵥ b₁ = (s.weightedVSubOfPoint p b₂) w +ᵥ b₂
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w : ι → k<VAR>p : ι → P<VAR>h : ∑ i ∈ s, w i = 1<VAR>b₁ b₂ : P<GOAL>b₁ -ᵥ b₂ + ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)) = 0
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w : ι → k<VAR>p : ι → P<VAR>h : ∑ i ∈ s, w i = 1<VAR>b₁ b₂ : P<GOAL>b₁ -ᵥ b₂ + ∑ x ∈ s, w x • (b₂ -ᵥ b₁) = 0
<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 : Set α<VAR>hs : NullMeasurableSet s (μ.restrict t)<VAR>u : Set α<VAR>hu : MeasurableSet u<GOAL>((μ.restrict t).restrict s) u = (μ.restrict (s ∩ t)) u
<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✝ : IsSimpleModule R N<VAR>f : M →ₗ[R] N<VAR>hf : Function.Surjective ⇑f<GOAL>IsCoatom (ker f)
<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✝ : IsSimpleModule R N<VAR>f : M →ₗ[R] N<VAR>hf : Function.Surjective ⇑f<GOAL>IsSimpleModule R (M ⧸ ker f)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>ι' : Type u_3<VAR>a b : α<VAR>h : {a} ≠ {b}<GOAL>(Disjoint on id) {a} {b}
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>f : α → β<VAR>hf : Isometry f<GOAL>Metric.diam (range f) = Metric.diam univ
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>f : α → β<VAR>hf : Isometry f<GOAL>Metric.diam (f '' univ) = Metric.diam univ
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → α → Prop<VAR>H : Transitive R<VAR>s✝ t✝ u✝ : WSeq α<VAR>h1✝ : LiftRel R s✝ t✝<VAR>h2✝ : LiftRel R t✝ u✝<VAR>s u t : WSeq α<VAR>h1 : LiftRel R s t<VAR>h2 : LiftRel R t u<GOAL>Computation.LiftRel (LiftRelO R fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) s.destruct u.destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → α → Prop<VAR>H : Transitive R<VAR>s✝ t✝ u✝ : WSeq α<VAR>h1✝¹ : LiftRel R s✝ t✝<VAR>h2✝ : LiftRel R t✝ u✝<VAR>s u t : WSeq α<VAR>h1✝ : LiftRel R s t<VAR>h2 : LiftRel R t u<VAR>h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct<GOAL>Computation.LiftRel (LiftRelO R fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) s.destruct u.destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → α → Prop<VAR>H : Transitive R<VAR>s✝ t✝ u✝ : WSeq α<VAR>h1✝¹ : LiftRel R s✝ t✝<VAR>h2✝¹ : LiftRel R t✝ u✝<VAR>s u t : WSeq α<VAR>h1✝ : LiftRel R s t<VAR>h2✝ : LiftRel R t u<VAR>h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct<VAR>h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct<GOAL>Computation.LiftRel (LiftRelO R fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) s.destruct u.destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → α → Prop<VAR>H : Transitive R<VAR>s✝ t✝ u✝ : WSeq α<VAR>h1✝¹ : LiftRel R s✝ t✝<VAR>h2✝¹ : LiftRel R t✝ u✝<VAR>s u t : WSeq α<VAR>h1✝ : LiftRel R s t<VAR>h2✝ : LiftRel R t u<VAR>h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct<VAR>h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct<VAR>a c : Option (α × WSeq α)<VAR>ha : a ∈ s.destruct<VAR>hc : c ∈ u.destruct<GOAL>LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) a c
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → α → Prop<VAR>H : Transitive R<VAR>s✝ t✝ u✝ : WSeq α<VAR>h1✝¹ : LiftRel R s✝ t✝<VAR>h2✝¹ : LiftRel R t✝ u✝<VAR>s u t : WSeq α<VAR>h1✝ : LiftRel R s t<VAR>h2✝ : LiftRel R t u<VAR>h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct<VAR>h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct<VAR>a c : Option (α × WSeq α)<VAR>ha : a ∈ s.destruct<VAR>hc : c ∈ u.destruct<VAR>b : Option (α × WSeq α)<VAR>hb : b ∈ t.destruct<VAR>t1 : LiftRelO R (LiftRel R) a b<GOAL>LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) a c
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → α → Prop<VAR>H : Transitive R<VAR>s✝ t✝ u✝ : WSeq α<VAR>h1✝¹ : LiftRel R s✝ t✝<VAR>h2✝¹ : LiftRel R t✝ u✝<VAR>s u t : WSeq α<VAR>h1✝ : LiftRel R s t<VAR>h2✝ : LiftRel R t u<VAR>h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct<VAR>h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct<VAR>a c : Option (α × WSeq α)<VAR>ha : a ∈ s.destruct<VAR>hc : c ∈ u.destruct<VAR>b : Option (α × WSeq α)<VAR>hb : b ∈ t.destruct<VAR>t1 : LiftRelO R (LiftRel R) a b<VAR>t2 : LiftRelO R (LiftRel R) b c<GOAL>LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) a c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>r : ℚ<GOAL>stieltjesFunctionAux f a ↑r = f a r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>r : ℚ<GOAL>⨅ q, f a ↑q = ⨅ r_1, f a ↑r_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>r : ℚ<GOAL>{ q' // ↑r < ↑q' } ≃ ↑(Ioi r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>r : ℚ<GOAL>∀ (x : { q' // ↑r < ↑q' }), f a ↑(?refine_1 x) = f a ↑x
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>tβ : TopologicalSpace β<VAR>inst✝⁶ : T2Space β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace α<VAR>s : Set γ<VAR>f : γ → β<VAR>inst✝³ : OpensMeasurableSpace β<VAR>tγ : TopologicalSpace γ<VAR>inst✝² : PolishSpace γ<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : BorelSpace γ<VAR>hs : MeasurableSet s<VAR>f_cont : ContinuousOn f s<VAR>f_inj : InjOn f s<GOAL>MeasurableSet (f '' s)
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>tβ : TopologicalSpace β<VAR>inst✝⁶ : T2Space β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace α<VAR>s : Set γ<VAR>f : γ → β<VAR>inst✝³ : OpensMeasurableSpace β<VAR>tγ : TopologicalSpace γ<VAR>inst✝² : PolishSpace γ<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : BorelSpace γ<VAR>hs : MeasurableSet s<VAR>f_cont : ContinuousOn f s<VAR>f_inj : InjOn f s<VAR>t' : TopologicalSpace γ<VAR>t't : t' ≤ tγ<VAR>t'_polish : PolishSpace γ<VAR>s_closed : IsClosed s<VAR>right✝ : IsOpen s<GOAL>MeasurableSet (f '' s)
<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>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x✝ : E<VAR>s✝ t : Set E<VAR>L L₁ L₂ : Filter E<VAR>iso : E ≃L[𝕜] F<VAR>f : F → G<VAR>s : Set F<VAR>x : E<GOAL>DifferentiableWithinAt 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) x ↔ DifferentiableWithinAt 𝕜 f s (iso x)
<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>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x✝ : E<VAR>s✝ t : Set E<VAR>L L₁ L₂ : Filter E<VAR>iso : E ≃L[𝕜] F<VAR>f : F → G<VAR>s : Set F<VAR>x : E<VAR>H : DifferentiableWithinAt 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) x<GOAL>DifferentiableWithinAt 𝕜 f s (iso x)
<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>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x✝ : E<VAR>s✝ t : Set E<VAR>L L₁ L₂ : Filter E<VAR>iso : E ≃L[𝕜] F<VAR>f : F → G<VAR>s : Set F<VAR>x : E<VAR>H : DifferentiableWithinAt 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) x<VAR>this : DifferentiableWithinAt 𝕜 ((f ∘ ⇑iso) ∘ ⇑iso.symm) s (iso x)<GOAL>DifferentiableWithinAt 𝕜 f s (iso x)
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : NonAssocRing α<VAR>inst✝ : ContinuousMul α<GOAL>Continuous fun a => -a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>f₁ f₂ : Filter α<GOAL>(f₁ ⊓ f₂) ×ˢ g = f₁ ×ˢ g ⊓ f₂ ×ˢ g
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op U))<VAR>n : ℕ<VAR>h : 0 < n<GOAL>X.basicOpen (f ^ n) = X.basicOpen f
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op U))<VAR>k : ℕ<VAR>h : 0 < k + Nat.succ 0<GOAL>X.basicOpen (f ^ (k + Nat.succ 0)) = X.basicOpen f
<VAR>R : Type u<VAR>inst✝³ : CommSemiring R<VAR>S : Type u_1<VAR>inst✝² : CommSemiring S<VAR>f : R →* S<VAR>g : R →+* S<VAR>p m n : ℕ<VAR>inst✝¹ : ExpChar R p<VAR>inst✝ : ExpChar S p<VAR>x y : R<GOAL>(iterateFrobenius R p 0) x = x
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>a : A<VAR>X : C<GOAL>(shiftFunctor C a).obj X = (shiftFunctor C (a + 0)).obj X
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>a : A<VAR>X : C<GOAL>(shiftFunctorAdd C a 0).inv.app X = (shiftFunctorZero C A).hom.app ((shiftFunctor C a).obj X) ≫ eqToHom ⋯
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : SeparationQuotient α × SeparationQuotient β → γ<GOAL>UniformContinuous f ↔ UniformContinuous fun p => f (mk p.1, mk p.2)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : SeparationQuotient α × SeparationQuotient β → γ<GOAL>Tendsto (((fun x => (f x.1, f x.2)) ∘ fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ∘ fun p => (Prod.map mk mk p.1, Prod.map mk mk p.2)) (𝓤 α ×ˢ 𝓤 β) (𝓤 γ) ↔ Tendsto ((fun x => (f (mk x.1.1, mk x.1.2), f (mk x.2.1, mk x.2.2))) ∘ fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 β) (𝓤 γ)
<VAR>C : Type u<VAR>𝒞 : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>X Y Y' : C<VAR>f : Y ⟶ Y'<VAR>Z : C<GOAL>(X ◁ f) ▷ Z = (α_ X Y Z).hom ≫ X ◁ f ▷ Z ≫ (α_ X Y' Z).inv
<VAR>C : Type u<VAR>𝒞 : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>X Y Y' : C<VAR>f : Y ⟶ Y'<VAR>Z : C<GOAL>(𝟙 X ⊗ f) ⊗ 𝟙 Z = (α_ X Y Z).hom ≫ (𝟙 X ⊗ f ⊗ 𝟙 Z) ≫ (α_ X Y' Z).inv
<VAR>C : Type u<VAR>𝒞 : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>X Y Y' : C<VAR>f : Y ⟶ Y'<VAR>Z : C<GOAL>(𝟙 X ⊗ f) ⊗ 𝟙 Z = (((𝟙 X ⊗ f) ⊗ 𝟙 Z) ≫ (α_ X Y' Z).hom) ≫ (α_ X Y' Z).inv
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s t : Set α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype ↑s<GOAL>s.toFinset = Finset.univ ↔ s = univ
<VAR>T : ℝ<GOAL>Subalgebra.toSubmodule fourierSubalgebra.toSubalgebra = span ℂ (range fourier)
<VAR>T : ℝ<GOAL>↑(Submonoid.closure (range fourier)) ⊆ ↑(span ℂ (range fourier))
<VAR>T : ℝ<GOAL>↑(Submonoid.closure (range fourier)) ⊆ range fourier
<VAR>T : ℝ<VAR>x : C(AddCircle T, ℂ)<VAR>hx : x ∈ ↑(Submonoid.closure (range fourier))<GOAL>x ∈ range fourier
<VAR>T : ℝ<VAR>x : C(AddCircle T, ℂ)<VAR>hx : x ∈ ↑(Submonoid.closure (range fourier))<GOAL>fourier 0 = 1
<VAR>T : ℝ<VAR>x : C(AddCircle T, ℂ)<VAR>hx : x ∈ ↑(Submonoid.closure (range fourier))<GOAL>∀ (x y : C(AddCircle T, ℂ)), x ∈ range fourier → y ∈ range fourier → x * y ∈ range fourier
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>h : Sbtw R x y z<VAR>hx : x ∉ s<VAR>hy : y ∈ s<GOAL>s.SOppSide x z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>h : Sbtw R x y z<VAR>hx : x ∉ s<VAR>hy : y ∈ s<VAR>hz : z ∈ s<GOAL>x ∈ s
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x z : P<VAR>hx : x ∉ s<VAR>hz : z ∈ s<VAR>t : R<VAR>ht0 : 0 ≤ t<VAR>ht1 : t ≤ 1<VAR>hy : (lineMap x z) t ∈ s<VAR>hyx : (lineMap x z) t ≠ x<VAR>hyz : (lineMap x z) t ≠ z<GOAL>x ∈ s
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x z : P<VAR>hx : x ∉ s<VAR>hz : z ∈ s<VAR>t : R<VAR>ht0 : 0 ≤ t<VAR>ht1 : t ≤ 1<VAR>hy : t • (z -ᵥ x) +ᵥ x ∈ s<VAR>hyx : (lineMap x z) t ≠ x<VAR>hyz : (lineMap x z) t ≠ z<GOAL>x ∈ s
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x z : P<VAR>hx : x ∉ s<VAR>hz : z ∈ s<VAR>t : R<VAR>ht0 : 0 ≤ t<VAR>ht1 : t ≤ 1<VAR>hy : t • (z -ᵥ x) +ᵥ x ∈ s<VAR>hyx : (lineMap x z) t ≠ x<VAR>hyz : (lineMap x z) t ≠ z<VAR>ht : t ≠ 1<GOAL>x ∈ s
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x z : P<VAR>hx : x ∉ s<VAR>hz : z ∈ s<VAR>t : R<VAR>ht0 : 0 ≤ t<VAR>ht1 : t ≤ 1<VAR>hy : t • (z -ᵥ x) +ᵥ x ∈ s<VAR>hyx : (lineMap x z) t ≠ x<VAR>hyz : (lineMap x z) t ≠ z<VAR>ht : t ≠ 1<VAR>hy' : t • (z -ᵥ x) +ᵥ x -ᵥ z ∈ s.direction<GOAL>x ∈ s
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x z : P<VAR>hx : x ∉ s<VAR>hz : z ∈ s<VAR>t : R<VAR>ht0 : 0 ≤ t<VAR>ht1 : t ≤ 1<VAR>hy : t • (z -ᵥ x) +ᵥ x ∈ s<VAR>hyx : (lineMap x z) t ≠ x<VAR>hyz : (lineMap x z) t ≠ z<VAR>ht : t ≠ 1<VAR>hy' : z -ᵥ x ∈ s.direction<GOAL>x ∈ s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : One α<VAR>s : Finset α<VAR>a : α<VAR>inst✝³ : DecidableEq β<VAR>inst✝² : One β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : OneHomClass F α β<VAR>f : F<GOAL>image (⇑f) 1 = 1
<VAR>p : ℂ × ℂ<VAR>hp : p.1 ∈ slitPlane<GOAL>HasStrictFDerivAt (fun x => x.1 ^ x.2) ((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℂ ℂ ℂ + (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℂ ℂ ℂ) p
<VAR>p : ℂ × ℂ<VAR>hp : p.1 ∈ slitPlane<VAR>A : p.1 ≠ 0<GOAL>HasStrictFDerivAt (fun x => x.1 ^ x.2) ((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℂ ℂ ℂ + (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℂ ℂ ℂ) p
<VAR>p : ℂ × ℂ<VAR>hp : p.1 ∈ slitPlane<VAR>A : p.1 ≠ 0<VAR>this : (fun x => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => cexp (log x.1 * x.2)<GOAL>HasStrictFDerivAt (fun x => x.1 ^ x.2) ((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℂ ℂ ℂ + (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℂ ℂ ℂ) p