mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α}, (m₁ ∪ m₂).get? k = (m₂.get? k).or (m₁.get? k)
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.fold_eq_foldM : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] {f : γ → β → γ} {init : γ} {it : Std.IterM m β},
  Std.IterM.fold f init it = Std.IterM.foldM (fun x1 x2 => pure (f x1 x2)) init it
-- Std.Data.DHashMap.Basic
/-- Folds the given function over the mappings in the hash map in some order.  -/
Std.DHashMap.fold : {α : Type u} →
  {β : α → Type v} →
    {δ : Type w} → {x : BEq α} → {x_1 : Hashable α} → (δ → (a : α) → β a → δ) → δ → Std.DHashMap α β → δ
-- Mathlib.Algebra.FreeAlgebra
/-- Internal definition used to define `lift`  -/
_private.Mathlib.Algebra.FreeAlgebra.0.FreeAlgebra.liftAux : (R : Type u_1) →
  {X : Type u_2} →
    [inst : CommSemiring R] →
      {A : Type u_3} → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → (X → A) → FreeAlgebra R X →ₐ[R] A
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.containsThenInsert_snd : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  (t.containsThenInsert k).2 = t.insert k
-- Mathlib.Algebra.Star.Subalgebra
StarAlgEquiv.restrictScalars_injective : ∀ (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : MulAction R S]
  [inst_5 : Module S A] [inst_6 : Module S B] [inst_7 : Module R A] [inst_8 : Module R B] [inst_9 : IsScalarTower R S A]
  [inst_10 : IsScalarTower R S B] [inst_11 : Star A] [inst_12 : Star B],
  Function.Injective (StarAlgEquiv.restrictScalars R)
-- Mathlib.Logic.Function.Basic
Function.injective_comp_left_iff : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} [Nonempty α] {g : β → γ},
  (Function.Injective fun x => g ∘ x) ↔ Function.Injective g
-- Std.Http.Protocol.H1
/-- Processes a parsed header field line.

Accounts for header byte/count limits, type-checks name/value pairs, appends
header to `reader.messageHead`, and recurses into the next header slot.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.processParsedHeader : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir → ℕ → ℕ → String → String → Std.Http.Protocol.H1.Machine dir
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.coe_toLinearEquiv : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂), ⇑e.toLinearEquiv = ⇑e
-- Mathlib.Analysis.Calculus.VectorField
ContDiffAt.lieBracket_vectorField : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W : E → E} {x : E} {m n : WithTop ℕ∞},
  ContDiffAt 𝕜 n V x → ContDiffAt 𝕜 n W x → m + 1 ≤ n → ContDiffAt 𝕜 m (VectorField.lieBracket 𝕜 V W) x
-- Mathlib.Algebra.Group.Graph
/-- **Goursat's lemma** for additive monoid isomorphisms.

Let `G ≤ H × I` be a submonoid of a product of additive monoids. Assume that the natural maps from
`G` to both factors are bijective. Then `G` is the graph of some isomorphism `f : H ≃+ I`.  -/
AddSubgroup.exists_addEquiv_eq_graph : ∀ {H : Type u_2} {I : Type u_3} [inst : AddGroup H] [inst_1 : AddGroup I] {G : AddSubgroup (H × I)},
  Function.Bijective (Prod.fst ∘ ⇑G.subtype) →
    Function.Bijective (Prod.snd ∘ ⇑G.subtype) → ∃ e, G = e.toAddMonoidHom.graph
-- Mathlib.CategoryTheory.Adjunction.Reflective
/-- The reflector `C ⥤ D` when `R : D ⥤ C` is reflective.  -/
CategoryTheory.reflector : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (i : CategoryTheory.Functor D C) → [CategoryTheory.Reflective i] → CategoryTheory.Functor C D
-- Mathlib.Order.Basic
Ne.not_ge_or_not_le : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, a ≠ b → ¬b ≤ a ∨ ¬a ≤ b
-- Std.Data.Internal.List.Associative
Std.Internal.List.List.getValue?_filter_containsKey_of_containsKey_right : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₂ = true →
      Std.Internal.List.getValue? k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) =
        Std.Internal.List.getValue? k l₁
