mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Returns an array `kinds` s.ts `kinds[i]` is the kind of the corresponding argument.

- a type (that is not a proposition) or type former (which has forward dependencies) or
- a proof, or
- an instance implicit argument

When `kinds[i].isSupport` is `true`, we say the corresponding argument is a "support" argument.
 -/
Lean.Meta.Grind.NormalizePattern.getPatternArgKinds : Lean.Expr → ℕ → Lean.MetaM (Array Lean.Meta.Grind.NormalizePattern.PatternArgKind)
-- Mathlib.Order.Bounds.Basic
lowerBounds_singleton : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, lowerBounds {a} = Set.Iic a
-- Mathlib.Analysis.Meromorphic.Divisor
/-- Special case of `MeromorphicOn.divisor_subset_finiteSupport` that frequently shows in complex
analysis, where  `U` is a closed ball and `V` is its interior.
 -/
MeromorphicOn.divisor_ball_support_finite : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [ProperSpace 𝕜] {f : 𝕜 → E} {R : ℝ} {c : 𝕜},
  MeromorphicOn f (Metric.closedBall c R) → (MeromorphicOn.divisor f (Metric.ball c R)).support.Finite
-- Mathlib.RingTheory.Noetherian.Orzech
/-- If `M ⊕ N` embeds into `M`, for `M` Noetherian over `R`, then `N` is trivial.  -/
IsNoetherian.subsingleton_of_prod_injective : ∀ {R : Type u_1} {M : Type u_2} {N : Type w} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [IsNoetherian R M] (f : M × N →ₗ[R] M),
  Function.Injective ⇑f → Subsingleton N
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.le_sSup : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C]
  [inst_2 : CategoryTheory.WellPowered.{w, v₁, u₁} C] [inst_3 : CategoryTheory.Limits.HasCoproducts C]
  [inst_4 : CategoryTheory.Limits.HasImages C] {A : C} (s : Set (CategoryTheory.Subobject A)),
  ∀ f ∈ s, f ≤ CategoryTheory.Subobject.sSup s
-- Mathlib.Algebra.Ring.InjSurj
/-- Pullback a `NonAssocCommRing` instance along an injective function.  -/
Function.Injective.nonAssocCommRing : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Add S] →
      [inst_1 : Mul S] →
        [inst_2 : Zero S] →
          [inst_3 : One S] →
            [inst_4 : Neg S] →
              [inst_5 : Sub S] →
                [inst_6 : SMul ℕ S] →
                  [inst_7 : SMul ℤ S] →
                    [inst_8 : NatCast S] →
                      [inst_9 : IntCast S] →
                        [inst_10 : NonAssocCommRing R] →
                          (f : S → R) →
                            Function.Injective f →
                              f 0 = 0 →
                                f 1 = 1 →
                                  (∀ (x y : S), f (x + y) = f x + f y) →
                                    (∀ (x y : S), f (x * y) = f x * f y) →
                                      (∀ (x : S), f (-x) = -f x) →
                                        (∀ (x y : S), f (x - y) = f x - f y) →
                                          (∀ (n : ℕ) (x : S), f (n • x) = n • f x) →
                                            (∀ (n : ℤ) (x : S), f (n • x) = n • f x) →
                                              (∀ (n : ℕ), f ↑n = ↑n) → (∀ (n : ℤ), f ↑n = ↑n) → NonAssocCommRing S
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.nonneg_prod_iff : ∀ {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid P] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R P] [inst_7 : Preorder P] [AddLeftMono P] {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P},
  (∀ (x : M₁ × M₂), 0 ≤ (Q₁.prod Q₂) x) ↔ (∀ (x : M₁), 0 ≤ Q₁ x) ∧ ∀ (x : M₂), 0 ≤ Q₂ x
-- Mathlib.RingTheory.Ideal.Prime
/-- An ideal `P` of a ring `R` is prime if `P ≠ R` and `xy ∈ P → x ∈ P ∨ y ∈ P`  -/
Ideal.IsPrime : {α : Type u} → [inst : Semiring α] → Ideal α → Prop
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.QuasiFiniteAt.comap_algEquiv : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] (p : Ideal S) [inst_5 : p.IsPrime] [Algebra.QuasiFiniteAt R p]
  (f : T ≃ₐ[R] S), Algebra.QuasiFiniteAt R (Ideal.comap f.toRingEquiv.toRingHom p)
