mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.Pell
/-- A solution is `1` or `-1` if and only if `y = 0`.  -/
Pell.Solution₁.eq_one_or_neg_one_iff_y_eq_zero : ∀ {d : ℤ} {a : Pell.Solution₁ d}, a = 1 ∨ a = -1 ↔ a.y = 0
-- Mathlib.Topology.Covering.Basic
IsEvenlyCovered.comp_homeomorph_iff : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {I : Type u_3}
  [inst_2 : TopologicalSpace I] {x : X} {E' : Type u_4} [inst_3 : TopologicalSpace E'] (g : E' ≃ₜ E),
  IsEvenlyCovered (f ∘ ⇑g) x I ↔ IsEvenlyCovered f x I
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.sumInl_isExpansionOn : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (M : Type u_1) [inst : L.Structure M] [inst_1 : L'.Structure M],
  FirstOrder.Language.LHom.sumInl.IsExpansionOn M
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
/-- Additive convolution exists when it exists at every point.  -/
DiscreteConvolution.AddConvolutionExists : {M : Type u_1} →
  {S : Type u_2} →
    {E : Type u_3} →
      {E' : Type u_4} →
        {F : Type u_6} →
          [AddMonoid M] →
            [inst : CommSemiring S] →
              [inst_1 : AddCommMonoid E] →
                [inst_2 : AddCommMonoid E'] →
                  [inst_3 : AddCommMonoid F] →
                    [inst_4 : Module S E] →
                      [inst_5 : Module S E'] →
                        [inst_6 : Module S F] → [TopologicalSpace F] → (E →ₗ[S] E' →ₗ[S] F) → (M → E) → (M → E') → Prop
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.mapOfHomotopy.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K₁ L₁ K₂ L₂ : CochainComplex C ℤ} {φ₁ : K₁ ⟶ L₁}
  {φ₂ : K₂ ⟶ L₂} {a : K₁ ⟶ K₂} {b : L₁ ⟶ L₂}
  (H : Homotopy (CategoryTheory.CategoryStruct.comp φ₁ b) (CategoryTheory.CategoryStruct.comp a φ₂)),
  CochainComplex.mappingCone.mapOfHomotopy H =
    CochainComplex.mappingCone.desc φ₁
      ((CochainComplex.HomComplex.Cochain.ofHom a).comp (CochainComplex.mappingCone.inl φ₂)
          CochainComplex.mappingCone.mapOfHomotopy._proof_2 +
        (↑((CochainComplex.HomComplex.Cochain.equivHomotopy (CategoryTheory.CategoryStruct.comp φ₁ b)
                  (CategoryTheory.CategoryStruct.comp a φ₂))
                H)).comp
          (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ₂))
          CochainComplex.mappingCone.mapOfHomotopy._proof_3)
      (CategoryTheory.CategoryStruct.comp b (CochainComplex.mappingCone.inr φ₂)) ⋯
-- Init.Data.UInt.Lemmas
instCommutativeUInt8HAdd : Std.Commutative fun x1 x2 => x1 + x2
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.recOn_zero : ∀ {α : Type u_1} {motive : FreeAddMonoid α → Sort u_6} (zero : motive 0)
  (of_add : (x : α) → (xs : FreeAddMonoid α) → motive xs → motive (FreeAddMonoid.of x + xs)),
  FreeAddMonoid.recOn 0 zero of_add = zero
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.mem_map : ∀ {K : Type u_1} {L : Type u_2} {L' : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Field L']
  [inst_3 : Algebra K L] [inst_4 : Algebra K L'] (S : IntermediateField K L) {f : L →ₐ[K] L'} {y : L'},
  y ∈ IntermediateField.map f S ↔ ∃ x ∈ S, f x = y
-- Init.Data.String.Slice
String.Slice.hash : String.Slice → UInt64
-- Mathlib.Data.Analysis.Topology
Ctop.inter : {α : Type u_1} → {σ : Type u_2} → (self : Ctop α σ) → (a b : σ) → (x : α) → x ∈ self.f a ∩ self.f b → σ
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.completeBasis_apply_of_ne : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (i : { w // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }),
  (NumberField.mixedEmbedding.fundamentalCone.completeBasis K) ↑i =
    ↑NumberField.mixedEmbedding.fundamentalCone.expMap.symm
      (NumberField.mixedEmbedding.normAtAllPlaces
        ((NumberField.mixedEmbedding K)
          ((algebraMap (NumberField.RingOfIntegers K) K)
            ↑(NumberField.Units.fundSystem K (NumberField.mixedEmbedding.fundamentalCone.equivFinRank.symm i)))))
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.H2π.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  groupHomology.H2π A = CategoryTheory.CategoryStruct.comp (groupHomology.isoCycles₂ A).inv (groupHomology.π A 2)
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
tprod_nat_mul_neg_add_one : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] [T2Space M] {f : ℤ → M},
  Multipliable f → ∏' (n : ℕ), f ↑n * f (-(↑n + 1)) = ∏' (n : ℤ), f n
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- If `p ≠ 0` and `p ≠ 1`, then `padicValRat p p` is `1`.  -/
padicValRat.self : ∀ {p : ℕ}, 1 < p → padicValRat p ↑p = 1
-- Lean.Meta.WHNF
/-- Forward declaration. It is defined in the module `src/Lean/Elab/PreDefinition/Structural/Eqns.lean`.
It is possible to avoid this hack if we move `Structural.EqnInfo` and `Structural.eqnInfoExt`
to this module.
 -/
Lean.Meta.getStructuralRecArgPos? : Lean.Name → Lean.CoreM (Option ℕ)
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.ringEquivOfRingEquiv_apply : ∀ {A : Type u_8} {K : Type u_9} {B : Type u_10} {L : Type u_11} [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : CommRing K] [inst_3 : CommRing L] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K]
  [inst_6 : Algebra B L] [inst_7 : IsFractionRing B L] (h : A ≃+* B) (a : K),
  (IsFractionRing.ringEquivOfRingEquiv h) a = (IsLocalization.map L ↑h ⋯) a
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.aefinStronglyMeasurable_zero : ∀ {α : Type u_5} {β : Type u_6} {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : Zero β]
  [inst_1 : TopologicalSpace β], MeasureTheory.AEFinStronglyMeasurable 0 μ
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
IsSMulRegular.skewMonoidAlgebra_iff : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] {S : Type u_3} [inst_1 : Monoid S] [inst_2 : DistribMulAction S k]
  {a : S} [Nonempty G], IsSMulRegular k a ↔ IsSMulRegular (SkewMonoidAlgebra k G) a
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.UnifyM.State.eAssignment : Lean.Meta.Sym.UnifyM.State✝ → Array (Option Lean.Expr)
-- Mathlib.CategoryTheory.Localization.StructuredArrow
CategoryTheory.Localization.induction_costructuredArrow : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : L.IsLocalization W] {Y : C}
  (P : CategoryTheory.CostructuredArrow L (L.obj Y) → Prop),
  P (CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.id (L.obj Y))) →
    (∀ ⦃X₁ X₂ : C⦄ (f : X₁ ⟶ X₂) (φ : L.obj X₂ ⟶ L.obj Y),
        P (CategoryTheory.CostructuredArrow.mk φ) →
          P (CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp (L.map f) φ))) →
      (∀ ⦃X₁ X₂ : C⦄ (w : X₁ ⟶ X₂) (hw : W w) (φ : L.obj X₁ ⟶ L.obj Y),
          P (CategoryTheory.CostructuredArrow.mk φ) →
            P
              (CategoryTheory.CostructuredArrow.mk
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.isoOfHom L W w hw).inv φ))) →
        ∀ (g : CategoryTheory.CostructuredArrow L (L.obj Y)), P g
