mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.Height.Basic
/-- The multiplicative height of `x * y` is at most the product of the multiplicative heights
of `x` and `y`.  -/
Height.mulHeight₁_mul_le : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] (x y : K),
  Height.mulHeight₁ (x * y) ≤ Height.mulHeight₁ x * Height.mulHeight₁ y
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.preimage_closedBall : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x : E) (r : ℝ), ⇑f ⁻¹' Metric.closedBall (f x) r = Metric.closedBall x r
-- Mathlib.Combinatorics.Quiver.Schreier
/-- The star map of the labelling prefunctor as an equivalence.  -/
Quiver.SchreierGraph.labellingStarEquiv : {V : Type u_1} →
  {M : Type u_2} →
    [inst : Group M] →
      [inst_1 : MulAction M V] →
        {S : Type u_3} →
          (ι : S → M) → (x : Quiver.SchreierGraph V ι) → Quiver.Star x ≃ Quiver.Star (Quiver.SingleObj.star S)
-- Mathlib.Order.GaloisConnection.Basic
sSup_image2_eq_sInf_sSup : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  [inst_2 : CompleteLattice γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β},
  (∀ (b : β), GaloisConnection (Function.swap l b ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₁ b)) →
    (∀ (a : α), GaloisConnection (l a) (u₂ a)) → sSup (Set.image2 l s t) = l (sInf s) (sSup t)
-- Mathlib.SetTheory.ZFC.Class
Class.toSet_of_ZFSet : ∀ (A : Class.{u}) (x : ZFSet.{u}), A.ToSet ↑x ↔ A x
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_sub_le : ∀ {R : Type u} [inst : Ring R] (p q : Polynomial R), (p - q).degree ≤ max p.degree q.degree
-- Mathlib.Tactic.Monotonicity.Basic
/-- `mono` applies monotonicity rules and local hypotheses repetitively.  For example,
```lean
example (x y z k : ℤ)
    (h : 3 ≤ (4 : ℤ))
    (h' : z ≤ y) :
    (k + 3 + x) - y ≤ (k + 4 + x) - z := by
  mono
```
 -/
Mathlib.Tactic.Monotonicity.mono : Lean.ParserDescr
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.farFromTriangleFree : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {𝕜 : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] (t : Finset (α × β × γ)) [inst_3 : DecidableEq α] [inst_4 : DecidableEq β]
  [inst_5 : DecidableEq γ] [inst_6 : Fintype α] [inst_7 : Fintype β] [inst_8 : Fintype γ]
  [SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint t] {ε : 𝕜},
  ε * ↑((Fintype.card α + Fintype.card β + Fintype.card γ) ^ 2) ≤ ↑t.card →
    (SimpleGraph.TripartiteFromTriangles.graph t).FarFromTriangleFree ε
-- Mathlib.FieldTheory.Differential.Basic
Differential.logDeriv_prod_of_eq_zero : ∀ {R : Type u_1} [inst : Field R] [inst_1 : Differential R] (ι : Type u_2) (s : Finset ι) (f : ι → R),
  (∀ x ∈ s, f x = 0) → Differential.logDeriv (∏ x ∈ s, f x) = ∑ x ∈ s, Differential.logDeriv (f x)
-- Lean.Expr
/-- Given `f a₀ a₁ ... aₙ`, returns the `i`th argument or returns `v₀` if out of bounds.  -/
Lean.Expr.getArgD : (e : Lean.Expr) → ℕ → Lean.Expr → optParam ℕ e.getAppNumArgs → Lean.Expr
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
ContinuousLinearMap.intervalIntegral_comp_comm : ∀ {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ}
  {μ : MeasureTheory.Measure ℝ} {f : ℝ → E} [inst_2 : RCLike 𝕜] [inst_3 : NormedSpace 𝕜 E]
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F] [inst_6 : NormedSpace ℝ F] [CompleteSpace F]
  [CompleteSpace E] (L : E →L[𝕜] F),
  IntervalIntegrable f μ a b → ∫ (x : ℝ) in a..b, L (f x) ∂μ = L (∫ (x : ℝ) in a..b, f x ∂μ)
