mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Omega.Constraint
_private.Init.Omega.Constraint.0.Lean.Omega.tidy?.match_1.eq_2 : ∀ (motive : Option (Lean.Omega.Constraint × Lean.Omega.Coeffs) → Sort u_1) (s' : Lean.Omega.Constraint)
  (x' : Lean.Omega.Coeffs) (h_1 : Unit → motive none)
  (h_2 : (s' : Lean.Omega.Constraint) → (x' : Lean.Omega.Coeffs) → motive (some (s', x'))),
  (match some (s', x') with
    | none => h_1 ()
    | some (s', x') => h_2 s' x') =
    h_2 s' x'
-- Mathlib.Data.List.Cycle
List.prev.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] (x : α) (x_1 : x ∈ []), [].prev x x_1 = ⋯.elim
-- Mathlib.Algebra.Category.AlgCat.TensorAlgebra
/-- The functor sending an `R`-module `M` to its tensor algebra over `R`.  -/
AlgCat.tensorAlgebra : (R : Type u) → [inst : CommRing R] → CategoryTheory.Functor (ModuleCat R) (AlgCat R)
-- Init.PropLemmas
ne_of_apply_ne : ∀ {α : Sort u_1} {β : Sort u_2} (f : α → β) {x y : α}, f x ≠ f y → x ≠ y
-- Mathlib.Data.Multiset.Fold
Multiset.fold_cons'_right : ∀ {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] (b a : α) (s : Multiset α),
  Multiset.fold op b (a ::ₘ s) = Multiset.fold op (op b a) s
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.instCompactSpace : ∀ {M : Type u_1} [inst : TopologicalSpace M] [CompactSpace M], CompactSpace Mᵈᵃᵃ
-- Init.Data.Int.Order
Int.lt_of_sub_pos : ∀ {a b : ℤ}, 0 < a - b → b < a
-- Mathlib.Data.ZMod.Basic
ZMod.val_ofNat : ∀ (n a : ℕ) [inst : a.AtLeastTwo], (OfNat.ofNat a).val = OfNat.ofNat a % n
-- Mathlib.Order.RelClasses
Order.Preimage.instRefl : ∀ {α : Type u} {β : Type v} {r : α → α → Prop} [Std.Refl r] {f : β → α}, Std.Refl (f ⁻¹'o r)
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
IsClosed.measurableSet_image_of_continuousOn_injOn : ∀ {γ : Type u_3} [inst : TopologicalSpace γ] [PolishSpace γ] {β : Type u_4} [inst_2 : TopologicalSpace β] [T2Space β]
  [inst_4 : MeasurableSpace β] [OpensMeasurableSpace β] {s : Set γ},
  IsClosed s → ∀ {f : γ → β}, ContinuousOn f s → Set.InjOn f s → MeasurableSet (f '' s)
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.instInv.eq_1 : ∀ {α : Type u} [inst : Inv α], WithOne.instInv = { inv := fun a => Option.map Inv.inv a }
-- Mathlib.MeasureTheory.Integral.Average
/-- **First moment method**. The maximum of a measurable function is greater than its integral,
while avoiding a null set.  -/
MeasureTheory.exists_notMem_null_lintegral_le : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {N : Set α} {f : α → ENNReal}
  [MeasureTheory.IsProbabilityMeasure μ], ∫⁻ (a : α), f a ∂μ ≠ ⊤ → μ N = 0 → ∃ x ∉ N, ∫⁻ (a : α), f a ∂μ ≤ f x
-- Mathlib.Topology.Category.Stonean.EffectiveEpi
Stonean.instEffectivelyEnoughCompHausToCompHaus : Stonean.toCompHaus.EffectivelyEnough
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.norm_lTensor_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} (G : Type u_4) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (g : E →L[𝕜] F),
  ‖ContinuousLinearMap.lTensor G g‖ ≤ ‖g‖
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  (t₁ ∪ t₂).getKey? k = (t₂.getKey? k).or (t₁.getKey? k)
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
_private.Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter.0.cyclotomicCharacter.termχ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Yoneda
/-- Unification hint for `(uliftCoyoneda.{w}.obj X).obj Y = ULift (unop Y ⟶ X)`.  -/
CategoryTheory.uliftCoyoneda_obj_obj_eq_hom' : {C : Type u₁} → [CategoryTheory.Category.{v₁, u₁} C] → Cᵒᵖ → Cᵒᵖ → C → C → Prop
-- Mathlib.CategoryTheory.Abelian.FreydMitchell
CategoryTheory.Abelian.FreydMitchell.instRingEmbeddingRing : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] → Ring (CategoryTheory.Abelian.FreydMitchell.EmbeddingRing C)
-- Mathlib.Data.Nat.Size
Nat.lt_size_self : ∀ (n : ℕ), n < 2 ^ n.size
-- Mathlib.Order.Defs.Unbundled
RelLowerSet.mk.sizeOf_spec : ∀ {α : Type u_1} [inst : LE α] {P : α → Prop} [inst_1 : SizeOf α] [inst_2 : (a : α) → SizeOf (P a)] (carrier : Set α)
  (isRelLowerSet' : IsRelLowerSet carrier P), sizeOf { carrier := carrier, isRelLowerSet' := isRelLowerSet' } = 1
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.monomial_mul_C : ∀ {R : Type u_1} {n : ℕ} [inst : Semiring R] {a b : R} [inst_1 : MulSemiringAction (Multiplicative ℕ) R],
  (SkewPolynomial.monomial n) a * SkewPolynomial.C b = (SkewPolynomial.monomial n) (a * (⇑SkewPolynomial.φ)^[n] b)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.le_of_iSup_eq_top : ∀ {X : AlgebraicGeometry.Scheme} {I J : X.IdealSheafData} {ι : Type u_1} (U : ι → ↑X.affineOpens),
  ⨆ i, ↑(U i) = ⊤ → (∀ (i : ι), I.ideal (U i) ≤ J.ideal (U i)) → I ≤ J
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.RightLinear.δᵣ_comp_μᵣ_assoc : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'} [self : F.RightLinear C] (d : D) (c : C) {Z : D'}
  (h : F.obj (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxRightLinear.δᵣ F d c)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxRightLinear.μᵣ F d c) h) =
    h
