mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.pullback_singleton : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : Y ⟶ X) (g : Z ⟶ X)
  [inst_1 : CategoryTheory.Limits.HasPullback g f],
  CategoryTheory.Presieve.pullbackArrows f (CategoryTheory.Presieve.singleton g) =
    CategoryTheory.Presieve.singleton (CategoryTheory.Limits.pullback.snd g f)
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.Splits.le_iff_exists_eq_append : ∀ {s : String.Slice} {p₁ p₂ : s.Pos} {t₁ t₂ t₃ t₄ : String},
  p₁.Splits t₁ t₂ → p₂.Splits t₃ t₄ → (p₁ ≤ p₂ ↔ ∃ t₅, t₃ = t₁ ++ t₅ ∧ t₂ = t₅ ++ t₄)
-- Batteries.Tactic.GeneralizeProofs
Batteries.Tactic.GeneralizeProofs.GState.mk.sizeOf_spec : ∀ (propToFVar : Lean.ExprMap Lean.Expr), sizeOf { propToFVar := propToFVar } = 1 + sizeOf propToFVar
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.insert_eq_insertₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α)
  (b : β a), m.insert a b = m.insertₘ a b
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- the morphism on the left objects  -/
CategoryTheory.ShortComplex.Hom.τ₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} → S₁.Hom S₂ → (S₁.X₁ ⟶ S₂.X₁)
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.instFullAddGrpCatForget₂AddMonoidHomCarrierCarrier : (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat).Full
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothPresheafAddCommGroup.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) (M : Type u) [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] (A : Type u)
  [inst_9 : TopologicalSpace A] [inst_10 : ChartedSpace H A] [inst_11 : AddCommGroup A]
  [inst_12 : LieAddGroup I (↑⊤) A],
  smoothPresheafAddCommGroup IM I M A =
    { obj := fun U => AddCommGrpCat.of ((smoothSheaf IM I M A).presheaf.obj U),
      map := fun {X Y} h => AddCommGrpCat.ofHom (ContMDiffMap.restrictAddMonoidHom IM I A ⋯), map_id := ⋯,
      map_comp := ⋯ }
-- Mathlib.Analysis.Calculus.ContDiff.Basic
iteratedFDerivWithin_prodMk : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {x : E} {n : WithTop ℕ∞} {f : E → F}
  {g : E → G},
  ContDiffWithinAt 𝕜 n f s x →
    ContDiffWithinAt 𝕜 n g s x →
      UniqueDiffOn 𝕜 s →
        x ∈ s →
          ∀ {i : ℕ},
            ↑i ≤ n →
              iteratedFDerivWithin 𝕜 i (fun x => (f x, g x)) s x =
                (iteratedFDerivWithin 𝕜 i f s x).prod (iteratedFDerivWithin 𝕜 i g s x)
