mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.fst.eq_1 : ∀ (A : Type u_2) (B : Type u_3) [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B],
  ContinuousMonoidHom.fst A B = { toMonoidHom := MonoidHom.fst A B, continuous_toFun := ⋯ }
-- Lean.Meta.Match.MatchEqsExt
Lean.Meta.Match.MatchEqnsExtState.map : Lean.Meta.Match.MatchEqnsExtState → Lean.PHashMap Lean.Name Lean.Meta.Match.MatchEqns
-- Aesop.Stats.Basic
Aesop.Stats.forwardState : Aesop.Stats → Aesop.Nanos
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrpObj.comp_sub : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G X Y : C} [inst_2 : CategoryTheory.AddGrpObj G] (f : X ⟶ Y) (g h : Y ⟶ G),
  CategoryTheory.CategoryStruct.comp f (g - h) =
    CategoryTheory.CategoryStruct.comp f g - CategoryTheory.CategoryStruct.comp f h
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.coe_sInf : ∀ {α : Type u_1} [inst : LE α] (S : Set (UpperSet α)), ↑(sInf S) = ⋃ s ∈ S, ↑s
-- Mathlib.Topology.Instances.ENNReal.Lemmas
/-- With truncation level `t`, the truncated cast `ℝ≥0∞ → ℝ` is given by `x ↦ (min t x).toReal`.
Unlike `ENNReal.toReal`, this cast is continuous and monotone when `t ≠ ∞`.  -/
ENNReal.truncateToReal : ENNReal → ENNReal → ℝ
-- Mathlib.SetTheory.ZFC.Class
Class.instCoeZFSet : Coe ZFSet.{u_1} Class.{u_1}
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
Complex.regularizedHGFunCoeff_eq_zero_iff : ∀ {a b : Multiset ℂ} {n : ℕ},
  Complex.regularizedHGFunCoeff a b n = 0 ↔ (∃ j ∈ a, ∃ k < n, j = -↑k) ∨ ∃ j ∈ b, ∃ m, j + ↑n = -↑m
-- Mathlib.RingTheory.Coalgebra.Basic
Prod.counit_comp_inl : ∀ (R : Type u) (A : Type v) (B : Type w) [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : AddCommMonoid B]
  [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : Coalgebra R A] [inst_6 : Coalgebra R B],
  CoalgebraStruct.counit ∘ₗ LinearMap.inl R A B = CoalgebraStruct.counit
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.orbitRel_apply : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {a b : α},
  (AddAction.orbitRel G α) a b ↔ a ∈ AddAction.orbit G b
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.instConcreteCategoryContinuousMapCarrier : CategoryTheory.ConcreteCategory TopCat fun X Y => C(↑X, ↑Y)
-- Mathlib.NumberTheory.SiegelsLemma
_private.Mathlib.NumberTheory.SiegelsLemma.0.Int.Matrix.termE : Lean.ParserDescr
-- Mathlib.Data.Fintype.BigOperators
/-- This lemma is specifically designed to be used backwards, whence the specialisation to `Fin n`
as the indexing type doesn't matter in practice. The more general forward direction lemma here is
`Fintype.card_pi`.  -/
Fintype.card_pi_const : ∀ (α : Type u_7) [inst : Fintype α] (n : ℕ), Fintype.card (Fin n → α) = Fintype.card α ^ n
-- Init.Data.List.Nat.Basic
List.tail_dropLast : ∀ {α : Type u_1} {l : List α}, l.dropLast.tail = l.tail.dropLast
-- Mathlib.LinearAlgebra.Finsupp.Pi
FunOnFinite.map_apply_apply : ∀ {M : Type u_5} [inst : AddCommMonoid M] {X : Type u_6} {Y : Type u_7} [inst_1 : Fintype X] [inst_2 : Finite Y]
  [inst_3 : DecidableEq Y] (f : X → Y) (s : X → M) (y : Y), FunOnFinite.map f s y = ∑ x with f x = y, s x
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.zpow_apply : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → DivInvMonoid (R i)] [inst_2 : ∀ (i : ι), SubgroupClass (S i) (R i)]
  (x : RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕) (n : ℤ) (i : ι), (x ^ n) i = x i ^ n
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- If `f` is integrable, then so is `-f`.  -/
MeasureTheory.Integrable.neg : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f : α → β}, MeasureTheory.Integrable f μ → MeasureTheory.Integrable (-f) μ
-- Mathlib.RingTheory.Multiplicity
emultiplicity_mk_eq_emultiplicity : ∀ {α : Type u_1} [inst : CommMonoid α] {a b : α}, emultiplicity (Associates.mk a) (Associates.mk b) = emultiplicity a b
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Substructure.fg_def : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] {N : L.Substructure M},
  N.FG ↔ ∃ S, S.Finite ∧ (FirstOrder.Language.Substructure.closure L).toFun S = N
