mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Fork.IsLimit.lift_ι' : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s : CategoryTheory.Limits.Fork f g}
  (hs : CategoryTheory.Limits.IsLimit s) {W : C} (k : W ⟶ X)
  (h : CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.IsLimit.lift hs k h) s.ι = k
-- Mathlib.Topology.EMetricSpace.Defs
MulOpposite.edist_unop : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (x y : αᵐᵒᵖ), edist (MulOpposite.unop x) (MulOpposite.unop y) = edist x y
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_add_le : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  (p : Submodule R M) [inst_6 : RingHomSurjective σ₁₂] (f g : M →ₛₗ[σ₁₂] M₂),
  Submodule.map (f + g) p ≤ Submodule.map f p ⊔ Submodule.map g p
-- Mathlib.Algebra.Free
FreeAddSemigroup.instAddSemigroup : {α : Type u} → AddSemigroup (FreeAddSemigroup α)
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.StructureSheaf.toPushforwardStalk.eq_1 : ∀ {R S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑R),
  AlgebraicGeometry.StructureSheaf.toPushforwardStalk f p =
    CategoryTheory.CategoryStruct.comp
      (CommRingCat.ofHom
        (algebraMap (↑S)
          ((AlgebraicGeometry.structureSheafInType ↑S ↑S).obj.obj
            ((TopologicalSpace.Opens.map (AlgebraicGeometry.Spec.topMap f)).op.obj (Opposite.op ⊤)))))
      (((TopCat.Presheaf.pushforward CommRingCat (AlgebraicGeometry.Spec.topMap f)).obj
            (AlgebraicGeometry.Spec.structureSheaf ↑S).obj).germ
        ⊤ p trivial)
-- Mathlib.CategoryTheory.Adjunction.Quadruple
CategoryTheory.Adjunction.Quadruple.mk.injEq : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C} {G : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor D C} (adj₁ : L ⊣ F) (adj₂ : F ⊣ G) (adj₃ : G ⊣ R) (adj₁_1 : L ⊣ F) (adj₂_1 : F ⊣ G)
  (adj₃_1 : G ⊣ R),
  ({ adj₁ := adj₁, adj₂ := adj₂, adj₃ := adj₃ } = { adj₁ := adj₁_1, adj₂ := adj₂_1, adj₃ := adj₃_1 }) =
    (adj₁ = adj₁_1 ∧ adj₂ = adj₂_1 ∧ adj₃ = adj₃_1)
