mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Birational.Composition
AlgebraicGeometry.Scheme.PartialMap.comp_restrict_right : ∀ {X Y Z : AlgebraicGeometry.Scheme} [inst : PreirreducibleSpace ↥X] [inst_1 : Nonempty ↥Y] (f : X.PartialMap Y)
  [inst_2 : AlgebraicGeometry.IsDominant f.hom] (g : Y.PartialMap Z) (V : Y.Opens) (hV : Dense ↑V) (hV' : V ≤ g.domain),
  f.comp (g.restrict V hV hV') =
    (f.comp g).restrict
      ((AlgebraicGeometry.Scheme.Hom.opensFunctor f.domain.ι).obj ((TopologicalSpace.Opens.map f.hom.base).obj V)) ⋯ ⋯
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.skipPrefix?_bool_eq_some_iff : ∀ {p : Char → Bool} {s : String.Slice} {pos : s.Pos},
  s.skipPrefix? p = some pos ↔ ∃ (h : s.startPos ≠ s.endPos), pos = s.startPos.next h ∧ p (s.startPos.get h) = true
-- Mathlib.Data.Sign.Defs
SignType.LE.of_pos : ∀ (a : SignType), a.LE SignType.pos
-- Std.Time.Time.Unit.Hour
Std.Time.Hour.instLawfulEqOrdOrdinal : Std.LawfulEqOrd Std.Time.Hour.Ordinal
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.HasAffineProperty.of_openCover : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : AlgebraicGeometry.AffineTargetMorphismProperty}
  [AlgebraicGeometry.HasAffineProperty P Q] {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (𝒰 : Y.OpenCover)
  [inst : ∀ (i : 𝒰.I₀), AlgebraicGeometry.IsAffine (𝒰.X i)],
  (∀ (i : 𝒰.toPreZeroHypercover.1), Q (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰 f i)) → P f
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getEntryGT_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) {k : α} {he : ∃ a ∈ t₁, compare a k = Ordering.gt},
  Std.DTreeMap.Internal.Impl.getEntryGT k t₁ ⋯ he = Std.DTreeMap.Internal.Impl.getEntryGT k t₂ ⋯ ⋯
-- Init.Data.Vector.Find
Vector.isSome_findFinIdx? : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {p : α → Bool}, (Vector.findFinIdx? p xs).isSome = xs.any p
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.mem_prod : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] {s : NonUnitalSubring R}
  {t : NonUnitalSubring S} {p : R × S}, p ∈ s.prod t ↔ p.1 ∈ s ∧ p.2 ∈ t
-- Lean.Elab.Command
/-- Execute the monadic action `elabFn xs` as a `CommandElabM` monadic action, where `xs` are free variables
corresponding to all active scoped variables declared using the `variable` command.

This method is similar to `liftTermElabM`, but it elaborates all scoped variables declared using the `variable`
command.

Example:
```
public import Lean

public section

open Lean Elab Command Meta

variable {α : Type u} {f : α → α}
variable (n : Nat)

#eval
  runTermElabM fun xs => do
    for x in xs do
      IO.println s!"{← ppExpr x} : {← ppExpr (← inferType x)}"
```
 -/
