mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
/-- For a functor `G : C ⥤ D`, and an object `U : D`, `Presieve.coverByImage G U` is the presieve
of `U` consisting of those arrows that factor through images of `G`.
 -/
CategoryTheory.Presieve.coverByImage : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] → CategoryTheory.Functor C D → (U : D) → CategoryTheory.Presieve U
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- The induced map from the quotient by the kernel to the codomain.  -/
QuotientAddGroup.kerLift : {G : Type u} → [inst : AddGroup G] → {H : Type v} → [inst_1 : AddGroup H] → (φ : G →+ H) → G ⧸ φ.ker →+ H
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.smeval_C : ∀ {R : Type u_1} [inst : Semiring R] (r : R) {S : Type u_2} [inst_1 : AddCommMonoid S] [inst_2 : Pow S ℕ]
  [inst_3 : MulActionWithZero R S] (x : S), (Polynomial.C r).smeval x = r • x ^ 0
-- Mathlib.RingTheory.KrullDimension.Basic
Ideal.mem_minimalPrimes_iff_isPrime : ∀ {R : Type u_1} [inst : CommSemiring R] [Ring.KrullDimLE 0 R] {I : Ideal R}, I ∈ minimalPrimes R ↔ I.IsPrime
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
CategoryTheory.ObjectProperty.instIsClosedUnderLimitsOfShapeDiscretePEmptyOfContainsZeroOfIsClosedUnderIsomorphisms : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) [P.ContainsZero]
  [P.IsClosedUnderIsomorphisms], P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- `AddMonoidAlgebra.coeff` as an equiv.  -/
AddMonoidAlgebra.coeffEquiv : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → AddMonoidAlgebra R M ≃ (M →₀ R)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableWithinAt.comp_of_preimage_mem_nhdsWithin : ∀ {𝕜 : 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'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {f : M → M'} (x : M) {s : Set M} {g : M' → M''} {u : Set M'},
  MDiffAt[u] g (f x) → MDiffAt[s] f x → f ⁻¹' u ∈ nhdsWithin x s → MDiffAt[s] (g ∘ f) x
