mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.OverArrows.yonedaArrow_val : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C}
  {η : CategoryTheory.yoneda.obj Y ⟶ A} {X : C} {s : CategoryTheory.yoneda.obj X ⟶ A} {f : X ⟶ Y}
  (hf : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) η = s),
  (CategoryTheory.OverPresheafAux.OverArrows.yonedaArrow f hf).val = f
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
toMul_list_sum : ∀ {M : Type u_3} [inst : Monoid M] (s : List (Additive M)), Additive.toMul s.sum = (List.map (⇑Additive.toMul) s).prod
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.whiskerLeft_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X x x_1 : CategoryTheory.Dial C) (f : x ⟶ x_1),
  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f).f =
    CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id X.src) f.f
-- Init.System.IO
IO.instLTTaskState : LT IO.TaskState
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.normSq_lt_one : ∀ (z : Complex.UnitClosedDisc), Complex.normSq ↑z ≤ 1
-- Mathlib.Algebra.Star.Basic
star_nsmul : ∀ {R : Type u} [inst : AddMonoid R] [inst_1 : StarAddMonoid R] (n : ℕ) (x : R), star (n • x) = n • star x
-- Mathlib.Topology.Compactness.Lindelof
mem_coclosed_Lindelof' : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  s ∈ Filter.coclosedLindelof X ↔ ∃ t, IsClosed t ∧ IsLindelof t ∧ sᶜ ⊆ t
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- Constant as a continuous bounded function.  -/
BoundedContinuousFunction.const : (α : Type u) →
  {β : Type v} → [inst : TopologicalSpace α] → [inst_1 : PseudoMetricSpace β] → β → BoundedContinuousFunction α β
-- Mathlib.Order.UpperLower.Basic
isUpperSet_setOfPred : ∀ {α : Type u_1} [inst : Preorder α] {p : α → Prop}, IsUpperSet {a | p a} ↔ Monotone p
-- Init.Data.Range.Polymorphic.UInt
USize.upwardEnumerableLT_ofBitVec : ∀ {x y : BitVec System.Platform.numBits},
  Std.PRange.UpwardEnumerable.LT { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LT x y
-- Mathlib.Logic.Equiv.PartialEquiv
Equiv.trans_toPartialEquiv : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α ≃ β) (e' : β ≃ γ),
  (e.trans e').toPartialEquiv = e.toPartialEquiv.trans e'.toPartialEquiv
-- Mathlib.Analysis.Normed.Group.Constructions
pi_nnnorm_const' : ∀ {ι : Type u_1} {E : Type u_2} [inst : Fintype ι] [inst_1 : SeminormedGroup E] [Nonempty ι] (a : E),
  ‖fun _i => a‖₊ = ‖a‖₊
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.ext_contains_unit : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {t₁ t₂ : Std.ExtTreeMap α Unit cmp}, (∀ (k : α), t₁.contains k = t₂.contains k) → t₁ = t₂
-- Mathlib.Analysis.SpecialFunctions.Exp
Continuous.cexp : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℂ}, Continuous f → Continuous fun y => Complex.exp (f y)
-- Mathlib.Algebra.Homology.GrothendieckAbelian
HomologicalComplex.hasExactColimitsOfShape : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {ι : Type t} (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J]
  [CategoryTheory.Limits.HasFiniteLimits C] [inst_4 : CategoryTheory.Limits.HasColimitsOfShape J C]
  [CategoryTheory.HasExactColimitsOfShape J C], CategoryTheory.HasExactColimitsOfShape J (HomologicalComplex C c)
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Key.arrow : Lean.Meta.DiscrTree.Key
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.restrictScalarsEquivalenceOfRingEquiv_unitIso : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S),
  (AlgCat.restrictScalarsEquivalenceOfRingEquiv e).unitIso =
    (AlgCat.restrictScalarsId' (RingHom.id S) ⋯).symm ≪≫
      AlgCat.restrictScalarsComp' e.symm.toRingHom e.toRingHom (RingHom.id S) ⋯
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normal_addSubgroupOf_of_le_normalizer : ∀ {G : Type u_1} [inst : AddGroup G] {H N : AddSubgroup G}, H ≤ AddSubgroup.normalizer ↑N → (N.addSubgroupOf H).Normal
-- Mathlib.Computability.Language
Language.reverse_zero : ∀ {α : Type u_1}, Language.reverse 0 = 0
-- Mathlib.Data.Nat.Choose.Basic
Nat.add_choose : ∀ (i j : ℕ), (i + j).choose j = (i + j).factorial / (i.factorial * j.factorial)
-- Mathlib.CategoryTheory.Functor.FullyFaithful
/-- The inverse map `(F.obj X ⟶ F.obj Y) ⟶ (X ⟶ Y)` of `F.map`.  -/
CategoryTheory.Functor.FullyFaithful.preimage : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} → F.FullyFaithful → {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.HasRingHomProperty.of_source_openCover : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  [AlgebraicGeometry.HasRingHomProperty P Q] {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [AlgebraicGeometry.IsAffine Y]
  (𝒰 : X.OpenCover) [∀ (i : 𝒰.I₀), AlgebraicGeometry.IsAffine (𝒰.X i)],
  (∀ (i : 𝒰.I₀),
      Q (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)))) →
    P f
