mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- The canonical compatibility square between (the object components of)
`precompose` and `transform`.
This is a "naturality square" if we think as `transform _|>.obj _` as the
(app component of the) map component of a pseudofunctor from the bicategory of
categorical cospans with value in pseudofunctors
(its value on the categorical cospan `F, G` being the pseudofunctor
`precompose F G|>.obj _`).  -/
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor A B} →
              {G : CategoryTheory.Functor C B} →
                {A₁ : Type u₄} →
                  {B₁ : Type u₅} →
                    {C₁ : Type u₆} →
                      [inst_3 : CategoryTheory.Category.{v₄, u₄} A₁] →
                        [inst_4 : CategoryTheory.Category.{v₅, u₅} B₁] →
                          [inst_5 : CategoryTheory.Category.{v₆, u₆} C₁] →
                            {F₁ : CategoryTheory.Functor A₁ B₁} →
                              {G₁ : CategoryTheory.Functor C₁ B₁} →
                                {X : Type u₇} →
                                  {Y : Type u₈} →
                                    [inst_6 : CategoryTheory.Category.{v₇, u₇} X] →
                                      [inst_7 : CategoryTheory.Category.{v₈, u₈} Y] →
                                        (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) →
                                          (U : CategoryTheory.Functor X Y) →
                                            CategoryTheory.CatCommSq
                                              ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F
                                                    G).obj
                                                U)
                                              ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj
                                                ψ)
                                              ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj
                                                ψ)
                                              ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁
                                                    G₁).obj
                                                U)
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.measure_Iio_of_tendsto_atBot_atBot : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R)
  [inst_2 : OrderTopology R] [inst_3 : CompactIccSpace R] [inst_4 : MeasurableSpace R] [inst_5 : BorelSpace R]
  [inst_6 : SecondCountableTopology R] [inst_7 : DenselyOrdered R],
  Filter.Tendsto (↑f) Filter.atBot Filter.atBot → ∀ (x : R), f.measure (Set.Iio x) = ⊤
