mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.DocString.Extension
Lean.addDocStringCore' : {m : Type → Type} →
  [Monad m] → [Lean.MonadError m] → [Lean.MonadEnv m] → [MonadLiftT BaseIO m] → Lean.Name → Option String → m Unit
-- Mathlib.Order.Monotone.Monovary
antivaryOn_const_left : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] (g : ι → β) (a : α)
  (s : Set ι), AntivaryOn (Function.const ι a) g s
-- Mathlib.CategoryTheory.Functor.Basic
CategoryTheory.Functor.toPrefunctor_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (a : X ⟶ Y), F.toPrefunctor.map a = F.map a
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.DBuilderName.regular.injEq : ∀ (b b_1 : Aesop.BuilderName),
  (Aesop.Frontend.DBuilderName.regular b = Aesop.Frontend.DBuilderName.regular b_1) = (b = b_1)
-- Mathlib.Algebra.Ring.Int.Defs
Int.cast_mul : ∀ {α : Type u_1} [inst : NonAssocRing α] (m n : ℤ), ↑(m * n) = ↑m * ↑n
-- Mathlib.Analysis.InnerProductSpace.l2Space
HilbertBasis.tsum_inner_mul_inner : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] (b : HilbertBasis ι 𝕜 E) (x y : E),
  ∑' (i : ι), inner 𝕜 x (b i) * inner 𝕜 (b i) y = inner 𝕜 x y
-- Init.TacticsExtra
/-- Normalize casts in the goal and the given expression, then close the goal with `exact`.
 -/
Lean.Parser.Tactic.tacticExact_mod_cast_ : Lean.ParserDescr
-- Mathlib.CategoryTheory.ObjectProperty.Kernels
CategoryTheory.MorphismProperty.instIsClosedUnderIsomorphismsCokernels : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (W : CategoryTheory.MorphismProperty C), W.cokernels.IsClosedUnderIsomorphisms
-- Init.Data.Char.Order
Char.instIsLinearOrder : Std.IsLinearOrder Char
-- Init.Util
/-- Print stack trace to stderr before evaluating given closure. Currently supported on Linux only.  -/
dbgStackTrace : {α : Type u} → (Unit → α) → α
-- Mathlib.Topology.Semicontinuity.Basic
LowerSemicontinuousAt.inf : ∀ {α : Type u_4} {β : Type u_5} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f g : α → β} {a : α},
  LowerSemicontinuousAt f a → LowerSemicontinuousAt g a → LowerSemicontinuousAt (fun x => min (f x) (g x)) a
-- Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
HasStrictFDerivAt.of_comp_of_leftInverse : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {g : E → F} {f : F → G} {h : E → G} {f' : F →L[𝕜] G}
  {h' : E →L[𝕜] G} {f'symm : G →L[𝕜] F} {a : E},
  ContinuousAt g a →
    HasStrictFDerivAt f f' (g a) →
      HasStrictFDerivAt h h' a →
        f ∘ g =ᶠ[nhds a] h → Function.LeftInverse ⇑f'symm ⇑f' → HasStrictFDerivAt g (f'symm ∘SL h') a
-- Mathlib.Topology.Closure
Disjoint.frontier_left : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsOpen t → Disjoint s t → Disjoint (frontier s) t
-- Mathlib.Order.Heyting.Basic
/-- Pullback a `GeneralizedCoheytingAlgebra` along an injection.  -/
Function.Injective.generalizedCoheytingAlgebra : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Max α] →
      [inst_1 : Min α] →
        [inst_2 : LE α] →
          [inst_3 : LT α] →
            [inst_4 : Bot α] →
              [inst_5 : SDiff α] →
                [inst_6 : GeneralizedCoheytingAlgebra β] →
                  (f : α → β) →
                    Function.Injective f →
                      (∀ {x y : α}, f x ≤ f y ↔ x ≤ y) →
                        (∀ {x y : α}, f x < f y ↔ x < y) →
                          (∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) →
                            (∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) →
                              f ⊥ = ⊥ → (∀ (a b : α), f (a \ b) = f a \ f b) → GeneralizedCoheytingAlgebra α
