mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_castLE_Iic_castLE : ∀ {m n : ℕ} (i : Fin m) (h : m ≤ n), Fin.castLE h ⁻¹' Set.Iic (Fin.castLE h i) = Set.Iic i
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- The image of a subsemigroup along a semigroup homomorphism is a subsemigroup.  -/
Subsemigroup.map : {M : Type u_1} → {N : Type u_2} → [inst : Mul M] → [inst_1 : Mul N] → (M →ₙ* N) → Subsemigroup M → Subsemigroup N
-- Mathlib.RingTheory.Multiplicity
multiplicity_eq_of_dvd_of_not_dvd : ∀ {α : Type u_1} [inst : Monoid α] {a b : α} {k : ℕ}, a ^ k ∣ b → ¬a ^ (k + 1) ∣ b → multiplicity a b = k
-- Mathlib.Order.Bounds.Image
IsCofinalFor.image_of_monotone : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s t : Set α} {f : α → β},
  IsCofinalFor s t → Monotone f → IsCofinalFor (f '' s) (f '' t)
-- Mathlib.Topology.Order.LeftRightLim
Antitone.leftLim_le : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Antitone f → ∀ {x y : α}, x < y → Function.leftLim f y ≤ f x
-- Init.Data.Array.Basic
/-- Version of `Array.uget` that does not increment the reference count of its result.

This is only intended for direct use by the compiler.
 -/
Array.ugetBorrowed : {α : Type u} → (xs : Array α) → (i : USize) → i.toNat < xs.size → α
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
/-- **Alias** of the reverse direction of `OpenPartialHomeomorph.IsImage.iff_symm_preimage_eq'`. -/
OpenPartialHomeomorph.IsImage.of_symm_preimage_eq' : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y},
  e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s) = e.target ∩ t → e.IsImage s t
-- Mathlib.Analysis.InnerProductSpace.Rayleigh
/-- For a self-adjoint operator `T`, a local extremum of the Rayleigh quotient of `T` on a sphere
centred at the origin is an eigenvector of `T`.  -/
IsSelfAdjoint.hasEigenvector_of_isLocalExtrOn : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] {T : E →L[𝕜] E},
  IsSelfAdjoint T →
    ∀ {x₀ : E},
      x₀ ≠ 0 →
        IsLocalExtrOn T.reApplyInnerSelf (Metric.sphere 0 ‖x₀‖) x₀ →
          Module.End.HasEigenvector (↑T) (↑(T.rayleighQuotient x₀)) x₀
-- Mathlib.Topology.Category.TopCat.Yoneda
ContinuousMap.comp_yonedaPresheaf' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C TopCat) (Y : Type w')
  [inst_1 : TopologicalSpace Y], ContinuousMap.yonedaPresheaf F Y = F.op.comp (ContinuousMap.yonedaPresheaf' Y)
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
/-- The two-variable Jacobi theta function is even in `z`.  -/
jacobiTheta₂_neg_left : ∀ (z τ : ℂ), jacobiTheta₂ (-z) τ = jacobiTheta₂ z τ
-- Mathlib.CategoryTheory.Preadditive.Indization
CategoryTheory.instPreadditiveInd : {C : Type u} →
  [inst : CategoryTheory.SmallCategory C] →
    [CategoryTheory.Preadditive C] →
      [CategoryTheory.Limits.HasFiniteColimits C] → CategoryTheory.Preadditive (CategoryTheory.Ind C)
-- Mathlib.Algebra.GroupWithZero.Action.Units
inv_smul_smul₀ : ∀ {α : Type u_4} {β : Type u_5} [inst : GroupWithZero α] [inst_1 : MulAction α β] {a : α},
  a ≠ 0 → ∀ (x : β), a⁻¹ • a • x = x
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.invVeblen₁_epsilon : ∀ {o : Ordinal.{u}}, o < o.epsilon → o.epsilon.invVeblen₁ = 1
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.endsWith_dropEndWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] [inst_2 : String.Slice.Pattern.BackwardPattern pat]
  [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat] {s : String.Slice},
  (s.dropEndWhile pat).endsWith pat = false
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.ΓSpec_adjunction_homEquiv_eq : ∀ {X : AlgebraicGeometry.Scheme} {B : CommRingCat} (φ : B ⟶ X.presheaf.obj (Opposite.op ⊤)),
  AlgebraicGeometry.Scheme.Hom.appTop ((AlgebraicGeometry.ΓSpec.adjunction.homEquiv X (Opposite.op B)) φ.op) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso B).hom φ
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.pushAlign : Bool → Lean.PrettyPrinter.FormatterM Unit
-- Mathlib.Analysis.Calculus.ContDiff.Basic
ContinuousLinearMap.contDiff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  (f : E →L[𝕜] F), ContDiff 𝕜 n ⇑f
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.le_iInf_lintegral : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Sort u_4} (f : ι → α → ENNReal),
  ∫⁻ (a : α), ⨅ i, f i a ∂μ ≤ ⨅ i, ∫⁻ (a : α), f i a ∂μ
