mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.toList_filterMap : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w} {m : Std.DHashMap.Raw α fun x => β}
  {f : α → β → Option γ},
  m.WF →
    (Std.DHashMap.Raw.Const.toList (Std.DHashMap.Raw.filterMap f m)).Perm
      (List.filterMap (fun p => Option.map (fun x => (p.1, x)) (f p.1 p.2)) (Std.DHashMap.Raw.Const.toList m))
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.IsCommMonObj.mul_comm' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (M : C)
  [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.BraidedCategory C] [CategoryTheory.IsCommMonObj M],
  CategoryTheory.CategoryStruct.comp (β_ M M).inv CategoryTheory.MonObj.mul = CategoryTheory.MonObj.mul
-- Lean.Meta.Sorry
/-- Returns `sorryAx type synthetic`. Recall that `synthetic` is true if this sorry is from an error.

See also `Lean.Meta.mkLabeledSorry`, for creating a `sorry` that is labeled or unique.
 -/
Lean.Meta.mkSorry : Lean.Expr → Bool → Lean.MetaM Lean.Expr
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- Functional equation for the even Hurwitz zeta function (alternative form).  -/
HurwitzZeta.completedCosZeta_one_sub : ∀ (a : UnitAddCircle) (s : ℂ), HurwitzZeta.completedCosZeta a (1 - s) = HurwitzZeta.completedHurwitzZetaEven a s
-- Mathlib.CategoryTheory.Monoidal.Braided.Reflection
CategoryTheory.Monoidal.Reflective.instIsIsoAppUnitObjIhom : ∀ {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.MonoidalCategory D]
  [CategoryTheory.SymmetricCategory D] [inst_4 : CategoryTheory.MonoidalClosed D]
  [inst_5 : CategoryTheory.MonoidalCategory C] {L : CategoryTheory.Functor D C} [L.Monoidal]
  {R : CategoryTheory.Functor C D} [R.Faithful] [R.Full] (adj : L ⊣ R) (c : C) (d : D),
  CategoryTheory.IsIso (adj.unit.app (d ⟹ R.obj c))
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.ofMonComonObj_comon_comul_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Mon (CategoryTheory.Comon C)),
  CategoryTheory.ComonObj.comul.hom = CategoryTheory.ComonObj.comul
-- Mathlib.Data.Multiset.ZeroCons
Multiset.induction_on' : ∀ {α : Type u_1} {p : Multiset α → Prop} (S : Multiset α),
  p 0 → (∀ {a : α} {s : Multiset α}, a ∈ S → s ⊆ S → p s → p (insert a s)) → p S
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionAssocIso_unop : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction Cᵒᵖ Dᵒᵖ] (d : Dᵒᵖ) (c c' : Cᵒᵖ),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso (Opposite.unop d) (Opposite.unop c)
      (Opposite.unop c') =
    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c c').symm.unop
-- Mathlib.Algebra.Order.Antidiag.Pi
Finset.map_nsmul_piAntidiag : ∀ {ι : Type u_1} [inst : DecidableEq ι] (s : Finset ι) (m : ℕ) {n : ℕ} (hn : n ≠ 0),
  Finset.map { toFun := fun x => n • x, inj' := ⋯ } (s.piAntidiag m) = {f ∈ s.piAntidiag (n * m) | ∀ i ∈ s, n ∣ f i}
-- Mathlib.Algebra.Homology.HomotopyFiber
HomologicalComplex.pathObject.lift_π₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {α : Type u_2}
  {c : ComplexShape α} {F K : HomologicalComplex C c} [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasPathObject]
  (φ₀ φ₁ : F ⟶ K) (h : Homotopy φ₀ φ₁),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.pathObject.lift φ₀ φ₁ h) (HomologicalComplex.pathObject.π₁ K) =
    φ₁
-- Mathlib.Logic.Equiv.Defs
Equiv.nontrivial_congr : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β), Nontrivial α ↔ Nontrivial β
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnriched.hComp_assoc_heq : ∀ {C : Type u_1} [inst : CategoryTheory.EnrichedCategory CategoryTheory.Cat C] {a b c d : CategoryTheory.CatEnriched C}
  {f f' : a ⟶ b} {g g' : b ⟶ c} {h h' : c ⟶ d} (η : f ⟶ f') (θ : g ⟶ g') (κ : h ⟶ h'),
  CategoryTheory.CatEnriched.hComp (CategoryTheory.CatEnriched.hComp η θ) κ ≍
    CategoryTheory.CatEnriched.hComp η (CategoryTheory.CatEnriched.hComp θ κ)
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.finrank_rootSpace_eq_one : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L] [FiniteDimensional K L]
  {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L]
  [LieModule.IsTriangularizable K (↥H) L] [CharZero K] (α : LieModule.Weight K (↥H) L),
  α.IsNonZero → Module.finrank K ↥(LieAlgebra.rootSpace H ⇑α) = 1
