mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Order
FirstOrder.Language.instOrderedStructureSubtypeMemSubstructure : ∀ {L : FirstOrder.Language} {M : Type w'} [inst : L.IsOrdered] [inst_1 : L.Structure M] [inst_2 : LE M]
  [L.OrderedStructure M] (S : L.Substructure M), L.OrderedStructure ↥S
-- Mathlib.Order.SupClosed
subset_latticeClosure : ∀ {α : Type u_3} [inst : Lattice α] {s : Set α}, s ⊆ latticeClosure s
-- Init.Data.BitVec.BasicAux
BitVec.instSub : {n : ℕ} → Sub (BitVec n)
-- Mathlib.Combinatorics.Additive.Convolution
Finset.addConvolution_op_vadd_eq_addConvolution_add_neg : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] (A B : Finset G) (s x : G),
  A.addConvolution (AddOpposite.op s +ᵥ B) x = A.addConvolution B (x + -s)
-- Mathlib.Topology.Constructions
instNoncompactSpaceAdditive : ∀ {X : Type u} [inst : TopologicalSpace X] [NoncompactSpace X], NoncompactSpace (Additive X)
-- Mathlib.Combinatorics.Quiver.Schreier
Quiver.SchreierGraph.labellingStarEquiv_symm_apply_snd_coe : ∀ {V : Type u_1} {M : Type u_2} [inst : Group M] [inst_1 : MulAction M V] {S : Type u_3} (ι : S → M)
  (x : Quiver.SchreierGraph V ι) (x_1 : Quiver.Star (Quiver.SingleObj.star S)),
  ↑((Quiver.SchreierGraph.labellingStarEquiv ι x).symm x_1).snd = x_1.snd
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.instIsRegularEpiOppositeOpOfIsRegularMono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsRegularMono f],
  CategoryTheory.IsRegularEpi f.op
-- Init.Data.String.Pattern.String
String.Slice.Pattern.ForwardSliceSearcher.instForwardPattern_1 : {pat : String} → String.Slice.Pattern.ForwardPattern pat
-- Mathlib.RingTheory.RingHom.EssFiniteType
RingHom.EssFiniteType.comp : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  {f : R →+* S} {g : S →+* T}, f.EssFiniteType → g.EssFiniteType → (g.comp f).EssFiniteType
-- Mathlib.GroupTheory.Perm.List
List.support_formPerm_of_nodup : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (l : List α),
  l.Nodup → (∀ (x : α), l ≠ [x]) → l.formPerm.support = l.toFinset
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.le_refl : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] (a : α),
  Std.PRange.UpwardEnumerable.LE a a
-- Mathlib.Topology.Bases
/-- **Alias** of `TopologicalSpace.IsTopologicalBasis.sdiff_empty`. -/
TopologicalSpace.IsTopologicalBasis.diff_empty : ∀ {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)},
  TopologicalSpace.IsTopologicalBasis s → TopologicalSpace.IsTopologicalBasis (s \ {∅})
