mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.nonempty_out : ∀ {x : Cardinal.{u_1}}, x ≠ 0 → Nonempty (Quotient.out x)
-- Init.Data.Fin.Lemmas
/-- An induction principle for `Fin` that considers a given `i : Fin n` as given by a sequence of `i`
applications of `Fin.succ`.

The cases in the induction are:
 * `zero` demonstrates the motive for `(0 : Fin (n + 1))` for all bounds `n`
 * `succ` demonstrates the motive for `Fin.succ` applied to an arbitrary `Fin` for an arbitrary
   bound `n`

Unlike `Fin.induction`, the motive quantifies over the bound, and the bound varies at each inductive
step. `Fin.succRecOn` is a version of this induction principle that takes the `Fin` argument first.
 -/
Fin.succRec : {motive : (n : ℕ) → Fin n → Sort u_1} →
  ((n : ℕ) → motive n.succ 0) →
    ((n : ℕ) → (i : Fin n) → motive n i → motive n.succ i.succ) → {n : ℕ} → (i : Fin n) → motive n i
-- Batteries.Data.UInt
UInt16.compare_eq_toNat_compare_toNat : ∀ (x y : UInt16), compare x y = compare x.toNat y.toNat
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.toContinuousLinearEquiv_mul : ∀ {R : Type u_1} {E : Type u_5} [inst : Semiring R] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module R E]
  (e e' : E ≃ₗᵢ[R] E), ↑(e * e') = ↑e * ↑e'
-- Mathlib.RingTheory.PiTensorProduct
PiTensorProduct.instRing : {ι : Type u_1} →
  {R : Type u_3} →
    {A : ι → Type u_4} →
      [inst : CommRing R] →
        [inst_1 : (i : ι) → Ring (A i)] → [inst_2 : (i : ι) → Algebra R (A i)] → Ring (PiTensorProduct R fun i => A i)
-- Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
/-- Given a function which is linear in the first argument
and is alternating in the other `n` arguments,
build an alternating form in `n + 1` arguments.

The function is given by
```
alternatizeUncurryFin f v = ∑ i : Fin (n + 1), (-1) ^ (i : ℕ) • f (v i) (removeNth i v)
```

Note that the round-trip with `curryFin` multiplies the form by `n + 1`,
since we want to avoid division in this definition.  -/
AlternatingMap.alternatizeUncurryFin : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : AddCommGroup N] →
            [inst_3 : Module R M] →
              [inst_4 : Module R N] → {n : ℕ} → (M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) → M [⋀^Fin (n + 1)]→ₗ[R] N
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.type_lt_mem_range_succ_iff : ∀ {α : Type u} [inst : LinearOrder α] [inst_1 : WellFoundedLT α],
  (Ordinal.type fun x1 x2 => x1 < x2) ∈ Set.range Order.succ ↔ ∃ x, IsMax x
-- Lean.Parser.Term
Lean.Parser.Term.structInstFieldDef.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.BitVec.Bitblast
BitVec.msb_smod : ∀ {w : ℕ} {x y : BitVec w},
  (decide ((x.smod y).msb = (x.msb && decide (y = 0))) || y.msb && decide (x.smod y ≠ 0)) = true
-- Mathlib.FieldTheory.Galois.Basic
/-- Let `E` be an intermediateField of a Galois extension `L / K`. If `E / K` is
Galois extension, then `E.fixingSubgroup` is a normal subgroup of `Gal(L / K)`.  -/
IsGalois.fixingSubgroup_normal_of_isGalois : ∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (E : IntermediateField K L)
  [IsGalois K L] [IsGalois K ↥E], E.fixingSubgroup.Normal
-- Mathlib.CategoryTheory.Subfunctor.Sieves
CategoryTheory.Subfunctor.family_of_elements_compatible : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)}
  (G : CategoryTheory.Subfunctor F) {U : Cᵒᵖ} (s : F.obj U), (G.familyOfElementsOfSection s).Compatible
-- Mathlib.RingTheory.RingHom.QuasiFinite
RingHom.QuasiFinite.propertyIsLocal : RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] => RingHom.QuasiFinite
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.mk.inj : ∀ {numVarsSucc : ℕ} {clause : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin numVarsSucc)}
  {nodupkey :
    autoParam (∀ (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin numVarsSucc), (l, true) ∉ clause ∨ (l, false) ∉ clause)
      Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.nodupkey._autoParam}
  {nodup : autoParam (List.Nodup clause) Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.nodup._autoParam}
  {clause_1 : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin numVarsSucc)}
  {nodupkey_1 :
    autoParam
      (∀ (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin numVarsSucc), (l, true) ∉ clause_1 ∨ (l, false) ∉ clause_1)
      Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.nodupkey._autoParam}
  {nodup_1 : autoParam (List.Nodup clause_1) Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.nodup._autoParam},
  { clause := clause, nodupkey := nodupkey, nodup := nodup } =
      { clause := clause_1, nodupkey := nodupkey_1, nodup := nodup_1 } →
    clause = clause_1