-- Mathlib.Algebra.Group.Subgroup.Finsupp
AddSubgroup.exists_of_mem_closure_range : ∀ {M : Type u_1} [inst : AddCommGroup M] {ι : Type u_2} (f : ι → M) (x : M) [inst_1 : Fintype ι],
  x ∈ AddSubgroup.closure (Set.range f) → ∃ a, x = ∑ i, a i • f i
-- Mathlib.Topology.UniformSpace.Defs
comp3_mem_uniformity : ∀ {α : Type ua} [inst : UniformSpace α] {s : SetRel α α},
  s ∈ uniformity α → ∃ t ∈ uniformity α, SetRel.comp t (SetRel.comp t t) ⊆ s
-- Mathlib.Algebra.Ring.Subring.Basic
/-- A subring `t` includes `closure s` if and only if it includes `s`.  -/
Subring.closure_le : ∀ {R : Type u} [inst : NonAssocRing R] {s : Set R} {t : Subring R}, Subring.closure s ≤ t ↔ s ⊆ ↑t
-- Mathlib.Algebra.MonoidAlgebra.Cardinal
/-- **Alias** of `MonoidAlgebra.cardinalMk_eq_max_lift_of_infinite'`. -/
MonoidAlgebra.cardinalMk_lift_of_infinite' : ∀ (R : Type u) (M' : Type v) [inst : Semiring R] [Nonempty M'] [Infinite R],
  Cardinal.mk (MonoidAlgebra R M') = max (Cardinal.lift.{v, u} (Cardinal.mk R)) (Cardinal.lift.{u, v} (Cardinal.mk M'))
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image2_mul : ∀ {α : Type u_2} [inst : Mul α] {s t : Set α}, Set.image2 (fun x1 x2 => x1 * x2) s t = s * t
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- Turn a morphism in `AddMagmaCat` back into an `AddHom`.  -/
AddMagmaCat.Hom.hom : {X Y : AddMagmaCat} → X.Hom Y → ↑X →ₙ+ ↑Y
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
DividedPowers.OfInvertibleFactorial.dpow_mul_of_add_lt : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} [inst_1 : DecidablePred fun x => x ∈ I] {n : ℕ},
  IsUnit ↑(n - 1).factorial →
    ∀ {m k : ℕ},
      m + k < n →
        ∀ {x : A},
          x ∈ I →
            DividedPowers.OfInvertibleFactorial.dpow I m x * DividedPowers.OfInvertibleFactorial.dpow I k x =
              ↑((m + k).choose m) * DividedPowers.OfInvertibleFactorial.dpow I (m + k) x
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
/-- The derivative of `expMap`, see `hasFDerivAt_expMap`.
 -/
NumberField.mixedEmbedding.fundamentalCone.fderiv_expMap : {K : Type u_1} →
  [inst : Field K] →
    NumberField.mixedEmbedding.realSpace K →
      NumberField.mixedEmbedding.realSpace K →L[ℝ] NumberField.mixedEmbedding.realSpace K
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
/-- The set of compact operators from a normed space to a complete topological vector space is
closed.  -/
isClosed_setOfPred_isCompactOperator : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NontriviallyNormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ₁₂ : 𝕜₁ →+* 𝕜₂}
  {M₁ : Type u_3} {M₂ : Type u_4} [inst_2 : SeminormedAddCommGroup M₁] [inst_3 : AddCommGroup M₂]
  [inst_4 : NormedSpace 𝕜₁ M₁] [inst_5 : Module 𝕜₂ M₂] [inst_6 : UniformSpace M₂] [inst_7 : IsUniformAddGroup M₂]
  [ContinuousConstSMul 𝕜₂ M₂] [T2Space M₂] [CompleteSpace M₂], IsClosed {f | IsCompactOperator ⇑f}
-- Lean.Meta.Tactic.Ext
/-- Gets the list of `@[ext]` theorems corresponding to the key `ty`,
ordered from high priority to low.  -/
Lean.Meta.Ext.getExtTheorems : Lean.Expr → Lean.MetaM (Array Lean.Meta.Ext.ExtTheorem)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst_2 : Inhabited γ] {f : α → β → γ} {k : α},
  (Std.ExtTreeMap.map f t)[k]! = (Option.map (f k) t[k]?).get!
