mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.SInt.Lemmas
Int8.ofIntLE_add : ∀ {a b : ℤ} {hab₁ : Int8.minValue.toInt ≤ a + b} {hab₂ : a + b ≤ Int8.maxValue.toInt},
  Int8.ofIntLE (a + b) hab₁ hab₂ = Int8.ofInt a + Int8.ofInt b
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- The 2nd group cohomology of `A`, defined as the 2nd cohomology of the complex of inhomogeneous
cochains, is isomorphic to `cocycles₂ A ⧸ coboundaries₂ A`, which is a simpler type.  -/
groupCohomology.H2Iso : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) → groupCohomology.H2 A ≅ (groupCohomology.shortComplexH2 A).moduleCatLeftHomologyData.H
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂)
  (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
  (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f)
  (X : ↑(F.obj b₀)),
  CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₁ f₁₃ f ⋯).hom.toNatTrans.app X)
      ((F.mapComp' f₁₂ f₂₃ f₁₃ ⋯).hom.toNatTrans.app ((F.map f₀₁).toFunctor.obj X)) =
    CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₂ f₂₃ f ⋯).hom.toNatTrans.app X)
      ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom.toNatTrans.app X))
-- Std.Do.PostCond
_private.Std.Do.PostCond.0.Std.Do.PostShape.args.match_1.eq_3 : ∀ (motive : Std.Do.PostShape → Sort u_2) (ε : Type u_1) (s : Std.Do.PostShape)
  (h_1 : Unit → motive Std.Do.PostShape.pure)
  (h_2 : (σ : Type u_1) → (s : Std.Do.PostShape) → motive (Std.Do.PostShape.arg σ s))
  (h_3 : (ε : Type u_1) → (s : Std.Do.PostShape) → motive (Std.Do.PostShape.except ε s)),
  (match Std.Do.PostShape.except ε s with
    | Std.Do.PostShape.pure => h_1 ()
    | Std.Do.PostShape.arg σ s => h_2 σ s
    | Std.Do.PostShape.except ε s => h_3 ε s) =
    h_3 ε s
