mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_roc_succ_right_eq_append_map : ∀ {m n : ℤ}, m ≤ n → (m<...=n + 1).toArray = #[m + 1] ++ Array.map (fun x => x + 1) (m<...=n).toArray
-- Mathlib.Data.PNat.Order
PNat.instNoMaxOrder : NoMaxOrder ℕ+
-- Std.Tactic.BVDecide.LRAT.Internal.Entails
/-- `f1` and `f2` are logically equivalent  -/
Std.Tactic.BVDecide.LRAT.Internal.Liff : (α : Type u) →
  {σ1 : Type v} →
    {σ2 : Type w} →
      [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ1] →
        [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ2] → σ1 → σ2 → Prop
-- Init.Control.StateRef
StateRefT'.instMonadFunctor : {ω : Type} → (σ : Type) → (m : Type → Type) → MonadFunctor m (StateRefT' ω σ m)
-- Mathlib.Analysis.Calculus.DiffContOnCl
DiffContOnCl.continuousOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E},
  DiffContOnCl 𝕜 f s → ContinuousOn f (closure s)
-- Mathlib.Topology.Clopen
isClopen_biInter_finset : ∀ {X : Type u} [inst : TopologicalSpace X] {Y : Type u_2} {s : Finset Y} {f : Y → Set X},
  (∀ i ∈ s, IsClopen (f i)) → IsClopen (⋂ i ∈ s, f i)
-- Lean.Elab.DocString
/-- Environment extension for docstring roles  -/
Lean.Doc.docCodeBlockExt : Lean.SimpleScopedEnvExtension (Lean.Name × Lean.Name) (Lean.NameMap (Array Lean.Name))
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
TensorProduct.finsuppRight_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] {N : Type u_4}
  [inst_7 : AddCommMonoid N] [inst_8 : Module R N] {ι : Type u_5} [inst_9 : DecidableEq ι]
  (t : TensorProduct R M (ι →₀ N)) (i : ι),
  ((TensorProduct.finsuppRight R S M N ι) t) i = (LinearMap.lTensor M (Finsupp.lapply i)) t
-- Mathlib.Data.Set.Basic
Set.inter_subset_inter : ∀ {α : Type u} {s₁ s₂ t₁ t₂ : Set α}, s₁ ⊆ t₁ → s₂ ⊆ t₂ → s₁ ∩ s₂ ⊆ t₁ ∩ t₂
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
CategoryTheory.Adjunction.hasRightCalculusOfFractions' : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁}
  [F.Full] [F.Faithful] (adj : F ⊣ G),
  ((CategoryTheory.MorphismProperty.isomorphisms C₂).inverseImage G).HasRightCalculusOfFractions
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- (Implementation). An auxiliary lemma to convert between sheaf conditions.  -/
CategoryTheory.Presheaf.isSheafForIsSheafFor' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        [inst_2 : CategoryTheory.Limits.HasProducts A] →
          [inst_3 : CategoryTheory.Limits.HasPullbacks C] →
            (P : CategoryTheory.Functor Cᵒᵖ A) →
              (s : CategoryTheory.Functor A (Type (max v₁ u₁))) →
                [∀ (J : Type (max v₁ u₁)), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete J) s] →
                  (U : C) →
                    (R : CategoryTheory.Presieve U) →
                      CategoryTheory.Limits.IsLimit
                          (s.mapCone (CategoryTheory.Limits.Fork.ofι (CategoryTheory.Presheaf.forkMap R P) ⋯)) ≃
                        CategoryTheory.Limits.IsLimit
                          (CategoryTheory.Limits.Fork.ofι (CategoryTheory.Equalizer.forkMap (P.comp s) R) ⋯)
