mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.llp_rlp_ιObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ] {X Y : C}
  (f : X ⟶ Y), I.rlp.llp (CategoryTheory.SmallObject.ιObj I κ f)
-- Mathlib.Order.TypeTags
WithBot.inhabited : {α : Type u_1} → Inhabited (WithBot α)
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.image_univ_of_surjective : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq α] [inst_2 : Fintype β] {f : β → α},
  Function.Surjective f → Finset.image f Finset.univ = Finset.univ
-- Mathlib.Tactic.CongrExclamation
/-- Whether to use the congruence generator that is used by `simp` and `congr`. This generator
is more strict, and it does not respect all configuration settings. It does respect
`preferLHS`, `partialApp` and `maxArgs` and transparency settings. It acts as if `sameFun := true`
and it ignores `typeEqs`.  -/
Congr!.Config.useCongrSimp : Congr!.Config → Bool
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RcoSliceData.mk.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : SizeOf α] [inst_2 : SizeOf β]
  (treeMap : Std.DTreeMap.Internal.Impl α fun x => β) (range : Std.Rco α),
  sizeOf { treeMap := treeMap, range := range } = 1 + sizeOf treeMap + sizeOf range
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- Pointwise unions of upper hemicontinuous maps are upper hemicontinuous.  -/
UpperHemicontinuous.union : ∀ {α : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → Set β},
  UpperHemicontinuous f → UpperHemicontinuous g → UpperHemicontinuous fun x => f x ∪ g x
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- We define `P` to be a sheaf for the presieve `R` if every compatible family has a unique
amalgamation.

This is the definition of a sheaf for the given presieve given in C2.1.2 of [Elephant], and
https://ncatlab.org/nlab/show/sheaf#GeneralDefinitionInComponents.
Using `compatible_iff_sieveCompatible`,
this is equivalent to the definition of a sheaf in [MM92], Chapter III, Section 4.
 -/
CategoryTheory.Presieve.IsSheafFor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} → CategoryTheory.Functor Cᵒᵖ (Type w) → CategoryTheory.Presieve X → Prop
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasColimit.mk' : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C},
  Nonempty (CategoryTheory.Limits.ColimitCocone F) → CategoryTheory.Limits.HasColimit F
