mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SolverTerms.next.injEq : ∀ (solverId : ℕ) (e : Lean.Expr) (rest : Lean.Meta.Grind.SolverTerms) (solverId_1 : ℕ) (e_1 : Lean.Expr)
  (rest_1 : Lean.Meta.Grind.SolverTerms),
  (Lean.Meta.Grind.SolverTerms.next solverId e rest = Lean.Meta.Grind.SolverTerms.next solverId_1 e_1 rest_1) =
    (solverId = solverId_1 ∧ e = e_1 ∧ rest = rest_1)
-- Aesop.Tree.TreeM
Aesop.Tree.numRapps : Aesop.Tree → ℕ
-- Mathlib.Analysis.InnerProductSpace.Positive
ContinuousLinearMap.isPositive_iff_complex : ∀ {E' : Type u_4} [inst : NormedAddCommGroup E'] [inst_1 : InnerProductSpace ℂ E'] (T : E' →L[ℂ] E'),
  T.IsPositive ↔ ∀ (x : E'), ↑(RCLike.re (inner ℂ (T x) x)) = inner ℂ (T x) x ∧ 0 ≤ RCLike.re (inner ℂ (T x) x)
-- Std.Time.DateTime
/-- Add `Year.Offset` to a `DateTime`, clipping to the last valid day.
 -/
Std.Time.DateTime.addYearsClip : Std.Time.DateTime → Std.Time.Year.Offset → Std.Time.DateTime
-- Mathlib.CategoryTheory.Retract
CategoryTheory.Retract.splitEpi_section_ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Retract X Y),
  h.splitEpi.section_ = h.i
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
NumberField.Units.finrank_eq_rank : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  Module.finrank ℝ (NumberField.Units.dirichletUnitTheorem.logSpace K) = NumberField.Units.rank K
-- Mathlib.Logic.Equiv.Sum
Equiv.sumComm_apply : ∀ (α : Type u_9) (β : Type u_10), ⇑(Equiv.sumComm α β) = Sum.swap
-- Mathlib.Tactic.NormNum.Result
/-- The result is `lit : ℕ` (a raw nat literal) and `proof : isNat x lit`.  -/
Mathlib.Meta.NormNum.Result.isNat : {u : Lean.Level} →
  {α : Q(Type u)} →
    {x : Q(«$α»)} →
      (inst : autoParam Q(AddMonoidWithOne «$α») Mathlib.Meta.NormNum.Result.isNat._auto_1) →
        (lit : Q(ℕ)) → Q(Mathlib.Meta.NormNum.IsNat «$x» «$lit») → Mathlib.Meta.NormNum.Result x
-- Mathlib.Order.OmegaCompletePartialOrder
Part.eq_of_chain : ∀ {α : Type u_2} {c : OmegaCompletePartialOrder.Chain (Part α)} {a b : α}, Part.some a ∈ c → Part.some b ∈ c → a = b
-- Lean.Parser.Command
Lean.Parser.Command.ctor.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.PartialSups
partialSups_le : ∀ {α : Type u_1} {ι : Type u_3} [inst : SemilatticeSup α] [inst_1 : Preorder ι] [inst_2 : LocallyFiniteOrderBot ι]
  (f : ι → α) (i : ι) (a : α), (∀ j ≤ i, f j ≤ a) → (partialSups f) i ≤ a
-- Mathlib.Algebra.Homology.TotalComplexSymmetry
HomologicalComplex₂.totalFlipIso_hom_f_D₂_assoc : ∀ {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Preadditive C] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  (K : HomologicalComplex₂ C c₁ c₂) (c : ComplexShape J) [inst_2 : TotalComplexShape c₁ c₂ c]
  [inst_3 : TotalComplexShape c₂ c₁ c] [inst_4 : TotalComplexShapeSymmetry c₁ c₂ c] [inst_5 : K.HasTotal c]
  [inst_6 : DecidableEq J] (j j' : J) {Z : C} (h : K.toGradedObject.mapObj (c₁.π c₂ c) j' ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((K.totalFlipIso c).hom.f j) (CategoryTheory.CategoryStruct.comp (K.D₂ c j j') h) =
    CategoryTheory.CategoryStruct.comp (K.flip.D₁ c j j')
      (CategoryTheory.CategoryStruct.comp ((K.totalFlipIso c).hom.f j') h)
-- Mathlib.Control.ULift
PLift.instMonad_mathlib : Monad PLift
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKeyD_eq_fallback : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {a fallback : α}, m.contains a = false → m.getKeyD a fallback = fallback
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeft_map_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {L₁ L₂ : CategoryTheory.Functor A T} (l : L₁ ⟶ L₂)
  (hl :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L₂ R P Q W),
      P (CategoryTheory.CategoryStruct.comp (l.app X.left) X.hom))
  {X Y : CategoryTheory.MorphismProperty.Comma L₂ R P Q W} (f : X ⟶ Y),
  ((CategoryTheory.MorphismProperty.Comma.mapLeft R l hl).map f).left =
    (CategoryTheory.MorphismProperty.Comma.Hom.hom f).left
-- Mathlib.Probability.Moments.ComplexMGF
/-- If the complex moment-generating functions of two random variables `X` and `Y` with respect to
the finite measures `μ`, `μ'`, respectively, coincide, then `μ.map X = μ'.map Y`. In other words,
complex moment-generating functions separate the distributions of random variables.  -/
MeasureTheory.Measure.ext_of_complexMGF_eq : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {Ω' : Type u_3}
  {mΩ' : MeasurableSpace Ω'} {Y : Ω' → ℝ} {μ' : MeasureTheory.Measure Ω'} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure μ'],
  AEMeasurable X μ →
    AEMeasurable Y μ' →
      ProbabilityTheory.complexMGF X μ = ProbabilityTheory.complexMGF Y μ' →
        MeasureTheory.Measure.map X μ = MeasureTheory.Measure.map Y μ'
-- Lean.Compiler.InitAttr
Lean.getInitFnNameFor? : Lean.Environment → Lean.Name → Option Lean.Name
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.mapTrifunctor_map_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) (I₁ : Type u_7)
  (I₂ : Type u_8) (I₃ : Type u_9) {X₁ Y₁ : CategoryTheory.GradedObject I₁ C₁} (φ : X₁ ⟶ Y₁)
  (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) (x : I₁ × I₂ × I₃),
  (((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).map φ).app X₂).app X₃ x =
    ((F.map (φ x.1)).app (X₂ x.2.1)).app (X₃ x.2.2)
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.measurePreserving_piFinSuccAbove : ∀ {n : ℕ} {α : Fin (n + 1) → Type u} {m : (i : Fin (n + 1)) → MeasurableSpace (α i)}
  (μ : (i : Fin (n + 1)) → MeasureTheory.Measure (α i)) [∀ (i : Fin (n + 1)), MeasureTheory.SigmaFinite (μ i)]
  (i : Fin (n + 1)),
  MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.piFinSuccAbove α i)) (MeasureTheory.Measure.pi μ)
    ((μ i).prod (MeasureTheory.Measure.pi fun j => μ (i.succAbove j)))
-- Mathlib.Data.Finsupp.Single
Finsupp.erase_update_eq_erase : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (f : α →₀ M) (a : α) (b : M),
  Finsupp.erase a (f.update a b) = Finsupp.erase a f
-- Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Mathlib.Tactic.Monoidal.naturality_rightUnitor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {p f pf : C}
  (η_f : CategoryTheory.MonoidalCategoryStruct.tensorObj p f ≅ pf),
  CategoryTheory.MonoidalCategory.whiskerLeftIso p (CategoryTheory.MonoidalCategoryStruct.rightUnitor f) ≪≫ η_f =
    Mathlib.Tactic.Monoidal.normalizeIsoComp η_f (CategoryTheory.MonoidalCategoryStruct.rightUnitor pf)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
contravariant_lt_of_contravariant_le : ∀ (M : Type u_1) (N : Type u_2) (μ : M → N → N) [inst : PartialOrder N],
  (Contravariant M N μ fun x1 x2 => x1 ≤ x2) → Contravariant M N μ fun x1 x2 => x1 < x2
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure
CategoryTheory.ObjectProperty.isStableUnderRetracts_colimitsCardinalClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) (κ : Cardinal.{w})
  [Fact κ.IsRegular], (P.colimitsCardinalClosure κ).IsStableUnderRetracts
-- Mathlib.Algebra.Star.MonoidHom
StarMulEquiv.apply_symm_apply : ∀ {A : Type u_2} {B : Type u_3} [inst : Mul A] [inst_1 : Mul B] [inst_2 : Star A] [inst_3 : Star B] (e : A ≃⋆* B)
  (x : B), e (e.symm x) = x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.cocone_inl : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P} (h : CategoryTheory.IsPushout f g inl inr), h.cocone.inl = inl
-- Lean.Meta.Tactic.Split
/-- Throws an error with message `msg` with a hint that a foreign metaprogram may be misusing `split` internals.  -/
_private.Lean.Meta.Tactic.Split.0.Lean.Meta.Split.throwInternalMisuseError : {m : Type → Type} → {α : Type} → [Monad m] → [Lean.MonadError m] → Lean.MessageData → m α
-- Batteries.Recycling.RBTree.Basic
/-- Every path from the root to a leaf must pass through the same number of black nodes.  -/
RBTree.RBColor.black : RBTree.RBColor
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
/-- The image of `IsFractionRing.liftAlgHom` is the intermediate field generated by the image
of the algebra hom.  -/
IsFractionRing.liftAlgHom_fieldRange : ∀ {F : Type u_1} {A : Type u_2} {K : Type u_3} {L : Type u_4} [inst : Field F] [inst_1 : CommRing A]
  [inst_2 : Algebra F A] [inst_3 : Field K] [inst_4 : Algebra F K] [inst_5 : Algebra A K] [inst_6 : IsFractionRing A K]
  [inst_7 : Field L] [inst_8 : Algebra F L] {g : A →ₐ[F] L} [inst_9 : IsScalarTower F A K] (hg : Function.Injective ⇑g),
  (IsFractionRing.liftAlgHom hg).fieldRange = IntermediateField.adjoin F ↑g.range
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.mk.congr_simp : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}}
  {D : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ} {e : J}
  (prop_id : D.W (CategoryTheory.CategoryStruct.id e)) (lift lift_1 : {j : J} → D.P j → (j ⟶ e))
  (e_lift : lift = lift_1) (hlift : ∀ {j : J} (hj : D.P j), D.W (lift hj))
  (uniq : ∀ {j : J} (hj : D.P j) {φ : j ⟶ e}, D.W φ → lift hj = φ)
  (comm : ∀ {i j : J} (f : i ⟶ j) (hf : D.W f), CategoryTheory.CategoryStruct.comp f (lift ⋯) = lift ⋯),
  { prop_id := prop_id, lift := lift, hlift := hlift, uniq := uniq, comm := comm } =
    { prop_id := prop_id, lift := lift_1, hlift := ⋯, uniq := ⋯, comm := ⋯ }
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.List.filter.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.HasPullbacksOfInclusions.hasPullbackInr' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  [CategoryTheory.HasPullbacksOfInclusions C] {X Y Z : C} (f : Z ⟶ X ⨿ Y),
  CategoryTheory.Limits.HasPullback f CategoryTheory.Limits.coprod.inr
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.toFinset_insert' : ∀ {α : Type u} [inst : DecidableEq α] {a : α} {s : Set α} (hs : s.Finite), ⋯.toFinset = insert a hs.toFinset
-- Mathlib.Algebra.Group.Action.Defs
smul_inv : ∀ {G : Type u_3} {H : Type u_4} [inst : Group G] [inst_1 : Group H] [inst_2 : MulAction G H] [SMulCommClass G H H]
  [IsScalarTower G H H] (g : G) (a : H), (g • a)⁻¹ = g⁻¹ • a⁻¹
