mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.LatticeIntervals
Set.Ici.codisjoint_iff : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderTop α] {a : α} {x y : ↑(Set.Ici a)},
  Codisjoint x y ↔ Codisjoint ↑x ↑y
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
ZetaAsymptotics.term_nonneg : ∀ (n : ℕ) (s : ℝ), 0 ≤ ZetaAsymptotics.term n s
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- The cones for `StructuredArrow.proj Y L ⋙ F`, as a functor from `RightExtension L F`.  -/
CategoryTheory.Functor.RightExtension.coneAtFunctor : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            (L : CategoryTheory.Functor C D) →
              (F : CategoryTheory.Functor C H) →
                (Y : D) →
                  CategoryTheory.Functor (L.RightExtension F)
                    (CategoryTheory.Limits.Cone ((CategoryTheory.StructuredArrow.proj Y L).comp F))
-- Mathlib.Algebra.Group.Hom.Instances
instIsRightCancelMulMonoidHom : ∀ {M : Type uM} {N : Type uN} [inst : MulOneClass M] [inst_1 : CommMonoid N] [IsRightCancelMul N],
  IsRightCancelMul (M →* N)
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.coe_id' : ∀ (R : Type u_1) [inst : CommSemiring R] (A : Type u_2) [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  [inst_3 : Algebra R A], ⇑(ContinuousAlgHom.id R A) = id
-- Mathlib.Topology.Order.DenselyOrdered
/-- If `α` is a nontrivial separable dense linear order, then there exists a
countable dense set `s : Set α` that contains neither top nor bottom elements of `α`.
For a dense set containing both bot and top elements, see
`exists_countable_dense_bot_top`.  -/
exists_countable_dense_no_bot_top : ∀ (α : Type u_1) [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [TopologicalSpace.SeparableSpace α] [Nontrivial α],
  ∃ s, s.Countable ∧ Dense s ∧ (∀ (x : α), IsBot x → x ∉ s) ∧ ∀ (x : α), IsTop x → x ∉ s
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
MeasureTheory.IntegrableOn.intervalIntegrable : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] {f : ℝ → ε} {a b : ℝ}
  {μ : MeasureTheory.Measure ℝ}, MeasureTheory.IntegrableOn f (Set.uIcc a b) μ → IntervalIntegrable f μ a b
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.CompleteBipartiteGraph.chromaticNumber : ∀ {V : Type u_4} {W : Type u_5} [Nonempty V] [Nonempty W], (completeBipartiteGraph V W).chromaticNumber = 2
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.image_exp_Ici : ∀ (a : ℝ), Real.exp '' Set.Ici a = Set.Ici (Real.exp a)
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.comp_id : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (F : L →ᴸ L'), F.comp (FirstOrder.Language.LHom.id L) = F
-- Mathlib.Computability.TuringMachine.Tape
/-- Construct a tape from a left side and an inclusive right side.  -/
Turing.Tape.mk₂ : {Γ : Type u_1} → [inst : Inhabited Γ] → List Γ → List Γ → Turing.Tape Γ
-- Mathlib.CategoryTheory.Equivalence.Symmetry
CategoryTheory.Equivalence.inverseFunctorObj'_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (e : C ≌ D) (X : D),
  e.inverseFunctorObj'.hom.app X = CategoryTheory.CategoryStruct.id (e.inverse.obj X)
-- Mathlib.Algebra.Polynomial.SpecificDegree
/-- A polynomial of degree 2 or 3 is irreducible iff it doesn't have roots.  -/
Polynomial.Monic.irreducible_iff_roots_eq_zero_of_degree_le_three : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R},
  p.Monic → 2 ≤ p.natDegree → p.natDegree ≤ 3 → (Irreducible p ↔ p.roots = 0)
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instLeftCancelSemigroup : {α : Type u_1} → {l : Filter α} → {M : Type u_5} → [LeftCancelSemigroup M] → LeftCancelSemigroup (l.Germ M)
-- Mathlib.Topology.Algebra.ConstMulAction
nhds_vadd : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : AddGroup G] [inst_2 : AddAction G α]
  [ContinuousConstVAdd G α] (c : G) (x : α), nhds (c +ᵥ x) = c +ᵥ nhds x
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.IsUnramified.eq_1 : ∀ (k : Type u_1) [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K]
  (w : NumberField.InfinitePlace K),
  NumberField.InfinitePlace.IsUnramified k w = ((w.comap (algebraMap k K)).mult = w.mult)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFractionRel.trans : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  {z₁ z₂ z₃ : W.LeftFraction X Y} [W.HasLeftCalculusOfFractions],
  CategoryTheory.MorphismProperty.LeftFractionRel z₁ z₂ →
    CategoryTheory.MorphismProperty.LeftFractionRel z₂ z₃ → CategoryTheory.MorphismProperty.LeftFractionRel z₁ z₃