-- Lean.Meta.Match.MatcherInfo
/-- Parameter structure information for each alternative  -/
Lean.Meta.Match.MatcherInfo.altInfos : Lean.Meta.MatcherInfo → Array Lean.Meta.Match.AltParamInfo
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- Given a graph over a finite vertex type `V` and a proof `hc` that `Fintype.card V = n`,
`G.overFin n` is an isomorphic (as shown in `overFinIso`) graph over `Fin n`.  -/
SimpleGraph.overFin : {V : Type u_1} → SimpleGraph V → [inst : Fintype V] → {n : ℕ} → Fintype.card V = n → SimpleGraph (Fin n)
-- Mathlib.Algebra.CharP.Basic
CharP.charP_iff_prime_eq_zero : ∀ {R : Type u_1} [inst : NonAssocSemiring R] [Nontrivial R] {p : ℕ}, Nat.Prime p → (CharP R p ↔ ↑p = 0)
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
Std.IterM.InternalCombinators.filterMap : {α β γ : Type w} →
  {m : Type w → Type w'} →
    {n : Type w → Type w''} →
      (lift : ⦃α : Type w⦄ → m α → n α) →
        [Std.Iterator α m β] → (f : β → Std.Iterators.PostconditionT n (Option γ)) → Std.IterM m β → Std.IterM n γ
-- Init.Data.Fin.Fold
_private.Init.Data.Fin.Fold.0.Fin.foldr.loop.match_1.eq_1 : ∀ {α : Sort u_2} (n : ℕ) (motive : (x : ℕ) → x ≤ n → α → Sort u_1) (x : 0 ≤ n) (x_1 : α)
  (h_1 : (x : 0 ≤ n) → (x_2 : α) → motive 0 x x_2) (h_2 : (i : ℕ) → (h : i + 1 ≤ n) → (x : α) → motive i.succ h x),
  (match 0, x, x_1 with
    | 0, x, x_2 => h_1 x x_2
    | i.succ, h, x => h_2 i h x) =
    h_1 x x_1
-- Mathlib.GroupTheory.GroupAction.Pointwise
AddGroup.preimage_vadd_setₛₗ : ∀ {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [inst : AddGroup G] [inst_1 : AddGroup H] (σ : G → H)
  [inst_2 : AddAction G α] [inst_3 : AddAction H β] {F : Type u_5} [inst_4 : FunLike F α β]
  [AddActionSemiHomClass F σ α β] (f : F) (c : G) (t : Set β), ⇑f ⁻¹' (σ c +ᵥ t) = c +ᵥ ⇑f ⁻¹' t
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.mem_alter! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k k' : α} {f : Option β → Option β},
      k' ∈ Std.DTreeMap.Internal.Impl.Const.alter! k f t ↔
        if compare k k' = Ordering.eq then (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true else k' ∈ t
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₂.congr_simp : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular] {ι : Type w}
  (D : ι → CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ)
  (hι : HasCardinalLT ι κ) {m : J} (u u_1 : (i : ι) → (D i).top ⟶ m),
  u = u_1 →
    CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₂ D hι u =
      CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₂ D hι u_1
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.IProp.and' : Mathlib.Tactic.ITauto.AndKind → Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.IProp
-- Lean.Data.Json.Basic
Lean.Json.Structured.arr.injEq : ∀ (elems elems_1 : Array Lean.Json),
  (Lean.Json.Structured.arr elems = Lean.Json.Structured.arr elems_1) = (elems = elems_1)
-- Std.Sync.Semaphore
_private.Std.Sync.Semaphore.0.Std.SemaphoreState.permits : Std.SemaphoreState✝ → ℕ
-- Mathlib.Topology.MetricSpace.Infsep
Set.Finite.einfsep : ∀ {α : Type u_1} [inst : EDist α] {s : Set α} (hs : s.Finite), s.einfsep = ⋯.toFinset.inf (Function.uncurry edist)
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.Subtype.instBot : {α : Type u_1} → [inst : MeasurableSpace α] → Bot (Subtype MeasurableSet)
-- Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation
ValueDistribution.Cartan.integrable_integral_norm_cartanKernel : ∀ {f : ℂ → ℂ} {R : ℝ},
  Meromorphic f →
    MeasureTheory.Integrable
      (fun x => ∫ (α : ℝ) in Set.Ioc 0 (2 * Real.pi), ‖ValueDistribution.Cartan.cartanKernel f R α x‖)
      (MeasureTheory.volume.restrict (Set.Ioc 0 (2 * Real.pi)))
-- Mathlib.Analysis.Normed.MulAction
ULift.instNormSMulClass : ∀ {α : Type u_1} {β : Type u_2} [inst : SeminormedRing α] [inst_1 : SeminormedAddGroup β] [inst_2 : SMul α β]
  [NormSMulClass α β], NormSMulClass α (ULift.{u_3, u_2} β)
-- Mathlib.Algebra.Group.WithOne.Map
/-- The image of a binary function `f : α → β → γ` as a function
`WithOne α → WithOne β → WithOne γ`.

Mathematically this should be thought of as the image of the corresponding function `α × β → γ`.  -/
WithOne.map₂ : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → (α → β → γ) → WithOne α → WithOne β → WithOne γ
-- Mathlib.RingTheory.WittVector.MulCoeff
WittVector.nthRemainder_spec : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : CommRing k] [inst_1 : CharP k p] (n : ℕ)
  (x y : WittVector p k),
  (x * y).coeff (n + 1) =
    x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1) + y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) +
      WittVector.nthRemainder p n (WittVector.truncateFun (n + 1) x) (WittVector.truncateFun (n + 1) y)
