mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.toBasicOpenOfGlobalSections.eq_1 : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {X : AlgebraicGeometry.Scheme} (f : A →+* ↑(X.presheaf.obj (Opposite.op ⊤)))
  {x : ↑(X.presheaf.obj (Opposite.op ⊤))} {t : A} {d : ℕ} (H : f t = x) (h0d : 0 < d) (hd : t ∈ 𝒜 d),
  AlgebraicGeometry.Proj.toBasicOpenOfGlobalSections 𝒜 f H h0d hd =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (X.isoOfEq ⋯).inv
        (CategoryTheory.CategoryStruct.comp (X.toSpecΓ ∣_ PrimeSpectrum.basicOpen x)
          (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.basicOpenIsoSpecAway x).hom
            (AlgebraicGeometry.Spec.map
              (CommRingCat.ofHom
                ((IsLocalization.map (Localization.Away x) f ⋯).comp
                  (algebraMap (HomogeneousLocalization.Away 𝒜 t) (Localization.Away t))))))))
      (AlgebraicGeometry.Proj.basicOpenIsoSpec 𝒜 t hd h0d).inv
-- Mathlib.Algebra.Group.Fin.Basic
Fin.sub_one_lt_iff : ∀ {n : ℕ} {k : Fin (n + 1)}, k - 1 < k ↔ 0 < k
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.instLaxMonoidalDiscretePUnitMonToLaxMonoidalObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (A : CategoryTheory.AddMon C) →
        (CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidalObj A).LaxMonoidal
-- Std.Time.Internal.UnitVal
Std.Time.Internal.instLEUnitVal : {x : ℚ} → LE (Std.Time.Internal.UnitVal x)
-- Mathlib.Order.Hom.Lattice
/-- Reinterpret a lattice homomorphism as a lattice homomorphism between the dual lattices.  -/
LatticeHom.dual : {α : Type u_2} → {β : Type u_3} → [inst : Lattice α] → [inst_1 : Lattice β] → LatticeHom α β ≃ LatticeHom αᵒᵈ βᵒᵈ
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- An image map is a morphism `image f → image g` fitting into a commutative square and satisfying
the obvious commutativity conditions.  -/
CategoryTheory.Limits.ImageMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {f g : CategoryTheory.Arrow C} →
      [CategoryTheory.Limits.HasImage f.hom] → [CategoryTheory.Limits.HasImage g.hom] → (f ⟶ g) → Type v
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeffs_one : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R], MvPolynomial.coeffs 1 ⊆ {1}
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.periods_subset_basisSet : ∀ {ι : Type u_3} {s : Set (ι → ℕ)} (hs : IsProperLinearSet s) [inst : Finite ι],
  IsProperLinearSet.periods✝ hs ⊆ IsProperLinearSet.basisSet✝ hs
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.MVarValue.delayedAssignment.inj : ∀ {da da_1 : Lean.DelayedMetavarAssignment},
  Aesop.EqualUpToIds.MVarValue.delayedAssignment da = Aesop.EqualUpToIds.MVarValue.delayedAssignment da_1 → da = da_1
-- Mathlib.Algebra.Notation.Defs
/-- `a /ₛ b` computes the quotient of `a` and `b`. The meaning of this notation is
type-dependent, but it is intended to be used for multiplicative torsors. 

Conventions for notations in identifiers:

 * The recommended spelling of `/ₛ` in identifiers is `sdiv`. -/
SDiv.sdiv : {G : outParam (Type u_1)} → {P : Type u_2} → [self : SDiv G P] → P → P → G
-- Mathlib.Tactic.GCongr.Core
/-- `GCongrKey` is the key used in the dictionary for looking up `gcongr` lemmas.  -/
Mathlib.Tactic.GCongr.GCongrKey : Type
-- Mathlib.Algebra.Module.Projective
Module.Projective.of_ulift : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_3} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Projective R (ULift.{w, u_3} M)], Module.Projective R M
-- Std.Http.Test.Helpers
/-- Run `tests` and wrap any failure message with the group name.
Use as `#eval runGroup "Topic" do ...`.
 -/
