mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Consumers.Monadic.Loop.0.Std.IterM.DefaultConsumers.forIn'.match_3.eq_2 : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Std.Iterator α m β] (it : Std.IterM m β)
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (h : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_2 it' h
-- Mathlib.Data.Setoid.Partition
IndexedPartition.some_index : ∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) (x : α), hs.setoid (hs.some (hs.index x)) x
-- Mathlib.Order.Cofinal
/-- **Alias** of `OrderIso.map_isCofinal`. -/
OrderIso.map_cofinal : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) {s : Set α},
  IsCofinal s → IsCofinal (⇑e '' s)
-- Lean.Meta.Tactic.Simp.Types
/-- Given an application `e`, recursively simplifies its function and arguments and constructs a proof
using `congrArg`, `congrFun`, `congrFun'` and `congr`.
 -/
Lean.Meta.Simp.simpAppUsingCongr : Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Result
-- Std.Time.Zoned.Database.TzIf
_private.Std.Time.Zoned.Database.TzIf.0.Std.Time.TimeZone.TZif.parseAbbreviations : Array Std.Time.TimeZone.TZif.LocalTimeType → UInt32 → Std.Internal.Parsec.ByteArray.Parser (Array String)
-- Mathlib.Data.Prod.TProd
List.TProd.elim_of_ne : ∀ {ι : Type u} {α : ι → Type v} {i j : ι} {l : List ι} [inst : DecidableEq ι] (hj : j ∈ i :: l) (hji : j ≠ i)
  (v : List.TProd α (i :: l)), v.elim hj = List.TProd.elim v.2 ⋯
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.map_pow : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] (f : R →+* S) (n : ℕ),
  Polynomial.map f (p ^ n) = Polynomial.map f p ^ n
-- Mathlib.Data.Holor
_private.Mathlib.Data.Holor.0.HolorIndex.take.match_1.eq_1 : ∀ {ds₂ : List ℕ} (motive : (x : List ℕ) → HolorIndex (x ++ ds₂) → Sort u_1) (ds : List ℕ) (is : HolorIndex (ds ++ ds₂))
  (h_1 : (ds : List ℕ) → (is : HolorIndex (ds ++ ds₂)) → motive ds is),
  (match ds, is with
    | ds, is => h_1 ds is) =
    h_1 ds is
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
conj_circleMap : ∀ (c : ℂ) (r θ : ℝ), (starRingEnd ℂ) (circleMap c r θ) = circleMap ((starRingEnd ℂ) c) r (-θ)
-- Mathlib.Combinatorics.SimpleGraph.Density
SimpleGraph.edgeDensity_comm : ∀ {α : Type u_4} (G : SimpleGraph α) [inst : DecidableRel G.Adj] (s t : Finset α), G.edgeDensity s t = G.edgeDensity t s
-- Mathlib.Algebra.Lie.SerreConstruction
/-- The ideal of the free Lie algebra generated by the relations.  -/
CartanMatrix.Relations.toIdeal : (R : Type u) →
  {B : Type v} →
    [inst : CommRing R] → Matrix B B ℤ → [DecidableEq B] → LieIdeal R (FreeLieAlgebra R (CartanMatrix.Generators B))
-- Init.Data.String.Defs
String.instLTPos : {s : String} → LT s.Pos
-- Mathlib.Data.Finsupp.Basic
Finsupp.extendDomain.congr_simp : ∀ {α : Type u_1} {M : Type u_12} [inst : Zero M] {P : α → Prop} {inst_1 : DecidablePred P} [inst_2 : DecidablePred P]
  (f f_1 : Subtype P →₀ M), f = f_1 → f.extendDomain = f_1.extendDomain
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
IsStarNormal.instContinuousFunctionalCalculus : ∀ {A : Type u_1} [inst : CStarAlgebra A], ContinuousFunctionalCalculus ℂ A IsStarNormal
-- Mathlib.Analysis.Fourier.AddCircle
fourierCoeff.congr_simp : ∀ {T : ℝ} [hT : Fact (0 < T)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E]
  (f f_1 : AddCircle T → E), f = f_1 → ∀ (n n_1 : ℤ), n = n_1 → fourierCoeff f n = fourierCoeff f_1 n_1
