mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.HasModel.succMany?_encode : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] {β : Type v} [inst_2 : LE β] [inst_3 : LT β]
  [inst_4 : Std.PRange.UpwardEnumerable β] [inst_5 : Std.PRange.LawfulUpwardEnumerable β]
  [inst_6 : Std.PRange.LawfulUpwardEnumerableLE β] [inst_7 : Std.PRange.LawfulUpwardEnumerableLT β] {n' : ℕ}
  [m : HasModel✝ α β] {x : α},
  Std.PRange.succMany? n' (HasModel.encode✝ x) = Option.map HasModel.encode✝ (Std.PRange.succMany? n' x)
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.mem_bot : ∀ {G : Type u_1} [inst : Group G] {x : G}, x ∈ ⊥ ↔ x = 1
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.sum_excenterWeights_eq_one_iff : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) {signs : Finset (Fin (n + 1))},
  ∑ i, s.excenterWeights signs i = 1 ↔ s.ExcenterExists signs
-- Mathlib.Data.Sum.Interval
Sum.Lex.Icc_inl_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] [inst_4 : LocallyFiniteOrderTop α] [inst_5 : LocallyFiniteOrderBot β] (a : α) (b : β),
  Finset.Icc (Sum.inlₗ a) (Sum.inrₗ b) = Finset.map toLex.toEmbedding ((Finset.Ici a).disjSum (Finset.Iic b))
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.stdSimplex.spineId_arrow_apply_zero : ∀ (n : ℕ) (i : Fin n), ((SSet.stdSimplex.spineId n).arrow i) 0 = i.castSucc
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.completeBasis.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.fundamentalCone.completeBasis K = basisOfLinearIndependentOfCardEqFinrank ⋯ ⋯
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
/-- The bifibrant resolution functor from the category of cofibrant objects
to the homotopy category of bifibrant objects.  -/
HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      CategoryTheory.Functor (HomotopicalAlgebra.CofibrantObject C) (HomotopicalAlgebra.BifibrantObject.HoCat C)
-- Mathlib.Algebra.Polynomial.Div
Polynomial.le_rootMultiplicity_mul : ∀ {R : Type u} [inst : CommRing R] {p q : Polynomial R} (x : R),
  p * q ≠ 0 → Polynomial.rootMultiplicity x p + Polynomial.rootMultiplicity x q ≤ Polynomial.rootMultiplicity x (p * q)
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.dropInfix?.go.match_1.splitter : {α : Type u_1} →
  (motive : Option (List α) → Sort u_2) →
    (x : Option (List α)) → (Unit → motive none) → ((s : List α) → motive (some s)) → motive x
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel'.trans : {R : Type u} →
  [inst : Rack R] →
    {a b c : Rack.PreEnvelGroup R} →
      Rack.PreEnvelGroupRel' R a b → Rack.PreEnvelGroupRel' R b c → Rack.PreEnvelGroupRel' R a c
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.self_add_star : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [inst : CommRing R],
  a + star a = 2 * ↑a.re + ↑c₂ * ↑a.imI
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.toFun_eq_coe : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α →ᵈ β}, f.toFun = ⇑f
-- Mathlib.Data.Finsupp.Basic
Finsupp.filter_eq_zero_iff : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (p : α → Prop) [inst_1 : DecidablePred p] (f : α →₀ M),
  Finsupp.filter p f = 0 ↔ ∀ (x : α), p x → f x = 0
-- Mathlib.MeasureTheory.Measure.NullMeasurable
/-- A set is called `NullMeasurableSet` if it can be approximated by a measurable set up to
a set of null measure.  -/
MeasureTheory.NullMeasurableSet : {α : Type u_2} →
  [inst : MeasurableSpace α] →
    Set α → autoParam (MeasureTheory.Measure α) MeasureTheory.NullMeasurableSet._auto_1 → Prop
-- Lean.Meta.Basic
Lean.Meta.Config.mk : Bool →
  Bool →
    Bool →
      Bool →
        Bool →
          Bool →
            Bool →
              Bool →
                Bool →
                  Lean.Meta.TransparencyMode →
                    Lean.Meta.EtaStructMode →
                      Bool → Bool → Bool → Lean.Meta.ProjReductionKind → Bool → Bool → Bool → Bool → Lean.Meta.Config
