mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
/-- Given
```
X₁ - f₁ -> X₂ - f₂ -> X₃
|          |          |
i₁         i₂         i₃
↓          ↓          ↓
Y₁ - g₁ -> Y₂ - g₂ -> Y₃
```
Then the big square is a pullback if both the small squares are.
 -/
CategoryTheory.Limits.pasteHorizIsPullback : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₃ Y₁ Y₂ Y₃ : C} →
      {g₁ : Y₁ ⟶ Y₂} →
        {g₂ : Y₂ ⟶ Y₃} →
          {i₃ : X₃ ⟶ Y₃} →
            {t₂ : CategoryTheory.Limits.PullbackCone g₂ i₃} →
              {i₂ : t₂.pt ⟶ Y₂} →
                {t₁ : CategoryTheory.Limits.PullbackCone g₁ i₂} →
                  (hi₂ : i₂ = t₂.fst) →
                    CategoryTheory.Limits.IsLimit t₂ →
                      CategoryTheory.Limits.IsLimit t₁ → CategoryTheory.Limits.IsLimit (t₂.pasteHoriz t₁ hi₂)
-- Mathlib.Data.Seq.Computation
_private.Mathlib.Data.Seq.Computation.0.Computation.Corec.f.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : α ⊕ β → Sort u_3) (a : α) (h_1 : (a : α) → motive (Sum.inl a))
  (h_2 : (val : β) → motive (Sum.inr val)),
  (match Sum.inl a with
    | Sum.inl a => h_1 a
    | Sum.inr val => h_2 val) =
    h_1 a
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MCasesPat.clear : Lean.Parser.Tactic.MCasesPat
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.isSubordinate_biUnionTagged : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {r : (ι → ℝ) → ↑(Set.Ioi 0)} [inst : Fintype ι]
  {π : BoxIntegral.Prepartition I} {πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J},
  (π.biUnionTagged πi).IsSubordinate r ↔ ∀ J ∈ π, (πi J).IsSubordinate r
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.card_lt_ofNat : ∀ {o : Ordinal.{u_1}} {n : ℕ} [inst : n.AtLeastTwo], o.card < OfNat.ofNat n ↔ o < OfNat.ofNat n
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.ModuleHierarchy.mk.inj : ∀ {item : Lean.Lsp.LeanImport} {children : Array Lean.Lsp.Ipc.ModuleHierarchy} {item_1 : Lean.Lsp.LeanImport}
  {children_1 : Array Lean.Lsp.Ipc.ModuleHierarchy},
  { item := item, children := children } = { item := item_1, children := children_1 } →
    item = item_1 ∧ children = children_1
-- Init.Data.Iterators.Lemmas.Combinators.Take
Std.Iter.step_take : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {n : ℕ} {it : Std.Iter β},
  (Std.Iter.take n it).step =
    match n with
    | 0 => Std.PlausibleIterStep.done ⋯
    | k.succ =>
      match it.step with
      | ⟨Std.IterStep.yield it' out, h⟩ => Std.PlausibleIterStep.yield (Std.Iter.take k it') out ⋯
      | ⟨Std.IterStep.skip it', h⟩ => Std.PlausibleIterStep.skip (Std.Iter.take (k + 1) it') ⋯
      | ⟨Std.IterStep.done, h⟩ => Std.PlausibleIterStep.done ⋯
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.CustomEliminator.elimName : Lean.Meta.CustomEliminator → Lean.Name
-- Mathlib.Order.Antisymmetrization
AntisymmRel.antisymmRel_congr_right : ∀ {α : Type u_1} {a b c : α} [inst : Preorder α],
  AntisymmRel (fun x1 x2 => x1 ≤ x2) b c →
    (AntisymmRel (fun x1 x2 => x1 ≤ x2) a b ↔ AntisymmRel (fun x1 x2 => x1 ≤ x2) a c)
-- Aesop.Script.StructureDynamic
_private.Aesop.Script.StructureDynamic.0.Aesop.Script.structureDynamicCore.go : Lean.MVarId →
  Lean.Meta.SavedState → Array Lean.MVarId → Aesop.Script.DynStructureM (Option Aesop.Script.DynStructureResult)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.HasLeftHomology.of_hasKernel_of_hasCokernel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} [inst_2 : CategoryTheory.Limits.HasKernel S.g]
  [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.lift S.g S.f ⋯)], S.HasLeftHomology
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
/-- The bijection between the intermediate fields of `ℚ(ζₙ)/ℚ` and the subgroups of the group
of Dirichlet characters of level `n`.
 -/
