mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Logic.Encodable.Basic
/-- A constructive version of `Classical.skolem` for `Encodable` types.  -/
Encodable.skolem : ∀ {α : Type u_1} {β : α → Type u_2} {P : (x : α) → β x → Prop} [(a : α) → Encodable (β a)]
  [(x : α) → (y : β x) → Decidable (P x y)], (∀ (x : α), ∃ y, P x y) ↔ ∃ f, ∀ (x : α), P x (f x)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.one_braiding : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : C) [inst_3 : CategoryTheory.MonObj X]
  [inst_4 : CategoryTheory.MonObj Y],
  CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (β_ X Y).hom = CategoryTheory.MonObj.one
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotientMap.congr_simp : ∀ {R : Type u} [inst : Ring R] {S : Type v} [inst_1 : Ring S] {I : Ideal R} (J : Ideal S) [inst_2 : I.IsTwoSided]
  [inst_3 : J.IsTwoSided] (f f_1 : R →+* S) (e_f : f = f_1) (hIJ : I ≤ Ideal.comap f J),
  Ideal.quotientMap J f hIJ = Ideal.quotientMap J f_1 ⋯
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.copy.eq_1 : ∀ {α : Type u} [inst : AddMonoid α] (u : AddUnits α) (val : α) (hv : val = ↑u) (inv : α) (hi : inv = ↑(-u)),
  u.copy val hv inv hi = { val := val, neg := inv, val_neg := ⋯, neg_val := ⋯ }
-- Mathlib.Probability.Distributions.Gaussian.CharFun
/-- Two Gaussian measures are equal if they have same mean and same covariance. This is
`IsGaussian.ext_covarianceBilinDual` specialized to Hilbert spaces.  -/
ProbabilityTheory.IsGaussian.ext : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [SecondCountableTopology E] [CompleteSpace E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {μ : MeasureTheory.Measure E} [inst_5 : InnerProductSpace ℝ E]
  {ν : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ] [ProbabilityTheory.IsGaussian ν],
  ∫ (x : E), id x ∂μ = ∫ (x : E), id x ∂ν →
    ProbabilityTheory.covarianceBilin μ = ProbabilityTheory.covarianceBilin ν → μ = ν
-- Mathlib.Order.Filter.EventuallyConst
Filter.eventuallyConst_atTop : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : SemilatticeSup α] [Nonempty α],
  Filter.EventuallyConst f Filter.atTop ↔ ∃ i, ∀ (j : α), i ≤ j → f j = f i
-- Init.Data.Range.Polymorphic.Basic
/-- This typeclass provides support for the size function for ranges with closed lower bound
\(`Ric.size`,
`Rio.size` and
`Rii.size`\).

The returned size should be equal to the number of elements returned by `toList`. This
condition is captured by the typeclass
`LawfulHasSize`.
 -/
