mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivAtFilter_id : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (L : Filter (𝕜 × 𝕜)), HasDerivAtFilter id 1 L
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_iUnion_le : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable β] (s : β → Set α)
  (f : α → ENNReal), ∫⁻ (a : α) in ⋃ i, s i, f a ∂μ ≤ ∑' (i : β), ∫⁻ (a : α) in s i, f a ∂μ
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.map_fst_toList_eq_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp}, List.map Prod.fst t.toList = t.keys
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeGroupBasis.ofFreeGroup.eq_1 : ∀ (X : Type u_5), FreeGroupBasis.ofFreeGroup X = { repr := MulEquiv.refl (FreeGroup X) }
-- Std.Data.DTreeMap.Internal.Balancing
/-- Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.rotateR : {α : Type u} →
  {β : α → Type v} →
    (k : α) →
      β k →
        (lk : α) →
          β lk →
            Std.DTreeMap.Internal.Impl α β →
              Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β
-- Mathlib.Algebra.Group.Commute.Hom
Commute.map : ∀ {F : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Mul M] [inst_1 : Mul N] {x y : M} [inst_2 : FunLike F M N]
  [MulHomClass F M N], Commute x y → ∀ (f : F), Commute (f x) (f y)
-- Mathlib.Analysis.Normed.Group.Defs
coe_lt_enorm : ∀ {E : Type u_8} [inst : NNNorm E] {x : E} {r : NNReal}, ↑r < ‖x‖ₑ ↔ r < ‖x‖₊
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.snakeInput_v₀₁_τ₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z),
  (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).v₀₁.τ₂ = CategoryTheory.kernelCokernelCompSequence.ι f g
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.withCurrentColumn : (ℕ → Lean.Parser.ParserFn) → Lean.Parser.ParserFn
-- Init.Data.Vector.Basic
/-- Returns `true` if `p` returns `true` for all elements of the vector.  -/
Vector.all : {α : Type u_1} → {n : ℕ} → Vector α n → (α → Bool) → Bool
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inf_sub_left : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : Sub α] [inst_2 : SemilatticeInf β]
  [inst_3 : OrderTop β] (s t : Finset α) (f : α → β), (s - t).inf f = s.inf fun x => t.inf fun x_1 => f (x - x_1)
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.mk.inj : ∀ {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}
  {functor functor_1 : CategoryTheory.Functor C V},
  { functor := functor } = { functor := functor_1 } → functor = functor_1
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∉ m₂ → (m₁ ∪ m₂)[k]? = m₁[k]?
-- Init.Data.UInt.Bitwise
UInt32.ofBitVec_and : ∀ (a b : BitVec 32), { toBitVec := a &&& b } = { toBitVec := a } &&& { toBitVec := b }
-- Mathlib.Combinatorics.Matroid.Circuit
/-- A cocircuit and a circuit cannot meet in exactly one element.  -/
Matroid.IsCircuit.inter_isCocircuit_ne_singleton : ∀ {α : Type u_1} {M : Matroid α} {C : Set α} {e : α} {K : Set α}, M.IsCircuit C → M.IsCocircuit K → C ∩ K ≠ {e}
-- Mathlib.CategoryTheory.Adjunction.Quadruple
/-- Adjunction `L ⊣ F` of the adjoint quadruple `L ⊣ F ⊣ G ⊣ R`.  -/
CategoryTheory.Adjunction.Quadruple.adj₁ : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {L : CategoryTheory.Functor C D} →
          {F : CategoryTheory.Functor D C} →
            {G : CategoryTheory.Functor C D} →
              {R : CategoryTheory.Functor D C} → CategoryTheory.Adjunction.Quadruple L F G R → (L ⊣ F)
-- Mathlib.Order.Atoms.Finite
Bool.instIsSimpleOrder : IsSimpleOrder Bool
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.instEmptyCollection : {α : Type u_1} → EmptyCollection (RBTree.RBNode α)
-- Mathlib.FieldTheory.IntermediateField.Basic
Subfield.toIntermediateField_toSubfield : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : Subfield L)
  (algebra_map_mem : ∀ (x : K), (algebraMap K L) x ∈ S), (S.toIntermediateField algebra_map_mem).toSubfield = S
