ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<VAR>ha_ne_zero : Ideal.span {a} ≠ 0<VAR>hJ_ne_zero : J ≠ 0<GOAL>∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) = 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<VAR>ha_ne_zero : Ideal.span {a} ≠ 0<VAR>hJ_ne_zero : J ≠ 0<VAR>h_subset : {v | ¬↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) = 0} ⊆ {v | v.asIdeal ∣ J} ∪ {v | v.asIdeal ∣ Ideal.span {a}}<GOAL>∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) = 0
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>X' X : C<VAR>Y Y' : D<VAR>f : X' ⟶ X<VAR>g : X ⟶ G.obj Y<GOAL>(adj.homEquiv X' Y).symm (f ≫ g) = F.map f ≫ (adj.homEquiv X Y).symm g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ✝ : Kernel α (γ × β)<VAR>ν✝ : Kernel α γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>inst✝ : IsFiniteKernel κ<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>seq : ℕ → Set β<VAR>hseq : Antitone seq<VAR>hseq_iInter : ⋂ i, seq i = ∅<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<VAR>h0 : ¬(ν a) (countablePartitionSet n x) = 0<GOAL>Tendsto (fun m => ((κ a) (countablePartitionSet n x ×ˢ seq m) / (ν a) (countablePartitionSet n x)).toReal) atTop (𝓝 ((κ a) (countablePartitionSet n x ×ˢ ∅) / (ν a) (countablePartitionSet n x)).toReal)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ✝ : Kernel α (γ × β)<VAR>ν✝ : Kernel α γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>inst✝ : IsFiniteKernel κ<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>seq : ℕ → Set β<VAR>hseq : Antitone seq<VAR>hseq_iInter : ⋂ i, seq i = ∅<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<VAR>h0 : ¬(ν a) (countablePartitionSet n x) = 0<GOAL>(κ a) (countablePartitionSet n x ×ˢ ∅) / (ν a) (countablePartitionSet n x) ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ✝ : Kernel α (γ × β)<VAR>ν✝ : Kernel α γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>inst✝ : IsFiniteKernel κ<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>seq : ℕ → Set β<VAR>hseq : Antitone seq<VAR>hseq_iInter : ⋂ i, seq i = ∅<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<VAR>h0 : ¬(ν a) (countablePartitionSet n x) = 0<GOAL>Tendsto (fun m => (κ a) (countablePartitionSet n x ×ˢ seq m) / (ν a) (countablePartitionSet n x)) atTop (𝓝 ((κ a) (countablePartitionSet n x ×ˢ ∅) / (ν a) (countablePartitionSet n x)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ✝ : Kernel α (γ × β)<VAR>ν✝ : Kernel α γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>inst✝ : IsFiniteKernel κ<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>seq : ℕ → Set β<VAR>hseq : Antitone seq<VAR>hseq_iInter : ⋂ i, seq i = ∅<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<VAR>h0 : ¬(ν a) (countablePartitionSet n x) = 0<GOAL>Tendsto (fun m => (κ a) (countablePartitionSet n x ×ˢ seq m)) atTop (𝓝 ((κ a) (countablePartitionSet n x ×ˢ ∅)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ✝ : Kernel α (γ × β)<VAR>ν✝ : Kernel α γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>inst✝ : IsFiniteKernel κ<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>seq : ℕ → Set β<VAR>hseq : Antitone seq<VAR>hseq_iInter : ⋂ i, seq i = ∅<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<VAR>h0 : ¬(ν a) (countablePartitionSet n x) = 0<GOAL>(κ a) (countablePartitionSet n x ×ˢ ∅) ≠ 0 ∨ (ν a) (countablePartitionSet n x) ≠ 0
<VAR>k : ℕ<VAR>x : ℝ<GOAL>HasDerivAt (fun x => bernoulliFun (k + 1) x / (↑k + 1)) (bernoulliFun k x) x
<VAR>k : ℕ<VAR>x : ℝ<GOAL>bernoulliFun k x = ↑(k + 1) * bernoulliFun (k + 1 - 1) x / (↑k + 1)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>x : α<VAR>h✝ : x ∈ l<VAR>y : α<VAR>h : x ∈ y :: l<VAR>hy : x ≠ y<VAR>hx : x = (y :: l).getLast ⋯<VAR>hl : l.Nodup<GOAL>(y :: l).next x h = y
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>x : α<VAR>h✝ : x ∈ l<VAR>y : α<VAR>h : x ∈ y :: l<VAR>hy : x ≠ y<VAR>hx : x = (y :: l).getLast ⋯<VAR>hl : l.Nodup<GOAL>(y :: l).getLast ⋯ ∉ (y :: l).dropLast
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>y : α<VAR>hl : l.Nodup<VAR>h✝ : (y :: l).getLast ⋯ ∈ l<VAR>h : (y :: l).getLast ⋯ ∈ y :: l<VAR>hy : (y :: l).getLast ⋯ ≠ y<VAR>H : (y :: l).getLast ⋯ ∈ (y :: l).dropLast<GOAL>False
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>y : α<VAR>hl : l.Nodup<VAR>h✝ : (y :: l).getLast ⋯ ∈ l<VAR>h : (y :: l).getLast ⋯ ∈ y :: l<VAR>hy : (y :: l).getLast ⋯ ≠ y<VAR>H : (y :: l).getLast ⋯ ∈ (y :: l).dropLast<VAR>hk : 0 < (y :: l).dropLast.length<VAR>hk' : (y :: l).dropLast.get ⟨0, hk⟩ = (y :: l).getLast ⋯<GOAL>False
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>y : α<VAR>hl : l.Nodup<VAR>h✝ : (y :: l).getLast ⋯ ∈ l<VAR>h : (y :: l).getLast ⋯ ∈ y :: l<VAR>hy : (y :: l).getLast ⋯ ≠ y<VAR>H : (y :: l).getLast ⋯ ∈ (y :: l).dropLast<VAR>k : ℕ<VAR>hk : k + 1 < (y :: l).dropLast.length<VAR>hk' : (y :: l).dropLast.get ⟨k + 1, hk⟩ = (y :: l).getLast ⋯<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<GOAL>IsCoprime (FermatLastTheoremForThreeGen.Solution.Y S) (FermatLastTheoremForThreeGen.Solution.Z S)
<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>IsCoprime (FermatLastTheoremForThreeGen.Solution.y S) (FermatLastTheoremForThreeGen.Solution.z S)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s✝ s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>ι : Type u_3<VAR>f : ι → E → F<VAR>s : Finset ι<VAR>h : ∀ i ∈ s, ContDiff 𝕜 n fun x => f i x<GOAL>ContDiff 𝕜 n fun x => ∑ i ∈ s, f i x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s✝ s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>ι : Type u_3<VAR>f : ι → E → F<VAR>s : Finset ι<VAR>h : ∀ i ∈ s, ContDiffOn 𝕜 n (fun x => f i x) univ<GOAL>ContDiffOn 𝕜 n (fun x => ∑ i ∈ s, f i x) univ
<VAR>o₁ o₂ : Ordinal.{u_1}<GOAL>aleph o₁ * aleph o₂ = aleph (max o₁ o₂)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>f : R[X]<GOAL>I.polynomialQuotientEquivQuotientPolynomial (Polynomial.map (Quotient.mk I) f) = (Quotient.mk (map C I)) f
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>f : R[X]<GOAL>I.polynomialQuotientEquivQuotientPolynomial.symm (I.polynomialQuotientEquivQuotientPolynomial (Polynomial.map (Quotient.mk I) f)) = I.polynomialQuotientEquivQuotientPolynomial.symm ((Quotient.mk (map C I)) f)
<VAR>M : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝² : CancelCommMonoidWithZero N<VAR>inst✝¹ : UniqueFactorizationMonoid N<VAR>inst✝ : UniqueFactorizationMonoid M<VAR>m p : Associates M<VAR>n : Associates N<VAR>hn : n ≠ 0<VAR>hp : p ∈ normalizedFactors m<VAR>d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)<VAR>s : ℕ<VAR>hs' : p ^ s ≤ m<VAR>hs : ¬s = 0<GOAL>↑(d ⟨p, ⋯⟩) ^ s ≤ n
<VAR>M : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝² : CancelCommMonoidWithZero N<VAR>inst✝¹ : UniqueFactorizationMonoid N<VAR>inst✝ : UniqueFactorizationMonoid M<VAR>m p : Associates M<VAR>n : Associates N<VAR>hn : n ≠ 0<VAR>hp : p ∈ normalizedFactors m<VAR>d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)<VAR>s : ℕ<VAR>hs' : p ^ s ≤ m<VAR>hs : ¬s = 0<GOAL>↑(d ⟨p, ⋯⟩) ^ s = ↑(d ⟨p ^ s, hs'⟩)
<VAR>M : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝² : CancelCommMonoidWithZero N<VAR>inst✝¹ : UniqueFactorizationMonoid N<VAR>inst✝ : UniqueFactorizationMonoid M<VAR>m : Associates M<VAR>n : Associates N<VAR>hn : n ≠ 0<VAR>d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)<VAR>s : ℕ<VAR>hs : ¬s = 0<VAR>c₁ : Fin (s + 1) → Associates M<VAR>hp : c₁ 1 ∈ normalizedFactors m<VAR>hs' : c₁ 1 ^ s ≤ m<VAR>hc₁' : StrictMono c₁<VAR>hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i<GOAL>↑(d ⟨c₁ 1, ⋯⟩) ^ s = ↑(d ⟨c₁ 1 ^ s, hs'⟩)
<VAR>M : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝² : CancelCommMonoidWithZero N<VAR>inst✝¹ : UniqueFactorizationMonoid N<VAR>inst✝ : UniqueFactorizationMonoid M<VAR>m : Associates M<VAR>n : Associates N<VAR>hn : n ≠ 0<VAR>d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)<VAR>s : ℕ<VAR>hs : ¬s = 0<VAR>c₁ : Fin (s + 1) → Associates M<VAR>hp : c₁ 1 ∈ normalizedFactors m<VAR>hs' : c₁ 1 ^ s ≤ m<VAR>hc₁' : StrictMono c₁<VAR>hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i<VAR>c₂ : Fin (s + 1) → Associates N := fun t => ↑(d ⟨c₁ t, ⋯⟩)<GOAL>↑(d ⟨c₁ 1, ⋯⟩) ^ s = ↑(d ⟨c₁ 1 ^ s, hs'⟩)
<VAR>M : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝² : CancelCommMonoidWithZero N<VAR>inst✝¹ : UniqueFactorizationMonoid N<VAR>inst✝ : UniqueFactorizationMonoid M<VAR>m : Associates M<VAR>n : Associates N<VAR>hn : n ≠ 0<VAR>d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)<VAR>s : ℕ<VAR>hs : ¬s = 0<VAR>c₁ : Fin (s + 1) → Associates M<VAR>hp : c₁ 1 ∈ normalizedFactors m<VAR>hs' : c₁ 1 ^ s ≤ m<VAR>hc₁' : StrictMono c₁<VAR>hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i<VAR>c₂ : Fin (s + 1) → Associates N := fun t => ↑(d ⟨c₁ t, ⋯⟩)<VAR>c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(d ⟨c₁ t, ⋯⟩)<GOAL>c₂ 1 ^ s = ↑(d ⟨c₁ 1 ^ s, hs'⟩)
<VAR>M : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝² : CancelCommMonoidWithZero N<VAR>inst✝¹ : UniqueFactorizationMonoid N<VAR>inst✝ : UniqueFactorizationMonoid M<VAR>m : Associates M<VAR>n : Associates N<VAR>hn : n ≠ 0<VAR>d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)<VAR>s : ℕ<VAR>hs : ¬s = 0<VAR>c₁ : Fin (s + 1) → Associates M<VAR>hp : c₁ 1 ∈ normalizedFactors m<VAR>hs' : c₁ 1 ^ s ≤ m<VAR>hc₁' : StrictMono c₁<VAR>hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i<VAR>c₂ : Fin (s + 1) → Associates N := fun t => ↑(d ⟨c₁ t, ⋯⟩)<VAR>c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(d ⟨c₁ t, ⋯⟩)<VAR>t u : Fin (s + 1)<VAR>h : t < u<GOAL>c₂ t < c₂ u
<VAR>M : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝² : CancelCommMonoidWithZero N<VAR>inst✝¹ : UniqueFactorizationMonoid N<VAR>inst✝ : UniqueFactorizationMonoid M<VAR>m : Associates M<VAR>n : Associates N<VAR>hn : n ≠ 0<VAR>d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)<VAR>s : ℕ<VAR>hs : ¬s = 0<VAR>c₁ : Fin (s + 1) → Associates M<VAR>hp : c₁ 1 ∈ normalizedFactors m<VAR>hs' : c₁ 1 ^ s ≤ m<VAR>hc₁' : StrictMono c₁<VAR>hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i<VAR>c₂ : Fin (s + 1) → Associates N := fun t => ↑(d ⟨c₁ t, ⋯⟩)<VAR>c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(d ⟨c₁ t, ⋯⟩)<VAR>r : Associates N<VAR>hr : r ≤ ↑(d ⟨c₁ 1 ^ s, hs'⟩)<GOAL>∃ i, r = c₂ i
<VAR>M : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝² : CancelCommMonoidWithZero N<VAR>inst✝¹ : UniqueFactorizationMonoid N<VAR>inst✝ : UniqueFactorizationMonoid M<VAR>m : Associates M<VAR>n : Associates N<VAR>hn : n ≠ 0<VAR>d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)<VAR>s : ℕ<VAR>hs : ¬s = 0<VAR>c₁ : Fin (s + 1) → Associates M<VAR>hp : c₁ 1 ∈ normalizedFactors m<VAR>hs' : c₁ 1 ^ s ≤ m<VAR>hc₁' : StrictMono c₁<VAR>hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i<VAR>c₂ : Fin (s + 1) → Associates N := fun t => ↑(d ⟨c₁ t, ⋯⟩)<VAR>c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(d ⟨c₁ t, ⋯⟩)<VAR>r : Associates N<GOAL>(∃ i, r = c₂ i) → r ≤ ↑(d ⟨c₁ 1 ^ s, hs'⟩)
<VAR>M : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝² : CancelCommMonoidWithZero N<VAR>inst✝¹ : UniqueFactorizationMonoid N<VAR>inst✝ : UniqueFactorizationMonoid M<VAR>m : Associates M<VAR>n : Associates N<VAR>hn : n ≠ 0<VAR>d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)<VAR>s : ℕ<VAR>hs : ¬s = 0<VAR>c₁ : Fin (s + 1) → Associates M<VAR>hp : c₁ 1 ∈ normalizedFactors m<VAR>hs' : c₁ 1 ^ s ≤ m<VAR>hc₁' : StrictMono c₁<VAR>hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i<VAR>c₂ : Fin (s + 1) → Associates N := fun t => ↑(d ⟨c₁ t, ⋯⟩)<VAR>c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(d ⟨c₁ t, ⋯⟩)<GOAL>↑(d ⟨c₁ 1 ^ s, hs'⟩) ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>f : α →₀ M<GOAL>⇑f = 0 ↔ f = 0
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>h : 0 ≤ ε<GOAL>x ∈ closedBall x ε
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Semiring β<VAR>a b : α<VAR>m n✝ : ℕ<VAR>ha : Even a<VAR>n : ℕ<VAR>x✝ : n + 1 ≠ 0<GOAL>Even (a ^ (n + 1))
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Semiring β<VAR>a b : α<VAR>m n✝ : ℕ<VAR>ha : Even a<VAR>n : ℕ<VAR>x✝ : n + 1 ≠ 0<GOAL>Even (a ^ n * a)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<GOAL>(o.blsub f).cof ≤ Cardinal.lift.{v, u} o.card
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<GOAL>(o.blsub f).cof ≤ Cardinal.lift.{v, u} #(Quotient.out o).α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort u_6<VAR>s t u : Set α<VAR>S : Set (Set α)<GOAL>generateFrom (insert ∅ S) = generateFrom S
<VAR>M : Type w<VAR>A : Set M<VAR>L : Language<VAR>inst✝ : L.Structure M<VAR>α : Type u₁<VAR>β : Type u_1<VAR>B : Set M<VAR>s : Set (α → M)<GOAL>A.Definable L s ↔ ∃ φ, s = {v | φ.Realize (Sum.elim Subtype.val v)}
<VAR>M : Type w<VAR>A : Set M<VAR>L : Language<VAR>inst✝ : L.Structure M<VAR>α : Type u₁<VAR>β : Type u_1<VAR>B : Set M<VAR>s : Set (α → M)<GOAL>(∃ b, s = setOf (Formula.Realize (BoundedFormula.constantsVarsEquiv.symm b))) ↔ ∃ φ, s = {v | φ.Realize (Sum.elim Subtype.val v)}
<VAR>M : Type w<VAR>A : Set M<VAR>L : Language<VAR>inst✝ : L.Structure M<VAR>α : Type u₁<VAR>β : Type u_1<VAR>B : Set M<VAR>s : Set (α → M)<VAR>φ : L.BoundedFormula (↑A ⊕ α) 0<VAR>x✝ : α → M<GOAL>x✝ ∈ setOf (Formula.Realize (BoundedFormula.constantsVarsEquiv.symm φ)) ↔ x✝ ∈ {v | Formula.Realize φ (Sum.elim Subtype.val v)}
<VAR>M : Type w<VAR>A : Set M<VAR>L : Language<VAR>inst✝ : L.Structure M<VAR>α : Type u₁<VAR>β : Type u_1<VAR>B : Set M<VAR>s : Set (α → M)<VAR>φ : L.BoundedFormula (↑A ⊕ α) 0<VAR>x✝ : α → M<GOAL>(BoundedFormula.mapTermRel (fun n => ⇑Term.constantsVarsEquivLeft.symm) (fun n => ⇑(Equiv.sumEmpty (L.Relations n) (Sequence₂ PEmpty.{1} PEmpty.{1} PEmpty.{1} n)).symm) (fun x => id) φ).Realize x✝ default ↔ φ.Realize (Sum.elim Subtype.val x✝) default
<VAR>M : Type w<VAR>A : Set M<VAR>L : Language<VAR>inst✝ : L.Structure M<VAR>α : Type u₁<VAR>β : Type u_1<VAR>B : Set M<VAR>s : Set (α → M)<VAR>φ : L.BoundedFormula (↑A ⊕ α) 0<VAR>x✝ : α → M<GOAL>∀ (n : ℕ) (t : L.Term ((↑A ⊕ α) ⊕ Fin n)) (xs : Fin n → M), Term.realize (Sum.elim x✝ xs) (Term.constantsVarsEquivLeft.symm t) = Term.realize (Sum.elim (Sum.elim Subtype.val x✝) xs) t
<VAR>M : Type w<VAR>A : Set M<VAR>L : Language<VAR>inst✝ : L.Structure M<VAR>α : Type u₁<VAR>β : Type u_1<VAR>B : Set M<VAR>s : Set (α → M)<VAR>φ : L.BoundedFormula (↑A ⊕ α) 0<VAR>x✝ : α → M<VAR>n✝ : ℕ<VAR>t✝ : L.Term ((↑A ⊕ α) ⊕ Fin n✝)<VAR>xs✝ : Fin n✝ → M<GOAL>Term.realize (Sum.elim x✝ xs✝) (Term.constantsVarsEquivLeft.symm t✝) = Term.realize (Sum.elim (Sum.elim Subtype.val x✝) xs✝) t✝
<VAR>M : Type w<VAR>A : Set M<VAR>L : Language<VAR>inst✝ : L.Structure M<VAR>α : Type u₁<VAR>β : Type u_1<VAR>B : Set M<VAR>s : Set (α → M)<VAR>φ : L.BoundedFormula (↑A ⊕ α) 0<VAR>x✝ : α → M<VAR>n✝ : ℕ<VAR>t✝ : L.Term ((↑A ⊕ α) ⊕ Fin n✝)<VAR>xs✝ : Fin n✝ → M<GOAL>Term.realize (Sum.elim (fun a => ↑a) (Sum.elim x✝ xs✝) ∘ ⇑(Equiv.sumAssoc (↑A) α (Fin n✝))) t✝ = Term.realize (Sum.elim (Sum.elim Subtype.val x✝) xs✝) t✝
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>x : P<VAR>hx : x ∉ s<VAR>p : P<VAR>hp : p ∈ ↑s<VAR>this : Nonempty ↥s<GOAL>IsConnected {y | s.SOppSide x y}
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>x : P<VAR>hx : x ∉ s<VAR>p : P<VAR>hp : p ∈ ↑s<VAR>this : Nonempty ↥s<GOAL>IsConnected ((fun x_1 => x_1.1 • (x -ᵥ p) +ᵥ x_1.2) '' Set.Iio 0 ×ˢ ↑s)
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>K : Type u_3<VAR>C : Type u_4<VAR>inst✝⁴ : Category.{u_5, u_4} C<VAR>X Y Z : GradedObject I C<VAR>φ : X ⟶ Y<VAR>e : X ≅ Y<VAR>ψ : Y ⟶ Z<VAR>p : I → J<VAR>j : J<VAR>inst✝³ : X.HasMap p<VAR>inst✝² : Y.HasMap p<VAR>inst✝¹ : Z.HasMap p<VAR>c : X.CofanMapObjFun p j<VAR>hc : IsColimit c<VAR>inst✝ : X.HasMap p<VAR>i : I<VAR>hi : p i = j<GOAL>X.ιMapObj p i j hi ≫ (iso hc).inv = Cofan.inj c ⟨i, hi⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>x✝¹ : Fin 0 → α → σ<VAR>x✝ : ∀ (i : Fin 0), Computable (x✝¹ i)<GOAL>Computable fun a => List.ofFn fun i => x✝¹ i a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>x✝¹ : Fin 0 → α → σ<VAR>x✝ : ∀ (i : Fin 0), Computable (x✝¹ i)<GOAL>Computable fun a => []
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>n : ℕ<VAR>f : Fin (n + 1) → α → σ<VAR>hf : ∀ (i : Fin (n + 1)), Computable (f i)<GOAL>Computable fun a => List.ofFn fun i => f i a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>n : ℕ<VAR>f : Fin (n + 1) → α → σ<VAR>hf : ∀ (i : Fin (n + 1)), Computable (f i)<GOAL>Computable fun a => f 0 a :: List.ofFn fun i => f i.succ a
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>n : ℕ<VAR>ha : a ≠ 0<GOAL>((monomial n) a).degree = ↑n
<VAR>α : Type u_1<VAR>a : α<VAR>n m : Nat<VAR>l : List α<VAR>h : m < n<VAR>i : Nat<GOAL>(take m (l.set n a))[i]? = (take m l)[i]?
<VAR>α : Type u_1<VAR>a : α<VAR>n m : Nat<VAR>l : List α<VAR>h : m < n<VAR>i : Nat<GOAL>(if i < m then (l.set n a)[i]? else none) = if i < m then l[i]? else none
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>R X Y Z : C<VAR>f : X ⟶ Y<VAR>a b : R ⟶ X<VAR>f₁ : X ⟶ Y<VAR>f₂ : Y ⟶ Z<VAR>inst✝ : Mono f₂<VAR>small_k : IsKernelPair f₁ a b<GOAL>IsLimit (PullbackCone.mk a b ⋯)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>R X Y Z : C<VAR>f : X ⟶ Y<VAR>a b : R ⟶ X<VAR>f₁ : X ⟶ Y<VAR>f₂ : Y ⟶ Z<VAR>inst✝ : Mono f₂<VAR>small_k : IsKernelPair f₁ a b<GOAL>∀ (s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)) (m : s.pt ⟶ (PullbackCone.mk a b ⋯).pt), (∀ (j : WalkingCospan), m ≫ (PullbackCone.mk a b ⋯).π.app j = s.π.app j) → m = (fun s => small_k.lift s.fst s.snd ⋯) s
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>R X Y Z : C<VAR>f : X ⟶ Y<VAR>a b : R ⟶ X<VAR>f₁ : X ⟶ Y<VAR>f₂ : Y ⟶ Z<VAR>inst✝ : Mono f₂<VAR>small_k : IsKernelPair f₁ a b<VAR>s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)<VAR>m : s.pt ⟶ (PullbackCone.mk a b ⋯).pt<VAR>hm : ∀ (j : WalkingCospan), m ≫ (PullbackCone.mk a b ⋯).π.app j = s.π.app j<GOAL>m = (fun s => small_k.lift s.fst s.snd ⋯) s
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>R X Y Z : C<VAR>f : X ⟶ Y<VAR>a b : R ⟶ X<VAR>f₁ : X ⟶ Y<VAR>f₂ : Y ⟶ Z<VAR>inst✝ : Mono f₂<VAR>small_k : IsKernelPair f₁ a b<VAR>s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)<VAR>m : s.pt ⟶ (PullbackCone.mk a b ⋯).pt<VAR>hm : ∀ (j : WalkingCospan), m ≫ (PullbackCone.mk a b ⋯).π.app j = s.π.app j<GOAL>∀ (j : WalkingCospan), m ≫ (IsPullback.cone small_k).π.app j = (fun s => small_k.lift s.fst s.snd ⋯) s ≫ (IsPullback.cone small_k).π.app j
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>R X Y Z : C<VAR>f : X ⟶ Y<VAR>a b : R ⟶ X<VAR>f₁ : X ⟶ Y<VAR>f₂ : Y ⟶ Z<VAR>inst✝ : Mono f₂<VAR>small_k : IsKernelPair f₁ a b<VAR>s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)<VAR>m : s.pt ⟶ (PullbackCone.mk a b ⋯).pt<VAR>hm : ∀ (j : WalkingCospan), m ≫ (PullbackCone.mk a b ⋯).π.app j = s.π.app j<GOAL>m ≫ (IsPullback.cone small_k).fst = (fun s => small_k.lift s.fst s.snd ⋯) s ≫ (IsPullback.cone small_k).fst
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>R X Y Z : C<VAR>f : X ⟶ Y<VAR>a b : R ⟶ X<VAR>f₁ : X ⟶ Y<VAR>f₂ : Y ⟶ Z<VAR>inst✝ : Mono f₂<VAR>small_k : IsKernelPair f₁ a b<VAR>s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)<VAR>m : s.pt ⟶ (PullbackCone.mk a b ⋯).pt<VAR>hm : ∀ (j : WalkingCospan), m ≫ (PullbackCone.mk a b ⋯).π.app j = s.π.app j<GOAL>m ≫ (IsPullback.cone small_k).snd = (fun s => small_k.lift s.fst s.snd ⋯) s ≫ (IsPullback.cone small_k).snd
<VAR>a b c : Ordinal.{u_1}<VAR>a0 : a ≠ 0<VAR>h : b.IsLimit<GOAL>a ^ b ≤ c ↔ ∀ b' < b, a ^ b' ≤ c
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>hv : v ≠ 0<VAR>s : Set ℝ<GOAL>(gaussianReal μ v) s = ENNReal.ofReal (∫ (x : ℝ) in s, gaussianPDFReal μ v x)
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>hv : v ≠ 0<VAR>s : Set ℝ<GOAL>∫⁻ (x : ℝ) in s, gaussianPDF μ v x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (gaussianPDFReal μ v x)
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>hv : v ≠ 0<VAR>s : Set ℝ<GOAL>Integrable (gaussianPDFReal μ v) (ℙ.restrict s)
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>hv : v ≠ 0<VAR>s : Set ℝ<GOAL>0 ≤ᶠ[ae (ℙ.restrict s)] gaussianPDFReal μ v