mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.constGetEntryGED_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α} {fallback : α × β},
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ → Std.DTreeMap.Raw.Const.getEntryGED t₁ k fallback = Std.DTreeMap.Raw.Const.getEntryGED t₂ k fallback
-- Init.Data.SInt.Lemmas
Int8.toNat_toInt : ∀ (x : Int8), x.toInt.toNat = x.toNatClampNeg
-- Mathlib.Analysis.Complex.Circle
Submonoid.unitSphere.eq_1 : ∀ (𝕜 : Type u_2) [inst : SeminormedRing 𝕜] [inst_1 : NormMulClass 𝕜] [inst_2 : NormOneClass 𝕜],
  Submonoid.unitSphere 𝕜 = { carrier := Metric.sphere 0 1, mul_mem' := ⋯, one_mem' := ⋯ }
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.emptyOn.eq_1 : ∀ (α : Type u_2),
  Matroid.emptyOn α =
    { E := ∅, IsBase := fun x => x = ∅, Indep := fun x => x = ∅, indep_iff' := ⋯, exists_isBase := ⋯,
      isBase_exchange := ⋯, maximality := ⋯, subset_ground := ⋯ }
-- Lean.Meta.Instances
Lean.Meta.InstanceEntry.mk.injEq : ∀ (keys : Array Lean.Meta.InstanceKey) (val : Lean.Expr) (priority : ℕ) (globalName? : Option Lean.Name)
  (synthOrder : Array ℕ) (attrKind : Lean.AttributeKind) (keys_1 : Array Lean.Meta.InstanceKey) (val_1 : Lean.Expr)
  (priority_1 : ℕ) (globalName?_1 : Option Lean.Name) (synthOrder_1 : Array ℕ) (attrKind_1 : Lean.AttributeKind),
  ({ keys := keys, val := val, priority := priority, globalName? := globalName?, synthOrder := synthOrder,
        attrKind := attrKind } =
      { keys := keys_1, val := val_1, priority := priority_1, globalName? := globalName?_1, synthOrder := synthOrder_1,
        attrKind := attrKind_1 }) =
    (keys = keys_1 ∧
      val = val_1 ∧
        priority = priority_1 ∧ globalName? = globalName?_1 ∧ synthOrder = synthOrder_1 ∧ attrKind = attrKind_1)
-- Init.Meta.Defs
/-- Returns the value of the hexadecimal numeral as a natural number.  -/
Lean.TSyntax.getHexNumVal : Lean.Syntax.HexNum → ℕ
-- Init.Data.Array.Lemmas
Array.map_empty : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Array.map f #[] = #[]
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
/-- This map sends `f : C(X, ℝ)` to `Real.toNNReal ∘ f`, bundled as a continuous map `C(X, ℝ≥0)`.  -/
ContinuousMapZero.toNNReal : {X : Type u_1} → [inst : TopologicalSpace X] → [inst_1 : Zero X] → ContinuousMapZero X ℝ → ContinuousMapZero X NNReal
-- Mathlib.Topology.Order.LiminfLimsup
/-- A monotone function between (conditionally) complete linear ordered spaces sends a
`Filter.limsInf` to the `Filter.liminf` of the image if the function is continuous at the `limsInf`
(and the filter is bounded from below and frequently bounded from above).  -/
Monotone.map_limsInf_of_continuousAt : ∀ {R : Type u_4} {S : Type u_5} [inst : ConditionallyCompleteLinearOrder R] [inst_1 : TopologicalSpace R]
  [OrderTopology R] [inst_3 : ConditionallyCompleteLinearOrder S] [inst_4 : TopologicalSpace S] [OrderTopology S]
  {F : Filter R} [F.NeBot] {f : R → S},
  Monotone f →
    ContinuousAt f F.limsInf →
      autoParam (Filter.IsCobounded (fun x1 x2 => x1 ≥ x2) F) Monotone.map_limsInf_of_continuousAt._auto_1 →
        autoParam (Filter.IsBounded (fun x1 x2 => x1 ≥ x2) F) Monotone.map_limsInf_of_continuousAt._auto_3 →
          f F.limsInf = Filter.liminf f F
