ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p✝ : R<VAR>k✝ n : ℕ<VAR>h : IsPrimePow n<VAR>hn0 : n ≠ 0<VAR>p k : ℕ<VAR>hk0 : 0 < k<VAR>h1 : n.factorization = Finsupp.single p k<VAR>pp : Nat.Prime p<VAR>q : ℕ<GOAL>(n / p ^ n.factorization p).factorization q = (Nat.factorization 1) q
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p✝ : R<VAR>k✝ n : ℕ<VAR>h : IsPrimePow n<VAR>hn0 : n ≠ 0<VAR>p k : ℕ<VAR>hk0 : 0 < k<VAR>h1 : n.factorization = Finsupp.single p k<VAR>pp : Nat.Prime p<VAR>q : ℕ<GOAL>(Finsupp.erase p (Finsupp.single p k)) q = (Nat.factorization 1) q
<VAR>x y : ℝ<GOAL>normSq (↑x + ↑y * I) = x ^ 2 + y ^ 2
<VAR>𝓕 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>inst✝ : FunLike 𝓕 E F<VAR>f : E → F<VAR>K : ℝ≥0<VAR>h : LipschitzWith K f<VAR>hf : f 1 = 1<VAR>x : E<GOAL>‖f x‖ ≤ ↑K * ‖x‖
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>h : Integrable I l f vol<VAR>hpos₁ : 0 < ε₁<VAR>hpos₂ : 0 < ε₂<VAR>h₁ : l.MemBaseSet I c₁ (h.convergenceR ε₁ c₁) π₁<VAR>h₂ : l.MemBaseSet I c₂ (h.convergenceR ε₂ c₂) π₂<VAR>HU : π₁.iUnion = π₂.iUnion<GOAL>dist (integralSum f vol π₁) (integralSum f vol π₂) ≤ ε₁ + ε₂
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π✝ : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>h : Integrable I l f vol<VAR>hpos₁ : 0 < ε₁<VAR>hpos₂ : 0 < ε₂<VAR>h₁ : l.MemBaseSet I c₁ (h.convergenceR ε₁ c₁) π₁<VAR>h₂ : l.MemBaseSet I c₂ (h.convergenceR ε₂ c₂) π₂<VAR>HU : π₁.iUnion = π₂.iUnion<VAR>π : Prepartition I<VAR>hπU : π.iUnion = ↑I \ π₁.iUnion<VAR>hπc₁ : l.bDistortion = true → π.distortion ≤ c₁<VAR>hπc₂ : l.bDistortion = true → π.distortion ≤ c₂<GOAL>dist (integralSum f vol π₁) (integralSum f vol π₂) ≤ ε₁ + ε₂
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π✝ : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>h : Integrable I l f vol<VAR>hpos₁ : 0 < ε₁<VAR>hpos₂ : 0 < ε₂<VAR>h₁ : l.MemBaseSet I c₁ (h.convergenceR ε₁ c₁) π₁<VAR>h₂ : l.MemBaseSet I c₂ (h.convergenceR ε₂ c₂) π₂<VAR>HU : π₁.iUnion = π₂.iUnion<VAR>π : Prepartition I<VAR>hπU : π.iUnion = ↑I \ π₁.iUnion<VAR>hπc₁ : l.bDistortion = true → π.distortion ≤ c₁<VAR>hπc₂ : l.bDistortion = true → π.distortion ≤ c₂<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0) := fun x => min (h.convergenceR ε₁ c₁ x) (h.convergenceR ε₂ c₂ x)<VAR>πr : TaggedPrepartition I := π.toSubordinate r<GOAL>dist (integralSum f vol π₁) (integralSum f vol π₂) ≤ ε₁ + ε₂
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π✝ : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>h : Integrable I l f vol<VAR>hpos₁ : 0 < ε₁<VAR>hpos₂ : 0 < ε₂<VAR>h₁ : l.MemBaseSet I c₁ (h.convergenceR ε₁ c₁) π₁<VAR>h₂ : l.MemBaseSet I c₂ (h.convergenceR ε₂ c₂) π₂<VAR>HU : π₁.iUnion = π₂.iUnion<VAR>π : Prepartition I<VAR>hπU : π.iUnion = ↑I \ π₁.iUnion<VAR>hπc₁ : l.bDistortion = true → π.distortion ≤ c₁<VAR>hπc₂ : l.bDistortion = true → π.distortion ≤ c₂<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0) := fun x => min (h.convergenceR ε₁ c₁ x) (h.convergenceR ε₂ c₂ x)<VAR>πr : TaggedPrepartition I := π.toSubordinate r<VAR>H₁ : dist (integralSum f vol (π₁.unionComplToSubordinate π hπU r)) (integral I l f vol) ≤ ε₁<GOAL>dist (integralSum f vol π₁) (integralSum f vol π₂) ≤ ε₁ + ε₂
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π✝ : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>h : Integrable I l f vol<VAR>hpos₁ : 0 < ε₁<VAR>hpos₂ : 0 < ε₂<VAR>h₁ : l.MemBaseSet I c₁ (h.convergenceR ε₁ c₁) π₁<VAR>h₂ : l.MemBaseSet I c₂ (h.convergenceR ε₂ c₂) π₂<VAR>HU : π₁.iUnion = π₂.iUnion<VAR>π : Prepartition I<VAR>hπU✝ : π.iUnion = ↑I \ π₁.iUnion<VAR>hπU : π.iUnion = ↑I \ π₂.iUnion<VAR>hπc₁ : l.bDistortion = true → π.distortion ≤ c₁<VAR>hπc₂ : l.bDistortion = true → π.distortion ≤ c₂<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0) := fun x => min (h.convergenceR ε₁ c₁ x) (h.convergenceR ε₂ c₂ x)<VAR>πr : TaggedPrepartition I := π.toSubordinate r<VAR>H₁ : dist (integralSum f vol (π₁.unionComplToSubordinate π hπU✝ r)) (integral I l f vol) ≤ ε₁<GOAL>dist (integralSum f vol π₁) (integralSum f vol π₂) ≤ ε₁ + ε₂
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π✝ : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>h : Integrable I l f vol<VAR>hpos₁ : 0 < ε₁<VAR>hpos₂ : 0 < ε₂<VAR>h₁ : l.MemBaseSet I c₁ (h.convergenceR ε₁ c₁) π₁<VAR>h₂ : l.MemBaseSet I c₂ (h.convergenceR ε₂ c₂) π₂<VAR>HU : π₁.iUnion = π₂.iUnion<VAR>π : Prepartition I<VAR>hπU✝ : π.iUnion = ↑I \ π₁.iUnion<VAR>hπU : π.iUnion = ↑I \ π₂.iUnion<VAR>hπc₁ : l.bDistortion = true → π.distortion ≤ c₁<VAR>hπc₂ : l.bDistortion = true → π.distortion ≤ c₂<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0) := fun x => min (h.convergenceR ε₁ c₁ x) (h.convergenceR ε₂ c₂ x)<VAR>πr : TaggedPrepartition I := π.toSubordinate r<VAR>H₁ : dist (integralSum f vol (π₁.unionComplToSubordinate π hπU✝ r)) (integral I l f vol) ≤ ε₁<VAR>H₂ : dist (integralSum f vol (π₂.unionComplToSubordinate π hπU r)) (integral I l f vol) ≤ ε₂<GOAL>dist (integralSum f vol π₁) (integralSum f vol π₂) ≤ ε₁ + ε₂
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : OrderedCommMonoid N<VAR>f g : ι → N<VAR>s t : Finset ι<GOAL>(∀ i ∈ s, 1 ≤ f i) → (∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1)
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι✝ : Type w<VAR>inst✝⁸ : Ring 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✝¹ : StrongRankCondition R<VAR>inst✝ : Module.Finite R M<VAR>ι : Type w<VAR>b : ι → M<VAR>h : LinearIndependent R b<GOAL>#ι ≤ ↑(finrank R M)
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι✝ : Type w<VAR>inst✝⁸ : Ring 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✝¹ : StrongRankCondition R<VAR>inst✝ : Module.Finite R M<VAR>ι : Type w<VAR>b : ι → M<VAR>h : LinearIndependent R b<GOAL>lift.{max v w, w} #ι ≤ lift.{max v w, w} ↑(finrank R M)
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>v : Vector α n<VAR>i j : Fin n<VAR>a : α<VAR>h✝ : ¬i = j<GOAL>(v.set i a).get j = v.get j
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>s : Set X<VAR>h : X ≃ₜ Y<VAR>hs : IsPreconnected (⇑h '' s)<GOAL>IsPreconnected s
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>c : PullbackCone f f<VAR>hc : IsLimit c<GOAL>Mono f ↔ IsIso c.fst
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>c : PullbackCone f f<VAR>hc : IsLimit c<GOAL>c.fst = c.snd ↔ IsIso c.fst
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f✝ : α ↪ β<VAR>s : Finset α<VAR>β' : Type u_4<VAR>f : β ↪ γ<VAR>g : α ↪ β<VAR>f' : α ↪ β'<VAR>g' : β' ↪ γ<VAR>h_comm : ∀ (a : α), f (g a) = g' (f' a)<GOAL>map f (map g s) = map g' (map f' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>z : ℝ≥0<GOAL>nndist 0 z = z
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝² : Category.{uD', uD} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>P Q X Y : C<VAR>inst✝ : HasBinaryBiproduct X Y<GOAL>(biprod.isoCoprod X Y).hom = biprod.desc coprod.inl coprod.inr
<VAR>x : ℝ<VAR>h : x < 0<GOAL>arctan x⁻¹ = -(π / 2) - arctan x
<VAR>x : ℝ<VAR>h : x < 0<VAR>this : arctan (-x)⁻¹ = π / 2 - arctan (-x)<GOAL>arctan x⁻¹ = -(π / 2) - arctan x
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>x y : M<VAR>c : ↥S<VAR>h : f.toMap (↑c * x) = f.toMap (↑c * y)<GOAL>f.toMap x = f.toMap y
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>x y : M<VAR>c : ↥S<VAR>h : f.toMap ↑c * f.toMap x = f.toMap ↑c * f.toMap y<GOAL>f.toMap x = f.toMap y
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>x y : M<VAR>c : ↥S<VAR>h : f.toMap ↑c * f.toMap x = f.toMap ↑c * f.toMap y<VAR>u : Nˣ<VAR>hu : ↑u = f.toMap ↑c<GOAL>f.toMap x = f.toMap y
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>x y : M<VAR>c : ↥S<VAR>u : Nˣ<VAR>h : ↑u * f.toMap x = ↑u * f.toMap y<VAR>hu : ↑u = f.toMap ↑c<GOAL>f.toMap x = f.toMap y
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>∡ p₂ p₃ p₁ = ↑(Real.arcsin (dist p₁ p₂ / dist p₁ p₃))
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<VAR>hs : (∡ p₂ p₃ p₁).sign = 1<GOAL>∡ p₂ p₃ p₁ = ↑(Real.arcsin (dist p₁ p₂ / dist p₁ p₃))
<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 W : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : W ⟶ X<VAR>x : ↑↑W.toPresheafedSpace<GOAL>x ∈ Set.range ⇑((fun x => pullback.snd (𝒰.map x) f) ((fun x => 𝒰.f (f.val.base x)) x)).val.base
<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 W : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : W ⟶ X<VAR>x : ↑↑W.toPresheafedSpace<GOAL>x ∈ Set.range ⇑((PreservesPullback.iso forgetToTop (𝒰.map (𝒰.f (f.val.base x))) f).hom ≫ pullback.snd (forgetToTop.map (𝒰.map (𝒰.f (f.val.base x)))) (forgetToTop.map f))
<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 W : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : W ⟶ X<VAR>x : ↑↑W.toPresheafedSpace<GOAL>x ∈ {y | ∃ x_1, (forgetToTop.map (𝒰.map (𝒰.f (f.val.base x)))) x_1 = (forgetToTop.map f) y}
<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 W : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : W ⟶ X<VAR>x : ↑↑W.toPresheafedSpace<GOAL>Function.Surjective ⇑(PreservesPullback.iso forgetToTop (𝒰.map (𝒰.f (f.val.base x))) f).hom
<VAR>b : ℕ<VAR>z : ℤ<VAR>hz : z ∈ List.pmap (fun p pp => legendreSym p 1) b.primeFactorsList ⋯<GOAL>z = 1
<VAR>b : ℕ<VAR>z : ℤ<VAR>hz : z ∈ List.pmap (fun p pp => legendreSym p 1) b.primeFactorsList ⋯<VAR>p : ℕ<VAR>hp : p ∈ b.primeFactorsList<VAR>he : legendreSym p 1 = z<GOAL>z = 1
<VAR>b : ℕ<VAR>z : ℤ<VAR>hz : z ∈ List.pmap (fun p pp => legendreSym p 1) b.primeFactorsList ⋯<VAR>p : ℕ<VAR>hp : p ∈ b.primeFactorsList<VAR>he : legendreSym p 1 = z<VAR>this : Fact (Nat.Prime p) := { out := prime_of_mem_primeFactorsList hp }<GOAL>z = 1
<VAR>α : Type u_1<VAR>m n : PosNum<GOAL>m.cmp n = Ordering.eq ↔ m = n
<VAR>α : Type u_1<VAR>m n : PosNum<VAR>this : Ordering.casesOn (m.cmp n) (↑m < ↑n) (m = n) (↑n < ↑m)<GOAL>m.cmp n = Ordering.eq ↔ m = n
<VAR>α : Type u_1<VAR>m n : PosNum<GOAL>Ordering.casesOn (m.cmp n) (↑m < ↑n) (m = n) (↑n < ↑m) → (m.cmp n = Ordering.eq ↔ m = n)
<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>u v : α → ℝ<GOAL>(fun x => ‖f' x‖) =O[l] g ↔ f' =O[l] 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>u v : α → ℝ<GOAL>(∃ c, IsBigOWith c l (fun x => ‖f' x‖) g) ↔ ∃ c, IsBigOWith c l f' g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : TopologicalSpace β<VAR>hα : TopologicalSpace α<VAR>h'α : OrderTopology α<VAR>f : α → β<VAR>a : α<VAR>h : 𝓝[<] a = ⊥<GOAL>leftLim f a = f a
<VAR>α : Type u_1<VAR>inst✝² : CanonicallyLinearOrderedAddCommMonoid α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<GOAL>a - b + min a b = a
<VAR>α : Type u_1<VAR>inst✝² : CanonicallyLinearOrderedAddCommMonoid α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<GOAL>min a b ≤ a
<VAR>α : Type u_1<VAR>inst✝² : GeneralizedBooleanAlgebra α<VAR>inst✝¹ : DecidableRel Disjoint<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>u v a b : α<VAR>hva : Disjoint v a<VAR>hua : u ≤ a<GOAL>compress u v ((a ⊔ v) \ u) = a
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.12556, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>i i' : I₂<VAR>w : ¬c₂.Rel i i'<VAR>j : I₁<GOAL>((fun i i' => { f := fun j => (K.X j).d i i', comm' := ⋯ }) i i').f j = Hom.f 0 j
<VAR>α : Type u<VAR>α' : Type u_1<VAR>β✝ : Type v<VAR>β' : Type u_2<VAR>γ✝ : Type u_3<VAR>φ : Type u_4<VAR>inst✝⁵ : OmegaCompletePartialOrder α<VAR>inst✝⁴ : OmegaCompletePartialOrder β✝<VAR>inst✝³ : OmegaCompletePartialOrder γ✝<VAR>inst✝² : OmegaCompletePartialOrder φ<VAR>inst✝¹ : OmegaCompletePartialOrder α'<VAR>inst✝ : OmegaCompletePartialOrder β'<VAR>β γ : Type v<VAR>f : α →𝒄 Part (β → γ)<VAR>g : α →𝒄 Part β<VAR>x✝ : α<VAR>a✝ : γ<GOAL>(a✝ ∈ Seq.seq (f x✝) fun x => g x✝) ↔ a✝ ∈ (f.bind (flip (_root_.flip map g))) x✝
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<GOAL>(𝓤 α).HasBasis (fun V => V ∈ 𝓤 α ∧ IsClosed V) id
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>t : Set (α × α)<VAR>h : t ∈ 𝓤 α<GOAL>∃ r ∈ 𝓤 α, IsClosed r ∧ r ⊆ t
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>t : Set (α × α)<VAR>h : t ∈ 𝓤 α<VAR>w : Set (α × α)<VAR>w_in : w ∈ 𝓤 α<VAR>w_symm : SymmetricRel w<VAR>r : w ○ w ○ w ⊆ t<GOAL>∃ r ∈ 𝓤 α, IsClosed r ∧ r ⊆ t
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>t : Set (α × α)<VAR>h : t ∈ 𝓤 α<VAR>w : Set (α × α)<VAR>w_in : w ∈ 𝓤 α<VAR>w_symm : SymmetricRel w<VAR>r : w ○ w ○ w ⊆ t<GOAL>closure w ⊆ t
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>t : Set (α × α)<VAR>h : t ∈ 𝓤 α<VAR>w : Set (α × α)<VAR>w_in : w ∈ 𝓤 α<VAR>w_symm : SymmetricRel w<VAR>r : w ○ w ○ w ⊆ t<GOAL>closure w ⊆ w ○ w ○ w
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>t : Set (α × α)<VAR>h : t ∈ 𝓤 α<VAR>w : Set (α × α)<VAR>w_in : w ∈ 𝓤 α<VAR>w_symm : SymmetricRel w<VAR>r : w ○ w ○ w ⊆ t<GOAL>⋂ V ∈ {V | V ∈ 𝓤 α ∧ SymmetricRel V}, V ○ w ○ V ⊆ w ○ w ○ w
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>t : Set (α × α)<VAR>h : t ∈ 𝓤 α<VAR>w : Set (α × α)<VAR>w_in : w ∈ 𝓤 α<VAR>w_symm : SymmetricRel w<VAR>r : w ○ w ○ w ⊆ t<GOAL>⋂ (_ : ?intro.intro.intro.i ∈ {V | V ∈ 𝓤 α ∧ SymmetricRel V}), ?intro.intro.intro.i ○ w ○ ?intro.intro.intro.i ⊆ w ○ w ○ w
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>t : Set (α × α)<VAR>h : t ∈ 𝓤 α<VAR>w : Set (α × α)<VAR>w_in : w ∈ 𝓤 α<VAR>w_symm : SymmetricRel w<VAR>r : w ○ w ○ w ⊆ t<GOAL>Set (α × α)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>t : Set (α × α)<VAR>h : t ∈ 𝓤 α<VAR>w : Set (α × α)<VAR>w_in : w ∈ 𝓤 α<VAR>w_symm : SymmetricRel w<VAR>r : w ○ w ○ w ⊆ t<GOAL>w ∈ {V | V ∈ 𝓤 α ∧ SymmetricRel V}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n : ℤ<GOAL>a * b = 1 ↔ a⁻¹ = b
<VAR>α β : Type<VAR>n : ℕ<VAR>f g : (α → ℕ) → ℕ<VAR>df : DiophFn f<VAR>dg : DiophFn g<GOAL>Dioph fun v => ∃ (h : 1 < v &0), xn h (v &1) = v &2 ∧ yn h (v &1) = v &3
<VAR>α β : Type<VAR>n : ℕ<VAR>f g : (α → ℕ) → ℕ<VAR>df : DiophFn f<VAR>dg : DiophFn g<VAR>proof : Dioph ({v | const (Fin2 4 → ℕ) 1 v < v &0} ∩ ({v | v &1 ≤ v &3} ∩ (((fun v => v &2 = const (Fin2 4 → ℕ) 1 v) ∩ fun v => v &3 = const (Fin2 4 → ℕ) 0 v) ∪ {v | ∃ x, (x :: v) ∈ {v | ∃ x, (x :: v) ∈ {v | ∃ x, (x :: v) ∈ {v | ∃ x, (x :: v) ∈ {v | ∃ x, (x :: v) ∈ (fun v => v &7 * v &7 - (v &5 * v &5 - const (Fin2 (succ 8) → ℕ) 1 v) * v &8 * v &8 = const (Fin2 (succ 8) → ℕ) 1 v) ∩ ((fun v => v &4 * v &4 - (v &5 * v &5 - const (Fin2 (succ 8) → ℕ) 1 v) * v &3 * v &3 = const (Fin2 (succ 8) → ℕ) 1 v) ∩ ((fun v => v &2 * v &2 - (v &0 * v &0 - const (Fin2 (succ 8) → ℕ) 1 v) * v &1 * v &1 = const (Fin2 (succ 8) → ℕ) 1 v) ∩ ({v | const (Fin2 (succ 8) → ℕ) 1 v < v &0} ∩ ((fun v => v &0 ≡ const (Fin2 (succ 8) → ℕ) 1 v [MOD const (Fin2 (succ 8) → ℕ) 4 v * v &8]) ∩ ((fun v => v &0 ≡ v &5 [MOD v &4]) ∩ ({v | const (Fin2 (succ 8) → ℕ) 0 v < v &3} ∩ ((fun v => v &8 * v &8 ∣ v &3) ∩ ((fun v => v &2 ≡ v &7 [MOD v &4]) ∩ fun v => v &1 ≡ v &6 [MOD const (Fin2 (succ 8) → ℕ) 4 v * v &8]))))))))}}}}})))<GOAL>Dioph fun v => ∃ (h : 1 < v &0), xn h (v &1) = v &2 ∧ yn h (v &1) = v &3
<VAR>α β : Type<VAR>n : ℕ<VAR>f g : (α → ℕ) → ℕ<VAR>df : DiophFn f<VAR>dg : DiophFn g<VAR>proof : Dioph ({v | const (Fin2 4 → ℕ) 1 v < v &0} ∩ ({v | v &1 ≤ v &3} ∩ (((fun v => v &2 = const (Fin2 4 → ℕ) 1 v) ∩ fun v => v &3 = const (Fin2 4 → ℕ) 0 v) ∪ {v | ∃ x, (x :: v) ∈ {v | ∃ x, (x :: v) ∈ {v | ∃ x, (x :: v) ∈ {v | ∃ x, (x :: v) ∈ {v | ∃ x, (x :: v) ∈ (fun v => v &7 * v &7 - (v &5 * v &5 - const (Fin2 (succ 8) → ℕ) 1 v) * v &8 * v &8 = const (Fin2 (succ 8) → ℕ) 1 v) ∩ ((fun v => v &4 * v &4 - (v &5 * v &5 - const (Fin2 (succ 8) → ℕ) 1 v) * v &3 * v &3 = const (Fin2 (succ 8) → ℕ) 1 v) ∩ ((fun v => v &2 * v &2 - (v &0 * v &0 - const (Fin2 (succ 8) → ℕ) 1 v) * v &1 * v &1 = const (Fin2 (succ 8) → ℕ) 1 v) ∩ ({v | const (Fin2 (succ 8) → ℕ) 1 v < v &0} ∩ ((fun v => v &0 ≡ const (Fin2 (succ 8) → ℕ) 1 v [MOD const (Fin2 (succ 8) → ℕ) 4 v * v &8]) ∩ ((fun v => v &0 ≡ v &5 [MOD v &4]) ∩ ({v | const (Fin2 (succ 8) → ℕ) 0 v < v &3} ∩ ((fun v => v &8 * v &8 ∣ v &3) ∩ ((fun v => v &2 ≡ v &7 [MOD v &4]) ∩ fun v => v &1 ≡ v &6 [MOD const (Fin2 (succ 8) → ℕ) 4 v * v &8]))))))))}}}}})))<VAR>this : Dioph {v | 1 < v &0 ∧ v &1 ≤ v &3 ∧ (v &2 = 1 ∧ v &3 = 0 ∨ ∃ u w s t b, v &2 * v &2 - (v &0 * v &0 - 1) * v &3 * v &3 = 1 ∧ u * u - (v &0 * v &0 - 1) * w * w = 1 ∧ s * s - (b * b - 1) * t * t = 1 ∧ 1 < b ∧ b ≡ 1 [MOD 4 * v &3] ∧ b ≡ v &0 [MOD u] ∧ 0 < w ∧ v &3 * v &3 ∣ w ∧ s ≡ v &2 [MOD u] ∧ t ≡ v &1 [MOD 4 * v &3])}<GOAL>Dioph fun v => ∃ (h : 1 < v &0), xn h (v &1) = v &2 ∧ yn h (v &1) = v &3
<VAR>M : Type u_1<VAR>inst✝¹⁵ : Monoid M<VAR>N : Type u_2<VAR>inst✝¹⁴ : Monoid N<VAR>P : Type u_3<VAR>inst✝¹³ : Monoid P<VAR>φ : M →* N<VAR>φ' : N →* M<VAR>ψ : N →* P<VAR>χ : M →* P<VAR>A : Type u_4<VAR>inst✝¹² : AddMonoid A<VAR>inst✝¹¹ : DistribMulAction M A<VAR>B : Type u_5<VAR>inst✝¹⁰ : AddMonoid B<VAR>inst✝⁹ : DistribMulAction N B<VAR>B₁ : Type u_6<VAR>inst✝⁸ : AddMonoid B₁<VAR>inst✝⁷ : DistribMulAction M B₁<VAR>C : Type u_7<VAR>inst✝⁶ : AddMonoid C<VAR>inst✝⁵ : DistribMulAction P C<VAR>A' : Type u_8<VAR>inst✝⁴ : AddGroup A'<VAR>inst✝³ : DistribMulAction M A'<VAR>B' : Type u_9<VAR>inst✝² : AddGroup B'<VAR>inst✝¹ : DistribMulAction N B'<VAR>F : Type u_10<VAR>inst✝ : FunLike F A B<VAR>f g : A →ₑ+[φ] B<VAR>h : ↑f = ↑g<VAR>a : A<GOAL>f a = g a
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>A B C : Matrix n n R<VAR>hC : C.det = 1<VAR>hA : A = C * B<GOAL>C.det * B.det = B.det
<VAR>ι : Type uι<VAR>inst✝¹⁰ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝⁸ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝⁶ : SeminormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>E' : ι → Type u_1<VAR>E'' : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E' i)<VAR>inst✝³ : (i : ι) → NormedSpace 𝕜 (E' i)<VAR>inst✝² : (i : ι) → SeminormedAddCommGroup (E'' i)<VAR>inst✝¹ : (i : ι) → NormedSpace 𝕜 (E'' i)<VAR>g : (i : ι) → E' i →L[𝕜] E'' i<VAR>f : (i : ι) → E i →L[𝕜] E' i<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>u : E i →L[𝕜] E' i<GOAL>update (fun j => ↑(f j)) i ↑u = fun j => ↑(update f i u j)