-- Mathlib.CategoryTheory.Action.Basic
Action.isIso_of_hom_isIso : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {M N : Action V G}
  (f : M ⟶ N) [CategoryTheory.IsIso f.hom], CategoryTheory.IsIso f
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- **Cauchy integral formula**: if `f : ℂ → E` is continuous on a closed disc of radius `R` and is
complex differentiable at all but countably many points of its interior, then for any `w` in this
interior we have $\oint_{|z-c|=R}(z-w)^{-1}f(z)\,dz=2πif(w)$.
 -/
Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {R : ℝ} {c w : ℂ} {f : ℂ → E}
  {s : Set ℂ},
  s.Countable →
    w ∈ Metric.ball c R →
      ContinuousOn f (Metric.closedBall c R) →
        (∀ x ∈ Metric.ball c R \ s, DifferentiableAt ℂ f x) →
          ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = (2 * ↑Real.pi * Complex.I) • f w
-- Mathlib.Data.Set.Operations
/-- `f ⁻¹' t` denotes the preimage of `t : Set β` under the function `f : α → β`.  -/
Set.«term_⁻¹'_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ)
  (n m : ℤ)
  (hnm : autoParam (n + m = 0) CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_app._auto_1),
  (CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C n m hnm).hom.app (Opposite.unop X)).op
      ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm).inv.app
        (Opposite.op ((CategoryTheory.shiftFunctor C n).obj (Opposite.unop X))))
-- Mathlib.GroupTheory.Exponent
AddSubgroup.exponent_top : ∀ {G : Type u} [inst : AddGroup G], AddMonoid.exponent ↥⊤ = AddMonoid.exponent G
-- Mathlib.RepresentationTheory.Intertwining
Representation.TensorProduct.toLinearMap_lid : ∀ {A : Type u_1} {G : Type u_2} {W : Type u_4} [inst : CommSemiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid W]
  [inst_3 : Module A W] (σ : Representation A G W),
  (↑(Representation.TensorProduct.lid A σ)).toLinearMap = ↑(TensorProduct.lid A W)
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.Sheaf.hom_ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] {F G : CategoryTheory.Sheaf J A} {f g : F ⟶ G}, f = g ↔ f.hom = g.hom
-- Mathlib.Order.Filter.Interval
Filter.tendsto_Ioo_Ici_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {a : α},
  Filter.TendstoIxxClass Set.Ioo (Filter.principal (Set.Ici a)) (Filter.principal (Set.Ioi a))
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- The source of every characteristic map of dimension `n` is
`(ball 0 1 : Set (Fin n → ℝ))`.  -/
Topology.CWComplex.source_eq : ∀ {X : Type u} {inst : TopologicalSpace X} {C : Set X} [self : Topology.CWComplex C] (n : ℕ)
  (i : Topology.CWComplex.cell C n), (Topology.CWComplex.map n i).source = Metric.ball 0 1
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers
/-- If `C` has all weak limits of diagrams `parallelPair f g`, then it has all weak equalizers  -/
CategoryTheory.Limits.hasWeakEqualizers_of_hasWeakLimit_parallelPair : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [∀ {X Y : C} {f g : X ⟶ Y}, CategoryTheory.Limits.HasWeakLimit (CategoryTheory.Limits.parallelPair f g)],
  CategoryTheory.Limits.HasWeakEqualizers C
-- Init.Data.SInt.Lemmas
Int64.toBitVec_ofBitVec : ∀ (b : BitVec 64), (Int64.ofBitVec b).toBitVec = b
-- Mathlib.LinearAlgebra.FreeModule.Basic
/-- If `B` is a basis of the `R`-algebra `S` such that `B i = 1` for some index `i`, then
each `r : R` gets represented as `s • B i` as an element of `S`.  -/
Module.Basis.repr_algebraMap : ∀ {R : Type u} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {ι : Type u_3}
  {B : Module.Basis ι R S} {i : ι}, B i = 1 → ∀ (r : R), B.repr ((algebraMap R S) r) = fun₀ | i => r
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsExistential.ex : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α (n + 1)}, φ.IsExistential → φ.ex.IsExistential
-- Mathlib.MeasureTheory.Group.AEStabilizer
MulAction.aestabilizer_univ : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {x : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_2 : MeasureTheory.SMulInvariantMeasure G α μ],
  MulAction.aestabilizer G μ Set.univ = ⊤