-- Mathlib.FieldTheory.AlgebraicClosure
/-- If `E` and `K` are isomorphic as `F`-algebras, then `algebraicClosure F E` and
`algebraicClosure F K` are also isomorphic as `F`-algebras.  -/
algebraicClosure.algEquivOfAlgEquiv : {F : Type u_1} →
  {E : Type u_2} →
    [inst : Field F] →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          {K : Type u_3} →
            [inst_3 : Field K] →
              [inst_4 : Algebra F K] → (E ≃ₐ[F] K) → ↥(algebraicClosure F E) ≃ₐ[F] ↥(algebraicClosure F K)
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.filterMap_replicate.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → (Unit → motive none) → ((b : β) → motive (some b)) → motive x
-- Lean.Elab.DefView
/-- Definitions of this mutual block.  -/
Lean.Elab.DefsParsedSnapshot.defs : Lean.Elab.DefsParsedSnapshot → Array Lean.Elab.DefParsed
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get!_inter_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [inst : Inhabited α] [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₂ → (t₁ ∩ t₂).get! k = t₁.get! k
-- Std.Tactic.BVDecide.LRAT.Parser
_private.Std.Tactic.BVDecide.LRAT.Parser.0.Std.Tactic.BVDecide.LRAT.Parser.Text.parseActions.go : Array Std.Tactic.BVDecide.LRAT.IntAction →
  Std.Internal.Parsec.ByteArray.Parser (Array Std.Tactic.BVDecide.LRAT.IntAction)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- Given `α : L ⋙ F' ⟶ F`, the property `F'.IsRightKanExtension α` asserts that
`(F', α)` is a terminal object in the category `RightExtension L F`, i.e. that `(F', α)`
is a right Kan extension of `F` along `L`.  -/
CategoryTheory.Functor.IsRightKanExtension : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            (F' : CategoryTheory.Functor D H) →
              {L : CategoryTheory.Functor C D} → {F : CategoryTheory.Functor C H} → (L.comp F' ⟶ F) → Prop
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokensOptions.full : Lean.Lsp.SemanticTokensOptions → Bool
-- Mathlib.Algebra.Order.CauSeq.BigOperators
IsCauSeq.of_mono_bounded : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] [Archimedean α] (f : ℕ → α)
  {a : α} {m : ℕ}, (∀ n ≥ m, |f n| ≤ a) → (∀ n ≥ m, f n ≤ f n.succ) → IsCauSeq abs f
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
/-- The Lévy-Prokhorov distance `levyProkhorovDist` makes `ProbabilityMeasure Ω` a pseudometric
space. The instance is recorded on the type synonym
`LevyProkhorov (ProbabilityMeasure Ω) := ProbabilityMeasure Ω`.

Note: For this pseudometric to give the topology of convergence in distribution, one must
furthermore assume that `Ω` is separable.  -/
MeasureTheory.LevyProkhorov.instPseudoMetricSpaceProbabilityMeasure : {Ω : Type u_1} →
  [inst : MeasurableSpace Ω] →
    [inst_1 : PseudoEMetricSpace Ω] →
      [OpensMeasurableSpace Ω] → PseudoMetricSpace (MeasureTheory.LevyProkhorov (MeasureTheory.ProbabilityMeasure Ω))
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.succ : Nat.Primrec' fun v => v.head.succ
-- Mathlib.Data.Rel.Separated
SetRel.IsSeparated.eq_1 : ∀ {X : Type u_1} (R : SetRel X X) (s : Set X), R.IsSeparated s = s.Pairwise fun x y => (x, y) ∉ R
-- Mathlib.RingTheory.LocalIso
Algebra.IsLocalIso.of_span_range_eq_top : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {ι : Type u_3}
  (f : ι → S),
  Ideal.span (Set.range f) = ⊤ →
    ∀ (T : ι → Type u_4) [inst_3 : (i : ι) → CommSemiring (T i)] [inst_4 : (i : ι) → Algebra R (T i)]
      [inst_5 : (i : ι) → Algebra S (T i)] [∀ (i : ι), IsScalarTower R S (T i)]
      [∀ (i : ι), IsLocalization.Away (f i) (T i)] [∀ (i : ι), Algebra.IsLocalIso R (T i)], Algebra.IsLocalIso R S
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey!_insert_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {k : α} {v : β}, t.isEmpty = true → (t.insert k v).minKey! = k
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
/-- If the union of the `ι`-indexed family `s` is cofinal and `ι` is smaller than the cofinality,
then `s` has a cofinal member.  -/
isCofinal_of_isCofinal_iUnion : ∀ {α ι : Type u_1} [inst : LinearOrder α] {s : ι → Set α},
  IsCofinal (⋃ i, s i) → Cardinal.mk ι < Order.cof α → ∃ i, IsCofinal (s i)
-- Init.Data.List.Nat.Count
List.Sublist.le_count : ∀ {α : Type u_1} [inst : BEq α] {l₁ l₂ : List α},
  l₁.Sublist l₂ → ∀ (a : α), List.count a l₂ - (l₂.length - l₁.length) ≤ List.count a l₁
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.inf_principal_neBot_iff : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → ∀ {t : Set α}, (l ⊓ Filter.principal t).NeBot ↔ ∀ ⦃i : ι⦄, p i → (s i ∩ t).Nonempty
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.chromaticNumber_eq_zero_of_isEmpty : ∀ {V : Type u} {G : SimpleGraph V} [IsEmpty V], G.chromaticNumber = 0
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.normSMulClassSeminormedAddCommGroupToPi : ∀ (p : ENNReal) {ι : Type u_2} (α : ι → Type u_3) [inst : Fact (1 ≤ p)] [inst_1 : Fintype ι]
  [inst_2 : (i : ι) → SeminormedAddCommGroup (α i)] {R : Type u_5} [inst_3 : SeminormedRing R]
  [inst_4 : (i : ι) → Module R (α i)] [∀ (i : ι), NormSMulClass R (α i)], NormSMulClass R ((i : ι) → α i)
-- Mathlib.Algebra.Order.Sub.Basic
tsub_lt_of_lt : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] {a b c : α}, a < b → a - c < b
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndepOn_iff_linearCombinationOnₛ : ∀ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M], LinearIndepOn R v s ↔ Function.Injective ⇑(Finsupp.linearCombinationOn ι M R v s)
-- Mathlib.RingTheory.Polynomial.DegreeLT
/-- Basis for `R[X]_m × R[X]_n`.  -/
Polynomial.degreeLT.basisProd : (R : Type u_1) →
  [inst : Semiring R] →
    (m n : ℕ) → Module.Basis (Fin (m + n)) R (↥(Polynomial.degreeLT R m) × ↥(Polynomial.degreeLT R n))