Lean.Elab.Command.runTermElabM : {α : Type} → (Array Lean.Expr → Lean.Elab.TermElabM α) → Lean.Elab.Command.CommandElabM α
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_eq_get!_getElem? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {a : α}, t[a]! = t[a]?.get!
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.injective_domRestrict_iff : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Ring R] [inst_1 : Ring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  {f : M →ₛₗ[τ₁₂] M₂} {S : Submodule R M}, Function.Injective ⇑(f.domRestrict S) ↔ Disjoint S f.ker
-- Mathlib.Order.Filter.AtTopBot.Defs
Filter.Iic_mem_atBot : ∀ {α : Type u_3} [inst : Preorder α] (a : α), Set.Iic a ∈ Filter.atBot
-- Mathlib.Analysis.InnerProductSpace.Subspace
Orthonormal.codRestrict : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {v : ι → E},
  Orthonormal 𝕜 v → ∀ (s : Submodule 𝕜 E) (hvs : ∀ (i : ι), v i ∈ s), Orthonormal 𝕜 (Set.codRestrict v (↑s) hvs)
-- Mathlib.Tactic.Linter.TextBased
/-- Verifies that no module in `modules` contains CON, PRN, AUX, NUL, COM1, COM2, COM3, COM4, COM5,
COM6, COM7, COM8, COM9, COM¹, COM², COM³, LPT1, LPT2, LPT3, LPT4, LPT5, LPT6, LPT7, LPT8, LPT9,
LPT¹, LPT² or LPT³ in its filename, as these are forbidden on Windows.

Also verify that module names contain no forbidden characters such as `*`, `?` (Windows),
`!` (forbidden on Nix OS), `.` (might result from confusion with a module name)
or `'` (causes shell escaping issues in scripts).

Source: https://learn.microsoft.com/en-gb/windows/win32/fileio/naming-a-file.
Return the number of module names violating this rule.  -/
Mathlib.Linter.TextBased.modulesOSForbidden : Lean.Linter.LinterOptions → Array Lean.Name → IO ℕ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey_erase_eq_of_not_compare_eq_minKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : (t.erase k).isEmpty = false}, ¬cmp k (t.minKey ⋯) = Ordering.eq → (t.erase k).minKey he = t.minKey ⋯
-- Mathlib.Data.Num.Basic
instDecidableEqPosNum.decEq : (x x_1 : PosNum) → Decidable (x = x_1)
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.ihom.coev_ev_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (A B : C)
  [inst_2 : CategoryTheory.Closed A] {Z : C} (h : A ⟹ B ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev A).app (A ⟹ B))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom A).map ((CategoryTheory.ihom.ev A).app B)) h) =
    h
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
le_algebraMap_of_spectrum_le : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [ContinuousSqrt R]
  [StarOrderedRing R] [inst_8 : TopologicalSpace A] [inst_9 : Ring A] [inst_10 : StarRing A] [inst_11 : PartialOrder A]
  [StarOrderedRing A] [inst_13 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {r : R} {a : A},
  (∀ x ∈ spectrum R a, x ≤ r) → autoParam (p a) le_algebraMap_of_spectrum_le._auto_1 → a ≤ (algebraMap R A) r
-- Mathlib.Algebra.DualNumber
/-- A universal property of the dual numbers, providing a unique `A[ε] →ₐ[R] B` for every map
`f : A →ₐ[R] B` and a choice of element `e : B` which squares to `0` and commutes with the range of
`f`.

This isomorphism is named to match the similar `Complex.lift`.
Note that when `f : R →ₐ[R] B := Algebra.ofId R B`, the commutativity assumption is automatic, and
we are free to choose any element `e : B`.  -/
DualNumber.lift : {R : Type u_1} →
  {B : Type u_3} →
    {A : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] →
                { fe // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 (fe.1 a) } ≃ (DualNumber A →ₐ[R] B)
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.instNonemptyMap : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v', u'} D]
  (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor C D) [P.Nonempty], (P.map F).Nonempty
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
/-- the Leibniz pushout  -/
CategoryTheory.Functor.PushoutObjObj.ι : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} →
              {X₁ Y₁ : C₁} →
                {f₁ : X₁ ⟶ Y₁} →
                  {X₂ Y₂ : C₂} → {f₂ : X₂ ⟶ Y₂} → (self : F.PushoutObjObj f₁ f₂) → self.pt ⟶ (F.obj Y₁).obj Y₂
