mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.congr.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] (G' : AddSubgroup G) (H' : AddSubgroup H)
  [inst_2 : G'.Normal] [inst_3 : H'.Normal] (e : G ≃+ H) (he : AddSubgroup.map (↑e) G' = H'),
  QuotientAddGroup.congr G' H' e he =
    { toFun := ⇑(QuotientAddGroup.map G' H' ↑e ⋯), invFun := ⇑(QuotientAddGroup.map H' G' ↑e.symm ⋯), left_inv := ⋯,
      right_inv := ⋯, map_add' := ⋯ }
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
Bundle.contMDiffAt_proj : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E] {p : Bundle.TotalSpace F E},
  ContMDiffAt (IB.prod (modelWithCornersSelf 𝕜 F)) IB n Bundle.TotalSpace.proj p
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getEntryLE?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.Equiv t₂ → t₁.getEntryLE? k = t₂.getEntryLE? k
-- Lean.Parser.Term
Lean.Parser.Term.waitIfTypeMVar.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Setup
Lean.ModuleSetup.mk.inj : ∀ {name : Lean.Name} {package? : Option Lean.PkgId} {isModule : Bool} {imports? : Option (Array Lean.Import)}
  {importArts : Lean.NameMap Lean.ImportArtifacts} {dynlibs : Array System.FilePath} {plugins : Array Lean.Plugin}
  {options : Lean.LeanOptions} {name_1 : Lean.Name} {package?_1 : Option Lean.PkgId} {isModule_1 : Bool}
  {imports?_1 : Option (Array Lean.Import)} {importArts_1 : Lean.NameMap Lean.ImportArtifacts}
  {dynlibs_1 : Array System.FilePath} {plugins_1 : Array Lean.Plugin} {options_1 : Lean.LeanOptions},
  { name := name, package? := package?, isModule := isModule, imports? := imports?, importArts := importArts,
        dynlibs := dynlibs, plugins := plugins, options := options } =
      { name := name_1, package? := package?_1, isModule := isModule_1, imports? := imports?_1,
        importArts := importArts_1, dynlibs := dynlibs_1, plugins := plugins_1, options := options_1 } →
    name = name_1 ∧
      package? = package?_1 ∧
        isModule = isModule_1 ∧
          imports? = imports?_1 ∧
            importArts = importArts_1 ∧ dynlibs = dynlibs_1 ∧ plugins = plugins_1 ∧ options = options_1
-- Lean.Data.SSet
Lean.SSet.forM : {α : Type u} →
  [inst : BEq α] →
    [inst_1 : Hashable α] →
      {m : Type u_1 → Type u_2} → [Monad m] → Lean.SSet α → (α → m PUnit.{u_1 + 1}) → m PUnit.{u_1 + 1}
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_diff_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₂ → (t₁ \ t₂)[k]! = t₁[k]!
-- Batteries.Data.Array.Basic
_private.Batteries.Data.Array.Basic.0.Array.unsafe_sizeFitsUSize : ∀ {α : Type u_1} (a : Array α), Array.SizeFitsUSize✝ a
-- Mathlib.Topology.NhdsWithin
nhdsSetWithin_univ : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α}, nhdsSetWithin s Set.univ = nhdsSet s
-- Mathlib.Topology.Category.CompHausLike.Limits
CompHausLike.pullback.hom_ext : ∀ {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [inst : CompHausLike.HasExplicitPullback f g]
  {Z : CompHausLike P} (a b : Z ⟶ CompHausLike.pullback f g),
  CategoryTheory.CategoryStruct.comp a (CompHausLike.pullback.fst f g) =
      CategoryTheory.CategoryStruct.comp b (CompHausLike.pullback.fst f g) →
    CategoryTheory.CategoryStruct.comp a (CompHausLike.pullback.snd f g) =
        CategoryTheory.CategoryStruct.comp b (CompHausLike.pullback.snd f g) →
      a = b
-- Mathlib.Order.Completion
/-- We can never have a computable decidable instance, for the same reason we can't on `Set α`.  -/
DedekindCut.instDecidableLE : {α : Type u_1} → [inst : Preorder α] → DecidableLE (DedekindCut α)
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- If a group satisfies the universal property of a free group with respect to a given type, then
it is free. Here, the universal property is expressed as in `IsFreeGroup.lift` and its
properties.  -/
IsFreeGroup.ofLift : ∀ {G : Type u} [inst : Group G] (X : Type u) (of : X → G)
  (lift : {H : Type u} → [inst_1 : Group H] → (X → H) ≃ (G →* H)),
  (∀ {H : Type u} [inst_1 : Group H] (f : X → H) (a : X), (lift f) (of a) = f a) → IsFreeGroup G
-- Init.Data.Nat.Lemmas
Nat.add_eq_one_iff : ∀ {m n : ℕ}, m + n = 1 ↔ m = 0 ∧ n = 1 ∨ m = 1 ∧ n = 0
-- Mathlib.RingTheory.Radical.Basic
/-- If `x` is a unit, then the finset of prime factors of `x` is empty.
The converse is true with a nonzero assumption, see `primeFactors_eq_empty_iff`.
 -/
UniqueFactorizationMonoid.primeFactors_of_isUnit : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a : M}, IsUnit a → UniqueFactorizationMonoid.primeFactors a = ∅
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.lift_neg_apply : ∀ {α : Type u} {G : Type u_1} [inst : AddCommGroup G] (f : α → G) (a : FreeAbelianGroup α),
  (FreeAbelianGroup.lift (-f)) a = -(FreeAbelianGroup.lift f) a