-- Mathlib.Algebra.Algebra.NonUnitalHom
/-- A unital morphism of algebras is a `NonUnitalAlgHom`.  -/
AlgHom.toNonUnitalAlgHom : {R : Type u_2} →
  [inst : CommSemiring R] →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] → [inst_3 : Algebra R A] → [inst_4 : Algebra R B] → (A →ₐ[R] B) → A →ₙₐ[R] B
-- Init.Data.BitVec.Lemmas
/-- Unsigned addition overflow reassociation.
If `(x + y)` and `(y + z)` do not overflow, then `(x + y) + z` overflows iff `x + (y + z)` overflows.
 -/
BitVec.uaddOverflow_assoc : ∀ {w : ℕ} {x y z : BitVec w},
  ¬x.uaddOverflow y = true → ¬y.uaddOverflow z = true → (x + y).uaddOverflow z = x.uaddOverflow (y + z)
-- Mathlib.Analysis.Complex.Circle
Circle.ext : ∀ {x y : Circle}, ↑x = ↑y → x = y
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.instSigmaFiniteRestrictInterSet : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}
  [MeasureTheory.SigmaFinite (μ.restrict s)], MeasureTheory.SigmaFinite (μ.restrict (s ∩ t))
-- Mathlib.Algebra.Group.Units.Defs
/-- Units of a monoid have division  -/
Units.instDiv : {α : Type u} → [inst : Monoid α] → Div αˣ
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- We say that a type has `MeasurableInv` if `x ↦ x⁻¹` is a measurable function.  -/
MeasurableInv : (G : Type u_2) → [Inv G] → [MeasurableSpace G] → Prop
-- Mathlib.RingTheory.MvPolynomial.Basic
MvPolynomial.monomial_mem_restrictSupport : ∀ {σ : Type u} (R : Type v) [inst : CommSemiring R] {s : Set (σ →₀ ℕ)} {m : σ →₀ ℕ} {r : R},
  (MvPolynomial.monomial m) r ∈ MvPolynomial.restrictSupport R s ↔ m ∈ s ∨ r = 0
-- Init.Data.String.Defs
String.Pos.mk.injEq : ∀ {s : String} (offset : String.Pos.Raw) (isValid : String.Pos.Raw.IsValid s offset) (offset_1 : String.Pos.Raw)
  (isValid_1 : String.Pos.Raw.IsValid s offset_1),
  ({ offset := offset, isValid := isValid } = { offset := offset_1, isValid := isValid_1 }) = (offset = offset_1)
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.instFaithfulOppositeFunctorTypeShrinkCoyoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C],
  CategoryTheory.shrinkCoyoneda.{w, v, u}.Faithful
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.WalkingReflexivePair.Hom.leftCompReflexion : CategoryTheory.Limits.WalkingReflexivePair.one.Hom CategoryTheory.Limits.WalkingReflexivePair.one
-- Lean.Meta.Injective
Lean.Meta.genInjectivity : Lean.Option Bool
-- Aesop.Rule.Forward
/-- If the rule is a norm or safe rule, its priority is an integer.  -/
Aesop.ForwardRulePriority.normSafe : ℤ → Aesop.ForwardRulePriority
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.comp_assoc : ∀ {M : Type u_2} {N : Type u_3} {P : Type u_4} {φ : M → N} {ψ : N → P} {χ : M → P} {X : Type u_5} [inst : SMul M X]
  {Y : Type u_6} [inst_1 : SMul N Y] {Z : Type u_7} [inst_2 : SMul P Z] {Q : Type u_8} {T : Type u_9}
  [inst_3 : SMul Q T] {η : P → Q} {θ : M → Q} {ζ : N → Q} (h : Z →ₑ[η] T) (g : Y →ₑ[ψ] Z) (f : X →ₑ[φ] Y)
  [inst_4 : CompTriple φ ψ χ] [inst_5 : CompTriple χ η θ] [inst_6 : CompTriple ψ η ζ] [inst_7 : CompTriple φ ζ θ],
  h.comp (g.comp f) = (h.comp g).comp f
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α},
  Std.DHashMap.Const.get? (m₁.diff m₂) k = if k ∈ m₂ then none else Std.DHashMap.Const.get? m₁ k
