ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝²² : NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>inst✝²¹ : NormedAddCommGroup EB<VAR>inst✝²⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝¹⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>inst✝¹⁸ : TopologicalSpace B<VAR>inst✝¹⁷ : ChartedSpace HB B<VAR>inst✝¹⁶ : SmoothManifoldWithCorners IB B<VAR>EM : Type u_9<VAR>inst✝¹⁵ : NormedAddCommGroup EM<VAR>inst✝¹⁴ : NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>inst✝¹³ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝¹² : TopologicalSpace M<VAR>inst✝¹¹ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝¹⁰ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁹ : (x : B) → Module 𝕜 (E x)<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : TopologicalSpace (TotalSpace F E)<VAR>inst✝⁵ : (x : B) → TopologicalSpace (E x)<VAR>inst✝⁴ : FiberBundle F E<VAR>inst✝³ : VectorBundle 𝕜 F E<VAR>inst✝² : SmoothVectorBundle F E IB<VAR>e e' : Trivialization F TotalSpace.proj<VAR>inst✝¹ : MemTrivializationAtlas e<VAR>inst✝ : MemTrivializationAtlas e'<VAR>s : Set M<VAR>f✝ : M → B<VAR>g : M → F<VAR>x : M<VAR>f : M → TotalSpace F E<VAR>hp : ContMDiffWithinAt IM IB n (TotalSpace.proj ∘ f) s x<VAR>hf : ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun y => (↑e (f y)).2) s x<VAR>he : (f x).proj ∈ e.baseSet<VAR>he' : (f x).proj ∈ e'.baseSet<GOAL>ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun y => (↑e' (f y)).2) s x
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝²² : NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>inst✝²¹ : NormedAddCommGroup EB<VAR>inst✝²⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝¹⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>inst✝¹⁸ : TopologicalSpace B<VAR>inst✝¹⁷ : ChartedSpace HB B<VAR>inst✝¹⁶ : SmoothManifoldWithCorners IB B<VAR>EM : Type u_9<VAR>inst✝¹⁵ : NormedAddCommGroup EM<VAR>inst✝¹⁴ : NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>inst✝¹³ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝¹² : TopologicalSpace M<VAR>inst✝¹¹ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝¹⁰ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁹ : (x : B) → Module 𝕜 (E x)<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : TopologicalSpace (TotalSpace F E)<VAR>inst✝⁵ : (x : B) → TopologicalSpace (E x)<VAR>inst✝⁴ : FiberBundle F E<VAR>inst✝³ : VectorBundle 𝕜 F E<VAR>inst✝² : SmoothVectorBundle F E IB<VAR>e e' : Trivialization F TotalSpace.proj<VAR>inst✝¹ : MemTrivializationAtlas e<VAR>inst✝ : MemTrivializationAtlas e'<VAR>s : Set M<VAR>f✝ : M → B<VAR>g : M → F<VAR>x : M<VAR>f : M → TotalSpace F E<VAR>hp : ContMDiffWithinAt IM IB n (TotalSpace.proj ∘ f) s x<VAR>hf : ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun y => (↑e (f y)).2) s x<VAR>he : (f x).proj ∈ e.baseSet<VAR>he' : (f x).proj ∈ e'.baseSet<GOAL>(fun y => (↑e' (f y)).2) =ᶠ[𝓝[s] x] fun y => e.coordChange e' ((TotalSpace.proj ∘ f) y) (↑e (f y)).2
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝²² : NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>inst✝²¹ : NormedAddCommGroup EB<VAR>inst✝²⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝¹⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>inst✝¹⁸ : TopologicalSpace B<VAR>inst✝¹⁷ : ChartedSpace HB B<VAR>inst✝¹⁶ : SmoothManifoldWithCorners IB B<VAR>EM : Type u_9<VAR>inst✝¹⁵ : NormedAddCommGroup EM<VAR>inst✝¹⁴ : NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>inst✝¹³ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝¹² : TopologicalSpace M<VAR>inst✝¹¹ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝¹⁰ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁹ : (x : B) → Module 𝕜 (E x)<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : TopologicalSpace (TotalSpace F E)<VAR>inst✝⁵ : (x : B) → TopologicalSpace (E x)<VAR>inst✝⁴ : FiberBundle F E<VAR>inst✝³ : VectorBundle 𝕜 F E<VAR>inst✝² : SmoothVectorBundle F E IB<VAR>e e' : Trivialization F TotalSpace.proj<VAR>inst✝¹ : MemTrivializationAtlas e<VAR>inst✝ : MemTrivializationAtlas e'<VAR>s : Set M<VAR>f✝ : M → B<VAR>g : M → F<VAR>x : M<VAR>f : M → TotalSpace F E<VAR>hp : ContMDiffWithinAt IM IB n (TotalSpace.proj ∘ f) s x<VAR>hf : ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun y => (↑e (f y)).2) s x<VAR>he : (f x).proj ∈ e.baseSet<VAR>he' : (f x).proj ∈ e'.baseSet<GOAL>(↑e' (f x)).2 = e.coordChange e' ((TotalSpace.proj ∘ f) x) (↑e (f x)).2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁵ : CommRing R<VAR>M✝ N : Matrix m m R<VAR>b : m → α<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>M : Matrix m m R<VAR>p : m → Prop<VAR>inst✝ : DecidablePred p<GOAL>M.det = (fromBlocks (M.toBlock p p) (M.toBlock p fun j => ¬p j) (M.toBlock (fun j => ¬p j) p) (M.toBlock (fun j => ¬p j) fun j => ¬p j)).det
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁵ : CommRing R<VAR>M✝ N : Matrix m m R<VAR>b : m → α<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>M : Matrix m m R<VAR>p : m → Prop<VAR>inst✝ : DecidablePred p<GOAL>((reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M).det = (fromBlocks (M.toBlock p p) (M.toBlock p fun j => ¬p j) (M.toBlock (fun j => ¬p j) p) (M.toBlock (fun j => ¬p j) fun j => ¬p j)).det
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁵ : CommRing R<VAR>M✝ N : Matrix m m R<VAR>b : m → α<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>M : Matrix m m R<VAR>p : m → Prop<VAR>inst✝ : DecidablePred p<GOAL>∑ σ : Equiv.Perm ({ a // p a } ⊕ { a // ¬p a }), ↑↑(Equiv.Perm.sign σ) * ∏ i : { a // p a } ⊕ { a // ¬p a }, (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M (σ i) i = ∑ σ : Equiv.Perm ({ a // p a } ⊕ { a // ¬p a }), ↑↑(Equiv.Perm.sign σ) * ∏ i : { a // p a } ⊕ { a // ¬p a }, fromBlocks (M.toBlock p p) (M.toBlock p fun j => ¬p j) (M.toBlock (fun j => ¬p j) p) (M.toBlock (fun j => ¬p j) fun j => ¬p j) (σ i) i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁵ : CommRing R<VAR>M✝ N : Matrix m m R<VAR>b : m → α<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>M : Matrix m m R<VAR>p : m → Prop<VAR>inst✝ : DecidablePred p<VAR>σ : Equiv.Perm ({ a // p a } ⊕ { a // ¬p a })<VAR>x y : { a // p a } ⊕ { a // ¬p a }<VAR>hy : σ x = y<GOAL>(reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M y x = fromBlocks (M.toBlock p p) (M.toBlock p fun j => ¬p j) (M.toBlock (fun j => ¬p j) p) (M.toBlock (fun j => ¬p j) fun j => ¬p j) y x
<VAR>a b m n k : ℕ<VAR>p : ℕ → Prop<VAR>H' : ¬p 0<VAR>H : ∃ n, p n<GOAL>∃ n, ¬p n ∧ p (n + 1)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k m n : ℕ<VAR>u v w : R<VAR>hkm : k < m<VAR>hmn : m < n<VAR>hw : w ≠ 0<GOAL>(trinomial k m n u v w).natDegree = n
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k m n : ℕ<VAR>u v w : R<VAR>hkm : k < m<VAR>hmn : m < n<VAR>hw : w ≠ 0<VAR>i : ℕ<VAR>h : i ∈ (trinomial k m n u v w).support<GOAL>↑i ≤ ↑n
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k m n : ℕ<VAR>u v w : R<VAR>hkm : k < m<VAR>hmn : m < n<VAR>hw : w ≠ 0<VAR>i : ℕ<VAR>h : i ∈ {k, m, n}<GOAL>↑i ≤ ↑n
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k m n : ℕ<VAR>u v w : R<VAR>hkm : k < m<VAR>hmn : m < n<VAR>hw : w ≠ 0<VAR>i : ℕ<VAR>h : i = k ∨ i = m ∨ i = n<GOAL>↑i ≤ ↑n
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>inst✝³ : Monoid M<VAR>inst✝² : LinearOrder M<VAR>inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : M<VAR>h : a ^ 2 ≤ b * c<GOAL>a ≤ max b c
<VAR>E : Type uE<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<VAR>s : Set M<VAR>hsc : IsClosed s<VAR>hs : s ⊆ support ↑f<VAR>e : PartialEquiv M E := extChartAt I c<GOAL>∃ r ∈ Ioo 0 f.rOut, s ⊆ (chartAt H c).source ∩ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) r
<VAR>E : Type uE<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<VAR>s : Set M<VAR>hsc : IsClosed s<VAR>hs : s ⊆ support ↑f<VAR>e : PartialEquiv M E := extChartAt I c<VAR>this : IsClosed (↑e '' s)<GOAL>∃ r ∈ Ioo 0 f.rOut, s ⊆ (chartAt H c).source ∩ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) r
<VAR>E : Type uE<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<VAR>s : Set M<VAR>hsc : IsClosed s<VAR>hs : s ⊆ (chartAt H c).source ∧ ↑(extChartAt I c) '' s ⊆ ball (↑(extChartAt I c) c) f.rOut<VAR>e : PartialEquiv M E := extChartAt I c<VAR>this : IsClosed (↑e '' s)<GOAL>∃ r ∈ Ioo 0 f.rOut, s ⊆ (chartAt H c).source ∩ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) r
<VAR>E : Type uE<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<VAR>s : Set M<VAR>hsc : IsClosed s<VAR>hs : s ⊆ (chartAt H c).source ∧ ↑(extChartAt I c) '' s ⊆ ball (↑(extChartAt I c) c) f.rOut<VAR>e : PartialEquiv M E := extChartAt I c<VAR>this : IsClosed (↑e '' s)<VAR>r : ℝ<VAR>hrR : r ∈ Ioo 0 f.rOut<VAR>hr : ↑e '' s ⊆ ball (↑(extChartAt I c) c) r<GOAL>∃ r ∈ Ioo 0 f.rOut, s ⊆ (chartAt H c).source ∩ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : One β<VAR>f : α → β<VAR>s : Set α<VAR>hs : ∀ a ∈ frontier s, f a = 1<VAR>hf : ContinuousOn f (closure s)<GOAL>Continuous (s.mulIndicator f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set ℕ<VAR>inst✝ : Infinite ↑s<VAR>x : ↑s<VAR>h : ¬∃ n, ↑x + n + 1 ∈ s<VAR>a : ℕ<VAR>ha : a ∈ s<VAR>hax : a ≥ ↑x + 1<GOAL>↑x + (a - (↑x + 1)) + 1 ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set ℕ<VAR>inst✝ : Infinite ↑s<VAR>x : ↑s<VAR>h : ¬∃ n, ↑x + n + 1 ∈ s<VAR>this : ∀ a ∈ s, a < ↑x + 1<GOAL>∀ a ∈ Multiset.filter (fun x => x ∈ s) (Multiset.range (↑x).succ), a ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set ℕ<VAR>inst✝ : Infinite ↑s<VAR>x : ↑s<VAR>h : ¬∃ n, ↑x + n + 1 ∈ s<VAR>this : ∀ a ∈ s, a < ↑x + 1<GOAL>∀ (x_1 : { y // y ∈ s }), x_1 ∈ (Multiset.pmap (fun y hy => ⟨y, hy⟩) (Multiset.filter (fun x => x ∈ s) (Multiset.range (↑x).succ)) ⋯).toFinset
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NontriviallyNormedField 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>x : 𝕜<GOAL>logDeriv id x = 1 / x
<VAR>S : ShortComplex Ab<VAR>x : ↑S.X₁<GOAL>((AddCommGrp.kernelIsLimit S.g).lift (Limits.KernelFork.ofι S.f ⋯) ≫ QuotientAddGroup.mk' S.abToCycles.range) x = 0 x
<VAR>S : ShortComplex Ab<VAR>x : ↑S.X₁<GOAL>((AddCommGrp.kernelIsLimit S.g).lift (Limits.KernelFork.ofι S.f ⋯)) x ∈ S.abToCycles.range
<VAR>S : ShortComplex Ab<VAR>x : ↑S.X₁<GOAL>∃ x_1, S.abToCycles x_1 = ((AddCommGrp.kernelIsLimit S.g).lift (Limits.KernelFork.ofι S.f ⋯)) x
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>inst✝ : Preorder α<VAR>s : Finset α<VAR>c : α<VAR>hcs : c ∈ s<GOAL>∃ m ∈ s, ∀ x ∈ s, ¬x < m
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>inst✝ : Preorder α<VAR>s : Finset α<VAR>c : α<VAR>hcs : c ∈ s<VAR>this : WellFounded LT.lt<GOAL>∃ m ∈ s, ∀ x ∈ s, ¬x < m
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>inst✝ : Preorder α<VAR>s : Finset α<VAR>c : α<VAR>hcs : c ∈ s<VAR>this : WellFounded LT.lt<VAR>m : α<VAR>hms : m ∈ s<VAR>H : ∀ x ∈ Set.univ, ¬x < ⟨m, hms⟩<GOAL>∃ m ∈ s, ∀ x ∈ s, ¬x < m
<VAR>R✝ : Type u<VAR>S : Type u_1<VAR>inst✝¹ : Ring R✝<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>n : ℕ<GOAL>(map (algebraMap (↥(Subring.closure ↑p.coeffs)) R) p.restriction).coeff n = p.coeff n
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ∠ p₁ p₂ p₃ = π / 2<GOAL>Real.tan (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₃ p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫_ℝ = 0<GOAL>Real.tan (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₃ p₂
<VAR>X : Type u_1<VAR>inst✝³ : NormedAddCommGroup X<VAR>M : Type u_2<VAR>inst✝² : Ring M<VAR>inst✝¹ : Module M X<VAR>inst✝ : FaithfulSMul M X<VAR>P Q R : { P // IsLprojection X P }<GOAL>(↑P + ↑Pᶜ * ↑R) * (↑P + ↑Q * ↑R * ↑Pᶜ) = ↑P + ↑Q * ↑R * ↑Pᶜ
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>U V : Set E<VAR>hU : U ∈ p.basisSets<VAR>hV : V ∈ p.basisSets<GOAL>∃ z ∈ p.basisSets, z ⊆ U ∩ V
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>r : Cofix F → Cofix F → Prop<VAR>h : ∀ (x y : Cofix F), r x y → Liftr r x.dest y.dest<GOAL>∀ (x y : Cofix F), r x y → x = y
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>r : Cofix F → Cofix F → Prop<VAR>h : ∀ (x y : Cofix F), r x y → Liftr r x.dest y.dest<GOAL>∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>r : Cofix F → Cofix F → Prop<VAR>h : ∀ (x y : Cofix F), r x y → Liftr r x.dest y.dest<VAR>x y : Cofix F<VAR>rxy : r x y<GOAL>Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>r : Cofix F → Cofix F → Prop<VAR>h : ∀ (x y : Cofix F), r x y → Liftr r x.dest y.dest<VAR>x y : Cofix F<VAR>rxy : r x y<VAR>a : (P F).A<VAR>f₀ f₁ : (P F).B a → Cofix F<VAR>dxeq : x.dest = abs ⟨a, f₀⟩<VAR>dyeq : y.dest = abs ⟨a, f₁⟩<VAR>h' : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)<GOAL>Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>r : Cofix F → Cofix F → Prop<VAR>h : ∀ (x y : Cofix F), r x y → Liftr r x.dest y.dest<VAR>x y : Cofix F<VAR>rxy : r x y<VAR>a : (P F).A<VAR>f₀ f₁ : (P F).B a → Cofix F<VAR>dxeq : x.dest = abs ⟨a, f₀⟩<VAR>dyeq : y.dest = abs ⟨a, f₁⟩<VAR>h' : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)<GOAL>abs ⟨a, Quot.mk r ∘ f₀⟩ = abs ⟨a, Quot.mk r ∘ f₁⟩
<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>s : AffineSubspace k P<VAR>v : V<VAR>hv : v ∈ s.direction<VAR>p : P<GOAL>v +ᵥ p ∈ s ↔ p ∈ 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>s : AffineSubspace k P<VAR>v : V<VAR>hv : v ∈ s.direction<VAR>p : P<VAR>h : v +ᵥ p ∈ s<GOAL>p ∈ 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>s : AffineSubspace k P<VAR>v : V<VAR>hv : v ∈ s.direction<VAR>p : P<VAR>h : v +ᵥ p ∈ s<GOAL>p = -v +ᵥ (v +ᵥ p)
<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✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : CommRing M<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : Algebra R L<VAR>inst✝ : Algebra R M<VAR>x : L<VAR>int : IsIntegral R x<VAR>h : Splits (algebraMap R K) (minpoly R x)<VAR>f : K →ₐ[R] L<GOAL>x ∈ ⇑f '' ?m.29144
<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✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : CommRing M<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : Algebra R L<VAR>inst✝ : Algebra R M<VAR>x : L<VAR>int : IsIntegral R x<VAR>h : Splits (algebraMap R K) (minpoly R x)<VAR>f : K →ₐ[R] L<GOAL>Polynomial.map (algebraMap R L) (minpoly R x) ≠ 0 ∧ (aeval x) (minpoly R x) = 0
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>f : α ↪ β<VAR>s : Finset α<VAR>t : Finset β<GOAL>map f s ⊆ t ↔ s ⊆ t.preimage ⇑f ⋯
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>h : μ = 0<VAR>this : f =ᶠ[ae μ] 0<GOAL>setToFun μ T hT f = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>r : Set β<VAR>hf : BijOn f s t<VAR>hrt : r ⊆ t<GOAL>BijOn f (s ∩ f ⁻¹' r) r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>r : Set β<VAR>hf : BijOn f s t<VAR>hrt : r ⊆ t<VAR>x : β<VAR>hx : x ∈ r<GOAL>x ∈ f '' (s ∩ f ⁻¹' r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>r : Set β<VAR>hf : BijOn f s t<VAR>hrt : r ⊆ t<VAR>y : α<VAR>hy : y ∈ s<VAR>hx : f y ∈ r<GOAL>f y ∈ f '' (s ∩ f ⁻¹' r)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>u : ℕ → Set E := fun n => disjointed (spanningSets μ) n<GOAL>∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤ μ (f '' s)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>u : ℕ → Set E := fun n => disjointed (spanningSets μ) n<VAR>u_meas : ∀ (n : ℕ), MeasurableSet (u n)<GOAL>∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤ μ (f '' s)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>u : ℕ → Set E := fun n => disjointed (spanningSets μ) n<VAR>u_meas : ∀ (n : ℕ), MeasurableSet (u n)<VAR>A : s = ⋃ n, s ∩ u n<GOAL>∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤ μ (f '' s)
<VAR>M₀ : Type u_1<VAR>G₀ : Type u_2<VAR>inst✝ : GroupWithZero G₀<VAR>s : Set G₀<VAR>a b : G₀<VAR>ha : a ∈ s.centralizer<GOAL>a⁻¹ ∈ s.centralizer
<VAR>M₀ : Type u_1<VAR>G₀ : Type u_2<VAR>inst✝ : GroupWithZero G₀<VAR>s : Set G₀<VAR>b : G₀<VAR>ha : 0 ∈ s.centralizer<GOAL>0⁻¹ ∈ s.centralizer
<VAR>M₀ : Type u_1<VAR>G₀ : Type u_2<VAR>inst✝ : GroupWithZero G₀<VAR>s : Set G₀<VAR>a b : G₀<VAR>ha : a ∈ s.centralizer<VAR>ha₀ : a ≠ 0<GOAL>a⁻¹ ∈ s.centralizer
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h₁ : min a b ≤ max c d<VAR>h₂ : min c d ≤ max a b<GOAL>Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>hab : a ≤ b<VAR>hcd : c ≤ d<VAR>h₁ : a ≤ d<VAR>h₂ : c ≤ b<GOAL>Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>hab : a ≤ b<VAR>hcd : d ≤ c<VAR>h₁ : a ≤ c<VAR>h₂ : d ≤ b<GOAL>Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>hab : b ≤ a<VAR>hcd : c ≤ d<VAR>h₁ : b ≤ d<VAR>h₂ : c ≤ a<GOAL>Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>hab : b ≤ a<VAR>hcd : d ≤ c<VAR>h₁ : b ≤ c<VAR>h₂ : d ≤ a<GOAL>Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Set α<VAR>t t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>d d' : δ<GOAL>image2 f (s ∩ s') (t ∪ t') ⊆ image2 f s t ∪ image2 f s' t'
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Set α<VAR>t t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>d d' : δ<GOAL>image2 f (s ∩ s') t ∪ image2 f (s ∩ s') t' ⊆ image2 f s t ∪ image2 f s' t'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>f g : CauSeq α abs<VAR>hf : f.LimZero<VAR>hg : g.LimZero<VAR>ε : α<VAR>ε0 : ε > 0<VAR>i : ℕ<VAR>H : ∀ j ≥ i, |↑f j| < ε ∧ |↑g j| < ε<VAR>j : ℕ<VAR>ij : j ≥ i<VAR>H₁ : |↑f j| < ε<VAR>H₂ : |↑g j| < ε<GOAL>|↑(f ⊔ g) j| < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>f g : CauSeq α abs<VAR>hf : f.LimZero<VAR>hg : g.LimZero<VAR>ε : α<VAR>ε0 : ε > 0<VAR>i : ℕ<VAR>H : ∀ j ≥ i, |↑f j| < ε ∧ |↑g j| < ε<VAR>j : ℕ<VAR>ij : j ≥ i<VAR>H₁ : -ε < ↑f j ∧ ↑f j < ε<VAR>H₂ : -ε < ↑g j ∧ ↑g j < ε<GOAL>-ε < ↑(f ⊔ g) j ∧ ↑(f ⊔ g) j < ε
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>m : ℕ<VAR>x : 𝕎 R<GOAL>truncateFun n (m • x) = m • truncateFun n x
<VAR>a b c : ℕ<GOAL>Fintype.card ↑(Set.Ioo a b) = b - a - 1