mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
MeasureTheory.condLExp_add_le : ∀ {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} (X Y : Ω → ENNReal),
  P⁻[X | mΩ] + P⁻[Y | mΩ] ≤ᵐ[P] P⁻[X + Y | mΩ]
-- Mathlib.Dynamics.BirkhoffSum.Average
/-- The average value of `g` on the first `n` points of the orbit of `x` under `f`,
i.e. the Birkhoff sum `∑ k ∈ Finset.range n, g (f^[k] x)` divided by `n`.

This average appears in many ergodic theorems
which say that `(birkhoffAverage R f g · x)`
converges to the "space average" `⨍ x, g x ∂μ` as `n → ∞`.

We use an auxiliary `[DivisionSemiring R]` to define division by `n`.
However, the definition does not depend on the choice of `R`,
see `birkhoffAverage_congr_ring`.  -/
birkhoffAverage : (R : Type u_1) →
  {α : Type u_2} →
    {M : Type u_3} →
      [inst : DivisionSemiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → (α → α) → (α → M) → ℕ → α → M
-- Mathlib.Algebra.QuadraticDiscriminant
discrim_eq_sq_of_quadratic_eq_zero : ∀ {R : Type u_1} [inst : CommRing R] {a b c x : R}, a * (x * x) + b * x + c = 0 → discrim a b c = (2 * a * x + b) ^ 2
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.mk.sizeOf_spec : ∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : SizeOf Γ] [inst_3 : SizeOf R]
  (coeff : Γ → R) (isPWO_support' : (Function.support coeff).IsPWO),
  sizeOf { coeff := coeff, isPWO_support' := isPWO_support' } = 1
-- Mathlib.NumberTheory.Divisors
Nat.divisorsAntidiagonal_one : Nat.divisorsAntidiagonal 1 = {(1, 1)}
-- Mathlib.Analysis.Normed.Group.Constructions
OrderDual.normedGroup : {E : Type u_2} → [NormedGroup E] → NormedGroup Eᵒᵈ
-- Mathlib.Data.Sym.Sym2
Sym2.isDiag_map : ∀ {α : Type u_1} {β : Type u_2} {z : Sym2 α} {f : α → β}, Function.Injective f → ((Sym2.map f z).IsDiag ↔ z.IsDiag)
-- Mathlib.LinearAlgebra.Determinant
/-- The determinant of a basis constructed by `isUnitSMul` is the product of the given units.  -/
Module.Basis.det_isUnitSMul : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_4}
  [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] (e : Module.Basis ι R M) {w : ι → R} (hw : ∀ (i : ι), IsUnit (w i)),
  e.det ⇑(e.isUnitSMul hw) = ∏ i, w i
-- Plausible.Testable
Plausible.Configuration.mk.sizeOf_spec : ∀ (numInst maxSize numRetries : ℕ) (traceDiscarded traceSuccesses traceShrink traceShrinkCandidates : Bool)
  (randomSeed : Option ℕ) (quiet sorryIfNoTestable : Bool),
  sizeOf
      { numInst := numInst, maxSize := maxSize, numRetries := numRetries, traceDiscarded := traceDiscarded,
        traceSuccesses := traceSuccesses, traceShrink := traceShrink, traceShrinkCandidates := traceShrinkCandidates,
        randomSeed := randomSeed, quiet := quiet, sorryIfNoTestable := sorryIfNoTestable } =
    1 + sizeOf numInst + sizeOf maxSize + sizeOf numRetries + sizeOf traceDiscarded + sizeOf traceSuccesses +
              sizeOf traceShrink +
            sizeOf traceShrinkCandidates +
          sizeOf randomSeed +
        sizeOf quiet +
      sizeOf sorryIfNoTestable
