mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Basic
/-- View an equivalence of Lie modules as a linear equivalence.  -/
LieModuleEquiv.toLinearEquiv : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {N : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : LieRingModule L M] → [inst_7 : LieRingModule L N] → (M ≃ₗ⁅R,L⁆ N) → M ≃ₗ[R] N
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.instIsScalarTower : ∀ {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : (i : ι) → AddCommMonoid (M₁ i)] [inst_1 : AddCommMonoid M₂]
  [inst_2 : (i : ι) → TopologicalSpace (M₁ i)] [inst_3 : TopologicalSpace M₂] {R' : Type u_1} {R'' : Type u_2}
  {A : Type u_3} [inst_4 : Semiring A] [inst_5 : (i : ι) → Module A (M₁ i)] [inst_6 : Module A M₂]
  [inst_7 : DistribSMul R' M₂] [inst_8 : ContinuousConstSMul R' M₂] [inst_9 : SMulCommClass A R' M₂]
  [inst_10 : DistribSMul R'' M₂] [inst_11 : ContinuousConstSMul R'' M₂] [inst_12 : SMulCommClass A R'' M₂]
  [inst_13 : SMul R' R''] [IsScalarTower R' R'' M₂], IsScalarTower R' R'' (ContinuousMultilinearMap A M₁ M₂)
-- Mathlib.Data.Sum.Interval
Sum.Icc_inl_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] (a₁ a₂ : α),
  Finset.Icc (Sum.inl a₁) (Sum.inl a₂) = Finset.map Function.Embedding.inl (Finset.Icc a₁ a₂)
-- Mathlib.RingTheory.RingHom.Flat
CommRingCat.flat_ofHom_iff : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  CommRingCat.flat (CommRingCat.ofHom f) ↔ f.Flat
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry_cons_of_beq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : (k == a) = true),
  Std.Internal.List.getEntry a (⟨k, v⟩ :: l) ⋯ = ⟨k, v⟩
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.transcendental : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K], Algebra.Transcendental K (RatFunc K)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.adjointify_η_ε : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (η : CategoryTheory.Functor.id C ≅ F.comp G)
  (ε : G.comp F ≅ CategoryTheory.Functor.id D) (X : C),
  CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.Equivalence.adjointifyη η ε).hom.app X))
      (ε.hom.app (F.obj X)) =
    CategoryTheory.CategoryStruct.id (F.obj X)
-- Mathlib.Algebra.Group.Finsupp
Finsupp.instNeg : {ι : Type u_1} → {G : Type u_6} → [inst : NegZeroClass G] → Neg (ι →₀ G)
-- Mathlib.Order.WithBot
WithTop.toDual_lt_toDual_iff : ∀ {α : Type u_1} [inst : LT α] {x y : WithTop α}, WithTop.toDual y < WithTop.toDual x ↔ x < y
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.equivCompletion_symm_apply_toCompletion : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K) (toCompletion : (↑v).Completion),
  ((NumberField.InfinitePlace.Completion.equivCompletion v).symm toCompletion).toCompletion = toCompletion
-- Mathlib.Algebra.Group.Defs
MulOneClass.ext : ∀ {M : Type u} ⦃m₁ m₂ : MulOneClass M⦄, Mul.mul = Mul.mul → m₁ = m₂
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_le_iff : ∀ {α : Type u_1} {M : Matroid α} {X : Set α} {n : ℕ∞}, M.eRk X ≤ n ↔ ∀ ⦃I : Set α⦄, I ⊆ X → M.Indep I → I.encard ≤ n
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.Graph.in₂₀_iff' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a : α} {c : γ},
  (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₂ c) (Sum3.in₀ a) ↔ ∃ x ∈ t, x.2.2 = c ∧ x.1 = a
-- Lean.Util.ForEachExprWhere
Lean.ForEachExprWhere.State.mk.injEq : ∀ (visited : Array Lean.Expr) (checked : Std.HashSet Lean.Expr) (visited_1 : Array Lean.Expr)
  (checked_1 : Std.HashSet Lean.Expr),
  ({ visited := visited, checked := checked } = { visited := visited_1, checked := checked_1 }) =
    (visited = visited_1 ∧ checked = checked_1)
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPInstances : Lean.Options → Bool
-- Mathlib.Algebra.Ring.Parity
even_two_mul : ∀ {α : Type u_2} [inst : Semiring α] (a : α), Even (2 * a)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.Indep.indepSet_of_measurableSet : ∀ {Ω : Type u_1} {m₁ m₂ _mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω},
  ProbabilityTheory.Indep m₁ m₂ μ →
    ∀ {s t : Set Ω}, MeasurableSet s → MeasurableSet t → ProbabilityTheory.IndepSet s t μ
-- Mathlib.MeasureTheory.Measure.Complex
/-- Given `s` and `t` signed measures, `s + it` is a complex measure  -/
MeasureTheory.SignedMeasure.toComplexMeasure : {α : Type u_1} →
  {m : MeasurableSpace α} →
    MeasureTheory.SignedMeasure α → MeasureTheory.SignedMeasure α → MeasureTheory.ComplexMeasure α
-- Init.Omega.Coeffs
/-- Shim for `IntList.sub`.  -/
Lean.Omega.Coeffs.sub : Lean.Omega.Coeffs → Lean.Omega.Coeffs → Lean.Omega.Coeffs
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
/-- An isomorphism of rings induces an isomorphism of residue fields.  -/
Ideal.residueFieldRingEquiv : {A : Type u_3} →
  {B : Type u_4} →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        (J : Ideal A) →
          (K : Ideal B) →
            [inst_2 : J.IsPrime] →
              [inst_3 : K.IsPrime] → (f : A ≃+* B) → J = Ideal.comap f K → J.ResidueField ≃+* K.ResidueField
-- Std.Data.TreeMap.Raw.Slice
Std.TreeMap.Raw.toList_rcc : ∀ {α : Type u} {β : Type v} (cmp : autoParam (α → α → Ordering) Std.TreeMap.Raw.toList_rcc._auto_1) [Std.TransCmp cmp]
  {t : Std.TreeMap.Raw α β cmp},
  t.WF →
    ∀ {lowerBound upperBound : α},
      Std.Slice.toList (Std.Rcc.Sliceable.mkSlice t lowerBound...=upperBound) =
        List.filter (fun e => decide ((cmp e.1 lowerBound).isGE = true ∧ (cmp e.1 upperBound).isLE = true)) t.toList
-- Std.Do.PostCond
Std.Do.ExceptConds.and_eq_left : ∀ {ps : Std.Do.PostShape} {p q : Std.Do.ExceptConds ps}, p.entails q → p = (p ∧ₑ q)