mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.mk.injEq : ∀ (toBddDistLat : BddDistLat) [isFintype : Fintype ↑toBddDistLat.toDistLat] (toBddDistLat_1 : BddDistLat)
  (isFintype_1 : Fintype ↑toBddDistLat_1.toDistLat),
  ({ toBddDistLat := toBddDistLat, isFintype := isFintype } =
      { toBddDistLat := toBddDistLat_1, isFintype := isFintype_1 }) =
    (toBddDistLat = toBddDistLat_1 ∧ isFintype ≍ isFintype_1)
-- Mathlib.Combinatorics.SimpleGraph.IncMatrix
SimpleGraph.incMatrix_apply_eq_one_iff : ∀ {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [inst : MulZeroOneClass R] [inst_1 : DecidableEq α]
  [inst_2 : DecidableRel G.Adj] {a : α} {e : Sym2 α} [Nontrivial R],
  SimpleGraph.incMatrix R G a e = 1 ↔ e ∈ G.incidenceSet a
-- Mathlib.Order.Category.Lat
Lat.hom_id : ∀ {X : Lat}, Lat.Hom.hom (CategoryTheory.CategoryStruct.id X) = LatticeHom.id ↑X
-- Mathlib.NumberTheory.NumberField.Completion.LiesOverInstances
NumberField.LiesOver.continuous_completionMap : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  {v : NumberField.InfinitePlace K} {w : NumberField.InfinitePlace L} [inst_3 : w.LiesOver v],
  Continuous ⇑NumberField.LiesOver.completionMap
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.both : Std.Tactic.BVDecide.LRAT.Internal.Assignment
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instCommSemiringQuotient : {R : Type u_1} → [inst : CommSemiring R] → (c : RingCon R) → CommSemiring c.Quotient
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
/-- The univariate polynomial `Ψ₂Sq` congruent to `ψ₂²`.  -/
WeierstrassCurve.Ψ₂Sq : {R : Type r} → [inst : CommRing R] → WeierstrassCurve R → Polynomial R
-- Mathlib.Analysis.Matrix.Spectrum
Matrix.IsHermitian.eigenvectorUnitary_mulVec : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n]
  (hA : A.IsHermitian) (j : n), (↑hA.eigenvectorUnitary).mulVec (Pi.single j 1) = (hA.eigenvectorBasis j).ofLp
-- Mathlib.CategoryTheory.Presentable.Dense
CategoryTheory.IsFinitelyAccessibleCategory.instIsDenseFullSubcategoryIsFinitelyPresentableι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFinitelyAccessibleCategory C],
  (CategoryTheory.ObjectProperty.isFinitelyPresentable C).ι.IsDense
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Initial.conesEquiv_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.Initial] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  (G : CategoryTheory.Functor D E),
  (CategoryTheory.Functor.Initial.conesEquiv F G).functor = CategoryTheory.Functor.Initial.extendCone
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- Notation for `actionHomRight`, the action of morphism in `C` on `D`.  -/
CategoryTheory.MonoidalCategory.MonoidalLeftAction.«term_⊴ₗ_» : Lean.TrailingParserDescr
-- Lean.Meta.Eqns
/-- A mapping from equational theorem to the declaration it was derived from.   -/
Lean.Meta.EqnsExtState : Type
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_neg : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIcoMod hp a (-b) = p - toIocMod hp (-a) b
-- Mathlib.Order.Hom.WithTopBot
/-- Adjoins a `⊤` to the domain of an `InfHom`.  -/
InfHom.withTop' : {α : Type u_1} →
  {β : Type u_2} →
    [inst : SemilatticeInf α] →
      [inst_1 : SemilatticeInf β] → [inst_2 : OrderTop β] → InfHom α β → InfTopHom (WithTop α) β
-- Mathlib.Probability.ConditionalProbability
ProbabilityTheory.inter_pos_of_cond_ne_zero : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s t : Set Ω},
  MeasurableSet s → μ[t | s] ≠ 0 → 0 < μ (s ∩ t)