-- Mathlib.GroupTheory.Index
AddSubgroup.index_map_dvd : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (H : AddSubgroup G) {f : G →+ G'},
  Function.Surjective ⇑f → (AddSubgroup.map f H).index ∣ H.index
-- Mathlib.GroupTheory.OrderOfElement
infinite_not_isOfFinOrder : ∀ {G : Type u_1} [inst : LeftCancelMonoid G] {x : G}, ¬IsOfFinOrder x → {y | ¬IsOfFinOrder y}.Infinite
-- Mathlib.Order.KrullDimension
/-- Another version when the `OrderHom` is unbundled  -/
Order.krullDim_le_of_krullDim_preimage_le' : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : PartialOrder β] {m : ℕ} (f : α → β),
  Monotone f → (∀ (x : β), Order.krullDim ↑(f ⁻¹' {x}) ≤ ↑m) → Order.krullDim α ≤ (↑m + 1) * Order.krullDim β + ↑m
-- Mathlib.Algebra.Divisibility.Basic
exists_dvd_and_dvd_of_dvd_mul : ∀ {α : Type u_1} [inst : Semigroup α] [DecompositionMonoid α] {b c a : α},
  a ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Copy.ofLE.congr_simp : ∀ {V : Type u_1} (G₁ G₂ : SimpleGraph V) (h : G₁ ≤ G₂), SimpleGraph.Copy.ofLE G₁ G₂ h = SimpleGraph.Copy.ofLE G₁ G₂ h
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
LinearIndepOn.id_image : ∀ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M], LinearIndepOn R v s → LinearIndepOn R id (v '' s)
-- Mathlib.Tactic.CrossRefAttribute
/-- The main parser for Wikidata identifiers: it accepts `Q` followed by one or more digits.  -/
Mathlib.CrossRef.wikidataIdParser : Lean.Parser.Parser
-- Batteries.Lean.AttributeExtra
/-- Does declaration `decl` have the tag `attr`?  -/
Lean.TagAttributeExtra.hasTag : Lean.TagAttributeExtra → Lean.Environment → Lean.Name → Bool
-- Mathlib.CategoryTheory.ObjectProperty.Opposite
CategoryTheory.ObjectProperty.op_injective_iff : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {P Q : CategoryTheory.ObjectProperty C},
  P.op = Q.op ↔ P = Q
-- Mathlib.RingTheory.Derivation.Lie
Derivation.bracket_eq_fun : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A] (X : Derivation R A A)
  (a : A), ⁅X, a⁆ = X a
-- Mathlib.Combinatorics.Graph.Basic
Graph.edgeSet_eq_setOfPred_exists_isLink : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β}, G.edgeSet = {e | ∃ x y, G.IsLink e x y}
-- Mathlib.Order.Filter.SmallSets
Filter.smallSets_principal : ∀ {α : Type u_1} (s : Set α), (Filter.principal s).smallSets = Filter.principal (𝒫 s)
-- Mathlib.Tactic.CategoryTheory.MonoidalComp
CategoryTheory.MonoidalCoherence.assoc' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (W X Y Z : C) →
        [CategoryTheory.MonoidalCoherence W
              (CategoryTheory.MonoidalCategoryStruct.tensorObj X
                (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))] →
          CategoryTheory.MonoidalCoherence W
            (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- Conversion to normal form at `x` changes the value only at x.  -/
MeromorphicAt.eqOn_compl_singleton_toMeromorphicNFAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜}, MeromorphicAt f x → Set.EqOn f (toMeromorphicNFAt f x) {x}ᶜ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.inl_isoPushout_inv_assoc : ∀ {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} (h : CategoryTheory.IsPushout f g inl inr) [inst_1 : CategoryTheory.Limits.HasPushout f g] {Z_1 : C}
  (h_1 : P ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g)
      (CategoryTheory.CategoryStruct.comp h.isoPushout.inv h_1) =
    CategoryTheory.CategoryStruct.comp inl h_1
-- Mathlib.NumberTheory.FunctionField
/-- **Alias** of `RatFunc.InftyValuation.map_zero'`. -/
FunctionField.InftyValuation.map_zero' : ∀ (F : Type u_1) [inst : Field F] [inst_1 : DecidableEq (RatFunc F)], RatFunc.inftyValuationDef F 0 = 0
-- Mathlib.Analysis.Seminorm
/-- Composition of a seminorm with a linear map is a seminorm.  -/
Seminorm.comp : {𝕜 : Type u_3} →
  {𝕜₂ : Type u_4} →
    {E : Type u_7} →
      {E₂ : Type u_8} →
        [inst : SeminormedRing 𝕜] →
          [inst_1 : SeminormedRing 𝕜₂] →
            {σ₁₂ : 𝕜 →+* 𝕜₂} →
              [RingHomIsometric σ₁₂] →
                [inst_3 : AddCommGroup E] →
                  [inst_4 : AddCommGroup E₂] →
                    [inst_5 : Module 𝕜 E] → [inst_6 : Module 𝕜₂ E₂] → Seminorm 𝕜₂ E₂ → (E →ₛₗ[σ₁₂] E₂) → Seminorm 𝕜 E
