mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.Lean.Name.demangleAux.match_4.splitter : (s : String) →
  (motive : Char → Option (s.Pos × ℕ) → Sort u_1) →
    (ch : Char) →
      (x : Option (s.Pos × ℕ)) →
        ((q : s.Pos) → (v : ℕ) → x = some (q, v) → motive 'u' (some (q, v))) →
          ((x_1 : Char) →
              (x_2 : Option (s.Pos × ℕ)) →
                (∀ (q : s.Pos) (v : ℕ), x_1 = 'u' → x_2 = some (q, v) → False) → x = x_2 → motive x_1 x_2) →
            motive ch x
-- Lean.Parser.Syntax
Lean.Parser.Command.macro_rules.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.coe_toLinearMap : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W) (f : ρ.IntertwiningMap σ), ⇑f.toLinearMap = ⇑f
-- Init.Data.Order.PackageFactories
Std.Packages.LinearPreorderOfOrdArgs.decidableLT : {α : Type u} →
  (self : Std.Packages.LinearPreorderOfOrdArgs α) →
    let this := self.ord;
    let this := self.lt;
    let this_1 := self.le;
    have this_2 := ⋯;
    have this_3 := ⋯;
    DecidableLT α
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
IsCyclotomicExtension.Rat.galEquivZMod_smul_of_pow_eq : ∀ (n : ℕ) [inst : NeZero n] (K : Type u_1) [inst_1 : Field K] [inst_2 : NumberField K]
  [hK : IsCyclotomicExtension {n} ℚ K] (σ : Gal(K/ℚ)) {x : NumberField.RingOfIntegers K},
  x ^ n = 1 → σ • x = x ^ (↑((IsCyclotomicExtension.Rat.galEquivZMod n K) σ)).val
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.size_insertMany_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List (α × β)},
      List.Pairwise (fun a b => (a.1 == b.1) = false) l →
        (∀ a ∈ m, (List.map Prod.fst l).contains a = false) →
          (Std.DHashMap.Raw.Const.insertMany m l).size = m.size + l.length
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.instEssSurjHomotopyCategoryIntUpQh : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C], DerivedCategory.Qh.EssSurj
-- Mathlib.Data.Finsupp.WellFounded
Finsupp.Lex.wellFoundedLT_of_finite : ∀ {α : Type u_1} {N : Type u_2} [inst : Zero N] [inst_1 : LinearOrder α] [Finite α] [inst_3 : LT N]
  [hwf : WellFoundedLT N], WellFoundedLT (Lex (α →₀ N))
-- Mathlib.Tactic.ClickSuggestions.SectionState
/-- Create the HTML corresponding to `s`.  -/
Mathlib.Tactic.ClickSuggestions.renderSection : {α : Type} →
  String →
    Mathlib.Tactic.ClickSuggestions.SectionKind → Mathlib.Tactic.ClickSuggestions.SectionState α → ProofWidgets.Html
-- Lean.Data.Lsp.Internal
/-- Identifier (potentially partial) to query.  -/
Lean.Lsp.LeanModuleQuery.identifier : Lean.Lsp.LeanModuleQuery → String
-- Mathlib.CategoryTheory.Filtered.Small
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsFiltered.FilteredClosureSmall.InductiveStep.max.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {n : ℕ} {X : (k : ℕ) → k < n → (t : Type (max v w)) × (t → C)}
  {k k' : ℕ} {hk : k < n} {hk' : k' < n} {a : (X k hk).fst} {a_1 : (X k' hk').fst} {k_1 k'_1 : ℕ} {hk_1 : k_1 < n}
  {hk'_1 : k'_1 < n} {a_2 : (X k_1 hk_1).fst} {a_3 : (X k'_1 hk'_1).fst},
  CategoryTheory.IsFiltered.FilteredClosureSmall.InductiveStep.max✝ hk hk' a a_1 =
      CategoryTheory.IsFiltered.FilteredClosureSmall.InductiveStep.max✝ hk_1 hk'_1 a_2 a_3 →
    k = k_1 ∧ k' = k'_1 ∧ a ≍ a_2 ∧ a_1 ≍ a_3
