mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Integral.IntegrableOn
ContinuousOn.integrableAt_nhdsWithin : ∀ {α : Type u_1} {E : Type u_5} {mα : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : TopologicalSpace α]
  [SecondCountableTopologyEither α E] [OpensMeasurableSpace α] {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsLocallyFiniteMeasure μ] {a : α} {t : Set α} {f : α → E},
  ContinuousOn f t → MeasurableSet t → a ∈ t → MeasureTheory.IntegrableAtFilter f (nhdsWithin a t) μ
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteElement.neg_mk : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] {x : K}
  (h : 0 ≤ ArchimedeanClass.mk x), -ArchimedeanClass.FiniteElement.mk x h = ArchimedeanClass.FiniteElement.mk (-x) ⋯
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.mapGlueData_V : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [inst_1 : CategoryTheory.Category.{v, u₂} C']
  (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C')
  [inst_2 : ∀ (i j k : D.J), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F]
  (i : D.J × D.J), (D.mapGlueData F).V i = F.obj (D.V i)
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.TerminationHints.mk : Lean.Syntax →
  Option Lean.Syntax →
    Option Lean.Elab.TerminationBy →
      Option Lean.Elab.PartialFixpoint → Option Lean.Elab.DecreasingBy → ℕ → Lean.Elab.TerminationHints
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.RightResolution.hw : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  (self : Φ.RightResolution X₂), W₂ self.w
-- Mathlib.Algebra.Group.Action.Opposite
Monoid.toOppositeMulAction.eq_1 : ∀ {α : Type u_3} [inst : Monoid α],
  Monoid.toOppositeMulAction = { toSMul := Mul.toSMulMulOpposite α, mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_bot_top : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : BoundedOrder α], Set.Icc ⊥ ⊤ = Set.univ
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
DirichletCharacter.LFunction.congr_simp : ∀ {N : ℕ} [inst : NeZero N] (χ χ_1 : DirichletCharacter ℂ N),
  χ = χ_1 → ∀ (s s_1 : ℂ), s = s_1 → DirichletCharacter.LFunction χ s = DirichletCharacter.LFunction χ_1 s_1
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.instAlgebra_1 : (K : Type u_1) → [inst : Field K] → Algebra (NumberField.RingOfIntegers K) K
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
SimpleGraph.instDecidableRelSumAdjBipartiteDoubleCover : {V : Type u_1} → {G : SimpleGraph V} → [h : DecidableRel G.Adj] → DecidableRel G.bipartiteDoubleCover.Adj
-- Mathlib.Data.Seq.Computation
/-- `empty α` is the computation that never returns, an infinite sequence of
`think`s.  -/
Computation.empty : (α : Type u_1) → Computation α
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- **Chinese remainder theorem**, specialized to two ideals.  -/
Ideal.quotientMulEquivQuotientProd : {R : Type u_2} → [inst : CommRing R] → (I J : Ideal R) → IsCoprime I J → R ⧸ I * J ≃+* (R ⧸ I) × R ⧸ J
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toArray_rco_eq_add : ∀ {m n i fallback : ℕ}, i < n - m → (m...n).toArray.getD i fallback = m + i
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.CoextendScalars.distribMulAction : {R : Type u₁} →
  {S : Type u₂} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        (f : R →+* S) →
          (M : Type v) →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : Module R M] →
                DistribMulAction S (↑((ModuleCat.restrictScalars f).obj (ModuleCat.of S S)) →ₗ[R] M)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.HasLeftHomology.of_zeros : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (X Y Z : C), { X₁ := X, X₂ := Y, X₃ := Z, f := 0, g := 0, zero := ⋯ }.HasLeftHomology
-- Mathlib.Order.Hom.Bounded
BotHom.inf_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Bot α] [inst_1 : SemilatticeInf β] [inst_2 : OrderBot β] (f g : BotHom α β)
  (a : α), (f ⊓ g) a = f a ⊓ g a
