mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Basic
Lean.Meta.Context.mk.inj : ∀ {keyedConfig : Lean.Meta.ConfigWithKey} {trackZetaDelta : Bool} {zetaDeltaSet : Lean.FVarIdSet}
  {lctx : Lean.LocalContext} {localInstances : Lean.LocalInstances} {defEqCtx? : Option Lean.Meta.DefEqContext}
  {synthPendingDepth : ℕ} {canUnfold? : Option (Lean.Meta.Config → Lean.ConstantInfo → Lean.CoreM Bool)}
  {univApprox inTypeClassResolution cacheInferType : Bool} {keyedConfig_1 : Lean.Meta.ConfigWithKey}
  {trackZetaDelta_1 : Bool} {zetaDeltaSet_1 : Lean.FVarIdSet} {lctx_1 : Lean.LocalContext}
  {localInstances_1 : Lean.LocalInstances} {defEqCtx?_1 : Option Lean.Meta.DefEqContext} {synthPendingDepth_1 : ℕ}
  {canUnfold?_1 : Option (Lean.Meta.Config → Lean.ConstantInfo → Lean.CoreM Bool)}
  {univApprox_1 inTypeClassResolution_1 cacheInferType_1 : Bool},
  { keyedConfig := keyedConfig, trackZetaDelta := trackZetaDelta, zetaDeltaSet := zetaDeltaSet, lctx := lctx,
        localInstances := localInstances, defEqCtx? := defEqCtx?, synthPendingDepth := synthPendingDepth,
        canUnfold? := canUnfold?, univApprox := univApprox, inTypeClassResolution := inTypeClassResolution,
        cacheInferType := cacheInferType } =
      { keyedConfig := keyedConfig_1, trackZetaDelta := trackZetaDelta_1, zetaDeltaSet := zetaDeltaSet_1,
        lctx := lctx_1, localInstances := localInstances_1, defEqCtx? := defEqCtx?_1,
        synthPendingDepth := synthPendingDepth_1, canUnfold? := canUnfold?_1, univApprox := univApprox_1,
        inTypeClassResolution := inTypeClassResolution_1, cacheInferType := cacheInferType_1 } →
    keyedConfig = keyedConfig_1 ∧
      trackZetaDelta = trackZetaDelta_1 ∧
        zetaDeltaSet = zetaDeltaSet_1 ∧
          lctx = lctx_1 ∧
            localInstances = localInstances_1 ∧
              defEqCtx? = defEqCtx?_1 ∧
                synthPendingDepth = synthPendingDepth_1 ∧
                  canUnfold? = canUnfold?_1 ∧
                    univApprox = univApprox_1 ∧
                      inTypeClassResolution = inTypeClassResolution_1 ∧ cacheInferType = cacheInferType_1
-- Init.Data.Array.Lemmas
Array.back_singleton : ∀ {α : Type u_1} {a : α}, #[a].back ⋯ = a
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.instCoeOutLinearEquivId : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid A] →
          [inst_2 : AddCommMonoid B] →
            [inst_3 : Module R A] →
              [inst_4 : Module R B] →
                [inst_5 : CoalgebraStruct R A] → [inst_6 : CoalgebraStruct R B] → CoeOut (A ≃ₗc[R] B) (A ≃ₗ[R] B)
-- Mathlib.Logic.Lemmas
Prop.forall : ∀ {f : Prop → Prop}, (∀ (p : Prop), f p) ↔ f True ∧ f False
-- Mathlib.Order.BoundedOrder.Basic
ULift.instOrderTop : {α : Type u} → [inst : LE α] → [OrderTop α] → OrderTop (ULift.{v, u} α)
-- Mathlib.Topology.MetricSpace.DilationEquiv
IsometryEquiv.toDilationEquiv_ratio : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (e : X ≃ᵢ Y),
  Dilation.ratio e.toDilationEquiv = 1
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
/-- Given a splitting `s` of a simplicial object `X` in a preadditive category,
this is the homotopy equivalence from the alternating face map complex of `X`
to the chain complex `s.nondegComplex`.  -/
CategoryTheory.SimplicialObject.Splitting.homotopyEquivNondegComplex : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : CategoryTheory.SimplicialObject C} →
      (s : X.Splitting) →
        [inst_1 : CategoryTheory.Preadditive C] →
          HomotopyEquiv (AlgebraicTopology.AlternatingFaceMapComplex.obj X) s.nondegComplex
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.counitInv_naturality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {X Y : D} (f : Y ⟶ X),
  CategoryTheory.CategoryStruct.comp (e.counitInv.app Y) (e.functor.map (e.inverse.map f)) =
    CategoryTheory.CategoryStruct.comp f (e.counitInv.app X)