-- Mathlib.Analysis.InnerProductSpace.Reproducing
/-- The kernel functions of a reproducing kernel Hilbert space are the adjoint of
the point evaluation.  -/
RKHS.kerFun : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {X : Type u_2} →
      {V : Type u_3} →
        [inst_1 : NormedAddCommGroup V] →
          [inst_2 : InnerProductSpace 𝕜 V] →
            (H : Type u_4) →
              [inst_3 : NormedAddCommGroup H] →
                [inst_4 : InnerProductSpace 𝕜 H] →
                  [RKHS 𝕜 H X V] → [CompleteSpace H] → [CompleteSpace V] → X → V →L[𝕜] H
-- Mathlib.Algebra.Group.AddChar
/-- The underlying function.

Do not use this function directly. Instead use the coercion coming from the `FunLike`
instance.  -/
AddChar.toFun : {A : Type u_1} → [inst : AddMonoid A] → {M : Type u_2} → [inst_1 : Monoid M] → AddChar A M → A → M
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Compacts.isClosedEmbedding_toCloseds : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : T2Space α] [CompleteSpace α],
  Topology.IsClosedEmbedding TopologicalSpace.Compacts.toCloseds
-- Mathlib.Data.Nat.Digits.Lemmas
_private.Mathlib.Data.Nat.Digits.Lemmas.0.Nat.digitsAppend.eq_1 : ∀ (b l n : ℕ), b.digitsAppend l n = b.digits n ++ List.replicate (l - (b.digits n).length) 0
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- Restriction of a vector measure onto a sub-σ-algebra.  -/
MeasureTheory.VectorMeasure.trim : {α : Type u_1} →
  {M : Type u_4} →
    [inst : AddCommMonoid M] →
      [inst_1 : TopologicalSpace M] →
        {m n : MeasurableSpace α} → MeasureTheory.VectorMeasure α M → m ≤ n → MeasureTheory.VectorMeasure α M
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKeyD_insertIfNew_le_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β}
  {fallback : α}, (cmp ((t.insertIfNew k v).minKeyD fallback) k).isLE = true
