mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.flip_apply : ∀ {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {S₂ : Type u_4} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : Semiring S] [inst_3 : Semiring S₂] {M : Type u_5} {N : Type u_7} {P : Type u_9} [inst_4 : AddCommMonoid M]
  [inst_5 : AddCommMonoid N] [inst_6 : AddCommMonoid P] [inst_7 : Module R M] [inst_8 : Module S N]
  [inst_9 : Module R₂ P] [inst_10 : Module S₂ P] [inst_11 : SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂}
  (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (m : M) (n : N), (f.flip n) m = (f m) n
-- Mathlib.SetTheory.Ordinal.Notation
NONote.instInhabited : Inhabited NONote
-- Mathlib.Data.Nat.Digits.Defs
/-- Any number m is less than b^(number of digits in the base b representation of m)  -/
Nat.lt_base_pow_length_digits : ∀ {b m : ℕ}, 1 < b → m < b ^ (b.digits m).length
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.instInhabited : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → Inhabited (CategoryTheory.Comon C)
-- Mathlib.Algebra.Group.Finsupp
Finsupp.embDomain_add : ∀ {ι : Type u_1} {F : Type u_2} {M : Type u_3} [inst : AddZeroClass M] (f : ι ↪ F) (v w : ι →₀ M),
  Finsupp.embDomain f (v + w) = Finsupp.embDomain f v + Finsupp.embDomain f w
-- Mathlib.Order.Basic
LE.le.lt_or_ge : ∀ {α : Type u_2} [inst : LinearOrder α] {a b : α}, b ≤ a → ∀ (c : α), c < a ∨ b ≤ c
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.Definable₁.out_equiv : ∀ (f : ZFSet.{u} → ZFSet.{u}) [inst : ZFSet.Definable₁ f] {x y : PSet.{u}},
  x ≈ y → ZFSet.Definable₁.out f x ≈ ZFSet.Definable₁.out f y
-- Mathlib.Analysis.Analytic.Constructions
AnalyticWithinAt.sub : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F} {s : Set E}
  {x : E}, AnalyticWithinAt 𝕜 f s x → AnalyticWithinAt 𝕜 g s x → AnalyticWithinAt 𝕜 (f - g) s x
-- Mathlib.Topology.Algebra.Equicontinuity
uniformEquicontinuous_of_equicontinuousAt_zero : ∀ {ι : Type u_1} {G : Type u_2} {M : Type u_3} {hom : Type u_4} [inst : UniformSpace G] [inst_1 : UniformSpace M]
  [inst_2 : AddGroup G] [inst_3 : AddGroup M] [IsUniformAddGroup G] [IsUniformAddGroup M] [inst_6 : FunLike hom G M]
  [AddMonoidHomClass hom G M] (F : ι → hom),
  EquicontinuousAt (DFunLike.coe ∘ F) 0 → UniformEquicontinuous (DFunLike.coe ∘ F)
-- Lean.Declaration
Lean.Declaration.forExprM : {m : Type → Type} → [Monad m] → Lean.Declaration → (Lean.Expr → m Unit) → m Unit
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.smul_tmul_smul : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (r s : R) (m : M) (n : N),
  (r • m) ⊗ₜ[R] (s • n) = (r * s) • m ⊗ₜ[R] n
-- Mathlib.Data.PNat.Basic
instCommMonoidPNat : CommMonoid ℕ+
-- Init.Data.Sum.Lemmas
Sum.liftRel_subrelation_lex : ∀ {α : Type u_1} {r : α → α → Prop} {β : Type u_2} {s : β → β → Prop}, Subrelation (Sum.LiftRel r s) (Sum.Lex r s)
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.separatingRight_iff_det_ne_zero : ∀ {R : Type u_1} {M₁ : Type u_6} {m : Type u_12} [inst : CommRing R] [inst_1 : DecidableEq m] [inst_2 : Fintype m]
  [IsDomain R] [inst_4 : AddCommMonoid M₁] [inst_5 : Module R M₁] (b : Module.Basis m R M₁) {B : M₁ →ₗ[R] M₁ →ₗ[R] R},
  B.SeparatingRight ↔ ((LinearMap.toMatrix₂ b b) B).det ≠ 0
