mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balance!.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) (size : ℕ) (k : α) (v : β k)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          motive
            (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf))
  (h_3 :
    (size : ℕ) →
      (rk : α) →
        (rv : β rk) →
          (rr : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k : α) →
                (v : β k) →
                  (l r : Std.DTreeMap.Internal.Impl α β) →
                    rr = Std.DTreeMap.Internal.Impl.inner size_1 k v l r →
                      motive
                        (Std.DTreeMap.Internal.Impl.inner size rk rv Std.DTreeMap.Internal.Impl.leaf
                          (Std.DTreeMap.Internal.Impl.inner size_1 k v l r)))
  (h_4 :
    (size : ℕ) →
      (rk : α) →
        (rv : β rk) →
          (size_1 : ℕ) →
            (rlk : α) →
              (rlv : β rlk) →
                (l r : Std.DTreeMap.Internal.Impl α β) →
                  motive
                    (Std.DTreeMap.Internal.Impl.inner size rk rv (Std.DTreeMap.Internal.Impl.inner size_1 rlk rlv l r)
                      Std.DTreeMap.Internal.Impl.leaf))
  (h_5 :
    (rs : ℕ) →
      (rk : α) →
        (rv : β rk) →
          (rls : ℕ) →
            (rlk : α) →
              (rlv : β rlk) →
                (rll rlr rr : Std.DTreeMap.Internal.Impl α β) →
                  (size : ℕ) →
                    (k : α) →
                      (v : β k) →
                        (l r : Std.DTreeMap.Internal.Impl α β) →
                          rr = Std.DTreeMap.Internal.Impl.inner size k v l r →
                            motive
                              (Std.DTreeMap.Internal.Impl.inner rs rk rv
                                (Std.DTreeMap.Internal.Impl.inner rls rlk rlv rll rlr)
                                (Std.DTreeMap.Internal.Impl.inner size k v l r))),
  (match Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf =>
      h_2 size k v
    |
    Std.DTreeMap.Internal.Impl.inner size rk rv Std.DTreeMap.Internal.Impl.leaf
        rr@h:(Std.DTreeMap.Internal.Impl.inner size_1 k v l r) =>
      h_3 size rk rv rr size_1 k v l r h
    |
    Std.DTreeMap.Internal.Impl.inner size rk rv (Std.DTreeMap.Internal.Impl.inner size_1 rlk rlv l r)
        Std.DTreeMap.Internal.Impl.leaf =>
      h_4 size rk rv size_1 rlk rlv l r
    |
    Std.DTreeMap.Internal.Impl.inner rs rk rv (Std.DTreeMap.Internal.Impl.inner rls rlk rlv rll rlr)
        rr@h:(Std.DTreeMap.Internal.Impl.inner size k v l r) =>
      h_5 rs rk rv rls rlk rlv rll rlr rr size k v l r h) =
    h_2 size k v
-- Mathlib.MeasureTheory.Integral.IntegrableOn
integrableOn_Icc_iff_integrableOn_Ioc' : ∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} [inst : PartialOrder α] [MeasurableSingletonClass α]
  [inst_2 : TopologicalSpace ε'] [inst_3 : ESeminormedAddMonoid ε'] [TopologicalSpace.PseudoMetrizableSpace ε']
  {f : α → ε'} {μ : MeasureTheory.Measure α} {a b : α},
  autoParam (μ {a} ≠ ⊤) integrableOn_Icc_iff_integrableOn_Ioc'._auto_1 →
    autoParam (‖f a‖ₑ ≠ ⊤) integrableOn_Icc_iff_integrableOn_Ioc'._auto_3 →
      (MeasureTheory.IntegrableOn f (Set.Icc a b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ioc a b) μ)
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.smul_restrictAppIso_inv : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (M : Y.Modules)
  (U : X.Opens) (r : ↑(Y.presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U)))),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.smul r)
      (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M U).inv =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M U).inv
      (AlgebraicGeometry.Scheme.Modules.smul
        ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appIso f U).hom) r))
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.trans_apply : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : AddCommGroup P] [inst_5 : Module R M]
  [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : LieRingModule L M] [inst_9 : LieRingModule L N]
  [inst_10 : LieRingModule L P] (e₁ : M ≃ₗ⁅R,L⁆ N) (e₂ : N ≃ₗ⁅R,L⁆ P) (m : M), (e₁.trans e₂) m = e₂ (e₁ m)