-- Mathlib.Order.Filter.Pointwise
Filter.map_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {f : Filter β} {a : α}, Filter.map (fun b => a • b) f = a • f
-- Mathlib.Data.Fin.VecNotation
Matrix.vecAppend.congr_simp : ∀ {m n : ℕ} {α : Type u_1} {o : ℕ} (ho : o = m + n) (u u_1 : Fin m → α),
  u = u_1 →
    ∀ (v v_1 : Fin n → α),
      v = v_1 → ∀ (a a_1 : Fin o), a = a_1 → Matrix.vecAppend ho u v a = Matrix.vecAppend ho u_1 v_1 a_1
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- Writing explicitly the `n+1`-th derivative as the composition of a currying linear equiv,
and the `n`-th derivative of the derivative.  -/
iteratedFDeriv_succ_eq_comp_right : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {n : ℕ},
  iteratedFDeriv 𝕜 (n + 1) f x =
    (⇑(continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm ∘ iteratedFDeriv 𝕜 n fun y => fderiv 𝕜 f y) x
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.tendsto_measure_biUnion_Ici_zero_of_pairwise_disjoint : ∀ {X : Type u_5} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ]
  {Es : ℕ → Set X},
  (∀ (i : ℕ), MeasureTheory.NullMeasurableSet (Es i) μ) →
    (Pairwise fun n m => Disjoint (Es n) (Es m)) →
      Filter.Tendsto (⇑μ ∘ fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i) Filter.atTop (nhds 0)
-- Mathlib.Analysis.RCLike.Basic
/-- Imaginary unit in `K`. Meant to be set to `0` for `K = ℝ`.  -/
RCLike.I : {K : semiOutParam (Type u_1)} → [self : RCLike K] → K
-- Mathlib.Algebra.Group.Center
Set.mul_mem_centralizer : ∀ {M : Type u_1} {S : Set M} [inst : Semigroup M] {a b : M},
  a ∈ S.centralizer → b ∈ S.centralizer → a * b ∈ S.centralizer
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.GuessLexRel.no_idea : Lean.Elab.WF.GuessLex.GuessLexRel
-- Lean.Attributes
Lean.AttributeExtensionOLeanEntry.builderId : Lean.AttributeExtensionOLeanEntry → Lean.Name
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.not_mem_emptyWithCapacity : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {a : α} {c : ℕ},
  a ∉ Std.HashMap.Raw.emptyWithCapacity c
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.id_apply : ∀ {α : Type u_2} [inst : OmegaCompletePartialOrder α] (a : α), OmegaCompletePartialOrder.ContinuousHom.id a = a
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.argPartialEquiv_apply : ↑Circle.argPartialEquiv = Complex.arg ∘ Subtype.val
-- Mathlib.Topology.Algebra.ConstMulAction
/-- The quotient of a second countable space by an additive group action is second
countable.  -/
ContinuousConstVAdd.secondCountableTopology : ∀ {Γ : Type u_4} [inst : AddGroup Γ] {T : Type u_5} [inst_1 : TopologicalSpace T] [inst_2 : AddAction Γ T]
  [SecondCountableTopology T] [ContinuousConstVAdd Γ T], SecondCountableTopology (Quotient (AddAction.orbitRel Γ T))
-- Mathlib.Order.Filter.Map
Filter.comap_neBot : ∀ {α : Type u_1} {β : Type u_2} {f : Filter β} {m : α → β}, (∀ t ∈ f, ∃ a, m a ∈ t) → (Filter.comap m f).NeBot
-- Init.Data.SInt.Lemmas
Int16.pow_zero : ∀ (x : Int16), x ^ 0 = 1
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- Mapping from Lean expressions to their representations as `SemiringExpr`  -/
Lean.Meta.Grind.Arith.CommRing.Semiring.denote : Lean.Meta.Grind.Arith.CommRing.Semiring →
  Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Grind.Arith.CommRing.SemiringExpr
-- Aesop.Script.StructureDynamic
_private.Aesop.Script.StructureDynamic.0.Aesop.Script.structureDynamicCore.goUnstructured : Lean.MVarId →
  Lean.Meta.SavedState → Array Lean.MVarId → Aesop.Script.DynStructureM (Option Aesop.Script.DynStructureResult)
-- Init.Data.Vector.Lemmas
Vector.exists_mem_of_size_pos : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n}, 0 < n → ∃ x, x ∈ xs
-- Mathlib.Topology.Algebra.Monoid
ContinuousAt.nsmul : ∀ {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M] [inst_2 : AddMonoid M]
  [ContinuousAdd M] {f : X → M} {x : X}, ContinuousAt f x → ∀ (n : ℕ), ContinuousAt (n • f) x