-- Init.Data.UInt.Lemmas
UInt32.toUInt16_add : ∀ (a b : UInt32), (a + b).toUInt16 = a.toUInt16 + b.toUInt16
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
/-- If `f` is a closed immersion with affine target such that the induced map on global
sections is injective, `f` is an isomorphism.  -/
AlgebraicGeometry.IsClosedImmersion.isIso_of_injective_of_isAffine : ∀ {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Y] {f : X ⟶ Y} [AlgebraicGeometry.IsClosedImmersion f],
  Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop f)) →
    CategoryTheory.IsIso f
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.modifyTR_go_eq : ∀ {α : Type u_1} {f : α → α} {acc : Array α} (l : List α) (i : ℕ),
  List.modifyTR.go✝ f l i acc = acc.toList ++ l.modify i f
-- Mathlib.Data.WSeq.Basic
_private.Mathlib.Data.WSeq.Basic.0.Computation.Corec.f.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : α ⊕ β → Sort u_3) (a : α) (h_1 : (a : α) → motive (Sum.inl a))
  (h_2 : (val : β) → motive (Sum.inr val)),
  (match Sum.inl a with
    | Sum.inl a => h_1 a
    | Sum.inr val => h_2 val) =
    h_1 a
-- Mathlib.RingTheory.Localization.Submodule
IsFractionRing.coeSubmodule_injective : ∀ (R : Type u_3) (K : Type u_4) [inst : CommRing R] [inst_1 : CommRing K] [inst_2 : Algebra R K] [IsFractionRing R K],
  Function.Injective (IsLocalization.coeSubmodule K)
