mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.FGModuleCat.Basic
FGModuleCat.of_carrier : ∀ (R : Type u) [inst : Ring R] (V : Type v) [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : Module.Finite R V], ↑(FGModuleCat.of R V) = V
-- Lean.Meta.MkIffOfInductiveProp
/-- Iterate over two lists, if the first element of the first list is `false`, insert `none` into the
result and continue with the tail of first list. Otherwise, wrap the first element of the second
list with `some` and continue with the tails of both lists. Return when either list is empty.

Example:
```
listBoolMerge [false, true, false, true] [0, 1, 2, 3, 4] = [none, (some 0), none, (some 1)]
```
 -/
_private.Lean.Meta.MkIffOfInductiveProp.0.Lean.Meta.listBoolMerge : {α : Type u_1} → List Bool → List α → List (Option α)
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.List.anyM.eq_2 : ∀ {m : Type → Type u} [inst : Monad m] {α : Type v} (p : α → m Bool) (a : α) (as : List α),
  List.anyM p (a :: as) = do
    let __do_lift ← p a
    match __do_lift with
      | true => pure true
      | false => List.anyM p as
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.isNormal_aleph : Order.IsNormal ⇑Cardinal.aleph
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_filter_le_size : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool}, (Std.ExtHashMap.filter f m).size ≤ m.size
-- Mathlib.Algebra.Group.Basic
inv_zpow : ∀ {α : Type u_1} [inst : DivisionMonoid α] (a : α) (n : ℤ), a⁻¹ ^ n = (a ^ n)⁻¹
-- Mathlib.Algebra.Order.Positive.Ring
Positive.instSemigroupSubtypeLtOfNat : {R : Type u_2} → [inst : Semiring R] → [inst_1 : PartialOrder R] → [IsStrictOrderedRing R] → Semigroup { x // 0 < x }
-- Std.Data.DTreeMap.Internal.Cell
/-- Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Cell.getEntry? : {α : Type u} →
  {β : α → Type v} → [inst : Ord α] → {k : α} → Std.DTreeMap.Internal.Cell α β (compare k) → Option ((a : α) × β a)
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.mk.congr_simp : ∀ {α : Type u_6} [inst : NonUnitalNonAssocSemiring α] (toAddMonoidHom toAddMonoidHom_1 : α →+ α)
  (e_toAddMonoidHom : toAddMonoidHom = toAddMonoidHom_1)
  (map_mul_left' : ∀ (a b : α), (↑toAddMonoidHom).toFun (a * b) = a * (↑toAddMonoidHom).toFun b)
  (map_mul_right' : ∀ (a b : α), (↑toAddMonoidHom).toFun (a * b) = (↑toAddMonoidHom).toFun a * b),
  { toAddMonoidHom := toAddMonoidHom, map_mul_left' := map_mul_left', map_mul_right' := map_mul_right' } =
    { toAddMonoidHom := toAddMonoidHom_1, map_mul_left' := ⋯, map_mul_right' := ⋯ }
-- Init.Data.UInt.Lemmas
UInt64.toUInt8_div : ∀ (a b : UInt64), a < 256 → b < 256 → (a / b).toUInt8 = a.toUInt8 / b.toUInt8
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
/-- The Radon-Nikodym derivative of `f ν` with respect to `ν` is `f`.  -/
MeasureTheory.Measure.rnDeriv_withDensity : ∀ {α : Type u_1} {m : MeasurableSpace α} (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite ν] {f : α → ENNReal},
  Measurable f → (ν.withDensity f).rnDeriv ν =ᵐ[ν] f
-- Mathlib.RingTheory.Localization.Defs
/-- If `S`, `Q` are localizations of `R` and `P` at submonoids `M, T` respectively, an
isomorphism `j : R ≃+* P` such that `j(M) = T` induces an isomorphism of localizations
`S ≃+* Q`.  -/
IsLocalization.ringEquivOfRingEquiv : {R : Type u_1} →
  [inst : CommSemiring R] →
    {M : Submonoid R} →
      (S : Type u_2) →
        [inst_1 : CommSemiring S] →
          [inst_2 : Algebra R S] →
            {P : Type u_3} →
              [inst_3 : CommSemiring P] →
                [IsLocalization M S] →
                  {T : Submonoid P} →
                    (Q : Type u_4) →
                      [inst_5 : CommSemiring Q] →
                        [inst_6 : Algebra P Q] →
                          [IsLocalization T Q] → (h : R ≃+* P) → Submonoid.map h.toMonoidHom M = T → S ≃+* Q
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.functorProdFunctorEquiv_functor : ∀ (A : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  (C : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} C],
  (CategoryTheory.functorProdFunctorEquiv A B C).functor = CategoryTheory.prodFunctorToFunctorProd A B C
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.algebra : {α : Type u_1} →
  [inst : TopologicalSpace α] →
    {R : Type u_2} →
      [inst_1 : CommSemiring R] →
        {A : Type u_3} →
          [inst_2 : TopologicalSpace A] →
            [inst_3 : Semiring A] → [Algebra R A] → [inst_5 : IsTopologicalSemiring A] → Algebra R C(α, A)
-- Mathlib.Order.Filter.Extr
IsExtrOn.inter : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsExtrOn f s a → ∀ (t : Set α), IsExtrOn f (s ∩ t) a
-- Mathlib.Data.Finset.Prod
Finset.product_subset_product : ∀ {α : Type u_1} {β : Type u_2} {s s' : Finset α} {t t' : Finset β}, s ⊆ s' → t ⊆ t' → s ×ˢ t ⊆ s' ×ˢ t'
-- Mathlib.Order.Partition.Basic
Partition.Rel.exists : ∀ {α : Type u_1} {x y : α} {u : Set α} {P : Partition u}, P.Rel x y → ∃ t ∈ P, x ∈ t ∧ y ∈ t
-- Init.Data.Dyadic.Basic
Dyadic.add.eq_3 : ∀ (n₁ k₁ : ℤ) (hn₁ : n₁ % 2 = 1) (n₂ k₂ : ℤ) (hn₂ : n₂ % 2 = 1),
  (Dyadic.ofOdd n₁ k₁ hn₁).add (Dyadic.ofOdd n₂ k₂ hn₂) =
    match k₁ - k₂ with
    | 0 => Dyadic.ofIntWithPrec (n₁ + n₂) k₁
    | Int.ofNat d@hd:d'.succ => Dyadic.ofOdd (n₁ + n₂ <<< d) k₁ ⋯
    | Int.negSucc d => Dyadic.ofOdd (n₁ <<< (d + 1) + n₂) k₂ ⋯
-- Mathlib.Algebra.Order.Group.Indicator
Set.indicator_le_indicator' : ∀ {α : Type u_2} {M : Type u_3} [inst : Preorder M] [inst_1 : Zero M] {s : Set α} {f g : α → M} {a : α},
  (a ∈ s → f a ≤ g a) → s.indicator f a ≤ s.indicator g a
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
MeasureTheory.condExp_mono : ∀ {α : Type u_1} {E : Type u_3} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → E}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] [inst_3 : PartialOrder E]
  [ClosedIciTopology E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E],
  MeasureTheory.Integrable f μ → MeasureTheory.Integrable g μ → f ≤ᵐ[μ] g → μ[f | m] ≤ᵐ[μ] μ[g | m]
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- The morphism in the homotopy category of a `2`-truncated simplicial set that
is induced by an edge.  -/
SSet.Truncated.HomotopyCategory.homMk : {V : SSet.Truncated 2} →
  {x₀ x₁ : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })} →
    SSet.Truncated.Edge x₀ x₁ → (SSet.Truncated.HomotopyCategory.mk x₀ ⟶ SSet.Truncated.HomotopyCategory.mk x₁)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.ordCompare_minKeyD_modify_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] {t : Std.TreeMap α β compare} {k : α} {f : β → β}
  {fallback : α}, compare ((t.modify k f).minKeyD fallback) (t.minKeyD fallback) = Ordering.eq
