mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_single_eq_same : ∀ {n : Type u_10} {α : Type u_12} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : AddCommMonoid α] (i : n)
  (c : α), (Matrix.single i i c).trace = c
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneOfCoconeRightOp.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ C} (c : CategoryTheory.Limits.Cocone F.rightOp),
  CategoryTheory.Limits.coneOfCoconeRightOp c =
    { pt := Opposite.unop c.pt, π := CategoryTheory.NatTrans.removeRightOp c.ι }
-- Lean.Parser.Command
/-- Displays all available tactic tags, with documentation.
 -/
Lean.Parser.Command.printTacTags : Lean.Parser.Parser
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous
/-- The pullback functor on sheaves of modules can be described as a composition
of the forget functor to presheaves, the pullback on presheaves of modules, and
the sheafification functor.  -/
SheafOfModules.pullbackIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : CategoryTheory.GrothendieckTopology C} →
          {K : CategoryTheory.GrothendieckTopology D} →
            {F : CategoryTheory.Functor C D} →
              {S : CategoryTheory.Sheaf J RingCat} →
                {R : CategoryTheory.Sheaf K RingCat} →
                  [inst_2 : F.IsContinuous J K] →
                    (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) →
                      [inst_3 : (PresheafOfModules.pushforward φ.hom).IsRightAdjoint] →
                        [inst_4 : CategoryTheory.HasWeakSheafify K AddCommGrpCat] →
                          [inst_5 : K.WEqualsLocallyBijective AddCommGrpCat] →
                            SheafOfModules.pullback φ ≅
                              (SheafOfModules.forget S).comp
                                ((PresheafOfModules.pullback φ.hom).comp
                                  (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id R.obj)))
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
/-- See `eLpNorm_smul_measure_of_ne_zero'` for a version with scalar multiplication by `ℝ≥0`.  -/
MeasureTheory.eLpNorm_smul_measure_of_ne_zero : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {ε : Type u_7} [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε]
  {c : ENNReal},
  c ≠ 0 →
    ∀ (f : α → ε) (p : ENNReal) (μ : MeasureTheory.Measure α),
      MeasureTheory.eLpNorm f p (c • μ) = c ^ (1 / p).toReal • MeasureTheory.eLpNorm f p μ
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.mem_roots_sub_C' : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R} {a x : R},
  x ∈ (p - Polynomial.C a).roots ↔ p ≠ Polynomial.C a ∧ Polynomial.eval x p = a
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.toPlots_iInf : ∀ {X : Type u_1} {ι : Type u_2} {D : ι → DiffeologicalSpace X}, (⨅ i, D i).toPlots = ⋂ i, (D i).toPlots
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
/-- The value of the Infimum of a nonempty family of outer measures on a set is not simply
the minimum value of a measure on that set: it is the infimum sum of measures of countable set of
sets that covers that set, where a different measure can be used for each set in the cover.  -/
MeasureTheory.OuterMeasure.iInf_apply : ∀ {α : Type u_1} {ι : Sort u_2} [Nonempty ι] (m : ι → MeasureTheory.OuterMeasure α) (s : Set α),
  (⨅ i, m i) s = ⨅ t, ⨅ (_ : s ⊆ Set.iUnion t), ∑' (n : ℕ), ⨅ i, (m i) (t n)
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.card_biUnion_lt_iff_forall_of_isRegular : ∀ {c : Cardinal.{u}} {α β : Type u} {s : Set α} {t : (a : α) → a ∈ s → Set β},
  c.IsRegular →
    Cardinal.mk ↑s < c →
      (Cardinal.mk ↑(⋃ a, ⋃ (h : a ∈ s), t a h) < c ↔ ∀ (a : α) (ha : a ∈ s), Cardinal.mk ↑(t a ha) < c)
-- Mathlib.Algebra.Exact.Basic
AddMonoidHom.exact_of_comp_of_mem_range : ∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} [inst : AddGroup M] [inst_1 : AddGroup N] [inst_2 : AddGroup P]
  {f : M →+ N} {g : N →+ P}, g.comp f = 0 → (∀ (x : N), g x = 0 → x ∈ f.range) → Function.Exact ⇑f ⇑g
