mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.Algebra.SMul
Diffeomorph.vadd.eq_1 : ∀ {𝕜 : 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) {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  (I' : ModelWithCorners 𝕜 E' H') {G : Type u_8} [inst_7 : TopologicalSpace G] [inst_8 : ChartedSpace H G]
  {M : Type u_9} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H' M] [inst_11 : AddGroup G]
  [inst_12 : AddAction G M] (n : WithTop ℕ∞) [inst_13 : ContMDiffVAdd I I' n G M] (g : G),
  Diffeomorph.vadd I I' n g = { toEquiv := AddAction.toPerm g, contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }
-- Mathlib.Algebra.Order.Star.Basic
star_le_iff : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  {x y : R}, star x ≤ y ↔ x ≤ star y
-- Mathlib.Order.Filter.Basic
Filter.GenerateSets.brecOn : ∀ {α : Type u} {g : Set (Set α)} {motive : (a : Set α) → Filter.GenerateSets g a → Prop} {a : Set α}
  (t : Filter.GenerateSets g a),
  (∀ (a : Set α) (t : Filter.GenerateSets g a), Filter.GenerateSets.below t → motive a t) → motive a t
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.node.parenthesizer : Lean.SyntaxNodeKind → Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Init.Core
instDecidableEqSum : {α : Type u_1} → {β : Type u_2} → [DecidableEq α] → [DecidableEq β] → DecidableEq (α ⊕ β)
-- Mathlib.CategoryTheory.GradedObject.Bifunctor
CategoryTheory.GradedObject.instIsIsoMapBifunctorMapMap : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {I : Type u_4} {J : Type u_5} {K : Type u_6}
  (p : I × J → K) {X₁ X₂ : CategoryTheory.GradedObject I C₁} {Y₁ Y₂ : CategoryTheory.GradedObject J C₂}
  [inst_3 : (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₁).obj Y₁).HasMap p]
  [inst_4 : (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₂).obj Y₂).HasMap p] (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂)
  [CategoryTheory.IsIso f] [CategoryTheory.IsIso g],
  CategoryTheory.IsIso (CategoryTheory.GradedObject.mapBifunctorMapMap F p f g)
-- Init.Data.Vector.Count
Vector.countP_false : ∀ {α : Type u_1} {n : ℕ}, (Vector.countP fun x => false) = fun x => 0
-- Mathlib.LinearAlgebra.Eigenspace.Zero
LinearMap.finrank_genEigenspace_le : ∀ {K : Type u_2} {M : Type u_3} [inst : Field K] [inst_1 : AddCommGroup M] [inst_2 : Module K M]
  [inst_3 : Module.Finite K M] (φ : Module.End K M) (μ : K) (k : ℕ),
  Module.finrank K ↥((φ.genEigenspace μ) ↑k) ≤ Polynomial.rootMultiplicity μ (LinearMap.charpoly φ)
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.le_noEdge_iff : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β} {X : Set α}, G ≤ Graph.noEdge X β ↔ G.vertexSet ⊆ X ∧ G.edgeSet = ∅
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.subset_normalClosure : ∀ {G : Type u_1} [inst : Group G] {s : Set G}, s ⊆ ↑(Subgroup.normalClosure s)
-- Mathlib.CategoryTheory.Iso
CategoryTheory.isIso_iff_of_thin : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [Quiver.IsThin C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.IsIso f ↔ Nonempty (Y ⟶ X)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_maxKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = false → ∀ {fallback : α}, t.getKey? (t.maxKeyD fallback) = some (t.maxKeyD fallback)
-- Mathlib.CategoryTheory.ObjectProperty.Kernels
/-- If an object property `P` is closed under cokernels, then `P.ι` creates cokernels.
In particular, this implies `P.ι` preserves cokernels.  -/
CategoryTheory.ObjectProperty.createsCokernels : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (P : CategoryTheory.ObjectProperty C) →
        [P.IsClosedUnderCokernels] →
          {X Y : P.FullSubcategory} →
            (f : X ⟶ Y) →
              [CategoryTheory.Limits.HasCokernel f.hom] →
                CategoryTheory.CreatesColimit (CategoryTheory.Limits.parallelPair f 0) P.ι
-- Mathlib.Analysis.Fourier.Notation
/-- `𝓕⁻ f` is the inverse Fourier transform of `f`. The meaning of this notation is
type-dependent.  -/
FourierTransformInv.fourierInv : {E : Type u} → {F : outParam (Type v)} → [self : FourierTransformInv E F] → E → F
-- Mathlib.Order.CompleteLattice.Basic
Monotone.iSup : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : Preorder α] [inst_1 : CompleteLattice β] {f : ι → α → β},
  (∀ (i : ι), Monotone (f i)) → Monotone (⨆ i, f i)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.smul_single' : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (r' : R) (m : M) (r : R),
  r' • AddMonoidAlgebra.single m r = AddMonoidAlgebra.single m (r' * r)
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.Hom.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X Y : C),
  (CategoryTheory.WithInitial.of X).Hom (CategoryTheory.WithInitial.of Y) = (X ⟶ Y)
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.«termλ» : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Ordered
Std.DTreeMap.Internal.Impl.Ordered.compare_left_beq_gt : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {k : α → Ordering} [Std.Internal.IsStrictCut compare k]
  {sz : ℕ} {k' : α} {v' : β k'} {l r : Std.DTreeMap.Internal.Impl α β},
  (Std.DTreeMap.Internal.Impl.inner sz k' v' l r).Ordered →
    (k k').isGE = true → ∀ p ∈ l.toListModel, (k p.fst == Ordering.gt) = true
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
/-- If the right adjoint is full, then each component of the counit is a split monomorphism.  -/
CategoryTheory.Adjunction.counitSplitMonoOfRFull : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {L : CategoryTheory.Functor C D} →
          {R : CategoryTheory.Functor D C} →
            (h : L ⊣ R) → [R.Full] → (X : D) → CategoryTheory.SplitMono (h.counit.app X)
-- Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence
/-- Pull back a right rigid structure along an equivalence.  -/
CategoryTheory.rightRigidCategoryOfEquivalence : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              [F.Monoidal] →
                {G : CategoryTheory.Functor D C} →
                  (F ⊣ G) →
                    [F.IsEquivalence] → [CategoryTheory.RightRigidCategory D] → CategoryTheory.RightRigidCategory C
-- Std.Async.Process
Std.IO.Process.instReprResourceUsageStats.repr : Std.IO.Process.ResourceUsageStats → ℕ → Std.Format
-- Mathlib.Algebra.Expr
/-- Produce a `Zero` instance for `Q($α)` such that `0 : Q($α)` is `q(0 : $α)`.  -/
Expr.instZero : {u : Lean.Level} → (α : Q(Type u)) → Q(Zero «$α») → Zero Q(«$α»)
-- Mathlib.Algebra.Order.Quantale
Quantale.mk.sizeOf_spec : ∀ {α : Type u_1} [inst : Semigroup α] [inst_1 : CompleteLattice α] [inst_2 : IsQuantale α] [inst_3 : SizeOf α],
  sizeOf { } = 1
-- Lean.Util.Trace
Lean.resetTraceState : {m : Type → Type} → [Lean.MonadTrace m] → m Unit
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.Stmt.halt : {K : Type u_1} → {Γ : K → Type u_2} → {Λ : Type u_3} → {σ : Type u_4} → Turing.TM2.Stmt Γ Λ σ
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.contains'.match_1.splitter : (motive : Ordering → Sort u_1) →
  (x : Ordering) → (Unit → motive Ordering.lt) → (Unit → motive Ordering.gt) → (Unit → motive Ordering.eq) → motive x
-- Mathlib.Topology.ContinuousMap.Units
ContinuousMap.unitsLift_apply_inv_apply : ∀ {X : Type u_1} {M : Type u_2} [inst : TopologicalSpace X] [inst_1 : Monoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : ContinuousMul M] (f : C(X, Mˣ)) (x : X), ↑(ContinuousMap.unitsLift f)⁻¹ x = ↑(f x)⁻¹
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.maxEntry.match_1.congr_eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : (x : Std.DTreeMap.Internal.Impl α fun x => β) → x.isEmpty = false → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl α fun x => β) (x_1 : x.isEmpty = false)
  (h_1 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            (x : (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).isEmpty = false) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l l_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β) →
                  (l_2 r : Std.DTreeMap.Internal.Impl α fun x => β) →
                    l_1 = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_2 r →
                      (h :
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                                (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_2 r)).isEmpty =
                            false) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                            (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_2 r))
                          h)
  (size : ℕ) (k : α) (v : β) (l : Std.DTreeMap.Internal.Impl α fun x => β) (size_1 : ℕ) (k_1 : α) (v_1 : β)
  (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β)
  (h :
    (Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)).isEmpty =
      false),
  x = Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) →
    x_1 ≍ h →
      (match x, x_1 with
        | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => h_1 size k v l x
        | Std.DTreeMap.Internal.Impl.inner size k v l l_2@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_3 r),
          h_3 => h_2 size k v l l_2 size_2 k_2 v_2 l_3 r h h_3) ≍
        h_2 size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) size_1 k_1 v_1 l_1 r ⋯ h
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.Heap.WF.deleteMin : ∀ {α : Type u_1} {le : α → α → Bool} {n : ℕ} {a : α} {s' s : Batteries.BinomialHeap.Imp.Heap α},
  Batteries.BinomialHeap.Imp.Heap.WF le n s →
    Batteries.BinomialHeap.Imp.Heap.deleteMin le s = some (a, s') → Batteries.BinomialHeap.Imp.Heap.WF le 0 s'
-- Std.Sat.AIG.Relabel
/-- `relabel` preserves unsatisfiablility.
 -/
Std.Sat.AIG.relabel_unsat_iff : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {β : Type} [inst_2 : Hashable β] [inst_3 : DecidableEq β]
  {idx : ℕ} {invert : Bool} {aig : Std.Sat.AIG α} {r : α → β} {hidx1 : idx < (Std.Sat.AIG.relabel r aig).decls.size}
  {hidx2 : idx < aig.decls.size},
  (∀ (x y : α), x ∈ aig → y ∈ aig → r x = r y → x = y) →
    ((Std.Sat.AIG.relabel r aig).UnsatAt idx invert hidx1 ↔ aig.UnsatAt idx invert hidx2)
-- Mathlib.Analysis.Calculus.Gradient.Basic
gradient.congr_simp : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] (f f_1 : F → 𝕜), f = f_1 → ∀ (x x_1 : F), x = x_1 → gradient f x = gradient f_1 x_1
-- Mathlib.Analysis.Fourier.AddCircle
tsum_sq_fourierCoeffOn : ∀ {a b : ℝ} {f : ℝ → ℂ} (hab : a < b),
  MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (Set.Ioc a b)) →
    ∑' (i : ℤ), ‖fourierCoeffOn hab f i‖ ^ 2 = (b - a)⁻¹ • ∫ (x : ℝ) in a..b, ‖f x‖ ^ 2
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.ResidueField.mapAlgEquiv'_residue : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsLocalRing S]
  [inst_3 : CommRing T] [inst_4 : IsLocalRing T] [inst_5 : Algebra R S] [inst_6 : Algebra R T]
  [inst_7 : IsLocalHom (algebraMap R S)] [inst_8 : IsLocalHom (algebraMap R T)] [inst_9 : IsLocalRing R] (e : S ≃ₐ[R] T)
  (x : S), (IsLocalRing.ResidueField.mapAlgEquiv' e) ((IsLocalRing.residue S) x) = (IsLocalRing.residue T) (e x)
-- Lean.Data.Lsp.CodeActions
/-- Capabilities of the server for handling code actions.  -/
Lean.Lsp.CodeActionOptions : Type
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The direction of the inf of two affine subspaces is less than or equal to the inf of their
directions.  -/
AffineSubspace.direction_inf : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] (s₁ s₂ : AffineSubspace k P), (s₁ ⊓ s₂).direction ≤ s₁.direction ⊓ s₂.direction
-- Mathlib.Algebra.Polynomial.Eval.Defs
/-- `eval₂` as a `RingHom`  -/
Polynomial.eval₂RingHom : {R : Type u} → {S : Type v} → [inst : Semiring R] → [inst_1 : CommSemiring S] → (R →+* S) → S → Polynomial R →+* S
-- Mathlib.Order.BoundedOrder.Basic
ULift.instOrderTop.eq_1 : ∀ {α : Type u} [inst : LE α] [inst_1 : OrderTop α], ULift.instOrderTop = OrderTop.lift ULift.down ⋯ ⋯
-- Std.Http.Transport
/-- Get a selector for receiving data asynchronously.
 -/
