mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Linter.TextBased.UnicodeLinter
/-- If `false`, the character is not allowed in Mathlib.

Implemented using an allowlist consisting of:
- certain ASCII characters
- certain emojis (`emojis`)
- certain non-emoji variants of emojifiable characters (`nonEmojis`)
- certain characters with no selector restrictions (`unrestricted`)
- characters with abbreviations in the VSCode extension (`withVSCodeAbbrev`)
- "the rest" (`othersInMathlib`)

Note: if `true`, a character might still not be allowed depending on context
(e.g. misplaced variant selectors).
 -/
Mathlib.Linter.TextBased.UnicodeLinter.isAllowedCharacter : Char → Bool
-- Mathlib.FieldTheory.Finite.Basic
pow_pow_modEq_one : ∀ (p m a : ℕ), (1 + p * a) ^ p ^ m ≡ 1 [MOD p ^ m]
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.mk.sizeOf_spec : ∀ {α : Type u_2} [inst : SizeOf α] (toFilter : Filter α) (neBot' : toFilter.NeBot)
  (le_of_le : ∀ (g : Filter α), g.NeBot → g ≤ toFilter → toFilter ≤ g),
  sizeOf { toFilter := toFilter, neBot' := neBot', le_of_le := le_of_le } = 1 + sizeOf toFilter + sizeOf neBot'
-- Mathlib.LinearAlgebra.Determinant
LinearMap.det_eq_one_of_subsingleton : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Subsingleton M]
  (f : M →ₗ[R] M), LinearMap.det f = 1
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
/-- The odd elliptic relator `ER(m + 1, m, 1, 0)` for `m ∈ ℤ`.  -/
IsEllipticNet.rel_odd : ∀ {R : Type u_1} [inst : CommRing R] (W : ℤ → R) (m : ℤ),
  IsEllipticNet.rel W (m + 1) m 1 0 = W (2 * m + 1) * W 1 ^ 3 - W (m + 2) * W m ^ 3 + W (m - 1) * W (m + 1) ^ 3
-- Mathlib.Logic.Equiv.Defs
/-- Transfer `LE` across an `Equiv`.  -/
Equiv.le : {α : Type u_1} → {β : Type u_2} → α ≃ β → [LE β] → LE α
-- Mathlib.Order.Category.BddLat
_private.Mathlib.Order.Category.BddLat.0.BddLat.Hom.mk.injEq : ∀ {X Y : BddLat} (hom' hom'_1 : BoundedLatticeHom ↑X.toLat ↑Y.toLat),
  ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Init.Data.Nat.Basic
Nat.not_le_of_gt : ∀ {n m : ℕ}, n > m → ¬n ≤ m
-- Mathlib.RingTheory.PowerSeries.PiTopology
/-- Coefficients are continuous  -/
PowerSeries.WithPiTopology.continuous_coeff : ∀ (R : Type u_1) [inst : TopologicalSpace R] [inst_1 : Semiring R] (d : ℕ), Continuous ⇑(PowerSeries.coeff d)
-- Mathlib.Algebra.Group.Int.Units
Int.isUnit_mul_self : ∀ {u : ℤ}, IsUnit u → u * u = 1
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinitePos_abs_iff_infinite_abs : ∀ {x : ℝ*}, |x|.InfinitePos ↔ |x|.Infinite
-- Mathlib.Algebra.Lie.Weights.Basic
/-- A weight of a Lie module is a map `L → R` such that the corresponding weight space is
non-trivial.  -/
LieModule.Weight : (R : Type u_2) →
  (L : Type u_3) →
    (M : Type u_4) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] → [LieModule R L M] → [LieRing.IsNilpotent L] → Type (max u_2 u_3)
