mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.Truncated.HomotopyCategory.mkNatIso_hom_app_mk : ∀ {V : SSet.Truncated 2} {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D]
  {F G : CategoryTheory.Functor V.HomotopyCategory D}
  (iso :
    (x : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })) →
      F.obj (SSet.Truncated.HomotopyCategory.mk x) ≅ G.obj (SSet.Truncated.HomotopyCategory.mk x))
  (hiso :
    autoParam
      (∀ ⦃x y : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })⦄
        (e : SSet.Truncated.Edge x y),
        CategoryTheory.CategoryStruct.comp (F.map (SSet.Truncated.HomotopyCategory.homMk e)) (iso y).hom =
          CategoryTheory.CategoryStruct.comp (iso x).hom (G.map (SSet.Truncated.HomotopyCategory.homMk e)))
      _auto_153✝)
  (v : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })),
  (SSet.Truncated.HomotopyCategory.mkNatIso iso hiso).hom.app (SSet.Truncated.HomotopyCategory.mk v) = (iso v).hom
-- Init.System.FilePath
/-- Extracts the extension part of `p.fileName`.

If the filename contains multiple extensions, then only the last one is extracted. Returns `none` if
there is no file name at the end of the path.

Examples:
 * `("app.exe" : System.FilePath).extension = some "exe"`
 * `("file.tar.gz" : System.FilePath).extension = some "gz"`
 * `("files/" : System.FilePath).extension = none`
 * `("files/picture.jpg" : System.FilePath).extension = some "jpg"`
 -/
System.FilePath.extension : System.FilePath → Option String
-- Mathlib.MeasureTheory.Measure.GiryMonad
/-- Monadic join on `Measure` in the category of measurable spaces and measurable
functions.  -/
MeasureTheory.Measure.join : {α : Type u_1} → {mα : MeasurableSpace α} → MeasureTheory.Measure (MeasureTheory.Measure α) → MeasureTheory.Measure α
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
/-- A bounded measurable function with compact support is in L^p.  -/
HasCompactSupport.memLp_of_bound : ∀ {E : Type u_2} {p : ENNReal} [inst : NormedAddCommGroup E] {X : Type u_3} [inst_1 : TopologicalSpace X]
  [inst_2 : MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {f : X → E},
  HasCompactSupport f →
    MeasureTheory.AEStronglyMeasurable f μ → ∀ (C : ℝ), (∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C) → MeasureTheory.MemLp f p μ
-- Mathlib.Topology.MetricSpace.Algebra
/-- The Lipschitz constant of an `AddMonoid` `β` satisfying `LipschitzAdd`  -/
LipschitzAdd.C : (β : Type u_2) → [inst : PseudoMetricSpace β] → [inst_1 : AddMonoid β] → [_i : LipschitzAdd β] → NNReal
-- Mathlib.Data.Nat.Digits.Lemmas
/-- The bijection `Nat.bijOn_digitsAppend` stated as a bijection between `Finset`.
This spelling can be helpful for some proofs.
 -/
Nat.bijOn_digitsAppend' : ∀ {b : ℕ} (hb : 1 < b) (l : ℕ), Set.BijOn (b.digitsAppend l) ↑(Finset.range (b ^ l)) ↑(List.fixedLengthDigits hb l)
-- Mathlib.Data.Set.NAry
Set.image2_left : ∀ {α : Type u_1} {β : Type u_3} {s : Set α} {t : Set β}, t.Nonempty → Set.image2 (fun x x_1 => x) s t = s
-- Mathlib.Data.Rel
SetRel.IsRefl.comp : ∀ {α : Type u_1} {R₁ R₂ : SetRel α α} [R₁.IsRefl] [R₂.IsRefl], (R₁.comp R₂).IsRefl
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.Nat.add_two_pow_eq_or_of_lt : ∀ {b : ℕ} (i : ℕ), b < 2 ^ i → ∀ (a : ℕ), b + 2 ^ i * a = b ||| 2 ^ i * a
-- Mathlib.Data.Set.Sigma
Set.image_sigmaMk_subset_sigma_right : ∀ {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι}, i ∈ s → Sigma.mk i '' t i ⊆ s.sigma t
-- Mathlib.Data.Part
Part.toOption.eq_1 : ∀ {α : Type u_1} (o : Part α) [inst : Decidable o.Dom], o.toOption = if h : o.Dom then some (o.get h) else none
-- Mathlib.Topology.MetricSpace.Antilipschitz
AntilipschitzWith.ediam_preimage_le : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
  AntilipschitzWith K f → ∀ (s : Set β), Metric.ediam (f ⁻¹' s) ≤ ↑K * Metric.ediam s
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.degree_mul_C : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {a : R} [NoZeroDivisors R],
  a ≠ 0 → (p * Polynomial.C a).degree = p.degree
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.rightUnshift_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L M : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) {m a : ℤ}
  (γ' : CochainComplex.HomComplex.Cochain L ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj M) m) {nm : ℤ}
  (hnm : n + m = nm) (nm' : ℤ) (hnm' : nm + a = nm') (m' : ℤ) (hm' : m + a = m'),
  (γ.comp γ' hnm).rightUnshift nm' hnm' = γ.comp (γ'.rightUnshift m' hm') ⋯
-- Mathlib.Analysis.Convex.Deriv
ConvexOn.monotoneOn_rightDeriv : ∀ {S : Set ℝ} {f : ℝ → ℝ}, ConvexOn ℝ S f → MonotoneOn (fun x => derivWithin f (Set.Ioi x) x) (interior S)
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.continuous_tmul : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F],
  Continuous fun x => x.1 ⊗ₜ[𝕜] x.2
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- The unipotent lower triangular matrix
```
(1 0)
(r 1)
```
as an isomorphism.
 -/
CategoryTheory.Biprod.unipotentLower : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] → {X₁ X₂ : C} → (X₂ ⟶ X₁) → (X₁ ⊞ X₂ ≅ X₁ ⊞ X₂)
-- Mathlib.Computability.EpsilonNFA
εNFA.IsPath.below : {α : Type u} →
  {σ : Type v} →
    {M : εNFA α σ} →
      {motive : (a a_1 : σ) → (a_2 : List (Option α)) → M.IsPath a a_1 a_2 → Prop} →
        {a a_1 : σ} → {a_2 : List (Option α)} → M.IsPath a a_1 a_2 → Prop