Std.Rxi.HasSize : Type u → Type u
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ico_union_Icc_eq_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, a ≤ b → b ≤ c → Set.Ico a b ∪ Set.Icc b c = Set.Icc a c
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.Nonempty.sub : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Sub α] {s t : Finset α}, s.Nonempty → t.Nonempty → (s - t).Nonempty
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.ClassifyResult.commRing.sizeOf_spec : ∀ (id : ℕ), sizeOf (Lean.Meta.Sym.Arith.ClassifyResult.commRing id) = 1 + sizeOf id
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.Anisotropic.eq_zero_iff : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {Q : QuadraticMap R M N},
  Q.Anisotropic → ∀ {x : M}, Q x = 0 ↔ x = 0
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.continuous_restrictScalars : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E]
  [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [ContinuousSMul 𝕜 E] {F : Type u_3} [inst_5 : AddCommGroup F]
  [inst_6 : TopologicalSpace F] [inst_7 : IsTopologicalAddGroup F] [inst_8 : Module 𝕜 F] (𝕜' : Type u_4)
  [inst_9 : NontriviallyNormedField 𝕜'] [inst_10 : NormedAlgebra 𝕜' 𝕜] [inst_11 : Module 𝕜' E]
  [inst_12 : IsScalarTower 𝕜' 𝕜 E] [inst_13 : Module 𝕜' F] [inst_14 : IsScalarTower 𝕜' 𝕜 F],
  Continuous (ContinuousLinearMap.restrictScalars 𝕜')
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.instAdditiveModuleCatCarrierModulesSpecOfFunctor : ∀ {R : CommRingCat}, (AlgebraicGeometry.tilde.functor R).Additive
-- Mathlib.Algebra.Group.Equiv.Defs
/-- The `MulHom` underlying a `MulEquiv`.  -/
MulEquiv.toMulHom : {M : Type u_9} → {N : Type u_10} → [inst : Mul M] → [inst_1 : Mul N] → M ≃* N → M →ₙ* N
-- Std.Data.HashSet.Raw
Std.HashSet.Raw.instForMOfMonad : {α : Type u} → {m : Type v → Type w} → [Monad m] → ForM m (Std.HashSet.Raw α) α
-- Std.Time.Time.Unit.Basic
/-- Converts a `Minute.Offset` to a `Second.Offset`.
 -/
Std.Time.Minute.Offset.toSeconds : Std.Time.Minute.Offset → Std.Time.Second.Offset
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.DischargeResult.noConfusionType : Sort v✝ → Lean.Meta.Simp.DischargeResult → Lean.Meta.Simp.DischargeResult → Sort v✝
-- Init.Data.AC
Lean.Data.AC.Expr.brecOn.eq : ∀ {motive : Lean.Data.AC.Expr → Sort u} (t : Lean.Data.AC.Expr)
  (F_1 : (t : Lean.Data.AC.Expr) → Lean.Data.AC.Expr.below t → motive t),
  Lean.Data.AC.Expr.brecOn t F_1 = F_1 t (Lean.Data.AC.Expr.brecOn.go t F_1).2
-- Mathlib.MeasureTheory.Integral.CircleIntegral
measurable_circleMap : ∀ (c : ℂ) (R : ℝ), Measurable (circleMap c R)
-- Mathlib.Topology.Order.Monotone
csSup_mem_closure : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  {s : Set α}, s.Nonempty → BddAbove s → sSup s ∈ closure s
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.toDeleteEdges_cons : ∀ {V : Type u} {G : SimpleGraph V} (s : Set (Sym2 V)) {u v w : V} (h : G.Adj u v) (p : G.Walk v w)
  (hp : ∀ e ∈ (SimpleGraph.Walk.cons h p).edges, e ∉ s),
  SimpleGraph.Walk.toDeleteEdges s (SimpleGraph.Walk.cons h p) hp =
    SimpleGraph.Walk.cons ⋯ (SimpleGraph.Walk.toDeleteEdges s p ⋯)
-- Mathlib.RingTheory.ZariskisMainTheorem
Algebra.not_isStronglyTranscendental_of_weaklyQuasiFiniteAt : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsReduced S] {x : S},
  (Polynomial.aeval x).Finite →
    ∀ (P : Ideal S) [inst_4 : P.IsPrime] [Algebra.WeaklyQuasiFiniteAt R P], ¬IsStronglyTranscendental R x
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cos_sub_sin_I : ∀ (x : ℂ), Complex.cos x - Complex.sin x * Complex.I = Complex.exp (-x * Complex.I)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} {A B : CategoryTheory.StructuredArrow S T} (f g : A ⟶ B),
  f = g ↔ CategoryTheory.StructuredArrow.Hom.right f = CategoryTheory.StructuredArrow.Hom.right g
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.liftRingHom_apply : ∀ {K : Type u} [inst : Field K] {L : Type u_1} [inst_1 : Field L] (φ : Polynomial K →+* L)
  (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (f : RatFunc K),
  (RatFunc.liftRingHom φ hφ) f = φ f.num / φ f.denom
-- Init.Data.String.Subslice
String.Slice.Subslice.mk.inj : ∀ {s : String.Slice} {startInclusive endExclusive : s.Pos}
  {startInclusive_le_endExclusive : startInclusive ≤ endExclusive} {startInclusive_1 endExclusive_1 : s.Pos}
  {startInclusive_le_endExclusive_1 : startInclusive_1 ≤ endExclusive_1},
  { startInclusive := startInclusive, endExclusive := endExclusive,
        startInclusive_le_endExclusive := startInclusive_le_endExclusive } =
      { startInclusive := startInclusive_1, endExclusive := endExclusive_1,
        startInclusive_le_endExclusive := startInclusive_le_endExclusive_1 } →
    startInclusive = startInclusive_1 ∧ endExclusive = endExclusive_1
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.isNormal_mul_right : ∀ {a : Ordinal.{u_4}}, 0 < a → Order.IsNormal fun x => a * x
-- Mathlib.Analysis.Complex.Basic
Complex.conjLIE_symm : Complex.conjLIE.symm = Complex.conjLIE
-- Mathlib.Order.Ideal
Order.Ideal.IsProper.notMem_or_compl_notMem : ∀ {P : Type u_1} [inst : BooleanAlgebra P] {x : P} {I : Order.Ideal P}, I.IsProper → x ∉ I ∨ xᶜ ∉ I
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_alter_eq_self_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)},
  k ∈ t → (f (t.get? k)).isSome = true → (t.alter k f).size = t.size
-- Plausible.DeriveArbitrary
/-- Takes the name of a constructor for an algebraic data type and returns an array
containing `(argument_name, argument_type)` pairs.

If the algebraic data type is defined using anonymous constructor argument syntax, i.e.
```
inductive T where
  C1 : τ1 → … → τn
  …
```
Lean produces macro scopes when we try to access the names for the constructor args.
In this case, we remove the macro scopes so that the name is user-accessible.
(This will result in constructor argument names being non-unique in the array
that is returned -- it is the caller's responsibility to produce fresh names.)
 -/
_private.Plausible.DeriveArbitrary.0.Plausible.getCtorArgsNamesAndTypes : Lean.Elab.Deriving.Header → Lean.InductiveVal → Lean.Name → Lean.MetaM (Array (Lean.Name × Lean.Expr))
-- Mathlib.NumberTheory.Padics.MahlerBasis
/-- The function `mahler k` extends `n ↦ n.choose k` on `ℕ`.  -/
mahler_natCast_eq : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (k n : ℕ), (mahler k) ↑n = ↑(n.choose k)
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgsResult.mk.sizeOf_spec : ∀ (ctx : Lean.Meta.Simp.Context) (simprocs : Lean.Meta.Simp.SimprocsArray)
  (simpArgs : Array (Lean.Syntax × Lean.Elab.Tactic.ElabSimpArgResult)),
  sizeOf { ctx := ctx, simprocs := simprocs, simpArgs := simpArgs } = 1 + sizeOf ctx + sizeOf simprocs + sizeOf simpArgs
-- Mathlib.Order.Heyting.Hom
BiheytingHom.toFun_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : BiheytingAlgebra α] [inst_1 : BiheytingAlgebra β] {f : BiheytingHom α β},
  f.toFun = ⇑f
-- Mathlib.Algebra.Order.Ring.WithTop
WithBot.instPosMulStrictMono : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] [inst_2 : Preorder α] [PosMulStrictMono α],
  PosMulStrictMono (WithBot α)
-- Mathlib.Order.CompleteLattice.Basic
sInf_image2 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CompleteLattice α] {f : β → γ → α} {s : Set β} {t : Set γ},
  sInf (Set.image2 f s t) = ⨅ a ∈ s, ⨅ b ∈ t, f a b