-- Mathlib.Algebra.Category.Grp.Limits
/-- The forgetful functor from additive groups to types preserves all limits.

This means the underlying type of a limit can be computed as a limit in the category of types.  -/
AddGrpCat.forget_preservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget AddGrpCat)
-- Batteries.Data.Nat.Lemmas
/-- Strong case analysis on `a < b ∨ a = b ∨ b < a`  -/
Nat.sum_trichotomy : (a b : ℕ) → a < b ⊕' a = b ⊕' b < a
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- When the second map `S.g` is zero, this is the left homology data on `S` given by
the chosen `cokernel S.f`  -/
CategoryTheory.ShortComplex.LeftHomologyData.ofHasCokernel : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) → [CategoryTheory.Limits.HasCokernel S.f] → S.g = 0 → S.LeftHomologyData
-- Lean.MetavarContext
Lean.instantiateMVarDeclMVars : {m : Type → Type} → [Monad m] → [Lean.MonadMCtx m] → Lean.MVarId → m Unit
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
CategoryTheory.Limits.HasZeroObject.from_zero_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C] {X : C}
  {f g : 0 ⟶ X}, f = g ↔ True
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.sum_map' : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : AddCommMonoid M] (s : Finset ι) (e : ι ↪ κ),
  (Finset.map e s).sum = fun f => ∑ x ∈ s, f (e x)
-- Init.Data.List.Nat.TakeDrop
List.zipWith_replicate : ∀ {α : Type u_1} {β : Type u_2} {α_1 : Type u_3} {f : α → β → α_1} {a : α} {b : β} {m n : ℕ},
  List.zipWith f (List.replicate m a) (List.replicate n b) = List.replicate (min m n) (f a b)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.findCell_of_gt : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {k : α → Ordering} [Std.Internal.IsStrictCut compare k]
  {sz : ℕ} {k' : α} {v' : β k'} {l r : Std.DTreeMap.Internal.Impl α β},
  k k' = Ordering.gt →
    (Std.DTreeMap.Internal.Impl.inner sz k' v' l r).Ordered →
      Std.DTreeMap.Internal.List.findCell (Std.DTreeMap.Internal.Impl.inner sz k' v' l r).toListModel k =
        Std.DTreeMap.Internal.List.findCell r.toListModel k
-- Init.Data.UInt.Bitwise
UInt8.ofNat_or : ∀ (a b : ℕ), UInt8.ofNat (a ||| b) = UInt8.ofNat a ||| UInt8.ofNat b
-- Lean.Meta.Basic
Lean.Meta.instInhabitedProjReductionKind.default : Lean.Meta.ProjReductionKind
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.symm_comp_ofAddEquivOfLocalizations_apply' : ∀ {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) {k : P ≃+ N} (x : M),
  k ((f.ofAddEquivOfLocalizations k.symm) x) = f x
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
/-- Auxiliary definition for `rightAdjointObjIsDefined_of_isLimit`.  -/
CategoryTheory.Functor.representableByCompYonedaObjOfIsLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {J : Type u_1} →
            [inst_2 : CategoryTheory.Category.{v_1, u_1} J] →
              {R : CategoryTheory.Functor J F.PartialRightAdjointSource} →
                {c : CategoryTheory.Limits.Cone (R.comp F.rightAdjointObjIsDefined.ι)} →
                  CategoryTheory.Limits.IsLimit c →
                    {c' : CategoryTheory.Limits.Cone (R.comp F.partialRightAdjoint)} →
                      CategoryTheory.Limits.IsLimit c' →
                        (F.op.comp (CategoryTheory.yoneda.obj c.pt)).RepresentableBy c'.pt
-- Mathlib.RingTheory.PowerBasis
PowerBasis.mem_span_pow' : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {x y : S} {d : ℕ},
  y ∈ Submodule.span R (Set.range fun i => x ^ ↑i) ↔ ∃ f, f.degree < ↑d ∧ y = (Polynomial.aeval x) f
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.nonempty_of_measure_ne_zero : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α}, μ s ≠ 0 → s.Nonempty
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.filter_edgeFinset_toFinset_subset : ∀ {V : Type u_1} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] [inst_2 : DecidableEq V]
  (s : Finset V), {e ∈ G.edgeFinset | e.toFinset ⊆ s} = G.edgeFinset ∩ s.sym2