-- Lean.Data.Lsp.Workspace
Lean.Lsp.instToJsonWorkspaceFolder : Lean.ToJson Lean.Lsp.WorkspaceFolder
-- Mathlib.Data.Nat.BitIndices
/-- **Alias** of `Nat.sum_map_two_pow_bitIndices`. -/
Nat.twoPowSum_bitIndices : ∀ (n : ℕ), (List.map (fun i => 2 ^ i) n.bitIndices).sum = n
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.card_ord : ∀ (c : Cardinal.{u_1}), c.ord.card = c
-- Mathlib.Algebra.Homology.Embedding.Connect
_private.Mathlib.Algebra.Homology.Embedding.Connect.0.CochainComplex.ConnectData.d.match_1.eq_1 : ∀ (motive : ℤ → ℤ → Sort u_1) (n m : ℕ) (h_1 : (n m : ℕ) → motive (Int.ofNat n) (Int.ofNat m))
  (h_2 : (n m : ℕ) → motive (Int.negSucc n) (Int.negSucc m)) (h_3 : Unit → motive (Int.negSucc 0) (Int.ofNat 0))
  (h_4 : (a a_1 : ℕ) → motive (Int.ofNat a) (Int.negSucc a_1))
  (h_5 : (a a_1 : ℕ) → motive (Int.negSucc a) (Int.ofNat a_1)),
  (match Int.ofNat n, Int.ofNat m with
    | Int.ofNat n, Int.ofNat m => h_1 n m
    | Int.negSucc n, Int.negSucc m => h_2 n m
    | Int.negSucc 0, Int.ofNat 0 => h_3 ()
    | Int.ofNat a, Int.negSucc a_1 => h_4 a a_1
    | Int.negSucc a, Int.ofNat a_1 => h_5 a a_1) =
    h_1 n m
-- Mathlib.Topology.Neighborhoods
/-- **Alias** of `isOpen_setOfPred_eventually_nhds`. -/
isOpen_setOf_eventually_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {p : X → Prop}, IsOpen {x | ∀ᶠ (y : X) in nhds x, p y}
-- Mathlib.GroupTheory.PushoutI
/-- The map from each indexing group into the pushout  -/
Monoid.PushoutI.of : {ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Monoid (G i)] →
        [inst_1 : Monoid H] → {φ : (i : ι) → H →* G i} → (i : ι) → G i →* Monoid.PushoutI φ
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.listProd : ∀ {R : Type u_1} [inst : Semiring R] {l : List (Polynomial R)}, (∀ f ∈ l, f.Splits) → l.prod.Splits
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.Hom.liftQuotient.eq_1 : ∀ {X : AlgebraicGeometry.Scheme} {A : CommRingCat} (f : X.Hom (AlgebraicGeometry.Spec A)) (I : Ideal ↑A)
  (hI :
    I ≤
      RingHom.ker
        (CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso A).inv f.appTop))),
  f.liftQuotient I hI =
    CategoryTheory.CategoryStruct.comp X.toSpecΓ
      (AlgebraicGeometry.Spec.map
        (CommRingCat.ofHom
          (Ideal.Quotient.lift I
            (CommRingCat.Hom.hom
              (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso A).inv f.appTop))
            hI)))