-- Mathlib.Probability.Process.LocalProperty
/-- A localizing sequence, witness of the local property of the stochastic process.  -/
ProbabilityTheory.Locally.localSeq : {ι : Type u_1} →
  {Ω : Type u_2} →
    {E : Type u_3} →
      {mΩ : MeasurableSpace Ω} →
        {P : MeasureTheory.Measure Ω} →
          [inst : LinearOrder ι] →
            {𝓕 : MeasureTheory.Filtration ι mΩ} →
              {X : ι → Ω → E} →
                {p : (ι → Ω → E) → Prop} →
                  [inst_1 : OrderBot ι] →
                    [inst_2 : TopologicalSpace ι] →
                      [inst_3 : OrderTopology ι] →
                        [inst_4 : Zero E] → ProbabilityTheory.Locally p 𝓕 X P → ℕ → Ω → WithTop ι
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.CustomEliminator.induction : Lean.Meta.CustomEliminator → Bool
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.fromLoop.eq_1 : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} [inst_1 : DecidableEq N] (i : N)
  (p : LoopSpace (↑(GenLoop { j // j ≠ i } X x)) GenLoop.const),
  GenLoop.fromLoop i p =
    ⟨({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp p.toContinuousMap).uncurry.comp ↑(Cube.splitAt i), ⋯⟩
-- Mathlib.NumberTheory.NumberField.Units.Regulator
NumberField.Units.regOfFamily_eq_det' : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (u : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ),
  NumberField.Units.regOfFamily u =
    |(Matrix.of fun i =>
          (NumberField.Units.logEmbedding K) (Additive.ofMul (u ((NumberField.Units.equivFinRank K).symm i)))).det|
-- Mathlib.Analysis.InnerProductSpace.Basic
norm_inner_eq_norm_tfae : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E),
  [‖inner 𝕜 x y‖ = ‖x‖ * ‖y‖, x = 0 ∨ y = (inner 𝕜 x y / inner 𝕜 x x) • x, x = 0 ∨ ∃ r, y = r • x,
      x = 0 ∨ y ∈ 𝕜 ∙ x].TFAE
-- Mathlib.Geometry.Manifold.Notation
/-- Attempt to find a model with corners from a normed field.
We attempt to find a global instance here.  -/
_private.Mathlib.Geometry.Manifold.Notation.0.Manifold.Elab.findModelInner.fromNormedField : Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.hom_id : ∀ (R : Type u) [inst : Ring R] [inst_1 : TopologicalSpace R] (X : TopModuleCat R),
  CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X) = ContinuousLinearMap.id R ↑X.toModuleCat
-- Init.Data.Int.Gcd
Int.lcm_eq_left : ∀ {a b : ℤ}, 0 ≤ a → b ∣ a → ↑(a.lcm b) = a
-- Mathlib.Tactic.Peel
/-- The list of constants that are regarded as being quantifiers.  -/
Mathlib.Tactic.Peel.quantifiers : List Lean.Name
-- Mathlib.Order.Filter.CountableInter
Filter.mem_ofCountableInter : ∀ {α : Type u_2} {l : Set (Set α)} (hl : ∀ (S : Set (Set α)), S.Countable → S ⊆ l → ⋂₀ S ∈ l)
  (h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l) {s : Set α}, s ∈ Filter.ofCountableInter l hl h_mono ↔ s ∈ l
-- Mathlib.Data.Nat.Fib.Zeckendorf
Nat.isZeckendorfRep_zeckendorf : ∀ (n : ℕ), n.zeckendorf.IsZeckendorfRep
-- Mathlib.MeasureTheory.Constructions.HaarToSphere
MeasureTheory.integral_fun_norm_addHaar : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] {F : Type u_2}
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [Nontrivial E] (μ : MeasureTheory.Measure E)
  [FiniteDimensional ℝ E] [BorelSpace E] [μ.IsAddHaarMeasure] (f : ℝ → F),
  ∫ (x : E), f ‖x‖ ∂μ =
    Module.finrank ℝ E • μ.real (Metric.ball 0 1) • ∫ (y : ℝ) in Set.Ioi 0, y ^ (Module.finrank ℝ E - 1) • f y
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.mem_factorSet_top : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] {p : Associates α} {hp : Irreducible p}, p ∈ ⊤
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
/-- The base change of `B[M]` to an `R`-algebra `A` is isomorphic to `(A ⊗[R] B)[M]`
as an `A`-algebra.  -/
AddMonoidAlgebra.lTensorAlgEquiv : (R : Type u_1) →
  {M : Type u_2} →
    (A : Type u_5) →
      (B : Type u_6) →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring A] →
            [inst_2 : CommSemiring B] →
              [inst_3 : Algebra R A] →
                [inst_4 : Algebra R B] →
                  [inst_5 : AddCommMonoid M] →
                    TensorProduct R (AddMonoidAlgebra A M) B ≃ₐ[R] AddMonoidAlgebra (TensorProduct R A B) M
