mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.map_le_iff_le_comap : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} {S : AddSubmonoid M} {T : AddSubmonoid N},
  AddSubmonoid.map f S ≤ T ↔ S ≤ AddSubmonoid.comap f T
-- Lean.Elab.Tactic.Omega.Core
/-- Whether the problem is possible.  -/
Lean.Elab.Tactic.Omega.Problem.possible : Lean.Elab.Tactic.Omega.Problem → Bool
-- Init.GrindInstances.Nat
Lean.Grind.instAddRightCancelNat : Lean.Grind.AddRightCancel ℕ
-- Std.Data.Internal.List.Associative
Std.Internal.List.interSmaller_perm_filter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] (l₁ l₂ : List ((a : α) × β a)),
  Std.Internal.List.DistinctKeys l₁ →
    (Std.Internal.List.interSmaller l₁ l₂).Perm (List.filter (fun kv => Std.Internal.List.containsKey kv.fst l₂) l₁)
-- Mathlib.SetTheory.ZFC.Rank
_private.Mathlib.SetTheory.ZFC.Rank.0.PSet.rank.match_1.splitter : (motive : PSet.{u_1} → Sort u_2) →
  (x : PSet.{u_1}) → ((α : Type u_1) → (A : α → PSet.{u_1}) → motive (PSet.mk α A)) → motive x
-- Mathlib.Order.Filter.Map
Filter.principal_bind : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → Filter β}, (Filter.principal s).bind f = ⨆ x ∈ s, f x
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.isOpenEmbedding_iff_comp_isIso : ∀ {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso g],
  Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) ↔
    Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Copy.coe_ofLE : ∀ {V : Type u_1} {G₁ G₂ : SimpleGraph V} (h : G₁ ≤ G₂), ⇑(SimpleGraph.Copy.ofLE G₁ G₂ h) = id
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.Semiring.mk : ℕ →
  Lean.Expr →
    Lean.Level →
      Lean.Expr →
        Option Lean.Expr →
          Option Lean.Expr →
            Option Lean.Expr →
              Option Lean.Expr →
                Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Grind.Arith.CommRing.SemiringExpr →
                  Lean.PArray Lean.Expr →
                    Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Grind.CommRing.Var →
                      Lean.Meta.Grind.Arith.CommRing.Semiring
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
CauchySeq.add : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3}
  [inst_3 : Preorder ι] {u v : ι → α}, CauchySeq u → CauchySeq v → CauchySeq (u + v)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RooSliceData.range : {α : Type u} → [inst : Ord α] → Std.DTreeMap.Internal.Unit.RooSliceData α → Std.Roo α
-- Init.Meta.Defs
/-- Return the first atom/identifier that has position information  -/
Lean.Syntax.getHead? : Lean.Syntax → Option Lean.Syntax
-- Mathlib.RingTheory.MvPolynomial.Tower
MvPolynomial.aeval_algebraMap_eq_zero_iff : ∀ {R : Type u_1} {A : Type u_2} (B : Type u_3) {σ : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : CommSemiring B] [inst_3 : Algebra R A] [inst_4 : Algebra A B] [inst_5 : Algebra R B] [IsScalarTower R A B]
  [IsDomain A] [Module.IsTorsionFree A B] [Nontrivial B] (x : σ → A) (p : MvPolynomial σ R),
  (MvPolynomial.aeval (⇑(algebraMap A B) ∘ x)) p = 0 ↔ (MvPolynomial.aeval x) p = 0
