mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.smul_of_comm : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} {G' : Type u_6} [inst_3 : Group G'] [inst_4 : MulAction G' α] [MeasurableConstSMul G' α]
  [MeasureTheory.SMulInvariantMeasure G' α μ] [SMulCommClass G' G α],
  MeasureTheory.IsFundamentalDomain G s μ → ∀ (g : G'), MeasureTheory.IsFundamentalDomain G (g • s) μ
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.evaln.match_1.eq_4 : ∀ (motive : ℕ → Nat.Partrec.Code → Sort u_1) (k : ℕ) (h_1 : (x : Nat.Partrec.Code) → motive 0 x)
  (h_2 : (k : ℕ) → motive k.succ Nat.Partrec.Code.zero) (h_3 : (k : ℕ) → motive k.succ Nat.Partrec.Code.succ)
  (h_4 : (k : ℕ) → motive k.succ Nat.Partrec.Code.left) (h_5 : (k : ℕ) → motive k.succ Nat.Partrec.Code.right)
  (h_6 : (k : ℕ) → (cf cg : Nat.Partrec.Code) → motive k.succ (cf.pair cg))
  (h_7 : (k : ℕ) → (cf cg : Nat.Partrec.Code) → motive k.succ (cf.comp cg))
  (h_8 : (k : ℕ) → (cf cg : Nat.Partrec.Code) → motive k.succ (cf.prec cg))
  (h_9 : (k : ℕ) → (cf : Nat.Partrec.Code) → motive k.succ cf.rfind'),
  (match k.succ, Nat.Partrec.Code.left with
    | 0, x => h_1 x
    | k.succ, Nat.Partrec.Code.zero => h_2 k
    | k.succ, Nat.Partrec.Code.succ => h_3 k
    | k.succ, Nat.Partrec.Code.left => h_4 k
    | k.succ, Nat.Partrec.Code.right => h_5 k
    | k.succ, cf.pair cg => h_6 k cf cg
    | k.succ, cf.comp cg => h_7 k cf cg
    | k.succ, cf.prec cg => h_8 k cf cg
    | k.succ, cf.rfind' => h_9 k cf) =
    h_4 k
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.CallHierarchy.brecOn.go : {motive_1 : Lean.Lsp.Ipc.CallHierarchy → Sort u} →
  {motive_2 : Array Lean.Lsp.Ipc.CallHierarchy → Sort u} →
    {motive_3 : List Lean.Lsp.Ipc.CallHierarchy → Sort u} →
      (t : Lean.Lsp.Ipc.CallHierarchy) →
        ((t : Lean.Lsp.Ipc.CallHierarchy) → t.below → motive_1 t) →
          ((t : Array Lean.Lsp.Ipc.CallHierarchy) → Lean.Lsp.Ipc.CallHierarchy.below_1 t → motive_2 t) →
            ((t : List Lean.Lsp.Ipc.CallHierarchy) → Lean.Lsp.Ipc.CallHierarchy.below_2 t → motive_3 t) →
              motive_1 t ×' t.below
-- Mathlib.Analysis.Normed.Module.Bases
/-- Assuming that the `finrank` of the range of `P n` is `n` then the `finrank` of the range of
`succSub P n` is `1`.  -/
SchauderBasis.finrank_range_succSub_eq_one : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] {P : ℕ → X →L[𝕜] X},
  (∀ (n : ℕ), Module.finrank 𝕜 ↥(↑(P n)).range = n) →
    (∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x) →
      ∀ (n : ℕ), Module.finrank 𝕜 ↥(↑(SchauderBasis.succSub P n)).range = 1
-- Mathlib.RepresentationTheory.Coinduced
Rep.coindFunctorIso_inv_app_hom_toFun_coe : ∀ {k : Type u} {G : Type v} {H : Type w} [inst : CommRing k] [inst_1 : Monoid G] [inst_2 : Monoid H] (φ : G →* H)
  (X : Rep.{max u w, u, v} k G) (a : Rep.res φ (Rep.leftRegular k H) ⟶ X) (h : H),
  ↑((Rep.Hom.hom ((Rep.coindFunctorIso φ).inv.app X)) a) h = (Rep.Hom.hom a) (MonoidAlgebra.single h 1)
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.obj_μ_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C))
  (m₁ m₂ m₃ : M) (X : C) [inst_3 : F.Monoidal],
  (F.obj m₃).map ((CategoryTheory.Functor.LaxMonoidal.μ F m₁ m₂).app X) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.LaxMonoidal.μ F m₂ m₃).app ((F.obj m₁).obj X))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Functor.LaxMonoidal.μ F m₁ (CategoryTheory.MonoidalCategoryStruct.tensorObj m₂ m₃)).app X)
        (CategoryTheory.CategoryStruct.comp
          ((F.map (CategoryTheory.MonoidalCategoryStruct.associator m₁ m₂ m₃).inv).app X)
          ((CategoryTheory.Functor.OplaxMonoidal.δ F (CategoryTheory.MonoidalCategoryStruct.tensorObj m₁ m₂) m₃).app
            X)))
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithInitial.opEquiv.match_15.eq_1 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (x y : CategoryTheory.WithTerminal Cᵒᵖ) → (x ⟶ y) → Sort u_3) (x y : C)
  (f : CategoryTheory.WithTerminal.of (Opposite.op x) ⟶ CategoryTheory.WithTerminal.of (Opposite.op y))
  (h_1 :
    (x y : C) →
      (f : CategoryTheory.WithTerminal.of (Opposite.op x) ⟶ CategoryTheory.WithTerminal.of (Opposite.op y)) →
        motive (CategoryTheory.WithTerminal.of (Opposite.op x)) (CategoryTheory.WithTerminal.of (Opposite.op y)) f)
  (h_2 :
    (unop : C) →
      (x : CategoryTheory.WithTerminal.of (Opposite.op unop) ⟶ CategoryTheory.WithTerminal.star) →
        motive (CategoryTheory.WithTerminal.of (Opposite.op unop)) CategoryTheory.WithTerminal.star x)
  (h_3 :
    (x : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.star) →
      motive CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star x),
  (match CategoryTheory.WithTerminal.of (Opposite.op x), CategoryTheory.WithTerminal.of (Opposite.op y), f with
    | CategoryTheory.WithTerminal.of (Opposite.op x), CategoryTheory.WithTerminal.of (Opposite.op y), f => h_1 x y f
    | CategoryTheory.WithTerminal.of (Opposite.op unop), CategoryTheory.WithTerminal.star, x => h_2 unop x
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => h_3 x) =
    h_1 x y f
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.orthogonalProjectionOnto_eq_sum_rankOne : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] {U : Submodule 𝕜 E} [inst_4 : U.HasOrthogonalProjection]
  (b : OrthonormalBasis ι 𝕜 ↥U), U.orthogonalProjectionOnto = ∑ i, ((InnerProductSpace.rankOne 𝕜) (b i)) ↑(b i)
