mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.mapN_type₂ : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι)
  [inst_1 : P.IsProper] [inst_2 : SuccOrder ι] [inst_3 : NoMaxOrder ι] {j : ι} (c : f.Cell j),
  f.mapN (SSet.Subcomplex.Pairing.RankFunction.Cell.type₂ f c) = { dim := (↑c.s).dim, simplex := (↑c.s).simplex }
-- Mathlib.Algebra.Star.MonoidHom
StarMonoidHom.instFunLike : {A : Type u_2} →
  {B : Type u_3} →
    [inst : Monoid A] → [inst_1 : Star A] → [inst_2 : Monoid B] → [inst_3 : Star B] → FunLike (A →⋆* B) A B
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes left covariance.
The lemma assuming right covariance is `Right.add_pos'`.  -/
Left.add_pos' : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftMono α] {a b : α}, 0 < a → 0 < b → 0 < a + b
-- Lean.Data.Options
Lean.OptionDecl.mk : Lean.Name →
  autoParam Lean.Name Lean.OptionDecl.declName._autoParam →
    Lean.DataValue → String → Option Lean.OptionDeprecation → Lean.OptionDecl
-- Mathlib.Data.List.Sigma
List.dlookup_nil : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α), List.dlookup a [] = none
-- Mathlib.Topology.Homotopy.Product
/-- Abbreviation for projection onto the ith coordinate.  -/
Path.Homotopic.proj : {ι : Type u_1} →
  {X : ι → Type u_2} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      {as bs : (i : ι) → X i} → (i : ι) → Path.Homotopic.Quotient as bs → Path.Homotopic.Quotient (as i) (bs i)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getD_inter_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α} {fallback : β k}, k ∉ m₁ → (m₁ ∩ m₂).getD k fallback = fallback
-- Mathlib.Geometry.Euclidean.MongePoint
/-- Suppose we are given a triangle `t₁`, and replace one of its
vertices by its orthocenter, yielding triangle `t₂` (with vertices not
necessarily listed in the same order).  Then an altitude of `t₂` from
a vertex that was not replaced is the corresponding side of `t₁`.  -/
Affine.Triangle.altitude_replace_orthocenter_eq_affineSpan : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {t₁ t₂ : Affine.Triangle ℝ P} {i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3},
  i₁ ≠ i₂ →
    i₁ ≠ i₃ →
      i₂ ≠ i₃ →
        j₁ ≠ j₂ →
          j₁ ≠ j₃ →
            j₂ ≠ j₃ →
              t₂.points j₁ = t₁.orthocenter →
                t₂.points j₂ = t₁.points i₂ →
                  t₂.points j₃ = t₁.points i₃ → Affine.Simplex.altitude t₂ j₂ = line[ℝ, t₁.points i₁, t₁.points i₂]
-- Mathlib.Logic.Equiv.Basic
Equiv.Perm.sumCongr_swap_refl : ∀ {α : Type u_9} {β : Type u_10} [inst : DecidableEq α] [inst_1 : DecidableEq β] (i j : α),
  (Equiv.swap i j).sumCongr (Equiv.refl β) = Equiv.swap (Sum.inl i) (Sum.inl j)
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.ExactPairing.tensor_evaluation : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X₁ X₂ Y₁ Y₂ : C} [inst_2 : CategoryTheory.ExactPairing X₁ Y₁] [inst_3 : CategoryTheory.ExactPairing X₂ Y₂],
  ε_ (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂) (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₂ Y₁) =
    CategoryTheory.monoidalComp
      (CategoryTheory.CategoryStruct.id
        (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₂ Y₁)
          (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂)))
      (CategoryTheory.monoidalComp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y₂
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight (ε_ X₁ Y₁) X₂))
        (ε_ X₂ Y₂))