-- Init.Data.BitVec.Lemmas
BitVec.toInt_ofNat : ∀ {n : ℕ} (x : ℕ), (OfNat.ofNat x).toInt = (↑x).bmod (2 ^ n)
-- Mathlib.Order.DirSupClosed
dirSupClosedOn_compl : ∀ {α : Type u_1} {s : Set α} {D : Set (Set α)} [inst : Preorder α], DirSupClosedOn D sᶜ ↔ DirSupInaccOn D s
-- Init.Data.SInt.Lemmas
UInt16.toInt16_ofBitVec : ∀ (b : BitVec 16), { toBitVec := b }.toInt16 = Int16.ofBitVec b
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.Header.mk.inj : ∀ {version : UInt8} {isutcnt isstdcnt leapcnt timecnt typecnt charcnt : UInt32} {version_1 : UInt8}
  {isutcnt_1 isstdcnt_1 leapcnt_1 timecnt_1 typecnt_1 charcnt_1 : UInt32},
  { version := version, isutcnt := isutcnt, isstdcnt := isstdcnt, leapcnt := leapcnt, timecnt := timecnt,
        typecnt := typecnt, charcnt := charcnt } =
      { version := version_1, isutcnt := isutcnt_1, isstdcnt := isstdcnt_1, leapcnt := leapcnt_1, timecnt := timecnt_1,
        typecnt := typecnt_1, charcnt := charcnt_1 } →
    version = version_1 ∧
      isutcnt = isutcnt_1 ∧
        isstdcnt = isstdcnt_1 ∧ leapcnt = leapcnt_1 ∧ timecnt = timecnt_1 ∧ typecnt = typecnt_1 ∧ charcnt = charcnt_1
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- additive version of `MeasureTheory.Measure.haar.chaar`  -/
MeasureTheory.Measure.haar.addCHaar : {G : Type u_1} →
  [inst : AddGroup G] →
    [inst_1 : TopologicalSpace G] →
      [IsTopologicalAddGroup G] → TopologicalSpace.PositiveCompacts G → TopologicalSpace.Compacts G → ℝ
-- Mathlib.CategoryTheory.Functor.FullyFaithful
/-- `F.map` is injective for each `X Y : C`.  -/
CategoryTheory.Functor.Faithful.map_injective : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D} [self : F.Faithful] {X Y : C}, Function.Injective F.map
-- Mathlib.Order.CompleteLattice.Lemmas
/-- This is a weaker version of `sup_sInf_eq`  -/
sup_sInf_le_iInf_sup : ∀ {α : Type u_1} [inst : CompleteLattice α] {a : α} {s : Set α}, a ⊔ sInf s ≤ ⨅ b ∈ s, a ⊔ b
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.left_le_veblenWith : ∀ {f : Ordinal.{u} → Ordinal.{u}}, Order.IsNormal f → 0 < f 0 → ∀ (o a : Ordinal.{u}), o ≤ Ordinal.veblenWith f o a
-- Std.Time.Zoned.RecurringRule
Std.Time.TimeZone.RecurringRule.mk.sizeOf_spec : ∀ (stdName : String) (stdOffset : Std.Time.TimeZone.Offset) (dst : Option Std.Time.TimeZone.DaylightSavingRule),
  sizeOf { stdName := stdName, stdOffset := stdOffset, dst := dst } = 1 + sizeOf stdName + sizeOf stdOffset + sizeOf dst
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.comap_inf : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (S T : AddSubsemigroup N) (f : M →ₙ+ N),
  AddSubsemigroup.comap f (S ⊓ T) = AddSubsemigroup.comap f S ⊓ AddSubsemigroup.comap f T
-- Mathlib.Order.Hom.Lattice
LatticeHom.comp_id : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (f : LatticeHom α β),
  f.comp (LatticeHom.id α) = f
-- Init.Data.Bool
Bool.not_inj_iff : ∀ {x y : Bool}, (!x) = !y ↔ x = y
-- Init.Internal.Order.Basic
/-- The “less-or-equal-to” or “approximates” relation is antisymmetric.  -/
Lean.Order.PartialOrder.rel_antisymm : ∀ {α : Sort u} [self : Lean.Order.PartialOrder α] {x y : α},
  Lean.Order.PartialOrder.rel x y → Lean.Order.PartialOrder.rel y x → x = y