Std.Http.Internal.Test.runGroup : String → IO Unit → IO Unit
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.Cofan.cofanTypes_ι : ∀ {C : Type u} {F : C → Type v} (c : CategoryTheory.Limits.Cofan F) (x : CategoryTheory.Discrete C)
  (a : (CategoryTheory.Discrete.functor F).obj x),
  c.cofanTypes.ι x a =
    (match (motive := (x : CategoryTheory.Discrete C) → (CategoryTheory.Discrete.functor F).obj x → c.pt) x with
      | { as := j } => ⇑(CategoryTheory.ConcreteCategory.hom (c.inj j)))
      a
-- Mathlib.Algebra.Order.Module.Archimedean
/-- Given an upper set `s` of finite archimedean classes in a linearly ordered module `M` with
Archimedean scalars, all elements belonging to these classes together with 0 form a submodule.

This has the same carrier as `FiniteArchimedeanClass.addSubgroup`.  -/
FiniteArchimedeanClass.submodule : {M : Type u_1} →
  [inst : AddCommGroup M] →
    [inst_1 : LinearOrder M] →
      [inst_2 : IsOrderedAddMonoid M] →
        (K : Type u_2) →
          [inst_3 : Ring K] →
            [inst_4 : LinearOrder K] →
              [IsOrderedRing K] →
                [Archimedean K] →
                  [inst_7 : Module K M] → [PosSMulMono K M] → UpperSet (FiniteArchimedeanClass M) → Submodule K M
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.evariance_eq_lintegral_ofReal : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.evariance X μ = ∫⁻ (ω : Ω), ENNReal.ofReal ((X ω - ∫ (x : Ω), X x ∂μ) ^ 2) ∂μ
-- Aesop.Rule.Name
Aesop.getRuleNameForExpr : Lean.Expr → Lean.MetaM Lean.Name
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
/-- For `a : F`, `quadraticChar F a = -1 ↔ ¬ IsSquare a`.  -/
quadraticChar_neg_one_iff_not_isSquare : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F] {a : F},
  (quadraticChar F) a = -1 ↔ ¬IsSquare a
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.lsingle_apply : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring S] [inst_1 : Semiring R] [inst_2 : Module R S] (a : M)
  (b : S), (AddMonoidAlgebra.lsingle a) b = AddMonoidAlgebra.single a b
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instAdd : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : AddZeroClass β] → [ContinuousAdd β] → Add (ZeroAtInftyContinuousMap α β)
-- Mathlib.Algebra.Homology.DifferentialObject
HomologicalComplex.homologicalComplexToDGO_obj_d : ∀ {β : Type u_1} [inst : AddCommGroup β] (b : β) (V : Type u_2) [inst_1 : CategoryTheory.Category.{v_1, u_2} V]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V (ComplexShape.up' b)) (i : β),
  ((HomologicalComplex.homologicalComplexToDGO b V).obj X).d i = X.d i ((fun b_1 => b_1 + { as := 1 }.as • b) i)
-- Mathlib.FieldTheory.IntermediateField.Algebraic
mem_subalgebraEquivIntermediateField_symm : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : Algebra.IsAlgebraic K L] {S : IntermediateField K L} {x : L},
  x ∈ subalgebraEquivIntermediateField.symm S ↔ x ∈ S
-- Mathlib.Analysis.Normed.Group.Quotient
/-- The operator norm of the projection is `1` if the subspace is not dense.  -/
AddSubgroup.norm_normedMk : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] (S : AddSubgroup M),
  ↑S.topologicalClosure ≠ Set.univ → ‖S.normedMk‖ = 1
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousMonoidHom.instTopologicalSpace.eq_1 : ∀ (A : Type u_2) (B : Type u_3) [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B],
  ContinuousMonoidHom.instTopologicalSpace A B =
    TopologicalSpace.induced ContinuousMonoidHom.toContinuousMap ContinuousMap.compactOpen
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.map_iInf : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] [inst_6 : Semiring B] [inst_7 : Algebra R B]
  [inst_8 : StarRing B] [inst_9 : StarModule R B] {ι : Sort u_5} [Nonempty ι] (f : A →⋆ₐ[R] B),
  Function.Injective ⇑f →
    ∀ (s : ι → StarSubalgebra R A), StarSubalgebra.map f (iInf s) = ⨅ i, StarSubalgebra.map f (s i)