-- Mathlib.Algebra.Notation.Prod
Prod.instNeg : {G : Type u_8} → {H : Type u_9} → [Neg G] → [Neg H] → Neg (G × H)
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.unop_closure : ∀ {M : Type u_2} [inst : Add M] (s : Set Mᵃᵒᵖ),
  (AddSubsemigroup.closure s).unop = AddSubsemigroup.closure (AddOpposite.op ⁻¹' s)
-- Mathlib.Order.Defs.Unbundled
asymm : ∀ {α : Sort u_1} {r : α → α → Prop} {a b : α} [Std.Asymm r], r a b → ¬r b a
-- Mathlib.Order.GaloisConnection.Defs
/-- Property of the choice function.  -/
GaloisInsertion.choice_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α}
  (self : GaloisInsertion l u) (a : α) (h : u (l a) ≤ a), self.choice a h = l a
-- Mathlib.RingTheory.Spectrum.Prime.Topology
/-- Zero loci of prime ideals are closed irreducible sets in the Zariski topology and any closed
irreducible set is a zero locus of some prime ideal.
 -/
PrimeSpectrum.zeroLocusEquivIrreducibleCloseds : {R : Type u} →
  [inst : CommSemiring R] →
    (I : Set R) → ↑(PrimeSpectrum.zeroLocus I) ≃o (TopologicalSpace.IrreducibleCloseds ↑(PrimeSpectrum.zeroLocus I))ᵒᵈ
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesEIso_inv_τ₂ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesEIso._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesEIso._auto_3),
  (X.cokernelSequenceCyclesEIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv.τ₂ = (X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).hom
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.closure_image_comap_zeroLocus : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (I : Ideal S),
  closure (PrimeSpectrum.comap f '' PrimeSpectrum.zeroLocus ↑I) = PrimeSpectrum.zeroLocus ↑(Ideal.comap f I)
-- Init.Data.Iterators.Lemmas.Consumers.Collect
Std.Iter.toArray_ensureTermination : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterators.Finite α Id] {it : Std.Iter β},
  it.ensureTermination.toArray = it.toArray
-- Mathlib.Topology.Algebra.OpenSubgroup
AddSubgroup.quotient_finite_of_isOpen : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [SeparatelyContinuousAdd G] [CompactSpace G]
  (U : AddSubgroup G), IsOpen ↑U → Finite (G ⧸ U)
