mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂.isoInv.injEq : ∀ (e : Lean.Expr) (isoLift : Mathlib.Tactic.BicategoryLike.IsoLift) (iso : Mathlib.Tactic.BicategoryLike.Mor₂Iso)
  (e_1 : Lean.Expr) (isoLift_1 : Mathlib.Tactic.BicategoryLike.IsoLift) (iso_1 : Mathlib.Tactic.BicategoryLike.Mor₂Iso),
  (Mathlib.Tactic.BicategoryLike.Mor₂.isoInv e isoLift iso =
      Mathlib.Tactic.BicategoryLike.Mor₂.isoInv e_1 isoLift_1 iso_1) =
    (e = e_1 ∧ isoLift = isoLift_1 ∧ iso = iso_1)
-- Mathlib.Data.List.Permutation
List.permutations'Aux_eq_permutationsAux2 : ∀ {α : Type u_1} (t : α) (ts : List α), List.permutations'Aux t ts = (List.permutationsAux2 t [] [ts ++ [t]] ts id).2
-- Mathlib.Topology.NhdsWithin
nhdsWithin_pi_neBot : ∀ {ι : Type u_5} {X : ι → Type u_6} [inst : (i : ι) → TopologicalSpace (X i)] {I : Set ι} {s : (i : ι) → Set (X i)}
  {x : (i : ι) → X i}, (nhdsWithin x (I.pi s)).NeBot ↔ ∀ i ∈ I, (nhdsWithin (x i) (s i)).NeBot
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.finite_countablePartition : ∀ (α : Type u_3) [inst : MeasurableSpace α] [inst_1 : MeasurableSpace.CountablyGenerated α] (n : ℕ),
  (MeasurableSpace.countablePartition α n).Finite
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.leadingCoeff_single : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : LinearOrder B] [inst_2 : OrderBot B]
  {D : A → B} [inst_3 : Nonempty A],
  Function.Injective D → ∀ (a : A) (r : R), AddMonoidAlgebra.leadingCoeff D (AddMonoidAlgebra.single a r) = r