-- Mathlib.CategoryTheory.Sums.Products
CategoryTheory.Sum.functorEquiv_functor_obj : ∀ (A : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} A] (A' : Type u_2)
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] (B : Type u) [inst_2 : CategoryTheory.Category.{v, u} B]
  (F : CategoryTheory.Functor (A ⊕ A') B),
  (CategoryTheory.Sum.functorEquiv A A' B).functor.obj F =
    ((CategoryTheory.Sum.inl_ A A').comp F, (CategoryTheory.Sum.inr_ A A').comp F)
-- Mathlib.Topology.Maps.Proper.Basic
/-- Definition of proper maps. See also `isClosedMap_iff_clusterPt` for a related criterion
for closed maps.  -/
isProperMap_iff_clusterPt : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
  IsProperMap f ↔ Continuous f ∧ ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.MatcherKey : Type
-- Lean.Elab.Tactic.Split
_private.Lean.Elab.Tactic.Split.0.Lean.Elab.Tactic.evalSplit.throwCouldNotSplitWildcard : {α : Type} → Array Lean.FVarId → Lean.MVarId → Lean.MetaM α
-- Lean.Environment
Lean.ConstantKind.thm.sizeOf_spec : sizeOf Lean.ConstantKind.thm = 1
-- Mathlib.CategoryTheory.Center.Basic
CategoryTheory.CatCenter.mul_app'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (x y : CategoryTheory.CatCenter C) (X : C) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((x * y).app X) h =
    CategoryTheory.CategoryStruct.comp (y.app X) (CategoryTheory.CategoryStruct.comp (x.app X) h)
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.yonedaEquiv_symm_naturality_left : ∀ {X : SSet} {m n : SimplexCategory} (f : m ⟶ n) (g : X.obj (Opposite.op n)),
  CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.map f) (SSet.yonedaEquiv.symm g) =
    SSet.yonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (X.map f.op)) g)
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.Limits.CoconePt.fac_apply : ∀ {J : Type u} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  {F : CategoryTheory.Functor J PartOrdEmb}
  {c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget PartOrdEmb))}
  (hc : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cocone F) (j : J) (x : ↑(F.obj j)),
  (PartOrdEmb.Limits.CoconePt.desc hc s) ((CategoryTheory.ConcreteCategory.hom (c.ι.app j)) x) =
    (CategoryTheory.ConcreteCategory.hom (s.ι.app j)) x
-- Mathlib.Algebra.Torsor.Defs
AddTorsor.toAddAction : {G : outParam (Type u_1)} → {P : Type u_2} → {inst : AddGroup G} → [self : AddTorsor G P] → AddAction G P
-- Mathlib.RingTheory.Localization.AsSubring
Localization.subalgebra.isLocalization_subalgebra : ∀ {A : Type u_1} (K : Type u_2) [inst : CommRing A] (S : Submonoid A) (hS : S ≤ nonZeroDivisors A) [inst_1 : CommRing K]
  [inst_2 : Algebra A K] [inst_3 : IsFractionRing A K], IsLocalization S ↥(Localization.subalgebra K S hS)
-- Mathlib.Data.Set.Prod
Set.update_mem_pi_iff : ∀ {ι : Type u_1} {α : ι → Type u_2} {s : Set ι} {t : (i : ι) → Set (α i)} [inst : DecidableEq ι] {a : (i : ι) → α i}
  {i : ι} {b : α i}, Function.update a i b ∈ s.pi t ↔ a ∈ (s \ {i}).pi t ∧ (i ∈ s → b ∈ t i)
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.hasNonTrivialExample : Lean.Meta.Match.Problem → Bool
-- Std.Do.SPred.DerivedLaws
/-- A mapping from propositions to `SPred` tautologies that are known to be logically equivalent.
This is used to rewrite proof goals into a form that is suitable for use with `mvcgen`.
 -/
