mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.δ_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) {m n : M}
  {X Y : C} (f : X ⟶ Y) [inst_3 : F.OplaxMonoidal],
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.OplaxMonoidal.δ F m n).app X)
      ((F.obj n).map ((F.obj m).map f)) =
    CategoryTheory.CategoryStruct.comp ((F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj m n)).map f)
      ((CategoryTheory.Functor.OplaxMonoidal.δ F m n).app Y)
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasNegAssignment.eq_4 : Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned.hasNegAssignment = false
-- Mathlib.RingTheory.Ideal.HasGoingUp
Ideal.exists_ideal_ge_liesOver_of_le : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.HasGoingUp R S] {p q : Ideal R} [q.IsPrime] (P : Ideal S) [P.IsPrime] [P.LiesOver p],
  p ≤ q → ∃ Q, P ≤ Q ∧ Q.IsPrime ∧ Q.LiesOver q
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instBEqSignature : {pu : Lean.Compiler.LCNF.Purity} → BEq (Lean.Compiler.LCNF.Signature pu)
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.HasAbsLeftKanLift.mk : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  [toHasLeftKanLift : CategoryTheory.Bicategory.HasLeftKanLift f g],
  (∀ {x : B} (h : x ⟶ c), CategoryTheory.Bicategory.LanLift.CommuteWith f g h) →
    CategoryTheory.Bicategory.HasAbsLeftKanLift f g
-- Mathlib.Data.TypeVec
TypeVec.subtypeVal.eq_2 : ∀ (n : ℕ) (x_4 : TypeVec.{u} n.succ) (x_5 : x_4.Arrow (TypeVec.repeat n.succ Prop)),
  TypeVec.subtypeVal x_5 Fin2.fz = Subtype.val
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_empty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {a fallback : α},
  ∅.getKeyD a fallback = fallback
-- Mathlib.RingTheory.Ideal.Maps
Submodule.mem_annihilator' : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M} {r : R}, r ∈ N.annihilator ↔ N ≤ Submodule.comap (r • LinearMap.id) ⊥
-- Mathlib.RingTheory.WittVector.DiscreteValuationRing
WittVector.inverseCoeff.eq_def : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : CommRing k] [inst_1 : CharP k p] (a : kˣ)
  (A : WittVector p k) (x : ℕ),
  WittVector.inverseCoeff a A x =
    match x with
    | 0 => ↑a⁻¹
    | n.succ => WittVector.succNthValUnits n a A fun i => WittVector.inverseCoeff a A ↑i
-- Mathlib.RingTheory.Flat.CategoryTheory
Module.Flat.lTensor_shortComplex_exact : ∀ {R : Type u} [inst : CommRing R] (M : ModuleCat R) [Module.Flat R ↑M] (C : CategoryTheory.ShortComplex (ModuleCat R)),
  C.Exact → (C.map (CategoryTheory.MonoidalCategory.tensorLeft M)).Exact
-- Aesop.Script.SScript
Aesop.Script.SScript.brecOn.go : {motive : Aesop.Script.SScript → Sort u} →
  (t : Aesop.Script.SScript) →
    ((t : Aesop.Script.SScript) → Aesop.Script.SScript.below t → motive t) → motive t ×' Aesop.Script.SScript.below t
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.infDist_inter_closedBall_of_mem : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x y : α},
  y ∈ s → Metric.infDist x (s ∩ Metric.closedBall x (dist y x)) = Metric.infDist x s
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- The inclusion homomorphism from a subgroup `H` contained in `K` to `K`.  -/
Subgroup.inclusion : {G : Type u_1} → [inst : Group G] → {H K : Subgroup G} → H ≤ K → ↥H →* ↥K
-- Init.Data.UInt.Bitwise
UInt8.toFin_not : ∀ (a : UInt8), (~~~a).toFin = a.toFin.rev
-- Std.Time.Zoned.TimeZone
Std.Time.TimeZone.Offset.ofSeconds.injEq : ∀ (second second_1 : Std.Time.Second.Offset), ({ second := second } = { second := second_1 }) = (second = second_1)
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- Given `J : CardinalFilteredPoset κ` and a regular cardinal `κ'`,
this is the predicate on `Set J.withTop.obj` that is satisfied by
subsets that are of cardinality `< κ'` and contain `⊤`.  -/
CategoryTheory.CardinalDirectedPoset.PropSetWithTop : {κ : Cardinal.{u}} →
  [inst : Fact κ.IsRegular] →
    (J : CategoryTheory.CardinalDirectedPoset κ) → (κ' : Cardinal.{u}) → [Fact κ'.IsRegular] → Set ↑J.withTop.obj → Prop
