mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.CatCommSq
/-- Horizontal composition of 2-commutative squares  -/
CategoryTheory.CatCommSq.hComp : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        {C₅ : Type u_5} →
          {C₆ : Type u_6} →
            [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
              [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
                [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
                  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                    [inst_4 : CategoryTheory.Category.{v_5, u_5} C₅] →
                      [inst_5 : CategoryTheory.Category.{v_6, u_6} C₆] →
                        (T₁ : CategoryTheory.Functor C₁ C₂) →
                          (T₂ : CategoryTheory.Functor C₂ C₃) →
                            (V₁ : CategoryTheory.Functor C₁ C₄) →
                              (V₂ : CategoryTheory.Functor C₂ C₅) →
                                (V₃ : CategoryTheory.Functor C₃ C₆) →
                                  (B₁ : CategoryTheory.Functor C₄ C₅) →
                                    (B₂ : CategoryTheory.Functor C₅ C₆) →
                                      [CategoryTheory.CatCommSq T₁ V₁ V₂ B₁] →
                                        [CategoryTheory.CatCommSq T₂ V₂ V₃ B₂] →
                                          CategoryTheory.CatCommSq (T₁.comp T₂) V₁ V₃ (B₁.comp B₂)
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.rat_inf_continuous_lemma : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {ε a₁ a₂ b₁ b₂ : α},
  |a₁ - b₁| < ε → |a₂ - b₂| < ε → |min a₁ a₂ - min b₁ b₂| < ε
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
/-- Partner function to `reduceCyclically`.
See `reduceCyclically.conj_conjugator_reduceCyclically`.  -/
FreeGroup.reduceCyclically.conjugator : {α : Type u} → [DecidableEq α] → List (α × Bool) → List (α × Bool)
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.asHom_injective : ∀ {G : AddCommGrpCat}, Function.Injective AddCommGrpCat.asHom
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instMonoid : {α : Type u_1} → [Monoid α] → Monoid (Colex α)
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} (α β : X ⟶ Y)
  (w : α.hom.base = β.hom.base),
  CategoryTheory.CategoryStruct.comp α.hom.c
        (CategoryTheory.Functor.whiskerRight (CategoryTheory.eqToHom ⋯) X.presheaf) =
      β.hom.c →
    α = β
-- Lean.Expr
Lean.FVarId.mk : Lean.Name → Lean.FVarId
-- Mathlib.Analysis.Normed.Module.Connected
Metric.contractibleSpace_closedBall : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ℝ},
  0 ≤ r → ContractibleSpace ↑(Metric.closedBall x r)
-- Mathlib.Data.Int.Interval
Int.card_Icc_of_le : ∀ (a b : ℤ), a ≤ b + 1 → ↑(Finset.Icc a b).card = b + 1 - a
-- Mathlib.CategoryTheory.Abelian.Opposite
CategoryTheory.imageUnopOp.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {A B : Cᵒᵖ}
  (g : A ⟶ B),
  CategoryTheory.imageUnopOp g =
    (CategoryTheory.Abelian.imageIsoImage g.unop).op ≪≫
      (CategoryTheory.cokernelOpOp (CategoryTheory.Limits.cokernel.π g.unop)).symm ≪≫
        CategoryTheory.Limits.cokernelIsoOfEq ⋯ ≪≫
          CategoryTheory.Limits.cokernelEpiComp (CategoryTheory.cokernelUnopOp g).hom
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) (CategoryTheory.eqToHom ⋯)) ≪≫
            CategoryTheory.Limits.cokernelCompIsIso (CategoryTheory.Limits.kernel.ι g) (CategoryTheory.eqToHom ⋯) ≪≫
              CategoryTheory.Abelian.coimageIsoImage' g
-- Mathlib.Data.Vector.Basic
List.Vector.mOfFn.eq_def : ∀ {m : Type u → Type u_6} [inst : Monad m] {α : Type u} (x : ℕ) (x_1 : Fin x → m α),
  List.Vector.mOfFn x_1 =
    match x, x_1 with
    | 0, x => pure List.Vector.nil
    | n.succ, f => do
      let a ← f 0
      let v ← List.Vector.mOfFn fun i => f i.succ
      pure (a ::ᵥ v)
