mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Additive
/-- An additive functor induces a functor between homological complexes.
This is sometimes called the "prolongation".
 -/
CategoryTheory.Functor.mapHomologicalComplex : {ι : Type u_1} →
  {W₁ : Type u_3} →
    {W₂ : Type u_4} →
      [inst : CategoryTheory.Category.{v_2, u_3} W₁] →
        [inst_1 : CategoryTheory.Category.{v_3, u_4} W₂] →
          [inst_2 : CategoryTheory.Limits.HasZeroMorphisms W₁] →
            [inst_3 : CategoryTheory.Limits.HasZeroMorphisms W₂] →
              (F : CategoryTheory.Functor W₁ W₂) →
                [F.PreservesZeroMorphisms] →
                  (c : ComplexShape ι) → CategoryTheory.Functor (HomologicalComplex W₁ c) (HomologicalComplex W₂ c)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.induce_eq_coe_induce_top : ∀ {V : Type u} {G : SimpleGraph V} (s : Set V), SimpleGraph.induce s G = (⊤.induce s).coe
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kronecker_add : ∀ {α : Type u_3} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [inst : Distrib α] (A : Matrix l m α)
  (B₁ B₂ : Matrix n p α),
  Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A (B₁ + B₂) =
    Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A B₁ + Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A B₂
-- Mathlib.Analysis.RCLike.ContinuousMap
ContinuousMap.range_realToRCLike_eq_isSelfAdjoint : ∀ (X : Type u_1) (𝕜 : Type u_2) [inst : TopologicalSpace X] [inst_1 : RCLike 𝕜],
  Set.range (ContinuousMap.realToRCLike 𝕜) = {f | IsSelfAdjoint f}
-- Mathlib.Algebra.GradedMonoid
/-- Build a `GMonoid` instance for a collection of subobjects.  -/
SetLike.gMonoid : {ι : Type u_1} →
  {R : Type u_2} →
    {S : Type u_3} →
      [inst : SetLike S R] →
        [inst_1 : Monoid R] →
          [inst_2 : AddMonoid ι] → (A : ι → S) → [SetLike.GradedMonoid A] → GradedMonoid.GMonoid fun i => ↥(A i)
-- Mathlib.Data.Nat.Factorization.Basic
Nat.sum_primeFactors_gcd_add_sum_primeFactors_mul : ∀ {β : Type u_1} [inst : AddCommMonoid β] (m n : ℕ) (f : ℕ → β),
  (m.gcd n).primeFactors.sum f + (m * n).primeFactors.sum f = m.primeFactors.sum f + n.primeFactors.sum f
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
Subgroup.isUniformGroup : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] (S : Subgroup α), IsUniformGroup ↥S
-- Mathlib.Data.Multiset.UnionInter
Multiset.map_set_pairwise : ∀ {α : Type u_1} {β : Type v} {f : α → β} {r : β → β → Prop} {m : Multiset α},
  ({a | a ∈ m}.Pairwise fun a₁ a₂ => r (f a₁) (f a₂)) → {b | b ∈ Multiset.map f m}.Pairwise r
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- If `f` is not meromorphic, conversion to normal form at `x` maps the function to `0`.  -/
toMeromorphicNFAt_of_not_meromorphicAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜}, ¬MeromorphicAt f x → toMeromorphicNFAt f x = 0
-- Mathlib.RingTheory.Localization.LocalizationLocalization
IsFractionRing.isFractionRing_of_isLocalization : ∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) (S : Type u_2) (T : Type u_3) [inst_1 : CommRing S]
  [inst_2 : CommRing T] [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T]
  [IsLocalization M S] [IsFractionRing R T], M ≤ nonZeroDivisors R → IsFractionRing S T
