mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.leftUnitor_inv_hom : ∀ (X : SFinKer),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv.hom =
    ProbabilityTheory.Kernel.id.map fun x => (PUnit.unit, x)
-- Mathlib.CategoryTheory.GuitartExact.VerticalComposition
/-- The vertical composition of 2-squares. (Variant where we allow the replacement of
the vertical compositions by isomorphic functors.)  -/
CategoryTheory.TwoSquare.vComp' : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {D₁ : Type u_4} →
        {D₂ : Type u_5} →
          {D₃ : Type u_6} →
            [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
              [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
                [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
                  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁] →
                    [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] →
                      [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃] →
                        {H₁ : CategoryTheory.Functor C₁ D₁} →
                          {L₁ : CategoryTheory.Functor C₁ C₂} →
                            {R₁ : CategoryTheory.Functor D₁ D₂} →
                              {H₂ : CategoryTheory.Functor C₂ D₂} →
                                CategoryTheory.TwoSquare H₁ L₁ R₁ H₂ →
                                  {L₂ : CategoryTheory.Functor C₂ C₃} →
                                    {R₂ : CategoryTheory.Functor D₂ D₃} →
                                      {H₃ : CategoryTheory.Functor C₃ D₃} →
                                        CategoryTheory.TwoSquare H₂ L₂ R₂ H₃ →
                                          {L₁₂ : CategoryTheory.Functor C₁ C₃} →
                                            {R₁₂ : CategoryTheory.Functor D₁ D₃} →
                                              (L₁.comp L₂ ≅ L₁₂) →
                                                (R₁.comp R₂ ≅ R₁₂) → CategoryTheory.TwoSquare H₁ L₁₂ R₁₂ H₃
-- Mathlib.CategoryTheory.Generator.StrongGenerator
CategoryTheory.ObjectProperty.IsStrongGenerator.isSeparating : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C},
  P.IsStrongGenerator → P.IsSeparating
-- Mathlib.Computability.TuringMachine.Tape
/-- Append a list on the left side of a `ListBlank`.  -/
Turing.ListBlank.append : {Γ : Type u_1} → [inst : Inhabited Γ] → List Γ → Turing.ListBlank Γ → Turing.ListBlank Γ
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.preimage_sphere : ∀ {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₂) (x : E₂) (r : ℝ), ⇑e ⁻¹' Metric.sphere x r = Metric.sphere (e.symm x) r
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} (t t_1 : Std.TreeSet.Raw α cmp) (e_t : t = t_1) (a a_1 : α) (e_a : a = a_1)
  (h : a ∈ t), t.get a h = t_1.get a_1 ⋯
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.toList_sorted : ∀ {α : Type u_1} {cmp : α → α → Ordering} {t : RBTree.RBSet α cmp}, List.Pairwise (RBTree.RBNode.cmpLT cmp) t.toList
-- Lean.Util.Trace
Lean.MonadTrace.modifyTraceState : {m : Type → Type} → [self : Lean.MonadTrace m] → (Lean.TraceState → Lean.TraceState) → m Unit
-- Mathlib.Topology.NhdsWithin
tendsto_const_nhdsWithin : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {l : Filter β} {s : Set α} {a : α},
  a ∈ s → Filter.Tendsto (fun x => a) l (nhdsWithin a s)
-- Mathlib.Order.Basic
le_of_forall_gt : ∀ {α : Type u_2} [inst : LinearOrder α] {a b : α}, (∀ (c : α), a < c → b < c) → b ≤ a
-- Mathlib.CategoryTheory.Types.Epimorphisms
CategoryTheory.Types.instIsStableUnderBaseChangeEpimorphismsType : (CategoryTheory.MorphismProperty.epimorphisms (Type u)).IsStableUnderBaseChange
-- Mathlib.Order.SuccPred.WithBot
WithTop.pred_eq_top : ∀ {α : Type u_2} [Nontrivial α] [inst : LinearOrder α] [inst_1 : OrderTop α] [inst_2 : PredOrder α] (a : WithTop α),
  a.pred = ⊤ ↔ a = ⊤