-- Mathlib.FieldTheory.Finite.Extension
FiniteField.Extension.exists_frob_pow_eq : ∀ (k : Type u_1) [inst : Field k] [inst_1 : Finite k] (p : ℕ) [inst_2 : Fact (Nat.Prime p)] [inst_3 : CharP k p] (n : ℕ)
  [inst_4 : NeZero n] (g : Gal(FiniteField.Extension k p n/k)), ∃ i < n, FiniteField.Extension.frob k p n ^ i = g
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_map_of_getKey?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [Inhabited γ] {f : α → β → γ} {k k' : α} {fallback : γ},
  t.getKey? k = some k' →
    Std.ExtDTreeMap.Const.getD (Std.ExtDTreeMap.map f t) k fallback =
      (Option.map (f k') (Std.ExtDTreeMap.Const.get? t k)).getD fallback
-- Lean.Elab.Tactic.RCases
/-- Runs `rcasesContinue` on the first pattern in `r` with a matching `ctorName`.
The unprocessed patterns (subsequent to the matching pattern) are returned.  -/
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.rcasesCore.align : {α : Type} →
  Lean.Meta.FVarSubst →
    Array Lean.FVarId →
      (Lean.MVarId → Lean.Meta.FVarSubst → Array Lean.FVarId → α → Lean.Elab.TermElabM α) →
        α →
          Lean.Meta.InductionSubgoal →
            Option Lean.Name →
              List (Lean.Name × List Lean.Elab.Tactic.RCases.RCasesPatt) →
                Lean.Elab.TermElabM (List (Lean.Name × List Lean.Elab.Tactic.RCases.RCasesPatt) × α)
-- Init.Data.List.Basic
/-- Rotates the elements of `xs` to the right, moving `i % xs.length` elements from the end of the list
to the start.

After rotation, the element at `xs[n]` is at index `(i + n) % l.length`. `O(|xs|)`.

Examples:
* `[1, 2, 3, 4, 5].rotateRight 3 = [3, 4, 5, 1, 2]`
* `[1, 2, 3, 4, 5].rotateRight 5 = [1, 2, 3, 4, 5]`
* `[1, 2, 3, 4, 5].rotateRight 1 = [5, 1, 2, 3, 4]`
 -/
List.rotateRight : {α : Type u} → List α → optParam ℕ 1 → List α
-- Init.Data.String.Basic
/-- Returns the byte at the given position in the string, or panics if the position is the end
position.  -/
String.Slice.Pos.get! : {s : String.Slice} → s.Pos → Char
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.Rel.mul : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {m n : ℕ}
  {a : M},
  DividedPowerAlgebra.Rel R M (MvPolynomial.X (m, a) * MvPolynomial.X (n, a))
    ((m + n).choose m • MvPolynomial.X (m + n, a))
-- Mathlib.CategoryTheory.Sites.PreservesLimits
instPreservesFiniteCoproductsSheafTypeYonedaOfPreservesFiniteProductsOppositeObjFunctorIsSheaf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : J.Subcanonical]
  [∀ (X : CategoryTheory.Sheaf J (Type v)), CategoryTheory.Limits.PreservesFiniteProducts X.obj],
  CategoryTheory.Limits.PreservesFiniteCoproducts J.yoneda
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.Hom.Simps.hom.eq_1 : ∀ (X Y : CommMonCat) (f : X.Hom Y), CommMonCat.Hom.Simps.hom X Y f = f.hom
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.instSliceableImplUnitRoiSlice : {α : Type u} →
  [inst : Ord α] →
    Std.Roi.Sliceable (Std.DTreeMap.Internal.Impl α fun x => Unit) α (Std.DTreeMap.Internal.Unit.RoiSlice α)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- Negating a rotation is equivalent to rotation by π plus the angle.  -/
Orientation.neg_rotation : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle) (x : V), -(o.rotation θ) x = (o.rotation (↑Real.pi + θ)) x
-- Batteries.Data.Nat.Bisect
_private.Batteries.Data.Nat.Bisect.0.Nat.bisect.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (x = false → motive false) → (x = true → motive true) → motive x
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.MVarValue.expr.sizeOf_spec : ∀ (e : Lean.Expr), sizeOf (Aesop.EqualUpToIds.MVarValue.expr e) = 1 + sizeOf e
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.toLin.eq_1 : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R],
  Matrix.GeneralLinearGroup.toLin = Units.mapEquiv Matrix.toLinAlgEquiv'.toMulEquiv
