mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Kaehler.JacobiZariski
SnakeLemma.δ'.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6}
  {N₃ : Type u_7} [inst_1 : AddCommGroup M₁] [inst_2 : Module R M₁] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M₂]
  [inst_5 : AddCommGroup M₃] [inst_6 : Module R M₃] [inst_7 : AddCommGroup N₁] [inst_8 : Module R N₁]
  [inst_9 : AddCommGroup N₂] [inst_10 : Module R N₂] [inst_11 : AddCommGroup N₃] [inst_12 : Module R N₃]
  (i₁ i₁_1 : M₁ →ₗ[R] N₁) (e_i₁ : i₁ = i₁_1) (i₂ i₂_1 : M₂ →ₗ[R] N₂) (e_i₂ : i₂ = i₂_1) (i₃ i₃_1 : M₃ →ₗ[R] N₃)
  (e_i₃ : i₃ = i₃_1) (f₁ f₁_1 : M₁ →ₗ[R] M₂) (e_f₁ : f₁ = f₁_1) (f₂ f₂_1 : M₂ →ₗ[R] M₃) (e_f₂ : f₂ = f₂_1)
  (hf : Function.Exact ⇑f₁ ⇑f₂) (g₁ g₁_1 : N₁ →ₗ[R] N₂) (e_g₁ : g₁ = g₁_1) (g₂ g₂_1 : N₂ →ₗ[R] N₃) (e_g₂ : g₂ = g₂_1)
  (hg : Function.Exact ⇑g₁ ⇑g₂) (h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁) (h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂) {K₃ : Type u_9} {C₁ : Type u_10}
  [inst_13 : AddCommGroup K₃] [inst_14 : Module R K₃] [inst_15 : AddCommGroup C₁] [inst_16 : Module R C₁]
  (ι₃ ι₃_1 : K₃ →ₗ[R] M₃) (e_ι₃ : ι₃ = ι₃_1) (hι₃ : Function.Exact ⇑ι₃ ⇑i₃) (π₁ π₁_1 : N₁ →ₗ[R] C₁) (e_π₁ : π₁ = π₁_1)
  (hπ₁ : Function.Exact ⋯ ⋯) (hf₂ : ⋯), ⋯
-- Mathlib.Data.Set.Insert
Set.union_insert : ∀ {α : Type u_1} {s t : Set α} {a : α}, s ∪ insert a t = insert a (s ∪ t)
-- Batteries.Recycling.RBTree.Basic
/-- `O(n)`. Fold a monadic function on the values from left to right (in increasing order).  -/
RBTree.RBMap.foldlM : {α : Type u} →
  {β : Type v} →
    {σ : Type w} →
      {cmp : α → α → Ordering} →
        {m : Type w → Type u_1} → [Monad m] → (σ → α → β → m σ) → σ → RBTree.RBMap α β cmp → m σ
-- Lean.Meta.Sym.Simp.SimpM
/-- Monad for the structural simplifier, layered on top of `SymM`.  -/
Lean.Meta.Sym.Simp.SimpM : Type → Type
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersion.of_opens : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_7} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_11}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞} [IsManifold I n M]
  (s : TopologicalSpace.Opens M), Manifold.IsImmersion I I n Subtype.val
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.subsingleton_iff : ∀ {M : Type u_1} [inst : MulOneClass M], Subsingleton (Submonoid M) ↔ Subsingleton M
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- **Alias** of the forward direction of `hasStrictDerivAt_iff_hasStrictFDerivAt`. -/
HasStrictDerivAt.hasStrictFDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] {f : 𝕜 → F} {f' : F} {x : 𝕜} [inst_4 : ContinuousSMul 𝕜 F],
  HasStrictDerivAt f f' x → HasStrictFDerivAt f (ContinuousLinearMap.toSpanSingleton 𝕜 f') x
