ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>v : ι → M<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : CommRing R₂<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M''<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R₂ M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>c d : R<VAR>x✝ y : M<VAR>b✝ : Basis ι R M<VAR>inst✝ : Nontrivial R<VAR>b : Basis ι R M<VAR>w : Set M<VAR>hi : LinearIndependent (ι := { x // x ∈ w }) R Subtype.val<VAR>h : Set.range ⇑b ≤ w<VAR>x : M<VAR>p : x ∈ w<VAR>q : x ∉ Set.range ⇑b<VAR>u : ι ↪ ↑w := { toFun := fun i => ⟨b i, ⋯⟩, inj' := ⋯ }<VAR>e : (Finsupp.total (↑w) M R Subtype.val) (Finsupp.embDomain u (b.repr x)) = ↑⟨x, p⟩<GOAL>False
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>v : ι → M<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : CommRing R₂<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M''<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R₂ M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>c d : R<VAR>x✝ y : M<VAR>b✝ : Basis ι R M<VAR>inst✝ : Nontrivial R<VAR>b : Basis ι R M<VAR>w : Set M<VAR>hi : LinearIndependent (ι := { x // x ∈ w }) R Subtype.val<VAR>h : Set.range ⇑b ≤ w<VAR>x : M<VAR>p : x ∈ w<VAR>q : x ∉ Set.range ⇑b<VAR>u : ι ↪ ↑w := { toFun := fun i => ⟨b i, ⋯⟩, inj' := ⋯ }<VAR>e : (Finsupp.total (↑w) M R Subtype.val) (Finsupp.embDomain u (b.repr x)) = ↑⟨x, p⟩<GOAL>⟨x, p⟩ ∉ (Finsupp.embDomain u (b.repr x)).support
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>v : ι → M<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : CommRing R₂<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M''<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R₂ M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>c d : R<VAR>x✝ y : M<VAR>b✝ : Basis ι R M<VAR>inst✝ : Nontrivial R<VAR>b : Basis ι R M<VAR>w : Set M<VAR>hi : LinearIndependent (ι := { x // x ∈ w }) R Subtype.val<VAR>h : Set.range ⇑b ≤ w<VAR>x : M<VAR>p : x ∈ w<VAR>q : x ∉ Set.range ⇑b<VAR>u : ι ↪ ↑w := { toFun := fun i => ⟨b i, ⋯⟩, inj' := ⋯ }<VAR>e : (Finsupp.total (↑w) M R Subtype.val) (Finsupp.embDomain u (b.repr x)) = ↑⟨x, p⟩<GOAL>¬∃ a ∈ (b.repr x).support, u a = ⟨x, p⟩
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>v : ι → M<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : CommRing R₂<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M''<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R₂ M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>c d : R<VAR>x✝ y : M<VAR>b✝ : Basis ι R M<VAR>inst✝ : Nontrivial R<VAR>b : Basis ι R M<VAR>w : Set M<VAR>hi : LinearIndependent (ι := { x // x ∈ w }) R Subtype.val<VAR>h : Set.range ⇑b ≤ w<VAR>x : M<VAR>p : x ∈ w<VAR>q : x ∉ Set.range ⇑b<VAR>u : ι ↪ ↑w := { toFun := fun i => ⟨b i, ⋯⟩, inj' := ⋯ }<VAR>e : (Finsupp.total (↑w) M R Subtype.val) (Finsupp.embDomain u (b.repr x)) = ↑⟨x, p⟩<VAR>j : ι<VAR>W : u j = ⟨x, p⟩<GOAL>False
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>v : ι → M<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : CommRing R₂<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M''<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R₂ M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>c d : R<VAR>x✝ y : M<VAR>b✝ : Basis ι R M<VAR>inst✝ : Nontrivial R<VAR>b : Basis ι R M<VAR>w : Set M<VAR>hi : LinearIndependent (ι := { x // x ∈ w }) R Subtype.val<VAR>h : Set.range ⇑b ≤ w<VAR>x : M<VAR>p : x ∈ w<VAR>q : x ∉ Set.range ⇑b<VAR>u : ι ↪ ↑w := { toFun := fun i => ⟨b i, ⋯⟩, inj' := ⋯ }<VAR>e : (Finsupp.total (↑w) M R Subtype.val) (Finsupp.embDomain u (b.repr x)) = ↑⟨x, p⟩<VAR>j : ι<VAR>W : b j = x<GOAL>False
<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 ⊓ 𝓟 (univ.pi s)).NeBot ↔ ∀ (i : ι), (f i ⊓ 𝓟 (s i)).NeBot
<VAR>η : Type u_1<VAR>α : Type u_2<VAR>ι : Type u_3<VAR>κ : Type u_4<VAR>l✝ : Line α ι<VAR>i✝ : ι<VAR>a✝ x : α<VAR>inst✝ : Nontrivial α<VAR>l m : Line α ι<VAR>hlm : (fun x x_1 i => (x.idxFun i).getD x_1) l = (fun x x_1 i => (x.idxFun i).getD x_1) m<VAR>i : ι<VAR>a : α<GOAL>a ∈ l.idxFun i ↔ a ∈ m.idxFun i
<VAR>η : Type u_1<VAR>α : Type u_2<VAR>ι : Type u_3<VAR>κ : Type u_4<VAR>l✝ : Line α ι<VAR>i✝ : ι<VAR>a✝ x : α<VAR>inst✝ : Nontrivial α<VAR>l m : Line α ι<VAR>hlm : (fun x x_1 i => (x.idxFun i).getD x_1) l = (fun x x_1 i => (x.idxFun i).getD x_1) m<VAR>i : ι<VAR>a b : α<VAR>hba : b ≠ a<GOAL>a ∈ l.idxFun i ↔ a ∈ m.idxFun i
<VAR>η : Type u_1<VAR>α : Type u_2<VAR>ι : Type u_3<VAR>κ : Type u_4<VAR>l✝ : Line α ι<VAR>i✝ : ι<VAR>a✝ x : α<VAR>inst✝ : Nontrivial α<VAR>l m : Line α ι<VAR>i : ι<VAR>a b : α<VAR>hba : b ≠ a<VAR>hlm : ∀ (a : α) (a_1 : ι), (l.idxFun a_1).getD a = (m.idxFun a_1).getD a<GOAL>l.idxFun i = some a ↔ m.idxFun i = some a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>a a' : α<VAR>v : Vector α n<GOAL>a ∈ v.toList ↔ ∃ i, v.get i = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>a a' : α<VAR>v : Vector α n<GOAL>(∃ i, ∃ (h : i < v.toList.length), v.toList.get ⟨i, h⟩ = a) ↔ ∃ i, ∃ (h : i < n), v.toList.get (Fin.cast ⋯ ⟨i, h⟩) = a
<VAR>m : ℕ∞<GOAL>↑m = 0 ↔ m = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : SeminormedRing α<VAR>l : List α<VAR>hl : l ≠ []<GOAL>(map norm l).prod = (fun a => ↑a) (map nnnorm l).prod
<VAR>α : Type u<VAR>β✝ : Type v<VAR>m : Type u → Type v<VAR>inst✝¹ : Monad m<VAR>inst✝ : LawfulMonad m<VAR>β : Type u<VAR>f : ℕ → α → m β<VAR>as : List α<GOAL>as.mapIdxM f = List.traverse (uncurry f) as.enum
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<VAR>s : Set α<GOAL>↑e '' (e.source ∩ s) = e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝³ : PseudoMetricSpace α<VAR>inst✝² : PseudoMetricSpace β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : DilationClass F α β<VAR>f : F<VAR>s : Set α<GOAL>Metric.diam (⇑f '' s) = ↑(ratio f) * Metric.diam s
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsIntegrallyClosed R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>hI : I.IsMaximal<VAR>hI' : I ≠ ⊥<VAR>hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤<VAR>hx' : _root_.IsIntegral R x<VAR>J : Ideal S<VAR>hJ : J ∈ normalizedFactors (Ideal.map (algebraMap R S) I)<GOAL>Multiset.count J (normalizedFactors (Ideal.map (algebraMap R S) I)) = Multiset.count J (Multiset.map (fun f => ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f)) (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsIntegrallyClosed R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>hI : I.IsMaximal<VAR>hI' : I ≠ ⊥<VAR>hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤<VAR>hx' : _root_.IsIntegral R x<VAR>J : Ideal S<VAR>hJ : J ∈ normalizedFactors (Ideal.map (algebraMap R S) I)<VAR>this : multiplicity J (Ideal.map (algebraMap R S) I) = multiplicity (↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩)) (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))<GOAL>Multiset.count J (normalizedFactors (Ideal.map (algebraMap R S) I)) = Multiset.count J (Multiset.map (fun f => ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f)) (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsIntegrallyClosed R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>hI : I.IsMaximal<VAR>hI' : I ≠ ⊥<VAR>hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤<VAR>hx' : _root_.IsIntegral R x<VAR>J : Ideal S<VAR>hJ : J ∈ normalizedFactors (Ideal.map (algebraMap R S) I)<VAR>this : Multiset.count J (normalizedFactors (Ideal.map (algebraMap R S) I)) = Multiset.count (↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩)) (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)))<GOAL>Multiset.count J (normalizedFactors (Ideal.map (algebraMap R S) I)) = Multiset.count J (Multiset.map (fun f => ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f)) (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsIntegrallyClosed R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>hI : I.IsMaximal<VAR>hI' : I ≠ ⊥<VAR>hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤<VAR>hx' : _root_.IsIntegral R x<VAR>J : Ideal S<VAR>hJ : J ∈ normalizedFactors (Ideal.map (algebraMap R S) I)<VAR>this : ↑(Multiset.count J (normalizedFactors (Ideal.map (algebraMap R S) I))) = ↑(Multiset.count (normalize ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩)) (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))))<GOAL>↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩) ∈ normalizedFactors ?m.130449
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsIntegrallyClosed R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>hI : I.IsMaximal<VAR>hI' : I ≠ ⊥<VAR>hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤<VAR>hx' : _root_.IsIntegral R x<VAR>J : Ideal S<VAR>hJ : J ∈ normalizedFactors (Ideal.map (algebraMap R S) I)<VAR>this : ↑(Multiset.count J (normalizedFactors (Ideal.map (algebraMap R S) I))) = ↑(Multiset.count (normalize ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩)) (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))))<GOAL>(R ⧸ I)[X]
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsIntegrallyClosed R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>hI : I.IsMaximal<VAR>hI' : I ≠ ⊥<VAR>hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤<VAR>hx' : _root_.IsIntegral R x<VAR>J : Ideal S<VAR>hJ : J ∈ normalizedFactors (Ideal.map (algebraMap R S) I)<VAR>this : ↑(Multiset.count (normalize J) (normalizedFactors (Ideal.map (algebraMap R S) I))) = multiplicity (↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩)) (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))<GOAL>Irreducible ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsIntegrallyClosed R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>hI : I.IsMaximal<VAR>hI' : I ≠ ⊥<VAR>hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤<VAR>hx' : _root_.IsIntegral R x<VAR>J : Ideal S<VAR>hJ : J ∈ normalizedFactors (Ideal.map (algebraMap R S) I)<VAR>this : ↑(Multiset.count (normalize J) (normalizedFactors (Ideal.map (algebraMap R S) I))) = multiplicity (↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩)) (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))<GOAL>Polynomial.map (Ideal.Quotient.mk I) (minpoly R x) ≠ 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsIntegrallyClosed R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>hI : I.IsMaximal<VAR>hI' : I ≠ ⊥<VAR>hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤<VAR>hx' : _root_.IsIntegral R x<VAR>J : Ideal S<VAR>hJ : J ∈ normalizedFactors (Ideal.map (algebraMap R S) I)<VAR>this : multiplicity J (Ideal.map (algebraMap R S) I) = multiplicity (↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩)) (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))<GOAL>Irreducible J
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsIntegrallyClosed R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>hI : I.IsMaximal<VAR>hI' : I ≠ ⊥<VAR>hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤<VAR>hx' : _root_.IsIntegral R x<VAR>J : Ideal S<VAR>hJ : J ∈ normalizedFactors (Ideal.map (algebraMap R S) I)<VAR>this : multiplicity J (Ideal.map (algebraMap R S) I) = multiplicity (↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩)) (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))<GOAL>Ideal.map (algebraMap R S) I ≠ 0
<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 z : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hz : z ≠ 0<GOAL>o.oangle x z - o.oangle x y = o.oangle y z
<VAR>C : Type u<VAR>inst✝¹⁰ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝⁹ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝⁸ : Category.{max v u, w₂} E<VAR>F✝ : D ⥤ E<VAR>inst✝⁷ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁶ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝⁵ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝⁴ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝³ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F✝<VAR>inst✝² : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F✝<VAR>P✝ P : Cᵒᵖ ⥤ D<VAR>F : D ⥤ E<VAR>inst✝¹ : (F : D ⥤ E) → (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>inst✝ : (F : D ⥤ E) → (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<GOAL>(J.plusCompIso F (J.plusObj P)).hom ≫ J.plusMap (J.plusCompIso F P).hom ≫ 𝟙 (J.plusObj (J.plusObj (P ⋙ F))) = (J.plusCompIso F (J.plusObj P)).hom ≫ J.plusMap (J.plusCompIso F P).hom
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>π : α → Type u_1<VAR>inst✝ : Finite α<VAR>s : (a : α) → Set (π a)<VAR>hs : ∀ (a : α), (s a).Countable<GOAL>{f | ∀ (a : α), f a ∈ s a}.Countable
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>K : ℝ≥0<VAR>s : Set α<VAR>f : α → β<GOAL>LipschitzOnWith K f s ↔ ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ ↑K * dist x y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>K : ℝ≥0<VAR>s : Set α<VAR>f : α → β<GOAL>(∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → ↑(nndist (f x) (f y)) ≤ ↑K * ↑(nndist x y)) ↔ ∀ x ∈ s, ∀ y ∈ s, ↑(nndist (f x) (f y)) ≤ ↑K * ↑(nndist x y)
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c d s t : ℝ<VAR>ht : 0 < t<GOAL>IntegrableOn (fun x => x ^ s) (Set.Ioo 0 t) volume ↔ -1 < s
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c d s t : ℝ<VAR>ht : 0 < t<VAR>h : IntegrableOn (fun x => x ^ s) (Set.Ioo 0 t) volume<GOAL>-1 < s
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c d s t : ℝ<VAR>ht : 0 < t<VAR>h : s ≤ -1<GOAL>¬IntegrableOn (fun x => x ^ s) (Set.Ioo 0 t) volume
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c d s t : ℝ<VAR>ht : 0 < t<VAR>h : s ≤ -1<VAR>H : IntegrableOn (fun x => x ^ s) (Set.Ioo 0 t) volume<GOAL>False
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c d s t : ℝ<VAR>ht : 0 < t<VAR>h : s ≤ -1<VAR>H : IntegrableOn (fun x => x ^ s) (Set.Ioo 0 t) volume<VAR>I : 0 < min 1 t<GOAL>False
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c d s t : ℝ<VAR>ht : 0 < t<VAR>h : s ≤ -1<VAR>H : IntegrableOn (fun x => x ^ s) (Set.Ioo 0 t) volume<VAR>I : 0 < min 1 t<VAR>H' : IntegrableOn (fun x => x ^ s) (Set.Ioo 0 (min 1 t)) volume<GOAL>False
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c d s t : ℝ<VAR>ht : 0 < t<VAR>h : s ≤ -1<VAR>H : IntegrableOn (fun x => x ^ s) (Set.Ioo 0 t) volume<VAR>I : 0 < min 1 t<VAR>H' : IntegrableOn (fun x => x ^ s) (Set.Ioo 0 (min 1 t)) volume<VAR>this : IntegrableOn (fun x => x⁻¹) (Set.Ioo 0 (min 1 t)) volume<GOAL>False
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c d s t : ℝ<VAR>ht : 0 < t<VAR>h : s ≤ -1<VAR>H : IntegrableOn (fun x => x ^ s) (Set.Ioo 0 t) volume<VAR>I : 0 < min 1 t<VAR>H' : IntegrableOn (fun x => x ^ s) (Set.Ioo 0 (min 1 t)) volume<VAR>this✝ : IntegrableOn (fun x => x⁻¹) (Set.Ioo 0 (min 1 t)) volume<VAR>this : IntervalIntegrable (fun x => x⁻¹) volume 0 (min 1 t)<GOAL>False
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>U : Set E<VAR>f : ℂ → ℂ<VAR>g : E → ℂ<VAR>z₀ w : ℂ<VAR>ε r m : ℝ<VAR>h : DiffContOnCl ℂ f (ball z₀ r)<VAR>hr : 0 < r<VAR>hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖<VAR>hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀<VAR>v : ℂ<VAR>hv : v ∈ ball (f z₀) (ε / 2)<GOAL>v ∈ f '' closedBall z₀ r
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>U : Set E<VAR>f : ℂ → ℂ<VAR>g : E → ℂ<VAR>z₀ w : ℂ<VAR>ε r m : ℝ<VAR>h : DiffContOnCl ℂ f (ball z₀ r)<VAR>hr : 0 < r<VAR>hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖<VAR>hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀<VAR>v : ℂ<VAR>hv : v ∈ ball (f z₀) (ε / 2)<VAR>h1 : DiffContOnCl ℂ (fun z => f z - v) (ball z₀ r)<GOAL>v ∈ f '' closedBall z₀ r
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>U : Set E<VAR>f : ℂ → ℂ<VAR>g : E → ℂ<VAR>z₀ w : ℂ<VAR>ε r m : ℝ<VAR>h : DiffContOnCl ℂ f (ball z₀ r)<VAR>hr : 0 < r<VAR>hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖<VAR>hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀<VAR>v : ℂ<VAR>hv : v ∈ ball (f z₀) (ε / 2)<VAR>h1 : DiffContOnCl ℂ (fun z => f z - v) (ball z₀ r)<VAR>h2 : ContinuousOn (fun z => ‖f z - v‖) (closedBall z₀ r)<GOAL>v ∈ f '' closedBall z₀ r
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>U : Set E<VAR>f : ℂ → ℂ<VAR>g : E → ℂ<VAR>z₀ w : ℂ<VAR>ε r m : ℝ<VAR>h : DiffContOnCl ℂ f (ball z₀ r)<VAR>hr : 0 < r<VAR>hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖<VAR>hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀<VAR>v : ℂ<VAR>hv : v ∈ ball (f z₀) (ε / 2)<VAR>h1 : DiffContOnCl ℂ (fun z => f z - v) (ball z₀ r)<VAR>h2 : ContinuousOn (fun z => ‖f z - v‖) (closedBall z₀ r)<VAR>h3 : AnalyticOn ℂ f (ball z₀ r)<GOAL>v ∈ f '' closedBall z₀ r
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>U : Set E<VAR>f : ℂ → ℂ<VAR>g : E → ℂ<VAR>z₀ w : ℂ<VAR>ε r m : ℝ<VAR>h : DiffContOnCl ℂ f (ball z₀ r)<VAR>hr : 0 < r<VAR>hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖<VAR>hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀<VAR>v : ℂ<VAR>hv : v ∈ ball (f z₀) (ε / 2)<VAR>h1 : DiffContOnCl ℂ (fun z => f z - v) (ball z₀ r)<VAR>h2 : ContinuousOn (fun z => ‖f z - v‖) (closedBall z₀ r)<VAR>h3 : AnalyticOn ℂ f (ball z₀ r)<VAR>h4 : ∀ z ∈ sphere z₀ r, ε / 2 ≤ ‖f z - v‖<GOAL>v ∈ f '' closedBall z₀ r
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>U : Set E<VAR>f : ℂ → ℂ<VAR>g : E → ℂ<VAR>z₀ w : ℂ<VAR>ε r m : ℝ<VAR>h : DiffContOnCl ℂ f (ball z₀ r)<VAR>hr : 0 < r<VAR>hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖<VAR>hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀<VAR>v : ℂ<VAR>hv : v ∈ ball (f z₀) (ε / 2)<VAR>h1 : DiffContOnCl ℂ (fun z => f z - v) (ball z₀ r)<VAR>h2 : ContinuousOn (fun z => ‖f z - v‖) (closedBall z₀ r)<VAR>h3 : AnalyticOn ℂ f (ball z₀ r)<VAR>h4 : ∀ z ∈ sphere z₀ r, ε / 2 ≤ ‖f z - v‖<VAR>h5 : ‖f z₀ - v‖ < ε / 2<GOAL>v ∈ f '' closedBall z₀ r
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>U : Set E<VAR>f : ℂ → ℂ<VAR>g : E → ℂ<VAR>z₀ w : ℂ<VAR>ε r m : ℝ<VAR>h : DiffContOnCl ℂ f (ball z₀ r)<VAR>hr : 0 < r<VAR>hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖<VAR>hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀<VAR>v : ℂ<VAR>hv : v ∈ ball (f z₀) (ε / 2)<VAR>h1 : DiffContOnCl ℂ (fun z => f z - v) (ball z₀ r)<VAR>h2 : ContinuousOn (fun z => ‖f z - v‖) (closedBall z₀ r)<VAR>h3 : AnalyticOn ℂ f (ball z₀ r)<VAR>h4 : ∀ z ∈ sphere z₀ r, ε / 2 ≤ ‖f z - v‖<VAR>h5 : ‖f z₀ - v‖ < ε / 2<VAR>z : ℂ<VAR>hz1 : z ∈ ball z₀ r<VAR>hz2 : IsLocalMin (fun z => ‖f z - v‖) z<GOAL>v ∈ f '' closedBall z₀ r
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>U : Set E<VAR>f : ℂ → ℂ<VAR>g : E → ℂ<VAR>z₀ w : ℂ<VAR>ε r m : ℝ<VAR>h : DiffContOnCl ℂ f (ball z₀ r)<VAR>hr : 0 < r<VAR>hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖<VAR>hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀<VAR>v : ℂ<VAR>hv : v ∈ ball (f z₀) (ε / 2)<VAR>h1 : DiffContOnCl ℂ (fun z => f z - v) (ball z₀ r)<VAR>h2 : ContinuousOn (fun z => ‖f z - v‖) (closedBall z₀ r)<VAR>h3 : AnalyticOn ℂ f (ball z₀ r)<VAR>h4 : ∀ z ∈ sphere z₀ r, ε / 2 ≤ ‖f z - v‖<VAR>h5 : ‖f z₀ - v‖ < ε / 2<VAR>z : ℂ<VAR>hz1 : z ∈ ball z₀ r<VAR>hz2 : IsLocalMin (fun z => ‖f z - v‖) z<GOAL>f z - v = 0
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>U : Set E<VAR>f : ℂ → ℂ<VAR>g : E → ℂ<VAR>z₀ w : ℂ<VAR>ε r m : ℝ<VAR>h : DiffContOnCl ℂ f (ball z₀ r)<VAR>hr : 0 < r<VAR>hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖<VAR>hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀<VAR>v : ℂ<VAR>hv : v ∈ ball (f z₀) (ε / 2)<VAR>h1 : DiffContOnCl ℂ (fun z => f z - v) (ball z₀ r)<VAR>h2 : ContinuousOn (fun z => ‖f z - v‖) (closedBall z₀ r)<VAR>h3 : AnalyticOn ℂ f (ball z₀ r)<VAR>h4 : ∀ z ∈ sphere z₀ r, ε / 2 ≤ ‖f z - v‖<VAR>h5 : ‖f z₀ - v‖ < ε / 2<VAR>z : ℂ<VAR>hz1 : z ∈ ball z₀ r<VAR>hz2 : IsLocalMin (fun z => ‖f z - v‖) z<VAR>h6 : ∀ᶠ (y : ℂ) in 𝓝 z, DifferentiableAt ℂ (fun z => f z - v) y<GOAL>f z - v = 0
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>U : Set E<VAR>f : ℂ → ℂ<VAR>g : E → ℂ<VAR>z₀ w : ℂ<VAR>ε r m : ℝ<VAR>h : DiffContOnCl ℂ f (ball z₀ r)<VAR>hr : 0 < r<VAR>hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖<VAR>hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀<VAR>v : ℂ<VAR>hv : v ∈ ball (f z₀) (ε / 2)<VAR>h1 : DiffContOnCl ℂ (fun z => f z - v) (ball z₀ r)<VAR>h2 : ContinuousOn (fun z => ‖f z - v‖) (closedBall z₀ r)<VAR>h3 : AnalyticOn ℂ f (ball z₀ r)<VAR>h4 : ∀ z ∈ sphere z₀ r, ε / 2 ≤ ‖f z - v‖<VAR>h5 : ‖f z₀ - v‖ < ε / 2<VAR>z : ℂ<VAR>hz1 : z ∈ ball z₀ r<VAR>hz2 : IsLocalMin (fun z => ‖f z - v‖) z<VAR>h6 : ∀ᶠ (y : ℂ) in 𝓝 z, DifferentiableAt ℂ (fun z => f z - v) y<VAR>key : ∀ᶠ (z_1 : ℂ) in 𝓝 z, f z_1 - v = f z - v<GOAL>False