-- Mathlib.Analysis.Meromorphic.Order
/-- `meromorphicOrderAt` is invariant under translation.  -/
meromorphicOrderAt_comp_sub_const_eq_meromorphicOrderAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x c : 𝕜} {f : 𝕜 → E},
  meromorphicOrderAt (f ∘ fun x => x - c) x = meromorphicOrderAt f (x - c)
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasDerivWithinAt.congr : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f f₁ : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜},
  HasDerivWithinAt f f' s x → (∀ x ∈ s, f₁ x = f x) → f₁ x = f x → HasDerivWithinAt f₁ f' s x
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α} {k : α}, k ∈ m.insertManyIfNewUnit l ↔ k ∈ m ∨ l.contains k = true
-- Mathlib.RingTheory.Polynomial.Subring
Polynomial.degree_toSubring : ∀ {R : Type u_1} [inst : Ring R] (p : Polynomial R) (T : Subring R) (hp : ↑p.coeffs ⊆ ↑T),
  (p.toSubring T hp).degree = p.degree
-- Mathlib.RingTheory.PowerSeries.Evaluation
/-- The evaluation homomorphism at `a` on `PowerSeries`, as a `RingHom`.  -/
PowerSeries.eval₂Hom : {R : Type u_1} →
  [inst : CommRing R] →
    {S : Type u_2} →
      [inst_1 : CommRing S] →
        {φ : R →+* S} →
          {a : S} →
            [inst_2 : UniformSpace R] →
              [inst_3 : UniformSpace S] →
                [IsUniformAddGroup R] →
                  [IsTopologicalSemiring R] →
                    [IsUniformAddGroup S] →
                      [T2Space S] →
                        [CompleteSpace S] →
                          [IsTopologicalRing S] →
                            [IsLinearTopology S S] → Continuous ⇑φ → PowerSeries.HasEval a → PowerSeries R →+* S
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile.0.Std.IterM.step_intermediateDropWhileM.match_1.eq_2 : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} [inst : MonadAttach m] {P : β → m (ULift.{u_1, 0} Bool)} (out : β)
  (motive : Subtype (MonadAttach.CanReturn (P out)) → Sort u_3) (hP : MonadAttach.CanReturn (P out) { down := false })
  (h_1 : (hP : MonadAttach.CanReturn (P out) { down := true }) → motive ⟨{ down := true }, hP⟩)
  (h_2 : (hP : MonadAttach.CanReturn (P out) { down := false }) → motive ⟨{ down := false }, hP⟩),
  (match ⟨{ down := false }, hP⟩ with
    | ⟨{ down := true }, hP⟩ => h_1 hP
    | ⟨{ down := false }, hP⟩ => h_2 hP) =
    h_2 hP
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instInf : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : SemilatticeInf β] →
        [inst_2 : Zero β] →
          [inst_3 : TopologicalSpace β] → [ContinuousInf β] → Min (CompactlySupportedContinuousMap α β)
-- Mathlib.RingTheory.Bialgebra.TensorProduct
/-- Multiplication on a bialgebra as a coalgebra hom.  -/
Bialgebra.mulCoalgHom : (R : Type u_1) →
  (A : Type u_2) →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Bialgebra R A] → TensorProduct R A A →ₗc[R] A
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.prod_X_pow_eq_monomial : ∀ {R : Type u} {σ : Type u_1} {s : σ →₀ ℕ} [inst : CommSemiring R],
  ∏ x ∈ s.support, MvPolynomial.X x ^ s x = (MvPolynomial.monomial s) 1