IsCyclotomicExtension.Rat.intermediateFieldEquivSubgroupChar : (n : ℕ) →
  [NeZero n] →
    (K : Type u_1) →
      [inst : Field K] →
        [inst_1 : NumberField K] →
          [hK : IsCyclotomicExtension {n} ℚ K] →
            (R : Type u_2) →
              [inst_2 : CommRing R] →
                [HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)] →
                  [IsAbelianGalois ℚ K] → IntermediateField ℚ K ≃o Subgroup (DirichletCharacter R n)
-- Init.Data.List.Perm
/-- A list with no duplicates that is a subset of another list is no longer than
that list.  -/
List.Nodup.length_le_of_subset : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Nodup → l₁ ⊆ l₂ → l₁.length ≤ l₂.length
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
exists_dist_le_lt : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] {x z : E} {δ ε : ℝ},
  0 ≤ δ → 0 < ε → dist x z < ε + δ → ∃ y, dist x y ≤ δ ∧ dist y z < ε
-- Std.Do.SPred.Laws
Std.Do.SPred.bientails.eq_2 : ∀ (σ : Type u) (tail : List (Type u)) (P_2 Q_2 : Std.Do.SPred (σ :: tail)), (P_2 ⊣⊢ₛ Q_2) = ∀ (s : σ), P_2 s ⊣⊢ₛ Q_2 s
-- Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
instMonoidalTopCatSSetToSSet : TopCat.toSSet.Monoidal
-- Mathlib.Analysis.Convex.Segment
mem_segment_iff_sameRay : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {x y z : E}, x ∈ segment 𝕜 y z ↔ SameRay 𝕜 (x - y) (z - x)
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.sub' : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f g : α → β},
  MeasureTheory.Integrable f μ → MeasureTheory.Integrable g μ → MeasureTheory.Integrable (fun a => f a - g a) μ
-- Batteries.Data.List.Basic
List.swapAt_eq_swapAtTR : @List.swapAt = @List.swapAtTR
-- Mathlib.RingTheory.Ideal.Defs
Ideal.neg_mem_iff : ∀ {α : Type u} [inst : Ring α] (I : Ideal α) {a : α}, -a ∈ I ↔ a ∈ I
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.affineLocally_iff_forall_isAffineOpen : ∀ (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) {X Y : AlgebraicGeometry.Scheme}
  (f : X ⟶ Y),
  AlgebraicGeometry.affineLocally (fun {R S} [CommRing R] [CommRing S] => P) f ↔
    ∀ {U : Y.Opens},
      AlgebraicGeometry.IsAffineOpen U →
        ∀ {V : X.Opens},
          AlgebraicGeometry.IsAffineOpen V →
            ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
              P (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e))
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperation.cons_tail : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  {op :
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl →
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl}
  {exp : ℝ} {coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl},
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperation op →
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperation fun ms =>
      (op (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef ms)).tail
-- Init.Data.Nat.ToString
Nat.length_repr_pos : ∀ {n : ℕ}, 0 < n.repr.length
-- Lean.Elab.Term.TermElabM
/-- Collect unassigned metavariables in `type` that are not already in `init` and not satisfying `except`.
 -/