-- Mathlib.Data.Nat.Nth
Nat.nth_add : ∀ {p : ℕ → Prop} {m n : ℕ}, (∀ k < m, ¬p k) → Nat.nth p n ≠ 0 → Nat.nth (fun i => p (i + m)) n + m = Nat.nth p n
-- Mathlib.Topology.MetricSpace.PartitionOfUnity
/-- Let `X` be a metric space. Let `K : ι → Set X` be a locally finite family of closed sets, let
`U : ι → Set X` be a family of open sets such that `K i ⊆ U i` for all `i`. Then there exists a
positive continuous function `δ : C(X, ℝ)` such that for any `i` and `x ∈ K i`, we have
`Metric.closedBall x (δ x) ⊆ U i`.  -/
Metric.exists_continuous_real_forall_closedBall_subset : ∀ {ι : Type u_1} {X : Type u_2} [inst : MetricSpace X] {K U : ι → Set X},
  (∀ (i : ι), IsClosed (K i)) →
    (∀ (i : ι), IsOpen (U i)) →
      (∀ (i : ι), K i ⊆ U i) →
        LocallyFinite K → ∃ δ, (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, Metric.closedBall x (δ x) ⊆ U i
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.toLax_mapComp' : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (fg : b₀ ⟶ b₂)
  (h : autoParam (CategoryTheory.CategoryStruct.comp f g = fg) CategoryTheory.Pseudofunctor.toLax_mapComp'._auto_1),
  F.toLax.mapComp' f g fg h = (F.mapComp' f g fg h).inv
-- Mathlib.Tactic.ProdAssoc
/-- Given two expressions corresponding to iterated products of the same types, associated in
possibly different ways, this constructs the "obvious" function from one to the other.  -/
Lean.Expr.mkProdFun : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.UInt.Lemmas
UInt8.toBitVec_add : ∀ {a b : UInt8}, (a + b).toBitVec = a.toBitVec + b.toBitVec
-- Lean.Meta.Tactic.Simp.Types
/-- Converts `Simp.Config` into `Meta.ConfigWithKey` used for `isDefEq`.
 -/
_private.Lean.Meta.Tactic.Simp.Types.0.Lean.Meta.Simp.mkMetaConfig : Lean.Meta.Simp.Config → Lean.MetaM Lean.Meta.ConfigWithKey
-- Mathlib.Order.NonemptyFiniteChains
PartialOrder.NonemptyFiniteChains.le_iff : ∀ {X : Type u_1} [inst : PartialOrder X] (A B : PartialOrder.NonemptyFiniteChains X), A ≤ B ↔ A.finset ⊆ B.finset
-- Mathlib.Algebra.Group.Action.Units
Units.smul_mk_apply : ∀ {M : Type u_6} {α : Type u_7} [inst : Monoid M] [inst_1 : SMul M α] (m n : M) (h₁ : m * n = 1) (h₂ : n * m = 1)
  (a : α), { val := m, inv := n, val_inv := h₁, inv_val := h₂ } • a = m • a
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.alter.match_3.eq_2 : ∀ (motive : Ordering → Sort u_1) (h_1 : Ordering.gt = Ordering.lt → motive Ordering.lt)
  (h_2 : Ordering.gt = Ordering.gt → motive Ordering.gt) (h_3 : Ordering.gt = Ordering.eq → motive Ordering.eq),
  (match h : Ordering.gt with
    | Ordering.lt => h_1 h
    | Ordering.gt => h_2 h
    | Ordering.eq => h_3 h) =
    h_2 ⋯
-- Mathlib.Algebra.Lie.Basic
LinearMap.instLieModule : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M]
  [inst_6 : LieModule R L M] [inst_7 : AddCommGroup N] [inst_8 : Module R N] [inst_9 : LieRingModule L N]
  [inst_10 : LieModule R L N], LieModule R L (M →ₗ[R] N)
-- Mathlib.Analysis.Analytic.Constructions
/-- Eta-expanded form of `Finset.analyticOnNhd_sum`

---

Finite sums of analytic functions are analytic  -/
Finset.analyticOnNhd_fun_sum : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {f : α → E → F} {s : Set E} (N : Finset α),
  (∀ n ∈ N, AnalyticOnNhd 𝕜 (f n) s) → AnalyticOnNhd 𝕜 (fun a => ∑ c ∈ N, f c a) s