-- Mathlib.Algebra.BigOperators.Finprod
/-- A more general version of `MonoidHom.map_finprod_mem` that requires `s ∩ mulSupport f` rather
than `s` to be finite.  -/
MonoidHom.map_finprod_mem' : ∀ {α : Type u_1} {M : Type u_5} {N : Type u_6} [inst : CommMonoid M] [inst_1 : CommMonoid N] {s : Set α} {f : α → M}
  (g : M →* N), (s ∩ Function.mulSupport f).Finite → g (∏ᶠ (j : α) (_ : j ∈ s), f j) = ∏ᶠ (i : α) (_ : i ∈ s), g (f i)
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepSets_iff : ∀ {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  (hm' : m' ≤ mΩ) (π : ι → Set (Set Ω)),
  (∀ (i : ι), ∀ s ∈ π i, MeasurableSet s) →
    ∀ (μ : MeasureTheory.Measure Ω) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
      ProbabilityTheory.iCondIndepSets m' hm' π μ ↔
        ∀ (s : Finset ι) {f : ι → Set Ω},
          (∀ i ∈ s, f i ∈ π i) →
            μ[(⋂ i ∈ s, f i).indicator fun ω => 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i).indicator fun ω => 1 | m']
-- Lean.Meta.Tactic.Grind.EMatchAction
_private.Lean.Meta.Tactic.Grind.EMatchAction.0.Lean.Meta.Grind.Action.CollectState.collectedThms : Lean.Meta.Grind.Action.CollectState✝ → Std.HashSet (Lean.Meta.Grind.Origin × Lean.Meta.Grind.EMatchTheoremKind)
-- Init.Prelude
/-- Throw an `unsupportedSyntax` exception.  -/
Lean.Macro.throwUnsupported : {α : Type} → Lean.MacroM α
-- Mathlib.AlgebraicGeometry.ColimitsOver
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.mk.injEq : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  {S : AlgebraicGeometry.Scheme} {J : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} J]
  {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover} [inst_2 : CategoryTheory.Category.{v_3, u_2} 𝒰.I₀]
  [inst_3 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  (cocone :
    (i : 𝒰.I₀) → CategoryTheory.Limits.Cocone (D.comp (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (𝒰.f i))))
  (isColimit : (i : 𝒰.I₀) → CategoryTheory.Limits.IsColimit (cocone i))
  (prop_trans : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), P (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij))
  (cocone_1 :
    (i : 𝒰.I₀) → CategoryTheory.Limits.Cocone (D.comp (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (𝒰.f i))))
  (isColimit_1 : (i : 𝒰.I₀) → CategoryTheory.Limits.IsColimit (cocone_1 i))
  (prop_trans_1 : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), P (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij)),
  ({ cocone := cocone, isColimit := isColimit, prop_trans := prop_trans } =
      { cocone := cocone_1, isColimit := isColimit_1, prop_trans := prop_trans_1 }) =
    (cocone = cocone_1 ∧ isColimit ≍ isColimit_1)
-- Mathlib.Computability.RE
REPred.of_eq : ∀ {α : Type u_1} [inst : Primcodable α] {p q : α → Prop}, REPred p → (∀ (a : α), p a ↔ q a) → REPred q
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instToJsonServerCapabilities : Lean.ToJson Lean.Lsp.ServerCapabilities
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.lift.congr_simp : ∀ {X Y : SSet} (f f_1 : X ⟶ Y) (e_f : f = f_1) {B : Y.Subcomplex} (hf : SSet.Subcomplex.range f ≤ B),
  SSet.Subcomplex.lift f hf = SSet.Subcomplex.lift f_1 ⋯