-- Mathlib.Topology.UniformSpace.Equicontinuity
equicontinuousWithinAt_iInf_rng : ∀ {ι : Type u_1} {κ : Type u_2} {X : Type u_3} {α' : Type u_7} [tX : TopologicalSpace X] {u : κ → UniformSpace α'}
  {F : ι → X → α'} {S : Set X} {x₀ : X}, EquicontinuousWithinAt F S x₀ ↔ ∀ (k : κ), EquicontinuousWithinAt F S x₀
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.type_eq_zero_of_empty : ∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r] [IsEmpty α], Ordinal.type r = 0
-- Mathlib.Topology.Constructions
isClosedMap_toAdd : ∀ {X : Type u} [inst : TopologicalSpace X], IsClosedMap ⇑Multiplicative.toAdd
-- Mathlib.Analysis.Calculus.FDeriv.Mul
HasStrictFDerivAt.mul_const' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸] {a : E → 𝔸}
  {a' : E →L[𝕜] 𝔸}, HasStrictFDerivAt a a' x → ∀ (b : 𝔸), HasStrictFDerivAt (fun y => a y * b) (MulOpposite.op b • a') x
-- Mathlib.RingTheory.Extension.Cotangent.Basis
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.basis_inr : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_4}
  {P : Algebra.Generators R S ι} {σ : Type u_5} {b : Module.Basis σ S P.toExtension.Cotangent}
  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b) [inst_3 : Nontrivial S] (i : σ),
  (Algebra.Generators.PresentationOfFreeCotangent.Aux.basis✝ D) (Sum.inr i) =
    (Algebra.Generators.PresentationOfFreeCotangent.Aux.cotangentEquivProd✝ D).symm
      (0, (Algebra.Generators.PresentationOfFreeCotangent.Aux.basisLeft✝ D) i)
-- Mathlib.Algebra.Algebra.Unitization
Unitization.sndHom_apply : ∀ (S : Type u_2) (R : Type u_3) (A : Type u_4) [inst : Semiring S] [inst_1 : Semiring R] [inst_2 : AddCommMonoid A]
  [inst_3 : Module S R] [inst_4 : Module S A] (a : Unitization R A), (Unitization.sndHom S R A) a = a.toProd.2
-- Batteries.Data.Nat.Basic
/-- Left leg for `Nat.recDiag`  -/
Nat.recDiag.left : {motive : ℕ → ℕ → Sort u_1} → motive 0 0 → ((n : ℕ) → motive 0 n → motive 0 (n + 1)) → (n : ℕ) → motive 0 n
-- Mathlib.Algebra.Group.Subgroup.Finite
/-- For finite index types, the `Subgroup.pi` is generated by the embeddings of the
additive groups.  -/
AddSubgroup.pi_le_iff : ∀ {η : Type u_3} {f : η → Type u_4} [inst : (i : η) → AddGroup (f i)] [inst_1 : DecidableEq η] [Finite η]
  {H : (i : η) → AddSubgroup (f i)} {J : AddSubgroup ((i : η) → f i)},
  AddSubgroup.pi Set.univ H ≤ J ↔ ∀ (i : η), AddSubgroup.map (AddMonoidHom.single f i) (H i) ≤ J
-- Aesop.Search.Expansion
_private.Aesop.Search.Expansion.0.Aesop.expandGoal.fmtSafe : {Q : Type} → [inst : Aesop.Queue Q] → Except Lean.Exception Aesop.SafeRulesResult → Aesop.SearchM Q Lean.MessageData
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_smul : ∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : SMulZeroClass S R] [IsScalarTower S R R] (s : S)
  (p : Polynomial R), Polynomial.derivative (s • p) = s • Polynomial.derivative p
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- The variable definition used by the bitblaster.
 -/
Std.Tactic.BVDecide.BVBit : Type
-- Mathlib.Algebra.Group.Action.Opposite
VAddCommClass.opposite_mid : ∀ {M : Type u_5} {N : Type u_6} [inst : Add N] [inst_1 : VAdd M N] [VAddAssocClass M N N], VAddCommClass M Nᵃᵒᵖ N
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.instLattice.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G],
  FiniteIndexNormalAddSubgroup.instLattice =
    { toSemilatticeSup := FiniteIndexNormalAddSubgroup.instSemilatticeSupFiniteIndexNormalAddSubgroup,
      inf := SemilatticeInf.inf, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }
-- Std.Http.Data.Headers
Std.Http.Headers.instInsertProdNameValue : Insert (Std.Http.Header.Name × Std.Http.Header.Value) Std.Http.Headers
-- Init.Data.UInt.Lemmas
UInt64.toUInt8_mul : ∀ (a b : UInt64), (a * b).toUInt8 = a.toUInt8 * b.toUInt8
-- Lean.Meta.RecursorInfo
Lean.Meta.RecursorUnivLevelPos.motive.sizeOf_spec : sizeOf Lean.Meta.RecursorUnivLevelPos.motive = 1
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.eq_prod_roots_of_monic : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} [inst_1 : IsDomain R],
  f.Splits → f.Monic → f = (Multiset.map (fun x => Polynomial.X - Polynomial.C x) f.roots).prod
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.isEmpty_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α],
  m.isEmpty = true ↔ m = ∅
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_filter_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {f : α → β → Bool}
  {k k' : α} {fallback : β},
  t.getKey? k = some k' →
    (Std.TreeMap.filter f t).getD k fallback = (Option.filter (fun x => f k' x) t[k]?).getD fallback
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getValue?_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [EquivBEq α] {f : α → β → Option γ} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α},
      Std.Internal.List.getValue? k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l) =
        (Std.Internal.List.getValue? k l).pbind fun v h => f (Std.Internal.List.getKey k l ⋯) v
-- Mathlib.Algebra.Group.Even
IsSquare.mul_self : ∀ {α : Type u_2} [inst : Mul α] (r : α), IsSquare (r * r)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- The quotient `G ⧸ N` of a complete first countable uniform additive group
`G` by a normal additive subgroup is itself complete. Consequently, quotients of Banach spaces by
subspaces are complete. In contrast to `QuotientAddGroup.completeSpace_left'`, in this version
`G` is already equipped with a uniform structure.
[N. Bourbaki, *General Topology*, IX.3.1 Proposition 4][bourbaki1966b]

Even though `G` is equipped with a uniform structure, the quotient `G ⧸ N` does not inherit a
uniform structure, so it is still provided manually via `IsTopologicalAddGroup.leftUniformSpace`.
In the most common use case ─ quotients of normed additive commutative groups by subgroups ─
significant care was taken so that the uniform structure inherent in that setting coincides
(definitionally) with the uniform structure provided here.  -/
QuotientAddGroup.completeSpace_left : ∀ (G : Type u_1) [inst : AddGroup G] [us : UniformSpace G] [inst_1 : IsLeftUniformAddGroup G] [FirstCountableTopology G]
  (N : AddSubgroup G) [inst_3 : N.Normal] [hG : CompleteSpace G], CompleteSpace (G ⧸ N)
-- Mathlib.AlgebraicGeometry.StructureSheaf
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.toBasicOpenₗ_mk : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (s : R) (f : M)
  (g : ↥(Submonoid.powers s)),
  (AlgebraicGeometry.StructureSheaf.toBasicOpenₗ✝ R M s) (LocalizedModule.mk f g) =
    AlgebraicGeometry.StructureSheaf.const f (↑g) (PrimeSpectrum.basicOpen s) ⋯
-- Mathlib.NumberTheory.LSeries.Nonvanishing
/-- If `χ` is a Dirichlet character, then `L(χ, s)` does not vanish when `s.re = 1`
except when `χ` is trivial and `s = 1` (then `L(χ, s)` has a simple pole at `s = 1`).  -/
DirichletCharacter.LFunction_ne_zero_of_re_eq_one : ∀ {N : ℕ} (χ : DirichletCharacter ℂ N) [inst : NeZero N] {s : ℂ},
  s.re = 1 → χ ≠ 1 ∨ s ≠ 1 → DirichletCharacter.LFunction χ s ≠ 0
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.oreSub_add_oreSub_comm : ∀ {R : Type u_1} [inst : AddCommMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {r₁ r₂ : R}
  {s₁ s₂ : ↥S}, r₁ -ₒ s₁ + (r₂ -ₒ s₂) = r₁ + r₂ -ₒ (s₁ + s₂)
-- Init.Data.Array.Lemmas
Array.getElem!_set!_ne : ∀ {α : Type u_1} [inst : Inhabited α] (xs : Array α) (i j : ℕ) (x : α), i ≠ j → (xs.set! i x)[j]! = xs[j]!
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Basic
Std.Tactic.BVDecide.BVExpr.Assignment.toAIGAssignment_apply : ∀ (assign : Std.Tactic.BVDecide.BVExpr.Assignment) (bit : Std.Tactic.BVDecide.BVBit),
  assign.toAIGAssignment bit = (assign.get bit.var).bv.getLsbD ↑bit.idx
-- Mathlib.Algebra.Homology.Embedding.StupidTrunc
HomologicalComplex.isZero_stupidTrunc_X : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c')
  [inst_3 : e.IsRelIff] (i' : ι'), (∀ (i : ι), e.f i ≠ i') → CategoryTheory.Limits.IsZero ((K.stupidTrunc e).X i')
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_add_size_eq_size_union_add_size_inter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α], m₁.size + m₂.size = (m₁ ∪ m₂).size + (m₁ ∩ m₂).size
-- Mathlib.GroupTheory.Exponent
commMonoidOfExponentTwo.eq_1 : ∀ {G : Type u} [inst : Monoid G] [inst_1 : IsCancelMul G] (hG : Monoid.exponent G = 2),
  commMonoidOfExponentTwo hG = { toMonoid := inst, mul_comm := ⋯ }
-- Mathlib.Computability.Reduce
stdRefl_oneOneReducible : ∀ {α : Type u_1} [inst : Primcodable α], Std.Refl OneOneReducible
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- Construct a bundled `Semigrp` from the underlying type and typeclass.  -/
Semigrp.of : (M : Type u) → [Semigroup M] → Semigrp
-- Init.Data.Option.Lemmas
Option.min_eq_none_iff : ∀ {α : Type u_1} [inst : Min α] {o o' : Option α}, o ⊓ o' = none ↔ o = none ∨ o' = none
-- Init.Data.UInt.Bitwise
USize.neg_one_shiftLeft_or_shiftLeft : ∀ {a b : USize}, (-1) <<< b ||| a <<< b = (-1) <<< b
-- Mathlib.Combinatorics.Matroid.Basic
/-- **Alias** of `Matroid.IsBase.sdiff_infinite_comm`. -/
Matroid.IsBase.diff_infinite_comm : ∀ {α : Type u_1} {M : Matroid α} {B₁ B₂ : Set α}, M.IsBase B₁ → M.IsBase B₂ → ((B₁ \ B₂).Infinite ↔ (B₂ \ B₁).Infinite)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
NumberField.instIsTotallyRealSubtypeMemSubfieldTop : ∀ (K : Type u_2) [inst : Field K] [NumberField.IsTotallyReal K], NumberField.IsTotallyReal ↥⊤
-- Lean.Server.FileWorker.SemanticHighlighting
Lean.Server.FileWorker.instHashableAbsoluteLspSemanticToken : Hashable Lean.Server.FileWorker.AbsoluteLspSemanticToken
-- Mathlib.LinearAlgebra.Finsupp.Pi
LinearMap.fst_prodOfFinsuppNat : ∀ {R : Type u_1} {M : Type u_2} {P : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid P] [inst_4 : Module R P] (f : P × M →ₗ[R] M) (x : ℕ →₀ P), (f.prodOfFinsuppNat x).1 = x 0
-- Aesop.Tree.TreeM
Aesop.TreeM.State.mk.injEq : ∀ (tree tree_1 : Aesop.Tree), ({ tree := tree } = { tree := tree_1 }) = (tree = tree_1)
-- Mathlib.Algebra.Group.Action.Units
AddUnits.vadd_mk_apply : ∀ {M : Type u_6} {α : Type u_7} [inst : AddMonoid M] [inst_1 : VAdd M α] (m n : M) (h₁ : m + n = 0) (h₂ : n + m = 0)
  (a : α), { val := m, neg := n, val_neg := h₁, neg_val := h₂ } +ᵥ a = m +ᵥ a
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited α]
  {l : List (α × β)} {k : α}, (List.map Prod.fst l).contains k = false → (Std.HashMap.Raw.ofList l).getKey! k = default
-- Lean.Meta.AppBuilder
/-- Returns `(n : type)`, a numeric literal of type `type`. The method fails if we don't have an instance `OfNat type n`  -/
Lean.Meta.mkNumeral : Lean.Expr → ℕ → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.GroupWithZero.Units.Basic
div_eq_div_iff : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] {a b c d : G₀}, b ≠ 0 → d ≠ 0 → (a / b = c / d ↔ a * d = c * b)
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.MatchM : Type → Type → Type
-- Mathlib.CategoryTheory.Sites.Point.Presheaf
/-- The family of points on the site `(C, ⊥)` (whose
sheaves are presheaves, see `sheafBotEquivalence`) given by the objects of `X`.  -/
CategoryTheory.GrothendieckTopology.pointsBot : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.LocallySmall.{w, v, u} C] → CategoryTheory.ObjectProperty ⊥.Point
-- Mathlib.CategoryTheory.FiberedCategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.instFaithfulαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor : ∀ {𝒮 : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 𝒮]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) (S : 𝒮),
  (CategoryTheory.Functor.Fiber.inducedFunctor ⋯).Faithful