-- Mathlib.Data.Matrix.Diagonal
Matrix.diagonal_injective : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α], Function.Injective Matrix.diagonal
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.subset_zeroLocus_iff_le_vanishingIdeal : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] (t : Set (ProjectiveSpectrum 𝒜)) (I : Ideal A),
  t ⊆ ProjectiveSpectrum.zeroLocus 𝒜 ↑I ↔ I ≤ (ProjectiveSpectrum.vanishingIdeal t).toIdeal
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiff.fun_comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {g : F → G} {f : E → F},
  ContDiff 𝕜 n g → ContDiff 𝕜 n f → ContDiff 𝕜 n fun x => g (f x)
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
_private.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.0.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore.analyzeArg : ℕ → Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeAppM Unit
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool} {k : α},
  Std.DHashMap.Const.get? (Std.DHashMap.filter f m) k =
    (Std.DHashMap.Const.get? m k).pfilter fun x_2 h' => f (m.getKey k ⋯) x_2
-- Mathlib.Combinatorics.Configuration
Configuration.ProjectivePlane.mk : {P : Type u_1} →
  {L : Type u_2} →
    [inst : Membership P L] →
      [toHasPoints : Configuration.HasPoints P L] →
        (mkLine : {p₁ p₂ : P} → p₁ ≠ p₂ → L) →
          (∀ {p₁ p₂ : P} (h : p₁ ≠ p₂), p₁ ∈ mkLine h ∧ p₂ ∈ mkLine h) →
            (∃ p₁ p₂ p₃ l₁ l₂ l₃, p₁ ∉ l₂ ∧ p₁ ∉ l₃ ∧ p₂ ∉ l₁ ∧ p₂ ∈ l₂ ∧ p₂ ∈ l₃ ∧ p₃ ∉ l₁ ∧ p₃ ∈ l₂ ∧ p₃ ∉ l₃) →
              Configuration.ProjectivePlane P L
-- Mathlib.Analysis.VonNeumannAlgebra.Basic
/-- An idempotent is an element in a von Neumann algebra if and only if
its range and kernel are invariant under the commutant.  -/
VonNeumannAlgebra.IsIdempotentElem.mem_iff : ∀ {H : Type u} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℂ H] [inst_2 : CompleteSpace H]
  {e : H →L[ℂ] H},
  IsIdempotentElem e →
    ∀ (S : VonNeumannAlgebra H),
      e ∈ S ↔ ∀ y ∈ S.commutant, (↑e).range ∈ Module.End.invtSubmodule ↑y ∧ (↑e).ker ∈ Module.End.invtSubmodule ↑y
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
HasFTaylorSeriesUpTo.zero_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {f : E → F} {p : E → FormalMultilinearSeries 𝕜 E F}, HasFTaylorSeriesUpTo n f p → ∀ (x : E), (p x 0).curry0 = f x
-- Mathlib.Logic.Equiv.Sum
/-- Sum of types is associative up to an equivalence.  -/
Equiv.sumAssoc : (α : Type u_9) → (β : Type u_10) → (γ : Type u_11) → (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γ
-- Init.Data.Vector.Lemmas
Vector.set_push : ∀ {α : Type u_1} {n i : ℕ} {xs : Vector α n} {x y : α} {h : i < n + 1},
  (xs.push x).set i y h = if x_1 : i < n then (xs.set i y x_1).push x else xs.push y
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey?_alter_eq_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β}, (t.alter k f).minKey? = some k ↔ (f t[k]?).isSome = true ∧ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.Analysis.Analytic.Basic
AnalyticOnNhd.congr' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F} {s : Set E},
  AnalyticOnNhd 𝕜 f s → f =ᶠ[nhdsSet s] g → AnalyticOnNhd 𝕜 g s