-- Lean.CompactedRegion
/-- Holds an opaque compactor handle returned by `CompactedRegion.save`, used to chain subsequent saves
so that objects shared between parts are emitted exactly once.

Not thread-safe: a `Compactor` value must not be used concurrently from multiple threads. The
`CompactedRegion`s passed as `depRegions` when the `Compactor` was first created must outlive the
`Compactor`; if any are freed (via `CompactedRegion.free`) while the `Compactor` is still in use,
subsequent saves will dereference dangling pointers.
 -/
Lean.Compactor : Type
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
/-- Trie used to organize those handlers provided in `EvalConfigItemView` and those
handlers that are synthesized.

The fields in this `structure` are given in the order they are applied.
Conceptually, searching for handlers is done recursively (however the algorithm is compiled
into non-recursive code via metaprogramming). At each step of the search the state
consists of a trie key `tkey`, a trie node `trie`, and a configuration key `ckey`.
Once any handler is applied, matching is complete (handlers can't decide not to apply at run time).
1. If `exact?` is present and `tkey == ckey`, then it is applied.
2. If `ckey` is of the form `root.ckey'` and there's a `(root, trie')` entry in `children`,
   then we recursively search for a handler using `tkey.root`, `trie'`, `ckey'`.
   If one is found, it is applied.
3. If `wildcard?` is present and `ckey'` is nonempty, then that handler is applied.
4. Otherwise, the search failed. If this is recursive, we return and continue.
 -/
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.HandlerTrie : Type
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_eq_some : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α},
  Std.Internal.List.containsKey a l = true → Std.Internal.List.getKey? a l = some a
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- The coevaluation natural transformation.  -/
CategoryTheory.ihom.coev : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (A : C) →
        [inst_2 : CategoryTheory.Closed A] →
          CategoryTheory.Functor.id C ⟶ (CategoryTheory.MonoidalCategory.tensorLeft A).comp (CategoryTheory.ihom A)
-- Lean.Elab.Tactic.ElabTerm
Lean.Elab.Tactic.evalExact : Lean.Elab.Tactic.Tactic
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.hasPushout : ∀ {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 → CategoryTheory.Limits.HasPushout f g
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.mk_trans_mk : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β) (g : β → γ) (hf : Function.Injective f)
  (hg : Function.Injective g),
  { toFun := f, inj' := hf }.trans { toFun := g, inj' := hg } = { toFun := g ∘ f, inj' := ⋯ }
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.piecewise_empty : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] (f g : MeasureTheory.SimpleFunc α β),
  MeasureTheory.SimpleFunc.piecewise ∅ ⋯ f g = g
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- The set of fixed points of a normal subgroup is stable under the group action.  -/
fixedPointsSubAddOfNormal : {G : Type u_1} →
  [inst : AddGroup G] →
    {α : Type u_2} → [inst_1 : AddAction G α] → {H : AddSubgroup G} → [hH : H.Normal] → SubAddAction G α
