mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.BifunctorFlip
HomologicalComplex.instHasMapBifunctorFlip : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [inst_8 : TotalComplexShape c₁ c₂ c]
  [inst_9 : TotalComplexShape c₂ c₁ c] [TotalComplexShapeSymmetry c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c],
  K₂.HasMapBifunctor K₁ F.flip c
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.hom_ext : ∀ {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.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  {X Y : CategoryTheory.Triangulated.SpectralObject C ι} {α β : X ⟶ Y}, α.hom = β.hom → α = β
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.instSMulCommClass : ∀ (X : Type u_2) {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring A] [inst_3 : Algebra R A] [inst_4 : Algebra S A], SMulCommClass R S (FreeAlgebra A X)
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.lift_cRank_submatrix_le : ∀ {m : Type um} {m₀ : Type um₀} {n : Type un} {n₀ : Type un₀} {R : Type uR} [inst : Semiring R] (A : Matrix m n R)
  (r : m₀ → m) (c : n₀ → n),
  Cardinal.lift.{um, max uR um₀} (A.submatrix r c).cRank ≤ Cardinal.lift.{um₀, max uR um} A.cRank
-- Mathlib.AlgebraicGeometry.QuasiAffine
/-- The affine basic opens of a quasi-affine scheme form an open cover.  -/
AlgebraicGeometry.Scheme.openCoverBasicOpenTop : (X : AlgebraicGeometry.Scheme) → [X.IsQuasiAffine] → X.OpenCover
-- Mathlib.Topology.Category.Profinite.Nobeling.Span
/-- The Kronecker delta as a locally constant map from `π C (· ∈ s)` to `ℤ`.  -/
Profinite.NobelingProof.spanFinBasis : {I : Type u} →
  (C : Set (I → Bool)) →
    [inst : LinearOrder I] →
      (s : Finset I) →
        ↑(Profinite.NobelingProof.π C fun x => x ∈ s) → LocallyConstant ↑(Profinite.NobelingProof.π C fun x => x ∈ s) ℤ
-- Mathlib.Tactic.Linter.TextBased
/-- Read a file and apply all text-based linters.
Return a list of all unexpected errors, and, if some errors could be fixed automatically,
the collection of all lines with every automatic fix applied.
`exceptions` are any pre-existing style exceptions for this file.  -/
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.lintFile : Lean.Linter.LinterOptions →
  System.FilePath →
    Array Mathlib.Linter.TextBased.ErrorContext✝ →
      IO (Array Mathlib.Linter.TextBased.ErrorContext✝ × Option (Array String))
-- Mathlib.Data.Multiset.MapFold
Multiset.nodup_map_iff_inj_on : ∀ {α : Type u_1} {β : Type v} {f : α → β} {s : Multiset α},
  s.Nodup → ((Multiset.map f s).Nodup ↔ ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y)
-- Mathlib.RingTheory.Artinian.Module
isArtinian_of_le : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {s t : Submodule R M} [IsArtinian R ↥t], s ≤ t → IsArtinian R ↥s
-- Mathlib.MeasureTheory.Group.Arithmetic
measurable_const_smul_iff : ∀ {β : Type u_5} {α : Type u_6} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace α] {f : α → β} {G : Type u_7}
  [inst_2 : Group G] [inst_3 : MulAction G β] [MeasurableConstSMul G β] (c : G),
  (Measurable fun x => c • f x) ↔ Measurable f
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.mopRingEquivOp_symm_apply : ∀ {R : Type u_2} [inst : NonAssocRing R] (S : Subring R) (a : ↥S.op),
  S.mopRingEquivOp.symm a = MulOpposite.op (S.addEquivOp.symm a)