-- Aesop.Util.UnorderedArraySet
Aesop.UnorderedArraySet.instToString : {α : Type u_1} → [inst : BEq α] → [ToString α] → ToString (Aesop.UnorderedArraySet α)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.lift_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift f g) CategoryTheory.Limits.prod.snd = g
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
/-- Formal operation of negation on general linear group on even cardinality `n` given by negating
each element.  -/
Matrix.instNegSubtypeGeneralLinearGroupMemSubgroupGLPos : {n : Type u} →
  {R : Type v} →
    [inst : DecidableEq n] →
      [inst_1 : Fintype n] →
        [inst_2 : CommRing R] →
          [inst_3 : LinearOrder R] →
            [inst_4 : IsStrictOrderedRing R] → [Fact (Even (Fintype.card n))] → Neg ↥(Matrix.GLPos n R)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.exp_mul_I_periodic : Function.Periodic (fun x => Complex.exp (x * Complex.I)) (2 * ↑Real.pi)
-- Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
/-- Assume `eᵢ` and `eᵢ'` are trivializations of the bundles `Eᵢ` over base `B` with fiber `Fᵢ`
(`i ∈ {1,2}`), then `Pretrivialization.continuousAlternatingMapCoordChange 𝕜 ι e₁ e₁' e₂ e₂'`
is the coordinate change function between the two induced (pre)trivializations
`Pretrivialization.continuousAlternatingMap 𝕜 ι e₁ e₂`
and `Pretrivialization.continuousAlternatingMap 𝕜 ι e₁' e₂'`
of the bundle of continuous alternating maps.  -/
Bundle.Pretrivialization.continuousAlternatingMapCoordChange : (𝕜 : Type u_1) →
  (ι : Type u_2) →
    [inst : NontriviallyNormedField 𝕜] →
      {B : Type u_3} →
        [inst_1 : TopologicalSpace B] →
          {F₁ : Type u_4} →
            [inst_2 : NormedAddCommGroup F₁] →
              [inst_3 : NormedSpace 𝕜 F₁] →
                {E₁ : B → Type u_5} →
                  [inst_4 : (x : B) → AddCommGroup (E₁ x)] →
                    [inst_5 : (x : B) → Module 𝕜 (E₁ x)] →
                      [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] →
                        {F₂ : Type u_6} →
                          [inst_7 : NormedAddCommGroup F₂] →
                            [inst_8 : NormedSpace 𝕜 F₂] →
                              {E₂ : B → Type u_7} →
                                [inst_9 : (x : B) → AddCommGroup (E₂ x)] →
                                  [inst_10 : (x : B) → Module 𝕜 (E₂ x)] →
                                    [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] →
                                      (e₁ e₁' : Bundle.Trivialization F₁ Bundle.TotalSpace.proj) →
                                        (e₂ e₂' : Bundle.Trivialization F₂ Bundle.TotalSpace.proj) →
                                          [Bundle.Trivialization.IsLinear 𝕜 e₁] →
                                            [Bundle.Trivialization.IsLinear 𝕜 e₁'] →
                                              [Bundle.Trivialization.IsLinear 𝕜 e₂] →
                                                [Bundle.Trivialization.IsLinear 𝕜 e₂'] →
                                                  B → F₁ [⋀^ι]→L[𝕜] F₂ →L[𝕜] F₁ [⋀^ι]→L[𝕜] F₂
-- Mathlib.Order.KrullDimension
Order.krullDim_eq_zero_iff_of_orderBot : ∀ {α : Type u_3} [inst : PartialOrder α] [OrderBot α], Order.krullDim α = 0 ↔ Subsingleton α
-- Init.Grind.Ordered.Linarith
_private.Init.Grind.Ordered.Linarith.0.Lean.Grind.Linarith.Poly.denote'_go_eq_denote : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] (ctx : Lean.Grind.Linarith.Context α) (p : Lean.Grind.Linarith.Poly)
  (r : α), Lean.Grind.Linarith.Poly.denote'.go ctx r p = Lean.Grind.Linarith.Poly.denote ctx p + r
-- Aesop.Index
Aesop.instInhabitedIndex.default : {α : Type} → Aesop.Index α
-- Mathlib.Order.CompleteBooleanAlgebra
CompleteDistribLattice.mk : {α : Type u_1} →
  [toFrame : Order.Frame α] →
    [toSDiff : SDiff α] →
      (∀ (a b c : α), a \ b ≤ c ↔ a ≤ b ⊔ c) → [toHNot : HNot α] → (∀ (a : α), ⊤ \ a = ￢a) → CompleteDistribLattice α
-- Mathlib.Analysis.Convex.Gauge
gauge_neg_set_eq_gauge_neg : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} (x : E), gauge (-s) x = gauge s (-x)
-- Mathlib.Logic.Equiv.Prod
/-- `PProd α β` is equivalent to `α × β`  -/
Equiv.pprodEquivProd : {α : Type u_9} → {β : Type u_10} → α ×' β ≃ α × β
-- Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
alternatingGroup.commutator_perm_le : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α], commutator (Equiv.Perm α) ≤ alternatingGroup α
-- Lean.Declaration
Lean.OpaqueVal.isUnsafeEx : Lean.OpaqueVal → Bool
-- Mathlib.Data.Nat.Hyperoperation
hyperoperation_one : ∀ (m k : ℕ), hyperoperation 1 m k = m + k
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.equivBoundedOfCompact_symm_apply : ∀ (α : Type u_1) (β : Type u_2) [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : PseudoMetricSpace β],
  ⇑(ContinuousMap.equivBoundedOfCompact α β).symm = BoundedContinuousFunction.toContinuousMap
-- Mathlib.Data.Multiset.AddSub
Multiset.add_left_inj : ∀ {α : Type u_1} {s t u : Multiset α}, s + u = t + u ↔ s = t
-- Mathlib.Order.Hom.Basic
OrderHom.coe_mk : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α → β) (hf : Monotone f),
  ⇑{ toFun := f, monotone' := hf } = f
-- Lean.Elab.InfoTree.Types
Lean.Elab.FieldInfo : Type
-- Std.Http.Data.Status
/-- 404 Not Found
 -/
Std.Http.Status.notFound : Std.Http.Status
-- Mathlib.Algebra.Group.Hom.Defs
OneHom.cancel_right : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : One M] [inst_1 : One N] [inst_2 : One P] {g₁ g₂ : OneHom N P}
  {f : OneHom M N}, Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.Order.Interval.Set.Image
StrictMono.mapsTo_Ioc : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : PartialOrder α] [inst_1 : Preorder β] {a b : α},
  StrictMono f → Set.MapsTo f (Set.Ioc a b) (Set.Ioc (f a) (f b))