-- Mathlib.Data.Fintype.Quotient
/-- Recursion principle for `Trunc`s indexed by a finite type.  -/
Trunc.finRecOn : {ι : Type u_1} →
  [DecidableEq ι] →
    [Fintype ι] →
      {α : ι → Sort u_2} →
        {C : ((i : ι) → Trunc (α i)) → Sort u_4} →
          (q : (i : ι) → Trunc (α i)) →
            (f : (a : (i : ι) → α i) → C fun x => Trunc.mk (a x)) → (∀ (a b : (i : ι) → α i), ⋯ ▸ f a = f b) → C q
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.Batteries.AssocList.forIn.match_1.eq_2 : ∀ {δ : Type u_1} (motive : ForInStep δ → Sort u_2) (d : δ) (h_1 : (d : δ) → motive (ForInStep.done d))
  (h_2 : (d : δ) → motive (ForInStep.yield d)),
  (match ForInStep.yield d with
    | ForInStep.done d => h_1 d
    | ForInStep.yield d => h_2 d) =
    h_2 d
-- Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
Set.Subsingleton.measure_zero : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α},
  s.Subsingleton → ∀ (μ : MeasureTheory.Measure α) [MeasureTheory.NullSingletonClass μ], μ s = 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.polynomialY.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve.Affine R),
  W.polynomialY =
    Polynomial.C (Polynomial.C 2) * Polynomial.X + Polynomial.C (Polynomial.C W.a₁ * Polynomial.X + Polynomial.C W.a₃)
-- Mathlib.NumberTheory.RamificationInertia.Basic
Ideal.inertiaDeg_le_finrank : ∀ {R : Type u} [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsDedekindDomain S]
  (K : Type u_1) (L : Type u_2) [inst_4 : Field K] [inst_5 : Field L] [IsDedekindDomain R] [inst_7 : Algebra R K]
  [IsFractionRing R K] [inst_9 : Algebra S L] [IsFractionRing S L] [inst_11 : Algebra K L] [inst_12 : Algebra R L]
  [IsScalarTower R S L] [IsScalarTower R K L] [Module.Finite R S] [NoZeroSMulDivisors R S] {p : Ideal R} [p.IsMaximal]
  (P : Ideal S) [hP₁ : P.IsPrime] [hP₂ : P.LiesOver p], p ≠ ⊥ → p.inertiaDeg' P ≤ Module.finrank K L
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whiskerLeft_inv_hom : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f η.inv)
      (CategoryTheory.Bicategory.whiskerLeft f η.hom) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Order.DirectedInverseSystem
InverseSystem.map_self : ∀ {ι : Type u_1} {inst : Preorder ι} {F : ι → Type u_4} {f : ⦃i j : ι⦄ → i ≤ j → F j → F i} [self : InverseSystem f]
  ⦃i : ι⦄ (x : F i), f ⋯ x = x
-- Mathlib.Algebra.BigOperators.Finprod
/-- Given a monoid homomorphism `g : M →* N` and a function `f : α → M`, the value of `g` at the
product of `f i` over `i ∈ s` equals the product of `g (f i)` over `s`.  -/
MonoidHom.map_finprod_mem : ∀ {α : Type u_1} {M : Type u_5} {N : Type u_6} [inst : CommMonoid M] [inst_1 : CommMonoid N] {s : Set α} (f : α → M)
  (g : M →* N), s.Finite → g (∏ᶠ (j : α) (_ : j ∈ s), f j) = ∏ᶠ (i : α) (_ : i ∈ s), g (f i)
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.orImpL.injEq : ∀ (p p_1 : Mathlib.Tactic.ITauto.Proof), (p.orImpL = p_1.orImpL) = (p = p_1)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} {h_mem : k ∈ t₁ \ t₂}, (t₁ \ t₂)[k] = t₁[k]
-- Lean.Language.Basic
Lean.Language.SnapshotLeaf.mk.inj : ∀ {toSnapshot toSnapshot_1 : Lean.Language.Snapshot},
  { toSnapshot := toSnapshot } = { toSnapshot := toSnapshot_1 } → toSnapshot = toSnapshot_1
