mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- If a binary bicone for `P` and `Q` is bilimit, then the binary bicone for `P'` and `Q'`
obtained using isomorphisms `P ≅ P'` and `Q ≅ Q'` is also bilimit.  -/
CategoryTheory.Limits.BinaryBicone.IsBilimit.ofIso : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q P' Q' : C} →
        {b : CategoryTheory.Limits.BinaryBicone P Q} →
          b.IsBilimit → (eP : P ≅ P') → (eQ : Q ≅ Q') → (b.ofIso eP eQ).IsBilimit
-- Mathlib.Data.Ordmap.Invariants
Ordnode.insert.eq_def : ∀ {α : Type u_1} [inst : LE α] [inst_1 : DecidableLE α] (x : α) (x_1 : Ordnode α),
  Ordnode.insert x x_1 =
    match x_1 with
    | Ordnode.nil => Ordnode.singleton x
    | Ordnode.node sz l y r =>
      match cmpLE x y with
      | Ordering.lt => (Ordnode.insert x l).balanceL y r
      | Ordering.eq => Ordnode.node sz l x r
      | Ordering.gt => l.balanceR y (Ordnode.insert x r)
-- Mathlib.RingTheory.DedekindDomain.Different
/-- A prime does not divide the different ideal iff it is unramified.  -/
not_dvd_differentIdeal_iff : ∀ {A : Type u_1} {B : Type u_3} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain A]
  [inst_4 : IsDedekindDomain A] [inst_5 : IsDedekindDomain B] [inst_6 : Module.IsTorsionFree A B]
  [inst_7 : Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] {P : Ideal B}
  [inst_9 : P.IsPrime], ¬P ∣ differentIdeal A B ↔ Algebra.IsUnramifiedAt A P
-- Mathlib.Algebra.Quandle
UnitalShelf.act_one : ∀ {α : Type u} [self : UnitalShelf α] (a : α), Shelf.act a 1 = a
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
/-- If `0 < n`, then `a 1` has order `2 * n`.
 -/
QuaternionGroup.orderOf_a_one : ∀ {n : ℕ}, orderOf (QuaternionGroup.a 1) = 2 * n
-- Init.Data.Range.Polymorphic.Instances
Std.instLawfulUpwardEnumerableLTOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLEOfLawfulOrderLT : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] [Std.LawfulOrderLT α],
  Std.PRange.LawfulUpwardEnumerableLT α
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey_eq_minKey! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → ∀ {he : t.isEmpty = false}, t.minKey he = t.minKey!
-- Mathlib.Util.CountHeartbeats
/-- An option used by the `countHeartbeats` linter: if set to `true`, then the countHeartbeats linter
rounds down to the nearest 1000 the heartbeat count.
 -/
Mathlib.Linter.linter.countHeartbeatsApprox : Lean.Option Bool
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂Iso.brecOn.eq : ∀ {motive : Mathlib.Tactic.BicategoryLike.Mor₂Iso → Sort u} (t : Mathlib.Tactic.BicategoryLike.Mor₂Iso)
  (F_1 : (t : Mathlib.Tactic.BicategoryLike.Mor₂Iso) → Mathlib.Tactic.BicategoryLike.Mor₂Iso.below t → motive t),
  Mathlib.Tactic.BicategoryLike.Mor₂Iso.brecOn t F_1 = F_1 t (Mathlib.Tactic.BicategoryLike.Mor₂Iso.brecOn.go t F_1).2
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.setOfFractNe : {ι : Type u_3} → {s : Set (ι → ℕ)} → IsProperLinearSet s → [Finite ι] → Set (ι → ℕ)
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
CategoryTheory.Limits.IsWeakLimit.equivIsoWeakLimit_symm_apply : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C] {F : CategoryTheory.Functor J C} {r t : CategoryTheory.Limits.Cone F}
  (i : r ≅ t) (P : CategoryTheory.Limits.IsWeakLimit t),
  (CategoryTheory.Limits.IsWeakLimit.equivIsoWeakLimit i).symm P = P.ofIsoWeakLimit i.symm