-- Mathlib.Topology.EMetricSpace.Defs
/-- Characterize the equality of points by the vanishing of their extended distance  -/
edist_eq_zero : ∀ {γ : Type w} [inst : EMetricSpace γ] {x y : γ}, edist x y = 0 ↔ x = y
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
TensorAlgebra.ι_ne_one : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial R]
  (x : M), (TensorAlgebra.ι R) x ≠ 1
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.Hom.ext_iff : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {X Y : SheafOfModules R} {x y : X.Hom Y}, x = y ↔ x.val = y.val
-- Mathlib.AlgebraicGeometry.Sites.Proetale
AlgebraicGeometry.Scheme.ProEt.topology_eq_inducedTopology : ∀ (S : AlgebraicGeometry.Scheme),
  AlgebraicGeometry.Scheme.ProEt.topology S =
    (AlgebraicGeometry.Scheme.ProEt.forget S).inducedTopology (AlgebraicGeometry.Scheme.proetaleTopology.over S)
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- The action map  -/
CategoryTheory.MonObj.termγ : Lean.ParserDescr
-- Mathlib.Analysis.Matrix.LDL
LDL.lower.eq_1 : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : LinearOrder n] [inst_2 : WellFoundedLT n]
  [inst_3 : LocallyFiniteOrderBot n] {S : Matrix n n 𝕜} [inst_4 : Fintype n] (hS : S.PosDef),
  LDL.lower hS = (LDL.lowerInv hS)⁻¹
-- Mathlib.Tactic.CrossRefAttribute
/-- `addTagEntry declName db tag comment` records a cross-reference for `declName` in `tagExt`.  -/
Mathlib.CrossRef.addTagEntry : {m : Type → Type} → [Lean.MonadEnv m] → Lean.Name → Mathlib.CrossRef.Database → String → String → m Unit
-- Mathlib.Topology.Closure
interior_eq_univ : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, interior s = Set.univ ↔ s = Set.univ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.inl_isoIsPushout_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z : C} (X Y : C) {P : C} {f : Z ⟶ X} {g : Z ⟶ Y}
  {inl : X ⟶ P} {inr : Y ⟶ P} {P' : C} {inl' : X ⟶ P'} {inr' : Y ⟶ P'} (h : CategoryTheory.IsPushout f g inl inr)
  (h' : CategoryTheory.IsPushout f g inl' inr'),
  CategoryTheory.CategoryStruct.comp inl (CategoryTheory.IsPushout.isoIsPushout X Y h h').hom = inl'
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
spinGroup.units_mem_lipschitzGroup : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {x : (CliffordAlgebra Q)ˣ}, ↑x ∈ spinGroup Q → x ∈ lipschitzGroup Q
-- Mathlib.Topology.Baire.Lemmas
/-- A property holds on a residual (comeagre) set if and only if it holds on some dense `Gδ` set.  -/
eventually_residual : ∀ {X : Type u_1} [inst : TopologicalSpace X] [BaireSpace X] {p : X → Prop},
  (∀ᶠ (x : X) in residual X, p x) ↔ ∃ t, IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.isOpenImmersion_fromSpec : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U),
  AlgebraicGeometry.IsOpenImmersion hU.fromSpec
-- Mathlib.Order.WellQuasiOrder
WellQuasiOrdered.of_surjective : ∀ {α : Type u_3} {β : Type u_4} {r : α → α → Prop} {s : β → β → Prop},
  WellQuasiOrdered r → ∀ (f : r →r s), Function.Surjective ⇑f → WellQuasiOrdered s
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew?_snd : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) {k : α}
  {v : β}, (Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew? m k v).2 = m.insertIfNew k v
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.instPreorderAbs : {α : Type u_1} →
  [inst : Field α] → [inst_1 : LinearOrder α] → [inst_2 : IsStrictOrderedRing α] → Preorder (CauSeq α abs)
-- Std.Data.HashSet.Lemmas
Std.HashSet.contains_eq_isSome_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {a : α},
  m.contains a = (m.get? a).isSome
-- Batteries.Control.LawfulMonadState
LawfulMonadStateOf.getModify_id : ∀ {σ : Type u_2} {m : Type u_2 → Type u_1} [inst : Monad m] [inst_1 : MonadStateOf σ m] [LawfulMonadStateOf σ m],
  getModify id = get
-- Init.Data.SInt.Lemmas
Int8.toInt_maxValue : Int8.maxValue.toInt = 2 ^ 7 - 1
-- Mathlib.Topology.EMetricSpace.Defs
/-- ε-characterization of the closure in pseudoemetric spaces  -/
EMetric.mem_closure_iff : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s : Set α}, x ∈ closure s ↔ ∀ ε > 0, ∃ y ∈ s, edist x y < ε
-- Mathlib.CategoryTheory.Center.Linear
/-- The scalar multiplication by `R` on the type `X ⟶ Y` of morphisms in
a category `C` equipped with a ring morphism `R →+* CatCenter C`.  -/
CategoryTheory.Linear.smulOfRingMorphism : {R : Type w} →
  [inst : Ring R] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Preadditive C] → (R →+* CategoryTheory.CatCenter C) → (X Y : C) → SMul R (X ⟶ Y)
-- Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
Multiset.prod_nonneg : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [inst_1 : PartialOrder R] [ZeroLEOneClass R] [PosMulMono R]
  {s : Multiset R}, (∀ a ∈ s, 0 ≤ a) → 0 ≤ s.prod
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
/-- The leading term of a multivariate polynomial with respect to a monomial ordering.  -/
MonomialOrder.leadingTerm : {σ : Type u_1} → MonomialOrder σ → {R : Type u_2} → [inst : CommSemiring R] → MvPolynomial σ R → MvPolynomial σ R
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.RingCompare.mk.inj : ∀ {u : Lean.Level} {α : Q(Type u)} {BaseType : Q(«$α») → Type} {eq : {x y : Q(«$α»)} → BaseType x → BaseType y → Bool}
  {compare : {x y : Q(«$α»)} → BaseType x → BaseType y → Ordering}
  {eq_1 : {x y : Q(«$α»)} → BaseType x → BaseType y → Bool}
  {compare_1 : {x y : Q(«$α»)} → BaseType x → BaseType y → Ordering},
  { eq := eq, compare := compare } = { eq := eq_1, compare := compare_1 } → eq = eq_1 ∧ compare = compare_1
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.subSchemeCover_map_inclusion_assoc : ∀ {X : AlgebraicGeometry.Scheme} {I J : X.IdealSheafData} (h : I ≤ J) (U : J.subschemeCover.I₀)
  {Z : AlgebraicGeometry.Scheme} (h_1 : I.subscheme ⟶ Z),
  CategoryTheory.CategoryStruct.comp (J.subschemeCover.f U)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.IdealSheafData.inclusion h) h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom h U)
        (I.subschemeCover.f U))
      h_1
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.admissibleIndex.eq_1 : ∀ {ι : Type u_1} (n : ℕ) [inst : NeZero n] [inst_1 : Fintype ι] (B : BoxIntegral.Box ι),
  BoxIntegral.unitPartition.admissibleIndex n B = ⋯.toFinset
-- Mathlib.RingTheory.Coalgebra.Convolution
/-- Non-unital convolution ring structure on linear maps from a coalgebra to a
non-unital algebra.  -/
LinearMap.convNonUnitalRing : {R : Type u_1} →
  {A : Type u_3} →
    {C : Type u_5} →
      [inst : CommSemiring R] →
        [inst_1 : NonUnitalRing A] →
          [inst_2 : AddCommMonoid C] →
            [inst_3 : Module R A] →
              [SMulCommClass R A A] →
                [IsScalarTower R A A] → [inst_6 : Module R C] → [Coalgebra R C] → NonUnitalRing (WithConv (C →ₗ[R] A))
-- Mathlib.Algebra.Lie.DirectSum
DirectSum.lie_module_bracket_apply : ∀ {ι : Type v} {L : Type w₁} {M : ι → Type w} [inst : LieRing L] [inst_1 : (i : ι) → AddCommGroup (M i)]
  [inst_2 : (i : ι) → LieRingModule L (M i)] (x : L) (m : DirectSum ι fun i => M i) (i : ι), ⁅x, m⁆ i = ⁅x, m i⁆
-- Mathlib.Algebra.Group.Pi.Basic
Pi.subNegZeroMonoid : {I : Type u} → {f : I → Type v₁} → [(i : I) → SubNegZeroMonoid (f i)] → SubNegZeroMonoid ((i : I) → f i)
-- Mathlib.Algebra.Order.Module.Defs
smul_nonpos_of_nonpos_of_nonneg : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β]
  [inst_3 : Preorder α] [inst_4 : Preorder β] [SMulPosMono α β], a ≤ 0 → 0 ≤ b → a • b ≤ 0
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.equivIoc.eq_1 : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜) [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [hp : Fact (0 < p)] (a : 𝕜) [inst_3 : Archimedean 𝕜], AddCircle.equivIoc p a = QuotientAddGroup.equivIocMod ⋯ a
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_eq_getD_default : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {a : α}, t.get! a = t.getD a default
-- Mathlib.Tactic.ReduceModChar
/-- Reduce all numeric subexpressions of `e` modulo their characteristic.

Use `derive (expensive := true)` to do more work in finding the characteristic of
the type of `e`.
 -/
Tactic.ReduceModChar.derive : optParam Bool false → Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.distribMulActionHom_ext'_iff : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N]
  [inst_3 : DistribMulAction R M] [inst_4 : DistribMulAction R N] {α : Type u_6} {f g : SkewMonoidAlgebra M α →+[R] N},
  f = g ↔
    ∀ (a : α),
      f.comp (SkewMonoidAlgebra.DistribMulActionHom.single a) = g.comp (SkewMonoidAlgebra.DistribMulActionHom.single a)
-- Mathlib.Topology.Covering.Quotient
IsQuotientCoveringMap.toPermFiber.congr_simp : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : Group G] [inst_3 : MulAction G E] (hf : IsQuotientCoveringMap f G) (x : X),
  hf.toPermFiber x = hf.toPermFiber x
