mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Field.Defs
/-- Scalar multiplication by a nonnegative rational number.

Unless there is a risk of a `Module ℚ≥0 _` instance diamond, write `nnqsmul := _`. This will set
`nnqsmul` to `(NNRat.cast · * ·)` thanks to unification in the default proof of `nnqsmul_def`.

Do not use directly. Instead use the `•` notation.  -/
DivisionSemiring.nnqsmul : {K : Type u_2} → [self : DivisionSemiring K] → ℚ≥0 → K → K
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.univ_eq_empty : ∀ {α : Type u_1} [inst : Fintype α] [IsEmpty α], Finset.univ = ∅
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.get?.match_1.eq_2 : ∀ {α : Type u_1} {δ : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => δ) → Sort u_3) (size : ℕ) (k' : α)
  (v' : δ) (l r : Std.DTreeMap.Internal.Impl α fun x => δ) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k' : α) →
        (v' : δ) →
          (l r : Std.DTreeMap.Internal.Impl α fun x => δ) → motive (Std.DTreeMap.Internal.Impl.inner size k' v' l r)),
  (match Std.DTreeMap.Internal.Impl.inner size k' v' l r with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k' v' l r => h_2 size k' v' l r) =
    h_2 size k' v' l r
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.ofHom_hom : ∀ {R S : CommRingCat} (f : R ⟶ S), CommRingCat.ofHom (CommRingCat.Hom.hom f) = f
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.coeff_orderTop_ne : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {x : HahnSeries Γ R} {g : Γ},
  x.orderTop = ↑g → x.coeff g ≠ 0
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_filterMap : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp] [inst_2 : Inhabited α] {f : (a : α) → β a → Option (γ a)}
  {k : α}, (Std.DTreeMap.filterMap f t).getKey! k = ((t.getKey? k).pfilter fun x h' => (f x (t.get x ⋯)).isSome).get!
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
/-- Negation as a measurable automorphism of an additive group.  -/
MeasurableEquiv.neg : (G : Type u_4) → [inst : MeasurableSpace G] → [inst_1 : InvolutiveNeg G] → [MeasurableNeg G] → G ≃ᵐ G
-- Std.Data.HashSet.Raw
/-- Check if any element satisfies the predicate, short-circuiting if a predicate succeeds.  -/
Std.HashSet.Raw.any : {α : Type u} → Std.HashSet.Raw α → (α → Bool) → Bool
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.JordanDecomposition.mk.inj : ∀ {α : Type u_2} {inst : MeasurableSpace α} {posPart negPart : MeasureTheory.Measure α}
  {posPart_finite : MeasureTheory.IsFiniteMeasure posPart} {negPart_finite : MeasureTheory.IsFiniteMeasure negPart}
  {mutuallySingular : posPart.MutuallySingular negPart} {posPart_1 negPart_1 : MeasureTheory.Measure α}
  {posPart_finite_1 : MeasureTheory.IsFiniteMeasure posPart_1}
  {negPart_finite_1 : MeasureTheory.IsFiniteMeasure negPart_1}
  {mutuallySingular_1 : posPart_1.MutuallySingular negPart_1},
  { posPart := posPart, negPart := negPart, posPart_finite := posPart_finite, negPart_finite := negPart_finite,
        mutuallySingular := mutuallySingular } =
      { posPart := posPart_1, negPart := negPart_1, posPart_finite := posPart_finite_1,
        negPart_finite := negPart_finite_1, mutuallySingular := mutuallySingular_1 } →
    posPart = posPart_1 ∧ negPart = negPart_1
-- Init.Data.Int.Repr
/-- Returns the decimal string representation of an integer.
 -/
Int.repr : ℤ → String
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.instDecidableIsIndepSetCoeFinsetOfDecidableEqOfDecidableRelAdj : {α : Type u_1} →
  (G : SimpleGraph α) → [DecidableEq α] → [DecidableRel G.Adj] → {s : Finset α} → Decidable (G.IsIndepSet ↑s)
-- Mathlib.Order.SuccPred.Basic
Order.pred_max : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] (a b : α),
  Order.pred (max a b) = max (Order.pred a) (Order.pred b)
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Poly.denote.match_1.splitter : (motive : Lean.Grind.CommRing.Poly → Sort u_1) →
  (p : Lean.Grind.CommRing.Poly) →
    ((k : ℤ) → motive (Lean.Grind.CommRing.Poly.num k)) →
      ((k : ℤ) →
          (m : Lean.Grind.CommRing.Mon) →
            (p : Lean.Grind.CommRing.Poly) → motive (Lean.Grind.CommRing.Poly.add k m p)) →
        motive p