-- Mathlib.GroupTheory.Index
Subgroup.IsFiniteRelIndex.relIndex_ne_zero : ∀ {G : Type u_1} {inst : Group G} {H K : Subgroup G} [self : H.IsFiniteRelIndex K], H.relIndex K ≠ 0
-- Init.Data.Bool
Bool.instAssociativeBne : Std.Associative fun x1 x2 => x1 != x2
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
Lean.Meta.Grind.Arith.CommRing.RingM.Context.mk.inj : ∀ {ringId : ℕ} {checkCoeffDvd : Bool} {ringId_1 : ℕ} {checkCoeffDvd_1 : Bool},
  { ringId := ringId, checkCoeffDvd := checkCoeffDvd } = { ringId := ringId_1, checkCoeffDvd := checkCoeffDvd_1 } →
    ringId = ringId_1 ∧ checkCoeffDvd = checkCoeffDvd_1
-- Mathlib.Order.PropInstances
Pi.disjoint_iff : ∀ {ι : Type u_1} {α' : ι → Type u_3} [inst : (i : ι) → PartialOrder (α' i)] [inst_1 : (i : ι) → OrderBot (α' i)]
  {f g : (i : ι) → α' i}, Disjoint f g ↔ ∀ (i : ι), Disjoint (f i) (g i)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.coe_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  (f : MeasureTheory.SimpleFunc β γ) {g : α → β} (hgm : Measurable g), ⇑(f.comp g hgm) = ⇑f ∘ g
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.sub_def : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Sub α] {s t : Finset α},
  s - t = Finset.image (fun p => p.1 - p.2) (s ×ˢ t)
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.Bool.bif_eq_bif : ∀ (d a b c : Bool), ((bif d then a else b) == bif d then a else c) = (d || b == c)
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.congr_toSkeleton_of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (e : X ≅ Y),
  CategoryTheory.toSkeleton X = CategoryTheory.toSkeleton Y
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousAlternatingMap.uniformContinuous_toContinuousMultilinearMap : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : UniformSpace F] [inst_7 : IsUniformAddGroup F],
  UniformContinuous ContinuousAlternatingMap.toContinuousMultilinearMap
-- Mathlib.Analysis.InnerProductSpace.Calculus
fderiv_norm_sq : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F],
  (fderiv ℝ fun x => ‖x‖ ^ 2) = 2 • ⇑(innerSL ℝ)
-- Mathlib.Order.BooleanAlgebra.Basic
/-- Transfer `BooleanAlgebra` across an `Equiv`.  -/
Equiv.booleanAlgebra : {α : Type u} → {β : Type u_1} → α ≃ β → [BooleanAlgebra β] → BooleanAlgebra α
-- Init.Grind.ToInt
Lean.Grind.IntInterval.ci.sizeOf_spec : ∀ (lo : ℤ), sizeOf (Lean.Grind.IntInterval.ci lo) = 1 + sizeOf lo
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.toBiconeFunctor_obj_ι : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} (b : CategoryTheory.Limits.BinaryBicone X Y) (j : CategoryTheory.Limits.WalkingPair),
  (CategoryTheory.Limits.BinaryBicone.toBiconeFunctor.obj b).ι j =
    CategoryTheory.Limits.WalkingPair.casesOn j b.inl b.inr
-- Mathlib.Data.List.Sublists
List.sublistsAux_eq_flatMap : ∀ {α : Type u}, List.sublistsAux = fun a r => List.flatMap (fun l => [l, a :: l]) r
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.natCast_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : NatCast β] (n : ℕ)
  (x : α), ↑n x = ↑n
