mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.diff_congr : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ t₄ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₃ → t₂.Equiv t₄ → (t₁ \ t₂).Equiv (t₃ \ t₄)
-- Init.Data.Int.LemmasAux
Int.toNat_lt_toNat : ∀ {n m : ℤ}, 0 < m → (n.toNat < m.toNat ↔ n < m)
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.ext_ring_iff : ∀ {N : Type u_3} [inst : AddCommMonoid N] {ι : Type u_7} {R : Type u_12} [inst_1 : CommSemiring R] [inst_2 : Module R N]
  [Finite ι] {f g : R [⋀^ι]→ₗ[R] N}, f = g ↔ (f fun x => 1) = g fun x => 1
-- Mathlib.Logic.Denumerable
/-- A denumerable type is equivalent to `ℕ`.  -/
Denumerable.eqv : (α : Type u_3) → [Denumerable α] → α ≃ ℕ
-- Mathlib.CategoryTheory.Limits.Shapes.KernelPair
/-- The kernel pair provided by `HasPullback f f` fits into an `IsKernelPair`.  -/
CategoryTheory.IsKernelPair.of_hasPullback : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPullback f f],
  CategoryTheory.IsKernelPair f (CategoryTheory.Limits.pullback.fst f f) (CategoryTheory.Limits.pullback.snd f f)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.not_mem_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [EquivBEq α] [LawfulHashable α] {a : α}, a ∉ ∅
-- Init.Data.Sum.Lemmas
Sum.isLeft_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (x : α ⊕ γ),
  (Sum.map f g x).isLeft = x.isLeft
-- Mathlib.RingTheory.Localization.FractionRing
/-- The fraction ring of a commutative ring `R` as a quotient type.

We instantiate this definition as generally as possible, and assume that the
commutative ring `R` is an integral domain only when this is needed for proving.

In this generality, this construction is also known as the *total fraction ring* of `R`.
 -/
FractionRing : (R : Type u_1) → [CommRing R] → Type u_1
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
/-- Alternative constructor for the edge of `Λ[n, i]` with endpoints `a` and `b`,
assuming `3 ≤ n`.  -/
SSet.horn.edge₃ : (n : ℕ) → (i a b : Fin (n + 1)) → a ≤ b → 3 ≤ n → (SSet.horn n i).toSSet.obj (Opposite.op { len := 1 })
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.comap_equiv_eq_map_symm : ∀ {N : Type u_2} [inst : AddZeroClass N] {M : Type u_5} [inst_1 : AddZeroClass M] (f : N ≃+ M) (K : AddSubmonoid M),
  AddSubmonoid.comap f K = AddSubmonoid.map f.symm K
-- Mathlib.NumberTheory.LegendreSymbol.ZModChar
/-- An explicit description of `χ₈'` on integers / naturals  -/
ZMod.χ₈'_int_eq_if_mod_eight : ∀ (n : ℤ), ZMod.χ₈' ↑n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 3 then 1 else -1
-- Mathlib.CategoryTheory.Sites.Types
CategoryTheory.eval.eq_1 : ∀ (P : CategoryTheory.Functor Type uᵒᵖ (Type u)) (α : Type u) (s : P.obj (Opposite.op α)),
  CategoryTheory.eval P α s =
    TypeCat.ofHom fun x => (CategoryTheory.ConcreteCategory.hom (P.map (TypeCat.ofHom fun x_1 => x).op)) s
-- Mathlib.Data.Finmap
Finmap.mem_list_toFinmap : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (xs : List (Sigma β)), a ∈ xs.toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ xs
-- Mathlib.Topology.Algebra.Polynomial
Polynomial.tendsto_abv_atTop : ∀ {R : Type u_1} {k : Type u_2} {α : Type u_3} [inst : Ring R] [inst_1 : Field k] [inst_2 : LinearOrder k]
  [IsStrictOrderedRing k] (abv : R → k) [IsAbsoluteValue abv] (p : Polynomial R),
  0 < p.degree →
    ∀ {l : Filter α} {z : α → R},
      Filter.Tendsto (abv ∘ z) l Filter.atTop → Filter.Tendsto (fun x => abv (Polynomial.eval (z x) p)) l Filter.atTop
