mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Filtered.Small
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsCofiltered.CofilteredClosureSmall.InductiveStep.min : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {n : ℕ} →
      {X : (k : ℕ) → k < n → (t : Type (max v w)) × (t → C)} →
        {k k' : ℕ} →
          (hk : k < n) →
            (hk' : k' < n) →
              (X k hk).fst → (X k' hk').fst → CategoryTheory.IsCofiltered.CofilteredClosureSmall.InductiveStep✝ n X
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.WF.constMergeWith : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {mergeFn : α → β → β → β}
  {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp}, t₁.WF → (Std.DTreeMap.Raw.Const.mergeWith mergeFn t₁ t₂).WF
-- Mathlib.Algebra.Order.SuccPred
Order.Iio_one : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : AddMonoidWithOne α] [SuccAddOrder α] [IsBotZeroClass α] [NeZero 1],
  Set.Iio 1 = {0}
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inl_isoPushout_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {Z X Y P : C}
  {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : CategoryTheory.IsPushout f g inl inr)
  [inst_2 : CategoryTheory.Limits.HasPushout f g] {Q Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Q P ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.Limits.pushout.inl f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q hP.isoPushout.inv) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q inl) h
-- Mathlib.Data.List.Lattice
List.bagInter.eq_1 : ∀ {α : Type u_1} [inst : BEq α] (x : List α), [].bagInter x = []
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.angleDiff.eq_1 : ∀ (x y : Circle), x.angleDiff y = if (↑x).arg ≤ (↑y).arg then (↑y).arg - (↑x).arg else 2 * Real.pi + (↑y).arg - (↑x).arg
-- Mathlib.Computability.TuringMachine.Tape
Turing.ListBlank.append_assoc : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (l₁ l₂ : List Γ) (l₃ : Turing.ListBlank Γ),
  Turing.ListBlank.append (l₁ ++ l₂) l₃ = Turing.ListBlank.append l₁ (Turing.ListBlank.append l₂ l₃)
-- Mathlib.Analysis.Complex.OperatorNorm
Complex.conjCLE_enorm : ‖↑Complex.conjCLE‖ₑ = 1
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.HasRightCalculusOfFractions.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  [toIsMultiplicative : W.IsMultiplicative],
  (∀ ⦃X Y : C⦄ (φ : W.LeftFraction X Y),
      ∃ ψ, CategoryTheory.CategoryStruct.comp ψ.s φ.f = CategoryTheory.CategoryStruct.comp ψ.f φ.s) →
    (∀ ⦃X Y Y' : C⦄ (f₁ f₂ : X ⟶ Y) (s : Y ⟶ Y'),
        W s →
          CategoryTheory.CategoryStruct.comp f₁ s = CategoryTheory.CategoryStruct.comp f₂ s →
            ∃ X' t, ∃ (_ : W t), CategoryTheory.CategoryStruct.comp t f₁ = CategoryTheory.CategoryStruct.comp t f₂) →
      W.HasRightCalculusOfFractions
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_insertMany_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    k ∉ t → List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (t.insertMany l).get! k' = k
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasLimit.isoOfEquivalence_inv_π : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C}
  [inst_3 : CategoryTheory.Limits.HasLimit F] {G : CategoryTheory.Functor K C}
  [inst_4 : CategoryTheory.Limits.HasLimit G] (e : J ≌ K) (w : e.functor.comp G ≅ F) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.HasLimit.isoOfEquivalence e w).inv
      (CategoryTheory.Limits.limit.π F j) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π G (e.functor.obj j)) (w.hom.app j)