-- Mathlib.Data.Bool.Basic
Bool.not_iff_not : ∀ {b : Bool}, (!b) = true ↔ ¬b = true
-- Mathlib.Order.SuccPred.Basic
Order.succ_eq_sInf : ∀ {α : Type u_1} [inst : CompleteLattice α] [inst_1 : SuccOrder α] (a : α), Order.succ a = sInf (Set.Ioi a)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_minKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {fallback : α}, t.contains (t.minKeyD fallback) = true
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.nil_of_subsingleton : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} [Subsingleton V] (p : G.Walk v w), p.Nil
-- Lean.Elab.InfoTree.Main
/-- Similar to `realizeGlobalConstNoOverloadWithInfo`, except if there are multiple name resolutions then it returns them as a list.  -/
Lean.Elab.realizeGlobalConstWithInfos : Lean.Syntax → optParam (Option Lean.Expr) none → Lean.CoreM (List Lean.Name)
-- Mathlib.Order.Interval.Set.Fin
Fin.image_succ_Ico : ∀ {n : ℕ} (i j : Fin n), Fin.succ '' Set.Ico i j = Set.Ico i.succ j.succ
-- Mathlib.Data.Holor
Holor.mul_assoc0 : ∀ {α : Type} {ds₁ ds₂ ds₃ : List ℕ} [inst : Semigroup α] (x : Holor α ds₁) (y : Holor α ds₂) (z : Holor α ds₃),
  (x.mul y).mul z = (x.mul (y.mul z)).assocLeft
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.uliftYonedaEquiv_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))}
  (τ : CategoryTheory.uliftYoneda.{w, v₁, u₁}.obj X ⟶ F),
  CategoryTheory.uliftYonedaEquiv τ =
    (CategoryTheory.ConcreteCategory.hom (τ.app (Opposite.op X))) { down := CategoryTheory.CategoryStruct.id X }
-- Mathlib.CategoryTheory.Filtered.Flat
CategoryTheory.isCofiltered_of_representablyFlat : ∀ {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.IsCofiltered D] [CategoryTheory.RepresentablyFlat F],
  CategoryTheory.IsCofiltered C