-- Mathlib.Topology.Order.WithTop
WithTop.sumHomeomorph.eq_1 : ∀ (ι : Type u_1) [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι] [inst_3 : OrderTop ι],
  WithTop.sumHomeomorph ι =
    { toFun := fun x => if h : x = ⊤ then Sum.inr () else Sum.inl x.untopA,
      invFun := fun x =>
        match x with
        | Sum.inl i => ↑i
        | Sum.inr PUnit.unit => ⊤,
      left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.Data.Set.Subsingleton
Set.Subsingleton.eq_empty_or_singleton : ∀ {α : Type u} {s : Set α}, s.Subsingleton → s = ∅ ∨ ∃ x, s = {x}
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.reverse_ι : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (m : M), CliffordAlgebra.reverse ((CliffordAlgebra.ι Q) m) = (CliffordAlgebra.ι Q) m
-- Mathlib.RingTheory.Ideal.Lattice
Ideal.eq_top_iff_one : ∀ {α : Type u} [inst : Semiring α] (I : Ideal α), I = ⊤ ↔ 1 ∈ I
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- The extra goals created by the rewrite  -/
Mathlib.Tactic.LibraryRewrite.RewriteInterface.extraGoals : Mathlib.Tactic.LibraryRewrite.RewriteInterface → Array Lean.Widget.CodeWithInfos
-- Init.Data.Iterators.Basic
/-- `IterStep.done` describes the situation that an iterator has finished and will neither emit
more values nor cause any monadic effects. In this case, no succeeding iterator is provided.
 -/
Std.IterStep.done : {α : Sort u_1} → {β : Sort u_2} → Std.IterStep α β
-- Std.Data.HashMap.Basic
/-- Creates a hash map from a list of mappings. If the same key appears multiple times, the last
occurrence takes precedence.  -/
Std.HashMap.ofList : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → List (α × β) → Std.HashMap α β
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β]
  {f g : CompactlySupportedContinuousMap α β}, f = g ↔ ∀ (x : α), f x = g x
-- Mathlib.Topology.Algebra.Monoid
/-- If multiplication is continuous in `α`, then it also is in `αᵐᵒᵖ`.  -/
MulOpposite.instContinuousMul : ∀ {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : Mul α] [ContinuousMul α], ContinuousMul αᵐᵒᵖ
-- Mathlib.Data.Set.Function
Set.RightInvOn.prodMap : ∀ {α₁ : Type u_7} {α₂ : Type u_8} {β₁ : Type u_9} {β₂ : Type u_10} {t₁ : Set β₁} {t₂ : Set β₂} {f₁ : α₁ → β₁}
  {f₂ : α₂ → β₂} {g₁ : β₁ → α₁} {g₂ : β₂ → α₂},
  Set.RightInvOn g₁ f₁ t₁ →
    Set.RightInvOn g₂ f₂ t₂ → Set.RightInvOn (fun x => (g₁ x.1, g₂ x.2)) (fun x => (f₁ x.1, f₂ x.2)) (t₁ ×ˢ t₂)
-- Std.Http.Internal.Char
/-- ctext = HTAB / SP / %x21-27 / %x2A-5B / %x5D-7E
; ASCII-only variant (no obs-text).
 -/
Std.Http.Internal.Char.ctext : Char → Bool
-- Mathlib.GroupTheory.Torsion
/-- `g` lies in the `p`-primary component iff `g ^ p ^ k = 1` for some `k`.  -/
CommGroup.mem_primaryComponent : ∀ {G : Type u_1} [inst : CommGroup G] {p : ℕ} {g : G}, g ∈ CommGroup.primaryComponent G p ↔ ∃ k, g ^ p ^ k = 1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey?_eq_some_minKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  (he : t ≠ ∅), t.minKey? = some (t.minKey he)
-- Mathlib.Data.List.Zip
List.instIsSymmOpZipWith : ∀ {α : Type u} {β : Type u_1} (f : α → α → β) [IsSymmOp f], IsSymmOp (List.zipWith f)
-- Mathlib.AlgebraicGeometry.Morphisms.FiniteType
AlgebraicGeometry.locallyOfFiniteType_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.LocallyOfFiniteType f ↔
    ∀ {U : Y.Opens},
      AlgebraicGeometry.IsAffineOpen U →
        ∀ {V : X.Opens},
          AlgebraicGeometry.IsAffineOpen V →
            ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
              (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).FiniteType
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- A structured arrow category on a `StructuredArrow.pre e F G` functor is equivalent to the
structured arrow category on F  -/
CategoryTheory.StructuredArrow.preEquivalence : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (F : CategoryTheory.Functor C D) →
              {G : CategoryTheory.Functor D E} →
                {e : E} →
                  (f : CategoryTheory.StructuredArrow e G) →
                    CategoryTheory.StructuredArrow f (CategoryTheory.StructuredArrow.pre e F G) ≌
                      CategoryTheory.StructuredArrow f.right F