-- Mathlib.CategoryTheory.Functor.EpiMono
/-- A functor preserves monomorphisms if it maps monomorphisms to monomorphisms.  -/
CategoryTheory.Functor.PreservesMonomorphisms : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.RingTheory.Finiteness.Ideal
Ideal.exists_pow_le_of_le_radical_of_fg_radical : ∀ {R : Type u_3} [inst : CommSemiring R] {I J : Ideal R}, I ≤ J.radical → J.radical.FG → ∃ k, I ^ k ≤ J
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso.eq_1 : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (i : 𝒰.I₀),
  AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso 𝒰 f g i =
    {
      hom :=
        CategoryTheory.Limits.pullback.lift
          (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.f i))
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.f i))
            (AlgebraicGeometry.Scheme.Pullback.p2 𝒰 f g))
          ⋯,
      inv :=
        CategoryTheory.Limits.pullback.lift ((AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).ι i)
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) ⋯,
      hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.S_zero : ∀ (R : Type u_1) [inst : CommRing R], Polynomial.Chebyshev.S R 0 = 1
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
LinearEquiv.ofLinearMap.congr_simp : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂}
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂}
  (f f_1 : M →ₛₗ[σ₁₂] M₂) (e_f : f = f_1) (g g_1 : M₂ →ₛₗ[σ₂₁] M) (e_g : g = g_1) (h₁ : f ∘ₛₗ g = LinearMap.id)
  (h₂ : g ∘ₛₗ f = LinearMap.id), LinearEquiv.ofLinearMap f g h₁ h₂ = LinearEquiv.ofLinearMap f_1 g_1 ⋯ ⋯
-- Mathlib.Combinatorics.Matroid.Loop
/-- A version of `restrict_loops_eq` without the hypothesis that `R ⊆ M.E`  -/
Matroid.restrict_loops_eq' : ∀ {α : Type u_1} (M : Matroid α) (R : Set α), (M.restrict R).loops = M.loops ∩ R ∪ R \ M.E
-- Mathlib.Algebra.Star.SelfAdjoint
/-- Scalar multiplication of a self-adjoint element by a skew-adjoint element produces a
skew-adjoint element.  -/
IsSelfAdjoint.smul_mem_skewAdjoint : ∀ {R : Type u_1} {A : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup A] [inst_2 : Module R A]
  [inst_3 : StarAddMonoid R] [inst_4 : StarAddMonoid A] [StarModule R A] {r : R},
  r ∈ skewAdjoint R → ∀ {a : A}, IsSelfAdjoint a → r • a ∈ skewAdjoint A
-- Mathlib.Algebra.GroupWithZero.Defs
MulDivCancelClass.mk : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Div M₀],
  (∀ (a b : M₀), b ≠ 0 → a * b / b = a) → MulDivCancelClass M₀
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.ε_η_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) (X : C)
  [inst_3 : F.Monoidal] {Z : C}
  (h : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor C C)).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.LaxMonoidal.ε F).app X)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.OplaxMonoidal.η F).app X) h) =
    h
-- Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
/-- Coercion from `E →Lₚₜ[𝕜] F` to `E →ₗ[𝕜] F` as a `𝕜`-linear map.  -/
PointwiseConvergenceCLM.coeLM : (𝕜 : Type u_3) →
  [inst : NormedField 𝕜] →
    (E : Type u_7) →
      (F : Type u_8) →
        [inst_1 : AddCommGroup E] →
          [inst_2 : TopologicalSpace E] →
            [inst_3 : AddCommGroup F] →
              [inst_4 : TopologicalSpace F] →
                [inst_5 : IsTopologicalAddGroup F] →
                  [inst_6 : Module 𝕜 E] →
                    [inst_7 : Module 𝕜 F] → [inst_8 : ContinuousConstSMul 𝕜 F] → (E →Lₚₜ[𝕜] F) →ₗ[𝕜] E →ₗ[𝕜] F
-- Mathlib.CategoryTheory.Sites.Over
/-- **Alias** of `BotHomClass.map_bot`. -/
CategoryTheory.Sieve.overEquiv_symm_bot : ∀ {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} {inst : Bot α} {inst_1 : Bot β}
  {inst_2 : FunLike F α β} [self : BotHomClass F α β] (f : F), f ⊥ = ⊥
