mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound
_private.Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound.0.Std.Tactic.BVDecide.LRAT.Internal.lratChecker.match_3.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : List (Std.Tactic.BVDecide.LRAT.Action β α) → Sort u_3) (id : ℕ)
  (rupHints : Array ℕ) (tail : List (Std.Tactic.BVDecide.LRAT.Action β α)) (h_1 : Unit → motive [])
  (h_2 :
    (id : ℕ) →
      (rupHints : Array ℕ) →
        (tail : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
          motive (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints :: tail))
  (h_3 :
    (id : ℕ) →
      (c : β) →
        (rupHints : Array ℕ) →
          (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
            motive (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints :: restPrf))
  (h_4 :
    (id : ℕ) →
      (c : β) →
        (pivot : Std.Sat.Literal α) →
          (rupHints : Array ℕ) →
            (ratHints : Array (ℕ × Array ℕ)) →
              (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
                motive (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints :: restPrf))
  (h_5 :
    (ids : Array ℕ) →
      (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
        motive (Std.Tactic.BVDecide.LRAT.Action.del ids :: restPrf)),
  (match Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints :: tail with
    | [] => h_1 ()
    | Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints :: tail => h_2 id rupHints tail
    | Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints :: restPrf => h_3 id c rupHints restPrf
    | Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints :: restPrf =>
      h_4 id c pivot rupHints ratHints restPrf
    | Std.Tactic.BVDecide.LRAT.Action.del ids :: restPrf => h_5 ids restPrf) =
    h_2 id rupHints tail
-- Mathlib.Topology.Algebra.Valued.WithVal
Equiv.subtypeEquivProp.eq_1 : ∀ {α : Sort u_1} {p q : α → Prop} (h : p = q), Equiv.subtypeEquivProp h = (Equiv.refl α).subtypeEquiv ⋯
-- Mathlib.Algebra.Lie.EngelSubalgebra
LieSubalgebra.engel_zero : ∀ (R : Type u_1) {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  LieSubalgebra.engel R 0 = ⊤
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.unop_iSup : ∀ {ι : Sort u_1} {M : Type u_2} [inst : AddZeroClass M] (S : ι → AddSubmonoid Mᵃᵒᵖ), (iSup S).unop = ⨆ i, (S i).unop
-- Mathlib.Order.SymmDiff
symmDiff_symmDiff_symmDiff_comm : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] (a b c d : α),
  symmDiff (symmDiff a b) (symmDiff c d) = symmDiff (symmDiff a c) (symmDiff b d)
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearMap.equivRange_symm_apply : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'}
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {F : Type u_4}
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [inst_6 : RingHomInvPair σ σ']
  [inst_7 : RingHomIsometric σ] [inst_8 : RingHomIsometric σ'] [inst_9 : CompleteSpace F] [inst_10 : CompleteSpace E]
  [inst_11 : RingHomInvPair σ' σ] {f : E →SL[σ] F} (hinj : Function.Injective ⇑f) (hclo : IsClosed (Set.range ⇑f))
  (x : E), (ContinuousLinearMap.equivRange hinj hclo).symm ⟨f x, ⋯⟩ = x
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
addMonoidAlgebraAlgEquivDirectSum_symm_apply : ∀ {ι : Type u_1} {R : Type u_2} {A : Type u_4} [inst : DecidableEq ι] [inst_1 : AddMonoid ι] [inst_2 : CommSemiring R]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : (m : A) → Decidable (m ≠ 0)],
  ⇑addMonoidAlgebraAlgEquivDirectSum.symm = DirectSum.toAddMonoidAlgebra
-- Mathlib.FieldTheory.Galois.NormalBasis
_private.Mathlib.FieldTheory.Galois.NormalBasis.0.exists_linearIndependent_algEquiv_apply_of_infinite : ∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [FiniteDimensional K L]
  [Infinite K], ∃ x, LinearIndependent K fun σ => σ x
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.filterM_eq_toIter_filterM_toIterM : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} {m : Type w → Type w'} [inst_1 : Monad m]
  [inst_2 : MonadAttach m] {f : β → m (ULift.{w, 0} Bool)}, Std.Iter.filterM f it = Std.IterM.filterM f it.toIterM
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp},
  t₁.Equiv t₂ → ∀ (f : α → β → γ), (Std.TreeMap.map f t₁).Equiv (Std.TreeMap.map f t₂)
-- Mathlib.Topology.Category.Stonean.Adjunctions
/-- The object part of the compactification functor from types to Stonean spaces.  -/
Stonean.stoneCechObj : Type u → Stonean
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.commutator_normal : ∀ {G : Type u_1} [inst : Group G] (H₁ H₂ : Subgroup G) [h₁ : H₁.Normal] [h₂ : H₂.Normal], ⁅H₁, H₂⁆.Normal
-- Mathlib.Tactic.Attr.Register
/-- Simplification procedure  -/
Parser.Attr.enat_to_nat_coe_proc : Lean.ParserDescr
-- Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
CategoryTheory.SmallObject.SuccStruct.extendToSuccObjSuccIso.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u} [inst_1 : LinearOrder J]
  [inst_2 : SuccOrder J] {j : J} (hj : ¬IsMax j) (F : CategoryTheory.Functor (↑(Set.Iic j)) C) {X : C}
  (τ : F.obj ⟨j, ⋯⟩ ⟶ X),
  CategoryTheory.SmallObject.SuccStruct.extendToSuccObjSuccIso hj F τ =
    CategoryTheory.SmallObject.SuccStruct.extendToSucc.objSuccIso hj F X
-- Lean.Meta.TryThis
Lean.Meta.Tactic.TryThis.instInhabitedSuggestionText.default : Lean.Meta.Tactic.TryThis.SuggestionText
-- Lean.Server.CodeActions.Attr
/-- Read a command code action from a declaration of the right type.  -/
Lean.CodeAction.mkCommandCodeAction : Lean.Name → Lean.ImportM Lean.CodeAction.CommandCodeAction
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
/-- A functor `F` preserves finite biproducts if it preserves biproducts of shape `J`
whenever `J` is a finite type.  -/
CategoryTheory.Limits.PreservesFiniteBiproducts : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (F : CategoryTheory.Functor C D) → [F.PreservesZeroMorphisms] → Prop
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (e : X ≅ Y) (y : ↥Y) {Z : CommRingCat} (h : Y.presheaf.stalk y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.stalkMap e.hom (e.inv y))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.stalkMap e.inv y) h) =
    CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkCongr ⋯).hom h
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftLeft
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeftConst.go.eq_def : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (input : aig.RefVec w)
  (distance curr : ℕ) (hcurr : curr ≤ w) (s : aig.RefVec curr),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeftConst.go aig input distance curr hcurr s =
    if hidx : curr < w then
      if hdist : curr < distance then
        have zeroRef := aig.mkConstCached false;
        have s := s.push zeroRef;
        Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeftConst.go aig input distance (curr + 1) ⋯ s
      else
        have s := s.push (input.get (curr - distance) ⋯);
        Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeftConst.go aig input distance (curr + 1) ⋯ s
    else
      have hcurr := ⋯;
      { aig := aig, vec := hcurr ▸ s }
-- Mathlib.CategoryTheory.Subobject.Basic
/-- The functor from subobjects of `X` to subobjects of `Y` given by
sending the subobject `S` to its "image" under `f`, usually denoted $\exists_f$.
For instance, when `C` is the category of types,
viewing `Subobject X` as `Set X` this is just `Set.image f`.

This functor is left adjoint to the `pullback f` functor (shown in `existsPullbackAdj`)
provided both are defined, and generalises the `map f` functor, again provided it is defined.
 -/
CategoryTheory.Subobject.exists : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      [CategoryTheory.Limits.HasImages C] →
        (X ⟶ Y) → CategoryTheory.Functor (CategoryTheory.Subobject X) (CategoryTheory.Subobject Y)
-- Mathlib.RingTheory.Ideal.Quotient.Basic
/-- The quotient of a commutative ring by a maximal ideal is a field.
This is a `def` rather than `instance`, since users
will have computable inverses (and `qsmul`, `ratCast`) in some applications.

See note [reducible non-instances].  -/
Ideal.Quotient.field : {R : Type u_5} → [inst : CommRing R] → (I : Ideal R) → [I.IsMaximal] → Field (R ⧸ I)
-- Mathlib.Tactic.Linter.TextBased
/-- Try parsing an `ErrorContext` from a string: return `some` if successful, `none` otherwise.
This should be the inverse of `fun ctx ↦ outputMessage ctx .exceptionsFile`
Used for, e.g., parsing the "exceptions" file.

Need to ensure (see unit tests in `MathlibTest/LintStyle.lean`) that
  `∀ (ec : ErrorContext), (parse?_errorContext <| outputMessage ec .exceptionsFile) = some ec`
 -/
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.parse?_errorContext : String → Option Mathlib.Linter.TextBased.ErrorContext✝
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.mop_tensorUnit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  { unmop := CategoryTheory.MonoidalCategoryStruct.tensorUnit C } =
    CategoryTheory.MonoidalCategoryStruct.tensorUnit Cᴹᵒᵖ
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List (α × β)} {k k' : α},
      cmp k k' = Ordering.eq →
        ∀ {v : β}, List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l → (k, v) ∈ l → (t.insertMany l)[k']? = some v
-- Init.Data.UInt.Lemmas
UInt8.lt_iff_toFin_lt : ∀ {a b : UInt8}, a < b ↔ a.toFin < b.toFin
-- Mathlib.Computability.TuringMachine.Computable
/-- type of function labels  -/
Turing.FinTM2.Λ : Turing.FinTM2 → Type
-- Lean.DocString.Extension
Lean.VersoModuleDocs.mk.sizeOf_spec : ∀ (snippets : Lean.PersistentArray Lean.VersoModuleDocs.Snippet), sizeOf { snippets := snippets } = 1 + sizeOf snippets
-- Mathlib.Analysis.Normed.Algebra.MatrixExponential
Matrix.exp_transpose : ∀ {m : Type u_1} {𝔸 : Type u_5} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : CommRing 𝔸]
  [inst_3 : TopologicalSpace 𝔸] [inst_4 : IsTopologicalRing 𝔸] [Algebra ℚ 𝔸] [T2Space 𝔸] (A : Matrix m m 𝔸),
  NormedSpace.exp A.transpose = (NormedSpace.exp A).transpose
-- Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
RootPairing.RootPositiveForm.rootLength_lt_of_pairingIn_notMem : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} [Finite ι]
  [inst_6 : CharZero R] [inst_7 : P.IsCrystallographic] [IsDomain R] (B : RootPairing.RootPositiveForm ℤ P) {i j : ι},
  P.root i ≠ P.root j → P.root i ≠ -P.root j → P.pairingIn ℤ i j ∉ {-1, 0, 1} → B.rootLength j < B.rootLength i
