ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>L✝ L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>β : Type v<VAR>f : α → β<VAR>x✝ y x : FreeGroup α<VAR>L : List (α × Bool)<GOAL>(map _root_.id) (Quot.mk Red.Step L) = Quot.mk Red.Step L
<VAR>R : Type u<VAR>inst✝² : Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>A : ι → Submodule R M<VAR>h : IsInternal A<GOAL>iSup A = ⊤
<VAR>R : Type u<VAR>inst✝² : Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>A : ι → Submodule R M<VAR>h : IsInternal A<GOAL>Function.Surjective ⇑((DFinsupp.lsum ℕ) fun i => (A i).subtype)
<VAR>a b c : ℕ<GOAL>(Iio b).card = b
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>c₁ c₂ : R<VAR>q : Basis A c₁ c₂<VAR>F : A →ₐ[R] B<GOAL>F q.i * F q.i = c₁ • 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>c₁ c₂ : R<VAR>q : Basis A c₁ c₂<VAR>F : A →ₐ[R] B<GOAL>F q.j * F q.j = c₂ • 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>c₁ c₂ : R<VAR>q : Basis A c₁ c₂<VAR>F : A →ₐ[R] B<GOAL>F q.i * F q.j = F q.k
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>c₁ c₂ : R<VAR>q : Basis A c₁ c₂<VAR>F : A →ₐ[R] B<GOAL>F q.j * F q.i = -F q.k
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommRing R<VAR>M : Type u_2<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝¹³ : AddCommGroup N<VAR>inst✝¹² : Module R N<VAR>inst✝¹¹ : AddCommGroup P<VAR>inst✝¹⁰ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁹ : Module.Free R M<VAR>inst✝⁸ : Module.Finite R M<VAR>inst✝⁷ : Module.Free R N<VAR>inst✝⁶ : Module.Finite R N<VAR>inst✝⁵ : Module.Free R P<VAR>inst✝⁴ : Module.Finite R P<VAR>p : Submodule R M<VAR>f : M →ₗ[R] M<VAR>h : IsProj p f<VAR>inst✝³ : Module.Free R ↥p<VAR>inst✝² : Module.Finite R ↥p<VAR>inst✝¹ : Module.Free R ↥(ker f)<VAR>inst✝ : Module.Finite R ↥(ker f)<GOAL>(LinearMap.trace R M) f = ↑(finrank R ↥p)
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>f : ι → R[X]<GOAL>(∑ i ∈ ∅, f i).degree ≤ ∅.sup fun b => (f b).degree
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>s✝ : Finset ι<VAR>f : ι → R[X]<VAR>a : ι<VAR>s : Finset ι<VAR>has : a ∉ s<VAR>ih : (∑ i ∈ s, f i).degree ≤ s.sup fun b => (f b).degree<GOAL>(∑ i ∈ Finset.cons a s has, f i).degree ≤ max (f a).degree (∑ i ∈ s, f i).degree
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>s✝ : Finset ι<VAR>f : ι → R[X]<VAR>a : ι<VAR>s : Finset ι<VAR>has : a ∉ s<VAR>ih : (∑ i ∈ s, f i).degree ≤ s.sup fun b => (f b).degree<GOAL>(f a + ∑ x ∈ s, f x).degree ≤ max (f a).degree (∑ i ∈ s, f i).degree
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>s✝ : Finset ι<VAR>f : ι → R[X]<VAR>a : ι<VAR>s : Finset ι<VAR>has : a ∉ s<VAR>ih : (∑ i ∈ s, f i).degree ≤ s.sup fun b => (f b).degree<GOAL>max (f a).degree (∑ i ∈ s, f i).degree ≤ (Finset.cons a s has).sup fun b => (f b).degree
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>s✝ : Finset ι<VAR>f : ι → R[X]<VAR>a : ι<VAR>s : Finset ι<VAR>has : a ∉ s<VAR>ih : (∑ i ∈ s, f i).degree ≤ s.sup fun b => (f b).degree<GOAL>max (f a).degree (∑ i ∈ s, f i).degree ≤ max (f a).degree (s.sup fun b => (f b).degree)
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>(o.oangle y (y - x)).sign = (o.oangle x y).sign
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g✝ : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>H : Type u_7<VAR>inst✝ : NormedAddCommGroup H<VAR>f g : ↥(Lp H 1 μ)<GOAL>dist f g = ∫ (a : α), dist (↑↑f a) (↑↑g a) ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g✝ : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>H : Type u_7<VAR>inst✝ : NormedAddCommGroup H<VAR>f g : ↥(Lp H 1 μ)<GOAL>∫ (a : α), ‖↑↑(f - g) a‖ ∂μ = ∫ (a : α), ‖↑↑f a - ↑↑g a‖ ∂μ
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝³ : Category.{v', u'} A<VAR>inst✝² : ConcreteCategory A<VAR>F₁ F₂ F₃ : Cᵒᵖ ⥤ A<VAR>f₁ : F₁ ⟶ F₂<VAR>f₂ : F₂ ⟶ F₃<VAR>inst✝¹ : IsLocallySurjective J (f₁ ≫ f₂)<VAR>inst✝ : IsLocallyInjective J f₂<VAR>X : C<VAR>x : (forget A).obj (F₂.obj (op X))<VAR>S : Sieve X := imageSieve (f₁ ≫ f₂) ((f₂.app (op X)) x)<VAR>T : ⦃Y : C⦄ → (f : Y ⟶ X) → S.arrows f → Sieve Y := fun Y f hf => equalizerSieve ((f₁.app (op Y)) (localPreimage (f₁ ≫ f₂) ((f₂.app (op X)) x) f hf)) ((F₂.map f.op) x)<GOAL>imageSieve f₁ x ∈ J.sieves X
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝³ : Category.{v', u'} A<VAR>inst✝² : ConcreteCategory A<VAR>F₁ F₂ F₃ : Cᵒᵖ ⥤ A<VAR>f₁ : F₁ ⟶ F₂<VAR>f₂ : F₂ ⟶ F₃<VAR>inst✝¹ : IsLocallySurjective J (f₁ ≫ f₂)<VAR>inst✝ : IsLocallyInjective J f₂<VAR>X : C<VAR>x : (forget A).obj (F₂.obj (op X))<VAR>S : Sieve X := imageSieve (f₁ ≫ f₂) ((f₂.app (op X)) x)<VAR>T : ⦃Y : C⦄ → (f : Y ⟶ X) → S.arrows f → Sieve Y := fun Y f hf => equalizerSieve ((f₁.app (op Y)) (localPreimage (f₁ ≫ f₂) ((f₂.app (op X)) x) f hf)) ((F₂.map f.op) x)<GOAL>Sieve.bind S.arrows T ≤ imageSieve f₁ x
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝³ : Category.{v', u'} A<VAR>inst✝² : ConcreteCategory A<VAR>F₁ F₂ F₃ : Cᵒᵖ ⥤ A<VAR>f₁ : F₁ ⟶ F₂<VAR>f₂ : F₂ ⟶ F₃<VAR>inst✝¹ : IsLocallySurjective J (f₁ ≫ f₂)<VAR>inst✝ : IsLocallyInjective J f₂<VAR>X : C<VAR>x : (forget A).obj (F₂.obj (op X))<VAR>S : Sieve X := imageSieve (f₁ ≫ f₂) ((f₂.app (op X)) x)<VAR>T : ⦃Y : C⦄ → (f : Y ⟶ X) → S.arrows f → Sieve Y := fun Y f hf => equalizerSieve ((f₁.app (op Y)) (localPreimage (f₁ ≫ f₂) ((f₂.app (op X)) x) f hf)) ((F₂.map f.op) x)<GOAL>∀ ⦃Y : C⦄ ⦃f : Y ⟶ unop (op X)⦄, (imageSieve (f₁ ≫ f₂) ((f₂.app (op X)) x)).arrows f → Sieve.pullback f (Sieve.bind S.arrows T) ∈ J.sieves Y
<VAR>R✝ : Type u<VAR>a✝ b✝ : R✝<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R✝<VAR>p q : R✝[X]<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>a b : R[ℕ]<GOAL>{ toFinsupp := a - b } = { toFinsupp := a } - { toFinsupp := b }
<VAR>R✝ : Type u<VAR>a✝ b✝ : R✝<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R✝<VAR>p q : R✝[X]<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>a b : R[ℕ]<GOAL>{ toFinsupp := a } + -{ toFinsupp := b } = { toFinsupp := a } - { toFinsupp := b }
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝ : Category.{v', u'} A<VAR>F : Cᵒᵖ ⥤ Type w<VAR>I : Type u_1<VAR>Y : I → C<VAR>x : FamilyOfElementsOnObjects F Y<VAR>hx : x.IsCompatible<VAR>hY : J.CoversTop Y<VAR>hF : IsSheaf J F<GOAL>∃! s, ∀ (i : I), ↑s (Opposite.op (Y i)) = x i
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝ : Category.{v', u'} A<VAR>F : Cᵒᵖ ⥤ Type w<VAR>I : Type u_1<VAR>Y : I → C<VAR>x : FamilyOfElementsOnObjects F Y<VAR>hx : x.IsCompatible<VAR>hY : J.CoversTop Y<VAR>hF : IsSheaf J F<VAR>H : Presieve.IsSheaf J F<GOAL>∃! s, ∀ (i : I), ↑s (Opposite.op (Y i)) = x i
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝ : Category.{v', u'} A<VAR>F : Cᵒᵖ ⥤ Type w<VAR>I : Type u_1<VAR>Y : I → C<VAR>x : FamilyOfElementsOnObjects F Y<VAR>hx : x.IsCompatible<VAR>hY : J.CoversTop Y<VAR>hF : IsSheaf J F<VAR>H : Presieve.IsSheaf J F<GOAL>∃ x_1, ∀ (i : I), ↑x_1 (Opposite.op (Y i)) = x i
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝ : Category.{v', u'} A<VAR>F : Cᵒᵖ ⥤ Type w<VAR>I : Type u_1<VAR>Y : I → C<VAR>x : FamilyOfElementsOnObjects F Y<VAR>hx : x.IsCompatible<VAR>hY : J.CoversTop Y<VAR>hF : IsSheaf J F<VAR>H : Presieve.IsSheaf J F<GOAL>∀ (y₁ y₂ : ↑F.sections), (∀ (i : I), ↑y₁ (Opposite.op (Y i)) = x i) → (∀ (i : I), ↑y₂ (Opposite.op (Y i)) = x i) → y₁ = y₂
<VAR>h : Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)<GOAL>False
<VAR>h : Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)<VAR>k : ℕ<VAR>hk : ∀ t ⊆ {n | k ≤ n}, ∑' (n : ↑t), {p | Nat.Prime p}.indicator (fun n => 1 / ↑n) ↑n ∈ Iio (1 / 2)<GOAL>False
<VAR>h : Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)<VAR>k : ℕ<VAR>hk : ∑' (n : ↑({p | Nat.Prime p} ∩ {p | k ≤ p})), {p | Nat.Prime p}.indicator (fun n => 1 / ↑n) ↑n ∈ Iio (1 / 2)<GOAL>False
<VAR>h : Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)<VAR>k : ℕ<VAR>hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) x < 1 / 2<GOAL>False
<VAR>h : Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)<VAR>k : ℕ<VAR>hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) x < 1 / 2<VAR>h' : Summable (({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator fun n => 1 / ↑n)<GOAL>False
<VAR>h : Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)<VAR>k : ℕ<VAR>hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) x < 1 / 2<VAR>h' : Summable (({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator fun n => 1 / ↑n)<GOAL>∑ p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow, 1 / ↑p ≤ ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) x
<VAR>h : Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)<VAR>k : ℕ<VAR>hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) x < 1 / 2<VAR>h' : Summable (({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator fun n => 1 / ↑n)<VAR>p : ℕ<VAR>hp : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow<GOAL>1 / ↑p = ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) p
<VAR>h : Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)<VAR>k : ℕ<VAR>hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) x < 1 / 2<VAR>h' : Summable (({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator fun n => 1 / ↑n)<VAR>p : ℕ<VAR>hp : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow<VAR>hp₁ : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow.val<VAR>hp₂ : p ∉ k.primesBelow<GOAL>1 / ↑p = ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) p
<VAR>h : Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)<VAR>k : ℕ<VAR>hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) x < 1 / 2<VAR>h' : Summable (({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator fun n => 1 / ↑n)<VAR>p : ℕ<VAR>hp : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow<VAR>hp₁ : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow.val<VAR>hp₂ : p ∉ k.primesBelow<VAR>hpp : Nat.Prime p<GOAL>1 / ↑p = ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) p
<VAR>h : Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)<VAR>k : ℕ<VAR>hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) x < 1 / 2<VAR>h' : Summable (({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator fun n => 1 / ↑n)<VAR>p : ℕ<VAR>hp : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow<VAR>hp₁ : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow.val<VAR>hp₂ : p ∉ k.primesBelow<VAR>hpp : Nat.Prime p<GOAL>p ∈ {p | k ≤ p}
<VAR>X Y : LightProfinite<VAR>f : X ⟶ Y<VAR>h : EffectiveEpi f<GOAL>Function.Surjective ⇑f
<VAR>X Y : LightProfinite<VAR>f : X ⟶ Y<VAR>h : EffectiveEpi f<GOAL>Epi f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : Group α<VAR>inst✝¹ : UniformGroup α<VAR>inst✝ : Group β<VAR>ι : Sort u_3<VAR>us' : ι → UniformSpace β<VAR>h' : ∀ (i : ι), UniformGroup β<GOAL>UniformGroup β
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : InnerProductSpace 𝕜 E<VAR>inst✝⁵ : InnerProductSpace 𝕜 F<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : CompleteSpace F<VAR>E' : Type u_4<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : InnerProductSpace ℂ E'<VAR>inst✝ : CompleteSpace E'<VAR>T : E' →L[ℂ] E'<GOAL>T.IsPositive ↔ ∀ (x : E'), ↑(re ⟪T x, x⟫_ℂ) = ⟪T x, x⟫_ℂ ∧ 0 ≤ re ⟪T x, x⟫_ℂ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : InnerProductSpace 𝕜 E<VAR>inst✝⁵ : InnerProductSpace 𝕜 F<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : CompleteSpace F<VAR>E' : Type u_4<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : InnerProductSpace ℂ E'<VAR>inst✝ : CompleteSpace E'<VAR>T : E' →L[ℂ] E'<GOAL>((∀ (v : E'), ↑(re ⟪↑T v, v⟫_ℂ) = ⟪↑T v, v⟫_ℂ) ∧ ∀ (x : E'), 0 ≤ T.reApplyInnerSelf x) ↔ (∀ (x : E'), ↑(re ⟪T x, x⟫_ℂ) = ⟪T x, x⟫_ℂ) ∧ ∀ (x : E'), 0 ≤ re ⟪T x, x⟫_ℂ
<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>c : F''<GOAL>(f'' =O[l] fun _x => c) ↔ (c = 0 → f'' =ᶠ[l] 0) ∧ IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => ‖f'' x‖
<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>c : F''<GOAL>((c = 0 → f'' =ᶠ[l] 0) ∧ IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => ‖f'' x‖) → f'' =O[l] fun _x => c
<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>c : F''<VAR>hcf : c = 0 → f'' =ᶠ[l] 0<VAR>hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => ‖f'' x‖<GOAL>f'' =O[l] fun _x => c
<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>c : F''<VAR>hcf : c = 0 → f'' =ᶠ[l] 0<VAR>hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => ‖f'' x‖<VAR>hc : c = 0<GOAL>f'' =O[l] fun _x => c
<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>c : F''<VAR>hcf : c = 0 → f'' =ᶠ[l] 0<VAR>hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => ‖f'' x‖<VAR>hc : c ≠ 0<GOAL>f'' =O[l] fun _x => c
<VAR>R : Type u_1<VAR>inst✝ : Monoid R<VAR>a b : R<VAR>h : a * b = 1<GOAL>IsRightRegular 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>h : ¬IsSFiniteKernel κ<GOAL>κ ⊗ₖ η = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>h : ¬IsSFiniteKernel κ<GOAL>¬(IsSFiniteKernel κ ∧ IsSFiniteKernel η)
<VAR>V : Type u<VAR>G✝ : SimpleGraph V<VAR>K L L' M : Set V<VAR>G : SimpleGraph V<VAR>v w : V<VAR>vK : v ∉ K<VAR>wK : w ∉ K<VAR>a : G.Adj v w<GOAL>G.componentComplMk vK = G.componentComplMk wK
<VAR>V : Type u<VAR>G✝ : SimpleGraph V<VAR>K L L' M : Set V<VAR>G : SimpleGraph V<VAR>v w : V<VAR>vK : v ∉ K<VAR>wK : w ∉ K<VAR>a : G.Adj v w<GOAL>(induce Kᶜ G).Reachable ⟨v, vK⟩ ⟨w, wK⟩
<VAR>V : Type u<VAR>G✝ : SimpleGraph V<VAR>K L L' M : Set V<VAR>G : SimpleGraph V<VAR>v w : V<VAR>vK : v ∉ K<VAR>wK : w ∉ K<VAR>a : G.Adj v w<GOAL>(induce Kᶜ G).Adj ⟨v, vK⟩ ⟨w, wK⟩
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>h : IsCoprime (x + y * z) y<VAR>a b : R<VAR>H : a * (x + y * z) + b * y = 1<GOAL>a * x + (a * z + b) * y = 1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>s : Multiset R<VAR>k : ℕ<VAR>h : k ≤ card s<GOAL>(map (fun t => X - C t) s).prod.coeff k = (-1) ^ (card s - k) * s.esymm (card s - k)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>s : Multiset R<VAR>k : ℕ<VAR>h : k ≤ card s<GOAL>(map (fun x => X + C (-x)) s).prod.coeff k = (-1) ^ (card s - k) * s.esymm (card s - k)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>s : Multiset R<VAR>k : ℕ<VAR>h : k ≤ card s<GOAL>(map (fun x => X + C (-x)) s).prod.coeff k = (map (fun r => X + C r) (map (fun t => -t) s)).prod.coeff ?convert_1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>s : Multiset R<VAR>k : ℕ<VAR>h : k ≤ card s<GOAL>(-1) ^ (card s - k) * s.esymm (card s - k) = (map (fun t => -t) s).esymm (card (map (fun t => -t) s) - ?convert_1)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>s : Multiset R<VAR>k : ℕ<VAR>h : k ≤ card s<GOAL>ℕ
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>s : Multiset R<VAR>k : ℕ<VAR>h : k ≤ card s<GOAL>?convert_1 ≤ card (map (fun t => -t) s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s✝ t : Set E<VAR>x✝ y : E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>x : E<VAR>hx : x ∉ (convexHull 𝕜) (s \ {x})<GOAL>Convex 𝕜 (s \ {x})
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s✝ t : Set E<VAR>x✝ y : E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>x : E<VAR>hx : x ∉ (convexHull 𝕜) (s \ {x})<GOAL>s \ {x} = (convexHull 𝕜) (s \ {x})
<VAR>M' : Type u_1<VAR>inst✝⁴ : Monoid M'<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝³ : Monoid M<VAR>inst✝² : Monoid N<VAR>inst✝¹ : Monoid P<VAR>φ : M →* N<VAR>ψ : N →* M<VAR>h : Function.RightInverse ⇑φ ⇑ψ<VAR>χ : M →* M<VAR>inst✝ : IsId χ<GOAL>ψ.comp φ = χ
<VAR>M' : Type u_1<VAR>inst✝⁴ : Monoid M'<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝³ : Monoid M<VAR>inst✝² : Monoid N<VAR>inst✝¹ : Monoid P<VAR>φ : M →* N<VAR>ψ : N →* M<VAR>h : Function.RightInverse ⇑φ ⇑ψ<VAR>χ : M →* M<VAR>inst✝ : IsId χ<GOAL>_root_.id = ⇑(id M)
<VAR>n✝ b m n : ℕ<VAR>hb : 0 < b<GOAL>b.digits n ++ b.digits m = b.digits (n + b ^ (b.digits n).length * m)
<VAR>n✝ m n : ℕ<VAR>hb : 0 < succ 0<GOAL>(succ 0).digits n ++ (succ 0).digits m = (succ 0).digits (n + succ 0 ^ ((succ 0).digits n).length * m)
<VAR>n✝ b m n : ℕ<VAR>hb✝ : 0 < b<VAR>hb : succ 0 < b<GOAL>b.digits n ++ b.digits m = b.digits (n + b ^ (b.digits n).length * m)
<VAR>n✝ b m n : ℕ<VAR>hb✝ : 0 < b<VAR>hb : succ 0 < b<GOAL>b.digits n ++ b.digits m = b.digits (ofDigits b (b.digits n ++ b.digits m))
<VAR>n✝ b m n : ℕ<VAR>hb✝ : 0 < b<VAR>hb : succ 0 < b<VAR>l : ℕ<VAR>hl : l ∈ b.digits n ++ b.digits m<GOAL>l < b
<VAR>n✝ b m n : ℕ<VAR>hb✝ : 0 < b<VAR>hb : succ 0 < b<VAR>h_append : b.digits n ++ b.digits m ≠ []<GOAL>(b.digits n ++ b.digits m).getLast h_append ≠ 0
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>v w : V<VAR>s : Set (Sym2 V)<VAR>p : G.Walk v w<VAR>hp : ∀ e ∈ p.edges, e ∉ s<GOAL>Walk.map (Hom.mapSpanningSubgraphs ⋯) (toDeleteEdges s p hp) = p