ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>f g : R → R<VAR>a : A<VAR>hg' : ∀ x ∈ spectrum R a, g x ≠ 0<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>cfc (fun x => f x / g x) a = cfc f a * Ring.inverse (cfc g 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>f g : R → R<VAR>a : A<VAR>hg' : ∀ x ∈ spectrum R a, g x ≠ 0<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>cfc (fun x => f x * (g x)⁻¹) a = cfc f a * Ring.inverse (cfc g a)
<VAR>α : Type u_1<VAR>l : List (α → Prop)<VAR>H : ∀ (a : α), (map (fun p => p a) l).TFAE<GOAL>(map (fun p => ∀ (a : α), p a) l).TFAE
<VAR>α : Type u_1<VAR>l : List (α → Prop)<VAR>H : ∀ (a : α), (map (fun p => p a) l).TFAE<GOAL>∀ (j : α → Prop), j ∈ l → ∀ (j_1 : α → Prop), j_1 ∈ l → ((∀ (a : α), j a) ↔ ∀ (a : α), j_1 a)
<VAR>α : Type u_1<VAR>l : List (α → Prop)<VAR>H : ∀ (a : α), (map (fun p => p a) l).TFAE<VAR>p₁ : α → Prop<VAR>hp₁ : p₁ ∈ l<VAR>p₂ : α → Prop<VAR>hp₂ : p₂ ∈ l<GOAL>(∀ (a : α), p₁ a) ↔ ∀ (a : α), p₂ a
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>h_nonempty : Nonempty ((i : ι) → α i)<VAR>I J : Finset ι<VAR>S : Set ((i : { x // x ∈ I }) → α ↑i)<VAR>T : Set ((i : { x // x ∈ J }) → α ↑i)<VAR>h_eq : cylinder I S = cylinder J T<VAR>hJI : J ⊆ I<GOAL>S = (fun f j => f ⟨↑j, ⋯⟩) ⁻¹' T
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>h_nonempty : Nonempty ((i : ι) → α i)<VAR>I J : Finset ι<VAR>S : Set ((i : { x // x ∈ I }) → α ↑i)<VAR>T : Set ((i : { x // x ∈ J }) → α ↑i)<VAR>h_eq : ∀ (x : (i : ι) → α i), x ∈ cylinder I S ↔ x ∈ cylinder J T<VAR>hJI : J ⊆ I<GOAL>S = (fun f j => f ⟨↑j, ⋯⟩) ⁻¹' T
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>h_nonempty : Nonempty ((i : ι) → α i)<VAR>I J : Finset ι<VAR>S : Set ((i : { x // x ∈ I }) → α ↑i)<VAR>T : Set ((i : { x // x ∈ J }) → α ↑i)<VAR>hJI : J ⊆ I<VAR>h_eq : ∀ (x : (i : ι) → α i), (fun i => x ↑i) ∈ S ↔ (fun i => x ↑i) ∈ T<GOAL>S = (fun f j => f ⟨↑j, ⋯⟩) ⁻¹' T
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>h_nonempty : Nonempty ((i : ι) → α i)<VAR>I J : Finset ι<VAR>S : Set ((i : { x // x ∈ I }) → α ↑i)<VAR>T : Set ((i : { x // x ∈ J }) → α ↑i)<VAR>hJI : J ⊆ I<VAR>h_eq : ∀ (x : (i : ι) → α i), (fun i => x ↑i) ∈ S ↔ (fun i => x ↑i) ∈ T<VAR>f : (i : { x // x ∈ I }) → α ↑i<GOAL>f ∈ S ↔ f ∈ (fun f j => f ⟨↑j, ⋯⟩) ⁻¹' T
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>h_nonempty : Nonempty ((i : ι) → α i)<VAR>I J : Finset ι<VAR>S : Set ((i : { x // x ∈ I }) → α ↑i)<VAR>T : Set ((i : { x // x ∈ J }) → α ↑i)<VAR>hJI : J ⊆ I<VAR>h_eq : ∀ (x : (i : ι) → α i), (fun i => x ↑i) ∈ S ↔ (fun i => x ↑i) ∈ T<VAR>f : (i : { x // x ∈ I }) → α ↑i<GOAL>f ∈ S ↔ (fun j => f ⟨↑j, ⋯⟩) ∈ T
<VAR>x y : ℂ<GOAL>sinh ((starRingEnd ℂ) x) = (starRingEnd ℂ) (sinh x)
<VAR>x y : ℂ<GOAL>(starRingEnd ℂ) (cexp x - cexp (-x)) / 2 = (starRingEnd ℂ) (cexp x - cexp (-x)) / (starRingEnd ℂ) 2
<VAR>n : ℕ<VAR>i : Fin (n + 3)<VAR>j : Fin (n + 2)<VAR>H : j.succ < i<VAR>hi : i = 0<GOAL>False
<VAR>n : ℕ<VAR>i : Fin (n + 3)<VAR>j : Fin (n + 2)<VAR>H : j.succ < i<GOAL>δ i ≫ σ j = σ (j.castLT ⋯) ≫ δ (i.pred ⋯)
<VAR>n : ℕ<VAR>i : Fin (n + 3)<VAR>j : Fin (n + 2)<VAR>H : j.succ < i<GOAL>δ i ≫ σ j = δ (i.pred ⋯).succ ≫ σ (j.castLT ⋯).castSucc
<VAR>n : ℕ<VAR>i : Fin (n + 3)<VAR>j : Fin (n + 2)<VAR>H : j.succ < i<GOAL>(j.castLT ⋯).castSucc < i.pred ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s : Rel β γ<VAR>t : Set α<VAR>z : γ<GOAL>z ∈ (r • s).image t ↔ z ∈ s.image (r.image t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s : Rel β γ<VAR>t : Set α<VAR>z : γ<GOAL>(∃ x ∈ t, (r • s) x z) ↔ ∃ x, (∃ x_1 ∈ t, r x_1 x) ∧ s x z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PartialOrder β<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>fst✝¹ : α<VAR>snd✝¹ : β<VAR>fst✝ : α<VAR>snd✝ : β<GOAL>(fst✝¹, snd✝¹) ⋖ (fst✝, snd✝) ↔ (fst✝¹, snd✝¹).1 ⋖ (fst✝, snd✝).1 ∧ (fst✝¹, snd✝¹).2 = (fst✝, snd✝).2 ∨ (fst✝¹, snd✝¹).2 ⋖ (fst✝, snd✝).2 ∧ (fst✝¹, snd✝¹).1 = (fst✝, snd✝).1
<VAR>α : Type u_1<VAR>S s : Set α<VAR>h_s : s ∈ {S}<VAR>t : Set α<VAR>h_t : t ∈ {S}<VAR>a✝ : (s ∩ t).Nonempty<GOAL>s ∩ t ∈ {S}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology β<GOAL>{x | ¬ContinuousWithinAt f (Ioi x) x}.Countable
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology β<GOAL>{x | ¬ContinuousWithinAt f (Ioi x) x} ⊆ {x | ∃ z, f x < z ∧ ∀ (y : α), x < y → z ≤ f y}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x✝ y : α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology β<VAR>x : α<VAR>hx : ¬ContinuousWithinAt f (Ioi x) x<GOAL>∃ z, f x < z ∧ ∀ (y : α), x < y → z ≤ f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x✝ y : α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology β<VAR>x : α<VAR>hx : ∀ (z : β), f x < z → ∃ y, x < y ∧ f y < z<GOAL>ContinuousWithinAt f (Ioi x) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x✝ y : α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology β<VAR>x : α<VAR>hx : ∀ (z : β), f x < z → ∃ y, x < y ∧ f y < z<VAR>m : β<VAR>hm : m < f x<GOAL>∀ᶠ (b : α) in 𝓝[>] x, m < f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x✝ y : α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology β<VAR>x : α<VAR>hx : ∀ (z : β), f x < z → ∃ y, x < y ∧ f y < z<VAR>u : β<VAR>hu : u > f x<GOAL>∀ᶠ (b : α) in 𝓝[>] x, f b < u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x✝ y : α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology β<VAR>x : α<VAR>hx : ∀ (z : β), f x < z → ∃ y, x < y ∧ f y < z<VAR>u : β<VAR>hu : u > f x<VAR>v : α<VAR>xv : x < v<VAR>fvu : f v < u<GOAL>∀ᶠ (b : α) in 𝓝[>] x, f b < u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x✝ y : α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology β<VAR>x : α<VAR>hx : ∀ (z : β), f x < z → ∃ y, x < y ∧ f y < z<VAR>u : β<VAR>hu : u > f x<VAR>v : α<VAR>xv : x < v<VAR>fvu : f v < u<VAR>this : Ioo x v ∈ 𝓝[>] x<GOAL>∀ᶠ (b : α) in 𝓝[>] x, f b < u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x✝ y✝ : α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology β<VAR>x : α<VAR>hx : ∀ (z : β), f x < z → ∃ y, x < y ∧ f y < z<VAR>u : β<VAR>hu : u > f x<VAR>v : α<VAR>xv : x < v<VAR>fvu : f v < u<VAR>this : Ioo x v ∈ 𝓝[>] x<VAR>y : α<VAR>hy : y ∈ Ioo x v<GOAL>f y < u
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝ : HereditarilyLindelofSpace X<VAR>ι : Type u<VAR>U : ι → Set X<VAR>h : ∀ (i : ι), IsOpen (U i)<GOAL>∃ t, t.Countable ∧ ⋃ i ∈ t, U i = ⋃ i, U i
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝ : HereditarilyLindelofSpace X<VAR>ι : Type u<VAR>U : ι → Set X<VAR>h : ∀ (i : ι), IsOpen (U i)<VAR>this : IsLindelof (⋃ i, U i)<GOAL>∃ t, t.Countable ∧ ⋃ i ∈ t, U i = ⋃ i, U i
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>inst✝ : HereditarilyLindelofSpace X<VAR>ι : Type u<VAR>U : ι → Set X<VAR>h : ∀ (i : ι), IsOpen (U i)<VAR>this : IsLindelof (⋃ i, U i)<VAR>t : Set ι<VAR>htc : t.Countable<VAR>htu : ⋃ i, U i ⊆ ⋃ i ∈ t, U i<GOAL>∃ t, t.Countable ∧ ⋃ i ∈ t, U i = ⋃ i, U i
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>inst✝ : HereditarilyLindelofSpace X<VAR>ι : Type u<VAR>U : ι → Set X<VAR>h : ∀ (i : ι), IsOpen (U i)<VAR>this : IsLindelof (⋃ i, U i)<VAR>t : Set ι<VAR>htc : t.Countable<VAR>htu : ⋃ i, U i ⊆ ⋃ i ∈ t, U i<GOAL>⋃ i ∈ t, U i = ⋃ i, U i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<VAR>ι : Type u_5<VAR>αi : ι → Type u_6<VAR>βi : ι → Type u_7<VAR>γi : ι → Type u_8<VAR>ei : (i : ι) → PartialEquiv (αi i) (βi i)<VAR>ei' : (i : ι) → PartialEquiv (βi i) (γi i)<GOAL>(PartialEquiv.pi ei).trans (PartialEquiv.pi ei') = PartialEquiv.pi fun i => (ei i).trans (ei' i)
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>f : Y ⟶ X<VAR>x : FamilyOfElements P S.arrows<VAR>h : x.Compatible<GOAL>(FamilyOfElements.pullback f x).Compatible
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>f : Y ⟶ X<VAR>x : FamilyOfElements P S.arrows<VAR>h : x.SieveCompatible<GOAL>(FamilyOfElements.pullback f x).SieveCompatible
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>f : Y ⟶ X<VAR>x : FamilyOfElements P S.arrows<VAR>h : x.SieveCompatible<VAR>W Z : C<VAR>f₁ : W ⟶ Y<VAR>f₂ : Z ⟶ W<VAR>hf : (Sieve.pullback f S).arrows f₁<GOAL>(f₂ ≫ f₁) ≫ f = f₂ ≫ f₁ ≫ f
<VAR>m n p q : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hq : Fact (Nat.Prime q)<VAR>hpq : p ≠ q<GOAL>↑q ≠ 0
<VAR>a b : Ordinal.{u_1}<GOAL>a ≤ b ♯ a
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : NormalizedGCDMonoid R<VAR>S : Type u_2<VAR>inst✝³ : Ring S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>p : R[X]<VAR>s : S<VAR>hpzero : p ≠ 0<VAR>hp : (aeval s) p = 0<GOAL>(aeval s) p.primPart = 0
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : NormalizedGCDMonoid R<VAR>S : Type u_2<VAR>inst✝³ : Ring S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>p : R[X]<VAR>s : S<VAR>hpzero : p ≠ 0<VAR>hp : (algebraMap R S) p.content * (aeval s) p.primPart = 0<GOAL>(aeval s) p.primPart = 0
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : NormalizedGCDMonoid R<VAR>S : Type u_2<VAR>inst✝³ : Ring S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>p : R[X]<VAR>s : S<VAR>hpzero : p ≠ 0<VAR>hp : (algebraMap R S) p.content * (aeval s) p.primPart = 0<VAR>hcont : p.content ≠ 0<GOAL>(aeval s) p.primPart = 0
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : NormalizedGCDMonoid R<VAR>S : Type u_2<VAR>inst✝³ : Ring S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>p : R[X]<VAR>s : S<VAR>hpzero : p ≠ 0<VAR>hp : (algebraMap R S) p.content * (aeval s) p.primPart = 0<VAR>hcont : (algebraMap R S) p.content ≠ (algebraMap R S) 0<GOAL>(aeval s) p.primPart = 0
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : NormalizedGCDMonoid R<VAR>S : Type u_2<VAR>inst✝³ : Ring S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>p : R[X]<VAR>s : S<VAR>hpzero : p ≠ 0<VAR>hp : (algebraMap R S) p.content * (aeval s) p.primPart = 0<VAR>hcont : (algebraMap R S) p.content ≠ 0<GOAL>(aeval s) p.primPart = 0
<VAR>n✝ m n p : ℕ<VAR>h : p ∈ n.primeFactors<GOAL>¬IsUnit ↑p
<VAR>n✝ m n p : ℕ<VAR>h : p ∈ n.primeFactors<GOAL>¬p.Coprime n
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : DecidableEq n<VAR>M : Matrix n n R<VAR>hM : M.PosSemidef<VAR>z : ℤ<GOAL>(M ^ z).PosSemidef
<VAR>m : Type u_1<VAR>n✝ : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n✝<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : DecidableEq n✝<VAR>M : Matrix n✝ n✝ R<VAR>hM : M.PosSemidef<VAR>n : ℕ<GOAL>(M ^ ↑n).PosSemidef
<VAR>m : Type u_1<VAR>n✝ : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n✝<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : DecidableEq n✝<VAR>M : Matrix n✝ n✝ R<VAR>hM : M.PosSemidef<VAR>n : ℕ<GOAL>(M ^ (-↑n)).PosSemidef
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PseudoMetricSpace α✝<VAR>π : β → Type u_3<VAR>inst✝² : Fintype β<VAR>inst✝¹ : (b : β) → PseudoMetricSpace (π b)<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u_4<VAR>inst✝ : (i : Fin (n + 1)) → PseudoMetricSpace (α i)<VAR>i : Fin (n + 1)<VAR>x y : α i<VAR>f g : (j : Fin n) → α (i.succAbove j)<VAR>c : ℝ≥0<GOAL>nndist (i.insertNth x f) (i.insertNth y g) ≤ c ↔ max (nndist x y) (nndist f g) ≤ c
<VAR>X✝ Y Z : Scheme<VAR>𝒰✝ : X✝.OpenCover<VAR>f : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f) g<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<GOAL>↑(⨆ i, Hom.opensRange (𝒰.map i)) = ↑⊤
<VAR>X✝ Y Z : Scheme<VAR>𝒰✝ : X✝.OpenCover<VAR>f : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f) g<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<GOAL>⋃ i, ↑(Hom.opensRange (𝒰.map i)) = ↑⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : NormedDivisionRing α<VAR>a : α<GOAL>(cobounded α)⁻¹ = 𝓝[≠] 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : NormedDivisionRing α<VAR>a : α<GOAL>comap Inv.inv (comap norm atTop) = comap norm (comap Inv.inv atTop)
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>n : ℕ<VAR>hn : (Nat.card α).Coprime n<VAR>a : α<GOAL>(a ^ (↑n)⁻¹.val) ^ n = a
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Group M<VAR>inst✝¹ : CommRing R<VAR>inst✝ : MulSemiringAction M R<VAR>a : M<VAR>S T : Ideal R<GOAL>a • S ≤ T ↔ S ≤ a⁻¹ • T
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : NormedDivisionRing α<VAR>a z w : α<VAR>hz : z ≠ 0<VAR>hw : w ≠ 0<GOAL>dist z⁻¹ w⁻¹ = dist z w / (‖z‖ * ‖w‖)
<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✝ : Semiring R<VAR>a : α<VAR>b : R<GOAL>b • single a 1 = single a b
<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<VAR>F : Filter X<GOAL>ClusterPt x (F.lift' closure) ↔ ClusterPt x F
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>k : Type u_2<VAR>inst✝ : Field k<VAR>f : k ≃+* K<VAR>φ : K →+* ℂ<VAR>H : IsReal (φ.comp ↑f)<GOAL>IsReal φ
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>k : Type u_2<VAR>inst✝ : Field k<VAR>f : k ≃+* K<VAR>φ : K →+* ℂ<VAR>H : IsReal (φ.comp ↑f)<GOAL>φ = (φ.comp ↑f).comp f.symm.toRingHom
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ inst✝ : NumberField K<VAR>i : Fin (rank K)<GOAL>Additive.ofMul ⟦fundSystem K i⟧ = (basisModTorsion K) i
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ inst✝ : NumberField K<VAR>i : Fin (rank K)<GOAL>Additive.toMul ((basisModTorsion K) i) = Additive.ofMul.symm ((basisModTorsion K) i)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hle : padicValRat p q ≤ padicValRat p r<GOAL>padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>hp : p.natDegree = 0<GOAL>derivative p = 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasZeroMorphisms C<VAR>X✝ Y✝ : C<VAR>f✝ : X✝ ⟶ Y✝<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>c : KernelFork f<VAR>hc : IsLimit c<VAR>hf : f = 0<VAR>e : c.pt ≅ X := hc.conePointUniqueUpToIso (ofId f hf)<GOAL>IsIso (Fork.ι c)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasZeroMorphisms C<VAR>X✝ Y✝ : C<VAR>f✝ : X✝ ⟶ Y✝<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>c : KernelFork f<VAR>hc : IsLimit c<VAR>hf : f = 0<VAR>e : c.pt ≅ X := hc.conePointUniqueUpToIso (ofId f hf)<VAR>eq : e.inv ≫ Fork.ι c = 𝟙 X<GOAL>IsIso (Fork.ι c)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasZeroMorphisms C<VAR>X✝ Y✝ : C<VAR>f✝ : X✝ ⟶ Y✝<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>c : KernelFork f<VAR>hc : IsLimit c<VAR>hf : f = 0<VAR>e : c.pt ≅ X := hc.conePointUniqueUpToIso (ofId f hf)<VAR>eq : e.inv ≫ Fork.ι c = 𝟙 X<VAR>this : IsIso (e.inv ≫ Fork.ι c)<GOAL>IsIso (Fork.ι c)
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<GOAL>(ofFn f).Nodup ↔ Function.Injective f
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<GOAL>(ofFn f).Nodup → Function.Injective f
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m mΩ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>μ : Measure Ω<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : NormedAddCommGroup F<VAR>f : Ω → F<VAR>hf_int : Integrable f μ<GOAL>∀ᵐ (ω : Ω) ∂μ, Integrable f ((condexpKernel μ m) ω)
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m mΩ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>μ : Measure Ω<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : NormedAddCommGroup F<VAR>f : Ω → F<VAR>hf_int : Integrable f μ<GOAL>∀ᵐ (ω : Ω) ∂μ, Integrable f (((condDistrib id id μ).comap id ⋯) ω)
<VAR>ι : Type u_1<VAR>π : ι → Sort u_2<VAR>s : Finset ι<VAR>f g : (i : ι) → π i<VAR>inst✝¹ : (j : ι) → Decidable (j ∈ s)<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>hi : i ∈ s<VAR>v : π i<GOAL>update (s.piecewise f g) i v = s.piecewise (update f i v) g
<VAR>ι : Type u_1<VAR>π : ι → Sort u_2<VAR>s : Finset ι<VAR>f g : (i : ι) → π i<VAR>inst✝¹ : (j : ι) → Decidable (j ∈ s)<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>hi : i ∈ s<VAR>v : π i<GOAL>s.piecewise (update f i v) (update g i v) = s.piecewise (update f i v) g
<VAR>ι : Type u_1<VAR>π : ι → Sort u_2<VAR>s : Finset ι<VAR>f g : (i : ι) → π i<VAR>inst✝¹ : (j : ι) → Decidable (j ∈ s)<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>hi : i ∈ s<VAR>v : π i<VAR>j : ι<VAR>hj : j ∉ s<GOAL>j ≠ i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E'✝ : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁵ : Norm E<VAR>inst✝¹⁴ : Norm F<VAR>inst✝¹³ : Norm G<VAR>inst✝¹² : SeminormedAddCommGroup E'✝<VAR>inst✝¹¹ : SeminormedAddCommGroup F'<VAR>inst✝¹⁰ : SeminormedAddCommGroup G'<VAR>inst✝⁹ : NormedAddCommGroup E''<VAR>inst✝⁸ : NormedAddCommGroup F''<VAR>inst✝⁷ : NormedAddCommGroup G''<VAR>inst✝⁶ : SeminormedRing R<VAR>inst✝⁵ : SeminormedAddGroup E'''<VAR>inst✝⁴ : SeminormedRing R'<VAR>inst✝³ : NormedDivisionRing 𝕜<VAR>inst✝² : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f✝ : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'✝<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>ι : Type u_17<VAR>inst✝¹ : Fintype ι<VAR>E' : ι → Type u_18<VAR>inst✝ : (i : ι) → NormedAddCommGroup (E' i)<VAR>f : α → (i : ι) → E' i<VAR>C : ℝ<VAR>hC : 0 ≤ C<GOAL>IsBigOWith C l f g' ↔ ∀ (i : ι), IsBigOWith C l (fun x => f x i) g'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E'✝ : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁵ : Norm E<VAR>inst✝¹⁴ : Norm F<VAR>inst✝¹³ : Norm G<VAR>inst✝¹² : SeminormedAddCommGroup E'✝<VAR>inst✝¹¹ : SeminormedAddCommGroup F'<VAR>inst✝¹⁰ : SeminormedAddCommGroup G'<VAR>inst✝⁹ : NormedAddCommGroup E''<VAR>inst✝⁸ : NormedAddCommGroup F''<VAR>inst✝⁷ : NormedAddCommGroup G''<VAR>inst✝⁶ : SeminormedRing R<VAR>inst✝⁵ : SeminormedAddGroup E'''<VAR>inst✝⁴ : SeminormedRing R'<VAR>inst✝³ : NormedDivisionRing 𝕜<VAR>inst✝² : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f✝ : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'✝<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>ι : Type u_17<VAR>inst✝¹ : Fintype ι<VAR>E' : ι → Type u_18<VAR>inst✝ : (i : ι) → NormedAddCommGroup (E' i)<VAR>f : α → (i : ι) → E' i<VAR>C : ℝ<VAR>hC : 0 ≤ C<VAR>this : ∀ (x : α), 0 ≤ C * ‖g' x‖<GOAL>IsBigOWith C l f g' ↔ ∀ (i : ι), IsBigOWith C l (fun x => f x i) g'
<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℂ F<VAR>c : ℂ<VAR>R C : ℝ<VAR>f : ℂ → F<VAR>hR : 0 < R<VAR>hd : DiffContOnCl ℂ f (ball c R)<VAR>hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C<VAR>e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL<GOAL>‖deriv f c‖ ≤ C / R
<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℂ F<VAR>c : ℂ<VAR>R C : ℝ<VAR>f : ℂ → F<VAR>hR : 0 < R<VAR>hd : DiffContOnCl ℂ f (ball c R)<VAR>hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C<VAR>e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL<VAR>this : HasDerivAt (⇑e ∘ f) (e (deriv f c)) c<GOAL>‖deriv f c‖ ≤ C / R
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>t' : Set M<VAR>h : t'.Finite<GOAL>(span R t').FG
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>t : Finset M<VAR>h : (↑t).Finite<GOAL>(span R ↑t).FG
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_3<VAR>inst✝ : CommMonoid M<VAR>n : ℕ<VAR>v : Fin n.succ → M<GOAL>∏ i ∈ Ioi 0, v i = ∏ j : Fin n, v j.succ
<VAR>n : ℕ<GOAL>fib (n + 2) = 0 ↔ n + 2 = 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<GOAL>∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ count K v I = I