-- Init.Data.SInt.Basic
/-- Bitwise exclusive or for 32-bit signed integers. Usually accessed via the `^^^` operator.

Each bit of the resulting integer is set if exactly one of the corresponding bits of the input
integers is set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.
 -/
Int32.xor : Int32 → Int32 → Int32
-- Lean.Setup
/-- Whether to activate this import when the current module itself is imported.  -/
Lean.Import.isExported : Lean.Import → Bool
-- Mathlib.Analysis.SpecialFunctions.Log.ERealExp
EReal.exp_top : ⊤.exp = ⊤
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
/-- The partial derivative `W_Z(X, Y, Z)` with respect to `Z` of the polynomial `W(X, Y, Z)`
associated to a Weierstrass curve `W` in projective coordinates.  -/
WeierstrassCurve.Projective.polynomialZ : {R : Type r} → [inst : CommRing R] → WeierstrassCurve.Projective R → MvPolynomial (Fin 3) R
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.coe_inf : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Min β] (f g : MeasureTheory.SimpleFunc α β),
  ⇑(f ⊓ g) = ⇑f ⊓ ⇑g
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.findEntry? : Lean.Expr → Lean.Meta.SynthInstance.SynthM (Option Lean.Meta.SynthInstance.TableEntry)
-- Mathlib.Data.Finsupp.MonomialOrder
MonomialOrder.mk.injEq : ∀ {σ : Type u_1} (syn : Type u_2)
  (addCommMonoidSyn : autoParam (AddCommMonoid syn) MonomialOrder.addCommMonoidSyn._autoParam)
  (linearOrderSyn : autoParam (LinearOrder syn) MonomialOrder.linearOrderSyn._autoParam)
  (isOrderedAddMonoid_syn : autoParam (IsOrderedAddMonoid syn) MonomialOrder.isOrderedAddMonoid_syn._autoParam)
  (toSyn : (σ →₀ ℕ) ≃+ syn) (toSyn_monotone : Monotone ⇑toSyn)
  (wellFoundedLT_syn : autoParam (WellFoundedLT syn) MonomialOrder.wellFoundedLT_syn._autoParam) (syn_1 : Type u_2)
  (addCommMonoidSyn_1 : autoParam (AddCommMonoid syn_1) MonomialOrder.addCommMonoidSyn._autoParam)
  (linearOrderSyn_1 : autoParam (LinearOrder syn_1) MonomialOrder.linearOrderSyn._autoParam)
  (isOrderedAddMonoid_syn_1 : autoParam (IsOrderedAddMonoid syn_1) MonomialOrder.isOrderedAddMonoid_syn._autoParam)
  (toSyn_1 : (σ →₀ ℕ) ≃+ syn_1) (toSyn_monotone_1 : Monotone ⇑toSyn_1)
  (wellFoundedLT_syn_1 : autoParam (WellFoundedLT syn_1) MonomialOrder.wellFoundedLT_syn._autoParam),
  ({ syn := syn, addCommMonoidSyn := addCommMonoidSyn, linearOrderSyn := linearOrderSyn,
        isOrderedAddMonoid_syn := isOrderedAddMonoid_syn, toSyn := toSyn, toSyn_monotone := toSyn_monotone,
        wellFoundedLT_syn := wellFoundedLT_syn } =
      { syn := syn_1, addCommMonoidSyn := addCommMonoidSyn_1, linearOrderSyn := linearOrderSyn_1,
        isOrderedAddMonoid_syn := isOrderedAddMonoid_syn_1, toSyn := toSyn_1, toSyn_monotone := toSyn_monotone_1,
        wellFoundedLT_syn := wellFoundedLT_syn_1 }) =
    (syn = syn_1 ∧ addCommMonoidSyn ≍ addCommMonoidSyn_1 ∧ linearOrderSyn ≍ linearOrderSyn_1 ∧ toSyn ≍ toSyn_1)