-- Mathlib.Analysis.Calculus.FDeriv.Basic
differentiableWithinAt_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {x : E} {s : Set E}, DifferentiableWithinAt 𝕜 id s x
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If the sign of the angle between two vectors is nonzero, the second vector is nonzero.  -/
Orientation.right_ne_zero_of_oangle_sign_ne_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, (o.oangle x y).sign ≠ 0 → y ≠ 0
-- Mathlib.Data.List.Sigma
List.nodupKeys_cons : ∀ {α : Type u} {β : α → Type v} {s : Sigma β} {l : List (Sigma β)}, (s :: l).NodupKeys ↔ s.fst ∉ l.keys ∧ l.NodupKeys
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Partial.apply_of_mem_stratum : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed)
  {x : ↥(↑f).domain} {c : FiniteArchimedeanClass M} (hx : ↑x ∈ seed.stratum c),
  ↑↑f x = toLex ((HahnSeries.single c) ((seed.coeff c) ⟨↑x, hx⟩))
-- Mathlib.Order.Category.CompleteLat
CompleteLat.of.sizeOf_spec : ∀ (carrier : Type u_1) [str : CompleteLattice carrier],
  sizeOf { carrier := carrier, str := str } = 1 + sizeOf carrier + sizeOf str
-- Mathlib.Algebra.Ring.Defs
/-- Multiplication is right distributive over addition  -/
Distrib.right_distrib : ∀ {R : Type u_1} [self : Distrib R] (a b c : R), (a + b) * c = a * c + b * c
-- Qq.AssertInstancesCommute
Qq.Impl.findRedundantLocalInst? : Qq.Impl.QuoteM (Option (Lean.FVarId × Lean.Expr))
-- Mathlib.Probability.Martingale.Centering
MeasureTheory.martingalePart_eq_sum : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : ℕ → Ω → E} {ℱ : MeasureTheory.Filtration ℕ m0},
  MeasureTheory.martingalePart f ℱ μ = fun n =>
    f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i - μ[f (i + 1) - f i | ↑ℱ i])
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddResult
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddResult.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.performRatCheck.match_1.splitter : {n : ℕ} →
  (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → Sort u_1) →
    (x : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)) →
      ((c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → motive (some c)) → (Unit → motive none) → motive x
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- Every acyclic subgraph of a connected graph can be extended to a spanning tree.  -/
SimpleGraph.Connected.exists_isTree_le_of_le_of_isAcyclic : ∀ {V : Type u_1} {G H : SimpleGraph V}, G.Connected → H ≤ G → H.IsAcyclic → ∃ F, H ≤ F ∧ F ≤ G ∧ F.IsTree
-- Lean.ReducibilityAttrs
Lean.allowUnsafeReducibility : Lean.Option Bool
-- Mathlib.RingTheory.Polynomial.Eisenstein.Basic
/-- Given an ideal `𝓟` of a commutative semiring `R`, we say that a polynomial `f : R[X]`
is *weakly Eisenstein at `𝓟`* if `∀ n, n < f.natDegree → f.coeff n ∈ 𝓟`.  -/
Polynomial.IsWeaklyEisensteinAt : {R : Type u} → [inst : CommSemiring R] → Polynomial R → Ideal R → Prop
-- Mathlib.Data.Finset.Filter
Finset.filter_mem_eq_of_subset : ∀ {α : Type u_1} {s t : Finset α} [inst : DecidablePred fun x => x ∈ s], s ⊆ t → {x ∈ t | x ∈ s} = s
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicones.functoriality_obj_pt : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type uD} [inst_2 : CategoryTheory.Category.{uD', uD} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (P Q : C) (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms]
  (A : CategoryTheory.Limits.BinaryBicone P Q),
  ((CategoryTheory.Limits.BinaryBicones.functoriality P Q F).obj A).pt = F.obj A.pt
-- Mathlib.Analysis.LocallyConvex.AbsConvex
absConvexHull_eq_convexHull_balancedHull : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {s : Set E}, (absConvexHull 𝕜) s = (convexHull 𝕜) (balancedHull 𝕜 s)
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.dist_eq_sum : ∀ {ι : Type u_2} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → Dist (α i)] {p : ENNReal},
  0 < p.toReal → ∀ (f g : PiLp p α), dist f g = (∑ i, dist (f.ofLp i) (g.ofLp i) ^ p.toReal) ^ (1 / p.toReal)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.hasFiniteProducts_opposite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasFiniteCoproducts C],
  CategoryTheory.Limits.HasFiniteProducts Cᵒᵖ