-- Init.Data.BitVec.Lemmas
BitVec.not_lt_iff_le : ∀ {w : ℕ} {x y : BitVec w}, ¬x < y ↔ y ≤ x
-- Mathlib.LinearAlgebra.Dual.Basis
/-- `simp` normal form version of `linearCombination_dualBasis`  -/
Module.Basis.linearCombination_coord : ∀ {R : Type uR} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Finite ι] (b : Module.Basis ι R M) (f : ι →₀ R) (i : ι), ((Finsupp.linearCombination R b.coord) f) (b i) = f i
-- Mathlib.Analysis.Normed.Group.NullSubmodule
/-- The additive null subgroup with respect to the norm.  -/
nullAddSubgroup : (M : Type u_1) → [inst : SeminormedAddCommGroup M] → AddSubgroup M
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- Any type satisfying `AddMonoidHomClass` and `ContinuousMapClass` can be cast into
`ContinuousAddMonoidHom` via `ContinuousAddMonoidHom.toContinuousAddMonoidHom`.  -/
ContinuousAddMonoidHom.instCoeOutOfAddMonoidHomClassOfContinuousMapClass : {A : Type u_2} →
  {B : Type u_3} →
    [inst : AddMonoid A] →
      [inst_1 : AddMonoid B] →
        [inst_2 : TopologicalSpace A] →
          [inst_3 : TopologicalSpace B] →
            {F : Type u_7} →
              [inst_4 : FunLike F A B] → [AddMonoidHomClass F A B] → [ContinuousMapClass F A B] → CoeOut F (A →ₜ+ B)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.symm_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D), e.symm.counit = e.unitInv
-- Mathlib.Data.Multiset.Bind
Multiset.coe_product : ∀ {α : Type u_1} {β : Type v} (l₁ : List α) (l₂ : List β), ↑l₁ ×ˢ ↑l₂ = ↑(l₁ ×ˢ l₂)
-- Mathlib.Probability.ConditionalProbability
ProbabilityTheory.instIsZeroOrProbabilityMeasureCond : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : Set Ω},
  MeasureTheory.IsZeroOrProbabilityMeasure μ[|s]
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
/-- Equivalence relation on monadic iterators. Equivalent iterators behave the same as long as the
internal state of them is not directly inspected.

Two iterators (possibly of different types) are equivalent if they have the same
`Iterator.IsPlausibleStep` relation and their step functions are the same *up to equivalence of the
successor iterators*. This coinductive definition captures the idea that the only relevant feature
of an iterator is its step function. Other information retrievable from the iterator -- for example,
whether it is a list iterator or an array iterator -- is totally irrelevant for the equivalence
judgement.
 -/
Std.IterM.Equiv : {m : Type w → Type w'} →
  [inst : Monad m] →
    [LawfulMonad m] →
      {β α₁ α₂ : Type w} → [Std.Iterator α₁ m β] → [Std.Iterator α₂ m β] → Std.IterM m β → Std.IterM m β → Prop
-- Mathlib.Data.Finsupp.Order
Finsupp.coe_tsub : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : CanonicallyOrderedAdd α]
  [inst_3 : Sub α] [inst_4 : OrderedSub α] (f g : ι →₀ α), ⇑(f - g) = ⇑f - ⇑g
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.outerMeasure_pos_of_is_mul_left_invariant : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] [inst_2 : Group G]
  [inst_3 : IsTopologicalGroup G],
  (∀ (g : G) {K : TopologicalSpace.Compacts G}, μ (TopologicalSpace.Compacts.map (fun x => g * x) ⋯ K) = μ K) →
    ∀ (K : TopologicalSpace.Compacts G), μ K ≠ 0 → ∀ {U : Set G}, IsOpen U → U.Nonempty → 0 < μ.outerMeasure U
-- Mathlib.RingTheory.PolynomialLaw.Basic
/-- The lift of `f.toFun` to the type `lifts`  -/
PolynomialLaw.φ : (R : Type u) →
  [inst : CommSemiring R] →
    {S : Type v} →
      [inst_1 : CommSemiring S] → [inst_2 : Algebra R S] → (s : Finset S) → MvPolynomial (Fin s.card) R →ₐ[R] S
-- Mathlib.Logic.Equiv.Finset
/-- `raise' l n` is a strictly increasing sequence.  -/
Denumerable.raise'_sorted : ∀ (l : List ℕ) (n : ℕ), (Denumerable.raise' l n).SortedLT
-- Lean.DocString.Types
Lean.Doc.Inline.footnote.sizeOf_spec : ∀ {i : Type u} [inst : SizeOf i] (name : String) (content : Array (Lean.Doc.Inline i)),
  sizeOf (Lean.Doc.Inline.footnote name content) = 1 + sizeOf name + sizeOf content
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.of : {C : Type u} → C → CategoryTheory.WithTerminal C
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.card_index_eq_twelve : ∀ {ι : 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) [P.EmbeddedG2]
  [Finite ι] [CharZero R] [IsDomain R] [P.IsIrreducible], Nat.card ι = 12
