mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- `conflict?` is `some ..` if a contradictory constraint was derived.
This field is only set when `caseSplits` is `true`. Otherwise, we
can convert `UnsatProof` into a Lean term and close the current `grind` goal.
 -/
Lean.Meta.Grind.Arith.Linear.Struct.conflict? : Lean.Meta.Grind.Arith.Linear.Struct → Option Lean.Meta.Grind.Arith.Linear.UnsatProof
-- Aesop.Tree.Data
Aesop.MVarCluster.parent? : Aesop.MVarCluster → Option Aesop.RappRef
-- Init.Data.List.MinMax
List.max_singleton : ∀ {α : Type u_1} [inst : Max α] {x : α}, [x].max ⋯ = x
-- Batteries.Recycling.RBTree.Basic
/-- `O(1)`. Construct a new empty map.  -/
RBTree.mkRBMap : (α : Type u) → (β : Type v) → (cmp : α → α → Ordering) → RBTree.RBMap α β cmp
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.limitCone.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteAddGrp.{max v u}),
  ProfiniteAddGrp.limitCone F =
    {
      pt :=
        ProfiniteAddGrp.ofProfinite
          (Profinite.limitCone (F.comp (CategoryTheory.forget₂ ProfiniteAddGrp.{max u v} Profinite))).pt,
      π :=
        { app := fun j => { hom' := { toFun := fun x => ↑x j, map_zero' := ⋯, map_add' := ⋯, continuous_toFun := ⋯ } },
          naturality := ⋯ } }
-- Mathlib.Order.Filter.Defs
/-- The *kernel* of a filter is the intersection of all its sets.  -/
Filter.ker : {α : Type u_1} → Filter α → Set α
-- Mathlib.LinearAlgebra.Projectivization.Action
Projectivization.generalLinearGroup_smul_def : ∀ {K : Type u_2} {V : Type u_3} [inst : AddCommGroup V] [inst_1 : DivisionRing K] [inst_2 : Module K V]
  (g : LinearMap.GeneralLinearGroup K V) (x : Projectivization K V), g • x = Projectivization.map ↑g.toLinearEquiv ⋯ x
-- Mathlib.LinearAlgebra.DFinsupp
/-- The canonical map out of a direct sum of a family of submodules is injective when the submodules
are `iSupIndep`.

Note that this is not generally true for `[Semiring R]`, for instance when `A` is the
`ℕ`-submodules of the positive and negative integers.

See `Counterexamples/DirectSumIsInternal.lean` for a proof of this fact.  -/
iSupIndep.dfinsupp_lsum_injective : ∀ {ι : Type u_1} {R : Type u_3} {N : Type u_6} [inst : DecidableEq ι] [inst_1 : Ring R] [inst_2 : AddCommGroup N]
  [inst_3 : Module R N] {p : ι → Submodule R N},
  iSupIndep p → Function.Injective ⇑((DFinsupp.lsum ℕ) fun i => (p i).subtype)
-- Mathlib.Algebra.Order.BigOperators.Expect
Finset.expect_lt_expect : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α]
  [inst_3 : Module ℚ≥0 α] [PosSMulStrictMono ℚ≥0 α] {s : Finset ι} {f g : ι → α},
  (∀ i ∈ s, f i ≤ g i) → (∃ i ∈ s, f i < g i) → (s.expect fun i => f i) < s.expect fun i => g i
-- Mathlib.Order.SupClosed
IsLowerSet.infClosed : ∀ {α : Type u_3} [inst : SemilatticeInf α] {s : Set α}, IsLowerSet s → InfClosed s
-- Lean.Meta.Check
/-- Runs `x` and, on any error, lazily checks whether `e` is type-correct at `instances` transparency.
If not, appends an explanatory note to the error message.

This is useful for tactics like `rw` and `simp` whose failure modes can be caused by
prior tactics (such as `unfold`) leaving the goal in a state that's type-correct only at
`.default` transparency, preventing unification etc at `.instances`.
 -/
