ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>ι : Sort u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : α → M<VAR>a : α<VAR>ha : ∀ (x : α), x ≠ a → f x = 1<VAR>this : mulSupport (f ∘ PLift.down) ⊆ ↑{{ down := a }}<GOAL>∏ᶠ (x : α), f x = f a
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>k : Type u_5<VAR>K : Type u_6<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₁ : Type u_9<VAR>M₂ : Type u_10<VAR>M₃ : Type u_11<VAR>N₁ : Type u_12<VAR>N₂ : Type u_13<VAR>N₃ : Type u_14<VAR>N₄ : Type u_15<VAR>ι : Type u_16<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : Semiring S<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : SMulCommClass R S M<VAR>f : R →ₗ[R] M<GOAL>(smulRight 1 ({ toFun := fun f => f 1, map_add' := ⋯, map_smul' := ⋯ }.toFun f)) 1 = f 1
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>M N : Mon_ C<GOAL>(λ_ (𝟙_ C)).inv ▷ (M.X ⊗ N.X) ≫ (M.one ⊗ N.one) ▷ (M.X ⊗ N.X) ≫ tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul) = (λ_ (M.X ⊗ N.X)).hom
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>M N : Mon_ C<GOAL>(λ_ (𝟙_ C)).inv ▷ (M.X ⊗ N.X) ≫ (tensor_μ C (𝟙_ C, 𝟙_ C) (M.X, N.X) ≫ (M.one ▷ M.X ⊗ N.one ▷ N.X)) ≫ (M.mul ⊗ N.mul) = (λ_ (M.X ⊗ N.X)).hom
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>M N : Mon_ C<GOAL>(λ_ (𝟙_ C)).inv ▷ (M.X ⊗ N.X) ≫ tensor_μ C (𝟙_ C, 𝟙_ C) (M.X, N.X) ≫ ((λ_ M.X).hom ⊗ (λ_ N.X).hom) = (λ_ (M.X ⊗ N.X)).hom
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>M N : Mon_ C<GOAL>(λ_ (M.X ⊗ N.X)).hom = (λ_ (𝟙_ C)).inv ▷ (M.X ⊗ N.X) ≫ tensor_μ C (𝟙_ C, 𝟙_ C) (M.X, N.X) ≫ ((λ_ M.X).hom ⊗ (λ_ N.X).hom)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : CommGroup G<VAR>a✝ b✝ c✝ d a b c : G<GOAL>a * b / (a / c) = b * c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>s t u : Finset α<VAR>a b : α<GOAL>_root_.Disjoint ↑s ↑t ↔ _root_.Disjoint s t
<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 : α<GOAL>f.IsCycleOn ∅
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_2<VAR>𝔸 : Type u_3<VAR>inst✝³ : NormedField 𝕜'<VAR>inst✝² : NormedRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕜 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝔸<VAR>c d : 𝕜 → 𝔸<VAR>c' d' : 𝔸<VAR>u v : 𝕜 → 𝕜'<VAR>hc : HasDerivWithinAt c c' s x<VAR>hd : HasDerivWithinAt d d' s x<GOAL>HasDerivWithinAt (fun y => c y * d y) (c' * d x + c x * d') s x
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_2<VAR>𝔸 : Type u_3<VAR>inst✝³ : NormedField 𝕜'<VAR>inst✝² : NormedRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕜 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝔸<VAR>c d : 𝕜 → 𝔸<VAR>c' d' : 𝔸<VAR>u v : 𝕜 → 𝕜'<VAR>hc : HasDerivWithinAt c c' s x<VAR>hd : HasDerivWithinAt d d' s x<VAR>this : HasDerivWithinAt (fun y => c y * d y) ((c x • smulRight 1 d' + (smulRight 1 c').smulRight (d x)) 1) s x<GOAL>HasDerivWithinAt (fun y => c y * d y) (c' * d x + c x * d') s x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K✝ : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K✝<VAR>inst✝ : IsDedekindDomain R<VAR>I J K : Ideal R<VAR>coprime : ∀ (P : Ideal R), J ≤ P → K ≤ P → ¬P.IsPrime<VAR>hJ : I ≤ J<VAR>hK : I ≤ K<GOAL>I ≤ J * K
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K✝ : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K✝<VAR>inst✝ : IsDedekindDomain R<VAR>I J K : Ideal R<VAR>coprime : ∀ (P : Ideal R), P ∣ J → P ∣ K → ¬P.IsPrime<VAR>hJ : J ∣ I<VAR>hK : K ∣ I<GOAL>J * K ∣ I
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K✝ : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K✝<VAR>inst✝ : IsDedekindDomain R<VAR>J K : Ideal R<VAR>coprime : ∀ (P : Ideal R), P ∣ J → P ∣ K → ¬P.IsPrime<VAR>hJ0 : ¬J = 0<VAR>I' : Ideal R<VAR>hJ : J ∣ K * I'<GOAL>J * K ∣ K * I'
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K✝ : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K✝<VAR>inst✝ : IsDedekindDomain R<VAR>J K : Ideal R<VAR>coprime : ∀ (P : Ideal R), P ∣ J → P ∣ K → ¬P.IsPrime<VAR>hJ0 : ¬J = 0<VAR>I' : Ideal R<VAR>hJ : J ∣ K * I'<GOAL>K * J ∣ K * I'
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K✝ : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K✝<VAR>inst✝ : IsDedekindDomain R<VAR>J K : Ideal R<VAR>coprime : ∀ (P : Ideal R), P ∣ J → P ∣ K → ¬P.IsPrime<VAR>hJ0 : ¬J = 0<VAR>I' : Ideal R<VAR>hJ : J ∣ K * I'<GOAL>∀ {d : Ideal R}, d ∣ J → d ∣ K → ¬Prime d
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>hG : IsPGroup p G<VAR>H : Type u_2<VAR>inst✝ : Group H<VAR>ϕ : G →* H<VAR>hϕ : Function.Surjective ⇑ϕ<GOAL>IsPGroup p H
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>hG : IsPGroup p G<VAR>H : Type u_2<VAR>inst✝ : Group H<VAR>ϕ : G →* H<VAR>hϕ : Function.Surjective ⇑ϕ<VAR>h : H<VAR>g : G<VAR>hg : ϕ g = h<VAR>k : ℕ<VAR>hk : g ^ p ^ k = 1<GOAL>h ^ p ^ k = 1
<VAR>B : Type u₁<VAR>inst✝² : Bicategory B<VAR>C : Type u₂<VAR>inst✝¹ : Bicategory C<VAR>D : Type u₃<VAR>inst✝ : Bicategory D<VAR>F✝ : Pseudofunctor B C<VAR>F : LaxFunctor B C<VAR>F' : F.PseudoCore<VAR>a✝ b✝ c✝ : B<VAR>f : a✝ ⟶ b✝<VAR>g h : b✝ ⟶ c✝<VAR>η : g ⟶ h<GOAL>F.map₂ (f ◁ η) = ((fun {a b c} => F'.mapCompIso) f g).hom ≫ F.map f ◁ F.map₂ η ≫ ((fun {a b c} => F'.mapCompIso) f h).inv
<VAR>B : Type u₁<VAR>inst✝² : Bicategory B<VAR>C : Type u₂<VAR>inst✝¹ : Bicategory C<VAR>D : Type u₃<VAR>inst✝ : Bicategory D<VAR>F✝ : Pseudofunctor B C<VAR>F : LaxFunctor B C<VAR>F' : F.PseudoCore<VAR>a✝ b✝ c✝ : B<VAR>f✝ g✝ : a✝ ⟶ b✝<VAR>η : f✝ ⟶ g✝<VAR>h : b✝ ⟶ c✝<GOAL>F.map₂ (η ▷ h) = ((fun {a b c} => F'.mapCompIso) f✝ h).hom ≫ F.map₂ η ▷ F.map h ≫ ((fun {a b c} => F'.mapCompIso) g✝ h).inv
<VAR>B : Type u₁<VAR>inst✝² : Bicategory B<VAR>C : Type u₂<VAR>inst✝¹ : Bicategory C<VAR>D : Type u₃<VAR>inst✝ : Bicategory D<VAR>F✝ : Pseudofunctor B C<VAR>F : LaxFunctor B C<VAR>F' : F.PseudoCore<VAR>a b c d : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<GOAL>F.map₂ (α_ f g h).hom = ((fun {a b c} => F'.mapCompIso) (f ≫ g) h).hom ≫ ((fun {a b c} => F'.mapCompIso) f g).hom ▷ F.map h ≫ (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ ((fun {a b c} => F'.mapCompIso) g h).inv ≫ ((fun {a b c} => F'.mapCompIso) f (g ≫ h)).inv
<VAR>B : Type u₁<VAR>inst✝² : Bicategory B<VAR>C : Type u₂<VAR>inst✝¹ : Bicategory C<VAR>D : Type u₃<VAR>inst✝ : Bicategory D<VAR>F✝ : Pseudofunctor B C<VAR>F : LaxFunctor B C<VAR>F' : F.PseudoCore<VAR>a b c d : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<GOAL>inv (((fun {a b c} => F'.mapCompIso) f g).hom ▷ F.map h) ≫ ((fun {a b c} => F'.mapCompIso) (f ≫ g) h).inv ≫ F.map₂ (α_ f g h).hom = (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ F.mapComp g h ≫ F.mapComp f (g ≫ h)
<VAR>B : Type u₁<VAR>inst✝² : Bicategory B<VAR>C : Type u₂<VAR>inst✝¹ : Bicategory C<VAR>D : Type u₃<VAR>inst✝ : Bicategory D<VAR>F✝ : Pseudofunctor B C<VAR>F : LaxFunctor B C<VAR>F' : F.PseudoCore<VAR>a b : B<VAR>f : a ⟶ b<GOAL>F.map₂ (λ_ f).hom = ((fun {a b c} => F'.mapCompIso) (𝟙 a) f).hom ≫ (F'.mapIdIso a).hom ▷ F.map f ≫ (λ_ (F.map f)).hom
<VAR>B : Type u₁<VAR>inst✝² : Bicategory B<VAR>C : Type u₂<VAR>inst✝¹ : Bicategory C<VAR>D : Type u₃<VAR>inst✝ : Bicategory D<VAR>F✝ : Pseudofunctor B C<VAR>F : LaxFunctor B C<VAR>F' : F.PseudoCore<VAR>a b : B<VAR>f : a ⟶ b<GOAL>F.map₂ (inv (λ_ f).hom) = inv (((fun {a b c} => F'.mapCompIso) (𝟙 a) f).hom ≫ (F'.mapIdIso a).hom ▷ F.map f ≫ (λ_ (F.map f)).hom)
<VAR>B : Type u₁<VAR>inst✝² : Bicategory B<VAR>C : Type u₂<VAR>inst✝¹ : Bicategory C<VAR>D : Type u₃<VAR>inst✝ : Bicategory D<VAR>F✝ : Pseudofunctor B C<VAR>F : LaxFunctor B C<VAR>F' : F.PseudoCore<VAR>a b : B<VAR>f : a ⟶ b<GOAL>F.map₂ (ρ_ f).hom = ((fun {a b c} => F'.mapCompIso) f (𝟙 b)).hom ≫ F.map f ◁ (F'.mapIdIso b).hom ≫ (ρ_ (F.map f)).hom
<VAR>B : Type u₁<VAR>inst✝² : Bicategory B<VAR>C : Type u₂<VAR>inst✝¹ : Bicategory C<VAR>D : Type u₃<VAR>inst✝ : Bicategory D<VAR>F✝ : Pseudofunctor B C<VAR>F : LaxFunctor B C<VAR>F' : F.PseudoCore<VAR>a b : B<VAR>f : a ⟶ b<GOAL>F.map₂ (inv (ρ_ f).hom) = inv (((fun {a b c} => F'.mapCompIso) f (𝟙 b)).hom ≫ F.map f ◁ (F'.mapIdIso b).hom ≫ (ρ_ (F.map f)).hom)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>u : κ → UniformSpace α'<VAR>F : ι → X → α'<VAR>S : Set X<GOAL>EquicontinuousOn F S ↔ ∀ (k : κ), EquicontinuousOn F S
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hdf : ∀ᶠ (x : ℝ) in atTop, DifferentiableAt ℝ f x<VAR>hg' : ∀ᶠ (x : ℝ) in atTop, deriv g x ≠ 0<VAR>hftop : Tendsto f atTop (𝓝 0)<VAR>hgtop : Tendsto g atTop (𝓝 0)<VAR>hdiv : Tendsto (fun x => deriv f x / deriv g x) atTop l<GOAL>Tendsto (fun x => f x / g x) atTop l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hdf : ∀ᶠ (x : ℝ) in atTop, DifferentiableAt ℝ f x<VAR>hg' : ∀ᶠ (x : ℝ) in atTop, deriv g x ≠ 0<VAR>hftop : Tendsto f atTop (𝓝 0)<VAR>hgtop : Tendsto g atTop (𝓝 0)<VAR>hdiv : Tendsto (fun x => deriv f x / deriv g x) atTop l<VAR>hdg : ∀ᶠ (x : ℝ) in atTop, DifferentiableAt ℝ g x<GOAL>Tendsto (fun x => f x / g x) atTop l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hdf : ∀ᶠ (x : ℝ) in atTop, DifferentiableAt ℝ f x<VAR>hg' : ∀ᶠ (x : ℝ) in atTop, deriv g x ≠ 0<VAR>hftop : Tendsto f atTop (𝓝 0)<VAR>hgtop : Tendsto g atTop (𝓝 0)<VAR>hdiv : Tendsto (fun x => deriv f x / deriv g x) atTop l<VAR>hdg : ∀ᶠ (x : ℝ) in atTop, DifferentiableAt ℝ g x<VAR>hdf' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt f (deriv f x) x<GOAL>Tendsto (fun x => f x / g x) atTop l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hdf : ∀ᶠ (x : ℝ) in atTop, DifferentiableAt ℝ f x<VAR>hg' : ∀ᶠ (x : ℝ) in atTop, deriv g x ≠ 0<VAR>hftop : Tendsto f atTop (𝓝 0)<VAR>hgtop : Tendsto g atTop (𝓝 0)<VAR>hdiv : Tendsto (fun x => deriv f x / deriv g x) atTop l<VAR>hdg : ∀ᶠ (x : ℝ) in atTop, DifferentiableAt ℝ g x<VAR>hdf' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt f (deriv f x) x<VAR>hdg' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt g (deriv g x) x<GOAL>Tendsto (fun x => f x / g x) atTop l
<VAR>n : ℕ<VAR>hn : 0 < n<VAR>a b : ℕ<GOAL>a.Coprime (b ^ n) ↔ a.Coprime b
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>a : α<VAR>l : Thunk (LazyList α)<GOAL>(∀ (x : α), x ∈ cons a l → p x) ↔ p a ∧ ∀ (x : α), x ∈ l.get → p x
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K V : Set G<VAR>hK : IsCompact K<VAR>hV : (interior V).Nonempty<GOAL>∃ t, K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V ∧ t.card = index K V
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K V : Set G<VAR>hK : IsCompact K<VAR>hV : (interior V).Nonempty<VAR>this : sInf (Finset.card '' {t | K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}) ∈ Finset.card '' {t | K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}<GOAL>∃ t, K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V ∧ t.card = index K V
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>i : σ<VAR>f g : MvPolynomial σ R<GOAL>degreeOf i (f * g) ≤ degreeOf i f + degreeOf i g
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x✝ y : G<VAR>n✝ m : ℕ<VAR>x : G<VAR>n : ℕ<GOAL>x ^ (n % orderOf x) = x ^ (n % orderOf x + orderOf x * (n / orderOf x))
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x✝ y : G<VAR>n✝ m : ℕ<VAR>x : G<VAR>n : ℕ<GOAL>x ^ (n % orderOf x + orderOf x * (n / orderOf x)) = x ^ n
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddCommMonoid γ<VAR>S : ι → AddSubmonoid γ<VAR>inst✝ : (i : ι) → (x : ↥(S i)) → Decidable (x ≠ 0)<VAR>x : γ<GOAL>x ∈ iSup S ↔ ∃ f, (f.sum fun i xi => ↑xi) = x
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddCommMonoid γ<VAR>S : ι → AddSubmonoid γ<VAR>inst✝ : (i : ι) → (x : ↥(S i)) → Decidable (x ≠ 0)<VAR>x : γ<GOAL>(∃ f, (sumAddHom fun i => (S i).subtype) f = x) ↔ ∃ f, (f.sum fun i xi => ↑xi) = x
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddCommMonoid γ<VAR>S : ι → AddSubmonoid γ<VAR>inst✝ : (i : ι) → (x : ↥(S i)) → Decidable (x ≠ 0)<VAR>x : γ<GOAL>(∃ f, (f.sum fun x => ⇑(S x).subtype) = x) ↔ ∃ f, (f.sum fun i xi => ↑xi) = x
<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>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ✝ k<VAR>inst✝ : IsDomain R<VAR>ζ : R<VAR>n : ℕ<VAR>h : IsPrimitiveRoot ζ n<GOAL>Multiset.card (nthRoots n 1) = n
<VAR>F : Type u_1<VAR>inst✝¹ : Fintype F<VAR>inst✝ : Field F<VAR>hF : ringChar F ≠ 2<GOAL>2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))
<VAR>F : Type u_1<VAR>inst✝¹ : Fintype F<VAR>inst✝ : Field F<VAR>hF : ringChar F ≠ 2<VAR>hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0<GOAL>2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))
<VAR>F : Type u_1<VAR>inst✝¹ : Fintype F<VAR>inst✝ : Field F<VAR>hF : ringChar F ≠ 2<VAR>hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0<VAR>n : ℕ+<VAR>hp : Nat.Prime (ringChar F)<VAR>hc : Fintype.card F = ringChar F ^ ↑n<GOAL>2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))
<VAR>F : Type u_1<VAR>inst✝¹ : Fintype F<VAR>inst✝ : Field F<VAR>hF : ringChar F ≠ 2<VAR>hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0<VAR>n : ℕ+<VAR>hp : Nat.Prime (ringChar F)<VAR>hc : Fintype.card F = ringChar F ^ ↑n<VAR>FF : Type u_1 := CyclotomicField 8 F<GOAL>2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))
<VAR>F : Type u_1<VAR>inst✝¹ : Fintype F<VAR>inst✝ : Field F<VAR>hF : ringChar F ≠ 2<VAR>hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0<VAR>n : ℕ+<VAR>hp : Nat.Prime (ringChar F)<VAR>hc : Fintype.card F = ringChar F ^ ↑n<VAR>FF : Type u_1 := CyclotomicField 8 F<VAR>hchar : ringChar F = ringChar FF<GOAL>2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))
<VAR>F : Type u_1<VAR>inst✝¹ : Fintype F<VAR>inst✝ : Field F<VAR>hF : ringChar F ≠ 2<VAR>hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0<VAR>n : ℕ+<VAR>hp : Nat.Prime (ringChar F)<VAR>hc : Fintype.card F = ringChar F ^ ↑n<VAR>FF : Type u_1 := CyclotomicField 8 F<VAR>hchar : ringChar F = ringChar FF<VAR>FFp : Nat.Prime (ringChar FF)<GOAL>2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))
<VAR>F : Type u_1<VAR>inst✝¹ : Fintype F<VAR>inst✝ : Field F<VAR>hF : ringChar F ≠ 2<VAR>hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0<VAR>n : ℕ+<VAR>hp : Nat.Prime (ringChar F)<VAR>hc : Fintype.card F = ringChar F ^ ↑n<VAR>FF : Type u_1 := CyclotomicField 8 F<VAR>hchar : ringChar F = ringChar FF<VAR>FFp : Nat.Prime (ringChar FF)<VAR>this : Fact (Nat.Prime (ringChar FF))<VAR>hFF : ringChar FF ≠ 2<GOAL>2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))
<VAR>F : Type u_1<VAR>inst✝¹ : Fintype F<VAR>inst✝ : Field F<VAR>hF : ringChar F ≠ 2<VAR>hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0<VAR>n : ℕ+<VAR>hp : Nat.Prime (ringChar F)<VAR>hc : Fintype.card F = ringChar F ^ ↑n<VAR>FF : Type u_1 := CyclotomicField 8 F<VAR>hchar : ringChar F = ringChar FF<VAR>FFp : Nat.Prime (ringChar FF)<VAR>this : Fact (Nat.Prime (ringChar FF))<VAR>hFF : ringChar FF ≠ 2<VAR>hu : IsUnit ↑(ringChar FF)<GOAL>2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))
<VAR>F : Type u_1<VAR>inst✝¹ : Fintype F<VAR>inst✝ : Field F<VAR>hF : ringChar F ≠ 2<VAR>hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0<VAR>n : ℕ+<VAR>hp : Nat.Prime (ringChar F)<VAR>hc : Fintype.card F = ringChar F ^ ↑n<VAR>FF : Type u_1 := CyclotomicField 8 F<VAR>hchar : ringChar F = ringChar FF<VAR>FFp : Nat.Prime (ringChar FF)<VAR>this : Fact (Nat.Prime (ringChar FF))<VAR>hFF : ringChar FF ≠ 2<VAR>hu : IsUnit ↑(ringChar FF)<VAR>ψ₈ : PrimitiveAddChar (ZMod ↑8) F := primitiveZModChar 8 F ⋯<VAR>ψ₈char : AddChar (ZMod 8) FF := ψ₈.char<VAR>τ : FF := ψ₈char 1<VAR>τ_spec : τ ^ 4 = -1<VAR>χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)<GOAL>2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))
<VAR>F : Type u_1<VAR>inst✝¹ : Fintype F<VAR>inst✝ : Field F<VAR>hF : ringChar F ≠ 2<VAR>hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0<VAR>n : ℕ+<VAR>hp : Nat.Prime (ringChar F)<VAR>hc : Fintype.card F = ringChar F ^ ↑n<VAR>FF : Type u_1 := CyclotomicField 8 F<VAR>hchar : ringChar F = ringChar FF<VAR>FFp : Nat.Prime (ringChar FF)<VAR>this : Fact (Nat.Prime (ringChar FF))<VAR>hFF : ringChar FF ≠ 2<VAR>hu : IsUnit ↑(ringChar FF)<VAR>ψ₈ : PrimitiveAddChar (ZMod ↑8) F := primitiveZModChar 8 F ⋯<VAR>ψ₈char : AddChar (ZMod 8) FF := ψ₈.char<VAR>τ : FF := ψ₈char 1<VAR>τ_spec : τ ^ 4 = -1<VAR>χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)<VAR>hχ : χ (-1) = 1<GOAL>2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))
<VAR>F : Type u_1<VAR>inst✝¹ : Fintype F<VAR>inst✝ : Field F<VAR>hF : ringChar F ≠ 2<VAR>hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0<VAR>n : ℕ+<VAR>hp : Nat.Prime (ringChar F)<VAR>hc : Fintype.card F = ringChar F ^ ↑n<VAR>FF : Type u_1 := CyclotomicField 8 F<VAR>hchar : ringChar F = ringChar FF<VAR>FFp : Nat.Prime (ringChar FF)<VAR>this : Fact (Nat.Prime (ringChar FF))<VAR>hFF : ringChar FF ≠ 2<VAR>hu : IsUnit ↑(ringChar FF)<VAR>ψ₈ : PrimitiveAddChar (ZMod ↑8) F := primitiveZModChar 8 F ⋯<VAR>ψ₈char : AddChar (ZMod 8) FF := ψ₈.char<VAR>τ : FF := ψ₈char 1<VAR>τ_spec : τ ^ 4 = -1<VAR>χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)<VAR>hχ : χ (-1) = 1<VAR>hq : χ.IsQuadratic<GOAL>2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))
<VAR>F : Type u_1<VAR>inst✝¹ : Fintype F<VAR>inst✝ : Field F<VAR>hF : ringChar F ≠ 2<VAR>hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0<VAR>n : ℕ+<VAR>hp : Nat.Prime (ringChar F)<VAR>hc : Fintype.card F = ringChar F ^ ↑n<VAR>FF : Type u_1 := CyclotomicField 8 F<VAR>hchar : ringChar F = ringChar FF<VAR>FFp : Nat.Prime (ringChar FF)<VAR>this : Fact (Nat.Prime (ringChar FF))<VAR>hFF : ringChar FF ≠ 2<VAR>hu : IsUnit ↑(ringChar FF)<VAR>ψ₈ : PrimitiveAddChar (ZMod ↑8) F := primitiveZModChar 8 F ⋯<VAR>ψ₈char : AddChar (ZMod 8) FF := ψ₈.char<VAR>τ : FF := ψ₈char 1<VAR>τ_spec : τ ^ 4 = -1<VAR>χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)<VAR>hχ : χ (-1) = 1<VAR>hq : χ.IsQuadratic<VAR>h₁ : (fun a => ↑(χ₈ a) * τ ^ ↑a) = fun a => χ a * ψ₈char a<GOAL>2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))
<VAR>F : Type u_1<VAR>inst✝¹ : Fintype F<VAR>inst✝ : Field F<VAR>hF : ringChar F ≠ 2<VAR>hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0<VAR>n : ℕ+<VAR>hp : Nat.Prime (ringChar F)<VAR>hc : Fintype.card F = ringChar F ^ ↑n<VAR>FF : Type u_1 := CyclotomicField 8 F<VAR>hchar : ringChar F = ringChar FF<VAR>FFp : Nat.Prime (ringChar FF)<VAR>this : Fact (Nat.Prime (ringChar FF))<VAR>hFF : ringChar FF ≠ 2<VAR>hu : IsUnit ↑(ringChar FF)<VAR>ψ₈ : PrimitiveAddChar (ZMod ↑8) F := primitiveZModChar 8 F ⋯<VAR>ψ₈char : AddChar (ZMod 8) FF := ψ₈.char<VAR>τ : FF := ψ₈char 1<VAR>τ_spec : τ ^ 4 = -1<VAR>χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)<VAR>hχ : χ (-1) = 1<VAR>hq : χ.IsQuadratic<VAR>h₁ : (fun a => ↑(χ₈ a) * τ ^ ↑a) = fun a => χ a * ψ₈char a<VAR>hg₁ : gaussSum χ ψ₈char = 2 * (τ - τ ^ 3)<GOAL>2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))
<VAR>F : Type u_1<VAR>inst✝¹ : Fintype F<VAR>inst✝ : Field F<VAR>hF : ringChar F ≠ 2<VAR>hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0<VAR>n : ℕ+<VAR>hp : Nat.Prime (ringChar F)<VAR>hc : Fintype.card F = ringChar F ^ ↑n<VAR>FF : Type u_1 := CyclotomicField 8 F<VAR>hchar : ringChar F = ringChar FF<VAR>FFp : Nat.Prime (ringChar FF)<VAR>this : Fact (Nat.Prime (ringChar FF))<VAR>hFF : ringChar FF ≠ 2<VAR>hu : IsUnit ↑(ringChar FF)<VAR>ψ₈ : PrimitiveAddChar (ZMod ↑8) F := primitiveZModChar 8 F ⋯<VAR>ψ₈char : AddChar (ZMod 8) FF := ψ₈.char<VAR>τ : FF := ψ₈char 1<VAR>τ_spec : τ ^ 4 = -1<VAR>χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)<VAR>hχ : χ (-1) = 1<VAR>hq : χ.IsQuadratic<VAR>h₁ : (fun a => ↑(χ₈ a) * τ ^ ↑a) = fun a => χ a * ψ₈char a<VAR>hg₁ : gaussSum χ ψ₈char = 2 * (τ - τ ^ 3)<VAR>hg : gaussSum χ ψ₈char ^ 2 = χ (-1) * ↑(Fintype.card (ZMod 8))<GOAL>2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))
<VAR>F : Type u_1<VAR>inst✝¹ : Fintype F<VAR>inst✝ : Field F<VAR>hF : ringChar F ≠ 2<VAR>hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0<VAR>n : ℕ+<VAR>hp : Nat.Prime (ringChar F)<VAR>hc : Fintype.card F = ringChar F ^ ↑n<VAR>FF : Type u_1 := CyclotomicField 8 F<VAR>hchar : ringChar F = ringChar FF<VAR>FFp : Nat.Prime (ringChar FF)<VAR>this : Fact (Nat.Prime (ringChar FF))<VAR>hFF : ringChar FF ≠ 2<VAR>hu : IsUnit ↑(ringChar FF)<VAR>ψ₈ : PrimitiveAddChar (ZMod ↑8) F := primitiveZModChar 8 F ⋯<VAR>ψ₈char : AddChar (ZMod 8) FF := ψ₈.char<VAR>τ : FF := ψ₈char 1<VAR>τ_spec : τ ^ 4 = -1<VAR>χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)<VAR>hχ : χ (-1) = 1<VAR>hq : χ.IsQuadratic<VAR>h₁ : (fun a => ↑(χ₈ a) * τ ^ ↑a) = fun a => χ a * ψ₈char a<VAR>hg₁ : gaussSum χ ψ₈char = 2 * (τ - τ ^ 3)<VAR>hg : gaussSum χ ψ₈char ^ 2 = χ (-1) * ↑(Fintype.card (ZMod 8))<VAR>h : (χ (-1) * ↑(Fintype.card (ZMod 8))) ^ (ringChar FF ^ ↑n / 2) = χ (↑(ringChar FF) ^ ↑n)<GOAL>2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))
<VAR>F : Type u_1<VAR>inst✝¹ : Fintype F<VAR>inst✝ : Field F<VAR>hF : ringChar F ≠ 2<VAR>hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0<VAR>n : ℕ+<VAR>hp : Nat.Prime (ringChar F)<VAR>hc : Fintype.card F = ringChar F ^ ↑n<VAR>FF : Type u_1 := CyclotomicField 8 F<VAR>hchar : ringChar F = ringChar FF<VAR>FFp : Nat.Prime (ringChar FF)<VAR>this : Fact (Nat.Prime (ringChar FF))<VAR>hFF : ringChar FF ≠ 2<VAR>hu : IsUnit ↑(ringChar FF)<VAR>ψ₈ : PrimitiveAddChar (ZMod ↑8) F := primitiveZModChar 8 F ⋯<VAR>ψ₈char : AddChar (ZMod 8) FF := ψ₈.char<VAR>τ : FF := ψ₈char 1<VAR>τ_spec : τ ^ 4 = -1<VAR>χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)<VAR>hχ : χ (-1) = 1<VAR>hq : χ.IsQuadratic<VAR>h₁ : (fun a => ↑(χ₈ a) * τ ^ ↑a) = fun a => χ a * ψ₈char a<VAR>hg₁ : gaussSum χ ψ₈char = 2 * (τ - τ ^ 3)<VAR>hg : gaussSum χ ψ₈char ^ 2 = χ (-1) * ↑(Fintype.card (ZMod 8))<VAR>h : ↑8 ^ (Fintype.card F / 2) = χ ↑(Fintype.card F)<GOAL>2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))
<VAR>F : Type u_1<VAR>inst✝¹ : Fintype F<VAR>inst✝ : Field F<VAR>hF : ringChar F ≠ 2<VAR>hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0<VAR>n : ℕ+<VAR>hp : Nat.Prime (ringChar F)<VAR>hc : Fintype.card F = ringChar F ^ ↑n<VAR>FF : Type u_1 := CyclotomicField 8 F<VAR>hchar : ringChar F = ringChar FF<VAR>FFp : Nat.Prime (ringChar FF)<VAR>this : Fact (Nat.Prime (ringChar FF))<VAR>hFF : ringChar FF ≠ 2<VAR>hu : IsUnit ↑(ringChar FF)<VAR>ψ₈ : PrimitiveAddChar (ZMod ↑8) F := primitiveZModChar 8 F ⋯<VAR>ψ₈char : AddChar (ZMod 8) FF := ψ₈.char<VAR>τ : FF := ψ₈char 1<VAR>τ_spec : τ ^ 4 = -1<VAR>χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)<VAR>hχ : χ (-1) = 1<VAR>hq : χ.IsQuadratic<VAR>h₁ : (fun a => ↑(χ₈ a) * τ ^ ↑a) = fun a => χ a * ψ₈char a<VAR>hg₁ : gaussSum χ ψ₈char = 2 * (τ - τ ^ 3)<VAR>hg : gaussSum χ ψ₈char ^ 2 = χ (-1) * ↑(Fintype.card (ZMod 8))<VAR>h : ↑8 ^ (Fintype.card F / 2) = χ ↑(Fintype.card F)<GOAL>8 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))