-- Mathlib.Order.Filter.Basic
Filter.eventually_iff : ∀ {α : Type u} {f : Filter α} {P : α → Prop}, (∀ᶠ (x : α) in f, P x) ↔ {x | P x} ∈ f
-- Mathlib.CategoryTheory.Monoidal.Opposite
/-- The identification `- ⊗ X = mop (unmop X ⊗ -)` as a natural isomorphism.  -/
CategoryTheory.MonoidalOpposite.tensorRightIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X : Cᴹᵒᵖ) →
        CategoryTheory.MonoidalCategory.tensorRight X ≅
          (CategoryTheory.unmopFunctor C).comp
            ((CategoryTheory.MonoidalCategory.tensorLeft X.unmop).comp (CategoryTheory.mopFunctor C))
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
/-- Given `L i : (E i)' × (E i)' → ℝ` a family of continuous bilinear forms,
`diagonalStrongDualPi L` is the continuous bilinear form over `(Π i, E i)'`
which maps `(x, y) : (Π i, E i)' × (Π i, E i)'` to
`∑ i, L i (fun a ↦ x aᵢ) (fun a ↦ y aᵢ)`.

This is an implementation detail used in `iIndepFun.hasGaussianLaw`.  -/
_private.Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence.0.ContinuousLinearMap.diagonalStrongDualPi : {ι : Type u_2} →
  [Fintype ι] →
    [DecidableEq ι] →
      {E : ι → Type u_3} →
        [inst : (i : ι) → NormedAddCommGroup (E i)] →
          [inst_1 : (i : ι) → NormedSpace ℝ (E i)] →
            ((i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ) →
              StrongDual ℝ ((i : ι) → E i) →L[ℝ] StrongDual ℝ ((i : ι) → E i) →L[ℝ] ℝ
-- Mathlib.AlgebraicGeometry.Sites.Proetale
/-- Construct an object of the pro-étale site of `S` by giving a weakly étale morphism
`f : X ⟶ S`.  -/
AlgebraicGeometry.Scheme.ProEt.mk : {S X : AlgebraicGeometry.Scheme} → (f : X ⟶ S) → [AlgebraicGeometry.WeaklyEtale f] → S.ProEt
-- Init.System.IO
/-- Creates a new task that waits for `t` to complete and then runs the `IO` action `f` on its result.
This new task has priority `prio`.

Running the resulting `BaseIO` action causes the task to be started eagerly. Unlike pure tasks
created by `Task.spawn`, tasks created by this function will run even if the last reference to the
task is dropped. The `act` should explicitly check for cancellation via `IO.checkCanceled` if it
should be terminated or otherwise react to the last reference being dropped. Because `EIO ε` actions
may throw an exception of type `ε`, the result of the task is an `Except ε α`.
 -/
EIO.mapTask : {α : Type u_1} →
  {ε β : Type} →
    (α → EIO ε β) →
      Task α → optParam Task.Priority Task.Priority.default → optParam Bool false → BaseIO (Task (Except ε β))
-- Mathlib.Algebra.FreeMonoid.Basic
/-- The identity equivalence between `FreeMonoid α` and `List α`.  -/
FreeMonoid.toList : {α : Type u_1} → FreeMonoid α ≃ List α
-- Mathlib.Order.Filter.Pointwise
Filter.vadd_tendsto_vadd_iff : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : AddGroup γ] [inst_1 : AddAction γ β] {m : α → β} {c : γ}
  {f : Filter α} {g : Filter β}, Filter.Tendsto (c +ᵥ m) f (c +ᵥ g) ↔ Filter.Tendsto m f g
-- Mathlib.LinearAlgebra.Dimension.Constructions
Module.Basis.sumQuot_inr : ∀ {R : Type u_2} {V : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {W : Submodule R V}
  {m : Type u_4} {n : Type u_5} (bW : Module.Basis m R ↥W) (bQ : Module.Basis n R (V ⧸ W)) (j : n),
  Submodule.Quotient.mk ((bW.sumQuot bQ) (Sum.inr j)) = bQ j
-- Mathlib.GroupTheory.CoprodI
/-- The free product (categorical coproduct) of an indexed family of monoids.  -/
Monoid.CoprodI : {ι : Type u_1} → (M : ι → Type u_2) → [(i : ι) → Monoid (M i)] → Type (max u_1 u_2)
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.coe_inv : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] (e : X ≃ᵈ X), ⇑e⁻¹ = ⇑e.symm
-- Mathlib.Analysis.Convex.Jensen
/-- If a function `f` is convex on `s`, then the value it takes at some center of mass of points of
`s` is less than the value it takes on one of those points.  -/
ConvexOn.exists_ge_of_centerMass : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : LinearOrder β]
  [IsOrderedAddMonoid β] [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β}
  {w : ι → 𝕜} {p : ι → E} {t : Finset ι},
  ConvexOn 𝕜 s f → (∀ i ∈ t, 0 ≤ w i) → 0 < ∑ i ∈ t, w i → (∀ i ∈ t, p i ∈ s) → ∃ i ∈ t, f (t.centerMass w p) ≤ f (p i)