-- Mathlib.Tactic.NormNum.BigOperators
Mathlib.Meta.Multiset.range_zero' : ∀ {n : ℕ}, Mathlib.Meta.NormNum.IsNat n 0 → Multiset.range n = 0
-- Init.Data.UInt.Lemmas
UInt32.toBitVec_zero : UInt32.toBitVec 0 = 0#32
-- Mathlib.NumberTheory.ModularForms.Basic
/-- The weight `k` slash action of the negative-determinant matrix `J` preserves holomorphic
functions.  -/
_private.Mathlib.NumberTheory.ModularForms.Basic.0.MDifferentiable.slashJ : ∀ {f : UpperHalfPlane → ℂ}, MDiff f → ∀ (k : ℤ), MDiff (SlashAction.map k UpperHalfPlane.J f)
-- Aesop.Script.SpecificTactics
Aesop.splitTargetS? : Lean.MVarId → Aesop.ScriptM (Option (Array Lean.MVarId))
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
CategoryTheory.IsAddModHom.addActionHom_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.AddMonObj M] {X : C} [inst_3 : CategoryTheory.AddModObj M X] {Y : C}
  [inst_4 : CategoryTheory.AddModObj M Y] (f : X ⟶ Y) [inst_5 : CategoryTheory.IsAddModHom M f] (Z : C) (x : Z ⟶ X),
  (CategoryTheory.IsAddModHom.addActionHom f Z) x = CategoryTheory.CategoryStruct.comp x f
-- Mathlib.Data.List.Sort
List.Pairwise.orderedInsert : ∀ {α : Type u_1} {r : α → α → Prop} [inst : DecidableRel r] [Std.Total r] [IsTrans α r] (a : α) (l : List α),
  List.Pairwise r l → List.Pairwise r (List.orderedInsert r a l)
-- Init.Data.List.Basic
List.replicate.eq_1 : ∀ {α : Type u} (x : α), List.replicate 0 x = []
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.inv_singleton : ∀ {α : Type u_2} [inst : InvolutiveInv α] (a : α), {a}⁻¹ = {a⁻¹}
-- Mathlib.Algebra.Ring.Defs
/-- The canonical map `ℕ → R` is a homomorphism.  -/
NonAssocRing.natCast_succ : ∀ {α : Type u_1} [self : NonAssocRing α] (n : ℕ), ↑(n + 1) = ↑n + 1
-- Lean.Meta.Tactic.Congr
/-- Given a goal of the form `⊢ f as = f bs`, `⊢ (p → q) = (p' → q')`, or `⊢ f as ≍ f bs`, try to apply congruence.
It takes proof irrelevance into account, and the fact that `Decidable p` is a subsingleton.
 -/
Lean.MVarId.congrCore : Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.reduce_replicate : ∀ {α : Type u_1} [inst : DecidableEq α] (n : ℕ) (x : α × Bool),
  FreeAddGroup.reduce (List.replicate n x) = List.replicate n x
-- Std.Http.Data.URI.Encoding
/-- Encodes a raw string into an encoded userinfo component.
 -/