-- Mathlib.Geometry.Euclidean.MongePoint
_private.Mathlib.Geometry.Euclidean.MongePoint.0.Affine.Simplex.mongePointWeightsWithCircumcenter.match_1.eq_1 : ∀ (n : ℕ) (motive : Affine.Simplex.PointsWithCircumcenterIndex (n + 2) → Sort u_1) (a : Fin (n + 2 + 1))
  (h_1 : (a : Fin (n + 2 + 1)) → motive (Affine.Simplex.PointsWithCircumcenterIndex.pointIndex a))
  (h_2 : Unit → motive Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndex),
  (match Affine.Simplex.PointsWithCircumcenterIndex.pointIndex a with
    | Affine.Simplex.PointsWithCircumcenterIndex.pointIndex a => h_1 a
    | Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndex => h_2 ()) =
    h_1 a
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.div_eq_iff : ∀ {α : Type u} [inst : DivisionMonoid α] {a b c : α}, IsUnit b → (a / b = c ↔ a = c * b)
-- Batteries.Logic
/-- **Alias** of the forward direction of `Classical.not_forall`. -/
Classical.exists_not_of_not_forall : ∀ {α : Sort u_1} {p : α → Prop}, (¬∀ (x : α), p x) → ∃ x, ¬p x
-- Mathlib.Order.Compare
/-- **Alias** of the forward direction of `Ordering.compares_swap`. -/
Ordering.Compares.of_swap : ∀ {α : Type u_1} [inst : LT α] {a b : α} {o : Ordering}, o.swap.Compares a b → o.Compares b a
-- Mathlib.Order.Interval.Finset.Fin
Fin.attachFin_Icc : ∀ {n : ℕ} (a b : Fin n), (Finset.Icc ↑a ↑b).attachFin ⋯ = Finset.Icc a b
-- Std.Sat.AIG.Relabel
Std.Sat.AIG.Decl.relabel_gate : ∀ {α β : Type} {idx : ℕ} {lhs rhs : Std.Sat.AIG.Fanin} {decls : Array (Std.Sat.AIG.Decl α)} {r : α → β}
  {hidx : idx < decls.size},
  Std.Sat.AIG.Decl.relabel r decls[idx] = Std.Sat.AIG.Decl.gate lhs rhs → decls[idx] = Std.Sat.AIG.Decl.gate lhs rhs
-- Mathlib.Algebra.Ring.Ext
NonUnitalRing.ext_iff : ∀ {R : Type u} {inst₁ inst₂ : NonUnitalRing R}, inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul
-- Mathlib.Algebra.Algebra.RestrictScalars
/-- `R ⟶ S` induces `S-Alg ⥤ R-Alg`  -/
RestrictScalars.algebra : (R : Type u_1) →
  (S : Type u_2) →
    (A : Type u_4) →
      [inst : Semiring A] →
        [inst_1 : CommSemiring S] →
          [Algebra S A] → [inst_3 : CommSemiring R] → [Algebra R S] → Algebra R (RestrictScalars R S A)
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- Projection to `ContinuousMultilinearMap`s as a bundled `AddMonoidHom`.  -/
ContinuousAlternatingMap.toMultilinearAddHom : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_4} →
      {ι : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : AddCommMonoid N] →
                  [inst_5 : Module R N] →
                    [inst_6 : TopologicalSpace N] →
                      [inst_7 : ContinuousAdd N] → M [⋀^ι]→L[R] N →+ ContinuousMultilinearMap R (fun x => M) N
-- Mathlib.RingTheory.ZMod
/-- The ring homomorphism `ℤ → ZMod n` has kernel generated by `n`.  -/
ZMod.ker_intCastRingHom : ∀ (n : ℕ), RingHom.ker (Int.castRingHom (ZMod n)) = Ideal.span {↑n}
-- Mathlib.Algebra.Lie.BaseChange
/-- If `A` is an `R`-algebra, any Lie submodule of a Lie module `M` with coefficients in `R` may be
pushed forward to a Lie submodule of `A ⊗ M` with coefficients in `A`.