Lean.Meta.withInstancesTypeCheckNote : {m : Type → Type u_1} → {α : Type} → [MonadControlT Lean.MetaM m] → [Monad m] → Lean.Expr → m α → m α
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- `exprToStructId` content as an array for traversal.  -/
Lean.Meta.Grind.Arith.Linear.State.exprToStructIdEntries : Lean.Meta.Grind.Arith.Linear.State → Lean.PArray (Lean.Expr × ℕ)
-- Mathlib.Algebra.GroupWithZero.ProdHom
MonoidWithZeroHom.fst_comp_inr : ∀ {G₀ : Type u_1} {H₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : GroupWithZero H₀]
  [inst_2 : DecidablePred fun x => x = 0], (MonoidWithZeroHom.fst G₀ H₀).comp (MonoidWithZeroHom.inr G₀ H₀) = 1
-- Mathlib.Combinatorics.SimpleGraph.Partition
/-- The partition where every vertex is in its own part.  -/
SimpleGraph.Partition.instInhabited : {V : Type u} → {G : SimpleGraph V} → Inhabited G.Partition
-- Lean.Meta.Constructions.CtorElim
_private.Lean.Meta.Constructions.CtorElim.0.Lean.mkCtorElimTypeName : Lean.Name → Lean.Name
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.BitVec.not_ite_beq : ∀ {w : ℕ} {a b : BitVec (w + 1)} {c : Bool}, ((~~~bif c then a else b) == a) = (!c && ~~~b == a)
-- Mathlib.Data.Setoid.Basic
Setoid.comap_rel_eq : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (r : Setoid β), ⇑(Setoid.comap f r) = Function.onFun (⇑r) f
-- Mathlib.LinearAlgebra.AnnihilatingPolynomial
/-- `annIdeal R a` is the *annihilating ideal* of all `p : R[X]` such that `p(a) = 0`.

The informal notation `p(a)` stands for `Polynomial.aeval a p`.
Again informally, the annihilating ideal of `a` is
`{ p ∈ R[X] | p(a) = 0 }`. This is an ideal in `R[X]`.
The formal definition uses the kernel of the aeval map.  -/
Polynomial.annIdeal : (R : Type u_1) →
  {A : Type u_2} → [inst : CommSemiring R] → [inst_1 : Semiring A] → [Algebra R A] → A → Ideal (Polynomial R)
-- Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
CategoryTheory.SimplicialObject.Homotopy.h_succ_comp_δ_castSucc_of_lt_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.SimplicialObject C} {f g : X ⟶ Y}
  (self : CategoryTheory.SimplicialObject.Homotopy f g) {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)),
  i ≤ j.castSucc →
    ∀ {Z : C} (h : Y.obj (Opposite.op { len := n + 1 }) ⟶ Z),
      CategoryTheory.CategoryStruct.comp (self.h j.succ) (CategoryTheory.CategoryStruct.comp (Y.δ i.castSucc) h) =
        CategoryTheory.CategoryStruct.comp (X.δ i) (CategoryTheory.CategoryStruct.comp (self.h j) h)
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.Infinite.of_smul_set : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s : Set β} {a : α}, (a • s).Infinite → s.Infinite
-- Mathlib.Data.List.Sublists
List.sublistsLen_succ_cons : ∀ {α : Type u} (n : ℕ) (a : α) (l : List α),
  List.sublistsLen (n + 1) (a :: l) = List.sublistsLen (n + 1) l ++ List.map (List.cons a) (List.sublistsLen n l)
-- Mathlib.Combinatorics.Matroid.Circuit
/-- **Alias** of `Matroid.isCircuit_iff_dep_forall_sdiff_singleton_indep`. -/
Matroid.isCircuit_iff_dep_forall_diff_singleton_indep : ∀ {α : Type u_1} {M : Matroid α} {C : Set α}, M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e})
-- Mathlib.Algebra.Category.Ring.Basic
CommSemiRingCat.ofHom_id : ∀ {R : Type u} [inst : CommSemiring R],
  CommSemiRingCat.ofHom (RingHom.id R) = CategoryTheory.CategoryStruct.id (CommSemiRingCat.of R)
