mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
/-- Takes in a formula f and an array of rupHints and attempts to verify that f is unsatisfiable. It returns:
- f', which is the same as f but the assignments field has been updated to be consistent with anything learned over the
  course of the rupCheck
- derivedLits, which is the list of literals that were derived over the course of the rupCheck (these are needed to
  eventually reconstruct the original assignment)
- derivedEmpty, which indicates whether the empty clause or a contradiction was derived
- encounteredError, which is true if the rupCheck failed and false otherwise

Note: This function assumes that any rupUnits and ratUnits corresponding to this rup check have already been added to f.
 -/
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.performRupCheck : {n : ℕ} →
  Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n →
    Array ℕ →
      Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n ×
        Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) × Bool × Bool
-- Mathlib.RingTheory.RingHom.QuasiFinite
/-- Helper lemma for the `algebraize` tactic  -/
RingHom.QuasiFinite.toAlgebra : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  f.QuasiFinite → Algebra.QuasiFinite R S
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
/-- If `G` is a group with measurable multiplication, then right multiplication by `g : G` is a
measurable automorphism of `G`.  -/
MeasurableEquiv.mulRight : {G : Type u_1} → [inst : Group G] → [inst_1 : MeasurableSpace G] → [MeasurableMul G] → G → G ≃ᵐ G
-- Init.Meta.Defs
Lean.Syntax.getOptionalIdent? : Lean.Syntax → Option Lean.Name
-- Mathlib.Topology.MetricSpace.IsometricSMul
diam_vadd : ∀ {M : Type u} {X : Type w} [inst : PseudoMetricSpace X] [inst_1 : VAdd M X] [IsIsometricVAdd M X] (c : M) (s : Set X),
  Metric.diam (c +ᵥ s) = Metric.diam s
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
CategoryTheory.Functor.instFullPlusMapHomotopyCategoryPlusOfFaithful : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [inst_4 : F.Additive] [F.Full] [F.Faithful],
  F.mapHomotopyCategoryPlus.Full
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_span : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  [RingHomClass F R S] (s : Set R), Ideal.map f (Ideal.span s) = Ideal.span (⇑f '' s)
-- Mathlib.AlgebraicGeometry.Cover.Sigma
AlgebraicGeometry.Scheme.Cover.Hom.sigma_s₀ : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme}
  [inst : AlgebraicGeometry.IsZariskiLocalAtSource P] [inst_1 : UnivLE.{v, u}]
  {𝒰 𝒱 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) S} (f : 𝒰 ⟶ 𝒱) (x : 𝒰.sigma.I₀),
  (AlgebraicGeometry.Scheme.Cover.Hom.sigma f).s₀ x = default
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.evaluation_naturality : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {V : Y.Opens} (x : ↥X) (hx : f x ∈ V),
  CategoryTheory.CategoryStruct.comp (Y.evaluation V (f x) hx) (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app f V)
      (X.evaluation ((TopologicalSpace.Opens.map f.base).obj V) x hx)
-- Mathlib.MeasureTheory.Integral.CircleIntegral
deriv_circleMap : ∀ (c : ℂ) (R θ : ℝ), deriv (circleMap c R) θ = circleMap 0 R θ * Complex.I
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensor_id_comp_id_tensor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y Z : C}
  (f : W ⟶ X) (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom g (CategoryTheory.CategoryStruct.id W))
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id Z) f) =
    CategoryTheory.MonoidalCategoryStruct.tensorHom g f
-- Mathlib.Order.SupIndep
Finset.supIndep_sigma_iff' : ∀ {α : Type u_1} {ι : Type u_3} [inst : Lattice α] [IsModularLattice α] [inst_2 : OrderBot α] {β : ι → Type u_5}
  {s : Finset ι} {g : (i : ι) → Finset (β i)} {f : Sigma β → α},
  (s.sigma g).SupIndep f ↔ (s.SupIndep fun i => (g i).sup fun b => f ⟨i, b⟩) ∧ ∀ i ∈ s, (g i).SupIndep fun b => f ⟨i, b⟩