-- Init.Data.Nat.Basic
Nat.le_iff_lt_or_eq : ∀ {n m : ℕ}, n ≤ m ↔ n < m ∨ n = m
-- Mathlib.Data.String.Lemmas
String.replicate.eq_1 : ∀ (n : ℕ) (c : Char), String.replicate n c = String.ofList (List.replicate n c)
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.ofCLM_toCLM : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] (A : E →SWOT[σ] F),
  ContinuousLinearMapWOT.ofCLM A.toCLM = A
-- Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
OrderDual.addRightMono : ∀ {α : Type u} [inst : LE α] [inst_1 : Add α] [c : AddRightMono α], AddRightMono αᵒᵈ
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- Also known as the stability axiom.  -/
CategoryTheory.GrothendieckTopology.pullback_stable : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {S : CategoryTheory.Sieve X}
  (J : CategoryTheory.GrothendieckTopology C) (f : Y ⟶ X), S ∈ J X → CategoryTheory.Sieve.pullback f S ∈ J Y
-- Mathlib.CategoryTheory.Idempotents.Basic
CategoryTheory.IsIdempotentComplete.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C],
  (∀ (X : C) (p : X ⟶ X),
      CategoryTheory.CategoryStruct.comp p p = p →
        ∃ Y i e,
          CategoryTheory.CategoryStruct.comp i e = CategoryTheory.CategoryStruct.id Y ∧
            CategoryTheory.CategoryStruct.comp e i = p) →
    CategoryTheory.IsIdempotentComplete C
-- Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
CategoryTheory.ShortComplex.FunctorEquivalence.counitIso_hom_app_app_τ₃ : ∀ (J : Type u_1) (C : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (X : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) (X_1 : J),
  (((CategoryTheory.ShortComplex.FunctorEquivalence.counitIso J C).hom.app X).app X_1).τ₃ =
    CategoryTheory.CategoryStruct.id (X.obj X_1).X₃
-- Mathlib.Algebra.Group.ULift
ULift.addGroup : {α : Type u} → [AddGroup α] → AddGroup (ULift.{u_1, u} α)
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.Const.alterₘ.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
/-- If a functor `F : C ⥤ D` preserves short exact sequences on the left-hand side, (i.e.
if `0 ⟶ A ⟶ B ⟶ C ⟶ 0` is exact then `0 ⟶ F(A) ⟶ F(B) ⟶ F(C)` is exact)
then it preserves monomorphism.
 -/
CategoryTheory.Functor.preservesMonomorphisms_of_preserves_shortExact_left : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Abelian C]
  [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_4 : F.Additive],
  (∀ (S : CategoryTheory.ShortComplex C), S.ShortExact → (S.map F).Exact ∧ CategoryTheory.Mono (F.map S.f)) →
    F.PreservesMonomorphisms
-- Mathlib.AlgebraicGeometry.Artinian
AlgebraicGeometry.IsLocallyArtinian.of_topologicalKrullDim_le_zero : ∀ {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X],
  topologicalKrullDim ↥X ≤ 0 → AlgebraicGeometry.IsLocallyArtinian X
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.MonadHom.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {T₁ T₂ : CategoryTheory.Monad C}
  {toNatTrans : CategoryTheory.NatTrans T₁.toFunctor T₂.toFunctor}
  {app_η :
    autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp (T₁.η.app X) (toNatTrans.app X) = T₂.η.app X)
      CategoryTheory.MonadHom.app_η._autoParam}
  {app_μ :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (T₁.μ.app X) (toNatTrans.app X) =
          CategoryTheory.CategoryStruct.comp
            (CategoryTheory.CategoryStruct.comp (T₁.map (toNatTrans.app X)) (toNatTrans.app (T₂.obj X))) (T₂.μ.app X))
      CategoryTheory.MonadHom.app_μ._autoParam}
  {toNatTrans_1 : CategoryTheory.NatTrans T₁.toFunctor T₂.toFunctor}
  {app_η_1 :
    autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp (T₁.η.app X) (toNatTrans_1.app X) = T₂.η.app X)
      CategoryTheory.MonadHom.app_η._autoParam}
  {app_μ_1 :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (T₁.μ.app X) (toNatTrans_1.app X) =
          CategoryTheory.CategoryStruct.comp
            (CategoryTheory.CategoryStruct.comp (T₁.map (toNatTrans_1.app X)) (toNatTrans_1.app (T₂.obj X)))
            (T₂.μ.app X))
      CategoryTheory.MonadHom.app_μ._autoParam},
  { toNatTrans := toNatTrans, app_η := app_η, app_μ := app_μ } =
      { toNatTrans := toNatTrans_1, app_η := app_η_1, app_μ := app_μ_1 } →
    toNatTrans = toNatTrans_1
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.hurwitzOddFEPair_g : ∀ (a : UnitAddCircle) (a_1 : ℝ), (HurwitzZeta.hurwitzOddFEPair a).g a_1 = (Complex.ofReal ∘ HurwitzZeta.sinKernel a) a_1
-- Plausible.Gen
Plausible.Gen.genFailure : Plausible.GenError → IO.Error
-- Mathlib.Topology.PartialHomeomorph.Basic
Set.partialHomeomorphSubtypeCoe_source : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : Set X) (hs : Nonempty ↑s),
  (s.partialHomeomorphSubtypeCoe hs).source = Set.univ
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.Cowedge.ext_inv_hom : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} {W₁ W₂ : CategoryTheory.Limits.Cowedge F}
  (e : W₁.pt ≅ W₂.pt)
  (he :
    autoParam
      (∀ (j : J),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicofork.π W₁ j) e.hom =
          CategoryTheory.Limits.Multicofork.π W₂ j)
      CategoryTheory.Limits.Cowedge.ext._auto_1),
  (CategoryTheory.Limits.Cowedge.ext e he).inv.hom = e.inv