-- Mathlib.Tactic.ProxyType
Mathlib.ProxyType.ProxyEquivConfig.mk.sizeOf_spec : ∀ (proxyName proxyEquivName : Lean.Name)
  (mkCtorProxyType : List (Lean.Expr × Lean.Name) → Lean.Elab.TermElabM (Lean.Expr × Lean.Term))
  (mkProxyType :
    Array (Lean.Name × Lean.Expr × Lean.Term) →
      Lean.Elab.TermElabM (Lean.Expr × Array Lean.Term × Lean.TSyntax `tactic)),
  sizeOf
      { proxyName := proxyName, proxyEquivName := proxyEquivName, mkCtorProxyType := mkCtorProxyType,
        mkProxyType := mkProxyType } =
    1 + sizeOf proxyName + sizeOf proxyEquivName
-- Mathlib.Data.Vector.Defs
/-- The head of a vector obtained by prepending is the element prepended.  -/
List.Vector.head_cons : ∀ {α : Type u_1} {n : ℕ} (a : α) (v : List.Vector α n), (a ::ᵥ v).head = a
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_insert_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  (t.insert k v).getKey? k = some k
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Structure.CG.out : ∀ {L : FirstOrder.Language} {M : Type u_1} {inst : L.Structure M} [self : FirstOrder.Language.Structure.CG L M], ⊤.CG
-- Std.Sync.RecursiveMutex
_private.Std.Sync.RecursiveMutex.0.Std.RecursiveMutex.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (ref : IO.Ref α) (mutex : Std.BaseRecursiveMutex),
  sizeOf { ref := ref, mutex := mutex } = 1 + sizeOf ref + sizeOf mutex
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Finset.card_truncatedSup_union_add_card_truncatedSup_infs : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (𝒜 ℬ : Finset (Finset α)) (s : Finset α),
  ((𝒜 ∪ ℬ).truncatedSup s).card + ((𝒜 ⊼ ℬ).truncatedSup s).card = (𝒜.truncatedSup s).card + (ℬ.truncatedSup s).card
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
nullMeasurableSet_Ioc : ∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : LinearOrder α]
  {a b : α} {μ : MeasureTheory.Measure α} [ClosedIicTopology α], MeasureTheory.NullMeasurableSet (Set.Ioc a b) μ
-- Std.Time.Date.Unit.Week
/-- Convert `Week.Offset` into `Millisecond.Offset`.
 -/
Std.Time.Week.Offset.toMilliseconds : Std.Time.Week.Offset → Std.Time.Millisecond.Offset
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.maxKey!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.maxKey! = t₂.maxKey!
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_conjTranspose : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : InvolutiveStar α] (M : Matrix m n α),
  M.conjTranspose.conjTranspose = M
-- Mathlib.Analysis.Convex.Strong
/-- A function `f` from a real normed space is `m`-strongly convex if it is uniformly convex with
modulus `φ(r) = m / 2 * r ^ 2`.

In an inner product space, this is equivalent to `x ↦ f x - m / 2 * ‖x‖ ^ 2` being convex.  -/
StrongConvexOn : {E : Type u_1} → [inst : NormedAddCommGroup E] → [NormedSpace ℝ E] → Set E → ℝ → (E → ℝ) → Prop
-- Mathlib.Analysis.Convex.Star
starConvex_iff_ordConnected : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {x : 𝕜} {s : Set 𝕜},
  x ∈ s → (StarConvex 𝕜 x s ↔ s.OrdConnected)
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.isOrthogonal_comm : ∀ {ι : 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] (P : RootPairing ι R M N) (i j : ι),
  P.IsOrthogonal i j → Commute (P.reflection i) (P.reflection j)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.π_descH : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) {A : C} (k : h.K ⟶ A)
  (hk : CategoryTheory.CategoryStruct.comp h.f' k = 0), CategoryTheory.CategoryStruct.comp h.π (h.descH k hk) = k
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.closure_closure_coe_preimage : ∀ {M : Type u_1} [inst : Add M] {s : Set M}, AddSubsemigroup.closure (Subtype.val ⁻¹' s) = ⊤
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.mk_apply : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring 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} {e : V ≃ₗ[A] W} (he : ∀ (g : G), ↑e ∘ₗ ρ g = σ g ∘ₗ ↑e) (v : V),
  (Representation.Equiv.mk e he) v = e v
-- Mathlib.RingTheory.Algebraic.Basic
/-- A special case of `IsAlgebraic.extendScalars`. This is extracted as a theorem
because in some cases `IsAlgebraic.extendScalars` will just runs out of memory.  -/
IsAlgebraic.tower_top_of_subalgebra_le : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {A B : Subalgebra R S},
  A ≤ B → ∀ {x : S}, IsAlgebraic (↥A) x → IsAlgebraic (↥B) x
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
AhlswedeZhang.infSum_union_add_infSum_sups : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (𝒜 ℬ : Finset (Finset α)),
  AhlswedeZhang.infSum (𝒜 ∪ ℬ) + AhlswedeZhang.infSum (𝒜 ⊻ ℬ) = AhlswedeZhang.infSum 𝒜 + AhlswedeZhang.infSum ℬ
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ Dᵒᵖ` preserves finite products, then `F.leftOp : Cᵒᵖ ⥤ D` preserves finite
coproducts.  -/
CategoryTheory.Limits.preservesFiniteCoproducts_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesFiniteProducts F],
  CategoryTheory.Limits.PreservesFiniteCoproducts F.leftOp
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vsub_mem_vsub : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] [inst_1 : DecidableEq α] {s t : Finset β} {b c : β},
  b ∈ s → c ∈ t → b -ᵥ c ∈ s -ᵥ t
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.Fork.isLimitOfιEquivIsColimitUnop.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y P : Cᵒᵖ} {f g : X ⟶ Y} (ι ι' : P ⟶ X)
  (w : CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g)
  (w' : CategoryTheory.CategoryStruct.comp f.unop ι'.unop = CategoryTheory.CategoryStruct.comp g.unop ι'.unop)
  (h : ι = ι'),
  CategoryTheory.Limits.Fork.isLimitOfιEquivIsColimitUnop ι ι' w w' h =
    CategoryTheory.Limits.Fork.isLimitOfιEquivIsColimitUnop ι ι' w w' h
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.IrreducibleCloseds.mk.congr_simp : ∀ {α : Type u_4} [inst : TopologicalSpace α] (carrier carrier_1 : Set α) (e_carrier : carrier = carrier_1)
  (isIrreducible' : IsIrreducible carrier) (isClosed' : IsClosed carrier),
  { carrier := carrier, isIrreducible' := isIrreducible', isClosed' := isClosed' } =
    { carrier := carrier_1, isIrreducible' := ⋯, isClosed' := ⋯ }
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_pi_div_sixteen : Real.cos (Real.pi / 16) = √(2 + √(2 + √2)) / 2
-- Mathlib.Topology.GDelta.Basic
isMeagre_biUnion : ∀ {X : Type u_1} {ι : Type u_3} [inst : TopologicalSpace X] {I : Set ι},
  I.Countable → ∀ {f : ι → Set X}, (∀ i ∈ I, IsMeagre (f i)) → IsMeagre (⋃ i ∈ I, f i)
-- Mathlib.Order.Filter.Basic
/-- There are only two filters on a `Subsingleton`: `⊥` and `⊤`. If the type is empty, then they are
equal.  -/
Filter.eq_top_of_neBot : ∀ {α : Type u} [Subsingleton α] (l : Filter α) [l.NeBot], l = ⊤
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- Let `L / K` be a field extension. If `x` is a separable element over `K` and the minimal polynomial
of `x` splits in `L`, then `x` is not in `K` if and only if there exists a conjugate
root of `x` over `K` in `L` which is not equal to `x` itself.
 -/
notMem_iff_exists_ne_and_isConjRoot : ∀ {K : Type u_2} {L : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {x : L},
  IsSeparable K x → (Polynomial.map (algebraMap K L) (minpoly K x)).Splits → (x ∉ ⊥ ↔ ∃ y, x ≠ y ∧ IsConjRoot K x y)
-- Mathlib.Util.Notation3
/-- `notation3` argument binding a name.  -/
Mathlib.Notation3.identOptScoped : Lean.ParserDescr
-- Mathlib.Algebra.Lie.Extension
/-- The 1-cochain attached to a pair of splittings of an extension.  -/
LieAlgebra.Extension.oneCochainOfTwoSplitting : {R : Type u_1} →
  {L : Type u_3} →
    {M : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : LieRing M] →
              [inst_4 : LieAlgebra R M] →
                (E : LieAlgebra.Extension R M L) →
                  {s₁ s₂ : L →ₗ[R] E.L} →
                    Function.LeftInverse ⇑E.proj ⇑s₁ →
                      Function.LeftInverse ⇑E.proj ⇑s₂ → LieModule.Cohomology.oneCochain R L M
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- `G.labelledCopyCount H` is the number of labelled copies of `H` in `G`, i.e. the number of graph
embeddings from `H` to `G`. See `SimpleGraph.copyCount` for the number of unlabelled copies.  -/
SimpleGraph.labelledCopyCount : {V : Type u_1} → {W : Type u_2} → [Fintype V] → [Fintype W] → SimpleGraph V → SimpleGraph W → ℕ
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.liftOn₂_mk' : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {p : Sort u_4} (f : M → ↥S → M → ↥S → p)
  (H :
    ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S},
      (AddLocalization.r S) (a, b) (a', b') → (AddLocalization.r S) (c, d) (c', d') → f a b c d = f a' b' c' d')
  (a c : M) (b d : ↥S),
  ((AddLocalization.addMonoidOf S).mk' a b).liftOn₂ ((AddLocalization.addMonoidOf S).mk' c d) f H = f a b c d
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- Let `sᵢ` and `tᵢ` be families of `R`-modules.
Then there is an `R`-linear map between `⨂ᵢ Hom(sᵢ, tᵢ)` and `Hom(⨂ᵢ sᵢ, ⨂ tᵢ)` defined by
`⨂ᵢ fᵢ ↦ ⨂ᵢ aᵢ ↦ ⨂ᵢ fᵢ aᵢ`.

This is `TensorProduct.homTensorHomMap` for an arbitrary family of modules.

Note that `PiTensorProduct.piTensorHomMap (tprod R f)` is equal to `PiTensorProduct.map f`.
 -/
PiTensorProduct.piTensorHomMap : {ι : Type u_1} →
  {R : Type u_4} →
    [inst : CommSemiring R] →
      {s : ι → Type u_7} →
        [inst_1 : (i : ι) → AddCommMonoid (s i)] →
          [inst_2 : (i : ι) → Module R (s i)] →
            {t : ι → Type u_11} →
              [inst_3 : (i : ι) → AddCommMonoid (t i)] →
                [inst_4 : (i : ι) → Module R (t i)] →
                  (PiTensorProduct R fun i => s i →ₗ[R] t i) →ₗ[R]
                    (PiTensorProduct R fun i => s i) →ₗ[R] PiTensorProduct R fun i => t i
-- Std.Time.Time.PlainTime
Std.Time.instLawfulEqOrdPlainTime : Std.LawfulEqOrd Std.Time.PlainTime
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.monotoneOn_or_antitoneOn_iff_uIcc : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β} {s : Set α},
  MonotoneOn f s ∨ AntitoneOn f s ↔ ∀ a ∈ s, ∀ b ∈ s, ∀ c ∈ s, c ∈ Set.uIcc a b → f c ∈ Set.uIcc (f a) (f b)
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.id_apex : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Wₗ Wᵣ : CategoryTheory.MorphismProperty C}
  [inst_1 : Wₗ.ContainsIdentities] [inst_2 : Wᵣ.ContainsIdentities] (c : C), (CategoryTheory.Span.id c).apex = c
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.Colorable.of_sum_left : ∀ {V : Type u_3} {W : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W} {n : ℕ}, (G ⊕g H).Colorable n → G.Colorable n
-- Mathlib.Analysis.SpecialFunctions.SmoothTransition
Real.smoothTransition.continuousAt : ∀ {x : ℝ}, ContinuousAt Real.smoothTransition x
-- Batteries.Data.List.Basic
List.forDiagM.eq_def : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} [inst : Monad m] (f : α → α → m PUnit.{u_1 + 1}) (x : List α),
  List.forDiagM f x =
    match x with
    | [] => pure PUnit.unit
    | x :: xs => do
      f x x
      xs.forM (f x)
      List.forDiagM f xs