-- Mathlib.Topology.MetricSpace.Infsep
Set.Finite.relatively_discrete : ∀ {α : Type u_1} [inst : EMetricSpace α] {s : Set α}, s.Finite → ∃ C > 0, ∀ x ∈ s, ∀ y ∈ s, x ≠ y → C ≤ edist x y
-- Mathlib.Logic.Relation
irrefl_iff_le_ne : ∀ {α : Type u_1} {r : α → α → Prop}, Std.Irrefl r ↔ r ≤ Ne
-- Mathlib.Geometry.Manifold.Instances.Real
closure_halfSpace : ∀ {n : ℕ} (p : ENNReal) (a : ℝ) (i : Fin n), closure {y | a ≤ y.ofLp i} = {y | a ≤ y.ofLp i}
-- Mathlib.Tactic.Variable
Mathlib.Command.Variable.variable?.maxSteps : Lean.Option ℕ
-- Mathlib.Algebra.Group.Hom.Defs
ZeroHom.mk_coe : ∀ {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] (f : ZeroHom M N) (h1 : f 0 = 0),
  { toFun := ⇑f, map_zero' := h1 } = f
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.HasPullbacks.hasPullbacks_of_mem : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.Precoverage C} [self : J.HasPullbacks]
  {X Y : C} {R : CategoryTheory.Presieve Y} (f : X ⟶ Y), R ∈ J.coverings Y → R.HasPullbacks f
-- Mathlib.CategoryTheory.Action.Basic
Action.Hom.mk : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_2} →
      [inst_1 : Monoid G] →
        {M N : Action V G} →
          (hom : M.V ⟶ N.V) →
            autoParam
                (∀ (g : G),
                  CategoryTheory.CategoryStruct.comp (M.ρ g) hom = CategoryTheory.CategoryStruct.comp hom (N.ρ g))
                Action.Hom.comm._autoParam →
              M.Hom N
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousMultilinearMap.alternatization_apply_apply : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommGroup N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] [inst_7 : IsTopologicalAddGroup N] [inst_8 : Fintype ι] [inst_9 : DecidableEq ι]
  (f : ContinuousMultilinearMap R (fun x => M) N) (v : ι → M),
  (ContinuousMultilinearMap.alternatization f) v = ∑ σ, Equiv.Perm.sign σ • f (v ∘ ⇑σ)
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
/-- Version of `exponent_def` using `ExpChar`.  -/
IsPurelyInseparable.exponent_def' : ∀ (K : Type u_2) {L : Type u_3} [inst : CommRing K] [inst_1 : Ring L] [inst_2 : Algebra K L]
  [inst_3 : IsPurelyInseparable.HasExponent K L] (p : ℕ) [ExpChar K p] (a : L),
  a ^ p ^ IsPurelyInseparable.exponent K L ∈ (algebraMap K L).range
-- Mathlib.CategoryTheory.Abelian.Projective.Ext
CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_add : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.ProjectiveResolution X) {n : ℕ}
  (x y : CategoryTheory.Abelian.Ext X Y n),
  R.extEquivCohomologyClass (x + y) = R.extEquivCohomologyClass x + R.extEquivCohomologyClass y
-- Lean.Util.MonadBacktrack
/-- Execute `x?`, but backtrack state if result is `none` or an exception was thrown.
 -/
Lean.commitWhenSome? : {m : Type → Type} →
  {s : Type} →
    {ε : Type u_1} →
      {α : Type} → [Monad m] → [Lean.MonadBacktrack s m] → [MonadExcept ε m] → m (Option α) → m (Option α)
-- Std.Data.TreeSet.Raw.WF
Std.TreeSet.Raw.WF.inter : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {t₁ t₂ : Std.TreeSet.Raw α cmp}, t₁.WF → (t₁ ∩ t₂).WF
-- Lean.Parser.Types
Lean.Parser.CacheableParserContext.mk.sizeOf_spec : ∀ (prec quotDepth : ℕ) (suppressInsideQuot : Bool) (savedPos? : Option String.Pos.Raw)
  (forbiddenTk? : Option Lean.Parser.Token),
  sizeOf
      { prec := prec, quotDepth := quotDepth, suppressInsideQuot := suppressInsideQuot, savedPos? := savedPos?,
        forbiddenTk? := forbiddenTk? } =
    1 + sizeOf prec + sizeOf quotDepth + sizeOf suppressInsideQuot + sizeOf savedPos? + sizeOf forbiddenTk?
