ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : LinearOrderedRing α<VAR>inst✝³ : LinearOrderedAddCommGroup β<VAR>inst✝² : Module α β<VAR>inst✝¹ : OrderedSMul α β<VAR>s : Finset ι<VAR>σ : Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>inst✝ : Fintype ι<VAR>hfg : Antivary f g<GOAL>∑ i : ι, f (σ i) • g i = ∑ i : ι, f i • g i ↔ Antivary (f ∘ ⇑σ) g
<VAR>R S : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝³ : CommRing R'<VAR>inst✝² : CommRing S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R R'<VAR>inst✝ : Algebra S S'<GOAL>RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f => Function.Surjective ⇑f
<VAR>R S : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝³ : CommRing R'<VAR>inst✝² : CommRing S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R R'<VAR>inst✝ : Algebra S S'<GOAL>RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] f => Function.Surjective ⇑f
<VAR>R S : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝³ : CommRing R'<VAR>inst✝² : CommRing S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R R'<VAR>inst✝ : Algebra S S'<GOAL>∀ {R S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), Function.Surjective ⇑e.toRingHom
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>f✝ : R →+* S₁<VAR>g✝ : σ → S₁<VAR>inst✝ : CommSemiring S₂<VAR>f : R →+* S₁<VAR>g : σ → S₁<VAR>φ : S₁ →+* S₂<GOAL>φ.comp (eval₂Hom f g) = eval₂Hom (φ.comp f) fun i => φ (g i)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>f✝ : R →+* S₁<VAR>g✝ : σ → S₁<VAR>inst✝ : CommSemiring S₂<VAR>f : R →+* S₁<VAR>g : σ → S₁<VAR>φ : S₁ →+* S₂<GOAL>∀ (r : R), (φ.comp (eval₂Hom f g)) (C r) = (eval₂Hom (φ.comp f) fun i => φ (g i)) (C r)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>f✝ : R →+* S₁<VAR>g✝ : σ → S₁<VAR>inst✝ : CommSemiring S₂<VAR>f : R →+* S₁<VAR>g : σ → S₁<VAR>φ : S₁ →+* S₂<GOAL>∀ (i : σ), (φ.comp (eval₂Hom f g)) (X i) = (eval₂Hom (φ.comp f) fun i => φ (g i)) (X i)
<VAR>J : Type v<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u<VAR>inst✝² : Category.{v, u} D<VAR>G : D ⥤ C<VAR>inst✝¹ : HasLimits D<VAR>inst✝ : PreservesLimits G<VAR>hG : SolutionSetCondition G<GOAL>G.IsRightAdjoint
<VAR>J : Type v<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u<VAR>inst✝² : Category.{v, u} D<VAR>G : D ⥤ C<VAR>inst✝¹ : HasLimits D<VAR>inst✝ : PreservesLimits G<VAR>hG : SolutionSetCondition G<GOAL>∀ (A : C), HasInitial (StructuredArrow A G)
<VAR>J : Type v<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u<VAR>inst✝² : Category.{v, u} D<VAR>G : D ⥤ C<VAR>inst✝¹ : HasLimits D<VAR>inst✝ : PreservesLimits G<VAR>A : C<VAR>ι : Type v<VAR>B : ι → D<VAR>f : (i : ι) → A ⟶ G.obj (B i)<VAR>g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h<VAR>B' : ι → StructuredArrow A G := fun i => StructuredArrow.mk (f i)<VAR>hB' : ∀ (A' : StructuredArrow A G), ∃ i, Nonempty (B' i ⟶ A')<GOAL>HasInitial (StructuredArrow A G)
<VAR>J : Type v<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u<VAR>inst✝² : Category.{v, u} D<VAR>G : D ⥤ C<VAR>inst✝¹ : HasLimits D<VAR>inst✝ : PreservesLimits G<VAR>A : C<VAR>ι : Type v<VAR>B : ι → D<VAR>f : (i : ι) → A ⟶ G.obj (B i)<VAR>g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h<VAR>B' : ι → StructuredArrow A G := fun i => StructuredArrow.mk (f i)<VAR>hB' : ∀ (A' : StructuredArrow A G), ∃ i, Nonempty (B' i ⟶ A')<VAR>T : StructuredArrow A G<VAR>hT : ∀ (X : StructuredArrow A G), Nonempty (T ⟶ X)<GOAL>HasInitial (StructuredArrow A G)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>inst✝⁷ : Category.{u_7, u_1} C<VAR>inst✝⁶ : Category.{u_6, u_2} D<VAR>inst✝⁵ : Category.{?u.55691, u_3} E<VAR>inst✝⁴ : Category.{?u.55695, u_4} E'<VAR>A : Type u_5<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : HasShift D A<VAR>inst✝¹ : HasShift E A<VAR>inst✝ : HasShift E' A<VAR>F G H : SingleFunctors C D A<VAR>e : F ≅ G<VAR>n : A<VAR>X : C<GOAL>(e.hom.hom n).app X ≫ (e.inv.hom n).app X = 𝟙 ((F.functor n).obj X)
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝⁴ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝² : Ring R<VAR>inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀<VAR>inst✝ : LinearOrderedCommMonoidWithZero Γ'₀<VAR>v v₁ : Valuation R Γ₀<VAR>v₂ : Valuation R Γ'₀<VAR>v₃ : Valuation R Γ''₀<VAR>v' : Valuation R Γ₀<VAR>f : Γ₀ →*₀ Γ'₀<VAR>hf : Monotone ⇑f<VAR>inf : Injective ⇑f<VAR>h : v.IsEquiv v'<VAR>H : StrictMono ⇑f := Monotone.strictMono_of_injective hf inf<VAR>r s : R<GOAL>f (v r) ≤ f (v s) ↔ v r ≤ v s
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝⁴ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝² : Ring R<VAR>inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀<VAR>inst✝ : LinearOrderedCommMonoidWithZero Γ'₀<VAR>v v₁ : Valuation R Γ₀<VAR>v₂ : Valuation R Γ'₀<VAR>v₃ : Valuation R Γ''₀<VAR>v' : Valuation R Γ₀<VAR>f : Γ₀ →*₀ Γ'₀<VAR>hf : Monotone ⇑f<VAR>inf : Injective ⇑f<VAR>h : v.IsEquiv v'<VAR>H : StrictMono ⇑f := Monotone.strictMono_of_injective hf inf<VAR>r s : R<GOAL>v' r ≤ v' s ↔ f (v' r) ≤ f (v' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>s t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : IsScalarTower ℝ 𝕜 E<VAR>hs : Balanced 𝕜 s<VAR>r : 𝕜<VAR>x : E<GOAL>gauge s (r • x) = ‖r‖ * gauge s x
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>x : α<VAR>xs l₂ : List α<VAR>h : ∀ (b : α), b ∈ x :: xs → ¬p b = true<GOAL>eraseP p (x :: xs ++ l₂) = x :: xs ++ eraseP p l₂
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<GOAL>↑(p - 1)! = -1
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<GOAL>∏ x ∈ Ico 1 (p - 1).succ, ↑x = ∏ x : (ZMod p)ˣ, ↑x
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hp : 0 < p<GOAL>∏ x ∈ Ico 1 (p - 1).succ, ↑x = ∏ x : (ZMod p)ˣ, ↑x
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hp : 0 < p<GOAL>∏ x : (ZMod p)ˣ, ↑x = ∏ x ∈ Ico 1 (p - 1).succ, ↑x
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hp : 0 < p<GOAL>∀ (a : (ZMod p)ˣ) (ha : a ∈ univ), (fun a x => (↑a).val) a ha ∈ Ico 1 (p - 1).succ
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hp : 0 < p<GOAL>∀ (a₁ : (ZMod p)ˣ) (ha₁ : a₁ ∈ univ) (a₂ : (ZMod p)ˣ) (ha₂ : a₂ ∈ univ), (fun a x => (↑a).val) a₁ ha₁ = (fun a x => (↑a).val) a₂ ha₂ → a₁ = a₂
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hp : 0 < p<GOAL>∀ b ∈ Ico 1 (p - 1).succ, ∃ a, ∃ (ha : a ∈ univ), (fun a x => (↑a).val) a ha = b
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hp : 0 < p<GOAL>∀ (a : (ZMod p)ˣ) (ha : a ∈ univ), ↑a = ↑((fun a x => (↑a).val) a ha)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝⁷ : Category.{u_4, u_1} C<VAR>inst✝⁶ : Category.{u_5, u_2} D<VAR>inst✝⁵ : Category.{?u.32181, u_3} E<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : Preadditive D<VAR>inst✝² : Preadditive E<VAR>F : C ⥤ D<VAR>inst✝¹ : F.Additive<VAR>inst✝ : HasZeroObject C<GOAL>IsZero (F.obj 0)
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → R<GOAL>(eval P) W'.polynomialX = W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4)
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → R<GOAL>(eval P) (C W'.a₁ * X y * X z - (C 3 * X x ^ 2 + C (2 * W'.a₂) * X x * X z ^ 2 + C W'.a₄ * X z ^ 4)) = W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4)
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>α : Type u_3<VAR>m : MeasurableSpace Ω<VAR>m' : MeasurableSpace Ω'<VAR>μ : Measure Ω<VAR>s t✝ : Set Ω<VAR>hms : MeasurableSet s<VAR>t : Set Ω<GOAL>μ[|s] t = (μ s)⁻¹ * μ (s ∩ t)
<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.Injective ⇑(lTensor M f) ↔ Function.Injective ⇑(rTensor M f)
<GOAL>2 • ↑(-π / 2) = ↑π
<VAR>x : ℂ<VAR>hx : x.arg ≠ π<GOAL>log x⁻¹ = -log x
<VAR>α β : Type u<VAR>ι : Type u_1<VAR>f : ι → Cardinal.{u_2}<GOAL>prod f ≠ 0 ↔ ∀ (i : ι), f i ≠ 0
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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 uX<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>m✝ n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>m : ℕ<VAR>h : ContDiffAt 𝕜 n f x<VAR>hm : ↑m ≤ n<GOAL>∃ u ∈ 𝓝 x, ContDiffOn 𝕜 (↑m) f u
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝ : AddGroup G<VAR>T : AddTorsor G P<VAR>v₁ v₂ : G<VAR>p : P<GOAL>v₁ +ᵥ p -ᵥ (v₂ +ᵥ p) = v₁ - v₂
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w : ι → k<VAR>p₁ : ι → P<VAR>p₂ : P<VAR>h : ∑ i ∈ s, w i = 0<GOAL>∑ i ∈ s, w i • (p₁ i -ᵥ p₂) = (s.weightedVSub p₁) w
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>r : R<VAR>x✝ y : M<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>p p' : Submodule R M<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁴ : Ring R₂<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>q : Submodule R₂ M₂<VAR>N : Type u_5<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>P : Submodule R M<VAR>Q : Submodule R N<VAR>f : M ≃ₗ[R] N<VAR>hf : map f P = Q<VAR>x : N<VAR>hx : x ∈ Q<GOAL>x ∈ comap (↑f.symm) P
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>r : R<VAR>x✝ y : M<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>p p' : Submodule R M<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁴ : Ring R₂<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>q : Submodule R₂ M₂<VAR>N : Type u_5<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>P : Submodule R M<VAR>Q : Submodule R N<VAR>f : M ≃ₗ[R] N<VAR>hf : map f P = Q<VAR>x : N<VAR>hx : ∃ y ∈ P, f y = x<GOAL>x ∈ comap (↑f.symm) P
<VAR>E : Type u_1<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup V<VAR>inst✝⁸ : InnerProductSpace ℝ V<VAR>inst✝⁷ : MeasurableSpace V<VAR>inst✝⁶ : BorelSpace V<VAR>inst✝⁵ : FiniteDimensional ℝ V<VAR>W : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : InnerProductSpace ℝ W<VAR>inst✝² : MeasurableSpace W<VAR>inst✝¹ : BorelSpace W<VAR>inst✝ : FiniteDimensional ℝ W<VAR>f : V → E<VAR>y : V<GOAL>𝓕⁻ f y = 𝓕 (fun x => f (-x)) y
<VAR>E : Type u_1<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup V<VAR>inst✝⁸ : InnerProductSpace ℝ V<VAR>inst✝⁷ : MeasurableSpace V<VAR>inst✝⁶ : BorelSpace V<VAR>inst✝⁵ : FiniteDimensional ℝ V<VAR>W : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : InnerProductSpace ℝ W<VAR>inst✝² : MeasurableSpace W<VAR>inst✝¹ : BorelSpace W<VAR>inst✝ : FiniteDimensional ℝ W<VAR>f : V → E<VAR>y : V<GOAL>𝓕 f (-y) = 𝓕 (fun x => f (-x)) y
<VAR>E : Type u_1<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup V<VAR>inst✝⁸ : InnerProductSpace ℝ V<VAR>inst✝⁷ : MeasurableSpace V<VAR>inst✝⁶ : BorelSpace V<VAR>inst✝⁵ : FiniteDimensional ℝ V<VAR>W : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : InnerProductSpace ℝ W<VAR>inst✝² : MeasurableSpace W<VAR>inst✝¹ : BorelSpace W<VAR>inst✝ : FiniteDimensional ℝ W<VAR>f : V → E<VAR>y : V<GOAL>𝓕 f ((LinearIsometryEquiv.neg ℝ) y) = 𝓕 (f ∘ ⇑(LinearIsometryEquiv.neg ℝ)) y
<VAR>R : Type u_1<VAR>k p i : ℕ<VAR>hp : Nat.Prime p<GOAL>(σ k) (p ^ i) = ∑ j ∈ range (i + 1), p ^ (j * k)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n : ℤ<VAR>h : a * c⁻¹ = b<GOAL>a = b * c
<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>n : ℕ∞<VAR>c : E → F →L[𝕜] G<VAR>hc : ContDiff 𝕜 n c<VAR>i : ℕ<VAR>hi : ↑i ≤ n<VAR>x : E<VAR>u : F<VAR>m : Fin i → E<GOAL>(iteratedFDeriv 𝕜 i (fun y => (c y) u) x) m = ((iteratedFDeriv 𝕜 i c x) m) u
<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>n : ℕ∞<VAR>c : E → F →L[𝕜] G<VAR>hc : ContDiff 𝕜 n c<VAR>i : ℕ<VAR>hi : ↑i ≤ n<VAR>x : E<VAR>u : F<VAR>m : Fin i → E<GOAL>(iteratedFDerivWithin 𝕜 i (fun y => (c y) u) univ x) m = ((iteratedFDerivWithin 𝕜 i c univ x) m) u
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>v : Fin 3 → R<GOAL>(crossProduct v) v = 0
<VAR>α : Type u_1<VAR>inst✝ : AddCommGroup α<VAR>p a a₁ a₂ b b₁ b₂ c : α<VAR>n : ℕ<VAR>z : ℤ<GOAL>a ≡ b [PMOD p] ↔ ↑b = ↑a
<VAR>M : Type u_1<VAR>inst✝¹ : OrderedCancelAddCommMonoid M<VAR>inst✝ : ExistsAddOfLE M<VAR>a b c d : M<GOAL>BijOn (fun x => x + d) (Ioc a b) (Ioc (a + d) (b + d))
<VAR>M : Type u_1<VAR>inst✝¹ : OrderedCancelAddCommMonoid M<VAR>inst✝ : ExistsAddOfLE M<VAR>a b c d : M<GOAL>BijOn (fun x => x + d) (Ioi a ∩ Iic b) (Ioi (a + d) ∩ Iic (b + d))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : NonPreadditiveAbelian C<VAR>X Y : C<VAR>a : X ⟶ Y<GOAL>a + 0 = a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : Monoid α<VAR>s t : Set α<VAR>a : α<VAR>m n : ℕ<VAR>hst : s ⊆ t<GOAL>s ^ 0 ⊆ t ^ 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : Monoid α<VAR>s t : Set α<VAR>a : α<VAR>m n : ℕ<VAR>hst : s ⊆ t<GOAL>1 ⊆ t ^ 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : Monoid α<VAR>s t : Set α<VAR>a : α<VAR>m n✝ : ℕ<VAR>hst : s ⊆ t<VAR>n : ℕ<GOAL>s ^ (n + 1) ⊆ t ^ (n + 1)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : Monoid α<VAR>s t : Set α<VAR>a : α<VAR>m n✝ : ℕ<VAR>hst : s ⊆ t<VAR>n : ℕ<GOAL>s ^ n * s ⊆ t ^ (n + 1)
<VAR>s : ℂ<GOAL>L (fun n => ↑(ζ n)) s = L 1 s
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>p : ℝ≥0<VAR>s : Set α<VAR>h : s ⊆ {x | v.limRatioMeas hρ x < ↑p}<VAR>t : Set α := {x | Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}<GOAL>ρ s ≤ ↑p * μ s
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>p : ℝ≥0<VAR>s : Set α<VAR>h : s ⊆ {x | v.limRatioMeas hρ x < ↑p}<VAR>t : Set α := {x | Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}<VAR>A : μ tᶜ = 0<GOAL>ρ s ≤ ↑p * μ s
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>p : ℝ≥0<VAR>s : Set α<VAR>h : s ⊆ {x | v.limRatioMeas hρ x < ↑p}<VAR>t : Set α := {x | Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}<VAR>A : μ tᶜ = 0<GOAL>ρ (s ∩ t) ≤ (p • μ) (s ∩ t)
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>p : ℝ≥0<VAR>s : Set α<VAR>h : s ⊆ {x | v.limRatioMeas hρ x < ↑p}<VAR>t : Set α := {x | Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}<VAR>A : μ tᶜ = 0<VAR>x : α<VAR>hx : x ∈ s ∩ t<GOAL>∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ (p • μ) a
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>p : ℝ≥0<VAR>s : Set α<VAR>h : s ⊆ {x | v.limRatioMeas hρ x < ↑p}<VAR>t : Set α := {x | Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}<VAR>A : μ tᶜ = 0<VAR>x : α<VAR>hx : x ∈ s ∩ t<VAR>I : ∀ᶠ (b : Set α) in v.filterAt x, ρ b / μ b < ↑p<GOAL>∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ (p • μ) a
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>p : ℝ≥0<VAR>s : Set α<VAR>h : s ⊆ {x | v.limRatioMeas hρ x < ↑p}<VAR>t : Set α := {x | Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}<VAR>A : μ tᶜ = 0<VAR>x : α<VAR>hx : x ∈ s ∩ t<VAR>I : ∀ᶠ (b : Set α) in v.filterAt x, ρ b / μ b < ↑p<VAR>a : Set α<VAR>ha : ρ a / μ a < ↑p<GOAL>ρ a ≤ (p • μ) a
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>p : ℝ≥0<VAR>s : Set α<VAR>h : s ⊆ {x | v.limRatioMeas hρ x < ↑p}<VAR>t : Set α := {x | Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}<VAR>A : μ tᶜ = 0<VAR>x : α<VAR>hx : x ∈ s ∩ t<VAR>I : ∀ᶠ (b : Set α) in v.filterAt x, ρ b / μ b < ↑p<VAR>a : Set α<VAR>ha : ρ a / μ a < ↑p<GOAL>ρ a ≤ ↑p * μ a
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>p : ℝ≥0<VAR>s : Set α<VAR>h : s ⊆ {x | v.limRatioMeas hρ x < ↑p}<VAR>t : Set α := {x | Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}<VAR>A : μ tᶜ = 0<VAR>x : α<VAR>hx : x ∈ s ∩ t<VAR>I : ∀ᶠ (b : Set α) in v.filterAt x, ρ b / μ b < ↑p<VAR>a : Set α<VAR>ha : ρ a / μ a < ↑p<GOAL>μ a ≠ 0 ∨ ↑p ≠ ⊤
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X<VAR>p : Path x₀ x₁<VAR>q : Path x₁ x₂<VAR>r : Path x₂ x₃<VAR>x : ↑I<GOAL>((p.trans q).trans r) x = ((p.trans (q.trans r)).reparam (fun t => ⟨transAssocReparamAux t, ⋯⟩) ⋯ ⋯ ⋯) x
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X<VAR>p : Path x₀ x₁<VAR>q : Path x₁ x₂<VAR>r : Path x₂ x₃<VAR>x : ↑I<GOAL>(if h : ↑x ≤ 1 / 2 then if h_1 : 2 * ↑x ≤ 1 / 2 then p ⟨2 * (2 * ↑x), ⋯⟩ else q ⟨2 * (2 * ↑x) - 1, ⋯⟩ else r ⟨2 * ↑x - 1, ⋯⟩) = if h : (if ↑x ≤ 1 / 4 then 2 * ↑x else if ↑x ≤ 1 / 2 then ↑x + 1 / 4 else 1 / 2 * (↑x + 1)) ≤ 1 / 2 then p ⟨if ↑x ≤ 1 / 4 then 2 * (2 * ↑x) else if ↑x ≤ 1 / 2 then 2 * (↑x + 1 / 4) else 2 * (1 / 2 * (↑x + 1)), ⋯⟩ else if h_1 : (if ↑x ≤ 1 / 4 then 2 * (2 * ↑x) else if ↑x ≤ 1 / 2 then 2 * (↑x + 1 / 4) else 2 * (1 / 2 * (↑x + 1))) - 1 ≤ 1 / 2 then q ⟨2 * ((if ↑x ≤ 1 / 4 then 2 * (2 * ↑x) else if ↑x ≤ 1 / 2 then 2 * (↑x + 1 / 4) else 2 * (1 / 2 * (↑x + 1))) - 1), ⋯⟩ else r ⟨2 * ((if ↑x ≤ 1 / 4 then 2 * (2 * ↑x) else if ↑x ≤ 1 / 2 then 2 * (↑x + 1 / 4) else 2 * (1 / 2 * (↑x + 1))) - 1) - 1, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Fintype α<VAR>s t : Finset α<VAR>inst✝ : Subsingleton α<VAR>x : α<VAR>hx : x ∈ s<GOAL>s = univ
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph α<VAR>inst✝² : Fintype (Sym2 α)<VAR>inst✝¹ : NonAssocSemiring R<VAR>a b : α<VAR>e : Sym2 α<VAR>inst✝ : Fintype α<GOAL>e ∈ G.edgeSet → ∑ a : α, incMatrix R G a e = 2
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>hm : m ≠ 0<GOAL>LiouvilleWith p (↑m * x) ↔ LiouvilleWith p x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f✝ f : α → β<VAR>h : μ ≤ ν<VAR>hf : Measurable f<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>(map f μ) s ≤ (map f ν) s
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type u<VAR>inst✝¹ : CommRing S<VAR>P : Type u<VAR>inst✝ : CommRing P<VAR>U V : Opens ↑(PrimeSpectrum.Top R)<VAR>iVU : V ⟶ U<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>p : ↥(unop (op V))<GOAL>↑((comap (RingHom.id R) U V ⋯) s) p = ↑(((structureSheaf R).val.map iVU.op) s) p
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type u<VAR>inst✝¹ : CommRing S<VAR>P : Type u<VAR>inst✝ : CommRing P<VAR>U V : Opens ↑(PrimeSpectrum.Top R)<VAR>iVU : V ⟶ U<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>p : ↥(unop (op V))<GOAL>(Localization.localRingHom ((PrimeSpectrum.comap (RingHom.id R)) ↑p).asIdeal (↑p).asIdeal (RingHom.id R) ⋯) (↑s ⟨(PrimeSpectrum.comap (RingHom.id R)) ↑p, ⋯⟩) = ↑(((structureSheaf R).val.map iVU.op) s) p