mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic
CategoryTheory.MonoidalCategory.externalProductSwap_hom_app_app : ∀ (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) [inst : CategoryTheory.Category.{v₁, u₁} J₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  [inst_3 : CategoryTheory.MonoidalCategory C] [inst_4 : CategoryTheory.BraidedCategory C]
  (X : CategoryTheory.Functor J₁ C × CategoryTheory.Functor J₂ C) (X_1 : J₂ × J₁),
  ((CategoryTheory.MonoidalCategory.externalProductSwap J₁ J₂ C).hom.app X).app X_1 =
    (β_ (X.1.obj X_1.2) (X.2.obj X_1.1)).hom
-- Init.Data.List.Nat.TakeDrop
List.mem_take_iff_getElem : ∀ {α : Type u_1} {i : ℕ} {l : List α} {a : α}, a ∈ List.take i l ↔ ∃ j, ∃ (hm : j < min i l.length), l[j] = a
-- Mathlib.Order.Basic
/-- **Alias** of `eq_or_lt_of_le`. -/
LE.le.eq_or_lt : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, a ≤ b → a = b ∨ a < b
-- Mathlib.LinearAlgebra.Finsupp.Pi
FunOnFinite.map.eq_1 : ∀ {M : Type u_5} [inst : AddCommMonoid M] {X : Type u_6} {Y : Type u_7} [inst_1 : Finite X] [inst_2 : Finite Y]
  (f : X → Y) (s : X → M),
  FunOnFinite.map f s = Finsupp.equivFunOnFinite (Finsupp.mapDomain f (Finsupp.equivFunOnFinite.symm s))
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
nnnorm_cfcₙ_nnreal_le_iff : ∀ {A : Type u_1} [inst : NonUnitalNormedRing A] [inst_1 : StarRing A] [inst_2 : NormedSpace ℝ A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : SMulCommClass ℝ A A] [inst_5 : PartialOrder A] [inst_6 : StarOrderedRing A]
  [inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_8 : NonnegSpectrumClass ℝ A]
  (f : NNReal → NNReal) (a : A) (c : NNReal),
  autoParam (ContinuousOn f (quasispectrum NNReal a)) nnnorm_cfcₙ_nnreal_le_iff._auto_1 →
    autoParam (f 0 = 0) nnnorm_cfcₙ_nnreal_le_iff._auto_3 →
      autoParam (0 ≤ a) nnnorm_cfcₙ_nnreal_le_iff._auto_5 → (‖cfcₙ f a‖₊ ≤ c ↔ ∀ x ∈ quasispectrum NNReal a, f x ≤ c)
-- Mathlib.Tactic.SplitIfs
/-- `split_ifs` splits the main goal in two goals for every if-then-else expression it contains,
by applying excluded middle to the condition. If the goal has the form `g (if p then x else y)`,
`split_ifs` will result in two goals `h✝ : p ⊢ g x` and `h✝ : ¬p ⊢ g y`. If there are multiple
if-then-else expressions, then `split_ifs` will split them all, starting with a top-most one whose
condition does not contain another if-then-else expression.

* `split_ifs with h₁ h₂ h₃` names the introduced hypotheses.
  Note that names are not reused across splits: on a goal of the form
  `⊢ (if p then 1 else 2) + (if q then 3 else 4)`, use `split_ifs with hp hq hq` to name all
  the hypotheses.
* `split_ifs at l` splits the if-then-else expressions at location(s) `l`.
 -/
Mathlib.Tactic.splitIfs : Lean.ParserDescr
-- Mathlib.Data.Rat.Defs
Rat.eq_num_of_isInt : ∀ {q : ℚ}, q.isInt = true → q = ↑q.num
-- Mathlib.Analysis.Calculus.FDeriv.Add
DifferentiableOn.neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {s : Set E}, DifferentiableOn 𝕜 f s → DifferentiableOn 𝕜 (-f) s
-- Mathlib.Order.CompleteLattice.Defs
instCompleteSemilatticeInfOrderDualOfCompleteSemilatticeSup : {α : Type u_8} → [CompleteSemilatticeSup α] → CompleteSemilatticeInf αᵒᵈ
-- Init.Data.Option.Monadic
Option.forIn_eq_elim : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] (o : Option α)
  (f : α → β → m (ForInStep β)) (b : β), forIn o b f = o.elim (pure b) fun a => ForInStep.value <$> f a b
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.mem_primesOverFinset_iff : ∀ {A : Type u_4} [inst : CommRing A] {p : Ideal A},
  p ≠ ⊥ →
    ∀ [hpm : p.IsMaximal] (B : Type u_5) [inst_1 : CommRing B] [inst_2 : IsDedekindDomain B] [inst_3 : Algebra A B]
      [IsDomain A] [Module.IsTorsionFree A B] {P : Ideal B},
      P ∈ IsDedekindDomain.primesOverFinset p B ↔ P ∈ p.primesOver B
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.add_pos_left : ∀ {a₁ : ℕ} (a₂ : ℕ), 0 < a₁ → 0 < a₁ + a₂
-- Mathlib.Data.Stream.Init
Stream'.take.eq_def : ∀ {α : Type u} (x : ℕ) (x_1 : Stream' α),
  Stream'.take x x_1 =
    match x, x_1 with
    | 0, x => []
    | n.succ, s => s.head :: Stream'.take n s.tail
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Finset.truncatedInf_of_isAntichain : ∀ {α : Type u_1} [inst : SemilatticeInf α] {s : Finset α} {a : α} [inst_1 : DecidableLE α] [inst_2 : BoundedOrder α],
  IsAntichain (fun x1 x2 => x1 ≤ x2) ↑s → a ∈ s → s.truncatedInf a = a