-- Mathlib.Topology.Constructible
Topology.IsConstructible.iInter : ∀ {ι : Sort u_1} {X : Type u_2} [inst : TopologicalSpace X] [Finite ι] {f : ι → Set X},
  (∀ (i : ι), Topology.IsConstructible (f i)) → Topology.IsConstructible (⋂ i, f i)
-- Init.Data.List.Nat.Modify
List.getElem_modifyHead_zero : ∀ {α : Type u_1} {l : List α} {f : α → α} {h : 0 < (List.modifyHead f l).length}, (List.modifyHead f l)[0] = f l[0]
-- Mathlib.Data.Sign.Defs
sign_ne_zero : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : LinearOrder α] {a : α}, SignType.sign a ≠ 0 ↔ a ≠ 0
-- LeanSearchClient.Syntax
/-- Search [LeanStateSearch](https://premise-search.com) from within Lean.
Your current main goal is sent as query. The revision to search can be set
using the `statesearch.revision` option. The number of results can be set
using the `statesearch.queries` option.

Hint: If you want to modify the query, you need to use the web interface.

```lean
set_option statesearch.queries 1
set_option statesearch.revision "v4.16.0"

example : 0 ≤ 1 := by
  #statesearch
  sorry
```

You can modify the LeanStateSearch URL by setting the `LEANSEARCHCLIENT_LEANSTATESEARCH_API_URL` environment variable.
 -/
LeanSearchClient.statesearch_search_tactic : Lean.ParserDescr
-- Std.Time.DateTime
/-- Add `Hour.Offset` to a `DateTime`.
 -/
Std.Time.DateTime.addHours : Std.Time.DateTime → Std.Time.Hour.Offset → Std.Time.DateTime
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
IsCompactOperator.smul_iff₀ : ∀ {M₁ : Type u_3} {M₂ : Type u_4} [inst : TopologicalSpace M₁] [inst_1 : AddCommMonoid M₁]
  [inst_2 : TopologicalSpace M₂] [inst_3 : AddCommMonoid M₂] {S : Type u_6} [inst_4 : GroupWithZero S]
  [inst_5 : DistribMulAction S M₂] [ContinuousConstSMul S M₂] {f : M₁ → M₂} {c : S},
  c ≠ 0 → (IsCompactOperator (c • f) ↔ IsCompactOperator f)
-- Lean.Elab.PreDefinition.Basic
Lean.Elab.cleanup.letToHave : Lean.Option Bool
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.noncompactSpace_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α], NoncompactSpace (TopologicalSpace.NonemptyCompacts α) ↔ NoncompactSpace α
-- Mathlib.Algebra.Order.Group.Abs
abs_eq_self : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] {a : G}, |a| = a ↔ 0 ≤ a
-- Batteries.Data.Array.Pairwise
Array.pairwise_push : ∀ {α : Type u_1} {a : α} {R : α → α → Prop} {as : Array α},
  Array.Pairwise R (as.push a) ↔ Array.Pairwise R as ∧ ∀ x ∈ as, R x a
-- Mathlib.Data.Nat.Init
Nat.leRecOn_succ_left : ∀ {C : ℕ → Sort u_1} {n m : ℕ} {next : {k : ℕ} → C k → C (k + 1)} (x : C n) (h1 : n ≤ m) (h2 : n + 1 ≤ m),
  Nat.leRecOn h2 (fun {k} => next) (next x) = Nat.leRecOn h1 (fun {k} => next) x