-- Lean.Elab.Syntax
Lean.Elab.Command.elabSyntaxAbbrev : Lean.Elab.Command.CommandElab
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
IsCyclic.mulAutMulEquiv_symm_apply_symm_apply : ∀ (G : Type u_2) [inst : Group G] [h : IsCyclic G] (a : (ZMod (Nat.card G))ˣ) (a_1 : G),
  (MulEquiv.symm ((IsCyclic.mulAutMulEquiv G).symm a)) a_1 =
    (zmodCyclicMulEquiv h)
      (Multiplicative.ofAdd
        ((AddEquiv.symm ((↑(AddEquiv.toMultiplicative (ZMod.AddAutEquivUnits (Nat.card G)))).symm a))
          (Multiplicative.toAdd ((zmodCyclicMulEquiv h).symm a_1))))
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.toENat_eq_natCast : ∀ {c : Cardinal.{u}} {n : ℕ}, Cardinal.toENat c = ↑n ↔ c = ↑n
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithInitial.map.match_1.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (X Y : CategoryTheory.WithInitial C) → (X ⟶ Y) → Sort u_3) (a a_1 : C)
  (f : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of a_1)
  (h_1 :
    (a a_2 : C) →
      (f : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of a_2) →
        motive (CategoryTheory.WithInitial.of a) (CategoryTheory.WithInitial.of a_2) f)
  (h_2 :
    (a : C) →
      (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.of a) →
        motive CategoryTheory.WithInitial.star (CategoryTheory.WithInitial.of a) x)
  (h_3 :
    (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.star) →
      motive CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star x),
  (match CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of a_1, f with
    | CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of a_2, f => h_1 a a_2 f
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of a, x => h_2 a x
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => h_3 x) =
    h_1 a a_1 f
-- Init.NotationExtra
unexpandListToArray : Lean.PrettyPrinter.Unexpander
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.inrCompInlCompAssociator_inv_app_down_down : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (X : D),
  ((CategoryTheory.sum.inrCompInlCompAssociator C D E).inv.app X).down.down =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (Sum.inr (Sum.inl X))).down.down
      (CategoryTheory.CategoryStruct.id (Sum.inr (Sum.inl X))).down.down
-- Mathlib.RingTheory.Algebraic.Integral
IsAlgebraic.sub : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [NoZeroDivisors R]
  {a b : S}, IsAlgebraic R a → IsAlgebraic R b → IsAlgebraic R (a - b)
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.MonoidalCategory.pentagon : ∀ {R : Type u} [inst : CommSemiring R] (W : SemimoduleCat R) (X : SemimoduleCat R) (Y : SemimoduleCat R)
  (Z : SemimoduleCat R),
  CategoryTheory.CategoryStruct.comp
      (SemimoduleCat.MonoidalCategory.whiskerRight (SemimoduleCat.MonoidalCategory.associator W X Y).hom Z)
      (CategoryTheory.CategoryStruct.comp
        (SemimoduleCat.MonoidalCategory.associator W (SemimoduleCat.MonoidalCategory.tensorObj X Y) Z).hom
        (SemimoduleCat.MonoidalCategory.whiskerLeft W (SemimoduleCat.MonoidalCategory.associator X Y Z).hom)) =
    CategoryTheory.CategoryStruct.comp
      (SemimoduleCat.MonoidalCategory.associator (SemimoduleCat.MonoidalCategory.tensorObj W X) Y Z).hom
      (SemimoduleCat.MonoidalCategory.associator W X (SemimoduleCat.MonoidalCategory.tensorObj Y Z)).hom
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
RingSeminorm.ringSeminormClass : ∀ {R : Type u_1} [inst : NonUnitalRing R], RingSeminormClass (RingSeminorm R) R ℝ
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.ofAlgEquiv_map_apply : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f) {T : Type u_1} [inst_3 : Ring T] [inst_4 : Algebra R T] (e : S ≃ₐ[R] T) (x : Polynomial R),
  (h.ofAlgEquiv e).map x = e (h.map x)
