mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FDeriv.Pi
fderiv_single : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : DecidableEq ι] [inst_1 : NontriviallyNormedField 𝕜] {E : ι → Type u_3}
  [inst_2 : (i : ι) → NormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] {i : ι} (y : E i),
  fderiv 𝕜 (Pi.single i) y = ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (E i)))
-- Lean.Elab.Tactic.Omega.Frontend
/-- Wrapper for `asLinearComboImpl`,
using a cache for previously visited expressions.

Gives a small (10%) speedup in testing.
I tried using a pointer based cache,
but there was never enough subexpression sharing to make it effective.
 -/
Lean.Elab.Tactic.Omega.asLinearCombo : Lean.Expr →
  Lean.Elab.Tactic.Omega.OmegaM (Lean.Omega.LinearCombo × Lean.Elab.Tactic.Omega.OmegaM Lean.Expr × List Lean.Expr)
-- Mathlib.Analysis.InnerProductSpace.Subspace
_private.Mathlib.Analysis.InnerProductSpace.Subspace.0.«term⟪_,_⟫_1» : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.nonsingular_negAdd_of_eval_derivative_ne_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} {x₁ x₂ y₁ ℓ : R},
  W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ) →
    Polynomial.eval (W'.addX x₁ x₂ ℓ) (Polynomial.derivative (W'.addPolynomial x₁ y₁ ℓ)) ≠ 0 →
      W'.Nonsingular (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ)
-- Lean.Meta.SynthInstance
/-- Given `(cNode, answer)` on the top of the resume stack, continue execution by using `answer` to solve the
next subgoal.  -/
Lean.Meta.SynthInstance.resume : Lean.Meta.SynthInstance.SynthM Unit
-- Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
/-- **Alias** of the reverse direction of `Matrix.nondegenerate_iff_separatingRight`. -/
Matrix.SeparatingRight.nondegenerate : ∀ {n : Type u_1} {A : Type u_4} [inst : CommRing A] [IsDomain A] {M : Matrix n n A} [inst_2 : Finite n],
  M.SeparatingRight → M.Nondegenerate
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_ne_zero_iff : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  autoParam (μ s ≠ ⊤) MeasureTheory.measureReal_ne_zero_iff._auto_1 → (μ.real s ≠ 0 ↔ μ s ≠ 0)
-- Std.Http.Server.Config
/-- Maximum length of request URI (default: 8192 bytes)
 -/
Std.Http.Config.maxUriLength : Std.Http.Config → ℕ
-- Mathlib.Computability.EpsilonNFA
εNFA.mk.inj : ∀ {α : Type u} {σ : Type v} {step : σ → Option α → Set σ} {start accept : Set σ} {step_1 : σ → Option α → Set σ}
  {start_1 accept_1 : Set σ},
  { step := step, start := start, accept := accept } = { step := step_1, start := start_1, accept := accept_1 } →
    step = step_1 ∧ start = start_1 ∧ accept = accept_1
-- Mathlib.RingTheory.RingHomProperties
RingHom.RespectsIso.cancel_left_isIso : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  RingHom.RespectsIso P →
    ∀ {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) [CategoryTheory.IsIso f],
      P ((CommRingCat.Hom.hom g).comp (CommRingCat.Hom.hom f)) ↔ P (CommRingCat.Hom.hom g)
-- Mathlib.Order.Bounded
Set.unbounded_ge_of_forall_exists_gt : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α], (∀ (a : α), ∃ b ∈ s, b < a) → Set.Unbounded (fun x1 x2 => x1 ≥ x2) s
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.dualTensorHom_toFun : ∀ {G : Type u_6} {k : Type u_7} {V : Type u_8} {W : Type u_9} [inst : Group G] [inst_1 : Field k]
  [inst_2 : AddCommGroup V] [inst_3 : Module k V] [inst_4 : AddCommGroup W] [inst_5 : Module k W]
  [inst_6 : FiniteDimensional k V] (ρ : Representation k G V) (σ : Representation k G W)
  (x : TensorProduct k (Module.Dual k V) W), (Representation.Equiv.dualTensorHom ρ σ) x = (dualTensorHom k V W) x