-- Init.Data.Int.Gcd
Int.gcd_dvd_gcd_mul_left_right : ∀ (a b c : ℤ), a.gcd b ∣ a.gcd (c * b)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
IsTopologicalAddGroup.tendstoLocallyUniformly_iff : ∀ {ι : Type u_1} {α : Type u_2} {G : Type u_3} [inst : AddGroup G] [u : UniformSpace G]
  [inst_1 : IsTopologicalAddGroup G] [inst_2 : TopologicalSpace α] (F : ι → α → G) (f : α → G) (p : Filter ι),
  IsTopologicalAddGroup.rightUniformSpace G = u →
    (TendstoLocallyUniformly F f p ↔
      ∀ u_1 ∈ nhds 0, ∀ (x : α), ∃ t ∈ nhds x, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a - f a ∈ u_1)
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_mul : ∀ {S : Type v} {F : Type u_1} [inst : CommSemiring S] {R : Type u_2} [inst_1 : Semiring R] [inst_2 : FunLike F R S]
  [RingHomClass F R S] (f : F) (I J : Ideal R), Ideal.map f (I * J) = Ideal.map f I * Ideal.map f J
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
/-- Given a morphism `f : X ⟶ Y` in a model category,
this structure contains the data of a factorization `i ≫ p = f`
with `p` a fibration, `i` a trivial cofibration which
has a retraction `r` that is a fibration.
That this structure is nonempty when `X`
and `Y` are fibrant is Ken Brown's factorization lemma.  -/
HomotopicalAlgebra.FibrantBrownFactorization : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [HomotopicalAlgebra.ModelCategory C] → {X Y : C} → (X ⟶ Y) → Type (max u_1 v_1)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.instFullTopCommaForget : ∀ {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]
  (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (P : CategoryTheory.MorphismProperty T),
  (CategoryTheory.MorphismProperty.Comma.forget L R P ⊤ ⊤).Full
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- The orthogonal projection onto `Kᗮ` of an element of `K` is zero.  -/
Submodule.orthogonalProjectionOnto_orthogonal_apply_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : Kᗮ.HasOrthogonalProjection] {v : E}, v ∈ K → Kᗮ.orthogonalProjectionOnto v = 0
-- Mathlib.ModelTheory.Bundled
FirstOrder.Language.Theory.ModelType.rightStructure : {L : FirstOrder.Language} → {L' : FirstOrder.Language} → {T : (L.sum L').Theory} → (M : T.ModelType) → L'.Structure ↑M
-- Mathlib.Algebra.Ring.Defs
NonUnitalNonAssocCommRing.toNonUnitalNonAssocCommSemiring : {α : Type u} → [self : NonUnitalNonAssocCommRing α] → NonUnitalNonAssocCommSemiring α
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get_eq_of_equiv : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β)
  [inst_2 : LawfulBEq α] (h₁ : (↑m₁).WF) (h₂ : (↑m₂).WF) (h : (↑m₁).Equiv ↑m₂) {k : α} (h' : m₁.contains k = true),
  m₁.get k h' = m₂.get k ⋯
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
ContinuousMap.toNNReal_mul_add_neg_mul_add_mul_neg_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] (f g : C(X, ℝ)),
  (f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal =
    (-(f * g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).toNNReal
-- Lean.ParserCompiler.Attribute
Lean.ParserCompiler.CombinatorAttribute.mk.sizeOf_spec : ∀ (impl : Lean.AttributeImpl)
  (ext : Lean.SimplePersistentEnvExtension (Lean.Name × Lean.Name) (Lean.NameMap Lean.Name)),
  sizeOf { impl := impl, ext := ext } = 1 + sizeOf impl + sizeOf ext
-- Mathlib.Algebra.Group.TypeTags.Basic
ofAdd_zero : ∀ {α : Type u} [inst : Zero α], Multiplicative.ofAdd 0 = 1
-- Lean.Meta.Tactic.Grind.EMatchTheoremPtr
Lean.Meta.Grind.EMatchTheoremPtr.mk.sizeOf_spec : ∀ (thm : Lean.Meta.Grind.EMatchTheorem), sizeOf { thm := thm } = 1 + sizeOf thm
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionEqualizerProducts.piInters.isoOfIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  {F : TopCat.Presheaf C X} {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) {G : TopCat.Presheaf C X} (α : F ≅ G),
  TopCat.Presheaf.SheafConditionEqualizerProducts.piInters.isoOfIso U α =
    CategoryTheory.Limits.Pi.mapIso fun x => α.app (Opposite.op (U x.1 ⊓ U x.2))
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.δ₀Iter_one : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) (n : ℕ),
  X.δ₀Iter 1 ⋯ = X.δ 0
-- Mathlib.Data.Finsupp.Lex
Finsupp.instLTLex : {α : Type u_1} → {N : Type u_2} → [inst : Zero N] → [LT α] → [LT N] → LT (Lex (α →₀ N))
-- Mathlib.Algebra.Group.Action.Pretransitive
AddAction.IsPretransitive.of_vaddAssocClass : ∀ (M : Type u_5) {N : Type u_6} {α : Type u_7} [inst : AddMonoid N] [inst_1 : VAdd M N] [inst_2 : AddAction N α]
  [inst_3 : VAdd M α] [VAddAssocClass M N α] [AddAction.IsPretransitive M α], AddAction.IsPretransitive N α
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- The definition of the "one" in the colimit is independent of the chosen object of `J`.
In particular, this lemma allows us to "unfold" the definition of `colimit_one` at a custom chosen
object `j`.
 -/
MonCat.FilteredColimits.colimit_one_eq : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat)
  [inst_1 : CategoryTheory.IsFiltered J] (j : J), 1 = MonCat.FilteredColimits.M.mk F ⟨j, 1⟩
