mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.ofIso_left_K : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) (h : S₁.HomologyData),
  (CategoryTheory.ShortComplex.HomologyData.ofIso e h).left.K = h.left.K
-- Mathlib.Order.Hom.Lattice
LatticeHom.subtypeVal_apply : ∀ {β : Type u_3} [inst : Lattice β] {P : β → Prop} (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y))
  (Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)) (x : { x // P x }), (LatticeHom.subtypeVal Psup Pinf) x = ↑x
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
HomotopicalAlgebra.FibrantObject.homMk_homMk_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_2 : CategoryTheory.Limits.HasTerminal C] {X Y Z : C} [inst_3 : HomotopicalAlgebra.IsFibrant X]
  [inst_4 : HomotopicalAlgebra.IsFibrant Y] [inst_5 : HomotopicalAlgebra.IsFibrant Z] (f : X ⟶ Y) (g : Y ⟶ Z)
  {Z_1 : HomotopicalAlgebra.FibrantObject C} (h : HomotopicalAlgebra.FibrantObject.mk Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.FibrantObject.homMk f)
      (CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.FibrantObject.homMk g) h) =
    CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.FibrantObject.homMk (CategoryTheory.CategoryStruct.comp f g))
      h
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
/-- The alternating coface map complex, as a functor  -/
AlgebraicTopology.alternatingCofaceMapComplex : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      CategoryTheory.Functor (CategoryTheory.CosimplicialObject C) (CochainComplex C ℕ)
-- Lean.Expr
Lean.mkLambdaEx : Lean.Name → Lean.Expr → Lean.Expr → Lean.BinderInfo → Lean.Expr
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.nle : ℕ → ℕ → Lean.Expr → Mathlib.Tactic.Order.AtomicFact
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.toSubMulAction_inj : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {p q : Submodule R M},
  p.toSubMulAction = q.toSubMulAction ↔ p = q
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.exists_eq_const : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [PreconnectedSpace X] [Nonempty Y] {f : X → Y},
  IsLocallyConstant f → ∃ y, f = Function.const X y
-- Mathlib.Data.Finset.Slice
/-- `A` is in the `r`-th slice of `𝒜` iff it's in `𝒜` and has cardinality `r`.  -/
Finset.mem_slice : ∀ {α : Type u_1} {𝒜 : Finset (Finset α)} {A : Finset α} {r : ℕ}, A ∈ 𝒜.slice r ↔ A ∈ 𝒜 ∧ A.card = r
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem_union_of_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} (mem : k ∈ m₂), (m₁ ∪ m₂)[k] = m₂[k]
-- Mathlib.CategoryTheory.PathCategory.MorphismProperty
/-- A natural transformation between `F G : Paths V ⥤ C` is defined by its components and
its unary naturality squares.  -/
CategoryTheory.Paths.liftNatTrans : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {V : Type u₁} →
      [inst_1 : Quiver V] →
        {F G : CategoryTheory.Functor (CategoryTheory.Paths V) C} →
          (α_app : (v : V) → F.obj v ⟶ G.obj v) →
            (∀ {X Y : V} (f : X ⟶ Y),
                CategoryTheory.CategoryStruct.comp (F.map f.toPath) (α_app Y) =
                  CategoryTheory.CategoryStruct.comp (α_app X) (G.map f.toPath)) →
              (F ⟶ G)
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.continuousOn_exp : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕂] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸]
  [CompleteSpace 𝔸] [CharZero 𝕂], ContinuousOn NormedSpace.exp (Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius)
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.t_snd : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (i j : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t 𝒰 f g i j)
      (CategoryTheory.Limits.pullback.snd
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) (𝒰.f j))
        (𝒰.f i)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
        (𝒰.f j))
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g)
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.symm : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {u v : α → β} {l : Filter α},
  Asymptotics.IsEquivalent l u v → Asymptotics.IsEquivalent l v u
-- Mathlib.Topology.Sheaves.CommRingCat
TopCat.instPowHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrierNat : (X : TopCat) → (R : TopCommRingCat) → Pow (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R) ℕ
-- Mathlib.Data.Int.Lemmas
/-- A specialization of `abs_sub_le_of_nonneg_of_le` for working with the signed subtraction
of natural numbers.  -/
Int.natAbs_coe_sub_coe_le_of_le : ∀ {a b n : ℕ}, a ≤ n → b ≤ n → (↑a - ↑b).natAbs ≤ n
-- Aesop.Search.Expansion.Norm
Aesop.NormM.State.mk.inj : ∀ {forwardState : Aesop.ForwardState} {forwardRuleMatches : Aesop.ForwardRuleMatches}
  {forwardState_1 : Aesop.ForwardState} {forwardRuleMatches_1 : Aesop.ForwardRuleMatches},
  { forwardState := forwardState, forwardRuleMatches := forwardRuleMatches } =
      { forwardState := forwardState_1, forwardRuleMatches := forwardRuleMatches_1 } →
    forwardState = forwardState_1 ∧ forwardRuleMatches = forwardRuleMatches_1