Std.Http.URI.EncodedUserInfo.encode : String → Std.Http.URI.EncodedUserInfo
-- Init.Data.Format.Basic
Std.Format.instInhabitedFlattenBehavior.default : Std.Format.FlattenBehavior
-- Mathlib.GroupTheory.OrderOfElement
orderOf_pow' : ∀ {G : Type u_1} [inst : Monoid G] (x : G) {n : ℕ}, n ≠ 0 → orderOf (x ^ n) = orderOf x / (orderOf x).gcd n
-- Mathlib.Tactic.TermCongr
Mathlib.Tactic.TermCongr.CongrResult.mk : Lean.Expr →
  Lean.Expr → Option (Mathlib.Tactic.TermCongr.CongrType → Lean.MetaM Lean.Expr) → Mathlib.Tactic.TermCongr.CongrResult
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.Core.mk : {α : Type u} →
  (uniformity : Filter (α × α)) →
    Filter.principal SetRel.id ≤ uniformity →
      Filter.Tendsto Prod.swap uniformity uniformity →
        (uniformity.lift' fun s => SetRel.comp s s) ≤ uniformity → UniformSpace.Core α
-- Mathlib.Topology.Sets.VietorisTopology
Set.powerset.eq_1 : ∀ {α : Type u} (s : Set α), 𝒫 s = {t | t ⊆ s}
-- Mathlib.GroupTheory.GroupAction.Period
AddAction.period_bounded_of_exponent_pos : ∀ (α : Type v) {M : Type u} [inst : AddMonoid M] [inst_1 : AddAction M α],
  0 < AddMonoid.exponent M → ∀ (m : M), BddAbove (Set.range fun a => AddAction.period m a)
-- Mathlib.Data.Multiset.Defs
Multiset.mem_pmap : ∀ {α : Type u_1} {β : Type v} {p : α → Prop} {f : (a : α) → p a → β} {s : Multiset α} {H : ∀ a ∈ s, p a} {b : β},
  b ∈ Multiset.pmap f s H ↔ ∃ a, ∃ (h : a ∈ s), f a ⋯ = b
-- Mathlib.Order.Circular
/-- The following lemmas are about the non-instances `LE.toBtw`, `LT.toSBtw` and
`LinearOrder.toCircularOrder`.  -/
sbtw_iff : ∀ {α : Type u_1} {a b c : α} [inst : LT α], sbtw a b c ↔ a < b ∧ b < c ∨ b < c ∧ c < a ∨ c < a ∧ a < b
-- Mathlib.Data.Set.Image
Set.image_id : ∀ {α : Type u_1} (s : Set α), id '' s = s
-- Mathlib.Data.EReal.Basic
/-- Extension for the `positivity` tactic: cast from `ℝ≥0∞` to `EReal`.  -/
Mathlib.Meta.Positivity.evalENNRealToEReal : Mathlib.Meta.Positivity.PositivityExt
-- 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.OplaxMonoidal.δ Action.FunctorCategoryEquivalence.functor A B =
    CategoryTheory.CategoryStruct.id
      (Action.FunctorCategoryEquivalence.functor.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj A B))
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.le_solvable_ideal_solvable : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {I J : LieIdeal R L},
  I ≤ J → LieAlgebra.IsSolvable ↥J → LieAlgebra.IsSolvable ↥I
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.unitOfList_eq_insertManyIfNewUnit_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {l : List α},
  Std.DHashMap.Const.unitOfList l = Std.DHashMap.Const.insertManyIfNewUnit ∅ l
