ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type u<VAR>G : Type v<VAR>X : Type w<VAR>inst✝⁶ : PseudoEMetricSpace X<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MulAction G X<VAR>inst✝³ : IsometricSMul G X<VAR>inst✝² : DivInvMonoid M<VAR>inst✝¹ : PseudoEMetricSpace M<VAR>inst✝ : IsometricSMul Mᵐᵒᵖ M<VAR>a b c : M<GOAL>edist (a / c) (b / c) = edist a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ : Finset ℕ<VAR>n : ℕ<VAR>hn : 2 ≤ n<VAR>s t : Finset ℕ<VAR>hst : { ofColex := s } < { ofColex := t }<GOAL>(fun s => ∑ k ∈ s.ofColex, n ^ k) { ofColex := s } < (fun s => ∑ k ∈ s.ofColex, n ^ k) { ofColex := t }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ : Finset ℕ<VAR>n : ℕ<VAR>hn : 2 ≤ n<VAR>s t : Finset ℕ<VAR>hst : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a<GOAL>(fun s => ∑ k ∈ s.ofColex, n ^ k) { ofColex := s } < (fun s => ∑ k ∈ s.ofColex, n ^ k) { ofColex := t }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ : Finset ℕ<VAR>n : ℕ<VAR>hn : 2 ≤ n<VAR>s t : Finset ℕ<VAR>a : ℕ<VAR>hat : a ∈ t<VAR>has : a ∉ s<VAR>ha : ∀ b ∈ s, b ∉ t → b < a<GOAL>(fun s => ∑ k ∈ s.ofColex, n ^ k) { ofColex := s } < (fun s => ∑ k ∈ s.ofColex, n ^ k) { ofColex := t }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ : Finset ℕ<VAR>n : ℕ<VAR>hn : 2 ≤ n<VAR>s t : Finset ℕ<VAR>a : ℕ<VAR>hat : a ∈ t<VAR>has : a ∉ s<VAR>ha : ∀ b ∈ s, b ∉ t → b < a<GOAL>∑ i ∈ { ofColex := s }.ofColex \ { ofColex := t }.ofColex, n ^ i < ∑ i ∈ { ofColex := t }.ofColex \ { ofColex := s }.ofColex, n ^ i
<VAR>K : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : DivisionRing L<VAR>inst✝ : DivisionRing M<VAR>S : Set (Subfield K)<VAR>x : K<GOAL>x ∈ ↑(sInf (toSubring '' S)) ↔ x ∈ ⋂ s ∈ S, ↑s
<VAR>K : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : DivisionRing L<VAR>inst✝ : DivisionRing M<VAR>S : Set (Subfield K)<VAR>x : K<GOAL>(∀ (i : Subring K), x ∈ ⋂ (_ : i ∈ toSubring '' S), ↑i) ↔ ∀ (i : Subfield K), x ∈ ⋂ (_ : i ∈ S), ↑i
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIocDiv hp (a + p) b = toIocDiv hp a b - 1
<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝⁴ : PseudoEMetricSpace α✝<VAR>inst✝³ : PseudoEMetricSpace β<VAR>inst✝² : PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>f✝ : α✝ → β<VAR>x y : α✝<VAR>r : ℝ≥0∞<VAR>α : ι → Type u<VAR>inst✝¹ : (i : ι) → PseudoEMetricSpace (α i)<VAR>inst✝ : Fintype ι<VAR>i : ι<VAR>f g : (x : ι) → α x<GOAL>edist (eval i f) (eval i g) ≤ edist f g
<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>T : Type u_3<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>g : S →+* T<VAR>f : R →+* S<VAR>hf₂ : (algebraMap R T).SurjectiveOnStalks<VAR>x : S ⊗[R] T<VAR>J : Ideal T<VAR>hJ : J.IsPrime<GOAL>∃ t r a, r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁸ : Category.{u_3, u_1} C<VAR>inst✝⁷ : Category.{u_4, u_2} D<VAR>inst✝⁶ : HasZeroMorphisms C<VAR>inst✝⁵ : HasZeroMorphisms D<VAR>S : ShortComplex C<VAR>h₁✝ : S.LeftHomologyData<VAR>h₂✝ : S.RightHomologyData<VAR>F✝ : C ⥤ D<VAR>inst✝⁴ : F✝.PreservesZeroMorphisms<VAR>hl : S.LeftHomologyData<VAR>hr : S.RightHomologyData<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hl₁ : S₁.LeftHomologyData<VAR>hr₁ : S₁.RightHomologyData<VAR>hl₂ : S₂.LeftHomologyData<VAR>hr₂ : S₂.RightHomologyData<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>F : C ⥤ D<VAR>inst✝³ : F.PreservesZeroMorphisms<VAR>inst✝² : S.HasHomology<VAR>inst✝¹ : (S.map F).HasHomology<VAR>inst✝ : F.PreservesLeftHomologyOf S<GOAL>leftHomologyMap' (𝟙 (S.map F)) (S.map F).homologyData.left (S.map F).leftHomologyData ≫ leftHomologyMap' (𝟙 (S.map F)) (S.map F).leftHomologyData (S.homologyData.left.map F) = (leftHomologyMap' (𝟙 (S.map F)) (S.map F).homologyData.left (S.map F).leftHomologyData ≫ leftHomologyMap' (𝟙 (S.map F)) (S.map F).leftHomologyData (hl.map F)) ≫ F.map (leftHomologyMap' (𝟙 S) hl S.leftHomologyData ≫ leftHomologyMap' (𝟙 S) S.leftHomologyData S.homologyData.left)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<VAR>x : α<VAR>F : Set α<VAR>hs : IsPreconnected s<VAR>hxs : x ∈ s<VAR>hsF : s ⊆ F<GOAL>s ⊆ connectedComponentIn F x
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<VAR>x : α<VAR>F : Set α<VAR>hs : IsPreconnected s<VAR>hxs : x ∈ s<VAR>hsF : s ⊆ F<VAR>this : IsPreconnected (Subtype.val ⁻¹' s)<GOAL>s ⊆ connectedComponentIn F x
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<VAR>x : α<VAR>F : Set α<VAR>hs : IsPreconnected s<VAR>hxs : x ∈ s<VAR>hsF : s ⊆ F<VAR>this : IsPreconnected (Subtype.val ⁻¹' s)<VAR>h2xs : ⟨x, ⋯⟩ ∈ Subtype.val ⁻¹' s<GOAL>s ⊆ connectedComponentIn F x
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<VAR>x : α<VAR>F : Set α<VAR>hs : IsPreconnected s<VAR>hxs : x ∈ s<VAR>hsF : s ⊆ F<VAR>this✝ : IsPreconnected (Subtype.val ⁻¹' s)<VAR>h2xs : ⟨x, ⋯⟩ ∈ Subtype.val ⁻¹' s<VAR>this : Subtype.val ⁻¹' s ⊆ connectedComponent ⟨x, ⋯⟩<GOAL>s ⊆ connectedComponentIn F x
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<VAR>x : α<VAR>F : Set α<VAR>hs : IsPreconnected s<VAR>hxs : x ∈ s<VAR>hsF : s ⊆ F<VAR>this✝ : IsPreconnected (Subtype.val ⁻¹' s)<VAR>h2xs : ⟨x, ⋯⟩ ∈ Subtype.val ⁻¹' s<VAR>this : Subtype.val ⁻¹' s ⊆ connectedComponent ⟨x, ⋯⟩<GOAL>s ⊆ Subtype.val '' connectedComponent ⟨x, ⋯⟩
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<VAR>x : α<VAR>F : Set α<VAR>hs : IsPreconnected s<VAR>hxs : x ∈ s<VAR>hsF : s ⊆ F<VAR>this✝ : IsPreconnected (Subtype.val ⁻¹' s)<VAR>h2xs : ⟨x, ⋯⟩ ∈ Subtype.val ⁻¹' s<VAR>this : Subtype.val ⁻¹' s ⊆ connectedComponent ⟨x, ⋯⟩<GOAL>s ⊆ Subtype.val '' (Subtype.val ⁻¹' s)
<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 : M<VAR>inst✝ : Nontrivial R<VAR>i : ι<VAR>s : Set ι<GOAL>b i ∈ span R (⇑b '' s) ↔ i ∈ s
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>r✝ : R<VAR>f p : R[X]<VAR>r : R<GOAL>((taylor r) p).natDegree = p.natDegree
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>r✝ : R<VAR>f p : R[X]<VAR>r : R<GOAL>∀ (n : ℕ) (c : R), c ≠ 0 → ((taylor r) ((monomial n) c)).natDegree = n
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>r✝ : R<VAR>f p : R[X]<VAR>r : R<VAR>a✝ : Nontrivial R<VAR>n : ℕ<VAR>c : R<VAR>c0 : c ≠ 0<GOAL>((taylor r) ((monomial n) c)).natDegree = n
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : StrictOrderedSemiring R<VAR>a x y : R<VAR>n✝ m : ℕ<VAR>h : 1 < a<VAR>this : 0 < a<VAR>n : ℕ<GOAL>a ^ n < a ^ (n + 1)
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : Preorder α<VAR>a b c d : α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : MulPosMono α<VAR>inst✝¹ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ha : a ≤ 0<VAR>hb : b ≤ 0<GOAL>0 ≤ a * b
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁸ : NontriviallyNormedField R<VAR>inst✝⁷ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁶ : (x : B) → Module R (E x)<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace R F<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace (TotalSpace F E)<VAR>inst✝¹ : (x : B) → TopologicalSpace (E x)<VAR>inst✝ : FiberBundle F E<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<VAR>b : B<VAR>a : F<VAR>i j : ι<GOAL>{ proj := b, snd := a } ∈ (Z.localTrivAt b).source
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁸ : NontriviallyNormedField R<VAR>inst✝⁷ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁶ : (x : B) → Module R (E x)<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace R F<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace (TotalSpace F E)<VAR>inst✝¹ : (x : B) → TopologicalSpace (E x)<VAR>inst✝ : FiberBundle F E<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<VAR>b : B<VAR>a : F<VAR>i j : ι<GOAL>{ proj := b, snd := a }.proj ∈ Z.baseSet (Z.indexAt b)
<VAR>ι : Type u_1<VAR>E : ι → Type u_2<VAR>inst✝ : (i : ι) → MetricSpace (E i)<VAR>fst✝¹ : ι<VAR>snd✝¹ : E fst✝¹<VAR>fst✝ : ι<VAR>snd✝ : E fst✝<VAR>h : dist ⟨fst✝¹, snd✝¹⟩ ⟨fst✝, snd✝⟩ < 1<GOAL>⟨fst✝¹, snd✝¹⟩.fst = ⟨fst✝, snd✝⟩.fst
<VAR>ι : Type u_1<VAR>E : ι → Type u_2<VAR>inst✝ : (i : ι) → MetricSpace (E i)<VAR>fst✝¹ : ι<VAR>snd✝¹ : E fst✝¹<VAR>fst✝ : ι<VAR>snd✝ : E fst✝<VAR>h : ⟨fst✝¹, snd✝¹⟩.fst ≠ ⟨fst✝, snd✝⟩.fst<GOAL>1 ≤ dist ⟨fst✝¹, snd✝¹⟩ ⟨fst✝, snd✝⟩
<VAR>a b : ℤ<VAR>b0 : ¬b = 0<VAR>n : ℤ<VAR>d : ℕ<VAR>h : d ≠ 0<VAR>c : n.natAbs.Coprime d<VAR>e : a /. b = { num := n, den := d, den_nz := h, reduced := c }<GOAL>↑{ num := n, den := d, den_nz := h, reduced := c }.den ∣ b
<VAR>a b : ℤ<VAR>b0 : ¬b = 0<VAR>n : ℤ<VAR>d : ℕ<VAR>h : d ≠ 0<VAR>c : n.natAbs.Coprime d<VAR>e : a * ↑d = n * b<GOAL>↑{ num := n, den := d, den_nz := h, reduced := c }.den ∣ b
<VAR>a b : ℤ<VAR>b0 : ¬b = 0<VAR>n : ℤ<VAR>d : ℕ<VAR>h : d ≠ 0<VAR>c : n.natAbs.Coprime d<VAR>e : a * ↑d = n * b<GOAL>d ∣ n.natAbs * b.natAbs
<VAR>a b : ℤ<VAR>b0 : ¬b = 0<VAR>n : ℤ<VAR>d : ℕ<VAR>h : d ≠ 0<VAR>c : n.natAbs.Coprime d<VAR>e : a * ↑d = n * b<GOAL>↑d ∣ a * ↑d
<VAR>p✝ q✝ : ℚ≥0<VAR>n₁ n₂ d₁ d₂ d : ℕ<VAR>p q : ℚ≥0<GOAL>p ≤ q ↔ p.num * q.den ≤ q.num * p.den
<VAR>p✝ q✝ : ℚ≥0<VAR>n₁ n₂ d₁ d₂ d : ℕ<VAR>p q : ℚ≥0<GOAL>(↑p).num * ↑(↑q).den ≤ (↑q).num * ↑(↑p).den ↔ p.num * q.den ≤ q.num * p.den
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>inst✝⁹ : Semiring R₁<VAR>inst✝⁸ : Semiring R₂<VAR>inst✝⁷ : Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>M₃ : Type u_6<VAR>inst✝⁶ : TopologicalSpace M₁<VAR>inst✝⁵ : TopologicalSpace M₂<VAR>inst✝⁴ : TopologicalSpace M₃<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : Module R₁ M₁<VAR>inst✝¹ : AddCommMonoid M₂<VAR>inst✝ : Module R₂ M₂<VAR>f : M₂ → M₃<VAR>hf : IsCompactOperator f<VAR>g : M₁ →SL[σ₁₂] M₂<GOAL>IsCompactOperator (f ∘ ⇑g)
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>inst✝⁹ : Semiring R₁<VAR>inst✝⁸ : Semiring R₂<VAR>inst✝⁷ : Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>M₃ : Type u_6<VAR>inst✝⁶ : TopologicalSpace M₁<VAR>inst✝⁵ : TopologicalSpace M₂<VAR>inst✝⁴ : TopologicalSpace M₃<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : Module R₁ M₁<VAR>inst✝¹ : AddCommMonoid M₂<VAR>inst✝ : Module R₂ M₂<VAR>f : M₂ → M₃<VAR>hf : IsCompactOperator f<VAR>g : M₁ →SL[σ₁₂] M₂<VAR>this : Tendsto (⇑g) (𝓝 0) (𝓝 (g 0))<GOAL>IsCompactOperator (f ∘ ⇑g)
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>inst✝⁹ : Semiring R₁<VAR>inst✝⁸ : Semiring R₂<VAR>inst✝⁷ : Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>M₃ : Type u_6<VAR>inst✝⁶ : TopologicalSpace M₁<VAR>inst✝⁵ : TopologicalSpace M₂<VAR>inst✝⁴ : TopologicalSpace M₃<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : Module R₁ M₁<VAR>inst✝¹ : AddCommMonoid M₂<VAR>inst✝ : Module R₂ M₂<VAR>f : M₂ → M₃<VAR>hf : IsCompactOperator f<VAR>g : M₁ →SL[σ₁₂] M₂<VAR>this : Tendsto (⇑g) (𝓝 0) (𝓝 0)<GOAL>IsCompactOperator (f ∘ ⇑g)
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>x : E<VAR>y : F<VAR>H : ∀ (c : R), c • x = 0 → c • y = 0<VAR>h : x ∈ (mkSpanSingleton' x y H).domain<GOAL>↑(mkSpanSingleton' x y H) ⟨x, h⟩ = y
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>x : E<VAR>y : F<VAR>H : ∀ (c : R), c • x = 0 → c • y = 0<VAR>h : x ∈ (mkSpanSingleton' x y H).domain<VAR>this : ↑(mkSpanSingleton' x y H) ⟨1 • x, ⋯⟩ = 1 • y<GOAL>↑(mkSpanSingleton' x y H) ⟨x, h⟩ = y
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ dt : ℝ<GOAL>IsIntegralCurveAt γ v t₀ ↔ IsIntegralCurveAt (γ ∘ fun x => x + dt) v (t₀ - dt)
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ dt : ℝ<VAR>hγ : IsIntegralCurveAt (γ ∘ fun x => x + dt) v (t₀ - dt)<GOAL>IsIntegralCurveAt γ v t₀
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ dt : ℝ<VAR>hγ : IsIntegralCurveAt (γ ∘ fun x => x + dt) v (t₀ - dt)<GOAL>γ = (γ ∘ fun x => x + dt) ∘ fun x => x + -dt
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ dt : ℝ<VAR>hγ : IsIntegralCurveAt (γ ∘ fun x => x + dt) v (t₀ - dt)<GOAL>t₀ = t₀ - dt - -dt
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>h : Subsingleton α<GOAL>∀ (x y : α), x = y
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>M N : Submodule R A<VAR>m n : A<VAR>I : Submodule R A<GOAL>I * (1 / I) ≤ 1
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>M N : Submodule R A<VAR>m n : A<VAR>I : Submodule R A<GOAL>∀ m ∈ I, ∀ n ∈ 1 / I, m * n ∈ 1
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>M N : Submodule R A<VAR>m✝ n✝ : A<VAR>I : Submodule R A<VAR>m : A<VAR>hm : m ∈ I<VAR>n : A<VAR>hn : n ∈ 1 / I<GOAL>m * n ∈ 1
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>M N : Submodule R A<VAR>m✝ n✝ : A<VAR>I : Submodule R A<VAR>m : A<VAR>hm : m ∈ I<VAR>n : A<VAR>hn : ∀ y ∈ I, n * y ∈ 1<GOAL>m * n ∈ 1
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>M N : Submodule R A<VAR>m✝ n✝ : A<VAR>I : Submodule R A<VAR>m : A<VAR>hm : m ∈ I<VAR>n : A<VAR>hn : ∀ y ∈ I, n * y ∈ 1<GOAL>n * m ∈ 1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : CommSemiring R<VAR>S : Set M<VAR>hS : closure S = ⊤<VAR>f : R[M]<GOAL>∃ a, (MvPolynomial.aeval fun s => of' R M ↑s) a = f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : CommSemiring R<VAR>S : Set M<VAR>hS : closure S = ⊤<VAR>m : M<GOAL>∃ a, (MvPolynomial.aeval fun s => of' R M ↑s) a = (of R M) (Multiplicative.ofAdd m)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : CommSemiring R<VAR>S : Set M<VAR>hS : closure S = ⊤<VAR>f g : R[M]<VAR>ihf : ∃ a, (MvPolynomial.aeval fun s => of' R M ↑s) a = f<VAR>ihg : ∃ a, (MvPolynomial.aeval fun s => of' R M ↑s) a = g<GOAL>∃ a, (MvPolynomial.aeval fun s => of' R M ↑s) a = f + g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : CommSemiring R<VAR>S : Set M<VAR>hS : closure S = ⊤<VAR>r : R<VAR>f : R[M]<VAR>ih : ∃ a, (MvPolynomial.aeval fun s => of' R M ↑s) a = f<GOAL>∃ a, (MvPolynomial.aeval fun s => of' R M ↑s) a = r • f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : EDist α<VAR>x y : α<VAR>s t : Set α<GOAL>edist x y ⊓ edist y x ≤ {x, y}.einfsep
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : EDist α<VAR>x y : α<VAR>s t : Set α<GOAL>∀ (x_1 : α), x_1 = x ∨ x_1 = y → ∀ (y_1 : α), y_1 = x ∨ y_1 = y → x_1 ≠ y_1 → edist x y ≤ edist x_1 y_1 ∨ edist y x ≤ edist x_1 y_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : Group α<VAR>inst✝ : UniformGroup α<VAR>s : Set α<GOAL>(∀ i ∈ 𝓝 1, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ {x | x.2⁻¹ * x.1 ∈ id i}}) ↔ ∀ U ∈ 𝓝 1, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, y • U
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>A : Cᵒᵖ ⥤ Type v<VAR>inst✝¹ : IsFiltered (CostructuredArrow yoneda A)<VAR>inst✝ : FinallySmall (CostructuredArrow yoneda A)<GOAL>IsIndObject A
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>A : Cᵒᵖ ⥤ Type v<VAR>inst✝¹ : IsFiltered (CostructuredArrow yoneda A)<VAR>inst✝ : FinallySmall (CostructuredArrow yoneda A)<VAR>h₁ : (factoring (fromFinalModel (CostructuredArrow yoneda A)) ⋙ inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final<GOAL>IsIndObject A
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>A : Cᵒᵖ ⥤ Type v<VAR>inst✝¹ : IsFiltered (CostructuredArrow yoneda A)<VAR>inst✝ : FinallySmall (CostructuredArrow yoneda A)<VAR>h₁ : (factoring (fromFinalModel (CostructuredArrow yoneda A)) ⋙ inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final<VAR>h₂ : (inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final<GOAL>IsIndObject A
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>A : Cᵒᵖ ⥤ Type v<VAR>inst✝¹ : IsFiltered (CostructuredArrow yoneda A)<VAR>inst✝ : FinallySmall (CostructuredArrow yoneda A)<VAR>h₁ : (factoring (fromFinalModel (CostructuredArrow yoneda A)) ⋙ inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final<VAR>h₂ : (inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final<VAR>c : Cocone (inclusion (fromFinalModel (CostructuredArrow yoneda A)) ⋙ CostructuredArrow.proj yoneda A ⋙ yoneda) := Cocone.whisker (inclusion (fromFinalModel (CostructuredArrow yoneda A))) (Presheaf.tautologicalCocone A)<VAR>hc : IsColimit c := (Functor.Final.isColimitWhiskerEquiv (inclusion (fromFinalModel (CostructuredArrow yoneda A))) (Presheaf.tautologicalCocone A)).symm (Presheaf.isColimitTautologicalCocone A)<GOAL>IsIndObject A
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>A : Cᵒᵖ ⥤ Type v<VAR>inst✝¹ : IsFiltered (CostructuredArrow yoneda A)<VAR>inst✝ : FinallySmall (CostructuredArrow yoneda A)<VAR>h₁ : (factoring (fromFinalModel (CostructuredArrow yoneda A)) ⋙ inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final<VAR>h₂ : (inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final<VAR>c : Cocone (inclusion (fromFinalModel (CostructuredArrow yoneda A)) ⋙ CostructuredArrow.proj yoneda A ⋙ yoneda) := Cocone.whisker (inclusion (fromFinalModel (CostructuredArrow yoneda A))) (Presheaf.tautologicalCocone A)<VAR>hc : IsColimit c := (Functor.Final.isColimitWhiskerEquiv (inclusion (fromFinalModel (CostructuredArrow yoneda A))) (Presheaf.tautologicalCocone A)).symm (Presheaf.isColimitTautologicalCocone A)<VAR>hq : Nonempty (FinalModel (CostructuredArrow yoneda A))<GOAL>IsIndObject A
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_5, u_2} D<VAR>L✝ : C ⥤ D<VAR>W✝ : MorphismProperty C<VAR>E : Type u_3<VAR>inst✝¹ : Category.{?u.65248, u_3} E<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>hW : W ≤ MorphismProperty.isomorphisms C<VAR>inst✝ : L.IsEquivalence<GOAL>L.IsLocalization W
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_5, u_2} D<VAR>L✝ : C ⥤ D<VAR>W✝ : MorphismProperty C<VAR>E : Type u_3<VAR>inst✝¹ : Category.{?u.65248, u_3} E<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>hW : W ≤ MorphismProperty.isomorphisms C<VAR>inst✝ : L.IsEquivalence<VAR>this : (𝟭 C).IsLocalization W<GOAL>L.IsLocalization W
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : DecidableEq L<VAR>inst✝⁷ : Algebra R K<VAR>inst✝⁶ : IsFractionRing R K<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra R L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsDedekindDomain R<VAR>I J : ↥(Ideal R)⁰<GOAL>mk0 I = mk0 J ↔ ∃ x y, ∃ (_ : x ≠ 0) (_ : y ≠ 0), Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : DecidableEq L<VAR>inst✝⁷ : Algebra R K<VAR>inst✝⁶ : IsFractionRing R K<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra R L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsDedekindDomain R<VAR>I J : ↥(Ideal R)⁰<GOAL>(∃ x, ∃ (_ : x ≠ 0), spanSingleton R⁰ x * ↑↑I = ↑↑J) → ∃ x y, ∃ (_ : x ≠ 0) (_ : y ≠ 0), Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : DecidableEq L<VAR>inst✝⁷ : Algebra R K<VAR>inst✝⁶ : IsFractionRing R K<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra R L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsDedekindDomain R<VAR>I J : ↥(Ideal R)⁰<GOAL>(∃ x y, ∃ (_ : x ≠ 0) (_ : y ≠ 0), Ideal.span {x} * ↑I = Ideal.span {y} * ↑J) → ∃ x, ∃ (_ : x ≠ 0), spanSingleton R⁰ x * ↑↑I = ↑↑J
<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 Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2<GOAL>W.add P Q = addZ P Q • ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)), W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)), 1]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : SuccOrder α<VAR>a b : α<VAR>h : a ≤ succ b<GOAL>Icc a (succ b) = insert (succ b) (Icc a b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : DecidableEq β<VAR>f✝ g : α → β<VAR>s✝ : Finset α<VAR>t : Finset β<VAR>a✝ : α<VAR>b c : β<VAR>inst✝ : DecidableEq α<VAR>f : α → β<VAR>hf : Injective f<VAR>s : Finset α<VAR>a : α<GOAL>↑(image f (s.erase a)) = ↑((image f s).erase (f a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : DecidableEq β<VAR>f✝ g : α → β<VAR>s✝ : Finset α<VAR>t : Finset β<VAR>a✝ : α<VAR>b c : β<VAR>inst✝ : DecidableEq α<VAR>f : α → β<VAR>hf : Injective f<VAR>s : Finset α<VAR>a : α<GOAL>f '' ↑s \ {f a} = f '' ↑s \ {f a}
<VAR>a x z : ℂ<GOAL>I.arg = π / 2
<VAR>x✝ y x : ℝ<GOAL>0 ≤ π / 2 - arcsin x
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝³ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝² : NormedRing 𝕜<VAR>inst✝¹ : (i : α) → Module 𝕜 (E i)<VAR>inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>f : (i : α) → E i<VAR>hf : Memℓp f p<VAR>c : 𝕜<GOAL>Memℓp (c • f) p
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>q : ℝ≥0∞<VAR>inst✝³ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝² : NormedRing 𝕜<VAR>inst✝¹ : (i : α) → Module 𝕜 (E i)<VAR>inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>f : (i : α) → E i<VAR>c : 𝕜<VAR>hf : Memℓp f 0<GOAL>Memℓp (c • f) 0