-- Aesop.Script.SpecificTactics
Aesop.renameInaccessibleFVarsS : Lean.MVarId → Aesop.ScriptM (Lean.MVarId × Array Lean.FVarId)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_eq_some_get! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → ∀ {a : α}, a ∈ t → t.get? a = some (t.get! a)
-- Mathlib.Algebra.Ring.GeomSum
sub_one_dvd_pow_sub_one : ∀ {R : Type u_1} [inst : Ring R] (x : R) (n : ℕ), x - 1 ∣ x ^ n - 1
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Subgroup.op_eq_bot : ∀ {G : Type u_2} [inst : Group G] {S : Subgroup G}, S.op = ⊥ ↔ S = ⊥
-- Mathlib.Algebra.Field.Opposite
AddOpposite.instRatCast.eq_1 : ∀ {α : Type u_1} [inst : RatCast α], AddOpposite.instRatCast = { ratCast := fun q => AddOpposite.op ↑q }
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.coe_const : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (x : β), ↑(CauSeq.const abv x) = Function.const ℕ x
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
AlgebraicGeometry.Scheme.Cover.forgetQc_toPreZeroHypercover : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.propQCPrecoverage P) S),
  𝒰.forgetQc.toPreZeroHypercover = 𝒰.toPreZeroHypercover
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.Comonad.comparisonForget_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) (x : C),
  (CategoryTheory.Comonad.comparisonForget h).inv.app x = CategoryTheory.CategoryStruct.id (L.obj x)
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.lcomp_injective_of_surjective : ∀ {R : Type u_1} {S : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] {M : Type u_5} {M₂ : Type u_6} {N : Type u_7}
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : AddCommMonoid N] [inst_5 : Module R M]
  [inst_6 : Module R M₂] [inst_7 : Module S N] [inst_8 : Module R N] [inst_9 : SMulCommClass R S N] (g : M →ₗ[R] M₂),
  Function.Surjective ⇑g → Function.Injective ⇑(LinearMap.lcomp S N g)
-- Mathlib.Analysis.Normed.Operator.Bilinear
/-- Derivative of a continuous bilinear map `f : E →L[𝕜] F →L[𝕜] G` interpreted as a map `E × F → G`
at point `p : E × F` evaluated at `q : E × F`, as a continuous bilinear map.  -/
ContinuousLinearMap.deriv₂ : {𝕜 : Type u_1} →
  {E : Type u_4} →
    {Fₗ : Type u_7} →
      {Gₗ : Type u_9} →
        [inst : SeminormedAddCommGroup E] →
          [inst_1 : SeminormedAddCommGroup Fₗ] →
            [inst_2 : SeminormedAddCommGroup Gₗ] →
              [inst_3 : NontriviallyNormedField 𝕜] →
                [inst_4 : NormedSpace 𝕜 E] →
                  [inst_5 : NormedSpace 𝕜 Fₗ] →
                    [inst_6 : NormedSpace 𝕜 Gₗ] → (E →L[𝕜] Fₗ →L[𝕜] Gₗ) → E × Fₗ →L[𝕜] E × Fₗ →L[𝕜] Gₗ
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
CategoryTheory.PreOneHypercover.toPullback_cylinder : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} [inst_1 : CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F)
  {i j : (CategoryTheory.PreOneHypercover.cylinder f g).I₀} (k : (CategoryTheory.PreOneHypercover.cylinder f g).I₁ i j),
  (CategoryTheory.PreOneHypercover.cylinder f g).toPullback k =
    CategoryTheory.Limits.pullback.fst
      (CategoryTheory.Limits.pullback.map (CategoryTheory.PreOneHypercover.cylinderf f g i.snd)
        (CategoryTheory.PreOneHypercover.cylinderf f g j.snd) (E.f i.fst) (E.f j.fst)
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ i.fst) (g.h₀ i.fst) ⋯)
          (F.toPullback i.snd))
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ j.fst) (g.h₀ j.fst) ⋯)
          (F.toPullback j.snd))
        (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
      (CategoryTheory.Limits.pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯)
-- Mathlib.Analysis.CStarAlgebra.Projection
isStarProjection_iff_quasispectrum_subset_and_isSelfAdjoint : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A] [inst_3 : Module ℝ A]
  [inst_4 : IsScalarTower ℝ A A] [inst_5 : SMulCommClass ℝ A A]
  [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] {p : A},
  IsStarProjection p ↔ quasispectrum ℝ p ⊆ {0, 1} ∧ IsSelfAdjoint p
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
/-- **Alias** of the reverse direction of `Matrix.separatingRight_transpose_iff`. -/
Matrix.SeparatingLeft.separatingRight_transpose : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : CommSemiring R] {M : Matrix m n R} [inst_1 : Finite m]
  [inst_2 : Finite n], M.SeparatingLeft → M.transpose.SeparatingRight
