mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Sat.AIG.If
Std.Sat.AIG.denote_mkIfCached : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {assign : α → Bool} {aig : Std.Sat.AIG α}
  {input : aig.TernaryInput},
  ⟦assign, aig.mkIfCached input⟧ =
    if ⟦assign, { aig := aig, ref := input.discr }⟧ = true then ⟦assign, { aig := aig, ref := input.lhs }⟧
    else ⟦assign, { aig := aig, ref := input.rhs }⟧
-- Mathlib.Order.Defs.LinearOrder
Ordering.Compares.eq_3 : ∀ {α : Type u_1} [inst : LT α] (x x_1 : α), Ordering.gt.Compares x x_1 = (x > x_1)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey_unitOfList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
      k ∈ l →
        ∀ {h' : k' ∈ Std.ExtDTreeMap.Const.unitOfList l cmp}, (Std.ExtDTreeMap.Const.unitOfList l cmp).getKey k' h' = k
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.succ_mem_succ_iff : ∀ {α : Type u} [inst : LE α] [DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LinearlyUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.PRange.InfinitelyUpwardEnumerable α] [Std.Rxc.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α]
  {hi a : α}, (Std.PRange.succ a ∈ *...=Std.PRange.succ hi) ↔ a ∈ *...=hi
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
tendstoLocallyUniformly_iff_filter : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {p : Filter ι}, TendstoLocallyUniformly F f p ↔ ∀ (x : α), TendstoUniformlyOnFilter F f p (nhds x)
-- Lean.Elab.DefView
/-- Snapshot after syntax tree has been split into separate mutual def headers.  -/
Lean.Elab.DefsParsedSnapshot : Type
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.inner_self_im : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] (x : F), RCLike.im (inner 𝕜 x x) = 0
-- Mathlib.Order.Lattice
Prod.fst_sup : ∀ (α : Type u) (β : Type v) [inst : Max α] [inst_1 : Max β] (p q : α × β), (p ⊔ q).1 = p.1 ⊔ q.1
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.instPseudoMetricSpace : (α : Type u_1) →
  (β : Type u_2) →
    [inst : TopologicalSpace α] → [CompactSpace α] → [inst_2 : PseudoMetricSpace β] → PseudoMetricSpace C(α, β)
-- Mathlib.Order.Filter.IndicatorFunction
tendsto_mulIndicator_biUnion_finset : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_5} [inst : One β] (s : ι → Set α) (f : α → β) (a : α),
  Filter.Tendsto (fun n => (⋃ i ∈ n, s i).mulIndicator f a) Filter.atTop (pure ((Set.iUnion s).mulIndicator f a))
-- Mathlib.NumberTheory.FrobeniusNumber
Nat.setGcd_eq_zero_iff : ∀ {s : Set ℕ}, Nat.setGcd s = 0 ↔ s ⊆ {0}
-- Mathlib.RingTheory.LocalProperties.Exactness
injective_of_isLocalization_of_span_eq_top : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] {s : Set R},
  Ideal.span s = ⊤ →
    ∀ (Rᵣ : ↑s → Type u_3) [inst_2 : (r : ↑s) → CommSemiring (Rᵣ r)] [inst_3 : (r : ↑s) → Algebra R (Rᵣ r)]
      (Sᵣ : ↑s → Type u_4) [inst_4 : (r : ↑s) → CommSemiring (Sᵣ r)] [inst_5 : (r : ↑s) → Algebra S (Sᵣ r)]
      (f : R →+* S) [inst_6 : ∀ (r : ↑s), IsLocalization.Away (↑r) (Rᵣ r)]
      [inst_7 : ∀ (r : ↑s), IsLocalization.Away (f ↑r) (Sᵣ r)],
      (∀ (r : ↑s), Function.Injective ⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f ↑r)) → Function.Injective ⇑f