-- Mathlib.Condensed.TopCatAdjunction
CondensedSet.instEpiTopCatAppCounitTopCatAdjunction : ∀ (X : TopCat), CategoryTheory.Epi (CondensedSet.topCatAdjunction.counit.app X)
-- Mathlib.Topology.VectorBundle.Riemannian
/-- A family of inner product space structures on the fibers of a fiber bundle, defining the same
topology as the already existing one, and varying continuously with the base point. See also
`ContMDiffRiemannianMetric` for a smooth version.

This structure is used through `RiemannianBundle` for typeclass inference, to register the inner
product space structure on the fibers without creating diamonds.  -/
Bundle.ContinuousRiemannianMetric : {B : Type u_4} →
  [inst : TopologicalSpace B] →
    (F : Type u_5) →
      [inst_1 : NormedAddCommGroup F] →
        [inst_2 : NormedSpace ℝ F] →
          (E : B → Type u_6) →
            [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] →
              [inst_4 : (b : B) → TopologicalSpace (E b)] →
                [inst_5 : (b : B) → AddCommGroup (E b)] →
                  [inst_6 : (b : B) → Module ℝ (E b)] →
                    [inst_7 : FiberBundle F E] → [VectorBundle ℝ F E] → Type (max u_4 u_6)
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.coe_toAlternatingMap : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] (f : M [⋀^ι]→L[R] N), ⇑f.toAlternatingMap = ⇑f
-- Mathlib.Algebra.Module.Torsion.PrimaryComponent
Ideal.iSupIndep_primaryComponent : ∀ (A : Type u_1) (M : Type u_2) [inst : CommRing A] [inst_1 : AddCommGroup M] [inst_2 : Module A M]
  [IsDedekindDomain A], iSupIndep fun P => Ideal.primaryComponent M P.asIdeal