-- Mathlib.Analysis.InnerProductSpace.Dual
InnerProductSpace.instIsContPerfPairRealInnerₗOfCompleteSpace : ∀ (E : Type u_2) [inst : NormedAddCommGroup E] [CompleteSpace E] [inst_2 : InnerProductSpace ℝ E],
  (innerₗ E).IsContPerfPair
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.Slice.startsWith_char_iff_get : ∀ {c : Char} {s : String.Slice}, s.startsWith c = true ↔ ∃ (h : s.startPos ≠ s.endPos), s.startPos.get h = c
-- Mathlib.Util.Export
Lean.Export.exportLevel : Lean.Level → Lean.ExportM ℕ
-- Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
GenContFract.exists_rat_eq_nth_den : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] (v : K) (n : ℕ),
  ∃ q, (GenContFract.of v).dens n = ↑q
-- Mathlib.Data.EReal.Basic
EReal.exists_rat_btwn_of_lt : ∀ {a b : EReal}, a < b → ∃ x, a < ↑↑x ∧ ↑↑x < b
-- Mathlib.Algebra.Category.Ring.FilteredColimits
CommRingCat.FilteredColimits.colimitCommRing : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [inst_1 : CategoryTheory.IsFiltered J] →
      (F : CategoryTheory.Functor J CommRingCat) → CommRing ↑(CommRingCat.FilteredColimits.R F)
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cocone.fromStructuredArrow_obj_pt : ∀ {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.StructuredArrow F (CategoryTheory.Functor.const J)),
  ((CategoryTheory.Limits.Cocone.fromStructuredArrow F).obj c).pt = c.right
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cyclesIsoH_hom_inv_id : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cyclesIsoH_hom_inv_id._auto_1),
  CategoryTheory.CategoryStruct.comp (X.cyclesIsoH f n₀ n₁ hn₁).hom
      (X.toCycles (CategoryTheory.CategoryStruct.id i₀) f f ⋯ n₀) =
    CategoryTheory.CategoryStruct.id (X.cycles (CategoryTheory.CategoryStruct.id i₀) f n₀)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- A vector measure `v` is absolutely continuous with respect to a measure `μ` if for all sets
`s`, `μ s = 0`, we have `v s = 0`.  -/
MeasureTheory.«term_≪ᵥ_» : Lean.TrailingParserDescr
-- Init.Data.List.MinMaxOn
List.maxOn_id : ∀ {α : Type u_1} [inst : Max α] [inst_1 : LE α] [inst_2 : DecidableLE α] [Std.LawfulOrderLeftLeaningMax α] {xs : List α}
  (h : xs ≠ []), List.maxOn id xs h = xs.max h
