mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.ContDiff.Operations
contDiffOn_prod' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {n : WithTop ℕ∞} {𝔸' : Type u_4} {ι : Type u_5} [inst_3 : NormedCommRing 𝔸']
  [inst_4 : NormedAlgebra 𝕜 𝔸'] {t : Finset ι} {f : ι → E → 𝔸'},
  (∀ i ∈ t, ContDiffOn 𝕜 n (f i) s) → ContDiffOn 𝕜 n (∏ i ∈ t, f i) s
-- Init.Data.Array.Lemmas
Array.foldr_flatMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Array β} {g : β → γ → γ} {xs : Array α} {init : γ},
  Array.foldr g init (Array.flatMap f xs) = Array.foldr (fun x acc => Array.foldr g acc (f x)) init xs
-- Mathlib.Combinatorics.SimpleGraph.LineGraph
SimpleGraph.IsContained.isIndContained_lineGraph : ∀ {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'},
  G.IsContained G' → G.lineGraph.IsIndContained G'.lineGraph
-- Lean.Meta.HaveTelescope
Lean.Meta.ZetaUnusedMode.twoPasses.sizeOf_spec : sizeOf Lean.Meta.ZetaUnusedMode.twoPasses = 1
-- Mathlib.Data.Set.Countable
Set.Infinite.exists_subset_countable_infinite : ∀ {α : Type u} {s : Set α}, s.Infinite → ∃ t ⊆ s, t.Countable ∧ t.Infinite
-- Mathlib.Algebra.ContinuedFractions.Computation.Approximations
/-- Shows that the partial denominators `bᵢ` correspond to an integer.  -/
GenContFract.exists_int_eq_of_partDen : ∀ {K : Type u_1} {v : K} {n : ℕ} [inst : Field K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] {b : K},
  (GenContFract.of v).partDens.get? n = some b → ∃ z, b = ↑z
-- Mathlib.SetTheory.ZFC.Rank
ZFSet.rank_mk : ∀ (x : PSet.{u_1}), (ZFSet.mk x).rank = x.rank
-- Mathlib.NumberTheory.LSeries.HurwitzZeta
HurwitzZeta.hurwitzZeta_one_sub : ∀ (a : UnitAddCircle) {s : ℂ},
  (∀ (n : ℕ), s ≠ -↑n) →
    a ≠ 0 ∨ s ≠ 1 →
      HurwitzZeta.hurwitzZeta a (1 - s) =
        (2 * ↑Real.pi) ^ (-s) * Complex.Gamma s *
          (Complex.exp (-↑Real.pi * Complex.I * s / 2) * HurwitzZeta.expZeta a s +
            Complex.exp (↑Real.pi * Complex.I * s / 2) * HurwitzZeta.expZeta (-a) s)
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_inv_atBot_atTop : ∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : PartialOrder G] [IsOrderedMonoid G],
  Filter.Tendsto Inv.inv Filter.atBot Filter.atTop
-- Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
/-- Every `LieAdmissibleAlgebra` is a `LieAlgebra` with the commutator bracket.  -/
LieAdmissibleAlgebra.instLieAlgebra : {R : Type u_1} →
  {L : Type u_2} → [inst : CommRing R] → [inst_1 : LieAdmissibleRing L] → [LieAdmissibleAlgebra R L] → LieAlgebra R L
