mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Complex.Basic
Complex.equivRealProd_symm_apply : ∀ (p : ℝ × ℝ), Complex.equivRealProd.symm p = ↑p.1 + ↑p.2 * Complex.I
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.IsRoot.dvd : ∀ {R : Type u_1} [inst : CommSemiring R] {p q : Polynomial R} {x : R}, p.IsRoot x → p ∣ q → q.IsRoot x
-- Mathlib.Order.Defs.Unbundled
/-- `Std.Symm` as a definition, suitable for use in proofs.  -/
Symmetric : {α : Sort u_1} → (α → α → Prop) → Prop
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
/-- `ContinuousLinearMap.compContinuousMultilinearMap` as a bundled continuous linear equiv.
Given a continuous linear equivalence `g : F ≃L[𝕜] G`,
this function builds a continuous linear equivalence
between the space of continuous multilinear maps with codomain `F`
and the space of continuous multilinear maps with codomain `G`,
by composing these maps with `g` or `g.symm`.  -/
ContinuousLinearEquiv.continuousMultilinearMapCongrRight : {𝕜 : Type u_1} →
  {ι : Type u_2} →
    (E : ι → Type u_3) →
      {F : Type u_5} →
        {G : Type u_6} →
          [inst : NormedField 𝕜] →
            [inst_1 : (i : ι) → TopologicalSpace (E i)] →
              [inst_2 : (i : ι) → AddCommGroup (E i)] →
                [inst_3 : (i : ι) → Module 𝕜 (E i)] →
                  [inst_4 : AddCommGroup F] →
                    [inst_5 : Module 𝕜 F] →
                      [inst_6 : TopologicalSpace F] →
                        [inst_7 : IsTopologicalAddGroup F] →
                          [inst_8 : ContinuousConstSMul 𝕜 F] →
                            [inst_9 : AddCommGroup G] →
                              [inst_10 : Module 𝕜 G] →
                                [inst_11 : TopologicalSpace G] →
                                  [inst_12 : IsTopologicalAddGroup G] →
                                    [inst_13 : ContinuousConstSMul 𝕜 G] →
                                      (F ≃L[𝕜] G) → ContinuousMultilinearMap 𝕜 E F ≃L[𝕜] ContinuousMultilinearMap 𝕜 E G
-- Mathlib.GroupTheory.Index
/-- A subgroup has index dividing 2 if and only if there exists `a` such that for all `b`, at least
one of `a * b` and `b` belongs to `H`.  -/
Subgroup.index_dvd_two_iff' : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.index ∣ 2 ↔ ∃ a, ∀ (b : G), a * b ∈ H ∨ b ∈ H
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- If `G.IsBipartiteWith s t` and `v ∈ s`, then the neighbor finset of `v` is a subset of `s`.  -/
SimpleGraph.isBipartiteWith_neighborFinset_subset : ∀ {V : Type u_1} {v : V} {G : SimpleGraph V} {s t : Finset V} [inst : Fintype ↑(G.neighborSet v)],
  G.IsBipartiteWith ↑s ↑t → v ∈ s → G.neighborFinset v ⊆ t
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- A connected component of an acyclic graph is a tree.  -/
SimpleGraph.IsAcyclic.isTree_connectedComponent : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsAcyclic → ∀ (c : G.ConnectedComponent), c.toSimpleGraph.IsTree
-- Mathlib.MeasureTheory.Measure.Count
MeasureTheory.Measure.count_ne_zero'' : ∀ {α : Type u_1} [inst : MeasurableSpace α] [Nonempty α], MeasureTheory.Measure.count ≠ 0
-- Mathlib.Data.Nat.Totient
Nat.totient.eq_1 : ∀ (n : ℕ), n.totient = {a ∈ Finset.range n | n.Coprime a}.card
-- Mathlib.Algebra.Group.Hom.Defs
map_comp_pow : ∀ {ι : Type u_1} {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : Monoid G]
  [inst_2 : Monoid H] [MonoidHomClass F G H] (f : F) (g : ι → G) (n : ℕ), ⇑f ∘ (g ^ n) = ⇑f ∘ g ^ n