-- Mathlib.ModelTheory.Definability
/-- A singleton is definable by parameter as itself.  -/
Set.Definable.singleton : ∀ {M : Type w} (L : FirstOrder.Language) [inst : L.Structure M] (a : M), {a}.Definable₁ L {a}
-- Mathlib.Data.Nat.ModEq
Nat.modEq_iff_exists_eq_add : ∀ {n a b : ℕ}, a ≤ b → (a ≡ b [MOD n] ↔ ∃ t, b = a + n * t)
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Localization.localAlgEquiv'_symm_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {P : Type u_3}
  [inst_3 : CommSemiring P] (I : Ideal R) [hI : I.IsPrime] [inst_4 : Algebra R P] (J : Ideal S) (K : Ideal P)
  [inst_5 : J.IsPrime] [inst_6 : K.IsPrime] [inst_7 : J.LiesOver I]
  [inst_8 : Algebra (Localization.AtPrime I) (Localization.AtPrime J)]
  [inst_9 : Localization.AtPrime.IsLiesOverAlgebra I J] [inst_10 : K.LiesOver I]
  [inst_11 : Algebra (Localization.AtPrime I) (Localization.AtPrime K)]
  [inst_12 : Localization.AtPrime.IsLiesOverAlgebra I K] (f : S ≃ₐ[R] P) (h : J = Ideal.comap f K)
  (a : Localization.AtPrime K),
  (Localization.localAlgEquiv' I J K f h).symm a =
    (Localization.localRingHom K J ↑{ toEquiv := ↑f.symm, map_mul' := ⋯, map_add' := ⋯ } ⋯) a
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
_private.Mathlib.CategoryTheory.Monoidal.Free.Coherence.0.CategoryTheory.FreeMonoidalCategory.normalizeIsoApp'.match_1.splitter : (C : Type u_1) →
  (motive :
      CategoryTheory.FreeMonoidalCategory C → CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C → Sort u_2) →
    (x : CategoryTheory.FreeMonoidalCategory C) →
      (x_1 : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) →
        ((a : C) →
            (x : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) →
              motive (CategoryTheory.FreeMonoidalCategory.of a) x) →
          ((x : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) →
              motive CategoryTheory.FreeMonoidalCategory.unit x) →
            ((X Y : CategoryTheory.FreeMonoidalCategory C) →
                (n : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) → motive (X.tensor Y) n) →
              motive x x_1
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
/-- Bessel's inequality.  -/
Orthonormal.tsum_inner_products_le : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} (x : E) {v : ι → E}, Orthonormal 𝕜 v → ∑' (i : ι), ‖inner 𝕜 (v i) x‖ ^ 2 ≤ ‖x‖ ^ 2
-- Mathlib.Analysis.Normed.Affine.Convex
dist_add_dist_of_mem_segment : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {x y z : E},
  y ∈ segment ℝ x z → dist x y + dist y z = dist x z
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.zero_eq_coe : ∀ {α : Type u} [inst : Zero α] {a : α}, 0 = ↑a ↔ a = 0
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv : ∀ {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} {assign : Std.Tactic.BVDecide.BVExpr.Assignment} {w : ℕ}
  (cache : Std.Tactic.BVDecide.BVExpr.Cache aig),
  Std.Tactic.BVDecide.BVExpr.Cache.Inv assign aig cache →
    ∀ (expr : Std.Tactic.BVDecide.BVExpr w),
      Std.Tactic.BVDecide.BVExpr.Cache.Inv assign
        (↑(Std.Tactic.BVDecide.BVExpr.bitblast.goCache aig expr cache).result).aig
        (Std.Tactic.BVDecide.BVExpr.bitblast.goCache aig expr cache).cache
-- Mathlib.Algebra.Ring.Parity
Nat.odd_sub' : ∀ {m n : ℕ}, n ≤ m → (Odd (m - n) ↔ (Odd n ↔ Even m))
-- Mathlib.Algebra.Group.Units.Defs
divp_mul_cancel : ∀ {α : Type u} [inst : Monoid α] (a : α) (u : αˣ), a /ₚ u * ↑u = a
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.SplitStatus.resolved : Lean.Meta.Grind.SplitStatus
-- Init.Data.Nat.ToString
_private.Init.Data.Nat.ToString.0.Nat.toDigitsCore.match_1.splitter : (motive : ℕ → ℕ → List Char → Sort u_1) →
  (x x_1 : ℕ) →
    (x_2 : List Char) →
      ((x : ℕ) → (ds : List Char) → motive 0 x ds) →
        ((fuel n : ℕ) → (ds : List Char) → motive fuel.succ n ds) → motive x x_1 x_2
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin.0.Fin.Value.mk.injEq : ∀ (n : ℕ) (value : Fin n) (n_1 : ℕ) (value_1 : Fin n_1),
  ({ n := n, value := value } = { n := n_1, value := value_1 }) = (n = n_1 ∧ value ≍ value_1)
