mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKeyD_le_minKeyD_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, t.erase k ≠ ∅ → ∀ {fallback : α}, (cmp (t.minKeyD fallback) ((t.erase k).minKeyD fallback)).isLE = true
-- Init.Data.Array.Lemmas
Array.toList_eraseIdx : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {h : i < xs.size}, (xs.eraseIdx i h).toList = xs.toList.eraseIdx i
-- Mathlib.Order.Minimal
maximal_true : ∀ {α : Type u_2} {x : α} [inst : LE α], Maximal (fun x => True) x ↔ IsMax x
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_comp_const_mul : ∀ {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]
  [ContinuousMap.UniqueHom R A] (r : R) (f : R → R) (a : A),
  autoParam (ContinuousOn f ((fun x => r * x) '' spectrum R a)) cfc_comp_const_mul._auto_1 →
    autoParam (p a) cfc_comp_const_mul._auto_3 → cfc (fun x => f (r * x)) a = cfc f (r • a)
-- Mathlib.Data.Nat.Factorization.Basic
Nat.ordCompl_mul : ∀ (a b p : ℕ), a * b / p ^ (a * b).factorization p = a / p ^ a.factorization p * (b / p ^ b.factorization p)
-- Mathlib.Order.Atoms
eq_sSup_atoms : ∀ {α : Type u_4} [inst : CompleteLattice α] [IsAtomistic α] (b : α), ∃ s, b = sSup s ∧ ∀ a ∈ s, IsAtom a
-- Mathlib.GroupTheory.GroupAction.Basic
AddAction.instIsPretransitiveElemOrbit_1 : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] (x : AddAction.orbitRel.Quotient G α),
  AddAction.IsPretransitive G ↑x.orbit
-- Lean.Meta.Tactic.Try.Collect
/-- `Set` with insertion order preserved.  -/
Lean.Meta.Try.Collector.OrdSet : (α : Type) → [Hashable α] → [BEq α] → Type
-- Mathlib.Algebra.Group.End
MulEquiv.mk.congr_simp : ∀ {M : Type u_9} {N : Type u_10} [inst : Mul M] [inst_1 : Mul N] (toEquiv toEquiv_1 : M ≃ N)
  (e_toEquiv : toEquiv = toEquiv_1) (map_mul' : ∀ (x y : M), toEquiv.toFun (x * y) = toEquiv.toFun x * toEquiv.toFun y),
  { toEquiv := toEquiv, map_mul' := map_mul' } = { toEquiv := toEquiv_1, map_mul' := ⋯ }
-- Mathlib.RingTheory.TensorProduct.Quotient
Algebra.TensorProduct.quotientTensorEquiv_symm_apply_tmul : ∀ {R : Type u_1} (S : Type u_2) (T : Type u_3) (A : Type u_4) [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : CommRing A] [inst_6 : Algebra R A]
  [inst_7 : Algebra S A] [inst_8 : IsScalarTower R S A] (I : Ideal A) (a : A) (t : T),
  (Algebra.TensorProduct.quotientTensorEquiv S T A I).symm
      ((Ideal.Quotient.mk (Ideal.map (algebraMap A (TensorProduct R A T)) I)) (a ⊗ₜ[R] t)) =
    (Ideal.Quotient.mk I) a ⊗ₜ[R] t
-- Mathlib.Topology.Algebra.Group.Basic
Specializes.inv : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Inv G] [ContinuousInv G] {x y : G}, x ⤳ y → x⁻¹ ⤳ y⁻¹
-- Mathlib.Algebra.Category.MonCat.Yoneda
AddCommMonCat.coyonedaType_obj_obj_coe : ∀ (X : Type uᵒᵖ) (M : AddCommMonCat), ↑((AddCommMonCat.coyonedaType.obj X).obj M) = (Opposite.unop X → ↑M)
-- Mathlib.RingTheory.Coalgebra.TensorProduct
_private.Mathlib.RingTheory.Coalgebra.TensorProduct.0.Coalgebra.termδ : Lean.ParserDescr
-- Std.Net.Addr
Std.Net.instDecidableEqSocketAddressV6.decEq : (x x_1 : Std.Net.SocketAddressV6) → Decidable (x = x_1)
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.δ_apply : ∀ {n d : ℕ} (x : (SSet.stdSimplex.obj { len := n }).obj (Opposite.op { len := d + 1 })) (i : Fin (d + 2))
  (j : Fin (d + 1)),
  ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (SSet.stdSimplex.obj { len := n }) i)) x) j =
    x (i.succAbove j)