Std.Http.Transport.recvSelector : {α : Type} → [self : Std.Http.Transport α] → α → UInt64 → Std.Async.Selector (Option ByteArray)
-- Lean.Data.Lsp.CodeActions
/-- The server provides support to resolve additional information for a code action.  -/
Lean.Lsp.CodeActionOptions.resolveProvider? : Lean.Lsp.CodeActionOptions → Option Bool
-- Mathlib.Algebra.Quaternion
Quaternion.normSq_star : ∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R), Quaternion.normSq (star a) = Quaternion.normSq a
-- Aesop.Tracing
Aesop.TraceOption.traceClass : Aesop.TraceOption → Lean.Name
-- Mathlib.Topology.Metrizable.Basic
TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace : ∀ (X : Type u_5) [inst : TopologicalSpace X] [LindelofSpace X] [TopologicalSpace.PseudoMetrizableSpace X],
  SecondCountableTopology X
-- Mathlib.RingTheory.Coalgebra.Hom
/-- Given `R`-modules `A, B` with comultiplication maps `Δ_A, Δ_B` and counit maps
`ε_A, ε_B`, an `R`-coalgebra homomorphism `A →ₗc[R] B` is an `R`-linear map `f` such that
`ε_B ∘ f = ε_A` and `(f ⊗ f) ∘ Δ_A = Δ_B ∘ f`.  -/
«term_→ₗc_» : Lean.TrailingParserDescr
-- Lean.Environment
_private.Lean.Environment.0.Lean.VisibilityMap.const : {α : Type} → α → Lean.VisibilityMap✝ α
-- Aesop.Rule.Name
Aesop.PhaseName.norm : Aesop.PhaseName
-- Mathlib.ModelTheory.Encoding
_private.Mathlib.ModelTheory.Encoding.0.FirstOrder.Language.BoundedFormula.listDecode.match_1.eq_3 : ∀ {L : FirstOrder.Language} {α : Type u_3}
  (motive : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) → Sort u_4) (n : ℕ) (R : L.Relations n)
  (k : ℕ) (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ))
  (h_1 :
    (n : ℕ) →
      (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) →
        motive (Sum.inr (Sum.inr n.succ.succ) :: l))
  (h_2 :
    (n₁ : ℕ) →
      (t₁ : L.Term (α ⊕ Fin n₁)) →
        (n₂ : ℕ) →
          (t₂ : L.Term (α ⊕ Fin n₂)) →
            (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) →
              motive (Sum.inl ⟨n₁, t₁⟩ :: Sum.inl ⟨n₂, t₂⟩ :: l))
  (h_3 :
    (n : ℕ) →
      (R : L.Relations n) →
        (k : ℕ) →
          (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) →
            motive (Sum.inr (Sum.inl ⟨n, R⟩) :: Sum.inr (Sum.inr k) :: l))
  (h_4 : (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) → motive (Sum.inr (Sum.inr 0) :: l))
  (h_5 : (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) → motive (Sum.inr (Sum.inr 1) :: l))
  (h_6 : (x : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) → motive x),
  (match Sum.inr (Sum.inl ⟨n, R⟩) :: Sum.inr (Sum.inr k) :: l with
    | Sum.inr (Sum.inr n.succ.succ) :: l => h_1 n l
    | Sum.inl ⟨n₁, t₁⟩ :: Sum.inl ⟨n₂, t₂⟩ :: l => h_2 n₁ t₁ n₂ t₂ l
    | Sum.inr (Sum.inl ⟨n, R⟩) :: Sum.inr (Sum.inr k) :: l => h_3 n R k l
    | Sum.inr (Sum.inr 0) :: l => h_4 l
    | Sum.inr (Sum.inr 1) :: l => h_5 l
    | x => h_6 x) =
    h_3 n R k l