-- Init.Omega.Constraint
/-- The sum of two constraints. `[a, b] + [c, d] = [a + c, b + d]`.  -/
Lean.Omega.Constraint.add : Lean.Omega.Constraint → Lean.Omega.Constraint → Lean.Omega.Constraint
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
ProfiniteGrp.diagram_obj : ∀ (P : ProfiniteGrp.{u}) (X : OpenNormalSubgroup ↑P.toProfinite.toTop),
  P.diagram.obj X = (CategoryTheory.forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).obj (P.toFiniteQuotientFunctor.obj X)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.one_le_aleph0 : 1 ≤ Cardinal.aleph0
-- Mathlib.Algebra.DualQuaternion
Quaternion.snd_imK_dualNumberEquiv_symm : ∀ {R : Type u_1} [inst : CommRing R] (d : DualNumber (Quaternion R)),
  TrivSqZeroExt.snd (Quaternion.dualNumberEquiv.symm d).imK = (TrivSqZeroExt.snd d).imK
-- Batteries.Data.Vector.Basic
_private.Batteries.Data.Vector.Basic.0.Vector.scanrMUnsafe : {m : Type u_1 → Type u_2} →
  {α : Type u_3} → {β : Type u_1} → {n : ℕ} → [Monad m] → (α → β → m β) → β → Vector α n → m (Vector β (n + 1))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_modify_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF → ∀ {k : α} {f : β k → β k}, (Std.DTreeMap.Internal.Impl.modify k f t).get? k = Option.map f (t.get? k)
-- Init.Data.Array.Extract
Array.size_extract_le : ∀ {α : Type u_1} {as : Array α} {i j : ℕ}, (as.extract i j).size ≤ j - i
-- Mathlib.Algebra.Homology.Augment
/-- Truncating an augmented cochain complex is isomorphic (with components the identity)
to the original complex.
 -/
CochainComplex.truncateAugment : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      (C : CochainComplex V ℕ) →
        {X : V} →
          (f : X ⟶ C.X 0) →
            (w : CategoryTheory.CategoryStruct.comp f (C.d 0 1) = 0) → CochainComplex.truncate.obj (C.augment f w) ≅ C
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.pi_zero : ∀ {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : AddTorsor V1 P1]
  [inst_3 : Module k V1] {ι : Type u_9} {φv : ι → Type u_10} [inst_4 : (i : ι) → AddCommGroup (φv i)]
  [inst_5 : (i : ι) → Module k (φv i)], (AffineMap.pi fun x => 0) = 0
-- Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
TensorialAt.mkHom_apply_eq_extend : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] {A : Type u_9} [inst_13 : AddCommGroup A]
  [inst_14 : Module 𝕜 A] [inst_15 : VectorBundle 𝕜 F V] [inst_16 : CompleteSpace 𝕜] [inst_17 : FiniteDimensional 𝕜 F]
  [inst_18 : ContMDiffVectorBundle 1 F V I] [inst_19 : TopologicalSpace A] [inst_20 : IsTopologicalAddGroup A]
  [inst_21 : ContinuousSMul 𝕜 A] {Φ : ((x : M) → V x) → A} {x : M} (hΦ : TensorialAt I F Φ x) (σ : V x),
  (TensorialAt.mkHom Φ x hΦ) σ = Φ (FiberBundle.extend F σ)
-- Aesop.Tree.Check
Aesop.MVarClusterRef.checkMVars : Aesop.MVarClusterRef → Lean.Meta.SavedState → Lean.MetaM Unit
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.maxKeyD.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → α → Sort u_3) (fallback : α)
  (h_1 : (fallback : α) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (x : α) → motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r_1 : Std.DTreeMap.Internal.Impl α β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1 →
                      (fallback : α) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                            (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1))
                          fallback),
  (match Std.DTreeMap.Internal.Impl.leaf, fallback with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => h_2 size k v l x
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1),
      fallback => h_3 size k v l r size_1 k_1 v_1 l_1 r_1 h fallback) =
    h_1 fallback
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.range_le_ker_iff : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] {M : Type u_7} [inst_2 : AddZeroClass M]
  (f : G →+ G') (g : G' →+ M), f.range ≤ g.ker ↔ g.comp f = 0