-- Mathlib.Data.WSeq.Productive
/-- Given a productive weak sequence, we can collapse all the `think`s to
produce a sequence.  -/
Stream'.WSeq.toSeq : {α : Type u} → (s : Stream'.WSeq α) → [s.Productive] → Stream'.Seq α
-- Mathlib.Data.EReal.Operations
EReal.mul_top_of_neg : ∀ {x : EReal}, x < 0 → x * ⊤ = ⊥
-- Std.Data.DTreeMap.Raw.Lemmas
/-- Variant of `get?_map` that holds without `LawfulEqCmp`.  -/
Std.DTreeMap.Raw.Const.get?_map' : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → γ} {k : α} (h : t.WF),
  Std.DTreeMap.Raw.Const.get? (Std.DTreeMap.Raw.map f t) k =
    Option.pmap (fun v h' => f (t.getKey k h') v) (Std.DTreeMap.Raw.Const.get? t k) ⋯
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Closure
/-- A `SubAddAction` is finitely generated if it is the closure of a finite set.  -/
SubAddAction.FG : {R : Type u_1} → {M : Type u_2} → [inst : VAdd R M] → SubAddAction R M → Prop
-- Init.Data.Int.DivMod.Lemmas
Int.mul_fmod : ∀ (a b n : ℤ), (a * b).fmod n = (a.fmod n * b.fmod n).fmod n
-- Mathlib.Data.Fintype.EquivFin
Finset.univ_map_embedding : ∀ {α : Type u_4} [inst : Fintype α] (e : α ↪ α), Finset.map e Finset.univ = Finset.univ
-- Mathlib.Algebra.Polynomial.Div
Polynomial.IsRoot.dvd_coeff_zero : ∀ {R : Type u} [inst : CommRing R] {p : Polynomial R} {x : R}, p.IsRoot x → x ∣ p.coeff 0
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.Hom.w₁₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} (self : E.Hom F) {i j : E.I₀} (k : E.I₁ i j),
  CategoryTheory.CategoryStruct.comp (self.h₁ k) (F.p₂ (self.s₁ k)) =
    CategoryTheory.CategoryStruct.comp (E.p₂ k) (self.h₀ j)
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff
ContDiffAt.toOpenPartialHomeomorph_coe : ∀ {𝕂 : Type u_1} [inst : RCLike 𝕂] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕂 E]
  {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕂 F] [inst_5 : CompleteSpace E] {f : E → F}
  {f' : E ≃L[𝕂] F} {a : E} {n : WithTop ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (↑f') a) (hn : n ≠ 0),
  ↑(ContDiffAt.toOpenPartialHomeomorph f hf hf' hn) = f
-- Mathlib.RingTheory.AlgebraTower
Module.Basis.smulTower_repr_mk : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid A]
  [inst_3 : Module R S] [inst_4 : Module S A] [inst_5 : Module R A] [inst_6 : IsScalarTower R S A] {ι : Type u_5}
  {ι' : Type u_6} (b : Module.Basis ι R S) (c : Module.Basis ι' S A) (x : A) (i : ι) (j : ι'),
  ((b.smulTower c).repr x) (i, j) = (b.repr ((c.repr x) j)) i
-- Mathlib.Data.ZMod.Basic
AddSubgroupClass.instZModModule : {n : ℕ} →
  {S : Type u_1} →
    {G : Type u_2} →
      [inst : AddCommGroup G] →
        [inst_1 : SetLike S G] → [inst_2 : AddSubgroupClass S G] → {K : S} → [Module (ZMod n) G] → Module (ZMod n) ↥K
-- Mathlib.Order.TypeTags
WithTop.recTopCoe_coe : ∀ {α : Type u_1} {C : WithTop α → Sort u_2} (d : C ⊤) (f : (a : α) → C ↑a) (x : α), WithTop.recTopCoe d f ↑x = f x
-- Mathlib.Topology.Separation.Basic
TopologicalSpace.IsTopologicalBasis.eq_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X] {b : Set (Set X)},
  TopologicalSpace.IsTopologicalBasis b → ∀ {x y : X}, x = y ↔ ∀ s ∈ b, x ∈ s ↔ y ∈ s
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.inner_comp_rightAngleRotation : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (x y : E), inner ℝ (o.rightAngleRotation x) (o.rightAngleRotation y) = inner ℝ x y
-- Init.Data.Array.Find
Array.isNone_finIdxOf? : ∀ {α : Type u_1} [inst : BEq α] [PartialEquivBEq α] {xs : Array α} {a : α}, (xs.finIdxOf? a).isNone = !xs.contains a
-- Mathlib.Order.InitialSeg
PrincipalSeg.relIsoTrans_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : r ≃r s)
  (g : PrincipalSeg s t) (a : α), (PrincipalSeg.relIsoTrans f g).toRelEmbedding a = g.toRelEmbedding (f a)
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
/-- Every morphism in the homotopy category `HomotopyCategory₂ A` is the equivalence class of
an edge of `A`.
 -/
SSet.Truncated.HomotopyCategory₂.homMk_surjective : ∀ {A : SSet.Truncated 2} [inst : A.Quasicategory₂]
  {x y : A.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 })},
  Function.Surjective SSet.Truncated.HomotopyCategory₂.homMk
-- Init.Prelude
LT.mk : {α : Type u} → (α → α → Prop) → LT α
-- Mathlib.Topology.Algebra.OpenSubgroup
Subgroup.quotient_finite_of_isOpen' : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (U : Subgroup G)
  (K : Subgroup ↥U), IsOpen ↑U → IsOpen ↑K → Finite (↥U ⧸ K)
-- Mathlib.GroupTheory.Divisible
QuotientGroup.rootableBy.eq_1 : ∀ {A : Type u_2} [inst : CommGroup A] (B : Subgroup A) [inst_1 : RootableBy A ℕ],
  QuotientGroup.rootableBy B = Function.Surjective.rootableBy QuotientGroup.mk ⋯ ⋯