-- Init.Data.Slice.InternalLemmas
Std.Slice.Internal.forIn_iter : ∀ {α : Type v} {γ : Type u} {β : Type v} {m : Type w → Type x} [inst : Monad m] {δ : Type w}
  [inst_1 : Std.ToIterator (Std.Slice γ) Id α β] [inst_2 : Std.Iterator α Id β] [inst_3 : Std.IteratorLoop α Id m]
  {s : Std.Slice γ} {init : δ} {f : β → δ → m (ForInStep δ)}, forIn (Std.Slice.Internal.iter s) init f = forIn s init f
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.Subcomplex.mk.sizeOf_spec : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] [inst_1 : SizeOf X]
  [inst_2 : (a : X) → SizeOf (C a)] [inst_3 : (a : X) → SizeOf (D a)] (carrier : Set X)
  (I : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) (closed' : IsClosed carrier)
  (union' : D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = carrier),
  sizeOf { carrier := carrier, I := I, closed' := closed', union' := union' } = 1 + sizeOf closed' + sizeOf union'
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.updateInc! : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.Code pu → Lean.FVarId → ℕ → Bool → Bool → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.Code pu
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.ofObjects_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} {X : I → C} {I' : Type u_2} {X' : I' → C}
  {Y : C}, Set.range X ⊆ Set.range X' → CategoryTheory.Sieve.ofObjects X Y ≤ CategoryTheory.Sieve.ofObjects X' Y
-- Mathlib.Data.Set.Sups
Set.mem_infs : ∀ {α : Type u_2} [inst : SemilatticeInf α] {s t : Set α} {c : α}, c ∈ s ⊼ t ↔ ∃ a ∈ s, ∃ b ∈ t, a ⊓ b = c
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.tr_ret_respects : ∀ (k : Turing.ToPartrec.Cont) (v : List ℕ) (s : Option Turing.PartrecToTM2.Γ'),
  ∃ b₂,
    Turing.PartrecToTM2.TrCfg (Turing.ToPartrec.stepRet k v) b₂ ∧
      StateTransition.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr)
        { l := some (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.trCont k)), var := s,
          stk := Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList v) [] [] (Turing.PartrecToTM2.trContStack k) }
        b₂
-- Mathlib.Algebra.Ring.Invertible
one_sub_invOf_two : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : Invertible 2], 1 - ⅟2 = ⅟2
-- Lean.Meta.Eqns
/-- If any equation theorem affecting option is not the default value, store the option values
for later use during lazy equation generation.
 -/