-- Std.Data.ExtHashMap.Basic
Std.ExtHashMap.instInsertProdOfEquivBEqOfLawfulHashable : {α : Type u} →
  {β : Type v} →
    {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Insert (α × β) (Std.ExtHashMap α β)
-- Mathlib.Algebra.Lie.Semisimple.Basic
/-- A simple lie algebra is non-trivial.  -/
LieAlgebra.IsSimple.nontrivial : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [LieAlgebra.IsSimple R L], Nontrivial L
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- Given a map `f : G →ₗ[𝕜] MultilinearMap 𝕜 E G'` and an estimate
`H : ∀ x m, ‖f x m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖`, construct a continuous linear
map from `G` to `ContinuousMultilinearMap 𝕜 E G'`.

In order to lift, e.g., a map `f : (MultilinearMap 𝕜 E G) →ₗ[𝕜] MultilinearMap 𝕜 E' G'`
to a map `(ContinuousMultilinearMap 𝕜 E G) →L[𝕜] ContinuousMultilinearMap 𝕜 E' G'`,
one can apply this construction to `f.comp ContinuousMultilinearMap.toMultilinearMapLinear`
which is a linear map from `ContinuousMultilinearMap 𝕜 E G` to `MultilinearMap 𝕜 E' G'`.  -/
MultilinearMap.mkContinuousLinear : {𝕜 : Type u} →
  {ι : Type v} →
    {E : ι → Type wE} →
      {G : Type wG} →
        {G' : Type wG'} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] →
              [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] →
                [inst_3 : SeminormedAddCommGroup G] →
                  [inst_4 : NormedSpace 𝕜 G] →
                    [inst_5 : SeminormedAddCommGroup G'] →
                      [inst_6 : NormedSpace 𝕜 G'] →
                        [inst_7 : Fintype ι] →
                          (f : G →ₗ[𝕜] MultilinearMap 𝕜 E G') →
                            (C : ℝ) →
                              (∀ (x : G) (m : (i : ι) → E i), ‖(f x) m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖) →
                                G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
-- Mathlib.MeasureTheory.Order.Lattice
AEMeasurable.sup : ∀ {M : Type u_1} [inst : MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f g : α → M} [inst_1 : Max M] [MeasurableSup₂ M], AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (f ⊔ g) μ
-- Lean.AddDecl
Lean.addAndCompile : Lean.Declaration → optParam Bool true → optParam Bool false → Lean.CoreM Unit
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt.0.Lean.Meta.Grind.Arith.Cutsat.checkDecl : Lean.Name → Lean.MetaM Unit
-- Mathlib.Data.Finset.Lattice.Fold
Finset.le_inf'_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] {s : Finset β} (H : s.Nonempty) (f : β → α) {a : α},
  a ≤ s.inf' H f ↔ ∀ b ∈ s, a ≤ f b
-- Mathlib.Data.PEquiv
PEquiv.instPartialOrderPEquiv : {α : Type u} → {β : Type v} → PartialOrder (α ≃. β)
-- Mathlib.Topology.Algebra.ConstMulAction
/-- Scalar multiplication by a nonzero scalar preserves neighborhoods.  -/
smul_mem_nhds_smul_iff₀ : ∀ {α : Type u_2} {G₀ : Type u_6} [inst : GroupWithZero G₀] [inst_1 : MulAction G₀ α] [inst_2 : TopologicalSpace α]
  [ContinuousConstSMul G₀ α] {c : G₀} {s : Set α} {x : α}, c ≠ 0 → (c • s ∈ nhds (c • x) ↔ s ∈ nhds x)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey_insertIfNew_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, t.isEmpty = true → (t.insertIfNew k v).minKey ⋯ = k
-- Mathlib.Algebra.BigOperators.Finprod
finsum_cond_eq_right : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {a : α}, ∑ᶠ (i : α) (_ : a = i), f i = f a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
/-- The pullback of `biprod.inl` and `biprod.inr` is the zero object.  -/
CategoryTheory.IsPullback.pullbackBiprodInlBiprodInr : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {X Y : C} →
          [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X Y] →
            CategoryTheory.Limits.pullback CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.inr ≅ 0
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Dependent recursion principle for `Localizations`: given elements `f a b : p (mk a b)`
for all `a b`, such that `r S (a, b) (c, d)` implies `f a b = f c d` (with the correct coercions),
then `f` is defined on the whole `Localization S`.  -/
Localization.rec : {M : Type u_1} →
  [inst : CommMonoid M] →
    {S : Submonoid M} →
      {p : Localization S → Sort u} →
        (f : (a : M) → (b : ↥S) → p (Localization.mk a b)) →
          (∀ {a c : M} {b d : ↥S} (h : (Localization.r S) (a, b) (c, d)), ⋯ ▸ f a b = f c d) →
            (x : Localization S) → p x
-- Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
CategoryTheory.Pretriangulated.commShiftIso_opOp_inv_app_assoc : ∀ {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.commShiftIso_opOp_inv_app._auto_1) {Z : Cᵒᵖᵒᵖ}
  (h : (CategoryTheory.opOp C).obj ((CategoryTheory.shiftFunctor C n).obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso (CategoryTheory.opOp C) n).inv.app X) h =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.shiftFunctorOpIso Cᵒᵖ n m hnm).hom.app (Opposite.op (Opposite.op X)))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C m n ⋯).inv.app (Opposite.op X)).op h)
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.fromNormalizedChainComplex.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C),
  X.fromNormalizedChainComplex R = (X.splitting.map (CategoryTheory.Limits.sigmaConst.obj R)).fromNondegComplex
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.constantCoeff_comp_map : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁),
  MvPolynomial.constantCoeff.comp (MvPolynomial.map f) = f.comp MvPolynomial.constantCoeff
