mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.presentation_relation : ∀ (R : Type u) [inst : CommRing R] (n : ℕ) (M : Type u_1) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (x : exteriorPower.presentation.Rels R (Fin n) M),
  (exteriorPower.presentation R n M).relation x =
    match x with
    | exteriorPower.presentation.Rels.add m i x y =>
      ((fun₀ | Function.update m i x => 1) + fun₀ | Function.update m i y => 1) -
        fun₀ | Function.update m i (x + y) => 1
    | exteriorPower.presentation.Rels.smul m i r x =>
      (fun₀ | Function.update m i (r • x) => 1) - fun₀ | Function.update m i x => r
    | exteriorPower.presentation.Rels.alt m i j hm hij => fun₀ | m => 1
-- Mathlib.Order.Hom.Set
/-- An order isomorphism between lattices induces an order isomorphism between corresponding
interval sublattices.  -/
OrderIso.Ici : {α : Type u_1} →
  {β : Type u_2} → [inst : Lattice α] → [inst_1 : Lattice β] → (e : α ≃o β) → (x : α) → ↑(Set.Ici x) ≃o ↑(Set.Ici (e x))
-- Batteries.Recycling.RBTree.Lemmas
/-- A stronger version of `lowerBoundP?_greatest` that holds when the cut is strict.  -/
RBTree.RBSet.lowerBoundP?_lt : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {x y : α} {t : RBTree.RBSet α cmp} [Std.TransCmp cmp]
  [RBTree.RBNode.IsStrictCut cmp cut],
  t.lowerBoundP? cut = some x → y ∈ t → (cmp x y = Ordering.lt ↔ cut y = Ordering.lt)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- A morphism of pre-`1`-hypercovers of `S` is a family of refinement morphisms commuting
with the structure morphisms of `E` and `F`.  -/
CategoryTheory.PreOneHypercover.Hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} → CategoryTheory.PreOneHypercover S → CategoryTheory.PreOneHypercover S → Type (max (max u_2 u_3) v)
-- Mathlib.Data.Nat.Nth
Nat.nth_monotone : ∀ {p : ℕ → Prop}, (Set.ofPred p).Infinite → Monotone (Nat.nth p)
-- Mathlib.Topology.Algebra.Group.GroupTopology
GroupTopology.toTopologicalSpace_le : ∀ {α : Type u} [inst : Group α] {x y : GroupTopology α}, x.toTopologicalSpace ≤ y.toTopologicalSpace ↔ x ≤ y
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.whiskerRight_app : ∀ {C D E : CategoryTheory.Cat} {F G : C ⟶ D} (H : D ⟶ E) (η : F ⟶ G) (X : ↑C),
  (CategoryTheory.Bicategory.whiskerRight η H).toNatTrans.app X = H.toFunctor.map (η.toNatTrans.app X)
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.Reachable.exists_walk_length_eq_dist : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, G.Reachable u v → ∃ p, p.length = G.dist u v
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.notMem_compl : ∀ {α : Type u_1} {s : Finset α} [inst : Fintype α] [inst_1 : DecidableEq α] {a : α}, a ∉ sᶜ ↔ a ∈ s
-- Mathlib.Topology.Sheaves.Abelian
TopCat.Sheaf.instIsGrothendieckAbelian : ∀ {X : TopCat} {D : Type u_1} [inst : CategoryTheory.Category.{u, u_1} D] [inst_1 : CategoryTheory.Abelian D]
  [CategoryTheory.IsGrothendieckAbelian.{u, u, u_1} D]
  [inst_3 : CategoryTheory.HasSheafify (Opens.grothendieckTopology ↑X) D],
  CategoryTheory.IsGrothendieckAbelian.{u, u, max u_1 u} (TopCat.Sheaf D X)