-- Mathlib.Analysis.InnerProductSpace.Basic
RCLike.inner_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (x y : 𝕜), inner 𝕜 x y = y * (starRingEnd 𝕜) x
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.root_mul_right_of_isRoot : ∀ {R : Type u} {a : R} [inst : CommSemiring R] {p : Polynomial R} (q : Polynomial R), p.IsRoot a → (p * q).IsRoot a
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Rci.toList_iter : ∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.Rxi.IsAlwaysFinite α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Rci α}, r.iter.toList = r.toList
-- Lean.Util.Sorry
/-- Returns `true` if the expression is an application of `sorryAx`.  -/
Lean.Expr.isSorry : Lean.Expr → Bool
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
lTensor.inverse_comp_lTensor : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P]
  {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [inst_7 : AddCommGroup Q] [inst_8 : Module R Q]
  (hfg : Function.Exact ⇑f ⇑g) (hg : Function.Surjective ⇑g),
  lTensor.inverse Q hfg hg ∘ₗ LinearMap.lTensor Q g = (LinearMap.lTensor Q f).range.mkQ
-- Batteries.Data.List.Lemmas
List.idxOfNth_cons_succ_of_beq : ∀ {α : Type u_1} {x : α} {xs : List α} {n : ℕ} {a : α} [inst : BEq α],
  (a == x) = true → List.idxOfNth x (a :: xs) (n + 1) = List.idxOfNth x xs n + 1
-- Mathlib.CategoryTheory.Join.Opposites
CategoryTheory.Join.inclLeftCompOpEquivInverse_inv_app_op : ∀ (C : Type u₁) {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (d : D),
  (CategoryTheory.Join.inclLeftCompOpEquivInverse C D).inv.app (Opposite.op d) =
    CategoryTheory.CategoryStruct.id (Opposite.op (CategoryTheory.Join.right d))
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
PresheafOfModules.sheafifyMap_val : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj)
  [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α]
  {M₀ : PresheafOfModules R₀} {A : CategoryTheory.Sheaf J AddCommGrpCat} (φ : M₀.presheaf ⟶ A.obj)
  [inst_3 : CategoryTheory.Presheaf.IsLocallyInjective J φ] [inst_4 : CategoryTheory.Presheaf.IsLocallySurjective J φ]
  [inst_5 : J.WEqualsLocallyBijective AddCommGrpCat] {M₀' : PresheafOfModules R₀}
  {A' : CategoryTheory.Sheaf J AddCommGrpCat} (φ' : M₀'.presheaf ⟶ A'.obj)
  [inst_6 : CategoryTheory.Presheaf.IsLocallyInjective J φ'] [inst_7 : CategoryTheory.Presheaf.IsLocallySurjective J φ']
  (τ₀ : M₀ ⟶ M₀') (τ : A ⟶ A')
  (fac :
    CategoryTheory.CategoryStruct.comp ((PresheafOfModules.toPresheaf R₀).map τ₀) φ' =
      CategoryTheory.CategoryStruct.comp φ τ.hom),
  (PresheafOfModules.sheafifyMap α φ φ' τ₀ τ fac).val = PresheafOfModules.homMk τ.hom ⋯
-- Init.Data.Array.Find
_private.Init.Data.Array.Find.0.Option.pmap_or.match_1.eq_2 : ∀ {α : Type u_1} {p : α → Prop} {o' : Option α}
  (motive : (o : Option α) → {h : ∀ (a : α), o.or o' = some a → p a} → Sort u_2) (a : α)
  (h : ∀ (a_1 : α), (some a).or o' = some a_1 → p a_1) (h_1 : (h : ∀ (a : α), none.or o' = some a → p a) → motive none)
  (h_2 : (a : α) → (h : ∀ (a_1 : α), (some a).or o' = some a_1 → p a_1) → motive (some a)),
  (match some a, h with
    | none, h => h_1 h
    | some a, h => h_2 a h) =
    h_2 a h
-- Mathlib.Data.List.Lex
List.Lex.asymm : ∀ {α : Type u} (r : α → α → Prop) [Std.Asymm r], Std.Asymm (List.Lex r)
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
/-- Version of `LinearIndepOn.singleton` that works for the zero ring.  -/
LinearIndepOn.singleton' : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {v : ι → M} {i : ι}, (∀ (r : R), r • v i = 0 → r = 0) → LinearIndepOn R v {i}
-- Mathlib.Analysis.Normed.Group.Basic
DiscreteTopology.of_forall_le_norm' : ∀ {E : Type u_5} [inst : SeminormedGroup E] {r : ℝ}, 0 < r → (∀ (x : E), x ≠ 1 → r ≤ ‖x‖) → DiscreteTopology E
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionLiteralSupport : Type
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.smul_of : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] (f : Polynomial R) [inst_1 : DistribSMul S R]
  [inst_2 : IsScalarTower S R R] (a : S) (x : R), a • (AdjoinRoot.of f) x = (AdjoinRoot.of f) (a • x)
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.gc_map_comap : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : FunLike F A B]
  [inst_6 : NonUnitalAlgHomClass F R A B] (f : F),
  GaloisConnection (NonUnitalSubalgebra.map f) (NonUnitalSubalgebra.comap f)
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.Ordered.eq_2 : ∀ {α : Type u_1} (cmp : α → α → Ordering) (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α) (r : RBTree.RBNode α),
  RBTree.RBNode.Ordered cmp (RBTree.RBNode.node c l v r) =
    (RBTree.RBNode.All (fun x => RBTree.RBNode.cmpLT cmp x v) l ∧
      RBTree.RBNode.All (fun x => RBTree.RBNode.cmpLT cmp v x) r ∧
        RBTree.RBNode.Ordered cmp l ∧ RBTree.RBNode.Ordered cmp r)
-- Batteries.Data.Char.AsciiCasing
Char.beqCaseInsensitiveAsciiOnly.eqv : Equivalence fun x1 x2 => x1.beqCaseInsensitiveAsciiOnly x2 = true
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_extractLsb : ∀ {w hi lo : ℕ} {x : BitVec w} {i : ℕ},
  (BitVec.extractLsb hi lo x).getMsbD i =
    (decide (i < hi - lo + 1) && (decide (max hi lo - i < w) && x.getMsbD (w - 1 - (max hi lo - i))))
-- Mathlib.Data.Finset.NatDivisors
/-- `Nat.divisors` as a `MonoidHom`.  -/
Nat.divisorsHom : ℕ →* Finset ℕ
-- Mathlib.Algebra.Order.Monoid.Defs
/-- An ordered cancellative monoid is an ordered monoid in which
multiplication is cancellative and monotone.  -/
IsOrderedCancelMonoid : (α : Type u_2) → [CommMonoid α] → [Preorder α] → Prop
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.Const.insertListₘ : {α : Type u} →
  {β : Type v} →
    [BEq α] →
      [Hashable α] → (Std.DHashMap.Internal.Raw₀ α fun x => β) → List (α × β) → Std.DHashMap.Internal.Raw₀ α fun x => β
-- Init.Data.List.Lemmas
List.exists_mem_of_ne_nil : ∀ {α : Type u_1} (l : List α), l ≠ [] → ∃ x, x ∈ l
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.forIn_eq_forIn_toList : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {cmp : α → α → Ordering} {α_1 : Type u_1} {init : α_1}
  {f : α → α_1 → m (ForInStep α_1)} [inst : Monad m] [LawfulMonad m] {t : RBTree.RBSet α cmp},
  forIn t init f = forIn t.toList init f
-- Mathlib.Data.Rel
SetRel.image_eq_cod_of_dom_subset : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α β} {s : Set α}, R.dom ⊆ s → R.image s = R.cod
-- Mathlib.NumberTheory.LSeries.Deriv
LSeries_analyticOn : ∀ (f : ℕ → ℂ), AnalyticOn ℂ (LSeries f) {s | LSeries.abscissaOfAbsConv f < ↑s.re}
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.swap_comp_swap : ∀ (M : Type u_1) (N : Type u_2) [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  (AddMonoid.Coprod.swap M N).comp (AddMonoid.Coprod.swap N M) = AddMonoidHom.id (AddMonoid.Coprod N M)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.mem_integerSet : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {a : NumberField.mixedEmbedding.mixedSpace K},
  a ∈ NumberField.mixedEmbedding.fundamentalCone.integerSet K ↔
    a ∈ NumberField.mixedEmbedding.fundamentalCone K ∧ ∃ x, (NumberField.mixedEmbedding K) ↑x = a
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.symm_trans_apply : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [inst_3 : RingHomInvPair σ₁₂ σ₂₁] [inst_4 : RingHomInvPair σ₂₁ σ₁₂]
  {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} [inst_5 : RingHomInvPair σ₂₃ σ₃₂] [inst_6 : RingHomInvPair σ₃₂ σ₂₃]
  {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [inst_7 : RingHomInvPair σ₁₃ σ₃₁] [inst_8 : RingHomInvPair σ₃₁ σ₁₃]
  [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_10 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {M₁ : Type u_4}
  [inst_11 : TopologicalSpace M₁] [inst_12 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_13 : TopologicalSpace M₂]
  [inst_14 : AddCommMonoid M₂] {M₃ : Type u_6} [inst_15 : TopologicalSpace M₃] [inst_16 : AddCommMonoid M₃]
  [inst_17 : Module R₁ M₁] [inst_18 : Module R₂ M₂] [inst_19 : Module R₃ M₃] (e₁ : M₂ ≃SL[σ₂₁] M₁) (e₂ : M₃ ≃SL[σ₃₂] M₂)
  (c : M₁), (e₂.trans e₁).symm c = e₂.symm (e₁.symm c)
-- Mathlib.Algebra.GroupWithZero.Units.Basic
eq_inv_mul_iff_mul_eq₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b c : G₀}, b ≠ 0 → (a = b⁻¹ * c ↔ b * a = c)
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.instSmallMin_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : CategoryTheory.ObjectProperty C}
  [CategoryTheory.ObjectProperty.Small.{w, v, u} P], CategoryTheory.ObjectProperty.Small.{w, v, u} (P ⊓ Q)
-- Mathlib.Data.Multiset.AddSub
Multiset.erase_cons_tail_of_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} {a b : α}, a ∈ s → (b ::ₘ s).erase a = b ::ₘ s.erase a
-- Mathlib.Algebra.Group.Submonoid.DistribMulAction
Submonoid.instDistribMulActionSubtypeMem : {M : Type u_1} →
  {α : Type u_2} →
    [inst : Monoid M] →
      {S : Type u_3} →
        [inst_1 : SetLike S M] →
          (s : S) →
            [inst_2 : SubmonoidClass S M] → [inst_3 : AddMonoid α] → [DistribMulAction M α] → DistribMulAction (↥s) α
-- Mathlib.Logic.Equiv.Basic
Equiv.ulift_symm_down : ∀ {α : Type v} (x : α), (Equiv.ulift.symm x).down = x
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
ContinuousMap.Homotopy.hcast_def : ∀ {X : TopCat} {x₀ x₁ : ↑X} (hx₀ : x₀ = x₁), ContinuousMap.Homotopy.hcast hx₀ = CategoryTheory.eqToHom ⋯
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquivClass.mk : ∀ {F : Type u_1} {R : outParam (Type u_2)} {A : outParam (Type u_3)} {B : outParam (Type u_4)} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B]
  [inst_5 : Algebra R A] [inst_6 : Algebra R B] [inst_7 : EquivLike F A B] [toAlgEquivClass : AlgEquivClass F R A B]
  [toHomeomorphClass : HomeomorphClass F A B], ContinuousAlgEquivClass F R A B
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- The adjoint is involutive.  -/
LinearMap.adjoint_adjoint : ∀ {𝕜 : 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 : FiniteDimensional 𝕜 E] [inst_6 : FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F),
  LinearMap.adjoint (LinearMap.adjoint A) = A
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
/-- The forgetful functor from `CostructuredArrow K B` preserves any connected limit.  -/
CategoryTheory.CostructuredArrow.instPreservesLimitsOfShapeProjOfIsConnected : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {D : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} D] {K : CategoryTheory.Functor C D}
  [CategoryTheory.IsConnected J] {B : D},
  CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.CostructuredArrow.proj K B)
-- Mathlib.Topology.Sheaves.Sheaf
/-- The forgetful functor from sheaves to presheaves.
 -/
TopCat.Sheaf.forget : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : TopCat) → CategoryTheory.Functor (TopCat.Sheaf C X) (TopCat.Presheaf C X)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
ContinuousLinearEquiv.hasMFDerivWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  (f : E ≃L[𝕜] E') {s : Set E} {x : E}, HasMFDerivAt[s] (⇑f) x ↑f
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
MeasureTheory.MeasurePreserving.smul_measure : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μa : MeasureTheory.Measure α}
  {μb : MeasureTheory.Measure β} {R : Type u_5} [inst_2 : SMul R ENNReal] [inst_3 : IsScalarTower R ENNReal ENNReal]
  {f : α → β}, MeasureTheory.MeasurePreserving f μa μb → ∀ (c : R), MeasureTheory.MeasurePreserving f (c • μa) (c • μb)