-- Mathlib.Analysis.Convex.Basic
Convex.linear_preimage : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid F] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F] {s : Set F},
  Convex 𝕜 s → ∀ (f : E →ₗ[𝕜] F), Convex 𝕜 (⇑f ⁻¹' s)
-- Mathlib.Topology.MetricSpace.GromovHausdorff
GromovHausdorff.instInhabitedAuxGluingStruct : (A : Type) → [inst : MetricSpace A] → Inhabited (GromovHausdorff.AuxGluingStruct A)
-- Mathlib.Topology.Order.OrderClosed
nhdsWithin_Ioc_eq_nhdsLE : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {a b : α},
  a < b → nhdsWithin b (Set.Ioc a b) = nhdsWithin b (Set.Iic b)
-- Mathlib.RingTheory.Trace.Quotient
_private.Mathlib.RingTheory.Trace.Quotient.0.termPSₚ : Lean.ParserDescr
-- Mathlib.Analysis.Complex.HalfPlane
/-- An open right half-plane is an open set in the complex plane.  -/
Complex.isOpen_re_gt : ∀ (x : ℝ), IsOpen {z | x < z.re}
-- Init.Data.Rat.Basic
instReprRat : Repr ℚ
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastUdivOutput.mk.injEq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {old : Std.Sat.AIG α} {w : ℕ} (aig : Std.Sat.AIG α)
  (q r : aig.RefVec w) (hle : old.decls.size ≤ aig.decls.size) (aig_1 : Std.Sat.AIG α) (q_1 r_1 : aig_1.RefVec w)
  (hle_1 : old.decls.size ≤ aig_1.decls.size),
  ({ aig := aig, q := q, r := r, hle := hle } = { aig := aig_1, q := q_1, r := r_1, hle := hle_1 }) =
    (aig = aig_1 ∧ q ≍ q_1 ∧ r ≍ r_1)
-- Lean.Elab.Do.Basic
/-- Wrap `dec.k` so it elaborates as dead iff `info.noFallthrough`.  -/
Lean.Elab.Do.DoElemCont.withDeadCodeFromInfo : Lean.Elab.Do.DoElemCont → Lean.Elab.Do.ControlInfo → Lean.Elab.Do.DoElemCont
-- Mathlib.Combinatorics.Graph.Simple
Graph.ofSimpleGraph_isLink : ∀ {α : Type u_1} (G : SimpleGraph α) (e : Sym2 α) (x y : α),
  (Graph.ofSimpleGraph G).IsLink e x y = (e = s(x, y) ∧ e ∈ G.edgeSet)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- If there are zero morphisms, any initial object is a zero object.  -/
CategoryTheory.Limits.hasZeroObject_of_hasInitial_object : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasInitial C], CategoryTheory.Limits.HasZeroObject C
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.check.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.coeff_natDegree_succ_eq_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.coeff (p.natDegree + 1) = 0
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
IsProperSemilinearSet.biUnion_finset : ∀ {M : Type u_1} {ι : Type u_3} [inst : AddCommMonoid M] {s : Finset ι} {t : ι → Set M},
  (∀ i ∈ s, IsProperSemilinearSet (t i)) → IsProperSemilinearSet (⋃ i ∈ s, t i)
