ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>ζ : R<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>n : ℕ+<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>p : ℕ := ringChar R<GOAL>NeZero ↑↑n
<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>ζ : R<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>n : ℕ+<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>p : ℕ := ringChar R<VAR>hfin : multiplicity.Finite p ↑n<GOAL>NeZero ↑↑n
<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>ζ : R<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>n : ℕ+<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>p : ℕ := ringChar R<VAR>hfin : multiplicity.Finite p ↑n<VAR>m : ℕ<VAR>hm : ↑n = p ^ (multiplicity p ↑n).get hfin * m ∧ ¬p ∣ m<GOAL>NeZero ↑↑n
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : ConcreteCategory C<VAR>J : Type w<VAR>inst✝¹ : Category.{t, w} J<VAR>F : J ⥤ C<VAR>inst✝ : PreservesLimit F (forget C)<VAR>D : Cone F<VAR>hD : IsLimit D<VAR>E : Cone (F ⋙ forget C) := (forget C).mapCone D<VAR>hE : IsLimit E := isLimitOfPreserves (forget C) hD<VAR>G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)<VAR>hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)<VAR>T : E.pt ≅ G.pt := hE.conePointUniqueUpToIso hG<VAR>h : Function.Injective T.hom<GOAL>Function.Injective (T.hom ≫ fun x j => G.π.app j x)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : ConcreteCategory C<VAR>J : Type w<VAR>inst✝¹ : Category.{t, w} J<VAR>F : J ⥤ C<VAR>inst✝ : PreservesLimit F (forget C)<VAR>D : Cone F<VAR>hD : IsLimit D<VAR>E : Cone (F ⋙ forget C) := (forget C).mapCone D<VAR>hE : IsLimit E := isLimitOfPreserves (forget C) hD<VAR>G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)<VAR>hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)<VAR>T : E.pt ≅ G.pt := hE.conePointUniqueUpToIso hG<VAR>h : Function.Injective T.hom<GOAL>Function.Injective fun x j => G.π.app j x
<VAR>ι✝ : Type u_1<VAR>κ✝ : Type u_2<VAR>α✝ : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α✝<VAR>a : α✝<VAR>f✝ g : α✝ → β<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>inst✝³ : Fintype ι<VAR>inst✝² : Fintype κ<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>f : ι → α<GOAL>(∏ j : ι, if j = i then f j else 1) = f i
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : Monoid M<VAR>a : M<VAR>s : Set M<GOAL>closure s = mrange (FreeMonoid.lift Subtype.val)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t : Set α<VAR>f g : α → E<VAR>h : s =ᶠ[ae μ] t<GOAL>⨍ (x : α) in s, f x ∂μ = ⨍ (x : α) in t, f x ∂μ
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>b b' : β a<GOAL>insert a b (singleton a b') = singleton a b
<VAR>R✝ : Type u_1<VAR>inst✝¹⁴ : CommRing R✝<VAR>I✝ : Ideal R✝<VAR>M✝¹ : Type u_2<VAR>inst✝¹³ : AddCommGroup M✝¹<VAR>inst✝¹² : Module R✝ M✝¹<VAR>N✝ : Type u_3<VAR>inst✝¹¹ : AddCommGroup N✝<VAR>inst✝¹⁰ : Module R✝ N✝<VAR>R : Type u<VAR>inst✝⁹ : CommRing R<VAR>I : Ideal R<VAR>M✝ : Type u<VAR>inst✝⁸ : AddCommGroup M✝<VAR>inst✝⁷ : Module R M✝<VAR>inst✝⁶ : IsNoetherianRing R<VAR>M : Type u<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>N : Type u<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>f : M →ₗ[R] N<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : Module.Finite R N<VAR>hf : Function.Injective ⇑f<GOAL>Function.Injective ⇑(AlgebraTensorModule.map LinearMap.id f)
<VAR>R✝ : Type u_1<VAR>inst✝¹⁴ : CommRing R✝<VAR>I✝ : Ideal R✝<VAR>M✝¹ : Type u_2<VAR>inst✝¹³ : AddCommGroup M✝¹<VAR>inst✝¹² : Module R✝ M✝¹<VAR>N✝ : Type u_3<VAR>inst✝¹¹ : AddCommGroup N✝<VAR>inst✝¹⁰ : Module R✝ N✝<VAR>R : Type u<VAR>inst✝⁹ : CommRing R<VAR>I : Ideal R<VAR>M✝ : Type u<VAR>inst✝⁸ : AddCommGroup M✝<VAR>inst✝⁷ : Module R M✝<VAR>inst✝⁶ : IsNoetherianRing R<VAR>M : Type u<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>N : Type u<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>f : M →ₗ[R] N<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : Module.Finite R N<VAR>hf : Function.Injective ⇑f<GOAL>Function.Injective ⇑(↑(ofTensorProductEquivOfFiniteNoetherian I N).symm ∘ₗ map I f ∘ₗ ↑(ofTensorProductEquivOfFiniteNoetherian I M))
<VAR>R✝ : Type u_1<VAR>inst✝¹⁴ : CommRing R✝<VAR>I✝ : Ideal R✝<VAR>M✝¹ : Type u_2<VAR>inst✝¹³ : AddCommGroup M✝¹<VAR>inst✝¹² : Module R✝ M✝¹<VAR>N✝ : Type u_3<VAR>inst✝¹¹ : AddCommGroup N✝<VAR>inst✝¹⁰ : Module R✝ N✝<VAR>R : Type u<VAR>inst✝⁹ : CommRing R<VAR>I : Ideal R<VAR>M✝ : Type u<VAR>inst✝⁸ : AddCommGroup M✝<VAR>inst✝⁷ : Module R M✝<VAR>inst✝⁶ : IsNoetherianRing R<VAR>M : Type u<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>N : Type u<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>f : M →ₗ[R] N<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : Module.Finite R N<VAR>hf : Function.Injective ⇑f<GOAL>Function.Injective ⇑(map I f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ζ : Type u_6<VAR>r : α → α → Prop<VAR>a b c d : α<GOAL>ReflTransGen (ReflGen r) = ReflTransGen r
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>hf : UniformContinuous fun x => f ↑x<VAR>ha : s ∈ 𝓝 a<GOAL>Tendsto f (𝓝 a) (𝓝 (f a))
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>hf : UniformContinuous fun x => f ↑x<VAR>ha : s ∈ 𝓝 a<GOAL>Tendsto f (map Subtype.val (𝓝 ⟨a, ⋯⟩)) (𝓝 (f a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι✝ : Type u_5<VAR>π : ι✝ → Type u_6<VAR>inst✝³ : (i : ι✝) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>ι : Sort u_7<VAR>f : α → β<VAR>s : ι → Set α<VAR>hs : ∀ (x : α), ∃ i, s i ∈ 𝓝 x<VAR>hf : ∀ (i : ι), ContinuousOn f (s i)<VAR>x : α<VAR>i : ι<VAR>hi : s i ∈ 𝓝 x<GOAL>ContinuousAt f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι✝ : Type u_5<VAR>π : ι✝ → Type u_6<VAR>inst✝³ : (i : ι✝) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>ι : Sort u_7<VAR>f : α → β<VAR>s : ι → Set α<VAR>hs : ∀ (x : α), ∃ i, s i ∈ 𝓝 x<VAR>hf : ∀ (i : ι), ContinuousOn f (s i)<VAR>x : α<VAR>i : ι<VAR>hi : s i ∈ 𝓝 x<GOAL>Tendsto f (𝓝[s i] x) (𝓝 (f x))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>r : R<VAR>x : PrimeSpectrum R<GOAL>x ∈ ↑(basicOpen r) ↔ x ∈ (zeroLocus {r})ᶜ
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>b c : α<GOAL>lcm (0 * b) (0 * c) = normalize 0 * lcm b c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Monoid α<VAR>n : ℕ<VAR>G : Type u_3<VAR>inst✝ : Group G<VAR>g : Fin (n + 1) → G<VAR>j : Fin (n + 1)<VAR>k : Fin n<GOAL>(partialProd g (j.succ.succAbove k.castSucc))⁻¹ * partialProd g (j.succAbove k).succ = j.contractNth (fun x x_1 => x * x_1) g k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Monoid α<VAR>n : ℕ<VAR>G : Type u_3<VAR>inst✝ : Group G<VAR>g : Fin (n + 1) → G<VAR>j : Fin (n + 1)<VAR>k : Fin n<VAR>h : ↑k < ↑j<GOAL>(partialProd g (j.succ.succAbove k.castSucc))⁻¹ * partialProd g (j.succAbove k).succ = j.contractNth (fun x x_1 => x * x_1) g k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Monoid α<VAR>n : ℕ<VAR>G : Type u_3<VAR>inst✝ : Group G<VAR>g : Fin (n + 1) → G<VAR>j : Fin (n + 1)<VAR>k : Fin n<VAR>h : ↑k = ↑j<GOAL>(partialProd g (j.succ.succAbove k.castSucc))⁻¹ * partialProd g (j.succAbove k).succ = j.contractNth (fun x x_1 => x * x_1) g k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Monoid α<VAR>n : ℕ<VAR>G : Type u_3<VAR>inst✝ : Group G<VAR>g : Fin (n + 1) → G<VAR>j : Fin (n + 1)<VAR>k : Fin n<VAR>h : ↑j < ↑k<GOAL>(partialProd g (j.succ.succAbove k.castSucc))⁻¹ * partialProd g (j.succAbove k).succ = j.contractNth (fun x x_1 => x * x_1) g k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : CancelCommMonoidWithZero β<VAR>e : α ≃* β<VAR>hα : UniqueFactorizationMonoid α<GOAL>UniqueFactorizationMonoid β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : CancelCommMonoidWithZero β<VAR>e : α ≃* β<VAR>hα : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a<GOAL>∀ (a : β), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : CancelCommMonoidWithZero β<VAR>e : α ≃* β<VAR>hα : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a<VAR>a : β<VAR>ha : a ≠ 0<GOAL>∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : CancelCommMonoidWithZero β<VAR>e : α ≃* β<VAR>hα : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a<VAR>a : β<VAR>ha : a ≠ 0<VAR>w : Multiset α<VAR>hp : ∀ b ∈ w, Prime b<VAR>u : αˣ<VAR>h : w.prod * ↑u = e.symm a<GOAL>∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : Nontrivial E<VAR>x : E<VAR>K : Set E<VAR>hK : IsCompact K<VAR>hx : x ∈ K<GOAL>∃ y ∈ frontier K, infDist x Kᶜ = dist x y
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : Nontrivial E<VAR>x : E<VAR>K : Set E<VAR>hK : IsCompact K<VAR>hx : x ∈ K<VAR>hx' : x ∈ interior K<GOAL>∃ y ∈ frontier K, infDist x Kᶜ = dist x y
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : Nontrivial E<VAR>x : E<VAR>K : Set E<VAR>hK : IsCompact K<VAR>hx : x ∈ K<VAR>hx' : x ∈ frontier K<GOAL>∃ y ∈ frontier K, infDist x Kᶜ = dist x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>A✝ : Matrix n n α<VAR>inst✝¹ : Star α<VAR>inst✝ : Star β<VAR>A : Matrix n n α<VAR>h : A.IsHermitian<GOAL>Aᵀ.IsHermitian
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>A✝ : Matrix n n α<VAR>inst✝¹ : Star α<VAR>inst✝ : Star β<VAR>A : Matrix n n α<VAR>h : A.IsHermitian<GOAL>(Aᵀ.map star)ᵀ = Aᵀ
<VAR>m₁ : List Char<VAR>c : Char<VAR>m₂ : List Char<VAR>x✝ : Substring<VAR>h : x✝.Valid<VAR>e : x✝.toString.data = m₁ ++ c :: m₂<GOAL>x✝.next { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len m₁ + c.utf8Size }
<VAR>m₁ : List Char<VAR>c : Char<VAR>m₂ : List Char<VAR>x✝ : Substring<VAR>h✝ : x✝.Valid<VAR>e : x✝.toString.data = m₁ ++ c :: m₂<VAR>l m r : List Char<VAR>h : ValidFor l m r x✝<GOAL>x✝.next { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len m₁ + c.utf8Size }
<VAR>m₁ : List Char<VAR>c : Char<VAR>m₂ : List Char<VAR>x✝ : Substring<VAR>h✝ : x✝.Valid<VAR>l m r : List Char<VAR>h : ValidFor l m r x✝<VAR>e : m = m₁ ++ c :: m₂<GOAL>x✝.next { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len m₁ + c.utf8Size }
<VAR>m₁ : List Char<VAR>c : Char<VAR>m₂ : List Char<VAR>x✝ : Substring<VAR>h✝ : x✝.Valid<VAR>l r : List Char<VAR>h : ValidFor l (m₁ ++ c :: m₂) r x✝<GOAL>x✝.next { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len m₁ + c.utf8Size }
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<GOAL>Filter.map rexp atBot = 𝓝[>] 0
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>h : IsPullback fst snd f g<VAR>P' X' Y' Z' : C<VAR>fst' : P' ⟶ X'<VAR>snd' : P' ⟶ Y'<VAR>f' : X' ⟶ Z'<VAR>g' : Y' ⟶ Z'<VAR>e₁ : P ≅ P'<VAR>e₂ : X ≅ X'<VAR>e₃ : Y ≅ Y'<VAR>e₄ : Z ≅ Z'<VAR>commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'<VAR>commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'<VAR>commf : f ≫ e₄.hom = e₂.hom ≫ f'<VAR>commg : g ≫ e₄.hom = e₃.hom ≫ g'<GOAL>fst' ≫ f' = snd' ≫ g'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o o' : Ordinal.{max u v}<VAR>f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}<VAR>hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj<VAR>g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}<VAR>hg : o'.blsub g = o<VAR>a : Ordinal.{max u v}<VAR>ha : a < o'<GOAL>g a ha < o'.blsub g
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>l : Filter α<VAR>m : Filter β<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : m.NeBot<VAR>s : Set α<VAR>t : Set β<GOAL>(∀ᶠ (x : α × β) in l.curry m, x ∈ s ×ˢ t) ↔ s ∈ l ∧ t ∈ m
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>l : Filter α<VAR>m : Filter β<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : m.NeBot<VAR>s : Set α<VAR>t : Set β<VAR>h : ∀ᶠ (x : α) in l, ∀ᶠ (y : β) in m, (x, y) ∈ s ×ˢ t<GOAL>s ∈ l
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>l : Filter α<VAR>m : Filter β<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : m.NeBot<VAR>s : Set α<VAR>t : Set β<VAR>h : ∀ᶠ (x : α) in l, ∀ᶠ (y : β) in m, (x, y) ∈ s ×ˢ t<GOAL>t ∈ m
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>l : Filter α<VAR>m : Filter β<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : m.NeBot<VAR>s : Set α<VAR>t : Set β<VAR>h : ∀ᶠ (x : α) in l, ∀ᶠ (y : β) in m, (x, y) ∈ s ×ˢ t<VAR>w✝ : α<VAR>hx : ∀ᶠ (y : β) in m, (w✝, y) ∈ s ×ˢ t<GOAL>t ∈ m
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>l : Filter α<VAR>m : Filter β<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : m.NeBot<VAR>s : Set α<VAR>t : Set β<VAR>h : ∀ᶠ (x : α) in l, ∀ᶠ (y : β) in m, (x, y) ∈ s ×ˢ t<VAR>w✝ : α<VAR>hx : ∀ᶠ (y : β) in m, (w✝, y) ∈ s ×ˢ t<GOAL>{x | (fun y => (w✝, y) ∈ s ×ˢ t) x} ⊆ t
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>s : Set A<GOAL>IsClosed (zeroLocus 𝒜 s)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>s : Set A<GOAL>∃ s_1, zeroLocus 𝒜 s = zeroLocus 𝒜 s_1
<VAR>C : Type u_1<VAR>inst✝⁷ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{?u.38390, u_2} D<VAR>E : Type u_3<VAR>inst✝⁵ : Category.{?u.38397, u_3} E<VAR>M : Type u_4<VAR>inst✝⁴ : AddMonoid M<VAR>inst✝³ : HasShift C M<VAR>inst✝² : HasShift D M<VAR>inst✝¹ : HasShift E M<VAR>X Y Z T : C<VAR>inst✝ : Preadditive C<VAR>a b c : M<VAR>α₁ α₂ : ShiftedHom X Y a<VAR>β : ShiftedHom Y Z b<VAR>h : b + a = c<GOAL>(α₁ + α₂).comp β h = α₁.comp β h + α₂.comp β h
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝² : LinearOrderedSemifield α<VAR>inst✝¹ : Archimedean α<VAR>inst✝ : ExistsAddOfLE α<VAR>x y ε : α<VAR>xpos : 0 < x<VAR>hx : x ≤ 1<VAR>ypos : 0 < y<VAR>hy : y < 1<GOAL>∃ n, y ^ (n + 1) < x ∧ x ≤ y ^ n
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝² : LinearOrderedSemifield α<VAR>inst✝¹ : Archimedean α<VAR>inst✝ : ExistsAddOfLE α<VAR>x y ε : α<VAR>xpos : 0 < x<VAR>hx : x ≤ 1<VAR>ypos : 0 < y<VAR>hy : y < 1<VAR>n : ℕ<VAR>hn : y⁻¹ ^ n ≤ x⁻¹<VAR>h'n : x⁻¹ < y⁻¹ ^ (n + 1)<GOAL>∃ n, y ^ (n + 1) < x ∧ x ≤ y ^ n
<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>ζ ^ k.pred = -∑ i ∈ range k.pred, ζ ^ i
<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>inst✝² : Finite G<VAR>N : Subgroup G<VAR>inst✝¹ : N.Normal<VAR>h1 : (Nat.card ↥N).Coprime N.index<VAR>h2 : ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'], Nat.card G' < Nat.card G → ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'<VAR>h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H<VAR>K : Subgroup ↥N<VAR>inst✝ : (map N.subtype K).Normal<GOAL>K = ⊥ ∨ K = ⊤
<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>inst✝² : Finite G<VAR>N : Subgroup G<VAR>inst✝¹ : N.Normal<VAR>h1 : (Nat.card ↥N).Coprime N.index<VAR>h2 : ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'], Nat.card G' < Nat.card G → ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'<VAR>h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H<VAR>K : Subgroup ↥N<VAR>inst✝ : (map N.subtype K).Normal<VAR>key : map N.subtype K = ⊥ ∨ map N.subtype K = N<GOAL>K = ⊥ ∨ K = ⊤
<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>inst✝² : Finite G<VAR>N : Subgroup G<VAR>inst✝¹ : N.Normal<VAR>h1 : (Nat.card ↥N).Coprime N.index<VAR>h2 : ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'], Nat.card G' < Nat.card G → ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'<VAR>h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H<VAR>K : Subgroup ↥N<VAR>inst✝ : (map N.subtype K).Normal<VAR>key : map N.subtype K = map N.subtype ⊥ ∨ map N.subtype K = N<GOAL>K = ⊥ ∨ K = ⊤
<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>inst✝² : Finite G<VAR>N : Subgroup G<VAR>inst✝¹ : N.Normal<VAR>h1 : (Nat.card ↥N).Coprime N.index<VAR>h2 : ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'], Nat.card G' < Nat.card G → ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'<VAR>h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H<VAR>K : Subgroup ↥N<VAR>inst✝ : (map N.subtype K).Normal<VAR>key : map N.subtype K = map N.subtype ⊥ ∨ map N.subtype K = map N.subtype ⊤<GOAL>K = ⊥ ∨ K = ⊤
<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>inst✝² : Finite G<VAR>N : Subgroup G<VAR>inst✝¹ : N.Normal<VAR>h1 : (Nat.card ↥N).Coprime N.index<VAR>h2 : ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'], Nat.card G' < Nat.card G → ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'<VAR>h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H<VAR>K : Subgroup ↥N<VAR>inst✝ : (map N.subtype K).Normal<VAR>key : map N.subtype K = map N.subtype ⊥ ∨ map N.subtype K = map N.subtype ⊤<VAR>inj : Function.Injective (map N.subtype)<GOAL>K = ⊥ ∨ K = ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : CommRing α<VAR>a b : α<VAR>u₁ u₂ : αˣ<GOAL>a /ₚ u₁ - b /ₚ u₂ = (a * ↑u₂ - ↑u₁ * b) /ₚ (u₁ * u₂)
<VAR>m n a b c d : ℕ<VAR>h : a ≡ b [MOD m]<VAR>hdm : d ∣ m<GOAL>d ∣ a ↔ d ∣ b
<VAR>m n a b c d : ℕ<VAR>h : a ≡ b [MOD m]<VAR>hdm : d ∣ m<GOAL>a ≡ 0 [MOD d] ↔ b ≡ 0 [MOD d]
<VAR>m n a b c d : ℕ<VAR>hdm : d ∣ m<VAR>h : a ≡ b [MOD d]<GOAL>a ≡ 0 [MOD d] ↔ b ≡ 0 [MOD d]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν✝ : Measure α<VAR>mb : MeasurableSpace β<VAR>ν : Measure β<VAR>g : α → β<VAR>hg : MeasurePreserving g μ ν<VAR>hge : MeasurableEmbedding g<VAR>f : β → ℝ≥0∞<VAR>s : Set β<GOAL>∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (b : β) in s, f b ∂ν
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : Semifield R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : TopologicalSemiring R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : HasContinuousInv₀ R<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a✝ : A<VAR>a : Aˣ<VAR>ha : autoParam (p ↑a) _auto✝<GOAL>cfc (fun x => x⁻¹) ↑a = ↑a⁻¹
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : Semifield R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : TopologicalSemiring R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : HasContinuousInv₀ R<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a✝ : A<VAR>a : Aˣ<VAR>ha : autoParam (p ↑a) _auto✝<GOAL>cfc (fun x => x⁻¹) ↑a = Ring.inverse ↑a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : Semifield R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : TopologicalSemiring R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : HasContinuousInv₀ R<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a✝ : A<VAR>a : Aˣ<VAR>ha : autoParam (p ↑a) _auto✝<GOAL>↑a = cfc id ↑a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : Semifield R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : TopologicalSemiring R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : HasContinuousInv₀ R<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a✝ : A<VAR>a : Aˣ<VAR>ha : autoParam (p ↑a) _auto✝<GOAL>∀ x ∈ spectrum R ↑a, id x ≠ 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>D : ℤ<VAR>f : LaurentSeries K<GOAL>Valued.v f ≤ ↑(Multiplicative.ofAdd (-D)) ↔ ∀ n < D, f.coeff n = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>D : ℤ<VAR>f : LaurentSeries K<VAR>h_val_f : ∀ n < D, f.coeff n = 0<GOAL>Valued.v f ≤ ↑(Multiplicative.ofAdd (-D))
<VAR>a b p q : ℝ<VAR>h✝ h : p.IsConjExponent q<GOAL>q = p / (p - 1)
<VAR>a b p q : ℝ<VAR>h✝ h : p.IsConjExponent q<VAR>this : p⁻¹ + q⁻¹ = 1<GOAL>q = p / (p - 1)
<VAR>a b p q : ℝ<VAR>h✝ h : p.IsConjExponent q<VAR>this : q = (1 - p⁻¹)⁻¹<GOAL>q = p / (p - 1)
<VAR>a : UnitAddCircle<GOAL>∃ p, 0 < p ∧ (fun x => evenKernel a x - if a = 0 then 1 else 0) =O[atTop] fun x => rexp (-p * x)
<VAR>b : ℝ<GOAL>∃ p, 0 < p ∧ (fun x => evenKernel (↑b) x - if ↑b = 0 then 1 else 0) =O[atTop] fun x => rexp (-p * x)
<VAR>b p : ℝ<VAR>hp : 0 < p<VAR>hp' : (fun t => HurwitzKernelBounds.F_int 0 (↑b) t - if ↑b = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)<GOAL>∃ p, 0 < p ∧ (fun x => evenKernel (↑b) x - if ↑b = 0 then 1 else 0) =O[atTop] fun x => rexp (-p * x)
<VAR>b p : ℝ<VAR>hp : 0 < p<VAR>hp' : (fun t => HurwitzKernelBounds.F_int 0 (↑b) t - if ↑b = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)<GOAL>(fun x => evenKernel (↑b) x - if ↑b = 0 then 1 else 0) =ᶠ[atTop] fun t => HurwitzKernelBounds.F_int 0 (↑b) t - if ↑b = 0 then 1 else 0
<VAR>b p : ℝ<VAR>hp : 0 < p<VAR>hp' : (fun t => HurwitzKernelBounds.F_int 0 (↑b) t - if ↑b = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>(evenKernel (↑b) t - if ↑b = 0 then 1 else 0) = HurwitzKernelBounds.F_int 0 (↑b) t - if ↑b = 0 then 1 else 0
<VAR>p q : ℕ+ → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>h✝ : ∃ n, p n<VAR>n m : ℕ+<VAR>h : ∃ n, p n<VAR>h₂ : ∃ n, p (n + 1)<VAR>h1 : ¬p 1<GOAL>PNat.find h = PNat.find h₂ + 1
<VAR>p q : ℕ+ → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>h✝ : ∃ n, p n<VAR>n✝ m : ℕ+<VAR>h : ∃ n, p n<VAR>h₂ : ∃ n, p (n + 1)<VAR>h1 : ¬p 1<VAR>n : ℕ+<GOAL>1 < PNat.find h₂ + 1 → ¬p 1
<VAR>p q : ℕ+ → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>h✝ : ∃ n, p n<VAR>n✝ m : ℕ+<VAR>h : ∃ n, p n<VAR>h₂ : ∃ n, p (n + 1)<VAR>h1 : ¬p 1<VAR>n : ℕ+<GOAL>∀ (n : ℕ+), (n < PNat.find h₂ + 1 → ¬p n) → n + 1 < PNat.find h₂ + 1 → ¬p (n + 1)
<VAR>p q : ℕ+ → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>h✝ : ∃ n, p n<VAR>n✝ m✝ : ℕ+<VAR>h : ∃ n, p n<VAR>h₂ : ∃ n, p (n + 1)<VAR>h1 : ¬p 1<VAR>n m : ℕ+<VAR>a✝ : m < PNat.find h₂ + 1 → ¬p m<VAR>hm : m + 1 < PNat.find h₂ + 1<GOAL>¬p (m + 1)
<VAR>p q : ℕ+ → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>h✝ : ∃ n, p n<VAR>n✝ m✝ : ℕ+<VAR>h : ∃ n, p n<VAR>h₂ : ∃ n, p (n + 1)<VAR>h1 : ¬p 1<VAR>n m : ℕ+<VAR>a✝ : m < PNat.find h₂ + 1 → ¬p m<VAR>hm : ∀ m_1 ≤ m, ¬p (m_1 + 1)<GOAL>¬p (m + 1)