mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- If `α` and `β` are arbitrary types and there is a surjection between them,
then the induced map on their additive free groups is also surjective.  -/
FreeAddGroup.map_surjective : ∀ {α : Type u} {β : Type v} {f : α → β}, Function.Surjective f → Function.Surjective ⇑(FreeAddGroup.map f)
-- Mathlib.Geometry.Manifold.MFDeriv.Defs
/-- `MDifferentiableAt I I' f x` indicates that the function `f` between manifolds
has a derivative at the point `x`.
This is a generalization of `DifferentiableAt` to manifolds.

We require continuity in the definition, as otherwise points close to `x` could be sent by
`f` outside of the chart domain around `f x`. Then the chart could do anything to the image points,
and in particular by coincidence `writtenInExtChartAt I I' x f` could be differentiable, while
this would not mean anything relevant.  -/
MDifferentiableAt : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              ModelWithCorners 𝕜 E H →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [ChartedSpace H M] →
                      {E' : Type u_5} →
                        [inst_6 : NormedAddCommGroup E'] →
                          [inst_7 : NormedSpace 𝕜 E'] →
                            {H' : Type u_6} →
                              [inst_8 : TopologicalSpace H'] →
                                ModelWithCorners 𝕜 E' H' →
                                  {M' : Type u_7} →
                                    [inst : TopologicalSpace M'] → [ChartedSpace H' M'] → (M → M') → M → Prop
-- Mathlib.Algebra.Order.ToIntervalMod
iUnion_Ico_add_zsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] [Archimedean α] {p : α},
  0 < p → ∀ (a : α), ⋃ n, Set.Ico (a + n • p) (a + (n + 1) • p) = Set.univ
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.elabSingleIndexingMode : Lean.Syntax → Aesop.ElabM Aesop.IndexingMode
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
/-- Any two `IsAddKleinFour` groups are isomorphic.  -/
IsAddKleinFour.nonempty_addEquiv : ∀ {G₁ : Type u_2} {G₂ : Type u_3} [inst : AddGroup G₁] [inst_1 : AddGroup G₂] [IsAddKleinFour G₁] [IsAddKleinFour G₂],
  Nonempty (G₁ ≃+ G₂)
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.isClosed_proj : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] (o : Ordinal.{u}),
  IsClosed C → IsClosed (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o)
-- Lean.Meta.Tactic.Simp.SimpCongrTheorems
Lean.Meta.SimpCongrTheorem.funName : Lean.Meta.SimpCongrTheorem → Lean.Name
-- Mathlib.Data.Finset.Sym
Finset.sym2_insert : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α),
  (insert a s).sym2 = Finset.image (fun b => s(a, b)) (insert a s) ∪ s.sym2
-- Init.Data.Array.Range
Array.range'_append : ∀ {s m n step : ℕ}, Array.range' s m step ++ Array.range' (s + step * m) n step = Array.range' s (m + n) step
-- Lean.Meta.Tactic.Grind.CollectParams
_private.Lean.Meta.Tactic.Grind.CollectParams.0.Lean.Meta.Grind.Collector.State.mk.inj : ∀ {params : Array Lean.Meta.Grind.TParam} {anchors : Array Lean.Meta.Grind.TAnchor✝} {hasSorry : Bool}
  {params_1 : Array Lean.Meta.Grind.TParam} {anchors_1 : Array Lean.Meta.Grind.TAnchor✝} {hasSorry_1 : Bool},
  { params := params, anchors := anchors, hasSorry := hasSorry } =
      { params := params_1, anchors := anchors_1, hasSorry := hasSorry_1 } →
    params = params_1 ∧ anchors = anchors_1 ∧ hasSorry = hasSorry_1
-- Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
/-- The continuous `σ`-semilinear maps between two vector bundles form a fiber bundle.  -/
Bundle.ContinuousAlternatingMap.instFiberBundle : {𝕜 : Type u_1} →
  {ι : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : Fintype ι] →
        {B : Type u_3} →
          [inst_2 : TopologicalSpace B] →
            {F₁ : Type u_4} →
              [inst_3 : NormedAddCommGroup F₁] →
                [inst_4 : NormedSpace 𝕜 F₁] →
                  {E₁ : B → Type u_5} →
                    [inst_5 : (x : B) → AddCommGroup (E₁ x)] →
                      [inst_6 : (x : B) → Module 𝕜 (E₁ x)] →
                        [inst_7 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] →
                          [inst_8 : (x : B) → TopologicalSpace (E₁ x)] →
                            [inst_9 : FiberBundle F₁ E₁] →
                              [inst_10 : VectorBundle 𝕜 F₁ E₁] →
                                {F₂ : Type u_6} →
                                  [inst_11 : NormedAddCommGroup F₂] →
                                    [inst_12 : NormedSpace 𝕜 F₂] →
                                      {E₂ : B → Type u_7} →
                                        [inst_13 : (x : B) → AddCommGroup (E₂ x)] →
                                          [inst_14 : (x : B) → Module 𝕜 (E₂ x)] →
                                            [inst_15 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] →
                                              [inst_16 : (x : B) → TopologicalSpace (E₂ x)] →
                                                [inst_17 : FiberBundle F₂ E₂] →
                                                  [inst_18 : VectorBundle 𝕜 F₂ E₂] →
                                                    [inst_19 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)] →
                                                      [inst_20 : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] →
                                                        FiberBundle (F₁ [⋀^ι]→L[𝕜] F₂) fun x => E₁ x [⋀^ι]→L[𝕜] E₂ x
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.StrictOrLazy.lazy.sizeOf_spec : ∀ {α β : Type} [inst : SizeOf α] [inst_1 : SizeOf β] (a : β), sizeOf (Lean.Widget.StrictOrLazy.lazy a) = 1 + sizeOf a
-- Mathlib.RingTheory.EssentialFiniteness
Algebra.EssFiniteType.of_surjective : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] (f : S →ₐ[R] T),
  Function.Surjective ⇑f → ∀ [Algebra.EssFiniteType R S], Algebra.EssFiniteType R T
-- Mathlib.Data.List.NatAntidiagonal
List.Nat.antidiagonal.eq_1 : ∀ (n : ℕ), List.Nat.antidiagonal n = List.map (fun i => (i, n - i)) (List.range (n + 1))
-- Mathlib.Data.Bool.AllAny
List.any_of_mem : ∀ {α : Type u_1} {l : List α} {a : α} {p : α → Bool}, a ∈ l → p a = true → l.any p = true
-- Mathlib.Analysis.Normed.Module.MStructure
IsLprojection.Lcomplement_iff : ∀ {X : Type u_1} [inst : NormedAddCommGroup X] {M : Type u_2} [inst_1 : Ring M] [inst_2 : Module M X] (P : M),
  IsLprojection X P ↔ IsLprojection X (1 - P)
-- Mathlib.Algebra.Lie.SkewAdjoint
mem_skewAdjointMatricesLieSubalgebra : ∀ {R : Type u} {n : Type w} [inst : CommRing R] [inst_1 : Fintype n] (J : Matrix n n R) [inst_2 : DecidableEq n]
  (A : Matrix n n R), A ∈ skewAdjointMatricesLieSubalgebra J ↔ A ∈ skewAdjointMatricesSubmodule J
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.image_source_eq_target : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), ↑e '' e.source = e.target
-- Mathlib.CategoryTheory.WithTerminal.Cone
/-- A cocone of a functor `K : J ⥤ Under X` consists of an object of `Under X`, together
with morphisms. This same object is a cocone of the extended functor
`liftFromUnder.obj K : WithInitial J ⥤ C`.  -/
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithInitial.coconeLift : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{w', w} J] →
        {X : C} →
          {K : CategoryTheory.Functor J (CategoryTheory.Under X)} →
            CategoryTheory.Functor (CategoryTheory.Limits.Cocone K)
              (CategoryTheory.Limits.Cocone (CategoryTheory.WithInitial.liftFromUnder.obj K))
-- Mathlib.GroupTheory.Perm.Sign
/-- `modSwap i j` contains permutations up to swapping `i` and `j`.

We use this to partition permutations in `Matrix.det_zero_of_row_eq`, such that each partition
sums up to `0`.
 -/
Equiv.Perm.modSwap : {α : Type u} → [DecidableEq α] → α → α → Setoid (Equiv.Perm α)
-- Mathlib.Algebra.Order.Kleene
IdemSemiring.mk : {α : Type u_5} →
  [toSemiring : Semiring α] →
    [toSemilatticeSup : SemilatticeSup α] →
      [toOrderBot : OrderBot α] →
        autoParam (∀ (a b : α), a + b = a ⊔ b) IdemSemiring.add_eq_sup._autoParam → IdemSemiring α
-- Mathlib.RingTheory.DedekindDomain.IntegralClosure
/-- If `L` is a finite separable extension of `K = Frac(A)`, where `A` is
integrally closed and Noetherian, the integral closure of `A` in `L` is
Noetherian.  -/
integralClosure.isNoetherianRing : ∀ {A : Type u_1} {K : Type u_2} [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K] [IsFractionRing A K]
  (L : Type u_3) [inst_4 : Field L] [inst_5 : Algebra K L] [inst_6 : Algebra A L] [IsScalarTower A K L]
  [FiniteDimensional K L] [IsDomain A] [Algebra.IsSeparable K L] [IsIntegrallyClosed A] [IsNoetherianRing A],
  IsNoetherianRing ↥(integralClosure A L)
-- Mathlib.Algebra.Lie.InvariantForm
LieAlgebra.InvariantForm.atomistic : ∀ {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) → ∀ (I : LieIdeal K L), sSup {J | IsAtom J ∧ J ≤ I} = I
-- Mathlib.Algebra.Group.Action.Hom
AddAction.compHom.eq_1 : ∀ {M : Type u_1} {N : Type u_2} (α : Type u_3) [inst : AddMonoid M] [inst_1 : AddAction M α] [inst_2 : AddMonoid N]
  (g : N →+ M), AddAction.compHom α g = { vadd := VAdd.comp.vadd ⇑g, add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.Analysis.Polynomial.MahlerMeasure
/-- **Landau's inequality**: the Mahler measure of a polynomial is at most the ℓ² norm
of its coefficient vector, `√(∑ ‖coeff i‖²)`.

This is the classical inequality due to Landau (1905). Combined with the multiplicativity of the
Mahler measure (`mahlerMeasure_mul`), it gives the Mignotte bound on coefficients of polynomial
factors.

TODO: restate using a dedicated polynomial ℓ² norm once one is defined (see the TODO in
`Mathlib.Analysis.Polynomial.Norm`).  -/
Polynomial.mahlerMeasure_le_sqrt_sum_sq_norm_coeff : ∀ (p : Polynomial ℂ), p.mahlerMeasure ≤ √(∑ i ∈ p.support, ‖p.coeff i‖ ^ 2)
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- `t.pt` maps to all other cocone covertices  -/
CategoryTheory.Limits.IsColimit.desc : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cocone F} →
            CategoryTheory.Limits.IsColimit t → (s : CategoryTheory.Limits.Cocone F) → t.pt ⟶ s.pt
-- Mathlib.Topology.Algebra.Group.Basic
isClosed_setOfPred_map_inv : ∀ (G₁ : Type u_2) (G₂ : Type u_3) [inst : TopologicalSpace G₂] [T2Space G₂] [inst_2 : Inv G₁] [inst_3 : Inv G₂]
  [ContinuousInv G₂], IsClosed {f | ∀ (x : G₁), f x⁻¹ = (f x)⁻¹}
-- Mathlib.Analysis.Asymptotics.LinearGrowth
/-- Lower linear growth of a sequence.  -/
LinearGrowth.linearGrowthInf : {R : Type u_1} → [ConditionallyCompleteLattice R] → [Div R] → [NatCast R] → (ℕ → R) → R
-- Std.Time.Internal.Bounded
Std.Time.Internal.Bounded.instLT : {rel : ℤ → ℤ → Prop} → {n m : ℤ} → LT (Std.Time.Internal.Bounded rel n m)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.singletonSubgraph_eq_induce : ∀ {V : Type u} {G : SimpleGraph V} {v : V}, G.singletonSubgraph v = ⊤.induce {v}
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
AddChar.zmod.congr_simp : ∀ (n : ℕ) [inst : NeZero n] (x x_1 : ZMod n), x = x_1 → AddChar.zmod n x = AddChar.zmod n x_1
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_updateCol_smul : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (M : Matrix n n R)
  (j : n) (s : R) (u : n → R), (M.updateCol j (s • u)).det = s * (M.updateCol j u).det
-- Mathlib.CategoryTheory.Functor.OfSequence
CategoryTheory.Functor.OfSequence.map_comp_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (i j k : ℕ)
  (hij : i ≤ j) (hjk : j ≤ k) {Z : C} (h : X k ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OfSequence.map f i k ⋯) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OfSequence.map f i j hij)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OfSequence.map f j k hjk) h)
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.LeftExactFunctor.whiskeringLeft_obj_map : ∀ (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 : C ⥤ₗ D) {X Y : D ⥤ₗ E} (f : X ⟶ Y),
  ((CategoryTheory.LeftExactFunctor.whiskeringLeft C D E).obj F).map f =
    CategoryTheory.ObjectProperty.homMk (F.obj.whiskerLeft f.hom)