-- Mathlib.RingTheory.Polynomial.Content
/-- `p.content` is the `gcd` of the coefficients of `p`.  -/
Polynomial.content : {R : Type u_1} → [inst : CommRing R] → [NormalizedGCDMonoid R] → Polynomial R → R
-- Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
/-- Auxiliary definition for `ofCocone`.  -/
CategoryTheory.SmallObject.SuccStruct.ofCocone.map : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {J : Type u} →
      [inst_1 : LinearOrder J] →
        {j : J} →
          {F : CategoryTheory.Functor (↑(Set.Iio j)) C} →
            (c : CategoryTheory.Limits.Cocone F) →
              (i₁ i₂ : J) →
                i₁ ≤ i₂ →
                  i₂ ≤ j →
                    (CategoryTheory.SmallObject.SuccStruct.ofCocone.obj c i₁ ⟶
                      CategoryTheory.SmallObject.SuccStruct.ofCocone.obj c i₂)
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.mkSortS : {m : Type → Type} → [Lean.Meta.Sym.Internal.MonadShareCommon m] → Lean.Level → m Lean.Expr
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.Hom.hom.eq_1 : ∀ {X Y : AddGrpCat} (f : X.Hom Y), f.hom = CategoryTheory.ConcreteCategory.hom f
-- Mathlib.Topology.Covering.AddCircle
AddCircle.isLocalHomeomorph_coe : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜) [inst_1 : TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜]
  [DiscreteTopology ↥(AddSubgroup.zmultiples p)], IsLocalHomeomorph QuotientAddGroup.mk
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
_private.Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing.0.AlgebraicGeometry.PresheafedSpace.GlueData.«termπ₂⁻¹_,_,_» : Lean.ParserDescr
-- Mathlib.Data.Set.Basic
/-- **Alias** of `Set.ofPred_and`. -/
Set.setOf_and : ∀ {α : Type u} {p q : α → Prop}, {a | p a ∧ q a} = {a | p a} ∩ {a | q a}
-- Mathlib.Algebra.Module.Torsion.Free
smul_left_inj : ∀ {R : Type u_1} {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {m : M} {r₁ r₂ : R}
  [IsCancelMulZero R] [Module.IsTorsionFree R M], m ≠ 0 → (r₁ • m = r₂ • m ↔ r₁ = r₂)
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.coeff_add : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (x y : PolynomialModule R M), (x + y).coeff = x.coeff + y.coeff
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.keys_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w}
  {f : (a : α) → β a → γ a}, (Std.DTreeMap.map f t).keys = t.keys
-- Init.Data.Array.Lex.Lemmas
Array.append_left_le : ∀ {α : Type u_1} [inst : LT α] [Std.Asymm fun x1 x2 => x1 < x2] [Std.Trichotomous fun x1 x2 => x1 < x2]
  {xs ys zs : Array α}, ys ≤ zs → xs ++ ys ≤ xs ++ zs
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.expSeries_hasSum_exp_of_mem_ball : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕂] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸]
  [CompleteSpace 𝔸] [CharZero 𝕂],
  ∀ x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius,
    HasSum (fun n => (NormedSpace.expSeries 𝕂 𝔸 n) fun x_1 => x) (NormedSpace.exp x)
-- Mathlib.NumberTheory.Divisors
Nat.map_div_right_divisors : ∀ {n : ℕ}, Finset.map { toFun := fun d => (d, n / d), inj' := ⋯ } n.divisors = n.divisorsAntidiagonal
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.isTopologicalAddGroup : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E},
  IsTopologicalAddGroup (ContDiffMapSupportedIn E F n K)
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_eq_bot : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Set M},
  Submodule.span R s = ⊥ ↔ ∀ x ∈ s, x = 0