-- Mathlib.RingTheory.PicardGroup
/-- `mk R M` is indeed the class of `M`.  -/
CommRing.Pic.mk.linearEquiv : (R : Type u) →
  (M : Type v) →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → [inst_3 : Module.Invertible R M] → (CommRing.Pic.mk R M).AsModule ≃ₗ[R] M
-- Lean.Util.Recognizers
/-- Recognizes `x1 ≍ x2`, returns `some (α1, x1, α2, x2)`.   -/
Lean.Expr.heq? : Lean.Expr → Option (Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr)
-- Mathlib.Geometry.Euclidean.Circumcenter
Affine.Simplex.circumradius_restrict : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) (S : AffineSubspace ℝ P)
  (hS : affineSpan ℝ (Set.range s.points) ≤ S), (s.restrict S hS).circumradius = s.circumradius
-- Mathlib.Analysis.Seminorm
Seminorm.finset_sup_apply_lt : ∀ {𝕜 : Type u_3} {E : Type u_7} {ι : Type u_11} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] {p : ι → Seminorm 𝕜 E} {s : Finset ι} {x : E} {a : ℝ},
  0 < a → (∀ i ∈ s, (p i) x < a) → (s.sup p) x < a
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersion.instNormedAddCommGroupComplement : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      {E'' : Type u} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup E''] →
              [inst_4 : NormedSpace 𝕜 E''] →
                {H : Type u_7} →
                  [inst_5 : TopologicalSpace H] →
                    {G : Type u_9} →
                      [inst_6 : TopologicalSpace G] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {J : ModelWithCorners 𝕜 E'' G} →
                            {M : Type u_11} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H M] →
                                  {N : Type u_13} →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace G N] →
                                        {n : WithTop ℕ∞} →
                                          {f : M → N} →
                                            (h : Manifold.IsImmersion I J n f) → NormedAddCommGroup h.complement
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- **Alias** of `DFunLike.ext_iff`. -/
MeasureTheory.VectorMeasure.ext_iff' : ∀ {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β] {f g : F}, f = g ↔ ∀ (x : α), f x = g x
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.extend_apply_of_le_zero : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  (F : f₀.Homotopy f₁) {t : ℝ}, t ≤ 0 → ∀ (x : X), (F.extend t) x = f₀ x
-- Mathlib.Order.Category.LinOrd
LinOrd.dual_map : ∀ {X Y : LinOrd} (f : X ⟶ Y), LinOrd.dual.map f = LinOrd.ofHom (OrderHom.dual (LinOrd.Hom.hom f))
-- Mathlib.Data.Nat.Choose.Multinomial
/-- The `multinomial` coefficients on `Multiset ℕ`.  -/
Multiset.multinomial : Multiset ℕ → ℕ
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.SeparatesPoints.mono : ∀ {α : Type u_1} {m m' : MeasurableSpace α} [hsep : MeasurableSpace.SeparatesPoints α],
  m ≤ m' → MeasurableSpace.SeparatesPoints α
-- Mathlib.Analysis.Normed.Group.Quotient
/-- The operator norm of the projection is at most `1`.  -/
AddSubgroup.norm_normedMk_le : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] (S : AddSubgroup M), ‖S.normedMk‖ ≤ 1
-- Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
/-- Elements of the character space are continuous linear maps.  -/
WeakDual.CharacterSpace.instContinuousLinearMapClass : ∀ {𝕜 : 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], ContinuousLinearMapClass (↑(WeakDual.characterSpace 𝕜 A)) 𝕜 A 𝕜
-- Mathlib.Analysis.Complex.Asymptotics
Int.cast_complex_isTheta_cast_real : Int.cast =Θ[Filter.cofinite] Int.cast
-- Mathlib.CategoryTheory.Sites.Descent.IsPrestack
/-- If `F` is a prestack from `Cᵒᵖ` to `Cat` relatively to a Grothendieck topology `J`,
and `M` and `N` are two objects in `F.obj (.mk (op S))`, this is the sheaf of
morphisms from `M` to `N`: it sends an object `T : Over S` corresponding to
a morphism `p : X ⟶ S` to the type of morphisms $p^* M ⟶ p^* N$.  -/
CategoryTheory.Pseudofunctor.sheafHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) →
      (J : CategoryTheory.GrothendieckTopology C) →
        [F.IsPrestack J] →
          {S : C} →
            ↑(F.obj { as := Opposite.op S }) →
              ↑(F.obj { as := Opposite.op S }) → CategoryTheory.Sheaf (J.over S) (Type v')
-- Batteries.Recycling.RBTree.Alter
/-- `O(log n)`. `alterP cut f t` simultaneously handles inserting, erasing and replacing an element
using a function `f : Option α → Option α`. It is passed the result of `t.findP? cut`
and can either return `none` to remove the element or `some a` to replace/insert
the element with `a` (which must have the same ordering properties as the original element).

The element is used linearly if `t` is unshared.

The `AlterWF` assumption is required because `f` may change
the ordering properties of the element, which would break the invariants.
 -/
RBTree.RBMap.alter : {α : Type u_1} →
  {β : Type u_2} → {cmp : α → α → Ordering} → RBTree.RBMap α β cmp → α → (Option β → Option β) → RBTree.RBMap α β cmp
-- Mathlib.Data.Set.BoolIndicator
Set.preimage_boolIndicator : ∀ {α : Type u_1} (s : Set α) (t : Set Bool),
  s.boolIndicator ⁻¹' t = Set.univ ∨ s.boolIndicator ⁻¹' t = s ∨ s.boolIndicator ⁻¹' t = sᶜ ∨ s.boolIndicator ⁻¹' t = ∅
-- Lean.Data.JsonRpc
Lean.JsonRpc.instInhabitedMessageMetaData.default : Lean.JsonRpc.MessageMetaData
-- Init.Data.SInt.Lemmas
Int16.toBitVec_one : Int16.toBitVec 1 = 1#16
-- Mathlib.Data.Sym.Card
Sym2.card_diagSet_compl : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α], Fintype.card ↑Sym2.diagSetᶜ = (Fintype.card α).choose 2
-- Mathlib.RepresentationTheory.Submodule
Representation.invtSubmodule.coe_bot : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommSemiring k] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] (ρ : Representation k G V), ↑⊥ = ⊥
-- Init.Data.UInt.Lemmas
UInt64.toNat_ofNat' : ∀ {n : ℕ}, (UInt64.ofNat n).toNat = n % 2 ^ 64
-- Mathlib.Combinatorics.Matroid.Rank.Finite
Matroid.isRkFinite_set : ∀ {α : Type u_1} (M : Matroid α) [M.RankFinite] (X : Set α), M.IsRkFinite X
-- Init.Grind.FieldNormNum
Lean.Grind.Field.NormNum.ofRat_div : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] [Lean.Grind.IsCharP α 0] (a b : ℚ),
  Lean.Grind.Field.NormNum.ofRat (a / b) = Lean.Grind.Field.NormNum.ofRat a / Lean.Grind.Field.NormNum.ofRat b
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.PendingSolverPropagationsData : Type
-- Mathlib.Topology.LocallyFinite
LocallyFinite.sumElim : ∀ {ι : Type u_1} {ι' : Type u_2} {X : Type u_4} [inst : TopologicalSpace X] {f : ι → Set X} {g : ι' → Set X},
  LocallyFinite f → LocallyFinite g → LocallyFinite (Sum.elim f g)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.FoldingRange.endLine : Lean.Lsp.FoldingRange → ℕ
