mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.DeriveEncodable
_private.Mathlib.Tactic.DeriveEncodable.0.Mathlib.Deriving.Encodable.S.brecOn.go : {motive : Mathlib.Deriving.Encodable.S✝ → Sort u} →
  (t : Mathlib.Deriving.Encodable.S✝) →
    ((t : Mathlib.Deriving.Encodable.S✝) → Mathlib.Deriving.Encodable.S.below✝ t → motive t) →
      motive t ×' Mathlib.Deriving.Encodable.S.below✝ t
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
/-- The approximations of the greatest fixed point stabilize at a fixed point of `f`  -/
OrdinalApprox.gfpApprox_eq_of_mem_fixedPoints : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α} {a b : Ordinal.{u}},
  a ≤ b →
    OrdinalApprox.gfpApprox f x a ∈ Function.fixedPoints ⇑f →
      OrdinalApprox.gfpApprox f x b = OrdinalApprox.gfpApprox f x a
-- Mathlib.Algebra.Notation.Pi.Basic
Pi.mulSingle.congr_simp : ∀ {ι : Type u_1} {M : ι → Type u_6} [inst : (i : ι) → One (M i)] {inst_1 : DecidableEq ι} [inst_2 : DecidableEq ι]
  (i : ι) (x x_1 : M i), x = x_1 → ∀ (j : ι), Pi.mulSingle i x j = Pi.mulSingle i x_1 j
-- Mathlib.Data.Set.Image
/-- **Alias** of the reverse direction of `Set.range_eq_univ`. -/
Function.Surjective.range_eq : ∀ {α : Type u_1} {ι : Sort u_4} {f : ι → α}, Function.Surjective f → Set.range f = Set.univ
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Biprod.ofComponents_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C} (f₁₁ : X₁ ⟶ Y₁) (f₁₂ : X₁ ⟶ Y₂)
  (f₂₁ : X₂ ⟶ Y₁) (f₂₂ : X₂ ⟶ Y₂) (g₁₁ : Y₁ ⟶ Z₁) (g₁₂ : Y₁ ⟶ Z₂) (g₂₁ : Y₂ ⟶ Z₁) (g₂₂ : Y₂ ⟶ Z₂),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂)
      (CategoryTheory.Biprod.ofComponents g₁₁ g₁₂ g₂₁ g₂₂) =
    CategoryTheory.Biprod.ofComponents
      (CategoryTheory.CategoryStruct.comp f₁₁ g₁₁ + CategoryTheory.CategoryStruct.comp f₁₂ g₂₁)
      (CategoryTheory.CategoryStruct.comp f₁₁ g₁₂ + CategoryTheory.CategoryStruct.comp f₁₂ g₂₂)
      (CategoryTheory.CategoryStruct.comp f₂₁ g₁₁ + CategoryTheory.CategoryStruct.comp f₂₂ g₂₁)
      (CategoryTheory.CategoryStruct.comp f₂₁ g₁₂ + CategoryTheory.CategoryStruct.comp f₂₂ g₂₂)
-- Mathlib.Tactic.Translate.Core
_private.Mathlib.Tactic.Translate.Core.0.Mathlib.Tactic.Translate.applyReplacementFun.visitApp : Mathlib.Tactic.Translate.TranslateData → Lean.Expr → Mathlib.Tactic.Translate.ReplacementM Lean.Expr
-- Mathlib.RingTheory.Polynomial.Subring
Polynomial.toSubring_zero : ∀ {R : Type u_1} [inst : Ring R] (T : Subring R), Polynomial.toSubring 0 T ⋯ = 0
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
CategoryTheory.ObjectProperty.prop_of_isTerminal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})] (X : C) (hX : CategoryTheory.Limits.IsTerminal X),
  P X
-- Mathlib.Analysis.Calculus.ContDiff.WithLp
PiLp.contDiff_toLp : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → NormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] [inst_3 : Fintype ι]
  {p : ENNReal} [inst_4 : Fact (1 ≤ p)] {n : WithTop ℕ∞}, ContDiff 𝕜 n (WithLp.toLp p)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- The structural isomorphism `(c ⊗ c') ⊙ₗ d ≅ c ⊙ₗ (c' ⊙ₗ d)`.  -/
CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso : {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.MonoidalCategoryStruct C} →
          [self : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct C D] →
            (c c' : C) →
              (d : D) →
                CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj
                    (CategoryTheory.MonoidalCategoryStruct.tensorObj c c') d ≅
                  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c
                    (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c' d)
-- Init.Core
instDecidableIff : {p q : Prop} → [Decidable p] → [Decidable q] → Decidable (p ↔ q)
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiffOn_finsetProd : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : CommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffMul I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {s : Set M} {t : Finset ι}
  {f : ι → M → G}, (∀ i ∈ t, ContMDiffOn I' I n (f i) s) → ContMDiffOn I' I n (fun x => ∏ i ∈ t, f i x) s
-- Mathlib.Computability.RegularExpressions
_private.Mathlib.Computability.RegularExpressions.0.RegularExpression.matches'.match_1.eq_5 : ∀ {α : Type u_1} (motive : RegularExpression α → Sort u_2) (P Q : RegularExpression α)
  (h_1 : Unit → motive RegularExpression.zero) (h_2 : Unit → motive RegularExpression.epsilon)
  (h_3 : (a : α) → motive (RegularExpression.char a)) (h_4 : (P Q : RegularExpression α) → motive (P.plus Q))
  (h_5 : (P Q : RegularExpression α) → motive (P.comp Q)) (h_6 : (P : RegularExpression α) → motive P.star),
  (match P.comp Q with
    | RegularExpression.zero => h_1 ()
    | RegularExpression.epsilon => h_2 ()
    | RegularExpression.char a => h_3 a
    | P.plus Q => h_4 P Q
    | P.comp Q => h_5 P Q
    | P.star => h_6 P) =
    h_5 P Q
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
IsCyclic.val_inv_mulAutMulEquiv_apply : ∀ (G : Type u_2) [inst : Group G] [h : IsCyclic G] (a : MulAut G),
  ↑((IsCyclic.mulAutMulEquiv G) a)⁻¹ =
    (AddEquiv.symm
        (Multiplicative.toAdd
          ((MulAutMultiplicative (ZMod (Nat.card G)))
            ((zmodCyclicMulEquiv h).trans (MulEquiv.trans a (zmodCyclicMulEquiv h).symm)))))
      1
-- Init.Data.UInt.Lemmas
UInt16.toUInt8_toUInt64 : ∀ (n : UInt16), n.toUInt64.toUInt8 = n.toUInt8
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsMeasurableRatCDF.nonneg : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℚ → ℝ},
  ProbabilityTheory.IsMeasurableRatCDF f → ∀ (a : α) (q : ℚ), 0 ≤ f a q
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.contSupp.eq_5 : Turing.PartrecToTM2.contSupp Turing.PartrecToTM2.Cont'.halt = ∅
-- Mathlib.Algebra.Group.Equiv.Opposite
AddEquiv.neg'_apply : ∀ (G : Type u_3) [inst : SubtractionMonoid G], ⇑(AddEquiv.neg' G) = AddOpposite.op ∘ Neg.neg
-- Mathlib.Data.List.AList
AList.mem_keys : ∀ {α : Type u} {β : α → Type v} {a : α} {s : AList β}, a ∈ s ↔ a ∈ s.keys
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
AlgebraicGeometry.LocallyRingedSpace.homMk.congr_simp : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f f_1 : X.toSheafedSpace ⟶ Y.toSheafedSpace) (e_f : f = f_1)
  (h : ∀ (x : ↑X.toTopCat), IsLocalHom (CommRingCat.Hom.hom (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f.hom x))),
  AlgebraicGeometry.LocallyRingedSpace.homMk f h = AlgebraicGeometry.LocallyRingedSpace.homMk f_1 ⋯
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.toArray_toList : ∀ {α : Type u} {r : Std.Rco α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.Rxo.IsAlwaysFinite α], r.toList.toArray = r.toArray
-- Lean.Util.MonadCache
Lean.MonadStateCacheT.instMonadLift : {α β : Type} →
  {m : Type → Type} → [inst : BEq α] → [inst_1 : Hashable α] → [Monad m] → MonadLift m (Lean.MonadStateCacheT α β m)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.compMeasurePreservingₗᵢ_apply_coe : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {β : Type u_7} [inst_1 : MeasurableSpace β] {μb : MeasureTheory.Measure β}
  (𝕜 : Type u_8) [inst_2 : NormedRing 𝕜] [inst_3 : Module 𝕜 E] [inst_4 : IsBoundedSMul 𝕜 E] [inst_5 : Fact (1 ≤ p)]
  (f : α → β) (hf : MeasureTheory.MeasurePreserving f μ μb) (a : ↥(MeasureTheory.Lp E p μb)),
  ↑((MeasureTheory.Lp.compMeasurePreservingₗᵢ 𝕜 f hf) a) = (↑a).compMeasurePreserving f hf
-- Lean.Meta.Basic
Lean.Meta.instInhabitedParamInfo : Inhabited Lean.Meta.ParamInfo
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.isEmptyAlgEquiv_symm_apply : ∀ (R : Type u) {σ : Type u_1} [inst : CommSemiring R] [inst_1 : IsEmpty σ] (r : R),
  (MvPolynomial.isEmptyAlgEquiv R σ).symm r = MvPolynomial.C r
-- Mathlib.AlgebraicGeometry.Morphisms.Constructors
/-- A variant of `topologically_isZariskiLocalAtTarget`
that takes one iff statement instead of two implications.  -/
AlgebraicGeometry.topologically_isZariskiLocalAtTarget' : ∀ (P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop)
  [(AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P).RespectsIso],
  (∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u}
      (U : ι → TopologicalSpace.Opens β),
      TopologicalSpace.IsOpenCover U → Continuous f → (P f ↔ ∀ (i : ι), P ((U i).carrier.restrictPreimage f))) →
    AlgebraicGeometry.IsZariskiLocalAtTarget
      (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P)