-- Lean.Data.Position
_private.Lean.Data.Position.0.Lean.FileMap.toPosition.loop : Lean.FileMap → String.Pos.Raw → String → Array String.Pos.Raw → ℕ → ℕ → Lean.Position
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- **Alias** of the reverse direction of `differentiableAt_add_const_iff`. -/
DifferentiableAt.add_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} (c : F), DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 (fun y => f y + c) x
-- Init.Data.Rat.Lemmas
Rat.mkRat_mul_mkRat : ∀ (n₁ n₂ : ℤ) (d₁ d₂ : ℕ), mkRat n₁ d₁ * mkRat n₂ d₂ = mkRat (n₁ * n₂) (d₁ * d₂)
-- Mathlib.Algebra.Homology.HomotopyCategory.KProjective
CochainComplex.instIsKProjectiveObjIntShiftFunctor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (K : CochainComplex C ℤ) [hK : K.IsKProjective] (n : ℤ),
  ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).IsKProjective
-- Mathlib.Control.Functor
/-- `AddConst.mk` is the canonical map `α → AddConst α β`, which is the identity,
where `AddConst α β = Const α β`. It can be used as a pattern to extract this value.  -/
Functor.AddConst.mk : {α : Type u_1} → {β : Type u_2} → α → Functor.AddConst α β
-- Mathlib.RingTheory.WittVector.FrobeniusFractionField
WittVector.RecursionMain.root_exists : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : Field k] [inst_1 : CharP k p] [IsAlgClosed k] (n : ℕ)
  (a₁ a₂ : WittVector p k) (bs : Fin (n + 1) → k),
  a₁.coeff 0 ≠ 0 → a₂.coeff 0 ≠ 0 → ∃ b, (WittVector.RecursionMain.succNthDefiningPoly p n a₁ a₂ bs).IsRoot b