-- Lean.HeadIndex
Lean.instReprHeadIndex : Repr Lean.HeadIndex
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instRingOfAddOpposite.eq_1 : ∀ {M : Type u_1} [inst : Ring Mᵃᵒᵖ], DomAddAct.instRingOfAddOpposite = inst
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.BodyState.chunkedSize.sizeOf_spec : sizeOf Std.Http.Protocol.H1.Reader.BodyState.chunkedSize = 1
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The continuous homomorphism given by the diagonal embedding.  -/
ContinuousMonoidHom.diag : (A : Type u_2) → [inst : Monoid A] → [inst_1 : TopologicalSpace A] → A →ₜ* A × A
-- Init.GrindInstances.ToInt
Lean.Grind.instToIntISizeSintNumBits : Lean.Grind.ToInt ISize (Lean.Grind.IntInterval.sint System.Platform.numBits)
-- Init.Data.List.Monadic
List.mapM'_eq_mapM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {f : α → m β} {l : List α},
  List.mapM' f l = List.mapM f l
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.lipschitzWith_pos_part : LipschitzWith 1 fun x => max x 0
-- Init.Data.BitVec.Lemmas
BitVec.getElem_replicate : ∀ {i n w : ℕ} {x : BitVec w} (h : i < w * n), (BitVec.replicate n x)[i] = if h' : w = 0 then false else x[i % w]
-- Mathlib.CategoryTheory.Abelian.LeftDerived
/-- We can compute a left derived functor using a chosen projective resolution.  -/
CategoryTheory.ProjectiveResolution.isoLeftDerivedObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        [inst_2 : CategoryTheory.Abelian C] →
          [inst_3 : CategoryTheory.HasProjectiveResolutions C] →
            [inst_4 : CategoryTheory.Abelian D] →
              {X : C} →
                (P : CategoryTheory.ProjectiveResolution X) →
                  (F : CategoryTheory.Functor C D) →
                    [inst_5 : F.Additive] →
                      (n : ℕ) →
                        (F.leftDerived n).obj X ≅
                          (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).obj
                            ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex)
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.prodEquiv_symm_apply : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃]
  [inst_4 : (i : ι) → Module R (M₁ i)] [inst_5 : Module R M₂] [inst_6 : Module R M₃]
  [inst_7 : (i : ι) → TopologicalSpace (M₁ i)] [inst_8 : TopologicalSpace M₂] [inst_9 : TopologicalSpace M₃]
  (f : ContinuousMultilinearMap R M₁ (M₂ × M₃)),
  ContinuousMultilinearMap.prodEquiv.symm f =
    ((ContinuousLinearMap.fst R M₂ M₃).compContinuousMultilinearMap f,
      (ContinuousLinearMap.snd R M₂ M₃).compContinuousMultilinearMap f)
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHom.comp_apply : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {P : Type u_3} [inst_2 : Monoid P] {φ : M →* N}
  {ψ : N →* P} {χ : M →* P} {A : Type u_4} [inst_3 : Monoid A] [inst_4 : MulDistribMulAction M A] {B : Type u_5}
  [inst_5 : Monoid B] [inst_6 : MulDistribMulAction N B] {C : Type u_7} [inst_7 : Monoid C]
  [inst_8 : MulDistribMulAction P C] (g : B →ₑ*[ψ] C) (f : A →ₑ*[φ] B) [inst_9 : φ.CompTriple ψ χ] (x : A),
  (g.comp f) x = g (f x)
-- Std.Time.Time.PlainTime
/-- `Nanoseconds` component of the `PlainTime`
 -/
Std.Time.PlainTime.nanosecond : Std.Time.PlainTime → Std.Time.Nanosecond.Ordinal
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
AddCommMonCat.FilteredColimits.colimitCocone.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J AddCommMonCat),
  AddCommMonCat.FilteredColimits.colimitCocone F =
    { pt := AddCommMonCat.FilteredColimits.colimit F,
      ι :=
        {
          app := fun j =>
            AddCommMonCat.ofHom
              (AddMonCat.Hom.hom
                ((AddMonCat.FilteredColimits.colimitCocone
                        (F.comp (CategoryTheory.forget₂ AddCommMonCat AddMonCat))).ι.app
                  j)),
          naturality := ⋯ } }
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- An isometric linear equivalence of two Hilbert spaces induces an equivalence of
⋆-algebras of their endomorphisms.

When `H = K`, this is exactly `Unitary.conjStarAlgAut`
(see `Unitary.conjStarAlgEquiv_unitaryLinearIsometryEquiv` and
`Unitary.conjStarAlgAut_symm_unitaryLinearIsometryEquiv`).  -/
LinearIsometryEquiv.conjStarAlgEquiv : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {H : Type u_5} →
      [inst_1 : NormedAddCommGroup H] →
        [inst_2 : InnerProductSpace 𝕜 H] →
          [inst_3 : CompleteSpace H] →
            {K : Type u_6} →
              [inst_4 : NormedAddCommGroup K] →
                [inst_5 : InnerProductSpace 𝕜 K] →
                  [inst_6 : CompleteSpace K] → (H ≃ₗᵢ[𝕜] K) → (H →L[𝕜] H) ≃⋆ₐ[𝕜] K →L[𝕜] K