-- Lean.Compiler.LCNF.Types
_private.Lean.Compiler.LCNF.Types.0.Lean.Compiler.LCNF.toLCNFType.visitForall : Lean.Expr → Array Lean.Expr → Lean.MetaM Lean.Expr
-- Lean.Parser.Term.Basic
/-- `sepBy1IndentSemicolon(p)` parses a (nonempty) sequence of `p` optionally followed by `;`,
similar to `many1Indent(p ";"?)`, except that if two occurrences of `p` occur on the same line,
the `;` is mandatory. This is used by tactic parsing, so that
```
example := by
  skip
  skip
```
is legal, but `by skip skip` is not - it must be written as `by skip; skip`.  -/
Lean.Parser.Tactic.sepBy1IndentSemicolon : Lean.Parser.Parser → Lean.Parser.Parser
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.instTrans : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → Trans Std.TreeMap.Raw.Equiv Std.TreeMap.Raw.Equiv Std.TreeMap.Raw.Equiv
-- Init.Data.List.Control
List.foldlM_nil : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] {f : β → α → m β} {b : β},
  List.foldlM f b [] = pure b
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthInf_congr : ∀ {R : Type u_1} [inst : ConditionallyCompleteLattice R] [inst_1 : Div R] [inst_2 : NatCast R] {u v : ℕ → R},
  u =ᶠ[Filter.atTop] v → LinearGrowth.linearGrowthInf u = LinearGrowth.linearGrowthInf v
-- Mathlib.Data.Set.Functor
/-- `Set.image2` in terms of monadic operations. Note that this can't be taken as the definition
because of the lack of universe polymorphism.  -/
Set.image2_def : ∀ {α β γ : Type u} (f : α → β → γ) (s : Set α) (t : Set β), Set.image2 f s t = f <$> s <*> t
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- The degree-sum formula for bipartite graphs, summing over the "left" part.