-- Mathlib.Analysis.Analytic.Uniqueness
/-- A one-dimensional formal multilinear series representing the zero function is zero.  -/
HasFPowerSeriesAt.eq_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} {x : 𝕜}, HasFPowerSeriesAt 0 p x → p = 0
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Problem.instInhabitedFourierMotzkinData : Inhabited Lean.Elab.Tactic.Omega.Problem.FourierMotzkinData
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.map_top : ∀ {α : Type u_1} {β : Type u_2} (f : α → β),
  (MeasureTheory.OuterMeasure.map f) ⊤ = (MeasureTheory.OuterMeasure.restrict (Set.range f)) ⊤
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.mapOpcyclesIso_hom_naturality_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S₁.HasRightHomology]
  [inst_6 : S₂.HasRightHomology] [inst_7 : F.PreservesRightHomologyOf S₁] [inst_8 : F.PreservesRightHomologyOf S₂]
  {Z : D} (h : F.obj S₂.opcycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap (F.mapShortComplex.map φ))
      (CategoryTheory.CategoryStruct.comp (S₂.mapOpcyclesIso F).hom h) =
    CategoryTheory.CategoryStruct.comp (S₁.mapOpcyclesIso F).hom
      (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.opcyclesMap φ)) h)
-- Lean.Elab.Tactic.RCases
/-- A type ascription like `pat : ty` (parentheses are optional)  -/
Lean.Elab.Tactic.RCases.RCasesPatt.typed : Lean.Syntax → Lean.Elab.Tactic.RCases.RCasesPatt → Lean.Term → Lean.Elab.Tactic.RCases.RCasesPatt
-- Init.Core
/-- `flip f a b` is `f b a`. It is useful for "point-free" programming,
since it can sometimes be used to avoid introducing variables.
For example, `(·<·)` is the less-than relation,
and `flip (·<·)` is the greater-than relation.
 -/
flip : {α : Sort u} → {β : Sort v} → {φ : Sort w} → (α → β → φ) → β → α → φ
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_eq_true_of_mod_eq_zero : ∀ {a b : ℤ}, (b % a == 0) = true → (a ∣ b) = True
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.trans_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Mul α] [inst_1 : Add α] [inst_2 : LE α] [inst_3 : Mul β]
  [inst_4 : Add β] [inst_5 : LE β] [inst_6 : Mul γ] [inst_7 : Add γ] [inst_8 : LE γ] (f : α ≃+*o β) (g : β ≃+*o γ)
  (a : α), (f.trans g) a = g (f a)
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.id_val : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {p : F.Elements},
  ↑(CategoryTheory.CategoryStruct.id p) = CategoryTheory.CategoryStruct.id p.fst
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.co.injEq : ∀ (lo hi lo_1 hi_1 : Lean.Meta.Grind.Arith.Cutsat.SymbolicBound),
  (Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.co lo hi =
      Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.co lo_1 hi_1) =
    (lo = lo_1 ∧ hi = hi_1)
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.t2Space_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α], T2Space (TopologicalSpace.NonemptyCompacts α) ↔ T2Space α
-- Mathlib.Analysis.Convex.Hull
Convex.convexHull_subset_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s t : Set E}, Convex 𝕜 t → ((convexHull 𝕜) s ⊆ t ↔ s ⊆ t)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
/-- Returns an array of indices corresponding to clauses that contain the negation of l  -/
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.getRatClauseIndices : {n : ℕ} →
  Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)) →
    Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Array ℕ
-- Mathlib.Data.Finsupp.MonomialOrder
MonomialOrder.zero_le : ∀ {σ : Type u_1} (m : MonomialOrder σ) (a : m.syn), 0 ≤ a
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- If `recheck` is `true`, then new equalities have been added to the basis since we checked
disequalities and implied equalities.
 -/
Lean.Meta.Grind.Arith.CommRing.CommRing.recheck : Lean.Meta.Grind.Arith.CommRing.CommRing → Bool
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerLeft_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (W : C)
  {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft W (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W f)
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W g)
-- Mathlib.CategoryTheory.Subfunctor.Equalizer
CategoryTheory.Subfunctor.range_le_equalizer_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F₁ F₂ : CategoryTheory.Functor C (Type w)}
  {A : CategoryTheory.Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) {G : CategoryTheory.Functor C (Type w)}
  (φ : G ⟶ A.toFunctor),
  CategoryTheory.Subfunctor.range (CategoryTheory.CategoryStruct.comp φ A.ι) ≤ CategoryTheory.Subfunctor.equalizer f g ↔
    CategoryTheory.CategoryStruct.comp φ f = CategoryTheory.CategoryStruct.comp φ g
-- Mathlib.Tactic.Ring.NamePowerVars
/-- The command `name_power_vars` names variables in
`MvPowerSeries (Fin n) R` for the appropriate value of `n`.
The notation introduced by this command is local.

Usage:

```lean
variable (R : Type) [CommRing R]

name_power_vars X, Y, Z over R

#check Y -- Y : MvPowerSeries (Fin 3) R
```
 -/