-- Mathlib.Data.Set.Lattice
/-- **Alias** of `Set.ofPred_forall`. -/
Set.setOf_forall : ∀ {β : Type u_2} {ι : Sort u_5} (p : ι → β → Prop), {x | ∀ (i : ι), p i x} = ⋂ i, {x | p i x}
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.atTop_add_nonneg : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedAddMonoid M] {l : Filter α}
  {f g : α → M},
  Filter.Tendsto f l Filter.atTop → (∀ (x : α), 0 ≤ g x) → Filter.Tendsto (fun x => f x + g x) l Filter.atTop
-- Init.Data.String.Lemmas.FindPos
String.posLT_eq_iff : ∀ {s : String} {p : String.Pos.Raw} {h : 0 < p} {q : s.Pos},
  s.posLT p h = q ↔ q.offset < p ∧ ∀ (q' : s.Pos), q'.offset < p → q' ≤ q
-- Mathlib.Order.Filter.Cofinite
/-- Given a family of maps `f i : α i → β i` and a family of filters `l i : Filter (α i)`,
if all but finitely many of `f i` are surjective,
then the indexed product of `f i`s maps the indexed product of the filters `l i`
to the indexed products of their pushforwards under individual `f i`s.

See also `map_piMap_pi_finite` for the case of a finite index type.
 -/
Filter.map_piMap_pi : ∀ {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} {f : (i : ι) → α i → β i},
  (∀ᶠ (i : ι) in Filter.cofinite, Function.Surjective (f i)) →
    ∀ (l : (i : ι) → Filter (α i)), Filter.map (Pi.map f) (Filter.pi l) = Filter.pi fun i => Filter.map (f i) (l i)
-- Mathlib.Topology.Path
/-- Image of a path from `x` to `y` by a continuous map  -/
Path.map : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → {x y : X} → Path x y → {f : X → Y} → Continuous f → Path (f x) (f y)
-- Mathlib.Computability.PartrecCode
/-- There are only countably many computable functions `ℕ → ℕ`.  -/
Nat.Partrec.Code.instCountableSubtypeForallComputable : Countable { f // Computable f }
-- Aesop.Search.Queue
Aesop.BestFirstQueue.ActiveGoal.le : Aesop.BestFirstQueue.ActiveGoal → Aesop.BestFirstQueue.ActiveGoal → Bool
-- Init.Data.UInt.Lemmas
UInt16.toUInt32_ofNat' : ∀ {n : ℕ}, n < UInt16.size → (UInt16.ofNat n).toUInt32 = UInt32.ofNat n
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.Splits.toByteArray_eq_left : ∀ {s : String.Slice} {p : s.Pos} {t₁ t₂ : String},
  p.Splits t₁ t₂ → t₁.toByteArray = s.copy.toByteArray.extract 0 p.offset.byteIdx
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.δ_v : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (n m : ℤ) (hnm : n + 1 = m) (z : CochainComplex.HomComplex.Cochain F G n) (p q : ℤ)
  (hpq : p + m = q) (q₁ q₂ : ℤ) (hq₁ : q₁ = q - 1) (hq₂ : p + 1 = q₂),
  (CochainComplex.HomComplex.δ n m z).v p q hpq =
    CategoryTheory.CategoryStruct.comp (z.v p q₁ ⋯) (G.d q₁ q) +
      m.negOnePow • CategoryTheory.CategoryStruct.comp (F.d p q₂) (z.v q₂ q ⋯)
-- Lean.Meta.AppBuilder
/-- Returns `eq_true h`  -/
Lean.Meta.mkEqTrueCore : Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.Algebra.Star.Basic
/-- This is not a simp lemma, since we usually want simp to keep `starRingEnd` bundled.
For example, for complex conjugation, we don't want simp to turn `conj x`
into the bare function `star x` automatically since most lemmas are about `conj x`.  -/
starRingEnd_apply : ∀ {R : Type u} [inst : CommSemiring R] [inst_1 : StarRing R] (x : R), (starRingEnd R) x = star x
-- Mathlib.Algebra.Group.Basic
neg_add_eq_sub : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b : α), -a + b = b - a
-- Lean.Util.Path
Lean.modToFilePath : System.FilePath → Lean.Name → String → System.FilePath
-- Lean.Elab.PreDefinition.Structural.Eqns
/-- Creates the proof of the unfolding theorem for `declName` with type `type`. It

1. unfolds the function on the left to expose the `.brecOn` application
2. rewrites that using the `.brecOn.eq` theorem, unrolling it once
3. let-binds the last argument, which should be the `.brecOn.go` call of type `.below …`.
   This way subsequent steps (which may involve `simp`) do not touch it and do
   not break the definitional equality with the recursive calls on the RHS.
4. repeatedly splits `match` statements (because on the left we have `match` statements with extra
   `.below` arguments, and on the right we have the original `match` statements) until the goal
   is solved using `rfl` or `contradiction`.
 -/
_private.Lean.Elab.PreDefinition.Structural.Eqns.0.Lean.Elab.Structural.mkProof : Lean.Name → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.AlgebraicGeometry.PointsPi
AlgebraicGeometry.eq_top_of_sigmaSpec_subset_of_isCompact : ∀ {ι : Type u} (R : ι → CommRingCat) (U : (AlgebraicGeometry.Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens)
  (V : Set ↥(AlgebraicGeometry.Spec (CommRingCat.of ((i : ι) → ↑(R i))))),
  ↑(AlgebraicGeometry.Scheme.Hom.opensRange (AlgebraicGeometry.sigmaSpec R)) ⊆ V → IsCompact V → V ⊆ ↑U → U = ⊤
-- Mathlib.Order.InitialSeg
/-- If we have order embeddings between `α` and `β` whose ranges are initial segments, and `β` is a
well order, then `α` and `β` are order-isomorphic.  -/
InitialSeg.antisymm : {α : Type u_1} →
  {β : Type u_2} →
    {r : α → α → Prop} → {s : β → β → Prop} → [IsWellOrder β s] → InitialSeg r s → InitialSeg s r → r ≃r s
-- Std.Sat.AIG.RelabelNat
/-- Build up a `State` that has all atoms of an `AIG` inserted.
 -/
Std.Sat.AIG.RelabelNat.State.ofAIGAux : {α : Type} →
  [inst : DecidableEq α] →
    [inst_1 : Hashable α] → (aig : Std.Sat.AIG α) → Std.Sat.AIG.RelabelNat.State α aig.decls aig.decls.size
-- Mathlib.Logic.Relation
Relation.EqvGen.symmGen_le_eqvGen : ∀ {α : Type u_1} (r : α → α → Prop), Relation.SymmGen r ≤ Relation.EqvGen r
-- Init.Data.Float.Model.Float32
/-- Converts an `Int` to a `Float32.Model`, returning positive zero on zero.  -/
Float32.Model.ofInt : ℤ → Float32.Model
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.forget_map_apply : ∀ {R S : CommRingCat} (f : R ⟶ S) (x : (CategoryTheory.forget CommRingCat).obj R),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget CommRingCat).map f)) x =
    (CategoryTheory.ConcreteCategory.hom f) x