-- Mathlib.MeasureTheory.Measure.AEDisjoint
MeasureTheory.AEDisjoint.sdiff_ae_eq_left : ∀ {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.AEDisjoint μ s t → s \ t =ᵐ[μ] s
-- Mathlib.Data.Nat.Log
Nat.clog.eq_def : ∀ (b n : ℕ), Nat.clog b n = if 1 < b ∧ 1 < n then (Nat.clog.go n b n).2 + 1 else 0
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.range.congr_simp : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] (f f_1 : M →ₛₗ[τ₁₂] M₂), f = f_1 → f.range = f_1.range
-- Mathlib.Topology.Algebra.TopologicallyNilpotent
/-- If `a` is topologically nilpotent, then `a * b` is topologically nilpotent.  -/
IsTopologicallyNilpotent.mul_right : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : CommRing R] [IsLinearTopology R R] {a : R},
  IsTopologicallyNilpotent a → ∀ (b : R), IsTopologicallyNilpotent (a * b)
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.row.eq_1 : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} (A : Matrix m n α), A.row = A
-- Mathlib.Control.Monad.Cont
Cont : Type u → Type w → Type (max u w)
-- Mathlib.RingTheory.Ideal.Pointwise
Ideal.pointwise_smul_def : ∀ {M : Type u_1} {R : Type u_3} [inst : Monoid M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] {a : M}
  (S : Ideal R), a • S = Ideal.map (MulSemiringAction.toRingHom M R a) S
-- Mathlib.RingTheory.Polynomial.Quotient
/-- Given a domain `R`, if `R[X]` is a principal ideal ring, then `R` is a field.  -/
Ideal.IsField.of_isPrincipalIdealRing_polynomial : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] [IsPrincipalIdealRing (Polynomial R)], IsField R
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.ΓSpec.left_triangle : ∀ (X : AlgebraicGeometry.LocallyRingedSpace),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity.inv.app
        (AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X)))
      ((AlgebraicGeometry.identityToΓSpec.app X).c.app (Opposite.op ⊤)) =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Functor.id CommRingCat).obj (AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X)))
-- Mathlib.Topology.MetricSpace.Pseudo.Pi
/-- An open ball in a product space is a product of open balls. See also `ball_pi'`
for a version assuming `Nonempty β` instead of `0 < r`.  -/
ball_pi : ∀ {β : Type u_2} {X : β → Type u_3} [inst : Fintype β] [inst_1 : (b : β) → PseudoMetricSpace (X b)] (x : (b : β) → X b)
  {r : ℝ}, 0 < r → Metric.ball x r = Set.univ.pi fun b => Metric.ball (x b) r
-- Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris
/-- The Mayer-Vietoris long exact sequence of an abelian sheaf `F : Sheaf J AddCommGrpCat`
for a Mayer-Vietoris square `S : J.MayerVietorisSquare`.  -/
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sequence : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] →
        [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat] →
          [CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] →
            J.MayerVietorisSquare →
              CategoryTheory.Sheaf J AddCommGrpCat →
                (n₀ n₁ : ℕ) → n₀ + 1 = n₁ → CategoryTheory.ComposableArrows AddCommGrpCat 5
-- Init.Sym.Lemmas
Lean.Sym.decide_isFalse : ∀ (p : Prop) {inst : Decidable p} {h : ¬p}, decide p = false
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
map_extChartAt_nhdsWithin : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} {s : Set M} [inst_5 : ChartedSpace H M] (x : M),
  Filter.map (↑(extChartAt I x)) (nhdsWithin x s) =
    nhdsWithin (↑(extChartAt I x) x) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I)
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.ext : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (h₁ : f.left = g.left)
  (h₂ : f.right = g.right),
  f.hom =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₁)
        (CategoryTheory.CategoryStruct.comp g.hom (CategoryTheory.eqToHom ⋯)) →
    f = g
-- Init.Data.List.Nat.TakeDrop
List.mem_drop_iff_getElem : ∀ {α : Type u_1} {i : ℕ} {l : List α} {a : α}, a ∈ List.drop i l ↔ ∃ j, ∃ (hm : j + i < l.length), l[i + j] = a
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
FixedPoints.intermediateField.congr_simp : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (M : Type u_3)
  [inst_3 : Monoid M] [inst_4 : MulSemiringAction M E] [inst_5 : SMulCommClass M F E],
  FixedPoints.intermediateField M = FixedPoints.intermediateField M
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
SSet.Subcomplex.Pairing.strongAnodyneExtensions : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) [P.IsRegular], SSet.strongAnodyneExtensions A.ι
-- Mathlib.Analysis.Meromorphic.FactorizedRational
/-- Compute the trailing coefficient of the factorized rational function associated with `d : 𝕜 → ℤ`.
 -/