-- Mathlib.CategoryTheory.Limits.Creates
/-- When `F` is fully faithful, and `HasLimit (K ⋙ F)`, to show that `F` creates the limit for `K`
it suffices to exhibit a lift of the chosen limit cone for `K ⋙ F`.
 -/
CategoryTheory.createsLimitOfFullyFaithfulOfLift : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              {F : CategoryTheory.Functor C D} →
                [F.Full] →
                  [F.Faithful] →
                    [inst_5 : CategoryTheory.Limits.HasLimit (K.comp F)] →
                      (c : CategoryTheory.Limits.Cone K) →
                        (F.mapCone c ≅ CategoryTheory.Limits.limit.cone (K.comp F)) → CategoryTheory.CreatesLimit K F
-- Mathlib.Data.Set.Basic
Set.Nonempty.mono : ∀ {α : Type u} {s t : Set α}, s ⊆ t → s.Nonempty → t.Nonempty
-- Mathlib.Algebra.Vertex.VertexOperator
VertexOperator.coeff_eq_ncoeff : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  (A : VertexOperator R V) (n : ℤ), HVertexOperator.coeff A n = VertexOperator.ncoeff A (-n - 1)
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.instIsClosedUnderIsomorphismsBounded : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C), t.bounded.IsClosedUnderIsomorphisms
-- Mathlib.Analysis.Complex.Trigonometric
Real.tan_div_sqrt_one_add_tan_sq : ∀ {x : ℝ}, 0 < Real.cos x → Real.tan x / √(1 + Real.tan x ^ 2) = Real.sin x
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- The subspace of vectors orthogonal to a given subspace, denoted `Kᗮ`.  -/
Submodule.«term_ᗮ» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Order.Floor.Defs
/-- `FloorRing.floor a` computes the greatest integer `z` such that `(z : α) ≤ a`.  -/
FloorRing.floor : {α : Type u_4} → {inst : Ring α} → {inst_1 : LinearOrder α} → [self : FloorRing α] → α → ℤ
-- Mathlib.Analysis.SpecialFunctions.Log.InvLog
Real.inv_log_isLittleO_one : (fun x => (Real.log x)⁻¹) =o[Filter.atTop] fun x => 1
-- Mathlib.GroupTheory.OrderOfElement
/-- 1 is of finite order in any monoid.  -/
IsOfFinOrder.one : ∀ {G : Type u_1} [inst : Monoid G], IsOfFinOrder 1
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.compLeft_injective : ∀ {R₁ : Type u_3} {M₁ : Type u_4} [inst : CommRing R₁] [inst_1 : AddCommGroup M₁] [inst_2 : Module R₁ M₁]
  (B : LinearMap.BilinForm R₁ M₁), B.Nondegenerate → Function.Injective B.compLeft
-- Lean.Attributes
Lean.instToStringAttributeKind : ToString Lean.AttributeKind
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.instIsStableUnderBaseChangeComapOfPreservesLimitsOfShapeWalkingCospan : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {F : CategoryTheory.Functor C D} {J : CategoryTheory.Precoverage D}
  [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F] [J.IsStableUnderBaseChange],
  (CategoryTheory.Precoverage.comap F J).IsStableUnderBaseChange
-- Mathlib.Topology.Algebra.GroupCompletion
UniformSpace.Completion.addGroup : {α : Type u_3} →
  [inst : UniformSpace α] → [inst_1 : AddGroup α] → [IsUniformAddGroup α] → AddGroup (UniformSpace.Completion α)
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
CategoryTheory.ObjectProperty.colimitsClosure_top : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type t} (J : α → Type u')
  [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)], ⊤.colimitsClosure J = ⊤