-- Init.Data.SInt.Bitwise
ISize.or_self : ∀ {a : ISize}, a ||| a = a
-- Init.Data.List.Lemmas
List.map_eq_foldr : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α}, List.map f l = List.foldr (fun a bs => f a :: bs) [] l
-- Mathlib.NumberTheory.LocalField.Basic
IsNonarchimedeanLocalField.instIsCyclicUnitsValueGroupWithZero : ∀ (K : Type u_1) [inst : Field K] [inst_1 : ValuativeRel K] [inst_2 : TopologicalSpace K]
  [IsNonarchimedeanLocalField K], IsCyclic (ValuativeRel.ValueGroupWithZero K)ˣ
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.setToL1_mono_left' : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {G'' : Type u_8} [inst_2 : NormedAddCommGroup G''] [inst_3 : PartialOrder G'']
  [IsOrderedAddMonoid G''] [inst_5 : NormedSpace ℝ G''] [inst_6 : CompleteSpace G''] [OrderClosedTopology G'']
  {T T' : Set α → E →L[ℝ] G''} {C C' : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C'),
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x) →
    ∀ (f : ↥(MeasureTheory.Lp E 1 μ)), (MeasureTheory.L1.setToL1 hT) f ≤ (MeasureTheory.L1.setToL1 hT') f
-- Mathlib.NumberTheory.Padics.PadicNumbers
PadicSeq.not_equiv_zero_const_of_nonzero : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {q : ℚ}, q ≠ 0 → ¬CauSeq.const (padicNorm p) q ≈ 0
-- Mathlib.LinearAlgebra.Projectivization.Subspace
Projectivization.Subspace.mk : {K : Type u_1} →
  {V : Type u_2} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] →
          (carrier : Set (Projectivization K V)) →
            (∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0),
                Projectivization.mk K v hv ∈ carrier →
                  Projectivization.mk K w hw ∈ carrier → Projectivization.mk K (v + w) hvw ∈ carrier) →
              Projectivization.Subspace K V
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.face_restrict : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} (s : Affine.Simplex k P n) {S : AffineSubspace k P}
  (hS : affineSpan k (Set.range s.points) ≤ S) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : fs.card = m + 1),
  (s.restrict S hS).face h = (s.face h).restrict S ⋯
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
AEMeasurable.ennreal_toNNReal : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → ENNReal} {μ : MeasureTheory.Measure α},
  AEMeasurable f μ → AEMeasurable (fun x => (f x).toNNReal) μ
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.sum_lt : ∀ {n d : ℕ}, ∑ i, d * (2 * d + 1) ^ ↑i < (2 * d + 1) ^ n
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
of the real line. If `f` is differentiable on the interior of `D` and `f'` is nonnegative, then
`f` is a monotone function on `D`.  -/
monotoneOn_of_deriv_nonneg : ∀ {D : Set ℝ},
  Convex ℝ D →
    ∀ {f : ℝ → ℝ},
      ContinuousOn f D → DifferentiableOn ℝ f (interior D) → (∀ x ∈ interior D, 0 ≤ deriv f x) → MonotoneOn f D
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.DominatedFinMeasAdditive.eq_zero : ∀ {α : Type u_1} {β : Type u_8} [inst : NormedAddCommGroup β] {T : Set α → β} {C : ℝ} {x : MeasurableSpace α},
  MeasureTheory.DominatedFinMeasAdditive 0 T C → ∀ {s : Set α}, MeasurableSet s → T s = 0
