ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>inst✝¹⁵ : Group G<VAR>inst✝¹⁴ : MeasurableSpace G<VAR>inst✝¹³ : TopologicalSpace G<VAR>inst✝¹² : TopologicalGroup G<VAR>inst✝¹¹ : BorelSpace G<VAR>inst✝¹⁰ : PolishSpace G<VAR>Γ : Subgroup G<VAR>inst✝⁹ : Countable ↥Γ<VAR>inst✝⁸ : Γ.Normal<VAR>inst✝⁷ : T2Space (G ⧸ Γ)<VAR>inst✝⁶ : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝⁵ : SigmaFinite ν<VAR>inst✝⁴ : ν.IsHaarMeasure<VAR>inst✝³ : ν.IsMulRightInvariant<VAR>inst✝² : LocallyCompactSpace G<VAR>inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ<VAR>i : HasFundamentalDomain (↥Γ.op) G ν<VAR>inst✝ : IsFiniteMeasure μ<VAR>K : PositiveCompacts G<GOAL>μ.IsHaarMeasure
<VAR>G : Type u_1<VAR>inst✝¹⁵ : Group G<VAR>inst✝¹⁴ : MeasurableSpace G<VAR>inst✝¹³ : TopologicalSpace G<VAR>inst✝¹² : TopologicalGroup G<VAR>inst✝¹¹ : BorelSpace G<VAR>inst✝¹⁰ : PolishSpace G<VAR>Γ : Subgroup G<VAR>inst✝⁹ : Countable ↥Γ<VAR>inst✝⁸ : Γ.Normal<VAR>inst✝⁷ : T2Space (G ⧸ Γ)<VAR>inst✝⁶ : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝⁵ : SigmaFinite ν<VAR>inst✝⁴ : ν.IsHaarMeasure<VAR>inst✝³ : ν.IsMulRightInvariant<VAR>inst✝² : LocallyCompactSpace G<VAR>inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ<VAR>i : HasFundamentalDomain (↥Γ.op) G ν<VAR>inst✝ : IsFiniteMeasure μ<VAR>K : PositiveCompacts G<VAR>K' : PositiveCompacts (G ⧸ Γ) := PositiveCompacts.map QuotientGroup.mk ⋯ ⋯ K<GOAL>μ.IsHaarMeasure
<VAR>G : Type u_1<VAR>inst✝¹⁵ : Group G<VAR>inst✝¹⁴ : MeasurableSpace G<VAR>inst✝¹³ : TopologicalSpace G<VAR>inst✝¹² : TopologicalGroup G<VAR>inst✝¹¹ : BorelSpace G<VAR>inst✝¹⁰ : PolishSpace G<VAR>Γ : Subgroup G<VAR>inst✝⁹ : Countable ↥Γ<VAR>inst✝⁸ : Γ.Normal<VAR>inst✝⁷ : T2Space (G ⧸ Γ)<VAR>inst✝⁶ : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝⁵ : SigmaFinite ν<VAR>inst✝⁴ : ν.IsHaarMeasure<VAR>inst✝³ : ν.IsMulRightInvariant<VAR>inst✝² : LocallyCompactSpace G<VAR>inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ<VAR>i : HasFundamentalDomain (↥Γ.op) G ν<VAR>inst✝ : IsFiniteMeasure μ<VAR>K : PositiveCompacts G<VAR>K' : PositiveCompacts (G ⧸ Γ) := PositiveCompacts.map QuotientGroup.mk ⋯ ⋯ K<VAR>this : μ.IsMulLeftInvariant<GOAL>μ.IsHaarMeasure
<VAR>G : Type u_1<VAR>inst✝¹⁵ : Group G<VAR>inst✝¹⁴ : MeasurableSpace G<VAR>inst✝¹³ : TopologicalSpace G<VAR>inst✝¹² : TopologicalGroup G<VAR>inst✝¹¹ : BorelSpace G<VAR>inst✝¹⁰ : PolishSpace G<VAR>Γ : Subgroup G<VAR>inst✝⁹ : Countable ↥Γ<VAR>inst✝⁸ : Γ.Normal<VAR>inst✝⁷ : T2Space (G ⧸ Γ)<VAR>inst✝⁶ : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝⁵ : SigmaFinite ν<VAR>inst✝⁴ : ν.IsHaarMeasure<VAR>inst✝³ : ν.IsMulRightInvariant<VAR>inst✝² : LocallyCompactSpace G<VAR>inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ<VAR>i : HasFundamentalDomain (↥Γ.op) G ν<VAR>inst✝ : IsFiniteMeasure μ<VAR>K : PositiveCompacts G<VAR>K' : PositiveCompacts (G ⧸ Γ) := PositiveCompacts.map QuotientGroup.mk ⋯ ⋯ K<VAR>this : μ.IsMulLeftInvariant<GOAL>(μ ↑K' • haarMeasure K').IsHaarMeasure
<VAR>G : Type u_1<VAR>inst✝¹⁵ : Group G<VAR>inst✝¹⁴ : MeasurableSpace G<VAR>inst✝¹³ : TopologicalSpace G<VAR>inst✝¹² : TopologicalGroup G<VAR>inst✝¹¹ : BorelSpace G<VAR>inst✝¹⁰ : PolishSpace G<VAR>Γ : Subgroup G<VAR>inst✝⁹ : Countable ↥Γ<VAR>inst✝⁸ : Γ.Normal<VAR>inst✝⁷ : T2Space (G ⧸ Γ)<VAR>inst✝⁶ : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝⁵ : SigmaFinite ν<VAR>inst✝⁴ : ν.IsHaarMeasure<VAR>inst✝³ : ν.IsMulRightInvariant<VAR>inst✝² : LocallyCompactSpace G<VAR>inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ<VAR>i : HasFundamentalDomain (↥Γ.op) G ν<VAR>inst✝ : IsFiniteMeasure μ<VAR>K : PositiveCompacts G<VAR>K' : PositiveCompacts (G ⧸ Γ) := PositiveCompacts.map QuotientGroup.mk ⋯ ⋯ K<VAR>this : μ.IsMulLeftInvariant<VAR>finiteCovol : covolume (↥Γ.op) G ν ≠ ⊤<GOAL>(μ ↑K' • haarMeasure K').IsHaarMeasure
<VAR>G : Type u_1<VAR>inst✝¹⁵ : Group G<VAR>inst✝¹⁴ : MeasurableSpace G<VAR>inst✝¹³ : TopologicalSpace G<VAR>inst✝¹² : TopologicalGroup G<VAR>inst✝¹¹ : BorelSpace G<VAR>inst✝¹⁰ : PolishSpace G<VAR>Γ : Subgroup G<VAR>inst✝⁹ : Countable ↥Γ<VAR>inst✝⁸ : Γ.Normal<VAR>inst✝⁷ : T2Space (G ⧸ Γ)<VAR>inst✝⁶ : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝⁵ : SigmaFinite ν<VAR>inst✝⁴ : ν.IsHaarMeasure<VAR>inst✝³ : ν.IsMulRightInvariant<VAR>inst✝² : LocallyCompactSpace G<VAR>inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ<VAR>inst✝ : IsFiniteMeasure μ<VAR>K : PositiveCompacts G<VAR>K' : PositiveCompacts (G ⧸ Γ) := PositiveCompacts.map QuotientGroup.mk ⋯ ⋯ K<VAR>this : μ.IsMulLeftInvariant<VAR>finiteCovol : covolume (↥Γ.op) G ν ≠ ⊤<VAR>s : Set G<VAR>fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν<GOAL>(μ ↑K' • haarMeasure K').IsHaarMeasure
<VAR>G : Type u_1<VAR>inst✝¹⁵ : Group G<VAR>inst✝¹⁴ : MeasurableSpace G<VAR>inst✝¹³ : TopologicalSpace G<VAR>inst✝¹² : TopologicalGroup G<VAR>inst✝¹¹ : BorelSpace G<VAR>inst✝¹⁰ : PolishSpace G<VAR>Γ : Subgroup G<VAR>inst✝⁹ : Countable ↥Γ<VAR>inst✝⁸ : Γ.Normal<VAR>inst✝⁷ : T2Space (G ⧸ Γ)<VAR>inst✝⁶ : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝⁵ : SigmaFinite ν<VAR>inst✝⁴ : ν.IsHaarMeasure<VAR>inst✝³ : ν.IsMulRightInvariant<VAR>inst✝² : LocallyCompactSpace G<VAR>inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ<VAR>inst✝ : IsFiniteMeasure μ<VAR>K : PositiveCompacts G<VAR>K' : PositiveCompacts (G ⧸ Γ) := PositiveCompacts.map QuotientGroup.mk ⋯ ⋯ K<VAR>this : μ.IsMulLeftInvariant<VAR>s : Set G<VAR>finiteCovol : ν s ≠ ⊤<VAR>fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν<GOAL>(μ ↑K' • haarMeasure K').IsHaarMeasure
<VAR>G : Type u_1<VAR>inst✝¹⁵ : Group G<VAR>inst✝¹⁴ : MeasurableSpace G<VAR>inst✝¹³ : TopologicalSpace G<VAR>inst✝¹² : TopologicalGroup G<VAR>inst✝¹¹ : BorelSpace G<VAR>inst✝¹⁰ : PolishSpace G<VAR>Γ : Subgroup G<VAR>inst✝⁹ : Countable ↥Γ<VAR>inst✝⁸ : Γ.Normal<VAR>inst✝⁷ : T2Space (G ⧸ Γ)<VAR>inst✝⁶ : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝⁵ : SigmaFinite ν<VAR>inst✝⁴ : ν.IsHaarMeasure<VAR>inst✝³ : ν.IsMulRightInvariant<VAR>inst✝² : LocallyCompactSpace G<VAR>inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ<VAR>inst✝ : IsFiniteMeasure μ<VAR>K : PositiveCompacts G<VAR>K' : PositiveCompacts (G ⧸ Γ) := PositiveCompacts.map QuotientGroup.mk ⋯ ⋯ K<VAR>this : μ.IsMulLeftInvariant<VAR>s : Set G<VAR>finiteCovol : ν s ≠ ⊤<VAR>fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν<GOAL>(ν (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' ↑K' ∩ s) • haarMeasure K').IsHaarMeasure
<VAR>G : Type u_1<VAR>inst✝¹⁵ : Group G<VAR>inst✝¹⁴ : MeasurableSpace G<VAR>inst✝¹³ : TopologicalSpace G<VAR>inst✝¹² : TopologicalGroup G<VAR>inst✝¹¹ : BorelSpace G<VAR>inst✝¹⁰ : PolishSpace G<VAR>Γ : Subgroup G<VAR>inst✝⁹ : Countable ↥Γ<VAR>inst✝⁸ : Γ.Normal<VAR>inst✝⁷ : T2Space (G ⧸ Γ)<VAR>inst✝⁶ : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝⁵ : SigmaFinite ν<VAR>inst✝⁴ : ν.IsHaarMeasure<VAR>inst✝³ : ν.IsMulRightInvariant<VAR>inst✝² : LocallyCompactSpace G<VAR>inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ<VAR>inst✝ : IsFiniteMeasure μ<VAR>K : PositiveCompacts G<VAR>K' : PositiveCompacts (G ⧸ Γ) := PositiveCompacts.map QuotientGroup.mk ⋯ ⋯ K<VAR>this : μ.IsMulLeftInvariant<VAR>s : Set G<VAR>finiteCovol : ν s ≠ ⊤<VAR>fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν<GOAL>ν (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' ↑K' ∩ s) ≠ 0
<VAR>G : Type u_1<VAR>inst✝¹⁵ : Group G<VAR>inst✝¹⁴ : MeasurableSpace G<VAR>inst✝¹³ : TopologicalSpace G<VAR>inst✝¹² : TopologicalGroup G<VAR>inst✝¹¹ : BorelSpace G<VAR>inst✝¹⁰ : PolishSpace G<VAR>Γ : Subgroup G<VAR>inst✝⁹ : Countable ↥Γ<VAR>inst✝⁸ : Γ.Normal<VAR>inst✝⁷ : T2Space (G ⧸ Γ)<VAR>inst✝⁶ : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝⁵ : SigmaFinite ν<VAR>inst✝⁴ : ν.IsHaarMeasure<VAR>inst✝³ : ν.IsMulRightInvariant<VAR>inst✝² : LocallyCompactSpace G<VAR>inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ<VAR>inst✝ : IsFiniteMeasure μ<VAR>K : PositiveCompacts G<VAR>K' : PositiveCompacts (G ⧸ Γ) := PositiveCompacts.map QuotientGroup.mk ⋯ ⋯ K<VAR>this : μ.IsMulLeftInvariant<VAR>s : Set G<VAR>finiteCovol : ν s ≠ ⊤<VAR>fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν<GOAL>ν (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' ↑K' ∩ s) ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>h : s ⊆ t<VAR>ht : autoParam t.Finite _auto✝<GOAL>(t \ s).ncard + s.ncard = t.ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>h : s ⊆ t<VAR>ht : autoParam t.Finite _auto✝<GOAL>↑(t \ s).ncard + ↑s.ncard = ↑t.ncard
<VAR>R : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁶ : CommRing P<VAR>inst✝⁵ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝⁴ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R₁ K<VAR>inst✝¹ : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>I : FractionalIdeal S P<GOAL>↑I.num ≤ I
<VAR>R : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁶ : CommRing P<VAR>inst✝⁵ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝⁴ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R₁ K<VAR>inst✝¹ : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>I : FractionalIdeal S P<GOAL>∀ z ∈ I, (algebraMap R P) ↑I.den * z ∈ I
<VAR>R : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁶ : CommRing P<VAR>inst✝⁵ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝⁴ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R₁ K<VAR>inst✝¹ : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>I : FractionalIdeal S P<VAR>z✝ : P<VAR>h : z✝ ∈ I<GOAL>(algebraMap R P) ↑I.den * z✝ ∈ I
<VAR>R : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁶ : CommRing P<VAR>inst✝⁵ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝⁴ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R₁ K<VAR>inst✝¹ : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>I : FractionalIdeal S P<VAR>z✝ : P<VAR>h : z✝ ∈ I<GOAL>↑I.den • z✝ ∈ I
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Category.{v₂, u₂} D<VAR>L₁ L₂ L₃ : C ⥤ D<VAR>R₁ R₂ R₃ : D ⥤ C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>α : R₁ ⟶ R₂<VAR>β : R₂ ⟶ R₁<VAR>αβ : α ≫ β = 𝟙 R₁<GOAL>(conjugateEquiv adj₂ adj₁).symm β ≫ (conjugateEquiv adj₁ adj₂).symm α = 𝟙 L₁
<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_5, u_2} D<VAR>inst✝² : Category.{?u.126128, u_3} E<VAR>F : Cᵒᵖ ⥤ D<VAR>inst✝¹ : Preregular C<VAR>inst✝ : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f<GOAL>EqualizerCondition F ↔ Presheaf.IsSheaf (Coverage.toGrothendieck C (regularCoverage C)) F
<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_5, u_2} D<VAR>inst✝² : Category.{?u.126128, u_3} E<VAR>F : Cᵒᵖ ⥤ D<VAR>inst✝¹ : Preregular C<VAR>inst✝ : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f<GOAL>EqualizerCondition F ↔ ∀ ⦃X : C⦄, ∀ R ∈ (regularCoverage C).covering X, Nonempty (IsLimit (F.mapCone (Sieve.generate R).arrows.cocone.op))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m✝ m0 : MeasurableSpace α<VAR>E : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>f : α →ₛ ℝ≥0<VAR>L : ℝ≥0∞<VAR>hL : L < ∫⁻ (x : α), ↑(↑f x) ∂μ<GOAL>∃ g, (∀ (x : α), ↑g x ≤ ↑f x) ∧ ∫⁻ (x : α), ↑(↑g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m✝ m0 : MeasurableSpace α<VAR>E : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>c : ℝ≥0<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>L : ℝ≥0∞<VAR>hL : L < ∫⁻ (x : α), ↑(↑(piecewise s hs (const α c) (const α 0)) x) ∂μ<GOAL>∃ g, (∀ (x : α), ↑g x ≤ ↑(piecewise s hs (const α c) (const α 0)) x) ∧ ∫⁻ (x : α), ↑(↑g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m✝ m0 : MeasurableSpace α<VAR>E : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>f₁ f₂ : α →ₛ ℝ≥0<VAR>a✝ : Disjoint (support ↑f₁) (support ↑f₂)<VAR>h₁ : ∀ {L : ℝ≥0∞}, L < ∫⁻ (x : α), ↑(↑f₁ x) ∂μ → ∃ g, (∀ (x : α), ↑g x ≤ ↑f₁ x) ∧ ∫⁻ (x : α), ↑(↑g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ<VAR>h₂ : ∀ {L : ℝ≥0∞}, L < ∫⁻ (x : α), ↑(↑f₂ x) ∂μ → ∃ g, (∀ (x : α), ↑g x ≤ ↑f₂ x) ∧ ∫⁻ (x : α), ↑(↑g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ<VAR>L : ℝ≥0∞<VAR>hL : L < ∫⁻ (x : α), ↑(↑(f₁ + f₂) x) ∂μ<GOAL>∃ g, (∀ (x : α), ↑g x ≤ ↑(f₁ + f₂) x) ∧ ∫⁻ (x : α), ↑(↑g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>κ : Type u_1<VAR>inst✝² : Monoid γ<VAR>inst✝¹ : (i : ι) → AddMonoid (β i)<VAR>inst✝ : (i : ι) → DistribMulAction γ (β i)<VAR>h : κ → ι<VAR>hh : Function.Injective h<VAR>r : γ<VAR>f : Π₀ (i : ι), β i<VAR>i✝ : κ<GOAL>(comapDomain h hh (r • f)) i✝ = (r • comapDomain h hh f) i✝
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : angle x (x - y) = angle y (y - x)<VAR>hpi : angle x y ≠ π<GOAL>‖x‖ = ‖y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>hpi : angle x y ≠ π<VAR>h : ⟪x, x - y⟫_ℝ / (‖x‖ * ‖x - y‖) = ⟪y, y - x⟫_ℝ / (‖y‖ * ‖y - x‖)<GOAL>‖x‖ = ‖y‖
<VAR>o a : ONote<VAR>h : o.fundamentalSequence = Sum.inl (some a)<GOAL>o.fastGrowing = fun i => a.fastGrowing^[i] i
<VAR>α : Type u<VAR>a : α<VAR>s t : Set α<VAR>x : Prop<GOAL>x ∈ {True, False}
<VAR>α : Type u<VAR>a : α<VAR>s t : Set α<VAR>x : Prop<GOAL>x = True ∨ x = False
<VAR>C : Type u_1<VAR>inst✝⁸ : Category.{u_4, u_1} C<VAR>inst✝⁷ : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝⁶ : HasHomotopyCofiber φ<VAR>inst✝⁵ : DecidableRel c.Rel<VAR>inst✝⁴ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)<VAR>inst✝³ : HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K))<VAR>φ₀ φ₁ : F ⟶ G<VAR>h : Homotopy φ₀ φ₁<VAR>hc : ∀ (j : ι), ∃ i, c.Rel i j<VAR>inst✝² : ∀ (i : ι), HasBinaryBiproduct (F.X i) (F.X i)<VAR>inst✝¹ : HasHomotopyCofiber (biprod.lift (𝟙 F) (-𝟙 F))<VAR>D : Type u_3<VAR>inst✝ : Category.{u_5, u_3} D<VAR>H : HomologicalComplex C c ⥤ D<VAR>hH : (homotopyEquivalences C c).IsInvertedBy H<GOAL>H.map φ₀ = H.map φ₁
<VAR>l : List ℕ<VAR>a m n : ℕ<VAR>h : n.greatestFib = 0<GOAL>n = 0
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → R<VAR>h : ¬P ≈ Q<VAR>u v : R<VAR>hu : IsUnit u<VAR>hv : IsUnit v<GOAL>W'.add (u • P) (v • Q) = (u * v) ^ 2 • W'.add P Q
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → R<VAR>h : ¬P ≈ Q<VAR>u v : R<VAR>hu : IsUnit u<VAR>hv : IsUnit v<VAR>smul : P ≈ Q ↔ u • P ≈ v • Q<GOAL>W'.add (u • P) (v • Q) = (u * v) ^ 2 • W'.add P Q
<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>t : Triangle ℝ P<VAR>i : Fin 3<GOAL>affineSpan ℝ {t.orthocenter, t.points i} ≤ altitude t i
<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>t : Triangle ℝ P<VAR>i : Fin 3<GOAL>{t.orthocenter, t.points i} ⊆ ↑(altitude t i)
<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>t : Triangle ℝ P<VAR>i : Fin 3<GOAL>t.orthocenter ∈ ↑(altitude t i) ∧ t.points i ∈ ↑(altitude t i)
<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>u✝ v✝ w u v : V<VAR>p : G.Walk u v<VAR>h : p.IsTrail<GOAL>p.reverse.IsTrail
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>V3 : Type u_6<VAR>P3 : Type u_7<VAR>V4 : Type u_8<VAR>P4 : Type u_9<VAR>inst✝¹³ : Ring k<VAR>inst✝¹² : AddCommGroup V1<VAR>inst✝¹¹ : Module k V1<VAR>inst✝¹⁰ : AffineSpace V1 P1<VAR>inst✝⁹ : AddCommGroup V2<VAR>inst✝⁸ : Module k V2<VAR>inst✝⁷ : AffineSpace V2 P2<VAR>inst✝⁶ : AddCommGroup V3<VAR>inst✝⁵ : Module k V3<VAR>inst✝⁴ : AffineSpace V3 P3<VAR>inst✝³ : AddCommGroup V4<VAR>inst✝² : Module k V4<VAR>inst✝¹ : AffineSpace V4 P4<VAR>inst✝ : NoZeroSMulDivisors k V1<VAR>p₀ p₁ : P1<VAR>c : k<GOAL>(lineMap p₀ p₁) c = p₀ ↔ p₀ = p₁ ∨ c = 0
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>f : End R M<VAR>hfn : IsNilpotent f<VAR>μ : R<VAR>hf : f.HasEigenvalue μ<GOAL>IsNilpotent μ
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>f : End R M<VAR>hfn : IsNilpotent f<VAR>μ : R<VAR>hf : f.HasEigenvalue μ<VAR>m : M<VAR>hm : f.HasEigenvector μ m<GOAL>IsNilpotent μ
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>f : End R M<VAR>μ : R<VAR>hf : f.HasEigenvalue μ<VAR>m : M<VAR>hm : f.HasEigenvector μ m<VAR>n : ℕ<VAR>hn : f ^ n = 0<GOAL>IsNilpotent μ
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝² : SemilatticeSup α<VAR>inst✝¹ : OrderBot α<VAR>s✝ s₁ s₂ : Finset β<VAR>f g : β → α<VAR>a : α<VAR>inst✝ : DecidableEq β<VAR>s : Finset γ<VAR>t : γ → Finset β<VAR>c : α<GOAL>(s.biUnion t).sup f ≤ c ↔ (s.sup fun x => (t x).sup f) ≤ c
<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>h : p.degree = q.degree<VAR>hlc : p.leadingCoeff + q.leadingCoeff ≠ 0<GOAL>(p + q).leadingCoeff = p.leadingCoeff + q.leadingCoeff
<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>h : p.degree = q.degree<VAR>hlc : p.leadingCoeff + q.leadingCoeff ≠ 0<VAR>this : (p + q).natDegree = p.natDegree<GOAL>(p + q).leadingCoeff = p.leadingCoeff + q.leadingCoeff
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>yonedaEquiv (yoneda.map f) = f
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(yoneda.map f).app (op X) (𝟙 X) = f
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I B X : Set α<VAR>hB : autoParam (B ⊆ M.E) _auto✝<GOAL>M✶.Base B ↔ M.Base (M.E \ B)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I B X : Set α<VAR>hB : autoParam (B ⊆ M.E) _auto✝<GOAL>((B ⊆ M.E ∧ ∃ B_1, M.Base B_1 ∧ Disjoint B B_1) ∧ ∀ (I : Set α), M✶.Indep I → B ⊆ I → B = I) ↔ (B ⊆ M.E ∧ ∃ B_1, M.Base B_1 ∧ Disjoint B B_1) ∧ ∀ ⦃y : Set α⦄, (y ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint y B) → B ⊆ y → B = y
<VAR>x✝ y x : ℝ<GOAL>1 < rexp x ↔ 0 < x
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>z1 z2 : ℤ_[p]<GOAL>‖z1 * z2‖ = ‖z1‖ * ‖z2‖
<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✝ x y : E<GOAL>(convexHull 𝕜) {x, y} = segment 𝕜 x y
<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✝ x y : E<GOAL>{x, y} ⊆ segment 𝕜 x y
<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✝ x y : E<GOAL>x ∈ segment 𝕜 x y ∧ y ∈ segment 𝕜 x y
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : Semiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module Rᵐᵒᵖ M<VAR>r : R<VAR>x : tsze R M<GOAL>r •> x.snd + 0 <• x.fst = r •> x.snd
<VAR>z w : ℂ<GOAL>((abs z + w) * abs z + w) ≤ ((abs z) + abs w) * ((abs z) + abs w)
<VAR>z w : ℂ<GOAL>(z * (starRingEnd ℂ) w).re ≤ abs z * (starRingEnd ℂ) w
<VAR>x : ℝ<GOAL>cos (x + π / 2) = -sin x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝⁷ : Preorder α<VAR>inst✝⁶ : Preorder β<VAR>inst✝⁵ : Preorder γ<VAR>inst✝⁴ : Preorder δ<VAR>inst✝³ : MulOneClass α<VAR>inst✝² : MulOneClass β<VAR>inst✝¹ : MulOneClass γ<VAR>inst✝ : MulOneClass δ<VAR>f✝ g✝ f g : α →*o β<VAR>h : f.toOrderHom = g.toOrderHom<GOAL>∀ (a : α), f a = g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t✝ u✝ : Set α<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>s t u : Set α<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>h : univ ⊆ s ∪ t<VAR>hsu : MeasurableSet (Subtype.val ⁻¹' u)<VAR>htu : MeasurableSet (Subtype.val ⁻¹' u)<GOAL>MeasurableSet u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t✝ u✝ : Set α<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>s t u : Set α<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>h : univ ⊆ s ∪ t<VAR>hsu : MeasurableSet (Subtype.val ⁻¹' u)<VAR>htu : MeasurableSet (Subtype.val ⁻¹' u)<GOAL>u = Subtype.val '' (Subtype.val ⁻¹' u) ∪ Subtype.val '' (Subtype.val ⁻¹' u)
<VAR>A : 0 < 3 / 2<GOAL>Gamma (3 / 2) < 1
<VAR>A : 0 < 3 / 2<VAR>this : (log ∘ Gamma) (↑2 + 1 / 2) ≤ (log ∘ Gamma) ↑2 + 1 / 2 * log ↑2<GOAL>Gamma (3 / 2) < 1
<VAR>A : 0 < 3 / 2<VAR>y : ℝ<VAR>hy : 0 < y<GOAL>(log ∘ Gamma) (y + 1) = (log ∘ Gamma) y + log y
<VAR>A : 0 < 3 / 2<VAR>this : Gamma (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))<GOAL>Gamma (3 / 2) < 1
<VAR>A : 0 < 3 / 2<VAR>this : Gamma (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))<GOAL>1 / 2 * log 2 - log (3 / 2) < 0
<VAR>A : 0 < 3 / 2<VAR>this : Gamma (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))<GOAL>(log 2 * 1 - 2 * log (3 / 2)) / 2 < 0
<VAR>A : 0 < 3 / 2<VAR>this : Gamma (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))<GOAL>log 2 * 1 - 2 * log (3 / 2) < 0
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>m : α → EReal<VAR>f : Filter α<GOAL>(∀ (i : ℝ), True → ∀ᶠ (x : α) in f, m x ∈ Ioi ↑i) ↔ ∀ (x : ℝ), ∀ᶠ (a : α) in f, ↑x < m a
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : Preorder β<VAR>inst✝ : Preorder γ<VAR>f : α → β<VAR>e : β → γ<VAR>l : Filter α<VAR>hm : ∀ (b₁ b₂ : β), e b₁ ≤ e b₂ ↔ b₁ ≤ b₂<VAR>hu : ∀ (c : γ), ∃ b, c ≤ e b<GOAL>Tendsto (e ∘ f) l atTop ↔ Tendsto f l atTop
<VAR>x y : ℝ<VAR>hx : 0 < x<GOAL>log x < y ↔ x < rexp y
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>x₁ x₂ y₁ y₂ : X<VAR>hsat₁ : IsMaximal (last s) x₁<VAR>hsat₂ : IsMaximal (last s) x₂<VAR>hsaty₁ : IsMaximal (snoc s x₁ hsat₁).last y₁<VAR>hsaty₂ : IsMaximal (snoc s x₂ hsat₂).last y₂<VAR>hr₁ : Iso (last s, x₁) (x₂, y₂)<VAR>hr₂ : Iso (x₁, y₁) (last s, x₂)<VAR>e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) := Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc<VAR>x✝ : Fin s.length<GOAL>x✝.castSucc.castSucc < (Fin.last s.length).castSucc