ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>d : ℤ<VAR>h₀ : 0 < d<GOAL>(∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0) ↔ ¬IsSquare d
<VAR>d : ℤ<VAR>h₀ : 0 < d<GOAL>(∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0) → ¬IsSquare d
<VAR>x y : ℤ<VAR>hy : y ≠ 0<VAR>a : ℤ<VAR>h₀ : 0 < a * a<VAR>hxy : x ^ 2 - a * a * y ^ 2 = 1<GOAL>False
<VAR>x y : ℤ<VAR>hy : y ≠ 0<VAR>a : ℤ<VAR>h₀ : 0 < a * a<VAR>hxy : (x + a * y) * (x - a * y) = 1<GOAL>False
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>U : Opens ↑↑X<GOAL>(Opens.map f.base).op.obj (op ((opensFunctor f).obj U)) = op U
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>U : Opens ↑↑X<GOAL>inv (invApp f U) = f.c.app (op ((opensFunctor f).obj U)) ≫ X.presheaf.map (eqToHom ⋯)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>U : Opens ↑↑X<GOAL>𝟙 (X.presheaf.obj (op U)) = invApp f U ≫ f.c.app (op ((opensFunctor f).obj U)) ≫ X.presheaf.map (eqToHom ⋯)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>U : Opens ↑↑X<GOAL>𝟙 (X.presheaf.obj (op U)) = (X.presheaf.map (eqToHom ⋯) ≫ inv (f.c.app (op ((opensFunctor f).obj U)))) ≫ f.c.app (op ((opensFunctor f).obj U)) ≫ X.presheaf.map (eqToHom ⋯)
<VAR>R : Type u_1<VAR>K : Type u_3<VAR>L : Type ?u.74540<VAR>S : Type u_2<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>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsIntegrallyClosed R<VAR>inst✝⁴ : IsDomain S<VAR>inst✝³ : Algebra R K<VAR>inst✝² : Algebra K S<VAR>inst✝¹ : IsScalarTower R K S<VAR>inst✝ : IsFractionRing R K<GOAL>map (algebraMap R S) (minpoly R x) /ₘ (X - C x) = map (algebraMap K S) (minpoly K x) /ₘ (X - C x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : SeminormedRing α<VAR>a b : α<VAR>l : List α<VAR>x✝ : a :: b :: l ≠ []<GOAL>‖(a :: b :: l).prod‖ ≤ (map norm (a :: b :: l)).prod
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : SeminormedRing α<VAR>a b : α<VAR>l : List α<VAR>x✝ : a :: b :: l ≠ []<GOAL>‖a * (b :: l).prod‖ ≤ ‖a‖ * (map norm (b :: l)).prod
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : SeminormedRing α<VAR>a b : α<VAR>l : List α<VAR>x✝ : a :: b :: l ≠ []<GOAL>‖(b :: l).prod‖ ≤ (map norm (b :: l)).prod
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁵ : TopologicalSpace X<VAR>m : MeasurableSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : T2Space Y<VAR>μ ν : Measure X<VAR>inst✝² : μ.IsOpenPosMeasure<VAR>s U F : Set X<VAR>x : X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>inst✝ : IsFiniteMeasure μ<VAR>hF : IsClosed F<GOAL>μ F = μ univ ↔ F = univ
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : IsNoetherianRing R<GOAL>finrank (ResidueField R) (CotangentSpace R) = 0 ↔ IsField R
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>f' : ℝ → E<VAR>C : ℝ<VAR>hf : ∀ x ∈ Icc 0 1, HasDerivWithinAt f (f' x) (Icc 0 1) x<VAR>bound : ∀ x ∈ Ico 0 1, ‖f' x‖ ≤ C<GOAL>‖f 1 - f 0‖ ≤ C
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v s t : Finset α<VAR>hP : P.IsEquipartition<VAR>hε : 0 ≤ ε<GOAL>↑((P.sparsePairs G ε).biUnion fun x => match x with | (U, V) => G.interedges U V).card ≤ 4 * ε * ↑A.card ^ 2
<VAR>r : ℝ<VAR>hr : 0 < r<VAR>x : ℝ<GOAL>↑(exponentialCDFReal r) x = if 0 ≤ x then 1 - rexp (-(r * x)) else 0
<VAR>r : ℝ<VAR>hr : 0 < r<VAR>x : ℝ<GOAL>0 ≤ if 0 ≤ x then 1 - rexp (-(r * x)) else 0
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u_1<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>s : R<VAR>x y : A<GOAL>x * s • y = s • (x * y)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f g : α → β<VAR>μ ν : Measure α<GOAL>AEMeasurable f (μ + ν) ↔ AEMeasurable f μ ∧ AEMeasurable f ν
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f g : α → β<VAR>μ ν : Measure α<GOAL>AEMeasurable f (bif true then μ else ν) ∧ AEMeasurable f (bif false then μ else ν) ↔ AEMeasurable f μ ∧ AEMeasurable f ν
<VAR>R : Type u_1<VAR>inst✝³ : Monoid R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddMonoid X<VAR>inst✝ : DistribMulAction R X<VAR>r r' : X<VAR>s s' : ↥S<VAR>rb sb : R<VAR>h : sb * ↑s = rb * ↑s'<VAR>h' : sb * ↑s ∈ S<GOAL>r /ₒ s + r' /ₒ s' = (sb • r + rb • r') /ₒ ⟨sb * ↑s, h'⟩
<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>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>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>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>hg : MDifferentiableWithinAt I' I'' g u (f x)<VAR>hf : MDifferentiableWithinAt I I' f s x<VAR>h : s ⊆ f ⁻¹' u<VAR>hxs : UniqueMDiffWithinAt I s x<GOAL>mfderivWithin I I'' (g ∘ f) s x = (mfderivWithin I' I'' g u (f x)).comp (mfderivWithin I I' f s x)
<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>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>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>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>hg : MDifferentiableWithinAt I' I'' g u (f x)<VAR>hf : MDifferentiableWithinAt I I' f s x<VAR>h : s ⊆ f ⁻¹' u<VAR>hxs : UniqueMDiffWithinAt I s x<GOAL>HasMFDerivWithinAt I I'' (g ∘ f) s x ((mfderivWithin I' I'' g u (f x)).comp (mfderivWithin I I' f s x))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<GOAL>(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPoly p n) = frobeniusPolyRat p n
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<GOAL>X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) = (bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ n)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<GOAL>∀ (n : ℕ), (∀ m < n, X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) = (bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)) → X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) = (bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ n)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<VAR>IH : ∀ m < n, X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) = (bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)<GOAL>X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) = (bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ n)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<VAR>IH : ∀ m < n, X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) = (bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)<GOAL>X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) = (bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) ((X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) * C (⅟↑p ^ n))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<VAR>IH : ∀ m < n, X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) = (bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)<GOAL>X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) = ((bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (X n) - ∑ x ∈ range n, C (↑p ^ x) * (bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) * C (⅟↑p ^ n)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<VAR>IH : ∀ m < n, X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) = (bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)<VAR>h1 : ↑p ^ n * ⅟↑p ^ n = 1<GOAL>X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) = ((bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (X n) - ∑ x ∈ range n, C (↑p ^ x) * (bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) * C (⅟↑p ^ n)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<VAR>IH : ∀ m < n, X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) = (bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)<VAR>h1 : ↑p ^ n * ⅟↑p ^ n = 1<GOAL>(∑ x ∈ range n, C (↑p ^ x) * (bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) * C (⅟↑p ^ n) - (∑ x ∈ range n, C (↑p ^ x) * X x ^ p ^ (n + 1 - x)) * C (⅟↑p ^ n) = C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (∑ i ∈ range n, ∑ j ∈ range (p ^ (n - i)), (X i ^ p) ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) * C ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p ⟨j + 1, ⋯⟩) * p ^ (j - v p ⟨j + 1, ⋯⟩)))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<VAR>IH : ∀ m < n, X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) = (bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)<VAR>h1 : ↑p ^ n * ⅟↑p ^ n = 1<GOAL>∑ x ∈ range n, (C (↑p ^ x) * (bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x) * C (⅟↑p ^ n) - C (↑p ^ x) * X x ^ p ^ (n + 1 - x) * C (⅟↑p ^ n)) = ∑ x ∈ range n, ∑ i ∈ range (p ^ (n - x)), C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) ((X x ^ p) ^ (p ^ (n - x) - (i + 1)) * frobeniusPolyAux p x ^ (i + 1) * C ↑((p ^ (n - x)).choose (i + 1) / p ^ (n - x - v p ⟨i + 1, ⋯⟩) * p ^ (i - v p ⟨i + 1, ⋯⟩)))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<VAR>IH : ∀ m < n, X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) = (bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)<VAR>h1 : ↑p ^ n * ⅟↑p ^ n = 1<GOAL>∀ x ∈ range n, C (↑p ^ x) * (bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x) * C (⅟↑p ^ n) - C (↑p ^ x) * X x ^ p ^ (n + 1 - x) * C (⅟↑p ^ n) = ∑ i ∈ range (p ^ (n - x)), C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) ((X x ^ p) ^ (p ^ (n - x) - (i + 1)) * frobeniusPolyAux p x ^ (i + 1) * C ↑((p ^ (n - x)).choose (i + 1) / p ^ (n - x - v p ⟨i + 1, ⋯⟩) * p ^ (i - v p ⟨i + 1, ⋯⟩)))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<VAR>IH : ∀ m < n, X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) = (bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)<VAR>h1 : ↑p ^ n * ⅟↑p ^ n = 1<VAR>i : ℕ<VAR>hi : i ∈ range n<GOAL>C (↑p ^ i) * (bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ i) ^ p ^ (n - i) * C (⅟↑p ^ n) - C (↑p ^ i) * X i ^ p ^ (n + 1 - i) * C (⅟↑p ^ n) = ∑ i_1 ∈ range (p ^ (n - i)), C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) ((X i ^ p) ^ (p ^ (n - i) - (i_1 + 1)) * frobeniusPolyAux p i ^ (i_1 + 1) * C ↑((p ^ (n - i)).choose (i_1 + 1) / p ^ (n - i - v p ⟨i_1 + 1, ⋯⟩) * p ^ (i_1 - v p ⟨i_1 + 1, ⋯⟩)))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<VAR>IH : ∀ m < n, X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) = (bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)<VAR>h1 : ↑p ^ n * ⅟↑p ^ n = 1<VAR>i : ℕ<VAR>hi : i < n<GOAL>C (↑p ^ i) * (bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ i) ^ p ^ (n - i) * C (⅟↑p ^ n) - C (↑p ^ i) * X i ^ p ^ (n + 1 - i) * C (⅟↑p ^ n) = ∑ i_1 ∈ range (p ^ (n - i)), C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) ((X i ^ p) ^ (p ^ (n - i) - (i_1 + 1)) * frobeniusPolyAux p i ^ (i_1 + 1) * C ↑((p ^ (n - i)).choose (i_1 + 1) / p ^ (n - i - v p ⟨i_1 + 1, ⋯⟩) * p ^ (i_1 - v p ⟨i_1 + 1, ⋯⟩)))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<VAR>h1 : ↑p ^ n * ⅟↑p ^ n = 1<VAR>i : ℕ<VAR>hi : i < n<GOAL>C (↑p ^ i) * (X i ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i)) ^ p ^ (n - i) * C (⅟↑p ^ n) - C (↑p ^ i) * X i ^ p ^ (n + 1 - i) * C (⅟↑p ^ n) = ∑ i_1 ∈ range (p ^ (n - i)), C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) ((X i ^ p) ^ (p ^ (n - i) - (i_1 + 1)) * frobeniusPolyAux p i ^ (i_1 + 1) * C ↑((p ^ (n - i)).choose (i_1 + 1) / p ^ (n - i - v p ⟨i_1 + 1, ⋯⟩) * p ^ (i_1 - v p ⟨i_1 + 1, ⋯⟩)))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<VAR>h1 : ↑p ^ n * ⅟↑p ^ n = 1<VAR>i : ℕ<VAR>hi : i < n<GOAL>∑ i_1 ∈ range (p ^ (n - i)), C (↑p ^ i) * ((C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i)) ^ (i_1 + 1) * (X i ^ p) ^ (p ^ (n - i) - (i_1 + 1)) * ↑((p ^ (n - i)).choose (i_1 + 1))) * C (⅟↑p ^ n) = ∑ i_1 ∈ range (p ^ (n - i)), C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) ((X i ^ p) ^ (p ^ (n - i) - (i_1 + 1)) * frobeniusPolyAux p i ^ (i_1 + 1) * C ↑((p ^ (n - i)).choose (i_1 + 1) / p ^ (n - i - v p ⟨i_1 + 1, ⋯⟩) * p ^ (i_1 - v p ⟨i_1 + 1, ⋯⟩)))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<VAR>h1 : ↑p ^ n * ⅟↑p ^ n = 1<VAR>i : ℕ<VAR>hi : i < n<GOAL>∀ x ∈ range (p ^ (n - i)), C (↑p ^ i) * ((C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i)) ^ (x + 1) * (X i ^ p) ^ (p ^ (n - i) - (x + 1)) * ↑((p ^ (n - i)).choose (x + 1))) * C (⅟↑p ^ n) = C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) ((X i ^ p) ^ (p ^ (n - i) - (x + 1)) * frobeniusPolyAux p i ^ (x + 1) * C ↑((p ^ (n - i)).choose (x + 1) / p ^ (n - i - v p ⟨x + 1, ⋯⟩) * p ^ (x - v p ⟨x + 1, ⋯⟩)))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<VAR>h1 : ↑p ^ n * ⅟↑p ^ n = 1<VAR>i : ℕ<VAR>hi : i < n<VAR>j : ℕ<VAR>hj : j ∈ range (p ^ (n - i))<GOAL>C (↑p ^ i) * ((C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i)) ^ (j + 1) * (X i ^ p) ^ (p ^ (n - i) - (j + 1)) * ↑((p ^ (n - i)).choose (j + 1))) * C (⅟↑p ^ n) = C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) ((X i ^ p) ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) * C ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p ⟨j + 1, ⋯⟩) * p ^ (j - v p ⟨j + 1, ⋯⟩)))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<VAR>h1 : ↑p ^ n * ⅟↑p ^ n = 1<VAR>i : ℕ<VAR>hi : i < n<VAR>j : ℕ<VAR>hj : j < p ^ (n - i)<GOAL>C (↑p ^ i) * ((C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i)) ^ (j + 1) * (X i ^ p) ^ (p ^ (n - i) - (j + 1)) * ↑((p ^ (n - i)).choose (j + 1))) * C (⅟↑p ^ n) = C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) ((X i ^ p) ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) * C ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p ⟨j + 1, ⋯⟩) * p ^ (j - v p ⟨j + 1, ⋯⟩)))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<VAR>h1 : ↑p ^ n * ⅟↑p ^ n = 1<VAR>i : ℕ<VAR>hi : i < n<VAR>j : ℕ<VAR>hj : j < p ^ (n - i)<GOAL>C ↑p ^ i * (C ↑p ^ (j + 1) * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) * (X i ^ p) ^ (p ^ (n - i) - (j + 1)) * ↑((p ^ (n - i)).choose (j + 1))) * C ⅟↑p ^ n = C ↑p * ((X i ^ p) ^ (p ^ (n - i) - (j + 1)) * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) * C ((Int.castRingHom ℚ) ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p ⟨j + 1, ⋯⟩) * p ^ (j - v p ⟨j + 1, ⋯⟩))))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<VAR>h1 : ↑p ^ n * ⅟↑p ^ n = 1<VAR>i : ℕ<VAR>hi : i < n<VAR>j : ℕ<VAR>hj : j < p ^ (n - i)<GOAL>(X i ^ p) ^ (p ^ (n - i) - (j + 1)) * ((MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) * C ↑p ^ (j + 1)) * ↑((p ^ (n - i)).choose (j + 1)) * C ↑p ^ i * C ⅟↑p ^ n = (X i ^ p) ^ (p ^ (n - i) - (j + 1)) * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) * C ((Int.castRingHom ℚ) ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p ⟨j + 1, ⋯⟩) * p ^ (j - v p ⟨j + 1, ⋯⟩))) * C ↑p
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<VAR>h1 : ↑p ^ n * ⅟↑p ^ n = 1<VAR>i : ℕ<VAR>hi : i < n<VAR>j : ℕ<VAR>hj : j < p ^ (n - i)<GOAL>(X i ^ p) ^ (p ^ (n - i) - (j + 1)) * ((MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) * (C ↑p ^ (j + 1) * (↑((p ^ (n - i)).choose (j + 1)) * (C ↑p ^ i * C ⅟↑p ^ n)))) = (X i ^ p) ^ (p ^ (n - i) - (j + 1)) * ((MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) * (C ((Int.castRingHom ℚ) ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p ⟨j + 1, ⋯⟩) * p ^ (j - v p ⟨j + 1, ⋯⟩))) * C ↑p))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<VAR>h1 : ↑p ^ n * ⅟↑p ^ n = 1<VAR>i : ℕ<VAR>hi : i < n<VAR>j : ℕ<VAR>hj : j < p ^ (n - i)<GOAL>C ↑p ^ (j + 1) * (↑((p ^ (n - i)).choose (j + 1)) * (C ↑p ^ i * C ⅟↑p ^ n)) = C ((Int.castRingHom ℚ) ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p ⟨j + 1, ⋯⟩) * p ^ (j - v p ⟨j + 1, ⋯⟩))) * C ↑p
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<VAR>h1 : ↑p ^ n * ⅟↑p ^ n = 1<VAR>i : ℕ<VAR>hi : i < n<VAR>j : ℕ<VAR>hj : j < p ^ (n - i)<GOAL>C ↑p ^ (j + 1) * (C ↑((p ^ (n - i)).choose (j + 1)) * (C ↑p ^ i * C ⅟↑p ^ n)) = C ((Int.castRingHom ℚ) ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p ⟨j + 1, ⋯⟩) * p ^ (j - v p ⟨j + 1, ⋯⟩))) * C ↑p
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<VAR>h1 : ↑p ^ n * ⅟↑p ^ n = 1<VAR>i : ℕ<VAR>hi : i < n<VAR>j : ℕ<VAR>hj : j < p ^ (n - i)<GOAL>C (↑p ^ (j + 1) * (↑((p ^ (n - i)).choose (j + 1)) * (↑p ^ i * ⅟↑p ^ n))) = C ((Int.castRingHom ℚ) ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p ⟨j + 1, ⋯⟩) * p ^ (j - v p ⟨j + 1, ⋯⟩)) * ↑p)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<VAR>h1 : ↑p ^ n * ⅟↑p ^ n = 1<VAR>i : ℕ<VAR>hi : i < n<VAR>j : ℕ<VAR>hj : j < p ^ (n - i)<GOAL>↑p ^ (j + 1) * (↑((p ^ (n - i)).choose (j + 1)) * (↑p ^ i * ⅟↑p ^ n)) = (Int.castRingHom ℚ) ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p ⟨j + 1, ⋯⟩) * p ^ (j - v p ⟨j + 1, ⋯⟩)) * ↑p
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<VAR>h1 : ↑p ^ n * ⅟↑p ^ n = 1<VAR>i : ℕ<VAR>hi : i < n<VAR>j : ℕ<VAR>hj : j < p ^ (n - i)<GOAL>↑p ^ (j + 1) * (↑((p ^ (n - i)).choose (j + 1)) * (↑p ^ i * (↑p ^ n)⁻¹)) = ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p ⟨j + 1, ⋯⟩)) * ↑(p ^ (j - v p ⟨j + 1, ⋯⟩)) * ↑p
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<VAR>h1 : ↑p ^ n * ⅟↑p ^ n = 1<VAR>i : ℕ<VAR>hi : i < n<VAR>j : ℕ<VAR>hj : j < p ^ (n - i)<GOAL>↑p ^ (j + 1) * (↑((p ^ (n - i)).choose (j + 1)) * (↑p ^ i * (↑p ^ n)⁻¹)) = ↑((p ^ (n - i)).choose (j + 1)) / ↑(p ^ (n - i - v p ⟨j + 1, ⋯⟩)) * ↑(p ^ (j - v p ⟨j + 1, ⋯⟩)) * ↑p
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<VAR>h1 : ↑p ^ n * ⅟↑p ^ n = 1<VAR>i : ℕ<VAR>hi : i < n<VAR>j : ℕ<VAR>hj : j < p ^ (n - i)<GOAL>↑p ^ j * ↑p * (↑((p ^ (n - i)).choose (j + 1)) * (↑p ^ i * (↑p ^ n)⁻¹)) = ↑((p ^ (n - i)).choose (j + 1)) / ↑p ^ (n - i - v p ⟨j + 1, ⋯⟩) * ↑p ^ (j - v p ⟨j + 1, ⋯⟩) * ↑p
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<VAR>h1 : ↑p ^ n * ⅟↑p ^ n = 1<VAR>i : ℕ<VAR>hi : i < n<VAR>j : ℕ<VAR>hj : j < p ^ (n - i)<GOAL>↑((p ^ (n - i)).choose (j + 1)) * ↑p ^ (j - v p ⟨j + 1, ⋯⟩) * ↑p * ↑p ^ n = ↑p ^ j * ↑p * ↑((p ^ (n - i)).choose (j + 1) * p ^ i) * ↑p ^ (n - i - v p ⟨j + 1, ⋯⟩)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<VAR>h1 : ↑p ^ n * ⅟↑p ^ n = 1<VAR>i : ℕ<VAR>hi : i < n<VAR>j : ℕ<VAR>hj : j < p ^ (n - i)<GOAL>↑p * (↑((p ^ (n - i)).choose (j + 1)) * ↑p ^ (i + j + (n - i - v p ⟨j + 1, ⋯⟩))) = ↑p ^ j * ↑p * (↑((p ^ (n - i)).choose (j + 1)) * ↑p ^ i) * ↑p ^ (n - i - v p ⟨j + 1, ⋯⟩)
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝⁷ : CommSemiring R✝<VAR>inst✝⁶ : NonUnitalRing A✝<VAR>inst✝⁵ : Module R✝ A✝<VAR>inst✝⁴ : IsScalarTower R✝ A✝ A✝<VAR>inst✝³ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝² : Semifield R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a : A<VAR>x : R<GOAL>x ∈ quasispectrum R a ↔ x = 0 ∨ x ∈ spectrum R a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort u_6<VAR>κ : ι → Sort u_7<VAR>inst✝ : FunLike F α β<VAR>e : α ≃ β<VAR>s : Set α<GOAL>(fun s => ⇑e.symm '' s) ((fun s => ⇑e '' s) s) = s