mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.State.mk : Lean.PArray Lean.Expr →
  Lean.PHashMap Lean.Meta.Sym.ExprPtr Int.Internal.Linear.Var →
    Lean.PArray Lean.Expr →
      Lean.PHashMap Lean.Meta.Sym.ExprPtr Int.Internal.Linear.Var →
        Lean.PHashMap Lean.Meta.Sym.ExprPtr (Lean.Expr × Lean.Expr) →
          Lean.PHashMap Lean.Meta.Sym.ExprPtr Int.Internal.Linear.Var →
            Lean.PArray (Option Lean.Meta.Grind.Arith.Cutsat.DvdCnstr) →
              Lean.PArray (Lean.PArray Lean.Meta.Grind.Arith.Cutsat.LeCnstr) →
                Lean.PArray (Lean.PArray Lean.Meta.Grind.Arith.Cutsat.LeCnstr) →
                  Lean.PArray (Lean.PArray Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr) →
                    Lean.PArray (Option Lean.Meta.Grind.Arith.Cutsat.EqCnstr) →
                      List Int.Internal.Linear.Var →
                        Lean.PArray Lean.Meta.Grind.Arith.Cutsat.VarSet →
                          Lean.PArray ℚ →
                            ℕ →
                              Bool →
                                ℕ →
                                  Option Lean.Meta.Grind.Arith.Cutsat.UnsatProof →
                                    Lean.PHashMap Int.Internal.Linear.Poly Lean.FVarId →
                                      Lean.PHashSet (Lean.Expr × ℤ) →
                                        Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ) →
                                          Lean.PArray Lean.Meta.Grind.Arith.Cutsat.ToIntInfo →
                                            Lean.PHashMap Lean.Meta.Sym.ExprPtr
                                                Lean.Meta.Grind.Arith.Cutsat.ToIntTermInfo →
                                              Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Expr →
                                                Bool →
                                                  Lean.PHashMap Int.Internal.Linear.Var (List Int.Internal.Linear.Var) →
                                                    Lean.Meta.Grind.Arith.Cutsat.State
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.instBEqPoly.beq.eq_2 : ∀ (a : ℤ) (a_1 : Lean.Grind.Linarith.Var) (a_2 : Lean.Grind.Linarith.Poly) (b : ℤ) (b_1 : Lean.Grind.Linarith.Var)
  (b_2 : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.instBEqPoly.beq (Lean.Grind.Linarith.Poly.add a a_1 a_2)
      (Lean.Grind.Linarith.Poly.add b b_1 b_2) =
    (a == b && (a_1 == b_1 && Lean.Grind.Linarith.instBEqPoly.beq a_2 b_2))
-- Init.Data.BitVec.Lemmas
BitVec.toInt_add_of_not_saddOverflow : ∀ {w : ℕ} {x y : BitVec w}, ¬x.saddOverflow y = true → (x + y).toInt = x.toInt + y.toInt
-- Init.Data.SInt.Lemmas
ISize.toInt64_ofNat' : ∀ {n : ℕ}, ↑n ≤ ISize.maxValue.toInt → (ISize.ofNat n).toInt64 = Int64.ofNat n
-- Init.Sym.Lemmas
Lean.Sym.UInt64.le_eq_false : ∀ (a b : UInt64), decide (a ≤ b) = false → (a ≤ b) = False
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.stdPart_real : ∀ (r : ℝ), ArchimedeanClass.stdPart r = r
-- Mathlib.Order.Filter.Basic
LE.le.eventuallyLE : ∀ {α : Type u_1} {l : Filter α} {s t : Set α}, s ⊆ t → s ≤ᶠ[l] t
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.inf_toSubalgebra : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] (S T : StarSubalgebra R A),
  (S ⊓ T).toSubalgebra = S.toSubalgebra ⊓ T.toSubalgebra
-- Init.Data.SInt.Basic
/-- Bitwise or for 16-bit signed integers. Usually accessed via the `|||` operator.

Each bit of the resulting integer is set if at least one of the corresponding bits of the input
integers is set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.
 -/