-- Mathlib.Topology.Homotopy.Path
/-- Casting a `Homotopy p₀ p₁` to a `Homotopy q₀ q₁` where `p₀ = q₀` and `p₁ = q₁`.  -/
Path.Homotopy.cast : {X : Type u} →
  [inst : TopologicalSpace X] →
    {x₀ x₁ : X} → {p₀ p₁ q₀ q₁ : Path x₀ x₁} → p₀.Homotopy p₁ → p₀ = q₀ → p₁ = q₁ → q₀.Homotopy q₁
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.coe_pointwise_smul : ∀ {K : Type u} [inst : Field K] {G : Type u_1} [inst_1 : Group G] [inst_2 : MulSemiringAction G K] (g : G)
  (S : ValuationSubring K), ↑(g • S) = g • ↑S
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_erase : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k a : α}, (m.erase k).getKey? a = if (k == a) = true then none else m.getKey? a
-- Mathlib.Algebra.Free
FreeSemigroup.lift_of : ∀ {α : Type u} {β : Type v} [inst : Semigroup β] (f : α → β) (x : α), (FreeSemigroup.lift f) (FreeSemigroup.of x) = f x
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_Icc_cast : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a b : Fin n),
  ∑ i ∈ Finset.Icc (Fin.cast h a) (Fin.cast h b), f i = ∑ i ∈ Finset.Icc a b, f (Fin.cast h i)
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- If a sequence of continuous functions converges uniformly on the circle,
then their circle integrals converge to the circle integral of the limit function.  -/
TendstoUniformlyOn.tendsto_circleIntegral_of_continuousOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {ι : Type u_2} {f : ι → ℂ → E} {g : ℂ → E}
  {c : ℂ} {R : ℝ} {l : Filter ι} [l.IsCountablyGenerated],
  0 ≤ R →
    (∀ᶠ (i : ι) in l, ContinuousOn (f i) (Metric.sphere c R)) →
      TendstoUniformlyOn f g l (Metric.sphere c R) →
        Filter.Tendsto (fun n => ∮ (z : ℂ) in C(c, R), f n z) l (nhds (∮ (z : ℂ) in C(c, R), g z))
-- Mathlib.Logic.Relation
Relation.onFun_map_onFun_eq_onFun : ∀ {α : Type u_1} {β : Type u_2} {r : β → β → Prop} (f : α → β),
  Function.onFun (Relation.Map (Function.onFun r f) f f) f = Function.onFun r f