-- Aesop.Tree.ExtractProof
_private.Aesop.Tree.ExtractProof.0.Aesop.extractSafePrefixMVarCluster : Lean.Environment → Aesop.MVarCluster → Aesop.SafePrefixM✝ Unit
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.zipWithLeft'TR.go.match_1.eq_3 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (motive : List α → List β → Array γ → Sort u_4) (a : α) (as : List α)
  (b : β) (bs : List β) (acc : Array γ) (h_1 : (bs : List β) → (acc : Array γ) → motive [] bs acc)
  (h_2 : (as : List α) → (acc : Array γ) → motive as [] acc)
  (h_3 : (a : α) → (as : List α) → (b : β) → (bs : List β) → (acc : Array γ) → motive (a :: as) (b :: bs) acc),
  (match a :: as, b :: bs, acc with
    | [], bs, acc => h_1 bs acc
    | as, [], acc => h_2 as acc
    | a :: as, b :: bs, acc => h_3 a as b bs acc) =
    h_3 a as b bs acc
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.toSubsemigroup_injective : ∀ {M : Type u_1} [inst : MulOneClass M], Function.Injective Submonoid.toSubsemigroup
-- Mathlib.Data.ENNReal.Operations
ENNReal.mul_lt_mul_left : ∀ {a b c : ENNReal}, a ≠ 0 → a ≠ ⊤ → b < c → b * a < c * a
-- Mathlib.Data.Set.Pairwise.Basic
Set.pairwiseDisjoint_empty : ∀ {α : Type u_1} {ι : Type u_4} [inst : PartialOrder α] [inst_1 : OrderBot α] {f : ι → α}, ∅.PairwiseDisjoint f
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsLittleO.right_isBigO_add : ∀ {α : Type u_1} {E' : Type u_6} [inst : SeminormedAddCommGroup E'] {l : Filter α} {f₁ f₂ : α → E'},
  f₁ =o[l] f₂ → f₂ =O[l] fun x => f₁ x + f₂ x
-- Mathlib.RepresentationTheory.Rep.Basic
/-- The category equivalence between `Rep` and `Action`.  -/
Rep.repIsoAction : (k : Type u) → (G : Type v) → [inst : Ring k] → [inst_1 : Monoid G] → Rep.{w, u, v} k G ≌ Action (ModuleCat k) G
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
/-- **Alias** of the forward direction of `LinearMap.isLeftQuasiInverse_iff_isRightQuasiInverse_swap`. -/
LinearMap.IsLeftQuasiInverse.isRightQuasiInverse : ∀ {K : Type u_1} {V₂ : Type u_4} {V₃ : Type u_6} [inst : CommRing K] [inst_1 : AddCommGroup V₂] [inst_2 : Module K V₂]
  [inst_3 : AddCommGroup V₃] [inst_4 : Module K V₃] {u : V₃ →ₗ[K] V₂} {v : V₂ →ₗ[K] V₃},
  u.IsLeftQuasiInverse v → v.IsRightQuasiInverse u
-- Aesop.RuleSet
Aesop.LocalRuleSet.forwardRulePatternSubstsInExpr : Aesop.LocalRuleSet → Lean.Expr → Aesop.BaseM (Array (Aesop.ForwardRule × Aesop.Substitution))
-- Mathlib.Logic.Function.Basic
/-- Non-dependent version of `Function.update_comp_eq_of_forall_ne'`  -/
Function.update_comp_eq_of_forall_ne : ∀ {α' : Sort w} [inst : DecidableEq α'] {α : Sort u_1} {β : Sort u_2} (g : α' → β) {f : α → α'} {i : α'} (a : β),
  (∀ (x : α), f x ≠ i) → Function.update g i a ∘ f = g ∘ f
-- Mathlib.Topology.Category.LightProfinite.AsLimit
/-- The transition map from `S_{n+1}` to `S_n` in `S.diagram`.  -/
LightProfinite.transitionMap : (S : LightProfinite) → (n : ℕ) → S.component (n + 1) ⟶ S.component n
-- Mathlib.Order.LiminfLimsup
Filter.bliminf_inf_not : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteDistribLattice α] {f : Filter β} {p : β → Prop} {u : β → α},
  (Filter.bliminf u f p ⊓ Filter.bliminf u f fun x => ¬p x) = Filter.liminf u f
-- Init.Data.AC
Lean.Data.AC.removeNeutrals.loop.eq_1 : ∀ {α : Sort u_1} [info : Lean.Data.AC.ContextInformation α] (ctx : α) (x_1 : ℕ) (xs : List ℕ),
  Lean.Data.AC.removeNeutrals.loop ctx (x_1 :: xs) =
    match Lean.Data.AC.ContextInformation.isNeutral ctx x_1 with
    | true => Lean.Data.AC.removeNeutrals.loop ctx xs
    | false => x_1 :: Lean.Data.AC.removeNeutrals.loop ctx xs
-- Mathlib.Condensed.Light.Sequence
_private.Mathlib.Condensed.Light.Sequence.0.InternalProjectivityProof.LightProfinite.fibre : {X Y : LightProfinite} → ↑Y.toTop → (X ⟶ Y) → LightProfinite
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
MeasureTheory.Measure.absolutelyContinuous_smul : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {c : ENNReal},
  c ≠ 0 → μ.AbsolutelyContinuous (c • μ)
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.infEDist_iUnion : ∀ {ι : Sort u_1} {α : Type u} [inst : PseudoEMetricSpace α] (f : ι → Set α) (x : α),
  Metric.infEDist x (⋃ i, f i) = ⨅ i, Metric.infEDist x (f i)
-- Mathlib.Order.NonemptyFiniteChains
PartialOrder.NonemptyFiniteChains.comparable : ∀ {X : Type u} [inst : PartialOrder X] (self : PartialOrder.NonemptyFiniteChains X) (a b : ↥self.finset), a ≤ b ∨ b ≤ a
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.State.mk.inj : ∀ {numSteps : ℕ} {persistentCache transientCache : Lean.Meta.Sym.Simp.Cache}
  {funext : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Expr} {numSteps_1 : ℕ}
  {persistentCache_1 transientCache_1 : Lean.Meta.Sym.Simp.Cache}
  {funext_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Expr},
  { numSteps := numSteps, persistentCache := persistentCache, transientCache := transientCache, funext := funext } =
      { numSteps := numSteps_1, persistentCache := persistentCache_1, transientCache := transientCache_1,
        funext := funext_1 } →
    numSteps = numSteps_1 ∧ persistentCache = persistentCache_1 ∧ transientCache = transientCache_1 ∧ funext = funext_1
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeffEquiv_symm_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (coeff : M →₀ R),
  AddMonoidAlgebra.coeffEquiv.symm coeff = AddMonoidAlgebra.ofCoeff coeff
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  [Std.TransCmp cmp] {f : α → β → Option γ} {k k' : α} {fallback : γ},
  t.WF →
    t.getKey? k = some k' →
      Std.DTreeMap.Raw.Const.getD (Std.DTreeMap.Raw.filterMap f t) k fallback =
        ((Std.DTreeMap.Raw.Const.get? t k).bind fun x => f k' x).getD fallback
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
/-- Induction principle for the objects of the small étale site of a scheme.  -/
AlgebraicGeometry.Scheme.Etale.rec : (X : AlgebraicGeometry.Scheme) →
  {motive : X.Etale → Sort u_1} →
    ((Y : AlgebraicGeometry.Scheme) →
        (f : Y ⟶ X) → (x : AlgebraicGeometry.Etale f) → motive (AlgebraicGeometry.Scheme.Etale.mk f)) →
      (T : X.Etale) → motive T
-- Mathlib.CategoryTheory.Sites.CartesianMonoidal
/-- **Alias** of `CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerRight_hom`. -/
CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerRight_val : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  (J : CategoryTheory.GrothendieckTopology C) [inst_2 : CategoryTheory.CartesianMonoidalCategory A]
  {X W : CategoryTheory.Sheaf J A} (f : W ⟶ X),
  (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X).hom =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom X.obj
-- Mathlib.Algebra.Module.Injective
Module.Baer.extensionOfMax_le : ∀ {R : Type u} [inst : Ring R] {Q : Type v} [inst_1 : AddCommGroup Q] [inst_2 : Module R Q] {M : Type u_1}
  {N : Type u_2} [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N]
  (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [inst_7 : Fact (Function.Injective ⇑i)] (h : Module.Baer R Q) {y : N},
  Module.Baer.extensionOfMax i f ≤ Module.Baer.extensionOfMaxAdjoin i f h y
-- Mathlib.Probability.Decision.Risk.Countable
ProbabilityTheory.bayesRisk_fintype' : ∀ {Θ : Type u_1} {𝓧 : Type u_3} {𝓨 : Type u_5} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : ProbabilityTheory.Kernel Θ 𝓧} {π : MeasureTheory.Measure Θ}
  [inst : Fintype 𝓨] [MeasurableSingletonClass 𝓨],
  Measurable ℓ →
    ProbabilityTheory.bayesRisk ℓ P π =
      ⨅ κ, ⨅ (_ : ProbabilityTheory.IsMarkovKernel κ), ∑ y, ∫⁻ (θ : Θ), ℓ θ y * ((P θ).bind ⇑κ) {y} ∂π
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
CategoryTheory.Idempotents.karoubiUniversal₁_functor : ∀ (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],
  (CategoryTheory.Idempotents.karoubiUniversal₁ C D).functor = CategoryTheory.Idempotents.functorExtension₁ C D
-- Lean.Meta.Basic
Lean.Meta.Diagnostics.mk : Lean.PHashMap Lean.Name ℕ →
  Lean.PHashMap Lean.Name ℕ →
    Lean.PHashMap Lean.Name ℕ →
      Lean.PHashMap Lean.Name ℕ → Lean.PHashMap Lean.Expr Lean.MessageData → Lean.Meta.Diagnostics
-- Init.Data.List.Basic
List.idxOf_nil : ∀ {α : Type u} {x : α} [inst : BEq α], List.idxOf x [] = 0
-- Mathlib.Computability.Language
Language.map_id : ∀ {α : Type u_1} (l : Language α), (Language.map id) l = l
-- Lean.Meta.Basic
Lean.Meta.instMonadBacktrackSavedStateMetaM : Lean.MonadBacktrack Lean.Meta.SavedState Lean.MetaM
-- Lean.Compiler.IR.Basic
Lean.IR.CtorInfo.mk.injEq : ∀ (name : Lean.Name) (cidx size usize ssize : ℕ) (name_1 : Lean.Name) (cidx_1 size_1 usize_1 ssize_1 : ℕ),
  ({ name := name, cidx := cidx, size := size, usize := usize, ssize := ssize } =
      { name := name_1, cidx := cidx_1, size := size_1, usize := usize_1, ssize := ssize_1 }) =
    (name = name_1 ∧ cidx = cidx_1 ∧ size = size_1 ∧ usize = usize_1 ∧ ssize = ssize_1)
-- Mathlib.NumberTheory.RamificationInertia.Galois
Ideal.instMulActionAlgEquivElemPrimesOver : {A : Type u_1} →
  {B : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        [inst_2 : Algebra A B] →
          {p : Ideal A} →
            (K : Type u_4) →
              (L : Type u_5) →
                [inst_3 : Field K] →
                  [inst_4 : Field L] →
                    [inst_5 : Algebra A K] →
                      [IsFractionRing A K] →
                        [inst_7 : Algebra B L] →
                          [inst_8 : Algebra K L] →
                            [inst_9 : Algebra A L] →
                              [IsScalarTower A B L] →
                                [IsScalarTower A K L] →
                                  [IsIntegralClosure B A L] →
                                    [FiniteDimensional K L] → MulAction Gal(L/K) ↑(p.primesOver B)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulMonC_nc : ℤ → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Poly → ℕ → Lean.Grind.CommRing.Poly
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteMulArchimedeanClass.mk.congr_simp : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] (a a_1 : M) (e_a : a = a_1)
  (h : a ≠ 1), FiniteMulArchimedeanClass.mk a h = FiniteMulArchimedeanClass.mk a_1 ⋯
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.d_sndX : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i j : ι) (hij : c.Rel i j),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.d φ i j)
      (HomologicalComplex.homotopyCofiber.sndX φ j) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.fstX φ i j hij) (φ.f j) +
      CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.sndX φ i) (G.d i j)