See `SimpleGraph.sum_degrees_eq_twice_card_edges` for the general version, and
`SimpleGraph.isBipartiteWith_sum_degrees_eq_card_edges'` for the version from the "right".  -/
SimpleGraph.isBipartiteWith_sum_degrees_eq_card_edges : ∀ {V : Type u_1} {G : SimpleGraph V} {s t : Finset V} [inst : Fintype V] [inst_1 : DecidableRel G.Adj],
  G.IsBipartiteWith ↑s ↑t → ∑ v ∈ s, G.degree v = G.edgeFinset.card
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.zero_seq : ∀ {α β : Type u} (x : FreeAbelianGroup α), 0 <*> x = 0
-- Mathlib.CategoryTheory.Preadditive.Comma
CategoryTheory.CommaMorphism.neg_right : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Preadditive A] {B : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} B] [inst_3 : CategoryTheory.Preadditive B] {T : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} T] [inst_5 : CategoryTheory.Preadditive T] (L : CategoryTheory.Functor A T)
  [inst_6 : L.Additive] (R : CategoryTheory.Functor B T) [inst_7 : R.Additive] {u v : CategoryTheory.Comma L R}
  (α : u ⟶ v), (-α).right = -α.right
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.pentagon_bimod : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C]
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [inst_4 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  {V W X Y Z : CategoryTheory.Mon C} (M : Bimod V W) (N : Bimod W X) (P : Bimod X Y) (Q : Bimod Y Z),
  CategoryTheory.CategoryStruct.comp (Bimod.whiskerRight (M.associatorBimod N P).hom Q)
      (CategoryTheory.CategoryStruct.comp (M.associatorBimod (N.tensorBimod P) Q).hom
        (M.whiskerLeft (N.associatorBimod P Q).hom)) =
    CategoryTheory.CategoryStruct.comp ((M.tensorBimod N).associatorBimod P Q).hom
      (M.associatorBimod N (P.tensorBimod Q)).hom
-- Mathlib.GroupTheory.Torsion
/-- The group exponent exists for any bounded torsion additive group.  -/
IsAddTorsion.exponentExists : ∀ {G : Type u_1} [inst : AddGroup G],
  IsAddTorsion G → (Set.range fun g => addOrderOf g).Finite → AddMonoid.ExponentExists G
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc
MeasureTheory.StronglyMeasurable.sinc : ∀ {α : Type u_1} {x : MeasurableSpace α} {f : α → ℝ},
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun x => Real.sinc (f x)
-- Mathlib.Algebra.Category.Grp.Basic
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
AddCommGrpCat.Hom.Simps.hom : (X Y : AddCommGrpCat) → X.Hom Y → ↑X →+ ↑Y
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_cpow : ∀ {a b : ℝ} {r : ℂ},
  -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ Set.uIcc a b → ∫ (x : ℝ) in a..b, ↑x ^ r = (↑b ^ (r + 1) - ↑a ^ (r + 1)) / (r + 1)
-- Mathlib.Topology.Homotopy.Equiv
ContinuousMap.HomotopyEquiv.ext : ∀ {X : Type u} {Y : Type v} {inst : TopologicalSpace X} {inst_1 : TopologicalSpace Y}
  {x y : ContinuousMap.HomotopyEquiv X Y}, x.toFun = y.toFun → x.invFun = y.invFun → x = y
-- Init.Data.List.MapIdx
List.length_mapIdx : ∀ {α : Type u_1} {α_1 : Type u_2} {f : ℕ → α → α_1} {l : List α}, (List.mapIdx f l).length = l.length
-- Mathlib.Tactic.LinearCombinationPrime
/-- The `(exp := n)` syntax for `linear_combination'` says to take the goal to the `n`th power before
subtracting the given combination of hypotheses.
 -/
Mathlib.Tactic.LinearCombinationPrime.expStx : Lean.ParserDescr
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.algebraMap_eq : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : CommRing R] (r : R),
  (algebraMap R (QuaternionAlgebra R c₁ c₂ c₃)) r = { re := r, imI := 0, imJ := 0, imK := 0 }
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.coe_singletonAddMonoidHom : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddZeroClass α], ⇑Finset.singletonAddMonoidHom = singleton
-- Mathlib.RingTheory.Finiteness.Ideal
Submodule.FG.smul : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {I : Ideal R}
  [I.IsTwoSided] {N : Submodule R M}, I.FG → N.FG → (I • N).FG
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.homologyMap_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K L : HomologicalComplex C c) (i : ι) [inst_2 : K.HasHomology i]
  [inst_3 : L.HasHomology i], HomologicalComplex.homologyMap 0 i = 0
-- Init.Notation
/-- The implementation of `~~~a : α`. 

Conventions for notations in identifiers:

 * The recommended spelling of `~~~` in identifiers is `not`. -/
«term~~~_» : Lean.ParserDescr
-- Mathlib.Data.Set.Prod
Set.univ_pi_update_univ : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] (i : ι) (s : Set (α i)),
  Set.univ.pi (Function.update (fun j => Set.univ) i s) = Function.eval i ⁻¹' s