-- Mathlib.Topology.Constructions
ULift.isOpen_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set (ULift.{v, u} X)}, IsOpen s ↔ IsOpen (ULift.up ⁻¹' s)
-- Batteries.Data.PairingHeap
/-- `O(1)`. Is the heap empty?  -/
Batteries.PairingHeapImp.Heap.isEmpty : {α : Type u_1} → Batteries.PairingHeapImp.Heap α → Bool
-- Mathlib.RingTheory.SimpleModule.Basic
IsSemisimpleModule.exists_sSupIndep_sSup_simples_eq_top : ∀ (R : Type u_2) [inst : Ring R] (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [IsSemisimpleModule R M], ∃ s, sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
-- Init.Data.Vector.Lemmas
Vector.toArray_insertIdx : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} {x : α} (h : i ≤ n),
  (xs.insertIdx i x h).toArray = xs.toArray.insertIdx i x ⋯
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.const_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (x : β), CauSeq.const abv (-x) = -CauSeq.const abv x
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
IsCovariantDerivativeOn.mk : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)]
  [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] [inst_14 : FiberBundle F V]
  {cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x} {s : optParam (Set M) Set.univ},
  (∀ {σ σ' : (x : M) → V x} {x : M},
      MDiffAt (T% σ) x →
        MDiffAt (T% σ') x → autoParam (x ∈ s) IsCovariantDerivativeOn._auto_1 → cov (σ + σ') x = cov σ x + cov σ' x) →
    (∀ {σ : (x : M) → V x} {g : M → 𝕜} {x : M},
        MDiffAt (T% σ) x →
          MDiffAt g x →
            autoParam (x ∈ s) IsCovariantDerivativeOn._auto_3 →
              cov (g • σ) x = g x • cov σ x + (d% g x).smulRight (σ x)) →
      IsCovariantDerivativeOn F cov s
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.mapWithPostcondition.eq_1 : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {m : Type w → Type w'} [inst_1 : Monad m]
  (f : β → Std.Iterators.PostconditionT m γ) (it : Std.Iter β),
  Std.Iter.mapWithPostcondition f it = Std.IterM.mapWithPostcondition f it.toIterM
-- Lean.Meta.Tactic.LibrarySearch
Lean.Meta.LibrarySearch.instHashableDeclMod : Hashable Lean.Meta.LibrarySearch.DeclMod
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
/-- Auxiliary definition for `leftAdjointObjIsDefined_of_isColimit`.  -/
CategoryTheory.Functor.corepresentableByCompCoyonedaObjOfIsColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor D C} →
          {J : Type u_1} →
            [inst_2 : CategoryTheory.Category.{v_1, u_1} J] →
              {R : CategoryTheory.Functor J F.PartialLeftAdjointSource} →
                {c : CategoryTheory.Limits.Cocone (R.comp F.leftAdjointObjIsDefined.ι)} →
                  CategoryTheory.Limits.IsColimit c →
                    {c' : CategoryTheory.Limits.Cocone (R.comp F.partialLeftAdjoint)} →
                      CategoryTheory.Limits.IsColimit c' →
                        (F.comp (CategoryTheory.coyoneda.obj (Opposite.op c.pt))).CorepresentableBy c'.pt
-- Mathlib.Topology.Algebra.FilterBasis
AddGroupFilterBasis.nhds_zero_hasBasis : ∀ {G : Type u} [inst : AddGroup G] (B : AddGroupFilterBasis G), (nhds 0).HasBasis (fun V => V ∈ B) id
-- Init.Data.String.PosRaw
String.Pos.Raw.zero_addString_eq : ∀ (s : String), 0 + s = { byteIdx := s.utf8ByteSize }
-- Mathlib.Topology.Connected.TotallyDisconnected
ConnectedComponents.totallyDisconnectedSpace : ∀ {α : Type u} [inst : TopologicalSpace α], TotallyDisconnectedSpace (ConnectedComponents α)
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.xz_succ : ∀ {a : ℕ} (a1 : 1 < a) (n : ℕ), Pell.xz a1 (n + 1) = Pell.xz a1 n * Pell.az a + ↑(Pell.d✝ a1) * Pell.yz a1 n
-- Mathlib.Data.Complex.Basic
Complex.div_ofNat : ∀ (z : ℂ) (n : ℕ) [inst : n.AtLeastTwo], z / OfNat.ofNat n = { re := z.re / OfNat.ofNat n, im := z.im / OfNat.ofNat n }
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.type_eq : ∀ {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder α r] [inst_1 : IsWellOrder β s],
  Ordinal.type r = Ordinal.type s ↔ Nonempty (r ≃r s)
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.equivalence_functor_map : ∀ {X Y : AddCommMonCat} (f : X ⟶ Y),
  AddCommMonCat.equivalence.functor.map f = CommMonCat.ofHom (AddMonoidHom.toMultiplicative (AddCommMonCat.Hom.hom f))
-- Mathlib.Data.Nat.Prime.Basic
Nat.not_prime_of_mul_eq : ∀ {a b n : ℕ}, a * b = n → a ≠ 1 → b ≠ 1 → ¬Nat.Prime n
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.SuperpolynomialDecay.param_inv_mul : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {k f : α → β} [inst : TopologicalSpace β] [inst_1 : Field β]
  [inst_2 : LinearOrder β] [IsStrictOrderedRing β] [OrderTopology β],
  Filter.Tendsto k l Filter.atTop →
    Asymptotics.SuperpolynomialDecay l k f → Asymptotics.SuperpolynomialDecay l k (f * k⁻¹)
-- Mathlib.RingTheory.SimpleRing.Principal
instIsSimpleOrderIdeal : ∀ {R : Type u_1} [inst : CommRing R] [IsSimpleRing R], IsSimpleOrder (Ideal R)
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instInvolutiveNeg.eq_1 : ∀ {α : Type u_1} [inst : InvolutiveNeg α], OrderDual.instInvolutiveNeg = { toNeg := OrderDual.instNeg, neg_neg := ⋯ }
-- Init.Data.BitVec.Bitblast
/-- Extract the `k`-th bit from `x` and extend it to have length `len`.  -/
BitVec.extractAndExtendBit : {w : ℕ} → ℕ → (len : ℕ) → BitVec w → BitVec len
-- Lean.Parser.Extra
Lean.Parser.many1.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Lean.Declaration
Lean.ConstructorVal.mk : Lean.ConstantVal → Lean.Name → ℕ → ℕ → ℕ → Bool → Lean.ConstructorVal
-- Mathlib.MeasureTheory.Measure.AEDisjoint
MeasureTheory.AEDisjoint.comm : ∀ {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.AEDisjoint μ s t ↔ MeasureTheory.AEDisjoint μ t s
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
/-- `weakPullback f g` computes the weak pullback of a pair of morphisms
with the same target.  -/
CategoryTheory.Limits.weakPullback : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → [CategoryTheory.Limits.HasWeakPullback f g] → C
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.spanCompIso_inv_app_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z),
  (CategoryTheory.Limits.spanCompIso F f g).inv.app CategoryTheory.Limits.WalkingSpan.left =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Limits.span (F.map f) (F.map g)).obj CategoryTheory.Limits.WalkingSpan.left)
-- Mathlib.Topology.GDelta.Basic
/-- The union of finitely many Gδ sets is a Gδ set, `Set.sUnion` version.  -/
IsGδ.sUnion : ∀ {X : Type u_1} [inst : TopologicalSpace X] {S : Set (Set X)}, S.Finite → (∀ s ∈ S, IsGδ s) → IsGδ (⋃₀ S)
-- Mathlib.Tactic.Linarith.Parsing
/-- `1` is represented by the empty monomial, the product of no variables.  -/
Mathlib.Tactic.Linarith.Monom.one : Mathlib.Tactic.Linarith.Monom
-- Mathlib.Algebra.Homology.BifunctorShift
HomologicalComplex₂.shiftFunctor₂XXIso.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (a b y b' : ℤ) (h : b' = b + y),
  K.shiftFunctor₂XXIso a b y b' h = CategoryTheory.eqToIso ⋯
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.lift_of' : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : AddMonoid M] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] (F : Multiplicative M →* A) (x : M),
  ((AddMonoidAlgebra.lift R A M) F) (AddMonoidAlgebra.of' R M x) = F (Multiplicative.ofAdd x)
-- Mathlib.CategoryTheory.Preadditive.CommGrp_
CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_grp_one : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.BraidedCategory C] (X : C),
  CategoryTheory.MonObj.one = 0
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- The congruence relation on `M × S`, `M` an `AddCommMonoid` and `S` an `AddSubmonoid` of `M`,
whose quotient is the localization of `M` at `S`, defined as the unique congruence relation on
`M × S` such that for any other congruence relation `s` on `M × S` where for all `y ∈ S`,
`(0, 0) ∼ (y, y)` under `s`, we have that `(x₁, y₁) ∼ (x₂, y₂)` by `r` implies
`(x₁, y₁) ∼ (x₂, y₂)` by `s`.  -/
AddLocalization.r : {M : Type u_1} → [inst : AddCommMonoid M] → (S : AddSubmonoid M) → AddCon (M × ↥S)
-- Mathlib.Order.Filter.Basic
Filter.compl_mem_comk : ∀ {α : Type u_1} {p : Set α → Prop} {he : p ∅} {hmono : ∀ (t : Set α), p t → ∀ s ⊆ t, p s}
  {hunion : ∀ (s : Set α), p s → ∀ (t : Set α), p t → p (s ∪ t)} {s : Set α}, sᶜ ∈ Filter.comk p he hmono hunion ↔ p s
-- Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
/-- If `f` is complex meromorphic on a circle in the complex plane, then `log ‖f ·‖` is circle
integrable over that circle.
 -/
MeromorphicOn.circleIntegrable_log_norm : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {c : ℂ} {R : ℝ} {f : ℂ → E},
  MeromorphicOn f (Metric.sphere c |R|) → CircleIntegrable (fun x => Real.log ‖f x‖) c R
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.trans_toContinuousLinearEquiv : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Semiring C]
  [inst_6 : TopologicalSpace C] [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : Algebra R C] (e₁ : A ≃A[R] B)
  (e₂ : B ≃A[R] C), ↑(e₁.trans e₂) = (↑e₁).trans ↑e₂
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.lambdaMetaTelescope.process : Option ℕ →
  Array Lean.Expr →
    Array Lean.BinderInfo → ℕ → Lean.Expr → Lean.MetaM (Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr)