-- Lean.ToExpr
Lean.instToExprFin : {n : ℕ} → Lean.ToExpr (Fin n)
-- Mathlib.Algebra.Algebra.Defs
/-- Coercion from a commutative semiring to an algebra over this semiring.  -/
Algebra.cast : {R : Type u_1} → {A : Type u_2} → [inst : CommSemiring R] → [inst_1 : Semiring A] → [Algebra R A] → R → A
-- Mathlib.Algebra.Lie.InvariantForm
/-- A finite-dimensional Lie algebra over a field is semisimple
if it does not have non-trivial abelian ideals and it admits a
non-degenerate reflexive invariant bilinear form.
Here a form is *invariant* if it is compatible with the Lie bracket: `Φ ⁅x, y⁆ z = Φ x ⁅y, z⁆`.
 -/
LieAlgebra.InvariantForm.isSemisimple_of_nondegenerate : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : LieRing L] [inst_2 : LieAlgebra K L] [Module.Finite K L]
  (Φ : LinearMap.BilinForm K L),
  Φ.Nondegenerate →
    LinearMap.BilinForm.lieInvariant L Φ →
      Φ.IsRefl → (∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I) → LieAlgebra.IsSemisimple K L
-- Mathlib.Order.Fin.Basic
Fin.castOrderIso_refl : ∀ {n : ℕ} (h : optParam (n = n) ⋯), Fin.castOrderIso h = OrderIso.refl (Fin n)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.instInfSet : {R : Type u} → {M : Type v} → [inst : SMul R M] → InfSet (SubMulAction R M)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.functorEquiv.eq_1 : ∀ {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) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X],
  CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X =
    { functor := CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver F G X,
      inverse := CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback F G X,
      unitIso :=
        CategoryTheory.NatIso.ofComponents
          (fun x =>
            CategoryTheory.NatIso.ofComponents
              (fun x_1 =>
                CategoryTheory.Limits.CategoricalPullback.mkIso
                  (CategoryTheory.Iso.refl
                    (((CategoryTheory.Functor.id
                                (CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G))).obj
                            x).obj
                        x_1).fst)
                  (CategoryTheory.Iso.refl
                    (((CategoryTheory.Functor.id
                                (CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G))).obj
                            x).obj
                        x_1).snd)
                  ⋯)
              ⋯)
          ⋯,
      counitIso :=
        CategoryTheory.NatIso.ofComponents
          (fun x =>
            CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mkIso
              (CategoryTheory.NatIso.ofComponents
                (fun x_1 =>
                  CategoryTheory.Iso.refl
                    ((((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback F G
                                    X).comp
                                (CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver F G X)).obj
                            x).fst.obj
                      x_1))
                ⋯)
              (CategoryTheory.NatIso.ofComponents
                (fun x_1 =>
                  CategoryTheory.Iso.refl
                    ((((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback F G
                                    X).comp
                                (CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver F G X)).obj
                            x).snd.obj
                      x_1))
                ⋯)
              ⋯)
          ⋯,
      functor_unitIso_comp := ⋯ }
-- Init.Data.List.Lemmas
List.getLast!.eq_1 : ∀ {α : Type u_1} [inst : Inhabited α],
  [].getLast! = panicWithPosWithDecl "Init.Data.List.BasicAux" "List.getLast!" 64 13 "empty list"
-- Mathlib.Tactic.CongrExclamation
_private.Mathlib.Tactic.CongrExclamation.0.Congr!.elabConfig.evalConfigItem : Lean.Elab.ConfigEval.EvalConfigItem Congr!.Config
-- Init.Data.Iterators.Consumers.Monadic.Partial
Std.IterM.Partial.mk.injEq : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} (it it_1 : Std.IterM m β),
  ({ it := it } = { it := it_1 }) = (it = it_1)