-- Mathlib.Condensed.Light.Sequence
/-- Given a map `π : T → S × OnePoint X`, define a new space `S'` and a map `y : S' ⟶ S` which has
the property that in the Cartesian diagram
```
T' -> S' ⨯ OnePoint X
|         |
v         v
T  -> S  ⨯ OnePoint X
```
there are maps `σ x : S' ⟶ T'` for each `x : OnePoint X` such that
`S' ⨯ OnePoint X ⟶ S' ⟶ T' ⟶ S' ⨯ OnePoint X` is the identity for
all points `⟨s, x⟩ : S' ⨯ OnePoint X`.  -/
_private.Mathlib.Condensed.Light.Sequence.0.InternalProjectivityProof.S' : {S : Type u_1} →
  {T : Type u_2} → {X : Type u_3} → (π : T → S × OnePoint X) → Set ((x : OnePoint X) → ↑(Prod.snd ∘ π ⁻¹' {x}))
-- Mathlib.MeasureTheory.Measure.WithDensityFinite
/-- Auxiliary definition for `MeasureTheory.Measure.toFinite`.  -/
MeasureTheory.Measure.toFiniteAux : {α : Type u_1} →
  {mα : MeasurableSpace α} → (μ : MeasureTheory.Measure α) → [MeasureTheory.SFinite μ] → MeasureTheory.Measure α
-- Mathlib.Algebra.Order.Group.PosPart
negPart_add_posPart : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] [AddLeftMono α] [AddRightMono α] (a : α), a⁻ + a⁺ = |a|
-- Init.Grind.Lemmas
Lean.Grind.or_eq_of_eq_true_left : ∀ {a b : Prop}, a = True → (a ∨ b) = True
-- Mathlib.Order.Filter.Cofinite
/-- If `f` tends to a countably generated filter `l` along `Filter.cofinite`,
then for all but countably many elements, `f x ∈ l.ker`.  -/
Filter.Tendsto.countable_compl_preimage_ker : ∀ {α : Type u_2} {β : Type u_3} {f : α → β} {l : Filter β} [l.IsCountablyGenerated],
  Filter.Tendsto f Filter.cofinite l → (f ⁻¹' l.ker)ᶜ.Countable
-- Mathlib.CategoryTheory.Products.Associator
CategoryTheory.prod.inverseAssociatorIsEquivalence : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E],
  (CategoryTheory.prod.inverseAssociator C D E).IsEquivalence
-- Init.Data.UInt.BasicAux
/-- Converts 32-bit unsigned integers to 16-bit unsigned integers. Wraps around on overflow.

This function is overridden at runtime with an efficient implementation.
 -/
UInt32.toUInt16 : UInt32 → UInt16
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_keysArray : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α] {k : α},
  m.WF → (k ∈ m.keysArray ↔ k ∈ m)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.lift.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst fst_1 : P ⟶ X} (e_fst : fst = fst_1)
  {snd snd_1 : P ⟶ Y} (e_snd : snd = snd_1) {f f_1 : X ⟶ Z} (e_f : f = f_1) {g g_1 : Y ⟶ Z} (e_g : g = g_1)
  (hP : CategoryTheory.IsPullback fst snd f g) {W : C} (h h_1 : W ⟶ X) (e_h : h = h_1) (k k_1 : W ⟶ Y) (e_k : k = k_1)
  (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g),
  hP.lift h k w = ⋯.lift h_1 k_1 ⋯
