mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
HomotopyCategory.Plus.instHasRightResolutionsArrowInjectiveObjectArrowIsomorphismsQuasiIsoArrowLocalizerMorphism : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.EnoughInjectives C], (HomotopyCategory.Plus.localizerMorphism C).arrow.HasRightResolutions
-- Lean.Elab.InfoTree.Types
Lean.Elab.InfoTree.brecOn_4.eq : ∀ {motive_1 : Lean.Elab.InfoTree → Sort u} {motive_2 : Lean.PersistentArray Lean.Elab.InfoTree → Sort u}
  {motive_3 : Lean.PersistentArrayNode Lean.Elab.InfoTree → Sort u} {motive_4 : Array Lean.Elab.InfoTree → Sort u}
  {motive_5 : Array (Lean.PersistentArrayNode Lean.Elab.InfoTree) → Sort u}
  {motive_6 : List Lean.Elab.InfoTree → Sort u} {motive_7 : List (Lean.PersistentArrayNode Lean.Elab.InfoTree) → Sort u}
  (t : Array (Lean.PersistentArrayNode Lean.Elab.InfoTree)) (F_1 : (t : Lean.Elab.InfoTree) → t.below → motive_1 t)
  (F_2 : (t : Lean.PersistentArray Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_1 t → motive_2 t)
  (F_3 : (t : Lean.PersistentArrayNode Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_2 t → motive_3 t)
  (F_4 : (t : Array Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_3 t → motive_4 t)
  (F_5 : (t : Array (Lean.PersistentArrayNode Lean.Elab.InfoTree)) → Lean.Elab.InfoTree.below_4 t → motive_5 t)
  (F_6 : (t : List Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_5 t → motive_6 t)
  (F_7 : (t : List (Lean.PersistentArrayNode Lean.Elab.InfoTree)) → Lean.Elab.InfoTree.below_6 t → motive_7 t),
  Lean.Elab.InfoTree.brecOn_4 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 =
    F_5 t (Lean.Elab.InfoTree.brecOn_4.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7).2
-- Mathlib.Data.Set.Basic
Set.sep_eq_empty_iff_mem_false : ∀ {α : Type u} {s : Set α} {p : α → Prop}, {x | x ∈ s ∧ p x} = ∅ ↔ ∀ x ∈ s, ¬p x
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.leadingCoeff_sub_of_degree_lt' : ∀ {R : Type u} [inst : Ring R] {p q : Polynomial R}, p.degree < q.degree → (p - q).leadingCoeff = -q.leadingCoeff
-- Init.Data.Nat.Basic
Nat.zero_lt_two : 0 < 2
-- Mathlib.Data.Nat.Fib.Basic
Nat.fib_zero : Nat.fib 0 = 0
-- Init.Data.String.Length
String.length_pushn : ∀ {s : String} (c : Char) (n : ℕ), (s.pushn c n).length = s.length + n
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.mem_closedEBall_self`. -/
EMetric.mem_closedBall_self : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {ε : ENNReal}, x ∈ Metric.closedEBall x ε
-- Mathlib.Algebra.Group.Subgroup.Finite
Subgroup.eq_top_of_card_eq : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [Finite ↥H], Nat.card ↥H = Nat.card G → H = ⊤
-- Lean.Meta.Sym.ReplaceS
_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.visitChild.match_1.eq_1 : ∀ (motive : Lean.Expr → Sort u_1) (a : Lean.Literal) (h_1 : (a : Lean.Literal) → motive (Lean.Expr.lit a))
  (h_2 : (mvarId : Lean.MVarId) → motive (Lean.Expr.mvar mvarId))
  (h_3 : (deBruijnIndex : ℕ) → motive (Lean.Expr.bvar deBruijnIndex))
  (h_4 : (fvarId : Lean.FVarId) → motive (Lean.Expr.fvar fvarId))
  (h_5 : (declName : Lean.Name) → (us : List Lean.Level) → motive (Lean.Expr.const declName us))
  (h_6 : (u : Lean.Level) → motive (Lean.Expr.sort u)) (h_7 : (e : Lean.Expr) → motive e),
  (match Lean.Expr.lit a with
    | Lean.Expr.lit a => h_1 a
    | Lean.Expr.mvar mvarId => h_2 mvarId
    | Lean.Expr.bvar deBruijnIndex => h_3 deBruijnIndex
    | Lean.Expr.fvar fvarId => h_4 fvarId
    | Lean.Expr.const declName us => h_5 declName us
    | Lean.Expr.sort u => h_6 u
    | e => h_7 e) =
    h_1 a
-- Mathlib.Data.Set.Card
Set.encard_prod : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β}, (s ×ˢ t).encard = s.encard * t.encard
-- Mathlib.Algebra.CharP.Algebra
/-- If `R` has characteristic `p`, then so does `FreeAlgebra R X`.  -/
FreeAlgebra.charP : ∀ {R : Type u_3} {X : Type u_4} [inst : CommSemiring R] (p : ℕ) [CharP R p], CharP (FreeAlgebra R X) p
-- Mathlib.Topology.FiberBundle.Basic
MemTrivializationAtlas.out : ∀ {B : Type u_2} {F : Type u_3} {inst : TopologicalSpace B} {inst_1 : TopologicalSpace F} {E : B → Type u_5}
  {inst_2 : TopologicalSpace (Bundle.TotalSpace F E)} {inst_3 : (b : B) → TopologicalSpace (E b)}
  {inst_4 : FiberBundle F E} {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [self : MemTrivializationAtlas e],
  e ∈ trivializationAtlas F E
-- Mathlib.Order.CompleteLattice.Basic
sInf_pair : ∀ {α : Type u_1} [inst : CompleteLattice α] {a b : α}, sInf {a, b} = a ⊓ b
-- Mathlib.Order.Filter.IsBounded
/-- In linear orders, frequent boundedness from below implies coboundedness for `≤`.  -/
Filter.IsCobounded.of_frequently_ge : ∀ {α : Type u_1} {f : Filter α} [inst : LinearOrder α] {l : α},
  (∃ᶠ (x : α) in f, l ≤ x) → Filter.IsCobounded (fun x1 x2 => x1 ≤ x2) f
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.infEDist_le_edist_add_infEDist : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α} {s : Set α},
  Metric.infEDist x s ≤ edist x y + Metric.infEDist y s
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor_naturality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (U : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolutionUnit U]
  {F : CategoryTheory.Functor C V}
  [inst_5 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution F U] {G : CategoryTheory.Functor C V}
  [inst_7 : CategoryTheory.MonoidalCategory.DayConvolution G U] (f : F ⟶ G),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.DayConvolution.map f (CategoryTheory.CategoryStruct.id U))
      (CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor U G).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor U F).hom f
-- Mathlib.Lean.Linter
/-- Runs a `CommandElabM` action when the provided linter option is `false`.

Note: this definition is marked as `@[macro_inline]`, so it is okay to supply it with a linter
option which has been registered in the same module.
 -/
Lean.Linter.whenNotLinterOption : {m : Type → Type} → [Monad m] → [Lean.MonadOptions m] → [Lean.MonadEnv m] → Lean.Option Bool → m Unit → m Unit
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
borel_eq_generateFrom_isClosed : ∀ {α : Type u_1} [inst : TopologicalSpace α], borel α = MeasurableSpace.generateFrom {s | IsClosed s}
-- Mathlib.Logic.Function.FromTypes
Function.fromTypes_cons : ∀ {n : ℕ} (α : Type u) (p : Fin n → Type u) (τ : Type u),
  Function.FromTypes (Matrix.vecCons α p) τ = (α → Function.FromTypes p τ)
-- Init.Data.Range.Polymorphic.Char
Char.instIsAlwaysFinite_1 : Std.Rxo.IsAlwaysFinite Char
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.incenter_map : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {V₂ : Type u_3} {P₂ : Type u_4} [inst_4 : NormedAddCommGroup V₂]
  [inst_5 : InnerProductSpace ℝ V₂] [inst_6 : MetricSpace P₂] [inst_7 : NormedAddTorsor V₂ P₂] {n : ℕ}
  [inst_8 : NeZero n] (s : Affine.Simplex ℝ P n) (f : P →ᵃⁱ[ℝ] P₂), (s.map f.toAffineMap ⋯).incenter = f s.incenter
-- Mathlib.Geometry.Manifold.Algebra.Monoid
/-- **Alias** of `contMDiffOn_finsetProd'`. -/
contMDiffOn_finset_prod' : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : CommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffMul I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {s : Set M} {t : Finset ι}
  {f : ι → M → G}, (∀ i ∈ t, ContMDiffOn I' I n (f i) s) → ContMDiffOn I' I n (∏ i ∈ t, f i) s
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_sub_pi : ∀ (x : ℝ), Real.sin (x - Real.pi) = -Real.sin x
-- Mathlib.Algebra.Order.Module.Defs
OrderDual.instPosSMulReflectLE : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : SMul α β] [inst_3 : Zero α]
  [PosSMulReflectLE α β], PosSMulReflectLE α βᵒᵈ
-- Mathlib.Topology.Order.OrderClosed
bddAbove_closure : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [ClosedIicTopology α] {s : Set α},
  BddAbove (closure s) ↔ BddAbove s
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.isGround.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.coe_centralizer : ∀ {R : Type u_1} [inst : Ring R] (s : Set R), ↑(Subring.centralizer s) = s.centralizer
-- Mathlib.Topology.IsLocalHomeomorph
IsLocalHomeomorphOn.continuousOn : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X},
  IsLocalHomeomorphOn f s → ContinuousOn f s
-- Mathlib.Topology.Connected.Basic
isPreconnected_connectedComponentIn : ∀ {α : Type u} [inst : TopologicalSpace α] {x : α} {F : Set α}, IsPreconnected (connectedComponentIn F x)
-- Mathlib.Data.Vector3
Vector3.append_insert : ∀ {α : Type u_1} {m n : ℕ} (a : α) (t : Vector3 α m) (v : Vector3 α n) (i : Fin2 (n + 1)) (e : n + 1 + m = n + m + 1),
  Vector3.insert a (t.append v) (Eq.recOn e (i.add m)) = Eq.recOn e (t.append (Vector3.insert a v i))
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.isSheaf_iff_isSheaf_of_type : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C)
  (P : CategoryTheory.Functor Cᵒᵖ (Type w)), CategoryTheory.Presheaf.IsSheaf J P ↔ CategoryTheory.Presieve.IsSheaf J P
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get!_diff_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} [inst_1 : Inhabited (β k)], k ∉ t₂ → (t₁ \ t₂).get! k = t₁.get! k
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.nat_lt_card : ∀ {o : Ordinal.{u_1}} {n : ℕ}, ↑n < o.card ↔ ↑n < o
-- Mathlib.Topology.Order
/-- See also `continuous_of_discreteTopology`, which works for `IsEmpty α`.  -/
continuous_empty_function : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [IsEmpty β] (f : α → β),
  Continuous f
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- Asymptotically, the logarithmic counting function for the zeros of `f * g` is less than or equal to
the sum of the logarithmic counting functions for the zeros of `f` and `g`, respectively.
 -/
ValueDistribution.logCounting_mul_zero_eventuallyLE : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : ProperSpace 𝕜] {f₁ f₂ : 𝕜 → 𝕜},
  Meromorphic f₁ →
    (∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤) →
      Meromorphic f₂ →
        (∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤) →
          ValueDistribution.logCounting (f₁ * f₂) 0 ≤ᶠ[Filter.atTop]
            ValueDistribution.logCounting f₁ 0 + ValueDistribution.logCounting f₂ 0
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.induce_verts : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (s : Set V), (G'.induce s).verts = s
-- Mathlib.CategoryTheory.Monoidal.Closed.Types
CategoryTheory.instMonoidalClosedFunctorTypeOfEssentiallySmall : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.EssentiallySmall.{v₁, v₁, u₁} C] →
      CategoryTheory.MonoidalClosed (CategoryTheory.Functor C (Type v₁))