-- Std.Data.HashMap.IteratorLemmas
_private.Std.Data.HashMap.IteratorLemmas.0.Std.HashMap.Raw.valuesIter.eq_1 : ∀ {α β : Type u} (m : Std.HashMap.Raw α β), m.valuesIter = m.inner.valuesIter
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.elabMatchAltViews.updateMatchType : Array Lean.Expr → Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
/-- Consider a point `x` at which a set `s` has density one, with respect to closed balls (i.e.,
a Lebesgue density point of `s`). Then `s` intersects the rescaled copies `{x} + r • t` of a given
set `t` with positive measure, for any small enough `r`.  -/
MeasureTheory.Measure.eventually_nonempty_inter_smul_of_density_one : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (s : Set E) (x : E),
  Filter.Tendsto (fun r => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0))
      (nhds 1) →
    ∀ (t : Set E), MeasurableSet t → μ t ≠ 0 → ∀ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), (s ∩ ({x} + r • t)).Nonempty
-- Mathlib.ModelTheory.Arithmetic.Presburger.Basic
FirstOrder.Language.presburger.realize_nsmul : ∀ {α : Type u_1} {t : FirstOrder.Language.presburger.Term α} {M : Type u_2} {v : α → M} [inst : AddMonoidWithOne M]
  {n : ℕ}, FirstOrder.Language.Term.realize v (n • t) = n • FirstOrder.Language.Term.realize v t
-- Mathlib.Data.Multiset.Defs
Multiset.nodupDecidable : {α : Type u_1} → [DecidableEq α] → (s : Multiset α) → Decidable s.Nodup
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.RotateRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateRight.go_get_aux : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (distance : ℕ)
  (input : aig.RefVec w) (curr : ℕ) (hcurr : curr ≤ w) (s : aig.RefVec curr) (idx : ℕ) (hidx : idx < curr),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateRight.go input distance curr hcurr s).get idx ⋯ = s.get idx hidx
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
CategoryTheory.Limits.map_π_preserves_coequalizer_inv_desc_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y : C} (f g : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCoequalizer f g]
  [inst_3 : CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)]
  [inst_4 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G] {W : D} (k : G.obj Y ⟶ W)
  (wk : CategoryTheory.CategoryStruct.comp (G.map f) k = CategoryTheory.CategoryStruct.comp (G.map g) k) {Z : D}
  (h : W ⟶ Z),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.coequalizer.π f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCoequalizer.iso G f g).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.desc k wk) h)) =
    CategoryTheory.CategoryStruct.comp k h
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
/-- `WellFormedBasis basis` means that all functions from `basis` tend to `atTop`, and
`basis` is sorted such that if
`g` goes after `f` in `basis`, then `log f =o[atTop] log g`.

We use two types `Basis` and `WellFormedBasis` instead of a single bundled one because it
it lets us to use the `List` API for `Basis`.  -/
Tactic.ComputeAsymptotics.WellFormedBasis : Tactic.ComputeAsymptotics.Basis → Prop
-- Mathlib.Tactic.Linter.CommandRanges
/-- The "commandRanges" linter logs the `getRange?` and the `getRangeWithTrailing?` for each command.
The format is `[start, end, trailing]`, where
* `start` is the start of the command,
* `end` is the end of the command, not including trailing whitespace and comments,
* `trailing` is the "syntactic end" of the command, so it contains all trailing whitespace and
  comments.

Thus, assuming that there has been no tampering with positions/synthetic syntax,
if the current command is followed by another command, then `trailing` for the previous command
coincides with `start` of the following.
 -/
_private.Mathlib.Tactic.Linter.CommandRanges.0.Mathlib.Linter.CommandRanges.commandRangesLinter : Lean.Linter
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkspaceEdit.instEmptyCollection : EmptyCollection Lean.Lsp.WorkspaceEdit
-- Aesop.Tree.Data
Aesop.Goal.setChildren : Array Aesop.RappRef → Aesop.Goal → Aesop.Goal
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
/-- The natural additive group isomorphism between fixing additive subgroups.  -/
SubAddAction.fixingAddSubgroupInsertEquiv : {M : Type u_1} →
  {α : Type u_2} →
    [inst : AddGroup M] →
      [inst_1 : AddAction M α] →
        (a : α) →
          (s : Set ↥(SubAddAction.ofStabilizer M a)) →
            ↥(fixingAddSubgroup M (insert a (Subtype.val '' s))) ≃+ ↥(fixingAddSubgroup (↥(AddAction.stabilizer M a)) s)