-- Mathlib.GroupTheory.Congruence.Defs
AddConGen.Rel.refl : ∀ {M : Type u_1} [inst : Add M] {r : M → M → Prop} (x : M), AddConGen.Rel r x x
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.norm_le_one_iff_of_nonneg : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] (a : A),
  autoParam (0 ≤ a) CStarAlgebra.norm_le_one_iff_of_nonneg._auto_1 → (‖a‖ ≤ 1 ↔ a ≤ 1)
-- Mathlib.Tactic.PPWithUniv
/-- Delaborator that prints the current application with universe parameters on the head symbol,
unless `pp.universes` is explicitly set to `false`.
 -/
Mathlib.PPWithUniv.delabWithUniv : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Topology.Order.Hom.Esakia
PseudoEpimorphism.cancel_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  {g₁ g₂ : PseudoEpimorphism β γ} {f : PseudoEpimorphism α β},
  Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.Topology.Irreducible
isIrreducible_iff_irreducibleSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsIrreducible s ↔ IrreducibleSpace ↑s
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.exp_mem_slitPlane : ∀ {z : ℂ}, Complex.exp z ∈ Complex.slitPlane ↔ toIocMod Real.two_pi_pos (-Real.pi) z.im ≠ Real.pi
-- Mathlib.Algebra.Group.Hom.Defs
ZeroHomClass.mk : ∀ {F : Type u_10} {M : outParam (Type u_11)} {N : outParam (Type u_12)} [inst : Zero M] [inst_1 : Zero N]
  [inst_2 : FunLike F M N], (∀ (f : F), f 0 = 0) → ZeroHomClass F M N
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.IsRat.mk : ∀ {α : Type u} [inst : Ring α] {a : α} {num : ℤ} {denom : ℕ} (inv : Invertible ↑denom),
  a = ↑num * ⅟↑denom → Mathlib.Meta.NormNum.IsRat a num denom
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.inf_addSubgroupOf_right : ∀ {G : Type u_1} [inst : AddGroup G] (H K : AddSubgroup G), (H ⊓ K).addSubgroupOf K = H.addSubgroupOf K
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minEntry.induct_unfolding : ∀ {α : Type u} {β : α → Type v}
  (motive : (t : Std.DTreeMap.Internal.Impl α β) → t.isEmpty = false → (a : α) × β a → Prop),
  (∀ (size : ℕ) (k : α) (v : β k) (r : Std.DTreeMap.Internal.Impl α β)
      (x : (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).isEmpty = false),
      (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).isEmpty = false →
        motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x ⟨k, v⟩) →
    (∀ (size : ℕ) (k : α) (v : β k) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1) (l r r_1 : Std.DTreeMap.Internal.Impl α β)
        (h :
          (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r)
                r_1).isEmpty =
            false),
        (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1).isEmpty =
            false →
          motive (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) ⋯
              ((Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r).minEntry ⋯) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1)
              h ((Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r).minEntry ⋯)) →
      ∀ (t : Std.DTreeMap.Internal.Impl α β) (h : t.isEmpty = false), motive t h (t.minEntry h)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.Types.sheafIso_hom_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D}
  {G : CategoryTheory.Functor C D} [inst_2 : G.IsCoverDense K] [inst_3 : G.IsLocallyFull K]
  {ℱ ℱ' : CategoryTheory.Sheaf K (Type v)} (i : G.op.comp ℱ.obj ≅ G.op.comp ℱ'.obj),
  (CategoryTheory.Functor.IsCoverDense.Types.sheafIso i).hom.hom =
    (CategoryTheory.Functor.IsCoverDense.Types.presheafIso i).hom