-- Mathlib.Order.Bounds.Basic
bddAbove_preimage_ofDual : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, BddAbove (⇑OrderDual.ofDual ⁻¹' s) ↔ BddBelow s
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.instSMulOfLinear : {C : Type u_3} →
  [inst : CategoryTheory.Category.{u_2, u_3} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {R : Type u_1} →
        [inst_2 : Ring R] →
          [CategoryTheory.Linear R C] →
            (F G : CochainComplex C ℤ) → (n : ℤ) → SMul R (CochainComplex.HomComplex.Cochain F G n)
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_le_one_iff : ∀ {α : Type u_1} {M : Matroid α} {X : Set α} [M.Nonempty],
  autoParam (X ⊆ M.E) Matroid.eRk_le_one_iff._auto_1 → (M.eRk X ≤ 1 ↔ ∃ e ∈ M.E, X ⊆ M.closure {e})
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.zero_on_compl' : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} (self : ContDiffMapSupportedIn E F n K),
  Set.EqOn self.toFun 0 (↑K)ᶜ
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE_assoc : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Z.Opens) (V : Y.Opens) (W : X.Opens)
  (e₁ : V ≤ (TopologicalSpace.Opens.map g.base).obj U) (e₂ : W ≤ (TopologicalSpace.Opens.map f.base).obj V)
  {Z_1 : CommRingCat} (h : X.presheaf.obj (Opposite.op W) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appLE g U V e₁)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appLE f V W e₂) h) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Hom.appLE (CategoryTheory.CategoryStruct.comp f g) U W ⋯) h
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.not_hasNeg_removeNeg : ∀ (assignment : Std.Tactic.BVDecide.LRAT.Internal.Assignment), ¬assignment.removeNegAssignment.hasNegAssignment = true
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
SemimoduleCat.MonoidalCategory.braiding_inv_apply : ∀ {R : Type u} [inst : CommSemiring R] {M N : SemimoduleCat R} (m : ↑M) (n : ↑N),
  (CategoryTheory.ConcreteCategory.hom (β_ M N).inv) (n ⊗ₜ[R] m) = m ⊗ₜ[R] n
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- If `f` is a multilinear map, then `f.toLinearMap m i` is the linear map obtained by fixing all
coordinates but `i` equal to those of `m`, and varying the `i`-th coordinate.  -/
MultilinearMap.toLinearMap : {R : Type uR} →
  {ι : Type uι} →
    {M₁ : ι → Type v₁} →
      {M₂ : Type v₂} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] →
                [inst_4 : Module R M₂] →
                  MultilinearMap R M₁ M₂ → [DecidableEq ι] → ((i : ι) → M₁ i) → (i : ι) → M₁ i →ₗ[R] M₂
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.Adj.adj_sub : ∀ {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {u v : V}, H.Adj u v → G.Adj u v
-- Lean.Util.ParamMinimizer
_private.Lean.Util.ParamMinimizer.0.Lean.Util.ParamMinimizer.State.mk.inj : ∀ {cur : Array Bool} {added : Array ℕ} {numCalls : ℕ} {found : Bool} {cur_1 : Array Bool} {added_1 : Array ℕ}
  {numCalls_1 : ℕ} {found_1 : Bool},
  { cur := cur, added := added, numCalls := numCalls, found := found } =
      { cur := cur_1, added := added_1, numCalls := numCalls_1, found := found_1 } →
    cur = cur_1 ∧ added = added_1 ∧ numCalls = numCalls_1 ∧ found = found_1
-- Mathlib.Algebra.Order.Group.MinMax
max_div_div_left' : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : LinearOrder α] [IsOrderedMonoid α] (a b c : α),
  max (a / b) (a / c) = a / min b c
-- Mathlib.Algebra.SkewMonoidAlgebra.Support
/-- **Alias** of `SkewMonoidAlgebra.support_single`. -/
SkewMonoidAlgebra.support_single_ne_zero : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {b : k} (a : G),
  b ≠ 0 → (SkewMonoidAlgebra.single a b).support = {a}
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanShape.mk.inj : ∀ {L : Type w} {R : Type w'} {fst snd : R → L} {L_1 : Type w} {R_1 : Type w'} {fst_1 snd_1 : R_1 → L_1},
  { L := L, R := R, fst := fst, snd := snd } = { L := L_1, R := R_1, fst := fst_1, snd := snd_1 } →
    L = L_1 ∧ R = R_1 ∧ fst ≍ fst_1 ∧ snd ≍ snd_1
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.one.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : One M],
  MonoidAlgebra.one = { one := MonoidAlgebra.single 1 1 }
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.lift_mk'_spec : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} (hg : ∀ (y : ↥S), IsAddUnit (g ↑y)) (x : M) (v : P)
  (y : ↥S), (f.lift hg) (f.mk' x y) = v ↔ g x = g ↑y + v
-- Mathlib.Algebra.Homology.LeftResolution.Reduced
CategoryTheory.Abelian.LeftResolution.karoubi.π'_app_f : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive A] [inst_4 : ι.Additive] (X : A),
  ((CategoryTheory.Abelian.LeftResolution.karoubi.π' Λ).app X).f = Λ.π.app X
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- The right dual of the object `X`.  -/
CategoryTheory.HasRightDual.rightDual : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} → (X : C) → [self : CategoryTheory.HasRightDual X] → C
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- Two additive groups of the same prime cardinality are isomorphic.  -/
addEquivOfPrimeCardEq : {G : Type u_2} →
  {G' : Type u_3} →
    {p : ℕ} →
      [inst : AddGroup G] → [inst_1 : AddGroup G'] → [Fact (Nat.Prime p)] → Nat.card G = p → Nat.card G' = p → G ≃+ G'
-- Mathlib.Algebra.Group.Units.Defs
Units.instMonoid.eq_1 : ∀ {α : Type u} [inst : Monoid α],
  Units.instMonoid =
    { toMul := inferInstance.toMul, mul_assoc := ⋯, toOne := inferInstance.toOne, one_mul := ⋯, mul_one := ⋯,
      npow := fun n a => { val := ↑a ^ n, inv := ↑a⁻¹ ^ n, val_inv := ⋯, inv_val := ⋯ }, npow_zero := ⋯,
      npow_succ := ⋯ }
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremConstraint.maxInsts.sizeOf_spec : ∀ (n : ℕ), sizeOf (Lean.Meta.Grind.EMatchTheoremConstraint.maxInsts n) = 1 + sizeOf n
-- Init.Data.UInt.Basic
instLTUInt16 : LT UInt16
-- Mathlib.RingTheory.IsAdjoinRoot
/-- `IsAdjoinRoot.modByMonicHom` sends the equivalence class of `f` mod `g` to `f %ₘ g`.  -/
IsAdjoinRootMonic.modByMonicHom : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : Ring S] → {f : Polynomial R} → [inst_2 : Algebra R S] → IsAdjoinRootMonic S f → S →ₗ[R] Polynomial R
-- Lean.Meta.Sym.AlphaShareCommon
/-- Readonly context for `AlphaShareCommonM`.  -/
Lean.Meta.Sym.AlphaShareCommon.Context : Type
-- Mathlib.Topology.Homotopy.Path
/-- Given a homotopy `H : f ∼ g`, get the path traced by the point `x` as it moves from
`f x` to `g x`.
 -/
ContinuousMap.Homotopy.evalAt : {X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → {f g : C(X, Y)} → f.Homotopy g → (x : X) → Path (f x) (g x)
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
MvPolynomial.weightedHomogeneousComponent_directSum : ∀ (R : Type u_1) {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] (w : σ → M)
  [inst_2 : DecidableEq M] (x : DirectSum M fun i => ↥(MvPolynomial.weightedHomogeneousSubmodule R w i)) (m : M),
  (MvPolynomial.weightedHomogeneousComponent w m)
      ((DirectSum.coeLinearMap fun i => MvPolynomial.weightedHomogeneousSubmodule R w i) x) =
    ↑(x m)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_inv_app_op_one : CategoryTheory.Limits.walkingParallelPairOpEquiv.counitIso.inv.app
    (Opposite.op CategoryTheory.Limits.WalkingParallelPair.one) =
  CategoryTheory.CategoryStruct.id (Opposite.op CategoryTheory.Limits.WalkingParallelPair.one)
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.instSubNegMonoid : (A : Type u_3) → (E : Type u_4) → [SubNegMonoid E] → SubNegMonoid (WithCStarModule A E)
-- Mathlib.Data.FinEnum
/-- create an exhaustive list of the values of a given type  -/
FinEnum.toList : (α : Type u_1) → [FinEnum α] → List α
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsIsometricVAdd.to_continuousConstVAdd : ∀ (M : Type u) (X : Type w) [inst : PseudoEMetricSpace X] [inst_1 : VAdd M X] [IsIsometricVAdd M X],
  ContinuousConstVAdd M X
-- Lean.Elab.Command
/-- Disables incremental command reuse *and* reporting for `act` if `cond` is true by setting
`Context.snap?` to `none`.
 -/
Lean.Elab.Command.withoutCommandIncrementality : {α : Type} → Bool → Lean.Elab.Command.CommandElabM α → Lean.Elab.Command.CommandElabM α
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.bijective : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β),
  Function.Bijective ⇑h
-- Mathlib.RingTheory.DedekindDomain.Different
FractionalIdeal.mem_dual : ∀ {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] [inst_11 : IsDomain A]
  [inst_12 : IsFractionRing A K] [inst_13 : FiniteDimensional K L] [inst_14 : Algebra.IsSeparable K L]
  [inst_15 : IsIntegralClosure B A L] [inst_16 : IsFractionRing B L] [inst_17 : IsIntegrallyClosed A]
  [inst_18 : IsDedekindDomain B] {I : FractionalIdeal (nonZeroDivisors B) L},
  I ≠ 0 → ∀ {x : L}, x ∈ FractionalIdeal.dual A K I ↔ ∀ a ∈ I, ((Algebra.traceForm K L) x) a ∈ (algebraMap A K).range
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Result.addForalls : Lean.Meta.Simp.Result → Array Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result
-- Lean.Meta.Transform
Lean.TransformStep.continue.inj : ∀ {e? e?_1 : Option Lean.Expr}, Lean.TransformStep.continue e? = Lean.TransformStep.continue e?_1 → e? = e?_1
-- Std.Do.SPred.SPred
Std.Do.SPred.ext_nil_iff : ∀ {P Q : Std.Do.SPred []}, P = Q ↔ (P.down ↔ Q.down)
-- Mathlib.Data.Sign.Defs
/-- Casting out of `SignType` respects composition with suitable bundled homomorphism types.  -/
SignType.map_cast : ∀ {α : Type u_2} {β : Type u_3} {F : Type u_4} [inst : AddGroupWithOne α] [inst_1 : One β]
  [inst_2 : SubtractionMonoid β] [inst_3 : FunLike F α β] [AddMonoidHomClass F α β] [OneHomClass F α β] (f : F)
  (s : SignType), f ↑s = ↑s
-- Mathlib.CategoryTheory.Triangulated.Opposite.Functor
CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_hom_app_unop : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ] (X : Cᵒᵖ) (n : ℤ),
  F.map ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.hom.app X).unop =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.commShiftIso F n).hom.app (Opposite.unop ((CategoryTheory.shiftFunctor Cᵒᵖ n).obj X)))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor D n).map ((CategoryTheory.Functor.commShiftIso F.op n).inv.app X).unop)
        ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence D n).unitIso.hom.app
            (Opposite.op (F.obj (Opposite.unop X)))).unop)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The functor `HomologicalComplex C c ⥤ ShortComplex C` which sends a homological