-- Mathlib.Topology.Category.TopCat.Basic
_private.Mathlib.Topology.Category.TopCat.Basic.0.TopCat.Hom.mk : {X Y : TopCat} → C(↑X, ↑Y) → X.Hom Y
-- Mathlib.Order.RelIso.Basic
RelHom.mk.injEq : ∀ {α : Type u_5} {β : Type u_6} {r : α → α → Prop} {s : β → β → Prop} (toFun : α → β)
  (map_rel' : ∀ {a b : α}, r a b → s (toFun a) (toFun b)) (toFun_1 : α → β)
  (map_rel'_1 : ∀ {a b : α}, r a b → s (toFun_1 a) (toFun_1 b)),
  ({ toFun := toFun, map_rel' := map_rel' } = { toFun := toFun_1, map_rel' := map_rel'_1 }) = (toFun = toFun_1)
-- Mathlib.CategoryTheory.Category.Factorisation
/-- Factorisations of a morphism `f` as a structure, containing, one object, two morphisms,
and the condition that their composition equals `f`.  -/
CategoryTheory.Factorisation : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (X ⟶ Y) → Type (max u v)
-- Mathlib.SetTheory.Ordinal.Notation
ONote.oadd_lt_oadd_2 : ∀ {e o₁ o₂ : ONote} {n₁ n₂ : ℕ+}, (e.oadd n₁ o₁).NF → ↑n₁ < ↑n₂ → e.oadd n₁ o₁ < e.oadd n₂ o₂
-- Mathlib.MeasureTheory.Function.AEEqOfLIntegral
MeasureTheory.withDensity_eq_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal},
  AEMeasurable f μ → AEMeasurable g μ → ∫⁻ (x : α), f x ∂μ ≠ ⊤ → (μ.withDensity f = μ.withDensity g ↔ f =ᵐ[μ] g)
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.relNorm_int : ∀ (S : Type u_3) [inst : CommRing S] [inst_1 : IsDomain S] [inst_2 : IsIntegrallyClosed S] [inst_3 : IsDedekindDomain S]
  [inst_4 : Module.Free ℤ S] [inst_5 : Module.Finite ℤ S] (I : Ideal S),
  (Ideal.relNorm ℤ) I = Ideal.span {↑(Ideal.absNorm I)}
-- Mathlib.GroupTheory.Perm.ConjAct
Equiv.Perm.cycleFactorsFinset_conj : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (g k : Equiv.Perm α),
  (ConjAct.toConjAct k • g).cycleFactorsFinset = Finset.map (MulAut.conj k).toEmbedding g.cycleFactorsFinset
-- Init.Data.Rat.Lemmas
Rat.le_add_iff_sub_le : ∀ {a b c : ℚ}, a ≤ b + c ↔ a - c ≤ b
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- We do not want `simps` automatically generate the lemma for simplifying the `Hom` field of
-- a category. So we need to write the `ext` lemma in terms of the categorical morphism, rather than
the underlying structure.  -/
CategoryTheory.Limits.BinaryBiconeMorphism.ext : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} {c c' : CategoryTheory.Limits.BinaryBicone P Q} (f g : c ⟶ c'), f.hom = g.hom → f = g
-- Mathlib.NumberTheory.Bernoulli
/-- The Bernoulli numbers are defined to be `bernoulli'` with a parity sign.  -/
bernoulli : ℕ → ℚ
-- Init.Data.String.Search
/-- Finds the position of the first match of the pattern `pattern` in after the position
`pos`. If there is no match `s.endPos` is returned.

This function is generic over all currently supported patterns.

Examples:

* `("coffee tea water".startPos.find Char.isWhitespace).get! == ' '`

* `("tea".pos ⟨1⟩ (by decide)).find (fun (c : Char) => c == 't') == "tea".endPos`
 -/
String.Pos.find : {ρ : Type} →
  {σ : String.Slice → Type} →
    [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] →
      [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] →
        {s : String} → s.Pos → (pattern : ρ) → [String.Slice.Pattern.ToForwardSearcher pattern σ] → s.Pos
