mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.zeroLocus_anti_mono : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {s t : Set A}, s ⊆ t → ProjectiveSpectrum.zeroLocus 𝒜 t ⊆ ProjectiveSpectrum.zeroLocus 𝒜 s
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.Key.bvar.inj : ∀ {deBruijnIndex nargs deBruijnIndex_1 nargs_1 : ℕ},
  Lean.Meta.RefinedDiscrTree.Key.bvar deBruijnIndex nargs =
      Lean.Meta.RefinedDiscrTree.Key.bvar deBruijnIndex_1 nargs_1 →
    deBruijnIndex = deBruijnIndex_1 ∧ nargs = nargs_1
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.denote_append : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] (ctx : Lean.Grind.Linarith.Context α)
  (p₁ p₂ : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.Poly.denote ctx (p₁.append p₂) =
    Lean.Grind.Linarith.Poly.denote ctx p₁ + Lean.Grind.Linarith.Poly.denote ctx p₂
-- Mathlib.Data.List.Dedup
List.Perm.dedup : ∀ {α : Type u_1} [inst : DecidableEq α] {l₁ l₂ : List α}, l₁.Perm l₂ → l₁.dedup.Perm l₂.dedup
-- Init.Data.Dyadic.Inv
/-- Divides two dyadic numbers at a given (maximum) precision.
Returns the greatest dyadic number with precision at most `prec` which is less than or equal
to `a/b`. For `b = 0`, returns `0`.
 -/
Dyadic.divAtPrec : Dyadic → Dyadic → ℤ → Dyadic
-- Mathlib.LinearAlgebra.Basis.Basic
Module.Basis.basis_singleton_iff : ∀ {R : Type u_7} {M : Type u_8} [inst : Ring R] [IsDomain R] [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [Module.IsTorsionFree R M] (ι : Type u_9) [Unique ι],
  Nonempty (Module.Basis ι R M) ↔ ∃ x, x ≠ 0 ∧ ∀ (y : M), ∃ r, r • x = y
-- Lean.ResolveName
Lean.ResolveName.backward.privateInPublic : Lean.Option Bool
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Subgroup.normal_op : ∀ {G : Type u_2} [inst : Group G] {H : Subgroup G}, H.op.Normal ↔ H.Normal
-- Mathlib.Topology.NhdsWithin
tendsto_nhdsWithin_iff_subtype : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {s : Set α} {a : α} (h : a ∈ s) (f : α → β) (l : Filter β),
  Filter.Tendsto f (nhdsWithin a s) l ↔ Filter.Tendsto (s.domRestrict f) (nhds ⟨a, h⟩) l
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.instConcreteCategoryAddMonoidHomCarrier.eq_1 : AddGrpCat.instConcreteCategoryAddMonoidHomCarrier =
  { hom := fun {X Y} => AddGrpCat.Hom.hom', ofHom := fun {X Y} => AddGrpCat.Hom.mk✝,
    hom_ofHom := @AddGrpCat.instConcreteCategoryAddMonoidHomCarrier._proof_1,
    ofHom_hom := @AddGrpCat.instConcreteCategoryAddMonoidHomCarrier._proof_2,
    id_apply := @AddGrpCat.instConcreteCategoryAddMonoidHomCarrier._proof_3,
    comp_apply := @AddGrpCat.instConcreteCategoryAddMonoidHomCarrier._proof_4 }
-- Lean.Parser.Term.Basic
/-- A `bracketedBinder` matches any kind of binder group that uses some kind of brackets:
* An explicit binder like `(x y : A)`
* An implicit binder like `{x y : A}`
* A strict implicit binder, `⦃y z : A⦄` or its ASCII alternative `{{y z : A}}`
* An instance binder `[A]` or `[x : A]` (multiple variables are not allowed here)
 -/
Lean.Parser.Term.bracketedBinder : optParam Bool false → Lean.Parser.Parser
-- Std.Sat.CNF.RelabelFin
Std.Sat.CNF.lt_numLiterals : ∀ {v : ℕ} {f : Std.Sat.CNF ℕ}, Std.Sat.CNF.VarMem v f → v < f.numLiterals
-- Mathlib.Algebra.Group.Finsupp
Finsupp.mapRange.addMonoidHom_toZeroHom : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] (f : M →+ N),
  ↑(Finsupp.mapRange.addMonoidHom f) = Finsupp.mapRange.zeroHom ↑f
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- `LinearEquiv.sumPiEquivProdPi` for `PiLp`, as an isometry.  -/
PiLp.sumPiLpEquivProdLpPiLp : {𝕜 : Type u_1} →
  [inst : Semiring 𝕜] →
    {ι : Type u_5} →
      {κ : Type u_6} →
        (p : ENNReal) →
          (α : ι ⊕ κ → Type u_7) →
            [inst_1 : Fintype ι] →
              [inst_2 : Fintype κ] →
                [inst_3 : Fact (1 ≤ p)] →
                  [inst_4 : (i : ι ⊕ κ) → SeminormedAddCommGroup (α i)] →
                    [inst_5 : (i : ι ⊕ κ) → Module 𝕜 (α i)] →
                      WithLp p ((i : ι ⊕ κ) → α i) ≃ₗᵢ[𝕜]
                        WithLp p (WithLp p ((i : ι) → α (Sum.inl i)) × WithLp p ((i : κ) → α (Sum.inr i)))
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.coequalizer.existsUnique : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasCoequalizer f g] {W : C} (k : Y ⟶ W),
  CategoryTheory.CategoryStruct.comp f k = CategoryTheory.CategoryStruct.comp g k →
    ∃! d, CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π f g) d = k
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.le_normalizer_closure_iff : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {s : Set G},
  H ≤ AddSubgroup.normalizer ↑(AddSubgroup.closure s) ↔ ∀ h ∈ H, ∀ g ∈ s, h + g + -h ∈ AddSubgroup.closure s
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.Hom.toAlgHom_X : ∀ {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 ι} {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [inst_3 : CommRing R']
  [inst_4 : CommRing S'] [inst_5 : Algebra R' S'] {P' : Algebra.Generators R' S' ι'} [inst_6 : Algebra R R']
  [inst_7 : Algebra S S'] (f : P.Hom P') (i : ι), f.toAlgHom (MvPolynomial.X i) = f.val i
-- Mathlib.AlgebraicGeometry.Birational.Birational
/-- The source open subscheme of a partial isomorphism.  -/
AlgebraicGeometry.Scheme.PartialIso.source : {X Y : AlgebraicGeometry.Scheme} → X.PartialIso Y → X.Opens
-- Mathlib.Geometry.Euclidean.NinePointCircle
Affine.Simplex.eulerPoint_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 : ℕ}
  (s : Affine.Simplex ℝ P n) (f : P →ᵃⁱ[ℝ] P₂) (i : Fin (n + 1)),
  (s.map f.toAffineMap ⋯).eulerPoint i = f (s.eulerPoint i)
-- Mathlib.Topology.Separation.Basic
Subtype.t1Space : ∀ {X : Type u} [inst : TopologicalSpace X] [T1Space X] {p : X → Prop}, T1Space (Subtype p)
-- Mathlib.Logic.Function.Defs
Function.snd_comp_prod : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} (f : ι → α) (g : ι → β), Prod.snd ∘ Function.prod f g = g
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.mulCayley_insert_one : ∀ {M : Type u_1} (s : Set M) [inst : MulOneClass M], SimpleGraph.mulCayley (insert 1 s) = SimpleGraph.mulCayley s
-- Mathlib.CategoryTheory.Sites.Plus
CategoryTheory.GrothendieckTopology.toPlus_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D}
  (η : P ⟶ Q) {Z : CategoryTheory.Functor Cᵒᵖ D} (h : J.plusObj Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp (J.toPlus Q) h) =
    CategoryTheory.CategoryStruct.comp (J.toPlus P) (CategoryTheory.CategoryStruct.comp (J.plusMap η) h)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