-- Mathlib.Algebra.Quandle
ShelfHom.comp_apply : ∀ {S₁ : Type u_1} {S₂ : Type u_2} {S₃ : Type u_3} [inst : Shelf S₁] [inst_1 : Shelf S₂] [inst_2 : Shelf S₃]
  (g : ShelfHom S₂ S₃) (f : ShelfHom S₁ S₂) (x : S₁), (g.comp f) x = g (f x)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.prod_toFun : ∀ {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : Monoid C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] (f : A →ₜ* B) (g : A →ₜ* C)
  (i : A), (f.prod g) i = (f i, g i)
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
/-- The function `x ^ s * exp (-b * x)` tends to `0` at `+∞`, for any real `s` and `b > 0`.  -/
tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero : ∀ (s b : ℝ), 0 < b → Filter.Tendsto (fun x => x ^ s * Real.exp (-b * x)) Filter.atTop (nhds 0)
-- Lean.Data.JsonRpc
Lean.JsonRpc.RequestID.num : Lean.JsonNumber → Lean.JsonRpc.RequestID
-- Mathlib.RingTheory.Ideal.Maps
Submodule.mem_annihilator : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Submodule R M}
  {r : R}, r ∈ N.annihilator ↔ ∀ n ∈ N, r • n = 0
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- If the inner product of two unit vectors is `1`, then the two vectors are equal. One form of
the equality case for Cauchy-Schwarz.  -/
inner_eq_one_iff_of_norm_eq_one : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {x y : E}, ‖x‖ = 1 → ‖y‖ = 1 → (inner 𝕜 x y = 1 ↔ x = y)
-- Mathlib.Order.Filter.Cocardinal
/-- The filter defined by all sets that have countable complements.  -/
Filter.cocountable : {α : Type u} → Filter α
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasurableEmbedding.memLp_map_measure_iff : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {β : Type u_8} {mβ : MeasurableSpace β} {f : α → β}
  {g : β → ε},
  MeasurableEmbedding f → (MeasureTheory.MemLp g p (MeasureTheory.Measure.map f μ) ↔ MeasureTheory.MemLp (g ∘ f) p μ)