-- Mathlib.Algebra.Module.CharacterModule
CharacterModule.ofSpanSingleton.eq_1 : ∀ {A : Type uA} [inst : AddCommGroup A] (a : A),
  CharacterModule.ofSpanSingleton a =
    (Submodule.liftQSpanSingleton (↑(addOrderOf a))
          (AddMonoidHom.toIntLinearMap (CharacterModule.int.divByNat (if addOrderOf a = 0 then 2 else addOrderOf a)))
          ⋯ ∘ₗ
        ↑(CharacterModule.intSpanEquivQuotAddOrderOf a)).toAddMonoidHom
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- Homotopy between morphisms of short complexes is compatible with addition.  -/
CategoryTheory.ShortComplex.Homotopy.add : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        {φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂} →
          CategoryTheory.ShortComplex.Homotopy φ₁ φ₂ →
            CategoryTheory.ShortComplex.Homotopy φ₃ φ₄ → CategoryTheory.ShortComplex.Homotopy (φ₁ + φ₃) (φ₂ + φ₄)
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.addHom_ext' : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_5} [inst_1 : AddMonoid M] {f g : SkewPolynomial R →+ M},
  (∀ (n : ℕ), f.comp (SkewPolynomial.monomial n).toAddMonoidHom = g.comp (SkewPolynomial.monomial n).toAddMonoidHom) →
    f = g
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
AlgHom.le_equalizer : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] {φ ψ : A →ₐ[R] B} {S : Subalgebra R A},
  S ≤ φ.equalizer ψ ↔ Set.EqOn ⇑φ ⇑ψ ↑S