-- Mathlib.CategoryTheory.Linear.Yoneda
CategoryTheory.full_linearCoyoneda : ∀ (R : Type w) [inst : Ring R] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C], (CategoryTheory.linearCoyoneda R C).Full
-- Mathlib.RingTheory.Extension.Basic
/-- A hom between extensions as an algebra homomorphism.  -/
Algebra.Extension.Hom.toAlgHom : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {P : Algebra.Extension R S} →
            {R' : Type u_1} →
              {S' : Type u_2} →
                [inst_3 : CommRing R'] →
                  [inst_4 : CommRing S'] →
                    [inst_5 : Algebra R' S'] →
                      {P' : Algebra.Extension R' S'} →
                        [inst_6 : Algebra R R'] →
                          [inst_7 : Algebra S S'] →
                            [inst_8 : Algebra R S'] → [inst_9 : IsScalarTower R R' S'] → P.Hom P' → P.Ring →ₐ[R] P'.Ring
-- Mathlib.Analysis.Complex.Basic
Complex.equivRealProdCLM_apply : ∀ (a : ℂ), Complex.equivRealProdCLM a = (a.re, a.im)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.π_comp_H2Iso_hom : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupCohomology.π A 2) (groupCohomology.H2Iso A).hom =
    CategoryTheory.CategoryStruct.comp (groupCohomology.isoCocycles₂ A).hom
      (groupCohomology.shortComplexH2 A).moduleCatLeftHomologyData.π
-- Init.GrindInstances.ToInt
Lean.Grind.instOfNatFinCoOfNatIntCast : ∀ {n : ℕ} [inst : NeZero n], Lean.Grind.ToInt.OfNat (Fin n) (Lean.Grind.IntInterval.co 0 ↑n)
-- Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
/-- If a cocone `c` over a functor `G : Grothendieck F ⥤ H` is a colimit, then the induced cocone
`coconeOfFiberwiseCocone G c`  -/
CategoryTheory.Limits.isColimitCoconeOfFiberwiseCocone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F : CategoryTheory.Functor C CategoryTheory.Cat} →
      {H : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} H] →
          {G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H} →
            [inst_2 :
                ∀ {X Y : C} (f : X ⟶ Y),
                  CategoryTheory.Limits.HasColimit
                    ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))] →
              {c : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.fiberwiseColimit G)} →
                CategoryTheory.Limits.IsColimit c →
                  CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeOfCoconeFiberwiseColimit c)
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The product of two `C^n` functions on a domain is `C^n`.  -/
ContDiffOn.mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {n : WithTop ℕ∞} {𝔸 : Type u_3} [inst_3 : NormedRing 𝔸]
  [inst_4 : NormedAlgebra 𝕜 𝔸] {f g : E → 𝔸},
  ContDiffOn 𝕜 n f s → ContDiffOn 𝕜 n g s → ContDiffOn 𝕜 n (fun x => f x * g x) s
-- Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
ContinuousLinearEquiv.compactConvergenceCLMCongrSL_apply : ∀ {𝕜 : Type u_7} {𝕜₂ : Type u_8} {𝕜₃ : Type u_9} {𝕜₄ : Type u_10} {E : Type u_11} {F : Type u_12} {G : Type u_13}
  {H : Type u_14} [inst : AddCommGroup E] [inst_1 : AddCommGroup F] [inst_2 : AddCommGroup G] [inst_3 : AddCommGroup H]
  [inst_4 : NormedField 𝕜] [inst_5 : NormedField 𝕜₂] [inst_6 : NormedField 𝕜₃] [inst_7 : NormedField 𝕜₄]
  [inst_8 : Module 𝕜 E] [inst_9 : Module 𝕜₂ F] [inst_10 : Module 𝕜₃ G] [inst_11 : Module 𝕜₄ H]
  [inst_12 : TopologicalSpace E] [inst_13 : TopologicalSpace F] [inst_14 : TopologicalSpace G]
  [inst_15 : TopologicalSpace H] [inst_16 : IsTopologicalAddGroup G] [inst_17 : IsTopologicalAddGroup H]
  [inst_18 : ContinuousConstSMul 𝕜₃ G] [inst_19 : ContinuousConstSMul 𝕜₄ H] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜}
  {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄}
  [inst_20 : RingHomInvPair σ₁₂ σ₂₁] [inst_21 : RingHomInvPair σ₂₁ σ₁₂] [inst_22 : RingHomInvPair σ₃₄ σ₄₃]
  [inst_23 : RingHomInvPair σ₄₃ σ₃₄] [inst_24 : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄] [inst_25 : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃]
  [inst_26 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_27 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄]
  [inst_28 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [inst_29 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] (e₁₂ : E ≃SL[σ₁₂] F)
  (e₄₃ : H ≃SL[σ₄₃] G) (φ : CompactConvergenceCLM σ₁₄ E H) (f : F), ⋯ = ⋯
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.mk : {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.MonoidalCategoryStruct C] →
          (actionObj : C → D → D) →
            ({c c' : C} → (c ⟶ c') → (d : D) → actionObj c d ⟶ actionObj c' d) →
              ((c : C) → {d d' : D} → (d ⟶ d') → (actionObj c d ⟶ actionObj c d')) →
                ({c c' : C} → {d d' : D} → (c ⟶ c') → (d ⟶ d') → (actionObj c d ⟶ actionObj c' d')) →
                  ((c c' : C) →
                      (d : D) →
                        actionObj (CategoryTheory.MonoidalCategoryStruct.tensorObj c c') d ≅
                          actionObj c (actionObj c' d)) →
                    ((d : D) → actionObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) d ≅ d) →
                      CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct C D
-- Mathlib.NumberTheory.Divisors
Int.nonempty_divisors : ∀ {z : ℤ}, z.divisors.Nonempty ↔ z ≠ 0
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.Functor.Braided.toMonoidal : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      {inst_2 : CategoryTheory.BraidedCategory C} →
        {D : Type u₂} →
          {inst_3 : CategoryTheory.Category.{v₂, u₂} D} →
            {inst_4 : CategoryTheory.MonoidalCategory D} →
              {inst_5 : CategoryTheory.BraidedCategory D} →
                {F : CategoryTheory.Functor C D} → [self : F.Braided] → F.Monoidal
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRightIso_unitIso_hom_app_left : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  {R₁ R₂ : CategoryTheory.Functor B T} (i : R₁ ≅ R₂) (X : CategoryTheory.Comma L R₁),
  ((CategoryTheory.Comma.mapRightIso L i).unitIso.hom.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.RingTheory.Algebraic.Integral
Algebra.IsAlgebraic.rank_fractionRing : ∀ (R : Type u_1) [inst : CommRing R] (S : Type u) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : FaithfulSMul R S] [Algebra.IsAlgebraic R S] [inst_5 : IsDomain S],
  Module.rank (FractionRing R) (FractionRing S) = Module.rank R S
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.num_div_denom : ∀ {K : Type u} [inst : Field K] (x : RatFunc K),
  (algebraMap (Polynomial K) (RatFunc K)) x.num / (algebraMap (Polynomial K) (RatFunc K)) x.denom = x
-- Mathlib.Analysis.InnerProductSpace.Reproducing
RKHS.instSeminormedAddCommGroupH₀ : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {X : Type u_2} →
      {V : Type u_3} →
        [inst_1 : NormedAddCommGroup V] →
          [inst_2 : InnerProductSpace 𝕜 V] →
            [inst_3 : CompleteSpace V] →
              {K : Matrix X X (V →L[𝕜] V)} → [Fact K.PosSemidef] → SeminormedAddCommGroup (RKHS.H₀ K)
-- Mathlib.Analysis.Calculus.ContDiff.Defs
HasFTaylorSeriesUpToOn.contDiffOn : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {n : ℕ∞} {f' : E → FormalMultilinearSeries 𝕜 E F},
  HasFTaylorSeriesUpToOn (↑n) f f' s → ContDiffOn 𝕜 (↑n) f s
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_castAdd_Iic_castAdd : ∀ {n : ℕ} (m : ℕ) (i : Fin n), Fin.castAdd m ⁻¹' Set.Iic (Fin.castAdd m i) = Set.Iic i
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.IsUniversal.hom_desc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {f : CategoryTheory.CostructuredArrow S T} (h : f.IsUniversal) {c : C}
  (η : c ⟶ f.left),
  η = h.lift (CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp (S.map η) f.hom))
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
FixedDetMatrices.ext : ∀ (n : Type u_1) [inst : DecidableEq n] [inst_1 : Fintype n] (R : Type u_2) [inst_2 : CommRing R] {m : R}
  {A B : FixedDetMatrix n R m}, (∀ (i j : n), ↑A i j = ↑B i j) → A = B
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.RelabelNat.State.addGate.congr_simp : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] {idx : ℕ} {decls : Array (Std.Sat.AIG.Decl α)}
  {hidx : idx < decls.size} (state state_1 : Std.Sat.AIG.RelabelNat.State α decls idx),
  state = state_1 →
    ∀ (lhs lhs_1 : Std.Sat.AIG.Fanin) (e_lhs : lhs = lhs_1) (rhs rhs_1 : Std.Sat.AIG.Fanin) (e_rhs : rhs = rhs_1)
      (h : decls[idx] = Std.Sat.AIG.Decl.gate lhs rhs), state.addGate lhs rhs h = state_1.addGate lhs_1 rhs_1 ⋯
-- Mathlib.Algebra.CharP.Algebra
/-- Given `R →+* A`, then `char A ∣ char R`.  -/
CharP.dvd_of_ringHom : ∀ {R : Type u_1} {A : Type u_2} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring A] (f : R →+* A) (p q : ℕ)
  [CharP R p] [CharP A q], q ∣ p
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.liftInner_bind : ∀ {m : Type w → Type w'} {n : Type w → Type w''} {α : Type u} {β : Type v} [inst : Monad m] [inst_1 : Monad n]
  [inst_2 : MonadLiftT m n] [LawfulMonadLiftT m n] [LawfulMonad m] [LawfulMonad n] {x : Std.Iterators.HetT m α}
  {f : α → Std.Iterators.HetT m β},
  Std.Iterators.HetT.liftInner n (x.bind f) =
    (Std.Iterators.HetT.liftInner n x).bind fun a => Std.Iterators.HetT.liftInner n (f a)
-- Mathlib.Algebra.Vertex.VertexOperator
/-- Given an endomorphism-valued function on integers satisfying a pointwise bounded-pole condition,
we produce a vertex operator.  -/
VertexOperator.of_coeff : {R : Type u_1} →
  {V : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module R V] →
          (f : ℤ → Module.End R V) → (∀ (x : V), BddBelow (Function.support fun y => (f y) x)) → VertexOperator R V
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
IsCyclotomicExtension.Rat.ramificationIdx_eq : ∀ (n : ℕ) {m p k : ℕ} [hp : Fact (Nat.Prime p)] (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (P : Ideal (NumberField.RingOfIntegers K)) [hP₁ : P.IsPrime] [hP₂ : P.LiesOver (Ideal.span {↑p})]
  [IsCyclotomicExtension {n} ℚ K], n = p ^ (k + 1) * m → ¬p ∣ m → P.ramificationIdx ℤ = p ^ k * (p - 1)
-- Mathlib.Algebra.Group.Defs
add_left_inj : ∀ {G : Type u_1} [inst : Add G] [IsRightCancelAdd G] (a : G) {b c : G}, b + a = c + a ↔ b = c
-- Init.Data.List.Find
List.findIdx.go.eq_2 : ∀ {α : Type u} (p : α → Bool) (a : ℕ) (a_1 : α) (l : List α),
  List.findIdx.go p (a_1 :: l) a = bif p a_1 then a else List.findIdx.go p l (a + 1)
-- Mathlib.Data.Matrix.DMatrix
/-- The `AddMonoidHom` between spaces of dependently typed matrices
induced by an `AddMonoidHom` between their coefficients.  -/
AddMonoidHom.mapDMatrix : {m : Type u_1} →
  {n : Type u_2} →
    {α : m → n → Type v} →
      [inst : (i : m) → (j : n) → AddMonoid (α i j)] →
        {β : m → n → Type w} →
          [inst_1 : (i : m) → (j : n) → AddMonoid (β i j)] →
            (⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j) → DMatrix m n α →+ DMatrix m n β
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- Reinterpret an `IntermediateField` as a `Subfield`.  -/
IntermediateField.toSubfield : {K : Type u_1} →
  {L : Type u_2} → [inst : Field K] → [inst_1 : Field L] → [inst_2 : Algebra K L] → IntermediateField K L → Subfield L
-- Mathlib.Data.Rel
SetRel.dom_empty : ∀ {α : Type u_1} {β : Type u_2}, ∅.dom = ∅
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
/-- Given a functor `Φ : C ⥤ C`, a natural transformation of the form `𝟭 C ⟶ Φ`
induces a successor structure on `C ⥤ C`.  -/
CategoryTheory.SmallObject.SuccStruct.ofNatTrans : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C C} →
      (CategoryTheory.Functor.id C ⟶ F) → CategoryTheory.SmallObject.SuccStruct (CategoryTheory.Functor C C)
-- Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
/-- A `𝒮ℒ` modular form of odd weight is zero (evaluate at `-1 ∈ SL(2, ℤ)`).  -/
ModularForm.levelOne_odd_weight_eq_zero : ∀ {k : ℤ}, Odd k → ∀ (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k), f = 0
-- Mathlib.Algebra.Lie.DirectSum
DirectSum.toLieAlgebra_apply : ∀ {R : Type u} {ι : Type v} [inst : CommRing R] {L : ι → Type w} [inst_1 : (i : ι) → LieRing (L i)]
  [inst_2 : (i : ι) → LieAlgebra R (L i)] [inst_3 : DecidableEq ι] (L' : Type w₁) [inst_4 : LieRing L']
  [inst_5 : LieAlgebra R L'] (f : (i : ι) → L i →ₗ⁅R⁆ L')
  (hf : Pairwise fun i j => ∀ (x : L i) (y : L j), ⁅(f i) x, (f j) y⁆ = 0) (a : DirectSum ι fun i => L i),
  (DirectSum.toLieAlgebra L' f hf) a = (DirectSum.toModule R ι L' fun i => ↑(f i)) a
-- Mathlib.Order.WellFoundedSet
BddAbove.wellFoundedOn_gt : ∀ {α : Type u_2} {s : Set α} [inst : Preorder α] [LocallyFiniteOrder α],
  BddAbove s → s.WellFoundedOn fun x1 x2 => x1 > x2
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_eq_some_getD_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a : α}
  {fallback : β}, t.contains a = true → t[a]? = some (t.getD a fallback)
-- Batteries.Data.Nat.Bisect
/-- Average of two natural numbers rounded toward zero.  -/
Nat.avg : ℕ → ℕ → ℕ
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.mk.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Zero β] [inst_2 : TopologicalSpace β]
  [inst_3 : SizeOf α] [inst_4 : SizeOf β] (toContinuousMap : C(α, β))
  (zero_at_infty' : Filter.Tendsto toContinuousMap.toFun (Filter.cocompact α) (nhds 0)),
  sizeOf { toContinuousMap := toContinuousMap, zero_at_infty' := zero_at_infty' } = 1 + sizeOf toContinuousMap
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.SimpleFunc.posPart_map_norm : ∀ {α : Type u_1} [inst : MeasurableSpace α] (f : MeasureTheory.SimpleFunc α ℝ),
  MeasureTheory.SimpleFunc.map norm f.posPart = f.posPart
-- Init.MetaTypes
/-- When `true` (default: `true`), reduces `match` expressions applied to constructors.
 -/
Lean.Meta.DSimp.Config.iota : Lean.Meta.DSimp.Config → Bool
-- Mathlib.LinearAlgebra.BilinearForm.TensorProduct
LinearMap.BilinForm.tensorDistrib_tmul : ∀ (R : Type uR) (A : Type uA) {M₁ : Type uM₁} {M₂ : Type uM₂} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : Algebra R A] [inst_5 : Module R M₁]
  [inst_6 : Module A M₁] [inst_7 : SMulCommClass R A M₁] [inst_8 : IsScalarTower R A M₁] [inst_9 : Module R M₂]
  (B₁ : LinearMap.BilinForm A M₁) (B₂ : LinearMap.BilinForm R M₂) (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂),
  (((LinearMap.BilinForm.tensorDistrib R A) (B₁ ⊗ₜ[R] B₂)) (m₁ ⊗ₜ[R] m₂)) (m₁' ⊗ₜ[R] m₂') = (B₂ m₂) m₂' • (B₁ m₁) m₁'
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_right_le_size_union : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h₁ : m₁.WF)
  (h₂ : m₂.WF), m₂.size ≤ (m₁.union m₂ ⋯ ⋯).size
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.valuation.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v v_1 : IsDedekindDomain.HeightOneSpectrum R),
  v = v_1 → IsDedekindDomain.HeightOneSpectrum.valuation K v = IsDedekindDomain.HeightOneSpectrum.valuation K v_1
-- Mathlib.Lean.Meta.KAbstractPositions
/-- Return the subexpression at position `pos` in `e` together with an occurrence number
that allows the expression to be found by `kabstract`.
Return `none` when the subexpression contains loose bound variables.  -/
Lean.Meta.viewKAbstractSubExpr : Lean.Expr → Lean.SubExpr.Pos → Lean.MetaM (Option (Lean.Expr × Option ℕ))
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.tendsto_exp_atBot : Filter.Tendsto Real.exp Filter.atBot (nhds 0)
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.smul_closure : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : Monoid α] [inst_2 : MulDistribMulAction α G] (a : α)
  (s : Set G), a • Subgroup.closure s = Subgroup.closure (a • s)
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
linearIndepOn_congr : ∀ {ι : 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] {w : ι → M}, Set.EqOn v w s → (LinearIndepOn R v s ↔ LinearIndepOn R w s)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PullbackCone.IsLimit.lift_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  {t : CategoryTheory.Limits.PullbackCone f g} (ht : CategoryTheory.Limits.IsLimit t) {W : C} (h : W ⟶ X) (k : W ⟶ Y)
  (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g) {Z_1 : C} (h_1 : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PullbackCone.IsLimit.lift ht h k w)
      (CategoryTheory.CategoryStruct.comp t.fst h_1) =
    CategoryTheory.CategoryStruct.comp h h_1
-- Mathlib.Data.Finsupp.Antidiagonal
Finsupp.antidiagonal'.eq_1 : ∀ {α : Type u} [inst : DecidableEq α] (f : α →₀ ℕ),
  f.antidiagonal' =
    Multiset.toFinsupp
      (Multiset.map (Prod.map ⇑Multiset.toFinsupp ⇑Multiset.toFinsupp) (Finsupp.toMultiset f).antidiagonal)
-- Mathlib.Order.Grade
OrderDual.gradeMaxOrder : {𝕆 : Type u_1} →
  {α : Type u_3} → [inst : Preorder 𝕆] → [inst_1 : Preorder α] → [GradeMinOrder 𝕆 α] → GradeMaxOrder 𝕆ᵒᵈ αᵒᵈ
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
IsProperSemilinearSet.sUnion : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : Set (Set M)},
  S.Finite → (∀ s ∈ S, IsProperSemilinearSet s) → IsProperSemilinearSet (⋃₀ S)