-- Mathlib.Algebra.Quaternion
Quaternion.coe_inv : ∀ {R : Type u_1} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] (x : R), ↑x⁻¹ = (↑x)⁻¹
-- Lean.Elab.PatternVar
Lean.Elab.Term.getPatternVarNames : Array Lean.Elab.Term.PatternVar → Array Lean.Name
-- Mathlib.MeasureTheory.Measure.NullMeasurable
Finset.nullMeasurableSet_biInter : ∀ {ι : Type u_1} {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ι → Set α} (s : Finset ι),
  (∀ b ∈ s, MeasureTheory.NullMeasurableSet (f b) μ) → MeasureTheory.NullMeasurableSet (⋂ b ∈ s, f b) μ
-- Mathlib.CategoryTheory.Iso
CategoryTheory.isIso_comp_right_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (g : Z ⟶ Y) (f : Y ⟶ X) [CategoryTheory.IsIso f],
  CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp g f) ↔ CategoryTheory.IsIso g
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.JordanDecomposition.mutuallySingular : ∀ {α : Type u_2} [inst : MeasurableSpace α] (self : MeasureTheory.JordanDecomposition α),
  self.posPart.MutuallySingular self.negPart
-- Mathlib.Topology.Order.LocalExtr
isLocalMaxOn_const : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {s : Set α} {a : α} {b : β},
  IsLocalMaxOn (fun x => b) s a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey!_insertIfNew! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF →
    ∀ {k : α} {v : β k},
      (Std.DTreeMap.Internal.Impl.insertIfNew! k v t).maxKey! =
        t.maxKey?.elim k fun k' => if compare k' k = Ordering.lt then k else k'
-- Mathlib.RingTheory.Algebraic.Integral
/-- If `x : K` is algebraic over `ℤ`, then a nonzero `ℕ`-multiple of it is contained in the
integral closure of `ℤ` in `K`.  -/
IsAlgebraic.exists_nsmul_eq : ∀ (S : Type u_2) [inst : CommRing S] {K : Type u_4} [inst_1 : CommRing K] [inst_2 : Algebra S K]
  [IsIntegralClosure S ℤ K] {x : K}, IsAlgebraic ℤ x → ∃ m s, m ≠ 0 ∧ m • x = (algebraMap S K) s
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
SSet.degenerate_iff_of_isIso : ∀ {X Y : SSet} (f : X ⟶ Y) [CategoryTheory.IsIso f] {n : ℕ} (x : X.obj (Opposite.op { len := n })),
  (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := n }))) x ∈ Y.degenerate n ↔ x ∈ X.degenerate n
-- Init.Data.SInt.Lemmas
Int8.toInt64_toInt32 : ∀ (n : Int8), n.toInt32.toInt64 = n.toInt64
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- The `vectorSpan` of an indexed family of `n + 1` points has
dimension at most `n`.  -/
finrank_vectorSpan_range_le : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : Fintype ι] (p : ι → P) {n : ℕ},
  Fintype.card ι = n + 1 → Module.finrank k ↥(vectorSpan k (Set.range p)) ≤ n
-- Aesop.Search.Expansion.Simp
Aesop.SimpResult.newGoal? : Aesop.SimpResult → Option Lean.MVarId
-- Std.Async.Signal
/-- File size limit exceeded.
 -/
Std.Async.Signal.sigxfsz : Std.Async.Signal
-- Mathlib.Geometry.Euclidean.NinePointCircle
Affine.Simplex.ninePointCircle_radius : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n), s.ninePointCircle.radius = s.circumradius / ↑n
-- Batteries.Data.String.Matcher
/-- The pattern for the matcher  -/
String.Matcher.pattern : String.Matcher → Substring.Raw
-- Mathlib.Analysis.Normed.Module.Basic
MulOpposite.instNormedSpace : {𝕜 : Type u_1} →
  {E : Type u_3} → [inst : NormedField 𝕜] → [inst_1 : SeminormedAddCommGroup E] → [NormedSpace 𝕜 E] → NormedSpace 𝕜 Eᵐᵒᵖ
