ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>r : ℝ<VAR>hnr : ↑(finrank ℝ E) < r<VAR>hr : 0 < r<GOAL>∫⁻ (x : E), ENNReal.ofReal ((1 + ‖x‖) ^ (-r)) ∂μ < ⊤
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>r : ℝ<VAR>hnr : ↑(finrank ℝ E) < r<VAR>hr : 0 < r<VAR>h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)<VAR>h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)<GOAL>∫⁻ (x : E), ENNReal.ofReal ((1 + ‖x‖) ^ (-r)) ∂μ < ⊤
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>r : ℝ<VAR>hnr : ↑(finrank ℝ E) < r<VAR>hr : 0 < r<VAR>h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)<VAR>h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)<GOAL>∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ (1 + ‖a‖) ^ (-r)} < ⊤
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>r : ℝ<VAR>hnr : ↑(finrank ℝ E) < r<VAR>hr : 0 < r<VAR>h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)<VAR>h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)<VAR>h_int : ∀ (t : ℝ), 0 < t → μ {a | t ≤ (1 + ‖a‖) ^ (-r)} = μ (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))<GOAL>∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ (1 + ‖a‖) ^ (-r)} < ⊤
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>r : ℝ<VAR>hnr : ↑(finrank ℝ E) < r<VAR>hr : 0 < r<VAR>h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)<VAR>h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)<VAR>h_int : ∀ (t : ℝ), 0 < t → μ {a | t ≤ (1 + ‖a‖) ^ (-r)} = μ (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))<GOAL>∫⁻ (x : ℝ) in Ioi 0, μ (Metric.closedBall 0 (x ^ (-r⁻¹) - 1)) ∂volume < ⊤
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>r : ℝ<VAR>hnr : ↑(finrank ℝ E) < r<VAR>hr : 0 < r<VAR>h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)<VAR>h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)<VAR>h_int : ∀ (t : ℝ), 0 < t → μ {a | t ≤ (1 + ‖a‖) ^ (-r)} = μ (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))<VAR>f : ℝ → ℝ≥0∞ := fun t => μ (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))<VAR>mB : ℝ≥0∞ := μ (Metric.ball 0 1)<GOAL>lintegral (volume.restrict (Ioi 0)) f < ⊤
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>r : ℝ<VAR>hnr : ↑(finrank ℝ E) < r<VAR>hr : 0 < r<VAR>h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)<VAR>h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)<VAR>h_int : ∀ (t : ℝ), 0 < t → μ {a | t ≤ (1 + ‖a‖) ^ (-r)} = μ (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))<VAR>f : ℝ → ℝ≥0∞ := fun t => μ (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))<VAR>mB : ℝ≥0∞ := μ (Metric.ball 0 1)<GOAL>∫⁻ (t : ℝ) in Ioc 0 1, f t < ⊤
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>r : ℝ<VAR>hnr : ↑(finrank ℝ E) < r<VAR>hr : 0 < r<VAR>h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)<VAR>h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)<VAR>h_int : ∀ (t : ℝ), 0 < t → μ {a | t ≤ (1 + ‖a‖) ^ (-r)} = μ (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))<VAR>f : ℝ → ℝ≥0∞ := fun t => μ (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))<VAR>mB : ℝ≥0∞ := μ (Metric.ball 0 1)<GOAL>∫⁻ (t : ℝ) in Ioi 1, f t < ⊤
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : NonUnitalNonAssocRing A<VAR>inst✝⁴ : NonUnitalNonAssocRing B<VAR>inst✝³ : NonUnitalNonAssocRing C<VAR>inst✝² : Module R A<VAR>inst✝¹ : Module R B<VAR>inst✝ : Module R C<VAR>S T : NonUnitalSubalgebra R A<VAR>h : S.toNonUnitalSubring = T.toNonUnitalSubring<VAR>x : A<GOAL>x ∈ S ↔ x ∈ T
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M : Type u₄<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : LieRing L₂<VAR>inst✝⁴ : LieAlgebra R L₂<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>I : LieIdeal R L<VAR>x : L<VAR>hxI : Submodule.span R {x} ⊔ (lieIdealSubalgebra R L I).toSubmodule = ⊤<VAR>y : L<GOAL>∃ t, ∃ z ∈ I, y = t • x + z
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M : Type u₄<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : LieRing L₂<VAR>inst✝⁴ : LieAlgebra R L₂<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>I : LieIdeal R L<VAR>x : L<VAR>hxI : Submodule.span R {x} ⊔ (lieIdealSubalgebra R L I).toSubmodule = ⊤<VAR>y : L<VAR>hy : y ∈ ⊤<GOAL>∃ t, ∃ z ∈ I, y = t • x + z
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M : Type u₄<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : LieRing L₂<VAR>inst✝⁴ : LieAlgebra R L₂<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>I : LieIdeal R L<VAR>x : L<VAR>hxI : Submodule.span R {x} ⊔ (lieIdealSubalgebra R L I).toSubmodule = ⊤<VAR>y : L<VAR>hy : ∃ y_1, (∃ a, a • x = y_1) ∧ ∃ z ∈ (lieIdealSubalgebra R L I).toSubmodule, y_1 + z = y<GOAL>∃ t, ∃ z ∈ I, y = t • x + z
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>hfg : f =ᶠ[ae μ] g<GOAL>μ.tilted f = μ.tilted g
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>hfg : f =ᶠ[ae μ] g<VAR>h_int_eq : ∫ (x : α), rexp (f x) ∂μ = ∫ (x : α), rexp (g x) ∂μ<GOAL>μ.tilted f = μ.tilted g
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>hfg : f =ᶠ[ae μ] g<VAR>h_int_eq : ∫ (x : α), rexp (f x) ∂μ = ∫ (x : α), rexp (g x) ∂μ<GOAL>(fun x => ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) =ᶠ[ae μ] fun x => ENNReal.ofReal (rexp (g x) / ∫ (x : α), rexp (g x) ∂μ)
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>hfg : f =ᶠ[ae μ] g<VAR>h_int_eq : ∫ (x : α), rexp (f x) ∂μ = ∫ (x : α), rexp (g x) ∂μ<VAR>x : α<VAR>hx : f x = g x<GOAL>ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) = ENNReal.ofReal (rexp (g x) / ∫ (x : α), rexp (g x) ∂μ)
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<GOAL>bernoulli' 3 = 0
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<GOAL>1 - ∑ k ∈ range 3, ↑(Nat.choose 3 k) / (↑3 - ↑k + 1) * bernoulli' k = 0
<VAR>c : Char<VAR>cs : List Char<GOAL>{ data := c :: cs }.extract 0 { data := c :: cs }.endPos = { data := c :: cs }
<VAR>c : Char<VAR>cs : List Char<GOAL>{ data := extract.go₁ (c :: cs) 0 0 { byteIdx := utf8Len cs + c.utf8Size } } = { data := c :: cs }
<VAR>c : Char<VAR>cs : List Char<GOAL>extract.go₁ (c :: cs) 0 0 { byteIdx := utf8Len cs + c.utf8Size } = c :: cs
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝³ : Semiring S<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Field K<VAR>p q : R[X]<VAR>r : R<VAR>h : p.leadingCoeff * q.leadingCoeff ≠ 0<GOAL>(p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>g : P →ₗ[R] Q<VAR>f : N →ₗ[R] P<GOAL>Function.Surjective ⇑(lTensor M f) ↔ Function.Surjective ⇑(rTensor M f)
<VAR>a b c : ℤ<VAR>ha : a ≠ 0<VAR>h3a : 3 ∣ a<VAR>Hgcd : {a, b, c}.gcd id = 1<VAR>H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3<VAR>HF : a ^ 3 + b ^ 3 + c ^ 3 = 0<GOAL>3 ∣ {a, b, c}.gcd id
<VAR>a b c : ℤ<VAR>ha : a ≠ 0<VAR>h3a : 3 ∣ a<VAR>Hgcd : {a, b, c}.gcd id = 1<VAR>H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3<VAR>HF : a ^ 3 + b ^ 3 + c ^ 3 = 0<VAR>x : ℤ<VAR>hx : x ∈ {a, b, c}<GOAL>3 ∣ id x
<VAR>a b c : ℤ<VAR>ha : a ≠ 0<VAR>h3a : 3 ∣ a<VAR>Hgcd : {a, b, c}.gcd id = 1<VAR>H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3<VAR>HF : a ^ 3 + b ^ 3 + c ^ 3 = 0<VAR>x : ℤ<VAR>hx : x = a ∨ x = b ∨ x = c<GOAL>3 ∣ id x
<VAR>a b c : ℤ<VAR>ha : a ≠ 0<VAR>h3a : 3 ∣ a<VAR>Hgcd : {a, b, c}.gcd id = 1<VAR>H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3<VAR>HF : a ^ 3 + b ^ 3 + c ^ 3 = 0<VAR>x : ℤ<VAR>hx : x = a ∨ x = b ∨ x = c<VAR>h3b : 3 ∣ b<GOAL>3 ∣ id x
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n✝ : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : AddCommGroup L<VAR>inst✝¹³ : Module R L<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝¹⁰ : Fintype ι<VAR>inst✝⁹ : Fintype ι'<VAR>inst✝⁸ : Fintype ιM<VAR>inst✝⁷ : DecidableEq ι<VAR>inst✝⁶ : DecidableEq ι'<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>b✝ : Basis ι R L<VAR>inst✝³ : Module.Finite R L<VAR>inst✝² : Module.Free R L<VAR>inst✝¹ : Nontrivial R<VAR>x : L<VAR>inst✝ : IsDomain R<VAR>h : ↑(finrank R M) ≤ #R<VAR>b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L<VAR>bₘ : Basis (ChooseBasisIndex R M) R M := chooseBasis R M<VAR>n : ℕ := Fintype.card (ChooseBasisIndex R M)<GOAL>∃ x, φ.IsNilRegular x
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n✝ : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : AddCommGroup L<VAR>inst✝¹³ : Module R L<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝¹⁰ : Fintype ι<VAR>inst✝⁹ : Fintype ι'<VAR>inst✝⁸ : Fintype ιM<VAR>inst✝⁷ : DecidableEq ι<VAR>inst✝⁶ : DecidableEq ι'<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>b✝ : Basis ι R L<VAR>inst✝³ : Module.Finite R L<VAR>inst✝² : Module.Free R L<VAR>inst✝¹ : Nontrivial R<VAR>x : L<VAR>inst✝ : IsDomain R<VAR>h : ↑(finrank R M) ≤ #R<VAR>b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L<VAR>bₘ : Basis (ChooseBasisIndex R M) R M := chooseBasis R M<VAR>n : ℕ := Fintype.card (ChooseBasisIndex R M)<VAR>aux : ((φ.polyCharpoly b).coeff φ.nilRank).IsHomogeneous (n - φ.nilRank)<GOAL>∃ x, φ.IsNilRegular x
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n✝ : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : AddCommGroup L<VAR>inst✝¹³ : Module R L<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝¹⁰ : Fintype ι<VAR>inst✝⁹ : Fintype ι'<VAR>inst✝⁸ : Fintype ιM<VAR>inst✝⁷ : DecidableEq ι<VAR>inst✝⁶ : DecidableEq ι'<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>b✝ : Basis ι R L<VAR>inst✝³ : Module.Finite R L<VAR>inst✝² : Module.Free R L<VAR>inst✝¹ : Nontrivial R<VAR>x✝ : L<VAR>inst✝ : IsDomain R<VAR>h : ↑(finrank R M) ≤ #R<VAR>b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L<VAR>bₘ : Basis (ChooseBasisIndex R M) R M := chooseBasis R M<VAR>n : ℕ := Fintype.card (ChooseBasisIndex R M)<VAR>aux : ((φ.polyCharpoly b).coeff φ.nilRank).IsHomogeneous (n - φ.nilRank)<VAR>x : ChooseBasisIndex R L → R<VAR>hx : (eval x) ((φ.polyCharpoly b).coeff φ.nilRank) ≠ 0<GOAL>∃ x, φ.IsNilRegular x
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n✝ : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : AddCommGroup L<VAR>inst✝¹³ : Module R L<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝¹⁰ : Fintype ι<VAR>inst✝⁹ : Fintype ι'<VAR>inst✝⁸ : Fintype ιM<VAR>inst✝⁷ : DecidableEq ι<VAR>inst✝⁶ : DecidableEq ι'<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>b✝ : Basis ι R L<VAR>inst✝³ : Module.Finite R L<VAR>inst✝² : Module.Free R L<VAR>inst✝¹ : Nontrivial R<VAR>x✝ : L<VAR>inst✝ : IsDomain R<VAR>h : ↑(finrank R M) ≤ #R<VAR>b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L<VAR>bₘ : Basis (ChooseBasisIndex R M) R M := chooseBasis R M<VAR>n : ℕ := Fintype.card (ChooseBasisIndex R M)<VAR>aux : ((φ.polyCharpoly b).coeff φ.nilRank).IsHomogeneous (n - φ.nilRank)<VAR>x : ChooseBasisIndex R L → R<VAR>hx : (eval x) ((φ.polyCharpoly b).coeff φ.nilRank) ≠ 0<VAR>c : ChooseBasisIndex R L →₀ R := Finsupp.equivFunOnFinite.symm x<GOAL>∃ x, φ.IsNilRegular x
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n✝ : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : AddCommGroup L<VAR>inst✝¹³ : Module R L<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝¹⁰ : Fintype ι<VAR>inst✝⁹ : Fintype ι'<VAR>inst✝⁸ : Fintype ιM<VAR>inst✝⁷ : DecidableEq ι<VAR>inst✝⁶ : DecidableEq ι'<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>b✝ : Basis ι R L<VAR>inst✝³ : Module.Finite R L<VAR>inst✝² : Module.Free R L<VAR>inst✝¹ : Nontrivial R<VAR>x✝ : L<VAR>inst✝ : IsDomain R<VAR>h : ↑(finrank R M) ≤ #R<VAR>b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L<VAR>bₘ : Basis (ChooseBasisIndex R M) R M := chooseBasis R M<VAR>n : ℕ := Fintype.card (ChooseBasisIndex R M)<VAR>aux : ((φ.polyCharpoly b).coeff φ.nilRank).IsHomogeneous (n - φ.nilRank)<VAR>x : ChooseBasisIndex R L → R<VAR>hx : (eval x) ((φ.polyCharpoly b).coeff φ.nilRank) ≠ 0<VAR>c : ChooseBasisIndex R L →₀ R := Finsupp.equivFunOnFinite.symm x<GOAL>φ.IsNilRegular (b.repr.symm c)
<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>inst✝¹ : NoMinOrder α<VAR>inst✝ : NoMaxOrder α<VAR>a b x : α<GOAL>Icc a b ∈ 𝓝 x ↔ x ∈ Ioo a b
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : Group H<VAR>inst✝⁴ : MulAction G α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MulAction H β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>ν : Measure β<VAR>h : IsFundamentalDomain G s μ<VAR>f : β → α<VAR>hf : QuasiMeasurePreserving f ν μ<VAR>e : G → H<VAR>he : Bijective e<VAR>hef : ∀ (g : G), Semiconj f (fun x => e g • x) fun x => g • x<VAR>x : β<VAR>x✝ : ∃ g, g • f x ∈ s<VAR>g : G<VAR>hg : g • f x ∈ s<GOAL>e g • x ∈ f ⁻¹' s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : Group H<VAR>inst✝⁴ : MulAction G α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MulAction H β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>ν : Measure β<VAR>h : IsFundamentalDomain G s μ<VAR>f : β → α<VAR>hf : QuasiMeasurePreserving f ν μ<VAR>a b : H<VAR>hab : a ≠ b<VAR>e : G ≃ H<VAR>hef : ∀ (g : G), Semiconj f (fun x => e g • x) fun x => g • x<VAR>this : (e.symm a⁻¹)⁻¹ ≠ (e.symm b⁻¹)⁻¹<GOAL>(AEDisjoint ν on fun g => g • f ⁻¹' s) a b
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : Group H<VAR>inst✝⁴ : MulAction G α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MulAction H β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>ν : Measure β<VAR>h : IsFundamentalDomain G s μ<VAR>f : β → α<VAR>hf : QuasiMeasurePreserving f ν μ<VAR>a b : H<VAR>hab : a ≠ b<VAR>e : G ≃ H<VAR>hef : ∀ (g : G), Semiconj f (fun x => e g • x) fun x => g • x<VAR>this✝ : (e.symm a⁻¹)⁻¹ ≠ (e.symm b⁻¹)⁻¹<VAR>this : AEDisjoint ν (f ⁻¹' (fun g => g • s) (e.symm a⁻¹)⁻¹) (f ⁻¹' (fun g => g • s) (e.symm b⁻¹)⁻¹)<GOAL>(AEDisjoint ν on fun g => g • f ⁻¹' s) a b
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : Group H<VAR>inst✝⁴ : MulAction G α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MulAction H β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>ν : Measure β<VAR>h : IsFundamentalDomain G s μ<VAR>f : β → α<VAR>hf : QuasiMeasurePreserving f ν μ<VAR>a b : H<VAR>hab : a ≠ b<VAR>e : G ≃ H<VAR>hef : ∀ (g : G) (x : β), f (e g • x) = g • f x<VAR>this✝ : (e.symm a⁻¹)⁻¹ ≠ (e.symm b⁻¹)⁻¹<VAR>this : AEDisjoint ν (f ⁻¹' (fun g => g • s) (e.symm a⁻¹)⁻¹) (f ⁻¹' (fun g => g • s) (e.symm b⁻¹)⁻¹)<GOAL>(AEDisjoint ν on fun g => g • f ⁻¹' s) a b
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>α : Type u_9<VAR>β : Type u_10<VAR>s : Set (α → β → Prop)<VAR>a : α<VAR>b : β<GOAL>sInf s a b ↔ ∀ r ∈ s, r a b
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>α : Type u_9<VAR>β : Type u_10<VAR>s : Set (α → β → Prop)<VAR>a : α<VAR>b : β<GOAL>(⨅ f, ↑f a) b ↔ ∀ r ∈ s, r a b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>l : List ℤ<VAR>n : ℤ<GOAL>l.sum % n = (map (fun x => x % n) l).sum % n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s✝ : Set α<VAR>t : Set β<VAR>s : Set α<VAR>x✝ : s ∈ ⊥<GOAL>m ⁻¹' ∅ ⊆ s
<VAR>X✝ : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X✝<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t : Set X✝<VAR>X : ι → Type u_2<VAR>inst✝ : (i : ι) → TopologicalSpace (X i)<VAR>s : (i : ι) → Set (X i)<GOAL>(∀ (i : ι), IsCompact (s i)) → IsCompact {x | ∀ (i : ι), x i ∈ s i}
<VAR>X✝ : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X✝<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t : Set X✝<VAR>X : ι → Type u_2<VAR>inst✝ : (i : ι) → TopologicalSpace (X i)<VAR>s : (i : ι) → Set (X i)<GOAL>(∀ (i : ι) (f : Ultrafilter (X i)), s i ∈ ↑f → ∃ x ∈ s i, ↑f ≤ 𝓝 x) → ∀ (f : Ultrafilter ((i : ι) → X i)), {x | ∀ (i : ι), x i ∈ s i} ∈ ↑f → ∃ x ∈ {x | ∀ (i : ι), x i ∈ s i}, ∀ (i : ι), Tendsto (eval i) (↑f) (𝓝 (x i))
<VAR>X✝ : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X✝<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t : Set X✝<VAR>X : ι → Type u_2<VAR>inst✝ : (i : ι) → TopologicalSpace (X i)<VAR>s : (i : ι) → Set (X i)<VAR>h : ∀ (i : ι) (f : Ultrafilter (X i)), s i ∈ ↑f → ∃ x ∈ s i, ↑f ≤ 𝓝 x<VAR>f : Ultrafilter ((i : ι) → X i)<VAR>hfs : {x | ∀ (i : ι), x i ∈ s i} ∈ ↑f<GOAL>∃ x ∈ {x | ∀ (i : ι), x i ∈ s i}, ∀ (i : ι), Tendsto (eval i) (↑f) (𝓝 (x i))
<VAR>X✝ : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X✝<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t : Set X✝<VAR>X : ι → Type u_2<VAR>inst✝ : (i : ι) → TopologicalSpace (X i)<VAR>s : (i : ι) → Set (X i)<VAR>h : ∀ (i : ι) (f : Ultrafilter (X i)), s i ∈ ↑f → ∃ x ∈ s i, ↑f ≤ 𝓝 x<VAR>f : Ultrafilter ((i : ι) → X i)<VAR>hfs : {x | ∀ (i : ι), x i ∈ s i} ∈ ↑f<VAR>this : ∀ (i : ι), ∃ x ∈ s i, Tendsto (eval i) (↑f) (𝓝 x)<GOAL>∃ x ∈ {x | ∀ (i : ι), x i ∈ s i}, ∀ (i : ι), Tendsto (eval i) (↑f) (𝓝 (x i))
<VAR>X✝ : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X✝<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t : Set X✝<VAR>X : ι → Type u_2<VAR>inst✝ : (i : ι) → TopologicalSpace (X i)<VAR>s : (i : ι) → Set (X i)<VAR>h : ∀ (i : ι) (f : Ultrafilter (X i)), s i ∈ ↑f → ∃ x ∈ s i, ↑f ≤ 𝓝 x<VAR>f : Ultrafilter ((i : ι) → X i)<VAR>hfs : {x | ∀ (i : ι), x i ∈ s i} ∈ ↑f<VAR>x : (i : ι) → X i<VAR>hx : ∀ (i : ι), x i ∈ s i ∧ Tendsto (eval i) (↑f) (𝓝 (x i))<GOAL>∃ x ∈ {x | ∀ (i : ι), x i ∈ s i}, ∀ (i : ι), Tendsto (eval i) (↑f) (𝓝 (x i))
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommRing P<VAR>K : Type u_4<VAR>inst✝ : IsLocalization M S<VAR>hM : M ≤ nonZeroDivisors R<GOAL>Injective ⇑(algebraMap R S)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommRing P<VAR>K : Type u_4<VAR>inst✝ : IsLocalization M S<VAR>hM : M ≤ nonZeroDivisors R<GOAL>∀ (a : R), (algebraMap R S) a = 0 → a = 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommRing P<VAR>K : Type u_4<VAR>inst✝ : IsLocalization M S<VAR>hM : M ≤ nonZeroDivisors R<VAR>a : R<VAR>ha : (algebraMap R S) a = 0<GOAL>a = 0
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>m m' : AddContent C<VAR>hC : IsSetSemiring C<VAR>h_ss : ↑I ⊆ C<VAR>h_dis : (↑I).PairwiseDisjoint id<VAR>ht : t ∈ C<VAR>hJt : ∀ s ∈ I, s ⊆ t<GOAL>∑ u ∈ I, m u ≤ m t
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>x : α × β<GOAL>x ∈ interedges r s₂ t₂ → x ∈ interedges r s₁ t₁
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>x : α × β<GOAL>x.1 ∈ s₂ ∧ x.2 ∈ t₂ ∧ r x.1 x.2 → x.1 ∈ s₁ ∧ x.2 ∈ t₁ ∧ r x.1 x.2
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G✝ : SimpleGraph V<VAR>a b c u v✝ w✝ : V<VAR>e : Sym2 V<VAR>G : SimpleGraph V<VAR>v w : V<GOAL>w ∈ G.neighborSet v ∪ Gᶜ.neighborSet v ↔ w ∈ {v}ᶜ
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G✝ : SimpleGraph V<VAR>a b c u v✝ w✝ : V<VAR>e : Sym2 V<VAR>G : SimpleGraph V<VAR>v w : V<VAR>h : ∀ {a b : V}, G.Adj a b → a ≠ b<GOAL>w ∈ G.neighborSet v ∪ Gᶜ.neighborSet v ↔ w ∈ {v}ᶜ
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G✝ : SimpleGraph V<VAR>a b c u v✝ w✝ : V<VAR>e : Sym2 V<VAR>G : SimpleGraph V<VAR>v w : V<VAR>h : ∀ {a b : V}, G.Adj a b → a ≠ b<GOAL>G.Adj v w ∨ v ≠ w ∧ ¬G.Adj v w ↔ ¬w = v
<VAR>n₁ n₂ : ℤ<GOAL>(n₁ - n₂).negOnePow = n₁.negOnePow * n₂.negOnePow
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : DecidableEq β<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → Fintype ↑(Rel.image r {a})<VAR>r' : α → Finset β := fun a => (Rel.image r {a}).toFinset<GOAL>(∀ (A : Finset α), A.card ≤ card ↑(Rel.image r ↑A)) ↔ ∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : DecidableEq β<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → Fintype ↑(Rel.image r {a})<VAR>r' : α → Finset β := fun a => (Rel.image r {a}).toFinset<VAR>h : ∀ (A : Finset α), card ↑(Rel.image r ↑A) = (A.biUnion r').card<GOAL>(∀ (A : Finset α), A.card ≤ card ↑(Rel.image r ↑A)) ↔ ∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : DecidableEq β<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → Fintype ↑(Rel.image r {a})<VAR>r' : α → Finset β := fun a => (Rel.image r {a}).toFinset<VAR>h : ∀ (A : Finset α), card ↑(Rel.image r ↑A) = (A.biUnion r').card<VAR>h' : ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x<GOAL>(∀ (A : Finset α), A.card ≤ card ↑(Rel.image r ↑A)) ↔ ∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)