-- Init.Data.List.Basic
/-- Auxiliary for `List.reverse`. `List.reverseAux l r = l.reverse ++ r`, but it is defined directly.  -/
List.reverseAux : {α : Type u} → List α → List α → List α
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.isoInv_hom_id_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory}
  (e : X ≅ Y) {Z : C} (h : Y.obj ⟶ Z),
  CategoryTheory.CategoryStruct.comp e.inv.hom (CategoryTheory.CategoryStruct.comp e.hom.hom h) = h
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveElabStep1.view : Lean.Elab.Command.InductiveElabStep1 → Lean.Elab.Command.InductiveView
-- Mathlib.Algebra.CubicDiscriminant
/-- Convert a cubic polynomial to a polynomial.  -/
Cubic.toPoly : {R : Type u_1} → [inst : Semiring R] → Cubic R → Polynomial R
-- Mathlib.Algebra.Polynomial.CoeffMem
Polynomial.coeff_divModByMonicAux_mem_span_pow_mul_span : ∀ {R : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (p q : Polynomial S)
  (hq : q.Monic) (i : ℕ),
  (p.divModByMonicAux hq).1.coeff i ∈
      (1 ⊔ Submodule.span R (Set.range q.coeff)) ^ p.natDegree * (1 ⊔ Submodule.span R (Set.range p.coeff)) ∧
    (p.divModByMonicAux hq).2.coeff i ∈
      (1 ⊔ Submodule.span R (Set.range q.coeff)) ^ p.natDegree * (1 ⊔ Submodule.span R (Set.range p.coeff))
-- Mathlib.Tactic.Linarith.Preprocessing
/-- Removes any expressions that are not proofs of inequalities, equalities, or negations thereof.
Negations are pushed into inequalities when possible.
 -/
Mathlib.Tactic.Linarith.filterComparisons : Mathlib.Tactic.Linarith.Preprocessor
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.T_nonneg : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r) (n : ℕ), 0 ≤ T n
-- Mathlib.LinearAlgebra.Basis.Fin
Module.Basis.coe_mkFinConsOfLE : ∀ {R : Type u_3} {M : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {n : ℕ}
  {N O : Submodule R M} (y : M) (yO : y ∈ O) (b : Module.Basis (Fin n) R ↥N) (hNO : N ≤ O)
  (hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0) (hsp : ∀ z ∈ O, ∃ c, z + c • y ∈ N),
  ⇑(Module.Basis.mkFinConsOfLE y yO b hNO hli hsp) = Fin.cons ⟨y, yO⟩ (⇑(Submodule.inclusion hNO) ∘ ⇑b)
-- Mathlib.Order.SupClosed
isLUB_supClosure : ∀ {α : Type u_3} [inst : SemilatticeSup α] {s : Set α} {a : α}, IsLUB (supClosure s) a ↔ IsLUB s a
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsPos.of_tail : ∀ {hd : ℝ} {tl : Tactic.ComputeAsymptotics.UnitMonomial},
  hd = 0 → tl.FirstNonzeroIsPos → Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsPos (hd :: tl)
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
CategoryTheory.Limits.Types.Pushout.Rel.inl_inr : ∀ {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} (s : S),
  CategoryTheory.Limits.Types.Pushout.Rel f g (Sum.inl ((CategoryTheory.ConcreteCategory.hom f) s))
    (Sum.inr ((CategoryTheory.ConcreteCategory.hom g) s))
-- Mathlib.Order.SetAccumulate
Set.mem_accumulate : ∀ {α : Type u_1} {β : Type u_2} {s : α → Set β} [inst : LE α] {x : α} {z : β}, z ∈ Set.accumulate s x ↔ ∃ y ≤ x, z ∈ s y
-- Init.Data.Int.Basic
/-- The canonical map `Int → R`.  -/
IntCast.intCast : {R : Type u} → [self : IntCast R] → ℤ → R
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.repr_reindex_apply : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (b : Module.Basis ι R M) (x : M) (e : ι ≃ ι') (i' : ι'),
  ((b.reindex e).repr x) i' = (b.repr x) (e.symm i')
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Ideal.IsHomogeneous.mem_iff : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] (𝒜 : ι → σ) [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι] [inst_5 : GradedRing 𝒜]
  {I : Ideal A}, Ideal.IsHomogeneous 𝒜 I → ∀ {x : A}, x ∈ I ↔ ∀ (i : ι), ↑(((DirectSum.decompose 𝒜) x) i) ∈ I