Int16.lor : Int16 → Int16 → Int16
-- Mathlib.CategoryTheory.GuitartExact.VerticalComposition
CategoryTheory.TwoSquare.vComp'_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃]
  {H₁ : CategoryTheory.Functor C₁ D₁} {L₁ : CategoryTheory.Functor C₁ C₂} {R₁ : CategoryTheory.Functor D₁ D₂}
  {H₂ : CategoryTheory.Functor C₂ D₂} (w : CategoryTheory.TwoSquare H₁ L₁ R₁ H₂) {L₂ : CategoryTheory.Functor C₂ C₃}
  {R₂ : CategoryTheory.Functor D₂ D₃} {H₃ : CategoryTheory.Functor C₃ D₃} (w' : CategoryTheory.TwoSquare H₂ L₂ R₂ H₃)
  {L₁₂ : CategoryTheory.Functor C₁ C₃} {R₁₂ : CategoryTheory.Functor D₁ D₃} (eL : L₁.comp L₂ ≅ L₁₂)
  (eR : R₁.comp R₂ ≅ R₁₂) (X : C₁),
  (w.vComp' w' eL eR).app X =
    CategoryTheory.CategoryStruct.comp (eR.inv.app (H₁.obj X))
      (CategoryTheory.CategoryStruct.comp (R₂.map (w.natTrans.app X))
        (CategoryTheory.CategoryStruct.comp (w'.natTrans.app (L₁.obj X)) (H₃.map (eL.hom.app X))))
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
/-- Over a characteristic-zero division ring, the centroids of two
faces of a simplex are equal if and only if those faces are given by
the same subset of points.  -/
Affine.Simplex.face_centroid_eq_iff : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [CharZero k] {n : ℕ} (s : Affine.Simplex k P n) {fs₁ fs₂ : Finset (Fin (n + 1))} {m₁ m₂ : ℕ}
  (h₁ : fs₁.card = m₁ + 1) (h₂ : fs₂.card = m₂ + 1),
  Finset.centroid k Finset.univ (s.face h₁).points = Finset.centroid k Finset.univ (s.face h₂).points ↔ fs₁ = fs₂
-- Mathlib.RingTheory.Derivation.Basic
Derivation.coe_to_linearMap_comp : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M] (D : Derivation R A M)
  {N : Type u_5} [inst_6 : AddCommMonoid N] [inst_7 : Module A N] [inst_8 : Module R N] [inst_9 : IsScalarTower R A M]
  [inst_10 : IsScalarTower R A N] (f : M →ₗ[A] N), ↑(f.compDer D) = ↑R f ∘ₗ ↑D
-- Mathlib.LinearAlgebra.Basis.Bilinear
LinearMap.ext_iff_basis : ∀ {ι₁ : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {R₂ : Type u_4} {S : Type u_5} {S₂ : Type u_6} {M : Type u_7}
  {N : Type u_8} {P : Type u_9} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Semiring R₂] [inst_3 : Semiring S₂]
  [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid N] [inst_6 : AddCommMonoid P] [inst_7 : Module R M]
  [inst_8 : Module S N] [inst_9 : Module R₂ P] [inst_10 : Module S₂ P] [inst_11 : SMulCommClass S₂ R₂ P]
  {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (b₁ : Module.Basis ι₁ R M) (b₂ : Module.Basis ι₂ S N)
  {B B' : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P}, B = B' ↔ ∀ (i : ι₁) (j : ι₂), (B (b₁ i)) (b₂ j) = (B' (b₁ i)) (b₂ j)
-- Mathlib.Data.Holor
Holor.instAddCommGroup : {α : Type} → {ds : List ℕ} → [AddCommGroup α] → AddCommGroup (Holor α ds)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arccos_lt_pi : ∀ {x : ℝ}, Real.arccos x < Real.pi ↔ -1 < x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.toArray_toList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp}, t.toList.toArray = t.toArray
-- Mathlib.Data.Finset.Prod
Finset.product_val : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β}, (s ×ˢ t).val = s.val ×ˢ t.val
-- Mathlib.Topology.Category.UniformSpace
/-- The function forgetting that a complete separated uniform spaces is complete and separated.  -/
CpltSepUniformSpace.toUniformSpace : CpltSepUniformSpace → UniformSpaceCat
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrixRight'_comp : ∀ {R : Type u_1} [inst : Semiring R] {l : Type u_2} {m : Type u_3} {n : Type u_4} [inst_1 : Fintype m]
  [inst_2 : DecidableEq m] [inst_3 : Fintype l] [inst_4 : DecidableEq l] (f : (l → R) →ₗ[R] m → R)
  (g : (m → R) →ₗ[R] n → R), LinearMap.toMatrixRight' (g ∘ₗ f) = LinearMap.toMatrixRight' f * LinearMap.toMatrixRight' g
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
ContinuousWithinAt.arccos : ∀ {X : Type u_1} [inst : TopologicalSpace X] {f : X → ℝ} {s : Set X} {x : X},
  ContinuousWithinAt f s x → ContinuousWithinAt (fun x => Real.arccos (f x)) s x
-- Mathlib.Topology.Order.LiminfLimsup
Prod.instBoundedGENhdsClass : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : TopologicalSpace α]
  [inst_3 : TopologicalSpace β] [BoundedGENhdsClass α] [BoundedGENhdsClass β], BoundedGENhdsClass (α × β)
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.irrelevant.congr_simp : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddCommMonoid ι]
  [inst_3 : PartialOrder ι] [inst_4 : CanonicallyOrderedAdd ι] [inst_5 : SetLike σ A] [inst_6 : AddSubmonoidClass σ A]
  (𝒜 : ι → σ) [inst_7 : GradedRing 𝒜], HomogeneousIdeal.irrelevant 𝒜 = HomogeneousIdeal.irrelevant 𝒜
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isEmpty_eq_isEmpty_erase_and_not_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ (k : α), t.isEmpty = ((t.erase k).isEmpty && !t.contains k)
-- Lean.DocString.Syntax
Lean.Doc.Syntax.metadataContents.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Combinatorics.Quiver.Symmetric
Quiver.Symmetrify.of_map : ∀ {V : Type u_2} [inst : Quiver V] {X Y : V} (val : X ⟶ Y), Quiver.Symmetrify.of.map val = Sum.inl val
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- The (left) homology map `S₁.leftHomology ⟶ S₂.leftHomology` induced by a morphism
`S₁ ⟶ S₂` of short complexes.  -/
CategoryTheory.ShortComplex.leftHomologyMap : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        [inst_2 : S₁.HasLeftHomology] → [inst_3 : S₂.HasLeftHomology] → (S₁ ⟶ S₂) → (S₁.leftHomology ⟶ S₂.leftHomology)
-- Mathlib.RingTheory.RingHom.StandardSmooth
RingHom.IsStandardSmoothOfRelativeDimension.equiv : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S),
  RingHom.IsStandardSmoothOfRelativeDimension 0 ↑e
-- Std.Async.Basic
Std.Async.EAsync.instMonadExceptOf : {ε : Type} → MonadExceptOf ε (Std.Async.EAsync ε)
-- Mathlib.Topology.MetricSpace.Defs
MetricSpace.replaceUniformity_eq : ∀ {γ : Type u_3} [U : UniformSpace γ] (m : MetricSpace γ) (H : uniformity γ = uniformity γ), m.replaceUniformity H = m
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplex.barycenter.eq_1 : ∀ {X : Type u_2} [inst : Fintype X] {𝕜 : Type u_5} [inst_1 : Field 𝕜] [inst_2 : LinearOrder 𝕜]
  [inst_3 : IsStrictOrderedRing 𝕜] [inst_4 : Nonempty X], stdSimplex.barycenter = ⟨fun i => (↑(Fintype.card X))⁻¹, ⋯⟩
-- Init.Prelude
/-- The number of distinct values representable by `UInt64`, that is, `2^64 = 18446744073709551616`.  -/
UInt64.size : ℕ
-- Init.Data.List.ToArray
Array.findSomeM?.eq_1 : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : α → m (Option β)) (as : Array α),
  Array.findSomeM? f as = do
    let __s ←
      forIn as (none, ()) fun a __s => do
          let __do_lift ← f a
          match __do_lift with
            | some b => pure (ForInStep.done (some (some b), ()))
            | x => pure (ForInStep.yield (none, ()))
    have __r : Option (Option β) × Unit := __s
    match __r.1 with
      | some r => pure r
      | none => pure none