-- Mathlib.Topology.Homotopy.Path
/-- The quotient on `Path x₀ x₁` by the equivalence relation `Path.Homotopic`.
 -/
Path.Homotopic.Quotient : {X : Type u} → [TopologicalSpace X] → X → X → Type u
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- Map an `Arrow` along a refinement `S ⟶ T`.  -/
CategoryTheory.GrothendieckTopology.Cover.Arrow.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} → {J : CategoryTheory.GrothendieckTopology C} → {S T : J.Cover X} → S.Arrow → (S ⟶ T) → T.Arrow
-- Batteries.Recycling.RBTree.Basic
/-- `O(n₁ * (log n₁ + log n₂))`. Constructs the set of all elements of `t₁` that are not in `t₂`.
 -/
RBTree.RBSet.sdiff : {α : Type u_1} → {cmp : α → α → Ordering} → RBTree.RBSet α cmp → RBTree.RBSet α cmp → RBTree.RBSet α cmp
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyMapData.instUnique : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        {φ : S₁ ⟶ S₂} →
          {h₁ : S₁.HomologyData} → {h₂ : S₂.HomologyData} → Unique (CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂)
-- Mathlib.RepresentationTheory.Rep.Basic
/-- Given a representation `A` of a finite group `G`, the norm map `A ⟶ A` defined by
`x ↦ ∑ A.ρ g x` for `g` in `G` defines a natural endomorphism of the identity functor.  -/
Rep.normNatTrans : {k : Type u} →
  [inst : Semiring k] →
    {G : Type v} →
      [inst_1 : Group G] → [Fintype G] → CategoryTheory.End (CategoryTheory.Functor.id (Rep.{u_1, u, v} k G))
-- Lean.Server.CodeActions.Basic
Lean.Server.LazyCodeAction.mk.sizeOf_spec : ∀ (eager : Lean.Lsp.CodeAction) (lazy? : Option (IO Lean.Lsp.CodeAction)),
  sizeOf { eager := eager, lazy? := lazy? } = 1 + sizeOf eager + sizeOf lazy?
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.leftUnitor_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (X : C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom =
    CategoryTheory.SemiCartesianMonoidalCategory.snd (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.instAddSubgroupClass : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M], AddSubgroupClass (LieSubmodule R L M) M
-- Std.Http.Data.URI.Encoding
/-- Proof that all characters in the byte array are valid encoded characters.
 -/
Std.Http.URI.EncodedString.valid : ∀ {r : UInt8 → Bool} (self : Std.Http.URI.EncodedString r), Std.Http.URI.IsAllowedEncodedChars r self.toByteArray
-- Mathlib.AlgebraicTopology.Reedy.Basic
HomotopicalAlgebra.ReedyStructure.le₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [inst_1 : W₁.IsMultiplicative] [inst_2 : W₂.IsMultiplicative] {α : Type u_2} [inst_3 : LinearOrder α]
  [inst_4 : OrderBot α] [inst_5 : SuccOrder α] [inst_6 : WellFoundedLT α]
  (r : HomotopicalAlgebra.ReedyStructure W₁ W₂ α) {X Y : C} (f : X ⟶ Y), W₁ f → r.deg Y ≤ r.deg X
-- Mathlib.Order.Bounds.Basic
/-- **Alias** of `LE.le.isCoinitialFor`.

---

**Alias** of `IsCoinitialFor.of_subset`. -/
HasSubset.Subset.isCoinitialFor : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α}, s ⊆ t → IsCoinitialFor s t
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.isIntertwining : ∀ {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) (f : ρ.IntertwiningMap σ) (g : G) (v : V),
  f ((ρ g) v) = (σ g) (f v)
