mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_diff_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Inhabited β] {k : α}, k ∉ t₁ → Std.ExtDTreeMap.Const.get! (t₁ \ t₂) k = default
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Real.rpowIntegrand₁₂_zero : ∀ {p t : ℝ}, 0 < t → p.rpowIntegrand₁₂ t 0 = 0
-- Qq.Macro
Qq.Impl.UnquoteState.mk.sizeOf_spec : ∀ (mvars : List (Lean.Expr × Qq.Impl.MVarSynth)) (levelSubst : Std.HashMap Lean.Expr Lean.Level)
  (exprSubst : Std.HashMap Lean.Expr Lean.Expr) (unquoted : Lean.LocalContext)
  (exprBackSubst : Std.HashMap Lean.Expr Qq.Impl.ExprBackSubstResult)
  (levelBackSubst : Std.HashMap Lean.Level Lean.Expr) (abstractedFVars : Array Lean.FVarId)
  (levelNames : List Lean.Name) (mayPostpone : Bool),
  sizeOf
      { mvars := mvars, levelSubst := levelSubst, exprSubst := exprSubst, unquoted := unquoted,
        exprBackSubst := exprBackSubst, levelBackSubst := levelBackSubst, abstractedFVars := abstractedFVars,
        levelNames := levelNames, mayPostpone := mayPostpone } =
    1 + sizeOf mvars + sizeOf levelSubst + sizeOf exprSubst + sizeOf unquoted + sizeOf exprBackSubst +
            sizeOf levelBackSubst +
          sizeOf abstractedFVars +
        sizeOf levelNames +
      sizeOf mayPostpone
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.instPartialOrder : {C : Type u} → [inst : CategoryTheory.Groupoid C] → PartialOrder (CategoryTheory.Subgroupoid C)
-- Std.Data.Internal.List.Associative
Std.Internal.List.find?_map_toProd_eq_some_iff_getKey?_eq_some_and_getValue?_eq_some : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] {β : Type v} {k k' : α} {v : β} {l : List ((_ : α) × β)},
  List.find? (fun a => a.1 == k) (List.map (fun x => (x.fst, x.snd)) l) = some (k', v) ↔
    Std.Internal.List.getKey? k l = some k' ∧ Std.Internal.List.getValue? k l = some v
-- Aesop.Util.UnorderedArraySet
/-- O(n^2)  -/
Aesop.UnorderedArraySet.ofArraySlow : {α : Type u_1} → [inst : BEq α] → Array α → Aesop.UnorderedArraySet α
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.preEquivalence_unitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.CostructuredArrow G e),
  (CategoryTheory.CostructuredArrow.preEquivalence F f).unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun X =>
        CategoryTheory.CostructuredArrow.isoMk
          (CategoryTheory.CostructuredArrow.isoMk
            (CategoryTheory.Iso.refl
              ((CategoryTheory.Functor.id
                        (CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.pre F G e) f)).obj
                    X).left.left)
            ⋯)
          ⋯)
      ⋯