-- Mathlib.Order.Hom.Lattice
InfHom.dual_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Min α] [inst_1 : Min β] [inst_2 : Min γ] (g : InfHom β γ)
  (f : InfHom α β), InfHom.dual (g.comp f) = (InfHom.dual g).comp (InfHom.dual f)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.min?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.min? = t₂.min?
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_eq_none_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α], t.WF → ∀ {a : α}, Std.DTreeMap.Internal.Impl.contains a t = false → t.get? a = none
-- Mathlib.LinearAlgebra.Prod
Submodule.span_prod_eq : ∀ (R : Type u) {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] {s : Set M} {t : Set M₂},
  0 ∈ s → 0 ∈ t → Submodule.span R (s ×ˢ t) = (Submodule.span R s).prod (Submodule.span R t)
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.exp_sub : ∀ {G : Type u_5} [inst : AddGroup G] (a b : G), WithZero.exp (a - b) = WithZero.exp a / WithZero.exp b
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  {k k' : α} [hi : Inhabited β] {f : β → β},
  Std.ExtDTreeMap.Const.get! (Std.ExtDTreeMap.Const.modify t k f) k' =
    if cmp k k' = Ordering.eq then (Option.map f (Std.ExtDTreeMap.Const.get? t k)).get!
    else Std.ExtDTreeMap.Const.get! t k'
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.keys_empty : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α}, ∅.keys = []
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.filterMap_eq_filter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool},
  Std.ExtHashMap.filterMap (fun k => Option.guard fun v => f k v) m = Std.ExtHashMap.filter f m
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.val_eq_toMeasure : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (ν : MeasureTheory.FiniteMeasure Ω), ↑ν = ↑ν
-- Mathlib.Algebra.Group.Action.End
/-- The tautological action by `AddAut M` on `M`.  -/
AddAut.applyAddAction : {M : Type u_2} → [inst : AddMonoid M] → AddAction (AddAut M) M
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.instLinear : {k : Type u} →
  {G : Type v} →
    [inst : TopologicalSpace k] → [inst_1 : CommRing k] → [inst_2 : Monoid G] → CategoryTheory.Linear k (TopRep k G)