-- Mathlib.Data.Complex.Basic
/-- Complex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.  -/
Complex : Type
-- Std.Data.HashMap.Lemmas
Std.HashMap.containsThenInsertIfNew_snd : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {k : α} {v : β},
  (m.containsThenInsertIfNew k v).2 = m.insertIfNew k v
-- Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
/-- `X □ Y` lifts against `Z` if and only if `Y` lifts against `X ⋔ Z`.  -/
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] [inst_3 : CategoryTheory.MonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalClosed C] {X Y Z : CategoryTheory.Arrow C},
  CategoryTheory.HasLiftingProperty (X □ Y).hom Z.hom ↔ CategoryTheory.HasLiftingProperty Y.hom (Opposite.op X ⋔ Z).hom
-- Mathlib.RingTheory.DedekindDomain.Different
_private.Mathlib.RingTheory.DedekindDomain.Different.0.FractionalIdeal.«term_ᵛ» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.OrderOfVanishing.Basic
Ring.ordMonoidWithZeroHom_isUnit : ∀ (R : Type u_1) [inst : CommRing R] [IsNoetherianRing R] [Ring.KrullDimLE 1 R] [inst_3 : Nontrivial R]
  (y : ↥(nonZeroDivisors R)), IsUnit ((Ring.ordMonoidWithZeroHom R) ↑y)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.mem_bot : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {x : R}, x ∈ ⊥ ↔ x = 0
-- Mathlib.Topology.Sheaves.Presheaf
/-- push forward of a presheaf  -/
AlgebraicGeometry.«term__*_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
/-- If `W₁ ≤ W₁'` and `W₂ ≤ W₂'`, then a functorial factorization for `W₁` and `W₂` induces
a functorial factorization for `W₁'` and `W₂'`.  -/
CategoryTheory.MorphismProperty.FunctorialFactorizationData.ofLE : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W₁ W₂ : CategoryTheory.MorphismProperty C} →
      W₁.FunctorialFactorizationData W₂ →
        {W₁' W₂' : CategoryTheory.MorphismProperty C} → W₁ ≤ W₁' → W₂ ≤ W₂' → W₁'.FunctorialFactorizationData W₂'
-- Mathlib.SetTheory.Ordinal.Family
/-- The supremum of a family of ordinals indexed by the set of ordinals less than some
`o : Ordinal.{u}`. This is a special case of `iSup` over the family provided by
`familyOfBFamily`.  -/
Ordinal.bsup : (o : Ordinal.{u}) → ((a : Ordinal.{u}) → a < o → Ordinal.{max u v}) → Ordinal.{max u v}
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.WalkingPair.swap_apply_left : CategoryTheory.Limits.WalkingPair.swap CategoryTheory.Limits.WalkingPair.left = CategoryTheory.Limits.WalkingPair.right
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.any_eq_true_iff_exists_mem_get : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [LawfulHashable α] [EquivBEq α]
  {p : α → Bool}, m.WF → (m.any p = true ↔ ∃ a, ∃ (h : a ∈ m), p (m.get a h) = true)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryGT?.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α),
  Std.DTreeMap.Internal.Impl.Const.getEntryGT? k = Std.DTreeMap.Internal.Impl.Const.getEntryGT?.go k none
-- Mathlib.Analysis.Calculus.TangentCone.Pi
/-- The tangent cone of a product contains the tangent cone of each factor.  -/
mapsTo_tangentConeAt_pi : ∀ {𝕜 : Type u_1} [inst : Semiring 𝕜] {ι : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → AddCommGroup (E i)]
  [inst_2 : (i : ι) → Module 𝕜 (E i)] [inst_3 : (i : ι) → TopologicalSpace (E i)] [∀ (i : ι), ContinuousAdd (E i)]
  [∀ (i : ι), ContinuousConstSMul 𝕜 (E i)] {s : (i : ι) → Set (E i)} {x : (i : ι) → E i} [inst_6 : DecidableEq ι]
  {i : ι},
  (∀ (j : ι), j ≠ i → x j ∈ closure (s j)) →
    Set.MapsTo (Pi.single i) (tangentConeAt 𝕜 (s i) (x i)) (tangentConeAt 𝕜 (Set.univ.pi s) x)
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.sum_Iio_add_eq_sum_Iic : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {f : α → M} [inst_1 : PartialOrder α]
  [inst_2 : LocallyFiniteOrderBot α] (a : α), ∑ x < a, f x + f a = ∑ x ≤ a, f x