-- Mathlib.Util.Export
Lean.Export.State.defs : Lean.Export.State → Std.HashSet Lean.Name
-- Mathlib.Order.CompleteLattice.Basic
sSup_eq_iSup : ∀ {α : Type u_1} [inst : CompleteLattice α] {s : Set α}, sSup s = ⨆ a ∈ s, a
-- Mathlib.FieldTheory.Minpoly.Field
minpoly.eq_of_irreducible : ∀ {A : Type u_1} {B : Type u_2} [inst : Field A] [inst_1 : Ring B] [inst_2 : Algebra A B] {x : B} [Nontrivial B]
  {p : Polynomial A}, Irreducible p → (Polynomial.aeval x) p = 0 → p * Polynomial.C p.leadingCoeff⁻¹ = minpoly A x
-- Mathlib.Data.Multiset.Sym
Multiset.sym2_zero : ∀ {α : Type u_1}, Multiset.sym2 0 = 0
-- Mathlib.LinearAlgebra.Dimension.Constructions
LinearIndepOn.quotient_iff_union : ∀ {R : Type u} {M : Type v} {ι : Type w} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {s t : Set ι}
  {f : ι → M},
  LinearIndepOn R f s →
    Disjoint s t → (LinearIndepOn R (⇑(Submodule.span R (f '' s)).mkQ ∘ f) t ↔ LinearIndepOn R f (s ∪ t))