-- Mathlib.MeasureTheory.Integral.Prod
/-- Integrals commute with addition inside another integral. `F` can be any function.  -/
MeasureTheory.integral_fn_integral_add : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  [inst_4 : NormedSpace ℝ E] [MeasureTheory.SFinite μ] {E' : Type u_4} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace ℝ E'] ⦃f g : α × β → E⦄ (F : E → E'),
  MeasureTheory.Integrable f (μ.prod ν) →
    MeasureTheory.Integrable g (μ.prod ν) →
      ∫ (x : α), F (∫ (y : β), f (x, y) + g (x, y) ∂ν) ∂μ =
        ∫ (x : α), F (∫ (y : β), f (x, y) ∂ν + ∫ (y : β), g (x, y) ∂ν) ∂μ
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
/-- Integration by parts of Schwartz functions for directional derivatives.

Version for a general bilinear map.  -/
SchwartzMap.integral_bilinear_lineDerivOp_right_eq_neg_left : ∀ {D : Type u_4} {E : Type u_5} {V : Type u_7} {F : Type u_8} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F] [inst_3 : NormedSpace ℝ E] [inst_4 : NormedAddCommGroup V]
  [inst_5 : NormedSpace ℝ V] [inst_6 : NormedAddCommGroup D] [inst_7 : NormedSpace ℝ D] [inst_8 : MeasurableSpace D]
  {μ : MeasureTheory.Measure D} [BorelSpace D] [FiniteDimensional ℝ D] [μ.IsAddHaarMeasure] (f : SchwartzMap D E)
  (g : SchwartzMap D F) (L : E →L[ℝ] F →L[ℝ] V) (v : D),
  ∫ (x : D), (L (f x)) ((LineDeriv.lineDerivOp v g) x) ∂μ = -∫ (x : D), (L ((LineDeriv.lineDerivOp v f) x)) (g x) ∂μ