-- Mathlib.Data.PNat.Factors
PrimeMultiset.prod_ofPrime : ∀ (p : Nat.Primes), (PrimeMultiset.ofPrime p).prod = ↑p
-- Mathlib.Algebra.Group.Subgroup.Defs
mul_mem_cancel_right : ∀ {G : Type u_1} [inst : Group G] {S : Type u_4} {H : S} [inst_1 : SetLike S G] [SubgroupClass S G] {x y : G},
  x ∈ H → (y * x ∈ H ↔ y ∈ H)
-- Lean.Elab.Command
Lean.Elab.Command.MacroExpandedSnapshot.mk : Lean.Language.Snapshot →
  Lean.Name →
    Lean.Syntax →
      ℕ →
        Bool →
          Array (Lean.Language.SnapshotTask Lean.Language.DynamicSnapshot) → Lean.Elab.Command.MacroExpandedSnapshot
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.power_eq_two_power : ∀ {c₁ c₂ : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c₁ → 2 ≤ c₂ → c₂ ≤ c₁ → c₂ ^ c₁ = 2 ^ c₁
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_filter_key : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {f : α → Bool} {k : α}, (Std.DHashMap.filter (fun k x => f k) m).getKey? k = Option.filter f (m.getKey? k)
-- Mathlib.NumberTheory.Padics.Complex
/-- The norm on `PadicAlgCl p` is nonarchimedean.  -/
PadicAlgCl.isNonarchimedean : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], IsNonarchimedean norm
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.least?_le : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.Least? α]
  [Std.PRange.LawfulUpwardEnumerableLeast? α] {a : α},
  ∃ init, Std.PRange.least? = some init ∧ Std.PRange.UpwardEnumerable.LE init a
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get_insert : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h : m.WF) {k a : α} {h₁ : a ∈ m.insert k},
  (m.insert k).get a h₁ = if h₂ : (k == a) = true ∧ k ∉ m then k else m.get a ⋯
-- Mathlib.Algebra.Category.Ring.Colimits
_private.Mathlib.Algebra.Category.Ring.Colimits.0.CommRingCat.Colimits.descFunLift.match_1.eq_4 : ∀ {J : Type u_1} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat)
  (motive : CommRingCat.Colimits.Prequotient F → Sort u_2) (x : CommRingCat.Colimits.Prequotient F)
  (h_1 : (j : J) → (x : ↑(F.obj j)) → motive (CommRingCat.Colimits.Prequotient.of j x))
  (h_2 : Unit → motive CommRingCat.Colimits.Prequotient.zero) (h_3 : Unit → motive CommRingCat.Colimits.Prequotient.one)
  (h_4 : (x : CommRingCat.Colimits.Prequotient F) → motive x.neg)
  (h_5 : (x y : CommRingCat.Colimits.Prequotient F) → motive (x.add y))
  (h_6 : (x y : CommRingCat.Colimits.Prequotient F) → motive (x.mul y)),
  (match x.neg with
    | CommRingCat.Colimits.Prequotient.of j x => h_1 j x
    | CommRingCat.Colimits.Prequotient.zero => h_2 ()
    | CommRingCat.Colimits.Prequotient.one => h_3 ()
    | x.neg => h_4 x
    | x.add y => h_5 x y
    | x.mul y => h_6 x y) =
    h_4 x
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.Internal.optionPelim'.match_1.eq_2 : ∀ {α : Type u_1} {β : Sort u_3} (motive : (t : Option α) → (t = none → β) → ((val : α) → t = some val → β) → Sort u_2)
  (n : none = none → β) (s : (val : α) → none = some val → β)
  (h_1 : (a : α) → (n : some a = none → β) → (s : (val : α) → some a = some val → β) → motive (some a) n s)
  (h_2 : (n : none = none → β) → (s : (val : α) → none = some val → β) → motive none n s),
  (match none, n, s with
    | some a, n, s => h_1 a n s
    | none, n, s => h_2 n s) =
    h_2 n s
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- The image of `algebraMap` is contained in the underlying set of the subalgebra  -/
Subalgebra.algebraMap_mem' : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (self : Subalgebra R A)
  (r : R), (algebraMap R A) r ∈ self.carrier