-- Mathlib.Order.PFilter
/-- Two filters are equal when their underlying sets are equal.  -/
Order.PFilter.ext : ∀ {P : Type u_1} [inst : Preorder P] (s t : Order.PFilter P), ↑s = ↑t → s = t
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKeyD_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = false → ∀ {fallback : α}, t.minKeyD fallback ∈ t
-- Plausible.Sampleable
Plausible.NoShrink.repr : {α : Type u_1} → [inst : Repr α] → Repr (Plausible.NoShrink α)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_
CategoryTheory.CommGrpObj.toGrpObj : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {inst_1 : CategoryTheory.CartesianMonoidalCategory C} →
      {inst_2 : CategoryTheory.BraidedCategory C} →
        {X : C} → [self : CategoryTheory.CommGrpObj X] → CategoryTheory.GrpObj X
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.instInhabitedUsedSimps : Inhabited Lean.Meta.Simp.UsedSimps
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.divCoeffs.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Cutsat.EqCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.divCoeffs c) = 1 + sizeOf c
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValInt_dvd_iff : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) (a : ℤ), ↑p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValInt p a
-- Std.Sync.RecursiveMutex
Std.instNonemptyRecursiveMutex : ∀ {α : Type} [Nonempty α], Nonempty (Std.RecursiveMutex α)
-- Init.Data.String.Termination
/-- The number of bytes between `p` and the end position. This number decreases as `p` advances.  -/
String.Slice.Pos.remainingBytes : {s : String.Slice} → s.Pos → ℕ
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- Given a bijection, there is an embedding from the comapped graph into the original
graph.  -/
SimpleGraph.Iso.comap : {V : Type u_1} → {W : Type u_2} → (f : V ≃ W) → (G : SimpleGraph W) → SimpleGraph.comap (⇑f) G ≃g G
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.insertMany_emptyWithCapacity_list_singleton : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {k : α} {v : β k},
  ↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany [⟨k, v⟩]) =
    Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insert k v
-- Mathlib.Data.Seq.Computation
Computation.has_bind_eq_bind : ∀ {α β : Type u} (c : Computation α) (f : α → Computation β), c >>= f = c.bind f
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.reorder : Lean.Meta.Grind.Arith.Cutsat.EqCnstr → Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
MultipliableLocallyUniformlyOn.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] (f : ι → β → α) (s : Set β)
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β],
  MultipliableLocallyUniformlyOn f s = ∃ g, HasProdLocallyUniformlyOn f g s
-- Mathlib.CategoryTheory.Presentable.SharplyLT.Basic
_private.Mathlib.CategoryTheory.Presentable.SharplyLT.Basic.0.Cardinal.SharplyLT.existsIsCardinalFilteredSetOfExistsCofinal.isCardinalFiltered_iUnion : ∀ {κ₁ κ₂ : Cardinal.{w}} [inst : Fact κ₁.IsRegular] [Fact κ₂.IsRegular],
  κ₁ < κ₂ →
    ∀ {X : Type w} [inst_2 : PartialOrder X]
      (Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (CategoryTheory.CardinalDirectedPoset.SetCardinalLT κ₁ ↑B)),
      (∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), HasCardinalLT (↑(Y B hB)) κ₂) →
        (∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), IsCofinal (Y B hB)) →
          ∀
            (m :
              (B : Set X) →
                (hB : HasCardinalLT (↑B) κ₂) →
                  (C : CategoryTheory.CardinalDirectedPoset.SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X),
            (∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂) (C : CategoryTheory.CardinalDirectedPoset.SetCardinalLT κ₁ ↑B)
                (hC : C ∈ Y B hB), ∀ b ∈ ↑C, ↑b ≤ m B hB C hC) →
              ∀ (A : Set X),
                HasCardinalLT (↑A) κ₂ →
                  CategoryTheory.IsCardinalFiltered
                    (↑(⋃ j,
                        transfiniteIterate (Cardinal.SharplyLT.existsIsCardinalFilteredSetOfExistsCofinal.φ✝ Y m) j A))
                    κ₁
