mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.FunctorialFactorizationData.fac_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  (data : W₁.FunctorialFactorizationData W₂) {f : CategoryTheory.Arrow C} {Z : C}
  (h : CategoryTheory.Arrow.rightFunc.obj f ⟶ Z),
  CategoryTheory.CategoryStruct.comp (data.i.app f) (CategoryTheory.CategoryStruct.comp (data.p.app f) h) =
    CategoryTheory.CategoryStruct.comp f.hom h
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.snd_toProd : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N] (x : Monoid.Coprod M N),
  (Monoid.Coprod.toProd x).2 = Monoid.Coprod.snd x
-- Mathlib.Algebra.Group.Subgroup.Defs
SubgroupClass.toSubmonoidClass : ∀ {S : Type u_3} {G : outParam (Type u_4)} {inst : DivInvMonoid G} {inst_1 : SetLike S G} [self : SubgroupClass S G],
  SubmonoidClass S G
-- Std.Do.WP.Basic
/-- `wp⟦x⟧ Q` is defined as `(WP.wp x).apply Q`.  -/
Std.Do.«termWp⟦_:_⟧» : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_union!_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k fallback : α},
        Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.union! m₂).getKeyD k fallback = m₁.getKeyD k fallback
-- Std.Data.Iterators.Combinators.Monadic.TakeWhile
Std.Iterators.Types.TakeWhile.instFinite : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Monad m] [inst_1 : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)},
  Std.Iterators.Finite (Std.Iterators.Types.TakeWhile α m β P) m
-- Mathlib.Order.Antichain
/-- A function `a` is strongly less than a function `b` if `a i < b i` for all `i`.  -/
_private.Mathlib.Order.Antichain.0.«term_≺_» : Lean.TrailingParserDescr
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.iUnion_ofWithBot : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (boxes : Finset (WithBot (BoxIntegral.Box ι)))
  (le_of_mem : ∀ J ∈ boxes, J ≤ ↑I) (pairwise_disjoint : (↑boxes).Pairwise Disjoint),
  (BoxIntegral.Prepartition.ofWithBot boxes le_of_mem pairwise_disjoint).iUnion = ⋃ J ∈ boxes, ↑J
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsTrail.isPath_iff_isSubwalk_imp_not_isCycle : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v},
  p.IsTrail → (p.IsPath ↔ ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → ¬w.IsCycle)
-- Mathlib.MeasureTheory.Measure.OpenPos
MeasureTheory.Measure.eqOn_Icc_of_ae_eq : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : LinearOrder X] [OrderTopology X]
  {m : MeasurableSpace X} [inst_3 : TopologicalSpace Y] [T2Space Y] (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure]
  [DenselyOrdered X] {a b : X},
  a ≠ b →
    ∀ {f g : X → Y},
      f =ᵐ[μ.restrict (Set.Icc a b)] g →
        ContinuousOn f (Set.Icc a b) → ContinuousOn g (Set.Icc a b) → Set.EqOn f g (Set.Icc a b)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.div_certC : Lean.Grind.CommRing.Poly → ℤ → Lean.Grind.CommRing.Poly → ℕ → Bool
-- Mathlib.Topology.Algebra.Group.Units
/-- If a submonoid is open in a topological additive monoid,
then its additive units form an open subset of the additive units of the monoid.  -/
AddSubmonoid.isOpen_addUnits : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : AddMonoid M] {U : AddSubmonoid M}, IsOpen ↑U → IsOpen ↑U.addUnits
-- Mathlib.FieldTheory.IsAlgClosed.Classification
/-- If `K` is an uncountable algebraically closed field, then its
cardinality is the same as that of a transcendence basis.