-- Lean.Meta.Tactic.Assert
_private.Lean.Meta.Tactic.Assert.0.Lean.MVarId.assertAfter'.visitLocalDecl : Lean.LocalDecl → StateRefT' IO.RealWorld Lean.LocalDecl Lean.MetaM Unit
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.hasBiproductsOfShape_finite : ∀ {J : Type w} (C : Type uC) [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [Finite J],
  CategoryTheory.Limits.HasBiproductsOfShape J C
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.smulRight_toContinuousMultilinearMap : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] [inst_5 : TopologicalSpace R]
  [inst_6 : TopologicalSpace M] [inst_7 : TopologicalSpace N] [inst_8 : ContinuousSMul R N] (f : M [⋀^ι]→L[R] R)
  (z : N), (f.smulRight z).toContinuousMultilinearMap = f.smulRight z
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey?_insertMany_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List (α × β)} {k k' : α},
      (k == k') = true →
        List.Pairwise (fun a b => (a.1 == b.1) = false) l →
          k ∈ List.map Prod.fst l → (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)).getKey? k' = some k
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.ExprCnstr.eq : Nat.Internal.Linear.ExprCnstr → Bool
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.codExtend'_target : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {s : Set B}
  (hs : IsOpen s) {proj : Z → ↑s} (e : Bundle.Pretrivialization F proj) [inst_2 : Nonempty (B → F → Z)],
  (Bundle.Pretrivialization.codExtend' hs e).target = Prod.map Subtype.val id '' e.target
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.mk.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (toLinearMap toLinearMap_1 : M →ₗ[R] N →ₗ[R] R)
  (e_toLinearMap : toLinearMap = toLinearMap_1) [isPerfPair_toLinearMap : toLinearMap.IsPerfPair] (root root_1 : ι ↪ M)
  (e_root : root = root_1) (coroot coroot_1 : ι ↪ N) (e_coroot : coroot = coroot_1)
  (root_coroot_two : ∀ (i : ι), (toLinearMap (root i)) (coroot i) = 2) (reflectionPerm reflectionPerm_1 : ι → ι ≃ ι)
  (e_reflectionPerm : reflectionPerm = reflectionPerm_1)
  (reflectionPerm_root : ∀ (i j : ι), root j - (toLinearMap (root j)) (coroot i) • root i = root ((reflectionPerm i) j))
  (reflectionPerm_coroot :
    ∀ (i j : ι), coroot j - (toLinearMap (root i)) (coroot j) • coroot i = coroot ((reflectionPerm i) j)),
  { toLinearMap := toLinearMap, isPerfPair_toLinearMap := isPerfPair_toLinearMap, root := root, coroot := coroot,
      root_coroot_two := root_coroot_two, reflectionPerm := reflectionPerm, reflectionPerm_root := reflectionPerm_root,
      reflectionPerm_coroot := reflectionPerm_coroot } =
    { toLinearMap := toLinearMap_1, isPerfPair_toLinearMap := ⋯, root := root_1, coroot := coroot_1,
      root_coroot_two := ⋯, reflectionPerm := reflectionPerm_1, reflectionPerm_root := ⋯, reflectionPerm_coroot := ⋯ }
-- Mathlib.Analysis.Normed.Ring.Units
Units.add.congr_simp : ∀ {R : Type u_1} [inst : NormedRing R] [inst_1 : HasSummableGeomSeries R] (x x_1 : Rˣ) (e_x : x = x_1) (t t_1 : R)
  (e_t : t = t_1) (h : ‖t‖ < ‖↑x⁻¹‖⁻¹), x.add t h = x_1.add t_1 ⋯
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.singularPart_eq_singularPart_measure : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {κ η : ProbabilityTheory.Kernel α γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] [inst : ProbabilityTheory.IsFiniteKernel η]
  [inst_1 : ProbabilityTheory.IsFiniteKernel κ] {a : α}, (κ.singularPart η) a = (κ a).singularPart (η a)
-- Mathlib.FieldTheory.IsPerfectClosure
PerfectRing.lift_lift_apply : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing K] [inst_1 : CommRing L]
  [inst_2 : CommRing M] [inst_3 : CommRing N] (i : K →+* L) (j : K →+* M) (g : L →+* N) (p : ℕ) [inst_4 : ExpChar M p]
  [inst_5 : ExpChar K p] [inst_6 : PerfectRing M p] [inst_7 : IsPRadical i p] [inst_8 : ExpChar L p]
  [inst_9 : ExpChar N p] [inst_10 : IsPRadical g p] [inst_11 : IsPRadical (g.comp i) p] (x : N),
  (PerfectRing.lift g (PerfectRing.lift i j p) p) x = (PerfectRing.lift (g.comp i) j p) x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  [Inhabited α] {k k' : α} {f : β → β} {hc : k' ∈ t.modify k f},
  (t.modify k f).getKey k' hc = if cmp k k' = Ordering.eq then k else t.getKey k' ⋯
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.pi.eq_1 : ∀ {α : Type u} (β : α → ProfiniteGrp.{u_1}),
  ProfiniteGrp.pi β = ProfiniteGrp.ofProfinite (Profinite.pi fun a => (β a).toProfinite)
-- Mathlib.CategoryTheory.Monad.Algebra
/-- The unit axiom associated to an algebra.  -/
CategoryTheory.Monad.Algebra.unit_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (self : T.Algebra) {Z : C}
  (h : self.A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (T.η.app self.A) (CategoryTheory.CategoryStruct.comp self.a h) = h
-- Mathlib.CategoryTheory.Presentable.SharplyLT.Basic
Cardinal.SharplyLT.mk : ∀ {κ₁ κ₂ : Cardinal.{w}} [inst : Fact κ₁.IsRegular] [inst_1 : Fact κ₂.IsRegular],
  κ₁ < κ₂ → CategoryTheory.IsCardinalAccessibleCategory (CategoryTheory.CardinalDirectedPoset κ₁) κ₂ → κ₁.SharplyLT κ₂
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.prod_sum_left : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {ι : Type u_4}
  (m : ι → MeasureTheory.Measure α) (μ : MeasureTheory.Measure β) [MeasureTheory.SFinite μ],
  (MeasureTheory.Measure.sum m).prod μ = MeasureTheory.Measure.sum fun i => (m i).prod μ
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.netEntropyInfEntourage_nonneg : ∀ {X : Type u_1} {F : Set X} (T : X → X), F.Nonempty → ∀ (U : SetRel X X), 0 ≤ Dynamics.netEntropyInfEntourage T F U
-- Mathlib.Analysis.Normed.Group.Defs
GroupSeminorm.toSeminormedGroup.eq_1 : ∀ {E : Type u_5} [inst : Group E] (f : GroupSeminorm E),
  f.toSeminormedGroup =
    { norm := ⇑f, toGroup := inst, dist := fun x y => f (x⁻¹ * y), dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯,
      edist_dist := ⋯, uniformity_dist := ⋯, cobounded_sets := ⋯, dist_eq := ⋯ }
-- Mathlib.Order.Bounds.Basic
IsCoinitialFor.trans : ∀ {α : Type u_1} [inst : Preorder α] {s t u : Set α}, IsCoinitialFor s t → IsCoinitialFor t u → IsCoinitialFor s u
-- Mathlib.MeasureTheory.Integral.Indicator
/-- If the indicators of measurable sets `Aᵢ` tend pointwise to the indicator of a set `A`
and we eventually have `Aᵢ ⊆ B` for some set `B` of finite measure, then the measures of `Aᵢ`
tend to the measure of `A`.  -/
MeasureTheory.tendsto_measure_of_tendsto_indicator : ∀ {α : Type u_1} [inst : MeasurableSpace α] {A : Set α} {ι : Type u_2} (L : Filter ι) [L.IsCountablyGenerated]
  {As : ι → Set α} {μ : MeasureTheory.Measure α},
  (∀ (i : ι), MeasurableSet (As i)) →
    ∀ {B : Set α},
      MeasurableSet B →
        μ B ≠ ⊤ →
          (∀ᶠ (i : ι) in L, As i ⊆ B) →
            (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) → Filter.Tendsto (fun i => μ (As i)) L (nhds (μ A))
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.const_zero : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : R)
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (hu : U ≤ PrimeSpectrum.basicOpen f),
  AlgebraicGeometry.StructureSheaf.const 0 f U hu = 0
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.trivial_I₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (S : C)
  (x x_1 : (CategoryTheory.PreZeroHypercover.singleton (CategoryTheory.CategoryStruct.id S)).I₀),
  (CategoryTheory.PreOneHypercover.trivial S).I₁ x x_1 = PUnit.{w + 1}
-- Qq.MatchImpl
Qq.Impl.PatVarDecl.fvarId : Qq.Impl.PatVarDecl → Lean.FVarId
-- Init.Data.Nat.Lemmas
Nat.pow_add : ∀ (a m n : ℕ), a ^ (m + n) = a ^ m * a ^ n
-- Lean.Parser.Command
Lean.Parser.Command.variable.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Order.Monoid.Lex
OrderAddMonoidHom.fstₗ.eq_1 : ∀ (α : Type u_1) (β : Type u_2) [inst : AddMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddMonoid β]
  [inst_3 : Preorder β],
  OrderAddMonoidHom.fstₗ α β = { toFun := fun p => (ofLex p).1, map_zero' := ⋯, map_add' := ⋯, monotone' := ⋯ }
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instToStringOffset : ToString Std.Time.Nanosecond.Offset
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernel.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : CategoryTheory.Limits.HasCokernel S.f] (hg : S.g = 0),
  CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernel S hg =
    CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork S hg
      (CategoryTheory.Limits.Cofork.ofπ (CategoryTheory.Limits.cokernel.π S.f) ⋯)
      (CategoryTheory.Limits.cokernelIsCokernel S.f)
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.MatchResult.covered.sizeOf_spec : ∀ (f : Lean.Elab.Term.Quotation.Alt → Lean.Elab.TermElabM Lean.Elab.Term.Quotation.Alt) (exhaustive : Bool),
  sizeOf (Lean.Elab.Term.Quotation.MatchResult.covered f exhaustive) = 1 + sizeOf exhaustive
-- Mathlib.Data.Set.Opposite
/-- Taking opposites as an equivalence of powersets.  -/
Set.opEquiv : {α : Type u_1} → Set α ≃ Set αᵒᵖ
-- Init.Data.Array.Zip
Array.zip_map' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : α → γ} {xs : Array α},
  (Array.map f xs).zip (Array.map g xs) = Array.map (fun a => (f a, g a)) xs
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.add_nsmul_modEq : ∀ {M : Type u_1} [inst : AddCommMonoid M] {a p : M} (n : ℕ), a + n • p ≡ a [PMOD p]
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.mapEquiv_coe : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [inst_1 : UniformSpace β]
  (pkg' : AbstractCompletion.{vβ, uβ} β) (e : α ≃ᵤ β) (a : α), (pkg.mapEquiv pkg' e) (pkg.coe a) = pkg'.coe (e a)
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.normalizationObjIso.congr_simp : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] {U : Y.Opens} (hU : AlgebraicGeometry.IsAffineOpen U),
  AlgebraicGeometry.Scheme.Hom.normalizationObjIso f hU = AlgebraicGeometry.Scheme.Hom.normalizationObjIso f hU