-- Init.Data.Option.Lemmas
Option.pmap_some' : ∀ {α : Type u_1} {β : Type u_2} {x : Option α} {a : α} {p : α → Prop} {f : (a : α) → p a → β} (he : x = some a)
  {h : ∀ (a : α), x = some a → p a}, Option.pmap f x h = some (f a ⋯)
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.IsSubDPIdeal.dpow_eq_of_mem : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} (hI : DividedPowers I) {J : Ideal A} (hJ : hI.IsSubDPIdeal J)
  [inst_1 : (x : A) → Decidable (x ∈ J)] {n : ℕ} {a : A},
  a ∈ J → (DividedPowers.IsSubDPIdeal.dividedPowers hI hJ).dpow n a = hI.dpow n a
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
/-- The tensor product of two orthonormal bases is orthonormal.  -/
Orthonormal.basisTensorProduct : ∀ {𝕜 : 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] {ι₁ : Type u_6}
  {ι₂ : Type u_7} {b₁ : Module.Basis ι₁ 𝕜 E} {b₂ : Module.Basis ι₂ 𝕜 F},
  Orthonormal 𝕜 ⇑b₁ → Orthonormal 𝕜 ⇑b₂ → Orthonormal 𝕜 ⇑(b₁.tensorProduct b₂)
-- Mathlib.Algebra.Homology.TotalComplex
/-- The morphism `K.total c₁₂ ⟶ L.total c₁₂` of homological complexes induced
by a morphism of bicomplexes `K ⟶ L`.  -/
HomologicalComplex₂.total.map : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {I₁ : Type u_2} →
        {I₂ : Type u_3} →
          {I₁₂ : Type u_4} →
            {c₁ : ComplexShape I₁} →
              {c₂ : ComplexShape I₂} →
                {K L : HomologicalComplex₂ C c₁ c₂} →
                  (K ⟶ L) →
                    (c₁₂ : ComplexShape I₁₂) →
                      [inst_2 : TotalComplexShape c₁ c₂ c₁₂] →
                        [inst_3 : DecidableEq I₁₂] →
                          [inst_4 : K.HasTotal c₁₂] → [inst_5 : L.HasTotal c₁₂] → K.total c₁₂ ⟶ L.total c₁₂
-- Mathlib.NumberTheory.Height.Basic
/-- The logarithmic height of the "multiplication table" `fun (i, j) ↦ x i * y j`
is the sum of the logarithmic heights of `x` and `y`.  -/
Height.logHeight_fun_mul_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} {ι' : Type u_3} [Finite ι]
  [Finite ι'] {x : ι → K},
  x ≠ 0 → ∀ {y : ι' → K}, y ≠ 0 → (Height.logHeight fun a => x a.1 * y a.2) = Height.logHeight x + Height.logHeight y
-- Std.Http.Data.Chunk
Std.Http.Trailer.mk.inj : ∀ {headers headers_1 : Std.Http.Headers}, { headers := headers } = { headers := headers_1 } → headers = headers_1
-- Mathlib.Order.CompleteLattice.Basic
biSup_le_eq_of_monotone : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] [inst_1 : Preorder β] {f : β → α},
  Monotone f → ∀ (b : β), ⨆ b', ⨆ (_ : b' ≤ b), f b' = f b
-- Mathlib.Probability.Distributions.SetBernoulli
ProbabilityTheory.setBernoulli_ae_subset : ∀ {ι : Type u_1} {u : Set ι} {p : ↑unitInterval} [Countable ι],
  ∀ᵐ (s : Set ι) ∂ProbabilityTheory.setBernoulli u p, s ⊆ u
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_of_mem_insertIfNew : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k a : α} {v : β k}, a ∈ (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl → compare k a ≠ Ordering.eq → a ∈ t
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.Equiv.beq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [LawfulHashable α] [EquivBEq α] [inst_4 : BEq β] [ReflBEq β],
  (↑m₁).WF → (↑m₂).WF → (↑m₁).Equiv ↑m₂ → Std.DHashMap.Internal.Raw₀.Const.beq m₁ m₂ = true
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₂₂.isPushout : CategoryTheory.IsPushout (SSet.stdSimplex.δ 0) (SSet.stdSimplex.δ 0) SSet.horn₂₂.ι₀₂ SSet.horn₂₂.ι₁₂
-- Mathlib.MeasureTheory.Measure.Complex
/-- The real part of a complex measure is a signed measure.  -/
MeasureTheory.ComplexMeasure.re : {α : Type u_1} → {m : MeasurableSpace α} → MeasureTheory.ComplexMeasure α →ₗ[ℝ] MeasureTheory.SignedMeasure α
-- Lean.Environment
Lean.instReprConstantKind.repr : Lean.ConstantKind → ℕ → Std.Format
-- Qq.Macro
Qq.Impl.ExprBackSubstResult : Type
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.TauPackage.iUnionUpTo.eq_1 : ∀ {α : Type u_1} [inst : MetricSpace α] {β : Type u} [inst_1 : Nonempty β] (p : Besicovitch.TauPackage β α)
  (i : Ordinal.{u}), p.iUnionUpTo i = ⋃ j, Metric.ball (p.c (p.index ↑j)) (p.r (p.index ↑j))
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.instIsFiniteKernelSectROfProd : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel (α × β) γ) (a : α) [ProbabilityTheory.IsFiniteKernel κ],
  ProbabilityTheory.IsFiniteKernel (κ.sectR a)