-- Init.Data.Range.Polymorphic.PRange
Std.Rco.mk : {α : Type u} → α → α → Std.Rco α
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rio_eq_nil : ∀ {n : ℕ}, n = 0 → (*...n).toList = []
-- Lean.Meta.Tactic.Grind.ProveEq
/-- Helper function for `proveEq?`. It abstracts nested ground terms in `lhs` and `rhs`.
Suppose `lhs` is `(b : Bool) → a[i]? = some b → Nat`, and
`rhs` is `(b : Bool) → some v = some b → Nat`.
Then, the result is
- `(fun x => (b : Bool) → x = some b → Nat) a[i]?`
- `(fun x => (b : Bool) → x = some b → Nat) (some v)`
 -/
_private.Lean.Meta.Tactic.Grind.ProveEq.0.Lean.Meta.Grind.abstractGroundMismatches? : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM (Option (Lean.Expr × Lean.Expr))
-- Mathlib.Data.Sym.Sym2
/-- **Alias** of `Sym2.toRel_symm`. -/
Sym2.toRel_symmetric : ∀ {α : Type u_1} (s : Set (Sym2 α)), Std.Symm (Sym2.ToRel s)
-- Std.Sync.StreamMap
/-- Cleanup function
 -/
Std.StreamMap.close : {α β : Type} → Std.StreamMap α β → IO Unit
-- Mathlib.Lean.Elab.Tactic.Basic
/-- Return expected type for the main goal, cleaning up annotations, using `Lean.MVarId.getType''`.
Remark: note that `MVarId.getType'` uses `whnf` instead of `cleanupAnnotations`, and
`MVarId.getType''` also uses `cleanupAnnotations`  -/
Lean.Elab.Tactic.getMainTarget'' : Lean.Elab.Tactic.TacticM Lean.Expr
-- Mathlib.CategoryTheory.Limits.Final
/-- When `F : C ⥤ D` is final, we denote by `lift F d` an arbitrary choice of object in `C` such that
there exists a morphism `d ⟶ F.obj (lift F d)`.
 -/