Std.Do.SPred.Tactic.PropAsSPredTautology : Prop → {σs : outParam (List (Type u))} → outParam (Std.Do.SPred σs) → Prop
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_inter_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → Std.DHashMap.Raw.Const.get? (m₁ ∩ m₂) k = none
-- Init.Data.BitVec.Bitblast
BitVec.getMsbD_udiv : ∀ {w : ℕ} (n d : BitVec w),
  0#w < d →
    ∀ (i : ℕ),
      (n / d).getMsbD i =
        (decide (i < w) && (BitVec.divRec w { n := n, d := d } (BitVec.DivModState.init w)).q.getMsbD i)
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_snd_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) {Z_1 : C} (h : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f)
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f g)
        (CategoryTheory.Limits.pullback.fst f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h)
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- The `k`-th iterated derivative of a multilinear map `f` at the point `x`. It is a multilinear
map of `k` vectors `v₁, ..., vₖ` (with the same type as `x`), mapping them
to `∑ f (x₁, (v_{i₁})₂, x₃, ...)`, where at each index `j` one uses either `xⱼ` or one
of the `(vᵢ)ⱼ`, and each `vᵢ` has to be used exactly once.
The sum is parameterized by the embeddings of `Fin k` in the index type `ι` (or, equivalently,
by the subsets `s` of `ι` of cardinality `k` and then the bijections between `Fin k` and `s`).

For the continuous version, see `ContinuousMultilinearMap.iteratedFDeriv`.  -/
MultilinearMap.iteratedFDeriv : {R : Type uR} →
  {ι : Type uι} →
    {M₁ : ι → Type v₁} →
      {M₂ : Type v₂} →
        [inst : CommSemiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] →
                [inst_4 : Module R M₂] →
                  [Fintype ι] →
                    MultilinearMap R M₁ M₂ → (k : ℕ) → ((i : ι) → M₁ i) → MultilinearMap R (fun x => (i : ι) → M₁ i) M₂
-- Aesop.Forward.State
_private.Aesop.Forward.State.0.Aesop.RuleState.update.addCompleteMatches.loop.eq_def : ∀ (rs : Aesop.RuleState) (clusterStates : Array Aesop.ClusterState) (clusterIdx : ℕ)
  (newClusterCompleteMatches : Array Aesop.Match) (m : Aesop.CompleteMatch) (i : ℕ),
  Aesop.RuleState.update.addCompleteMatches.loop✝ rs clusterStates clusterIdx newClusterCompleteMatches m i =
    if h : i < clusterStates.size then
      if (i == clusterIdx) = true then do
        forIn newClusterCompleteMatches PUnit.unit fun cm __s => do
            Aesop.RuleState.update.addCompleteMatches.loop✝ rs clusterStates clusterIdx newClusterCompleteMatches
                { clusterMatches := m.clusterMatches.push cm } (i + 1)
            pure (ForInStep.yield PUnit.unit)
        pure ()
      else do
        forIn clusterStates[i].completeMatches PUnit.unit fun cm __s => do
            Aesop.RuleState.update.addCompleteMatches.loop✝ rs clusterStates clusterIdx newClusterCompleteMatches
                { clusterMatches := m.clusterMatches.push cm } (i + 1)
            pure (ForInStep.yield PUnit.unit)
        pure ()
    else modify fun ms => ms.push { rule := rs.rule, «match» := m }
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {h_mem : k ∈ m₁ \ m₂},
  Std.ExtDHashMap.Const.get (m₁ \ m₂) k h_mem = Std.ExtDHashMap.Const.get m₁ k ⋯
-- Mathlib.Algebra.GroupWithZero.Basic
div_sq_cancel : ∀ {G₀ : Type u_2} [inst : CommGroupWithZero G₀] (a b : G₀), a ^ 2 * b / a = a * b
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.inv_fst : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B)
  {x y : CategoryTheory.Limits.CategoricalPullback F G} (f : x ⟶ y) [inst_3 : CategoryTheory.IsIso f],
  (CategoryTheory.inv f).fst = CategoryTheory.inv f.fst