-- Mathlib.Analysis.Convex.Gauge
gauge_smul_left_of_nonneg : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {α : Type u_3} [inst_2 : Field α]
  [inst_3 : LinearOrder α] [IsStrictOrderedRing α] [inst_5 : MulActionWithZero α ℝ] [IsStrictOrderedModule α ℝ]
  [inst_7 : MulActionWithZero α E] [SMulCommClass α ℝ ℝ] [IsScalarTower α ℝ ℝ] [IsScalarTower α ℝ E] {s : Set E}
  {a : α}, 0 ≤ a → gauge (a • s) = a⁻¹ • gauge s
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.RightHomologyData.exact_iff_mono_g' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} [S.HasHomology] (h : S.RightHomologyData), S.Exact ↔ CategoryTheory.Mono h.g'
-- Mathlib.Analysis.SpecialFunctions.Arsinh
ContinuousWithinAt.arsinh : ∀ {X : Type u_1} [inst : TopologicalSpace X] {f : X → ℝ} {s : Set X} {a : X},
  ContinuousWithinAt f s a → ContinuousWithinAt (fun x => Real.arsinh (f x)) s a
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.mul.congr_simp : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k_1 k_2 : ℤ} [inst : Γ.HasDetPlusMinusOne] (f f_1 : ModularForm Γ k_1),
  f = f_1 → ∀ (g g_1 : ModularForm Γ k_2), g = g_1 → f.mul g = f_1.mul g_1
-- Lean.Elab.App
/-- When applied to `f`, effectively expands to `constName ... (Struct.toBase f)`, with the argument placed in the correct
positional argument if possible, or otherwise as a named argument. The `Struct.toBase` is not present if `baseStructName == structName`,
in which case these do not need to be structures. Supports generalized field notation.  -/
Lean.Elab.Term.LValResolution.const : Lean.Name → Lean.Name → Lean.Name → List Lean.Level → Lean.Elab.Term.LValResolution
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoidClass.toAddMemClass : ∀ {S : Type u_3} {M : outParam (Type u_4)} {inst : AddZeroClass M} {inst_1 : SetLike S M}
  [self : AddSubmonoidClass S M], AddMemClass S M
-- Init.Data.Nat.Lcm
Nat.lcm_dvd_lcm_mul_left_left : ∀ (m n k : ℕ), m.lcm n ∣ (k * m).lcm n
-- Lean.Meta.ArgsPacker
Lean.Meta.ArgsPacker.Mutual.uncurry : Array Lean.Expr → Lean.MetaM Lean.Expr
-- Lean.Elab.PreDefinition.FixedParams
Lean.Elab.FixedParams.Info.mk : Array (Array (Option (Array (Option ℕ)))) → Array (Array (Array ℕ)) → Lean.Elab.FixedParams.Info
-- Mathlib.Topology.Separation.Hausdorff
t2_iff_isClosed_diagonal : ∀ {X : Type u_1} [inst : TopologicalSpace X], T2Space X ↔ IsClosed (Set.diagonal X)
-- Mathlib.RingTheory.KrullDimension.Regular
/-- [Stacks Tag 0B52](https://stacks.math.columbia.edu/tag/0B52) (the equality case) -/
Module.supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_maximalIdeal : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] {M : Type u_2} [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [Module.Finite R M] [inst_5 : IsLocalRing R] {x : R},
  (∀ p ∈ (Module.annihilator R M).minimalPrimes, x ∉ p) →
    x ∈ IsLocalRing.maximalIdeal R → Module.supportDim R (QuotSMulTop x M) + 1 = Module.supportDim R M
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearEquiv.rTensor_trans_congr : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : AddCommMonoid S] [inst_6 : Module R M] [inst_7 : Module R N] [inst_8 : Module R S] [inst_9 : Module R P]
  [inst_10 : Module R Q] (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) (f' : S ≃ₗ[R] M),
  LinearEquiv.rTensor N f' ≪≫ₗ TensorProduct.congr f g = TensorProduct.congr (f' ≪≫ₗ f) g