-- Mathlib.Order.Interval.Set.OrdConnected
Set.ordConnected_preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {F : Type u_3} [inst_2 : FunLike F α β]
  [OrderHomClass F α β] (f : F) {s : Set β} [hs : s.OrdConnected], (⇑f ⁻¹' s).OrdConnected
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.node4L.match_1.splitter : {α : Type u_1} →
  (motive : Ordnode α → α → Ordnode α → α → Ordnode α → Sort u_2) →
    (x : Ordnode α) →
      (x_1 : α) →
        (x_2 : Ordnode α) →
          (x_3 : α) →
            (x_4 : Ordnode α) →
              ((l : Ordnode α) →
                  (x : α) →
                    (size : ℕ) →
                      (ml : Ordnode α) →
                        (y : α) →
                          (mr : Ordnode α) → (z : α) → (r : Ordnode α) → motive l x (Ordnode.node size ml y mr) z r) →
                ((l : Ordnode α) → (x z : α) → (r : Ordnode α) → motive l x Ordnode.nil z r) → motive x x_1 x_2 x_3 x_4
-- Mathlib.RingTheory.Polynomial.Pochhammer
ascPochhammer_succ_comp_X_add_one : ∀ (S : Type u) [inst : Semiring S] (n : ℕ),
  (ascPochhammer S (n + 1)).comp (Polynomial.X + 1) =
    ascPochhammer S (n + 1) + (n + 1) • (ascPochhammer S n).comp (Polynomial.X + 1)
-- Lean.Util.Recognizers
Lean.Expr.ne? : Lean.Expr → Option (Lean.Expr × Lean.Expr × Lean.Expr)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.w_prod_fst_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (S : CategoryTheory.Functor C D) (S' : CategoryTheory.Functor C' D')
  (T : D) (T' : D') {A B : CategoryTheory.CostructuredArrow (S.prod S') (T, T')} (f : A ⟶ B) {Z : D} (h : T ⟶ Z),
  CategoryTheory.CategoryStruct.comp (S.map f.left.1) (CategoryTheory.CategoryStruct.comp B.hom.1 h) =
    CategoryTheory.CategoryStruct.comp A.hom.1 h
-- Mathlib.Order.Hom.Bounded
instCoeTCTopHomOfTopHomClass.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Top α] [inst_2 : Top β]
  [inst_3 : TopHomClass F α β], instCoeTCTopHomOfTopHomClass = { coe := TopHomClass.toTopHom }
-- Mathlib.RepresentationTheory.Basic
Representation.ofDistribMulAction.congr_simp : ∀ (k : Type u_1) (G : Type u_2) (A : Type u_3) [inst : Semiring k] [inst_1 : Monoid G] [inst_2 : AddCommMonoid A]
  [inst_3 : Module k A] [inst_4 : DistribMulAction G A] [inst_5 : SMulCommClass G k A],
  Representation.ofDistribMulAction k G A = Representation.ofDistribMulAction k G A
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
_private.Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform.0.EisensteinSeries.aux_identity : ∀ (z : UpperHalfPlane) (b n : ℤ),
  (↑b * ↑z + ↑n + 1)⁻¹ * ((↑b * ↑z + ↑n) ^ 2)⁻¹ + EisensteinSeries.δ✝ ![b, n] +
      ((↑b * ↑z + ↑n)⁻¹ - (↑b * ↑z + ↑n + 1)⁻¹) =
    ((↑b * ↑z + ↑n) ^ 2)⁻¹
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.isPatternDontCare : Lean.Expr → Bool
-- Mathlib.LinearAlgebra.Dual.Lemmas
ULift.instModuleIsReflexive : ∀ (R : Type u_1) (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.IsReflexive R M], Module.IsReflexive R (ULift.{w, u_2} M)
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.SurjectiveOfEpiAuxs.agree : ∀ {A B : GrpCat} (f : A ⟶ B),
  ↑(GrpCat.Hom.hom f).range = {x | (GrpCat.SurjectiveOfEpiAuxs.h f) x = (GrpCat.SurjectiveOfEpiAuxs.g f) x}
-- Aesop.Forward.State
/-- The initial (empty) rule state for a given forward rule.  -/
Aesop.ForwardRule.initialRuleState : Aesop.ForwardRule → Aesop.RuleState
-- Mathlib.Analysis.Calculus.FDeriv.Congr
DifferentiableWithinAt.congr_of_eventuallyEq_of_mem : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f f₁ : E → F} {x : E} {s : Set E},
  DifferentiableWithinAt 𝕜 f s x → f₁ =ᶠ[nhdsWithin x s] f → x ∈ s → DifferentiableWithinAt 𝕜 f₁ s x