-- Mathlib.Data.List.Sigma
List.exists_of_mem_keys : ∀ {α : Type u} {β : α → Type v} {a : α} {l : List (Sigma β)}, a ∈ l.keys → ∃ b, ⟨a, b⟩ ∈ l
-- Mathlib.Data.QPF.Multivariate.Basic
/-- Any type function `F` that is (extensionally) equivalent to a QPF, is itself a QPF,
assuming that the functorial map of `F` behaves similar to `MvFunctor.ofEquiv eqv`  -/
MvQPF.ofEquiv : {n : ℕ} →
  {F : TypeVec.{u} n → Type u_2} →
    {F' : TypeVec.{u} n → Type u_3} →
      [q : MvQPF F'] →
        [inst : MvFunctor F] →
          (eqv : (α : TypeVec.{u} n) → F α ≃ F' α) →
            autoParam
                (∀ (α β : TypeVec.{u} n) (f : α.Arrow β) (a : F α),
                  MvFunctor.map f a = (eqv β).symm (MvFunctor.map f ((eqv α) a)))
                MvQPF.ofEquiv._auto_1 →
              MvQPF F
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
/-- The curve integral of a closed 1-form along the boundary of the image of a unit square
under a smooth map is zero.

This theorem is stated in terms of a `C^2` homotopy between two paths.  -/
ContinuousMap.Homotopy.curveIntegral_add_curveIntegral_eq_of_hasFDerivWithinAt : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedSpace ℝ E]
  [inst_6 : NormedSpace ℝ F] {a b c d : E} {γ₁ : Path a b} {γ₂ : Path c d} {t : Set E} {ω : E → E →L[𝕜] F}
  {dω : E → E →L[ℝ] E →L[𝕜] F} (φ : (↑γ₁).Homotopy ↑γ₂),
  (∀ a_1 ∈ Set.Ioo 0 1, ∀ b_1 ∈ Set.Ioo 0 1, φ (a_1, b_1) ∈ t) →
    (∀ x ∈ t, HasFDerivWithinAt ω (dω x) t x) →
      ContinuousOn ω (closure t) →
        (∀ x ∈ t, ∀ u ∈ tangentConeAt ℝ t x, ∀ v ∈ tangentConeAt ℝ t x, ((dω x) u) v = ((dω x) v) u) →
          ContDiffOn ℝ 2 (fun xy => Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2) (Set.Icc 0 1) →
            ∫ᶜ (x : E) in γ₁, ω x + ∫ᶜ (x : E) in φ.evalAt 1, ω x =
              ∫ᶜ (x : E) in γ₂, ω x + ∫ᶜ (x : E) in φ.evalAt 0, ω x
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.mk_one : Complex.UnitClosedDisc.mk 1 Complex.UnitClosedDisc.mk_one._proof_1 = 1
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.copy_K : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) {K' H' : C} (eK : K' ≅ h.K) (eH : H' ≅ h.H),
  (h.copy eK eH).K = K'
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeGroupBasis.instIsFreeGroupFreeGroup : ∀ (X : Type u_5), IsFreeGroup (FreeGroup X)
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
standardBorelSpace_of_discreteMeasurableSpace : ∀ {α : Type u_1} [inst : MeasurableSpace α] [DiscreteMeasurableSpace α] [Countable α], StandardBorelSpace α
-- Mathlib.Topology.Sets.Order
/-- The type of clopen upper sets of a topological space.  -/
ClopenUpperSet : (α : Type u_2) → [TopologicalSpace α] → [LE α] → Type u_2
-- Init.System.IO
termPrintln!__ : Lean.ParserDescr
-- Std.Data.ExtDTreeMap.Basic
/-- Given a proof that the tree map is not empty, retrieves the key-value pair with the smallest key.
 -/
Std.ExtDTreeMap.minEntry : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → (t : Std.ExtDTreeMap α β cmp) → t ≠ ∅ → (a : α) × β a
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.instDistribMulAction : {Γ : Type u_1} →
  {R : Type u_3} →
    [inst : PartialOrder Γ] →
      {V : Type u_8} →
        [inst_1 : Monoid R] → [inst_2 : AddMonoid V] → [DistribMulAction R V] → DistribMulAction R (HahnSeries Γ V)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
CategoryTheory.Limits.FormalCoproduct.power_I : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) (α : Type t)
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C], (U.power α).I = (α → U.I)
-- Mathlib.Analysis.Normed.Lp.LpEquiv
/-- The canonical `Equiv` between `lp E p ≃ PiLp p E` when `E : α → Type u` with `[Finite α]`.  -/
Equiv.lpPiLp : {α : Type u_1} →
  {E : α → Type u_2} → [inst : (i : α) → NormedAddCommGroup (E i)] → {p : ENNReal} → [Finite α] → ↥(lp E p) ≃ PiLp p E
-- Mathlib.Order.RelClasses
/-- Set notation form of `Eq.trans_le` -/
Eq.trans_subset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] {a b c : α} [inst : LE α], a = b → b ⊆ c → a ⊆ c
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- Scalar multiplication with a continuous linear map as a continuous linear map on Schwartz
functions.  -/
SchwartzMap.smulRightCLM : (𝕜 : Type u_2) →
  {E : Type u_5} →
    (F : Type u_6) →
      {G : Type u_7} →
        [inst : NormedAddCommGroup E] →
          [inst_1 : NormedSpace ℝ E] →
            [inst_2 : NormedAddCommGroup F] →
              [inst_3 : NormedSpace ℝ F] →
                [inst_4 : NontriviallyNormedField 𝕜] →
                  [inst_5 : NormedAlgebra ℝ 𝕜] →
                    [inst_6 : NormedAddCommGroup G] →
                      [inst_7 : NormedSpace ℝ G] →
                        [inst_8 : NormedSpace 𝕜 F] →
                          (E →L[ℝ] G →L[ℝ] ℝ) → SchwartzMap E F →L[𝕜] SchwartzMap E (G →L[ℝ] F)
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_36 : HSub Std.Time.Week.Offset Std.Time.Nanosecond.Offset Std.Time.Nanosecond.Offset
-- Mathlib.Order.Interval.Set.OrdConnected
Set.image_subtype_val_uIoo : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} [s.OrdConnected] (a b : ↑s),
  Subtype.val '' Set.uIoo a b = Set.uIoo ↑a ↑b
