ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>I : Type w₀<VAR>J : Type w₁<VAR>C : I → Type u₁<VAR>inst✝² : (i : I) → Category.{v₁, u₁} (C i)<VAR>D : I → Type u₂<VAR>inst✝¹ : (i : I) → Category.{v₂, u₂} (D i)<VAR>A : Type u₃<VAR>inst✝ : Category.{v₃, u₃} A<VAR>f f' : A ⥤ ((i : I) → C i)<VAR>h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i<GOAL>f = f'
<VAR>I : Type w₀<VAR>J : Type w₁<VAR>C : I → Type u₁<VAR>inst✝² : (i : I) → Category.{v₁, u₁} (C i)<VAR>D : I → Type u₂<VAR>inst✝¹ : (i : I) → Category.{v₂, u₂} (D i)<VAR>A : Type u₃<VAR>inst✝ : Category.{v₃, u₃} A<VAR>f f' : A ⥤ ((i : I) → C i)<VAR>h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i<GOAL>autoParam (∀ (X Y : A) (f_1 : X ⟶ Y), f.map f_1 = eqToHom ⋯ ≫ f'.map f_1 ≫ eqToHom ⋯) _auto✝
<VAR>I : Type w₀<VAR>J : Type w₁<VAR>C : I → Type u₁<VAR>inst✝² : (i : I) → Category.{v₁, u₁} (C i)<VAR>D : I → Type u₂<VAR>inst✝¹ : (i : I) → Category.{v₂, u₂} (D i)<VAR>A : Type u₃<VAR>inst✝ : Category.{v₃, u₃} A<VAR>f f' : A ⥤ ((i : I) → C i)<VAR>h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i<GOAL>∀ (X : A), f.obj X = f'.obj X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>s : Set α<VAR>a : ↑s<VAR>t : Set ↑s<GOAL>t ∈ 𝓝 a ↔ Subtype.val '' t ∈ 𝓝[s] ↑a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f✝ g✝ : X → Y<VAR>f g : (i : ι) → π i<GOAL>f ⤳ g ↔ ∀ (i : ι), f i ⤳ g i
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type w'<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>P : Type u_1<VAR>inst✝¹ : L.Structure P<VAR>Q : Type u_2<VAR>inst✝ : L.Structure Q<VAR>f : M ≃[L] N<VAR>x✝ : N<GOAL>(f.comp f.symm) x✝ = (refl L N) x✝
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : Fintype F<VAR>hF : ringChar F ≠ 2<VAR>a : F<VAR>ha : a ≠ 0<GOAL>IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : Fintype F<VAR>hF : ringChar F ≠ 2<VAR>a : F<VAR>ha : a ≠ 0<GOAL>IsSquare (Units.mk0 a ha) ↔ IsSquare a
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : Fintype F<VAR>hF : ringChar F ≠ 2<VAR>a : F<VAR>ha : a ≠ 0<GOAL>(∃ r, a = ↑r * ↑r) ↔ ∃ r, a = r * r
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<VAR>p : PrimeSpectrum ↑R<GOAL>f ≫ toPushforwardStalk f p = (toOpen ↑R ⊤ ≫ (structureSheaf ↑R).presheaf.germ ⟨p, True.intro⟩) ≫ (TopCat.Presheaf.stalkFunctor CommRingCat p).map (Spec.sheafedSpaceMap f).c
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<VAR>p : PrimeSpectrum ↑R<GOAL>f ≫ toPushforwardStalk f p = toOpen ↑R ⊤ ≫ (structureSheaf ↑R).presheaf.germ ⟨p, True.intro⟩ ≫ (TopCat.Presheaf.stalkFunctor CommRingCat p).map (Spec.sheafedSpaceMap f).c
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<VAR>p : PrimeSpectrum ↑R<GOAL>f ≫ toPushforwardStalk f p = toOpen ↑R ⊤ ≫ (Spec.sheafedSpaceMap f).c.app (op ⊤) ≫ ((TopCat.Presheaf.pushforward CommRingCat (Spec.sheafedSpaceMap f).base).obj (Spec.sheafedSpaceObj S).presheaf).germ ⟨p, True.intro⟩
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>x : E<GOAL>(orthogonalProjection K) x = (K.linearProjOfIsCompl Kᗮ ⋯) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>x : E<VAR>this : IsCompl K Kᗮ<GOAL>(orthogonalProjection K) x = (K.linearProjOfIsCompl Kᗮ ⋯) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>x : E<VAR>this : IsCompl K Kᗮ<GOAL>(orthogonalProjection K) (↑((K.linearProjOfIsCompl Kᗮ this) x) + ↑((Kᗮ.linearProjOfIsCompl K ⋯) x)) = (K.linearProjOfIsCompl Kᗮ ⋯) x
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>u : UniformSpace α<VAR>a : α<GOAL>𝓝 a = 𝓝 a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ l₃ : List α<VAR>a b : α<VAR>m n : ℕ<VAR>l : List α<GOAL>l.reverse.inits = (map reverse l.tails).reverse
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ l₃ : List α<VAR>a b : α<VAR>m n : ℕ<VAR>l : List α<GOAL>l.reverse.inits = (map reverse (map reverse l.reverse.inits).reverse).reverse
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<VAR>inst✝ : LocallyFiniteOrderBot α<GOAL>Ico a b ⊆ Iio b
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : Karoubi (ChainComplex C ℕ)<VAR>n : ℕ<GOAL>((((whiskeringLeft (ChainComplex C ℕ) (Karoubi (ChainComplex C ℕ)) (Karoubi (ChainComplex C ℕ))).obj (toKaroubi (ChainComplex C ℕ))).preimage (N₁Γ₀.inv ≫ N₂Γ₂ToKaroubiIso.inv)).app X).f.f n = X.p.f n ≫ ((Γ₀.splitting X.X).cofan (op [n])).inj (Splitting.IndexSet.id (op [n]))
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : Karoubi (ChainComplex C ℕ)<VAR>n : ℕ<GOAL>((𝟭 (Karoubi (ChainComplex C ℕ))).map X.decompId_i).f.f n ≫ X.p.f n ≫ ((Γ₀.splitting X.X).cofan (op [n])).inj (Splitting.IndexSet.id (op [n])) = X.p.f n ≫ ((Γ₀.splitting X.X).cofan (op [n])).inj (Splitting.IndexSet.id (op [n]))
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : Ring 𝕜<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module 𝕜 V<VAR>inst✝¹ : TopologicalSpace P<VAR>inst✝ : AddTorsor V P<VAR>s✝ t : Set P<VAR>x : P<VAR>s : Set P<GOAL>intrinsicInterior 𝕜 s ∪ intrinsicFrontier 𝕜 s = intrinsicClosure 𝕜 s
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>S : Set (Set X)<VAR>hS : Nonempty ↑S<VAR>hSd : DirectedOn (fun x x_1 => x ⊇ x_1) S<VAR>hSn : ∀ U ∈ S, U.Nonempty<VAR>hSc : ∀ U ∈ S, IsCompact U<VAR>hScl : ∀ U ∈ S, IsClosed U<GOAL>(⋂₀ S).Nonempty
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>S : Set (Set X)<VAR>hS : Nonempty ↑S<VAR>hSd : DirectedOn (fun x x_1 => x ⊇ x_1) S<VAR>hSn : ∀ U ∈ S, U.Nonempty<VAR>hSc : ∀ U ∈ S, IsCompact U<VAR>hScl : ∀ U ∈ S, IsClosed U<GOAL>(⋂ i, ↑i).Nonempty
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : X → Y<VAR>hf : Continuous f<GOAL>comap f (cocompact Y) ≤ cocompact X
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : X → Y<VAR>hf : Continuous f<GOAL>∀ (i' : Set X), IsCompact i' → ∃ i, IsCompact i ∧ f ⁻¹' iᶜ ⊆ i'ᶜ
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>f : X → Y<VAR>hf : Continuous f<VAR>t : Set X<VAR>ht : IsCompact t<GOAL>∃ i, IsCompact i ∧ f ⁻¹' iᶜ ⊆ tᶜ
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>f : X → Y<VAR>hf : Continuous f<VAR>t : Set X<VAR>ht : IsCompact t<GOAL>f ⁻¹' (f '' t)ᶜ ⊆ tᶜ
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a : α<GOAL>⌈a⌉ = 0 ↔ a ∈ Ioc (-1) 0
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>r x : ℝ<VAR>hr : 0 < r<VAR>ε : ℝ<VAR>L₁ L₂ : F<VAR>h₁ : x ∈ A f L₁ r ε<VAR>h₂ : x ∈ A f L₂ r ε<GOAL>‖L₁ - L₂‖ ≤ 4 * ε
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>r x : ℝ<VAR>hr : 0 < r<VAR>ε : ℝ<VAR>L₁ L₂ : F<VAR>h₁ : x ∈ A f L₁ r ε<VAR>h₂ : x ∈ A f L₂ r ε<GOAL>‖(r / 2) • (L₁ - L₂)‖ ≤ r / 2 * (4 * ε)
<VAR>x : ℝ<GOAL>sinKernel 0 x = 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Seq α<GOAL>(↑s).head = Computation.pure s.head
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Seq α<GOAL>Computation.pure (Option.map (Prod.fst ∘ fun a => (a, ↑s.tail)) s.head) = Computation.pure s.head
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝ : Zero β<VAR>f : α →ₛ β<VAR>hf : ∀ (y : β), y ≠ 0 → μ (↑f ⁻¹' {y}) < ⊤<GOAL>μ (support ↑f) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝ : Zero β<VAR>f : α →ₛ β<VAR>hf : ∀ (y : β), y ≠ 0 → μ (↑f ⁻¹' {y}) < ⊤<GOAL>μ (⋃ y ∈ filter (fun y => y ≠ 0) f.range, ↑f ⁻¹' {y}) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝ : Zero β<VAR>f : α →ₛ β<VAR>hf : ∀ (y : β), y ≠ 0 → μ (↑f ⁻¹' {y}) < ⊤<VAR>y : β<VAR>hy : y ∈ filter (fun y => y ≠ 0) f.range<GOAL>μ (↑f ⁻¹' {y}) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝ : Zero β<VAR>f : α →ₛ β<VAR>hf : ∀ (y : β), y ≠ 0 → μ (↑f ⁻¹' {y}) < ⊤<VAR>y : β<VAR>hy : y ∈ f.range ∧ y ≠ 0<GOAL>μ (↑f ⁻¹' {y}) < ⊤
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>f : SmoothPartitionOfUnity ι I M s<VAR>n : ℕ∞<VAR>x₀ : M<VAR>g : ι → M → F<VAR>hφ : ∀ (i : ι), x₀ ∈ tsupport ⇑(f i) → ContMDiffAt I 𝓘(ℝ, F) n (g i) x₀<GOAL>ContMDiffAt I 𝓘(ℝ, F) n (fun x => ∑ᶠ (i : ι), (f i) x • g i x) x₀
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>f : SmoothPartitionOfUnity ι I M s<VAR>n : ℕ∞<VAR>x₀ : M<VAR>g : ι → M → F<VAR>hφ : ∀ (i : ι), x₀ ∈ tsupport ⇑(f i) → ContMDiffAt I 𝓘(ℝ, F) n (g i) x₀<VAR>i : ι<GOAL>ContMDiffAt I 𝓘(ℝ, F) n (fun x => (f i) x • g i x) x₀
<VAR>a✝ b c d m n a : ℤ<GOAL>(-a.succ).succ = -a
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>i : α<GOAL>Tendsto (r i) atTop atTop
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>i : α<GOAL>∀ (b : ℕ), ∀ᶠ (a : ℕ) in atTop, b ≤ r i a
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b✝ : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b✝ r<VAR>i : α<VAR>b : ℕ<GOAL>∀ᶠ (a : ℕ) in atTop, b ≤ r i a
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b✝ : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b✝ r<VAR>i : α<VAR>b : ℕ<VAR>this : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑b ≤ ↑(r i n)<GOAL>∀ᶠ (a : ℕ) in atTop, b ≤ r i a
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b✝ : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b✝ r<VAR>i : α<VAR>b : ℕ<VAR>this : ∀ (i : α), ∀ᶠ (x : ℕ) in atTop, ↑b ≤ ↑(r i x)<GOAL>∀ᶠ (a : ℕ) in atTop, b ≤ r i a
<VAR>P : ℕ → Sort u_1<VAR>h0 : P 0<VAR>h_even : (i : ℕ) → P i → P (2 * i)<VAR>h_odd : (i : ℕ) → P i → P (2 * i + 1)<VAR>H : h_even 0 h0 = h0<VAR>n : ℕ<GOAL>evenOddRec h0 h_even h_odd (2 * n + 1) = h_odd n (evenOddRec h0 h_even h_odd n)
<VAR>P : ℕ → Sort u_1<VAR>h0 : P 0<VAR>h_even : (i : ℕ) → P i → P (2 * i)<VAR>h_odd : (i : ℕ) → P i → P (2 * i + 1)<VAR>H : h_even 0 h0 = h0<VAR>n : ℕ<GOAL>(match false, 0, h0 with | false, i, hi => h_even i hi | true, i, hi => h_odd i hi) = h0 ∨ (n = 0 → true = true)
<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<GOAL>λ ^ 2 ∣ S'.a + S'.b ∨ λ ^ 2 ∣ S'.a + ↑η * S'.b ∨ λ ^ 2 ∣ S'.a + ↑η ^ 2 * S'.b
<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 : ¬λ ^ 2 ∣ S'.a + S'.b ∧ ¬λ ^ 2 ∣ S'.a + ↑η * S'.b ∧ ¬λ ^ 2 ∣ 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>h1 : ¬λ ^ 2 ∣ S'.a + S'.b<VAR>h2 : ¬λ ^ 2 ∣ S'.a + ↑η * S'.b<VAR>h3 : ¬λ ^ 2 ∣ 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>h1 : multiplicity λ (S'.a + S'.b) < ↑2<VAR>h2 : multiplicity λ (S'.a + ↑η * S'.b) < ↑2<VAR>h3 : multiplicity λ (S'.a + ↑η ^ 2 * S'.b) < ↑2<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>h1 : multiplicity λ (S'.a + S'.b) < ↑2<VAR>h2 : multiplicity λ (S'.a + ↑η * S'.b) < ↑2<VAR>h3 : multiplicity λ (S'.a + ↑η ^ 2 * S'.b) < ↑2<VAR>h1' : multiplicity.Finite λ (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>h1 : multiplicity λ (S'.a + S'.b) < ↑2<VAR>h2 : multiplicity λ (S'.a + ↑η * S'.b) < ↑2<VAR>h3 : multiplicity λ (S'.a + ↑η ^ 2 * S'.b) < ↑2<VAR>h1' : multiplicity.Finite λ (S'.a + S'.b)<VAR>h2' : multiplicity.Finite λ (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>h1 : multiplicity λ (S'.a + S'.b) < ↑2<VAR>h2 : multiplicity λ (S'.a + ↑η * S'.b) < ↑2<VAR>h3 : multiplicity λ (S'.a + ↑η ^ 2 * S'.b) < ↑2<VAR>h1' : multiplicity.Finite λ (S'.a + S'.b)<VAR>h2' : multiplicity.Finite λ (S'.a + ↑η * S'.b)<VAR>h3' : multiplicity.Finite λ (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>h1 : multiplicity λ (S'.a + S'.b) < ↑2<VAR>h2 : multiplicity λ (S'.a + ↑η * S'.b) < ↑2<VAR>h3 : multiplicity λ (S'.a + ↑η ^ 2 * S'.b) < ↑2<VAR>h1'✝ : multiplicity.Finite λ (S'.a + S'.b)<VAR>h2' : multiplicity.Finite λ (S'.a + ↑η * S'.b)<VAR>h3' : multiplicity.Finite λ (S'.a + ↑η ^ 2 * S'.b)<VAR>h1' : ↑((multiplicity λ (S'.a + S'.b)).get h1'✝) = multiplicity λ (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>h1 : multiplicity λ (S'.a + S'.b) < ↑2<VAR>h2 : multiplicity λ (S'.a + ↑η * S'.b) < ↑2<VAR>h3 : multiplicity λ (S'.a + ↑η ^ 2 * S'.b) < ↑2<VAR>h1'✝ : multiplicity.Finite λ (S'.a + S'.b)<VAR>h2'✝ : multiplicity.Finite λ (S'.a + ↑η * S'.b)<VAR>h3' : multiplicity.Finite λ (S'.a + ↑η ^ 2 * S'.b)<VAR>h1' : ↑((multiplicity λ (S'.a + S'.b)).get h1'✝) = multiplicity λ (S'.a + S'.b)<VAR>h2' : ↑((multiplicity λ (S'.a + ↑η * S'.b)).get h2'✝) = multiplicity λ (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>h1 : multiplicity λ (S'.a + S'.b) < ↑2<VAR>h2 : multiplicity λ (S'.a + ↑η * S'.b) < ↑2<VAR>h3 : multiplicity λ (S'.a + ↑η ^ 2 * S'.b) < ↑2<VAR>h1'✝ : multiplicity.Finite λ (S'.a + S'.b)<VAR>h2'✝ : multiplicity.Finite λ (S'.a + ↑η * S'.b)<VAR>h3'✝ : multiplicity.Finite λ (S'.a + ↑η ^ 2 * S'.b)<VAR>h1' : ↑((multiplicity λ (S'.a + S'.b)).get h1'✝) = multiplicity λ (S'.a + S'.b)<VAR>h2' : ↑((multiplicity λ (S'.a + ↑η * S'.b)).get h2'✝) = multiplicity λ (S'.a + ↑η * S'.b)<VAR>h3' : ↑((multiplicity λ (S'.a + ↑η ^ 2 * S'.b)).get h3'✝) = multiplicity λ (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>h2 : multiplicity λ (S'.a + ↑η * S'.b) < ↑2<VAR>h3 : multiplicity λ (S'.a + ↑η ^ 2 * S'.b) < ↑2<VAR>h1'✝ : multiplicity.Finite λ (S'.a + S'.b)<VAR>h1 : (multiplicity λ (S'.a + S'.b)).get h1'✝ < 2<VAR>h2'✝ : multiplicity.Finite λ (S'.a + ↑η * S'.b)<VAR>h3'✝ : multiplicity.Finite λ (S'.a + ↑η ^ 2 * S'.b)<VAR>h1' : ↑((multiplicity λ (S'.a + S'.b)).get h1'✝) = multiplicity λ (S'.a + S'.b)<VAR>h2' : ↑((multiplicity λ (S'.a + ↑η * S'.b)).get h2'✝) = multiplicity λ (S'.a + ↑η * S'.b)<VAR>h3' : ↑((multiplicity λ (S'.a + ↑η ^ 2 * S'.b)).get h3'✝) = multiplicity λ (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>h3 : multiplicity λ (S'.a + ↑η ^ 2 * S'.b) < ↑2<VAR>h1'✝ : multiplicity.Finite λ (S'.a + S'.b)<VAR>h1 : (multiplicity λ (S'.a + S'.b)).get h1'✝ < 2<VAR>h2'✝ : multiplicity.Finite λ (S'.a + ↑η * S'.b)<VAR>h2 : (multiplicity λ (S'.a + ↑η * S'.b)).get h2'✝ < 2<VAR>h3'✝ : multiplicity.Finite λ (S'.a + ↑η ^ 2 * S'.b)<VAR>h1' : ↑((multiplicity λ (S'.a + S'.b)).get h1'✝) = multiplicity λ (S'.a + S'.b)<VAR>h2' : ↑((multiplicity λ (S'.a + ↑η * S'.b)).get h2'✝) = multiplicity λ (S'.a + ↑η * S'.b)<VAR>h3' : ↑((multiplicity λ (S'.a + ↑η ^ 2 * S'.b)).get h3'✝) = multiplicity λ (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>h1'✝ : multiplicity.Finite λ (S'.a + S'.b)<VAR>h1 : (multiplicity λ (S'.a + S'.b)).get h1'✝ < 2<VAR>h2'✝ : multiplicity.Finite λ (S'.a + ↑η * S'.b)<VAR>h2 : (multiplicity λ (S'.a + ↑η * S'.b)).get h2'✝ < 2<VAR>h3'✝ : multiplicity.Finite λ (S'.a + ↑η ^ 2 * S'.b)<VAR>h3 : (multiplicity λ (S'.a + ↑η ^ 2 * S'.b)).get h3'✝ < 2<VAR>h1' : ↑((multiplicity λ (S'.a + S'.b)).get h1'✝) = multiplicity λ (S'.a + S'.b)<VAR>h2' : ↑((multiplicity λ (S'.a + ↑η * S'.b)).get h2'✝) = multiplicity λ (S'.a + ↑η * S'.b)<VAR>h3' : ↑((multiplicity λ (S'.a + ↑η ^ 2 * S'.b)).get h3'✝) = multiplicity λ (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>h1'✝ : multiplicity.Finite λ (S'.a + S'.b)<VAR>h1 : (multiplicity λ (S'.a + S'.b)).get h1'✝ < 2<VAR>h2'✝ : multiplicity.Finite λ (S'.a + ↑η * S'.b)<VAR>h2 : (multiplicity λ (S'.a + ↑η * S'.b)).get h2'✝ < 2<VAR>h3'✝ : multiplicity.Finite λ (S'.a + ↑η ^ 2 * S'.b)<VAR>h3 : (multiplicity λ (S'.a + ↑η ^ 2 * S'.b)).get h3'✝ < 2<VAR>h1' : ↑((multiplicity λ (S'.a + S'.b)).get h1'✝) = multiplicity λ (S'.a + S'.b)<VAR>h2' : ↑((multiplicity λ (S'.a + ↑η * S'.b)).get h2'✝) = multiplicity λ (S'.a + ↑η * S'.b)<VAR>h3' : ↑((multiplicity λ (S'.a + ↑η ^ 2 * S'.b)).get h3'✝) = multiplicity λ (S'.a + ↑η ^ 2 * S'.b)<VAR>this : (λ ^ 2) ^ 3 ∣ ↑S'.u * S'.c ^ 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>h1'✝ : multiplicity.Finite λ (S'.a + S'.b)<VAR>h1 : (multiplicity λ (S'.a + S'.b)).get h1'✝ < 2<VAR>h2'✝ : multiplicity.Finite λ (S'.a + ↑η * S'.b)<VAR>h2 : (multiplicity λ (S'.a + ↑η * S'.b)).get h2'✝ < 2<VAR>h3'✝ : multiplicity.Finite λ (S'.a + ↑η ^ 2 * S'.b)<VAR>h3 : (multiplicity λ (S'.a + ↑η ^ 2 * S'.b)).get h3'✝ < 2<VAR>h1' : ↑((multiplicity λ (S'.a + S'.b)).get h1'✝) = multiplicity λ (S'.a + S'.b)<VAR>h2' : ↑((multiplicity λ (S'.a + ↑η * S'.b)).get h2'✝) = multiplicity λ (S'.a + ↑η * S'.b)<VAR>h3' : ↑((multiplicity λ (S'.a + ↑η ^ 2 * S'.b)).get h3'✝) = multiplicity λ (S'.a + ↑η ^ 2 * S'.b)<VAR>this : 2 * 3 ≤ (multiplicity λ (S'.a + S'.b)).get h1'✝ + (multiplicity λ (S'.a + ↑η * S'.b)).get h2'✝ + (multiplicity λ (S'.a + ↑η ^ 2 * S'.b)).get h3'✝<GOAL>False
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>r : α → α → Prop<VAR>x y : F α<VAR>a : (P F).A<VAR>f₀ f₁ : (P F).B a → α<VAR>xeq : x = abs ⟨a, f₀⟩<VAR>yeq : y = abs ⟨a, f₁⟩<VAR>h : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)<GOAL>Liftr r x y
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>r : α → α → Prop<VAR>x y : F α<VAR>a : (P F).A<VAR>f₀ f₁ : (P F).B a → α<VAR>xeq : x = abs ⟨a, f₀⟩<VAR>yeq : y = abs ⟨a, f₁⟩<VAR>h : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)<GOAL>(fun t => (↑t).1) <$> abs ⟨a, fun i => ⟨(f₀ i, f₁ i), ⋯⟩⟩ = x ∧ (fun t => (↑t).2) <$> abs ⟨a, fun i => ⟨(f₀ i, f₁ i), ⋯⟩⟩ = y
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>r : α → α → Prop<VAR>x y : F α<VAR>a : (P F).A<VAR>f₀ f₁ : (P F).B a → α<VAR>xeq : x = abs ⟨a, f₀⟩<VAR>yeq : y = abs ⟨a, f₁⟩<VAR>h : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)<GOAL>(fun t => (↑t).2) <$> abs ⟨a, fun i => ⟨(f₀ i, f₁ i), ⋯⟩⟩ = y
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>r : α → α → Prop<VAR>x y : F α<VAR>a : (P F).A<VAR>f₀ f₁ : (P F).B a → α<VAR>xeq : x = abs ⟨a, f₀⟩<VAR>yeq : y = abs ⟨a, f₁⟩<VAR>h : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)<GOAL>abs ((P F).map (fun t => (↑t).2) ⟨a, fun i => ⟨(f₀ i, f₁ i), ⋯⟩⟩) = abs ⟨a, f₁⟩
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>hi : I.radical.IsMaximal<VAR>this : I.radical = I.jacobson<VAR>x y : R<VAR>hxy : x * y ∈ I<VAR>x✝ : ∃ y_1, y_1 * y - 1 ∈ I<VAR>z : R<VAR>hz : z * y - 1 ∈ I<GOAL>x ∈ I
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>hi : I.radical.IsMaximal<VAR>this : I.radical = I.jacobson<VAR>x y : R<VAR>hxy : x * y ∈ I<VAR>x✝ : ∃ y_1, y_1 * y - 1 ∈ I<VAR>z : R<VAR>hz : z * y - 1 ∈ I<GOAL>z * (x * y) - x * (z * y - 1) ∈ I