Function.FactorizedRational.meromorphicTrailingCoeffAt_factorizedRational : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {d : 𝕜 → ℤ} {x : 𝕜},
  Function.HasFiniteSupport d →
    meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), (fun x => x - u) ^ d u) x = ∏ᶠ (u : 𝕜), (x - u) ^ Function.update d x 0 u
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.intCast_re : ∀ (x : GaussianInt), ↑x.re = (GaussianInt.toComplex x).re
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.centralAlgebraMulHom_apply : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommSemiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module A V] (ρ : Representation A G V) (z : ↥(Submonoid.center (MonoidAlgebra A G))),
  (Representation.IntertwiningMap.centralAlgebraMulHom ρ) z = Representation.IntertwiningMap.centralAlgebraMul ρ ⋯
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.mem_keys : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α],
  (↑m).WF → ∀ {k : α}, k ∈ (↑m).keys ↔ m.contains k = true
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.zeroLocus_singleton_one : ∀ {R : Type u} [inst : CommSemiring R], PrimeSpectrum.zeroLocus {1} = ∅
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Multipliable.congr_atTop : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : TopologicalSpace α] [IsTopologicalGroup α] {f₁ g₁ : ℕ → α},
  Multipliable f₁ → f₁ =ᶠ[Filter.atTop] g₁ → Multipliable g₁
-- Mathlib.Topology.Algebra.Module.Equiv
LinearEquiv.isUniformEmbedding : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {E₁ : Type u_8} {E₂ : Type u_9}
  [inst_4 : UniformSpace E₁] [inst_5 : UniformSpace E₂] [inst_6 : AddCommGroup E₁] [inst_7 : AddCommGroup E₂]
  [inst_8 : Module R₁ E₁] [inst_9 : Module R₂ E₂] [IsUniformAddGroup E₁] [IsUniformAddGroup E₂] (e : E₁ ≃ₛₗ[σ₁₂] E₂),
  Continuous ⇑e → Continuous ⇑e.symm → IsUniformEmbedding ⇑e
-- Mathlib.Algebra.Group.ForwardDiff
fwdDiff_iter_choose_zero : ∀ (m n : ℕ), (fwdDiff 1)^[n] (fun x => ↑(x.choose m)) 0 = if n = m then 1 else 0
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.AbsolutelyContinuous.compProd_left : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : MeasureTheory.Measure α}
  [MeasureTheory.SFinite ν],
  μ.AbsolutelyContinuous ν → ∀ (κ : ProbabilityTheory.Kernel α β), (μ.compProd κ).AbsolutelyContinuous (ν.compProd κ)
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.algebraMap_inj : ∀ {R : Type u1} [inst : CommRing R] (M : Type u2) [inst_1 : AddCommGroup M] [inst_2 : Module R M] (x y : R),
  (algebraMap R (ExteriorAlgebra R M)) x = (algebraMap R (ExteriorAlgebra R M)) y ↔ x = y
-- Std.Time.Internal.Bounded
Std.Time.Internal.Bounded.instOrd : {rel : ℤ → ℤ → Prop} → {n m : ℤ} → Ord (Std.Time.Internal.Bounded rel n m)
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.D_off_diag_nonpos : ∀ (n : ℕ) (i j : Fin n), i ≠ j → CartanMatrix.D n i j ≤ 0
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.findSome?.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : (b : β) → motive (some b)) (h_2 : Unit → motive none),
  (match none with
    | some b => h_1 b
    | none => h_2 ()) =
    h_2 ()
-- Init.Data.Slice.List.Lemmas
List.size_mkSlice_roo : ∀ {α : Type u_1} {xs : List α} {lo hi : ℕ},
  Std.Slice.size (Std.Roo.Sliceable.mkSlice xs lo<...hi) = min hi xs.length - (lo + 1)