-- Mathlib.Analysis.InnerProductSpace.Rayleigh
ContinuousLinearMap.rayleighQuotient_apply_neg : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (T : E →L[𝕜] E) (x : E), T.rayleighQuotient (-x) = T.rayleighQuotient x
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.ContainsIdentities.iff_identities_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C},
  W.ContainsIdentities ↔ CategoryTheory.MorphismProperty.identities C ≤ W
-- Mathlib.Order.Notation
HNot.mk : {α : Type u_1} → (α → α) → HNot α
-- Mathlib.Algebra.Polynomial.Eval.Defs
/-- `eval x p` is the evaluation of the polynomial `p` at `x`  -/
Polynomial.eval : {R : Type u} → [inst : Semiring R] → R → Polynomial R → R
-- Init.Data.List.Zip
List.map_fst_zip : ∀ {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List β}, l₁.length ≤ l₂.length → List.map Prod.fst (l₁.zip l₂) = l₁
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.degrees_esymm : ∀ (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ] [Nontrivial R] {n : ℕ},
  0 < n → n ≤ Fintype.card σ → (MvPolynomial.esymm σ R n).degrees = Finset.univ.val
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_filter : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] {f : (a : α) → β a → Bool} {k : α} (h : (↑m).WF),
  (Std.DHashMap.Internal.Raw₀.filter f m).getKey? k = (m.getKey? k).pfilter fun x h' => f x (m.get x ⋯)
-- Init.Data.BitVec.Bitblast
BitVec.not_add_one : ∀ {w : ℕ} {x : BitVec w}, ~~~(x + 1#w) = ~~~x - 1#w
-- Lean.Expr
/-- Return `true` if the given expression is of the form `.sort (.succ ..)`.  -/
Lean.Expr.isType : Lean.Expr → Bool
-- Mathlib.Analysis.Analytic.Inverse
/-- First technical lemma to control the growth of coefficients of the inverse. Bound the explicit
expression for `∑_{k<n+1} aᵏ Qₖ` in terms of a sum of powers of the same sum one step before,
in a general abstract setup.  -/
FormalMultilinearSeries.radius_right_inv_pos_of_radius_pos_aux1 : ∀ (n : ℕ) (p : ℕ → ℝ),
  (∀ (k : ℕ), 0 ≤ p k) →
    ∀ {r a : ℝ},
      0 ≤ r →
        0 ≤ a →
          ∑ k ∈ Finset.Ico 2 (n + 1), a ^ k * ∑ c ∈ {c | 1 < c.length}.toFinset, r ^ c.length * ∏ j, p (c.blocksFun j) ≤
            ∑ j ∈ Finset.Ico 2 (n + 1), r ^ j * (∑ k ∈ Finset.Ico 1 n, a ^ k * p k) ^ j
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.mkBelowInductive.go : Lean.Meta.IndPredBelow.Context✝ → Array Lean.Expr → Lean.Expr → ℕ → Array Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.InvariantForm.pairing_mul_eq_pairing_mul_swap : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (B : P.InvariantForm)
  (i j : ι), P.pairing j i * (B.form (P.root i)) (P.root i) = P.pairing i j * (B.form (P.root j)) (P.root j)
-- Std.Async.Process
/-- Number of block output operations (disk writes)
 -/
Std.IO.Process.ResourceUsageStats.blockOutputOps : Std.IO.Process.ResourceUsageStats → UInt64
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.preimage_of_isOpenImmersion : ∀ {X Y : AlgebraicGeometry.Scheme} {U : Y.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f],
      U ≤ AlgebraicGeometry.Scheme.Hom.opensRange f →
        AlgebraicGeometry.IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj U)
-- Mathlib.Topology.Closure
frontier_closure_subset : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, frontier (closure s) ⊆ frontier s
-- Mathlib.Topology.Sheaves.Skyscraper
instIsLeftAdjointSheafCompPresheafForgetStalkFunctor : ∀ {X : TopCat} (p₀ : ↑X) {C : Type v} [inst : CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasTerminal C]
  [inst_2 : CategoryTheory.Limits.HasColimits C],
  ((TopCat.Sheaf.forget C X).comp (TopCat.Presheaf.stalkFunctor C p₀)).IsLeftAdjoint