-- Mathlib.Topology.Sets.Order
ClopenUpperSet.instBot : {α : Type u_1} → [inst : TopologicalSpace α] → [inst_1 : LE α] → Bot (ClopenUpperSet α)
-- Lean.Class
Lean.ClassState.mk.inj : ∀ {outParamMap outLevelParamMap outParamMap_1 outLevelParamMap_1 : Lean.SMap Lean.Name (Array ℕ)},
  { outParamMap := outParamMap, outLevelParamMap := outLevelParamMap } =
      { outParamMap := outParamMap_1, outLevelParamMap := outLevelParamMap_1 } →
    outParamMap = outParamMap_1 ∧ outLevelParamMap = outLevelParamMap_1
-- Mathlib.RingTheory.Ideal.Pointwise
Ideal.pointwise_smul_le_pointwise_smul_iff : ∀ {M : Type u_1} {R : Type u_3} [inst : Group M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] {a : M}
  {S T : Ideal R}, a • S ≤ a • T ↔ S ≤ T
-- Init.Data.Nat.Gcd
Nat.gcd_add_mul_right_right : ∀ (m n k : ℕ), m.gcd (n + k * m) = m.gcd n
-- Mathlib.Algebra.Module.Presentation.Tensor
Module.Relations.Solution.IsPresentation.tensor : ∀ {A : Type u} [inst : CommRing A] {M₁ : Type v₁} {M₂ : Type v₂} [inst_1 : AddCommGroup M₁] [inst_2 : AddCommGroup M₂]
  [inst_3 : Module A M₁] [inst_4 : Module A M₂] {relations₁ : Module.Relations A} {relations₂ : Module.Relations A}
  {solution₁ : relations₁.Solution M₁} {solution₂ : relations₂.Solution M₂},
  solution₁.IsPresentation → solution₂.IsPresentation → (solution₁.tensor solution₂).IsPresentation
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_eq_some : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k : α}, k ∈ t → t.getKey? k = some k
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.LHom.onTerm.eq_1 : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} (φ : L →ᴸ L') (i : α),
  φ.onTerm (FirstOrder.Language.var i) = FirstOrder.Language.var i
-- Mathlib.RingTheory.UniqueFactorizationDomain.Defs
UniqueFactorizationMonoid.irreducible_of_factor : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {a : α},
  ∀ x ∈ UniqueFactorizationMonoid.factors a, Irreducible x
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.isUnit_nnrpow_iff : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] (a : A) (y : NNReal),
  y ≠ 0 → autoParam (0 ≤ a) CFC.isUnit_nnrpow_iff._auto_1 → (IsUnit (a ^ y) ↔ IsUnit a)
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.OneCochain.instOne : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (G : CategoryTheory.Functor Cᵒᵖ GrpCat) →
      {I : Type w'} → (U : I → C) → One (CategoryTheory.PresheafOfGroups.OneCochain G U)
-- Mathlib.CategoryTheory.Category.Cat
/-- The natural transformation underlying a 2-morphism in `Cat`  -/
CategoryTheory.Cat.Hom₂.toNatTrans : {C D : CategoryTheory.Cat} → {F G : C ⟶ D} → CategoryTheory.Cat.Hom₂ F G → (F.toFunctor ⟶ G.toFunctor)
-- Mathlib.Data.ENat.Lattice
ENat.mul_sSup : ∀ {s : Set ℕ∞} {a : ℕ∞}, a * sSup s = ⨆ b ∈ s, a * b
-- Mathlib.Algebra.Lie.AdjointAction.Derivation
/-- A derivation `D` belongs to the ideal range of the adjoint action iff it is of the form `ad x`
for some `x` in the Lie algebra `L`.  -/
LieDerivation.mem_ad_idealRange_iff : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  {D : LieDerivation R L L}, D ∈ (LieDerivation.ad R L).idealRange ↔ ∃ x, (LieDerivation.ad R L) x = D
-- Init.Data.Int.Linear
Int.Internal.Linear.dvd_solve_combine_cert : ℤ → Int.Internal.Linear.Poly → ℤ → Int.Internal.Linear.Poly → ℤ → Int.Internal.Linear.Poly → ℤ → ℤ → ℤ → Bool
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.desc' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} [CategoryTheory.Balanced C],
  S.Exact →
    ∀ {A : C} (k : S.X₂ ⟶ A),
      CategoryTheory.CategoryStruct.comp S.f k = 0 →
        ∀ [CategoryTheory.Epi S.g], ∃ l, CategoryTheory.CategoryStruct.comp S.g l = k
-- Mathlib.Order.SuccPred.CompleteLinearOrder
iSup_Iio_eq_self_iff_isSuccPrelimit : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrderBot α] {x : α}, ⨆ a, ↑a = x ↔ Order.IsSuccPrelimit x
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- If `y` is a conjugate root of `x`, then `-y` is a conjugate root of `-x`.
 -/