-- Init.Data.Vector.Lemmas
Vector.toList_set! : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} {x : α}, (xs.set! i x).toList = xs.toList.set i x
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.instNormedSpace : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : SMulCommClass 𝕜 A A] → [inst_4 : IsScalarTower 𝕜 A A] → NormedSpace 𝕜 (DoubleCentralizer 𝕜 A)
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.isAddRightInvariant_smul : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Add G] {μ : MeasureTheory.Measure G} [μ.IsAddRightInvariant]
  (c : ENNReal), (c • μ).IsAddRightInvariant
-- Lean.Meta.Tactic.Grind.Proof
_private.Lean.Meta.Tactic.Grind.Proof.0.Lean.Meta.Grind.realizeEqProof : Lean.Expr → Lean.Expr → Lean.Expr → Bool → Bool → Lean.Meta.Grind.GoalM Lean.Expr
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.autCongr_refl : ∀ {R : Type uR} {A₁ : Type uA₁} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Algebra R A₁],
  AlgEquiv.refl.autCongr = MulEquiv.refl (A₁ ≃ₐ[R] A₁)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.deleteEdges_deleteEdges : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (s s' : Set (Sym2 V)),
  (G'.deleteEdges s).deleteEdges s' = G'.deleteEdges (s ∪ s')
-- Mathlib.GroupTheory.CosetCover
Subgroup.exists_leftTransversal_of_FiniteIndex : ∀ {G : Type u_1} [inst : Group G] {D H : Subgroup G} [D.FiniteIndex],
  D ≤ H → ∃ t, Subgroup.IsComplement ↑t ↑(D.subgroupOf H) ∧ ⋃ g ∈ t, ↑g • ↑D = ↑H
-- Init.Data.Array.Lemmas
Array.foldrM_congr : ∀ {α : Type u_1} {β : Type u_2} {start start' stop stop' : ℕ} {m : Type u_2 → Type u_3} [inst : Monad m]
  {f g : α → β → m β} {b : β} {xs xs' : Array α},
  xs = xs' →
    (∀ (x : α) (y : β), f x y = g x y) →
      start = start' → stop = stop' → Array.foldrM f b xs start stop = Array.foldrM g b xs' start' stop'
-- Init.Data.Nat.Bitwise.Lemmas
Nat.testBit_and : ∀ (x y i : ℕ), (x &&& y).testBit i = (x.testBit i && y.testBit i)
-- Mathlib.Tactic.ProxyType
/-- Returns a proxy type for a constructor and a pattern to use to match against it.

Input: a list of pairs associated to each argument of the constructor consisting
of (1) an fvar for this argument and (2) a name to use for this argument in patterns.

For example, given `#[(a, x), (b, y)]` with `x : Nat` and `y : Fin x`, then this function
returns `Sigma (fun x => Fin x)` and `⟨a, b⟩`.

Always returns a `Type*`. Uses `Unit`, `PLift`, and `Sigma`. Avoids using `PSigma` since
the `Fintype` instances for it go through `Sigma`s anyway.

The `decorateSigma` function is to wrap the `Sigma` a decorator such as `Lex`.
It should yield a definitionally equal type.  -/
Mathlib.ProxyType.defaultMkCtorProxyType : List (Lean.Expr × Lean.Name) →
  optParam (Lean.Expr → Lean.Elab.TermElabM Lean.Expr) pure → Lean.Elab.TermElabM (Lean.Expr × Lean.Term)
-- Mathlib.Data.ENNReal.Inv
/-- See `ENNReal.mul_iInf'` for the general case, and `ENNReal.mul_iInf_of_ne` for another special
case that assumes `a ≠ 0` but does not require `Nonempty ι`.  -/
ENNReal.mul_iInf : ∀ {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal} [Nonempty ι],
  (a = ⊤ → ⨅ i, f i = 0 → ∃ i, f i = 0) → a * ⨅ i, f i = ⨅ i, a * f i
-- Std.Sync.Channel
/-- `ch.forAsync f` calls `f` for every message received on `ch`.

Note that if this function is called twice, each message will only arrive at exactly one invocation.
 -/
Std.CloseableChannel.forAsync : {α : Type} →
  (α → BaseIO Unit) → Std.CloseableChannel α → optParam Task.Priority Task.Priority.default → BaseIO (Task Unit)
-- Mathlib.Algebra.Ring.Invertible
neg_one_eq_invOf_mul_add_invOf_mul_iff : ∀ {R : Type u_1} [inst : Ring R] {a b : R} [inst_1 : Invertible a] [inst_2 : Invertible b]
  [inst_3 : Invertible (a + b)], ⅟(a + b) = ⅟a + ⅟b ↔ -1 = ⅟a * b + ⅟b * a
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs
/-- An element `x` of `A` is said to be integral over `R` with respect to `f`
if it is a root of a monic polynomial `p : R[X]` evaluated under `f`  -/
RingHom.IsIntegralElem : {R : Type u_1} → {A : Type u_3} → [inst : CommRing R] → [inst_1 : Ring A] → (R →+* A) → A → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback_map_app_snd : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X}
  (φ : S ⟶ S') (x : X),
  (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback F G X).map φ).app x).snd =
    φ.snd.app x