Lean.Meta.saveEqnAffectingOptions : Lean.Name → Lean.MetaM Unit
-- Mathlib.Algebra.Category.Grp.Basic
AddEquiv.toAddGrpIso_inv : ∀ {X Y : AddGrpCat} (e : ↑X ≃+ ↑Y), e.toAddGrpIso.inv = AddGrpCat.ofHom e.symm.toAddMonoidHom
-- Mathlib.Data.Nat.PSub
Nat.ppred_succ : ∀ {n : ℕ}, n.succ.ppred = some n
-- Mathlib.Topology.Algebra.GroupCompletion
AddMonoidHom.completion_add : ∀ {α : Type u_3} [inst : UniformSpace α] [inst_1 : AddGroup α] [inst_2 : IsUniformAddGroup α] {γ : Type u_5}
  [inst_3 : AddCommGroup γ] [inst_4 : UniformSpace γ] [inst_5 : IsUniformAddGroup γ] (f g : α →+ γ) (hf : Continuous ⇑f)
  (hg : Continuous ⇑g), (f + g).completion ⋯ = f.completion hf + g.completion hg
-- Mathlib.Order.RelSeries
RelSeries.last_tail : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (len_pos : p.length ≠ 0), (p.tail len_pos).last = p.last
-- Lean.Widget.TaggedText
_private.Lean.Widget.TaggedText.0.Lean.Widget.TaggedText.TaggedState.column : Lean.Widget.TaggedText.TaggedState✝ → ℕ
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
/-- An even function is interval integrable (with respect to the volume measure) on every interval
of the form `0..x` if it is interval integrable (with respect to the volume measure) on every
interval of the form `0..x`, for positive `x`.

See `intervalIntegrable_of_even` for a stronger result.  -/
intervalIntegrable_of_even₀ : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] {f : ℝ → E},
  (∀ (x : ℝ), f x = f (-x)) →
    (∀ (x : ℝ), 0 < x → IntervalIntegrable f MeasureTheory.volume 0 x) →
      ∀ {t : ℝ},
        autoParam (‖f (min 0 t)‖ₑ ≠ ⊤) intervalIntegrable_of_even₀._auto_1 →
          IntervalIntegrable f MeasureTheory.volume 0 t
-- Mathlib.Analysis.Convex.Approximation
/-- The real version of `sSup_of_countable_affine_eq`.  -/
ConvexOn.real_sSup_of_countable_affine_eq : ∀ {E : Type u_2} {s : Set E} {φ : E → ℝ} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E]
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [HereditarilyLindelofSpace E],
  IsClosed s →
    LowerSemicontinuousOn φ s →
      ConvexOn ℝ s φ →
        ∃ 𝓕',
          𝓕'.Countable ∧
            sSup 𝓕' = s.domRestrict φ ∧
              ∀ f ∈ 𝓕', f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict ⇑l + Function.const (↑s) c
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleSets.mk.injEq : ∀ (ruleSets ruleSets_1 : Array Aesop.RuleSetName),
  ({ ruleSets := ruleSets } = { ruleSets := ruleSets_1 }) = (ruleSets = ruleSets_1)
-- Mathlib.Algebra.Homology.HomotopyCategory
/-- A natural transformation induces a natural transformation between
the induced functors on the homotopy category.  -/
CategoryTheory.NatTrans.mapHomotopyCategory : {ι : Type u_2} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {W : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_1, u_3} W] →
            [inst_3 : CategoryTheory.Preadditive W] →
              {F G : CategoryTheory.Functor V W} →
                [inst_4 : F.Additive] →
                  [inst_5 : G.Additive] →
                    (F ⟶ G) → (c : ComplexShape ι) → F.mapHomotopyCategory c ⟶ G.mapHomotopyCategory c
-- Mathlib.Algebra.Category.Ring.Basic
/-- The underlying ring hom.  -/
CommSemiRingCat.Hom.hom' : {R S : CommSemiRingCat} → R.Hom S → ↑R →+* ↑S
-- Mathlib.CategoryTheory.Triangulated.Opposite.Functor
CategoryTheory.Pretriangulated.Opposite.commShift_natTrans_op_int : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] {F : CategoryTheory.Functor C D} [inst_4 : F.CommShift ℤ]
  {G : CategoryTheory.Functor C D} [inst_5 : G.CommShift ℤ] (τ : F ⟶ G) [CategoryTheory.NatTrans.CommShift τ ℤ],
  CategoryTheory.NatTrans.CommShift (CategoryTheory.NatTrans.op τ) ℤ