-- Mathlib.CategoryTheory.Category.PartialFun
partialFunEquivPointed_unitIso_hom_app : ∀ (X : PartialFun),
  partialFunEquivPointed.unitIso.hom.app X =
    (PartialFun.Iso.mk
        { toFun := fun a => ⟨some a, ⋯⟩, invFun := fun a => (↑a).get ⋯, left_inv := ⋯, right_inv := ⋯ }).hom
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop
Std.IterM.step_drop : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] [inst_1 : Std.Iterator α m β] {n : ℕ}
  {it : Std.IterM m β},
  (Std.IterM.drop n it).step = do
    let __do_lift ← it.step
    match __do_lift.inflate with
      | ⟨Std.IterStep.yield it' out, h⟩ =>
        match h' : n with
        | 0 => pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield (Std.IterM.drop 0 it') out ⋯))
        | k.succ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.drop k it') ⋯))
      | ⟨Std.IterStep.skip it', h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.drop n it') ⋯))
      | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.Ring.of_f : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι]
  [inst_4 : (i : ι) → NonAssocSemiring (G i)] [inst_5 : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)]
  [inst_6 : Nonempty ι] {i j : ι} (hij : i ≤ j) (x : G i),
  (DirectLimit.Ring.of G f j) ((f i j hij) x) = (DirectLimit.Ring.of G f i) x