-- Mathlib.Topology.UnitInterval
unitInterval.subtype_Ioi_eq_Ioc : ∀ (x : ↑unitInterval), Subtype.val ⁻¹' Set.Ioi ↑x = Set.Ioc x 1
-- Mathlib.Order.BooleanAlgebra.Set
Set.inter_sdiff_left_comm : ∀ {α : Type u_1} (s t u : Set α), s ∩ (t \ u) = t ∩ (s \ u)
-- Mathlib.LinearAlgebra.FixedSubmodule
LinearEquiv.mem_stabilizer_submodule_of_le_fixedSubmodule : ∀ {R : Type u_1} [inst : Semiring R] {V : Type u_3} [inst_1 : AddCommMonoid V] [inst_2 : Module R V] {e : V ≃ₗ[R] V}
  {W : Submodule R V}, W ≤ (↑e).fixedSubmodule → e ∈ MulAction.stabilizer (V ≃ₗ[R] V) W
-- Mathlib.Algebra.BigOperators.Finprod
/-- If the multiplicative supports of `f` and `g` are finite, then the product of `f i * g i` equals
the product of `f i` multiplied by the product of `g i`.  -/
finprod_mul_distrib : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f g : α → M},
  Function.HasFiniteMulSupport f →
    Function.HasFiniteMulSupport g → ∏ᶠ (i : α), f i * g i = (∏ᶠ (i : α), f i) * ∏ᶠ (i : α), g i
-- Std.Http.Data.Status
/-- A custom status code not covered by the standard constructors above.
 -/
Std.Http.Status.other : Std.Http.CustomStatus → Std.Http.Status
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.Cover.trans_comp : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X)
  [inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] [inst_1 : 𝒰.LocallyDirected] {i j k : 𝒰.I₀} (hij : i ⟶ j)
  (hjk : j ⟶ k),
  𝒰.trans (CategoryTheory.CategoryStruct.comp hij hjk) = CategoryTheory.CategoryStruct.comp (𝒰.trans hij) (𝒰.trans hjk)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.comp_smul : ∀ {R : Type r} [inst : CommRing R] {S : Type s} [inst_1 : CommRing S] (f : R →+* S) (P : Fin 3 → R) (u : R),
  ⇑f ∘ (u • P) = f u • ⇑f ∘ P
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.norm_curryMid : ∀ {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (p : Fin (n + 1)) (f : ContinuousMultilinearMap 𝕜 Ei G),
  ‖ContinuousMultilinearMap.curryMid p f‖ = ‖f‖
-- Lean.DocString.Types
Lean.Doc.Block.para.injEq : ∀ {i : Type u} {b : Type v} (contents contents_1 : Array (Lean.Doc.Inline i)),
  (Lean.Doc.Block.para contents = Lean.Doc.Block.para contents_1) = (contents = contents_1)
-- Mathlib.CategoryTheory.Sigma.Basic
CategoryTheory.Sigma.SigmaHom.comp_id : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {X Y : (i : I) × C i}
  (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id Y) = f
-- Mathlib.Data.QPF.Multivariate.Constructions.Prj
/-- `map` on functor `Prj i`  -/
MvQPF.Prj.map : {n : ℕ} → (i : Fin2 n) → ⦃α : TypeVec.{u_1} n⦄ → ⦃β : TypeVec.{u_2} n⦄ → α.Arrow β → MvQPF.Prj i α → MvQPF.Prj i β
-- Init.Data.SInt.Bitwise
Int64.and_eq_neg_one_iff : ∀ {a b : Int64}, a &&& b = -1 ↔ a = -1 ∧ b = -1
-- Mathlib.Analysis.Normed.Order.UpperLower
IsUpperSet.thickening' : ∀ {α : Type u_1} [inst : NormedCommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α] {s : Set α},
  IsUpperSet s → ∀ (ε : ℝ), IsUpperSet (Metric.thickening ε s)
-- Mathlib.Data.PNat.Basic
PNat.natPred_inj : ∀ {m n : ℕ+}, m.natPred = n.natPred ↔ m = n
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_insertMany_list : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List (α × β)} {k : α} {fallback : β},
      (t.insertMany l).getD k fallback =
        (List.findSomeRev?
              (fun x =>
                match x with
                | (a, b) => if cmp a k = Ordering.eq then some b else none)
              l).getD
          (t.getD k fallback)