-- Mathlib.Data.Num.Lemmas
PosNum.bit0_of_bit0 : ∀ (n : PosNum), n + n = n.bit0
-- Mathlib.FieldTheory.RatFunc.Luroth
/-- The height of `generator E`.  -/
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.m : {K : Type u_1} → [inst : Field K] → IntermediateField K (RatFunc K) → ℕ
-- Mathlib.LinearAlgebra.TensorProduct.Pi
_private.Mathlib.LinearAlgebra.TensorProduct.Pi.0.TensorProduct.piRightInv_single : ∀ (R : Type u_1) [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (N : Type u_3)
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : Module S N] [inst_6 : IsScalarTower R S N] {ι : Type u_4}
  (M : ι → Type u_5) [inst_7 : (i : ι) → AddCommMonoid (M i)] [inst_8 : (i : ι) → Module R (M i)] [inst_9 : Fintype ι]
  [inst_10 : DecidableEq ι] (x : N) (i : ι) (m : M i),
  (TensorProduct.piRightInv R S N M) (Pi.single i (x ⊗ₜ[R] m)) = x ⊗ₜ[R] Pi.single i m
-- Init.Data.String.Basic
String.Slice.Pos.toSlice_ofToSlice : ∀ {s : String} (pos : s.toSlice.Pos), (String.Pos.ofToSlice pos).toSlice = pos
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.isAdjointPair_zero : ∀ {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} {M₃ : Type u_8} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] [inst_5 : AddCommMonoid M₃]
  [inst_6 : Module R M₃] {I : R →+* R} {B : M →ₗ[R] M →ₛₗ[I] M₃} {B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃}, B.IsAdjointPair B' 0 0