CategoryTheory.Functor.Final.lift : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (F : CategoryTheory.Functor C D) → [F.Final] → D → C
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
CategoryTheory.MorphismProperty.RightFraction₂.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {X Y X' : C} → (s : X' ⟶ X) → W s → (X' ⟶ Y) → (X' ⟶ Y) → W.RightFraction₂ X Y
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.SignedMeasure.toMeasureOfZeroLE.congr_simp : ∀ {α : Type u_1} {m : MeasurableSpace α} (s s_1 : MeasureTheory.SignedMeasure α) (e_s : s = s_1) (i i_1 : Set α)
  (e_i : i = i_1) (hi₁ : MeasurableSet i)
  (hi₂ : MeasureTheory.VectorMeasure.restrict 0 i ≤ MeasureTheory.VectorMeasure.restrict s i),
  s.toMeasureOfZeroLE i hi₁ hi₂ = s_1.toMeasureOfZeroLE i_1 ⋯ ⋯
-- Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
TopCat.Sheaf.eq_of_locally_eq_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : C → C → Type u_2} {CC : C → Type u_3}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.HasLimitsOfSize.{x, x, v_1, u_1} C] [(CategoryTheory.forget C).ReflectsIsomorphisms]
  [CategoryTheory.Limits.PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)] {X : TopCat}
  {F : TopCat.Sheaf C X} {ι : Type u_4} {U : ι → TopologicalSpace.Opens ↑X}
  {s t : CategoryTheory.ToType (F.obj.obj (Opposite.op (iSup U)))},
  s = t ↔
    ∀ (i : ι),
      (CategoryTheory.ConcreteCategory.hom (F.obj.map (TopologicalSpace.Opens.leSupr U i).op)) s =
        (CategoryTheory.ConcreteCategory.hom (F.obj.map (TopologicalSpace.Opens.leSupr U i).op)) t