-- Lean.Server.Requests
Lean.Server.RequestError.code : Lean.Server.RequestError → Lean.JsonRpc.ErrorCode
-- Mathlib.Tactic.Positivity.Core
Mathlib.Meta.Positivity.PositivityExt.mk : ({u : Lean.Level} →
    {α : Q(Type u)} →
      (zα : Q(Zero «$α»)) →
        (pα? : Option Q(PartialOrder «$α»)) →
          (e : Q(«$α»)) → Lean.MetaM (Mathlib.Meta.Positivity.Strictness zα e pα?)) →
  Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
/-- The type of objects in a `BasedCategory`  -/
CategoryTheory.BasedCategory.obj : {𝒮 : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] → CategoryTheory.BasedCategory 𝒮 → Type u₂
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.instCategory : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {B : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
        {T : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} T] →
            (L : CategoryTheory.Functor A T) →
              (R : CategoryTheory.Functor B T) →
                (P : CategoryTheory.MorphismProperty T) →
                  (Q : CategoryTheory.MorphismProperty A) →
                    (W : CategoryTheory.MorphismProperty B) →
                      [Q.IsMultiplicative] →
                        [W.IsMultiplicative] →
                          CategoryTheory.Category.{max v_1 v_2, max (max v_3 u_2) u_1}
                            (CategoryTheory.MorphismProperty.Comma L R P Q W)
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.removeUnusedVars : Array Lean.Expr →
  Array Lean.Elab.DefViewElabHeader →
    Array Lean.Expr →
      List Lean.Elab.Term.LetRecToLift → Lean.Elab.TermElabM (Lean.LocalContext × Lean.LocalInstances × Array Lean.Expr)
-- Mathlib.Computability.PartrecBasis
Nat.Partrec'.part_iff₁ : ∀ {f : ℕ →. ℕ}, (Nat.Partrec' fun v => f v.head) ↔ Partrec f
-- Init.Data.Option.Lemmas
_private.Init.Data.Option.Lemmas.0.Option.pfilter.match_1.splitter : {α : Type u_1} →
  (motive : (o : Option α) → ((a : α) → o = some a → Bool) → Sort u_2) →
    (o : Option α) →
      (p : (a : α) → o = some a → Bool) →
        ((p : (a : α) → none = some a → Bool) → motive none p) →
          ((a : α) → (p : (a_1 : α) → some a = some a_1 → Bool) → motive (some a) p) → motive o p
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.coeffAddEquiv_symm_apply : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] (coeff : G →₀ k),
  SkewMonoidAlgebra.coeffAddEquiv.symm coeff = { coeff := coeff }
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.gaussianPDFReal_sub : ∀ {μ : ℝ} {v : NNReal} (x y : ℝ),
  ProbabilityTheory.gaussianPDFReal μ v (x - y) = ProbabilityTheory.gaussianPDFReal (μ + y) v x
-- Init.Prelude
/-- Replaces the state with the result of applying `f` to it. Returns the old value of the state.

It is equivalent to `get <* modify f` but may be more efficient.
 -/
getModify : {σ : Type u} → {m : Type u → Type v} → [MonadState σ m] → (σ → σ) → m σ
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.instMonoidalForget.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.Mon.instMonoidalForget C =
    { εIso := CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategoryStruct.tensorUnit C),
        μIso := fun x x_1 =>
          CategoryTheory.Iso.refl
            (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.Mon.forget C).obj x)
              ((CategoryTheory.Mon.forget C).obj x_1)),
        μIso_hom_natural_left := ⋯, μIso_hom_natural_right := ⋯, associativity := ⋯, left_unitality := ⋯,
        right_unitality := ⋯ }.toMonoidal
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.instOne.eq_1 : ∀ {α : Type u}, WithOne.instOne = { one := none }
-- Std.Time.Zoned.ZoneRules
/-- Represents the type of local time in relation to UTC.
 -/
Std.Time.TimeZone.UTLocal : Type
-- Aesop.Util.OrderedHashSet
Aesop.OrderedHashSet.toHashSet : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → Aesop.OrderedHashSet α → Std.HashSet α
-- Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
GaussianFourier.integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace : ∀ {b : ℂ} {ι : Type u_2} [inst : Fintype ι],
  0 < b.re →
    ∀ (c : ℂ) (w : EuclideanSpace ℝ ι),
      MeasureTheory.Integrable (fun v => Complex.exp (-b * ↑‖v‖ ^ 2 + c * ↑(inner ℝ w v))) MeasureTheory.volume