-- Mathlib.Data.Sym.Basic
Sym.filter_ne_fill : ∀ {α : Type u_1} {n : ℕ} [inst : DecidableEq α] (a : α) (m : (i : Fin (n + 1)) × Sym α (n - ↑i)),
  a ∉ m.snd → Sym.filterNe a (Sym.fill a m.fst m.snd) = m
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instAddCommGroup.eq_1 : ∀ {α : Type u_1} {l : Filter α} {G : Type u_6} [inst : AddCommGroup G],
  Filter.Germ.instAddCommGroup = { toAddGroup := Filter.Germ.instAddGroup, add_comm := ⋯ }
-- Aesop.Search.Expansion.Norm
Aesop.NormM.instInhabitedState : Inhabited Aesop.NormM.State
-- Mathlib.Algebra.Category.Grp.Basic
/-- Typecheck an `AddMonoidHom` as a morphism in `AddGrpCat`.  -/
AddGrpCat.ofHom : {X Y : Type u} → [inst : AddGroup X] → [inst_1 : AddGroup Y] → (X →+ Y) → (AddGrpCat.of X ⟶ AddGrpCat.of Y)
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.hom_ext : ∀ {M N : SemiNormedGrp} {f g : M ⟶ N}, SemiNormedGrp.Hom.hom f = SemiNormedGrp.Hom.hom g → f = g
-- Mathlib.Logic.Encodable.Basic
/-- If `α` is countable, then it has a (non-canonical) `Encodable` structure.  -/
Encodable.ofCountable : (α : Type u_3) → [Countable α] → Encodable α
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.mk_zero : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] {𝒜 : ι → σ}
  [inst_5 : GradedRing 𝒜] (x : Submonoid A), HomogeneousLocalization.mk 0 = 0
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.toSubmodule_mk : ∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L] (p : Submodule A L)
  (h : ∀ {a b : L}, a ∈ p.carrier → b ∈ p.carrier → ⁅a, b⁆ ∈ p.carrier),
  { toSubmodule := p, lie_mem' := h }.toSubmodule = p
-- Mathlib.CategoryTheory.Sites.CompatiblePlus
/-- The isomorphism between `P⁺ ⋙ F` and `(P ⋙ F)⁺`.  -/
CategoryTheory.GrothendieckTopology.plusCompIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type u_1} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
          {E : Type u_2} →
            [inst_2 : CategoryTheory.Category.{v_2, u_2} E] →
              (F : CategoryTheory.Functor D E) →
                [inst_3 :
                    ∀ (J : CategoryTheory.Limits.MulticospanShape),
                      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] →
                  [inst_4 :
                      ∀ (J : CategoryTheory.Limits.MulticospanShape),
                        CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] →
                    [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
                          CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] →
                      (P : CategoryTheory.Functor Cᵒᵖ D) →
                        [inst_6 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] →
                          [inst_7 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] →
                            [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] →
                              (J.plusObj P).comp F ≅ J.plusObj (P.comp F)
-- Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
LindemannWeierstrass.hasDerivAt_cexp_mul_sumIDeriv : ∀ (p : Polynomial ℂ) (s : ℂ) (x : ℝ),
  HasDerivAt (fun x => -(Complex.exp (-(x • s)) * Polynomial.eval (x • s) (Polynomial.sumIDeriv p)))
    (s * (Complex.exp (-(x • s)) * Polynomial.eval (x • s) p)) x
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.instFullPresheafOfModulesToPresheafOfModules : ∀ {X : AlgebraicGeometry.Scheme}, (AlgebraicGeometry.Scheme.Modules.toPresheafOfModules X).Full
-- Mathlib.Data.Multiset.Filter
Multiset.count_map : ∀ {α : Type u_3} {β : Type u_4} (f : α → β) (s : Multiset α) [inst : DecidableEq β] (b : β),
  Multiset.count b (Multiset.map f s) = (Multiset.filter (fun a => b = f a) s).card
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.inl_v_descCochain_v_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain K M m) (β : CochainComplex.HomComplex.Cochain L M n) (h : m + 1 = n)
  (p q : ℤ) (hpq : p + m = q) {Z : C} (h_1 : M.X q ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.inl φ).v p p ⋯)
      (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.descCochain φ α β h).v p q hpq) h_1) =
    CategoryTheory.CategoryStruct.comp (α.v p q hpq) h_1