-- Batteries.Data.PairingHeap
/-- `O(n)`. Convert the heap to an array in arbitrary order.  -/
Batteries.PairingHeapImp.Heap.toArrayUnordered : {α : Type u_1} → Batteries.PairingHeapImp.Heap α → Array α
-- Mathlib.RingTheory.Nakayama
Submodule.le_of_le_smul_of_le_jacobson_bot : ∀ {R : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
  {N N' : Submodule R M}, N'.FG → I ≤ ⊥.jacobson → N' ≤ N ⊔ I • N' → N' ≤ N
-- Mathlib.Data.Finset.Prod
Finset.offDiag_insert : ∀ {α : Type u_1} {s : Finset α} [inst : DecidableEq α] {a : α},
  a ∉ s → (insert a s).offDiag = s.offDiag ∪ {a} ×ˢ s ∪ s ×ˢ {a}
-- Mathlib.Data.Set.Piecewise
Set.range_piecewise : ∀ {α : Type u_1} {β : Type u_2} (s : Set α) [inst : (j : α) → Decidable (j ∈ s)] (f g : α → β),
  Set.range (s.piecewise f g) = f '' s ∪ g '' sᶜ
-- Init.Data.List.MinMaxOn
List.minOn_cons_cons : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {a b : α} {l : List α} {f : α → β},
  List.minOn f (a :: b :: l) ⋯ = List.minOn f (minOn f a b :: l) ⋯
-- Mathlib.Order.Heyting.Basic
GeneralizedHeytingAlgebra.mk : {α : Type u_4} →
  [toLattice : Lattice α] →
    [toOrderTop : OrderTop α] → [toHImp : HImp α] → (∀ (a b c : α), a ≤ b ⇨ c ↔ a ⊓ b ≤ c) → GeneralizedHeytingAlgebra α
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.addCommSemigroup : {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] → AddCommSemigroup (TensorProduct R M N)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule
/-- If `N₁` and `N₂` are submodule with `N₁ ≤ N₂`, this is the associated inclusion
of presheaves of modules.  -/
PresheafOfModules.Submodule.homOfLE : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      {M : PresheafOfModules R} → {N₁ N₂ : M.Submodule} → N₁ ≤ N₂ → (N₁.toPresheafOfModules ⟶ N₂.toPresheafOfModules)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.unitOfList_eq_insertManyIfNewUnit_empty : ∀ {α : Type u} {cmp : α → α → Ordering} {l : List α}, Std.TreeMap.unitOfList l cmp = ∅.insertManyIfNewUnit l
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.fromSpecResidueField.hcongr_2 : ∀ (X X' : AlgebraicGeometry.Scheme),
  X = X' → ∀ (x : ↥X) (x' : ↥X'), x ≍ x' → X.fromSpecResidueField x ≍ X'.fromSpecResidueField x'
-- Mathlib.Data.ULift
ULift.instDecidableEq_mathlib : {α : Type u} → [DecidableEq α] → DecidableEq (ULift.{u_1, u} α)
-- Mathlib.Algebra.Ring.ULift
ULift.commSemiring : {R : Type u} → [CommSemiring R] → CommSemiring (ULift.{u_1, u} R)
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.spanFunctorIsoIndexFunctor_hom_app_hom_hom_apply_coe : ∀ {I : Type u} {C : Set (I → Bool)} [inst : (s : Finset I) → (i : I) → Decidable (i ∈ s)] (hC : IsCompact C)
  (X : (Finset I)ᵒᵖ) (x : ↑(Profinite.NobelingProof.π C fun x => x ∈ Opposite.unop X))
  (i : { i // (fun x => x ∈ Opposite.unop X) i }),
  ↑((TopCat.Hom.hom ((Profinite.NobelingProof.spanFunctorIsoIndexFunctor hC).hom.app X).hom) x) i = ↑x ↑i
-- Mathlib.RingTheory.Ideal.Height
/-- If J has finite height and I ≤ J, then I has finite height  -/
Ideal.finiteHeight_of_le : ∀ {R : Type u_1} [inst : CommRing R] {I J : Ideal R}, I ≤ J → J ≠ ⊤ → ∀ [J.FiniteHeight], I.FiniteHeight
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α},
  Std.Internal.List.containsKey k l = false →
    toInsert.contains k = false → Std.Internal.List.getKey? k (Std.Internal.List.insertListIfNewUnit l toInsert) = none
-- Mathlib.AlgebraicGeometry.StructureSheaf
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.isUnit_toStalk : ∀ {R : Type u} [inst : CommRing R] (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (f : R),
  x ∈ PrimeSpectrum.basicOpen f →
    IsUnit ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.StructureSheaf.toStalk R x)) f)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey!_erase_le_maxKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {k : α}, (t.erase k).isEmpty = false → (cmp (t.erase k).maxKey! t.maxKey!).isLE = true
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_eq_some_getKey! : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {a : α}, a ∈ m → m.getKey? a = some (m.getKey! a)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenModifier.modification : Lean.Lsp.SemanticTokenModifier
-- Mathlib.Algebra.Module.Equiv.Basic
Units.mulRightLinearEquiv_trans_mulRightLinearEquiv : ∀ {R : Type u_9} {A : Type u_10} [inst : Semiring R] [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] (a b : Aˣ),
  Units.mulRightLinearEquiv R a ≪≫ₗ Units.mulRightLinearEquiv R b = Units.mulRightLinearEquiv R (a * b)
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.BuilderOption.casesPatterns.inj : ∀ {pats pats_1 : Array Aesop.CasesPattern},
  Aesop.Frontend.BuilderOption.casesPatterns pats = Aesop.Frontend.BuilderOption.casesPatterns pats_1 → pats = pats_1
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Expr.denoteN.match_1.congr_eq_4 : ∀ (motive : Lean.Grind.Linarith.Expr → Sort u_1) (x : Lean.Grind.Linarith.Expr)
  (h_1 : (a b : Lean.Grind.Linarith.Expr) → motive (a.sub b)) (h_2 : (a : Lean.Grind.Linarith.Expr) → motive a.neg)
  (h_3 : (k : ℤ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.intMul k a))
  (h_4 : Unit → motive Lean.Grind.Linarith.Expr.zero)
  (h_5 : (v : Lean.Grind.Linarith.Var) → motive (Lean.Grind.Linarith.Expr.var v))
  (h_6 : (a b : Lean.Grind.Linarith.Expr) → motive (a.add b))
  (h_7 : (k : ℕ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.natMul k a)),
  x = Lean.Grind.Linarith.Expr.zero →
    (match x with
      | a.sub b => h_1 a b
      | a.neg => h_2 a
      | Lean.Grind.Linarith.Expr.intMul k a => h_3 k a
      | Lean.Grind.Linarith.Expr.zero => h_4 ()
      | Lean.Grind.Linarith.Expr.var v => h_5 v
      | a.add b => h_6 a b
      | Lean.Grind.Linarith.Expr.natMul k a => h_7 k a) ≍
      h_4 ()
-- Mathlib.Algebra.GCDMonoid.Basic
StrongNormalizedGCDMonoid.toStrongNormalizationMonoid : {α : Type u_2} → {inst : CommMonoidWithZero α} → [self : StrongNormalizedGCDMonoid α] → StrongNormalizationMonoid α
-- Mathlib.Topology.Algebra.Constructions
/-- An auxiliary lemma that can be used to prove that coercion `AddUnits M → M` is a
topological embedding. Use `AddUnits.isEmbedding_val` or `toAddUnits_homeomorph` instead.  -/
AddUnits.isEmbedding_val_mk' : ∀ {M : Type u_4} [inst : AddMonoid M] [inst_1 : TopologicalSpace M] {f : M → M},
  ContinuousOn f {x | IsAddUnit x} → (∀ (u : AddUnits M), f ↑u = ↑(-u)) → Topology.IsEmbedding AddUnits.val
-- Init.Data.Nat.Basic
Nat.lt_or_lt_of_ne : ∀ {a b : ℕ}, a ≠ b → a < b ∨ b < a
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.FamilyOfElements.comp_of_compatible : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X Y : C}
  (S : CategoryTheory.Sieve X) {x : CategoryTheory.Presieve.FamilyOfElements P S.arrows},
  x.Compatible →
    ∀ {f : Y ⟶ X} (hf : S.arrows f) {Z : C} (g : Z ⟶ Y),
      x (CategoryTheory.CategoryStruct.comp g f) ⋯ = (CategoryTheory.ConcreteCategory.hom (P.map g.op)) (x f hf)
-- Mathlib.Topology.MetricSpace.Closeds
/-- **Alias** of `TopologicalSpace.Closeds.isometry_singleton`. -/
EMetric.Closeds.isometry_singleton : ∀ {α : Type u_1} [inst : EMetricSpace α], Isometry fun x => {x}
-- Mathlib.Algebra.Field.ULift
ULift.up_ratCast : ∀ {α : Type u} [inst : RatCast α] (q : ℚ), { down := ↑q } = ↑q
-- Mathlib.RingTheory.PowerSeries.Ideal
PowerSeries.eq_of_le_of_X_notMem_of_fg_of_isPrime : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal (PowerSeries R)} [I.IsPrime] {J : Ideal (PowerSeries R)},
  J ≤ I →
    PowerSeries.X ∉ I → J.FG → Ideal.map PowerSeries.constantCoeff I ≤ Ideal.map PowerSeries.constantCoeff J → I = J