-- Mathlib.GroupTheory.OrderOfElement
powCoprime.eq_1 : ∀ {n : ℕ} {G : Type u_6} [inst : Group G] (h : (Nat.card G).Coprime n),
  powCoprime h = { toFun := fun g => g ^ n, invFun := fun g => g ^ (Nat.card G).gcdB n, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.firstDiff_comm : ∀ {E : ℕ → Type u_1} (x y : (n : ℕ) → E n), PiNat.firstDiff x y = PiNat.firstDiff y x
-- Mathlib.Data.Set.Basic
Set.Nonempty.eq_1 : ∀ {α : Type u} (s : Set α), s.Nonempty = ∃ x, x ∈ s
-- Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
PointwiseConvergenceCLM.instT2Space : ∀ {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_7}
  {F : Type u_8} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : IsTopologicalAddGroup F] [inst_7 : Module 𝕜₁ E] [inst_8 : Module 𝕜₂ F]
  [T2Space F], T2Space (E →SLₚₜ[σ] F)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.algHom_ext' : ∀ {S : Type u_1} {R : Type u} {M : Type v} [inst : CommSemiring S] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Algebra S R] [inst_4 : Module S M] [inst_5 : Module R M] [inst_6 : Module Rᵐᵒᵖ M]
  [inst_7 : SMulCommClass R Rᵐᵒᵖ M] [inst_8 : IsScalarTower S R M] [inst_9 : IsScalarTower S Rᵐᵒᵖ M] {A : Type u_2}
  [inst_10 : Semiring A] [inst_11 : Algebra S A] ⦃f g : TrivSqZeroExt R M →ₐ[S] A⦄,
  f.comp (TrivSqZeroExt.inlAlgHom S R M) = g.comp (TrivSqZeroExt.inlAlgHom S R M) →
    f.toLinearMap ∘ₗ ↑S (TrivSqZeroExt.inrHom R M) = g.toLinearMap ∘ₗ ↑S (TrivSqZeroExt.inrHom R M) → f = g