-- Init.Grind.Ordered.Field
Lean.Grind.Field.IsOrdered.mul_lt_mul_iff_of_pos_right : ∀ {R : Type u} [inst : Lean.Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] {a b c : R}, 0 < c → (a * c < b * c ↔ a < b)
-- Mathlib.RingTheory.Smooth.AdicCompletion
_private.Mathlib.RingTheory.Smooth.AdicCompletion.0.Algebra.FormallySmooth.liftAdicCompletionAux.eq_1 : ∀ {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],
  Algebra.FormallySmooth.liftAdicCompletionAux✝ I f 0 = default
-- Mathlib.NumberTheory.Bernoulli
_private.Mathlib.NumberTheory.Bernoulli.0.Bernoulli.vonStaudtPrimes : ℕ → Finset ℕ
-- Lean.Elab.Binders
Lean.Elab.Term.expandLetEqnsDecl : Lean.Syntax → optParam Bool true → Lean.MacroM Lean.Syntax
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.add_assoc : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (a b c : Lean.Grind.Ring.OfSemiring.Q α),
  Lean.Grind.Ring.OfSemiring.add (Lean.Grind.Ring.OfSemiring.add a b) c =
    Lean.Grind.Ring.OfSemiring.add a (Lean.Grind.Ring.OfSemiring.add b c)
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.FinalizeContext.params : Lean.Elab.Command.FinalizeContext✝ → Array Lean.Expr
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_algebraMap : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (r : R) (f : R → R),
  cfc f ((algebraMap R A) r) = (algebraMap R A) (f r)
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeGroupBasis.reindex.eq_1 : ∀ {ι : Type u_1} {ι' : Type u_2} {G : Type u_3} [inst : Group G] (b : FreeGroupBasis ι G) (e : ι ≃ ι'),
  b.reindex e = { repr := b.repr.trans (FreeGroup.freeGroupCongr e) }
-- Mathlib.Order.Filter.IndicatorFunction
Monotone.tendsto_indicator : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_5} [inst : Preorder ι] [inst_1 : Zero β] (s : ι → Set α),
  Monotone s →
    ∀ (f : α → β) (a : α), Filter.Tendsto (fun i => (s i).indicator f a) Filter.atTop (pure ((⋃ i, s i).indicator f a))
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.reflexiveCoforkEquivCofork_inverse_obj_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C)
  (X :
    CategoryTheory.Limits.Cofork (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left)
      (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right)),
  ((CategoryTheory.Limits.reflexiveCoforkEquivCofork F).inverse.obj X).pt = X.pt
-- Mathlib.Algebra.Order.Antidiag.Prod
/-- The disjoint union of mulAntidiagonals `Σ (n : A), mulAntidiagonal n` is equivalent to the
product `A × A`. This is such an equivalence, obtained by mapping `(n, (k, l))` to `(k, l)`.  -/
Finset.HasMulAntidiagonal.sigmaMulAntidiagonalEquivProd : {A : Type u_1} →
  [inst : Monoid A] →
    [inst_1 : Finset.HasMulAntidiagonal A] → (n : A) × ↥(Finset.HasMulAntidiagonal.mulAntidiagonal n) ≃ A × A
-- Mathlib.Algebra.Quaternion
Quaternion.im_sq : ∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R), a.im ^ 2 = -↑(Quaternion.normSq a.im)
-- Mathlib.Logic.Equiv.Basic
/-- Extend the domain of `e : Equiv.Perm α` to one that is over `β` via `f : α → Subtype p`,
where `p : β → Prop`, permuting only the `b : β` that satisfy `p b`.
This can be used to extend the domain across a function `f : α → β`,
keeping everything outside of `Set.range f` fixed. For this use-case `Equiv` given by `f` can
be constructed by `Equiv.of_leftInverse'` or `Equiv.of_leftInverse` when there is a known
inverse, or `Equiv.ofInjective` in the general case.
 -/
Equiv.Perm.extendDomain : {α' : Type u_9} →
  {β' : Type u_10} → Equiv.Perm α' → {p : β' → Prop} → [DecidablePred p] → α' ≃ Subtype p → Equiv.Perm β'