-- Mathlib.Algebra.Group.Pi.Basic
Function.comp_eq_one_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : One β] [inst_1 : One γ] (f : α → β) {g : β → γ},
  Function.Injective g → g 1 = 1 → (g ∘ f = 1 ↔ f = 1)
-- Mathlib.Logic.ExistsUnique
existsUnique_const : ∀ {b : Prop} (α : Sort u_2) [i : Nonempty α] [Subsingleton α], (∃! x, b) ↔ b
-- Std.Time.Time.Unit.Basic
/-- Converts a `Nanosecond.Offset` to an `Hour.Offset`.
 -/
Std.Time.Nanosecond.Offset.toHours : Std.Time.Nanosecond.Offset → Std.Time.Hour.Offset
-- Mathlib.Tactic.Linter.TextBased
Mathlib.Linter.TextBased.ErrorFormat.exceptionsFile.sizeOf_spec : sizeOf Mathlib.Linter.TextBased.ErrorFormat.exceptionsFile = 1
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
/-- The interchange law for horizontal and vertical composition of 2-cells in a bicategory.  -/
CategoryTheory.CatEnriched.hComp_comp : ∀ {C : Type u_1} [inst : CategoryTheory.EnrichedCategory CategoryTheory.Cat C] {a b c : CategoryTheory.CatEnriched C}
  {f₁ f₂ f₃ : a ⟶ b} {g₁ g₂ g₃ : b ⟶ c} (η : f₁ ⟶ f₂) (η' : f₂ ⟶ f₃) (θ : g₁ ⟶ g₂) (θ' : g₂ ⟶ g₃),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CatEnriched.hComp η θ) (CategoryTheory.CatEnriched.hComp η' θ') =
    CategoryTheory.CatEnriched.hComp (CategoryTheory.CategoryStruct.comp η η') (CategoryTheory.CategoryStruct.comp θ θ')
-- Aesop.RuleSet
_private.Aesop.RuleSet.0.Aesop.LocalRuleSet.postprocessForwardMatchRules : {α : Type} →
  Lean.Options →
    Aesop.LocalRuleSet → (Aesop.Rule α → Bool) → Array (Aesop.Rule α) → Array (Aesop.IndexMatchResult (Aesop.Rule α))
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
AlgebraicTopology.DoldKan.Compatibility.equivalenceCounitIso_hom_app : ∀ {A : Type u_1} {B : Type u_3} {B' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} B] [inst_2 : CategoryTheory.Category.{v_4, u_4} B'] {eB : B ≌ B'}
  {F : CategoryTheory.Functor A B'} {G : CategoryTheory.Functor B A} (η : G.comp F ≅ eB.functor) (X : B),
  (AlgebraicTopology.DoldKan.Compatibility.equivalenceCounitIso η).hom.app X =
    CategoryTheory.CategoryStruct.comp (eB.inverse.map (η.hom.app X)) (eB.unitIso.inv.app X)
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.centerEquivRootsOfUnity.congr_simp : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : Module.Free R V] [inst_4 : Module.Finite R V],
  SpecialLinearGroup.centerEquivRootsOfUnity = SpecialLinearGroup.centerEquivRootsOfUnity
-- Std.Internal.Parsec.Basic
Std.Internal.Parsec.Input.curr : {ι : Type} →
  {elem idx : outParam Type} →
    {inst : DecidableEq idx} → {inst_1 : DecidableEq elem} → [self : Std.Internal.Parsec.Input ι elem idx] → ι → elem
-- Mathlib.Dynamics.TopologicalEntropy.Subset
Dynamics.coverEntropyInf_monotone : ∀ {X : Type u_1} [inst : UniformSpace X] (T : X → X), Monotone fun F => Dynamics.coverEntropyInf T F
-- Mathlib.Geometry.Manifold.Submersion
Manifold.IsSubmersionAtOfComplement.property : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : TopologicalSpace H] [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace H M] [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N}
  {x : M},
  Manifold.IsSubmersionAtOfComplement F I J n f x →
    Manifold.LiftSourceTargetPropertyAt I J n f x (Manifold.SubmersionAtProp F I J M N)