-- Mathlib.GroupTheory.GroupAction.Primitive
AddAction.IsBlock.subsingleton_or_eq_univ : ∀ {G : Type u_1} {X : Type u_2} [inst : VAdd G X] [AddAction.IsPreprimitive G X] {B : Set X},
  AddAction.IsBlock G B → B.Subsingleton ∨ B = Set.univ
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.inter_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp}, t₁.inter t₂ = t₁ ∩ t₂
-- Mathlib.Topology.Path
ContinuousAt.pathExtend : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {g : Y → ℝ} {l r : Y → X}
  (γ : (y : Y) → Path (l y) (r y)) {y : Y},
  ContinuousAt ↿γ (y, Set.projIcc 0 1 ⋯ (g y)) → ContinuousAt g y → ContinuousAt (fun i => (γ i).extend (g i)) y
-- Batteries.Data.String.Lemmas
String.offsetOfPos_of_valid : ∀ (l r : List Char), String.Pos.Raw.offsetOfPos (String.ofList (l ++ r)) { byteIdx := String.utf8Len l } = l.length
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
/-- The map of a fan is a limit iff the fan consisting of the mapped morphisms is a limit. This
essentially lets us commute `Fan.mk` with `Functor.mapCone`.
 -/
CategoryTheory.Limits.isLimitMapConeFanMkEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {J : Type w} →
            (f : J → C) →
              {P : C} →
                (g : (j : J) → P ⟶ f j) →
                  CategoryTheory.Limits.IsLimit (G.mapCone (CategoryTheory.Limits.Fan.mk P g)) ≃
                    CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk (G.obj P) fun j => G.map (g j))
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.mono_iff_isZero_kernel : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} (f : X ⟶ Y)
  [inst_2 : CategoryTheory.Limits.HasKernel f],
  CategoryTheory.Mono f ↔ CategoryTheory.Limits.IsZero (CategoryTheory.Limits.kernel f)
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.isPosSemidef_def : ∀ {R : Type u_1} {M : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {I₁ : R →+* R}
  [inst_3 : LE R] {B : M →ₛₗ[I₁] M →ₗ[R] R}, B.IsPosSemidef ↔ B.IsSymm ∧ B.IsNonneg
-- Init.Data.Slice.Notation
/-- Slices `carrier` up to `range.upper` \(exclusive\).
   -/
Std.Rio.Sliceable.mkSlice : {α : Type u} → {β : outParam (Type v)} → {γ : outParam (Type w)} → [self : Std.Rio.Sliceable α β γ] → α → Std.Rio β → γ
-- Mathlib.Topology.Defs.Basic
/-- An open quotient map is an open map.  -/
IsOpenQuotientMap.isOpenMap : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsOpenQuotientMap f → IsOpenMap f
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.expansion_smul_finset : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (K : ℝ) (S A : Finset G) (a : G),
  Finset.expansion✝ K S (a • A) = Finset.expansion✝ K S A
-- Mathlib.Logic.Equiv.Sum
Equiv.sumCompl_apply_inr : ∀ {α : Type u_9} {p : α → Prop} [inst : DecidablePred p] (x : { a // ¬p a }), (Equiv.sumCompl p) (Sum.inr x) = ↑x
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.S_neg_two : ∀ (R : Type u_1) [inst : CommRing R], Polynomial.Chebyshev.S R (-2) = -1
-- Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
/-- **Alias** of `CategoryTheory.Precoverage.toGrothendieck_comap_eq_restrictedTopology`. -/
CategoryTheory.Precoverage.toGrothendieck_comap_eq_inducedTopology : ∀ {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_3, u_3} C]
  [inst_1 : CategoryTheory.Category.{v_4, u_4} D] (F : CategoryTheory.Functor C D) (K : CategoryTheory.Precoverage D)
  [K.HasIsos] [K.IsStableUnderBaseChange] [K.IsStableUnderComposition] [K.HasPullbacks] [F.Faithful] [F.Full],
  (∀ {S : C} {R : CategoryTheory.Presieve (F.obj S)},
      R ∈ K.coverings (F.obj S) →
        CategoryTheory.Presieve.map F (CategoryTheory.Presieve.functorPullback F R) ∈ K.coverings (F.obj S)) →
    (CategoryTheory.Precoverage.comap F K).toGrothendieck = F.restrictedTopology K.toGrothendieck
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Multiset.toFinset_sum_count_eq : ∀ {ι : Type u_1} [inst : DecidableEq ι] (s : Multiset ι), ∑ a ∈ s.toFinset, Multiset.count a s = s.card
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.functorOfNatTransComp_inv_app_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F₀ F₁ F₂ : CategoryTheory.Functor C C} (α : F₀ ⟶ F₁)
  (β : F₁ ⟶ F₂) (X : CategoryTheory.Endofunctor.Algebra F₂),
  ((CategoryTheory.Endofunctor.Algebra.functorOfNatTransComp α β).inv.app X).f = CategoryTheory.CategoryStruct.id X.a
-- Mathlib.Algebra.Category.MonCat.Limits
/-- The category of commutative monoids has all limits.  -/
CommMonCat.hasLimitsOfSize : ∀ [UnivLE.{v, u}], CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} CommMonCat
-- Mathlib.Algebra.Module.Presentation.Basic
/-- Given `relations : Relations A` and a solution in `relations.Solution M`, this is
the linear map `(relations.G →₀ A) →ₗ[A] M` canonically associated to the solution.  -/
Module.Relations.Solution.π : {A : Type u} →
  [inst : Ring A] →
    {relations : Module.Relations A} →
      {M : Type v} →
        [inst_1 : AddCommGroup M] → [inst_2 : Module A M] → relations.Solution M → (relations.G →₀ A) →ₗ[A] M