-- Std.Data.DHashMap.Basic
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise panics.
If no panic occurs the result is guaranteed to be pointer equal to the key in the map.
 -/
Std.DHashMap.getKey! : {α : Type u} → {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → [Inhabited α] → Std.DHashMap α β → α → α
-- Mathlib.Topology.Algebra.Monoid
SeparatelyContinuousAdd.to_continuousVAdd : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Add M] [SeparatelyContinuousAdd M], ContinuousConstVAdd M M
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.toNontrivial : ∀ {α : Type u_3} [self : LinearOrderedAddCommGroupWithTop α], Nontrivial α
-- Lean.Meta.Tactic.Grind.Action
Lean.Meta.Grind.Action.instOrElse : OrElse Lean.Meta.Grind.Action
-- Mathlib.Data.Finset.Sort
Finset.orderEmbOfFin_compl_singleton_apply : ∀ {n : ℕ} {i : Fin (n + 1)} {k : ℕ} (h : {i}ᶜ.card = k) (j : Fin k),
  ({i}ᶜ.orderEmbOfFin h) j = i.succAbove (Fin.cast ⋯ j)
-- Mathlib.GroupTheory.Congruence.Defs
Con.instMembershipProd.eq_1 : ∀ {M : Type u_1} [inst : Mul M], Con.instMembershipProd = { mem := fun c x => c x.1 x.2 }
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.ordCompare_maxKey!_modify_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] {t : Std.DTreeMap.Raw α (fun x => β) compare}
  [inst_2 : Inhabited α],
  t.WF → ∀ {k : α} {f : β → β}, compare (Std.DTreeMap.Raw.Const.modify t k f).maxKey! t.maxKey! = Ordering.eq
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.yonedaEquiv_symm_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ⟶ Y)
  {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (t : F.obj X),
  CategoryTheory.yonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (F.map f)) t) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f.unop) (CategoryTheory.yonedaEquiv.symm t)