This is a simpler, but less general statement of
`cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt`.  -/
IsAlgClosed.cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt' : ∀ {R : Type u} [inst : CommRing R] {K' : Type u} [inst_1 : Field K'] [inst_2 : Algebra R K'] [IsAlgClosed K']
  {ι' : Type u} (v' : ι' → K') [Nontrivial R],
  IsTranscendenceBasis R v' →
    Cardinal.mk R ≤ Cardinal.aleph0 → Cardinal.aleph0 < Cardinal.mk K' → Cardinal.mk K' = Cardinal.mk ι'
-- Init.Data.BitVec.Basic
/-- Converts a list of `Bool`s into a big-endian `BitVec`.  -/
BitVec.ofBoolListBE : (bs : List Bool) → BitVec bs.length
-- Lean.Data.NameMap.Basic
Lean.MacroScopesView.isPrefixOf : Lean.MacroScopesView → Lean.MacroScopesView → Bool
-- Mathlib.SetTheory.ZFC.Ordinal
ZFSet.IsOrdinal.subset_iff_eq_or_mem : ∀ {x y : ZFSet.{u}}, x.IsOrdinal → y.IsOrdinal → (x ⊆ y ↔ x = y ∨ x ∈ y)
-- Init.Data.Array.BasicAux
_private.Init.Data.Array.BasicAux.0.Array.mapM'.go.eq_def : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : α → m β) (as : Array α) (i : ℕ)
  (acc : { bs // bs.size = i }) (hle : i ≤ as.size),
  Array.mapM'.go✝ f as i acc hle =
    if h : i = as.size then pure (h ▸ acc)
    else
      have hlt := ⋯;
      do
      let b ← f as[i]
      Array.mapM'.go✝ f as (i + 1) ⟨(↑acc).push b, ⋯⟩ hlt
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- The isomorphism `F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y)` when `F` is a monoidal functor.  -/
CategoryTheory.Functor.Monoidal.μIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            (F : CategoryTheory.Functor C D) →
              [F.Monoidal] →
                (X Y : C) →
                  CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ≅
                    F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
ApproximatesLinearOn.surjective : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E ≃L[𝕜] F} {c : NNReal} [CompleteSpace E],
  ApproximatesLinearOn f (↑f') Set.univ c → Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹ → Function.Surjective f
-- Mathlib.SetTheory.Cardinal.Free
instCountableFreeMonoid : ∀ (α : Type u) [Countable α], Countable (FreeMonoid α)
-- Aesop.Saturate
_private.Aesop.Saturate.0.Aesop.saturateCore.runRule : {α : Type} →
  Lean.MVarId →
    Aesop.UnorderedArraySet Lean.MVarId →
      Lean.Meta.SavedState →
        Aesop.IndexMatchResult (Aesop.Rule α) →
          Aesop.SaturateM (Option (Aesop.GoalDiff × Option (Array Aesop.Script.LazyStep)))
-- Mathlib.Data.Fin.SuccPred
Fin.castSucc_ne_zero_of_lt : ∀ {n : ℕ} {p i : Fin n}, p < i → i.castSucc ≠ 0
-- Init.Data.Array.Lemmas
Array.append_eq_append_iff_of_size_eq_right : ∀ {α : Type u_1} {ws xs ys zs : Array α}, ys.size = zs.size → (ws ++ ys = xs ++ zs ↔ ws = xs ∧ ys = zs)
-- Init.Grind.Order
Lean.Grind.Order.lt_eq_false_of_lt : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] {a b : α},
  a < b → (b < a) = False
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_minKey! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → t.isEmpty = false → ∀ {fallback : α}, t.getKeyD t.minKey! fallback = t.minKey!
-- Lean.Data.NameTrie
Lean.NameTrie : Type u → Type u
-- Mathlib.Analysis.InnerProductSpace.OfNorm
InnerProductSpaceable.inner_.conj_symm : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] (x y : E),
  (starRingEnd 𝕜) (inner_✝ 𝕜 y x) = inner_✝ 𝕜 x y
-- Mathlib.Combinatorics.Graph.Basic
Graph.IsLoopAt.eq_of_inc : ∀ {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β}, G.IsLoopAt e x → G.Inc e y → x = y
-- Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
_private.Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence.0.Mathlib.Tactic.Bicategory.«term_▷_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Action.Monoidal
Action.FunctorCategoryEquivalence.functor_μ : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.MonoidalCategory V] (A B : Action V G),
  CategoryTheory.Functor.LaxMonoidal.μ Action.FunctorCategoryEquivalence.functor A B =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.MonoidalCategoryStruct.tensorObj (Action.FunctorCategoryEquivalence.functor.obj A)
        (Action.FunctorCategoryEquivalence.functor.obj B))
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.Hom.mk.sizeOf_spec : ∀ {R : Type u} [inst : CommRing R] {A B : CommHopfAlgCat R} [inst_1 : SizeOf R] (hom' : ↑A →ₐc[R] ↑B),
  sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Batteries.Data.Array.Match
Array.PrefixTable.mk : {α : Type u_1} → (toArray : Array (α × ℕ)) → (∀ {i : ℕ} (h : i < toArray.size), toArray[i].2 ≤ i) → Array.PrefixTable α
-- Mathlib.Combinatorics.SetFamily.Compression.UV
/-- `a` is in the UV-compressed family iff it's in the original and its compression is in the
original, or it's not in the original but it's the compression of something in the original.  -/
UV.mem_compression : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableRel Disjoint] [inst_2 : DecidableLE α]
  {s : Finset α} {u v a : α} [inst_3 : DecidableEq α],
  a ∈ UV.compression u v s ↔ a ∈ s ∧ UV.compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, UV.compress u v b = a