-- Mathlib.Data.PNat.Basic
PNat.le_one_iff : ∀ {n : ℕ+}, n ≤ 1 ↔ n = 1
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.isoOfEq_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B : C} (X Y : CategoryTheory.Subobject B) (h : X = Y),
  (X.isoOfEq Y h).hom = X.ofLE Y ⋯
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- A vector measure `v` is absolutely continuous with respect to a measure `μ` if for all sets
`s`, `μ s = 0`, we have `v s = 0`.  -/
MeasureTheory.VectorMeasure.AbsolutelyContinuous : {α : Type u_1} →
  {m : MeasurableSpace α} →
    {M : Type u_4} →
      {N : Type u_5} →
        [inst : AddCommMonoid M] →
          [inst_1 : TopologicalSpace M] →
            [inst_2 : AddCommMonoid N] →
              [inst_3 : TopologicalSpace N] → MeasureTheory.VectorMeasure α M → MeasureTheory.VectorMeasure α N → Prop
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Over
CategoryTheory.Limits.PreservesFiniteColimits.underPost : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : C} {F : CategoryTheory.Functor C D} [CategoryTheory.Limits.PreservesFiniteColimits F],
  CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.Under.post F)
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.exists_lt_add_of_not_isPrincipal_add : ∀ {a : Ordinal.{u}}, ¬Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) a → ∃ b < a, ∃ c < a, b + c = a
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aeval_one : ∀ {R : Type u} {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A),
  (Polynomial.aeval x) 1 = 1
-- Mathlib.Combinatorics.Additive.Energy
Finset.addEnergy_comm : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : AddCommMonoid α] (s t : Finset α), s.addEnergy t = t.addEnergy s
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbol.mk.injEq : ∀ (sym sym_1 : Lean.Lsp.DocumentSymbolAux Lean.Lsp.DocumentSymbol),
  (Lean.Lsp.DocumentSymbol.mk sym = Lean.Lsp.DocumentSymbol.mk sym_1) = (sym = sym_1)
-- Init.Data.Vector.Lemmas
Vector.toList_push : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {x : α}, (xs.push x).toList = xs.toList ++ [x]
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc.0.CategoryTheory.Limits.termW_1 : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.Scheme.toSpecΓ_naturality : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp f Y.toSpecΓ =
    CategoryTheory.CategoryStruct.comp X.toSpecΓ (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.appTop f))
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  {f g : α ≃*o β}, (∀ (a : α), f a = g a) → f = g
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.closedInterior_sdiff_interior : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [inst_4 : LinearOrder k] [IsOrderedAddMonoid k] [ZeroLEOneClass k] {n : ℕ}
  [inst_7 : NeZero n] (s : Affine.Simplex k P n), s.closedInterior \ s.interior = ⋃ i, (s.faceOpposite i).closedInterior
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.T_derivative_eq_U : ∀ {R : Type u_1} [inst : CommRing R] (n : ℤ),
  Polynomial.derivative (Polynomial.Chebyshev.T R n) = ↑n * Polynomial.Chebyshev.U R (n - 1)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t₁.WF → t₂.WF → ∀ {k : α}, (t₁ \ t₂).getKey! k = if k ∈ t₂ then default else t₁.getKey! k