-- Std.Data.ByteSlice
instSliceableByteArrayNatByteSlice_4 : Std.Roo.Sliceable ByteArray ℕ ByteSlice
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
/-- Monad for collecting types that we should try deriving `EvalTerm` or `EvalExpr` instances for.  -/
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.M : Type → Type
-- Mathlib.Analysis.SpecialFunctions.SmoothTransition
Real.smoothTransition.one : Real.smoothTransition 1 = 1
-- Init.Data.String.Lemmas.FindPos
String.posLE_eq_iff : ∀ {s : String} {p : String.Pos.Raw} {q : s.Pos}, s.posLE p = q ↔ q.offset ≤ p ∧ ∀ (q' : s.Pos), q'.offset ≤ p → q' ≤ q
-- Mathlib.Algebra.Homology.ShortComplex.Linear
CategoryTheory.ShortComplex.smul_τ₁ : ∀ {R : Type u_1} {C : Type u_2} [inst : Semiring R] [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] {S₁ S₂ : CategoryTheory.ShortComplex C}
  (a : R) (φ : S₁ ⟶ S₂), (a • φ).τ₁ = a • φ.τ₁
-- Lean.Elab.InfoTree.Types
Lean.Elab.CommandInfo.mk.injEq : ∀ (toElabInfo toElabInfo_1 : Lean.Elab.ElabInfo),
  ({ toElabInfo := toElabInfo } = { toElabInfo := toElabInfo_1 }) = (toElabInfo = toElabInfo_1)
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_eq_zero_of_hasSubgaussianMGF_zero : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'}
  {κ : ProbabilityTheory.Kernel Ω' Ω} {X : Ω → ℝ},
  ProbabilityTheory.Kernel.HasSubgaussianMGF X 0 κ ν → ∀ᵐ (ω' : Ω') ∂ν, X =ᵐ[κ ω'] 0
-- Mathlib.Order.Iterate
Function.Commute.iterate_pos_lt_iff_map_lt : ∀ {α : Type u_1} [inst : LinearOrder α] {f g : α → α},
  Function.Commute f g → Monotone f → StrictMono g → ∀ {x : α} {n : ℕ}, 0 < n → (f^[n] x < g^[n] x ↔ f x < g x)
-- Mathlib.Data.Set.Functor
/-- Evaluates the `SetM` monad, yielding a `Set`.
Implementation note: this is the identity function.  -/
SetM.run : {α : Type u_1} → SetM α → Set α
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.mul_rpow_of_ne_top : ∀ {x y : ENNReal}, x ≠ ⊤ → y ≠ ⊤ → ∀ (z : ℝ), (x * y) ^ z = x ^ z * y ^ z
-- Mathlib.RingTheory.Localization.BaseChange
Algebra.IsPushout.of_bijective_left : ∀ {R : Type u_1} [inst : CommSemiring R] (A : Type u_2) [inst_1 : CommSemiring A] [inst_2 : Algebra R A] (T : Type u_5)
  [inst_3 : CommSemiring T] [inst_4 : Algebra R T] [inst_5 : Algebra A T] [inst_6 : IsScalarTower R A T],
  Function.Bijective ⇑(algebraMap R A) → Algebra.IsPushout R T A T
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
BialgEquiv.toHopfAlgIso_hom : ∀ {R : Type u} [inst : CommRing R] {X Y : Type v} [inst_1 : Ring X] [inst_2 : Ring Y] [inst_3 : HopfAlgebra R X]
  [inst_4 : HopfAlgebra R Y] (e : X ≃ₐc[R] Y), e.toHopfAlgIso.hom = HopfAlgCat.ofHom ↑e
-- Mathlib.Algebra.Ring.Defs
Semiring.toAddCommMonoid : {α : Type u} → [self : Semiring α] → AddCommMonoid α
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeRightOpOfConeEquiv.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ C},
  CategoryTheory.Limits.coconeRightOpOfConeEquiv =
    {
      functor :=
        { obj := fun c => CategoryTheory.Limits.coconeRightOpOfCone (Opposite.unop c),
          map := fun {X Y} f => { hom := f.unop.hom.op, w := ⋯ }, map_id := ⋯, map_comp := ⋯ },
      inverse :=
        { obj := fun c => Opposite.op (CategoryTheory.Limits.coneOfCoconeRightOp c),
          map := fun {X Y} f => Opposite.op { hom := f.hom.unop, w := ⋯ }, map_id := ⋯, map_comp := ⋯ },
      unitIso := CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)ᵒᵖ),
      counitIso :=
        CategoryTheory.Iso.refl
          ({ obj := fun c => Opposite.op (CategoryTheory.Limits.coneOfCoconeRightOp c),
                map := fun {X Y} f => Opposite.op { hom := f.hom.unop, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp
            { obj := fun c => CategoryTheory.Limits.coconeRightOpOfCone (Opposite.unop c),
              map := fun {X Y} f => { hom := f.unop.hom.op, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }),
      functor_unitIso_comp := ⋯ }
-- Lean.Meta.PProdN
/-- `PProd.fst` or `And.left` (using `.proj`), inferring the type of `e`  -/
Lean.Meta.mkPProdFstM : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.sigma_pos : ∀ (k n : ℕ), n ≠ 0 → 0 < (ArithmeticFunction.sigma k) n
-- Init.Data.List.MinMax
List.max?.eq_2 : ∀ {α : Type u} [inst : Max α] (a : α) (as : List α), (a :: as).max? = some (List.foldl max a as)
-- Init.Data.SInt.Lemmas
Int32.toInt8_ofIntLE : ∀ {n : ℤ} (h₁ : Int32.minValue.toInt ≤ n) (h₂ : n ≤ Int32.maxValue.toInt), (Int32.ofIntLE n h₁ h₂).toInt8 = Int8.ofInt n
-- Lean.Meta.Tactic.Grind.ProveEq
/-- Returns `true` if current terms occur under binders.  -/
_private.Lean.Meta.Tactic.Grind.ProveEq.0.Lean.Meta.Grind.inBinder : Lean.Meta.Grind.AbstractM✝ Bool
-- Init.Data.AC
Lean.Data.AC.Expr.op : Lean.Data.AC.Expr → Lean.Data.AC.Expr → Lean.Data.AC.Expr
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.below.id_comp : ∀ {B : Type u} [inst : Quiver B]
  {motive :
    {a b : CategoryTheory.FreeBicategory B} →
      {f g : a ⟶ b} →
        (a_1 a_2 : CategoryTheory.FreeBicategory.Hom₂ f g) → CategoryTheory.FreeBicategory.Rel a_1 a_2 → Prop}
  {a b : B} {f g : CategoryTheory.FreeBicategory.Hom a b} (η : CategoryTheory.FreeBicategory.Hom₂ f g),
  CategoryTheory.FreeBicategory.Rel.below ⋯
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.not_isNonloop_iff : ∀ {α : Type u_1} {M : Matroid α} {e : α},
  autoParam (e ∈ M.E) Matroid.not_isNonloop_iff._auto_1 → (¬M.IsNonloop e ↔ M.IsLoop e)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.exists_isBasis_disjoint_isBasis_of_subset : ∀ {α : Type u_1} (M : Matroid α) {X Y : Set α},
  X ⊆ Y →
    autoParam (Y ⊆ M.E) Matroid.exists_isBasis_disjoint_isBasis_of_subset._auto_1 →
      ∃ I J, M.IsBasis I X ∧ M.IsBasis (I ∪ J) Y ∧ Disjoint X J
-- Mathlib.RingTheory.ZMod.UnitsCyclic
ZMod.not_isCyclic_units_eight : ¬IsCyclic (ZMod 8)ˣ
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.forIn'_cons.match_1.eq_2 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.yield b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_2 b
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.instLinearOrder : {M : Type u_1} →
  [inst : CommGroup M] → [inst_1 : LinearOrder M] → [inst_2 : IsOrderedMonoid M] → LinearOrder (MulArchimedeanClass M)
-- Mathlib.InformationTheory.Hamming
Hamming.ofHamming_symm_eq : ∀ {ι : Type u_2} {β : ι → Type u_3}, Hamming.ofHamming.symm = Hamming.toHamming
-- Mathlib.Algebra.MvPolynomial.Basic
/-- A polynomial all of whose support degrees equal a fixed `d₀` is the single monomial
`monomial d₀ (coeff d₀ φ)`.  -/
MvPolynomial.eq_monomial_of_support_subset_singleton : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {φ : MvPolynomial σ R} {d₀ : σ →₀ ℕ},
  (∀ d ∈ φ.support, d = d₀) → φ = (MvPolynomial.monomial d₀) (MvPolynomial.coeff d₀ φ)
-- Lean.Setup
Lean.Plugin.fromJson? : Lean.Json → Except String Lean.Plugin
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.pullbackCone_condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.Limits.FormalCoproduct C} (f : X ⟶ Z)
  (g : Y ⟶ Z)
  (pb :
    (i : Function.Pullback f.f g.f) →
      CategoryTheory.Limits.PullbackCone (CategoryTheory.CategoryStruct.comp (f.φ (↑i).1) (CategoryTheory.eqToHom ⋯))
        (g.φ (↑i).2)),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb).fst f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb).snd g