-- Mathlib.Order.Types.Arithmetic
OrderType.liftOn.congr_simp : ∀ {δ : Sort v} (o o_1 : OrderType.{u_1}),
  o = o_1 →
    ∀ (f f_1 : (α : Type u_1) → [LinearOrder α] → δ) (e_f : f = f_1)
      (c :
        ∀ (α : Type u_1) [inst : LinearOrder α] (β : Type u_1) [inst_1 : LinearOrder β],
          OrderType.type α = OrderType.type β → f α = f β),
      o.liftOn f c = o_1.liftOn f_1 ⋯
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- the condition that `r` is a retraction of `S.f`  -/
CategoryTheory.ShortComplex.Splitting.f_r_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (self : S.Splitting) {Z : C} (h : S.X₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.f (CategoryTheory.CategoryStruct.comp self.r h) = h
-- Mathlib.Analysis.Convex.EGauge
le_egauge_ball_one : ∀ (𝕜 : Type u_1) [inst : NormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  (x : E), ‖x‖ₑ ≤ egauge 𝕜 (Metric.ball 0 1) x
-- Mathlib.Algebra.Divisibility.Units
/-- In a commutative monoid, an element `a` divides an element `b` iff all
left associates of `a` divide `b`.  -/
IsUnit.mul_left_dvd : ∀ {α : Type u_1} [inst : CommMonoid α] {a b u : α}, IsUnit u → (u * a ∣ b ↔ a ∣ b)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
ProfiniteAddGrp.ProfiniteCompletion.completion.eq_1 : ∀ (G : AddGrpCat),
  ProfiniteAddGrp.ProfiniteCompletion.completion G =
    ProfiniteAddGrp.limit (ProfiniteAddGrp.ProfiniteCompletion.diagram G)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_iUnion : ∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {α : Type u_2}
  (s : α → Set A), Algebra.adjoin R (Set.iUnion s) = ⨆ i, Algebra.adjoin R (s i)
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.opEquivalence_functor : ∀ {ι : Type u_1} (V : Type u_2) [inst : CategoryTheory.Category.{v_1, u_2} V] (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V],
  (HomologicalComplex.opEquivalence V c).functor = HomologicalComplex.opFunctor V c
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.one_def : ∀ (K : Type u) [inst : CommRing K] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p],
  1 = PerfectClosure.mk K p (0, 1)
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- The 'unopposite' of an iso `αᵐᵒᵖ ≃+ βᵐᵒᵖ`. Inverse to `AddEquiv.mul_op`.  -/
AddEquiv.mulUnop : {α : Type u_3} → {β : Type u_4} → [inst : Add α] → [inst_1 : Add β] → αᵐᵒᵖ ≃+ βᵐᵒᵖ ≃ (α ≃+ β)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_modify_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] {k : α} [inst_4 : Inhabited β] {f : β → β}, m.WF → (m.modify k f)[k]! = (Option.map f m[k]?).get!
-- Lean.Level
Lean.Level : Type
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.union_vsub : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] [inst_1 : DecidableEq α] {s₁ s₂ t : Finset β}
  [inst_2 : DecidableEq β], s₁ ∪ s₂ -ᵥ t = s₁ -ᵥ t ∪ (s₂ -ᵥ t)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.ordered_insertIfNew! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {k : α} {v : β k} {l : Std.DTreeMap.Internal.Impl α β},
  l.Balanced → l.Ordered → (Std.DTreeMap.Internal.Impl.insertIfNew! k v l).Ordered
-- Mathlib.Algebra.Group.Pointwise.Finset.BigOperators
Finset.prod_neg_index : ∀ {α : Type u_1} {ι : Type u_2} [inst : CommMonoid α] [inst_1 : DecidableEq ι] [inst_2 : InvolutiveNeg ι] (s : Finset ι)
  (f : ι → α), ∏ i ∈ -s, f i = ∏ i ∈ s, f (-i)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α} {k : α} (mem : k ∈ m) {h : k ∈ m.insertManyIfNewUnit l},
  (m.insertManyIfNewUnit l).getKey k h = m.getKey k mem
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- **Alias** of the forward direction of `hasDerivAt_iff_hasFDerivAt`.

---