-- Init.Data.UInt.Bitwise
UInt16.right_le_or : ∀ {a b : UInt16}, b ≤ a ||| b
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.Over.hasLimit_of_hasLimit_liftFromOver : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} (F : CategoryTheory.Functor J (CategoryTheory.Over X))
  [CategoryTheory.Limits.HasLimit (CategoryTheory.WithTerminal.liftFromOver.obj F)], CategoryTheory.Limits.HasLimit F
-- Init.Data.List.Control
List.filterAuxM : {m : Type → Type v} → [Monad m] → {α : Type} → (α → m Bool) → List α → List α → m (List α)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
/-- The `AddMonoidHom` from a profinite additive group `P` to the projective limit of
its quotients by open normal subgroups ordered by inclusion  -/
ProfiniteAddGrp.toLimitFun : (P : ProfiniteAddGrp.{u}) → ↑P.toProfinite.toTop →+ ↑(ProfiniteAddGrp.limit P.diagram).toProfinite.toTop
-- Mathlib.MeasureTheory.Group.Prod
/-- The map `(x, y) ↦ (x + y, y)` preserves the measure `μ × ν`.  -/
MeasureTheory.measurePreserving_add_prod : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [μ.IsAddRightInvariant],
  MeasureTheory.MeasurePreserving (fun z => (z.1 + z.2, z.2)) (μ.prod ν) (μ.prod ν)
-- Mathlib.Order.Std
Preorder.OfStdArgs.mk.sizeOf_spec : ∀ {α : Type u_1} [inst : SizeOf α] (le : autoParam (LE α) Preorder.OfStdArgs.le._autoParam)
  (lt :
    autoParam
      (let this := le;
      LT α)
      Preorder.OfStdArgs.lt._autoParam)
  (lawfulOrderLT :
    autoParam
      (let this := le;
      let this_1 := lt;
      Std.LawfulOrderLT α)
      Preorder.OfStdArgs.lawfulOrderLT._autoParam)
  (isPreorder :
    autoParam
      (let this := le;
      Std.IsPreorder α)
      Preorder.OfStdArgs.isPreorder._autoParam),
  sizeOf { le := le, lt := lt, lawfulOrderLT := lawfulOrderLT, isPreorder := isPreorder } =
    1 + sizeOf le + sizeOf lt + sizeOf lawfulOrderLT + sizeOf isPreorder
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.isBoundary₁_iff : ∀ {G : Type u_1} {A : Type u_2} [inst : Group G] [inst_1 : AddCommGroup A] [inst_2 : DistribMulAction G A] (x : G →₀ A),
  groupHomology.IsBoundary₁ x ↔
    ∃ y, (y.sum fun g a => ((fun₀ | g.2 => a) - fun₀ | g.1 * g.2 => g.1 • a) + fun₀ | g.1 => g.1 • a) = x
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.mem_of_mem_rcc : ∀ {α : Type u} [inst : LE α] {lo hi a : α}, (a ∈ lo...=hi) → a ∈ *...=hi
-- Lean.Data.JsonRpc
Lean.JsonRpc.MessageKind.ofMessage : Lean.JsonRpc.Message → Lean.JsonRpc.MessageKind
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.algEquiv_self : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f), h.algEquiv h = AlgEquiv.refl
-- Mathlib.Data.Finset.Image
Finset.map_erase : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : DecidableEq α] (f : α ↪ β) (s : Finset α) (a : α),
  Finset.map f (s.erase a) = (Finset.map f s).erase (f a)