-- Mathlib.Analysis.Normed.Group.Basic
norm_add_eq_norm_left : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (x : E) {y : E}, ‖y‖ = 0 → ‖x + y‖ = ‖x‖
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
/-- The sup of two finite-dimensional submodules is
finite-dimensional.  -/
Submodule.finiteDimensional_sup : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (S₁ S₂ : Submodule K V) [h₁ : FiniteDimensional K ↥S₁] [h₂ : FiniteDimensional K ↥S₂], FiniteDimensional K ↥(S₁ ⊔ S₂)
-- Mathlib.Data.ZMod.IntUnitsPower
uzpow_natCast : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : Module R (Additive ℤˣ)] (u : ℤˣ) (n : ℕ), u ^ ↑n = u ^ n
-- Mathlib.Order.Filter.Basic
Filter.nonempty_of_mem : ∀ {α : Type u} {f : Filter α} [hf : f.NeBot] {s : Set α}, s ∈ f → s.Nonempty
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.isZero₃_iff_isIso₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    CategoryTheory.Limits.IsZero T.obj₃ ↔ CategoryTheory.IsIso T.mor₁
-- Mathlib.RingTheory.Norm.Transitivity
/-- Given a ((m-1)+1)x((m-1)+1) block matrix `M = [[A,b],[c,d]]`, `auxMat M k` is the auxiliary
matrix `[[dI,0],[-c,1]]`. `k` corresponds to the last row/column of the matrix.  -/
Algebra.Norm.Transitivity.auxMat : {S : Type u_2} → {m : Type u_5} → [CommRing S] → Matrix m m S → [DecidableEq m] → m → Matrix m m S
-- Mathlib.Topology.Irreducible
Function.Surjective.preirreducibleSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f → Function.Surjective f → ∀ [PreirreducibleSpace X], PreirreducibleSpace Y
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.insertMin!.eq_def : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (t : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.insertMin! k v t =
    match t with
    | Std.DTreeMap.Internal.Impl.leaf =>
      Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf
    | Std.DTreeMap.Internal.Impl.inner size k' v' l' r' =>
      Std.DTreeMap.Internal.Impl.balanceL! k' v' (Std.DTreeMap.Internal.Impl.insertMin! k v l') r'
-- Mathlib.Algebra.Category.Grp.Ulift
/-- The universe lift functor for groups is full.
 -/
GrpCat.instFullUliftFunctor : GrpCat.uliftFunctor.Full
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.constVAdd_add : ∀ (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (v w : V₁),
  AffineEquiv.constVAdd k P₁ (v + w) = (AffineEquiv.constVAdd k P₁ w).trans (AffineEquiv.constVAdd k P₁ v)
-- Lean.Util.ShareCommon
Lean.ShareCommon.PShareCommonT.run : {m : Type u_1 → Type u_2} → {α : Type u_1} → [Monad m] → Lean.ShareCommon.PShareCommonT m α → m α
-- Init.Data.UInt.IntToBitVec
USize.toBitVec32_mod : ∀ {a b : USize} (h : System.Platform.numBits = 32), (a % b).toBitVec32 h = a.toBitVec32 h % b.toBitVec32 h
-- Init.Data.SInt.Lemmas
Int64.lt_iff_le_and_ne : ∀ {a b : Int64}, a < b ↔ a ≤ b ∧ a ≠ b
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.mcast.congr_simp : ∀ {a b : ℤ} {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} (h : a = b) (f f_1 : ModularForm Γ a),
  f = f_1 → ∀ (hΓ : Γ' = Γ), ModularForm.mcast h f hΓ = ModularForm.mcast h f_1 hΓ
-- Mathlib.ModelTheory.ElementarySubstructures
FirstOrder.Language.ElementarySubstructure.isElementary : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] (S : L.ElementarySubstructure M), (↑S).IsElementary
-- Init.Data.SInt.Lemmas
Int16.toInt_eq_toNatClampNeg : ∀ {a : Int16}, 0 ≤ a → a.toInt = ↑a.toNatClampNeg
-- Mathlib.Analysis.RCLike.Basic
RCLike.I_mem_skewAdjoint : ∀ {K : Type u_1} [inst : RCLike K], RCLike.I ∈ skewAdjoint K
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.principalUnitGroup_symm_apply : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (a : ↥(Units.map ↑(IsLocalRing.residue ↥A)).ker),
  ↑↑(A.principalUnitGroupEquiv.symm a) = ↑↑↑a
-- Mathlib.Data.Fintype.EquivFin
/-- An embedding from a `Fintype` to itself can be promoted to an equivalence.  -/
Function.Embedding.equivOfFiniteSelfEmbedding : {α : Type u_1} → [Finite α] → (α ↪ α) → α ≃ α
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.bernoulli.eq_1 : ∀ (p : NNReal) (h : p ≤ 1), PMF.bernoulli p h = PMF.ofFintype (fun b => bif b then ↑p else 1 - ↑p) ⋯
-- Init.Data.Int.DivMod.Lemmas
Int.mul_ediv_mul_of_pos : ∀ {a : ℤ} (b c : ℤ), 0 < a → a * b / (a * c) = b / c
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_of_mem_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] {f : (a : α) → β a → γ a} {k : α}, k ∈ Std.ExtDTreeMap.map f t → k ∈ t
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
CategoryTheory.ObjectProperty.IsClosedUnderFiniteProducts.isClosedUnderLimitsOfShape : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {P : CategoryTheory.ObjectProperty C}
  [self : P.IsClosedUnderFiniteProducts] (J : Type) [Finite J], P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete J)
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ServerCapabilities.declarationProvider : Lean.Lsp.ServerCapabilities → Bool
-- Mathlib.Algebra.CharP.Basic
instIsCharPOfIsLeftCancelAddOfCharP : ∀ (α : Type u_2) [inst : Semiring α] [IsLeftCancelAdd α] (n : ℕ) [CharP α n], Lean.Grind.IsCharP α n
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey!_alterKey_eq_self : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  [inst_4 : Std.LawfulEqOrd α] [inst_5 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      (Std.Internal.List.alterKey k f l).isEmpty = false →
        (Std.Internal.List.maxKey! (Std.Internal.List.alterKey k f l) = k ↔
          (f (Std.Internal.List.getValueCast? k l)).isSome = true ∧
            ∀ (k' : α), Std.Internal.List.containsKey k' l = true → (compare k' k).isLE = true)
-- Mathlib.Order.CompleteLattice.Lemmas
iInf_nat_gt_zero_eq : ∀ {α : Type u_1} [inst : CompleteLattice α] (f : ℕ → α), ⨅ i, ⨅ (_ : i > 0), f i = ⨅ i, f (i + 1)
-- Mathlib.AlgebraicTopology.SimplicialSet.RegularEpi
SSet.instIsRegularEpiCategory : CategoryTheory.IsRegularEpiCategory SSet
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.inl_desc_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} (hP : CategoryTheory.IsPushout f g inl inr) {W : C} (h : X ⟶ W) (k : Y ⟶ W)
  (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) {Z_1 : C} (h_1 : W ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp inl (CategoryTheory.CategoryStruct.comp (hP.desc h k w) h_1) =
    CategoryTheory.CategoryStruct.comp h h_1
-- Mathlib.ModelTheory.Substructures
/-- `map f` and `comap f` form a `GaloisInsertion` when `f` is surjective.  -/
FirstOrder.Language.Substructure.giMapComap : {L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type u_1} →
      [inst : L.Structure M] →
        [inst_1 : L.Structure N] →
          {f : L.Hom M N} →
            Function.Surjective ⇑f →
              GaloisInsertion (FirstOrder.Language.Substructure.map f) (FirstOrder.Language.Substructure.comap f)
-- Mathlib.Analysis.InnerProductSpace.Completion
UniformSpace.Completion.toInner.eq_1 : ∀ {𝕜' : Type u_4} {E' : Type u_5} [inst : TopologicalSpace 𝕜'] [inst_1 : UniformSpace E'] [inst_2 : Inner 𝕜' E'],
  UniformSpace.Completion.toInner = { inner := Function.curry (⋯.extend (Function.uncurry (inner 𝕜'))) }
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.monomial_def : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : DecidableEq σ] (n : σ →₀ ℕ),
  MvPowerSeries.monomial n = LinearMap.single R (fun x => R) n
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.ratio_le_opNorm : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  (f : NormedAddGroupHom V₁ V₂) (x : V₁), ‖f x‖ / ‖x‖ ≤ ‖f‖
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toList_ric_eq_none_iff : ∀ {n i : ℕ}, (*...=n).toList[i]? = none ↔ n < i
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.Types.coproductIso_ι_comp_hom : ∀ {J : Type v} (F : J → Type (max v u)) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι F j)
      (CategoryTheory.Limits.Types.coproductIso F).hom =
    TypeCat.ofHom fun x => ⟨j, x⟩
-- Mathlib.Data.List.Basic
List.length_eq_four : ∀ {α : Type u} {l : List α}, l.length = 4 ↔ ∃ a b c d, l = [a, b, c, d]
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- The sections of the restriction of `M` over `U` are isomorphic to `Γ(M, f ''ᵁ U).  -/
AlgebraicGeometry.Scheme.Modules.restrictAppIso : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    [inst : AlgebraicGeometry.IsOpenImmersion f] →
      (M : Y.Modules) →
        (U : X.Opens) →
          (M.restrict f).presheaf.obj (Opposite.op U) ≅
            M.presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U))
-- Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
AlgebraicGeometry.isOpenImmersion_isZariskiLocalAtTarget : AlgebraicGeometry.IsZariskiLocalAtTarget AlgebraicGeometry.IsOpenImmersion
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.adjugate_diagonal : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (v : n → α),
  (Matrix.diagonal v).adjugate = Matrix.diagonal fun i => ∏ j ∈ Finset.univ.erase i, v j
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
AlgebraicTopology.AlternatingCofaceMapComplex.d_eq_unop_d : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.CosimplicialObject C) (n : ℕ),
  AlgebraicTopology.AlternatingCofaceMapComplex.objD X n =
    (AlgebraicTopology.AlternatingFaceMapComplex.objD
        ((CategoryTheory.cosimplicialSimplicialEquiv C).functor.obj (Opposite.op X)) n).unop
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.imageSubobjectCompIso_inv_arrow_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasEqualizers C]
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasImage f] {Y' : C} (h : Y ⟶ Y') [inst_3 : CategoryTheory.IsIso h]
  {Z : C} (h_1 : Y' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectCompIso f h).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp f h)).arrow h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow
      (CategoryTheory.CategoryStruct.comp h h_1)
-- Std.Time.Format.Modifier
Std.Time.Modifier.K.injEq : ∀ (presentation presentation_1 : Std.Time.Number),
  (Std.Time.Modifier.K presentation = Std.Time.Modifier.K presentation_1) = (presentation = presentation_1)
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.N.le_iff : ∀ {X : SSet} {x y : X.N}, x ≤ y ↔ x.subcomplex ≤ y.subcomplex
-- Mathlib.GroupTheory.GroupAction.Hom
MulSemiringActionSemiHomClass.toRingHomClass : ∀ {F : Type u_15} {M : outParam (Type u_16)} {N : outParam (Type u_17)} [inst : Monoid M] [inst_1 : Monoid N]
  (φ : outParam (M → N)) {R : outParam (Type u_18)} {S : outParam (Type u_19)} [inst_2 : Semiring R]
  [inst_3 : Semiring S] [inst_4 : DistribMulAction M R] [inst_5 : DistribMulAction N S] [inst_6 : FunLike F R S]
  [self : MulSemiringActionSemiHomClass F φ R S], RingHomClass F R S
-- Mathlib.RingTheory.Smooth.Kaehler
/-- Given a surjective algebra homomorphism `f : P →ₐ[R] S` with square-zero kernel `I`,
there is a one-to-one correspondence between `P`-linear retractions of `I →ₗ[P] S ⊗[P] Ω[P/R]`
and algebra homomorphism sections of `f`.
 -/
retractionKerToTensorEquivSection : {R : Type u_1} →
  {P : Type u_2} →
    {S : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing P] →
          [inst_2 : CommRing S] →
            [inst_3 : Algebra R P] →
              [inst_4 : Algebra P S] →
                [inst_5 : Algebra R S] →
                  [inst_6 : IsScalarTower R P S] →
                    RingHom.ker (algebraMap P S) ^ 2 = ⊥ →
                      Function.Surjective ⇑(algebraMap P S) →
                        { l // l ∘ₗ KaehlerDifferential.kerToTensor R P S = LinearMap.id } ≃
                          { g // (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S }
-- Mathlib.RingTheory.PowerBasis
PowerBasis.basis : {R : Type u_7} →
  {S : Type u_8} →
    [inst : CommRing R] →
      [inst_1 : Ring S] → [inst_2 : Algebra R S] → (self : PowerBasis R S) → Module.Basis (Fin self.dim) R S
-- Mathlib.FieldTheory.Finite.Basic
/-- If `p` is a prime natural number and `x` is a natural number, then there exist natural numbers
`a ≤ p / 2` and `b ≤ p / 2` such that `a ^ 2 + b ^ 2 ≡ x [MOD p]`. This is a version of
`ZMod.sq_add_sq` with estimates on `a` and `b`.  -/
Nat.sq_add_sq_modEq : ∀ (p : ℕ) [Fact (Nat.Prime p)] (x : ℕ), ∃ a b, a ≤ p / 2 ∧ b ≤ p / 2 ∧ a ^ 2 + b ^ 2 ≡ x [MOD p]
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.aestronglyMeasurable : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (f : ↥(MeasureTheory.Lp E p μ)), MeasureTheory.AEStronglyMeasurable (↑↑f) μ
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicofork.ofπ_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) (P : C) (π : (b : J.R) → I.right b ⟶ P)
  (w :
    ∀ (a : J.L),
      CategoryTheory.CategoryStruct.comp (I.fst a) (π (J.fst a)) =
        CategoryTheory.CategoryStruct.comp (I.snd a) (π (J.snd a))),
  (CategoryTheory.Limits.Multicofork.ofπ I P π w).pt = P
-- Mathlib.GroupTheory.Congruence.BigOperators
/-- **Alias** of `AddCon.finsetSum`.

---

Additive congruence relations preserve finite sum.  -/
AddCon.finset_sum : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] (c : AddCon M) (s : Finset ι) {f g : ι → M},
  (∀ i ∈ s, c (f i) (g i)) → c (s.sum f) (s.sum g)
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.ofReal_toReal_ae_eq : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  (∀ᵐ (x : α) ∂μ, f x < ⊤) → (fun x => ENNReal.ofReal (f x).toReal) =ᵐ[μ] f
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- Equality holds when `a ≠ 0`. See `mul_inv_cancel_left`.  -/
mul_inv_left_le : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : Preorder G₀] {a b : G₀}, 0 ≤ b → a * (a⁻¹ * b) ≤ b
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.continuousOn_toReal : ContinuousOn ENNReal.toReal {a | a ≠ ⊤}
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.IsLimit.liftConeMorphism_eq_isTerminal_from : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c)
  (s : CategoryTheory.Limits.Cone F), hc.liftConeMorphism s = (c.isLimitEquivIsTerminal hc).from s
-- Mathlib.Algebra.GroupWithZero.Defs
/-- Multiplication by a nonzero element is left cancellative.  -/
IsLeftCancelMulZero.mul_left_cancel_of_ne_zero : ∀ {M₀ : Type u} {inst : Mul M₀} {inst_1 : Zero M₀} [self : IsLeftCancelMulZero M₀] {a : M₀}, a ≠ 0 → IsLeftRegular a
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_eq_getD_getKey? : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a fallback : α}, m.getKeyD a fallback = (m.getKey? a).getD fallback
-- Lean.Meta.Tactic.Split
/-- Internal exception for discriminant generalization failures due to type errors.
 -/
Lean.Meta.Split.discrGenExId : Lean.InternalExceptionId
-- Mathlib.Analysis.Convex.Combination
Finset.centerMass_congr_fun : ∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  {t : Finset ι} {w : ι → R} {z z' : ι → E}, (∀ i ∈ t, w i ≠ 0 → z i = z' i) → t.centerMass w z = t.centerMass w z'
-- Init.Data.String.Termination
String.Pos.lt_next_next : ∀ {s : String} {p : s.Pos} {h : p ≠ s.endPos} {h' : p.next h ≠ s.endPos}, p < (p.next h).next h'
-- Mathlib.Tactic.ClickSuggestions.Util
/-- The token for the solved goals.  -/
Mathlib.Tactic.ClickSuggestions.Context.solvedToken : Mathlib.Tactic.ClickSuggestions.Context → ProofWidgets.RefreshToken
-- Batteries.Data.AssocList
Batteries.AssocList.replace.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : BEq α] (a : α) (b : β),
  Batteries.AssocList.replace a b Batteries.AssocList.nil = Batteries.AssocList.nil
-- Mathlib.Geometry.Euclidean.Projection
EuclideanGeometry.reflection_apply' : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] (s : AffineSubspace 𝕜 P)
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] (p : P),
  (EuclideanGeometry.reflection s) p =
    (↑((EuclideanGeometry.orthogonalProjection s) p) -ᵥ p) +ᵥ ↑((EuclideanGeometry.orthogonalProjection s) p)
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.sUnion_mul : ∀ {α : Type u_2} [inst : Mul α] (S : Set (Set α)) (t : Set α), ⋃₀ S * t = ⋃ s ∈ S, s * t
-- Mathlib.RingTheory.MvPolynomial.Expand
MvPolynomial.map_frobenius_expand : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (p : ℕ) [inst_1 : ExpChar R p] {f : MvPolynomial σ R},
  (MvPolynomial.map (frobenius R p)) ((MvPolynomial.expand p) f) = f ^ p
-- Mathlib.Topology.Sheaves.Skyscraper
instIsLeftAdjointPresheafStalkFunctor : ∀ {X : TopCat} (p₀ : ↑X) {C : Type v} [inst : CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasTerminal C]
  [inst_2 : CategoryTheory.Limits.HasColimits C], (TopCat.Presheaf.stalkFunctor C p₀).IsLeftAdjoint
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.Disjoint.cycleType_mul : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ τ : Equiv.Perm α},
  σ.Disjoint τ → (σ * τ).cycleType = σ.cycleType + τ.cycleType
-- Mathlib.Combinatorics.SimpleGraph.DegreeSum
/-- The handshaking lemma.  See also `SimpleGraph.sum_degrees_eq_twice_card_edges`.  -/
SimpleGraph.even_card_odd_degree_vertices : ∀ {V : Type u} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj], Even {v | Odd (G.degree v)}.card