-- Init.Data.Option.Instances
/-- Partial filter. If `o : Option α`, `p : (a : α) → o = some a → Bool`, then `o.pfilter p` is
the same as `o.filter p` but `p` is passed the proof that `o = some a`.  -/
Option.pfilter : {α : Type u_1} → (o : Option α) → ((a : α) → o = some a → Bool) → Option α
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
/-- Let `F` be a functor from sheaf of `R`-module to sheaf of `S`-module, if `F` preserves
colimits and `F.obj (unit R) ≅ unit S`, given a `P : Presentation M`, then we will obtain
generators of `Presentation (F.obj M)`.  -/
SheafOfModules.Presentation.mapGenerators : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat] →
          [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] →
            {C' : Type u₂} →
              [inst_3 : CategoryTheory.Category.{v₂, u₂} C'] →
                {J' : CategoryTheory.GrothendieckTopology C'} →
                  {S : CategoryTheory.Sheaf J' RingCat} →
                    [inst_4 : CategoryTheory.HasSheafify J' AddCommGrpCat] →
                      [inst_5 : J'.WEqualsLocallyBijective AddCommGrpCat] →
                        {M : SheafOfModules R} →
                          (P : M.Presentation) →
                            (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) →
                              [CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u₁, max u u₂,
                                      max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂}
                                    F] →
                                (SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)) →
                                  (SheafOfModules.free P.generators.I ⟶ F.obj M)
-- Mathlib.RingTheory.Ideal.Height
/-- For a prime ideal, its height equals its prime height.  -/
_private.Mathlib.RingTheory.Ideal.Height.0.Ideal.height_eq_primeHeight : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) [inst_1 : I.IsPrime], I.height = Ideal.primeHeight✝ I
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Priority.percent.inj : ∀ {p p_1 : Aesop.Percent}, Aesop.Frontend.Priority.percent p = Aesop.Frontend.Priority.percent p_1 → p = p_1
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_eq_default : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {a : α}, a ∉ m → Std.ExtDHashMap.Const.get! m a = default
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.exists_SL2_smul_eq_of_apply_zero_one_ne_zero : ∀ (g : Matrix.SpecialLinearGroup (Fin 2) ℝ),
  ↑g 1 0 ≠ 0 →
    ∃ u v w, (fun x => g • x) = (fun x => w +ᵥ x) ∘ (fun x => ModularGroup.S • x) ∘ (fun x => v +ᵥ x) ∘ fun x => u • x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.entryAtIdx!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited ((a : α) × β a)] {i : ℕ}, t₁.Equiv t₂ → t₁.entryAtIdx! i = t₂.entryAtIdx! i
-- Mathlib.Geometry.Euclidean.SignedDist
AffineSubspace.signedInfDist_singleton : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (p q : P), (affineSpan ℝ {q}).signedInfDist p = (signedDist (p -ᵥ q)) q
-- Init.Data.Float.Model.Float32
Float32.Model.instMul : Mul Float32.Model
-- Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
SSet.modelCategoryQuillen.horn_ι_mem_J : ∀ (n : ℕ) [NeZero n] (i : Fin (n + 1)), SSet.modelCategoryQuillen.J (SSet.horn n i).ι
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- The natural isomorphism between a pullback cone and the corresponding pullback cone
reconstructed using `PullbackCone.mk`.  -/
CategoryTheory.Limits.PullbackCone.eta : {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) → t ≅ CategoryTheory.Limits.PullbackCone.mk t.fst t.snd ⋯
-- Mathlib.Topology.Order.OrderClosed
Ico_mem_nhdsGE : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {a b : α},
  b < a → Set.Ico b a ∈ nhdsWithin b (Set.Ici b)
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.OrdSet.mk.sizeOf_spec : ∀ {α : Type} [inst : Hashable α] [inst_1 : BEq α] [inst_2 : SizeOf α] (elems : Array α) (set : Std.HashSet α),
  sizeOf { elems := elems, set := set } = 1 + sizeOf elems + sizeOf set
-- Std.Async.Select
_private.Std.Async.Select.0.Std.Async.Waiter.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (finished : IO.Ref Bool) (promise : IO.Promise (Except IO.Error α)),
  sizeOf { finished := finished, promise := promise } = 1 + sizeOf finished + sizeOf promise
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.innerSL_apply_comp : ∀ {𝕜 : 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 : CompleteSpace E] [inst_6 : CompleteSpace F] (x : F) (f : E →L[𝕜] F),
  (innerSL 𝕜) x ∘SL f = (innerSL 𝕜) ((ContinuousLinearMap.adjoint f) x)
-- Mathlib.Data.Vector.Basic
/-- The first element of `scanl` of a vector `v : Vector α n`,
retrieved via `head`, is the starting value `b : β`.
 -/
List.Vector.scanl_head : ∀ {α : Type u_1} {n : ℕ} {β : Type u_6} (f : β → α → β) (b : β) (v : List.Vector α n),
  (List.Vector.scanl f b v).head = b
-- Mathlib.Logic.Embedding.Basic
Equiv.embeddingCongr_apply_trans : ∀ {α₁ : Sort u_1} {β₁ : Sort u_2} {γ₁ : Sort u_3} {α₂ : Sort u_4} {β₂ : Sort u_5} {γ₂ : Sort u_6} (ea : α₁ ≃ α₂)
  (eb : β₁ ≃ β₂) (ec : γ₁ ≃ γ₂) (f : α₁ ↪ β₁) (g : β₁ ↪ γ₁),
  (ea.embeddingCongr ec) (f.trans g) = ((ea.embeddingCongr eb) f).trans ((eb.embeddingCongr ec) g)
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.PreservesEpimorphisms.of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} [F.PreservesEpimorphisms] (α : F ≅ G), G.PreservesEpimorphisms
-- Mathlib.Order.Filter.FilterProduct
Filter.Germ.instGroupWithZero : {α : Type u} → {β : Type v} → {φ : Ultrafilter α} → [GroupWithZero β] → GroupWithZero ((↑φ).Germ β)
-- Mathlib.MeasureTheory.Group.AEStabilizer
MulAction.aestabilizer_congr : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {x : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_2 : MeasureTheory.SMulInvariantMeasure G α μ] {s t : Set α},
  s =ᵐ[μ] t → MulAction.aestabilizer G μ s = MulAction.aestabilizer G μ t