-- Mathlib.Algebra.Category.AlgCat.Basic
CategoryTheory.Iso.toAlgEquiv_apply : ∀ {R : Type u} [inst : CommRing R] {X Y : AlgCat R} (i : X ≅ Y) (a : ↑X),
  i.toAlgEquiv a = (CategoryTheory.ConcreteCategory.hom i.hom) a
-- Mathlib.AlgebraicGeometry.StructureSheaf
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.toOpenₗ_germ : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
  (hx : x ∈ U),
  CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (AlgebraicGeometry.StructureSheaf.toOpenₗ R M U))
      ((AlgebraicGeometry.structurePresheafInModuleCat R M).germ U x hx) =
    AlgebraicGeometry.StructureSheaf.toStalkₗ'✝ R M x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- Functorially transform a `CatCommSqOver F G X` by whiskering it with a
`CatCospanTransform`.  -/
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor A B} →
              {G : CategoryTheory.Functor C B} →
                {A₁ : Type u₄} →
                  {B₁ : Type u₅} →
                    {C₁ : Type u₆} →
                      [inst_3 : CategoryTheory.Category.{v₄, u₄} A₁] →
                        [inst_4 : CategoryTheory.Category.{v₅, u₅} B₁] →
                          [inst_5 : CategoryTheory.Category.{v₆, u₆} C₁] →
                            {F₁ : CategoryTheory.Functor A₁ B₁} →
                              {G₁ : CategoryTheory.Functor C₁ B₁} →
                                (X : Type u₇) →
                                  [inst_6 : CategoryTheory.Category.{v₇, u₇} X] →
                                    CategoryTheory.Functor (CategoryTheory.Limits.CatCospanTransform F G F₁ G₁)
                                      (CategoryTheory.Functor
                                        (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X)
                                        (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F₁ G₁ X))
-- Mathlib.RepresentationTheory.Continuous.TopRep
_private.Mathlib.RepresentationTheory.Continuous.TopRep.0.TopRep.mk.sizeOf_spec : ∀ {k : Type u} {G : Type v} [inst : Ring k] [inst_1 : TopologicalSpace k] [inst_2 : Monoid G] [inst_3 : SizeOf k]
  [inst_4 : SizeOf G] (V : Type w) [hV1 : AddCommGroup V] [hV2 : Module k V] [hV3 : TopologicalSpace V]
  [hV4 : IsTopologicalAddGroup V] [hV5 : ContinuousSMul k V] (ρ : ContRepresentation k G V),
  sizeOf { V := V, hV1 := hV1, hV2 := hV2, hV3 := hV3, hV4 := hV4, hV5 := hV5, ρ := ρ } =
    1 + sizeOf V + sizeOf hV1 + sizeOf hV2 + sizeOf hV3 + sizeOf hV4 + sizeOf hV5 + sizeOf ρ
-- Mathlib.Algebra.Group.ULift
ULift.addRightCancelMonoid.eq_1 : ∀ {α : Type u} [inst : AddRightCancelMonoid α],
  ULift.addRightCancelMonoid = Function.Injective.addRightCancelMonoid ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (self : AlgebraicGeometry.SheafedSpace C),
  AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace.obj self = self.toPresheafedSpace
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instAddCommGroup : {R : Type u_3} → {A : Type u_4} → [AddCommGroup R] → [AddCommGroup A] → AddCommGroup (Unitization R A)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
vectorSpan_prod_eq : ∀ {k : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : AddCommGroup W] [inst_5 : Module k W]
  [inst_6 : AddTorsor W Q] {s : Set P} {t : Set Q},
  s.Nonempty → t.Nonempty → vectorSpan k (s ×ˢ t) = (vectorSpan k s).prod (vectorSpan k t)
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Closeds.continuous_closure : ∀ {α : Type u_1} [inst : UniformSpace α], Continuous TopologicalSpace.Closeds.closure
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_neg' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIocMod hp (-a) b = p - toIcoMod hp a (-b)
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.AttrKind.unfold.sizeOf_spec : sizeOf Lean.Meta.Grind.AttrKind.unfold = 1
-- Mathlib.Computability.EpsilonNFA
εNFA.mem_εClosure_iff_exists_path : ∀ {α : Type u} {σ : Type v} (M : εNFA α σ) {s₁ s₂ : σ},
  s₂ ∈ M.εClosure {s₁} ↔ ∃ n, M.IsPath s₁ s₂ (List.replicate n none)