complex `K` to the short complex `K.X (c.prev i) ⟶ K.X i ⟶ K.X (c.next i)`.  -/
HomologicalComplex.shortComplexFunctor : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        (c : ComplexShape ι) → ι → CategoryTheory.Functor (HomologicalComplex C c) (CategoryTheory.ShortComplex C)
-- Lean.Meta.Tactic.Simp.Types
/-- Try to use automatically generated congruence theorems. See `mkCongrSimp?`.
 -/
Lean.Meta.Simp.tryAutoCongrTheorem? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Meta.Simp.Result)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey_ofList_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l →
        ∀ {h' : k' ∈ Std.TreeMap.Raw.ofList l cmp}, (Std.TreeMap.Raw.ofList l cmp).getKey k' h' = k
-- Init.Data.Int.Lemmas
Int.negSucc_eq : ∀ (n : ℕ), Int.negSucc n = -(↑n + 1)
-- Batteries.Lean.Meta.UnusedNames
/-- Obtain the least natural number `i` such that `suggestion ++ "_i"` is an unused
name in the given local context. If `suggestion` itself is unused, the result
is `none`.
 -/
Lean.LocalContext.getUnusedUserNameIndex : Lean.LocalContext → Lean.Name → Option ℕ
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- `P.IsStableUnderCobaseChangeAgainst P'` states that for any morphism `f` satisfying `P` and
any morphism `g` with the same domain as `f` satisfying `P'`, any pushout of `f` along `g`
also satisfies `P`.  -/
CategoryTheory.MorphismProperty.IsStableUnderCobaseChangeAgainst : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.isNNRat_eq_true : ∀ {α : Type u} [inst : Semiring α] {a b : α} {n d : ℕ},
  Mathlib.Meta.NormNum.IsNNRat a n d → Mathlib.Meta.NormNum.IsNNRat b n d → a = b
-- Mathlib.CategoryTheory.Subobject.Comma
/-- If `C` is well-powered and complete and `T` preserves limits, then `StructuredArrow S T` is
well-powered.  -/
CategoryTheory.StructuredArrow.wellPowered_structuredArrow : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} [inst_2 : CategoryTheory.LocallySmall.{w, v₁, u₁} C]
  [CategoryTheory.WellPowered.{w, v₁, u₁} C] [CategoryTheory.Limits.HasFiniteLimits C]
  [CategoryTheory.Limits.PreservesFiniteLimits T],
  CategoryTheory.WellPowered.{w, v₁, max u₁ v₂} (CategoryTheory.StructuredArrow S T)
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
/-- The `ℤ`-linear map induced by precomposition of the projection `C → π C (ord I · < o)`.  -/
Profinite.NobelingProof.πs : {I : Type u} →
  (C : Set (I → Bool)) →
    [inst : LinearOrder I] →
      [inst_1 : WellFoundedLT I] →
        (o : Ordinal.{u}) →
          LocallyConstant ↑(Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o) ℤ →ₗ[ℤ]
            LocallyConstant ↑C ℤ