mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.WittVector.Truncated
WittVector.truncate_liftFun : ∀ {p : ℕ} (n : ℕ) {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] {S : Type u_2} [inst_2 : Semiring S]
  {f : (k : ℕ) → S →+* TruncatedWittVector p k R},
  (∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁) →
    ∀ (s : S), (WittVector.truncate n) (WittVector.liftFun f s) = (f n) s
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- The affine version of `LinearMap.map_span`.  -/
AffineMap.map_vectorSpan : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) {s : Set P₁},
  Submodule.map f.linear (vectorSpan k s) = vectorSpan k (⇑f '' s)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- Adjoint equivalences between two objects.  -/
CategoryTheory.Bicategory.Equivalence : {B : Type u₁} → [CategoryTheory.Bicategory B] → B → B → Type (max v₁ w₁)
-- Mathlib.Data.ZMod.Basic
ZMod.natCast_toNat : ∀ (p : ℕ) {z : ℤ}, 0 ≤ z → ↑z.toNat = ↑z
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_alter_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  [inst : Inhabited β] {f : Option β → Option β}, (t.alter k f)[k]! = (f t[k]?).get!
-- Mathlib.Data.List.Sublists
List.mem_sublistsLen : ∀ {α : Type u} {n : ℕ} {l l' : List α}, l' ∈ List.sublistsLen n l ↔ l'.Sublist l ∧ l'.length = n
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.orderTop_le_orderTop_smul : ∀ {R : Type u_3} {V : Type u_8} [inst : Zero V] [inst_1 : SMulZeroClass R V] {Γ : Type u_9} [inst_2 : LinearOrder Γ]
  (r : R) (x : HahnSeries Γ V), x.orderTop ≤ (r • x).orderTop
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.twoShortAddLong.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N)
  [inst_5 : P.EmbeddedG2],
  RootPairing.EmbeddedG2.twoShortAddLong P =
    (P.reflectionPerm (RootPairing.EmbeddedG2.short P))
      ((P.reflectionPerm (RootPairing.EmbeddedG2.long P)) (RootPairing.EmbeddedG2.short P))
-- Mathlib.Logic.Equiv.Basic
Equiv.piCongrLeft_refl : ∀ {α : Sort u_1} (P : α → Sort u_9), Equiv.piCongrLeft P (Equiv.refl α) = Equiv.refl ((a : α) → P a)
-- Lean.Elab.Term.TermElabM
/-- Return the universe level names explicitly provided by the user.
 -/
Lean.Elab.Term.getLevelNames : Lean.Elab.TermElabM (List Lean.Name)
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.VariableChange.instInv : {R : Type u} → [inst : CommRing R] → Inv (WeierstrassCurve.VariableChange R)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.symm_symm : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂), e.symm.symm = e
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- A family of monoid homomorphisms `f a : γ →* β a` defines a monoid homomorphism
`Pi.monoidHom f : γ →* Π a, β a` given by `Pi.monoidHom f x b = f b x`.  -/
MonoidHom.pi : {I : Type u} →
  {f : I → Type v} →
    [inst : (i : I) → MulOneClass (f i)] →
      {γ : Type w} → [inst_1 : MulOneClass γ] → ((i : I) → γ →* f i) → γ →* (i : I) → f i
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_zero_measure : ∀ {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε]
  {f : α → ε}, MeasureTheory.Integrable f 0
-- Mathlib.RingTheory.MvPowerSeries.Rename
MvPowerSeries.killCompl_monomial_embDomain : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {e : σ ↪ τ} (x : σ →₀ ℕ) (r : R),
  (MvPowerSeries.killCompl e) ((MvPowerSeries.monomial (Finsupp.embDomain e x)) r) = (MvPowerSeries.monomial x) r
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.rotCompInvRot_hom_app_hom₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  (CategoryTheory.Pretriangulated.rotCompInvRot.hom.app X).hom₃ = CategoryTheory.CategoryStruct.id X.obj₃
-- Mathlib.GroupTheory.Rank
AddSubgroup.rank_congr : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G} [inst_1 : AddGroup.FG ↥H] [inst_2 : AddGroup.FG ↥K],
  H = K → AddGroup.rank ↥H = AddGroup.rank ↥K
-- Mathlib.Topology.MetricSpace.Dilation
Isometry.toDilation_toFun : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (f : α → β)
  (hf : Isometry f) (a : α), (Isometry.toDilation f hf) a = f a