-- Mathlib.Algebra.Order.Module.Defs
smul_pos_iff_of_pos_left : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulZeroClass α β]
  [inst_3 : Preorder α] [inst_4 : Preorder β] [PosSMulStrictMono α β] [PosSMulReflectLT α β],
  0 < a → (0 < a • b ↔ 0 < b)
-- Mathlib.Data.List.Sort
/-- **Alias** of the forward direction of `List.sortedLE_map_toDual`. -/
List.SortedLE.map_toDual : ∀ {α : Type u_1} [inst : Preorder α] {l : List α}, (List.map (⇑OrderDual.toDual) l).SortedLE → l.SortedGE
-- Mathlib.CategoryTheory.Equivalence
/-- If `G` and `F ⋙ G` are equivalence of categories, then `F` is also an equivalence.  -/
CategoryTheory.Functor.isEquivalence_of_comp_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [G.IsEquivalence] [(F.comp G).IsEquivalence], F.IsEquivalence
-- Batteries.Data.BinomialHeap.Basic
/-- `O(log n)`. Removes the smallest element from the heap, or `none` if the heap is empty.  -/
Batteries.BinomialHeap.tail? : {α : Type u} → {le : α → α → Bool} → Batteries.BinomialHeap α le → Option (Batteries.BinomialHeap α le)
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.map_apply : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (S : Type u_4)
  [inst_3 : CommSemiring S] {N : Type u_5} [inst_4 : AddCommMonoid N] [inst_5 : Module R N] [inst_6 : Module S N]
  (f : M →ₗ[R] N) [inst_7 : Algebra R S] [inst_8 : IsScalarTower R S N] {p : MvPolynomial (ℕ × M) R},
  (DividedPowerAlgebra.map S f) ↑p = (MvPolynomial.aeval fun nm => DividedPowerAlgebra.dp S nm.1 (f nm.2)) p
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get_eq_get : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [inst_2 : LawfulBEq α],
  (↑m).WF → ∀ {a : α} {h : m.contains a = true}, Std.DHashMap.Internal.Raw₀.Const.get m a h = m.get a h
-- Init.Data.Iterators.Internal.LawfulMonadLiftFunction
Std.Internal.LawfulMonadLiftFunction.mk : ∀ {m : Type u → Type v} {n : Type u → Type w} [inst : Monad m] [inst_1 : Monad n] {lift : ⦃α : Type u⦄ → m α → n α},
  (∀ {α : Type u} (a : α), lift (pure a) = pure a) →
    (∀ {α β : Type u} (ma : m α) (f : α → m β),
        lift (ma >>= f) = do
          let x ← lift ma
          lift (f x)) →
      Std.Internal.LawfulMonadLiftFunction lift
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Injective.comp_factorThru_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J X Y : C} [inst_1 : CategoryTheory.Injective J]
  (g : X ⟶ J) (f : X ⟶ Y) [inst_2 : CategoryTheory.Mono f] {Z : C} (h : J ⟶ Z),
  CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Injective.factorThru g f) h) =
    CategoryTheory.CategoryStruct.comp g h