-- Lean.Environment
_private.Lean.Environment.0.Lean.Kernel.Environment.extensions : Lean.Kernel.Environment → Array Lean.EnvExtensionState
-- Std.Http.Data.Request
/-- Optional dynamic metadata attached to the request.
 -/
Std.Http.Request.Builder.extensions : Std.Http.Request.Builder → Std.Http.Extensions
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.le_of_mono : ∀ {n m : ℕ} (f : { len := n } ⟶ { len := m }) [CategoryTheory.Mono f], n ≤ m
-- Batteries.Recycling.MonadSatisfying.Basic
/-- `SatisfiesM` distributes over `<*`, general version.  -/
SatisfiesM.seqLeft : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {p₁ : α → Prop} {a : Type u_1} {p₂ : a → Prop} {y : m a} {q : α → Prop}
  [inst : Applicative m] [LawfulApplicative m] {x : m α},
  SatisfiesM p₁ x → SatisfiesM p₂ y → (∀ {a_1 : α} {b : a}, p₁ a_1 → p₂ b → q a_1) → SatisfiesM q (x <* y)
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.symm_apply_mk_proj : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) {x : Z},
  x ∈ e.source → ↑e.symm (proj x, (↑e x).2) = x
-- Mathlib.Data.Num.Lemmas
Num.mul_to_nat : ∀ (m n : Num), ↑(m * n) = ↑m * ↑n
-- Mathlib.Data.Finset.Lattice.Basic
Finset.union_congr_left : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Finset α}, t ⊆ s ∪ u → u ⊆ s ∪ t → s ∪ t = s ∪ u
-- Mathlib.Topology.Order.OrderClosed
BddBelow.of_closure : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] {s : Set α}, BddBelow (closure s) → BddBelow s
-- Mathlib.Analysis.CStarAlgebra.Classes
CommCStarAlgebra.toNonUnitalCommCStarAlgebra : (A : Type u_1) → [CommCStarAlgebra A] → NonUnitalCommCStarAlgebra A
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_eval_C : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (r : R) (a : A),
  autoParam (p a) cfc_eval_C._auto_1 → cfc (fun x => Polynomial.eval x (Polynomial.C r)) a = (algebraMap R A) r