SheafOfModules.GeneratingSections.epi : ∀ {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] {M : SheafOfModules R} (self : M.GeneratingSections),
  CategoryTheory.Epi (M.freeHomEquiv.symm self.s)
-- Aesop.RuleTac.Cases
Aesop.CasesPattern.toExpr : Aesop.CasesPattern → Lean.MetaM Lean.Expr
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.toList_empty : ∀ {α : Type u}, ∅.toList = []
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.subtypeEquivToFinset_apply_coe : ∀ {α : Type u} {s : Set α} (hs : s.Finite) (a : { a // a ∈ s }), ↑(hs.subtypeEquivToFinset a) = ↑a
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapCycles₁_id_comp : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B C : Rep.{u, u, u} k G} (φ : A ⟶ B) (ψ : B ⟶ C),
  groupHomology.mapCycles₁ (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ) =
    CategoryTheory.CategoryStruct.comp (groupHomology.mapCycles₁ (MonoidHom.id G) φ)
      (groupHomology.mapCycles₁ (MonoidHom.id G) ψ)
-- Mathlib.Analysis.RCLike.Basic
RCLike.instOrderClosedTopology : ∀ {K : Type u_1} [inst : RCLike K], OrderClosedTopology K
-- Mathlib.Combinatorics.Hypergraph.Basic
/-- A hypergraph is nonempty if it has at least one vertex or at least one edge.  -/
Hypergraph.IsNonempty : {α : Type u_1} → Hypergraph α → Prop
-- Init.Grind.Ring.Field
Lean.Grind.Field.intCast_div_of_dvd : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] {x y : ℤ}, y ∣ x → ↑y ≠ 0 → ↑(x / y) = ↑x / ↑y
-- Mathlib.GroupTheory.GroupAction.Period
AddAction.period_eq_zero_iff : ∀ {α : Type v} {M : Type u} [inst : AddMonoid M] [inst_1 : AddAction M α] {m : M} {a : α},
  AddAction.period m a = 1 ↔ m +ᵥ a = a
