ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : TopologicalGroup G<VAR>inst✝⁵ : MulAction G X<VAR>inst✝⁴ : SigmaCompactSpace G<VAR>inst✝³ : BaireSpace X<VAR>inst✝² : T2Space X<VAR>inst✝¹ : ContinuousSMul G X<VAR>inst✝ : IsPretransitive G X<VAR>x : X<VAR>g : G<VAR>U : Set G<VAR>hU : U ∈ 𝓝 g<VAR>this : (fun x_1 => x_1 • x) = (fun x_1 => x_1 • g • x) ∘ fun x => x * g⁻¹<GOAL>(fun g => g • x) '' U ∈ 𝓝 (g • x)
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : TopologicalGroup G<VAR>inst✝⁵ : MulAction G X<VAR>inst✝⁴ : SigmaCompactSpace G<VAR>inst✝³ : BaireSpace X<VAR>inst✝² : T2Space X<VAR>inst✝¹ : ContinuousSMul G X<VAR>inst✝ : IsPretransitive G X<VAR>x : X<VAR>g : G<VAR>U : Set G<VAR>hU : U ∈ 𝓝 g<VAR>this : (fun x_1 => x_1 • x) = (fun x_1 => x_1 • g • x) ∘ fun x => x * g⁻¹<GOAL>(fun x => x * g⁻¹) '' U • {g • x} ∈ 𝓝 (g • x)
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : TopologicalGroup G<VAR>inst✝⁵ : MulAction G X<VAR>inst✝⁴ : SigmaCompactSpace G<VAR>inst✝³ : BaireSpace X<VAR>inst✝² : T2Space X<VAR>inst✝¹ : ContinuousSMul G X<VAR>inst✝ : IsPretransitive G X<VAR>x : X<VAR>g : G<VAR>U : Set G<VAR>hU : U ∈ 𝓝 g<VAR>this : (fun x_1 => x_1 • x) = (fun x_1 => x_1 • g • x) ∘ fun x => x * g⁻¹<GOAL>(fun x => x * g⁻¹) '' U ∈ 𝓝 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>p : PMF α<VAR>s✝ t✝ s t : Set α<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>h : s ∩ p.support ⊆ t<GOAL>p.toMeasure s ≤ p.toMeasure t
<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 z • p]<VAR>m : ℤ<VAR>hm : b - a = m • z • p<GOAL>b - a = (m * z) • p
<VAR>T : Type u<VAR>inst✝ : Category.{v, u} T<VAR>f g : Arrow T<VAR>e : f ≅ g<GOAL>g.hom = e.inv.left ≫ f.hom ≫ e.hom.right
<VAR>T : Type u<VAR>inst✝ : Category.{v, u} T<VAR>f g : Arrow T<VAR>e : f ≅ g<VAR>eq : (e.inv ≫ e.hom).right = (𝟙 g).right<GOAL>g.hom = e.inv.left ≫ f.hom ≫ e.hom.right
<VAR>T : Type u<VAR>inst✝ : Category.{v, u} T<VAR>f g : Arrow T<VAR>e : f ≅ g<VAR>eq : e.inv.right ≫ e.hom.right = 𝟙 g.right<GOAL>g.hom = e.inv.left ≫ f.hom ≫ e.hom.right
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X✝ Y : Set α<VAR>e : α<VAR>ι : Type u_2<VAR>inst✝ : Nonempty ι<VAR>X : ι → Set α<VAR>hI : ∀ (i : ι), M.Basis I (X i)<GOAL>M.Basis I (⋃ i, X i)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X✝ Y : Set α<VAR>e : α<VAR>ι : Type u_2<VAR>inst✝ : Nonempty ι<VAR>X : ι → Set α<VAR>hI : ∀ (i : ι), M.Basis I (X i)<GOAL>M.Indep I
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>K : Type u_5<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<GOAL>IsUnit ↑(den A 0)
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B C : Matrix n n α<VAR>h : B * A = 1<VAR>g : C * A = 1<GOAL>B = C
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : NormedAddCommGroup β<VAR>l : Filter α<VAR>f : α → β<VAR>hf : l.ZeroAtFilter f<GOAL>l.BoundedAtFilter f
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : NormedAddCommGroup β<VAR>l : Filter α<VAR>f : α → β<VAR>hf : f =o[l] fun _x => 1<GOAL>l.BoundedAtFilter f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : SMul 𝕜 E<VAR>s : Set E<VAR>x✝ y✝ x y : E<GOAL>[x-[𝕜]y] = (fun p => p.1 • x + p.2 • y) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1}
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CommRing T<VAR>α : Type u_4<VAR>β : Type u_5<VAR>x✝ y : 𝕎 R<VAR>m : ℕ<VAR>x : 𝕎 R<GOAL>WittVector.ghostFun (m • x) = m • WittVector.ghostFun x
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>h : λ ∣ FermatLastTheoremForThreeGen.Solution.x S<GOAL>False
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>h : λ ^ (3 * S.multiplicity - 2) * λ ∣ λ ^ (3 * S.multiplicity - 2) * FermatLastTheoremForThreeGen.Solution.x S<GOAL>False
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>h : λ * λ ^ (3 * S.multiplicity - 2) ∣ S.a + S.b<GOAL>False
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>h : λ * λ ^ (3 * S.multiplicity - 2) * λ * λ ∣ (S.a + S.b) * (S.a + ↑η * S.b) * (S.a + ↑η ^ 2 * S.b)<GOAL>False
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>h : λ * λ ^ (3 * S.multiplicity - 2) * λ * λ ∣ (λ ^ S.multiplicity * FermatLastTheoremForThreeGen.Solution.w S) ^ 3<GOAL>False
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>h : λ ^ (3 * S.multiplicity - 2 + 1 + 1) * λ ∣ (λ ^ S.multiplicity * FermatLastTheoremForThreeGen.Solution.w S) ^ 3<GOAL>False
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>h : λ ^ (3 * S.multiplicity - 2 + 1 + 1) * λ ∣ (λ ^ S.multiplicity * FermatLastTheoremForThreeGen.Solution.w S) ^ 3<VAR>this : 2 ≤ S.multiplicity<GOAL>False
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>h : λ ∣ FermatLastTheoremForThreeGen.Solution.w S ^ 3<VAR>this : 2 ≤ S.multiplicity<GOAL>False
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>h : λ ^ (3 * S.multiplicity) * λ ∣ λ ^ (3 * S.multiplicity) * FermatLastTheoremForThreeGen.Solution.w S ^ 3<VAR>this : 2 ≤ S.multiplicity<GOAL>λ ^ (3 * S.multiplicity) ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoid α<VAR>a b : α<GOAL>Associates.mk a ∣ Associates.mk b ↔ a ∣ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoid α<VAR>a b : α<GOAL>(∃ x, a * x ~ᵤ b) ↔ ∃ c, b = a * c
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>M'' : Type u_5<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : AddCommGroup M''<VAR>inst✝ : Module R M''<VAR>N : Submodule R M<VAR>r : R<GOAL>(∀ (a : M) (b : a ∈ N), r • ⟨a, b⟩ = 0 → ⟨a, b⟩ = 0) ↔ ∀ x ∈ N, r • x = 0 → x = 0
<VAR>V : Type (u + 1)<VAR>inst✝² : LargeCategory V<VAR>G : MonCat<VAR>inst✝¹ : MonoidalCategory V<VAR>H : Grp<VAR>X : Action V ((forget₂ Grp MonCat).obj H)<VAR>inst✝ : LeftRigidCategory V<VAR>h : ↑H<GOAL>(ᘁX).ρ h = ᘁX.ρ h⁻¹
<VAR>V : Type (u + 1)<VAR>inst✝² : LargeCategory V<VAR>G : MonCat<VAR>inst✝¹ : MonoidalCategory V<VAR>H : Grp<VAR>X : Action V ((forget₂ Grp MonCat).obj H)<VAR>inst✝ : LeftRigidCategory V<VAR>h : ↑H<GOAL>(ᘁX).ρ h = ᘁX.ρ (inv h)
<VAR>V : Type (u + 1)<VAR>inst✝² : LargeCategory V<VAR>G : MonCat<VAR>inst✝¹ : MonoidalCategory V<VAR>H : Grp<VAR>X : Action V ((forget₂ Grp MonCat).obj H)<VAR>inst✝ : LeftRigidCategory V<VAR>h : ↑H<GOAL>SingleObj H.1
<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✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a✝ b✝ : ℝ<VAR>f✝ g : ℝ → E<VAR>μ : Measure ℝ<VAR>f : ℝ → E<VAR>a b : ℝ<GOAL>∫ (x : ℝ) in a..b, f x ∂μ ∈ {∫ (x : ℝ) in Ι a b, f x ∂μ, -∫ (x : ℝ) in Ι a b, f x ∂μ}
<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✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a✝ b✝ : ℝ<VAR>f✝ g : ℝ → E<VAR>μ : Measure ℝ<VAR>f : ℝ → E<VAR>a b : ℝ<GOAL>(if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, f x ∂μ ∈ {∫ (x : ℝ) in Ι a b, f x ∂μ, -∫ (x : ℝ) in Ι a b, f x ∂μ}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>f : α →₀ M<VAR>y : M<GOAL>y ∈ f.frange ↔ y ≠ 0 ∧ ∃ x, f x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>f : α →₀ M<VAR>y : M<GOAL>(∃ a ∈ f.support, f a = y) ↔ y ≠ 0 ∧ ∃ x, f x = y
<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>p₁ p₂ p₃ p₃' : P<VAR>h : Wbtw ℝ p₂ p₃ p₃'<VAR>hp₃p₂ : p₃ ≠ p₂<GOAL>∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>A✝ : Type u_3<VAR>B : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : AddMonoidWithOne B<VAR>inst✝⁴ : FunLike F ℕ A✝<VAR>inst✝³ : AddMonoidWithOne A✝<VAR>A : Type u_6<VAR>inst✝² : AddMonoidWithOne A<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : AddMonoidHomClass F A B<VAR>f : F<VAR>h : f 1 = 1<GOAL>f ↑0 = ↑0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>A✝ : Type u_3<VAR>B : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : AddMonoidWithOne B<VAR>inst✝⁴ : FunLike F ℕ A✝<VAR>inst✝³ : AddMonoidWithOne A✝<VAR>A : Type u_6<VAR>inst✝² : AddMonoidWithOne A<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : AddMonoidHomClass F A B<VAR>f : F<VAR>h : f 1 = 1<VAR>n : ℕ<GOAL>f ↑(n + 1) = ↑(n + 1)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : Monoid α<VAR>s t : Set α<VAR>a✝ : α<VAR>m n✝ : ℕ<VAR>a : α<VAR>n : ℕ<VAR>f : Fin n → Set α<GOAL>a ∈ (List.ofFn f).prod ↔ ∃ l', (List.map (fun x => ↑x.snd) l').prod = a ∧ List.map Sigma.fst l' = List.ofFn f
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : Monoid α<VAR>s t : Set α<VAR>a✝ : α<VAR>m n✝ : ℕ<VAR>a : α<VAR>n : ℕ<VAR>f : Fin n → Set α<GOAL>(∃ f_1, (List.ofFn fun i => ↑(f_1 i)).prod = a) ↔ ∃ x, (List.ofFn fun x_1 => ↑(x x_1).snd).prod = a ∧ (fun x_1 => (x x_1).fst) = f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : MetricSpace R<VAR>inst✝⁸ : TopologicalSemiring R<VAR>inst✝⁷ : ContinuousStar R<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : ContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝<VAR>inst✝¹ : UniqueContinuousFunctionalCalculus R A<VAR>inst✝ : Nontrivial A<VAR>r : R<GOAL>spectrum R ((algebraMap R A) r) = {r}
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : MetricSpace R<VAR>inst✝⁸ : TopologicalSemiring R<VAR>inst✝⁷ : ContinuousStar R<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : ContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝<VAR>inst✝¹ : UniqueContinuousFunctionalCalculus R A<VAR>inst✝ : Nontrivial A<VAR>r : R<VAR>hp : p 0<GOAL>spectrum R ((algebraMap R A) r) = {r}
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : MetricSpace R<VAR>inst✝⁸ : TopologicalSemiring R<VAR>inst✝⁷ : ContinuousStar R<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : ContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝<VAR>inst✝¹ : UniqueContinuousFunctionalCalculus R A<VAR>inst✝ : Nontrivial A<VAR>r : R<VAR>hp : p 0<GOAL>(fun x => r) '' spectrum R 0 = {r}
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>Fintype.card ↑(Set.Iio b) = ↑b
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ✝ : M<VAR>f : F<VAR>h : IsPrimitiveRoot ζ✝ k<VAR>n : ℕ<VAR>ζ : M<VAR>hζ : IsPrimitiveRoot ζ n<GOAL>Set.InjOn (fun x => ζ ^ x) ↑(range n)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ✝ : M<VAR>f : F<VAR>h : IsPrimitiveRoot ζ✝ k<VAR>ζ : M<VAR>hζ : IsPrimitiveRoot ζ 0<GOAL>Set.InjOn (fun x => ζ ^ x) ↑(range 0)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ✝ : M<VAR>f : F<VAR>h : IsPrimitiveRoot ζ✝ k<VAR>n : ℕ<VAR>ζ : M<VAR>hζ : IsPrimitiveRoot ζ n<VAR>hn : n > 0<GOAL>Set.InjOn (fun x => ζ ^ x) ↑(range n)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ✝ : M<VAR>f : F<VAR>h : IsPrimitiveRoot ζ✝ k<VAR>n : ℕ<VAR>ζ : M<VAR>hζ : IsPrimitiveRoot ζ n<VAR>hn : n > 0<VAR>i : ℕ<VAR>hi : i ∈ ↑(range n)<VAR>j : ℕ<VAR>hj : j ∈ ↑(range n)<VAR>e : (fun x => ζ ^ x) i = (fun x => ζ ^ x) j<GOAL>i = j
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ✝ : M<VAR>f : F<VAR>h : IsPrimitiveRoot ζ✝ k<VAR>n : ℕ<VAR>ζ : M<VAR>hζ : IsPrimitiveRoot ζ n<VAR>hn : n > 0<VAR>i : ℕ<VAR>hi : i < n<VAR>j : ℕ<VAR>hj : j < n<VAR>e : (fun x => ζ ^ x) i = (fun x => ζ ^ x) j<GOAL>i = j
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ✝ : M<VAR>f : F<VAR>h : IsPrimitiveRoot ζ✝ k<VAR>n : ℕ<VAR>ζ : M<VAR>hζ : IsPrimitiveRoot ζ n<VAR>hn : n > 0<VAR>i : ℕ<VAR>hi : i < n<VAR>j : ℕ<VAR>hj : j < n<VAR>e : (fun x => ζ ^ x) i = (fun x => ζ ^ x) j<VAR>this : ⋯.unit ^ i = ⋯.unit ^ j<GOAL>i = j
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ✝ : M<VAR>f : F<VAR>h : IsPrimitiveRoot ζ✝ k<VAR>n : ℕ<VAR>ζ : M<VAR>hζ : IsPrimitiveRoot ζ n<VAR>hn : n > 0<VAR>i : ℕ<VAR>hi : i < n<VAR>j : ℕ<VAR>hj : j < n<VAR>e : (fun x => ζ ^ x) i = (fun x => ζ ^ x) j<VAR>this : i % orderOf ({ toFun := Units.val, map_one' := ⋯, map_mul' := ⋯ } ⋯.unit) = j % orderOf ({ toFun := Units.val, map_one' := ⋯, map_mul' := ⋯ } ⋯.unit)<GOAL>i = j
<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>β : Type u_7<VAR>inst✝ : Group β<VAR>f g : α → β<GOAL>f / g =ᶠ[ae μ] 1 ↔ f =ᶠ[ae μ] g
<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>β : Type u_7<VAR>inst✝ : Group β<VAR>f g : α → β<VAR>h : f / g =ᶠ[ae μ] 1<VAR>x : α<VAR>hx : (f / g) x = 1 x<GOAL>f x = g x
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β✝ : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β✝<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>β : Type u_7<VAR>inst✝ : Group β<VAR>f g : α → β<VAR>h : f =ᶠ[ae μ] g<VAR>x : α<VAR>hx : f x = g x<GOAL>(f / g) x = 1 x
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>w : ℂ<VAR>hf : CircleIntegrable f c R<VAR>hw : Complex.abs w < R<GOAL>HasSum (fun n => ∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>w : ℂ<VAR>hf : CircleIntegrable f c R<VAR>hw : Complex.abs w < R<VAR>hR : 0 < R<GOAL>HasSum (fun n => ∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>w : ℂ<VAR>hf : CircleIntegrable f c R<VAR>hw : Complex.abs w < R<VAR>hR : 0 < R<VAR>hwR : Complex.abs w / R ∈ Ico 0 1<GOAL>HasSum (fun n => ∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>w : ℂ<VAR>hf : CircleIntegrable f c R<VAR>hw : Complex.abs w < R<VAR>hR : 0 < R<VAR>hwR : Complex.abs w / R ∈ Ico 0 1<VAR>n : ℕ<GOAL>AEStronglyMeasurable (fun θ => deriv (circleMap c R) θ • (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R θ)) (volume.restrict (Ι 0 (2 * π)))
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>w : ℂ<VAR>hf : CircleIntegrable f c R<VAR>hw : Complex.abs w < R<VAR>hR : 0 < R<VAR>hwR : Complex.abs w / R ∈ Ico 0 1<VAR>n : ℕ<GOAL>∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → ‖deriv (circleMap c R) t • (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R t)‖ ≤ (fun n θ => ‖f (circleMap c R θ)‖ * (Complex.abs w / R) ^ n) n t
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>w : ℂ<VAR>hf : CircleIntegrable f c R<VAR>hw : Complex.abs w < R<VAR>hR : 0 < R<VAR>hwR : Complex.abs w / R ∈ Ico 0 1<GOAL>∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → Summable fun n => (fun n θ => ‖f (circleMap c R θ)‖ * (Complex.abs w / R) ^ n) n t
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>w : ℂ<VAR>hf : CircleIntegrable f c R<VAR>hw : Complex.abs w < R<VAR>hR : 0 < R<VAR>hwR : Complex.abs w / R ∈ Ico 0 1<GOAL>IntervalIntegrable (fun t => ∑' (n : ℕ), (fun n θ => ‖f (circleMap c R θ)‖ * (Complex.abs w / R) ^ n) n t) volume 0 (2 * π)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>w : ℂ<VAR>hf : CircleIntegrable f c R<VAR>hw : Complex.abs w < R<VAR>hR : 0 < R<VAR>hwR : Complex.abs w / R ∈ Ico 0 1<GOAL>∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → HasSum (fun n => deriv (circleMap c R) t • (fun z => (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R t)) (deriv (circleMap c R) t • (fun z => (z - (c + w))⁻¹ • f z) (circleMap c R t))
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : TopologicalSpace V<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : Module R V<VAR>inst✝ : SeparatingDual R V<VAR>x y : V<VAR>h : x ≠ y<GOAL>∃ f, f x ≠ f y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : TopologicalSpace V<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : Module R V<VAR>inst✝ : SeparatingDual R V<VAR>x y : V<VAR>h : x ≠ y<VAR>f : V →L[R] R<VAR>hf : f (x - y) ≠ 0<GOAL>∃ f, f x ≠ f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>l✝ m✝ : Language α<VAR>a b x : List α<VAR>l m : Language α<GOAL>(l * m).reverse = m.reverse * l.reverse
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>l✝ m✝ : Language α<VAR>a b x : List α<VAR>l m : Language α<GOAL>image2 (fun a b => b.reverse ++ a.reverse) l m = image2 (fun a b => a.reverse ++ b.reverse) m l
<VAR>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>hf : f.FinitePresentation<VAR>this✝ : Algebra R S := f.toAlgebra<VAR>this : Algebra R S' := ((algebraMap S S').comp f).toAlgebra<GOAL>(IsLocalization.map S' f ⋯).FinitePresentation
<VAR>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>hf : f.FinitePresentation<VAR>this✝ : Algebra R S := f.toAlgebra<VAR>this : Algebra R S' := ((algebraMap S S').comp f).toAlgebra<VAR>f' : R' →+* S' := IsLocalization.map S' f ⋯<GOAL>(IsLocalization.map S' f ⋯).FinitePresentation
<VAR>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>hf : f.FinitePresentation<VAR>this✝¹ : Algebra R S := f.toAlgebra<VAR>this✝ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra<VAR>f' : R' →+* S' := IsLocalization.map S' f ⋯<VAR>this : Algebra R' S' := f'.toAlgebra<GOAL>(IsLocalization.map S' f ⋯).FinitePresentation
<VAR>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>hf : f.FinitePresentation<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra<VAR>f' : R' →+* S' := IsLocalization.map S' f ⋯<VAR>this✝ : Algebra R' S' := f'.toAlgebra<VAR>this : IsScalarTower R R' S'<GOAL>(IsLocalization.map S' f ⋯).FinitePresentation