mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k a : α} {fallback v : β},
  Std.ExtDTreeMap.Const.getD (t.insert k v) a fallback =
    if cmp k a = Ordering.eq then v else Std.ExtDTreeMap.Const.getD t a fallback
-- Mathlib.Data.Fintype.Basic
Finset.val_univ_fin : ∀ (n : ℕ), Finset.univ.val = ↑(List.finRange n)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Tactic.ComputeAsymptotics.Seq.FriendlyOperation.unfold.congr_simp : ∀ {α : Type u_1} {op op_1 : Stream'.Seq α → Stream'.Seq α} (e_op : op = op_1)
  (h : Tactic.ComputeAsymptotics.Seq.FriendlyOperation op) (hd? hd?_1 : Option α),
  hd? = hd?_1 → h.unfold hd? = ⋯.unfold hd?_1
-- Mathlib.Algebra.Category.Grp.Ulift
/-- The universe lift functor for commutative additive groups is faithful.  -/
AddCommGrpCat.instFaithfulUliftFunctor : AddCommGrpCat.uliftFunctor.Faithful
-- Mathlib.FieldTheory.Galois.Infinite
/-- If `H` is a closed normal subgroup of `Gal(K / k)`,
then `Gal(fixedField H / k)` is isomorphic to `Gal(K / k) ⧸ H`.  -/
InfiniteGalois.normalAutEquivQuotient : {k : Type u_1} →
  {K : Type u_2} →
    [inst : Field k] →
      [inst_1 : Field K] →
        [inst_2 : Algebra k K] →
          [IsGalois k K] →
            (H : ClosedSubgroup Gal(K/k)) →
              [inst_4 : (↑H).Normal] → Gal(K/k) ⧸ ↑H ≃* Gal(↥(IntermediateField.fixedField ↑H)/k)
-- Mathlib.Data.FunLike.IsApply
FunLike.coe_one_eq_id : ∀ {F' : Type u_4} {α : Type u_5} [inst : FunLike F' α α] [inst_1 : One F'] [IsOneApplyEqSelf F' α], ⇑1 = id
-- Mathlib.CategoryTheory.Category.KleisliCat
CategoryTheory.KleisliCat.categoryStruct : {m : Type u → Type v} → [Monad m] → CategoryTheory.CategoryStruct.{max u v, u + 1} (CategoryTheory.KleisliCat m)
-- Batteries.Data.Nat.Lemmas
Nat.recAux_zero : ∀ {motive : ℕ → Sort u_1} (zero : motive 0) (succ : (n : ℕ) → motive n → motive (n + 1)), Nat.recAux zero succ 0 = zero
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.map_id_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct W X] [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct W Y]
  [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct W Z] {Z_1 : C} (h : W ⨿ Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id W) (CategoryTheory.CategoryStruct.comp f g))
      h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id W) f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id W) g) h)
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.isCoprime_iff_aeval_ne_zero : ∀ {K : Type v} [inst : Field K] (f g : Polynomial K),
  IsCoprime f g ↔
    ∀ {A : Type v} [inst_1 : CommRing A] [IsDomain A] [inst_3 : Algebra K A] (a : A),
      (Polynomial.aeval a) f ≠ 0 ∨ (Polynomial.aeval a) g ≠ 0