-- Lean.Meta.Tactic.Cases
/-- Similar to `generalizeTargets` but customized for the `casesOn` motive.
Given a metavariable `mvarId` representing the
```
Ctx, h : I A j, D |- T
```
where `fvarId` is `h`s id, and the type `I A j` is an inductive datatype where `A` are parameters,
and `j` the indices. Generate the goal
```
Ctx, h : I A j, D, j' : J, h' : I A j' |- j == j' -> h == h' -> T
```
Remark: `(j == j' -> h == h')` is a "telescopic" equality.
Remark: `j` is sequence of terms, and `j'` a sequence of free variables.
The result contains the fields
- `mvarId`: the new goal
- `indicesFVarIds`: `j'` ids
- `fvarId`: `h'` id
- `numEqs`: number of equations in the target  -/
Lean.Meta.generalizeIndices : Lean.MVarId → Lean.FVarId → Lean.MetaM Lean.Meta.GeneralizeIndicesSubgoal
-- Aesop.Search.Main
Aesop.checkRootUnprovable : {Q : Type} → [inst : Aesop.Queue Q] → Aesop.SearchM Q (Option Lean.MessageData)
-- Init.Core
le_of_le_of_eq : ∀ {α : Type u_1} {a b c : α} [inst : LE α], a ≤ b → b = c → a ≤ c
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.source_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (self : ModelWithCorners 𝕜 E H),
  self.source = Set.univ