-- Lean.Elab.MutualInductive
Lean.Elab.Command.instInhabitedInductiveElabStep1.default : Lean.Elab.Command.InductiveElabStep1
-- Aesop.Stats.Extension
Aesop.StatsExtensionEntry.mk.injEq : ∀ (aesopStx : Lean.Syntax) (fileName : String) (position? : Option Lean.Position) (stats : Aesop.Stats)
  (aesopStx_1 : Lean.Syntax) (fileName_1 : String) (position?_1 : Option Lean.Position) (stats_1 : Aesop.Stats),
  ({ aesopStx := aesopStx, fileName := fileName, position? := position?, stats := stats } =
      { aesopStx := aesopStx_1, fileName := fileName_1, position? := position?_1, stats := stats_1 }) =
    (aesopStx = aesopStx_1 ∧ fileName = fileName_1 ∧ position? = position?_1 ∧ stats = stats_1)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.isGLB_inf_id : ∀ {α : Type u_2} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {s : Finset α}, IsGLB (↑s) (s.inf id)
-- Batteries.Data.Fin.Coding
Fin.decodeQuotient.eq_1 : ∀ {n : ℕ} (s : Setoid (Fin n)) [inst : DecidableRel ⇑s] (i : Fin (Fin.countP fun i => decide (Fin.getRepr s i = i))),
  Fin.decodeQuotient s i = ⟦↑(Fin.decodeSubtype (fun x => Fin.getRepr s x = x) i)⟧
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
SheafOfModules.GeneratingSections.map_π_eq : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₁} [inst_3 : CategoryTheory.Category.{v₁, u₁} C']
  {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat}
  [inst_4 : CategoryTheory.HasSheafify J' AddCommGrpCat] [inst_5 : J'.WEqualsLocallyBijective AddCommGrpCat]
  {M : SheafOfModules R} (G : M.GeneratingSections) (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S))
  [inst_6 :
    CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u', max u u₁, max (max (u + 1) u') v',
        max (max (u + 1) u₁) v₁}
      F]
  (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)),
  (G.map F η).π = CategoryTheory.CategoryStruct.comp (SheafOfModules.mapFreeIso F G.I η).hom (F.map G.π)
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.instReflectsLimitsOfShapeDiscreteOfReflectsFiniteProductsOfFinite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsFiniteProducts F] (J : Type u) [Finite J],
  CategoryTheory.Limits.ReflectsLimitsOfShape (CategoryTheory.Discrete J) F
-- Mathlib.Topology.Spectral.Hom
/-- Composition of `SpectralMap`s as a `SpectralMap`.  -/
SpectralMap.comp : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : TopologicalSpace α] →
        [inst_1 : TopologicalSpace β] →
          [inst_2 : TopologicalSpace γ] → SpectralMap β γ → SpectralMap α β → SpectralMap α γ
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Set.smul_set_subset_smul_set_iff₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst_1 : MulAction α β] {a : α},
  a ≠ 0 → ∀ {A B : Set β}, a • A ⊆ a • B ↔ A ⊆ B