-- Mathlib.Data.Analysis.Filter
CFilter.inf_le_left : ∀ {α : Type u_1} {σ : Type u_2} [inst : PartialOrder α] (self : CFilter α σ) (a b : σ), self.f (self.inf a b) ≤ self.f a
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.edgeSet_ssubset_edgeSet : ∀ {V : Type u} {G₁ G₂ : SimpleGraph V}, G₁.edgeSet ⊂ G₂.edgeSet ↔ G₁ < G₂
-- Std.Data.DHashMap.Lemmas
/-- Simpler variant of `get?_filter` when `LawfulBEq` is available.  -/
Std.DHashMap.Const.get?_filter' : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [LawfulBEq α]
  {f : α → β → Bool} {k : α},
  Std.DHashMap.Const.get? (Std.DHashMap.filter f m) k = Option.filter (f k) (Std.DHashMap.Const.get? m k)
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- Eta-expanded form of `HasFDerivWithinAt.mul` -/
HasFDerivWithinAt.fun_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {𝔸' : Type u_6} [inst_3 : NormedCommRing 𝔸']
  [inst_4 : NormedAlgebra 𝕜 𝔸'] {c d : E → 𝔸'} {c' d' : E →L[𝕜] 𝔸'},
  HasFDerivWithinAt c c' s x →
    HasFDerivWithinAt d d' s x → HasFDerivWithinAt (fun i => c i * d i) (c x • d' + d x • c') s x
-- Mathlib.Analysis.Convex.Segment
openSegment.lift : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [ZeroLEOneClass 𝕜] [inst_4 : Module 𝕜 E] (R : Type u_7) [inst_5 : Semiring R] [inst_6 : PartialOrder R]
  [inst_7 : Module R E] [inst_8 : Module R 𝕜] [IsScalarTower R 𝕜 E] [Nontrivial 𝕜] [SMulPosStrictMono R 𝕜] (x y : E),
  openSegment R x y ⊆ openSegment 𝕜 x y
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.topEquiv.eq_1 : ∀ {M : Type u_1} [inst : Mul M],
  Subsemigroup.topEquiv =
    { toFun := fun x => ↑x, invFun := fun x => ⟨x, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
-- Std.Async.Process
Std.IO.Process.instInhabitedPId : Inhabited Std.IO.Process.PId
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.UnifyM.State.us : Lean.Meta.Sym.UnifyM.State✝ → List Lean.Level
-- Aesop.Forward.Match.Types
/-- The rule to which this match belongs.  -/
Aesop.ForwardRuleMatch.rule : Aesop.ForwardRuleMatch → Aesop.ForwardRule
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.hasHomology_of_epi_of_isIso_of_mono' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [S₂.HasHomology] [CategoryTheory.Epi φ.τ₁]
  [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃], S₁.HasHomology
-- Init.Data.List.MinMaxOn
List.apply_minOn_append_le_left : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {xs ys : List α}
  {f : α → β} (h : xs ≠ []), f (List.minOn f (xs ++ ys) ⋯) ≤ f (List.minOn f xs h)
-- Mathlib.Computability.RegularExpressions
RegularExpression.map_pow : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (P : RegularExpression α) (n : ℕ),
  RegularExpression.map f (P ^ n) = RegularExpression.map f P ^ n
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.map_obj_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S S' : D} {T : CategoryTheory.Functor C D} (f : S ⟶ S')
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S') T),
  ((CategoryTheory.StructuredArrow.map f).obj X).hom = CategoryTheory.CategoryStruct.comp f X.hom
-- Init.Data.String.Lemmas.TakeDrop
String.Slice.toList_copy_dropEnd : ∀ {s : String.Slice} {n : ℕ}, (s.dropEnd n).copy.toList = List.take (s.copy.toList.length - n) s.copy.toList
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.component_sumInv : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {ι : Type u_6} (M : ι → Type u_7)
  [inst_1 : (i : ι) → AddCommGroup (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : Fintype ι]
  (x : AdicCompletion I (DirectSum ι fun j => M j)) (j : ι),
  (DirectSum.component (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) j) ((AdicCompletion.sumInv I M) x) =
    (AdicCompletion.map I (DirectSum.component R ι M j)) x
-- Lean.Compiler.IR.Basic
/-- Jump to join point `j`  -/
Lean.IR.FnBody.jmp : Lean.IR.JoinPointId → Array Lean.IR.Arg → Lean.IR.FnBody
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.containsThenInsert_fst : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β k}, (t.containsThenInsert k v).1 = t.contains k
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.forM : {α : Type u} →
  {β : α → Type v} →
    {m : Type w → Type w'} →
      [Monad m] → ((a : α) → β a → m PUnit.{w + 1}) → Std.DHashMap.Internal.AssocList α β → m PUnit.{w + 1}
-- Mathlib.Data.Finset.Sups
Finset.image_subset_sups_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] {s t : Finset α} {a : α},
  a ∈ s → Finset.image (fun x => a ⊔ x) t ⊆ s ⊻ t
-- Mathlib.Topology.PartitionOfUnity
PartitionOfUnity.instInhabited : {ι : Type u} →
  {X : Type v} → [inst : TopologicalSpace X] → {s : Set X} → [Inhabited ι] → Inhabited (PartitionOfUnity ι X s)
-- Mathlib.Analysis.Convex.Topology
/-- If `x ∈ closure s` and `x + y ∈ interior s`, then `x + t y ∈ interior s` for `t ∈ (0, 1]`.  -/
Convex.add_smul_mem_interior' : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E]
  [AddRightMono 𝕜] {s : Set E},
  Convex 𝕜 s → ∀ {x y : E}, x ∈ closure s → x + y ∈ interior s → ∀ {t : 𝕜}, t ∈ Set.Ioc 0 1 → x + t • y ∈ interior s
-- Init.Control.Lawful.Instances
_private.Init.Control.Lawful.Instances.0.Option.getD.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (x : α) → motive (some x)) (h_2 : Unit → motive none),
  (match none with
    | some x => h_1 x
    | none => h_2 ()) =
    h_2 ()