-- Mathlib.Analysis.RCLike.Sqrt
RCLike.sqrt_of_nonneg : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {a : 𝕜}, 0 ≤ a → RCLike.sqrt a = ↑√(RCLike.re a)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.RenameParams.toTextDocumentPositionParams : Lean.Lsp.RenameParams → Lean.Lsp.TextDocumentPositionParams
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelpParams.toTextDocumentPositionParams : Lean.Lsp.SignatureHelpParams → Lean.Lsp.TextDocumentPositionParams
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.instAddGroup : {σ : Type u_1} → {R : Type u_2} → [AddGroup R] → AddGroup (MvPowerSeries σ R)
-- Mathlib.Algebra.Order.Antidiag.Prod
Finset.HasAntidiagonal.swap_mem_antidiagonal : ∀ {A : Type u_1} [inst : AddCommMonoid A] [inst_1 : Finset.HasAntidiagonal A] {n : A} {xy : A × A},
  xy.swap ∈ Finset.HasAntidiagonal.antidiagonal n ↔ xy ∈ Finset.HasAntidiagonal.antidiagonal n
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.map_target : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y)
  {x : Y}, x ∈ e.target → ↑e.symm x ∈ e.source
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.snd_univ : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {ρ : MeasureTheory.Measure (α × β)}, ρ.snd Set.univ = ρ Set.univ
-- Init.Data.String.Basic
String.Slice.Pos.offset_cast : ∀ {s t : String.Slice} {pos : s.Pos} {h : s.copy = t.copy}, (pos.cast h).offset = pos.offset
-- Mathlib.FieldTheory.Finite.Basic
/-- The **Fermat-Euler totient theorem**. `Nat.ModEq.pow_totient` is an alternative statement
of the same theorem.  -/
ZMod.pow_totient : ∀ {n : ℕ} (x : (ZMod n)ˣ), x ^ n.totient = 1
-- Mathlib.Tactic.Convert
_private.Mathlib.Tactic.Convert.0.instEvalExprCheapConfig : Lean.Elab.ConfigEval.EvalExpr Convert.CheapConfig
-- Lean.Exception
Lean.MonadRecDepth.getMaxRecDepth : {m : Type → Type} → [self : Lean.MonadRecDepth m] → m ℕ
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.mapShortComplexH2.eq_1 : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u_1, u, u} k H}
  {B : Rep.{u_1, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B),
  groupCohomology.mapShortComplexH2 f φ =
    { τ₁ := groupCohomology.cochainsMap₁ f φ, τ₂ := groupCohomology.cochainsMap₂ f φ,
      τ₃ := groupCohomology.cochainsMap₃ f φ, comm₁₂ := ⋯, comm₂₃ := ⋯ }
-- Mathlib.Logic.Encodable.Basic
IsEmpty.toEncodable : {α : Type u_1} → [IsEmpty α] → Encodable α
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
/-- The image of a monomial under `esymmAlgHom`.  -/
MvPolynomial.esymmAlgHomMonomial : (σ : Type u_1) → {R : Type u_3} → {n : ℕ} → [inst : CommSemiring R] → [Fintype σ] → (Fin n →₀ ℕ) → R → MvPolynomial σ R
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_filter_eq_size_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool},
  (Std.ExtDTreeMap.filter f t).size = t.size ↔ ∀ (k : α) (h : k ∈ t), f k (t.get k h) = true