-- Mathlib.Data.ZMod.Basic
ZMod.natCast_eq_one_iff_odd : ∀ {n : ℕ}, ↑n = 1 ↔ Odd n
-- Mathlib.Topology.Order.LeftRight
nhdsLT_sup_nhdsGT : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] (a : α),
  nhdsWithin a (Set.Iio a) ⊔ nhdsWithin a (Set.Ioi a) = nhdsWithin a {a}ᶜ
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.op_smul_eq_op_smul_iff_mem : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {x y : G},
  x ∈ MulOpposite.op y • ↑H ↔ MulOpposite.op x • ↑H = MulOpposite.op y • ↑H
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.insertListIfNewₘ : {α : Type u} →
  {β : α → Type v} →
    [BEq α] → [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → List ((a : α) × β a) → Std.DHashMap.Internal.Raw₀ α β
-- Mathlib.Algebra.Group.Action.Pi
/-- Non-dependent version of `Pi.vaddCommClass`. Lean gets confused by the dependent
instance if this is not present.  -/
Function.vaddCommClass : ∀ {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : Type u_7} [inst : VAdd M α] [inst_1 : VAdd N α]
  [VAddCommClass M N α], VAddCommClass M N (ι → α)
-- Lean.Expr
/-- Return true iff `e` contains a free variable which satisfies `p`.  -/
Lean.Expr.hasAnyFVar : Lean.Expr → (Lean.FVarId → Bool) → Bool
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.op_map : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (φ : W.LeftFraction X Y) (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L), (φ.map L hL).op = φ.op.map L.op ⋯
-- Mathlib.MeasureTheory.PiSystem
MeasurableSpace.DynkinSystem.GenerateHas.compl : ∀ {α : Type u_3} {s : Set (Set α)} {a : Set α},
  MeasurableSpace.DynkinSystem.GenerateHas s a → MeasurableSpace.DynkinSystem.GenerateHas s aᶜ
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap
fderiv_continuousMultilinearMapCompContinuousLinearMap : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} {H : Type u_6}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : (i : ι) → NormedAddCommGroup (F i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (F i)]
  [inst_5 : (i : ι) → NormedAddCommGroup (G i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (G i)] [inst_7 : NormedAddCommGroup H]
  [inst_8 : NormedSpace 𝕜 H] {f : E → ContinuousMultilinearMap 𝕜 G H} {g : (i : ι) → E → F i →L[𝕜] G i} {x : E}
  [inst_9 : Fintype ι] [inst_10 : DecidableEq ι],
  DifferentiableAt 𝕜 f x →
    (∀ (i : ι), DifferentiableAt 𝕜 (g i) x) →
      fderiv 𝕜 (fun x => (f x).compContinuousLinearMap fun x_1 => g x_1 x) x =
        (ContinuousMultilinearMap.compContinuousLinearMapL fun x_1 => g x_1 x) ∘SL fderiv 𝕜 f x +
          ((f x).fderivCompContinuousLinearMap fun x_1 => g x_1 x) ∘SL ContinuousLinearMap.pi fun i => fderiv 𝕜 (g i) x
-- Mathlib.Algebra.Lie.UniversalEnveloping
UniversalEnvelopingAlgebra.hom_ext_iff : ∀ {R : Type u₁} {L : Type u₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {A : Type u₃}
  [inst_3 : Ring A] [inst_4 : Algebra R A] {g₁ g₂ : UniversalEnvelopingAlgebra R L →ₐ[R] A},
  g₁ = g₂ ↔ g₁.toLieHom.comp (UniversalEnvelopingAlgebra.ι R) = g₂.toLieHom.comp (UniversalEnvelopingAlgebra.ι R)
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles_apply : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) (x : ↑S.moduleCatLeftHomologyData.K),
  (CategoryTheory.ConcreteCategory.hom S.iCycles) ((CategoryTheory.ConcreteCategory.hom S.moduleCatCyclesIso.inv) x) =
    (CategoryTheory.ConcreteCategory.hom S.moduleCatLeftHomologyData.i) x
-- Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
_private.Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess.0.Finset.orderEmbOfFinWithBot_succ : ∀ {T : Type u_1} [inst : LinearOrder T] (I : Finset T) [inst_1 : Bot T] (i : Fin I.card),
  Finset.orderEmbOfFinWithBot✝ I i.succ = (I.orderEmbOfFin ⋯) i
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.c₄_of_isCharThreeJNeZeroNF_of_char_three : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF] [CharP R 3], W.c₄ = W.a₂ ^ 2
-- Mathlib.Analysis.LocallyConvex.Basic
/-- **Alias** of the forward direction of `absorbent_iff_eventually_nhdsNE_zero`. -/
Absorbent.eventually_nhdsNE_zero : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {s : Set E}, Absorbent 𝕜 s → ∀ (x : E), ∀ᶠ (c : 𝕜) in nhdsWithin 0 {0}ᶜ, c • x ∈ s
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
/-- The first triangle identity for the counit and unit of the adjunction.  -/
CategoryTheory.ExponentiableMorphism.ev_coev : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I J : C} (f : I ⟶ J)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong f] [inst_2 : CategoryTheory.ExponentiableMorphism f]
  (X : CategoryTheory.Over J),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.ChosenPullbacksAlong.pullback f).map ((CategoryTheory.ExponentiableMorphism.coev f).app X))
      ((CategoryTheory.ExponentiableMorphism.ev f).app ((CategoryTheory.ChosenPullbacksAlong.pullback f).obj X)) =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.ChosenPullbacksAlong.pullback f).obj X)
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
ProbabilityTheory.Kernel.partialTraj_succ_of_le : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} {a b : ℕ}
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))},
  a ≤ b →
    ProbabilityTheory.Kernel.partialTraj κ a (b + 1) =
      ((ProbabilityTheory.Kernel.id.prod ((κ b).map ⇑(MeasurableEquiv.piSingleton b))).comp
            (ProbabilityTheory.Kernel.partialTraj κ a b)).map
        (IicProdIoc b (b + 1))
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.replace.eq_1 : ∀ {α : Type u} [inst : BEq α] (xs : Array α) (a b : α),
  xs.replace a b =
    match xs.finIdxOf? a with
    | none => xs
    | some i => xs.set (↑i) b ⋯
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
/-- Exactness of `Hᵢ(G, X₃) ⟶ Hⱼ(G, X₁) ⟶ Hⱼ(G, X₂)`.  -/
groupHomology.mapShortComplex₁_exact : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)}
  (hX : X.ShortExact) {i j : ℕ} (hij : j + 1 = i), (groupHomology.mapShortComplex₁ hX hij).Exact