-- Mathlib.Algebra.DirectSum.Internal
DirectSum.coe_of_mul_apply : ∀ {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [inst : DecidableEq ι] [inst_1 : Semiring R] [inst_2 : SetLike σ R]
  [inst_3 : AddSubmonoidClass σ R] (A : ι → σ) [inst_4 : AddCommMonoid ι] [inst_5 : PartialOrder ι]
  [CanonicallyOrderedAdd ι] [inst_7 : SetLike.GradedMonoid A] [inst_8 : Sub ι] [OrderedSub ι] [AddLeftReflectLE ι]
  {i : ι} (r : ↥(A i)) (r' : DirectSum ι fun i => ↥(A i)) (n : ι) [inst_11 : Decidable (i ≤ n)],
  ↑(((DirectSum.of (fun i => ↥(A i)) i) r * r') n) = if i ≤ n then ↑r * ↑(r' (n - i)) else 0
-- Mathlib.NumberTheory.Divisors
Nat.sortedLT_map_fst_divisorsAntidiagonalList : ∀ {n : ℕ}, (List.map Prod.fst n.divisorsAntidiagonalList).SortedLT
-- Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
/-- The map sending a matrix to the endomorphism it represents. This is an `R`-algebra morphism.  -/
Matrix.isRepresentation.toEnd : {ι : Type u_1} →
  [inst : Fintype ι] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] →
        (R : Type u_3) →
          [inst_2 : CommRing R] →
            [inst_3 : Module R M] →
              (b : ι → M) →
                [inst_4 : DecidableEq ι] →
                  Submodule.span R (Set.range b) = ⊤ → ↥(Matrix.isRepresentation R b) →ₐ[R] Module.End R M
-- Mathlib.Data.Finset.MulAntidiagonal
/-- `Finset.antidiagonal hs ht a` is the set of all pairs of an element in
`s` and an element in `t` that add to `a`, but its construction requires proofs that `s` and `t` are
well-ordered.  -/
Finset.antidiagonal : {α : Type u_1} →
  [inst : AddCommMonoid α] →
    [inst_1 : PartialOrder α] → [IsOrderedCancelAddMonoid α] → {s t : Set α} → s.IsPWO → t.IsPWO → α → Finset (α × α)
-- Mathlib.Combinatorics.Enumerative.Stirling
Nat.stirlingSecond_succ_succ : ∀ (n k : ℕ), (n + 1).stirlingSecond (k + 1) = (k + 1) * n.stirlingSecond (k + 1) + n.stirlingSecond k
-- Mathlib.Topology.ContinuousMap.Ideals
ContinuousMap.idealOfEmpty_eq_bot : ∀ {X : Type u_1} {R : Type u_2} [inst : TopologicalSpace X] [inst_1 : Semiring R] [inst_2 : TopologicalSpace R]
  [inst_3 : IsTopologicalSemiring R], ContinuousMap.idealOfSet R ∅ = ⊥
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.r_of_eq : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {x y : M × ↥S},
  ↑y.2 + x.1 = ↑x.2 + y.1 → (AddLocalization.r S) x y
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- The seminorm applied to a sum is dominated by the maximum of the function applied to the
addends.  -/
NonarchAddGroupSeminorm.add_le_max' : ∀ {G : Type u_6} [inst : AddGroup G] (self : NonarchAddGroupSeminorm G) (r s : G),
  self.toFun (r + s) ≤ max (self.toFun r) (self.toFun s)
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.subsingleton : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F},
  Subsingleton (CategoryTheory.Limits.IsColimit t)
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffSection.coe_add : ∀ {𝕜 : 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] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [inst_13 : VectorBundle 𝕜 F V] (s t : ContMDiffSection I F n V),
  ⇑(s + t) = ⇑s + ⇑t
-- Mathlib.Combinatorics.Graph.Simple
Graph.simple_iff : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β),
  G.Simple ↔ G.Loopless ∧ ∀ ⦃e f : β⦄ ⦃x y : α⦄, G.IsLink e x y → G.IsLink f x y → e = f
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- The canonical categorical commutative square in which `CategoricalPullback F G` sits.  -/
CategoryTheory.Limits.CategoricalPullback.catCommSq : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            (F : CategoryTheory.Functor A B) →
              (G : CategoryTheory.Functor C B) →
                CategoryTheory.CatCommSq (CategoryTheory.Limits.CategoricalPullback.π₁ F G)
                  (CategoryTheory.Limits.CategoricalPullback.π₂ F G) F G
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.type₁_simplex : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι)
  [inst_1 : P.IsProper] {j : ι} (c : f.Cell j),
  (SSet.Subcomplex.Pairing.RankFunction.Cell.type₁ f c).simplex =
    (CategoryTheory.ConcreteCategory.hom (c.ιSigmaStdSimplex.app (Opposite.op { len := c.dim + 1 })))
      (SSet.stdSimplex.objEquiv.symm
        (CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.op { len := c.dim + 1 }))))
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.equivProd_unitIso_hom_app_right : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1}))
  (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : CategoryTheory.Comma L R),
  ((CategoryTheory.Comma.equivProd L R).unitIso.hom.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.Topology.Algebra.OpenSubgroup
/-- Coercion from `OpenAddSubgroup G` to `Opens G`.  -/
OpenAddSubgroup.toOpens : {G : Type u_1} → [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → OpenAddSubgroup G → TopologicalSpace.Opens G
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.trans_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {a b c : C} (α : a ≅ b) (β : b ≅ c), Trans.trans α β = α ≪≫ β
-- Mathlib.Order.BooleanAlgebra.Defs
/-- For any `a`, `b`, `(a ⊓ b) ⊔ (a / b) = a`  -/
GeneralizedBooleanAlgebra.sup_inf_sdiff : ∀ {α : Type u} [self : GeneralizedBooleanAlgebra α] (a b : α), a ⊓ b ⊔ a \ b = a
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverEntropyEntourage_le_log_coverMincard_div : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X} {F : Set X} {n : ℕ},
  Set.MapsTo T F F →
    ∀ [U.IsSymm], n ≠ 0 → Dynamics.coverEntropyEntourage T F (U.comp U) ≤ (↑(Dynamics.coverMincard T F U n)).log / ↑n
-- Init.Grind.ToInt
Lean.Grind.IntInterval.nonEmpty.eq_1 : ∀ (lo hi : ℤ), (Lean.Grind.IntInterval.co lo hi).nonEmpty = decide (lo < hi)
-- Mathlib.Topology.Compactness.SigmaCompact
CompactExhaustion.subset_succ : ∀ {X : Type u_1} [inst : TopologicalSpace X] (K : CompactExhaustion X) (n : ℕ), K n ⊆ K (n + 1)
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ofArray.folder.eq_2 : ∀ {n : ℕ} (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))
  (map : Std.HashMap (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) Bool),
  Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ofArray.folder (some map) l =
    match map.getThenInsertIfNew? l.1 l.2 with
    | (val?, map) =>
      match val? with
      | some val' => if (l.2 != val') = true then none else some map
      | x => some map