-- Mathlib.CategoryTheory.Shift.Localization
CategoryTheory.LocalizerMorphism.commShift_iso_inv_app_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) {M : Type u_3}
  [inst_2 : AddMonoid M] [inst_3 : CategoryTheory.HasShift C₁ M] [inst_4 : CategoryTheory.HasShift C₂ M]
  [inst_5 : Φ.functor.CommShift M] {D₁ : Type u_4} {D₂ : Type u_5} [inst_6 : CategoryTheory.Category.{v_3, u_4} D₁]
  [inst_7 : CategoryTheory.Category.{v_4, u_5} D₂] (L₁ : CategoryTheory.Functor C₁ D₁) [inst_8 : L₁.IsLocalization W₁]
  (L₂ : CategoryTheory.Functor C₂ D₂) [inst_9 : CategoryTheory.HasShift D₁ M] [inst_10 : CategoryTheory.HasShift D₂ M]
  [inst_11 : L₁.CommShift M] [inst_12 : L₂.CommShift M] (G : CategoryTheory.Functor D₁ D₂)
  (e : Φ.functor.comp L₂ ≅ L₁.comp G) (m : M) (X : C₁) {Z : D₂}
  (h : G.obj ((CategoryTheory.shiftFunctor D₁ m).obj (L₁.obj X)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso G m).inv.app (L₁.obj X)) h =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D₂ m).map (e.inv.app X))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso L₂ m).inv.app (Φ.functor.obj X))
        (CategoryTheory.CategoryStruct.comp (L₂.map ((CategoryTheory.Functor.commShiftIso Φ.functor m).inv.app X))
          (CategoryTheory.CategoryStruct.comp (e.hom.app ((CategoryTheory.shiftFunctor C₁ m).obj X))
            (CategoryTheory.CategoryStruct.comp (G.map ((CategoryTheory.Functor.commShiftIso L₁ m).hom.app X)) h))))
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey!_modify_eq_maxKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst : Inhabited α], t.WF → ∀ {k : α} {f : β → β}, (t.modify k f).maxKey! = t.maxKey!
-- Std.Data.DTreeMap.Internal.Operations
/-- Builds the tree `l ++ r` without any balancing information at the root.  -/
Std.DTreeMap.Internal.Impl.link2 : {α : Type u} →
  {β : α → Type v} →
    (l r : Std.DTreeMap.Internal.Impl α β) →
      l.Balanced → r.Balanced → Std.DTreeMap.Internal.Impl.Tree α β (l.size + r.size)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.continue : Lean.Syntax → Lean.Elab.Term.Do.Code
-- Mathlib.Combinatorics.Additive.Corner.Defs
IsCorner.fst_snd_mem : ∀ {G : Type u_1} [inst : AddCommMonoid G] {A : Set (G × G)} {x₁ y₁ x₂ y₂ : G}, IsCorner A x₁ y₁ x₂ y₂ → (x₁, y₂) ∈ A
-- Init.Notation
/-- The standardized "low" priority `low = 100`, for things that should be lower than default priority.  -/
prioLow : Lean.ParserDescr
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instCancelMonoid : {α : Type u_1} → [CancelMonoid α] → CancelMonoid (Colex α)
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.RelabelNat.State.Inv1.below.empty : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α]
  {motive : (a : ℕ) → (a_1 : Std.HashMap α ℕ) → Std.Sat.AIG.RelabelNat.State.Inv1 a a_1 → Prop},
  Std.Sat.AIG.RelabelNat.State.Inv1.below ⋯
