mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Shift.CommShiftTwo
CategoryTheory.Functor.CommShift₂.commShift_flip_map : ∀ {C₁ : Type u_1} {C₂ : Type u_3} {D : Type u_5} {inst : CategoryTheory.Category.{v_1, u_1} C₁}
  {inst_1 : CategoryTheory.Category.{v_3, u_3} C₂} {inst_2 : CategoryTheory.Category.{v_5, u_5} D} {M : Type u_6}
  {inst_3 : AddCommMonoid M} {inst_4 : CategoryTheory.HasShift C₁ M} {inst_5 : CategoryTheory.HasShift C₂ M}
  {inst_6 : CategoryTheory.HasShift D M} {G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)}
  {h : CategoryTheory.CommShift₂Setup D M} [self : G.CommShift₂ h] {X₂ Y₂ : C₂} (g : X₂ ⟶ Y₂),
  CategoryTheory.NatTrans.CommShift (G.flip.map g) M
-- Mathlib.Logic.Nonempty
Nonempty.elim_to_inhabited : ∀ {α : Sort u_3} [h : Nonempty α] {p : Prop}, (∀ (a : Inhabited α), p) → p
-- Mathlib.Data.Bundle
Bundle.Pullback.lift_snd : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} {B' : Type u_4} (f : B' → B) (a : Bundle.TotalSpace F (f *ᵖ E)),
  (Bundle.Pullback.lift f a).snd = a.snd