-- Lean.Compiler.IR.Format
Lean.IR.declToString : Lean.IR.Decl → String
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k a : α}
  {h' : a ∈ t.erase k}, (t.erase k).get a h' = t.get a ⋯
-- Batteries.Data.String.Lemmas
/-- `it.ValidFor l r` means that `it` is a string iterator whose underlying string is
`l.reverse ++ r`, and where the cursor is pointing at the end of `l.reverse`.  -/
String.Legacy.Iterator.ValidFor : List Char → List Char → String.Legacy.Iterator → Prop
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
AlgHom.subalgebraMap_surjective : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (S : Subalgebra R A) (f : A →ₐ[R] B),
  Function.Surjective ⇑(AlgHom.subalgebraMap S f)
-- Mathlib.LinearAlgebra.QuadraticForm.Dual
QuadraticForm.toDualProd_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) [inst_3 : Invertible 2] (i : M × M),
  Q.toDualProd i = ((QuadraticMap.associated Q) i.1 + (QuadraticMap.associated Q) i.2, i.1 - i.2)
-- Mathlib.Order.WellFoundedSet
/-- `s.IsWF` indicates that `<` is well-founded when restricted to `s`.  -/
Set.IsWF : {α : Type u_2} → [LT α] → Set α → Prop
-- Mathlib.Order.Filter.Pointwise
Filter.one_prod : ∀ {α : Type u_2} {β : Type u_3} [inst : One α] {l : Filter β}, 1 ×ˢ l = Filter.map (fun x => (1, x)) l
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.natDegree_X_sub_C : ∀ {R : Type u} [inst : Ring R] [Nontrivial R] (x : R), (Polynomial.X - Polynomial.C x).natDegree = 1
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.LambdaTheorems.mk.injEq : ∀
  (theorems theorems_1 :
    Std.HashMap (Lean.Name × Mathlib.Meta.FunProp.LambdaTheoremType) (Array Mathlib.Meta.FunProp.LambdaTheorem)),
  ({ theorems := theorems } = { theorems := theorems_1 }) = (theorems = theorems_1)
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- Predicate for an additive monoid object to be commutative.  -/
CategoryTheory.IsCommAddMonObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → (X : C) → [CategoryTheory.AddMonObj X] → Prop
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α} {fallback : β},
  (List.map Prod.fst l).contains k = false → (Std.TreeMap.ofList l cmp).getD k fallback = fallback
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.zmodRepr_lt_p : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]), x.zmodRepr < p
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
/-- The ideal `⟨Y - y(X)⟩` of `R[W]` for some `y(X)` in `R[X]`.  -/
WeierstrassCurve.Affine.CoordinateRing.YIdeal : {R : Type r} → [inst : CommRing R] → (W' : WeierstrassCurve.Affine R) → Polynomial R → Ideal W'.CoordinateRing
-- Mathlib.CategoryTheory.Adjunction.Evaluation
CategoryTheory.evaluationIsLeftAdjoint : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D] (c : C),
  ((CategoryTheory.evaluation C D).obj c).IsLeftAdjoint
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.mod_le : ∀ (a b : Ordinal.{u_4}), a % b ≤ a
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientGroup.instFirstCountableTopology : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [SeparatelyContinuousMul G] (N : Subgroup G)
  [FirstCountableTopology G], FirstCountableTopology (G ⧸ N)
-- Mathlib.Data.Matrix.PEquiv
PEquiv.toMatrix_toPEquiv_mulVec : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : NonAssocSemiring α]
  (σ : m ≃ n) (a : n → α), σ.toPEquiv.toMatrix.mulVec a = a ∘ ⇑σ
-- Init.Data.Order.Lemmas
Std.instTransNotLtOfLawfulOrderLTOfTotalOfLe : {α : Type u} →
  {x : LT α} →
    [inst : LE α] →
      [Std.LawfulOrderLT α] →
        [Std.Total fun x1 x2 => x1 ≤ x2] →
          [Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2] →
            Trans (fun x1 x2 => ¬x1 < x2) (fun x1 x2 => ¬x1 < x2) fun x1 x2 => ¬x1 < x2