-- Mathlib.Data.List.Sigma
List.dlookup_kinsert : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b : β a} (l : List (Sigma β)),
  List.dlookup a (List.kinsert a b l) = some b
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.liftEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {T X Y : C} (f : (T ⟶ X) × (T ⟶ Y)),
  CategoryTheory.CartesianMonoidalCategory.liftEquiv f = CategoryTheory.CartesianMonoidalCategory.lift f.1 f.2
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.support_refl : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α], Equiv.Perm.support (Equiv.refl α) = ∅
-- Aesop.Script.Step
Aesop.Script.LazyStep.postState : Aesop.Script.LazyStep → Lean.Meta.SavedState
-- Mathlib.Algebra.GroupWithZero.Units.Basic
IsUnit.mul_left_eq_zero : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {a b : M₀}, IsUnit b → (a * b = 0 ↔ a = 0)
-- Mathlib.Data.Sum.Interval
/-- Lifts maps `α₁ → β₁ → Finset γ₁`, `α₂ → β₂ → Finset γ₂`, `α₁ → β₂ → Finset γ₁`,
`α₂ → β₂ → Finset γ₂`  to a map `α₁ ⊕ α₂ → β₁ ⊕ β₂ → Finset (γ₁ ⊕ γ₂)`. Could be generalized to
alternative monads if we can make sure to keep computability and universe polymorphism.  -/
Finset.sumLexLift : {α₁ : Type u_1} →
  {α₂ : Type u_2} →
    {β₁ : Type u_3} →
      {β₂ : Type u_4} →
        {γ₁ : Type u_5} →
          {γ₂ : Type u_6} →
            (α₁ → β₁ → Finset γ₁) →
              (α₂ → β₂ → Finset γ₂) →
                (α₁ → β₂ → Finset γ₁) → (α₁ → β₂ → Finset γ₂) → α₁ ⊕ α₂ → β₁ ⊕ β₂ → Finset (γ₁ ⊕ γ₂)
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.toMultilinearMap_zero : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [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₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂],
  ContinuousMultilinearMap.toMultilinearMap 0 = 0
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- Addition in the colimit is well-defined in the left argument.  -/
AddMonCat.FilteredColimits.colimitAddAux_eq_of_rel_left : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCat)
  [inst_1 : CategoryTheory.IsFiltered J] {x x' y : (j : J) × ↑(F.obj j)},
  CategoryTheory.Limits.Types.FilteredColimit.Rel (F.comp (CategoryTheory.forget AddMonCat)) x x' →
    AddMonCat.FilteredColimits.colimitAddAux F x y = AddMonCat.FilteredColimits.colimitAddAux F x' y
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.pi_eq_bot_iff : ∀ {η : Type u_7} {f : η → Type u_8} [inst : (i : η) → Group (f i)] (H : (i : η) → Subgroup (f i)),
  Subgroup.pi Set.univ H = ⊥ ↔ ∀ (i : η), H i = ⊥
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryLT?.go.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (best : Option ((a : α) × β a)) (size : ℕ) (k' : α) (v : β k')
  (l r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.getEntryLT?.go k best (Std.DTreeMap.Internal.Impl.inner size k' v l r) =
    match compare k k' with
    | Ordering.gt => Std.DTreeMap.Internal.Impl.getEntryLT?.go k (some ⟨k', v⟩) r
    | x => Std.DTreeMap.Internal.Impl.getEntryLT?.go k best l
-- Mathlib.CategoryTheory.Comma.Over.StrictInitial
CategoryTheory.MorphismProperty.overEquivOfIsInitial_unitIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P Q : CategoryTheory.MorphismProperty C)
  [inst_1 : P.ContainsIdentities] [inst_2 : Q.IsMultiplicative] [inst_3 : Q.RespectsIso]
  [inst_4 : CategoryTheory.Limits.HasStrictInitialObjects C] (X : C) (h : CategoryTheory.Limits.IsInitial X),
  (CategoryTheory.MorphismProperty.overEquivOfIsInitial.{w, v_1, u_1} P Q X h).unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun A => CategoryTheory.MorphismProperty.Over.isoMk (CategoryTheory.asIso A.hom) ⋯) ⋯
-- Mathlib.GroupTheory.Perm.Sign
_private.Mathlib.GroupTheory.Perm.Sign.0.Equiv.Perm.signAux2.match_1.splitter : {α : Type u_1} →
  (motive : List α → Equiv.Perm α → Sort u_2) →
    (x : List α) →
      (x_1 : Equiv.Perm α) →
        ((x : Equiv.Perm α) → motive [] x) →
          ((x : α) → (l : List α) → (f : Equiv.Perm α) → motive (x :: l) f) → motive x x_1
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
/-- If `F` is an equivalence and `F.map f` is a normal mono, then `f` is a normal mono.  -/
CategoryTheory.equivalenceReflectsNormalMono : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₁, u₂} D] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (F : CategoryTheory.Functor C D) →
              [F.IsEquivalence] →
                {X Y : C} → {f : X ⟶ Y} → CategoryTheory.NormalMono (F.map f) → CategoryTheory.NormalMono f