-- Mathlib.Control.Fold
Traversable.foldrm_map : ∀ {α β γ : Type u} {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] {m : Type u → Type u}
  [inst_2 : Monad m] [LawfulMonad m] (g : β → γ) (f : γ → α → m α) (a : α) (l : t β),
  Traversable.foldrm f a (g <$> l) = Traversable.foldrm (f ∘ g) a l
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.isCongruent.go : Lean.Meta.Grind.ENodeMap → Lean.Expr → Lean.Expr → Bool
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
Lean.Meta.Grind.Arith.Cutsat.getModThm? : Lean.Meta.Grind.Arith.Cutsat.ToIntM (Option Lean.Expr)
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.lift_apply_inl : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] [inst_2 : AddMonoid P]
  (f : M →+ P) (g : N →+ P) (x : M), (AddMonoid.Coprod.lift f g) (AddMonoid.Coprod.inl x) = f x
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.Colorable.chromaticNumber_pos : ∀ {V : Type u} {G : SimpleGraph V} [Nonempty V] {n : ℕ}, G.Colorable n → 0 < G.chromaticNumber
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.single_eq_C : ∀ {R : Type u_1} [inst : Semiring R] (r : R), AddMonoidAlgebra.single 0 r = LaurentPolynomial.C r
-- Mathlib.Combinatorics.Graph.Basic
Graph.IsNonloopAt.edge_mem : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β}, G.IsNonloopAt e x → e ∈ G.edgeSet
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.homogeneousComponent_eq_zero : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (n : ℕ) (φ : MvPolynomial σ R),
  φ.totalDegree < n → (MvPolynomial.homogeneousComponent n) φ = 0