-- Init.RCases
/-- A `@` before a tuple pattern as in `@⟨p1, p2, p3⟩` will bind all arguments in the constructor,
while leaving the `@` off will only use the patterns on the explicit arguments.
 -/
Lean.Parser.Tactic.rcasesPat.explicit : Lean.ParserDescr
-- Mathlib.Analysis.Analytic.Polynomial
AnalyticAt.aeval_polynomial : ∀ {𝕜 : Type u_1} {E : Type u_2} {A : Type u_3} {B : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : CommSemiring A] {z : E} [inst_4 : NormedRing B]
  [inst_5 : NormedAlgebra 𝕜 B] [inst_6 : Algebra A B] {f : E → B},
  AnalyticAt 𝕜 f z → ∀ (p : Polynomial A), AnalyticAt 𝕜 (fun x => (Polynomial.aeval (f x)) p) z
-- Mathlib.Algebra.Group.Hom.Defs
OneHom.mk_coe : ∀ {M : Type u_4} {N : Type u_5} [inst : One M] [inst_1 : One N] (f : OneHom M N) (h1 : f 1 = 1),
  { toFun := ⇑f, map_one' := h1 } = f
-- Lean.Elab.Quotation
_private.Lean.Elab.Quotation.0.Lean.Elab.Term.Quotation.findUsedAlts.go : Lean.NameMap ℕ → Lean.Syntax → StateRefT' IO.RealWorld Lean.Elab.Term.Quotation.IdxSet Lean.Elab.TermElabM Lean.Syntax
-- Mathlib.Tactic.DepRewrite
Mathlib.Tactic.DepRewrite.instBEqCastMode : BEq Mathlib.Tactic.DepRewrite.CastMode
-- Mathlib.Topology.PartitionOfUnity
BumpCovering.toPartitionOfUnity_eq_mul_prod : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι) (x : X)
  (t : Finset ι),
  (∀ (j : ι), WellOrderingRel j i → (f j) x ≠ 0 → j ∈ t) →
    (f.toPartitionOfUnity i) x = (f i) x * ∏ j ∈ t with WellOrderingRel j i, (1 - (f j) x)
-- Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_fromBiprod_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_3 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare)
  (F : CategoryTheory.Sheaf J AddCommGrpCat) (n : ℕ) {Z : AddCommGrpCat} (h : F.H' n S.X₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (S.toBiprod F n) (CategoryTheory.CategoryStruct.comp (S.fromBiprod F n) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
Matrix.toBilin'_toMatrix' : ∀ {R₁ : Type u_1} [inst : CommSemiring R₁] {n : Type u_5} [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  (B : LinearMap.BilinForm R₁ (n → R₁)), Matrix.toBilin' (LinearMap.BilinForm.toMatrix' B) = B
-- Std.Async.Select
_private.Std.Async.Select.0.Std.Async.shuffleIt.go.match_1.splitter : (motive : ℕ × StdGen → Sort u_1) → (x : ℕ × StdGen) → ((j : ℕ) → (gen : StdGen) → motive (j, gen)) → motive x
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_diff_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k : α}, k ∈ m₂ → (m₁ \ m₂).getKey! k = default
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.quasiIsoAt_unopFunctor_map_iff : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex Vᵒᵖ c} (φ : K ⟶ L) (i : ι)
  [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i],
  QuasiIsoAt ((HomologicalComplex.unopFunctor V c).map φ.op) i ↔ QuasiIsoAt φ i
-- Mathlib.Algebra.Order.Floor.Semifield
/-- Natural division is the floor of field division.  -/
Nat.floor_div_eq_div : ∀ {K : Type u_2} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [inst_3 : FloorSemiring K]
  (m n : ℕ), ⌊↑m / ↑n⌋₊ = m / n
-- Init.Data.List.Attach
/-- This lemma identifies folds over lists of subtypes, where the function only depends on the value, not the proposition,
and simplifies these to the function directly taking the value.
 -/
List.foldr_subtype : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {l : List { x // p x }} {f : { x // p x } → β → β} {g : α → β → β}
  {x : β}, (∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b) → List.foldr f x l = List.foldr g x l.unattach
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.closure_eq_top_of_mclosure_eq_top : ∀ {G : Type u_1} [inst : AddGroup G] {S : Set G}, AddSubmonoid.closure S = ⊤ → AddSubgroup.closure S = ⊤
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
jacobiTheta₂_term.eq_1 : ∀ (n : ℤ) (z τ : ℂ),
  jacobiTheta₂_term n z τ = Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * z + ↑Real.pi * Complex.I * ↑n ^ 2 * τ)
-- Mathlib.CategoryTheory.Linear.Yoneda
CategoryTheory.linearCoyoneda_obj_map : ∀ (R : Type w) [inst : Ring R] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] (Y : Cᵒᵖ) {X Y_1 : C} (f : X ⟶ Y_1),
  ((CategoryTheory.linearCoyoneda R C).obj Y).map f =
    ModuleCat.ofHom (CategoryTheory.Linear.rightComp R (Opposite.unop Y) f)
-- Std.Data.Iterators.Combinators.Monadic.StepSize
Std.Iterators.Types.StepSizeIterator : Type w → (Type w → Type w') → Type w → Type w
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
/-- `X.opcycles` also identifies to a kernel. More precisely,
`opZ(f, g)` identifies to the kernel of `H^n(f ≫ g) ⟶ H^n(g)`  -/
CategoryTheory.Abelian.SpectralObject.opcyclesIsoKernel : {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 : ι} →
              (f : i ⟶ j) →
                (g : j ⟶ k) →
                  (fg : i ⟶ k) →
                    (h : CategoryTheory.CategoryStruct.comp f g = fg) →
                      (n : ℤ) →
                        X.opcycles f g n ≅
                          CategoryTheory.Limits.kernel
                            ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h))
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- **Alias** of `CategoryTheory.Lax.LaxTrans.comp_naturality`. -/
CategoryTheory.Lax.LaxTrans.vComp_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {X Y Z : CategoryTheory.LaxFunctor B C} (η : CategoryTheory.Lax.LaxTrans X Y) (θ : CategoryTheory.Lax.LaxTrans Y Z)
  {a b : B} (f : a ⟶ b),
  (CategoryTheory.CategoryStruct.comp η θ).naturality f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (Z.map f)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (η.app a) (θ.naturality f))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (Y.map f) (θ.app b)).inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f) (θ.app b))
            (CategoryTheory.Bicategory.associator (X.map f) (η.app b) (θ.app b)).hom)))
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.coe_chainTopCoeff_eq_sSup : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι},
  LinearIndependent R ![P.root i, P.root j] →
    ↑(RootPairing.chainTopCoeff i j) = sSup {k | P.root j + k • P.root i ∈ Set.range ⇑P.root}