-- Mathlib.LinearAlgebra.Projectivization.Basic
Projectivization.mk''_submodule : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (v : Projectivization K V), Projectivization.mk'' v.submodule ⋯ = v
-- Mathlib.CategoryTheory.Core
/-- Equivalent categories have equivalent cores.  -/
CategoryTheory.Equivalence.core : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (C ≌ D) → (CategoryTheory.Core C ≌ CategoryTheory.Core D)
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.IsRat.of_raw : ∀ (α : Type u_1) [inst : DivisionRing α] (n : ℤ) (d : ℕ), ↑d ≠ 0 → Mathlib.Meta.NormNum.IsRat (Rat.rawCast n d) n d
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.posFittingComp_le_iInf_lowerCentralSeries : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L], LieModule.posFittingComp R L M ≤ ⨅ k, LieModule.lowerCentralSeries R L M k
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get_insertIfNew : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] (h : (↑m).WF) {k a : α} {v : β k} {h₁ : (m.insertIfNew k v).contains a = true},
  (m.insertIfNew k v).get a h₁ = if h₂ : (k == a) = true ∧ m.contains k = false then cast ⋯ v else m.get a ⋯
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
MeasureTheory.SignedMeasure.singularPart_smul_nnreal : ∀ {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α) (r : NNReal),
  (r • s).singularPart μ = r • s.singularPart μ
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- When a functor `F` preserves the left homology of a short complex `S`, this is the
canonical isomorphism `(S.map F).cycles ≅ F.obj S.cycles`.  -/
CategoryTheory.ShortComplex.mapCyclesIso : {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.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (S : CategoryTheory.ShortComplex C) →
              (F : CategoryTheory.Functor C D) →
                [inst_4 : F.PreservesZeroMorphisms] →
                  [inst_5 : S.HasLeftHomology] →
                    [inst_6 : F.PreservesLeftHomologyOf S] → (S.map F).cycles ≅ F.obj S.cycles
-- Mathlib.Tactic.Linarith.Frontend
_private.Mathlib.Tactic.Linarith.Frontend.0.Mathlib.Tactic.instEvalExprLinarithConfig.unsafe_impl_2 : Lean.Expr → Lean.MetaM Mathlib.Tactic.Linarith.LinarithConfig
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- If `f : G → H` is a multiplicative homomorphism between two monoids, then
`MonoidAlgebra.mapDomain f` is a ring homomorphism between their monoid algebras.  -/
MonoidAlgebra.mapDomainRingHom : (R : Type u_3) →
  {M : Type u_6} →
    {N : Type u_7} →
      [inst : Semiring R] →
        [inst_1 : Monoid M] → [inst_2 : Monoid N] → (M →* N) → MonoidAlgebra R M →+* MonoidAlgebra R N
-- Mathlib.Probability.Kernel.Category.Stoch
instIsMarkovKernelCarrierObjSFinKerStochHomHomHomWideSubcategory : ∀ {X Y : Stoch} (κ : X ⟶ Y), ProbabilityTheory.IsMarkovKernel κ.hom.hom
-- Mathlib.Data.Sym.Sym2
Sym2.fromRel_eq_fromRel_iff_eq : ∀ {α : Type u_1} {r₁ r₂ : α → α → Prop} (sym₁ : Std.Symm r₁) (sym₂ : Std.Symm r₂),
  Sym2.fromRel sym₁ = Sym2.fromRel sym₂ ↔ r₁ = r₂
-- Mathlib.Data.Nat.Bits
Nat.bodd_eq_one_and_ne_zero : ∀ (n : ℕ), n.bodd = (1 &&& n != 0)
-- Mathlib.Topology.MetricSpace.PiNat
/-- If two points `x, y` coincide up to length `n`, and the longest common prefix of `x` with `s`
is strictly shorter than `n`, then the longest common prefix of `y` with `s` is the same, and both
cylinders of this length based at `x` and `y` coincide.  -/
PiNat.cylinder_longestPrefix_eq_of_longestPrefix_lt_firstDiff : ∀ {E : ℕ → Type u_1} [inst : (n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)] {x y : (n : ℕ) → E n}
  {s : Set ((n : ℕ) → E n)},
  IsClosed s →
    s.Nonempty →
      PiNat.longestPrefix x s < PiNat.firstDiff x y →
        x ∉ s → y ∉ s → PiNat.cylinder x (PiNat.longestPrefix x s) = PiNat.cylinder y (PiNat.longestPrefix y s)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- A morphism `f` has a cokernel if the functor `ParallelPair f 0` has a colimit.  -/
CategoryTheory.Limits.HasCokernel : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Limits.HasZeroMorphisms C] → {X Y : C} → (X ⟶ Y) → Prop
-- Aesop.Tree.Data
Aesop.GoalData.state : {Rapp MVarCluster : Type} → Aesop.GoalData Rapp MVarCluster → Aesop.GoalState
-- Mathlib.Data.Quot
/-- Places an element of a type into the quotient that equates terms according to an equivalence
relation.