Mathlib.Tactic.namePowerVarsOver : Lean.ParserDescr
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- The equalizer of two non-unital `R`-algebra homomorphisms  -/
NonUnitalAlgHom.equalizer : {F : Type v'} →
  {R : Type u} →
    {A : Type v} →
      {B : Type w} →
        [inst : CommSemiring R] →
          [inst_1 : NonUnitalNonAssocSemiring A] →
            [inst_2 : Module R A] →
              [inst_3 : NonUnitalNonAssocSemiring B] →
                [inst_4 : Module R B] →
                  [inst_5 : FunLike F A B] → [NonUnitalAlgHomClass F R A B] → F → F → NonUnitalSubalgebra R A
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.of_coe : ∀ {α : Type u} (f : Ultrafilter α), Ultrafilter.of ↑f = f
-- Mathlib.RingTheory.WittVector.Identities
/-- Verschiebung is the same as multiplication by `p` on the ring of Witt vectors of `ZMod p`.  -/
WittVector.verschiebung_zmod : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (x : WittVector p (ZMod p)), WittVector.verschiebung x = x * ↑p
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.below.triangle : ∀ {C : Type u}
  {motive :
    {X Y : CategoryTheory.FreeMonoidalCategory C} →
      (a a_1 : X.Hom Y) → CategoryTheory.FreeMonoidalCategory.HomEquiv a a_1 → Prop}
  {X Y : CategoryTheory.FreeMonoidalCategory C}, CategoryTheory.FreeMonoidalCategory.HomEquiv.below ⋯
-- Batteries.Data.List.Lemmas
List.dropInfix?.go.eq_def : ∀ {α : Type u_1} [inst : BEq α] (i a a_1 : List α),
  List.dropInfix?.go i a a_1 =
    match a, a_1 with
    | [], acc => if i.isEmpty = true then some (acc.reverse, []) else none
    | a :: as, acc =>
      match (a :: as).dropPrefix? i with
      | none => List.dropInfix?.go i as (a :: acc)
      | some s => some (acc.reverse, s)
-- Mathlib.Topology.Perfect
IsOpen.preperfect : ∀ {α : Type u_1} [inst : TopologicalSpace α] [PerfectSpace α] {U : Set α}, IsOpen U → Preperfect U
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanOrder.orderHom.eq_1 : ∀ {M : Type u_2} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {N : Type u_3}
  [inst_3 : CommGroup N] [inst_4 : LinearOrder N] [inst_5 : IsOrderedMonoid N] (f : M →*o N),
  MulArchimedeanOrder.orderHom f =
    { toFun := fun a => MulArchimedeanOrder.of (f (MulArchimedeanOrder.val a)), monotone' := ⋯ }
-- Mathlib.Analysis.Calculus.Deriv.ZPow
iter_deriv_pow' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (n k : ℕ),
  (deriv^[k] fun x => x ^ n) = fun x => (∏ i ∈ Finset.range k, (↑n - ↑i)) * x ^ (n - k)
-- Mathlib.Tactic.FieldSimp
_private.Mathlib.Tactic.FieldSimp.0.Mathlib.Tactic.FieldSimp.qNF.mul.match_1.eq_2 : ∀ {v : Lean.Level} {M : Q(Type v)}
  (motive : Mathlib.Tactic.FieldSimp.qNF q(«$M») → Mathlib.Tactic.FieldSimp.qNF q(«$M») → Sort u_1)
  (l : Mathlib.Tactic.FieldSimp.qNF q(«$M»)) (h_1 : (l : Mathlib.Tactic.FieldSimp.qNF q(«$M»)) → motive [] l)
  (h_2 : (l : Mathlib.Tactic.FieldSimp.qNF q(«$M»)) → motive l [])
  (h_3 :
    (a₁ : ℤ) →
      (x₁ : Q(«$M»)) →
        (k₁ : ℕ) →
          (t₁ : List ((ℤ × Q(«$M»)) × ℕ)) →
            (a₂ : ℤ) →
              (x₂ : Q(«$M»)) →
                (k₂ : ℕ) → (t₂ : List ((ℤ × Q(«$M»)) × ℕ)) → motive (((a₁, x₁), k₁) :: t₁) (((a₂, x₂), k₂) :: t₂)),
  (l = [] → False) →
    (match l, [] with
      | [], l => h_1 l
      | l, [] => h_2 l
      | ((a₁, x₁), k₁) :: t₁, ((a₂, x₂), k₂) :: t₂ => h_3 a₁ x₁ k₁ t₁ a₂ x₂ k₂ t₂) =
      h_2 l
-- Mathlib.Data.Set.Function
Function.Semiconj.injOn_image : ∀ {α : Type u_1} {β : Type u_2} {fa : α → α} {fb : β → β} {f : α → β} {s : Set α},
  Function.Semiconj f fa fb → Set.InjOn fa s → Set.InjOn f (fa '' s) → Set.InjOn fb (f '' s)
-- Lean.Server.FileWorker.ExampleHover
_private.Lean.Server.FileWorker.ExampleHover.0.Lean.Server.FileWorker.Hover.RWState.nonOutput.sizeOf_spec : ∀ (ticks : ℕ), sizeOf (Lean.Server.FileWorker.Hover.RWState.nonOutput✝ ticks) = 1 + sizeOf ticks
-- Mathlib.Combinatorics.Additive.FreimanHom
IsMulFreimanHom.comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : CommMonoid α] [inst_1 : CommMonoid β] [inst_2 : CommMonoid γ]
  {A : Set α} {B : Set β} {C : Set γ} {f : α → β} {g : β → γ} {n : ℕ},
  IsMulFreimanHom n B C g → IsMulFreimanHom n A B f → IsMulFreimanHom n A C (g ∘ f)
-- Init.Data.FloatArray.Basic
FloatArray.instBEq : BEq FloatArray
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.num_smul : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A] {𝒜 : ι → σ} (x : Submonoid A)
  {α : Type u_4} [inst_2 : SMul α A] [inst_3 : SMulMemClass σ α A] (c : HomogeneousLocalization.NumDenSameDeg 𝒜 x)
  (m : α), ↑(m • c).num = m • ↑c.num
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.curryAlgEquiv_single : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Monoid M] [inst_4 : Monoid N] (m : M) (n : N) (a : A),
  (MonoidAlgebra.curryAlgEquiv R) (MonoidAlgebra.single (m, n) a) = MonoidAlgebra.single m (MonoidAlgebra.single n a)