-- Init.Data.BitVec.Lemmas
_private.Init.Data.BitVec.Lemmas.0.BitVec.sdiv_eq.match_1.eq_4 : ∀ (motive : Bool → Bool → Sort u_1) (h_1 : Unit → motive false false) (h_2 : Unit → motive false true)
  (h_3 : Unit → motive true false) (h_4 : Unit → motive true true),
  (match true, true with
    | false, false => h_1 ()
    | false, true => h_2 ()
    | true, false => h_3 ()
    | true, true => h_4 ()) =
    h_4 ()
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.PreInstance.mk.inj : ∀ {proof : Lean.Expr} {assignment : Array Lean.Expr} {proof_1 : Lean.Expr} {assignment_1 : Array Lean.Expr},
  { proof := proof, assignment := assignment } = { proof := proof_1, assignment := assignment_1 } →
    proof = proof_1 ∧ assignment = assignment_1
-- Init.Data.UInt.Lemmas
UInt64.not_lt : ∀ {a b : UInt64}, ¬a < b ↔ b ≤ a
-- Mathlib.Algebra.Group.Basic
/-- To show a property of all multiples of `g` it suffices to show it is closed under
addition by `g` and `-g` on the right. For additive subgroups generated by more than one element,
see `AddSubgroup.closure_induction_right`.  -/
zsmul_induction_right : ∀ {G : Type u_3} [inst : AddGroup G] {g : G} {P : G → Prop},
  P 0 → (∀ (a : G), P a → P (a + g)) → (∀ (a : G), P a → P (a + -g)) → ∀ (n : ℤ), P (n • g)
-- Mathlib.Order.Monotone.Defs
Monotone.prodMk : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : γ → α}
  {g : γ → β}, Monotone f → Monotone g → Monotone fun x => (f x, g x)
-- Mathlib.MeasureTheory.Function.SimpleFunc
/-- Combine two simple functions `f : α →ₛ β` and `g : α →ₛ β`
into `fun a => (f a, g a)`.  -/
MeasureTheory.SimpleFunc.pair : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      [inst : MeasurableSpace α] →
        MeasureTheory.SimpleFunc α β → MeasureTheory.SimpleFunc α γ → MeasureTheory.SimpleFunc α (β × γ)
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.algebra : {R : Type u} → [inst : CommRing R] → (self : CommAlgCat R) → Algebra R ↑self
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_neg : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (A : Matrix n n R),
  (-A).det = (-1) ^ Fintype.card n * A.det
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.instMetricSpace : (α : Type u_1) →
  [inst : TopologicalSpace α] → [CompactSpace α] → {β : Type u_4} → [inst_2 : MetricSpace β] → MetricSpace C(α, β)
-- Mathlib.Algebra.Algebra.Subalgebra.Tower
Subalgebra.restrictScalars_top : ∀ (R : Type u) {S : Type v} {A : Type w} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [inst_6 : IsScalarTower R S A],
  Subalgebra.restrictScalars R ⊤ = ⊤
-- Mathlib.Analysis.Normed.Group.Constructions
ULift.normedGroup.eq_1 : ∀ {E : Type u_2} [inst : NormedGroup E],
  ULift.normedGroup = NormedGroup.induced (ULift.{u_5, u_2} E) E { toFun := ULift.down, map_one' := ⋯, map_mul' := ⋯ } ⋯