-- Mathlib.Algebra.Star.Unitary
/-- Unitary conjugation preserves the spectrum, star on right.  -/
Unitary.spectrum_star_right_conjugate : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] [inst_3 : StarMul A]
  {a : A} {U : ↥(unitary A)}, spectrum R (↑U * a * star ↑U) = spectrum R a
-- Init.Prelude
/-- A `sepBy(p, sep)` parses 0 or more occurrences of `p` separated by `sep`.
`psep` is usually the same as `symbol sep`, but it can be overridden.
`sep` is only used in the antiquot syntax: `$x;*` would match if `sep` is `";"`.
`allowTrailingSep` is true if e.g. `a, b,` is also allowed to match.  -/
Lean.ParserDescr.sepBy : Lean.ParserDescr → String → Lean.ParserDescr → optParam Bool false → Lean.ParserDescr
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sigma_ι_isOpenImmersion_aux : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] {ι : Type v}
  (F : CategoryTheory.Functor (CategoryTheory.Discrete ι) (AlgebraicGeometry.SheafedSpace C))
  [inst_2 : CategoryTheory.Limits.HasColimit F] (i : CategoryTheory.Discrete ι)
  [CategoryTheory.Limits.HasStrictTerminalObjects C],
  AlgebraicGeometry.SheafedSpace.IsOpenImmersion (CategoryTheory.Limits.colimit.ι F i)
-- Mathlib.Topology.Category.Profinite.EffectiveEpi
/-- An effective presentation of an `X : Profinite` with respect to the inclusion functor from `Stonean`
 -/