-- Mathlib.Combinatorics.SimpleGraph.Density
Rel.edgeDensity.eq_1 : ∀ {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [inst : (a : α) → DecidablePred (r a)] (s : Finset α) (t : Finset β),
  Rel.edgeDensity r s t = ↑(Rel.interedges r s t).card / (↑s.card * ↑t.card)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_eq_cfcₙ_iff_eqOn : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] {f g : R → R} {a : A},
  autoParam (p a) cfcₙ_eq_cfcₙ_iff_eqOn._auto_1 →
    autoParam (ContinuousOn f (quasispectrum R a)) cfcₙ_eq_cfcₙ_iff_eqOn._auto_3 →
      autoParam (f 0 = 0) cfcₙ_eq_cfcₙ_iff_eqOn._auto_5 →
        autoParam (ContinuousOn g (quasispectrum R a)) cfcₙ_eq_cfcₙ_iff_eqOn._auto_7 →
          autoParam (g 0 = 0) cfcₙ_eq_cfcₙ_iff_eqOn._auto_9 → (cfcₙ f a = cfcₙ g a ↔ Set.EqOn f g (quasispectrum R a))
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.maxGenEigenspace_eq_maxGenEigenspace_zero : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : Module.End R M)
  (μ : R), f.maxGenEigenspace μ = (f - μ • 1).maxGenEigenspace 0
-- Mathlib.Algebra.Torsor.Defs
/-- Multiplying a group element with a point, then dividing by another point,
produces the same result as dividing the points then multiplying the group element.  -/
smul_sdiv_assoc : ∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [T : Torsor G P] (g : G) (p₁ p₂ : P), g • p₁ /ₛ p₂ = g * (p₁ /ₛ p₂)
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.instSub : (A : Type u_3) → (E : Type u_4) → [Sub E] → Sub (WithCStarModule A E)
-- Mathlib.Tactic.Module
_private.Mathlib.Tactic.Module.0.Mathlib.Tactic.Module.qNF.mkAddProof.eq_def : ∀ {u v : Lean.Level} {M : Q(Type v)} {R : Q(Type u)} {iR : Q(Semiring «$R»)} {iM : Q(AddCommMonoid «$M»)}
  (iRM : Q(Module «$R» «$M»)) (l₁ l₂ : Mathlib.Tactic.Module.qNF R M),
  Mathlib.Tactic.Module.qNF.mkAddProof iRM l₁ l₂ =
    match l₁, l₂ with
    | [], l =>
      have a := l.toNF;
      q(⋯)
    | l, [] =>
      have a := l.toNF;
      q(⋯)
    | ((a₁, x₁), k₁) :: t₁, ((a₂, x₂), k₂) :: t₂ =>
      if k₁ < k₂ then
        have pf := Mathlib.Tactic.Module.qNF.mkAddProof iRM t₁ (((a₂, x₂), k₂) ::ᵣ t₂);
        q(⋯)
      else
        if k₁ = k₂ then
          have pf := Mathlib.Tactic.Module.qNF.mkAddProof iRM t₁ t₂;
          q(⋯)
        else
          have pf := Mathlib.Tactic.Module.qNF.mkAddProof iRM (((a₁, x₁), k₁) ::ᵣ t₁) t₂;
          q(⋯)
-- Std.Async.System
Std.Async.System.CPUTimes.mk.inj : ∀
  {userTime niceTime systemTime idleTime interruptTime userTime_1 niceTime_1 systemTime_1 idleTime_1 interruptTime_1 :
    Std.Time.Millisecond.Offset},
  { userTime := userTime, niceTime := niceTime, systemTime := systemTime, idleTime := idleTime,
        interruptTime := interruptTime } =
      { userTime := userTime_1, niceTime := niceTime_1, systemTime := systemTime_1, idleTime := idleTime_1,
        interruptTime := interruptTime_1 } →
    userTime = userTime_1 ∧
      niceTime = niceTime_1 ∧ systemTime = systemTime_1 ∧ idleTime = idleTime_1 ∧ interruptTime = interruptTime_1
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- `C` has all limits of size `v₁ u₁` (`HasLimitsOfSize.{v₁ u₁} C`)
if it has limits of every shape `J : Type u₁` with `[Category.{v₁} J]`.
 -/
CategoryTheory.Limits.HasLimitsOfSize : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} {l : List α} {k : α} {fallback : Unit},
  (Std.TreeMap.unitOfList l cmp).getD k fallback = ()