-- Mathlib.Algebra.Module.Submodule.Defs
/-- A submodule of a module is one which is closed under vector operations.
This is a sufficient condition for the subset of vectors in the submodule
to themselves form a module.  -/
Submodule : (R : Type u) → (M : Type v) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Type v
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.refl.eq_1 : ∀ (M : Type u_1) [inst : TopologicalSpace M] [inst_1 : Add M],
  ContinuousAddEquiv.refl M = { toAddEquiv := AddEquiv.refl M, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.RingTheory.Ideal.GoingDown
Algebra.HasGoingDown.exists_ideal_le_liesOver_of_lt : ∀ {R : Type u_1} {S : Type u_2} {inst : CommRing R} {inst_1 : CommRing S} {inst_2 : Algebra R S}
  [self : Algebra.HasGoingDown R S] {p : Ideal R} [p.IsPrime] (Q : Ideal S) [Q.IsPrime],
  p < Ideal.under R Q → ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
-- Init.Data.Option.Lemmas
Option.mem_ite_none_right : ∀ {α : Type u_1} {p : Prop} {x : α} {x_1 : Decidable p} {l : Option α}, (x ∈ if p then l else none) ↔ p ∧ x ∈ l
-- Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
CategoryTheory.Functor.instCommShiftHomologicalComplexIntUpFunctorQuasiIsoMapHomologicalComplexUpToQuasiIsoLocalizerMorphism : {C₁ : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
    [inst_1 : CategoryTheory.Abelian C₁] →
      {C₂ : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_3 : CategoryTheory.Abelian C₂] →
            (F : CategoryTheory.Functor C₁ C₂) →
              [inst_4 : F.Additive] →
                [inst_5 : CategoryTheory.Limits.PreservesFiniteLimits F] →
                  [inst_6 : CategoryTheory.Limits.PreservesFiniteColimits F] →
                    (F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism (ComplexShape.up ℤ)).functor.CommShift ℤ
-- Mathlib.Order.Cover
apply_covBy_apply_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {a b : α} {E : Type u_3}
  [inst_2 : EquivLike E α β] [OrderIsoClass E α β] (e : E), e a ⋖ e b ↔ a ⋖ b
-- Mathlib.Data.Matrix.Basic
AlgEquiv.mapMatrix_refl : ∀ {m : Type u_2} {R : Type u_7} {α : Type u_11} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : CommSemiring R]
  [inst_3 : Semiring α] [inst_4 : Algebra R α], AlgEquiv.refl.mapMatrix = AlgEquiv.refl
-- Mathlib.LinearAlgebra.QuadraticForm.Radical
/-- If `2` is invertible in the coefficient ring,
a quadratic map is nondegenerate
iff its polar bilinear map is nondegenerate.  -/
QuadraticMap.nondegenerate_polar_iff : ∀ {R : Type u_1} {M : Type u_2} {P : Type u_4} [inst : AddCommGroup M] [inst_1 : AddCommGroup P] [inst_2 : CommRing R]
  [inst_3 : Module R M] [inst_4 : Module R P] {Q : QuadraticMap R M P} [Invertible 2],
  LinearMap.Nondegenerate Q.polarBilin ↔ QuadraticMap.Nondegenerate
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.const_equiv : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] {x y : β},
  CauSeq.const abv x ≈ CauSeq.const abv y ↔ x = y
-- Mathlib.Data.Set.Defs
/-- The universal set on a type `α` is the set containing all elements of `α`.

This is conceptually the "same as" `α` (in set theory, it is actually the same), but type theory
makes the distinction that `α` is a type while `Set.univ` is a term of type `Set α`. `Set.univ` can
itself be coerced to a type `↥Set.univ` which is in bijection with (but distinct from) `α`.  -/
Set.univ : {α : Type u} → Set α
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
ENNReal.hasMeasurablePow : MeasurablePow ENNReal ℝ
-- Mathlib.Algebra.Field.IsField
/-- Nonzero elements have multiplicative inverses.  -/
IsField.mul_inv_cancel : ∀ {R : Type u} [inst : Semiring R], IsField R → ∀ {a : R}, a ≠ 0 → ∃ b, a * b = 1
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
CategoryTheory.Limits.compNatIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} {D : Type u'} [inst_2 : CategoryTheory.Category.{v, u'} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [inst_4 : F.IsEquivalence],
  CategoryTheory.Limits.compNatIso F =
    CategoryTheory.NatIso.ofComponents
      (fun j =>
        match j with
        | CategoryTheory.Limits.WalkingParallelPair.zero =>
          CategoryTheory.Iso.refl
            (((CategoryTheory.Limits.parallelPair f 0).comp F).obj CategoryTheory.Limits.WalkingParallelPair.zero)
        | CategoryTheory.Limits.WalkingParallelPair.one =>
          CategoryTheory.Iso.refl
            (((CategoryTheory.Limits.parallelPair f 0).comp F).obj CategoryTheory.Limits.WalkingParallelPair.one))
      ⋯
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Set.powersetCard.mulActionHom_compl_mulActionHom_compl : ∀ (G : Type u_1) [inst : Group G] (α : Type u_2) [inst_1 : MulAction G α] {n : ℕ} [inst_2 : DecidableEq α]
  [inst_3 : Fintype α] {m : ℕ} (hm : m + n = Fintype.card α),
  (Set.powersetCard.mulActionHom_compl G α ⋯).comp (Set.powersetCard.mulActionHom_compl G α hm) = MulActionHom.id G