-- Mathlib.CategoryTheory.Sites.PreservesLocallyBijective
CategoryTheory.Presheaf.isLocallySurjective_whisker : ∀ {C : Type u_1} {D : Type u_2} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} A]
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D)
  (H : CategoryTheory.Functor C D) {F G : CategoryTheory.Functor Dᵒᵖ A} (f : F ⟶ G) {FA : A → A → Type u_4}
  {CA : A → Type u_5} [inst_3 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
  [inst_4 : CategoryTheory.ConcreteCategory A FA] [H.IsCocontinuous J K]
  [CategoryTheory.Presheaf.IsLocallySurjective K f], CategoryTheory.Presheaf.IsLocallySurjective J (H.op.whiskerLeft f)
-- Mathlib.LinearAlgebra.Projectivization.Basic
Projectivization.instFiniteDimensionalSubtypeMemSubmoduleSubmodule : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (v : Projectivization K V), FiniteDimensional K ↥v.submodule
-- Mathlib.Algebra.Polynomial.Basic
/-- `X` is the polynomial variable (aka indeterminate).  -/
Polynomial.X : {R : Type u} → [inst : Semiring R] → Polynomial R
-- Std.Sat.AIG.Cached
/-- A version of `AIG.mkGate` that uses the subterm cache in `AIG`. This version is meant for
programming, for proving purposes use `AIG.mkGate` and equality theorems to this one.

Beyond caching this function also implements a subset of the optimizations presented in:
 -/
Std.Sat.AIG.mkGateCached : {α : Type} →
  [inst : Hashable α] → [inst_1 : DecidableEq α] → (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α
-- Mathlib.Topology.Order.AtTopBotIxx
tendsto_Iio_atTop : ∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] {a : X} {α : Type u_2}
  {l : Filter α} {f : α → ↑(Set.Iio a)},
  autoParam (Order.IsSuccPrelimit a) tendsto_Iio_atTop._auto_1 →
    (Filter.Tendsto f l Filter.atTop ↔ Filter.Tendsto (fun x => ↑(f x)) l (nhdsWithin a (Set.Iio a)))
-- Init.Data.String.Lemmas.Intercalate
_private.Init.Data.String.Lemmas.Intercalate.0.String.intercalate.eq_1 : ∀ (s : String), s.intercalate [] = ""
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
subalgebraOfSubring_toSubsemiring : ∀ {R : Type u_1} [inst : Ring R] (S : Subring R), (subalgebraOfSubring S).toSubsemiring = S.toSubsemiring
-- Mathlib.Control.Monad.Writer
/-- Transitivity.

see Note [lower instance priority]  -/
monadWriterAdapterTrans : {ω : Type u} →
  {m : Type u → Type u_1} →
    {n : Type u → Type v} → [MonadWriterAdapter ω m] → [MonadFunctor m n] → MonadWriterAdapter ω n
-- Mathlib.Tactic.NormNum.BigOperators
Mathlib.Meta.Finset.univ_eq_elems : ∀ {α : Type u_1} [inst : Fintype α] (elems : Finset α), (∀ (x : α), x ∈ elems) → Finset.univ = elems
-- Mathlib.Logic.Equiv.Basic
Equiv.piCongrLeft_apply_eq_cast : ∀ {α : Sort u_1} {β : Sort u_4} {P : β → Sort v} {e : α ≃ β} (f : (a : α) → P (e a)) (b : β),
  (Equiv.piCongrLeft P e) f b = cast ⋯ (f (e.symm b))
-- Mathlib.Data.Bool.Basic
Bool.and_intro : ∀ {a b : Bool}, a = true → b = true → (a && b) = true
-- Mathlib.Algebra.Free
AddMagma.FreeAddSemigroup.instInhabited.eq_1 : ∀ {α : Type u} [inst : Add α] [inst_1 : Inhabited α],
  AddMagma.FreeAddSemigroup.instInhabited = { default := AddMagma.FreeAddSemigroup.of default }
-- Mathlib.GroupTheory.Solvable
derivedSeries_normal : ∀ (G : Type u_1) [inst : Group G] (n : ℕ), (derivedSeries G n).Normal
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.yonedaAddGrpObj_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (G : C)
  [inst_2 : CategoryTheory.AddGrpObj G] {X Y : Cᵒᵖ} (φ : X ⟶ Y),
  (CategoryTheory.yonedaAddGrpObj G).map φ =
    AddGrpCat.ofHom (AddMonCat.Hom.hom ((CategoryTheory.yonedaAddMonObj G).map φ))
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
/-- The composition of two functors `pullFunctor` is isomorphic to `pullFunctor` applied
to the compositions.  -/
CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} →
              {S' : C} →
                {p : S' ⟶ S} →
                  {ι' : Type t'} →
                    {X' : ι' → C} →
                      {f' : (j : ι') → X' j ⟶ S'} →
                        {α : ι' → ι} →
                          {p' : (j : ι') → X' j ⟶ X (α j)} →
                            (w :
                                ∀ (j : ι'),
                                  CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) =
                                    CategoryTheory.CategoryStruct.comp (f' j) p) →
                              {S'' : C} →
                                {q : S'' ⟶ S'} →
                                  {ι'' : Type t''} →
                                    {X'' : ι'' → C} →
                                      {f'' : (k : ι'') → X'' k ⟶ S''} →
                                        {β : ι'' → ι'} →
                                          {q' : (k : ι'') → X'' k ⟶ X' (β k)} →
                                            (w' :
                                                ∀ (k : ι''),
                                                  CategoryTheory.CategoryStruct.comp (q' k) (f' (β k)) =
                                                    CategoryTheory.CategoryStruct.comp (f'' k) q) →
                                              (r : S'' ⟶ S) →
                                                {r' : (k : ι'') → X'' k ⟶ X (α (β k))} →
                                                  (hr :
                                                      autoParam (CategoryTheory.CategoryStruct.comp q p = r)
                                                        CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso._auto_1) →
                                                    (hr' :
                                                        autoParam
                                                          (∀ (k : ι''),
                                                            CategoryTheory.CategoryStruct.comp (q' k) (p' (β k)) = r' k)
                                                          CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso._auto_3) →
                                                      (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F w).comp
                                                          (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F w') ≅
                                                        CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯
-- Mathlib.Algebra.Category.Grp.FilteredColimits
AddGrpCat.FilteredColimits.forget₂AddMon_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ AddGrpCat AddMonCat)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.add_eq_zero_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SubtractionMonoid α] {s t : Finset α},
  s + t = 0 ↔ ∃ a b, s = {a} ∧ t = {b} ∧ a + b = 0
-- Init.Data.SInt.Lemmas
Int64.neg_neg : ∀ {a : Int64}, - -a = a
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- The inner product is *Hermitian*, taking the `conj` swaps the arguments.  -/
InnerProductSpace.conj_inner_symm : ∀ {𝕜 : Type u_4} {E : Type u_5} {inst : RCLike 𝕜} {inst_1 : SeminormedAddCommGroup E} [self : InnerProductSpace 𝕜 E]
  (x y : E), (starRingEnd 𝕜) (inner 𝕜 y x) = inner 𝕜 x y
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.postcompCLM_apply : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} {F' : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : SMulCommClass ℝ 𝕜 F] [inst_7 : NormedAddCommGroup F'] [inst_8 : NormedSpace ℝ F']
  [inst_9 : NormedSpace 𝕜 F'] [inst_10 : SMulCommClass ℝ 𝕜 F'] {n : ℕ∞} {K : TopologicalSpace.Compacts E}
  [inst_11 : LinearMap.CompatibleSMul F F' ℝ 𝕜] (T : F →L[𝕜] F') (f : ContDiffMapSupportedIn E F n K),
  ⇑((ContDiffMapSupportedIn.postcompCLM T) f) = ⇑T ∘ ⇑f
-- Mathlib.Analysis.Normed.Group.Hom
/-- If `φ : NormedAddGroupHom V₁ V` is such that `f.comp φ = g.comp φ`, the induced morphism
`NormedAddGroupHom V₁ (f.equalizer g)`.  -/
NormedAddGroupHom.Equalizer.lift : {V : Type u_1} →
  {W : Type u_2} →
    {V₁ : Type u_3} →
      [inst : SeminormedAddCommGroup V] →
        [inst_1 : SeminormedAddCommGroup W] →
          [inst_2 : SeminormedAddCommGroup V₁] →
            {f g : NormedAddGroupHom V W} →
              (φ : NormedAddGroupHom V₁ V) → f.comp φ = g.comp φ → NormedAddGroupHom V₁ ↥(f.equalizer g)
-- Init.Data.SInt.Lemmas
Int64.ofIntLE_mul : ∀ {a b : ℤ} {hab₁ : Int64.minValue.toInt ≤ a * b} {hab₂ : a * b ≤ Int64.maxValue.toInt},
  Int64.ofIntLE (a * b) hab₁ hab₂ = Int64.ofInt a * Int64.ofInt b
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
SimpleGraph.finsetWalkLengthLT.eq_1 : ∀ {V : Type u} (G : SimpleGraph V) [inst : DecidableEq V] [inst_1 : G.LocallyFinite] (n : ℕ) (u v : V),
  G.finsetWalkLengthLT n u v = (Finset.range n).disjiUnion (fun l => G.finsetWalkLength l u v) ⋯
-- Mathlib.Topology.Order.MonotoneContinuity
/-- A monotone surjective function with a densely ordered codomain is continuous.  -/
Monotone.continuous_of_surjective : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : α → β},
  Monotone f → Function.Surjective f → Continuous f
-- Mathlib.CategoryTheory.Sites.Subcanonical
CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] {X Y : Cᵒᵖ} (f : X ⟶ Y) {F : CategoryTheory.Sheaf J (Type v)} (t : F.obj.obj X),
  J.yonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (F.obj.map f)) t) =
    CategoryTheory.CategoryStruct.comp (J.yoneda.map f.unop) (J.yonedaEquiv.symm t)
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.add : {R : Type u_1} → [inst : AddMonoid R] → Add (ArithmeticFunction R)
-- Mathlib.RingTheory.Invariant.Basic
/-- A technical lemma for `fixed_of_fixed1`.  -/
_private.Mathlib.RingTheory.Invariant.Basic.0.fixed_of_fixed1_aux1 : ∀ {B : Type u_2} [inst : CommRing B] (G : Type u_3) [inst_1 : Group G] [Finite G] [inst_3 : MulSemiringAction G B]
  (Q : Ideal B) [Q.IsPrime],
  ∃ a b,
    (∀ (g : G), g • a = a) ∧
      a ∉ Q ∧ ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a else 0)
-- Mathlib.Algebra.QuaternionBasis
/-- Two `R`-algebra morphisms from the quaternions are equal if they agree on `i` and `j`.  -/
Quaternion.hom_ext : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A]
  ⦃f g : Quaternion R →ₐ[R] A⦄,
  f (QuaternionAlgebra.Basis.self R).i = g (QuaternionAlgebra.Basis.self R).i →
    f (QuaternionAlgebra.Basis.self R).j = g (QuaternionAlgebra.Basis.self R).j → f = g
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitBall.instIsRightCancelMulZero : ∀ {𝕜 : Type u_1} [inst : NonUnitalSeminormedRing 𝕜] [IsRightCancelMulZero 𝕜], IsRightCancelMulZero ↑(Metric.ball 0 1)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` preserves limits, then `F.unop : C ⥤ D` preserves colimits.  -/
CategoryTheory.Limits.preservesColimitsOfSize_unop : ∀ {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.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.unop
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Ric.Internal.forIn'_eq_forIn'_iter : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerableLeast? α] [inst_6 : Std.Rxc.IsAlwaysFinite α]
  [inst_7 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_8 : Monad m]
  {r : Std.Ric α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f = forIn' (Std.Ric.Internal.iter r) init fun a ha acc => f a ⋯ acc
-- Mathlib.CategoryTheory.Sites.Over
/-- Two identical morphisms give isomorphic `overMapPullback` functors on sheaves.  -/
CategoryTheory.GrothendieckTopology.overMapPullbackCongr : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (A : Type u') →
        [inst_1 : CategoryTheory.Category.{v', u'} A] →
          {X Y : C} → {f g : X ⟶ Y} → f = g → (J.overMapPullback A f ≅ J.overMapPullback A g)
-- Mathlib.Order.Filter.Map
Filter.frequently_bind : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → Filter β} {p : β → Prop},
  (∃ᶠ (y : β) in f.bind m, p y) ↔ ∃ᶠ (x : α) in f, ∃ᶠ (y : β) in m x, p y
-- Mathlib.Combinatorics.Quiver.Path
/-- An arrow witnesses that its target is reachable from its source.  -/
Quiver.Hom.reachable : ∀ {V : Type u} [inst : Quiver V] {a b : V} (e : a ⟶ b), Quiver.Reachable a b
-- Mathlib.Data.List.AList
AList.keys_subset_keys_of_entries_subset_entries : ∀ {α : Type u} {β : α → Type v} {s₁ s₂ : AList β}, s₁.entries ⊆ s₂.entries → s₁.keys ⊆ s₂.keys
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the reverse direction of `Asymptotics.isBigO_abs_left`. -/
Asymptotics.IsBigO.abs_left : ∀ {α : Type u_1} {F : Type u_4} [inst : Norm F] {g : α → F} {l : Filter α} {u : α → ℝ},
  u =O[l] g → (fun x => |u x|) =O[l] g
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- The preimage of the normalizer is equal to the normalizer of the preimage of a surjective
function.  -/
Subgroup.comap_normalizer_eq_of_surjective : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (H : Subgroup G) {f : N →* G},
  Function.Surjective ⇑f → Subgroup.comap f (Subgroup.normalizer ↑H) = Subgroup.normalizer ↑(Subgroup.comap f H)
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.default_def : ∀ (V : Type u), default = ⊥
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `antivaryOn_inv_right₀`. -/
MonovaryOn.inv_right₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : Semifield β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] {s : Set ι} {f : ι → α} {g : ι → β},
  (∀ i ∈ s, 0 < g i) → MonovaryOn f g s → AntivaryOn f g⁻¹ s
-- Mathlib.Topology.Algebra.Support
HasCompactSupport.comp_left : ∀ {α : Type u_2} {β : Type u_4} {γ : Type u_5} [inst : TopologicalSpace α] [inst_1 : Zero β] [inst_2 : Zero γ]
  {g : β → γ} {f : α → β}, HasCompactSupport f → g 0 = 0 → HasCompactSupport (g ∘ f)
-- Mathlib.Topology.MetricSpace.Holder
/-- **Alias** of the reverse direction of `holderWith_one`. -/
LipschitzWith.holderWith : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C : NNReal} {f : X → Y},
  LipschitzWith C f → HolderWith C 1 f
-- Mathlib.Data.Set.Defs
/-- Unexpander for set builder notation.  -/
Mathlib.Meta.ofPred.unexpander : Lean.PrettyPrinter.Unexpander
-- Std.Data.DTreeMap.Internal.Def
Std.DTreeMap.Internal.instInhabitedImpl : {a : Type u_1} → {a_1 : a → Type u_2} → Inhabited (Std.DTreeMap.Internal.Impl a a_1)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.count_le_of_ideal_ge : ∀ {T : Type u_4} [inst : CommRing T] [inst_1 : IsDedekindDomain T] {I J : Ideal T},
  I ≤ J →
    I ≠ ⊥ →
      ∀ (K : Ideal T),
        Multiset.count K (UniqueFactorizationMonoid.normalizedFactors J) ≤
          Multiset.count K (UniqueFactorizationMonoid.normalizedFactors I)
-- Mathlib.Data.List.Pi
/-- Given `f` a function whose domain is `i :: l`, produce a function whose domain
is restricted to `l`.  -/
List.Pi.tail : {ι : Type u_1} → {α : ι → Sort u_2} → {i : ι} → {l : List ι} → ((j : ι) → j ∈ i :: l → α j) → (j : ι) → j ∈ l → α j
-- Mathlib.Data.Nat.Sqrt
Nat.sqrt_le_sqrt : ∀ {m n : ℕ}, m ≤ n → m.sqrt ≤ n.sqrt
-- Mathlib.Analysis.Convex.Star
starConvex_iUnion₂ : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {x : E} {ι : Sort u_4} {κ : ι → Sort u_5} {s : (i : ι) → κ i → Set E},
  (∀ (i : ι) (j : κ i), StarConvex 𝕜 x (s i j)) → StarConvex 𝕜 x (⋃ i, ⋃ j, s i j)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.splitEpiBiproductComparison_section_ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {J : Type w₁}
  (F : CategoryTheory.Functor C D) (f : J → C) [inst_4 : CategoryTheory.Limits.HasBiproduct f]
  [inst_5 : CategoryTheory.Limits.HasBiproduct (F.obj ∘ f)] [inst_6 : F.PreservesZeroMorphisms],
  (F.splitEpiBiproductComparison f).section_ = F.biproductComparison' f
-- Mathlib.GroupTheory.OrderOfElement
/-- Elements of finite additive order are closed under addition.  -/
IsOfFinAddOrder.add : ∀ {G : Type u_1} [inst : AddCommMonoid G] {x y : G}, IsOfFinAddOrder x → IsOfFinAddOrder y → IsOfFinAddOrder (x + y)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.comp_fst : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {x : MeasurableSpace α} [mβ : MeasurableSpace β]
  [inst : TopologicalSpace γ] {f : α → γ},
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun z => f z.1
-- Mathlib.Algebra.Group.Subgroup.Defs
HasMemOrNegMem.neg_mem_of_notMem : ∀ {S : Type u_3} {G : Type u_4} [inst : Neg G] [inst_1 : SetLike S G] (s : S) [HasMemOrNegMem s], ∀ x ∉ s, -x ∈ s
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_eq_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [inst_2 : Inhabited α] {k : α}, t.contains k = true → t.get! k = k
-- Mathlib.Data.Multiset.Lattice
Multiset.sup_coe : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (l : List α),
  (↑l).sup = List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ l
-- Mathlib.Tactic.FBinop
_private.Mathlib.Tactic.FBinop.0.FBinopElab.Tree.term.injEq : ∀ (ref : Lean.Syntax) (infoTrees : Lean.PersistentArray Lean.Elab.InfoTree) (val : Lean.Expr) (ref_1 : Lean.Syntax)
  (infoTrees_1 : Lean.PersistentArray Lean.Elab.InfoTree) (val_1 : Lean.Expr),
  (FBinopElab.Tree.term✝ ref infoTrees val = FBinopElab.Tree.term✝ ref_1 infoTrees_1 val_1) =
    (ref = ref_1 ∧ infoTrees = infoTrees_1 ∧ val = val_1)
-- Mathlib.Algebra.Order.Kleene
Prod.fst_kstar : ∀ {α : Type u_1} {β : Type u_2} [inst : KleeneAlgebra α] [inst_1 : KleeneAlgebra β] (a : α × β),
  (KStar.kstar a).1 = KStar.kstar a.1
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.codRestrict₂.congr_simp : ∀ {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} {M₃ : Type u_8} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : AddCommMonoid M₃]
  [inst_5 : Module R M] [inst_6 : Module R M₁] [inst_7 : Module R M₂] [inst_8 : Module R M₃]
  (f f_1 : M₁ →ₗ[R] M₂ →ₗ[R] M) (e_f : f = f_1) (i i_1 : M₃ →ₗ[R] M) (e_i : i = i_1) (hi : Function.Injective ⇑i)
  (hf : ∀ (x : M₁) (y : M₂), (f x) y ∈ i.range), f.codRestrict₂ i hi hf = f_1.codRestrict₂ i_1 ⋯ ⋯
-- Lean.Meta.Tactic.Grind.EMatch
/-- When using the mod-time optimization with multi-patterns,
we must start ematching at each different pattern. That is,
if we have `[p₁, p₂, p₃]`, we must execute
- `main p₁ [.continue p₂, .continue p₃]`
- `main p₂ [.continue p₁, .continue p₃]`
- `main p₃ [.continue p₁, .continue p₂]`
 -/
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.ematchTheorem.tryAll : List Lean.Expr → List Lean.Meta.Grind.EMatch.Cnstr → Lean.Meta.Grind.EMatch.M Unit
-- Aesop.Index
_private.Aesop.Index.0.Aesop.Index.unindex.filterDiscrTree' : {α : Type} →
  (Aesop.Rule α → Bool) →
    Lean.PHashSet (Aesop.Rule α) →
      Lean.Meta.DiscrTree (Aesop.Rule α) → Lean.Meta.DiscrTree (Aesop.Rule α) × Lean.PHashSet (Aesop.Rule α)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
/-- The function `Real.sin` is real analytic.  -/
Real.analyticAt_sin : ∀ {x : ℝ}, AnalyticAt ℝ Real.sin x
-- Mathlib.Geometry.Manifold.Bordism
/-- The product of a singular `I`- and a singular `J`-manifold into a one-point space
is a singular `I.prod J`-manifold.
This construction is used to prove that the bordism group of `PUnit` is a graded commutative ring.

NB. This definition as written makes sense more generally, for `SingularManifold X k I` whenever `X`
is a topological (additive) group. However, this would not be the correct definition if `X` is not
`(P)Unit`: the bordism ring can be defined for every `C^k` manifold `X`, but the product of two
singular manifolds `(M, f)` and `(N, g)` is the fibre product of `M` and `N` w.r.t. `f` and `g`,
with its induced map into `X`.
(If `f` and `g` intersect transversely, this fibre product is a smooth manifold, of dimension
`dim M + dim N - dim X`. Otherwise, the transversality theorem proves that `f` (or `g`) admits an
arbitrarily small perturbation `f'` so `f'` and `g` are transverse. One can prove that different
perturbations yield bordant manifolds.)
 -/
SingularManifold.prod : {k : WithTop ℕ∞} →
  {E : Type u_4} →
    {H : Type u_5} →
      [inst : NormedAddCommGroup E] →
        [inst_1 : NormedSpace ℝ E] →
          [inst_2 : FiniteDimensional ℝ E] →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners ℝ E H} →
                {E' : Type u_7} →
                  {H' : Type u_8} →
                    [inst_4 : NormedAddCommGroup E'] →
                      [inst_5 : NormedSpace ℝ E'] →
                        [inst_6 : TopologicalSpace H'] →
                          {I' : ModelWithCorners ℝ E' H'} →
                            [inst_7 : FiniteDimensional ℝ E'] →
                              SingularManifold PUnit.{u_10 + 1} k I →
                                SingularManifold PUnit.{u_12 + 1} k I' → SingularManifold PUnit.{u_13 + 1} k (I.prod I')
-- Lean.Data.Json.Basic
Lean.Json.getObjVal? : Lean.Json → String → Except String Lean.Json
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits
SheafOfModules.instPreservesFiniteLimitsFunctorOppositeAddCommGrpCatCompSheafToSheafSheafToPresheaf : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  (R : CategoryTheory.Sheaf J RingCat),
  CategoryTheory.Limits.PreservesFiniteLimits
    ((SheafOfModules.toSheaf R).comp (CategoryTheory.sheafToPresheaf J AddCommGrpCat))
-- Lean.Elab.Tactic.Rewrite
_private.Lean.Elab.Tactic.Rewrite.0.Lean.Elab.Tactic.instEvalExprConfig.evalExpr : Lean.Expr → Lean.MetaM Lean.Meta.Rewrite.Config