The setoid instance is provided explicitly. `Quotient.mk'` uses instance synthesis instead.

Given `v : α`, `Quotient.mk s v : Quotient s` is like `v`, except all observations of `v`'s value
must respect `s.r`. `Quotient.lift` allows values in a quotient to be mapped to other types, so long
as the mapping respects `s.r`.
 -/
Quotient.«term⟦_⟧» : Lean.ParserDescr
-- Mathlib.Data.DFinsupp.WellFounded
DFinsupp.Lex.wellFounded : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop},
  (∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0) →
    (∀ (i : ι), WellFounded (s i)) → WellFounded (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) → WellFounded (DFinsupp.Lex r s)
-- Mathlib.Analysis.Normed.Operator.NormedSpace
/-- Postcomposition of a continuous linear map with a linear isometry preserves
the operator norm.  -/
LinearIsometry.norm_toContinuousLinearMap_comp : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_3} {𝕜₃ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_8}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₃ : 𝕜₂ →+* 𝕜₃}
  {σ₁₃ : 𝕜 →+* 𝕜₃} [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomIsometric σ₁₂] (f : F →ₛₗᵢ[σ₂₃] G)
  {g : E →SL[σ₁₂] F}, ‖f.toContinuousLinearMap ∘SL g‖ = ‖g‖