-- Mathlib.CategoryTheory.FinCategory.Basic
/-- A category with a `Fintype` of objects, and a `Fintype` for each morphism space.  -/
CategoryTheory.FinCategory : (J : Type v) → [CategoryTheory.SmallCategory J] → Type v
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
/-- Given functors `F G H` and natural transformations `f : F ⟶ H` and `g : g : G ⟶ H`, together
with a collection of limiting pullback cones for each cospan `F X ⟶ H X, G X ⟶ H X`, we can stitch
them together to give a pullback cone for the cospan formed by `f` and `g`.
`combinePullbackConesIsLimit` shows that this pullback cone is limiting.  -/
CategoryTheory.Limits.PullbackCone.combine : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F G H : CategoryTheory.Functor D C} →
          (f : F ⟶ H) →
            (g : G ⟶ H) →
              (c : (X : D) → CategoryTheory.Limits.PullbackCone (f.app X) (g.app X)) →
                ((X : D) → CategoryTheory.Limits.IsLimit (c X)) → CategoryTheory.Limits.PullbackCone f g
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.zero_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M N : C} [inst_3 : CategoryTheory.AddMonObj M]
  [inst_4 : CategoryTheory.AddMonObj N],
  CategoryTheory.AddMonObj.zero =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.zero CategoryTheory.AddMonObj.zero)
-- Mathlib.RingTheory.Localization.AsSubring
Localization.map_isUnit_of_le : ∀ {A : Type u_1} (K : Type u_2) [inst : CommRing A] (S : Submonoid A) [inst_1 : CommRing K] [inst_2 : Algebra A K]
  [IsFractionRing A K], S ≤ nonZeroDivisors A → ∀ (s : ↥S), IsUnit ((algebraMap A K) ↑s)
-- Mathlib.Data.Sym.Card
Sym2.card_subtype_diag : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α], Fintype.card { a // a.IsDiag } = Fintype.card α
-- Mathlib.Logic.OpClass
LeftCommutative.mk : ∀ {α : Sort u} {β : Sort v} {op : α → β → β},
  (∀ (a₁ a₂ : α) (b : β), op a₁ (op a₂ b) = op a₂ (op a₁ b)) → LeftCommutative op
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.IsRightDescent.eq_1 : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W) (i : B),
  cs.IsRightDescent w i = (cs.length (w * cs.simple i) < cs.length w)
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- `P` is a sheaf for `R` iff it is separated for `R` and there exists an amalgamation.  -/
CategoryTheory.Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X},
  (CategoryTheory.Presieve.IsSeparatedFor P R ∧
      ∀ (x : CategoryTheory.Presieve.FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) ↔
    CategoryTheory.Presieve.IsSheafFor P R
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getD_eq_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp],
  t.WF → ∀ {k fallback : α}, t.contains k = true → t.getD k fallback = k
-- Mathlib.Data.ZMod.ValMinAbs
ZMod.valMinAbs_nonneg_iff : ∀ {n : ℕ} [NeZero n] (x : ZMod n), 0 ≤ x.valMinAbs ↔ x.val ≤ n / 2
-- Mathlib.Data.Matrix.Mul
Matrix.vecMulVec_mulVec : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalSemiring α] [inst_1 : Fintype n] (u : m → α)
  (v w : n → α), (Matrix.vecMulVec u v).mulVec w = MulOpposite.op (v ⬝ᵥ w) • u
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.cRk_mono : ∀ {α : Type u} (M : Matroid α), Monotone M.cRk
-- Init.Data.List.Sublist
List.suffix_rfl : ∀ {α : Type u_1} {l : List α}, l <:+ l
-- Mathlib.Order.Filter.IsBounded
Filter.IsBounded.isCobounded_le : ∀ {α : Type u_1} {f : Filter α} [inst : Preorder α] [f.NeBot],
  Filter.IsBounded (fun x1 x2 => x2 ≤ x1) f → Filter.IsCobounded (fun x1 x2 => x1 ≤ x2) f
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.coker.π_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasCokernels C] (f : CategoryTheory.Arrow C),
  (CategoryTheory.Limits.coker.π C).app f = CategoryTheory.Limits.cokernel.π f.hom