-- Init.Data.Array.Lemmas
Array.setIfInBounds_setIfInBounds : ∀ {α : Type u_1} (a : α) {b : α} {xs : Array α} {i : ℕ}, (xs.setIfInBounds i a).setIfInBounds i b = xs.setIfInBounds i b
-- Init.Data.UInt.Lemmas
UInt8.toNat_toUSize : ∀ (x : UInt8), x.toUSize.toNat = x.toNat
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.splitRevInTwo.eq_1 : ∀ {α : Type u_1} {n : ℕ} (l : { l // l.length = n }),
  List.MergeSort.Internal.splitRevInTwo l =
    (⟨(List.MergeSort.Internal.splitRevAt ((n + 1) / 2) ↑l).1, ⋯⟩,
      ⟨(List.MergeSort.Internal.splitRevAt ((n + 1) / 2) ↑l).2, ⋯⟩)
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.TakeWhile.0.Std.Iter.atIdxSlow?_eq_match.match_3.eq_3 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toArray_filterMapM_filterMapWithPostcondition : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Monad m]
  [LawfulMonad m] [inst_2 : Monad n] [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
  [inst_6 : Monad o] [inst_7 : MonadAttach o] [LawfulMonad o] [WeaklyLawfulMonadAttach o] [inst_10 : MonadLiftT m n]
  [inst_11 : MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → Std.Iterators.PostconditionT n (Option γ)} {g : γ → o (Option δ)}
  {it : Std.IterM m β},
  (Std.IterM.filterMapM g (Std.IterM.filterMapWithPostcondition f it)).toArray =
    (Std.IterM.filterMapM
        (fun b => do
          let __do_lift ← liftM (f b).run
          match __do_lift with
            | none => pure none
            | some fb => g fb)
        it).toArray
-- Std.Data.ExtDHashMap.Basic
/-- Checks whether a key is present in a map, returning the associated value, and inserts a value for
the key if it was not found.

If the returned value is `some v`, then the returned map is unaltered. If it is `none`, then the
returned map has a new value inserted.

Equivalent to (but potentially faster than) calling `get?` followed by `insertIfNew`.

Uses the `LawfulBEq` instance to cast the retrieved value to the correct type.
 -/
Std.ExtDHashMap.getThenInsertIfNew? : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} → [LawfulBEq α] → Std.ExtDHashMap α β → (a : α) → β a → Option (β a) × Std.ExtDHashMap α β
-- Mathlib.GroupTheory.Sylow
IsPGroup.mem_toSylow : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] [inst_1 : Fact (Nat.Prime p)] {P : Subgroup G} (hP1 : IsPGroup p ↥P)
  (hP2 : ¬p ∣ P.index) {g : G}, g ∈ hP1.toSylow hP2 ↔ g ∈ P
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.IsAddMonHom.add_hom_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {M' N' : C}
  {inst_2 : CategoryTheory.AddMonObj M'} {inst_3 : CategoryTheory.AddMonObj N'} (f : M' ⟶ N')
  [self : CategoryTheory.IsAddMonHom f] {Z : C} (h : N' ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h)
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.notMem_neighborSet_self : ∀ {V : Type u} (G : SimpleGraph V) {a : V}, a ∉ G.neighborSet a
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k a : α},
  (m.erase k).get? a = if (k == a) = true then none else m.get? a
