mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.map_congr : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} {f g : G →* H} {φ : Rep.res f A ⟶ B} {ψ : Rep.res g A ⟶ B},
  f = g →
    (Rep.Hom.hom φ).toLinearMap = (Rep.Hom.hom ψ).toLinearMap →
      ∀ (n : ℕ), groupCohomology.map f φ n = groupCohomology.map g ψ n
-- Mathlib.Tactic.DeriveTraversable
/-- Prove the functor laws and derive `LawfulFunctor`.  -/
Mathlib.Deriving.Traversable.deriveLawfulFunctor : Lean.MVarId → Lean.Elab.TermElabM Unit
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.instUniqueHomLeftExtensionFunctorOppositeTypeUliftYonedaCompMkLanOpHomCompULiftYonedaIsoULiftYonedaCompLan : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [inst_2 : ∀ (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))), F.op.HasLeftKanExtension P] →
            (Φ :
                CategoryTheory.StructuredArrow (F.comp CategoryTheory.uliftYoneda.{max w v₁, v₂, u₂})
                  ((CategoryTheory.Functor.whiskeringLeft C (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂)))
                        (CategoryTheory.Functor Dᵒᵖ (Type (max w v₁ v₂)))).obj
                    CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁})) →
              Unique
                (CategoryTheory.Functor.LeftExtension.mk F.op.lan
                    (CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan F).hom ⟶
                  Φ)
-- Mathlib.Algebra.Lie.Weights.Cartan
LieAlgebra.rootSpaceWeightSpaceProduct.congr_simp : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (H : LieSubalgebra R L) [inst_3 : LieRing.IsNilpotent ↥H] (M : Type u_3) [inst_4 : AddCommGroup M]
  [inst_5 : Module R M] [inst_6 : LieRingModule L M] [inst_7 : LieModule R L M] (χ₁ χ₂ χ₃ : ↥H → R) (hχ : χ₁ + χ₂ = χ₃),
  LieAlgebra.rootSpaceWeightSpaceProduct R L H M χ₁ χ₂ χ₃ hχ =
    LieAlgebra.rootSpaceWeightSpaceProduct R L H M χ₁ χ₂ χ₃ hχ
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.coe_pos : ∀ {α : Type u} [inst : Zero α] {a : α} [inst_1 : LT α], 0 < ↑a ↔ 0 < a
-- Mathlib.Topology.Order.Basic
IsUpperSet.isClosed : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [WellFoundedLT α] {s : Set α},
  IsUpperSet s → IsClosed s
-- Mathlib.Algebra.Group.Equiv.Opposite
MulEquiv.op_symm_apply_apply : ∀ {α : Type u_3} {β : Type u_4} [inst : Mul α] [inst_1 : Mul β] (f : αᵐᵒᵖ ≃* βᵐᵒᵖ) (a : α),
  (MulEquiv.op.symm f) a = (MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op) a
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
_private.Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion.0.Tactic.ComputeAsymptotics.Seq.FriendlyOperation.coind_comp_friend_right.match_1_1.eq_1 : ∀ {α : Type u_1} (motive : Option (α × Subtype Tactic.ComputeAsymptotics.Seq.FriendlyOperation) → Sort u_2)
  (h_1 : Unit → motive none)
  (h_2 : (hd : α) → (opf' : Subtype Tactic.ComputeAsymptotics.Seq.FriendlyOperation) → motive (some (hd, opf'))),
  (match none with
    | none => h_1 ()
    | some (hd, opf') => h_2 hd opf') =
    h_1 ()
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Cpop
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Cpop.0.Std.Tactic.BVDecide.BVExpr.bitblast.denote_append_blastExtractAndExtendBit : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {idx : ℕ} (assign : α → Bool) (aig : Std.Sat.AIG α)
  (currIdx w : ℕ) (x : BitVec w) (xc : aig.RefVec w) (acc : aig.RefVec (w * currIdx)) (hidx : idx < w * currIdx + w),
  (∀ (idx : ℕ) (hidx : idx < w * currIdx),
      ⟦assign, { aig := aig, ref := acc.get idx hidx }⟧ = (BitVec.extractAndExtend w x).getLsbD idx) →
    (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := xc.get idx hidx }⟧ = x.getLsbD idx) →
      ⟦assign,
          { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtendBit aig { start := currIdx, x := xc }).aig,
            ref :=
              ((acc.cast ⋯).append
                    (Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtendBit aig
                        { start := currIdx, x := xc }).vec).get
                idx hidx }⟧ =
        (BitVec.extractAndExtend w x).getLsbD idx
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.assemble₂.eq_def : ∀ (w x : UInt8),
  ByteArray.utf8DecodeChar?.assemble₂ w x =
    if ByteArray.utf8DecodeChar?.isInvalidContinuationByte x = true then none
    else
      let r := ByteArray.utf8DecodeChar?.assemble₂Unchecked w x;
      if r < 128 then none else some { val := r, valid := ⋯ }