-- Mathlib.CategoryTheory.Action.Continuous
CategoryTheory.Equivalence.mapContAction_functor : ∀ {V : Type u_5} {W : Type u_6} [inst : CategoryTheory.Category.{v_2, u_5} V] {FV : V → V → Type u_7}
  {CV : V → Type u_8} [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
  [inst_2 : CategoryTheory.ConcreteCategory V FV] [inst_3 : CategoryTheory.HasForget₂ V TopCat]
  [inst_4 : CategoryTheory.Category.{v_3, u_6} W] {FW : W → W → Type u_9} {CW : W → Type u_10}
  [inst_5 : (X Y : W) → FunLike (FW X Y) (CW X) (CW Y)] [inst_6 : CategoryTheory.ConcreteCategory W FW]
  [inst_7 : CategoryTheory.HasForget₂ W TopCat] (G : Type u_11) [inst_8 : Monoid G] [inst_9 : TopologicalSpace G]
  (E : V ≌ W) (H₁ : ∀ (X : ContAction V G), ((E.functor.mapAction G).obj X.obj).IsContinuous)
  (H₂ : ∀ (X : ContAction W G), ((E.inverse.mapAction G).obj X.obj).IsContinuous),
  (CategoryTheory.Equivalence.mapContAction G E H₁ H₂).functor = CategoryTheory.Functor.mapContAction G E.functor H₁
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
/-- `charFun` as the integral of a bounded continuous function.  -/
MeasureTheory.charFun_eq_integral_innerProbChar : ∀ {E : Type u_2} {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} {t : E} [inst : SeminormedAddCommGroup E]
  [inst_1 : InnerProductSpace ℝ E],
  MeasureTheory.charFun μ t = ∫ (v : E), (BoundedContinuousFunction.innerProbChar t) v ∂μ
-- Init.Data.String.Lemmas.Iterate
_private.Init.Data.String.Lemmas.Iterate.0.String.Slice.foldl.eq_1 : ∀ {α : Type u} (f : α → Char → α) (init : α) (s : String.Slice),
  String.Slice.foldl f init s = Std.Iter.fold f init s.chars
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.cokernelCoforkOfCofork_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} {f g : X ⟶ Y}
  (c : CategoryTheory.Limits.Cofork f g),
  CategoryTheory.Limits.Cofork.π (CategoryTheory.Preadditive.cokernelCoforkOfCofork c) = c.π
