ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R✝ : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>a b : R✝<VAR>n : ℕ<VAR>inst✝⁶ : CommRing R✝<VAR>inst✝⁵ : IsDomain R✝<VAR>p q : R✝[X]<VAR>inst✝⁴ : CommRing T<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : Semiring R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>inst✝ : DecidableEq S<VAR>m : R →+* S<VAR>d : ℕ<VAR>U : Set R<VAR>h : U.Finite<VAR>π : R[X] → Fin (d + 1) → R := fun f i => f.coeff ↑i<GOAL>Set.Finite fun f => f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U
<VAR>R✝ : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>a b : R✝<VAR>n : ℕ<VAR>inst✝⁶ : CommRing R✝<VAR>inst✝⁵ : IsDomain R✝<VAR>p q : R✝[X]<VAR>inst✝⁴ : CommRing T<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : Semiring R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>inst✝ : DecidableEq S<VAR>m : R →+* S<VAR>d : ℕ<VAR>U : Set R<VAR>h : U.Finite<VAR>π : R[X] → Fin (d + 1) → R := fun f i => f.coeff ↑i<GOAL>(π '' fun f => f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U) ⊆ Set.univ.pi fun x => U
<VAR>R✝ : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>a b : R✝<VAR>n : ℕ<VAR>inst✝⁶ : CommRing R✝<VAR>inst✝⁵ : IsDomain R✝<VAR>p q : R✝[X]<VAR>inst✝⁴ : CommRing T<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : Semiring R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>inst✝ : DecidableEq S<VAR>m : R →+* S<VAR>d : ℕ<VAR>U : Set R<VAR>h : U.Finite<VAR>π : R[X] → Fin (d + 1) → R := fun f i => f.coeff ↑i<GOAL>Set.InjOn π fun f => f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U
<VAR>R : Type u<VAR>inst✝¹¹ : Ring R<VAR>ι : Type v<VAR>inst✝¹⁰ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁹ : (i : ι) → AddCommGroup (G i)<VAR>inst✝⁸ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝⁷ : DecidableEq ι<VAR>P : Type u₁<VAR>inst✝⁶ : AddCommGroup P<VAR>inst✝⁵ : Module R P<VAR>g : (i : ι) → G i →ₗ[R] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>G' : ι → Type v'<VAR>inst✝⁴ : (i : ι) → AddCommGroup (G' i)<VAR>inst✝³ : (i : ι) → Module R (G' i)<VAR>f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j<VAR>G'' : ι → Type v''<VAR>inst✝² : (i : ι) → AddCommGroup (G'' i)<VAR>inst✝¹ : (i : ι) → Module R (G'' i)<VAR>f'' : (i j : ι) → i ≤ j → G'' i →ₗ[R] G'' j<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>g₁ : (i : ι) → G i →ₗ[R] G' i<VAR>g₂ : (i : ι) → G' i →ₗ[R] G'' i<VAR>hg₁ : ∀ (i j : ι) (h : i ≤ j), g₁ j ∘ₗ f i j h = f' i j h ∘ₗ g₁ i<VAR>hg₂ : ∀ (i j : ι) (h : i ≤ j), g₂ j ∘ₗ f' i j h = f'' i j h ∘ₗ g₂ i<VAR>i j : ι<VAR>h : i ≤ j<GOAL>(fun i => g₂ i ∘ₗ g₁ i) j ∘ₗ f i j h = f'' i j h ∘ₗ (fun i => g₂ i ∘ₗ g₁ i) i
<VAR>z τ : ℂ<GOAL>(starRingEnd ℂ) (jacobiTheta₂'' z τ) = jacobiTheta₂'' ((starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>v : V<VAR>w : W<GOAL>HasFDerivAt (fun w' => 𝐞 (-(L v) w') • f v) (𝐞 (-(L v) w) • fourierSMulRight L f v) w
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>v : V<VAR>w : W<VAR>ha : HasFDerivAt (fun w' => (L v) w') (L v) w<GOAL>HasFDerivAt (fun w' => 𝐞 (-(L v) w') • f v) (𝐞 (-(L v) w) • fourierSMulRight L f v) w
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>v : V<VAR>w : W<VAR>ha : HasFDerivAt (fun w' => (L v) w') (L v) w<GOAL>𝐞 (-(L v) w) • fourierSMulRight L f v = ((ContinuousLinearMap.smulRight 1 (2 * ↑π * I * ↑(𝐞 (-(L v) w)))).comp (-L v)).smulRight (f v)
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>v : V<VAR>w : W<VAR>ha : HasFDerivAt (fun w' => (L v) w') (L v) w<VAR>w' : W<GOAL>(𝐞 (-(L v) w) • fourierSMulRight L f v) w' = (((ContinuousLinearMap.smulRight 1 (2 * ↑π * I * ↑(𝐞 (-(L v) w)))).comp (-L v)).smulRight (f v)) w'
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>v : V<VAR>w : W<VAR>ha : HasFDerivAt (fun w' => (L v) w') (L v) w<VAR>w' : W<GOAL>𝐞 (-(L v) w) • -(2 * ↑π * I) • (L v) w' • f v = ((ContinuousLinearMap.smulRight 1 (2 * ↑π * I * ↑(𝐞 (-(L v) w)))).comp (-L v)) w' • f v
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>v : V<VAR>w : W<VAR>ha : HasFDerivAt (fun w' => (L v) w') (L v) w<VAR>w' : W<GOAL>(↑((L v) w') * (↑(𝐞 (-(L v) w)) * -(2 * ↑π * I))) • f v = (↑(-(L v) w') * (2 * ↑π * I * ↑(𝐞 (-(L v) w)))) • f v
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : Ideal R<VAR>hI : I ≠ 0<GOAL>{v | v.asIdeal ∣ I}.Finite
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : Ideal R<VAR>hI : I ≠ 0<GOAL>Finite { x // x.asIdeal ∣ I }
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : Ideal R<VAR>hI : I ≠ 0<VAR>h_fin : Fintype { x // x ∣ I }<GOAL>Finite { x // x.asIdeal ∣ I }
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : Ideal R<VAR>hI : I ≠ 0<VAR>h_fin : Fintype { x // x ∣ I }<GOAL>Injective fun v => ⟨(↑v).asIdeal, ⋯⟩
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v✝ : HeightOneSpectrum R<VAR>I : Ideal R<VAR>hI : I ≠ 0<VAR>h_fin : Fintype { x // x ∣ I }<VAR>v w : { x // x.asIdeal ∣ I }<VAR>hvw : (↑v).asIdeal = (↑w).asIdeal<GOAL>v = w
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<VAR>p : ι → Prop<VAR>s : ι → Set β<VAR>f : Filter β<VAR>u : β → α<VAR>h : f.HasBasis p s<GOAL>⨅ i, ⨅ (_ : p i), sSup (u '' s i) = ⨅ i, ⨅ (_ : p i), ⨆ a ∈ s i, u a
<VAR>r : ℝ<VAR>hr : 0 < r<VAR>x : ℂ<VAR>hx : x ≠ 0<GOAL>log (↑r * x) = ↑(Real.log r) + log x
<VAR>r : ℝ<VAR>hr : 0 < r<VAR>x : ℂ<VAR>hx : abs x ≠ 0<GOAL>log (↑r * x) = ↑(Real.log r) + log x
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>hα : α.IsNonZero<GOAL>α (coroot α) = 2
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>hα : α.IsNonZero<GOAL>(Weight.toLinear K (↥H) L α) (coroot α) = 2
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommMonoid M<VAR>s₂ s₁ s : Finset α<VAR>a✝ : α<VAR>g f✝ : α → M<VAR>inst✝² : OrderedCancelAddCommMonoid α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : LocallyFiniteOrder α<VAR>f : α → M<VAR>a b c : α<GOAL>∏ x ∈ Ico a b, f (x + c) = ∏ x ∈ Ico (a + c) (b + c), f x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommMonoid M<VAR>s₂ s₁ s : Finset α<VAR>a✝ : α<VAR>g f✝ : α → M<VAR>inst✝² : OrderedCancelAddCommMonoid α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : LocallyFiniteOrder α<VAR>f : α → M<VAR>a b c : α<GOAL>∏ x ∈ Ico a b, f (x + c) = ∏ x ∈ Ico a b, f ((addRightEmbedding c) x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f✝ : α → β<VAR>hp_one : 1 ≤ p<VAR>hp_top : p ≠ ⊤<VAR>n : ℕ<VAR>h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p μ) → UnifIntegrable f p μ<VAR>f : Fin (n + 1) → α → β<VAR>hfLp : ∀ (i : Fin (n + 1)), Memℒp (f i) p μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>g : Fin n → α → β := fun k => f ↑↑k<VAR>hgLp : ∀ (i : Fin n), Memℒp (g i) p μ<VAR>δ₁ : ℝ<VAR>hδ₁pos : 0 < δ₁<VAR>hδ₁ : ∀ (i : Fin n) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε<GOAL>∃ δ, ∃ (_ : 0 < δ), ∀ (i : Fin (n + 1)) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f✝ : α → β<VAR>hp_one : 1 ≤ p<VAR>hp_top : p ≠ ⊤<VAR>n : ℕ<VAR>h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p μ) → UnifIntegrable f p μ<VAR>f : Fin (n + 1) → α → β<VAR>hfLp : ∀ (i : Fin (n + 1)), Memℒp (f i) p μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>g : Fin n → α → β := fun k => f ↑↑k<VAR>hgLp : ∀ (i : Fin n), Memℒp (g i) p μ<VAR>δ₁ : ℝ<VAR>hδ₁pos : 0 < δ₁<VAR>hδ₁ : ∀ (i : Fin n) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε<VAR>δ₂ : ℝ<VAR>hδ₂pos : 0 < δ₂<VAR>hδ₂ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (f ↑n)) p μ ≤ ENNReal.ofReal ε<GOAL>∃ δ, ∃ (_ : 0 < δ), ∀ (i : Fin (n + 1)) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f✝ : α → β<VAR>hp_one : 1 ≤ p<VAR>hp_top : p ≠ ⊤<VAR>n : ℕ<VAR>h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p μ) → UnifIntegrable f p μ<VAR>f : Fin (n + 1) → α → β<VAR>hfLp : ∀ (i : Fin (n + 1)), Memℒp (f i) p μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>g : Fin n → α → β := fun k => f ↑↑k<VAR>hgLp : ∀ (i : Fin n), Memℒp (g i) p μ<VAR>δ₁ : ℝ<VAR>hδ₁pos : 0 < δ₁<VAR>hδ₁ : ∀ (i : Fin n) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε<VAR>δ₂ : ℝ<VAR>hδ₂pos : 0 < δ₂<VAR>hδ₂ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (f ↑n)) p μ ≤ ENNReal.ofReal ε<VAR>i : Fin (n + 1)<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≤ ENNReal.ofReal (min δ₁ δ₂)<GOAL>eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
<VAR>a b✝ c d : ℝ≥0∞<VAR>r p q b : ℝ≥0<VAR>h0 : ↑b ≠ 0 ∨ c ≠ 0<VAR>ht : ↑b ≠ ⊤ ∨ c ≠ ⊤<GOAL>a ≤ c / ↑b ↔ a * ↑b ≤ c
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h0 : ↑0 ≠ 0 ∨ c ≠ 0<VAR>ht : ↑0 ≠ ⊤ ∨ c ≠ ⊤<GOAL>a ≤ c / ↑0 ↔ a * ↑0 ≤ c
<VAR>a b✝ c d : ℝ≥0∞<VAR>r p q b : ℝ≥0<VAR>h0 : ↑b ≠ 0 ∨ c ≠ 0<VAR>ht : ↑b ≠ ⊤ ∨ c ≠ ⊤<VAR>hb : b ≠ 0<GOAL>a ≤ c / ↑b ↔ a * ↑b ≤ c
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>s : Set α<VAR>inst✝² : Preorder α<VAR>inst✝¹ : InfSet α<VAR>inst✝ : Inhabited ↑s<VAR>t : Set ↑s<VAR>h' : t.Nonempty<VAR>h'' : BddBelow t<VAR>h : sInf (Subtype.val '' t) ∈ s<GOAL>sInf (Subtype.val '' t) = ↑(sInf t)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : 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>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>κ₁ : Type u_13<VAR>κ₂ : Type u_14<VAR>p₁ : κ₁ → Prop<VAR>s₁ : κ₁ → Set (β × β)<VAR>p₂ : κ₂ → Prop<VAR>s₂ : κ₂ → Set (α × α)<VAR>F : ι → β → α<VAR>hβ : (𝓤 β).HasBasis p₁ s₁<VAR>hα : (𝓤 α).HasBasis p₂ s₂<GOAL>UniformEquicontinuous F ↔ ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : 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>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>κ₁ : Type u_13<VAR>κ₂ : Type u_14<VAR>p₁ : κ₁ → Prop<VAR>s₁ : κ₁ → Set (β × β)<VAR>p₂ : κ₂ → Prop<VAR>s₂ : κ₂ → Set (α × α)<VAR>F : ι → β → α<VAR>hβ : (𝓤 β).HasBasis p₁ s₁<VAR>hα : (𝓤 α).HasBasis p₂ s₂<GOAL>(∀ (ib : κ₂), p₂ ib → ∃ ia, p₁ ia ∧ ∀ x ∈ s₁ ia, ((⇑UniformFun.ofFun ∘ swap F) x.1, (⇑UniformFun.ofFun ∘ swap F) x.2) ∈ (UniformFun.gen ι α ∘ s₂) ib) ↔ ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : 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>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>κ₁ : Type u_13<VAR>κ₂ : Type u_14<VAR>p₁ : κ₁ → Prop<VAR>s₁ : κ₁ → Set (β × β)<VAR>p₂ : κ₂ → Prop<VAR>s₂ : κ₂ → Set (α × α)<VAR>F : ι → β → α<VAR>hβ : (𝓤 β).HasBasis p₁ s₁<VAR>hα : (𝓤 α).HasBasis p₂ s₂<GOAL>(∀ (ib : κ₂), p₂ ib → ∃ ia, p₁ ia ∧ ∀ (a b : β), (a, b) ∈ s₁ ia → ((⇑UniformFun.ofFun ∘ swap F) a, (⇑UniformFun.ofFun ∘ swap F) b) ∈ (UniformFun.gen ι α ∘ s₂) ib) ↔ ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : Algebra R S<VAR>P : Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>inst✝¹¹ : CommRing R'<VAR>inst✝¹⁰ : CommRing S'<VAR>inst✝⁹ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝⁸ : Algebra R R'<VAR>inst✝⁷ : Algebra S S'<VAR>inst✝⁶ : Algebra R S'<VAR>inst✝⁵ : IsScalarTower R R' S'<VAR>inst✝⁴ : IsScalarTower R S S'<VAR>T : Type uT<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>f g : P.Hom P'<VAR>r : S<VAR>x : P.Ring<GOAL>(f.sub g) (r ⊗ₜ[P.Ring] (D R P.Ring) x) = r • Cotangent.mk ((f.subToKer g) x)
<VAR>R : Type u<VAR>S : Type v<VAR>S' : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra S R<VAR>inst✝³ : CommSemiring S'<VAR>inst✝² : Algebra S' R<VAR>inst✝¹ : Algebra S S'<VAR>inst✝ : IsScalarTower S S' R<VAR>I : Ideal R<VAR>x y : ↥I<GOAL>I.toCotangent x = I.toCotangent y ↔ ↑x - ↑y ∈ I ^ 2
<VAR>R : Type u<VAR>S : Type v<VAR>S' : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra S R<VAR>inst✝³ : CommSemiring S'<VAR>inst✝² : Algebra S' R<VAR>inst✝¹ : Algebra S S'<VAR>inst✝ : IsScalarTower S S' R<VAR>I : Ideal R<VAR>x y : ↥I<GOAL>I.toCotangent x - I.toCotangent y = 0 ↔ ↑x - ↑y ∈ I ^ 2
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>A✝ B✝ B' X✝ Y✝ Y'✝ : C<VAR>i✝ : A✝ ⟶ B✝<VAR>i' : B✝ ⟶ B'<VAR>p✝ : X✝ ⟶ Y✝<VAR>p'✝ : Y✝ ⟶ Y'✝<VAR>A B X Y X' Y' : C<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>p' : X' ⟶ Y'<VAR>e : Arrow.mk p ≅ Arrow.mk p'<VAR>hip : HasLiftingProperty i p<GOAL>HasLiftingProperty i p'
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>A✝ B✝ B' X✝ Y✝ Y'✝ : C<VAR>i✝ : A✝ ⟶ B✝<VAR>i' : B✝ ⟶ B'<VAR>p✝ : X✝ ⟶ Y✝<VAR>p'✝ : Y✝ ⟶ Y'✝<VAR>A B X Y X' Y' : C<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>p' : X' ⟶ Y'<VAR>e : Arrow.mk p ≅ Arrow.mk p'<VAR>hip : HasLiftingProperty i p<GOAL>HasLiftingProperty i (e.inv.left ≫ p ≫ e.hom.right)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>h : Presieve.IsSheaf J F<GOAL>Presieve.IsSheaf J G.toPresheaf ↔ ∀ (U : Cᵒᵖ) (s : F.obj U), G.sieveOfSection s ∈ J.sieves (unop U) → s ∈ G.obj U
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>h : Presieve.IsSheaf J F<GOAL>G = sheafify J G ↔ ∀ (U : Cᵒᵖ) (s : F.obj U), G.sieveOfSection s ∈ J.sieves (unop U) → s ∈ G.obj U
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>h : Presieve.IsSheaf J F<GOAL>G = sheafify J G ↔ sheafify J G ≤ G
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>inst✝ : SFinite μ<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>hf : AEMeasurable f (μ.restrict s)<VAR>g : α → ℝ≥0∞<VAR>h'f : ∀ᵐ (x : α) ∂μ.restrict s, f x < ⊤<GOAL>∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>a b x y z : α<VAR>h : IsCompl y z<GOAL>Disjoint x y ↔ x ≤ z
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>l : List α<VAR>ih : indexOf a l = l.length ↔ ¬a ∈ l<GOAL>indexOf a (b :: l) = (b :: l).length ↔ ¬a ∈ b :: l
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>l : List α<VAR>ih : indexOf a l = l.length ↔ ¬a ∈ l<GOAL>(bif b == a then 0 else indexOf a l + 1) = l.length + 1 ↔ ¬(a = b ∨ a ∈ l)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>l : List α<VAR>ih : indexOf a l = l.length ↔ ¬a ∈ l<GOAL>(if (b == a) = true then 0 else indexOf a l + 1) = l.length + 1 ↔ ¬(a = b ∨ a ∈ l)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>q : ℕ<VAR>hF : ExpChar F q<GOAL>IsPurelyInseparable F E ↔ ∀ (x : E), ∃ n y, minpoly F x = X ^ q ^ n - C y
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>inst✝ : IsProbabilityMeasure μ<VAR>hf : PreErgodic f μ<VAR>hs : MeasurableSet s<VAR>hs' : f ⁻¹' s = s<GOAL>μ s = 0 ∨ μ s = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>d : α<GOAL>Primrec₂ fun l n => l.getD n d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>d : α<GOAL>Primrec₂ fun l n => (l.get? n).getD d
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : InnerProductSpace ℝ F<VAR>K : Set F<VAR>ne : K.Nonempty<VAR>h₁ : IsComplete K<VAR>h₂ : Convex ℝ K<VAR>u : F<VAR>δ : ℝ := ⨅ w, ‖u - ↑w‖<GOAL>∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : InnerProductSpace ℝ F<VAR>K : Set F<VAR>ne : K.Nonempty<VAR>h₁ : IsComplete K<VAR>h₂ : Convex ℝ K<VAR>u : F<VAR>δ : ℝ := ⨅ w, ‖u - ↑w‖<VAR>this : Nonempty ↑K := Set.Nonempty.to_subtype ne<GOAL>∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : InnerProductSpace ℝ F<VAR>K : Set F<VAR>ne : K.Nonempty<VAR>h₁ : IsComplete K<VAR>h₂ : Convex ℝ K<VAR>u : F<VAR>δ : ℝ := ⨅ w, ‖u - ↑w‖<VAR>this : Nonempty ↑K := Set.Nonempty.to_subtype ne<VAR>zero_le_δ : 0 ≤ δ<GOAL>∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : InnerProductSpace ℝ F<VAR>K : Set F<VAR>ne : K.Nonempty<VAR>h₁ : IsComplete K<VAR>h₂ : Convex ℝ K<VAR>u : F<VAR>δ : ℝ := ⨅ w, ‖u - ↑w‖<VAR>this : Nonempty ↑K := Set.Nonempty.to_subtype ne<VAR>zero_le_δ : 0 ≤ δ<VAR>δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖<GOAL>∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : InnerProductSpace ℝ F<VAR>K : Set F<VAR>ne : K.Nonempty<VAR>h₁ : IsComplete K<VAR>h₂ : Convex ℝ K<VAR>u : F<VAR>δ : ℝ := ⨅ w, ‖u - ↑w‖<VAR>this : Nonempty ↑K := Set.Nonempty.to_subtype ne<VAR>zero_le_δ : 0 ≤ δ<VAR>δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖<VAR>δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖<GOAL>∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : InnerProductSpace ℝ F<VAR>K : Set F<VAR>ne : K.Nonempty<VAR>h₁ : IsComplete K<VAR>h₂ : Convex ℝ K<VAR>u : F<VAR>δ : ℝ := ⨅ w, ‖u - ↑w‖<VAR>this : Nonempty ↑K := Set.Nonempty.to_subtype ne<VAR>zero_le_δ : 0 ≤ δ<VAR>δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖<VAR>δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖<VAR>exists_seq : ∃ w, ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)<GOAL>∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : InnerProductSpace ℝ F<VAR>K : Set F<VAR>ne : K.Nonempty<VAR>h₁ : IsComplete K<VAR>h₂ : Convex ℝ K<VAR>u : F<VAR>δ : ℝ := ⨅ w, ‖u - ↑w‖<VAR>this : Nonempty ↑K := Set.Nonempty.to_subtype ne<VAR>zero_le_δ : 0 ≤ δ<VAR>δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖<VAR>δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖<VAR>w : ℕ → ↑K<VAR>hw : ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)<GOAL>∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : InnerProductSpace ℝ F<VAR>K : Set F<VAR>ne : K.Nonempty<VAR>h₁ : IsComplete K<VAR>h₂ : Convex ℝ K<VAR>u : F<VAR>δ : ℝ := ⨅ w, ‖u - ↑w‖<VAR>this : Nonempty ↑K := Set.Nonempty.to_subtype ne<VAR>zero_le_δ : 0 ≤ δ<VAR>δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖<VAR>δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖<VAR>w : ℕ → ↑K<VAR>hw : ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)<VAR>norm_tendsto : Tendsto (fun n => ‖u - ↑(w n)‖) atTop (𝓝 δ)<GOAL>∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : InnerProductSpace ℝ F<VAR>K : Set F<VAR>ne : K.Nonempty<VAR>h₁ : IsComplete K<VAR>h₂ : Convex ℝ K<VAR>u : F<VAR>δ : ℝ := ⨅ w, ‖u - ↑w‖<VAR>this : Nonempty ↑K := Set.Nonempty.to_subtype ne<VAR>zero_le_δ : 0 ≤ δ<VAR>δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖<VAR>δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖<VAR>w : ℕ → ↑K<VAR>hw : ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)<VAR>norm_tendsto : Tendsto (fun n => ‖u - ↑(w n)‖) atTop (𝓝 δ)<VAR>seq_is_cauchy : CauchySeq fun n => ↑(w n)<GOAL>∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