mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Index
Subgroup.card_range_dvd : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (f : G →* G'), Nat.card ↥f.range ∣ Nat.card G
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1.stmts₁.match_1.splitter : {Γ : Type u_1} →
  {Λ : Type u_2} →
    {σ : Type u_3} →
      (motive : Turing.TM1.Stmt Γ Λ σ → Sort u_4) →
        (x : Turing.TM1.Stmt Γ Λ σ) →
          ((a : Turing.Dir) → (q : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.move a q)) →
            ((a : Γ → σ → Γ) → (q : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.write a q)) →
              ((a : Γ → σ → σ) → (q : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.load a q)) →
                ((a : Γ → σ → Bool) → (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.branch a q₁ q₂)) →
                  ((Q : Turing.TM1.Stmt Γ Λ σ) →
                      (∀ (a : Turing.Dir) (q : Turing.TM1.Stmt Γ Λ σ), Q = Turing.TM1.Stmt.move a q → False) →
                        (∀ (a : Γ → σ → Γ) (q : Turing.TM1.Stmt Γ Λ σ), Q = Turing.TM1.Stmt.write a q → False) →
                          (∀ (a : Γ → σ → σ) (q : Turing.TM1.Stmt Γ Λ σ), Q = Turing.TM1.Stmt.load a q → False) →
                            (∀ (a : Γ → σ → Bool) (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ),
                                Q = Turing.TM1.Stmt.branch a q₁ q₂ → False) →
                              motive Q) →
                    motive x
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- a left homology data  -/
CategoryTheory.ShortComplex.HomologyData.left : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} → S.HomologyData → S.LeftHomologyData
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
SimpleGraph.FarFromTriangleFree.lt_half : ∀ {α : Type u_1} {𝕜 : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {G : SimpleGraph α}
  {ε : 𝕜} [inst_3 : Fintype α] [inst_4 : DecidableRel G.Adj] [Nonempty α], G.FarFromTriangleFree ε → ε < 2⁻¹
-- Mathlib.Algebra.Group.Hom.Basic
/-- If `f` and `g` are monoid homomorphisms to an additive commutative group,
then `f - g` is the homomorphism sending `x` to `(f x) - (g x)`.  -/
AddMonoidHom.instSub : {M : Type u_2} → {G : Type u_5} → [inst : AddZeroClass M] → [inst_1 : AddCommGroup G] → Sub (M →+ G)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
mul_inv_le_one_of_le₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {a b : G₀}
  [ZeroLEOneClass G₀], a ≤ b → 0 ≤ b → a * b⁻¹ ≤ 1
-- Lean.Data.KVMap
Lean.KVMap.instValueSyntax : Lean.KVMap.Value Lean.Syntax
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.toBiconeFunctor_map_hom : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} {X_1 Y_1 : CategoryTheory.Limits.BinaryBicone X Y} (f : X_1 ⟶ Y_1),
  (CategoryTheory.Limits.BinaryBicone.toBiconeFunctor.map f).hom = f.hom
-- Mathlib.Algebra.Module.Equiv.Basic
LinearMap.ringLmapEquivSelf_apply : ∀ (R : Type u_1) (S : Type u_4) (M : Type u_5) [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : Module S M] [inst_5 : SMulCommClass R S M] (f : R →ₗ[R] M),
  (LinearMap.ringLmapEquivSelf R S M) f = f 1
-- Init.Data.Float.Float
/-- Converts a floating-point number to a 64-bit unsigned integer.

If the given `Float` is non-negative, truncates the value to a positive integer, rounding down and
clamping to the range of `UInt64`. Returns `0` if the `Float` is negative or `NaN`, and returns the
largest `UInt64` value (i.e. `UInt64.size - 1`) if the float is larger than it.

This function has a logical model in terms of `Float.Model`.
 -/
Float.toUInt64 : Float → UInt64
-- Mathlib.RingTheory.Bialgebra.Basic
/-- The counit on a bialgebra preserves multiplication. Note that this is written
in a rather obscure way: it says that two bilinear maps `A →ₗ[R] A →ₗ[R]` are equal.
The two corresponding equal linear maps `A ⊗[R] A →ₗ[R]`
are the following: the first factors through `A` and is multiplication on `A` followed
by `counit`. The second factors through `R ⊗[R] R`, and is `counit ⊗ counit` followed by
multiplication on `R`.