-- Mathlib.Order.Max
NoMinOrder.mk : ∀ {α : Type u_3} [inst : LT α], (∀ (a : α), ∃ b, b < a) → NoMinOrder α
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement'.index_eq_card : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H.IsComplement' K → K.index = Nat.card ↥H
-- Init.Data.Array.Lemmas
Array.contains_push : ∀ {α : Type u_1} [inst : BEq α] {xs : Array α} {a b : α}, (xs.push a).contains b = (xs.contains b || b == a)
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.prodMkRight_zero : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ}, ProbabilityTheory.Kernel.prodMkRight α 0 = 0
-- Lean.Elab.App
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.isNextOutParamOfLocalInstanceAndResult.isOutParamOf : Lean.Expr → ℕ → Array Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.toLinearEquiv_smul : ∀ {S : Type u_1} {R : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid V] [inst_3 : Module R V] [inst_4 : TopologicalSpace V] [inst_5 : Module S V]
  [inst_6 : ContinuousConstSMul S V] [inst_7 : AddCommMonoid W] [inst_8 : Module R W] [inst_9 : TopologicalSpace W]
  [inst_10 : Module S W] [inst_11 : ContinuousConstSMul S W] [inst_12 : SMulCommClass R S W] [inst_13 : SMul S R]
  [inst_14 : IsScalarTower S R V] [inst_15 : IsScalarTower S R W] (e : V ≃L[R] W) (α : Sˣ), ↑(α • e) = α • ↑e
-- Mathlib.Topology.Separation.Basic
ContinuousWithinAt.eqOn_const_closure : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T1Space Y] {f : X → Y}
  {s : Set X} {c : Y},
  (∀ x ∈ closure s, ContinuousWithinAt f s x) → Set.EqOn f (fun x => c) s → Set.EqOn f (fun x => c) (closure s)
-- Batteries.Classes.Order
Std.instLawfulOrdInt : Std.LawfulOrd ℤ
-- Mathlib.Topology.Semicontinuity.Basic
Continuous.comp_upperSemicontinuousOn_antitone : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {γ : Type u_4} [inst_1 : LinearOrder γ]
  [inst_2 : TopologicalSpace γ] [OrderTopology γ] {δ : Type u_5} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ]
  [OrderTopology δ] {g : γ → δ} {f : α → γ},
  Continuous g → UpperSemicontinuousOn f s → Antitone g → LowerSemicontinuousOn (g ∘ f) s
-- Mathlib.CategoryTheory.Quotient.Linear
/-- Assuming `Quotient r` has already been endowed with a preadditive category structure
such that `functor r : C ⥤ Quotient r` is additive, and that `C` has an `R`-linear category
structure compatible with `r`, this is the induced `R`-linear category structure on
`Quotient r`.  -/
CategoryTheory.Quotient.linear : (R : Type u_1) →
  {C : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : CategoryTheory.Category.{v_1, u_2} C] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [inst_3 : CategoryTheory.Linear R C] →
            (r : HomRel C) →
              [CategoryTheory.Congruence r] →
                (∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)) →
                  [inst_5 : CategoryTheory.Preadditive (CategoryTheory.Quotient r)] →
                    [(CategoryTheory.Quotient.functor r).Additive] → CategoryTheory.Linear R (CategoryTheory.Quotient r)