-- Mathlib.Algebra.Homology.Opposite
/-- Sends a complex `X` with objects in `V` to the corresponding complex with objects in `Vᵒᵖ`.  -/
HomologicalComplex.opSymm : {ι : Type u_1} →
  {V : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} V] →
      {c : ComplexShape ι} →
        [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] → HomologicalComplex V c.symm → HomologicalComplex Vᵒᵖ c
-- Mathlib.Data.Rat.Sqrt
Rat.sqrt_natCast : ∀ (n : ℕ), Rat.sqrt ↑n = ↑n.sqrt
-- Mathlib.LinearAlgebra.CliffordAlgebra.Grading
CliffordAlgebra.one_le_evenOdd_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M), 1 ≤ CliffordAlgebra.evenOdd Q 0
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- a morphism between the second lines  -/
CategoryTheory.ShortComplex.SnakeInput.Hom.f₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {S₁ S₂ : CategoryTheory.ShortComplex.SnakeInput C} → S₁.Hom S₂ → (S₁.L₂ ⟶ S₂.L₂)
-- Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
UpperHalfPlane.continuous_toSL2R : Continuous UpperHalfPlane.toSL2R
-- Mathlib.GroupTheory.OrderOfElement
/-- The equivalence between `Fin (orderOf x)` and `Submonoid.powers x`, sending `i` to `x ^ i`  -/
finEquivPowers : {G : Type u_1} → [inst : Monoid G] → {x : G} → IsOfFinOrder x → Fin (orderOf x) ≃ ↥(Submonoid.powers x)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_filter_of_getKey?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  {f : α → β → Bool} {k k' : α},
  t.WF →
    t.getKey? k = some k' →
      Std.DTreeMap.Raw.Const.get? (Std.DTreeMap.Raw.filter f t) k =
        Option.filter (fun x => f k' x) (Std.DTreeMap.Raw.Const.get? t k)
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.diam_range : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β]
  [inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F),
  Metric.diam (Set.range ⇑f) = ↑(Dilation.ratio f) * Metric.diam Set.univ
-- Mathlib.Data.Nat.Cast.Defs
/-- Recognize numeric literals which are at least `2` as terms of `R` via `Nat.cast`. This
instance is what makes things like `37 : R` type check.  Note that `0` and `1` are not needed
because they are recognized as terms of `R` (at least when `R` is an `AddMonoidWithOne`) through
`Zero` and `One`, respectively.  -/
instOfNatAtLeastTwo : {R : Type u_1} → {n : ℕ} → [NatCast R] → [n.AtLeastTwo] → OfNat R n
-- Mathlib.Analysis.InnerProductSpace.Orientation
/-- `adjustToOrientation` gives an orthonormal basis with the required orientation.  -/
OrthonormalBasis.orientation_adjustToOrientation : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {ι : Type u_2} [inst_2 : Fintype ι]
  [inst_3 : DecidableEq ι] (e : OrthonormalBasis ι ℝ E) (x : Orientation ℝ E ι) [inst_4 : Nonempty ι],
  (e.adjustToOrientation x).toBasis.orientation = x
-- Init.Data.Fin.Lemmas
Fin.sub_self : ∀ {n : ℕ} [inst : NeZero n] {x : Fin n}, x - x = 0
-- Mathlib.Algebra.Category.Grp.Yoneda
CommGrpCat.coyonedaForget.eq_1 : CommGrpCat.coyonedaForget =
  CategoryTheory.NatIso.ofComponents
    (fun X =>
      CategoryTheory.NatIso.ofComponents
        (fun Y =>
          { hom := TypeCat.ofHom fun f => CommGrpCat.ofHom f, inv := TypeCat.ofHom fun f => CommGrpCat.Hom.hom f,
            hom_inv_id := ⋯, inv_hom_id := ⋯ })
        ⋯)
    @CommGrpCat.coyonedaForget._proof_4
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_sub_div₀ : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10}
  {m : MeasurableSpace β} [inst : Sub β] [MeasurableSub₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), AEMeasurable (f i) μ) →
      ∀ (i j k l : ι), i ≠ k → i ≠ l → j ≠ k → j ≠ l → ProbabilityTheory.IndepFun (f i - f j) (f k - f l) μ
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
/-- The sum type `X ⊕ Y` forms a cocone for the binary coproduct of `X` and `Y`.  -/
CategoryTheory.Limits.Types.binaryCoproductCocone : (X Y : Type u) → CategoryTheory.Limits.Cocone (CategoryTheory.Limits.pair X Y)
-- Mathlib.SetTheory.ZFC.PSet
PSet.instIsEmptyTypeEmptyCollection : IsEmpty ∅.Type
-- Init.Data.String.PosRaw
String.Pos.Raw.pos_iff_ne_zero : ∀ {p : String.Pos.Raw}, 0 < p ↔ p ≠ 0
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.realize_rel₂ : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {v : α → M} {R : L.Relations 2}
  {t₁ t₂ : L.Term α},
  (R.formula₂ t₁ t₂).Realize v ↔
    FirstOrder.Language.Structure.RelMap R
      ![FirstOrder.Language.Term.realize v t₁, FirstOrder.Language.Term.realize v t₂]