-- Mathlib.Algebra.Group.Hom.End
AddMonoid.End.instSemiring : {M : Type uM} → [inst : AddCommMonoid M] → Semiring (AddMonoid.End M)
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- `c.divMod b a` (i.e. `c / b mod a`) is an arbitrary `x` such that `c = bx + a`.
This is zero if the above is not possible, i.e. when `a = 0` or `b = 0` or `¬ a ≤ c`.  -/
FractionalIdeal.divMod : {R : Type u_1} →
  [inst : CommRing R] →
    {K : Type u_2} →
      [inst_1 : Field K] →
        [inst_2 : Algebra R K] →
          [IsFractionRing R K] →
            [IsDedekindDomain R] →
              FractionalIdeal (nonZeroDivisors R) K →
                FractionalIdeal (nonZeroDivisors R) K → FractionalIdeal (nonZeroDivisors R) K → K
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of the forward direction of `SimpleGraph.Walk.isCircuit_rotate`. -/
SimpleGraph.Walk.IsCircuit.of_rotate : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : DecidableEq V] {c : G.Walk v v} (hu : u ∈ c.support),
  (c.rotate u hu).IsCircuit → c.IsCircuit
-- Lean.Message
Lean.MessageData.ofGoal.sizeOf_spec : ∀ (a : Lean.MVarId), sizeOf (Lean.MessageData.ofGoal a) = 1 + sizeOf a
-- Init.Data.Vector.Lemmas
Vector.sum_append : ∀ {α : Type u_1} {n m : ℕ} [inst : Zero α] [inst_1 : Add α] [Std.Associative fun x1 x2 => x1 + x2]
  [Std.LeftIdentity (fun x1 x2 => x1 + x2) 0] [Std.LawfulLeftIdentity (fun x1 x2 => x1 + x2) 0] {as₁ : Vector α n}
  {as₂ : Vector α m}, (as₁ ++ as₂).sum = as₁.sum + as₂.sum
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.nonsingularLift_iff : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P : Fin 3 → R),
  W'.NonsingularLift ⟦P⟧ ↔ W'.Nonsingular P