-- Lean.Environment
/-- Accesses only the state of the current environment branch. Modifications on other branches are not
visible and are ultimately discarded except for the main branch. Provides the fastest accessors,
will never block.

This mode is particularly suitable for extensions where state does not escape from lexical scopes
even without parallelism, e.g. `ScopedEnvExtension`s when setting local entries.
 -/
Lean.EnvExtension.AsyncMode.local : Lean.EnvExtension.AsyncMode
-- Mathlib.Topology.ContinuousOn
/-- If `f` is continuous on an open set `s` and continuous at each point of another
set `t` then `f` is continuous on `s ∪ t`.  -/
ContinuousOn.union_continuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s t : Set α} {f : α → β},
  IsOpen s → ContinuousOn f s → (∀ x ∈ t, ContinuousAt f x) → ContinuousOn f (s ∪ t)
-- Mathlib.RingTheory.TensorProduct.Maps
/-- If `R →+* S` is surjective, the multiplication map `S ⊗[R] S →+* S` is an isomorphism. This
is the algebraic version of closed immersions are monomorphisms.  -/
LinearMap.mul'_bijective_of_surjective : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A],
  Function.Surjective ⇑(algebraMap R A) → Function.Bijective ⇑(LinearMap.mul' R A)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_eq_fallback : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {a fallback : α},
  Std.Internal.List.containsKey a l = false → Std.Internal.List.getKeyD a l fallback = fallback
-- Init.Data.SInt.Bitwise
Int16.neg_one_xor : ∀ {a : Int16}, -1 ^^^ a = ~~~a
-- Mathlib.Analysis.Normed.Group.Pointwise
IsCompact.sub_closedBall_zero : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] {δ : ℝ} {s : Set E},
  IsCompact s → 0 ≤ δ → s - Metric.closedBall 0 δ = Metric.cthickening δ s
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_diff_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k : α},
  k ∉ t₂ → (t₁ \ t₂).get! k = t₁.get! k
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_modify : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k k' : α} {f : β k → β k},
  m.WF → (m.modify k f).get? k' = if h : (k == k') = true then cast ⋯ (Option.map f (m.get? k)) else m.get? k'