-- Mathlib.Condensed.Discrete.Colimit
/-- Given a presheaf `F` on `Profinite`, `lanPresheaf F` is the left Kan extension of its
restriction to finite sets along the inclusion functor of finite sets into `Profinite`.
 -/
Condensed.lanPresheaf : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1)) → CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))
-- Mathlib.Data.Finset.Lattice.Fold
/-- **Alias** of the reverse direction of `Finset.sup'_le_iff`. -/
Finset.sup'_le : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (f : β → α) {a : α},
  (∀ b ∈ s, f b ≤ a) → s.sup' H f ≤ a
-- Mathlib.Algebra.Category.Ring.Basic
/-- The object in the category of semirings associated to a type equipped with the appropriate
typeclasses.  -/
SemiRingCat.of : (carrier : Type u) → [semiring : Semiring carrier] → SemiRingCat
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.isBigOTVS_iff_smallSets : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {f : α → E} {g : α → F},
  f =O[𝕜; l] g ↔
    ∀ U ∈ nhds 0, ∀ᶠ (V : Set F) in (nhds 0).smallSets, ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ egauge 𝕜 V (g x)
-- Mathlib.Algebra.Module.LinearMap.Index
LinearEquiv.index_eq_zero : ∀ {M : Type u_1} {N : Type u_2} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] {R : Type u_3} [inst_2 : Ring R]
  [inst_3 : Module R M] [inst_4 : Module R N] [StrongRankCondition R] {e : M ≃ₗ[R] N}, (↑e).index = 0
-- Mathlib.Algebra.BigOperators.GroupWithZero.Action
List.smul_sum : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid N] [inst_1 : DistribSMul M N] {r : M} {l : List N},
  r • l.sum = (List.map (fun x => r • x) l).sum
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- Pulling back with respect to a composition is the composition of the pullbacks.  -/
CategoryTheory.GrothendieckTopology.Cover.pullbackComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {X Y Z : C} →
        (S : J.Cover X) →
          (f : Z ⟶ Y) → (g : Y ⟶ X) → S.pullback (CategoryTheory.CategoryStruct.comp f g) ≅ (S.pullback g).pullback f
-- Mathlib.GroupTheory.MonoidLocalization.DivPairs
/-- Given an additive commutative monoid `M`, a localization map `f` to its Grothendieck group `G`
and a submonoid `s` of `G`, `s.subPairs f` is the submonoid of pairs `(a, b)`
such that `f a - f b ∈ s`.  -/
AddSubmonoid.subPairs : {M : Type u_1} →
  {G : Type u_2} →
    [inst : AddCommMonoid M] → [inst_1 : AddCommGroup G] → ⊤.LocalizationMap G → AddSubmonoid G → AddSubmonoid (M × M)
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.precomposingCat_map : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a b c : B) {X Y : a ⟶ b} (η : X ⟶ Y),
  (CategoryTheory.Bicategory.precomposingCat a b c).map η =
    CategoryTheory.NatTrans.toCatHom₂ ((CategoryTheory.Bicategory.precomposing a b c).map η)