-- Mathlib.LinearAlgebra.Projection
LinearMap.IsProj.codRestrict_ker : ∀ {S : Type u_5} [inst : Semiring S] {M : Type u_6} [inst_1 : AddCommMonoid M] [inst_2 : Module S M] {m : Submodule S M}
  {f : M →ₗ[S] M} (h : LinearMap.IsProj m f), h.codRestrict.ker = f.ker
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
NumberField.Units.dirichletUnitTheorem.unitLattice_inter_ball_finite : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (r : ℝ),
  (↑(NumberField.Units.unitLattice K) ∩ Metric.closedBall 0 r).Finite
-- Mathlib.GroupTheory.RegularWreathProduct
IteratedWreathProduct.card : ∀ (G : Type u) (n : ℕ) [Finite G],
  Nat.card (IteratedWreathProduct G n) = Nat.card G ^ ∑ i ∈ Finset.range n, Nat.card G ^ i
-- Mathlib.GroupTheory.NoncommCoprod
AddMonoidHom.noncommCoprod_unique : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] [inst_2 : AddMonoid P]
  (f : M × N →+ P), (f.comp (AddMonoidHom.inl M N)).noncommCoprod (f.comp (AddMonoidHom.inr M N)) ⋯ = f
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instAddGroupWithOne : {n : Type u_2} → {A : Type u_5} → [DecidableEq n] → [AddGroupWithOne A] → AddGroupWithOne (CStarMatrix n n A)
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- For any `σ : X ⟶ Y` between `StrictSegal` simplicial sets, `spineToSimplex`
commutes with `Path.map`.  -/
SSet.StrictSegal.spineToSimplex_map : ∀ {X Y : SSet} (sx : X.StrictSegal) (sy : Y.StrictSegal) {n : ℕ} (f : X.Path (n + 1)) (σ : X ⟶ Y),
  sy.spineToSimplex (f.map σ) =
    (CategoryTheory.ConcreteCategory.hom (σ.app (Opposite.op { len := n + 1 }))) (sx.spineToSimplex f)
-- Mathlib.NumberTheory.ClassNumber.Finite
/-- A nonzero ideal has an element of minimal norm.  -/
ClassGroup.exists_min : ∀ {R : Type u_1} {S : Type u_2} [inst : EuclideanDomain R] [inst_1 : CommRing S] [IsDomain S] [inst_3 : Algebra R S]
  (abv : AbsoluteValue R ℤ) (I : ↥(nonZeroDivisors (Ideal S))),
  ∃ b ∈ ↑I, b ≠ 0 ∧ ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0
-- Init.Data.String.Lemmas.Pattern.Find.Pred
String.contains_prop_eq : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String}, s.contains p = s.toList.any fun b => decide (p b)
-- Init.Core
/-- The second component of a dependent pair. Its type depends on the first component.
 -/