-- Std.Data.DHashMap.Raw
/-- Computes the union of the given hash 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, so the expected runtime is
`O(min(m₁.size, m₂.size))`.
 -/
Std.DHashMap.Raw.union : {α : Type u} →
  {β : α → Type v} → [BEq α] → [Hashable α] → Std.DHashMap.Raw α β → Std.DHashMap.Raw α β → Std.DHashMap.Raw α β
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- `p : S.X₂ ⟶ Q` is a cokernel of `S.f : S.X₁ ⟶ S.X₂`  -/
CategoryTheory.ShortComplex.RightHomologyData.hp : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} →
        (self : S.RightHomologyData) →
          CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ self.p ⋯)
-- Mathlib.CategoryTheory.PathCategory.Basic
CategoryTheory.quotientPathsTo_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C]
  (a : CategoryTheory.Quotient (CategoryTheory.pathsHomRel C)), (CategoryTheory.quotientPathsTo C).obj a = a.as
-- Mathlib.Data.Finset.Image
Finset.map_empty : ∀ {α : Type u_1} {β : Type u_2} (f : α ↪ β), Finset.map f ∅ = ∅
-- Mathlib.RepresentationTheory.Basic
/-- If we equip `k[G]` with the `k`-linear `G`-representation induced by the left regular action of
`G` on itself, the resulting object is isomorphic as a `k[G]`-module to `k[G]` with its natural
`k[G]`-module structure.  -/
Representation.ofMulActionSelfAsModuleEquiv : {k : Type u_1} →
  {G : Type u_2} →
    [inst : CommSemiring k] →
      [inst_1 : Group G] → (Representation.ofMulAction k G G).asModule ≃ₗ[MonoidAlgebra k G] MonoidAlgebra k G