Lean.Elab.Term.collectUnassignedMVars : Lean.Expr →
  optParam (Array Lean.Expr) #[] →
    (optParam (Lean.MVarId → Bool) fun x => false) → Lean.Elab.TermElabM (Array Lean.Expr)
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheorems.mk.injEq : ∀ (pre post : Lean.Meta.SimpTheoremTree) (lemmaNames : Lean.PHashSet Lean.Meta.Origin)
  (toUnfold : Lean.PHashSet Lean.Name) (erased : Lean.PHashSet Lean.Meta.Origin)
  (toUnfoldThms : Lean.PHashMap Lean.Name (Array Lean.Name)) (pre_1 post_1 : Lean.Meta.SimpTheoremTree)
  (lemmaNames_1 : Lean.PHashSet Lean.Meta.Origin) (toUnfold_1 : Lean.PHashSet Lean.Name)
  (erased_1 : Lean.PHashSet Lean.Meta.Origin) (toUnfoldThms_1 : Lean.PHashMap Lean.Name (Array Lean.Name)),
  ({ pre := pre, post := post, lemmaNames := lemmaNames, toUnfold := toUnfold, erased := erased,
        toUnfoldThms := toUnfoldThms } =
      { pre := pre_1, post := post_1, lemmaNames := lemmaNames_1, toUnfold := toUnfold_1, erased := erased_1,
        toUnfoldThms := toUnfoldThms_1 }) =
    (pre = pre_1 ∧
      post = post_1 ∧
        lemmaNames = lemmaNames_1 ∧ toUnfold = toUnfold_1 ∧ erased = erased_1 ∧ toUnfoldThms = toUnfoldThms_1)
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
MvQPF.Fix.rec_unique : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : F (α ::: β) → β)
  (h : MvQPF.Fix F α → β),
  (∀ (x : F (α ::: MvQPF.Fix F α)), h (MvQPF.Fix.mk x) = g (MvFunctor.map (TypeVec.id ::: h) x)) → MvQPF.Fix.rec g = h
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.maxView.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (l : Std.DTreeMap.Internal.Impl α β)
  (motive :
    (r : Std.DTreeMap.Internal.Impl α β) →
      r.Balanced → Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size → Sort u_3)
  (size : ℕ) (k' : α) (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β)
  (hr : (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').Balanced)
  (hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').size)
  (h_1 :
    (hr : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
      (hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size Std.DTreeMap.Internal.Impl.leaf.size) →
        motive Std.DTreeMap.Internal.Impl.leaf hr hlr)
  (h_2 :
    (size : ℕ) →
      (k' : α) →
        (v' : β k') →
          (l' r' : Std.DTreeMap.Internal.Impl α β) →
            (hr : (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').Balanced) →
              (hlr :
                  Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size
                    (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').size) →
                motive (Std.DTreeMap.Internal.Impl.inner size k' v' l' r') hr hlr),
  (match Std.DTreeMap.Internal.Impl.inner size k' v' l' r', hr, hlr with
    | Std.DTreeMap.Internal.Impl.leaf, hr, hlr => h_1 hr hlr
    | Std.DTreeMap.Internal.Impl.inner size k' v' l' r', hr, hlr => h_2 size k' v' l' r' hr hlr) =
    h_2 size k' v' l' r' hr hlr
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
/-- For a Lie group `G` and open sets `U ⊆ V` in `N`, the 'restriction' group homomorphism from
`C^n⟮I, V; I', G⟯` to `C^n⟮I, U; I', G⟯`.  -/
ContMDiffMap.restrictMonoidHom : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    (I : ModelWithCorners 𝕜 E H) →
                      {H' : Type u_5} →
                        [inst_6 : TopologicalSpace H'] →
                          (I' : ModelWithCorners 𝕜 E' H') →
                            {N : Type u_6} →
                              [inst_7 : TopologicalSpace N] →
                                [inst_8 : ChartedSpace H N] →
                                  {n : WithTop ℕ∞} →
                                    (G : Type u_10) →
                                      [inst_9 : Monoid G] →
                                        [inst_10 : TopologicalSpace G] →
                                          [inst_11 : ChartedSpace H' G] →
                                            [inst_12 : ContMDiffMul I' n G] →
                                              {U V : TopologicalSpace.Opens N} →
                                                U ≤ V → ContMDiffMap I I' (↥V) G n →* ContMDiffMap I I' (↥U) G n
-- Init.Data.Iterators.Lemmas.Consumers.Access
_private.Init.Data.Iterators.Lemmas.Consumers.Access.0.Std.Iter.atIdxSlow?_eq_match.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 ()
-- Init.Data.Rat.Lemmas
Rat.lt_sub_right_iff_add_lt : ∀ {a b c : ℚ}, a < c - b ↔ a + b < c
-- Mathlib.CategoryTheory.ConcreteCategory.EpiMono
/-- In any concrete category, surjective morphisms are epimorphisms.  -/
CategoryTheory.ConcreteCategory.epi_of_surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y : C}
  (f : X ⟶ Y), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f) → CategoryTheory.Epi f
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.pow_card : ∀ {K : Type u_1} [inst : GroupWithZero K] [inst_1 : Fintype K] (a : K), a ^ Fintype.card K = a
-- Init.Data.Int.Linear
Int.Internal.Linear.dvd_elim_cert.eq_1 : ∀ (k₁ : ℤ) (p₁ : Int.Internal.Linear.Poly) (k₂ : ℤ) (p₂ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.dvd_elim_cert k₁ p₁ k₂ p₂ =
    Int.Internal.Linear.Poly.rec (fun x => false) (fun a x p x_1 => (k₂.beq' ↑(k₁.gcd a)).and' (p₂.beq' p)) p₁
-- Mathlib.Topology.Homotopy.HSpaces
/-- The loop space at x carries a structure of an H-space. Note that the field `eHmul`
(resp. `hmulE`) neither implies nor is implied by `Path.Homotopy.reflTrans`
(resp. `Path.Homotopy.transRefl`).
 -/
Path.instHSpace : {X : Type u} → [inst : TopologicalSpace X] → (x : X) → HSpace (Path x x)
-- Mathlib.Analysis.Calculus.Deriv.Abs
ContDiffAt.abs : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {n : ℕ∞} {f : E → ℝ} {x : E},
  ContDiffAt ℝ (↑n) f x → f x ≠ 0 → ContDiffAt ℝ (↑n) (fun x => |f x|) x
-- Mathlib.Data.Multiset.Filter
Multiset.filter_sub : ∀ {α : Type u_1} [inst : DecidableEq α] (p : α → Prop) [inst_1 : DecidablePred p] (s t : Multiset α),
  Multiset.filter p (s - t) = Multiset.filter p s - Multiset.filter p t
-- Mathlib.Logic.Encodable.Basic
Encodable.decode_unit_succ : ∀ (n : ℕ), Encodable.decode n.succ = none
-- Mathlib.Dynamics.OmegaLimit
omegaLimit_inter : ∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β)
  (s₁ s₂ : Set α), omegaLimit f ϕ (s₁ ∩ s₂) ⊆ omegaLimit f ϕ s₁ ∩ omegaLimit f ϕ s₂
-- Init.System.ST
instMonadFinallyEST : {ε σ : Type} → MonadFinally (EST ε σ)
-- Mathlib.Algebra.Group.Pi.Units
/-- The additive-monoid equivalence between (additive) units of a product,
and the product of the (additive) units of each monoid.  -/
AddEquiv.piAddUnits : {ι : Type u_1} →
  {M : ι → Type u_2} → [inst : (i : ι) → AddMonoid (M i)] → AddUnits ((i : ι) → M i) ≃+ ((i : ι) → AddUnits (M i))
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.MulStruct.δ_map_of_lt : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g fg : X.PtSimplex n x} {i : Fin n}
  (self : f.MulStruct g fg i),
  ∀ j < i.castSucc.castSucc, CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) self.map = SSet.const x
-- Mathlib.RingTheory.Valuation.Extension
Valuation.HasExtension.instIsLocalHomSubtypeMemValuationSubringValuationSubringRingHomAlgebraMap : ∀ {K : outParam (Type u_5)} {L : outParam (Type u_6)} {Γ₀ : outParam (Type u_7)} {Γ₁ : outParam (Type u_8)}
  [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [inst_3 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_4 : LinearOrderedCommGroupWithZero Γ₁] (vK : Valuation K Γ₀) (vL : Valuation L Γ₁)
  [inst_5 : vK.HasExtension vL], IsLocalHom (algebraMap ↥vK.valuationSubring ↥vL.valuationSubring)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.map₂Congr_inv_app_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B}
  {R' : CategoryTheory.Functor A B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : L' ⟶ G.obj L)
  (β : R.comp G ⟶ F.comp R') {F' : CategoryTheory.Functor C A} {G' : CategoryTheory.Functor D B} (e₁ : F ≅ F')
  (e₂ : G ≅ G') (α' : L' ⟶ G'.obj L) (β' : R.comp G' ⟶ F'.comp R')
  (hα :
    autoParam (α = CategoryTheory.CategoryStruct.comp α' (e₂.inv.app L))
      CategoryTheory.StructuredArrow.map₂Congr._auto_1)
  (hβ :
    autoParam
      (CategoryTheory.CategoryStruct.comp β (CategoryTheory.Functor.whiskerRight e₁.hom R') =
        CategoryTheory.CategoryStruct.comp (R.whiskerLeft e₂.hom) β')
      CategoryTheory.StructuredArrow.map₂Congr._auto_3)
  (X : CategoryTheory.StructuredArrow L R),
  ((CategoryTheory.StructuredArrow.map₂Congr α β e₁ e₂ α' β' hα hβ).inv.app X).right = e₁.inv.app X.right
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.cos_int_mul_two_pi : ∀ (n : ℤ), Complex.cos (↑n * (2 * ↑Real.pi)) = 1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.iteratedDeriv_odd_sinh : ∀ (n : ℕ), iteratedDeriv (2 * n + 1) Real.sinh = Real.cosh
-- Mathlib.Order.Category.NonemptyFinLinOrd
/-- The forgetful functor `NonemptyFinLinOrd ⥤ FinPartOrd` and `OrderDual` commute.  -/
nonemptyFinLinOrdDualCompForgetToFinPartOrd : NonemptyFinLinOrd.dual.comp (CategoryTheory.forget₂ NonemptyFinLinOrd FinPartOrd) ≅
  (CategoryTheory.forget₂ NonemptyFinLinOrd FinPartOrd).comp FinPartOrd.dual
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_6 : HAdd Std.Time.Millisecond.Offset Std.Time.Nanosecond.Offset Std.Time.Nanosecond.Offset
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.appIso_inv_app_apply : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : X.Opens)
  (x : ↑(X.presheaf.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom
        (AlgebraicGeometry.Scheme.Hom.app f ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U)))
      ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appIso f U).inv) x) =
    (CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.eqToHom ⋯).op)) x
-- Mathlib.Data.NNRat.Defs
Rat.lt_toNNRat_iff_coe_lt : ∀ {p : ℚ} {q : ℚ≥0}, q < p.toNNRat ↔ ↑q < p
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
summable_eisSummand : ∀ {k : ℕ}, 3 ≤ k → ∀ (z : UpperHalfPlane), Summable fun x => EisensteinSeries.eisSummand (↑k) x z
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.mapWithPostcondition.eq_1 : ∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad n] [inst_1 : MonadLiftT m n]
  [inst_2 : Std.Iterator α m β] (f : β → Std.Iterators.PostconditionT n γ) (it : Std.IterM m β),
  Std.IterM.mapWithPostcondition f it = Std.IterM.InternalCombinators.map (fun {x} => monadLift) f it
-- Mathlib.Order.Shrink
equivShrink_symm_bot : ∀ {α : Type u_1} [inst : Small.{u, u_1} α] [inst_1 : Bot α], (equivShrink α).symm ⊥ = ⊥
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.encodePi.match_5.splitter : (motive : (n : ℕ) → (f : Fin n → ℕ) → ((i : Fin n) → Fin (f i)) → Sort u_1) →
  (n : ℕ) →
    (f : Fin n → ℕ) →
      (x : (i : Fin n) → Fin (f i)) →
        ((x : Fin 0 → ℕ) → (x_1 : (i : Fin 0) → Fin (x i)) → motive 0 x x_1) →
          ((n : ℕ) → (f : Fin (n + 1) → ℕ) → (x : (i : Fin (n + 1)) → Fin (f i)) → motive n.succ f x) → motive n f x
-- Mathlib.RepresentationTheory.Coinduced
Rep.coindFunctorIso_hom_app_hom_toFun_hom_toFun : ∀ {k : Type u} {G : Type v} {H : Type w} [inst : CommRing k] [inst_1 : Monoid G] [inst_2 : Monoid H] (φ : G →* H)
  (X : Rep.{max u w, u, v} k G) (f : ↥(Representation.coindV φ X.ρ)) (x : ↑(Rep.leftRegular k H)),
  (Rep.Hom.hom ((Rep.Hom.hom ((Rep.coindFunctorIso φ).hom.app X)) f)) x = (Finsupp.linearCombination k ↑f) x.coeff
-- Mathlib.Tactic.GrindAttrs
/-- `closedness` is a simple tactic that tries various lemmas to prove that a set is closed,
and reasoning about the closure of sets.
It is implemented using `grind`, and has the same configuration options as `grind`.

It also exists as a grind attribute, and can be combined with other grind attributes using
`grind only [closedness, ...]`.
 -/
tacticClosedness?_ : Lean.ParserDescr
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.ae_measure_lt_top : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {s : Set (α × β)},
  MeasurableSet s → (μ.prod ν) s ≠ ⊤ → ∀ᵐ (x : α) ∂μ, ν (Prod.mk x ⁻¹' s) < ⊤
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.isPeriodicPt_prodMap : ∀ {α : Type u_1} {β : Type u_2} {f : α → α} {g : β → β} {n : ℕ} (x : α × β),
  Function.IsPeriodicPt (Prod.map f g) n x ↔ Function.IsPeriodicPt f n x.1 ∧ Function.IsPeriodicPt g n x.2
-- Mathlib.RingTheory.Trace.Defs
Algebra.traceForm_apply : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (x y : S),
  ((Algebra.traceForm R S) x) y = (Algebra.trace R S) (x * y)
-- Lean.Server.Utils
/-- Finds the module name corresponding to `uri` in `srcSearchPath`.  -/
Lean.Server.moduleFromDocumentUri : Lean.Lsp.DocumentUri → IO Lean.Name
-- Mathlib.Probability.Process.Adapted
MeasureTheory.Adapted.measurable_le : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : ι → Type u_3} [inst_1 : (i : ι) → MeasurableSpace (β i)] {u : (i : ι) → Ω → β i} {i j : ι},
  MeasureTheory.Adapted f u → i ≤ j → Measurable (u i)
-- Mathlib.Topology.Sheaves.Limits
TopCat.instCreatesLimitsSheafPresheafForgetOfHasLimits : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasLimits C] → (X : TopCat) → CategoryTheory.CreatesLimits (TopCat.Sheaf.forget C X)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray_fold_fn.match_1.splitter : {n : ℕ} →
  (motive : Option (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) → Sort u_1) →
    (x : Option (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) →
      (Unit → motive none) →
        ((l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → motive (some (l, true))) →
          ((l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → motive (some (l, false))) → motive x
-- Mathlib.Topology.Covering.Basic
IsOpen.trivializationDiscrete_baseSet : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X}
  [inst_2 : Nonempty (X → E)] {ι : Type u_3} [inst_3 : Nonempty ι] [inst_4 : TopologicalSpace ι]
  [inst_5 : DiscreteTopology ι] (U : ι → Set E) (V : Set X) (open_V : IsOpen V)
  (open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen W ↔ IsOpen (f ⁻¹' W ∩ U i))) (inj : ∀ (i : ι), Set.InjOn f (U i))
  (surj : ∀ (i : ι), Set.SurjOn f (U i) V) (disjoint : Pairwise (Function.onFun Disjoint U))
  (exhaustive : f ⁻¹' V ⊆ ⋃ i, U i),
  (IsOpen.trivializationDiscrete U V open_V open_iff inj surj disjoint exhaustive).baseSet = V
-- Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
FirstOrder.Field.instModelACFOfCharPOfIsAlgClosed : ∀ {K : Type u_1} [inst : Field K] [inst_1 : FirstOrder.Ring.CompatibleRing K] {p : ℕ} [CharP K p] [IsAlgClosed K],
  K ⊨ FirstOrder.Language.Theory.ACF p
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SyntheticMVarDecl.mk : Lean.Syntax → Lean.Elab.Term.SyntheticMVarKind → Lean.Elab.Term.SyntheticMVarDecl
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblen_le_veblen_iff_right : ∀ {o a b : Ordinal.{u}}, Ordinal.veblen o a ≤ Ordinal.veblen o b ↔ a ≤ b
-- Std.Sync.Broadcast
/-- Closes a `Broadcast` channel.
 -/
Std.Broadcast.close : {α : Type} → Std.Broadcast α → IO Unit
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.below : {motive : {n : ℕ} → (a : List.Vector ℕ n → ℕ) → Nat.Primrec' a → Prop} →
  {n : ℕ} → {a : List.Vector ℕ n → ℕ} → Nat.Primrec' a → Prop