ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>b : ℝ<VAR>hb : 0 < b<GOAL>Integrable (fun x => rexp (-b * x ^ 2)) volume
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>m✝ : MeasurableSpace α✝<VAR>h : CountablyGenerated α✝<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝ : CountablyGenerated α<GOAL>generateFrom (⋃ n, countablePartition α n) = m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>A✝ : Matrix n n α<VAR>inst✝¹ : RCLike α<VAR>inst✝ : RCLike β<VAR>A : Matrix n n α<VAR>h : A.IsHermitian<VAR>i : n<GOAL>↑(re (A i i)) = A i i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ l₃ : List α<VAR>a b : α<VAR>m n✝ : ℕ<VAR>x✝¹ x✝ : List α<VAR>h : x✝¹ <+ x✝<VAR>n : ℕ<GOAL>drop (n + 1) x✝¹ <+ drop (n + 1) x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ l₃ : List α<VAR>a b : α<VAR>m n✝ : ℕ<VAR>x✝¹ x✝ : List α<VAR>h : x✝¹ <+ x✝<VAR>n : ℕ<GOAL>drop n x✝¹.tail <+ drop n x✝.tail
<VAR>m n k : Nat<VAR>x✝ : m.Coprime k ∧ n.Coprime k<VAR>h : m.Coprime k<VAR>right✝ : n.Coprime k<GOAL>(m * n).Coprime k
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<GOAL>sin (angle x y) = 1 ↔ angle x y = π / 2
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : sin (angle x y) = 1<GOAL>angle x y = π / 2
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : sin (angle x y) = 1<GOAL>√(1 - 1 ^ 2) = 0
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹⁴ : Semiring R<VAR>inst✝¹³ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝¹² : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝¹¹ : AddCommMonoid M₂<VAR>inst✝¹⁰ : AddCommMonoid M₃<VAR>inst✝⁹ : AddCommMonoid M'<VAR>inst✝⁸ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁷ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : Module R M₃<VAR>inst✝⁴ : Module R M'<VAR>f✝ f' : MultilinearMap R M₁ M₂<VAR>M₁' : ι → Type u_1<VAR>inst✝³ : (i : ι) → AddCommMonoid (M₁' i)<VAR>inst✝² : (i : ι) → Module R (M₁' i)<VAR>M₁'' : ι → Type u_2<VAR>inst✝¹ : (i : ι) → AddCommMonoid (M₁'' i)<VAR>inst✝ : (i : ι) → Module R (M₁'' i)<VAR>f : (i : ι) → M₁ i →ₗ[R] M₁' i<VAR>hf : ∀ (i : ι), Surjective ⇑(f i)<VAR>g₁ g₂ : MultilinearMap R M₁' M₂<VAR>h : (fun g => g.compLinearMap f) g₁ = (fun g => g.compLinearMap f) g₂<VAR>x : (i : ι) → M₁' i<GOAL>g₁ x = g₂ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : PredOrder α<VAR>a b : α<VAR>ha : ¬IsMin a<GOAL>Ioo (pred a) b = Ico a b
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<GOAL>bernoulli' 0 = 1
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<GOAL>1 - ∑ k ∈ range 0, ↑(Nat.choose 0 k) / (↑0 - ↑k + 1) * bernoulli' k = 1
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>r✝ : α → β → Prop<VAR>p : γ → δ → Prop<VAR>r : α → α → Prop<VAR>inst✝² : IsTrans α r<VAR>inst✝¹ : IsSymm α r<VAR>s t : Multiset α<VAR>x : α<VAR>inst✝ : DecidablePred (r x)<VAR>h : Rel r s t<GOAL>countP (r x) s = countP (r x) t
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>r✝ : α → β → Prop<VAR>p : γ → δ → Prop<VAR>r : α → α → Prop<VAR>inst✝² : IsTrans α r<VAR>inst✝¹ : IsSymm α r<VAR>x : α<VAR>inst✝ : DecidablePred (r x)<VAR>t : Multiset α<VAR>h : Rel r 0 t<GOAL>countP (r x) 0 = countP (r x) t
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>r✝ : α → β → Prop<VAR>p : γ → δ → Prop<VAR>r : α → α → Prop<VAR>inst✝² : IsTrans α r<VAR>inst✝¹ : IsSymm α r<VAR>x : α<VAR>inst✝ : DecidablePred (r x)<VAR>y : α<VAR>s : Multiset α<VAR>ih : ∀ {t : Multiset α}, Rel r s t → countP (r x) s = countP (r x) t<VAR>t : Multiset α<VAR>h : Rel r (y ::ₘ s) t<GOAL>countP (r x) (y ::ₘ s) = countP (r x) t
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : CommSemiring A'<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R B<VAR>p✝ q : R[X]<VAR>x : A<VAR>p : R[X]<GOAL>p.coeff 0 = (aeval 0) p
<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✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f : ℝ → E<VAR>c ca cb : E<VAR>l l' la la' lb lb' : Filter ℝ<VAR>lt : Filter ι<VAR>a b z : ℝ<VAR>u v ua ub va vb : ι → ℝ<VAR>inst✝¹ : FTCFilter a la la'<VAR>inst✝ : FTCFilter b lb lb'<VAR>hf : IntervalIntegrable f volume a b<VAR>hmeas : StronglyMeasurableAtFilter f (𝓝 a) volume<VAR>ha : Tendsto f (𝓝 a ⊓ ae volume) (𝓝 c)<GOAL>HasStrictDerivAt (fun u => ∫ (x : ℝ) in u..b, f x) (-c) a
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<VAR>j : ι<VAR>hj : e.BoundaryLE j<VAR>inst✝ : e.IsTruncGE<GOAL>False
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<VAR>j : ι<VAR>hj : e.BoundaryLE j<VAR>inst✝ : e.IsTruncGE<VAR>k : ι<VAR>hk : e.f k = c'.next (e.f j)<GOAL>False
<VAR>K : Type u<VAR>inst✝² : CommRing K<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : CharP K p<VAR>x1 x2 y : ℕ × K<VAR>H : R K p x1 x2<VAR>n : ℕ<VAR>x : K<GOAL>R K p ((n, x).1 + y.1, (⇑(frobenius K p))^[y.1] (n, x).2 * (⇑(frobenius K p))^[(n, x).1] y.2) ((n + 1, (frobenius K p) x).1 + y.1, (⇑(frobenius K p))^[y.1] (n + 1, (frobenius K p) x).2 * (⇑(frobenius K p))^[(n + 1, (frobenius K p) x).1] y.2)
<VAR>K : Type u<VAR>inst✝² : CommRing K<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : CharP K p<VAR>x1 x2 y : ℕ × K<VAR>H : R K p x1 x2<VAR>n : ℕ<VAR>x : K<GOAL>R K p ((n, x).1 + y.1, (⇑(frobenius K p))^[y.1] (n, x).2 * (⇑(frobenius K p))^[(n, x).1] y.2) ((n + y.1).succ, (frobenius K p) ((⇑(frobenius K p))^[y.1] x * (⇑(frobenius K p))^[n] y.2))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>I : Finset ι<VAR>κ : ι → Kernel α β<VAR>a : α<GOAL>(∑ i ∈ I, κ i) a = ∑ i ∈ I, (κ i) a
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>inst✝⁵ : Category.{v₁, u₂} D<VAR>i : D ⥤ C<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : Reflective i<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : HasFiniteProducts D<VAR>inst✝ : ExponentialIdeal i<VAR>A B : C<GOAL>prodComparison (reflector i) A B ≫ (bijection i A B ((reflector i).obj (A ⨯ B))) (𝟙 ((reflector i).obj (A ⨯ B))) = 𝟙 ((reflector i).obj (A ⨯ B))
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>inst✝⁵ : Category.{v₁, u₂} D<VAR>i : D ⥤ C<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : Reflective i<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : HasFiniteProducts D<VAR>inst✝ : ExponentialIdeal i<VAR>A B : C<GOAL>(bijection i A B ((reflector i).obj (A ⨯ B))) (𝟙 ((reflector i).obj (A ⨯ B))) ≫ prodComparison (reflector i) A B = 𝟙 ((reflector i).obj A ⨯ (reflector i).obj B)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁵ : DecidableEq α<VAR>inst✝⁴ : DecidableEq N<VAR>inst✝³ : Zero M<VAR>inst✝² : DecidableEq P<VAR>inst✝¹ : Zero P<VAR>inst✝ : Zero N<VAR>F : M → N → P<VAR>F0 : F 0 0 = 0<VAR>f : α →₀ M<VAR>g₁ g₂ : α →₀ N<VAR>hF : ∀ (f : M), Function.Injective fun g => F f g<VAR>a✝ : α<GOAL>a✝ ∈ (zipWith F F0 f g₁).neLocus (zipWith F F0 f g₂) ↔ a✝ ∈ g₁.neLocus g₂
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasZeroMorphisms C<VAR>X✝ Y✝ : C<VAR>f✝ : X✝ ⟶ Y✝<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>c : CokernelCofork f<VAR>hc : IsColimit c<VAR>hf : f = 0<VAR>e : c.pt ≅ Y := hc.coconePointUniqueUpToIso (ofId f hf)<GOAL>IsIso (Cofork.π c)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasZeroMorphisms C<VAR>X✝ Y✝ : C<VAR>f✝ : X✝ ⟶ Y✝<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>c : CokernelCofork f<VAR>hc : IsColimit c<VAR>hf : f = 0<VAR>e : c.pt ≅ Y := hc.coconePointUniqueUpToIso (ofId f hf)<VAR>eq : Cofork.π c ≫ e.hom = 𝟙 Y<GOAL>IsIso (Cofork.π c)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasZeroMorphisms C<VAR>X✝ Y✝ : C<VAR>f✝ : X✝ ⟶ Y✝<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>c : CokernelCofork f<VAR>hc : IsColimit c<VAR>hf : f = 0<VAR>e : c.pt ≅ Y := hc.coconePointUniqueUpToIso (ofId f hf)<VAR>eq : Cofork.π c ≫ e.hom = 𝟙 Y<VAR>this : IsIso (Cofork.π c ≫ e.hom)<GOAL>IsIso (Cofork.π c)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>A : C<VAR>inst✝ : S.HasHomology<VAR>h : S.RightHomologyData<GOAL>(S.rightHomologyIso.symm ≪≫ h.rightHomologyIso).hom ≫ h.ι = (S.rightHomologyIso.inv ≫ S.rightHomologyι) ≫ h.opcyclesIso.hom
<VAR>E : Type u_1<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>P : Type u_2<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>c : P<VAR>r : ℝ<VAR>this : 0 ∈ (univBall c r).source<GOAL>↑(univBall c r).symm c = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x✝ y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>ι : Type u_4<VAR>l : Filter ι<VAR>x : ι → ℝ<VAR>hx : liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤<GOAL>∃ R, ∃ᶠ (n : ι) in l, x n < R
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x✝ y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>ι : Type u_4<VAR>l : Filter ι<VAR>x : ι → ℝ<VAR>hx : liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤<VAR>h : ¬∃ R, ∃ᶠ (n : ι) in l, x n < R<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x✝ y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>ι : Type u_4<VAR>l : Filter ι<VAR>x : ι → ℝ<VAR>hx : liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤<VAR>h : ∀ (x_1 : ℝ), ∀ᶠ (x_2 : ι) in l, x_1 ≤ x x_2<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r✝ p q : ℝ≥0<VAR>x✝ y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>ι : Type u_4<VAR>l : Filter ι<VAR>x : ι → ℝ<VAR>hx : liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤<VAR>h : ∀ (x_1 : ℝ), ∀ᶠ (x_2 : ι) in l, x_1 ≤ x x_2<VAR>r : ℝ≥0<GOAL>∀ᶠ (n : ℝ≥0∞) in map (fun n => ↑(Real.nnabs (x n))) l, ↑r ≤ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r✝ p q : ℝ≥0<VAR>x✝ y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>ι : Type u_4<VAR>l : Filter ι<VAR>x : ι → ℝ<VAR>hx : liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤<VAR>h : ∀ (x_1 : ℝ), ∀ᶠ (x_2 : ι) in l, x_1 ≤ x x_2<VAR>r : ℝ≥0<GOAL>∀ᶠ (a : ι) in l, r ≤ Real.nnabs (x a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>c₁ c₂ : R<VAR>q : Basis A c₁ c₂<GOAL>q.k * q.i = -c₁ • q.j
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)<VAR>h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), ∃ a, i = f ≫ a ∧ j = g ≫ a<VAR>Z : C<VAR>a : Y ⟶ Z<VAR>f₁ : mk (f ≫ a) ⟶ mk a := homMk left ⋯<VAR>f₂ : mk (g ≫ a) ⟶ mk a := homMk right ⋯<GOAL>Zigzag (mk (f ≫ a)) (mk (g ≫ a))
<VAR>b : ℂ<VAR>hb : 0 < b.re<GOAL>∫ (x : ℝ), cexp (-b * ↑x ^ 2) = (↑π / b) ^ (1 / 2)
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0<GOAL>∫ (x : ℝ), cexp (-b * ↑x ^ 2) = (↑π / b) ^ (1 / 2)
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0<GOAL>ContinuousOn (fun {b} => ∫ (x : ℝ), cexp (-b * ↑x ^ 2)) {c | 0 < c.re}
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0<GOAL>ContinuousOn (fun {b} => (↑π / b) ^ (1 / 2)) {c | 0 < c.re}
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0<GOAL>∫ (x : ℝ), cexp (-1 * ↑x ^ 2) = (↑π / 1) ^ (1 / 2)
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0<VAR>c : ℂ<VAR>hc : c ∈ {c | 0 < c.re}<GOAL>((fun {b} => ∫ (x : ℝ), cexp (-b * ↑x ^ 2)) ^ 2) c = ((fun {b} => (↑π / b) ^ (1 / 2)) ^ 2) c
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0<VAR>c : ℂ<VAR>hc : c ∈ {c | 0 < c.re}<GOAL>(↑π / c) ^ (1 / 2) ≠ 0
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>inst✝ : CompactSpace β<VAR>v : Set β<VAR>hv₁ : IsOpen v<VAR>hv₂ : ω f ϕ s ⊆ v<GOAL>∀ᶠ (t : τ) in f, MapsTo (ϕ t) s v
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>inst✝ : CompactSpace β<VAR>v : Set β<VAR>hv₁ : IsOpen v<VAR>hv₂ : ω f ϕ s ⊆ v<VAR>u : Set τ<VAR>hu_mem : u ∈ f<VAR>hu : closure (image2 ϕ u s) ⊆ v<GOAL>∀ᶠ (t : τ) in f, MapsTo (ϕ t) s v
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>inst✝ : CompactSpace β<VAR>v : Set β<VAR>hv₁ : IsOpen v<VAR>hv₂ : ω f ϕ s ⊆ v<VAR>u : Set τ<VAR>hu_mem : u ∈ f<VAR>hu : closure (image2 ϕ u s) ⊆ v<VAR>t : τ<VAR>ht : t ∈ u<VAR>x : α<VAR>hx : x ∈ s<GOAL>ϕ t x ∈ v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoid α<VAR>a b : Associates α<GOAL>a ≤ b * a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoid α<VAR>a b : Associates α<GOAL>a ≤ a * b
<VAR>E : Type u_1<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : T1Space E<VAR>s : Set E<VAR>hsa : Absorbent ℝ s<VAR>hsb : IsVonNBounded ℝ s<VAR>x : E<GOAL>gaugeRescale s s x = x
<VAR>E : Type u_1<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : T1Space E<VAR>s : Set E<VAR>hsa : Absorbent ℝ s<VAR>hsb : IsVonNBounded ℝ s<GOAL>gaugeRescale s s 0 = 0
<VAR>E : Type u_1<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : T1Space E<VAR>s : Set E<VAR>hsa : Absorbent ℝ s<VAR>hsb : IsVonNBounded ℝ s<VAR>x : E<VAR>hx : x ≠ 0<GOAL>gaugeRescale s s x = x
<VAR>E : Type u_1<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : T1Space E<VAR>s : Set E<VAR>hsa : Absorbent ℝ s<VAR>hsb : IsVonNBounded ℝ s<VAR>x : E<VAR>hx : x ≠ 0<GOAL>gauge s x ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β<VAR>s : Set α<GOAL>(range f)ᶜ ⊆ kernImage f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β<VAR>s : Set α<GOAL>kernImage f ∅ ⊆ kernImage f s
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>s : Multiset α<VAR>_l : List α<GOAL>countP p (Quot.mk Setoid.r _l) = 0 ↔ ∀ a ∈ Quot.mk Setoid.r _l, ¬p a
<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>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Set P<VAR>p : P<VAR>hp : p ∈ s<GOAL>vectorSpan k s = Submodule.span k ((fun x => p -ᵥ x) '' s)
<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>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Set P<VAR>p : P<VAR>hp : p ∈ s<GOAL>Submodule.span k (s -ᵥ s) = Submodule.span k ((fun x => p -ᵥ x) '' s)
<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>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Set P<VAR>p : P<VAR>hp : p ∈ s<GOAL>Submodule.span k (s -ᵥ s) ≤ Submodule.span k ((fun x => p -ᵥ x) '' s)
<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>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Set P<VAR>p : P<VAR>hp : p ∈ s<GOAL>(fun x => p -ᵥ x) '' s ⊆ s -ᵥ s
<VAR>A : Type u_1<VAR>inst✝⁸ : PartialOrder A<VAR>inst✝⁷ : NormedRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : TopologicalRing A<VAR>inst✝³ : NormedAlgebra ℝ A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>inst✝ : UniqueContinuousFunctionalCalculus ℝ A<VAR>r : ℝ<VAR>a : A<VAR>ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x<VAR>hr : 0 < r<VAR>ha₁ : autoParam (IsSelfAdjoint a) _auto✝<GOAL>log (r • a) = (algebraMap ℝ A) (Real.log r) + log a
<VAR>A : Type u_1<VAR>inst✝⁸ : PartialOrder A<VAR>inst✝⁷ : NormedRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : TopologicalRing A<VAR>inst✝³ : NormedAlgebra ℝ A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>inst✝ : UniqueContinuousFunctionalCalculus ℝ A<VAR>r : ℝ<VAR>a : A<VAR>ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x<VAR>hr : 0 < r<VAR>ha₁ : autoParam (IsSelfAdjoint a) _auto✝<VAR>this : ∀ x ∈ spectrum ℝ a, x ≠ 0<GOAL>log (r • a) = (algebraMap ℝ A) (Real.log r) + log a
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹¹ : CommRing S<VAR>inst✝¹⁰ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁹ : CommRing P<VAR>Rₘ : Type u_4<VAR>Sₘ : Type u_5<VAR>inst✝⁸ : CommRing Rₘ<VAR>inst✝⁷ : CommRing Sₘ<VAR>inst✝⁶ : Algebra R Rₘ<VAR>inst✝⁵ : IsLocalization M Rₘ<VAR>inst✝⁴ : Algebra S Sₘ<VAR>i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>inst✝³ : Algebra Rₘ Sₘ<VAR>inst✝² : Algebra R Sₘ<VAR>inst✝¹ : IsScalarTower R Rₘ Sₘ<VAR>inst✝ : IsScalarTower R S Sₘ<VAR>x : R<GOAL>(algebraMap Rₘ Sₘ) ((algebraMap R Rₘ) x) = (algebraMap S Sₘ) ((algebraMap R S) x)
<VAR>R✝ : Type u_1<VAR>inst✝⁷ : CommSemiring R✝<VAR>M : Submonoid R✝<VAR>S✝ : Type u_2<VAR>inst✝⁶ : CommSemiring S✝<VAR>inst✝⁵ : Algebra R✝ S✝<VAR>P : Type u_3<VAR>inst✝⁴ : CommSemiring P<VAR>inst✝³ : IsLocalization M S✝<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>e : R<VAR>he : IsIdempotentElem e<VAR>H : RingHom.ker (algebraMap R S) = Ideal.span {1 - e}<VAR>H' : Function.Surjective ⇑(algebraMap R S)<VAR>r : ↥(Submonoid.powers e)<GOAL>IsUnit ((algebraMap R S) ↑r)
<VAR>R✝ : Type u_1<VAR>inst✝⁷ : CommSemiring R✝<VAR>M : Submonoid R✝<VAR>S✝ : Type u_2<VAR>inst✝⁶ : CommSemiring S✝<VAR>inst✝⁵ : Algebra R✝ S✝<VAR>P : Type u_3<VAR>inst✝⁴ : CommSemiring P<VAR>inst✝³ : IsLocalization M S✝<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>e : R<VAR>he : IsIdempotentElem e<VAR>H : RingHom.ker (algebraMap R S) = Ideal.span {1 - e}<VAR>H' : Function.Surjective ⇑(algebraMap R S)<VAR>r : ↥(Submonoid.powers e)<VAR>this : (algebraMap R S) e = 1<GOAL>IsUnit ((algebraMap R S) ↑r)
<VAR>R✝ : Type u_1<VAR>inst✝⁷ : CommSemiring R✝<VAR>M : Submonoid R✝<VAR>S✝ : Type u_2<VAR>inst✝⁶ : CommSemiring S✝<VAR>inst✝⁵ : Algebra R✝ S✝<VAR>P : Type u_3<VAR>inst✝⁴ : CommSemiring P<VAR>inst✝³ : IsLocalization M S✝<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>e : R<VAR>he : IsIdempotentElem e<VAR>H : RingHom.ker (algebraMap R S) = Ideal.span {1 - e}<VAR>H' : Function.Surjective ⇑(algebraMap R S)<VAR>x y : R<VAR>h : (algebraMap R S) x = (algebraMap R S) y<GOAL>∃ c, ↑c * x = ↑c * y
<VAR>R✝ : Type u_1<VAR>inst✝⁷ : CommSemiring R✝<VAR>M : Submonoid R✝<VAR>S✝ : Type u_2<VAR>inst✝⁶ : CommSemiring S✝<VAR>inst✝⁵ : Algebra R✝ S✝<VAR>P : Type u_3<VAR>inst✝⁴ : CommSemiring P<VAR>inst✝³ : IsLocalization M S✝<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>e : R<VAR>he : IsIdempotentElem e<VAR>H : RingHom.ker (algebraMap R S) = Ideal.span {1 - e}<VAR>H' : Function.Surjective ⇑(algebraMap R S)<VAR>x y : R<VAR>h : 1 - e ∣ x - y<GOAL>∃ c, ↑c * x = ↑c * y
<VAR>R✝ : Type u_1<VAR>inst✝⁷ : CommSemiring R✝<VAR>M : Submonoid R✝<VAR>S✝ : Type u_2<VAR>inst✝⁶ : CommSemiring S✝<VAR>inst✝⁵ : Algebra R✝ S✝<VAR>P : Type u_3<VAR>inst✝⁴ : CommSemiring P<VAR>inst✝³ : IsLocalization M S✝<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>e : R<VAR>he : IsIdempotentElem e<VAR>H : RingHom.ker (algebraMap R S) = Ideal.span {1 - e}<VAR>H' : Function.Surjective ⇑(algebraMap R S)<VAR>x y k : R<VAR>hk : x - y = (1 - e) * k<GOAL>∃ c, ↑c * x = ↑c * y
<VAR>R✝ : Type u_1<VAR>inst✝⁷ : CommSemiring R✝<VAR>M : Submonoid R✝<VAR>S✝ : Type u_2<VAR>inst✝⁶ : CommSemiring S✝<VAR>inst✝⁵ : Algebra R✝ S✝<VAR>P : Type u_3<VAR>inst✝⁴ : CommSemiring P<VAR>inst✝³ : IsLocalization M S✝<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>e : R<VAR>he : IsIdempotentElem e<VAR>H : RingHom.ker (algebraMap R S) = Ideal.span {1 - e}<VAR>H' : Function.Surjective ⇑(algebraMap R S)<VAR>x y k : R<VAR>hk : x - y = (1 - e) * k<GOAL>↑⟨e, ⋯⟩ * x = ↑⟨e, ⋯⟩ * y
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>P : Finpartition univ<VAR>u : Finset α<VAR>ε✝ : ℝ<VAR>l✝ : ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>l : ℕ<GOAL>100 < 4 ^ initialBound ε l * ε ^ 5
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>P : Finpartition univ<VAR>u : Finset α<VAR>ε✝ : ℝ<VAR>l✝ : ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>l : ℕ<GOAL>log (100 / ε ^ 5) / log 4 < max (↑7) (max ↑l ↑(⌊log (100 / ε ^ 5) / log 4⌋₊ + 1))
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>P : Finpartition univ<VAR>u : Finset α<VAR>ε✝ : ℝ<VAR>l✝ : ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>l : ℕ<GOAL>0 < log 4
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>P : Finpartition univ<VAR>u : Finset α<VAR>ε✝ : ℝ<VAR>l✝ : ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>l : ℕ<GOAL>0 < 100 / ε ^ 5
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>L' : Type w₁<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>I J : LieIdeal R L<VAR>f : L' →ₗ⁅R⁆ L<GOAL>IsLieAbelian ↥↑I ↔ D 1 I = ⊥
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>v : Vector α (n + 1)<VAR>f : α → β<GOAL>(map f v).tail = map f v.tail
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>v : Vector α (n + 1)<VAR>f : α → β<VAR>a : α<VAR>v' : Vector α n<VAR>h : v = a ::ᵥ v'<GOAL>(map f v).tail = map f v.tail
<VAR>α : Type u_1<VAR>l l₁ l₂ : List α<VAR>p : α → Prop<VAR>a : α<VAR>inst✝ : DecidableEq α<GOAL>(∀ (x : α), x ∈ l₁ ∪ l₂ → p x) ↔ (∀ (x : α), x ∈ l₁ → p x) ∧ ∀ (x : α), x ∈ l₂ → p x
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>k : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : LieRingModule L M₂<VAR>inst✝¹ : LieModule R L M₂<VAR>inst✝ : IsNilpotent R L M<VAR>h : ¬IsTrivial L M<GOAL>(match nilpotencyLength R L M with | 0 => ⊥ | k.succ => lowerCentralSeries R L M k) ≤ lowerCentralSeries R L M 1
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>k : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : LieRingModule L M₂<VAR>inst✝¹ : LieModule R L M₂<VAR>inst✝ : IsNilpotent R L M<VAR>h : 1 < nilpotencyLength R L M<GOAL>(match nilpotencyLength R L M with | 0 => ⊥ | k.succ => lowerCentralSeries R L M k) ≤ lowerCentralSeries R L M 1
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : IsPurelyInseparable F E<GOAL>insepDegree F E = Module.rank F E
<VAR>B : Type u_1<VAR>inst✝⁶ : TopologicalSpace B<VAR>F₁ : Type u_2<VAR>inst✝⁵ : TopologicalSpace F₁<VAR>E₁ : B → Type u_3<VAR>inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_4<VAR>inst✝³ : TopologicalSpace F₂<VAR>E₂ : B → Type u_5<VAR>inst✝² : TopologicalSpace (TotalSpace F₂ E₂)<VAR>e₁ : Trivialization F₁ TotalSpace.proj<VAR>e₂ : Trivialization F₂ TotalSpace.proj<VAR>inst✝¹ : (x : B) → Zero (E₁ x)<VAR>inst✝ : (x : B) → Zero (E₂ x)<GOAL>ContinuousOn (invFun' e₁ e₂) ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)