mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.interFst_s₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S)
  (F : CategoryTheory.PreOneHypercover S)
  [inst_1 : ∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)]
  [inst_2 :
    ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b),
      CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i))
        (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))]
  {i j : (E.inter F).I₀} (k : (E.inter F).I₁ i j), (E.interFst F).s₁ k = k.1
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Subgroup.op.instNormal : ∀ {G : Type u_2} [inst : Group G] {H : Subgroup G} [H.Normal], H.op.Normal
-- Lean.Parser.Term.Basic
Lean.Parser.Term.implicitBinder.formatter : optParam Bool false → Lean.PrettyPrinter.Formatter
-- Mathlib.AlgebraicTopology.DoldKan.Normalized
AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap_assoc : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] [inst_1 : CategoryTheory.Abelian A]
  (X : CategoryTheory.SimplicialObject A) {Z : ChainComplex A ℕ}
  (h : (AlgebraicTopology.alternatingFaceMapComplex A).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex X)
      (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.inclusionOfMooreComplexMap X) h) =
    CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty h
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_empty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} [Std.TransOrd α] [inst : Std.LawfulEqOrd α] {a : α},
  Std.DTreeMap.Internal.Impl.empty.get? a = none
-- Mathlib.CategoryTheory.Preadditive.LeftExact
/-- A functor between preadditive categories which preserves cokernels preserves finite coproducts.
 -/
CategoryTheory.Functor.isColimitMapCoconeBinaryCofanOfPreservesCokernels : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.Preadditive D] →
            (F : CategoryTheory.Functor C D) →
              [F.PreservesZeroMorphisms] →
                {X Y Z : C} →
                  (ι₁ : X ⟶ Z) →
                    (ι₂ : Y ⟶ Z) →
                      [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair ι₂ 0) F] →
                        CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk ι₁ ι₂) →
                          CategoryTheory.Limits.IsColimit (F.mapCocone (CategoryTheory.Limits.BinaryCofan.mk ι₁ ι₂))