-- Std.Data.Internal.List.Associative
Std.Internal.List.isSome_minKey?_eq_not_isEmpty : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {l : List ((a : α) × β a)},
  (Std.Internal.List.minKey? l).isSome = !l.isEmpty
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.IsImage.restr_toPartialHomeomorph : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) (hs : IsOpen (e.source ∩ s)),
  (h.restr hs).toPartialHomeomorph = { toPartialEquiv := ⋯.restr, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ }
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
/-- The conditions on a spectral object indexed by `EInt` which allow
to obtain a (convergent) first quadrant `E₂` cohomological spectral sequence.  -/
CategoryTheory.Abelian.SpectralObject.IsFirstQuadrant : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → CategoryTheory.Abelian.SpectralObject C EInt → Prop
-- Std.Sync.StreamMap
/-- Filter streams based on their names
 -/
Std.StreamMap.filterByName : {α β : Type} → Std.StreamMap α β → (α → Bool) → Std.StreamMap α β
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
HasFTaylorSeriesUpTo.cont : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {f : E → F} {p : E → FormalMultilinearSeries 𝕜 E F},
  HasFTaylorSeriesUpTo n f p → ∀ (m : ℕ), ↑m ≤ n → Continuous fun x => p x m
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.lt_card_mul_inv_eq : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {K : ℝ} {A B : Finset G} {x : G},
  ↑(B * A).card < K * ↑A.card → x ∈ B⁻¹ * B → (2 - K) * ↑A.card < ↑{ab ∈ A ×ˢ A | ab.1 * ab.2⁻¹ = x}.card