-- Lean.Server.CodeActions.Basic
Lean.Server.CodeActionResolveData.params : Lean.Server.CodeActionResolveData → Lean.Lsp.CodeActionParams
-- Mathlib.Data.Int.Init
Int.lt_div_iff_of_dvd_of_neg : ∀ {a b c : ℤ}, c < 0 → c ∣ b → (a < b / c ↔ b < c * a)
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (x : B) {a b : Bᵒᵖ} {f g : a ⟶ b} (a_1 : f ⟶ g)
  (x_1 : Opposite.unop a ⟶ x),
  ((CategoryTheory.Bicategory.yoneda₀ x).map₂ a_1).toNatTrans.app x_1 =
    CategoryTheory.Bicategory.whiskerRight a_1.unop2 x_1
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂)
  (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
  (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f)
  (X : ↑(F.obj b₀)) {Z : ↑(F.obj b₃)} (h : (F.map f₁₃).toFunctor.obj ((F.map f₀₁).toFunctor.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₁ f₁₃ f ⋯).hom.toNatTrans.app X) h =
    CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₂ f₂₃ f ⋯).hom.toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp
        ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom.toNatTrans.app X))
        (CategoryTheory.CategoryStruct.comp
          ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv.toNatTrans.app ((F.map f₀₁).toFunctor.obj X)) h))
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.map_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor C D) {X Y : CategoryTheory.WithTerminal C} (f : X ⟶ Y),
  (CategoryTheory.WithTerminal.map F).map f =
    match X, Y, f with
    | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_1, f =>
      F.map (CategoryTheory.WithTerminal.down f)
    | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.star, x => PUnit.unit
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => PUnit.unit
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndep.eq_1 : ∀ {Ω : Type u_1} {ι : Type u_2} (m : ι → MeasurableSpace Ω) {_mΩ : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.iIndep m μ =
    ProbabilityTheory.Kernel.iIndep m (ProbabilityTheory.Kernel.const Unit μ) (MeasureTheory.Measure.dirac ())
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.braiding_leftUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : C),
  CategoryTheory.CategoryStruct.comp (β_ X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEmbedding.subtype_coe : ∀ {α : Type u_1} {s : Set α} {mα : MeasurableSpace α}, MeasurableSet s → MeasurableEmbedding Subtype.val
-- Mathlib.Geometry.Euclidean.Incenter
/-- The inverse of the distance from one vertex to the opposite face, expressed as a sum of
multiples of that quantity for the other vertices. The multipliers, expressed here in terms of
inner products, are equal to the cosines of angles between faces (informally, the inverse
distances are proportional to the volumes of the faces and this is equivalent to expressing
the volume of a face as the sum of the signed volumes of projections of the other faces onto that
face).  -/
Affine.Simplex.inv_height_eq_sum_mul_inv_dist : ∀ {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 : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  (s.height i)⁻¹ =
    ∑ j with j ≠ i,
      -(inner ℝ (s.points i -ᵥ s.altitudeFoot i) (s.points j -ᵥ s.altitudeFoot j) / (s.height i * s.height j)) *
        (s.height j)⁻¹
-- Std.Internal.UV.Loop
Std.Internal.UV.Loop.Options.mk.sizeOf_spec : ∀ (accumulateIdleTime blockSigProfSignal : Bool),
  sizeOf { accumulateIdleTime := accumulateIdleTime, blockSigProfSignal := blockSigProfSignal } =
    1 + sizeOf accumulateIdleTime + sizeOf blockSigProfSignal
-- Init.Data.UInt.Lemmas
UInt64.toNat_ofFin : ∀ (x : Fin UInt64.size), (UInt64.ofFin x).toNat = ↑x
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get_eq_get_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {a : α}
  {h : a ∈ m}, m.get a h = (m.get? a).get ⋯
-- Std.Time.Zoned.Database.TZdb
Std.Time.Database.TZdb.instBEqTZSpec : BEq Std.Time.Database.TZdb.TZSpec
-- Init.Core
DoResultPRBC.pure.sizeOf_spec : ∀ {α β σ : Type u} [inst : SizeOf α] [inst_1 : SizeOf β] [inst_2 : SizeOf σ] (a : α) (a_1 : σ),
  sizeOf (DoResultPRBC.pure a a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.Algebra.Group.Hom.Defs
/-- The monoid of endomorphisms.  -/
Monoid.End : (M : Type u_4) → [MulOne M] → Type u_4
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.EqResult.decide.injEq : ∀ (b b_1 : Bool), (Nat.EqResult.decide✝ b = Nat.EqResult.decide✝ b_1) = (b = b_1)
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.power_one : ∀ (a : Cardinal.{u}), a ^ 1 = a
-- Mathlib.Topology.Algebra.Ring.Ideal
instCompactSpaceQuotientIdeal : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : CommRing R] (N : Ideal R) [CompactSpace R], CompactSpace (R ⧸ N)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.RightHomologyData.homologyIso_rightHomologyData : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology],
  S.rightHomologyData.homologyIso = S.rightHomologyIso.symm
-- Mathlib.Algebra.Homology.ComplexShapeSigns
/-- The obvious `TotalComplexShapeSymmetry c₂ c₁ c₁₂` deduced from a
`TotalComplexShapeSymmetry c₁ c₂ c₁₂`.  -/
TotalComplexShapeSymmetry.symmetry : {I₁ : Type u_1} →
  {I₂ : Type u_2} →
    {I₁₂ : Type u_4} →
      (c₁ : ComplexShape I₁) →
        (c₂ : ComplexShape I₂) →
          (c₁₂ : ComplexShape I₁₂) →
            [inst : TotalComplexShape c₁ c₂ c₁₂] →
              [inst_1 : TotalComplexShape c₂ c₁ c₁₂] →
                [TotalComplexShapeSymmetry c₁ c₂ c₁₂] → TotalComplexShapeSymmetry c₂ c₁ c₁₂
-- Mathlib.Data.Seq.Defs
Stream'.Seq.BisimO.eq_2 : ∀ {α : Type u} (R : Stream'.Seq α → Stream'.Seq α → Prop) (a : α) (s : Stream'.Seq α) (a' : α) (s' : Stream'.Seq α),
  Stream'.Seq.BisimO R (some (a, s)) (some (a', s')) = (a = a' ∧ R s s')
-- Mathlib.AlgebraicGeometry.Geometrically.Integral
AlgebraicGeometry.GeometricallyIntegral.eq_geometricallyReduced_inf_geometricallyIrreducible : @AlgebraicGeometry.GeometricallyIntegral =
  @AlgebraicGeometry.GeometricallyReduced ⊓ @AlgebraicGeometry.GeometricallyIrreducible
-- Mathlib.CategoryTheory.Limits.Cones
/-- Extending a cocone by the identity does nothing.  -/
CategoryTheory.Limits.Cocone.extendId : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (s : CategoryTheory.Limits.Cocone F) → s.extend (CategoryTheory.CategoryStruct.id s.pt) ≅ s
-- Init.Data.Iterators.Basic
Std.IterStep.yield.sizeOf_spec : ∀ {α : Sort u_1} {β : Sort u_2} [inst : SizeOf α] [inst_1 : SizeOf β] (it : α) (out : β),
  sizeOf (Std.IterStep.yield it out) = 1 + sizeOf it + sizeOf out
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Precylinder.map_i₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (P : HomotopicalAlgebra.Precylinder X) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor C D), (P.map F).i₁ = F.map P.i₁
-- Mathlib.Analysis.Meromorphic.Complex
Meromorphic.Gamma : Meromorphic Complex.Gamma
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.toAddCommMonoid : {α : Type u_3} → [self : LinearOrderedAddCommGroupWithTop α] → AddCommMonoid α
-- Mathlib.Geometry.Convex.Cone.Pointed
/-- Coercion from submodules to pointed cones as a lattice homomorphism.  -/
PointedCone.ofSubmoduleLatticeHom : {R : Type u_1} →
  {E : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] →
        [inst_2 : IsOrderedRing R] →
          [inst_3 : AddCommMonoid E] → [inst_4 : Module R E] → CompleteLatticeHom (Submodule R E) (PointedCone R E)