-- Mathlib.NumberTheory.ClassNumber.Finite
ClassGroup.mkMMem_surjective : ∀ {R : Type u_1} {S : Type u_2} [inst : EuclideanDomain R] [inst_1 : CommRing S] [inst_2 : IsDomain S]
  [inst_3 : Algebra R S] {abv : AbsoluteValue R ℤ} {ι : Type u_5} [inst_4 : DecidableEq ι] [inst_5 : Fintype ι]
  (bS : Module.Basis ι R S) (adm : abv.IsAdmissible) [inst_6 : Infinite R] [inst_7 : DecidableEq R]
  [inst_8 : IsDedekindDomain S] [Algebra.IsAlgebraic R S], Function.Surjective (ClassGroup.mkMMem bS adm)
-- Mathlib.Data.Num.Bitwise
/-- `n.oneBits` is the list of indices of active bits in the binary representation of `n`.  -/
Num.oneBits : Num → List ℕ
-- Std.Data.Internal.List.Associative
Std.Internal.List.isNone_maxKey?_eq_isEmpty : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {l : List ((a : α) × β a)},
  (Std.Internal.List.maxKey? l).isNone = l.isEmpty
-- Lean.Meta.Match.Match
/-- Given a list of `AltLHS`, create a minor premise for each one, convert them into `Alt`, and then execute `k`  -/
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.withAlts : {α : Type} →
  Lean.Expr →
    Array Lean.Expr →
      Array Lean.Meta.Match.DiscrInfo →
        List Lean.Meta.Match.AltLHS →
          Option Lean.Meta.Match.Overlaps →
            (List Lean.Meta.Match.Alt → Array Lean.Expr → Array Lean.Meta.Match.AltParamInfo → Lean.MetaM α) →
              Lean.MetaM α
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.pairwise_toList_ne : ∀ {α : Type u} {r : Std.Rii α} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_4 : Std.Rxi.IsAlwaysFinite α], List.Pairwise (fun a b => a ≠ b) r.toList
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.coe_compl : ∀ {α : Type u_1} {n : ℕ} [inst : DecidableEq α] [inst_1 : Fintype α] {m : ℕ} {hm : m + n = Fintype.card α}
  {s : ↑(Set.powersetCard α n)}, ↑((Set.powersetCard.compl hm) s) = (↑s)ᶜ
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.OneCocycle.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {G : CategoryTheory.Functor Cᵒᵖ GrpCat} →
      {I : Type w'} →
        {U : I → C} →
          (toOneCochain : CategoryTheory.PresheafOfGroups.OneCochain G U) →
            autoParam
                (∀ (i j k : I) ⦃T : C⦄ (a : T ⟶ U i) (b : T ⟶ U j) (c : T ⟶ U k),
                  toOneCochain.ev i j a b * toOneCochain.ev j k b c = toOneCochain.ev i k a c)
                CategoryTheory.PresheafOfGroups.OneCocycle.ev_trans._autoParam →
              CategoryTheory.PresheafOfGroups.OneCocycle G U
-- Mathlib.Analysis.Calculus.AddTorsor.AffineMap
ContDiffOn.lineMap : ∀ {𝕜 : Type u_1} {V : Type u_2} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f₁ f₂ : E → V} {g : E → 𝕜}
  {s : Set E} {n : WithTop ℕ∞},
  ContDiffOn 𝕜 n f₁ s →
    ContDiffOn 𝕜 n f₂ s → ContDiffOn 𝕜 n g s → ContDiffOn 𝕜 n (fun x => (AffineMap.lineMap (f₁ x) (f₂ x)) (g x)) s