-- Lean.DocString.Parser
Lean.Doc.Parser.instBEqUnorderedListType.beq : Lean.Doc.Parser.UnorderedListType → Lean.Doc.Parser.UnorderedListType → Bool
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.face.eq_1 : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} (s : Affine.Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : fs.card = m + 1),
  s.face h = { points := s.points ∘ ⇑(fs.orderEmbOfFin h), independent := ⋯ }
-- Mathlib.Algebra.Algebra.Defs
algebraMap.coe_pow : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (a : R) (n : ℕ),
  ↑(a ^ n) = ↑a ^ n
-- Mathlib.CategoryTheory.Limits.Final
/-- If `F` is final and `F ⋙ G` creates colimits of `H`, then so does `G`.  -/
CategoryTheory.Functor.Final.createsColimitOfComp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [F.Final] →
            {E : Type u₃} →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} E] →
                {G : CategoryTheory.Functor D E} →
                  {B : Type u₄} →
                    [inst_4 : CategoryTheory.Category.{v₄, u₄} B] →
                      {H : CategoryTheory.Functor E B} →
                        [CategoryTheory.CreatesColimit (F.comp G) H] → CategoryTheory.CreatesColimit G H
-- Mathlib.Topology.Connected.TotallyDisconnected
Topology.IsEmbedding.isTotallyDisconnected_image : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α},
  Topology.IsEmbedding f → (IsTotallyDisconnected (f '' s) ↔ IsTotallyDisconnected s)
-- Init.Core
instLawfulBEqChar : LawfulBEq Char
-- Mathlib.Data.Set.Basic
Set.ofPred_and : ∀ {α : Type u} {p q : α → Prop}, {a | p a ∧ q a} = {a | p a} ∩ {a | q a}
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_diff_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → Std.DHashMap.Raw.Const.get? (m₁.diff m₂) k = Std.DHashMap.Raw.Const.get? m₁ k
-- Mathlib.Data.Set.Enumerate
Set.enumerate_eq_none_of_sel : ∀ {α : Type u_1} (sel : Set α → Option α) {s : Set α}, sel s = none → ∀ {n : ℕ}, Set.enumerate sel s n = none
-- Mathlib.RingTheory.DividedPowers.DPMorphism
/-- Given a ring homomorphism `A → B` and ideals `I ⊆ A` and `J ⊆ B` such that `I.map f ≤ J`,
this is the `A`-ideal on which `f (hI.dpow n x) = hJ.dpow n (f x)`.
See [N. Roby, *Les algèbres à puissances dividées* (Proposition 2)][Roby-1965].  -/
DividedPowers.ideal_from_ringHom : {A : Type u_3} →
  {B : Type u_4} →
    [inst : CommSemiring A] →
      [inst_1 : CommSemiring B] →
        {I : Ideal A} → {J : Ideal B} → DividedPowers I → DividedPowers J → {f : A →+* B} → Ideal.map f I ≤ J → Ideal A
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- The underlying function.

Do NOT use directly. Use the coercion instead.  -/
QuadraticMap.toFun : {R : Type u} →
  {M : Type v} →
    {N : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] → [inst_3 : AddCommMonoid N] → [inst_4 : Module R N] → QuadraticMap R M N → M → N
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.isSt_symm_real : ∀ {r s : ℝ}, (↑r).IsSt s ↔ (↑s).IsSt r
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.lineMap_apply_ring : ∀ {k : Type u_1} [inst : Ring k] (a b c : k), (AffineMap.lineMap a b) c = (1 - c) * a + c * b
-- Mathlib.Tactic.Simps.Basic
/-- A renaming rule `before→after` or
Each name comes with the syntax used to write the rule,
which is used to declare hover information.  -/
Simps.ProjectionRule.rename : Lean.Name → Lean.Syntax → Lean.Name → Lean.Syntax → Simps.ProjectionRule
-- Aesop.Frontend.Saturate
Aesop.Frontend.Parser.additionalRule : Lean.ParserDescr
-- Lean.Meta.FunInfo
_private.Lean.Meta.FunInfo.0.Lean.Meta.FunInfoEnvCacheKey.ls : Lean.Meta.FunInfoEnvCacheKey✝ → List Lean.Level
-- Lean.Elab.Declaration
/-- Given declarations such as `@[...] def Foo.Bla.f ...` return `some (Foo.Bla, @[...] def f ...)`
Remark: if the id starts with `_root_`, we return `none`.
 -/