-- Init.Data.UInt.Basic
instXorOpUInt16 : XorOp UInt16
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.instStarForall : {ι : Type u_1} → {R : ι → Type u_6} → [(i : ι) → Star (R i)] → Star ((i : ι) → R i)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Triangle.affineSpan_pair_eq_orthRadius : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P) [Fact (Module.finrank ℝ V = 2)] (signs : Finset (Fin 3))
  {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ →
    i₁ ≠ i₃ →
      i₂ ≠ i₃ →
        line[ℝ, t.points i₂, t.points i₃] =
          (Affine.Simplex.exsphere t signs).orthRadius (Affine.Simplex.touchpoint t signs i₁)
-- Lean.Meta.Basic
Lean.Meta.Context.mk : Lean.Meta.ConfigWithKey →
  Bool →
    Lean.FVarIdSet →
      Lean.LocalContext →
        Lean.LocalInstances →
          Option Lean.Meta.DefEqContext →
            ℕ → Option (Lean.Meta.Config → Lean.ConstantInfo → Lean.CoreM Bool) → Bool → Bool → Bool → Lean.Meta.Context
-- Lean.MetavarContext
Lean.instInhabitedMetavarKind.default : Lean.MetavarKind
-- Mathlib.Topology.Order.Bornology
/-- Predicate for a preorder to be equipped with its order-bornology, namely for its bounded sets
to be the ones that are bounded both above and below.  -/
IsOrderBornology : (α : Type u_1) → [Bornology α] → [Preorder α] → Prop
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
LinearMap.BilinForm.IsSymm.eq_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M}, B.IsSymm → ∀ {x y : M}, (B x) y = 0 ↔ (B y) x = 0
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.ν_comp_unitDesc_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]
  [hasDayConvolution :
    ∀ (F G : CategoryTheory.Functor C V),
      (CategoryTheory.MonoidalCategory.tensor C).HasPointwiseLeftKanExtension
        (CategoryTheory.MonoidalCategory.externalProduct F G)]
  [hasDayConvolutionUnit :
    (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension
      (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))]
  [inst_4 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_5 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_6 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_7 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_8 :
    ∀ (v : V) (d : C × C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          ((CategoryTheory.Functor.id C).prod
            (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
          d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_9 :
    ∀ (v : V) (d : C × C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          ((CategoryTheory.MonoidalCategory.tensor C).prod (CategoryTheory.Functor.id C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  {F : CategoryTheory.MonoidalCategory.DayFunctor C V}
  (φ :
    CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶
      F.functor.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
  {Z : V} (h : F.functor.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayFunctor.ν C V)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.MonoidalCategory.DayFunctor.unitDesc φ).natTrans.app
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
        h) =
    CategoryTheory.CategoryStruct.comp φ h
-- Aesop.RuleTac.GoalDiff
Aesop.isGoalDiffDefeqExpr : Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.π_homologyMap_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (φ : S₁ ⟶ S₂),
  CategoryTheory.CategoryStruct.comp S₁.homologyπ
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) S₂.homologyι) =
    CategoryTheory.CategoryStruct.comp S₁.iCycles (CategoryTheory.CategoryStruct.comp φ.τ₂ S₂.pOpcycles)
-- Init.Data.Array.Lemmas
Array.any_toList : ∀ {α : Type u_1} {p : α → Bool} {as : Array α}, as.toList.any p = as.any p
-- Mathlib.Condensed.Discrete.LocallyConstant
/-- The unit of the adjunction is an iso.  -/
CompHausLike.LocallyConstant.unitIso : (P : TopCat → Prop) →
  [inst : CompHausLike.HasProp P PUnit.{u + 1}] →
    [inst_1 : CompHausLike.HasExplicitFiniteCoproducts P] →
      [inst_2 : CompHausLike.HasExplicitPullbacks P] →
        (hs :
            ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
              CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) →
          CategoryTheory.Functor.id (Type (max u w)) ≅
            (CompHausLike.LocallyConstant.functor P hs).comp
              ((CategoryTheory.sheafSections (CategoryTheory.coherentTopology (CompHausLike P)) (Type (max u w))).obj
                (Opposite.op (CompHausLike.of P PUnit.{u + 1})))
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.insertManyIfNewUnit_cons : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => Unit},
  m.WF →
    ∀ {l : List α} {k : α},
      Std.DHashMap.Raw.Const.insertManyIfNewUnit m (k :: l) =
        Std.DHashMap.Raw.Const.insertManyIfNewUnit (m.insertIfNew k ()) l
-- Init.Data.Nat.Lemmas
Nat.lt_two_pow_self : ∀ {n : ℕ}, n < 2 ^ n
-- Mathlib.Algebra.Algebra.Hom
AlgHom.coe_comp : ∀ {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Semiring C] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R C]
  (φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B), ⇑(φ₁.comp φ₂) = ⇑φ₁ ∘ ⇑φ₂
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.equivProdDFinsupp_apply : ∀ {ι : Type u} {α : Option ι → Type v} [inst : (i : Option ι) → Zero (α i)] (f : Π₀ (i : Option ι), α i),
  DFinsupp.equivProdDFinsupp f = (f none, DFinsupp.comapDomain some ⋯ f)
-- Mathlib.Topology.Order.LocalExtr
IsLocalMin.max : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f g : α → β} {a : α},
  IsLocalMin f a → IsLocalMin g a → IsLocalMin (fun x => max (f x) (g x)) a
-- Mathlib.Data.Fin.SuccPred
Fin.one_pos' : ∀ {n : ℕ} [NeZero n], 0 < 1
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.smulRight_eq_comp : ∀ {R : Type u_12} {M₁ : Type u_13} {M₂ : Type u_14} {ι : Type u_15} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] (f : M₁ [⋀^ι]→ₗ[R] R) (z : M₂),
  f.smulRight z = (LinearMap.id.smulRight z).compAlternatingMap f
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
/-- The lattice formed by the image of the logarithmic embedding.  -/
NumberField.Units.unitLattice : (K : Type u_1) →
  [inst : Field K] → [inst_1 : NumberField K] → Submodule ℤ (NumberField.Units.dirichletUnitTheorem.logSpace K)
