mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Module.FiniteDimension
AffineEquiv.toAffineEquiv_toContinuousAffineEquiv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type w} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : CompleteSpace 𝕜] {PE : Type u_1} {PF : Type u_2} [inst_6 : MetricSpace PE] [inst_7 : NormedAddTorsor E PE]
  [inst_8 : MetricSpace PF] [inst_9 : NormedAddTorsor F PF] [inst_10 : FiniteDimensional 𝕜 E] (f : PE ≃ᵃ[𝕜] PF),
  ↑(AffineEquiv.toContinuousAffineEquiv f) = f
-- Mathlib.CategoryTheory.Subfunctor.Finite
CategoryTheory.PresheafIsGeneratedBy.range : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {ι : Type w'}
  {X : ι → Cᵒᵖ} {x : (i : ι) → F.obj (X i)},
  CategoryTheory.PresheafIsGeneratedBy F x →
    ∀ {F' : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : F ⟶ F'),
      (CategoryTheory.Subfunctor.range f).IsGeneratedBy fun i =>
        (CategoryTheory.ConcreteCategory.hom (f.app (X i))) (x i)
-- Lean.PrettyPrinter.Delaborator.Basic
_private.Lean.PrettyPrinter.Delaborator.Basic.0.Lean.PrettyPrinter.Delaborator.addTermInfo.mkTermInfo : Lean.Syntax → Lean.Expr → Bool → Lean.PrettyPrinter.Delaborator.DelabM Lean.Elab.TermInfo
-- Mathlib.LinearAlgebra.Trace
Matrix.trace_toLin_eq : ∀ {R : Type u} [inst : CommSemiring R] {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type w}
  [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] (A : Matrix ι ι R) (b : Module.Basis ι R M),
  (LinearMap.trace R M) ((Matrix.toLin b b) A) = A.trace
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for the horizontal composition `η ◫ θ`.  -/
Mathlib.Tactic.BicategoryLike.MonadMor₂.horizontalCompM : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadMor₂ m] →
    Mathlib.Tactic.BicategoryLike.Mor₂ → Mathlib.Tactic.BicategoryLike.Mor₂ → m Mathlib.Tactic.BicategoryLike.Mor₂
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_sub' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIocDiv hp (a - p) b = toIocDiv hp a b + 1
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.next_π₂ : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} (c₁ : ComplexShape I₁) {c₂ : ComplexShape I₂}
  (c₁₂ : ComplexShape I₁₂) [inst : TotalComplexShape c₁ c₂ c₁₂] (i₁ : I₁) {i₂ i₂' : I₂},
  c₂.Rel i₂ i₂' → c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂)) = c₁.π c₂ c₁₂ (i₁, i₂')
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
CategoryTheory.Over.conePostIso_inv_app_hom : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) (i : J) (X : CategoryTheory.Limits.Cone F),
  ((CategoryTheory.Over.conePostIso F i).inv.app X).hom = CategoryTheory.CategoryStruct.id X.pt
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.tail.eq_1 : ∀ {α : Type u_1} (le : α → α → Bool) (h : Batteries.PairingHeapImp.Heap α),
  Batteries.PairingHeapImp.Heap.tail le h =
    (Batteries.PairingHeapImp.Heap.tail? le h).getD Batteries.PairingHeapImp.Heap.nil
-- Mathlib.NumberTheory.NumberField.CMField
/-- The equiv between the infinite places of `K` and the infinite places of `K⁺` induced by the
restriction to `K⁺`, see `equivInfinitePlace_apply`.
 -/
NumberField.IsCMField.equivInfinitePlace : (K : Type u_1) →
  [inst : Field K] →
    [inst_1 : CharZero K] →
      [NumberField.IsCMField K] →
        [NumberField K] → NumberField.InfinitePlace K ≃ NumberField.InfinitePlace ↥(NumberField.maximalRealSubfield K)