-- Mathlib.RingTheory.Bialgebra.GroupLike
/-- **Alias** of the forward direction of `isGroupLikeElem_unitsInv`. -/
IsGroupLikeElem.of_unitsInv : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A] {u : Aˣ},
  IsGroupLikeElem R ↑u⁻¹ → IsGroupLikeElem R ↑u
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.DeclValue : Lean.Compiler.LCNF.Purity → Type
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.zeta_apply : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : Zero 𝕜] [inst_1 : One 𝕜] [inst_2 : LE α] [inst_3 : DecidableLE α] (a b : α),
  (IncidenceAlgebra.zeta 𝕜) a b = if a ≤ b then 1 else 0
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
CategoryTheory.Functor.IsStronglyCartesian.domainIsoOfBaseIso_inv : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R R' S : 𝒮} {a a' b : 𝒳} {f : R ⟶ S} {f' : R' ⟶ S} {g : R' ≅ R}
  (h : f' = CategoryTheory.CategoryStruct.comp g.hom f) (φ : a ⟶ b) (φ' : a' ⟶ b) [inst_2 : p.IsStronglyCartesian f φ]
  [inst_3 : p.IsStronglyCartesian f' φ'],
  (CategoryTheory.Functor.IsStronglyCartesian.domainIsoOfBaseIso p h φ φ').inv =
    CategoryTheory.Functor.IsStronglyCartesian.map p f' φ' ⋯ φ
-- Mathlib.RingTheory.DividedPowers.DPMorphism
DividedPowers.DPMorphism.ext : ∀ {A : Type u_3} {B : Type u_4} {inst : CommSemiring A} {inst_1 : CommSemiring B} {I : Ideal A} {J : Ideal B}
  {hI : DividedPowers I} {hJ : DividedPowers J} {x y : hI.DPMorphism hJ},
  (↑↑x.toRingHom).toFun = (↑↑y.toRingHom).toFun → x = y
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsValidSearchFrom.below : {ρ : Type} →
  {pat : ρ} →
    [inst : String.Slice.Pattern.Model.PatternModel pat] →
      {s : String.Slice} →
        {motive :
            (a : s.Pos) →
              (a_1 : List (String.Slice.Pattern.SearchStep s)) →
                String.Slice.Pattern.Model.IsValidSearchFrom pat a a_1 → Prop} →
          {a : s.Pos} →
            {a_1 : List (String.Slice.Pattern.SearchStep s)} →
              String.Slice.Pattern.Model.IsValidSearchFrom pat a a_1 → Prop
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
/-- A non-trivial `concat` walk is representable as a `cons` walk.  -/
SimpleGraph.Walk.exists_concat_eq_cons : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (h : G.Adj v w),
  ∃ x, ∃ (h' : G.Adj u x), ∃ q, p.concat h = SimpleGraph.Walk.cons h' q
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_castLEEmb_Iio : ∀ {n m : ℕ} (a : Fin n) (h : n ≤ m), Finset.map (Fin.castLEEmb h) (Finset.Iio a) = Finset.Iio (Fin.castLE h a)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.preEquivalence_unitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G),
  (CategoryTheory.StructuredArrow.preEquivalence F f).unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun X =>
        CategoryTheory.StructuredArrow.isoMk
          (CategoryTheory.StructuredArrow.isoMk
            (CategoryTheory.Iso.refl
              ((CategoryTheory.Functor.id
                        (CategoryTheory.StructuredArrow f (CategoryTheory.StructuredArrow.pre e F G))).obj
                    X).right.right)
            ⋯)
          ⋯)
      ⋯
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IndObjectPresentation.instFinalICostructuredArrowFunctorOppositeTypeYonedaToCostructuredArrow : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  (P : CategoryTheory.Limits.IndObjectPresentation A), P.toCostructuredArrow.Final
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.unitOfList_singleton : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {k : α},
  Std.ExtTreeMap.unitOfList [k] cmp = ∅.insertIfNew k ()
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.InjectivePresentation.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} [inst_1 : SizeOf C] (J : C)
  (injective : autoParam (CategoryTheory.Injective J) CategoryTheory.InjectivePresentation.injective._autoParam)
  (f : X ⟶ J) (mono : autoParam (CategoryTheory.Mono f) CategoryTheory.InjectivePresentation.mono._autoParam),
  sizeOf { J := J, injective := injective, f := f, mono := mono } =
    1 + sizeOf J + sizeOf injective + sizeOf f + sizeOf mono
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
/-- If `M` is quasicoherent, it is locally generated by sections.  -/
SheafOfModules.QuasicoherentData.localGeneratorsData : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] →
          [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] →
            {M : SheafOfModules R} → M.QuasicoherentData → M.LocalGeneratorsData
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
/-- Define the cube root of unity `ρ := (-1 + √-3) / 2` as an element of the upper half plane.  -/
UpperHalfPlane.ρ : UpperHalfPlane
-- Init.Data.String.Lemmas.Intercalate
String.Slice.join_eq : ∀ {l : List String.Slice}, String.Slice.join l = String.join (List.map String.Slice.copy l)
-- Mathlib.Topology.Homotopy.Path
Path.Homotopy.hcomp_apply : ∀ {X : Type u} [inst : TopologicalSpace X] {x₀ x₁ x₂ : X} {p₀ q₀ : Path x₀ x₁} {p₁ q₁ : Path x₁ x₂} (F : p₀.Homotopy q₀)
  (G : p₁.Homotopy q₁) (x : ↑unitInterval × ↑unitInterval),
  (F.hcomp G) x = if h : ↑x.2 ≤ 1 / 2 then (F.eval x.1) ⟨2 * ↑x.2, ⋯⟩ else (G.eval x.1) ⟨2 * ↑x.2 - 1, ⋯⟩
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.instCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.Preadditive C] → CategoryTheory.Category.{v₁, max 1 u₁} (CategoryTheory.Mat_ C)
-- Std.Data.DHashMap.Basic
/-- Tries to retrieve the mapping for the given key, panicking if no such mapping is present.

Uses the `LawfulBEq` instance to cast the retrieved value to the correct type.
 -/