-- Mathlib.CategoryTheory.Monoidal.Closed.Enrichment
CategoryTheory.MonoidalClosed.enrichedCategorySelf_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.MonoidalClosed C] (X Y Z : C),
  CategoryTheory.eComp C X Y Z = CategoryTheory.MonoidalClosed.comp X Y Z
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLT_obj_coe : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ), t.eTruncLT.obj (WithBotTop.coe n) = t.truncLT n
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Summable.tsum_nsmul : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {L : SummationFilter β} [T2Space α] [ContinuousAdd α] [L.NeBot],
  Summable f L → ∀ (n : ℕ), ∑'[L] (b : β), n • f b = n • ∑'[L] (b : β), f b
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Roo.toList_iter : ∀ {α : Type u_1} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [inst_4 : Std.Rxo.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Roo α}, r.iter.toList = r.toList
-- Mathlib.Algebra.Group.Action.Prod
/-- Scalar multiplication as a multiplicative homomorphism.  -/
smulMulHom : {α : Type u_5} →
  {β : Type u_6} →
    [inst : Monoid α] →
      [inst_1 : Mul β] → [inst_2 : MulAction α β] → [IsScalarTower α β β] → [SMulCommClass α β β] → α × β →ₙ* β
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.of_intCast : ∀ {ι : Type u_1} [inst : DecidableEq ι] (A : ι → Type u_2) [inst_1 : (i : ι) → AddCommGroup (A i)]
  [inst_2 : AddMonoid ι] [inst_3 : DirectSum.GRing A] (n : ℤ), (DirectSum.of A 0) ↑n = ↑n
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- The algebra hom `A/I →+* B/J` induced by an algebra hom `f : A →ₐ[R₁] B` with `I ≤ f⁻¹(J)`.  -/
Ideal.quotientMapₐ : {R₁ : Type u_1} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : CommSemiring R₁] →
        [inst_1 : Ring A] →
          [inst_2 : Algebra R₁ A] →
            [inst_3 : Ring B] →
              [inst_4 : Algebra R₁ B] →
                {I : Ideal A} →
                  (J : Ideal B) →
                    [inst_5 : I.IsTwoSided] →
                      [inst_6 : J.IsTwoSided] → (f : A →ₐ[R₁] B) → I ≤ Ideal.comap f J → A ⧸ I →ₐ[R₁] B ⧸ J
-- Mathlib.RingTheory.Ideal.Pointwise
Ideal.pointwise_smul_subset_iff : ∀ {M : Type u_1} {R : Type u_3} [inst : Group M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] {a : M}
  {S T : Ideal R}, a • S ≤ T ↔ S ≤ a⁻¹ • T
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_mem_Icc : ∀ (x : ℝ), Real.cos x ∈ Set.Icc (-1) 1
-- Init.Grind.ToInt
_private.Init.Grind.ToInt.0.Lean.Grind.instBEqIntInterval.beq.match_1.eq_5 : ∀ (motive : Lean.Grind.IntInterval → Lean.Grind.IntInterval → Sort u_1) (x x_1 : Lean.Grind.IntInterval)
  (h_1 : (a a_1 b b_1 : ℤ) → motive (Lean.Grind.IntInterval.co a a_1) (Lean.Grind.IntInterval.co b b_1))
  (h_2 : (a b : ℤ) → motive (Lean.Grind.IntInterval.ci a) (Lean.Grind.IntInterval.ci b))
  (h_3 : (a b : ℤ) → motive (Lean.Grind.IntInterval.io a) (Lean.Grind.IntInterval.io b))
  (h_4 : Unit → motive Lean.Grind.IntInterval.ii Lean.Grind.IntInterval.ii)
  (h_5 : (x x_2 : Lean.Grind.IntInterval) → motive x x_2),
  (∀ (a a_1 b b_1 : ℤ), x = Lean.Grind.IntInterval.co a a_1 → x_1 = Lean.Grind.IntInterval.co b b_1 → False) →
    (∀ (a b : ℤ), x = Lean.Grind.IntInterval.ci a → x_1 = Lean.Grind.IntInterval.ci b → False) →
      (∀ (a b : ℤ), x = Lean.Grind.IntInterval.io a → x_1 = Lean.Grind.IntInterval.io b → False) →
        (x = Lean.Grind.IntInterval.ii → x_1 = Lean.Grind.IntInterval.ii → False) →
          (match x, x_1 with
            | Lean.Grind.IntInterval.co a a_1, Lean.Grind.IntInterval.co b b_1 => h_1 a a_1 b b_1
            | Lean.Grind.IntInterval.ci a, Lean.Grind.IntInterval.ci b => h_2 a b
            | Lean.Grind.IntInterval.io a, Lean.Grind.IntInterval.io b => h_3 a b
            | Lean.Grind.IntInterval.ii, Lean.Grind.IntInterval.ii => h_4 ()
            | x, x_6 => h_5 x x_6) =
            h_5 x x_1