-- Init.Prelude
/-- Executes an action from a monad with a read-only value in the underlying monad `m`.
 -/
ReaderT.run : {ρ : Type u} → {m : Type u → Type v} → {α : Type u} → ReaderT ρ m α → ρ → m α
-- Mathlib.Analysis.Normed.Group.Pointwise
inv_cthickening : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (s : Set E),
  (Metric.cthickening δ s)⁻¹ = Metric.cthickening δ s⁻¹
-- Std.Sat.AIG.Cached
Std.Sat.AIG.mkGateCached.go : {α : Type} →
  [inst : Hashable α] → [inst_1 : DecidableEq α] → (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α
-- Mathlib.Data.Set.Finite.Lattice
Set.Finite.preimage' : ∀ {α : Type u} {β : Type v} {f : α → β} {s : Set β}, s.Finite → (∀ b ∈ s, (f ⁻¹' {b}).Finite) → (f ⁻¹' s).Finite
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.eq_d₃₂_comp_inv : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₃ A).inv ((groupHomology.inhomogeneousChains A).d 3 2) =
    CategoryTheory.CategoryStruct.comp (groupHomology.d₃₂ A) (groupHomology.chainsIso₂ A).inv
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.map_powers : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_4} {F : Type u_5} [inst_1 : Monoid N] [inst_2 : FunLike F M N]
  [inst_3 : MonoidHomClass F M N] (f : F) (m : M), Submonoid.map f (Submonoid.powers m) = Submonoid.powers (f m)
-- Lean.Meta.Match.Basic
/-- Right-hand-side of the alternative.
 -/
Lean.Meta.Match.Alt.rhs : Lean.Meta.Match.Alt → Lean.Expr
-- Mathlib.Analysis.Calculus.FDeriv.Const
hasFDerivAtFilter_natCast : ∀ {𝕜 : 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] [inst_7 : NatCast F] (n : ℕ) (L : Filter (E × E)), HasFDerivAtFilter (↑n) 0 L
-- Mathlib.Data.Finsupp.Defs
Finsupp.support_eq_empty : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] {f : α →₀ M}, f.support = ∅ ↔ f = 0
-- Mathlib.CategoryTheory.Sites.Continuous
/-- The action of a natural transformation on pushforward functors of sheaves.  -/
CategoryTheory.Functor.sheafPushforwardContinuousNatTrans : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F F' : CategoryTheory.Functor C D} →
          (F ⟶ F') →
            (A : Type u) →
              [inst_2 : CategoryTheory.Category.{t, u} A] →
                (J : CategoryTheory.GrothendieckTopology C) →
                  (K : CategoryTheory.GrothendieckTopology D) →
                    [inst_3 : F.IsContinuous J K] →
                      [inst_4 : F'.IsContinuous J K] →
                        F'.sheafPushforwardContinuous A J K ⟶ F.sheafPushforwardContinuous A J K
-- Mathlib.RingTheory.RingHom.QuasiFinite
RingHom.QuasiFinite.eq_1 : ∀ {R : Type u_4} {S : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  f.QuasiFinite = Algebra.QuasiFinite R S
-- Mathlib.RingTheory.Extension.Presentation.Basic
/-- If `S` is the localization of `R` away from `r`, we can construct a natural
presentation of `S` as `R`-algebra with a single generator `X` and the relation `r * X - 1 = 0`.  -/
Algebra.Presentation.localizationAway : {R : Type u} →
  (S : Type v) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] → (r : R) → [IsLocalization.Away r S] → Algebra.Presentation R S Unit Unit
-- Mathlib.AlgebraicGeometry.Sites.Pretopology
/-- **Alias** of the forward direction of `AlgebraicGeometry.Scheme.mem_pretopology_iff`. -/
AlgebraicGeometry.Scheme.exists_cover_of_mem_pretopology : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  [inst_1 : P.IsMultiplicative] {X : AlgebraicGeometry.Scheme} {R : CategoryTheory.Presieve X},
  R ∈ (AlgebraicGeometry.Scheme.pretopology P).coverings X → ∃ 𝒰, R = CategoryTheory.Presieve.ofArrows 𝒰.X 𝒰.f
-- Mathlib.Topology.Homeomorph.Defs
/-- If a bijective map `e : X ≃ Y` is continuous and open, then it is a homeomorphism.  -/
Equiv.toHomeomorphOfContinuousClosed : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → (e : X ≃ Y) → Continuous ⇑e → IsClosedMap ⇑e → X ≃ₜ Y
-- Mathlib.Logic.Equiv.Defs
/-- The sort of maps to `PUnit.{v}` is equivalent to `PUnit.{w}`.  -/
Equiv.arrowPUnitEquivPUnit : (α : Sort u_1) → (α → PUnit.{v}) ≃ PUnit.{w}
-- Mathlib.Tactic.FunProp.ToBatteries
/-- For `(x₀, .., xₙ₋₁)` return `xᵢ` but as a product projection.

We need to know the total size of the product to be considered.

For example for `xyz : X × Y × Z`
- `mkProdProj xyz 1 3` returns `xyz.snd.fst`.
- `mkProdProj xyz 1 2` returns `xyz.snd`.
 -/
Mathlib.Meta.FunProp.mkProdProj : Lean.Expr → ℕ → ℕ → Lean.MetaM Lean.Expr
-- Mathlib.Data.NNRat.BigOperators
NNRat.cast_multisetProd : ∀ {K : Type u_2} [inst : Semifield K] [CharZero K] (s : Multiset ℚ≥0), ↑s.prod = (Multiset.map NNRat.cast s).prod
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
CategoryTheory.epi_of_effectiveEpi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : Y ⟶ X) [CategoryTheory.EffectiveEpi f],
  CategoryTheory.Epi f
-- Mathlib.Topology.Compactness.Compact
IsCompact.sigma_exists_finite_sigma_eq : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] (u : Set ((i : ι) × X i)),
  IsCompact u → ∃ s t, s.Finite ∧ (∀ (i : ι), IsCompact (t i)) ∧ s.sigma t = u