-- Lean.Elab.DocString
Lean.Doc.CodeBlockSuggestion.mk : Lean.Name → Option String → Option String → Lean.Doc.CodeBlockSuggestion
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.Orthogonal.indefiniteDiagonal.eq_1 : ∀ (p : Type u_2) (q : Type u_3) (R : Type u₂) [inst : DecidableEq p] [inst_1 : DecidableEq q] [inst_2 : CommRing R],
  LieAlgebra.Orthogonal.indefiniteDiagonal p q R = Matrix.diagonal (Sum.elim (fun x => 1) fun x => -1)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.colimitIsoOfIsLeftKanExtension.eq_1 : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : F ⟶ L.comp F') [inst_3 : F'.IsLeftKanExtension α] [inst_4 : CategoryTheory.Limits.HasColimit F]
  [inst_5 : CategoryTheory.Limits.HasColimit F'],
  F'.colimitIsoOfIsLeftKanExtension α =
    (CategoryTheory.Limits.colimit.isColimit F').coconePointUniqueUpToIso
      (F'.isColimitCoconeOfIsLeftKanExtension α (CategoryTheory.Limits.colimit.isColimit F))
-- Mathlib.Algebra.Category.Ring.Basic
/-- The type of morphisms in `CommSemiRingCat`.  -/
CommSemiRingCat.Hom : CommSemiRingCat → CommSemiRingCat → Type u
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Take
Std.Iterators.Types.Take.isPlausibleStep_take_yield : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} {it' : Std.IterM m β} {out : β} [inst : Monad m]
  [inst_1 : Std.Iterator α m β] {n : ℕ} {it : Std.IterM m β},
  it.IsPlausibleStep (Std.IterStep.yield it' out) →
    (Std.IterM.take (n + 1) it).IsPlausibleStep (Std.IterStep.yield (Std.IterM.take n it') out)
-- Std.Time.Date.PlainDate
Std.Time.PlainDate.ext : ∀ {x y : Std.Time.PlainDate}, x.year = y.year → x.month = y.month → x.day = y.day → x = y
-- Mathlib.Lean.Elab.InfoTree
/-- Gets the first child info of each `Lean.Elab.BodyInfo`, which should be the only child, and
should be a `TermInfo`, `PartialTermInfo`, or `TacticInfo`. `getDeclBodyInfos` does not validate
either of these conditions.  -/
Lean.Elab.InfoTree.getDeclBodyInfos : Lean.Elab.InfoTree → List (Lean.Syntax × Lean.Elab.ContextInfo × Lean.Elab.Info)
-- Mathlib.Order.Interval.Set.OrderEmbedding
OrderEmbedding.preimage_Icc : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ↪o β) (x y : α),
  ⇑e ⁻¹' Set.Icc (e x) (e y) = Set.Icc x y
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.full_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} E]
  (e : C ≌ E), e.inverse.Full
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.prop.fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {Φ : CategoryTheory.SmallObject.SuccStruct C} {X Y : C}
  {f : X ⟶ Y} (hf : Φ.prop f), f = CategoryTheory.CategoryStruct.comp (Φ.toSucc X) (CategoryTheory.eqToHom ⋯)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_insertManyIfNewUnit_list : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α] [inst : BEq α]
  [Std.LawfulBEqOrd α] (h : t.WF) {l : List α},
  List.Pairwise (fun a b => ¬compare a b = Ordering.eq) l →
    (∀ a ∈ t, l.contains a = false) →
      (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l ⋯)).size = t.size + l.length
-- Mathlib.Tactic.CategoryTheory.BicategoricalComp
CategoryTheory.BicategoricalCoherence.right : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      (f g : a ⟶ b) →
        [CategoryTheory.BicategoricalCoherence f g] →
          CategoryTheory.BicategoricalCoherence
            (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b)) g