-- Mathlib.Data.ENNReal.Operations
ENNReal.sub_right_inj : ∀ {a b c : ENNReal}, a ≠ ⊤ → b ≤ a → c ≤ a → (a - b = a - c ↔ b = c)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_max : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {he : t.isEmpty = false}
  {fallback : α}, t.getD (t.max he) fallback = t.max he
-- Mathlib.NumberTheory.Fermat
Nat.pairwise_coprime_fermatNumber : Pairwise fun m n => m.fermatNumber.Coprime n.fermatNumber
-- Mathlib.Analysis.Convex.Side
AffineSubspace.sSameSide_vadd_right_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P} {v : V}, v ∈ s.direction → (s.SSameSide x (v +ᵥ y) ↔ s.SSameSide x y)
-- Mathlib.CategoryTheory.Subobject.Basic
/-- An equality of subobjects gives an isomorphism of the corresponding objects.
(One could use `underlying.mapIso (eqToIso h))` here, but this is more readable.)  -/
CategoryTheory.Subobject.isoOfEq : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {B : C} →
      (X Y : CategoryTheory.Subobject B) →
        X = Y → (CategoryTheory.Subobject.underlying.obj X ≅ CategoryTheory.Subobject.underlying.obj Y)
-- Mathlib.Topology.ContinuousMap.Ordered
ContinuousMap.semilatticeSup : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : SemilatticeSup β] → [ContinuousSup β] → SemilatticeSup C(α, β)
-- Init.Data.String.Basic
String.Pos.copy_ofCopy : ∀ {s : String.Slice} {pos : s.copy.Pos}, pos.ofCopy.copy = pos
-- Mathlib.Order.WellFoundedSet
Set.Subsingleton.isWF : ∀ {α : Type u_2} [inst : Preorder α] {s : Set α}, s.Subsingleton → s.IsWF
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.map_zero : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (Q : QuadraticMap R M N), Q 0 = 0
-- Std.Data.DTreeMap.Basic
/-- Checks whether a key is present in a map and unconditionally inserts a value for the key.