-- Mathlib.CategoryTheory.Limits.Chosen.End
/-- Morphisms out of the chosen coend are determined by their composites with `chosenCoend.ι`.  -/
CategoryTheory.Limits.chosenCoend.hom_ext : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} J] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)}
  [inst_2 : CategoryTheory.Limits.ChosenCoendsOfShape J C] {X : C} {f g : CategoryTheory.Limits.chosenCoend F ⟶ X},
  (∀ (j : J),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.chosenCoend.ι F j) f =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.chosenCoend.ι F j) g) →
    f = g
-- Mathlib.Logic.Equiv.Defs
Equiv.arrowCongr'_refl : ∀ {α : Type u_1} {β : Type u_2}, (Equiv.refl α).arrowCongr' (Equiv.refl β) = Equiv.refl (α → β)
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.VectorsProdEqOne.mem_iff : ∀ (G : Type u_2) [inst : Group G] {n : ℕ} (v : List.Vector G n), v ∈ Equiv.Perm.vectorsProdEqOne G n ↔ v.toList.prod = 1
-- Mathlib.Algebra.Algebra.Basic
Algebra.algebraMap_pUnit : ∀ {R : Type u_1} [inst : CommSemiring R] (r : R), (algebraMap R PUnit.{u_4 + 1}) r = PUnit.unit
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.shortComplexFunctor_obj_X₂ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i : ι) (K : HomologicalComplex C c),
  ((HomologicalComplex.shortComplexFunctor C c i).obj K).X₂ = K.X i
-- Aesop.Tree.ExtractScript
Aesop.ExtractScriptM.State.mk.inj : ∀ {script : Aesop.Script.UScript} {proofHasMVar : Bool} {script_1 : Aesop.Script.UScript} {proofHasMVar_1 : Bool},
  { script := script, proofHasMVar := proofHasMVar } = { script := script_1, proofHasMVar := proofHasMVar_1 } →
    script = script_1 ∧ proofHasMVar = proofHasMVar_1
-- Mathlib.LinearAlgebra.Complex.FiniteDimensional
Complex.rank_real_complex' : Cardinal.lift.{u, 0} (Module.rank ℝ ℂ) = 2