-- Mathlib.Algebra.Order.Antidiag.Prod
Finset.HasAntidiagonal.antidiagonal.fst_le : ∀ {A : Type u_1} [inst : AddCommMonoid A] [inst_1 : PartialOrder A] [CanonicallyOrderedAdd A]
  [inst_3 : Finset.HasAntidiagonal A] {n : A} {kl : A × A}, kl ∈ Finset.HasAntidiagonal.antidiagonal n → kl.1 ≤ n
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.two_le_pi : 2 ≤ Real.pi
-- Mathlib.Order.Comparable
/-- **Alias** of `CompRel.of_le`. -/
LE.le.compRel : ∀ {α : Type u_1} {a b : α} [inst : LE α], a ≤ b → CompRel (fun x1 x2 => x1 ≤ x2) a b
-- Mathlib.Algebra.Homology.Single
ChainComplex.fromSingle₀Equiv_symm_apply_f_succ : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {C : ChainComplex V ℕ} {X : V} (f : X ⟶ C.X 0) (n : ℕ),
  ((C.fromSingle₀Equiv X).symm f).f (n + 1) = 0
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.liftOrderBot.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : OrderBot α] [inst_2 : PartialOrder β] {l : α → β}
  {u : β → α} (gc : GaloisConnection l u), gc.liftOrderBot = { bot := l ⊥, bot_le := ⋯ }
-- Mathlib.Order.Heyting.Basic
/-- `⊤ \ a` is `￢a`  -/
BiheytingAlgebra.top_sdiff : ∀ {α : Type u_4} [self : BiheytingAlgebra α] (a : α), ⊤ \ a = ￢a
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
IsCompact.measure_zero_of_nhdsWithin : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α},
  IsCompact s → (∀ a ∈ s, ∃ t ∈ nhdsWithin a s, μ t = 0) → μ s = 0
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.InitResults.mk : {α : Type} →
  Lean.Meta.LazyDiscrTree.PreDiscrTree α →
    Array Lean.Meta.LazyDiscrTree.ImportFailure → Lean.Meta.LazyDiscrTree.InitResults α
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.tan_pi_div_six : Real.tan (Real.pi / 6) = 1 / √3
-- Init.Data.UInt.Lemmas
UInt64.ofNatClamp_uInt16ToNat : ∀ (n : UInt16), UInt64.ofNatClamp n.toNat = n.toUInt64
-- Mathlib.NumberTheory.NumberField.CMField
/-- Any field `F` such that `K/F` is a CM-extension is isomorphic to the maximal real subfield of `K`.
 -/