-- Mathlib.SetTheory.Cardinal.Finite
ENat.card_lt_top : ∀ {α : Type u_1}, ENat.card α < ⊤ ↔ Finite α
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.mem_of_mem_of_le : ∀ {α : Type u} {r : Std.Roo α} [inst : LT α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [Std.Rxo.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {a b : α},
  Std.PRange.UpwardEnumerable.LE r.lower b → (a ∈ b<...r.upper) → a ∈ r
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.move.injEq : ∀ (p : Turing.PartrecToTM2.Γ' → Bool) (k₁ k₂ : Turing.PartrecToTM2.K') (q : Turing.PartrecToTM2.Λ')
  (p_1 : Turing.PartrecToTM2.Γ' → Bool) (k₁_1 k₂_1 : Turing.PartrecToTM2.K') (q_1 : Turing.PartrecToTM2.Λ'),
  (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q = Turing.PartrecToTM2.Λ'.move p_1 k₁_1 k₂_1 q_1) =
    (p = p_1 ∧ k₁ = k₁_1 ∧ k₂ = k₂_1 ∧ q = q_1)
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.smul_right_def : ∀ {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] {R : Type u_3} {T : Type u_4} [inst_2 : Semiring R]
  (v : AbsoluteValue R S) [inst_3 : SMul T R] (t : T) (x : WithAbs v), t • x = WithAbs.toAbs v (t • x.ofAbs)
-- Mathlib.Order.Basic
not_lt_iff_le_imp_ge : ∀ {α : Type u_2} [inst : Preorder α] {a b : α}, ¬a < b ↔ a ≤ b → b ≤ a
-- Mathlib.Algebra.Homology.HomologicalBicomplex
HomologicalComplex₂.flipEquivalenceCounitIso_inv_app_f_f : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (X : HomologicalComplex₂ C c₂ c₁)
  (i : I₂) (i_1 : I₁),
  (((HomologicalComplex₂.flipEquivalenceCounitIso C c₁ c₂).inv.app X).f i).f i_1 =
    CategoryTheory.CategoryStruct.id ((X.X i).X i_1)
-- Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
CochainComplex.mappingConeCompTriangle_obj₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃),
  (CochainComplex.mappingConeCompTriangle f g).obj₂ =
    CochainComplex.mappingCone (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.CategoryTheory.Filtered.Final
/-- `StructuredArrow.post X T S` is final if `T` and `S` are final and the domain of `T` is
filtered.  -/
CategoryTheory.StructuredArrow.final_post : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.IsFiltered C] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E] (X : D)
  (T : CategoryTheory.Functor C D) [T.Final] (S : CategoryTheory.Functor D E) [S.Final],
  (CategoryTheory.StructuredArrow.post X T S).Final
-- Lean.Data.Json.Elab
/-- Json key/value syntax.  -/
Lean.Json.jsonField : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullbackFstFstIso.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X Y S X' Y' S' : C} (f : X ⟶ S) (g : Y ⟶ S) (f' : X' ⟶ S') (g' : Y' ⟶ S') (i₁ : X ⟶ X') (i₂ : Y ⟶ Y')
  (i₃ i₃_1 : S ⟶ S') (e_i₃ : i₃ = i₃_1)
  (e₁ : CategoryTheory.CategoryStruct.comp f i₃ = CategoryTheory.CategoryStruct.comp i₁ f')
  (e₂ : CategoryTheory.CategoryStruct.comp g i₃ = CategoryTheory.CategoryStruct.comp i₂ g')
  [inst_2 : CategoryTheory.Mono i₃],
  CategoryTheory.Limits.pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂ =
    CategoryTheory.Limits.pullbackFstFstIso f g f' g' i₁ i₂ i₃_1 ⋯ ⋯
-- Init.Data.String.Hashable
String.instHashablePos_1.hash : {s : String.Slice} → s.Pos → UInt64
-- Lean.Parser.Command
Lean.Parser.Command.evalBang.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.LocalRing.Module
Module.mem_support_iff_nontrivial_residueField_tensorProduct : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Finite R M]
  (p : PrimeSpectrum R), p ∈ Module.support R M ↔ Nontrivial (TensorProduct R p.asIdeal.ResidueField M)
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- Given a quadratic map `Q` and a basis, `basisRepr` is the basis representation of `Q`.  -/
QuadraticMap.basisRepr : {R : Type u_3} →
  {M : Type u_4} →
    {N : Type u_5} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] →
                {ι : Type u_8} → [Finite ι] → QuadraticMap R M N → Module.Basis ι R M → QuadraticMap R (ι → R) N
-- Std.Sync.StreamMap
/-- Get the number of registered streams
 -/
Std.StreamMap.size : {α β : Type} → Std.StreamMap α β → ℕ
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt8.reduceOfNat : Lean.Meta.Simp.DSimproc
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getD_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} {fallback : β k}, k ∉ t₁ → (t₁ ∩ t₂).getD k fallback = fallback
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_maxKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {he : l.isEmpty = false},
  Std.Internal.List.getKey (Std.Internal.List.maxKey l he) l ⋯ = Std.Internal.List.maxKey l he
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
/-- *Fundamental Theorem of Calculus* for absolutely continuous functions: if `f` is absolutely
continuous on `uIcc a b`, then `∫ (x : ℝ) in a..b, deriv f x = f b - f a`.  -/
AbsolutelyContinuousOnInterval.integral_deriv_eq_sub : ∀ {f : ℝ → ℝ} {a b : ℝ}, AbsolutelyContinuousOnInterval f a b → ∫ (x : ℝ) in a..b, deriv f x = f b - f a
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.evaln.eq_def : ∀ (x : ℕ) (x_1 : Nat.Partrec.Code),
  Nat.Partrec.Code.evaln x x_1 =
    match (motive := ℕ → Nat.Partrec.Code → ℕ → Option ℕ) x, x_1 with
    | 0, x => fun x => none
    | k.succ, Nat.Partrec.Code.zero => fun n => do
      guard (n ≤ k)
      pure 0
    | k.succ, Nat.Partrec.Code.succ => fun n => do
      guard (n ≤ k)
      pure n.succ
    | k.succ, Nat.Partrec.Code.left => fun n => do
      guard (n ≤ k)
      pure (Nat.unpair n).1
    | k.succ, Nat.Partrec.Code.right => fun n => do
      guard (n ≤ k)
      pure (Nat.unpair n).2
    | k.succ, cf.pair cg => fun n => do
      guard (n ≤ k)
      Nat.pair <$> Nat.Partrec.Code.evaln (k + 1) cf n <*> Nat.Partrec.Code.evaln (k + 1) cg n
    | k.succ, cf.comp cg => fun n => do
      guard (n ≤ k)
      let x ← Nat.Partrec.Code.evaln (k + 1) cg n
      Nat.Partrec.Code.evaln (k + 1) cf x
    | k.succ, cf.prec cg => fun n => do
      guard (n ≤ k)
      Nat.unpaired
          (fun a n =>
            Nat.casesOn n (Nat.Partrec.Code.evaln (k + 1) cf a) fun y => do
              let i ← Nat.Partrec.Code.evaln k (cf.prec cg) (Nat.pair a y)
              Nat.Partrec.Code.evaln (k + 1) cg (Nat.pair a (Nat.pair y i)))
          n
    | k.succ, cf.rfind' => fun n => do
      guard (n ≤ k)
      Nat.unpaired
          (fun a m => do
            let x ← Nat.Partrec.Code.evaln (k + 1) cf (Nat.pair a m)
            if x = 0 then pure m else Nat.Partrec.Code.evaln k cf.rfind' (Nat.pair a (m + 1)))
          n
-- Aesop.Search.ExpandSafePrefix
_private.Aesop.Search.ExpandSafePrefix.0.Aesop.Goal.isSafeExpanded : Aesop.Goal → BaseIO Bool
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.continuousOn : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), ContinuousOn (↑e) e.source
-- Mathlib.Analysis.Normed.Ring.Basic
/-- An injective non-unital ring homomorphism from a `NonUnitalRing` to a
`NonUnitalNormedRing` induces a `NonUnitalNormedRing` structure on the domain.

See note [reducible non-instances]  -/
NonUnitalNormedRing.induced : {F : Type u_5} →
  (R : Type u_6) →
    (S : Type u_7) →
      [inst : FunLike F R S] →
        [inst_1 : NonUnitalRing R] →
          [inst_2 : NonUnitalNormedRing S] →
            [NonUnitalRingHomClass F R S] → (f : F) → Function.Injective ⇑f → NonUnitalNormedRing R
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Path.Ordered.del : ∀ {α : Type u_1} {cmp : α → α → Ordering} {path : RBTree.RBNode.Path α} {t : RBTree.RBNode α} {c : RBTree.RBColor},
  RBTree.RBNode.Ordered cmp t →
    RBTree.RBNode.Path.Ordered cmp path →
      RBTree.RBNode.All (RBTree.RBNode.Path.RootOrdered cmp path) t → RBTree.RBNode.Ordered cmp (path.del t c)
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.isBlock_top : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] {B : Set X},
  AddAction.IsBlock (↥⊤) B ↔ AddAction.IsBlock G B
-- Mathlib.Order.Monotone.Monovary
Subsingleton.monovaryOn : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [Subsingleton ι] (f : ι → α)
  (g : ι → β) (s : Set ι), MonovaryOn f g s
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
tangentMap_proj : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {p : TangentBundle I M},
  (tangentMap I I' f p).proj = f p.proj
-- Mathlib.Order.Max
Prod.isTop_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β}, IsTop x ↔ IsTop x.1 ∧ IsTop x.2
-- Init.Data.List.Lex
List.not_cons_lex_cons_iff : ∀ {α : Type u_1} {r : α → α → Prop} [DecidableEq α] [DecidableRel r] {a b : α} {l₁ l₂ : List α},
  ¬List.Lex r (a :: l₁) (b :: l₂) ↔ ¬r a b ∧ a ≠ b ∨ ¬r a b ∧ ¬List.Lex r l₁ l₂
-- Mathlib.Algebra.Group.Action.Units
Units.smulCommClass_right : ∀ {M : Type u_3} {N : Type u_4} {α : Type u_5} [inst : Monoid N] [inst_1 : SMul M α] [inst_2 : SMul N α]
  [SMulCommClass M N α], SMulCommClass M Nˣ α
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.sub_iInter₂_subset : ∀ {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : Sub α] (s : Set α) (t : (i : ι) → κ i → Set α),
  s - ⋂ i, ⋂ j, t i j ⊆ ⋂ i, ⋂ j, s - t i j
-- Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
OrderDual.addLeftReflectLT : ∀ {α : Type u} [inst : LT α] [inst_1 : Add α] [c : AddLeftReflectLT α], AddLeftReflectLT αᵒᵈ
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
/-- A `Prop` asserting that two submodules `N₁, N₂` satisfy `N₁ ≤ N₂` and
`N₂ / N₁` is isomorphic to `A / p` for some prime ideal `p` of `A`.  -/
Submodule.IsQuotientEquivQuotientPrime : {A : Type u} →
  [inst : CommRing A] →
    {M : Type v} → [inst_1 : AddCommGroup M] → [inst_2 : Module A M] → Submodule A M → Submodule A M → Prop
-- Lean.Server.Completion.SyntheticCompletion
_private.Lean.Server.Completion.SyntheticCompletion.0.Lean.Server.Completion.findBest?.choose : {α : Type} →
  (α → α → Bool) →
    (Lean.Elab.ContextInfo → Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → Option α) →
      Lean.Elab.ContextInfo →
        Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → List (Option (Option α)) → Option α
-- Mathlib.CategoryTheory.RegularCategory.Basic
/-- In a regular category, every morphism `f` factors as `e ≫ m`, with `e` a strong epimorphism
and `m` a monomorphism.
 -/
CategoryTheory.Regular.hasStrongEpiMonoFactorisations : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Regular C],
  CategoryTheory.Limits.HasStrongEpiMonoFactorisations C
-- Init.Data.BitVec.Lemmas
/-- `x.toInt` is less than `2^(w-1)`.
We phrase the fact in terms of `2^w` to prevent a case split on `w=0` when the lemma is used.
 -/
BitVec.two_mul_toInt_lt : ∀ {w : ℕ} {x : BitVec w}, 2 * x.toInt < 2 ^ w
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBiproductData.mk : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} →
        (bicone : CategoryTheory.Limits.BinaryBicone P Q) →
          bicone.IsBilimit → CategoryTheory.Limits.BinaryBiproductData P Q
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.isUnit : ∀ {M : Type u_1} [inst : Monoid M] {a b : M}, Associated a b → IsUnit a → IsUnit b
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.yonedaGrp.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.yonedaGrp =
    { obj := fun G => CategoryTheory.yonedaGrpObj G.X,
      map := fun {G H} ψ =>
        { app := fun Y => GrpCat.ofHom (MonCat.Hom.hom ((CategoryTheory.yonedaMon.map ψ.hom).app Y)), naturality := ⋯ },
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.RingTheory.RingInvo
RingInvo.instRingInvoClass : ∀ {R : Type u_2} [inst : Semiring R], RingInvoClass (RingInvo R) R
-- Std.Data.DTreeMap.Internal.Model
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getEntryGT?ₘ : {α : Type u} → {β : α → Type v} → [Ord α] → α → Std.DTreeMap.Internal.Impl α β → Option ((a : α) × β a)
-- Mathlib.Analysis.MellinTransform
mellin_comp_mul_right : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℝ → E) (s : ℂ) {a : ℝ},
  0 < a → mellin (fun t => f (t * a)) s = ↑a ^ (-s) • mellin f s