-- Mathlib.Order.SuccPred.Basic
Order.succ_le_iff_of_not_isMax : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a b : α}, ¬IsMax a → (Order.succ a ≤ b ↔ a < b)
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
CategoryTheory.ConcreteCategory.ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y : C}
  {f g : X ⟶ Y}, f = g ↔ CategoryTheory.ConcreteCategory.hom f = CategoryTheory.ConcreteCategory.hom g
-- Mathlib.Topology.Homeomorph.Defs
Equiv.toHomeomorphOfContinuousOpen_symm_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ Y)
  (h₁ : Continuous ⇑e) (h₂ : IsOpenMap ⇑e), ⇑(e.toHomeomorphOfContinuousOpen h₁ h₂).symm = ⇑e.symm
-- Mathlib.Order.Fin.Tuple
/-- The space of functions `Fin 2 → α` is order equivalent to `α × α`. See also
`OrderIso.piFinTwoIso`.  -/
OrderIso.finTwoArrowIso : (α : Type u_2) → [inst : Preorder α] → (Fin 2 → α) ≃o α × α
-- Init.Data.List.Basic
/-- Removes the first `n` elements of the list `xs`. Returns the empty list if `n` is greater than the
length of the list.

`O(min n |xs|)`.

Examples:
* `[0, 1, 2, 3, 4].drop 0 = [0, 1, 2, 3, 4]`
* `[0, 1, 2, 3, 4].drop 3 = [3, 4]`
* `[0, 1, 2, 3, 4].drop 6 = []`
 -/
