ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>K✝ : Type u_2<VAR>inst✝¹³ : Field F<VAR>inst✝¹² : Field K✝<VAR>inst✝¹¹ : Algebra F K✝<VAR>K₁ : Type u_3<VAR>K₂ : Type u_4<VAR>K₃ : Type u_5<VAR>inst✝¹⁰ : Field F<VAR>inst✝⁹ : Field K₁<VAR>inst✝⁸ : Field K₂<VAR>inst✝⁷ : Field K₃<VAR>inst✝⁶ : Algebra F K₁<VAR>inst✝⁵ : Algebra F K₂<VAR>inst✝⁴ : Algebra F K₃<VAR>ϕ : K₁ →ₐ[F] K₂<VAR>χ : K₁ ≃ₐ[F] K₂<VAR>ψ : K₂ →ₐ[F] K₃<VAR>ω : K₂ ≃ₐ[F] K₃<VAR>K : Type u_6<VAR>L : Type u_7<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Normal K L<VAR>x y : L<VAR>hy : IsAlgebraic K y<VAR>h_ev : (Polynomial.aeval x) (minpoly K y) = 0<VAR>σ : L ≃ₐ[K] L<VAR>hσ : σ x = y<GOAL>∃ σ, σ y = x
<VAR>F : Type u_1<VAR>K✝ : Type u_2<VAR>inst✝¹³ : Field F<VAR>inst✝¹² : Field K✝<VAR>inst✝¹¹ : Algebra F K✝<VAR>K₁ : Type u_3<VAR>K₂ : Type u_4<VAR>K₃ : Type u_5<VAR>inst✝¹⁰ : Field F<VAR>inst✝⁹ : Field K₁<VAR>inst✝⁸ : Field K₂<VAR>inst✝⁷ : Field K₃<VAR>inst✝⁶ : Algebra F K₁<VAR>inst✝⁵ : Algebra F K₂<VAR>inst✝⁴ : Algebra F K₃<VAR>ϕ : K₁ →ₐ[F] K₂<VAR>χ : K₁ ≃ₐ[F] K₂<VAR>ψ : K₂ →ₐ[F] K₃<VAR>ω : K₂ ≃ₐ[F] K₃<VAR>K : Type u_6<VAR>L : Type u_7<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Normal K L<VAR>x y : L<VAR>hy : IsAlgebraic K y<VAR>h_ev : (Polynomial.aeval x) (minpoly K y) = 0<VAR>σ : L ≃ₐ[K] L<VAR>hσ : σ x = y<GOAL>σ.symm y = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ inst✝ : PseudoEMetricSpace α<VAR>f : ℕ → α<VAR>d : ℕ → ℝ≥0<VAR>hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)<VAR>hd : Summable d<GOAL>CauchySeq f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ inst✝ : PseudoEMetricSpace α<VAR>f : ℕ → α<VAR>d : ℕ → ℝ≥0<VAR>hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)<VAR>hd : Summable d<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<GOAL>∃ N, ∀ (n : ℕ), N ≤ n → edist (f n) (f N) < ↑ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ inst✝ : PseudoEMetricSpace α<VAR>f : ℕ → α<VAR>d : ℕ → ℝ≥0<VAR>hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>hd : CauchySeq fun n => ∑ x ∈ Finset.range n, d x<GOAL>∃ N, ∀ (n : ℕ), N ≤ n → edist (f n) (f N) < ↑ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ inst✝ : PseudoEMetricSpace α<VAR>f : ℕ → α<VAR>d : ℕ → ℝ≥0<VAR>hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>hd : CauchySeq fun n => ∑ x ∈ Finset.range n, d x<VAR>N : ℕ<VAR>hN : ∀ n ≥ N, dist (∑ x ∈ Finset.range n, d x) (∑ x ∈ Finset.range N, d x) < ↑ε<VAR>n : ℕ<VAR>hn : N ≤ n<GOAL>edist (f n) (f N) < ↑ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ inst✝ : PseudoEMetricSpace α<VAR>f : ℕ → α<VAR>d : ℕ → ℝ≥0<VAR>hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>hd : CauchySeq fun n => ∑ x ∈ Finset.range n, d x<VAR>N n : ℕ<VAR>hn : N ≤ n<VAR>hN : dist (∑ x ∈ Finset.range n, d x) (∑ x ∈ Finset.range N, d x) < ↑ε<GOAL>edist (f n) (f N) < ↑ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ inst✝ : PseudoEMetricSpace α<VAR>f : ℕ → α<VAR>d : ℕ → ℝ≥0<VAR>hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>hd : CauchySeq fun n => ∑ x ∈ Finset.range n, d x<VAR>N n : ℕ<VAR>hn : N ≤ n<VAR>hN : ∑ k ∈ Finset.Ico N n, d k < ε ∧ ∑ x ∈ Finset.range N, d x - (∑ k ∈ Finset.range N, d k + ∑ k ∈ Finset.Ico N n, d k) < ε<GOAL>edist (f n) (f N) < ↑ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ inst✝ : PseudoEMetricSpace α<VAR>f : ℕ → α<VAR>d : ℕ → ℝ≥0<VAR>hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>hd : CauchySeq fun n => ∑ x ∈ Finset.range n, d x<VAR>N n : ℕ<VAR>hn : N ≤ n<VAR>hN : ∑ k ∈ Finset.Ico N n, d k < ε ∧ ∑ x ∈ Finset.range N, d x - (∑ k ∈ Finset.range N, d k + ∑ k ∈ Finset.Ico N n, d k) < ε<GOAL>edist (f N) (f n) < ↑ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ inst✝ : PseudoEMetricSpace α<VAR>f : ℕ → α<VAR>d : ℕ → ℝ≥0<VAR>hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>hd : CauchySeq fun n => ∑ x ∈ Finset.range n, d x<VAR>N n : ℕ<VAR>hn : N ≤ n<VAR>hN : ∑ k ∈ Finset.Ico N n, d k < ε ∧ ∑ x ∈ Finset.range N, d x - (∑ k ∈ Finset.range N, d k + ∑ k ∈ Finset.Ico N n, d k) < ε<GOAL>∑ i ∈ Finset.Ico N n, ↑(d i) < ↑ε
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<GOAL>s ∈ 𝓓 a 𝒜 → s.erase a ∈ 𝓓 a 𝒜
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<GOAL>s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s ∉ 𝒜 ∧ insert a s ∈ 𝒜 → s.erase a ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s.erase a ∉ 𝒜 ∧ insert a (s.erase a) ∈ 𝒜
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<VAR>h : s ∉ 𝒜 ∧ insert a s ∈ 𝒜<GOAL>s.erase a ∉ 𝒜 ∧ insert a (s.erase a) ∈ 𝒜
<VAR>a b : ℤ<GOAL>Fintype.card ↑(Set.Ico a b) = (b - a).toNat
<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>I : Set ι<VAR>hI : I.Finite<VAR>s : (i : ι) → Set (π i)<VAR>x : (i : ι) → π i<GOAL>𝓝[I.pi s] x = ⨅ i, comap (fun x => x i) (𝓝 (x i) ⊓ ⨅ (_ : i ∈ I), 𝓟 (s i))
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hf : Integrable f μ<VAR>hm : m ≤ m0<VAR>hsig : SigmaFinite (μ.trim hm)<GOAL>eLpNorm (μ[f|m]) 1 μ ≤ eLpNorm f 1 μ
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : Algebra R S<VAR>P : Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>inst✝¹¹ : CommRing R'<VAR>inst✝¹⁰ : CommRing S'<VAR>inst✝⁹ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝⁸ : Algebra R R'<VAR>inst✝⁷ : Algebra S S'<VAR>inst✝⁶ : Algebra R S'<VAR>inst✝⁵ : IsScalarTower R R' S'<VAR>inst✝⁴ : IsScalarTower R S S'<VAR>T : Type uT<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>f g : P.Hom P'<VAR>x y : P.Ring<VAR>this : Algebra P.Ring S' := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra<GOAL>f.toAlgHom (x * y) - g.toAlgHom (x * y) - (P'.σ ((algebraMap P.Ring S') x) * (f.toAlgHom y - g.toAlgHom y) + P'.σ ((algebraMap P.Ring S') y) * (f.toAlgHom x - g.toAlgHom x)) ∈ P'.ker ^ 2
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : Algebra R S<VAR>P : Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>inst✝¹¹ : CommRing R'<VAR>inst✝¹⁰ : CommRing S'<VAR>inst✝⁹ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝⁸ : Algebra R R'<VAR>inst✝⁷ : Algebra S S'<VAR>inst✝⁶ : Algebra R S'<VAR>inst✝⁵ : IsScalarTower R R' S'<VAR>inst✝⁴ : IsScalarTower R S S'<VAR>T : Type uT<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>f g : P.Hom P'<VAR>x y : P.Ring<VAR>this✝ : Algebra P.Ring S' := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra<VAR>this : (f.toAlgHom x - P'.σ ((algebraMap P.Ring S') x)) * (f.toAlgHom y - g.toAlgHom y) + (g.toAlgHom y - P'.σ ((algebraMap P.Ring S') y)) * (f.toAlgHom x - g.toAlgHom x) ∈ P'.ker ^ 2<GOAL>f.toAlgHom (x * y) - g.toAlgHom (x * y) - (P'.σ ((algebraMap P.Ring S') x) * (f.toAlgHom y - g.toAlgHom y) + P'.σ ((algebraMap P.Ring S') y) * (f.toAlgHom x - g.toAlgHom x)) ∈ P'.ker ^ 2
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : Algebra R S<VAR>P : Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>inst✝¹¹ : CommRing R'<VAR>inst✝¹⁰ : CommRing S'<VAR>inst✝⁹ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝⁸ : Algebra R R'<VAR>inst✝⁷ : Algebra S S'<VAR>inst✝⁶ : Algebra R S'<VAR>inst✝⁵ : IsScalarTower R R' S'<VAR>inst✝⁴ : IsScalarTower R S S'<VAR>T : Type uT<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>f g : P.Hom P'<VAR>x y : P.Ring<VAR>this✝ : Algebra P.Ring S' := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra<VAR>this : (f.toAlgHom x - P'.σ ((algebraMap P.Ring S') x)) * (f.toAlgHom y - g.toAlgHom y) + (g.toAlgHom y - P'.σ ((algebraMap P.Ring S') y)) * (f.toAlgHom x - g.toAlgHom x) ∈ P'.ker ^ 2<GOAL>f.toAlgHom (x * y) - g.toAlgHom (x * y) - (P'.σ ((algebraMap P.Ring S') x) * (f.toAlgHom y - g.toAlgHom y) + P'.σ ((algebraMap P.Ring S') y) * (f.toAlgHom x - g.toAlgHom x)) = (f.toAlgHom x - P'.σ ((algebraMap P.Ring S') x)) * (f.toAlgHom y - g.toAlgHom y) + (g.toAlgHom y - P'.σ ((algebraMap P.Ring S') y)) * (f.toAlgHom x - g.toAlgHom x)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : Algebra R S<VAR>P : Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>inst✝¹¹ : CommRing R'<VAR>inst✝¹⁰ : CommRing S'<VAR>inst✝⁹ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝⁸ : Algebra R R'<VAR>inst✝⁷ : Algebra S S'<VAR>inst✝⁶ : Algebra R S'<VAR>inst✝⁵ : IsScalarTower R R' S'<VAR>inst✝⁴ : IsScalarTower R S S'<VAR>T : Type uT<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>f g : P.Hom P'<VAR>x y : P.Ring<VAR>this✝ : Algebra P.Ring S' := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra<VAR>this : (f.toAlgHom x - P'.σ ((algebraMap P.Ring S') x)) * (f.toAlgHom y - g.toAlgHom y) + (g.toAlgHom y - P'.σ ((algebraMap P.Ring S') y)) * (f.toAlgHom x - g.toAlgHom x) ∈ P'.ker ^ 2<GOAL>f.toAlgHom x * f.toAlgHom y - g.toAlgHom x * g.toAlgHom y - (P'.σ ((algebraMap P.Ring S') x) * (f.toAlgHom y - g.toAlgHom y) + P'.σ ((algebraMap P.Ring S') y) * (f.toAlgHom x - g.toAlgHom x)) = (f.toAlgHom x - P'.σ ((algebraMap P.Ring S') x)) * (f.toAlgHom y - g.toAlgHom y) + (g.toAlgHom y - P'.σ ((algebraMap P.Ring S') y)) * (f.toAlgHom x - g.toAlgHom x)
<VAR>C : Type u<VAR>inst✝¹² : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝¹¹ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝¹⁰ : Category.{max v u, w₂} E<VAR>F✝ : D ⥤ E<VAR>inst✝⁹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁸ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝⁷ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F✝<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝⁶ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝⁵ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝⁴ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F✝<VAR>F G : D ⥤ E<VAR>η : F ⟶ G<VAR>P : Cᵒᵖ ⥤ D<VAR>inst✝³ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>inst✝² : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>inst✝¹ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ G<VAR>inst✝ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan G<VAR>X : Cᵒᵖ<GOAL>(whiskerLeft (J.plusObj P) η ≫ (J.plusCompIso G P).hom).app X = ((J.plusCompIso F P).hom ≫ J.plusMap (whiskerLeft P η)).app X
<VAR>C : Type u<VAR>inst✝¹² : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝¹¹ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝¹⁰ : Category.{max v u, w₂} E<VAR>F✝ : D ⥤ E<VAR>inst✝⁹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁸ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝⁷ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F✝<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝⁶ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝⁵ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝⁴ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F✝<VAR>F G : D ⥤ E<VAR>η : F ⟶ G<VAR>P : Cᵒᵖ ⥤ D<VAR>inst✝³ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>inst✝² : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>inst✝¹ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ G<VAR>inst✝ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan G<VAR>X : Cᵒᵖ<GOAL>∀ (j : (J.Cover (unop X))ᵒᵖ), (F.mapCocone (colimit.cocone (J.diagram P (unop X)))).ι.app j ≫ (whiskerLeft (J.plusObj P) η ≫ (J.plusCompIso G P).hom).app X = (F.mapCocone (colimit.cocone (J.diagram P (unop X)))).ι.app j ≫ ((J.plusCompIso F P).hom ≫ J.plusMap (whiskerLeft P η)).app X
<VAR>C : Type u<VAR>inst✝¹² : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝¹¹ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝¹⁰ : Category.{max v u, w₂} E<VAR>F✝ : D ⥤ E<VAR>inst✝⁹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁸ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝⁷ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F✝<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝⁶ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝⁵ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝⁴ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F✝<VAR>F G : D ⥤ E<VAR>η : F ⟶ G<VAR>P : Cᵒᵖ ⥤ D<VAR>inst✝³ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>inst✝² : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>inst✝¹ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ G<VAR>inst✝ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan G<VAR>X : Cᵒᵖ<VAR>W : (J.Cover (unop X))ᵒᵖ<GOAL>F.map (colimit.ι (J.diagram P (unop X)) W) ≫ η.app (colimit (J.diagram P (unop X))) ≫ (J.plusCompIso G P).hom.app X = F.map (colimit.ι (J.diagram P (unop X)) W) ≫ (J.plusCompIso F P).hom.app X ≫ colimMap (J.diagramNatTrans (whiskerLeft P η) (unop X))
<VAR>C : Type u<VAR>inst✝¹² : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝¹¹ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝¹⁰ : Category.{max v u, w₂} E<VAR>F✝ : D ⥤ E<VAR>inst✝⁹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁸ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝⁷ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F✝<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝⁶ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝⁵ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝⁴ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F✝<VAR>F G : D ⥤ E<VAR>η : F ⟶ G<VAR>P : Cᵒᵖ ⥤ D<VAR>inst✝³ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>inst✝² : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>inst✝¹ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ G<VAR>inst✝ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan G<VAR>X : Cᵒᵖ<VAR>W : (J.Cover (unop X))ᵒᵖ<GOAL>η.app (multiequalizer ((unop W).index P)) ≫ (J.diagramCompIso G P (unop X)).hom.app W ≫ colimit.ι (J.diagram (P ⋙ G) (unop X)) W = (J.diagramCompIso F P (unop X)).hom.app W ≫ Multiequalizer.lift ((unop W).index (P ⋙ G)) ((J.diagram (P ⋙ F) (unop X)).obj W) (fun i => Multiequalizer.ι ((unop W).index (P ⋙ F)) i ≫ η.app (P.obj (op i.Y))) ⋯ ≫ colimit.ι (J.diagram (P ⋙ G) (unop X)) W
<VAR>C : Type u<VAR>inst✝¹² : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝¹¹ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝¹⁰ : Category.{max v u, w₂} E<VAR>F✝ : D ⥤ E<VAR>inst✝⁹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁸ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝⁷ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F✝<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝⁶ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝⁵ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝⁴ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F✝<VAR>F G : D ⥤ E<VAR>η : F ⟶ G<VAR>P : Cᵒᵖ ⥤ D<VAR>inst✝³ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>inst✝² : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>inst✝¹ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ G<VAR>inst✝ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan G<VAR>X : Cᵒᵖ<VAR>W : (J.Cover (unop X))ᵒᵖ<GOAL>(η.app (multiequalizer ((unop W).index P)) ≫ (J.diagramCompIso G P (unop X)).hom.app W) ≫ colimit.ι (J.diagram (P ⋙ G) (unop X)) W = ((J.diagramCompIso F P (unop X)).hom.app W ≫ Multiequalizer.lift ((unop W).index (P ⋙ G)) ((J.diagram (P ⋙ F) (unop X)).obj W) (fun i => Multiequalizer.ι ((unop W).index (P ⋙ F)) i ≫ η.app (P.obj (op i.Y))) ⋯) ≫ colimit.ι (J.diagram (P ⋙ G) (unop X)) W
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>ι : Type u_5<VAR>s : Finset ι<VAR>f : ι → K<GOAL>spanFinset R₁ s f = 0 ↔ ∀ j ∈ s, f j = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : IsLawson α<VAR>a : α<GOAL>IsClosed {a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : IsLawson α<VAR>a : α<GOAL>IsClosed (⇑WithLawson.ofLawson ⁻¹' (↑(upperClosure {a}) ∩ ↑(lowerClosure {a})))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : IsLawson α<VAR>a : α<GOAL>IsClosed ↑(lowerClosure {a})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : IsLawson α<VAR>a : α<GOAL>IsClosed (⇑WithLawson.ofLawson ⁻¹' Iic a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : IsLawson α<VAR>a : α<GOAL>IsClosed (⇑WithScott.ofScott ⁻¹' Iic a)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝ : Category.{v₂, u₂} A<VAR>J : GrothendieckTopology C<VAR>P : Cᵒᵖ ⥤ A<VAR>X : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>E : Aᵒᵖ<VAR>x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows<VAR>hx : x.SieveCompatible<GOAL>Nonempty (IsLimit (P.mapCone S.arrows.cocone.op)) ↔ ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), x.Compatible → ∃! t, x.IsAmalgamation t
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝ : Category.{v₂, u₂} A<VAR>J : GrothendieckTopology C<VAR>P : Cᵒᵖ ⥤ A<VAR>X : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>E : Aᵒᵖ<VAR>x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows<VAR>hx : x.SieveCompatible<GOAL>Nonempty (IsLimit (P.mapCone S.arrows.cocone.op)) ↔ ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), x.SieveCompatible → ∃! t, x.IsAmalgamation t
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝ : Category.{v₂, u₂} A<VAR>J : GrothendieckTopology C<VAR>P : Cᵒᵖ ⥤ A<VAR>X : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>E : Aᵒᵖ<VAR>x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows<VAR>hx : x.SieveCompatible<GOAL>Nonempty ((X_1 : Cone (S.arrows.diagram.op ⋙ P)) → Unique (X_1 ⟶ P.mapCone S.arrows.cocone.op)) ↔ ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), x.SieveCompatible → ∃! t, x.IsAmalgamation t
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝ : Category.{v₂, u₂} A<VAR>J : GrothendieckTopology C<VAR>P : Cᵒᵖ ⥤ A<VAR>X : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>E : Aᵒᵖ<VAR>x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows<VAR>hx : x.SieveCompatible<GOAL>(∀ (i : Cone (S.arrows.diagram.op ⋙ P)), Nonempty (Unique (i ⟶ P.mapCone S.arrows.cocone.op))) ↔ ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), x.SieveCompatible → ∃! t, x.IsAmalgamation t
<VAR>n k m : ℕ<GOAL>n + k - (m + k) + (m + k - (n + k)) = n - m + (m + k - (n + k))
<VAR>n k m : ℕ<GOAL>n - m + (m + k - (n + k)) = n - m + (m - n)
<VAR>R : Type u1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>A : Type u_1<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>g : ExteriorAlgebra R M →ₐ[R] A<VAR>m : M<GOAL>g ((ι R) m) * g ((ι R) m) = 0
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>inst✝⁵ : DecidableEq α<VAR>M : α → Type u_3<VAR>P : α → Type u_4<VAR>inst✝⁴ : (a : α) → Zero (N a)<VAR>inst✝³ : (a : α) → Zero (M a)<VAR>inst✝² : (a : α) → Zero (P a)<VAR>inst✝¹ : (a : α) → DecidableEq (N a)<VAR>inst✝ : (a : α) → DecidableEq (M a)<VAR>f g : Π₀ (a : α), N a<VAR>F : (a : α) → N a → M a<VAR>F0 : ∀ (a : α), F a 0 = 0<VAR>hF : ∀ (a : α), Function.Injective (F a)<VAR>a : α<GOAL>a ∈ (mapRange F F0 f).neLocus (mapRange F F0 g) ↔ a ∈ f.neLocus g
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : E<VAR>p q : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f g : 𝕜 → E<VAR>n : ℕ<VAR>z z₀ : 𝕜<VAR>hp : HasFPowerSeriesAt f p z₀<GOAL>∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ p.order • (swap dslope z₀)^[p.order] f z
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : E<VAR>p q : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f g : 𝕜 → E<VAR>n : ℕ<VAR>z z₀ : 𝕜<VAR>hp : HasFPowerSeriesAt f p z₀<VAR>hq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, HasSum (fun n => (z - z₀) ^ n • (fslope^[p.order] p).coeff n) ((swap dslope z₀)^[p.order] f z)<GOAL>∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ p.order • (swap dslope z₀)^[p.order] f z
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : E<VAR>p q : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f g : 𝕜 → E<VAR>n : ℕ<VAR>z z₀ : 𝕜<VAR>hp : HasFPowerSeriesAt f p z₀<VAR>hq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, HasSum (fun n => (z - z₀) ^ n • (fslope^[p.order] p).coeff n) ((swap dslope z₀)^[p.order] f z)<VAR>x : 𝕜<VAR>hx1 : HasSum (fun n => (x - z₀) ^ n • (fslope^[p.order] p).coeff n) ((swap dslope z₀)^[p.order] f x)<VAR>hx2 : HasSum (fun n => (x - z₀) ^ n • p.coeff n) (f x)<GOAL>f x = (x - z₀) ^ p.order • (swap dslope z₀)^[p.order] f x
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : E<VAR>p q : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f g : 𝕜 → E<VAR>n : ℕ<VAR>z z₀ : 𝕜<VAR>hp : HasFPowerSeriesAt f p z₀<VAR>hq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, HasSum (fun n => (z - z₀) ^ n • (fslope^[p.order] p).coeff n) ((swap dslope z₀)^[p.order] f z)<VAR>x : 𝕜<VAR>hx1 : HasSum (fun n => (x - z₀) ^ n • (fslope^[p.order] p).coeff n) ((swap dslope z₀)^[p.order] f x)<VAR>hx2 : HasSum (fun n => (x - z₀) ^ n • p.coeff n) (f x)<VAR>this : ∀ k < p.order, p.coeff k = 0<GOAL>f x = (x - z₀) ^ p.order • (swap dslope z₀)^[p.order] f x
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s✝ : E<VAR>p q : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f g : 𝕜 → E<VAR>n : ℕ<VAR>z z₀ : 𝕜<VAR>hp : HasFPowerSeriesAt f p z₀<VAR>hq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, HasSum (fun n => (z - z₀) ^ n • (fslope^[p.order] p).coeff n) ((swap dslope z₀)^[p.order] f z)<VAR>x : 𝕜<VAR>hx1 : HasSum (fun n => (x - z₀) ^ n • (fslope^[p.order] p).coeff n) ((swap dslope z₀)^[p.order] f x)<VAR>hx2 : HasSum (fun n => (x - z₀) ^ n • p.coeff n) (f x)<VAR>this : ∀ k < p.order, p.coeff k = 0<VAR>s : E<VAR>hs1 : (x - z₀) ^ p.order • s = f x<VAR>hs2 : HasSum (fun m => (x - z₀) ^ m • p.coeff (m + p.order)) s<GOAL>f x = (x - z₀) ^ p.order • (swap dslope z₀)^[p.order] f x
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s✝ : E<VAR>p q : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f g : 𝕜 → E<VAR>n : ℕ<VAR>z z₀ : 𝕜<VAR>hp : HasFPowerSeriesAt f p z₀<VAR>hq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, HasSum (fun n => (z - z₀) ^ n • (fslope^[p.order] p).coeff n) ((swap dslope z₀)^[p.order] f z)<VAR>x : 𝕜<VAR>hx1 : HasSum (fun n => (x - z₀) ^ n • (fslope^[p.order] p).coeff n) ((swap dslope z₀)^[p.order] f x)<VAR>hx2 : HasSum (fun n => (x - z₀) ^ n • p.coeff n) (f x)<VAR>this : ∀ k < p.order, p.coeff k = 0<VAR>s : E<VAR>hs1 : (x - z₀) ^ p.order • s = f x<VAR>hs2 : HasSum (fun m => (x - z₀) ^ m • p.coeff (m + p.order)) s<GOAL>(swap dslope z₀)^[p.order] f x = s