-- Init.Data.Array.Find
Array.back?_filterMap : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : Array α},
  (Array.filterMap f xs).back? = Array.findSomeRev? f xs
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.reverse_neg : ∀ {R : Type u_1} [inst : Ring R] (f : Polynomial R), (-f).reverse = -f.reverse
-- Lean.Modifiers
Lean.addProtected : Lean.Environment → Lean.Name → Lean.Environment
-- Mathlib.Tactic.Simps.Basic
Simps.instInhabitedProjectionData.default : Simps.ProjectionData
-- Mathlib.Data.Set.Order
Monotone.inter : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f g : β → Set α},
  Monotone f → Monotone g → Monotone fun x => f x ∩ g x
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.map_add₂ : ∀ {R : Type u_1} {𝕜₂ : Type u_3} {𝕜₃ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [inst : Semiring R]
  [inst_1 : NormedField 𝕜₂] [inst_2 : NormedField 𝕜₃] [inst_3 : AddCommMonoid E] [inst_4 : Module R E]
  [inst_5 : TopologicalSpace E] [inst_6 : AddCommGroup F] [inst_7 : Module 𝕜₂ F] [inst_8 : TopologicalSpace F]
  [inst_9 : AddCommGroup G] [inst_10 : Module 𝕜₃ G] [inst_11 : TopologicalSpace G] [inst_12 : IsTopologicalAddGroup G]
  [inst_13 : ContinuousConstSMul 𝕜₃ G] {σ₁₃ : R →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃} (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (x x' : E)
  (y : F), (f (x + x')) y = (f x) y + (f x') y
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.orderIsoOfIso_symm_apply : ∀ {α β : PartOrdEmb} (e : α ≅ β) (a : ↑β),
  (RelIso.symm (PartOrdEmb.orderIsoOfIso e)) a = (CategoryTheory.ConcreteCategory.hom e.inv) a
-- Mathlib.Algebra.Algebra.Equiv
/-- **Alias** of `AlgEquiv.coe_toAlgHom`. -/
AlgEquiv.coe_algHom : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂), ⇑↑e = ⇑e
-- Aesop.Forward.Substitution
/-- A substitution for the premises of a rule. Given a rule with type
`∀ (x₁ : T₁) ... (xₙ : Tₙ), U` a substitution is a finite partial map with
domain `{1, ..., n}` that associates an expression with some or all of the
premises.  -/
Aesop.Substitution : Type
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.hasFiniteCoproducts_of_opposite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasFiniteProducts Cᵒᵖ],
  CategoryTheory.Limits.HasFiniteCoproducts C
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.reverseAux.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (r : List α) (h_1 : (r : List α) → motive [] r)
  (h_2 : (a : α) → (l r : List α) → motive (a :: l) r),
  (match [], r with
    | [], r => h_1 r
    | a :: l, r => h_2 a l r) =
    h_1 r
-- Mathlib.CategoryTheory.LiftingProperties.Basic
CategoryTheory.RetractArrow.leftLiftingProperty : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {B A Z W B' A' : C} {f : A ⟶ B} {f' : A' ⟶ B'}
  (h : CategoryTheory.RetractArrow f' f) (g : W ⟶ Z) [CategoryTheory.HasLiftingProperty f g],
  CategoryTheory.HasLiftingProperty f' g
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
SSet.Subcomplex.Pairing.RankFunction.mk.congr_simp : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {α : Type v} [inst : PartialOrder α] (rank rank_1 : ↑P.II → α)
  (e_rank : rank = rank_1) (lt : ∀ {x y : ↑P.II}, P.AncestralRel x y → rank x < rank y),
  { rank := rank, lt := lt } = { rank := rank_1, lt := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.inr_isoPushout_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P} (h : CategoryTheory.IsPushout f g inl inr) [inst_1 : CategoryTheory.Limits.HasPushout f g] {Z_1 : C}
  (h_1 : CategoryTheory.Limits.pushout f g ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp inr (CategoryTheory.CategoryStruct.comp h.isoPushout.hom h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g) h_1
-- Mathlib.MeasureTheory.Constructions.Cylinders
/-- **Alias** of `MeasureTheory.sdiff_mem_measurableCylinders`. -/
MeasureTheory.diff_mem_measurableCylinders : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (α i)] {s t : Set ((i : ι) → α i)},
  s ∈ MeasureTheory.measurableCylinders α →
    t ∈ MeasureTheory.measurableCylinders α → s \ t ∈ MeasureTheory.measurableCylinders α
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
_private.Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis.0.Tactic.ComputeAsymptotics.BasisExtension.getBasis.match_1.eq_3 : ∀ (motive : (basis : Tactic.ComputeAsymptotics.Basis) → Tactic.ComputeAsymptotics.BasisExtension basis → Sort u_1)
  (basis : Tactic.ComputeAsymptotics.Basis) (f : ℝ → ℝ) (ex : Tactic.ComputeAsymptotics.BasisExtension basis)
  (h_1 : Unit → motive [] Tactic.ComputeAsymptotics.BasisExtension.nil)
  (h_2 :
    (basis_hd : ℝ → ℝ) →
      (basis_tl : Tactic.ComputeAsymptotics.Basis) →
        (ex : Tactic.ComputeAsymptotics.BasisExtension basis_tl) →
          motive (basis_hd :: basis_tl) (Tactic.ComputeAsymptotics.BasisExtension.keep basis_hd ex))
  (h_3 :
    (basis : Tactic.ComputeAsymptotics.Basis) →
      (f : ℝ → ℝ) →
        (ex : Tactic.ComputeAsymptotics.BasisExtension basis) →
          motive basis (Tactic.ComputeAsymptotics.BasisExtension.insert f ex)),
  (match basis, Tactic.ComputeAsymptotics.BasisExtension.insert f ex with
    | .([]), Tactic.ComputeAsymptotics.BasisExtension.nil => h_1 ()
    | .(basis_hd :: basis_tl), Tactic.ComputeAsymptotics.BasisExtension.keep basis_hd ex => h_2 basis_hd basis_tl ex
    | basis, Tactic.ComputeAsymptotics.BasisExtension.insert f ex => h_3 basis f ex) =
    h_3 basis f ex
-- Mathlib.Data.PFunctor.Multivariate.Basic
MvPFunctor.const.mk_get : ∀ {n : ℕ} {A : Type u} {α : TypeVec.{u} n} (x : ↑(MvPFunctor.const n A) α),
  MvPFunctor.const.mk n (MvPFunctor.const.get x) = x
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.getKey.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a a_1 : α) (e_a : a = a_1) (l l_1 : Std.DHashMap.Internal.AssocList α β)
  (e_l : l = l_1) (a_2 : Std.DHashMap.Internal.AssocList.contains a l = true),
  Std.DHashMap.Internal.AssocList.getKey a l a_2 = Std.DHashMap.Internal.AssocList.getKey a_1 l_1 ⋯
-- Mathlib.AlgebraicTopology.SimplicialObject.Op
SimplicialObject.opObjIso.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] {X : CategoryTheory.SimplicialObject C}
  {n : SimplexCategoryᵒᵖ},
  SimplicialObject.opObjIso = CategoryTheory.Iso.refl ((SimplicialObject.opFunctor.obj X).obj n)
-- Mathlib.Dynamics.Transitive
AddAction.IsTopologicallyTransitive.exists_vadd_inter : ∀ {M : Type u_1} {α : Type u_2} {inst : AddMonoid M} {inst_1 : TopologicalSpace α} {inst_2 : AddAction M α}
  [self : AddAction.IsTopologicallyTransitive M α] {U V : Set α},
  IsOpen U → U.Nonempty → IsOpen V → V.Nonempty → ∃ m, ((m +ᵥ U) ∩ V).Nonempty
-- Mathlib.CategoryTheory.Action.Continuous
/-- For `HasForget₂ V TopCat`, this is the full subcategory of `Action V G` where the induced
action is continuous.  -/
ContAction : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {FV : V → V → Type u_2} →
      {CV : V → Type u_3} →
        [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory V FV] →
            [CategoryTheory.HasForget₂ V TopCat] →
              (G : Type u_4) → [Monoid G] → [TopologicalSpace G] → Type (max (max u_1 u_4) v_1)
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.liftWith_ReaderT : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ρ α : Type u}
  {epost : EPred} (f : ({β : Type u} → ReaderT ρ m β → m β) → m α) (post : α → ρ → Pred),
  ⦃ fun r => Std.Internal.Do.wp (f fun {β} x => x.run r) (fun a => post a r) epost ⦄ MonadControl.liftWith f ⦃ post;
    epost ⦄
-- Mathlib.Algebra.Algebra.Operations
Submodule.span.ringHom_apply : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] (s : SetSemiring A),
  Submodule.span.ringHom s = Submodule.span R (SetSemiring.down s)
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_empty : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Submodule.span R ∅ = ⊥
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.instCategory.eq_1 : MagmaCat.instCategory =
  { Hom := fun X Y => X.Hom Y, id := fun X => { hom' := MulHom.id ↑X },
    comp := fun {X Y Z} f g => { hom' := g.hom'.comp f.hom' }, id_comp := @MagmaCat.instCategory._proof_1,
    comp_id := @MagmaCat.instCategory._proof_2, assoc := @MagmaCat.instCategory._proof_3 }
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.center_zero : ∀ (z : UpperHalfPlane), z.center 0 = z
-- Init.Data.Vector.Basic
/-- The last element of a non-empty vector.  -/
Vector.back : {n : ℕ} → {α : Type u_1} → [NeZero n] → Vector α n → α
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.arrowArrowEquivalence_unitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Square.arrowArrowEquivalence.unitIso =
    CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Square C))