-- Mathlib.Data.PNat.Basic
PNat.natPred_add_one : ∀ (n : ℕ+), n.natPred + 1 = ↑n
-- Mathlib.CategoryTheory.Widesubcategory
CategoryTheory.wideInducedFunctor_map : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} D] (F : C → D)
  (P : CategoryTheory.MorphismProperty D) [inst_1 : P.IsMultiplicative]
  {x x_1 : CategoryTheory.InducedWideCategory D F P} (f : x ⟶ x_1),
  (CategoryTheory.wideInducedFunctor F P).map f = f.hom
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.mk.sizeOf_spec : ∀ {α : Type u_5} {β : Type u_6} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
  [inst_2 : SizeOf α] [inst_3 : SizeOf β] (toMulHom : α →ₙ* β) (map_zero' : toMulHom.toFun 0 = 0)
  (map_add' : ∀ (x y : α), toMulHom.toFun (x + y) = toMulHom.toFun x + toMulHom.toFun y),
  sizeOf { toMulHom := toMulHom, map_zero' := map_zero', map_add' := map_add' } = 1 + sizeOf toMulHom + sizeOf map_zero'
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} {X Y : C} {p : X ⟶ Y} {f : F.obj ⊥ ⟶ X}
  {g : c.pt ⟶ Y} {j : J} (sq' : CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct c p f g j),
  CategoryTheory.CategoryStruct.comp f p = CategoryTheory.CategoryStruct.comp (c.ι.app ⊥) g
-- Mathlib.Order.RelIso.Basic
RelIso.toEquiv_injective : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop}, Function.Injective RelIso.toEquiv
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanShape.mk.sizeOf_spec : ∀ (L : Type w) (R : Type w') (fst snd : R → L),
  sizeOf { L := L, R := R, fst := fst, snd := snd } = 1 + sizeOf L + sizeOf R
-- Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.Preprocessor.mk.inj : ∀ {toPreprocessorBase : Mathlib.Tactic.Linarith.PreprocessorBase} {transform : Lean.Expr → Lean.MetaM (List Lean.Expr)}
  {toPreprocessorBase_1 : Mathlib.Tactic.Linarith.PreprocessorBase}
  {transform_1 : Lean.Expr → Lean.MetaM (List Lean.Expr)},
  { toPreprocessorBase := toPreprocessorBase, transform := transform } =
      { toPreprocessorBase := toPreprocessorBase_1, transform := transform_1 } →
    toPreprocessorBase = toPreprocessorBase_1 ∧ transform = transform_1
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.rfl : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp}, t.Equiv t
-- Init.Data.List.Pairwise
List.pairwise_and_iff : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α} {S : α → α → Prop},
  List.Pairwise (fun a b => R a b ∧ S a b) l ↔ List.Pairwise R l ∧ List.Pairwise S l
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
TateCohomology.map_tateComplexFunctor_shortExact : ∀ {R G : Type u} [inst : CommRing R] [inst_1 : Group G] [inst_2 : Fintype G]
  {S : CategoryTheory.ShortComplex (Rep.{u, u, u} R G)}, S.ShortExact → (S.map (tateComplexFunctor R G)).ShortExact
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintKind.type.sizeOf_spec : sizeOf Lean.Lsp.InlayHintKind.type = 1
-- Init.Data.Sum.Basic
/-- `inl a` and `inr b` are always related via `Lex r s`.  -/
Sum.Lex.sep : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (a : α) (b : β),
  Sum.Lex r s (Sum.inl a) (Sum.inr b)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey!_eq_getLast!_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t.maxKey! = t.keys.getLast!
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.tan_pi_div_two_sub : ∀ (x : ℝ), Real.tan (Real.pi / 2 - x) = (Real.tan x)⁻¹
-- Init.Data.Int.Order
Int.natAbs_negOfNat : ∀ (n : ℕ), (Int.negOfNat n).natAbs = n
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasLimit.isoOfNatIso_hom_π : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F]
  [inst_3 : CategoryTheory.Limits.HasLimit G] (w : F ≅ G) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.HasLimit.isoOfNatIso w).hom
      (CategoryTheory.Limits.limit.π G j) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j) (w.hom.app j)
-- Mathlib.CategoryTheory.Filtered.Basic
/-- for every pair of objects there exists another object "to the right"  -/
CategoryTheory.IsFilteredOrEmpty.cocone_objs : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.IsFilteredOrEmpty C] (X Y : C),
  ∃ Z x x, True
-- Mathlib.LinearAlgebra.LinearDisjoint
Submodule.LinearDisjoint.val_mulMap_tmul : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M N : Submodule R S}
  (H : M.LinearDisjoint N) (m : ↥M) (n : ↥N), ↑(H.mulMap (m ⊗ₜ[R] n)) = ↑m * ↑n
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.apply : ∀ {K : Type u_1} [inst : Field K] (φ : K →+* ℂ) (x : K), (NumberField.InfinitePlace.mk φ) x = ‖φ x‖
-- Mathlib.Analysis.SpecialFunctions.Log.ERealExp
EReal.exp_le_one_iff : ∀ {a : EReal}, a.exp ≤ 1 ↔ a ≤ 0
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
CategoryTheory.Precoverage.SubsheafClosure.brecOn : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))}
  {motive : (Z : C) → (a : F.obj (Opposite.op Z)) → K.SubsheafClosure 𝒮 Z a → Prop} {Z : C} {a : F.obj (Opposite.op Z)}
  (t : K.SubsheafClosure 𝒮 Z a),
  (∀ (Z : C) (a : F.obj (Opposite.op Z)) (t : K.SubsheafClosure 𝒮 Z a),
      CategoryTheory.Precoverage.SubsheafClosure.below t → motive Z a t) →
    motive Z a t