-- Mathlib.Order.Filter.Cofinite
/-- For a function with finite fibres, inverse images of finite sets are finite.  -/
Filter.Tendsto.cofinite_of_finite_preimage_singleton : ∀ {α : Type u_2} {β : Type u_3} {f : α → β},
  (∀ (b : β), Finite ↑(f ⁻¹' {b})) → Filter.Tendsto f Filter.cofinite Filter.cofinite
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- The canonical map from `P.obj (op X)` to the multiequalizer associated to a covering sieve,
assuming such a multiequalizer exists. This will be used in `Sheaf.lean` to provide an equivalent
sheaf condition in terms of multiequalizers.  -/
CategoryTheory.GrothendieckTopology.Cover.toMultiequalizer : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      {J : CategoryTheory.GrothendieckTopology C} →
        {D : Type u₁} →
          [inst_1 : CategoryTheory.Category.{v₁, u₁} D] →
            (S : J.Cover X) →
              (P : CategoryTheory.Functor Cᵒᵖ D) →
                [inst_2 : CategoryTheory.Limits.HasMultiequalizer (S.index P)] →
                  P.obj (Opposite.op X) ⟶ CategoryTheory.Limits.multiequalizer (S.index P)
-- Mathlib.RepresentationTheory.Homological.Resolution
Rep.standardComplex.eq_1 : ∀ (k G : Type u) [inst : CommRing k] [inst_1 : Monoid G],
  Rep.standardComplex k G =
    (AlgebraicTopology.alternatingFaceMapComplex (Rep.{u, u, u} k G)).obj
      (CategoryTheory.Functor.comp (classifyingSpaceUniversalCover G) (Rep.linearization k G))
-- Mathlib.RingTheory.Artinian.Module
/-- A sequence `f` of submodules of an Artinian module,
with the supremum `f (n+1)` and the infimum of `f 0`, ..., `f n` being ⊤,
is eventually ⊤.  -/
IsArtinian.disjoint_partial_infs_eventually_top : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [IsArtinian R M]
  (f : ℕ → Submodule R M),
  (∀ (n : ℕ), Disjoint ((partialSups (⇑OrderDual.toDual ∘ f)) n) (OrderDual.toDual (f (n + 1)))) →
    ∃ n, ∀ (m : ℕ), n ≤ m → f m = ⊤
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey?_empty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp], ∅.maxKey? = none
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Path.insertNew_toList : ∀ {α : Type u_1} {v : α} {p : RBTree.RBNode.Path α}, (p.insertNew v).toList = p.withList [v]
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Split.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) (s : X.Splitting)
  (X_1 : CategoryTheory.SimplicialObject C) (s_1 : X_1.Splitting),
  ({ X := X, s := s } = { X := X_1, s := s_1 }) = (X = X_1 ∧ s ≍ s_1)
-- Mathlib.Data.Set.Semiring
/-- The identity function `Set α → SetSemiring α`.  -/
Set.up : {α : Type u_1} → Set α ≃ SetSemiring α
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.toContIntertwiningMap_trans : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  [inst_10 : AddCommGroup U] [inst_11 : Module R U] [inst_12 : TopologicalSpace U] [inst_13 : IsTopologicalAddGroup U]
  {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} {τ : ContRepresentation R G U} (φ : ρ.Equiv σ)
  (ψ : σ.Equiv τ), ↑(φ.trans ψ) = (↑ψ).comp ↑φ
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
/-- The short complex `Hᵢ(G, X₂) ⟶ Hᵢ(G, X₃) ⟶ Hⱼ(G, X₁)` associated to an exact sequence of
representations `0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0`.  -/
groupHomology.mapShortComplex₃ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)} →
        X.ShortExact → {i j : ℕ} → j + 1 = i → CategoryTheory.ShortComplex (ModuleCat k)
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.lanLiftLeftLift_unit : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : b ⟶ a) (g : c ⟶ a)
  [inst_1 : CategoryTheory.Bicategory.HasLeftKanLift f g],
  (CategoryTheory.Bicategory.lanLiftLeftLift f g).unit = CategoryTheory.Bicategory.lanLiftUnit f g