_private.Lean.Elab.Declaration.0.Lean.Elab.Command.expandDeclNamespace? : Lean.Syntax → Lean.MacroM (Option (Lean.Name × Lean.Syntax))
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.homothety_linear : ∀ {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [inst : CommRing k] [inst_1 : AddCommGroup V1]
  [inst_2 : AddTorsor V1 P1] [inst_3 : Module k V1] (c : P1) (r : k),
  (AffineMap.homothety c r).linear = r • LinearMap.id
-- Mathlib.GroupTheory.GroupAction.Pointwise
image_smul_set : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} {F : Type u_4} [inst : SMul M α] [inst_1 : SMul M β]
  [inst_2 : FunLike F α β] [MulActionHomClass F M α β] (f : F) (c : M) (s : Set α), ⇑f '' (c • s) = c • ⇑f '' s
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.mapShortComplexH1_τ₂ : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{max u u_1, u, u} k H}
  {B : Rep.{max u u_1, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B),
  (groupCohomology.mapShortComplexH1 f φ).τ₂ = groupCohomology.cochainsMap₁ f φ
-- Mathlib.Algebra.Group.Equiv.Defs
MonoidHom.toMulEquiv_apply : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M →* N) (g : N →* M)
  (h₁ : g.comp f = MonoidHom.id M) (h₂ : f.comp g = MonoidHom.id N), ⇑(f.toMulEquiv g h₁ h₂) = ⇑f
-- Mathlib.RingTheory.Spectrum.Prime.RingHom
/-- An infinite product of nontrivial commutative semirings has a maximal ideal outside of the
range of `sigmaToPi`, i.e. is not of the form `πᵢ⁻¹(𝔭)` for some prime `𝔭 ⊂ R i`, where
`πᵢ : (Π i, R i) →+* R i` is the projection. For a complete description of all prime ideals,
see https://math.stackexchange.com/a/1563190.  -/
PrimeSpectrum.exists_maximal_notMem_range_sigmaToPi_of_infinite : ∀ {ι : Type u_3} (R : ι → Type u_2) [inst : (i : ι) → CommSemiring (R i)] [Infinite ι] [∀ (i : ι), Nontrivial (R i)],
  ∃ I, ∃ (x : I.IsMaximal), { asIdeal := I, isPrime := ⋯ } ∉ Set.range (PrimeSpectrum.sigmaToPi R)
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
/-- `Free.lift` is unique amongst `R`-linear functors `Free R C ⥤ D`
which compose with `embedding ℤ C` to give the original functor.
 -/
CategoryTheory.Free.liftUnique : (R : Type u_1) →
  [inst : CommRing R] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {D : Type u} →
          [inst_2 : CategoryTheory.Category.{v, u} D] →
            [inst_3 : CategoryTheory.Preadditive D] →
              [inst_4 : CategoryTheory.Linear R D] →
                (F : CategoryTheory.Functor C D) →
                  (L : CategoryTheory.Functor (CategoryTheory.Free R C) D) →
                    [L.Additive] →
                      [CategoryTheory.Functor.Linear R L] →
                        ((CategoryTheory.Free.embedding R C).comp L ≅ F) → (L ≅ CategoryTheory.Free.lift R F)
-- Lean.LocalContext
_private.Lean.LocalContext.0.Lean.LocalContext.getUnusedNameAux : Lean.LocalContext → Lean.Name → ℕ → Lean.Name × ℕ
-- Init.Data.String.Iterate
/-- Creates an iterator over all valid positions within `s` that are strictly smaller than
`p`, starting from the position before `p` and iterating towards the first one.
 -/
String.revPositionsFrom : (s : String) → s.Pos → Std.Iter { p // p ≠ s.endPos }
-- Lean.Elab.Tactic.Config
/-- Expands a field access into full field access like `toB.toA.x`.
Returns that and the last projection function for `x` itself.
 -/
_private.Lean.Elab.Tactic.Config.0.Lean.Elab.Tactic.expandFieldName : Lean.Name → Lean.Name → Lean.MetaM (Lean.Name × Lean.Name)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.all.eq_1 : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Std.DTreeMap.Raw α β cmp) (p : (a : α) → β a → Bool),
  t.all p = Id.run (t.inner.all p)
-- Mathlib.Order.Atoms
covBy_top_iff : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, a ⋖ ⊤ ↔ IsCoatom a