-- Mathlib.Topology.Compactness.DeltaGeneratedSpace
/-- **Alias** of `Topology.WithGeneratedByTopology.equiv`. -/
DeltaGeneratedSpace.counit : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      {Y : Type v} → [tY : TopologicalSpace Y] → Topology.WithGeneratedByTopology X Y ≃ Y
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.restrictScalars_apply : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ] (R₀ : Type u_11)
  [inst_9 : CommSemiring R₀] [inst_10 : Algebra R₀ R] [inst_11 : Algebra R₀ A] [inst_12 : Algebra R₀ B]
  [inst_13 : IsScalarTower R₀ R A] [inst_14 : IsScalarTower R₀ R B] (f : 𝒜 →ₐᵍ[R] ℬ) (a : A), (↑R₀ f) a = f a
-- Mathlib.Order.WithBot
WithTop.coe_min : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), ↑(min a b) = min ↑a ↑b
-- Mathlib.Algebra.Lie.Weights.Cartan
/-- Given a nilpotent Lie subalgebra `H ⊆ L`, the root space of a map `χ : H → R` is the weight
space of `L` regarded as a module of `H` via the adjoint action.  -/
LieAlgebra.rootSpace : {R : Type u_1} →
  {L : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] →
          (H : LieSubalgebra R L) → [LieRing.IsNilpotent ↥H] → (↥H → R) → LieSubmodule R (↥H) L
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {J₀ : CategoryTheory.GrothendieckTopology C₀} →
            {J : CategoryTheory.GrothendieckTopology C} →
              {S : C} → F.OneHypercoverDenseData J₀ J S → F.PreOneHypercoverDenseData S
-- Mathlib.LinearAlgebra.Dimension.Constructions
LinearIndependent.sumElim_of_quotient : ∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {M' : Submodule R M}
  {ι₁ : Type u_2} {ι₂ : Type u_3} {f : ι₁ → ↥M'},
  LinearIndependent R f →
    ∀ (g : ι₂ → M), LinearIndependent R (Submodule.Quotient.mk ∘ g) → LinearIndependent R (Sum.elim (fun x => ↑(f x)) g)
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.enorm_rid : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x : TensorProduct 𝕜 E 𝕜), ‖(TensorProduct.rid 𝕜 E) x‖ₑ = ‖x‖ₑ
-- Init.Data.Repr
Sigma.repr : {α : Type u_1} → {β : α → Type v} → [Repr α] → [(x : α) → Repr (β x)] → Sigma β → ℕ → Std.Format
-- Mathlib.SetTheory.ZFC.Class
Class.sInter_empty : ∅.sInter = Class.univ
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.neg_pos : ∀ {α : Type u_2} [inst : LinearOrderedAddCommGroupWithTop α] {a : α}, 0 < -a ↔ a < 0 ∨ a = ⊤
-- Lean.Declaration
Lean.Declaration.thmDecl.inj : ∀ {val val_1 : Lean.TheoremVal}, Lean.Declaration.thmDecl val = Lean.Declaration.thmDecl val_1 → val = val_1
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.coe_ofEq_apply : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] {R' : Type u_12} [inst_1 : Ring R'] [inst_2 : Module R' E]
  {p q : Submodule R' E} (h : p = q) (x : ↥p), ↑((LinearIsometryEquiv.ofEq p q h) x) = ↑x
-- Mathlib.MeasureTheory.PiSystem
isPiSystem_Iic : ∀ {α : Type u_1} [inst : LinearOrder α], IsPiSystem (Set.range Set.Iic)
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.unmop_hom_associator : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y Z : Cᴹᵒᵖ),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom.unmop =
    (CategoryTheory.MonoidalCategoryStruct.associator Z.unmop Y.unmop X.unmop).inv
-- Mathlib.GroupTheory.GroupAction.Pointwise
IsAddUnit.preimage_vadd_setₛₗ : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_4} {β : Type u_5} [inst : AddMonoid M] [inst_1 : AddMonoid N]
  [inst_2 : AddAction M α] [inst_3 : AddAction N β] {c : M} {F : Type u_6} {G : Type u_7} [inst_4 : FunLike G M N]
  [AddMonoidHomClass G M N] (σ : G) [inst_6 : FunLike F α β] [AddActionSemiHomClass F (⇑σ) α β] (f : F),
  IsAddUnit c → ∀ (t : Set β), ⇑f ⁻¹' (σ c +ᵥ t) = c +ᵥ ⇑f ⁻¹' t
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.length_comp : ∀ {V : Type u} [inst : Quiver V] {a b : V} (p : Quiver.Path a b) {c : V} (q : Quiver.Path b c),
  (p.comp q).length = p.length + q.length