-- Mathlib.Data.Nat.Factorization.Defs
/-- For coprime `a` and `b`, the power of `p` in `a * b` is the sum of the powers in `a` and `b`  -/
Nat.factorization_mul_apply_of_coprime : ∀ {p a b : ℕ}, a.Coprime b → (a * b).factorization p = a.factorization p + b.factorization p
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.sub_mem : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) {x y : R}, x ∈ I → y ∈ I → x - y ∈ I
-- Mathlib.Topology.Algebra.Support
/-- The topological support of a function is the closure of its support, i.e. the closure of the
set of all elements where the function is not equal to 1.  -/
mulTSupport : {X : Type u_1} → {α : Type u_2} → [One α] → [TopologicalSpace X] → (X → α) → Set X
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vadd_mem_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {s : Finset α} {t : Finset β} {a : α}
  {b : β}, a ∈ s → b ∈ t → a +ᵥ b ∈ s +ᵥ t
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
/-- A `2 × 2` matrix is *parabolic* if it is non-scalar and its discriminant is 0.  -/
Matrix.IsParabolic : {R : Type u_1} → [CommRing R] → Matrix (Fin 2) (Fin 2) R → Prop
-- Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom
CochainComplex.HomComplex.CohomologyClass.toSmallShiftedHom_mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {K L : CochainComplex C ℤ}
  {n : ℤ}
  [inst_2 :
    CategoryTheory.Localization.HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L]
  (x : CochainComplex.HomComplex.Cocycle K L n),
  (CochainComplex.HomComplex.CohomologyClass.mk x).toSmallShiftedHom =
    CategoryTheory.Localization.SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ))
      (CochainComplex.HomComplex.Cocycle.equivHomShift.symm x)
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.CommRingObjCat.instFaithfulForget : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C], (CategoryTheory.CommRingObjCat.forget C).Faithful
-- Mathlib.Algebra.NonAssoc.PreLie.Basic
/-- Every left pre-Lie ring is a right pre-Lie ring with the opposite multiplication  -/
RightPreLieRing.instLeftPreLieRingMulOpposite : {L : Type u_2} → [RightPreLieRing L] → LeftPreLieRing Lᵐᵒᵖ
-- Mathlib.Algebra.Module.LinearMap.Basic
Sum.elimZeroLeft_apply : ∀ {ι : Type u_6} {κ : Type u_7} {R : Type u_8} [inst : Semiring R] (g : ι → R) (a : κ ⊕ ι),
  Sum.elimZeroLeft g a = Sum.elim 0 g a
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.ExistsHomHomCompEqCompAux.mk.inj : ∀ {I : Type u} {inst : CategoryTheory.Category.{u, u} I} {S X : AlgebraicGeometry.Scheme}
  {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme} {t : D ⟶ (CategoryTheory.Functor.const I).obj S} {f : X ⟶ S}
  {c : CategoryTheory.Limits.Cone D} {hc : CategoryTheory.Limits.IsLimit c} {i : I} {a : D.obj i ⟶ X}
  {ha : t.app i = CategoryTheory.CategoryStruct.comp a f} {b : D.obj i ⟶ X}
  {hb : t.app i = CategoryTheory.CategoryStruct.comp b f}
  {hab : CategoryTheory.CategoryStruct.comp (c.π.app i) a = CategoryTheory.CategoryStruct.comp (c.π.app i) b}
  {𝒰S : S.OpenCover} {h𝒰S : ∀ (i : 𝒰S.I₀), AlgebraicGeometry.IsAffine (𝒰S.X i)}
  {𝒰X :
    (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰S).I₀) →
      ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰S).X i).OpenCover}
  {h𝒰X :
    ∀ (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰S).I₀) (j : (𝒰X i).I₀),
      AlgebraicGeometry.IsAffine ((𝒰X i).X j)}
  {c_1 : CategoryTheory.Limits.Cone D} {hc_1 : CategoryTheory.Limits.IsLimit c_1} {i_1 : I} {a_1 : D.obj i_1 ⟶ X}
  {ha_1 : t.app i_1 = CategoryTheory.CategoryStruct.comp a_1 f} {b_1 : D.obj i_1 ⟶ X}
  {hb_1 : t.app i_1 = CategoryTheory.CategoryStruct.comp b_1 f}
  {hab_1 :
    CategoryTheory.CategoryStruct.comp (c_1.π.app i_1) a_1 = CategoryTheory.CategoryStruct.comp (c_1.π.app i_1) b_1}
  {𝒰S_1 : S.OpenCover} {h𝒰S_1 : ∀ (i : 𝒰S_1.I₀), AlgebraicGeometry.IsAffine (𝒰S_1.X i)}
  {𝒰X_1 :
    (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰S_1).I₀) →
      ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰S_1).X i).OpenCover}
  {h𝒰X_1 :
    ∀ (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰S_1).I₀) (j : (𝒰X_1 i).I₀),
      AlgebraicGeometry.IsAffine ((𝒰X_1 i).X j)},
  { c := c, hc := hc, i := i, a := a, ha := ha, b := b, hb := hb, hab := hab, 𝒰S := 𝒰S, h𝒰S := h𝒰S, 𝒰X := 𝒰X,
        h𝒰X := h𝒰X } =
      { c := c_1, hc := hc_1, i := i_1, a := a_1, ha := ha_1, b := b_1, hb := hb_1, hab := hab_1, 𝒰S := 𝒰S_1,
        h𝒰S := h𝒰S_1, 𝒰X := 𝒰X_1, h𝒰X := h𝒰X_1 } →
    c = c_1 ∧ hc ≍ hc_1 ∧ i = i_1 ∧ a ≍ a_1 ∧ b ≍ b_1 ∧ 𝒰S = 𝒰S_1 ∧ 𝒰X ≍ 𝒰X_1
-- Mathlib.Data.Fin.Tuple.Curry
Function.FromTypes.uncurry_apply_cons : ∀ {n : ℕ} {α : Type u} {p : Fin n → Type u} {τ : Type u} (f : Function.FromTypes (Matrix.vecCons α p) τ) (a : α)
  (args : (i : Fin n) → p i), f.uncurry (Fin.cons a args) = (f a).uncurry args
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.coe_insert : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : MeasurableSingletonClass α] (a : α) (s : Subtype MeasurableSet),
  ↑(insert a s) = insert a ↑s