-- Mathlib.Data.Finset.Max
Finset.max'_insert : ∀ {α : Type u_2} [inst : LinearOrder α] (a : α) (s : Finset α) (H : s.Nonempty), (insert a s).max' ⋯ = max a (s.max' H)
-- Mathlib.Order.WithBotTop
WithBotTop.coe_monotone : ∀ {ι : Type u_1} [inst : Preorder ι], Monotone WithBotTop.coe
-- Init.Data.UInt.Bitwise
USize.neg_eq_not_add : ∀ (a : USize), -a = ~~~a + 1
-- Mathlib.LinearAlgebra.QuadraticForm.AlgClosed
/-- A nondegenerate quadratic form on an algebraically closed field of characteristic not equal to 2
is equivalent to the sum of squares, i.e. `weightedSumSquares` with weight `fun (i : ι) => 1`.  -/
QuadraticForm.equivalent_weightedSumSquares_of_isAlgClosed : ∀ {K : Type u_2} [inst : Field K] [IsAlgClosed K] [inst_2 : Invertible 2] {M : Type u_3} [inst_3 : AddCommGroup M]
  [inst_4 : Module K M] [FiniteDimensional K M] (Q : QuadraticForm K M),
  LinearMap.SeparatingLeft (QuadraticMap.associated Q) → QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares K 1)
-- Mathlib.FieldTheory.Relrank
IntermediateField.relfinrank_self : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (A : IntermediateField F E),
  A.relfinrank A = 1
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Valuation.exists_setOfPred_restrict_le_iff : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_2} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  (v : Valuation R Γ₀) [v.Compatible] (x : R) (s : Set R),
  (∃ γ, {z | v.restrict (z - x) < ↑γ} ⊆ s) ↔ ∃ γ, {a | (ValuativeRel.valuation R) (a - x) < ↑γ} ⊆ s
-- Mathlib.Topology.Instances.Rat
Nat.isUniformEmbedding_coe_rat : IsUniformEmbedding Nat.cast
-- Mathlib.SetTheory.ZFC.Basic
/-- Induction on the `∈` relation.  -/
ZFSet.inductionOn : ∀ {p : ZFSet.{u_1} → Prop} (x : ZFSet.{u_1}), (∀ (x : ZFSet.{u_1}), (∀ y ∈ x, p y) → p x) → p x
-- Mathlib.Algebra.Field.Rat
Rat.instField : Field ℚ
-- Mathlib.FieldTheory.Galois.Basic
IsGalois.IntermediateField.AdjoinSimple.card_aut_eq_finrank : ∀ (F : Type u_1) [inst : Field F] (E : Type u_2) [inst_1 : Field E] [inst_2 : Algebra F E] [FiniteDimensional F E]
  {α : E},
  IsIntegral F α →
    IsSeparable F α →
      (Polynomial.map (algebraMap F ↥F⟮α⟯) (minpoly F α)).Splits → Nat.card Gal(↥F⟮α⟯/F) = Module.finrank F ↥F⟮α⟯
-- Mathlib.Algebra.Group.Subsemigroup.Basic
/-- `closure` forms a Galois insertion with the coercion to set.  -/
AddSubsemigroup.gi : (M : Type u_1) → [inst : Add M] → GaloisInsertion AddSubsemigroup.closure SetLike.coe
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.mul : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Mul β]
  [ContinuousMul β],
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable (f * g)
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- One can reformulate being `C^n` on a set as continuity on this set, and being `C^n` in any
extended chart in the target.  -/
contMDiffOn_iff_target : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M}
  {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold I' n M'],
  ContMDiffOn I I' n f s ↔
    ContinuousOn f s ∧
      ∀ (y : M'),
        ContMDiffOn I (modelWithCornersSelf 𝕜 E') n (↑(extChartAt I' y) ∘ f) (s ∩ f ⁻¹' (extChartAt I' y).source)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