-- Mathlib.Algebra.Order.Floor.Defs
Int.floorRing_floor_eq : @FloorRing.floor = @Int.floor
-- Init.Data.Slice.Array.Lemmas
Subarray.toArray_mkSlice_rco : ∀ {α : Type u_1} {xs : Subarray α} {lo hi : ℕ},
  Std.Slice.toArray (Std.Rco.Sliceable.mkSlice xs lo...hi) = (Std.Slice.toArray xs).extract lo hi
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
CategoryTheory.Limits.IsCofiltered.sequentialFunctor_obj.congr_simp : ∀ (J : Type u_2) [inst : Countable J] [inst_1 : Preorder J] [inst_2 : CategoryTheory.IsCofiltered J] (a a_1 : ℕ),
  a = a_1 →
    CategoryTheory.Limits.IsCofiltered.sequentialFunctor_obj J a =
      CategoryTheory.Limits.IsCofiltered.sequentialFunctor_obj J a_1
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
/-- A class of morphisms `W : MorphismProperty C` is stable under infinite composition
if for any functor `F : ℕ ⥤ C` such that `F.obj n ⟶ F.obj (n + 1)` is in `W` for any `n : ℕ`,
the map `F.obj 0 ⟶ c.pt` is in `W` for any colimit cocone `c : Cocone F`.  -/
CategoryTheory.MorphismProperty.IsStableUnderInfiniteComposition : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → Prop
-- Init.Data.Order.Ord
Std.TransOrd.opposite : ∀ {α : Type u} [inst : Ord α] [Std.TransOrd α], Std.TransOrd α
-- Mathlib.Algebra.Order.GroupWithZero.Basic
one_le_mul_of_one_le_of_one_le : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Preorder M₀] {a b : M₀} [ZeroLEOneClass M₀] [PosMulMono M₀],
  1 ≤ a → 1 ≤ b → 1 ≤ a * b
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.namespaceId.inj : ∀ {stx stx_1 : Lean.Syntax},
  Lean.Elab.CompletionInfo.namespaceId stx = Lean.Elab.CompletionInfo.namespaceId stx_1 → stx = stx_1
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- The prime spectrum as an object of `TopCat`.  -/
AlgebraicGeometry.PrimeSpectrum.Top : (R : Type u) → [CommRing R] → TopCat
-- Mathlib.Order.Category.BddLat
/-- The equivalence between `BddLat` and itself induced by `OrderDual` both ways.  -/
BddLat.dualEquiv : BddLat ≌ BddLat
-- Mathlib.Probability.Process.FiniteDimensionalLaws
/-- The projective limit of the finite-dimensional distributions of a stochastic process is the law
of the process.  -/
ProbabilityTheory.isProjectiveLimit_map : ∀ {T : Type u_1} {Ω : Type u_2} {𝓧 : T → Type u_3} {mΩ : MeasurableSpace Ω} {mα : (t : T) → MeasurableSpace (𝓧 t)}
  {X : (t : T) → Ω → 𝓧 t} {P : MeasureTheory.Measure Ω},
  AEMeasurable (fun ω x => X x ω) P →
    MeasureTheory.IsProjectiveLimit (MeasureTheory.Measure.map (fun ω x => X x ω) P) fun I =>
      MeasureTheory.Measure.map (fun ω => I.restrict fun x => X x ω) P