-- Mathlib.Analysis.BoxIntegral.Partition.Measure
BoxIntegral.BoxAdditiveMap.volume_apply : ∀ {ι : Type u_1} [inst : Fintype ι] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  (I : BoxIntegral.Box ι) (x : E), (BoxIntegral.BoxAdditiveMap.volume I) x = (∏ j, (I.upper j - I.lower j)) • x
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.extend_iUnion_le_tsum_nat' : ∀ {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal}
  (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)),
  (∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯) →
    ∀ (s : ℕ → Set α), MeasureTheory.extend m (⋃ i, s i) ≤ ∑' (i : ℕ), MeasureTheory.extend m (s i)
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.instZero : {α : Type u_1} →
  {β : Type u_2} → {mα : MeasurableSpace α} → {mβ : MeasurableSpace β} → Zero (ProbabilityTheory.Kernel α β)
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.comp_toAlgHom : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Semiring C] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R C]
  [inst_7 : CoalgebraStruct R A] [inst_8 : CoalgebraStruct R B] [inst_9 : CoalgebraStruct R C] (φ₁ : B →ₐc[R] C)
  (φ₂ : A →ₐc[R] B), ↑(φ₁.comp φ₂) = (↑φ₁).comp ↑φ₂
-- Init.Data.Array.Lemmas
Array.elem_iff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {xs : Array α}, Array.elem a xs = true ↔ a ∈ xs
-- Mathlib.Algebra.Ring.Opposite
MulOpposite.instNonAssocSemiring : {R : Type u_1} → [NonAssocSemiring R] → NonAssocSemiring Rᵐᵒᵖ
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.connectivity_le_expansion : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {K : ℝ} {A S : Finset G},
  K ≤ 1 → S.Nonempty → A.Nonempty → Finset.connectivity✝ K S ≤ Finset.expansion✝ K S A
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
Finset.measurableSet_biInter : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : β → Set α} (s : Finset β),
  (∀ b ∈ s, MeasurableSet (f b)) → MeasurableSet (⋂ b ∈ s, f b)
-- Mathlib.Analysis.Meromorphic.Basic
MeromorphicAt.add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f g : 𝕜 → E}, MeromorphicAt f x → MeromorphicAt g x → MeromorphicAt (f + g) x
-- Batteries.Recycling.MonadSatisfying.Array
Array.SatisfiesM_foldrM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {as : Array α} {init : β}
  {motive : ℕ → β → Prop} {f : α → β → m β},
  motive as.size init →
    (∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → SatisfiesM (motive ↑i) (f as[i] b)) →
      SatisfiesM (motive 0) (Array.foldrM f init as)
-- Init.Data.List.Perm
List.replicate_perm : ∀ {α : Type u_1} {n : ℕ} {a : α} {l : List α}, (List.replicate n a).Perm l ↔ List.replicate n a = l
-- Std.Http.Data.Status
Std.Http.Status.instEncodeV11 : Std.Http.Internal.Encode Std.Http.Version.v11 Std.Http.Status
-- Lean.Elab.Match
Lean.Elab.Term.ToDepElimPattern.TopSort.State.mk.inj : ∀ {visitedFVars : Lean.FVarIdSet} {visitedMVars : Lean.MVarIdSet} {result : Array Lean.Expr}
  {visitedFVars_1 : Lean.FVarIdSet} {visitedMVars_1 : Lean.MVarIdSet} {result_1 : Array Lean.Expr},
  { visitedFVars := visitedFVars, visitedMVars := visitedMVars, result := result } =
      { visitedFVars := visitedFVars_1, visitedMVars := visitedMVars_1, result := result_1 } →
    visitedFVars = visitedFVars_1 ∧ visitedMVars = visitedMVars_1 ∧ result = result_1
-- Mathlib.Data.ZMod.Basic
ZMod.val_mul_le : ∀ {n : ℕ} (a b : ZMod n), (a * b).val ≤ a.val * b.val
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
CategoryTheory.Limits.pullbackAssoc_hom_snd_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁)
  (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [inst_1 : CategoryTheory.Limits.HasPullback f₁ f₂]
  [inst_2 : CategoryTheory.Limits.HasPullback f₃ f₄]
  [inst_3 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃)
      f₄]
  [inst_4 :
    CategoryTheory.Limits.HasPullback f₁
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)]
  {Z : C} (h : X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd f₁
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₃ f₄) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄)
      h
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.isLittleOTVS_neg_left : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {f : α → E} {g : α → F} [ContinuousNeg E],
  (-f) =o[𝕜; l] g ↔ f =o[𝕜; l] g