-- Mathlib.Topology.Order.LeftRightLim
Monotone.rightLim : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {f : α → β}, Monotone f → Monotone (Function.rightLim f)
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.instInhabitedCasesTypes : Inhabited Lean.Meta.Grind.CasesTypes
-- Aesop.RuleTac.Tactic
Aesop.RuleTac.tacGen : Lean.Name → Aesop.RuleTac
-- Init.Omega.Int
Lean.Omega.Int.mul_congr : ∀ {a b c d : ℤ}, a = b → c = d → a * c = b * d
-- Init.Data.Ord.Basic
Ord.ext : ∀ {α : Type u} {x y : Ord α}, compare = compare → x = y
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
SpectrumRestricts.nnreal_add : ∀ {A : Type u_1} [inst : CStarAlgebra A] {a b : A},
  IsSelfAdjoint a →
    IsSelfAdjoint b →
      SpectrumRestricts a ⇑ContinuousMap.realToNNReal →
        SpectrumRestricts b ⇑ContinuousMap.realToNNReal → SpectrumRestricts (a + b) ⇑ContinuousMap.realToNNReal
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.add_mul : ∀ {R : Type u_1} [inst : CommSemiring R] {a₁ a₂ b c₁ c₂ d : R},
  a₁ * b = c₁ → a₂ * b = c₂ → c₁ + c₂ = d → (a₁ + a₂) * b = d
-- Mathlib.RingTheory.LaurentSeries
PowerSeries.coe_sub : ∀ {R' : Type u_2} [inst : Ring R'] (f' g' : PowerSeries R'),
  (HahnSeries.ofPowerSeries ℤ R') (f' - g') = (HahnSeries.ofPowerSeries ℤ R') f' - (HahnSeries.ofPowerSeries ℤ R') g'
-- Std.Data.ExtDTreeMap.Basic
/-- Computes the union of the given tree maps. If a key appears in both maps, the entry contained in
the second argument will appear in the result.

This function always merges the smaller map into the larger map.
 -/
Std.ExtDTreeMap.union : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → Std.ExtDTreeMap α β cmp → Std.ExtDTreeMap α β cmp
-- Aesop.Script.StructureStatic
_private.Aesop.Script.StructureStatic.0.Aesop.Script.structureStaticCore.go : Aesop.Script.TacticState → Aesop.Script.StaticStructureM (List Aesop.Script.Step × Aesop.Script.TacticState)
-- Mathlib.Data.EReal.Operations
EReal.nsmul_eq_mul : ∀ (n : ℕ) (x : EReal), n • x = ↑n * x
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearEquiv.rTensor_zpow : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (f : M ≃ₗ[R] M) (n : ℤ),
  LinearEquiv.rTensor N f ^ n = LinearEquiv.rTensor N (f ^ n)
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- In a topological vector space, if the unit ball of a continuous inner product is von Neumann
bounded, then the inner product defines the same topology as the original one.  -/
InnerProductSpace.Core.topology_eq : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [cd : InnerProductSpace.Core 𝕜 F] [tF : TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜 F],
  ContinuousAt (fun v => inner 𝕜 v v) 0 →
    Bornology.IsVonNBounded 𝕜 {v | RCLike.re (inner 𝕜 v v) < 1} →
      tF = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.homEquiv_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (X : C) (Y : D) (f : F.obj X ⟶ Y),
  (adj.homEquiv X Y) f = CategoryTheory.CategoryStruct.comp (adj.unit.app X) (G.map f)
-- Mathlib.Analysis.InnerProductSpace.Rayleigh
IsSelfAdjoint.eq_smul_self_of_isLocalExtrOn : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] {T : E →L[𝕜] E},
  IsSelfAdjoint T →
    ∀ {x₀ : E}, IsLocalExtrOn T.reApplyInnerSelf (Metric.sphere 0 ‖x₀‖) x₀ → T x₀ = ↑(T.rayleighQuotient x₀) • x₀
-- Lean.Parser.Term
Lean.Parser.Term.prop.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
/-- If a finset `u` is contained in the scalar sum of two sets `s +ᵥ t`, we can find two
finsets `s'`, `t'` such that `s' ⊆ s`, `t' ⊆ t` and `u ⊆ s' +ᵥ t'`.  -/
Finset.subset_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {u : Finset β} {s : Set α} {t : Set β},
  ↑u ⊆ s +ᵥ t → ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' +ᵥ t'
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.ringHomComp_pow : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommRing R'] {R'' : Type u_3} [inst_2 : CommRing R'']
  (χ : MulChar R R') (f : R' →+* R'') (n : ℕ), χ.ringHomComp f ^ n = (χ ^ n).ringHomComp f