-- Init.Data.BitVec.Bitblast
BitVec.mulRec.eq_1 : ∀ {w : ℕ} (x y : BitVec w), x.mulRec y 0 = if y.getLsbD 0 = true then x <<< 0 else 0
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
/-- Version of `LinearIndependent.of_subsingleton` that works for the zero ring.  -/
LinearIndependent.of_subsingleton' : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {v : ι → M} [Subsingleton ι] (i : ι), (∀ (r : R), r • v i = 0 → r = 0) → LinearIndependent R v
-- Mathlib.Data.Finset.Sigma
Finset.card_sigmaLift : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {γ : ι → Type u_4} [inst : DecidableEq ι]
  (f : ⦃i : ι⦄ → α i → β i → Finset (γ i)) (a : (i : ι) × α i) (b : (i : ι) × β i),
  (Finset.sigmaLift f a b).card = if h : a.fst = b.fst then (f (h ▸ a.snd) b.snd).card else 0
-- Mathlib.Algebra.Order.Quantale
Quantale.rightMulResiduation.eq_1 : ∀ {α : Type u_1} [inst : Semigroup α] [inst_1 : CompleteLattice α] (x y : α),
  Quantale.rightMulResiduation x y = sSup {z | x * z ≤ y}
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
/-- If `H` has at least one edge, then there exists an extremal `H.Free` graph.  -/
SimpleGraph.exists_isExtremal_free : ∀ {V : Type u_1} [inst : Fintype V] {W : Type u_2} {H : SimpleGraph W}, H ≠ ⊥ → ∃ G x, G.IsExtremal H.Free
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner
_private.Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner.0.MeasureTheory.«term⟪_,_⟫» : Lean.ParserDescr
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.Stmt.inhabited : {K : Type u_1} → (Γ : K → Type u_2) → (Λ : Type u_3) → (σ : Type u_4) → Inhabited (Turing.TM2.Stmt Γ Λ σ)
-- Mathlib.Order.KrullDimension
Order.coheight_le_coheight_apply_of_strictMono : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α → β),
  StrictMono f → ∀ (x : α), Order.coheight x ≤ Order.coheight (f x)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