-- Mathlib.Data.Nat.BitIndices
Nat.bitIndices_nodup : ∀ {n : ℕ}, n.bitIndices.Nodup
-- Lean.Elab.DocString
Lean.Doc.CodeBlockSuggestion.mk.sizeOf_spec : ∀ (name : Lean.Name) (args moreInfo : Option String),
  sizeOf { name := name, args := args, moreInfo := moreInfo } = 1 + sizeOf name + sizeOf args + sizeOf moreInfo
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.one_smul' : ∀ {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [inst : PartialOrder Γ'] [inst_1 : AddCommMonoid V] {Γ : Type u_6}
  [inst_2 : AddCommMonoid Γ] [inst_3 : PartialOrder Γ] [inst_4 : AddAction Γ Γ'] [inst_5 : IsOrderedCancelVAdd Γ Γ']
  [inst_6 : MonoidWithZero R] [inst_7 : MulActionWithZero R V] {x : HahnModule Γ' R V}, 1 • x = x
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.orderIsoIsTwoSided_apply_coe : ∀ {R : Type u_1} [inst : Ring R] (I : TwoSidedIdeal R), ↑(TwoSidedIdeal.orderIsoIsTwoSided I) = TwoSidedIdeal.asIdeal I
-- Mathlib.CategoryTheory.Widesubcategory
/-- The underlying morphism.  -/
CategoryTheory.InducedWideCategory.Hom.hom : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₂} D] →
      {F : C → D} →
        {P : CategoryTheory.MorphismProperty D} →
          [inst_1 : P.IsMultiplicative] → {X Y : CategoryTheory.InducedWideCategory D F P} → X.Hom Y → (F X ⟶ F Y)
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesOnBall.coeff_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {pf : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal},
  HasFPowerSeriesOnBall f pf x r → ∀ (v : Fin 0 → E), (pf 0) v = f x
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
HomotopicalAlgebra.AttachCells.ofArrowIso_isColimit₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a}
  {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : HomotopicalAlgebra.AttachCells g f) {Y₁ Y₂ : C} {f' : Y₁ ⟶ Y₂}
  (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f'), (c.ofArrowIso e).isColimit₁ = c.isColimit₁
-- Mathlib.Algebra.GroupWithZero.Action.Hom
ZeroHom.instIsCentralScalar : ∀ {M : Type u_1} {A : Type u_3} {B : Type u_4} [inst : Zero A] [inst_1 : Zero B] [inst_2 : SMulZeroClass M B]
  [inst_3 : SMulZeroClass Mᵐᵒᵖ B] [IsCentralScalar M B], IsCentralScalar M (ZeroHom A B)
-- Mathlib.Algebra.Homology.ShortComplex.ShortExact
CategoryTheory.ShortComplex.isIso₂_of_shortExact_of_isIso₁₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [CategoryTheory.Balanced C] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂),
  S₁.ShortExact → S₂.ShortExact → ∀ [CategoryTheory.IsIso φ.τ₁] [CategoryTheory.IsIso φ.τ₃], CategoryTheory.IsIso φ.τ₂
-- Mathlib.Data.PFun
PFun.core_mono : ∀ {α : Type u_1} {β : Type u_2} (f : α →. β) {s t : Set β}, s ⊆ t → f.core s ⊆ f.core t
-- Mathlib.Tactic.NormNum.Result
/-- Obtain a `Result` from a `BoolResult`.  -/
Mathlib.Meta.NormNum.Result.ofBoolResult : {p : Q(Prop)} → {b : Bool} → Mathlib.Meta.NormNum.BoolResult p b → Mathlib.Meta.NormNum.Result q(Prop)
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
IsPrimitiveRoot.integralPowerBasisOfPrimePow.congr_simp : ∀ {p p_1 : ℕ} (e_p : p = p_1) {k k_1 : ℕ} (e_k : k = k_1) {K : Type u} [inst : Field K] {ζ ζ_1 : K} (e_ζ : ζ = ζ_1)
  [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K] [inst_2 : IsCyclotomicExtension {p ^ k} ℚ K]
  (hζ : IsPrimitiveRoot ζ (p ^ k)), hζ.integralPowerBasisOfPrimePow = ⋯.integralPowerBasisOfPrimePow
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
ContinuousOn.clm_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {X : Type u_5} [inst_5 : TopologicalSpace X] {f : X → E →L[𝕜] F} {g : X → E} {s : Set X},
  ContinuousOn f s → ContinuousOn g s → ContinuousOn (fun x => (f x) (g x)) s
-- Mathlib.RingTheory.TensorProduct.Basic
/-- A version of `TensorProduct.ext` for `AlgHom`.

Using this as the `@[ext]` lemma instead of `Algebra.TensorProduct.ext'` allows `ext` to apply
lemmas specific to `A →ₐ[S] _` and `B →ₐ[R] _`; notably this allows recursion into nested tensor
products of algebras.

See note [partially-applied ext lemmas].  -/
Algebra.TensorProduct.ext : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Semiring C] [inst_6 : Algebra R C]
  [inst_7 : CommSemiring S] [inst_8 : Algebra S A] [inst_9 : Algebra R S] [inst_10 : Algebra S C]
  [inst_11 : IsScalarTower R S A] [inst_12 : IsScalarTower R S C] ⦃f g : TensorProduct R A B →ₐ[S] C⦄,
  f.comp Algebra.TensorProduct.includeLeft = g.comp Algebra.TensorProduct.includeLeft →
    (AlgHom.restrictScalars R f).comp Algebra.TensorProduct.includeRight =
        (AlgHom.restrictScalars R g).comp Algebra.TensorProduct.includeRight →
      f = g
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.disjoint_map_of_ker_le_right : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {p q : Submodule R M},
  Disjoint p q → f.ker ≤ q → Disjoint (Submodule.map f p) (Submodule.map f q)