-- Mathlib.Data.Set.Image
Set.preimage_eq_preimage : ∀ {α : Type u_1} {β : Type u_2} {s t : Set α} {f : β → α}, Function.Surjective f → (f ⁻¹' s = f ⁻¹' t ↔ s = t)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Final
/-- The version of `final_of_final_costructuredArrowToOver` on small categories used to prove the
full statement.  -/
_private.Mathlib.CategoryTheory.Comma.StructuredArrow.Final.0.CategoryTheory.Functor.final_of_final_costructuredArrowToOver_small : ∀ {A : Type u₁} [inst : CategoryTheory.SmallCategory A] {B : Type u₁} [inst_1 : CategoryTheory.SmallCategory B]
  {T : Type u₁} [inst_2 : CategoryTheory.SmallCategory T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) [R.Final] [∀ (b : B), (CategoryTheory.CostructuredArrow.toOver L (R.obj b)).Final],
  L.Final
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.toFinset.eq_1 : ∀ {α : Type u} {s : Set α} (h : s.Finite), h.toFinset = s.toFinset
-- Mathlib.Topology.Covering.Quotient
Topology.IsQuotientMap.trivializationOfVAddDisjoint_target : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : AddGroup G] [inst_3 : AddAction G E] (hf : Topology.IsQuotientMap f) [inst_4 : ContinuousConstVAdd G E]
  (hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ AddAction.orbit G e₂) [inst_5 : TopologicalSpace G]
  [inst_6 : DiscreteTopology G] (U : Set E) (open_U : IsOpen U)
  (disjoint : ∀ (g : G), ((fun x => g +ᵥ x) '' U ∩ U).Nonempty → g = 0),
  (hf.trivializationOfVAddDisjoint hfG U open_U disjoint).target = (f '' U) ×ˢ Set.univ
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.induction_linear : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {motive : MonoidAlgebra R M → Prop} (x : MonoidAlgebra R M),
  motive 0 →
    (∀ (x y : MonoidAlgebra R M), motive x → motive y → motive (x + y)) →
      (∀ (m : M) (r : R), motive (MonoidAlgebra.single m r)) → motive x
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.symm_linearMapAt : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : AddCommMonoid F]
  [inst_5 : Module R F] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module R (E x)]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_8 : Bundle.Trivialization.IsLinear R e] {b : B},
  b ∈ e.baseSet → ∀ (y : E b), e.symm b ((Bundle.Trivialization.linearMapAt R e b) y) = y
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
NonUnitalStarAlgHom.mk.congr_simp : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : Star B] (toNonUnitalAlgHom toNonUnitalAlgHom_1 : A →ₙₐ[R] B)
  (e_toNonUnitalAlgHom : toNonUnitalAlgHom = toNonUnitalAlgHom_1)
  (map_star' : ∀ (a : A), toNonUnitalAlgHom.toFun (star a) = star (toNonUnitalAlgHom.toFun a)),
  { toNonUnitalAlgHom := toNonUnitalAlgHom, map_star' := map_star' } =
    { toNonUnitalAlgHom := toNonUnitalAlgHom_1, map_star' := ⋯ }
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.dvd_of_dvd_mul_right : ∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsCoprime x z → x ∣ y * z → x ∣ y
-- Mathlib.Analysis.Convex.Function
ConvexOn.openSegment_subset_strict_epigraph : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [IsOrderedCancelAddMonoid β] [inst_6 : Module 𝕜 E]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] {s : Set E} {f : E → β},
  ConvexOn 𝕜 s f →
    ∀ (p q : E × β), p.1 ∈ s ∧ f p.1 < p.2 → q.1 ∈ s ∧ f q.1 ≤ q.2 → openSegment 𝕜 p q ⊆ {p | p.1 ∈ s ∧ f p.1 < p.2}
-- Mathlib.Analysis.Normed.Group.Basic
norm_pow_le_mul_norm : ∀ {E : Type u_5} [inst : SeminormedGroup E] {a : E} {n : ℕ}, ‖a ^ n‖ ≤ ↑n * ‖a‖
-- Mathlib.Util.Notation3
/-- Matches lambdas. The `matchBody` takes the fvar introduced when visiting the body.  -/
Mathlib.Notation3.matchLambda : Mathlib.Notation3.Matcher → (Lean.Expr → Mathlib.Notation3.Matcher) → Mathlib.Notation3.Matcher
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.getEntry?.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α), Std.Internal.List.getEntry? a [] = none
-- Mathlib.FieldTheory.PolynomialGaloisGroup
Polynomial.Gal.mapRoots_bijective : ∀ {F : Type u_1} [inst : Field F] (p : Polynomial F) (E : Type u_2) [inst_1 : Field E] [inst_2 : Algebra F E]
  [h : Fact (Polynomial.map (algebraMap F E) p).Splits], Function.Bijective (Polynomial.Gal.mapRoots p E)