-- Mathlib.RingTheory.PowerSeries.Basic
Polynomial.pUnitAlgEquiv_symm_toPowerSeries : ∀ {R : Type u_1} [inst : CommSemiring R] {f : Polynomial R}, ↑f = ↑((MvPolynomial.uniqueAlgEquiv R PUnit.{1}).symm f)
-- Mathlib.Algebra.Order.Quantale
/-- Left- and right- residuation operators on a quantale are similar to the Heyting
operator on complete lattices, but for a non-commutative logic.
I.e. `x ≤ y ⇨ᵣ z ↔ y * x ≤ z` or alternatively `x ⇨ₗ y = sSup { z | x * z ≤ y }`.
 -/
Quantale.«term_⇨ᵣ_» : Lean.TrailingParserDescr
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_insertList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α}
  (not_contains : (List.map Sigma.fst toInsert).contains k = false)
  {h : Std.Internal.List.containsKey k (Std.Internal.List.insertList l toInsert) = true},
  Std.Internal.List.getKey k (Std.Internal.List.insertList l toInsert) h = Std.Internal.List.getKey k l ⋯
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.instSemilatticeInf : {α : Type u_1} →
  [inst : TopologicalSpace α] → [QuasiSeparatedSpace α] → SemilatticeInf (TopologicalSpace.CompactOpens α)