-- Init.Data.Array.InsertIdx
Array.getElem?_insertIdx_of_lt : ∀ {α : Type u} {xs : Array α} {x : α} {i k : ℕ} (w : i ≤ xs.size), k < i → (xs.insertIdx i x w)[k]? = xs[k]?
-- Mathlib.Algebra.Homology.Embedding.TruncLE
HomologicalComplex.ιTruncLE_naturality : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [inst_2 : e.IsTruncLE]
  [inst_3 : ∀ (i' : ι'), K.HasHomology i'] [inst_4 : ∀ (i' : ι'), L.HasHomology i']
  [inst_5 : CategoryTheory.Limits.HasZeroObject C],
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncLEMap φ e) (L.ιTruncLE e) =
    CategoryTheory.CategoryStruct.comp (K.ιTruncLE e) φ
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
/-- `F : D ⥤ K ⥤ C` preserves limits of shape `J` if it does for each `k : K`.  -/
CategoryTheory.Limits.preservesLimitsOfShape_of_evaluation : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K]
  (F : CategoryTheory.Functor D (CategoryTheory.Functor K C)) (J : Type u_1)
  [inst_3 : CategoryTheory.Category.{v_1, u_1} J],
  (∀ (k : K), CategoryTheory.Limits.PreservesLimitsOfShape J (F.comp ((CategoryTheory.evaluation K C).obj k))) →
    CategoryTheory.Limits.PreservesLimitsOfShape J F
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.IsLowerSet.lowerSet_le_lower : ∀ {α : Type u_1} [inst : Preorder α] {t₁ t₂ : TopologicalSpace α} [Topology.IsLowerSet α] [Topology.IsLower α], t₁ ≤ t₂
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.OneCocycle.toOneCochain : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {G : CategoryTheory.Functor Cᵒᵖ GrpCat} →
      {I : Type w'} →
        {U : I → C} → CategoryTheory.PresheafOfGroups.OneCocycle G U → CategoryTheory.PresheafOfGroups.OneCochain G U
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.eq_symm_apply : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) {p₁ : P₂} {p₂ : P₁},
  p₂ = e.symm p₁ ↔ e p₂ = p₁