-- Mathlib.RingTheory.IsTensorProduct
IsBaseChange.lift_comp : ∀ {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  [inst_2 : CommSemiring R] [inst_3 : CommSemiring S] [inst_4 : Algebra R S] [inst_5 : Module R M] [inst_6 : Module R N]
  [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) {Q : Type u_3}
  [inst_9 : AddCommMonoid Q] [inst_10 : Module S Q] [inst_11 : Module R Q] [inst_12 : IsScalarTower R S Q]
  (g : M →ₗ[R] Q), ↑R (h.lift g) ∘ₗ f = g
-- Lean.Parser.Types
Lean.Parser.ParserState.mkError : Lean.Parser.ParserState → String → Lean.Parser.ParserState
-- Mathlib.Computability.RecursiveIn
ComputableIn.sumInr : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {O : Set (ℕ →. ℕ)},
  ComputableIn O Sum.inr
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
instDenselyOrderedUnits : ∀ {α : Type u_1} [inst : LinearOrderedCommGroupWithZero α] [DenselyOrdered α], DenselyOrdered αˣ
-- Mathlib.Logic.Relation
/-- `ReflGen r`: reflexive closure of `r`  -/
Relation.ReflGen : {α : Type u_1} → (α → α → Prop) → α → α → Prop
-- Mathlib.Algebra.Homology.Additive
CategoryTheory.Functor.mapHomologicalComplex_obj_d : ∀ {ι : 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₂)
  [inst_4 : F.PreservesZeroMorphisms] (c : ComplexShape ι) (C : HomologicalComplex W₁ c) (i j : ι),
  ((F.mapHomologicalComplex c).obj C).d i j = F.map (C.d i j)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.FoldingRange : Type
-- Lean.Server.Completion.CompletionUtils
Lean.Server.Completion.HoverInfo.after.sizeOf_spec : sizeOf Lean.Server.Completion.HoverInfo.after = 1
-- Mathlib.Topology.Algebra.NonUnitalAlgebra
/-- The coercion from an elemental algebra to the full algebra is a `IsClosedEmbedding`.  -/
NonUnitalAlgebra.elemental.isClosedEmbedding_coe : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] [inst_5 : TopologicalSpace A]
  [inst_6 : IsSemitopologicalSemiring A] [inst_7 : ContinuousConstSMul R A] (x : A),
  Topology.IsClosedEmbedding Subtype.val
-- Mathlib.Order.SuccPred.Basic
Order.succ_le_succ_iff : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α} [NoMaxOrder α],
  Order.succ a ≤ Order.succ b ↔ a ≤ b
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- The isomorphism `S.X₂ ≅ S.X₁ ⊞ S.X₃` induced by a splitting of the short complex `S`.  -/
CategoryTheory.ShortComplex.Splitting.isoBinaryBiproduct : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S : CategoryTheory.ShortComplex C} →
        S.Splitting → [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct S.X₁ S.X₃] → S.X₂ ≅ S.X₁ ⊞ S.X₃