-- Lean.Elab.PreDefinition.WF.Fix
_private.Lean.Elab.PreDefinition.WF.Fix.0.Lean.Elab.WF.replaceRecApps.loop : (recFnName : Lean.Name) → ℕ → Lean.Expr → Lean.Expr → Lean.Elab.WF.RecM✝ recFnName Lean.Expr
-- Init.Data.SInt.Lemmas
ISize.int64MinValue_le_toInt : ∀ (x : ISize), Int64.minValue.toInt ≤ x.toInt
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
measurable_const : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} {x_1 : MeasurableSpace β} {a : α}, Measurable fun x => a
-- Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily
/-- Up to a measurable equivalence, `projectiveFamily I` is the centered multivariate Gaussian
with covariance matrix `covMatrix I`.  -/
ProbabilityTheory.BrownianReal.measurePreserving_ofLp_multivariateGaussian : ∀ (I : Finset NNReal),
  MeasureTheory.MeasurePreserving WithLp.ofLp
    (ProbabilityTheory.multivariateGaussian 0 (ProbabilityTheory.BrownianReal.covMatrix I))
    (ProbabilityTheory.BrownianReal.projectiveFamily I)
-- Aesop.Util.Basic
Aesop.SimpTheorems.foldSimpEntriesM : {m : Type u_1 → Type u_2} →
  {σ : Type u_1} → [Monad m] → (σ → Lean.Meta.SimpEntry → m σ) → σ → Lean.Meta.SimpTheorems → m σ
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getKey?_modifyKey : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {k k' : α} {f : β → β} (l : List ((_ : α) × β)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKey? k' (Std.Internal.List.Const.modifyKey k f l) =
      if (k == k') = true then if Std.Internal.List.containsKey k l = true then some k else none
      else Std.Internal.List.getKey? k' l
-- Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
/-- In a GCD domain, every invertible fractional ideal is principal.

Public API note: see `ClassGroup.isPrincipal_coeSubmodule_of_isUnit`.  -/
_private.Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup.0.IsGCDMonoid.isPrincipal_fractionalIdeal_of_isUnit : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] [IsGCDMonoid R]
  (I : (FractionalIdeal (nonZeroDivisors R) (FractionRing R))ˣ), (↑↑I).IsPrincipal
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion
SemiNormedGrp.completion.norm_incl_eq : ∀ {V : SemiNormedGrp} {v : V.carrier}, ‖(CategoryTheory.ConcreteCategory.hom SemiNormedGrp.completion.incl) v‖ = ‖v‖
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
/-- An `AlgHom` between two rings restrict to an `AlgHom` between the integral closures inside
them.  -/
AlgHom.mapIntegralClosure : {R : Type u_1} →
  {A : Type u_2} →
    {S : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : CommRing A] →
          [inst_2 : CommRing S] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R S] → (A →ₐ[R] S) → ↥(integralClosure R A) →ₐ[R] ↥(integralClosure R S)
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.jacobian.eq_1 : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.PreSubmersivePresentation R S ι σ) [inst_3 : Finite σ],
  P.jacobian = (algebraMap P.Ring S) (LinearMap.det P.differential)
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.instSubsemiringClass : ∀ (R : Type u_1) [inst : CommRing R], SubsemiringClass (RingPreordering R) R
-- Mathlib.Topology.Algebra.Ring.Basic
ContinuousAddEquiv.mulLeft_apply : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : Semiring R] [inst_2 : IsTopologicalSemiring R] (r : Rˣ) (x : R),
  (ContinuousAddEquiv.mulLeft r) x = ↑r * x
-- Mathlib.Topology.Order.MonotoneConvergence
Antitone.le_of_tendsto : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder α] [OrderClosedTopology α]
  [inst_3 : Preorder β] [IsDirectedOrder β] {f : β → α} {a : α},
  Antitone f → Filter.Tendsto f Filter.atTop (nhds a) → ∀ (b : β), a ≤ f b