-- Mathlib.Data.PNat.Factors
/-- Converts a `PrimeMultiset` to a `Multiset ℕ+`.  -/
PrimeMultiset.toPNatMultiset : PrimeMultiset → Multiset ℕ+
-- Mathlib.CategoryTheory.Groupoid.Grpd.Basic
CategoryTheory.Grpd.forgetToCat_faithful : CategoryTheory.Grpd.forgetToCat.Faithful
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_mul_right_Ioc : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {c : G₀} (a b : G₀),
  0 < c → (fun x => x * c) '' Set.Ioc a b = Set.Ioc (a * c) (b * c)
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctor.id_mapComp_hom : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  ((CategoryTheory.StrictlyUnitaryPseudofunctor.id B).mapComp f g).hom =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- The supremum of two finite-dimensional affine subspaces is finite-dimensional.  -/
AffineSubspace.finiteDimensional_sup : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (s₁ s₂ : AffineSubspace k P) [FiniteDimensional k ↥s₁.direction]
  [FiniteDimensional k ↥s₂.direction], FiniteDimensional k ↥(s₁ ⊔ s₂).direction
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.equivQuotientZSMulOfEquiv.eq_1 : ∀ {A B : Type u} [inst : AddCommGroup A] [inst_1 : AddCommGroup B] (e : A ≃+ B) (n : ℤ),
  QuotientAddGroup.equivQuotientZSMulOfEquiv e n =
    (QuotientAddGroup.homQuotientZSMulOfHom (↑e) n).toAddEquiv (QuotientAddGroup.homQuotientZSMulOfHom (↑e.symm) n) ⋯ ⋯
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.sum_tmul : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {α : Type u_22} (s : Finset α) (m : α → M)
  (n : N), (∑ a ∈ s, m a) ⊗ₜ[R] n = ∑ a ∈ s, m a ⊗ₜ[R] n
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.contains_filterMap : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w}
  [inst : LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α},
  (Std.DHashMap.filterMap f m).contains k = Option.any (fun x => (f k x).isSome) (m.get? k)
-- Mathlib.Order.CompleteBooleanAlgebra
/-- The `Order.Coframe.MinimalAxioms` element corresponding to a frame.  -/
Order.Coframe.MinimalAxioms.of : ∀ {α : Type u} [inst : Order.Coframe α], Order.Coframe.MinimalAxioms α
-- Mathlib.Combinatorics.Matroid.Basic
/-- Typeclass for a matroid having finite ground set. Just a wrapper for `M.E.Finite`.  -/
Matroid.Finite : {α : Type u_1} → Matroid α → Prop
-- Mathlib.Data.Nat.Hyperoperation
_private.Mathlib.Data.Nat.Hyperoperation.0.hyperoperation.match_1.splitter : (motive : ℕ → ℕ → ℕ → Sort u_1) →
  (x x_1 x_2 : ℕ) →
    ((x k : ℕ) → motive 0 x k) →
      ((m : ℕ) → motive 1 m 0) →
        ((x : ℕ) → motive 2 x 0) →
          ((n x : ℕ) → motive n.succ.succ.succ x 0) → ((n m k : ℕ) → motive n.succ m k.succ) → motive x x_1 x_2
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.comap_obj_addMod : ∀ {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.MonoidalLeftAction C D]
  {A B : C} [inst_4 : CategoryTheory.AddMonObj A] [inst_5 : CategoryTheory.AddMonObj B] (f : A ⟶ B)
  [inst_6 : CategoryTheory.IsAddMonHom f] (M : CategoryTheory.AddMod D B),
  ((CategoryTheory.AddMod.comap f).obj M).addMod = CategoryTheory.AddMod.scalarRestriction f M.X
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.instNeg : {K : Type u} → [inst : CommRing K] → Neg (RatFunc K)
-- Mathlib.RingTheory.PolynomialLaw.Basic
/-- For semirings in the universe `u`, `PolynomialLaw.toFun` coincides
with `PolynomialLaw.toFun'`.  -/
PolynomialLaw.toFun'_eq_toFun : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_2}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (f : M →ₚₗ[R] N) (S : Type u) [inst_5 : CommSemiring S]
  [inst_6 : Algebra R S], f.toFun' S = PolynomialLaw.toFun S f