This "base change" operation is also known as "extension of scalars".  -/
LieSubmodule.baseChange : {R : Type u_1} →
  (A : 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] →
                    [inst_6 : LieModule R L M] →
                      [inst_7 : CommRing A] →
                        [inst_8 : Algebra R A] →
                          LieSubmodule R L M → LieSubmodule A (TensorProduct R A L) (TensorProduct R A M)
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) {S : Type u_3} [inst_2 : Field K]
  [inst_3 : CommSemiring S] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K]
  (v : IsDedekindDomain.HeightOneSpectrum R) [inst_6 : Algebra S K],
  ⇑(algebraMap S (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) =
    (fun x => { toCompletion := ↑((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation K v)).symm x) }) ∘
      ⇑(algebraMap S K)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.map_sum : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {N : Type u_3} {P : Type u_4} [inst_1 : AddCommMonoid N]
  [inst_2 : AddCommMonoid P] {H : Type u_5} [inst_3 : FunLike H N P] [AddMonoidHomClass H N P] (h : H)
  (f : SkewMonoidAlgebra k G) (g : G → k → N), h (f.sum g) = f.sum fun a b => h (g a b)
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
SimpleGraph.EdgeLabeling.get.eq_1 : ∀ {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} (C : G.EdgeLabeling K) (x y : V) (h : G.Adj x y),
  C.get x y h = C ⟨s(x, y), h⟩
-- Mathlib.Topology.Order
coinduced_bot : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, TopologicalSpace.coinduced f ⊥ = ⊥
-- Lean.Elab.Tactic.Omega.MinNatAbs
Lean.Elab.Tactic.Omega.List.nonzeroMinimum_mem : ∀ {xs : List ℕ}, Lean.Elab.Tactic.Omega.List.nonzeroMinimum xs ≠ 0 → Lean.Elab.Tactic.Omega.List.nonzeroMinimum xs ∈ xs
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.toPoly'.go.eq_2 : ∀ (coeff : ℤ) (v : Lean.Grind.Linarith.Var),
  Lean.Grind.Linarith.Expr.toPoly'.go coeff (Lean.Grind.Linarith.Expr.var v) = fun x =>
    Lean.Grind.Linarith.Poly.add coeff v x
-- Mathlib.RingTheory.Perfection
Perfection.coeffMonoidHom_pow_p : ∀ {M : Type u_1} [inst : CommMonoid M] {p : ℕ} (f : Perfection M p) (n : ℕ),
  (Perfection.coeffMonoidHom M p (n + 1)) (f ^ p) = (Perfection.coeffMonoidHom M p n) f
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensor_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C × C}
  (f : X ⟶ Y),
  (CategoryTheory.MonoidalCategory.tensor C).map f = CategoryTheory.MonoidalCategoryStruct.tensorHom f.1 f.2
-- Init.Core
DoResultPR.pure.injEq : ∀ {α β σ : Type u} (a : α) (a_1 : σ) (a_2 : α) (a_3 : σ),
  (DoResultPR.pure a a_1 = DoResultPR.pure a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.CategoryTheory.Sites.PreservesSheafification
CategoryTheory.GrothendieckTopology.instPreservesSheafificationForgetOfPreservesLimitsOfHasColimitsOfShapeOfPreservesColimitsOfShapeOppositeCoverOfHasLimitsOfShapeWalkingMulticospanOfReflectsIsomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_3}
  [inst_1 : CategoryTheory.Category.{max v u, u_3} D] {FD : D → D → Type u_4} {CD : D → Type (max v u)}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [inst_3 : CategoryTheory.ConcreteCategory D FD]
  [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)]
  [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)]
  [∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D]
  [(CategoryTheory.forget D).ReflectsIsomorphisms], J.PreservesSheafification (CategoryTheory.forget D)
-- Mathlib.Tactic.NormNum.Prime
Mathlib.Meta.NormNum.isNat_minFac_3 : ∀ {n n' : ℕ} (k : ℕ),
  Mathlib.Meta.NormNum.IsNat n n' →
    Mathlib.Meta.NormNum.MinFacHelper n' k → 0 = n' % k → Mathlib.Meta.NormNum.IsNat n.minFac k
-- Mathlib.AlgebraicGeometry.StructureSheaf
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.localizationToStalk_stalkToFiberRingHom_assoc : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) {Z : ModuleCat R}
  (h : ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.localizationtoStalkₗ✝ R M x)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.stalkToLocalizationₗ✝ R M x) h) =
    h
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- For an endomorphism of a Noetherian module, the maximal eigenspace is always of the form kernel
`(f - μ • id) ^ k` for some `k`.  -/
Module.End.genEigenspace_top_eq_maxUnifEigenspaceIndex : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsNoetherian R M]
  (f : Module.End R M) (μ : R), (f.genEigenspace μ) ⊤ = (f.genEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ)