-- Mathlib.Order.ULift
ULift.instOrd_mathlib : {α : Type u} → [Ord α] → Ord (ULift.{v, u} α)
-- Aesop.Forward.State
/-- Erase all pattern substitutions whose source is the target.  -/
Aesop.ForwardState.eraseTargetPatSubsts : Aesop.ForwardState → Aesop.ForwardState
-- Mathlib.Data.NNRat.Defs
/-- The absolute value on `ℚ` as a map to `ℚ≥0`.  -/
Rat.nnabs : ℚ → ℚ≥0
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.sub_nonempty : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Sub α] {s t : Finset α}, (s - t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiff.add_section : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {s t : (x : M) → V x},
  (ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun x => ⟨x, s x⟩) →
    (ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun x => ⟨x, t x⟩) →
      ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun x => ⟨x, (s + t) x⟩
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- If two functions coincide in a neighborhood of `x` within a set `s` and at `x`, then their
iterated differentials within this set at `x` coincide.  -/
Filter.EventuallyEq.iteratedFDerivWithin_eq : ∀ {𝕜 : 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] {s : Set E}
  {f f₁ : E → F} {x : E},
  f₁ =ᶠ[nhdsWithin x s] f → f₁ x = f x → ∀ (n : ℕ), iteratedFDerivWithin 𝕜 n f₁ s x = iteratedFDerivWithin 𝕜 n f s x
-- Mathlib.Data.Int.GCD
/-- The extended GCD `a` value in the equation `gcd x y = x * a + y * b`.  -/
Nat.gcdA : ℕ → ℕ → ℤ
-- Mathlib.RingTheory.WittVector.FrobeniusFractionField
WittVector.RecursionBase.solution.congr_simp : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : Field k] [inst_1 : IsAlgClosed k] (a₁ a₁_1 : WittVector p k),
  a₁ = a₁_1 →
    ∀ (a₂ a₂_1 : WittVector p k),
      a₂ = a₂_1 → WittVector.RecursionBase.solution p a₁ a₂ = WittVector.RecursionBase.solution p a₁_1 a₂_1
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.indep_limsup_atBot_self : ∀ {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  [inst : SemilatticeInf ι] [NoMinOrder ι] [Nonempty ι],
  (∀ (n : ι), s n ≤ m0) →
    ProbabilityTheory.iIndep s μ →
      ProbabilityTheory.Indep (Filter.limsup s Filter.atBot) (Filter.limsup s Filter.atBot) μ
-- Mathlib.RingTheory.GradedAlgebra.Basic
instGradedAlgebraRestrictScalars : {ι : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} →
      [inst : DecidableEq ι] →
        [inst_1 : AddMonoid ι] →
          [inst_2 : CommSemiring R] →
            [inst_3 : Semiring A] →
              [inst_4 : Algebra R A] →
                (𝒜 : ι → Submodule R A) →
                  (R₀ : Type u_5) →
                    [inst_5 : CommSemiring R₀] →
                      [inst_6 : Algebra R₀ R] →
                        [inst_7 : Algebra R₀ A] →
                          [inst_8 : IsScalarTower R₀ R A] →
                            [i : GradedAlgebra 𝒜] → GradedAlgebra fun x => Submodule.restrictScalars R₀ (𝒜 x)
-- Lean.Meta.Tactic.Grind.Extension
/-- Instantiates the theorem only if its generation is less than `n`
 -/
Lean.Meta.Grind.EMatchTheoremConstraint.genLt : ℕ → Lean.Meta.Grind.EMatchTheoremConstraint
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
/-- The negation of a nonsingular point on a Weierstrass curve in affine coordinates.

Given a nonsingular point `P` in affine coordinates, use `-P` instead of `neg P`.  -/
WeierstrassCurve.Affine.Point.neg : {R : Type r} → [inst : CommRing R] → {W' : WeierstrassCurve.Affine R} → W'.Point → W'.Point
-- Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
SimplexCategory.mkOfLe.congr_simp : ∀ {n : ℕ} (i i_1 : Fin (n + 1)) (e_i : i = i_1) (j j_1 : Fin (n + 1)) (e_j : j = j_1) (h : i ≤ j),
  SimplexCategory.mkOfLe i j h = SimplexCategory.mkOfLe i_1 j_1 ⋯
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- The converse to `GenLoop.homotopyTo`: a homotopy between two loops in the space of
`n`-dimensional loops can be seen as a homotopy between two `n+1`-dimensional paths.  -/
GenLoop.homotopyFrom : {N : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace X] →
      {x : X} →
        [inst_1 : DecidableEq N] →
          (i : N) →
            {p q : ↑(GenLoop N X x)} →
              Path.Homotopy (GenLoop.toLoop i p) (GenLoop.toLoop i q) → C(↑unitInterval × (N → ↑unitInterval), X)
-- Mathlib.Topology.ContinuousMap.Interval
ContinuousMap.IccExtendCM.eq_1 : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α] {a b : α}
  [inst_3 : Fact (a ≤ b)] {E : Type u_2} [inst_4 : TopologicalSpace E],
  ContinuousMap.IccExtendCM = { toFun := fun f => f.comp ContinuousMap.projIccCM, continuous_toFun := ⋯ }
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.sSameSide_point_excenter_singleton : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) [n.AtLeastTwo]
  {i j : Fin (n + 1)},
  i ≠ j → (affineSpan ℝ (Set.range (s.faceOpposite i).points)).SSameSide (s.points i) (s.excenter {j})
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.exists_of_res_eq_of_qcqs : ∀ {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↥X},
  IsCompact U.carrier →
    IsQuasiSeparated U.carrier →
      ∀ {f g s : ↑(X.presheaf.obj (Opposite.op U))},
        TopCat.Presheaf.restrictOpen f (X.basicOpen s) ⋯ = TopCat.Presheaf.restrictOpen g (X.basicOpen s) ⋯ →
          ∃ n, s ^ n * f = s ^ n * g