-- Mathlib.CategoryTheory.Adjunction.Comma
/-- If each costructured arrow category on `G` has a terminal object, `G` is a left adjoint.  -/
CategoryTheory.isLeftAdjoint_of_costructuredArrowTerminals : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor D C)
  [∀ (A : C), CategoryTheory.Limits.HasTerminal (CategoryTheory.CostructuredArrow G A)], G.IsLeftAdjoint
-- Mathlib.RepresentationTheory.Coinvariants
Rep.instLinearModuleCatObjFunctorCoinvariantsTensor : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] (A : Rep.{u, u, v} k G),
  CategoryTheory.Functor.Linear k ((Rep.coinvariantsTensor k G).obj A)
-- Mathlib.Algebra.Order.Round
abs_sub_round : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] (x : α),
  |x - ↑(round x)| ≤ 1 / 2
-- Mathlib.CategoryTheory.Core
CategoryTheory.Core.forgetFunctorToCore_map_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : Type u₂} [inst_1 : CategoryTheory.Groupoid G]
  {X Y : CategoryTheory.Functor G (CategoryTheory.Core C)} (α : X ⟶ Y) (X_1 : G),
  (CategoryTheory.Core.forgetFunctorToCore.map α).app X_1 = (α.app X_1).iso.hom
-- Mathlib.Topology.Maps.Proper.Basic
/-- An injective and continuous function is proper if and only if it is closed.  -/
isProperMap_iff_isClosedMap_of_inj : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f → Function.Injective f → (IsProperMap f ↔ IsClosedMap f)
-- Mathlib.CategoryTheory.GradedObject.Braiding
CategoryTheory.GradedObject.Monoidal.hexagon_forward : ∀ {I : Type u_1} [inst : AddCommMonoid I] {C : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X Y Z : CategoryTheory.GradedObject I C)
  [inst_3 : CategoryTheory.BraidedCategory C] [inst_4 : X.HasTensor Y] [inst_5 : Y.HasTensor X] [inst_6 : Y.HasTensor Z]
  [inst_7 : Z.HasTensor X] [inst_8 : X.HasTensor Z]
  [inst_9 : (CategoryTheory.GradedObject.Monoidal.tensorObj X Y).HasTensor Z]
  [inst_10 : X.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj Y Z)]
  [inst_11 : (CategoryTheory.GradedObject.Monoidal.tensorObj Y Z).HasTensor X]
  [inst_12 : Y.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj Z X)]
  [inst_13 : (CategoryTheory.GradedObject.Monoidal.tensorObj Y X).HasTensor Z]
  [inst_14 : Y.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X Z)] [inst_15 : X.HasGoodTensor₁₂Tensor Y Z]
  [inst_16 : X.HasGoodTensorTensor₂₃ Y Z] [inst_17 : Y.HasGoodTensor₁₂Tensor Z X]
  [inst_18 : Y.HasGoodTensorTensor₂₃ Z X] [inst_19 : Y.HasGoodTensor₁₂Tensor X Z]
  [inst_20 : Y.HasGoodTensorTensor₂₃ X Z],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.associator X Y Z).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.GradedObject.Monoidal.braiding X (CategoryTheory.GradedObject.Monoidal.tensorObj Y Z)).hom
        (CategoryTheory.GradedObject.Monoidal.associator Y Z X).hom) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.Monoidal.whiskerRight (CategoryTheory.GradedObject.Monoidal.braiding X Y).hom Z)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.associator Y X Z).hom
        (CategoryTheory.GradedObject.Monoidal.whiskerLeft Y (CategoryTheory.GradedObject.Monoidal.braiding X Z).hom))
