ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>f✝ : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝³ : CompleteSpace E<VAR>f f' : ℝ → E<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra ℝ A<VAR>inst✝ : CompleteSpace A<VAR>u v u' v' : ℝ → A<VAR>hu : ContinuousOn u [[a, b]]<VAR>hv : ContinuousOn v [[a, b]]<VAR>huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x<VAR>hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x<VAR>hu' : IntervalIntegrable u' volume a b<VAR>hv' : IntervalIntegrable v' volume a b<GOAL>IntervalIntegrable (fun x => u' x * v x) volume a b
<VAR>α✝ : Sort u<VAR>β✝ : Sort v<VAR>γ : Sort w<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>e : α ≃ β<VAR>x : β<VAR>y : α<VAR>H : e.symm x = y<GOAL>x = e y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>A : Matrix α β ℤ<VAR>v : β → ℤ<VAR>hn : m < n<VAR>hm : 0 < m<VAR>hA : A ≠ 0<GOAL>∃ t, t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ (↑n * ‖A‖) ^ e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>A : Matrix α β ℤ<VAR>v : β → ℤ<VAR>hn : m < n<VAR>hm : 0 < m<VAR>hA : A ≠ 0<VAR>this : ∃ t, t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ (↑n * max 1 ‖A‖) ^ e<GOAL>∃ t, t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ (↑n * ‖A‖) ^ e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>A : Matrix α β ℤ<VAR>v : β → ℤ<VAR>hn : m < n<VAR>hm : 0 < m<VAR>hA : A ≠ 0<VAR>this : ∃ t, t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ (↑n * max 1 ‖A‖) ^ e<GOAL>1 ≤ ‖A‖
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : NonPreadditiveAbelian C<VAR>X Y : C<VAR>a b : X ⟶ Y<GOAL>-a - b = -b - a
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>s✝ t✝ : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<GOAL>(s ∩ t).dens + (s ∪ t).dens = s.dens + t.dens
<VAR>q : ℚ<VAR>n₁ d₁ n₂ d₂ : ℤ<GOAL>n₁ /. d₁ / (n₂ /. d₂) = n₁ * d₂ /. (d₁ * n₂)
<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : ArithmeticFunction R<VAR>x : ℕ<GOAL>(f.pmul ↑ζ) x = f x
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>s✝ : Set α<VAR>inst✝ : ConditionallyCompleteLinearOrder α<VAR>s : Set α<VAR>hs : s.OrdConnected<VAR>t : Set ↑s<VAR>c : ↑s<VAR>hct : c ∈ t<VAR>B : ↑s<VAR>hB : B ∈ upperBounds t<GOAL>sSup (Subtype.val '' t) ∈ s
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>s✝ : Set α<VAR>inst✝ : ConditionallyCompleteLinearOrder α<VAR>s : Set α<VAR>hs : s.OrdConnected<VAR>t : Set ↑s<VAR>c : ↑s<VAR>hct : c ∈ t<VAR>B : ↑s<VAR>hB : B ∈ upperBounds t<GOAL>↑c ≤ sSup (Subtype.val '' t)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>s✝ : Set α<VAR>inst✝ : ConditionallyCompleteLinearOrder α<VAR>s : Set α<VAR>hs : s.OrdConnected<VAR>t : Set ↑s<VAR>c : ↑s<VAR>hct : c ∈ t<VAR>B : ↑s<VAR>hB : B ∈ upperBounds t<GOAL>sSup (Subtype.val '' t) ≤ ↑B
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>inst✝² : Finite F<VAR>R : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>χ : MulChar F R<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hχ : χ ^ n = 1<VAR>μ : R<VAR>hμ : IsPrimitiveRoot μ n<VAR>a : F<VAR>ha : a ≠ 0<GOAL>∃ k < n, χ a = μ ^ k
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>inst✝² : Finite F<VAR>R : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>χ : MulChar F R<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hχ : χ ^ n = 1<VAR>μ : R<VAR>hμ : IsPrimitiveRoot μ n<VAR>a : F<VAR>ha : a ≠ 0<VAR>hn' : 0 < n<GOAL>∃ k < n, χ a = μ ^ k
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>inst✝² : Finite F<VAR>R : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>χ : MulChar F R<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hχ : χ ^ n = 1<VAR>μ : R<VAR>hμ : IsPrimitiveRoot μ n<VAR>a : F<VAR>ha : a ≠ 0<VAR>hn' : 0 < n<VAR>ζ : Rˣ<VAR>hζ₁ : ζ ∈ rootsOfUnity ⟨n, ⋯⟩ R<VAR>hζ₂ : ↑ζ = χ a<GOAL>∃ k < n, χ a = μ ^ k
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>inst✝² : Finite F<VAR>R : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>χ : MulChar F R<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hχ : χ ^ n = 1<VAR>μ : R<VAR>hμ : IsPrimitiveRoot μ n<VAR>a : F<VAR>ha : a ≠ 0<VAR>hn' : 0 < n<VAR>ζ : Rˣ<VAR>hζ₁ : ζ ∈ rootsOfUnity ⟨n, ⋯⟩ R<VAR>hζ₂ : ↑ζ = χ a<VAR>hζ' : ↑ζ ^ n = 1<GOAL>∃ k < n, χ a = μ ^ k
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>inst✝² : Finite F<VAR>R : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>χ : MulChar F R<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hχ : χ ^ n = 1<VAR>μ : R<VAR>hμ : IsPrimitiveRoot μ n<VAR>a : F<VAR>ha : a ≠ 0<VAR>hn' : 0 < n<VAR>ζ : Rˣ<VAR>hζ₁ : ζ ∈ rootsOfUnity ⟨n, ⋯⟩ R<VAR>hζ₂ : ↑ζ = χ a<VAR>hζ' : ↑ζ ^ n = 1<VAR>k : ℕ<VAR>hk₁ : k < n<VAR>hk₂ : μ ^ k = ↑ζ<GOAL>∃ k < n, χ a = μ ^ k
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 < x<VAR>hy : 0 < y<VAR>hz : z < 0<GOAL>x ^ z⁻¹ < y ↔ y ^ z < x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>l l' : List α<VAR>a : α<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>x : α<GOAL>x ∈ (replicate n a).toFinset ↔ x ∈ {a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>C : Ordinal.{u_4} → Sort u_5<VAR>o : Ordinal.{u_4}<VAR>H₁ : C 0<VAR>H₂ : (o : Ordinal.{u_4}) → C o → C (succ o)<VAR>H₃ : (o : Ordinal.{u_4}) → o.IsLimit → ((o' : Ordinal.{u_4}) → o' < o → C o') → C o<GOAL>(succ o).limitRecOn H₁ H₂ H₃ = H₂ o (o.limitRecOn H₁ H₂ H₃)
<VAR>a : ℤ<GOAL>χ₈' ↑a = χ₄ ↑a * χ₈ ↑a
<VAR>a : ℤ<GOAL>χ₈' ↑a = χ₄ (↑a).cast * χ₈ ↑a
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' G'' : G.Subgraph<VAR>s s' : Set V<VAR>v : V<GOAL>G.singletonSubgraph v = ⊤.induce {v}
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>s : Set α<GOAL>IsComplete (range Subtype.val) ↔ IsComplete s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>x y z : X<VAR>ι✝ : Type u_3<VAR>γ✝ : Path x y<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace ι<VAR>a b : ι → X<VAR>γ : (t : ι) → Path (a t) (b t)<VAR>h : Continuous ↿γ<GOAL>Continuous ↿fun t => (γ t).extend
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>x y z : X<VAR>ι✝ : Type u_3<VAR>γ✝ : Path x y<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace ι<VAR>a b : ι → X<VAR>γ : (t : ι) → Path (a t) (b t)<VAR>h : Continuous ↿γ<GOAL>0 ≤ 1
<VAR>K : Type u_1<VAR>S : Type u_2<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : Algebra K S<VAR>R : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Algebra R K<VAR>inst✝⁵ : IsScalarTower R K S<VAR>A : Type u_4<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : IsScalarTower R S A<VAR>B : PowerBasis S A<VAR>hB : IsIntegral R B.gen<VAR>inst✝ : IsDomain S<VAR>x y : A<VAR>hx : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)<VAR>hy : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr y) i)<VAR>hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)<VAR>i : Fin B.dim<GOAL>IsIntegral R ((B.basis.repr (x * y)) i)
<VAR>K : Type u_1<VAR>S : Type u_2<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : Algebra K S<VAR>R : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Algebra R K<VAR>inst✝⁵ : IsScalarTower R K S<VAR>A : Type u_4<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : IsScalarTower R S A<VAR>B : PowerBasis S A<VAR>hB : IsIntegral R B.gen<VAR>inst✝ : IsDomain S<VAR>x y : A<VAR>hx : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)<VAR>hy : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr y) i)<VAR>hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)<VAR>i : Fin B.dim<GOAL>IsIntegral R (∑ k ∈ Finset.univ ×ˢ Finset.univ, (B.basis.repr ((B.basis.repr x) k.1 • B.basis k.1 * (B.basis.repr y) k.2 • B.basis k.2)) i)
<VAR>K : Type u_1<VAR>S : Type u_2<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : Algebra K S<VAR>R : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Algebra R K<VAR>inst✝⁵ : IsScalarTower R K S<VAR>A : Type u_4<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : IsScalarTower R S A<VAR>B : PowerBasis S A<VAR>hB : IsIntegral R B.gen<VAR>inst✝ : IsDomain S<VAR>x y : A<VAR>hx : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)<VAR>hy : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr y) i)<VAR>hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)<VAR>i : Fin B.dim<VAR>I : Fin B.dim × Fin B.dim<VAR>x✝ : I ∈ Finset.univ ×ˢ Finset.univ<GOAL>IsIntegral R ((B.basis.repr ((B.basis.repr x) I.1 • B.basis I.1 * (B.basis.repr y) I.2 • B.basis I.2)) i)
<VAR>K : Type u_1<VAR>S : Type u_2<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : Algebra K S<VAR>R : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Algebra R K<VAR>inst✝⁵ : IsScalarTower R K S<VAR>A : Type u_4<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : IsScalarTower R S A<VAR>B : PowerBasis S A<VAR>hB : IsIntegral R B.gen<VAR>inst✝ : IsDomain S<VAR>x y : A<VAR>hx : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)<VAR>hy : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr y) i)<VAR>hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)<VAR>i : Fin B.dim<VAR>I : Fin B.dim × Fin B.dim<VAR>x✝ : I ∈ Finset.univ ×ˢ Finset.univ<GOAL>IsIntegral R ((B.basis.repr y) I.2 * ((B.basis.repr x) I.1 * (B.basis.repr (B.basis I.1 * B.basis I.2)) i))
<VAR>K : Type u_1<VAR>S : Type u_2<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : Algebra K S<VAR>R : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Algebra R K<VAR>inst✝⁵ : IsScalarTower R K S<VAR>A : Type u_4<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : IsScalarTower R S A<VAR>B : PowerBasis S A<VAR>hB : IsIntegral R B.gen<VAR>inst✝ : IsDomain S<VAR>x y : A<VAR>hx : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)<VAR>hy : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr y) i)<VAR>hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)<VAR>i : Fin B.dim<VAR>I : Fin B.dim × Fin B.dim<VAR>x✝ : I ∈ Finset.univ ×ˢ Finset.univ<GOAL>IsIntegral R ((B.basis.repr (B.basis I.1 * B.basis I.2)) i)
<VAR>K : Type u_1<VAR>S : Type u_2<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : Algebra K S<VAR>R : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Algebra R K<VAR>inst✝⁵ : IsScalarTower R K S<VAR>A : Type u_4<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : IsScalarTower R S A<VAR>B : PowerBasis S A<VAR>hB : IsIntegral R B.gen<VAR>inst✝ : IsDomain S<VAR>x y : A<VAR>hx : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)<VAR>hy : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr y) i)<VAR>hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)<VAR>i : Fin B.dim<VAR>I : Fin B.dim × Fin B.dim<VAR>x✝ : I ∈ Finset.univ ×ˢ Finset.univ<GOAL>IsIntegral R ((B.basis.repr (B.gen ^ (↑I.1 + ↑I.2))) i)
<VAR>z : ℂ<VAR>this : 0 ≤ abs z<VAR>x✝ : 0 ≤ z<VAR>h₁ : re 0 ≤ z.re<VAR>h₂ : im 0 = z.im<GOAL>z.re = abs z
<VAR>o : ONote<VAR>b₁ b₂ : Ordinal.{0}<VAR>e : ONote<VAR>n : ℕ+<VAR>a : ONote<VAR>eb b : Ordinal.{0}<VAR>h₁ : e.NFBelow eb<VAR>h₂ : a.NFBelow e.repr<VAR>h₃ : e.repr < b<VAR>a_ih✝¹ : eb ≤ b₂ → e.NFBelow b₂<VAR>a_ih✝ : e.repr ≤ b₂ → a.NFBelow b₂<VAR>bb : b ≤ b₂<GOAL>e.NFBelow ?oadd'.eb
<VAR>o : ONote<VAR>b₁ b₂ : Ordinal.{0}<VAR>e : ONote<VAR>n : ℕ+<VAR>a : ONote<VAR>eb b : Ordinal.{0}<VAR>h₁ : e.NFBelow eb<VAR>h₂ : a.NFBelow e.repr<VAR>h₃ : e.repr < b<VAR>a_ih✝¹ : eb ≤ b₂ → e.NFBelow b₂<VAR>a_ih✝ : e.repr ≤ b₂ → a.NFBelow b₂<VAR>bb : b ≤ b₂<GOAL>a.NFBelow e.repr
<VAR>o : ONote<VAR>b₁ b₂ : Ordinal.{0}<VAR>e : ONote<VAR>n : ℕ+<VAR>a : ONote<VAR>eb b : Ordinal.{0}<VAR>h₁ : e.NFBelow eb<VAR>h₂ : a.NFBelow e.repr<VAR>h₃ : e.repr < b<VAR>a_ih✝¹ : eb ≤ b₂ → e.NFBelow b₂<VAR>a_ih✝ : e.repr ≤ b₂ → a.NFBelow b₂<VAR>bb : b ≤ b₂<GOAL>e.repr < b₂
<VAR>o : ONote<VAR>b₁ b₂ : Ordinal.{0}<VAR>e : ONote<VAR>n : ℕ+<VAR>a : ONote<VAR>eb b : Ordinal.{0}<VAR>h₁ : e.NFBelow eb<VAR>h₂ : a.NFBelow e.repr<VAR>h₃ : e.repr < b<VAR>a_ih✝¹ : eb ≤ b₂ → e.NFBelow b₂<VAR>a_ih✝ : e.repr ≤ b₂ → a.NFBelow b₂<VAR>bb : b ≤ b₂<GOAL>Ordinal.{0}
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s t : Set α<VAR>a b x y : α<VAR>hf : f.IsCycleOn s<GOAL>(f.subtypePerm ⋯).IsCycleOn _root_.Set.univ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s t : Set α<VAR>a b x y : α<VAR>hf : f.IsCycleOn s<VAR>hs : s.Subsingleton<GOAL>(f.subtypePerm ⋯).IsCycleOn _root_.Set.univ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s t : Set α<VAR>a b x y : α<VAR>hf : f.IsCycleOn s<VAR>hs : s.Nontrivial<GOAL>(f.subtypePerm ⋯).IsCycleOn _root_.Set.univ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s t : Set α<VAR>a b x y : α<VAR>hf : f.IsCycleOn s<VAR>hs : s.Nontrivial<GOAL>_root_.Set.univ = {x | (f.subtypePerm ⋯) x ≠ x}
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s t : Set α<VAR>a b x y : α<VAR>hf : f.IsCycleOn s<VAR>hs : s.Nontrivial<GOAL>∀ (x : { x // x ∈ s }), x ∈ {x | (f.subtypePerm ⋯) x ≠ x}
<VAR>x : ℝ<GOAL>Real.toEReal '' Ioi x = Ioo ↑x ⊤
<VAR>x : ℝ<GOAL>WithBot.some '' (WithTop.some '' Ioi x) = Ioo ↑x ⊤
<VAR>x : ℝ<GOAL>Ioo ↑↑x ↑⊤ = Ioo ↑x ⊤
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup L<VAR>inst✝⁹ : Module R L<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : Fintype ι'<VAR>inst✝⁴ : Fintype ιM<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : DecidableEq ι'<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>b✝ b : Basis ι R L<VAR>b' : Basis ι' R L<VAR>k : ℕ<VAR>H : (φ.polyCharpoly b).coeff k = 0<GOAL>(φ.polyCharpoly b').coeff k = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup L<VAR>inst✝⁹ : Module R L<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : Fintype ι'<VAR>inst✝⁴ : Fintype ιM<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : DecidableEq ι'<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>b✝ b : Basis ι R L<VAR>b' : Basis ι' R L<VAR>k : ℕ<VAR>H : ↑(MvPolynomial.bind₁ (toMvPolynomial b (Module.Free.chooseBasis R M).end φ)) ((charpoly.univ R (Module.Free.ChooseBasisIndex R M)).coeff k) = 0<GOAL>↑(MvPolynomial.bind₁ (toMvPolynomial b' (Module.Free.chooseBasis R M).end φ)) ((charpoly.univ R (Module.Free.ChooseBasisIndex R M)).coeff k) = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup L<VAR>inst✝⁹ : Module R L<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : Fintype ι'<VAR>inst✝⁴ : Fintype ιM<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : DecidableEq ι'<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>b✝ b : Basis ι R L<VAR>b' : Basis ι' R L<VAR>k : ℕ<VAR>B : Basis (Module.Free.ChooseBasisIndex R M × Module.Free.ChooseBasisIndex R M) R (Module.End R M) := (Module.Free.chooseBasis R M).end<VAR>g : ι → MvPolynomial ι' R := toMvPolynomial b' b id<VAR>H : (MvPolynomial.bind₁ g) (↑(MvPolynomial.bind₁ (toMvPolynomial b B φ)) ((charpoly.univ R (Module.Free.ChooseBasisIndex R M)).coeff k)) = (MvPolynomial.bind₁ g) 0<GOAL>↑(MvPolynomial.bind₁ (toMvPolynomial b' B φ)) ((charpoly.univ R (Module.Free.ChooseBasisIndex R M)).coeff k) = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup L<VAR>inst✝⁹ : Module R L<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : Fintype ι'<VAR>inst✝⁴ : Fintype ιM<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : DecidableEq ι'<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>b✝ b : Basis ι R L<VAR>b' : Basis ι' R L<VAR>k : ℕ<VAR>B : Basis (Module.Free.ChooseBasisIndex R M × Module.Free.ChooseBasisIndex R M) R (Module.End R M) := (Module.Free.chooseBasis R M).end<VAR>g : ι → MvPolynomial ι' R := toMvPolynomial b' b id<VAR>H : (MvPolynomial.bind₁ g) (↑(MvPolynomial.bind₁ (toMvPolynomial b B φ)) ((charpoly.univ R (Module.Free.ChooseBasisIndex R M)).coeff k)) = (MvPolynomial.bind₁ g) 0<VAR>this : toMvPolynomial b' B φ = fun i => (MvPolynomial.bind₁ g) (toMvPolynomial b B φ i)<GOAL>↑(MvPolynomial.bind₁ (toMvPolynomial b' B φ)) ((charpoly.univ R (Module.Free.ChooseBasisIndex R M)).coeff k) = 0
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>n : ℕ<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r<GOAL>HasFiniteFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x n r
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>n : ℕ<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r<GOAL>HasFiniteFPowerSeriesOnBall (fun z => (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin (z - x) 1)) p.derivSeries x n r
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>n : ℕ<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r<VAR>z : E<VAR>hz : z ∈ EMetric.ball x r<GOAL>(fun z => (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin (z - x) 1)) z = fderiv 𝕜 f z
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>n : ℕ<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r<VAR>z : E<VAR>hz : z ∈ EMetric.ball x r<GOAL>(continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin (z - x) 1) = fderiv 𝕜 f z
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>n : ℕ<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r<VAR>z : E<VAR>hz : z ∈ EMetric.ball x r<GOAL>↑‖z - x‖₊ < r
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>s : Sphere P<VAR>p₁ p₂ p₃ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₃ : p₃ ∈ s<VAR>hp₂p₁ : p₂ ≠ p₁<VAR>hp₂p₃ : p₂ ≠ p₃<VAR>hp₁p₃ : p₁ ≠ p₃<GOAL>2 • ∡ p₃ p₁ s.center + 2 • ∡ p₁ p₂ p₃ = ↑π
<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>inst✝¹ : DivisionSemiring S<VAR>inst✝ : Module S M<VAR>x✝³ : α → α<VAR>x✝² : α → M<VAR>x✝¹ : ℕ<VAR>x✝ : α<GOAL>birkhoffAverage R x✝³ x✝² x✝¹ x✝ = birkhoffAverage S x✝³ x✝² x✝¹ x✝
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>A : Type u_2<VAR>inst✝² : NormedField A<VAR>inst✝¹ : IsAlgClosed A<VAR>inst✝ : NormedAlgebra ℚ A<VAR>B : ℝ<VAR>C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑((finrank ℚ K).choose (finrank ℚ K / 2))⌉₊<GOAL>{x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖φ x‖ ≤ B}.Finite
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>A : Type u_2<VAR>inst✝² : NormedField A<VAR>inst✝¹ : IsAlgClosed A<VAR>inst✝ : NormedAlgebra ℚ A<VAR>B : ℝ<VAR>C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑((finrank ℚ K).choose (finrank ℚ K / 2))⌉₊<VAR>this : (⋃ f, ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), f.coeff i ∈ Icc (-↑C) ↑C), ↑(map (algebraMap ℤ K) f).roots.toFinset).Finite<GOAL>{x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖φ x‖ ≤ B}.Finite
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>A : Type u_2<VAR>inst✝² : NormedField A<VAR>inst✝¹ : IsAlgClosed A<VAR>inst✝ : NormedAlgebra ℚ A<VAR>B : ℝ<VAR>C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑((finrank ℚ K).choose (finrank ℚ K / 2))⌉₊<VAR>this : (⋃ f, ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), f.coeff i ∈ Icc (-↑C) ↑C), ↑(map (algebraMap ℤ K) f).roots.toFinset).Finite<VAR>x : K<VAR>hx : x ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖φ x‖ ≤ B}<GOAL>x ∈ ⋃ f, ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), f.coeff i ∈ Icc (-↑C) ↑C), ↑(map (algebraMap ℤ K) f).roots.toFinset
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>A : Type u_2<VAR>inst✝² : NormedField A<VAR>inst✝¹ : IsAlgClosed A<VAR>inst✝ : NormedAlgebra ℚ A<VAR>B : ℝ<VAR>C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑((finrank ℚ K).choose (finrank ℚ K / 2))⌉₊<VAR>this : (⋃ f, ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), f.coeff i ∈ Icc (-↑C) ↑C), ↑(map (algebraMap ℤ K) f).roots.toFinset).Finite<VAR>x : K<VAR>hx : x ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖φ x‖ ≤ B}<GOAL>∃ i, ∃ (_ : i.natDegree ≤ finrank ℚ K ∧ ∀ (i_1 : ℕ), i.coeff i_1 ∈ Icc (-↑C) ↑C), x ∈ ↑(map (algebraMap ℤ K) i).roots.toFinset
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>A : Type u_2<VAR>inst✝² : NormedField A<VAR>inst✝¹ : IsAlgClosed A<VAR>inst✝ : NormedAlgebra ℚ A<VAR>B : ℝ<VAR>C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑((finrank ℚ K).choose (finrank ℚ K / 2))⌉₊<VAR>this : (⋃ f, ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), f.coeff i ∈ Icc (-↑C) ↑C), ↑(map (algebraMap ℤ K) f).roots.toFinset).Finite<VAR>x : K<VAR>hx : x ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖φ x‖ ≤ B}<VAR>h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)<GOAL>∃ i, ∃ (_ : i.natDegree ≤ finrank ℚ K ∧ ∀ (i_1 : ℕ), i.coeff i_1 ∈ Icc (-↑C) ↑C), x ∈ ↑(map (algebraMap ℤ K) i).roots.toFinset
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>A : Type u_2<VAR>inst✝² : NormedField A<VAR>inst✝¹ : IsAlgClosed A<VAR>inst✝ : NormedAlgebra ℚ A<VAR>B : ℝ<VAR>C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑((finrank ℚ K).choose (finrank ℚ K / 2))⌉₊<VAR>this : (⋃ f, ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), f.coeff i ∈ Icc (-↑C) ↑C), ↑(map (algebraMap ℤ K) f).roots.toFinset).Finite<VAR>x : K<VAR>hx : x ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖φ x‖ ≤ B}<VAR>h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)<GOAL>(minpoly ℤ x).natDegree ≤ finrank ℚ K
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>A : Type u_2<VAR>inst✝² : NormedField A<VAR>inst✝¹ : IsAlgClosed A<VAR>inst✝ : NormedAlgebra ℚ A<VAR>B : ℝ<VAR>C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑((finrank ℚ K).choose (finrank ℚ K / 2))⌉₊<VAR>this : (⋃ f, ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), f.coeff i ∈ Icc (-↑C) ↑C), ↑(map (algebraMap ℤ K) f).roots.toFinset).Finite<VAR>x : K<VAR>hx : x ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖φ x‖ ≤ B}<VAR>h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)<VAR>i : ℕ<GOAL>(minpoly ℤ x).coeff i ∈ Icc (-↑C) ↑C