-- Mathlib.Data.Stream.Init
Stream'.head_zip : ∀ {α : Type u} {β : Type v} {δ : Type w} (f : α → β → δ) (s₁ : Stream' α) (s₂ : Stream' β),
  (Stream'.zip f s₁ s₂).head = f s₁.head s₂.head
-- Mathlib.Topology.EMetricSpace.Defs
/-- The product of two pseudoemetric spaces, with the max distance, is an extended
pseudometric spaces. We make sure that the uniform structure thus constructed is the one
corresponding to the product of uniform spaces, to avoid diamond problems.  -/
Prod.pseudoEMetricSpaceMax : {α : Type u} → {β : Type v} → [PseudoEMetricSpace α] → [PseudoEMetricSpace β] → PseudoEMetricSpace (α × β)
-- Mathlib.Control.Fold
Traversable.foldrm : {α β : Type u} →
  {t : Type u → Type u} → [Traversable t] → {m : Type u → Type u} → [Monad m] → (α → β → m β) → β → t α → m β
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.monoidHomSubgroup_apply : ∀ {G : Type u_2} [inst : Group G] {H K : Subgroup G} (h : K ≤ Subgroup.normalizer ↑H)
  (a : ↥H ⋊[H.normalizerMonoidHom.comp (Subgroup.inclusion h)] ↥K),
  (SemidirectProduct.monoidHomSubgroup h) a = ↑a.left * ↑a.right
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.IsSt.not_infinite : ∀ {x : ℝ*} {r : ℝ}, x.IsSt r → ¬x.Infinite
-- Init.Data.Int.DivMod.Lemmas
Int.mul_lt_mul_left : ∀ {a b c : ℤ}, 0 < a → (a * b < a * c ↔ b < c)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SetLike.vadd'.eq_1 : ∀ {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [inst : SetLike S α] [inst_1 : VAdd M N] [inst_2 : VAdd M α]
  [inst_3 : AddMonoid N] [inst_4 : AddAction N α] [inst_5 : VAddMemClass S N α] [inst_6 : VAddAssocClass M N α] (s : S),
  SetLike.vadd' s = { vadd := fun r x => ⟨r +ᵥ ↑x, ⋯⟩ }
-- Lean.Expr
Lean.Expr.litValue! : Lean.Expr → Lean.Literal
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.hsum_add : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R]
  {s t : HahnSeries.SummableFamily Γ R α}, (s + t).hsum = s.hsum + t.hsum
-- Mathlib.Tactic.Linter.OverlappingInstances
/-- Find classes for which multiple different instances can be synthesized in the local context.
The result maps classes to the (at least 2) local instances that generate them.  -/
_private.Mathlib.Tactic.Linter.OverlappingInstances.0.Mathlib.Linter.OverlappingInstances.findOverlappingInstances : Lean.MetaM (Lean.ExprMap (Array Lean.FVarId))
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.isUnit_of_dvd' : ∀ {R : Type u} [inst : CommSemiring R] {a b x : R}, IsCoprime a b → x ∣ a → x ∣ b → IsUnit x
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
SimpleGraph.isUniform_one : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (G : SimpleGraph α)
  [inst_3 : DecidableRel G.Adj] {s t : Finset α}, G.IsUniform 1 s t
-- Mathlib.Data.Fintype.Card
Finite.wellFounded_of_trans_of_irrefl : ∀ {α : Type u_1} [Finite α] (r : α → α → Prop) [IsTrans α r] [Std.Irrefl r], WellFounded r
-- Mathlib.MeasureTheory.Group.Integral
/-- Translating a function by right-addition does not change its integral with respect to a
right-invariant measure.  -/
MeasureTheory.integral_add_right_eq_self : ∀ {G : Type u_4} {E : Type u_5} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure G} [inst_3 : AddGroup G] [MeasurableAdd G] [μ.IsAddRightInvariant] (f : G → E) (g : G),
  ∫ (x : G), f (x + g) ∂μ = ∫ (x : G), f x ∂μ