-- Init.NotationExtra
unexpandGetElem : Lean.PrettyPrinter.Unexpander
-- Mathlib.Data.Num.Bitwise
/-- Right-shift the binary representation of a `PosNum`.  -/
PosNum.shiftr : PosNum → ℕ → Num
-- Mathlib.Analysis.Normed.Group.Defs
SeminormedGroup.toNorm : {E : Type u_8} → [self : SeminormedGroup E] → Norm E
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLT_obj_map_eTruncLTι_app : ∀ {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]
  (t : CategoryTheory.Triangulated.TStructure C) (i : EInt) (X : C),
  (t.eTruncLT.obj i).map ((t.eTruncLTι i).app X) = (t.eTruncLTι i).app ((t.eTruncLT.obj i).obj X)
-- Init.Data.Array.Lemmas
/-- Variant of `foldrM_append` with a side condition for the `start` argument.  -/
Array.foldrM_append' : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {f : α → β → m β} {b : β}
  {xs ys : Array α} {start : ℕ},
  start = xs.size + ys.size →
    Array.foldrM f b (xs ++ ys) start = do
      let init ← Array.foldrM f b ys
      Array.foldrM f init xs
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.exp_one_mul_le_exp : ∀ {x : ℝ}, Real.exp 1 * x ≤ Real.exp x
-- Mathlib.CategoryTheory.Action.Basic
Action.resId_inv_app_hom : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} [inst_1 : Monoid G] (X : Action V G),
  ((Action.resId V).inv.app X).hom = CategoryTheory.CategoryStruct.id X.V
-- Mathlib.Order.SupClosed
sup_mem_supClosure : ∀ {α : Type u_3} [inst : SemilatticeSup α] {s : Set α} {a b : α}, a ∈ s → b ∈ s → a ⊔ b ∈ supClosure s
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.smul_set_pi_of_isUnit : ∀ {M : Type u_5} {ι : Type u_6} {α : ι → Type u_7} [inst : Monoid M] [inst_1 : (i : ι) → MulAction M (α i)] {c : M},
  IsUnit c → ∀ (I : Set ι) (s : (i : ι) → Set (α i)), c • I.pi s = I.pi (c • s)
-- Mathlib.RingTheory.Ideal.Operations
Submodule.map_pointwise_smul : ∀ {R : Type u} {M : Type v} {M' : Type u_1} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (r : R) (N : Submodule R M) (f : M →ₗ[R] M'),
  Submodule.map f (r • N) = r • Submodule.map f N
-- Mathlib.Topology.Maps.Basic
IsClosedMap.id : ∀ {X : Type u_1} [inst : TopologicalSpace X], IsClosedMap id
-- Mathlib.Algebra.Homology.DerivedCategory.Plus
DerivedCategory.Plus.instCommShiftPlusQhInt : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → [inst_2 : HasDerivedCategory C] → DerivedCategory.Plus.Qh.CommShift ℤ
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.encodeCode_eq : Encodable.encode = Nat.Partrec.Code.encodeCode
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.minEntry!.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Inhabited (α × β)],
  Std.DTreeMap.Internal.Impl.Const.minEntry! Std.DTreeMap.Internal.Impl.leaf =
    panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.Const.minEntry!" 816 13
      "Map is empty"
-- Lean.CoreM
/-- Trace messages  -/
Lean.Core.State.traceState : Lean.Core.State → Lean.TraceState
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
SemimoduleCat.MonoidalCategory.braiding_naturality_right : ∀ {R : Type u} [inst : CommSemiring R] (X : SemimoduleCat R) {Y Z : SemimoduleCat R} (f : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) (X.braiding Z).hom =
    CategoryTheory.CategoryStruct.comp (X.braiding Y).hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.subst1.injEq : ∀ (k : ℤ) (c₁ : Lean.Meta.Grind.Arith.Linear.EqCnstr) (c₂ : Lean.Meta.Grind.Arith.Linear.DiseqCnstr) (k_1 : ℤ)
  (c₁_1 : Lean.Meta.Grind.Arith.Linear.EqCnstr) (c₂_1 : Lean.Meta.Grind.Arith.Linear.DiseqCnstr),
  (Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.subst1 k c₁ c₂ =
      Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.subst1 k_1 c₁_1 c₂_1) =
    (k = k_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1)