-- Mathlib.Algebra.Quandle
UnitalShelf.toShelf : {α : Type u} → [self : UnitalShelf α] → Shelf α
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.nnnorm_fst : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : StarRing A]
  [CStarRing A] (a : DoubleCentralizer 𝕜 A), ‖a.toProd.1‖₊ = ‖a‖₊
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.eq_prod_roots : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} [inst_1 : IsDomain R],
  f.Splits → f = Polynomial.C f.leadingCoeff * (Multiset.map (fun x => Polynomial.X - Polynomial.C x) f.roots).prod
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
/-- If `f : R → ℝ` is a nonzero, nonnegative, multiplicatively bounded function, then
`seminormFromBounded' f 1 = 1`.  -/
seminormFromBounded_one : ∀ {R : Type u_1} [inst : CommRing R] {f : R → ℝ} {c : ℝ},
  f ≠ 0 → 0 ≤ f → (∀ (x y : R), f (x * y) ≤ c * f x * f y) → seminormFromBounded' f 1 = 1
-- Mathlib.Combinatorics.Graph.Basic
/-- `G.incidenceSet x` is the set of edges incident to `x` in `G`.  -/
Graph.incidenceSet : {α : Type u_1} → {β : Type u_2} → {G : Graph α β} → α → Set β
-- Batteries.Data.AssocList
/-- Converts a list into an `AssocList`. This is the inverse function to `AssocList.toList`.  -/
List.toAssocList : {α : Type u_1} → {β : Type u_2} → List (α × β) → Batteries.AssocList α β
-- Init.Data.Int.DivMod.Lemmas
Int.emod_eq_emod_iff_emod_sub_eq_zero : ∀ {m n k : ℤ}, m % n = k % n ↔ (m - k) % n = 0
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.mk.sizeOf_spec : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  [inst_2 : SizeOf X] [inst_3 : SizeOf Y] (toContinuousMap : C(↑unitInterval × X, Y))
  (map_zero_left : ∀ (x : X), toContinuousMap.toFun (0, x) = f₀ x)
  (map_one_left : ∀ (x : X), toContinuousMap.toFun (1, x) = f₁ x),
  sizeOf { toContinuousMap := toContinuousMap, map_zero_left := map_zero_left, map_one_left := map_one_left } =
    1 + sizeOf toContinuousMap
-- Lean.CoreM
_private.Lean.CoreM.0.Lean.DeclNameGenerator.mkUniqueName.isConflict : Lean.Environment → Lean.Name → Bool
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.Trimmed.nil : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil.Trimmed
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_nat_eq_sum_factorization : ∀ (n : ℕ), Real.log ↑n = n.factorization.sum fun p t => ↑t * Real.log ↑p
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
/-- Notation for composition of based functors.  -/
CategoryTheory.BasedFunctor.«term_⋙_» : Lean.TrailingParserDescr
-- Mathlib.AlgebraicTopology.SimplicialSet.Presentable
SSet.Finite.exists_epi_from_isCardinalPresentable : ∀ (X : SSet) [X.Finite], ∃ Y, ∃ (_ : Y.Finite) (_ : CategoryTheory.IsFinitelyPresentable Y), ∃ p, CategoryTheory.Epi p
-- Mathlib.LinearAlgebra.Semisimple
Module.End.IsSemisimple_smul : ∀ {M : Type u_2} [inst : AddCommGroup M] {K : Type u_3} [inst_1 : Field K] [inst_2 : Module K M] {f : Module.End K M}
  (t : K), f.IsSemisimple → (t • f).IsSemisimple
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.Equivalence_mk'_counitInv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C)
  (unit_iso : CategoryTheory.Functor.id C ≅ functor.comp inverse)
  (counit_iso : inverse.comp functor ≅ CategoryTheory.Functor.id D)
  (f :
    ∀ (X : C),
      CategoryTheory.CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) =
        CategoryTheory.CategoryStruct.id (functor.obj X)),
  { functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso,
        functor_unitIso_comp := f }.counitInv =
    counit_iso.inv