-- Mathlib.CategoryTheory.SmallRepresentatives
CategoryTheory.CoreSmallCategoryOfSet.mk.injEq : ∀ {Ω : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (obj : Set Ω) (hom : ↑obj → ↑obj → Set Ω)
  (objEquiv : ↑obj ≃ C) (homEquiv : {X Y : ↑obj} → ↑(hom X Y) ≃ (objEquiv X ⟶ objEquiv Y)) (obj_1 : Set Ω)
  (hom_1 : ↑obj_1 → ↑obj_1 → Set Ω) (objEquiv_1 : ↑obj_1 ≃ C)
  (homEquiv_1 : {X Y : ↑obj_1} → ↑(hom_1 X Y) ≃ (objEquiv_1 X ⟶ objEquiv_1 Y)),
  ({ obj := obj, hom := hom, objEquiv := objEquiv, homEquiv := homEquiv } =
      { obj := obj_1, hom := hom_1, objEquiv := objEquiv_1, homEquiv := homEquiv_1 }) =
    (obj = obj_1 ∧ hom ≍ hom_1 ∧ objEquiv ≍ objEquiv_1 ∧ homEquiv ≍ homEquiv_1)
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.funLike : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_4} →
      {ι : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : AddCommMonoid N] →
                  [inst_5 : Module R N] → [inst_6 : TopologicalSpace N] → FunLike (M [⋀^ι]→L[R] N) (ι → M) N
-- Mathlib.Data.List.Sublists
List.range_bind_sublistsLen_perm : ∀ {α : Type u} (l : List α), (List.flatMap (fun n => List.sublistsLen n l) (List.range (l.length + 1))).Perm l.sublists'
-- Mathlib.RingTheory.Polynomial.Nilpotent
Polynomial.isNilpotent_X_mul_iff : ∀ {R : Type u_1} [inst : Semiring R] {P : Polynomial R}, IsNilpotent (Polynomial.X * P) ↔ IsNilpotent P
-- Mathlib.Order.GameAdd
/-- **Alias** of `Prod.GameAdd.recursion_eq`. -/
Prod.GameAdd.fix_eq : ∀ {α : Type u_1} {β : Type u_2} {rα : α → α → Prop} {rβ : β → β → Prop} {C : α → β → Sort u_3} (hα : WellFounded rα)
  (hβ : WellFounded rβ)
  (IH : (a₁ : α) → (b₁ : β) → ((a₂ : α) → (b₂ : β) → Prod.GameAdd rα rβ (a₂, b₂) (a₁, b₁) → C a₂ b₂) → C a₁ b₁) (a : α)
  (b : β), Prod.GameAdd.recursion hα hβ IH a b = IH a b fun a' b' x => Prod.GameAdd.recursion hα hβ IH a' b'
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.comp_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)}
  {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ D₃ : F.DescentDataAsCoalgebra f} (φ : D₁ ⟶ D₂)
  (φ' : D₂ ⟶ D₃) (i : ι) {Z : ↑(F.obj { as := Opposite.op (X i) }).obj} (h : D₃.obj i ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp φ φ').hom i) h =
    CategoryTheory.CategoryStruct.comp (φ.hom i) (CategoryTheory.CategoryStruct.comp (φ'.hom i) h)
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddHom.mem_eqLocus : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f g : M →ₙ+ N} {x : M}, x ∈ f.eqLocus g ↔ f x = g x
-- Mathlib.RingTheory.Localization.Ideal
IsLocalization.under_map_of_isPrime_disjoint : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] {I : Ideal R},
  I.IsPrime → Disjoint ↑M ↑I → Ideal.under R (Ideal.map (algebraMap R S) I) = I
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.op_inl : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (b : CategoryTheory.Limits.BinaryBicone P Q), b.op.inl = b.fst.op
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.balanced_empty : ∀ {α : Type u} {β : α → Type v}, Std.DTreeMap.Internal.Impl.empty.Balanced
-- Mathlib.Topology.Homotopy.Product
Path.Homotopic.projLeft.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {c₁ c₂ : α × β}
  (p : Path.Homotopic.Quotient c₁ c₂), Path.Homotopic.projLeft p = p.map { toFun := Prod.fst, continuous_toFun := ⋯ }