See `Bialgebra.mk'` for a constructor for bialgebras which uses
the more familiar but mathematically equivalent `counit (a * b) = counit a * counit b`.  -/
Bialgebra.mul_compr₂_counit : ∀ {R : Type u} {A : Type v} {inst : CommSemiring R} {inst_1 : Semiring A} [self : Bialgebra R A],
  (LinearMap.mul R A).compr₂ CoalgebraStruct.counit =
    (LinearMap.mul R R).compl₁₂ CoalgebraStruct.counit CoalgebraStruct.counit
-- Mathlib.Data.Finsupp.Defs
Finsupp.support_onFinset_subset : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] {s : Finset α} {f : α → M} {hf : ∀ (a : α), f a ≠ 0 → a ∈ s},
  (Finsupp.onFinset s f hf).support ⊆ s
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.lower_bound_le_one' : ∀ {N : ℕ}, 2 ≤ N → N ≤ 4096 → ↑N * Real.exp (-4 * √(Real.log ↑N)) ≤ 1
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.surjective_of_target_eq_univ : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), e.target = Set.univ → Function.Surjective ↑e
-- Std.Data.HashSet.Basic
/-- Checks if given key is contained and returns the key if it is, otherwise `fallback`.
If they key is contained the result is guaranteed to be pointer equal to the key in the set.
 -/
Std.HashSet.getD : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → Std.HashSet α → α → α → α
-- Lean.Expr
_private.Lean.Expr.0.Lean.intModFn : Lean.Expr
-- Mathlib.RingTheory.Coprime.Lemmas
IsCoprime.prod_right_iff : ∀ {R : Type u} {I : Type v} [inst : CommSemiring R] {x : R} {s : I → R} {t : Finset I},
  IsCoprime x (∏ i ∈ t, s i) ↔ ∀ i ∈ t, IsCoprime x (s i)
-- Mathlib.Tactic.ClickSuggestions.FindPremises
/-- The `apply` discrimination tree root.  -/
Mathlib.Tactic.ClickSuggestions.PreDiscrTrees.app : Mathlib.Tactic.ClickSuggestions.PreDiscrTrees →
  Lean.Meta.RefinedDiscrTree.PreDiscrTree Mathlib.Tactic.ClickSuggestions.ApplyLemma
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cochain.fromSingleMk_postcomp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ}
  (h : p + n = q) {L : CochainComplex C ℤ} (g : K ⟶ L),
  CochainComplex.HomComplex.Cochain.fromSingleMk (CategoryTheory.CategoryStruct.comp f (g.f q)) h =
    (CochainComplex.HomComplex.Cochain.fromSingleMk f h).comp (CochainComplex.HomComplex.Cochain.ofHom g) ⋯
-- Mathlib.Tactic.MkIffOfInductiveProp
/-- `mkOpList op empty [x1, x2, ...]` is defined as `op x1 (op x2 ...)`.
Returns `empty` if the list is empty.  -/
Mathlib.Tactic.MkIff.mkOpList : Lean.Expr → Lean.Expr → List Lean.Expr → Lean.Expr
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_unitIso_inv_app : ∀ (X : CategoryTheory.Limits.WalkingParallelFamily (ULift.{w, 0} Bool)),
  CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair.unitIso.inv.app X = CategoryTheory.eqToHom ⋯
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.colimitIsoColimitGrothendieck.eq_1 : ∀ {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] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] (G : CategoryTheory.Functor C H)
  [inst_3 : L.HasPointwiseLeftKanExtension G] [inst_4 : CategoryTheory.Limits.HasColimitsOfShape D H]
  [inst_5 : CategoryTheory.Limits.HasColimitsOfShape C H],
  L.colimitIsoColimitGrothendieck G =
    Trans.trans
      (Trans.trans ((L.leftKanExtension G).colimitIsoOfIsLeftKanExtension (L.leftKanExtensionUnit G)).symm
        (CategoryTheory.Limits.HasColimit.isoOfNatIso (L.leftKanExtensionIsoFiberwiseColimit G)))
      (CategoryTheory.Limits.colimitFiberwiseColimitIso ((CategoryTheory.CostructuredArrow.grothendieckProj L).comp G))
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Cases.extractAlt! : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.Cases pu → Lean.Name → Lean.Compiler.LCNF.Alt pu × Lean.Compiler.LCNF.Cases pu
-- Mathlib.Dynamics.PeriodicPts.Lemmas
Function.Injective.mem_periodicPts : ∀ {α : Type u_1} {f : α → α} [Finite α], Function.Injective f → ∀ (x : α), x ∈ Function.periodicPts f
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.Functor.leftDerivedZeroIsoSelf_inv_hom_id_assoc : ∀ {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] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteColimits F] {Z : CategoryTheory.Functor C D} (h : F ⟶ Z),
  CategoryTheory.CategoryStruct.comp F.leftDerivedZeroIsoSelf.inv
      (CategoryTheory.CategoryStruct.comp F.fromLeftDerivedZero h) =
    h