/-- The Weierstrass curve in Jacobian coordinates mapped over a ring homomorphism `f : R →+* S`.  -/
WeierstrassCurve.Jacobian.map : {R : Type r} →
  [inst : CommRing R] →
    WeierstrassCurve.Jacobian R → {S : Type s} → [inst_1 : CommRing S] → (R →+* S) → WeierstrassCurve.Jacobian S
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.exists_measurable_le_withDensity_eq : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] (f : α → ENNReal),
  ∃ g, Measurable g ∧ g ≤ f ∧ μ.withDensity g = μ.withDensity f
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.mem_center_iff : ∀ {R : Type u_1} [inst : Semiring R] {z : R}, z ∈ Subsemiring.center R ↔ ∀ (g : R), g * z = z * g
-- Init.Data.Int.DivMod.Lemmas
Int.le_ediv_iff_of_dvd_of_pos : ∀ {a b c : ℤ}, 0 < c → c ∣ b → (a ≤ b / c ↔ c * a ≤ b)
-- Lean.Expr
Lean.FVarId.mk.sizeOf_spec : ∀ (name : Lean.Name), sizeOf { name := name } = 1 + sizeOf name
-- Mathlib.Algebra.Module.Torsion.Free
smul_ne_zero_iff_right : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {r : R} {m : M}
  [Module.IsTorsionFree R M] [IsCancelMulZero R], r ≠ 0 → (r • m ≠ 0 ↔ m ≠ 0)
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- A left Kan extension of `g` along `f` is an initial object in `LeftExtension f g`.  -/
CategoryTheory.Bicategory.LeftExtension.IsKan : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} → {f : a ⟶ b} → {g : a ⟶ c} → CategoryTheory.Bicategory.LeftExtension f g → Type (max (max v w) w)
-- Mathlib.Computability.TuringMachine.Computable
Turing.inhabitedTM2Outputs : Inhabited
  (Turing.TM2Outputs (Turing.idComputer Bool) (List.map (Equiv.cast ⋯).invFun [false])
    (some (List.map (Equiv.cast ⋯).invFun [false])))
-- Lean.Meta.Tactic.Grind.EMatchTheoremParam
Lean.Meta.Grind.globalDeclToGrindParamSyntax : Lean.Name → Lean.Meta.Grind.EMatchTheoremKind → Bool → Lean.MetaM (Lean.TSyntax `Lean.Parser.Tactic.grindParam)
-- Mathlib.Algebra.Group.End
/-- **Alias** of `AddAut.zero_apply`. -/
AddAut.one_apply : ∀ (M : Type u_2) [inst : Add M] (m : M), 0 m = m
-- Init.Data.List.OfFn
List.getElem_ofFn : ∀ {n : ℕ} {α : Type u_1} {i : ℕ} {f : Fin n → α} (h : i < (List.ofFn f).length), (List.ofFn f)[i] = f ⟨i, ⋯⟩
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
IsIntegrallyClosed.of_equiv : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (f : R ≃+* S) [h : IsIntegrallyClosed R],
  IsIntegrallyClosed S
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.rightUnitor.eq_1 : ∀ (a : SimplexCategory),
  AugmentedSimplexCategory.rightUnitor (CategoryTheory.WithInitial.of a) =
    CategoryTheory.Iso.refl
      (AugmentedSimplexCategory.tensorObj (CategoryTheory.WithInitial.of a) AugmentedSimplexCategory.tensorUnit)
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
AbsolutelyContinuousOnInterval.disjWithin_comm : ∀ (a b : ℝ), AbsolutelyContinuousOnInterval.disjWithin a b = AbsolutelyContinuousOnInterval.disjWithin b a
-- Mathlib.Algebra.Category.Grp.Biproducts
/-- We verify that the biproduct we've just defined is isomorphic to the `AddCommGrpCat` structure
on the dependent function type.
 -/
AddCommGrpCat.biproductIsoPi : {J : Type} → [inst : Finite J] → (f : J → AddCommGrpCat) → ⨁ f ≅ AddCommGrpCat.of ((j : J) → ↑(f j))