-- Std.Time.Date.ValidDate
Std.Time.Internal.Bounded.cast.congr_simp : ∀ {rel : ℤ → ℤ → Prop} {lo₁ lo₂ hi₁ hi₂ : ℤ} (h₁ : lo₁ = lo₂) (h₂ : hi₁ = hi₂)
  (b b_1 : Std.Time.Internal.Bounded rel lo₁ hi₁),
  b = b_1 → Std.Time.Internal.Bounded.cast h₁ h₂ b = Std.Time.Internal.Bounded.cast h₁ h₂ b_1
-- Lean.Meta.Match.CaseArraySizes
Lean.Meta.CaseArraySizesSubgoal.mk.sizeOf_spec : ∀ (mvarId : Lean.MVarId) (elems diseqs : Array Lean.FVarId) (subst : Lean.Meta.FVarSubst),
  sizeOf { mvarId := mvarId, elems := elems, diseqs := diseqs, subst := subst } =
    1 + sizeOf mvarId + sizeOf elems + sizeOf diseqs + sizeOf subst
-- Mathlib.NumberTheory.LSeries.Basic
LSeriesSummable_zero : ∀ {s : ℂ}, LSeriesSummable 0 s
-- Mathlib.Topology.ContinuousMap.Sigma
ContinuousMap.isEmbedding_sigmaMk_comp : ∀ {X : Type u_1} {ι : Type u_2} {Y : ι → Type u_3} [inst : TopologicalSpace X]
  [inst_1 : (i : ι) → TopologicalSpace (Y i)] [Nonempty X],
  Topology.IsEmbedding fun g => (ContinuousMap.sigmaMk g.fst).comp g.snd
-- Mathlib.LinearAlgebra.Basis.Basic
Module.Basis.mem_span : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) (x : M), x ∈ Submodule.span R (Set.range ⇑b)
-- Std.Data.Internal.List.Associative
Std.Internal.List.self_le_maxKeyD_insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {v : β k} {fallback : α},
      (compare k (Std.Internal.List.maxKeyD (Std.Internal.List.insertEntry k v l) fallback)).isLE = true
