ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>o.oangle y (y - x) = ↑(Real.arccos (‖y‖ / ‖y - x‖))
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<VAR>hs : (o.oangle y (y - x)).sign = 1<GOAL>o.oangle y (y - x) = ↑(Real.arccos (‖y‖ / ‖y - x‖))
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s : Set E<VAR>a b m : ℝ<VAR>x y : E<VAR>f g : E → ℝ<VAR>hf : UniformConvexOn s φ f<VAR>hg : UniformConvexOn s ψ g<GOAL>UniformConvexOn s (φ + ψ) (f + g)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s : Set E<VAR>a✝ b✝ m : ℝ<VAR>x✝ y✝ : E<VAR>f g : E → ℝ<VAR>hf : UniformConvexOn s φ f<VAR>hg : UniformConvexOn s ψ g<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>a b : ℝ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>(f + g) (a • x + b • y) ≤ a • (f + g) x + b • (f + g) y - a * b * (φ + ψ) ‖x - y‖
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : R[X]<VAR>n m : ℕ<VAR>dvd : q ^ n ∣ p<GOAL>q ^ (n - m) ∣ (⇑derivative)^[m] p
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>m n : ℤ<VAR>hm : 0 ≤ m<VAR>hn : 0 ≤ n<GOAL>A ^ (m + n) = A ^ m * A ^ n
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>n : ℤ<VAR>hn : 0 ≤ n<VAR>k : ℕ<VAR>hm : 0 ≤ ↑k<GOAL>A ^ (↑k + n) = A ^ ↑k * A ^ n
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>k : ℕ<VAR>hm : 0 ≤ ↑k<VAR>l : ℕ<VAR>hn : 0 ≤ ↑l<GOAL>A ^ (↑k + ↑l) = A ^ ↑k * A ^ ↑l
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S S₁ S₂ S₃ : SnakeInput C<VAR>f : S₁ ⟶ S₂<GOAL>S₁.φ₁ ≫ f.f₂.τ₁ = functorP.map f ≫ S₂.φ₁
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : M<VAR>f : F<VAR>h : IsPrimitiveRoot ζ k<VAR>i : ℕ<VAR>hi : i.Coprime k<VAR>h0 : ¬k = 0<GOAL>IsPrimitiveRoot (ζ ^ i) k
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>f : F<VAR>i : ℕ<VAR>hi : i.Coprime k<VAR>h0 : ¬k = 0<VAR>ζ : Mˣ<VAR>h : IsPrimitiveRoot (↑ζ) k<GOAL>IsPrimitiveRoot (↑ζ ^ i) k
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>f : F<VAR>i : ℕ<VAR>hi : i.Coprime k<VAR>h0 : ¬k = 0<VAR>ζ : Mˣ<VAR>h : IsPrimitiveRoot (↑ζ) k<GOAL>IsPrimitiveRoot (↑(ζ ^ i)) k
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>f : F<VAR>i : ℕ<VAR>hi : i.Coprime k<VAR>h0 : ¬k = 0<VAR>ζ : Mˣ<VAR>h : IsPrimitiveRoot ζ k<GOAL>IsPrimitiveRoot (ζ ^ i) k
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>f : F<VAR>i : ℕ<VAR>hi : i.Coprime k<VAR>h0 : ¬k = 0<VAR>ζ : Mˣ<VAR>h : IsPrimitiveRoot ζ k<GOAL>∀ (l : ℕ), (ζ ^ i) ^ l = 1 → k ∣ l
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l✝ : ℕ<VAR>f : F<VAR>i : ℕ<VAR>hi : i.Coprime k<VAR>h0 : ¬k = 0<VAR>ζ : Mˣ<VAR>h : IsPrimitiveRoot ζ k<VAR>l : ℕ<VAR>hl : (ζ ^ i) ^ l = 1<GOAL>k ∣ l
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l✝ : ℕ<VAR>f : F<VAR>i : ℕ<VAR>hi : i.Coprime k<VAR>h0 : ¬k = 0<VAR>ζ : Mˣ<VAR>h : IsPrimitiveRoot ζ k<VAR>l : ℕ<VAR>hl : (ζ ^ i) ^ l = 1<GOAL>ζ ^ l = 1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l✝ : ℕ<VAR>f : F<VAR>i : ℕ<VAR>hi : i.Coprime k<VAR>h0 : ¬k = 0<VAR>ζ : Mˣ<VAR>h : IsPrimitiveRoot ζ k<VAR>l : ℕ<VAR>hl : (ζ ^ i) ^ l = 1<GOAL>ζ ^ (↑i * ↑l * i.gcdA k) * (ζ ^ (↑k * i.gcdB k)) ^ l = 1
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>L : Type v<VAR>ζ : L<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)<VAR>hk : p ^ (k + 1) ≠ 2<GOAL>discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = (-1) ^ (φ (↑p ^ (k + 1)) / 2) * ↑↑p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1))
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>L : Type v<VAR>ζ : L<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)<VAR>hk : p ^ (k + 1) ≠ 2<VAR>hne : NeZero ↑↑(p ^ (k + 1))<GOAL>discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = (-1) ^ (φ (↑p ^ (k + 1)) / 2) * ↑↑p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1))
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>L : Type v<VAR>ζ : L<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)<VAR>hk : p ^ (k + 1) ≠ 2<VAR>hne : NeZero ↑↑(p ^ (k + 1))<VAR>mf : Module.Finite K L<GOAL>discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = (-1) ^ (φ (↑p ^ (k + 1)) / 2) * ↑↑p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1))
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>L : Type v<VAR>ζ : L<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)<VAR>hk : p ^ (k + 1) ≠ 2<VAR>hne : NeZero ↑↑(p ^ (k + 1))<VAR>mf : Module.Finite K L<VAR>se : Algebra.IsSeparable K L<GOAL>discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = (-1) ^ (φ (↑p ^ (k + 1)) / 2) * ↑↑p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1))
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>L : Type v<VAR>ζ : L<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)<VAR>hk : p ^ (k + 1) ≠ 2<VAR>hne : NeZero ↑↑(p ^ (k + 1))<VAR>mf : Module.Finite K L<VAR>se : Algebra.IsSeparable K L<GOAL>(-1) ^ (↑p ^ k * (↑p - 1) * (↑p ^ k * (↑p - 1) - 1) / 2) * (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (↑p ^ (k + 1)) K))) = (-1) ^ (↑p ^ k * (↑p - 1) / 2) * ↑↑p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1))
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i : ι<VAR>c : R<VAR>x✝ x : M<GOAL>(∀ (i : ι), (b.coord i) x = 0) ↔ b.repr x = 0
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>hp : p ≠ 0<VAR>hn : ∀ m < n, p.coeff m = 0<GOAL>n ≤ p.natTrailingDegree
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>hp : p ≠ 0<VAR>hn : ∀ m < n, p.coeff m = 0<GOAL>n ≤ p.support.min' ⋯
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : Nonempty V<VAR>k : ℕ<VAR>h : ∀ (v : V), k ≤ G.degree v<GOAL>k ≤ G.minDegree
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : Nonempty V<VAR>k : ℕ<VAR>h : ∀ (v : V), k ≤ G.degree v<VAR>v : V<VAR>hv : G.minDegree = G.degree v<GOAL>k ≤ G.minDegree
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>M : Matroid α<VAR>Xs : Set (Set α)<GOAL>M.closure (⋃ X ∈ Xs, M.closure X) = M.closure (⋃₀ Xs)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : Preorder β<VAR>f : β → Finset α<VAR>h : Monotone f<VAR>h' : ∀ (x : α), ∃ n, x ∈ f n<GOAL>Tendsto f atTop atTop
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : Preorder β<VAR>f : β → Finset α<VAR>h : Monotone f<VAR>h' : ∀ (x : α), ∃ n, x ∈ f n<GOAL>∀ (i : α), ∀ᶠ (a : β) in atTop, f a ∈ Ici {i}
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : Preorder β<VAR>f : β → Finset α<VAR>h : Monotone f<VAR>h' : ∀ (x : α), ∃ n, x ∈ f n<VAR>a : α<VAR>b : β<VAR>hb : a ∈ f b<GOAL>∀ᶠ (a_1 : β) in atTop, f a_1 ∈ Ici {a}
<VAR>α✝ : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>α : Sort u_4<GOAL>IsEmpty (PLift α) ↔ IsEmpty α
<VAR>P : Type u_1<VAR>inst✝ : Preorder P<VAR>C : Set (Set P)<VAR>hidl : ∀ I ∈ C, IsIdeal I<VAR>hD : DirectedOn (fun x x_1 => x ⊆ x_1) C<VAR>hNe : C.Nonempty<GOAL>IsIdeal (⋃₀ C)
<VAR>P : Type u_1<VAR>inst✝ : Preorder P<VAR>C : Set (Set P)<VAR>hidl : ∀ I ∈ C, IsIdeal I<VAR>hD : DirectedOn (fun x x_1 => x ⊆ x_1) C<VAR>hNe : C.Nonempty<GOAL>∃ s ∈ C, s.Nonempty
<VAR>P : Type u_1<VAR>inst✝ : Preorder P<VAR>C : Set (Set P)<VAR>hidl : ∀ I ∈ C, IsIdeal I<VAR>hD : DirectedOn (fun x x_1 => x ⊆ x_1) C<VAR>hNe : C.Nonempty<VAR>I : Set P<VAR>hI : I ∈ C<GOAL>∃ s ∈ C, s.Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>x : α<GOAL>∃ s, x ∈ s ∧ IsOpen s ∧ μ s < ⊤
<VAR>A : Type u'<VAR>inst✝⁸ : Category.{v', u'} A<VAR>inst✝⁷ : ConcreteCategory A<VAR>inst✝⁶ : HasFunctorialSurjectiveInjectiveFactorization A<VAR>inst✝⁵ : (coherentTopology CompHaus).WEqualsLocallyBijective A<VAR>inst✝⁴ : HasSheafify (coherentTopology CompHaus) A<VAR>inst✝³ : (coherentTopology CompHaus).HasSheafCompose (CategoryTheory.forget A)<VAR>inst✝² : Balanced (Sheaf (coherentTopology CompHaus) A)<VAR>inst✝¹ : PreservesFiniteProducts (CategoryTheory.forget A)<VAR>inst✝ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X Stonean.toCompHaus.op) A<VAR>X Y : Condensed A<VAR>f : X ⟶ Y<GOAL>Epi f ↔ ∀ (S : CompHaus) (y : (CategoryTheory.forget A).obj (Y.val.obj (op S))), ∃ S' φ, ∃ (_ : Function.Surjective ⇑φ), ∃ x, (f.val.app (op S')) x = (Y.val.map (op φ)) y
<VAR>A : Type u'<VAR>inst✝⁸ : Category.{v', u'} A<VAR>inst✝⁷ : ConcreteCategory A<VAR>inst✝⁶ : HasFunctorialSurjectiveInjectiveFactorization A<VAR>inst✝⁵ : (coherentTopology CompHaus).WEqualsLocallyBijective A<VAR>inst✝⁴ : HasSheafify (coherentTopology CompHaus) A<VAR>inst✝³ : (coherentTopology CompHaus).HasSheafCompose (CategoryTheory.forget A)<VAR>inst✝² : Balanced (Sheaf (coherentTopology CompHaus) A)<VAR>inst✝¹ : PreservesFiniteProducts (CategoryTheory.forget A)<VAR>inst✝ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X Stonean.toCompHaus.op) A<VAR>X Y : Condensed A<VAR>f : X ⟶ Y<GOAL>(∀ (X_1 : CompHaus) (y : (CategoryTheory.forget A).obj (Y.val.obj (op X_1))), ∃ X' φ, ∃ (_ : EffectiveEpi φ), ∃ x, (f.val.app (op X')) x = (Y.val.map (op φ)) y) ↔ ∀ (S : CompHaus) (y : (CategoryTheory.forget A).obj (Y.val.obj (op S))), ∃ S' φ, ∃ (_ : Function.Surjective ⇑φ), ∃ x, (f.val.app (op S')) x = (Y.val.map (op φ)) y
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : MonoidalCategory C<VAR>A B X✝ X' Y Y' Z : C<VAR>inst✝¹ : Closed A<VAR>inst✝ : Closed B<VAR>f : B ⟶ A<VAR>X : C<GOAL>uncurry ((pre f).app X) = f ▷ (ihom A).obj X ≫ (ihom.ev A).app X
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>a b : α<VAR>h : normalize b = b<GOAL>lcm a b = b ↔ a ∣ b
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x✝ : 𝕜<VAR>s✝ t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>f : 𝕜 → F<VAR>s : Set F<VAR>x : 𝕜<GOAL>deriv f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ deriv f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s
<VAR>x✝ y : ℂ<VAR>x : ℝ<GOAL>(sinh ↑x).im = 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>S : Type u_1<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>P Q : Fin 3 → R<VAR>u : R<VAR>i : Fin 3<GOAL>(⇑f ∘ (u • P)) i = (f u • ⇑f ∘ P) i
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : MulAction (Perm α) β<VAR>i j : α<VAR>x : β<GOAL>swap i j • swap i j • x = x
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : T2Space α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace α<VAR>s : Set α<VAR>hs : AnalyticSet s<VAR>hsc : AnalyticSet sᶜ<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : T2Space α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace α<VAR>s : Set α<VAR>hs : AnalyticSet s<VAR>hsc : AnalyticSet sᶜ<VAR>u : Set α<VAR>hsu : s ⊆ u<VAR>hdu : Disjoint sᶜ u<VAR>hmu : MeasurableSet u<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : T2Space α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace α<VAR>s : Set α<VAR>hs : AnalyticSet s<VAR>hsc : AnalyticSet sᶜ<VAR>hsu : s ⊆ s<VAR>hdu : Disjoint sᶜ s<VAR>hmu : MeasurableSet s<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>inst✝ : CommMonoid α<VAR>x y z : α<VAR>hu : IsUnit x<GOAL>IsRelPrime (y * x) z ↔ IsRelPrime y z
<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✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>v✝ : Valuation R Γ₀<VAR>x✝ y z : R<VAR>v : Valuation K Γ₀<VAR>x : K<VAR>h : x ≠ 0<GOAL>1 ≤ v x ↔ v x⁻¹ ≤ 1
<VAR>a b : EReal<VAR>h₁ : b ≠ ⊥<VAR>h₂ : b ≠ ⊤<VAR>h₃ : b ≠ 0<GOAL>b * (a / b) = a
<VAR>N : ℕ<VAR>a : Fin 2 → ZMod N<VAR>k : ℤ<VAR>hk : 3 ≤ k<VAR>z : ℍ<GOAL>Complex.abs (eisensteinSeries a k z) ≤ ∑' (x : Fin 2 → ℤ), Complex.abs (eisSummand k x z)
<VAR>N : ℕ<VAR>a : Fin 2 → ZMod N<VAR>k : ℤ<VAR>hk : 3 ≤ k<VAR>z : ℍ<GOAL>‖∑' (x : ↑(gammaSet N a)), eisSummand k (↑x) z‖ ≤ ∑' (x : Fin 2 → ℤ), ‖eisSummand k x z‖
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝² : MulZeroClass α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : MulPosMono α<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<GOAL>0 ≤ a * b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<GOAL>multiplicity a b = 0 ↔ ¬a ∣ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<GOAL>a ^ 0 ∣ b ∧ ¬a ^ (0 + 1) ∣ b ↔ ¬a ∣ b
<VAR>R : Type u_1<VAR>inst✝⁸ : StrictOrderedCommRing R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R N<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝³ : Fintype ι<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι'<VAR>inst✝ : DecidableEq ι'<VAR>e : Basis ι R M<VAR>w : ι → Rˣ<GOAL>(e.unitsSMul w).orientation = (∏ i : ι, w i)⁻¹ • e.orientation
<VAR>R : Type u_1<VAR>inst✝⁸ : StrictOrderedCommRing R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R N<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝³ : Fintype ι<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι'<VAR>inst✝ : DecidableEq ι'<VAR>e : Basis ι R M<VAR>w : ι → Rˣ<GOAL>SameRay R (e.unitsSMul w).det ((↑(∏ i : ι, w i)⁻¹ * ∏ i : ι, ↑(w i)) • (e.unitsSMul w).det)
<VAR>R : Type u_1<VAR>inst✝⁸ : StrictOrderedCommRing R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R N<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝³ : Fintype ι<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι'<VAR>inst✝ : DecidableEq ι'<VAR>e : Basis ι R M<VAR>w : ι → Rˣ<GOAL>SameRay R (e.unitsSMul w).det (↑((∏ i : ι, w i)⁻¹ * ∏ i : ι, w i) • (e.unitsSMul w).det)
<VAR>R : Type u_1<VAR>inst✝⁸ : StrictOrderedCommRing R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R N<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝³ : Fintype ι<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι'<VAR>inst✝ : DecidableEq ι'<VAR>e : Basis ι R M<VAR>w : ι → Rˣ<GOAL>SameRay R (e.unitsSMul w).det (e.unitsSMul w).det
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>inst✝² : Finite ι<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>b : AffineBasis ι ℝ E<GOAL>interior ((convexHull ℝ) (range ⇑b)) = {x | ∀ (i : ι), 0 < (b.coord i) x}
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>inst✝² : Finite ι<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>b : AffineBasis ι ℝ E<VAR>h✝ : Subsingleton ι<GOAL>interior ((convexHull ℝ) (range ⇑b)) = {x | ∀ (i : ι), 0 < (b.coord i) x}
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>inst✝² : Finite ι<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>b : AffineBasis ι ℝ E<VAR>h✝ : Nontrivial ι<GOAL>interior ((convexHull ℝ) (range ⇑b)) = {x | ∀ (i : ι), 0 < (b.coord i) x}
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>S : Submonoid G<VAR>g : G<VAR>g_in_s : g ∈ S<GOAL>g ^ exponent ↥S = 1
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>S : Submonoid G<VAR>g : G<VAR>g_in_s : g ∈ S<VAR>this : ⟨g, g_in_s⟩ ^ exponent ↥S = 1<GOAL>g ^ exponent ↥S = 1
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>ι : Type u_5<VAR>fi : Filter ι<VAR>inst✝ : Fact (1 ≤ p)<VAR>f : ι → ↥(Lp E p μ)<VAR>f_lim : α → E<VAR>f_lim_ℒp : Memℒp f_lim p μ<GOAL>Tendsto f fi (𝓝 (Memℒp.toLp f_lim f_lim_ℒp)) ↔ Tendsto (fun n => eLpNorm (↑↑(f n) - f_lim) p μ) fi (𝓝 0)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>ι : Type u_5<VAR>fi : Filter ι<VAR>inst✝ : Fact (1 ≤ p)<VAR>f : ι → ↥(Lp E p μ)<VAR>f_lim : α → E<VAR>f_lim_ℒp : Memℒp f_lim p μ<GOAL>Tendsto (fun n => eLpNorm (↑↑(f n) - ↑↑(Memℒp.toLp f_lim f_lim_ℒp)) p μ) fi (𝓝 0) ↔ Tendsto (fun n => eLpNorm (↑↑(f n) - f_lim) p μ) fi (𝓝 0)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>ι : Type u_5<VAR>fi : Filter ι<VAR>inst✝ : Fact (1 ≤ p)<VAR>f : ι → ↥(Lp E p μ)<VAR>f_lim : α → E<VAR>f_lim_ℒp : Memℒp f_lim p μ<GOAL>(fun n => eLpNorm (↑↑(f n) - ↑↑(Memℒp.toLp f_lim f_lim_ℒp)) p μ) = fun n => eLpNorm (↑↑(f n) - f_lim) p μ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝⁴ : LinearOrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : DenselyOrdered 𝕜<VAR>inst✝ : NoZeroSMulDivisors 𝕜 E<VAR>A B : Set E<VAR>x✝ x : E<VAR>hx : x ∈ extremePoints 𝕜 ((convexHull 𝕜) A)<GOAL>x ∈ A
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝⁴ : LinearOrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : DenselyOrdered 𝕜<VAR>inst✝ : NoZeroSMulDivisors 𝕜 E<VAR>A B : Set E<VAR>x✝ x : E<VAR>hx : x ∈ (convexHull 𝕜) A ∧ Convex 𝕜 ((convexHull 𝕜) A \ {x})<GOAL>x ∈ A
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝⁴ : LinearOrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : DenselyOrdered 𝕜<VAR>inst✝ : NoZeroSMulDivisors 𝕜 E<VAR>A B : Set E<VAR>x✝ x : E<VAR>hx : x ∈ (convexHull 𝕜) A ∧ Convex 𝕜 ((convexHull 𝕜) A \ {x})<VAR>h : x ∉ A<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f g : α → F'<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : F'<GOAL>(condexpL1CLM F' hm μ) ↑(simpleFunc.indicatorConst 1 hs hμs x) = (condexpInd F' hm μ s) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f g : α → F'<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : F'<GOAL>(condexpL1CLM F' hm μ) (indicatorConstLp 1 hs hμs x) = (condexpInd F' hm μ s) x
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>Q : QuadraticMap R M N<GOAL>Q 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>a : α<GOAL>(uniformOfFintype α) a = (↑(Fintype.card α))⁻¹
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Ring R'<VAR>inst✝⁵ : AddZeroClass A<VAR>inst✝⁴ : SemilatticeSup B<VAR>inst✝³ : Add B<VAR>inst✝² : OrderBot B<VAR>D : A → B<VAR>p q : R[A]<VAR>hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2<VAR>inst✝¹ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>s : R[A]<VAR>hs : s.support.Nonempty<GOAL>s.support.sup (WithBot.some ∘ D) = ↑(s.support.sup D)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>x : ↑(PrimeSpectrum.Top R)<GOAL>toStalk R x ≫ stalkToFiberRingHom R x = algebraMap R (Localization.AtPrime x.asIdeal)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>x : ↑(PrimeSpectrum.Top R)<GOAL>toOpen R ⊤ ≫ openToLocalization R ⊤ ↑⟨x, True.intro⟩ ⋯ = algebraMap R (Localization.AtPrime x.asIdeal)