-- Lean.MetavarContext
/-- Substitutes assigned metavariables in `e` with their assigned value according to the
`MetavarContext`, recursively.

Example:
```
run_meta do
  let mvar1 ← mkFreshExprMVar (mkConst `Nat)
  let e := (mkConst `Nat.succ).app mvar1
  -- e is `Nat.succ ?m.773`, `?m.773` is unassigned
  mvar1.mvarId!.assign (mkNatLit 42)
  -- e is `Nat.succ ?m.773`, `?m.773` is assigned to `42`
  let e' ← instantiateMVars e
  -- e' is `Nat.succ 42`, `?m.773` is assigned to `42`
```

There are a few gotchas concerning delayed assignments.

* Regular assignments take precedence over delayed ones. This happens when an error occurs, in which
  case Lean assigns `sorry` to all unassigned metavariables, delayed assigned or not.
* Unless a delayed assigned metavariable `?m := fun fvars => ?pending` is fully applied to its free
  variables `fvars`, it will not be instantiated to `?pending`.
* A delayed assigned metavariable `?m := fun fvars => ?pending` that occurs fully applied `?m fvars`
  will not be instantiated to `?pending` unless (1) `?pending` is assigned, and (2) the
  assignment to `?pending` is ground (i.e., does not contain unassigned metavariables).
 -/
Lean.instantiateMVars : {m : Type → Type} → [Monad m] → [Lean.MonadMCtx m] → Lean.Expr → m Lean.Expr
-- Mathlib.Order.Antichain
/-- **Alias** of `setOfPred_maximal_antichain`. -/
setOf_maximal_antichain : ∀ {α : Type u_1} [inst : PartialOrder α] (P : α → Prop), IsAntichain (fun x1 x2 => x1 ≤ x2) {x | Maximal P x}
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_le_mul_of_nonpos_of_nonneg : ∀ {R : Type u} [inst : Semiring R] [inst_1 : Preorder R] {a b c d : R} [ExistsAddOfLE R] [MulPosMono R] [PosMulMono R]
  [AddRightMono R] [AddRightReflectLE R], a ≤ c → d ≤ b → c ≤ 0 → 0 ≤ b → a * b ≤ c * d
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.continuous_equivIoc_symm : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜) [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [hp : Fact (0 < p)] (a : 𝕜) [inst_3 : Archimedean 𝕜] [inst_4 : TopologicalSpace 𝕜],
  Continuous ⇑(AddCircle.equivIoc p a).symm
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
/-- The codomain of the isomorphism  -/
CategoryTheory.WalkingIso.one : CategoryTheory.WalkingIso
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.degree_derivative_eq : ∀ {R : Type u} [inst : Semiring R] [IsAddTorsionFree R] (p : Polynomial R),
  0 < p.natDegree → (Polynomial.derivative p).degree = ↑(p.natDegree - 1)
-- Mathlib.Data.Set.Semiring
SetSemiring.instIdemCommSemiringOfCommMonoid : {α : Type u_1} → [CommMonoid α] → IdemCommSemiring (SetSemiring α)
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.coe_compTendsto : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} (f : α → β) {lc : Filter γ} {g : γ → α}
  (hg : Filter.Tendsto g lc l), (↑f).compTendsto g hg = ↑(f ∘ g)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.ElementarilyEquivalent.realize_sentence : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N],
  L.ElementarilyEquivalent M N → ∀ (φ : L.Sentence), M ⊨ φ ↔ N ⊨ φ
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Replicate
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Replicate.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastReplicate.aux1 : ∀ {a b c : ℕ}, b < a * c → 0 < a
-- Mathlib.CategoryTheory.Limits.Types.Products
/-- The category of types has `X × Y`, the usual Cartesian product,
as the binary product of `X` and `Y`.
 -/