-- Mathlib.Algebra.Group.Defs
nsmulBinRec_zero : ∀ {M : Type u_2} [inst : Add M] [inst_1 : Zero M] (m : M), nsmulBinRec 0 m = 0
-- Mathlib.Order.CompleteLattice.Basic
OrderIso.map_sSup_eq_sSup_symm_preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : α ≃o β) (s : Set α),
  f (sSup s) = sSup (⇑f.symm ⁻¹' s)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.tr_init : ∀ (c : Turing.ToPartrec.Code) (v : List ℕ),
  ∃ b,
    Turing.PartrecToTM2.TrCfg (Turing.ToPartrec.stepNormal c Turing.ToPartrec.Cont.halt v) b ∧
      StateTransition.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr) (Turing.PartrecToTM2.init c v) b
-- Mathlib.Data.Seq.Basic
/-- Coinductive principle for `All`.  -/
Stream'.Seq.all_coind : ∀ {α : Type u} {s : Stream'.Seq α} {p : α → Prop} (motive : Stream'.Seq α → Prop),
  motive s → (∀ (hd : α) (tl : Stream'.Seq α), motive (Stream'.Seq.cons hd tl) → p hd ∧ motive tl) → ∀ x ∈ s, p x
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
CategoryTheory.SpectralSequence.Hom.mk.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Abelian C] {κ : Type u_2}
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} {E E' : CategoryTheory.SpectralSequence C c r₀}
  (hom hom_1 :
    (r : ℤ) → (hr : autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence.Hom._auto_1) → E.page r ⋯ ⟶ E'.page r ⋯)
  (e_hom : hom = hom_1)
  (comm :
    ∀ (r r' : ℤ) (pq : κ) (hrr' : autoParam (r + 1 = r') CategoryTheory.SpectralSequence.Hom._auto_5)
      (hr : autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence.Hom._auto_7),
      CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (hom r ⋯) pq) (E'.iso r r' pq ⋯ ⋯).hom =
        CategoryTheory.CategoryStruct.comp (E.iso r r' pq ⋯ ⋯).hom ((hom r' ⋯).f pq)),
  { hom := hom, comm := comm } = { hom := hom_1, comm := ⋯ }
-- Lean.Meta.DiscrTree.Main
/-- Append `n` wildcards to `todo`
 -/
_private.Lean.Meta.DiscrTree.Main.0.Lean.Meta.DiscrTree.pushWildcards : ℕ → Array Lean.Expr → Array Lean.Expr
-- Lean.Data.LOption
Lean.instToStringLOption : {α : Type u_1} → [ToString α] → ToString (Lean.LOption α)