-- Lean.Elab.Tactic.Rewrite
Lean.Elab.Tactic.withRWRulesSeq : Lean.Syntax → Lean.Syntax → (Bool → Lean.Syntax → Lean.Elab.Tactic.TacticM Unit) → Lean.Elab.Tactic.TacticM Unit
-- Std.Data.DHashMap.Basic
/-- Inserts multiple mappings into the hash map by iterating over the given collection and calling
`insert`. If the same key appears multiple times, the last occurrence takes precedence.

Note: this precedence behavior is true for `HashMap`, `DHashMap`, `HashMap.Raw` and `DHashMap.Raw`.
The `insertMany` function on `HashSet` and `HashSet.Raw` behaves differently: it will prefer the first
appearance.
 -/
Std.DHashMap.Const.insertMany : {α : Type u} →
  {x : BEq α} →
    {x_1 : Hashable α} →
      {β : Type v} → {ρ : Type w} → [ForIn Id ρ (α × β)] → (Std.DHashMap α fun x => β) → ρ → Std.DHashMap α fun x => β
-- Mathlib.Probability.Process.Adapted
MeasureTheory.stronglyAdapted_zero : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] (β : Type u_4) [inst_1 : TopologicalSpace β]
  [inst_2 : Zero β] (f : MeasureTheory.Filtration ι m), MeasureTheory.StronglyAdapted f 0
-- Mathlib.Topology.Semicontinuity.Defs
lowerHemicontinuous_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β},
  LowerHemicontinuous f ↔ ∀ (x : α), LowerHemicontinuousAt f x