-- Mathlib.Data.Set.Lattice
Set.iUnion₂_subset_iUnion : ∀ {α : Type u_1} {ι : Sort u_5} (κ : ι → Sort u_12) (s : ι → Set α), ⋃ i, ⋃ x, s i ⊆ ⋃ i, s i
-- Init.WFExtrinsicFix
WellFounded.extrinsicFix₂_eq_fix : ∀ {α : Sort u_2} {β : α → Sort u_3} {C₂ : (a : α) → β a → Sort u_1} [inst : ∀ (a : α) (b : β a), Nonempty (C₂ a b)]
  {R : (a : α) ×' β a → (a : α) ×' β a → Prop}
  {F : (a : α) → (b : β a) → ((a' : α) → (b' : β a') → R ⟨a', b'⟩ ⟨a, b⟩ → C₂ a' b') → C₂ a b} (wf : WellFounded R)
  {a : α} {b : β a},
  WellFounded.extrinsicFix₂ R F a b = wf.fix (fun x G => F x.fst x.snd fun a b h => G ⟨a, b⟩ h) ⟨a, b⟩
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.mk : {α : Type u_8} →
  {β : Type u_9} →
    [inst : CompleteLattice α] →
      [inst_1 : CompleteLattice β] →
        (tosInfHom : sInfHom α β) →
          (∀ (s : Set α), tosInfHom.toFun (sSup s) = sSup (tosInfHom.toFun '' s)) → CompleteLatticeHom α β
-- Mathlib.LinearAlgebra.PiTensorProduct.Finsupp
PiTensorProduct.ofFinsuppEquiv'_tprod_single : ∀ {R : Type u_1} {ι : Type u_2} {κ : ι → Type u_3} [inst : CommSemiring R] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι]
  [inst_3 : (i : ι) → DecidableEq (κ i)] [inst_4 : DecidableEq R] (p : (i : ι) → κ i) (r : ι → R),
  PiTensorProduct.ofFinsuppEquiv' ((PiTensorProduct.tprod R) fun i => fun₀ | p i => r i) = fun₀ | p => ∏ i, r i
-- Mathlib.Algebra.Order.BigOperators.Ring.Finset
/-- **Sedrakyan's lemma**, aka **Titu's lemma** or **Engel's form**.

This is a specialization of the Cauchy-Schwarz inequality with the sequences `f n / √(g n)` and
`√(g n)`, though here it is proven without relying on square roots.  -/
Finset.sq_sum_div_le_sum_sq_div : ∀ {ι : Type u_1} {R : Type u_2} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R]
  (s : Finset ι) (f : ι → R) {g : ι → R},
  (∀ i ∈ s, 0 < g i) → (∑ i ∈ s, f i) ^ 2 / ∑ i ∈ s, g i ≤ ∑ i ∈ s, f i ^ 2 / g i
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.singleFunctorsPostcompQIso.eq_1 : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C],
  DerivedCategory.singleFunctorsPostcompQIso C =
    (CategoryTheory.SingleFunctors.postcompFunctor C ℤ DerivedCategory.Qh).mapIso
        (HomotopyCategory.singleFunctorsPostcompQuotientIso C) ≪≫
      (CochainComplex.singleFunctors C).postcompPostcompIso (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          DerivedCategory.Qh ≪≫
        (CochainComplex.singleFunctors C).postcompIsoOfIso (DerivedCategory.quotientCompQhIso C)
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
/-- `lipschitzGroup` is the subgroup closure of all the invertible elements in the form of `ι Q m`
where `ι` is the canonical linear map `M →ₗ[R] CliffordAlgebra Q`.  -/
lipschitzGroup : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (Q : QuadraticForm R M) → Subgroup (CliffordAlgebra Q)ˣ
-- Mathlib.Algebra.Group.Equiv.TypeTags
AddEquiv.additiveMultiplicative_symm_apply : ∀ (G : Type u_2) [inst : AddZeroClass G] (a : G),
  (AddEquiv.additiveMultiplicative G).symm a = Additive.ofMul (Multiplicative.ofAdd a)
-- Mathlib.Geometry.Manifold.VectorField.Pullback
VectorField.mpullback_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {V : (x : M) → TangentSpace I x},
  VectorField.mpullback I I id V = V
-- Mathlib.Data.Finset.Fold
Finset.fold_insert_idem : ∀ {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β} {b : β}
  {s : Finset α} {a : α} [inst : DecidableEq α] [hi : Std.IdempotentOp op],
  Finset.fold op b f (insert a s) = op (f a) (Finset.fold op b f s)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Param.borrow : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Param pu → Bool
-- Mathlib.Order.Filter.Pointwise
Filter.comap_mul_comap_le : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : MulOneClass α] [inst_1 : MulOneClass β] [inst_2 : FunLike F α β]
  [MulHomClass F α β] (m : F) {f g : Filter β}, Filter.comap (⇑m) f * Filter.comap (⇑m) g ≤ Filter.comap (⇑m) (f * g)
-- Mathlib.Analysis.Convex.PathConnected
Path.segment_same : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [inst_3 : ContinuousAdd E]
  [inst_4 : ContinuousSMul ℝ E] (a : E), Path.segment a a = Path.refl a
-- Mathlib.Topology.IsClosedRestrict
Topology.reorderRestrictProd_of_mem : ∀ {ι : Type u_1} {α : ι → Type u_2} {s : Set ((i : ι) → α i)} {S : Set ι}
  (p : ↑(Sᶜ.domRestrict '' s) × ((i : ↑S) → α ↑i)) (j : ↑S), Topology.reorderRestrictProd S s p ↑j = p.2 j
-- Lean.Elab.Tactic.Simp
/-- Recall that when we declare a `simp` attribute using `register_simp_attr`, we automatically
create a `simproc` attribute. However, if the user creates `simp` and `simproc` attributes
programmatically, then one of them may be missing. Moreover, when we write `simp [seval]`,
we want to retrieve both the simp and simproc sets. We want to hide from users that
`simp` and `simproc` sets are stored in different data-structures.
 -/
Lean.Elab.Tactic.ResolveSimpIdResult.ext : (ext₁? : Option Lean.Meta.SimpExtension) →
  (ext₂? : Option Lean.Meta.Simp.SimprocExtension) →
    (ext₁?.isSome || ext₂?.isSome) = true → Lean.Elab.Tactic.ResolveSimpIdResult
-- Mathlib.Data.TypeVec
TypeVec.repeatEq.eq_1 : ∀ (x_2 : TypeVec.{u_1} 0), x_2.repeatEq = TypeVec.nilFun
-- Std.Time.Format.Basic
Std.Time.instCoeModifierFormatPart : Coe Std.Time.Modifier Std.Time.FormatPart
-- Mathlib.Topology.Algebra.InfiniteSum.Module
/-- Given a group `α` acting on a type `β`, and a function `f : β → M`, we "automorphize" `f` to a
function `β ⧸ α → M` by summing over `α` orbits, `b ↦ ∑' (a : α), f(a • b)`.  -/
MulAction.automorphize : {α : Type u_1} →
  {β : Type u_2} →
    {M : Type u_11} →
      [TopologicalSpace M] →
        [AddCommMonoid M] →
          [inst : Group α] → [inst_1 : MulAction α β] → (β → M) → Quotient (MulAction.orbitRel α β) → M
-- Lean.Util.Diff
/-- Determines a prefix to show on a given line when printing diff results.

For `delete`, the prefix is `"-"`, for `insert`, it is `"+"`, and for `skip` it is `" "`.
 -/
Lean.Diff.Action.linePrefix : Lean.Diff.Action → String
-- Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky
/-- If `0 ∉ S`, then there is a maximal element in `kaplanskySet S`.  -/
_private.Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky.0.UniqueFactorizationMonoid.exists_mem_kaplanskySet_eq_of_le : ∀ {R : Type u_1} [inst : Semiring R] {S : Subsemigroup R},
  0 ∉ S →
    ∃ P ∈ UniqueFactorizationMonoid.kaplanskySet✝ S, ∀ I ∈ UniqueFactorizationMonoid.kaplanskySet✝ S, P ≤ I → I = P
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
/-- The centroid of the face opposite a vertex lies in the affine span of that face.  -/
Affine.Simplex.faceOppositeCentroid_mem_affineSpan_face : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [inst_4 : NeZero n] [CharZero k] (s : Affine.Simplex k P n) (i : Fin (n + 1)),
  s.faceOppositeCentroid i ∈ affineSpan k (Set.range (s.faceOpposite i).points)
-- Mathlib.Data.Matrix.Composition
Matrix.instIsStablyFiniteRing : ∀ (I : Type u_1) [inst : Fintype I] (R : Type u_7) [inst_1 : MulOne R] [inst_2 : AddCommMonoid R]
  [inst_3 : DecidableEq I] [IsStablyFiniteRing R], IsStablyFiniteRing (Matrix I I R)
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.instUniqueSubtypeMemLieIdealBot : {R : Type u} → {L : Type v} → [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → Unique ↥⊥
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEmbedding.measurable_comp_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} [inst : MeasurableSpace β]
  [inst_1 : MeasurableSpace γ] {f : α → β} {g : β → γ}, MeasurableEmbedding g → (Measurable (g ∘ f) ↔ Measurable f)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.Limits.IsKernel.isoKernel.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) {Z : C} (l : Z ⟶ X) {s : CategoryTheory.Limits.KernelFork f} (hs : CategoryTheory.Limits.IsLimit s)
  (i : Z ≅ s.pt) (h : CategoryTheory.CategoryStruct.comp i.hom (CategoryTheory.Limits.Fork.ι s) = l),
  CategoryTheory.Limits.IsKernel.isoKernel f l hs i h = hs.ofIsoLimit (CategoryTheory.Limits.Cone.ext i.symm ⋯)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.insertManyIfNewUnit_cons : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α fun x => Unit} {l : List α} {k : α},
  Std.DHashMap.Const.insertManyIfNewUnit m (k :: l) = Std.DHashMap.Const.insertManyIfNewUnit (m.insertIfNew k ()) l