-- Mathlib.Data.Part
Part.bind_some_right : ∀ {α : Type u_1} (x : Part α), x.bind Part.some = x
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitInfo.source : Lean.Meta.Grind.SplitInfo → Lean.Meta.Grind.SplitSource
-- Mathlib.Order.Lattice
Pi.sup_apply : ∀ {ι : Type u_1} {α' : ι → Type u_2} [inst : (i : ι) → Max (α' i)] (f g : (i : ι) → α' i) (i : ι), (f ⊔ g) i = f i ⊔ g i
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- The triangle in the following diagram is commutative:
```
      restrict₀ v                embedding
    R –––––––––––> ValueGroup₀ v –––––––––> Γ
    │                ∧
    │               /
    │              / embed v
    ∨             /
ValueGroupWithZero R
```
where the first row is the map `v` factored through its image group (with zero) in `Γ`.
 -/
ValuativeRel.ValueGroupWithZero.embed_valuation_eq_restrict₀ : ∀ {R : Type u_2} {Γ : Type u_3} [inst : Ring R] [inst_1 : ValuativeRel R] [inst_2 : LinearOrderedCommGroupWithZero Γ]
  (v : Valuation R Γ) [inst_3 : v.Compatible] (x : R),
  (ValuativeRel.ValueGroupWithZero.embed v) ((ValuativeRel.valuation R) x) =
    (MonoidWithZeroHom.ValueGroup₀.restrict₀ (MonoidWithZeroHom.ofClass v)) x
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.Lean.Name.demangleAux.match_4.eq_1 : ∀ (s : String) (motive : Char → Option (s.Pos × ℕ) → Sort u_1) (q : s.Pos) (v : ℕ)
  (h_1 : (q_1 : s.Pos) → (v_1 : ℕ) → some (q, v) = some (q_1, v_1) → motive 'u' (some (q_1, v_1)))
  (h_2 : (x : Char) → (x_1 : Option (s.Pos × ℕ)) → some (q, v) = x_1 → motive x x_1),
  (match 'u', h₂ : some (q, v) with
    | 'u', some (q_1, v_1) => h_1 q_1 v_1 h₂
    | x, x_1 => h_2 x x_1 h₂) =
    h_1 q v ⋯
-- Mathlib.Analysis.Normed.Group.Quotient
QuotientAddGroup.instSeminormedAddCommGroup.eq_1 : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] (S : AddSubgroup M),
  QuotientAddGroup.instSeminormedAddCommGroup S =
    { toNorm := QuotientAddGroup.addGroupSeminorm.toSeminormedAddCommGroup.toNorm,
      toAddCommGroup := QuotientAddGroup.addGroupSeminorm.toSeminormedAddCommGroup.toAddCommGroup,
      toDist := QuotientAddGroup.addGroupSeminorm.toSeminormedAddCommGroup.toDist, dist_self := ⋯, dist_comm := ⋯,
      dist_triangle := ⋯, edist := PseudoMetricSpace.edist, edist_dist := ⋯,
      toUniformSpace := IsTopologicalAddGroup.leftUniformSpace (M ⧸ S), uniformity_dist := ⋯,
      toBornology := PseudoMetricSpace.toBornology, cobounded_sets := ⋯, dist_eq := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- If a matrix has a repeated row, the determinant will be zero.  -/
Matrix.det_zero_of_row_eq : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {M : Matrix n n R}
  {i j : n}, i ≠ j → M i = M j → M.det = 0
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.FlatMap.0.Std.Iter.step_flatMapAfterM.match_1.eq_3 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {it₁ : Std.Iter β} (motive : it₁.Step → Sort u_2)
  (h : it₁.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it₁' : Std.Iter β) →
      (b : β) → (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' b)) → motive ⟨Std.IterStep.yield it₁' b, h⟩)
  (h_2 : (it₁' : Std.Iter β) → (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', h⟩)
  (h_3 : (h : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.done, h⟩ with
    | ⟨Std.IterStep.yield it₁' b, h⟩ => h_1 it₁' b h
    | ⟨Std.IterStep.skip it₁', h⟩ => h_2 it₁' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_3 h
-- Mathlib.GroupTheory.Congruence.Defs
Con.liftOnUnits_mk : ∀ {M : Type u_1} {α : Type u_4} [inst : Monoid M] {c : Con M} (f : (x y : M) → c (x * y) 1 → c (y * x) 1 → α)
  (Hf :
    ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1) (x' y' : M) (hxy' : c (x' * y') 1) (hyx' : c (y' * x') 1),
      c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx')
  (x y : M) (hxy : ↑x * ↑y = 1) (hyx : ↑y * ↑x = 1),
  Con.liftOnUnits { val := ↑x, inv := ↑y, val_inv := hxy, inv_val := hyx } f Hf = f x y ⋯ ⋯
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.mk.sizeOf_spec : ∀ {α : Type u_4} [inst : TopologicalSpace α] [inst_1 : SizeOf α] (toCompacts : TopologicalSpace.Compacts α)
  (isOpen' : IsOpen toCompacts.carrier),
  sizeOf { toCompacts := toCompacts, isOpen' := isOpen' } = 1 + sizeOf toCompacts + sizeOf isOpen'
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.instNonemptyCarrierCarrierCommRingCatPullbackOfSubsingleton : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} [Nonempty ↥X] [Nonempty ↥Y] [Subsingleton ↥S],
  Nonempty ↥(CategoryTheory.Limits.pullback f g)
-- Mathlib.Algebra.Group.PUnit
PUnit.instOne_mathlib : One PUnit.{u_1 + 1}
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.isPrimePow_card : ∀ (K : Type u_1) [Field K] [inst : Fintype K], IsPrimePow (Fintype.card K)
-- Mathlib.SetTheory.ZFC.Class
Class.instUsesSetNotationForOrder : UsesSetNotationForOrder Class.{u_1}
-- Mathlib.CategoryTheory.Triangulated.TriangleShift
CategoryTheory.Pretriangulated.Triangle.shiftFunctor_map_hom₂ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] (n : ℤ) {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y),
  ((CategoryTheory.Pretriangulated.Triangle.shiftFunctor C n).map f).hom₂ = (CategoryTheory.shiftFunctor C n).map f.hom₂
-- Mathlib.Topology.UnitInterval
unitInterval.pos_iff_ne_zero : ∀ {x : ↑unitInterval}, 0 < x ↔ x ≠ 0
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.eq_interpolate_of_eval_eq : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} (r : ι → F)
  {f : Polynomial F},
  Set.InjOn v ↑s → f.degree < ↑s.card → (∀ i ∈ s, Polynomial.eval (v i) f = r i) → f = (Lagrange.interpolate s v) r
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.antitone_logSizeBallSeq_add_one_subset : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [inst_1 : DecidableEq T]
  (hJ : J.Nonempty), Antitone fun i => (PairReduction.logSizeBallSeq J hJ a c i).finset
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnrichedOrdinary.instCategory : {C : Type u} →
  [CategoryTheory.Category.{v, u} C] → CategoryTheory.Category.{v, u} (CategoryTheory.CatEnrichedOrdinary C)
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.le_wp_liftWith_OptionT_apply : ∀ {Pred : Type u} {EPred : Type u_1} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α : Type u}
  {post : α → Pred} {epost : EPost.Cons✝ Pred EPred} (f : ({β : Type u} → OptionT m β → m (Option β)) → m α),
  Lean.Order.PartialOrder.rel (Std.Internal.Do.wp (f fun {β} x => x.run) post epost.tail)
    (Std.Internal.Do.wp (MonadControl.liftWith f) post epost)
-- Mathlib.NumberTheory.Padics.PadicNumbers
instAddPadic : (p : ℕ) → [inst : Fact (Nat.Prime p)] → Add ℚ_[p]
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ClientCapabilities.textDocument? : Lean.Lsp.ClientCapabilities → Option Lean.Lsp.TextDocumentClientCapabilities
-- Mathlib.RingTheory.Conductor
/-- Let `S / R` be a ring extension and `x : S`, then the conductor of `R<x>` is the
biggest ideal of `S` contained in `R<x>`.  -/
conductor : (R : Type u_1) → {S : Type u_2} → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → S → Ideal S
-- Mathlib.Algebra.Group.Commute.Defs
AddCommute.self_nsmul : ∀ {M : Type u_2} [inst : AddMonoid M] (a : M) (n : ℕ), AddCommute a (n • a)
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.additiveObjIsoBiproduct_naturality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.Preadditive D]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor (CategoryTheory.Mat_ C) D)
  [inst_5 : F.Additive] {M N : CategoryTheory.Mat_ C} (f : M ⟶ N),
  CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.Mat_.additiveObjIsoBiproduct F N).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Mat_.additiveObjIsoBiproduct F M).hom
      (CategoryTheory.Limits.biproduct.matrix fun i j => F.map ((CategoryTheory.Mat_.embedding C).map (f i j)))
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instSemigroupWithZero : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : SemigroupWithZero β] → [ContinuousMul β] → SemigroupWithZero (ZeroAtInftyContinuousMap α β)
-- Mathlib.Algebra.Torsor.Defs
/-- `v ↦ v +ᵥ p` as an equivalence.  -/
Equiv.vaddConst : {G : Type u_1} → {P : Type u_2} → [inst : AddGroup G] → [AddTorsor G P] → P → G ≃ P
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_ne_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} [IsAddTorsionFree R],
  Polynomial.derivative p ≠ 0 ↔ p.natDegree ≠ 0