-- Mathlib.GroupTheory.OrderOfElement
AddRightCancelMonoid.addGroupOfFinite.eq_1 : ∀ {H : Type u_6} [inst : AddRightCancelMonoid H] [inst_1 : Finite H],
  AddRightCancelMonoid.addGroupOfFinite = (AddEquiv.opOp H).addGroup
-- Mathlib.GroupTheory.Congruence.Basic
Con.comapQuotientEquiv.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (c : Con M) (f : N →* M),
  c.comapQuotientEquiv f = (Con.congr (MulEquiv.refl N) ⋯).trans (Con.quotientKerEquivRange (c.mk'.comp f))
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.mapM.eq_1 : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {m : Type w → Type w'} [inst_1 : Monad m] [inst_2 : MonadAttach m]
  (f : β → m γ) (it : Std.Iter β), Std.Iter.mapM f it = Std.IterM.mapM f it.toIterM
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.Iso.homCongr_eq_arrowCongr : ∀ {S : Type u} [inst : CommSemiring S] {X Y X' Y' : SemimoduleCat S} (i : X ≅ X') (j : Y ≅ Y') (f : X ⟶ Y),
  (i.homCongr j) f = { hom' := (i.toLinearEquivₛ.arrowCongr j.toLinearEquivₛ) (SemimoduleCat.Hom.hom f) }
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
isAddCyclic_left_of_prod : ∀ (M : Type u_4) (N : Type u_5) [inst : AddGroup M] [inst_1 : AddGroup N] [cyc : IsAddCyclic (M × N)], IsAddCyclic M
-- Lean.Log
/-- If `warningAsError` is set to `true`, then warning messages are treated as errors.  -/
Lean.warningAsError : Lean.Option Bool
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.insertMany_ind : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {ρ : Type w} [inst : ForIn Id ρ (α × β)]
  [inst_1 : EquivBEq α] [inst_2 : LawfulHashable α] {motive : Std.ExtHashMap α β → Prop} (m : Std.ExtHashMap α β)
  {l : ρ},
  motive m → (∀ (m : Std.ExtHashMap α β) (a : α) (b : β), motive m → motive (m.insert a b)) → motive (m.insertMany l)
-- Mathlib.Data.Set.Image
Subtype.coe_image : ∀ {α : Type u_1} {p : α → Prop} {s : Set (Subtype p)}, Subtype.val '' s = {x | ∃ (h : p x), ⟨x, h⟩ ∈ s}
-- Mathlib.ModelTheory.Definability
/-- **Alias** of `Set.DefinableFun.ofPred_eq`.

---

The set where two definable functions agree is definable.  -/
Set.DefinableFun.setOf_eq : ∀ {M : Type u_1} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u_2} {A : Set M} {f g : (α → M) → M},
  Set.DefinableFun L A f → Set.DefinableFun L A g → A.Definable L {v | f v = g v}
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.map_apply_div : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {R : Type u_1} {F : Type u_2} [inst_2 : CommRing R]
  [inst_3 : IsDomain R] [inst_4 : FunLike F (Polynomial K) (Polynomial R)]
  [inst_5 : MonoidWithZeroHomClass F (Polynomial K) (Polynomial R)] (φ : F)
  (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial R))) (p q : Polynomial K),
  (RatFunc.map φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q) =
    (algebraMap (Polynomial R) (RatFunc R)) (φ p) / (algebraMap (Polynomial R) (RatFunc R)) (φ q)
-- Mathlib.Control.ULift
ULift.instMonad_mathlib : Monad ULift.{u_2, u_1}
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasStrictDerivAt.scomp_of_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) {𝕜' : Type u_1} [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  [inst_5 : NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {h : 𝕜 → 𝕜'} {h' : 𝕜'} {g₁ : 𝕜' → F} {g₁' : F} {y : 𝕜'},
  HasStrictDerivAt g₁ g₁' y → HasStrictDerivAt h h' x → y = h x → HasStrictDerivAt (g₁ ∘ h) (h' • g₁') x
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
_private.Mathlib.Algebra.BigOperators.Group.Finset.Defs.0.BigOperators.FinsetResult.finset.sizeOf_spec : ∀ (s : Lean.Term), sizeOf (BigOperators.FinsetResult.finset✝ s) = 1 + sizeOf s
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
SSet.nonempty_of_hom : ∀ {X Y : SSet} (f : Y ⟶ X) [Y.Nonempty], X.Nonempty
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.zero_def : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  [inst_2 : Zero β], 0 = MeasureTheory.AEEqFun.mk (fun x => 0) ⋯
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_neg_eq_log : ∀ (x : ℝ), Real.log (-x) = Real.log x
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.size_union_le_size_add_size : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  (t₁ ∪ t₂).size ≤ t₁.size + t₂.size
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
/-- Given edges `f`, `g` and `h` of a `2`-truncated quasicategory,
there exists a structure `CompStruct f g h` iff
`homMk f ≫ homMk g = homMk h` holds in the homotopy category.
 -/
SSet.Truncated.Edge.CompStruct.nonempty_iff : ∀ {A : SSet.Truncated 2} [inst : A.Quasicategory₂]
  {x y z : A.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 })}
  {f : SSet.Truncated.Edge x y} {g : SSet.Truncated.Edge y z} {h : SSet.Truncated.Edge x z},
  Nonempty (f.CompStruct g h) ↔
    CategoryTheory.CategoryStruct.comp (SSet.Truncated.HomotopyCategory₂.homMk f)
        (SSet.Truncated.HomotopyCategory₂.homMk g) =
      SSet.Truncated.HomotopyCategory₂.homMk h
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- For a group with zero, `MulPosReflectLT G₀` implies `MulPosStrictMono G₀`.  -/
MulPosReflectLT.toMulPosStrictMono : ∀ (G₀ : Type u_3) [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀], MulPosStrictMono G₀
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
/-- The set of functions on `X ⊕ Y` that are candidates distances to realize the
minimum of the Hausdorff distances between `X` and `Y` in a coupling.  -/
GromovHausdorff.candidates : (X : Type u) → (Y : Type v) → [MetricSpace X] → [MetricSpace Y] → Set (GromovHausdorff.ProdSpaceFun✝ X Y)
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
/-- Given a perfect pairing between `M` and `N`, we may interchange the roles of `M` and `N`.  -/
LinearMap.IsPerfPair.flip : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_5} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] [inst_2 : CommRing R]
  [inst_3 : Module R M] [inst_4 : Module R N] {p : M →ₗ[R] N →ₗ[R] R}, p.IsPerfPair → p.flip.IsPerfPair