-- Mathlib.Topology.EMetricSpace.Diam
/-- **Alias** of `Metric.ediam_le_iff`. -/
EMetric.diam_le_iff : ∀ {X : Type u_2} {s : Set X} [inst : PseudoEMetricSpace X] {d : ENNReal},
  Metric.ediam s ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d
-- Mathlib.Order.Interval.Set.Monotone
MonotoneOn.Ici : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  MonotoneOn f s → AntitoneOn (fun x => Set.Ici (f x)) s
-- Init.Data.Ord.UInt
UInt16.instLawfulEqOrd : Std.LawfulEqOrd UInt16
-- Mathlib.Algebra.Lie.Abelian
lie_eq_self_of_isAtom_of_ne_bot : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] {N : LieSubmodule R L M}
  {I : LieIdeal R L}, IsAtom N → ⁅I, N⁆ ≠ ⊥ → ⁅I, N⁆ = N
-- Lean.Meta.Match.MatcherApp.Basic
Lean.Meta.MatcherApp.params : Lean.Meta.MatcherApp → Array Lean.Expr
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.map_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β → γ) (f : α → β),
  FreeAddMonoid.map (g ∘ f) = (FreeAddMonoid.map g).comp (FreeAddMonoid.map f)
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.functorProdToProdFunctor_map : ∀ (A : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  (C : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {X Y : CategoryTheory.Functor A (B × C)} (α : X ⟶ Y),
  (CategoryTheory.functorProdToProdFunctor A B C).map α =
    CategoryTheory.Prod.mkHom (CategoryTheory.Functor.whiskerRight α (CategoryTheory.Prod.fst B C))
      (CategoryTheory.Functor.whiskerRight α (CategoryTheory.Prod.snd B C))
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.volume_preserving_funUnique : ∀ (α : Type u) (β : Type v) [inst : Unique α] [inst_1 : MeasureTheory.MeasureSpace β],
  MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.funUnique α β)) MeasureTheory.volume MeasureTheory.volume
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.arrows_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {R S : CategoryTheory.Sieve X},
  R.arrows = S.arrows → R = S
-- Mathlib.Order.Cofinal
GaloisConnection.map_isCofinal : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : β → α} {g : α → β},
  GaloisConnection f g → ∀ {s : Set α}, IsCofinal s → IsCofinal (g '' s)
-- Mathlib.Computability.AkraBazzi.AkraBazzi
_private.Mathlib.Computability.AkraBazzi.AkraBazzi.0.AkraBazziRecurrence.termε : Lean.ParserDescr
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.IsHomogeneous.finSuccEquiv_coeff_isHomogeneous : ∀ {R : Type u_3} [inst : CommSemiring R] {N : ℕ} {φ : MvPolynomial (Fin (N + 1)) R} {n : ℕ},
  φ.IsHomogeneous n → ∀ (i j : ℕ), i + j = n → (((MvPolynomial.finSuccEquiv R N) φ).coeff i).IsHomogeneous j
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.instContinuousSMul : ∀ {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F], ContinuousSMul 𝕜 (SchwartzMap E F)
-- Std.Http.Protocol.H1
/-- Whether a forced flush has been requested by the user.
 -/