-- Mathlib.CategoryTheory.Monoidal.Category
/-- The left whiskering of an isomorphism is an isomorphism.  -/
CategoryTheory.MonoidalCategory.«term_◁ᵢ_» : Lean.TrailingParserDescr
-- Mathlib.Combinatorics.SetFamily.Shatter
Finset.mem_shatterer : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α}, s ∈ 𝒜.shatterer ↔ 𝒜.Shatters s
-- Mathlib.Analysis.Calculus.FDeriv.Prod
hasFDerivAt_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {ι : Type u_6} {F' : ι → Type u_7}
  [inst_1 : (i : ι) → NormedAddCommGroup (F' i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (F' i)] (i : ι) (f : (i : ι) → F' i),
  HasFDerivAt (fun f => f i) (ContinuousLinearMap.proj i) f
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.symm_apply_eq : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) {p₁ : P₂} {p₂ : P₁},
  e.symm p₁ = p₂ ↔ p₁ = e p₂
-- Mathlib.LinearAlgebra.RootSystem.Hom
/-- The contravariant equivalence of coweight spaces given by an equivalence of root pairings.  -/
RootPairing.Equiv.coweightEquiv : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  {ι₂ : Type u_5} →
                    {M₂ : Type u_6} →
                      {N₂ : Type u_7} →
                        [inst_5 : AddCommGroup M₂] →
                          [inst_6 : Module R M₂] →
                            [inst_7 : AddCommGroup N₂] →
                              [inst_8 : Module R N₂] →
                                (P : RootPairing ι R M N) → (Q : RootPairing ι₂ R M₂ N₂) → P.Equiv Q → N₂ ≃ₗ[R] N
-- Mathlib.Order.Filter.Prod
Filter.le_prod : ∀ {α : Type u_1} {β : Type u_2} {f : Filter (α × β)} {g : Filter α} {g' : Filter β},
  f ≤ g ×ˢ g' ↔ Filter.Tendsto Prod.fst f g ∧ Filter.Tendsto Prod.snd f g'
-- Mathlib.Data.Multiset.UnionInter
Multiset.union_comm : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α), s ∪ t = t ∪ s
-- Mathlib.Algebra.Star.SelfAdjoint
skewAdjoint.instSMulSubtypeMemAddSubgroupOfStarModule : {R : Type u_1} →
  {A : Type u_2} →
    [inst : Star R] →
      [TrivialStar R] →
        [inst_2 : AddCommGroup A] →
          [inst_3 : StarAddMonoid A] →
            [inst_4 : Monoid R] → [inst_5 : DistribMulAction R A] → [StarModule R A] → SMul R ↥(skewAdjoint A)
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
Order.IsNormal.isClub_range : ∀ {α : Type v} [inst : LinearOrder α] [WellFoundedLT α] {f : α → α}, Order.IsNormal f → IsClub (Set.range f)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.j_eq_zero : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [inst_1 : W.IsElliptic], W.c₄ = 0 → W.j = 0
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_of_getKey?_eq_some : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α}, m.getKey? k = some k' → k' ∈ m
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.getEntryLTD_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α}
  {fallback : (a : α) × β a}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getEntryLTD k fallback = t₂.getEntryLTD k fallback
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.normAtAllPlaces_normAtAllPlaces : ∀ {K : Type u_1} [inst : Field K] (x : NumberField.mixedEmbedding.mixedSpace K),
  NumberField.mixedEmbedding.normAtAllPlaces
      (NumberField.mixedEmbedding.mixedSpaceOfRealSpace (NumberField.mixedEmbedding.normAtAllPlaces x)) =
    NumberField.mixedEmbedding.normAtAllPlaces x