-- Batteries.Data.UnionFind.Basic
/-- Find root of a union-find node, updating the structure using path compression.
Returns inputs unchanged when index is out of bounds.  -/
Batteries.UnionFind.findD : Batteries.UnionFind → ℕ → Batteries.UnionFind × ℕ
-- Mathlib.MeasureTheory.OuterMeasure.Caratheodory
MeasureTheory.OuterMeasure.isCaratheodory_iUnion : ∀ {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : ℕ → Set α},
  (∀ (i : ℕ), m.IsCaratheodory (s i)) → m.IsCaratheodory (⋃ i, s i)
-- Mathlib.Analysis.SpecialFunctions.Log.ERealExp
EReal.exp_bot : ⊥.exp = 0
-- Mathlib.Order.Hom.Bounded
TopHom.instDistribLattice : {α : Type u_2} →
  {β : Type u_3} → [inst : Top α] → [inst_1 : DistribLattice β] → [inst_2 : OrderTop β] → DistribLattice (TopHom α β)
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.head_congr : ∀ {α : Type u} {s t : Stream'.WSeq α}, s ~ʷ t → s.head.Equiv t.head
-- Aesop.Tree.Data
Aesop.NormalizationState.normalizedGoal? : Aesop.NormalizationState → Option Lean.MVarId
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap.0.Std.IterM.flattenAfter.eq_1 : ∀ {α α₂ β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m (Std.IterM m β)]
  [inst_2 : Std.Iterator α₂ m β] (it₁ : Std.IterM m (Std.IterM m β)) (it₂ : Option (Std.IterM m β)),
  Std.IterM.flattenAfter✝ it₁ it₂ = { internalState := { it₁ := it₁, it₂ := it₂ } }
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
/-- A distributive multiplicative action of a monoid on an additive monoid `β` gives a distributive
multiplicative action on `Finset β`.  -/
Finset.distribMulAction : {α : Type u_1} →
  {β : Type u_2} →
    [inst : DecidableEq β] →
      [inst_1 : Monoid α] → [inst_2 : AddMonoid β] → [DistribMulAction α β] → DistribMulAction α (Finset β)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.toList_map : ∀ {β : Type v} {γ : Type w} {α : Type u} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) {f : α → β → γ},
  (Std.DHashMap.Raw.Const.toList ↑(Std.DHashMap.Internal.Raw₀.map f m)).Perm
    (List.map (fun p => (p.1, f p.1 p.2)) (Std.DHashMap.Raw.Const.toList ↑m))