-- Init.Data.Range.Polymorphic.UpwardEnumerable
/-- This typeclass ensures that an `UpwardEnumerable α` instance is compatible with a `Least? α`
instance. For nonempty `α`, it ensures that `least?` has a value and that every other value is
a transitive successor of it.
 -/
Std.PRange.LawfulUpwardEnumerableLeast? : (α : Type u) → [Std.PRange.UpwardEnumerable α] → [Std.PRange.Least? α] → Prop
-- Mathlib.NumberTheory.ModularForms.LFunction
ModularForm.weakFEPair_f : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1}
  [inst_1 : FunLike F UpperHalfPlane ℂ] (f : F) [inst_2 : ModularFormClass F Γ k] (t : ℝ),
  (ModularForm.weakFEPair hk f).f t = f (↑UpperHalfPlane.ofComplex (Complex.I * ↑t))
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.ι_app_homEquiv_symm : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F} (h : CategoryTheory.Limits.IsColimit t) {W : C}
  (f : F ⟶ (CategoryTheory.Functor.const J).obj W) (j : J),
  CategoryTheory.CategoryStruct.comp (t.ι.app j) (h.homEquiv.symm f) = f.app j
-- Init.Data.UInt.Bitwise
USize.or_zero : ∀ {a : USize}, a ||| 0 = a
-- Mathlib.Order.Partition.Basic
Partition.IsRepFun.mapsTo_of_disjoint : ∀ {α : Type u_1} {s u : Set α} {P : Partition u} {f : α → α}, P.IsRepFun f → Disjoint u s → Set.MapsTo f s s
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.limitCurrySwapCompLimIsoLimitCurryCompLim.eq_1 : ∀ {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]
  (G : CategoryTheory.Functor (J × K) C) [inst_3 : CategoryTheory.Limits.HasLimitsOfShape K C]
  [inst_4 : CategoryTheory.Limits.HasLimitsOfShape J C]
  [inst_5 : CategoryTheory.Limits.HasLimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim)],
  CategoryTheory.Limits.limitCurrySwapCompLimIsoLimitCurryCompLim G =
    Trans.trans
      (Trans.trans (CategoryTheory.Limits.limitIsoLimitCurryCompLim ((CategoryTheory.Prod.swap K J).comp G)).symm
        (CategoryTheory.Limits.HasLimit.isoOfEquivalence (CategoryTheory.Prod.braiding K J)
          (CategoryTheory.Iso.refl ((CategoryTheory.Prod.braiding K J).functor.comp G))))
      (CategoryTheory.Limits.limitIsoLimitCurryCompLim G)
-- Mathlib.Logic.Small.Set
small_empty : ∀ {α : Type u1}, Small.{u, u1} ↑∅
-- Mathlib.Order.Sublattice
Sublattice.mem_map_equiv : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] {L : Sublattice α} {f : α ≃o β} {a : β},
  a ∈ Sublattice.map { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯ } L ↔ f.symm a ∈ L
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKeyD_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] {l : List (α × β)} {k k' fallback : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l → (Std.DTreeMap.Raw.Const.ofList l cmp).getKeyD k' fallback = k
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.continuous : ∀ {𝕜 : 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] {H' : Type u_6} [inst_6 : TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {M' : Type u_10} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {n : WithTop ℕ∞}
  (h : Diffeomorph I I' M M' n), Continuous ⇑h
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
/-- The codiagonal morphism `pushout f f ⟶ Y` for a morphism `f : X ⟶ Y`.  -/
CategoryTheory.Limits.pushout.codiagonal : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y : C} →
      (f : X ⟶ Y) → [inst_1 : CategoryTheory.Limits.HasPushout f f] → CategoryTheory.Limits.pushout.codiagonalObj f ⟶ Y
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.continuous_lintegral_boundedContinuousFunction : ∀ {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [inst_2 : OpensMeasurableSpace X]
  (f : BoundedContinuousFunction X NNReal), Continuous fun μ => ∫⁻ (x : X), ↑(f x) ∂↑μ
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
CategoryTheory.MorphismProperty.LeftFraction₃.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y Y' : C}
  (f f' f'' : X ⟶ Y') (s : Y ⟶ Y') (hs : W s) (Y'_1 : C) (f_1 f'_1 f''_1 : X ⟶ Y'_1) (s_1 : Y ⟶ Y'_1) (hs_1 : W s_1),
  ({ Y' := Y', f := f, f' := f', f'' := f'', s := s, hs := hs } =
      { Y' := Y'_1, f := f_1, f' := f'_1, f'' := f''_1, s := s_1, hs := hs_1 }) =
    (Y' = Y'_1 ∧ f ≍ f_1 ∧ f' ≍ f'_1 ∧ f'' ≍ f''_1 ∧ s ≍ s_1)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.eq_coeff : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] [Lean.Grind.NoNatZeroDivisors α] (ctx : Lean.Grind.Linarith.Context α)
  (p₁ p₂ : Lean.Grind.Linarith.Poly) (k : ℕ),
  Lean.Grind.Linarith.eq_coeff_cert p₁ p₂ k = true →
    Lean.Grind.Linarith.Poly.denote' ctx p₁ = 0 → Lean.Grind.Linarith.Poly.denote' ctx p₂ = 0
-- Init.WFExtrinsicFix
WellFounded.fix.congr_simp : ∀ {α : Sort u} {C : α → Sort v} {r : α → α → Prop} (hwf : WellFounded r)
  (F F_1 : (x : α) → ((y : α) → r y x → C y) → C x), F = F_1 → ∀ (x : α), hwf.fix F x = hwf.fix F_1 x
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.edges_transfer : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet),
  (p.transfer H hp).edges = p.edges
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.OfNatIso.homOfCone_coneOfHom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {X : C} (h : F.cones.RepresentableBy X) {Y : C} (f : Y ⟶ X),
  CategoryTheory.Limits.IsLimit.OfNatIso.homOfCone h (CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom h f) = f