-- Mathlib.RingTheory.Artinian.Module
isArtinian_iff_submodule_quotient : ∀ {R : Type u_1} {P : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup P] [inst_2 : Module R P] (S : Submodule R P),
  IsArtinian R P ↔ IsArtinian R ↥S ∧ IsArtinian R (P ⧸ S)
-- Mathlib.Data.Tree.Basic
BinaryTree.node.injEq : ∀ {α : Type u} (value : α) (left right : BinaryTree α) (value_1 : α) (left_1 right_1 : BinaryTree α),
  (BinaryTree.node value left right = BinaryTree.node value_1 left_1 right_1) =
    (value = value_1 ∧ left = left_1 ∧ right = right_1)
-- Mathlib.Combinatorics.Quiver.Cast
Quiver.Hom.cast_eq_iff_heq : ∀ {U : Type u_1} [inst : Quiver U] {u v u' v' : U} (hu : u = u') (hv : v = v') (e : u ⟶ v) (e' : u' ⟶ v'),
  Quiver.Hom.cast hu hv e = e' ↔ e ≍ e'
-- Init.Data.Vector.Lemmas
Vector.toArray_eraseIdx! : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ}, i < n → (xs.eraseIdx! i).toArray = xs.toArray.eraseIdx! i
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.Equiv.beq_congr : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [EquivBEq α] [LawfulHashable α] {m₃ m₄ : Std.DHashMap.Internal.Raw₀ α fun x => β} [inst_4 : BEq β],
  (↑m₁).WF →
    (↑m₂).WF →
      (↑m₃).WF →
        (↑m₄).WF →
          (↑m₁).Equiv ↑m₃ →
            (↑m₂).Equiv ↑m₄ → Std.DHashMap.Internal.Raw₀.Const.beq m₁ m₂ = Std.DHashMap.Internal.Raw₀.Const.beq m₃ m₄
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent
/-- **Alias** of the reverse direction of `ContinuousLinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff`.

---

`ker f` is invariant under `T` if and only if `f ∘L T ∘L f = f ∘L T`,
for idempotent `f`.  -/
ContinuousLinearMap.IsIdempotentElem.ker_mem_invtSubmodule : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {f T : M →L[R] M},
  IsIdempotentElem f → f ∘SL T ∘SL f = f ∘SL T → (↑f).ker ∈ Module.End.invtSubmodule ↑T
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
/-- The underlying `NormedAddGroupHom`.  -/
SemiNormedGrp.Hom.hom' : {M N : SemiNormedGrp} → M.Hom N → NormedAddGroupHom M.carrier N.carrier
-- Mathlib.Analysis.Normed.Module.Convex
convex_eball : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (a : E) (r : ENNReal),
  Convex ℝ (Metric.eball a r)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.maxKeyD_alter_eq_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β},
  (Std.DTreeMap.Const.alter t k f).isEmpty = false →
    ∀ {fallback : α},
      (Std.DTreeMap.Const.alter t k f).maxKeyD fallback = k ↔
        (f (Std.DTreeMap.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.Topology.Bornology.Constructions
Bornology.isBounded_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Bornology α] [inst_1 : Bornology β] {s : Set α} {t : Set β},
  Bornology.IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ Bornology.IsBounded s ∧ Bornology.IsBounded t
-- Std.Time.Format.Modifier
Std.Time.Modifier.X.inj : ∀ {presentation presentation_1 : Std.Time.OffsetX},
  Std.Time.Modifier.X presentation = Std.Time.Modifier.X presentation_1 → presentation = presentation_1
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
Differentiable.continuousAlternatingMap_apply : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [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] {f : E → F [⋀^ι]→L[𝕜] G} {g : ι → E → F} [Finite ι],
  Differentiable 𝕜 f → (∀ (i : ι), Differentiable 𝕜 (g i)) → Differentiable 𝕜 fun x => (f x) fun x_1 => g x_1 x
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.indepSets_of_indepSets_of_le_left : ∀ {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s₁ s₂ s₃ : Set (Set Ω)},
  ProbabilityTheory.IndepSets s₁ s₂ μ → s₃ ⊆ s₁ → ProbabilityTheory.IndepSets s₃ s₂ μ
-- Mathlib.Data.ENNReal.Inv
ENNReal.div_le_div_right : ∀ {a b : ENNReal}, a ≤ b → ∀ (c : ENNReal), a / c ≤ b / c
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- The pointwise multiplication of finsets `s * t` and `t` is defined as `{x * y | x ∈ s, y ∈ t}`
in scope `Pointwise`.  -/
Finset.mul : {α : Type u_2} → [DecidableEq α] → [Mul α] → Mul (Finset α)
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instGroupCoeOfSubgroupClass.eq_1 : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → Group (R i)] [inst_2 : ∀ (i : ι), SubgroupClass (S i) (R i)],
  RestrictedProduct.instGroupCoeOfSubgroupClass R = Function.Injective.group DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Init.Data.String.Lemmas.IsEmpty