-- Mathlib.Lean.Json
Lean.instFromJsonFin_mathlib : {n : ℕ} → Lean.FromJson (Fin n)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Bounded.weak : ∀ {α : Type u_1} [inst : Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α}, t.Bounded o₁ o₂ → t.Bounded ⊥ ⊤
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.instInhabited.eq_1 : ∀ {α : Type u_1}, FreeMonoid.instInhabited = { default := 1 }
-- Mathlib.Data.Int.GCD
Int.gcd_greatest : ∀ {a b d : ℤ}, 0 ≤ d → d ∣ a → d ∣ b → (∀ (e : ℤ), e ∣ a → e ∣ b → e ∣ d) → d = ↑(a.gcd b)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.toLinearMapHom_apply_apply : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A ≃ₐ[R] A)
  (a : A), ((AlgEquiv.toLinearMapHom R A) x) a = x a
-- Mathlib.Order.Ideal
/-- A subset of a preorder `P` is an ideal if it is
- nonempty
- upward directed (any pair of elements in the ideal has an upper bound in the ideal)
- downward closed (any element less than an element of the ideal is in the ideal).  -/
Order.IsIdeal : {P : Type u_2} → [LE P] → Set P → Prop
-- Mathlib.Data.ENNReal.Basic
ENNReal.toNNReal_eq_toNNReal_iff : ∀ (x y : ENNReal), x.toNNReal = y.toNNReal ↔ x = y ∨ x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_smul_const : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_8} [inst : NontriviallyNormedField 𝕜]
  [CompleteSpace 𝕜] {E : Type u_9} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f : α → 𝕜} {c : E},
  c ≠ 0 → (MeasureTheory.Integrable (fun x => f x • c) μ ↔ MeasureTheory.Integrable f μ)
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Module.Basis.mk_eq_rank'' : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  {ι : Type v} (v : Module.Basis ι R M), Cardinal.mk ι = Module.rank R M
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
/-- The evaluation functors jointly reflect limits: that is, to show a cone is a limit of `F`
it suffices to show that each evaluation cone is a limit. In other words, to prove a cone is
limiting you can show it's pointwise limiting.
 -/
CategoryTheory.Limits.evaluationJointlyReflectsLimits : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} J] →
        {K : Type u₂} →
          [inst_2 : CategoryTheory.Category.{v₂, u₂} K] →
            {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} →
              (c : CategoryTheory.Limits.Cone F) →
                ((k : K) → CategoryTheory.Limits.IsLimit (((CategoryTheory.evaluation K C).obj k).mapCone c)) →
                  CategoryTheory.Limits.IsLimit c
-- Mathlib.Order.Interval.Finset.Defs
Subtype.instLocallyFiniteOrderBot.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] (p : α → Prop) [inst_1 : DecidablePred p] [inst_2 : LocallyFiniteOrderBot α],
  Subtype.instLocallyFiniteOrderBot p =
    { finsetIio := fun a => Finset.subtype p (Finset.Iio ↑a), finsetIic := fun a => Finset.subtype p (Finset.Iic ↑a),
      finset_mem_Iic := ⋯, finset_mem_Iio := ⋯ }
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instCommSemigroup : {α : Type u_1} → [CommSemigroup α] → CommSemigroup (Colex α)
-- Mathlib.Data.Set.Subsingleton
Set.nontrivial_iff_pair_subset : ∀ {α : Type u} {s : Set α}, s.Nontrivial ↔ ∃ x y, x ≠ y ∧ {x, y} ⊆ s
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
/-- Any isomorphism is an effective epi.  -/
CategoryTheory.effectiveEpiStructOfIsIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y : C} → (f : X ⟶ Y) → [CategoryTheory.IsIso f] → CategoryTheory.EffectiveEpiStruct f
-- Mathlib.Algebra.Lie.Subalgebra
LieHom.equivRangeOfInjective_apply : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {L₂ : Type w}
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (h : Function.Injective ⇑f) (x : L),
  (f.equivRangeOfInjective h) x = ⟨f x, ⋯⟩