-- Mathlib.Algebra.Category.BoolRing
/-- Construct a bundled `BoolRing` from a `BooleanRing`.  -/
BoolRing.of : (carrier : Type u) → [booleanRing : BooleanRing carrier] → BoolRing
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_minKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → t.contains t.minKey! = true
-- Mathlib.Data.Part
Part.Mem.left_unique : ∀ {α : Type u_1}, Relator.LeftUnique fun x1 x2 => x1 ∈ x2
-- Mathlib.Order.WithBot
WithBot.map_eq_some_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {y : β} {v : WithBot α}, WithBot.map f v = ↑y ↔ ∃ x, v = ↑x ∧ f x = y
-- Mathlib.NumberTheory.Divisors
Nat.properDivisors_zero : Nat.properDivisors 0 = ∅
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.re_sub : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : AddGroup R] (a b : QuaternionAlgebra R c₁ c₂ c₃), (a - b).re = a.re - b.re
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntry?.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (size : ℕ) (k' : α) (v : β k')
  (l r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k' v l r).getEntry? k =
    match compare k k' with
    | Ordering.lt => l.getEntry? k
    | Ordering.gt => r.getEntry? k
    | Ordering.eq => some ⟨k', v⟩
-- Mathlib.Data.Fin.Tuple.Take
/-- `take` is the same after `update` for indices outside the range of `take`.  -/
Fin.take_update_of_ge : ∀ {n : ℕ} {α : Fin n → Sort u_1} (m : ℕ) (h : m ≤ n) (v : (i : Fin n) → α i) (i : Fin n),
  ↑i ≥ m → ∀ (x : α i), Fin.take m h (Function.update v i x) = Fin.take m h v
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.ediam_range : ∀ {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₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂), Metric.ediam (Set.range ⇑f) = Metric.ediam Set.univ
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.isEmpty_takeEndWhile_eq_true : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice}, s.endsWith pat = false → (s.takeEndWhile pat).isEmpty = true
-- Mathlib.Order.Interval.Set.Fin
Fin.image_castSucc_uIoc : ∀ {n : ℕ} (i j : Fin n), Fin.castSucc '' Set.uIoc i j = Set.uIoc i.castSucc j.castSucc
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.Slice.startsWith_string_eq_false_iff : ∀ {pat : String} {s : String.Slice}, s.startsWith pat = false ↔ ¬pat.toList <+: s.copy.toList
-- Mathlib.RingTheory.Kaehler.TensorProduct
KaehlerDifferential.mulActionBaseChange_smul_zero : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing A] [inst_4 : Algebra R A] (a : A), a • 0 = 0
-- Mathlib.Data.Multiset.Powerset
/-- A helper function for the powerset of a multiset. Given a list `l`, returns a list
of sublists of `l` as multisets.  -/
Multiset.powersetAux : {α : Type u_1} → List α → List (Multiset α)
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.instIsIsoF : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c}
  (f : C₁ ⟶ C₂) [CategoryTheory.IsIso f] (j : ι), CategoryTheory.IsIso (f.f j)