-- Mathlib.CategoryTheory.PathCategory.Basic
/-- Composition of paths as functor from the path category of a category to the category.  -/
CategoryTheory.pathComposition : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Functor (CategoryTheory.Paths C) C
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.BuilderOption.index : Aesop.IndexingMode → Aesop.Frontend.BuilderOption
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.contains'.match_3.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) (size : ℕ) (k' : α) (v : β k')
  (l r : Std.DTreeMap.Internal.Impl α β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k' : α) →
        (v : β k') → (l r : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner size k' v l r)),
  (match Std.DTreeMap.Internal.Impl.inner size k' v l r with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k' v l r => h_2 size k' v l r) =
    h_2 size k' v l r
-- Mathlib.CategoryTheory.Types.Basic
Equiv.toIso_inv_hom_apply : ∀ {X Y : Type u} (e : X ≃ Y) (x : Y), (CategoryTheory.ConcreteCategory.hom e.toIso.inv) x = e.symm x
-- Mathlib.FieldTheory.RatFunc.Basic
/-- The multiplicative unit of rational functions.  -/
RatFunc.one : {K : Type u_1} → [inst : CommRing K] → RatFunc K
-- Mathlib.Algebra.Order.Floor.Defs
Nat.ceil_nat : Nat.ceil = id
-- Mathlib.Topology.Sheaves.SheafCondition.Sites
/-- If `R` is a presieve in the Grothendieck topology on `Opens X`, the covering family associated
to `R` really is _covering_, i.e. the union of all open sets equals `U`.
 -/
TopCat.Presheaf.coveringOfPresieve.iSup_eq_of_mem_grothendieck : ∀ {X : TopCat} (U : TopologicalSpace.Opens ↑X) (R : CategoryTheory.Presieve U),
  CategoryTheory.Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) U →
    iSup (TopCat.Presheaf.coveringOfPresieve U R) = U
-- Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid
/-- `toStrongNormalizedGCDMonoid` constructs a GCD monoid out of a strong normalization on a
unique factorization domain.  -/
UniqueFactorizationMonoid.toStrongNormalizedGCDMonoid : (α : Type u_2) →
  [inst : CommMonoidWithZero α] →
    [UniqueFactorizationMonoid α] → [StrongNormalizationMonoid α] → StrongNormalizedGCDMonoid α
-- Mathlib.CategoryTheory.LiftingProperties.Basic
CategoryTheory.HasLiftingProperty.iff_op : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} {i : A ⟶ B} {p : X ⟶ Y},
  CategoryTheory.HasLiftingProperty i p ↔ CategoryTheory.HasLiftingProperty p.op i.op
-- Mathlib.Order.Interval.Set.Defs
Set.Icc_def : ∀ {α : Type u_1} [inst : Preorder α] (a b : α), {x | a ≤ x ∧ x ≤ b} = Set.Icc a b
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Equivalence.rightOp_inverse_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : Cᵒᵖ ≌ D) (X : Dᵒᵖ), e.rightOp.inverse.obj X = Opposite.unop (e.inverse.obj (Opposite.unop X))
-- Std.Data.HashMap.Basic
/-- Two hash maps are equivalent in the sense of `Equiv` iff
all the keys and values are equal.
 -/
Std.HashMap.«term_~m_» : Lean.TrailingParserDescr
-- Mathlib.NumberTheory.NumberField.Discriminant.Basic
/-- If `|discr K| ≤ N` then the degree of `K` is at most `rankOfDiscrBdd`.  -/
NumberField.hermiteTheorem.rank_le_rankOfDiscrBdd : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {N : ℕ},
  |NumberField.discr K| ≤ ↑N → Module.finrank ℚ K ≤ NumberField.hermiteTheorem.rankOfDiscrBdd N
-- Mathlib.SetTheory.ZFC.Class
ZFSet.coeEquiv_apply_coe : ∀ (x : ZFSet.{u}), ↑(ZFSet.coeEquiv x) = ↑x
-- Mathlib.Tactic.TermCongr
Mathlib.Tactic.TermCongr.CongrType.heq : Mathlib.Tactic.TermCongr.CongrType
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.SelectM.State.thms : Lean.Meta.Grind.SelectM.State✝ → Array Lean.Meta.Grind.EMatchTheorem
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
DerivedCategory.from_singleFunctor_obj_eq_zero_of_projective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {P : C} [CategoryTheory.Projective P] {L : CochainComplex C ℤ} {i : ℤ}
  (φ : DerivedCategory.Q.obj ((CochainComplex.singleFunctor C i).obj P) ⟶ DerivedCategory.Q.obj L),
  ∀ n < i, ∀ [L.IsStrictlyLE n], φ = 0
-- Mathlib.Computability.EpsilonNFA
εNFA.stepSet_empty : ∀ {α : Type u} {σ : Type v} {M : εNFA α σ} (a : α), M.stepSet ∅ a = ∅
-- Mathlib.Order.Interval.Set.Image
MonotoneOn.mapsTo_Ici : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a : α},
  MonotoneOn f (Set.Ici a) → Set.MapsTo f (Set.Ici a) (Set.Ici (f a))