-- Init.Data.AC
Lean.Data.AC.Context.assoc : ∀ {α : Sort u} (self : Lean.Data.AC.Context α), Std.Associative self.op
-- Qq.MetaM
Qq.instReprMaybeDefEq : {u : Lean.Level} →
  {α :
      have u := u;
      Q(Sort u)} →
    {a b : Q(«$α»)} → Repr (Qq.MaybeDefEq a b)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.negRev_involutive : ∀ {α : Type u}, Function.Involutive FreeAddGroup.negRev
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.mem_restrict' : ∀ {ι : Type u_1} {I J J₁ : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I),
  J₁ ∈ π.restrict J ↔ ∃ J' ∈ π, ↑J₁ = ↑J ∩ ↑J'
-- Init.Data.List.Basic
List.isPrefixOf_cons_cons : ∀ {α : Type u} {as : List α} {b : α} {bs : List α} [inst : BEq α] {a : α},
  (a :: as).isPrefixOf (b :: bs) = (a == b && as.isPrefixOf bs)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
IsCyclic.card_powMonoidHom_range : ∀ (G : Type u_2) [inst : CommGroup G] [hG : IsCyclic G] [Finite G] (d : ℕ),
  Nat.card ↥(powMonoidHom d).range = Nat.card G / (Nat.card G).gcd d
-- Mathlib.CategoryTheory.Triangulated.TriangleShift
CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero_eq : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive],
  CategoryTheory.shiftFunctorZero (CategoryTheory.Pretriangulated.Triangle C) ℤ =
    CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero C
-- Mathlib.Analysis.Normed.Lp.PiLp
LinearIsometryEquiv.piLpCurry_apply : ∀ {𝕜 : Type u_1} [inst : Semiring 𝕜] {ι : Type u_5} {κ : ι → Type u_6} (p : ENNReal) [inst_1 : Fact (1 ≤ p)]
  [inst_2 : Fintype ι] [inst_3 : (i : ι) → Fintype (κ i)] (α : (i : ι) → κ i → Type u_7)
  [inst_4 : (i : ι) → (k : κ i) → SeminormedAddCommGroup (α i k)] [inst_5 : (i : ι) → (k : κ i) → Module 𝕜 (α i k)]
  (f : PiLp p fun i => α i.fst i.snd),
  (LinearIsometryEquiv.piLpCurry 𝕜 p α) f = WithLp.toLp p fun i => WithLp.toLp p (Sigma.curry f.ofLp i)
-- Std.Tactic.BVDecide.LRAT.Internal.CNF
Std.Tactic.BVDecide.LRAT.Internal.Literal.sat_iff : ∀ {α : Type u_1} (p : α → Bool) (a : α) (b : Bool), Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p (a, b) ↔ p a = b
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- Constructor for `LaxMonoidalFunctor C D`.  -/
CategoryTheory.LaxMonoidalFunctor.of : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            (F : CategoryTheory.Functor C D) → [F.LaxMonoidal] → CategoryTheory.LaxMonoidalFunctor C D
-- Mathlib.Topology.Sheaves.EtaleSpace
TopCat.Presheaf.EtaleSpace.mk : {X : TopCat} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {CC : C → Type v} →
        {FC : C → C → Type w} →
          [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
            [inst_2 : CategoryTheory.ConcreteCategory C FC] →
              [inst_3 : CategoryTheory.Limits.HasColimits C] →
                {F : TopCat.Presheaf C X} → (base : ↑X) → CategoryTheory.ToType (F.stalk base) → F.EtaleSpace
-- Mathlib.Computability.Primrec.List
/-- `List.take` is primitive recursive.  -/
Primrec.list_take : ∀ {α : Type u_1} [inst : Primcodable α], Primrec₂ List.take
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.IsUpper.tendsto_nhds_iff_not_le : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsUpper α] {β : Type u_3} {f : β → α}
  {l : Filter β} {x : α}, Filter.Tendsto f l (nhds x) ↔ ∀ (y : α), ¬x ≤ y → ∀ᶠ (z : β) in l, ¬f z ≤ y
-- Mathlib.Control.Monad.Writer
WriterT.instMonadWriter : {M : Type u → Type v} → {ω : Type u} → [Monad M] → MonadWriter ω (WriterT ω M)
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Run a tactic at each proof step, with optional timing.

`label` is an optional human-readable name for output. If `none`, the tactic syntax is used.

Reports elapsed time in milliseconds for each successful replacement
when `linter.tacticAnalysis.tryAtEachStep.showTiming` is true.