-- Init.Data.String.Slice
/-- Converts a string to the Lean compiler's representation of names. The resulting name is
hierarchical, and the string is split at the dots \(`'.'`\).

`"a.b".toSlice.toName` is the name `a.b`, not `«a.b»`. For the latter, use
`Name.mkSimple`.
 -/
String.Slice.toName : String.Slice → Lean.Name
-- Lean.Elab.InfoTree.Types
Lean.Elab.MonadParentDecl : (Type → Type) → Type
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_nil : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {a fallback : α}, Std.Internal.List.getKeyD a [] fallback = fallback
-- Mathlib.Order.Filter.IsBounded
Filter.isBoundedUnder_ge_sum : ∀ {α : Type u_5} {f : Filter α} {R : Type u_6} [inst : Preorder R] {κ : Type u_7} [inst_1 : AddCommMonoid R]
  [AddLeftMono R] [AddRightMono R] {u : κ → α → R} (s : Finset κ),
  (∀ k ∈ s, Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) f (u k)) →
    Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) f (∑ k ∈ s, u k)
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.tag.eq_1 : ∀ {ι : Type u_1} (n : ℕ) (ν : ι → ℤ) (i : ι), BoxIntegral.unitPartition.tag n ν i = (↑(ν i) + 1) / ↑n
-- Mathlib.GroupTheory.Torsion
IsAddTorsion.torsionAddEquiv_apply : ∀ {G : Type u_1} [inst : AddCommMonoid G] (tG : IsAddTorsion G) (a : ↥(AddCommMonoid.addTorsion G)),
  tG.torsionAddEquiv a = ↑((AddEquiv.addSubmonoidCongr ⋯) a)
-- Lean.Widget.TaggedText
Lean.Widget.TaggedText.brecOn_2.go : {α : Type u} →
  {motive_1 : Lean.Widget.TaggedText α → Sort u_1} →
    {motive_2 : Array (Lean.Widget.TaggedText α) → Sort u_1} →
      {motive_3 : List (Lean.Widget.TaggedText α) → Sort u_1} →
        (t : List (Lean.Widget.TaggedText α)) →
          ((t : Lean.Widget.TaggedText α) → t.below → motive_1 t) →
            ((t : Array (Lean.Widget.TaggedText α)) → Lean.Widget.TaggedText.below_1 t → motive_2 t) →
              ((t : List (Lean.Widget.TaggedText α)) → Lean.Widget.TaggedText.below_2 t → motive_3 t) →
                motive_3 t ×' Lean.Widget.TaggedText.below_2 t
-- Mathlib.RingTheory.PowerSeries.Evaluation
PowerSeries.uniformContinuous_eval₂ : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {φ : R →+* S} {a : S}
  [inst_2 : UniformSpace R] [inst_3 : UniformSpace S] [IsUniformAddGroup R] [IsTopologicalSemiring R]
  [IsUniformAddGroup S] [T2Space S] [CompleteSpace S] [IsTopologicalRing S] [IsLinearTopology S S],
  Continuous ⇑φ → PowerSeries.HasEval a → UniformContinuous (PowerSeries.eval₂ φ a)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_smul_measure : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} (f : α → G) (c : ENNReal), ∫ (x : α), f x ∂c • μ = c.toReal • ∫ (x : α), f x ∂μ
-- Aesop.Tree.Data
Aesop.Rapp.setIsIrrelevant : Bool → Aesop.Rapp → Aesop.Rapp
-- Init.Data.BitVec.Basic
/-- Unexpander for bitvector literals without truncation.  -/
BitVec.unexpandBitVecOfNatLt : Lean.PrettyPrinter.Unexpander
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey_eq_getElem_keysArray : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {he : t.isEmpty = false}, t.minKey he = t.keysArray[0]
-- Init.Data.Int.DivMod.Lemmas
Int.fmod.eq_1 : ∀ (x : ℤ), Int.fmod 0 x = 0