IsConjRoot.neg : ∀ {K : Type u_2} {S : Type u_4} [inst : CommRing S] [inst_1 : Field K] [inst_2 : Algebra K S] {x y : S},
  IsConjRoot K x y → IsConjRoot K (-x) (-y)
-- Mathlib.CategoryTheory.Preadditive.EilenbergMoore
CategoryTheory.Comonad.coalgebraPreadditive_homGroup_add_f : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (U : CategoryTheory.Comonad C) [inst_2 : U.Additive] (F G : U.Coalgebra) (α β : F ⟶ G), (α + β).f = α.f + β.f
-- Mathlib.Tactic.Translate.UnfoldBoundary
Mathlib.Tactic.UnfoldBoundary.instInhabitedUnfoldBoundaries : Inhabited Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Under.isoMk_inv_right : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T}
  [inst_1 : Q.IsMultiplicative] [inst_2 : Q.RespectsIso] {A B : P.Under Q X} (f : A.right ≅ B.right)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp A.hom f.hom = B.hom)
      CategoryTheory.MorphismProperty.Under.isoMk._auto_1),
  (CategoryTheory.MorphismProperty.Under.isoMk f w).inv.right = f.inv
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
DirectedOn.le_ciInf_set_iff : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderInf α] {ι : Type u_5} {s : Set ι} {f : ι → α} {a : α},
  s.Nonempty → DirectedOn (fun x1 x2 => x2 ≤ x1) (f '' s) → BddBelow (f '' s) → (a ≤ ⨅ i, f ↑i ↔ ∀ i ∈ s, a ≤ f i)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.PositiveCompacts.interior_nonempty' : ∀ {α : Type u_4} [inst : TopologicalSpace α] (self : TopologicalSpace.PositiveCompacts α),
  (interior self.carrier).Nonempty
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.faithfulSMul : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring S] [inst_1 : SMulZeroClass R S] [FaithfulSMul R S]
  [Nonempty M], FaithfulSMul R (AddMonoidAlgebra S M)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isSome_min?_of_isSome_min?_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  (t.erase k).min?.isSome = true → t.min?.isSome = true