-- Mathlib.Topology.UniformSpace.Pi
Pi.uniformContinuous_postcomp : ∀ {ι : Type u_1} {β : Type u_3} [inst : UniformSpace β] {α : Type u_4} [inst_1 : UniformSpace α] {g : α → β},
  UniformContinuous g → UniformContinuous fun x => g ∘ x
-- Mathlib.Analysis.Normed.Operator.Mul
/-- Scalar multiplication as a continuous bilinear map.  -/
ContinuousLinearMap.lsmul : (𝕜 : Type u_1) →
  {E : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          (R : Type u_3) →
            [inst_3 : SeminormedRing R] →
              [inst_4 : NormedAlgebra 𝕜 R] →
                [inst_5 : Module R E] → [IsBoundedSMul R E] → [IsScalarTower 𝕜 R E] → R →L[𝕜] E →L[𝕜] E
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.ContinuousMulEquiv.toProfiniteGrpIso.eq_1 : ∀ {X Y : ProfiniteGrp.{u_1}} (e : ↑X.toProfinite.toTop ≃ₜ* ↑Y.toProfinite.toTop),
  ProfiniteGrp.ContinuousMulEquiv.toProfiniteGrpIso e =
    { hom := ProfiniteGrp.ofHom ↑e, inv := ProfiniteGrp.ofHom ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.Data.List.Lattice
List.inter_cons_of_notMem : ∀ {α : Type u_1} {l₂ : List α} {a : α} [inst : DecidableEq α] (l₁ : List α), a ∉ l₂ → (a :: l₁) ∩ l₂ = l₁ ∩ l₂
-- Mathlib.Data.Holor
Holor.CPRankMax.below.zero : ∀ {α : Type} [inst : Mul α] [inst_1 : AddMonoid α]
  {motive : (a : ℕ) → {ds : List ℕ} → (a_1 : Holor α ds) → Holor.CPRankMax a a_1 → Prop} {ds : List ℕ},
  Holor.CPRankMax.below ⋯
-- Mathlib.Data.Real.Basic
Real.linearOrder : LinearOrder ℝ
-- Mathlib.Order.BoundedOrder.Basic
Pi.bot_apply : ∀ {ι : Type u_1} {α' : ι → Type u_2} [inst : (i : ι) → Bot (α' i)] (i : ι), ⊥ i = ⊥
-- Plausible.Shrinkable
Plausible.Sigma.shrinkable : {α : Type u_1} →
  {β : Type u_2} →
    [shrA : Plausible.Shrinkable α] → [shrB : Plausible.Shrinkable β] → Plausible.Shrinkable ((_ : α) × β)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.app : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} → CategoryTheory.Oplax.StrongTrans F G → (a : B) → F.obj a ⟶ G.obj a
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.instAddCommMonoid : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → AddCommMonoid (AddMonoidAlgebra R M)
-- Mathlib.CategoryTheory.Monad.Limits
/-- (Impl) Prove that the lifted cocone is colimiting.  -/
CategoryTheory.Comonad.ForgetCreatesColimits'.liftedCoconeIsColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} J] →
        {T : CategoryTheory.Comonad C} →
          (D : CategoryTheory.Functor J T.Coalgebra) →
            (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) →
              (t : CategoryTheory.Limits.IsColimit c) →
                CategoryTheory.Limits.IsColimit (CategoryTheory.Comonad.ForgetCreatesColimits'.liftedCocone D c t)
-- Std.Data.HashSet.Basic
/-- Partition a hashset into two hashsets based on a predicate.  -/
Std.HashSet.partition : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → (α → Bool) → Std.HashSet α → Std.HashSet α × Std.HashSet α
-- Mathlib.SetTheory.Ordinal.Basic
/-- The order isomorphism between ordinals less than `o` and `o.ToType`.  -/
Ordinal.ToType.mk : {o : Ordinal.{u_1}} → ↑(Set.Iio o) ≃o o.ToType
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.liftAlgEquiv_apply : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {E : IntermediateField K L}
  (F : IntermediateField K ↥E) (x : ↥F), ↑((IntermediateField.liftAlgEquiv F) x) = ↑↑x
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.comp_add_right : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] {f : ℝ → ε} {a b : ℝ}
  [TopologicalSpace.PseudoMetrizableSpace ε],
  IntervalIntegrable f MeasureTheory.volume a b →
    ∀ (c : ℝ),
      autoParam (‖f (min a b)‖ₑ ≠ ⊤) IntervalIntegrable.comp_add_right._auto_1 →
        IntervalIntegrable (fun x => f (x + c)) MeasureTheory.volume (a - c) (b - c)