-- Mathlib.Data.QPF.Multivariate.Constructions.Sigma
MvQPF.Sigma.instMvFunctor : {n : ℕ} → {A : Type u} → (F : A → TypeVec.{u} n → Type u) → [(α : A) → MvFunctor (F α)] → MvFunctor (MvQPF.Sigma F)
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.containsThenInsertIfNew.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Raw α β) (a : α) (b : β a),
  m.containsThenInsertIfNew a b =
    if h : 0 < m.buckets.size then
      match Std.DHashMap.Internal.Raw₀.containsThenInsertIfNew ⟨m, h⟩ a b with
      | (previous, ⟨r, property⟩) => (previous, r)
    else (false, m)
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Unbounded.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (state : Std.Mutex (Std.CloseableChannel.Unbounded.State✝ α)),
  sizeOf { state := state } = 1 + sizeOf state
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.forM_eq_forM_toArray : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {m' : Type w → Type w'}
  [inst_2 : Monad m'] [LawfulMonad m'] {f : (a : α) → β a → m' PUnit.{w + 1}},
  m.WF → Std.DHashMap.Raw.forM f m = Array.forM (fun a => f a.fst a.snd) m.toArray
-- Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
/-- A submodule has dimension at most `1` if and only if there is a
single vector, not necessarily in the submodule, such that the
submodule is contained in its span.  -/
rank_submodule_le_one_iff' : ∀ {K : Type u} {V : Type v} [inst : Ring K] [StrongRankCondition K] [inst_2 : AddCommGroup V] [inst_3 : Module K V]
  (s : Submodule K V) [Module.Free K ↥s], Module.rank K ↥s ≤ 1 ↔ ∃ v₀, s ≤ K ∙ v₀
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- Bundle `d ↦ c ⊙ₗ d` as a functor.  -/
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionLeft : {C : Type u_1} →
  (D : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] → C → CategoryTheory.Functor D D
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.maxKey!_alter!_eq_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      (Std.DTreeMap.Internal.Impl.Const.alter! k f t).isEmpty = false →
        ((Std.DTreeMap.Internal.Impl.Const.alter! k f t).maxKey! = k ↔
          (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (compare k' k).isLE = true)
-- Mathlib.ModelTheory.Order
FirstOrder.Language.orderedStructure_iff : ∀ {L : FirstOrder.Language} {M : Type w'} [inst : L.IsOrdered] [inst_1 : L.Structure M] [inst_2 : LE M]
  [inst_3 : FirstOrder.Language.order.Structure M] [FirstOrder.Language.order.OrderedStructure M],
  L.OrderedStructure M ↔ L.orderLHom.IsExpansionOn M
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubAddAction.ofStabilizer.snoc_last : ∀ {G : Type u_1} [inst : AddGroup G] {α : Type u_2} [inst_1 : AddAction G α] {a : α} {n : ℕ}
  (x : Fin n ↪ ↥(SubAddAction.ofStabilizer G a)), (SubAddAction.ofStabilizer.snoc x) (Fin.last n) = a
-- Mathlib.Data.Finset.Lattice.Fold
Finset.ofDual_sup' : ∀ {α : Type u_2} {ι : Type u_5} [inst : SemilatticeInf α] {s : Finset ι} (hs : s.Nonempty) (f : ι → αᵒᵈ),
  OrderDual.ofDual (s.sup' hs f) = s.inf' hs (⇑OrderDual.ofDual ∘ f)
-- Mathlib.RepresentationTheory.Coinvariants
/-- The bilinear map sending `a : A, b : B` to `⟦a ⊗ₜ b⟧` in `(A ⊗[k] B)_G`.  -/
Rep.coinvariantsTensorMk : {k : Type u} →
  {G : Type v} →
    [inst : CommRing k] →
      [inst_1 : Monoid G] → (A B : Rep.{u, u, v} k G) → ↑A →ₗ[k] ↑B →ₗ[k] ↑(((Rep.coinvariantsTensor k G).obj A).obj B)
-- Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.PreprocessorBase.mk : autoParam Lean.Name Mathlib.Tactic.Linarith.PreprocessorBase.name._autoParam →
  String → Mathlib.Tactic.Linarith.PreprocessorBase
-- Mathlib.FieldTheory.Normal.Closure
/-- Normal closures of `K/F` are unique up to F-algebra isomorphisms.  -/
IsNormalClosure.equiv : {F : Type u_1} →
  {K : Type u_2} →
    {L : Type u_3} →
      [inst : Field F] →
        [inst_1 : Field K] →
          [inst_2 : Field L] →
            [inst_3 : Algebra F K] →
              [inst_4 : Algebra F L] →
                {L' : Type u_4} →
                  [inst_5 : Field L'] →
                    [inst_6 : Algebra F L'] → [h : IsNormalClosure F K L] → [h' : IsNormalClosure F K L'] → L ≃ₐ[F] L'
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inlX_sndX : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i j : ι) (hij : c.Rel j i),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX φ i j hij)
      (HomologicalComplex.homotopyCofiber.sndX φ j) =
    0
-- Mathlib.CategoryTheory.ConcreteCategory.Forget
CategoryTheory.ObjectProperty.FullSubcategory.hasForget₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {FC : outParam (C → C → Type u_2)} →
      {CC : outParam (C → Type w)} →
        [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] →
          [inst_2 : CategoryTheory.ConcreteCategory C FC] →
            (P : CategoryTheory.ObjectProperty C) → CategoryTheory.HasForget₂ P.FullSubcategory C
-- Lean.LibrarySuggestions.Basic
/-- A `Suggestion` is essentially just an identifier and a confidence score that the identifier is relevant.
If the premise selection request included information about the intended use (e.g. in the simplifier, in `grind`, etc.)
the score may be adjusted for that application.

 -/
Lean.LibrarySuggestions.Suggestion : Type
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.ResidueField.instAlgebra : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : IsLocalRing R] →
        [inst_2 : CommRing S] →
          [inst_3 : IsLocalRing S] →
            [inst_4 : Algebra R S] →
              [IsLocalHom (algebraMap R S)] → Algebra (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S)
-- Mathlib.Order.Hom.Bounded
/-- Morphisms preserve the bottom element. The preferred spelling is `_root_.map_bot`.  -/
BoundedOrderHomClass.map_bot : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} {inst : LE α} {inst_1 : LE β} {inst_2 : BoundedOrder α}
  {inst_3 : BoundedOrder β} {inst_4 : FunLike F α β} [self : BoundedOrderHomClass F α β] (f : F), f ⊥ = ⊥
-- Init.Data.BitVec.Bitblast
/-- Preliminary overflow flag for fast umulOverflow circuit as introduced in
`Efficient integer multiplication overflow detection circuits` (https://ieeexplore.ieee.org/abstract/document/987767).
 -/
BitVec.resRec : {w : ℕ} → BitVec w → BitVec w → (s : ℕ) → s < w → 0 < s → Bool
-- Mathlib.Condensed.Equivalence
/-- An effective presentation of an `X : Profinite` with respect to the inclusion functor from `Stonean`
 -/
Condensed.StoneanProfinite.stoneanToProfiniteEffectivePresentation : (X : Profinite) → Stonean.toProfinite.EffectivePresentation X
-- Lean.Meta.Match.CaseArraySizes
_private.Lean.Meta.Match.CaseArraySizes.0.Lean.Meta.mkArrayGetLit : Lean.Expr → ℕ → ℕ → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Combinatorics.Enumerative.Bell
Nat.bell.eq_def : ∀ (x : ℕ),
  x.bell =
    match x with
    | 0 => 1
    | n.succ => ∑ i ≤ n, n.choose i * (n - i).bell
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.tendsto_logb_nat_add_one_sub_logb : ∀ {b : ℝ}, Filter.Tendsto (fun k => Real.logb b (↑k + 1) - Real.logb b ↑k) Filter.atTop (nhds 0)
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.neg_mk : ∀ {K : Type u_1} [inst : Field K] (x : K) (hx : x ∈ integralClosure ℤ K), -⟨x, hx⟩ = ⟨-x, ⋯⟩
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
CategoryTheory.Functor.regularEpiOfPreserves_left : ∀ {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_3, u_3} C]
  [inst_1 : CategoryTheory.Category.{v_4, u_4} D] {X Y : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.EffectiveEpi f]
  (F : CategoryTheory.Functor C D) [inst_3 : F.PreservesEffectiveEpis]
  [inst_4 : CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F]
  (c : CategoryTheory.Limits.PullbackCone f f) (hc : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.Functor.regularEpiOfPreserves f F c hc).left = F.map c.fst
-- Mathlib.Order.Basic
/-- The preimage of a decidable order is decidable.  -/
Order.Preimage.decidable : {α : Type u_2} → {β : Type u_3} → (f : α → β) → (s : β → β → Prop) → [H : DecidableRel s] → DecidableRel (f ⁻¹'o s)
-- Mathlib.MeasureTheory.Integral.Layercake
MeasureTheory.Integrable.integral_eq_integral_Ioc_meas_le : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ} {M : ℝ},
  MeasureTheory.Integrable f μ →
    0 ≤ᵐ[μ] f → (f ≤ᵐ[μ] fun x => M) → ∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Set.Ioc 0 M, μ.real {a | t ≤ f a}
-- Mathlib.Order.UpperLower.Basic
isUpperSet_preimage_toDual_iff : ∀ {α : Type u_1} [inst : LE α] {s : Set αᵒᵈ}, IsUpperSet (⇑OrderDual.toDual ⁻¹' s) ↔ IsLowerSet s
-- Init.Data.Iterators.Basic
Std.IterM.IsPlausibleIndirectOutput.trans : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] {it' it : Std.IterM m β} {out : β},
  it'.IsPlausibleIndirectSuccessorOf it → it'.IsPlausibleIndirectOutput out → it.IsPlausibleIndirectOutput out
-- Mathlib.Algebra.Category.Grp.Colimits
QuotientAddGroup.lift.congr_simp : ∀ {G : Type u_1} {M : Type u_4} [inst : AddGroup G] [inst_1 : AddMonoid M] (N : AddSubgroup G) [nN : N.Normal]
  (φ φ_1 : G →+ M) (e_φ : φ = φ_1) (HN : N ≤ φ.ker), QuotientAddGroup.lift N φ HN = QuotientAddGroup.lift N φ_1 ⋯
-- Mathlib.Algebra.Group.Subsemigroup.Operations
MulHom.coe_srange : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N), ↑f.srange = Set.range ⇑f
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.addCommMonoidWithOne : {α : Type u} → [AddCommMonoidWithOne α] → AddCommMonoidWithOne (WithBot α)