-- Mathlib.RingTheory.Binomial
Ring.choose_zero_pos : ∀ (R : Type u_2) [inst : NonAssocRing R] [inst_1 : Pow R ℕ] [NatPowAssoc R] [inst_3 : BinomialRing R] {k : ℕ},
  0 < k → Ring.choose 0 k = 0
-- Mathlib.Logic.Nonempty
exists_true_iff_nonempty : ∀ {α : Sort u_3}, (∃ x, True) ↔ Nonempty α
-- Init.Data.RArray
_private.Init.Data.RArray.0.Lean.RArray.get_eq_def.match_1.eq_1 : ∀ {α : Type u_1} (motive : Lean.RArray α → Sort u_2) (x : α) (h_1 : (x : α) → motive (Lean.RArray.leaf x))
  (h_2 : (p : ℕ) → (l r : Lean.RArray α) → motive (Lean.RArray.branch p l r)),
  (match Lean.RArray.leaf x with
    | Lean.RArray.leaf x => h_1 x
    | Lean.RArray.branch p l r => h_2 p l r) =
    h_1 x
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- A special case of `ContDiffWithinAt.fderivWithin''` where we require that `s ⊆ g⁻¹(t)`.  -/
ContDiffWithinAt.fderivWithin' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {x₀ : E} {m n : WithTop ℕ∞} {f : E → F → G}
  {g : E → F} {t : Set F},
  ContDiffWithinAt 𝕜 n (Function.uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀) →
    ContDiffWithinAt 𝕜 m g s x₀ →
      (∀ᶠ (x : E) in nhdsWithin x₀ (insert x₀ s), UniqueDiffWithinAt 𝕜 t (g x)) →
        m + 1 ≤ n → s ⊆ g ⁻¹' t → ContDiffWithinAt 𝕜 m (fun x => fderivWithin 𝕜 (f x) t (g x)) s x₀