When `linter.tacticAnalysis.tryAtEachStep.selfReplacements` is false, cases where
the suggested tactic matches the existing proof are suppressed.
 -/
Mathlib.TacticAnalysis.tryAtEachStepCore : (Lean.Syntax → Lean.MVarId → Lean.Elab.Command.CommandElabM (Lean.TSyntax `tactic)) →
  optParam (Option String) none → Mathlib.TacticAnalysis.Config
-- Init.Data.Array.Lemmas
Array.anyM_stop_le_start : ∀ {m : Type → Type u_1} {α : Type u_2} [inst : Monad m] {p : α → m Bool} {as : Array α} {start stop : ℕ},
  min stop as.size ≤ start → Array.anyM p as start stop = pure false
-- Mathlib.Data.UInt
UInt32.toBitVec_intCast : ∀ (z : ℤ), (↑z).toBitVec = ↑z
-- Std.Sync.CancellationToken
Std.CancellationToken.Consumer.normal.inj : ∀ {promise promise_1 : IO.Promise Unit},
  Std.CancellationToken.Consumer.normal promise = Std.CancellationToken.Consumer.normal promise_1 → promise = promise_1
-- Mathlib.Logic.Function.Basic
InvImage.equivalence : ∀ {α : Sort u} {β : Sort v} (r : β → β → Prop) (f : α → β), Equivalence r → Equivalence (InvImage r f)
-- Init.Data.Option.Lemmas
Option.associative_merge : ∀ {α : Type u_1} (f : α → α → α) [Std.Associative f], Std.Associative (Option.merge f)
-- Lean.Parser.Syntax
Lean.Parser.Syntax.cat.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.InnerProductSpace.SingularValues
LinearMap.hasEigenvalue_adjoint_comp_self_sq_singularValues : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F]
  [inst_6 : FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F) {n : ℕ},
  n < Module.finrank 𝕜 E → Module.End.HasEigenvalue (LinearMap.adjoint T ∘ₗ T) (↑(T.singularValues n) ^ 2)
-- Mathlib.Logic.Basic
iff_comm_eq : ∀ (a b : Prop), (a ↔ b) = (b ↔ a)
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleCompIso_hom_app_hom₁ : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.HasShift D ℤ] [inst_5 : CategoryTheory.HasShift E ℤ]
  (F : CategoryTheory.Functor C D) [inst_6 : F.CommShift ℤ] (G : CategoryTheory.Functor D E) [inst_7 : G.CommShift ℤ]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  ((F.mapTriangleCompIso G).hom.app X).hom₁ = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.obj₁))
-- Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
ChartedSpace.locallyRingedSpace_comp : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {EM : Type u_1} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_2} [inst_3 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM}
  {M : Type u} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace HM M] {EN : Type u_3}
  [inst_6 : NormedAddCommGroup EN] [inst_7 : NormedSpace 𝕜 EN] {HN : Type u_4} [inst_8 : TopologicalSpace HN]
  {IN : ModelWithCorners 𝕜 EN HN} {N : Type u} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace HN N]
  {EP : Type u_5} [inst_11 : NormedAddCommGroup EP] [inst_12 : NormedSpace 𝕜 EP] {HP : Type u_6}
  [inst_13 : TopologicalSpace HP] (IP : ModelWithCorners 𝕜 EP HP) {P : Type u} [inst_14 : TopologicalSpace P]
  [inst_15 : ChartedSpace HP P] {f : M → N} (hf : ContMDiff IM IN (↑⊤) f) {g : N → P} (hg : ContMDiff IN IP (↑⊤) g),
  ChartedSpace.locallyRingedSpaceMap (g ∘ f) ⋯ =
    CategoryTheory.CategoryStruct.comp (ChartedSpace.locallyRingedSpaceMap f hf)
      (ChartedSpace.locallyRingedSpaceMap g hg)
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.ofSet_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : Set X) (hs : IsOpen s), ↑(OpenPartialHomeomorph.ofSet s hs) = id
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.bal : ∀ {α : Type u_1} [inst : Preorder α] {lo : WithBot α} {t : Ordnode α} {hi : WithTop α},
  Ordnode.Valid' lo t hi → t.Balanced
-- Mathlib.SetTheory.ZFC.Ordinal
/-- An ordinal is a transitive set.  -/
ZFSet.IsOrdinal.isTransitive : ∀ {x : ZFSet.{u_1}}, x.IsOrdinal → x.IsTransitive
-- Mathlib.Computability.DFA
DFA.reindex_refl : ∀ {α : Type u} {σ : Type v} (M : DFA α σ), (DFA.reindex (Equiv.refl σ)) M = M
-- Mathlib.GroupTheory.OrderOfElement
nsmul_eq_nsmul_iff_modEq : ∀ {G : Type u_1} [inst : AddLeftCancelMonoid G] {x : G} {m n : ℕ}, n • x = m • x ↔ n ≡ m [MOD addOrderOf x]
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RccSliceData.mk.inj : ∀ {α : Type u} {inst : Ord α} {treeMap : Std.DTreeMap.Internal.Impl α fun x => Unit} {range : Std.Rcc α}
  {treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => Unit} {range_1 : Std.Rcc α},
  { treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 } →
    treeMap = treeMap_1 ∧ range = range_1
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.image_symm_eq_preimage : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (s : Set A₂), ⇑e.symm '' s = ⇑e ⁻¹' s
-- Mathlib.Computability.Primrec.Basic
Primrec₂.mk : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : α → β → σ}, (Primrec fun p => f p.1 p.2) → Primrec₂ f
-- Mathlib.Order.Category.BoolAlg
BoolAlg.hasForgetToBddDistLat : CategoryTheory.HasForget₂ BoolAlg BddDistLat
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.single_zero_ofScientific : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommGroup Γ] [inst_1 : LinearOrder Γ] [IsOrderedAddMonoid Γ]
  [inst_3 : Field R] (m : ℕ) (e : Bool) (s : ℕ),
  (HahnSeries.single 0) (OfScientific.ofScientific m e s) = OfScientific.ofScientific m e s
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getD_ofList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp]
  [inst_2 : BEq α] [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α} {fallback : β k},
  (List.map Sigma.fst l).contains k = false → (Std.ExtDTreeMap.ofList l cmp).getD k fallback = fallback
-- Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
/-- The bijection `Fin (n + 2) ≃ (⦋n⦌ ⟶ ⦋1⦌)` which sends `i : Fin (n + 2)` to the
morphism `⦋n⦌ ⟶ ⦋1⦌` in the simplex category which corresponds to the monotone map
`Fin (n + 1) → Fin 2` which takes `i` times the value `0`.  -/
SimplexCategory.toMk₁Equiv : {n : ℕ} → Fin (n + 2) ≃ ({ len := n } ⟶ { len := 1 })
-- Mathlib.Order.Concept
Concept.leftInverse_ofAttributes_extent : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop}, Function.LeftInverse (Concept.ofAttributes r) Concept.intent
-- Init.Data.Array.Lemmas
/-- Variant of `map_id`, with a side condition that the function is pointwise the identity.  -/
Array.map_id'' : ∀ {α : Type u_1} {f : α → α}, (∀ (x : α), f x = x) → ∀ (xs : Array α), Array.map f xs = xs
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalAddSubgroup.instSemilatticeSupOpenNormalAddSubgroup.eq_1 : ∀ {G : Type u} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : SeparatelyContinuousAdd G],
  OpenNormalAddSubgroup.instSemilatticeSupOpenNormalAddSubgroup =
    Function.Injective.semilatticeSup (fun H => ↑H.toOpenAddSubgroup) ⋯ ⋯ ⋯ ⋯
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.cons_pos : ∀ {M : Type u_1} [inst : GroupWithZero M] [inst_1 : PartialOrder M] [PosMulStrictMono M] [PosMulReflectLT M]
  [ZeroLEOneClass M] (r : ℤ) {x : M},
  0 < x → ∀ {l : Mathlib.Tactic.FieldSimp.NF M}, 0 < l.eval → 0 < ((r, x) ::ᵣ l).eval
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_diff_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → (m₁ \ m₂).getKey! k = m₁.getKey! k
-- Mathlib.Algebra.Torsor.Basic
/-- In the special case of additive commutative groups (as opposed to just additive torsors),
`Equiv.pointReflection x` coincides with `Equiv.subLeft (2 • x)`.  -/
Equiv.pointReflection_eq_subLeft : ∀ {G : Type u_5} [inst : AddCommGroup G] (x : G), Equiv.pointReflection x = Equiv.subLeft (2 • x)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.Stmt.pop.sizeOf_spec : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : SizeOf K] [inst_1 : (a : K) → SizeOf (Γ a)]
  [inst_2 : SizeOf Λ] [inst_3 : SizeOf σ] (k : K) (a : σ → Option (Γ k) → σ) (a_1 : Turing.TM2.Stmt Γ Λ σ),
  sizeOf (Turing.TM2.Stmt.pop k a a_1) = 1 + sizeOf k + sizeOf a_1
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidIso.val_unitsWithZero_symm_apply : ∀ {α : Type u_6} [inst : Group α] [inst_1 : Preorder α] (a : α), ↑(OrderMonoidIso.unitsWithZero.symm a) = ↑a
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.superpose_head_idempotent.inj : ∀ {x : Lean.Grind.AC.Var} {c₁ : Lean.Meta.Grind.AC.EqCnstr} {x_1 : Lean.Grind.AC.Var}
  {c₁_1 : Lean.Meta.Grind.AC.EqCnstr},
  Lean.Meta.Grind.AC.EqCnstrProof.superpose_head_idempotent x c₁ =
      Lean.Meta.Grind.AC.EqCnstrProof.superpose_head_idempotent x_1 c₁_1 →
    x = x_1 ∧ c₁ = c₁_1
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.prodOpEquiv_functor_map : ∀ (C : Type u₃) [inst : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [inst_1 : CategoryTheory.Category.{v₄, u₄} D]
  {X Y : (C × D)ᵒᵖ} (f : X ⟶ Y),
  (CategoryTheory.prodOpEquiv C).functor.map f = CategoryTheory.Prod.mkHom f.unop.1.op f.unop.2.op
-- Mathlib.Topology.Homotopy.Path
Path.Homotopic.symm : ∀ {X : Type u} [inst : TopologicalSpace X] {x₀ x₁ : X} ⦃p₀ p₁ : Path x₀ x₁⦄, p₀.Homotopic p₁ → p₁.Homotopic p₀
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.toCLM_intCast : ∀ {𝕜₂ : Type u_2} [inst : NormedField 𝕜₂] {F : Type u_4} [inst_1 : AddCommGroup F] [inst_2 : TopologicalSpace F]
  [inst_3 : Module 𝕜₂ F] [inst_4 : IsTopologicalAddGroup F] (n : ℤ), (↑n).toCLM = ↑n
-- Mathlib.RepresentationTheory.Basic
/-- If `ρ : Representation k G V`, then `ρ.asModule` is a type synonym for `V`,
which we equip with an instance `Module k[G] ρ.asModule`.

You should use `asModuleEquiv : ρ.asModule ≃+ V` to translate terms.
 -/
Representation.asModule : {k : Type u_4} →
  {G : Type u_5} →
    {V : Type u_6} →
      [inst : Semiring k] →
        [inst_1 : Monoid G] → [inst_2 : AddCommMonoid V] → [inst_3 : Module k V] → Representation k G V → Type u_6
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.trans : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.DTreeMap.Raw α β cmp},
  t₁.Equiv t₂ → t₂.Equiv t₃ → t₁.Equiv t₃
-- Lean.Data.Lsp.Internal
Lean.Lsp.instOrdRefIdent : Ord Lean.Lsp.RefIdent
-- Mathlib.RingTheory.PowerBasis
PowerBasis.constr_pow_gen : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] {S' : Type u_7}
  [inst_3 : Ring S'] [inst_4 : Algebra A S'] (pb : PowerBasis A S) {y : S'},
  (Polynomial.aeval y) (minpoly A pb.gen) = 0 → ((pb.basis.constr A) fun i => y ^ ↑i) pb.gen = y
-- Mathlib.Computability.Primrec.Basic
Primrec.of_equiv_symm_iff : ∀ {α : Type u_1} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable σ] {β : Type u_4} (e : β ≃ α) {f : σ → α},
  (Primrec fun a => e.symm (f a)) ↔ Primrec f
-- Init.Data.Nat.Simproc
Nat.Simproc.le_add_ge : ∀ (a : ℕ) {b c : ℕ}, a ≥ c → (a ≤ b + c) = (a - c ≤ b)