-- Lean.Meta.CoeAttr
Lean.Meta.CoeFnType.noConfusionType : Sort v✝ → Lean.Meta.CoeFnType → Lean.Meta.CoeFnType → Sort v✝
-- Mathlib.Analysis.Seminorm
Seminorm.preimage_metric_closedBall : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (p : Seminorm 𝕜 E) {r : ℝ}, ⇑p ⁻¹' Metric.closedBall 0 r = {x | p x ≤ r}
-- Lean.Util.MonadCache
Lean.MonadHashMapCacheAdapter.modifyCache : {α β : Type} →
  {m : Type → Type} →
    {inst : BEq α} →
      {inst_1 : Hashable α} →
        [self : Lean.MonadHashMapCacheAdapter α β m] → (Std.HashMap α β → Std.HashMap α β) → m Unit
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.eq_empty_iff_size_eq_zero : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [Std.TransCmp cmp], t = ∅ ↔ t.size = 0
-- Mathlib.RingTheory.WittVector.Frobenius
WittVector.frobeniusPolyRat.eq_1 : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ),
  WittVector.frobeniusPolyRat p n = (MvPolynomial.bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ n)
-- Std.Data.ExtTreeSet.Basic
/-- Returns the `n`-th smallest element.  -/
Std.ExtTreeSet.atIdx : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → (t : Std.ExtTreeSet α cmp) → (n : ℕ) → n < t.size → α