-- Mathlib.Data.NNRat.Defs
NNRat.coe_coeHom : ⇑NNRat.coeHom = NNRat.cast
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.affineLocally_le : ∀ {P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, P f → Q f) →
    (AlgebraicGeometry.affineLocally fun {R S} [CommRing R] [CommRing S] => P) ≤
      AlgebraicGeometry.affineLocally fun {R S} [CommRing R] [CommRing S] => Q
-- Std.Data.DTreeMap.Raw.Slice
Std.DTreeMap.Raw.instSliceableRcoSlice : {α : Type u} →
  {β : α → Type v} →
    (cmp : autoParam (α → α → Ordering) Std.DTreeMap.Raw.instSliceableRcoSlice._auto_1) →
      Std.Rco.Sliceable (Std.DTreeMap.Raw α β cmp) α (Std.DTreeMap.Internal.RcoSlice α β)
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.mk.sizeOf_spec : ∀ {α : Type u_8} {β : Type u_9} [inst : SupSet α] [inst_1 : SupSet β] [inst_2 : SizeOf α] [inst_3 : SizeOf β]
  (toFun : α → β) (map_sSup' : ∀ (s : Set α), toFun (sSup s) = sSup (toFun '' s)),
  sizeOf { toFun := toFun, map_sSup' := map_sSup' } = 1
-- Std.Internal.Parsec.String
/-- Skips the given string.
 -/
Std.Internal.Parsec.String.skipString : String → Std.Internal.Parsec.String.Parser Unit
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimTargetInfo.mk.sizeOf_spec : ∀ (view : Lean.Elab.Tactic.ElimTargetView) (expr : Lean.Expr) (arg? : Option Lean.Meta.GeneralizeArg),
  sizeOf { view := view, expr := expr, arg? := arg? } = 1 + sizeOf view + sizeOf expr + sizeOf arg?
-- Mathlib.Data.Part
Part.right_dom_of_sdiff_dom : ∀ {α : Type u_1} [inst : SDiff α] {a b : Part α}, (a \ b).Dom → b.Dom
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.instSMulCommClass_1 : ∀ {R : Type u_1} {M : Type u_3} {X : Type u_4} [inst : Monoid M] {S : Submonoid M} [inst_1 : OreLocalization.OreSet S]
  [inst_2 : MulAction M X] [inst_3 : SMul R X] [inst_4 : SMul R M] [inst_5 : IsScalarTower R M M]
  [inst_6 : IsScalarTower R M X] [SMulCommClass R M M], SMulCommClass R (OreLocalization S M) (OreLocalization S X)
-- Mathlib.Algebra.Category.MonCat.Basic
MulEquiv.toCommMonCatIso_inv : ∀ {X Y : Type u} [inst : CommMonoid X] [inst_1 : CommMonoid Y] (e : X ≃* Y),
  e.toCommMonCatIso.inv = CommMonCat.ofHom e.symm.toMonoidHom
-- Init.MethodSpecsSimp
Sub.sub_eq_hSub : ∀ {α : Type u_1} [inst : Sub α], Sub.sub = HSub.hSub
-- Init.Coe
CoeHead.mk : {α : Sort u} → {β : semiOutParam (Sort v)} → (α → β) → CoeHead α β
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Mon.zero_hom : ∀ {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D] [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory D]
  (M N : CategoryTheory.Mon D),
  CategoryTheory.Mon.Hom.hom 0 =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit M.X)
      CategoryTheory.MonObj.one