-- Mathlib.Algebra.Order.Group.Synonym
isLeftRegular_ofLex : ∀ {α : Type u_1} [inst : Monoid α] {a : Lex α}, IsLeftRegular (ofLex a) ↔ IsLeftRegular a
-- Mathlib.Order.Basic
Pi.compl_apply : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : (i : ι) → Compl (π i)] (x : (i : ι) → π i) (i : ι), xᶜ i = (x i)ᶜ
-- Mathlib.Algebra.Group.Conj
conj_inv : ∀ {α : Type u} [inst : Group α] {a b : α}, (b * a * b⁻¹)⁻¹ = b * a⁻¹ * b⁻¹
-- Mathlib.Algebra.Group.Even
even_iff_exists_two_nsmul : ∀ {α : Type u_2} [inst : AddMonoid α] (a : α), Even a ↔ ∃ r, a = 2 • r
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
/-- To ease type checking, we also provide a version of inr that lives in
`SimplexCategory`.  -/
AugmentedSimplexCategory.inr' : (x y : SimplexCategory) → y ⟶ AugmentedSimplexCategory.tensorObjOf x y
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
/-- The identity arrows of the walking cospan.  -/
CategoryTheory.Limits.WalkingCospan.Hom.id : (X : CategoryTheory.Limits.WalkingCospan) → X ⟶ X
-- Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
BoundedContinuousFunction.apply_le_nndist_zero : ∀ {X : Type u_1} [inst : TopologicalSpace X] (f : BoundedContinuousFunction X NNReal) (x : X), f x ≤ nndist 0 f
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- `map₂` is invariant under isomorphisms.  -/
CategoryTheory.StructuredArrow.map₂Congr : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {A : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} A] →
            {B : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} B] →
                {L : D} →
                  {R : CategoryTheory.Functor C D} →
                    {L' : B} →
                      {R' : CategoryTheory.Functor A B} →
                        {F : CategoryTheory.Functor C A} →
                          {G : CategoryTheory.Functor D B} →
                            (α : L' ⟶ G.obj L) →
                              (β : R.comp G ⟶ F.comp R') →
                                {F' : CategoryTheory.Functor C A} →
                                  {G' : CategoryTheory.Functor D B} →
                                    (e₁ : F ≅ F') →
                                      (e₂ : G ≅ G') →
                                        (α' : L' ⟶ G'.obj L) →
                                          (β' : R.comp G' ⟶ F'.comp R') →
                                            autoParam (α = CategoryTheory.CategoryStruct.comp α' (e₂.inv.app L))
                                                CategoryTheory.StructuredArrow.map₂Congr._auto_1 →
                                              autoParam
                                                  (CategoryTheory.CategoryStruct.comp β
                                                      (CategoryTheory.Functor.whiskerRight e₁.hom R') =
                                                    CategoryTheory.CategoryStruct.comp (R.whiskerLeft e₂.hom) β')
                                                  CategoryTheory.StructuredArrow.map₂Congr._auto_3 →
                                                (CategoryTheory.StructuredArrow.map₂ α β ≅
                                                  CategoryTheory.StructuredArrow.map₂ α' β')
-- Mathlib.Combinatorics.Enumerative.Composition
/-- Embedding the `i`-th block of a composition (identified with `Fin (c.blocksFun i)`) into
`Fin n` at the relevant position.  -/
Composition.embedding : {n : ℕ} → (c : Composition n) → (i : Fin c.length) → Fin (c.blocksFun i) ↪o Fin n
-- Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
/-- By definition, every `LieAdmissibleRing` yields a `LieRing` with the commutator bracket.  -/
LieAdmissibleRing.instLieRing : {L : Type u_2} → [LieAdmissibleRing L] → LieRing L
-- Lean.Compiler.CSimpAttr
Lean.Compiler.CSimp.Entry : Type
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Functor.FullyFaithful.hasZeroMorphisms_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {F : CategoryTheory.Functor D C} (hF : F.FullyFaithful) (X Y : D),
  0 = hF.preimage 0