-- Mathlib.Order.RelIso.Basic
RelIso.rel_symm_apply : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) {x : α} {y : β},
  r x (e.symm y) ↔ s (e x) y
-- Init.Data.SInt.Bitwise
instAssociativeInt16HOr : Std.Associative fun x1 x2 => x1 ||| x2
-- Mathlib.Algebra.Module.Equiv.Basic
/-- Left multiplication by a unit of a semiring as a linear equivalence.  -/
Units.mulLeftLinearEquiv : (R : Type u_9) →
  (A : Type u_10) →
    [inst : Semiring R] → [inst_1 : Semiring A] → [inst_2 : Module R A] → [SMulCommClass R A A] → Aˣ →* A ≃ₗ[R] A
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.not_real_of_infinitesimal_ne_zero : ∀ (x : ℝ*), x.Infinitesimal → x ≠ 0 → ∀ (r : ℝ), x ≠ ↑r
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.archimedeanClassOrderIso_symm_apply : ∀ {M : Type u_2} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] (m : M) (s : ℕ+),
  (DivisibleHull.archimedeanClassOrderIso M).symm (ArchimedeanClass.mk (DivisibleHull.mk m s)) = ArchimedeanClass.mk m
-- Mathlib.Algebra.Opposites
AddOpposite.opEquiv_symm_apply : ∀ {α : Type u_1}, ⇑AddOpposite.opEquiv.symm = AddOpposite.unop
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roc_eq_cons_iff : ∀ {xs : List ℕ} {m n a : ℕ}, (m<...=n).toList = a :: xs ↔ m + 1 = a ∧ m < n ∧ ((m + 1)<...=n).toList = xs
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.indepSet_empty_left : ∀ {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsZeroOrProbabilityMeasure μ]
  (s : Set Ω), ProbabilityTheory.IndepSet ∅ s μ
-- Mathlib.LinearAlgebra.Matrix.Basis
Module.Basis.toMatrix_update : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (e : Module.Basis ι R M) (v : ι' → M) (j : ι') [inst_3 : DecidableEq ι'] (x : M),
  e.toMatrix (Function.update v j x) = (e.toMatrix v).updateCol j ⇑(e.repr x)
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.toList_prod : ∀ {α : Type u_1} (xs : List (FreeMonoid α)), FreeMonoid.toList xs.prod = (List.map (⇑FreeMonoid.toList) xs).flatten
-- Lean.Data.NameMap.Basic
Lean.NameSSet : Type
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.not_mem_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₁ → k ∉ t₁ ∩ t₂
-- Mathlib.Topology.Instances.Discrete
OrderTopology.of_discreteTopology : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [PredOrder α] [SuccOrder α] [DiscreteTopology α],
  OrderTopology α
-- Lean.Widget.Commands
Lean.Widget.elabShowPanelWidgetsCmd : Lean.Elab.Command.CommandElab
-- Mathlib.CategoryTheory.EssentialImage
CategoryTheory.Functor.essImage.liftFunctor_map : ∀ {J : Type u_1} {C : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  (G : CategoryTheory.Functor J D) (F : CategoryTheory.Functor C D) [inst_3 : F.Full] [inst_4 : F.Faithful]
  (hG : ∀ (j : J), F.essImage (G.obj j)) {i j : J} (f : i ⟶ j),
  (CategoryTheory.Functor.essImage.liftFunctor G F hG).map f =
    F.preimage
      (CategoryTheory.CategoryStruct.comp (F.toEssImage.objObjPreimageIso { obj := G.obj i, property := ⋯ }).hom.hom
        (CategoryTheory.CategoryStruct.comp (G.map f)
          (F.toEssImage.objObjPreimageIso { obj := G.obj j, property := ⋯ }).inv.hom))
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- A class asserting the existence of a right adjoint.  -/
CategoryTheory.Functor.IsLeftAdjoint : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Init.Core
iff_iff_eq : ∀ {a b : Prop}, (a ↔ b) ↔ a = b