-- Mathlib.ModelTheory.Order
FirstOrder.Language.HomClass.monotone : ∀ {L : FirstOrder.Language} {M : Type w'} [inst : L.IsOrdered] [inst_1 : L.Structure M] {N : Type u_1}
  [inst_2 : L.Structure N] {F : Type u_2} [inst_3 : FunLike F M N] [L.HomClass F M N] [inst_5 : Preorder M]
  [L.OrderedStructure M] [inst_7 : Preorder N] [L.OrderedStructure N] (f : F), Monotone ⇑f
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- Transfer `AddGrpObj` along an isomorphism.  -/
CategoryTheory.AddGrpObj.ofIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {G' X : C} → [CategoryTheory.AddGrpObj G'] → (G' ≅ X) → CategoryTheory.AddGrpObj X
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.equivSigma_apply_fst : ∀ (T : Type u) [inst : CategoryTheory.Category.{v, u} T] (f : CategoryTheory.Arrow T),
  ((CategoryTheory.Arrow.equivSigma T) f).fst = f.left
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- structure morphism of the algebra  -/
CategoryTheory.Endofunctor.Algebra.str : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C C} → (self : CategoryTheory.Endofunctor.Algebra F) → F.obj self.a ⟶ self.a
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.isZero.eq_1 : Nat.Internal.Linear.Poly.isZero [] = true
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.nullHomotopicMap_f_of_not_rel_left : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {k₁ k₀ : ι},
  c.Rel k₁ k₀ →
    (∀ (l : ι), ¬c.Rel k₀ l) →
      ∀ (hom : (i j : ι) → C.X i ⟶ D.X j),
        (Homotopy.nullHomotopicMap hom).f k₀ = CategoryTheory.CategoryStruct.comp (hom k₀ k₁) (D.d k₁ k₀)
-- Mathlib.Analysis.InnerProductSpace.Orientation
Orientation.volumeForm_robust' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
  [_i : Fact (Module.finrank ℝ E = n)] (o : Orientation ℝ E (Fin n)) (b : OrthonormalBasis (Fin n) ℝ E) (v : Fin n → E),
  |o.volumeForm v| = |b.toBasis.det v|
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.Presheaf.isSheaf_iff_multiequalizer : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  (J : CategoryTheory.GrothendieckTopology C) (P : CategoryTheory.Functor Cᵒᵖ A)
  [inst_2 : ∀ (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)],
  CategoryTheory.Presheaf.IsSheaf J P ↔ ∀ (X : C) (S : J.Cover X), CategoryTheory.IsIso (S.toMultiequalizer P)
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- Composing a multilinear map with the identity linear map in each argument.  -/
MultilinearMap.compLinearMap_id : ∀ {R : Type uR} {ι : Type uι} {M₁' : ι → Type v₁'} {M₂ : Type v₂} [inst : Semiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : Module R M₂] [inst_3 : (i : ι) → AddCommMonoid (M₁' i)] [inst_4 : (i : ι) → Module R (M₁' i)]
  (g : MultilinearMap R M₁' M₂), (g.compLinearMap fun x => LinearMap.id) = g
-- Mathlib.Data.List.Shortlex
List.shortlex_def : ∀ {α : Type u_1} {r : α → α → Prop} {s t : List α},
  List.Shortlex r s t ↔ s.length < t.length ∨ s.length = t.length ∧ List.Lex r s t
-- Batteries.Data.Nat.Lemmas
Nat.casesDiagOn_succ_succ : ∀ {motive : ℕ → ℕ → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : ℕ) → motive 0 (n + 1))
  (succ_zero : (m : ℕ) → motive (m + 1) 0) (succ_succ : (m n : ℕ) → motive (m + 1) (n + 1)) (m n : ℕ),
  Nat.casesDiagOn (m + 1) (n + 1) zero_zero zero_succ succ_zero succ_succ = succ_succ m n
-- Mathlib.ModelTheory.ElementaryMaps
FirstOrder.Language.ElementaryEmbedding.refl_apply : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] (x : M),
  (FirstOrder.Language.ElementaryEmbedding.refl L M) x = x
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntInfo : Type
-- Init.Data.List.Erase
List.erase_replicate : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {n : ℕ} {a b : α},
  (List.replicate n a).erase b = if (b == a) = true then List.replicate (n - 1) a else List.replicate n a
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- The degree of `cyclotomic n` is `totient n`.  -/
Polynomial.degree_cyclotomic : ∀ (n : ℕ) (R : Type u_1) [inst : Ring R] [Nontrivial R], (Polynomial.cyclotomic n R).degree = ↑n.totient
-- Mathlib.Algebra.Polynomial.Taylor
Polynomial.degree_taylor : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R) (r : R), ((Polynomial.taylor r) p).degree = p.degree
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.instSemilatticeInfOpenSubgroup.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G],
  OpenSubgroup.instSemilatticeInfOpenSubgroup = Function.Injective.semilatticeInf SetLike.coe ⋯ ⋯ ⋯ ⋯
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.mk_fintype : ∀ (α : Type u) [h : Fintype α], Cardinal.mk α = ↑(Fintype.card α)
-- Batteries.Data.List.Lemmas
List.idxsOf_start : ∀ {α : Type u_1} {xs : List α} {x : α} {s : ℕ} [inst : BEq α],
  List.idxsOf x xs s = List.map (fun x => x + s) (List.idxsOf x xs)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
instCommRingCarrierObjOppositeRingCatCompCommRingCatForget₂RingHomCarrier : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} →
      (X : Cᵒᵖ) → CommRing ↑((R.comp (CategoryTheory.forget₂ CommRingCat RingCat)).obj X)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
/-- Given a polynomial `p`, returns `some (x, k, c)` if `p` contains the monomial `k*x`,
and `x` has been eliminated using the equality `c`.
 -/
Int.Internal.Linear.Poly.findVarToSubst : Int.Internal.Linear.Poly →
  Lean.Meta.Grind.GoalM (Option (ℤ × Int.Internal.Linear.Var × Lean.Meta.Grind.Arith.Cutsat.EqCnstr))
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftLeft
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.TwoPowShiftTarget.n : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} → {w : ℕ} → Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.TwoPowShiftTarget aig w → ℕ
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.insertManyIfNew_eq_insertManyIfNew!_impl : ∀ {α : Type u} {β : α → Type v} {x : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} (h : t₁.Balanced),
  ↑(t₁.insertManyIfNew t₂ h) = ↑(t₁.insertManyIfNew! t₂)