String.Slice.isEmpty_iff : ∀ {s : String.Slice}, s.isEmpty = true ↔ s.utf8ByteSize = 0
-- Mathlib.Analysis.Distribution.DerivNotation
/-- The notation typeclass for the Laplace operator.
 -/
Laplacian : Type v → outParam (Type w) → Type (max v w)
-- Lean.Syntax
Lean.Syntax.instReprRange : Repr Lean.Syntax.Range
-- Mathlib.Data.Rat.Lemmas
Rat.add_num_den : ∀ (q r : ℚ), q + r = Rat.divInt (q.num * ↑r.den + ↑q.den * r.num) (↑q.den * ↑r.den)
-- Init.Data.Order.Classes
Std.LawfulOrderMax.mk : ∀ {α : Type u} [inst : Max α] [inst_1 : LE α] [toMaxEqOr : Std.MaxEqOr α] [toLawfulOrderSup : Std.LawfulOrderSup α],
  Std.LawfulOrderMax α
-- Mathlib.Computability.RE
Partrec.merge : ∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] {f g : α →. σ},
  Partrec f →
    Partrec g →
      (∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y) → ∃ k, Partrec k ∧ ∀ (a : α) (x : σ), x ∈ k a ↔ x ∈ f a ∨ x ∈ g a
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Equiv.Perm.IsCycle.existsUnique_cycle_subtype : ∀ {α : Type u_1} [Finite α] [inst : DecidableEq α] {f : Equiv.Perm α}, f.IsCycle → ∃! s, (↑s).formPerm ⋯ = f
-- Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
CategoryTheory.ObjectProperty.preservesColimitsOfShape_iff : ∀ {J : Type u_1} {C : Type u_3} (K : Type u_5) [inst : CategoryTheory.Category.{v_1, u_5} K]
  [inst_1 : CategoryTheory.Category.{v_3, u_1} J] [inst_2 : CategoryTheory.Category.{v_5, u_3} C]
  (F : CategoryTheory.Functor J C),
  CategoryTheory.ObjectProperty.preservesColimitsOfShape K F ↔ CategoryTheory.Limits.PreservesColimitsOfShape K F