-- Mathlib.LinearAlgebra.SModEq.Basic
SModEq.pow : ∀ {A : Type u_3} [inst : CommRing A] {I : Ideal A} {x y : A} (n : ℕ), x ≡ y [SMOD I] → x ^ n ≡ y ^ n [SMOD I]
-- Mathlib.Order.Heyting.Regular
/-- A decidable proposition is intuitionistically Heyting-regular.  -/
Heyting.isRegular_of_decidable : ∀ (p : Prop) [Decidable p], Heyting.IsRegular p
-- Lean.Data.Json.Basic
Lean.instInhabitedJson : Inhabited Lean.Json
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.mk.sizeOf_spec : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} [inst_2 : SizeOf B] [inst_3 : SizeOf C] (app : (a : B) → F.obj a ⟶ G.obj a)
  (naturality :
    {a b : B} →
      (f : a ⟶ b) →
        CategoryTheory.CategoryStruct.comp (F.map f) (app b) ≅ CategoryTheory.CategoryStruct.comp (app a) (G.map f))
  (naturality_naturality :
    autoParam
      (∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (app b))
            (naturality g).hom =
          CategoryTheory.CategoryStruct.comp (naturality f).hom
            (CategoryTheory.Bicategory.whiskerLeft (app a) (G.map₂ η)))
      CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality._autoParam)
  (naturality_id :
    autoParam
      (∀ (a : B),
        CategoryTheory.CategoryStruct.comp (naturality (CategoryTheory.CategoryStruct.id a)).hom
            (CategoryTheory.Bicategory.whiskerLeft (app a) (G.mapId a).hom) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a).hom (app a))
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (app a)).hom
              (CategoryTheory.Bicategory.rightUnitor (app a)).inv))
      CategoryTheory.Pseudofunctor.StrongTrans.naturality_id._autoParam)
  (naturality_comp :
    autoParam
      (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
        CategoryTheory.CategoryStruct.comp (naturality (CategoryTheory.CategoryStruct.comp f g)).hom
            (CategoryTheory.Bicategory.whiskerLeft (app a) (G.mapComp f g).hom) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g).hom (app c))
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (app c)).hom
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (naturality g).hom)
                (CategoryTheory.CategoryStruct.comp
                  (CategoryTheory.Bicategory.associator (F.map f) (app b) (G.map g)).inv
                  (CategoryTheory.CategoryStruct.comp
                    (CategoryTheory.Bicategory.whiskerRight (naturality f).hom (G.map g))
                    (CategoryTheory.Bicategory.associator (app a) (G.map f) (G.map g)).hom)))))
      CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp._autoParam),
  sizeOf
      { app := app, naturality := naturality, naturality_naturality := naturality_naturality,
        naturality_id := naturality_id, naturality_comp := naturality_comp } =
    1
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.IsHomogeneous.coeff_eq_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {f : MvPowerSeries σ R} {p : ℕ},
  f.IsHomogeneous p → ∀ {d : σ →₀ ℕ}, Finsupp.degree d ≠ p → (MvPowerSeries.coeff d) f = 0