NumberField.CMExtension.equivMaximalRealSubfield : (F : Type u_1) →
  (K : Type u_2) →
    [inst : Field F] →
      [NumberField.IsTotallyReal F] →
        [inst_2 : Field K] →
          [inst_3 : CharZero K] →
            [Algebra.IsIntegral ℚ K] →
              [NumberField.IsTotallyComplex K] →
                [inst_6 : Algebra F K] → [Algebra.IsQuadraticExtension F K] → F ≃+* ↥(NumberField.maximalRealSubfield K)
-- Mathlib.Algebra.Polynomial.UnitTrinomial
Polynomial.IsUnitTrinomial.irreducible_of_coprime : ∀ {p : Polynomial ℤ}, p.IsUnitTrinomial → IsRelPrime p p.mirror → Irreducible p
-- Mathlib.CategoryTheory.Limits.Cones
/-- A map from the vertex of a cocone induces a cocone by composition.  -/
CategoryTheory.Limits.Cocone.extend : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (c : CategoryTheory.Limits.Cocone F) → {X : C} → (c.pt ⟶ X) → CategoryTheory.Limits.Cocone F
-- Mathlib.Algebra.BigOperators.Fin
/-- Equivalence between `∀ i : Fin m, Fin (n i)` and `Fin (∏ i : Fin m, n i)`.  -/
finPiFinEquiv : {m : ℕ} → {n : Fin m → ℕ} → ((i : Fin m) → Fin (n i)) ≃ Fin (∏ i, n i)
-- Mathlib.Geometry.Manifold.Instances.Real
frontier_range_modelWithCornersEuclideanHalfSpace : ∀ (n : ℕ) [inst : NeZero n], frontier (Set.range ↑(modelWithCornersEuclideanHalfSpace n)) = {y | 0 = y.ofLp 0}
-- Lean.Parser.Term
Lean.Parser.Term.valConfigItem.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- On an orthogonal basis, the basis representation of `Q` is just a sum of squares.  -/
QuadraticMap.basisRepr_eq_of_iIsOrtho : ∀ {ι : Type u_8} [inst : Fintype ι] {R : Type u_9} {M : Type u_10} [inst_1 : CommRing R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : Invertible 2] (Q : QuadraticForm R M) (v : Module.Basis ι R M),
  LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑v →
    QuadraticMap.basisRepr Q v = QuadraticMap.weightedSumSquares R fun i => Q (v i)
-- Lean.Data.Lsp.Utf16
_private.Lean.Data.Lsp.Utf16.0.Lean.FileMap.lineStartPos : Lean.FileMap → ℕ → String.Pos.Raw
-- Mathlib.Combinatorics.Additive.Energy
Finset.le_addEnergy : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Add α] {s t : Finset α}, s.card * t.card ≤ s.addEnergy t
-- Init.Data.String.Iterate
String.Slice.ByteIterator.mk : String.Slice → String.Pos.Raw → String.Slice.ByteIterator
-- Mathlib.AlgebraicTopology.ModelCategory.Over
HomotopicalAlgebra.instHasFactorizationOverCofibrationsTrivialFibrations : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (S : C)
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [(HomotopicalAlgebra.cofibrations C).HasFactorization (HomotopicalAlgebra.trivialFibrations C)],
  (HomotopicalAlgebra.cofibrations (CategoryTheory.Over S)).HasFactorization
    (HomotopicalAlgebra.trivialFibrations (CategoryTheory.Over S))
-- Mathlib.Algebra.Ring.AddAut
AddAut.mulLeft_apply_symm_apply : ∀ {R : Type u_1} [inst : Semiring R] (x : Rˣ) (a : R), (AddEquiv.symm (AddAut.mulLeft x)) a = x⁻¹ • a
-- Mathlib.Analysis.Normed.Group.Int
Int.abs_le_floor_nnreal_iff : ∀ (z : ℤ) (c : NNReal), |z| ≤ ↑⌊c⌋₊ ↔ ‖z‖₊ ≤ c