-- Std.Sat.AIG.Relabel
Std.Sat.AIG.Decl.relabel_false : ∀ {α β : Type} {idx : ℕ} {decls : Array (Std.Sat.AIG.Decl α)} {r : α → β} {hidx : idx < decls.size},
  Std.Sat.AIG.Decl.relabel r decls[idx] = Std.Sat.AIG.Decl.false → decls[idx] = Std.Sat.AIG.Decl.false
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.inclusion.eq_1 : ∀ {M : Type u_1} {α : Type u_2} [inst : Monoid M] [inst_1 : MulAction M α] (s : SubMulAction M α),
  s.inclusion = { toFun := Subtype.val, map_smul' := ⋯ }
-- Lean.Environment
_private.Lean.Environment.0.Lean.Kernel.Environment.markQuotInit : Lean.Kernel.Environment → Lean.Kernel.Environment
-- Mathlib.Combinatorics.Graph.Basic
Graph.isLink_comm : ∀ {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β}, G.IsLink e x y ↔ G.IsLink e y x
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_injective : ∀ {K : Type u_1} [inst : RCLike K], Function.Injective RCLike.ofReal
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.kernelSubobject_arrow_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobject f).arrow
      (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Algebra.Algebra.Subalgebra.Directed
Subalgebra.iSupLift_of_mem : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] {ι : Type u_4} [inst_5 : Nonempty ι] (K : ι → Subalgebra R A)
  {dir : Directed (fun x1 x2 => x1 ≤ x2) K} {f : (i : ι) → ↥(K i) →ₐ[R] B}
  {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (Subalgebra.inclusion h)} {T : Subalgebra R A} {hT : T ≤ iSup K}
  {i : ι} (x : ↥T) (hx : ↑x ∈ K i), (Subalgebra.iSupLift K dir f hf T hT) x = (f i) ⟨↑x, hx⟩
-- Mathlib.RingTheory.WittVector.WittPolynomial
wittPolynomial_vars : ∀ (p : ℕ) (R : Type u_1) [inst : CommRing R] [hp : NeZero p] [CharZero R] (n : ℕ),
  (wittPolynomial p R n).vars = Finset.range (n + 1)
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
CategoryTheory.Over.conePost_map_hom : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) (i : J) {X Y : CategoryTheory.Limits.Cone F} (f : X ⟶ Y),
  ((CategoryTheory.Over.conePost F i).map f).hom = CategoryTheory.Over.homMk f.hom ⋯
-- Mathlib.Algebra.Order.Kleene
mul_kstar_le_self : ∀ {α : Type u_1} [inst : KleeneAlgebra α] {a b : α}, b * a ≤ b → b * KStar.kstar a ≤ b
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.AbelianStruct.fac_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  {f : X ⟶ Y} (self : CategoryTheory.Abelian.AbelianStruct f) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.imageπ (CategoryTheory.CategoryStruct.comp self.imageι h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.OuterMeasure.pi_pi_le : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] (m : (i : ι) → MeasureTheory.OuterMeasure (α i))
  (s : (i : ι) → Set (α i)), (MeasureTheory.OuterMeasure.pi m) (Set.univ.pi s) ≤ ∏ i, (m i) (s i)
-- Init.Data.Range.Polymorphic.Nat
Std.PRange.instLawfulUpwardEnumerableLeast?Nat : Std.PRange.LawfulUpwardEnumerableLeast? ℕ
-- Init.Data.Nat.Bitwise.Lemmas
Nat.shiftRight_bitwise_distrib : ∀ {f : Bool → Bool → Bool} {i a b : ℕ},
  autoParam (f false false = false) Nat.shiftRight_bitwise_distrib._auto_5 →
    Nat.bitwise f a b >>> i = Nat.bitwise f (a >>> i) (b >>> i)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RoiSliceData.range : {α : Type u} → {β : α → Type v} → [inst : Ord α] → Std.DTreeMap.Internal.RoiSliceData α β → Std.Roi α
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.ιNormalizedChainComplex_fromNormalizedChainComplex_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) {R : C} {n : ℕ} (x : X.obj (Opposite.op { len := n })),
  CategoryTheory.CategoryStruct.comp (X.ιNormalizedChainComplex x) ((X.fromNormalizedChainComplex R).f n) =
    CategoryTheory.CategoryStruct.comp (X.ιChainComplex x) (AlgebraicTopology.DoldKan.PInfty.f n)