-- Mathlib.Data.W.Constructions
_private.Mathlib.Data.W.Constructions.0.WType.ofList.match_1.eq_1 : ∀ (γ : Type u_1) (motive : List γ → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (hd : γ) → (tl : List γ) → motive (hd :: tl)),
  (match [] with
    | [] => h_1 ()
    | hd :: tl => h_2 hd tl) =
    h_1 ()
-- Mathlib.Order.DirectedInverseSystem
_private.Mathlib.Order.DirectedInverseSystem.0.InverseSystem.«term_⁺» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Quandle
ShelfHom.toFun_eq_coe : ∀ {S₁ : Type u_1} {S₂ : Type u_2} [inst : Shelf S₁] [inst_1 : Shelf S₂] (f : ShelfHom S₁ S₂), f.toFun = ⇑f
-- Init.Data.Array.Zip
Array.map_prod_right_eq_zip : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → β}, Array.map (fun x => (f x, x)) xs = (Array.map f xs).zip xs
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_right₀ : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [inst : Mul β]
  [MeasurableMul₂ β] {f : ι → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ)) →
      ∀ (i j k : ι), i ≠ j → i ≠ k → ProbabilityTheory.Kernel.IndepFun (f i) (f j * f k) κ μ
-- Batteries.Data.HashMap.Basic
Batteries.HashMap.mk.injEq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (inner inner_1 : Std.HashMap α β),
  ({ inner := inner } = { inner := inner_1 }) = (inner = inner_1)