-- Mathlib.AlgebraicGeometry.LimitsOver
AlgebraicGeometry.instIsOpenImmersionLeftSchemeDiscretePUnitιOverTopMorphismProperty : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [inst : AlgebraicGeometry.IsZariskiLocalAtSource P]
  {S : AlgebraicGeometry.Scheme} {J : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} J]
  (F : CategoryTheory.Functor J (P.Over ⊤ S))
  [inst_2 : ∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f).left]
  [inst_3 :
    (F.comp
        ((CategoryTheory.MorphismProperty.Over.forget P ⊤ S).comp
          ((CategoryTheory.Over.forget S).comp AlgebraicGeometry.Scheme.forget))).IsLocallyDirected]
  [inst_4 : Quiver.IsThin J] [inst_5 : Small.{u, u_1} J] (j : J),
  AlgebraicGeometry.IsOpenImmersion (CategoryTheory.Limits.colimit.ι F j).left
-- Mathlib.RepresentationTheory.Action
Action.tensor_ρ_apply : ∀ {G : Type v} [inst : Monoid G] {X Y : Action (Type w) G} (g : G)
  (xy : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).V),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).ρ g)) xy =
    ((CategoryTheory.ConcreteCategory.hom (X.ρ g)) xy.1, (CategoryTheory.ConcreteCategory.hom (Y.ρ g)) xy.2)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ofDiseqSplit : Lean.Meta.Grind.Arith.Linear.DiseqCnstr →
  Lean.FVarId →
    Lean.Meta.Grind.Arith.Linear.UnsatProof → Array Lean.FVarId → Lean.Meta.Grind.Arith.Linear.IneqCnstrProof
-- Mathlib.Algebra.Algebra.Spectrum.Basic
/-- **Alias** of `spectrum.setOfPred_isUnit_inter_mul_comm`. -/
spectrum.setOf_isUnit_inter_mul_comm : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] (a b : A),
  {r | IsUnit r} ∩ spectrum R (a * b) = {r | IsUnit r} ∩ spectrum R (b * a)
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.stats : {α : Type u_1} →
  {β : Type u_2} → {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashMap α β → Lean.PersistentHashMap.Stats
-- Mathlib.Algebra.GCDMonoid.FinsetLemmas
Finset.Rat.den_sum_dvd_lcm_den : ∀ {ι : Type u_3} (s : Finset ι) (f : ι → ℚ), (∑ i ∈ s, f i).den ∣ s.lcm fun i => (f i).den
-- Mathlib.Data.Set.Card
Set.encard_lt_encard_iff_encard_sdiff_lt_encard_sdiff : ∀ {α : Type u_1} {s t : Set α}, (s ∩ t).Finite → (s.encard < t.encard ↔ (s \ t).encard < (t \ s).encard)
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
CategoryTheory.LaxFunctor.mapComp_assoc_left_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.LaxFunctor B C) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) {Z : F.obj a ⟶ F.obj d}
  (h_1 : F.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (F.map h))
      (CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.comp f g) h) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (F.map h)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapComp g h))
        (CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.comp g h))
          (CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.associator f g h).inv) h_1)))
-- Mathlib.Algebra.Field.Basic
OrderDual.instRatCast : {K : Type u_1} → [RatCast K] → RatCast Kᵒᵈ
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- **Alias** of `MonoidAlgebra.coeff_mul_single_eq_coeff_mul`. -/
MonoidAlgebra.mul_single_apply_aux : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {x : MonoidAlgebra R M} {r : R} {m m₁ : M} [inst_1 : Mul M]
  (m₂ : M), (∀ m' ∈ x.coeff.support, m' * m = m₁ ↔ m' = m₂) → (x * MonoidAlgebra.single m r).coeff m₁ = x.coeff m₂ * r
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
IsUnit.prod_iff : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : CommMonoid M] {f : ι → M},
  IsUnit (∏ a ∈ s, f a) ↔ ∀ a ∈ s, IsUnit (f a)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Map
MeasureTheory.setLIntegral_map : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {f : β → ENNReal} {g : α → β} {s : Set β},
  MeasurableSet s →
    Measurable f →
      Measurable g → ∫⁻ (y : β) in s, f y ∂MeasureTheory.Measure.map g μ = ∫⁻ (x : α) in g ⁻¹' s, f (g x) ∂μ
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.AssocList.foldlM.eq_1 : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w'} [inst : Monad m] (f : δ → (a : α) → β a → m δ)
  (x : δ), Std.DHashMap.Internal.AssocList.foldlM f x Std.DHashMap.Internal.AssocList.nil = pure x