List.drop : {α : Type u} → ℕ → List α → List α
-- Init.Data.Int.Lemmas
Int.instCommutativeHMul : Std.Commutative fun x1 x2 => x1 * x2
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.snd_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.IsProbabilityMeasure μ], (μ.prod ν).snd = ν
-- Mathlib.Topology.NhdsWithin
DenseRange.piMap : ∀ {ι : Type u_5} {X : ι → Type u_6} {Y : ι → Type u_7} [inst : (i : ι) → TopologicalSpace (Y i)]
  {f : (i : ι) → X i → Y i}, (∀ (i : ι), DenseRange (f i)) → DenseRange (Pi.map f)
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.NormalizePattern.ParentKind.genPattern.sizeOf_spec : sizeOf Lean.Meta.Grind.NormalizePattern.ParentKind.genPattern✝ = 1
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.union_insert_right_equiv_union_insert : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {p : (a : α) × β a}, (m₁ ∪ m₂.insert p.fst p.snd).Equiv ((m₁ ∪ m₂).insert p.fst p.snd)
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearEquiv.rTensor_pow : ∀ {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] (f : M ≃ₗ[R] M) (n : ℕ),
  LinearEquiv.rTensor N f ^ n = LinearEquiv.rTensor N (f ^ n)
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.unreachable : Lean.IR.FnBody
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
/-- The vector between two `faceOppositeCentroid` equals `n⁻¹` times the vector between the
corresponding vertices.  -/
Affine.Simplex.faceOppositeCentroid_vsub_faceOppositeCentroid : ∀ {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 j : Fin (n + 1)),
  s.faceOppositeCentroid i -ᵥ s.faceOppositeCentroid j = (↑n)⁻¹ • (s.points j -ᵥ s.points i)
