ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>J : Type v'<VAR>inst✝⁹ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝⁷ : Category.{?u.207926, u_1} K<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_2} D<VAR>inst✝⁵ : HasColimitsOfShape J C<VAR>Gl : C ⥤ D<VAR>Gr : D ⥤ C<VAR>adj : Gl ⊣ Gr<VAR>inst✝⁴ : Gr.Full<VAR>inst✝³ : Gr.Faithful<VAR>F : J ⥤ D<VAR>c : Cocone (F ⋙ Gr)<VAR>H : IsVanKampenColimit c<VAR>inst✝² : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)<VAR>inst✝¹ : (X : D) → (f : X ⟶ Gl.obj c.pt) → PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl<VAR>inst✝ : (X : C) → (i : J) → (f : X ⟶ c.pt) → PreservesLimit (cospan f (c.ι.app i)) Gl<VAR>this✝³ : PreservesLimitsOfSize.{0, 0, u_3, v, u_2, u} Gr<VAR>this✝² : PreservesColimitsOfSize.{u', v', v, u_3, u, u_2} Gl<VAR>F' : J ⥤ D<VAR>c' : Cocone F'<VAR>α : F' ⟶ (F ⋙ Gr) ⋙ Gl<VAR>f : c'.pt ⟶ (Gl.mapCocone c).pt<VAR>h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>hc' : IsColimit c'<VAR>j : J<VAR>α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ whiskerLeft F adj.counit ≫ F.rightUnitor.hom<VAR>hα' : NatTrans.Equifibered α'<VAR>hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.toPrefunctor.1 j) ≫ α.app j<VAR>β : F' ⋙ Gr ⋙ Gl ≅ F' := isoWhiskerLeft F' (asIso adj.counit) ≪≫ F'.rightUnitor<VAR>hl : IsColimit ((Cocones.precompose β.hom).obj c') := (IsColimit.precomposeHomEquiv β c').symm hc'<VAR>hr : IsColimit (Gl.mapCocone (colimit.cocone (F' ⋙ Gr))) := isColimitOfPreserves Gl (colimit.isColimit (F' ⋙ Gr))<VAR>this✝¹ : α.app j = β.inv.app j ≫ Gl.map (Gr.map (α'.app j))<VAR>this✝ : f = (hl.coconePointUniqueUpToIso hr).hom ≫ Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })<VAR>this : IsPullback (Gl.map ((colimit.cocone (F' ⋙ Gr)).ι.app j)) (Gl.map ((whiskerRight α' Gr).app j)) (Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })) (Gl.map (c.ι.app j))<GOAL>IsPullback (c'.ι.app j) (β.inv.app j ≫ Gl.map (Gr.map (α'.app j))) ((hl.coconePointUniqueUpToIso hr).hom ≫ Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })) ((Gl.mapCocone c).ι.app j)
<VAR>J : Type v'<VAR>inst✝⁹ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝⁷ : Category.{?u.207926, u_1} K<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_2} D<VAR>inst✝⁵ : HasColimitsOfShape J C<VAR>Gl : C ⥤ D<VAR>Gr : D ⥤ C<VAR>adj : Gl ⊣ Gr<VAR>inst✝⁴ : Gr.Full<VAR>inst✝³ : Gr.Faithful<VAR>F : J ⥤ D<VAR>c : Cocone (F ⋙ Gr)<VAR>H : IsVanKampenColimit c<VAR>inst✝² : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)<VAR>inst✝¹ : (X : D) → (f : X ⟶ Gl.obj c.pt) → PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl<VAR>inst✝ : (X : C) → (i : J) → (f : X ⟶ c.pt) → PreservesLimit (cospan f (c.ι.app i)) Gl<VAR>this✝² : PreservesLimitsOfSize.{0, 0, u_3, v, u_2, u} Gr<VAR>this✝¹ : PreservesColimitsOfSize.{u', v', v, u_3, u, u_2} Gl<VAR>F' : J ⥤ D<VAR>c' : Cocone F'<VAR>α : F' ⟶ (F ⋙ Gr) ⋙ Gl<VAR>f : c'.pt ⟶ (Gl.mapCocone c).pt<VAR>h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>hc' : IsColimit c'<VAR>j : J<VAR>α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ whiskerLeft F adj.counit ≫ F.rightUnitor.hom<VAR>hα' : NatTrans.Equifibered α'<VAR>hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.toPrefunctor.1 j) ≫ α.app j<VAR>β : F' ⋙ Gr ⋙ Gl ≅ F' := isoWhiskerLeft F' (asIso adj.counit) ≪≫ F'.rightUnitor<VAR>hl : IsColimit ((Cocones.precompose β.hom).obj c') := (IsColimit.precomposeHomEquiv β c').symm hc'<VAR>hr : IsColimit (Gl.mapCocone (colimit.cocone (F' ⋙ Gr))) := isColimitOfPreserves Gl (colimit.isColimit (F' ⋙ Gr))<VAR>this✝ : α.app j = β.inv.app j ≫ Gl.map (Gr.map (α'.app j))<VAR>this : f = (hl.coconePointUniqueUpToIso hr).hom ≫ Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })<GOAL>whiskerRight α' Gr ≫ c.ι = (colimit.cocone (F' ⋙ Gr)).ι ≫ (Functor.const J).map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>γ : Type x<VAR>ι : Type u_1<VAR>s : Set ι<VAR>hs : s.Finite<VAR>t : (i : ι) → i ∈ s → Set α<VAR>ht : ∀ (i : ι) (hi : i ∈ s), (t i hi).Finite<GOAL>(⋃ i, ⋃ (h : i ∈ s), t i h).Finite
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>γ : Type x<VAR>ι : Type u_1<VAR>s : Set ι<VAR>hs : s.Finite<VAR>t : (i : ι) → i ∈ s → Set α<VAR>ht : ∀ (i : ι) (hi : i ∈ s), (t i hi).Finite<VAR>this : Finite ↑s<GOAL>(⋃ i, ⋃ (h : i ∈ s), t i h).Finite
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>γ : Type x<VAR>ι : Type u_1<VAR>s : Set ι<VAR>hs : s.Finite<VAR>t : (i : ι) → i ∈ s → Set α<VAR>ht : ∀ (i : ι) (hi : i ∈ s), (t i hi).Finite<VAR>this : Finite ↑s<GOAL>(⋃ x, t ↑x ⋯).Finite
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w : V<VAR>inst✝ : DecidableEq V<VAR>u v : V<VAR>c : G.Walk v v<VAR>hc : c.IsCycle<VAR>h : u ∈ c.support<GOAL>(c.rotate h).IsCycle
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w : V<VAR>inst✝ : DecidableEq V<VAR>u v : V<VAR>c : G.Walk v v<VAR>hc : c.IsCycle<VAR>h : u ∈ c.support<GOAL>(c.rotate h).support.tail.Nodup
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w : V<VAR>inst✝ : DecidableEq V<VAR>u v : V<VAR>c : G.Walk v v<VAR>hc : c.IsCycle<VAR>h : u ∈ c.support<GOAL>c.support.tail.Nodup
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : ContinuousMul M<VAR>f : ι → X → M<VAR>s : Multiset ι<VAR>l : List ι<GOAL>(∀ i ∈ Quot.mk Setoid.r l, Continuous (f i)) → Continuous fun a => (Multiset.map (fun i => f i a) (Quot.mk Setoid.r l)).prod
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁴ : CountablyGenerated γ<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>κ : Kernel α (γ × ℝ)<VAR>inst✝ : IsFiniteKernel κ<GOAL>κ.fst ⊗ₖ κ.condKernelReal = κ
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.57464, u_1} C<VAR>X : SimplicialObject C<VAR>s : Splitting X<VAR>inst✝ : Preadditive C<VAR>i j : ℕ<VAR>hij : ¬(ComplexShape.down ℕ).Rel i j<GOAL>s.d i j = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.57464, u_1} C<VAR>X : SimplicialObject C<VAR>s : Splitting X<VAR>inst✝ : Preadditive C<VAR>i j k : ℕ<VAR>x✝¹ : (ComplexShape.down ℕ).Rel i j<VAR>x✝ : (ComplexShape.down ℕ).Rel j k<GOAL>s.d i j ≫ s.d j k = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.57464, u_1} C<VAR>X : SimplicialObject C<VAR>s : Splitting X<VAR>inst✝ : Preadditive C<VAR>i j k : ℕ<VAR>x✝¹ : (ComplexShape.down ℕ).Rel i j<VAR>x✝ : (ComplexShape.down ℕ).Rel j k<GOAL>(s.cofan (op [i])).inj (IndexSet.id (op [i])) ≫ K[X].d i j ≫ s.πSummand (IndexSet.id (op [j])) ≫ (s.cofan (op [j])).inj (IndexSet.id (op [j])) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op [k])) = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.57464, u_1} C<VAR>X : SimplicialObject C<VAR>s : Splitting X<VAR>inst✝ : Preadditive C<VAR>i j k : ℕ<VAR>x✝¹ : (ComplexShape.down ℕ).Rel i j<VAR>x✝ : (ComplexShape.down ℕ).Rel j k<VAR>eq : K[X].d i j ≫ 𝟙 (X _[j]) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op [k])) = 0<GOAL>(s.cofan (op [i])).inj (IndexSet.id (op [i])) ≫ K[X].d i j ≫ s.πSummand (IndexSet.id (op [j])) ≫ (s.cofan (op [j])).inj (IndexSet.id (op [j])) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op [k])) = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.57464, u_1} C<VAR>X : SimplicialObject C<VAR>s : Splitting X<VAR>inst✝ : Preadditive C<VAR>i j k : ℕ<VAR>x✝¹ : (ComplexShape.down ℕ).Rel i j<VAR>x✝ : (ComplexShape.down ℕ).Rel j k<VAR>eq : K[X].d i j ≫ (∑ A : IndexSet (op [j]), s.πSummand A ≫ (s.cofan (op [j])).inj A) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op [k])) = 0<GOAL>(s.cofan (op [i])).inj (IndexSet.id (op [i])) ≫ K[X].d i j ≫ s.πSummand (IndexSet.id (op [j])) ≫ (s.cofan (op [j])).inj (IndexSet.id (op [j])) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op [k])) = 0
<VAR>M G✝ : Type v<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Group G✝<VAR>G : Type v<VAR>inst✝ : Group G<VAR>J : SingleObj G ⥤ Type u<VAR>x y : J.obj (SingleObj.star G)<GOAL>Types.Quot.Rel J ⟨SingleObj.star G, x⟩ ⟨SingleObj.star G, y⟩ ↔ (MulAction.orbitRel G (J.obj (SingleObj.star G))).Rel x y
<VAR>M G✝ : Type v<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Group G✝<VAR>G : Type v<VAR>inst✝ : Group G<VAR>J : SingleObj G ⥤ Type u<VAR>x y : J.obj (SingleObj.star G)<VAR>h : ∀ (g : G), y = g • x ↔ g • x = y<GOAL>Types.Quot.Rel J ⟨SingleObj.star G, x⟩ ⟨SingleObj.star G, y⟩ ↔ (MulAction.orbitRel G (J.obj (SingleObj.star G))).Rel x y
<VAR>M G✝ : Type v<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Group G✝<VAR>G : Type v<VAR>inst✝ : Group G<VAR>J : SingleObj G ⥤ Type u<VAR>x y : J.obj (SingleObj.star G)<VAR>h : ∀ (g : G), y = g • x ↔ g • x = y<GOAL>Types.Quot.Rel J ⟨SingleObj.star G, x⟩ ⟨SingleObj.star G, y⟩ ↔ (MulAction.orbitRel G (J.obj (SingleObj.star G))).Rel y x
<VAR>M G✝ : Type v<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Group G✝<VAR>G : Type v<VAR>inst✝ : Group G<VAR>J : SingleObj G ⥤ Type u<VAR>x y : J.obj (SingleObj.star G)<VAR>h : ∀ (g : G), y = g • x ↔ g • x = y<GOAL>(∃ g, y = g • x) ↔ ∃ g, g • x = y
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Category.{v₂, u₂} D<VAR>L₁ L₂ : C ⥤ D<VAR>R₁ R₂ : D ⥤ C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<GOAL>(conjugateEquiv adj₁ adj₁).symm (𝟙 R₁) = 𝟙 L₁
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Category.{v₂, u₂} D<VAR>L₁ L₂ : C ⥤ D<VAR>R₁ R₂ : D ⥤ C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<GOAL>𝟙 R₁ = (conjugateEquiv adj₁ adj₁) (𝟙 L₁)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I J : Ideal R<VAR>N N' : Submodule R M<VAR>hN' : N'.FG<VAR>hIJ : I ≤ J.jacobson<VAR>hNN : N' ≤ N ⊔ I • N'<GOAL>N ⊔ N' = N ⊔ J • N'
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I J : Ideal R<VAR>N N' : Submodule R M<VAR>hN' : N'.FG<VAR>hIJ : I ≤ J.jacobson<VAR>hNN : N' ≤ N ⊔ I • N'<VAR>hNN' : N ⊔ N' = N ⊔ I • N'<GOAL>N ⊔ N' = N ⊔ J • N'
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I J : Ideal R<VAR>N N' : Submodule R M<VAR>hN' : N'.FG<VAR>hIJ : I ≤ J.jacobson<VAR>hNN : N' ≤ N ⊔ I • N'<VAR>hNN' : N ⊔ N' = N ⊔ I • N'<VAR>h_comap : Function.Injective (comap N.mkQ)<GOAL>N ⊔ N' = N ⊔ J • N'
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I J : Ideal R<VAR>N N' : Submodule R M<VAR>hN' : N'.FG<VAR>hIJ : I ≤ J.jacobson<VAR>hNN : N' ≤ N ⊔ I • N'<VAR>hNN' : N ⊔ N' = N ⊔ I • N'<VAR>h_comap : Function.Injective (comap N.mkQ)<VAR>this : map N.mkQ (I • N') = map N.mkQ N'<GOAL>N ⊔ N' = N ⊔ J • N'
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I J : Ideal R<VAR>N N' : Submodule R M<VAR>hN' : N'.FG<VAR>hIJ : I ≤ J.jacobson<VAR>hNN : N' ≤ N ⊔ I • N'<VAR>hNN' : N ⊔ N' = N ⊔ I • N'<VAR>h_comap : Function.Injective (comap N.mkQ)<VAR>this✝ : map N.mkQ (I • N') = map N.mkQ N'<VAR>this : map N.mkQ N' = J • map N.mkQ N'<GOAL>N ⊔ N' = N ⊔ J • N'
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>a : A<VAR>X : C<GOAL>(shiftFunctorAdd' C a 0 a ⋯).inv.app X = (shiftFunctorZero C A).hom.app ((shiftFunctor C a).obj X)
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>X : FintypeCat<VAR>inst✝¹ : MulAction G ↑X<VAR>inst✝ : MulAction.IsPretransitive G ↑X<VAR>h : Nonempty ↑X<VAR>Y : Action FintypeCat (MonCat.of G)<VAR>i : Y ⟶ Action.FintypeCat.ofMulAction G X<VAR>hm : Mono i<VAR>hni : IsInitial Y → False<GOAL>IsIso i
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>X : FintypeCat<VAR>inst✝¹ : MulAction G ↑X<VAR>inst✝ : MulAction.IsPretransitive G ↑X<VAR>h : Nonempty ↑X<VAR>Y : Action FintypeCat (MonCat.of G)<VAR>i : Y ⟶ Action.FintypeCat.ofMulAction G X<VAR>hm : Mono i<VAR>hni : IsInitial Y → False<VAR>y : ↑Y.V<GOAL>IsIso i
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>X : FintypeCat<VAR>inst✝¹ : MulAction G ↑X<VAR>inst✝ : MulAction.IsPretransitive G ↑X<VAR>h : Nonempty ↑X<VAR>Y : Action FintypeCat (MonCat.of G)<VAR>i : Y ⟶ Action.FintypeCat.ofMulAction G X<VAR>hm : Mono i<VAR>hni : IsInitial Y → False<VAR>y : ↑Y.V<VAR>this : IsIso i.hom<GOAL>IsIso i
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝¹ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝ : Monoid N<GOAL>Submonoid.closure (⋃ i, range ⇑of) = ⊤
<VAR>a b : Prop<GOAL>Xor' a b ↔ (a ↔ ¬b)
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁶ : Fintype ι<VAR>inst✝¹⁵ : Fintype ι'<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹¹ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁹ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁸ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁷ : SeminormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>inst✝⁵ : SeminormedAddCommGroup G'<VAR>inst✝⁴ : NormedSpace 𝕜 G'<VAR>c : 𝕜<VAR>f g : ContinuousMultilinearMap 𝕜 E G<VAR>m : (i : ι) → E i<VAR>𝕜' : Type u_1<VAR>inst✝³ : NormedField 𝕜'<VAR>inst✝² : NormedSpace 𝕜' G<VAR>inst✝¹ : SMulCommClass 𝕜 𝕜' G<VAR>inst✝ : Subsingleton ι<VAR>i : ι<GOAL>‖(ofSubsingleton 𝕜 G G i) (ContinuousLinearMap.id 𝕜 G)‖ ≤ 1
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁶ : Fintype ι<VAR>inst✝¹⁵ : Fintype ι'<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹¹ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁹ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁸ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁷ : SeminormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>inst✝⁵ : SeminormedAddCommGroup G'<VAR>inst✝⁴ : NormedSpace 𝕜 G'<VAR>c : 𝕜<VAR>f g : ContinuousMultilinearMap 𝕜 E G<VAR>m : (i : ι) → E i<VAR>𝕜' : Type u_1<VAR>inst✝³ : NormedField 𝕜'<VAR>inst✝² : NormedSpace 𝕜' G<VAR>inst✝¹ : SMulCommClass 𝕜 𝕜' G<VAR>inst✝ : Subsingleton ι<VAR>i : ι<GOAL>‖ContinuousLinearMap.id 𝕜 G‖ ≤ 1
<VAR>α✝ : Type u_1<VAR>σ : Type u_2<VAR>inst✝³ : Primcodable α✝<VAR>inst✝² : Primcodable σ<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable β<VAR>n : ℕ<GOAL>Nat.unpaired (fun z n => Nat.casesOn n 0 fun y => Nat.unpaired (fun z n => Nat.casesOn n 0 fun y => (Nat.unpair (Nat.pair z y)).1.succ) (Nat.pair (Nat.unpair (Nat.pair z y)).2 (encode (decode (Nat.unpair (Nat.pair z y)).1)))) (Nat.pair (Nat.unpair n).2 (encode (decode (Nat.unpair n).1))) = encode (Option.map Prod.fst (decode n))
<VAR>α✝ : Type u_1<VAR>σ : Type u_2<VAR>inst✝³ : Primcodable α✝<VAR>inst✝² : Primcodable σ<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable β<VAR>n : ℕ<GOAL>Nat.rec 0 (fun n_1 n_ih => Nat.rec 0 (fun n n_ih => n_1.succ) (encode (decode (Nat.unpair n).2))) (encode (decode (Nat.unpair n).1)) = encode (Option.map Prod.fst ((decode (Nat.unpair n).1).bind fun a => Option.map (Prod.mk a) (decode (Nat.unpair n).2)))
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<GOAL>s * ball x δ = x • thickening δ s
<VAR>x : ℝ≥0∞<VAR>z : ℝ<VAR>hx1 : 0 < x<VAR>hx2 : x < 1<VAR>hz : z < 0<GOAL>1 < x ^ z
<VAR>z : ℝ<VAR>hz : z < 0<VAR>x : ℝ≥0<VAR>hx1 : 0 < ↑x<VAR>hx2 : ↑x < 1<GOAL>1 < ↑x ^ z
<VAR>z : ℝ<VAR>hz : z < 0<VAR>x : ℝ≥0<VAR>hx1 : 0 < x<VAR>hx2 : x < 1<GOAL>1 < ↑x ^ z
<VAR>x✝ y✝¹ z✝¹ w x y✝ z✝ : ℝ<VAR>hx : 0 < x<VAR>y z : ℝ<GOAL>x ^ (y + z) = x ^ y * x ^ z
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s✝ t s : Set M<VAR>x : M<VAR>hs : s ⊆ f.source<VAR>hx : x ∈ f.source<GOAL>↑(f.extend I).symm ⁻¹' s ∩ range ↑I =ᶠ[𝓝 (↑(f.extend I) x)] ↑(f.extend I) '' s
<VAR>x y : ℤ<VAR>d : ℕ<VAR>hd : x.gcd y = d<VAR>h : d.beq 1 = false<GOAL>¬IsCoprime x y
<VAR>x y : ℤ<VAR>d : ℕ<VAR>hd : x.gcd y = d<VAR>h : d.beq 1 = false<GOAL>¬d = 1
<VAR>I : Type u_1<VAR>A : Type u_2<VAR>X : I → Type u_3<VAR>inst✝¹ : (i : I) → TopologicalSpace (X i)<VAR>inst✝ : TopologicalSpace A<VAR>f g : (i : I) → C(A, X i)<VAR>S : Set A<VAR>homotopies : (i : I) → (f i).HomotopyRel (g i) S<VAR>t : ↑unitInterval<VAR>x : A<VAR>hx : x ∈ S<GOAL>{ toFun := fun x => __src✝.toFun (t, x), continuous_toFun := ⋯ } x = (ContinuousMap.pi f) x
<VAR>I : Type u_1<VAR>A : Type u_2<VAR>X : I → Type u_3<VAR>inst✝¹ : (i : I) → TopologicalSpace (X i)<VAR>inst✝ : TopologicalSpace A<VAR>f g : (i : I) → C(A, X i)<VAR>S : Set A<VAR>homotopies : (i : I) → (f i).HomotopyRel (g i) S<VAR>t : ↑unitInterval<VAR>x : A<VAR>hx : x ∈ S<GOAL>(Homotopy.pi fun i => (homotopies i).toHomotopy).toContinuousMap (t, x) = fun i => (f i) x
<VAR>I : Type u_1<VAR>A : Type u_2<VAR>X : I → Type u_3<VAR>inst✝¹ : (i : I) → TopologicalSpace (X i)<VAR>inst✝ : TopologicalSpace A<VAR>f g : (i : I) → C(A, X i)<VAR>S : Set A<VAR>homotopies : (i : I) → (f i).HomotopyRel (g i) S<VAR>t : ↑unitInterval<VAR>x : A<VAR>hx : x ∈ S<GOAL>∀ (a : I), (Homotopy.pi fun i => (homotopies i).toHomotopy).toContinuousMap (t, x) a = (f a) x
<VAR>I : Type u_1<VAR>A : Type u_2<VAR>X : I → Type u_3<VAR>inst✝¹ : (i : I) → TopologicalSpace (X i)<VAR>inst✝ : TopologicalSpace A<VAR>f g : (i : I) → C(A, X i)<VAR>S : Set A<VAR>homotopies : (i : I) → (f i).HomotopyRel (g i) S<VAR>t : ↑unitInterval<VAR>x : A<VAR>hx : x ∈ S<VAR>i : I<GOAL>(Homotopy.pi fun i => (homotopies i).toHomotopy).toContinuousMap (t, x) i = (f i) x
<VAR>f : Char → Char<VAR>l : List Char<VAR>c : Char<VAR>r : List Char<GOAL>(if h : { data := l ++ c :: r }.atEnd { byteIdx := utf8Len l } = true then { data := l ++ c :: r } else let c_1 := f ({ data := l ++ c :: r }.get { byteIdx := utf8Len l }); let_fun this := ⋯; let s := { data := l ++ c :: r }.set { byteIdx := utf8Len l } c_1; mapAux f (s.next { byteIdx := utf8Len l }) s) = { data := l ++ List.map f (c :: r) }
<VAR>f : Char → Char<VAR>l : List Char<VAR>c : Char<VAR>r : List Char<GOAL>(let c_1 := f ({ data := l ++ c :: r }.get { byteIdx := utf8Len l }); let_fun this := ⋯; let s := { data := l ++ c :: r }.set { byteIdx := utf8Len l } c_1; mapAux f (s.next { byteIdx := utf8Len l }) s) = { data := l ++ List.map f (c :: r) }
<VAR>f : Char → Char<VAR>l : List Char<VAR>c : Char<VAR>r : List Char<GOAL>mapAux f { byteIdx := utf8Len l + (f c).utf8Size } { data := l ++ f c :: r } = { data := l ++ f c :: List.map f r }
<VAR>R : Type uR<VAR>inst✝⁴ : Semiring R<VAR>S : Type uS<VAR>inst✝³ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra S A<VAR>r✝ : R → R → Prop<VAR>inst✝ : Semiring T<VAR>r : R → R → Prop<VAR>f : RingQuot r →+* T<GOAL>f = lift ⟨f.comp (mkRingHom r), ⋯⟩
<VAR>R : Type uR<VAR>inst✝⁴ : Semiring R<VAR>S : Type uS<VAR>inst✝³ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra S A<VAR>r✝ : R → R → Prop<VAR>inst✝ : Semiring T<VAR>r : R → R → Prop<VAR>f : RingQuot r →+* T<GOAL>lift (lift.symm f) = lift ⟨f.comp (mkRingHom r), ⋯⟩
<VAR>R : Type uR<VAR>inst✝⁴ : Semiring R<VAR>S : Type uS<VAR>inst✝³ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra S A<VAR>r✝ : R → R → Prop<VAR>inst✝ : Semiring T<VAR>r : R → R → Prop<VAR>f : RingQuot r →+* T<GOAL>{ toFun := fun f => preLift ⋯, invFun := fun F => ⟨F.comp (mkRingHom r), ⋯⟩, left_inv := ⋯, right_inv := ⋯ } ({ toFun := fun f => preLift ⋯, invFun := fun F => ⟨F.comp (mkRingHom r), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }.symm f) = { toFun := fun f => preLift ⋯, invFun := fun F => ⟨F.comp (mkRingHom r), ⋯⟩, left_inv := ⋯, right_inv := ⋯ } ⟨f.comp (mkRingHom r), ⋯⟩
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>p q : Set α → Prop<VAR>U : Set α<VAR>ε : ℝ≥0∞<VAR>H : μ.InnerRegularWRT p q<VAR>hU : q U<GOAL>μ U = ⨆ K, ⨆ (_ : K ⊆ U), ⨆ (_ : p K), μ K
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>p q : Set α → Prop<VAR>U : Set α<VAR>ε : ℝ≥0∞<VAR>H : μ.InnerRegularWRT p q<VAR>hU : q U<VAR>r : ℝ≥0∞<VAR>hr : r < μ U<GOAL>r < ⨆ K, ⨆ (_ : K ⊆ U), ⨆ (_ : p K), μ K
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → ℂ<VAR>f' x : ℂ<VAR>h₁ : HasStrictDerivAt f f' x<VAR>h₂ : f x ∈ slitPlane<GOAL>HasStrictDerivAt (fun t => log (f t)) (f' / f x) x
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → ℂ<VAR>f' x : ℂ<VAR>h₁ : HasStrictDerivAt f f' x<VAR>h₂ : f x ∈ slitPlane<GOAL>HasStrictDerivAt (fun t => log (f t)) ((f x)⁻¹ * f') x
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ✝ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝³ : CommMonoid β<VAR>γ : Type u_6<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : OrderedCommMonoid γ<VAR>inst✝ : CovariantClass γ γ (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>s : Finset α<VAR>d : α<VAR>hd : d ∈ s<VAR>f : α → γ<VAR>hdf : 1 < f d<GOAL>∏ m ∈ s.erase d, f m < ∏ m ∈ s, f m
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ✝ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝³ : CommMonoid β<VAR>γ : Type u_6<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : OrderedCommMonoid γ<VAR>inst✝ : CovariantClass γ γ (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>s : Finset α<VAR>d : α<VAR>hd : d ∈ s<VAR>f : α → γ<VAR>hdf : 1 < f d<GOAL>∏ m ∈ s.erase d, f m < ∏ m ∈ insert d (s.erase d), f m
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ✝ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝³ : CommMonoid β<VAR>γ : Type u_6<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : OrderedCommMonoid γ<VAR>inst✝ : CovariantClass γ γ (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>s : Finset α<VAR>d : α<VAR>hd : d ∈ s<VAR>f : α → γ<VAR>hdf : 1 < f d<GOAL>∏ m ∈ s.erase d, f m < f d * ∏ x ∈ s.erase d, f x
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>s t : Set α<VAR>a x y : α<VAR>inst✝¹ : AlexandrovDiscrete α<VAR>inst✝ : AlexandrovDiscrete β<GOAL>IsOpen (exterior s)
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>s t : Set α<VAR>a x y : α<VAR>inst✝¹ : AlexandrovDiscrete α<VAR>inst✝ : AlexandrovDiscrete β<GOAL>IsOpen (⋂₀ {t | IsOpen t ∧ s ⊆ t})
<VAR>k : Type u<VAR>inst✝¹ : Field k<VAR>inst✝ : IsAlgClosed k<VAR>p : k[X]<GOAL>p.roots = 0 ↔ p = C (p.coeff 0)
<VAR>k : Type u<VAR>inst✝¹ : Field k<VAR>inst✝ : IsAlgClosed k<VAR>p : k[X]<VAR>h : p.roots = 0<GOAL>p = C (p.coeff 0)
<VAR>k : Type u<VAR>inst✝¹ : Field k<VAR>inst✝ : IsAlgClosed k<VAR>p : k[X]<VAR>h : p.roots = 0<VAR>hd : p.degree ≤ 0<GOAL>p = C (p.coeff 0)
<VAR>k : Type u<VAR>inst✝¹ : Field k<VAR>inst✝ : IsAlgClosed k<VAR>p : k[X]<VAR>h : p.roots = 0<VAR>hd : 0 < p.degree<GOAL>p = C (p.coeff 0)
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>E : Type u_2<VAR>inst✝¹ : PseudoEMetricSpace E<VAR>β : Type u_3<VAR>inst✝ : LinearOrder β<VAR>f : α → E<VAR>t : Set β<VAR>φ : β → α<VAR>hφ : MonotoneOn φ t<GOAL>eVariationOn (f ∘ φ) t = eVariationOn f (φ '' t)