-- Mathlib.CategoryTheory.Preadditive.EilenbergMoore
CategoryTheory.Monad.algebraPreadditive_homGroup_sub_f : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (T : CategoryTheory.Monad C) [inst_2 : T.Additive] (F G : T.Algebra) (α β : F ⟶ G), (α - β).f = α.f - β.f
-- Mathlib.CategoryTheory.Adjunction.Evaluation
CategoryTheory.evaluationAdjunctionRight_unit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : ∀ (a b : C), CategoryTheory.Limits.HasCoproductsOfShape (a ⟶ b) D] (c : C) (X : D),
  (CategoryTheory.evaluationAdjunctionRight D c).unit.app X =
    CategoryTheory.Limits.Sigma.ι (fun x => X) (CategoryTheory.CategoryStruct.id c)
-- Mathlib.Analysis.Normed.Algebra.Spectrum
_private.Mathlib.Analysis.Normed.Algebra.Spectrum.0.spectrum.termσ : Lean.ParserDescr
-- Mathlib.Topology.Separation.Basic
t0Space_iff_inseparable : ∀ (X : Type u) [inst : TopologicalSpace X], T0Space X ↔ ∀ (x y : X), Inseparable x y → x = y
-- Mathlib.Algebra.MvPolynomial.Equiv
Polynomial.toMvPolynomial_C : ∀ {R : Type u_1} {σ : Type u_3} [inst : CommSemiring R] (i : σ) (r : R),
  (Polynomial.toMvPolynomial i) (Polynomial.C r) = MvPolynomial.C r
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.coe_ker : ∀ {G : Type u_1} [inst : Group G] {M : Type u_7} [inst_1 : MulOneClass M] (f : G →* M), ↑f.ker = ⇑f ⁻¹' {1}
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.isAlgebra : {R : Type u} → [inst : CommRing R] → (self : AlgCat R) → Algebra R ↑self
-- Init.Data.UInt.Lemmas
UInt32.ofNat_le_iff_le : ∀ {a b : ℕ}, a < UInt32.size → b < UInt32.size → (UInt32.ofNat a ≤ UInt32.ofNat b ↔ a ≤ b)
-- Mathlib.Algebra.Order.Monovary
Monovary.pow_right₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : Semiring β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] {f : ι → α} {g : ι → β}, 0 ≤ g → Monovary f g → ∀ (n : ℕ), Monovary f (g ^ n)
-- Mathlib.Data.Finsupp.Option
Finsupp.optionElim_apply_none : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (y : M) (f : α →₀ M), (Finsupp.optionElim y f) none = y
-- Init.Data.Rat.Lemmas
Rat.le_floor_iff : ∀ {x : ℤ} {a : ℚ}, x ≤ a.floor ↔ ↑x ≤ a
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csSup_lowerBounds_range : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] [Nonempty β] {f : β → α},
  BddBelow (Set.range f) → sSup (lowerBounds (Set.range f)) = ⨅ i, f i
-- Mathlib.Data.Holor
Holor.instAdd : {α : Type} → {ds : List ℕ} → [Add α] → Add (Holor α ds)
-- Init.Data.List.Lemmas
List.not_mem_nil : ∀ {α : Type u_1} {a : α}, a ∉ []
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsStrictRestriction.irrefl : ∀ {α : Type u_1} (M : Matroid α), ¬M.IsStrictRestriction M
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.SplittingFieldAux.instIsSplittingFieldNatDegree : ∀ {K : Type v} [inst : Field K] (f : Polynomial K),
  Polynomial.IsSplittingField K (Polynomial.SplittingFieldAux f.natDegree f) f