-- Mathlib.MeasureTheory.Function.UniformIntegrable
MeasureTheory.MemLp.eLpNorm_indicator_le : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {p : ENNReal} {f : α → β},
  1 ≤ p →
    p ≠ ⊤ →
      MeasureTheory.MemLp f p μ →
        ∀ {ε : ℝ},
          0 < ε →
            ∃ δ,
              ∃ (_ : 0 < δ),
                ∀ (s : Set α),
                  MeasurableSet s →
                    μ s ≤ ENNReal.ofReal δ → MeasureTheory.eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
/-- Constructor for edges in the nerve of a category. (See also `homEquiv`.)  -/
CategoryTheory.nerve.edgeMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {x y : C} → (x ⟶ y) → SSet.Edge (CategoryTheory.nerveEquiv.symm x) (CategoryTheory.nerveEquiv.symm y)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.mem_unitOfList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α},
  k ∈ Std.DHashMap.Const.unitOfList l ↔ l.contains k = true
-- Std.Data.TreeMap.Raw.Lemmas
/-- Simpler variant of `getElem!_filterMap` when `LawfulEqCmp` is available.  -/
Std.TreeMap.Raw.getElem!_filterMap' : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst : Inhabited γ] {f : α → β → Option γ} {k : α},
  t.WF → (Std.TreeMap.Raw.filterMap f t)[k]! = (t[k]?.bind (f k)).get!