-- Mathlib.Order.Preorder.Finsupp
Finsupp.preorder : {ι : Type u_1} → {M : Type u_2} → [inst : Zero M] → [Preorder M] → Preorder (ι →₀ M)
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.instMin : {α : Type u_1} → [inst : LE α] → Min (UpperSet α)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.comp_eq_sum_left : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p.comp q = p.sum fun e a => Polynomial.C a * q ^ e
-- Mathlib.Data.Int.ModEq
Int.modEq_add_fac_self : ∀ {a t n : ℤ}, a + n * t ≡ a [ZMOD n]
-- Mathlib.Order.Atoms
isAtomic_of_orderBot_wellFounded_lt : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderBot α], (WellFounded fun x1 x2 => x1 < x2) → IsAtomic α
-- Mathlib.Data.Rat.Cast.Defs
Rat.cast_commute : ∀ {α : Type u_3} [inst : DivisionRing α] (r : ℚ) (a : α), Commute (↑r) a
-- Mathlib.LinearAlgebra.Projectivization.Subspace
/-- If a set of points in projective space is contained in a subspace, and that subspace is
contained in the span of the set of points, then the span of the set of points is equal to
the subspace.  -/
Projectivization.Subspace.span_eq_of_le : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {S : Set (Projectivization K V)} {W : Projectivization.Subspace K V},
  S ⊆ ↑W → W ≤ Projectivization.Subspace.span S → Projectivization.Subspace.span S = W
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
Submonoid.inclusion.congr_simp : ∀ {M : Type u_1} [inst : MulOneClass M] {S T : Submonoid M} (h : S ≤ T), Submonoid.inclusion h = Submonoid.inclusion h
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.isoClosure_eq_self : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) [P.RespectsIso],
  P.isoClosure = P
