ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝⁴ : TopologicalSpace B<VAR>inst✝³ : TopologicalSpace F<VAR>proj : Z → B<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace (TotalSpace F E)<VAR>e✝ : Trivialization F proj<VAR>x✝ : Z<VAR>X : Type u_6<VAR>inst✝ : TopologicalSpace X<VAR>f : X → Z<VAR>x : X<VAR>e : Trivialization F proj<VAR>hf_proj : ContinuousAt (proj ∘ f) x<VAR>he : proj (f x) ∈ e.baseSet<VAR>hf : ContinuousAt (↑e ∘ f) x<GOAL>f ⁻¹' e.source ∈ 𝓝 x
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝⁴ : TopologicalSpace B<VAR>inst✝³ : TopologicalSpace F<VAR>proj : Z → B<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace (TotalSpace F E)<VAR>e✝ : Trivialization F proj<VAR>x✝ : Z<VAR>X : Type u_6<VAR>inst✝ : TopologicalSpace X<VAR>f : X → Z<VAR>x : X<VAR>e : Trivialization F proj<VAR>hf_proj : ContinuousAt (proj ∘ f) x<VAR>he : proj (f x) ∈ e.baseSet<VAR>hf : ContinuousAt (↑e ∘ f) x<GOAL>proj ∘ f ⁻¹' e.baseSet ∈ 𝓝 x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : ProperSpace α<VAR>x : α<VAR>r : ℝ<VAR>s : Set α<VAR>hr : 0 < r<VAR>hs : IsClosed s<VAR>h : s ⊆ ball x r<GOAL>∃ r' ∈ Ioo 0 r, s ⊆ ball x r'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : ProperSpace α<VAR>x : α<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hs : IsClosed ∅<VAR>h : ∅ ⊆ ball x r<GOAL>∃ r' ∈ Ioo 0 r, ∅ ⊆ ball x r'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : ProperSpace α<VAR>x : α<VAR>r : ℝ<VAR>s : Set α<VAR>hr : 0 < r<VAR>hs : IsClosed s<VAR>h : s ⊆ ball x r<VAR>hne : s.Nonempty<GOAL>∃ r' ∈ Ioo 0 r, s ⊆ ball x r'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : ProperSpace α<VAR>x : α<VAR>r : ℝ<VAR>s : Set α<VAR>hr : 0 < r<VAR>hs : IsClosed s<VAR>h : s ⊆ ball x r<VAR>hne : s.Nonempty<VAR>this : IsCompact s<GOAL>∃ r' ∈ Ioo 0 r, s ⊆ ball x r'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : ProperSpace α<VAR>x : α<VAR>r : ℝ<VAR>s : Set α<VAR>hr : 0 < r<VAR>hs : IsClosed s<VAR>h : s ⊆ ball x r<VAR>hne : s.Nonempty<VAR>this : IsCompact s<VAR>y : α<VAR>hys : y ∈ s<VAR>hy : s ⊆ closedBall x (dist y x)<GOAL>∃ r' ∈ Ioo 0 r, s ⊆ ball x r'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : ProperSpace α<VAR>x : α<VAR>r : ℝ<VAR>s : Set α<VAR>hr : 0 < r<VAR>hs : IsClosed s<VAR>h : s ⊆ ball x r<VAR>hne : s.Nonempty<VAR>this : IsCompact s<VAR>y : α<VAR>hys : y ∈ s<VAR>hy : s ⊆ closedBall x (dist y x)<VAR>hyr : dist y x < r<GOAL>∃ r' ∈ Ioo 0 r, s ⊆ ball x r'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : ProperSpace α<VAR>x : α<VAR>r : ℝ<VAR>s : Set α<VAR>hr : 0 < r<VAR>hs : IsClosed s<VAR>h : s ⊆ ball x r<VAR>hne : s.Nonempty<VAR>this : IsCompact s<VAR>y : α<VAR>hys : y ∈ s<VAR>hy : s ⊆ closedBall x (dist y x)<VAR>hyr : dist y x < r<VAR>r' : ℝ<VAR>hyr' : dist y x < r'<VAR>hrr' : r' < r<GOAL>∃ r' ∈ Ioo 0 r, s ⊆ ball x r'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>μa : Measure α<VAR>μb : Measure β<VAR>μc : Measure γ<VAR>μd : Measure δ<VAR>f : α → β<VAR>hf : MeasurePreserving f μa μb<VAR>s : Set β<VAR>hs : NullMeasurableSet s μb<GOAL>μa (f ⁻¹' s) = μb s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>μa : Measure α<VAR>μb : Measure β<VAR>μc : Measure γ<VAR>μd : Measure δ<VAR>f : α → β<VAR>hf : MeasurePreserving f μa μb<VAR>s : Set β<VAR>hs : NullMeasurableSet s (map f μa)<GOAL>μa (f ⁻¹' s) = (map f μa) s
<VAR>m n✝ n : ℕ<VAR>a b : ZMod n<GOAL>(a * b).val ≤ a.val * b.val
<VAR>m n✝ n : ℕ<VAR>a b : ZMod n<GOAL>a.val * b.val % n ≤ a.val * b.val
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>(𝓝[s] x).NeBot ↔ ∀ ⦃t : Set X⦄, t ∈ 𝓝 x → (t ∩ s).Nonempty
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>(∀ ⦃s_1 : Set X⦄, s_1 ∈ 𝓝 x → ∀ ⦃s' : Set X⦄, s' ∈ 𝓟 s → (s_1 ∩ s').Nonempty) ↔ ∀ ⦃t : Set X⦄, t ∈ 𝓝 x → (t ∩ s).Nonempty
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F✝ G F' G' : C ⥤ D<VAR>α : F✝ ⟶ G<VAR>β✝ : F' ⟶ G'<VAR>F : C ⥤ D<VAR>β : F' ⟶ G'<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(tensorObj F F').map f ≫ (fun X => F.obj X ◁ β.app X) Y = (fun X => F.obj X ◁ β.app X) X ≫ (tensorObj F G').map f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F✝ G F' G' : C ⥤ D<VAR>α : F✝ ⟶ G<VAR>β✝ : F' ⟶ G'<VAR>F : C ⥤ D<VAR>β : F' ⟶ G'<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(tensorObj F F').map f ≫ (𝟙 (F.obj Y) ⊗ β.app Y) = (𝟙 (F.obj X) ⊗ β.app X) ≫ (tensorObj F G').map f
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>M : Matrix n n R<VAR>j : n<VAR>s : Finset n<VAR>hj : j ∉ s<VAR>c : n → R<VAR>a : R<GOAL>(M.updateRow j (a • M j + ∑ k ∈ s, c k • M k)).det = a • M.det
<VAR>m x✝ : ℕ<GOAL>Nat.shiftLeft' false m x✝ = m * 2 ^ x✝
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f✝ f : R[X]<VAR>r : R<VAR>N n✝ : ℕ<GOAL>(reflect N (C r * f)).coeff n✝ = (C r * reflect N f).coeff n✝
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<VAR>hp₁ : Fact (1 ≤ p)<VAR>β : Type u_5<VAR>l : Filter β<VAR>t : β → Set α<VAR>ht : ∀ (b : β), MeasurableSet (t b)<VAR>hμt : ∀ (b : β), μ (t b) ≠ ⊤<VAR>hp : p ≠ ⊤<VAR>h : Tendsto (fun b => μ (t b ∆ s)) l (𝓝 0)<GOAL>Tendsto (fun b => indicatorConstLp p ⋯ ⋯ c) l (𝓝 (indicatorConstLp p hs hμs c))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<VAR>hp₁ : Fact (1 ≤ p)<VAR>β : Type u_5<VAR>l : Filter β<VAR>t : β → Set α<VAR>ht : ∀ (b : β), MeasurableSet (t b)<VAR>hμt : ∀ (b : β), μ (t b) ≠ ⊤<VAR>hp : p ≠ ⊤<VAR>h : Tendsto (fun b => μ (t b ∆ s)) l (𝓝 0)<GOAL>Tendsto (fun b => dist (indicatorConstLp p ⋯ ⋯ c) (indicatorConstLp p hs hμs c)) l (𝓝 0)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<VAR>hp₁ : Fact (1 ≤ p)<VAR>β : Type u_5<VAR>l : Filter β<VAR>t : β → Set α<VAR>ht : ∀ (b : β), MeasurableSet (t b)<VAR>hμt : ∀ (b : β), μ (t b) ≠ ⊤<VAR>hp : p ≠ ⊤<VAR>h : Tendsto (fun b => μ (t b ∆ s)) l (𝓝 0)<VAR>hp₀ : p ≠ 0<GOAL>Tendsto (fun b => dist (indicatorConstLp p ⋯ ⋯ c) (indicatorConstLp p hs hμs c)) l (𝓝 0)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<VAR>hp₁ : Fact (1 ≤ p)<VAR>β : Type u_5<VAR>l : Filter β<VAR>t : β → Set α<VAR>ht : ∀ (b : β), MeasurableSet (t b)<VAR>hμt : ∀ (b : β), μ (t b) ≠ ⊤<VAR>hp : p ≠ ⊤<VAR>h : Tendsto (fun b => μ (t b ∆ s)) l (𝓝 0)<VAR>hp₀ : p ≠ 0<GOAL>Tendsto (fun b => ‖c‖ * (μ (t b ∆ s)).toReal ^ (1 / p.toReal)) l (𝓝 0)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<VAR>hp₁ : Fact (1 ≤ p)<VAR>β : Type u_5<VAR>l : Filter β<VAR>t : β → Set α<VAR>ht : ∀ (b : β), MeasurableSet (t b)<VAR>hμt : ∀ (b : β), μ (t b) ≠ ⊤<VAR>hp : p ≠ ⊤<VAR>h : Tendsto (fun b => μ (t b ∆ s)) l (𝓝 0)<VAR>hp₀ : p ≠ 0<GOAL>0 = ‖c‖ * ENNReal.toReal 0 ^ (1 / p.toReal)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<VAR>hp₁ : Fact (1 ≤ p)<VAR>β : Type u_5<VAR>l : Filter β<VAR>t : β → Set α<VAR>ht : ∀ (b : β), MeasurableSet (t b)<VAR>hμt : ∀ (b : β), μ (t b) ≠ ⊤<VAR>hp : p ≠ ⊤<VAR>h : Tendsto (fun b => μ (t b ∆ s)) l (𝓝 0)<VAR>hp₀ : p ≠ 0<GOAL>ENNReal.toReal 0 ≠ 0 ∨ 0 ≤ 1 / p.toReal
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>a : ℝ<GOAL>ContinuousAt (fun p => p.1 + p.2) (⊤, ↑a)
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>a : ℝ<GOAL>∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ↑a), ↑x < a.1 + a.2
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>a r : ℝ<VAR>x✝ : EReal × EReal<VAR>h : ↑(r - (a - 1)) < x✝.1 ∧ ↑(a - 1) < x✝.2<GOAL>↑r < x✝.1 + x✝.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MeasurableSpace α<VAR>K : Type u_5<VAR>q : ℚ<GOAL>ennrealRatEmbed (Encodable.encode q) = ↑(↑q).toNNReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MeasurableSpace α<VAR>K : Type u_5<VAR>q : ℚ<GOAL>ENNReal.ofReal ↑((some q).getD 0) = ↑(↑q).toNNReal
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>P : G.Partition<VAR>v : V<GOAL>P.partOfVertex v ∈ P.parts
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>P : G.Partition<VAR>v : V<VAR>h : Exists.choose ⋯ ∈ P.parts<GOAL>P.partOfVertex v ∈ P.parts
<VAR>C : Type u_1<VAR>C₁ : Type u_2<VAR>C₂ : Type u_3<VAR>C₃ : Type u_4<VAR>D₁ : Type u_5<VAR>D₂ : Type u_6<VAR>D₃ : Type u_7<VAR>inst✝⁹ : Category.{u_9, u_1} C<VAR>inst✝⁸ : Category.{?u.42595, u_2} C₁<VAR>inst✝⁷ : Category.{?u.42599, u_3} C₂<VAR>inst✝⁶ : Category.{?u.42603, u_4} C₃<VAR>inst✝⁵ : Category.{u_8, u_5} D₁<VAR>inst✝⁴ : Category.{?u.42611, u_6} D₂<VAR>inst✝³ : Category.{?u.42615, u_7} D₃<VAR>W : MorphismProperty C<VAR>L₁ : C ⥤ D₁<VAR>inst✝² : L₁.IsLocalization W<VAR>L₂ : C ⥤ D₂<VAR>inst✝¹ : L₂.IsLocalization W<VAR>L₃ : C ⥤ D₃<VAR>inst✝ : L₃.IsLocalization W<VAR>X Y Z : C<VAR>f : L₁.obj X ⟶ L₁.obj Y<GOAL>(homEquiv W L₁ L₁) f = f
<VAR>K✝ : Type u_1<VAR>inst✝² : Field K✝<VAR>K : Type u_2<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>ζ : K<VAR>n : ℕ<VAR>h : IsPrimitiveRoot ζ n<GOAL>∃ P, map (Int.castRingHom K) P = cyclotomic' n K ∧ P.degree = (cyclotomic' n K).degree ∧ P.Monic
<VAR>K✝ : Type u_1<VAR>inst✝² : Field K✝<VAR>K : Type u_2<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>ζ : K<VAR>n : ℕ<VAR>h : IsPrimitiveRoot ζ n<GOAL>cyclotomic' n K ∈ lifts (Int.castRingHom K)
<VAR>K✝ : Type u_1<VAR>inst✝² : Field K✝<VAR>K : Type u_2<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>k : ℕ<VAR>ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)<VAR>ζ : K<VAR>h : IsPrimitiveRoot ζ k<GOAL>cyclotomic' k K ∈ lifts (Int.castRingHom K)
<VAR>K✝ : Type u_1<VAR>inst✝² : Field K✝<VAR>K : Type u_2<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>ζ : K<VAR>ihk : ∀ m < 0, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)<VAR>h : IsPrimitiveRoot ζ 0<GOAL>cyclotomic' 0 K ∈ lifts (Int.castRingHom K)
<VAR>K✝ : Type u_1<VAR>inst✝² : Field K✝<VAR>K : Type u_2<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>k : ℕ<VAR>ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)<VAR>ζ : K<VAR>h : IsPrimitiveRoot ζ k<VAR>hpos : k > 0<GOAL>cyclotomic' k K ∈ lifts (Int.castRingHom K)
<VAR>K✝ : Type u_1<VAR>inst✝² : Field K✝<VAR>K : Type u_2<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>k : ℕ<VAR>ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)<VAR>ζ : K<VAR>h : IsPrimitiveRoot ζ k<VAR>hpos : k > 0<VAR>B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K<GOAL>cyclotomic' k K ∈ lifts (Int.castRingHom K)
<VAR>K✝ : Type u_1<VAR>inst✝² : Field K✝<VAR>K : Type u_2<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>k : ℕ<VAR>ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)<VAR>ζ : K<VAR>h : IsPrimitiveRoot ζ k<VAR>hpos : k > 0<VAR>B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K<VAR>Bmo : B.Monic<GOAL>cyclotomic' k K ∈ lifts (Int.castRingHom K)
<VAR>K✝ : Type u_1<VAR>inst✝² : Field K✝<VAR>K : Type u_2<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>k : ℕ<VAR>ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)<VAR>ζ : K<VAR>h : IsPrimitiveRoot ζ k<VAR>hpos : k > 0<VAR>B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K<VAR>Bmo : B.Monic<VAR>Bint : B ∈ lifts (Int.castRingHom K)<GOAL>cyclotomic' k K ∈ lifts (Int.castRingHom K)
<VAR>K✝ : Type u_1<VAR>inst✝² : Field K✝<VAR>K : Type u_2<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>k : ℕ<VAR>ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)<VAR>ζ : K<VAR>h : IsPrimitiveRoot ζ k<VAR>hpos : k > 0<VAR>B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K<VAR>Bmo : B.Monic<VAR>Bint : ∃ q, map (Int.castRingHom K) q = B ∧ q.degree = B.degree ∧ q.Monic<GOAL>cyclotomic' k K ∈ lifts (Int.castRingHom K)
<VAR>K✝ : Type u_1<VAR>inst✝² : Field K✝<VAR>K : Type u_2<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>k : ℕ<VAR>ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)<VAR>ζ : K<VAR>h : IsPrimitiveRoot ζ k<VAR>hpos : k > 0<VAR>B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K<VAR>Bmo : B.Monic<VAR>B₁ : ℤ[X]<VAR>hB₁ : map (Int.castRingHom K) B₁ = B<VAR>left✝ : B₁.degree = B.degree<VAR>hB₁mo : B₁.Monic<VAR>Q₁ : ℤ[X] := (X ^ k - 1) /ₘ B₁<VAR>huniq : 0 + B * cyclotomic' k K = X ^ k - 1 ∧ degree 0 < B.degree<GOAL>cyclotomic' k K ∈ lifts (Int.castRingHom K)
<VAR>K✝ : Type u_1<VAR>inst✝² : Field K✝<VAR>K : Type u_2<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>k : ℕ<VAR>ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)<VAR>ζ : K<VAR>h : IsPrimitiveRoot ζ k<VAR>hpos : k > 0<VAR>B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K<VAR>Bmo : B.Monic<VAR>B₁ : ℤ[X]<VAR>hB₁ : map (Int.castRingHom K) B₁ = B<VAR>left✝ : B₁.degree = B.degree<VAR>hB₁mo : B₁.Monic<VAR>Q₁ : ℤ[X] := (X ^ k - 1) /ₘ B₁<VAR>huniq : (X ^ k - 1) /ₘ B = cyclotomic' k K ∧ (X ^ k - 1) %ₘ B = 0<GOAL>cyclotomic' k K ∈ lifts (Int.castRingHom K)
<VAR>K✝ : Type u_1<VAR>inst✝² : Field K✝<VAR>K : Type u_2<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>k : ℕ<VAR>ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)<VAR>ζ : K<VAR>h : IsPrimitiveRoot ζ k<VAR>hpos : k > 0<VAR>B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K<VAR>Bmo : B.Monic<VAR>B₁ : ℤ[X]<VAR>hB₁ : map (Int.castRingHom K) B₁ = B<VAR>left✝ : B₁.degree = B.degree<VAR>hB₁mo : B₁.Monic<VAR>Q₁ : ℤ[X] := (X ^ k - 1) /ₘ B₁<VAR>huniq : (X ^ k - 1) /ₘ B = cyclotomic' k K ∧ (X ^ k - 1) %ₘ B = 0<GOAL>∃ x, (mapRingHom (Int.castRingHom K)) x = cyclotomic' k K
<VAR>K✝ : Type u_1<VAR>inst✝² : Field K✝<VAR>K : Type u_2<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>k : ℕ<VAR>ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)<VAR>ζ : K<VAR>h : IsPrimitiveRoot ζ k<VAR>hpos : k > 0<VAR>B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K<VAR>Bmo : B.Monic<VAR>B₁ : ℤ[X]<VAR>hB₁ : map (Int.castRingHom K) B₁ = B<VAR>left✝ : B₁.degree = B.degree<VAR>hB₁mo : B₁.Monic<VAR>Q₁ : ℤ[X] := (X ^ k - 1) /ₘ B₁<VAR>huniq : (X ^ k - 1) /ₘ B = cyclotomic' k K ∧ (X ^ k - 1) %ₘ B = 0<GOAL>(mapRingHom (Int.castRingHom K)) Q₁ = cyclotomic' k K
<VAR>K✝ : Type u_1<VAR>inst✝² : Field K✝<VAR>K : Type u_2<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>k : ℕ<VAR>ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)<VAR>ζ : K<VAR>h : IsPrimitiveRoot ζ k<VAR>hpos : k > 0<VAR>B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K<VAR>Bmo : B.Monic<VAR>B₁ : ℤ[X]<VAR>hB₁ : map (Int.castRingHom K) B₁ = B<VAR>left✝ : B₁.degree = B.degree<VAR>hB₁mo : B₁.Monic<VAR>Q₁ : ℤ[X] := (X ^ k - 1) /ₘ B₁<VAR>huniq : (X ^ k - 1) /ₘ B = cyclotomic' k K ∧ (X ^ k - 1) %ₘ B = 0<GOAL>map (Int.castRingHom K) (X ^ k - 1) /ₘ B = (X ^ k - 1) /ₘ B
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h₁ : c < b<VAR>x : α<GOAL>x ∈ Iic b ∪ Ioc c d ↔ x ∈ Iic (max b d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h₁ : c < b<VAR>x : α<GOAL>x ≤ b ∨ c < x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<GOAL>(2 * X ^ 6 + C W.b₂ * X ^ 5 + 5 * C W.b₄ * X ^ 4 + 10 * C W.b₆ * X ^ 3 + 10 * C W.b₈ * X ^ 2 + C (W.b₂ * W.b₈ - W.b₄ * W.b₆) * X + C (W.b₄ * W.b₈ - W.b₆ ^ 2)).coeff 6 = 2
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>k✝ r k : ℕ<GOAL>∂ ^[k] ∅ = ∅
<VAR>p a b n : ℕ<VAR>ha : Nat.Prime a<VAR>hb : b ≠ 0<GOAL>n ≤ padicValNat a b ↔ replicate n a <+~ b.primeFactorsList
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>r r' : ι → ι → Prop<VAR>inst✝¹ : IsWellOrder ι r<VAR>inst✝ : IsWellOrder ι r'<VAR>f : ι → Ordinal.{max u v}<GOAL>(type r).blsub (bfamilyOfFamily' r f) = (type r').blsub (bfamilyOfFamily' r' f)
<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>s : Set E<VAR>f g : E → F<VAR>hf : ContDiffOn 𝕜 n f s<VAR>hg : ContDiffOn 𝕜 n g s<GOAL>ContDiffOn 𝕜 n (fun x => f x - g x) s
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k : Set α<VAR>inst✝ : OpensMeasurableSpace α<VAR>hs : MeasurableSet s<GOAL>MeasurableSet (μ.everywherePosSubset s)
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k : Set α<VAR>inst✝ : OpensMeasurableSpace α<VAR>hs : MeasurableSet s<VAR>u : Set α<VAR>u_open : IsOpen u<VAR>hu : μ.everywherePosSubset s = s \ u<GOAL>MeasurableSet (μ.everywherePosSubset s)
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k : Set α<VAR>inst✝ : OpensMeasurableSpace α<VAR>hs : MeasurableSet s<VAR>u : Set α<VAR>u_open : IsOpen u<VAR>hu : μ.everywherePosSubset s = s \ u<GOAL>MeasurableSet (s \ u)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PredOrder α<VAR>a✝ b✝ a b : α<GOAL>pred a ≤ b ∧ b ≤ a ↔ b = a ∨ b = pred a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PredOrder α<VAR>a✝ b✝ a b : α<GOAL>b = a ∨ b = pred a → pred a ≤ b ∧ b ≤ a
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : Ring S<VAR>M : Type u_4<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>m : Submodule R M<VAR>N✝ : Type u_5<VAR>inst✝² : AddCommGroup N✝<VAR>inst✝¹ : Module R N✝<VAR>inst✝ : IsSemisimpleModule R M<VAR>N : Submodule R M<GOAL>N = ⊥ ∨ ∃ m ≤ N, IsSimpleModule R ↥m
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>e : C ≌ D<VAR>X Y : C<VAR>f f' : X ⟶ e.inverse.obj (e.functor.obj Y)<GOAL>f ≫ e.unitInv.app Y = f' ≫ e.unitInv.app Y ↔ f = f'
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 ≤ x<VAR>h : y + 1 ≠ 0<GOAL>x ^ (y + 1) = x ^ y * x
<VAR>α : Type u_1<VAR>inst✝² : CanonicallyLinearOrderedAddCommMonoid α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<GOAL>a - b + b = max a b
<VAR>α : Type u_1<VAR>inst✝² : CanonicallyLinearOrderedAddCommMonoid α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>h : a ≤ b<GOAL>a - b + b = max a b
<VAR>α : Type u_1<VAR>inst✝² : CanonicallyLinearOrderedAddCommMonoid α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>h : b ≤ a<GOAL>a - b + b = max a b
<VAR>α β : Type u<VAR>m n : ℕ<GOAL>↑m < ↑n ↔ m < n
<VAR>α β : Type u<VAR>m n : ℕ<GOAL>↑m ≤ ↑n ∧ ¬↑n ≤ ↑m ↔ ¬n ≤ m
<VAR>α β : Type u<VAR>m n : ℕ<GOAL>m < n → m ≤ n
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>a a' : α<VAR>b : β a<VAR>b' : β a'<VAR>s : AList β<VAR>h : a ≠ a'<GOAL>(insert a' b' (insert a b s)).entries ~ (insert a b (insert a' b' s)).entries
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>a a' : α<VAR>b : β a<VAR>b' : β a'<VAR>s : AList β<VAR>h : a ≠ a'<GOAL>⟨a', b'⟩ :: kerase a' (⟨a, b⟩ :: kerase a s.entries) ~ ⟨a, b⟩ :: kerase a (⟨a', b'⟩ :: kerase a' s.entries)
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : AddCommMonoid μ<VAR>inst✝¹ : HasAntidiagonal μ<VAR>inst✝ : DecidableEq μ<VAR>n✝ : μ<VAR>s : Finset ι<VAR>n : μ<VAR>f : ι → μ<VAR>hn : n ≠ 0<GOAL>∀ (x : ι → μ), x ∉ ∅.piAntidiag n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s : Finset ι<VAR>H : s.Nonempty<VAR>f : ι → α<VAR>a : α<GOAL>a < s.sup' H f ↔ ∃ b ∈ s, a < f b
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s : Finset ι<VAR>H : s.Nonempty<VAR>f : ι → α<VAR>a : α<GOAL>(∃ b ∈ s, ↑a < (WithBot.some ∘ f) b) ↔ ∃ b ∈ s, a < f b
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t✝ : Set α<VAR>hs : MeasurableSet s<VAR>H : μ.restrict s = ν.restrict s<VAR>t : Set α<VAR>hts : t ⊆ s<VAR>ht : MeasurableSet t<GOAL>μ t = ν t
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t✝ : Set α<VAR>hs : MeasurableSet s<VAR>H : ∀ t ⊆ s, MeasurableSet t → μ t = ν t<VAR>t : Set α<VAR>ht : MeasurableSet t<GOAL>(μ.restrict s) t = (ν.restrict s) t
<VAR>α✝ : Sort u_1<VAR>β : Sort u_2<VAR>p✝ q✝ : α✝ → Prop<VAR>α : Sort u_3<VAR>p : α → Sort u_4<VAR>inst✝ : ∀ (x : α), Subsingleton (p x)<VAR>q : (x : α) → p x → Prop<VAR>h : ∃! x, ∃! hx, q x hx<VAR>y₁ y₂ : α<VAR>hpy₁ : p y₁<VAR>hqy₁ : q y₁ hpy₁<VAR>hpy₂ : p y₂<VAR>hqy₂ : q y₂ hpy₂<GOAL>y₁ = y₂
<VAR>α✝ : Sort u_1<VAR>β : Sort u_2<VAR>p✝ q✝ : α✝ → Prop<VAR>α : Sort u_3<VAR>p : α → Sort u_4<VAR>inst✝ : ∀ (x : α), Subsingleton (p x)<VAR>q : (x : α) → p x → Prop<VAR>y₁ y₂ : α<VAR>hpy₁ : p y₁<VAR>hqy₁ : q y₁ hpy₁<VAR>hpy₂ : p y₂<VAR>hqy₂ : q y₂ hpy₂<VAR>h : ∃! x, ∃ hx, q x hx<GOAL>y₁ = y₂
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f f₁ f₂ : (i : ι) → Filter (α i)<VAR>s : (i : ι) → Set (α i)<VAR>p : (i : ι) → α i → Prop<GOAL>(pi f).NeBot ↔ ∀ (i : ι), (f i).NeBot
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f g : End R M<VAR>p : Submodule R M<VAR>hp : MapsTo ⇑f ↑p ↑p<VAR>hf : f.IsSemisimple<GOAL>IsSemisimple (LinearMap.restrict f hp)