-- Init.Data.List.Basic
List.filterTR.eq_1 : ∀ {α : Type u} (p : α → Bool) (as : List α), List.filterTR p as = List.filterTR.loop p as []
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.diag_μ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C),
  CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Functor.diag C) X Y =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.Functor.diag C).obj X)
        ((CategoryTheory.Functor.diag C).obj Y))
-- Mathlib.Data.Nat.Factorization.Basic
Nat.Ico_pow_dvd_eq_Ico_of_lt : ∀ {n p b : ℕ}, Nat.Prime p → n ≠ 0 → n < p ^ b → {i ∈ Finset.Ico 1 n | p ^ i ∣ n} = {i ∈ Finset.Ico 1 b | p ^ i ∣ n}
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
MonoidAlgebra.rTensorEquiv_symm_singleAlgEquiv : ∀ {R : Type u_1} {M : Type u_2} {S : Type u_4} {A : Type u_5} {B : Type u_6} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : CommSemiring A] [inst_3 : CommSemiring B] [inst_4 : Algebra R S]
  [inst_5 : Algebra R A] [inst_6 : Algebra R B] [inst_7 : Algebra S A] [inst_8 : IsScalarTower R S A]
  [inst_9 : CommMonoid M] (m : M) (a : A) (b : B),
  (MonoidAlgebra.rTensorEquivAlgEquiv R S A B).symm (MonoidAlgebra.single m (a ⊗ₜ[R] b)) =
    a ⊗ₜ[R] MonoidAlgebra.single m b
