mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- Reinterpret an equivalence relation as a transitive relation.  -/
CategoryTheory.EquivalenceRelation.toTransitiveRelation : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {R X : C} → {p₁ p₂ : R ⟶ X} → CategoryTheory.EquivalenceRelation p₁ p₂ → CategoryTheory.TransitiveRelation p₁ p₂
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron'.comm₃_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : Z₁₂ ⟶ X₁}
  {w₁₂ : X₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₂}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₂₃}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₃}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (self : CategoryTheory.Triangulated.Octahedron' comm h₁₂ h₂₃ h₁₃) {Z : C}
  (h : (CategoryTheory.shiftFunctor C 1).obj Z₂₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp w₁₃
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).map self.m₃) h) =
    CategoryTheory.CategoryStruct.comp w₂₃ h
-- Mathlib.RingTheory.Congruence.Defs
RingCon.comap_ringHomId : ∀ {R : Type u_5} [inst : NonAssocSemiring R] (J : RingCon R), J.comap (RingHom.id R) = J
-- Mathlib.Tactic.Positivity.Basic
/-- **Alias** of the reverse direction of `Rat.num_ne_zero`. -/
Mathlib.Meta.Positivity.num_ne_zero_of_ne_zero : ∀ {q : ℚ}, q ≠ 0 → q.num ≠ 0
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeffEquiv_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (self : MonoidAlgebra R M),
  MonoidAlgebra.coeffEquiv self = self.coeff
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getD_diff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α],
  m₁.WF →
    m₂.WF → ∀ {k : α} {fallback : β k}, (m₁ \ m₂).getD k fallback = if k ∈ m₂ then fallback else m₁.getD k fallback
-- Mathlib.Order.RelIso.Basic
Subtype.wellFoundedLT : ∀ {α : Type u_1} [inst : LT α] [WellFoundedLT α] (p : α → Prop), WellFoundedLT (Subtype p)
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- **Alias** of `SimpleGraph.IsTree.connected`. -/
SimpleGraph.IsTree.isConnected : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsTree → G.Connected
-- Mathlib.Analysis.Matrix.Spectrum
/-- Eigenvalues of a Hermitian matrix A are in the ℝ spectrum of A.  -/
Matrix.IsHermitian.eigenvalues_mem_spectrum_real : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n]
  (hA : A.IsHermitian) (i : n), hA.eigenvalues i ∈ spectrum ℝ A
-- Mathlib.AlgebraicTopology.SimplicialSet.Op
SSet.opFunctor_map : ∀ {X Y : SSet} (f : X ⟶ Y) {n : SimplexCategoryᵒᵖ} (x : X.op.obj n),
  (CategoryTheory.ConcreteCategory.hom ((SSet.opFunctor.map f).app n)) x =
    SSet.opObjEquiv.symm ((CategoryTheory.ConcreteCategory.hom (f.app n)) (SSet.opObjEquiv x))
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.toList_rio : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] (t : Std.DTreeMap.Internal.Impl α fun x => β),
  t.Ordered →
    ∀ (bound : α),
      Std.Slice.toList (Std.Rio.Sliceable.mkSlice t *...bound) =
        List.filter (fun e => (compare e.1 bound).isLT) (Std.DTreeMap.Internal.Impl.Const.toList t)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
_private.Mathlib.Analysis.InnerProductSpace.Adjoint.0.ContinuousLinearMap.adjointAux_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : CompleteSpace E] (A : E →L[𝕜] F) (x : F),
  (ContinuousLinearMap.adjointAux✝ A) x = (InnerProductSpace.toDual 𝕜 E).symm ((ContinuousLinearMap.toSesqForm A) x)
-- Lean.Elab.Open
Lean.Elab.OpenDecl.M : {m : Type → Type} → Type → Type
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.isLongestRevMatchAtChain_startPos_endPos_iff_toList : ∀ {p : Char → Bool} {s : String.Slice},
  String.Slice.Pattern.Model.IsLongestRevMatchAtChain p s.startPos s.endPos ↔ ∀ c ∈ s.copy.toList, p c = true
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getValue!_map : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [EquivBEq α] [inst_2 : Inhabited γ] {f : α → β → γ}
  {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α},
      Std.Internal.List.getValue! k (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l) =
        (Option.pmap (fun v h => f (Std.Internal.List.getKey k l h) v) (Std.Internal.List.getValue? k l) ⋯).get!
-- Mathlib.CategoryTheory.Adjunction.Quadruple
/-- The right part of an adjoint quadruple `L ⊣ F ⊣ G ⊣ R`.  -/
CategoryTheory.Adjunction.Quadruple.rightTriple : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {L : CategoryTheory.Functor C D} →
          {F : CategoryTheory.Functor D C} →
            {G : CategoryTheory.Functor C D} →
              {R : CategoryTheory.Functor D C} →
                CategoryTheory.Adjunction.Quadruple L F G R → CategoryTheory.Adjunction.Triple F G R
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.ofList_cons : ∀ {α : Type u} {cmp : α → α → Ordering} {hd : α} {tl : List α},
  Std.TreeSet.Raw.ofList (hd :: tl) cmp = (∅.insert hd).insertMany tl
-- Init.Data.String.Lemmas.IsEmpty
String.Slice.isEmpty_sliceTo : ∀ {s : String.Slice} {p : s.Pos}, (s.sliceTo p).isEmpty = true ↔ p = s.startPos
-- Init.Omega.Coeffs
Lean.Omega.Coeffs.get_nil : ∀ {i : ℕ}, Lean.Omega.Coeffs.get [] i = 0
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableWithinAt.congr_of_eventuallyEq : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f f₁ : M → M'} {x : M} {s : Set M},
  MDiffAt[s] f x → f₁ =ᶠ[nhdsWithin x s] f → f₁ x = f x → MDiffAt[s] f₁ x
-- Mathlib.Data.Multiset.Replicate
Multiset.eq_replicate : ∀ {α : Type u_1} {a : α} {n : ℕ} {s : Multiset α}, s = Multiset.replicate n a ↔ s.card = n ∧ ∀ b ∈ s, b = a
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vsub_subset_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {s t : Set β} {u : Set α}, s -ᵥ t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x -ᵥ y ∈ u
-- Mathlib.Data.NNRat.Lemmas
NNRat.mul_den : ∀ (q₁ q₂ : ℚ≥0), (q₁ * q₂).den = q₁.den * q₂.den / (q₁.num * q₂.num).gcd (q₁.den * q₂.den)
-- Mathlib.Tactic.NormNum.PowMod
/-- Evaluates and proves `a^b % m` for natural numbers using fast modular exponentiation.  -/
Mathlib.Meta.NormNum.evalNatPowMod : (a b m : Q(ℕ)) → (c : Q(ℕ)) × Q((«$a».pow «$b»).mod «$m» = «$c»)