-- Mathlib.Topology.Category.TopCat.GrothendieckTopology
TopCat.instSmallPrecoverage : TopCat.precoverage.Small
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_X_p : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (α : Type u_3)
  [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α]
  (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.down α))) (n : α),
  (((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).functor.obj P).X n).p = P.p.f n
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_diff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k fallback : α},
  (t₁ \ t₂).getD k fallback = if k ∈ t₂ then fallback else t₁.getD k fallback
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k a : α} {v : β k},
  (t.insert k v).getKey! a = if cmp k a = Ordering.eq then k else t.getKey! a
-- Mathlib.Computability.PartrecBasis
Nat.Partrec'.below.prim : ∀ {motive : {n : ℕ} → (a : List.Vector ℕ n →. ℕ) → Nat.Partrec' a → Prop} {n : ℕ} {f : List.Vector ℕ n → ℕ}
  (a : Nat.Primrec' f), Nat.Partrec'.below ⋯
-- Mathlib.CategoryTheory.Sites.MayerVietorisSquare
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.SheafCondition.ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] {S : J.MayerVietorisSquare}
  {P : CategoryTheory.Functor Cᵒᵖ (Type v')},
  S.SheafCondition P →
    ∀ {x y : P.obj (Opposite.op S.X₄)},
      (CategoryTheory.ConcreteCategory.hom (P.map S.f₂₄.op)) x =
          (CategoryTheory.ConcreteCategory.hom (P.map S.f₂₄.op)) y →
        (CategoryTheory.ConcreteCategory.hom (P.map S.f₃₄.op)) x =
            (CategoryTheory.ConcreteCategory.hom (P.map S.f₃₄.op)) y →
          x = y
-- Std.Net.Addr
/-- This structure represents the address: `octets[0]:octets[1]:octets[2]:octets[3]:octets[4]:octets[5]`.
 -/
Std.Net.MACAddr.octets : Std.Net.MACAddr → Vector UInt8 6
-- Mathlib.RingTheory.PolynomialAlgebra
/-- The `A`-algebra isomorphism `A[X] ≃ₐ[A] A ⊗[R] R[X]` (when `A` is commutative).  -/
polyEquivTensor' : (R : Type u_1) →
  [inst : CommSemiring R] →
    (A : Type u_4) →
      [inst_1 : CommSemiring A] → [inst_2 : Algebra R A] → Polynomial A ≃ₐ[A] TensorProduct R A (Polynomial R)
-- Mathlib.LinearAlgebra.Prod
LinearMap.fst_prod : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃), LinearMap.fst R M₂ M₃ ∘ₗ f.prod g = f
-- Init.Data.Order.Lemmas
Std.instMaxSubtypeOfMaxEqOr : {α : Type u} → [inst : Max α] → [Std.MaxEqOr α] → {P : α → Prop} → Max (Subtype P)
-- Mathlib.Topology.EMetricSpace.VariationOnFromTo
variationOnFromTo.eq_zero_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α},
  LocallyBoundedVariationOn f s →
    ∀ {a b : α},
      a ∈ s →
        b ∈ s →
          (variationOnFromTo f s a b = 0 ↔
            ∀ ⦃x : α⦄, x ∈ s ∩ Set.uIcc a b → ∀ ⦃y : α⦄, y ∈ s ∩ Set.uIcc a b → edist (f x) (f y) = 0)
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.DBuilderName.elab : Lean.Syntax → Aesop.ElabM Aesop.Frontend.DBuilderName
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- The map `u ↦ f • u` is an isometry between the `L^1` spaces for `μ.withDensity f` and `μ`.  -/
MeasureTheory.withDensitySMulLI : {α : Type u_1} →
  {m : MeasurableSpace α} →
    (μ : MeasureTheory.Measure α) →
      {E : Type u_8} →
        [inst : NormedAddCommGroup E] →
          [inst_1 : NormedSpace ℝ E] →
            {f : α → NNReal} →
              Measurable f → ↥(MeasureTheory.Lp E 1 (μ.withDensity fun x => ↑(f x))) →ₗᵢ[ℝ] ↥(MeasureTheory.Lp E 1 μ)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
IsCyclic.image_range_orderOf : ∀ {α : Type u_1} {a : α} [inst : Group α] [inst_1 : Fintype α] [inst_2 : DecidableEq α],
  (∀ (x : α), x ∈ Subgroup.zpowers a) → Finset.image (fun i => a ^ i) (Finset.range (orderOf a)) = Finset.univ
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.factor.eq_1 : ∀ {K : Type v} [inst : Field K] (f : Polynomial K),
  f.factor = if H : ∃ g, Irreducible g ∧ g ∣ f then Classical.choose H else Polynomial.X