-- Mathlib.Analysis.Normed.Group.Quotient
NormedAddGroupHom.IsQuotient.norm : ∀ {M : Type u_1} {N : Type u_2} [inst : SeminormedAddCommGroup M] [inst_1 : SeminormedAddCommGroup N]
  {f : NormedAddGroupHom M N}, f.IsQuotient → ∀ (x : M), ‖f x‖ = sInf ((fun m => ‖x + m‖) '' ↑f.ker)
-- Mathlib.Data.PFunctor.Multivariate.W
/-- Constructor of a value of `P.obj (α ::: β)` from components.
Useful to avoid complicated type annotation  -/
MvPFunctor.objAppend1 : {n : ℕ} →
  (P : MvPFunctor.{u} (n + 1)) →
    {α : TypeVec.{u} n} → {β : Type u} → (a : P.A) → (P.drop.B a).Arrow α → (P.last.B a → β) → ↑P (α ::: β)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.mem_ofFixingSubgroup_insert_iff : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {a : α}
  {s : Set ↥(SubMulAction.ofStabilizer M a)} {x : α},
  x ∈ SubMulAction.ofFixingSubgroup M (insert a ((fun x => ↑x) '' s)) ↔
    ∃ (hx : x ∈ SubMulAction.ofStabilizer M a), ⟨x, hx⟩ ∈ SubMulAction.ofFixingSubgroup (↥(MulAction.stabilizer M a)) s
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
_private.Mathlib.Combinatorics.SimpleGraph.Walk.Operations.0.SimpleGraph.Walk.drop.match_1.eq_2 : ∀ {V : Type u_1} {G : SimpleGraph V} {u : V} (motive : (v : V) → G.Walk u v → ℕ → Sort u_2) (v : V) (p : G.Walk u v)
  (h_1 : (x : ℕ) → motive u SimpleGraph.Walk.nil x) (h_2 : (v : V) → (p : G.Walk u v) → motive v p 0)
  (h_3 : (v v_1 : V) → (h : G.Adj u v_1) → (q : G.Walk v_1 v) → (n : ℕ) → motive v (SimpleGraph.Walk.cons h q) n.succ),
  (v = u → p ≍ SimpleGraph.Walk.nil → False) →
    (match v, p, 0 with
      | .(u), SimpleGraph.Walk.nil, x => h_1 x
      | v, p, 0 => h_2 v p
      | v, SimpleGraph.Walk.cons h q, n.succ => h_3 v v_1 h q n) =
      h_2 v p
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
cfcₙ_complex_eq_real : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A] [inst_3 : Module ℂ A]
  [inst_4 : IsScalarTower ℂ A A] [inst_5 : SMulCommClass ℂ A A] [T2Space A]
  [inst_7 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] {f : ℂ → ℂ} (a : A),
  (∀ x ∈ quasispectrum ℂ a, star (f x) = f x) →
    autoParam (IsSelfAdjoint a) cfcₙ_complex_eq_real._auto_1 → cfcₙ f a = cfcₙ (fun x => (f ↑x).re) a
-- Lean.Meta.Tactic.Simp.LoopProtection
Lean.Meta.Simp.linter.loopingSimpArgs : Lean.Option Bool
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Submodule.finrank_add_le_finrank_add_finrank : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (s t : Submodule K V) [FiniteDimensional K ↥s] [FiniteDimensional K ↥t],
  Module.finrank K ↥(s ⊔ t) ≤ Module.finrank K ↥s + Module.finrank K ↥t
-- Init.Grind.Order
_private.Init.Grind.Order.0.Lean.Grind.Order.add_lt_add_of_le_of_lt : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [inst_3 : Std.IsPreorder α]
  [inst_4 : Lean.Grind.Ring α] [Lean.Grind.OrderedRing α] {a b c d : α}, a ≤ b → c < d → a + c < b + d
-- Lean.Data.OpenDecl
Lean.OpenDecl.simple.injEq : ∀ (ns : Lean.Name) (except : List Lean.Name) (ns_1 : Lean.Name) (except_1 : List Lean.Name),
  (Lean.OpenDecl.simple ns except = Lean.OpenDecl.simple ns_1 except_1) = (ns = ns_1 ∧ except = except_1)