-- Init.Control.Do
/-- A wrapper around `ExceptT` signifying early return.  -/
EarlyReturnT : Type u_1 → (Type u_1 → Type u_2) → Type u_1 → Type u_2
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- Isomorphic rings have isomorphic monoid algebras.  -/
MonoidAlgebra.mapRingEquiv : {R : Type u_3} →
  {S : Type u_4} →
    (M : Type u_6) →
      [inst : Semiring R] →
        [inst_1 : Semiring S] → [inst_2 : Monoid M] → R ≃+* S → MonoidAlgebra R M ≃+* MonoidAlgebra S M
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.ortho_smul_right : ∀ {K : Type u_13} {K₁ : Type u_14} {K₂ : Type u_15} {V : Type u_16} {V₁ : Type u_17} {V₂ : Type u_18} [inst : Field K]
  [inst_1 : AddCommGroup V] [inst_2 : Module K V] [inst_3 : Field K₁] [inst_4 : AddCommGroup V₁] [inst_5 : Module K₁ V₁]
  [inst_6 : Field K₂] [inst_7 : AddCommGroup V₂] [inst_8 : Module K₂ V₂] {I₁ : K₁ →+* K} {I₂ : K₂ →+* K}
  {B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V} {x : V₁} {y : V₂} {a : K₂} {ha : a ≠ 0}, B.IsOrtho x y ↔ B.IsOrtho x (a • y)
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.smul_apply : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W) (a : A) (f : ρ.IntertwiningMap σ) (v : V), (a • f) v = a • f v
-- Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence
Mathlib.Tactic.BicategoryLike.Normalize.Result.mk.injEq : ∀ (normalizedHom : Mathlib.Tactic.BicategoryLike.NormalizedHom) (toNormalize : Mathlib.Tactic.BicategoryLike.Mor₂Iso)
  (normalizedHom_1 : Mathlib.Tactic.BicategoryLike.NormalizedHom)
  (toNormalize_1 : Mathlib.Tactic.BicategoryLike.Mor₂Iso),
  ({ normalizedHom := normalizedHom, toNormalize := toNormalize } =
      { normalizedHom := normalizedHom_1, toNormalize := toNormalize_1 }) =
    (normalizedHom = normalizedHom_1 ∧ toNormalize = toNormalize_1)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isClosedEmbedding_comap_snd : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S],
  Topology.IsClosedEmbedding (PrimeSpectrum.comap (RingHom.snd R S))
-- Mathlib.LinearAlgebra.QuadraticForm.Dual
/-- The isometry sending `(Q.prod <| -Q)` to `(QuadraticForm.dualProd R M)`.

This is `σ` from Proposition 4.8, page 84 of
[*Hermitian K-Theory and Geometric Applications*][hyman1973]; though we swap the order of the pairs.
 -/