-- Lean.Expr
Lean.Expr.bindingBody! : Lean.Expr → Lean.Expr
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.nontrivial_span_singleton : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {x : M},
  x ≠ 0 → Nontrivial ↥(R ∙ x)
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpEntry.toUnfoldThms.sizeOf_spec : ∀ (a : Lean.Name) (a_1 : Array Lean.Name), sizeOf (Lean.Meta.SimpEntry.toUnfoldThms a a_1) = 1 + sizeOf a + sizeOf a_1
-- Std.Sat.AIG.Basic
Std.Sat.AIG.CacheHit.hvalid : ∀ {α : Type} {decls : Array (Std.Sat.AIG.Decl α)} {decl : Std.Sat.AIG.Decl α} (self : Std.Sat.AIG.CacheHit decls decl),
  decls[self.idx] = decl
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.algebraMapInv.eq_1 : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  ExteriorAlgebra.algebraMapInv = (ExteriorAlgebra.lift R) ⟨0, ⋯⟩
-- Init.Data.Rat.Lemmas
Rat.intCast_pow : ∀ (a : ℤ) (n : ℕ), ↑(a ^ n) = ↑a ^ n
-- Mathlib.SetTheory.Cardinal.Regular
/-- A cardinal equals its own cofinality. See `IsRegular.cof_eq`.  -/
Cardinal.IsRegular.le_cof_ord : ∀ {c : Cardinal.{u_1}}, c.IsRegular → c ≤ c.ord.cof
-- Aesop.Builder.Basic
Aesop.PhaseSpec : Type
-- Mathlib.Order.Filter.AtTopBot.Tendsto
Filter.OrderTop.atTop_eq : ∀ (α : Type u_6) [inst : PartialOrder α] [inst_1 : OrderTop α], Filter.atTop = pure ⊤
-- Batteries.Data.String.Lemmas
String.extract_zero_rawEndPos : ∀ (s : String), String.Pos.Raw.extract s 0 s.rawEndPos = s
-- Mathlib.GroupTheory.Torsion
/-- The additive `p`-primary component is the subgroup of elements `g` such that
`p ^ k • g = 0` for some `k`. For prime `p`, these are exactly the elements of additive
`p`-power order.  -/
AddCommGroup.primaryComponent : (G : Type u_1) → [inst : AddCommGroup G] → ℕ → AddSubgroup G
-- Std.Data.DTreeMap.Raw.Lemmas
/-- Simpler variant of `get?_filter` when `LawfulEqCmp` is available.  -/
Std.DTreeMap.Raw.Const.get?_filter' : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {f : α → β → Bool} {k : α},
  t.WF →
    Std.DTreeMap.Raw.Const.get? (Std.DTreeMap.Raw.filter f t) k = Option.filter (f k) (Std.DTreeMap.Raw.Const.get? t k)
