ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>I✝ J✝ I J : FractionalIdeal R₁⁰ K<VAR>h : I * J = 1<GOAL>J = 1 / I
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>I✝ J✝ I J : FractionalIdeal R₁⁰ K<VAR>h : I * J = 1<VAR>hI : I ≠ 0<GOAL>J = 1 / I
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>I✝ J✝ I J : FractionalIdeal R₁⁰ K<VAR>h : I * J = 1<VAR>hI : I ≠ 0<GOAL>I * (1 / I) = 1
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>I✝ J✝ I J : FractionalIdeal R₁⁰ K<VAR>h : I * J = 1<VAR>hI : I ≠ 0<GOAL>I * (1 / I) ≤ 1
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>I✝ J✝ I J : FractionalIdeal R₁⁰ K<VAR>h : I * J = 1<VAR>hI : I ≠ 0<GOAL>1 ≤ I * (1 / I)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>I✝ J✝ I J : FractionalIdeal R₁⁰ K<VAR>h : I * J = 1<VAR>hI : I ≠ 0<GOAL>I * J ≤ I * (I * J / I)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>I✝ J✝ I J : FractionalIdeal R₁⁰ K<VAR>h : I * J = 1<VAR>hI : I ≠ 0<GOAL>J ≤ I * J / I
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>I✝ J✝ I J : FractionalIdeal R₁⁰ K<VAR>h : I * J = 1<VAR>hI : I ≠ 0<GOAL>∀ x ∈ J, ∀ y ∈ I, x * y ∈ I * J
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>I✝ J✝ I J : FractionalIdeal R₁⁰ K<VAR>h : I * J = 1<VAR>hI : I ≠ 0<VAR>y : K<VAR>hy : y ∈ J<VAR>x : K<VAR>hx : x ∈ I<GOAL>y * x ∈ I * J
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>I✝ J✝ I J : FractionalIdeal R₁⁰ K<VAR>h : I * J = 1<VAR>hI : I ≠ 0<VAR>y : K<VAR>hy : y ∈ J<VAR>x : K<VAR>hx : x ∈ I<GOAL>x * y ∈ I * J
<VAR>J : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝ : Category.{v₂, u₂} K<VAR>h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂<GOAL>IsPreconnected J
<VAR>J : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝ : Category.{v₂, u₂} K<VAR>h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂<GOAL>∀ {α : Type u₁} (F : J → α), (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂) → ∀ (j j' : J), F j = F j'
<VAR>X✝ Y Z : Scheme<VAR>𝒰✝ : X✝.OpenCover<VAR>f : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝¹ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f) g<VAR>X : Scheme<VAR>U : X.Opens<VAR>s : ↑Γ(X, U)<VAR>𝒰 : X.OpenCover<VAR>inst✝ : Finite 𝒰.J<VAR>fn : 𝒰.J → ℕ<VAR>hfn : ∀ (i : 𝒰.J), (Hom.app (𝒰.map i) U) s ^ fn i = 0<VAR>this : Fintype 𝒰.J<VAR>N : ℕ := Finset.univ.sup fn<GOAL>IsNilpotent s
<VAR>X✝ Y Z : Scheme<VAR>𝒰✝ : X✝.OpenCover<VAR>f : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝¹ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f) g<VAR>X : Scheme<VAR>U : X.Opens<VAR>s : ↑Γ(X, U)<VAR>𝒰 : X.OpenCover<VAR>inst✝ : Finite 𝒰.J<VAR>fn : 𝒰.J → ℕ<VAR>hfn : ∀ (i : 𝒰.J), (Hom.app (𝒰.map i) U) s ^ fn i = 0<VAR>this : Fintype 𝒰.J<VAR>N : ℕ := Finset.univ.sup fn<VAR>hfnleN : ∀ (i : 𝒰.J), fn i ≤ N<GOAL>IsNilpotent s
<VAR>X✝ Y Z : Scheme<VAR>𝒰✝ : X✝.OpenCover<VAR>f : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝¹ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f) g<VAR>X : Scheme<VAR>U : X.Opens<VAR>s : ↑Γ(X, U)<VAR>𝒰 : X.OpenCover<VAR>inst✝ : Finite 𝒰.J<VAR>fn : 𝒰.J → ℕ<VAR>hfn : ∀ (i : 𝒰.J), (Hom.app (𝒰.map i) U) s ^ fn i = 0<VAR>this : Fintype 𝒰.J<VAR>N : ℕ := Finset.univ.sup fn<VAR>hfnleN : ∀ (i : 𝒰.J), fn i ≤ N<GOAL>s ^ N = 0
<VAR>X✝ Y Z : Scheme<VAR>𝒰✝ : X✝.OpenCover<VAR>f : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝¹ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f) g<VAR>X : Scheme<VAR>U : X.Opens<VAR>s : ↑Γ(X, U)<VAR>𝒰 : X.OpenCover<VAR>inst✝ : Finite 𝒰.J<VAR>fn : 𝒰.J → ℕ<VAR>hfn : ∀ (i : 𝒰.J), (Hom.app (𝒰.map i) U) s ^ fn i = 0<VAR>this : Fintype 𝒰.J<VAR>N : ℕ := Finset.univ.sup fn<VAR>hfnleN : ∀ (i : 𝒰.J), fn i ≤ N<GOAL>∀ (i : ?h.𝒰.J), (Hom.app (?h.𝒰.map i) U) (s ^ N) = 0
<VAR>X✝ Y Z : Scheme<VAR>𝒰✝ : X✝.OpenCover<VAR>f : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝¹ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f) g<VAR>X : Scheme<VAR>U : X.Opens<VAR>s : ↑Γ(X, U)<VAR>𝒰 : X.OpenCover<VAR>inst✝ : Finite 𝒰.J<VAR>fn : 𝒰.J → ℕ<VAR>hfn : ∀ (i : 𝒰.J), (Hom.app (𝒰.map i) U) s ^ fn i = 0<VAR>this : Fintype 𝒰.J<VAR>N : ℕ := Finset.univ.sup fn<VAR>hfnleN : ∀ (i : 𝒰.J), fn i ≤ N<GOAL>X.OpenCover
<VAR>X✝ Y Z : Scheme<VAR>𝒰✝ : X✝.OpenCover<VAR>f : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝¹ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f) g<VAR>X : Scheme<VAR>U : X.Opens<VAR>s : ↑Γ(X, U)<VAR>𝒰 : X.OpenCover<VAR>inst✝ : Finite 𝒰.J<VAR>fn : 𝒰.J → ℕ<VAR>hfn : ∀ (i : 𝒰.J), (Hom.app (𝒰.map i) U) s ^ fn i = 0<VAR>this : Fintype 𝒰.J<VAR>N : ℕ := Finset.univ.sup fn<VAR>hfnleN : ∀ (i : 𝒰.J), fn i ≤ N<VAR>i : ?h.𝒰.J<GOAL>(Hom.app (?h.𝒰.map i) U) s ^ N = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>p : R[X]<VAR>s : R<VAR>i : ℕ<GOAL>(p.scaleRoots s).coeff i = p.coeff i * s ^ (p.natDegree - i)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderTopology α<VAR>a : α<VAR>s : Set α<VAR>hs : s ∈ 𝓝 a<GOAL>∃ b c, a ∈ Icc b c ∧ Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderTopology α<VAR>a : α<VAR>s : Set α<VAR>hs : s ∈ 𝓝 a<VAR>b : α<VAR>hba : b ≤ a<VAR>hb_nhds : Icc b a ∈ 𝓝[≤] a<VAR>hbs : Icc b a ⊆ s<GOAL>∃ b c, a ∈ Icc b c ∧ Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderTopology α<VAR>a : α<VAR>s : Set α<VAR>hs : s ∈ 𝓝 a<VAR>b : α<VAR>hba : b ≤ a<VAR>hb_nhds : Icc b a ∈ 𝓝[≤] a<VAR>hbs : Icc b a ⊆ s<VAR>c : α<VAR>hac : a ≤ c<VAR>hc_nhds : Icc a c ∈ 𝓝[≥] a<VAR>hcs : Icc a c ⊆ s<GOAL>∃ b c, a ∈ Icc b c ∧ Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderTopology α<VAR>a : α<VAR>s : Set α<VAR>hs : s ∈ 𝓝 a<VAR>b : α<VAR>hba : b ≤ a<VAR>hb_nhds : Icc b a ∈ 𝓝[≤] a<VAR>hbs : Icc b a ⊆ s<VAR>c : α<VAR>hac : a ≤ c<VAR>hc_nhds : Icc a c ∈ 𝓝[≥] a<VAR>hcs : Icc a c ⊆ s<GOAL>Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderTopology α<VAR>a : α<VAR>s : Set α<VAR>hs : s ∈ 𝓝 a<VAR>b : α<VAR>hba : b ≤ a<VAR>hb_nhds : Icc b a ∈ 𝓝[≤] a<VAR>hbs : Icc b a ⊆ s<VAR>c : α<VAR>hac : a ≤ c<VAR>hc_nhds : Icc a c ∈ 𝓝[≥] a<VAR>hcs : Icc a c ⊆ s<GOAL>Icc b a ∪ Icc a c ∈ 𝓝[≤] a ⊔ 𝓝[≥] a ∧ Icc b a ∪ Icc a c ⊆ s
<VAR>p q : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Fact (Nat.Prime q)<VAR>hp : p ≠ 2<VAR>hq : q ≠ 2<VAR>hpq : p ≠ q<GOAL>legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))
<VAR>p q : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Fact (Nat.Prime q)<VAR>hp : p ≠ 2<VAR>hq : q ≠ 2<VAR>hpq : p ≠ q<VAR>hp₁ : p % 2 = 1<GOAL>legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))
<VAR>p q : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Fact (Nat.Prime q)<VAR>hp : p ≠ 2<VAR>hq : q ≠ 2<VAR>hpq : p ≠ q<VAR>hp₁ : p % 2 = 1<VAR>hq₁ : q % 2 = 1<GOAL>legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))
<VAR>p q : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Fact (Nat.Prime q)<VAR>hp : p ≠ 2<VAR>hq : q ≠ 2<VAR>hpq : p ≠ q<VAR>hp₁ : p % 2 = 1<VAR>hq₁ : q % 2 = 1<VAR>hq₂ : ringChar (ZMod q) ≠ 2<GOAL>legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))
<VAR>p q : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Fact (Nat.Prime q)<VAR>hp : p ≠ 2<VAR>hq : q ≠ 2<VAR>hpq : p ≠ q<VAR>hp₁ : p % 2 = 1<VAR>hq₁ : q % 2 = 1<VAR>hq₂ : ringChar (ZMod q) ≠ 2<VAR>h : (quadraticChar (ZMod p)) ↑q = (quadraticChar (ZMod q)) (↑(χ₄ ↑(Fintype.card (ZMod p))) * ↑(Fintype.card (ZMod p)))<GOAL>legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))
<VAR>p q : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Fact (Nat.Prime q)<VAR>hp : p ≠ 2<VAR>hq : q ≠ 2<VAR>hpq : p ≠ q<VAR>hp₁ : p % 2 = 1<VAR>hq₁ : q % 2 = 1<VAR>hq₂ : ringChar (ZMod q) ≠ 2<VAR>h : (quadraticChar (ZMod p)) ↑q = (quadraticChar (ZMod q)) (↑(χ₄ ↑p) * ↑p)<GOAL>legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))
<VAR>p q : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Fact (Nat.Prime q)<VAR>hp : p ≠ 2<VAR>hq : q ≠ 2<VAR>hpq : p ≠ q<VAR>hp₁ : p % 2 = 1<VAR>hq₁ : q % 2 = 1<VAR>hq₂ : ringChar (ZMod q) ≠ 2<VAR>h : (quadraticChar (ZMod p)) ↑q = (quadraticChar (ZMod q)) (↑(χ₄ ↑p) * ↑p)<VAR>nc : ∀ (n r : ℕ), ↑↑n = ↑n<VAR>nc' : ↑((-1) ^ (p / 2)) = (-1) ^ (p / 2)<GOAL>legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>n : ℕ<VAR>s : Set X<VAR>h : IsPathConnected s<VAR>p : Fin (n + 1) → X<VAR>hp : ∀ (i : Fin (n + 1)), p i ∈ s<GOAL>∃ γ, range ⇑γ ⊆ s ∧ ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>n : ℕ<VAR>s : Set X<VAR>h : IsPathConnected s<VAR>p : Fin (n + 1) → X<VAR>hp : ∀ (i : Fin (n + 1)), p i ∈ s<VAR>p' : ℕ → X := fun k => if h : k < n + 1 then p ⟨k, h⟩ else p ⟨0, ⋯⟩<GOAL>∃ γ, range ⇑γ ⊆ s ∧ ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>n : ℕ<VAR>s : Set X<VAR>h : IsPathConnected s<VAR>p : Fin (n + 1) → X<VAR>hp : ∀ (i : Fin (n + 1)), p i ∈ s<VAR>p' : ℕ → X := fun k => if h : k < n + 1 then p ⟨k, h⟩ else p ⟨0, ⋯⟩<VAR>γ : Path (p' 0) (p' n)<VAR>hγ : (∀ i ≤ n, p' i ∈ range ⇑γ) ∧ range ⇑γ ⊆ s<GOAL>∃ γ, range ⇑γ ⊆ s ∧ ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>n : ℕ<VAR>s : Set X<VAR>h : IsPathConnected s<VAR>p : Fin (n + 1) → X<VAR>hp : ∀ (i : Fin (n + 1)), p i ∈ s<VAR>p' : ℕ → X := fun k => if h : k < n + 1 then p ⟨k, h⟩ else p ⟨0, ⋯⟩<VAR>γ : Path (p' 0) (p' n)<VAR>hγ : (∀ i ≤ n, p' i ∈ range ⇑γ) ∧ range ⇑γ ⊆ s<VAR>hpp' : ∀ k < n + 1, p ↑k = p' k<GOAL>∃ γ, range ⇑γ ⊆ s ∧ ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>n : ℕ<VAR>s : Set X<VAR>h : IsPathConnected s<VAR>p : Fin (n + 1) → X<VAR>hp : ∀ (i : Fin (n + 1)), p i ∈ s<VAR>p' : ℕ → X := fun k => if h : k < n + 1 then p ⟨k, h⟩ else p ⟨0, ⋯⟩<VAR>γ : Path (p' 0) (p' n)<VAR>hγ : (∀ i ≤ n, p' i ∈ range ⇑γ) ∧ range ⇑γ ⊆ s<VAR>hpp' : ∀ k < n + 1, p ↑k = p' k<GOAL>range ⇑(γ.cast ⋯ ⋯) ⊆ s ∧ ∀ (i : Fin (n + 1)), p i ∈ range ⇑(γ.cast ⋯ ⋯)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>n : ℕ<VAR>s : Set X<VAR>h : IsPathConnected s<VAR>p : Fin (n + 1) → X<VAR>hp : ∀ (i : Fin (n + 1)), p i ∈ s<VAR>p' : ℕ → X := fun k => if h : k < n + 1 then p ⟨k, h⟩ else p ⟨0, ⋯⟩<VAR>γ : Path (p' 0) (p' n)<VAR>hγ : (∀ i ≤ n, p' i ∈ range ⇑γ) ∧ range ⇑γ ⊆ s<VAR>hpp' : ∀ k < n + 1, p ↑k = p' k<GOAL>range ⇑γ ⊆ s ∧ ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>n : ℕ<VAR>s : Set X<VAR>h : IsPathConnected s<VAR>p : Fin (n + 1) → X<VAR>hp : ∀ (i : Fin (n + 1)), p i ∈ s<VAR>p' : ℕ → X := fun k => if h : k < n + 1 then p ⟨k, h⟩ else p ⟨0, ⋯⟩<VAR>γ : Path (p' 0) (p' n)<VAR>hγ : (∀ i ≤ n, p' i ∈ range ⇑γ) ∧ range ⇑γ ⊆ s<VAR>hpp' : ∀ k < n + 1, p ↑k = p' k<GOAL>∀ (i : Fin (n + 1)), p i ∈ range ⇑γ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>n : ℕ<VAR>s : Set X<VAR>h : IsPathConnected s<VAR>p : Fin (n + 1) → X<VAR>hp : ∀ (i : Fin (n + 1)), p i ∈ s<VAR>p' : ℕ → X := fun k => if h : k < n + 1 then p ⟨k, h⟩ else p ⟨0, ⋯⟩<VAR>γ : Path (p' 0) (p' n)<VAR>hγ : (∀ i ≤ n, p' i ∈ range ⇑γ) ∧ range ⇑γ ⊆ s<VAR>hpp' : ∀ k < n + 1, p ↑k = p' k<VAR>i : ℕ<VAR>hi : i < n + 1<GOAL>p ⟨i, hi⟩ ∈ range ⇑γ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>n : ℕ<VAR>s : Set X<VAR>h : IsPathConnected s<VAR>p : Fin (n + 1) → X<VAR>hp : ∀ (i : Fin (n + 1)), p i ∈ s<VAR>p' : ℕ → X := fun k => if h : k < n + 1 then p ⟨k, h⟩ else p ⟨0, ⋯⟩<VAR>γ : Path (p' 0) (p' n)<VAR>hγ : (∀ i ≤ n, p' i ∈ range ⇑γ) ∧ range ⇑γ ⊆ s<VAR>hpp' : ∀ k < n + 1, p ↑k = p' k<VAR>i : ℕ<VAR>hi : i < n + 1<GOAL>p ⟨i, hi⟩ = p' i
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>n : ℕ<VAR>s : Set X<VAR>h : IsPathConnected s<VAR>p : Fin (n + 1) → X<VAR>hp : ∀ (i : Fin (n + 1)), p i ∈ s<VAR>p' : ℕ → X := fun k => if h : k < n + 1 then p ⟨k, h⟩ else p ⟨0, ⋯⟩<VAR>γ : Path (p' 0) (p' n)<VAR>hγ : (∀ i ≤ n, p' i ∈ range ⇑γ) ∧ range ⇑γ ⊆ s<VAR>hpp' : ∀ k < n + 1, p ↑k = p' k<VAR>i : ℕ<VAR>hi : i < n + 1<GOAL>i = i % n.succ
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>p q : A → Prop<VAR>inst✝²² : Semifield R<VAR>inst✝²¹ : StarRing R<VAR>inst✝²⁰ : MetricSpace R<VAR>inst✝¹⁹ : TopologicalSemiring R<VAR>inst✝¹⁸ : ContinuousStar R<VAR>inst✝¹⁷ : Field S<VAR>inst✝¹⁶ : StarRing S<VAR>inst✝¹⁵ : MetricSpace S<VAR>inst✝¹⁴ : TopologicalRing S<VAR>inst✝¹³ : ContinuousStar S<VAR>inst✝¹² : TopologicalSpace A<VAR>inst✝¹¹ : NonUnitalRing A<VAR>inst✝¹⁰ : StarRing A<VAR>inst✝⁹ : Module S A<VAR>inst✝⁸ : IsScalarTower S A A<VAR>inst✝⁷ : SMulCommClass S A A<VAR>inst✝⁶ : NonUnitalContinuousFunctionalCalculus S q<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Module R A<VAR>inst✝³ : IsScalarTower R S A<VAR>inst✝² : StarModule R S<VAR>inst✝¹ : ContinuousSMul R S<VAR>inst✝ : CompleteSpace R<VAR>a : A<VAR>φ : C(↑(σₙ S a), S)₀ →⋆ₙₐ[S] A<VAR>f : C(S, R)<VAR>h : QuasispectrumRestricts a ⇑f<VAR>h_id : φ (ContinuousMapZero.id ⋯) = a<GOAL>(nonUnitalStarAlgHom φ h) (ContinuousMapZero.id ⋯) = a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>p q : A → Prop<VAR>inst✝²² : Semifield R<VAR>inst✝²¹ : StarRing R<VAR>inst✝²⁰ : MetricSpace R<VAR>inst✝¹⁹ : TopologicalSemiring R<VAR>inst✝¹⁸ : ContinuousStar R<VAR>inst✝¹⁷ : Field S<VAR>inst✝¹⁶ : StarRing S<VAR>inst✝¹⁵ : MetricSpace S<VAR>inst✝¹⁴ : TopologicalRing S<VAR>inst✝¹³ : ContinuousStar S<VAR>inst✝¹² : TopologicalSpace A<VAR>inst✝¹¹ : NonUnitalRing A<VAR>inst✝¹⁰ : StarRing A<VAR>inst✝⁹ : Module S A<VAR>inst✝⁸ : IsScalarTower S A A<VAR>inst✝⁷ : SMulCommClass S A A<VAR>inst✝⁶ : NonUnitalContinuousFunctionalCalculus S q<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Module R A<VAR>inst✝³ : IsScalarTower R S A<VAR>inst✝² : StarModule R S<VAR>inst✝¹ : ContinuousSMul R S<VAR>inst✝ : CompleteSpace R<VAR>a : A<VAR>φ : C(↑(σₙ S a), S)₀ →⋆ₙₐ[S] A<VAR>f : C(S, R)<VAR>h : QuasispectrumRestricts a ⇑f<VAR>h_id : φ (ContinuousMapZero.id ⋯) = a<GOAL>φ ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯, map_zero' := ⋯ }.comp ((ContinuousMapZero.id ⋯).comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯, map_zero' := ⋯ })) = a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>p q : A → Prop<VAR>inst✝²² : Semifield R<VAR>inst✝²¹ : StarRing R<VAR>inst✝²⁰ : MetricSpace R<VAR>inst✝¹⁹ : TopologicalSemiring R<VAR>inst✝¹⁸ : ContinuousStar R<VAR>inst✝¹⁷ : Field S<VAR>inst✝¹⁶ : StarRing S<VAR>inst✝¹⁵ : MetricSpace S<VAR>inst✝¹⁴ : TopologicalRing S<VAR>inst✝¹³ : ContinuousStar S<VAR>inst✝¹² : TopologicalSpace A<VAR>inst✝¹¹ : NonUnitalRing A<VAR>inst✝¹⁰ : StarRing A<VAR>inst✝⁹ : Module S A<VAR>inst✝⁸ : IsScalarTower S A A<VAR>inst✝⁷ : SMulCommClass S A A<VAR>inst✝⁶ : NonUnitalContinuousFunctionalCalculus S q<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Module R A<VAR>inst✝³ : IsScalarTower R S A<VAR>inst✝² : StarModule R S<VAR>inst✝¹ : ContinuousSMul R S<VAR>inst✝ : CompleteSpace R<VAR>a : A<VAR>φ : C(↑(σₙ S a), S)₀ →⋆ₙₐ[S] A<VAR>f : C(S, R)<VAR>h : QuasispectrumRestricts a ⇑f<VAR>h_id : φ (ContinuousMapZero.id ⋯) = a<VAR>x : ↑(σₙ S a)<GOAL>({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯, map_zero' := ⋯ }.comp ((ContinuousMapZero.id ⋯).comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯, map_zero' := ⋯ })) x = (ContinuousMapZero.id ⋯) x
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : C<VAR>g : X ⟶ Y<VAR>inst✝ : IsIso g<VAR>f : Y ⟶ X<VAR>h : g ≫ f = 𝟙 X<GOAL>IsIso f
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : C<VAR>g : X ⟶ Y<VAR>inst✝ : IsIso g<VAR>f : Y ⟶ X<VAR>h : g ≫ f = 𝟙 X<GOAL>IsIso (inv g)
<VAR>a : Rat<GOAL>mkRat a.num a.den = a
<VAR>K : Type u_1<VAR>L : Type ?u.614660<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>p q : K[X]<VAR>hp : p ≠ 0<VAR>hpq : Associated p q<GOAL>(algEquivOfAssociated hp hpq) (root p) = root q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : DecidableEq β<VAR>f✝ g : α → β<VAR>s✝¹ : Finset α<VAR>t✝ : Finset β<VAR>a✝ : α<VAR>b c : β<VAR>inst✝ : DecidableEq γ<VAR>s✝ : Finset α<VAR>t : α → Finset β<VAR>f : β → γ<VAR>this : DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>x✝ : a ∉ s<VAR>ih : image f (s.biUnion t) = s.biUnion fun a => image f (t a)<GOAL>image f ((insert a s).biUnion t) = (insert a s).biUnion fun a => image f (t a)
<VAR>C : Type u<VAR>𝒞 : Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝¹ : HasLimit (pair X Y)<VAR>inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))<VAR>π₁ : X ⨯ Y ⟶ X := prod.fst<VAR>π₂ : X ⨯ Y ⟶ Y := prod.snd<VAR>e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)<GOAL>(e ≫ π₁) ≫ f = (e ≫ π₂) ≫ g
<VAR>C : Type u<VAR>𝒞 : Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝¹ : HasLimit (pair X Y)<VAR>inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))<VAR>π₁ : X ⨯ Y ⟶ X := prod.fst<VAR>π₂ : X ⨯ Y ⟶ Y := prod.snd<VAR>e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)<GOAL>equalizer.ι (π₁ ≫ f) (π₂ ≫ g) ≫ π₂ ≫ g = (e ≫ π₂) ≫ g
<VAR>C : Type u<VAR>𝒞 : Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝¹ : HasLimit (pair X Y)<VAR>inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))<VAR>π₁ : X ⨯ Y ⟶ X := prod.fst<VAR>π₂ : X ⨯ Y ⟶ Y := prod.snd<VAR>e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)<VAR>s : PullbackCone f g<GOAL>prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right) ≫ π₁ ≫ f = prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right) ≫ π₂ ≫ g
<VAR>C : Type u<VAR>𝒞 : Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝¹ : HasLimit (pair X Y)<VAR>inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))<VAR>π₁ : X ⨯ Y ⟶ X := prod.fst<VAR>π₂ : X ⨯ Y ⟶ Y := prod.snd<VAR>e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)<VAR>s : PullbackCone f g<GOAL>(BinaryFan.mk (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)).π.app { as := WalkingPair.left } ≫ f = (BinaryFan.mk (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)).π.app { as := WalkingPair.right } ≫ g
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.102730, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.102737, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.102744, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.102796, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ✝ : Dᵒᵖ ⥤ A<VAR>ℱ'✝ ℱ ℱ' : Sheaf K A<VAR>i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val<GOAL>({ val := (presheafIso i).hom } ≫ { val := (presheafIso i).inv }).val = (𝟙 ℱ).val
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.102730, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.102737, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.102744, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.102796, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ✝ : Dᵒᵖ ⥤ A<VAR>ℱ'✝ ℱ ℱ' : Sheaf K A<VAR>i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val<GOAL>({ val := (presheafIso i).inv } ≫ { val := (presheafIso i).hom }).val = (𝟙 ℱ').val
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>X Y : C<VAR>f f' : X ⟶ Y<VAR>inst✝² : HasImage f<VAR>inst✝¹ : HasImage f'<VAR>inst✝ : HasEqualizers C<VAR>h : f = f'<GOAL>ι f = (eqToIso h).hom ≫ ι f'
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>X Y : C<VAR>f f' : X ⟶ Y<VAR>inst✝² : HasImage f<VAR>inst✝¹ : HasImage f'<VAR>inst✝ : HasEqualizers C<VAR>h : f = f'<GOAL>factorThruImage f ≫ ι f = factorThruImage f ≫ (eqToIso h).hom ≫ ι f'
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>X Y : C<VAR>f f' : X ⟶ Y<VAR>inst✝² : HasImage f<VAR>inst✝¹ : HasImage f'<VAR>inst✝ : HasEqualizers C<VAR>h : f = f'<GOAL>factorThruImage f ≫ ι f = factorThruImage f ≫ lift (MonoFactorisation.mk (image f') (ι f') (factorThruImage f') ⋯) ≫ ι f'
<VAR>s r : ℝ<VAR>hs : 0 < s<VAR>r' : ℝ := max r 1<VAR>hr : 0 < r'<VAR>H : 0 < s / r'<VAR>x : ℝ<VAR>hx : 1 ≤ log x<GOAL>‖log x ^ r‖ ≤ 1 * ‖log x ^ r'‖
<VAR>s r : ℝ<VAR>hs : 0 < s<VAR>r' : ℝ := max r 1<VAR>hr : 0 < r'<VAR>H : 0 < s / r'<VAR>x : ℝ<VAR>hx : 1 ≤ log x<VAR>hx₀ : 0 ≤ log x<GOAL>‖log x ^ r‖ ≤ 1 * ‖log x ^ r'‖
<VAR>s r : ℝ<VAR>hs : 0 < s<VAR>r' : ℝ := max r 1<VAR>hr : 0 < r'<VAR>H : 0 < s / r'<VAR>x : ℝ<VAR>hx : 0 ≤ x<GOAL>(fun x => (x ^ (s / r')) ^ r') x = (fun x => x ^ s) x
<VAR>a b c : Cardinal.{u_1}<VAR>hc : ℵ₀ ≤ c<VAR>h1 : a < c<VAR>h2 : b < c<VAR>h : ℵ₀ ≤ max a b<GOAL>max a b * max a b < c
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝³ : Semiring S<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Field K<VAR>p : S[X]<VAR>f : S →+* K<VAR>hf : Function.Injective ⇑f<VAR>r s : S<VAR>hr : eval₂ f (f r / f s) p = 0<VAR>hs : s ∈ nonZeroDivisors S<GOAL>eval₂ f (f r) (p.scaleRoots s) = 0