-- Mathlib.Analysis.Calculus.FDeriv.Add
HasStrictFDerivAt.const_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} {R : Type u_4} [inst_5 : Monoid R] [inst_6 : DistribMulAction R F]
  [inst_7 : SMulCommClass 𝕜 R F] [inst_8 : ContinuousConstSMul R F],
  HasStrictFDerivAt f f' x → ∀ (c : R), HasStrictFDerivAt (c • f) (c • f') x
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift
/-- Consider a point `A` with barycentric coordinates associated to a collection of points `P`.
If the coordinate associated to one of the points `Pᵢ` is `r`, then the point `A` is on the span
of `P \ {Pᵢ}` shifted towards `Pᵢ` with parameter `1 - r`.  -/
AffineSubspace.affineCombination_mem_shift : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : AddTorsor V P]
  [inst_3 : Module k V] {ι : Type u_4} [inst_4 : Fintype ι] [Nontrivial ι] (p : ι → P) (i : ι) {w : ι → k},
  ∑ i, w i = 1 → (Finset.affineCombination k Finset.univ p) w ∈ (affineSpan k (p '' {i}ᶜ)).shift (p i) (1 - w i)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Measurable.norm : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup α] [OpensMeasurableSpace α]
  [inst_3 : MeasurableSpace β] {f : β → α}, Measurable f → Measurable fun a => ‖f a‖
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instVAdd'.eq_1 : ∀ {β : Type u_2} {α : Type u_1} [inst : VAdd β α], Colex.instVAdd' = inst
-- Init.Data.UInt.Lemmas
UInt32.add_sub_cancel : ∀ (a b : UInt32), a + b - b = a
-- Mathlib.CategoryTheory.Functor.KanExtension.Dense
_private.Mathlib.CategoryTheory.Functor.KanExtension.Dense.0.CategoryTheory.Functor.IsDense.of_fullyFaithful_restrictedULiftYoneda.match_1_1.eq_1 : ∀ {C : Type u_4} {D : Type u_5} [inst : CategoryTheory.Category.{u_1, u_4} C]
  [inst_1 : CategoryTheory.Category.{u_2, u_5} D] {F : CategoryTheory.Functor C D} (Y : D) (X : C)
  (motive : ((CategoryTheory.Presheaf.restrictedULiftYoneda F).obj Y).obj (Opposite.op X) → Sort u_6)
  (x : (CategoryTheory.yoneda.obj Y).obj (F.op.obj (Opposite.op X)))
  (h_1 : (x : (CategoryTheory.yoneda.obj Y).obj (F.op.obj (Opposite.op X))) → motive { down := x }),
  (match { down := x } with
    | { down := x } => h_1 x) =
    h_1 x
-- Lean.Data.FuzzyMatching
_private.Lean.Data.FuzzyMatching.0.Lean.FuzzyMatching.Score.inner : Lean.FuzzyMatching.Score✝ → Int16
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality
ContinuousCohomology.cocyclesMap_comp_assoc : ∀ {k : Type u} {G H K : Type v} [inst : Ring k] [inst_1 : TopologicalSpace k] [inst_2 : Group G]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalGroup G] [inst_5 : Group H] [inst_6 : TopologicalSpace H]
  [inst_7 : IsTopologicalGroup H] [inst_8 : Group K] [inst_9 : TopologicalSpace K] [inst_10 : IsTopologicalGroup K]
  {X : TopRep k G} {Y : TopRep k H} {Z : TopRep k K} (φ : H →ₜ* G) (ψ : K →ₜ* H) (f : TopRep.res (↑φ) X ⟶ Y)
  (g : TopRep.res (↑ψ) Y ⟶ Z) (n : ℕ) {Z_1 : TopModuleCat k} (h : ContinuousCohomology.cocycles Z n ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (ContinuousCohomology.cocyclesMap (φ.comp ψ)
        (CategoryTheory.CategoryStruct.comp (TopRep.ofHom (ContIntertwiningMap.restrict (↑ψ) (TopRep.Hom.hom f))) g) n)
      h =
    CategoryTheory.CategoryStruct.comp (ContinuousCohomology.cocyclesMap φ f n)
      (CategoryTheory.CategoryStruct.comp (ContinuousCohomology.cocyclesMap ψ g n) h)
-- Mathlib.Computability.Primrec.List
Primrec.vector_length : ∀ {α : Type u_1} [inst : Primcodable α] {n : ℕ}, Primrec List.Vector.length
-- Mathlib.Combinatorics.SimpleGraph.Metric
/-- The extended distance between vertices is equal to `1` if and only if these vertices are adjacent.
 -/
SimpleGraph.edist_eq_one_iff_adj : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, G.edist u v = 1 ↔ G.Adj u v
-- Mathlib.CategoryTheory.Sites.MayerVietorisSquare
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_exact : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat]
  (S : J.MayerVietorisSquare), S.shortComplex.Exact
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.isIntegral_root : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRootMonic S f), IsIntegral R h.root
-- Mathlib.RingTheory.FiniteType
Algebra.FiniteType.of_restrictScalars_finiteType : ∀ (R : Type uR) (S : Type uS) (A : Type uA) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A]
  [hA : Algebra.FiniteType R A], Algebra.FiniteType S A