-- Std.Sat.AIG.CNF
/-- Given an atom assignment, produce an assignment that will always satisfy the CNF generated by our
Tseitin transformation. This is done by combining the atom assignment with an assignment for the
auxiliary variables, that just evaluates the AIG at the corresponding node.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.cnfSatAssignment : Std.Sat.AIG ℕ → (ℕ → Bool) → ℕ → Bool
-- Init.Data.Nat.Basic
Nat.sub_le_sub_right : ∀ {n m : ℕ}, n ≤ m → ∀ (k : ℕ), n - k ≤ m - k
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instOrdDiagnosticSeverity.ord : Lean.Lsp.DiagnosticSeverity → Lean.Lsp.DiagnosticSeverity → Ordering
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.image_basicOpen : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] {U : X.Opens}
  (r : ↑(X.presheaf.obj (Opposite.op U))),
  (AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj (X.basicOpen r) =
    Y.basicOpen ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appIso f U).inv) r)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.instHasPullbacksAlongCompOfIsStableUnderBaseChangeAlong : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z) [P.IsStableUnderBaseChangeAlong g] [P.HasPullbacksAlong f] [P.HasPullbacksAlong g],
  P.HasPullbacksAlong (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.RingTheory.Congruence.Basic
RingCon.coe_bot : ∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R], ⇑⊥ = Eq
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.lift_whiskerLeft : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : Z ⟶ W),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f g)
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y h) =
    CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CategoryStruct.comp g h)