-- Init.Data.Order.Ord
Bool.instTransOrd : Std.TransOrd Bool
-- Lean.Parser.Term
Lean.Parser.Term.depArrow.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Combinatorics.Hindman
/-- Constructor for `FP`. This is the preferred spelling over `FP.head'`.  -/
Hindman.FP.head : ∀ {M : Type u_1} [inst : Semigroup M] (a : Stream' M), a.head ∈ Hindman.FP a
-- Mathlib.Algebra.Star.MonoidHom
/-- `α →⋆* β` denotes the type of star monoid homomorphisms from `α` to `β`.  -/
«term_→⋆*_» : Lean.TrailingParserDescr
-- Init.Prelude
/-- The Boolean value `true`, not to be confused with the proposition `True`.  -/
Bool.true : Bool
-- Mathlib.Algebra.Field.Opposite
AddOpposite.unop_ratCast : ∀ {α : Type u_1} [inst : RatCast α] (q : ℚ), AddOpposite.unop ↑q = ↑q
-- Mathlib.Data.Quot
Quotient.out_eq' : ∀ {α : Sort u_1} {s₁ : Setoid α} (q : Quotient s₁), Quotient.mk'' q.out = q
-- Aesop.RuleSet.Member
Aesop.GlobalRuleSetMember.normSimpRule.sizeOf_spec : ∀ (e : Aesop.NormSimpRule), sizeOf (Aesop.GlobalRuleSetMember.normSimpRule e) = 1 + sizeOf e
-- Init.Data.Range.Polymorphic.PRange
Std.instDecidableEqRio : {α : Type u_1} → [DecidableEq α] → DecidableEq (Std.Rio α)
-- Mathlib.Algebra.Module.Submodule.RestrictScalars
Submodule.isCompl_restrictScalars_iff : ∀ (S : Type u_1) {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Semiring S]
  [inst_3 : Module S M] [inst_4 : Module R M] [inst_5 : SMul S R] [inst_6 : IsScalarTower S R M] {s t : Submodule R M},
  IsCompl (Submodule.restrictScalars S s) (Submodule.restrictScalars S t) ↔ IsCompl s t
-- Mathlib.Topology.MetricSpace.Similarity
/-- Change between equivalent index sets ι and ι'.  -/
Similar.index_equiv : ∀ {ι : Type u_1} {ι' : Type u_2} {P₁ : Type u_3} {P₂ : Type u_4} [inst : PseudoEMetricSpace P₁]
  [inst_1 : PseudoEMetricSpace P₂] (f : ι' ≃ ι) (v₁ : ι → P₁) (v₂ : ι → P₂), Similar (v₁ ∘ ⇑f) (v₂ ∘ ⇑f) ↔ Similar v₁ v₂
-- Batteries.Data.List.Lemmas
List.countPBefore.go.eq_2 : ∀ {α : Type u_1} (p : α → Bool) (s : ℕ) (a : α) (xs_1 : List α) (i_1 : ℕ),
  List.countPBefore.go p (a :: xs_1) i_1.succ s =
    bif p a then List.countPBefore.go p xs_1 i_1 (s + 1) else List.countPBefore.go p xs_1 i_1 s
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
CategoryTheory.ProjectiveResolution.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} [inst_3 : SizeOf C] (complex : ChainComplex C ℕ)
  (projective :
    autoParam (∀ (n : ℕ), CategoryTheory.Projective (complex.X n))
      CategoryTheory.ProjectiveResolution.projective._autoParam)
  [hasHomology : ∀ (i : ℕ), HomologicalComplex.HasHomology complex i] (π : complex ⟶ (ChainComplex.single₀ C).obj Z)
  (quasiIso : autoParam (QuasiIso π) CategoryTheory.ProjectiveResolution.quasiIso._autoParam),
  sizeOf { complex := complex, projective := projective, hasHomology := hasHomology, π := π, quasiIso := quasiIso } =
    1 + sizeOf complex + sizeOf π + sizeOf quasiIso
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normal_le_normalCore : ∀ {G : Type u_1} [inst : AddGroup G] {H N : AddSubgroup G} [hN : N.Normal], N ≤ H.normalCore ↔ N ≤ H
-- Mathlib.Tactic.CrossRefAttribute
/-- A lowercase short name for the given database. Useful when exporting to JSON.  -/
Mathlib.CrossRef.Database.shortName : Mathlib.CrossRef.Database → String
-- Mathlib.Algebra.Category.Grp.Limits
/-- If `J` is `u`-small, `CommGrpCat.{u}` has limits of shape `J`.  -/
CommGrpCat.hasLimitsOfShape : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] [Small.{u, v} J],
  CategoryTheory.Limits.HasLimitsOfShape J CommGrpCat
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Set.subgroupClosure_mul : ∀ {G : Type u_2} [inst : Group G] {s : Set G}, s.Nonempty → ↑(Subgroup.closure s) * s = ↑(Subgroup.closure s)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_diff_add_size_inter_eq_size_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → (m₁ \ m₂).size + (m₁ ∩ m₂).size = m₁.size
-- Mathlib.Order.GaloisConnection.Defs
/-- Make a `GaloisInsertion` between `αᵒᵈ` and `βᵒᵈ` from a `GaloisCoinsertion` between `α` and
`β`.  -/
GaloisCoinsertion.dual : {α : Type u} →
  {β : Type v} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        {l : α → β} →
          {u : β → α} →
            GaloisCoinsertion l u →
              GaloisInsertion (⇑OrderDual.toDual ∘ u ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ l ∘ ⇑OrderDual.ofDual)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct
SSet.anodyneExtensions_unionProd_ι' : ∀ {X Y : SSet} (A : X.Subcomplex) (B : Y.Subcomplex),
  SSet.anodyneExtensions A.ι → SSet.anodyneExtensions (A.unionProd B).ι
-- Lean.Meta.Hint
/-- Produces a diff that splits either on characters, tokens, or not at all, depending on the selected
`diffMode`.

Guarantees that all actions in the output will be maximally grouped; that is, instead of returning
`#[(.insert, "a"), (.insert, "b")]`, it will return `#[(.insert, "ab")]`.
 -/
Lean.Meta.Hint.readableDiff : String →
  String →
    optParam Lean.Meta.Hint.DiffGranularity Lean.Meta.Hint.DiffGranularity.auto → Array (Lean.Diff.Action × String)
-- Lean.Parser.Types
Lean.Parser.Error.expected : Lean.Parser.Error → List String
-- Mathlib.Tactic.Clear_
/-- Clear all hypotheses starting with `_`, like `_match` and `_let_match`.  -/
Mathlib.Tactic.clear_ : Lean.ParserDescr
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
/-- When `β` has a top element, `conditional β` is given by limits over finite intervals
`{y | x ≤ y}` as `x → atBot`.  -/
SummationFilter.conditional_filter_eq_map_Ici : ∀ {γ : Type u_4} [inst : PartialOrder γ] [inst_1 : LocallyFiniteOrder γ] [inst_2 : OrderTop γ],
  (SummationFilter.conditional γ).filter = Filter.map Finset.Ici Filter.atBot
-- Init.Prelude
/-- Converts a 32-bit unsigned integer to an arbitrary-precision natural number.

This function is overridden at runtime with an efficient implementation.
 -/
UInt32.toNat : UInt32 → ℕ
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.OuterMeasure.null_of_trim_null : ∀ {α : Type u_1} [inst : MeasurableSpace α] (m : MeasureTheory.OuterMeasure α) {s : Set α}, m.trim s = 0 → m s = 0
-- Lean.Data.JsonRpc
Lean.JsonRpc.instBEqResponse.beq : {α : Type u_1} → [BEq α] → Lean.JsonRpc.Response α → Lean.JsonRpc.Response α → Bool
-- Mathlib.Logic.Equiv.Set
Equiv.prod_assoc_preimage : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} {s : Set α} {t : Set β} {u : Set γ},
  ⇑(Equiv.prodAssoc α β γ) ⁻¹' s ×ˢ t ×ˢ u = (s ×ˢ t) ×ˢ u