-- Mathlib.Data.Fin.Tuple.Finset
Fin.mem_piFinset_iff_zero_tail : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} {f : (i : Fin (n + 1)) → α i} {s : (i : Fin (n + 1)) → Finset (α i)},
  f ∈ Fintype.piFinset s ↔ f 0 ∈ s 0 ∧ Fin.tail f ∈ Fintype.piFinset (Fin.tail s)
-- Mathlib.Topology.Maps.Basic
isClosedMap_iff_kernImage_interior : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsClosedMap f ↔ ∀ {s : Set X}, Set.kernImage f (interior s) ⊆ interior (Set.kernImage f s)
-- Mathlib.Tactic.ClickSuggestions.GRewrite
/-- Some information about the rewrite position.  -/
Mathlib.Tactic.ClickSuggestions.GrwInfo.rwKind : Mathlib.Tactic.ClickSuggestions.GrwInfo → Mathlib.Tactic.ClickSuggestions.RwKind
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.addSubmonoidClosure_single : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R],
  AddSubmonoid.closure {x | ∃ m r, x = AddMonoidAlgebra.single m r} = ⊤
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.Cache.mk.sizeOf_spec : ∀ {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit}
  (map : Std.DHashMap Std.Tactic.BVDecide.BVExpr.Cache.Key fun k => Vector Std.Sat.AIG.Fanin k.w)
  (hbound :
    ∀ {i : ℕ} (k : Std.Tactic.BVDecide.BVExpr.Cache.Key) (h1 : k ∈ map) (h2 : i < k.w),
      (map.get k h1)[i].gate < aig.decls.size),
  sizeOf { map := map, hbound := hbound } = 1 + sizeOf map