-- Mathlib.Order.Std
/-- Arguments for `LinearOrder.ofStd`; see that function for details.  -/
LinearOrder.OfStdArgs : Type u_1 → Type u_1
-- Mathlib.Algebra.DirectSum.Ring
/-- The `CommSemiring` structure derived from `GCommSemiring A`.  -/
DirectSum.instCommSemiringOfNat : {ι : Type u_1} →
  [DecidableEq ι] →
    (A : ι → Type u_2) →
      [inst : (i : ι) → AddCommMonoid (A i)] →
        [inst_1 : AddCommMonoid ι] → [DirectSum.GCommSemiring A] → CommSemiring (A 0)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintLabelPart.tooltip? : Lean.Lsp.InlayHintLabelPart → Option Lean.Lsp.InlayHintTooltip
-- Init.Data.Option.Lemmas
Option.map_map : ∀ {β : Type u_1} {γ : Type u_2} {α : Type u_3} (h : β → γ) (g : α → β) (x : Option α),
  Option.map h (Option.map g x) = Option.map (h ∘ g) x
-- Mathlib.Algebra.Homology.Embedding.TruncGE
/-- The canonical truncation of a homological complex relative to an embedding
of complex shapes `e` which satisfies `e.IsTruncGE`.  -/
HomologicalComplex.truncGE' : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              (K : HomologicalComplex C c') →
                (e : c.Embedding c') → [e.IsTruncGE] → [∀ (i' : ι'), K.HasHomology i'] → HomologicalComplex C c
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.inv_zero : ∀ {R : Type u_2} [inst : Semifield R], 0⁻¹ = 0
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.normalizedFactors_zero : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α],
  UniqueFactorizationMonoid.normalizedFactors 0 = 0
-- Mathlib.Algebra.Symmetrized
SymAlg.sym_add : ∀ {α : Type u_1} [inst : Add α] (a b : α), SymAlg.sym (a + b) = SymAlg.sym a + SymAlg.sym b
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- State for each `CommSemiring` processed by this module.
Recall that `CommSemiring` are processed using the envelop `OfCommSemiring.Q`
 -/
Lean.Meta.Grind.Arith.CommRing.CommSemiring : Type
-- Mathlib.NumberTheory.DirichletCharacter.Orthogonality
/-- If `R` is an integral domain that has enough roots of unity and `n ≠ 0`, then
for each `a ≠ 1` in `ZMod n`, the sum of `χ a` over all Dirichlet characters mod `n`
with values in `R` vanishes.  -/
DirichletCharacter.sum_characters_eq_zero : ∀ (R : Type u_1) [inst : CommRing R] {n : ℕ} [NeZero n] [HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)]
  [inst_3 : IsDomain R] ⦃a : ZMod n⦄, a ≠ 1 → ∑ χ, χ a = 0
-- Mathlib.FieldTheory.Differential.Basic
algebraMap.coe_logDeriv : ∀ {F : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field K] [inst_2 : Differential F] [inst_3 : Differential K]
  [inst_4 : Algebra F K] [DifferentialAlgebra F K] (a : F), ↑(Differential.logDeriv a) = Differential.logDeriv ↑a
-- Mathlib.LinearAlgebra.Finsupp.LSum
Finsupp.domLCongr_apply : ∀ {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α₁ : Type u_9}
  {α₂ : Type u_10} (e : α₁ ≃ α₂) (v : α₁ →₀ M), (Finsupp.domLCongr e) v = (Finsupp.domCongr e) v
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalCategory.tensorμ.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X₁ X₂ Y₁ Y₂ : C),
  CategoryTheory.MonoidalCategory.tensorμ X₁ X₂ Y₁ Y₂ =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂
          (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ Y₂)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁
          (CategoryTheory.MonoidalCategoryStruct.associator X₂ Y₁ Y₂).inv)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁
            (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X₂ Y₁).hom Y₂))
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁
              (CategoryTheory.MonoidalCategoryStruct.associator Y₁ X₂ Y₂).hom)
            (CategoryTheory.MonoidalCategoryStruct.associator X₁ Y₁
                (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ Y₂)).inv)))