-- Init.Prelude
/-- An opaque reference to the `Methods` object. This is done to break a
dependency cycle: the `Methods` involve `MacroM` which has not been defined yet.  -/
Lean.Macro.Context.methods : Lean.Macro.Context → Lean.Macro.MethodsRef
-- Mathlib.Algebra.Algebra.Subalgebra.Centralizer
Subalgebra.centralizer_coe_iSup : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : Algebra R A] {ι : Sort u_3}
  (S : ι → Subalgebra R A), Subalgebra.centralizer R ↑(⨆ i, S i) = ⨅ i, Subalgebra.centralizer R ↑(S i)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_eq_some_getD_of_contains : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {a : α}
  {fallback : β a}, m.contains a = true → m.get? a = some (m.getD a fallback)
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.isPartition_single : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {x : ι → ℝ} (h : x ∈ BoxIntegral.Box.Icc I),
  (BoxIntegral.TaggedPrepartition.single I I ⋯ x h).IsPartition
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasDerivAt.iterate : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜) {f : 𝕜 → 𝕜} {f' : 𝕜},
  HasDerivAt f f' x → f x = x → ∀ (n : ℕ), HasDerivAt f^[n] (f' ^ n) x
-- Mathlib.Analysis.ODE.PicardLindelof
ODE.FunSpace.next_apply : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E → E} {tmin tmax : ℝ}
  {t₀ : ↑(Set.Icc tmin tmax)} {x₀ x : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K)
  (hx : x ∈ Metric.closedBall x₀ ↑r) (α : ODE.FunSpace t₀ x₀ r L) {t : ↑(Set.Icc tmin tmax)},
  (ODE.FunSpace.next hf hx α).toFun t = ODE.picard f (↑t₀) x α.compProj ↑t
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.atom_odd : ∀ {R : Type u_1} [inst : CommRing R] (W : ℤ → R) (a b : ℤ),
  IsEllipticNet.atom W (2 * a + 1) (2 * b + 1) = W (a + b + 1) * W (a - b)
-- Std.Http.Internal.IndexMultiMap
/-- Removes a key and all its values from the map. This function rebuilds the entire
`entries` array and `indexes` map from scratch by filtering out all pairs whose
key matches, then re-inserting the survivors.
 -/
Std.Internal.IndexMultiMap.erase : {α : Type u} →
  {β : Type v} →
    [inst : BEq α] →
      [inst_1 : Hashable α] →
        [EquivBEq α] → [LawfulHashable α] → Std.Internal.IndexMultiMap α β → α → Std.Internal.IndexMultiMap α β
-- Lean.Meta.Match.MatcherInfo
/-- Overlap assumption (for splitters only)  -/
Lean.Meta.Match.AltParamInfo.numOverlaps : Lean.Meta.Match.AltParamInfo → ℕ