Expressing `HasDerivAt f f' x` in terms of `HasFDerivAt`  -/
HasDerivAt.hasFDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] {f : 𝕜 → F} {x : 𝕜} [inst_4 : ContinuousSMul 𝕜 F] {f' : F},
  HasDerivAt f f' x → HasFDerivAt f (ContinuousLinearMap.toSpanSingleton 𝕜 f') x
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasProjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] {F G H : CategoryTheory.Functor C D} (α : F ⟶ G) (β : G ⟶ H) [inst_5 : F.Additive]
  [inst_6 : G.Additive] [inst_7 : H.Additive],
  CategoryTheory.NatTrans.leftDerivedToHomotopyCategory (CategoryTheory.CategoryStruct.comp α β) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftDerivedToHomotopyCategory α)
      (CategoryTheory.NatTrans.leftDerivedToHomotopyCategory β)
-- Mathlib.RingTheory.LocalRing.Pullback
/-- The first projection from the pullback of `f : R →+* T` and `g : S →+* T` to `R`.  -/
RingHom.pullbackFst : {R : Type u_1} →
  {S : Type u_2} →
    {T : Type u_3} →
      [inst : Ring R] →
        [inst_1 : Ring S] → [inst_2 : Semiring T] → (f : R →+* T) → (g : S →+* T) → ↥(f.pullback g) →+* R
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_filter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {f : (a : α) → β a → Bool}
  {l : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.containsKey k (List.filter (fun p => f p.fst p.snd) l) =
      Option.any (f k) (Std.Internal.List.getValueCast? k l)
-- Mathlib.SetTheory.Ordinal.Rank
IsWellFounded.mem_range_rank_of_le : ∀ {α : Type u} {a : α} {r : α → α → Prop} [hwf : IsWellFounded α r] {o : Ordinal.{u}},
  o ≤ IsWellFounded.rank r a → o ∈ Set.range (IsWellFounded.rank r)
-- Init.Data.List.MinMax
List.min?_eq_some_min : ∀ {α : Type u_1} [inst : Min α] {l : List α} (hl : l ≠ []), l.min? = some (l.min hl)
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.coe_restrictScalars : ∀ (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Monoid R] [inst_1 : Monoid S]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : MulAction R S]
  [inst_5 : DistribMulAction S A] [inst_6 : DistribMulAction S B] [inst_7 : DistribMulAction R A]
  [inst_8 : DistribMulAction R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B] (f : A →ₙₐ[S] B),
  ↑(NonUnitalAlgHom.restrictScalars R f) = ↑f
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?.congr_simp : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtDHashMap α fun x => β),
  m = m_1 → ∀ (a a_1 : α), a = a_1 → Std.ExtDHashMap.Const.get? m a = Std.ExtDHashMap.Const.get? m_1 a_1
-- Init.Data.SInt.Lemmas
ISize.toInt8_ofNat' : ∀ {n : ℕ}, (ISize.ofNat n).toInt8 = Int8.ofNat n
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
/-- The natural isomorphism witnessing the pseudo-functoriality of `CoGrothendieck.map`.  -/
CategoryTheory.Pseudofunctor.CoGrothendieck.mapCompIso : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {F G H : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} →
      (α : F ⟶ G) →
        (β : G ⟶ H) →
          CategoryTheory.Pseudofunctor.CoGrothendieck.map (CategoryTheory.CategoryStruct.comp α β) ≅
            (CategoryTheory.Pseudofunctor.CoGrothendieck.map α).comp (CategoryTheory.Pseudofunctor.CoGrothendieck.map β)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- A vector has an angle of `θ` from the rotation of that vector by `θ`.  -/
Orientation.oangle_rotation_self_right : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x : V}, x ≠ 0 → ∀ (θ : Real.Angle), o.oangle x ((o.rotation θ) x) = θ
-- Mathlib.RingTheory.RamificationInertia.Ramification
Ideal.ramificationIdx_eq_one : ∀ {S : Type u_1} [inst : CommRing S] (q : Ideal S) (R : Type u_2) [inst_1 : CommRing R] [inst_2 : Algebra R S]
  [inst_3 : q.IsPrime] [Algebra.EssFiniteType R S] [Algebra.IsUnramifiedAt R q], q.ramificationIdx R = 1
-- Lean.Parser.Term.Basic
Lean.Parser.Term.syntheticHole.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Order.Bounds.Basic
IsGreatest.lt_iff : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a b : α}, IsGreatest s a → (a < b ↔ ∀ x ∈ s, x < b)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey!_alter_eq_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] [inst_2 : Inhabited α] {k : α} {f : Option (β k) → Option (β k)},
  t.alter k f ≠ ∅ → ((t.alter k f).maxKey! = k ↔ (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (cmp k' k).isLE = true)