-- ProofWidgets.Data.Html
ProofWidgets.Html.component.sizeOf_spec : ∀ (a : UInt64) (a_1 : String) (a_2 : ProofWidgets.LazyEncodable Lean.Json) (a_3 : Array ProofWidgets.Html),
  sizeOf (ProofWidgets.Html.component a a_1 a_2 a_3) = 1 + sizeOf a + sizeOf a_1 + sizeOf a_3
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
MeasureTheory.Measure.ae_le_iff_absolutelyContinuous : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  MeasureTheory.ae μ ≤ MeasureTheory.ae ν ↔ μ.AbsolutelyContinuous ν
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupNorm.instSemilatticeSup : {E : Type u_3} → [inst : Group E] → SemilatticeSup (GroupNorm E)
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.mk.inj : ∀ {X : Type u_1} {Y : Type u_2} {inst : PseudoEMetricSpace X} {inst_1 : PseudoEMetricSpace Y} {toEquiv : X ≃ Y}
  {edist_eq' : ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (toEquiv.toFun x) (toEquiv.toFun y) = ↑r * edist x y} {toEquiv_1 : X ≃ Y}
  {edist_eq'_1 : ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (toEquiv_1.toFun x) (toEquiv_1.toFun y) = ↑r * edist x y},
  { toEquiv := toEquiv, edist_eq' := edist_eq' } = { toEquiv := toEquiv_1, edist_eq' := edist_eq'_1 } →
    toEquiv = toEquiv_1
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork_φK : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (hg : S.g = 0) (c : CategoryTheory.Limits.KernelFork S.g)
  (hc : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork S hf hg c hc).φK =
    CategoryTheory.Limits.Fork.ι c
-- Mathlib.Order.Interval.Basic
Interval.dual_pure : ∀ {α : Type u_1} [inst : Preorder α] (a : α), Interval.dual (Interval.pure a) = Interval.pure (OrderDual.toDual a)
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
/-- Every `NonPreadditiveAbelian` category is preadditive.  -/
CategoryTheory.NonPreadditiveAbelian.preadditive : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.NonPreadditiveAbelian C] → CategoryTheory.Preadditive C
-- Mathlib.Data.Ordmap.Ordnode
Ordnode.toBinaryTree_toOrdNode : ∀ {α : Type u_1} (b : BinaryTree α), b.toOrdNode.toBinaryTree = b
-- Mathlib.Data.Set.Lattice
/-- **Alias** of `Set.sdiff_iInter`. -/
Set.diff_iInter : ∀ {β : Type u_2} {ι : Sort u_5} (s : Set β) (t : ι → Set β), s \ ⋂ i, t i = ⋃ i, s \ t i
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- Definition for $\oint_{|z-c|=R} f(z)\,dz$  -/
circleIntegral : {E : Type u_1} → [inst : NormedAddCommGroup E] → [NormedSpace ℂ E] → (ℂ → E) → ℂ → ℝ → E
-- Mathlib.Data.Matrix.Basic
AddEquiv.entryAddHom_comp_mapMatrix : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} [inst : Add α] [inst_1 : Add β] (f : α ≃+ β) (i : m)
  (j : n), (Matrix.entryAddHom β i j).comp ↑f.mapMatrix = (↑f).comp (Matrix.entryAddHom α i j)
-- Lean.Language.Basic
/-- Tree of snapshots where each snapshot comes with an array of asynchronous further subtrees. Used
for asynchronously collecting information about the entirety of snapshots in the language server.
The involved tasks may form a DAG on the `Task` dependency level but this is not captured by this
data structure.  -/
Lean.Language.SnapshotTree : Type
-- Lean.Server.Requests
Lean.Server.RequestContext.rpcSessions : Lean.Server.RequestContext → Std.TreeMap UInt64 (IO.Ref Lean.Server.FileWorker.RpcSession) compare