-- Mathlib.Algebra.Group.Prod
AddEquiv.prodComm.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  AddEquiv.prodComm = { toEquiv := Equiv.prodComm M N, map_add' := ⋯ }
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.stmts₁.eq_5 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (x : Turing.TM1.Stmt Γ Λ σ),
  (∀ (a : Turing.Dir) (q : Turing.TM1.Stmt Γ Λ σ), x = Turing.TM1.Stmt.move a q → False) →
    (∀ (a : Γ → σ → Γ) (q : Turing.TM1.Stmt Γ Λ σ), x = Turing.TM1.Stmt.write a q → False) →
      (∀ (a : Γ → σ → σ) (q : Turing.TM1.Stmt Γ Λ σ), x = Turing.TM1.Stmt.load a q → False) →
        (∀ (a : Γ → σ → Bool) (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ), x = Turing.TM1.Stmt.branch a q₁ q₂ → False) →
          Turing.TM1.stmts₁ x = {x}
-- Mathlib.Algebra.Order.GroupWithZero.Defs
/-- Typeclass for reverse monotonicity of multiplication by positive elements on the right,
namely `a₁ * b ≤ a₂ * b → a₁ ≤ a₂` if `0 < b`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`IsStrictOrderedRing`.  -/
MulPosReflectLE : (α : Type u_1) → [Mul α] → [Zero α] → [Preorder α] → Prop
-- Mathlib.RingTheory.MatrixPolynomialAlgebra
matPolyEquiv_coeff_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type w} [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  (m : Matrix n n (Polynomial R)) (k : ℕ) (i j : n), (matPolyEquiv m).coeff k i j = (m i j).coeff k
-- Mathlib.AlgebraicGeometry.Limits
/-- `Spec ℤ` is the terminal object in the category of schemes.  -/
AlgebraicGeometry.specULiftZIsTerminal : CategoryTheory.Limits.IsTerminal (AlgebraicGeometry.Spec (CommRingCat.of (ULift.{u, 0} ℤ)))
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minView_tree_impl_eq_minView! : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} {hl : l.Balanced}
  {hr : r.Balanced} {hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size},
  (Std.DTreeMap.Internal.Impl.minView k v l r hl hr hlr).tree.impl = (Std.DTreeMap.Internal.Impl.minView! k v l r).tree
-- Mathlib.RingTheory.SimpleModule.WedderburnArtin
/-- The **Wedderburn–Artin Theorem**: an Artinian simple ring is isomorphic to a matrix
ring over a division ring.  -/
IsSimpleRing.exists_ringEquiv_matrix_divisionRing : ∀ (R : Type u) [inst : Ring R] [IsSimpleRing R] [IsArtinianRing R],
  ∃ n, ∃ (_ : NeZero n), ∃ D x, Nonempty (R ≃+* Matrix (Fin n) (Fin n) D)
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.GuessLexRel.eq.sizeOf_spec : sizeOf Lean.Elab.WF.GuessLex.GuessLexRel.eq = 1
-- Mathlib.Algebra.Order.Ring.GeomSum
geom_sum_neg_iff : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {n : ℕ} {x : R},
  n ≠ 0 → (∑ i ∈ Finset.range n, x ^ i < 0 ↔ Even n ∧ x + 1 < 0)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.mulAction'.eq_1 : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] [inst_2 : Monoid S]
  [inst_3 : SMul S R] [inst_4 : MulAction S M] [inst_5 : IsScalarTower S R M] (p : SubMulAction R M),
  p.mulAction' = { toSMul := p.smul', mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.RepresentationTheory.Induced
Rep.indResHomEquiv_symm_apply : ∀ {k : Type u} {G : Type v} {H : Type v'} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] (φ : G →* H)
  (A : Rep.{max w v' u, u, v} k G) (B : Rep.{max w v' u, u, v'} k H) (f : A ⟶ Rep.res φ B),
  (Rep.indResHomEquiv φ A B).symm f =
    Rep.ofHom
      {
        toLinearMap :=
          Representation.Coinvariants.lift
            (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
            (TensorProduct.lift
              (((Finsupp.lift (↑A →ₗ[k] ↑B) k H) fun h => B.ρ h⁻¹ ∘ₗ (Rep.Hom.hom f).toLinearMap) ∘ₗ
                ↑(MonoidAlgebra.coeffLinearEquiv k)))
            ⋯,
        isIntertwining' := ⋯ }
-- Init.Data.Int.Order
Int.neg_of_mul_pos_left : ∀ {a b : ℤ}, 0 < a * b → b < 0 → a < 0