-- Mathlib.Data.Nat.Size
/-- **Alias** of `Nat.shiftLeft'_true_ne_zero`. -/
Nat.shiftLeft'_tt_ne_zero : ∀ (m : ℕ) {n : ℕ}, n ≠ 0 → Nat.shiftLeft' true m n ≠ 0
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.toBitVec_maxValueSealed_eq_intMaxSealed : Int64.maxValueSealed✝.toBitVec = BitVec.Signed.intMaxSealed✝ 64
-- Init.Sym.Lemmas
Lean.Sym.Nat.dvd_eq_true : ∀ (a b : ℕ), decide (a ∣ b) = true → (a ∣ b) = True
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.pullHom'_eq_pullHom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {obj obj' : (i : ι) → ↑(F.obj { as := Opposite.op (X i) })}
  (hom :
    (i j : ι) →
      (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j))
  ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (p : Y ⟶ (sq i₁ i₂).pullback)
  (hf₁ :
    autoParam (CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
      CategoryTheory.Pseudofunctor.DescentData'.pullHom'_eq_pullHom._auto_1)
  (hf₂ :
    autoParam (CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q)
      CategoryTheory.Pseudofunctor.DescentData'.pullHom'_eq_pullHom._auto_3)
  (hp₁ :
    autoParam (CategoryTheory.CategoryStruct.comp p (sq i₁ i₂).p₁ = f₁)
      CategoryTheory.Pseudofunctor.DescentData'.pullHom'_eq_pullHom._auto_5)
  (hp₂ :
    autoParam (CategoryTheory.CategoryStruct.comp p (sq i₁ i₂).p₂ = f₂)
      CategoryTheory.Pseudofunctor.DescentData'.pullHom'_eq_pullHom._auto_7)
  {Z : ↑(F.obj { as := Opposite.op Y })} (h : (F.map f₂.op.toLoc).toFunctor.obj (obj' i₂) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom q f₁ f₂ hf₁ hf₂) h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom (hom i₁ i₂) p f₁ f₂ ⋯ ⋯) h
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- Construct a `MonoOver X`.  -/
CategoryTheory.MonoOver.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X A : C} → (f : A ⟶ X) → [hf : CategoryTheory.Mono f] → CategoryTheory.MonoOver X
-- Mathlib.Algebra.Group.Finsupp
Finsupp.embDomain.addMonoidHom_apply : ∀ {ι : Type u_1} {F : Type u_2} {M : Type u_3} [inst : AddZeroClass M] (f : ι ↪ F) (v : ι →₀ M),
  (Finsupp.embDomain.addMonoidHom f) v = Finsupp.embDomain f v
-- Mathlib.SetTheory.Cardinal.Ordinal
/-- **Alias** of `Ordinal.isPrincipal_add_omega`. -/
Ordinal.principal_add_omega : ∀ (o : Ordinal.{u_1}), Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) (Ordinal.omega o)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
PartialOrder.mk.congr_simp : ∀ {α : Type u_2} [toPreorder : Preorder α] [toPreorder_1 : Preorder α] (e_toPreorder : toPreorder = toPreorder_1)
  (le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b),
  { toPreorder := toPreorder, le_antisymm := le_antisymm } = { toPreorder := toPreorder_1, le_antisymm := ⋯ }
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.nfp_mul_zero : ∀ (a : Ordinal.{u_1}), Ordinal.nfp (fun x => a * x) 0 = 0
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.comm_trans_comm : ∀ (R : Type u_1) [inst : CommSemiring R] (M : Type u_7) (N : Type u_8) [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N],
  TensorProduct.comm R N M ≪≫ₗ TensorProduct.comm R M N = LinearEquiv.refl R (TensorProduct R N M)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- The pullback cone obtained by flipping `fst` and `snd`.  -/
CategoryTheory.Limits.PullbackCone.flip : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f : X ⟶ Z} → {g : Y ⟶ Z} → CategoryTheory.Limits.PullbackCone f g → CategoryTheory.Limits.PullbackCone g f