-- Mathlib.CategoryTheory.Abelian.FreydMitchell
/-- The Freyd-Mitchell embedding theorem. See also `FreydMitchell.functor` for a functor which
has the relevant instances.  -/
CategoryTheory.Abelian.freyd_mitchell : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C],
  ∃ R x F,
    F.Full ∧
      F.Faithful ∧ CategoryTheory.Limits.PreservesFiniteLimits F ∧ CategoryTheory.Limits.PreservesFiniteColimits F
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.Config.mk.inj : ∀ {maxTransitionDepth maxSteps maxTransitionDepth_1 maxSteps_1 : ℕ},
  { maxTransitionDepth := maxTransitionDepth, maxSteps := maxSteps } =
      { maxTransitionDepth := maxTransitionDepth_1, maxSteps := maxSteps_1 } →
    maxTransitionDepth = maxTransitionDepth_1 ∧ maxSteps = maxSteps_1
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isSome_getKey?_eq_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {a : α},
  (t.getKey? a).isSome = t.contains a
-- Mathlib.CategoryTheory.Preadditive.Yoneda.Injective
CategoryTheory.Injective.injective_iff_preservesEpimorphisms_preadditive_yoneda_obj' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (J : C),
  CategoryTheory.Injective J ↔ (CategoryTheory.preadditiveYonedaObj J).PreservesEpimorphisms
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.sub_hom : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {A B : Rep.{w, u, v} k G} (f g : A ⟶ B),
  Rep.Hom.hom (f - g) = Rep.Hom.hom f - Rep.Hom.hom g
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
/-- The congruence subgroup `Gamma1` (as a subgroup of `Gamma0`) of matrices whose bottom
row is congruent to `(0, 1)` modulo `N`.  -/
CongruenceSubgroup.Gamma1' : (N : ℕ) → Subgroup ↥(CongruenceSubgroup.Gamma0 N)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.map.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {K : CategoryTheory.Precoverage D} (F : CategoryTheory.Functor C D)
  (E E_1 : J.ZeroHypercover S),
  E = E_1 →
    ∀ (h : J ≤ CategoryTheory.Precoverage.comap F K),
      CategoryTheory.Precoverage.ZeroHypercover.map F E h = CategoryTheory.Precoverage.ZeroHypercover.map F E_1 h
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.changeLevel_toUnitHom : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) {m : ℕ} (hm : n ∣ m),
  MulChar.toUnitHom ((DirichletCharacter.changeLevel hm) χ) = (MulChar.toUnitHom χ).comp (ZMod.unitsMap hm)
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.IntegrableOn.continuousOn_smul_of_subset : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] {A K : Set X} {𝕜 : Type u_9} [inst_4 : NormedRing 𝕜]
  [inst_5 : Module 𝕜 E] [IsBoundedSMul 𝕜 E] [SecondCountableTopologyEither X 𝕜] {f : X → 𝕜},
  ContinuousOn f K →
    ∀ {g : X → E},
      MeasureTheory.IntegrableOn g A μ →
        IsCompact K → MeasurableSet A → A ⊆ K → MeasureTheory.IntegrableOn (fun x => f x • g x) A μ
-- Mathlib.RingTheory.Algebraic.Defs
IsAlgebraic.eq_1 : ∀ (R : Type u) {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] (x : A),
  IsAlgebraic R x = ∃ p, p ≠ 0 ∧ (Polynomial.aeval x) p = 0
-- Mathlib.Algebra.Torsor.Defs
/-- If the same point added to two group elements produces equal
results, those group elements are equal.  -/
vadd_right_cancel : ∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] {g₁ g₂ : G} (p : P), g₁ +ᵥ p = g₂ +ᵥ p → g₁ = g₂
-- Lean.Environment
Lean.Kernel.Exception.funExpected.sizeOf_spec : ∀ (env : Lean.Kernel.Environment) (lctx : Lean.LocalContext) (expr : Lean.Expr),
  sizeOf (Lean.Kernel.Exception.funExpected env lctx expr) = 1 + sizeOf env + sizeOf lctx + sizeOf expr