-- Mathlib.RingTheory.Algebraic.Integral
IsAlgebraic.tmul : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] (s : S) {a : A},
  IsAlgebraic R a → ∀ [FaithfulSMul R S], IsAlgebraic S (s ⊗ₜ[R] a)
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.comp_val : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} {T : Type u_2} [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (Q : Algebra.Generators S T ι') (P : Algebra.Generators R S ι) (a : ι' ⊕ ι),
  (Q.comp P).val a = Sum.elim Q.val (⇑(algebraMap S T) ∘ P.val) a
-- Mathlib.CategoryTheory.Abelian.Refinements
CategoryTheory.ShortComplex.epi_homologyMap_iff_up_to_refinements : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂),
  CategoryTheory.Epi (CategoryTheory.ShortComplex.homologyMap φ) ↔
    ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
      CategoryTheory.CategoryStruct.comp y₂ S₂.g = 0 →
        ∃ A' π,
          ∃ (_ : CategoryTheory.Epi π),
            ∃ x₂,
              ∃ (_ : CategoryTheory.CategoryStruct.comp x₂ S₁.g = 0),
                ∃ y₁,
                  CategoryTheory.CategoryStruct.comp π y₂ =
                    CategoryTheory.CategoryStruct.comp x₂ φ.τ₂ + CategoryTheory.CategoryStruct.comp y₁ S₂.f
-- Lean.Meta.Sym.LooseBVarsS
/-- Lowers the loose bound variables `>= s` in `e` by `d`.
That is, a loose bound variable `bvar i` with `i >= s` is mapped to `bvar (i-d)`.
It assumes the input is maximally shared, and ensures the output is too.
Remark: if `s < d`, then the result is `e`.
 -/
Lean.Meta.Sym.lowerLooseBVarsS' : Lean.Expr → ℕ → ℕ → Lean.Meta.Sym.Internal.AlphaShareBuilderM Lean.Expr
-- Mathlib.Algebra.Star.Subalgebra
/-- If all elements of `s : Set A` commute pairwise and also commute pairwise with elements of
`star s`, then `StarSubalgebra.adjoin R s` is commutative. See note [reducible non-instances].  -/
StarAlgebra.adjoinCommRingOfComm : (R : Type u) →
  {A : Type v} →
    [inst : CommRing R] →
      [inst_1 : StarRing R] →
        [inst_2 : Ring A] →
          [inst_3 : Algebra R A] →
            [inst_4 : StarRing A] →
              [inst_5 : StarModule R A] →
                {s : Set A} →
                  (∀ a ∈ s, ∀ b ∈ s, a * b = b * a) →
                    (∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a) → CommRing ↥(StarAlgebra.adjoin R s)
-- Mathlib.CategoryTheory.Yoneda
/-- When `C` is a category such that `Category.{v₁} C`, then
the functor `uliftCoyoneda.{w} : C ⥤ Cᵒᵖ ⥤ Type (max w v₁)` is fully faithful.  -/
CategoryTheory.Coyoneda.ULiftCoyoneda.fullyFaithful : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.uliftCoyoneda.{w, v₁, u₁}.FullyFaithful
-- Batteries.Data.Vector.Lemmas
Vector.scanr_empty : ∀ {α : Type u_1} {β : Type u_2} {init : β} {f : α → β → β}, Vector.scanr f init #v[] = #v[init]
-- Lean.Elab.App
_private.Lean.Elab.App.0.Lean.Elab.Term.resolveLVal : Lean.Expr → Lean.Elab.Term.LVal → Bool → Lean.Elab.TermElabM (Lean.Expr × Lean.Elab.Term.LValResolution)
-- Init.Data.Float.Model.Unpacked.Round
Float.Model.UnpackedFloat.ExtendedMantissa.mk.injEq : ∀ (mantissa : ℕ) (roundBit stickyBit : Bool) (mantissa_1 : ℕ) (roundBit_1 stickyBit_1 : Bool),
  ({ mantissa := mantissa, roundBit := roundBit, stickyBit := stickyBit } =
      { mantissa := mantissa_1, roundBit := roundBit_1, stickyBit := stickyBit_1 }) =
    (mantissa = mantissa_1 ∧ roundBit = roundBit_1 ∧ stickyBit = stickyBit_1)