-- Mathlib.Algebra.Group.Action.Basic
/-- Scalar multiplication by `r` as a `MonoidHom`.  -/
MulDistribMulAction.toMonoidHom : {M : Type u_2} → (A : Type u_3) → [inst : Monoid M] → [inst_1 : Monoid A] → [MulDistribMulAction M A] → M → A →* A
-- Lean.Util.Path
/-- If the package of `mod` can be found in `sp`, return the path with extension
`ext` (`lean` or `olean`) corresponding to `mod`. Otherwise, return `none`. Does
not check whether the returned path exists.  -/
Lean.SearchPath.findWithExt : Lean.SearchPath → String → Lean.Name → IO (Option System.FilePath)
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.measurable_join : ∀ {α : Type u_1} {mα : MeasurableSpace α}, Measurable MeasureTheory.Measure.join
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithInitial.map.match_1.splitter : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    (motive : (X Y : CategoryTheory.WithInitial C) → (X ⟶ Y) → Sort u_3) →
      (X Y : CategoryTheory.WithInitial C) →
        (f : X ⟶ Y) →
          ((a a_1 : C) →
              (f : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of a_1) →
                motive (CategoryTheory.WithInitial.of a) (CategoryTheory.WithInitial.of a_1) f) →
            ((a : C) →
                (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.of a) →
                  motive CategoryTheory.WithInitial.star (CategoryTheory.WithInitial.of a) x) →
              ((x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.star) →
                  motive CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star x) →
                motive X Y f
-- Lean.Server.CodeActions.Attr
Lean.CodeAction.instInhabitedCommandCodeActions.default : Lean.CodeAction.CommandCodeActions
-- Mathlib.Analysis.Normed.Ring.Basic
nnnorm_natAbs : ∀ {α : Type u_2} [inst : SeminormedRing α] (z : ℤ), ‖↑z.natAbs‖₊ = ‖↑z‖₊
-- Mathlib.Order.Partition.Finpartition
/-- A setoid over a finite type induces a finpartition of the type's elements,
where the parts are the setoid's equivalence classes.  -/
Finpartition.ofSetoid : {α : Type u_1} →
  [inst : DecidableEq α] → [inst_1 : Fintype α] → (s : Setoid α) → [DecidableRel ⇑s] → Finpartition Finset.univ
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesOnBall.congr : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal},
  HasFPowerSeriesOnBall f p x r → Set.EqOn f g (Metric.eball x r) → HasFPowerSeriesOnBall g p x r
-- Mathlib.GroupTheory.GroupAction.Primitive
/-- A pretransitive action on a nontrivial type is preprimitive iff
the set of blocks containing a given element is a simple order  -/
AddAction.isSimpleOrder_blockMem_iff_isPreprimitive : ∀ (G : Type u_3) [inst : AddGroup G] {X : Type u_4} [inst_1 : AddAction G X] [AddAction.IsPretransitive G X]
  [Nontrivial X] (a : X), IsSimpleOrder (AddAction.BlockMem G a) ↔ AddAction.IsPreprimitive G X
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
SemiNormedGrp₁.Hom.Simps.hom : (M N : SemiNormedGrp₁) → M.Hom N → NormedAddGroupHom M.carrier N.carrier
-- Init.Data.String.Lemmas.Basic
String.Slice.startPos.eq_1 : ∀ (s : String.Slice), s.startPos = { offset := 0, isValidForSlice := ⋯ }
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.contains_of_contains_insertIfNew : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β},
  (m.insertIfNew k v).contains a = true → (k == a) = false → m.contains a = true
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- Taking the multiequalizer over the multicospan index is equivalent to taking the equalizer over
the two morphisms `∏ᶜ I.left ⇉ ∏ᶜ I.right`. This is the diagram of the latter.
 -/
CategoryTheory.Limits.MulticospanIndex.parallelPairDiagram : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MulticospanShape} →
      (I : CategoryTheory.Limits.MulticospanIndex J C) →
        [CategoryTheory.Limits.HasProduct I.left] →
          [CategoryTheory.Limits.HasProduct I.right] →
            CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.isIso_of_coyoneda_map_bijective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y),
  (∀ (T : C), Function.Bijective fun x => CategoryTheory.CategoryStruct.comp f x) → CategoryTheory.IsIso f