-- Mathlib.Algebra.Module.Basic
Function.support_const_smul_of_ne_zero : ∀ {α : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Semiring R] [IsDomain R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [Module.IsTorsionFree R M] (c : R) (g : α → M),
  c ≠ 0 → Function.support (c • g) = Function.support g
-- Mathlib.Data.Multiset.Dedup
Multiset.Disjoint.dedup_add : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, Disjoint s t → (s + t).dedup = s.dedup + t.dedup
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.TextDocumentClientCapabilities.mk : Option Lean.Lsp.CompletionClientCapabilities →
  Option Lean.Lsp.CodeActionClientCapabilities →
    Option Lean.Lsp.InlayHintClientCapabilities → Lean.Lsp.TextDocumentClientCapabilities
-- Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Real.Gamma_three_div_two_lt_one : Real.Gamma (3 / 2) < 1
-- Lean.Syntax
Lean.Syntax.Traverser.mk.sizeOf_spec : ∀ (cur : Lean.Syntax) (parents : Array Lean.Syntax) (idxs : Array ℕ),
  sizeOf { cur := cur, parents := parents, idxs := idxs } = 1 + sizeOf cur + sizeOf parents + sizeOf idxs
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsCircuit.disjoint_coloops : ∀ {α : Type u_1} {M : Matroid α} {C : Set α}, M.IsCircuit C → Disjoint C M.coloops
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.Nonempty.inv : ∀ {α : Type u_2} [inst : InvolutiveInv α] {s : Set α}, s.Nonempty → s⁻¹.Nonempty
-- Lean.Elab.Do.Basic
Lean.Elab.Do.doElabToSyntaxWithExpectedType : {α : Type} →
  Lean.MessageData →
    (Option Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr) →
      (Lean.Term → Lean.Elab.Do.DoElabM α) → optParam Lean.Syntax Lean.Syntax.missing → Lean.Elab.Do.DoElabM α
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The minimal distances to a set and its closure coincide.  -/
Metric.infDist_closure : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x : α}, Metric.infDist x (closure s) = Metric.infDist x s
-- Mathlib.Order.BoundedOrder.Basic
not_lt_top_iff : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, ¬a < ⊤ ↔ a = ⊤
-- Mathlib.Data.PNat.Xgcd
PNat.gcdB'_coe : ∀ (a b : ℕ+), ↑(a.gcdB' b) = a.gcdY b + ↑(a.gcdZ b)
-- Init.MetaTypes
Lean.Meta.Occurrences.all.sizeOf_spec : sizeOf Lean.Meta.Occurrences.all = 1
-- Init.Data.BitVec.Lemmas
BitVec.clzAuxRec_succ : ∀ {w n : ℕ} (x : BitVec w),
  x.clzAuxRec (n + 1) = if x.getLsbD (n + 1) = true then BitVec.ofNat w (w - 1 - (n + 1)) else x.clzAuxRec n
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.exists_revMatchesAt_iff_eq_append : ∀ {pat : String} {s : String.Slice},
  (∃ pos, String.Slice.Pattern.Model.RevMatchesAt pat pos) ↔ ∃ t₁ t₂, s.copy = t₁ ++ pat ++ t₂
-- Mathlib.Dynamics.TopologicalEntropy.Subset
Dynamics.coverEntropy_monotone : ∀ {X : Type u_1} [inst : UniformSpace X] (T : X → X), Monotone fun F => Dynamics.coverEntropy T F
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.shift_v : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a p q : ℤ) (hpq : p + n = q)
  (p' q' : ℤ) (hp' : p' = p + a) (hq' : q' = q + a),
  (γ.shift a).v p q hpq =
    CategoryTheory.CategoryStruct.comp (K.shiftFunctorObjXIso a p p' hp').hom
      (CategoryTheory.CategoryStruct.comp (γ.v p' q' ⋯) (L.shiftFunctorObjXIso a q q' hq').inv)
-- Mathlib.NumberTheory.ArithmeticFunction.Liouville
ArithmeticFunction.isMultiplicative_liouville : ArithmeticFunction.liouville.IsMultiplicative
-- Std.Time.Date.Unit.Month
Std.Time.Month.instReprQuarter : Repr Std.Time.Month.Quarter
-- Mathlib.Algebra.Lie.Subalgebra
/-- Given a Lie algebra `L` containing a Lie subalgebra `L' ⊆ L`, together with a Lie module `M` of
`L`, we may regard `M` as a Lie module of `L'` by restriction.  -/
LieSubalgebra.lieModule : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (L' : LieSubalgebra R L)
  {M : Type w} [inst_3 : AddCommGroup M] [inst_4 : LieRingModule L M] [inst_5 : Module R M] [LieModule R L M],
  LieModule R (↥L') M