-- Mathlib.Order.Sublocale
Sublocale.top_mem : ∀ {X : Type u_1} [inst : Order.Frame X] {S : Sublocale X}, ⊤ ∈ S
-- Init.Data.Iterators.Combinators.Monadic.Append
Std.Iterators.Types.Append.rel_of_fst : ∀ {α₁ α₂ : Type w} {m : Type w → Type w'} {β : Type w} [inst : Monad m] [inst_1 : Std.Iterator α₁ m β]
  [inst_2 : Std.Iterator α₂ m β] [inst_3 : Std.Iterators.Finite α₁ m] [inst_4 : Std.Iterators.Finite α₂ m]
  {it₁ it₁' : Std.IterM m β} {it₂ : Std.IterM m β},
  it₁'.finitelyManySteps.Rel it₁.finitelyManySteps →
    Std.Iterators.Types.Append.Rel α₁ α₂ m β (it₁'.append it₂) (it₁.append it₂)
-- Mathlib.AlgebraicGeometry.EllipticCurve.LFunction
/-- The L-function of a Weierstrass curve `W` over a number field `K` as a formal Dirichlet series.

For each prime ideal `p` of the ring of integers of `K` with norm `‖p‖` residue field `κ_p`,
we define the local polynomial `fₚ(T)` as:
* `fₚ = 1 - aₚ T + ‖p‖ T ^ 2` where `aₚ = ‖p‖ + 1 - |W(κ_p)|` if `W` has good reduction at `p`,
* `fₚ = 1 - T` if `W` has split multiplicative reduction at `p`,
* `fₚ = 1 + T` if `W` has nonsplit multiplicative reduction at `p`,
* `fₚ = 1` if `W` has additive reduction at `p`.
Then the L-function of `W` is the formal Dirichlet series defined as the product of `1 / fₚ(‖p‖⁻ˢ)`
as `p` ranges over all prime ideals of the ring of integers of `K`.
 -/
WeierstrassCurve.LFunction : {K : Type u_1} → [inst : Field K] → [NumberField K] → WeierstrassCurve K → ArithmeticFunction ℤ
-- Mathlib.Order.RelClasses
/-- Set notation form of `lt_of_le_not_ge` -/
ssubset_of_subset_not_superset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b : α}, a ⊆ b → ¬b ⊆ a → a ⊂ b
-- Mathlib.Analysis.Convex.Radon
/-- Corner case for `helly_theorem'`.  -/
_private.Mathlib.Analysis.Convex.Radon.0.Convex.helly_theorem_corner : ∀ {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {F : ι → Set E} {s : Finset ι},
  s.card ≤ Module.finrank 𝕜 E + 1 →
    (∀ I ⊆ s, I.card ≤ Module.finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) → (⋂ i ∈ s, F i).Nonempty
-- Lean.Data.Json.FromToJson.Basic
Lean.Float.fromJson? : Lean.Json → Except String Float
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.coconePointsIsoOfEquivalence.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
  {s : CategoryTheory.Limits.Cocone F} {G : CategoryTheory.Functor K C} {t : CategoryTheory.Limits.Cocone G}
  (P : CategoryTheory.Limits.IsColimit s) (Q : CategoryTheory.Limits.IsColimit t) (e : J ≌ K)
  (w : e.functor.comp G ≅ F),
  P.coconePointsIsoOfEquivalence Q e w =
    { hom := P.desc ((CategoryTheory.Limits.Cocone.equivalenceOfReindexing e w).functor.obj t),
      inv :=
        Q.desc
          ((CategoryTheory.Limits.Cocone.equivalenceOfReindexing e.symm
                  ((e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G)).functor.obj
            s),
      hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.δToCycles.congr_simp : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ : ℤ)
  (hn₁ : n₀ + 1 = n₁), X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁ = X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.comap_top : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R →+* S),
  Subsemiring.comap f ⊤ = ⊤
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.ext_of_generateFrom_of_cover : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {S T : Set (Set α)},
  m0 = MeasurableSpace.generateFrom S →
    T.Countable →
      IsPiSystem S →
        ⋃₀ T = Set.univ → (∀ t ∈ T, μ t ≠ ⊤) → (∀ t ∈ T, ∀ s ∈ S, μ (s ∩ t) = ν (s ∩ t)) → (∀ t ∈ T, μ t = ν t) → μ = ν
-- Mathlib.Geometry.Euclidean.Projection
/-- Adding a vector to a point in the given subspace, then taking the
orthogonal projection, produces the original point if the vector was
in the orthogonal direction.  -/
EuclideanGeometry.orthogonalProjection_vadd_eq_self : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {s : AffineSubspace 𝕜 P}
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] {p : P} (hp : p ∈ s) {v : V},
  v ∈ s.directionᗮ → (EuclideanGeometry.orthogonalProjection s) (v +ᵥ p) = ⟨p, hp⟩
-- Init.Data.Iterators.Combinators.FilterMap
/-- If `it` is an iterator, then `it.filterMap f` is another iterator that applies a function `f` to all
values emitted by `it`. `f` is expected to return an `Option`. If it returns `none`, then nothing is
emitted; if it returns `some x`, then `x` is emitted.

In situations where `f` is monadic, use `filterMapM` instead.

**Marble diagram:**

```text
it               ---a --b--c --d-e--⊥
it.filterMap     ---a'-----c'-------⊥
```

(given that `f a = some a'`, `f c = c'` and `f b = f d = d e = none`)

**Termination properties:**

* `Finite` instance: only if `it` is finite
* `Productive` instance: only if `it` is finite`

For certain mapping functions `f`, the resulting iterator will be productive even though
no `Productive` instance is provided. For example, if `f` never returns `none`, then
this combinator will preserve productiveness. In such situations, the missing instance needs to
be proved manually.

**Performance:**

For each value emitted by the base iterator `it`, this combinator calls `f` and matches on the
returned `Option` value.
 -/
Std.Iter.filterMap : {α β γ : Type w} → [Std.Iterator α Id β] → (f : β → Option γ) → Std.Iter β → Std.Iter γ
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousLinearMap.norm_map_removeNth_le : ∀ {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {i : Fin (n + 1)}
  (f : Ei i →L[𝕜] Ei (i.succAbove j) [×n]→L[𝕜] G) (m : (i : Fin n.succ) → Ei i),
  ‖(f (m i)) (i.removeNth m)‖ ≤ ‖f‖ * ∏ j, ‖m j‖
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.Context.sharedExprs : Lean.Meta.Sym.Context → Lean.Meta.Sym.SharedExprs
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.fundamentalFrontier_union_fundamentalInterior : ∀ (G : Type u_1) {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] (s : Set α),
  MeasureTheory.fundamentalFrontier G s ∪ MeasureTheory.fundamentalInterior G s = s
-- Mathlib.Probability.Distributions.Beta
/-- The probability density function of the beta distribution with shape parameters `α` and `β`.
Returns `(1 / beta α β) * x ^ (α - 1) * (1 - x) ^ (β - 1)`
when `0 < x < 1` and `0` otherwise.  -/
ProbabilityTheory.betaPDFReal : ℝ → ℝ → ℝ → ℝ
-- Mathlib.Analysis.Fourier.ZMod
ZMod.dft_smul_const : ∀ {N : ℕ} [inst : NeZero N] {E : Type u_1} [inst_1 : AddCommGroup E] [inst_2 : Module ℂ E] {R : Type u_2}
  [inst_3 : Ring R] [inst_4 : Module ℂ R] [inst_5 : Module R E] [IsScalarTower ℂ R E] (Φ : ZMod N → R) (e : E),
  (ZMod.dft fun j => Φ j • e) = fun k => ZMod.dft Φ k • e
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.rotateL.match_1.eq_2 : ∀ {α : Type u_1} (motive : Ordnode α → α → Ordnode α → Sort u_2) (l : Ordnode α) (x : α)
  (h_1 :
    (l : Ordnode α) →
      (x : α) → (size : ℕ) → (m : Ordnode α) → (y : α) → (r : Ordnode α) → motive l x (Ordnode.node size m y r))
  (h_2 : (l : Ordnode α) → (x : α) → motive l x Ordnode.nil),
  (match l, x, Ordnode.nil with
    | l, x, Ordnode.node size m y r => h_1 l x size m y r
    | l, x, Ordnode.nil => h_2 l x) =
    h_2 l x
-- Std.Data.DTreeMap.Internal.Operations
/-- Returns the tree consisting of the mappings `(k, (f k v).get)` where `(k, v)` was a mapping in
the original tree and `(f k v).isSome`.
 -/
Std.DTreeMap.Internal.Impl.filterMap : {α : Type u} →
  {β : α → Type v} →
    {γ : α → Type w} →
      [Ord α] →
        ((a : α) → β a → Option (γ a)) →
          (t : Std.DTreeMap.Internal.Impl α β) → t.Balanced → Std.DTreeMap.Internal.Impl.BalancedTree α γ
-- Mathlib.Tactic.ClickSuggestions.Rewrite
/-- The lemma  -/
Mathlib.Tactic.ClickSuggestions.RwLemma.name : Mathlib.Tactic.ClickSuggestions.RwLemma → Mathlib.Tactic.ClickSuggestions.Premise
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.integral_average_sub : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure α} {f : α → E} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Integrable f μ → ∫ (x : α), ⨍ (a : α), f a ∂μ - f x ∂μ = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPushout.isIso_inl_of_isIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P},
  CategoryTheory.IsPushout f g inl inr →
    autoParam (CategoryTheory.IsIso g) CategoryTheory.IsPushout.isIso_inl_of_isIso._auto_1 → CategoryTheory.IsIso inl
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.parseNum : ℕ → Std.Internal.Parsec.String.Parser ℕ
-- Mathlib.Algebra.Order.Monovary
AntivaryOn.pow_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : CommGroup β] [inst_2 : LinearOrder β]
  [IsOrderedMonoid β] {s : Set ι} {f : ι → α} {g : ι → β}, AntivaryOn f g s → ∀ (n : ℕ), AntivaryOn f (g ^ n) s
-- Mathlib.Order.RelClasses
instAsymmLt : ∀ {α : Type u} [inst : Preorder α], Std.Asymm fun x1 x2 => x1 < x2
-- Mathlib.Data.Nat.Log
Nat.clog_one_right : ∀ (b : ℕ), Nat.clog b 1 = 0
-- Mathlib.Order.Heyting.Basic
Disjoint.disjoint_sdiff_right : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, Disjoint a b → Disjoint a (b \ c)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- The union of two subgraphs.  -/
SimpleGraph.Subgraph.instMax : {V : Type u} → {G : SimpleGraph V} → Max G.Subgraph
-- Mathlib.Topology.Order.MonotoneConvergence
iInf_eq_iInf_subseq_of_monotone : ∀ {ι₁ : Type u_3} {ι₂ : Type u_4} {α : Type u_5} [inst : Preorder ι₂] [inst_1 : CompleteLattice α] {l : Filter ι₁}
  [l.NeBot] {f : ι₂ → α} {φ : ι₁ → ι₂}, Monotone f → Filter.Tendsto φ l Filter.atBot → ⨅ i, f i = ⨅ i, f (φ i)
-- Lean.Meta.Tactic.Grind.CasesMatch
/-- Annotates the `match`-expression conditions in the alternatives in the given
`match` splitter type.
 -/
_private.Lean.Meta.Tactic.Grind.CasesMatch.0.Lean.Meta.Grind.addMatchCondsToSplitter : Lean.Expr → ℕ → Lean.Expr
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.restrictScalars_injective : ∀ (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Monoid R] [inst_1 : Monoid S] [inst_2 : Star A]
  [inst_3 : Star B] [inst_4 : NonUnitalNonAssocSemiring A] [inst_5 : NonUnitalNonAssocSemiring B]
  [inst_6 : MulAction R S] [inst_7 : DistribMulAction S A] [inst_8 : DistribMulAction S B]
  [inst_9 : DistribMulAction R A] [inst_10 : DistribMulAction R B] [inst_11 : IsScalarTower R S A]
  [inst_12 : IsScalarTower R S B], Function.Injective (NonUnitalStarAlgHom.restrictScalars R)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- A non-commutative version of `SkewMonoidAlgebra.lift`: given an additive homomorphism
`f : k →+ R` and a homomorphism `g : G → R`, returns the additive homomorphism from
`SkewMonoidAlgebra k G` such that `liftNC f g (single a b) = f b * g a`.

If `k` is a semiring and `f` is a ring homomorphism and for all `x : R`, `y : G` the equality
`(f (y • x)) * g y = (g y) * (f x))` holds, then the result is a ring homomorphism (see
`SkewMonoidAlgebra.liftNCRingHom`).

If `R` is a `k`-algebra and `f = algebraMap k R`, then the result is an algebra homomorphism called
`SkewMonoidAlgebra.lift`.  -/
SkewMonoidAlgebra.liftNC : {k : Type u_1} →
  {G : Type u_2} →
    [inst : AddCommMonoid k] →
      {R : Type u_5} → [inst_1 : NonUnitalNonAssocSemiring R] → (k →+ R) → (G → R) → SkewMonoidAlgebra k G →+ R
-- Mathlib.RingTheory.Grassmannian
/-- `G(k, M; R)` is the `k`ᵗʰ Grassmannian of the `R`-module `M`. It is defined to be the set of
submodules of `M` whose quotient is locally free of rank `k`. Note that there is another convention
in literature where instead the submodule is required to have rank `k`. See the module docstring
of `RingTheory.Grassmannian`.  -/
Module.Grassmannian.«termG(_,_;_)» : Lean.ParserDescr
-- Batteries.Data.Random.MersenneTwister
/-- Tempering step for Mersenne Twister.  -/
_private.Batteries.Data.Random.MersenneTwister.0.Batteries.Random.MersenneTwister.State.next.temper : {cfg : Batteries.Random.MersenneTwister.Config} → BitVec cfg.wordSize → BitVec cfg.wordSize
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.RegularMono.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} [inst_1 : SizeOf C] (Z : C)
  (left right : Y ⟶ Z)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp f left = CategoryTheory.CategoryStruct.comp f right)
      CategoryTheory.RegularMono.w._autoParam)
  (isLimit : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f w)),
  sizeOf { Z := Z, left := left, right := right, w := w, isLimit := isLimit } =
    1 + sizeOf Z + sizeOf left + sizeOf right + sizeOf w + sizeOf isLimit
-- Mathlib.Topology.Category.LightProfinite.Basic
LightProfinite.instSecondCountableTopologyCarrierToTopAndTotallyDisconnectedSpace : ∀ {X : LightProfinite}, SecondCountableTopology ↑X.toTop
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- Notation for the `Ω₀` in an arbitrary choice of a subobject classifier  -/
CategoryTheory.HasSubobjectClassifier.Ω₀ : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.HasSubobjectClassifier C] → C
-- Mathlib.Algebra.Free
/-- The length of an element of a free magma is positive.  -/
FreeMagma.length_pos : ∀ {α : Type u} (x : FreeMagma α), 0 < x.length
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instCommMonoid.eq_1 : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : CommMonoid M],
  Filter.Germ.instCommMonoid = { toMonoid := Filter.Germ.instMonoid, mul_comm := ⋯ }
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cocone.toCostructuredArrowCompToOverCompForget_hom_app : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) (X : J),
  c.toCostructuredArrowCompToOverCompForget.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeftIso_functor_obj_hom : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {L₁ L₂ : CategoryTheory.Functor A T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : L₁ ≅ L₂) (X : CategoryTheory.MorphismProperty.Comma L₁ R P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapLeftIso R e).functor.obj X).hom =
    CategoryTheory.CategoryStruct.comp (e.inv.app X.left) X.hom
-- Mathlib.FieldTheory.CardinalEmb
Field.Emb.Cardinal.strictMono_filtration : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [rank_inf : Fact (Cardinal.aleph0 ≤ Module.rank F E)] [inst_3 : Algebra.IsAlgebraic F E],
  StrictMono fun x =>
    IntermediateField.adjoin F
      (⇑(Field.Emb.Cardinal.wellOrderedBasis F E) ∘ Field.Emb.Cardinal.leastExt F E '' Set.Iio x)
-- Mathlib.Algebra.IsPrimePow
IsPrimePow.one_lt : ∀ {n : ℕ}, IsPrimePow n → 1 < n
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.removeFactor.eq_1 : ∀ {K : Type v} [inst : Field K] (f : Polynomial K),
  f.removeFactor = Polynomial.map (AdjoinRoot.of f.factor) f /ₘ (Polynomial.X - Polynomial.C (AdjoinRoot.root f.factor))
-- Aesop.Stats.Extension
Aesop.StatsExtensionEntry.fileName : Aesop.StatsExtensionEntry → String
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- If a coequalizer of `f` and `g` exists, we can access the corresponding projection by
saying `coequalizer.π f g`.  -/
CategoryTheory.Limits.coequalizer.π : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (f g : X ⟶ Y) → [inst_1 : CategoryTheory.Limits.HasCoequalizer f g] → Y ⟶ CategoryTheory.Limits.coequalizer f g
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.instTop_1 : {α : Type u_1} → [inst : CompleteLattice α] → Top (CompleteSublattice α)