-- Mathlib.Data.ENat.Pow
ENat.instPow : Pow ℕ∞ ℕ∞
-- Mathlib.RingTheory.Localization.AtPrime.Basic
IsLocalization.AtPrime.map_eq_top_of_not_le : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {I p : Ideal R}
  [inst_3 : p.IsPrime] [IsLocalization.AtPrime S p], ¬I ≤ p → Ideal.map (algebraMap R S) I = ⊤
-- Mathlib.Data.Vector.Snoc
_private.Mathlib.Data.Vector.Snoc.0.List.Vector.cons.match_1.eq_1 : ∀ {α : Type u_1} {n : ℕ} (motive : α → List.Vector α n → Sort u_2) (a : α) (v : List α) (h : v.length = n)
  (h_1 : (a : α) → (v : List α) → (h : v.length = n) → motive a ⟨v, h⟩),
  (match a, ⟨v, h⟩ with
    | a, ⟨v, h⟩ => h_1 a v h) =
    h_1 a v h
-- Init.Data.List.Sublist
List.Sublist.eq_of_length : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → l₁.length = l₂.length → l₁ = l₂
-- Mathlib.LinearAlgebra.Projection
Submodule.projection_apply_of_mem_left : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (hpq : IsCompl p q) {x : E}, x ∈ p → (p.projection q hpq) x = x
-- Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
/-- The projection to the cokernel.  -/
CategoryTheory.Triangulated.AbelianSubcategory.πQ : {C : Type u_1} →
  {A : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} A] →
        {ι : CategoryTheory.Functor A C} →
          {X₂ : A} → {X₃ : C} → (ι.obj X₂ ⟶ X₃) → {Q : A} → (X₃ ⟶ ι.obj Q) → [ι.Full] → X₂ ⟶ Q
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
/-- Auxiliary predicate to express that a morphism is purely a composition of `δ i`s.  -/
SimplexCategoryGenRel.P_δ : CategoryTheory.MorphismProperty SimplexCategoryGenRel
-- Init.Data.List.Range
List.range'_inj : ∀ {s n s' n' : ℕ}, List.range' s n = List.range' s' n' ↔ n = n' ∧ (n = 0 ∨ s = s')
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.instHasProductSigmaFstSndOfPiObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} (f : ι → Type u_2) (g : (i : ι) → f i → C)
  [inst_1 : ∀ (i : ι), CategoryTheory.Limits.HasProduct (g i)] [CategoryTheory.Limits.HasProduct fun i => ∏ᶜ g i],
  CategoryTheory.Limits.HasProduct fun p => g p.fst p.snd
-- Mathlib.RingTheory.WittVector.Verschiebung
WittVector.verschiebung_coeff_add_one : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [hp : Fact (Nat.Prime p)] (x : WittVector p R) (n : ℕ),
  (WittVector.verschiebung x).coeff (n + 1) = x.coeff n
-- Init.Data.List.Sublist
List.IsInfix.subset : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+: l₂ → l₁ ⊆ l₂
-- Mathlib.CategoryTheory.MorphismProperty.LocalEpi
CategoryTheory.ObjectProperty.isLocal_le_localEpi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C},
  P.isLocal ≤ P.localEpi
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey?_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {v : β k},
      (t.insert k v).minKey? = some (t.minKey?.elim k fun k' => if (cmp k k').isLE = true then k else k')