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✝⁴ : ν.IsMulLeftInvariant<VAR>inst✝³ : ν.IsMulRightInvariant<VAR>inst✝² : SigmaFinite ν<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : SigmaFinite μ<VAR>s : Set G<VAR>fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν<VAR>V : Set (G ⧸ Γ)<VAR>meas_V : MeasurableSet V<VAR>neZeroV : μ V ≠ 0<VAR>hV : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ s)<VAR>neTopV : μ V ≠ ⊤<VAR>U : Set (G ⧸ Γ)<VAR>a✝ : MeasurableSet U<GOAL>μ U = (map (Quotient.mk (MulAction.orbitRel (↥Γ.op) G)) (ν.restrict s)) U
<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✝⁴ : ν.IsMulLeftInvariant<VAR>inst✝³ : ν.IsMulRightInvariant<VAR>inst✝² : SigmaFinite ν<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : SigmaFinite μ<VAR>s : Set G<VAR>fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν<VAR>V : Set (G ⧸ Γ)<VAR>meas_V : MeasurableSet V<VAR>neZeroV : μ V ≠ 0<VAR>hV : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ s)<VAR>neTopV : μ V ≠ ⊤<VAR>U : Set (G ⧸ Γ)<VAR>a✝ : MeasurableSet U<VAR>meas_π : Measurable QuotientGroup.mk<GOAL>μ U = (map (Quotient.mk (MulAction.orbitRel (↥Γ.op) G)) (ν.restrict s)) U
<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✝⁴ : ν.IsMulLeftInvariant<VAR>inst✝³ : ν.IsMulRightInvariant<VAR>inst✝² : SigmaFinite ν<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : SigmaFinite μ<VAR>s : Set G<VAR>fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν<VAR>V : Set (G ⧸ Γ)<VAR>meas_V : MeasurableSet V<VAR>neZeroV : μ V ≠ 0<VAR>hV : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ s)<VAR>neTopV : μ V ≠ ⊤<VAR>U : Set (G ⧸ Γ)<VAR>a✝ : MeasurableSet U<VAR>meas_π : Measurable QuotientGroup.mk<VAR>μ' : Measure (G ⧸ Γ) := map QuotientGroup.mk (ν.restrict s)<VAR>has_fund : HasFundamentalDomain (↥Γ.op) G ν<GOAL>μ U = (map (Quotient.mk (MulAction.orbitRel (↥Γ.op) G)) (ν.restrict s)) U
<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✝⁴ : ν.IsMulLeftInvariant<VAR>inst✝³ : ν.IsMulRightInvariant<VAR>inst✝² : SigmaFinite ν<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : SigmaFinite μ<VAR>s : Set G<VAR>fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν<VAR>V : Set (G ⧸ Γ)<VAR>meas_V : MeasurableSet V<VAR>neZeroV : μ V ≠ 0<VAR>hV : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ s)<VAR>neTopV : μ V ≠ ⊤<VAR>U : Set (G ⧸ Γ)<VAR>a✝ : MeasurableSet U<VAR>meas_π : Measurable QuotientGroup.mk<VAR>μ' : Measure (G ⧸ Γ) := map QuotientGroup.mk (ν.restrict s)<VAR>has_fund : HasFundamentalDomain (↥Γ.op) G ν<VAR>i : QuotientMeasureEqMeasurePreimage ν μ'<GOAL>μ U = (map (Quotient.mk (MulAction.orbitRel (↥Γ.op) G)) (ν.restrict s)) U
<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✝⁴ : ν.IsMulLeftInvariant<VAR>inst✝³ : ν.IsMulRightInvariant<VAR>inst✝² : SigmaFinite ν<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : SigmaFinite μ<VAR>s : Set G<VAR>fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν<VAR>V : Set (G ⧸ Γ)<VAR>meas_V : MeasurableSet V<VAR>neZeroV : μ V ≠ 0<VAR>hV : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ s)<VAR>neTopV : μ V ≠ ⊤<VAR>U : Set (G ⧸ Γ)<VAR>a✝ : MeasurableSet U<VAR>meas_π : Measurable QuotientGroup.mk<VAR>μ' : Measure (G ⧸ Γ) := map QuotientGroup.mk (ν.restrict s)<VAR>has_fund : HasFundamentalDomain (↥Γ.op) G ν<VAR>i : QuotientMeasureEqMeasurePreimage ν μ'<VAR>this : μ'.IsMulLeftInvariant<GOAL>μ U = (map (Quotient.mk (MulAction.orbitRel (↥Γ.op) G)) (ν.restrict s)) U
<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✝⁴ : ν.IsMulLeftInvariant<VAR>inst✝³ : ν.IsMulRightInvariant<VAR>inst✝² : SigmaFinite ν<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : SigmaFinite μ<VAR>s : Set G<VAR>fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν<VAR>V : Set (G ⧸ Γ)<VAR>meas_V : MeasurableSet V<VAR>neZeroV : μ V ≠ 0<VAR>hV : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ s)<VAR>neTopV : μ V ≠ ⊤<VAR>U : Set (G ⧸ Γ)<VAR>a✝ : MeasurableSet U<VAR>meas_π : Measurable QuotientGroup.mk<VAR>μ' : Measure (G ⧸ Γ) := map QuotientGroup.mk (ν.restrict s)<VAR>has_fund : HasFundamentalDomain (↥Γ.op) G ν<VAR>i : QuotientMeasureEqMeasurePreimage ν μ'<VAR>this : μ'.IsMulLeftInvariant<GOAL>μ = μ'
<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✝⁴ : ν.IsMulLeftInvariant<VAR>inst✝³ : ν.IsMulRightInvariant<VAR>inst✝² : SigmaFinite ν<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : SigmaFinite μ<VAR>s : Set G<VAR>fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν<VAR>V : Set (G ⧸ Γ)<VAR>meas_V : MeasurableSet V<VAR>neZeroV : μ V ≠ 0<VAR>hV : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ s)<VAR>neTopV : μ V ≠ ⊤<VAR>U : Set (G ⧸ Γ)<VAR>a✝ : MeasurableSet U<VAR>meas_π : Measurable QuotientGroup.mk<VAR>μ' : Measure (G ⧸ Γ) := map QuotientGroup.mk (ν.restrict s)<VAR>has_fund : HasFundamentalDomain (↥Γ.op) G ν<VAR>i : QuotientMeasureEqMeasurePreimage ν μ'<VAR>this✝ : μ'.IsMulLeftInvariant<VAR>this : SigmaFinite μ'<GOAL>μ = μ'
<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✝⁴ : ν.IsMulLeftInvariant<VAR>inst✝³ : ν.IsMulRightInvariant<VAR>inst✝² : SigmaFinite ν<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : SigmaFinite μ<VAR>s : Set G<VAR>fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν<VAR>V : Set (G ⧸ Γ)<VAR>meas_V : MeasurableSet V<VAR>neZeroV : μ V ≠ 0<VAR>hV : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ s)<VAR>neTopV : μ V ≠ ⊤<VAR>U : Set (G ⧸ Γ)<VAR>a✝ : MeasurableSet U<VAR>meas_π : Measurable QuotientGroup.mk<VAR>μ' : Measure (G ⧸ Γ) := map QuotientGroup.mk (ν.restrict s)<VAR>has_fund : HasFundamentalDomain (↥Γ.op) G ν<VAR>i : QuotientMeasureEqMeasurePreimage ν μ'<VAR>this✝ : μ'.IsMulLeftInvariant<VAR>this : SigmaFinite μ'<GOAL>μ = (μ' V / ν (QuotientGroup.mk ⁻¹' V ∩ s)) • μ
<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✝⁴ : ν.IsMulLeftInvariant<VAR>inst✝³ : ν.IsMulRightInvariant<VAR>inst✝² : SigmaFinite ν<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : SigmaFinite μ<VAR>s : Set G<VAR>fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν<VAR>V : Set (G ⧸ Γ)<VAR>meas_V : MeasurableSet V<VAR>neZeroV : μ V ≠ 0<VAR>hV : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ s)<VAR>neTopV : μ V ≠ ⊤<VAR>U : Set (G ⧸ Γ)<VAR>a✝ : MeasurableSet U<VAR>meas_π : Measurable QuotientGroup.mk<VAR>μ' : Measure (G ⧸ Γ) := map QuotientGroup.mk (ν.restrict s)<VAR>has_fund : HasFundamentalDomain (↥Γ.op) G ν<VAR>i : QuotientMeasureEqMeasurePreimage ν μ'<VAR>this✝ : μ'.IsMulLeftInvariant<VAR>this : SigmaFinite μ'<GOAL>(μ' V / ν (QuotientGroup.mk ⁻¹' V ∩ s)) • μ = μ
<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✝⁴ : ν.IsMulLeftInvariant<VAR>inst✝³ : ν.IsMulRightInvariant<VAR>inst✝² : SigmaFinite ν<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : SigmaFinite μ<VAR>s : Set G<VAR>fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν<VAR>V : Set (G ⧸ Γ)<VAR>meas_V : MeasurableSet V<VAR>neZeroV : μ V ≠ 0<VAR>hV : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ s)<VAR>neTopV : μ V ≠ ⊤<VAR>U : Set (G ⧸ Γ)<VAR>a✝ : MeasurableSet U<VAR>meas_π : Measurable QuotientGroup.mk<VAR>μ' : Measure (G ⧸ Γ) := map QuotientGroup.mk (ν.restrict s)<VAR>has_fund : HasFundamentalDomain (↥Γ.op) G ν<VAR>i : QuotientMeasureEqMeasurePreimage ν μ'<VAR>this✝ : μ'.IsMulLeftInvariant<VAR>this : SigmaFinite μ'<GOAL>μ' V / ν (QuotientGroup.mk ⁻¹' V ∩ s) = 1
<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✝⁴ : ν.IsMulLeftInvariant<VAR>inst✝³ : ν.IsMulRightInvariant<VAR>inst✝² : SigmaFinite ν<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : SigmaFinite μ<VAR>s : Set G<VAR>fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν<VAR>V : Set (G ⧸ Γ)<VAR>meas_V : MeasurableSet V<VAR>neZeroV : μ V ≠ 0<VAR>hV : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ s)<VAR>neTopV : μ V ≠ ⊤<VAR>U : Set (G ⧸ Γ)<VAR>a✝ : MeasurableSet U<VAR>meas_π : Measurable QuotientGroup.mk<VAR>μ' : Measure (G ⧸ Γ) := map QuotientGroup.mk (ν.restrict s)<VAR>has_fund : HasFundamentalDomain (↥Γ.op) G ν<VAR>i : QuotientMeasureEqMeasurePreimage ν μ'<VAR>this✝ : μ'.IsMulLeftInvariant<VAR>this : SigmaFinite μ'<GOAL>ν (QuotientGroup.mk ⁻¹' V ∩ s) / ν (QuotientGroup.mk ⁻¹' V ∩ s) = 1
<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✝⁴ : ν.IsMulLeftInvariant<VAR>inst✝³ : ν.IsMulRightInvariant<VAR>inst✝² : SigmaFinite ν<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : SigmaFinite μ<VAR>s : Set G<VAR>fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν<VAR>V : Set (G ⧸ Γ)<VAR>meas_V : MeasurableSet V<VAR>neZeroV : μ V ≠ 0<VAR>hV : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ s)<VAR>neTopV : μ V ≠ ⊤<VAR>U : Set (G ⧸ Γ)<VAR>a✝ : MeasurableSet U<VAR>meas_π : Measurable QuotientGroup.mk<VAR>μ' : Measure (G ⧸ Γ) := map QuotientGroup.mk (ν.restrict s)<VAR>has_fund : HasFundamentalDomain (↥Γ.op) G ν<VAR>i : QuotientMeasureEqMeasurePreimage ν μ'<VAR>this✝ : μ'.IsMulLeftInvariant<VAR>this : SigmaFinite μ'<GOAL>MeasurableSet (QuotientGroup.mk ⁻¹' V)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>a b : R<VAR>S : Type v<VAR>x✝ y✝ x y : R<GOAL>(mk (span {x})) y = 0 ↔ x ∣ y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f g : End R M<VAR>hn : IsNilpotent f<VAR>hs : f.IsSemisimple<VAR>n : ℕ<VAR>h0 : f ^ n = 0<GOAL>f = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f g : End R M<VAR>hn : IsNilpotent f<VAR>hs : f.IsSemisimple<VAR>n : ℕ<VAR>h0 : f ^ n = 0<GOAL>(aeval f) X = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f g : End R M<VAR>hn : IsNilpotent f<VAR>hs : f.IsSemisimple<VAR>n : ℕ<VAR>h0 : (aeval f) (X ^ n) = 0<GOAL>(aeval f) X = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f g : End R M<VAR>hn : IsNilpotent f<VAR>hs : f.IsSemisimple<VAR>n : ℕ<VAR>h0 : X ^ n ∈ annihilator R[X] (AEval R M f)<GOAL>X ∈ annihilator R[X] (AEval R M f)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>r : α → β → Prop<VAR>p : γ → δ → Prop<VAR>b : Multiset β<GOAL>Rel r 0 b ↔ b = 0
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>r : α → β → Prop<VAR>p : γ → δ → Prop<VAR>b : Multiset β<GOAL>(0 = 0 ∧ b = 0 ∨ ∃ a b_1 as bs, r a b_1 ∧ Rel r as bs ∧ 0 = a ::ₘ as ∧ b = b_1 ::ₘ bs) ↔ b = 0
<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝ : SemilatticeSup α✝<VAR>a b c✝ d : α✝<VAR>α : Type u_1<VAR>A B : SemilatticeSup α<VAR>H : ∀ (x y : α), x ≤ y ↔ x ≤ y<VAR>x y c : α<GOAL>x ⊔ y ≤ c ↔ x ⊔ y ≤ c
<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝ : SemilatticeSup α✝<VAR>a b c✝ d : α✝<VAR>α : Type u_1<VAR>A B : SemilatticeSup α<VAR>H : ∀ (x y : α), x ≤ y ↔ x ≤ y<VAR>x y c : α<GOAL>x ⊔ y ≤ c ↔ x ≤ c ∧ y ≤ c
<VAR>a b c d✝ m n k : ℕ<VAR>p q : ℕ → Prop<VAR>h : a * b ∣ c<VAR>ha✝ : ¬a = 0<VAR>ha : 0 < a<VAR>h1 : ∃ d, c = a * b * d<VAR>d : ℕ<VAR>hd : c = a * b * d<GOAL>c = a * (b * d)
<VAR>X✝ : Type u<VAR>Y✝ : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X✝<VAR>inst✝⁴ : TopologicalSpace Y✝<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>X : Type u_5<VAR>Y : Type u_6<VAR>s : Set (Set X)<VAR>t : Set (Set Y)<VAR>hs : ⋃₀ s = univ<VAR>ht : ⋃₀ t = univ<VAR>G : TopologicalSpace (X × Y) := generateFrom (image2 (fun x x_1 => x ×ˢ x_1) s t)<VAR>u : Set X<VAR>hu : u ∈ s<GOAL>⋃ v ∈ t, u ×ˢ v = Prod.fst ⁻¹' u
<VAR>X✝ : Type u<VAR>Y✝ : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X✝<VAR>inst✝⁴ : TopologicalSpace Y✝<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>X : Type u_5<VAR>Y : Type u_6<VAR>s : Set (Set X)<VAR>t : Set (Set Y)<VAR>hs : ⋃₀ s = univ<VAR>ht : ⋃₀ t = univ<VAR>G : TopologicalSpace (X × Y) := generateFrom (image2 (fun x x_1 => x ×ˢ x_1) s t)<VAR>u : Set X<VAR>hu : u ∈ s<VAR>this : ⋃ v ∈ t, u ×ˢ v = Prod.fst ⁻¹' u<GOAL>TopologicalSpace.IsOpen (⋃ v ∈ t, u ×ˢ v)
<VAR>X✝ : Type u<VAR>Y✝ : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X✝<VAR>inst✝⁴ : TopologicalSpace Y✝<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>X : Type u_5<VAR>Y : Type u_6<VAR>s : Set (Set X)<VAR>t : Set (Set Y)<VAR>hs : ⋃₀ s = univ<VAR>ht : ⋃₀ t = univ<VAR>G : TopologicalSpace (X × Y) := generateFrom (image2 (fun x x_1 => x ×ˢ x_1) s t)<VAR>v : Set Y<VAR>hv : v ∈ t<GOAL>⋃ u ∈ s, u ×ˢ v = Prod.snd ⁻¹' v
<VAR>X✝ : Type u<VAR>Y✝ : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X✝<VAR>inst✝⁴ : TopologicalSpace Y✝<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>X : Type u_5<VAR>Y : Type u_6<VAR>s : Set (Set X)<VAR>t : Set (Set Y)<VAR>hs : ⋃₀ s = univ<VAR>ht : ⋃₀ t = univ<VAR>G : TopologicalSpace (X × Y) := generateFrom (image2 (fun x x_1 => x ×ˢ x_1) s t)<VAR>v : Set Y<VAR>hv : v ∈ t<VAR>this : ⋃ u ∈ s, u ×ˢ v = Prod.snd ⁻¹' v<GOAL>TopologicalSpace.IsOpen (⋃ u ∈ s, u ×ˢ v)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n' + a = n<VAR>x : R<VAR>p q : ℤ<VAR>hpq : p + n' = q<GOAL>((x • γ).rightShift a n' hn').v p q hpq = x • (γ.rightShift a n' hn').v p q hpq
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x✝ : α<VAR>inst✝¹ : Semiring α<VAR>inst✝ : InvolutiveNeg β<VAR>h : Antiperiodic f c<VAR>n : ℕ<VAR>x : α<GOAL>f (x + (↑n * (2 * c) + c)) = -f x
<VAR>R : Type u_1<VAR>c₁ c₂ : R<VAR>inst✝ : Infinite R<GOAL>#ℍ[R,c₁,c₂] = #R
<VAR>R : Type u_1<VAR>F : Type u<VAR>inst✝ : Field F<VAR>p q : F[X]<VAR>f g : RatFunc F<VAR>d : ℤ<VAR>α : F<VAR>hα : α ≠ 0<GOAL>(single (-d)) α⁻¹ = ((single d) α)⁻¹
<VAR>R : Type u_1<VAR>F : Type u<VAR>inst✝ : Field F<VAR>p q : F[X]<VAR>f g : RatFunc F<VAR>d : ℤ<VAR>α : F<VAR>hα : α ≠ 0<GOAL>(single d) α * (single (-d)) α⁻¹ = 1
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>inst✝¹ : StrongRankCondition R<VAR>ι : Type u_1<VAR>v : ι → M<VAR>i : LinearIndependent R v<VAR>w : Set M<VAR>inst✝ : Fintype ↑w<VAR>s : span R w = ⊤<GOAL>#ι ≤ ↑(Fintype.card ↑w)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>inst✝¹ : StrongRankCondition R<VAR>ι : Type u_1<VAR>v : ι → M<VAR>i : LinearIndependent R v<VAR>w : Set M<VAR>inst✝ : Fintype ↑w<VAR>s : span R w = ⊤<GOAL>range v ≤ ↑(span R w)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>inst✝¹ : StrongRankCondition R<VAR>ι : Type u_1<VAR>v : ι → M<VAR>i : LinearIndependent R v<VAR>w : Set M<VAR>inst✝ : Fintype ↑w<VAR>s : span R w = ⊤<GOAL>range v ≤ ↑⊤
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝²² : NontriviallyNormedField R<VAR>inst✝²¹ : (x : B) → AddCommMonoid (E x)<VAR>inst✝²⁰ : (x : B) → Module R (E x)<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace R F<VAR>inst✝¹⁷ : TopologicalSpace B<VAR>inst✝¹⁶ : (x : B) → TopologicalSpace (E x)<VAR>𝕜₁ : Type u_5<VAR>𝕜₂ : Type u_6<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜₁<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>B' : Type u_7<VAR>inst✝¹³ : TopologicalSpace B'<VAR>inst✝¹² : NormedSpace 𝕜₁ F<VAR>inst✝¹¹ : (x : B) → Module 𝕜₁ (E x)<VAR>inst✝¹⁰ : TopologicalSpace (TotalSpace F E)<VAR>F' : Type u_8<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜₂ F'<VAR>E' : B' → Type u_9<VAR>inst✝⁷ : (x : B') → AddCommMonoid (E' x)<VAR>inst✝⁶ : (x : B') → Module 𝕜₂ (E' x)<VAR>inst✝⁵ : TopologicalSpace (TotalSpace F' E')<VAR>inst✝⁴ : FiberBundle F E<VAR>inst✝³ : VectorBundle 𝕜₁ F E<VAR>inst✝² : (x : B') → TopologicalSpace (E' x)<VAR>inst✝¹ : FiberBundle F' E'<VAR>inst✝ : VectorBundle 𝕜₂ F' E'<VAR>ι : Type u_10<VAR>ι' : Type u_11<VAR>Z : VectorBundleCore 𝕜₁ B F ι<VAR>Z' : VectorBundleCore 𝕜₂ B' F' ι'<VAR>x₀ x : B<VAR>y₀ y : B'<VAR>ϕ : F →SL[σ] F'<VAR>hx : x ∈ Z.baseSet (Z.indexAt x₀)<VAR>hy : y ∈ Z'.baseSet (Z'.indexAt y₀)<GOAL>inCoordinates F Z.Fiber F' Z'.Fiber x₀ x y₀ y ϕ = (Z'.coordChange (Z'.indexAt y) (Z'.indexAt y₀) y).comp (ϕ.comp (Z.coordChange (Z.indexAt x₀) (Z.indexAt x) x))
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : CommGroupWithZero G₀<VAR>a b✝ c d b : G₀<VAR>h : a ≠ 0<GOAL>1 / (a * b) * a = 1 / b
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ ε : ℝ<VAR>s t : Set α<VAR>x : α<VAR>E : Set α<GOAL>closure E = ⋂ δ, ⋂ (_ : 0 < δ), thickening δ E
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ ε : ℝ<VAR>s t : Set α<VAR>x : α<VAR>E : Set α<GOAL>cthickening 0 E = ⋂ δ, ⋂ (_ : 0 < δ), thickening δ E
<GOAL>(abscissaOfAbsConv fun n => ↑(μ n)) = 1
<GOAL>(fun n => ↑n !) ~[atTop] fun n => √(2 * ↑n * π) * (↑n / rexp 1) ^ n
<GOAL>∀ᶠ (x : ℕ) in atTop, √(2 * ↑x * π) * (↑x / rexp 1) ^ x = 0 → ↑x ! = 0
<GOAL>Tendsto ((fun n => ↑n !) / fun n => √(2 * ↑n * π) * (↑n / rexp 1) ^ n) atTop (𝓝 1)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁷ : DecidableEq α'<VAR>inst✝⁶ : DecidableEq β'<VAR>inst✝⁵ : DecidableEq γ<VAR>inst✝⁴ : DecidableEq γ'<VAR>inst✝³ : DecidableEq δ<VAR>inst✝² : DecidableEq δ'<VAR>inst✝¹ : DecidableEq ε<VAR>inst✝ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>h : ∀ a ∈ s, ∀ b ∈ t, f a b = f' a b<GOAL>image2 f ↑s ↑t = image2 f' ↑s ↑t
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : RCLike 𝕜<VAR>n : Type u_2<VAR>inst✝³ : LinearOrder n<VAR>inst✝² : IsWellOrder n fun x x_1 => x < x_1<VAR>inst✝¹ : LocallyFiniteOrderBot n<VAR>S : Matrix n n 𝕜<VAR>inst✝ : Fintype n<VAR>hS : S.PosDef<GOAL>lower hS * diag hS * (lower hS)ᴴ = S
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : RCLike 𝕜<VAR>n : Type u_2<VAR>inst✝³ : LinearOrder n<VAR>inst✝² : IsWellOrder n fun x x_1 => x < x_1<VAR>inst✝¹ : LocallyFiniteOrderBot n<VAR>S : Matrix n n 𝕜<VAR>inst✝ : Fintype n<VAR>hS : S.PosDef<GOAL>diag hS = lowerInv hS * S * (lowerInv hS)ᴴ
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<GOAL>HasDerivAt (fun x => jacobiTheta₂ x τ) (jacobiTheta₂' z τ) z
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<VAR>eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ := { toFun := fun f => f (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }<GOAL>HasDerivAt (fun x => jacobiTheta₂ x τ) (jacobiTheta₂' z τ) z
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<VAR>eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ := { toFun := fun f => f (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }<VAR>step1 : HasSum (fun n => (jacobiTheta₂_term_fderiv n z τ) (1, 0)) ((jacobiTheta₂_fderiv z τ) (1, 0))<GOAL>HasDerivAt (fun x => jacobiTheta₂ x τ) (jacobiTheta₂' z τ) z
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<VAR>eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ := { toFun := fun f => f (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }<VAR>step1 : HasSum (fun n => (jacobiTheta₂_term_fderiv n z τ) (1, 0)) ((jacobiTheta₂_fderiv z τ) (1, 0))<VAR>step2 : ∀ (n : ℤ), (jacobiTheta₂_term_fderiv n z τ) (1, 0) = jacobiTheta₂'_term n z τ<GOAL>HasDerivAt (fun x => jacobiTheta₂ x τ) (jacobiTheta₂' z τ) z
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<VAR>eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ := { toFun := fun f => f (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }<VAR>step1 : HasSum (fun x => jacobiTheta₂'_term x z τ) ((jacobiTheta₂_fderiv z τ) (1, 0))<VAR>step2 : ∀ (n : ℤ), (jacobiTheta₂_term_fderiv n z τ) (1, 0) = jacobiTheta₂'_term n z τ<GOAL>HasDerivAt (fun x => jacobiTheta₂ x τ) (jacobiTheta₂' z τ) z
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<VAR>eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ := { toFun := fun f => f (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }<VAR>step1 : HasSum (fun x => jacobiTheta₂'_term x z τ) ((jacobiTheta₂_fderiv z τ) (1, 0))<VAR>step2 : ∀ (n : ℤ), (jacobiTheta₂_term_fderiv n z τ) (1, 0) = jacobiTheta₂'_term n z τ<VAR>step3 : HasDerivAt (fun x => jacobiTheta₂ x τ) ((jacobiTheta₂_fderiv z τ) (1, 0)) z<GOAL>HasDerivAt (fun x => jacobiTheta₂ x τ) (jacobiTheta₂' z τ) z
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>𝕜 : ?m.59015<VAR>h : I * I = -1<GOAL>im I = 1