-- Mathlib.Data.FinEnum
/-- `FinEnum α` means that `α` is finite and can be enumerated in some order,
i.e. `α` has an explicit bijection with `Fin n` for some n.  -/
FinEnum : Sort u_1 → Sort (max 1 u_1)
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.map_surjective_iff : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁),
  Function.Surjective ⇑(MvPolynomial.map f) ↔ Function.Surjective ⇑f
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey_le_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  (hc : k ∈ t), (cmp (t.minKey ⋯) k).isLE = true
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
/-- the index type  -/
SSet.Subcomplex.PairingCore.ι : {X : SSet} → {A : X.Subcomplex} → A.PairingCore → Type v
-- Init.Data.SInt.Bitwise
Int64.not_eq_neg_sub : ∀ (a : Int64), ~~~a = -a - 1
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.coe_one : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : MonoidWithZero B] (f : A →*₀ B), ⟨1, ⋯⟩ = 1
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.isZero_X₂_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C}, S.Exact → (CategoryTheory.Limits.IsZero S.X₂ ↔ S.f = 0 ∧ S.g = 0)
-- Mathlib.Analysis.CStarAlgebra.Classes
instNonUnitalCStarAlgebraSubtypeMemNonUnitalStarSubalgebraComplexElemental : {A : Type u_1} →
  [inst : NonUnitalCStarAlgebra A] → (x : A) → NonUnitalCStarAlgebra ↥(NonUnitalStarAlgebra.elemental ℂ x)
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
CategoryTheory.ShortComplex.ShortExact.mapShiftedHom_singleδ' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Abelian D] [inst_4 : HasDerivedCategory C]
  [inst_5 : HasDerivedCategory D] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact)
  (F : CategoryTheory.Functor C D) [inst_6 : F.Additive] [inst_7 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_8 : CategoryTheory.Limits.PreservesFiniteColimits F],
  CategoryTheory.CategoryStruct.comp ((F.mapDerivedCategorySingleFunctor 0).inv.app S.X₃)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShiftedHom.map hS.singleδ F.mapDerivedCategory)
        ((CategoryTheory.shiftFunctor (DerivedCategory D) 1).map
          ((F.mapDerivedCategorySingleFunctor 0).hom.app S.X₁))) =
    ⋯.singleδ
-- Init.Data.ByteArray.Lemmas
ByteArray.getElem!_push_eq : ∀ (data : ByteArray) (b : UInt8), (data.push b)[data.size]! = b
-- Mathlib.GroupTheory.Divisible
ULift.instRootableBy.eq_1 : ∀ (A : Type u_1) (α : Type u_2) [inst : Monoid A] [inst_1 : Pow A α] [inst_2 : Zero α] [inst_3 : RootableBy A α],
  ULift.instRootableBy A α =
    { root := fun x a => { down := RootableBy.root x.down a }, root_zero := ⋯, root_cancel := ⋯ }