-- Mathlib.Data.Nat.GCD.Basic
Nat.not_coprime_zero_zero : ¬Nat.Coprime 0 0
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.leadingCoeff_zero : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R], HahnSeries.leadingCoeff 0 = 0
-- Mathlib.Order.Filter.NAry
Filter.map₂_mono_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f₁ f₂ : Filter α} {g : Filter β},
  f₁ ≤ f₂ → Filter.map₂ m f₁ g ≤ Filter.map₂ m f₂ g
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.mem_modify : ∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  t.WF → ∀ {k k' : α} {f : β → β}, k' ∈ Std.DTreeMap.Internal.Impl.Const.modify k f t ↔ k' ∈ t
-- Mathlib.Topology.Algebra.OpenSubgroup
AddSubgroup.isOpen_mono : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [SeparatelyContinuousAdd G] {H₁ H₂ : AddSubgroup G},
  H₁ ≤ H₂ → IsOpen ↑H₁ → IsOpen ↑H₂
-- Mathlib.CategoryTheory.Action.Basic
Action.Hom.instInhabited : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_2} → [inst_1 : Monoid G] → (M : Action V G) → Inhabited (M.Hom M)
-- Mathlib.Analysis.Normed.Group.Continuity
/-- If `‖y‖→∞`, then we can assume `y≠x` for any
fixed `x`  -/
eventually_ne_of_tendsto_norm_atTop : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedAddGroup E] {l : Filter α} {f : α → E},
  Filter.Tendsto (fun y => ‖f y‖) l Filter.atTop → ∀ (x : E), ∀ᶠ (y : α) in l, f y ≠ x
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ D` preserves limits of `K.leftOp : Jᵒᵖ ⥤ C`, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` preserves
colimits of `K : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.preservesColimit_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J Cᵒᵖ)
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimit K.leftOp F],
  CategoryTheory.Limits.PreservesColimit K F.op
-- Mathlib.Condensed.Discrete.LocallyConstant
/-- The functor from the category of sets to presheaves on `CompHausLike P` given by locally constant
maps.
 -/
CompHausLike.LocallyConstant.functorToPresheaves : {P : TopCat → Prop} →
  CategoryTheory.Functor (Type (max u w)) (CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w)))
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.ofAlgHom_symm_apply : ∀ {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₂] (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ : f.comp g = AlgHom.id R A₂)
  (h₂ : g.comp f = AlgHom.id R A₁) (a : A₂), (AlgEquiv.ofAlgHom f g h₁ h₂).symm a = g a
-- Mathlib.Data.QPF.Univariate.Basic
/-- destructor for type defined by `Cofix`  -/
QPF.Cofix.dest : {F : Type u → Type u} → [q : QPF F] → QPF.Cofix F → F (QPF.Cofix F)
-- Mathlib.Algebra.CharP.Pi
CharP.pi : ∀ (ι : Type u) [hi : Nonempty ι] (R : Type v) [inst : Semiring R] (p : ℕ) [CharP R p], CharP (ι → R) p
-- Mathlib.Topology.Bases
/-- If a family of sets `s` generates the topology, then intersections of finite
subcollections of `s` form a topological basis.  -/
TopologicalSpace.isTopologicalBasis_of_subbasis : ∀ {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)},
  t = TopologicalSpace.generateFrom s → TopologicalSpace.IsTopologicalBasis ((fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s})
-- Init.Data.Range.Polymorphic.Fin
Fin.instHasSize : {n : ℕ} → Std.Rxc.HasSize (Fin n)
-- Mathlib.Data.Finsupp.SMul
/-- `Finsupp.single` as a `DistribMulActionSemiHom`.

See also `Finsupp.lsingle` for the version as a linear map.  -/
Finsupp.DistribMulActionHom.single : {α : Type u_1} →
  {M : Type u_3} →
    {R : Type u_6} → [inst : Monoid R] → [inst_1 : AddMonoid M] → [inst_2 : DistribMulAction R M] → α → M →+[R] α →₀ M
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for unsigned less than or equal `ule` on `BitVec`s.  -/
BitVec.reduceULE : Lean.Meta.Simp.DSimproc
-- Mathlib.Analysis.Normed.Module.Connected
/-- In a real vector space of dimension `> 1`, the complement of any countable set is
connected.  -/
Set.Countable.isConnected_compl_of_one_lt_rank : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [ContinuousAdd E]
  [ContinuousSMul ℝ E], 1 < Module.rank ℝ E → ∀ {s : Set E}, s.Countable → IsConnected sᶜ
-- Mathlib.AlgebraicGeometry.PullbackCarrier
/-- The comparison map for pullbacks under the forgetful functor `Scheme ⥤ Type u` is surjective.  -/
AlgebraicGeometry.Scheme.pullbackComparison_forget_surjective : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S),
  Function.Surjective
    ⇑(CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.Limits.pullbackComparison AlgebraicGeometry.Scheme.forget f g))
-- Mathlib.GroupTheory.QuotientGroup.Defs
/-- An `AddGroup` homomorphism `φ : G →+ M` with `N ⊆ ker(φ)` descends (i.e. `lift`s)
to an `AddGroup` homomorphism `G/N →+ M`.  -/
QuotientAddGroup.lift : {G : Type u_1} →
  {M : Type u_4} →
    [inst : AddGroup G] →
      [inst_1 : AddMonoid M] → (N : AddSubgroup G) → [nN : N.Normal] → (φ : G →+ M) → N ≤ φ.ker → G ⧸ N →+ M
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.unsat_eq_cert.eq_1 : ∀ (p : Lean.Grind.CommRing.Poly) (k : ℤ),
  Lean.Grind.CommRing.Stepwise.unsat_eq_cert p k = (!k.beq' 0).and' (p.beq' (Lean.Grind.CommRing.Poly.num k))
-- Mathlib.Algebra.Group.Pi.Lemmas
MonoidHom.pi.eq_1 : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → MulOneClass (f i)] {γ : Type w} [inst_1 : MulOneClass γ]
  (g : (i : I) → γ →* f i), MonoidHom.pi g = { toFun := fun x i => (g i) x, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.SetTheory.Cardinal.NatCard
Finite.card_eq : ∀ {α : Type u_1} {β : Type u_2} [Finite α] [Finite β], Nat.card α = Nat.card β ↔ Nonempty (α ≃ β)
-- Plausible.Gen
Plausible.instInhabitedGenError.default : Plausible.GenError
-- Mathlib.Algebra.Ring.BooleanRing
BooleanRing.instIdempotentOpHMul : ∀ {α : Type u_1} [inst : BooleanRing α], Std.IdempotentOp fun x1 x2 => x1 * x2
-- Mathlib.CategoryTheory.Localization.Bifunctor
CategoryTheory.Localization.Lifting₂.liftingLift₂Flip : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D₁ : Type u_3} →
      {D₂ : Type u_4} →
        {E : Type u_5} →
          [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_5} E] →
                    (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E)) →
                      {W₁ : CategoryTheory.MorphismProperty C₁} →
                        {W₂ : CategoryTheory.MorphismProperty C₂} →
                          (hF : W₁.IsInvertedBy₂ W₂ F) →
                            (L₁ : CategoryTheory.Functor C₁ D₁) →
                              (L₂ : CategoryTheory.Functor C₂ D₂) →
                                [inst_5 : L₁.IsLocalization W₁] →
                                  [inst_6 : L₂.IsLocalization W₂] →
                                    [inst_7 : W₁.ContainsIdentities] →
                                      [inst_8 : W₂.ContainsIdentities] →
                                        (X₂ : C₂) →
                                          CategoryTheory.Localization.Lifting L₁ W₁ (F.flip.obj X₂)
                                            ((CategoryTheory.Localization.lift₂ F hF L₁ L₂).flip.obj (L₂.obj X₂))
-- Batteries.Data.Char.AsciiCasing
Char.isLower_toLower_eq_isAlpha : ∀ (c : Char), c.toLower.isLower = c.isAlpha
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.contract_restrict_eq_restrict_contract : ∀ {α : Type u_1} {R C : Set α} (M : Matroid α),
  Disjoint C R → (M.contract C).restrict R = (M.restrict (R ∪ C)).contract C
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.mk_sub : ∀ {R : Type u_1} {M : Type u_2} {x y : M} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (p : Submodule R M), Submodule.Quotient.mk (x - y) = Submodule.Quotient.mk x - Submodule.Quotient.mk y
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
ConjRootClass.carrier_eq_mk_aroots_minpoly : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : Algebra.IsSeparable K L] (c : ConjRootClass K L) [inst_4 : Fintype ↑c.carrier],
  c.carrier.toFinset = { val := c.minpoly.aroots L, nodup := ⋯ }
-- Std.Data.Iterators.Lemmas.Equivalence.StepCongr
_private.Std.Data.Iterators.Lemmas.Equivalence.StepCongr.0.Std.bind_comp_eq_map_bind : ∀ {α β γ : Type u_1} {m : Type u_1 → Type u_2} [inst : Monad m] [LawfulMonad m] {f : α → β} {g : β → m γ} {x : m α},
  x >>= g ∘ f = f <$> x >>= g
-- Mathlib.Topology.Separation.Basic
/-- Given an open finite set `S` in a T₀ space, there is some `x ∈ S` such that `{x}` is open.  -/
exists_isOpen_singleton_of_isOpen_finite : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X] {s : Set X},
  s.Finite → s.Nonempty → IsOpen s → ∃ x ∈ s, IsOpen {x}
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_add_Ioo : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b c : α),
  (fun x => a + x) ⁻¹' Set.Ioo b c = Set.Ioo (b - a) (c - a)
-- Mathlib.CategoryTheory.Localization.Construction
/-- The morphism in the path category corresponding to a formal inverse.  -/
CategoryTheory.Localization.Construction.ψ₂ : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    (W : CategoryTheory.MorphismProperty C) →
      {X Y : C} →
        (w : X ⟶ Y) →
          W w →
            (CategoryTheory.Localization.Construction.ιPaths W Y ⟶ CategoryTheory.Localization.Construction.ιPaths W X)
-- Mathlib.CategoryTheory.Simple
CategoryTheory.simple_obj_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [F.IsEquivalence] (X : C), CategoryTheory.Simple (F.obj X) ↔ CategoryTheory.Simple X
-- Mathlib.SetTheory.Cardinal.Order
nonempty_embedding_to_cardinal : ∀ {α : Type u}, Nonempty (α ↪ Cardinal.{u})
-- Mathlib.Analysis.InnerProductSpace.Basic
re_inner_le_norm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E), RCLike.re (inner 𝕜 x y) ≤ ‖x‖ * ‖y‖
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.HaveLebesgueDecomposition.sum_left : ∀ {α : Type u_1} {m : MeasurableSpace α} {ν : MeasureTheory.Measure α} {ι : Type u_2} [Countable ι]
  (μ : ι → MeasureTheory.Measure α) [∀ (i : ι), (μ i).HaveLebesgueDecomposition ν],
  (MeasureTheory.Measure.sum μ).HaveLebesgueDecomposition ν
-- Std.Sync.RecursiveMutex
_private.Std.Sync.RecursiveMutex.0.Std.RecursiveMutex.mk.injEq : ∀ {α : Type} (ref : IO.Ref α) (mutex : Std.BaseRecursiveMutex) (ref_1 : IO.Ref α) (mutex_1 : Std.BaseRecursiveMutex),
  ({ ref := ref, mutex := mutex } = { ref := ref_1, mutex := mutex_1 }) = (ref = ref_1 ∧ mutex = mutex_1)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.card_lt_card_of_left_finite : ∀ {α : Type u} {A B : Set α}, A.Finite → A ⊂ B → Cardinal.mk ↑A < Cardinal.mk ↑B
-- Init.Data.UInt.Lemmas
UInt8.toFin_ofNatClamp_of_lt : ∀ {n : ℕ} (hn : n < UInt8.size), (UInt8.ofNatClamp n).toFin = ⟨n, hn⟩
-- Mathlib.GroupTheory.Perm.List
List.formPerm_reverse : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), l.reverse.formPerm = l.formPerm⁻¹
-- Lean.Data.Lsp.Internal
Lean.Lsp.RefIdent.RefIdentJsonRepr.c.inj : ∀ {m n m_1 n_1 : String},
  Lean.Lsp.RefIdent.RefIdentJsonRepr.c m n = Lean.Lsp.RefIdent.RefIdentJsonRepr.c m_1 n_1 → m = m_1 ∧ n = n_1
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Pretrivialization.IsLinear.mk : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : AddCommMonoid F] [inst_4 : Module R F]
  [inst_5 : (x : B) → AddCommMonoid (E x)] [inst_6 : (x : B) → Module R (E x)]
  {e : Bundle.Pretrivialization F Bundle.TotalSpace.proj},
  (∀ b ∈ e.baseSet, IsLinearMap R fun x => (↑e ⟨b, x⟩).2) → Bundle.Pretrivialization.IsLinear R e