-- Mathlib.SetTheory.ZFC.Rank
PSet.rank_pair : ∀ (x y : PSet.{u_1}), {x, y}.rank = max (Order.succ x.rank) (Order.succ y.rank)
-- Init.Data.List.Impl
List.eraseP_eq_erasePTR : @List.eraseP = @List.erasePTR
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.isCoprime_x_z : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [inst_2 : IsCyclotomicExtension {3} ℚ K],
  IsCoprime (FermatLastTheoremForThreeGen.Solution.x✝ S) (FermatLastTheoremForThreeGen.Solution.z✝ S)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_inv_natCast_pow : ∀ (x : NNReal) {n : ℕ}, n ≠ 0 → (x ^ (↑n)⁻¹) ^ n = x
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_const_mul : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {L : Type u_6} [inst : RCLike L] (r : L)
  (f : α → L), ∫ (a : α), r * f a ∂μ = r * ∫ (a : α), f a ∂μ
-- Mathlib.Topology.Order.DenselyOrdered
Ico_subset_closure_interior : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] (a b : α),
  Set.Ico a b ⊆ closure (interior (Set.Ico a b))
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.uset : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.FVarId →
    ℕ →
      Lean.FVarId →
        autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_5 →
          Lean.Compiler.LCNF.CodeDecl pu
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.cycles.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S S_1 : CategoryTheory.ShortComplex C) (e_S : S = S_1) [inst_2 : S.HasLeftHomology], S.cycles = S_1.cycles
-- Mathlib.Data.Set.Lattice.Image
Set.surjOn_iInter : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [Nonempty ι] {s : ι → Set α} {t : Set β} {f : α → β},
  (∀ (i : ι), Set.SurjOn f (s i) t) → Set.InjOn f (⋃ i, s i) → Set.SurjOn f (⋂ i, s i) t
-- Mathlib.Order.WithBot
WithBot.lt_def' : ∀ {α : Type u_1} [inst : LT α] {x y : WithBot α}, y < x ↔ (∃ a, x = ↑a) ∧ y = ⊥ ∨ ∃ a, ∃ b < a, x = ↑a ∧ y = ↑b
-- Mathlib.RingTheory.Finiteness.Basic
Module.Finite.of_pi : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_6} (M : ι → Type u_7) [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [Module.Finite R ((i : ι) → M i)] (i : ι), Module.Finite R (M i)
-- Mathlib.GroupTheory.Commutator.Basic
AddCommute.addCommutator_eq : ∀ {G : Type u_1} [inst : AddGroup G] {g₁ g₂ : G}, AddCommute g₁ g₂ → ⁅g₁, g₂⁆ = 0
-- Mathlib.Topology.Algebra.Module.LinearPMap
/-- If `f` is invertible and closable, then taking the closure and the inverse commute.  -/
LinearPMap.inverse_closure : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  {f : E →ₗ.[R] F} [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : TopologicalSpace R]
  [inst_10 : ContinuousSMul R E] [inst_11 : ContinuousSMul R F],
  f.toFun.ker = ⊥ → f.IsClosable → f.closure.toFun.ker = ⊥ → f.inverse.closure = f.closure.inverse
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- In a pseudometric space, the extended distance is always finite  -/
edist_ne_top : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y : α), edist x y ≠ ⊤
-- Mathlib.CategoryTheory.Products.Basic
/-- Any morphism in a product factors as a morphism whose left component is an identity
followed by a morphism whose right component is an identity.  -/
CategoryTheory.Prod.fac_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {x y : C × D} (f : x ⟶ y) {Z : C × D} (h : y ⟶ Z),
  CategoryTheory.CategoryStruct.comp f h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id x.1) f.2)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Prod.mkHom f.1 (CategoryTheory.CategoryStruct.id y.2)) h)
-- Mathlib.Algebra.Group.Defs
AddCommMonoid.mk : {M : Type u} → [toAddMonoid : AddMonoid M] → (∀ (a b : M), a + b = b + a) → AddCommMonoid M
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonLeanDidOpenTextDocumentParams : Lean.FromJson Lean.Lsp.LeanDidOpenTextDocumentParams
-- Init.Data.Int.Order
Int.mul_le_mul_of_nonpos_right : ∀ {a b c : ℤ}, b ≤ a → c ≤ 0 → a * c ≤ b * c
-- Mathlib.Data.List.Nodup
List.disjoint_of_nodup_append : ∀ {α : Type u} {l₁ l₂ : List α}, (l₁ ++ l₂).Nodup → l₁.Disjoint l₂
-- Mathlib.Control.Monad.Cont
OptionT.goto_mkLabel : ∀ {m : Type u → Type v} [inst : Monad m] {α β : Type u} (x : MonadCont.Label (Option α) m β) (i : α),
  MonadCont.goto (OptionT.mkLabel x) i =
    OptionT.mk do
      let a ← MonadCont.goto x (some i)
      pure (some a)