-- Mathlib.RingTheory.WittVector.FrobeniusFractionField
_private.Mathlib.RingTheory.WittVector.FrobeniusFractionField.0.WittVector.frobeniusRotationCoeff.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.Algebra.Polynomial.Laurent
Polynomial.toLaurent_C : ∀ {R : Type u_1} [inst : Semiring R] (r : R), Polynomial.toLaurent (Polynomial.C r) = LaurentPolynomial.C r
-- Mathlib.Order.Hom.Basic
/-- Evaluation of an unbundled function at a point (`Function.eval`) as an `OrderHom`.  -/
Pi.evalOrderHom : {ι : Type u_6} → {π : ι → Type u_7} → [inst : (i : ι) → Preorder (π i)] → (i : ι) → ((j : ι) → π j) →o π i
-- Mathlib.Combinatorics.SimpleGraph.Trails
SimpleGraph.Walk.IsTrail.isEulerian_of_forall_mem : ∀ {V : Type u_1} {G : SimpleGraph V} [inst : DecidableEq V] {u v : V} {p : G.Walk u v},
  p.IsTrail → (∀ e ∈ G.edgeSet, e ∈ p.edges) → p.IsEulerian
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instAddQuotient : {R : Type u_1} → [inst : Add R] → [inst_1 : Mul R] → (c : RingCon R) → Add c.Quotient
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.of_mul_add_right_left : ∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsRelPrime (z * y + x) y → IsRelPrime x y
-- Mathlib.Analysis.Convex.LinearIsometry
LinearIsometry.strictConvexSpace_range_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedField 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F]
  (e : E →ₗᵢ[𝕜] F), StrictConvexSpace 𝕜 ↥(↑e).range ↔ StrictConvexSpace 𝕜 E
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.Quotient.dividedPowers_unique : ∀ {A : Type u_1} [inst : CommRing A] {I : Ideal A} (hI : DividedPowers I) {J : Ideal A} (hIJ : hI.IsSubDPIdeal (J ⊓ I))
  (hquot : DividedPowers (Ideal.map (Ideal.Quotient.mk J) I)),
  hI.IsDPMorphism hquot (Ideal.Quotient.mk J) → hquot = DividedPowers.Quotient.dividedPowers hI hIJ
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotientMulEquivQuotientProd_fst : ∀ {R : Type u_2} [inst : CommRing R] (I J : Ideal R) (coprime : IsCoprime I J) (x : R ⧸ I * J),
  ((I.quotientMulEquivQuotientProd J coprime) x).1 = (Ideal.Quotient.factor ⋯) x
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.Config.mk.inj : ∀ {verbose enforceUnfoldReducible enforceFoldProjs verbose_1 enforceUnfoldReducible_1 enforceFoldProjs_1 : Bool},
  { verbose := verbose, enforceUnfoldReducible := enforceUnfoldReducible, enforceFoldProjs := enforceFoldProjs } =
      { verbose := verbose_1, enforceUnfoldReducible := enforceUnfoldReducible_1,
        enforceFoldProjs := enforceFoldProjs_1 } →
    verbose = verbose_1 ∧ enforceUnfoldReducible = enforceUnfoldReducible_1 ∧ enforceFoldProjs = enforceFoldProjs_1
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.centerToMulOpposite_symm_apply_coe : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (r : ↥(Subsemigroup.center Rᵐᵒᵖ)),
  ↑(NonUnitalSubsemiring.centerToMulOpposite.symm r) = MulOpposite.unop ↑r