-- Mathlib.Data.Rat.Floor
Rat.instFloorRing : FloorRing ℚ
-- Mathlib.LinearAlgebra.TensorProduct.Associator
LinearMap.rTensor_tensor : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R Q] [inst_8 : Module R P] (g : P →ₗ[R] Q),
  LinearMap.rTensor (TensorProduct R M N) g =
    ↑(TensorProduct.assoc R Q M N) ∘ₗ LinearMap.rTensor N (LinearMap.rTensor M g) ∘ₗ ↑(TensorProduct.assoc R P M N).symm
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.Normal.of_map_subtype : ∀ {G : Type u_1} [inst : Group G] {K : Subgroup G} {L : Subgroup ↥K}, (Subgroup.map K.subtype L).Normal → L.Normal
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.forgetReflectsIsos : (CategoryTheory.forget AddSemigrp).ReflectsIsomorphisms
-- Mathlib.GroupTheory.GroupAction.Support
AddAction.Supports.mono : ∀ {G : Type u_1} {α : Type u_3} {β : Type u_4} [inst : VAdd G α] [inst_1 : VAdd G β] {s t : Set α} {b : β},
  s ⊆ t → AddAction.Supports G s b → AddAction.Supports G t b
-- Mathlib.Control.Fold
Traversable.foldMap_hom : ∀ {α β γ : Type u} {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] [inst_2 : Monoid α]
  [inst_3 : Monoid β] (f : α →* β) (g : γ → α) (x : t γ), f (Traversable.foldMap g x) = Traversable.foldMap (⇑f ∘ g) x