-- Mathlib.Topology.Algebra.Group.Basic
tendsto_neg_nhdsLT : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : AddCommGroup H] [inst_2 : PartialOrder H] [IsOrderedAddMonoid H]
  [ContinuousNeg H] {a : H}, Filter.Tendsto Neg.neg (nhdsWithin a (Set.Iio a)) (nhdsWithin (-a) (Set.Ioi (-a)))
-- Mathlib.Data.PFunctor.Multivariate.M
MvPFunctor.M.dest_corec' : ∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {β : Type v} (g₀ : β → P.A)
  (g₁ : (b : β) → (P.drop.B (g₀ b)).Arrow α) (g₂ : (b : β) → P.last.B (g₀ b) → β) (x : β),
  MvPFunctor.M.dest P (MvPFunctor.M.corec' P g₀ g₁ g₂ x) =
    ⟨g₀ x, TypeVec.splitFun (g₁ x) (MvPFunctor.M.corec' P g₀ g₁ g₂ ∘ g₂ x)⟩
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a fallback : α}, m.contains a = false → m.getKeyD a fallback = fallback
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.pow_mod_card_support_cycleOf_self_apply : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] (f : Equiv.Perm α) (n : ℕ) (x : α),
  (f ^ (n % (f.cycleOf x).support.card)) x = (f ^ n) x
-- Mathlib.Algebra.Homology.HomotopyCofiber
/-- The right inclusion `G.X i ⟶ (homotopyCofiber φ).X i`.  -/
HomologicalComplex.homotopyCofiber.inrX : {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 : ι) → G.X i ⟶ HomologicalComplex.homotopyCofiber.X φ i
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.eval_polynomialZ : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P : Fin 3 → R),
  (MvPolynomial.eval P) W'.polynomialZ =
    P 1 ^ 2 + W'.a₁ * P 0 * P 1 + 2 * W'.a₃ * P 1 * P 2 -
      (W'.a₂ * P 0 ^ 2 + 2 * W'.a₄ * P 0 * P 2 + 3 * W'.a₆ * P 2 ^ 2)
-- Mathlib.CategoryTheory.Action.Continuous
/-- A predicate on an `X : ContAction V G` saying that the topology on the underlying type of `X`
is discrete.  -/
ContAction.IsDiscrete : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {FV : V → V → Type u_2} →
      {CV : V → Type u_3} →
        [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory V FV] →
            [inst_3 : CategoryTheory.HasForget₂ V TopCat] →
              {G : Type u_4} → [inst_4 : Monoid G] → [inst_5 : TopologicalSpace G] → ContAction V G → Prop
-- Mathlib.Data.Finset.Prod
Finset.offDiag_empty : ∀ {α : Type u_1}, ∅.offDiag = ∅
-- Batteries.Lean.Meta.Basic
/-- Sort the given `FVarId`s by the order in which they appear in the current local
context. If any of the `FVarId`s do not appear in the current local context, the
result is unspecified.
 -/
Lean.Meta.sortFVarsByContextOrder : {m : Type → Type} → [Monad m] → [Lean.MonadLCtx m] → Array Lean.FVarId → m (Array Lean.FVarId)
-- Mathlib.Data.Stream.Init
Stream'.const_eq : ∀ {α : Type u} (a : α), Stream'.const a = Stream'.cons a (Stream'.const a)
-- Mathlib.Topology.Metrizable.Uniformity
/-- Construct on a pseudometrizable space a pseudometric compatible with the topology.  -/
TopologicalSpace.pseudoMetrizableSpacePseudoMetric : (X : Type u_2) → [inst : TopologicalSpace X] → [TopologicalSpace.PseudoMetrizableSpace X] → PseudoMetricSpace X
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.instNeg : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {U : Set X} → {Y : Type u_2} → [inst_1 : AddGroup Y] → Neg (Function.locallyFinsuppWithin U Y)
-- Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
TrivSqZeroExt.nnnorm_inl : ∀ {R : Type u_3} {M : Type u_4} [inst : SeminormedRing R] [inst_1 : SeminormedAddCommGroup M] (r : R),
  ‖TrivSqZeroExt.inl r‖₊ = ‖r‖₊
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroup.brecOn.go : {R : Type u} →
  {motive : Rack.PreEnvelGroup R → Sort u_1} →
    (t : Rack.PreEnvelGroup R) →
      ((t : Rack.PreEnvelGroup R) → Rack.PreEnvelGroup.below t → motive t) → motive t ×' Rack.PreEnvelGroup.below t