-- Mathlib.Algebra.GroupWithZero.Defs
isRightCancelMulZero_iff : ∀ (M₀ : Type u) [inst : Mul M₀] [inst_1 : Zero M₀], IsRightCancelMulZero M₀ ↔ ∀ {a : M₀}, a ≠ 0 → IsRightRegular a
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec.0.BitVec.instReprLiteral.repr : BitVec.Literal✝ → ℕ → Std.Format
-- Lean.Declaration
Lean.ConstantInfo.inductInfo : Lean.InductiveVal → Lean.ConstantInfo
-- Mathlib.GroupTheory.Commensurable
Subgroup.Commensurable.commensurator_mem_iff : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) (g : G),
  g ∈ Subgroup.Commensurable.commensurator H ↔ (ConjAct.toConjAct g • H).Commensurable H
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.opow_lt_opow_iff_right : ∀ {a b c : Ordinal.{u_1}}, 1 < a → (a ^ b < a ^ c ↔ b < c)
-- Lean.Data.Lsp.Internal
/-- Version of the file these references are from.  -/
Lean.Lsp.LeanIleanInfoParams.version : Lean.Lsp.LeanIleanInfoParams → ℕ
-- Mathlib.LinearAlgebra.FreeModule.PID
Submodule.smithNormalFormBotBasis.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsDomain R] [inst_4 : IsPrincipalIdealRing R] {N : Submodule R M} [inst_5 : Finite ι]
  (b b_1 : Module.Basis ι R M),
  b = b_1 →
    ∀ (h : Module.finrank R ↥N = Module.finrank R M),
      Submodule.smithNormalFormBotBasis b h = Submodule.smithNormalFormBotBasis b_1 h
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.evalSuggestImpl : Lean.Elab.Tactic.Try.TryTactic
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
CategoryTheory.InjectiveResolution.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (cocomplex : CochainComplex C ℕ)
  (injective :
    autoParam (∀ (n : ℕ), CategoryTheory.Injective (cocomplex.X n))
      CategoryTheory.InjectiveResolution.injective._autoParam)
  [hasHomology : ∀ (i : ℕ), HomologicalComplex.HasHomology cocomplex i]
  (ι : (CochainComplex.single₀ C).obj Z ⟶ cocomplex)
  (quasiIso : autoParam (QuasiIso ι) CategoryTheory.InjectiveResolution.quasiIso._autoParam)
  (cocomplex_1 : CochainComplex C ℕ)
  (injective_1 :
    autoParam (∀ (n : ℕ), CategoryTheory.Injective (cocomplex_1.X n))
      CategoryTheory.InjectiveResolution.injective._autoParam)
  (hasHomology_1 : ∀ (i : ℕ), HomologicalComplex.HasHomology cocomplex_1 i)
  (ι_1 : (CochainComplex.single₀ C).obj Z ⟶ cocomplex_1)
  (quasiIso_1 : autoParam (QuasiIso ι_1) CategoryTheory.InjectiveResolution.quasiIso._autoParam),
  ({ cocomplex := cocomplex, injective := injective, hasHomology := hasHomology, ι := ι, quasiIso := quasiIso } =
      { cocomplex := cocomplex_1, injective := injective_1, hasHomology := hasHomology_1, ι := ι_1,
        quasiIso := quasiIso_1 }) =
    (cocomplex = cocomplex_1 ∧ ι ≍ ι_1)
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
Topology.IsOpenEmbedding.toOpenPartialHomeomorph_apply : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y)
  (h : Topology.IsOpenEmbedding f) [inst_2 : Nonempty X], ↑(Topology.IsOpenEmbedding.toOpenPartialHomeomorph f h) = f