-- Mathlib.InformationTheory.Hamming
Hamming.nndist_eq_hammingDist : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)] (x y : Hamming β),
  nndist x y = ↑(hammingDist (Hamming.ofHamming x) (Hamming.ofHamming y))
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.instOrderIsoClass : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β],
  OrderIsoClass (α ≃*o β) α β
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey?_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.filter f m).getKey? k = (m.getKey? k).pfilter fun x_2 h' => f x_2 (Std.DHashMap.Const.get m x_2 ⋯)
-- Mathlib.MeasureTheory.Group.Measure
/-- A Haar measure on a σ-compact space is σ-finite.

See Note [lower instance priority]  -/
MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalSpace G]
  (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [SigmaCompactSpace G], MeasureTheory.SigmaFinite μ
-- Mathlib.Topology.MetricSpace.Gluing
/-- The map `toInductiveLimit n` mapping `X n` to the inductive limit is an isometry.  -/
Metric.toInductiveLimit_isometry : ∀ {X : ℕ → Type u} [inst : (n : ℕ) → MetricSpace (X n)] {f : (n : ℕ) → X n → X (n + 1)} (I : ∀ (n : ℕ), Isometry (f n))
  (n : ℕ), Isometry (Metric.toInductiveLimit I n)
-- Mathlib.Algebra.Homology.Homotopy
_private.Mathlib.Algebra.Homology.Homotopy.0.Homotopy.mkInductiveAux₁.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (n : ℕ) → motive n.succ.succ),
  (match 0 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | n.succ.succ => h_3 n) =
    h_1 ()