-- Mathlib.Analysis.InnerProductSpace.Projection.Submodule
/-- The closure of `K` is the full space iff `Kᗮ` is trivial.  -/
Submodule.topologicalClosure_eq_top_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [CompleteSpace E], K.topologicalClosure = ⊤ ↔ Kᗮ = ⊥
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
/-- The type of finite-index normal subgroups of a group.  -/
FiniteIndexNormalSubgroup : (G : Type u_1) → [Group G] → Type u_1
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
AlgebraicTopology.DoldKan.PInfty_f_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (n : ℕ)
  {X Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y) {Z : C}
  (h : (AlgebraicTopology.AlternatingFaceMapComplex.obj Y).X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f.app (Opposite.op { len := n }))
      (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n)
      (CategoryTheory.CategoryStruct.comp (f.app (Opposite.op { len := n })) h)
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
/-- When `star x = x` on the coefficients (such as the real numbers) `conjTranspose` and `transpose`
are the same operation.  -/
Matrix.conjTranspose_eq_transpose_of_trivial : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Star α] [TrivialStar α] (A : Matrix m n α),
  A.conjTranspose = A.transpose
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.toDescentDataFunctor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} (sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j))
  (sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃))
  (D : F.DescentData' sq sq₃),
  (CategoryTheory.Pseudofunctor.DescentData'.toDescentDataFunctor F sq sq₃).obj D = D.descentData
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndepOn_finset_iffₒₛ : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : LinearOrder R] [CanonicallyOrderedAdd R] [AddRightReflectLE R] [IsCancelAdd M]
  [inst_7 : DecidableEq ι] {s : Finset ι},
  LinearIndepOn R v ↑s ↔ ∀ t ⊆ s, ∀ (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i → ∀ i ∈ s, f i = 0
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  (m₁ \ m₂).get? k = if k ∈ m₂ then none else m₁.get? k
-- Mathlib.AlgebraicGeometry.Scheme
/-- The forgetful functor from `Scheme` to `LocallyRingedSpace`.  -/
AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace : CategoryTheory.Functor AlgebraicGeometry.Scheme AlgebraicGeometry.LocallyRingedSpace
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
aemeasurable_restrict_of_monotoneOn : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  [inst_2 : TopologicalSpace β] {mβ : MeasurableSpace β} [BorelSpace β] [inst_4 : LinearOrder α] [OrderTopology α]
  [SecondCountableTopology α] [inst : LinearOrder β] [OrderClosedTopology β] {μ : MeasureTheory.Measure β} {s : Set β},
  MeasurableSet s → ∀ {f : β → α}, MonotoneOn f s → AEMeasurable f (μ.restrict s)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.ValueGroupWithZero.embed.congr_simp : ∀ {R : Type u_2} {Γ : Type u_3} [inst : Ring R] [inst_1 : ValuativeRel R] [inst_2 : LinearOrderedCommGroupWithZero Γ]
  (v : Valuation R Γ) [inst_3 : v.Compatible],
  ValuativeRel.ValueGroupWithZero.embed v = ValuativeRel.ValueGroupWithZero.embed v
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.contains_of_contains_map : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → γ} {k : α}, m.WF → (Std.HashMap.Raw.map f m).contains k = true → m.contains k = true
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.Context.params : Lean.Elab.Tactic.Grind.Context → Lean.Meta.Grind.Params
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
/-- An absolute derivation of `M'` descends as a morphism `M ⟶ M'`.  -/
PresheafOfModules.Derivation.Universal.desc : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} →
          {F : CategoryTheory.Functor C D} →
            {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} →
              {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} →
                {φ : S ⟶ F.op.comp R} →
                  {d : M.Derivation φ} →
                    d.Universal →
                      {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} →
                        M'.Derivation φ → (M ⟶ M')
-- Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
CategoryTheory.SmallObject.SuccStruct.toSuccArrow.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) (X : C),
  Φ.toSuccArrow X = CategoryTheory.Arrow.mk (Φ.toSucc X)
-- Mathlib.Algebra.Colimit.Module
Module.DirectLimit.hom_ext_iff : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_2} [inst_1 : Preorder ι] {G : ι → Type u_3}
  [inst_2 : (i : ι) → AddCommMonoid (G i)] [inst_3 : (i : ι) → Module R (G i)] {f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
  [inst_4 : DecidableEq ι] {P : Type u_4} [inst_5 : AddCommMonoid P] [inst_6 : Module R P]
  {g₁ g₂ : Module.DirectLimit G f →ₗ[R] P},
  g₁ = g₂ ↔ ∀ (i : ι), g₁ ∘ₗ Module.DirectLimit.of R ι G f i = g₂ ∘ₗ Module.DirectLimit.of R ι G f i
-- Mathlib.AlgebraicGeometry.Morphisms.Affine
AlgebraicGeometry.isAffineHom_of_forall_exists_isAffineOpen : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  (∀ (x : ↥Y),
      ∃ U,
        x ∈ U ∧
          AlgebraicGeometry.IsAffineOpen U ∧
            AlgebraicGeometry.IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj U)) →
    AlgebraicGeometry.IsAffineHom f