-- Mathlib.Topology.Basic
Classical.epsilon.congr_simp : ∀ {α : Sort u} [h : Nonempty α] (p p_1 : α → Prop), p = p_1 → Classical.epsilon p = Classical.epsilon p_1
-- Init.Core
Quot.liftBeta : ∀ {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) (c : ∀ (a b : α), r a b → f a = f b) (a : α),
  Quot.lift f c (Quot.mk r a) = f a
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesColimit
_private.Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesColimit.0.SSet.isColimitCoconeN.fac_assoc : ∀ {X : SSet} (s : CategoryTheory.Limits.Cocone X.functorN) (x : X.N) {Z : SSet} (h : s.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp x.subcomplex.ι
      (CategoryTheory.CategoryStruct.comp (SSet.Subcomplex.topIso X).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.Multicofork.IsColimit.desc ⋯.isColimit (fun x => s.ι.app x) ⋯) h)) =
    CategoryTheory.CategoryStruct.comp (s.ι.app x) h
-- Mathlib.GroupTheory.SpecificGroups.Alternating
alternatingGroup.conj_smul_range_ofSubtype : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (s : Finset α) (g : ↥(alternatingGroup α)),
  MulAut.conj g • (alternatingGroup.ofSubtype s).range = (alternatingGroup.ofSubtype (g • s)).range
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.instGroup : {ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Group (G i)] → [inst_1 : Group H] → {φ : (i : ι) → H →* G i} → Group (Monoid.PushoutI φ)
-- Init.Data.SInt.Basic
Int8.ofUInt8.inj : ∀ {toUInt8 toUInt8_1 : UInt8}, { toUInt8 := toUInt8 } = { toUInt8 := toUInt8_1 } → toUInt8 = toUInt8_1
-- Mathlib.Algebra.Prime.Lemmas
not_irreducible_of_not_isUnit_of_dvdNotUnit : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {p q : M}, ¬IsUnit p → DvdNotUnit p q → ¬Irreducible q
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.congr_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.TreeSet α cmp}, t₁.Equiv t₂ → (t₃.Equiv t₁ ↔ t₃.Equiv t₂)
-- Mathlib.Analysis.Convex.Body
ConvexBody.hausdorffDist_coe : ∀ {V : Type u_1} [inst : SeminormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] (K L : ConvexBody V),
  Metric.hausdorffDist ↑K ↑L = dist K L
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.instEssSurjCompPre : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {B : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} B] (S : D) (F : CategoryTheory.Functor B C)
  (G : CategoryTheory.Functor C D) [F.EssSurj], (CategoryTheory.StructuredArrow.pre S F G).EssSurj