-- Mathlib.Topology.Category.TopPair
/-- The functor from topological pairs to topological spaces that forgets the first space, i.e. the
projection to the second space.  -/
TopPair.proj₂ : CategoryTheory.Functor TopPair TopCat
-- Mathlib.Tactic.CasesM
/-- Auxiliary for `casesMatching`. Accumulates generated subgoals in `acc`.  -/
_private.Mathlib.Tactic.CasesM.0.Lean.MVarId.casesMatching.go : (Lean.Expr → Lean.MetaM Bool) →
  Bool → Bool → Lean.MVarId → optParam (Array Lean.MVarId) #[] → Lean.MetaM (Array Lean.MVarId)
-- Mathlib.Topology.Constructions.SumProd
isInducing_sumElim : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Z} {g : Y → Z},
  Topology.IsInducing (Sum.elim f g) ↔
    Topology.IsInducing f ∧
      Topology.IsInducing g ∧
        Disjoint (closure (Set.range f)) (Set.range g) ∧ Disjoint (Set.range f) (closure (Set.range g))
-- Mathlib.Topology.Category.TopCat.OpenNhds
/-- The type of open neighbourhoods of a point `x` in a (bundled) topological space.  -/
TopologicalSpace.OpenNhds : {X : TopCat} → ↑X → Type u
-- Mathlib.Condensed.Epi
CondensedSet.epi_iff_surjective_on_stonean : ∀ {X Y : CondensedSet} (f : X ⟶ Y),
  CategoryTheory.Epi f ↔
    ∀ (S : Stonean), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op S.compHaus)))