Std.DHashMap.get! : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} → {x_1 : Hashable α} → [LawfulBEq α] → Std.DHashMap α β → (a : α) → [Inhabited (β a)] → β a
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
ThreeAPFree.vadd_set : ∀ {α : Type u_2} [inst : AddCommMonoid α] [IsCancelAdd α] {s : Set α} {a : α}, ThreeAPFree s → ThreeAPFree (a +ᵥ s)
-- Mathlib.Algebra.Group.Prod
/-- Four-way commutativity of `Prod`.
The name matches `mul_mul_mul_comm`  -/
AddEquiv.prodProdProdComm : (M : Type u_3) →
  (N : Type u_4) →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass N] →
        (M' : Type u_6) →
          (N' : Type u_7) →
            [inst_2 : AddZeroClass N'] → [inst_3 : AddZeroClass M'] → (M × N) × M' × N' ≃+ (M × M') × N × N'
-- Mathlib.CategoryTheory.Comma.Basic
/-- Two equal natural transformations `L₁ ⟶ L₂` yield naturally isomorphic functors
`Comma L₁ R ⥤ Comma L₂ R`.  -/
CategoryTheory.Comma.mapLeftEq : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            (R : CategoryTheory.Functor B T) →
              {L₁ L₂ : CategoryTheory.Functor A T} →
                (l l' : L₁ ⟶ L₂) → l = l' → (CategoryTheory.Comma.mapLeft R l ≅ CategoryTheory.Comma.mapLeft R l')
-- Mathlib.CategoryTheory.Monad.Monadicity
CategoryTheory.Monad.PreservesColimitOfIsSplitPair.out : ∀ {C : Type u₁} {D : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.Category.{v₁, u₂} D}
  {G : CategoryTheory.Functor D C} [self : CategoryTheory.Monad.PreservesColimitOfIsSplitPair G] {A B : D} (f g : A ⟶ B)
  [G.IsSplitPair f g], CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- Conversion to normal form on `U` does not change values outside of `U`.
 -/
toMeromorphicNFOn_eq_self_on_compl : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜}, MeromorphicOn f U → Set.EqOn (toMeromorphicNFOn f U) f Uᶜ
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.coeff_add : ∀ {R : Type u_1} [inst : Semiring R] (p q : SkewPolynomial R) (n : ℕ), (p + q).coeff n = p.coeff n + q.coeff n
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.map_id_comp_H0Iso_hom_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B : Rep.{u, u, u} k G} (f : A ⟶ B)
  (x : ↑(groupHomology A 0)),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.H0Iso B).hom)
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.map (MonoidHom.id G) f 0)) x) =
    (Representation.Coinvariants.map A.ρ B.ρ (Rep.Hom.hom f))
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.H0Iso A).hom) x)
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.of_mul_add_right_right : ∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsRelPrime x (z * x + y) → IsRelPrime x y
-- Mathlib.Order.Interval.Set.Pi
Set.image_mulSingle_Ioc_right : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : (i : ι) → One (α i)] (i : ι) (b : α i), Pi.mulSingle i '' Set.Ioc 1 b = Set.Ioc 1 (Pi.mulSingle i b)
-- Mathlib.Algebra.Ring.BooleanRing
ofBoolRing_add : ∀ {α : Type u_1} [inst : BooleanAlgebra α] (a b : AsBoolRing α),
  ofBoolRing (a + b) = symmDiff (ofBoolRing a) (ofBoolRing b)
-- Init.Data.Int.Order
Int.exists_eq_neg_ofNat : ∀ {a : ℤ}, a ≤ 0 → ∃ n, a = -↑n
-- Init.Data.UInt.Lemmas
UInt32.toFin_inj : ∀ {a b : UInt32}, a.toFin = b.toFin ↔ a = b
-- Mathlib.Logic.Equiv.Finset
/-- The elements of a `Fintype` as a sorted list.  -/
Encodable.sortedUniv : (α : Type u_1) → [Fintype α] → [Encodable α] → List α
-- Mathlib.NumberTheory.ModularForms.Cusps
IsCusp.smul_of_mem : ∀ {c : OnePoint ℝ} {𝒢 : Subgroup (GL (Fin 2) ℝ)}, IsCusp c 𝒢 → ∀ {g : GL (Fin 2) ℝ}, g ∈ 𝒢 → IsCusp (g • c) 𝒢
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.uliftFunctorInclusion_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) (X_1 : Cᵒᵖ),
  S.uliftFunctorInclusion.app X_1 = TypeCat.ofHom fun x => { down := ↑x.down }
-- Mathlib.Topology.Order.AtTopBotIxx
tendsto_comp_coe_Ioo_atTop : ∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] {a b : X} {α : Type u_2}
  {l : Filter α} {f : X → α},
  a < b →
    autoParam (Order.IsSuccPrelimit b) tendsto_comp_coe_Ioo_atTop._auto_1 →
      (Filter.Tendsto (fun x => f ↑x) Filter.atTop l ↔ Filter.Tendsto f (nhdsWithin b (Set.Iio b)) l)