-- Init.Data.Nat.Lcm
Nat.lcm_one_left : ∀ (m : ℕ), Nat.lcm 1 m = m
-- Lean.Meta.Basic
Lean.Meta.SavedState.mk.inj : ∀ {core : Lean.Core.SavedState} {«meta» : Lean.Meta.State} {core_1 : Lean.Core.SavedState} {meta_1 : Lean.Meta.State},
  { core := core, «meta» := «meta» } = { core := core_1, «meta» := meta_1 } → core = core_1 ∧ «meta» = meta_1
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Problem.mk.injEq : ∀ (assumptions : Array Lean.Elab.Tactic.Omega.Proof) (numVars : ℕ)
  (constraints : Std.HashMap Lean.Omega.Coeffs Lean.Elab.Tactic.Omega.Fact) (equalities : Std.HashSet Lean.Omega.Coeffs)
  (eliminations : List (Lean.Elab.Tactic.Omega.Fact × ℕ × ℤ)) (possible : Bool)
  (proveFalse? : Option Lean.Elab.Tactic.Omega.Proof)
  (proveFalse?_spec :
    autoParam ((possible || proveFalse?.isSome) = true) Lean.Elab.Tactic.Omega.Problem.proveFalse?_spec._autoParam)
  (explanation? : Thunk String) (assumptions_1 : Array Lean.Elab.Tactic.Omega.Proof) (numVars_1 : ℕ)
  (constraints_1 : Std.HashMap Lean.Omega.Coeffs Lean.Elab.Tactic.Omega.Fact)
  (equalities_1 : Std.HashSet Lean.Omega.Coeffs) (eliminations_1 : List (Lean.Elab.Tactic.Omega.Fact × ℕ × ℤ))
  (possible_1 : Bool) (proveFalse?_1 : Option Lean.Elab.Tactic.Omega.Proof)
  (proveFalse?_spec_1 :
    autoParam ((possible_1 || proveFalse?_1.isSome) = true) Lean.Elab.Tactic.Omega.Problem.proveFalse?_spec._autoParam)
  (explanation?_1 : Thunk String),
  ({ assumptions := assumptions, numVars := numVars, constraints := constraints, equalities := equalities,
        eliminations := eliminations, possible := possible, proveFalse? := proveFalse?,
        proveFalse?_spec := proveFalse?_spec, explanation? := explanation? } =
      { assumptions := assumptions_1, numVars := numVars_1, constraints := constraints_1, equalities := equalities_1,
        eliminations := eliminations_1, possible := possible_1, proveFalse? := proveFalse?_1,
        proveFalse?_spec := proveFalse?_spec_1, explanation? := explanation?_1 }) =
    (assumptions = assumptions_1 ∧
      numVars = numVars_1 ∧
        constraints = constraints_1 ∧
          equalities = equalities_1 ∧
            eliminations = eliminations_1 ∧
              possible = possible_1 ∧ proveFalse? = proveFalse?_1 ∧ explanation? = explanation?_1)
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.Path.listL.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode.Path α → Sort u_2) (h_1 : Unit → motive RBTree.RBNode.Path.root)
  (h_2 :
    (c : RBTree.RBColor) →
      (parent : RBTree.RBNode.Path α) → (v : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left c parent v r))
  (h_3 :
    (c : RBTree.RBColor) →
      (l : RBTree.RBNode α) →
        (v : α) → (parent : RBTree.RBNode.Path α) → motive (RBTree.RBNode.Path.right c l v parent)),
  (match RBTree.RBNode.Path.root with
    | RBTree.RBNode.Path.root => h_1 ()
    | RBTree.RBNode.Path.left c parent v r => h_2 c parent v r
    | RBTree.RBNode.Path.right c l v parent => h_3 c l v parent) =
    h_1 ()