-- Mathlib.RingTheory.FormalGroup.Basic
FormalGroup.zero_add : ∀ {R : Type u_1} [inst : CommRing R] {σ : Type u_3} (F : FormalGroup R) {f : MvPowerSeries σ R},
  PowerSeries.HasSubst f → MvPowerSeries.subst ![0, f] F.toPowerSeries = f
-- Init.MetaTypes
Lean.instInhabitedNameGenerator.default : Lean.NameGenerator
-- Mathlib.MeasureTheory.Covering.Differentiation
VitaliFamily.withDensity_limRatioMeas_eq : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (v : VitaliFamily μ) [inst_1 : SecondCountableTopology α] [inst_2 : BorelSpace α]
  [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ] {ρ : MeasureTheory.Measure α}
  [inst_4 : MeasureTheory.IsLocallyFiniteMeasure ρ] (hρ : ρ.AbsolutelyContinuous μ),
  μ.withDensity (v.limRatioMeas hρ) = ρ
-- Lean.Parser.Types
/-- Input string and related data. Recall that the `FileMap` is a helper structure for mapping
`String.Pos` in the input string to line/column information.   -/
Lean.Parser.InputContext : Type
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctor.map₂_iso_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.PrelaxFunctor B C) {a b : B} {f g : a ⟶ b} (η : f ≅ g),
  F.map₂ η.inv = CategoryTheory.inv (F.map₂ η.hom)
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.instIsRepresentableObjOppositeTypeYoneda : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C}, (CategoryTheory.yoneda.obj X).IsRepresentable
-- Mathlib.Topology.Constructions
isClosed_set_pi : ∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] {i : Set ι} {s : (a : ι) → Set (A a)},
  (∀ a ∈ i, IsClosed (s a)) → IsClosed (i.pi s)
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithUpperSet.ofUpperSet_le_ofUpperSet : ∀ {α : Type u_1} [inst : Preorder α] {a b : Topology.WithUpperSet α},
  Topology.WithUpperSet.ofUpperSet a ≤ Topology.WithUpperSet.ofUpperSet b ↔ b ⤳ a
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instDiv.eq_1 : ∀ {α : Type u_1} [inst : Div α], Colex.instDiv = inst
-- Mathlib.Order.Interval.Set.Image
StrictAnti.image_Ioi_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a : α},
  StrictAnti f → f '' Set.Ioi a ⊆ Set.Iio (f a)
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
SSet.S.mk.sizeOf_spec : ∀ {X : SSet} {dim : ℕ} (simplex : X.obj (Opposite.op { len := dim })),
  sizeOf { dim := dim, simplex := simplex } = 1 + sizeOf dim + sizeOf simplex
-- Lean.Compiler.MetaAttr
/-- Set of IR decls that should be made available to any importer. This is a superset of `metaExt`
(except for non-defs such as `meta structure`), which is managed by the elaborator and has a
different async mode. More precisely, it contains the closure of `metaExt` as well as further
derived decls such as `_boxed` versions. We store this set primarily to filter exports in
`declMapExt`; we persist it in `.olean.private` for the benefit of `shake`.
 -/
_private.Lean.Compiler.MetaAttr.0.Lean.declMetaExt : Lean.SimplePersistentEnvExtension Lean.Name Lean.NameSet
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
Std.Iterators.Types.Flatten.mk : {α α₂ β : Type w} →
  {m : Type w → Type u_1} → Std.IterM m (Std.IterM m β) → Option (Std.IterM m β) → Std.Iterators.Types.Flatten α α₂ β m
-- Mathlib.Algebra.Category.Grp.FilteredColimits
AddCommGrpCat.FilteredColimits.forget_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget AddCommGrpCat)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.sqrt_eq_rpow : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] {a : A}, CFC.sqrt a = a ^ (1 / 2)