-- Mathlib.Data.Seq.Computation
Computation.mem_promises : ∀ {α : Type u} {s : Computation α} {a : α}, a ∈ s → s.Promises a
-- Aesop.Tree.Data
Aesop.Goal.postNormGoal? : Aesop.Goal → Option Lean.MVarId
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.liftAux_tmul : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7}
  {N : Type u_8} {P₂ : Type u_17} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : AddCommMonoid P₂]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R₂ P₂] (f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂) (m : M) (n : N),
  (TensorProduct.liftAux f') (m ⊗ₜ[R] n) = (f' m) n
-- Lean.Parser.Syntax
Lean.Parser.Command.syntaxCat.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.pow_mem : ∀ {G : Type u_1} [inst : Group G] (K : Subgroup G) {x : G}, x ∈ K → ∀ (n : ℕ), x ^ n ∈ K
-- Lean.Server.AsyncList
Lean.AsyncList.getFinishedPrefixWithConsistentLatency : {ε α : Type} →
  Lean.AsyncList ε α → UInt32 → optParam (List (Lean.Server.ServerTask Unit)) [] → BaseIO (List α × Option ε × Bool)
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.bind₂_C_left : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R],
  MvPolynomial.bind₂ MvPolynomial.C = RingHom.id (MvPolynomial σ R)
-- Mathlib.Data.Holor
Holor.mul_assoc : ∀ {α : 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)
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.leadingCoeff_zero : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R], m.leadingCoeff 0 = 0
-- Mathlib.Topology.Instances.Real.Lemmas
/-- A continuous, periodic function is bounded.  -/
Function.Periodic.isBounded_of_continuous : ∀ {α : Type u} [inst : PseudoMetricSpace α] {f : ℝ → α} {c : ℝ},
  Function.Periodic f c → c ≠ 0 → Continuous f → Bornology.IsBounded (Set.range f)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.isSome_get?_iff_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α}, (Std.ExtDHashMap.Const.get? m a).isSome = true ↔ a ∈ m
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.map_id : ∀ {V : Type u} {G : SimpleGraph V} (H : G.Subgraph), SimpleGraph.Subgraph.map SimpleGraph.Hom.id H = H
-- Lean.Elab.MutualInductive
Lean.Elab.Command.ComputedFieldView.fieldId : Lean.Elab.Command.ComputedFieldView → Lean.Name
-- Mathlib.Order.Minimal
maximal_iff : ∀ {α : Type u_2} {P : α → Prop} {x : α} [inst : PartialOrder α], Maximal P x ↔ P x ∧ ∀ ⦃y : α⦄, P y → x ≤ y → x = y
-- Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
CategoryTheory.IsSplitCoequalizer.map_leftSection : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X Y : C} {f g : X ⟶ Y} {Z : C} {π : Y ⟶ Z} (q : CategoryTheory.IsSplitCoequalizer f g π)
  (F : CategoryTheory.Functor C D), (q.map F).leftSection = F.map q.leftSection
-- Mathlib.Algebra.BigOperators.Finprod
finsum_emb_domain : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] (f : α ↪ β)
  [inst_1 : DecidablePred fun x => x ∈ Set.range ⇑f] (g : α → M),
  (∑ᶠ (b : β), if h : b ∈ Set.range ⇑f then g (Classical.choose h) else 0) = ∑ᶠ (a : α), g a