-- Mathlib.Geometry.Manifold.ContMDiff.Atlas
contMDiffWithinAt_extChartAt_symm_target : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞} [IsManifold I n M] (x : M) {y : E},
  y ∈ (extChartAt I x).target →
    ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) I n (↑(extChartAt I x).symm) (extChartAt I x).target y
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.Rel.mul_left : ∀ {R : Type u} {X : Type v} [inst : CommRing R] (a : FreeNonUnitalNonAssocAlgebra R X)
  {b c : FreeNonUnitalNonAssocAlgebra R X}, FreeLieAlgebra.Rel R X b c → FreeLieAlgebra.Rel R X (a * b) (a * c)
-- Init.Data.SInt.Lemmas
ISize.ofNat_sub : ∀ (a b : ℕ), b ≤ a → ISize.ofNat (a - b) = ISize.ofNat a - ISize.ofNat b
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
FractionalIdeal.exists_notMem_one_of_ne_bot : ∀ {A : Type u_2} {K : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K]
  [inst_3 : IsFractionRing A K] [inst_4 : IsDedekindDomain A] {I : Ideal A}, I ≠ ⊥ → I ≠ ⊤ → ∃ x ∈ (↑I)⁻¹, x ∉ 1
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- Scalar multiplication acting on the domain.

This is not an instance as it would conflict with the action on the range.
See the file `MathlibTest/instance_diamonds.lean` for examples of such conflicts.  -/
SkewMonoidAlgebra.comapSMul : {G : Type u_2} →
  {M : Type u_6} →
    {α : Type u_7} → [inst : Monoid G] → [inst_1 : AddCommMonoid M] → [MulAction G α] → SMul G (SkewMonoidAlgebra M α)