-- Mathlib.Analysis.Normed.Module.FiniteDimension
/-- In an infinite-dimensional space, given a finite number of points, one may find a point
with norm at most `R` which is at distance at least `1` of all these points.  -/
exists_norm_le_le_norm_sub_of_finset : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CompleteSpace 𝕜] {c : 𝕜},
  1 < ‖c‖ → ∀ {R : ℝ}, ‖c‖ < R → ¬FiniteDimensional 𝕜 E → ∀ (s : Finset E), ∃ x, ‖x‖ ≤ R ∧ ∀ y ∈ s, 1 ≤ ‖y - x‖
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRank_lt_top_iff : ∀ {α : Type u_1} {M : Matroid α}, M.eRank < ⊤ ↔ M.RankFinite
-- Mathlib.Analysis.InnerProductSpace.Positive
/-- `A.toMatrix` is positive semi-definite if and only if `A` is positive.  -/
LinearMap.posSemidef_toMatrix_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] {A : E →ₗ[𝕜] E} (b : OrthonormalBasis ι 𝕜 E),
  ((LinearMap.toMatrix b.toBasis b.toBasis) A).PosSemidef ↔ A.IsPositive
-- Lean.Elab.ConfigEval.Commands
/-- `derive_eval_expr_instance_using_meta_eval type` defines a `ConfigItem.EvalExpr type` instance
using `Meta.evalExpr'` to evaluate expressions. This sort of item evaluator is a reasonable
backup strategy for infrequently used configuration options, if term- or expression-based
evaluation does not work and the cost of compilation is acceptible.

This should be avoided in core Lean due to the difficulties it creates for bootstrapping.
 -/
Lean.Elab.ConfigEval.deriveEvalExprUsingMeta : Lean.ParserDescr
-- Mathlib.Lean.Elab.InfoTree
/-- Get the declarations elaborated in the infotree `t` which are theorems according to the
environment. This includes e.g. `instance`s of `Prop` classes in addition to declarations declared
using the keyword `theorem` directly.
 -/
Lean.Elab.InfoTree.getTheorems : Lean.Elab.InfoTree → Lean.Environment → List Lean.ConstantVal
-- Mathlib.SetTheory.Cardinal.Continuum
Cardinal.continuum_add_nat : ∀ (n : ℕ), Cardinal.continuum + ↑n = Cardinal.continuum
-- Mathlib.Logic.Equiv.Defs
Equiv.sigmaCongrRight_apply : ∀ {α : Type u_3} {β₁ : α → Type u_1} {β₂ : α → Type u_2} (F : (a : α) → β₁ a ≃ β₂ a) (a : (a : α) × β₁ a),
  (Equiv.sigmaCongrRight F) a = ⟨a.fst, (F a.fst) a.snd⟩
-- Mathlib.Algebra.BigOperators.Ring.Finset
Finset.sum_boole : ∀ {ι : Type u_1} {R : Type u_4} [inst : AddCommMonoidWithOne R] (p : ι → Prop) [inst_1 : DecidablePred p]
  (s : Finset ι), (∑ x ∈ s, if p x then 1 else 0) = ↑{x ∈ s | p x}.card