lt_of_mul_lt_mul_of_le₀ : ∀ {α : Type u_1} [inst : LinearOrderedCommGroupWithZero α] {a b c d : α}, a * b < c * d → 0 < c → c ≤ a → b < d
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.coe_mk : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B]
  [inst_4 : SMul R A] [inst_5 : SMul R B] [inst_6 : Star A] [inst_7 : Star B] (e : A ≃⋆+* B)
  (h : ∀ (r : R) (a : A), e.toFun (r • a) = r • e.toFun a), ⇑{ toStarRingEquiv := e, map_smul' := h } = ⇑e
-- Mathlib.LinearAlgebra.Lagrange
/-- Lagrange basis polynomials indexed by `s : Finset ι`, defined at nodes `v i` for a
map `v : ι → F`. For `i, j ∈ s`, `basis s v i` evaluates to 0 at `v j` for `i ≠ j`. When
`v` is injective on `s`, `basis s v i` evaluates to 1 at `v i`.  -/
Lagrange.basis : {F : Type u_1} → [inst : Field F] → {ι : Type u_2} → [DecidableEq ι] → Finset ι → (ι → F) → ι → Polynomial F
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- The forgetful functor.  -/
CategoryTheory.MorphismProperty.Comma.forget : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {B : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
        {T : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} T] →
            (L : CategoryTheory.Functor A T) →
              (R : CategoryTheory.Functor B T) →
                (P : CategoryTheory.MorphismProperty T) →
                  (Q : CategoryTheory.MorphismProperty A) →
                    (W : CategoryTheory.MorphismProperty B) →
                      [inst_3 : Q.IsMultiplicative] →
                        [inst_4 : W.IsMultiplicative] →
                          CategoryTheory.Functor (CategoryTheory.MorphismProperty.Comma L R P Q W)
                            (CategoryTheory.Comma L R)
-- Mathlib.Algebra.Module.Projective
/-- A variant of `of_lifting_property'` when we're working over a `[Ring R]`,
which only requires quantifying over modules with an `AddCommGroup` instance.  -/
Module.Projective.of_lifting_property : ∀ {R : Type u} [inst : Ring R] {P : Type v} [inst_1 : AddCommGroup P] [inst_2 : Module R P] [Small.{v, u} R],
  (∀ {M N : Type v} [inst_4 : AddCommGroup M] [inst_5 : AddCommGroup N] [inst_6 : Module R M] [inst_7 : Module R N]
      (f : M →ₗ[R] N) (g : P →ₗ[R] N), Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g) →
    Module.Projective R P
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSet.compl_iff : ∀ {α : Type u_1} {s : Set α} {m : MeasurableSpace α}, MeasurableSet sᶜ ↔ MeasurableSet s
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ElabImage.mk : String → Lean.StrLit → Lean.Doc.ElabImage✝
-- Lean.Parser.Term
Lean.Parser.Term.sorry.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Meta.Hint
/-- Character-level diff.  -/
Lean.Meta.Hint.DiffGranularity.char : Lean.Meta.Hint.DiffGranularity
-- Aesop.Stats.Basic
Aesop.ScriptGenerated.method : Aesop.ScriptGenerated → Aesop.ScriptGenerated.Method
-- Mathlib.Algebra.Lie.Killing
LieIdeal.isCompl_killingCompl : ∀ {K : Type u_2} {L : Type u_3} [inst : Field K] [inst_1 : LieRing L] [inst_2 : LieAlgebra K L]
  [LieAlgebra.IsKilling K L] [Module.Finite K L] (I : LieIdeal K L), IsCompl I (LieIdeal.killingCompl K L I)
-- Mathlib.Analysis.InnerProductSpace.PiL2
DirectSum.IsInternal.card_filter_subordinateOrthonormalBasisIndex_eq : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : FiniteDimensional 𝕜 E] {n : ℕ}
  (hn : Module.finrank 𝕜 E = n) [inst_5 : DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : DirectSum.IsInternal V)
  (hV' : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ) (i : ι),
  {a | DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn hV a hV' = i}.card = Module.finrank 𝕜 ↥(V i)
-- Init.Data.SInt.Lemmas
UInt8.toBitVec_toInt8 : ∀ (x : UInt8), x.toInt8.toBitVec = x.toBitVec
-- Mathlib.Algebra.Group.Defs
/-- A `RightCancelSemigroup` is a semigroup such that `a * b = c * b` implies `a = c`.  -/
RightCancelSemigroup : Type u → Type u
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
NumberField.nrComplexPlaces_eq_zero_iff : ∀ {K : Type u_2} [inst : Field K] [inst_1 : NumberField K],
  NumberField.InfinitePlace.nrComplexPlaces K = 0 ↔ NumberField.IsTotallyReal K
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cont.cons₁.inj : ∀ {a : Turing.ToPartrec.Code} {a_1 : List ℕ} {a_2 : Turing.ToPartrec.Cont} {a_3 : Turing.ToPartrec.Code} {a_4 : List ℕ}
  {a_5 : Turing.ToPartrec.Cont},
  Turing.ToPartrec.Cont.cons₁ a a_1 a_2 = Turing.ToPartrec.Cont.cons₁ a_3 a_4 a_5 → a = a_3 ∧ a_1 = a_4 ∧ a_2 = a_5
-- Mathlib.CategoryTheory.Subobject.Limits
/-- The image of a morphism `f g : X ⟶ Y` as a `Subobject Y`.  -/
CategoryTheory.Limits.imageSubobject : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → (f : X ⟶ Y) → [CategoryTheory.Limits.HasImage f] → CategoryTheory.Subobject Y
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.ball.eq_1 : ∀ {V : Type u_1} (G : SimpleGraph V) (c : V) (r : ℕ∞), G.ball c r = {v | G.edist v c < r}
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.coe_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Max α] [inst_1 : Bot α] [inst_2 : Max β] [inst_3 : Bot β]
  [inst_4 : Max γ] [inst_5 : Bot γ] (f : SupBotHom β γ) (g : SupBotHom α β), ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Mathlib.Algebra.Group.Hom.Instances
/-- If `G` is a commutative group, then so is `OneHom M G`.  -/
OneHom.instCommGroup : {M : Type uM} → {N : Type uN} → [inst : One M] → [inst_1 : CommGroup N] → CommGroup (OneHom M N)
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.uliftFunctor_obj_coe : ∀ (X : MonCat), ↑(MonCat.uliftFunctor.obj X) = ULift.{u, v} ↑X
-- Mathlib.Data.Ordmap.Invariants
Ordnode.all_node4L : ∀ {α : Type u_1} {P : α → Prop} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α},
  Ordnode.All P (l.node4L x m y r) ↔ Ordnode.All P l ∧ P x ∧ Ordnode.All P m ∧ P y ∧ Ordnode.All P r