-- Lean.Meta.WHNF
_private.Lean.Meta.WHNF.0.Lean.Meta.toCtorWhenK : Lean.RecursorVal → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Logic.Relation
Relation.isTrans_join : ∀ {α : Type u_1} {r : α → α → Prop} [IsTrans α r],
  (∀ (a b c : α), r a b → r a c → Relation.Join r b c) → IsTrans α (Relation.Join r)
-- Lean.Language.Lean.Types
/-- Shortcut accessor to the final header state, if successful.  -/
Lean.Language.Lean.HeaderParsedSnapshot.processedResult : Lean.Language.Lean.HeaderParsedSnapshot → Lean.Language.SnapshotTask (Option Lean.Language.Lean.HeaderProcessedState)
-- Lean.Elab.ConfigEval.Commands
Lean.Elab.ConfigEval.configEntryHandlerKeyPrefix : Lean.ParserDescr
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_maxKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {km : α}, t.maxKey? = some km → t.getKey! km = km
-- Init.Data.String.Basic
String.asString_data : ∀ {b : String}, String.ofList b.toList = b
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_filterMap_le_size : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  {γ : α → Type w} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β a → Option (γ a)},
  (↑m).WF → (↑(Std.DHashMap.Internal.Raw₀.filterMap f m)).size ≤ (↑m).size