-- Init.PropLemmas
exists_and_right : ∀ {α : Sort u_1} {p : α → Prop} {b : Prop}, (∃ x, p x ∧ b) ↔ (∃ x, p x) ∧ b
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mfderiv_sumSwap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {M' : Type u_21} [inst_6 : TopologicalSpace M']
  [inst_7 : ChartedSpace H M'] {p : M ⊕ M'}, mfderiv% Sum.swap p = ContinuousLinearMap.id 𝕜 (TangentSpace I p)
-- Mathlib.RingTheory.DedekindDomain.SelmerGroup
/-- The Selmer group `K⟮S, n⟯`.  -/
IsDedekindDomain.selmerGroup : {R : Type u} →
  [inst : CommRing R] →
    [IsDedekindDomain R] →
      {K : Type v} →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] →
            [IsFractionRing R K] →
              {S : Set (IsDedekindDomain.HeightOneSpectrum R)} → {n : ℕ} → Subgroup (Kˣ ⧸ (powMonoidHom n).range)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mapIso_unitIso_hom_app_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S S' : D} {T : CategoryTheory.Functor C D} (i : S ≅ S')
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) T),
  ((CategoryTheory.StructuredArrow.mapIso i).unitIso.hom.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Lean.Meta.Tactic.FVarSubst
Lean.Meta.instInhabitedFVarSubst.default : Lean.Meta.FVarSubst
-- Mathlib.Topology.Algebra.FilterBasis
GroupFilterBasis.t2Space_iff : ∀ {G : Type u} [inst : Group G] [t : TopologicalSpace G] (F : GroupFilterBasis G),
  F.topology = t → (T2Space G ↔ ⋂₀ F.sets = {1})
-- Mathlib.Data.List.Defs
/-- Given a decidable predicate `p` and a proof of existence of `a ∈ l` such that `p a`,
choose the first element with this property. This version returns both `a` and proofs
of `a ∈ l` and `p a`.  -/
List.chooseX : {α : Type u_1} → (p : α → Prop) → [DecidablePred p] → (l : List α) → (∃ a ∈ l, p a) → { a // a ∈ l ∧ p a }
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat.instFullMat_SingleObjMulOppositeEquivalenceSingleObjInverse : ∀ (R : Type) [inst : Ring R], (CategoryTheory.Mat.equivalenceSingleObjInverse R).Full
-- Mathlib.Topology.Instances.Rat
Rat.isUniformEmbedding_coe_real : IsUniformEmbedding Rat.cast
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RciSliceData.mk.inj : ∀ {α : Type u} {inst : Ord α} {treeMap : Std.DTreeMap.Internal.Impl α fun x => Unit} {range : Std.Rci α}
  {treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => Unit} {range_1 : Std.Rci α},
  { treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 } →
    treeMap = treeMap_1 ∧ range = range_1
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffAt.eq_1 : ∀ (𝕜 : Type u) [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (n : WithTop ℕ∞)
  (f : E → F) (x : E), ContDiffAt 𝕜 n f x = ContDiffWithinAt 𝕜 n f Set.univ x
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- A morphism of comonoid objects.  -/
CategoryTheory.Comon.Hom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → CategoryTheory.Comon C → CategoryTheory.Comon C → Type v₁
-- Mathlib.Algebra.BigOperators.Finprod
finprod_eq_if : ∀ {M : Type u_2} [inst : CommMonoid M] {p : Prop} [inst_1 : Decidable p] {x : M}, ∏ᶠ (_ : p), x = if p then x else 1
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- additive equivalences between `Add`s are the same
as (isomorphic to) isomorphisms in `AddMagmaCat`  -/
addEquivIsoAddMagmaIso : {X Y : Type u} → [inst : Add X] → [inst_1 : Add Y] → X ≃+ Y ≅ AddMagmaCat.of X ≅ AddMagmaCat.of Y
-- Mathlib.Topology.Bases
TopologicalSpace.IsTopologicalBasis.open_eq_iUnion : ∀ {α : Type u} [t : TopologicalSpace α] {B : Set (Set α)},
  TopologicalSpace.IsTopologicalBasis B → ∀ {u : Set α}, IsOpen u → ∃ β f, u = ⋃ i, f i ∧ ∀ (i : β), f i ∈ B
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A) (x : ↑((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).toTopCat),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.ΓSpecIso (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).inv
      (CategoryTheory.CategoryStruct.comp
        ((AlgebraicGeometry.Spec.locallyRingedSpaceObj
                (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).presheaf.germ
          ⊤ ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec 𝒜 f).base) x) ⋯)
        (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec 𝒜 f) x)) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ 𝒜 f)
      (((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).presheaf.Γgerm x)
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.formatMonthNarrow : Std.Time.DateFormatSymbols → Std.Time.Month.Ordinal → String
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.closedComplemented_iff_exists_isTopCompl : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p : Submodule R M}, p.ClosedComplemented ↔ ∃ q, Submodule.IsTopCompl p q
-- Mathlib.CategoryTheory.GuitartExact.Basic
CategoryTheory.TwoSquare.GuitartExact.isConnected_rightwards : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} {inst : CategoryTheory.Category.{v₁, u₁} C₁}
  {inst_1 : CategoryTheory.Category.{v₂, u₂} C₂} {inst_2 : CategoryTheory.Category.{v₃, u₃} C₃}
  {inst_3 : CategoryTheory.Category.{v₄, u₄} C₄} {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} {w : CategoryTheory.TwoSquare T L R B}
  [self : w.GuitartExact] {X₂ : C₂} {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃),
  CategoryTheory.IsConnected (w.StructuredArrowRightwards g)