-- Mathlib.Data.Nat.Cast.Commute
Commute.ofNat_left : ∀ {α : Type u_1} [inst : NonAssocSemiring α] (n : ℕ) [inst_1 : n.AtLeastTwo] (x : α), Commute (OfNat.ofNat n) x
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.prodEquiv_apply : ∀ {G : Type u} [inst : AddGroup G] {H : Type v} [inst_1 : AddGroup H] (A : AddSubgroup G) (B : AddSubgroup H)
  (q : (G × H) ⧸ A.prod B),
  (QuotientAddGroup.prodEquiv A B) q =
    Quotient.liftOn' q
      (fun x =>
        match x with
        | (g, h) => (↑g, ↑h))
      ⋯
-- Mathlib.Order.Filter.Basic
Filter.isLUB_sSup : ∀ {α : Type u} (s : Set (Filter α)), IsLUB s (sSup s)
-- Lean.Server.References
_private.Lean.Server.References.0.Lean.Server.combineIdents.insertIdMap : Lean.Lsp.RefIdent → Lean.Lsp.RefIdent → StateT (Std.HashMap Lean.Lsp.RefIdent Lean.Lsp.RefIdent) Id Unit
-- Mathlib.Order.WellFoundedSet
Set.wellFoundedOn_union : ∀ {α : Type u_2} {r : α → α → Prop} [IsStrictOrder α r] {s t : Set α},
  (s ∪ t).WellFoundedOn r ↔ s.WellFoundedOn r ∧ t.WellFoundedOn r
-- Init.Data.Int.DivMod.Lemmas
Int.mul_emod_bmod : ∀ {y : ℤ} (x : ℤ) (n : ℕ), (y * (x % ↑n)).bmod n = (y * x).bmod n
-- Lean.Expr
/-- If the expression is a constant, return that name.
Otherwise panic.
 -/
Lean.Expr.constName! : Lean.Expr → Lean.Name
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getD_diff_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k fallback : α}, k ∉ t₂ → (t₁ \ t₂).getD k fallback = t₁.getD k fallback
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.get?.eq_2 : ∀ {α : Type u} {δ : Type w} [inst : Ord α] (k : α) (size : ℕ) (k' : α) (v' : δ)
  (l r : Std.DTreeMap.Internal.Impl α fun x => δ),
  Std.DTreeMap.Internal.Impl.Const.get? (Std.DTreeMap.Internal.Impl.inner size k' v' l r) k =
    match compare k k' with
    | Ordering.lt => Std.DTreeMap.Internal.Impl.Const.get? l k
    | Ordering.gt => Std.DTreeMap.Internal.Impl.Const.get? r k
    | Ordering.eq => some v'
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.Measure.smul_finite : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] {c : ENNReal},
  c ≠ ⊤ → MeasureTheory.IsFiniteMeasure (c • μ)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey_congr : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h : m.WF) {k₁ k₂ : α} (h' : (k₁ == k₂) = true) (h₁ : k₁ ∈ m),
  m.getKey k₁ h₁ = m.getKey k₂ ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Cofork.IsColimit.π_desc : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y}
  {s t : CategoryTheory.Limits.Cofork f g} (hs : CategoryTheory.Limits.IsColimit s),
  CategoryTheory.CategoryStruct.comp s.π (hs.desc t) = t.π
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- Eta-expanded form of `ContDiffWithinAt.inv` -/
ContDiffWithinAt.fun_inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {x : E} {𝕜' : Type u_4} [inst_3 : NormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  {f : E → 𝕜'} {n : WithTop ℕ∞}, ContDiffWithinAt 𝕜 n f s x → f x ≠ 0 → ContDiffWithinAt 𝕜 n (fun i => (f i)⁻¹) s x
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.ordered_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β} {h : t.Balanced}
  {f : (a : α) → β a → Option (γ a)}, t.Ordered → (Std.DTreeMap.Internal.Impl.filterMap f t h).impl.Ordered