-- Mathlib.RingTheory.MvPowerSeries.Rename
_private.Mathlib.RingTheory.MvPowerSeries.Rename.0.MvPowerSeries.renameFunAux : ∀ {σ : Type u_1} {τ : Type u_2} (f : σ → τ) [Filter.TendstoCofinite f] [inst : DecidableEq σ] (x : τ →₀ ℕ),
  {p | Finsupp.mapDomain f p.1 = x ∧ p.2 ∈ Finset.HasAntidiagonal.antidiagonal p.1}.Finite
-- Mathlib.Analysis.Calculus.FDeriv.Prod
HasFDerivAtFilter.snd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {L : Filter (E × E)} {f₂ : E → F × G}
  {f₂' : E →L[𝕜] F × G},
  HasFDerivAtFilter f₂ f₂' L → HasFDerivAtFilter (fun x => (f₂ x).2) (ContinuousLinearMap.snd 𝕜 F G ∘SL f₂') L
-- Init.Data.SInt.Bitwise
instLawfulCommIdentityInt16HXorOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 ^^^ x2) 0
-- Mathlib.Data.Real.Basic
Real.ofCauchy_one : { cauchy := 1 } = 1
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.le_weightedOrder_subst_of_forall_ne_zero : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S} (w : τ → ℕ),
  MvPowerSeries.HasSubst a →
    (∀ (i : σ), a i ≠ 0) →
      ∀ (f : MvPowerSeries σ R),
        MvPowerSeries.weightedOrder (ENat.toNat ∘ MvPowerSeries.weightedOrder w ∘ a) f ≤
          MvPowerSeries.weightedOrder w (MvPowerSeries.subst a f)
-- Init.Data.Nat.Gcd
Nat.gcd_mul_right_left : ∀ (m n : ℕ), (n * m).gcd n = n
-- Mathlib.Data.ENNReal.Inv
ENNReal.inv_le_inv : ∀ {a b : ENNReal}, a⁻¹ ≤ b⁻¹ ↔ b ≤ a
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.acyclic_truncLE_iff : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_3, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ)
  [inst_3 : ∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n₀ n₁ : ℤ),
  autoParam (n₀ + 1 = n₁) CochainComplex.acyclic_truncLE_iff._auto_1 →
    (HomologicalComplex.Acyclic (K.truncLE n₀) ↔ K.IsGE n₁)
-- Init.Core
/-- `strictAnd` is the same as `and`, but it does not use short-circuit evaluation semantics:
both sides are evaluated, even if the first value is `false`.
 -/
strictAnd : Bool → Bool → Bool
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Path.map_vertex : ∀ {X Y : SSet} {n : ℕ} (f : X.Path n) (σ : X ⟶ Y) (i : Fin (n + 1)),
  (f.map σ).vertex i = (CategoryTheory.ConcreteCategory.hom (σ.app (Opposite.op { len := 0 }))) (f.vertex i)
-- Std.Sync.Barrier
_private.Std.Sync.Barrier.0.Std.BarrierState.count : Std.BarrierState✝ → ℕ
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.indep_zero_right : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {m₁ m₂ _mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω}, ProbabilityTheory.Kernel.Indep m₁ m₂ κ 0
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
/-- An intermediate equivalence `A ≌ B'` whose functor is `F` and whose inverse is
`e'.inverse ⋙ eA.inverse`.  -/
AlgebraicTopology.DoldKan.Compatibility.equivalence₁ : {A : Type u_1} →
  {A' : Type u_2} →
    {B' : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} A] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} B'] →
            {eA : A ≌ A'} →
              {e' : A' ≌ B'} → {F : CategoryTheory.Functor A B'} → (eA.functor.comp e'.functor ≅ F) → (A ≌ B')
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- Eta-expanded form of `MeasureTheory.AEStronglyMeasurable.const_nsmul` -/
MeasureTheory.AEStronglyMeasurable.fun_const_nsmul : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} [inst_1 : AddMonoid β] [ContinuousAdd β],
  MeasureTheory.AEStronglyMeasurable f μ → ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (fun i => n • f i) μ
-- Mathlib.SetTheory.ZFC.PSet
PSet.mem_powerset : ∀ {x y : PSet.{u_1}}, y ∈ x.powerset ↔ y ⊆ x
-- Mathlib.RingTheory.Ideal.Operations
Ideal.isRadical_bot : ∀ {R : Type u} [inst : CommSemiring R] [IsReduced R], ⊥.IsRadical