-- Init.Data.UInt.Lemmas
UInt16.ofNat_finVal : ∀ (n : Fin UInt16.size), UInt16.ofNat ↑n = UInt16.ofFin n
-- Mathlib.NumberTheory.Padics.PadicNumbers
PadicSeq.eq_zero_iff_equiv_zero : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (f : PadicSeq p), CauSeq.Completion.mk f = 0 ↔ f ≈ 0
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instDiv.eq_1 : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Div G] [inst_2 : ContinuousDiv G],
  SeparationQuotient.instDiv = { div := Quotient.map₂ (fun x1 x2 => x1 / x2) ⋯ }
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.topEquiv_symm_apply_coe : ∀ {R : Type u} [inst : NonAssocRing R] (r : R), ↑(Subring.topEquiv.symm r) = r
-- Init.Data.Iterators.Lemmas.Monadic.Basic
_private.Init.Data.Iterators.Lemmas.Monadic.Basic.0.Std.IterM.inductSteps.eq_def : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β]
  [inst_1 : Std.Iterators.Finite α m] (motive : Std.IterM m β → Sort x)
  (step :
    (it : Std.IterM m β) →
      ({it' : Std.IterM m β} → {out : β} → it.IsPlausibleStep (Std.IterStep.yield it' out) → motive it') →
        ({it' : Std.IterM m β} → it.IsPlausibleStep (Std.IterStep.skip it') → motive it') → motive it)
  (it : Std.IterM m β),
  Std.IterM.inductSteps motive step it =
    step it (fun {it'} {x} x_1 => Std.IterM.inductSteps motive step it') fun {it'} x =>
      Std.IterM.inductSteps motive step it'
-- Mathlib.Combinatorics.SimpleGraph.Operations
SimpleGraph.sdiff_edge : ∀ {V : Type u_1} (G : SimpleGraph V) {u v : V}, ¬G.Adj u v → G \ SimpleGraph.edge u v = G
-- Mathlib.ModelTheory.Syntax
/-- Raises all of the `Fin`-indexed variables of a term greater than or equal to `m` by `n'`.  -/
FirstOrder.Language.Term.liftAt : {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → (n' : ℕ) → ℕ → L.Term (α ⊕ Fin n) → L.Term (α ⊕ Fin (n + n'))
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.Syntax.splitNameLitAux : Substring.Raw → List Substring.Raw → List Substring.Raw
-- Mathlib.RingTheory.Perfection
PreTilt.coeff_iterate_frobenius : ∀ {O : Type u₂} [inst : CommRing O] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] [inst_2 : Fact ¬IsUnit ↑p] (m n : ℕ)
  (x : PreTilt O p), (PreTilt.coeff (m + n)) ((⇑(frobenius (PreTilt O p) p))^[n] x) = (PreTilt.coeff m) x
-- Lean.Elab.Import
Lean.Elab.parseImports : String → optParam (Option String) none → IO (Array Lean.Import × Lean.Position × Lean.MessageLog)
-- Mathlib.Data.Set.Card
Set.ncard_compl_add_ncard : ∀ {α : Type u_1} (s : Set α),
  autoParam s.Finite Set.ncard_compl_add_ncard._auto_1 →
    autoParam sᶜ.Finite Set.ncard_compl_add_ncard._auto_3 → sᶜ.ncard + s.ncard = Nat.card α
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.aleph0_le_preAleph : ∀ {o : Ordinal.{u_1}}, Cardinal.aleph0 ≤ Cardinal.preAleph o ↔ Ordinal.omega0 ≤ o
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for the inverse `Iso.symm η`.  -/
Mathlib.Tactic.BicategoryLike.MonadMor₂Iso.symmM : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m] →
    Mathlib.Tactic.BicategoryLike.Mor₂Iso → m Mathlib.Tactic.BicategoryLike.Mor₂Iso
-- Mathlib.LinearAlgebra.Projectivization.Subspace
Projectivization.Subspace.span_sup : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {S : Set (Projectivization K V)} {W : Projectivization.Subspace K V},
  Projectivization.Subspace.span S ⊔ W = Projectivization.Subspace.span (S ∪ ↑W)