-- Mathlib.Tactic.Simproc.Divisors
_private.Mathlib.Tactic.Simproc.Divisors.0.Nat.properDivisors_ofNat.unsafe_impl_2 : ℕ → List ℕ
-- Mathlib.Algebra.GradedMulAction
SetLike.coe_GSMul : ∀ {ιA : Type u_1} {ιB : Type u_2} {S : Type u_5} {R : Type u_6} {N : Type u_7} {M : Type u_8} [inst : SetLike S R]
  [inst_1 : SetLike N M] [inst_2 : SMul R M] [inst_3 : VAdd ιA ιB] (A : ιA → S) (B : ιB → N)
  [inst_4 : SetLike.GradedSMul A B] {i : ιA} {j : ιB} (x : ↥(A i)) (y : ↥(B j)),
  ↑(GradedMonoid.GSMul.smul x y) = ↑x • ↑y
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
/-- For every set `s` and a countable collection of measures `μ i` there exists a measurable
superset `t ⊇ s` such that each measure `μ i` takes the same value on `s` and `t`.  -/
MeasureTheory.exists_measurable_superset_forall_eq : ∀ {α : Type u_1} {ι : Sort u_5} [inst : MeasurableSpace α] [Countable ι] (μ : ι → MeasureTheory.Measure α) (s : Set α),
  ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ (i : ι), (μ i) t = (μ i) s
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.lt_aleph_one_iff : ∀ {c : Cardinal.{u_1}}, c < Cardinal.aleph 1 ↔ c ≤ Cardinal.aleph0
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.normAtComplexPlaces_apply_isComplex : ∀ {K : Type u_1} [inst : Field K] {x : NumberField.mixedEmbedding.mixedSpace K} (w : { w // w.IsComplex }),
  NumberField.mixedEmbedding.normAtComplexPlaces x ↑w = ‖x.2 w‖
-- Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
BoundedVariationOn.vectorMeasure_Iio : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : DenselyOrdered α] [inst_2 : TopologicalSpace α]
  [inst_3 : OrderTopology α] [inst_4 : SecondCountableTopology α] [inst_5 : CompactIccSpace α] [hα : MeasurableSpace α]
  [inst_6 : BorelSpace α] {E : Type u_2} [inst_7 : NormedAddCommGroup E] [inst_8 : CompleteSpace E] {f : α → E}
  (hf : BoundedVariationOn f Set.univ) (a : α),
  hf.vectorMeasure (Set.Iio a) = Function.leftLim f a - Filter.atBot.limUnder f
-- Init.Data.String.Basic
/-- Creates a new string that consists of the region of the input string delimited by the two positions.

The result is `""` if the start position is greater than or equal to the end position or if the
start position is at the end of the string. If either position is invalid (that is, if either points
at the middle of a multi-byte UTF-8 character) then the result is unspecified.

This is a legacy function. The recommended alternative is `String.Pos.extract`, but usually
it is even better to operate on `String.Slice` instead and call `String.Slice.copy` (only) if
required.

Examples:
* `"red green blue".extract ⟨0⟩ ⟨3⟩ = "red"`
* `"red green blue".extract ⟨3⟩ ⟨0⟩ = ""`
* `"red green blue".extract ⟨0⟩ ⟨100⟩ = "red green blue"`
* `"red green blue".extract ⟨4⟩ ⟨100⟩ = "green blue"`
* `"L∃∀N".extract ⟨1⟩ ⟨2⟩ = "∃∀N"`
* `"L∃∀N".extract ⟨2⟩ ⟨100⟩ = ""`
 -/
String.Pos.Raw.extract : String → String.Pos.Raw → String.Pos.Raw → String
-- Init.Data.Rat.Lemmas
Rat.pow_pos : ∀ {a : ℚ} {n : ℕ}, 0 < a → 0 < a ^ n
-- Mathlib.NumberTheory.Padics.AddChar
/-- Equivalence between continuous additive characters `ℤ_[p] → R`, and `r ∈ R` with `‖r‖ < 1`,
for rings with strictly multiplicative norm.  -/
PadicInt.continuousAddCharEquiv_of_norm_mul : (p : ℕ) →
  [inst : Fact (Nat.Prime p)] →
    (R : Type u_1) →
      [inst_1 : NormedRing R] →
        [inst_2 : Algebra ℤ_[p] R] →
          [IsBoundedSMul ℤ_[p] R] →
            [IsUltrametricDist R] → [CompleteSpace R] → [NormMulClass R] → { κ // Continuous ⇑κ } ≃ { r // ‖r‖ < 1 }
-- Init.Data.Range.Basic
_private.Init.Data.Range.Basic.0.Std.Legacy.Range.forM.loop : {m : Type u_1 → Type u_2} → [Monad m] → Std.Legacy.Range → (ℕ → m PUnit.{u_1 + 1}) → ℕ → m PUnit.{u_1 + 1}
-- Batteries.Data.ByteArray
ByteArray.get_append_right : ∀ {i : ℕ} {a b : ByteArray} (hle : a.size ≤ i) (h : i < (a ++ b).size) (h' : optParam (i - a.size < b.size) ⋯),
  (a ++ b)[i] = b[i - a.size]
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isCoseparator_prod_of_isCoseparator_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] (G H : C)
  [inst_2 : CategoryTheory.Limits.HasBinaryProduct G H],
  CategoryTheory.IsCoseparator H → CategoryTheory.IsCoseparator (G ⨯ H)
-- Mathlib.Data.Real.Basic
Real.mk_pos : ∀ {f : CauSeq ℚ abs}, 0 < Real.mk f ↔ f.Pos
-- Mathlib.Order.Lattice
Monotone.of_map_inf_le : ∀ {α : Type u} {β : Type v} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β] {f : α → β},
  (∀ (x y : α), f (x ⊓ y) ≤ f x ⊓ f y) → Monotone f
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.getKey? : {α : Type u} → {β : α → Type v} → [BEq α] → α → List ((a : α) × β a) → Option α