-- Lean.Compiler.IR.Basic
Lean.IR.reshape : Array Lean.IR.FnBody → Lean.IR.FnBody → Lean.IR.FnBody
-- Mathlib.Tactic.NormNum.DivMod
Mathlib.Meta.NormNum.isInt_emod_neg : ∀ {a b : ℤ} {r : ℕ}, Mathlib.Meta.NormNum.IsNat (a % -b) r → Mathlib.Meta.NormNum.IsNat (a % b) r
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get!_map : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {γ : α → Type w}
  [inst : LawfulBEq α] {f : (a : α) → β a → γ a} {k : α} [inst_1 : Inhabited (γ k)],
  (Std.ExtDHashMap.map f m).get! k = (Option.map (f k) (m.get? k)).get!
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.AbsolutelyContinuous.mutuallySingular_compProd_iff : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : MeasureTheory.Measure α}
  {κ η : ProbabilityTheory.Kernel α β} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν],
  μ.AbsolutelyContinuous ν →
    ((μ.compProd κ).MutuallySingular (ν.compProd η) ↔ (μ.compProd κ).MutuallySingular (μ.compProd η))
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.comp_φK : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {φ' : S₂ ⟶ S₃} {h₁ : S₁.LeftHomologyData}
  {h₂ : S₂.LeftHomologyData} {h₃ : S₃.LeftHomologyData} (ψ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂)
  (ψ' : CategoryTheory.ShortComplex.LeftHomologyMapData φ' h₂ h₃),
  (ψ.comp ψ').φK = CategoryTheory.CategoryStruct.comp ψ.φK ψ'.φK
-- Mathlib.Order.DirSupClosed
DirSupClosed.inter : ∀ {α : Type u_1} {s t : Set α} [inst : Preorder α], DirSupClosed s → DirSupClosed t → DirSupClosed (s ∩ t)
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
_private.Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject.0.CategoryTheory.SimplicialObject.Splitting.toNondegComplex.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Preadditive C],
  s.toNondegComplex =
    (CategoryTheory.Idempotents.fullyFaithfulToKaroubi (ChainComplex C ℕ)).preimage
      (CategoryTheory.CategoryStruct.comp { f := AlgebraicTopology.DoldKan.PInfty, comm := ⋯ }
        s.toKaroubiNondegComplexIsoN₁.inv)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ParameterInformationLabel.range : ℕ → ℕ → Lean.Lsp.ParameterInformationLabel
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mapNatIso_inverse_obj_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T T' : CategoryTheory.Functor C D} (i : T ≅ T')
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) T'),
  ((CategoryTheory.StructuredArrow.mapNatIso i).inverse.obj X).hom =
    CategoryTheory.CategoryStruct.comp X.hom (i.inv.app X.right)
-- Init.Data.String.Lemmas.Iterate
_private.Init.Data.String.Lemmas.Iterate.0.String.Model.revPositionsFrom.eq_def : ∀ {s : String} (p : s.Pos),
  String.Model.revPositionsFrom p =
    if h : p = s.startPos then [] else ⟨p.prev h, ⋯⟩ :: String.Model.revPositionsFrom (p.prev h)
-- Init.Meta.Defs
Lean.Syntax.instEmptyCollectionTSepArray : {sep : Lean.SyntaxNodeKinds} → {k : String} → EmptyCollection (Lean.Syntax.TSepArray sep k)
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.xgcdAux_fst : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] (x y s t s' t' : R),
  (EuclideanDomain.xgcdAux x s t y s' t').1 = EuclideanDomain.gcd x y