-- Mathlib.CategoryTheory.Galois.Prorepresentability
/-- Functorial isomorphism `Aut A ≅ F.obj A` for Galois objects `A`.  -/
CategoryTheory.PreGaloisCategory.autIsoFibers : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [inst_1 : CategoryTheory.GaloisCategory C] →
      (F : CategoryTheory.Functor C FintypeCat) →
        [CategoryTheory.PreGaloisCategory.FiberFunctor F] →
          (CategoryTheory.PreGaloisCategory.autGaloisSystem F).comp (CategoryTheory.forget GrpCat) ≅
            (CategoryTheory.PreGaloisCategory.PointedGaloisObject.incl F).comp (F.comp FintypeCat.incl)
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.curryAlgEquiv.eq_1 : ∀ (R : Type u_1) {A : Type u_4} {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddMonoid M] [inst_4 : AddMonoid N],
  AddMonoidAlgebra.curryAlgEquiv R =
    { toEquiv := AddMonoidAlgebra.curryRingEquiv.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
-- Mathlib.RingTheory.Finiteness.Basic
AlgHom.Finite.of_surjective : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B), Function.Surjective ⇑f → f.Finite
-- Aesop.Tree.Data
Aesop.Goal.mvars : Aesop.Goal → Aesop.UnorderedArraySet Lean.MVarId
-- Mathlib.Tactic.FunProp.Theorems
/-- Pi theorem e.g. `∀ y, Continuous (f · y) → Continuous fun x y ↦ f x y`  -/
Mathlib.Meta.FunProp.LambdaTheoremType.pi : Mathlib.Meta.FunProp.LambdaTheoremType
-- Mathlib.Topology.UniformSpace.Ultra.Basic
/-- A uniform space with a nonarchimedean uniformity is zero-dimensional.  -/
TopologicalSpace.isTopologicalBasis_clopens : ∀ {X : Type u_1} [inst : UniformSpace X] [IsUltraUniformity X], TopologicalSpace.IsTopologicalBasis {s | IsClopen s}
-- Qq.MetaM
Qq.MaybeDefEq.notDefEq.sizeOf_spec : ∀ {u : Lean.Level}
  {α :
    let u := u;
    Q(Sort u)}
  {a b : Q(«$α»)}, sizeOf Qq.MaybeDefEq.notDefEq = 1
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- Schwartz functions as continuous functions  -/
SchwartzMap.toContinuousMap : {E : Type u_5} →
  {F : Type u_6} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] → [inst_3 : NormedSpace ℝ F] → SchwartzMap E F → C(E, F)