-- Init.Data.Nat.Lemmas
Nat.sub_one_add_self : ∀ (n : ℕ), n - 1 + n = 2 * n - 1
-- Mathlib.RingTheory.Valuation.Basic
Valuation.map_mul : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  (x y : R), v (x * y) = v x * v y
-- Mathlib.Topology.CWComplex.Classical.Graph
Topology.CWComplex.OneSkeletonGraph.adj_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {C : Set X} [inst_1 : Topology.CWComplex C]
  (x y : Topology.RelCWComplex.cell C 0),
  (Topology.CWComplex.OneSkeletonGraph C).Adj x y ↔
    ∃ e,
      Topology.RelCWComplex.cellFrontier 1 e =
        Topology.RelCWComplex.closedCell 0 x ∪ Topology.RelCWComplex.closedCell 0 y
-- Mathlib.Algebra.Category.Ring.Under.Basic
CommRingCat.instCoeSortUnderType : {R : CommRingCat} → CoeSort (CategoryTheory.Under R) (Type u)
-- Mathlib.FieldTheory.IsPerfectClosure
/-- If `i : K →+* L` and `j : K →+* M` are ring homomorphisms of characteristic `p` rings, such that
`i` is `p`-radical, and `M` is a perfect ring, then `PerfectRing.liftAux`
is a ring homomorphism. This is similar to `IsAlgClosed.lift` and `IsSepClosed.lift`.  -/
PerfectRing.lift : {K : Type u_1} →
  {L : Type u_2} →
    {M : Type u_3} →
      [inst : CommRing K] →
        [inst_1 : CommRing L] →
          [inst_2 : CommRing M] →
            (i : K →+* L) →
              (K →+* M) →
                (p : ℕ) → [ExpChar M p] → [ExpChar K p] → [PerfectRing M p] → [IsPRadical i p] → [ExpChar L p] → L →+* M
-- Mathlib.RingTheory.Smooth.AdicCompletion
_private.Mathlib.RingTheory.Smooth.AdicCompletion.0.Algebra.FormallySmooth.liftAdicCompletionAux.eq_3 : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {S : Type u_3}
  [inst_3 : CommRing S] [inst_4 : Algebra R S] (I : Ideal S) (f : A →ₐ[R] S ⧸ I) [inst_5 : Algebra.FormallySmooth R A]
  (m : ℕ),
  Algebra.FormallySmooth.liftAdicCompletionAux✝ I f m.succ.succ =
    Algebra.FormallySmooth.lift (Ideal.map (Ideal.Quotient.mkₐ R (I ^ (m + 1 + 1))) (I ^ (m + 1))) ⋯
      ((↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R ⋯).symm).comp (Algebra.FormallySmooth.liftAdicCompletionAux✝ I f (m + 1)))
-- Init.Data.String.Subslice
String.Slice.Subslice.instCoeOut : {s : String.Slice} → CoeOut s.Subslice String.Slice
-- Mathlib.MeasureTheory.Measure.Trim
MeasureTheory.trim_add : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} (hm : m ≤ m0),
  (μ + ν).trim hm = μ.trim hm + ν.trim hm
-- Lean.Meta.Tactic.Grind.EMatch
/-- Stores new theorem instance in the state.
Recall that new instances are internalized later, after a full round of ematching.
 -/
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.addNewInstance : Lean.Meta.Grind.EMatchTheorem →
  Lean.Expr →
    ℕ → List Lean.Meta.Grind.TheoremGuard → Lean.PHashSet Lean.Meta.Grind.EMatchDiagNode → Lean.Meta.Grind.EMatch.M Unit
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
/-- A braided functor between braided monoidal categories is a monoidal functor
which preserves the braiding.
 -/