-- Mathlib.Algebra.Group.Action.Defs
VAddAssocClass.to₁₃₄ : ∀ (M : Type u_9) (N : Type u_10) (P : Type u_11) (Q : Type u_12) [inst : VAdd M N] [inst_1 : VAdd M P]
  [inst_2 : VAdd M Q] [inst_3 : VAdd P Q] [inst_4 : AddMonoid N] [inst_5 : AddAction N P] [inst_6 : AddAction N Q]
  [VAddAssocClass M N P] [VAddAssocClass M N Q] [VAddAssocClass N P Q], VAddAssocClass M P Q
-- Mathlib.Order.CompleteLattice.Basic
iInf_mono' : ∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [inst : CompleteLattice α] {f : ι → α} {g : ι' → α},
  (∀ (i : ι), ∃ i', g i' ≤ f i) → iInf g ≤ iInf f
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1to1.write.match_1.eq_2 : ∀ {Γ : Type u_3} {Λ : Type u_2} {σ : Type u_1}
  (motive : List Bool → Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ → Sort u_4) (a : Bool) (l : List Bool)
  (q : Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ)
  (h_1 : (q : Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ) → motive [] q)
  (h_2 : (a : Bool) → (l : List Bool) → (q : Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ) → motive (a :: l) q),
  (match a :: l, q with
    | [], q => h_1 q
    | a :: l, q => h_2 a l q) =
    h_2 a l q