-- Mathlib.CategoryTheory.Limits.Chosen.End
CategoryTheory.Limits.chosenEnd.map_π_assoc : ∀ {J : Type u_3} {C : Type u_4} [inst : CategoryTheory.Category.{v_3, u_4} C]
  [inst_1 : CategoryTheory.Category.{v_4, u_3} J] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)}
  [inst_2 : CategoryTheory.Limits.ChosenEndsOfShape J C] {G : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)}
  (f : F ⟶ G) (j : J) {Z : C} (h : (G.obj (Opposite.op j)).obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.chosenEnd.map f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.chosenEnd.π G j) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.chosenEnd.π F j)
      (CategoryTheory.CategoryStruct.comp ((f.app (Opposite.op j)).app j) h)
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
linearIndepOn_insert_iff : ∀ {ι : Type u'} {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {s : Set ι} {a : ι} {f : ι → V},
  LinearIndepOn K f (insert a s) ↔ LinearIndepOn K f s ∧ (f a ∈ Submodule.span K (f '' s) → a ∈ s)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The forward map of a homeomorphism is a continuous function.  -/
ContinuousAddEquiv.continuous_toFun : ∀ {G : Type u} [inst : TopologicalSpace G] {H : Type v} [inst_1 : TopologicalSpace H] [inst_2 : Add G] [inst_3 : Add H]
  (self : G ≃ₜ+ H), Continuous self.toFun
-- Mathlib.Order.Interval.Finset.Basic
Finset.image_subset_Iic_sup : ∀ {ι : Type u_1} {α : Type u_2} [inst : SemilatticeSup α] [inst_1 : LocallyFiniteOrderBot α] [inst_2 : OrderBot α]
  [inst_3 : DecidableEq α] (f : ι → α) (s : Finset ι), Finset.image f s ⊆ Finset.Iic (s.sup f)
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.instFourierAdd : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
  [inst_2 : FiniteDimensional ℝ E] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] [inst_5 : AddCommGroup F]
  [inst_6 : Module ℂ F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousConstSMul ℂ F], FourierAdd (TemperedDistribution E F) (TemperedDistribution E F)
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
mem_fixingAddSubgroup_iff_subset_fixedBy : ∀ (M : Type u_1) {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {s : Set α} {m : M},
  m ∈ fixingAddSubgroup M s ↔ s ⊆ AddAction.fixedBy α m
-- Mathlib.Data.Nat.Factorization.Defs
Nat.factorization_eq_zero_of_not_dvd : ∀ {n p : ℕ}, ¬p ∣ n → n.factorization p = 0
-- Mathlib.Logic.Relation
Relation.reflTransGen_eq_self : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Refl r] [IsTrans α r], Relation.ReflTransGen r = r
-- Mathlib.Algebra.AffineMonoid.UniqueSums
AffineMonoid.to_twoUniqueProds : ∀ {M : Type u_1} [inst : CancelCommMonoid M] [Monoid.FG M] [IsMulTorsionFree M], TwoUniqueProds M
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.normalize_lcm : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
  {f : β → α}, normalize (s.lcm f) = s.lcm f
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_const : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : CommMonoid M] (b : M), ∏ _x ∈ s, b = b ^ s.card
-- Init.Data.Iterators.Basic
/-- The type of the step object returned by `Iter.step`, containing an `IterStep`
and a proof that this is a plausible step for the given iterator.
 -/
Std.Iter.Step : {α β : Type w} → [Std.Iterator α Id β] → Std.Iter β → Type (max 0 w)
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.IsColimit.funext : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} {c : F.CoconeTypes},
  c.IsColimit → ∀ {T : Type w₂} {f g : c.pt → T}, (∀ (j : J), f ∘ c.ι j = g ∘ c.ι j) → f = g
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.ComonadHom.app_δ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {M N : CategoryTheory.Comonad C}
  (self : CategoryTheory.ComonadHom M N) (X : C),
  CategoryTheory.CategoryStruct.comp (self.app X) (N.δ.app X) =
    CategoryTheory.CategoryStruct.comp (M.δ.app X)
      (CategoryTheory.CategoryStruct.comp (self.app (M.obj X)) (N.map (self.app X)))
-- Mathlib.Algebra.Lie.CartanExists
LieAlgebra.engel_isBot_of_isMin.lieCharpoly_monic : ∀ (R : Type u_2) {L : Type u_3} (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : Module.Finite R L] [inst_8 : Module.Free R L] [inst_9 : Module.Finite R M] [inst_10 : Module.Free R M]
  (x y : L), (LieAlgebra.engel_isBot_of_isMin.lieCharpoly✝ R M x y).Monic
-- Mathlib.Data.Set.Basic
Set.inter_inter_inter_comm : ∀ {α : Type u} (s t u v : Set α), s ∩ t ∩ (u ∩ v) = s ∩ u ∩ (t ∩ v)