-- Mathlib.RingTheory.WittVector.MulP
/-- `wittMulN p n` is the family of polynomials that computes
the coefficients of `x * n` in terms of the coefficients of the Witt vector `x`.  -/
WittVector.wittMulN : (p : ℕ) → [hp : Fact (Nat.Prime p)] → ℕ → ℕ → MvPolynomial ℕ ℤ
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
/-- The canonical morphism from `X` to the spectrum of its global sections.  -/
AlgebraicGeometry.LocallyRingedSpace.toΓSpec : (X : AlgebraicGeometry.LocallyRingedSpace) →
  X ⟶ AlgebraicGeometry.Spec.locallyRingedSpaceObj (AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))
-- Mathlib.Algebra.Group.Subsemigroup.Basic
AddSubsemigroup.mem_closure_of_mem : ∀ {M : Type u_1} [inst : Add M] {s : Set M} {x : M}, x ∈ s → x ∈ AddSubsemigroup.closure s
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.rpow_one : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] (a : A), autoParam (0 ≤ a) CFC.rpow_one._auto_1 → a ^ 1 = a
-- Lean.Meta.Tactic.Grind.Core
/-- Adds a new equality `lhs = rhs`. It assumes `lhs` and `rhs` have already been internalized.  -/
_private.Lean.Meta.Tactic.Grind.Core.0.Lean.Meta.Grind.addEq : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.symm_apply_eq : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂) {x : E₂} {y : E}, e.symm x = y ↔ x = e y
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
/-- If a set has zero measure in a neighborhood of each of its points, then it has zero measure
in a second-countable space.  -/
MeasureTheory.exists_ne_forall_mem_nhds_pos_measure_preimage : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [inst : TopologicalSpace β]
  [T1Space β] [SecondCountableTopology β] [Nonempty β] {f : α → β},
  (∀ (b : β), ∃ᵐ (x : α) ∂μ, f x ≠ b) → ∃ a b, a ≠ b ∧ (∀ s ∈ nhds a, 0 < μ (f ⁻¹' s)) ∧ ∀ t ∈ nhds b, 0 < μ (f ⁻¹' t)
-- Mathlib.GroupTheory.Submonoid.Center
AddSubmonoid.decidableMemCenter.eq_1 : ∀ {M : Type u_1} [inst : AddMonoid M] (a : M) [inst_1 : Decidable (∀ (b : M), b + a = a + b)],
  AddSubmonoid.decidableMemCenter a = decidable_of_iff' (∀ (g : M), g + a = a + g) ⋯
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
/-- Auxiliary definition for `SSet.Subcomplex.Pairing.Rank`.  -/
SSet.Subcomplex.Pairing.rank' : {X : SSet} → {A : X.Subcomplex} → (P : A.Pairing) → {y : ↑P.II} → Acc P.AncestralRel y → ℕ
-- Mathlib.Algebra.Group.Submonoid.MulAction
AddSubmonoid.vadd : {M' : Type u_1} → {α : Type u_2} → [inst : AddZeroClass M'] → [VAdd M' α] → (S : AddSubmonoid M') → VAdd (↥S) α
-- Init.Data.List.BasicAux
/-- Applies a function that returns a disjoint union to each element of a list, collecting the `Sum.inl`
and `Sum.inr` results into separate lists.

Examples:
 * `[0, 1, 2, 3].partitionMap (fun x => if x % 2 = 0 then .inl x else .inr x) = ([0, 2], [1, 3])`
 * `[0, 1, 2, 3].partitionMap (fun x => if x = 0 then .inl x else .inr x) = ([0], [1, 2, 3])`
 -/
List.partitionMap : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → (α → β ⊕ γ) → List α → List β × List γ
-- Mathlib.Analysis.Calculus.ContDiff.Comp
contDiffOn_prod_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {n : WithTop ℕ∞} (f : E → F × G),
  ContDiffOn 𝕜 n f s ↔ ContDiffOn 𝕜 n (Prod.fst ∘ f) s ∧ ContDiffOn 𝕜 n (Prod.snd ∘ f) s