-- Mathlib.Analysis.Normed.Group.Basic
norm_le_norm_add_norm_neg_add : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (u v : E), ‖u‖ ≤ ‖v‖ + ‖-u + v‖
-- Lean.Parser.Command
Lean.Parser.Command.register_tactic_tag.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.TransvectionStruct.inv_i : ∀ {n : Type u_1} {R : Type u₂} [inst : CommRing R] (t : Matrix.TransvectionStruct n R), t.inv.i = t.i
-- Mathlib.Topology.Bornology.Hom
LocallyBoundedMap.coe_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Bornology α] [inst_1 : Bornology β] [inst_2 : Bornology γ]
  (f : LocallyBoundedMap β γ) (g : LocallyBoundedMap α β), ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropAt_congr_iff_of_eventuallyEq : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'}
  {P : (H → H') → Set H → H → Prop} {g g' : M → M'} {x : M},
  G.LocalInvariantProp G' P → g' =ᶠ[nhds x] g → (ChartedSpace.LiftPropAt P g' x ↔ ChartedSpace.LiftPropAt P g x)
-- Mathlib.Order.CompleteBooleanAlgebra
iInf_sup_of_monotone : ∀ {α : Type u} [inst : Order.Coframe α] {ι : Type u_1} [inst_1 : Preorder ι] [IsCodirectedOrder ι] {f g : ι → α},
  Monotone f → Monotone g → ⨅ i, f i ⊔ g i = (⨅ i, f i) ⊔ ⨅ i, g i
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instSMulWithZeroOfContinuousConstSMul : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : Zero β] →
          {R : Type u_5} →
            [inst_3 : Zero R] →
              [inst_4 : SMulWithZero R β] →
                [ContinuousConstSMul R β] → SMulWithZero R (CompactlySupportedContinuousMap α β)
-- Mathlib.Tactic.Ring.Common
/-- Cast `ExBase btℕ sℕ` to `ExBaseNat`.  -/
Mathlib.Tactic.Ring.Common.ExBase.toExBaseNat : (e : Q(ℕ)) →
  Mathlib.Tactic.Ring.Common.ExBase Mathlib.Tactic.Ring.Common.btℕ Mathlib.Tactic.Ring.Common.sℕ e →
    (e' : Q(ℕ)) × Mathlib.Tactic.Ring.Common.ExBaseNat e'
-- Mathlib.Geometry.Convex.Cone.Dual
PointedCone.dual_dual_flip_dual : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {p : M →ₗ[R] N →ₗ[R] R} (s : Set M),
  PointedCone.dual p ↑(PointedCone.dual p.flip ↑(PointedCone.dual p s)) = PointedCone.dual p s
-- Mathlib.Topology.DiscreteSubset
Disjoint.nhdsWithin_eq_of_cofinite : ∀ {X : Type u_1} [inst : TopologicalSpace X] {p : X} {s : Set X},
  Disjoint (nhdsWithin p s) Filter.cofinite → nhdsWithin p s = Filter.principal ({x | x ⤳ p} ∩ s)
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.loopyOn_empty : ∀ (α : Type u_2), Matroid.loopyOn ∅ = Matroid.emptyOn α
-- Mathlib.Analysis.Complex.Trigonometric
/-- The real hyperbolic tangent function, defined as the real part of
the complex hyperbolic tangent  -/
Real.tanh : ℝ → ℝ
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitSource.mbtc.inj : ∀ {a b : Lean.Expr} {i : ℕ} {a_1 b_1 : Lean.Expr} {i_1 : ℕ},
  Lean.Meta.Grind.SplitSource.mbtc a b i = Lean.Meta.Grind.SplitSource.mbtc a_1 b_1 i_1 → a = a_1 ∧ b = b_1 ∧ i = i_1
-- Mathlib.Analysis.Normed.Field.Lemmas
TendstoLocallyUniformlyOn.inv₀_of_disjoint : ∀ {α : Type u_1} [inst : NormedDivisionRing α] {X : Type u_4} {ι : Type u_5} [inst_1 : TopologicalSpace X] {s : Set X}
  {F : ι → X → α} {f : X → α} {l : Filter ι},
  TendstoLocallyUniformlyOn F f l s →
    (∀ x ∈ s, Disjoint (Filter.map f (nhdsWithin x s)) (nhds 0)) → TendstoLocallyUniformlyOn F⁻¹ f⁻¹ l s
-- Init.Data.List.Find
_private.Init.Data.List.Find.0.List.of_findIdx?_eq_some.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → ((a : α) → motive (some a)) → (Unit → motive none) → motive x
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.lcm_empty : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {f : β → α}, ∅.lcm f = 1
-- Mathlib.Order.Filter.Prod
Filter.Eventually.prod_inr : ∀ {α : Type u_1} {β : Type u_2} {lb : Filter β} {p : β → Prop},
  (∀ᶠ (x : β) in lb, p x) → ∀ (la : Filter α), ∀ᶠ (x : α × β) in la ×ˢ lb, p x.2
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
/-- If each component of the counit is an epimorphism, then the right adjoint is faithful.  -/
CategoryTheory.Adjunction.faithful_R_of_epi_counit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R)
  [∀ (X : D), CategoryTheory.Epi (h.counit.app X)], R.Faithful
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
/-- The partial derivative `W_X(X, Y, Z)` with respect to `X` of the polynomial `W(X, Y, Z)`
associated to a Weierstrass curve `W` in projective coordinates.  -/
WeierstrassCurve.Projective.polynomialX : {R : Type r} → [inst : CommRing R] → WeierstrassCurve.Projective R → MvPolynomial (Fin 3) R
-- Mathlib.CategoryTheory.Presentable.Limits
CategoryTheory.isClosedUnderColimitsOfShape_isCardinalPresentable : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {κ : Cardinal.{w}}
  [inst_2 : Fact κ.IsRegular] {J : Type u'} [inst_3 : CategoryTheory.Category.{v', u'} J]
  [CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (Type w)],
  HasCardinalLT (CategoryTheory.Arrow J) κ → (CategoryTheory.isCardinalPresentable C κ).IsClosedUnderColimitsOfShape J
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.prodEquiv.eq_1 : ∀ {N : Type u_2} [inst : MulOneClass N] {M : Type u_5} [inst_1 : MulOneClass M] (s : Submonoid M) (t : Submonoid N),
  s.prodEquiv t = { toEquiv := Equiv.Set.prod ↑s ↑t, map_mul' := ⋯ }
-- Batteries.Classes.Order
Std.TransOrd.instOrdLex' : ∀ {α : Type u_1} (ord₁ ord₂ : Ord α) [Std.TransOrd α] [Std.TransOrd α], Std.TransOrd α
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.Instance.mk : Lean.Expr → Array ℕ → Lean.Meta.SynthInstance.Instance
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_filterMap : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.ExtDHashMap α fun x => β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : α → β → Option γ} {k : α} {fallback : γ},
  Std.ExtDHashMap.Const.getD (Std.ExtDHashMap.filterMap f m) k fallback =
    ((Std.ExtDHashMap.Const.get? m k).pbind fun x_2 h' => f (m.getKey k ⋯) x_2).getD fallback
-- Mathlib.LinearAlgebra.Pi
LinearEquiv.sumArrowLequivProdArrow_symm_apply_inl : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α : Type u_5}
  {β : Type u_6} (f : α → M) (g : β → M) (a : α),
  (LinearEquiv.sumArrowLequivProdArrow α β R M).symm (f, g) (Sum.inl a) = f a
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.G.eq_1 : ∀ (L : List (List (Option ℕ))),
  Nat.Partrec.Code.G✝ L =
    some
      (have a := Denumerable.ofNat (ℕ × Nat.Partrec.Code) L.length;
      have k := a.1;
      have c := a.2;
      List.map
        (fun n =>
          Nat.casesOn k none fun k' =>
            Nat.Partrec.Code.recOn c (some 0) (some n.succ) (some (Nat.unpair n).1) (some (Nat.unpair n).2)
              (fun cf cg x x_1 => do
                let x ← Nat.Partrec.Code.lup✝ L (k, cf) n
                let y ← Nat.Partrec.Code.lup✝ L (k, cg) n
                some (Nat.pair x y))
              (fun cf cg x x_1 => do
                let x ← Nat.Partrec.Code.lup✝ L (k, cg) n
                Nat.Partrec.Code.lup✝ L (k, cf) x)
              (fun cf cg x x_1 =>
                have z := (Nat.unpair n).1;
                Nat.casesOn (Nat.unpair n).2 (Nat.Partrec.Code.lup✝ L (k, cf) z) fun y => do
                  let i ← Nat.Partrec.Code.lup✝ L (k', c) (Nat.pair z y)
                  Nat.Partrec.Code.lup✝ L (k, cg) (Nat.pair z (Nat.pair y i)))
              fun cf x =>
              have z := (Nat.unpair n).1;
              have m := (Nat.unpair n).2;
              do
              let x ← Nat.Partrec.Code.lup✝ L (k, cf) (Nat.pair z m)
              Nat.casesOn x (some m) fun x => Nat.Partrec.Code.lup✝ L (k', c) (Nat.pair z (m + 1)))
        (List.range k))
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Subcomplex.map_ι_liftPath : ∀ {X : SSet} (A : X.Subcomplex) {n : ℕ} (p : X.Path n)
  (hp₀ : ∀ (j : Fin (n + 1)), p.vertex j ∈ A.obj (Opposite.op { len := 0 }))
  (hp₁ : ∀ (j : Fin n), p.arrow j ∈ A.obj (Opposite.op { len := 1 })), (A.liftPath p hp₀ hp₁).map A.ι = p
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
_private.Mathlib.Algebra.BigOperators.Group.Finset.Defs.0.BigOperators.FinsetResult.Ioi.sizeOf_spec : ∀ (n : Lean.Term), sizeOf (BigOperators.FinsetResult.Ioi✝ n) = 1 + sizeOf n
-- Batteries.Data.List.Lemmas
/-- **Alias** of `List.rel_of_isChain_cons_cons`. -/
List.IsChain.rel : ∀ {α : Type u_1} {R : α → α → Prop} {a b : α} {l : List α}, List.IsChain R (a :: b :: l) → R a b
-- Mathlib.Order.Zorn
zorn_superset_nonempty : ∀ {α : Type u_1} (S : Set (Set α)),
  (∀ c ⊆ S, IsChain (fun x1 x2 => x1 ⊆ x2) c → c.Nonempty → ∃ lb ∈ S, ∀ s ∈ c, lb ⊆ s) →
    ∀ x ∈ S, ∃ m ⊆ x, Minimal (fun x => x ∈ S) m
-- Mathlib.Analysis.Normed.Group.Constructions
ULift.seminormedAddCommGroup.eq_1 : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E],
  ULift.seminormedAddCommGroup =
    SeminormedAddCommGroup.induced (ULift.{u_5, u_2} E) E { toFun := ULift.down, map_zero' := ⋯, map_add' := ⋯ }
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getEntryGE!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited (α × β)] {k : α}, t₁.Equiv t₂ → t₁.getEntryGE! k = t₂.getEntryGE! k
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.leftOp : Cᵒᵖ ⥤ D` preserves limits, then `F : C ⥤ Dᵒᵖ` preserves colimits.  -/
CategoryTheory.Limits.preservesColimits_of_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesLimits F.leftOp],
  CategoryTheory.Limits.PreservesColimits F
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.cylinder.homotopyEquiv_homotopyHomInvId : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasCylinder]
  (hc : ∀ (j : ι), ∃ i, c.Rel i j),
  (HomologicalComplex.cylinder.homotopyEquiv K hc).homotopyHomInvId = HomologicalComplex.cylinder.πCompι₀Homotopy K hc
-- Mathlib.Data.Fintype.Card
Finset.card_lt_iff_ne_univ : ∀ {α : Type u_1} [inst : Fintype α] (s : Finset α), s.card < Fintype.card α ↔ s ≠ Finset.univ
-- Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
Lean.Meta.Grind.Arith.Linear.LinearM.getRing : Lean.Meta.Grind.Arith.Linear.LinearM Lean.Meta.Grind.Arith.CommRing.Ring
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.sumCongr_inr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_9} [inst_6 : TopologicalSpace M]
  [inst_7 : ChartedSpace H M] {n : WithTop ℕ∞} {M' : Type u_13} [inst_8 : TopologicalSpace M']
  [inst_9 : ChartedSpace H M'] {N : Type u_15} [inst_10 : TopologicalSpace N] [inst_11 : ChartedSpace H N]
  {J : ModelWithCorners 𝕜 E' H} {N' : Type u_17} [inst_12 : TopologicalSpace N'] [inst_13 : ChartedSpace H N']
  (φ : Diffeomorph I J M N n) (ψ : Diffeomorph I J M' N' n), ⇑(φ.sumCongr ψ) ∘ Sum.inr = Sum.inr ∘ ⇑ψ
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.uliftCoyonedaEquiv.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {F : CategoryTheory.Functor C (Type (max w v₁))},
  CategoryTheory.uliftCoyonedaEquiv =
    {
      toFun := fun τ =>
        (CategoryTheory.ConcreteCategory.hom (τ.app (Opposite.unop X)))
          { down := CategoryTheory.CategoryStruct.id (Opposite.unop X) },
      invFun := fun x =>
        { app := fun Y => TypeCat.ofHom fun y => (CategoryTheory.ConcreteCategory.hom (F.map y.down)) x,
          naturality := ⋯ },
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- **Alias** of `FunLike.coe_add`. -/
AddGroupNorm.coe_add : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Add β]
  [IsAddApply F α β] (f g : F), ⇑(f + g) = ⇑f + ⇑g
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivWithinAt_inter : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s t : Set 𝕜},
  t ∈ nhds x → (HasDerivWithinAt f f' (s ∩ t) x ↔ HasDerivWithinAt f f' s x)
-- Lean.Elab.Tactic.Conv.Simp
Lean.Elab.Tactic.Conv.evalSimp : Lean.Elab.Tactic.Tactic
-- Mathlib.GroupTheory.Coset.Defs
QuotientAddGroup.instInhabitedQuotientAddSubgroup : {α : Type u_1} → [inst : AddGroup α] → (s : AddSubgroup α) → Inhabited (α ⧸ s)
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.DiagramOfCocones.mk.sizeOf_spec : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} [inst_3 : SizeOf J] [inst_4 : SizeOf K]
  [inst_5 : SizeOf C] (obj : (j : J) → CategoryTheory.Limits.Cocone (F.obj j))
  (map : {j j' : J} → (f : j ⟶ j') → obj j ⟶ (CategoryTheory.Limits.Cocone.precompose (F.map f)).obj (obj j'))
  (id :
    autoParam (∀ (j : J), (map (CategoryTheory.CategoryStruct.id j)).hom = CategoryTheory.CategoryStruct.id (obj j).pt)
      CategoryTheory.Limits.DiagramOfCocones.id._autoParam)
  (comp :
    autoParam
      (∀ {j₁ j₂ j₃ : J} (f : j₁ ⟶ j₂) (g : j₂ ⟶ j₃),
        (map (CategoryTheory.CategoryStruct.comp f g)).hom = CategoryTheory.CategoryStruct.comp (map f).hom (map g).hom)
      CategoryTheory.Limits.DiagramOfCocones.comp._autoParam),
  sizeOf { obj := obj, map := map, id := id, comp := comp } = 1
-- Mathlib.Algebra.Group.Action.Defs
AddMonoid.toAddAction.eq_1 : ∀ (M : Type u_1) [inst : AddMonoid M],
  AddMonoid.toAddAction M = { vadd := fun x1 x2 => x1 + x2, add_vadd := ⋯, zero_vadd := ⋯ }
-- Init.Data.BitVec.Bitblast
BitVec.resRec.eq_def : ∀ {w : ℕ} (x y : BitVec w) (s : ℕ) (hs : s < w) (hslt : 0 < s),
  x.resRec y s hs hslt =
    match hs0 : s, hs, hslt with
    | 0, hs, hslt => ⋯.elim
    | s'.succ, hs, hslt =>
      match hs' : s', hs, hslt, hs0 with
      | 0, hs, hslt, hs0 => x.aandRec y 1 hs
      | s''.succ, hs, hslt, hs0 => x.resRec y s' ⋯ ⋯ || x.aandRec y s ⋯
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.formatWeekdayLong : Std.Time.DateFormatSymbols → Std.Time.Weekday → String
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
/-- An abbreviation for a Weierstrass curve in Jacobian coordinates.  -/
WeierstrassCurve.Jacobian : Type r → Type r
-- Mathlib.Analysis.Normed.Group.Defs
SeminormedAddGroup.toPseudoMetricSpace : {E : Type u_8} → [self : SeminormedAddGroup E] → PseudoMetricSpace E
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Adjunction.injective_of_map_injective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) [G.Full] [G.Faithful] (I : D), CategoryTheory.Injective (G.obj I) → CategoryTheory.Injective I
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.algebraMap_apply : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  (x : ↥S), (algebraMap (↥S) L) x = ↑x
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.toPartialEquiv_injective : ∀ {X : Type u_1} {G : Type u_2} [inst : SMul G X], Function.Injective Equidecomp.toPartialEquiv
-- Mathlib.MeasureTheory.OuterMeasure.Defs
MeasureTheory.OuterMeasure.mk : {α : Type u_2} →
  (measureOf : Set α → ENNReal) →
    measureOf ∅ = 0 →
      (∀ {s₁ s₂ : Set α}, s₁ ⊆ s₂ → measureOf s₁ ≤ measureOf s₂) →
        (∀ (s : ℕ → Set α), Pairwise (Function.onFun Disjoint s) → measureOf (⋃ i, s i) ≤ ∑' (i : ℕ), measureOf (s i)) →
          MeasureTheory.OuterMeasure α
-- Mathlib.Tactic.Core
/-- `iterateUntilFailureCount` is similar to `iterateUntilFailure` except it counts
the number of successful calls to `tac`. Always succeeds.
 -/
Lean.Elab.Tactic.iterateUntilFailureCount : {m : Type → Type u} → [Monad m] → [MonadExcept Lean.Exception m] → {α : Type} → m α → m ℕ
-- Mathlib.SetTheory.Descriptive.Tree
Descriptive.coe_def : ∀ (A : Type u_1) (self : ↥(Descriptive.tree A)), ↑self = ↑self
-- Lean.Meta.Match.SimpH
/-- Auxiliary method for simplifying equational theorem hypotheses.

Recall that each equation contains additional hypotheses to ensure the associated case was not taken by previous cases.
We have one hypothesis for each previous case.
 -/
Lean.Meta.Match.simpH? : Lean.Expr → ℕ → Lean.MetaM (Option Lean.Expr)
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.ae_restrict_of_ae : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {p : α → Prop},
  (∀ᵐ (x : α) ∂μ, p x) → ∀ᵐ (x : α) ∂μ.restrict s, p x
-- Init.Data.String.Lemmas.Order
String.Pos.endPos_le : ∀ {s : String} (p : s.Pos), s.endPos ≤ p ↔ p = s.endPos
-- Mathlib.Topology.Category.TopCat.GrothendieckTopology
/-- The precoverage on `TopCat` given by jointly surjective families of open embeddings.  -/
TopCat.precoverage : CategoryTheory.Precoverage TopCat
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MCasesPat.brecOn.eq : ∀ {motive_1 : Lean.Parser.Tactic.MCasesPat → Sort u} {motive_2 : List Lean.Parser.Tactic.MCasesPat → Sort u}
  (t : Lean.Parser.Tactic.MCasesPat) (F_1 : (t : Lean.Parser.Tactic.MCasesPat) → t.below → motive_1 t)
  (F_2 : (t : List Lean.Parser.Tactic.MCasesPat) → Lean.Parser.Tactic.MCasesPat.below_1 t → motive_2 t),
  t.brecOn F_1 F_2 = F_1 t (Lean.Parser.Tactic.MCasesPat.brecOn.go t F_1 F_2).2
-- Mathlib.Algebra.Order.GroupWithZero.WithZero
WithZero.withZeroUnitsEquiv_strictMono : ∀ {α : Type u_1} [inst : LinearOrderedCommGroupWithZero α], StrictMono ⇑WithZero.withZeroUnitsEquiv
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {s t : CategoryTheory.Limits.Cone F} (P : CategoryTheory.Limits.IsLimit s)
  (Q : CategoryTheory.Limits.IsLimit t) (j : J) {Z : C} (h : F.obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (P.conePointUniqueUpToIso Q).hom
      (CategoryTheory.CategoryStruct.comp (t.π.app j) h) =
    CategoryTheory.CategoryStruct.comp (s.π.app j) h
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instContinuousConstVAdd : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : VAdd M X] [inst_2 : ContinuousConstVAdd M X],
  ContinuousConstVAdd M (SeparationQuotient X)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- `X ^⦋n⦌` denotes the `n`th-term of the cosimplicial object X  -/
Simplicial.«term_^⦋_⦌» : Lean.TrailingParserDescr
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.instInhabitedSigmaQuotedConstMkStr1NilLevelExBaseNat : Inhabited ((e : Q(ℕ)) × Mathlib.Tactic.Ring.Common.ExBaseNat e)
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
_private.Init.Data.String.Lemmas.Pattern.String.ForwardPattern.0.String.Slice.Pos.skipWhile.match_1.eq_1 : ∀ {s : String.Slice} (motive : Option s.Pos → Sort u_1) (nextCurr : s.Pos)
  (h_1 : (nextCurr : s.Pos) → motive (some nextCurr)) (h_2 : Unit → motive none),
  (match some nextCurr with
    | some nextCurr => h_1 nextCurr
    | none => h_2 ()) =
    h_1 nextCurr
-- Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
/-- (Implementation): Use `ChartedSpace.stalkMap_locallyRingedSpaceMap_evalHom`.  -/
ChartedSpace.stalkMap_locallyRingedSpaceMapAux : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {EM : Type u_1} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_2} [inst_3 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM}
  {M : Type u} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace HM M] {EN : Type u_3}
  [inst_6 : NormedAddCommGroup EN] [inst_7 : NormedSpace 𝕜 EN] {HN : Type u_4} [inst_8 : TopologicalSpace HN]
  {IN : ModelWithCorners 𝕜 EN HN} {N : Type u} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace HN N] (f : M → N)
  (hf : ContMDiff IM IN (↑⊤) f) (x : M),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (ChartedSpace.locallyRingedSpaceMapAux f hf) x)
      (smoothSheafCommRing.evalHom IM (modelWithCornersSelf 𝕜 𝕜) M 𝕜 x) =
    smoothSheafCommRing.evalHom IN (modelWithCornersSelf 𝕜 𝕜) N 𝕜 (f x)