-- Mathlib.Order.Directed
directedOn_onFun_iff : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {f : β → α} {s : Set β},
  DirectedOn (Function.onFun r f) s ↔ DirectedOn r (f '' s)
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.map.eq_1 : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {S : Type u_1}
  [inst_3 : CommRing S] (f : R →+* S), Matrix.GeneralLinearGroup.map f = Units.map ↑f.mapMatrix
-- Mathlib.Data.PFunctor.Multivariate.M
MvPFunctor.M.Path.child.inj : ∀ {n : ℕ} {P : MvPFunctor.{u} (n + 1)} {x : P.last.M} {a : P.A} {f : P.last.B a → P.last.M} {h : x.dest = ⟨a, f⟩}
  {j : P.last.B a} {i : Fin2 n} {c : MvPFunctor.M.Path P (f j) i} {a_1 : P.A} {f_1 : P.last.B a_1 → P.last.M}
  {h_1 : x.dest = ⟨a_1, f_1⟩} {j_1 : P.last.B a_1} {c_1 : MvPFunctor.M.Path P (f_1 j_1) i},
  MvPFunctor.M.Path.child x a f h j i c = MvPFunctor.M.Path.child x a_1 f_1 h_1 j_1 i c_1 →
    a = a_1 ∧ f ≍ f_1 ∧ j ≍ j_1 ∧ c ≍ c_1
-- Mathlib.Data.Set.Lattice.Image
Set.prod_eq_biUnion_right : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β}, s ×ˢ t = ⋃ b ∈ t, (fun a => (a, b)) '' s
-- Mathlib.ModelTheory.Semantics
/-- A bounded formula can be evaluated as true or false by giving values to each free and bound
variable.  -/
FirstOrder.Language.BoundedFormula.Realize : {L : FirstOrder.Language} →
  {M : Type w} → [L.Structure M] → {α : Type u'} → {l : ℕ} → L.BoundedFormula α l → (α → M) → (Fin l → M) → Prop
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
/-- `pinGroup Q` forms a group where the inverse is `star`.  -/
pinGroup.instGroupSubtypeCliffordAlgebraMemSubmonoid : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {Q : QuadraticForm R M} → Group ↥(pinGroup Q)
-- Std.Do.PredTrans
Std.Do.PredTrans.instMonad : {ps : Std.Do.PostShape} → Monad (Std.Do.PredTrans ps)
-- Lean.Server.FileWorker.ExampleHover
/-- Splits a string into lines, preserving newline characters.
 -/
_private.Lean.Server.FileWorker.ExampleHover.0.Lean.Server.FileWorker.Hover.lines : String → Array String
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackComparison_comp_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_2 : CategoryTheory.Limits.HasPullback f g] [inst_3 : CategoryTheory.Limits.HasPullback (G.map f) (G.map g)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackComparison G f g)
      (CategoryTheory.Limits.pullback.snd (G.map f) (G.map g)) =
    G.map (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.Topology.Algebra.Module.Star
continuous_skewAdjointPart : ∀ (R : Type u_1) (A : Type u_2) [inst : Semiring R] [inst_1 : StarMul R] [inst_2 : TrivialStar R]
  [inst_3 : AddCommGroup A] [inst_4 : Module R A] [inst_5 : StarAddMonoid A] [inst_6 : StarModule R A]
  [inst_7 : Invertible 2] [inst_8 : TopologicalSpace A] [ContinuousSub A] [ContinuousStar A] [ContinuousConstSMul R A],
  Continuous ⇑(skewAdjointPart R)
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.anyTR.loop.eq_def : ∀ (n : ℕ) (f : (i : ℕ) → i < n → Bool) (i : ℕ) (a : i ≤ n),
  Nat.anyTR.loop✝ n f i a =
    match i, a with
    | 0, h => false
    | m.succ, h => f (n - m.succ) ⋯ || Nat.anyTR.loop✝ n f m ⋯
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.π_comp_isoHomology_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g}
  {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf)
  (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt}
  (fac :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) =
      CategoryTheory.CategoryStruct.comp π ι)
  [inst_2 : CategoryTheory.Epi π] [inst_3 : CategoryTheory.Mono ι] {Z : C} (h : S.homology ⟶ Z),
  CategoryTheory.CategoryStruct.comp π
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology S hkf hcc fac).hom h) =
    CategoryTheory.CategoryStruct.comp (S.isoCyclesOfIsLimit hkf).hom (CategoryTheory.CategoryStruct.comp S.homologyπ h)
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.rightUnitor_comp_inv_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c) {Z : a ⟶ c}
  (h :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id c) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.comp f g)).inv h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.rightUnitor g).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.id c)).inv h)