Sigma.snd : {α : Type u} → {β : α → Type v} → (self : Sigma β) → β self.fst
-- Lean.Meta.Tactic.Grind.AC.Seq
Lean.Grind.AC.SubsetResult.false.sizeOf_spec : sizeOf Lean.Grind.AC.SubsetResult.false = 1
-- Mathlib.Analysis.Analytic.CPolynomial
ContinuousMultilinearMap.analyticOn_uncurry_of_linear : ∀ {𝕜 : Type u_1} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {ι : Type u_5}
  {Em : ι → Type u_6} [inst_5 : (i : ι) → NormedAddCommGroup (Em i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (Em i)]
  [inst_7 : Fintype ι] (f : ContinuousMultilinearMap 𝕜 Em (G →L[𝕜] F)) {s : Set (((i : ι) → Em i) × G)},
  AnalyticOn 𝕜 (fun p => (f p.1) p.2) s
-- Mathlib.Data.Nat.Init
Nat.AtLeastTwo.prop : ∀ {n : ℕ} [self : n.AtLeastTwo], 2 ≤ n
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
CFC.eq_zero_of_spectrum_subset_zero : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (a : A),
  spectrum R a ⊆ {0} → autoParam (p a) CFC.eq_zero_of_spectrum_subset_zero._auto_1 → a = 0
-- Mathlib.MeasureTheory.Measure.Regular
MeasurableSet.exists_isOpen_sdiff_lt : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α] [μ.OuterRegular]
  {A : Set α}, MeasurableSet A → μ A ≠ ⊤ → ∀ {ε : ENNReal}, ε ≠ 0 → ∃ U ⊇ A, IsOpen U ∧ μ U < ⊤ ∧ μ (U \ A) < ε