-- Lean.Parser.Command
Lean.Parser.Command.print : Lean.Parser.Parser
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.comap_comap : ∀ {R : Type u} {S : Type v} {T : Type w} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  [inst_2 : NonUnitalNonAssocSemiring T] {F : Type u_1} {G : Type u_2} [inst_3 : FunLike F R S]
  [inst_4 : NonUnitalRingHomClass F R S] [inst_5 : FunLike G S T] [inst_6 : NonUnitalRingHomClass G S T]
  (s : NonUnitalSubsemiring T) (g : G) (f : F),
  NonUnitalSubsemiring.comap f (NonUnitalSubsemiring.comap g s) = NonUnitalSubsemiring.comap ((↑g).comp ↑f) s
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
/-- A version of `Equiv.optionCongr` for `WithZero` on `OrderMonoidIso`.  -/
OrderMonoidIso.withZero : {G : Type u_6} →
  {H : Type u_7} →
    [inst : Group G] →
      [inst_1 : PartialOrder G] →
        [inst_2 : Group H] → [inst_3 : PartialOrder H] → (G ≃*o H) ≃ (WithZero G ≃*o WithZero H)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.isoHomologyι_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) (hj : c.next i = j) (h : K.d i j = 0)
  [inst_2 : K.HasHomology i], (K.isoHomologyι i j hj h).hom = K.homologyι i
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.IsLocalizationMap.mk : ∀ {M : Type u_1} [inst : CommMonoid M] {N : Type u_2} [inst_1 : CommMonoid N] {S : Submonoid M} {f : M → N},
  (∀ (y : ↥S), IsUnit (f ↑y)) →
    (∀ (z : N), ∃ x, z * f ↑x.2 = f x.1) → (∀ {x y : M}, f x = f y → ∃ c, ↑c * x = ↑c * y) → S.IsLocalizationMap f
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.restrictTopIso_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C),
  X.restrictTopIso.inv = X.toRestrictTop