-- Mathlib.Order.Heyting.Basic
Function.Injective.coheytingAlgebra.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Max α] [inst_2 : LE α] [inst_3 : LT α] [inst_4 : Bot α]
  [inst_5 : Top α] [inst_6 : HNot α] [inst_7 : SDiff α] [inst_8 : CoheytingAlgebra β] (f : α → β)
  (hf : Function.Injective f) (le : ∀ {y x : α}, f y ≤ f x ↔ y ≤ x) (lt : ∀ {y x : α}, f y < f x ↔ y < x)
  (map_inf : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_sup : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) (map_bot : f ⊤ = ⊤)
  (map_top : f ⊥ = ⊥) (map_compl : ∀ (a : α), f (￢a) = ￢f a) (map_himp : ∀ (b a : α), f (b \ a) = f b \ f a),
  Function.Injective.coheytingAlgebra f hf le lt map_inf map_sup map_bot map_top map_compl map_himp =
    {
      toGeneralizedCoheytingAlgebra :=
        Function.Injective.generalizedCoheytingAlgebra f hf ⋯ ⋯ map_inf map_sup map_top ⋯,
      toTop := inst_5, le_top := ⋯, toHNot := inst_6, top_sdiff := ⋯ }
-- ProofWidgets.Presentation.Expr
ProofWidgets.instRpcEncodableGetExprPresentationsParams : Lean.Server.RpcEncodable ProofWidgets.GetExprPresentationsParams
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.smul_basis_mul_C : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} (y p q : Polynomial R),
  (p • 1 + q • (WeierstrassCurve.Affine.CoordinateRing.mk W') Polynomial.X) *
      (WeierstrassCurve.Affine.CoordinateRing.mk W') (Polynomial.C y) =
    (p * y) • 1 + (q * y) • (WeierstrassCurve.Affine.CoordinateRing.mk W') Polynomial.X
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
/-- Any object at the bottom right of a pushout square is isomorphic to the object at the bottom
right of any other pushout square with the same span.  -/
CategoryTheory.IsPushout.isoIsPushout : {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'} →
                        CategoryTheory.IsPushout f g inl inr → CategoryTheory.IsPushout f g inl' inr' → (P ≅ P')
-- Lean.Language.Lean.Types
Lean.Language.Lean.CommandElaboratingSnapshot.toSnapshot : Lean.Language.Lean.CommandElaboratingSnapshot → Lean.Language.Snapshot
-- Mathlib.RingTheory.Perfection
Perfection.coeffMonoidHom_pthRootMonoidHom : ∀ {M : Type u_1} [inst : CommMonoid M] {p : ℕ} (f : Perfection M p) (n : ℕ),
  (Perfection.coeffMonoidHom M p n) ((Perfection.pthRootMonoidHom M p) f) = (Perfection.coeffMonoidHom M p (n + 1)) f
-- Mathlib.Topology.UniformSpace.Ultra.Basic
UniformSpace.isOpen_ball_of_mem_uniformity : ∀ {X : Type u_1} [inst : UniformSpace X] (x : X) {V : SetRel X X} [V.IsTrans],
  V ∈ uniformity X → IsOpen (UniformSpace.ball x V)
-- Mathlib.Data.Nat.Factorial.Basic
Nat.add_factorial_lt_factorial_add : ∀ {i n : ℕ}, 2 ≤ i → 1 ≤ n → i + n.factorial < (i + n).factorial