ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>R : P.M α → P.M α → Prop<VAR>h₀ : Equivalence R<VAR>x y : P.M α<VAR>ax : P.A<VAR>fx fy : P.B ax ⟹ α ::: P.M α<VAR>h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy<VAR>Hdrop : dropFun fx = dropFun fy<GOAL>⟨ax, fx⟩ = ⟨ax, splitFun (dropFun fx) (lastFun fx)⟩ ∧ ⟨ax, fy⟩ = ⟨ax, splitFun (dropFun fx) (lastFun fy)⟩ ∧ ∀ (i : (P.B ax).last), R (lastFun fx i) (lastFun fy i)
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>R : P.M α → P.M α → Prop<VAR>h₀ : Equivalence R<VAR>x y : P.M α<VAR>ax : P.A<VAR>fx fy : P.B ax ⟹ α ::: P.M α<VAR>h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy<VAR>Hdrop : dropFun fx = dropFun fy<GOAL>⟨ax, fx⟩ = ⟨ax, fx⟩ ∧ ⟨ax, fy⟩ = ⟨ax, fy⟩ ∧ ∀ (i : (P.B ax).last), R (lastFun fx i) (lastFun fy i)
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>R : P.M α → P.M α → Prop<VAR>h₀ : Equivalence R<VAR>x y : P.M α<VAR>ax : P.A<VAR>fx fy : P.B ax ⟹ α ::: P.M α<VAR>h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy<VAR>Hdrop : dropFun fx = dropFun fy<GOAL>∀ (i : (P.B ax).last), R (lastFun fx i) (lastFun fy i)
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>R : P.M α → P.M α → Prop<VAR>h₀ : Equivalence R<VAR>x y : P.M α<VAR>ax : P.A<VAR>fx fy : P.B ax ⟹ α ::: P.M α<VAR>Hdrop : dropFun fx = dropFun fy<VAR>i : (P.B ax).last<VAR>h₁ : Quot.mk R (fx Fin2.fz i) = Quot.mk R (fy Fin2.fz i)<GOAL>R (lastFun fx i) (lastFun fy i)
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>R : P.M α → P.M α → Prop<VAR>h₀ : Equivalence R<VAR>x y : P.M α<VAR>ax : P.A<VAR>fx fy : P.B ax ⟹ α ::: P.M α<VAR>Hdrop : dropFun fx = dropFun fy<VAR>i : (P.B ax).last<VAR>h₁ : EqvGen R (fx Fin2.fz i) (fy Fin2.fz i)<GOAL>R (lastFun fx i) (lastFun fy i)
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>R : P.M α → P.M α → Prop<VAR>h₀ : Equivalence R<VAR>x y : P.M α<VAR>ax : P.A<VAR>fx fy : P.B ax ⟹ α ::: P.M α<VAR>Hdrop : dropFun fx = dropFun fy<VAR>i : (P.B ax).last<VAR>h₁ : R (fx Fin2.fz i) (fy Fin2.fz i)<GOAL>R (lastFun fx i) (lastFun fy i)
<VAR>E : Type uE<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<GOAL>support ↑f ⊆ (chartAt H c).source
<VAR>E : Type uE<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<GOAL>(extChartAt I c).source ∩ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) f.rOut ⊆ (extChartAt I c).source
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : List α<GOAL>l.sublists' = foldr (fun a r => sublists'Aux a r r) [[]] l
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : List α<GOAL>(foldr (fun a arr => Array.foldl (fun r l => r.push (a :: l)) arr arr 0) #[[]] l).toList = foldr (fun a r => (Array.foldl (fun r l => r.push (a :: l)) (toArray r) (toArray r) 0).toList) [[]] l
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : List α<GOAL>foldr ?g₂ #[[]].toList l = foldr (fun a r => (Array.foldl (fun r l => r.push (a :: l)) (toArray r) (toArray r) 0).toList) [[]] l
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : List α<GOAL>α → List (List α) → List (List α)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : List α<GOAL>∀ (x : α) (y : Array (List α)), ?g₂ x y.toList = (Array.foldl (fun r l => r.push (x :: l)) y y 0).toList
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_3<VAR>l l' la : Filter α<VAR>lb : Filter β<VAR>p : α → Prop<GOAL>(∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, p x) ↔ ∀ᶠ (x : α) in l, p x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype m<VAR>inst✝ : Fintype n<VAR>M₁₁ : Matrix m m R<VAR>M₁₂ : Matrix m n R<VAR>M₂₁ : Matrix n m R<VAR>M₂₂ M : Matrix n n R<VAR>i j : n<GOAL>M.charmatrix i i = X - C (M i i)
<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 : Submodule 𝕜 E<VAR>inst✝¹ : HasOrthogonalProjection K<VAR>U : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection U<VAR>y : E<GOAL>‖y - ↑((orthogonalProjection U) y)‖ = ⨅ x, ‖y - ↑x‖
<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 : Submodule 𝕜 E<VAR>inst✝¹ : HasOrthogonalProjection K<VAR>U : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection U<VAR>y : E<GOAL>∀ w ∈ U, ⟪y - ↑((orthogonalProjection U) y), w⟫_𝕜 = 0
<VAR>q✝ : ℚ<VAR>x y : ℝ<VAR>h : Irrational x<VAR>q : ℚ<VAR>hq : q ≠ 0<GOAL>Irrational (x * ↑q * ↑q⁻¹)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hX : autoParam (X ⊆ M.E) _auto✝<GOAL>M.Basis' I X ↔ M.Basis I X
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : StrictOrderedSemiring α<VAR>inst✝ : Archimedean α<VAR>y x : α<VAR>n : ℕ<VAR>hn : x < n • 1<GOAL>x < ↑n
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>i j : (Quotient.out (aleph 1).ord).α<VAR>h : i ≤ j<VAR>x : Set α<VAR>hx : x ∈ generateMeasurableRec s i<GOAL>x ∈ generateMeasurableRec s j
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>i : (Quotient.out (aleph 1).ord).α<VAR>x : Set α<VAR>hx : x ∈ generateMeasurableRec s i<VAR>h : i ≤ i<GOAL>x ∈ generateMeasurableRec s i
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>i j : (Quotient.out (aleph 1).ord).α<VAR>h✝ : i ≤ j<VAR>x : Set α<VAR>hx : x ∈ generateMeasurableRec s i<VAR>h : i < j<GOAL>x ∈ generateMeasurableRec s j
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>r : ℝ<VAR>x : (𝓞 K)ˣ<VAR>hr : 0 ≤ r<VAR>h : ‖(logEmbedding K) x‖ ≤ r<VAR>w : InfinitePlace K<GOAL>|Real.log (w ((algebraMap (𝓞 K) K) ↑x))| ≤ ↑(Fintype.card (InfinitePlace K)) * r
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>r : ℝ<VAR>x : (𝓞 K)ˣ<VAR>hr : 0 ≤ r<VAR>h : ‖(logEmbedding K) x‖ ≤ r<VAR>w : InfinitePlace K<VAR>tool : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑w.mult * x<GOAL>|Real.log (w ((algebraMap (𝓞 K) K) ↑x))| ≤ ↑(Fintype.card (InfinitePlace K)) * r
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>m : Ordnode α<VAR>y : α<VAR>r : Ordnode α<GOAL>(match l with | nil => 0 | node sz l x r => sz) + (((match m with | nil => 0 | node sz l x r => sz) + match r with | nil => 0 | node sz l x r => sz) + 1) + 1 = (((match l with | nil => 0 | node sz l x r => sz) + match m with | nil => 0 | node sz l x r => sz) + match r with | nil => 0 | node sz l x r => sz) + 2
<VAR>e₁ : ONote<VAR>n₁ : ℕ+<VAR>a₁ : ONote<VAR>b₁ : Ordinal.{0}<VAR>h₁ : (e₁.oadd n₁ a₁).NFBelow b₁<VAR>e₂ : ONote<VAR>n₂ : ℕ+<VAR>a₂ : ONote<VAR>b₂ : Ordinal.{0}<VAR>h₂ : (e₂.oadd n₂ a₂).NFBelow b₂<GOAL>(e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).NFBelow (e₁.repr + b₂)
<VAR>e₁ : ONote<VAR>n₁ : ℕ+<VAR>a₁ : ONote<VAR>b₁ : Ordinal.{0}<VAR>h₁ : (e₁.oadd n₁ a₁).NFBelow b₁<VAR>e₂ : ONote<VAR>n₂ : ℕ+<VAR>a₂ : ONote<VAR>b₂ : Ordinal.{0}<VAR>h₂ : (e₂.oadd n₂ a₂).NFBelow b₂<VAR>IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)<GOAL>(e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).NFBelow (e₁.repr + b₂)
<VAR>e₁ : ONote<VAR>n₁ : ℕ+<VAR>a₁ : ONote<VAR>b₁ : Ordinal.{0}<VAR>h₁ : (e₁.oadd n₁ a₁).NFBelow b₁<VAR>e₂ : ONote<VAR>n₂ : ℕ+<VAR>a₂ : ONote<VAR>b₂ : Ordinal.{0}<VAR>h₂ : (e₂.oadd n₂ a₂).NFBelow b₂<VAR>IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)<VAR>e0 : e₂ = 0<GOAL>(e₁.oadd (n₁ * n₂) a₁).NFBelow (e₁.repr + b₂)
<VAR>e₁ : ONote<VAR>n₁ : ℕ+<VAR>a₁ : ONote<VAR>b₁ : Ordinal.{0}<VAR>h₁ : (e₁.oadd n₁ a₁).NFBelow b₁<VAR>e₂ : ONote<VAR>n₂ : ℕ+<VAR>a₂ : ONote<VAR>b₂ : Ordinal.{0}<VAR>h₂ : (e₂.oadd n₂ a₂).NFBelow b₂<VAR>IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)<VAR>e0 : ¬e₂ = 0<GOAL>((e₁ + e₂).oadd n₂ (e₁.oadd n₁ a₁ * a₂)).NFBelow (e₁.repr + b₂)
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>p q : Submodule R E<VAR>S : Type u_5<VAR>inst✝² : Semiring S<VAR>M : Type u_6<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module S M<VAR>m : Submodule S M<VAR>f : E →ₗ[R] E<VAR>h : IsProj p f<GOAL>f = ↑(p.prodEquivOfIsCompl (ker f) ⋯) ∘ₗ id.prodMap 0 ∘ₗ ↑(p.prodEquivOfIsCompl (ker f) ⋯).symm
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>p q : Submodule R E<VAR>S : Type u_5<VAR>inst✝² : Semiring S<VAR>M : Type u_6<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module S M<VAR>m : Submodule S M<VAR>f : E →ₗ[R] E<VAR>h : IsProj p f<GOAL>f ∘ₗ ↑(p.prodEquivOfIsCompl (ker f) ⋯) = ↑(p.prodEquivOfIsCompl (ker f) ⋯) ∘ₗ id.prodMap 0
<VAR>R : Type u_1<VAR>inst✝ : Field R<VAR>f : R⟦X⟧<VAR>h : ¬(constantCoeff R) f = 0<GOAL>(d⁄dX R) f⁻¹ = -f⁻¹ ^ 2 * (d⁄dX R) f
<VAR>R : Type u_1<VAR>inst✝ : Field R<VAR>f : R⟦X⟧<VAR>h : ¬(constantCoeff R) f = 0<GOAL>f⁻¹ * f = 1
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>h : IsUnit A.det<GOAL>IsUnit Aᵀ.det
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>h : IsUnit A.det<GOAL>IsUnit A.det
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>p : ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν + (1 - (2 * n) • X) * ∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν + n ^ 2 • X ^ 2 * ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν = ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν + (1 - (2 * n) • X) * ∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν + n ^ 2 • X ^ 2 * ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν<GOAL>∑ ν ∈ Finset.range (n + 1), (n • X - ↑ν) ^ 2 * bernsteinPolynomial R n ν = n • X * (1 - X)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>p : ∑ x ∈ Finset.range (n + 1), (↑(x * (x - 1)) + (1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x = ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν + (1 - (2 * n) • X) * ∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν + n ^ 2 • X ^ 2 * ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν<GOAL>∑ ν ∈ Finset.range (n + 1), (n • X - ↑ν) ^ 2 * bernsteinPolynomial R n ν = n • X * (1 - X)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>p : ∑ x ∈ Finset.range (n + 1), (↑(x * (x - 1)) + (1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x = ↑(n * (n - 1)) * X ^ 2 + (1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1<GOAL>∑ ν ∈ Finset.range (n + 1), (n • X - ↑ν) ^ 2 * bernsteinPolynomial R n ν = n • X * (1 - X)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>p : ∑ x ∈ Finset.range (n + 1), (↑(x * (x - 1)) + (1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x = ↑(n * (n - 1)) * X ^ 2 + (1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1<VAR>k : ℕ<VAR>m : k ∈ Finset.range (n + 1)<GOAL>(n • X - ↑k) ^ 2 * bernsteinPolynomial R n k = (↑(k * (k - 1)) + (1 - ↑(2 * n) * X) * ↑k + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n k
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>p : ∑ x ∈ Finset.range (n + 1), (↑(x * (x - 1)) + (1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x = ↑(n * (n - 1)) * X ^ 2 + (1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1<GOAL>↑(n * (n - 1)) * X ^ 2 + (1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1 = n • X * (1 - X)
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u_1<VAR>x : (i : Fin n) → α i.castSucc<VAR>xₙ : α (last n)<VAR>s : (i : Fin n) → Finset (α i.castSucc)<VAR>sₙ : Finset (α (last n))<GOAL>snoc x xₙ ∈ piFinset (snoc s sₙ) ↔ x ∈ piFinset s ∧ xₙ ∈ sₙ
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>V : Set (α × α)<VAR>h : V ∈ 𝓤 α<GOAL>symmetrizeRel V ∈ 𝓤 α
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>V : Set (α × α)<VAR>h : V ∈ 𝓤 α<GOAL>Prod.swap ⁻¹' V ∈ (𝓤 α).sets
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>V : Set (α × α)<VAR>h : V ∈ 𝓤 α<GOAL>Prod.swap '' V ∈ (Prod.swap <$> 𝓤 α).sets
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>h : s ∈ 𝔖<GOAL>map (fun x => ((⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖)) x.1, (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖)) x.2)) (𝓤 (α →ᵤ[𝔖] β)) ≤ 𝓤 (↑s →ᵤ β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>h : s ∈ 𝔖<GOAL>⨅ i ∈ 𝔖, 𝓤 (α →ᵤ[𝔖] β) ≤ comap (fun x => ((⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖)) x.1, (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖)) x.2)) (𝓤 (↑s →ᵤ β))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l✝ : Filter α<VAR>inst✝ : PartialOrder β<VAR>l : Filter α<VAR>f g : α → β<GOAL>f =ᶠ[l] g ↔ f ≤ᶠ[l] g ∧ g ≤ᶠ[l] f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : UniformSpace γ<VAR>e : β → α<VAR>h_e : UniformInducing e<VAR>h_dense : DenseRange e<VAR>f : β → γ<VAR>h_f : UniformContinuous f<VAR>inst✝ : CompleteSpace γ<VAR>d : Set (γ × γ)<VAR>hd : d ∈ 𝓤 γ<VAR>s : Set (γ × γ)<VAR>hs : s ∈ 𝓤 γ<VAR>hs_comp : s ○ (s ○ s) ⊆ d<VAR>h_pnt : ∀ {a : α} {m : Set α}, m ∈ 𝓝 a → ∃ c ∈ f '' (e ⁻¹' m), (c, ⋯.extend f a) ∈ s ∧ (⋯.extend f a, c) ∈ s<VAR>this : Prod.map f f ⁻¹' s ∈ 𝓤 β<GOAL>Prod.map f f ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : UniformSpace γ<VAR>e : β → α<VAR>h_e : UniformInducing e<VAR>h_dense : DenseRange e<VAR>f : β → γ<VAR>h_f : UniformContinuous f<VAR>inst✝ : CompleteSpace γ<VAR>d : Set (γ × γ)<VAR>hd : d ∈ 𝓤 γ<VAR>s : Set (γ × γ)<VAR>hs : s ∈ 𝓤 γ<VAR>hs_comp : s ○ (s ○ s) ⊆ d<VAR>h_pnt : ∀ {a : α} {m : Set α}, m ∈ 𝓝 a → ∃ c ∈ f '' (e ⁻¹' m), (c, ⋯.extend f a) ∈ s ∧ (⋯.extend f a, c) ∈ s<VAR>this✝ : Prod.map f f ⁻¹' s ∈ 𝓤 β<VAR>this : Prod.map f f ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α)<VAR>t : Set (α × α)<VAR>ht : t ∈ 𝓤 α<VAR>ts : Prod.map e e ⁻¹' t ⊆ Prod.map f f ⁻¹' s<VAR>x✝ : α × α<VAR>x₁ x₂ : α<VAR>hx_t : (x₁, x₂) ∈ interior t<GOAL>(x₁, x₂) ∈ Prod.map (⋯.extend f) (⋯.extend f) ⁻¹' d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : UniformSpace γ<VAR>e : β → α<VAR>h_e : UniformInducing e<VAR>h_dense : DenseRange e<VAR>f : β → γ<VAR>h_f : UniformContinuous f<VAR>inst✝ : CompleteSpace γ<VAR>d : Set (γ × γ)<VAR>hd : d ∈ 𝓤 γ<VAR>s : Set (γ × γ)<VAR>hs : s ∈ 𝓤 γ<VAR>hs_comp : s ○ (s ○ s) ⊆ d<VAR>h_pnt : ∀ {a : α} {m : Set α}, m ∈ 𝓝 a → ∃ c ∈ f '' (e ⁻¹' m), (c, ⋯.extend f a) ∈ s ∧ (⋯.extend f a, c) ∈ s<VAR>this✝¹ : Prod.map f f ⁻¹' s ∈ 𝓤 β<VAR>this✝ : Prod.map f f ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α)<VAR>t : Set (α × α)<VAR>ht : t ∈ 𝓤 α<VAR>ts : Prod.map e e ⁻¹' t ⊆ Prod.map f f ⁻¹' s<VAR>x✝ : α × α<VAR>x₁ x₂ : α<VAR>hx_t : (x₁, x₂) ∈ interior t<VAR>this : interior t ∈ 𝓝 (x₁, x₂)<GOAL>(x₁, x₂) ∈ Prod.map (⋯.extend f) (⋯.extend f) ⁻¹' d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : UniformSpace γ<VAR>e : β → α<VAR>h_e : UniformInducing e<VAR>h_dense : DenseRange e<VAR>f : β → γ<VAR>h_f : UniformContinuous f<VAR>inst✝ : CompleteSpace γ<VAR>d : Set (γ × γ)<VAR>hd : d ∈ 𝓤 γ<VAR>s : Set (γ × γ)<VAR>hs : s ∈ 𝓤 γ<VAR>hs_comp : s ○ (s ○ s) ⊆ d<VAR>h_pnt : ∀ {a : α} {m : Set α}, m ∈ 𝓝 a → ∃ c ∈ f '' (e ⁻¹' m), (c, ⋯.extend f a) ∈ s ∧ (⋯.extend f a, c) ∈ s<VAR>this✝¹ : Prod.map f f ⁻¹' s ∈ 𝓤 β<VAR>this✝ : Prod.map f f ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α)<VAR>t : Set (α × α)<VAR>ht : t ∈ 𝓤 α<VAR>ts : Prod.map e e ⁻¹' t ⊆ Prod.map f f ⁻¹' s<VAR>x✝ : α × α<VAR>x₁ x₂ : α<VAR>hx_t : (x₁, x₂) ∈ interior t<VAR>this : interior t ∈ 𝓝 (x₁, x₂)<VAR>m₁ : Set α<VAR>hm₁ : m₁ ∈ 𝓝 x₁<VAR>m₂ : Set α<VAR>hm₂ : m₂ ∈ 𝓝 x₂<VAR>hm : m₁ ×ˢ m₂ ⊆ interior t<GOAL>(x₁, x₂) ∈ Prod.map (⋯.extend f) (⋯.extend f) ⁻¹' d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : UniformSpace γ<VAR>e : β → α<VAR>h_e : UniformInducing e<VAR>h_dense : DenseRange e<VAR>f : β → γ<VAR>h_f : UniformContinuous f<VAR>inst✝ : CompleteSpace γ<VAR>d : Set (γ × γ)<VAR>hd : d ∈ 𝓤 γ<VAR>s : Set (γ × γ)<VAR>hs : s ∈ 𝓤 γ<VAR>hs_comp : s ○ (s ○ s) ⊆ d<VAR>h_pnt : ∀ {a : α} {m : Set α}, m ∈ 𝓝 a → ∃ c ∈ f '' (e ⁻¹' m), (c, ⋯.extend f a) ∈ s ∧ (⋯.extend f a, c) ∈ s<VAR>this✝¹ : Prod.map f f ⁻¹' s ∈ 𝓤 β<VAR>this✝ : Prod.map f f ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α)<VAR>t : Set (α × α)<VAR>ht : t ∈ 𝓤 α<VAR>ts : Prod.map e e ⁻¹' t ⊆ Prod.map f f ⁻¹' s<VAR>x✝ : α × α<VAR>x₁ x₂ : α<VAR>hx_t : (x₁, x₂) ∈ interior t<VAR>this : interior t ∈ 𝓝 (x₁, x₂)<VAR>m₁ : Set α<VAR>hm₁ : m₁ ∈ 𝓝 x₁<VAR>m₂ : Set α<VAR>hm₂ : m₂ ∈ 𝓝 x₂<VAR>hm : m₁ ×ˢ m₂ ⊆ interior t<VAR>a : β<VAR>ha₁ : a ∈ e ⁻¹' m₁<VAR>left✝ : (f a, ⋯.extend f x₁) ∈ s<VAR>ha₂ : (⋯.extend f x₁, f a) ∈ s<VAR>b : β<VAR>hb₁ : b ∈ e ⁻¹' m₂<VAR>hb₂ : (f b, ⋯.extend f x₂) ∈ s<VAR>right✝ : (⋯.extend f x₂, f b) ∈ s<GOAL>(x₁, x₂) ∈ Prod.map (⋯.extend f) (⋯.extend f) ⁻¹' d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : UniformSpace γ<VAR>e : β → α<VAR>h_e : UniformInducing e<VAR>h_dense : DenseRange e<VAR>f : β → γ<VAR>h_f : UniformContinuous f<VAR>inst✝ : CompleteSpace γ<VAR>d : Set (γ × γ)<VAR>hd : d ∈ 𝓤 γ<VAR>s : Set (γ × γ)<VAR>hs : s ∈ 𝓤 γ<VAR>hs_comp : s ○ (s ○ s) ⊆ d<VAR>h_pnt : ∀ {a : α} {m : Set α}, m ∈ 𝓝 a → ∃ c ∈ f '' (e ⁻¹' m), (c, ⋯.extend f a) ∈ s ∧ (⋯.extend f a, c) ∈ s<VAR>this✝² : Prod.map f f ⁻¹' s ∈ 𝓤 β<VAR>this✝¹ : Prod.map f f ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α)<VAR>t : Set (α × α)<VAR>ht : t ∈ 𝓤 α<VAR>ts : Prod.map e e ⁻¹' t ⊆ Prod.map f f ⁻¹' s<VAR>x✝ : α × α<VAR>x₁ x₂ : α<VAR>hx_t : (x₁, x₂) ∈ interior t<VAR>this✝ : interior t ∈ 𝓝 (x₁, x₂)<VAR>m₁ : Set α<VAR>hm₁ : m₁ ∈ 𝓝 x₁<VAR>m₂ : Set α<VAR>hm₂ : m₂ ∈ 𝓝 x₂<VAR>hm : m₁ ×ˢ m₂ ⊆ interior t<VAR>a : β<VAR>ha₁ : a ∈ e ⁻¹' m₁<VAR>left✝ : (f a, ⋯.extend f x₁) ∈ s<VAR>ha₂ : (⋯.extend f x₁, f a) ∈ s<VAR>b : β<VAR>hb₁ : b ∈ e ⁻¹' m₂<VAR>hb₂ : (f b, ⋯.extend f x₂) ∈ s<VAR>right✝ : (⋯.extend f x₂, f b) ∈ s<VAR>this : Prod.map f f (a, b) ∈ s<GOAL>(x₁, x₂) ∈ Prod.map (⋯.extend f) (⋯.extend f) ⁻¹' d
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : LinearOrderedRing R<VAR>inst✝⁴ : FloorRing R<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : OrderTopology R<VAR>inst✝¹ : MeasurableSpace R<VAR>inst✝ : BorelSpace R<VAR>s : Set R<VAR>hs : MeasurableSet s<GOAL>MeasurableSet (Int.fract '' s)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : LinearOrderedRing R<VAR>inst✝⁴ : FloorRing R<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : OrderTopology R<VAR>inst✝¹ : MeasurableSpace R<VAR>inst✝ : BorelSpace R<VAR>s : Set R<VAR>hs : MeasurableSet s<GOAL>MeasurableSet (⋃ m, (fun x => x + ↑m) ⁻¹' s ∩ Ico 0 1)
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>x : E<VAR>r : ℝ<VAR>hr : r ≠ 0<GOAL>closure (ball x r) = closedBall x r
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>x : E<VAR>r : ℝ<VAR>hr : r ≠ 0<VAR>y : E<VAR>hy : y ∈ closedBall x r<GOAL>y ∈ closure (ball x r)
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>x : E<VAR>r : ℝ<VAR>hr : r ≠ 0<VAR>y : E<VAR>hy : y ∈ closedBall x r<VAR>this : ContinuousWithinAt (fun c => c • (y - x) + x) (Ico 0 1) 1<GOAL>y ∈ closure (ball x r)
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>x : E<VAR>r : ℝ<VAR>hr : r ≠ 0<VAR>y : E<VAR>hy : y ∈ closedBall x r<VAR>this : ContinuousWithinAt (fun c => c • (y - x) + x) (Ico 0 1) 1<GOAL>y = 1 • (y - x) + x
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>x : E<VAR>r : ℝ<VAR>hr : r ≠ 0<VAR>y : E<VAR>hy : y ∈ closedBall x r<VAR>this : ContinuousWithinAt (fun c => c • (y - x) + x) (Ico 0 1) 1<GOAL>1 ∈ closure (Ico 0 1)
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>x : E<VAR>r : ℝ<VAR>hr : r ≠ 0<VAR>y : E<VAR>hy : y ∈ closedBall x r<VAR>this : ContinuousWithinAt (fun c => c • (y - x) + x) (Ico 0 1) 1<GOAL>MapsTo (fun c => c • (y - x) + x) (Ico 0 1) (ball x r)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : CommRing R<VAR>a b : R<GOAL>(a - b) ^ 2 = a ^ 2 - 2 * a * b + b ^ 2
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CanonicallyOrderedAddCommMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>b : A<VAR>n i : ι<VAR>h : ¬i ≤ n<VAR>a : ↥(𝒜 i)<GOAL>↑(((decompose 𝒜) (↑a * b)) n) = 0
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>N : ℕ<VAR>inst✝ : NeZero N<VAR>j : ZMod N<GOAL>toAddCircle j = ↑(↑j.val / ↑N)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>Y Z : C<VAR>inst✝ : HasLeftDual Z<VAR>f : Y ⟶ ᘁZ<GOAL>(λ_ Y).inv ≫ η_ (ᘁZ) Z ▷ Y ≫ (α_ (ᘁZ) Z Y).hom ≫ ᘁZ ◁ (Z ◁ f ≫ ε_ (ᘁZ) Z) = 𝟙 Y ⊗≫ (η_ (ᘁZ) Z ▷ Y ≫ (ᘁZ ⊗ Z) ◁ f) ⊗≫ ᘁZ ◁ ε_ (ᘁZ) Z
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>Y Z : C<VAR>inst✝ : HasLeftDual Z<VAR>f : Y ⟶ ᘁZ<GOAL>𝟙 Y ⊗≫ (η_ (ᘁZ) Z ▷ Y ≫ (ᘁZ ⊗ Z) ◁ f) ⊗≫ ᘁZ ◁ ε_ (ᘁZ) Z = f ⊗≫ η_ (ᘁZ) Z ▷ ᘁZ ⊗≫ ᘁZ ◁ ε_ (ᘁZ) Z
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>Y Z : C<VAR>inst✝ : HasLeftDual Z<VAR>f : Y ⟶ ᘁZ<GOAL>𝟙 Y ⊗≫ (𝟙_ C ◁ f ≫ η_ (ᘁZ) Z ▷ ᘁZ) ⊗≫ ᘁZ ◁ ε_ (ᘁZ) Z = f ⊗≫ η_ (ᘁZ) Z ▷ ᘁZ ⊗≫ ᘁZ ◁ ε_ (ᘁZ) Z
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>Y Z : C<VAR>inst✝ : HasLeftDual Z<VAR>f : Y ⟶ ᘁZ<GOAL>f ⊗≫ η_ (ᘁZ) Z ▷ ᘁZ ⊗≫ ᘁZ ◁ ε_ (ᘁZ) Z = f ≫ (ρ_ ᘁZ).inv
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>Y Z : C<VAR>inst✝ : HasLeftDual Z<VAR>f : Y ⟶ ᘁZ<GOAL>f ⊗≫ ⊗𝟙 = f ≫ (ρ_ ᘁZ).inv
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : HeytingAlgebra α<VAR>a✝ b✝ c a b : α<GOAL>a ⇨ bᶜ = b ⇨ aᶜ
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>J✝ : Type v<VAR>inst✝ : HasFiniteLimits C<VAR>J : Type<VAR>x✝ : Finite J<GOAL>HasLimitsOfShape (WidePullbackShape J) C
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>J✝ : Type v<VAR>inst✝ : HasFiniteLimits C<VAR>J : Type<VAR>x✝ : Finite J<VAR>val✝ : Fintype J<GOAL>HasLimitsOfShape (WidePullbackShape J) C
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>inst✝² : FiniteDimensional ℝ F<VAR>inst✝¹ : MeasurableSpace F<VAR>inst✝ : BorelSpace F<VAR>m n : ℕ<VAR>_i : Fact (finrank ℝ F = n)<VAR>o : Orientation ℝ F (Fin n)<GOAL>o.volumeForm.measure = volume