-- Init.Tactics
/-- Assuming `x` is a variable in the local context with an inductive type,
`induction x` applies induction on `x` to the main goal,
producing one goal for each constructor of the inductive type,
in which the target is replaced by a general instance of that constructor
and an inductive hypothesis is added for each recursive argument to the constructor.
If the type of an element in the local context depends on `x`,
that element is reverted and reintroduced afterward,
so that the inductive hypothesis incorporates that hypothesis as well.

For example, given `n : Nat` and a goal with a hypothesis `h : P n` and target `Q n`,
`induction n` produces one goal with hypothesis `h : P 0` and target `Q 0`,
and one goal with hypotheses `h : P (Nat.succ a)` and `ih₁ : P a → Q a` and target `Q (Nat.succ a)`.
Here the names `a` and `ih₁` are chosen automatically and are not accessible.
You can use `with` to provide the variables names for each constructor.
- `induction e`, where `e` is an expression instead of a variable,
  generalizes `e` in the goal, and then performs induction on the resulting variable.
- `induction e using r` allows the user to specify the principle of induction that should be used.
  Here `r` should be a term whose result type must be of the form `C t`,
  where `C` is a bound variable and `t` is a (possibly empty) sequence of bound variables
- `induction e generalizing z₁ ... zₙ`, where `z₁ ... zₙ` are variables in the local context,
  generalizes over `z₁ ... zₙ` before applying the induction but then introduces them in each goal.
  In other words, the net effect is that each inductive hypothesis is generalized.
- Given `x : Nat`, `induction x with | zero => tac₁ | succ x' ih => tac₂`
  uses tactic `tac₁` for the `zero` case, and `tac₂` for the `succ` case.
 -/