CategoryTheory.Functor.Braided : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.MonoidalCategory D] →
              [CategoryTheory.BraidedCategory D] → CategoryTheory.Functor C D → Type (max u₁ v₂)
-- Mathlib.FieldTheory.SeparableDegree
_private.Mathlib.FieldTheory.SeparableDegree.0.IntermediateField.finSepDegree_adjoin_simple_dvd_finrank : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (α : E),
  Field.finSepDegree F ↥F⟮α⟯ ∣ Module.finrank F ↥F⟮α⟯
-- Init.Data.List.ControlImpl
_private.Init.Data.List.ControlImpl.0.List.flatMapM.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → List (List β) → Sort u_3) (a : α) (as : List α) (bs : List (List β))
  (h_1 : (bs : List (List β)) → motive [] bs)
  (h_2 : (a : α) → (as : List α) → (bs : List (List β)) → motive (a :: as) bs),
  (match a :: as, bs with
    | [], bs => h_1 bs
    | a :: as, bs => h_2 a as bs) =
    h_2 a as bs
-- Mathlib.Analysis.Normed.Group.Pointwise
closedBall_one_div_singleton : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (x : E), Metric.closedBall 1 δ / {x} = Metric.closedBall x⁻¹ δ
-- Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
instProperlyDiscontinuousVAddSubtypeMemAddSubgroup : ∀ {Γ : Type u_1} {α : Type u_2} [inst : AddGroup Γ] [inst_1 : TopologicalSpace α] [inst_2 : VAdd Γ α]
  [ProperlyDiscontinuousVAdd Γ α] (G : AddSubgroup Γ), ProperlyDiscontinuousVAdd (↥G) α
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.Return.result : {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} →
  {w : ℕ} → Std.Tactic.BVDecide.BVExpr.Return aig w → aig.ExtendingRefVecEntry w
-- Mathlib.CategoryTheory.Abelian.Exact
CategoryTheory.ShortComplex.exact_kernel : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y),
  { X₁ := CategoryTheory.Limits.kernel f, X₂ := X, X₃ := Y, f := CategoryTheory.Limits.kernel.ι f, g := f,
      zero := ⋯ }.Exact
-- Init.Prelude
/-- Construct a synthetic `SourceInfo` from the `ref` in the monad state.  -/
Lean.MonadRef.mkInfoFromRefPos : {m : Type → Type} → [Monad m] → [Lean.MonadRef m] → m Lean.SourceInfo
-- Mathlib.FieldTheory.IsSepClosed
/-- An algebraically closed field is also separably closed.  -/
IsSepClosed.of_isAlgClosed : ∀ (k : Type u) [inst : Field k] [IsAlgClosed k], IsSepClosed k
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.equivUnits_symm_apply_symm_apply : ∀ {G : Type u_1} [inst : Add G] {a : G} (u : (AddConstMap G G a a)ˣ), ⇑(AddConstEquiv.equivUnits.symm u).symm = ⇑↑u⁻¹
-- Init.Data.BitVec.Lemmas
/-- A nonzero bitvector is lower-bounded by its trailing zeroes.  -/
BitVec.two_pow_ctz_le_toNat_of_ne_zero : ∀ {w : ℕ} {x : BitVec w}, x ≠ 0#w → 2 ^ x.ctz.toNat ≤ x.toNat
-- Mathlib.Data.DFinsupp.Defs
/-- Note the general `SMul` instance doesn't apply as `ℤ` is not distributive
unless `β i`'s addition is commutative.  -/
DFinsupp.hasIntScalar : {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → AddGroup (β i)] → SMul ℤ (Π₀ (i : ι), β i)
-- Lean.Meta.CoeAttr
Lean.Meta.CoeFnType.coeSort.sizeOf_spec : sizeOf Lean.Meta.CoeFnType.coeSort = 1
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.instZeroHom : {S : Type u_1} →
  [inst : AddMonoidWithOne S] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.HasShift C S] →
            [(CategoryTheory.shiftFunctor C 1).PreservesZeroMorphisms] →
              {X Y : CategoryTheory.DifferentialObject S C} → Zero (X ⟶ Y)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Cell.ofOption.match_1.splitter : {α : Type u_3} →
  {β : α → Type u_1} →
    (k : α) →
      (motive : Option (β k) → Sort u_2) →
        (v? : Option (β k)) → (Unit → motive none) → ((v : β k) → motive (some v)) → motive v?
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.leftUnitorImpl_hom_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C),
  X.leftUnitorImpl.hom.F =
    CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.terminal.from (((⊤_ C) ⨯ X.src) ⨯ X.tgt))
      CategoryTheory.Limits.prod.snd