-- Mathlib.Algebra.Torsor.Defs
/-- If the same point multiplied with two group elements produces equal
results, those group elements are equal.  -/
smul_right_cancel : ∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [T : Torsor G P] {g₁ g₂ : G} (p : P), g₁ • p = g₂ • p → g₁ = g₂
-- Mathlib.Order.Hom.Bounded
BoundedOrderHom.dual_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : BoundedOrder α] [inst_2 : Preorder β]
  [inst_3 : BoundedOrder β] [inst_4 : Preorder γ] [inst_5 : BoundedOrder γ] (g : BoundedOrderHom β γ)
  (f : BoundedOrderHom α β), BoundedOrderHom.dual (g.comp f) = (BoundedOrderHom.dual g).comp (BoundedOrderHom.dual f)
-- Lean.Structure
Lean.instInhabitedStructureResolutionOrderResult.default : Lean.StructureResolutionOrderResult
-- Mathlib.Data.ENat.Basic
/-- **Alias** of `ENat.addLECancellable_natCast`. -/
ENat.addLECancellable_coe : ∀ (a : ℕ), AddLECancellable ↑a
-- Init.Omega.Constraint
/-- Shorthand for the second component of `normalize`.  -/
Lean.Omega.normalizeCoeffs : Lean.Omega.Constraint → Lean.Omega.Coeffs → Lean.Omega.Coeffs
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.size_filterMap_eq_size_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  [Std.TransCmp cmp] {f : α → β → Option γ},
  t.WF →
    ((Std.DTreeMap.Raw.filterMap f t).size = t.size ↔
      ∀ (k : α) (h : k ∈ t), (f (t.getKey k h) (Std.DTreeMap.Raw.Const.get t k h)).isSome = true)
