ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{?u.132220, u_2} D<VAR>inst✝¹ : Category.{?u.132224, u_3} E<VAR>inst✝ : Preregular C<VAR>W X w✝ Y : C<VAR>f : Y ⟶ X<VAR>hf : EffectiveEpi f<VAR>hS : ∃ f_1, ((ofArrows (fun x => Y) fun x => f) = ofArrows (fun x => w✝) fun x => f_1) ∧ EffectiveEpi f_1<VAR>this : (ofArrows (fun x => Y) fun x => f).regular<VAR>h_colim : IsColimit (Sieve.generate (ofArrows (fun x => Y) fun x => f)).arrows.cocone<VAR>x : FamilyOfElements (yoneda.obj W) (ofArrows (fun x => Y) fun x => f)<VAR>hx : x.Compatible<VAR>x_ext : FamilyOfElements (yoneda.obj W) (Sieve.generate (ofArrows (fun x => Y) fun x => f)).arrows := x.sieveExtend<VAR>hx_ext : x.sieveExtend.Compatible<GOAL>∃! t, x.IsAmalgamation t
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{?u.132220, u_2} D<VAR>inst✝¹ : Category.{?u.132224, u_3} E<VAR>inst✝ : Preregular C<VAR>W X w✝ Y : C<VAR>f : Y ⟶ X<VAR>hf : EffectiveEpi f<VAR>hS : ∃ f_1, ((ofArrows (fun x => Y) fun x => f) = ofArrows (fun x => w✝) fun x => f_1) ∧ EffectiveEpi f_1<VAR>this : (ofArrows (fun x => Y) fun x => f).regular<VAR>h_colim : IsColimit (Sieve.generate (ofArrows (fun x => Y) fun x => f)).arrows.cocone<VAR>x : FamilyOfElements (yoneda.obj W) (ofArrows (fun x => Y) fun x => f)<VAR>hx : x.Compatible<VAR>x_ext : FamilyOfElements (yoneda.obj W) (Sieve.generate (ofArrows (fun x => Y) fun x => f)).arrows := x.sieveExtend<VAR>hx_ext : x.sieveExtend.Compatible<VAR>S : Sieve X := Sieve.generate (ofArrows (fun x => Y) fun x => match x with | PUnit.unit => f)<GOAL>∃! t, x.IsAmalgamation t
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{?u.132220, u_2} D<VAR>inst✝¹ : Category.{?u.132224, u_3} E<VAR>inst✝ : Preregular C<VAR>W X w✝ Y : C<VAR>f : Y ⟶ X<VAR>hf : EffectiveEpi f<VAR>hS : ∃ f_1, ((ofArrows (fun x => Y) fun x => f) = ofArrows (fun x => w✝) fun x => f_1) ∧ EffectiveEpi f_1<VAR>this : (ofArrows (fun x => Y) fun x => f).regular<VAR>h_colim : IsColimit (Sieve.generate (ofArrows (fun x => Y) fun x => f)).arrows.cocone<VAR>x : FamilyOfElements (yoneda.obj W) (ofArrows (fun x => Y) fun x => f)<VAR>hx : x.Compatible<VAR>x_ext : FamilyOfElements (yoneda.obj W) (Sieve.generate (ofArrows (fun x => Y) fun x => f)).arrows := x.sieveExtend<VAR>hx_ext : x.sieveExtend.Compatible<VAR>S : Sieve X := Sieve.generate (ofArrows (fun x => Y) fun x => match x with | PUnit.unit => f)<VAR>t : (yoneda.obj W).obj (op X)<VAR>t_amalg : x_ext.IsAmalgamation t<VAR>t_uniq : ∀ (y : (yoneda.obj W).obj (op X)), (fun t => x_ext.IsAmalgamation t) y → y = t<GOAL>∃! t, x.IsAmalgamation t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>h_mono : Monotone f<VAR>h_surj : Surjective f<VAR>a : α<GOAL>SurjOn f (Ioi a) (Ioi (f a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>h_mono : Monotone f<VAR>h_surj : Surjective f<VAR>a : α<GOAL>SurjOn f (Iic a)ᶜ (Ioi (f a))ᶜᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>h_mono : Monotone f<VAR>h_surj : Surjective f<VAR>a : α<GOAL>MapsTo f (Iic a) (Ioi (f a))ᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝¹ : DivisionMonoid K<VAR>inst✝ : HasDistribNeg K<VAR>a✝ b✝ a b : K<GOAL>-b / a = -(b / a)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>x : R<GOAL>(constantCoeff.comp C) x = (RingHom.id R) x
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b : ℝ<VAR>f✝ g : ℝ → E<VAR>μ : Measure ℝ<VAR>f : ℝ → E<GOAL>‖∫ (x : ℝ) in a..b, f x ∂μ‖ = ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖
<VAR>J : Type u'<VAR>inst✝⁴ : Category.{v', u'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasColimitsOfShape J TopCat<VAR>inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)<VAR>inst✝ : HasLimitsOfShape Jᵒᵖ C<VAR>F : J ⥤ PresheafedSpace C<VAR>U : Opens ↑↑(Limits.colimit F)<VAR>j : J<GOAL>(colimitPresheafObjIsoComponentwiseLimit F U).hom ≫ limit.π (componentwiseDiagram F U) (op j) = (colimit.ι F j).c.app (op U)
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>j : σ<VAR>f : MvPolynomial σ R<GOAL>degreeOf j (f * X j) ≤ degreeOf j f + 1
<VAR>A✝ : Type u_1<VAR>inst✝⁹ : AddCommGroup A✝<VAR>inst✝⁸ : Module ℂ A✝<VAR>inst✝⁷ : StarAddMonoid A✝<VAR>inst✝⁶ : StarModule ℂ A✝<VAR>A : Type u_2<VAR>inst✝⁵ : NonUnitalRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : Module ℂ A<VAR>inst✝² : IsScalarTower ℂ A A<VAR>inst✝¹ : SMulCommClass ℂ A A<VAR>inst✝ : StarModule ℂ A<VAR>a : A<VAR>a_eq : a = ↑(ℜ a) + I • ↑(ℑ a)<GOAL>star (↑(ℜ a) + I • ↑(ℑ a)) * (↑(ℜ a) + I • ↑(ℑ a)) + (↑(ℜ a) + I • ↑(ℑ a)) * star (↑(ℜ a) + I • ↑(ℑ a)) = 2 • (↑(ℜ a) * ↑(ℜ a) + ↑(ℑ a) * ↑(ℑ a))
<VAR>A✝ : Type u_1<VAR>inst✝⁹ : AddCommGroup A✝<VAR>inst✝⁸ : Module ℂ A✝<VAR>inst✝⁷ : StarAddMonoid A✝<VAR>inst✝⁶ : StarModule ℂ A✝<VAR>A : Type u_2<VAR>inst✝⁵ : NonUnitalRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : Module ℂ A<VAR>inst✝² : IsScalarTower ℂ A A<VAR>inst✝¹ : SMulCommClass ℂ A A<VAR>inst✝ : StarModule ℂ A<VAR>a : A<VAR>a_eq : a = ↑(ℜ a) + I • ↑(ℑ a)<GOAL>↑(ℜ a) * ↑(ℜ a) + -(I • (↑(ℑ a) * ↑(ℜ a))) + (I • (↑(ℜ a) * ↑(ℑ a)) + ↑(ℑ a) * ↑(ℑ a)) + (↑(ℜ a) * ↑(ℜ a) + I • (↑(ℑ a) * ↑(ℜ a)) + (↑(ℑ a) * ↑(ℑ a) + -(I • (↑(ℜ a) * ↑(ℑ a))))) = ↑(ℜ a) * ↑(ℜ a) + ↑(ℜ a) * ↑(ℜ a) + (↑(ℑ a) * ↑(ℑ a) + ↑(ℑ a) * ↑(ℑ a))
<VAR>σ : Type u_1<VAR>τ✝ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>τ : Type u_6<VAR>f : σ → τ<VAR>φ : MvPolynomial σ R<GOAL>constantCoeff ((rename f) φ) = constantCoeff φ
<VAR>σ : Type u_1<VAR>τ✝ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>τ : Type u_6<VAR>f : σ → τ<VAR>φ : MvPolynomial σ R<GOAL>∀ (a : R), constantCoeff ((rename f) (C a)) = constantCoeff (C a)
<VAR>σ : Type u_1<VAR>τ✝ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>τ : Type u_6<VAR>f : σ → τ<VAR>φ : MvPolynomial σ R<GOAL>∀ (p q : MvPolynomial σ R), constantCoeff ((rename f) p) = constantCoeff p → constantCoeff ((rename f) q) = constantCoeff q → constantCoeff ((rename f) (p + q)) = constantCoeff (p + q)
<VAR>σ : Type u_1<VAR>τ✝ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>τ : Type u_6<VAR>f : σ → τ<VAR>φ : MvPolynomial σ R<GOAL>∀ (p : MvPolynomial σ R) (n : σ), constantCoeff ((rename f) p) = constantCoeff p → constantCoeff ((rename f) (p * X n)) = constantCoeff (p * X n)
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝¹ : Group H<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>w₁ w₂ : ReducedWord G A B<VAR>hprod : ReducedWord.prod φ w₁ = ReducedWord.prod φ w₂<VAR>d : TransversalPair G A B<GOAL>List.map Prod.fst w₁.toList = List.map Prod.fst w₂.toList ∧ ∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁.head⁻¹ * w₂.head ∈ toSubgroup A B (-u)
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝¹ : Group H<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>w₁ w₂ : ReducedWord G A B<VAR>hprod : ReducedWord.prod φ w₁ = ReducedWord.prod φ w₂<VAR>d : TransversalPair G A B<VAR>w₁' : NormalWord d<VAR>hw₁'1 : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₁<VAR>hw₁'2 : List.map Prod.fst w₁'.toList = List.map Prod.fst w₁.toList<VAR>hw₁'3 : ∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁'.head⁻¹ * w₁.head ∈ toSubgroup A B (-u)<GOAL>List.map Prod.fst w₁.toList = List.map Prod.fst w₂.toList ∧ ∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁.head⁻¹ * w₂.head ∈ toSubgroup A B (-u)
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝¹ : Group H<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>w₁ w₂ : ReducedWord G A B<VAR>hprod : ReducedWord.prod φ w₁ = ReducedWord.prod φ w₂<VAR>d : TransversalPair G A B<VAR>w₁' : NormalWord d<VAR>hw₁'1 : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₁<VAR>hw₁'2 : List.map Prod.fst w₁'.toList = List.map Prod.fst w₁.toList<VAR>hw₁'3 : ∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁'.head⁻¹ * w₁.head ∈ toSubgroup A B (-u)<VAR>w₂' : NormalWord d<VAR>hw₂'1 : ReducedWord.prod φ w₂'.toReducedWord = ReducedWord.prod φ w₂<VAR>hw₂'2 : List.map Prod.fst w₂'.toList = List.map Prod.fst w₂.toList<VAR>hw₂'3 : ∀ u ∈ Option.map Prod.fst w₂.toList.head?, w₂'.head⁻¹ * w₂.head ∈ toSubgroup A B (-u)<GOAL>List.map Prod.fst w₁.toList = List.map Prod.fst w₂.toList ∧ ∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁.head⁻¹ * w₂.head ∈ toSubgroup A B (-u)
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝¹ : Group H<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>w₁ w₂ : ReducedWord G A B<VAR>hprod : ReducedWord.prod φ w₁ = ReducedWord.prod φ w₂<VAR>d : TransversalPair G A B<VAR>w₁' : NormalWord d<VAR>hw₁'1 : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₁<VAR>hw₁'2 : List.map Prod.fst w₁'.toList = List.map Prod.fst w₁.toList<VAR>hw₁'3 : ∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁'.head⁻¹ * w₁.head ∈ toSubgroup A B (-u)<VAR>w₂' : NormalWord d<VAR>hw₂'1 : ReducedWord.prod φ w₂'.toReducedWord = ReducedWord.prod φ w₂<VAR>hw₂'2 : List.map Prod.fst w₂'.toList = List.map Prod.fst w₂.toList<VAR>hw₂'3 : ∀ u ∈ Option.map Prod.fst w₂.toList.head?, w₂'.head⁻¹ * w₂.head ∈ toSubgroup A B (-u)<VAR>this : w₁' = w₂'<GOAL>List.map Prod.fst w₁.toList = List.map Prod.fst w₂.toList ∧ ∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁.head⁻¹ * w₂.head ∈ toSubgroup A B (-u)
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝¹ : Group H<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>w₁ w₂ : ReducedWord G A B<VAR>hprod : ReducedWord.prod φ w₁ = ReducedWord.prod φ w₂<VAR>d : TransversalPair G A B<VAR>w₁' : NormalWord d<VAR>hw₁'1 : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₁<VAR>hw₁'2 : List.map Prod.fst w₁'.toList = List.map Prod.fst w₁.toList<VAR>hw₁'3 : ∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁'.head⁻¹ * w₁.head ∈ toSubgroup A B (-u)<VAR>hw₂'1 : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₂<VAR>hw₂'2 : List.map Prod.fst w₁'.toList = List.map Prod.fst w₂.toList<VAR>hw₂'3 : ∀ u ∈ Option.map Prod.fst w₂.toList.head?, w₁'.head⁻¹ * w₂.head ∈ toSubgroup A B (-u)<GOAL>∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁.head⁻¹ * w₂.head ∈ toSubgroup A B (-u)
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝¹ : Group H<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>w₁ w₂ : ReducedWord G A B<VAR>hprod : ReducedWord.prod φ w₁ = ReducedWord.prod φ w₂<VAR>d : TransversalPair G A B<VAR>w₁' : NormalWord d<VAR>hw₁'1 : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₁<VAR>hw₁'2 : List.map Prod.fst w₁'.toList = List.map Prod.fst w₁.toList<VAR>hw₂'1 : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₂<VAR>hw₂'2 : List.map Prod.fst w₁'.toList = List.map Prod.fst w₂.toList<VAR>hw₁'3 : ∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁'.head • ↑(toSubgroup A B (-u)) = w₁.head • ↑(toSubgroup A B (-u))<VAR>hw₂'3 : ∀ u ∈ Option.map Prod.fst w₂.toList.head?, w₁'.head • ↑(toSubgroup A B (-u)) = w₂.head • ↑(toSubgroup A B (-u))<GOAL>∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁.head • ↑(toSubgroup A B (-u)) = w₂.head • ↑(toSubgroup A B (-u))
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝¹ : Group H<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>w₁ w₂ : ReducedWord G A B<VAR>hprod : ReducedWord.prod φ w₁ = ReducedWord.prod φ w₂<VAR>d : TransversalPair G A B<VAR>w₁' : NormalWord d<VAR>hw₁'1 : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₁<VAR>hw₁'2 : List.map Prod.fst w₁'.toList = List.map Prod.fst w₁.toList<VAR>hw₂'1 : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₂<VAR>hw₂'2 : List.map Prod.fst w₁'.toList = List.map Prod.fst w₂.toList<VAR>hw₁'3 : ∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁'.head • ↑(toSubgroup A B (-u)) = w₁.head • ↑(toSubgroup A B (-u))<VAR>hw₂'3 : ∀ u ∈ Option.map Prod.fst w₂.toList.head?, w₁'.head • ↑(toSubgroup A B (-u)) = w₂.head • ↑(toSubgroup A B (-u))<VAR>u : ℤˣ<VAR>hu : u ∈ Option.map Prod.fst w₁.toList.head?<GOAL>u ∈ Option.map Prod.fst w₂.toList.head?
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : ConditionallyCompleteLattice α<VAR>f : Filter β<VAR>u : β → α<VAR>p : β → Prop<GOAL>blimsup u f p = limsup (u ∘ Subtype.val) (comap Subtype.val f)
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>c : 𝕜<VAR>s✝ t : Set E<VAR>x✝ y : E<VAR>r : ℝ≥0∞<VAR>hc : c ≠ 0<VAR>s : Set E<VAR>x : E<GOAL>egauge 𝕜 (c • s) x = egauge 𝕜 s x / ↑‖c‖₊
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>c : 𝕜<VAR>s✝ t : Set E<VAR>x✝ y : E<VAR>r : ℝ≥0∞<VAR>hc : c ≠ 0<VAR>s : Set E<VAR>x : E<GOAL>egauge 𝕜 (c • s) x ≤ egauge 𝕜 s x / ↑‖c‖₊
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>c : 𝕜<VAR>s✝ t : Set E<VAR>x✝ y : E<VAR>r : ℝ≥0∞<VAR>hc : c ≠ 0<VAR>s : Set E<VAR>x : E<GOAL>egauge 𝕜 (c • s) x * ↑‖c‖₊ ≤ egauge 𝕜 s x
<VAR>d : ℤ<VAR>a : Solution₁ d<VAR>h : IsFundamental a<VAR>n : ℤ<GOAL>a ^ n = 1 ↔ n = 0
<VAR>d : ℤ<VAR>a : Solution₁ d<VAR>h : IsFundamental a<VAR>n : ℤ<GOAL>a ^ n = a ^ 0 ↔ n = 0
<VAR>M₀ : Type u_1<VAR>M₀' : Type u_2<VAR>inst✝² : MulZeroOneClass M₀<VAR>inst✝¹ : Nontrivial M₀<VAR>G₀ : Type u_3<VAR>inst✝ : GroupWithZero G₀<VAR>a : G₀<VAR>h : a ≠ 0<VAR>a_eq_0 : a⁻¹ = 0<GOAL>False
<VAR>M₀ : Type u_1<VAR>M₀' : Type u_2<VAR>inst✝² : MulZeroOneClass M₀<VAR>inst✝¹ : Nontrivial M₀<VAR>G₀ : Type u_3<VAR>inst✝ : GroupWithZero G₀<VAR>a : G₀<VAR>h : a ≠ 0<VAR>a_eq_0 : a⁻¹ = 0<VAR>this : a * a⁻¹ = 1<GOAL>False
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>h : 0 < x<VAR>h₁ : 0 < y<GOAL>logb b x ≤ logb b y ↔ y ≤ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>hx : IsPeriodicPt f n x<VAR>hy : IsPeriodicPt f n y<VAR>hn : 0 < n<VAR>h : f x = f y<GOAL>x = y
<VAR>f : StieltjesFunction<VAR>hf0 : Tendsto (↑f) atBot (𝓝 0)<VAR>hf1 : Tendsto (↑f) atTop (𝓝 1)<GOAL>cdf f.measure = f
<VAR>f : StieltjesFunction<VAR>hf0 : Tendsto (↑f) atBot (𝓝 0)<VAR>hf1 : Tendsto (↑f) atTop (𝓝 1)<GOAL>(cdf f.measure).measure = f.measure
<VAR>f : StieltjesFunction<VAR>hf0 : Tendsto (↑f) atBot (𝓝 0)<VAR>hf1 : Tendsto (↑f) atTop (𝓝 1)<VAR>h_prob : IsProbabilityMeasure f.measure<GOAL>(cdf f.measure).measure = f.measure
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>i : ι<GOAL>Continuous (f.toPOUFun i)
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>i : ι<GOAL>LocallyFinite fun i => mulSupport fun x => 1 - (f i) x
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>i : ι<GOAL>LocallyFinite fun i => support ⇑(f i)
<VAR>K : Type u_1<VAR>n✝ : ℕ<VAR>inst✝ : LinearOrderedField K<VAR>c : ContFract K<VAR>n : ℕ<GOAL>(↑↑c).convs.get n = Stream'.get (↑↑c).convs' n
<VAR>K : Type u_1<VAR>n✝ : ℕ<VAR>inst✝ : LinearOrderedField K<VAR>c : ContFract K<VAR>n : ℕ<GOAL>∀ {gp : Pair K} {m : ℕ}, m < n → (↑↑c).s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
<VAR>K : Type u_1<VAR>n✝ : ℕ<VAR>inst✝ : LinearOrderedField K<VAR>c : ContFract K<VAR>n : ℕ<VAR>gp : Pair K<VAR>m : ℕ<VAR>a✝ : m < n<VAR>s_nth_eq : (↑↑c).s.get? m = some gp<GOAL>0 < gp.a ∧ 0 < gp.b
<VAR>r s : ℤ<VAR>h2 : IsCoprime s r<GOAL>IsCoprime (r * r + s * s) r
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>x y : R<VAR>h : IsCoprime x y<VAR>z : R<GOAL>IsCoprime x (y + z * x)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>x y : R<VAR>h : IsCoprime x y<VAR>z : R<GOAL>IsCoprime (y + z * x) x
<VAR>R : Type u_1<VAR>m i : ℕ<VAR>hi : i ∈ range (m + 1)<GOAL>i ≤ 2 * m + 1
<VAR>R : Type u_1<VAR>m : ℕ<VAR>this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i<GOAL>2 * ∑ i ∈ range (m + 1), (2 * m + 1).choose i = ∑ i ∈ range (m + 1), (2 * m + 1).choose i + ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i)
<VAR>R : Type u_1<VAR>m : ℕ<VAR>this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i<GOAL>∑ i ∈ range (m + 1), (2 * m + 1).choose i + ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i + ∑ i ∈ Ico (m + 1) (2 * m + 2), (2 * m + 1).choose i
<VAR>R : Type u_1<VAR>m : ℕ<VAR>this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i<GOAL>∑ i ∈ Ico 0 (m + 1), (2 * m + 1).choose i + ∑ j ∈ Ico (2 * m + 1 + 1 - (m + 1)) (2 * m + 1 + 1 - 0), (2 * m + 1).choose j = ∑ i ∈ Ico 0 (m + 1), (2 * m + 1).choose i + ∑ i ∈ Ico (m + 1) (2 * m + 2), (2 * m + 1).choose i
<VAR>R : Type u_1<VAR>m : ℕ<VAR>this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i<GOAL>m + 1 ≤ 2 * m + 1 + 1
<VAR>R : Type u_1<VAR>m : ℕ<VAR>this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i<GOAL>2 ^ (2 * m + 1) = 2 * 4 ^ m
<VAR>R : Type u_1<VAR>m : ℕ<VAR>this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i<GOAL>2 * (2 ^ 2) ^ m = 2 * 4 ^ m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r✝ : Setoid α<VAR>f✝ f : α → β<VAR>r : Setoid β<VAR>x y : α<GOAL>Setoid.r x y ↔ ⟦f x⟧ = ⟦f y⟧
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r✝ : Setoid α<VAR>f✝ f : α → β<VAR>r : Setoid β<VAR>x y : α<GOAL>Setoid.r x y ↔ f x ≈ f y
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝⁵ : AddCommMonoid M₁<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M₁<VAR>inst✝² : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>M₃ : Type u_7<VAR>inst✝¹ : AddCommMonoid M₃<VAR>inst✝ : Module R M₃<VAR>v₃ : Basis l R M₃<VAR>M : Matrix n n R<VAR>v : M₁<GOAL>v₁.equivFun.symm ((toLinAlgEquiv' M) ⇑(v₁.repr v)) = ∑ j : n, (M *ᵥ ⇑(v₁.repr v)) j • v₁ j
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W✝ : Affine R<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Nonsingular x₁ y₁<VAR>h₂ : W.Nonsingular x₂ y₂<VAR>hx : x₁ = x₂<VAR>hy : y₁ = W.negY x₂ y₂<GOAL>some h₁ + some h₂ = 0
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W✝ : Affine R<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Nonsingular x₁ y₁<VAR>h₂ : W.Nonsingular x₂ y₂<VAR>hx : x₁ = x₂<VAR>hy : y₁ = W.negY x₂ y₂<GOAL>(if h : x₁ = x₂ ∧ y₁ = W.negY x₂ y₂ then 0 else some ⋯) = 0
<VAR>A : Type u_1<VAR>inst✝³ : AddCommGroup A<VAR>inst✝² : Module ℂ A<VAR>inst✝¹ : StarAddMonoid A<VAR>inst✝ : StarModule ℂ A<VAR>x : A<VAR>hx : IsSelfAdjoint x<GOAL>ℑ x = 0
<VAR>b n : ℕ<GOAL>0 < log b n ↔ b ≤ n ∧ 1 < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>s : Set α<VAR>a b : α<VAR>h : a < b<GOAL>frontier (Ioo a b) = {a, b}
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<GOAL>Disjoint I (hC.diffFinset₀ hs hI)
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<VAR>h : ¬Disjoint I (hC.diffFinset₀ hs hI)<GOAL>False
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<VAR>h : ∃ a ∈ I, a ∈ hC.diffFinset₀ hs hI<GOAL>False
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<VAR>u : Set α<VAR>huI : u ∈ I<VAR>hu_diffFinset₀ : u ∈ hC.diffFinset₀ hs hI<GOAL>False
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<VAR>u : Set α<VAR>huI : u ∈ I<VAR>hu_diffFinset₀ : u ∈ hC.diffFinset₀ hs hI<VAR>h_disj : u ≤ ⊥<GOAL>False
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<VAR>u : Set α<VAR>huI : u ∈ I<VAR>hu_diffFinset₀ : u ∈ hC.diffFinset₀ hs hI<VAR>h_disj : u = ∅<GOAL>False
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<VAR>u : Set α<VAR>huI : u ∈ I<VAR>hu_diffFinset₀ : u ∈ hC.diffFinset₀ hs hI<VAR>h_disj : u = ∅<GOAL>∅ ∈ hC.diffFinset₀ hs hI
<VAR>X : Type u<VAR>inst✝² : MetricSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : Nonempty X<VAR>p : NonemptyCompacts ↥(lp (fun n => ℝ) ⊤)<GOAL>⟦p⟧ = toGHSpace X ↔ ∃ Ψ, Isometry Ψ ∧ range Ψ = ↑p
<VAR>X : Type u<VAR>inst✝² : MetricSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : Nonempty X<VAR>p : NonemptyCompacts ↥(lp (fun n => ℝ) ⊤)<GOAL>p ≈ NonemptyCompacts.kuratowskiEmbedding X ↔ ∃ Ψ, Isometry Ψ ∧ range Ψ = ↑p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g g' : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : LinearOrderedField β<VAR>inst✝ : OrderTopology β<VAR>hk : Tendsto k l atTop<VAR>n : ℕ<GOAL>SuperpolynomialDecay l k (f * k ^ n) ↔ SuperpolynomialDecay l k f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderClosedTopology β<VAR>inst✝¹ : Nonempty γ<VAR>ι : Sort u_4<VAR>inst✝ : Nonempty ι<VAR>f : α → β<VAR>g : ι → α<VAR>Cf : ContinuousAt f (iInf g)<VAR>Mf : Monotone f<VAR>bdd : autoParam (BddBelow (range g)) _auto✝<GOAL>f (⨅ i, g i) = ⨅ i, f (g i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderClosedTopology β<VAR>inst✝¹ : Nonempty γ<VAR>ι : Sort u_4<VAR>inst✝ : Nonempty ι<VAR>f : α → β<VAR>g : ι → α<VAR>Cf : ContinuousAt f (iInf g)<VAR>Mf : Monotone f<VAR>bdd : autoParam (BddBelow (range g)) _auto✝<GOAL>sInf (range (f ∘ g)) = sInf (range fun i => f (g i))
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s t : Finset α<VAR>P : Finpartition univ<VAR>ε : ℝ<VAR>hε : ε ≤ 0<GOAL>triangleRemovalBound ε ≤ 0
<VAR>y z : ℝ<VAR>f : ℝ → ℝ≥0∞<VAR>hzy : z ≤ y<GOAL>∫⁻ (x : ℝ) in Iic y, f x = (∫⁻ (x : ℝ) in Iio z, f x) + ∫⁻ (x : ℝ) in Icc z y, f x
<VAR>y z : ℝ<VAR>f : ℝ → ℝ≥0∞<VAR>hzy : z ≤ y<GOAL>Disjoint (Iio z) (Icc z y)
<VAR>y z : ℝ<VAR>f : ℝ → ℝ≥0∞<VAR>hzy : z ≤ y<GOAL>Iio z ∩ Icc z y ⊆ ∅
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℝ<VAR>ha : 0 < a<GOAL>∑' (n : ℤ), rexp (-π * a * ↑n ^ 2) = 1 / a ^ (1 / 2) * ∑' (n : ℤ), rexp (-π / a * ↑n ^ 2)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X Y : ModuleCat R<VAR>f : X ⟶ Y<VAR>Z : ModuleCat R<GOAL>f ▷ Z ≫ (Y.braiding Z).hom = (X.braiding Z).hom ≫ Z ◁ f
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X Y : ModuleCat R<VAR>f : X ⟶ Y<VAR>Z : ModuleCat R<GOAL>f ▷ Z ≫ (Y.braiding Z).hom = (X.braiding Z).hom ≫ (𝟙 Z ⊗ f)
<VAR>n : ℕ<GOAL>antidiagonal n = map { toFun := fun i => (n - i, i), inj' := ⋯ } (range (n + 1))