-- Lean.Elab.BuiltinCommand
_private.Lean.Elab.BuiltinCommand.0.Lean.Elab.Command.elabReduce.go : Lean.Syntax → Lean.Syntax → Lean.Meta.Command.ReduceConfig → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.Util.Qq
/-- Return a local declaration whose type is definitionally equal to `sort`.

This is a Qq version of `Lean.Meta.findLocalDeclWithType?`  -/
Qq.findLocalDeclWithTypeQ? : {u : Lean.Level} → (sort : Q(Sort u)) → Lean.MetaM (Option Q(«$sort»))
-- Mathlib.Tactic.NormNum.NatSqrt
Mathlib.Meta.NormNum.isNat_sqrt : ∀ {x nx z : ℕ}, Mathlib.Meta.NormNum.IsNat x nx → nx.sqrt = z → Mathlib.Meta.NormNum.IsNat x.sqrt z
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.Struct.negFn : Lean.Meta.Grind.Arith.Linear.Struct → Lean.Expr
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_univ_getElem : ∀ {M : Type u_2} [inst : CommMonoid M] (l : List M), ∏ i, l[↑i] = l.prod
-- Init.Prelude
/-- Unpacks a `USize` into a `BitVec System.Platform.numBits`. This function is overridden with a native
implementation.
 -/
USize.toBitVec : USize → BitVec System.Platform.numBits
-- Mathlib.CategoryTheory.EqToHom
/-- We can push `eqToHom` to the left through families of morphisms.  -/
CategoryTheory.eqToHom_naturality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {β : Sort u_1} {f g : β → C} (z : (b : β) → f b ⟶ g b)
  {j j' : β} (w : j = j'),
  CategoryTheory.CategoryStruct.comp (z j) (CategoryTheory.eqToHom ⋯) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (z j')
-- Mathlib.Topology.UniformSpace.Cauchy
isCompact_iff_totallyBounded_isComplete : ∀ {α : Type u} [uniformSpace : UniformSpace α] {s : Set α}, IsCompact s ↔ TotallyBounded s ∧ IsComplete s
-- Lean.Elab.Command
_private.Lean.Elab.Command.0.Lean.Elab.Command.elabCommandUsing : Lean.Elab.Command.State →
  Lean.Syntax →
    List (Lean.KeyedDeclsAttribute.AttributeEntry Lean.Elab.Command.CommandElab) → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
/-- The image of a submodules basis is a module filter basis.  -/
SubmodulesBasis.toModuleFilterBasis : {ι : Type u_1} →
  {R : Type u_2} →
    [inst : CommRing R] →
      {M : Type u_4} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [inst_3 : TopologicalSpace R] →
              [Nonempty ι] → {B : ι → Submodule R M} → SubmodulesBasis B → ModuleFilterBasis R M
-- Mathlib.Analysis.SpecificLimits.Normed
geom_series_succ : ∀ {R : Type u_4} [inst : NormedRing R] [HasSummableGeomSeries R] (x : R),
  ‖x‖ < 1 → ∑' (i : ℕ), x ^ (i + 1) = ∑' (i : ℕ), x ^ i - 1
-- Lean.Elab.Term.TermElabM
/-- Create a synthetic sorry for the given expected type. If `expectedType? = none`, then a fresh
metavariable is created to represent the type.
 -/
_private.Lean.Elab.Term.TermElabM.0.Lean.Elab.Term.mkSyntheticSorryFor : Option Lean.Expr → Lean.Elab.TermElabM Lean.Expr