-- Mathlib.Data.Set.Insert
Set.insert_inter_distrib : ∀ {α : Type u_1} (a : α) (s t : Set α), insert a (s ∩ t) = insert a s ∩ insert a t
-- Mathlib.Algebra.Order.GroupWithZero.Basic
div_le_one₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {a b : G₀},
  0 < b → (a / b ≤ 1 ↔ a ≤ b)
-- Mathlib.CategoryTheory.Monoidal.Category
/-- Tensor product of identity maps is the identity: `𝟙 X₁ ⊗ₘ 𝟙 X₂ = 𝟙 (X₁ ⊗ X₂)`  -/
CategoryTheory.MonoidalCategoryStruct.tensorHom : {C : Type u} →
  {𝒞 : CategoryTheory.Category.{v, u} C} →
    [self : CategoryTheory.MonoidalCategoryStruct C] →
      {X₁ Y₁ X₂ Y₂ : C} →
        (X₁ ⟶ Y₁) →
          (X₂ ⟶ Y₂) →
            (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂ ⟶
              CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ Y₂)
-- Mathlib.Algebra.Homology.TotalComplexShift
HomologicalComplex₂.instHasTotalIntObjUpShiftFunctor₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [K.HasTotal (ComplexShape.up ℤ)],
  ((HomologicalComplex₂.shiftFunctor₁ C x).obj K).HasTotal (ComplexShape.up ℤ)
-- Mathlib.Algebra.Group.Basic
add_eq_of_eq_sub' : ∀ {G : Type u_3} [inst : AddCommGroup G] {a b c : G}, b = c - a → a + b = c
-- Mathlib.Data.Nat.Prime.Pow
Nat.pow_minFac : ∀ {n k : ℕ}, k ≠ 0 → (n ^ k).minFac = n.minFac
-- Init.Data.BitVec.Lemmas
BitVec.allOnes.eq_1 : ∀ (n : ℕ), BitVec.allOnes n = (2 ^ n - 1)#'⋯
-- Mathlib.RingTheory.Extension.ExtendScalars
Algebra.Extension.h1CotangentExtendScalarsEquiv_symm_toLinearMap : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S),
  ↑P.h1CotangentExtendScalarsEquiv.symm =
    Algebra.Extension.H1Cotangent.map (Algebra.Extension.defaultHom P.Ring S P.extendScalars)
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- `r` is the morphism witnessing reflexivity  -/
CategoryTheory.ReflexiveRelation.r : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {R X : C} → {p₁ p₂ : R ⟶ X} → CategoryTheory.ReflexiveRelation p₁ p₂ → (X ⟶ R)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
/-- Use `getElem_edges_eq_edge_getElem_darts` to rewrite in the reverse direction.  -/
SimpleGraph.Walk.edge_getElem_darts : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {i : ℕ} (h : i < p.darts.length),
  p.darts[i].edge = p.edges[i]
-- Mathlib.RingTheory.Ideal.Int
Int.absNorm_under_eq_sInf : ∀ {R : Type u_1} [inst : Ring R] (I : Ideal R), Ideal.absNorm (Ideal.under ℤ I) = sInf {d | 0 < d ∧ ↑d ∈ I}
-- Mathlib.Tactic.Abel
/-- Evaluate a term with coefficient `n`, atom `x` and successor terms `a`.  -/
Mathlib.Tactic.Abel.mkTerm : Lean.Expr → Lean.Expr → Lean.Expr → Mathlib.Tactic.Abel.M Lean.Expr
-- Mathlib.Tactic.FunProp.FunctionData
/-- The function is in uncurried form.  -/
Mathlib.Meta.FunProp.DecompositionResult.uncurried : Mathlib.Meta.FunProp.DecompositionResult