-- Mathlib.Analysis.ConstantSpeed
/-- The natural parameterization of `f` on `s`, which, if `f` has locally bounded variation on `s`,
* has unit speed on `s` (by `has_unit_speed_naturalParameterization`).
* composed with `variationOnFromTo f s a`, is at distance zero from `f`
  (by `edist_naturalParameterization_eq_zero`).
 -/
naturalParameterization : {α : Type u_1} → [LinearOrder α] → {E : Type u_2} → [PseudoEMetricSpace E] → (α → E) → Set α → α → ℝ → E
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isEmpty_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insert k v).isEmpty = false
-- Mathlib.Topology.Connected.Basic
Subtype.connectedSpace : ∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α}, IsConnected s → ConnectedSpace ↑s
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.ColimitType.AddGroup : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J CommRingCat) → AddGroup (CommRingCat.Colimits.ColimitType F)
-- Mathlib.Algebra.CharP.Basic
/-- If a ring `R` is of characteristic `p`, then for any prime number `q` different from `p`,
it is not zero in `R`.  -/
CharP.cast_ne_zero_of_ne_of_prime : ∀ (R : Type u_1) [inst : NonAssocSemiring R] [Nontrivial R] {p q : ℕ} [CharP R p], Nat.Prime q → p ≠ q → ↑q ≠ 0
-- Mathlib.Tactic.Explode.Datatypes
Mathlib.Explode.Status.cintro.sizeOf_spec : sizeOf Mathlib.Explode.Status.cintro = 1
-- Mathlib.ModelTheory.Graph
FirstOrder.Language.instDecidableEqGraphRel : {a : ℕ} → DecidableEq (FirstOrder.Language.graphRel a)
-- Mathlib.NumberTheory.SmoothNumbers
Nat.smoothNumbersUpTo.eq_1 : ∀ (N k : ℕ), N.smoothNumbersUpTo k = {n ∈ Finset.range (N + 1) | n ∈ k.smoothNumbers}
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.coe_comap : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S] {F : Type u_1}
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (s : NonUnitalSubsemiring S) (f : F),
  ↑(NonUnitalSubsemiring.comap f s) = ⇑f ⁻¹' ↑s
-- Batteries.Data.List.Lemmas
/-- **Alias** of `List.rel_of_isChain_cons_cons`. -/
List.rel_of_chain_cons : ∀ {α : Type u_1} {R : α → α → Prop} {a b : α} {l : List α}, List.IsChain R (a :: b :: l) → R a b
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_replaceEntry : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α} {v : β k},
  Std.Internal.List.getKey? a (Std.Internal.List.replaceEntry k v l) =
    if Std.Internal.List.containsKey k l = true ∧ (k == a) = true then some k else Std.Internal.List.getKey? a l
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
SimpleGraph.instDecidableIsUniform : {α : Type u_1} →
  {𝕜 : Type u_2} →
    [inst : Field 𝕜] →
      [inst_1 : LinearOrder 𝕜] →
        (G : SimpleGraph α) → [inst_2 : DecidableRel G.Adj] → (ε : 𝕜) → (s t : Finset α) → Decidable (G.IsUniform ε s t)