-- Mathlib.Algebra.Free
FreeAddMagma.toFreeAddSemigroup.eq_1 : ∀ {α : Type u}, FreeAddMagma.toFreeAddSemigroup = FreeAddMagma.lift FreeAddSemigroup.of
-- Mathlib.FieldTheory.RatFunc.Luroth
/-- The minimal polynomial of `X` with coefficients in `E`.  -/
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.φ : {K : Type u_1} → [inst : Field K] → (E : IntermediateField K (RatFunc K)) → Polynomial ↥E
-- Mathlib.Algebra.Ring.IsFormallyReal
/-- The property of being a sum of squares of nonzero elements (S) is defined inductively by:
`a * a : R` is (S) for all nonzero `a`, and
if `s : R` is (S), and `a ≠ 0`, then `a * a + s` is (S).
 -/
IsSumNonzeroSq : {R : Type u_1} → [Mul R] → [Add R] → [Zero R] → R → Prop
-- Mathlib.Data.ZMod.Basic
ZMod.neg_one_ne_one : ∀ {n : ℕ} [Fact (2 < n)], -1 ≠ 1
-- Init.Data.SInt.Bitwise
Int64.ofBitVec_intMin : Int64.ofBitVec (BitVec.intMin 64) = Int64.minValue
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
MvQPF.instInhabitedCofixOfAP : {n : ℕ} →
  {F : TypeVec.{u} (n + 1) → Type u} →
    [q : MvQPF F] →
      {α : TypeVec.{u} n} → [Inhabited (MvQPF.P F).A] → [(i : Fin2 n) → Inhabited (α i)] → Inhabited (MvQPF.Cofix F α)
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
TensorProduct.finsuppScalarRight.eq_1 : ∀ (R : Type u_1) (S : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (M : Type u_3)
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] (ι : Type u_5)
  [inst_7 : DecidableEq ι],
  TensorProduct.finsuppScalarRight R S M ι =
    TensorProduct.finsuppRight R S M R ι ≪≫ₗ Finsupp.mapRange.linearEquiv (TensorProduct.AlgebraTensorModule.rid R S M)
-- Mathlib.Data.Prod.Lex
Prod.Lex.noMaxOrder_of_right : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [NoMaxOrder β], NoMaxOrder (Lex (α × β))
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.conv_withDensity_eq_lconvolution : ∀ {G : Type u_3} [inst : AddGroup G] {mG : MeasurableSpace G} [MeasurableAdd₂ G] [MeasurableNeg G]
  {μ : MeasureTheory.Measure G} [MeasureTheory.SFinite μ] [μ.IsAddLeftInvariant] {f g : G → ENNReal},
  Measurable f →
    Measurable g → (μ.withDensity f).conv (μ.withDensity g) = μ.withDensity (MeasureTheory.lconvolution f g μ)
-- Mathlib.Logic.Equiv.Prod
Equiv.sigmaCongrRight_sigmaEquivProd : ∀ {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : α₁ → β₁ ≃ β₂),
  (Equiv.sigmaCongrRight e).trans (Equiv.sigmaEquivProd α₁ β₂) =
    (Equiv.sigmaEquivProd α₁ β₁).trans (Equiv.prodCongrRight e)
-- Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
CategoryTheory.Triangulated.AbelianSubcategory.exists_lift_ιK : ∀ {C : Type u_1} {A : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_5 : CategoryTheory.Pretriangulated C] [inst_6 : CategoryTheory.Category.{v_2, u_2} A]
  {ι : CategoryTheory.Functor A C},
  (∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (CategoryTheory.shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0) →
    ∀ {X₁ X₂ : A} {f₁ : X₁ ⟶ X₂} {X₃ : C} {f₂ : ι.obj X₂ ⟶ X₃}
      {f₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj (ι.obj X₁)},
      CategoryTheory.Pretriangulated.Triangle.mk (ι.map f₁) f₂ f₃ ∈
          CategoryTheory.Pretriangulated.distinguishedTriangles →
        ∀ {K Q : A} {α : (CategoryTheory.shiftFunctor C 1).obj (ι.obj K) ⟶ X₃} {β : X₃ ⟶ ι.obj Q}
          {γ : ι.obj Q ⟶ (CategoryTheory.shiftFunctor C 1).obj ((CategoryTheory.shiftFunctor C 1).obj (ι.obj K))},
          CategoryTheory.Pretriangulated.Triangle.mk α β γ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
            ∀ [inst_7 : ι.Full] [inst_8 : CategoryTheory.Preadditive A] [ι.Faithful] {B : A} (x₁ : B ⟶ X₁),
              CategoryTheory.CategoryStruct.comp x₁ f₁ = 0 →
                ∃ k, CategoryTheory.CategoryStruct.comp k (CategoryTheory.Triangulated.AbelianSubcategory.ιK f₃ α) = x₁
-- Lean.LocalContext
Lean.LocalContext.mkEmpty : Unit → Lean.LocalContext
-- Mathlib.Data.Fin.Pigeonhole
/-- If we have an embedding from `Fin m` to `Fin n`, then `m ≤ n`.
See also `Fintype.card_le_of_embedding` for the generalisation to arbitrary finite types.
 -/
Fin.le_of_embedding : ∀ {m n : ℕ} (f : Fin m ↪ Fin n), m ≤ n
-- Std.Async.System
/-- The name of the group.
 -/
Std.Async.System.GroupInfo.groupName : Std.Async.System.GroupInfo → String
-- Mathlib.Algebra.Category.ModuleCat.Descent
ModuleCat.preservesFiniteLimits_extendScalars_of_flat : ∀ {A B : Type u} [inst : CommRing A] [inst_1 : CommRing B] {f : A →+* B},
  f.Flat → CategoryTheory.Limits.PreservesFiniteLimits (ModuleCat.extendScalars f)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for signed division of `BitVec`s using the SMT-LIB conventions.  -/
BitVec.reduceSMTSDiv : Lean.Meta.Simp.DSimproc
-- Lean.Compiler.Specialize
Lean.Compiler.SpecializeAttributeKind.specialize.sizeOf_spec : sizeOf Lean.Compiler.SpecializeAttributeKind.specialize = 1
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.sectL_obj : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] (c : C)
  (a : B), (CategoryTheory.Bicategory.Prod.sectL B c).obj a = (a, c)
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.FindMin.WF.mk.injEq : ∀ {α : Type u_1} {le : α → α → Bool} {res : Batteries.BinomialHeap.Imp.FindMin α} (rank : ℕ)
  (before :
    ∀ {s : Batteries.BinomialHeap.Imp.Heap α},
      Batteries.BinomialHeap.Imp.Heap.WF le rank s → Batteries.BinomialHeap.Imp.Heap.WF le 0 (res.before s))
  (node : Batteries.BinomialHeap.Imp.HeapNode.WF le res.val res.node rank)
  (next : Batteries.BinomialHeap.Imp.Heap.WF le (rank + 1) res.next) (rank_1 : ℕ)
  (before_1 :
    ∀ {s : Batteries.BinomialHeap.Imp.Heap α},
      Batteries.BinomialHeap.Imp.Heap.WF le rank_1 s → Batteries.BinomialHeap.Imp.Heap.WF le 0 (res.before s))
  (node_1 : Batteries.BinomialHeap.Imp.HeapNode.WF le res.val res.node rank_1)
  (next_1 : Batteries.BinomialHeap.Imp.Heap.WF le (rank_1 + 1) res.next),
  ({ rank := rank, before := before, node := node, next := next } =
      { rank := rank_1, before := before_1, node := node_1, next := next_1 }) =
    (rank = rank_1)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.forIn'_congr : ∀ {α : Type u} [inst : LT α] [inst_1 : Std.PRange.UpwardEnumerable α] [inst_2 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_3 : Std.Rxi.IsAlwaysFinite α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w}
  [inst_5 : Monad m] {γ : Type u} {init init' : γ} {r r' : Std.Roi α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)}
  {f' : (a : α) → a ∈ r' → γ → m (ForInStep γ)} (hr : r = r'),
  init = init' → (∀ (a : α) (m_1 : a ∈ r') (b : γ), f a ⋯ b = f' a m_1 b) → forIn' r init f = forIn' r' init' f'
-- Init.Data.Vector.Basic
/-- Swap two elements of a vector using `Nat` indices. Panics if either index is out of bounds.

This will perform the update destructively provided that the vector has a reference count of 1.
 -/
Vector.swapIfInBounds : {α : Type u_1} → {n : ℕ} → Vector α n → ℕ → ℕ → Vector α n
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.algebraMap_apply : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {r : R},
  (algebraMap R (PowerSeries A)) r = PowerSeries.C ((algebraMap R A) r)
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- If `R` and `S` are isomorphic rings, `S` viewed as an `R`-module is isomorphic to `R`.  -/
ModuleCat.restrictScalarsIsoOfEquiv : {R S : Type v} →
  [inst : Ring R] →
    [inst_1 : Ring S] →
      (e : R ≃+* S) → (ModuleCat.restrictScalars e.toRingHom).obj (ModuleCat.of S S) ≅ ModuleCat.of R R