-- Init.Data.UInt.Lemmas
USize.lt_of_le_of_ne : ∀ {a b : USize}, a ≤ b → a ≠ b → a < b
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatIso.op_symm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ≅ G), CategoryTheory.NatIso.op α.symm = (CategoryTheory.NatIso.op α).symm
-- Mathlib.CategoryTheory.Limits.MonoCoprod
CategoryTheory.Limits.MonoCoprod.instMonoInl : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B : C} [CategoryTheory.Limits.MonoCoprod C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct A B], CategoryTheory.Mono CategoryTheory.Limits.coprod.inl
-- Mathlib.Topology.Compactification.OnePoint.Basic
/-- If `X` is not a compact space, then the natural embedding `X → OnePoint X` has dense range.
 -/
OnePoint.denseRange_coe : ∀ {X : Type u_1} [inst : TopologicalSpace X] [NoncompactSpace X], DenseRange OnePoint.some
-- Mathlib.CategoryTheory.Limits.Lattice
CategoryTheory.Limits.CompleteLattice.finiteColimitCocone_isColimit_desc : ∀ {α : Type u} {J : Type w} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.FinCategory J]
  [inst_2 : SemilatticeSup α] [inst_3 : OrderBot α] (F : CategoryTheory.Functor J α)
  (s : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.Limits.CompleteLattice.finiteColimitCocone F).isColimit.desc s = CategoryTheory.homOfLE ⋯
-- Mathlib.Analysis.Normed.Lp.ProdLp
LinearIsometryEquiv.withLpProdComm_symm : ∀ (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : Semiring 𝕜]
  [inst_1 : SeminormedAddCommGroup α] [inst_2 : Module 𝕜 α] [inst_3 : SeminormedAddCommGroup β] [inst_4 : Module 𝕜 β],
  (LinearIsometryEquiv.withLpProdComm p 𝕜 α β).symm = LinearIsometryEquiv.withLpProdComm p 𝕜 β α
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.lift_coe : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddGroup α] (h : Function.Periodic f c) (a : α),
  h.lift ↑a = f a
-- Mathlib.Tactic.NormNum.NatLog
/-- Evaluates the `Nat.log` function.
 -/
Mathlib.Meta.NormNum.evalNatLog : Mathlib.Meta.NormNum.NormNumExt
-- Std.Internal.Parsec.ByteArray
/-- Skips until a predicate is satisfied.
 -/