-- Lean.Elab.ConfigEval.Basic
Lean.Elab.ConfigEval.ConfigItem.throwCannotSetOption : {α : Type} → Lean.Elab.ConfigEval.ConfigItem → Option Lean.Name → Lean.Elab.TermElabM α
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.setRed_toList : ∀ {α : Type u_1} {t : RBTree.RBNode α}, t.setRed.toList = t.toList
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- A non-unital star subalgebra is a non-unital subalgebra which is closed under the `star`
operation.  -/
NonUnitalStarSubalgebra : (R : Type u) →
  (A : Type v) → [inst : CommSemiring R] → [inst_1 : NonUnitalNonAssocSemiring A] → [Module R A] → [Star A] → Type v
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.exp_log_eq_abs : ∀ {x : ℝ}, x ≠ 0 → Real.exp (Real.log x) = |x|
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
/-- The measurable atom of a point in a countably generated measurable space is given by
a `countablyGeneratedAtom`.  -/
MeasurableSpace.measurableAtom_eq_countablyGeneratedAtom_natGeneratingSequence : ∀ {α : Type u_1} {mα : MeasurableSpace α} [inst : MeasurableSpace.CountablyGenerated α] (x : α),
  measurableAtom x = MeasurableSpace.countablyGeneratedAtom α fun x_1 => x ∈ MeasurableSpace.natGeneratingSequence α x_1
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- The actual `Subgroup` obtained from an element of a `SubgroupClass`  -/
Subgroup.ofClass : {S : Type u_3} → {G : Type u_4} → [inst : Group G] → [inst_1 : SetLike S G] → [SubgroupClass S G] → S → Subgroup G
-- Mathlib.Data.List.Nodup
/-- This is a variant of the `nodup_append` from the standard library,
which does not use `Disjoint`.  -/
List.nodup_append' : ∀ {α : Type u} {l₁ l₂ : List α}, (l₁ ++ l₂).Nodup ↔ l₁.Nodup ∧ l₂.Nodup ∧ l₁.Disjoint l₂
-- Mathlib.Algebra.Free
AddMagma.FreeAddSemigroup.quot_mk_assoc_left : ∀ {α : Type u} [inst : Add α] (x y z w : α),
  Quot.mk (AddMagma.AssocRel α) (x + (y + z + w)) = Quot.mk (AddMagma.AssocRel α) (x + (y + (z + w)))
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.denoteS.eq_5 : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (a b : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.Expr.denoteS ctx (a.mul b) =
    Lean.Grind.CommRing.Expr.denoteS ctx a * Lean.Grind.CommRing.Expr.denoteS ctx b
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Complex.cpow_inv_two_re : ∀ (x : ℂ), (x ^ 2⁻¹).re = √((‖x‖ + x.re) / 2)
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.smeval_C_mul_T_n : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid S] [inst_2 : SMulWithZero R S]
  [inst_3 : Monoid S] (x : Sˣ) (n : ℤ) (r : R), (LaurentPolynomial.C r * LaurentPolynomial.T n).smeval x = r • ↑(x ^ n)
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthSup_iSup : ∀ {ι : Type u_1} [Finite ι] (u : ι → ℕ → ENNReal), ExpGrowth.expGrowthSup (⨆ i, u i) = ⨆ i, ExpGrowth.expGrowthSup (u i)
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.Theorems.getOrigins : {α : Type} → Lean.Meta.Grind.Theorems α → List Lean.Meta.Grind.Origin
-- Mathlib.Algebra.Colimit.Module
AddCommGroup.DirectLimit.map_comp : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} [inst_1 : (i : ι) → AddCommMonoid (G i)]
  {f : (i j : ι) → i ≤ j → G i →+ G j} [inst_2 : DecidableEq ι] {G' : ι → Type u_5}
  [inst_3 : (i : ι) → AddCommMonoid (G' i)] {f' : (i j : ι) → i ≤ j → G' i →+ G' j} {G'' : ι → Type u_6}
  [inst_4 : (i : ι) → AddCommMonoid (G'' i)] {f'' : (i j : ι) → i ≤ j → G'' i →+ G'' j} (g₁ : (i : ι) → G i →+ G' i)
  (g₂ : (i : ι) → G' i →+ G'' i) (hg₁ : ∀ (i j : ι) (h : i ≤ j), (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i))
  (hg₂ : ∀ (i j : ι) (h : i ≤ j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)),
  (AddCommGroup.DirectLimit.map g₂ hg₂).comp (AddCommGroup.DirectLimit.map g₁ hg₁) =
    AddCommGroup.DirectLimit.map (fun i => (g₂ i).comp (g₁ i)) ⋯
-- Mathlib.Tactic.ExtractGoal
/-- Format a goal into a type signature for a declaration named `name`.

Example output: `myTheorem (a b : Nat) : a + b = b + a`.

The return values are:
* A formatted piece of `MessageData`, like `m!"myTheorem (a b : Nat) : a + b = b + a"`.
* The full type of the declaration, like `∀ a b, a + b = b + a`.
* The imports needed to state this declaration, as an array of module names.
* A boolean indicating whether the original goal type had top-level foralls.
 -/
Mathlib.Tactic.ExtractGoal.goalSignature : Lean.Name → Lean.MVarId → Lean.Elab.TermElabM (Lean.MessageData × Lean.Expr × Array Lean.Name × Bool)
-- Std.Sync.Channel
Std.CloseableChannel.instAsyncReadOptionOfInhabited : {α : Type} → [Inhabited α] → Std.Async.IO.AsyncRead (Std.CloseableChannel α) (Option α)
-- Mathlib.RingTheory.Ideal.Maps
RingHom.ker_eq_bot_iff_eq_zero : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Ring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S]
  [rc : RingHomClass F R S] (f : F), RingHom.ker f = ⊥ ↔ ∀ (x : R), f x = 0 → x = 0
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
DirichletCharacter.gammaFactor.eq_1 : ∀ {N : ℕ} (χ : DirichletCharacter ℂ N) (s : ℂ), χ.gammaFactor s = if χ.Even then s.Gammaℝ else (s + 1).Gammaℝ
-- Mathlib.Analysis.Analytic.CPolynomial
ContinuousMultilinearMap.cpolynomialAt_uncurry_compContinuousLinearMap : ∀ {𝕜 : Type u_1} {G : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] {ι : Type u_5} {Em : ι → Type u_6} {Fm : ι → Type u_7}
  [inst_3 : (i : ι) → NormedAddCommGroup (Em i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (Em i)]
  [inst_5 : (i : ι) → NormedAddCommGroup (Fm i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (Fm i)] [inst_7 : Fintype ι]
  {q : ((i : ι) → Fm i →L[𝕜] Em i) × ContinuousMultilinearMap 𝕜 Em G},
  CPolynomialAt 𝕜 (fun p => p.2.compContinuousLinearMap p.1) q
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (J : Type) [Finite J]
  [CategoryTheory.Limits.HasFiniteWidePushouts C],
  CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Limits.WidePushoutShape J) C
-- Mathlib.Algebra.Group.Submonoid.MulAction
Submonoid.smul : {M' : Type u_1} → {α : Type u_2} → [inst : MulOneClass M'] → [SMul M' α] → (S : Submonoid M') → SMul (↥S) α
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- Given binary fans `sXY` over `X Y`, and `sYZ` over `Y Z`, and `s` over `sXY.X Z`,
if `sYZ` is a limit cone we can construct a binary fan over `X sYZ.X`.

This is an ingredient of building the associator for a Cartesian category.  -/
CategoryTheory.Limits.BinaryFan.assoc : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {sXY : CategoryTheory.Limits.BinaryFan X Y} →
        {sYZ : CategoryTheory.Limits.BinaryFan Y Z} →
          CategoryTheory.Limits.IsLimit sYZ →
            CategoryTheory.Limits.BinaryFan sXY.pt Z → CategoryTheory.Limits.BinaryFan X sYZ.pt
-- Init.Data.Vector.Lemmas
Vector.replace_cast : ∀ {α : Type u_1} [inst : BEq α] {n m : ℕ} {h : n = m} {xs : Vector α n} {a b : α},
  (Vector.cast h xs).replace a b = Vector.cast ⋯ (xs.replace a b)
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.ValidFor.remainingBytes : ∀ {l r : List Char} {it : String.Legacy.Iterator},
  String.Legacy.Iterator.ValidFor l r it → it.remainingBytes = String.utf8Len r
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f] {Z : AlgebraicGeometry.SheafedSpace C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict f).inv
      (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp (Y.ofRestrict ⋯) h
-- Mathlib.Data.Nat.Factorization.Basic
Nat.factorizationEquiv_inv_apply : ∀ {f : ℕ →₀ ℕ} (hf : ∀ p ∈ f.support, Nat.Prime p), ↑(Nat.factorizationEquiv.symm ⟨f, hf⟩) = f.prod fun x1 x2 => x1 ^ x2
-- Init.System.IO
/-- File metadata.

The metadata for a file can be accessed with `System.FilePath.metadata`/
`System.FilePath.symlinkMetadata`.
 -/
IO.FS.Metadata : Type
-- Std.Data.Iterators.Lemmas.Consumers.Set
Std.Iter.toExtHashSet_eq_ofList : ∀ {α β : Type w} {x : BEq β} {x_1 : Hashable β} [inst : EquivBEq β] [inst_1 : LawfulHashable β]
  [inst_2 : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_4 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β}, it.toExtHashSet = Std.ExtHashSet.ofList it.toList
-- Mathlib.Analysis.Distribution.TestFunction
/-- The **universal property** of the topology on `𝓓^{n}(Ω, F)`: a **linear** map from
`𝓓^{n}(Ω, F)` to a locally convex topological vector space is continuous if and only if its
precomposition with the inclusion `ofSupportedIn K_sub_Ω : 𝓓^{n}_{K}(E, F) → 𝓓^{n}(Ω, F)` is
continuous for every compact `K ⊆ Ω`.  -/
TestFunction.continuous_iff_continuous_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F] {n : ℕ∞} {V : Type u_6} [inst_6 : AddCommGroup V]
  [inst_7 : Module ℝ V] [t : TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul ℝ V] [LocallyConvexSpace ℝ V]
  [inst_11 : Algebra ℝ 𝕜] [inst_12 : IsScalarTower ℝ 𝕜 F] [inst_13 : Module 𝕜 V] [IsScalarTower ℝ 𝕜 V]
  (f : TestFunction Ω F n →ₗ[𝕜] V),
  Continuous ⇑f ↔
    ∀ (K : TopologicalSpace.Compacts E) (K_sub_Ω : ↑K ⊆ ↑Ω), Continuous (⇑f ∘ TestFunction.ofSupportedIn K_sub_Ω)
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.PhaseName.elab : Lean.Syntax → Aesop.ElabM Aesop.PhaseName
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.get.match_1.splitter : {α : Type u_2} →
  {β : Type u_1} →
    [inst : BEq α] →
      (a : α) →
        (motive :
            (x : Std.DHashMap.Internal.AssocList α fun x => β) →
              Std.DHashMap.Internal.AssocList.contains a x = true → Sort u_3) →
          (x : Std.DHashMap.Internal.AssocList α fun x => β) →
            (x_1 : Std.DHashMap.Internal.AssocList.contains a x = true) →
              ((k : α) →
                  (v : β) →
                    (es : Std.DHashMap.Internal.AssocList α fun x => β) →
                      (h :
                          Std.DHashMap.Internal.AssocList.contains a (Std.DHashMap.Internal.AssocList.cons k v es) =
                            true) →
                        motive (Std.DHashMap.Internal.AssocList.cons k v es) h) →
                motive x x_1
-- Mathlib.Geometry.Convex.ConvexSpace.Module
/-- Eta-expanded form of `Convexity.IsAffineMap.add` -/
Convexity.IsAffineMap.fun_add : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : AddCommMonoid N]
  [inst_6 : Module R N] {f g : M → N} [inst_7 : Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M]
  [inst_9 : Convexity.ConvexSpace R N] [Convexity.IsModuleConvexSpace R N],
  Convexity.IsAffineMap R f → Convexity.IsAffineMap R g → Convexity.IsAffineMap R fun i => f i + g i
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
Filter.EventuallyEq.lineDifferentiableAt_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f₀ f₁ : E → F}
  {x v : E}, f₀ =ᶠ[nhds x] f₁ → (LineDifferentiableAt 𝕜 f₀ x v ↔ LineDifferentiableAt 𝕜 f₁ x v)
-- Mathlib.CategoryTheory.Sites.MorphismProperty
CategoryTheory.Precoverage.morphismProperty_sup : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {K L : CategoryTheory.Precoverage C},
  (K ⊔ L).morphismProperty = K.morphismProperty ⊔ L.morphismProperty
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.add.inj : ∀ {k : ℤ} {v : Lean.Grind.CommRing.Mon} {p : Lean.Grind.CommRing.Poly} {k_1 : ℤ} {v_1 : Lean.Grind.CommRing.Mon}
  {p_1 : Lean.Grind.CommRing.Poly},
  Lean.Grind.CommRing.Poly.add k v p = Lean.Grind.CommRing.Poly.add k_1 v_1 p_1 → k = k_1 ∧ v = v_1 ∧ p = p_1
-- Mathlib.Tactic.CategoryTheory.BicategoryCoherence
/-- A typeclass carrying a choice of lift of a 2-morphism from `B` to `FreeBicategory B`.  -/
Mathlib.Tactic.BicategoryCoherence.LiftHom₂ : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      {f g : a ⟶ b} →
        [Mathlib.Tactic.BicategoryCoherence.LiftHom f] →
          [Mathlib.Tactic.BicategoryCoherence.LiftHom g] → (f ⟶ g) → Type (max u v)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_pi : Real.sin Real.pi = 0