-- Init.Internal.Order.Basic
Lean.Order.MonoBind.bind_mono_right : ∀ {m : Type u → Type v} {inst : Bind m} {inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)}
  [self : Lean.Order.MonoBind m] {α β : Type u} {a : m α} {f₁ f₂ : α → m β},
  (∀ (x : α), Lean.Order.PartialOrder.rel (f₁ x) (f₂ x)) → Lean.Order.PartialOrder.rel (a >>= f₁) (a >>= f₂)
-- Init.Data.Range.Polymorphic.SInt
Int16.instRxoHasSize : Std.Rxo.HasSize Int16
-- Init.Data.BitVec.Bootstrap
BitVec.msb.eq_1 : ∀ {n : ℕ} (x : BitVec n), x.msb = x.getMsbD 0
-- Mathlib.CategoryTheory.Sites.Limits
/-- If `E` is a cone of shape `K` of sheaves, which is a limit on the level of presheaves,
this definition shows that the limit presheaf satisfies the multifork variant of the sheaf
condition, at a given covering `W`.

This is used below in `isSheaf_of_isLimit` to show that the limit presheaf is indeed a sheaf.
 -/
CategoryTheory.Sheaf.isLimitMultiforkOfIsLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {D : Type w} →
        [inst_1 : CategoryTheory.Category.{w', w} D] →
          {K : Type z} →
            [inst_2 : CategoryTheory.Category.{z', z} K] →
              [CategoryTheory.Limits.HasLimitsOfShape K D] →
                (F : CategoryTheory.Functor K (CategoryTheory.Sheaf J D)) →
                  (E : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.sheafToPresheaf J D))) →
                    CategoryTheory.Limits.IsLimit E →
                      (X : C) → (W : J.Cover X) → CategoryTheory.Limits.IsLimit (W.multifork E.pt)
-- Mathlib.CategoryTheory.Category.Cat.Op
CategoryTheory.Cat.opFunctorInvolutive_inv_app_toFunctor_map : ∀ (X : CategoryTheory.Cat) {X_1 Y : ↑X} (f : X_1 ⟶ Y),
  (CategoryTheory.Cat.opFunctorInvolutive.inv.app X).toFunctor.map f = f.op.op
-- Mathlib.Analysis.InnerProductSpace.Adjoint
_private.Mathlib.Analysis.InnerProductSpace.Adjoint.0.ContinuousLinearMap.adjointAux_inner_left : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : CompleteSpace E] (A : E →L[𝕜] F) (x : E) (y : F),
  inner 𝕜 ((ContinuousLinearMap.adjointAux✝ A) y) x = inner 𝕜 y (A x)
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.rename_monomial : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] (f : σ → τ) (d : σ →₀ ℕ) (r : R),
  (MvPolynomial.rename f) ((MvPolynomial.monomial d) r) = (MvPolynomial.monomial (Finsupp.mapDomain f d)) r
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
ContinuousLinearEquiv.comp_right_hasFDerivWithinAt_iff' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : F → G} {s : Set F} {x : E}
  {f' : E →L[𝕜] G}, HasFDerivWithinAt (f ∘ ⇑iso) f' (⇑iso ⁻¹' s) x ↔ HasFDerivWithinAt f (f' ∘SL ↑iso.symm) s (iso x)
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
AlgebraicGeometry.Scheme.AffineZariskiSite.instIsCoverDenseOpensToOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat : ∀ {X : AlgebraicGeometry.Scheme},
  (AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor X).IsCoverDense (Opens.grothendieckTopology ↥X)
-- Mathlib.Order.CompleteLatticeIntervals
Set.Icc.coe_iInf : ∀ {ι : Sort u_1} {α : Type u_2} [inst : ConditionallyCompleteLattice α] {a b : α} (h : a ≤ b) [Nonempty ι]
  {S : ι → ↑(Set.Icc a b)},
  have this := ⋯;
  ↑(iInf S) = ⨅ i, ↑(S i)
-- Mathlib.Condensed.Discrete.Colimit
/-- The functor which takes a finite set to the set of maps into `F(*)` for a presheaf `F` on
`Profinite`.
 -/
Condensed.finYoneda : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1)) → CategoryTheory.Functor FintypeCatᵒᵖ (Type (u + 1))
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.Reachable.eq_1 : ∀ {V : Type u} (G : SimpleGraph V) (u v : V), G.Reachable u v = Nonempty (G.Walk u v)
-- Mathlib.Combinatorics.Enumerative.DyckWord
/-- The first element of a nonempty Dyck word is `U`.  -/
DyckWord.head_eq_U : ∀ (p : DyckWord) (h : ↑p ≠ []), (↑p).head h = DyckStep.U
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.mul_nc.induct_unfolding : ∀ (m₂ : Lean.Grind.CommRing.Mon) (motive : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Prop),
  motive Lean.Grind.CommRing.Mon.unit m₂ →
    (∀ (pw : Lean.Grind.CommRing.Power),
        motive (Lean.Grind.CommRing.Mon.mult pw Lean.Grind.CommRing.Mon.unit)
          (Lean.Grind.CommRing.Mon.mulPow_nc pw m₂)) →
      (∀ (pw : Lean.Grind.CommRing.Power) (m₁ : Lean.Grind.CommRing.Mon),
          (m₁ = Lean.Grind.CommRing.Mon.unit → False) →
            motive m₁ (m₁.mul_nc m₂) →
              motive (Lean.Grind.CommRing.Mon.mult pw m₁) (Lean.Grind.CommRing.Mon.mult pw (m₁.mul_nc m₂))) →
        ∀ (m₁ : Lean.Grind.CommRing.Mon), motive m₁ (m₁.mul_nc m₂)
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
Lean.Meta.Simp.Arith.Int.ToLinear.State : Type
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.id_f₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C),
  (CategoryTheory.CategoryStruct.id S).f₂ = CategoryTheory.CategoryStruct.id S.L₂
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instAddRightCancelSemigroupOfAddOpposite : {M : Type u_1} → [AddRightCancelSemigroup Mᵃᵒᵖ] → AddRightCancelSemigroup Mᵈᵃᵃ
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
Std.IterM.toList_toArray : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m β] [Std.Iterators.Finite α m]
  {it : Std.IterM m β}, Array.toList <$> it.toArray = it.toList
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.SupportsStmt.eq_def : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (S : Finset Λ) (x : Turing.TM1.Stmt Γ Λ σ),
  Turing.TM1.SupportsStmt S x =
    match x with
    | Turing.TM1.Stmt.move a q => Turing.TM1.SupportsStmt S q
    | Turing.TM1.Stmt.write a q => Turing.TM1.SupportsStmt S q
    | Turing.TM1.Stmt.load a q => Turing.TM1.SupportsStmt S q
    | Turing.TM1.Stmt.branch a q₁ q₂ => Turing.TM1.SupportsStmt S q₁ ∧ Turing.TM1.SupportsStmt S q₂
    | Turing.TM1.Stmt.goto l => ∀ (a : Γ) (v : σ), l a v ∈ S
    | Turing.TM1.Stmt.halt => True