-- Mathlib.Algebra.Category.Ring.Constructions
CommRingCat.Limits.π_isLocalHom : ∀ {J : Type u'} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat)
  {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (j : J),
  (∀ (x : ↑c.pt),
      IsUnit ((CategoryTheory.ConcreteCategory.hom (c.π.app j)) x) →
        ∀ (i : J),
          ∃ k f g,
            IsLocalHom (CommRingCat.Hom.hom (F.map f)) ∧
              (CategoryTheory.ConcreteCategory.hom (F.map f)) ((CategoryTheory.ConcreteCategory.hom (c.π.app i)) x) =
                (CategoryTheory.ConcreteCategory.hom (F.map g)) ((CategoryTheory.ConcreteCategory.hom (c.π.app j)) x)) →
    IsLocalHom (CommRingCat.Hom.hom (c.π.app j))
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Feature.builder.inj : ∀ {b b_1 : Aesop.Frontend.DBuilderName}, Aesop.Frontend.Feature.builder b = Aesop.Frontend.Feature.builder b_1 → b = b_1
-- Mathlib.CategoryTheory.Monoidal.CommMon_
/-- `mapCommMon` is functorial in the lax braided functor.  -/
CategoryTheory.Functor.mapCommMonFunctor : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        (D : Type u₂) →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.MonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                CategoryTheory.Functor (CategoryTheory.LaxBraidedFunctor C D)
                  (CategoryTheory.Functor (CategoryTheory.CommMon C) (CategoryTheory.CommMon D))
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
/-- For a given compact subset `C` of `I → Bool`, `spanFunctor` is the functor from the poset of finsets
of `I` to `Profinite`, sending a finite subset set `J` to the image of `C` under the projection
`Proj J`.
 -/
Profinite.NobelingProof.spanFunctor : {I : Type u} →
  {C : Set (I → Bool)} →
    [(s : Finset I) → (i : I) → Decidable (i ∈ s)] → IsCompact C → CategoryTheory.Functor (Finset I)ᵒᵖ Profinite
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.Lean.parseLowerHex?.match_1.congr_eq_2 : ∀ (motive : Option ℕ → Sort u_1) (x : Option ℕ) (h_1 : (d : ℕ) → motive (some d)) (h_2 : Unit → motive none),
  x = none →
    (match x with
      | some d => h_1 d
      | none => h_2 ()) ≍
      h_2 ()
-- Mathlib.RingTheory.Perfection
Perfection.coeff_pow_p' : ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [inst_1 : CharP R p] (f : Perfection R p)
  (n : ℕ), (Perfection.coeff R p (n + 1)) f ^ p = (Perfection.coeff R p n) f
-- Batteries.Data.AssocList
/-- `O(n)`. Returns the first entry in the list whose key is equal to `a`.  -/
Batteries.AssocList.findEntry? : {α : Type u_1} → {β : Type u_2} → [BEq α] → α → Batteries.AssocList α β → Option (α × β)
-- Mathlib.CategoryTheory.Skeletal
/-- Applying `map F` and then `fromThinSkeleton` is isomorphic to first applying `fromThinSkeleton`
and then applying `F`.
 -/
CategoryTheory.ThinSkeleton.mapCompFromThinSkeletonIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : Quiver.IsThin C] →
          [inst_3 : Quiver.IsThin D] →
            (F : CategoryTheory.Functor C D) →
              (CategoryTheory.ThinSkeleton.map F).comp (CategoryTheory.ThinSkeleton.fromThinSkeleton D) ≅
                (CategoryTheory.ThinSkeleton.fromThinSkeleton C).comp F
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.smul_oreDiv : ∀ {R : Type u_1} {M : Type u_3} {X : Type u_4} [inst : Monoid M] {S : Submonoid M} [inst_1 : OreLocalization.OreSet S]
  [inst_2 : MulAction M X] [inst_3 : SMul R X] [inst_4 : SMul R M] [inst_5 : IsScalarTower R M M]
  [inst_6 : IsScalarTower R M X] (r : R) (x : X) (s : ↥S),
  r • (x /ₒ s) = OreLocalization.oreNum (r • 1) s • x /ₒ OreLocalization.oreDenom (r • 1) s
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_insert_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF → ∀ {k : α} {v : β}, Std.DHashMap.Internal.Raw₀.Const.get? (m.insert k v) k = some v
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toArray_roc_eq_add : ∀ {m n : ℤ} {i : ℕ}, i < (n - m).toNat → (m<...=n).toArray[i]! = m + 1 + ↑i
-- Lean.Elab.BuiltinCommand
/-- Auxiliary method for processing binder annotation update commands:
`variable (α)`, `variable {α}`, `variable ⦃α⦄`, and `variable [α]`.
The argument `binder` is the binder of the `variable` command.
The method returns an array containing the "residue", that is, variables that do not correspond to updates.
Recall that a `bracketedBinder` can be of the form `(x y)`.
```
variable {α β : Type}
variable (α γ)
```
The second `variable` command updates the binder annotation for `α`, and returns "residue" `γ`.
 -/
_private.Lean.Elab.BuiltinCommand.0.Lean.Elab.Command.replaceBinderAnnotation : Lean.TSyntax `Lean.Parser.Term.bracketedBinder →
  Lean.Elab.Command.CommandElabM (Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder))
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.instInhabited : {G : Type u_1} → [inst : AddGroup G] → Inhabited (AddSubgroup G)
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.isoHom_inv_id_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory}
  (e : X ≅ Y) {Z : C} (h : X.obj ⟶ Z),
  CategoryTheory.CategoryStruct.comp e.hom.hom (CategoryTheory.CategoryStruct.comp e.inv.hom h) = h
-- Batteries.Lean.LawfulMonadLift
StateRefT'.lift_bind : ∀ {m : Type → Type} {α β ω σ : Type} [inst : Monad m] (ma : m α) (f : α → m β),
  StateRefT'.lift (ma >>= f) = do
    let a ← StateRefT'.lift ma
    StateRefT'.lift (f a)
-- Mathlib.RepresentationTheory.Homological.Resolution
/-- The projective resolution of `k` as a trivial `k`-linear `G`-representation with `n`th
differential `(Gⁿ⁺¹ →₀ k[G]) → (Gⁿ →₀ k[G])` sending `(g₀, ..., gₙ)` to
`g₀·(g₁, ..., gₙ) + ∑ (-1)ʲ⁺¹·(g₀, ..., gⱼgⱼ₊₁, ..., gₙ) + (-1)ⁿ⁺¹·(g₀, ..., gₙ₋₁)` for
`j = 0, ..., n - 1`.  -/
Rep.barComplex : (k G : Type u) → [inst : CommRing k] → [inst_1 : Group G] → ChainComplex (Rep.{u, u, u} k G) ℕ
-- Mathlib.Analysis.Normed.Group.Defs
NormedCommGroup.toCommGroup : {E : Type u_8} → [self : NormedCommGroup E] → CommGroup E
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.eq_zero_or_eq_zero_of_mul_eq_zero : ∀ {d : ℕ} [dnsq : Zsqrtd.Nonsquare d] {a b : ℤ√↑d}, a * b = 0 → a = 0 ∨ b = 0
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.le_stabilizer_vadd_left : ∀ {G : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : AddAction G β]
  [inst_3 : VAdd α β] [VAddAssocClass G α β] (a : α) (b : β), AddAction.stabilizer G a ≤ AddAction.stabilizer G (a +ᵥ b)
-- Mathlib.Tactic.Linter.Lint
/-- Linter that check that all `deprecated` tags come with `since` dates.  -/
Batteries.Tactic.Lint.deprecatedNoSince : Batteries.Tactic.Lint.Linter
-- Mathlib.Dynamics.TopologicalEntropy.Subset
Dynamics.coverEntropy_closure : ∀ {X : Type u_1} {T : X → X} {F : Set X} [inst : UniformSpace X],
  Continuous T → Dynamics.coverEntropy T (closure F) = Dynamics.coverEntropy T F
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.Algebra.Hom.ext_iff : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {T : CategoryTheory.Monad C} {A B : T.Algebra}
  {x y : A.Hom B}, x = y ↔ x.f = y.f
-- Mathlib.Tactic.NormNum.Ineq
Mathlib.Meta.NormNum.isRat_le_true : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α} {na nb : ℤ} {da db : ℕ},
  Mathlib.Meta.NormNum.IsRat a na da →
    Mathlib.Meta.NormNum.IsRat b nb db → decide (na.mul (Int.ofNat db) ≤ nb.mul (Int.ofNat da)) = true → a ≤ b
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulMonC_nc.go.eq_def : ∀ (k : ℤ) (m : Lean.Grind.CommRing.Mon) (c : ℕ) (p acc : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.mulMonC_nc.go k m c p acc =
    match p with
    | Lean.Grind.CommRing.Poly.num k' => Lean.Grind.CommRing.Poly.insert (k * k' % ↑c) m acc
    | Lean.Grind.CommRing.Poly.add k' m' p =>
      Lean.Grind.CommRing.Poly.mulMonC_nc.go k m c p (Lean.Grind.CommRing.Poly.insert (k * k' % ↑c) (m.mul_nc m') acc)
-- Mathlib.LinearAlgebra.Matrix.Notation
injective_pair_iff_ne : ∀ {α : Type u_1} {x y : α}, Function.Injective ![x, y] ↔ x ≠ y
-- Init.Data.UInt.Lemmas
UInt8.toBitVec_toUInt32 : ∀ (n : UInt8), n.toUInt32.toBitVec = BitVec.setWidth 32 n.toBitVec
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedBilinearMap.isBoundedLinearMap_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F] [inst_5 : SeminormedAddCommGroup G]
  [inst_6 : Module 𝕜 G] {f : E × F → G}, IsBoundedBilinearMap 𝕜 f → ∀ (x : E), IsBoundedLinearMap 𝕜 fun y => f (x, y)
-- Lean.Widget.InteractiveDiagnostic
/-- Nested tags are ignored, show nested text as-is.  -/
_private.Lean.Widget.InteractiveDiagnostic.0.Lean.Widget.EmbedFmt.ignoreTags : Lean.Widget.EmbedFmt✝
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RocSliceData.mk.injEq : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (treeMap : Std.DTreeMap.Internal.Impl α β) (range : Std.Roc α)
  (treeMap_1 : Std.DTreeMap.Internal.Impl α β) (range_1 : Std.Roc α),
  ({ treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 }) =
    (treeMap = treeMap_1 ∧ range = range_1)
-- Mathlib.Algebra.BigOperators.WithTop
/-- A product of finite terms is finite.  -/
WithTop.prod_lt_top : ∀ {ι : Type u_1} {M₀ : Type u_3} [inst : CommMonoidWithZero M₀] [inst_1 : NoZeroDivisors M₀] [inst_2 : Nontrivial M₀]
  [inst_3 : DecidableEq M₀] {s : Finset ι} {f : ι → WithTop M₀} [inst_4 : LT M₀], (∀ i ∈ s, f i < ⊤) → ∏ i ∈ s, f i < ⊤
-- Mathlib.CategoryTheory.Limits.FintypeCat
CategoryTheory.Limits.FintypeCat.instHasLimitsOfShapeFintypeCatOfFinCategory : ∀ {J : Type} [inst : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J],
  CategoryTheory.Limits.HasLimitsOfShape J FintypeCat
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_ofList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List ((a : α) × β a)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
      k ∈ List.map Sigma.fst l → (Std.ExtDHashMap.ofList l).getKey? k' = some k
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
/-- The operator norm on `CStarMatrix m n A`.  -/
CStarMatrix.instNorm : {m : Type u_1} →
  {n : Type u_2} →
    {A : Type u_5} →
      [Fintype m] →
        [inst : NonUnitalCStarAlgebra A] →
          [inst_1 : PartialOrder A] → [StarOrderedRing A] → [Fintype n] → Norm (CStarMatrix m n A)
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- Given two left-invariant measures which are finite on
compacts, they coincide in the following sense: they give the same value to the integral of
continuous compactly supported functions, up to a multiplicative constant.  -/
MeasureTheory.Measure.exists_integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [BorelSpace G] (μ' μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure]
  [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsAddLeftInvariant],
  ∃ c, ∀ (f : G → ℝ), Continuous f → HasCompactSupport f → ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂c • μ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.sin_sub_pi : ∀ (x : ℂ), Complex.sin (x - ↑Real.pi) = -Complex.sin x
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.isNonZero : Nat.Internal.Linear.Poly → Bool