-- Mathlib.RingTheory.Adjoin.FG
Subalgebra.induction_on_adjoin : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] [IsNoetherian R A]
  (P : Subalgebra R A → Prop),
  P ⊥ → (∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x ↑S))) → ∀ (S : Subalgebra R A), P S
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
/-- Given a prepartition `π : BoxIntegral.Prepartition I`, `π.iUnion` is the part of `I` covered by
the boxes of `π`.  -/
BoxIntegral.Prepartition.iUnion : {ι : Type u_1} → {I : BoxIntegral.Box ι} → BoxIntegral.Prepartition I → Set (ι → ℝ)
-- Init.Data.Slice.List.Lemmas
ListSlice.toArray_mkSlice_rci_eq_toArray_mkSlice_rco : ∀ {α : Type u_1} {xs : ListSlice α} {lo : ℕ},
  Std.Slice.toArray (Std.Rci.Sliceable.mkSlice xs lo...*) =
    Std.Slice.toArray (Std.Rco.Sliceable.mkSlice xs lo...Std.Slice.size xs)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.zero_of_source_iso_zero' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y), CategoryTheory.IsIsomorphic X 0 → f = 0
-- Mathlib.AlgebraicGeometry.LimitsOver
AlgebraicGeometry.instMonoObjWalkingSpanCompOverSchemeTopMorphismPropertySpanOverForgetForgetForgetNoneWalkingPairSomeMapInitOfIsOpenImmersionLeftDiscretePUnit : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {S : AlgebraicGeometry.Scheme} {U X Y : P.Over ⊤ S}
  (f : U ⟶ X) (g : U ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f.left] [AlgebraicGeometry.IsOpenImmersion g.left]
  (i : CategoryTheory.Limits.WalkingPair),
  CategoryTheory.Mono
    (((CategoryTheory.Limits.span f g).comp
          ((CategoryTheory.MorphismProperty.Over.forget P ⊤ S).comp
            ((CategoryTheory.Over.forget S).comp AlgebraicGeometry.Scheme.forget))).map
      (CategoryTheory.Limits.WidePushoutShape.Hom.init i))
-- Std.Data.String.ToNat
String.toNat?_append_underscore_append_eq_some : ∀ {s t : String} {n m : ℕ},
  s.toNat? = some n →
    t.toNat? = some m → (s ++ "_" ++ t).toNat? = some (10 ^ (List.filter (fun x => x != '_') t.toList).length * n + m)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ D` reflects limits, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` reflects colimits.  -/
CategoryTheory.Limits.reflectsColimits_op : ∀ {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.ReflectsLimits F], CategoryTheory.Limits.ReflectsColimits F.op
-- Lean.Elab.Tactic.Omega.Frontend
_private.Lean.Elab.Tactic.Omega.Frontend.0.Lean.Elab.Tactic.Omega.instEvalExprOmegaConfig.evalExpr : Lean.Expr → Lean.MetaM Lean.Meta.Omega.OmegaConfig
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.elabSimpConfigCtxCore : Lean.Syntax →
  optParam Lean.Meta.Simp.ConfigCtx { } →
    optParam Lean.Options ∅ → Lean.Elab.Tactic.TacticM Lean.Meta.Simp.ConfigWithOptions
-- Mathlib.Algebra.Star.Basic
starMulEquiv_apply : ∀ {R : Type u} [inst : Mul R] [inst_1 : StarMul R] (x : R), starMulEquiv x = MulOpposite.op (star x)
-- Init.Data.String.Basic
String.Slice.Pos.sliceFrom.congr_simp : ∀ {s : String.Slice} (p₀ pos pos_1 : s.Pos) (e_pos : pos = pos_1) (h : p₀ ≤ pos),
  p₀.sliceFrom pos h = p₀.sliceFrom pos_1 ⋯