CategoryTheory.Limits.Types.binaryProductLimitCone : (X Y : Type u) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)
-- Mathlib.Data.Fin.Fin2
/-- Ex falso. The dependent eliminator for the empty `Fin2 0` type.  -/
Fin2.elim0 : {C : Fin2 0 → Sort u} → (i : Fin2 0) → C i
-- Mathlib.NumberTheory.RamificationInertia.Basic
Ideal.card_primesOverFinset_le_finrank : ∀ {R : Type u} [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsDedekindDomain S] (K : Type u_1) (L : Type u_2) [inst_4 : Field K] [inst_5 : Field L] [IsDedekindDomain R]
  [inst_7 : Algebra R K] [IsFractionRing R K] [inst_9 : Algebra S L] [IsFractionRing S L] [inst_11 : Algebra K L]
  [inst_12 : Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [Module.Finite R S] [NoZeroSMulDivisors R S]
  {p : Ideal R} [p.IsMaximal], p ≠ ⊥ → (IsDedekindDomain.primesOverFinset p S).card ≤ Module.finrank K L
-- Mathlib.Algebra.Group.Submonoid.Finsupp
/-- A variant of `AddSubmonoid.mem_closure_finset` using `s` as the index type.  -/
AddSubmonoid.mem_closure_finset' : ∀ {M : Type u_1} [inst : AddCommMonoid M] {x : M} {s : Finset M}, x ∈ AddSubmonoid.closure ↑s ↔ ∃ a, x = ∑ i, a i • ↑i
-- Lean.Environment
Lean.Kernel.isDefEqGuarded : Lean.Environment → Lean.LocalContext → Lean.Expr → Lean.Expr → Bool
-- Std.Async.Basic
/-- Starts an asynchronous computation in another monad.
 -/
Std.Async.MonadAsync.async : {t m : Type → Type} →
  [self : Std.Async.MonadAsync t m] → {α : Type} → m α → optParam Task.Priority Task.Priority.default → m (t α)
-- Mathlib.Analysis.Calculus.VectorField
VectorField.lieBracket.eq_1 : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (V W : E → E) (x : E),
  VectorField.lieBracket 𝕜 V W x = (fderiv 𝕜 W x) (V x) - (fderiv 𝕜 V x) (W x)
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.commute_X : ∀ {R : Type u_1} [inst : Semiring R] (φ : PowerSeries R), Commute φ PowerSeries.X
-- Mathlib.Algebra.Lie.Abelian
LieModule.instIsTrivialOfSubsingleton' : ∀ {L : Type u_1} {M : Type u_2} [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M]
  [Subsingleton M], LieModule.IsTrivial L M
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof.erase_dup.sizeOf_spec : ∀ (c : Lean.Meta.Grind.AC.DiseqCnstr), sizeOf (Lean.Meta.Grind.AC.DiseqCnstrProof.erase_dup c) = 1 + sizeOf c
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ring.DimensionLeOne.prime_le_prime_iff_eq : ∀ {R : Type u_1} [inst : CommRing R] [Ring.DimensionLEOne R] {P Q : Ideal R} [hP : P.IsPrime] [hQ : Q.IsPrime],
  P ≠ ⊥ → (P ≤ Q ↔ P = Q)
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.mk.inj : ∀ {X : Type u_7} {Y : Type u_8} {inst : TopologicalSpace X} {inst_1 : TopologicalSpace Y}
  {toPartialHomeomorph : PartialHomeomorph X Y} {open_source : IsOpen toPartialHomeomorph.source}
  {open_target : IsOpen toPartialHomeomorph.target} {toPartialHomeomorph_1 : PartialHomeomorph X Y}
  {open_source_1 : IsOpen toPartialHomeomorph_1.source} {open_target_1 : IsOpen toPartialHomeomorph_1.target},
  { toPartialHomeomorph := toPartialHomeomorph, open_source := open_source, open_target := open_target } =
      { toPartialHomeomorph := toPartialHomeomorph_1, open_source := open_source_1, open_target := open_target_1 } →
    toPartialHomeomorph = toPartialHomeomorph_1
-- Mathlib.Data.Set.Image
Set.image_sdiff_subset : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s t : Set α), f '' (s \ t) ⊆ f '' s ∩ f '' tᶜ
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.yonedaMap_app_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v₁, u_1} D] (F : CategoryTheory.Functor C D) {Y : C} {X : Cᵒᵖ}
  (f : Opposite.unop X ⟶ Y), (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.yonedaMap F Y).app X)) f = F.map f