-- Mathlib.RingTheory.WittVector.Defs
WittVector.wittOne_pos_eq_zero : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ), 0 < n → WittVector.wittOne p n = 0
-- Mathlib.CategoryTheory.Sites.MorphismProperty
CategoryTheory.Precoverage.galoisConnection_morphismProperty_precoverage : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C],
  GaloisConnection CategoryTheory.Precoverage.morphismProperty CategoryTheory.MorphismProperty.precoverage
-- Mathlib.NumberTheory.RamificationInertia.Ramification
Ideal.le_pow_of_le_ramificationIdx' : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R} {P : Ideal S}
  {n : ℕ}, n ≤ p.ramificationIdx' P → Ideal.map (algebraMap R S) p ≤ P ^ n
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
MeasureTheory.indicatorConstLp.congr_simp : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  {s s_1 : Set α} (e_s : s = s_1) (p : ENNReal) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (c c_1 : E),
  c = c_1 → MeasureTheory.indicatorConstLp p hs hμs c = MeasureTheory.indicatorConstLp p ⋯ ⋯ c_1
-- Init.Data.SInt.Bitwise
Int64.toISize_and : ∀ (a b : Int64), (a &&& b).toISize = a.toISize &&& b.toISize
-- Mathlib.Tactic.ClickSuggestions.Apply
/-- The name length of the used lemma.  -/
Mathlib.Tactic.ClickSuggestions.ApplyKey.nameLength : Mathlib.Tactic.ClickSuggestions.ApplyKey → ℕ
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.State.mk.sizeOf_spec : ∀ (symState : Lean.Meta.Sym.State) (grindState : Lean.Meta.Grind.State) (goals : List Lean.Meta.Grind.Goal)
  (cache : Lean.Elab.Tactic.Grind.Cache),
  sizeOf { symState := symState, grindState := grindState, goals := goals, cache := cache } =
    1 + sizeOf symState + sizeOf grindState + sizeOf goals + sizeOf cache
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.mk.inj : ∀ {α : Type u_6} {β : Type u_7} {inst : Preorder α} {inst_1 : Preorder β} {inst_2 : MulOneClass α}
  {inst_3 : MulOneClass β} {toMonoidHom : α →* β} {monotone' : Monotone (↑toMonoidHom).toFun} {toMonoidHom_1 : α →* β}
  {monotone'_1 : Monotone (↑toMonoidHom_1).toFun},
  { toMonoidHom := toMonoidHom, monotone' := monotone' } = { toMonoidHom := toMonoidHom_1, monotone' := monotone'_1 } →
    toMonoidHom = toMonoidHom_1
-- Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
CategoryTheory.colimitCompWhiskeringRightIsoColimitComp.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  {J : Type u_4} [inst_3 : CategoryTheory.Category.{v_4, u_4} J] [inst_4 : CategoryTheory.Limits.HasColimitsOfShape J D]
  (F : CategoryTheory.Functor D E) [inst_5 : CategoryTheory.Limits.PreservesColimitsOfShape J F]
  (G : CategoryTheory.Functor J (CategoryTheory.Functor C D)),
  CategoryTheory.colimitCompWhiskeringRightIsoColimitComp F G =
    (CategoryTheory.preservesColimitIso ((CategoryTheory.Functor.whiskeringRight C D E).obj F) G).symm
-- Mathlib.Algebra.Lie.Cochain
LieModule.Cohomology.d₁₂_apply_coe_apply_apply : ∀ (R : Type u_1) [inst : CommRing R] (L : Type u_2) [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (f : LieModule.Cohomology.oneCochain R L M) (x y : L),
  (↑((LieModule.Cohomology.d₁₂ R L M) f) x) y = ⁅x, f y⁆ - ⁅y, f x⁆ - f ⁅x, y⁆
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons.eq_1 : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} (exp : ℝ)
  (coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl)
  (tl : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl),
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef tl = Stream'.Seq.cons (exp, coef) tl
-- Lean.Declaration
Lean.ConstantInfo.ctorInfo.injEq : ∀ (val val_1 : Lean.ConstructorVal), (Lean.ConstantInfo.ctorInfo val = Lean.ConstantInfo.ctorInfo val_1) = (val = val_1)