-- Mathlib.RepresentationTheory.Basic
Representation.instModuleAsModule : {k : Type u_1} →
  {G : Type u_3} →
    {V : Type u_2} →
      [inst : Semiring k] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid V] → [inst_3 : Module k V] → (x : Representation k G V) → Module k x.asModule
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerLeft_hom_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C) {Y Z : C}
  (f : Y ≅ Z) {Z_1 : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f.hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f.inv) h) =
    h
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_of_contains_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k a : α} {v : β},
  (t.insertIfNew k v).contains a = true → cmp k a ≠ Ordering.eq → t.contains a = true
-- Lean.Server.FileWorker.SignatureHelp
Lean.Server.FileWorker.SignatureHelp.findSignatureHelp? : Lean.FileMap →
  Option Lean.Lsp.SignatureHelpContext →
    Lean.Syntax → Lean.Elab.InfoTree → String.Pos.Raw → IO (Option Lean.Lsp.SignatureHelp)
-- Init.Data.Array.Monadic
_private.Init.Data.Array.Monadic.0.List.filterMapM.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) →
    (__do_lift : Option β) → (Unit → motive none) → ((b : β) → motive (some b)) → motive __do_lift
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.toLinearEquiv_to_linearMap : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  (A : SpecialLinearGroup R V), ↑(SpecialLinearGroup.toLinearEquiv A) = ↑↑A
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.LawfulEqCmp cmp] (t t_1 : Std.DTreeMap α β cmp)
  (e_t : t = t_1) (a : α) (h : a ∈ t), t.get a h = t_1.get a ⋯
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.mapInclIsometry_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] (E' : Submodule 𝕜 E)
  (F' : Submodule 𝕜 F) (x : TensorProduct 𝕜 ↥E' ↥F'),
  (TensorProduct.mapInclIsometry E' F') x = (TensorProduct.mapIncl E' F') x
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Zero.close : {α : Type} → Std.CloseableChannel.Zero✝ α → EIO Std.CloseableChannel.Error Unit
-- Mathlib.Data.PSigma.Order
/-- The notation `Σₗ' i, α i` refers to a sigma type which is locally equipped with the
lexicographic order.  -/
PSigma.«termΣₗ'_,_» : Lean.ParserDescr
-- Mathlib.Computability.TuringMachine.Tape
Turing.ListBlank.hasEmptyc : {Γ : Type u_1} → [inst : Inhabited Γ] → EmptyCollection (Turing.ListBlank Γ)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_updateBucket_alter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} {f : Option (β a) → Option (β a)},
      (Std.DHashMap.Internal.toListModel
            (Std.DHashMap.Internal.updateBucket (↑m).buckets ⋯ a (Std.DHashMap.Internal.AssocList.alter a f))).Perm
        (Std.Internal.List.alterKey a f (Std.DHashMap.Internal.toListModel (↑m).buckets))
-- Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
SSet.instFiniteTensorObj : ∀ {X₁ X₂ : SSet} [X₁.Finite] [X₂.Finite], (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂).Finite
-- Mathlib.Algebra.Order.Rearrangement
/-- **Rearrangement Inequality**: Pointwise multiplication of `f` and `g` is minimized when `f` and
`g` antivary together. Stated by permuting the entries of `f`.  -/
Antivary.sum_mul_le_sum_comp_perm_mul : ∀ {ι : Type u_1} {α : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  {σ : Equiv.Perm ι} {f g : ι → α} [inst_4 : Fintype ι], Antivary f g → ∑ i, f i * g i ≤ ∑ i, f (σ i) * g i
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- **Alias** of `ClosedSubmodule.toSubmodule_orthogonal_eq`. -/
ClosedSubmodule.orthogonal_toSubmodule_eq : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : ClosedSubmodule 𝕜 E), ↑Kᗮ = (↑K)ᗮ