-- Mathlib.LinearAlgebra.Eigenspace.Pi
Module.End.disjoint_iInf_maxGenEigenspace : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (f : ι → Module.End R M) [IsDomain R] [Module.IsTorsionFree R M] {χ₁ χ₂ : ι → R},
  χ₁ ≠ χ₂ → Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (⨅ i, (f i).maxGenEigenspace (χ₂ i))
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.LHom.onBoundedFormula.eq_def : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} (g : L →ᴸ L') (x : ℕ) (x_1 : L.BoundedFormula α x),
  g.onBoundedFormula x_1 =
    match x, x_1 with
    | _k, FirstOrder.Language.BoundedFormula.falsum => FirstOrder.Language.BoundedFormula.falsum
    | _k, FirstOrder.Language.BoundedFormula.equal t₁ t₂ => (g.onTerm t₁).bdEqual (g.onTerm t₂)
    | _k, FirstOrder.Language.BoundedFormula.rel R ts => (g.onRelation R).boundedFormula (g.onTerm ∘ ts)
    | _k, f₁.imp f₂ => (g.onBoundedFormula f₁).imp (g.onBoundedFormula f₂)
    | _k, f.all => (g.onBoundedFormula f).all
-- Mathlib.Topology.Constructions.SumProd
Homeomorph.coe_punitProd : ∀ (X : Type u) [inst : TopologicalSpace X], ⇑(Homeomorph.punitProd X) = Prod.snd
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.map_algebraMap_eq_subst_X : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {S : Type u_5} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (f : MvPowerSeries σ R), (MvPowerSeries.map (algebraMap R S)) f = MvPowerSeries.subst MvPowerSeries.X f
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_insertIfNew_le : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {v : β k}, (m.insertIfNew k v).size ≤ m.size + 1
-- Mathlib.Analysis.InnerProductSpace.Orientation
OrthonormalBasis.toBasis_adjustToOrientation : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {ι : Type u_2} [inst_2 : Fintype ι]
  [inst_3 : DecidableEq ι] (e : OrthonormalBasis ι ℝ E) (x : Orientation ℝ E ι) [inst_4 : Nonempty ι],
  (e.adjustToOrientation x).toBasis = e.toBasis.adjustToOrientation x
-- Std.Sat.AIG.LawfulVecOperator
Std.Sat.AIG.LawfulVecOperator.denote_cast_entry : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {β : Std.Sat.AIG α → ℕ → Type}
  {f : {len : ℕ} → (aig : Std.Sat.AIG α) → β aig len → Std.Sat.AIG.RefVecEntry α len}
  [Std.Sat.AIG.LawfulVecOperator α β fun {len} => f] {len : ℕ} {assign : α → Bool} (entry : Std.Sat.AIG.Entrypoint α)
  {input : β entry.aig len} {h : entry.aig.decls.size ≤ (f entry.aig input).aig.decls.size},
  ⟦assign, { aig := (f entry.aig input).aig, ref := entry.ref.cast h }⟧ = ⟦assign, entry⟧
-- Mathlib.Analysis.Normed.Group.Hom
/-- Subtraction of normed group homs.  -/
NormedAddGroupHom.sub : {V₁ : Type u_2} →
  {V₂ : Type u_3} →
    [inst : SeminormedAddCommGroup V₁] → [inst_1 : SeminormedAddCommGroup V₂] → Sub (NormedAddGroupHom V₁ V₂)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_union_closure_right_eq : ∀ {α : Type u_2} (M : Matroid α) (X Y : Set α), M.closure (X ∪ M.closure Y) = M.closure (X ∪ Y)
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.oddCommuteEquiv_apply : ∀ {n : ℕ} (hn : Odd n) (x : { p // Commute p.1 p.2 }),
  (DihedralGroup.oddCommuteEquiv hn) x =
    match x with
    | ⟨(DihedralGroup.sr i, DihedralGroup.r a), property⟩ => Sum.inl i
    | ⟨(DihedralGroup.r a, DihedralGroup.sr j), property⟩ => Sum.inr (Sum.inl j)
    | ⟨(DihedralGroup.sr i, DihedralGroup.sr j), property⟩ => Sum.inr (Sum.inr (Sum.inl (i + j)))
    | ⟨(DihedralGroup.r i, DihedralGroup.r j), property⟩ => Sum.inr (Sum.inr (Sum.inr (i, j)))