-- Mathlib.Combinatorics.Quiver.Push
Quiver.Push.lift_comp : ∀ {V : Type u_1} [inst : Quiver V] {W : Type u_2} (σ : V → W) {W' : Type u_3} [inst_1 : Quiver W'] (φ : V ⥤q W')
  (τ : W → W') (h : ∀ (x : V), φ.obj x = τ (σ x)), Quiver.Push.of σ ⋙q Quiver.Push.lift σ φ τ h = φ
-- Mathlib.RingTheory.Algebraic.Integral
Algebra.IsAlgebraic.of_isIntegralClosure : ∀ (R : Type u_1) (B : Type u_2) (C : Type u_3) [inst : CommRing R] [Nontrivial R] [inst_2 : CommRing B]
  [inst_3 : CommRing C] [inst_4 : Algebra R B] [inst_5 : Algebra R C] [inst_6 : Algebra B C] [IsScalarTower R B C]
  [IsIntegralClosure B R C], Algebra.IsAlgebraic R B
-- Mathlib.Order.RelIso.Basic
RelEmbedding.prodLexMkRight_apply : ∀ {α : Type u_1} {β : Type u_2} {s : β → β → Prop} (r : α → α → Prop) {b : β} (h : ¬s b b) (a : α),
  (RelEmbedding.prodLexMkRight r h) a = (a, b)
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ResolveSimpIdResult : Type
-- Batteries.Data.BinomialHeap.Basic
/-- `O(n)`. The "real size" of the heap, counting up how many values of type `α` are stored.
This is intended mainly for specification purposes.
Prefer `Heap.size`, which is the same for well formed heaps.
 -/
Batteries.BinomialHeap.Imp.Heap.realSize : {α : Type u_1} → Batteries.BinomialHeap.Imp.Heap α → ℕ
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.toExtension_algebra₂ : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Generators R S ι), P.toExtension.algebra₂ = P.instRing
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.comp_l : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Wₗ Wᵣ : CategoryTheory.MorphismProperty C}
  [inst_1 : Wₗ.HasPullbacksAgainst Wᵣ] [inst_2 : Wₗ.IsStableUnderBaseChangeAgainst Wᵣ]
  [inst_3 : Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] [inst_4 : Wₗ.IsStableUnderComposition]
  [inst_5 : Wᵣ.IsStableUnderComposition] {c c' c'' : C} (S₁ : CategoryTheory.Span Wₗ Wᵣ c c')
  (S₂ : CategoryTheory.Span Wₗ Wᵣ c' c''),
  (S₁.comp S₂).l = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst S₁.r S₂.l) S₁.l
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.coroot_zero : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra]
  [inst_5 : LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [CharZero K] [inst_8 : Nontrivial L],
  LieAlgebra.IsKilling.coroot 0 = 0
-- Mathlib.Data.Set.Operations
Set.mem_range : ∀ {α : Type u} {ι : Sort u_1} {f : ι → α} {x : α}, x ∈ Set.range f ↔ ∃ y, f y = x
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.not_mem_inter_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → k ∉ m₁ ∩ m₂
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.congrIsometry_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : InnerProductSpace 𝕜 H] (f : E ≃ₗᵢ[𝕜] G) (g : F ≃ₗᵢ[𝕜] H)
  (x : TensorProduct 𝕜 E F), (TensorProduct.congrIsometry f g) x = (TensorProduct.congr ↑↑f ↑↑g) x
-- Init.Data.BitVec.Lemmas
BitVec.msb_eq_toInt : ∀ {w : ℕ} {x : BitVec w}, x.msb = decide (x.toInt < 0)
-- Init.Data.Stream
/-- Streams are used to implement parallel `for` statements.
Example:
```
for x in xs, y in ys do
  ...
```
is expanded into
```
let mut s := toStream ys
for x in xs do
  match Stream.next? s with
  | none => break
  | some (y, s') =>
    s := s'
    ...
```
 -/
Std.ToStream : Type u → outParam (Type u) → Type u
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k a : α}
  {h' : a ∈ t.erase k}, (t.erase k)[a] = t[a]
-- Init.Data.Float.Model.Unpacked.Sign
Float.Model.UnpackedFloat.Sign.negative.sizeOf_spec : sizeOf Float.Model.UnpackedFloat.Sign.negative = 1
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.Cowedge.IsColimit.desc.congr_simp : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} {c : CategoryTheory.Limits.Cowedge F}
  (hc hc_1 : CategoryTheory.Limits.IsColimit c),
  hc = hc_1 →
    ∀ {X : C} (f f_1 : (j : J) → (F.obj (Opposite.op j)).obj j ⟶ X) (e_f : f = f_1)
      (hf :
        ∀ ⦃i j : J⦄ (g : i ⟶ j),
          CategoryTheory.CategoryStruct.comp ((F.map g.op).app i) (f i) =
            CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op j)).map g) (f j)),
      CategoryTheory.Limits.Cowedge.IsColimit.desc hc f hf = CategoryTheory.Limits.Cowedge.IsColimit.desc hc_1 f_1 ⋯