-- Mathlib.CategoryTheory.Monoidal.Braided.Reflection
_private.Mathlib.CategoryTheory.Monoidal.Braided.Reflection.0.CategoryTheory.Monoidal.Reflective.adjRetractionAux.congr_simp : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory D]
  [inst_3 : CategoryTheory.SymmetricCategory D] [inst_4 : CategoryTheory.MonoidalClosed D]
  {R : CategoryTheory.Functor C D} [inst_5 : R.Faithful] [inst_6 : R.Full] {L : CategoryTheory.Functor D C}
  (adj adj_1 : L ⊣ R) (e_adj : adj = adj_1) (c : C) (d : D)
  [inst_7 :
    CategoryTheory.IsIso
      (L.map (CategoryTheory.MonoidalCategoryStruct.tensorHom (adj.unit.app (d ⟹ R.obj c)) (adj.unit.app d)))],
  CategoryTheory.Monoidal.Reflective.adjRetractionAux✝ adj c d =
    CategoryTheory.Monoidal.Reflective.adjRetractionAux✝ adj_1 c d
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.prod_multiset_root_eq_finset_root : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R} [inst_2 : DecidableEq R],
  (Multiset.map (fun a => Polynomial.X - Polynomial.C a) p.roots).prod =
    ∏ a ∈ p.roots.toFinset, (Polynomial.X - Polynomial.C a) ^ Polynomial.rootMultiplicity a p
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt32.reduceToNat : Lean.Meta.Simp.DSimproc
-- Mathlib.Topology.Algebra.Ring.Basic
NonUnitalSubring.le_topologicalClosure : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : NonUnitalRing R] [inst_2 : IsSemitopologicalRing R]
  (s : NonUnitalSubring R), s ≤ s.topologicalClosure