-- Std.Data.Iterators.Lemmas.Producers.Slice
Std.Slice.foldM_iter : ∀ {γ : Type u} {α β : Type v} {δ : Type w} {init : δ} {m : Type w → Type w'} [inst : Monad m]
  [inst_1 : Std.ToIterator (Std.Slice γ) Id α β] [inst_2 : Std.Iterator α Id β] [inst_3 : Std.IteratorLoop α Id m]
  [Std.Iterators.Finite α Id] {s : Std.Slice γ} {f : δ → β → m δ},
  Std.Iter.foldM f init s.iter = Std.Slice.foldlM f init s
-- Mathlib.Tactic.CategoryTheory.Slice
/-- `slice_rhs a b => tac` zooms to the right-hand side, uses associativity for categorical
composition as needed, zooms in on the `a`-th through `b`-th morphisms, and invokes `tac`.
 -/
Mathlib.Tactic.Slice.sliceRHS : Lean.ParserDescr
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.lift₃.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Full] {A₁ A₂ A₃ : C} {X : D} {f₁ : F.obj A₁ ⟶ X}
  (hf₁ : F.relativelyRepresentable f₁) (f₂ : F.obj A₂ ⟶ X) (f₃ : F.obj A₃ ⟶ X)
  [inst_3 : CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)] [inst_4 : F.Faithful] {Z : C}
  (x₁ x₁_1 : Z ⟶ A₁) (e_x₁ : x₁ = x₁_1) (x₂ x₂_1 : Z ⟶ A₂) (e_x₂ : x₂ = x₂_1) (x₃ x₃_1 : Z ⟶ A₃) (e_x₃ : x₃ = x₃_1)
  (h₁₂ : CategoryTheory.CategoryStruct.comp (F.map x₁) f₁ = CategoryTheory.CategoryStruct.comp (F.map x₂) f₂)
  (h₁₃ : CategoryTheory.CategoryStruct.comp (F.map x₁) f₁ = CategoryTheory.CategoryStruct.comp (F.map x₃) f₃),
  hf₁.lift₃ f₂ f₃ x₁ x₂ x₃ h₁₂ h₁₃ = hf₁.lift₃ f₂ f₃ x₁_1 x₂_1 x₃_1 ⋯ ⋯
