ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z : ℂ<VAR>M r δ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>hf : TendstoLocallyUniformlyOn F f φ U<VAR>hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U<VAR>hU : IsOpen U<GOAL>∀ K ⊆ U, IsCompact K → TendstoUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ K
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z : ℂ<VAR>M r δ : ℝ<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>hU : IsOpen U<VAR>hf : TendstoLocallyUniformlyOn F f ⊥ U<VAR>hF : ∀ᶠ (n : ι) in ⊥, DifferentiableOn ℂ (F n) U<GOAL>∀ K ⊆ U, IsCompact K → TendstoUniformlyOn (deriv ∘ F) (deriv f) ⊥ K
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z : ℂ<VAR>M r δ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>hf : TendstoLocallyUniformlyOn F f φ U<VAR>hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U<VAR>hU : IsOpen U<VAR>hne : φ.NeBot<GOAL>∀ K ⊆ U, IsCompact K → TendstoUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ K
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K✝ : Set ℂ<VAR>z : ℂ<VAR>M r δ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>hf : TendstoLocallyUniformlyOn F f φ U<VAR>hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U<VAR>hU : IsOpen U<VAR>hne : φ.NeBot<VAR>K : Set ℂ<VAR>hKU : K ⊆ U<VAR>hK : IsCompact K<GOAL>TendstoUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ K
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K✝ : Set ℂ<VAR>z : ℂ<VAR>M r δ✝ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>hf : TendstoLocallyUniformlyOn F f φ U<VAR>hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U<VAR>hU : IsOpen U<VAR>hne : φ.NeBot<VAR>K : Set ℂ<VAR>hKU : K ⊆ U<VAR>hK : IsCompact K<VAR>δ : ℝ<VAR>hδ : δ > 0<VAR>hK4 : cthickening δ K ⊆ U<VAR>h : TendstoUniformlyOn (_root_.deriv ∘ F) (cderiv δ f) φ K<GOAL>TendstoUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ K
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K✝ : Set ℂ<VAR>z✝ : ℂ<VAR>M r δ✝ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>hf : TendstoLocallyUniformlyOn F f φ U<VAR>hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U<VAR>hU : IsOpen U<VAR>hne : φ.NeBot<VAR>K : Set ℂ<VAR>hKU : K ⊆ U<VAR>hK : IsCompact K<VAR>δ : ℝ<VAR>hδ : δ > 0<VAR>hK4 : cthickening δ K ⊆ U<VAR>h : TendstoUniformlyOn (_root_.deriv ∘ F) (cderiv δ f) φ K<VAR>z : ℂ<VAR>hz : z ∈ K<GOAL>closedBall z δ ⊆ U
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : MulZeroClass β<VAR>f f' : α → β<VAR>x : α<VAR>hf : HasCompactSupport f'<GOAL>HasCompactSupport (f * f')
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : MulZeroClass β<VAR>f f' : α → β<VAR>x : α<VAR>hf : f' =ᶠ[coclosedCompact α] 0<GOAL>f * f' =ᶠ[coclosedCompact α] 0
<VAR>a x✝ z x : ℂ<GOAL>x⁻¹.arg = if x.arg = π then π else -x.arg
<VAR>a x✝ z x : ℂ<GOAL>(↑(normSq x)⁻¹ * (starRingEnd ℂ) x).arg = ((starRingEnd ℂ) x).arg
<VAR>α : Type u_1<VAR>inst✝ : AddCommGroup α<VAR>p a a₁ a₂ b b₁ b₂ c : α<VAR>n : ℕ<VAR>z : ℤ<VAR>x✝ : a ≡ b [PMOD n • p]<VAR>m : ℤ<VAR>hm : b - a = m • n • p<GOAL>b - a = (m * ↑n) • p
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>f : ((a : α) → Part (β a)) → (a : α) → Part (β a)<VAR>x : α<VAR>h' : ¬∃ i, (Fix.approx f i x).Dom<GOAL>(assert (∃ i, (Fix.approx f i x).Dom) fun h => ⋯.fix (fixAux f) Upto.zero x) = none
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<GOAL>ContDiffAt 𝕜 ⊤ f x ↔ ∀ (n : ℕ), ContDiffAt 𝕜 (↑n) f x
<VAR>G : Type u_1<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : TopologicalGroup G<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : BorelSpace G<VAR>inst✝³ : CompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : IsFiniteMeasureOnCompacts μ'<VAR>s : Set G<VAR>_hs : MeasurableSet s<GOAL>μ' s = (μ'.haarScalarFactor μ • μ) s
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>this : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule<VAR>π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0<VAR>π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1<VAR>f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1<GOAL>Tendsto (fun p => normSq (↑(p 0) * ↑z + ↑(p 1))) cofinite atTop
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>this : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule<VAR>π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0<VAR>π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1<VAR>f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1<VAR>f_def : ⇑f = fun p => ↑(p 0) * ↑z + ↑(p 1)<GOAL>Tendsto (fun p => normSq (↑(p 0) * ↑z + ↑(p 1))) cofinite atTop
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule<VAR>π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0<VAR>π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1<VAR>f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1<VAR>f_def : ⇑f = fun p => ↑(p 0) * ↑z + ↑(p 1)<VAR>this : (fun p => normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p => Int.cast ∘ p<GOAL>Tendsto (fun p => normSq (↑(p 0) * ↑z + ↑(p 1))) cofinite atTop
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule<VAR>π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0<VAR>π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1<VAR>f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1<VAR>f_def : ⇑f = fun p => ↑(p 0) * ↑z + ↑(p 1)<VAR>this : (fun p => normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p => Int.cast ∘ p<VAR>hf : LinearMap.ker f = ⊥<GOAL>Tendsto (⇑normSq ∘ ⇑f ∘ fun p => Int.cast ∘ p) cofinite atTop
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule<VAR>π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0<VAR>π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1<VAR>f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1<VAR>f_def : ⇑f = fun p => ↑(p 0) * ↑z + ↑(p 1)<VAR>this : (fun p => normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p => Int.cast ∘ p<VAR>hf : LinearMap.ker f = ⊥<VAR>hf' : ClosedEmbedding ⇑f<GOAL>Tendsto (⇑normSq ∘ ⇑f ∘ fun p => Int.cast ∘ p) cofinite atTop
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>this✝ : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule<VAR>π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0<VAR>π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1<VAR>f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1<VAR>f_def : ⇑f = fun p => ↑(p 0) * ↑z + ↑(p 1)<VAR>this : (fun p => normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p => Int.cast ∘ p<VAR>hf : LinearMap.ker f = ⊥<VAR>hf' : ClosedEmbedding ⇑f<VAR>h₂ : Tendsto (fun p => Int.cast ∘ p) cofinite (cocompact (Fin 2 → ℝ))<GOAL>Tendsto (⇑normSq ∘ ⇑f ∘ fun p => Int.cast ∘ p) cofinite atTop
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v✝ w : V<VAR>ι : Type u_2<VAR>f : ι → G.Subgraph<VAR>hM : ∀ (i : ι), (f i).IsMatching<VAR>hd : Pairwise fun i j => Disjoint (f i).support (f j).support<VAR>v : V<VAR>hv : v ∈ (⨆ i, f i).verts<GOAL>∃! w, (⨆ i, f i).Adj v w
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v✝ w : V<VAR>ι : Type u_2<VAR>f : ι → G.Subgraph<VAR>hM : ∀ (i : ι), (f i).IsMatching<VAR>hd : Pairwise fun i j => Disjoint (f i).support (f j).support<VAR>v : V<VAR>hv : v ∈ (⨆ i, f i).verts<VAR>i : ι<VAR>hi : v ∈ (f i).verts<GOAL>∃! w, (⨆ i, f i).Adj v w
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v✝ w✝ : V<VAR>ι : Type u_2<VAR>f : ι → G.Subgraph<VAR>hM : ∀ (i : ι), (f i).IsMatching<VAR>hd : Pairwise fun i j => Disjoint (f i).support (f j).support<VAR>v : V<VAR>hv : v ∈ (⨆ i, f i).verts<VAR>i : ι<VAR>hi : v ∈ (f i).verts<VAR>w : V<VAR>hw : (fun w => (f i).Adj v w) w ∧ ∀ (y : V), (fun w => (f i).Adj v w) y → y = w<GOAL>∃! w, (⨆ i, f i).Adj v w
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v✝ w✝ : V<VAR>ι : Type u_2<VAR>f : ι → G.Subgraph<VAR>hM : ∀ (i : ι), (f i).IsMatching<VAR>hd : Pairwise fun i j => Disjoint (f i).support (f j).support<VAR>v : V<VAR>hv : v ∈ (⨆ i, f i).verts<VAR>i : ι<VAR>hi : v ∈ (f i).verts<VAR>w : V<VAR>hw : (fun w => (f i).Adj v w) w ∧ ∀ (y : V), (fun w => (f i).Adj v w) y → y = w<GOAL>(fun w => (⨆ i, f i).Adj v w) w ∧ ∀ (y : V), (fun w => (⨆ i, f i).Adj v w) y → y = w
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v✝ w✝ : V<VAR>ι : Type u_2<VAR>f : ι → G.Subgraph<VAR>hM : ∀ (i : ι), (f i).IsMatching<VAR>hd : Pairwise fun i j => Disjoint (f i).support (f j).support<VAR>v : V<VAR>hv : v ∈ (⨆ i, f i).verts<VAR>i : ι<VAR>hi : v ∈ (f i).verts<VAR>w : V<VAR>hw : (fun w => (f i).Adj v w) w ∧ ∀ (y : V), (fun w => (f i).Adj v w) y → y = w<GOAL>∀ (y : V), (fun w => (⨆ i, f i).Adj v w) y → y = w
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v✝ w✝ : V<VAR>ι : Type u_2<VAR>f : ι → G.Subgraph<VAR>hM : ∀ (i : ι), (f i).IsMatching<VAR>hd : Pairwise fun i j => Disjoint (f i).support (f j).support<VAR>v : V<VAR>hv : v ∈ (⨆ i, f i).verts<VAR>i : ι<VAR>hi : v ∈ (f i).verts<VAR>w : V<VAR>hw : (fun w => (f i).Adj v w) w ∧ ∀ (y : V), (fun w => (f i).Adj v w) y → y = w<VAR>y : V<VAR>hy : (⨆ i, f i).Adj v y<GOAL>y = w
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v✝ w✝ : V<VAR>ι : Type u_2<VAR>f : ι → G.Subgraph<VAR>hM : ∀ (i : ι), (f i).IsMatching<VAR>hd : Pairwise fun i j => Disjoint (f i).support (f j).support<VAR>v : V<VAR>hv : v ∈ (⨆ i, f i).verts<VAR>i : ι<VAR>hi : v ∈ (f i).verts<VAR>w : V<VAR>hw : (fun w => (f i).Adj v w) w ∧ ∀ (y : V), (fun w => (f i).Adj v w) y → y = w<VAR>y : V<VAR>hy : (⨆ i, f i).Adj v y<VAR>i' : ι<VAR>hi' : (f i').Adj v y<GOAL>y = w
<VAR>α : Type u<VAR>g : Set (Set α)<VAR>a : α<VAR>this : TopologicalSpace α := generateFrom g<GOAL>𝓝 a = ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s
<VAR>α : Type u<VAR>g : Set (Set α)<VAR>a : α<VAR>this : TopologicalSpace α := generateFrom g<GOAL>⨅ s ∈ {s | a ∈ s ∧ IsOpen s}, 𝓟 s = ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s
<VAR>α : Type u<VAR>g : Set (Set α)<VAR>a : α<VAR>this : TopologicalSpace α := generateFrom g<GOAL>∀ i ∈ {s | a ∈ s ∧ IsOpen s}, ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s ≤ 𝓟 i
<VAR>α : Type u<VAR>g : Set (Set α)<VAR>a : α<VAR>this : TopologicalSpace α := generateFrom g<VAR>s : Set α<VAR>ha : a ∈ s<VAR>hs : IsOpen s<GOAL>⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s ≤ 𝓟 s
<VAR>x✝ : ℕ<VAR>hk : x✝ ≤ 0<GOAL>0 < choose 0 x✝
<VAR>x✝ : ℕ<VAR>hk : x✝ ≤ 0<GOAL>0 < choose 0 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>s : Set α<VAR>hs : s.Countable<VAR>f : α → β<GOAL>(f '' s).Countable
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>s : Set α<VAR>hs : s.Countable<VAR>f : α → β<GOAL>(range fun x => f ↑x).Countable
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>s : Set α<VAR>hs : s.Countable<VAR>f : α → β<VAR>this : Countable ↑s<GOAL>(range fun x => f ↑x).Countable
<VAR>α : Type u_1<VAR>R✝ : Type u_2<VAR>k : Type u_3<VAR>S✝ : Type u_4<VAR>M : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>ι : Type u_8<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>F : Type u_9<VAR>inst✝⁵ : FunLike F M M₂<VAR>inst✝⁴ : AddMonoidHomClass F M M₂<VAR>f : F<VAR>R : Type u_10<VAR>S : Type u_11<VAR>inst✝³ : Semiring R<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module S M₂<VAR>x : ℕ<VAR>a : M<GOAL>f (↑x • a) = ↑x • f a
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P<VAR>X✝ : C<VAR>G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁<VAR>φ : F ⋙ yoneda ⟶ yoneda ⋙ G<VAR>X : C<GOAL>yonedaEquiv (presheafHom φ (yoneda.obj X)) = (φ.app X).app (F.op.obj (Opposite.op X)) (𝟙 (Opposite.unop (F.op.obj (Opposite.op X))))
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>s : Set X<VAR>hs : s.Countable<GOAL>dimH (⋃ x ∈ s, {x}) = 0
<VAR>u : Level<VAR>α : Q(Type u)<VAR>zα : Q(Zero «$α»)<VAR>pα : Q(PartialOrder «$α»)<VAR>A : Type u_1<VAR>e : A<VAR>n : ℤ<VAR>d : ℕ<VAR>inst✝ : LinearOrderedRing A<VAR>inv : Invertible ↑d<VAR>eq : e = ↑n * ⅟↑d<VAR>h : decide (n < 0) = true<GOAL>e ≠ 0
<VAR>u : Level<VAR>α : Q(Type u)<VAR>zα : Q(Zero «$α»)<VAR>pα : Q(PartialOrder «$α»)<VAR>A : Type u_1<VAR>e : A<VAR>n : ℤ<VAR>d : ℕ<VAR>inst✝ : LinearOrderedRing A<VAR>inv : Invertible ↑d<VAR>eq : e = ↑n * ⅟↑d<VAR>h : decide (n < 0) = true<VAR>pos_invOf_d : 0 < ⅟↑d<GOAL>e ≠ 0
<VAR>u : Level<VAR>α : Q(Type u)<VAR>zα : Q(Zero «$α»)<VAR>pα : Q(PartialOrder «$α»)<VAR>A : Type u_1<VAR>e : A<VAR>n : ℤ<VAR>d : ℕ<VAR>inst✝ : LinearOrderedRing A<VAR>inv : Invertible ↑d<VAR>eq : e = ↑n * ⅟↑d<VAR>h : decide (n < 0) = true<VAR>pos_invOf_d : 0 < ⅟↑d<VAR>neg_n : ↑n < 0<GOAL>e ≠ 0
<VAR>u : Level<VAR>α : Q(Type u)<VAR>zα : Q(Zero «$α»)<VAR>pα : Q(PartialOrder «$α»)<VAR>A : Type u_1<VAR>e : A<VAR>n : ℤ<VAR>d : ℕ<VAR>inst✝ : LinearOrderedRing A<VAR>inv : Invertible ↑d<VAR>eq : e = ↑n * ⅟↑d<VAR>h : decide (n < 0) = true<VAR>pos_invOf_d : 0 < ⅟↑d<VAR>neg_n : ↑n < 0<VAR>neg : ↑n * ⅟↑d < 0<GOAL>e ≠ 0
<VAR>u : Level<VAR>α : Q(Type u)<VAR>zα : Q(Zero «$α»)<VAR>pα : Q(PartialOrder «$α»)<VAR>A : Type u_1<VAR>e : A<VAR>n : ℤ<VAR>d : ℕ<VAR>inst✝ : LinearOrderedRing A<VAR>inv : Invertible ↑d<VAR>eq : e = ↑n * ⅟↑d<VAR>h : decide (n < 0) = true<VAR>pos_invOf_d : 0 < ⅟↑d<VAR>neg_n : ↑n < 0<VAR>neg : ↑n * ⅟↑d < 0<GOAL>↑n * ⅟↑d ≠ 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁷ : CommRing R<VAR>inst✝¹⁶ : CommRing S<VAR>inst✝¹⁵ : CommRing T<VAR>inst✝¹⁴ : Algebra R S<VAR>inst✝¹³ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : Field L<VAR>inst✝¹⁰ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝⁹ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁸ : Field F<VAR>inst✝⁷ : Algebra R L<VAR>inst✝⁶ : Algebra L F<VAR>inst✝⁵ : Algebra R F<VAR>inst✝⁴ : IsScalarTower R L F<VAR>inst✝³ : Algebra K F<VAR>inst✝² : IsScalarTower K L F<VAR>E : Type u_7<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra K E<VAR>pb : PowerBasis K L<VAR>hE : Splits (algebraMap K E) (minpoly K pb.gen)<VAR>hfx : IsSeparable K pb.gen<VAR>this✝ : DecidableEq E := Classical.decEq E<VAR>this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb<GOAL>(algebraMap K E) ((Algebra.trace K L) pb.gen) = ∑ σ : L →ₐ[K] E, σ pb.gen
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁷ : CommRing R<VAR>inst✝¹⁶ : CommRing S<VAR>inst✝¹⁵ : CommRing T<VAR>inst✝¹⁴ : Algebra R S<VAR>inst✝¹³ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : Field L<VAR>inst✝¹⁰ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝⁹ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁸ : Field F<VAR>inst✝⁷ : Algebra R L<VAR>inst✝⁶ : Algebra L F<VAR>inst✝⁵ : Algebra R F<VAR>inst✝⁴ : IsScalarTower R L F<VAR>inst✝³ : Algebra K F<VAR>inst✝² : IsScalarTower K L F<VAR>E : Type u_7<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra K E<VAR>pb : PowerBasis K L<VAR>hE : Splits (algebraMap K E) (minpoly K pb.gen)<VAR>hfx : IsSeparable K pb.gen<VAR>this✝ : DecidableEq E := Classical.decEq E<VAR>this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb<GOAL>((minpoly K pb.gen).aroots E).Nodup
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁷ : CommRing R<VAR>inst✝¹⁶ : CommRing S<VAR>inst✝¹⁵ : CommRing T<VAR>inst✝¹⁴ : Algebra R S<VAR>inst✝¹³ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : Field L<VAR>inst✝¹⁰ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝⁹ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁸ : Field F<VAR>inst✝⁷ : Algebra R L<VAR>inst✝⁶ : Algebra L F<VAR>inst✝⁵ : Algebra R F<VAR>inst✝⁴ : IsScalarTower R L F<VAR>inst✝³ : Algebra K F<VAR>inst✝² : IsScalarTower K L F<VAR>E : Type u_7<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra K E<VAR>pb : PowerBasis K L<VAR>hE : Splits (algebraMap K E) (minpoly K pb.gen)<VAR>hfx : IsSeparable K pb.gen<VAR>this✝ : DecidableEq E := Classical.decEq E<VAR>this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb<GOAL>{ x // x ∈ (minpoly K pb.gen).aroots E } → E
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁷ : CommRing R<VAR>inst✝¹⁶ : CommRing S<VAR>inst✝¹⁵ : CommRing T<VAR>inst✝¹⁴ : Algebra R S<VAR>inst✝¹³ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : Field L<VAR>inst✝¹⁰ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝⁹ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁸ : Field F<VAR>inst✝⁷ : Algebra R L<VAR>inst✝⁶ : Algebra L F<VAR>inst✝⁵ : Algebra R F<VAR>inst✝⁴ : IsScalarTower R L F<VAR>inst✝³ : Algebra K F<VAR>inst✝² : IsScalarTower K L F<VAR>E : Type u_7<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra K E<VAR>pb : PowerBasis K L<VAR>hE : Splits (algebraMap K E) (minpoly K pb.gen)<VAR>hfx : IsSeparable K pb.gen<VAR>this✝ : DecidableEq E := Classical.decEq E<VAR>this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb<GOAL>∀ (x : { x // x ∈ (minpoly K pb.gen).aroots E }), ?f x = _root_.id ↑x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁷ : CommRing R<VAR>inst✝¹⁶ : CommRing S<VAR>inst✝¹⁵ : CommRing T<VAR>inst✝¹⁴ : Algebra R S<VAR>inst✝¹³ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : Field L<VAR>inst✝¹⁰ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝⁹ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁸ : Field F<VAR>inst✝⁷ : Algebra R L<VAR>inst✝⁶ : Algebra L F<VAR>inst✝⁵ : Algebra R F<VAR>inst✝⁴ : IsScalarTower R L F<VAR>inst✝³ : Algebra K F<VAR>inst✝² : IsScalarTower K L F<VAR>E : Type u_7<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra K E<VAR>pb : PowerBasis K L<VAR>hE : Splits (algebraMap K E) (minpoly K pb.gen)<VAR>hfx : IsSeparable K pb.gen<VAR>this✝ : DecidableEq E := Classical.decEq E<VAR>this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb<GOAL>∀ (x : L →ₐ[K] E), x pb.gen = ?f (pb.liftEquiv' x)
<VAR>m n✝ n : ℤ<GOAL>∃ k, n = 2 * k ∨ n = 2 * k + 1
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : DivisionSemiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>S : Type u_4<VAR>F : Type u_5<VAR>N : Type u_6<VAR>inst✝⁴ : DivisionSemiring S<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module S N<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : AddMonoidHomClass F M N<VAR>g' : F<VAR>f : α → α<VAR>g : α → M<VAR>n : ℕ<VAR>x : α<GOAL>g' (birkhoffAverage R f g n x) = birkhoffAverage S f (⇑g' ∘ g) n x
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>a : α<VAR>x : γ<GOAL>x ∈ {x | 1 ≤ κ.rnDerivAux (κ + η) a x} ↔ 1 ≤ κ.rnDerivAux (κ + η) a x
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>h : T.IsMaximal<VAR>φ : L.Sentence<VAR>hφ : T ⊨ᵇ φ<GOAL>φ ∈ T
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>h : T.IsMaximal<VAR>φ : L.Sentence<VAR>hφ : T ⊨ᵇ φ<VAR>con : Formula.not φ ∈ T<GOAL>False
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>h : T.IsMaximal<VAR>φ : L.Sentence<VAR>hφ : ¬T.IsSatisfiable<VAR>con : Formula.not φ ∈ T<GOAL>False
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>h e f : L<VAR>t : IsSl2Triple h e f<GOAL>⁅h, f⁆ = -(2 • f)
<VAR>α✝ : Sort u<VAR>β✝ : Sort v<VAR>γ : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>p : α → Prop<GOAL>{b | p (e.symm b)} = ⇑e '' {a | p a}
<VAR>a b m n p✝ p q : ℕ<VAR>hp : Prime p<VAR>h : p.factorization q ≠ 0<GOAL>p = q
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : R[X]<GOAL>(map f p).degree ≤ p.degree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m✝ n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : R[X]<VAR>m : ℕ<VAR>hm : p.degree < ↑m<GOAL>(map f p).coeff m = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m✝ n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : R[X]<VAR>m : ℕ<VAR>hm : ∀ (m_1 : ℕ), m ≤ m_1 → p.coeff m_1 = 0<GOAL>(map f p).coeff m = 0
<VAR>n : ℕ<GOAL>map Prod.swap (antidiagonal n) = (antidiagonal n).reverse
<VAR>n : ℕ<GOAL>map (Prod.swap ∘ fun i => (i, n - i)) (range (n + 1)) = map ((fun i => (i, n - i)) ∘ fun x => 0 + (n + 1) - 1 - x) (range (n + 1))
<VAR>n : ℕ<GOAL>∀ a ∈ range (n + 1), (Prod.swap ∘ fun i => (i, n - i)) a = ((fun i => (i, n - i)) ∘ fun x => 0 + (n + 1) - 1 - x) a
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b c d : R<VAR>n✝ m : ℕ<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>hn : 0 < n<VAR>a : R<VAR>h : X ^ n + C a = 1<GOAL>n = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x y✝ : α<VAR>hx : f x ≠ x<VAR>hf : f.IsCycle<VAR>y : α<VAR>x✝ : f.SameCycle x y<VAR>hy : f y = y<VAR>i : ℤ<VAR>hi : (f ^ i) x = y<GOAL>f x = x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x y✝ : α<VAR>hx : f x ≠ x<VAR>hf : f.IsCycle<VAR>y : α<VAR>x✝ : f.SameCycle x y<VAR>hy : f y = y<VAR>i : ℤ<VAR>hi : x = y<GOAL>f x = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a : Ordinal.{u_4}<VAR>a0 : a ≠ 0<VAR>b : Ordinal.{u_4}<GOAL>a * (a * b / a) = a * b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedRing α<VAR>f g : ι → α<VAR>s : Set ι<VAR>a b c d : α<GOAL>Monovary f g ↔ ∀ (i j : ι), 0 ≤ (f j - f i) * (g j - g i)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹¹ : ConditionallyCompleteLinearOrder α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : OrderTopology α<VAR>inst✝⁸ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁷ : TopologicalSpace β<VAR>inst✝⁶ : OrderTopology β<VAR>inst✝⁵ : Nonempty γ<VAR>inst✝⁴ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>δ : Type u_1<VAR>inst✝³ : LinearOrder δ<VAR>inst✝² : TopologicalSpace δ<VAR>inst✝¹ : OrderClosedTopology δ<VAR>inst✝ : BoundedOrder α<VAR>f : α → δ<VAR>hf_c : Continuous f<VAR>hf : f ⊥ ≤ f ⊤<VAR>hf_i : Injective f<VAR>a b : α<VAR>hab : a < b<GOAL>f a < f b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹¹ : ConditionallyCompleteLinearOrder α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : OrderTopology α<VAR>inst✝⁸ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁷ : TopologicalSpace β<VAR>inst✝⁶ : OrderTopology β<VAR>inst✝⁵ : Nonempty γ<VAR>inst✝⁴ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>δ : Type u_1<VAR>inst✝³ : LinearOrder δ<VAR>inst✝² : TopologicalSpace δ<VAR>inst✝¹ : OrderClosedTopology δ<VAR>inst✝ : BoundedOrder α<VAR>f : α → δ<VAR>hf_c : Continuous f<VAR>hf : f ⊥ ≤ f ⊤<VAR>hf_i : Injective f<VAR>a b : α<VAR>hab : a < b<VAR>h : f b ≤ f a<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹¹ : ConditionallyCompleteLinearOrder α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : OrderTopology α<VAR>inst✝⁸ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁷ : TopologicalSpace β<VAR>inst✝⁶ : OrderTopology β<VAR>inst✝⁵ : Nonempty γ<VAR>inst✝⁴ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>δ : Type u_1<VAR>inst✝³ : LinearOrder δ<VAR>inst✝² : TopologicalSpace δ<VAR>inst✝¹ : OrderClosedTopology δ<VAR>inst✝ : BoundedOrder α<VAR>f : α → δ<VAR>hf_c : Continuous f<VAR>hf : f ⊥ ≤ f ⊤<VAR>hf_i : Injective f<VAR>a b : α<VAR>hab : a < b<VAR>h : f b ≤ f a<VAR>H : f b < f a<GOAL>False