-- Mathlib.RingTheory.IsTensorProduct
Algebra.IsPushout.equiv_symm_algebraMap_right : ∀ (R : Type u_1) (S : Type v₃) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (R' : Type u_6)
  (S' : Type u_7) [inst_3 : CommSemiring R'] [inst_4 : CommSemiring S'] [inst_5 : Algebra R R'] [inst_6 : Algebra S S']
  [inst_7 : Algebra R' S'] [inst_8 : Algebra R S'] [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S']
  [inst_11 : Algebra.IsPushout R S R' S'] (a : R'),
  (Algebra.IsPushout.equiv R S R' S').symm ((algebraMap R' S') a) = 1 ⊗ₜ[R] a
-- Aesop.Tree.ExtractScript
Aesop.ExtractScript.lazyStepToStep : Aesop.DisplayRuleName → Aesop.Script.LazyStep → Lean.MetaM Aesop.Script.Step
-- Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
/-- An element of the character space, as a non-unital algebra homomorphism.  -/
WeakDual.CharacterSpace.toNonUnitalAlgHom : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring 𝕜] →
      [inst_1 : TopologicalSpace 𝕜] →
        [inst_2 : ContinuousAdd 𝕜] →
          [inst_3 : ContinuousConstSMul 𝕜 𝕜] →
            [inst_4 : NonUnitalNonAssocSemiring A] →
              [inst_5 : TopologicalSpace A] → [inst_6 : Module 𝕜 A] → ↑(WeakDual.characterSpace 𝕜 A) → A →ₙₐ[𝕜] 𝕜
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.HasSubgaussianMGF.memLp_exp_mul : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c : NNReal},
  ProbabilityTheory.HasSubgaussianMGF X c μ →
    ∀ (t : ℝ) (p : NNReal), MeasureTheory.MemLp (fun ω => Real.exp (t * X ω)) (↑p) μ
-- Mathlib.CategoryTheory.CofilteredSystem
/-- The eventual range of the functor `F : J ⥤ Type v` at index `j : J` is the intersection
of the ranges of all maps `F.map f` with `i : J` and `f : i ⟶ j`.  -/
CategoryTheory.Functor.eventualRange : {J : Type u} →
  [inst : CategoryTheory.Category.{v_1, u} J] →
    (F : CategoryTheory.Functor J (Type v)) → (j : J) → Set ((fun X => X) (F.obj j))
-- Lean.DocString.Add
/-- Interprets a docstring that has been saved as a Markdown string as Verso, elaborating it. This is
used during bootstrapping.
 -/
Lean.makeDocStringVerso : Lean.Name → Lean.Elab.TermElabM Unit
-- Aesop.Frontend.Extension.Init
Aesop.instInhabitedDeclaredRuleSets : Inhabited Aesop.DeclaredRuleSets
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- Given a finite set of accessible `Λ` machine states, there is a finite set of accessible
machine states in the target (even though the type `Λ'` is infinite).  -/
Turing.TM1to0.trStmts : {Γ : Type u_1} →
  {Λ : Type u_2} →
    {σ : Type u_3} → (M : Λ → Turing.TM1.Stmt Γ Λ σ) → [Fintype σ] → Finset Λ → Finset (Turing.TM1to0.Λ' M)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_one_of_mul_lt_right : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : LT α] [MulLeftReflectLT α] {a b : α}, a * b < a → b < 1
-- Mathlib.GroupTheory.Focal
AddSubgroup.transferFocal.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [inst_1 : H.FiniteIndex],
  H.transferFocal = (QuotientAddGroup.mk' H.focalAddSubgroupOf).transfer
-- Mathlib.Data.Nat.Choose.Basic
Nat.ascFactorial_eq_factorial_mul_choose : ∀ (n k : ℕ), (n + 1).ascFactorial k = k.factorial * (n + k).choose k
-- Mathlib.SetTheory.Cardinal.Order
/-- **König's theorem**  -/
Cardinal.sum_lt_prod : ∀ {ι : Type u_1} (f g : ι → Cardinal.{u_2}), (∀ (i : ι), f i < g i) → Cardinal.sum f < Cardinal.prod g
-- Mathlib.MeasureTheory.Integral.Bochner.Set
/-- **Inclusion-exclusion principle** for the integral of a function over a union.

The integral of a function `f` over the union of the `s i` over `i ∈ t` is the alternating sum of
the integrals of `f` over the intersections of the `s i`.  -/
MeasureTheory.integral_biUnion_eq_sum_powerset : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {μ : MeasureTheory.Measure X} {ι : Type u_5} {t : Finset ι} {s : ι → Set X},
  (∀ i ∈ t, MeasurableSet (s i)) →
    (∀ i ∈ t, MeasureTheory.IntegrableOn f (s i) μ) →
      ∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ =
        ∑ u ∈ t.powerset with u.Nonempty, (-1) ^ (u.card + 1) • ∫ (x : X) in ⋂ i ∈ u, s i, f x ∂μ
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.IsUltra.mk : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero R] [inst_1 : Add R] [inst_2 : LE R] [inst_3 : Max R]
  {d : PseudoMetric X R}, (∀ (x y z : X), d x z ≤ d x y ⊔ d y z) → d.IsUltra
-- Mathlib.Algebra.Field.Opposite
MulOpposite.instRatCast.eq_1 : ∀ {α : Type u_1} [inst : RatCast α], MulOpposite.instRatCast = { ratCast := fun q => MulOpposite.op ↑q }
-- Mathlib.LinearAlgebra.FreeModule.Int
/-- Given a submodule `N` in Smith normal form of a free `R`-module, its index as an additive
subgroup is infinite (represented as zero) if the submodule basis has fewer vectors than the basis
for the module, and otherwise equals the product of the indexes of the ideals generated by each
basis vector.  -/
Module.Basis.SmithNormalForm.toAddSubgroup_index_eq_ite : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {n : ℕ} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Fintype ι] [Infinite R] [inst_4 : Module R M] {N : Submodule R M}
  (snf : Module.Basis.SmithNormalForm N ι n),
  N.toAddSubgroup.index = if n = Fintype.card ι then ∏ i, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index else 0
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- The `n`-independent sets in a graph as a set.  -/
SimpleGraph.indepSetSet : {α : Type u_1} → SimpleGraph α → ℕ → Set (Finset α)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.mul : {R : Type u} → {M : Type v} → [Mul R] → [Add M] → [SMul R M] → [SMul Rᵐᵒᵖ M] → Mul (TrivSqZeroExt R M)
-- Mathlib.GroupTheory.Subsemigroup.Lemmas
Subsemigroup.center_prod : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N],
  Subsemigroup.center (M × N) = (Subsemigroup.center M).prod (Subsemigroup.center N)