-- Mathlib.RingTheory.Congruence.Basic
RingCon.coe_smul : ∀ {α : Type u_1} {R : Type u_3} [inst : Add R] [inst_1 : MulOneClass R] [inst_2 : SMul α R]
  [inst_3 : IsScalarTower α R R] (c : RingCon R) (a : α) (x : R), ↑(a • x) = a • ↑x
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
/-- If `G : ComposableArrows C n`, then `G.hom : G.left ⟶ G.right` is a
transfinite composition of shape `Fin (n + 1)`.  -/
CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {n : ℕ} →
      (G : CategoryTheory.ComposableArrows C n) → CategoryTheory.TransfiniteCompositionOfShape (Fin (n + 1)) G.hom
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Roi.toList_iter_eq_toList : ∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.Rxi.IsAlwaysFinite α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Roi α}, r.iter.toList = r.toList
-- Mathlib.CategoryTheory.Adjunction.Unique
CategoryTheory.Adjunction.leftAdjointUniq_hom_app_counit_assoc : ∀ {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 F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (x : D) {Z : D} (h : x ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((adj1.leftAdjointUniq adj2).hom.app (G.obj x))
      (CategoryTheory.CategoryStruct.comp (adj2.counit.app x) h) =
    CategoryTheory.CategoryStruct.comp (adj1.counit.app x) h
-- Mathlib.Order.RelSeries
RelSeries.fromListIsChain.congr_simp : ∀ {α : Type u_1} {r : SetRel α α} (x x_1 : List α) (e_x : x = x_1) (x_ne_nil : x ≠ [])
  (hx : List.IsChain (fun x1 x2 => (x1, x2) ∈ r) x),
  RelSeries.fromListIsChain x x_ne_nil hx = RelSeries.fromListIsChain x_1 ⋯ ⋯
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxi.Iterator.Monadic.isPlausibleSuccessorOf_iff : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] {it' it : Std.IterM Id α},
  it'.IsPlausibleSuccessorOf it ↔ ∃ a, it.internalState.next = some a ∧ Std.PRange.succ? a = it'.internalState.next