-- Mathlib.Order.Minimal
maximal_mem_iff : ∀ {α : Type u_2} {x : α} [inst : PartialOrder α] {s : Set α},
  Maximal (fun x => x ∈ s) x ↔ x ∈ s ∧ ∀ ⦃y : α⦄, y ∈ s → x ≤ y → x = y
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubAddAction.ofStabilizer.eq_1 : ∀ (G : Type u_1) [inst : AddGroup G] {α : Type u_2} [inst_1 : AddAction G α] (a : α),
  SubAddAction.ofStabilizer G a = { carrier := {a}ᶜ, vadd_mem' := ⋯ }
-- Mathlib.RingTheory.Localization.Finiteness
/-- If `S` is an `R' = M⁻¹R` algebra, and `x ∈ adjoin R' s`,
then `t • x ∈ adjoin R s` for some `t : M`.  -/
multiple_mem_adjoin_of_mem_localization_adjoin : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (M : Submonoid R) (R' : Type u_3)
  [inst_2 : CommSemiring R'] [inst_3 : Algebra R R'] [inst_4 : Algebra R' S] [inst_5 : Algebra R S]
  [IsScalarTower R R' S] [IsLocalization M R'] (s : Set S), ∀ x ∈ Algebra.adjoin R' s, ∃ t, t • x ∈ Algebra.adjoin R s
-- Init.Data.SInt.Lemmas
Int8.mul_add : ∀ {a b c : Int8}, a * (b + c) = a * b + a * c
-- Mathlib.Analysis.SpecialFunctions.Exp
Complex.continuousOn_exp : ∀ {s : Set ℂ}, ContinuousOn Complex.exp s
-- Mathlib.CategoryTheory.Enriched.Basic
/-- The underlying natural transformation of an enriched transformation.  -/
CategoryTheory.EnrichedNatTrans.out : {V : Type v} →
  [inst : CategoryTheory.Category.{w, v} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₁} →
        [inst_2 : CategoryTheory.EnrichedCategory V C] →
          {D : Type u₂} →
            [inst_3 : CategoryTheory.EnrichedCategory V D] →
              {F G : CategoryTheory.EnrichedFunctor V C D} → CategoryTheory.EnrichedNatTrans F G → (F.forget ⟶ G.forget)
-- Mathlib.Topology.Order.DenselyOrdered
Ico_mem_nhds_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [NoMinOrder α] {a b x : α}, Set.Ico a b ∈ nhds x ↔ x ∈ Set.Ioo a b
-- Init.Data.Int.LemmasAux
Int.ofNat_add_out : ∀ (m n : ℕ), ↑m + ↑n = ↑(m + n)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.instRespectsIsoOfIsStableUnderBaseChange : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.IsStableUnderBaseChange],
  J.RespectsIso
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.filterMap.match_1.eq_1 : ∀ {α : Type u_1} {γ : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl.BalancedTree α γ → Sort u_3)
  (r' : Std.DTreeMap.Internal.Impl α γ) (hr' : r'.Balanced)
  (h_1 : (r' : Std.DTreeMap.Internal.Impl α γ) → (hr' : r'.Balanced) → motive { impl := r', balanced_impl := hr' }),
  (match { impl := r', balanced_impl := hr' } with
    | { impl := r', balanced_impl := hr' } => h_1 r' hr') =
    h_1 r' hr'
-- Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
/-- Variant of `MeromorphicOn.circleIntegrable_posLog_norm` for non-negative radii.
 -/
MeromorphicOn.circleIntegrable_posLog_norm_of_nonneg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {c : ℂ} {R : ℝ} {f : ℂ → E},
  MeromorphicOn f (Metric.sphere c R) → 0 ≤ R → CircleIntegrable (fun x => ‖f x‖.posLog) c R
-- Mathlib.Algebra.Group.Defs
nsmulBinRec.eq_1 : ∀ {M : Type u_2} [inst : Zero M] [inst_1 : Add M] (k : ℕ), nsmulBinRec k = nsmulBinRec.go k 0
-- Init.Data.List.TakeDrop
List.map_take : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {i : ℕ},
  List.map f (List.take i l) = List.take i (List.map f l)
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.lift_pre : ∀ {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] (E : CategoryTheory.Functor K J)
  [inst_4 : CategoryTheory.Limits.HasLimit (E.comp F)] (c : CategoryTheory.Limits.Cone F),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.lift F c) (CategoryTheory.Limits.limit.pre F E) =
    CategoryTheory.Limits.limit.lift (E.comp F) (CategoryTheory.Limits.Cone.whisker E c)
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Multiset.sum_pair : ∀ {M : Type u_3} [inst : AddCommMonoid M] (a b : M), {a, b}.sum = a + b