-- Mathlib.Data.List.Sigma
/-- `kunion l₁ l₂` is the append to l₁ of l₂ after, for each key in l₁, the
first matching pair in l₂ is erased.  -/
List.kunion : {α : Type u} → {β : α → Type v} → [DecidableEq α] → List (Sigma β) → List (Sigma β) → List (Sigma β)
-- Init.Data.Range.Polymorphic.PRange
Std.Roo.instDecidableMemOfDecidableLT : {α : Type u} → {r : Std.Roo α} → {a : α} → [inst : LT α] → [DecidableLT α] → Decidable (a ∈ r)
-- Mathlib.NumberTheory.LocalField.Basic
IsNonarchimedeanLocalField.instIsDiscreteValuationRingSubtypeMemSubringIntegerValueGroupWithZeroValuation : ∀ (K : Type u_1) [inst : Field K] [inst_1 : ValuativeRel K] [inst_2 : TopologicalSpace K]
  [IsNonarchimedeanLocalField K], IsDiscreteValuationRing ↥(ValuativeRel.valuation K).integer
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtDTreeMap α β cmp),
  t = t_1 → ∀ (a a_1 : α), a = a_1 → t.getKey? a = t_1.getKey? a_1
-- Mathlib.Analysis.Convex.Gauge
gauge_smul_left : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {α : Type u_3} [inst_2 : Field α]
  [inst_3 : LinearOrder α] [IsStrictOrderedRing α] [inst_5 : MulActionWithZero α ℝ] [IsStrictOrderedModule α ℝ]
  [inst_7 : Module α E] [SMulCommClass α ℝ ℝ] [IsScalarTower α ℝ ℝ] [IsScalarTower α ℝ E] {s : Set E},
  (∀ x ∈ s, -x ∈ s) → ∀ (a : α), gauge (a • s) = |a|⁻¹ • gauge s
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
/-- The right Kan extension functor `(C ⥤ H) ⥤ (D ⥤ H)` along a functor `C ⥤ D`.  -/
CategoryTheory.Functor.ran : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (L : CategoryTheory.Functor C D) →
          {H : Type u_3} →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} H] →
              [∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F] →
                CategoryTheory.Functor (CategoryTheory.Functor C H) (CategoryTheory.Functor D H)
-- Mathlib.Data.Num.ZNum
_private.Mathlib.Data.Num.ZNum.0.PosNum.sub'.match_1.eq_4 : ∀ (motive : PosNum → PosNum → Sort u_1) (a b : PosNum) (h_1 : (a : PosNum) → motive a PosNum.one)
  (h_2 : (b : PosNum) → motive PosNum.one b) (h_3 : (a b : PosNum) → motive a.bit0 b.bit0)
  (h_4 : (a b : PosNum) → motive a.bit0 b.bit1) (h_5 : (a b : PosNum) → motive a.bit1 b.bit0)
  (h_6 : (a b : PosNum) → motive a.bit1 b.bit1),
  (match a.bit0, b.bit1 with
    | a, PosNum.one => h_1 a
    | PosNum.one, b => h_2 b
    | a.bit0, b.bit0 => h_3 a b
    | a.bit0, b.bit1 => h_4 a b
    | a.bit1, b.bit0 => h_5 a b
    | a.bit1, b.bit1 => h_6 a b) =
    h_4 a b
-- Init.Core
MProd.mk.inj : ∀ {α β : Type u} {fst : α} {snd : β} {fst_1 : α} {snd_1 : β}, ⟨fst, snd⟩ = ⟨fst_1, snd_1⟩ → fst = fst_1 ∧ snd = snd_1