-- Init.Data.UInt.Basic
/-- Converts word-sized unsigned integers to 16-bit unsigned integers. Wraps around on overflow.

This function is overridden at runtime with an efficient implementation.
 -/
USize.toUInt16 : USize → UInt16
-- Mathlib.RingTheory.RegularLocalRing.Defs
IsRegularRing.isRegularLocalRing_localization : ∀ {R : Type u_2} {inst : CommRing R} [self : IsRegularRing R] (p : Ideal R) [inst_1 : p.IsPrime],
  IsRegularLocalRing (Localization.AtPrime p)
-- Lean.Parser.Command
Lean.Parser.Command.include.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- Reinterpret a `Subgroup` as a `Submonoid`.  -/
Subgroup.toSubmonoid : {G : Type u_3} → [inst : Group G] → Subgroup G → Submonoid G
-- Init.Data.Array.Lemmas
/-- Variant of `all_append` with a side condition for the `stop` argument.  -/
Array.all_append' : ∀ {α : Type u_1} {stop : ℕ} {f : α → Bool} {xs ys : Array α},
  stop = (xs ++ ys).size → (xs ++ ys).all f 0 stop = (xs.all f && ys.all f)
-- Mathlib.Order.OrderDual
Equiv.himp_def : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) [inst : HImp β] (a b : α), a ⇨ b = e.symm (e a ⇨ e b)
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegular.innerRegular : ∀ {α : Type u_1} {inst : MeasurableSpace α} {inst_1 : TopologicalSpace α} {μ : MeasureTheory.Measure α}
  [self : μ.InnerRegular], μ.InnerRegularWRT IsCompact MeasurableSet
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
csSup_Icc : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderSup α] {a b : α}, a ≤ b → sSup (Set.Icc a b) = b
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.Hom.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C}
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)}
  {D₁ D₂ : F.DescentData' sq sq₃} {hom : (i : ι) → D₁.obj i ⟶ D₂.obj i}
  {comm :
    autoParam
      (∀ (i₁ i₂ : ι),
        CategoryTheory.CategoryStruct.comp ((F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (hom i₁)) (D₂.hom i₁ i₂) =
          CategoryTheory.CategoryStruct.comp (D₁.hom i₁ i₂) ((F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.map (hom i₂)))
      CategoryTheory.Pseudofunctor.DescentData'.Hom.comm._autoParam}
  {hom_1 : (i : ι) → D₁.obj i ⟶ D₂.obj i}
  {comm_1 :
    autoParam
      (∀ (i₁ i₂ : ι),
        CategoryTheory.CategoryStruct.comp ((F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (hom_1 i₁)) (D₂.hom i₁ i₂) =
          CategoryTheory.CategoryStruct.comp (D₁.hom i₁ i₂) ((F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.map (hom_1 i₂)))
      CategoryTheory.Pseudofunctor.DescentData'.Hom.comm._autoParam},
  { hom := hom, comm := comm } = { hom := hom_1, comm := comm_1 } → hom = hom_1
-- Init.Data.Int.Lemmas
Int.add_neg_one : ∀ (i : ℤ), i + -1 = i - 1
-- Mathlib.Data.Finsupp.Multiset
Finsupp.instWellFoundedRelationNat : (ι : Type u_3) → WellFoundedRelation (ι →₀ ℕ)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} →
        (Q H : C) →
          (p : S.X₂ ⟶ Q) →
            (ι : H ⟶ Q) →
              (wp : CategoryTheory.CategoryStruct.comp S.f p = 0) →
                (hp : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ p wp)) →
                  (wι :
                      CategoryTheory.CategoryStruct.comp ι (hp.desc (CategoryTheory.Limits.CokernelCofork.ofπ S.g ⋯)) =
                        0) →
                    CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι ι wι) → S.RightHomologyData
-- Mathlib.CategoryTheory.Core
CategoryTheory.Iso.core_hom_app_iso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ≅ G) (X : CategoryTheory.Core C),
  (α.core.hom.app X).iso.inv = α.inv.app X.of
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.LoogleMatch.name : LeanSearchClient.LoogleMatch → String
-- Lean.Util.Diff
/-- A histogram for arrays maps each element to a count and, if applicable, an index. -/
Lean.Diff.Histogram : (α : Type u) → ℕ → ℕ → [BEq α] → [Hashable α] → Type (max u 0)
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardSliceSearcher.revMatchesAt_iff_isLongestRevMatchAt : ∀ {pat s : String.Slice} {pos : s.Pos},
  pat.isEmpty = false →
    (String.Slice.Pattern.Model.RevMatchesAt pat pos ↔
      ∃ (h : String.Pos.Raw.IsValidForSlice s (pos.offset.decreaseBy pat.utf8ByteSize)),
        String.Slice.Pattern.Model.IsLongestRevMatchAt pat (s.pos (pos.offset.decreaseBy pat.utf8ByteSize) h) pos)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get_union_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} (mem : m₂.contains k = true),
  Std.DHashMap.Const.get (m₁.union m₂) k ⋯ = Std.DHashMap.Const.get m₂ k mem
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.inl.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  AddMonoid.Coprod.inl =
    { toFun := fun x => AddMonoid.Coprod.mk (FreeAddMonoid.of (Sum.inl x)), map_zero' := ⋯, map_add' := ⋯ }