-- Mathlib.Topology.Connected.Basic
instPreconnectedSpaceForall : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), PreconnectedSpace (X i)],
  PreconnectedSpace ((i : ι) → X i)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.size_insertManyIfNewUnit_list_le : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap α (fun x => Unit) cmp} [Std.TransCmp cmp] {l : List α},
  (Std.DTreeMap.Const.insertManyIfNewUnit t l).size ≤ t.size + l.length
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.Embedding.IsTruncLE.toIsRelIff : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {e : c.Embedding c'} [self : e.IsTruncLE],
  e.IsRelIff
-- Mathlib.Probability.Decision.Risk.Defs
ProbabilityTheory.minimaxRisk_of_isEmpty'' : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : ProbabilityTheory.Kernel Θ 𝓧} [Nonempty 𝓨] [IsEmpty Θ],
  ProbabilityTheory.minimaxRisk ℓ P = 0
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.nrRealPlaces.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.InfinitePlace.nrRealPlaces K = NumberField.InfinitePlace.nrRealPlaces K
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.upperCentralSeriesStep_eq_comap_center`.

---

The proof that `upperCentralSeriesStep N` is the preimage of the centre of `G/N` under
the canonical surjection.  -/
upperCentralSeriesStep_eq_comap_center : ∀ {G : Type u_1} [inst : Group G] (N : Subgroup G) [inst_1 : N.Normal],
  N.upperCentralSeriesStep = Subgroup.comap (QuotientGroup.mk' N) (Subgroup.center (G ⧸ N))
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitSphere.instCommMonoid : {𝕜 : Type u_1} → [inst : SeminormedCommRing 𝕜] → [NormMulClass 𝕜] → [NormOneClass 𝕜] → CommMonoid ↑(Metric.sphere 0 1)
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.instModuleCarrierStalkAbPresheafOpensCarrierTopModuleStructurePresheaf : {R M : Type u} →
  [inst : CommRing R] →
    [inst_1 : AddCommGroup M] →
      [inst_2 : Module R M] →
        (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) →
          Module R ↑(TopCat.Presheaf.stalk (AlgebraicGeometry.moduleStructurePresheaf R M).presheaf x)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β} {h : t.Balanced}
  {f : (a : α) → β a → Option (γ a)},
  (Std.DTreeMap.Internal.Impl.filterMap f t h).impl.toListModel =
    List.filterMap (fun x => Option.map (fun x_1 => ⟨x.fst, x_1⟩) (f x.fst x.snd)) t.toListModel
-- Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
alternatingGroup.kleinFour.eq_1 : ∀ (α : Type u_1) [inst : DecidableEq α] [inst_1 : Fintype α],
  alternatingGroup.kleinFour α = Subgroup.closure {g | (↑g).cycleType = {2, 2}}
-- Mathlib.LinearAlgebra.Multilinear.DFinsupp
MultilinearMap.dfinsuppFamily_apply_toFun : ∀ {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN}
  [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : Semiring R]
  [inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)] [inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)]
  [inst_5 : (i : ι) → (k : κ i) → Module R (M i k)] [inst_6 : (p : (i : ι) → κ i) → Module R (N p)]
  (f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)) (x : (i : ι) → Π₀ (j : κ i), M i j)
  (p : (i : ι) → κ i), ((MultilinearMap.dfinsuppFamily f) x) p = (f p) fun i => (x i) (p i)
-- Mathlib.Algebra.Lie.OfAssociative
LieModule.IsFaithful.mk : ∀ {R : Type u} {L : Type v} {M : Type w} [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],
  Function.Injective ⇑(LieModule.toEnd R L M) → LieModule.IsFaithful R L M
-- Lean.Meta.Tactic.Grind.MatchCond
_private.Lean.Meta.Tactic.Grind.MatchCond.0.Lean.Meta.Grind.isMatchCondFalseHyp.isFalse : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Bool
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.codExtend'_source : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace Z] {s : Set B} (hs : IsOpen s) {proj : Z → ↑s} (e : Bundle.Trivialization F proj)
  [inst_3 : Nonempty (B → F → Z)], (Bundle.Trivialization.codExtend' hs e).source = e.toPretrivialization.source
-- Init.Data.Array.Find
Array.findIdx_getElem?_eq_getElem_of_exists : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α} (h : ∃ x ∈ xs, p x = true),
  xs[Array.findIdx p xs]? = some xs[Array.findIdx p xs]
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.map_app_comp_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  [inst_4 : CategoryTheory.MonoidalClosed V] {F G H : CategoryTheory.Functor C V}
  (ℌ : CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F G H) {G' H' : CategoryTheory.Functor C V}
  (f : G ⟶ G') (ℌ' : CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F G' H') (c j : C),
  CategoryTheory.CategoryStruct.comp ((ℌ.map f ℌ').app c) (ℌ'.π c j) =
    CategoryTheory.CategoryStruct.comp (ℌ.π c j)
      ((CategoryTheory.ihom (F.obj j)).map (f.app (CategoryTheory.MonoidalCategoryStruct.tensorObj j c)))
-- Mathlib.Tactic.Translate.Core
/-- Linter used by translate attributes that checks if the given reorder is
equal to the automatically generated name  -/
Mathlib.Tactic.Translate.linter.translateReorder : Lean.Option Bool
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.sInf_eq_zero_iff : ∀ {s : Set Cardinal.{u_1}}, sInf s = 0 ↔ s = ∅ ∨ ∃ a ∈ s, a = 0
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
/-- The best proof would probably to establish the bijection with Finpartitions, but we opt
for a direct argument, embedding `OrderedPartition n` in a type which is obviously finite.  -/
OrderedFinpartition.instFintype : {n : ℕ} → Fintype (OrderedFinpartition n)
-- Mathlib.Topology.UniformSpace.Basic
MulOpposite.uniformContinuous_op : ∀ {α : Type ua} [inst : UniformSpace α], UniformContinuous MulOpposite.op
-- Mathlib.Data.Finset.Max
Finset.map_ofDual_min : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset αᵒᵈ),
  WithTop.map (⇑OrderDual.ofDual) s.min = (Finset.image (⇑OrderDual.ofDual) s).max
-- Std.Http.Data.Status
/-- 301 Moved Permanently
 -/
Std.Http.Status.movedPermanently : Std.Http.Status
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
_private.Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf.0.CategoryTheory.Precoverage.SmallConstruction.Witness.restrict.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C} {ι : C → Type w} {X Y : C}
  (f : X ⟶ Y) (a : CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι Y) (Y_1 : C) (f_1 : X ⟶ Y_1)
  (a_1 : CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι Y_1),
  (CategoryTheory.Precoverage.SmallConstruction.Witness.restrict✝ f a =
      CategoryTheory.Precoverage.SmallConstruction.Witness.restrict✝ f_1 a_1) =
    (Y = Y_1 ∧ f ≍ f_1 ∧ a ≍ a_1)
-- Mathlib.Algebra.Lie.Ideal
LieHom.le_ker_iff : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] (f : L →ₗ⁅R⁆ L') (I : LieIdeal R L), I ≤ f.ker ↔ ∀ x ∈ I, f x = 0
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.toLinearMapₛₗ₂_symm : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {N₂ : Type u_10} {n : Type u_11} {m : Type u_12}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂]
  [inst_4 : Module R M₂] [inst_5 : AddCommMonoid N₂] [inst_6 : Module R N₂] {σ₁ : R →+* R} [inst_7 : Fintype n]
  [inst_8 : Fintype m] [inst_9 : DecidableEq m] [inst_10 : DecidableEq n] (b₁ : Module.Basis n R M₁)
  (b₂ : Module.Basis m R M₂), (Matrix.toLinearMapₛₗ₂ σ₁ b₁ b₂).symm = LinearMap.toMatrix₂ b₁ b₂
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_inter_eq_size_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α], (∀ a ∈ m₁, a ∈ m₂) → (m₁ ∩ m₂).size = m₁.size
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.instHasColimitsOfShape : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {J : Type v} [inst_1 : CategoryTheory.SmallCategory J]
  [CategoryTheory.Limits.HasColimitsOfShape J C],
  CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.SimplicialObject C)
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.monomial.eq_1 : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (n : σ →₀ ℕ),
  MvPowerSeries.monomial n = LinearMap.single R (fun x => R) n
-- Mathlib.Dynamics.Flow
Flow.reverse_apply : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α]
  [inst_2 : SubtractionCommMonoid τ] [inst_3 : ContinuousNeg τ] (ϕ : Flow τ α) (t : τ) (x : α),
  ϕ.reverse.toFun t x = ϕ.toFun (-t) x
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntTermInfo.mk.injEq : ∀ (eToInt α he eToInt_1 α_1 he_1 : Lean.Expr),
  ({ eToInt := eToInt, α := α, he := he } = { eToInt := eToInt_1, α := α_1, he := he_1 }) =
    (eToInt = eToInt_1 ∧ α = α_1 ∧ he = he_1)
-- Mathlib.Data.PFunctor.Univariate.M
/-- corecursor where the state of the computation can be sent downstream
in the form of a recursive call  -/
PFunctor.M.corec₁ : {P : PFunctor.{uA, uB}} → {α : Type u} → ((X : Type u) → (α → X) → α → ↑P X) → α → P.M
-- Lean.Meta.KExprMap
Lean.Meta.instInhabitedKExprMap.default : {α : Type} → Lean.Meta.KExprMap α
-- Mathlib.Algebra.Group.Defs
/-- A monoid in which multiplication is left-cancellative.  -/
LeftCancelMonoid : Type u → Type u
-- Mathlib.Analysis.InnerProductSpace.Calculus
HasStrictFDerivAt.inner : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : NormedSpace ℝ E] {G : Type u_4} [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G] {f g : G → E}
  {f' g' : G →L[ℝ] E} {x : G},
  HasStrictFDerivAt f f' x →
    HasStrictFDerivAt g g' x →
      HasStrictFDerivAt (fun t => inner 𝕜 (f t) (g t)) (fderivInnerCLM 𝕜 (f x, g x) ∘SL f'.prod g') x
-- Lean.Meta.Tactic.Simp.Arith.Int.Simp
Lean.Meta.Simp.Arith.Int.simpEq? : Lean.Expr → Lean.MetaM (Option (Lean.Expr × Lean.Expr))
-- Mathlib.Algebra.Group.Basic
natCast_sub_one_zsmul : ∀ {G : Type u_3} [inst : AddGroup G] (a : G) (n : ℕ), (↑n - 1) • a = n • a - a
-- Mathlib.RingTheory.MvPowerSeries.Order
/-- The order of the monomial `a*X^n` is `n` if `a ≠ 0`.  -/
MvPowerSeries.order_monomial_of_ne_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {d : σ →₀ ℕ} {a : R},
  a ≠ 0 → ((MvPowerSeries.monomial d) a).order = ↑(Finsupp.degree d)
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.evalCompEqToEquivalenceFunctor_hom : ∀ {I : Type w₀} (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {i j : I} (h : i = j),
  (CategoryTheory.Pi.evalCompEqToEquivalenceFunctor C h).hom = CategoryTheory.eqToHom ⋯
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.support_binomial_subset : ∀ {R : Type u} [inst : Semiring R] (k m : ℕ) (x y : R),
  (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m).support ⊆ {k, m}
-- Mathlib.Analysis.Fourier.AddCircle
fourier_eval_zero : ∀ {T : ℝ} (n : ℤ), (fourier n) 0 = 1
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.balanced_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β} {h : t.Balanced}
  {f : (a : α) → β a → Option (γ a)}, (Std.DTreeMap.Internal.Impl.filterMap f t h).impl.Balanced
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.diag2_coe : ∀ {F : Type u_1} [inst : Field F] (a : F) (ha : a ≠ 0),
  ↑(Matrix.SpecialLinearGroup.diag2 a ha) =
    Matrix.diagonal fun i =>
      match i with
      | 0 => a
      | 1 => a⁻¹
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.IsInduced.top : ∀ {V : Type u} {G : SimpleGraph V}, ⊤.IsInduced
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ D` preserves limits, then `F.rightOp : C ⥤ Dᵒᵖ` preserves colimits.  -/
CategoryTheory.Limits.preservesColimits_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesLimits F],
  CategoryTheory.Limits.PreservesColimits F.rightOp
-- Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Nat.nthRoot_one_right : ∀ {n : ℕ}, n.nthRoot 1 = 1
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRange_eq_top_of_injective : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover)
  (𝒱 : (i : 𝒰.I₀) → (CategoryTheory.Limits.pullback f (𝒰.f i)).OpenCover),
  Function.Injective ⇑f → AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRange f 𝒰 𝒱 = ⊤
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.ForgetEnrichment.homOf_homTo : ∀ {C : Type u₁} (W : Type v) [inst : CategoryTheory.Category.{w, v} W] [inst_1 : CategoryTheory.MonoidalCategory W]
  [inst_2 : CategoryTheory.EnrichedCategory W C] {X Y : CategoryTheory.ForgetEnrichment W C} (f : X ⟶ Y),
  CategoryTheory.ForgetEnrichment.homOf W (CategoryTheory.ForgetEnrichment.homTo W f) = f
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasDerivAtFilter.comp_hasFDerivAtFilter : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type w} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕜' : Type u_1} [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  {h₂ : 𝕜' → 𝕜'} {h₂' : 𝕜'} {L' : Filter (𝕜' × 𝕜')} {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} {L'' : Filter (E × E)},
  HasDerivAtFilter h₂ h₂' L' →
    HasFDerivAtFilter f f' L'' → Filter.Tendsto (Prod.map f f) L'' L' → HasFDerivAtFilter (h₂ ∘ f) (h₂' • f') L''