Std.Http.Protocol.H1.Machine.forcedFlush : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Bool
-- Init.Data.Int.DivMod.Lemmas
Int.bmod_eq_neg : ∀ {n : ℕ} {m : ℤ}, 0 ≤ m → ↑n = 2 * m → m.bmod n = -m
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- The cofork obtained by precomposing a coequalizer cofork with an epimorphism is
a coequalizer.  -/
CategoryTheory.Limits.isCoequalizerEpiComp : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} →
        {c : CategoryTheory.Limits.Cofork f g} →
          CategoryTheory.Limits.IsColimit c →
            {W : C} →
              (h : W ⟶ X) →
                [hm : CategoryTheory.Epi h] →
                  have this := ⋯;
                  CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ c.π this)
-- Lean.Meta.Tactic.Grind.Types
/-- A helper function used to mark a theorem instance found by the E-matching module.
It returns `true` if it is a new instance and `false` otherwise.
 -/
Lean.Meta.Grind.markTheoremInstance : Lean.Expr → Array Lean.Expr → Lean.Meta.Grind.GoalM Bool
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_ofNat : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (n : ℕ)
  [inst_4 : n.AtLeastTwo], ⌈OfNat.ofNat n⌉ = OfNat.ofNat n
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
/-- The functor `F.DescentData f ⥤ F.DescentData f` corresponding to `pullFunctor`
applied to identity morphisms is isomorphic to the identity functor.  -/
CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso : {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} →
              CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯ ≅ CategoryTheory.Functor.id (F.DescentData f)
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_prodMk₀ : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : ι → Type u_8}
  {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ)) →
      ∀ (i j k : ι), i ≠ k → j ≠ k → ProbabilityTheory.Kernel.IndepFun (fun a => (f i a, f j a)) (f k) κ μ
-- Mathlib.MeasureTheory.Measure.Map
/-- Lift a linear map between `OuterMeasure` spaces such that for each measure `μ` every measurable
set is Carathéodory-measurable w.r.t. `f μ` to a linear map between `Measure` spaces.  -/
MeasureTheory.Measure.liftLinear : {α : Type u_1} →
  {β : Type u_2} →
    {mα : MeasurableSpace α} →
      [inst : MeasurableSpace β] →
        (f : MeasureTheory.OuterMeasure α →ₗ[ENNReal] MeasureTheory.OuterMeasure β) →
          (∀ (μ : MeasureTheory.Measure α), inst ≤ (f μ.toOuterMeasure).caratheodory) →
            MeasureTheory.Measure α →ₗ[ENNReal] MeasureTheory.Measure β
-- Mathlib.Tactic.Basic
/-- Result of `withResetServerInfo`.  -/
Mathlib.Tactic.withResetServerInfo.Result : Type → Type
-- Mathlib.Order.Partition.Equipartition
Finpartition.isEquipartition_iff_card_parts_eq_average : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (P : Finpartition s),
  P.IsEquipartition ↔ ∀ a ∈ P.parts, a.card = s.card / P.parts.card ∨ a.card = s.card / P.parts.card + 1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.contains_insert : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a k : α} {v : β k}, (m.insert k v).contains a = (k == a || m.contains a)
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.instSemilatticeInf : {R : Type u_2} →
  {M : Type u_3} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : TopologicalSpace M] → [inst_3 : Module R M] → SemilatticeInf (ClosedSubmodule R M)