-- Mathlib.NumberTheory.Padics.PadicNumbers
/-- For all `n ≥ stationaryPoint f hf`, the `p`-adic norm of `f n` is the same.  -/
PadicSeq.stationaryPoint : {p : ℕ} → [inst : Fact (Nat.Prime p)] → {f : PadicSeq p} → ¬f ≈ 0 → ℕ
-- Init.System.IO
/-- Converts `s` to a string using its `ToString α` instance, and prints it with a trailing newline to
the current standard error (as determined by `IO.getStderr`).
 -/
IO.eprintln : {α : Type u_1} → [ToString α] → α → IO Unit
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.primeSpectrumProdOfSum.eq_1 : ∀ (R : Type u) (S : Type v) [inst : CommSemiring R] [inst_1 : CommSemiring S] (I : Ideal R) (isPrime : I.IsPrime),
  PrimeSpectrum.primeSpectrumProdOfSum R S (Sum.inl { asIdeal := I, isPrime := isPrime }) =
    { asIdeal := I.prod ⊤, isPrime := ⋯ }
-- Mathlib.Analysis.Meromorphic.Order
/-- Adding a locally vanishing function does not change the order.
 -/
meromorphicOrderAt_add_of_top_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E} {x : 𝕜},
  meromorphicOrderAt f₁ x = ⊤ → meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₂ x
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Eq
Std.Tactic.BVDecide.BVPred.instLawfulOperatorBinaryRefVecMkEq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ},
  Std.Sat.AIG.LawfulOperator α (fun x => x.BinaryRefVec w) Std.Tactic.BVDecide.BVPred.mkEq
-- Std.Sat.AIG.Basic
Std.Sat.AIG.instInhabitedFanin : Inhabited Std.Sat.AIG.Fanin
-- Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
CategoryTheory.PreOneHypercover.IsStronglySheafFor.isSeparatedFor_sieve₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : C} {E : CategoryTheory.PreOneHypercover X}
  {F : CategoryTheory.Functor Cᵒᵖ (Type u_3)},
  E.IsStronglySheafFor F →
    ∀ ⦃i j : E.I₀⦄ ⦃W : C⦄ (p₁ : W ⟶ E.X i) (p₂ : W ⟶ E.X j),
      CategoryTheory.CategoryStruct.comp p₁ (E.f i) = CategoryTheory.CategoryStruct.comp p₂ (E.f j) →
        CategoryTheory.Presieve.IsSeparatedFor F (E.sieve₁ p₁ p₂).arrows
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basis
SymmetricAlgebra.IsSymmetricAlgebra.mvPolynomial : ∀ {R : Type uR} {M : Type uM} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (I : Type u_1)
  (b : Module.Basis I R M), IsSymmetricAlgebra ((b.constr R) MvPolynomial.X)