-- Mathlib.GroupTheory.Coset.Defs
QuotientAddGroup.instDecidableEqQuotientAddSubgroupOfDecidablePredMem.eq_1 : ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) [inst_1 : DecidablePred fun x => x ∈ s],
  QuotientAddGroup.instDecidableEqQuotientAddSubgroupOfDecidablePredMem s = Quotient.decidableEq
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_of_perm : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] [inst_2 : Inhabited α] {l l' : List ((a : α) × β a)}
  {a : α}, Std.Internal.List.DistinctKeys l → l.Perm l' → Std.Internal.List.getKey! a l = Std.Internal.List.getKey! a l'
-- Mathlib.RingTheory.Etale.Locus
/-- `Algebra.etaleLocus R A` is the set of primes `p` of `A` that are etale.  -/
Algebra.etaleLocus : (R : Type u_1) → (A : Type u_2) → [inst : CommRing R] → [inst_1 : CommRing A] → [Algebra R A] → Set (PrimeSpectrum A)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
/-- The canonical isomorphism `Proj A |_ D₊(f) ≅ Spec (A_f)₀`
when `f` is homogeneous of positive degree.  -/
AlgebraicGeometry.Proj.basicOpenIsoSpec : {σ : Type u_1} →
  {A : Type u} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          (𝒜 : ℕ → σ) →
            [inst_3 : GradedRing 𝒜] →
              (f : A) →
                {m : ℕ} →
                  f ∈ 𝒜 m →
                    0 < m →
                      (↑(AlgebraicGeometry.Proj.basicOpen 𝒜 f) ≅
                        AlgebraicGeometry.Spec (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f)))
-- Mathlib.GroupTheory.Index
Subgroup.index_ne_zero_iff_finite : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.index ≠ 0 ↔ Finite (G ⧸ H)
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
NonnegSpectrumClass.iff_spectrum_nonneg : ∀ {𝕜 : Type u_3} {A : Type u_4} [inst : Semifield 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : Ring A]
  [inst_3 : PartialOrder A] [inst_4 : Algebra 𝕜 A],
  NonnegSpectrumClass 𝕜 A ↔ ∀ (a : A), 0 ≤ a → ∀ x ∈ spectrum 𝕜 a, 0 ≤ x
-- Mathlib.Topology.Order.Lattice
ContinuousOn.sup : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] [inst_2 : Max L]
  [ContinuousSup L] {f g : X → L} {s : Set X}, ContinuousOn f s → ContinuousOn g s → ContinuousOn (fun a => f a ⊔ g a) s
-- Mathlib.Algebra.BigOperators.Fin
finSigmaFinEquiv.eq_def : ∀ {m : ℕ} {n : Fin m → ℕ},
  finSigmaFinEquiv =
    match m, n with
    | 0, n => Equiv.equivOfIsEmpty ((i : Fin 0) × Fin (n i)) (Fin (∑ i, n i))
    | m.succ, n =>
      Trans.trans
        (Trans.trans
          (Trans.trans
            (Trans.trans finSumFinEquiv.sigmaCongrLeft.symm (Equiv.sumSigmaDistrib fun a => Fin (n (finSumFinEquiv a))))
            (finSigmaFinEquiv.sumCongr (Equiv.uniqueSigma fun i => Fin (n (finSumFinEquiv (Sum.inr i))))))
          finSumFinEquiv)
        (finCongr ⋯)
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.norm_single : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] [inst_1 : DecidableEq α],
  0 < p → ∀ (i : α) (x : E i), ‖lp.single p i x‖ = ‖x‖