-- Mathlib.Logic.Embedding.Basic
/-- `α ↪ β` is a bundled injective function.  -/
Function.Embedding : Sort u_1 → Sort u_2 → Sort (max (max 1 u_1) u_2)
-- Mathlib.Topology.UniformSpace.Equiv
/-- Change the uniform equiv `f` to make the inverse function definitionally equal to `g`.  -/
UniformEquiv.changeInv : {α : Type u} →
  {β : Type u_1} →
    [inst : UniformSpace α] →
      [inst_1 : UniformSpace β] → (f : α ≃ᵤ β) → (g : β → α) → Function.RightInverse g ⇑f → α ≃ᵤ β
-- Batteries.Data.AssocList
Batteries.AssocList.replace.eq_2 : ∀ {α : Type u_1} {β : Type u_2} [inst : BEq α] (a : α) (b : β) (a_1 : α) (b_1 : β) (es : Batteries.AssocList α β),
  Batteries.AssocList.replace a b (Batteries.AssocList.cons a_1 b_1 es) =
    match a_1 == a with
    | true => Batteries.AssocList.cons a b es
    | false => Batteries.AssocList.cons a_1 b_1 (Batteries.AssocList.replace a b es)
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.disjoint_interior_closedInterior_face : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [inst_4 : PartialOrder k] {n : ℕ} (s : Affine.Simplex k P n) {fs : Finset (Fin (n + 1))},
  fs ≠ Finset.univ → ∀ {m : ℕ} (h : fs.card = m + 1), Disjoint s.interior (s.face h).closedInterior
-- Mathlib.Computability.Partrec
/-- Find the smallest `n` satisfying `f n`, where all `f k` for `k < n` are defined as false.
Returns a `Part`.  -/
Nat.rfindOpt : {α : Type u_1} → (ℕ → Option α) → Part α
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
Complex.deriv_exp : deriv Complex.exp = Complex.exp
-- Lean.Attributes
Lean.AttributeImpl.mk.injEq : ∀ (toAttributeImplCore : Lean.AttributeImplCore) (add : Lean.Name → Lean.Syntax → Lean.AttributeKind → Lean.AttrM Unit)
  (erase : Lean.Name → Lean.AttrM Unit) (toAttributeImplCore_1 : Lean.AttributeImplCore)
  (add_1 : Lean.Name → Lean.Syntax → Lean.AttributeKind → Lean.AttrM Unit) (erase_1 : Lean.Name → Lean.AttrM Unit),
  ({ toAttributeImplCore := toAttributeImplCore, add := add, erase := erase } =
      { toAttributeImplCore := toAttributeImplCore_1, add := add_1, erase := erase_1 }) =
    (toAttributeImplCore = toAttributeImplCore_1 ∧ add = add_1 ∧ erase = erase_1)
-- Mathlib.Topology.MetricSpace.MetricSeparated
Metric.AreSeparated.union_right_iff : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {s t t' : Set X},
  Metric.AreSeparated s (t ∪ t') ↔ Metric.AreSeparated s t ∧ Metric.AreSeparated s t'
-- Mathlib.RepresentationTheory.FiniteIndex
Rep.resIndAdjunction_counit_app : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] {S : Subgroup G}
  [inst_2 : DecidableRel ⇑(QuotientGroup.rightRel S)] [inst_3 : S.FiniteIndex] (A : Rep.{max w u v, u, v} k ↥S),
  (Rep.resIndAdjunction k S).counit.app A =
    CategoryTheory.CategoryStruct.comp ((Rep.resFunctor S.subtype).map A.indCoindIso.hom)
      ((Rep.resCoindAdjunction k S.subtype).counit.app A)
-- Mathlib.Order.Fin.Basic
Fin.instBiheytingAlgebra : {n : ℕ} → [NeZero n] → BiheytingAlgebra (Fin n)
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof.simp_prefix : Bool →
  Lean.Grind.AC.Seq → Lean.Meta.Grind.AC.EqCnstr → Lean.Meta.Grind.AC.DiseqCnstr → Lean.Meta.Grind.AC.DiseqCnstrProof
-- Mathlib.Data.Set.Basic
Set.inter_ssubset_left_iff : ∀ {α : Type u} {s t : Set α}, s ∩ t ⊂ s ↔ ¬s ⊆ t
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.FoldingRangeKind : Type
-- Init.Data.Int.LemmasAux
Int.neg_lt_self_iff : ∀ {n : ℤ}, -n < n ↔ 0 < n