-- Mathlib.Order.Interval.Finset.Defs
/-- Transfer `LocallyFiniteOrder` across an `OrderIso`.  -/
OrderIso.locallyFiniteOrder : {α : Type u_1} →
  {β : Type u_2} → [inst : Preorder α] → [inst_1 : Preorder β] → [LocallyFiniteOrder β] → α ≃o β → LocallyFiniteOrder α
-- Mathlib.CategoryTheory.Category.ULift
CategoryTheory.eqToHom_down : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : CategoryTheory.AsSmall C} (h : X = Y),
  (CategoryTheory.eqToHom h).down = CategoryTheory.eqToHom ⋯
-- Lean.Meta.Constructions.CtorElim
_private.Lean.Meta.Constructions.CtorElim.0.Lean.reassocMax : Lean.Level → Lean.Level
-- Mathlib.RingTheory.Noetherian.Basic
isNoetherian_of_surjective : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {P : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module S P] {σ : R →+* S}
  [inst_6 : RingHomSurjective σ] (f : M →ₛₗ[σ] P), f.range = ⊤ → ∀ [IsNoetherian R M], IsNoetherian S P
-- Mathlib.Algebra.Order.ToIntervalMod
AddCommGroup.modEq_iff_toIcoMod_add_period_eq_toIocMod : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) {a b : α}, a ≡ b [PMOD p] ↔ toIcoMod hp a b + p = toIocMod hp a b
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {a b : B} (f : a ⟶ b),
  CategoryTheory.Bicategory.whiskerRight (F.mapId a).hom (F.map f) =
    CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.id a) f).inv
      (CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom)
        (CategoryTheory.Bicategory.leftUnitor (F.map f)).inv)
-- Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
MeasureTheory.measure_liminf_atTop_eq_zero : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F}
  {s : ℕ → Set α}, ∑' (i : ℕ), μ (s i) ≠ ⊤ → μ (Filter.liminf s Filter.atTop) = 0
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey_inter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} {h_mem : k ∈ m₁ ∩ m₂},
  (m₁ ∩ m₂).getKey k h_mem = m₁.getKey k ⋯