-- Mathlib.Data.Rat.Defs
Rat.mul_eq_mkRat : ∀ (q r : ℚ), q * r = mkRat (q.num * r.num) (q.den * r.den)
-- Mathlib.Tactic.CrossRefAttribute
/-- Extract the underlying identifier as a string from a `lmfdbId` node.  -/
Lean.TSyntax.getLmfdbId : Lean.TSyntax Mathlib.CrossRef.lmfdbIdKind → Lean.CoreM String
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
/-- The bijection `SmallShiftedHom.{w} W X Y m ≃ ShiftedHom (L.obj X) (L.obj Y) m`
for all `m : M`, and `X` and `Y` in `C` when `L : C ⥤ D` is a localization functor for
`W : MorphismProperty C` such that the category `D` is equipped with a shift by `M`
and `L` commutes with the shifts.  -/
CategoryTheory.Localization.SmallShiftedHom.equiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (W : CategoryTheory.MorphismProperty C) →
          {M : Type w'} →
            [inst_2 : AddMonoid M] →
              [inst_3 : CategoryTheory.HasShift C M] →
                [inst_4 : CategoryTheory.HasShift D M] →
                  (L : CategoryTheory.Functor C D) →
                    [L.IsLocalization W] →
                      [L.CommShift M] →
                        {X Y : C} →
                          [inst_7 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] →
                            {m : M} →
                              CategoryTheory.Localization.SmallShiftedHom W X Y m ≃
                                CategoryTheory.ShiftedHom (L.obj X) (L.obj Y) m
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
CategoryTheory.Projective.zero_projective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C],
  CategoryTheory.Projective 0
-- Mathlib.CategoryTheory.Limits.Opposites
/-- Turn a limit for `F.unop : J ⥤ C` into a colimit for `F : Jᵒᵖ ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.isColimitOfConeUnopOfCocone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
        (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) →
          {c : CategoryTheory.Limits.Cocone F} →
            CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneUnopOfCocone c) → CategoryTheory.Limits.IsColimit c
-- Mathlib.Data.Int.Order.Basic
Int.instLinearOrder : LinearOrder ℤ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.Hover.mk.inj : ∀ {contents : Lean.Lsp.MarkupContent} {range? : Option Lean.Lsp.Range} {contents_1 : Lean.Lsp.MarkupContent}
  {range?_1 : Option Lean.Lsp.Range},
  { contents := contents, range? := range? } = { contents := contents_1, range? := range?_1 } →
    contents = contents_1 ∧ range? = range?_1
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- A constructor for chain maps between `α`-indexed cochain complexes built using `CochainComplex.of`,
from a dependently typed collection of morphisms.
 -/
CochainComplex.ofHom : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      {α : Type u_2} →
        [inst_2 : AddRightCancelSemigroup α] →
          [inst_3 : One α] →
            {X Y : CochainComplex V α} →
              (f : (i : α) → X.X i ⟶ Y.X i) →
                (∀ (i : α),
                    CategoryTheory.CategoryStruct.comp (f i) (Y.d i (i + 1)) =
                      CategoryTheory.CategoryStruct.comp (X.d i (i + 1)) (f (i + 1))) →
                  (X ⟶ Y)
-- Init.Data.Int.Lemmas
Int.neg_neg : ∀ (a : ℤ), - -a = a
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.leftRightHomologyComparison'_fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h₁ : S.LeftHomologyData) (h₂ : S.RightHomologyData) [inst_2 : S.HasHomology],
  CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂ =
    CategoryTheory.CategoryStruct.comp h₁.homologyIso.inv h₂.homologyIso.hom