-- Mathlib.Algebra.CharP.Defs
/-- Noncomputable function that outputs the unique characteristic of a semiring.  -/
ringChar : (R : Type u_1) → [NonAssocSemiring R] → ℕ
-- Mathlib.SetTheory.ZFC.VonNeumann
ZFSet.iUnion_vonNeumann : ⋃ o, ↑(ZFSet.vonNeumann o) = Class.univ
-- Mathlib.RingTheory.Congruence.Opposite
/-- If `c` is a `RingCon Rᵐᵒᵖ`, then `(a, b) ↦ c b.op a.op` is a `RingCon R`.
 -/
RingCon.unop : {R : Type u_1} → [inst : Add R] → [inst_1 : Mul R] → RingCon Rᵐᵒᵖ → RingCon R
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- Given `AddSubgroup`s `H`, `K` of `AddGroup`s `A`, `B` respectively, `H × K`
as an `AddSubgroup` of `A × B`.  -/
AddSubgroup.prod : {G : Type u_1} →
  [inst : AddGroup G] → {N : Type u_5} → [inst_1 : AddGroup N] → AddSubgroup G → AddSubgroup N → AddSubgroup (G × N)
-- Mathlib.Algebra.Order.Sub.Basic
/-- See `lt_tsub_iff_left_of_le_of_le` for a weaker statement in a partial order.  -/
AddLECancellable.tsub_lt_tsub_iff_left_of_le : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] {a b c : α}, AddLECancellable a → AddLECancellable b → b ≤ a → (a - b < a - c ↔ c < b)
-- Mathlib.CategoryTheory.Pi.Monoidal
/-- The unit for the adjunction `tensorLeft X ⊣ ihom X`.  -/
CategoryTheory.Pi.closedUnit : {I : Type w₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] →
        [inst_2 : (i : I) → CategoryTheory.MonoidalClosed (C i)] →
          (X : (i : I) → C i) →
            CategoryTheory.Functor.id ((i : I) → C i) ⟶
              (CategoryTheory.MonoidalCategory.tensorLeft X).comp (CategoryTheory.Pi.ihom X)
-- Mathlib.Probability.UniformOn
ProbabilityTheory.uniformOn_singleton : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [MeasurableSingletonClass Ω] (ω : Ω) (t : Set Ω)
  [inst_2 : Decidable (ω ∈ t)], (ProbabilityTheory.uniformOn {ω}) t = if ω ∈ t then 1 else 0
-- Mathlib.MeasureTheory.Measure.Comap
/-- Pullback of a `Measure`. If `f` sends each measurable set to a null-measurable set,
then for each measurable set `s` we have `comap f μ s = μ (f '' s)`.