-- Init.Data.List.Lemmas
List.splitAt.go.eq_1 : ∀ {α : Type u} (l : List α) (a : ℕ) (a_1 : List α), List.splitAt.go l [] a a_1 = (l, [])
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.left_eq_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} {X Y : CategoryTheory.StructuredArrow S T} (f : X ⟶ Y),
  f.left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Computability.Language
Language.instOrderedSub : ∀ {α : Type u_1}, OrderedSub (Language α)
-- Lean.MetavarContext
/-- Assignment table for delayed abstraction metavariables.
For more information about delayed abstraction, see the docstring for `DelayedMetavarAssignment`.  -/
Lean.MetavarContext.dAssignment : Lean.MetavarContext → Lean.PersistentHashMap Lean.MVarId Lean.DelayedMetavarAssignment
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.symm_symm : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  (e : P₁ ≃ᴬ[k] P₂), e.symm.symm = e
-- Lean.Environment
Lean.instInhabitedEnvExtensionState : Inhabited Lean.EnvExtensionState
-- Mathlib.Topology.Sheaves.EtaleSpace
TopCat.Presheaf.EtaleSpace.exists_section_of_tendsto : ∀ {X : TopCat} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {CC : C → Type v} {FC : C → C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [inst_3 : CategoryTheory.Limits.HasColimits C] {F : TopCat.Presheaf C X}
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] {α : Type u_1} {l : Filter α}
  {g : α → F.EtaleSpace} {g₀ : F.EtaleSpace},
  Filter.Tendsto g l (nhds g₀) →
    ∃ U,
      g₀.base ∈ U ∧
        ∃ f,
          ∀ᶠ (a : α) in l,
            ∃ (ha : (g a).base ∈ U), (g a).germ = (CategoryTheory.ConcreteCategory.hom (F.germ U (g a).base ha)) f
-- Mathlib.Probability.Distributions.Poisson.Basic
ProbabilityTheory.hasSum_integral_poissonMeasure : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {r : NNReal} {f : ℕ → E},
  MeasureTheory.Integrable f (ProbabilityTheory.poissonMeasure r) →
    HasSum (fun n => (Real.exp (-↑r) * ↑r ^ n / ↑n.factorial) • f n)
      (∫ (n : ℕ), f n ∂ProbabilityTheory.poissonMeasure r)
-- Mathlib.Analysis.Analytic.Constructions
hasFPowerSeriesOnBall_inv_one_sub : ∀ (𝕜 : Type u_2) [inst : NontriviallyNormedField 𝕜] (𝕝 : Type u_8) [inst_1 : NormedDivisionRing 𝕝]
  [inst_2 : NormedAlgebra 𝕜 𝕝], HasFPowerSeriesOnBall (fun x => (1 - x)⁻¹) (formalMultilinearSeries_geometric 𝕜 𝕝) 0 1
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- If `A` has a constructive inverse, produce one for `A.det`.  -/
Matrix.detInvertibleOfInvertible : {n : Type u'} →
  {α : Type v} →
    [inst : Fintype n] →
      [inst_1 : DecidableEq n] → [inst_2 : CommRing α] → (A : Matrix n n α) → [Invertible A] → Invertible A.det