ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>T a b : ℝ<VAR>hab : a < b<VAR>f f' : ℝ → ℂ<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>hf : ContinuousOn f [[a, b]]<VAR>hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x<VAR>hf' : IntervalIntegrable f' volume a b<VAR>hT : Fact (0 < b - a)<GOAL>1 / ↑(b - a) * ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x * f x = 1 / (-2 * ↑π * I * ↑n) * ((fourier (-n)) ↑a * (f b - f a) - ↑(b - a) * (1 / ↑(b - a) * ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x * f' x))
<VAR>T a b : ℝ<VAR>hab : a < b<VAR>f f' : ℝ → ℂ<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>hf : ContinuousOn f [[a, b]]<VAR>hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x<VAR>hf' : IntervalIntegrable f' volume a b<VAR>hT : Fact (0 < b - a)<GOAL>1 / ↑(b - a) * ∫ (x : ℝ) in a..b, f x * (fourier (-n)) ↑x = 1 / (-2 * ↑π * I * ↑n) * ((f b - f a) * (fourier (-n)) ↑a - ↑(b - a) * (1 / ↑(b - a) * ∫ (x : ℝ) in a..b, f' x * (fourier (-n)) ↑x))
<VAR>T a b : ℝ<VAR>hab : a < b<VAR>f f' : ℝ → ℂ<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>hf : ContinuousOn f [[a, b]]<VAR>hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x<VAR>hf' : IntervalIntegrable f' volume a b<VAR>hT : Fact (0 < b - a)<GOAL>1 / ↑(b - a) * (f b * (↑(b - a) / (-2 * ↑π * I * ↑n) * (fourier (-n)) ↑b) - f a * (↑(b - a) / (-2 * ↑π * I * ↑n) * (fourier (-n)) ↑a) - ∫ (x : ℝ) in a..b, f' x * (↑(b - a) / (-2 * ↑π * I * ↑n) * (fourier (-n)) ↑x)) = 1 / (-2 * ↑π * I * ↑n) * ((f b - f a) * (fourier (-n)) ↑a - ↑(b - a) * (1 / ↑(b - a) * ∫ (x : ℝ) in a..b, f' x * (fourier (-n)) ↑x))
<VAR>T a b : ℝ<VAR>hab : a < b<VAR>f f' : ℝ → ℂ<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>hf : ContinuousOn f [[a, b]]<VAR>hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x<VAR>hf' : IntervalIntegrable f' volume a b<VAR>hT : Fact (0 < b - a)<VAR>this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)<GOAL>1 / ↑(b - a) * (f b * (↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * (fourier (-n)) ↑b) - f a * (↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * (fourier (-n)) ↑a) - ∫ (x : ℝ) in a..b, ↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * (f' x * (fourier (-n)) ↑x)) = 1 / (-2 * ↑π * I * ↑n) * ((f b - f a) * (fourier (-n)) ↑a - ↑(b - a) * (1 / ↑(b - a) * ∫ (x : ℝ) in a..b, f' x * (fourier (-n)) ↑x))
<VAR>T a b : ℝ<VAR>hab : a < b<VAR>f f' : ℝ → ℂ<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>hf : ContinuousOn f [[a, b]]<VAR>hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x<VAR>hf' : IntervalIntegrable f' volume a b<VAR>hT : Fact (0 < b - a)<VAR>this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)<VAR>s2 : ↑b = ↑a<GOAL>1 / ↑(b - a) * (f b * (↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * (fourier (-n)) ↑b) - f a * (↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * (fourier (-n)) ↑a) - ∫ (x : ℝ) in a..b, ↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * (f' x * (fourier (-n)) ↑x)) = 1 / (-2 * ↑π * I * ↑n) * ((f b - f a) * (fourier (-n)) ↑a - ↑(b - a) * (1 / ↑(b - a) * ∫ (x : ℝ) in a..b, f' x * (fourier (-n)) ↑x))
<VAR>T a b : ℝ<VAR>hab : a < b<VAR>f f' : ℝ → ℂ<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>hf : ContinuousOn f [[a, b]]<VAR>hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x<VAR>hf' : IntervalIntegrable f' volume a b<VAR>hT : Fact (0 < b - a)<VAR>this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)<VAR>s2 : ↑b = ↑a<GOAL>1 / ↑(b - a) * ((f b - f a) * (↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * (fourier (-n)) ↑a)) - 1 / ↑(b - a) * (↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * ∫ (x : ℝ) in a..b, f' x * (fourier (-n)) ↑x) = 1 / (-2 * ↑π * I * ↑n) * ((f b - f a) * (fourier (-n)) ↑a) - 1 / (-2 * ↑π * I * ↑n) * (↑(b - a) * (1 / ↑(b - a) * ∫ (x : ℝ) in a..b, f' x * (fourier (-n)) ↑x))
<VAR>s : Finset ℕ<VAR>m k : ℕ<VAR>h' : k ∣ m<VAR>h₁ : m ≠ 0<VAR>h₂ : ∀ p ∈ m.primeFactorsList, p ∈ s<GOAL>k ∈ factoredNumbers s
<VAR>s : Finset ℕ<VAR>m k : ℕ<VAR>h' : k ∣ m<VAR>h₁ : m ≠ 0<VAR>h₂ : ∀ p ∈ m.primeFactorsList, p ∈ s<VAR>hk : k ≠ 0<GOAL>k ∈ factoredNumbers s
<VAR>s : Finset ℕ<VAR>m k : ℕ<VAR>h' : k ∣ m<VAR>h₁ : m ≠ 0<VAR>h₂ : ∀ p ∈ m.primeFactorsList, p ∈ s<VAR>hk : k ≠ 0<VAR>p : ℕ<VAR>hp : p ∈ k.primeFactorsList<GOAL>p ∈ m.primeFactorsList
<VAR>s : Finset ℕ<VAR>m k : ℕ<VAR>h' : k ∣ m<VAR>h₁ : m ≠ 0<VAR>h₂ : ∀ p ∈ m.primeFactorsList, p ∈ s<VAR>hk : k ≠ 0<VAR>p : ℕ<VAR>hp : Prime p ∧ p ∣ k<GOAL>Prime p ∧ p ∣ m
<VAR>l r : List Char<GOAL>{ data := l ++ r }.offsetOfPos { byteIdx := utf8Len l } = l.length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : ProperSpace α<VAR>x : α<VAR>r : ℝ<VAR>s : Set α<VAR>hs : IsClosed s<VAR>h : s ⊆ ball x r<GOAL>∃ r' < r, s ⊆ ball x r'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : ProperSpace α<VAR>x : α<VAR>r : ℝ<VAR>s : Set α<VAR>hs : IsClosed s<VAR>h : s ⊆ ball x r<VAR>hr : r ≤ 0<GOAL>∃ r' < r, s ⊆ ball x r'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : ProperSpace α<VAR>x : α<VAR>r : ℝ<VAR>s : Set α<VAR>hs : IsClosed s<VAR>h : s ⊆ ball x r<VAR>hr : 0 < r<GOAL>∃ r' < r, s ⊆ ball x r'
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>κ : Type u_1<VAR>α : ι → Type u_2<VAR>δ : (i : ι) → α i → Type v<VAR>inst✝² : (i : ι) → (j : α i) → Zero (δ i j)<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (α i)<VAR>i : ι<VAR>j : α i<VAR>x : δ i j<VAR>i' : ι<VAR>j' : α i'<GOAL>(single i (single j x)).sigmaUncurry ⟨i', j'⟩ = (single ⟨i, j⟩ x) ⟨i', j'⟩
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>κ : Type u_1<VAR>α : ι → Type u_2<VAR>δ : (i : ι) → α i → Type v<VAR>inst✝² : (i : ι) → (j : α i) → Zero (δ i j)<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (α i)<VAR>i : ι<VAR>j : α i<VAR>x : δ i j<VAR>i' : ι<VAR>j' : α i'<GOAL>((single i (single j x)) i') j' = (single ⟨i, j⟩ x) ⟨i', j'⟩
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>κ : Type u_1<VAR>α : ι → Type u_2<VAR>δ : (i : ι) → α i → Type v<VAR>inst✝² : (i : ι) → (j : α i) → Zero (δ i j)<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (α i)<VAR>i : ι<VAR>j : α i<VAR>x : δ i j<VAR>j' : α i<GOAL>((single i (single j x)) i) j' = (single ⟨i, j⟩ x) ⟨i, j'⟩
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>κ : Type u_1<VAR>α : ι → Type u_2<VAR>δ : (i : ι) → α i → Type v<VAR>inst✝² : (i : ι) → (j : α i) → Zero (δ i j)<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (α i)<VAR>i : ι<VAR>j : α i<VAR>x : δ i j<VAR>i' : ι<VAR>j' : α i'<VAR>hi : i ≠ i'<GOAL>((single i (single j x)) i') j' = (single ⟨i, j⟩ x) ⟨i', j'⟩
<VAR>d : ℤ<VAR>h₀ : 0 < d<VAR>hd : ¬IsSquare d<GOAL>∃ a, 1 < a.x ∧ 0 < a.y
<VAR>d : ℤ<VAR>h₀ : 0 < d<VAR>hd : ¬IsSquare d<VAR>x y : ℤ<VAR>h : x ^ 2 - d * y ^ 2 = 1<VAR>hy : y ≠ 0<GOAL>∃ a, 1 < a.x ∧ 0 < a.y
<VAR>d : ℤ<VAR>h₀ : 0 < d<VAR>hd : ¬IsSquare d<VAR>x y : ℤ<VAR>h : x ^ 2 - d * y ^ 2 = 1<VAR>hy : y ≠ 0<GOAL>1 < (mk |x| |y| ⋯).x
<VAR>d : ℤ<VAR>h₀ : 0 < d<VAR>hd : ¬IsSquare d<VAR>x y : ℤ<VAR>h : x ^ 2 - d * y ^ 2 = 1<VAR>hy : y ≠ 0<GOAL>0 < d * y ^ 2
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>X : SimplicialObject C<VAR>s : Splitting X<VAR>inst✝ : Preadditive C<VAR>n : ℕ<GOAL>PInfty.f n ≫ s.πSummand (IndexSet.id (op [n])) = s.πSummand (IndexSet.id (op [n]))
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>X : SimplicialObject C<VAR>s : Splitting X<VAR>inst✝ : Preadditive C<VAR>n : ℕ<GOAL>PInfty.f n ≫ s.πSummand (IndexSet.id (op [n])) = 𝟙 (X _[n]) ≫ s.πSummand (IndexSet.id (op [n]))
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>X : SimplicialObject C<VAR>s : Splitting X<VAR>inst✝ : Preadditive C<VAR>n : ℕ<GOAL>𝟙 (X _[n]) ≫ s.πSummand (IndexSet.id (op [n])) = PInfty.f n ≫ s.πSummand (IndexSet.id (op [n]))
<VAR>R : Type u_1<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Finite R<VAR>inst✝ : CharP R 0<GOAL>False
<VAR>R : Type u_1<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Finite R<VAR>inst✝ : CharP R 0<VAR>this : CharZero R<GOAL>False
<VAR>R : Type u_1<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Finite R<VAR>inst✝ : CharP R 0<VAR>this : CharZero R<VAR>val✝ : Fintype R<GOAL>False
<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>inst✝¹² : SmoothManifoldWithCorners I 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>inst✝⁶ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝³ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝² : TopologicalSpace M''<VAR>inst✝¹ : ChartedSpace H'' M''<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>c : M'<VAR>inst✝ : One M'<GOAL>ContMDiff I I' n 1
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : CharP R 2<VAR>x : R<GOAL>-x = x
<VAR>a b c : Ordinal.{u}<GOAL>succ a ♯ b = succ (a ♯ b)
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>f : α → β → γ<VAR>p : γ → Prop<VAR>a : α<VAR>l₁ : List α<VAR>b : β<VAR>l₂ : List β<VAR>h : (a :: l₁).length = (b :: l₂).length<GOAL>Forall p (zipWith f (a :: l₁) (b :: l₂)) ↔ Forall₂ (fun x y => p (f x y)) (a :: l₁) (b :: l₂)
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>f : α → β → γ<VAR>p : γ → Prop<VAR>a : α<VAR>l₁ : List α<VAR>b : β<VAR>l₂ : List β<VAR>h : l₁.length = l₂.length<GOAL>Forall p (zipWith f (a :: l₁) (b :: l₂)) ↔ Forall₂ (fun x y => p (f x y)) (a :: l₁) (b :: l₂)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>f✝ : α → β<VAR>f : α → α<VAR>hf : LocallyLipschitz f<GOAL>LocallyLipschitz f^[0]
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>f✝ : α → β<VAR>f : α → α<VAR>hf : LocallyLipschitz f<VAR>n : ℕ<GOAL>LocallyLipschitz f^[n + 1]
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>f✝ : α → β<VAR>f : α → α<VAR>hf : LocallyLipschitz f<VAR>n : ℕ<GOAL>LocallyLipschitz (f^[n] ∘ f)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>h : HomologyMapData φ h₁ h₂<GOAL>h.left.φH ≫ h₂.iso.hom = h₁.iso.hom ≫ h.right.φH
<VAR>J : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>F✝ : J ⥤ C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>F : J ⥤ C<VAR>inst✝¹ : HasLimit F<VAR>G : C ⥤ D<VAR>inst✝ : HasLimit (F ⋙ G)<VAR>j : J<GOAL>post F G ≫ π (F ⋙ G) j = G.map (π F j)
<VAR>J : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>F✝ : J ⥤ C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>F : J ⥤ C<VAR>inst✝¹ : HasLimit F<VAR>G : C ⥤ D<VAR>inst✝ : HasLimit (F ⋙ G)<VAR>j : J<GOAL>(G.mapCone (cone F)).π.app j = G.map (π F j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x : α<VAR>l : List α<VAR>h : l.Nodup<VAR>hl : 1 < l.length<GOAL>l.formPerm (l.nthLe 0 ⋯) = l.nthLe 1 hl
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>m : ι → OuterMeasure α<VAR>s : Set α<VAR>h : MeasurableSet s<VAR>t : Set α<GOAL>(sum m) t = (sum m) (t ∩ s) + (sum m) (t \ s)
<VAR>p q : ℚ<GOAL>q.toNNRat = 0 ↔ q ≤ 0
<VAR>R✝ : Type u_1<VAR>inst✝⁴ : Semiring R✝<VAR>p q : R✝[X]<VAR>S : Type u_2<VAR>inst✝³ : AddCommMonoid S<VAR>inst✝² : Pow S ℕ<VAR>inst✝¹ : Module R✝ S<VAR>x : S<VAR>R : Type u_3<VAR>inst✝ : Semiring R<VAR>r : R<GOAL>⇑(leval r) = fun p => p.smeval r
<VAR>R✝ : Type u_1<VAR>inst✝⁴ : Semiring R✝<VAR>p q : R✝[X]<VAR>S : Type u_2<VAR>inst✝³ : AddCommMonoid S<VAR>inst✝² : Pow S ℕ<VAR>inst✝¹ : Module R✝ S<VAR>x : S<VAR>R : Type u_3<VAR>inst✝ : Semiring R<VAR>r : R<GOAL>∀ (a : R[X]), (leval r) a = a.smeval r
<VAR>R✝ : Type u_1<VAR>inst✝⁴ : Semiring R✝<VAR>p q : R✝[X]<VAR>S : Type u_2<VAR>inst✝³ : AddCommMonoid S<VAR>inst✝² : Pow S ℕ<VAR>inst✝¹ : Module R✝ S<VAR>x : S<VAR>R : Type u_3<VAR>inst✝ : Semiring R<VAR>r : R<VAR>a✝ : R[X]<GOAL>(leval r) a✝ = a✝.smeval r
<VAR>R✝ : Type u_1<VAR>inst✝⁴ : Semiring R✝<VAR>p q : R✝[X]<VAR>S : Type u_2<VAR>inst✝³ : AddCommMonoid S<VAR>inst✝² : Pow S ℕ<VAR>inst✝¹ : Module R✝ S<VAR>x : S<VAR>R : Type u_3<VAR>inst✝ : Semiring R<VAR>r : R<VAR>a✝ : R[X]<GOAL>(a✝.sum fun e a => a * r ^ e) = a✝.sum (smul_pow r)
<VAR>α : Type v<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>j : ℤ<VAR>g : G<VAR>a : α<GOAL>g ^ (j % ↑(period g a)) • a = g ^ j • a
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>x : α<VAR>f : α → E<VAR>hf : LocallyIntegrable f μ<VAR>w : Set α<VAR>w_nhds : w ∈ 𝓝 x<VAR>hw : IntegrableOn f w μ<GOAL>∀ᶠ (a : Set α) in v.filterAt x, IntegrableOn f a μ
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>x : α<VAR>f : α → E<VAR>hf : LocallyIntegrable f μ<VAR>w : Set α<VAR>w_nhds : w ∈ 𝓝 x<VAR>hw : IntegrableOn f w μ<VAR>a : Set α<VAR>ha : a ⊆ w<GOAL>IntegrableOn f a μ
<VAR>a q m : ℤ<VAR>b' r : ℕ<VAR>hm : q * ↑b' = m<VAR>h₂ : r.blt b' = true<VAR>h : ↑r + m = a<GOAL>a % ↑b' = ↑r
<VAR>a q m : ℤ<VAR>b' r : ℕ<VAR>hm : q * ↑b' = m<VAR>h₂ : r.blt b' = true<VAR>h : ↑r + m = a<GOAL>↑r % ↑b' = ↑r
<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>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>inst✝ : IsSemisimpleRing R<VAR>this✝ : Module R S := Module.compHom S f<VAR>this : RingHomSurjective f<VAR>e : S →ₛₗ[f] S := let __src := AddMonoidHom.id S; { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }<GOAL>IsSemisimpleRing S
<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>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>inst✝ : IsSemisimpleRing R<VAR>this✝ : Module R S := Module.compHom S f<VAR>this : RingHomSurjective f<VAR>e : S →ₛₗ[f] S := let __src := AddMonoidHom.id S; { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }<GOAL>IsSemisimpleModule R S
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>h : IsClosed s<VAR>hs : s.Nonempty<GOAL>x ∈ s ↔ infDist x s = 0
<VAR>R : Type u_2<VAR>K : Type ?u.69654<VAR>L : Type ?u.69657<VAR>S : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra K L<VAR>x✝ : S<VAR>hx : IsIntegral R x✝<VAR>x : S<VAR>i : ℕ<GOAL>(minpolyDiv R x).coeff i ∈ Algebra.adjoin R {x}
<VAR>R : Type u_2<VAR>K : Type ?u.69654<VAR>L : Type ?u.69657<VAR>S : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra K L<VAR>x✝ : S<VAR>hx : IsIntegral R x✝<VAR>x : S<VAR>i : ℕ<VAR>H : (minpolyDiv R x).coeff i ∉ Algebra.adjoin R {x}<GOAL>False
<VAR>R : Type u_2<VAR>K : Type ?u.69654<VAR>L : Type ?u.69657<VAR>S : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra K L<VAR>x✝ : S<VAR>hx : IsIntegral R x✝<VAR>x : S<VAR>i : ℕ<VAR>H : (minpolyDiv R x).coeff i ∉ Algebra.adjoin R {x}<VAR>this : ∀ (j : ℕ), (minpolyDiv R x).coeff (i + j) ∉ Algebra.adjoin R {x}<GOAL>False
<VAR>R : Type u_2<VAR>K : Type ?u.69654<VAR>L : Type ?u.69657<VAR>S : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra K L<VAR>x✝ : S<VAR>hx : IsIntegral R x✝<VAR>x : S<VAR>i : ℕ<VAR>H : (minpolyDiv R x).coeff i ∉ Algebra.adjoin R {x}<VAR>this : ∀ (j : ℕ), (minpolyDiv R x).coeff (i + j) ∉ Algebra.adjoin R {x}<GOAL>(minpolyDiv R x).coeff (i + ((minpolyDiv R x).natDegree + 1)) ∈ Algebra.adjoin R {x}
<VAR>R : Type u_2<VAR>K : Type ?u.69654<VAR>L : Type ?u.69657<VAR>S : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra K L<VAR>x✝ : S<VAR>hx : IsIntegral R x✝<VAR>x : S<VAR>i : ℕ<VAR>H : (minpolyDiv R x).coeff i ∉ Algebra.adjoin R {x}<VAR>this : ∀ (j : ℕ), (minpolyDiv R x).coeff (i + j) ∉ Algebra.adjoin R {x}<GOAL>0 ∈ Algebra.adjoin R {x}
<VAR>R : Type u_2<VAR>K : Type ?u.69654<VAR>L : Type ?u.69657<VAR>S : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra K L<VAR>x✝ : S<VAR>hx : IsIntegral R x✝<VAR>x : S<VAR>i : ℕ<VAR>H : (minpolyDiv R x).coeff i ∉ Algebra.adjoin R {x}<VAR>this : ∀ (j : ℕ), (minpolyDiv R x).coeff (i + j) ∉ Algebra.adjoin R {x}<GOAL>(minpolyDiv R x).natDegree < i + ((minpolyDiv R x).natDegree + 1)
<VAR>R : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero R<VAR>y p d : R<VAR>inst✝ : DecompositionMonoid R<GOAL>IsRadical 0
<VAR>R : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero R<VAR>y p d : R<VAR>inst✝ : DecompositionMonoid R<GOAL>IsReduced R
<VAR>α : Type u<VAR>α' : Type u_1<VAR>β✝ : Type v<VAR>β' : Type u_2<VAR>γ✝ : Type u_3<VAR>φ : Type u_4<VAR>inst✝⁵ : OmegaCompletePartialOrder α<VAR>inst✝⁴ : OmegaCompletePartialOrder β✝<VAR>inst✝³ : OmegaCompletePartialOrder γ✝<VAR>inst✝² : OmegaCompletePartialOrder φ<VAR>inst✝¹ : OmegaCompletePartialOrder α'<VAR>inst✝ : OmegaCompletePartialOrder β'<VAR>β γ : Type v<VAR>f : β → γ<VAR>g : α →𝒄 Part β<VAR>x✝ : α<GOAL>f <$> g x✝ = (g.bind (const (pure ∘ f))) x✝
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝² : Group H<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>d : TransversalPair G A B<VAR>inst✝ : DecidableEq G<VAR>g : G<VAR>u : ℤˣ<VAR>w : NormalWord d<VAR>h1 : w.head ∈ d.set u<VAR>h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'<GOAL>ReducedWord.prod φ (cons g u w h1 h2).toReducedWord = of g * (t ^ ↑u * ReducedWord.prod φ w.toReducedWord)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁹ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : InnerProductSpace ℝ F'<VAR>inst✝ : Fintype ι<VAR>v : Basis ι 𝕜 E<VAR>hv : Orthonormal 𝕜 ⇑v<GOAL>⇑(v.toOrthonormalBasis hv) = ⇑(v.toOrthonormalBasis hv).toBasis
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<GOAL>IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, ball x ε ⊆ s
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z w : K<GOAL>z ≤ 0 ↔ ∃ x ≤ 0, ↑x = z
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z w : K<GOAL>re z ≤ 0 ∧ im z = 0 ↔ ∃ x ≤ 0, re ↑x = re z ∧ im ↑x = im z
<VAR>R : Type uR<VAR>inst✝³ : CommRing R<VAR>A : Type uA<VAR>inst✝² : AddCommGroup A<VAR>A' : Type u_1<VAR>inst✝¹ : AddCommGroup A'<VAR>B : Type uB<VAR>inst✝ : AddCommGroup B<VAR>a : A<VAR>h : (ofSpanSingleton a) ⟨a, ⋯⟩ = 0<GOAL>a = 0
<VAR>R : Type uR<VAR>inst✝³ : CommRing R<VAR>A : Type uA<VAR>inst✝² : AddCommGroup A<VAR>A' : Type u_1<VAR>inst✝¹ : AddCommGroup A'<VAR>B : Type uB<VAR>inst✝ : AddCommGroup B<VAR>a : A<VAR>h : ∃ n, n • 1 = (↑(if addOrderOf a = 0 then 2 else addOrderOf a))⁻¹<GOAL>a = 0
<VAR>R : Type uR<VAR>inst✝³ : CommRing R<VAR>A : Type uA<VAR>inst✝² : AddCommGroup A<VAR>A' : Type u_1<VAR>inst✝¹ : AddCommGroup A'<VAR>B : Type uB<VAR>inst✝ : AddCommGroup B<VAR>a : A<VAR>n : ℤ<VAR>hn : (n • 1).den = (↑(if addOrderOf a = 0 then 2 else addOrderOf a))⁻¹.den<GOAL>a = 0
<VAR>R : Type uR<VAR>inst✝³ : CommRing R<VAR>A : Type uA<VAR>inst✝² : AddCommGroup A<VAR>A' : Type u_1<VAR>inst✝¹ : AddCommGroup A'<VAR>B : Type uB<VAR>inst✝ : AddCommGroup B<VAR>a : A<VAR>n : ℤ<VAR>hn : 1 = if addOrderOf a = 0 then 2 else addOrderOf a<GOAL>a = 0
<VAR>R : Type uR<VAR>inst✝³ : CommRing R<VAR>A : Type uA<VAR>inst✝² : AddCommGroup A<VAR>A' : Type u_1<VAR>inst✝¹ : AddCommGroup A'<VAR>B : Type uB<VAR>inst✝ : AddCommGroup B<VAR>a : A<VAR>n : ℤ<VAR>hn : 1 = (↑(if addOrderOf a = 0 then 2 else addOrderOf a))⁻¹.den<GOAL>0 < if addOrderOf a = 0 then 2 else addOrderOf a
<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>a b c d x y z : P<VAR>r R : ℝ<GOAL>inversion c R x = c ↔ x = c ∨ R = 0
<VAR>G✝ : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁵ : TopologicalSpace G✝<VAR>inst✝⁴ : Group G✝<VAR>inst✝³ : TopologicalGroup G✝<VAR>inst✝² : TopologicalSpace α<VAR>f : α → G✝<VAR>s : Set α<VAR>x : α<VAR>G : Type u<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalSpace G<VAR>hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)<VAR>hinv : Tendsto (fun x => x⁻¹) (𝓝 1) (𝓝 1)<VAR>hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)<VAR>hright : ∀ (x₀ : G), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)<VAR>x₀ : G<GOAL>map (fun x => x₀ * x * x₀⁻¹) (𝓝 1) = 𝓝 1
<VAR>G✝ : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁵ : TopologicalSpace G✝<VAR>inst✝⁴ : Group G✝<VAR>inst✝³ : TopologicalGroup G✝<VAR>inst✝² : TopologicalSpace α<VAR>f : α → G✝<VAR>s : Set α<VAR>x : α<VAR>G : Type u<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalSpace G<VAR>hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)<VAR>hinv : Tendsto (fun x => x⁻¹) (𝓝 1) (𝓝 1)<VAR>hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)<VAR>hright : ∀ (x₀ : G), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)<VAR>x₀ : G<GOAL>map ((fun x => x * x₀⁻¹) ∘ fun x => x * x₀) (𝓝 1) = 𝓝 1
<VAR>n : ℕ<VAR>inst✝ : NeZero n<GOAL>1 ≤ n
<VAR>n : ℕ<VAR>inst✝ : NeZero n<VAR>this : n ≠ 0<GOAL>1 ≤ n
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<GOAL>(mk W) W.ψ₂ ^ 2 = (mk W) (C W.Ψ₂Sq)
<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>ε : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>hf : ApproximatesLinearOn f (↑f') s c<VAR>hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹<GOAL>ContinuousOn (↑(hf.toPartialEquiv hc).symm) (f '' s)