-- Aesop.Tracing
Aesop.TraceOption.script : Aesop.TraceOption
-- Mathlib.GroupTheory.GroupAction.Quotient
MulAction.selfEquivOrbitsQuotientProd'.eq_1 : ∀ {G : Type u} {X : Type v} [inst : Group G] [inst_1 : MulAction G X] {φ : Quotient (MulAction.orbitRel G X) → X}
  (hφ : Function.LeftInverse Quotient.mk'' φ) (h : ∀ (b : X), MulAction.stabilizer G b = ⊥),
  MulAction.selfEquivOrbitsQuotientProd' hφ h =
    (MulAction.selfEquivSigmaOrbitsQuotientStabilizer' G X hφ).trans
      ((Equiv.sigmaCongrRight fun x => (Subgroup.quotientEquivOfEq ⋯).trans (QuotientGroup.quotientEquivSelf G)).trans
        (Equiv.sigmaEquivProd (Quotient (MulAction.orbitRel G X)) G))
-- Mathlib.Algebra.Group.Units.Hom
IsAddUnit.liftRight.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : AddMonoid M] [inst_1 : AddMonoid N] (f : M →+ N)
  (hf : ∀ (x : M), IsAddUnit (f x)), IsAddUnit.liftRight f hf = AddUnits.liftRight f (fun x => ⋯.addUnit) ⋯
-- Init.Core
DoResultPRBC.break.injEq : ∀ {α β σ : Type u} (a a_1 : σ), (DoResultPRBC.break a = DoResultPRBC.break a_1) = (a = a_1)
-- Init.Data.List.Nat.TakeDrop
List.head_take : ∀ {α : Type u_1} {l : List α} {i : ℕ} (h : List.take i l ≠ []), (List.take i l).head h = l.head ⋯
-- Mathlib.Topology.MetricSpace.Lipschitz
/-- A function `f : α → ℝ` which is `K`-Lipschitz on a subset `s` admits a `K`-Lipschitz extension
to the whole space.  -/
LipschitzOnWith.extend_real : ∀ {α : Type u} [inst : PseudoMetricSpace α] {f : α → ℝ} {s : Set α} {K : NNReal},
  LipschitzOnWith K f s → ∃ g, LipschitzWith K g ∧ Set.EqOn f g s
-- Mathlib.Data.Nat.Factorization.Defs
Nat.ordProj_dvd : ∀ (n p : ℕ), p ^ n.factorization p ∣ n
-- Mathlib.Order.Bounds.Basic
/-- If `a` is a least upper bound for sets `s` and `p`, then it is a least upper bound for any
set `t`, `s ⊆ t ⊆ p`.  -/
IsLUB.of_subset_of_superset : ∀ {α : Type u_1} [inst : Preorder α] {a : α} {s t p : Set α}, IsLUB s a → IsLUB p a → s ⊆ t → t ⊆ p → IsLUB t a
-- Mathlib.Data.Finsupp.Defs
Finsupp.mapRange_comp : ∀ {α : Type u_1} {M : Type u_4} {N : Type u_5} {O : Type u_6} [inst : Zero M] [inst_1 : Zero N] [inst_2 : Zero O]
  (f : N → O) (hf : f 0 = 0) (f₂ : M → N) (hf₂ : f₂ 0 = 0) (h : (f ∘ f₂) 0 = 0) (g : α →₀ M),
  Finsupp.mapRange (f ∘ f₂) h g = Finsupp.mapRange f hf (Finsupp.mapRange f₂ hf₂ g)
-- Mathlib.Analysis.Real.OfDigits
Real.digits.congr_simp : ∀ (x x_1 : ℝ), x = x_1 → ∀ (b : ℕ) [inst : NeZero b] (a a_1 : ℕ), a = a_1 → x.digits b a = x_1.digits b a_1
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.πTruncGE_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : ∀ (i : ℤ), HomologicalComplex.HasHomology K i] [inst_4 : ∀ (i : ℤ), HomologicalComplex.HasHomology L i]
  (n : ℤ),
  CategoryTheory.CategoryStruct.comp (K.πTruncGE n) (CochainComplex.truncGEMap φ n) =
    CategoryTheory.CategoryStruct.comp φ (L.πTruncGE n)
