ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝ : EuclideanDomain R<VAR>x z : R<VAR>hz : ¬z = 0<VAR>p : R<GOAL>x * (z * p) / z = x * (z * p / z)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a✝ a b c : α<VAR>h : 0 < c<GOAL>(fun x => x * c) ⁻¹' Icc a b = Icc (a / c) (b / c)
<VAR>α : Type u_1<VAR>s t : Set α<VAR>x✝ : α × α<VAR>a : α<VAR>x : α × α<GOAL>x ∈ (s ∩ t).offDiag ↔ x ∈ s.offDiag ∩ t.offDiag
<VAR>α : Type u_1<VAR>s t : Set α<VAR>x✝ : α × α<VAR>a : α<VAR>x : α × α<GOAL>(x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 ↔ (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : α → β<VAR>s✝ t✝ : Set α<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<GOAL>f '' (s \ f ⁻¹' t) = f '' s \ t
<VAR>C : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝⁵ : Category.{v₃, u₃} E<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasZeroMorphisms D<VAR>inst✝² : HasZeroMorphisms E<VAR>F : C ⥤ D<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>inst✝ : F.Faithful<VAR>X Y : C<GOAL>F.map 0 = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<GOAL>S.L₀.g ≫ S.δ = 0
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : PartialOrder α<VAR>a b c d : α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : MulPosStrictMono α<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>hb : b < 0<VAR>h : 1 < a<GOAL>a * b < b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>H : ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m<VAR>a : α<GOAL>Bounded r (s ∩ {b | ¬r b a}) ↔ Bounded r s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>H : ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m<VAR>a : α<GOAL>Bounded r (s ∩ {b | ¬r b a}) → Bounded r s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>H : ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m<VAR>a b : α<VAR>hb : ∀ b_1 ∈ s ∩ {b | ¬r b a}, r b_1 b<VAR>m : α<VAR>hm : ∀ (c : α), r c a ∨ r c b → r c m<GOAL>Bounded r s
<VAR>J : Type u'<VAR>inst✝⁴ : Category.{v', u'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasColimitsOfShape J TopCat<VAR>inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)<VAR>inst✝ : HasLimitsOfShape Jᵒᵖ C<VAR>F : J ⥤ PresheafedSpace C<VAR>U : Opens ↑↑(Limits.colimit F)<VAR>j : J<GOAL>((sheafIsoOfIso (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm).app (op U) ≪≫ limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U)) ≪≫ Limits.lim.mapIso (NatIso.ofComponents (fun X => mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯)).inv ≫ (colimit.ι F j).c.app (op U) = limit.π (componentwiseDiagram F U) (op j)
<VAR>J : Type u'<VAR>inst✝⁴ : Category.{v', u'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasColimitsOfShape J TopCat<VAR>inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)<VAR>inst✝ : HasLimitsOfShape Jᵒᵖ C<VAR>F : J ⥤ PresheafedSpace C<VAR>U : Opens ↑↑(Limits.colimit F)<VAR>j : J<GOAL>(((Limits.lim.mapIso (NatIso.ofComponents (fun X => mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯)).inv ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U))).inv) ≫ ((colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom.c.app (op ((Opens.map ((forget C).mapIso (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm).symm.inv).obj (unop (op U)))) ≫ (Limits.colimit F).presheaf.map (eqToHom ⋯)) ≫ (Limits.colimit F).presheaf.map (eqToHom ⋯)) ≫ (colimit.ι F j).c.app (op U) = limit.π (componentwiseDiagram F U) (op j)
<VAR>J : Type u'<VAR>inst✝⁴ : Category.{v', u'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasColimitsOfShape J TopCat<VAR>inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)<VAR>inst✝ : HasLimitsOfShape Jᵒᵖ C<VAR>F : J ⥤ PresheafedSpace C<VAR>U : Opens ↑↑(Limits.colimit F)<VAR>j : J<GOAL>((limMap (NatIso.ofComponents (fun X => mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).inv) ≫ ((colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom.c.app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) ≫ (Limits.colimit F).presheaf.map (𝟙 (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom.base).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))))) ≫ (Limits.colimit F).presheaf.map (eqToHom ⋯)) ≫ (colimit.ι F j).c.app (op U) = limit.π (componentwiseDiagram F U) (op j)
<VAR>J : Type u'<VAR>inst✝⁴ : Category.{v', u'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasColimitsOfShape J TopCat<VAR>inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)<VAR>inst✝ : HasLimitsOfShape Jᵒᵖ C<VAR>F : J ⥤ PresheafedSpace C<VAR>U : Opens ↑↑(Limits.colimit F)<VAR>j : J<GOAL>limMap (NatIso.ofComponents (fun X => mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).inv ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom.c.app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) ≫ (colimit.ι F j).c.app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom.base).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) ≫ ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯) = limit.π (componentwiseDiagram F U) (op j)
<VAR>J : Type u'<VAR>inst✝⁴ : Category.{v', u'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasColimitsOfShape J TopCat<VAR>inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)<VAR>inst✝ : HasLimitsOfShape Jᵒᵖ C<VAR>F : J ⥤ PresheafedSpace C<VAR>U : Opens ↑↑(Limits.colimit F)<VAR>j : J<GOAL>limMap (NatIso.ofComponents (fun X => mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).inv ≫ (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).c.app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) ≫ ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯) = limit.π (componentwiseDiagram F U) (op j)
<VAR>J : Type u'<VAR>inst✝⁴ : Category.{v', u'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasColimitsOfShape J TopCat<VAR>inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)<VAR>inst✝ : HasLimitsOfShape Jᵒᵖ C<VAR>F : J ⥤ PresheafedSpace C<VAR>U : Opens ↑↑(Limits.colimit F)<VAR>j : J<GOAL>limMap (NatIso.ofComponents (fun X => mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).inv ≫ ({ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.ι.app j).c.app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) ≫ (F.obj j).presheaf.map (eqToHom ⋯) ≫ ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯) = limit.π (componentwiseDiagram F U) (op j)
<VAR>J : Type u'<VAR>inst✝⁴ : Category.{v', u'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasColimitsOfShape J TopCat<VAR>inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)<VAR>inst✝ : HasLimitsOfShape Jᵒᵖ C<VAR>F : J ⥤ PresheafedSpace C<VAR>U : Opens ↑↑(Limits.colimit F)<VAR>j : J<VAR>f : (componentwiseDiagram F U).obj (op j) ⟶ (F.obj j).presheaf.obj (op ((Opens.map (colimit.ι F j).base).obj U)) := (NatIso.ofComponents (fun X => mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv.app (op j) ≫ (F.obj j).presheaf.map (eqToHom ⋯) ≫ ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯)<GOAL>limit.π (componentwiseDiagram F U) (op j) ≫ f = limit.π (componentwiseDiagram F U) (op j)
<VAR>J : Type u'<VAR>inst✝⁴ : Category.{v', u'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasColimitsOfShape J TopCat<VAR>inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)<VAR>inst✝ : HasLimitsOfShape Jᵒᵖ C<VAR>F : J ⥤ PresheafedSpace C<VAR>U : Opens ↑↑(Limits.colimit F)<VAR>j : J<VAR>f : (componentwiseDiagram F U).obj (op j) ⟶ (F.obj j).presheaf.obj (op ((Opens.map (colimit.ι F j).base).obj U)) := (NatIso.ofComponents (fun X => mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv.app (op j) ≫ (F.obj j).presheaf.map (eqToHom ⋯) ≫ ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯)<GOAL>f = 𝟙 ((componentwiseDiagram F U).obj (op j))
<VAR>J : Type u'<VAR>inst✝⁴ : Category.{v', u'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasColimitsOfShape J TopCat<VAR>inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)<VAR>inst✝ : HasLimitsOfShape Jᵒᵖ C<VAR>F : J ⥤ PresheafedSpace C<VAR>U : Opens ↑↑(Limits.colimit F)<VAR>j : J<VAR>f : (componentwiseDiagram F U).obj (op j) ⟶ (F.obj j).presheaf.obj (op ((Opens.map (colimit.ι F j).base).obj U)) := (NatIso.ofComponents (fun X => mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv.app (op j) ≫ (F.obj j).presheaf.map (eqToHom ⋯) ≫ ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯)<GOAL>f = (F.obj j).presheaf.map (𝟙 (op ((Opens.map (colimit.ι F (unop (op j))).base).obj U)))
<VAR>J : Type u'<VAR>inst✝⁴ : Category.{v', u'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasColimitsOfShape J TopCat<VAR>inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)<VAR>inst✝ : HasLimitsOfShape Jᵒᵖ C<VAR>F : J ⥤ PresheafedSpace C<VAR>U : Opens ↑↑(Limits.colimit F)<VAR>j : J<VAR>f : (componentwiseDiagram F U).obj (op j) ⟶ (F.obj j).presheaf.obj (op ((Opens.map (colimit.ι F j).base).obj U)) := (NatIso.ofComponents (fun X => mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv.app (op j) ≫ (F.obj j).presheaf.map (eqToHom ⋯) ≫ ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯)<GOAL>(F.obj j).presheaf.map (eqToIso ⋯).inv ≫ (F.obj j).presheaf.map (eqToHom ⋯) ≫ ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯) = (F.obj j).presheaf.map (𝟙 (op ((Opens.map (colimit.ι F (unop (op j))).base).obj U)))
<VAR>J : Type u'<VAR>inst✝⁴ : Category.{v', u'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasColimitsOfShape J TopCat<VAR>inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)<VAR>inst✝ : HasLimitsOfShape Jᵒᵖ C<VAR>F : J ⥤ PresheafedSpace C<VAR>U : Opens ↑↑(Limits.colimit F)<VAR>j : J<VAR>f : (componentwiseDiagram F U).obj (op j) ⟶ (F.obj j).presheaf.obj (op ((Opens.map (colimit.ι F j).base).obj U)) := (NatIso.ofComponents (fun X => mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv.app (op j) ≫ (F.obj j).presheaf.map (eqToHom ⋯) ≫ ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯)<GOAL>(F.obj j).presheaf.map ((eqToIso ⋯).inv ≫ eqToHom ⋯ ≫ (Opens.map (colimit.ι F j).base).op.map (eqToHom ⋯)) = (F.obj j).presheaf.map (𝟙 (op ((Opens.map (colimit.ι F (unop (op j))).base).obj U)))
<VAR>n : ℕ<GOAL>(2 * n + 2).choose (n + 1) * (n + 1) = (2 * n + 1).choose n * (2 * n + 2)
<VAR>n : ℕ<GOAL>2 * ((2 * n + 1).choose n * (n + 1)) = 2 * ((2 * n + 1).choose n * (2 * n + 1 - n))
<VAR>n : ℕ<GOAL>2 * ((2 * n + 1).choose n * (2 * n + 1 - n)) = 2 * ((2 * n).choose n * (2 * n + 1))
<VAR>n : ℕ<GOAL>2 * ((2 * n).choose n * (2 * n + 1)) = 2 * (2 * n + 1) * (2 * n).choose n
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<VAR>x y : L<GOAL>__src✝.toFun ⁅x, y⁆ = ⁅__src✝.toFun x, __src✝.toFun y⁆
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<VAR>x y : L<GOAL>(mkAlgHom R L) (ιₜ ⁅x, y⁆ + ιₜ y * ιₜ x) = (mkAlgHom R L) (ιₜ x * ιₜ y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t u v : Finset α<VAR>a b : α<VAR>ha : a ∈ s<GOAL>s \ s.erase a = {a}
<VAR>σ : Type u_1<VAR>inst✝² : Fintype σ<VAR>inst✝¹ : DecidableEq σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>f : Finset σ × σ → MvPolynomial σ R<GOAL>∑ t ∈ filter (fun t => t.1.card < k) (MvPolynomial.NewtonIdentities.pairs σ k), f t = ∑ a ∈ filter (fun a => a.1 < k) (antidiagonal k), ∑ A ∈ powersetCard a.1 univ, ∑ j : σ, f (A, j)
<VAR>σ : Type u_1<VAR>inst✝² : Fintype σ<VAR>inst✝¹ : DecidableEq σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>f : Finset σ × σ → MvPolynomial σ R<GOAL>∑ i ∈ range k, ∑ x ∈ powersetCard i univ, ∑ y : σ, f (x, y) = ∑ a ∈ filter (fun a => a.1 < k) (antidiagonal k), ∑ A ∈ powersetCard a.1 univ, ∑ j : σ, f (A, j)
<VAR>s : Set ℕ<VAR>m : ℕ<VAR>hm : m ∈ s<GOAL>sInf s ≤ m
<VAR>s : Set ℕ<VAR>m : ℕ<VAR>hm : m ∈ s<GOAL>Nat.find ⋯ ≤ m
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>I J : Ideal R<GOAL>zeroLocus ↑I ⊆ zeroLocus ↑J ↔ J ≤ I.radical
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>x : 𝕜<GOAL>MeromorphicAt f x ↔ ∃ n g, AnalyticAt 𝕜 g x ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>x : 𝕜<VAR>x✝ : MeromorphicAt f x<VAR>n : ℕ<VAR>hn : AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) x<GOAL>∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → f x_1 = (x_1 - x) ^ (-↑n) • (x_1 - x) ^ n • f x_1
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>x : 𝕜<GOAL>(∃ n g, AnalyticAt 𝕜 g x ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z) → MeromorphicAt f x
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝¹ : IsIso fst<VAR>inst✝ : IsIso g<VAR>sq : CommSq fst snd f g<VAR>s : PullbackCone f g<GOAL>(fun s => s.fst ≫ inv fst) s ≫ snd = s.snd
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>t : Cocone F<VAR>X : C<VAR>h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones<VAR>s : Cocone F<GOAL>(colimitCocone h).extend (homOfCocone h s) = s
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>t : Cocone F<VAR>X : C<VAR>h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones<VAR>s : Cocone F<GOAL>(colimitCocone h).extend (homOfCocone h (coconeOfHom h (homOfCocone h s))) = coconeOfHom h (homOfCocone h s)
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>t : Cocone F<VAR>X : C<VAR>h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones<VAR>s : Cocone F<GOAL>(colimitCocone h).extend (homOfCocone h s) = coconeOfHom h (homOfCocone h s)
<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>S : Type v<VAR>inst✝¹ : CommSemiring S<VAR>p q : ℕ<VAR>inst✝ : ExpChar R p<VAR>f : R[X]<GOAL>map (frobenius R p) ((expand R p) f) = f ^ p
<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>S : Type v<VAR>inst✝¹ : CommSemiring S<VAR>p q : ℕ<VAR>inst✝ : ExpChar R p<VAR>f a b : R[X]<VAR>ha : map (frobenius R p) ((expand R p) a) = a ^ p<VAR>hb : map (frobenius R p) ((expand R p) b) = b ^ p<GOAL>map (frobenius R p) ((expand R p) (a + b)) = (a + b) ^ p
<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>S : Type v<VAR>inst✝¹ : CommSemiring S<VAR>p q : ℕ<VAR>inst✝ : ExpChar R p<VAR>f : R[X]<VAR>n : ℕ<VAR>a : R<GOAL>map (frobenius R p) ((expand R p) ((monomial n) a)) = (monomial n) a ^ p
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ ε : ℝ<VAR>s t : Set α<VAR>x : α<VAR>hst : Disjoint s t<VAR>hs : IsCompact s<VAR>ht : IsClosed t<GOAL>∃ δ, 0 < δ ∧ Disjoint (cthickening δ s) (cthickening δ t)
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s t : Set α<VAR>x : α<VAR>hst : Disjoint s t<VAR>hs : IsCompact s<VAR>ht : IsClosed t<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>h : Disjoint (thickening δ s) (thickening δ t)<GOAL>∃ δ, 0 < δ ∧ Disjoint (cthickening δ s) (cthickening δ t)
<VAR>ψ θ : Angle<GOAL>2 • ψ = 2 • θ ↔ ψ = θ ∨ ψ = θ + ↑π
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z : ℂ<VAR>M r δ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>hr : 0 < r<VAR>hfM : ∀ w ∈ sphere z r, ‖f w‖ < M<VAR>hf : ContinuousOn f (sphere z r)<GOAL>‖cderiv r f z‖ < M / r
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z : ℂ<VAR>M r δ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>hr : 0 < r<VAR>hfM : ∀ w ∈ sphere z r, ‖f w‖ < M<VAR>hf : ContinuousOn f (sphere z r)<VAR>L : ℝ<VAR>hL1 : L < M<VAR>hL2 : ∀ w ∈ sphere z r, ‖f w‖ ≤ L<GOAL>‖cderiv r f z‖ < M / r
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p✝¹ pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x✝² : E<VAR>r✝ r' : ℝ≥0∞<VAR>n✝ m : ℕ<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>x✝¹ y : E<VAR>r R : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<VAR>k : ℕ<VAR>x : E<VAR>x✝ : Fin k → E<GOAL>((p.changeOriginSeries k).sum x) x✝ = ((p.changeOriginSeries k).partialSum (n - k) x) x✝
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p✝¹ pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x✝² : E<VAR>r✝ r' : ℝ≥0∞<VAR>n✝ m : ℕ<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>x✝¹ y : E<VAR>r R : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<VAR>k : ℕ<VAR>x : E<VAR>x✝ : Fin k → E<GOAL>∀ b ∉ Finset.range (n - k), ((p.changeOriginSeries k b) fun x_1 => x) = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p✝¹ pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x✝² : E<VAR>r✝ r' : ℝ≥0∞<VAR>n✝ m✝ : ℕ<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>x✝¹ y : E<VAR>r R : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<VAR>k : ℕ<VAR>x : E<VAR>x✝ : Fin k → E<VAR>m : ℕ<VAR>hm : m ∉ Finset.range (n - k)<GOAL>((p.changeOriginSeries k m) fun x_1 => x) = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p✝¹ pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x✝² : E<VAR>r✝ r' : ℝ≥0∞<VAR>n✝ m✝ : ℕ<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>x✝¹ y : E<VAR>r R : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<VAR>k : ℕ<VAR>x : E<VAR>x✝ : Fin k → E<VAR>m : ℕ<VAR>hm : n - k ≤ m<GOAL>((p.changeOriginSeries k m) fun x_1 => x) = 0
<VAR>l m✝ n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m n : ℕ<VAR>P : Matrix (Fin (m + 1)) (Fin n) α → Prop<GOAL>Forall P ↔ ∀ (x : Matrix (Fin (m + 1)) (Fin n) α), P x
<VAR>l m✝ n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m n : ℕ<VAR>P : Matrix (Fin (m + 1)) (Fin n) α → Prop<GOAL>(∀ (x : Fin n → α) (x_1 : Matrix (Fin m) (Fin n) α), P (of (vecCons x x_1))) ↔ ∀ (x : Matrix (Fin (m + 1)) (Fin n) α), P x
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>R : P.M α → P.M α → Prop<VAR>h₀ : Equivalence R<VAR>h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y<VAR>x y : P.M α<VAR>r : R x y<GOAL>x = y
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>R : P.M α → P.M α → Prop<VAR>h₀ : Equivalence R<VAR>h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y<VAR>x y : P.M α<VAR>r : R x y<GOAL>∀ (x y : P.M α), R x y → ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>R : P.M α → P.M α → Prop<VAR>h₀ : Equivalence R<VAR>x y : P.M α<VAR>ax : P.A<VAR>fx : P.B ax ⟹ α ::: P.M α<VAR>ay : P.A<VAR>fy : P.B ay ⟹ α ::: P.M α<VAR>h : (TypeVec.id ::: Quot.mk R) <$$> ⟨ax, fx⟩ = (TypeVec.id ::: Quot.mk R) <$$> ⟨ay, fy⟩<GOAL>∃ a f f₁ f₂, ⟨ax, fx⟩ = ⟨a, splitFun f f₁⟩ ∧ ⟨ay, fy⟩ = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>R : P.M α → P.M α → Prop<VAR>h₀ : Equivalence R<VAR>x y : P.M α<VAR>ax : P.A<VAR>fx : P.B ax ⟹ α ::: P.M α<VAR>ay : P.A<VAR>fy : P.B ay ⟹ α ::: P.M α<VAR>h : ⟨ax, (TypeVec.id ::: Quot.mk R) ⊚ fx⟩ = ⟨ay, (TypeVec.id ::: Quot.mk R) ⊚ fy⟩<GOAL>∃ a f f₁ f₂, ⟨ax, fx⟩ = ⟨a, splitFun f f₁⟩ ∧ ⟨ay, fy⟩ = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>R : P.M α → P.M α → Prop<VAR>h₀ : Equivalence R<VAR>x y : P.M α<VAR>ax : P.A<VAR>fx fy : P.B ax ⟹ α ::: P.M α<VAR>h₁ : HEq ((TypeVec.id ::: Quot.mk R) ⊚ fx) ((TypeVec.id ::: Quot.mk R) ⊚ fy)<GOAL>∃ a f f₁ f₂, ⟨ax, fx⟩ = ⟨a, splitFun f f₁⟩ ∧ ⟨ax, fy⟩ = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>R : P.M α → P.M α → Prop<VAR>h₀ : Equivalence R<VAR>x y : P.M α<VAR>ax : P.A<VAR>fx fy : P.B ax ⟹ α ::: P.M α<VAR>h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy<GOAL>∃ a f f₁ f₂, ⟨ax, fx⟩ = ⟨a, splitFun f f₁⟩ ∧ ⟨ax, fy⟩ = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)