-- Mathlib.Order.WithBot
WithTop.decidableLT : {α : Type u_1} → [inst : LT α] → [DecidableLT α] → DecidableLT (WithTop α)
-- Aesop.Rule
Aesop.UnfoldRule.name : Aesop.UnfoldRule → Aesop.RuleName
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Zipper.done.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} [inst : SizeOf α] [inst_1 : (a : α) → SizeOf (β a)],
  sizeOf Std.DTreeMap.Internal.Zipper.done = 1
-- Mathlib.Data.PNat.Prime
PNat.dvd_gcd : ∀ {m n k : ℕ+}, k ∣ m → k ∣ n → k ∣ m.gcd n
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.size_tail?_lt : ∀ {α : Type u_1} {le : α → α → Bool} {s' s : Batteries.PairingHeapImp.Heap α},
  Batteries.PairingHeapImp.Heap.tail? le s = some s' → s'.size < s.size
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.instNonempty : ∀ (A : Type u_3) (E : Type u_4) [Nonempty E], Nonempty (WithCStarModule A E)
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.coe_sub : ∀ {α : Type u} [inst : TopologicalSpace α] {R : Type u_2} [inst_1 : PseudoMetricSpace R] [inst_2 : Sub R]
  [inst_3 : BoundedSub R] [inst_4 : ContinuousSub R] (f g : BoundedContinuousFunction α R), ⇑(f - g) = ⇑f - ⇑g
-- Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
CategoryTheory.ObjectProperty.prop_of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderIsomorphisms] {X Y : C} (e : X ≅ Y), P X → P Y
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.below.getThenInsertIfNew?₀ : ∀ {α : Type u}
  {motive : {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → (a : Std.DHashMap.Raw α β) → a.WF → Prop}
  {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {m : Std.DHashMap.Raw α β}
  {h : 0 < m.buckets.size} {a : α} {b : β a} (a_1 : m.WF),
  Std.DHashMap.Raw.WF.below a_1 → motive m a_1 → Std.DHashMap.Raw.WF.below ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.equalizer.congr_simp : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f f_1 : X ⟶ Y) (e_f : f = f_1) (g g_1 : X ⟶ Y)
  (e_g : g = g_1) [inst_1 : CategoryTheory.Limits.HasEqualizer f g],
  CategoryTheory.Limits.equalizer f g = CategoryTheory.Limits.equalizer f_1 g_1
-- Mathlib.Topology.UniformSpace.Basic
ball_preimage : ∀ {α : Type ua} {β : Type ub} {f : α → β} {U : SetRel β β} {x : α},
  UniformSpace.ball x (Prod.map f f ⁻¹' U) = f ⁻¹' UniformSpace.ball (f x) U
-- Init.Data.Int.Order
Int.lt_of_le_of_lt : ∀ {a b c : ℤ}, a ≤ b → b < c → a < c
-- Mathlib.Algebra.Group.Action.Faithful
VAddAssocClass.to₁₂₃ : ∀ (M : Type u_4) (N : Type u_5) (P : Type u_6) (Q : Type u_7) [inst : VAdd M N] [inst_1 : VAdd M P] [inst_2 : VAdd M Q]
  [inst_3 : VAdd N P] [inst_4 : VAdd N Q] [inst_5 : VAdd P Q] [FaithfulVAdd P Q] [VAddAssocClass M N Q]
  [VAddAssocClass M P Q] [VAddAssocClass N P Q], VAddAssocClass M N P
-- Mathlib.CategoryTheory.Presentable.LocallyPresentable
/-- A category `C` is accessible if it is `κ`-accessible
for some regular cardinal `κ`.  -/
CategoryTheory.IsAccessibleCategory : (C : Type u) → [hC : CategoryTheory.Category.{v, u} C] → Prop
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.Valid.prev : ∀ {it : String.Legacy.Iterator}, it.Valid → it.prev.Valid