Equivalent to (but potentially faster than) calling `contains` followed by `insert`.
 -/
Std.DTreeMap.containsThenInsert : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → (a : α) → β a → Bool × Std.DTreeMap α β cmp
-- Mathlib.Analysis.Meromorphic.Basic
/-- `MeromorphicOn` is invariant under translation, special case where the set is a ball.  -/
MeromorphicOn.meromorphicOn_ball_comp_sub_const_iff_meromorphicOn_ball : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {c : 𝕜} {R : ℝ},
  MeromorphicOn (f ∘ fun x => x - c) (Metric.ball c R) ↔ MeromorphicOn f (Metric.ball 0 R)
-- Mathlib.Topology.Order
isOpen_induced_iff : ∀ {α : Type u_1} {β : Type u_2} [t : TopologicalSpace β] {s : Set α} {f : α → β},
  IsOpen s ↔ ∃ t_1, IsOpen t_1 ∧ f ⁻¹' t_1 = s
-- Plausible.Testable
/-- If `true`, when the `Testable` instance required to begin testing cannot be synthesized,
silently admit the goal with `sorry` instead of throwing an error.
 -/
Plausible.Configuration.sorryIfNoTestable : Plausible.Configuration → Bool
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.Path.del.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode.Path α → RBTree.RBNode α → RBTree.RBColor → Sort u_2) (t : RBTree.RBNode α)
  (x : RBTree.RBColor) (h_1 : (t : RBTree.RBNode α) → (x : RBTree.RBColor) → motive RBTree.RBNode.Path.root t x)
  (h_2 :
    (c : RBTree.RBColor) →
      (parent : RBTree.RBNode.Path α) →
        (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left c parent y b) a RBTree.RBColor.red)
  (h_3 :
    (c : RBTree.RBColor) →
      (a : RBTree.RBNode α) →
        (y : α) →
          (parent : RBTree.RBNode.Path α) →
            (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right c a y parent) b RBTree.RBColor.red)
  (h_4 :
    (c : RBTree.RBColor) →
      (parent : RBTree.RBNode.Path α) →
        (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left c parent y b) a RBTree.RBColor.black)
  (h_5 :
    (c : RBTree.RBColor) →
      (a : RBTree.RBNode α) →
        (y : α) →
          (parent : RBTree.RBNode.Path α) →
            (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right c a y parent) b RBTree.RBColor.black),
  (match RBTree.RBNode.Path.root, t, x with
    | RBTree.RBNode.Path.root, t, x => h_1 t x
    | RBTree.RBNode.Path.left c parent y b, a, RBTree.RBColor.red => h_2 c parent y b a
    | RBTree.RBNode.Path.right c a y parent, b, RBTree.RBColor.red => h_3 c a y parent b
    | RBTree.RBNode.Path.left c parent y b, a, RBTree.RBColor.black => h_4 c parent y b a
    | RBTree.RBNode.Path.right c a y parent, b, RBTree.RBColor.black => h_5 c a y parent b) =
    h_1 t x
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.coe_nonneg : ∀ {α : Type u} [inst : Zero α] {a : α} [inst_1 : LE α], 0 ≤ ↑a ↔ 0 ≤ a
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.getExprKind : Lean.PrettyPrinter.Delaborator.DelabM Lean.Name
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.convs'Aux.eq_def : ∀ {K : Type u_2} [inst : DivisionRing K] (x : Stream'.Seq (GenContFract.Pair K)) (x_1 : ℕ),
  GenContFract.convs'Aux x x_1 =
    match x, x_1 with
    | x, 0 => 0
    | s, n.succ =>
      match s.head with
      | none => 0
      | some gp => gp.a / (gp.b + GenContFract.convs'Aux s.tail n)
-- Init.Data.Array.OfFn
Array.ofFn_add : ∀ {α : Type u_1} {n m : ℕ} {f : Fin (n + m) → α},
  Array.ofFn f = (Array.ofFn fun i => f (Fin.castLE ⋯ i)) ++ Array.ofFn fun i => f (Fin.natAdd n i)
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.mem_top : ∀ {M : Type u_1} [inst : AddZeroClass M] (x : M), x ∈ ⊤
-- Mathlib.Order.Grade
Preorder.toGradeBoundedOrder : {α : Type u_3} → [inst : Preorder α] → GradeBoundedOrder α α
-- Init.Data.Nat.Coprime
Nat.exists_coprime : ∀ (m n : ℕ), ∃ m' n', m'.Coprime n' ∧ m = m' * m.gcd n ∧ n = n' * m.gcd n
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.of_vadd_left : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {f : Filter α} {g : Filter β}, (f +ᵥ g).NeBot → f.NeBot
-- Std.Time.DateTime.Timestamp
_private.Std.Time.DateTime.Timestamp.0.Std.Time.Timestamp.mk.inj : ∀ {val val_1 : Std.Time.Duration}, { val := val } = { val := val_1 } → val = val_1
-- Lean.Elab.Term.TermElabM
/-- Adds an `InlayHintInfo` for the fvar auto implicits in `autos` at `inlayHintPos`.
The inserted inlay hint has a hover that denotes the type of the auto-implicit (with meta-variables)
and can be inserted at `inlayHintPos`.
 -/
Lean.Elab.Term.addAutoBoundImplicitsInlayHint : Array Lean.Expr → String.Pos.Raw → Lean.Elab.TermElabM Unit
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.struct : Lean.Lsp.SemanticTokenType
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.insert_Ioc_left_eq_Ioc_pred : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : PredOrder α] {a b : α} [NoMinOrder α],
  a ≤ b → insert a (Finset.Ioc a b) = Finset.Ioc (Order.pred a) b
-- Mathlib.Order.PiLex
Pi.toLex_apply : ∀ {ι : Type u_1} {β : ι → Type u_2} (x : (i : ι) → β i) (i : ι), toLex x i = x i
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
Lean.Meta.Grind.Arith.Cutsat.getOfLT? : Lean.Meta.Grind.Arith.Cutsat.ToIntM (Option Lean.Expr)
-- Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Filter.eventually_iff_seq_eventually : ∀ {ι : Type u_3} {l : Filter ι} {p : ι → Prop} [l.IsCountablyGenerated],
  (∀ᶠ (n : ι) in l, p n) ↔ ∀ (x : ℕ → ι), Filter.Tendsto x Filter.atTop l → ∀ᶠ (n : ℕ) in Filter.atTop, p (x n)