-- Mathlib.RingTheory.Valuation.Integers
/-- Given a valuation v : R → Γ₀ and a ring homomorphism O →+* R, we say that O is the integers of v
if f is injective, and its range is exactly `v.integer`.  -/
Valuation.Integers : {R : Type u} →
  {Γ₀ : Type v} →
    [inst : CommRing R] →
      [inst_1 : LinearOrderedCommGroupWithZero Γ₀] →
        Valuation R Γ₀ → (O : Type w) → [inst_2 : CommRing O] → [Algebra O R] → Prop
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
SheafOfModules.GeneratingSections.localGeneratorsData_generators : ∀ {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]
  [inst_3 : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat]
  [inst_4 : CategoryTheory.Limits.HasBinaryProducts C]
  [inst_5 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R}
  (G : M.GeneratingSections) (x : C),
  G.localGeneratorsData.generators x =
    G.map (SheafOfModules.pushforward (CategoryTheory.CategoryStruct.id (R.over x)))
      (CategoryTheory.Iso.refl (SheafOfModules.unit (R.over x)))
-- Mathlib.Topology.Semicontinuity.Basic
/-- **Alias** of the reverse direction of `lowerSemicontinuouAt_inv_iff`. -/
UpperSemicontinuousAt.inv : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} {f : α → β} {a : α} [inst_1 : PartialOrder β]
  [inst_2 : CommGroup β] [IsOrderedMonoid β], UpperSemicontinuousAt f a → LowerSemicontinuousAt f⁻¹ a
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.HomRel.IsStableUnderPrecomp.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {r : HomRel C},
  (∀ {X Y Z : C} (f : X ⟶ Y) {g g' : Y ⟶ Z},
      r g g' → r (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp f g')) →
    CategoryTheory.HomRel.IsStableUnderPrecomp r
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- **Alias** of `QuadraticForm.toMatrix'`.