Note that if `f` is not injective, this definition assigns `Set.univ` measure zero.  -/
MeasureTheory.Measure.comap : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      [inst_1 : MeasurableSpace β] → (α → β) → MeasureTheory.Measure β → MeasureTheory.Measure α
-- Lean.Level
Lean.mkLevelSuccEx : Lean.Level → Lean.Level
-- Mathlib.GroupTheory.PGroup
IsPGroup.of_equiv : ∀ {p : ℕ} {G : Type u_1} [inst : Group G], IsPGroup p G → ∀ {H : Type u_2} [inst_1 : Group H] (ϕ : G ≃* H), IsPGroup p H
-- Init.Data.Vector.Attach
Vector.map_attachWith_eq_pmap : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {P : α → Prop} {H : ∀ a ∈ xs, P a} {f : { x // P x } → β},
  Vector.map f (xs.attachWith P H) = Vector.pmap (fun a h => f ⟨a, ⋯⟩) xs ⋯
-- Aesop.Util.Basic
Aesop.getConclusionDiscrTreeKeys : Lean.Expr → Lean.MetaM (Array Lean.Meta.DiscrTree.Key)
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Equiv.Perm.two_le_length_toList_iff_mem_support : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {p : Equiv.Perm α} {x : α},
  2 ≤ (p.toList x).length ↔ x ∈ p.support
-- Mathlib.Logic.Function.Defs
/-- The diagonal map into `Prod`.  -/
Function.diag : {α : Type u_1} → α → α × α
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.valuation_le_one_iff : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (x : K), A.valuation x ≤ 1 ↔ x ∈ A
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.a₃_of_isCharTwoJNeZeroNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJNeZeroNF], W.a₃ = 0
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_eq_iff_of_pos : ∀ {k x y : ℤ}, 0 < k → (x / k = y ↔ y * k ≤ x ∧ x < y * k + k)
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Key.lit.injEq : ∀ (a a_1 : Lean.Literal), (Lean.Meta.DiscrTree.Key.lit a = Lean.Meta.DiscrTree.Key.lit a_1) = (a = a_1)
-- Init.Data.SInt.Basic
Int8.instNeg : Neg Int8
-- Mathlib.RingTheory.AlgebraicIndependent.Defs
/-- Canonical isomorphism between polynomials and the subalgebra generated by
algebraically independent elements.  -/
AlgebraicIndependent.aevalEquiv : {ι : Type u_1} →
  {R : Type u_3} →
    {A : Type u_5} →
      {x : ι → A} →
        [inst : CommRing R] →
          [inst_1 : CommRing A] →
            [inst_2 : Algebra R A] → AlgebraicIndependent R x → MvPolynomial ι R ≃ₐ[R] ↥(Algebra.adjoin R (Set.range x))
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.instBoundedOrderCarrier : (X : FinBddDistLat) → BoundedOrder ↑X.toDistLat
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.logMahlerMeasure_mul_eq_add_logMahlerMeasure : ∀ {p q : Polynomial ℂ}, p * q ≠ 0 → (p * q).logMahlerMeasure = p.logMahlerMeasure + q.logMahlerMeasure
-- Std.Data.Internal.List.Associative
Std.Internal.List.self_le_maxKey_insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {v : β k}, (compare k (Std.Internal.List.maxKey (Std.Internal.List.insertEntry k v l) ⋯)).isLE = true
-- Mathlib.Order.Cover
Prod.mk_wcovBy_mk_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] {a₁ a₂ : α} {b₁ b₂ : β},
  (a₁, b₁) ⩿ (a₂, b₂) ↔ a₁ ⩿ a₂ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₂
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2to1.stRun.match_1.splitter : {K : Type u_1} →
  {Γ : K → Type u_2} →
    {σ : Type u_3} →
      {k : K} →
        (motive : Turing.TM2to1.StAct K Γ σ k → Sort u_4) →
          (x : Turing.TM2to1.StAct K Γ σ k) →
            ((f : σ → Γ k) → motive (Turing.TM2to1.StAct.push f)) →
              ((f : σ → Option (Γ k) → σ) → motive (Turing.TM2to1.StAct.peek f)) →
                ((f : σ → Option (Γ k) → σ) → motive (Turing.TM2to1.StAct.pop f)) → motive x
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.symm_vadd : ∀ {G : Type u_1} {α : Type u_3} [inst : MeasurableSpace α] [inst_1 : AddGroup G] [inst_2 : AddAction G α]
  [inst_3 : MeasurableConstVAdd G α] (c : G), (MeasurableEquiv.vadd c).symm = MeasurableEquiv.vadd (-c)
-- Mathlib.Data.List.AList
/-- Erase a key from the map, and return the corresponding value, if found.  -/
AList.extract : {α : Type u} → {β : α → Type v} → [DecidableEq α] → (a : α) → AList β → Option (β a) × AList β
-- Mathlib.Order.Category.BddDistLat
BddDistLat.mk.injEq : ∀ (toDistLat : DistLat) [isBoundedOrder : BoundedOrder ↑toDistLat] (toDistLat_1 : DistLat)
  (isBoundedOrder_1 : BoundedOrder ↑toDistLat_1),
  ({ toDistLat := toDistLat, isBoundedOrder := isBoundedOrder } =
      { toDistLat := toDistLat_1, isBoundedOrder := isBoundedOrder_1 }) =
    (toDistLat = toDistLat_1 ∧ isBoundedOrder ≍ isBoundedOrder_1)