Lean.Parser.Tactic.induction : Lean.ParserDescr
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.mk.sizeOf_spec : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : Star B] [inst_7 : SizeOf R] [inst_8 : SizeOf A] [inst_9 : SizeOf B]
  (toNonUnitalAlgHom : A →ₙₐ[R] B)
  (map_star' : ∀ (a : A), toNonUnitalAlgHom.toFun (star a) = star (toNonUnitalAlgHom.toFun a)),
  sizeOf { toNonUnitalAlgHom := toNonUnitalAlgHom, map_star' := map_star' } = 1 + sizeOf toNonUnitalAlgHom
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.Lean.parseLowerHex?.eq_2 : ∀ (s : String) (p : s.Pos) (acc k_1 : ℕ),
  Lean.parseLowerHex?✝ k_1.succ s p acc =
    if h : p = s.endPos then none
    else
      match Lean.fromHex?✝ (p.get h) with
      | some d => Lean.parseLowerHex?✝ k_1 s (p.next h) (acc <<< 4 ||| d)
      | none => none
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.disjoint_mul_inv_of_mem_cycleFactorsFinset : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {f g : Equiv.Perm α},
  f ∈ g.cycleFactorsFinset → (g * f⁻¹).Disjoint f
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetRing.iInter_le_mem : ∀ {α : Type u_1} {C : Set (Set α)},
  MeasureTheory.IsSetRing C → ∀ {s : ℕ → Set α}, (∀ (n : ℕ), s n ∈ C) → ∀ (n : ℕ), ⋂ i, ⋂ (_ : i ≤ n), s i ∈ C
-- Aesop.RuleSet.Member
Aesop.GlobalRuleSetMember.normSimpRule.inj : ∀ {e e_1 : Aesop.NormSimpRule},
  Aesop.GlobalRuleSetMember.normSimpRule e = Aesop.GlobalRuleSetMember.normSimpRule e_1 → e = e_1
-- Init.Data.Range.Polymorphic.PRange
Std.Rci.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (lower : α), sizeOf lower...* = 1 + sizeOf lower
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.adjugate_eq_one_of_card_eq_one : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] {A : Matrix n n α},
  Fintype.card n = 1 → A.adjugate = 1
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.eval_id : ∀ (n : ℕ), Nat.Partrec.Code.id.eval n = Part.some n
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
HasStrictFDerivAt.map_nhds_eq_of_equiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E ≃L[𝕜] F} {a : E} [CompleteSpace E], HasStrictFDerivAt f (↑f') a → Filter.map f (nhds a) = nhds (f a)
-- Mathlib.Topology.Order.IntermediateValue
isPreconnected_Ioi : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {a : α}, IsPreconnected (Set.Ioi a)
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
HasFTaylorSeriesUpTo.zero_eq' : ∀ {𝕜 : 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] {f : E → F}
  {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F},
  HasFTaylorSeriesUpTo n f p → ∀ (x : E), p x 0 = (continuousMultilinearCurryFin0 𝕜 E F).symm (f x)
-- Batteries.Data.String.Lemmas
Substring.Raw.ValidFor.str : ∀ {l m r : List Char} {s : Substring.Raw}, Substring.Raw.ValidFor l m r s → s.str = String.ofList (l ++ m ++ r)
-- Mathlib.GroupTheory.OrderOfElement
isPeriodicPt_add_iff_nsmul_eq_zero : ∀ {G : Type u_1} [inst : AddMonoid G] {n : ℕ} (x : G), Function.IsPeriodicPt (fun x_1 => x + x_1) n 0 ↔ n • x = 0
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.content_dvd_coeff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] {p : Polynomial R} (n : ℕ), p.content ∣ p.coeff n
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.op_inf : ∀ {M : Type u_2} [inst : Mul M] (S₁ S₂ : Subsemigroup M), (S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op
-- Init.Data.Array.Basic
/-- Reverses an array by repeatedly swapping elements.

The original array is modified in place if there are no other references to it.

Examples:
* `(#[] : Array Nat).reverse = #[]`
* `#[0, 1].reverse = #[1, 0]`
* `#[0, 1, 2].reverse = #[2, 1, 0]`
 -/
Array.reverse : {α : Type u} → Array α → Array α
-- Std.Data.Internal.List.Associative
Std.Internal.List.DistinctKeys.insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  Std.Internal.List.DistinctKeys l → Std.Internal.List.DistinctKeys (Std.Internal.List.insertEntry k v l)
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instDiv : {α : Type u_1} → [Div α] → Div (Lex α)
-- Mathlib.NumberTheory.Real.Irrational
Irrational.of_ratCast_add : ∀ (q : ℚ) {x : ℝ}, Irrational (↑q + x) → Irrational x
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_rco_append_toList_rco : ∀ {l m n : ℤ}, l ≤ m → m ≤ n → (l...m).toList ++ (m...n).toList = (l...n).toList
-- Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
ValueDistribution.proximity_const : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {c : E} {r : ℝ},
  ValueDistribution.proximity (fun x => c) ⊤ r = ‖c‖.posLog
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
/-- The subcomplex of a simplicial set that is generated by a simplex.  -/
SSet.Subcomplex.ofSimplex : {X : SSet} → {n : ℕ} → X.obj (Opposite.op { len := n }) → X.Subcomplex
-- Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
TensorPower.toTensorAlgebra_galgebra_toFun : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (r : R),
  TensorPower.toTensorAlgebra (DirectSum.GAlgebra.toFun r) = (algebraMap R (TensorAlgebra R M)) r
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.adjMatrix_mulVec_apply : ∀ {α : Type u_1} {V : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : Fintype V]
  [inst_2 : NonAssocSemiring α] (v : V) (vec : V → α),
  (SimpleGraph.adjMatrix α G).mulVec vec v = ∑ u ∈ G.neighborFinset v, vec u
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.coe_equiv_fst_eq_one_iff_mem : ∀ {G : Type u_1} [inst : Group G] {S T : Set G} (hST : Subgroup.IsComplement S T) {g : G},
  1 ∈ S → (↑(hST.equiv g).1 = 1 ↔ g ∈ T)
-- Init.Data.List.Pairwise
List.pairwise_iff_forall_sublist : ∀ {α : Type u_1} {l : List α} {R : α → α → Prop}, List.Pairwise R l ↔ ∀ {a b : α}, [a, b].Sublist l → R a b
-- Lean.Util.Diff
/-- Shows a line-by-line edit script with markers for added and removed lines.  -/
Lean.Diff.linesToString : {α : Type u_1} → [ToString α] → Array (Lean.Diff.Action × α) → String
-- Mathlib.Algebra.Star.Basic
/-- **Alias** of the forward direction of `commute_star_comm`. -/
Commute.star_right : ∀ {R : Type u} [inst : Mul R] [inst_1 : StarMul R] {x y : R}, Commute (star x) y → Commute x (star y)