Std.Internal.Parsec.ByteArray.skipUntil : (UInt8 → Bool) → Std.Internal.Parsec.ByteArray.Parser Unit
-- Mathlib.Logic.Equiv.Basic
/-- Transport dependent functions through an equality of sets.  -/
Equiv.piCongrSet : {α : Type u_11} →
  {W : α → Sort w} → {s t : Set α} → s = t → ((i : { i // i ∈ s }) → W ↑i) ≃ ((i : { i // i ∈ t }) → W ↑i)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
mulintEquivOfZPowersEqTop_strictAnti : ∀ {G : Type u_2} [inst : Infinite G] [inst_1 : CommGroup G] [inst_2 : PartialOrder G] [IsOrderedMonoid G] {g : G}
  (hg : Subgroup.zpowers g = ⊤), g < 1 → StrictAnti ⇑(intEquivOfZPowersEqTop g hg)
-- Mathlib.Data.Set.Card
Set.one_lt_ncard : ∀ {α : Type u_1} {s : Set α}, autoParam s.Finite Set.one_lt_ncard._auto_1 → (1 < s.ncard ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b)
-- Mathlib.NumberTheory.MulChar.Duality
/-- The cardinality of the group of `R`-valued multiplicative characters on a finite commutative
monoid `M` is the same as that of its unit group `Mˣ` when `R` is a ring that has enough roots
of unity.  -/
MulChar.card_eq_card_units_of_hasEnoughRootsOfUnity : ∀ (M : Type u_1) (R : Type u_2) [inst : CommMonoid M] [inst_1 : CommRing R] [Finite M]
  [HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)], Nat.card (MulChar M R) = Nat.card Mˣ
-- Mathlib.Data.Nat.Squarefree
Nat.coprime_div_gcd_of_squarefree : ∀ {m n : ℕ}, Squarefree m → n ≠ 0 → (m / m.gcd n).Coprime n
-- Mathlib.GroupTheory.Perm.Subgroup
Equiv.Perm.subtypeCongrHom.card_range : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] [inst_1 : Fintype ↥(Equiv.Perm.subtypeCongrHom p).range]
  [inst_2 : Fintype (Equiv.Perm { a // p a } × Equiv.Perm { a // ¬p a })],
  Fintype.card ↥(Equiv.Perm.subtypeCongrHom p).range = Fintype.card (Equiv.Perm { a // p a } × Equiv.Perm { a // ¬p a })
-- Init.Data.UInt.Bitwise
USize.shiftRight_or : ∀ {a b c : USize}, (a ||| b) >>> c = a >>> c ||| b >>> c
-- Init.Data.UInt.Bitwise
UInt8.toUInt16_shiftLeft_of_lt : ∀ (a b : UInt8), b < 8 → (a <<< b).toUInt16 = a.toUInt16 <<< b.toUInt16 % 256
-- Init.Data.List.Impl
List.findSomeRev?.eq_1 : ∀ {α : Type u} {β : Type v} (f : α → Option β), List.findSomeRev? f [] = none
-- Mathlib.Topology.NhdsSet
nhdsSet_sInter_le : ∀ {X : Type u_2} [inst : TopologicalSpace X] (s : Set (Set X)), nhdsSet (⋂₀ s) ≤ ⨅ x ∈ s, nhdsSet x
-- Aesop.Tree.TreeM
Aesop.TreeM.Context.mk.injEq : ∀ (currentIteration : Aesop.Iteration) (ruleSet : Aesop.LocalRuleSet) (currentIteration_1 : Aesop.Iteration)
  (ruleSet_1 : Aesop.LocalRuleSet),
  ({ currentIteration := currentIteration, ruleSet := ruleSet } =
      { currentIteration := currentIteration_1, ruleSet := ruleSet_1 }) =
    (currentIteration = currentIteration_1 ∧ ruleSet = ruleSet_1)
-- Lean.Util.Path
Lean.getBuiltinSearchPath : System.FilePath → IO Lean.SearchPath
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.FinitePlace.hasFiniteMulSupport_fun_pow_multiplicity : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {M : Type u_3} [inst_2 : CommMonoid M]
  {I : Ideal (NumberField.RingOfIntegers K)},
  I ≠ ⊥ →
    ∀ (f : Ideal (NumberField.RingOfIntegers K) → M),
      Function.HasFiniteMulSupport fun v => f v.maximalIdeal.asIdeal ^ multiplicity v.maximalIdeal.asIdeal I
-- Mathlib.Combinatorics.Enumerative.Stirling
Nat.stirlingFirst_eq_zero_of_lt : ∀ {n k : ℕ}, n < k → n.stirlingFirst k = 0
-- Lean.Meta.Tactic.Grind.Internalize
Lean.Meta.Grind.preprocessTheorem : Lean.Meta.Grind.EMatchTheorem → ℕ → Lean.Meta.Grind.GoalM Lean.Meta.Grind.EMatchTheorem
-- Lean.Elab.Tactic.Grind.Config
Lean.Elab.Tactic.elabGrobnerConfig : Lean.Syntax → optParam Lean.Grind.GrobnerConfig { } → optParam Bool true → Lean.Elab.Tactic.TacticM Lean.Grind.Config
-- Lean.Parser.Term
Lean.Parser.Term.logNamedWarningMacro.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.LinearAlgebra.BilinearForm.Hom
LinearMap.BilinForm.linMulLin_compLeft : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {f g : M →ₗ[R] R} (l : M →ₗ[R] M),
  (LinearMap.BilinForm.linMulLin f g).compLeft l = LinearMap.BilinForm.linMulLin (f ∘ₗ l) g
-- Init.Data.Iterators.Combinators.Monadic.Append
Std.Iterators.Types.Append.instIteratorLoop : {m : Type w → Type w'} →
  {β α₁ α₂ : Type w} →
    {n : Type x → Type x'} →
      [inst : Monad m] →
        [Monad n] →
          [inst_2 : Std.Iterator α₁ m β] →
            [inst_3 : Std.Iterator α₂ m β] → Std.IteratorLoop (Std.Iterators.Types.Append α₁ α₂ m β) m n
-- Mathlib.Order.Filter.Pointwise
Filter.addAction.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : AddMonoid α] [inst_1 : AddAction α β],
  Filter.addAction = { toVAdd := Filter.instVAdd, add_vadd := ⋯, zero_vadd := ⋯ }