-- Lean.Server.ServerTask
Lean.Server.ServerTask.BaseIO.mapTaskCostly : {α : Type u_1} → {β : Type} → (α → BaseIO β) → Lean.Server.ServerTask α → BaseIO (Lean.Server.ServerTask β)
-- Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
Subgroup.discreteTopology_iff_of_isFiniteRelIndex : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] {H K : Subgroup G},
  H ≤ K → ∀ [H.IsFiniteRelIndex K], DiscreteTopology ↥H ↔ DiscreteTopology ↥K
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.quotEquivQuotMap_symm_apply_mk : ∀ {R : Type u_1} [inst : CommRing R] (f g : Polynomial R) (I : Ideal R),
  (AdjoinRoot.quotEquivQuotMap f I).symm
      ((Ideal.Quotient.mk (Ideal.span {Polynomial.map (Ideal.Quotient.mk I) f}))
        (Polynomial.map (Ideal.Quotient.mk I) g)) =
    (Ideal.Quotient.mk (Ideal.map (AdjoinRoot.of f) I)) ((AdjoinRoot.mk f) g)
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.gluing_V : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (x : 𝒰.I₀ × 𝒰.I₀),
  (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).V x =
    match x with
    | (i, j) => AlgebraicGeometry.Scheme.Pullback.v 𝒰 f g i j
-- Mathlib.Data.Set.Countable
Set.Countable.of_sdiff : ∀ {α : Type u} {s t : Set α}, (s \ t).Countable → t.Countable → s.Countable
-- Mathlib.LinearAlgebra.TensorProduct.Finiteness
/-- Variation of `TensorProduct.exists_finite_submodule_of_setFinite` where `M` and `N` are
already submodules.  -/
TensorProduct.exists_finite_submodule_of_setFinite' : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {M₁ : Submodule R M} {N₁ : Submodule R N}
  (s : Set (TensorProduct R ↥M₁ ↥N₁)),
  s.Finite →
    ∃ M' N',
      ∃ (hM : M' ≤ M₁) (hN : N' ≤ N₁),
        Module.Finite R ↥M' ∧
          Module.Finite R ↥N' ∧ s ⊆ ↑(TensorProduct.map (Submodule.inclusion hM) (Submodule.inclusion hN)).range
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.fold_hom : ∀ {α β γ₁ γ₂ : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β} (f : γ₁ → γ₂)
  {g₁ : γ₁ → β → γ₁} {g₂ : γ₂ → β → γ₂} {init : γ₁},
  (∀ (x : γ₁) (y : β), g₂ (f x) y = f (g₁ x y)) → Std.IterM.fold g₂ (f init) it = f <$> Std.IterM.fold g₁ init it
-- Mathlib.Algebra.Torsor.Defs
Equiv.coe_vaddConst : ∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [inst_1 : AddTorsor G P] (p : P),
  ⇑(Equiv.vaddConst p) = fun v => v +ᵥ p
-- Mathlib.Topology.Category.CompHausLike.Limits
/-- The functor to `TopCat` preserves pullbacks.  -/
CompHausLike.instPreservesLimitTopCatWalkingCospanCospanCompHausLikeToTop : ∀ {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [CompHausLike.HasExplicitPullback f g],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) (CompHausLike.compHausLikeToTop P)
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- We say that the action of `M` on `α` has `MeasurableVAdd₂` if the map
`(c, x) ↦ c +ᵥ x` is a measurable function.  -/
MeasurableVAdd₂ : (M : Type u_2) → (α : Type u_3) → [VAdd M α] → [MeasurableSpace M] → [MeasurableSpace α] → Prop
-- Init.Data.Vector.Lemmas
Vector.getElem?_eq_some_getElem_iff : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} (h : i < n), xs[i]? = some xs[i] ↔ True
-- Std.Tactic.BVDecide.LRAT.Internal.Convert
/-- Turn a `CNF PosFin` into the representation used by the LRAT checker.
 -/
Std.Tactic.BVDecide.LRAT.Internal.CNF.convertLRAT' : {n : ℕ} →
  Std.Sat.CNF (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) →
    Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n))
-- Mathlib.Data.ENat.Basic
ENat.add_eq_top : ∀ {a b : ℕ∞}, a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤
-- Init.Data.UInt.Lemmas
USize.toUInt64_ofNatTruncate_of_le : ∀ {n : ℕ},
  USize.size ≤ n →
    (USize.ofNatClamp n).toUInt64 = UInt64.ofNatLT (USize.size - 1) USize.toUInt64_ofNatClamp_of_le._proof_1
-- Lean.Meta.LetToHave
Lean.Meta.LetToHave.instInhabitedResult.default : Lean.Meta.LetToHave.Result✝