-- Lean.Setup
Lean.ModuleArtifacts.ir? : Lean.ModuleArtifacts → Option System.FilePath
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Ideal.IsHomogeneous.iSup : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_5 : GradedRing 𝒜] {κ : Sort u_4}
  {f : κ → Ideal A}, (∀ (i : κ), Ideal.IsHomogeneous 𝒜 (f i)) → Ideal.IsHomogeneous 𝒜 (⨆ i, f i)
-- Mathlib.Algebra.Order.Field.Basic
le_of_one_div_le_one_div : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a b : α},
  0 < a → 1 / a ≤ 1 / b → b ≤ a
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.End.addOppositeEquiv_apply : ∀ {M : Type u_2} [inst : AddMonoid M] (f : M →ₑ[id] M), AddActionHom.End.addOppositeEquiv f = f 0
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.Trimmed.cons : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {exp : ℝ}
  {coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl}
  {tl : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl},
  coef.Trimmed → ¬coef.IsZero → (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef tl).Trimmed
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.getFlag.asFlag : Lean.Syntax → Option (Lean.TSyntax `ident × Bool)
-- Mathlib.CategoryTheory.Sites.Plus
CategoryTheory.GrothendieckTopology.plusMap_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q R : CategoryTheory.Functor Cᵒᵖ D}
  (η : P ⟶ Q) (γ : Q ⟶ R),
  J.plusMap (CategoryTheory.CategoryStruct.comp η γ) = CategoryTheory.CategoryStruct.comp (J.plusMap η) (J.plusMap γ)
-- Mathlib.Data.Multiset.Defs
Multiset.subset_of_le : ∀ {α : Type u_1} {s t : Multiset α}, s ≤ t → s ⊆ t
-- Mathlib.LinearAlgebra.Ray
instNonemptyRayVectorOfNontrivial : ∀ {R : Type u_1} {M : Type u_2} [inst : Zero M] [Nontrivial M], Nonempty (RayVector R M)
-- Mathlib.Topology.UniformSpace.Equicontinuity
Equicontinuous.eq_1 : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] (F : ι → X → α),
  Equicontinuous F = ∀ (x₀ : X), EquicontinuousAt F x₀
-- Mathlib.Topology.Compactness.Lindelof
/-- The neighborhood filter of a Lindelöf set is disjoint with a filter `l` with the countable
intersection property if and only if the neighborhood filter of each point of this set
is disjoint with `l`.  -/
IsLindelof.disjoint_nhdsSet_left : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {l : Filter X} [CountableInterFilter l],
  IsLindelof s → (Disjoint (nhdsSet s) l ↔ ∀ x ∈ s, Disjoint (nhds x) l)
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.map_shiftFunctorComm_hom_app : ∀ {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] (F : CategoryTheory.Functor C D) {B : Type u_5}
  [inst_2 : AddCommMonoid B] [inst_3 : CategoryTheory.HasShift C B] [inst_4 : CategoryTheory.HasShift D B]
  [inst_5 : F.CommShift B] (X : C) (a b : B),
  F.map ((CategoryTheory.shiftFunctorComm C a b).hom.app X) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.commShiftIso F b).hom.app ((CategoryTheory.shiftFunctor C a).obj X))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor D b).map ((CategoryTheory.Functor.commShiftIso F a).hom.app X))
        (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorComm D a b).hom.app (F.obj X))
          (CategoryTheory.CategoryStruct.comp
            ((CategoryTheory.shiftFunctor D a).map ((CategoryTheory.Functor.commShiftIso F b).inv.app X))
            ((CategoryTheory.Functor.commShiftIso F a).inv.app ((CategoryTheory.shiftFunctor C b).obj X)))))
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.instFunLike.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Top α] [inst_2 : Min β] [inst_3 : Top β],
  InfTopHom.instFunLike = { coe := fun f => f.toFun, coe_injective := ⋯ }
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.additiveObjIsoBiproduct_hom_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.Preadditive D]
  (F : CategoryTheory.Functor (CategoryTheory.Mat_ C) D) [inst_4 : F.Additive] (M : CategoryTheory.Mat_ C) (i : M.ι),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Mat_.additiveObjIsoBiproduct F M).hom
      (CategoryTheory.Limits.biproduct.π (fun i => F.obj ((CategoryTheory.Mat_.embedding C).obj (M.X i))) i) =
    F.map
      (CategoryTheory.CategoryStruct.comp M.isoBiproductEmbedding.hom
        (CategoryTheory.Limits.biproduct.π (fun i => (CategoryTheory.Mat_.embedding C).obj (M.X i)) i))
-- Mathlib.Data.Finset.Card
Finset.card_range : ∀ (n : ℕ), (Finset.range n).card = n
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.sum_eq_multiset_sum : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] (s : Finset ι) (f : ι → M),
  ∑ x ∈ s, f x = (Multiset.map f s.val).sum
-- Mathlib.Algebra.Order.Archimedean.Basic
Multiplicative.instMulArchimedean : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : PartialOrder G] [Archimedean G], MulArchimedean (Multiplicative G)
-- Mathlib.Tactic.NormNum.Core
/-- The extension should be run in the `post` phase when used as simp plugin.  -/
Mathlib.Meta.NormNum.NormNumExt.post : Mathlib.Meta.NormNum.NormNumExt → Bool
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
/-- Auxiliary definition for `transfiniteComposition.wellOrderInductionData`.  -/
CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.lift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : LinearOrder J] →
        [inst_2 : OrderBot J] →
          {F : CategoryTheory.Functor J C} →
            {c : CategoryTheory.Limits.Cocone F} →
              {X Y : C} →
                {p : X ⟶ Y} →
                  {f : F.obj ⊥ ⟶ X} →
                    {g : c.pt ⟶ Y} →
                      [F.IsWellOrderContinuous] →
                        {j : J} →
                          Order.IsSuccLimit j →
                            ↑(⋯.functor.op.comp
                                    (CategoryTheory.HasLiftingProperty.transfiniteComposition.sqFunctor c p f
                                      g)).sections →
                              (CategoryTheory.HasLiftingProperty.transfiniteComposition.sqFunctor c p f g).obj
                                (Opposite.op j)
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int16.instHasModelBitVecOfNatNat : HasModel✝ Int16 (BitVec 16)
-- Mathlib.Analysis.InnerProductSpace.Calculus
contDiffWithinAt_euclidean : ∀ {𝕜 : Type u_1} {ι : Type u_2} {H : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup H]
  [inst_2 : NormedSpace 𝕜 H] {f : H → EuclideanSpace 𝕜 ι} {t : Set H} {y : H} [inst_3 : Fintype ι] {n : WithTop ℕ∞},
  ContDiffWithinAt 𝕜 n f t y ↔ ∀ (i : ι), ContDiffWithinAt 𝕜 n (fun x => (f x).ofLp i) t y
-- Mathlib.AlgebraicTopology.DoldKan.NCompGamma
AlgebraicTopology.DoldKan.Γ₂N₁.natTrans_app_f_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] (X : CategoryTheory.SimplicialObject C)
  (Δ : SimplexCategoryᵒᵖ),
  (AlgebraicTopology.DoldKan.Γ₂N₁.natTrans.app X).f.app Δ =
    (AlgebraicTopology.DoldKan.Γ₀.splitting (AlgebraicTopology.AlternatingFaceMapComplex.obj X)).desc Δ fun A =>
      CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f (Opposite.unop A.fst).len) (X.map A.e.op)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.RotateRight
Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastRotateRight : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (target : aig.ShiftTarget w)
  (assign : α → Bool) (idx : ℕ) (hidx : idx < w),
  ⟦assign,
      { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateRight aig target).aig,
        ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateRight aig target).vec.get idx hidx }⟧ =
    if hidx2 : idx < w - target.distance % w then
      ⟦assign, { aig := aig, ref := target.vec.get (target.distance % w + idx) ⋯ }⟧
    else ⟦assign, { aig := aig, ref := target.vec.get (idx - (w - target.distance % w)) ⋯ }⟧
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.ι_pre : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C)
  [inst_3 : CategoryTheory.Limits.HasColimit F] (E : CategoryTheory.Functor K J)
  [inst_4 : CategoryTheory.Limits.HasColimit (E.comp F)] (k : K),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (E.comp F) k)
      (CategoryTheory.Limits.colimit.pre F E) =
    CategoryTheory.Limits.colimit.ι F (E.obj k)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKeyD_insertMany_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k k' fallback : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l → (Std.ExtDHashMap.Const.insertMany m l).getKeyD k' fallback = k
-- Lean.Meta.Tactic.Grind.Arith.Simproc
Lean.Meta.Grind.Arith.normPowRatInt : Lean.Meta.Simp.DSimproc
-- Mathlib.GroupTheory.Coxeter.Length
/-- The proposition that `ω` is reduced; that is, it has minimal length among all words that
represent the same element of `W`.  -/
CoxeterSystem.IsReduced : {B : Type u_1} → {W : Type u_2} → [inst : Group W] → {M : CoxeterMatrix B} → CoxeterSystem M W → List B → Prop
-- Mathlib.RingTheory.FractionalIdeal.Basic
/-- `coeIdealHom (S : Submonoid R) P` is `(↑) : Ideal R → FractionalIdeal S P` as a ring hom  -/
FractionalIdeal.coeIdealHom : {R : Type u_1} →
  [inst : CommRing R] →
    (S : Submonoid R) →
      (P : Type u_2) → [inst_1 : CommRing P] → [inst_2 : Algebra R P] → Ideal R →+* FractionalIdeal S P
-- Mathlib.Topology.Algebra.Monoid
ContinuousMap.mulLeft.eq_1 : ∀ {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : Mul X] [inst_2 : SeparatelyContinuousMul X] (x : X),
  ContinuousMap.mulLeft x = { toFun := fun x_1 => x * x_1, continuous_toFun := ⋯ }
-- Mathlib.Data.Bundle
Bundle.instNonemptyPullback : ∀ {B : Type u_1} {E : B → Type u_3} {B' : Type u_4} {f : B' → B} {x : B'} [Nonempty (E (f x))], Nonempty ((f *ᵖ E) x)
-- Init.Data.Range.Basic
Membership.mem.upper : ∀ {i : ℕ} {r : Std.Legacy.Range}, i ∈ r → i < r.stop