-- Mathlib.Algebra.Lie.Ideal
LieHom.IsIdealMorphism.eq : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] {f : L →ₗ⁅R⁆ L'},
  f.IsIdealMorphism → LieIdeal.toLieSubalgebra R L' f.idealRange = f.range
-- Mathlib.Algebra.Group.Basic
eq_inv_of_mul_eq_one_right : ∀ {α : Type u_1} [inst : DivisionMonoid α] {a b : α}, a * b = 1 → b = a⁻¹
-- Mathlib.Data.ENat.Lattice
ENat.iInf_add : ∀ {ι : Sort u_2} {f : ι → ℕ∞} {a : ℕ∞}, iInf f + a = ⨅ i, f i + a
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- We can map monomorphisms over `X` to monomorphisms over `Y`
by post-composition with a monomorphism `f : X ⟶ Y`.
 -/
CategoryTheory.MonoOver.map : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      (f : X ⟶ Y) →
        [CategoryTheory.Mono f] → CategoryTheory.Functor (CategoryTheory.MonoOver X) (CategoryTheory.MonoOver Y)
-- Mathlib.CategoryTheory.Monoidal.Closed.Functor
/-- If `F` is full and faithful and has a left adjoint `L` which preserves binary products, then the
Frobenius morphism is an isomorphism.
 -/
CategoryTheory.frobeniusMorphism_iso_of_preserves_binary_products : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v, u'} D]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) {L : CategoryTheory.Functor D C} (h : L ⊣ F) (A : C)
  [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) L] [F.Full]
  [F.Faithful], CategoryTheory.IsIso (CategoryTheory.frobeniusMorphism F h A).natTrans