Profinite.profiniteToCompHausEffectivePresentation : (X : CompHaus) → profiniteToCompHaus.EffectivePresentation X
-- Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty
CategoryTheory.MorphismProperty.ofObjectProperty_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P Q : CategoryTheory.ObjectProperty C) {X Y : C}
  (f : X ⟶ Y), CategoryTheory.MorphismProperty.ofObjectProperty P Q f ↔ P X ∧ Q Y
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [Std.TransOrd α] [inst : Inhabited γ] {f : α → β → Option γ} {k k' : α} (h : t.WF),
  t.getKey? k = some k' →
    Std.DTreeMap.Internal.Impl.Const.get! (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl k =
      ((Std.DTreeMap.Internal.Impl.Const.get? t k).bind fun x => f k' x).get!
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.MkSimpContextResult.mk.injEq : ∀ (ctx : Lean.Meta.Simp.Context) (simprocs : Lean.Meta.Simp.SimprocsArray)
  (dischargeWrapper : Lean.Elab.Tactic.Simp.DischargeWrapper)
  (simpArgs : Array (Lean.Syntax × Lean.Elab.Tactic.ElabSimpArgResult)) (ctx_1 : Lean.Meta.Simp.Context)
  (simprocs_1 : Lean.Meta.Simp.SimprocsArray) (dischargeWrapper_1 : Lean.Elab.Tactic.Simp.DischargeWrapper)
  (simpArgs_1 : Array (Lean.Syntax × Lean.Elab.Tactic.ElabSimpArgResult)),
  ({ ctx := ctx, simprocs := simprocs, dischargeWrapper := dischargeWrapper, simpArgs := simpArgs } =
      { ctx := ctx_1, simprocs := simprocs_1, dischargeWrapper := dischargeWrapper_1, simpArgs := simpArgs_1 }) =
    (ctx = ctx_1 ∧ simprocs = simprocs_1 ∧ dischargeWrapper = dischargeWrapper_1 ∧ simpArgs = simpArgs_1)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.unitIso_inv_hom_id_app_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) (X : C) {Z : C} (h : e.inverse.obj (e.functor.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.unitInv.app X) (CategoryTheory.CategoryStruct.comp (e.unit.app X) h) = h
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.coe_ne_infty : ∀ {X : Type u_1} (x : X), ↑x ≠ OnePoint.infty
-- Mathlib.Topology.Order.LeftRightLim
Antitone.rightLim_le_leftLim : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Antitone f → ∀ {x y : α}, x ≤ y → Function.rightLim f y ≤ Function.leftLim f x
-- Lean.Util.FoldConsts
Lean.Expr.FoldConstsImpl.foldUnsafe : {α : Type} → Lean.Expr → α → (Lean.Name → α → α) → α
-- Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
/-- Given a Localization map `f : M →*₀ N` for a Submonoid `S ⊆ M` and a map of
`CommMonoidWithZero`s `g : M →*₀ P` such that `g y` is invertible for all `y : S`, the
homomorphism induced from `N` to `P` sending `z : N` to `g x * (g y)⁻¹`, where `(x, y) : M × S`
are such that `z = f x * (f y)⁻¹`.  -/
Submonoid.LocalizationMap.lift₀ : {M : Type u_1} →
  [inst : CommMonoidWithZero M] →
    {S : Submonoid M} →
      {N : Type u_2} →
        [inst_1 : CommMonoidWithZero N] →
          {P : Type u_3} →
            [inst_2 : CommMonoidWithZero P] →
              S.LocalizationMap N → (g : M →*₀ P) → (∀ (y : ↥S), IsUnit (g ↑y)) → N →*₀ P
-- Mathlib.Data.Set.Image
Set.range_ite_subset : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} [inst : DecidablePred p] {f g : α → β},
  (Set.range fun x => if p x then f x else g x) ⊆ Set.range f ∪ Set.range g
-- Mathlib.Topology.Order.Basic
tendsto_order_unbounded : ∀ {α : Type u} {β : Type v} [ts : TopologicalSpace α] [inst : Preorder α] [OrderTopology α] {f : β → α} {a : α}
  {x : Filter β},
  (∃ u, a < u) →
    (∃ l, l < a) → (∀ (l u : α), l < a → a < u → ∀ᶠ (b : β) in x, l < f b ∧ f b < u) → Filter.Tendsto f x (nhds a)
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalTerm.evalStringStx : Lean.Term → Lean.Elab.TermElabM (String × Lean.Expr)
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.map_adj_apply' : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {u v : V} {f : V → W},
  G.Adj u v → f u ≠ f v → (SimpleGraph.map f G).Adj (f u) (f v)
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.NatTrans.CommShift.of_iso_symm : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F₁ F₂ : CategoryTheory.Functor C D} (e : F₁ ≅ F₂) (A : Type u_5)
  [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A]
  [inst_5 : F₁.CommShift A] [inst_6 : F₂.CommShift A] [CategoryTheory.NatTrans.CommShift e.hom A],
  CategoryTheory.NatTrans.CommShift e.symm.hom A
-- Mathlib.Algebra.Ring.IsFormallyReal
IsSumNonzeroSq.brecOn : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Add R] [inst_2 : Zero R] {motive : (a : R) → IsSumNonzeroSq a → Prop} {a : R}
  (t : IsSumNonzeroSq a), (∀ (a : R) (t : IsSumNonzeroSq a), IsSumNonzeroSq.below t → motive a t) → motive a t
-- Lean.Setup
/-- Available for execution in the final native code.  -/
Lean.IRPhases.runtime : Lean.IRPhases
-- Mathlib.Algebra.Category.FGModuleCat.Limits
FGModuleCat.instPreservesFiniteLimitsModuleCatForget₂LinearMapIdCarrierObjIsFG : ∀ {k : Type u} [inst : Ring k] [IsNoetherianRing k],
  CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k))
-- Mathlib.Probability.ProbabilityMassFunction.Binomial
/-- The binomial distribution on one coin is the Bernoulli distribution.  -/
PMF.binomial_one_eq_bernoulli : ∀ (p : NNReal) (h : p ≤ 1), PMF.binomial p h 1 = PMF.map (fun x => bif x then 1 else 0) (PMF.bernoulli p h)
-- Lean.Meta.MatchUtil
Lean.Meta.matchNe? : Lean.Expr → Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr))
-- Lean.Meta.Tactic.Grind.AC.Seq
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.Seq.noAdjacentDuplicates.go : Lean.Grind.AC.Var → Lean.Grind.AC.Seq → Bool
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Measurable.forall : ∀ {α : Type u_1} {ι : Sort uι} [inst : MeasurableSpace α] [Countable ι] {p : ι → α → Prop},
  (∀ (i : ι), Measurable (p i)) → Measurable fun a => ∀ (i : ι), p i a
-- Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction
/-- Given a parametrized adjunction `F ⊣₂ G` between bifunctors, structures
`sq₁₂ : F.PushoutObjObj f₁ f₂` and `sq₁₃ : G.PullbackObjObj f₁ f₃`,
there are as many liftings for the commutative square given by a
map `α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃` as there are liftings
for the square given by the corresponding map `Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π`.  -/
CategoryTheory.ParametrizedAdjunction.liftStructEquiv : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} →
              {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} →
                (adj₂ : F ⊣₂ G) →
                  {X₁ Y₁ : C₁} →
                    {f₁ : X₁ ⟶ Y₁} →
                      {X₂ Y₂ : C₂} →
                        {f₂ : X₂ ⟶ Y₂} →
                          {X₃ Y₃ : C₃} →
                            {f₃ : X₃ ⟶ Y₃} →
                              (sq₁₂ : F.PushoutObjObj f₁ f₂) →
                                (sq₁₃ : G.PullbackObjObj f₁ f₃) →
                                  (α : CategoryTheory.Arrow.mk sq₁₂.ι ⟶ CategoryTheory.Arrow.mk f₃) →
                                    CategoryTheory.Arrow.LiftStruct α ≃
                                      CategoryTheory.Arrow.LiftStruct ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.prod_mono : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {s₁ s₂ : AddSubsemigroup M} {t₁ t₂ : AddSubsemigroup N},
  s₁ ≤ s₂ → t₁ ≤ t₂ → s₁.prod t₁ ≤ s₂.prod t₂
-- Mathlib.Tactic.NormNum.IsSquare
Mathlib.Meta.NormNum.not_isSquare_of_isRat_neg : ∀ (a : ℚ) (n d : ℕ), n ≠ 0 → d ≠ 0 → Mathlib.Meta.NormNum.IsRat a (Int.negOfNat n) d → ¬IsSquare a
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.IsDiscrete.subsingleton : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} [self : CategoryTheory.IsDiscrete C] (X Y : C),
  Subsingleton (X ⟶ Y)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- We show that the converse to `isSplitMonoEqualizes` is true:
Whenever `f` equalizes `(r ≫ f)` and `(𝟙 Y)`, then `r` is a retraction of `f`.  -/
CategoryTheory.Limits.splitMonoOfEqualizer : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f : X ⟶ Y} →
        {r : Y ⟶ X} →
          (hr : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp r f) = f) →
            CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f ⋯) → CategoryTheory.SplitMono f
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.IsSFiniteKernel.comap : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {g : γ → α} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ]
  (hg : Measurable g), ProbabilityTheory.IsSFiniteKernel (κ.comap g hg)
-- Mathlib.Algebra.Lie.Basic
/-- View an equivalence of Lie modules as a type level equivalence.  -/
LieModuleEquiv.toEquiv : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {N : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : LieRingModule L M] → [inst_7 : LieRingModule L N] → (M ≃ₗ⁅R,L⁆ N) → M ≃ N
-- Mathlib.Order.Filter.Pointwise
Filter.vadd.instNeBot : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {f : Filter α} {g : Filter β} [f.NeBot] [g.NeBot], (f +ᵥ g).NeBot
-- Mathlib.Algebra.Lie.Extension
/-- A preparatory function for making a 2-cocycle from a linear splitting of an extension.  -/
_private.Mathlib.Algebra.Lie.Extension.0.LieAlgebra.Extension.twoCocycleAux : {R : Type u_1} →
  {L : Type u_3} →
    {M : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : LieRing M] →
              [inst_4 : LieAlgebra R M] →
                (E : LieAlgebra.Extension R M L) →
                  {s : L →ₗ[R] E.L} → Function.LeftInverse ⇑E.proj ⇑s → L →ₗ[R] L →ₗ[R] ↥E.proj.ker
-- Mathlib.Data.Nat.Count
Nat.count_succ_eq_count_iff : ∀ {p : ℕ → Prop} [inst : DecidablePred p] {n : ℕ}, Nat.count p (n + 1) = Nat.count p n ↔ ¬p n