ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f✝ : α✝ → E<VAR>g✝ : α✝ → F<VAR>k : α✝ → G<VAR>f' : α✝ → E'<VAR>g' : α✝ → F'<VAR>k' : α✝ → G'<VAR>f'' : α✝ → E''<VAR>g'' : α✝ → F''<VAR>k'' : α✝ → G''<VAR>l✝ l' : Filter α✝<VAR>α : Type u_17<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0<VAR>h : IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => ‖f x / g x‖<GOAL>f =O[l] g
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f✝ : α✝ → E<VAR>g✝ : α✝ → F<VAR>k : α✝ → G<VAR>f' : α✝ → E'<VAR>g' : α✝ → F'<VAR>k' : α✝ → G'<VAR>f'' : α✝ → E''<VAR>g'' : α✝ → F''<VAR>k'' : α✝ → G''<VAR>l✝ l' : Filter α✝<VAR>α : Type u_17<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0<VAR>c : ℝ<VAR>hc : ∀ᶠ (x : ℝ) in map (fun x => ‖f x / g x‖) l, (fun x x_1 => x ≤ x_1) x c<GOAL>f =O[l] g
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f✝ : α✝ → E<VAR>g✝ : α✝ → F<VAR>k : α✝ → G<VAR>f' : α✝ → E'<VAR>g' : α✝ → F'<VAR>k' : α✝ → G'<VAR>f'' : α✝ → E''<VAR>g'' : α✝ → F''<VAR>k'' : α✝ → G''<VAR>l✝ l' : Filter α✝<VAR>α : Type u_17<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0<VAR>c : ℝ<VAR>hc : ∀ᶠ (a : α) in l, ‖f a‖ / ‖g a‖ ≤ c<GOAL>f =O[l] g
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f✝ : α✝ → E<VAR>g✝ : α✝ → F<VAR>k : α✝ → G<VAR>f' : α✝ → E'<VAR>g' : α✝ → F'<VAR>k' : α✝ → G'<VAR>f'' : α✝ → E''<VAR>g'' : α✝ → F''<VAR>k'' : α✝ → G''<VAR>l✝ l' : Filter α✝<VAR>α : Type u_17<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0<VAR>c : ℝ<VAR>hc : ∀ᶠ (a : α) in l, ‖f a‖ / ‖g a‖ ≤ c<VAR>x : α<VAR>hx₁ : g x = 0 → f x = 0<VAR>hx₂ : ‖f x‖ / ‖g x‖ ≤ c<GOAL>‖f x‖ ≤ c * ‖g x‖
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x : α<VAR>s✝ t : Set α<VAR>r : ℝ<VAR>s : Set α<VAR>c : α<GOAL>IsCobounded s ↔ ∃ r, (closedBall c r)ᶜ ⊆ s
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x : α<VAR>s✝ t : Set α<VAR>r : ℝ<VAR>s : Set α<VAR>c : α<GOAL>(∃ r, sᶜ ⊆ closedBall c r) ↔ ∃ r, (closedBall c r)ᶜ ⊆ s
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x : α<VAR>s✝ t : Set α<VAR>r : ℝ<VAR>s : Set α<VAR>c : α<GOAL>∀ (a : ℝ), sᶜ ⊆ closedBall c a ↔ (closedBall c a)ᶜ ⊆ s
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x : α<VAR>s✝ t : Set α<VAR>r✝ : ℝ<VAR>s : Set α<VAR>c : α<VAR>r : ℝ<GOAL>sᶜ ⊆ closedBall c r ↔ (closedBall c r)ᶜ ⊆ s
<GOAL>1 * -1 - 0 * 0 = -1
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : ι → Submodule R M<VAR>inst✝² : DecidableEq ι<VAR>h : IsInternal N<VAR>inst✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)<VAR>inst✝ : ∀ (i : ι), Module.Free R ↥(N i)<VAR>s : Set ι<VAR>f : Module.End R M<VAR>hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)<GOAL>MapsTo ⇑f ↑(⨆ i ∈ s, N i) ↑(⨆ i ∈ s, N i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : ι → Submodule R M<VAR>inst✝² : DecidableEq ι<VAR>h : IsInternal N<VAR>inst✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)<VAR>inst✝ : ∀ (i : ι), Module.Free R ↥(N i)<VAR>s : Set ι<VAR>f : Module.End R M<VAR>hf : ∀ (i : ι), Submodule.map f (N i) ≤ N i<GOAL>MapsTo ⇑f ↑(⨆ i ∈ s, N i) ↑(⨆ i ∈ s, N i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : ι → Submodule R M<VAR>inst✝² : DecidableEq ι<VAR>h : IsInternal N<VAR>inst✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)<VAR>inst✝ : ∀ (i : ι), Module.Free R ↥(N i)<VAR>s : Set ι<VAR>f : Module.End R M<VAR>hf : ∀ (i : ι), Submodule.map f (N i) ≤ N i<GOAL>Submodule.map f (⨆ i ∈ s, N i) ≤ ⨆ i ∈ s, N i
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f✝ f : R[X]<GOAL>f.reverse.natDegree ≤ f.natDegree
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f✝ f : R[X]<GOAL>∀ (m : ℕ), ↑f.natDegree < ↑m → f.reverse.coeff m = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f✝ f : R[X]<VAR>n : ℕ<VAR>hn : ↑f.natDegree < ↑n<GOAL>f.reverse.coeff n = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f✝ f : R[X]<VAR>n : ℕ<VAR>hn : f.natDegree < n<GOAL>f.reverse.coeff n = 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : X → Y<VAR>S : Set X<GOAL>IsClosed S ∧ DiscreteTopology ↑S ↔ ∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 S)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : X → Y<VAR>S : Set X<GOAL>(∀ (x : X), (ClusterPt x (𝓟 S) → x ∈ S) ∧ (x ∈ S → 𝓝[≠] x ⊓ 𝓟 S = ⊥)) ↔ ∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 S)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : X → Y<VAR>S : Set X<VAR>x : X<GOAL>(ClusterPt x (𝓟 S) → x ∈ S) ∧ (x ∈ S → 𝓝[≠] x ⊓ 𝓟 S = ⊥) ↔ Disjoint (𝓝[≠] x) (𝓟 S)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : X → Y<VAR>S : Set X<VAR>x : X<GOAL>(x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S)) ↔ Disjoint (𝓝[≠] x) (𝓟 S)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>H✝ K✝ : Subgroup G<VAR>k : Set G<VAR>N : Type u_5<VAR>inst✝¹ : Group N<VAR>P : Type u_6<VAR>inst✝ : Group P<VAR>H : Subgroup G<VAR>K : Subgroup N<VAR>J : Subgroup (G × N)<GOAL>H.prod K ≤ J ↔ map (MonoidHom.inl G N) H ≤ J ∧ map (MonoidHom.inr G N) K ≤ J
<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>F : Type u_3<VAR>inst✝ : Field F<VAR>φ : K →+* ℂ<VAR>h : ComplexEmbedding.IsReal φ<GOAL>(mk φ).embedding = φ
<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>F : Type u_3<VAR>inst✝ : Field F<VAR>φ : K →+* ℂ<VAR>h : ComplexEmbedding.IsReal φ<VAR>this : (mk φ).embedding = φ ∨ (mk φ).embedding = ComplexEmbedding.conjugate φ<GOAL>(mk φ).embedding = φ
<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 A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>I J : Ideal A<GOAL>IsCoprime I J ↔ gcd I J = 1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n ν : ℕ<GOAL>Polynomial.derivative (↑((n + 1).choose (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n + 1 - (ν + 1))) = (↑n + 1) * (bernsteinPolynomial R n ν - bernsteinPolynomial R n (ν + 1))
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n ν : ℕ<GOAL>↑((n + 1).choose (ν + 1)) * (↑(ν + 1) * X ^ ν) * (1 - X) ^ (n - ν) - ↑((n + 1).choose (ν + 1)) * X ^ (ν + 1) * (↑(n - ν) * (1 - X) ^ (n - ν - 1)) = ↑(n + 1) * (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν) - ↑(n.choose (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n - (ν + 1)))
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n ν : ℕ<GOAL>↑((n + 1).choose (ν + 1)) * (↑(ν + 1) * X ^ ν) * (1 - X) ^ (n - ν) - ↑((n + 1).choose (ν + 1)) * X ^ (ν + 1) * (↑(n - ν) * (1 - X) ^ (n - ν - 1)) = ↑(n + 1) * (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν)) - ↑(n + 1) * (↑(n.choose (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n - (ν + 1)))
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n ν : ℕ<GOAL>↑((n + 1).choose (ν + 1)) * (↑(ν + 1) * X ^ ν) * (1 - X) ^ (n - ν) = ↑(n + 1) * (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν))
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n ν : ℕ<GOAL>↑((n + 1).choose (ν + 1)) * X ^ (ν + 1) * (↑(n - ν) * (1 - X) ^ (n - ν - 1)) = ↑(n + 1) * (↑(n.choose (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n - (ν + 1)))
<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>Rₘ : Type u_4<VAR>Sₘ : Type u_5<VAR>inst✝⁷ : CommRing Rₘ<VAR>inst✝⁶ : CommRing Sₘ<VAR>inst✝⁵ : Algebra R Rₘ<VAR>inst✝⁴ : IsLocalization M Rₘ<VAR>inst✝³ : Algebra S Sₘ<VAR>inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>inst✝¹ : Algebra Rₘ S<VAR>inst✝ : IsScalarTower R Rₘ S<VAR>x : S<VAR>hx : IsIntegral Rₘ x<GOAL>∃ m, IsIntegral R (m • x)
<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>Rₘ : Type u_4<VAR>Sₘ : Type u_5<VAR>inst✝⁷ : CommRing Rₘ<VAR>inst✝⁶ : CommRing Sₘ<VAR>inst✝⁵ : Algebra R Rₘ<VAR>inst✝⁴ : IsLocalization M Rₘ<VAR>inst✝³ : Algebra S Sₘ<VAR>inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>inst✝¹ : Algebra Rₘ S<VAR>inst✝ : IsScalarTower R Rₘ S<VAR>x : S<VAR>hx : IsIntegral Rₘ x<VAR>h✝ : Subsingleton Rₘ<GOAL>∃ m, IsIntegral R (m • x)
<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>Rₘ : Type u_4<VAR>Sₘ : Type u_5<VAR>inst✝⁷ : CommRing Rₘ<VAR>inst✝⁶ : CommRing Sₘ<VAR>inst✝⁵ : Algebra R Rₘ<VAR>inst✝⁴ : IsLocalization M Rₘ<VAR>inst✝³ : Algebra S Sₘ<VAR>inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>inst✝¹ : Algebra Rₘ S<VAR>inst✝ : IsScalarTower R Rₘ S<VAR>x : S<VAR>hx : IsIntegral Rₘ x<VAR>nontriv : Nontrivial Rₘ<GOAL>∃ m, IsIntegral R (m • x)
<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>Rₘ : Type u_4<VAR>Sₘ : Type u_5<VAR>inst✝⁷ : CommRing Rₘ<VAR>inst✝⁶ : CommRing Sₘ<VAR>inst✝⁵ : Algebra R Rₘ<VAR>inst✝⁴ : IsLocalization M Rₘ<VAR>inst✝³ : Algebra S Sₘ<VAR>inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>inst✝¹ : Algebra Rₘ S<VAR>inst✝ : IsScalarTower R Rₘ S<VAR>x : S<VAR>nontriv : Nontrivial Rₘ<VAR>p : Rₘ[X]<VAR>hp₁ : p.Monic<VAR>hp₂ : eval₂ (algebraMap Rₘ S) x p = 0<GOAL>∃ m, IsIntegral R (m • x)
<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>Rₘ : Type u_4<VAR>Sₘ : Type u_5<VAR>inst✝⁷ : CommRing Rₘ<VAR>inst✝⁶ : CommRing Sₘ<VAR>inst✝⁵ : Algebra R Rₘ<VAR>inst✝⁴ : IsLocalization M Rₘ<VAR>inst✝³ : Algebra S Sₘ<VAR>inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>inst✝¹ : Algebra Rₘ S<VAR>inst✝ : IsScalarTower R Rₘ S<VAR>x : S<VAR>nontriv : Nontrivial Rₘ<VAR>p : Rₘ[X]<VAR>hp₁ : p.Monic<VAR>hp₂ : eval₂ (algebraMap Rₘ S) x p = 0<VAR>this : ∃ q, Polynomial.map (algebraMap R Rₘ) q = p.scaleRoots ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff)) ∧ q.natDegree = (p.scaleRoots ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff))).natDegree ∧ q.Monic<GOAL>∃ m, IsIntegral R (m • x)
<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>Rₘ : Type u_4<VAR>Sₘ : Type u_5<VAR>inst✝⁷ : CommRing Rₘ<VAR>inst✝⁶ : CommRing Sₘ<VAR>inst✝⁵ : Algebra R Rₘ<VAR>inst✝⁴ : IsLocalization M Rₘ<VAR>inst✝³ : Algebra S Sₘ<VAR>inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>inst✝¹ : Algebra Rₘ S<VAR>inst✝ : IsScalarTower R Rₘ S<VAR>x : S<VAR>nontriv : Nontrivial Rₘ<VAR>p : Rₘ[X]<VAR>hp₁ : p.Monic<VAR>hp₂ : eval₂ (algebraMap Rₘ S) x p = 0<GOAL>p.leadingCoeff ∈ (algebraMap R Rₘ).range
<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>Rₘ : Type u_4<VAR>Sₘ : Type u_5<VAR>inst✝⁷ : CommRing Rₘ<VAR>inst✝⁶ : CommRing Sₘ<VAR>inst✝⁵ : Algebra R Rₘ<VAR>inst✝⁴ : IsLocalization M Rₘ<VAR>inst✝³ : Algebra S Sₘ<VAR>inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>inst✝¹ : Algebra Rₘ S<VAR>inst✝ : IsScalarTower R Rₘ S<VAR>x : S<VAR>nontriv : Nontrivial Rₘ<VAR>p : Rₘ[X]<VAR>hp₁ : p.Monic<VAR>hp₂ : eval₂ (algebraMap Rₘ S) x p = 0<GOAL>(p.scaleRoots ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff))).Monic
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ζ : Type u_6<VAR>r : α → α → Prop<VAR>a b c d : α<VAR>h : ReflTransGen r a b<GOAL>a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ζ : Type u_6<VAR>r : α → α → Prop<VAR>a b c d : α<GOAL>b = b ∨ ∃ c, r b c ∧ ReflTransGen r c b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ζ : Type u_6<VAR>r : α → α → Prop<VAR>a b c d a✝¹ c✝ : α<VAR>h'✝ : r a✝¹ c✝<VAR>h✝ : ReflTransGen r c✝ b<VAR>a✝ : c✝ = b ∨ ∃ c, r c✝ c ∧ ReflTransGen r c b<GOAL>a✝¹ = b ∨ ∃ c, r a✝¹ c ∧ ReflTransGen r c b
<VAR>R : Type u<VAR>M : Type v<VAR>M'✝ : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid M'✝<VAR>inst✝² : Module R M'✝<VAR>I J : Ideal R<VAR>N✝ P : Submodule R M<VAR>S : Set R<VAR>T : Set M<VAR>M' : Type w<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>r : R<VAR>N : Submodule R M<VAR>f : M →ₗ[R] M'<GOAL>map f (r • N) = r • map f N
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ : L.BoundedFormula α n<VAR>M : T.ModelType<VAR>v : α → ↑M<VAR>xs : Fin n → ↑M<GOAL>(φ ⇔ φ).Realize v xs
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>hp : p.Monic<VAR>hq : q.Monic<VAR>h : q.natDegree ≠ 0<GOAL>(p.comp q).Monic
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁹ : CommRing K<VAR>inst✝⁸ : CommRing L<VAR>inst✝⁷ : CommRing M<VAR>inst✝⁶ : CommRing N<VAR>i : K →+* L<VAR>j : K →+* M<VAR>k : K →+* N<VAR>f : L →+* M<VAR>g : L →+* N<VAR>p : ℕ<VAR>inst✝⁵ : ExpChar K p<VAR>inst✝⁴ : ExpChar L p<VAR>inst✝³ : ExpChar M p<VAR>inst✝² : ExpChar N p<VAR>inst✝¹ : PerfectRing M p<VAR>inst✝ : IsPRadical i p<VAR>x : L<VAR>n : ℕ<VAR>y : K<VAR>h : i y = x ^ p ^ n<GOAL>(iterateFrobeniusEquiv M p (Classical.choose ⋯).1).symm (j (Classical.choose ⋯).2) = (iterateFrobeniusEquiv M p n).symm (j y)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁹ : CommRing K<VAR>inst✝⁸ : CommRing L<VAR>inst✝⁷ : CommRing M<VAR>inst✝⁶ : CommRing N<VAR>i : K →+* L<VAR>j : K →+* M<VAR>k : K →+* N<VAR>f : L →+* M<VAR>g : L →+* N<VAR>p : ℕ<VAR>inst✝⁵ : ExpChar K p<VAR>inst✝⁴ : ExpChar L p<VAR>inst✝³ : ExpChar M p<VAR>inst✝² : ExpChar N p<VAR>inst✝¹ : PerfectRing M p<VAR>inst✝ : IsPRadical i p<VAR>x : L<VAR>n : ℕ<VAR>y : K<VAR>h : i y = x ^ p ^ n<VAR>h' : i (Classical.choose ⋯).2 = x ^ p ^ (Classical.choose ⋯).1<GOAL>(iterateFrobeniusEquiv M p (Classical.choose ⋯).1).symm (j (Classical.choose ⋯).2) = (iterateFrobeniusEquiv M p n).symm (j y)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁹ : CommRing K<VAR>inst✝⁸ : CommRing L<VAR>inst✝⁷ : CommRing M<VAR>inst✝⁶ : CommRing N<VAR>i : K →+* L<VAR>j : K →+* M<VAR>k : K →+* N<VAR>f : L →+* M<VAR>g : L →+* N<VAR>p : ℕ<VAR>inst✝⁵ : ExpChar K p<VAR>inst✝⁴ : ExpChar L p<VAR>inst✝³ : ExpChar M p<VAR>inst✝² : ExpChar N p<VAR>inst✝¹ : PerfectRing M p<VAR>inst✝ : IsPRadical i p<VAR>x : L<VAR>n : ℕ<VAR>y : K<VAR>h : i y = x ^ p ^ n<VAR>n' : ℕ := (Classical.choose ⋯).1<VAR>h' : i (Classical.choose ⋯).2 = x ^ p ^ n'<GOAL>(iterateFrobeniusEquiv M p n').symm (j (Classical.choose ⋯).2) = (iterateFrobeniusEquiv M p n).symm (j y)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁹ : CommRing K<VAR>inst✝⁸ : CommRing L<VAR>inst✝⁷ : CommRing M<VAR>inst✝⁶ : CommRing N<VAR>i : K →+* L<VAR>j : K →+* M<VAR>k : K →+* N<VAR>f : L →+* M<VAR>g : L →+* N<VAR>p : ℕ<VAR>inst✝⁵ : ExpChar K p<VAR>inst✝⁴ : ExpChar L p<VAR>inst✝³ : ExpChar M p<VAR>inst✝² : ExpChar N p<VAR>inst✝¹ : PerfectRing M p<VAR>inst✝ : IsPRadical i p<VAR>x : L<VAR>n : ℕ<VAR>y : K<VAR>n' : ℕ := (Classical.choose ⋯).1<VAR>h' : i (Classical.choose ⋯).2 = x ^ p ^ n'<VAR>h : (x ^ p ^ n) ^ p ^ n' = i y ^ p ^ n'<GOAL>(iterateFrobeniusEquiv M p n').symm (j (Classical.choose ⋯).2) = (iterateFrobeniusEquiv M p n).symm (j y)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁹ : CommRing K<VAR>inst✝⁸ : CommRing L<VAR>inst✝⁷ : CommRing M<VAR>inst✝⁶ : CommRing N<VAR>i : K →+* L<VAR>j : K →+* M<VAR>k : K →+* N<VAR>f : L →+* M<VAR>g : L →+* N<VAR>p : ℕ<VAR>inst✝⁵ : ExpChar K p<VAR>inst✝⁴ : ExpChar L p<VAR>inst✝³ : ExpChar M p<VAR>inst✝² : ExpChar N p<VAR>inst✝¹ : PerfectRing M p<VAR>inst✝ : IsPRadical i p<VAR>x : L<VAR>n : ℕ<VAR>y : K<VAR>n' : ℕ := (Classical.choose ⋯).1<VAR>h' : i (Classical.choose ⋯).2 = x ^ p ^ n'<VAR>h : (Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n' ∈ RingHom.ker i<GOAL>(iterateFrobeniusEquiv M p n').symm (j (Classical.choose ⋯).2) = (iterateFrobeniusEquiv M p n).symm (j y)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁹ : CommRing K<VAR>inst✝⁸ : CommRing L<VAR>inst✝⁷ : CommRing M<VAR>inst✝⁶ : CommRing N<VAR>i : K →+* L<VAR>j : K →+* M<VAR>k : K →+* N<VAR>f : L →+* M<VAR>g : L →+* N<VAR>p : ℕ<VAR>inst✝⁵ : ExpChar K p<VAR>inst✝⁴ : ExpChar L p<VAR>inst✝³ : ExpChar M p<VAR>inst✝² : ExpChar N p<VAR>inst✝¹ : PerfectRing M p<VAR>inst✝ : IsPRadical i p<VAR>x : L<VAR>n : ℕ<VAR>y : K<VAR>n' : ℕ := (Classical.choose ⋯).1<VAR>h' : i (Classical.choose ⋯).2 = x ^ p ^ n'<VAR>h✝ : (Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n' ∈ RingHom.ker i<VAR>m : ℕ<VAR>h : ((Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n') ^ p ^ m = 0<GOAL>(iterateFrobeniusEquiv M p n').symm (j (Classical.choose ⋯).2) = (iterateFrobeniusEquiv M p n).symm (j y)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁹ : CommRing K<VAR>inst✝⁸ : CommRing L<VAR>inst✝⁷ : CommRing M<VAR>inst✝⁶ : CommRing N<VAR>i : K →+* L<VAR>j : K →+* M<VAR>k : K →+* N<VAR>f : L →+* M<VAR>g : L →+* N<VAR>p : ℕ<VAR>inst✝⁵ : ExpChar K p<VAR>inst✝⁴ : ExpChar L p<VAR>inst✝³ : ExpChar M p<VAR>inst✝² : ExpChar N p<VAR>inst✝¹ : PerfectRing M p<VAR>inst✝ : IsPRadical i p<VAR>x : L<VAR>n : ℕ<VAR>y : K<VAR>n' : ℕ := (Classical.choose ⋯).1<VAR>h' : i (Classical.choose ⋯).2 = x ^ p ^ n'<VAR>h✝ : (Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n' ∈ RingHom.ker i<VAR>m : ℕ<VAR>h : ((Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n') ^ p ^ m = 0<GOAL>(iterateFrobeniusEquiv M p (m + n + n')) ((iterateFrobeniusEquiv M p n').symm (j (Classical.choose ⋯).2)) = (iterateFrobeniusEquiv M p (m + n + n')) ((iterateFrobeniusEquiv M p n).symm (j y))
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁹ : CommRing K<VAR>inst✝⁸ : CommRing L<VAR>inst✝⁷ : CommRing M<VAR>inst✝⁶ : CommRing N<VAR>i : K →+* L<VAR>j : K →+* M<VAR>k : K →+* N<VAR>f : L →+* M<VAR>g : L →+* N<VAR>p : ℕ<VAR>inst✝⁵ : ExpChar K p<VAR>inst✝⁴ : ExpChar L p<VAR>inst✝³ : ExpChar M p<VAR>inst✝² : ExpChar N p<VAR>inst✝¹ : PerfectRing M p<VAR>inst✝ : IsPRadical i p<VAR>x : L<VAR>n : ℕ<VAR>y : K<VAR>n' : ℕ := (Classical.choose ⋯).1<VAR>h' : i (Classical.choose ⋯).2 = x ^ p ^ n'<VAR>h✝ : (Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n' ∈ RingHom.ker i<VAR>m : ℕ<VAR>h : ((Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n') ^ p ^ m = 0<GOAL>(iterateFrobeniusEquiv M p (m + n)) (j (Classical.choose ⋯).2) = (iterateFrobeniusEquiv M p (m + n + n')) ((iterateFrobeniusEquiv M p n).symm (j y))
<VAR>f : Bool → Bool → Bool<GOAL>bitwise (swap f) = swap (bitwise f)
<VAR>f : Bool → Bool → Bool<VAR>m n : ℕ<GOAL>bitwise (swap f) m n = swap (bitwise f) m n
<VAR>f : Bool → Bool → Bool<VAR>m : ℕ<VAR>ih : ∀ (m_1 : ℕ), m_1 < m → ∀ (n : ℕ), bitwise (swap f) m_1 n = bitwise f n m_1<VAR>n : ℕ<GOAL>bitwise (swap f) m n = bitwise f n m
<VAR>f : Bool → Bool → Bool<VAR>m : ℕ<VAR>ih : ∀ (m_1 : ℕ), m_1 < m + 1 → ∀ (n : ℕ), bitwise (swap f) m_1 n = bitwise f n m_1<VAR>n : ℕ<GOAL>bitwise (swap f) (m + 1) (n + 1) = bitwise f (n + 1) (m + 1)
<VAR>C : Type u_1<VAR>inst✝¹³ : Category.{u_5, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝¹² : Category.{u_6, u_2} A<VAR>inst✝¹¹ : HasWeakSheafify J A<VAR>inst✝¹⁰ : (constantSheaf J A).Faithful<VAR>inst✝⁹ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>B : Type u_3<VAR>inst✝⁸ : Category.{u_4, u_3} B<VAR>U : A ⥤ B<VAR>inst✝⁷ : HasWeakSheafify J A<VAR>inst✝⁶ : HasWeakSheafify J B<VAR>inst✝⁵ : (constantSheaf J A).Faithful<VAR>inst✝⁴ : (constantSheaf J A).Full<VAR>inst✝³ : (constantSheaf J B).Faithful<VAR>inst✝² : (constantSheaf J B).Full<VAR>inst✝¹ : J.PreservesSheafification U<VAR>inst✝ : J.HasSheafCompose U<VAR>F : Sheaf J A<GOAL>((sheafifyComposeIso J U ((const Cᵒᵖ).obj (F.val.obj (op t)))).symm ≪≫ (presheafToSheaf J B ⋙ sheafToPresheaf J B).mapIso (constComp Cᵒᵖ (F.val.obj (op t)) U)).hom ≫ ((constantSheafAdj J B ht).counit.app ((sheafCompose J U).obj F)).val = ((sheafCompose J U).map ((constantSheafAdj J A ht).counit.app F)).val