-- Init.Control.Lawful.Instances
_private.Init.Control.Lawful.Instances.0.EStateM.bind.match_1.splitter : {ε σ α : Type u_1} →
  (motive : EStateM.Result ε σ α → Sort u_2) →
    (x : EStateM.Result ε σ α) →
      ((a : α) → (s : σ) → motive (EStateM.Result.ok a s)) →
        ((e : ε) → (s : σ) → motive (EStateM.Result.error e s)) → motive x
-- Mathlib.Topology.WithTopology
WithTopology.instDecidableLT : {X : Type u_1} → (t : TopologicalSpace X) → [inst : LT X] → [DecidableLT X] → DecidableLT (WithTopology X t)
-- Mathlib.Analysis.Fourier.AddCircle
/-- The Fourier coefficients of a function on `AddCircle T` can be computed as an integral
over `[a, a + T]`, for any real `a`.  -/
fourierCoeff_eq_intervalIntegral : ∀ {T : ℝ} [hT : Fact (0 < T)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E]
  (f : AddCircle T → E) (n : ℤ) (a : ℝ), fourierCoeff f n = (1 / T) • ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • f ↑x
-- Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
CategoryTheory.Functor.imageSieve_map : ∀ {C : Type uC} [inst : CategoryTheory.Category.{vC, uC} C] {D : Type uD} [inst_1 : CategoryTheory.Category.{vD, uD} D]
  (G : CategoryTheory.Functor C D) {U V : C} (f : U ⟶ V), G.imageSieve (G.map f) = ⊤
-- Mathlib.NumberTheory.ModularForms.DedekindEta
/-- The eta function, whose value at z is `q^ 1 / 24 * ∏' 1 - q ^ (n + 1)` for `q = e ^ 2 π i z`.  -/
ModularForm.eta : ℂ → ℂ
-- Init.Data.UInt.Lemmas
USize.toFin_ofNatTruncate_of_lt : ∀ {n : ℕ} (hn : n < USize.size), (USize.ofNatClamp n).toFin = ⟨n, hn⟩
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.inverse'_inverse' : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : SMul M X] {Y : Type u_6} [inst_1 : SMul N Y]
  {φ' : N → M} {f : X →ₑ[φ] Y} {g : Y → X} {k₁ : Function.LeftInverse φ' φ} {k₂ : Function.RightInverse φ' φ}
  {h₁ : Function.LeftInverse g ⇑f} {h₂ : Function.RightInverse g ⇑f}, (f.inverse' g k₂ h₁ h₂).inverse' (⇑f) k₁ h₂ h₁ = f
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.op_sup : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S₁ S₂ : Subalgebra R A), (S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op
-- Mathlib.Algebra.Ring.Centralizer
Set.add_mem_centralizer : ∀ {M : Type u_1} {S : Set M} {a b : M} [inst : Distrib M], a ∈ S.centralizer → b ∈ S.centralizer → a + b ∈ S.centralizer
-- Mathlib.CategoryTheory.Functor.Flat
CategoryTheory.instIsCofilteredElementsCompOfRepresentablyFlat : ∀ {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] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D (Type u_4)) [CategoryTheory.RepresentablyFlat F]
  [CategoryTheory.IsCofiltered G.Elements], CategoryTheory.IsCofiltered (F.comp G).Elements
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransformMorphism.left_coherence_app_assoc : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {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}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (α : ψ ⟶ ψ') (x : A) {Z : B'}
  (h : F'.obj (ψ'.left.obj x) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso F ψ.left ψ.base F').hom.app x)
      (CategoryTheory.CategoryStruct.comp (F'.map (α.left.app x)) h) =
    CategoryTheory.CategoryStruct.comp (α.base.app (F.obj x))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso F ψ'.left ψ'.base F').hom.app x) h)
-- Init.Data.UInt.Lemmas
USize.sub_add_cancel : ∀ (a b : USize), a - b + b = a
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.WF.ofArray : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {a : Array (α × β)}, (Std.HashMap.Raw.ofArray a).WF
-- Mathlib.Algebra.Ring.Equiv
/-- A non-unital commutative ring is isomorphic to its opposite.  -/
RingEquiv.toOpposite : (R : Type u_4) → [inst : NonUnitalCommSemiring R] → R ≃+* Rᵐᵒᵖ
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.Nonempty.mul : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] {s t : Finset α}, s.Nonempty → t.Nonempty → (s * t).Nonempty
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.map_leftUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X : C),
  F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxMonoidal.δ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.OplaxMonoidal.η F) (F.obj X))
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).hom)
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.instZeroLEOneClassCastInt : ∀ {d : ℕ}, ZeroLEOneClass (ℤ√↑d)
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.instReprElimInfo : Repr Lean.Meta.ElimInfo
-- Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
GaussianInt.mod_four_eq_three_of_nat_prime_of_prime : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], Prime ↑p → p % 4 = 3
-- Mathlib.Order.WithBot
WithBot.lt_iff_exists_coe_btwn : ∀ {α : Type u_1} [inst : Preorder α] [DenselyOrdered α] [NoMinOrder α] {a b : WithBot α}, a < b ↔ ∃ x, a < ↑x ∧ ↑x < b
-- Lean.Elab.PreDefinition.Structural.Eqns
Lean.Elab.Structural.EqnInfo.declName : Lean.Elab.Structural.EqnInfo → Lean.Name
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.exactAt_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι), K.ExactAt i ↔ (K.sc i).Exact
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instBoundedOrder : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] → [inst_1 : LE β] → [BoundedOrder β] → BoundedOrder (MeasureTheory.SimpleFunc α β)
-- Lean.Parser.Term
/-- `(opt := val)` sets the `opt` configuration option to `val`.