QuadraticForm.toDualProd : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (Q : QuadraticForm R M) → [Invertible 2] → QuadraticMap.prod Q (-Q) →qᵢ QuadraticForm.dualProd R M
-- Init.Data.Iterators.Lemmas.Combinators.Append
_private.Init.Data.Iterators.Lemmas.Combinators.Append.0.Std.Iter.step_append.match_1.splitter : {α₁ β : Type u_1} →
  [inst : Std.Iterator α₁ Id β] →
    {it₁ : Std.Iter β} →
      (motive : it₁.Step → Sort u_2) →
        (x : it₁.Step) →
          ((it₁' : Std.Iter β) →
              (out : β) →
                (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out)) → motive ⟨Std.IterStep.yield it₁' out, h⟩) →
            ((it₁' : Std.Iter β) →
                (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', h⟩) →
              ((h : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) → motive x
-- Init.Data.SInt.Basic
/-- Bitwise exclusive or for 16-bit signed integers. Usually accessed via the `^^^` operator.

Each bit of the resulting integer is set if exactly 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.xor : Int16 → Int16 → Int16
-- Mathlib.Topology.Bases
TopologicalSpace.isTopologicalBasis_singleton_empty : ∀ {α : Type u} [t : TopologicalSpace α], TopologicalSpace.IsTopologicalBasis {∅} ↔ IsEmpty α
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
/-- The source vertex of `coherentIso`.  -/
SSet.coherentIso.x₀ : SSet.coherentIso.obj (Opposite.op { len := 0 })
-- Mathlib.Probability.Independence.Conditional
/-- Two random variables are conditionally independent iff they satisfy the almost sure equality
of conditional expectations `μ⟦f ⁻¹' s ∩ g ⁻¹' t | m'⟧ =ᵐ[μ] μ⟦f ⁻¹' s | m'⟧ * μ⟦g ⁻¹' t | m'⟧`
for all measurable sets `s` and `t` (see `condIndepFun_iff_condExp_inter_preimage_eq_mul`).
Here, this is phrased with Markov kernels associated to the conditional expectations.

For a random variable `f`, `(condExpKernel μ m').map f` is the law of the conditional expectation
of `f` given `m'`: almost surely, `(condExpKernel μ m').map f ω s = μ⟦f ⁻¹' s | m'⟧ ω`.  -/
ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_map_map : ∀ {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {f : Ω → β} {g : Ω → β'}
  {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} [MeasurableSpace.CountableOrCountablyGenerated Ω (β × β')],
  Measurable f →
    Measurable g →
      (ProbabilityTheory.CondIndepFun m' hm' f g μ ↔
        ⇑((ProbabilityTheory.condExpKernel μ m').map fun ω => (f ω, g ω)) =ᵐ[μ.trim hm']
          ⇑(((ProbabilityTheory.condExpKernel μ m').map f).prod ((ProbabilityTheory.condExpKernel μ m').map g)))
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.MorphismProperty.relative_map_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {P : CategoryTheory.MorphismProperty C} [F.Faithful] [F.Full]
  [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F]
  [CategoryTheory.Limits.HasPullbacks C] [P.IsStableUnderBaseChange] {X Y : C} {f : X ⟶ Y},
  CategoryTheory.MorphismProperty.relative F P (F.map f) ↔ P f
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.dist_eq_norm : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (f g : ↥(MeasureTheory.Lp E p μ)), dist f g = ‖-f + g‖
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.Ioo_add_one_right_eq_Ioc : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Add α]
  [SuccAddOrder α] [NoMaxOrder α] (a b : α), Finset.Ioo a (b + 1) = Finset.Ioc a b
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
/-- A function has finite integral for the counting measure iff its enorm has finite `tsum`.  -/
MeasureTheory.hasFiniteIntegral_count_iff_enorm : ∀ {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} [inst : ENorm ε] [MeasurableSingletonClass α] {f : α → ε},
  MeasureTheory.HasFiniteIntegral f MeasureTheory.Measure.count ↔ ∑' (x : α), ‖f x‖ₑ < ⊤
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.phaseNorm : Lean.ParserDescr
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.Triangle.rotate_obj₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C),
  T.rotate.obj₃ = (CategoryTheory.shiftFunctor C 1).obj T.obj₁
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_iff_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, t.contains k = true ↔ k ∈ t
-- Mathlib.Order.CompleteLattice.Basic
biInf_ge_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.LinearAlgebra.TensorProduct.RightExactness
rTensor.inverse_of_rightInverse_comp_rTensor : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P]
  {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [inst_7 : AddCommGroup Q] [inst_8 : Module R Q]
  (hfg : Function.Exact ⇑f ⇑g) {h : P → N} (hgh : Function.RightInverse h ⇑g),
  rTensor.inverse_of_rightInverse Q hfg hgh ∘ₗ LinearMap.rTensor Q g = (LinearMap.rTensor Q f).range.mkQ
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.mapBifunctorLeftUnitor_hasMap : ∀ {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : Zero I] [inst_3 : DecidableEq I]
  [inst_4 : CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C)
  (e : F.obj X ≅ CategoryTheory.Functor.id D)
  [∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)] (p : I × J → J),
  (∀ (j : J), p (0, j) = j) →
    ∀ (Y : CategoryTheory.GradedObject J D),
      (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj
            Y).HasMap
        p
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.Params.anchorRefs? : Lean.Meta.Grind.Params → Option (Array Lean.Meta.Grind.AnchorRef)
-- Mathlib.Analysis.BoxIntegral.UnitPartition
/-- If `B : BoxIntegral.Box` has integral vertices, then `prepartition n B` is a partition of
`B`.  -/
BoxIntegral.unitPartition.prepartition_isPartition : ∀ {ι : Type u_1} (n : ℕ) [inst : NeZero n] [inst_1 : Fintype ι] {B : BoxIntegral.Box ι},
  BoxIntegral.hasIntegralVertices B → (BoxIntegral.unitPartition.prepartition n B).IsPartition
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.instMin.eq_1 : ∀ {R : Type u} {M : Type v} [inst : VAdd R M],
  SubAddAction.instMin = { min := fun s t => { carrier := ↑s ∩ ↑t, vadd_mem' := ⋯ } }
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Option.isSome.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (val : α) (h_1 : (val : α) → motive (some val))
  (h_2 : Unit → motive none),
  (match some val with
    | some val => h_1 val
    | none => h_2 ()) =
    h_1 val
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.filter.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (f f_1 : (a : α) → β a → Bool),
  f = f_1 →
    ∀ (t t_1 : Std.DTreeMap.Internal.Impl α β) (e_t : t = t_1) (hl : t.Balanced),
      Std.DTreeMap.Internal.Impl.filter f t hl = Std.DTreeMap.Internal.Impl.filter f_1 t_1 ⋯