ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁹ : NormedField 𝕜<VAR>inst✝⁸ : NormedRing A<VAR>inst✝⁷ : NormedAlgebra 𝕜 A<VAR>inst✝⁶ : CompleteSpace A<VAR>B : Type u_3<VAR>inst✝⁵ : NonUnitalNormedRing B<VAR>inst✝⁴ : NormedSpace 𝕜 B<VAR>inst✝³ : CompleteSpace B<VAR>inst✝² : IsScalarTower 𝕜 B B<VAR>inst✝¹ : SMulCommClass 𝕜 B B<VAR>inst✝ : ProperSpace 𝕜<VAR>a : B<GOAL>IsCompact (quasispectrum 𝕜 a)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁹ : NormedField 𝕜<VAR>inst✝⁸ : NormedRing A<VAR>inst✝⁷ : NormedAlgebra 𝕜 A<VAR>inst✝⁶ : CompleteSpace A<VAR>B : Type u_3<VAR>inst✝⁵ : NonUnitalNormedRing B<VAR>inst✝⁴ : NormedSpace 𝕜 B<VAR>inst✝³ : CompleteSpace B<VAR>inst✝² : IsScalarTower 𝕜 B B<VAR>inst✝¹ : SMulCommClass 𝕜 B B<VAR>inst✝ : ProperSpace 𝕜<VAR>a : B<GOAL>IsCompact (σ ((WithLp.unitizationAlgEquiv 𝕜).symm ↑a))
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsBezout R<VAR>a b c : R<VAR>hab : IsCoprime a b<VAR>k : ℕ<VAR>h : Associated (c ^ k) (a * b)<GOAL>∃ d, Associated (d ^ k) a
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsBezout R<VAR>a b c : R<VAR>hab : IsCoprime a b<VAR>k : ℕ<VAR>h : Associated (c ^ k) (a * b)<VAR>u : Rˣ<VAR>hu : a * b * ↑u = c ^ k<GOAL>∃ d, Associated (d ^ k) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r✝ r₁ r₂ : α → α → Prop<VAR>s✝ t : Set α<VAR>a b x✝ : α<VAR>f✝ : α → β<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>y : Set β<VAR>x : Set α<VAR>f : r ↪r s<VAR>h : y ⊆ ⇑f '' x<GOAL>x ∩ ⇑f ⁻¹' maximals s y = maximals r (x ∩ ⇑f ⁻¹' y)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : MeasurableSpace Y<VAR>inst✝⁵ : TopologicalSpace Y<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>f✝ g✝ : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>inst✝ : T2Space X<VAR>f : X → ℝ<VAR>hf : LocallyIntegrable f μ<VAR>g : X → E<VAR>hg : Continuous g<VAR>h'g : HasCompactSupport g<VAR>K : Set X := tsupport g<VAR>hK : IsCompact K<GOAL>Integrable (fun x => f x • g x) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : MeasurableSpace Y<VAR>inst✝⁵ : TopologicalSpace Y<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>f✝ g✝ : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>inst✝ : T2Space X<VAR>f : X → ℝ<VAR>hf : LocallyIntegrable f μ<VAR>g : X → E<VAR>hg : Continuous g<VAR>h'g : HasCompactSupport g<VAR>K : Set X := tsupport g<VAR>hK : IsCompact K<VAR>this : (K.indicator fun x => f x • g x) = fun x => f x • g x<GOAL>Integrable (fun x => f x • g x) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : MeasurableSpace Y<VAR>inst✝⁵ : TopologicalSpace Y<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>f✝ g✝ : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>inst✝ : T2Space X<VAR>f : X → ℝ<VAR>hf : LocallyIntegrable f μ<VAR>g : X → E<VAR>hg : Continuous g<VAR>h'g : HasCompactSupport g<VAR>K : Set X := tsupport g<VAR>hK : IsCompact K<VAR>this : (K.indicator fun x => f x • g x) = fun x => f x • g x<GOAL>Integrable (fun a => K.indicator f a • g a) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : MeasurableSpace Y<VAR>inst✝⁵ : TopologicalSpace Y<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>f✝ g✝ : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>inst✝ : T2Space X<VAR>f : X → ℝ<VAR>hf : LocallyIntegrable f μ<VAR>g : X → E<VAR>hg : Continuous g<VAR>h'g : HasCompactSupport g<VAR>K : Set X := tsupport g<VAR>hK : IsCompact K<VAR>this : (K.indicator fun x => f x • g x) = fun x => f x • g x<GOAL>Integrable (K.indicator f) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : MeasurableSpace Y<VAR>inst✝⁵ : TopologicalSpace Y<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>f✝ g✝ : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>inst✝ : T2Space X<VAR>f : X → ℝ<VAR>hf : LocallyIntegrable f μ<VAR>g : X → E<VAR>hg : Continuous g<VAR>h'g : HasCompactSupport g<VAR>K : Set X := tsupport g<VAR>hK : IsCompact K<VAR>this : (K.indicator fun x => f x • g x) = fun x => f x • g x<GOAL>Memℒp g ⊤ μ
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>⟪o.rightAngleRotation x, y⟫_ℝ = -⟪x, o.rightAngleRotation y⟫_ℝ
<VAR>m n : ℕ<GOAL>↑(m % n) = ↑m % ↑n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : Zero α<VAR>inst✝³ : Zero β<VAR>inst✝² : SMulWithZero α β<VAR>inst✝¹ : DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>inst✝ : NoZeroSMulDivisors α β<VAR>a : α<GOAL>0 ∈ s • t ↔ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : Zero α<VAR>inst✝³ : Zero β<VAR>inst✝² : SMulWithZero α β<VAR>inst✝¹ : DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>inst✝ : NoZeroSMulDivisors α β<VAR>a : α<GOAL>0 ∈ ↑s ∧ (↑t).Nonempty ∨ 0 ∈ ↑t ∧ (↑s).Nonempty ↔ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h : IsPrimitiveRoot ζ✝ k<VAR>inst✝ : IsDomain R<VAR>ζ : R<VAR>hζ : IsPrimitiveRoot ζ k<VAR>hk : 1 < k<GOAL>∑ i ∈ range k, ζ ^ i = 0
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h : IsPrimitiveRoot ζ✝ k<VAR>inst✝ : IsDomain R<VAR>ζ : R<VAR>hζ : IsPrimitiveRoot ζ k<VAR>hk : 1 < k<GOAL>(1 - ζ) * ∑ i ∈ range k, ζ ^ i = 0
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ConcaveOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<GOAL>(f z - f y) / (z - y) ≤ (f y - f x) / (y - x)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ConcaveOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<VAR>this : -(((-f) z - (-f) y) / (z - y)) ≤ -(((-f) y - (-f) x) / (y - x))<GOAL>(f z - f y) / (z - y) ≤ (f y - f x) / (y - x)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ConcaveOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<VAR>this : (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)<GOAL>(f z - f y) / (z - y) ≤ (f y - f x) / (y - x)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>s : PullbackCone f g<VAR>i : 𝒰.J<GOAL>(pullbackP1Iso 𝒰 f g i).hom ≫ pullback.fst (𝒰.map i ≫ f) g = pullback.snd (p1 𝒰 f g) (𝒰.map i)
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℕ<VAR>n k : ℕ<GOAL>n.descFactorial (k + 1) = ∏ i ∈ range (k + 1), (n - i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>f g : α → β<VAR>inst✝¹ : Add β<VAR>inst✝ : ContinuousAdd β<VAR>f' : α → β<VAR>h_f'_meas : StronglyMeasurable f'<VAR>hff' : f =ᶠ[ae μ] f'<VAR>g' : α → β<VAR>h_g'_meas : StronglyMeasurable g'<VAR>hgg' : g =ᶠ[ae μ] g'<GOAL>AEStronglyMeasurable' m (f + g) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>inst✝ : CompleteLattice β<VAR>s : Set (Set β)<GOAL>sSup (⋃₀ s) = ⨆ t ∈ s, sSup t
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<GOAL>a / 2 ≤ a ↔ 0 ≤ a
<VAR>M : Type u_1<VAR>inst✝⁵ : Zero M<VAR>l : List M<VAR>inst✝⁴ : DecidablePred fun x => l.getD x 0 ≠ 0<VAR>n✝ : ℕ<VAR>R : Type u_2<VAR>inst✝³ : AddZeroClass R<VAR>l₁ l₂ : List R<VAR>inst✝² : DecidablePred fun x => (l₁ ++ l₂).getD x 0 ≠ 0<VAR>inst✝¹ : DecidablePred fun x => l₁.getD x 0 ≠ 0<VAR>inst✝ : DecidablePred fun x => l₂.getD x 0 ≠ 0<VAR>n : ℕ<GOAL>(l₁ ++ l₂).toFinsupp n = (l₁.toFinsupp + Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp) n
<VAR>M : Type u_1<VAR>inst✝⁵ : Zero M<VAR>l : List M<VAR>inst✝⁴ : DecidablePred fun x => l.getD x 0 ≠ 0<VAR>n✝ : ℕ<VAR>R : Type u_2<VAR>inst✝³ : AddZeroClass R<VAR>l₁ l₂ : List R<VAR>inst✝² : DecidablePred fun x => (l₁ ++ l₂).getD x 0 ≠ 0<VAR>inst✝¹ : DecidablePred fun x => l₁.getD x 0 ≠ 0<VAR>inst✝ : DecidablePred fun x => l₂.getD x 0 ≠ 0<VAR>n : ℕ<GOAL>(l₁ ++ l₂).getD n 0 = l₁.getD n 0 + (Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp) n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² inst✝¹ : Group α<VAR>inst✝ : MulAction α β<VAR>x : β<VAR>y₁ y₂ : α ⧸ stabilizer α x<VAR>g₁ g₂ : α<VAR>H : g₁ • x = g₂ • x<GOAL>Setoid.r g₁ g₂
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² inst✝¹ : Group α<VAR>inst✝ : MulAction α β<VAR>x : β<VAR>y₁ y₂ : α ⧸ stabilizer α x<VAR>g₁ g₂ : α<VAR>H : g₁ • x = g₂ • x<GOAL>g₁⁻¹ * g₂ ∈ stabilizer α x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² inst✝¹ : Group α<VAR>inst✝ : MulAction α β<VAR>x : β<VAR>y₁ y₂ : α ⧸ stabilizer α x<VAR>g₁ g₂ : α<VAR>H : g₁ • x = g₂ • x<GOAL>(g₁⁻¹ * g₂) • x = x
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>ncs : CauSeq ℤ_[p] norm<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>ncs_der_val : ∀ (n : ℕ), ‖Polynomial.eval (↑ncs n) (Polynomial.derivative F)‖ = ‖Polynomial.eval a (Polynomial.derivative F)‖<GOAL>Tendsto (fun i => ‖Polynomial.eval (↑ncs i) (Polynomial.derivative F)‖) atTop (𝓝 ‖Polynomial.eval a (Polynomial.derivative F)‖)
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>ncs : CauSeq ℤ_[p] norm<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>ncs_der_val : ∀ (n : ℕ), ‖Polynomial.eval (↑ncs n) (Polynomial.derivative F)‖ = ‖Polynomial.eval a (Polynomial.derivative F)‖<VAR>x✝ : ℕ<GOAL>‖Polynomial.eval (↑ncs x✝) (Polynomial.derivative F)‖ = ‖Polynomial.eval a (Polynomial.derivative F)‖
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : MetricSpace E<VAR>f✝ : ℕ → α → E<VAR>g✝ : α → E<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>f : ι → α → E<VAR>g : α → E<VAR>hfg : TendstoInMeasure μ f u g<GOAL>∃ ns, ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : MetricSpace E<VAR>f✝ : ℕ → α → E<VAR>g✝ : α → E<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>f : ι → α → E<VAR>g : α → E<VAR>hfg : TendstoInMeasure μ f u g<VAR>ms : ℕ → ι<VAR>hms : TendstoInMeasure μ (fun n => f (ms n)) atTop g<GOAL>∃ ns, ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : MetricSpace E<VAR>f✝ : ℕ → α → E<VAR>g✝ : α → E<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>f : ι → α → E<VAR>g : α → E<VAR>hfg : TendstoInMeasure μ f u g<VAR>ms : ℕ → ι<VAR>hms : TendstoInMeasure μ (fun n => f (ms n)) atTop g<VAR>ns : ℕ → ℕ<VAR>hns : ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ms (ns i)) x) atTop (𝓝 (g x))<GOAL>∃ ns, ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
<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>K : Type u_3<VAR>K' : Type u_4<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field K'<VAR>inst✝⁴ : Algebra R K<VAR>inst✝³ : IsFractionRing R K<VAR>inst✝² : Algebra R K'<VAR>inst✝¹ : IsFractionRing R K'<VAR>I J : FractionalIdeal R⁰ K<VAR>h : K →ₐ[R] K'<VAR>inst✝ : Nontrivial R<VAR>hI : I ≠ 0<GOAL>map h I ≠ 0
<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>K : Type u_3<VAR>K' : Type u_4<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field K'<VAR>inst✝⁴ : Algebra R K<VAR>inst✝³ : IsFractionRing R K<VAR>inst✝² : Algebra R K'<VAR>inst✝¹ : IsFractionRing R K'<VAR>I J : FractionalIdeal R⁰ K<VAR>h : K →ₐ[R] K'<VAR>inst✝ : Nontrivial R<VAR>hI : I ≠ 0<VAR>x : R<VAR>x_ne_zero : x ≠ 0<VAR>hx : (algebraMap R K) x ∈ I<GOAL>map h I ≠ 0
<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>K : Type u_3<VAR>K' : Type u_4<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field K'<VAR>inst✝⁴ : Algebra R K<VAR>inst✝³ : IsFractionRing R K<VAR>inst✝² : Algebra R K'<VAR>inst✝¹ : IsFractionRing R K'<VAR>I J : FractionalIdeal R⁰ K<VAR>h : K →ₐ[R] K'<VAR>inst✝ : Nontrivial R<VAR>hI : I ≠ 0<VAR>x : R<VAR>hx : (algebraMap R K) x ∈ I<VAR>map_eq_zero : map h I = 0<GOAL>x = 0
<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>K : Type u_3<VAR>K' : Type u_4<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field K'<VAR>inst✝⁴ : Algebra R K<VAR>inst✝³ : IsFractionRing R K<VAR>inst✝² : Algebra R K'<VAR>inst✝¹ : IsFractionRing R K'<VAR>I J : FractionalIdeal R⁰ K<VAR>h : K →ₐ[R] K'<VAR>inst✝ : Nontrivial R<VAR>hI : I ≠ 0<VAR>x : R<VAR>hx : (algebraMap R K) x ∈ I<VAR>map_eq_zero : map h I = 0<GOAL>∃ x_1 ∈ I, h x_1 = (algebraMap R K') x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Mod α<VAR>a b : Part α<VAR>hab : (a % b).Dom<GOAL>(a % b).get hab = a.get ⋯ % b.get ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Mod α<VAR>a b : Part α<VAR>hab : (a % b).Dom<GOAL>(a.bind fun y => map (fun x => y % x) b).get ⋯ = a.get ⋯ % b.get ⋯
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CharP R 2<VAR>l : Multiset R<GOAL>l.sum * l.sum = (Multiset.map (fun x => x * x) l).sum
<VAR>p n : ℕ<VAR>hp : 1 < p<VAR>hn : 0 < n<GOAL>p.maxPowDiv (p * n) = p.maxPowDiv n + 1
<VAR>p n : ℕ<VAR>hp : 1 < p<VAR>hn : 0 < n<VAR>this : 0 < p<GOAL>p.maxPowDiv (p * n) = p.maxPowDiv n + 1
<VAR>p n : ℕ<VAR>hp : 1 < p<VAR>hn : 0 < n<VAR>this : 0 < p<GOAL>go 0 p (p * n) = go 0 p n + 1
<VAR>p n : ℕ<VAR>hp : 1 < p<VAR>hn : 0 < n<VAR>this : 0 < p<GOAL>go (0 + 1) p n = go 0 p n + 1
<VAR>p n : ℕ<VAR>hp : 1 < p<VAR>hn : 0 < n<VAR>this : 0 < p<GOAL>1 < p ∧ 0 < p * n ∧ p * n % p = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>w : ι' → ↑S.X₃<VAR>hv : ⊤ ≤ span R (range v)<VAR>hw : ⊤ ≤ span R (range w)<VAR>hE : Epi S.g<GOAL>⊤ ≤ span R (range (Sum.elim (⇑S.f ∘ v) (Function.invFun S.g.toFun ∘ w)))
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>w : ι' → ↑S.X₃<VAR>hv : ⊤ ≤ span R (range v)<VAR>hw : ⊤ ≤ span R (range w)<VAR>hE : Epi S.g<GOAL>Sum.elim (⇑S.f ∘ v) (Function.invFun S.g.toFun ∘ w) ∘ Sum.inl = ⇑S.f ∘ v
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>w : ι' → ↑S.X₃<VAR>hv : ⊤ ≤ span R (range v)<VAR>hw : ⊤ ≤ span R (range w)<VAR>hE : Epi S.g<GOAL>⊤ ≤ span R (range (⇑S.g ∘ Sum.elim (⇑S.f ∘ v) (Function.invFun S.g.toFun ∘ w) ∘ Sum.inr))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s t : Set α<VAR>x : α<GOAL>BddAbove ↑(lowerClosure s) ↔ BddAbove s
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A : Type u_2<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_3<VAR>inst✝ : Group N<VAR>a b k : ℤ<GOAL>(fun x => x • a) k = b ↔ b = a * k
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : StarRing R<VAR>x : R<VAR>hx : x ∈ skewAdjoint R<VAR>z : R<GOAL>z * x * star z ∈ skewAdjoint R
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>inst✝² : (x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq δ<VAR>s t : Finset δ<VAR>f✝ g : ((i : δ) → π i) → ℝ≥0∞<VAR>x✝ y : (i : δ) → π i<VAR>i✝ : δ<VAR>f : ((i : δ) → π i) → ℝ≥0∞<VAR>i : δ<VAR>α : Type u_1 := { x // x ∈ {i} }<VAR>e : π ↑default ≃ᵐ ((i_1 : α) → π ↑i_1) := (MeasurableEquiv.piUnique fun j => π ↑j).symm<VAR>x : (i : δ) → π i<GOAL>(∫⋯∫⁻_{i}, f ∂μ) x = ∫⁻ (xᵢ : π i), f (update x i xᵢ) ∂μ i
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module K M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<VAR>hI : IsAtom I<GOAL>(Φ.restrict (lieIdealSubalgebra K L (orthogonal Φ hΦ_inv I)).toSubmodule).Nondegenerate
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module K M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<VAR>hI : IsAtom I<GOAL>IsCompl (lieIdealSubalgebra K L (orthogonal Φ hΦ_inv I)).toSubmodule (Φ.orthogonal (lieIdealSubalgebra K L (orthogonal Φ hΦ_inv I)).toSubmodule)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module K M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<VAR>hI : IsAtom I<GOAL>IsCompl (Φ.orthogonal ↑I) ↑I
<VAR>a b n : ℕ<GOAL>a ^ n ∣ b ↔ a ∣ n.floorRoot b
<VAR>a b : ℕ<GOAL>a ^ 0 ∣ b ↔ a ∣ floorRoot 0 b
<VAR>a b n : ℕ<VAR>hn : n ≠ 0<GOAL>a ^ n ∣ b ↔ a ∣ n.floorRoot b
<VAR>a n : ℕ<VAR>hn : n ≠ 0<GOAL>a ^ n ∣ 0 ↔ a ∣ n.floorRoot 0
<VAR>a b n : ℕ<VAR>hn : n ≠ 0<VAR>hb : b ≠ 0<GOAL>a ^ n ∣ b ↔ a ∣ n.floorRoot b
<VAR>b n : ℕ<VAR>hn : n ≠ 0<VAR>hb : b ≠ 0<GOAL>0 ^ n ∣ b ↔ 0 ∣ n.floorRoot b
<VAR>a b n : ℕ<VAR>hn : n ≠ 0<VAR>hb : b ≠ 0<VAR>ha : a ≠ 0<GOAL>a ^ n ∣ b ↔ a ∣ n.floorRoot b
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a : α<VAR>h : a ≠ 0<GOAL>(Associates.mk a).factors = ↑(factors' a)
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X✝<VAR>X : Type u<VAR>inst✝ : TopologicalSpace X<GOAL>T0Space X ↔ Pairwise fun x y => ∃ U, IsOpen U ∧ Xor' (x ∈ U) (y ∈ U)
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : Ring 𝕜<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module 𝕜 V<VAR>inst✝¹ : TopologicalSpace P<VAR>inst✝ : AddTorsor V P<VAR>s t : Set P<VAR>x✝ x : P<GOAL>intrinsicClosure 𝕜 {x} = {x}
<VAR>p n : ℕ<VAR>hp : Nat.Prime p<VAR>hdiv : ¬p ∣ n<VAR>R : Type u_1<VAR>inst✝ : CommRing R<GOAL>(expand R p) (cyclotomic n R) = cyclotomic (n * p) R * cyclotomic n R
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>hdiv : ¬p ∣ 0<GOAL>(expand R p) (cyclotomic 0 R) = cyclotomic (0 * p) R * cyclotomic 0 R
<VAR>p n : ℕ<VAR>hp : Nat.Prime p<VAR>hdiv : ¬p ∣ n<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>hnpos : n > 0<GOAL>(expand R p) (cyclotomic n R) = cyclotomic (n * p) R * cyclotomic n R
<VAR>p n : ℕ<VAR>hp : Nat.Prime p<VAR>hdiv : ¬p ∣ n<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>hnpos : n > 0<VAR>this : NeZero n<GOAL>(expand R p) (cyclotomic n R) = cyclotomic (n * p) R * cyclotomic n R
<VAR>p n : ℕ<VAR>hp : Nat.Prime p<VAR>hdiv : ¬p ∣ n<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>hnpos : n > 0<VAR>this : NeZero n<GOAL>(expand ℤ p) (cyclotomic n ℤ) = cyclotomic (n * p) ℤ * cyclotomic n ℤ
<VAR>p n : ℕ<VAR>hp : Nat.Prime p<VAR>hdiv : ¬p ∣ n<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>hnpos : n > 0<VAR>this : NeZero n<GOAL>cyclotomic (n * p) ℤ * cyclotomic n ℤ ∣ (expand ℤ p) (cyclotomic n ℤ)
<VAR>p n : ℕ<VAR>hp : Nat.Prime p<VAR>hdiv : ¬p ∣ n<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>hnpos : n > 0<VAR>this : NeZero n<GOAL>((expand ℤ p) (cyclotomic n ℤ)).natDegree ≤ (cyclotomic (n * p) ℤ * cyclotomic n ℤ).natDegree
<VAR>ι : Type u_1<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L M K' L' : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>φ' : L ⟶ M<VAR>i : ι<VAR>inst✝² : K.HasHomology i<VAR>inst✝¹ : L.HasHomology i<VAR>inst✝ : M.HasHomology i<VAR>hφ' : QuasiIsoAt φ' i<VAR>hφφ' : QuasiIsoAt (φ ≫ φ') i<GOAL>QuasiIsoAt φ i
<VAR>ι : Type u_1<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L M K' L' : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>φ' : L ⟶ M<VAR>i : ι<VAR>inst✝² : K.HasHomology i<VAR>inst✝¹ : L.HasHomology i<VAR>inst✝ : M.HasHomology i<VAR>hφ' : IsIso (homologyMap φ' i)<VAR>hφφ' : IsIso (homologyMap (φ ≫ φ') i)<GOAL>IsIso (homologyMap φ i)
<VAR>ι : Type u_1<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L M K' L' : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>φ' : L ⟶ M<VAR>i : ι<VAR>inst✝² : K.HasHomology i<VAR>inst✝¹ : L.HasHomology i<VAR>inst✝ : M.HasHomology i<VAR>hφ' : IsIso (homologyMap φ' i)<VAR>hφφ' : IsIso (homologyMap φ i ≫ homologyMap φ' i)<GOAL>IsIso (homologyMap φ i)
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : Fintype ι'<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹¹ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹⁰ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁹ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁸ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁷ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁶ : SeminormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>inst✝⁴ : SeminormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>A : Type u_1<VAR>inst✝² : NormedCommRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : Nonempty ι<GOAL>‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ ≤ 1
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : Fintype ι'<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹¹ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹⁰ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁹ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁸ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁷ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁶ : SeminormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>inst✝⁴ : SeminormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>A : Type u_1<VAR>inst✝² : NormedCommRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : Nonempty ι<VAR>m : ι → A<GOAL>‖(ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) m‖ ≤ 1 * ∏ i : ι, ‖m i‖