As a special case, `(config := ...)` sets the entire configuration.
 -/
Lean.Parser.Term.valConfigItem : Lean.Parser.Parser
-- Mathlib.Data.FunLike.Equiv
/-- This lemma is only supposed to be used in the generic context, when working with instances
of classes extending `EquivLike`.
For concrete isomorphism types such as `Equiv`, you should use `Equiv.apply_symm_apply`
or its equivalent.

TODO: define a generic form of `Equiv.symm`.  -/
EquivLike.apply_inv_apply : ∀ {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [inst : EquivLike E α β] (e : E) (b : β), e (EquivLike.inv e b) = b
-- Mathlib.CategoryTheory.Products.Basic
/-- Any morphism in a product factors as a morphism whose right component is an identity
followed by a morphism whose left component is an identity.  -/
CategoryTheory.Prod.fac' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {x y : C × D} (f : x ⟶ y),
  f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Prod.mkHom f.1 (CategoryTheory.CategoryStruct.id x.2))
      (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id y.1) f.2)
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCatLeftHomologyData_descH_hom : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) {M : ModuleCat R}
  (φ : S.moduleCatLeftHomologyData.K ⟶ M) (h : CategoryTheory.CategoryStruct.comp S.moduleCatLeftHomologyData.f' φ = 0),
  ModuleCat.Hom.hom (S.moduleCatLeftHomologyData.descH φ h) =
    (ModuleCat.Hom.hom S.moduleCatLeftHomologyData.f').range.liftQ (ModuleCat.Hom.hom φ) ⋯
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionActionOfMonoidalFunctorToEndofunctorIso_inv_app_app : ∀ {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]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) [inst_3 : F.Monoidal] (X : C) (X_1 : D),
  ((CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionActionOfMonoidalFunctorToEndofunctorIso F).inv.app
          X).app
      X_1 =
    CategoryTheory.CategoryStruct.id ((F.obj X).obj X_1)