-- Mathlib.GroupTheory.GroupAction.Embedding
Function.Embedding.vadd_def : ∀ {G : Type u_1} {α : Type u_3} {β : Type u_4} [inst : AddGroup G] [inst_1 : AddAction G β] (g : G) (f : α ↪ β),
  g +ᵥ f = f.trans (Equiv.toEmbedding (AddAction.toPerm g))
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.distinct_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp],
  List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) t.toList
-- Mathlib.Data.PFunctor.Multivariate.W
/-- **Alias** of `MvPFunctor.wCases`.

---

Cases lemma for `W` types  -/
MvPFunctor.w_cases : {n : ℕ} →
  (P : MvPFunctor.{u} (n + 1)) →
    {α : TypeVec.{u} n} →
      {C : P.W α → Sort v} →
        ((a : P.A) → (f' : (P.drop.B a).Arrow α) → (f : P.last.B a → P.W α) → C (P.wMk a f' f)) → (x : P.W α) → C x
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.instHasOfPrecompPropertyTop : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C),
  ⊤.HasOfPrecompProperty W
-- Lean.Compiler.IR.CompilerM
Lean.IR.addDecl : Lean.IR.Decl → Lean.IR.CompilerM Unit
-- Init.Data.List.Sort.Impl
List.MergeSort.Internal.splitRevInTwo_snd : ∀ {α : Type u_1} {n : ℕ} (l : { l // l.length = n }),
  (List.MergeSort.Internal.splitRevInTwo l).2 = ⟨↑(List.MergeSort.Internal.splitInTwo l).2, ⋯⟩