---

A matrix representation of a quadratic form `Q : QuadraticForm R (n → R)`.
See also `QuadraticForm.toMatrix` which gives the matrix in a given basis of a quadratic form on
an abstract vector space.  -/
QuadraticForm.QuadraticMap.toMatrix' : {R : Type u_3} →
  {n : Type w} →
    [Fintype n] → [DecidableEq n] → [inst : CommRing R] → [Invertible 2] → QuadraticForm R (n → R) → Matrix n n R
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.interSmallerFnₘ : {α : Type u} →
  {β : α → Type v} →
    [BEq α] →
      [Hashable α] →
        Std.DHashMap.Internal.Raw₀ α β → Std.DHashMap.Internal.Raw₀ α β → α → Std.DHashMap.Internal.Raw₀ α β
-- Mathlib.Algebra.Order.ZeroLEOne
ZeroLEOneClass.mk : ∀ {α : Type u_2} [inst : Zero α] [inst_1 : One α] [inst_2 : LE α], 0 ≤ 1 → ZeroLEOneClass α
-- Std.Async.Process
/-- Peak resident set size (max physical memory usage) in kilobytes
 -/
Std.IO.Process.ResourceUsageStats.peakResidentSetSizeKb : Std.IO.Process.ResourceUsageStats → UInt64