-- Mathlib.Algebra.Homology.HomotopyCategory.KProjective
/-- A choice of homotopy to zero for a morphism from a
K-projective cochain complex to an acyclic cochain complex.  -/
CochainComplex.IsKProjective.homotopyZero : {C : Type u_2} →
  [inst : CategoryTheory.Category.{u_3, u_2} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {K L : CochainComplex C ℤ} → (f : K ⟶ L) → HomologicalComplex.Acyclic L → [K.IsKProjective] → Homotopy f 0
-- Mathlib.Data.PFunctor.Univariate.M
/-- for a non-trivial approximation, return all the subtrees of the root  -/
PFunctor.Approx.children' : {F : PFunctor.{uA, uB}} →
  {n : ℕ} → (x : PFunctor.Approx.CofixA F n.succ) → F.B (PFunctor.Approx.head' x) → PFunctor.Approx.CofixA F n
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.ofEpiOfIsIsoOfMono'_φK : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₂.LeftHomologyData) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  (CategoryTheory.ShortComplex.LeftHomologyMapData.ofEpiOfIsIsoOfMono' φ h).φK =
    CategoryTheory.CategoryStruct.id (CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono' φ h).K
-- Mathlib.Computability.ContextFreeGrammar
/-- Initial nonterminal.  -/
ContextFreeGrammar.initial : {T : Type u_1} → (self : ContextFreeGrammar T) → self.NT
-- Init.Data.String.Iterator
String.iter : String → String.Legacy.Iterator
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey?_eq_getLast?_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.maxKey? = t.keys.getLast?
-- Mathlib.Algebra.BigOperators.ModEq
Int.ModEq.multisetSum_map : ∀ {α : Type u_1} {n : ℤ} {f g : α → ℤ} {s : Multiset α},
  (∀ x ∈ s, f x ≡ g x [ZMOD n]) → (Multiset.map f s).sum ≡ (Multiset.map g s).sum [ZMOD n]
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get!_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k k' : α} [inst_1 : Inhabited (β k')] {f : Option (β k) → Option (β k)},
  (t.alter k f).get! k' = if heq : cmp k k' = Ordering.eq then (Option.map (cast ⋯) (f (t.get? k))).get! else t.get! k'
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolution.unit_app_map_app_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  {F G : CategoryTheory.Functor C V} [inst_4 : CategoryTheory.MonoidalCategory.DayConvolution F G]
  {F' G' : CategoryTheory.Functor C V} [inst_5 : CategoryTheory.MonoidalCategory.DayConvolution F' G'] (f : F ⟶ F')
  (g : G ⟶ G') (x y : C) {Z : V}
  (h :
    (CategoryTheory.MonoidalCategory.DayConvolution.convolution F' G').obj
        (CategoryTheory.MonoidalCategoryStruct.tensorObj x y) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.unit F G).app (x, y))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.MonoidalCategory.DayConvolution.map f g).app
          (CategoryTheory.MonoidalCategoryStruct.tensorObj x y))
        h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (f.app x) (g.app y))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.unit F' G').app (x, y)) h)
-- Lean.Meta.Tactic.Grind.EMatch
/-- State for the E-matching monad  -/
Lean.Meta.Grind.EMatch.SearchState : Type