-- Mathlib.RingTheory.KrullDimension.Basic
/-- If `I` is an ideal of `R`, then `ringKrullDim (R ⧸ I) ≤ ringKrullDim R`.  -/
ringKrullDim_quotient_le : ∀ {R : Type u_3} [inst : CommRing R] (I : Ideal R), ringKrullDim (R ⧸ I) ≤ ringKrullDim R
-- Mathlib.Algebra.Ring.Subsemiring.Defs
/-- The natural ring hom from a subsemiring of semiring `R` to `R`.  -/
Subsemiring.subtype : {R : Type u} → [inst : NonAssocSemiring R] → (s : Subsemiring R) → ↥s →+* R
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instOrdDiagnosticRelatedInformation.ord : Lean.Lsp.DiagnosticRelatedInformation → Lean.Lsp.DiagnosticRelatedInformation → Ordering
-- Mathlib.Topology.Constructions
Finset.continuous_restrict : ∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] (s : Finset ι), Continuous s.restrict
-- Mathlib.Data.ENNReal.Operations
ENNReal.mul_right_strictMono : ∀ {a : ENNReal}, a ≠ 0 → a ≠ ⊤ → StrictMono fun x => a * x
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.toMvPolynomial_eval_eq_apply : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {ι₁ : Type u_4} {ι₂ : Type u_5} [inst : CommRing R]
  [inst_1 : AddCommGroup M₁] [inst_2 : AddCommGroup M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂]
  [inst_5 : Fintype ι₁] [inst_6 : Finite ι₂] [inst_7 : DecidableEq ι₁] (b₁ : Module.Basis ι₁ R M₁)
  (b₂ : Module.Basis ι₂ R M₂) (f : M₁ →ₗ[R] M₂) (i : ι₂) (c : ι₁ →₀ R),
  (MvPolynomial.eval ⇑c) (LinearMap.toMvPolynomial b₁ b₂ f i) = (b₂.repr (f (b₁.repr.symm c))) i
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instSMul.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {K : Type u_5} [inst_1 : SMul K β],
  MeasureTheory.SimpleFunc.instSMul = { smul := fun k f => MeasureTheory.SimpleFunc.map (fun x => k • x) f }
-- Mathlib.Logic.Equiv.Basic
Equiv.semiconj₂_conj : ∀ {α₁ : Type u_11} {β₁ : Type u_12} (e : α₁ ≃ β₁) (f : α₁ → α₁ → α₁),
  Function.Semiconj₂ (⇑e) f ((e.arrowCongr e.conj) f)
-- Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.arrowMap_functor_to_top : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Φ : CategoryTheory.SmallObject.SuccStruct C}
  {J : Type u} [inst_1 : LinearOrder J] [inst_2 : OrderBot J] [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  [inst_5 : CategoryTheory.Limits.HasIterationOfShape J C] {j : J} (hj : Order.IsSuccLimit j)
  (iter : (i : J) → i < j → Φ.Iteration i) (i : J) (hi : i < j),
  CategoryTheory.SmallObject.SuccStruct.arrowMap
      (CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.functor hj iter) i j ⋯ ⋯ =
    CategoryTheory.Arrow.mk
      (CategoryTheory.Limits.colimit.ι (CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.inductiveSystem iter)
        ⟨i, hi⟩)
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.mk.injEq : ∀ {A : Type u_9} {B : Type u_10} [inst : Add A] [inst_1 : Add B] (toEquiv : A ≃ B)
  (map_add' : ∀ (x y : A), toEquiv.toFun (x + y) = toEquiv.toFun x + toEquiv.toFun y) (toEquiv_1 : A ≃ B)
  (map_add'_1 : ∀ (x y : A), toEquiv_1.toFun (x + y) = toEquiv_1.toFun x + toEquiv_1.toFun y),
  ({ toEquiv := toEquiv, map_add' := map_add' } = { toEquiv := toEquiv_1, map_add' := map_add'_1 }) =
    (toEquiv = toEquiv_1)