-- Lean.Meta.Tactic.SolveByElim
Lean.Meta.SolveByElim.SolveByElimConfig.mk.injEq : ∀ (toApplyRulesConfig : Lean.Meta.SolveByElim.ApplyRulesConfig) (backtracking intro constructor suggestions : Bool)
  (toApplyRulesConfig_1 : Lean.Meta.SolveByElim.ApplyRulesConfig)
  (backtracking_1 intro_1 constructor_1 suggestions_1 : Bool),
  ({ toApplyRulesConfig := toApplyRulesConfig, backtracking := backtracking, intro := intro, constructor := constructor,
        suggestions := suggestions } =
      { toApplyRulesConfig := toApplyRulesConfig_1, backtracking := backtracking_1, intro := intro_1,
        constructor := constructor_1, suggestions := suggestions_1 }) =
    (toApplyRulesConfig = toApplyRulesConfig_1 ∧
      backtracking = backtracking_1 ∧ intro = intro_1 ∧ constructor = constructor_1 ∧ suggestions = suggestions_1)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.neg_mem : ∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : SubMulAction R M)
  {x : M}, x ∈ p → -x ∈ p
-- Init.Notation
/-- Format and print the info trees for a given command.
This is mostly useful for debugging info trees.
 -/
Lean.infoTreesCmd : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.mk.sizeOf_spec : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} [inst_2 : SizeOf J] [inst_3 : SizeOf C] (pt : C)
  (ι : F ⟶ (CategoryTheory.Functor.const J).obj pt), sizeOf { pt := pt, ι := ι } = 1 + sizeOf pt + sizeOf ι
-- Init.Data.UInt.Basic
/-- Multiplies two 16-bit unsigned integers, wrapping around on overflow.  Usually accessed via the `*`
operator.

This function is overridden at runtime with an efficient implementation.
 -/
UInt16.mul : UInt16 → UInt16 → UInt16
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- A bilinear map is called right-separating if
the only element that is right-orthogonal to every other element is `0`; i.e.,
for every nonzero `y` in `M₂`, there exists `x` in `M₁` with `B x y ≠ 0`.  -/
LinearMap.SeparatingRight : {R : Type u_1} →
  {R₁ : Type u_2} →
    {R₂ : Type u_3} →
      {M : Type u_5} →
        {M₁ : Type u_6} →
          {M₂ : Type u_7} →
            [inst : CommSemiring R] →
              [inst_1 : AddCommMonoid M] →
                [inst_2 : Module R M] →
                  [inst_3 : CommSemiring R₁] →
                    [inst_4 : AddCommMonoid M₁] →
                      [inst_5 : Module R₁ M₁] →
                        [inst_6 : CommSemiring R₂] →
                          [inst_7 : AddCommMonoid M₂] →
                            [inst_8 : Module R₂ M₂] →
                              {I₁ : R₁ →+* R} → {I₂ : R₂ →+* R} → (M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M) → Prop
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
/-- Abstraction function for `cofix F α`  -/
MvQPF.Cofix.abs : {n : ℕ} → {F : TypeVec.{u} (n + 1) → Type u} → [q : MvQPF F] → {α : TypeVec.{u} n} → (MvQPF.P F).M α → MvQPF.Cofix F α
-- Mathlib.Data.Num.Bitwise
/-- Left-shift the binary representation of a `Num`.  -/
Num.shiftl : Num → ℕ → Num
-- Mathlib.Algebra.Homology.Embedding.Extend
/-- Auxiliary definition for the `d` field of `HomologicalComplex.extend`.  -/
HomologicalComplex.extend.d : {ι : Type u_1} →
  {c : ComplexShape ι} →
    {C : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_3} C] →
        [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
          [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
            (K : HomologicalComplex C c) →
              (i j : Option ι) → HomologicalComplex.extend.X K i ⟶ HomologicalComplex.extend.X K j