-- Mathlib.Analysis.Convex.Star
starConvex_singleton : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] (x : E), StarConvex 𝕜 x {x}
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.closure_insert : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] (s : Set M) (m : M),
  (FirstOrder.Language.Substructure.closure L).toFun (insert m s) =
    (FirstOrder.Language.Substructure.closure L).toFun {m} ⊔ (FirstOrder.Language.Substructure.closure L).toFun s
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.mk.injEq : ∀ {α : Type u} [inst : UniformSpace α] (space : Type v) (coe : α → space) (uniformStruct : UniformSpace space)
  (complete : CompleteSpace space) (separation : T0Space space) (isUniformInducing : IsUniformInducing coe)
  (dense : DenseRange coe) (space_1 : Type v) (coe_1 : α → space_1) (uniformStruct_1 : UniformSpace space_1)
  (complete_1 : CompleteSpace space_1) (separation_1 : T0Space space_1) (isUniformInducing_1 : IsUniformInducing coe_1)
  (dense_1 : DenseRange coe_1),
  ({ space := space, coe := coe, uniformStruct := uniformStruct, complete := complete, separation := separation,
        isUniformInducing := isUniformInducing, dense := dense } =
      { space := space_1, coe := coe_1, uniformStruct := uniformStruct_1, complete := complete_1,
        separation := separation_1, isUniformInducing := isUniformInducing_1, dense := dense_1 }) =
    (space = space_1 ∧ coe ≍ coe_1 ∧ uniformStruct ≍ uniformStruct_1)
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciSup_le' : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrderBot α] {f : ι → α} {a : α},
  (∀ (i : ι), f i ≤ a) → ⨆ i, f i ≤ a
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.isCDotTac : Lean.TSyntax `tactic → Bool
-- Init.Data.Array.Monadic
_private.Init.Data.Array.Monadic.0.Array.forIn'_eq_foldlM.match_1.eq_2 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.yield b))
  (h_2 : (b : β) → motive (ForInStep.done b)),
  (match ForInStep.done b with
    | ForInStep.yield b => h_1 b
    | ForInStep.done b => h_2 b) =
    h_2 b
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
Group.isCyclic_of_coprime_card_ker : ∀ {M : Type u_4} {N : Type u_5} [inst : CommGroup M] [inst_1 : Group N] (f : M →* N),
  (Nat.card ↥f.ker).Coprime (Nat.card N) → ∀ [IsCyclic ↥f.ker] [hN : IsCyclic N], Function.Surjective ⇑f → IsCyclic M
-- Std.Async.Signal
Std.Async.Signal.sigvtalrm.sizeOf_spec : sizeOf Std.Async.Signal.sigvtalrm = 1
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars_hom_apply : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) {X : ModuleCat R}
  {Y : ModuleCat S} (g : X ⟶ (ModuleCat.restrictScalars f).obj Y)
  (z : TensorProduct R ↑((ModuleCat.restrictScalars f).obj (ModuleCat.of S S)) ↑X),
  (ModuleCat.Hom.hom (ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars f g)) z =
    (TensorProduct.lift
        { toFun := fun s => ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g, map_add' := ⋯, map_smul' := ⋯ })
      z
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- `LinearMapClass F R M M₂` asserts `F` is a type of bundled `R`-linear maps `M → M₂`.

This is an abbreviation for `SemilinearMapClass F (RingHom.id R) M M₂`.
 -/
LinearMapClass : (F : Type u_14) →
  (R : outParam (Type u_15)) →
    (M : Type u_16) →
      (M₂ : Type u_17) →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid M₂] → [Module R M] → [Module R M₂] → [FunLike F M M₂] → Prop
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.homInhabited : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → (X : AlgebraicGeometry.PresheafedSpace C) → Inhabited (X.Hom X)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- `AddRightCancel` instance for `type` if available.  -/
Lean.Meta.Grind.Arith.CommRing.CommSemiring.addRightCancelInst? : Lean.Meta.Grind.Arith.CommRing.CommSemiring → Option (Option Lean.Expr)
-- Mathlib.RingTheory.Multiplicity
FiniteMultiplicity.pow : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α] {p a : α},
  Prime p → FiniteMultiplicity p a → ∀ {k : ℕ}, FiniteMultiplicity p (a ^ k)
-- Mathlib.Algebra.Field.ULift
ULift.instNNRatCast : {α : Type u} → [NNRatCast α] → NNRatCast (ULift.{u_1, u} α)
-- Mathlib.Data.Prod.Lex
Ord.lex_eq : ∀ {α : Type u_1} {β : Type u_2} [oα : Ord α] [oβ : Ord β], oα.lex oβ = Prod.Lex.instOrdLexProd
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.setLIntegral_paramSet_exp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {n : ℕ},
  0 < n →
    ∫⁻ (x : NumberField.mixedEmbedding.realSpace K) in NumberField.mixedEmbedding.fundamentalCone.paramSet K,
        ENNReal.ofReal (Real.exp (x NumberField.Units.dirichletUnitTheorem.w₀ * ↑n)) =
      (↑n)⁻¹
-- Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
CategoryTheory.ObjectProperty.IsVerdierLeftLocalizing.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B : CategoryTheory.ObjectProperty C},
  (∀ {X Y : C} (f : X ⟶ Y), A X → B Y → ∃ Z a b, A Z ∧ B Z ∧ CategoryTheory.CategoryStruct.comp a b = f) →
    A.IsVerdierLeftLocalizing B
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- If three points are not collinear, the first and third are different.  -/
ne₁₃_of_not_collinear : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p₁ p₂ p₃ : P}, ¬Collinear k {p₁, p₂, p₃} → p₁ ≠ p₃
-- Mathlib.Algebra.Group.Basic
zero_sub_add_eq_sub : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b : α), 0 - a + b = b - a
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
AbstractSimplicialComplex.instCompleteSemilatticeInf : {ι : Type u_1} → CompleteSemilatticeInf (AbstractSimplicialComplex ι)
-- Mathlib.Order.Bounds.Image
AntitoneOn.mem_lowerBounds_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s t : Set α} {a : α},
  AntitoneOn f t → s ⊆ t → a ∈ upperBounds s → a ∈ t → f a ∈ lowerBounds (f '' s)
-- Mathlib.Topology.Separation.CompletelyRegular
T35Space.toCompletelyRegularSpace : ∀ {X : Type u} {inst : TopologicalSpace X} [self : T35Space X], CompletelyRegularSpace X
-- Mathlib.Order.Bounded
Set.bounded_lt_inter_le : ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α] (a : α),
  Set.Bounded (fun x1 x2 => x1 < x2) (s ∩ {b | a ≤ b}) ↔ Set.Bounded (fun x1 x2 => x1 < x2) s
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.erase_dup_rhs.inj : ∀ {c c_1 : Lean.Meta.Grind.AC.EqCnstr},
  Lean.Meta.Grind.AC.EqCnstrProof.erase_dup_rhs c = Lean.Meta.Grind.AC.EqCnstrProof.erase_dup_rhs c_1 → c = c_1
-- Init.Data.Char.Basic
Char.instLT : LT Char
-- Lean.Meta.GeneralizeTelescope
Lean.Meta.GeneralizeTelescope.Entry.mk : Lean.Expr → Lean.Expr → Bool → Lean.Meta.GeneralizeTelescope.Entry
-- Mathlib.RingTheory.IsTensorProduct
IsTensorProduct.equiv_symm_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (h : IsTensorProduct f) (x₁ : M₁) (x₂ : M₂),
  h.equiv.symm ((f x₁) x₂) = x₁ ⊗ₜ[R] x₂
-- Mathlib.Order.Interval.Set.Basic
Set.Iio_inter_Ici : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Iio a ∩ Set.Ici b = Set.Ico b a
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso_hom_app_hom_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : CategoryTheory.CommMon C),
  ((CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso C).hom.app X).hom.hom =
    CategoryTheory.CategoryStruct.id X.X
-- Mathlib.Algebra.Order.CompleteField
/-- **Alias** of `ConditionallyCompleteLinearOrderedField.inducedOrderRingHom`.

---

`inducedMap` as an `OrderRingHom`.  -/
LinearOrderedField.inducedOrderRingHom : (α : Type u_2) →
  (β : Type u_3) →
    [inst : Field α] →
      [inst_1 : LinearOrder α] →
        [IsStrictOrderedRing α] →
          [inst_3 : Field β] →
            [inst_4 : ConditionallyCompleteLinearOrder β] → [IsStrictOrderedRing β] → [Archimedean α] → α →+*o β
-- Mathlib.RingTheory.WittVector.Defs
WittVector.constantCoeff_wittMul : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ), MvPolynomial.constantCoeff (WittVector.wittMul p n) = 0