-- Init.Grind.Norm
Lean.Grind.Int.lt_eq : ∀ (a b : ℤ), (a < b) = (a + 1 ≤ b)
-- Mathlib.Topology.EMetricSpace.Lipschitz
/-- Iterates of a Lipschitz function are Lipschitz.  -/
LipschitzWith.iterate : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {K : NNReal} {f : α → α},
  LipschitzWith K f → ∀ (n : ℕ), LipschitzWith (K ^ n) f^[n]
-- Lean.Meta.WHNF
Lean.Meta.reduceMatcher? : Lean.Expr → Lean.MetaM Lean.Meta.ReduceMatcherResult
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.copy.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G) (s : Set G) (hs : s = ↑K),
  K.copy s hs = { carrier := s, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
-- Init.Data.UInt.Lemmas
UInt64.toNat_sub_of_le : ∀ (a b : UInt64), b ≤ a → (a - b).toNat = a.toNat - b.toNat
-- Batteries.Data.BinomialHeap.Basic
_private.Batteries.Data.BinomialHeap.Basic.0.Batteries.BinomialHeap.Imp.HeapNode.realSize.match_1.eq_1 : ∀ {α : Type u_1} (motive : Batteries.BinomialHeap.Imp.HeapNode α → Sort u_2)
  (h_1 : Unit → motive Batteries.BinomialHeap.Imp.HeapNode.nil)
  (h_2 :
    (a : α) → (c s : Batteries.BinomialHeap.Imp.HeapNode α) → motive (Batteries.BinomialHeap.Imp.HeapNode.node a c s)),
  (match Batteries.BinomialHeap.Imp.HeapNode.nil with
    | Batteries.BinomialHeap.Imp.HeapNode.nil => h_1 ()
    | Batteries.BinomialHeap.Imp.HeapNode.node a c s => h_2 a c s) =
    h_1 ()
-- Lean.Meta.Tactic.FunIndInfo
Lean.Meta.FunIndInfo.mk : Lean.Name → Lean.Name → Array Bool → Array Lean.Meta.FunIndParamKind → Lean.Meta.FunIndInfo
-- Mathlib.LinearAlgebra.BilinearForm.Hom
/-- Apply a linear map to the right argument of a bilinear form.  -/
LinearMap.BilinForm.compRight : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → LinearMap.BilinForm R M → (M →ₗ[R] M) → LinearMap.BilinForm R M
-- Mathlib.Topology.MetricSpace.Lipschitz
/-- For functions to `ℝ`, it suffices to prove `f x ≤ f y + K * dist x y`; this version
doesn't assume `0≤K`.  -/
LipschitzWith.of_le_add_mul' : ∀ {α : Type u} [inst : PseudoMetricSpace α] {f : α → ℝ} (K : ℝ),
  (∀ (x y : α), f x ≤ f y + K * dist x y) → LipschitzWith K.toNNReal f
-- Std.Sat.CNF.RelabelFin
/-- Relabel `f` to a `CNF` formula with a known upper bound for its literals.

This operation might be useful when e.g. using the literals to index into an array of known size
without conducting bounds checks.
 -/
Std.Sat.CNF.relabelFin : (f : Std.Sat.CNF ℕ) → Std.Sat.CNF (Fin f.numLiterals)
-- Mathlib.Order.Minimal
/-- **Alias** of `OrderIso.mapSetOfPredMinimal`.

---

If two sets are order isomorphic, their minimals are also order isomorphic.  -/
OrderIso.mapSetOfMinimal : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        {s : Set α} → {t : Set β} → ↑s ≃o ↑t → ↑{x | Minimal (fun x => x ∈ s) x} ≃o ↑{x | Minimal (fun x => x ∈ t) x}
-- Mathlib.CategoryTheory.EqToHom
/-- If we (perhaps unintentionally) perform equational rewriting on
the source object of a morphism,
we can replace the resulting `_.mpr f` term by a composition with an `eqToHom`.

It may be advisable to introduce any necessary `eqToHom` morphisms manually,
rather than relying on this lemma firing.
 -/
CategoryTheory.congrArg_mpr_hom_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (p : X = Y) (q : Y ⟶ Z),
  ⋯.mpr q = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom p) q
-- Lean.Server.References
Lean.Server.References.DocumentRefInfo.mk : Lean.Lsp.Location → Lean.Name → Option Lean.Server.References.ParentDecl → Lean.Server.References.DocumentRefInfo
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile.0.Std.IterM.step_takeWhile.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (x = true → motive true) → (x = false → motive false) → motive x