ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ ψ θ : L.BoundedFormula α n<VAR>h1 : T.SemanticallyEquivalent φ ψ<VAR>h2 : T.SemanticallyEquivalent ψ θ<VAR>M : T.ModelType<VAR>v : α → ↑M<VAR>xs : Fin n → ↑M<VAR>h1' : φ.Realize v xs ↔ ψ.Realize v xs<VAR>h2' : ψ.Realize v xs ↔ θ.Realize v xs<GOAL>φ.Realize v xs ↔ θ.Realize v xs
<VAR>α : Type v<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>n : ℕ<VAR>m : M<VAR>a : α<GOAL>m ^ (n % period m a) • a = m ^ n • a
<VAR>α : Type u_1<VAR>inst✝⁶ : MeasurableSpace α<VAR>μ : Measure α<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>F : H → α → E<VAR>x₀ : H<VAR>bound : α → ℝ<VAR>ε : ℝ<VAR>F' : H → α → H →L[𝕜] E<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) μ<VAR>hF_int : Integrable (F x₀) μ<VAR>hF'_meas : AEStronglyMeasurable (F' x₀) μ<VAR>h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F' x a‖ ≤ bound a<VAR>bound_integrable : Integrable bound μ<VAR>h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, HasFDerivAt (fun x => F x a) (F' x a) x<VAR>this : NormedSpace ℝ H := NormedSpace.restrictScalars ℝ 𝕜 H<GOAL>HasFDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀
<VAR>α : Type u_1<VAR>inst✝⁶ : MeasurableSpace α<VAR>μ : Measure α<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>F : H → α → E<VAR>x₀ : H<VAR>bound : α → ℝ<VAR>ε : ℝ<VAR>F' : H → α → H →L[𝕜] E<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) μ<VAR>hF_int : Integrable (F x₀) μ<VAR>hF'_meas : AEStronglyMeasurable (F' x₀) μ<VAR>h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F' x a‖ ≤ bound a<VAR>bound_integrable : Integrable bound μ<VAR>h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, HasFDerivAt (fun x => F x a) (F' x a) x<VAR>this : NormedSpace ℝ H := NormedSpace.restrictScalars ℝ 𝕜 H<VAR>x₀_in : x₀ ∈ ball x₀ ε<GOAL>HasFDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀
<VAR>α : Type u_1<VAR>inst✝⁶ : MeasurableSpace α<VAR>μ : Measure α<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>F : H → α → E<VAR>x₀ : H<VAR>bound : α → ℝ<VAR>ε : ℝ<VAR>F' : H → α → H →L[𝕜] E<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) μ<VAR>hF_int : Integrable (F x₀) μ<VAR>hF'_meas : AEStronglyMeasurable (F' x₀) μ<VAR>h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F' x a‖ ≤ bound a<VAR>bound_integrable : Integrable bound μ<VAR>h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, HasFDerivAt (fun x => F x a) (F' x a) x<VAR>this✝ : NormedSpace ℝ H := NormedSpace.restrictScalars ℝ 𝕜 H<VAR>x₀_in : x₀ ∈ ball x₀ ε<VAR>diff_x₀ : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x => F x a) (F' x₀ a) x₀<VAR>this : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x => F x a) (ball x₀ ε)<GOAL>HasFDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : α<VAR>ts ys l : List α<GOAL>l ∈ (permutationsAux2 t ts [] ys fun x => [] ++ x).2 ↔ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l = l₁ ++ t :: l₂ ++ ts
<VAR>α : Type u<VAR>a : α<VAR>inst✝² : Group α<VAR>inst✝¹ : IsCyclic α<VAR>inst✝ : Fintype α<VAR>d : ℕ<VAR>hd : d ∣ Fintype.card α<GOAL>(filter (fun a => orderOf a = d) univ).card = φ d
<VAR>R : Type u<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>k n : ℕ<VAR>r : R<GOAL>X ^ k * (monomial n) r = (monomial (n + k)) r
<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>x y : E<VAR>hK : Dense ↑K<VAR>h : ∀ (v : ↥K), ⟪↑v, x⟫_𝕜 = 0<VAR>v : ↥K<GOAL>⟪↑v, x⟫_𝕜 = ⟪↑v, 0⟫_𝕜
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : DistribLattice α<VAR>inst✝² : LinearOrderedCommSemiring β<VAR>inst✝¹ : ExistsAddOfLE β<VAR>f f₁ f₂ f₃ f₄ g μ : α → β<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<GOAL>s.card * t.card ≤ (s ⊼ t).card * (s ⊻ t).card
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<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>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>x y z : L<GOAL>((traceForm R L M) ⁅x, y⁆) z = -((traceForm R L M) y) ⁅x, z⁆
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>I : MulticospanIndex C<VAR>K : Multifork I<VAR>b : I.R<GOAL>K.π.app (WalkingMulticospan.right b) = K.ι (I.fstTo b) ≫ I.fst b
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>I : MulticospanIndex C<VAR>K : Multifork I<VAR>b : I.R<GOAL>K.π.app (WalkingMulticospan.left (I.fstTo b)) ≫ I.multicospan.map (WalkingMulticospan.Hom.fst b) = K.ι (I.fstTo b) ≫ I.fst b
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.121497, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<VAR>h' : Homotopy φ₃ φ₄<GOAL>(φ₁ + φ₃).τ₁ = S₁.f ≫ (h.h₁ + h'.h₁) + (h.h₀ + h'.h₀) + (φ₂ + φ₄).τ₁
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.121497, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<VAR>h' : Homotopy φ₃ φ₄<GOAL>S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁ + (S₁.f ≫ h'.h₁ + h'.h₀ + φ₄.τ₁) = S₁.f ≫ h.h₁ + S₁.f ≫ h'.h₁ + (h.h₀ + h'.h₀) + (φ₂.τ₁ + φ₄.τ₁)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.121497, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<VAR>h' : Homotopy φ₃ φ₄<GOAL>(φ₁ + φ₃).τ₂ = S₁.g ≫ (h.h₂ + h'.h₂) + (h.h₁ + h'.h₁) ≫ S₂.f + (φ₂ + φ₄).τ₂
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.121497, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<VAR>h' : Homotopy φ₃ φ₄<GOAL>S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ + (S₁.g ≫ h'.h₂ + h'.h₁ ≫ S₂.f + φ₄.τ₂) = S₁.g ≫ h.h₂ + S₁.g ≫ h'.h₂ + (h.h₁ ≫ S₂.f + h'.h₁ ≫ S₂.f) + (φ₂.τ₂ + φ₄.τ₂)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.121497, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<VAR>h' : Homotopy φ₃ φ₄<GOAL>(φ₁ + φ₃).τ₃ = h.h₃ + h'.h₃ + (h.h₂ + h'.h₂) ≫ S₂.g + (φ₂ + φ₄).τ₃
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.121497, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<VAR>h' : Homotopy φ₃ φ₄<GOAL>h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃ + (h'.h₃ + h'.h₂ ≫ S₂.g + φ₄.τ₃) = h.h₃ + h'.h₃ + (h.h₂ ≫ S₂.g + h'.h₂ ≫ S₂.g) + (φ₂.τ₃ + φ₄.τ₃)
<VAR>R : Type u₁<VAR>inst✝¹ : CommSemiring R<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CharP R p<VAR>f : Ring.Perfection R p<VAR>n : ℕ<GOAL>(coeff R p (n + 1)) ((frobenius (Ring.Perfection R p) p) f) = (coeff R p n) f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>D' : Type u_3<VAR>inst✝⁴ : Category.{?u.202, u_1} C<VAR>inst✝³ : Category.{?u.206, u_2} D<VAR>inst✝² : Category.{?u.210, u_3} D'<VAR>W : MorphismProperty C<VAR>L : C ⥤ D<VAR>L' : C ⥤ D'<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : L'.IsLocalization W<VAR>X : C<VAR>f : StructuredArrow (L.obj X) L<GOAL>(fun f => StructuredArrow.mk ((homEquiv W L' L) f.hom)) ((fun f => StructuredArrow.mk ((homEquiv W L L') f.hom)) f) = f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>D' : Type u_3<VAR>inst✝⁴ : Category.{?u.202, u_1} C<VAR>inst✝³ : Category.{?u.206, u_2} D<VAR>inst✝² : Category.{?u.210, u_3} D'<VAR>W : MorphismProperty C<VAR>L : C ⥤ D<VAR>L' : C ⥤ D'<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : L'.IsLocalization W<VAR>X Y : C<VAR>f : L.obj X ⟶ L.obj Y<GOAL>(fun f => StructuredArrow.mk ((homEquiv W L' L) f.hom)) ((fun f => StructuredArrow.mk ((homEquiv W L L') f.hom)) (StructuredArrow.mk f)) = StructuredArrow.mk f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>D' : Type u_3<VAR>inst✝⁴ : Category.{?u.202, u_1} C<VAR>inst✝³ : Category.{?u.206, u_2} D<VAR>inst✝² : Category.{?u.210, u_3} D'<VAR>W : MorphismProperty C<VAR>L : C ⥤ D<VAR>L' : C ⥤ D'<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : L'.IsLocalization W<VAR>X Y : C<VAR>f : L.obj X ⟶ L.obj Y<GOAL>StructuredArrow.mk ((homEquiv W L' L) ((homEquiv W L L') f)) = StructuredArrow.mk f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>D' : Type u_3<VAR>inst✝⁴ : Category.{?u.202, u_1} C<VAR>inst✝³ : Category.{?u.206, u_2} D<VAR>inst✝² : Category.{?u.210, u_3} D'<VAR>W : MorphismProperty C<VAR>L : C ⥤ D<VAR>L' : C ⥤ D'<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : L'.IsLocalization W<VAR>X : C<VAR>f : StructuredArrow (L'.obj X) L'<GOAL>(fun f => StructuredArrow.mk ((homEquiv W L L') f.hom)) ((fun f => StructuredArrow.mk ((homEquiv W L' L) f.hom)) f) = f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>D' : Type u_3<VAR>inst✝⁴ : Category.{?u.202, u_1} C<VAR>inst✝³ : Category.{?u.206, u_2} D<VAR>inst✝² : Category.{?u.210, u_3} D'<VAR>W : MorphismProperty C<VAR>L : C ⥤ D<VAR>L' : C ⥤ D'<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : L'.IsLocalization W<VAR>X Y : C<VAR>f : L'.obj X ⟶ L'.obj Y<GOAL>(fun f => StructuredArrow.mk ((homEquiv W L L') f.hom)) ((fun f => StructuredArrow.mk ((homEquiv W L' L) f.hom)) (StructuredArrow.mk f)) = StructuredArrow.mk f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>D' : Type u_3<VAR>inst✝⁴ : Category.{?u.202, u_1} C<VAR>inst✝³ : Category.{?u.206, u_2} D<VAR>inst✝² : Category.{?u.210, u_3} D'<VAR>W : MorphismProperty C<VAR>L : C ⥤ D<VAR>L' : C ⥤ D'<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : L'.IsLocalization W<VAR>X Y : C<VAR>f : L'.obj X ⟶ L'.obj Y<GOAL>StructuredArrow.mk ((homEquiv W L L') ((homEquiv W L' L) f)) = StructuredArrow.mk f
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I : FractionalIdeal S P<GOAL>I.den • ↑I = Submodule.map (Algebra.linearMap R P) I.num
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I : FractionalIdeal S P<GOAL>⟨Exists.choose ⋯, ⋯⟩ • ↑I = LinearMap.range (Algebra.linearMap R P) ⊓ I.den • ↑I
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I : FractionalIdeal S P<GOAL>⟨Exists.choose ⋯, ⋯⟩ • ↑I ≤ LinearMap.range (Algebra.linearMap R P)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I : FractionalIdeal S P<VAR>a : P<VAR>ha : a ∈ ↑↑I<GOAL>(DistribMulAction.toLinearMap R P (S.subtype ⟨Exists.choose ⋯, ⋯⟩)) a ∈ LinearMap.range (Algebra.linearMap R P)
<VAR>R : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁶ : CommRing P<VAR>inst✝⁵ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝⁴ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R₁ K<VAR>inst✝¹ : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>x : P<VAR>I J : FractionalIdeal S P<GOAL>(∀ {zI : P}, zI ∈ I → zI ∈ spanSingleton S x * J) ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f₂ : 𝕜 → F<VAR>s₂ : Set 𝕜<VAR>n : ℕ<VAR>hs : UniqueDiffOn 𝕜 s₂<GOAL>ContDiffOn 𝕜 (↑(n + 1)) f₂ s₂ ↔ DifferentiableOn 𝕜 f₂ s₂ ∧ ContDiffOn 𝕜 (↑n) (derivWithin f₂ s₂) s₂
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f₂ : 𝕜 → F<VAR>s₂ : Set 𝕜<VAR>n : ℕ<VAR>hs : UniqueDiffOn 𝕜 s₂<GOAL>DifferentiableOn 𝕜 f₂ s₂ → (ContDiffOn 𝕜 (↑n) (fun y => fderivWithin 𝕜 f₂ s₂ y) s₂ ↔ ContDiffOn 𝕜 (↑n) (derivWithin f₂ s₂) s₂)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>M N : Matrix n n R<VAR>p : n → n<VAR>H : ¬Bijective p<GOAL>∑ σ : Perm n, ↑↑(sign σ) * ∏ x : n, M (σ x) (p x) * N (p x) x = 0
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>M N : Matrix n n R<VAR>p : n → n<VAR>H : ¬Bijective p<VAR>i j : n<VAR>hpij : p i = p j<VAR>hij : i ≠ j<GOAL>∑ σ : Perm n, ↑↑(sign σ) * ∏ x : n, M (σ x) (p x) * N (p x) x = 0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a✝ a₁ a₂ b✝ c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>a b : G<VAR>h : f (a⁻¹ * b) = 1<GOAL>f a = f b
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a✝ a₁ a₂ b✝ c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>a b : G<VAR>h : (f a)⁻¹ * f b = 1<GOAL>f a = f b
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a✝ a₁ a₂ b✝ c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>a b : G<VAR>h : (f a)⁻¹ * f b = 1<GOAL>(f a)⁻¹ = (f b)⁻¹
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a b c x : α<VAR>u : αˣ<VAR>y : α<GOAL>x = y /ₚ u ↔ x * ↑u = y
<VAR>n m : ℕ<VAR>a : Fin (n + 1)<VAR>ha : a ≠ 0<GOAL>(a.pred ha).castSucc < a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoid α<VAR>u : (Associates α)ˣ<GOAL>↑u = 1
<VAR>θ : Angle<GOAL>(-θ).sign = -θ.sign
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d✝ : ℝ<VAR>f : ℝ → E<VAR>hc : c ≠ 0<VAR>d : ℝ<GOAL>∫ (x : ℝ) in a..b, f (d - x / c) = c • ∫ (x : ℝ) in d - b / c..d - a / c, f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Preorder α<VAR>s t : Set α<GOAL>DirSupClosed sᶜ ↔ DirSupInacc s
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>H K : G.Subgraph<VAR>Hconn : H.Connected<VAR>Kconn : K.Connected<VAR>u v : V<VAR>uH : u ∈ H.verts<VAR>vK : v ∈ K.verts<VAR>huv : G.Adj u v<GOAL>(⊤.induce {u, v} ⊔ H ⊔ K).Connected
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>H K : G.Subgraph<VAR>Hconn : H.Connected<VAR>Kconn : K.Connected<VAR>u v : V<VAR>uH : u ∈ H.verts<VAR>vK : v ∈ K.verts<VAR>huv : G.Adj u v<GOAL>(⊤.induce {u, v} ⊓ H).verts.Nonempty
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>H K : G.Subgraph<VAR>Hconn : H.Connected<VAR>Kconn : K.Connected<VAR>u v : V<VAR>uH : u ∈ H.verts<VAR>vK : v ∈ K.verts<VAR>huv : G.Adj u v<GOAL>((⊤.induce {u, v} ⊔ H) ⊓ K).verts.Nonempty
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<VAR>t : Set (SeparationQuotient X)<GOAL>Filter.map mk (𝓝 x) = 𝓝 (mk x)
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>p : ℕ<VAR>inst✝ : ExpChar R p<VAR>x y : R<GOAL>x - y ∈ pNilradical R p ↔ ∃ n, x ^ p ^ n = y ^ p ^ n
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>L : Type u<VAR>inst✝² : Field L<VAR>f : K →+* L<VAR>a : L<VAR>S : Type u_1<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : Algebra S K[X]<VAR>p : S<GOAL>eval f a ((algebraMap S (RatFunc K)) p) = Polynomial.eval₂ f a ((algebraMap S K[X]) p)
<VAR>n : Nat<VAR>α : Sort u_1<VAR>f : Fin n → α → α<VAR>x : α<GOAL>foldl n (fun x i => f i.rev x) x = foldr n f x
<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>F : Type u_3<VAR>inst✝ : Field F<VAR>w : InfinitePlace K<VAR>x : K<GOAL>‖w.embedding x‖ = w x
<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>F : Type u_3<VAR>inst✝ : Field F<VAR>w : InfinitePlace K<VAR>x : K<GOAL>‖w.embedding x‖ = (mk w.embedding) x
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph α<VAR>inst✝¹ : Fintype (Sym2 α)<VAR>inst✝ : Semiring R<VAR>a b : α<VAR>e : Sym2 α<VAR>h : G.Adj a b<GOAL>(incMatrix R G * (incMatrix R G)ᵀ) a b = 1
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : DistribLattice α<VAR>x y z a b c : α<GOAL>(a ⊔ b) ⊓ c = a ⊓ c ⊔ b ⊓ c
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>K : Type u_3<VAR>V : Type u_4<VAR>V' : Type u_5<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>f : V →ₗ[K] V'<VAR>hf_inj : ker f = ⊥<VAR>B : Set V := Basis.ofVectorSpaceIndex K V<VAR>hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V<GOAL>∃ g, g ∘ₗ f = id
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>K : Type u_3<VAR>V : Type u_4<VAR>V' : Type u_5<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>f : V →ₗ[K] V'<VAR>hf_inj : ker f = ⊥<VAR>B : Set V := Basis.ofVectorSpaceIndex K V<VAR>hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V<VAR>hB₀ : LinearIndependent (ι := { x // x ∈ Set.range ⇑hB }) K Subtype.val<GOAL>∃ g, g ∘ₗ f = id
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>K : Type u_3<VAR>V : Type u_4<VAR>V' : Type u_5<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>f : V →ₗ[K] V'<VAR>hf_inj : ker f = ⊥<VAR>B : Set V := Basis.ofVectorSpaceIndex K V<VAR>hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V<VAR>hB₀ : LinearIndependent (ι := { x // x ∈ Set.range ⇑hB }) K Subtype.val<VAR>this : LinearIndependent K fun (x : ↑(⇑f '' B)) => ↑x<GOAL>∃ g, g ∘ₗ f = id
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>K : Type u_3<VAR>V : Type u_4<VAR>V' : Type u_5<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>f : V →ₗ[K] V'<VAR>hf_inj : ker f = ⊥<VAR>B : Set V := Basis.ofVectorSpaceIndex K V<VAR>hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V<VAR>hB₀ : LinearIndependent (ι := { x // x ∈ Set.range ⇑hB }) K Subtype.val<VAR>this : LinearIndependent K fun (x : ↑(⇑f '' B)) => ↑x<VAR>C : Set V' := this.extend ⋯<GOAL>∃ g, g ∘ₗ f = id
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>K : Type u_3<VAR>V : Type u_4<VAR>V' : Type u_5<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>f : V →ₗ[K] V'<VAR>hf_inj : ker f = ⊥<VAR>B : Set V := Basis.ofVectorSpaceIndex K V<VAR>hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V<VAR>hB₀ : LinearIndependent (ι := { x // x ∈ Set.range ⇑hB }) K Subtype.val<VAR>this : LinearIndependent K fun (x : ↑(⇑f '' B)) => ↑x<VAR>C : Set V' := this.extend ⋯<VAR>BC : ⇑f '' B ⊆ this.extend ⋯<GOAL>∃ g, g ∘ₗ f = id
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>K : Type u_3<VAR>V : Type u_4<VAR>V' : Type u_5<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>f : V →ₗ[K] V'<VAR>hf_inj : ker f = ⊥<VAR>B : Set V := Basis.ofVectorSpaceIndex K V<VAR>hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V<VAR>hB₀ : LinearIndependent (ι := { x // x ∈ Set.range ⇑hB }) K Subtype.val<VAR>this : LinearIndependent K fun (x : ↑(⇑f '' B)) => ↑x<VAR>C : Set V' := this.extend ⋯<VAR>BC : ⇑f '' B ⊆ this.extend ⋯<VAR>hC : Basis (↑(this.extend ⋯)) K V' := Basis.extend this<VAR>Vinh : Inhabited V<GOAL>∃ g, g ∘ₗ f = id
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>K : Type u_3<VAR>V : Type u_4<VAR>V' : Type u_5<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>f : V →ₗ[K] V'<VAR>hf_inj : ker f = ⊥<VAR>B : Set V := Basis.ofVectorSpaceIndex K V<VAR>hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V<VAR>hB₀ : LinearIndependent (ι := { x // x ∈ Set.range ⇑hB }) K Subtype.val<VAR>this : LinearIndependent K fun (x : ↑(⇑f '' B)) => ↑x<VAR>C : Set V' := this.extend ⋯<VAR>BC : ⇑f '' B ⊆ this.extend ⋯<VAR>hC : Basis (↑(this.extend ⋯)) K V' := Basis.extend this<VAR>Vinh : Inhabited V<VAR>b : ↑(Basis.ofVectorSpaceIndex K V)<GOAL>((hC.constr ℕ) (C.restrict (invFun ⇑f)) ∘ₗ f) (hB b) = id (hB b)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>K : Type u_3<VAR>V : Type u_4<VAR>V' : Type u_5<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>f : V →ₗ[K] V'<VAR>hf_inj : ker f = ⊥<VAR>B : Set V := Basis.ofVectorSpaceIndex K V<VAR>hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V<VAR>hB₀ : LinearIndependent (ι := { x // x ∈ Set.range ⇑hB }) K Subtype.val<VAR>this : LinearIndependent K fun (x : ↑(⇑f '' B)) => ↑x<VAR>C : Set V' := this.extend ⋯<VAR>BC : B ⊆ ⇑f ⁻¹' this.extend ⋯<VAR>hC : Basis (↑(this.extend ⋯)) K V' := Basis.extend this<VAR>Vinh : Inhabited V<VAR>b : ↑(Basis.ofVectorSpaceIndex K V)<GOAL>((hC.constr ℕ) (C.restrict (invFun ⇑f)) ∘ₗ f) (hB b) = id (hB b)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>K : Type u_3<VAR>V : Type u_4<VAR>V' : Type u_5<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>f : V →ₗ[K] V'<VAR>hf_inj : ker f = ⊥<VAR>B : Set V := Basis.ofVectorSpaceIndex K V<VAR>hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V<VAR>hB₀ : LinearIndependent (ι := { x // x ∈ Set.range ⇑hB }) K Subtype.val<VAR>this : LinearIndependent K fun (x : ↑(⇑f '' B)) => ↑x<VAR>C : Set V' := this.extend ⋯<VAR>BC : B ⊆ ⇑f ⁻¹' this.extend ⋯<VAR>hC : Basis (↑(this.extend ⋯)) K V' := Basis.extend this<VAR>Vinh : Inhabited V<VAR>b : ↑(Basis.ofVectorSpaceIndex K V)<VAR>fb_eq : f ↑b = hC ⟨f ↑b, ⋯⟩<GOAL>((hC.constr ℕ) (C.restrict (invFun ⇑f)) ∘ₗ f) (hB b) = id (hB b)