-- Lean.Meta.Eqns
Lean.Meta.EqnsExtState.mapInv : Lean.Meta.EqnsExtState → Lean.PHashMap Lean.Name Lean.Name
-- Mathlib.Analysis.SpecialFunctions.Exp
/-- The real exponential function tends to `1` at `0`.  -/
Real.tendsto_exp_nhds_zero_nhds_one : Filter.Tendsto Real.exp (nhds 0) (nhds 1)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.IsImage.isoExt_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  {F F' : CategoryTheory.Limits.MonoFactorisation f} (hF : CategoryTheory.Limits.IsImage F)
  (hF' : CategoryTheory.Limits.IsImage F'), (hF.isoExt hF').hom = hF.lift F'
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.leftOp : Cᵒᵖ ⥤ D` reflects limits of shape `Jᵒᵖ`, then `F : C ⥤ Dᵒᵖ` reflects colimits
of shape `J`.  -/
CategoryTheory.Limits.reflectsColimitsOfShape_of_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C Dᵒᵖ)
  [CategoryTheory.Limits.ReflectsLimitsOfShape Jᵒᵖ F.leftOp], CategoryTheory.Limits.ReflectsColimitsOfShape J F
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.recOn.eq_1 : ∀ {α : Type u_1} {motive : FreeMonoid α → Sort u_6} (xs : FreeMonoid α) (one : motive 1)
  (of_mul : (x : α) → (xs : FreeMonoid α) → motive xs → motive (FreeMonoid.of x * xs)),
  FreeMonoid.recOn xs one of_mul = List.rec one of_mul xs
-- Mathlib.Topology.Compactness.CountablyCompact
/-- The union of two countably compact sets is countably compact.  -/
IsCountablyCompact.union : ∀ {E : Type u_2} [inst : TopologicalSpace E] {A B : Set E},
  IsCountablyCompact A → IsCountablyCompact B → IsCountablyCompact (A ∪ B)
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.nnrealPart_smul_neg : ∀ {α : Type u_2} [inst : TopologicalSpace α] (f : CompactlySupportedContinuousMap α ℝ) {a : ℝ},
  a ≤ 0 → (a • f).nnrealPart = (-a).toNNReal • (-f).nnrealPart
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremKind.fwd.sizeOf_spec : sizeOf Lean.Meta.Grind.EMatchTheoremKind.fwd = 1
-- Mathlib.Analysis.Complex.Periodic
Function.Periodic.invQParam.eq_1 : ∀ (h : ℝ) (q : ℂ), Function.Periodic.invQParam h q = ↑h / (2 * ↑Real.pi * Complex.I) * Complex.log q
-- Init.Data.BitVec.Lemmas
BitVec.getElem_ushiftRight : ∀ {w : ℕ} (x : BitVec w) (i n : ℕ) (h : i < w), (x >>> n)[i] = x.getLsbD (n + i)
-- Mathlib.Order.Filter.Tendsto
Filter.tendsto_iInf : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : α → β} {x : Filter α} {y : ι → Filter β},
  Filter.Tendsto f x (⨅ i, y i) ↔ ∀ (i : ι), Filter.Tendsto f x (y i)
-- Lean.Elab.InfoTree.Types
Lean.Elab.ContextInfo.toCommandContextInfo : Lean.Elab.ContextInfo → Lean.Elab.CommandContextInfo
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
/-- Given an entourage `U` and a time `n`, a minimal dynamical cover by `U ○ U` has a smaller
cardinality than a maximal dynamical net by `U`. This lemma is the second of two key results to
compare two versions topological entropy: with cover and with nets.  -/
Dynamics.coverMincard_le_netMaxcard : ∀ {X : Type u_1} {U : SetRel X X} (T : X → X) (F : Set X) [U.IsRefl] [U.IsSymm] (n : ℕ),
  Dynamics.coverMincard T F (U.comp U) n ≤ Dynamics.netMaxcard T F U n
-- Lean.Widget.InteractiveGoal
Lean.Widget.InteractiveGoals.mk : Array Lean.Widget.InteractiveGoal → Lean.Widget.InteractiveGoals
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
CategoryTheory.HasLiftingProperty.transfiniteComposition.sqFunctor_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) {X Y : C} (p : X ⟶ Y) (f : F.obj ⊥ ⟶ X)
  (g : c.pt ⟶ Y) {X_1 Y_1 : Jᵒᵖ} (α : X_1 ⟶ Y_1),
  (CategoryTheory.HasLiftingProperty.transfiniteComposition.sqFunctor c p f g).map α =
    TypeCat.ofHom fun sq' => sq'.map α.unop
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bsup_id_succ : ∀ (o : Ordinal.{u}), ((Order.succ o).bsup fun x x_1 => x) = o
-- Mathlib.Order.CompleteLattice.Basic
Set.BijOn.iInf_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CompleteLattice α] {s : Set β} {t : Set γ} {f : β → γ}
  (g : γ → α), Set.BijOn f s t → ⨅ x ∈ s, g (f x) = ⨅ y ∈ t, g y
-- Mathlib.RingTheory.Artinian.Module
/-- [Stacks Tag 00J7](https://stacks.math.columbia.edu/tag/00J7) -/
IsArtinianRing.setOfPred_isMaximal_finite : ∀ (R : Type u_1) [inst : CommSemiring R] [IsArtinianRing R], {I | I.IsMaximal}.Finite
-- Mathlib.Geometry.Convex.Cone.Face.Basic
PointedCone.IsFaceOf.mem_of_add_mem_right : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {C F : PointedCone R M},
  F.IsFaceOf C → ∀ {x y : M}, x ∈ C → y ∈ C → x + y ∈ F → y ∈ F
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.Stmt.goto.inj : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {a a_1 : Γ → σ → Λ},
  Turing.TM1.Stmt.goto a = Turing.TM1.Stmt.goto a_1 → a = a_1
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
_private.Mathlib.Analysis.InnerProductSpace.Orthonormal.0.«term⟪_,_⟫_1» : Lean.ParserDescr
-- Mathlib.Topology.Instances.NNReal.Lemmas
NNReal.hasSum_real_toNNReal_of_nonneg : ∀ {α : Type u_2} {L : SummationFilter α} {f : α → ℝ},
  (∀ (n : α), 0 ≤ f n) → Summable f L → HasSum (fun n => (f n).toNNReal) (∑'[L] (n : α), f n).toNNReal L
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheorems.mk.sizeOf_spec : ∀ (pre post : Lean.Meta.SimpTheoremTree) (lemmaNames : Lean.PHashSet Lean.Meta.Origin)
  (toUnfold : Lean.PHashSet Lean.Name) (erased : Lean.PHashSet Lean.Meta.Origin)
  (toUnfoldThms : Lean.PHashMap Lean.Name (Array Lean.Name)),
  sizeOf
      { pre := pre, post := post, lemmaNames := lemmaNames, toUnfold := toUnfold, erased := erased,
        toUnfoldThms := toUnfoldThms } =
    1 + sizeOf pre + sizeOf post + sizeOf lemmaNames + sizeOf toUnfold + sizeOf erased + sizeOf toUnfoldThms
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_inter_le_size_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (m₁ ∩ m₂).size ≤ m₁.size
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs
BirdDet.sumFrom.induct : ∀ (n : ℕ) (motive : ℕ → Prop),
  (∀ x < n, motive (x + 1) → motive x) → (∀ (x : ℕ), ¬x < n → motive x) → ∀ (lo : ℕ), motive lo
-- Init.Data.Order.PackageFactories
Std.FactoryInstances.instMaxOfOrd : {α : Type u} → [Ord α] → Max α
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.Hom.ext' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.Mon C} {f g : M ⟶ N}, f.hom = g.hom → f = g
-- Mathlib.RingTheory.Jacobson.Radical
/-- A form of Nakayama's lemma for modules over noncommutative rings.  -/
Submodule.FG.eq_bot_of_le_jacobson_smul : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Submodule R M},
  N.FG → N ≤ Ring.jacobson R • N → N = ⊥
-- Mathlib.Tactic.Linarith.Datatypes
/-- The name of the preprocessor, populated automatically, to create linkable trace messages.  -/
Mathlib.Tactic.Linarith.PreprocessorBase.name : Mathlib.Tactic.Linarith.PreprocessorBase → Lean.Name
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.polarCoord_source : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  (NumberField.mixedEmbedding.polarCoord K).source = Set.univ ×ˢ Set.univ.pi fun i => Complex.polarCoord.source
-- Mathlib.NumberTheory.Modular
ModularGroup.fdo.eq_1 : ModularGroup.fdo = {z | 1 < Complex.normSq ↑z ∧ |z.re| < 1 / 2}
-- Init.Data.Vector.Zip
Vector.unzip_zip : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {as : Vector α n} {bs : Vector β n}, (as.zip bs).unzip = (as, bs)
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.zmodEquivZPowers_symm_apply_pow : ∀ {R : Type u_4} {k : ℕ} [inst : CommRing R] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) (i : ℕ),
  h.zmodEquivZPowers.symm (Additive.ofMul ⟨ζ ^ i, ⋯⟩) = ↑i
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.opcyclesIsoH_inv_hom_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.opcyclesIsoH_inv_hom_id._auto_1),
  CategoryTheory.CategoryStruct.comp (X.opcyclesIsoH f n₀ n₁ hn₁).inv
      (X.fromOpcycles f (CategoryTheory.CategoryStruct.id i₁) f ⋯ n₁) =
    CategoryTheory.CategoryStruct.id ((X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f))
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.instSetLike.eq_1 : ∀ {G : Type u_1} [inst : Group G], Subgroup.instSetLike = { coe := fun s => s.carrier, coe_injective := ⋯ }
-- Mathlib.Order.Bounded
Set.bounded_gt_Ioi : ∀ {α : Type u_1} [inst : Preorder α] (a : α), Set.Bounded (fun x1 x2 => x1 > x2) (Set.Ioi a)
-- Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
/-- Given `i : Fin (n + 2)`, this is the morphism `⦋n⦌ ⟶ ⦋1⦌` in the simplex
category which corresponds to the monotone map `Fin (n + 1) → Fin 2` which
takes `i` times the value `0`.  -/
SimplexCategory.toMk₁ : {n : ℕ} → Fin (n + 2) → ({ len := n } ⟶ { len := 1 })
-- Mathlib.Data.Finset.Powerset
Finset.powerset_image : ∀ {α : Type u_1} {s : Finset α} {β : Type u_2} [inst : DecidableEq β] {f : α → β},
  (Finset.image f s).powerset = Finset.image (fun x => Finset.image f x) s.powerset