-- Lean.Elab.Command
Lean.Elab.Command.instInhabitedCommandElabM : {α : Type} → Inhabited (Lean.Elab.Command.CommandElabM α)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.Hom.naturality_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M₁ M₂ : PresheafOfModules R} (self : M₁.Hom M₂) {X Y : Cᵒᵖ} (f : X ⟶ Y) {Z : ModuleCat ↑(R.obj X)}
  (h : (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M₂.obj Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (M₁.map f)
      (CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (self.app Y))
        h) =
    CategoryTheory.CategoryStruct.comp (self.app X) (CategoryTheory.CategoryStruct.comp (M₂.map f) h)
-- Mathlib.Algebra.Group.Subgroup.Pointwise
AddSubgroup.toAddSubmonoid_zmultiples : ∀ {G : Type u_2} [inst : AddGroup G] (g : G),
  (AddSubgroup.zmultiples g).toAddSubmonoid = AddSubmonoid.multiples g ⊔ AddSubmonoid.multiples (-g)
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
/-- A slight strengthening of `exists_nontrivial_relation_sum_zero_of_rank_succ_lt_card`
available when working over an ordered field:
we can ensure a positive coefficient, not just a nonzero coefficient.
 -/
FiniteDimensional.exists_relation_sum_zero_pos_coefficient_of_finrank_succ_lt_card : ∀ {L : Type u_1} [inst : Field L] [inst_1 : LinearOrder L] [IsStrictOrderedRing L] {W : Type v}
  [inst_3 : AddCommGroup W] [inst_4 : Module L W] [FiniteDimensional L W] {t : Finset W},
  Module.finrank L W + 1 < t.card → ∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, 0 < f x
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.MonoFactorisation.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X Y : C} {f : X ⟶ Y} {I : C} {m : I ⟶ Y}
  {m_mono : CategoryTheory.Mono m} {e : X ⟶ I}
  {fac : autoParam (CategoryTheory.CategoryStruct.comp e m = f) CategoryTheory.Limits.MonoFactorisation.fac._autoParam}
  {I_1 : C} {m_1 : I_1 ⟶ Y} {m_mono_1 : CategoryTheory.Mono m_1} {e_1 : X ⟶ I_1}
  {fac_1 :
    autoParam (CategoryTheory.CategoryStruct.comp e_1 m_1 = f) CategoryTheory.Limits.MonoFactorisation.fac._autoParam},
  { I := I, m := m, m_mono := m_mono, e := e, fac := fac } =
      { I := I_1, m := m_1, m_mono := m_mono_1, e := e_1, fac := fac_1 } →
    I = I_1 ∧ m ≍ m_1 ∧ e ≍ e_1
-- Lean.Meta.Tactic.Grind.Split
/-- Given `e` of the form `a ∨ b`, check whether we are ready to case-split on `e`.
That is, `e` is `True`, but neither `a` nor `b` is `True`."
 -/
_private.Lean.Meta.Tactic.Grind.Split.0.Lean.Meta.Grind.checkDisjunctStatus : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Lean.Meta.Grind.SplitStatus
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.contains_alter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β},
  m.WF →
    (Std.DHashMap.Raw.Const.alter m k f).contains k' =
      if (k == k') = true then (f (Std.DHashMap.Raw.Const.get? m k)).isSome else m.contains k'
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.instBEqPolyCnstr.beq.eq_def : ∀ (x x_1 : Nat.Internal.Linear.PolyCnstr),
  Nat.Internal.Linear.instBEqPolyCnstr.beq x x_1 =
    match x, x_1 with
    | { eq := a, lhs := a_1, rhs := a_2 }, { eq := b, lhs := b_1, rhs := b_2 } => a == b && (a_1 == b_1 && a_2 == b_2)
    | x, x_2 => false
-- Mathlib.Computability.Primrec.Basic
Primrec.option_orElse : ∀ {α : Type u_1} [inst : Primcodable α], Primrec₂ fun x1 x2 => x1 <|> x2
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.natDegree_ΨSq_pos : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [NoZeroDivisors R] {n : ℤ},
  1 < n.natAbs → ↑n ≠ 0 → 0 < (W.ΨSq n).natDegree
-- Lean.Meta.MethodSpecs
/-- Whether the specs should be public or private  -/
Lean.MethodSpecsAttrData.privateSpecs : Lean.MethodSpecsAttrData → Bool
-- Lean.MetavarContext
/-- Update the type of the given metavariable. This function assumes the new type is
definitionally equal to the current one  -/
Lean.MetavarContext.setMVarType : Lean.MetavarContext → Lean.MVarId → Lean.Expr → Lean.MetavarContext