-- Init.Meta.Defs
Lean.Name.instLawfulBEq : LawfulBEq Lean.Name
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.instTop.eq_1 : ∀ {R : Type u} {M : Type v} [inst : SMul R M], SubMulAction.instTop = { top := { carrier := Set.univ, smul_mem' := ⋯ } }
-- Mathlib.Tactic.DeclarationNames
/-- Used for linters which use `0` instead of `false` for disabling.  -/
Mathlib.Linter.logLint0Disable : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadLog m] →
      [Lean.AddMessageContext m] → [Lean.MonadOptions m] → Lean.Option ℕ → Lean.Syntax → Lean.MessageData → m Unit
-- Init.Data.Nat.Fold
Nat.fold_congr : ∀ {α : Type u} {n m : ℕ} (w : n = m) (f : (i : ℕ) → i < n → α → α) (init : α),
  n.fold f init = m.fold (fun i h => f i ⋯) init
-- Mathlib.Topology.Category.Profinite.Projective
Profinite.projective_ultrafilter : ∀ (X : Type u), CategoryTheory.Projective (Profinite.of (Ultrafilter X))
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedAddSubmonoid.instSetLike : (M : Type u_1) → [inst : AddZeroClass M] → SetLike (SaturatedAddSubmonoid M) M
-- Std.Tactic.Do.Syntax
/-- `mhave` is like `have`, but operating on a stateful `Std.Do.SPred` goal.
```lean
example (P Q : SPred σs) : P ⊢ₛ (P → Q) → Q := by
  mintro HP HPQ
  mhave HQ : Q := by mspecialize HPQ HP; mexact HPQ
  mexact HQ
```
 -/
Lean.Parser.Tactic.mhave : Lean.ParserDescr
-- Batteries.Data.List.Lemmas
List.findIdxNth_eq_length_of_ge_countP : ∀ {α : Type u_1} {p : α → Bool} {n : ℕ} {xs : List α}, List.countP p xs ≤ n → List.findIdxNth p xs n = xs.length
-- Mathlib.NumberTheory.Harmonic.Defs
/-- The nth-harmonic number defined as a finset sum of consecutive reciprocals.  -/
harmonic : ℕ → ℚ
-- Std.Internal.UV.UDP
/-- Returns an `IO.Promise` that resolves once `socket` has data available for reading. Calling this
function twice on the same `Socket` or in parallel with `recv` is not supported.
 -/
Std.Internal.UV.UDP.Socket.waitReadable : Std.Internal.UV.UDP.Socket → IO (IO.Promise (Except IO.Error Unit))
-- Init.Data.Int.DivMod.Lemmas
Int.le_of_dvd : ∀ {a b : ℤ}, 0 < b → a ∣ b → a ≤ b
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.degree_mul_X : ∀ {R : Type u} [inst : Semiring R] [Nontrivial R] {p : Polynomial R}, (p * Polynomial.X).degree = p.degree + 1
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.contains.match_3.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k' : α) →
        (v : β k') → (l r : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner size k' v l r)),
  (match Std.DTreeMap.Internal.Impl.leaf with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k' v l r => h_2 size k' v l r) =
    h_1 ()
-- Mathlib.Data.Part
Part.one_def : ∀ {α : Type u_1} [inst : One α], 1 = Part.some 1